%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP470-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n024.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 : Sat Jul 16 09:14:10 EDT 2022 % Result : Unsatisfiable 1.62s 2.02s % Output : CNFRefutation 1.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : GRP470-1 : TPTP v8.1.0. Released v2.6.0. % 0.13/0.14 % Command : fiesta-wrapper %s % 0.14/0.36 % Computer : n024.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Mon Jun 13 04:48:48 EDT 2022 % 0.14/0.36 % CPUTime : % 1.62/2.02 Theorem Proved. % 1.62/2.02 % SZS status Unsatisfiable % 1.62/2.02 % SZS output start CNFRefutation % 1.62/2.02 [1=axiom,[], % 1.62/2.02 divide(X10,inverse(X11)) = multiply(X10,X11)]. % 1.62/2.02 [2=axiom,[], % 1.62/2.02 divide(inverse(divide(X10,divide(X11,divide(X12,X13)))),divide(divide(X13,X12),X10)) = X11]. % 1.62/2.02 [3=axiom,[], % 1.62/2.02 thtop(X10,X10) = thmfalse]. % 1.62/2.02 [4=axiom,[], % 1.62/2.02 thtop(multiply(multiply(inverse(b2),b2),a2),a2) = thmtrue]. % 1.62/2.02 [5=param(2,1),[], % 1.62/2.02 divide(inverse(divide(X10,divide(X11,multiply(X12,X13)))),divide(divide(inverse(X13),X12),X10)) = X11]. % 1.62/2.02 [6=param(2,1),[], % 1.62/2.02 divide(inverse(divide(inverse(X10),divide(X11,divide(X12,X13)))),multiply(divide(X13,X12),X10)) = X11]. % 1.62/2.02 [7=param(2,1),[], % 1.62/2.02 divide(inverse(divide(X10,divide(X11,divide(inverse(X12),X13)))),divide(multiply(X13,X12),X10)) = X11]. % 1.62/2.02 [10=param(6,1),[], % 1.62/2.02 divide(inverse(divide(inverse(X10),divide(X11,multiply(X12,X13)))),multiply(divide(inverse(X13),X12),X10)) = X11]. % 1.62/2.02 [12=param(2,2),[1], % 1.62/2.02 divide(inverse(X10),multiply(divide(X11,X12),divide(divide(X12,X11),divide(X10,divide(X13,X14))))) = divide(X14,X13)]. % 1.62/2.02 [13=param(2,2),[], % 1.62/2.02 divide(inverse(divide(X10,X11)),divide(divide(X12,divide(X13,X14)),X10)) = inverse(divide(X12,divide(X11,divide(X14,X13))))]. % 1.62/2.02 [15=param(2,5),[1], % 1.62/2.02 divide(inverse(X10),multiply(divide(X11,X12),divide(divide(X12,X11),divide(X10,multiply(X13,X14))))) = divide(inverse(X14),X13)]. % 1.62/2.02 [17=param(2,7),[1], % 1.62/2.02 divide(inverse(X10),multiply(divide(X11,X12),divide(divide(X12,X11),divide(X10,divide(inverse(X13),X14))))) = multiply(X14,X13)]. % 1.62/2.02 [18=param(13,2),[], % 1.62/2.02 inverse(divide(X10,divide(divide(X11,divide(divide(X12,X13),X10)),divide(X13,X12)))) = X11]. % 1.62/2.02 [19=param(13,5),[], % 1.62/2.02 inverse(divide(inverse(X10),divide(divide(X11,multiply(divide(X12,X13),X10)),divide(X13,X12)))) = X11]. % 1.62/2.02 [20=param(2,13),[], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),divide(divide(X12,divide(X13,X14)),X10)),divide(divide(X13,X14),X12)) = X11]. % 1.62/2.02 [24=param(1,18),[], % 1.62/2.02 divide(X10,X11) = multiply(X10,divide(X12,divide(divide(X11,divide(divide(X13,X14),X12)),divide(X14,X13))))]. % 1.62/2.02 [25=param(1,19),[], % 1.62/2.02 divide(X10,X11) = multiply(X10,divide(inverse(X12),divide(divide(X11,multiply(divide(X13,X14),X12)),divide(X14,X13))))]. % 1.62/2.02 [31=param(20,2),[2], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),divide(divide(X12,X13),X10)),divide(X13,X12)) = X11]. % 1.62/2.02 [32=param(31,1),[], % 1.62/2.02 divide(divide(inverse(multiply(X10,X11)),divide(divide(X12,X13),X10)),divide(X13,X12)) = inverse(X11)]. % 1.62/2.02 [33=param(31,1),[], % 1.62/2.02 divide(divide(inverse(divide(inverse(X10),X11)),multiply(divide(X12,X13),X10)),divide(X13,X12)) = X11]. % 1.62/2.02 [34=param(31,1),[], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),divide(multiply(X12,X13),X10)),divide(inverse(X13),X12)) = X11]. % 1.62/2.02 [37=param(2,31),[], % 1.62/2.02 divide(inverse(divide(X10,X11)),divide(divide(X12,X13),X10)) = divide(inverse(divide(X14,X11)),divide(divide(X12,X13),X14))]. % 1.62/2.02 [38=param(2,31),[1], % 1.62/2.02 divide(inverse(divide(divide(X10,X11),divide(X12,multiply(divide(divide(X11,X10),X13),divide(X13,X14))))),X14) = X12]. % 1.62/2.02 [40=param(12,31),[1], % 1.62/2.02 divide(inverse(X10),multiply(multiply(divide(divide(divide(X11,X12),X10),X13),divide(X13,X14)),X14)) = divide(X12,X11)]. % 1.62/2.02 [41=param(15,31),[1], % 1.62/2.02 divide(inverse(X10),multiply(multiply(divide(divide(multiply(X11,X12),X10),X13),divide(X13,X14)),X14)) = divide(inverse(X12),X11)]. % 1.62/2.02 [43=param(32,1),[], % 1.62/2.02 divide(divide(inverse(multiply(inverse(X10),X11)),multiply(divide(X12,X13),X10)),divide(X13,X12)) = inverse(X11)]. % 1.62/2.02 [44=param(32,1),[], % 1.62/2.02 divide(divide(inverse(multiply(X10,X11)),divide(multiply(X12,X13),X10)),divide(inverse(X13),X12)) = inverse(X11)]. % 1.62/2.02 [47=param(2,32),[1,1], % 1.62/2.02 multiply(inverse(divide(divide(X10,X11),divide(X12,multiply(divide(divide(X11,X10),X13),multiply(X13,X14))))),X14) = X12]. % 1.62/2.02 [49=param(12,32),[1], % 1.62/2.02 divide(inverse(X10),multiply(multiply(divide(divide(divide(X11,X12),X10),X13),multiply(X13,X14)),inverse(X14))) = divide(X12,X11)]. % 1.62/2.02 [50=param(32,31),[1], % 1.62/2.02 divide(divide(inverse(multiply(divide(X10,X11),X12)),X13),multiply(divide(divide(X11,X10),X14),divide(X14,X13))) = inverse(X12)]. % 1.62/2.02 [51=param(31,32),[1,1], % 1.62/2.02 divide(multiply(inverse(divide(divide(X10,X11),X12)),X13),multiply(divide(divide(X11,X10),X14),multiply(X14,X13))) = X12]. % 1.62/2.02 [58=param(34,1),[], % 1.62/2.02 divide(divide(inverse(divide(inverse(X10),X11)),multiply(multiply(X12,X13),X10)),divide(inverse(X13),X12)) = X11]. % 1.62/2.02 [61=param(31,34),[1], % 1.62/2.02 divide(divide(inverse(divide(divide(inverse(X10),X11),X12)),X13),multiply(divide(multiply(X11,X10),X14),divide(X14,X13))) = X12]. % 1.62/2.02 [75=param(37,2),[2], % 1.62/2.02 divide(inverse(divide(X10,X11)),divide(X12,X10)) = divide(inverse(divide(X13,X11)),divide(X12,X13))]. % 1.62/2.02 [76=param(75,1),[1], % 1.62/2.02 divide(inverse(multiply(X10,X11)),divide(X12,X10)) = divide(inverse(multiply(X13,X11)),divide(X12,X13))]. % 1.62/2.02 [77=param(75,1),[], % 1.62/2.02 divide(inverse(divide(inverse(X10),X11)),multiply(X12,X10)) = divide(inverse(divide(X13,X11)),divide(X12,X13))]. % 1.62/2.02 [79=param(12,75),[17,1], % 1.62/2.02 multiply(divide(X10,X11),divide(X11,X12)) = multiply(divide(X10,X13),divide(X13,X12))]. % 1.62/2.02 [80=param(79,1),[], % 1.62/2.02 multiply(multiply(X10,X11),divide(inverse(X11),X12)) = multiply(divide(X10,X13),divide(X13,X12))]. % 1.62/2.02 [81=param(79,1),[1], % 1.62/2.02 multiply(divide(X10,X11),multiply(X11,X12)) = multiply(divide(X10,X13),multiply(X13,X12))]. % 1.62/2.02 [84=param(81,1),[], % 1.62/2.02 multiply(multiply(X10,X11),multiply(inverse(X11),X12)) = multiply(divide(X10,X13),multiply(X13,X12))]. % 1.62/2.02 [87=param(76,1),[], % 1.62/2.02 divide(inverse(multiply(inverse(X10),X11)),multiply(X12,X10)) = divide(inverse(multiply(X13,X11)),divide(X12,X13))]. % 1.62/2.02 [89=param(58,40),[13,1,1], % 1.62/2.02 multiply(divide(X10,X11),divide(divide(X11,X10),divide(X12,multiply(X13,X12)))) = X13]. % 1.62/2.02 [94=param(89,33),[1], % 1.62/2.02 multiply(multiply(multiply(divide(multiply(X10,X11),X11),X12),divide(inverse(X12),X13)),X13) = X10]. % 1.62/2.02 [99=param(89,58),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(multiply(X10,inverse(X11)),X11),X12),divide(inverse(X12),X13)),X13) = X10]. % 1.62/2.02 [100=param(58,41),[13,1,1], % 1.62/2.02 multiply(divide(inverse(X10),X11),divide(multiply(X11,X10),divide(X12,multiply(X13,X12)))) = X13]. % 1.62/2.02 [101=param(33,100),[1], % 1.62/2.02 divide(divide(inverse(divide(inverse(divide(multiply(X10,X11),divide(X12,multiply(X13,X12)))),X14)),X13),multiply(X10,X11)) = X14]. % 1.62/2.02 [107=param(100,50),[1,1], % 1.62/2.02 multiply(divide(inverse(X10),X11),multiply(multiply(X11,X10),X12)) = multiply(divide(X13,X14),multiply(divide(X14,X13),X12))]. % 1.62/2.02 [109=param(101,89),[89], % 1.62/2.02 divide(divide(inverse(divide(inverse(divide(X10,divide(X11,multiply(X12,X11)))),X13)),X12),X10) = X13]. % 1.62/2.02 [112=param(109,1),[], % 1.62/2.02 divide(divide(inverse(multiply(inverse(divide(X10,divide(X11,multiply(X12,X11)))),X13)),X12),X10) = inverse(X13)]. % 1.62/2.02 [115=param(31,109),[1], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),X12),multiply(X13,divide(inverse(divide(X10,divide(X14,multiply(X13,X14)))),X12))) = X11]. % 1.62/2.02 [119=param(109,77),[1], % 1.62/2.02 multiply(divide(inverse(divide(inverse(divide(X10,divide(X11,multiply(X12,X11)))),divide(X13,X10))),X12),X14) = multiply(X13,X14)]. % 1.62/2.02 [126=param(89,61),[1], % 1.62/2.02 multiply(divide(X10,X11),divide(divide(X11,X10),X12)) = multiply(multiply(X13,X14),divide(divide(inverse(X14),X13),X12))]. % 1.62/2.02 [130=param(89,119),[89], % 1.62/2.02 divide(inverse(divide(inverse(divide(X11,divide(X12,multiply(X13,X12)))),divide(X10,X11))),X13) = X10]. % 1.62/2.02 [136=param(126,1),[1], % 1.62/2.02 multiply(divide(X10,X11),multiply(divide(X11,X10),X12)) = multiply(multiply(X13,X14),multiply(divide(inverse(X14),X13),X12))]. % 1.62/2.02 [138=param(136,107),[], % 1.62/2.02 multiply(multiply(X10,X11),multiply(divide(inverse(X11),X10),X12)) = multiply(divide(inverse(X13),X14),multiply(multiply(X14,X13),X12))]. % 1.62/2.02 [196=param(12,12),[17], % 1.62/2.02 multiply(multiply(divide(X10,X11),divide(divide(X11,X10),divide(X12,divide(X13,X14)))),X12) = divide(X13,X14)]. % 1.62/2.02 [240=param(32,112),[1,1], % 1.62/2.02 divide(multiply(inverse(multiply(X10,X11)),X12),multiply(X13,multiply(inverse(divide(X10,divide(X14,multiply(X13,X14)))),X12))) = inverse(X11)]. % 1.62/2.02 [260=param(196,2),[2], % 1.62/2.02 multiply(multiply(divide(X10,X11),divide(divide(X11,X10),divide(X12,X13))),X12) = X13]. % 1.62/2.02 [262=param(260,1),[], % 1.62/2.02 multiply(multiply(divide(inverse(X10),X11),divide(multiply(X11,X10),divide(X12,X13))),X12) = X13]. % 1.62/2.02 [263=param(260,1),[], % 1.62/2.02 multiply(multiply(divide(X10,X11),divide(divide(X11,X10),multiply(X12,X13))),X12) = inverse(X13)]. % 1.62/2.02 [268=param(260,31),[1], % 1.62/2.02 multiply(multiply(multiply(divide(divide(X10,X11),X12),divide(X12,X13)),X13),X11) = X10]. % 1.62/2.02 [269=param(260,32),[1], % 1.62/2.02 multiply(multiply(multiply(divide(divide(X10,X11),X12),multiply(X12,X13)),inverse(X13)),X11) = X10]. % 1.62/2.02 [270=param(260,33),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(divide(X10,X11),X12),divide(inverse(X12),X13)),X13),X11) = X10]. % 1.62/2.02 [271=param(260,34),[1], % 1.62/2.02 multiply(multiply(multiply(divide(multiply(X10,X11),X12),divide(X12,X13)),X13),inverse(X11)) = X10]. % 1.62/2.02 [272=param(260,43),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(divide(X10,X11),X12),multiply(inverse(X12),X13)),inverse(X13)),X11) = X10]. % 1.62/2.02 [292=param(271,80),[], % 1.62/2.02 multiply(multiply(multiply(multiply(multiply(X10,X11),X12),divide(inverse(X12),X13)),X13),inverse(X11)) = X10]. % 1.62/2.02 [298=param(269,84),[], % 1.62/2.02 multiply(divide(multiply(divide(divide(X10,multiply(inverse(inverse(X11)),X12)),X13),multiply(X13,X11)),X14),multiply(X14,X12)) = X10]. % 1.62/2.02 [301=param(262,24),[], % 1.62/2.02 multiply(divide(divide(inverse(X10),X11),X12),divide(X12,divide(divide(X13,X14),multiply(X11,X10)))) = divide(X14,X13)]. % 1.62/2.02 [312=param(292,1),[], % 1.62/2.02 multiply(multiply(multiply(multiply(multiply(X10,X11),X12),multiply(inverse(X12),X13)),inverse(X13)),inverse(X11)) = X10]. % 1.62/2.02 [325=param(292,268),[], % 1.62/2.02 multiply(multiply(X10,X11),inverse(divide(X12,X13))) = divide(divide(X10,divide(inverse(X13),X11)),X12)]. % 1.62/2.02 [327=param(292,269),[], % 1.62/2.02 divide(divide(X10,divide(inverse(inverse(X13)),X11)),X12) = multiply(multiply(X10,X11),inverse(multiply(X12,X13)))]. % 1.62/2.02 [330=param(292,270),[], % 1.62/2.02 multiply(multiply(X10,X11),inverse(divide(inverse(X12),X13))) = multiply(divide(X10,divide(inverse(X13),X11)),X12)]. % 1.62/2.02 [336=param(327,1),[], % 1.62/2.02 divide(divide(X10,multiply(inverse(inverse(X11)),X12)),X13) = multiply(multiply(X10,inverse(X12)),inverse(multiply(X13,X11)))]. % 1.62/2.02 [337=demod(298),[336], % 1.62/2.02 multiply(divide(multiply(multiply(multiply(X10,inverse(X11)),inverse(multiply(X12,X13))),multiply(X12,X13)),X14),multiply(X14,X11)) = X10]. % 1.62/2.02 [362=param(89,325),[13,1,1], % 1.62/2.02 multiply(divide(X10,X11),multiply(divide(X11,X10),divide(X12,divide(X13,multiply(X14,X13))))) = multiply(X12,X14)]. % 1.62/2.02 [363=param(100,325),[13,1,1], % 1.62/2.02 multiply(divide(inverse(X10),X11),multiply(multiply(X11,X10),divide(X12,divide(X13,multiply(X14,X13))))) = multiply(X12,X14)]. % 1.62/2.02 [370=param(2,325),[], % 1.62/2.02 divide(inverse(divide(X10,divide(X11,divide(divide(inverse(X12),X13),X14)))),multiply(multiply(X14,X13),inverse(divide(X10,X12)))) = X11]. % 1.62/2.02 [372=param(13,325),[1], % 1.62/2.02 divide(inverse(divide(X10,X11)),multiply(multiply(X12,X13),inverse(divide(X10,X14)))) = inverse(divide(X12,divide(X11,multiply(X13,X14))))]. % 1.62/2.02 [373=demod(370),[372], % 1.62/2.02 inverse(divide(X10,divide(divide(X11,divide(divide(inverse(X12),X13),X10)),multiply(X13,X12)))) = X11]. % 1.62/2.02 [387=param(373,17),[260], % 1.62/2.02 inverse(divide(X10,divide(divide(X11,divide(multiply(X12,X13),X10)),divide(inverse(X13),X12)))) = X11]. % 1.62/2.02 [455=param(312,268),[], % 1.62/2.02 multiply(multiply(X10,inverse(X11)),inverse(divide(X12,X13))) = divide(divide(X10,multiply(inverse(X13),X11)),X12)]. % 1.62/2.02 [478=param(58,49),[327], % 1.62/2.02 divide(divide(X10,X11),divide(inverse(multiply(X12,X13)),multiply(multiply(divide(X11,X10),X14),inverse(multiply(X12,X13))))) = X14]. % 1.62/2.02 [505=param(89,455),[], % 1.62/2.02 multiply(divide(multiply(inverse(X10),X11),X12),multiply(multiply(X12,inverse(X11)),inverse(divide(divide(X13,multiply(X14,X13)),X10)))) = X14]. % 1.62/2.02 [561=param(362,301),[], % 1.62/2.02 multiply(divide(X10,divide(inverse(divide(X11,X12)),X13)),divide(X12,X11)) = multiply(X10,X13)]. % 1.62/2.02 [567=param(561,330),[], % 1.62/2.02 multiply(multiply(X10,X11),inverse(divide(inverse(divide(X12,X13)),divide(X13,X12)))) = multiply(X10,X11)]. % 1.62/2.02 [568=param(362,561),[], % 1.62/2.02 multiply(divide(divide(inverse(divide(divide(X10,multiply(X11,X10)),X12)),X13),X14),multiply(X14,X13)) = multiply(X12,X11)]. % 1.62/2.02 [570=param(567,47),[47], % 1.62/2.02 multiply(X10,inverse(divide(inverse(divide(X11,X12)),divide(X12,X11)))) = X10]. % 1.62/2.02 [571=param(570,1),[], % 1.62/2.02 multiply(X10,inverse(divide(inverse(multiply(X11,X12)),divide(inverse(X12),X11)))) = X10]. % 1.62/2.02 [572=param(570,1),[], % 1.62/2.02 multiply(X10,inverse(divide(inverse(divide(inverse(X11),X12)),multiply(X12,X11)))) = X10]. % 1.62/2.02 [601=param(33,570),[], % 1.62/2.02 divide(divide(inverse(divide(inverse(inverse(divide(inverse(divide(X10,X11)),divide(X11,X10)))),X12)),divide(X13,X14)),divide(X14,X13)) = X12]. % 1.62/2.02 [622=param(76,570),[570], % 1.62/2.02 divide(inverse(X10),divide(X11,X10)) = divide(inverse(X12),divide(X11,X12))]. % 1.62/2.02 [628=param(81,570),[570], % 1.62/2.02 multiply(divide(X10,X11),X11) = multiply(divide(X10,X12),X12)]. % 1.62/2.02 [630=param(84,570),[570], % 1.62/2.02 multiply(multiply(X10,X11),inverse(X11)) = multiply(divide(X10,X12),X12)]. % 1.62/2.02 [633=param(87,570),[570], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(X11,X10)) = divide(inverse(X12),divide(X11,X12))]. % 1.62/2.02 [647=param(570,130),[1], % 1.62/2.02 multiply(X10,inverse(divide(inverse(multiply(X11,divide(inverse(divide(X12,divide(X13,multiply(X11,X13)))),divide(X14,X12)))),X14))) = X10]. % 1.62/2.02 [660=param(570,270),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,divide(inverse(divide(X11,X12)),divide(X12,X11))),X13),divide(inverse(X13),X14)),X14) = X10]. % 1.62/2.02 [663=param(570,272),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,divide(inverse(divide(X11,X12)),divide(X12,X11))),X13),multiply(inverse(X13),X14)),inverse(X14)) = X10]. % 1.62/2.02 [689=param(570,455),[1], % 1.62/2.02 multiply(divide(X10,multiply(inverse(divide(X12,X13)),X11)),divide(X13,X12)) = multiply(X10,inverse(X11))]. % 1.62/2.02 [825=param(630,268),[1], % 1.62/2.02 multiply(divide(multiply(divide(multiply(X10,X11),X12),divide(X12,X11)),X13),X13) = X10]. % 1.62/2.02 [885=param(84,630),[], % 1.62/2.02 multiply(multiply(multiply(X10,X11),inverse(X11)),multiply(inverse(X12),X13)) = multiply(divide(divide(X10,X12),X14),multiply(X14,X13))]. % 1.62/2.02 [897=param(263,630),[], % 1.62/2.02 multiply(multiply(divide(X10,X11),divide(divide(X11,X10),multiply(multiply(X12,X13),inverse(X13)))),divide(X12,X14)) = inverse(X14)]. % 1.62/2.02 [916=param(2,622),[1], % 1.62/2.02 divide(inverse(divide(inverse(X10),divide(X11,X10))),multiply(divide(X12,X13),divide(X13,X12))) = X11]. % 1.62/2.02 [934=param(622,32),[1], % 1.62/2.02 divide(inverse(X13),divide(divide(inverse(multiply(X14,X12)),divide(divide(X11,X10),X14)),X13)) = multiply(inverse(divide(X10,X11)),X12)]. % 1.62/2.02 [938=param(34,622),[1], % 1.62/2.02 divide(divide(inverse(divide(inverse(X10),divide(X11,X10))),multiply(multiply(X12,X13),X14)),divide(inverse(X13),X12)) = divide(X11,X14)]. % 1.62/2.02 [940=param(622,43),[1], % 1.62/2.02 divide(inverse(X13),divide(divide(inverse(multiply(inverse(X14),X12)),multiply(divide(X11,X10),X14)),X13)) = multiply(inverse(divide(X10,X11)),X12)]. % 1.62/2.02 [942=param(622,44),[1], % 1.62/2.02 divide(inverse(X13),divide(divide(inverse(multiply(X14,X12)),divide(multiply(X11,X10),X14)),X13)) = multiply(inverse(divide(inverse(X10),X11)),X12)]. % 1.62/2.02 [945=param(75,622),[1], % 1.62/2.02 divide(inverse(divide(inverse(X10),divide(X11,X10))),multiply(X12,X13)) = divide(inverse(divide(X14,divide(X11,X13))),divide(X12,X14))]. % 1.62/2.02 [951=param(81,622),[], % 1.62/2.02 multiply(divide(inverse(X10),divide(X11,X10)),multiply(divide(X11,X12),X13)) = multiply(divide(inverse(X12),X14),multiply(X14,X13))]. % 1.62/2.02 [952=param(622,109),[], % 1.62/2.02 divide(inverse(X12),divide(divide(inverse(divide(inverse(divide(X10,divide(X13,multiply(X14,X13)))),X11)),X14),X12)) = divide(inverse(X10),X11)]. % 1.62/2.02 [955=param(622,112),[1], % 1.62/2.02 divide(inverse(X12),divide(divide(inverse(multiply(inverse(divide(X10,divide(X13,multiply(X14,X13)))),X11)),X14),X12)) = multiply(inverse(X10),X11)]. % 1.62/2.02 [970=param(363,622),[], % 1.62/2.02 multiply(divide(inverse(X10),X11),multiply(multiply(X11,X10),divide(inverse(X12),divide(X13,X12)))) = multiply(inverse(multiply(X14,X13)),X14)]. % 1.62/2.02 [985=param(572,1),[], % 1.62/2.02 multiply(X10,inverse(divide(inverse(multiply(inverse(X11),X12)),multiply(inverse(X12),X11)))) = X10]. % 1.62/2.02 [1014=param(572,269),[], % 1.62/2.02 multiply(X10,inverse(divide(inverse(divide(inverse(X11),multiply(multiply(divide(divide(X12,X11),X13),multiply(X13,X14)),inverse(X14)))),X12))) = X10]. % 1.62/2.02 [1049=param(571,99),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,inverse(X11)),X11),X12),multiply(inverse(X12),divide(inverse(multiply(X13,X14)),divide(inverse(X14),X13)))) = X10]. % 1.62/2.02 [1073=param(571,272),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,divide(inverse(multiply(X11,X12)),divide(inverse(X12),X11))),X13),multiply(inverse(X13),X14)),inverse(X14)) = X10]. % 1.62/2.02 [1074=param(292,571),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,X11),X12),multiply(inverse(X12),divide(inverse(multiply(X13,X14)),divide(inverse(X14),X13)))),inverse(X11)) = X10]. % 1.62/2.02 [1075=param(325,571),[1], % 1.62/2.02 multiply(X10,inverse(divide(X11,X12))) = divide(divide(X10,multiply(inverse(X12),divide(inverse(multiply(X13,X14)),divide(inverse(X14),X13)))),X11)]. % 1.62/2.02 [1089=param(38,633),[], % 1.62/2.02 divide(inverse(divide(divide(X10,X11),divide(inverse(X12),divide(divide(divide(X11,X10),X13),X12)))),X14) = inverse(inverse(divide(X13,X14)))]. % 1.62/2.02 [1108=param(633,94),[], % 1.62/2.02 divide(inverse(X12),divide(multiply(multiply(divide(multiply(X11,X13),X13),X14),divide(inverse(X14),X10)),X12)) = divide(inverse(inverse(X10)),X11)]. % 1.62/2.02 [1130=param(633,561),[], % 1.62/2.02 divide(inverse(X14),divide(divide(X12,divide(inverse(divide(X11,X10)),X13)),X14)) = divide(inverse(inverse(divide(X10,X11))),multiply(X12,X13))]. % 1.62/2.02 [1135=param(633,628),[], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(divide(X11,X12),X12)) = divide(inverse(X13),divide(divide(X11,X10),X13))]. % 1.62/2.02 [1137=param(633,630),[], % 1.62/2.02 divide(inverse(inverse(inverse(X10))),multiply(divide(X11,X12),X12)) = divide(inverse(X13),divide(multiply(X11,X10),X13))]. % 1.62/2.02 [1138=param(633,630),[], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(multiply(X11,X12),inverse(X12))) = divide(inverse(X13),divide(divide(X11,X10),X13))]. % 1.62/2.02 [1172=param(387,633),[1], % 1.62/2.02 inverse(divide(inverse(inverse(X10)),multiply(divide(X11,multiply(multiply(X12,X13),divide(inverse(X13),X12))),X10))) = X11]. % 1.62/2.02 [1187=param(985,270),[1], % 1.62/2.02 multiply(multiply(multiply(multiply(X10,divide(inverse(multiply(inverse(X11),X12)),multiply(inverse(X12),X11))),X13),divide(inverse(X13),X14)),X14) = X10]. % 1.62/2.02 [1212=param(362,825),[], % 1.62/2.02 multiply(divide(divide(X10,divide(X11,multiply(X12,X11))),multiply(divide(multiply(X13,X14),X15),divide(X15,X14))),X13) = multiply(X10,X12)]. % 1.62/2.02 [1219=param(825,630),[], % 1.62/2.02 multiply(multiply(multiply(divide(multiply(X10,X11),X12),divide(X12,X11)),X13),inverse(X13)) = X10]. % 1.62/2.02 [1220=param(633,825),[], % 1.62/2.02 divide(inverse(X12),divide(divide(multiply(divide(multiply(X11,X13),X14),divide(X14,X13)),X10),X12)) = divide(inverse(inverse(X10)),X11)]. % 1.62/2.02 [1221=param(825,985),[1], % 1.62/2.02 multiply(multiply(divide(multiply(X10,X11),X12),divide(X12,X11)),divide(inverse(multiply(inverse(X13),X14)),multiply(inverse(X14),X13))) = X10]. % 1.62/2.02 [1237=param(689,633),[561], % 1.62/2.02 multiply(inverse(X10),X10) = multiply(inverse(inverse(X11)),inverse(X11))]. % 1.62/2.02 [1243=param(10,1237),[1], % 1.62/2.02 divide(inverse(divide(inverse(X10),divide(X11,multiply(inverse(inverse(X12)),inverse(X12))))),multiply(multiply(inverse(X13),X13),X10)) = X11]. % 1.62/2.02 [1244=param(1237,18),[-24], % 1.62/2.02 divide(X10,X10) = multiply(inverse(inverse(X11)),inverse(X11))]. % 1.62/2.02 [1253=param(51,1237),[], % 1.62/2.02 divide(multiply(inverse(inverse(X10)),inverse(X10)),multiply(divide(divide(X11,X12),X13),multiply(X13,divide(divide(X12,X11),X14)))) = X14]. % 1.62/2.02 [1268=param(89,1237),[], % 1.62/2.02 multiply(divide(X10,X11),divide(divide(X11,X10),divide(X12,multiply(inverse(inverse(X13)),inverse(X13))))) = inverse(X12)]. % 1.62/2.02 [1345=param(2,1244),[], % 1.62/2.02 divide(inverse(divide(divide(X10,X11),divide(X12,divide(X11,X10)))),multiply(inverse(inverse(X13)),inverse(X13))) = X12]. % 1.62/2.02 [1365=param(17,1244),[1268,1], % 1.62/2.02 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 1.62/2.02 [1381=param(40,1244),[], % 1.62/2.02 divide(inverse(X10),multiply(multiply(divide(divide(divide(X11,X12),X10),X13),multiply(inverse(inverse(X14)),inverse(X14))),X13)) = divide(X12,X11)]. % 1.62/2.02 [1397=param(81,1244),[], % 1.62/2.02 multiply(multiply(inverse(inverse(X10)),inverse(X10)),multiply(X11,X12)) = multiply(divide(X11,X13),multiply(X13,X12))]. % 1.62/2.02 [1403=param(260,1244),[], % 1.62/2.02 multiply(multiply(divide(X10,X11),multiply(inverse(inverse(X12)),inverse(X12))),X11) = X10]. % 1.62/2.02 [1404=demod(1381),[1403], % 1.62/2.02 divide(inverse(X10),divide(divide(X11,X12),X10)) = divide(X12,X11)]. % 1.62/2.02 [1409=demod(952),[1404,1], % 1.62/2.02 multiply(X10,divide(inverse(divide(X11,divide(X12,multiply(X10,X12)))),X13)) = divide(inverse(X11),X13)]. % 1.62/2.02 [1410=demod(647),[1409], % 1.62/2.02 multiply(X10,inverse(divide(inverse(divide(inverse(X11),divide(X12,X11))),X12))) = X10]. % 1.62/2.02 [1415=demod(115),[1409], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),X12),divide(inverse(X10),X12)) = X11]. % 1.62/2.02 [1421=demod(955),[1404,1], % 1.62/2.02 multiply(X10,multiply(inverse(divide(X11,divide(X12,multiply(X10,X12)))),X13)) = multiply(inverse(X11),X13)]. % 1.62/2.02 [1424=demod(240),[1421], % 1.62/2.02 divide(multiply(inverse(multiply(X10,X11)),X12),multiply(inverse(X10),X12)) = inverse(X11)]. % 1.62/2.02 [1430=demod(1089),[1404], % 1.62/2.02 divide(inverse(divide(divide(X10,X11),divide(X12,divide(X11,X10)))),X13) = inverse(inverse(divide(X12,X13)))]. % 1.62/2.02 [1431=demod(1345),[1430], % 1.62/2.02 inverse(inverse(divide(X10,multiply(inverse(inverse(X11)),inverse(X11))))) = X10]. % 1.62/2.02 [1432=demod(1220),[1404], % 1.62/2.02 divide(X10,multiply(divide(multiply(X11,X12),X13),divide(X13,X12))) = divide(inverse(inverse(X10)),X11)]. % 1.62/2.02 [1433=demod(1138),[1404], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(multiply(X11,X12),inverse(X12))) = divide(X10,X11)]. % 1.62/2.02 [1434=demod(1135),[1404], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(divide(X11,X12),X12)) = divide(X10,X11)]. % 1.62/2.02 [1435=demod(1137),[1434], % 1.62/2.02 divide(inverse(X12),divide(multiply(X11,X10),X12)) = divide(inverse(X10),X11)]. % 1.62/2.02 [1454=demod(1108),[1435], % 1.62/2.02 divide(inverse(divide(inverse(X10),X11)),multiply(divide(multiply(X12,X13),X13),X10)) = divide(inverse(inverse(X11)),X12)]. % 1.62/2.02 [1462=demod(934),[1404,1], % 1.62/2.02 multiply(divide(divide(X10,X11),X12),multiply(X12,X13)) = multiply(inverse(divide(X11,X10)),X13)]. % 1.62/2.02 [1479=demod(1014),[1462], % 1.62/2.02 multiply(X10,inverse(divide(inverse(divide(inverse(X11),multiply(multiply(inverse(divide(X11,X12)),X13),inverse(X13)))),X12))) = X10]. % 1.62/2.02 [1482=demod(568),[1462,1], % 1.62/2.02 multiply(inverse(multiply(X10,divide(divide(X11,multiply(X12,X11)),X13))),X10) = multiply(X13,X12)]. % 1.62/2.02 [1483=demod(885),[1462], % 1.62/2.02 multiply(multiply(multiply(X10,X11),inverse(X11)),multiply(inverse(X12),X13)) = multiply(inverse(divide(X12,X10)),X13)]. % 1.62/2.02 [1487=demod(1253),[1462], % 1.62/2.02 divide(multiply(inverse(inverse(X10)),inverse(X10)),multiply(inverse(divide(X11,X12)),divide(divide(X11,X12),X13))) = X13]. % 1.62/2.02 [1492=demod(942),[1404,1], % 1.62/2.02 multiply(divide(multiply(X10,X11),X12),multiply(X12,X13)) = multiply(inverse(divide(inverse(X11),X10)),X13)]. % 1.62/2.02 [1499=demod(337),[1492], % 1.62/2.02 multiply(inverse(divide(inverse(multiply(X10,X11)),multiply(multiply(X12,inverse(X13)),inverse(multiply(X10,X11))))),X13) = X12]. % 1.62/2.02 [1506=demod(940),[1404,1], % 1.62/2.02 multiply(multiply(divide(X10,X11),X12),multiply(inverse(X12),X13)) = multiply(inverse(divide(X11,X10)),X13)]. % 1.62/2.02 [1514=demod(1130),[1404], % 1.62/2.02 divide(divide(inverse(divide(X10,X11)),X12),X13) = divide(inverse(inverse(divide(X11,X10))),multiply(X13,X12))]. % 1.62/2.02 [1531=demod(601),[1514,1,570], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(divide(X11,X12),divide(X12,X11))) = X10]. % 1.62/2.02 [1535=demod(58),[1514,1], % 1.62/2.02 divide(inverse(inverse(multiply(X10,X11))),multiply(divide(inverse(X12),X13),multiply(multiply(X13,X12),X11))) = X10]. % 1.62/2.02 [1536=demod(938),[1514,1], % 1.62/2.02 divide(inverse(inverse(multiply(divide(X10,X11),X11))),multiply(divide(inverse(X12),X13),multiply(multiply(X13,X12),X14))) = divide(X10,X14)]. % 1.62/2.02 [1545=demod(1415),[1514,1434,1], % 1.62/2.02 multiply(divide(X10,X11),X11) = X10]. % 1.62/2.02 [1546=demod(1536),[1545], % 1.62/2.02 divide(inverse(inverse(X10)),multiply(divide(inverse(X11),X12),multiply(multiply(X12,X11),X13))) = divide(X10,X13)]. % 1.62/2.02 [1547=demod(1535),[1546], % 1.62/2.02 divide(multiply(X10,X11),X11) = X10]. % 1.62/2.02 [1549=demod(1454),[1547], % 1.62/2.02 divide(inverse(divide(inverse(X10),X11)),multiply(X12,X10)) = divide(inverse(inverse(X11)),X12)]. % 1.62/2.02 [1558=demod(1243),[1549,1431], % 1.62/2.02 divide(X10,multiply(inverse(X11),X11)) = X10]. % 1.62/2.02 [1560=demod(1431),[1558], % 1.62/2.02 inverse(inverse(X10)) = X10]. % 1.62/2.02 [1565=demod(1531),[1560], % 1.62/2.02 divide(X10,multiply(divide(X11,X12),divide(X12,X11))) = X10]. % 1.62/2.02 [1566=demod(916),[1565], % 1.62/2.02 inverse(divide(inverse(X10),divide(X11,X10))) = X11]. % 1.62/2.02 [1570=demod(945),[1566], % 1.62/2.02 divide(inverse(divide(X13,divide(X10,X12))),divide(X11,X13)) = divide(X10,multiply(X11,X12))]. % 1.62/2.02 [1573=demod(7),[1570], % 1.62/2.02 divide(X10,multiply(multiply(X11,X12),divide(inverse(X12),X11))) = X10]. % 1.62/2.02 [1589=demod(1410),[1566], % 1.62/2.02 multiply(X10,inverse(divide(X11,X11))) = X10]. % 1.62/2.02 [1594=demod(1487),[1560], % 1.62/2.02 divide(multiply(X10,inverse(X10)),multiply(inverse(divide(X11,X12)),divide(divide(X11,X12),X13))) = X13]. % 1.62/2.02 [1596=demod(1433),[1560], % 1.62/2.02 divide(X10,multiply(multiply(X11,X12),inverse(X12))) = divide(X10,X11)]. % 1.62/2.02 [1608=demod(1479),[1596,1], % 1.62/2.02 multiply(X10,inverse(divide(inverse(multiply(inverse(X11),divide(X11,X12))),X12))) = X10]. % 1.62/2.02 [1613=demod(897),[1596], % 1.62/2.02 multiply(multiply(divide(X10,X11),divide(divide(X11,X10),X12)),divide(X12,X13)) = inverse(X13)]. % 1.62/2.02 [1621=demod(1432),[1560], % 1.62/2.02 divide(X10,multiply(divide(multiply(X11,X12),X13),divide(X13,X12))) = divide(X10,X11)]. % 1.62/2.02 [1622=demod(1212),[1621,1545], % 1.62/2.02 divide(X10,divide(X11,multiply(X12,X11))) = multiply(X10,X12)]. % 1.62/2.02 [1653=demod(478),[1622], % 1.62/2.02 multiply(divide(X10,X11),multiply(divide(X11,X10),X12)) = X12]. % 1.62/2.02 [1654=demod(136),[1653], % 1.62/2.02 multiply(multiply(X11,X12),multiply(divide(inverse(X12),X11),X10)) = X10]. % 1.62/2.02 [1655=demod(138),[1654], % 1.62/2.02 multiply(divide(inverse(X11),X12),multiply(multiply(X12,X11),X10)) = X10]. % 1.62/2.02 [1656=demod(970),[1655], % 1.62/2.02 divide(inverse(X10),divide(X11,X10)) = multiply(inverse(multiply(X12,X11)),X12)]. % 1.62/2.02 [1666=demod(1397),[1560], % 1.62/2.02 multiply(multiply(X10,inverse(X10)),multiply(X11,X12)) = multiply(divide(X11,X13),multiply(X13,X12))]. % 1.62/2.02 [1690=demod(1172),[1560,1573], % 1.62/2.02 inverse(divide(X10,multiply(X11,X10))) = X11]. % 1.62/2.02 [1691=demod(1499),[1690], % 1.62/2.02 multiply(multiply(X10,inverse(X11)),X11) = X10]. % 1.62/2.02 [1692=demod(1049),[1691], % 1.62/2.02 multiply(multiply(X10,X11),multiply(inverse(X11),divide(inverse(multiply(X12,X13)),divide(inverse(X13),X12)))) = X10]. % 1.62/2.02 [1693=demod(1074),[1692], % 1.62/2.02 multiply(multiply(X10,X11),inverse(X11)) = X10]. % 1.62/2.02 [1694=demod(1219),[1693], % 1.62/2.02 multiply(divide(multiply(X10,X11),X12),divide(X12,X11)) = X10]. % 1.62/2.02 [1695=demod(1221),[1694], % 1.62/2.02 multiply(X10,divide(inverse(multiply(inverse(X11),X12)),multiply(inverse(X12),X11))) = X10]. % 1.62/2.02 [1700=demod(1187),[1695], % 1.62/2.02 multiply(multiply(multiply(X10,X11),divide(inverse(X11),X12)),X12) = X10]. % 1.62/2.02 [1701=demod(660),[1700], % 1.62/2.02 multiply(X10,divide(inverse(divide(X11,X12)),divide(X12,X11))) = X10]. % 1.62/2.02 [1702=demod(663),[1701], % 1.62/2.02 multiply(multiply(multiply(X10,X11),multiply(inverse(X11),X12)),inverse(X12)) = X10]. % 1.62/2.02 [1703=demod(1073),[1702], % 1.62/2.02 multiply(X10,divide(inverse(multiply(X11,X12)),divide(inverse(X12),X11))) = X10]. % 1.62/2.02 [1704=demod(1075),[1703,1], % 1.62/2.02 multiply(X10,inverse(divide(X11,X12))) = divide(multiply(X10,X12),X11)]. % 1.62/2.02 [1707=demod(1424),[-1704,-1704,1589,1560], % 1.62/2.02 multiply(inverse(multiply(X10,X11)),X10) = inverse(X11)]. % 1.62/2.02 [1710=demod(1482),[1707], % 1.62/2.02 inverse(divide(divide(X10,multiply(X11,X10)),X12)) = multiply(X12,X11)]. % 1.62/2.02 [1711=demod(505),[1710], % 1.62/2.02 multiply(divide(multiply(inverse(X10),X11),X12),multiply(multiply(X12,inverse(X11)),multiply(X10,X13))) = X13]. % 1.62/2.02 [1713=demod(1656),[1707], % 1.62/2.02 divide(inverse(X10),divide(X11,X10)) = inverse(X11)]. % 1.62/2.02 [1714=demod(951),[1713], % 1.62/2.02 multiply(inverse(X10),multiply(divide(X10,X11),X12)) = multiply(divide(inverse(X11),X13),multiply(X13,X12))]. % 1.62/2.02 [1716=demod(1404),[1713], % 1.62/2.02 inverse(divide(X10,X11)) = divide(X11,X10)]. % 1.62/2.02 [1750=demod(1608),[-1716,1,1560], % 1.62/2.02 multiply(X10,multiply(X11,multiply(inverse(X12),divide(X12,X11)))) = X10]. % 1.62/2.02 [1802=demod(1435),[1713], % 1.62/2.02 divide(inverse(X11),X10) = inverse(multiply(X10,X11))]. % 1.62/2.02 [1808=demod(19),[1802,1560], % 1.62/2.02 multiply(divide(divide(X10,multiply(divide(X11,X12),X13)),divide(X12,X11)),X13) = X10]. % 1.62/2.02 [1810=demod(25),[1802,1808], % 1.62/2.02 divide(X10,X11) = multiply(X10,inverse(X11))]. % 1.62/2.02 [1820=demod(84),[1810], % 1.62/2.02 multiply(multiply(X10,X11),multiply(inverse(X11),X12)) = multiply(multiply(X10,inverse(X13)),multiply(X13,X12))]. % 1.62/2.02 [1823=demod(1716),[1810,1810], % 1.62/2.02 inverse(multiply(X10,inverse(X11))) = multiply(X11,inverse(X10))]. % 1.62/2.02 [1826=demod(1653),[1810,1810], % 1.62/2.02 multiply(multiply(X10,inverse(X11)),multiply(multiply(X11,inverse(X10)),X12)) = X12]. % 1.62/2.02 [1828=demod(1506),[1810,1810], % 1.62/2.02 multiply(multiply(multiply(X10,inverse(X11)),X12),multiply(inverse(X12),X13)) = multiply(inverse(multiply(X11,inverse(X10))),X13)]. % 1.62/2.02 [1834=demod(1711),[1810], % 1.62/2.02 multiply(multiply(multiply(inverse(X10),X11),inverse(X12)),multiply(multiply(X12,inverse(X11)),multiply(X10,X13))) = X13]. % 1.62/2.02 [1841=demod(1613),[1810,1810,1810,1826,1810], % 1.62/2.02 multiply(inverse(X10),multiply(X10,inverse(X11))) = inverse(X11)]. % 1.62/2.02 [1849=demod(1666),[1810], % 1.62/2.02 multiply(multiply(X10,inverse(X10)),multiply(X11,X12)) = multiply(multiply(X11,inverse(X13)),multiply(X13,X12))]. % 1.62/2.02 [1865=demod(1594),[1810,1810,1810,1841,1810,1560], % 1.62/2.02 multiply(multiply(X10,inverse(X10)),X11) = X11]. % 1.62/2.02 [1867=demod(1849),[1865], % 1.62/2.02 multiply(multiply(X10,inverse(X12)),multiply(X12,X11)) = multiply(X10,X11)]. % 1.62/2.02 [1868=demod(1820),[1867], % 1.62/2.02 multiply(multiply(X10,X11),multiply(inverse(X11),X12)) = multiply(X10,X12)]. % 1.62/2.02 [1869=demod(1828),[1868], % 1.62/2.02 multiply(multiply(X10,inverse(X11)),X12) = multiply(inverse(multiply(X11,inverse(X10))),X12)]. % 1.62/2.02 [1899=demod(1750),[1810,1841], % 1.62/2.02 multiply(X10,multiply(X11,inverse(X11))) = X10]. % 1.62/2.02 [1912=demod(1704),[1810,1810], % 1.62/2.02 multiply(X10,inverse(multiply(X11,inverse(X12)))) = multiply(multiply(X10,X12),inverse(X11))]. % 1.62/2.02 [1958=demod(1492),[1810,1867,1810], % 1.62/2.02 multiply(multiply(X10,X11),X12) = multiply(inverse(multiply(inverse(X11),inverse(X10))),X12)]. % 1.62/2.02 [2008=demod(1714),[1810,1810,1867], % 1.62/2.02 multiply(inverse(X10),multiply(multiply(X10,inverse(X11)),X12)) = multiply(inverse(X11),X12)]. % 1.62/2.02 [2116=demod(1483),[-1912,1823,1899,1810], % 1.62/2.02 multiply(inverse(multiply(X11,inverse(X10))),X12) = multiply(X10,multiply(inverse(X11),X12))]. % 1.62/2.02 [2121=demod(1869),[2116], % 1.62/2.02 multiply(multiply(X10,inverse(X11)),X12) = multiply(X10,multiply(inverse(X11),X12))]. % 1.62/2.02 [2132=demod(2008),[2121], % 1.62/2.02 multiply(inverse(X10),multiply(X10,multiply(inverse(X11),X12))) = multiply(inverse(X11),X12)]. % 1.62/2.02 [2138=demod(1834),[2121,2121,2132,1868], % 1.62/2.02 multiply(inverse(X10),multiply(X10,X11)) = X11]. % 1.62/2.02 [2191=demod(1958),[2116,1560], % 1.62/2.02 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 1.62/2.02 [2332=param(4,1365),[2191,2138,3], % 1.62/2.02 thmtrue = thmfalse]. % 1.62/2.02 % SZS output end CNFRefutation % 1.62/2.02 Space: 4126 KB %------------------------------------------------------------------------------