-- Self-contained Macaulay2 verifier:  t_4(u1..u4) certificate for e_9(x,y).
-- Run:  M2 --script verify_e9.m2
isLeaf = t -> not instance(t, List);
-- canonical string: fold commutativity by sorting children
canonStr = t -> if isLeaf t then toString t else ( a := canonStr t#0; b := canonStr t#1; "(" | (if a <= b then a | b else b | a) | ")" );
-- graft int-labelled shape with mapping us (HashTable label=>tree)
graft = (sh, us) -> if isLeaf sh then us#sh else {graft(sh#0,us), graft(sh#1,us)};
-- replace the single "*" leaf of O by block
substStar = (o, block) -> if isLeaf o then (if o === "*" then block else o) else {substStar(o#0,block), substStar(o#1,block)};

-- the 15 arity-4 commutative shapes (int leaves 1..4)
SHAPES = {{1,{2,{3,4}}}, {1,{{2,3},4}}, {1,{{2,4},3}}, {{1,2},{3,4}}, {{1,3},{2,4}}, {{1,{2,3}},4}, {{{1,2},3},4}, {{{1,3},2},4}, {{1,4},{2,3}}, {{1,{2,4}},3}, {{{1,2},4},3}, {{{1,4},2},3}, {{1,{3,4}},2}, {{{1,3},4},2}, {{{1,4},3},2}};

-- accumulate acc as MutableHashTable canonStr => QQ coeff
acc = new MutableHashTable;
addTerm = (key, c) -> ( if acc#?key then acc#key = acc#key + c else acc#key = c; );
-- one certificate term: coeff * context[O]( t_4(u1,u2,u3,u4) )
doTerm = (coeff, o, u1, u2, u3, u4) -> (
  us := hashTable{1=>u1, 2=>u2, 3=>u3, 4=>u4};
  for sh in SHAPES do (
    block := graft(sh, us);
    addTerm(canonStr substStar(o, block), coeff);
  ););

-- 482 certificate terms
doTerm(253/31500, {"*",{"y",{"y",{"y",{"y",{"y","x"}}}}}}, "y", "y", "y", "y");
doTerm(13/10500, {"*",{"y",{"y",{"y",{{"y","y"},"x"}}}}}, "y", "y", "y", "y");
doTerm(-19/25200, {"*",{"y",{"y",{{"y","y"},{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(17/5250, {"*",{"y",{{"y","y"},{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-1/21000, {"*",{"y",{{"y","y"},{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-2/1575, {"*",{{"y","y"},{"y",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(1/2800, {"*",{{"y","y"},{"y",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-47/16800, {"*",{{"y","y"},{{"y","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-1/1680, {"*",{{"y",{"y",{"y",{"y","y"}}}},"x"}}, "y", "y", "y", "y");
doTerm(-7/375, {"y",{"*",{"y",{"y",{"y",{"y","x"}}}}}}, "y", "y", "y", "y");
doTerm(41/21000, {"y",{"*",{"y",{"y",{{"y","y"},"x"}}}}}, "y", "y", "y", "y");
doTerm(-99/14000, {"y",{"*",{"y",{{"y","y"},{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(11/7000, {"y",{"*",{{"y","y"},{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(83/42000, {"y",{"*",{{"y","y"},{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-2/75, {"y",{"y",{"*",{"y",{"y",{"y","x"}}}}}}, "y", "y", "y", "y");
doTerm(61/42000, {"y",{"y",{"*",{"y",{{"y","y"},"x"}}}}}, "y", "y", "y", "y");
doTerm(-79/9000, {"y",{"y",{"*",{{"y","y"},{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-179/21000, {"y",{"y",{"y",{"*",{"y",{"y","x"}}}}}}, "y", "y", "y", "y");
doTerm(17/2625, {"y",{"y",{"y",{"*",{{"y","y"},"x"}}}}}, "y", "y", "y", "y");
doTerm(89/7875, {"y",{"y",{"y",{"y",{"*",{"y","x"}}}}}}, "y", "y", "y", "y");
doTerm(-13/7000, {"y",{"y",{"y",{"y",{"y",{"*","x"}}}}}}, "y", "y", "y", "y");
doTerm(131/42000, {"y",{"y",{"y",{"y",{{"*","y"},"x"}}}}}, "y", "y", "y", "y");
doTerm(-323/63000, {"y",{"y",{"y",{{"*","y"},{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-407/42000, {"y",{"y",{"y",{{"y","y"},{"*","x"}}}}}, "y", "y", "y", "y");
doTerm(37/7000, {"y",{"y",{"y",{{"*",{"y","y"}},"x"}}}}, "y", "y", "y", "y");
doTerm(37/21000, {"y",{"y",{"y",{{"y",{"*","y"}},"x"}}}}, "y", "y", "y", "y");
doTerm(-89/9000, {"y",{"y",{{"*","y"},{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-29/42000, {"y",{"y",{{"*","y"},{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(521/42000, {"y",{"y",{{"y","y"},{"*",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-13/10500, {"y",{"y",{{"y","y"},{"y",{"*","x"}}}}}, "y", "y", "y", "y");
doTerm(53/84000, {"y",{"y",{{"y","y"},{{"*","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(2/525, {"y",{"y",{{"*",{"y","y"}},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(2/1575, {"y",{"y",{{"y",{"*","y"}},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-31/6000, {"y",{"y",{{"y",{"y","y"}},{"*","x"}}}}, "y", "y", "y", "y");
doTerm(59/6300, {"y",{"y",{{"*",{"y",{"y","y"}}},"x"}}}, "y", "y", "y", "y");
doTerm(223/25200, {"y",{"y",{{"y",{"*",{"y","y"}}},"x"}}}, "y", "y", "y", "y");
doTerm(-13/25200, {"y",{"y",{{{"*","y"},{"y","y"}},"x"}}}, "y", "y", "y", "y");
doTerm(-997/63000, {"y",{{"*","y"},{"y",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(1/1400, {"y",{{"*","y"},{"y",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-221/126000, {"y",{{"*","y"},{{"y","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-41/4200, {"y",{{"y","y"},{"*",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-13/28000, {"y",{{"y","y"},{"*",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-11/2000, {"y",{{"y","y"},{"y",{"*",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(-1/1120, {"y",{{"y","y"},{"y",{{"*","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(11/6000, {"y",{{"y","y"},{{"*","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-1/480, {"y",{{"y","y"},{{"y","y"},{"*","x"}}}}, "y", "y", "y", "y");
doTerm(-1/700, {"y",{{"y","y"},{{"*",{"y","y"}},"x"}}}, "y", "y", "y", "y");
doTerm(-1/2100, {"y",{{"y","y"},{{"y",{"*","y"}},"x"}}}, "y", "y", "y", "y");
doTerm(-43/7000, {"y",{{"*",{"y","y"}},{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/1000, {"y",{{"*",{"y","y"}},{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-43/21000, {"y",{{"y",{"*","y"}},{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/3000, {"y",{{"y",{"*","y"}},{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-73/126000, {"y",{{"y",{"y","y"}},{"*",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/875, {"y",{{"y",{"y","y"}},{"y",{"*","x"}}}}, "y", "y", "y", "y");
doTerm(19/84000, {"y",{{"y",{"y","y"}},{{"*","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-2/225, {"y",{{"*",{"y",{"y","y"}}},{"y","x"}}}, "y", "y", "y", "y");
doTerm(-29/3600, {"y",{{"y",{"*",{"y","y"}}},{"y","x"}}}, "y", "y", "y", "y");
doTerm(1/1200, {"y",{{{"*","y"},{"y","y"}},{"y","x"}}}, "y", "y", "y", "y");
doTerm(-1/4200, {"y",{{"*",{"y",{"y",{"y","y"}}}},"x"}}, "y", "y", "y", "y");
doTerm(-31/25200, {"y",{{"y",{"*",{"y",{"y","y"}}}},"x"}}, "y", "y", "y", "y");
doTerm(-19/31500, {"y",{{"y",{"y",{"*",{"y","y"}}}},"x"}}, "y", "y", "y", "y");
doTerm(-1/10500, {"y",{{"y",{"y",{"y",{"*","y"}}}},"x"}}, "y", "y", "y", "y");
doTerm(1/5040, {"y",{{"y",{{"*","y"},{"y","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(1/4200, {"y",{{{"*","y"},{"y",{"y","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(-1/14000, {"y",{{{"y","y"},{"*",{"y","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(-1/7000, {"y",{{{"y","y"},{"y",{"*","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(-187/31500, {{"*","y"},{"y",{"y",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(1/3500, {{"*","y"},{"y",{"y",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-7/3600, {{"*","y"},{"y",{{"y","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-71/63000, {{"*","y"},{{"y","y"},{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/14000, {{"*","y"},{{"y","y"},{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(37/63000, {{"y","y"},{"*",{"y",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(13/42000, {{"y","y"},{"*",{"y",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-1/16800, {{"y","y"},{"*",{{"y","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-11/10500, {{"y","y"},{"y",{"*",{"y",{"y","x"}}}}}, "y", "y", "y", "y");
doTerm(1/2000, {{"y","y"},{"y",{"*",{{"y","y"},"x"}}}}, "y", "y", "y", "y");
doTerm(-13/21000, {{"y","y"},{"y",{"y",{"y",{"*","x"}}}}}, "y", "y", "y", "y");
doTerm(-1/1575, {{"y","y"},{"y",{{"*","y"},{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-1/2100, {{"y","y"},{"y",{{"y","y"},{"*","x"}}}}, "y", "y", "y", "y");
doTerm(1/1750, {{"y","y"},{"y",{{"*",{"y","y"}},"x"}}}, "y", "y", "y", "y");
doTerm(1/5250, {{"y","y"},{"y",{{"y",{"*","y"}},"x"}}}, "y", "y", "y", "y");
doTerm(-23/63000, {{"y","y"},{{"*","y"},{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(-1/6000, {{"y","y"},{{"*","y"},{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(1/350, {{"y","y"},{{"y","y"},{"*",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/750, {{"y","y"},{{"*",{"y","y"}},{"y","x"}}}, "y", "y", "y", "y");
doTerm(1/2250, {{"y","y"},{{"y",{"*","y"}},{"y","x"}}}, "y", "y", "y", "y");
doTerm(53/50400, {{"y","y"},{{"*",{"y",{"y","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(47/25200, {{"y","y"},{{"y",{"*",{"y","y"}}},"x"}}, "y", "y", "y", "y");
doTerm(41/50400, {{"y","y"},{{{"*","y"},{"y","y"}},"x"}}, "y", "y", "y", "y");
doTerm(-31/10500, {{"*",{"y","y"}},{"y",{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(3/7000, {{"*",{"y","y"}},{"y",{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-1/525, {{"*",{"y","y"}},{{"y","y"},{"y","x"}}}, "y", "y", "y", "y");
doTerm(-31/31500, {{"y",{"*","y"}},{"y",{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/7000, {{"y",{"*","y"}},{"y",{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-1/1575, {{"y",{"*","y"}},{{"y","y"},{"y","x"}}}, "y", "y", "y", "y");
doTerm(-17/7000, {{"y",{"y","y"}},{"*",{"y",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(13/42000, {{"y",{"y","y"}},{"*",{{"y","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-47/31500, {{"y",{"y","y"}},{"y",{"*",{"y","x"}}}}, "y", "y", "y", "y");
doTerm(1/5250, {{"y",{"y","y"}},{"y",{"y",{"*","x"}}}}, "y", "y", "y", "y");
doTerm(-1/2625, {{"y",{"y","y"}},{"y",{{"*","y"},"x"}}}, "y", "y", "y", "y");
doTerm(-13/12600, {{"y",{"y","y"}},{{"*","y"},{"y","x"}}}, "y", "y", "y", "y");
doTerm(17/8400, {{"*",{"y",{"y","y"}}},{"y",{"y","x"}}}, "y", "y", "y", "y");
doTerm(59/50400, {{"*",{"y",{"y","y"}}},{{"y","y"},"x"}}, "y", "y", "y", "y");
doTerm(11/12600, {{"y",{"*",{"y","y"}}},{"y",{"y","x"}}}, "y", "y", "y", "y");
doTerm(11/6300, {{"y",{"*",{"y","y"}}},{{"y","y"},"x"}}, "y", "y", "y", "y");
doTerm(-29/25200, {{{"*","y"},{"y","y"}},{"y",{"y","x"}}}, "y", "y", "y", "y");
doTerm(29/50400, {{{"*","y"},{"y","y"}},{{"y","y"},"x"}}, "y", "y", "y", "y");
doTerm(-1/2000, {{"y",{"y",{"y","y"}}},{"*",{"y","x"}}}, "y", "y", "y", "y");
doTerm(-1/2000, {{"y",{"y",{"y","y"}}},{"y",{"*","x"}}}, "y", "y", "y", "y");
doTerm(1/10500, {{"y",{"y",{"y","y"}}},{{"*","y"},"x"}}, "y", "y", "y", "y");
doTerm(1/4200, {{"*",{"y",{"y",{"y","y"}}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(17/25200, {{"y",{"*",{"y",{"y","y"}}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(-4/7875, {{"y",{"y",{"*",{"y","y"}}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(1/10500, {{"y",{"y",{"y",{"*","y"}}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(-19/25200, {{"y",{{"*","y"},{"y","y"}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(-1/4200, {{{"*","y"},{"y",{"y","y"}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(1/14000, {{{"y","y"},{"*",{"y","y"}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(1/7000, {{{"y","y"},{"y",{"*","y"}}},{"y","x"}}, "y", "y", "y", "y");
doTerm(1/144, {{"*",{"y",{"y",{"y",{"y","y"}}}}},"x"}, "y", "y", "y", "y");
doTerm(-1/240, {{"y",{"y",{"*",{"y",{"y","y"}}}}},"x"}, "y", "y", "y", "y");
doTerm(1/200, {{"y",{"y",{"y",{"*",{"y","y"}}}}},"x"}, "y", "y", "y", "y");
doTerm(-1/900, {{"y",{"y",{"y",{"y",{"*","y"}}}}},"x"}, "y", "y", "y", "y");
doTerm(1/240, {{"y",{"y",{{"*","y"},{"y","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(1/360, {{"y",{{"*","y"},{"y",{"y","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(1/600, {{"y",{{"y","y"},{"*",{"y","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(-1/1200, {{"y",{{"y","y"},{"y",{"*","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(-1/720, {{{"*","y"},{"y",{"y",{"y","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(-1/360, {{{"y","y"},{"*",{"y",{"y","y"}}}},"x"}, "y", "y", "y", "y");
doTerm(1/360, {{{"y","y"},{{"*","y"},{"y","y"}}},"x"}, "y", "y", "y", "y");
doTerm(1/600, {{{"*",{"y","y"}},{"y",{"y","y"}}},"x"}, "y", "y", "y", "y");
doTerm(1/1800, {{{"y",{"*","y"}},{"y",{"y","y"}}},"x"}, "y", "y", "y", "y");
doTerm(-1/4500, {"*",{"y",{"y",{"y",{"y","x"}}}}}, "y", "y", "y", {"y","y"});
doTerm(-3/7000, {"*",{"y",{"y",{{"y","y"},"x"}}}}, "y", "y", "y", {"y","y"});
doTerm(-19/25200, {"*",{"y",{{"y","y"},{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/750, {"*",{{"y","y"},{"y",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(-37/42000, {"*",{{"y","y"},{{"y","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(169/9000, {"y",{"*",{"y",{"y",{"y","x"}}}}}, "y", "y", "y", {"y","y"});
doTerm(1/525, {"y",{"*",{"y",{{"y","y"},"x"}}}}, "y", "y", "y", {"y","y"});
doTerm(517/63000, {"y",{"*",{{"y","y"},{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(-77/4500, {"y",{"y",{"*",{"y",{"y","x"}}}}}, "y", "y", "y", {"y","y"});
doTerm(17/5250, {"y",{"y",{"*",{{"y","y"},"x"}}}}, "y", "y", "y", {"y","y"});
doTerm(124/7875, {"y",{"y",{"y",{"*",{"y","x"}}}}}, "y", "y", "y", {"y","y"});
doTerm(-479/42000, {"y",{"y",{"y",{"y",{"*","x"}}}}}, "y", "y", "y", {"y","y"});
doTerm(37/21000, {"y",{"y",{"y",{{"*","y"},"x"}}}}, "y", "y", "y", {"y","y"});
doTerm(2/1575, {"y",{"y",{{"*","y"},{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(-157/84000, {"y",{"y",{{"y","y"},{"*","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(59/6300, {"y",{"y",{{"*",{"y","y"}},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(-43/21000, {"y",{{"*","y"},{"y",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/3000, {"y",{{"*","y"},{{"y","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(-11/1500, {"y",{{"y","y"},{"*",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/1120, {"y",{{"y","y"},{"y",{"*","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(-1/2100, {"y",{{"y","y"},{{"*","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(-2/225, {"y",{{"*",{"y","y"}},{"y","x"}}}, "y", "y", "y", {"y","y"});
doTerm(179/84000, {"y",{{"y",{"y","y"}},{"*","x"}}}, "y", "y", "y", {"y","y"});
doTerm(-1/4200, {"y",{{"*",{"y",{"y","y"}}},"x"}}, "y", "y", "y", {"y","y"});
doTerm(-31/25200, {"y",{{"y",{"*",{"y","y"}}},"x"}}, "y", "y", "y", {"y","y"});
doTerm(1/2625, {"y",{{"y",{"y",{"*","y"}}},"x"}}, "y", "y", "y", {"y","y"});
doTerm(1/10500, {"y",{{{"*","y"},{"y","y"}},"x"}}, "y", "y", "y", {"y","y"});
doTerm(-31/31500, {{"*","y"},{"y",{"y",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/7000, {{"*","y"},{"y",{{"y","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(-1/1575, {{"*","y"},{{"y","y"},{"y","x"}}}, "y", "y", "y", {"y","y"});
doTerm(-43/63000, {{"y","y"},{"*",{"y",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/1500, {{"y","y"},{"*",{{"y","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(1/1575, {{"y","y"},{"y",{"*",{"y","x"}}}}, "y", "y", "y", {"y","y"});
doTerm(1/5250, {{"y","y"},{"y",{{"*","y"},"x"}}}, "y", "y", "y", {"y","y"});
doTerm(1/2250, {{"y","y"},{{"*","y"},{"y","x"}}}, "y", "y", "y", {"y","y"});
doTerm(53/50400, {{"y","y"},{{"*",{"y","y"}},"x"}}, "y", "y", "y", {"y","y"});
doTerm(17/8400, {{"*",{"y","y"}},{"y",{"y","x"}}}, "y", "y", "y", {"y","y"});
doTerm(59/50400, {{"*",{"y","y"}},{{"y","y"},"x"}}, "y", "y", "y", {"y","y"});
doTerm(-1/4200, {{"y",{"y","y"}},{"*",{"y","x"}}}, "y", "y", "y", {"y","y"});
doTerm(1/1750, {{"y",{"y","y"}},{"y",{"*","x"}}}, "y", "y", "y", {"y","y"});
doTerm(1/4200, {{"*",{"y",{"y","y"}}},{"y","x"}}, "y", "y", "y", {"y","y"});
doTerm(17/25200, {{"y",{"*",{"y","y"}}},{"y","x"}}, "y", "y", "y", {"y","y"});
doTerm(-1/2625, {{"y",{"y",{"*","y"}}},{"y","x"}}, "y", "y", "y", {"y","y"});
doTerm(-1/10500, {{{"*","y"},{"y","y"}},{"y","x"}}, "y", "y", "y", {"y","y"});
doTerm(3/14000, {{"y",{"y",{"y","y"}}},{"*","x"}}, "y", "y", "y", {"y","y"});
doTerm(1/720, {{"*",{"y",{"y",{"y","y"}}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(-1/360, {{"y",{"*",{"y",{"y","y"}}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(-1/240, {{"y",{"y",{"*",{"y","y"}}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(1/225, {{"y",{"y",{"y",{"*","y"}}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(7/3600, {{"y",{{"*","y"},{"y","y"}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(1/1800, {{{"*","y"},{"y",{"y","y"}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(-1/360, {{{"y","y"},{"*",{"y","y"}}},"x"}, "y", "y", "y", {"y","y"});
doTerm(61/10500, {"*",{"y",{"y",{"y","x"}}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/5250, {"*",{"y",{{"y","y"},"x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(23/25200, {"*",{{"y","y"},{"y","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(27/1750, {"y",{"*",{"y",{"y","x"}}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/21000, {"y",{"*",{{"y","y"},"x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(43/4200, {"y",{"y",{"*",{"y","x"}}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-121/21000, {"y",{"y",{"y",{"*","x"}}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(13/12600, {"y",{"y",{{"*","y"},"x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/600, {"y",{{"*","y"},{"y","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(1/1200, {"y",{{"y","y"},{"*","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/3500, {"y",{{"*",{"y","y"}},"x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-37/63000, {"y",{{"y",{"*","y"}},"x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(29/12600, {{"*","y"},{"y",{"y","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-29/25200, {{"*","y"},{{"y","y"},"x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(17/7875, {{"y","y"},{"*",{"y","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(1/2625, {{"y","y"},{"y",{"*","x"}}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-41/25200, {{"y","y"},{{"*","y"},"x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(1/3500, {{"*",{"y","y"}},{"y","x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(107/63000, {{"y",{"*","y"}},{"y","x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(1/840, {{"y",{"y","y"}},{"*","x"}}, "y", "y", "y", {"y",{"y","y"}});
doTerm(1/900, {{"*",{"y",{"y","y"}}},"x"}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/600, {{"y",{"*",{"y","y"}}},"x"}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-19/1800, {{"y",{"y",{"*","y"}}},"x"}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-1/180, {{{"*","y"},{"y","y"}},"x"}, "y", "y", "y", {"y",{"y","y"}});
doTerm(-11/3150, {"*",{"y",{"y","x"}}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(-11/1575, {"*",{{"y","y"},"x"}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(29/900, {"y",{"*",{"y","x"}}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(-257/12600, {"y",{"y",{"*","x"}}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(17/6300, {"y",{{"*","y"},"x"}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(11/6300, {{"*","y"},{"y","x"}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(-73/12600, {{"y","y"},{"*","x"}}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(1/360, {{"*",{"y","y"}},"x"}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(-1/180, {{"y",{"*","y"}},"x"}, "y", "y", "y", {"y",{"y",{"y","y"}}});
doTerm(1/525, {"*",{"y","x"}}, "y", "y", "y", {"y",{"y",{"y",{"y","y"}}}});
doTerm(-1/525, {"y",{"*","x"}}, "y", "y", "y", {"y",{"y",{"y",{"y","y"}}}});
doTerm(1/360, {{"*","y"},"x"}, "y", "y", "y", {"y",{"y",{"y",{"y","y"}}}});
doTerm(1/180, {"*","x"}, "y", "y", "y", {"y",{"y",{"y",{"y",{"y","y"}}}}});
doTerm(-1/360, {"*","x"}, "y", "y", "y", {{"y","y"},{"y",{"y",{"y","y"}}}});
doTerm(-1/120, {"*",{"y",{"y",{"y",{"y",{"y","y"}}}}}}, "y", "y", "y", "x");
doTerm(3/200, {"y",{"y",{"*",{"y",{"y",{"y","y"}}}}}}, "y", "y", "y", "x");
doTerm(-13/700, {"y",{"y",{"y",{"*",{"y",{"y","y"}}}}}}, "y", "y", "y", "x");
doTerm(-479/21000, {"y",{"y",{"y",{"y",{"*",{"y","y"}}}}}}, "y", "y", "y", "x");
doTerm(199/10500, {"y",{"y",{"y",{"y",{"y",{"*","y"}}}}}}, "y", "y", "y", "x");
doTerm(-43/1500, {"y",{"y",{"y",{{"*","y"},{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(-31/3000, {"y",{"y",{{"*","y"},{"y",{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(-157/42000, {"y",{"y",{{"y","y"},{"*",{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(-53/21000, {"y",{"y",{{"y","y"},{"y",{"*","y"}}}}}, "y", "y", "y", "x");
doTerm(1/280, {"y",{{"y","y"},{"*",{"y",{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(1/560, {"y",{{"y","y"},{"y",{"*",{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(-1/420, {"y",{{"y","y"},{{"*","y"},{"y","y"}}}}, "y", "y", "y", "x");
doTerm(179/42000, {"y",{{"*",{"y","y"}},{"y",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(-1/300, {"y",{{"y",{"*","y"}},{"y",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(1/600, {{"y","y"},{"*",{"y",{"y",{"y","y"}}}}}, "y", "y", "y", "x");
doTerm(-13/10500, {{"y","y"},{"y",{"y",{"y",{"*","y"}}}}}, "y", "y", "y", "x");
doTerm(-1/1050, {{"y","y"},{"y",{{"*","y"},{"y","y"}}}}, "y", "y", "y", "x");
doTerm(3/7000, {{"*",{"y","y"}},{"y",{"y",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(-1/500, {{"y",{"*","y"}},{"y",{"y",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(1/420, {{"y",{"y","y"}},{"*",{"y",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(1/875, {{"y",{"y","y"}},{"y",{"*",{"y","y"}}}}, "y", "y", "y", "x");
doTerm(-3/3500, {{"y",{"y","y"}},{"y",{"y",{"*","y"}}}}, "y", "y", "y", "x");
doTerm(1/840, {{"y",{"y","y"}},{{"*","y"},{"y","y"}}}, "y", "y", "y", "x");
doTerm(319/63000, {"y",{"y",{"*",{"y",{"y","y"}}}}}, "y", "y", "y", {"y","x"});
doTerm(109/9000, {"y",{"y",{"y",{"*",{"y","y"}}}}}, "y", "y", "y", {"y","x"});
doTerm(53/875, {"y",{"y",{"y",{"y",{"*","y"}}}}}, "y", "y", "y", {"y","x"});
doTerm(409/12600, {"y",{"y",{{"*","y"},{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(-29/3150, {"y",{{"*","y"},{"y",{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(-113/6000, {"y",{{"y","y"},{"*",{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(-229/21000, {"y",{{"y","y"},{"y",{"*","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(-19/5250, {{"*","y"},{"y",{"y",{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(4/1575, {{"y","y"},{"*",{"y",{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(1/3150, {{"y","y"},{"y",{"*",{"y","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(-13/10500, {{"y","y"},{"y",{"y",{"*","y"}}}}, "y", "y", "y", {"y","x"});
doTerm(11/1575, {{"y","y"},{{"*","y"},{"y","y"}}}, "y", "y", "y", {"y","x"});
doTerm(-1/2100, {{"*",{"y","y"}},{"y",{"y","y"}}}, "y", "y", "y", {"y","x"});
doTerm(1/15750, {{"y",{"*","y"}},{"y",{"y","y"}}}, "y", "y", "y", {"y","x"});
doTerm(-1/500, {"*",{"y",{"y",{"y","y"}}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(2033/63000, {"y",{"*",{"y",{"y","y"}}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(-149/15750, {"y",{"y",{"*",{"y","y"}}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(1529/31500, {"y",{"y",{"y",{"*","y"}}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(1/10500, {"y",{{"*","y"},{"y","y"}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(-71/31500, {{"*","y"},{"y",{"y","y"}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(137/31500, {{"y","y"},{"*",{"y","y"}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(-17/15750, {{"y","y"},{"y",{"*","y"}}}, "y", "y", "y", {"y",{"y","x"}});
doTerm(3/7000, {"*",{"y",{"y",{"y","y"}}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(17/6000, {"y",{"*",{"y",{"y","y"}}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(23/8400, {"y",{"y",{"*",{"y","y"}}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(-113/10500, {"y",{"y",{"y",{"*","y"}}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(1/7000, {"y",{{"*","y"},{"y","y"}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(37/21000, {{"*","y"},{"y",{"y","y"}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(1/750, {{"y","y"},{"*",{"y","y"}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(1/1500, {{"y","y"},{"y",{"*","y"}}}, "y", "y", "y", {{"y","y"},"x"});
doTerm(23/2250, {"*",{"y",{"y","y"}}}, "y", "y", "y", {"y",{"y",{"y","x"}}});
doTerm(173/15750, {"y",{"*",{"y","y"}}}, "y", "y", "y", {"y",{"y",{"y","x"}}});
doTerm(293/4500, {"y",{"y",{"*","y"}}}, "y", "y", "y", {"y",{"y",{"y","x"}}});
doTerm(157/15750, {{"*","y"},{"y","y"}}, "y", "y", "y", {"y",{"y",{"y","x"}}});
doTerm(-4/2625, {"*",{"y",{"y","y"}}}, "y", "y", "y", {"y",{{"y","y"},"x"}});
doTerm(23/21000, {"y",{"*",{"y","y"}}}, "y", "y", "y", {"y",{{"y","y"},"x"}});
doTerm(47/3500, {"y",{"y",{"*","y"}}}, "y", "y", "y", {"y",{{"y","y"},"x"}});
doTerm(-1/5250, {{"*","y"},{"y","y"}}, "y", "y", "y", {"y",{{"y","y"},"x"}});
doTerm(19/12600, {"*",{"y",{"y","y"}}}, "y", "y", "y", {{"y","y"},{"y","x"}});
doTerm(-23/12600, {"y",{"*",{"y","y"}}}, "y", "y", "y", {{"y","y"},{"y","x"}});
doTerm(701/31500, {"y",{"y",{"*","y"}}}, "y", "y", "y", {{"y","y"},{"y","x"}});
doTerm(1/300, {{"*","y"},{"y","y"}}, "y", "y", "y", {{"y","y"},{"y","x"}});
doTerm(-1/300, {"*",{"y","y"}}, "y", "y", "y", {"y",{"y",{"y",{"y","x"}}}});
doTerm(-62/2625, {"y",{"*","y"}}, "y", "y", "y", {"y",{"y",{"y",{"y","x"}}}});
doTerm(-1/1750, {"*",{"y","y"}}, "y", "y", "y", {"y",{"y",{{"y","y"},"x"}}});
doTerm(-13/2625, {"y",{"*","y"}}, "y", "y", "y", {"y",{"y",{{"y","y"},"x"}}});
doTerm(-73/25200, {"*",{"y","y"}}, "y", "y", "y", {"y",{{"y","y"},{"y","x"}}});
doTerm(-547/12600, {"y",{"*","y"}}, "y", "y", "y", {"y",{{"y","y"},{"y","x"}}});
doTerm(-13/10500, {"*",{"y","y"}}, "y", "y", "y", {{"y","y"},{"y",{"y","x"}}});
doTerm(-89/2100, {"y",{"*","y"}}, "y", "y", "y", {{"y","y"},{"y",{"y","x"}}});
doTerm(-3/7000, {"*",{"y","y"}}, "y", "y", "y", {{"y","y"},{{"y","y"},"x"}});
doTerm(1/700, {"y",{"*","y"}}, "y", "y", "y", {{"y","y"},{{"y","y"},"x"}});
doTerm(1/600, {"*",{"y","y"}}, "y", "y", "y", {{"y",{"y",{"y","y"}}},"x"});
doTerm(19/750, {"y",{"*","y"}}, "y", "y", "y", {{"y",{"y",{"y","y"}}},"x"});
doTerm(-113/4500, {"*","y"}, "y", "y", "y", {"y",{"y",{"y",{"y",{"y","x"}}}}});
doTerm(-13/3500, {"*","y"}, "y", "y", "y", {"y",{"y",{"y",{{"y","y"},"x"}}}});
doTerm(-47/6300, {"*","y"}, "y", "y", "y", {"y",{"y",{{"y","y"},{"y","x"}}}});
doTerm(23/15750, {"*","y"}, "y", "y", "y", {"y",{{"y","y"},{"y",{"y","x"}}}});
doTerm(233/42000, {"*","y"}, "y", "y", "y", {"y",{{"y","y"},{{"y","y"},"x"}}});
doTerm(-83/10500, {"*","y"}, "y", "y", "y", {"y",{{"y",{"y",{"y","y"}}},"x"}});
doTerm(-367/31500, {"*","y"}, "y", "y", "y", {{"y","y"},{"y",{"y",{"y","x"}}}});
doTerm(3/1400, {"*","y"}, "y", "y", "y", {{"y","y"},{"y",{{"y","y"},"x"}}});
doTerm(17/3150, {"*","y"}, "y", "y", "y", {{"y","y"},{{"y","y"},{"y","x"}}});
doTerm(-281/63000, {"*","y"}, "y", "y", "y", {{"y",{"y",{"y","y"}}},{"y","x"}});
doTerm(-61/8400, {"*","y"}, "y", "y", "y", {{"y",{"y",{"y",{"y","y"}}}},"x"});
doTerm(1/45, "*", "y", "y", "y", {"y",{"y",{"y",{"y",{"y",{"y","x"}}}}}});
doTerm(31/10500, "*", "y", "y", "y", {"y",{"y",{"y",{"y",{{"y","y"},"x"}}}}});
doTerm(67/15750, "*", "y", "y", "y", {"y",{"y",{"y",{{"y","y"},{"y","x"}}}}});
doTerm(101/10500, "*", "y", "y", "y", {"y",{"y",{{"y","y"},{"y",{"y","x"}}}}});
doTerm(1/2100, "*", "y", "y", "y", {"y",{"y",{{"y","y"},{{"y","y"},"x"}}}});
doTerm(-11/5250, "*", "y", "y", "y", {"y",{"y",{{"y",{"y",{"y","y"}}},"x"}}});
doTerm(-257/31500, "*", "y", "y", "y", {"y",{{"y","y"},{"y",{"y",{"y","x"}}}}});
doTerm(-1/7000, "*", "y", "y", "y", {"y",{{"y","y"},{"y",{{"y","y"},"x"}}}});
doTerm(-19/2100, "*", "y", "y", "y", {"y",{{"y","y"},{{"y","y"},{"y","x"}}}});
doTerm(1/180, "*", "y", "y", "y", {"y",{{"y",{"y",{"y","y"}}},{"y","x"}}});
doTerm(-3/1400, "*", "y", "y", "y", {"y",{{"y",{"y",{"y",{"y","y"}}}},"x"}});
doTerm(-227/15750, "*", "y", "y", "y", {{"y","y"},{"y",{"y",{"y",{"y","x"}}}}});
doTerm(1/10500, "*", "y", "y", "y", {{"y","y"},{"y",{"y",{{"y","y"},"x"}}}});
doTerm(-79/12600, "*", "y", "y", "y", {{"y","y"},{"y",{{"y","y"},{"y","x"}}}});
doTerm(-3/1750, "*", "y", "y", "y", {{"y","y"},{{"y","y"},{"y",{"y","x"}}}});
doTerm(-1/875, "*", "y", "y", "y", {{"y","y"},{{"y","y"},{{"y","y"},"x"}}});
doTerm(1/1050, "*", "y", "y", "y", {{"y","y"},{{"y",{"y",{"y","y"}}},"x"}});
doTerm(13/1500, "*", "y", "y", "y", {{"y",{"y",{"y","y"}}},{"y",{"y","x"}}});
doTerm(1/3000, "*", "y", "y", "y", {{"y",{"y",{"y","y"}}},{{"y","y"},"x"}});
doTerm(37/6300, "*", "y", "y", "y", {{"y",{"y",{"y",{"y","y"}}}},{"y","x"}});
doTerm(-47/4200, "*", "y", "y", "y", {{"y",{"y",{"y",{"y",{"y","y"}}}}},"x"});
doTerm(-1/4200, "*", "y", "y", "y", {{{"y","y"},{"y",{"y",{"y","y"}}}},"x"});
doTerm(31/10500, {"*",{"y",{"y",{"y","x"}}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-3/7000, {"*",{"y",{{"y","y"},"x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(1/525, {"*",{{"y","y"},{"y","x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(43/7000, {"y",{"*",{"y",{"y","x"}}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/1000, {"y",{"*",{{"y","y"},"x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-2/525, {"y",{"y",{"*",{"y","x"}}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-37/7000, {"y",{"y",{"y",{"*","x"}}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(1/700, {"y",{{"y","y"},{"*","x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(1/14000, {"y",{{"*",{"y","y"}},"x"}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-3/7000, {"y",{{"y",{"*","y"}},"x"}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/750, {{"y","y"},{"*",{"y","x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/1750, {{"y","y"},{"y",{"*","x"}}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/14000, {{"*",{"y","y"}},{"y","x"}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(3/7000, {{"y",{"*","y"}},{"y","x"}}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/600, {{"*",{"y",{"y","y"}}},"x"}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/600, {{"y",{"*",{"y","y"}}},"x"}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-1/200, {{"y",{"y",{"*","y"}}},"x"}, "y", "y", {"y","y"}, {"y","y"});
doTerm(-29/8400, {"*",{"y",{"y","x"}}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(29/16800, {"*",{{"y","y"},"x"}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(1/400, {"y",{"*",{"y","x"}}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(-13/8400, {"y",{"y",{"*","x"}}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(1/1680, {"y",{{"*","y"},"x"}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(-19/8400, {{"*","y"},{"y","x"}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(41/16800, {{"y","y"},{"*","x"}}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(1/120, {{"*",{"y","y"}},"x"}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(1/80, {{"y",{"*","y"}},"x"}, "y", "y", {"y","y"}, {"y",{"y","y"}});
doTerm(-1/1400, {"*",{"y","x"}}, "y", "y", {"y","y"}, {"y",{"y",{"y","y"}}});
doTerm(1/1400, {"y",{"*","x"}}, "y", "y", {"y","y"}, {"y",{"y",{"y","y"}}});
doTerm(-1/48, {"*","x"}, "y", "y", {"y","y"}, {"y",{"y",{"y",{"y","y"}}}});
doTerm(31/2000, {"y",{"y",{"*",{"y",{"y","y"}}}}}, "y", "y", {"y","y"}, "x");
doTerm(407/14000, {"y",{"y",{"y",{"*",{"y","y"}}}}}, "y", "y", {"y","y"}, "x");
doTerm(-27/1400, {"y",{"y",{"y",{"y",{"*","y"}}}}}, "y", "y", {"y","y"}, "x");
doTerm(51/14000, {"y",{{"*","y"},{"y",{"y","y"}}}}, "y", "y", {"y","y"}, "x");
doTerm(1/160, {"y",{{"y","y"},{"*",{"y","y"}}}}, "y", "y", {"y","y"}, "x");
doTerm(17/7000, {{"*","y"},{"y",{"y",{"y","y"}}}}, "y", "y", {"y","y"}, "x");
doTerm(1/700, {{"y","y"},{"y",{"*",{"y","y"}}}}, "y", "y", {"y","y"}, "x");
doTerm(13/7000, {{"y","y"},{"y",{"y",{"*","y"}}}}, "y", "y", {"y","y"}, "x");
doTerm(17/7000, {"*",{"y",{"y",{"y","y"}}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(37/4200, {"y",{"*",{"y",{"y","y"}}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(-573/14000, {"y",{"y",{"*",{"y","y"}}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(-113/4200, {"y",{"y",{"y",{"*","y"}}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(13/10500, {{"*","y"},{"y",{"y","y"}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(-3/350, {{"y","y"},{"*",{"y","y"}}}, "y", "y", {"y","y"}, {"y","x"});
doTerm(73/21000, {"*",{"y",{"y","y"}}}, "y", "y", {"y","y"}, {"y",{"y","x"}});
doTerm(179/14000, {"y",{"*",{"y","y"}}}, "y", "y", {"y","y"}, {"y",{"y","x"}});
doTerm(-33/1400, {"y",{"y",{"*","y"}}}, "y", "y", {"y","y"}, {"y",{"y","x"}});
doTerm(-13/14000, {"*",{"y",{"y","y"}}}, "y", "y", {"y","y"}, {{"y","y"},"x"});
doTerm(39/28000, {"y",{"*",{"y","y"}}}, "y", "y", {"y","y"}, {{"y","y"},"x"});
doTerm(-33/2800, {"y",{"y",{"*","y"}}}, "y", "y", {"y","y"}, {{"y","y"},"x"});
doTerm(-103/21000, {"*",{"y","y"}}, "y", "y", {"y","y"}, {"y",{"y",{"y","x"}}});
doTerm(11/1400, {"y",{"*","y"}}, "y", "y", {"y","y"}, {"y",{"y",{"y","x"}}});
doTerm(1/1750, {"*",{"y","y"}}, "y", "y", {"y","y"}, {"y",{{"y","y"},"x"}});
doTerm(39/3500, {"y",{"*","y"}}, "y", "y", {"y","y"}, {"y",{{"y","y"},"x"}});
doTerm(1/5600, {"*",{"y","y"}}, "y", "y", {"y","y"}, {{"y","y"},{"y","x"}});
doTerm(1919/42000, {"y",{"*","y"}}, "y", "y", {"y","y"}, {{"y","y"},{"y","x"}});
doTerm(487/10500, {"*","y"}, "y", "y", {"y","y"}, {"y",{"y",{"y",{"y","x"}}}});
doTerm(11/7000, {"*","y"}, "y", "y", {"y","y"}, {"y",{"y",{{"y","y"},"x"}}});
doTerm(341/10500, {"*","y"}, "y", "y", {"y","y"}, {"y",{{"y","y"},{"y","x"}}});
doTerm(-43/10500, {"*","y"}, "y", "y", {"y","y"}, {{"y","y"},{"y",{"y","x"}}});
doTerm(-117/14000, {"*","y"}, "y", "y", {"y","y"}, {{"y","y"},{{"y","y"},"x"}});
doTerm(-149/3500, "*", "y", "y", {"y","y"}, {"y",{"y",{"y",{"y",{"y","x"}}}}});
doTerm(-29/7000, "*", "y", "y", {"y","y"}, {"y",{"y",{"y",{{"y","y"},"x"}}}});
doTerm(-7/1200, "*", "y", "y", {"y","y"}, {"y",{"y",{{"y","y"},{"y","x"}}}});
doTerm(-191/21000, "*", "y", "y", {"y","y"}, {"y",{{"y","y"},{"y",{"y","x"}}}});
doTerm(-2/875, "*", "y", "y", {"y","y"}, {"y",{{"y","y"},{{"y","y"},"x"}}});
doTerm(2/525, "*", "y", "y", {"y","y"}, {{"y","y"},{"y",{"y",{"y","x"}}}});
doTerm(-3/2800, "*", "y", "y", {"y","y"}, {{"y","y"},{"y",{{"y","y"},"x"}}});
doTerm(47/5600, "*", "y", "y", {"y","y"}, {{"y","y"},{{"y","y"},{"y","x"}}});
doTerm(1/560, "*", "y", "y", {"y","y"}, {{"y",{"y",{"y",{"y","y"}}}},"x"});
doTerm(-1/1400, {"*",{"y","x"}}, "y", "y", {"y",{"y","y"}}, {"y",{"y","y"}});
doTerm(1/1400, {"y",{"*","x"}}, "y", "y", {"y",{"y","y"}}, {"y",{"y","y"}});
doTerm(1/120, {{"*","y"},"x"}, "y", "y", {"y",{"y","y"}}, {"y",{"y","y"}});
doTerm(-1/120, {"*","x"}, "y", "y", {"y",{"y","y"}}, {"y",{"y",{"y","y"}}});
doTerm(1/1750, {"*",{"y",{"y",{"y","y"}}}}, "y", "y", {"y",{"y","y"}}, "x");
doTerm(19/14000, {"y",{"*",{"y",{"y","y"}}}}, "y", "y", {"y",{"y","y"}}, "x");
doTerm(53/14000, {"y",{"y",{"*",{"y","y"}}}}, "y", "y", {"y",{"y","y"}}, "x");
doTerm(-8/875, {"y",{"y",{"y",{"*","y"}}}}, "y", "y", {"y",{"y","y"}}, "x");
doTerm(9/7000, {{"*","y"},{"y",{"y","y"}}}, "y", "y", {"y",{"y","y"}}, "x");
doTerm(-11/4200, {"*",{"y",{"y","y"}}}, "y", "y", {"y",{"y","y"}}, {"y","x"});
doTerm(229/14000, {"y",{"*",{"y","y"}}}, "y", "y", {"y",{"y","y"}}, {"y","x"});
doTerm(-373/10500, {"y",{"y",{"*","y"}}}, "y", "y", {"y",{"y","y"}}, {"y","x"});
doTerm(17/10500, {"*",{"y","y"}}, "y", "y", {"y",{"y","y"}}, {"y",{"y","x"}});
doTerm(67/3000, {"y",{"*","y"}}, "y", "y", {"y",{"y","y"}}, {"y",{"y","x"}});
doTerm(-1/1000, {"*",{"y","y"}}, "y", "y", {"y",{"y","y"}}, {{"y","y"},"x"});
doTerm(-11/1750, {"y",{"*","y"}}, "y", "y", {"y",{"y","y"}}, {{"y","y"},"x"});
doTerm(-137/10500, {"*","y"}, "y", "y", {"y",{"y","y"}}, {"y",{"y",{"y","x"}}});
doTerm(1/1400, {"*","y"}, "y", "y", {"y",{"y","y"}}, {"y",{{"y","y"},"x"}});
doTerm(-167/42000, {"*","y"}, "y", "y", {"y",{"y","y"}}, {{"y","y"},{"y","x"}});
doTerm(-43/3500, "*", "y", "y", {"y",{"y","y"}}, {"y",{"y",{"y",{"y","x"}}}});
doTerm(1/3500, "*", "y", "y", {"y",{"y","y"}}, {"y",{"y",{{"y","y"},"x"}}});
doTerm(-43/8400, "*", "y", "y", {"y",{"y","y"}}, {"y",{{"y","y"},{"y","x"}}});
doTerm(-71/10500, "*", "y", "y", {"y",{"y","y"}}, {{"y","y"},{"y",{"y","x"}}});
doTerm(3/7000, "*", "y", "y", {"y",{"y","y"}}, {{"y","y"},{{"y","y"},"x"}});
doTerm(1/1400, {"*",{"y",{"y","y"}}}, "y", "y", {"y",{"y",{"y","y"}}}, "x");
doTerm(3/200, {"y",{"*",{"y","y"}}}, "y", "y", {"y",{"y",{"y","y"}}}, "x");
doTerm(-9/1400, {"y",{"y",{"*","y"}}}, "y", "y", {"y",{"y",{"y","y"}}}, "x");
doTerm(-1/120, {"*",{"y","y"}}, "y", "y", {"y",{"y",{"y","y"}}}, {"y","x"});
doTerm(29/4200, {"y",{"*","y"}}, "y", "y", {"y",{"y",{"y","y"}}}, {"y","x"});
doTerm(43/700, {"*","y"}, "y", "y", {"y",{"y",{"y","y"}}}, {"y",{"y","x"}});
doTerm(-1/100, {"*","y"}, "y", "y", {"y",{"y",{"y","y"}}}, {{"y","y"},"x"});
doTerm(31/1050, "*", "y", "y", {"y",{"y",{"y","y"}}}, {"y",{"y",{"y","x"}}});
doTerm(-3/700, "*", "y", "y", {"y",{"y",{"y","y"}}}, {"y",{{"y","y"},"x"}});
doTerm(2/105, "*", "y", "y", {"y",{"y",{"y","y"}}}, {{"y","y"},{"y","x"}});
doTerm(1/700, {"*",{"y","y"}}, "y", "y", {"y",{"y",{"y",{"y","y"}}}}, "x");
doTerm(83/1400, {"y",{"*","y"}}, "y", "y", {"y",{"y",{"y",{"y","y"}}}}, "x");
doTerm(-7/120, {"*","y"}, "y", "y", {"y",{"y",{"y",{"y","y"}}}}, {"y","x"});
doTerm(2/105, "*", "y", "y", {"y",{"y",{"y",{"y","y"}}}}, {"y",{"y","x"}});
doTerm(1/280, "*", "y", "y", {"y",{"y",{"y",{"y","y"}}}}, {{"y","y"},"x"});
doTerm(-1/56, {"*","y"}, "y", "y", {"y",{"y",{"y",{"y",{"y","y"}}}}}, "x");
doTerm(-9/280, "*", "y", "y", {"y",{"y",{"y",{"y",{"y","y"}}}}}, {"y","x"});
doTerm(1/60, "*", "y", "y", {"y",{"y",{"y",{"y",{"y",{"y","y"}}}}}}, "x");
doTerm(-11/12600, {"*",{"y",{"y","x"}}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(-11/6300, {"*",{{"y","y"},"x"}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(29/3600, {"y",{"*",{"y","x"}}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(-223/25200, {"y",{"y",{"*","x"}}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(13/12600, {"y",{{"*","y"},"x"}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(1/12600, {{"*","y"},{"y","x"}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(-47/25200, {{"y","y"},{"*","x"}}, "y", {"y","y"}, {"y","y"}, {"y","y"});
doTerm(-13/14000, {"*",{"y",{"y",{"y","y"}}}}, "y", {"y","y"}, {"y","y"}, "x");
doTerm(-99/14000, {"y",{"*",{"y",{"y","y"}}}}, "y", {"y","y"}, {"y","y"}, "x");
doTerm(13/3500, {"y",{"y",{"*",{"y","y"}}}}, "y", {"y","y"}, {"y","y"}, "x");
doTerm(87/3500, {"y",{"y",{"y",{"*","y"}}}}, "y", {"y","y"}, {"y","y"}, "x");
doTerm(-1/1750, {{"*","y"},{"y",{"y","y"}}}, "y", {"y","y"}, {"y","y"}, "x");
doTerm(2/525, {"*",{"y",{"y","y"}}}, "y", {"y","y"}, {"y","y"}, {"y","x"});
doTerm(33/2000, {"y",{"*",{"y","y"}}}, "y", {"y","y"}, {"y","y"}, {"y","x"});
doTerm(-223/7000, {"y",{"y",{"*","y"}}}, "y", {"y","y"}, {"y","y"}, {"y","x"});
doTerm(11/3500, {"*",{"y","y"}}, "y", {"y","y"}, {"y","y"}, {"y",{"y","x"}});
doTerm(81/1000, {"y",{"*","y"}}, "y", {"y","y"}, {"y","y"}, {"y",{"y","x"}});
doTerm(-3/2000, {"*",{"y","y"}}, "y", {"y","y"}, {"y","y"}, {{"y","y"},"x"});
doTerm(-107/14000, {"y",{"*","y"}}, "y", {"y","y"}, {"y","y"}, {{"y","y"},"x"});
doTerm(-31/3500, {"*","y"}, "y", {"y","y"}, {"y","y"}, {"y",{"y",{"y","x"}}});
doTerm(-11/1400, {"*","y"}, "y", {"y","y"}, {"y","y"}, {"y",{{"y","y"},"x"}});
doTerm(-271/14000, {"*","y"}, "y", {"y","y"}, {"y","y"}, {{"y","y"},{"y","x"}});
doTerm(97/5250, "*", "y", {"y","y"}, {"y","y"}, {"y",{"y",{"y",{"y","x"}}}});
doTerm(3/7000, "*", "y", {"y","y"}, {"y","y"}, {"y",{"y",{{"y","y"},"x"}}});
doTerm(17/2100, "*", "y", {"y","y"}, {"y","y"}, {"y",{{"y","y"},{"y","x"}}});
doTerm(-13/21000, "*", "y", {"y","y"}, {"y","y"}, {{"y","y"},{"y",{"y","x"}}});
doTerm(17/7000, "*", "y", {"y","y"}, {"y","y"}, {{"y","y"},{{"y","y"},"x"}});
doTerm(-1/280, {"*",{"y",{"y","y"}}}, "y", {"y","y"}, {"y",{"y","y"}}, "x");
doTerm(-3/560, {"y",{"*",{"y","y"}}}, "y", {"y","y"}, {"y",{"y","y"}}, "x");
doTerm(39/1400, {"y",{"y",{"*","y"}}}, "y", {"y","y"}, {"y",{"y","y"}}, "x");
doTerm(-2/525, {"*",{"y","y"}}, "y", {"y","y"}, {"y",{"y","y"}}, {"y","x"});
doTerm(-97/4200, {"y",{"*","y"}}, "y", {"y","y"}, {"y",{"y","y"}}, {"y","x"});
doTerm(-41/700, {"*","y"}, "y", {"y","y"}, {"y",{"y","y"}}, {"y",{"y","x"}});
doTerm(3/1400, {"*","y"}, "y", {"y","y"}, {"y",{"y","y"}}, {{"y","y"},"x"});
doTerm(-7/300, "*", "y", {"y","y"}, {"y",{"y","y"}}, {"y",{"y",{"y","x"}}});
doTerm(1/700, "*", "y", {"y","y"}, {"y",{"y","y"}}, {"y",{{"y","y"},"x"}});
doTerm(-11/1680, "*", "y", {"y","y"}, {"y",{"y","y"}}, {{"y","y"},{"y","x"}});
doTerm(-1/200, {"*",{"y","y"}}, "y", {"y","y"}, {"y",{"y",{"y","y"}}}, "x");
doTerm(-9/200, {"y",{"*","y"}}, "y", {"y","y"}, {"y",{"y",{"y","y"}}}, "x");
doTerm(1/40, "*", "y", {"y","y"}, {"y",{"y",{"y",{"y",{"y","y"}}}}}, "x");

-- drop zero coefficients
nz = select(keys acc, k -> acc#k != 0);
<< "nonzero monomials in reconstructed sum: " << #nz << endl;

-- target e_9(x,y) = ((((((((x y)y)y)y)y)y)y)y)y  (left comb, 9 y''s)
e9 = "x"; for i from 1 to 9 do e9 = {e9, "y"};
e9key = canonStr e9;
-- equality: reconstructed sum has exactly the single monomial e9 with coeff 1
ok = (#nz == 1) and (nz#0 === e9key) and (acc#e9key == 1);
<< "e9 monomial: " << e9key << endl;
<< "reconstructed coeff on e9: " << (if acc#?e9key then acc#e9key else 0) << endl;
<< "CERTIFICATE VERIFIES (sum == e_9 exactly): " << ok << endl;