%------------------------------------------------------------------------------
% File : Gandalf---c-2.6
% Problem : LAT041-1 : TPTP v3.4.2. Released v2.4.0.
% Transfm : add_equality:r
% Format : otter:hypothesis:set(auto),clear(print_given)
% Command : gandalf-wrapper -time %d %s
% Computer : art05.cs.miami.edu
% Model : i686 unknown
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1000MB
% OS : Linux 2.4.22-21mdk-i686-up-4GB
% CPULimit : 600s
% Result : Unsatisfiable 357.9s
% Output : Assurance 357.9s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
%
% Gandalf c-2.6 r1 starting to prove: /home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/LAT/LAT041-1+eq_r.in
% Using automatic strategy selection.
% Time limit in seconds: 600
%
% prove-all-passes started
%
% detected problem class: heq
% detected subclass: medium
% detected subclass: short
%
% strategies selected:
% (binary-posweight-order 57 #f 6 5)
% (binary-unit 28 #f 6 5)
% (binary-double 28 #f 6 5)
% (binary 45 #t 6 5)
% (hyper 11 #t 6 5)
% (hyper 28 #f)
% (binary-unit-uniteq 16 #f)
% (binary-weightorder 22 #f)
% (binary-posweight-order 159 #f)
% (binary-posweight-lex-big-order 57 #f)
% (binary-posweight-lex-small-order 11 #f)
% (binary-order 28 #f)
% (binary-unit 45 #f)
% (binary 65 #t)
%
%
% **** EMPTY CLAUSE DERIVED ****
%
%
% timer checkpoints: c(18,40,0,36,0,0,21207,3,2853,28980,4,4314,39844,5,5701,39844,1,5701,39844,50,5704,39844,40,5704,39862,0,5704,57885,3,7110,62018,4,7812,67247,5,8505,67247,1,8505,67247,50,8507,67247,40,8507,67265,0,8507,169846,3,9908,174454,4,10608,179249,5,11308,179249,1,11308,179249,50,11311,179249,40,11311,179267,0,11311,320300,3,13574,323800,4,14690,333121,5,15813,333122,5,15813,333122,1,15813,333122,50,15817,333122,40,15817,333140,0,15817,343114,4,16643,343154,5,16918,343154,1,16918,343154,50,16918,343154,40,16918,343172,0,16918,380106,4,19042,387934,5,19719,387934,1,19719,387934,50,19721,387934,40,19721,387952,0,19721,411234,3,20524,417737,4,20928,423805,5,21322,423805,1,21322,423805,50,21324,423805,40,21324,423823,0,21324,497216,3,22434,507120,4,22975,523593,5,23525,523593,1,23525,523593,50,23528,523593,40,23528,523611,0,23528,643450,3,31480,718245,4,35463)
%
%
% START OF PROOF
% 523596 [] equal(big_p(term2,X,Y),Y).
% 523597 [] equal(big_p(term3,X,Y),times(X,Y)).
% 523598 [] equal(big_p(term4,X,Y),times(Y,X)).
% 523599 [] equal(big_p(term5,X,Y),plus(X,Y)).
% 523600 [] equal(big_p(term6,X,Y),plus(Y,X)).
% 523603 [] term(term2).
% 523604 [] term(term3).
% 523605 [] term(term4).
% 523606 [] term(term5).
% 523607 [] term(term6).
% 523608 [] equal(big_p(X,big_p(X,Y,Z),U),big_p(X,Y,big_p(X,Z,U))) | -term(X).
% 523609 [] equal(big_p(X,big_p(X,Y,Z),big_p(X,U,V)),big_p(X,big_p(X,Y,U),big_p(X,Z,V))) | -term(X).
% 523610 [] equal(big_p(X,big_p(Y,big_p(X,Z,U),V),big_p(Y,U,V)),big_p(Y,big_p(X,Z,U),V)) | -term(Y) | -term(X).
% 523611 [] -equal(times(a,plus(b,times(d,times(c,e)))),times(a,plus(b,times(plus(b,c),times(d,times(c,e)))))).
% 523614 [binary:523604,523608.2,demod:523597] equal(times(times(X,Y),Z),times(X,times(Y,Z))).
% 523615 [binary:523606,523608.2,demod:523599] equal(plus(plus(X,Y),Z),plus(X,plus(Y,Z))).
% 523617 [binary:523604,523609.2,demod:523614,523597] equal(times(X,times(Y,times(Z,U))),times(X,times(Z,times(Y,U)))).
% 523618 [binary:523606,523609.2,demod:523615,523599] equal(plus(X,plus(Y,plus(Z,U))),plus(X,plus(Z,plus(Y,U)))).
% 523621 [binary:523603,523610.2,demod:523596] equal(big_p(X,Y,Y),Y) | -term(X).
% 523622 [binary:523604,523610.2,demod:523597] equal(big_p(X,times(big_p(X,Y,Z),U),times(Z,U)),times(big_p(X,Y,Z),U)) | -term(X).
% 523623 [binary:523605,523610.2,demod:523598] equal(big_p(X,times(Y,big_p(X,Z,U)),times(Y,U)),times(Y,big_p(X,Z,U))) | -term(X).
% 523624 [binary:523606,523610.2,demod:523599] equal(big_p(X,plus(big_p(X,Y,Z),U),plus(Z,U)),plus(big_p(X,Y,Z),U)) | -term(X).
% 523625 [binary:523607,523610.2,demod:523600] equal(big_p(X,plus(Y,big_p(X,Z,U)),plus(Y,U)),plus(Y,big_p(X,Z,U))) | -term(X).
% 523627 [binary:523604,523621.2,demod:523597] equal(times(X,X),X).
% 523628 [binary:523606,523621.2,demod:523599] equal(plus(X,X),X).
% 523629 [para:523627.1.1,523614.1.1] equal(times(X,Y),times(X,times(Y,times(X,Y)))).
% 523630 [para:523627.1.1,523614.1.1.1] equal(times(X,Y),times(X,times(X,Y))).
% 523632 [para:523615.1.1,523628.1.1] equal(plus(X,plus(Y,plus(X,Y))),plus(X,Y)).
% 523633 [para:523628.1.1,523615.1.1.1] equal(plus(X,Y),plus(X,plus(X,Y))).
% 523639 [para:523614.1.1,523617.1.1.2,demod:523614] equal(times(X,times(Y,times(Z,times(U,V)))),times(X,times(U,times(Y,times(Z,V))))).
% 523641 [para:523617.1.1,523627.1.1,demod:523614] equal(times(X,times(Y,times(Z,times(Y,times(X,Z))))),times(X,times(Y,Z))).
% 523642 [para:523627.1.1,523617.1.1.2.2] equal(times(X,times(Y,Z)),times(X,times(Z,times(Y,Z)))).
% 523643 [para:523617.1.1,523630.1.2] equal(times(X,times(Y,Z)),times(X,times(Y,times(X,Z)))).
% 523644 [para:523617.1.1,523611.1.2.2.2] -equal(times(a,plus(b,times(d,times(c,e)))),times(a,plus(b,times(plus(b,c),times(c,times(d,e)))))).
% 523649 [para:523614.1.1,523642.1.2.2.2,demod:523614] equal(times(X,times(Y,times(Z,U))),times(X,times(U,times(Y,times(Z,U))))).
% 523651 [para:523643.1.2,523614.1.1,demod:523614] equal(times(X,times(Y,times(Z,U))),times(X,times(Y,times(Z,times(X,times(Y,U)))))).
% 523652 [para:523614.1.1,523643.1.2.2,demod:523614] equal(times(X,times(Y,times(Z,U))),times(X,times(Y,times(Z,times(X,U))))).
% 523653 [para:523618.1.1,523628.1.1,demod:523615] equal(plus(X,plus(Y,plus(Z,plus(Y,plus(X,Z))))),plus(X,plus(Y,Z))).
% 523654 [para:523628.1.1,523618.1.1.2.2] equal(plus(X,plus(Y,Z)),plus(X,plus(Z,plus(Y,Z)))).
% 523656 [para:523615.1.1,523618.1.1.2,demod:523615] equal(plus(X,plus(Y,plus(Z,plus(U,V)))),plus(X,plus(U,plus(Y,plus(Z,V))))).
% 523658 [para:523618.1.1,523633.1.2] equal(plus(X,plus(Y,Z)),plus(X,plus(Y,plus(X,Z)))).
% 523659 [para:523618.1.1,523632.1.1.2.2,demod:523615] equal(plus(X,plus(Y,plus(Z,plus(U,plus(X,plus(Z,plus(Y,U))))))),plus(X,plus(Y,plus(Z,U)))).
% 523662 [para:523615.1.1,523654.1.2.2.2,demod:523615] equal(plus(X,plus(Y,plus(Z,U))),plus(X,plus(U,plus(Y,plus(Z,U))))).
% 523665 [para:523615.1.1,523658.1.2.2,demod:523615] equal(plus(X,plus(Y,plus(Z,U))),plus(X,plus(Y,plus(Z,plus(X,U))))).
% 523667 [binary:523606,523622.2,demod:523599] equal(plus(times(plus(X,Y),Z),times(Y,Z)),times(plus(X,Y),Z)).
% 523668 [binary:523607,523622.2,demod:523600] equal(plus(times(X,Y),times(plus(X,Z),Y)),times(plus(X,Z),Y)).
% 523670 [para:523627.1.1,523667.1.1.1,demod:523627,523615] equal(plus(X,plus(Y,times(Y,plus(X,Y)))),plus(X,Y)).
% 523671 [para:523627.1.1,523667.1.1.2] equal(plus(times(plus(X,Y),Y),Y),times(plus(X,Y),Y)).
% 523673 [para:523630.1.2,523667.1.1.2] equal(plus(times(plus(X,Y),times(Y,Z)),times(Y,Z)),times(plus(X,Y),times(Y,Z))).
% 523674 [para:523667.1.1,523615.1.1.1] equal(plus(times(plus(X,Y),Z),U),plus(times(plus(X,Y),Z),plus(times(Y,Z),U))).
% 523675 [para:523615.1.1,523667.1.1.1.1,demod:523615] equal(plus(times(plus(X,plus(Y,Z)),U),times(Z,U)),times(plus(X,plus(Y,Z)),U)).
% 523676 [para:523632.1.1,523667.1.1.1.1,demod:523633,523654] equal(plus(times(plus(X,Y),Z),times(plus(Y,plus(X,Y)),Z)),times(plus(X,Y),Z)).
% 523679 [para:523643.1.2,523667.1.1.2] equal(plus(times(plus(X,Y),times(Z,times(Y,U))),times(Y,times(Z,U))),times(plus(X,Y),times(Z,times(Y,U)))).
% 523680 [para:523667.1.1,523618.1.1.2.2] equal(plus(X,plus(Y,times(plus(Z,U),V))),plus(X,plus(times(plus(Z,U),V),plus(Y,times(U,V))))).
% 523682 [para:523667.1.1,523654.1.2.2.2,demod:523667] equal(plus(X,times(plus(Y,Z),U)),plus(X,plus(times(Z,U),times(plus(Y,Z),U)))).
% 523687 [binary:523606,523623.2,demod:523599] equal(plus(times(X,plus(Y,Z)),times(X,Z)),times(X,plus(Y,Z))).
% 523688 [binary:523607,523623.2,demod:523600] equal(plus(times(X,Y),times(X,plus(Y,Z))),times(X,plus(Y,Z))).
% 523693 [para:523670.1.1,523632.1.1.2.2,demod:523670,523658,523662,523615] equal(plus(X,plus(times(Y,plus(X,Y)),Y)),plus(X,Y)).
% 523698 [para:523670.1.1,523654.1.2.2.2,demod:523662,523615,523670] equal(plus(X,plus(Y,Z)),plus(X,plus(times(Z,plus(Y,Z)),plus(Y,Z)))).
% 523700 [para:523670.1.1,523658.1.2.2] equal(plus(X,plus(Y,times(X,plus(Y,X)))),plus(X,plus(Y,X))).
% 523701 [para:523670.1.1,523658.1.2.2.2,demod:523658] equal(plus(X,plus(Y,plus(Z,times(Z,plus(X,Z))))),plus(X,plus(Y,Z))).
% 523703 [para:523670.1.1,523667.1.1.1.1,demod:523670] equal(plus(times(plus(X,Y),Z),times(plus(Y,times(Y,plus(X,Y))),Z)),times(plus(X,Y),Z)).
% 523704 [para:523670.1.1,523670.1.1.2.2.2,demod:523670,523668,523615] equal(plus(X,plus(Y,times(plus(Y,times(Y,plus(X,Y))),plus(X,Y)))),plus(X,Y)).
% 523706 [binary:523604,523624.2,demod:523597] equal(times(plus(times(X,Y),Z),plus(Y,Z)),plus(times(X,Y),Z)).
% 523707 [binary:523605,523624.2,demod:523598] equal(times(plus(X,Y),plus(times(X,Z),Y)),plus(times(X,Z),Y)).
% 523711 [para:523617.1.1,523671.1.1.1] equal(plus(times(plus(X,times(Y,times(Z,U))),times(Z,times(Y,U))),times(Y,times(Z,U))),times(plus(X,times(Y,times(Z,U))),times(Y,times(Z,U)))).
% 523714 [para:523671.1.1,523618.1.1.2] equal(plus(X,times(plus(Y,plus(Z,U)),plus(Z,U))),plus(X,plus(Z,plus(times(plus(Y,plus(Z,U)),plus(Z,U)),U)))).
% 523717 [?] ?
% 523718 [para:523671.1.1,523654.1.2.2.2,demod:523671] equal(plus(X,times(plus(Y,Z),Z)),plus(X,plus(Z,times(plus(Y,Z),Z)))).
% 523725 [para:523632.1.1,523693.1.1.2.1.2,demod:523633,523671,523654] equal(plus(X,times(plus(Y,plus(X,Y)),plus(X,Y))),plus(X,Y)).
% 523741 [para:523627.1.1,523668.1.1.1] equal(plus(X,times(plus(X,Y),X)),times(plus(X,Y),X)).
% 523742 [para:523627.1.1,523668.1.1.2,demod:523627] equal(plus(times(X,plus(X,Y)),plus(X,Y)),plus(X,Y)).
% 523743 [para:523630.1.2,523668.1.1.1] equal(plus(times(X,Y),times(plus(X,Z),times(X,Y))),times(plus(X,Z),times(X,Y))).
% 523744 [para:523630.1.2,523668.1.1.2,demod:523630] equal(plus(times(X,times(plus(X,Y),Z)),times(plus(X,Y),Z)),times(plus(X,Y),Z)).
% 523745 [para:523668.1.1,523615.1.1.1] equal(plus(times(plus(X,Y),Z),U),plus(times(X,Z),plus(times(plus(X,Y),Z),U))).
% 523749 [para:523643.1.2,523668.1.1.2,demod:523643] equal(plus(times(X,times(Y,times(plus(X,Z),U))),times(plus(X,Z),times(Y,U))),times(plus(X,Z),times(Y,U))).
% 523753 [para:523741.1.1,523615.1.1.1] equal(plus(times(plus(X,Y),X),Z),plus(X,plus(times(plus(X,Y),X),Z))).
% 523765 [para:523742.1.1,523658.1.2.2,demod:523633] equal(plus(X,plus(times(X,plus(X,Y)),Y)),plus(X,Y)).
% 523767 [binary:523604,523625.2,demod:523597] equal(times(plus(X,times(Y,Z)),plus(X,Z)),plus(X,times(Y,Z))).
% 523768 [binary:523605,523625.2,demod:523598] equal(times(plus(X,Y),plus(X,times(Y,Z))),plus(X,times(Y,Z))).
% 523771 [para:523765.1.1,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(X,plus(times(X,plus(X,Y)),plus(Y,Z)))).
% 523777 [para:523765.1.1,523670.1.1.2.2.2,demod:523765,523771,523615] equal(plus(X,plus(Y,times(plus(times(X,plus(X,Y)),Y),plus(X,Y)))),plus(X,Y)).
% 523779 [para:523614.1.1,523687.1.1.1,demod:523614] equal(plus(times(X,times(Y,plus(Z,U))),times(X,times(Y,U))),times(X,times(Y,plus(Z,U)))).
% 523780 [para:523627.1.1,523687.1.1.1,demod:523627,523718,523615] equal(plus(X,times(plus(X,Y),Y)),plus(X,Y)).
% 523781 [para:523627.1.1,523687.1.1.2] equal(plus(times(X,plus(Y,X)),X),times(X,plus(Y,X))).
% 523792 [para:523687.1.1,523654.1.2.2.2,demod:523687] equal(plus(X,times(Y,plus(Z,U))),plus(X,plus(times(Y,U),times(Y,plus(Z,U))))).
% 523794 [para:523687.1.1,523658.1.2.2.2] equal(plus(times(X,plus(Y,Z)),plus(U,times(X,Z))),plus(times(X,plus(Y,Z)),plus(U,times(X,plus(Y,Z))))).
% 523804 [para:523780.1.1,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(X,plus(times(plus(X,Y),Y),Z))).
% 523805 [para:523632.1.1,523780.1.1.2.1,demod:523633,523654] equal(plus(X,times(plus(X,Y),plus(Y,plus(X,Y)))),plus(X,Y)).
% 523811 [para:523780.1.1,523658.1.2.2.2,demod:523658] equal(plus(X,plus(Y,times(plus(X,Z),Z))),plus(X,plus(Y,Z))).
% 523820 [para:523781.1.1,523615.1.1.1] equal(plus(times(X,plus(Y,X)),Z),plus(times(X,plus(Y,X)),plus(X,Z))).
% 523821 [para:523615.1.1,523781.1.1.1.2,demod:523615] equal(plus(times(X,plus(Y,plus(Z,X))),X),times(X,plus(Y,plus(Z,X)))).
% 523827 [para:523781.1.1,523654.1.2.2.2,demod:523781] equal(plus(X,times(Y,plus(Z,Y))),plus(X,plus(Y,times(Y,plus(Z,Y))))).
% 523834 [para:523781.1.1,523693.1.1.2] equal(plus(X,times(Y,plus(X,Y))),plus(X,Y)).
% 523837 [para:523614.1.1,523834.1.1.2] equal(plus(X,times(Y,times(Z,plus(X,times(Y,Z))))),plus(X,times(Y,Z))).
% 523838 [para:523834.1.1,523615.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(X,plus(Y,times(Z,plus(X,plus(Y,Z)))))).
% 523843 [para:523834.1.1,523658.1.2.2.2,demod:523658] equal(plus(X,plus(Y,times(Z,plus(X,Z)))),plus(X,plus(Y,Z))).
% 523846 [para:523765.1.1,523834.1.1.2.2,demod:523765] equal(plus(X,times(plus(times(X,plus(X,Y)),Y),plus(X,Y))),plus(X,Y)).
% 523851 [para:523627.1.1,523688.1.1.1] equal(plus(X,times(X,plus(X,Y))),times(X,plus(X,Y))).
% 523852 [para:523627.1.1,523688.1.1.2,demod:523627] equal(plus(times(plus(X,Y),X),plus(X,Y)),plus(X,Y)).
% 523867 [para:523851.1.1,523615.1.1.1] equal(plus(times(X,plus(X,Y)),Z),plus(X,plus(times(X,plus(X,Y)),Z))).
% 523869 [para:523851.1.1,523668.1.1.2.1,demod:523851,523614] equal(plus(times(X,Y),times(X,times(plus(X,Z),Y))),times(X,times(plus(X,Z),Y))).
% 523870 [para:523851.1.1,523741.1.1.2.1,demod:523851,523614] equal(plus(X,times(X,times(plus(X,Y),X))),times(X,times(plus(X,Y),X))).
% 523871 [para:523765.1.1,523851.1.1.2.2,demod:523867,523851] equal(times(X,plus(X,Y)),times(X,plus(times(X,plus(X,Y)),Y))).
% 523882 [para:523852.1.1,523658.1.2.2,demod:523633,523753] equal(plus(times(plus(X,Y),X),Y),plus(X,Y)).
% 523888 [para:523882.1.1,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(times(plus(X,Y),X),plus(Y,Z))).
% 523889 [para:523615.1.1,523882.1.1.1.1,demod:523615] equal(plus(times(plus(X,plus(Y,Z)),plus(X,Y)),Z),plus(X,plus(Y,Z))).
% 523900 [para:523765.1.1,523700.1.1.2.2.2,demod:523633,523867,523742,523654,523615,523846] equal(plus(X,Y),plus(times(X,plus(X,Y)),Y)).
% 523906 [para:523614.1.1,523900.1.2.1] equal(plus(times(X,Y),Z),plus(times(X,times(Y,plus(times(X,Y),Z))),Z)).
% 523907 [para:523900.1.2,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(times(X,plus(X,Y)),plus(Y,Z))).
% 523914 [para:523900.1.2,523693.1.1.2.1.2,demod:523900,523781] equal(plus(times(X,plus(X,Y)),times(Y,plus(X,Y))),plus(X,Y)).
% 523919 [para:523628.1.1,523706.1.1.1,demod:523628,523614] equal(times(X,times(Y,plus(Y,times(X,Y)))),times(X,Y)).
% 523920 [para:523628.1.1,523706.1.1.2] equal(times(plus(times(X,Y),Y),Y),plus(times(X,Y),Y)).
% 523927 [para:523706.1.1,523642.1.2.2.2,demod:523706] equal(times(X,plus(times(Y,Z),U)),times(X,times(plus(Z,U),plus(times(Y,Z),U)))).
% 523934 [para:523706.1.1,523667.1.1.1,demod:523706,523827,523615] equal(plus(times(X,Y),times(Z,plus(Y,Z))),plus(times(X,Y),Z)).
% 523936 [para:523667.1.1,523706.1.1.1,demod:523667,523614] equal(times(plus(X,Y),times(Z,plus(Z,times(Y,Z)))),times(plus(X,Y),Z)).
% 523939 [para:523671.1.1,523706.1.1.2] equal(times(plus(times(X,times(plus(Y,Z),Z)),Z),times(plus(Y,Z),Z)),plus(times(X,times(plus(Y,Z),Z)),Z)).
% 523964 [para:523919.1.1,523629.1.2.2.2,demod:523643,523649,523614,523919] equal(times(X,Y),times(X,times(plus(Y,times(X,Y)),Y))).
% 523980 [para:523920.1.1,523614.1.1.1] equal(times(plus(times(X,Y),Y),Z),times(plus(times(X,Y),Y),times(Y,Z))).
% 523988 [para:523920.1.1,523642.1.2.2.2,demod:523920] equal(times(X,plus(times(Y,Z),Z)),times(X,times(Z,plus(times(Y,Z),Z)))).
% 524003 [para:523629.1.2,523964.1.2.2.1.2,demod:523920,523630,523642] equal(times(X,Y),times(X,plus(times(Y,times(X,Y)),times(X,Y)))).
% 524046 [para:523628.1.1,523707.1.1.1] equal(times(X,plus(times(X,Y),X)),plus(times(X,Y),X)).
% 524047 [para:523628.1.1,523707.1.1.2,demod:523628] equal(times(plus(X,times(X,Y)),times(X,Y)),times(X,Y)).
% 524049 [para:523633.1.2,523707.1.1.1] equal(times(plus(X,Y),plus(times(X,Z),plus(X,Y))),plus(times(X,Z),plus(X,Y))).
% 524066 [para:523741.1.1,523707.1.1.1,demod:523614] equal(times(plus(X,Y),times(X,plus(times(X,Z),times(plus(X,Y),X)))),plus(times(X,Z),times(plus(X,Y),X))).
% 524068 [para:523707.1.1,523687.1.1.1,demod:523707,523718,523615] equal(plus(times(X,Y),times(plus(X,Z),Z)),plus(times(X,Y),Z)).
% 524071 [para:523687.1.1,523707.1.1.2,demod:523687] equal(times(plus(X,times(X,Y)),times(X,plus(Z,Y))),times(X,plus(Z,Y))).
% 524081 [para:524046.1.1,523614.1.1.1] equal(times(plus(times(X,Y),X),Z),times(X,times(plus(times(X,Y),X),Z))).
% 524094 [para:524047.1.1,523617.1.1.2] equal(times(X,times(Y,Z)),times(X,times(Y,times(plus(Y,times(Y,Z)),Z)))).
% 524097 [para:524047.1.1,523642.1.2] equal(times(plus(X,times(X,times(Y,X))),times(Y,X)),times(X,times(Y,X))).
% 524098 [para:524047.1.1,523643.1.2.2,demod:523630] equal(times(X,times(plus(X,times(X,Y)),Y)),times(X,Y)).
% 524108 [para:524098.1.1,523643.1.2.2.2,demod:523643] equal(times(X,times(Y,times(plus(X,times(X,Z)),Z))),times(X,times(Y,Z))).
% 524124 [para:523725.1.1,523654.1.2.2.2,demod:523671,523725] equal(plus(X,plus(Y,Z)),plus(X,times(plus(Z,plus(Y,Z)),plus(Y,Z)))).
% 524146 [para:523642.1.2,523639.1.1.2.2] equal(times(X,times(Y,times(Z,times(U,V)))),times(X,times(V,times(Y,times(Z,times(U,V)))))).
% 524232 [para:523628.1.1,523767.1.1.1,demod:523628,523988,523614] equal(times(X,plus(times(X,Y),Y)),times(X,Y)).
% 524233 [para:523628.1.1,523767.1.1.2] equal(times(plus(X,times(Y,X)),X),plus(X,times(Y,X))).
% 524240 [para:523767.1.1,523642.1.2.2.2,demod:523767] equal(times(X,plus(Y,times(Z,U))),times(X,times(plus(Y,U),plus(Y,times(Z,U))))).
% 524242 [para:523767.1.1,523643.1.2.2.2] equal(times(plus(X,times(Y,Z)),times(U,plus(X,Z))),times(plus(X,times(Y,Z)),times(U,plus(X,times(Y,Z))))).
% 524243 [para:523643.1.2,523767.1.1.1.2,demod:523643] equal(times(plus(X,times(Y,times(Z,U))),plus(X,times(Z,times(Y,U)))),plus(X,times(Y,times(Z,U)))).
% 524255 [para:523767.1.1,523668.1.1.2,demod:523767] equal(plus(times(X,plus(X,Y)),plus(X,times(Z,Y))),plus(X,times(Z,Y))).
% 524256 [para:523668.1.1,523767.1.1.1,demod:523668,523988,523614] equal(times(plus(X,Y),plus(times(X,Z),Z)),times(plus(X,Y),Z)).
% 524288 [para:524232.1.1,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(plus(times(X,Y),Y),Z))).
% 524289 [para:523629.1.2,524232.1.1.2.1,demod:523630,523642] equal(times(X,plus(times(X,Y),times(Y,times(X,Y)))),times(X,Y)).
% 524301 [para:524232.1.1,523919.1.1.2.2.2,demod:524232,524288,523615] equal(times(X,times(Y,plus(times(X,Y),plus(Y,times(X,Y))))),times(X,Y)).
% 524310 [para:524233.1.1,523614.1.1.1] equal(times(plus(X,times(Y,X)),Z),times(plus(X,times(Y,X)),times(X,Z))).
% 524311 [para:523614.1.1,524233.1.1.1.2,demod:523614] equal(times(plus(X,times(Y,times(Z,X))),X),plus(X,times(Y,times(Z,X)))).
% 524318 [para:524233.1.1,523642.1.2.2.2,demod:524233] equal(times(X,plus(Y,times(Z,Y))),times(X,times(Y,plus(Y,times(Z,Y))))).
% 524330 [para:524233.1.1,523964.1.2.2] equal(times(X,Y),times(X,plus(Y,times(X,Y)))).
% 524345 [para:524330.1.2,523614.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(Y,plus(Z,times(X,times(Y,Z)))))).
% 524346 [para:524330.1.2,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(plus(Y,times(X,Y)),Z))).
% 524351 [para:524330.1.2,523643.1.2.2.2,demod:523643] equal(times(X,times(Y,plus(Z,times(X,Z)))),times(X,times(Y,Z))).
% 524363 [para:523768.1.1,523614.1.1.1] equal(times(plus(X,times(Y,Z)),U),times(plus(X,Y),times(plus(X,times(Y,Z)),U))).
% 524365 [para:523628.1.1,523768.1.1.1] equal(times(X,plus(X,times(X,Y))),plus(X,times(X,Y))).
% 524366 [para:523628.1.1,523768.1.1.2,demod:523628] equal(times(plus(times(X,Y),X),times(X,Y)),times(X,Y)).
% 524368 [para:523633.1.2,523768.1.1.1] equal(times(plus(X,Y),plus(X,times(plus(X,Y),Z))),plus(X,times(plus(X,Y),Z))).
% 524392 [para:523768.1.1,523688.1.1.2,demod:523768] equal(plus(times(plus(X,Y),X),plus(X,times(Y,Z))),plus(X,times(Y,Z))).
% 524394 [para:523688.1.1,523768.1.1.2,demod:523688] equal(times(plus(times(X,Y),X),times(X,plus(Y,Z))),times(X,plus(Y,Z))).
% 524419 [para:524365.1.1,523614.1.1.1] equal(times(plus(X,times(X,Y)),Z),times(X,times(plus(X,times(X,Y)),Z))).
% 524433 [para:524047.1.1,523641.1.1.2.2.2,demod:524419,523630,524047,523642] equal(times(X,Y),times(plus(X,times(X,Y)),Y)).
% 524434 [para:524098.1.1,523641.1.1.2.2,demod:524311,523630,523642,524047] equal(times(X,Y),times(X,plus(Y,times(Y,times(X,Y))))).
% 524438 [para:524433.1.2,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(plus(X,times(X,Y)),times(Y,Z))).
% 524439 [para:523614.1.1,524433.1.2.1.2,demod:523614] equal(times(X,times(Y,Z)),times(plus(times(X,Y),times(X,times(Y,Z))),Z)).
% 524440 [para:523615.1.1,524433.1.2.1] equal(times(plus(X,Y),Z),times(plus(X,plus(Y,times(plus(X,Y),Z))),Z)).
% 524444 [para:524433.1.2,523643.1.2.2,demod:523643] equal(times(X,times(plus(Y,times(Y,times(X,Z))),Z)),times(X,times(Y,Z))).
% 524467 [para:524366.1.1,523643.1.2.2,demod:523630,524081] equal(times(plus(times(X,Y),X),Y),times(X,Y)).
% 524484 [para:524467.1.1,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(plus(times(X,Y),X),times(Y,Z))).
% 524498 [para:524467.1.1,523964.1.2.2.1.2,demod:524233,524467] equal(times(X,Y),times(plus(times(X,Y),X),plus(Y,times(X,Y)))).
% 524516 [para:524434.1.2,523643.1.2.2.2,demod:523643] equal(times(X,times(Y,plus(Z,times(Z,times(X,Z))))),times(X,times(Y,Z))).
% 524543 [para:523804.1.2,523654.1.2,demod:523811] equal(plus(X,plus(Y,Z)),plus(X,plus(Z,plus(Y,times(plus(X,Z),Z))))).
% 524611 [para:523668.1.1,523811.1.1.2,demod:523780] equal(plus(X,Y),plus(X,plus(times(X,Y),Y))).
% 524665 [para:524611.1.2,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(X,plus(times(X,Y),plus(Y,Z)))).
% 524675 [para:524611.1.2,523658.1.2.2.2,demod:523658] equal(plus(X,plus(Y,plus(times(X,Z),Z))),plus(X,plus(Y,Z))).
% 524762 [para:523688.1.1,523843.1.1.2,demod:523834] equal(plus(X,Y),plus(X,plus(times(Y,X),Y))).
% 524786 [para:524762.1.2,523615.1.1.1,demod:523615] equal(plus(X,plus(Y,Z)),plus(X,plus(times(Y,X),plus(Y,Z)))).
% 524792 [para:524762.1.2,523618.1.1.2] equal(plus(X,plus(Y,Z)),plus(X,plus(times(Z,Y),plus(Y,Z)))).
% 524798 [para:524762.1.2,523765.1.1.2.1.2,demod:524762,523867] equal(plus(times(X,plus(X,Y)),plus(times(Y,X),Y)),plus(X,Y)).
% 524803 [para:523919.1.1,524762.1.2.2.1,demod:524762,523907] equal(plus(times(X,plus(X,times(Y,X))),Y),plus(X,Y)).
% 524823 [para:524803.1.1,523633.1.2.2,demod:524803] equal(plus(X,Y),plus(times(X,plus(X,times(Y,X))),plus(X,Y))).
% 524837 [para:523741.1.1,524803.1.1.1.2,demod:523633] equal(plus(times(X,times(plus(X,Y),X)),plus(X,Y)),plus(X,Y)).
% 524842 [para:524803.1.1,523900.1.2.1.2,demod:523614,524803] equal(plus(X,Y),plus(times(X,times(plus(X,times(Y,X)),plus(X,Y))),Y)).
% 524941 [para:523888.1.2,523654.1.2,demod:523654] equal(plus(times(plus(X,Y),X),plus(Z,Y)),plus(X,plus(Z,Y))).
% 524943 [para:523888.1.2,523658.1.2.2,demod:523658] equal(plus(X,plus(times(plus(Y,X),Y),Z)),plus(X,plus(Y,Z))).
% 525058 [para:523654.1.2,523907.1.2.1.2,demod:523658,523615] equal(plus(X,plus(Y,plus(Z,U))),plus(times(X,plus(X,plus(Z,Y))),plus(Y,plus(Z,U)))).
% 525059 [para:523907.1.2,523658.1.2.2,demod:523658] equal(plus(X,plus(times(Y,plus(Y,X)),Z)),plus(X,plus(Y,Z))).
% 525181 [para:523614.1.1,523934.1.1.1,demod:523614] equal(plus(times(X,times(Y,Z)),times(U,plus(Z,U))),plus(times(X,times(Y,Z)),U)).
% 525202 [para:523934.1.1,523688.1.1] equal(plus(times(X,Y),X),times(X,plus(Y,X))).
% 525276 [para:523614.1.1,525202.1.1.1,demod:523614] equal(plus(times(X,times(Y,Z)),times(X,Y)),times(X,times(Y,plus(Z,times(X,Y))))).
% 525277 [para:525202.1.1,523615.1.1.1] equal(plus(times(X,plus(Y,X)),Z),plus(times(X,Y),plus(X,Z))).
% 525295 [para:525202.1.1,523767.1.1.2] equal(times(plus(times(X,Y),times(Z,X)),times(X,plus(Y,X))),plus(times(X,Y),times(Z,X))).
% 525296 [para:524232.1.1,525202.1.1.1,demod:523615,525202] equal(times(X,plus(Y,X)),times(X,plus(times(X,Y),plus(Y,X)))).
% 525300 [para:525202.1.1,524366.1.1.1,demod:523643,523614] equal(times(X,times(plus(Y,X),Y)),times(X,Y)).
% 525312 [para:525300.1.1,523614.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(Y,times(plus(Z,times(X,Y)),Z)))).
% 525313 [para:525300.1.1,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(plus(Y,X),times(Y,Z)))).
% 525314 [para:523615.1.1,525300.1.1.2.1] equal(times(X,times(plus(Y,plus(Z,X)),plus(Y,Z))),times(X,plus(Y,Z))).
% 525317 [para:525300.1.1,523617.1.1.2] equal(times(X,times(Y,Z)),times(X,times(plus(Z,Y),times(Y,Z)))).
% 525321 [para:525300.1.1,523643.1.2.2.2,demod:523643] equal(times(X,times(Y,times(plus(Z,X),Z))),times(X,times(Y,Z))).
% 525327 [para:523670.1.1,525300.1.1.2.1,demod:525300,524438] equal(times(X,Y),times(plus(X,times(X,plus(Y,X))),Y)).
% 525357 [para:525327.1.2,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(plus(X,times(X,plus(Y,X))),times(Y,Z))).
% 525447 [para:524068.1.1,523658.1.2.2.2,demod:523658] equal(plus(times(X,Y),plus(Z,times(plus(X,U),U))),plus(times(X,Y),plus(Z,U))).
% 525457 [para:524068.1.1,523668.1.1] equal(plus(times(X,Y),Y),times(plus(X,Y),Y)).
% 525465 [para:524068.1.1,523920.1.1.1,demod:523744,523939] equal(plus(times(X,times(plus(X,Y),Y)),Y),times(plus(X,Y),Y)).
% 525500 [para:523614.1.1,525457.1.1.1] equal(plus(times(X,times(Y,Z)),Z),times(plus(times(X,Y),Z),Z)).
% 525501 [para:525457.1.1,523615.1.1.1] equal(plus(times(plus(X,Y),Y),Z),plus(times(X,Y),plus(Y,Z))).
% 525503 [para:523617.1.1,525457.1.1.1] equal(plus(times(X,times(Y,times(Z,U))),times(Z,times(Y,U))),times(plus(X,times(Z,times(Y,U))),times(Z,times(Y,U)))).
% 525507 [para:525457.1.1,523618.1.1.2] equal(plus(X,times(plus(Y,plus(Z,U)),plus(Z,U))),plus(X,plus(Z,plus(times(Y,plus(Z,U)),U)))).
% 525511 [para:525457.1.1,523658.1.2.2] equal(plus(X,plus(times(Y,plus(X,Z)),Z)),plus(X,times(plus(Y,plus(X,Z)),plus(X,Z)))).
% 525523 [para:525457.1.1,523767.1.1.2] equal(times(plus(times(X,Y),times(Z,Y)),times(plus(X,Y),Y)),plus(times(X,Y),times(Z,Y))).
% 525524 [para:525457.1.1,524232.1.1.2] equal(times(X,times(plus(X,Y),Y)),times(X,Y)).
% 525527 [para:524467.1.1,525457.1.1.1,demod:525277,525202,525457] equal(times(plus(X,Y),Y),times(plus(times(X,Y),plus(X,Y)),Y)).
% 525542 [para:525524.1.1,523614.1.1.1,demod:523614] equal(times(X,times(Y,Z)),times(X,times(plus(X,Y),times(Y,Z)))).
% 525543 [para:523615.1.1,525524.1.1.2.1] equal(times(plus(X,Y),times(plus(X,plus(Y,Z)),Z)),times(plus(X,Y),Z)).
% 525546 [para:525524.1.1,523617.1.1.2] equal(times(X,times(Y,Z)),times(X,times(plus(Y,Z),times(Y,Z)))).
% 525582 [para:525524.1.1,524003.1.2.2.1.2,demod:523643,523615,525457,523642,523614,525524] equal(times(X,Y),times(X,times(plus(X,plus(Y,times(X,Y))),Y))).
% 525586 [para:524256.1.1,523614.1.1.1,demod:525457,523614] equal(times(plus(X,Y),times(Z,U)),times(plus(X,Y),times(plus(X,Z),times(Z,U)))).
% 525588 [para:524256.1.1,523630.1.2.2,demod:523630,525457] equal(times(plus(X,Y),times(plus(X,Z),Z)),times(plus(X,Y),Z)).
% 525593 [para:524256.1.1,523643.1.2.2.2,demod:523643,525457] equal(times(plus(X,Y),times(Z,times(plus(X,U),U))),times(plus(X,Y),times(Z,U))).
% 525611 [para:523920.1.1,524256.1.1.2.1,demod:523628,525501,525457] equal(times(plus(times(X,Y),plus(Y,Z)),times(plus(X,Y),Y)),times(plus(times(X,Y),plus(Y,Z)),Y)).
% 525640 [para:524438.1.2,523617.1.1] equal(times(X,times(Y,times(Z,U))),times(plus(X,times(X,Y)),times(Z,times(Y,U)))).
% 525643 [para:524438.1.2,523642.1.2,demod:523642] equal(times(plus(X,times(X,Y)),times(Z,Y)),times(X,times(Z,Y))).
% 525645 [para:524438.1.2,523643.1.2.2,demod:523643] equal(times(X,times(plus(Y,times(Y,X)),Z)),times(X,times(Y,Z))).
% 525665 [para:524232.1.1,524438.1.2.1.2,demod:525640,525542,523614,525457] equal(times(X,times(Y,Z)),times(X,times(Y,times(plus(X,Y),Z)))).
% 525786 [para:525300.1.1,524289.1.1.2.1,demod:523642,523614,525300] equal(times(X,plus(times(X,Y),times(plus(Y,X),times(X,Y)))),times(X,Y)).
% 525848 [para:524346.1.2,523642.1.2.2,demod:523642] equal(times(X,times(plus(Y,times(Z,Y)),Z)),times(X,times(Y,Z))).
% 525929 [para:525524.1.1,523652.1.2.2,demod:523643] equal(times(X,times(Y,times(plus(Y,times(X,Z)),Z))),times(X,times(Y,Z))).
% 526025 [para:524484.1.2,523617.1.1,demod:523614,525202] equal(times(X,times(Y,times(Z,U))),times(X,times(plus(Y,X),times(Z,times(Y,U))))).
% 526071 [para:524256.1.1,524484.1.2.1.1,demod:526025,525202,525586,523614,525457] equal(times(plus(X,Y),times(Z,U)),times(plus(X,Y),times(Z,times(plus(X,Z),U)))).
% 526090 [para:523765.1.1,523653.1.1.2.2,demod:523821,523633,523654,525058] equal(plus(X,Y),plus(X,times(Y,plus(Y,plus(X,Y))))).
% 526428 [para:525202.1.1,524665.1.2.2.2,demod:525181,525202] equal(plus(X,times(Y,plus(Z,Y))),plus(X,plus(times(X,times(Y,Z)),Y))).
% 526620 [para:523671.1.1,523656.1.1.2.2,demod:525457,523628,523615,525501] equal(plus(X,plus(Y,times(plus(Z,plus(U,V)),plus(U,V)))),plus(X,plus(U,plus(Y,times(plus(Z,plus(U,V)),plus(U,V)))))).
% 526786 [para:524068.1.1,523656.1.1.2.2.2] equal(plus(X,plus(Y,plus(Z,plus(times(U,V),W)))),plus(X,plus(times(U,V),plus(Y,plus(Z,times(plus(U,W),W)))))).
% 526953 [para:523851.1.1,524786.1.2.2.2,demod:523851] equal(plus(X,times(Y,plus(Y,Z))),plus(X,plus(times(Y,X),times(Y,plus(Y,Z))))).
% 526980 [para:525457.1.1,524786.1.2.2.2,demod:524068,523614,525457] equal(plus(X,times(plus(Y,Z),Z)),plus(X,plus(times(Y,times(Z,X)),Z))).
% 527022 [para:524792.1.2,524675.1.1,demod:523614,525202,525500,523780,525457] equal(plus(X,Y),plus(X,times(Y,times(plus(X,Y),Y)))).
% 527050 [para:523614.1.1,527022.1.2.2,demod:523643,523649] equal(plus(X,times(Y,Z)),plus(X,times(Y,times(plus(X,times(Y,Z)),Z)))).
% 527226 [para:523671.1.1,523659.1.1.2.2.2.2.2,demod:525507,525511,523628,526620,523665,525457,526786,523658,523633,523615,525501] equal(plus(X,plus(Y,times(plus(Z,plus(U,Y)),plus(U,Y)))),plus(X,times(plus(Z,plus(U,Y)),plus(U,Y)))).
% 527502 [para:523615.1.1,524941.1.1.2,demod:523615] equal(plus(times(plus(X,Y),X),plus(Z,plus(U,Y))),plus(X,plus(Z,plus(U,Y)))).
% 527596 [para:524837.1.1,524941.1.1.1.1,demod:523658,527502,523630,523642] equal(plus(X,plus(Y,Z)),plus(times(X,times(plus(X,Z),X)),plus(Y,plus(X,Z)))).
% 527616 [para:523667.1.1,524943.1.1.2] equal(plus(X,times(plus(Y,X),Y)),plus(X,plus(Y,times(X,Y)))).
% 527622 [para:523741.1.1,524943.1.1.2.1.1,demod:523633,523627,523614] equal(plus(times(plus(X,Y),X),Z),plus(times(plus(X,Y),X),plus(X,Z))).
% 527672 [para:525457.1.1,524943.1.1.2,demod:523628,523615] equal(plus(X,times(plus(Y,plus(X,Y)),Y)),plus(X,Y)).
% 527717 [para:527672.1.1,523671.1.1.1.1,demod:527672,523741,525501,525300] equal(plus(times(X,Y),times(plus(Y,plus(X,Y)),Y)),times(plus(X,Y),Y)).
% 527753 [para:527672.1.1,525524.1.1.2.1,demod:525524,525300] equal(times(X,Y),times(X,times(plus(Y,plus(X,Y)),Y))).
% 527819 [para:525457.1.1,527753.1.2.2.1.2,demod:524318,524233,523627,523614] equal(times(X,Y),times(X,plus(Y,times(plus(X,Y),Y)))).
% 527844 [para:523615.1.1,527819.1.2.2,demod:525511,527226] equal(times(X,plus(Y,Z)),times(X,plus(Y,plus(times(X,plus(Y,Z)),Z)))).
% 527971 [para:523667.1.1,523662.1.2.2.2.2,demod:523667] equal(plus(X,plus(Y,times(plus(Z,U),V))),plus(X,plus(times(U,V),plus(Y,times(plus(Z,U),V))))).
% 527974 [para:523671.1.1,523662.1.2.2.2.2,demod:525457,523628,525501] equal(plus(X,plus(Y,times(plus(Z,U),U))),plus(X,plus(U,plus(Y,times(plus(Z,U),U))))).
% 528062 [?] ?
% 528250 [para:523687.1.1,525059.1.1.2] equal(plus(X,times(Y,plus(Y,X))),plus(X,plus(Y,times(Y,X)))).
% 528255 [para:523851.1.1,525059.1.1.2.1.2,demod:523633,523630] equal(plus(times(X,plus(X,Y)),Z),plus(times(X,plus(X,Y)),plus(X,Z))).
% 528380 [para:523615.1.1,525277.1.1.1.2] equal(plus(times(X,plus(Y,plus(Z,X))),U),plus(times(X,plus(Y,Z)),plus(X,U))).
% 528440 [para:525277.1.1,525457.1.1,demod:523654] equal(plus(times(X,Y),plus(Y,X)),times(plus(X,plus(Y,X)),plus(Y,X))).
% 528441 [para:525457.1.1,525277.1.1.1.2] equal(plus(times(X,times(plus(Y,X),X)),Z),plus(times(X,times(Y,X)),plus(X,Z))).
% 528539 [para:523654.1.2,525296.1.2.2,demod:524049,523654,525501] equal(times(plus(X,Y),plus(Y,plus(X,Y))),plus(times(X,Y),plus(X,Y))).
% 528761 [para:527672.1.1,525317.1.2.2.1,demod:525317,525313,523614] equal(times(X,times(plus(Y,plus(Z,Y)),times(Y,Z))),times(X,times(Y,Z))).
% 528817 [para:524047.1.1,525321.1.1.2,demod:528250,528062,523615,525300] equal(times(X,Y),times(X,times(plus(Y,times(X,plus(X,Y))),Y))).
% 528852 [para:525321.1.1,525524.1.1,demod:525300] equal(times(X,times(plus(X,times(plus(Y,X),Y)),Y)),times(X,Y)).
% 528890 [para:524823.1.2,525321.1.1.2.2.1,demod:524318,523643,523936] equal(times(plus(X,Y),times(Z,X)),times(plus(X,Y),times(Z,plus(X,times(Y,X))))).
% 529223 [para:524068.1.1,523665.1.2.2.2.2,demod:523665] equal(plus(times(X,Y),plus(Z,plus(U,times(plus(X,V),V)))),plus(times(X,Y),plus(Z,plus(U,V)))).
% 529237 [para:523665.1.2,524792.1.2,demod:523658] equal(plus(X,plus(Y,Z)),plus(X,plus(times(plus(X,Z),Y),plus(Y,Z)))).
% 529261 [para:523627.1.1,525500.1.1.1,demod:523614,525457] equal(times(plus(X,Y),Y),times(plus(times(X,times(Y,X)),Y),Y)).
% 529262 [para:523630.1.2,525500.1.1.1.2,demod:525457] equal(times(plus(X,times(Y,Z)),times(Y,Z)),times(plus(times(X,Y),times(Y,Z)),times(Y,Z))).
% 529266 [para:523642.1.2,525500.1.1.1,demod:525457] equal(times(plus(X,times(Y,Z)),times(Y,Z)),times(plus(times(X,Z),times(Y,Z)),times(Y,Z))).
% 529274 [para:525500.1.1,523654.1.2,demod:523654] equal(plus(times(X,times(Y,plus(Z,plus(U,Z)))),plus(U,Z)),times(plus(times(X,Y),plus(U,Z)),plus(Z,plus(U,Z)))).
% 529404 [para:523615.1.1,525501.1.1.1.1] equal(plus(times(plus(X,plus(Y,Z)),Z),U),plus(times(plus(X,Y),Z),plus(Z,U))).
% 529406 [para:523617.1.1,525501.1.1.1] equal(plus(times(plus(X,times(Y,times(Z,U))),times(Z,times(Y,U))),V),plus(times(X,times(Y,times(Z,U))),plus(times(Y,times(Z,U)),V))).
% 529542 [para:525527.1.2,523643.1.2.2,demod:523643] equal(times(X,times(plus(times(Y,times(X,Z)),plus(Y,times(X,Z))),Z)),times(X,times(plus(Y,times(X,Z)),Z))).
% 529825 [para:525542.1.2,525500.1.1.1,demod:525457] equal(times(plus(X,times(Y,Z)),times(Y,Z)),times(plus(times(X,plus(X,Y)),times(Y,Z)),times(Y,Z))).
% 530007 [para:523741.1.1,525582.1.2.2.1.2,demod:524363,528250,528062,523615] equal(times(plus(X,Y),X),times(plus(X,times(Y,plus(Y,X))),X)).
% 530235 [para:523673.1.1,523934.1.1.2.2,demod:525500,525503,523643,523649,523614] equal(times(plus(X,times(Y,times(plus(Z,Y),U))),times(Y,times(plus(Z,Y),U))),times(plus(times(X,plus(Z,Y)),times(Y,U)),times(Y,U))).
% 530297 [para:524365.1.1,525643.1.1.1.2,demod:524242,523633] equal(times(plus(X,times(X,Y)),times(Z,plus(X,Y))),times(X,times(Z,plus(X,times(X,Y))))).
% 530400 [para:523767.1.1,525645.1.1.2] equal(times(X,plus(Y,times(Y,X))),times(X,times(Y,plus(Y,X)))).
% 530524 [para:525665.1.2,525457.1.1.1,demod:529825,530235] equal(plus(times(X,times(Y,Z)),times(Y,times(plus(X,Y),Z))),times(plus(X,times(Y,Z)),times(Y,Z))).
% 531587 [para:523675.1.1,524943.1.1.2,demod:527616,523615] equal(plus(X,plus(Y,times(plus(Z,plus(X,Y)),Z))),plus(X,plus(Y,times(plus(Z,Y),Z)))).
% 531919 [para:527616.1.2,523632.1.1.2.2,demod:527616,528250,528062,527971,523615] equal(plus(X,plus(Y,times(X,plus(X,Y)))),plus(X,times(plus(Y,X),Y))).
% 532147 [para:523676.1.1,523654.1.2.2.2,demod:523667,523676] equal(plus(X,times(plus(Y,Z),U)),plus(X,times(plus(Z,plus(Y,Z)),U))).
% 532218 [para:523633.1.2,528817.1.2.2.1.2.2,demod:523767,531919,523615] equal(times(X,plus(X,Y)),times(X,plus(X,times(plus(Y,X),Y)))).
% 532341 [para:524823.1.2,528852.1.1.2.1.2.1,demod:524363,524318,528250,528062,523615,523627,528890] equal(times(plus(X,times(Y,plus(Y,X))),plus(X,times(Y,X))),times(plus(X,Y),X)).
% 532449 [para:525527.1.2,529261.1.2.1.1.2,demod:523706,523654,528441,524786] equal(times(plus(X,plus(Y,X)),plus(times(Y,X),plus(Y,X))),plus(times(X,times(Y,X)),plus(Y,X))).
% 532572 [para:527616.1.2,530007.1.2.1.2.2,demod:532341,526953,532218,523768,523834,525202,523615] equal(plus(X,times(Y,X)),times(plus(X,Y),X)).
% 532574 [para:523614.1.1,532572.1.1.2] equal(plus(X,times(Y,times(Z,X))),times(plus(X,times(Y,Z)),X)).
% 532575 [para:532572.1.1,523615.1.1,demod:523615] equal(times(plus(X,plus(Y,Z)),plus(X,Y)),plus(X,plus(Y,times(Z,plus(X,Y))))).
% 532576 [para:532572.1.1,523615.1.1.1] equal(plus(times(plus(X,Y),X),Z),plus(X,plus(times(Y,X),Z))).
% 532601 [para:532572.1.1,524803.1.1.1.2] equal(plus(times(X,times(plus(X,Y),X)),Y),plus(X,Y)).
% 532609 [para:524256.1.1,532572.1.1.2,demod:525611,532572,525501,525457] equal(plus(times(X,Y),times(plus(Y,plus(X,Z)),Y)),times(plus(times(X,Y),plus(Y,plus(X,Z))),Y)).
% 532631 [para:532572.1.1,525277.1.1,demod:525277] equal(times(plus(times(X,Y),plus(X,Z)),times(X,plus(Y,X))),plus(times(X,Y),plus(X,times(Z,times(X,plus(Y,X)))))).
% 532787 [para:532601.1.1,523658.1.2.2.2,demod:527596] equal(plus(times(X,times(plus(X,Y),X)),plus(Z,Y)),plus(X,plus(Z,Y))).
% 533397 [para:523627.1.1,532574.1.1.2,demod:523614,532572] equal(times(plus(X,Y),X),times(plus(X,times(Y,times(X,Y))),X)).
% 533405 [para:523643.1.2,532574.1.1.2] equal(plus(times(X,Y),times(X,times(Z,Y))),times(plus(times(X,Y),times(X,Z)),times(X,Y))).
% 533424 [para:524046.1.1,532574.1.1.2.2,demod:525295,532572,532631,525277,525202] equal(times(plus(times(X,Y),plus(X,Z)),times(X,plus(Y,X))),plus(times(X,Y),times(plus(X,Z),X))).
% 533454 [para:523649.1.2,532574.1.1.2,demod:532572] equal(times(plus(times(X,times(Y,Z)),U),times(X,times(Y,Z))),times(plus(times(X,times(Y,Z)),times(U,Z)),times(X,times(Y,Z)))).
% 533462 [para:524256.1.1,532574.1.1.2.2,demod:525611,532574,525501,525457] equal(plus(times(X,Y),times(plus(Y,times(Z,plus(X,U))),Y)),times(plus(times(X,Y),plus(Y,times(Z,plus(X,U)))),Y)).
% 533534 [para:523615.1.1,532576.1.1.1.1,demod:523615] equal(plus(times(plus(X,plus(Y,Z)),plus(X,Y)),U),plus(X,plus(Y,plus(times(Z,plus(X,Y)),U)))).
% 533540 [para:523658.1.2,532576.1.1.1.1,demod:532576] equal(plus(X,plus(times(plus(Y,Z),X),U)),plus(X,plus(times(plus(Y,plus(X,Z)),X),U))).
% 533543 [para:523668.1.1,532576.1.1.1.1,demod:523642,523614] equal(plus(times(plus(X,Y),times(X,Z)),U),plus(times(X,Z),plus(times(plus(X,Y),times(X,Z)),U))).
% 534006 [para:523614.1.1,533397.1.2.1.2,demod:523643,523649] equal(times(plus(X,times(Y,Z)),X),times(plus(X,times(Y,times(X,Z))),X)).
% 534282 [para:523805.1.1,523680.1.2.2.2,demod:523717] equal(plus(X,plus(Y,times(plus(Z,plus(Y,U)),plus(U,plus(Y,U))))),plus(X,times(plus(Z,plus(Y,U)),plus(U,plus(Y,U))))).
% 534575 [para:523701.1.1,523698.1.2,demod:525277,525202,528380,528539,523643,530400,523614,523627,523628,532575] equal(plus(X,Y),plus(X,times(Y,plus(times(X,Y),plus(X,Y))))).
% 534576 [para:523614.1.1,534575.1.2.2] equal(plus(X,times(Y,Z)),plus(X,times(Y,times(Z,plus(times(X,times(Y,Z)),plus(X,times(Y,Z))))))).
% 534642 [para:526090.1.2,534575.1.2.2.2.2,demod:532449,523614,523706,529274,526090] equal(plus(X,Y),plus(X,times(Y,plus(times(Y,times(X,Y)),plus(X,Y))))).
% 536470 [?] ?
% 536544 [para:523679.1.1,523827.1.2.2.2.2,demod:523652,523643,524146,523614,523679] equal(plus(X,times(Y,times(Z,times(plus(U,Y),V)))),plus(X,plus(times(Y,times(Z,V)),times(Y,times(Z,times(plus(U,Y),V)))))).
% 538406 [para:523936.1.1,523614.1.1.1,demod:523643,532572,523614] equal(times(plus(X,Y),times(Z,U)),times(plus(X,Y),times(Z,times(plus(Z,Y),U)))).
% 538408 [para:523615.1.1,523936.1.1.1,demod:523615,523642,532572] equal(times(plus(X,plus(Y,Z)),times(plus(U,Z),U)),times(plus(X,plus(Y,Z)),U)).
% 538414 [para:523936.1.1,523643.1.2.2.2,demod:523643,523642,532572] equal(times(plus(X,Y),times(Z,times(plus(U,Y),U))),times(plus(X,Y),times(Z,U))).
% 538435 [para:523936.1.1,524233.1.1.1.2,demod:523627,538406,538408,523642,532787,533454,532572] equal(times(plus(X,plus(Y,Z)),X),plus(times(X,times(plus(X,Z),X)),times(plus(Y,Z),X))).
% 538436 [para:524233.1.1,523936.1.1.2.2.2,demod:523642,523741,532572] equal(times(plus(X,times(plus(Y,Z),Y)),times(plus(Y,Z),Y)),times(plus(X,times(plus(Y,Z),Y)),Y)).
% 538459 [para:523936.1.1,523652.1.2.2.2.2,demod:523652,523642,532572] equal(times(plus(X,Y),times(Z,times(U,times(plus(V,Y),V)))),times(plus(X,Y),times(Z,times(U,V)))).
% 538488 [para:523936.1.1,525582.1.2.2.1.2.2,demod:525543,523642,531587,523615,538435,523627,538406,532572] equal(times(plus(X,Y),Z),times(plus(X,Y),times(plus(Z,Y),Z))).
% 538568 [para:538488.1.2,523614.1.1.1,demod:523614] equal(times(plus(X,Y),times(Z,U)),times(plus(X,Y),times(plus(Z,Y),times(Z,U)))).
% 538585 [para:524233.1.1,538488.1.2.2,demod:532572] equal(times(plus(X,times(Y,Z)),Z),times(plus(X,times(Y,Z)),times(plus(Z,Y),Z))).
% 538623 [para:538488.1.2,525500.1.1.1.2,demod:538436] equal(plus(times(X,times(plus(Y,Z),U)),times(plus(U,Z),U)),times(plus(times(X,plus(Y,Z)),times(plus(U,Z),U)),U)).
% 538631 [para:538488.1.2,525848.1.1.2.1.2,demod:525546,523614,532572,523682,532576] equal(times(X,times(Y,plus(Z,U))),times(X,times(plus(Y,U),times(Y,plus(Z,U))))).
% 539078 [para:524233.1.1,523980.1.2.2,demod:538436,529262,523642,523627,523614,538623,532572] equal(times(plus(times(X,plus(Y,Z)),times(plus(Y,Z),Y)),Y),times(plus(X,times(plus(Y,Z),Y)),Y)).
% 539232 [para:525665.1.2,523988.1.2.2.2.1,demod:523643,523642,525593,523614,530524,525665] equal(times(X,times(plus(Y,times(Z,U)),times(Z,U))),times(X,times(Z,times(plus(Y,Z),U)))).
% 539254 [para:523988.1.2,532574.1.1.2,demod:525523,532572,533462,532574,525501,525457] equal(times(plus(times(X,Y),plus(Y,times(Z,plus(X,Y)))),Y),plus(times(X,Y),times(plus(Y,Z),Y))).
% 539455 [para:524071.1.1,523643.1.2.2,demod:523630,524419] equal(times(plus(X,times(X,Y)),plus(Z,Y)),times(X,plus(Z,Y))).
% 539496 [para:523871.1.2,524071.1.1.2,demod:523900,524365,530297] equal(plus(X,times(X,Y)),times(X,plus(X,Y))).
% 539503 [para:525300.1.1,524071.1.1.1.2,demod:523643,523614,539496] equal(times(X,times(plus(X,Y),plus(Z,times(plus(Y,X),Y)))),times(X,plus(Z,times(plus(Y,X),Y)))).
% 539529 [para:524071.1.1,524498.1.2.1.1,demod:523869,533405,523628,523630,538631,523614,539496] equal(times(X,plus(Y,Z)),times(X,times(plus(X,Z),plus(Y,Z)))).
% 539580 [para:532572.1.1,524071.1.1.2.2,demod:532572,538585,523643,523614,539496] equal(times(X,times(plus(X,times(Y,Z)),Z)),times(X,times(plus(Z,Y),Z))).
% 539610 [para:523889.1.1,524071.1.1.2.2,demod:523838,523615,525202,533534,523643,523614,539496] equal(times(X,times(plus(X,Y),plus(Z,plus(U,Y)))),times(X,plus(Z,plus(U,Y)))).
% 539621 [para:539496.1.1,523615.1.1,demod:523615] equal(times(plus(X,Y),plus(X,plus(Y,Z))),plus(X,plus(Y,times(plus(X,Y),Z)))).
% 539622 [para:539496.1.1,523615.1.1.1] equal(plus(times(X,plus(X,Y)),Z),plus(X,plus(times(X,Y),Z))).
% 539623 [para:523629.1.2,539496.1.1.2,demod:539496] equal(times(X,plus(X,Y)),times(X,plus(X,times(Y,times(X,Y))))).
% 539625 [para:523642.1.2,539496.1.1.2,demod:539496] equal(times(X,plus(X,times(Y,Z))),times(X,plus(X,times(Z,times(Y,Z))))).
% 539629 [para:539496.1.1,523658.1.2.2.2] equal(plus(X,plus(Y,times(X,Z))),plus(X,plus(Y,times(X,plus(X,Z))))).
% 539638 [para:539496.1.1,523767.1.1.2] equal(times(plus(X,times(Y,times(X,Z))),times(X,plus(X,Z))),plus(X,times(Y,times(X,Z)))).
% 539670 [para:539496.1.1,525277.1.1,demod:539496,523614,525277] equal(times(X,times(plus(Y,X),plus(times(X,Y),plus(X,Z)))),plus(times(X,Y),times(X,plus(X,times(plus(Y,X),Z))))).
% 539689 [para:539496.1.1,532576.1.1.1.1,demod:523614] equal(plus(times(X,times(plus(X,Y),X)),Z),plus(X,plus(times(X,times(Y,X)),Z))).
% 539717 [para:539455.1.1,523614.1.1.1,demod:539496,523614] equal(times(X,times(plus(Y,Z),U)),times(X,times(plus(X,Z),times(plus(Y,Z),U)))).
% 539719 [para:523630.1.2,539455.1.1.1.2,demod:523614,539496] equal(times(X,times(plus(X,Y),plus(Z,times(X,Y)))),times(X,plus(Z,times(X,Y)))).
% 539792 [para:524071.1.1,539455.1.1.1.2,demod:539719,523614,523792,539622,539496] equal(times(X,plus(Y,times(X,plus(Z,U)))),times(X,times(plus(X,U),plus(Y,times(X,plus(Z,U)))))).
% 539805 [para:523706.1.1,539529.1.2.2,demod:523614] equal(times(X,times(Y,plus(Y,Z))),times(X,times(Y,plus(times(X,Y),Z)))).
% 539810 [para:523811.1.1,539529.1.2.2.1] equal(times(X,plus(Y,plus(Z,times(plus(X,U),U)))),times(X,times(plus(X,plus(Z,U)),plus(Y,plus(Z,times(plus(X,U),U)))))).
% 539894 [para:523906.1.2,539529.1.2.2.2,demod:539529,539805] equal(times(X,plus(times(Y,times(Z,plus(Z,U))),U)),times(X,plus(times(Y,Z),U))).
% 540189 [para:539623.1.2,523642.1.2.2.2,demod:539638,523630,539496,539625] equal(times(X,times(Y,plus(Y,Z))),times(X,plus(Y,times(Z,times(Y,Z))))).
% 540193 [?] ?
% 540331 [para:524094.1.2,527022.1.2.2.2,demod:523649,539232,523630,525524,523614,539496] equal(plus(X,times(Y,Z)),plus(X,times(Y,times(plus(X,Y),Z)))).
% 540332 [para:524094.1.2,524798.1.1.2.1,demod:525202,539805,523630,525524,523614,539496] equal(plus(times(X,times(Y,plus(Y,Z))),times(Z,plus(times(X,Y),Z))),plus(times(X,Y),Z)).
% 540473 [para:523617.1.1,540331.1.2.2] equal(plus(X,times(Y,times(Z,U))),plus(X,times(Y,times(Z,times(plus(X,Y),U))))).
% 540480 [para:523781.1.1,540331.1.2.2.2.1,demod:539670,523630,523614,539496,525277] equal(plus(times(X,Y),times(X,plus(X,Z))),times(X,times(plus(Y,X),plus(times(X,Y),plus(X,Z))))).
% 540489 [para:523767.1.1,540331.1.2.2.2,demod:523837,523614] equal(plus(X,times(Y,times(Z,plus(X,Z)))),plus(X,times(Y,Z))).
% 540502 [para:524256.1.1,540331.1.2.2.2,demod:540331,525457] equal(plus(X,times(Y,times(plus(X,Z),Z))),plus(X,times(Y,Z))).
% 540630 [para:523632.1.1,540489.1.1.2.2.2,demod:528440] equal(plus(X,times(Y,plus(times(Z,X),plus(X,Z)))),plus(X,times(Y,plus(Z,plus(X,Z))))).
% 540818 [para:523700.1.1,540502.1.1.2.2.1,demod:528440,523834] equal(plus(X,times(Y,plus(times(X,Z),plus(Z,X)))),plus(X,times(Y,plus(Z,X)))).
% 541062 [para:523906.1.2,523704.1.1.2.2.1.2.2,demod:540332,536470,525296,528440,539894,523614,539496,539805] equal(plus(times(X,Y),Z),plus(times(X,times(Y,plus(Y,Z))),Z)).
% 541075 [para:523741.1.1,541062.1.2.1.2.2,demod:539078,538623,523642] equal(plus(times(X,Y),times(plus(Y,Z),Y)),times(plus(X,times(plus(Y,Z),Y)),Y)).
% 541081 [para:523882.1.1,541062.1.2.1.2.2,demod:541062,540189,540193,523614] equal(plus(times(X,times(plus(Y,Z),Y)),Z),plus(times(X,Y),Z)).
% 541156 [para:532574.1.1,541062.1.2.1.2.2,demod:523642] equal(plus(times(X,Y),times(Z,times(U,Y))),plus(times(X,times(plus(Y,times(Z,U)),Y)),times(Z,times(U,Y)))).
% 541317 [para:541081.1.1,532576.1.1.1.1,demod:525321,532576,538414] equal(plus(times(X,Y),plus(times(Z,times(X,Y)),U)),plus(times(X,times(plus(Y,Z),Y)),plus(times(Z,times(X,Y)),U))).
% 541401 [para:525527.1.2,524108.1.1.2,demod:529542,523630,539232,525524,523614,539496] equal(times(X,times(plus(Y,X),Z)),times(X,times(plus(Y,times(X,Z)),Z))).
% 541440 [para:524124.1.2,523718.1.2.2.2.1,demod:525507,525511,527226,540818,523615,524792,528440] equal(plus(X,times(plus(Y,plus(Z,U)),plus(times(U,Z),plus(Z,U)))),plus(X,plus(times(U,Z),times(plus(Y,plus(Z,U)),plus(Z,U))))).
% 541498 [para:523711.1.1,523914.1.1.1.2,demod:540473,536544,523615,525503,523643,523711,523652,523630,524146,539232,523614] equal(times(plus(X,times(Y,times(Z,U))),times(Y,times(Z,times(plus(X,Y),U)))),times(plus(X,times(Y,times(Z,U))),times(Y,times(Z,U)))).
% 541505 [para:523711.1.1,525524.1.1.2.1,demod:523652,523630,524146,539232,523643,523649,523614] equal(times(plus(X,times(Y,times(Z,U))),times(Z,times(Y,times(plus(X,Y),U)))),times(plus(X,times(Y,times(Z,U))),times(Z,times(Y,U)))).
% 541574 [para:524255.1.1,523658.1.2.2,demod:523633,539622] equal(plus(X,plus(times(X,Y),times(Z,Y))),plus(X,times(Z,Y))).
% 541690 [para:523667.1.1,541574.1.1.2,demod:539496,539621,523615] equal(times(plus(X,Y),plus(X,plus(Y,Z))),plus(X,times(Y,plus(Y,Z)))).
% 542014 [para:539529.1.2,524301.1.1.2.2.1,demod:539503,524240,532572,523615,539805,523614,523745,523794,539529] equal(times(X,plus(Y,times(plus(Z,X),Z))),times(X,plus(Y,Z))).
% 542020 [para:523615.1.1,542014.1.1.2,demod:523615] equal(times(X,plus(Y,plus(Z,times(plus(U,X),U)))),times(X,plus(Y,plus(Z,U)))).
% 542038 [para:523741.1.1,542014.1.1.2.2.1,demod:523627,523614] equal(times(plus(X,Y),times(X,plus(Z,times(plus(X,Y),X)))),times(plus(X,Y),times(X,plus(Z,X)))).
% 542057 [para:542014.1.1,524233.1.1.1.2,demod:542014,523768,524240,523614,532575,523792,532576,523615] equal(plus(X,times(plus(Y,Z),Y)),times(plus(X,plus(Y,Z)),plus(X,Y))).
% 542153 [para:523889.1.1,542014.1.1.2,demod:532147,526980,523614,532576,523615,542057,542020] equal(times(X,plus(Y,plus(Z,U))),times(X,plus(Y,plus(Z,times(plus(X,U),U))))).
% 542480 [para:524310.1.2,525202.1.1.1,demod:524066,542038,525276,523614,532572] equal(times(plus(X,Y),times(X,plus(Z,X))),plus(times(X,Z),times(plus(X,Y),X))).
% 543095 [para:523852.1.1,523714.1.2.2.2.1.1.2,demod:534282,540630,541440,532576,525457,523654,523615,525501,523633,524941] equal(plus(X,times(plus(Y,plus(Z,U)),plus(Z,U))),plus(X,times(plus(Y,plus(Z,U)),plus(U,plus(Z,U))))).
% 543287 [para:523633.1.2,524392.1.1.1.1,demod:532576,527622] equal(plus(X,plus(times(Y,X),times(plus(X,Y),Z))),plus(X,times(plus(X,Y),Z))).
% 543292 [para:524392.1.1,523658.1.2.2,demod:523633,532576] equal(plus(X,plus(times(Y,X),times(Y,Z))),plus(X,times(Y,Z))).
% 543302 [para:523851.1.1,524392.1.1.1.1,demod:539629,539689,539496,523614] equal(plus(X,plus(times(X,times(Y,X)),times(X,times(plus(X,Y),Z)))),times(X,plus(X,times(plus(X,Y),Z)))).
% 543326 [para:524068.1.1,524392.1.1.2,demod:524068,533543,532576,527622] equal(plus(times(plus(X,Y),times(X,Z)),Y),plus(times(X,Z),Y)).
% 543449 [para:524351.1.1,543292.1.1.2.1,demod:543292,541317,532572] equal(plus(times(X,Y),times(Z,U)),plus(times(X,times(plus(Y,Z),Y)),times(Z,U))).
% 543523 [para:523617.1.1,543326.1.1.1] equal(plus(times(plus(X,Y),times(Z,times(X,U))),Y),plus(times(X,times(Z,U)),Y)).
% 543525 [para:523643.1.2,543326.1.1.1,demod:543326] equal(plus(times(X,Y),Z),plus(times(X,times(plus(X,Z),Y)),Z)).
% 543542 [para:523851.1.1,543326.1.1.1.1,demod:539792,525276,523643,523614] equal(times(X,plus(Y,times(X,plus(X,Z)))),plus(times(X,Y),times(X,plus(X,Z)))).
% 543593 [para:543326.1.1,524941.1.1.1.1,demod:524941,538568] equal(plus(times(X,Y),plus(Z,U)),plus(times(plus(X,U),times(X,Y)),plus(Z,U))).
% 543594 [para:524941.1.1,543326.1.1.1.1,demod:543593,543523,523614] equal(plus(times(X,times(plus(X,Y),Z)),plus(U,Y)),plus(times(X,Z),plus(U,Y))).
% 543621 [para:543326.1.1,532576.1.1.1.1,demod:523674,525313,532576,538568] equal(plus(times(X,Y),plus(times(Z,times(X,Y)),U)),plus(times(plus(X,Z),times(X,Y)),U)).
% 543685 [para:523614.1.1,543525.1.2.1,demod:523614] equal(plus(times(X,times(Y,Z)),U),plus(times(X,times(Y,times(plus(times(X,Y),U),Z))),U)).
% 543690 [para:543525.1.2,523658.1.2.2.2,demod:543594] equal(plus(times(X,Y),plus(Z,U)),plus(times(X,times(plus(X,U),Y)),plus(Z,plus(times(X,Y),U)))).
% 543712 [para:523871.1.2,543525.1.2.1.2,demod:536470,526428,523780,525457,539622,541690,523615] equal(plus(X,plus(times(X,plus(Y,Z)),Y)),plus(X,times(Y,plus(Z,Y)))).
% 543803 [para:523906.1.2,543525.1.2.1.2.1,demod:543685,539717,523614,539805] equal(plus(times(X,times(Y,times(plus(Y,Z),U))),Z),plus(times(X,times(Y,U)),Z)).
% 543842 [para:543525.1.2,524392.1.1.2,demod:543525,543621,543803,543690,532576] equal(plus(times(plus(X,Y),times(X,Z)),times(Y,U)),plus(times(X,Z),times(Y,U))).
% 543849 [para:523633.1.2,524394.1.1.2.2,demod:523633,523643,523614,525202] equal(times(X,times(plus(Y,X),plus(Y,Z))),times(X,plus(Y,Z))).
% 543861 [para:523781.1.1,524394.1.1.1,demod:541690,523643,523614,523615] equal(times(X,plus(Y,times(X,plus(X,Z)))),times(X,plus(Y,plus(X,Z)))).
% 544339 [para:543849.1.1,523639.1.1.2.2] equal(times(X,times(Y,times(Z,plus(U,V)))),times(X,times(plus(U,Z),times(Y,times(Z,plus(U,V)))))).
% 544544 [para:524046.1.1,524439.1.2.1.1,demod:543861,543542,540480,539670,539496,525277,523630,523614,525202] equal(times(X,times(plus(Y,X),Z)),times(X,times(plus(Y,plus(X,Z)),Z))).
% 544650 [para:524440.1.2,523630.1.2.2,demod:541690,539621] equal(times(plus(X,times(Y,plus(Y,Z))),Z),times(plus(X,times(Y,plus(Y,Z))),times(plus(X,Y),Z))).
% 544651 [para:523630.1.2,524440.1.2.1.2.2,demod:544650,541690,539621,523630] equal(times(plus(X,Y),Z),times(plus(X,times(Y,plus(Y,Z))),Z)).
% 544765 [para:523870.1.1,524440.1.2.1.2.2.1,demod:539580,523851,543302,539689,523643,523614,523870] equal(times(X,times(plus(X,Y),Z)),times(X,times(plus(Z,plus(X,Y)),Z))).
% 544911 [para:523668.1.1,544651.1.2.1,demod:544651,541690,543712,539622,528255,523615] equal(times(plus(X,times(Y,plus(Z,Y))),Z),times(plus(X,Y),Z)).
% 544913 [para:523687.1.1,544651.1.2.1,demod:544544,523614,523654,523615,525202] equal(times(X,times(plus(Y,plus(Z,X)),Z)),times(X,times(plus(Y,X),Z))).
% 545056 [para:523934.1.1,544911.1.1.1.2.2,demod:544911,523927,523614] equal(times(plus(X,Y),times(Z,U)),times(plus(X,times(Y,plus(U,Y))),times(Z,U))).
% 545096 [para:544911.1.1,525643.1.1.1.2,demod:545056,541690,539621,527971,525277,523615] equal(times(plus(X,times(Y,plus(Y,Z))),times(U,Z)),times(plus(X,Y),times(U,Z))).
% 545243 [para:524444.1.1,524318.1.2.2.2.2,demod:523643,523642,538414,532572,543449,525321,539580,523614,539496] equal(times(X,times(plus(times(Y,Z),U),times(Y,Z))),times(X,times(Y,times(plus(Z,U),Z)))).
% 545751 [para:524516.1.1,532574.1.1.2,demod:523642,532574,523627,543449,532572,539496] equal(times(plus(X,times(Y,Z)),X),times(plus(X,times(Y,Z)),times(plus(X,Y),X))).
% 546053 [para:524543.1.2,525465.1.1.1.2.1,demod:523811,527974,523654,525457,529223,542153,539810] equal(times(plus(X,plus(Y,Z)),plus(Z,plus(Y,Z))),times(plus(X,plus(Y,Z)),plus(Z,plus(Y,times(plus(X,Z),Z))))).
% 546099 [para:524543.1.2,523718.1.2.2.2.1,demod:525457,523658,523654,525447,525501,523615,543095,546053,523811,527974] equal(plus(X,times(plus(Y,plus(Z,U)),plus(Z,U))),plus(X,plus(Z,times(plus(Y,U),U)))).
% 547220 [para:525277.1.1,524842.1.2.1.2.1,demod:539610,523643,544339,543861,543542,540480,523614,542480,533424,532631,525277] equal(plus(times(X,Y),plus(X,Z)),plus(times(X,plus(Y,plus(X,Z))),Z)).
% 547228 [para:524842.1.2,523820.1.2.2,demod:547220,543861,539792,523630,539496,539625,540193,523614,532572] equal(plus(times(X,Y),plus(X,Z)),plus(times(X,plus(Y,plus(X,Z))),plus(X,Z))).
% 547779 [para:525312.1.2,524318.1.2.2.2.2,demod:545751,523643,523649,523614,545243,532572,541156,525312] equal(times(X,times(Y,times(plus(Z,U),Z))),times(X,times(Y,times(plus(Z,times(U,Y)),Z)))).
% 548212 [para:525357.1.2,523703.1.1.2,demod:532572,543842] equal(times(plus(times(X,Y),Z),times(X,Y)),times(plus(X,Z),times(X,Y))).
% 549012 [para:525786.1.1,541574.1.1.2.1,demod:528761,548212,532572] equal(plus(X,times(plus(X,Y),times(X,Z))),plus(X,times(Y,times(X,Z)))).
% 549100 [para:525929.1.1,524310.1.2.1.2,demod:523643,523652,523614,548212,532572,543449,525321,539580] equal(times(plus(X,Y),times(X,times(Z,U))),times(plus(X,Y),times(X,times(Z,times(plus(Z,Y),U))))).
% 552640 [para:526980.1.2,523658.1.2,demod:523633,546099,541081] equal(plus(X,plus(times(Y,X),Z)),plus(X,times(plus(Y,Z),Z))).
% 552642 [para:523658.1.2,526980.1.2,demod:541081,523633,546099] equal(plus(X,times(plus(Y,Z),Z)),plus(X,plus(times(Y,X),Z))).
% 552944 [para:523667.1.1,552640.1.1.2,demod:532574,545096,539496,523615,532572] equal(times(plus(X,plus(Y,Z)),X),times(plus(X,times(plus(Y,Z),Z)),X)).
% 552945 [para:523667.1.1,552640.1.2.2.1,demod:523642,523614] equal(plus(X,plus(times(plus(Y,Z),times(U,X)),times(Z,U))),plus(X,times(plus(Y,Z),times(Z,U)))).
% 552951 [para:552640.1.1,523741.1.1.2.1,demod:523741,552944] equal(times(plus(X,plus(Y,Z)),X),times(plus(X,plus(times(Y,X),Z)),X)).
% 553158 [para:525501.1.1,552640.1.1.2,demod:523615,523658] equal(plus(X,plus(times(Y,X),Z)),plus(X,times(plus(Y,plus(X,Z)),Z))).
% 553634 [para:523707.1.1,552642.1.2.2.1,demod:523658,553158,523615] equal(plus(times(X,Y),plus(Z,plus(times(X,Z),U))),plus(times(X,Y),plus(Z,U))).
% 554767 [para:527050.1.2,523767.1.1.1,demod:540331,541401,524368] equal(plus(X,times(plus(X,times(Y,Z)),Z)),plus(X,times(Y,Z))).
% 554896 [para:554767.1.1,524345.1.2.2.2,demod:523649,547779,523642,523614,532574] equal(times(plus(X,times(Y,Z)),times(Z,X)),times(plus(X,times(Y,Z)),times(Z,times(plus(X,Y),X)))).
% 556244 [para:523743.1.1,523706.1.1.2,demod:529266] equal(times(plus(X,times(plus(Y,Z),times(Y,U))),times(plus(Y,Z),times(Y,U))),plus(times(X,times(Y,U)),times(plus(Y,Z),times(Y,U)))).
% 556245 [para:523920.1.1,523743.1.1.1,demod:532609,552951,523658,532572,525611,523627,523614,525501,525457] equal(times(plus(times(X,Y),plus(Y,plus(X,Z))),Y),times(plus(times(X,Y),plus(Y,Z)),Y)).
% 556267 [para:523743.1.1,525501.1.1,demod:556245,532609,523658,532572,525588,523615] equal(times(plus(X,plus(Y,Z)),Y),times(plus(times(X,Y),plus(Y,Z)),Y)).
% 556281 [para:523743.1.1,538488.1.2.2.1,demod:556244,523630,523642,523614] equal(times(plus(X,times(plus(Y,Z),times(Y,U))),times(Y,U)),plus(times(X,times(Y,U)),times(plus(Y,Z),times(Y,U)))).
% 557045 [para:523744.1.1,544911.1.1.1,demod:547228,539610,525300,523614] equal(times(plus(X,Y),Z),times(plus(times(X,Z),plus(X,Y)),Z)).
% 557075 [para:523707.1.1,557045.1.2.1.1,demod:542057,523658,523615] equal(times(plus(X,plus(Y,Z)),plus(times(X,U),Y)),plus(times(X,U),times(plus(Y,plus(X,Z)),Y))).
% 558341 [para:523745.1.2,523618.1.1] equal(plus(times(plus(X,Y),Z),plus(U,V)),plus(times(X,Z),plus(U,plus(times(plus(X,Y),Z),V)))).
% 558416 [para:523745.1.2,525501.1.1,demod:558341,533540,523615] equal(plus(times(plus(X,plus(Y,Z)),Y),U),plus(times(plus(X,Z),Y),plus(Y,U))).
% 558441 [para:523745.1.2,523682.1.2] equal(plus(times(X,Y),times(plus(Z,plus(X,U)),Y)),plus(times(plus(X,U),Y),times(plus(Z,plus(X,U)),Y))).
% 558933 [para:527717.1.1,523667.1.1.1.1,demod:525588,525457,523628,557075,532147,556281,558441,523614] equal(times(plus(X,times(plus(X,Y),times(Y,Z))),times(Y,Z)),times(plus(X,Y),times(Y,Z))).
% 558994 [para:527717.1.1,525314.1.1.2.2,demod:525588,525457,523628,557075,544913,556267,525611,553634,532576,527622,529404] equal(times(X,times(plus(Y,X),Z)),times(X,times(plus(Y,Z),Z))).
% 559405 [para:558994.1.2,524233.1.1.1.2,demod:541075,539254,523627,526071,523614,523843,556267,533462,532574,525501] equal(times(plus(X,plus(Y,Z)),Y),times(plus(X,times(plus(Y,Z),Y)),Y)).
% 559835 [para:558994.1.2,524310.1.2,demod:523633,559405,542057,532575,523615] equal(times(plus(X,plus(Y,Z)),Y),times(plus(X,times(plus(Y,Z),Y)),times(plus(X,plus(Y,Z)),Y))).
% 562290 [para:523749.1.1,524941.1.1.1.1,demod:523652,523643,524146,523614] equal(plus(times(plus(X,Y),times(Z,times(X,U))),plus(V,times(plus(X,Y),times(Z,U)))),plus(times(X,times(Z,times(plus(X,Y),U))),plus(V,times(plus(X,Y),times(Z,U))))).
% 562501 [para:523741.1.1,527844.1.2.2.2.1.2,demod:544765,523658,532572,559405,539078,538623,523741] equal(times(X,times(plus(Y,Z),Y)),times(X,times(plus(X,Z),Y))).
% 562677 [para:562501.1.1,523804.1.2.2.1,demod:558416,559835,523834,525202,523615,532576] equal(plus(X,plus(Y,plus(times(Z,Y),U))),plus(X,plus(times(plus(X,Z),Y),plus(Y,U)))).
% 562743 [para:562501.1.2,523651.1.2.2.2,demod:523652,548212] equal(times(plus(X,Y),times(Z,times(X,U))),times(plus(X,Y),times(Z,times(X,times(plus(Z,Y),U))))).
% 562946 [para:562501.1.2,533397.1.2.1.2.2,demod:534006,549012,523642,562743,523614] equal(times(plus(X,times(plus(X,Y),Z)),X),times(plus(X,times(Y,Z)),X)).
% 563037 [para:562501.1.1,524097.1.1.1.2.2,demod:538459,554896,523649,562946,532574,543287,532576,523642,549100,523614] equal(times(plus(X,times(Y,Z)),times(Z,X)),times(plus(X,Y),times(Z,X))).
% 569323 [para:554767.1.1,529237.1.2.2.2,demod:552945,563037,523614,562677,554767] equal(plus(X,plus(Y,times(Z,U))),plus(X,plus(Y,times(plus(Y,Z),times(Z,U))))).
% 574741 [para:532147.1.2,525643.1.1.1,demod:539629,541690,539621,523615] equal(times(plus(X,plus(Y,times(X,Z))),times(U,Z)),times(plus(X,plus(Y,X)),times(U,Z))).
% 576150 [para:523711.1.1,523777.1.1.2.2.1.1.2,demod:558933,532147,556281,523743,529406,574741,548212,532572,541498,523643,523711,541505,523652,523630,524146,539232,523614] equal(times(plus(X,Y),times(Y,times(Z,U))),times(plus(X,times(Y,times(Z,U))),times(Y,times(Z,U)))).
% 577077 [para:523779.1.1,523907.1.2.2,demod:576150,525457,539622,523779] equal(plus(X,times(Y,times(Z,plus(U,V)))),plus(X,times(plus(X,Y),times(Y,times(Z,plus(U,V)))))).
% 580503 [para:524288.1.2,534642.1.2.2.2.1.2,demod:534576,577077,569323,525665,562290,523643,523649,523614,525457] equal(plus(X,times(plus(X,Y),times(Y,Z))),plus(X,times(Y,Z))).
% 580700 [para:580503.1.1,523644.1.2.2] -equal(times(a,plus(b,times(d,times(c,e)))),times(a,plus(b,times(c,times(d,e))))).
% 725761 [para:523643.1.2,524240.1.2.2.2.2,demod:524243,523643,slowcut:580700] contradiction
% END OF PROOF
%
% Proof found by the following strategy:
%
% using binary resolution
% using first neg lit preferred strategy
% not using sos strategy
% using unit paramodulation strategy
% using unit strategy
% using dynamic demodulation
% using ordered paramodulation
% using kb ordering for equality
% preferring bigger arities for lex ordering
% using clause demodulation
% seconds given: 159
%
%
% old unit clauses discarded
%
% ***GANDALF_FOUND_A_REFUTATION***
%
% Global statistics over all passes:
%
% given clauses: 6756
% derived clauses: 4350798
% kept clauses: 372037
% kept size sum: 0
% kept mid-nuclei: 30
% kept new demods: 228144
% forw unit-subs: 2798162
% forw double-subs: 208147
% forw overdouble-subs: 33412
% backward subs: 148
% fast unit cutoff: 3377
% full unit cutoff: 75
% dbl unit cutoff: 0
% real runtime : 365.78
% process. runtime: 363.5
% specific non-discr-tree subsumption statistics:
% tried: 108263
% length fails: 26
% strength fails: 2694
% predlist fails: 1743
% aux str. fails: 0
% by-lit fails: 0
% full subs tried: 103800
% full subs fail: 69540
%
% ; program args: ("/home/graph/tptp/Systems/Gandalf---c-2.6/gandalf" "-time" "600" "/home/graph/tptp/TSTP/PreparedTPTP/otter:hypothesis:set(auto),clear(print_given)---add_equality:r/LAT/LAT041-1+eq_r.in")
%
%------------------------------------------------------------------------------