%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : RNG035-7 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 20:27:51 EDT 2022 % Result : Unsatisfiable 159.97s 160.39s % Output : CNFRefutation 160.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : RNG035-7 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.14/0.35 % Computer : n019.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon May 30 20:19:40 EDT 2022 % 0.14/0.35 % CPUTime : % 159.97/160.39 Theorem Proved. % 159.97/160.39 % SZS status Unsatisfiable % 159.97/160.39 % SZS output start CNFRefutation % 159.97/160.39 [1=axiom,[], % 159.97/160.39 multiply(a,b) = c]. % 159.97/160.39 [2=axiom,[], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,X10))) = X10]. % 159.97/160.39 [3=axiom,[], % 159.97/160.39 add(multiply(X10,X12),multiply(X11,X12)) = multiply(add(X10,X11),X12)]. % 159.97/160.39 [4=axiom,[], % 159.97/160.39 add(multiply(X10,X11),multiply(X10,X12)) = multiply(X10,add(X11,X12))]. % 159.97/160.39 [5=axiom,[], % 159.97/160.39 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 159.97/160.39 [6=axiom,[], % 159.97/160.39 add(X10,X11) = add(X11,X10)]. % 159.97/160.39 [7=axiom,[], % 159.97/160.39 add(add(X10,X11),X12) = add(X10,add(X11,X12))]. % 159.97/160.39 [8=axiom,[], % 159.97/160.39 add(X10,additive_inverse(X10)) = additive_identity]. % 159.97/160.39 [9=axiom,[], % 159.97/160.39 add(X10,additive_identity) = X10]. % 159.97/160.39 [10=axiom,[], % 159.97/160.39 add(additive_identity,X10) = X10]. % 159.97/160.39 [11=axiom,[], % 159.97/160.39 thtop(X10,X10) = thmfalse]. % 159.97/160.39 [12=axiom,[], % 159.97/160.39 thtop(multiply(b,a),c) = thmtrue]. % 159.97/160.39 [13=param(8,10),[], % 159.97/160.39 additive_inverse(additive_identity) = additive_identity]. % 159.97/160.39 [14=param(3,1),[], % 159.97/160.39 multiply(add(a,X10),b) = add(c,multiply(X10,b))]. % 159.97/160.39 [15=param(3,1),[6], % 159.97/160.39 add(c,multiply(X10,b)) = multiply(add(X10,a),b)]. % 159.97/160.39 [16=param(6,3),[3], % 159.97/160.39 multiply(add(X10,X11),X12) = multiply(add(X11,X10),X12)]. % 159.97/160.39 [18=param(14,9),[1], % 159.97/160.39 add(c,multiply(additive_identity,b)) = c]. % 159.97/160.39 [19=param(4,1),[], % 159.97/160.39 multiply(a,add(b,X10)) = add(c,multiply(a,X10))]. % 159.97/160.39 [20=param(4,1),[6], % 159.97/160.39 add(c,multiply(a,X10)) = multiply(a,add(X10,b))]. % 159.97/160.39 [21=param(4,2),[], % 159.97/160.39 multiply(X10,add(multiply(X10,multiply(X10,X10)),X11)) = add(X10,multiply(X10,X11))]. % 159.97/160.39 [22=param(4,2),[6], % 159.97/160.39 add(X10,multiply(X10,X11)) = multiply(X10,add(X11,multiply(X10,multiply(X10,X10))))]. % 159.97/160.39 [23=param(4,3),[], % 159.97/160.39 multiply(X10,add(X11,X11)) = multiply(add(X10,X10),X11)]. % 159.97/160.39 [24=param(4,6),[4], % 159.97/160.39 multiply(X10,add(X11,X12)) = multiply(X10,add(X12,X11))]. % 159.97/160.39 [27=param(5,1),[], % 159.97/160.39 multiply(a,multiply(b,X10)) = multiply(c,X10)]. % 159.97/160.39 [28=param(5,2),[5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(X10,X11)))) = multiply(X10,X11)]. % 159.97/160.39 [29=param(5,14),[], % 159.97/160.39 multiply(add(a,X10),multiply(b,X11)) = multiply(add(c,multiply(X10,b)),X11)]. % 159.97/160.39 [31=param(27,2),[1], % 159.97/160.39 multiply(c,multiply(b,multiply(b,b))) = c]. % 159.97/160.39 [32=param(4,27),[], % 159.97/160.39 multiply(a,add(multiply(b,X10),X11)) = add(multiply(c,X10),multiply(a,X11))]. % 159.97/160.39 [33=param(4,27),[], % 159.97/160.39 add(multiply(a,X10),multiply(c,X11)) = multiply(a,add(X10,multiply(b,X11)))]. % 159.97/160.39 [34=param(7,6),[], % 159.97/160.39 add(X10,add(X11,X12)) = add(X12,add(X10,X11))]. % 159.97/160.39 [35=param(7,6),[7], % 159.97/160.39 add(X10,add(X11,X12)) = add(X11,add(X10,X12))]. % 159.97/160.39 [37=param(7,8),[10], % 159.97/160.39 add(X11,add(additive_inverse(X11),X10)) = X10]. % 159.97/160.39 [38=param(7,18),[], % 159.97/160.39 add(c,add(multiply(additive_identity,b),X10)) = add(c,X10)]. % 159.97/160.39 [40=param(37,6),[], % 159.97/160.39 add(X10,add(X11,additive_inverse(X10))) = X11]. % 159.97/160.39 [41=param(37,7),[], % 159.97/160.39 add(X11,add(X12,add(additive_inverse(add(X11,X12)),X10))) = X10]. % 159.97/160.39 [42=param(37,8),[9], % 159.97/160.39 additive_inverse(additive_inverse(X10)) = X10]. % 159.97/160.39 [48=param(5,15),[], % 159.97/160.39 multiply(add(c,multiply(X10,b)),X11) = multiply(add(X10,a),multiply(b,X11))]. % 159.97/160.39 [51=param(40,7),[], % 159.97/160.39 add(X10,add(X11,add(X12,additive_inverse(X10)))) = add(X11,X12)]. % 159.97/160.39 [55=param(4,31),[], % 159.97/160.39 multiply(c,add(multiply(b,multiply(b,b)),X10)) = add(c,multiply(c,X10))]. % 159.97/160.39 [57=param(5,31),[5,5], % 159.97/160.39 multiply(c,multiply(b,multiply(b,multiply(b,X10)))) = multiply(c,X10)]. % 159.97/160.39 [66=param(16,20),[5,6], % 159.97/160.39 multiply(a,multiply(add(X10,b),X11)) = multiply(add(c,multiply(a,X10)),X11)]. % 159.97/160.39 [67=param(20,20),[6,19], % 159.97/160.39 add(c,add(c,multiply(a,X10))) = add(c,multiply(a,add(X10,b)))]. % 159.97/160.39 [68=param(4,20),[7,4,7], % 159.97/160.39 add(c,multiply(a,add(X10,X11))) = multiply(a,add(X10,add(b,X11)))]. % 159.97/160.39 [80=param(21,8),[], % 159.97/160.39 add(X10,multiply(X10,additive_inverse(multiply(X10,multiply(X10,X10))))) = multiply(X10,additive_identity)]. % 159.97/160.39 [81=param(21,9),[2], % 159.97/160.39 add(X10,multiply(X10,additive_identity)) = X10]. % 159.97/160.39 [84=param(81,10),[], % 159.97/160.39 multiply(additive_identity,additive_identity) = additive_identity]. % 159.97/160.39 [86=param(37,81),[8], % 159.97/160.39 multiply(additive_inverse(X10),additive_identity) = additive_identity]. % 159.97/160.39 [87=param(5,84),[], % 159.97/160.39 multiply(additive_identity,multiply(additive_identity,X10)) = multiply(additive_identity,X10)]. % 159.97/160.39 [90=param(3,86),[6,10], % 159.97/160.39 multiply(add(X10,additive_inverse(X11)),additive_identity) = multiply(X10,additive_identity)]. % 159.97/160.39 [100=param(87,23),[9,87], % 159.97/160.39 multiply(additive_identity,add(X10,X10)) = multiply(additive_identity,X10)]. % 159.97/160.39 [104=param(4,100),[4,7], % 159.97/160.39 multiply(additive_identity,add(X10,add(X10,X11))) = multiply(additive_identity,add(X10,X11))]. % 159.97/160.39 [105=param(4,100),[4], % 159.97/160.39 multiply(additive_identity,add(X10,add(X11,X11))) = multiply(additive_identity,add(X10,X11))]. % 159.97/160.39 [120=param(20,24),[6,19], % 159.97/160.39 add(c,multiply(a,add(X10,X11))) = add(c,multiply(a,add(X11,X10)))]. % 159.97/160.39 [128=param(28,1),[1], % 159.97/160.39 multiply(a,multiply(a,multiply(a,c))) = c]. % 159.97/160.39 [129=param(28,27),[27], % 159.97/160.39 multiply(a,multiply(a,multiply(a,multiply(c,X10)))) = multiply(c,X10)]. % 159.97/160.39 [132=param(4,128),[], % 159.97/160.39 multiply(a,add(multiply(a,multiply(a,c)),X10)) = add(c,multiply(a,X10))]. % 159.97/160.39 [141=param(90,8),[84], % 159.97/160.39 multiply(X10,additive_identity) = additive_identity]. % 159.97/160.39 [142=demod(80),[141], % 159.97/160.39 add(X10,multiply(X10,additive_inverse(multiply(X10,multiply(X10,X10))))) = additive_identity]. % 159.97/160.39 [144=param(32,6),[], % 159.97/160.39 multiply(a,add(X10,multiply(b,X11))) = add(multiply(c,X11),multiply(a,X10))]. % 159.97/160.39 [169=param(34,40),[], % 159.97/160.39 add(additive_inverse(X10),add(X10,X11)) = X11]. % 159.97/160.39 [174=param(38,34),[], % 159.97/160.39 add(c,add(X10,add(multiply(additive_identity,b),X11))) = add(c,add(X11,X10))]. % 159.97/160.39 [177=param(38,40),[8], % 159.97/160.39 multiply(additive_identity,b) = additive_identity]. % 159.97/160.39 [178=demod(174),[177,10], % 159.97/160.39 add(c,add(X10,X11)) = add(c,add(X11,X10))]. % 159.97/160.39 [181=param(35,6),[7], % 159.97/160.39 add(X10,add(X11,X12)) = add(X10,add(X12,X11))]. % 159.97/160.39 [184=param(35,34),[], % 159.97/160.39 add(X10,add(X11,X12)) = add(X12,add(X11,X10))]. % 159.97/160.39 [189=param(5,177),[], % 159.97/160.39 multiply(additive_identity,multiply(b,X10)) = multiply(additive_identity,X10)]. % 159.97/160.39 [190=param(4,189),[4], % 159.97/160.39 multiply(additive_identity,add(multiply(b,X10),X11)) = multiply(additive_identity,add(X10,X11))]. % 159.97/160.39 [212=param(41,40),[], % 159.97/160.39 add(X10,additive_inverse(add(X10,X11))) = additive_inverse(X11)]. % 159.97/160.39 [217=param(212,3),[], % 159.97/160.39 add(multiply(X10,X11),additive_inverse(multiply(add(X10,X12),X11))) = additive_inverse(multiply(X12,X11))]. % 159.97/160.39 [218=param(212,4),[], % 159.97/160.39 add(multiply(X10,X11),additive_inverse(multiply(X10,add(X11,X12)))) = additive_inverse(multiply(X10,X12))]. % 159.97/160.39 [219=param(212,6),[], % 159.97/160.39 add(X10,additive_inverse(add(X11,X10))) = additive_inverse(X11)]. % 159.97/160.39 [228=param(212,35),[], % 159.97/160.39 add(X10,additive_inverse(add(X11,add(X10,X12)))) = additive_inverse(add(X11,X12))]. % 159.97/160.39 [232=param(212,40),[], % 159.97/160.39 add(X10,additive_inverse(X11)) = additive_inverse(add(X11,additive_inverse(X10)))]. % 159.97/160.39 [235=param(212,169),[], % 159.97/160.39 add(additive_inverse(X10),additive_inverse(X11)) = additive_inverse(add(X10,X11))]. % 159.97/160.39 [244=param(35,235),[], % 159.97/160.39 add(X10,additive_inverse(add(X11,X12))) = add(additive_inverse(X11),add(X10,additive_inverse(X12)))]. % 159.97/160.39 [245=param(235,42),[], % 159.97/160.39 add(additive_inverse(X10),X11) = additive_inverse(add(X10,additive_inverse(X11)))]. % 159.97/160.39 [302=param(232,232),[7,245,42], % 159.97/160.39 add(X10,add(X11,additive_inverse(X12))) = additive_inverse(add(X12,additive_inverse(add(X11,X10))))]. % 159.97/160.39 [313=param(190,8),[141], % 159.97/160.39 multiply(additive_identity,add(X10,additive_inverse(multiply(b,X10)))) = additive_identity]. % 159.97/160.39 [339=param(105,51),[6,104,302,219,42], % 159.97/160.39 multiply(additive_identity,add(X10,additive_inverse(X11))) = multiply(additive_identity,X10)]. % 159.97/160.39 [340=demod(313),[339], % 159.97/160.39 multiply(additive_identity,X10) = additive_identity]. % 159.97/160.39 [346=param(184,20),[], % 159.97/160.39 add(X10,multiply(a,add(X11,b))) = add(multiply(a,X11),add(c,X10))]. % 159.97/160.39 [350=param(181,3),[3], % 159.97/160.39 add(X10,multiply(add(X11,X12),X13)) = add(X10,multiply(add(X12,X11),X13))]. % 159.97/160.39 [371=param(68,20),[], % 159.97/160.39 add(c,add(c,multiply(a,X10))) = multiply(a,add(X10,add(b,b)))]. % 159.97/160.39 [424=param(219,142),[13,6,10], % 159.97/160.39 multiply(X10,additive_inverse(multiply(X10,multiply(X10,X10)))) = additive_inverse(X10)]. % 159.97/160.39 [426=param(28,424),[424], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,additive_inverse(X10)))) = additive_inverse(X10)]. % 159.97/160.39 [434=param(426,42),[42], % 159.97/160.39 multiply(additive_inverse(X10),multiply(additive_inverse(X10),multiply(additive_inverse(X10),X10))) = X10]. % 159.97/160.39 [474=param(217,8),[340,13,6,10], % 159.97/160.39 additive_inverse(multiply(additive_inverse(X10),X11)) = multiply(X10,X11)]. % 159.97/160.39 [481=param(217,245),[474,3,-244,212], % 159.97/160.39 multiply(additive_inverse(X10),X11) = additive_inverse(multiply(X10,X11))]. % 159.97/160.39 [489=demod(434),[481,481,481], % 159.97/160.39 additive_inverse(multiply(X10,additive_inverse(multiply(X10,additive_inverse(multiply(X10,X10)))))) = X10]. % 159.97/160.39 [502=param(218,8),[141,13,6,10], % 159.97/160.39 additive_inverse(multiply(X10,additive_inverse(X11))) = multiply(X10,X11)]. % 159.97/160.39 [505=demod(489),[502,2], % 159.97/160.39 additive_inverse(X10) = X10]. % 159.97/160.39 [506=demod(51),[505], % 159.97/160.39 add(X10,add(X11,add(X12,X10))) = add(X11,X12)]. % 159.97/160.39 [507=demod(8),[505], % 159.97/160.39 add(X10,X10) = additive_identity]. % 159.97/160.39 [512=demod(371),[507,9], % 159.97/160.39 add(c,add(c,multiply(a,X10))) = multiply(a,X10)]. % 159.97/160.39 [513=demod(67),[512], % 159.97/160.39 add(c,multiply(a,add(X10,b))) = multiply(a,X10)]. % 159.97/160.39 [516=demod(228),[505,505], % 159.97/160.39 add(X10,add(X11,add(X10,X12))) = add(X11,X12)]. % 159.97/160.39 [517=demod(219),[505,505], % 159.97/160.39 add(X10,add(X11,X10)) = X11]. % 159.97/160.39 [518=demod(212),[505,505], % 159.97/160.39 add(X10,add(X10,X11)) = X11]. % 159.97/160.39 [526=param(518,144),[], % 159.97/160.39 add(multiply(c,X10),multiply(a,add(X11,multiply(b,X10)))) = multiply(a,X11)]. % 159.97/160.39 [551=param(3,5),[], % 159.97/160.39 add(multiply(X10,multiply(X11,X12)),multiply(X13,X12)) = multiply(add(multiply(X10,X11),X13),X12)]. % 159.97/160.39 [552=param(3,5),[], % 159.97/160.39 add(multiply(X10,X11),multiply(X12,multiply(X13,X11))) = multiply(add(X10,multiply(X12,X13)),X11)]. % 159.97/160.39 [554=param(7,3),[], % 159.97/160.39 add(multiply(add(X10,X11),X12),X13) = add(multiply(X10,X12),add(multiply(X11,X12),X13))]. % 159.97/160.39 [560=param(516,3),[], % 159.97/160.39 add(multiply(X10,X11),add(X12,multiply(add(X10,X13),X11))) = add(X12,multiply(X13,X11))]. % 159.97/160.39 [563=param(506,4),[], % 159.97/160.39 add(multiply(X10,X11),add(X12,multiply(X10,add(X13,X11)))) = add(X12,multiply(X10,X13))]. % 159.97/160.39 [566=param(35,4),[], % 159.97/160.39 add(X10,multiply(X11,add(X12,X13))) = add(multiply(X11,X12),add(X10,multiply(X11,X13)))]. % 159.97/160.39 [568=param(22,4),[], % 159.97/160.39 multiply(X10,multiply(X10,add(X11,multiply(X10,X10)))) = add(X10,multiply(X10,multiply(X10,X11)))]. % 159.97/160.39 [569=param(34,3),[], % 159.97/160.39 add(X10,multiply(add(X11,X12),X13)) = add(multiply(X12,X13),add(X10,multiply(X11,X13)))]. % 159.97/160.39 [570=param(34,4),[], % 159.97/160.39 add(X10,multiply(X11,add(X12,X13))) = add(multiply(X11,X13),add(X10,multiply(X11,X12)))]. % 159.97/160.39 [571=param(4,28),[4], % 159.97/160.39 multiply(X10,add(multiply(X10,multiply(X10,multiply(X10,X11))),X12)) = multiply(X10,add(X11,X12))]. % 159.97/160.39 [572=param(4,28),[4], % 159.97/160.39 multiply(X10,add(X11,multiply(X10,multiply(X10,multiply(X10,X12))))) = multiply(X10,add(X11,X12))]. % 159.97/160.39 [573=param(28,19),[19], % 159.97/160.39 multiply(a,multiply(a,multiply(a,add(c,multiply(a,X10))))) = add(c,multiply(a,X10))]. % 159.97/160.39 [574=param(28,21),[21], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,add(X10,multiply(X10,X11))))) = add(X10,multiply(X10,X11))]. % 159.97/160.39 [577=param(129,21),[21], % 159.97/160.39 multiply(a,multiply(a,multiply(a,add(c,multiply(c,X10))))) = add(c,multiply(c,X10))]. % 159.97/160.39 [580=param(4,57),[4], % 159.97/160.39 multiply(c,add(X10,multiply(b,multiply(b,multiply(b,X11))))) = multiply(c,add(X10,X11))]. % 159.97/160.39 [582=param(33,2),[6], % 159.97/160.39 add(c,multiply(a,X10)) = multiply(a,add(X10,multiply(b,multiply(c,multiply(c,c)))))]. % 159.97/160.39 [585=param(55,4),[], % 159.97/160.39 multiply(c,multiply(b,add(multiply(b,b),X10))) = add(c,multiply(c,multiply(b,X10)))]. % 159.97/160.39 [596=param(552,1),[], % 159.97/160.39 add(multiply(X10,b),multiply(X11,c)) = multiply(add(X10,multiply(X11,a)),b)]. % 159.97/160.39 [597=param(552,2),[6], % 159.97/160.39 add(X10,multiply(X11,multiply(X10,X10))) = multiply(add(X11,multiply(X10,X10)),multiply(X10,X10))]. % 159.97/160.39 [598=param(552,4),[], % 159.97/160.39 multiply(add(X10,multiply(X10,X11)),X12) = multiply(X10,add(X12,multiply(X11,X12)))]. % 159.97/160.39 [599=param(22,552),[], % 159.97/160.39 multiply(X10,multiply(add(X11,multiply(X10,X10)),X10)) = add(X10,multiply(X10,multiply(X11,X10)))]. % 159.97/160.39 [605=param(596,4),[6], % 159.97/160.39 multiply(add(X10,multiply(X10,a)),b) = multiply(X10,add(c,b))]. % 159.97/160.39 [606=param(596,6),[], % 159.97/160.39 multiply(add(X10,multiply(X11,a)),b) = add(multiply(X11,c),multiply(X10,b))]. % 159.97/160.39 [607=param(517,596),[], % 159.97/160.39 add(multiply(X10,c),multiply(add(X11,multiply(X10,a)),b)) = multiply(X11,b)]. % 159.97/160.39 [610=param(5,605),[5], % 159.97/160.39 multiply(X10,multiply(add(c,b),X11)) = multiply(add(X10,multiply(X10,a)),multiply(b,X11))]. % 159.97/160.39 [613=param(607,6),[], % 159.97/160.39 add(multiply(X10,c),multiply(add(multiply(X10,a),X11),b)) = multiply(X11,b)]. % 159.97/160.39 [614=param(613,518),[], % 159.97/160.39 multiply(add(multiply(X10,a),X11),b) = add(multiply(X10,c),multiply(X11,b))]. % 159.97/160.39 [616=param(551,2),[], % 159.97/160.39 multiply(add(multiply(X10,X10),X11),multiply(X10,X10)) = add(X10,multiply(X11,multiply(X10,X10)))]. % 159.97/160.39 [617=param(21,551),[], % 159.97/160.39 multiply(X10,multiply(add(multiply(X10,X10),X11),X10)) = add(X10,multiply(X10,multiply(X11,X10)))]. % 159.97/160.39 [621=param(132,551),[], % 159.97/160.39 multiply(a,multiply(add(multiply(a,a),X10),c)) = add(c,multiply(a,multiply(X10,c)))]. % 159.97/160.39 [622=param(621,66),[27], % 159.97/160.39 multiply(add(c,multiply(a,multiply(a,a))),c) = add(c,multiply(c,c))]. % 159.97/160.39 [627=param(617,66),[27], % 159.97/160.39 add(a,multiply(c,a)) = multiply(add(c,multiply(a,multiply(a,a))),a)]. % 159.97/160.39 [630=param(616,48),[27,5], % 159.97/160.39 add(b,multiply(c,b)) = multiply(add(c,multiply(b,multiply(b,b))),b)]. % 159.97/160.39 [641=param(571,518),[], % 159.97/160.39 multiply(X10,add(X12,add(multiply(X10,multiply(X10,multiply(X10,X12))),X11))) = multiply(X10,X11)]. % 159.97/160.39 [646=param(641,34),[], % 159.97/160.39 multiply(X10,add(X11,add(X12,multiply(X10,multiply(X10,multiply(X10,X12)))))) = multiply(X10,X11)]. % 159.97/160.39 [648=param(582,20),[], % 159.97/160.39 multiply(a,add(X10,multiply(b,multiply(c,multiply(c,c))))) = multiply(a,add(X10,b))]. % 159.97/160.39 [655=param(3,31),[], % 159.97/160.39 add(c,multiply(X10,multiply(b,multiply(b,b)))) = multiply(add(c,X10),multiply(b,multiply(b,b)))]. % 159.97/160.39 [657=param(5,2),[5,5], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X10,multiply(X11,multiply(X10,multiply(X11,multiply(X10,X11))))))) = multiply(X10,X11)]. % 159.97/160.39 [671=param(5,21),[], % 159.97/160.39 multiply(X10,multiply(add(multiply(X10,multiply(X10,X10)),X11),X12)) = multiply(add(X10,multiply(X10,X11)),X12)]. % 159.97/160.39 [675=param(184,627),[], % 159.97/160.39 add(X10,multiply(add(c,multiply(a,multiply(a,a))),a)) = add(multiply(c,a),add(a,X10))]. % 159.97/160.39 [676=param(184,630),[], % 159.97/160.39 add(X10,multiply(add(c,multiply(b,multiply(b,b))),b)) = add(multiply(c,b),add(b,X10))]. % 159.97/160.39 [678=param(16,22),[5,6], % 159.97/160.39 multiply(X10,multiply(add(X11,multiply(X10,multiply(X10,X10))),X12)) = multiply(add(X10,multiply(X10,X11)),X12)]. % 159.97/160.39 [681=param(516,22),[], % 159.97/160.39 add(X10,add(X11,multiply(X10,add(X12,multiply(X10,multiply(X10,X10)))))) = add(X11,multiply(X10,X12))]. % 159.97/160.39 [683=param(35,22),[], % 159.97/160.39 add(X10,multiply(X11,add(X12,multiply(X11,multiply(X11,X11))))) = add(X11,add(X10,multiply(X11,X12)))]. % 159.97/160.39 [694=param(614,34),[], % 159.97/160.39 multiply(add(X10,add(multiply(X11,a),X12)),b) = add(multiply(X11,c),multiply(add(X12,X10),b))]. % 159.97/160.39 [699=param(614,516),[], % 159.97/160.39 add(multiply(X12,c),multiply(add(X10,add(multiply(X12,a),X11)),b)) = multiply(add(X10,X11),b)]. % 159.97/160.39 [727=param(5,32),[], % 159.97/160.39 multiply(a,multiply(add(multiply(b,X10),X11),X12)) = multiply(add(multiply(c,X10),multiply(a,X11)),X12)]. % 159.97/160.39 [734=param(3,622),[7,3,7], % 159.97/160.39 multiply(add(c,add(multiply(a,multiply(a,a)),X10)),c) = add(c,multiply(add(c,X10),c))]. % 159.97/160.39 [780=param(55,3),[], % 159.97/160.39 multiply(c,multiply(add(b,X10),multiply(b,b))) = add(c,multiply(c,multiply(X10,multiply(b,b))))]. % 159.97/160.39 [782=param(5,55),[], % 159.97/160.39 multiply(c,multiply(add(multiply(b,multiply(b,b)),X10),X11)) = multiply(add(c,multiply(c,X10)),X11)]. % 159.97/160.39 [812=param(3,605),[], % 159.97/160.39 add(multiply(X10,b),multiply(X11,add(c,b))) = multiply(add(X10,add(X11,multiply(X11,a))),b)]. % 159.97/160.39 [813=param(605,7),[], % 159.97/160.39 multiply(add(X10,add(X11,multiply(add(X10,X11),a))),b) = multiply(add(X10,X11),add(c,b))]. % 159.97/160.39 [913=param(585,4),[], % 159.97/160.39 multiply(c,multiply(b,multiply(b,add(b,X10)))) = add(c,multiply(c,multiply(b,multiply(b,X10))))]. % 159.97/160.39 [944=param(913,6),[], % 159.97/160.39 multiply(c,multiply(b,multiply(b,add(X10,b)))) = add(c,multiply(c,multiply(b,multiply(b,X10))))]. % 159.97/160.39 [945=param(913,517),[], % 159.97/160.39 add(c,multiply(c,multiply(b,multiply(b,add(X10,b))))) = multiply(c,multiply(b,multiply(b,X10)))]. % 159.97/160.39 [999=param(780,517),[], % 159.97/160.39 add(c,multiply(c,multiply(add(X10,b),multiply(b,b)))) = multiply(c,multiply(X10,multiply(b,b)))]. % 159.97/160.39 [1065=param(655,2),[], % 159.97/160.39 multiply(add(c,b),multiply(b,multiply(b,b))) = add(c,b)]. % 159.97/160.39 [1075=param(5,1065),[5,5], % 159.97/160.39 multiply(add(c,b),multiply(b,multiply(b,multiply(b,X10)))) = multiply(add(c,b),X10)]. % 159.97/160.39 [1163=param(572,4),[], % 159.97/160.39 multiply(X10,add(multiply(X10,X11),X12)) = multiply(X10,multiply(X10,add(X11,multiply(X10,multiply(X10,X12)))))]. % 159.97/160.39 [1246=param(734,346),[6,19,516,518], % 159.97/160.39 multiply(add(X10,multiply(a,multiply(a,a))),c) = add(c,multiply(X10,c))]. % 159.97/160.39 [1247=param(734,506),[517], % 159.97/160.39 multiply(add(multiply(a,multiply(a,a)),X10),c) = add(c,multiply(X10,c))]. % 159.97/160.39 [1266=param(599,727),[5,27], % 159.97/160.39 multiply(add(multiply(c,X10),multiply(a,multiply(a,a))),a) = add(a,multiply(c,multiply(X10,a)))]. % 159.97/160.39 [1268=param(782,1246),[5,5,580,507,141], % 159.97/160.39 multiply(add(c,multiply(c,multiply(a,multiply(a,a)))),c) = additive_identity]. % 159.97/160.39 [1274=param(3,1268),[10,7], % 159.97/160.39 multiply(add(c,add(multiply(c,multiply(a,multiply(a,a))),X10)),c) = multiply(X10,c)]. % 159.97/160.39 [1275=param(3,1268),[6,10], % 159.97/160.39 multiply(add(X10,add(c,multiply(c,multiply(a,multiply(a,a))))),c) = multiply(X10,c)]. % 159.97/160.39 [1288=param(1275,569),[5,5,5,128], % 159.97/160.39 multiply(add(c,multiply(add(c,X10),multiply(a,multiply(a,a)))),c) = multiply(X10,c)]. % 159.97/160.39 [1290=param(3,1288),[3,7,554,1274], % 159.97/160.39 multiply(add(multiply(X10,multiply(a,multiply(a,a))),X11),c) = multiply(add(X10,X11),c)]. % 159.97/160.39 [1305=param(671,1266),[5,572,507,141], % 159.97/160.39 multiply(add(c,multiply(c,multiply(a,multiply(a,a)))),a) = additive_identity]. % 159.97/160.39 [1308=param(5,1305),[340], % 159.97/160.39 multiply(add(c,multiply(c,multiply(a,multiply(a,a)))),multiply(a,X10)) = additive_identity]. % 159.97/160.39 [1360=param(657,27),[27,27], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(c,a)))) = multiply(b,a)]. % 159.97/160.39 [1364=param(657,1308),[141], % 159.97/160.39 multiply(a,add(c,multiply(c,multiply(a,multiply(a,a))))) = additive_identity]. % 159.97/160.39 [1365=param(4,1360),[4], % 159.97/160.39 multiply(b,add(multiply(c,multiply(c,multiply(c,a))),X10)) = multiply(b,add(a,X10))]. % 159.97/160.39 [1367=param(5,1360),[5,5,5,5], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(c,multiply(a,X10))))) = multiply(b,multiply(a,X10))]. % 159.97/160.39 [1377=param(577,1364),[141,141], % 159.97/160.39 add(c,multiply(c,multiply(a,multiply(a,a)))) = additive_identity]. % 159.97/160.39 [1386=param(184,1377),[9], % 159.97/160.39 add(multiply(c,multiply(a,multiply(a,a))),add(c,X10)) = X10]. % 159.97/160.39 [1396=param(1386,516),[], % 159.97/160.39 add(multiply(c,multiply(a,multiply(a,a))),X10) = add(c,X10)]. % 159.97/160.39 [1402=param(1396,9),[9], % 159.97/160.39 multiply(c,multiply(a,multiply(a,a))) = c]. % 159.97/160.39 [1404=param(5,1402),[5,5], % 159.97/160.39 multiply(c,multiply(a,multiply(a,multiply(a,X10)))) = multiply(c,X10)]. % 159.97/160.39 [1420=param(1404,1),[], % 159.97/160.39 multiply(c,multiply(a,multiply(a,c))) = multiply(c,b)]. % 159.97/160.39 [1425=param(1404,27),[], % 159.97/160.39 multiply(c,multiply(a,multiply(a,multiply(c,X10)))) = multiply(c,multiply(b,X10))]. % 159.97/160.39 [1448=param(33,1420),[33], % 159.97/160.39 multiply(a,add(X10,multiply(b,multiply(a,multiply(a,c))))) = multiply(a,add(X10,multiply(b,b)))]. % 159.97/160.39 [1459=param(1425,2),[1420], % 159.97/160.39 multiply(c,multiply(b,multiply(c,multiply(c,c)))) = multiply(c,b)]. % 159.97/160.39 [1460=param(1425,28),[1425], % 159.97/160.39 multiply(c,multiply(b,multiply(c,multiply(c,multiply(c,X10))))) = multiply(c,multiply(b,X10))]. % 159.97/160.39 [1489=param(675,560),[3,34,6,518], % 159.97/160.39 multiply(add(multiply(a,multiply(a,a)),X10),a) = add(a,multiply(X10,a))]. % 159.97/160.39 [1500=param(1489,517),[], % 159.97/160.39 add(a,multiply(add(X10,multiply(a,multiply(a,a))),a)) = multiply(X10,a)]. % 159.97/160.39 [1504=param(676,560),[3,34,6,518], % 159.97/160.39 multiply(add(multiply(b,multiply(b,b)),X10),b) = add(b,multiply(X10,b))]. % 159.97/160.39 [1506=param(5,1504),[], % 159.97/160.39 multiply(add(multiply(b,multiply(b,b)),X10),multiply(b,X11)) = multiply(add(b,multiply(X10,b)),X11)]. % 159.97/160.39 [1519=param(1504,517),[], % 159.97/160.39 add(b,multiply(add(X10,multiply(b,multiply(b,b))),b)) = multiply(X10,b)]. % 159.97/160.39 [1526=param(678,1504),[5,5,572,507,141], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(b,multiply(b,b)))),b) = additive_identity]. % 159.97/160.39 [1528=param(3,1526),[6,10], % 159.97/160.39 multiply(add(X10,add(X11,multiply(X11,multiply(b,multiply(b,b))))),b) = multiply(X10,b)]. % 159.97/160.39 [1529=param(5,1526),[340], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(b,multiply(b,b)))),multiply(b,X11)) = additive_identity]. % 159.97/160.39 [1536=param(657,1529),[141], % 159.97/160.39 multiply(b,add(X10,multiply(X10,multiply(b,multiply(b,b))))) = additive_identity]. % 159.97/160.39 [1537=param(1529,678),[1506,5,5], % 159.97/160.39 multiply(X10,multiply(add(b,multiply(X10,multiply(X10,multiply(X10,b)))),X11)) = additive_identity]. % 159.97/160.39 [1539=param(4,1536),[6,10], % 159.97/160.39 multiply(b,add(X10,add(X11,multiply(X11,multiply(b,multiply(b,b)))))) = multiply(b,X10)]. % 159.97/160.39 [1541=param(27,1536),[141], % 159.97/160.39 multiply(c,add(X10,multiply(X10,multiply(b,multiply(b,b))))) = additive_identity]. % 159.97/160.39 [1546=param(563,1536),[9], % 159.97/160.39 add(multiply(b,multiply(X10,multiply(b,multiply(b,b)))),X11) = add(X11,multiply(b,X10))]. % 159.97/160.39 [1552=param(1075,1536),[141,141,141], % 159.97/160.39 multiply(add(c,b),add(X10,multiply(X10,multiply(b,multiply(b,b))))) = additive_identity]. % 159.97/160.39 [1554=param(4,1541),[6,10], % 159.97/160.39 multiply(c,add(X10,add(X11,multiply(X11,multiply(b,multiply(b,b)))))) = multiply(c,X10)]. % 159.97/160.39 [1555=param(5,1541),[340], % 159.97/160.39 multiply(c,multiply(add(X10,multiply(X10,multiply(b,multiply(b,b)))),X11)) = additive_identity]. % 159.97/160.39 [1592=param(657,1555),[141], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(b,multiply(b,b)))),c) = additive_identity]. % 159.97/160.39 [1603=param(5,1592),[340], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(b,multiply(b,b)))),multiply(c,X11)) = additive_identity]. % 159.97/160.39 [1611=param(1592,598),[5,5], % 159.97/160.39 multiply(X10,add(c,multiply(b,multiply(b,multiply(b,c))))) = additive_identity]. % 159.97/160.39 [1614=param(1592,1290),[5,5,5,27], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(a,multiply(a,multiply(c,multiply(b,b)))))),c) = additive_identity]. % 159.97/160.39 [1617=param(5,1611),[340], % 159.97/160.39 multiply(X10,multiply(add(c,multiply(b,multiply(b,multiply(b,c)))),X11)) = additive_identity]. % 159.97/160.39 [1620=param(526,1611),[6,10], % 159.97/160.39 multiply(a,c) = multiply(c,multiply(b,multiply(b,c)))]. % 159.97/160.39 [1635=demod(1448),[1620], % 159.97/160.39 multiply(a,add(X10,multiply(b,multiply(a,multiply(c,multiply(b,multiply(b,c))))))) = multiply(a,add(X10,multiply(b,b)))]. % 159.97/160.39 [1676=param(5,1620),[5,5,5], % 159.97/160.39 multiply(a,multiply(c,X10)) = multiply(c,multiply(b,multiply(b,multiply(c,X10))))]. % 159.97/160.39 [1707=demod(1635),[1676], % 159.97/160.39 multiply(a,add(X10,multiply(b,multiply(c,multiply(b,multiply(b,multiply(c,multiply(b,multiply(b,c))))))))) = multiply(a,add(X10,multiply(b,b)))]. % 159.97/160.39 [1719=demod(1614),[1676,1676], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(c,multiply(b,multiply(b,multiply(c,multiply(b,multiply(b,multiply(c,multiply(b,b)))))))))),c) = additive_identity]. % 159.97/160.39 [1721=param(20,1620),[-944], % 159.97/160.39 multiply(a,add(c,b)) = multiply(c,multiply(b,multiply(b,add(c,b))))]. % 159.97/160.39 [1750=param(694,4),[6], % 159.97/160.39 multiply(add(X10,add(X11,multiply(add(X11,X10),a))),b) = multiply(add(X11,X10),add(c,b))]. % 159.97/160.39 [1751=param(1617,2),[], % 159.97/160.39 add(c,multiply(b,multiply(b,multiply(b,c)))) = additive_identity]. % 159.97/160.39 [1755=param(184,1751),[9], % 159.97/160.39 add(multiply(b,multiply(b,multiply(b,c))),add(c,X10)) = X10]. % 159.97/160.39 [1765=param(1755,516),[], % 159.97/160.39 add(multiply(b,multiply(b,multiply(b,c))),X10) = add(c,X10)]. % 159.97/160.39 [1768=param(1765,3),[], % 159.97/160.39 multiply(add(b,X10),multiply(b,multiply(b,c))) = add(c,multiply(X10,multiply(b,multiply(b,c))))]. % 159.97/160.39 [1769=param(1765,4),[1163,4], % 159.97/160.39 multiply(b,multiply(b,multiply(b,add(c,multiply(b,X10))))) = add(c,multiply(b,X10))]. % 159.97/160.39 [1770=param(1765,9),[9], % 159.97/160.39 multiply(b,multiply(b,multiply(b,c))) = c]. % 159.97/160.39 [1772=param(4,1770),[6], % 159.97/160.39 add(c,multiply(b,X10)) = multiply(b,add(X10,multiply(b,multiply(b,c))))]. % 159.97/160.39 [1773=param(5,1770),[5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(c,X10)))) = multiply(c,X10)]. % 159.97/160.39 [1774=param(22,1770),[6,4,4], % 159.97/160.39 multiply(b,multiply(b,multiply(b,add(c,b)))) = add(c,b)]. % 159.97/160.39 [1791=param(4,1773),[], % 159.97/160.39 add(multiply(b,X10),multiply(c,X11)) = multiply(b,add(X10,multiply(b,multiply(b,multiply(c,X11)))))]. % 159.97/160.39 [1796=param(1773,657),[1770], % 159.97/160.39 multiply(c,multiply(b,multiply(c,multiply(b,multiply(c,multiply(b,c)))))) = c]. % 159.97/160.39 [1797=param(1773,1360),[], % 159.97/160.39 multiply(b,multiply(b,multiply(b,a))) = multiply(c,multiply(c,multiply(c,a)))]. % 159.97/160.39 [1804=param(1791,606),[], % 159.97/160.39 multiply(b,add(c,multiply(b,multiply(b,multiply(c,b))))) = multiply(add(c,multiply(b,a)),b)]. % 159.97/160.39 [1847=param(1768,1519),[5,1770,5,1770], % 159.97/160.39 add(c,multiply(add(X10,multiply(b,multiply(b,b))),c)) = multiply(X10,c)]. % 159.97/160.39 [1851=param(518,1847),[], % 159.97/160.39 add(c,multiply(X10,c)) = multiply(add(X10,multiply(b,multiply(b,b))),c)]. % 159.97/160.39 [1867=param(1603,678),[], % 159.97/160.39 multiply(X10,multiply(add(multiply(b,multiply(b,b)),multiply(X10,multiply(X10,X10))),multiply(c,X11))) = additive_identity]. % 159.97/160.39 [1883=param(1552,27),[], % 159.97/160.39 multiply(add(c,b),add(a,multiply(c,multiply(b,b)))) = additive_identity]. % 159.97/160.39 [1887=param(5,1883),[340], % 159.97/160.39 multiply(add(c,b),multiply(add(a,multiply(c,multiply(b,b))),X10)) = additive_identity]. % 159.97/160.39 [1891=param(657,1887),[141], % 159.97/160.39 multiply(add(a,multiply(c,multiply(b,b))),add(c,b)) = additive_identity]. % 159.97/160.39 [1894=param(5,1891),[340], % 159.97/160.39 multiply(add(a,multiply(c,multiply(b,b))),multiply(add(c,b),X10)) = additive_identity]. % 159.97/160.39 [1896=param(1894,610),[22,5,29,5,5,14,5,5,31,507,141,141,9], % 159.97/160.39 multiply(add(a,multiply(c,multiply(b,b))),multiply(c,X10)) = additive_identity]. % 159.97/160.39 [1904=param(657,1896),[141], % 159.97/160.39 multiply(c,add(a,multiply(c,multiply(b,b)))) = additive_identity]. % 159.97/160.39 [1907=param(4,1904),[6,10], % 159.97/160.39 multiply(c,add(X10,add(a,multiply(c,multiply(b,b))))) = multiply(c,X10)]. % 159.97/160.39 [1927=param(1907,517),[], % 159.97/160.39 multiply(c,multiply(c,multiply(b,b))) = multiply(c,a)]. % 159.97/160.39 [1934=param(5,1927),[5,5,5], % 159.97/160.39 multiply(c,multiply(a,X10)) = multiply(c,multiply(c,multiply(b,multiply(b,X10))))]. % 159.97/160.39 [1947=demod(1367),[1934,28], % 159.97/160.39 multiply(b,multiply(a,X10)) = multiply(b,multiply(c,multiply(b,multiply(b,X10))))]. % 159.97/160.39 [1976=param(28,1927),[], % 159.97/160.39 multiply(c,multiply(b,b)) = multiply(c,multiply(c,multiply(c,a)))]. % 159.97/160.39 [2010=demod(1719),[1976,1360], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(c,multiply(b,multiply(b,multiply(c,multiply(b,multiply(b,a)))))))),c) = additive_identity]. % 159.97/160.39 [2022=param(551,1976),[], % 159.97/160.39 add(multiply(c,multiply(c,multiply(c,a))),multiply(X10,b)) = multiply(add(multiply(c,b),X10),b)]. % 159.97/160.39 [2095=param(657,1537),[141], % 159.97/160.39 multiply(add(b,multiply(X10,multiply(X10,multiply(X10,b)))),X10) = additive_identity]. % 159.97/160.39 [2099=param(3,2095),[6,10], % 159.97/160.39 multiply(add(X10,add(b,multiply(X11,multiply(X11,multiply(X11,b))))),X11) = multiply(X10,X11)]. % 159.97/160.39 [2150=param(560,1851),[-1546,5,2,3,516], % 159.97/160.39 multiply(add(multiply(b,multiply(b,b)),X10),c) = add(c,multiply(X10,c))]. % 159.97/160.39 [2152=param(1851,1246),[], % 159.97/160.39 multiply(add(X10,multiply(a,multiply(a,a))),c) = multiply(add(X10,multiply(b,multiply(b,b))),c)]. % 159.97/160.39 [2154=param(5,2150),[], % 159.97/160.39 multiply(add(multiply(b,multiply(b,b)),X10),multiply(c,X11)) = multiply(add(c,multiply(X10,c)),X11)]. % 159.97/160.39 [2155=demod(1867),[2154,5,5], % 159.97/160.39 multiply(X10,multiply(add(c,multiply(X10,multiply(X10,multiply(X10,c)))),X11)) = additive_identity]. % 159.97/160.39 [2160=param(657,2155),[141], % 159.97/160.39 multiply(add(c,multiply(X10,multiply(X10,multiply(X10,c)))),X10) = additive_identity]. % 159.97/160.39 [2163=param(3,2160),[6,10], % 159.97/160.39 multiply(add(X10,add(c,multiply(X11,multiply(X11,multiply(X11,c))))),X11) = multiply(X10,X11)]. % 159.97/160.39 [2171=param(597,2160),[9,5,5,28,5,6,-566], % 159.97/160.39 multiply(add(c,multiply(X10,add(X10,multiply(X10,multiply(X10,c))))),multiply(X10,X10)) = X10]. % 159.97/160.39 [2180=param(178,1772),[6,518], % 159.97/160.39 add(c,multiply(b,add(X10,multiply(b,multiply(b,c))))) = multiply(b,X10)]. % 159.97/160.39 [2190=param(2180,552),[], % 159.97/160.39 add(c,multiply(b,multiply(add(X10,multiply(b,b)),c))) = multiply(b,multiply(X10,c))]. % 159.97/160.39 [2193=param(2190,6),[], % 159.97/160.39 add(c,multiply(b,multiply(add(multiply(b,b),X10),c))) = multiply(b,multiply(X10,c))]. % 159.97/160.39 [2195=param(2193,518),[], % 159.97/160.39 multiply(b,multiply(add(multiply(b,b),X10),c)) = add(c,multiply(b,multiply(X10,c)))]. % 159.97/160.39 [2196=param(2195,4),[5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(add(b,X10),c))) = add(c,multiply(b,multiply(b,multiply(X10,c))))]. % 159.97/160.39 [2208=param(2163,178),[6,518,5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(c,X10)))) = multiply(c,X10)]. % 159.97/160.39 [2209=param(2163,566),[5], % 159.97/160.39 multiply(add(c,multiply(X10,add(X11,multiply(X10,multiply(X10,c))))),X10) = multiply(X10,multiply(X11,X10))]. % 159.97/160.39 [2212=param(5,2208),[5,5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(c,multiply(X10,X11))))) = multiply(c,multiply(X10,X11))]. % 159.97/160.39 [2246=param(2212,2208),[2208], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(c,multiply(c,X10))))) = multiply(c,multiply(c,X10))]. % 159.97/160.39 [2264=param(2099,517),[5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(b,X10)))) = multiply(b,X10)]. % 159.97/160.39 [2268=param(5,2264),[5,5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(b,multiply(X10,X11))))) = multiply(b,multiply(X10,X11))]. % 159.97/160.39 [2270=param(2264,27),[1676,1676], % 159.97/160.39 multiply(c,multiply(b,multiply(b,multiply(c,multiply(b,multiply(b,multiply(c,a))))))) = multiply(b,a)]. % 159.97/160.39 [2322=param(2268,1360),[1360], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(b,a)))) = multiply(b,a)]. % 159.97/160.39 [2323=param(2268,1459),[], % 159.97/160.39 multiply(b,multiply(c,multiply(c,c))) = multiply(c,multiply(c,multiply(c,b)))]. % 159.97/160.39 [2328=demod(648),[2323], % 159.97/160.39 multiply(a,add(X10,multiply(c,multiply(c,multiply(c,b))))) = multiply(a,add(X10,b))]. % 159.97/160.39 [2329=param(2268,1460),[], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(c,X10)))) = multiply(c,multiply(c,multiply(c,multiply(b,X10))))]. % 159.97/160.39 [2333=param(2268,1796),[], % 159.97/160.39 multiply(b,multiply(c,multiply(b,multiply(c,multiply(b,c))))) = multiply(c,multiply(c,c))]. % 159.97/160.39 [2336=param(2268,2264),[2264], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(b,multiply(b,X10))))) = multiply(b,multiply(b,X10))]. % 159.97/160.39 [2341=param(1773,2323),[2329,1976,28], % 159.97/160.39 multiply(b,multiply(c,multiply(c,a))) = multiply(c,multiply(c,c))]. % 159.97/160.39 [2344=param(22,2322),[4,4,6], % 159.97/160.39 multiply(c,multiply(c,multiply(c,add(c,multiply(b,a))))) = add(c,multiply(b,a))]. % 159.97/160.39 [2346=param(2268,2322),[2322], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(b,multiply(b,a))))) = multiply(b,multiply(b,a))]. % 159.97/160.39 [2380=param(813,350),[], % 159.97/160.39 multiply(add(X10,add(X11,multiply(add(X11,X10),a))),b) = multiply(add(X10,X11),add(c,b))]. % 159.97/160.39 [2384=param(1773,2333),[2323,2329,1976,28], % 159.97/160.39 multiply(c,multiply(b,multiply(c,multiply(b,c)))) = multiply(c,multiply(c,a))]. % 159.97/160.39 [2386=param(2268,2384),[28], % 159.97/160.39 multiply(b,multiply(c,multiply(b,c))) = multiply(c,a)]. % 159.97/160.39 [2387=param(4,2386),[], % 159.97/160.39 multiply(b,add(multiply(c,multiply(b,c)),X10)) = add(multiply(c,a),multiply(b,X10))]. % 159.97/160.39 [2388=param(5,2386),[5,1934,5,5], % 159.97/160.39 multiply(b,multiply(c,multiply(b,multiply(c,X10)))) = multiply(c,multiply(c,multiply(b,multiply(b,X10))))]. % 159.97/160.39 [2389=param(27,2386),[1676], % 159.97/160.39 multiply(c,multiply(b,multiply(b,multiply(c,a)))) = multiply(c,multiply(c,multiply(b,c)))]. % 159.97/160.39 [2390=demod(2270),[2389], % 159.97/160.39 multiply(c,multiply(b,multiply(b,multiply(c,multiply(c,multiply(b,c)))))) = multiply(b,a)]. % 159.97/160.39 [2408=param(1773,2386),[], % 159.97/160.39 multiply(b,multiply(b,multiply(c,a))) = multiply(c,multiply(b,c))]. % 159.97/160.39 [2412=param(2387,6),[], % 159.97/160.39 multiply(b,add(X10,multiply(c,multiply(b,c)))) = add(multiply(c,a),multiply(b,X10))]. % 159.97/160.39 [2424=param(2388,1976),[2329,2322,2], % 159.97/160.39 multiply(b,multiply(c,multiply(b,a))) = multiply(c,multiply(c,b))]. % 159.97/160.39 [2425=param(2388,2264),[2390], % 159.97/160.39 multiply(b,multiply(c,multiply(b,multiply(b,c)))) = multiply(c,multiply(b,a))]. % 159.97/160.39 [2431=demod(1707),[2425,2424,2329,1976,28], % 159.97/160.39 multiply(a,add(X10,multiply(b,b))) = multiply(a,add(X10,multiply(c,multiply(c,a))))]. % 159.97/160.39 [2446=param(4,2424),[], % 159.97/160.39 multiply(b,add(multiply(c,multiply(b,a)),X10)) = add(multiply(c,multiply(c,b)),multiply(b,X10))]. % 159.97/160.39 [2457=param(2431,6),[32], % 159.97/160.39 add(multiply(c,b),multiply(a,X10)) = multiply(a,add(X10,multiply(c,multiply(c,a))))]. % 159.97/160.39 [2464=param(1773,2425),[2424], % 159.97/160.39 multiply(c,multiply(b,multiply(b,c))) = multiply(b,multiply(c,multiply(c,b)))]. % 159.97/160.39 [2488=demod(1620),[2464], % 159.97/160.39 multiply(a,c) = multiply(b,multiply(c,multiply(c,b)))]. % 159.97/160.39 [2490=param(5,2488),[5,5,5,1676], % 159.97/160.39 multiply(c,multiply(b,multiply(b,multiply(c,X10)))) = multiply(b,multiply(c,multiply(c,multiply(b,X10))))]. % 159.97/160.39 [2493=demod(1676),[2490], % 159.97/160.39 multiply(a,multiply(c,X10)) = multiply(b,multiply(c,multiply(c,multiply(b,X10))))]. % 159.97/160.39 [2507=demod(2010),[2490,1797,28,2341], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(c,multiply(c,c)))),c) = additive_identity]. % 159.97/160.39 [2516=param(2336,2464),[], % 159.97/160.39 multiply(b,multiply(b,c)) = multiply(c,multiply(c,multiply(b,multiply(c,multiply(c,b)))))]. % 159.97/160.39 [2536=demod(1772),[2516], % 159.97/160.39 add(c,multiply(b,X10)) = multiply(b,add(X10,multiply(c,multiply(c,multiply(b,multiply(c,multiply(c,b)))))))]. % 159.97/160.39 [2538=demod(1770),[2516], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(b,multiply(c,multiply(c,b)))))) = c]. % 159.97/160.39 [2541=param(3,2507),[6,10], % 159.97/160.39 multiply(add(X10,add(X11,multiply(X11,multiply(c,multiply(c,c))))),c) = multiply(X10,c)]. % 159.97/160.39 [2542=param(5,2507),[340], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(c,multiply(c,c)))),multiply(c,X11)) = additive_identity]. % 159.97/160.39 [2557=param(657,2542),[141], % 159.97/160.39 multiply(c,add(X10,multiply(X10,multiply(c,multiply(c,c))))) = additive_identity]. % 159.97/160.39 [2567=param(4,2557),[6,10], % 159.97/160.39 multiply(c,add(X10,add(X11,multiply(X11,multiply(c,multiply(c,c)))))) = multiply(c,X10)]. % 159.97/160.39 [2626=param(2388,2538),[2388,2490,1976,28,2388,2346], % 159.97/160.39 multiply(c,multiply(b,multiply(b,a))) = multiply(b,multiply(c,c))]. % 159.97/160.39 [2627=demod(2346),[2626], % 159.97/160.39 multiply(b,multiply(b,a)) = multiply(c,multiply(c,multiply(b,multiply(c,c))))]. % 159.97/160.39 [2634=demod(1797),[2627], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(b,multiply(c,c))))) = multiply(c,multiply(c,multiply(c,a)))]. % 159.97/160.39 [2641=param(2490,2341),[2323,28], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(b,multiply(c,a))))) = multiply(c,b)]. % 159.97/160.39 [2642=param(2490,2408),[], % 159.97/160.39 multiply(b,multiply(c,multiply(c,multiply(b,a)))) = multiply(c,multiply(c,multiply(b,c)))]. % 159.97/160.39 [2644=param(1773,2641),[], % 159.97/160.39 multiply(b,multiply(b,multiply(c,b))) = multiply(c,multiply(c,multiply(b,multiply(c,a))))]. % 159.97/160.39 [2645=demod(1804),[2644], % 159.97/160.39 multiply(b,add(c,multiply(c,multiply(c,multiply(b,multiply(c,a)))))) = multiply(add(c,multiply(b,a)),b)]. % 159.97/160.39 [2647=param(2490,2641),[2388,2627,2268,2268], % 159.97/160.39 multiply(b,multiply(b,multiply(c,c))) = multiply(c,multiply(b,multiply(c,b)))]. % 159.97/160.39 [2648=param(5,2647),[5,5,5,5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(c,multiply(c,X10)))) = multiply(c,multiply(b,multiply(c,multiply(b,X10))))]. % 159.97/160.39 [2656=param(2446,6),[], % 159.97/160.39 multiply(b,add(X10,multiply(c,multiply(b,a)))) = add(multiply(c,multiply(c,b)),multiply(b,X10))]. % 159.97/160.39 [2661=param(120,2328),[513], % 159.97/160.39 add(c,multiply(a,add(multiply(c,multiply(c,multiply(c,b))),X10))) = multiply(a,X10)]. % 159.97/160.39 [2663=param(518,2661),[], % 159.97/160.39 multiply(a,add(multiply(c,multiply(c,multiply(c,b))),X10)) = add(c,multiply(a,X10))]. % 159.97/160.39 [2666=param(2567,517),[], % 159.97/160.39 multiply(c,multiply(X10,multiply(c,multiply(c,c)))) = multiply(c,X10)]. % 159.97/160.39 [2674=param(5,2666),[5,5,5,5], % 159.97/160.39 multiply(c,multiply(X10,multiply(c,multiply(c,multiply(c,X11))))) = multiply(c,multiply(X10,X11))]. % 159.97/160.39 [2676=param(2666,671),[1163,4,574], % 159.97/160.39 multiply(add(c,multiply(c,X10)),multiply(c,multiply(c,c))) = add(c,multiply(c,X10))]. % 159.97/160.39 [2677=param(2676,999),[5,5,5,2323,2329,1976,28,999], % 159.97/160.39 multiply(c,multiply(X10,multiply(b,b))) = multiply(c,multiply(X10,multiply(c,multiply(c,a))))]. % 159.97/160.39 [2698=param(2674,57),[2674], % 159.97/160.39 multiply(c,multiply(X10,multiply(b,multiply(b,multiply(b,X11))))) = multiply(c,multiply(X10,X11))]. % 159.97/160.39 [2727=param(2541,35),[], % 159.97/160.39 multiply(add(X10,add(X11,multiply(X10,multiply(c,multiply(c,c))))),c) = multiply(X11,c)]. % 159.97/160.39 [2751=param(2727,1247),[5,5,2493,2634,2493,2341,2,27], % 159.97/160.39 add(c,multiply(add(X10,multiply(c,multiply(c,c))),c)) = multiply(X10,c)]. % 159.97/160.39 [2757=param(518,2751),[], % 159.97/160.39 add(c,multiply(X10,c)) = multiply(add(X10,multiply(c,multiply(c,c))),c)]. % 159.97/160.39 [2773=param(2757,1851),[], % 159.97/160.39 multiply(add(X10,multiply(b,multiply(b,b))),c) = multiply(add(X10,multiply(c,multiply(c,c))),c)]. % 159.97/160.39 [2774=demod(2152),[2773], % 159.97/160.39 multiply(add(X10,multiply(a,multiply(a,a))),c) = multiply(add(X10,multiply(c,multiply(c,c))),c)]. % 159.97/160.39 [2832=param(1365,2022),[], % 159.97/160.39 multiply(b,multiply(add(multiply(c,b),X10),b)) = multiply(b,add(a,multiply(X10,b)))]. % 159.97/160.39 [2833=param(2832,3),[5,5], % 159.97/160.39 multiply(b,add(a,multiply(X10,multiply(b,b)))) = multiply(b,multiply(add(c,X10),multiply(b,b)))]. % 159.97/160.39 [2851=param(2833,22),[], % 159.97/160.39 add(b,multiply(b,a)) = multiply(b,multiply(add(c,b),multiply(b,b)))]. % 159.97/160.39 [2854=param(681,2833),[], % 159.97/160.39 add(b,add(X10,multiply(b,multiply(add(c,b),multiply(b,b))))) = add(X10,multiply(b,a))]. % 159.97/160.39 [2855=param(683,2833),[], % 159.97/160.39 add(X10,multiply(b,multiply(add(c,b),multiply(b,b)))) = add(b,add(X10,multiply(b,a)))]. % 159.97/160.39 [2871=param(1554,517),[], % 159.97/160.39 multiply(c,multiply(X10,multiply(b,multiply(b,b)))) = multiply(c,X10)]. % 159.97/160.39 [2879=param(2871,29),[2677], % 159.97/160.39 multiply(c,add(a,X10)) = multiply(c,multiply(add(c,multiply(X10,b)),multiply(c,multiply(c,a))))]. % 159.97/160.39 [2891=param(1539,517),[], % 159.97/160.39 multiply(b,multiply(X10,multiply(b,multiply(b,b)))) = multiply(b,X10)]. % 159.97/160.39 [2901=param(2891,29),[], % 159.97/160.39 multiply(b,add(a,X10)) = multiply(b,multiply(add(c,multiply(X10,b)),multiply(b,b)))]. % 159.97/160.39 [2916=param(2901,1500),[5,1,2774,2751,5,1976], % 159.97/160.39 multiply(b,multiply(X10,multiply(c,multiply(c,multiply(c,a))))) = multiply(b,multiply(X10,a))]. % 159.97/160.39 [2922=param(5,2916),[5,5,5,5,5,5,1934,28], % 159.97/160.39 multiply(b,multiply(X10,multiply(a,X11))) = multiply(b,multiply(X10,multiply(c,multiply(b,multiply(b,X11)))))]. % 159.97/160.39 [2962=param(1528,569),[5,5,5,2], % 159.97/160.39 multiply(add(X10,multiply(add(X10,X11),multiply(b,multiply(b,b)))),b) = multiply(X11,b)]. % 159.97/160.39 [2963=param(1528,570),[5], % 159.97/160.39 multiply(add(X10,multiply(X10,add(multiply(b,multiply(b,b)),X11))),b) = multiply(X10,multiply(X11,b))]. % 159.97/160.39 [2967=param(2962,518),[], % 159.97/160.39 multiply(add(X10,multiply(X11,multiply(b,multiply(b,b)))),b) = multiply(add(X10,X11),b)]. % 159.97/160.39 [3019=param(2963,646),[2967,507,340], % 159.97/160.39 multiply(X10,multiply(add(X11,multiply(X10,multiply(X10,multiply(X10,X11)))),b)) = additive_identity]. % 159.97/160.39 [3031=param(5,3019),[340,5], % 159.97/160.39 multiply(X10,multiply(add(X11,multiply(X10,multiply(X10,multiply(X10,X11)))),multiply(b,X12))) = additive_identity]. % 159.97/160.39 [3037=param(657,3031),[141], % 159.97/160.39 multiply(add(X10,multiply(b,multiply(b,multiply(b,X10)))),b) = additive_identity]. % 159.97/160.39 [3048=param(3031,2698),[], % 159.97/160.39 multiply(c,multiply(add(X10,multiply(c,multiply(c,multiply(c,X10)))),X11)) = additive_identity]. % 159.97/160.39 [3051=param(3,3037),[6,10], % 159.97/160.39 multiply(add(X10,add(X11,multiply(b,multiply(b,multiply(b,X11))))),b) = multiply(X10,b)]. % 159.97/160.39 [3192=param(657,3048),[141], % 159.97/160.39 multiply(add(X10,multiply(c,multiply(c,multiply(c,X10)))),c) = additive_identity]. % 159.97/160.39 [3197=param(3,3192),[6,10], % 159.97/160.39 multiply(add(X10,add(X11,multiply(c,multiply(c,multiply(c,X11))))),c) = multiply(X10,c)]. % 159.97/160.39 [3252=param(3197,517),[5,5,5], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(X10,c)))) = multiply(X10,c)]. % 159.97/160.39 [3261=param(5,3252),[5,5,5,5], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(X10,multiply(c,X11))))) = multiply(X10,multiply(c,X11))]. % 159.97/160.39 [3295=param(1773,3252),[3252], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(X10,c)))) = multiply(X10,c)]. % 159.97/160.39 [3306=param(5,3295),[5,5,5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(X10,multiply(c,X11))))) = multiply(X10,multiply(c,X11))]. % 159.97/160.39 [3307=param(27,3295),[], % 159.97/160.39 multiply(a,multiply(X10,c)) = multiply(c,multiply(b,multiply(b,multiply(X10,c))))]. % 159.97/160.39 [3318=param(3295,2196),[], % 159.97/160.39 multiply(add(b,X10),c) = multiply(b,add(c,multiply(b,multiply(b,multiply(X10,c)))))]. % 159.97/160.39 [3325=param(5,3307),[5,5,5,5,5], % 159.97/160.39 multiply(a,multiply(X10,multiply(c,X11))) = multiply(c,multiply(b,multiply(b,multiply(X10,multiply(c,X11)))))]. % 159.97/160.39 [3366=param(3261,2246),[2666,2], % 159.97/160.39 multiply(c,multiply(c,multiply(c,X10))) = multiply(X10,multiply(c,multiply(c,c)))]. % 159.97/160.39 [3371=param(3261,2674),[], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(X10,X11)))) = multiply(X10,multiply(c,multiply(c,multiply(c,X11))))]. % 159.97/160.39 [3405=param(3051,517),[5,5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(X10,b)))) = multiply(X10,b)]. % 159.97/160.39 [3413=param(5,3405),[5,5,5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(X10,multiply(b,X11))))) = multiply(X10,multiply(b,X11))]. % 159.97/160.39 [3470=param(3413,2336),[2891,2], % 159.97/160.39 multiply(b,multiply(b,multiply(b,X10))) = multiply(X10,multiply(b,multiply(b,b)))]. % 159.97/160.39 [3896=param(2854,4),[4], % 159.97/160.39 add(b,multiply(b,add(X10,multiply(add(c,b),multiply(b,b))))) = multiply(b,add(X10,a))]. % 159.97/160.39 [4088=param(551,2171),[2209], % 159.97/160.39 multiply(add(multiply(X10,multiply(X10,X10)),X11),X10) = add(X10,multiply(X11,X10))]. % 159.97/160.39 [4091=param(5,4088),[], % 159.97/160.39 multiply(add(multiply(X10,multiply(X10,X10)),X11),multiply(X10,X12)) = multiply(add(X10,multiply(X11,X10)),X12)]. % 159.97/160.39 [4099=param(4088,516),[], % 159.97/160.39 add(X12,multiply(add(X10,add(multiply(X12,multiply(X12,X12)),X11)),X12)) = multiply(add(X10,X11),X12)]. % 159.97/160.39 [4101=param(678,4088),[5,5,572,507,141], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(X11,multiply(X11,X11)))),X11) = additive_identity]. % 159.97/160.39 [4104=param(5,4101),[340], % 159.97/160.39 multiply(add(X10,multiply(X10,multiply(X11,multiply(X11,X11)))),multiply(X11,X12)) = additive_identity]. % 159.97/160.39 [4118=param(4104,22),[5,4091,5,5], % 159.97/160.39 multiply(X10,multiply(add(X11,multiply(X10,multiply(X10,multiply(X10,X11)))),X12)) = additive_identity]. % 159.97/160.39 [4131=param(657,4104),[141], % 159.97/160.39 multiply(X10,add(X11,multiply(X11,multiply(X10,multiply(X10,X10))))) = additive_identity]. % 159.97/160.39 [4151=param(4,4131),[6,10], % 159.97/160.39 multiply(X10,add(X11,add(X12,multiply(X12,multiply(X10,multiply(X10,X10)))))) = multiply(X10,X11)]. % 159.97/160.39 [4157=param(563,4131),[9], % 159.97/160.39 add(multiply(X10,multiply(X11,multiply(X10,multiply(X10,X10)))),X12) = add(X12,multiply(X10,X11))]. % 159.97/160.39 [4408=param(657,4118),[141], % 159.97/160.39 multiply(add(X10,multiply(X11,multiply(X11,multiply(X11,X10)))),X11) = additive_identity]. % 159.97/160.39 [4414=param(3,4408),[6,10], % 159.97/160.39 multiply(add(X10,add(X12,multiply(X11,multiply(X11,multiply(X11,X12))))),X11) = multiply(X10,X11)]. % 159.97/160.39 [4491=param(4414,517),[5,5,5], % 159.97/160.39 multiply(X11,multiply(X11,multiply(X11,multiply(X10,X11)))) = multiply(X10,X11)]. % 159.97/160.39 [4496=param(4491,5),[5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(X11,multiply(X12,X10))))) = multiply(X11,multiply(X12,X10))]. % 159.97/160.39 [4497=param(5,4491),[5,5,5,5], % 159.97/160.39 multiply(X11,multiply(X11,multiply(X11,multiply(X10,multiply(X11,X12))))) = multiply(X10,multiply(X11,X12))]. % 159.97/160.39 [4510=param(573,4491),[4491], % 159.97/160.39 multiply(a,multiply(a,multiply(a,add(c,multiply(X10,a))))) = add(c,multiply(X10,a))]. % 159.97/160.39 [4514=param(4491,671),[4088], % 159.97/160.39 multiply(X10,multiply(X10,multiply(add(X10,multiply(X10,X11)),X10))) = add(X10,multiply(X11,X10))]. % 159.97/160.39 [4537=demod(4099),[], % 159.97/160.39 add(X10,multiply(add(X11,add(multiply(X10,multiply(X10,X10)),X12)),X10)) = multiply(add(X11,X12),X10)]. % 159.97/160.39 [4538=param(1947,4491),[2922,2493,57,2648,2388,57,-3371], % 159.97/160.39 multiply(c,multiply(c,multiply(c,multiply(b,multiply(X10,a))))) = multiply(b,multiply(X10,a))]. % 159.97/160.39 [4617=param(4151,517),[], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X10,multiply(X10,X10)))) = multiply(X10,X11)]. % 159.97/160.39 [4624=param(4617,5),[], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X12,multiply(X10,multiply(X10,X10))))) = multiply(X10,multiply(X11,X12))]. % 159.97/160.39 [4625=param(5,4617),[5,5,5,5], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X10,multiply(X10,multiply(X10,X12))))) = multiply(X10,multiply(X11,X12))]. % 159.97/160.39 [4633=param(4497,4617),[], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,X11))) = multiply(X11,multiply(X10,multiply(X10,X10)))]. % 159.97/160.39 [4652=param(4497,4625),[], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(X11,X12)))) = multiply(X11,multiply(X10,multiply(X10,multiply(X10,X12))))]. % 159.97/160.39 [5267=param(4514,2322),[5,5,5,2488,2648,1976,-3371,2322,2322], % 159.97/160.39 multiply(c,multiply(c,multiply(add(c,multiply(b,a)),c))) = add(c,multiply(b,a))]. % 159.97/160.39 [5272=param(28,5267),[], % 159.97/160.39 multiply(c,multiply(add(c,multiply(b,a)),c)) = multiply(c,multiply(c,add(c,multiply(b,a))))]. % 159.97/160.39 [5273=param(4491,5272),[2344], % 159.97/160.39 multiply(add(c,multiply(b,a)),c) = multiply(c,add(c,multiply(b,a)))]. % 159.97/160.39 [5274=param(5,5273),[5], % 159.97/160.39 multiply(add(c,multiply(b,a)),multiply(c,X10)) = multiply(c,multiply(add(c,multiply(b,a)),X10))]. % 159.97/160.39 [5288=param(2412,552),[], % 159.97/160.39 multiply(b,add(multiply(X10,a),multiply(c,multiply(b,c)))) = multiply(add(c,multiply(b,X10)),a)]. % 159.97/160.39 [5292=param(5288,33),[2516,1947,-2536], % 159.97/160.39 multiply(add(c,multiply(b,a)),a) = multiply(b,multiply(c,multiply(b,add(c,multiply(b,a)))))]. % 159.97/160.39 [6051=param(4652,2),[5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X11,multiply(X10,multiply(X11,multiply(X10,multiply(X11,X11))))))) = multiply(X10,X11)]. % 159.97/160.39 [6060=param(4497,6051),[], % 159.97/160.39 multiply(X11,multiply(X10,multiply(X11,multiply(X10,multiply(X11,X11))))) = multiply(X10,multiply(X10,X11))]. % 159.97/160.39 [6063=param(4497,6060),[], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X11,multiply(X11,X10)))) = multiply(X11,multiply(X10,multiply(X11,multiply(X10,X10))))]. % 159.97/160.39 [6175=param(4,4491),[1163,4], % 159.97/160.39 multiply(X11,multiply(X11,multiply(X11,add(multiply(X10,X11),multiply(X11,X12))))) = add(multiply(X10,X11),multiply(X11,X12))]. % 159.97/160.39 [6233=param(5,2516),[5,5,5,5,5,5], % 159.97/160.39 multiply(b,multiply(b,multiply(c,X10))) = multiply(c,multiply(c,multiply(b,multiply(c,multiply(c,multiply(b,X10))))))]. % 159.97/160.39 [6246=param(29,1774),[], % 159.97/160.39 multiply(add(a,X10),add(c,b)) = multiply(add(c,multiply(X10,b)),multiply(b,multiply(b,add(c,b))))]. % 159.97/160.39 [6540=param(552,5),[], % 159.97/160.39 add(multiply(X10,multiply(X11,X12)),multiply(X13,multiply(X14,X12))) = multiply(add(multiply(X10,X11),multiply(X13,X14)),X12)]. % 159.97/160.39 [6541=param(552,5),[5], % 159.97/160.39 add(multiply(X10,X11),multiply(X12,multiply(X13,multiply(X14,X11)))) = multiply(add(X10,multiply(X12,multiply(X13,X14))),X11)]. % 159.97/160.39 [6560=param(552,1947),[], % 159.97/160.39 add(multiply(X10,X11),multiply(b,multiply(c,multiply(b,multiply(b,X11))))) = multiply(add(X10,multiply(b,a)),X11)]. % 159.97/160.39 [6568=param(551,2),[6541,-4633], % 159.97/160.39 multiply(X12,multiply(X12,multiply(X12,add(multiply(X10,X12),X11)))) = multiply(add(X10,multiply(X11,multiply(X12,X12))),X12)]. % 159.97/160.39 [6570=demod(6175),[6568,5], % 159.97/160.39 add(multiply(X10,X11),multiply(X11,X12)) = multiply(add(X10,multiply(X11,multiply(X12,multiply(X11,X11)))),X11)]. % 159.97/160.39 [6579=param(551,5),[5], % 159.97/160.39 add(multiply(X10,multiply(X11,multiply(X12,X13))),multiply(X14,X13)) = multiply(add(multiply(X10,multiply(X11,X12)),X14),X13)]. % 159.97/160.39 [6586=param(551,1947),[], % 159.97/160.39 add(multiply(b,multiply(c,multiply(b,multiply(b,X10)))),multiply(X11,X10)) = multiply(add(multiply(b,a),X11),X10)]. % 159.97/160.39 [6711=param(5,6060),[5,5,5,5,5,5], % 159.97/160.39 multiply(X11,multiply(X10,multiply(X11,multiply(X10,multiply(X11,multiply(X11,X12)))))) = multiply(X10,multiply(X10,multiply(X11,X12)))]. % 159.97/160.39 [6975=param(4625,5),[5], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X12,multiply(X10,multiply(X10,multiply(X10,X13)))))) = multiply(X10,multiply(X11,multiply(X12,X13)))]. % 159.97/160.39 [7086=param(598,568),[518,5,5,5], % 159.97/160.39 multiply(X10,add(X12,multiply(X10,multiply(add(X11,multiply(X10,X10)),X12)))) = multiply(X10,multiply(X10,multiply(X11,X12)))]. % 159.97/160.39 [7165=param(5,4510),[5,5], % 159.97/160.39 multiply(a,multiply(a,multiply(a,multiply(add(c,multiply(X10,a)),X11)))) = multiply(add(c,multiply(X10,a)),X11)]. % 159.97/160.39 [7180=param(4497,5),[5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(X11,multiply(X12,multiply(X10,X13)))))) = multiply(X11,multiply(X12,multiply(X10,X13)))]. % 159.97/160.39 [7198=param(4496,5),[5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X10,multiply(X11,multiply(X12,multiply(X13,X10)))))) = multiply(X11,multiply(X12,multiply(X13,X10)))]. % 159.97/160.39 [7322=param(3306,5),[5], % 159.97/160.39 multiply(b,multiply(b,multiply(b,multiply(X10,multiply(X11,multiply(c,X12)))))) = multiply(X10,multiply(X11,multiply(c,X12)))]. % 159.97/160.39 [7578=param(4491,727),[], % 159.97/160.39 multiply(add(multiply(b,X10),X11),a) = multiply(a,multiply(a,multiply(add(multiply(c,X10),multiply(a,X11)),a)))]. % 159.97/160.39 [7593=param(4,4633),[], % 159.97/160.39 add(multiply(X10,multiply(X10,multiply(X10,X11))),multiply(X11,X12)) = multiply(X11,add(multiply(X10,multiply(X10,X10)),X12))]. % 159.97/160.39 [7855=param(812,605),[3,7], % 159.97/160.39 multiply(add(X10,add(multiply(X10,a),add(X11,multiply(X11,a)))),b) = multiply(add(X10,X11),add(c,b))]. % 159.97/160.39 [7894=param(6579,1774),[7], % 159.97/160.39 multiply(add(multiply(b,multiply(b,b)),X10),add(c,b)) = add(c,add(b,multiply(X10,add(c,b))))]. % 159.97/160.39 [9508=param(598,4514),[518,5,5,5], % 159.97/160.39 multiply(X11,add(X12,multiply(X11,multiply(add(X11,multiply(X11,X10)),multiply(X11,X12))))) = multiply(X10,multiply(X11,X12))]. % 159.97/160.39 [9812=param(699,7855),[], % 159.97/160.39 add(multiply(X10,c),multiply(add(X10,X11),add(c,b))) = multiply(add(X10,add(X11,multiply(X11,a))),b)]. % 159.97/160.39 [10852=param(7086,6),[], % 159.97/160.39 multiply(X10,add(X11,multiply(X10,multiply(add(multiply(X10,X10),X12),X11)))) = multiply(X10,multiply(X10,multiply(X12,X11)))]. % 159.97/160.39 [10856=param(4537,1750),[7894,516,7578,1976,7593,5,4491], % 159.97/160.39 multiply(add(X10,multiply(add(multiply(c,multiply(c,c)),X10),a)),b) = add(c,multiply(X10,add(c,b)))]. % 159.97/160.39 [11088=param(4537,2380),[7578,1976,7593,5,4491,10856], % 159.97/160.39 add(b,multiply(add(X10,multiply(b,multiply(b,b))),add(c,b))) = add(c,multiply(X10,add(c,b)))]. % 159.97/160.39 [11090=param(11088,6246),[5,5,2,1721,945,2516,7180], % 159.97/160.39 add(b,multiply(add(c,b),multiply(b,multiply(b,add(c,b))))) = multiply(b,multiply(c,multiply(c,b)))]. % 159.97/160.39 [11091=param(517,11090),[-4157,-3470,6063,1976,-3371,2322,2424], % 159.97/160.39 add(multiply(b,multiply(c,multiply(c,b))),multiply(add(c,b),multiply(b,multiply(b,add(c,b))))) = b]. % 159.97/160.39 [11102=param(6711,3366),[4624], % 159.97/160.39 multiply(c,multiply(X10,multiply(c,multiply(X10,X11)))) = multiply(X10,multiply(X10,multiply(c,multiply(c,X11))))]. % 159.97/160.39 [11103=param(6711,3366),[28], % 159.97/160.39 multiply(c,multiply(X10,multiply(c,X10))) = multiply(X10,multiply(X10,multiply(c,c)))]. % 159.97/160.39 [11107=param(6711,4617),[], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X10,X11))) = multiply(X11,multiply(X11,multiply(X10,X10)))]. % 159.97/160.39 [11108=param(6711,4625),[], % 159.97/160.39 multiply(X10,multiply(X11,multiply(X10,multiply(X11,X12)))) = multiply(X11,multiply(X11,multiply(X10,multiply(X10,X12))))]. % 159.97/160.39 [11113=param(27,11107),[], % 159.97/160.39 multiply(a,multiply(X10,multiply(X10,multiply(b,b)))) = multiply(c,multiply(X10,multiply(b,X10)))]. % 159.97/160.39 [11128=param(7198,11107),[5,5,4617,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X11,multiply(X10,X11)))) = multiply(X11,multiply(X10,multiply(X10,multiply(X11,X10))))]. % 159.97/160.39 [11178=param(4497,11107),[5,5,5], % 159.97/160.39 multiply(X10,multiply(X10,multiply(X11,multiply(X10,multiply(X10,multiply(X11,X10)))))) = multiply(X10,multiply(X11,multiply(X10,X11)))]. % 160.05/160.43 [11202=param(2457,11103),[2493,2642,4491,6570,1976,-3371,2322,2493,-11128,4,4,6,2879,5,5,1976,-3371,2322,5274,5274,5292,4497,2493,6233,7180,11108,6233,1769,7180], % 160.05/160.43 multiply(add(c,multiply(b,a)),b) = multiply(c,multiply(b,multiply(c,multiply(c,add(c,multiply(b,a))))))]. % 160.05/160.43 [11203=demod(2645),[11202], % 160.05/160.43 multiply(b,add(c,multiply(c,multiply(c,multiply(b,multiply(c,a)))))) = multiply(c,multiply(b,multiply(c,multiply(c,add(c,multiply(b,a))))))]. % 160.05/160.43 [11263=param(6975,11113),[27], % 160.05/160.43 multiply(a,multiply(X10,multiply(X11,multiply(b,b)))) = multiply(a,multiply(X10,multiply(X11,multiply(c,multiply(c,a)))))]. % 160.05/160.43 [11271=param(7165,11263),[3325,2493,7322,27,7180], % 160.05/160.43 multiply(add(c,multiply(X10,a)),multiply(b,b)) = multiply(add(c,multiply(X10,a)),multiply(c,multiply(c,a)))]. % 160.05/160.43 [11294=param(28,11178),[4497], % 160.05/160.43 multiply(X11,multiply(X10,multiply(X11,multiply(X11,multiply(X10,X11))))) = multiply(X10,multiply(X11,X10))]. % 160.05/160.43 [11295=param(5,11294),[5,5,5,5,5,5], % 160.05/160.43 multiply(X11,multiply(X10,multiply(X11,multiply(X11,multiply(X10,multiply(X11,X12)))))) = multiply(X10,multiply(X11,multiply(X10,X12)))]. % 160.05/160.43 [11306=param(11295,11294),[4491,4491], % 160.05/160.43 multiply(X10,multiply(X11,multiply(X11,X10))) = multiply(X11,multiply(X10,multiply(X10,X11)))]. % 160.05/160.43 [11309=param(4,11306),[], % 160.05/160.43 add(multiply(X10,X11),multiply(X12,multiply(X10,multiply(X10,X12)))) = multiply(X10,add(X11,multiply(X12,multiply(X12,X10))))]. % 160.05/160.43 [11310=demod(11091),[11309,6540,9812,2851,5], % 160.05/160.43 multiply(b,multiply(add(c,multiply(b,multiply(add(c,b),multiply(b,b)))),multiply(b,b))) = b]. % 160.05/160.43 [11324=param(6541,11306),[], % 160.05/160.43 add(multiply(X10,X11),multiply(X12,multiply(X11,multiply(X11,X12)))) = multiply(add(X10,multiply(X11,multiply(X12,X12))),X11)]. % 160.05/160.43 [11335=param(10852,11324),[5,9508,5,5,5,5], % 160.05/160.43 multiply(X10,multiply(X10,multiply(X11,X12))) = multiply(X11,multiply(X11,multiply(X10,multiply(X11,multiply(X11,multiply(X10,X12))))))]. % 160.05/160.43 [11443=param(3896,6586),[34,6,-2855,11310,507,2,6,2901,5,5,1976,-3371,2322,11271,5274,5274,5292], % 160.05/160.43 multiply(b,multiply(c,multiply(c,multiply(b,multiply(c,multiply(b,add(c,multiply(b,a)))))))) = additive_identity]. % 160.05/160.43 [11458=param(6560,2656),[5274,11202,11335,1976,28,4538,6540,6570,3318,5,5,5,-3366,28,11335,1976,28,11203,5,5,5,5,5292,11443,141,141], % 160.05/160.43 multiply(c,multiply(c,multiply(b,multiply(c,multiply(c,add(c,multiply(b,a))))))) = additive_identity]. % 160.05/160.43 [11459=param(2663,6560),[5274,5274,11202,11458,141,141,-11102,1976,-3371,2322,2642,2493,11107,1976,28,-3371,2322], % 160.05/160.43 add(c,multiply(b,a)) = additive_identity]. % 160.05/160.43 [11473=demod(11459),[], % 160.05/160.43 add(c,multiply(b,a)) = additive_identity]. % 160.05/160.43 [11475=param(517,11473),[6,10], % 160.05/160.43 multiply(b,a) = c]. % 160.05/160.43 [12415=param(12,11475),[11], % 160.05/160.43 thmtrue = thmfalse]. % 160.05/160.43 % SZS output end CNFRefutation % 160.05/160.43 Space: 622884 KB %------------------------------------------------------------------------------