%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP504-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n029.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:19 EDT 2022 % Result : Unsatisfiable 2.73s 3.12s % Output : CNFRefutation 2.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP504-1 : TPTP v8.1.0. Released v2.6.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 12:12:25 EDT 2022 % 0.12/0.33 % CPUTime : % 2.73/3.12 Theorem Proved. % 2.73/3.12 % SZS status Unsatisfiable % 2.73/3.12 % SZS output start CNFRefutation % 2.73/3.12 [1=axiom,[], % 2.73/3.12 inverse(double_divide(X11,X10)) = multiply(X10,X11)]. % 2.73/3.12 [2=axiom,[1,1], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),double_divide(inverse(X12),multiply(double_divide(X10,X13),X13))) = X11]. % 2.73/3.12 [3=axiom,[], % 2.73/3.12 thtop(X10,X10) = thmfalse]. % 2.73/3.12 [4=axiom,[], % 2.73/3.12 thtop(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) = thmtrue]. % 2.73/3.12 [5=param(1,2),[], % 2.73/3.12 multiply(double_divide(inverse(X11),multiply(double_divide(X12,X13),X13)),double_divide(X12,multiply(X10,X11))) = inverse(X10)]. % 2.73/3.12 [6=param(2,1),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X12,X13))),double_divide(multiply(X13,X12),multiply(double_divide(X10,X14),X14))) = X11]. % 2.73/3.12 [7=param(1,6),[], % 2.73/3.12 multiply(double_divide(multiply(X11,X12),multiply(double_divide(X13,X14),X14)),double_divide(X13,multiply(X10,double_divide(X12,X11)))) = inverse(X10)]. % 2.73/3.12 [8=param(2,2),[], % 2.73/3.12 double_divide(double_divide(double_divide(X10,multiply(X11,X12)),multiply(X13,X14)),double_divide(inverse(X14),multiply(X11,double_divide(inverse(X12),multiply(double_divide(X10,X15),X15))))) = X13]. % 2.73/3.12 [9=param(2,5),[1], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),double_divide(multiply(multiply(X11,X12),X13),multiply(double_divide(X10,X14),X14))) = double_divide(inverse(X12),multiply(double_divide(X13,X15),X15))]. % 2.73/3.12 [11=param(2,9),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),double_divide(double_divide(X13,inverse(X14)),double_divide(multiply(multiply(X14,X12),X10),multiply(double_divide(X13,X15),X15)))) = X11]. % 2.73/3.12 [13=param(11,1),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),double_divide(double_divide(X13,multiply(X14,X15)),double_divide(multiply(multiply(double_divide(X15,X14),X12),X10),multiply(double_divide(X13,X16),X16)))) = X11]. % 2.73/3.12 [15=param(8,5),[1], % 2.73/3.12 double_divide(double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(X12),X13),X13)),X12)),multiply(X14,X15)),double_divide(inverse(X15),multiply(X11,X10))) = X14]. % 2.73/3.12 [16=param(1,15),[], % 2.73/3.12 multiply(double_divide(inverse(X11),multiply(X12,X13)),double_divide(double_divide(X13,multiply(double_divide(inverse(X12),multiply(double_divide(inverse(X14),X15),X15)),X14)),multiply(X10,X11))) = inverse(X10)]. % 2.73/3.12 [17=param(6,2),[], % 2.73/3.12 double_divide(double_divide(double_divide(X10,multiply(X11,X12)),multiply(X13,double_divide(X14,X15))),double_divide(multiply(X15,X14),multiply(X11,double_divide(inverse(X12),multiply(double_divide(X10,X16),X16))))) = X13]. % 2.73/3.12 [19=param(2,7),[1], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),double_divide(multiply(multiply(X11,double_divide(X12,X13)),X14),multiply(double_divide(X10,X15),X15))) = double_divide(multiply(X13,X12),multiply(double_divide(X14,X16),X16))]. % 2.73/3.12 [22=param(9,1),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),double_divide(multiply(multiply(double_divide(X12,X11),X13),X14),multiply(double_divide(X10,X15),X15))) = double_divide(inverse(X13),multiply(double_divide(X14,X16),X16))]. % 2.73/3.12 [29=param(19,9),[1], % 2.73/3.12 double_divide(multiply(X10,X11),multiply(double_divide(X12,X13),X13)) = double_divide(multiply(X10,X11),multiply(double_divide(X12,X14),X14))]. % 2.73/3.12 [30=param(1,29),[1], % 2.73/3.12 multiply(multiply(double_divide(X10,X11),X11),multiply(X12,X13)) = multiply(multiply(double_divide(X10,X14),X14),multiply(X12,X13))]. % 2.73/3.12 [33=param(6,29),[], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),multiply(double_divide(X12,X13),X13)),double_divide(multiply(X14,X15),multiply(double_divide(multiply(X10,X11),X16),X16))) = double_divide(X12,double_divide(X15,X14))]. % 2.73/3.12 [34=param(13,29),[33], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),double_divide(X13,double_divide(X10,multiply(double_divide(X14,double_divide(X13,X14)),X12)))) = X11]. % 2.73/3.12 [35=param(22,29),[33], % 2.73/3.12 double_divide(X10,double_divide(X11,multiply(double_divide(X12,double_divide(X10,X12)),X13))) = double_divide(inverse(X13),multiply(double_divide(X11,X14),X14))]. % 2.73/3.12 [37=param(34,2),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(X11,double_divide(double_divide(X12,multiply(X13,X10)),X12))),X13) = X11]. % 2.73/3.12 [39=param(34,5),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),double_divide(X12,double_divide(X10,multiply(double_divide(X13,double_divide(X12,X13)),double_divide(X14,multiply(X11,X15)))))) = double_divide(inverse(X15),multiply(double_divide(X14,X16),X16))]. % 2.73/3.12 [40=param(34,6),[], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),multiply(X12,double_divide(double_divide(X13,multiply(X14,double_divide(X11,X10))),X13))),X14) = X12]. % 2.73/3.12 [47=param(1,37),[], % 2.73/3.12 multiply(X11,double_divide(inverse(X12),multiply(X10,double_divide(double_divide(X13,multiply(X11,X12)),X13)))) = inverse(X10)]. % 2.73/3.12 [50=param(37,5),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),inverse(X11)),X12) = double_divide(inverse(X13),multiply(double_divide(double_divide(multiply(X11,X13),multiply(X12,X10)),X14),X14))]. % 2.73/3.12 [53=param(37,7),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),inverse(X11)),X12) = double_divide(multiply(X13,X14),multiply(double_divide(double_divide(multiply(X11,double_divide(X14,X13)),multiply(X12,X10)),X15),X15))]. % 2.73/3.12 [58=param(37,16),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),inverse(X11)),double_divide(inverse(X12),multiply(double_divide(inverse(X10),X13),X13))) = double_divide(inverse(X14),multiply(X12,multiply(X11,X14)))]. % 2.73/3.12 [71=param(40,5),[], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),inverse(X12)),X13) = double_divide(inverse(X14),multiply(double_divide(double_divide(multiply(X12,X14),multiply(X13,double_divide(X11,X10))),X15),X15))]. % 2.73/3.12 [78=param(30,2),[], % 2.73/3.12 multiply(multiply(X10,double_divide(inverse(X11),multiply(double_divide(X12,X13),X13))),multiply(X14,X15)) = multiply(multiply(double_divide(double_divide(X12,multiply(X10,X11)),X16),X16),multiply(X14,X15))]. % 2.73/3.12 [79=param(2,30),[2], % 2.73/3.12 multiply(double_divide(X10,X11),X11) = multiply(double_divide(X10,X12),X12)]. % 2.73/3.12 [83=param(2,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),double_divide(inverse(X13),multiply(double_divide(X10,X14),X14))) = double_divide(X11,X13)]. % 2.73/3.12 [84=param(6,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),double_divide(multiply(X13,X14),multiply(double_divide(X10,X15),X15))) = double_divide(X11,double_divide(X14,X13))]. % 2.73/3.12 [89=param(11,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),double_divide(double_divide(X13,inverse(X14)),double_divide(multiply(multiply(X14,X15),X10),multiply(double_divide(X13,X16),X16)))) = double_divide(X11,X15)]. % 2.73/3.12 [94=param(34,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X12,X13))),double_divide(X12,double_divide(X10,multiply(double_divide(X13,X14),X14)))) = X11]. % 2.73/3.12 [106=param(1,94),[], % 2.73/3.12 multiply(double_divide(X11,double_divide(X12,multiply(double_divide(X13,X14),X14))),double_divide(X12,multiply(X10,double_divide(X11,X13)))) = inverse(X10)]. % 2.73/3.12 [123=param(1,83),[1], % 2.73/3.12 multiply(double_divide(inverse(X10),multiply(double_divide(X12,X13),X13)),double_divide(X12,multiply(double_divide(X11,X14),X14))) = multiply(X10,X11)]. % 2.73/3.12 [127=param(83,37),[], % 2.73/3.12 double_divide(X10,double_divide(double_divide(X12,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(X13),X14),X14)),X13)),X12)) = double_divide(X10,X11)]. % 2.73/3.12 [132=param(37,123),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(X11,X12)),X13) = double_divide(inverse(X11),multiply(double_divide(double_divide(multiply(double_divide(X12,X14),X14),multiply(X13,X10)),X15),X15))]. % 2.73/3.12 [133=param(40,123),[], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),multiply(X12,X13)),X14) = double_divide(inverse(X12),multiply(double_divide(double_divide(multiply(double_divide(X13,X15),X15),multiply(X14,double_divide(X11,X10))),X16),X16))]. % 2.73/3.12 [148=param(1,127),[1], % 2.73/3.12 multiply(double_divide(double_divide(X12,multiply(double_divide(inverse(X10),multiply(double_divide(inverse(X13),X14),X14)),X13)),X12),X11) = multiply(X10,X11)]. % 2.73/3.12 [152=param(2,148),[2], % 2.73/3.12 double_divide(double_divide(X11,multiply(double_divide(inverse(X10),multiply(double_divide(inverse(X12),X13),X13)),X12)),X11) = X10]. % 2.73/3.12 [154=param(152,1),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(multiply(X11,X12),multiply(double_divide(inverse(X13),X14),X14)),X13)),X10) = double_divide(X12,X11)]. % 2.73/3.12 [156=param(1,152),[], % 2.73/3.12 multiply(X11,double_divide(X11,multiply(double_divide(inverse(X10),multiply(double_divide(inverse(X12),X13),X13)),X12))) = inverse(X10)]. % 2.73/3.12 [159=param(8,152),[123], % 2.73/3.12 double_divide(X10,double_divide(inverse(X11),multiply(X10,multiply(X12,X11)))) = X12]. % 2.73/3.12 [161=param(17,152),[123], % 2.73/3.12 double_divide(X10,double_divide(multiply(X11,X12),multiply(X10,multiply(X13,double_divide(X12,X11))))) = X13]. % 2.73/3.12 [182=param(83,159),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(inverse(X12),multiply(X13,multiply(X11,X12))))),double_divide(inverse(X14),multiply(double_divide(X10,X15),X15))) = double_divide(X13,X14)]. % 2.73/3.12 [188=param(35,2),[1], % 2.73/3.12 double_divide(multiply(X10,double_divide(X10,multiply(X11,X12))),multiply(double_divide(inverse(X12),X13),X13)) = X11]. % 2.73/3.12 [200=param(35,79),[1], % 2.73/3.12 double_divide(X10,double_divide(X11,multiply(double_divide(X12,X13),X13))) = double_divide(multiply(X12,X10),multiply(double_divide(X11,X14),X14))]. % 2.73/3.12 [220=param(1,161),[], % 2.73/3.12 multiply(double_divide(multiply(X11,X12),multiply(X13,multiply(X10,double_divide(X12,X11)))),X13) = inverse(X10)]. % 2.73/3.12 [245=param(1,188),[], % 2.73/3.12 multiply(multiply(double_divide(inverse(X11),X12),X12),multiply(X13,double_divide(X13,multiply(X10,X11)))) = inverse(X10)]. % 2.73/3.12 [254=param(22,188),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(X11,X12)),X13) = double_divide(inverse(X14),multiply(double_divide(double_divide(multiply(double_divide(X12,X11),X14),multiply(X13,X10)),X15),X15))]. % 2.73/3.12 [284=param(39,47),[1,188], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),double_divide(X12,double_divide(X10,inverse(X11)))) = double_divide(X13,double_divide(X12,X13))]. % 2.73/3.12 [286=param(39,106),[1], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),double_divide(X12,double_divide(X10,inverse(X11)))) = double_divide(multiply(X13,multiply(double_divide(X13,X14),X14)),multiply(double_divide(X12,X15),X15))]. % 2.73/3.12 [293=param(159,245),[1], % 2.73/3.12 double_divide(multiply(double_divide(inverse(X10),X11),X11),double_divide(multiply(multiply(X12,X10),X13),inverse(X12))) = X13]. % 2.73/3.12 [296=param(1,293),[], % 2.73/3.12 multiply(double_divide(multiply(multiply(X11,X12),X10),inverse(X11)),multiply(double_divide(inverse(X12),X13),X13)) = inverse(X10)]. % 2.73/3.12 [397=param(284,37),[37], % 2.73/3.12 double_divide(X10,double_divide(X11,X10)) = double_divide(X12,double_divide(X11,X12))]. % 2.73/3.12 [449=param(397,159),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(X11,multiply(X12,X10))),X12) = double_divide(X13,double_divide(X11,X13))]. % 2.73/3.12 [458=param(397,397),[], % 2.73/3.12 double_divide(double_divide(X10,X11),double_divide(X12,double_divide(X10,X12))) = double_divide(X13,double_divide(X11,X13))]. % 2.73/3.12 [459=param(1,458),[1], % 2.73/3.12 multiply(double_divide(X10,X11),X11) = multiply(double_divide(X12,double_divide(X13,X12)),double_divide(X13,X10))]. % 2.73/3.12 [468=param(458,94),[], % 2.73/3.12 double_divide(X10,double_divide(multiply(X11,double_divide(multiply(double_divide(X12,X13),X13),X12)),X10)) = X11]. % 2.73/3.12 [490=param(1,468),[], % 2.73/3.12 multiply(double_divide(multiply(X10,double_divide(multiply(double_divide(X11,X12),X12),X11)),X13),X13) = inverse(X10)]. % 2.73/3.12 [546=param(490,459),[], % 2.73/3.12 multiply(double_divide(X11,double_divide(X12,X11)),double_divide(X12,multiply(X10,double_divide(multiply(double_divide(X13,X14),X14),X13)))) = inverse(X10)]. % 2.73/3.12 [547=param(1,449),[1], % 2.73/3.12 multiply(double_divide(X10,X11),X11) = multiply(X12,double_divide(inverse(X13),multiply(X10,multiply(X12,X13))))]. % 2.73/3.12 [616=param(547,123),[], % 2.73/3.12 multiply(double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(X12),X13),X13)),X12)),X14),X14) = multiply(X11,X10)]. % 2.73/3.12 [618=param(188,547),[], % 2.73/3.12 double_divide(multiply(double_divide(X10,X11),X11),multiply(double_divide(inverse(multiply(inverse(X12),X12)),X13),X13)) = X10]. % 2.73/3.12 [623=param(1,618),[], % 2.73/3.12 multiply(multiply(double_divide(inverse(multiply(inverse(X11),X11)),X12),X12),multiply(double_divide(X10,X13),X13)) = inverse(X10)]. % 2.73/3.12 [624=param(2,618),[], % 2.73/3.12 double_divide(X10,double_divide(inverse(X11),multiply(double_divide(multiply(double_divide(X10,X12),X12),X13),X13))) = double_divide(inverse(multiply(inverse(X14),X14)),X11)]. % 2.73/3.12 [627=param(6,618),[], % 2.73/3.12 double_divide(double_divide(inverse(multiply(inverse(X10),X10)),multiply(X11,double_divide(X12,double_divide(X13,X12)))),X13) = X11]. % 2.73/3.12 [682=param(627,152),[1], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(multiply(double_divide(inverse(multiply(inverse(X11),X11)),X12),X12),X13),X13)) = X10]. % 2.73/3.12 [711=param(161,623),[], % 2.73/3.12 double_divide(multiply(double_divide(inverse(multiply(inverse(X10),X10)),X11),X11),double_divide(multiply(X12,X13),inverse(X14))) = double_divide(X14,double_divide(X13,X12))]. % 2.73/3.12 [727=param(161,296),[], % 2.73/3.12 double_divide(double_divide(multiply(multiply(X10,X11),X12),inverse(X10)),double_divide(multiply(X13,X14),inverse(X12))) = double_divide(inverse(X11),double_divide(X14,X13))]. % 2.73/3.12 [760=param(293,156),[], % 2.73/3.12 double_divide(multiply(double_divide(inverse(X10),X11),X11),double_divide(inverse(X12),inverse(X13))) = double_divide(multiply(X13,X10),multiply(double_divide(inverse(X12),multiply(double_divide(inverse(X14),X15),X15)),X14))]. % 2.73/3.12 [766=param(2,682),[], % 2.73/3.12 double_divide(double_divide(multiply(double_divide(inverse(multiply(inverse(X10),X10)),X11),X11),multiply(X12,X13)),X13) = X12]. % 2.73/3.12 [819=param(766,152),[], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(inverse(multiply(double_divide(inverse(multiply(inverse(X11),X11)),X12),X12)),X13),X13)) = X10]. % 2.73/3.12 [835=param(766,618),[], % 2.73/3.12 double_divide(inverse(multiply(inverse(X10),X10)),X11) = double_divide(inverse(multiply(inverse(X12),X12)),X11)]. % 2.73/3.12 [839=param(1,835),[1], % 2.73/3.12 multiply(X10,inverse(multiply(inverse(X11),X11))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 2.73/3.12 [856=param(83,835),[83], % 2.73/3.12 double_divide(X10,multiply(inverse(X11),X11)) = double_divide(X10,multiply(inverse(X12),X12))]. % 2.73/3.12 [861=param(152,835),[152], % 2.73/3.12 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 2.73/3.12 [883=param(6,861),[1], % 2.73/3.12 double_divide(double_divide(X10,multiply(inverse(X11),X11)),double_divide(multiply(X12,X13),multiply(double_divide(X10,X14),X14))) = multiply(X12,X13)]. % 2.73/3.12 [891=param(13,861),[883], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,X12)),multiply(multiply(double_divide(X13,inverse(X13)),X12),X10)) = X11]. % 2.73/3.12 [912=param(159,861),[], % 2.73/3.12 double_divide(inverse(multiply(X10,X11)),double_divide(inverse(X11),multiply(inverse(X12),X12))) = X10]. % 2.73/3.12 [913=param(161,861),[], % 2.73/3.12 double_divide(X10,double_divide(multiply(inverse(X11),X11),multiply(X10,multiply(X12,double_divide(X13,inverse(X13)))))) = X12]. % 2.73/3.12 [920=param(1,856),[1], % 2.73/3.12 multiply(multiply(inverse(X10),X10),X11) = multiply(multiply(inverse(X12),X12),X11)]. % 2.73/3.12 [934=param(856,152),[], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(double_divide(inverse(X11),multiply(double_divide(inverse(X12),X13),X13)),X12)),multiply(inverse(X14),X14)) = X11]. % 2.73/3.12 [947=param(58,53),[616], % 2.73/3.12 double_divide(inverse(X10),multiply(X11,multiply(X12,X10))) = double_divide(multiply(X13,X14),multiply(X11,multiply(X12,double_divide(X14,X13))))]. % 2.73/3.12 [1007=param(152,839),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(inverse(multiply(inverse(X12),X12))),X13),X13)),inverse(multiply(inverse(X14),X14)))),X10) = X11]. % 2.73/3.12 [1093=param(891,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,inverse(X12))),multiply(multiply(double_divide(X12,X13),X13),X10)) = X11]. % 2.73/3.12 [1110=param(891,220),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),multiply(multiply(double_divide(X12,inverse(X12)),X13),X10)) = double_divide(multiply(X14,X15),multiply(X13,multiply(X11,double_divide(X15,X14))))]. % 2.73/3.12 [1126=param(891,547),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(inverse(X12),multiply(X13,multiply(X11,X12))))),multiply(multiply(double_divide(X14,inverse(X14)),X15),X10)) = double_divide(X13,X15)]. % 2.73/3.12 [1155=param(1,1093),[], % 2.73/3.12 multiply(multiply(multiply(double_divide(X11,X12),X12),X13),double_divide(X13,multiply(X10,inverse(X11)))) = inverse(X10)]. % 2.73/3.12 [1183=param(1093,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),multiply(multiply(double_divide(X13,X14),X14),X10)) = double_divide(X11,inverse(X13))]. % 2.73/3.12 [1236=param(1093,856),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(inverse(X11),X11)),multiply(multiply(double_divide(X12,X13),X13),X10)) = inverse(inverse(X12))]. % 2.73/3.12 [1256=param(293,1155),[], % 2.73/3.12 double_divide(multiply(double_divide(inverse(X10),X11),X11),double_divide(inverse(X12),inverse(multiply(double_divide(X13,X14),X14)))) = double_divide(X10,multiply(X12,inverse(X13)))]. % 2.73/3.12 [1299=param(1236,37),[1], % 2.73/3.12 multiply(X11,double_divide(X11,multiply(multiply(multiply(double_divide(X10,X12),X12),inverse(X13)),X13))) = inverse(inverse(X10))]. % 2.73/3.12 [1359=param(1236,835),[1236], % 2.73/3.12 inverse(inverse(inverse(multiply(inverse(X10),X10)))) = inverse(inverse(inverse(multiply(inverse(X11),X11))))]. % 2.73/3.12 [1383=param(152,1359),[152], % 2.73/3.12 inverse(inverse(multiply(inverse(X10),X10))) = inverse(inverse(multiply(inverse(X11),X11)))]. % 2.73/3.12 [1384=param(152,1359),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(inverse(inverse(multiply(inverse(X12),X12)))),X13),X13)),inverse(inverse(multiply(inverse(X14),X14))))),X10) = X11]. % 2.73/3.12 [1394=param(83,1383),[83], % 2.73/3.12 double_divide(X10,inverse(multiply(inverse(X11),X11))) = double_divide(X10,inverse(multiply(inverse(X12),X12)))]. % 2.73/3.12 [1404=param(1,1394),[1], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),X11) = multiply(inverse(multiply(inverse(X12),X12)),X11)]. % 2.73/3.12 [1417=param(1404,547),[], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),double_divide(inverse(X11),multiply(X12,multiply(inverse(multiply(inverse(X13),X13)),X11)))) = multiply(double_divide(X12,X14),X14)]. % 2.73/3.12 [1420=param(1404,861),[], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 2.73/3.12 [1473=param(293,1299),[], % 2.73/3.12 double_divide(multiply(double_divide(inverse(X10),X11),X11),double_divide(inverse(inverse(X12)),inverse(X13))) = double_divide(multiply(X13,X10),multiply(multiply(multiply(double_divide(X12,X14),X14),inverse(X15)),X15))]. % 2.73/3.12 [1530=param(913,296),[727], % 2.73/3.12 double_divide(inverse(X10),double_divide(X11,inverse(X11))) = double_divide(inverse(X10),double_divide(X12,inverse(X12)))]. % 2.73/3.12 [1557=param(1530,397),[], % 2.73/3.12 double_divide(inverse(X10),double_divide(X11,inverse(X11))) = double_divide(X12,double_divide(X10,X12))]. % 2.73/3.12 [1581=param(1,1557),[1], % 2.73/3.12 multiply(double_divide(X10,X11),X11) = multiply(double_divide(X12,inverse(X12)),inverse(X10))]. % 2.73/3.12 [1617=param(2,1581),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,inverse(X11)),inverse(X12))),double_divide(inverse(X13),multiply(double_divide(X10,X14),X14))) = double_divide(X12,X13)]. % 2.73/3.12 [1663=param(2,1581),[83], % 2.73/3.12 double_divide(X10,inverse(X10)) = double_divide(X11,inverse(X11))]. % 2.73/3.12 [1682=param(50,1663),[-50], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),X11) = double_divide(double_divide(inverse(X12),inverse(inverse(X12))),X11)]. % 2.73/3.12 [1693=param(71,1663),[-71], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),X11) = double_divide(double_divide(multiply(X12,X13),inverse(multiply(X12,X13))),X11)]. % 2.73/3.12 [1699=param(1663,1394),[], % 2.73/3.12 double_divide(X10,inverse(X10)) = double_divide(multiply(inverse(X11),X11),inverse(multiply(inverse(X12),X12)))]. % 2.73/3.12 [1728=param(83,1699),[1617], % 2.73/3.12 double_divide(multiply(inverse(X10),X10),X11) = double_divide(multiply(inverse(X12),X12),X11)]. % 2.73/3.12 [1750=param(1,1728),[1], % 2.73/3.12 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,multiply(inverse(X12),X12))]. % 2.73/3.12 [1788=param(293,1750),[711], % 2.73/3.12 double_divide(X10,double_divide(X11,multiply(X10,multiply(inverse(X12),X12)))) = X11]. % 2.73/3.12 [1801=param(1788,1),[], % 2.73/3.12 double_divide(X10,double_divide(X11,multiply(X10,multiply(multiply(X12,X13),double_divide(X13,X12))))) = X11]. % 2.73/3.12 [1817=param(1788,79),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(inverse(X11),X11)),double_divide(X12,multiply(double_divide(X10,X13),X13))) = X12]. % 2.73/3.12 [1822=param(94,1788),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(double_divide(X12,multiply(inverse(X13),X13)),X12))),X10) = X11]. % 2.73/3.12 [1840=param(1788,856),[], % 2.73/3.12 double_divide(inverse(multiply(inverse(X10),X10)),double_divide(X11,multiply(inverse(X12),X12))) = X11]. % 2.73/3.12 [1842=param(1788,920),[], % 2.73/3.12 double_divide(multiply(inverse(X10),X10),double_divide(X11,multiply(multiply(inverse(X12),X12),multiply(inverse(X13),X13)))) = X11]. % 2.73/3.12 [1844=param(1788,1093),[], % 2.73/3.12 double_divide(multiply(double_divide(X10,X11),X11),X12) = double_divide(multiply(inverse(X13),X13),multiply(X12,inverse(X10)))]. % 2.73/3.12 [1884=param(1,1840),[], % 2.73/3.12 multiply(double_divide(X10,multiply(inverse(X11),X11)),inverse(multiply(inverse(X12),X12))) = inverse(X10)]. % 2.73/3.12 [1901=param(152,1840),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(X12,double_divide(X12,multiply(inverse(X13),X13)))),multiply(inverse(X14),X14))),X10) = X11]. % 2.73/3.12 [1906=param(618,1840),[], % 2.73/3.12 double_divide(multiply(double_divide(X10,X11),X11),multiply(X12,double_divide(X12,multiply(inverse(X13),X13)))) = X10]. % 2.73/3.12 [1967=param(1,1801),[], % 2.73/3.12 multiply(double_divide(X10,multiply(X11,multiply(multiply(X12,X13),double_divide(X13,X12)))),X11) = inverse(X10)]. % 2.73/3.12 [1987=param(83,1801),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X11,multiply(X12,multiply(multiply(X13,X14),double_divide(X14,X13)))))),double_divide(inverse(X15),multiply(double_divide(X10,X16),X16))) = double_divide(X12,X15)]. % 2.73/3.12 [1996=param(1801,188),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(multiply(X11,X12),double_divide(X12,X11))),X13) = multiply(X14,double_divide(X14,multiply(X13,X10)))]. % 2.73/3.12 [2014=param(1801,835),[], % 2.73/3.12 double_divide(inverse(multiply(inverse(X11),X11)),double_divide(X10,multiply(inverse(multiply(inverse(X12),X12)),multiply(multiply(X13,X14),double_divide(X14,X13))))) = X10]. % 2.73/3.12 [2034=param(1,1682),[1], % 2.73/3.12 multiply(X10,double_divide(inverse(X11),inverse(inverse(X11)))) = multiply(X10,double_divide(X12,inverse(X12)))]. % 2.73/3.12 [2103=param(2,78),[2], % 2.73/3.12 multiply(double_divide(double_divide(X10,multiply(X11,X12)),X13),X13) = multiply(X11,double_divide(inverse(X12),multiply(double_divide(X10,X14),X14)))]. % 2.73/3.12 [2109=param(78,1155),[1], % 2.73/3.12 multiply(multiply(double_divide(double_divide(X11,multiply(multiply(multiply(double_divide(X10,X14),X14),inverse(X15)),X15)),X16),X16),multiply(X12,X13)) = multiply(multiply(inverse(X10),X11),multiply(X12,X13))]. % 2.73/3.12 [2314=param(891,1967),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),multiply(multiply(double_divide(X12,inverse(X12)),X13),X10)) = double_divide(X11,multiply(X13,multiply(multiply(X14,X15),double_divide(X15,X14))))]. % 2.73/3.12 [2316=param(1093,1967),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),multiply(multiply(double_divide(X12,X13),X13),X10)) = double_divide(X11,multiply(inverse(X12),multiply(multiply(X14,X15),double_divide(X15,X14))))]. % 2.73/3.12 [2325=param(1906,2),[], % 2.73/3.12 double_divide(multiply(X10,double_divide(inverse(X11),multiply(double_divide(X12,X13),X13))),multiply(X14,double_divide(X14,multiply(inverse(X15),X15)))) = double_divide(X12,multiply(X10,X11))]. % 2.73/3.12 [2356=param(1906,83),[2325], % 2.73/3.12 double_divide(X10,multiply(double_divide(X11,X12),X12)) = double_divide(X10,multiply(double_divide(X11,X13),X13))]. % 2.73/3.12 [2360=param(94,1906),[], % 2.73/3.12 double_divide(X10,double_divide(X11,double_divide(multiply(double_divide(X10,X12),X12),multiply(double_divide(multiply(inverse(X13),X13),X14),X14)))) = X11]. % 2.73/3.12 [2385=param(1906,490),[], % 2.73/3.12 double_divide(inverse(X10),multiply(X11,double_divide(X11,multiply(inverse(X12),X12)))) = multiply(X10,double_divide(multiply(double_divide(X13,X14),X14),X13))]. % 2.73/3.12 [2430=param(84,79),[84], % 2.73/3.12 double_divide(X10,double_divide(X11,double_divide(X12,X11))) = double_divide(X10,double_divide(X13,double_divide(X12,X13)))]. % 2.73/3.12 [2445=param(84,861),[84], % 2.73/3.12 double_divide(X10,double_divide(X11,inverse(X11))) = double_divide(X10,double_divide(X12,inverse(X12)))]. % 2.73/3.12 [2449=param(84,1420),[84], % 2.73/3.12 double_divide(X10,double_divide(X11,inverse(X11))) = double_divide(X10,double_divide(multiply(inverse(X12),X12),inverse(multiply(inverse(X13),X13))))]. % 2.73/3.12 [2456=param(84,1581),[84], % 2.73/3.12 double_divide(X10,double_divide(inverse(X11),double_divide(X12,inverse(X12)))) = double_divide(X10,double_divide(X13,double_divide(X11,X13)))]. % 2.73/3.12 [2457=param(84,1728),[], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(double_divide(X11,X12),X12)),double_divide(multiply(X13,X14),multiply(double_divide(multiply(inverse(X15),X15),X16),X16))) = double_divide(X11,double_divide(X14,X13))]. % 2.73/3.12 [2466=param(1,2445),[1], % 2.73/3.12 multiply(double_divide(X10,inverse(X10)),X11) = multiply(double_divide(X12,inverse(X12)),X11)]. % 2.73/3.12 [2469=param(2445,50),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),inverse(X11)),double_divide(X12,inverse(X12))) = double_divide(inverse(X13),multiply(double_divide(double_divide(multiply(X11,X13),multiply(double_divide(X14,inverse(X14)),X10)),X15),X15))]. % 2.73/3.12 [2585=param(2430,835),[], % 2.73/3.12 double_divide(X10,double_divide(inverse(multiply(inverse(X11),X11)),double_divide(X12,inverse(multiply(inverse(X13),X13))))) = double_divide(X10,double_divide(X14,double_divide(X12,X14)))]. % 2.73/3.12 [2653=param(1,2356),[1], % 2.73/3.12 multiply(multiply(double_divide(X10,X11),X11),X12) = multiply(multiply(double_divide(X10,X13),X13),X12)]. % 2.73/3.12 [2832=param(1822,37),[1], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,multiply(X12,double_divide(X12,multiply(inverse(X13),X13))))),X10) = X11]. % 2.73/3.12 [2907=param(1801,1822),[], % 2.73/3.12 double_divide(multiply(X10,multiply(multiply(X12,X13),double_divide(X13,X12))),multiply(X11,double_divide(double_divide(X14,multiply(inverse(X15),X15)),X14))) = double_divide(X10,X11)]. % 2.73/3.12 [2966=param(2832,245),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(inverse(X11))),X10) = multiply(double_divide(inverse(X11),X12),X12)]. % 2.73/3.12 [2976=param(2832,682),[1906], % 2.73/3.12 double_divide(X10,inverse(X10)) = inverse(multiply(inverse(X11),X11))]. % 2.73/3.12 [3025=param(1,2976),[], % 2.73/3.12 inverse(inverse(multiply(inverse(X10),X10))) = multiply(inverse(X11),X11)]. % 2.73/3.12 [3061=param(397,2976),[], % 2.73/3.12 double_divide(inverse(X10),inverse(multiply(inverse(X11),X11))) = double_divide(X12,double_divide(X10,X12))]. % 2.73/3.12 [3069=param(1530,2976),[], % 2.73/3.12 double_divide(inverse(X10),inverse(multiply(inverse(X11),X11))) = double_divide(inverse(X10),double_divide(X12,inverse(X12)))]. % 2.73/3.12 [3073=param(2034,2976),[], % 2.73/3.12 multiply(X10,inverse(multiply(inverse(X11),X11))) = multiply(X10,double_divide(X12,inverse(X12)))]. % 2.73/3.12 [3076=param(2445,2976),[], % 2.73/3.12 double_divide(X10,inverse(multiply(inverse(X11),X11))) = double_divide(X10,double_divide(X12,inverse(X12)))]. % 2.73/3.12 [3077=param(2466,2976),[], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),X11) = multiply(double_divide(X12,inverse(X12)),X11)]. % 2.73/3.12 [3100=param(1359,2976),[1], % 2.73/3.12 inverse(multiply(inverse(X10),X10)) = inverse(inverse(inverse(multiply(inverse(X11),X11))))]. % 2.73/3.12 [3105=param(1840,2976),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),double_divide(X11,multiply(inverse(X12),X12))) = X11]. % 2.73/3.12 [3107=param(1840,2976),[], % 2.73/3.12 double_divide(inverse(multiply(inverse(X10),X10)),double_divide(X11,multiply(double_divide(X12,inverse(X12)),multiply(inverse(X13),X13)))) = X11]. % 2.73/3.12 [3109=param(1884,2976),[], % 2.73/3.12 multiply(double_divide(X10,multiply(inverse(X11),X11)),double_divide(X12,inverse(X12))) = inverse(X10)]. % 2.73/3.12 [3121=param(58,3025),[1817], % 2.73/3.12 double_divide(inverse(X11),multiply(X10,multiply(inverse(multiply(inverse(X12),X12)),X11))) = inverse(X10)]. % 2.73/3.12 [3122=demod(1417),[3121], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),inverse(X11)) = multiply(double_divide(X11,X12),X12)]. % 2.73/3.12 [3125=param(152,3025),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(multiply(inverse(X12),X12),X13),X13)),inverse(multiply(inverse(X14),X14)))),X10) = X11]. % 2.73/3.12 [3133=param(912,3025),[], % 2.73/3.12 double_divide(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),double_divide(multiply(inverse(X12),X12),multiply(inverse(X13),X13))) = X10]. % 2.73/3.12 [3147=param(6,3025),[1], % 2.73/3.12 double_divide(double_divide(X10,inverse(inverse(multiply(inverse(X11),X11)))),double_divide(multiply(X12,X13),multiply(double_divide(X10,X14),X14))) = multiply(X12,X13)]. % 2.73/3.12 [3183=param(1840,3025),[], % 2.73/3.12 double_divide(inverse(inverse(inverse(multiply(inverse(X10),X10)))),double_divide(X11,multiply(inverse(X12),X12))) = X11]. % 2.73/3.12 [3197=param(89,1383),[3147], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),multiply(multiply(inverse(multiply(inverse(X13),X13)),X14),X10)) = double_divide(X11,X14)]. % 2.73/3.12 [3255=param(152,3100),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(inverse(inverse(multiply(inverse(X12),X12)))),X13),X13)),multiply(inverse(X14),X14))),X10) = X11]. % 2.73/3.12 [3269=param(1394,3100),[], % 2.73/3.12 double_divide(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = double_divide(X10,inverse(multiply(inverse(X12),X12)))]. % 2.73/3.12 [3284=param(3100,2976),[], % 2.73/3.12 inverse(inverse(inverse(multiply(inverse(X10),X10)))) = double_divide(X11,inverse(X11))]. % 2.73/3.12 [3318=param(152,3284),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(double_divide(X12,inverse(X12)),X13),X13)),inverse(inverse(multiply(inverse(X14),X14))))),X10) = X11]. % 2.73/3.12 [3341=param(1,3284),[], % 2.73/3.12 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = multiply(inverse(X11),X11)]. % 2.73/3.12 [3380=param(1530,3284),[], % 2.73/3.12 double_divide(inverse(X10),inverse(inverse(inverse(multiply(inverse(X11),X11))))) = double_divide(inverse(X10),double_divide(X12,inverse(X12)))]. % 2.73/3.12 [3384=param(2034,3284),[], % 2.73/3.12 multiply(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = multiply(X10,double_divide(X12,inverse(X12)))]. % 2.73/3.12 [3408=param(912,3341),[], % 2.73/3.12 double_divide(inverse(multiply(X10,inverse(inverse(inverse(multiply(inverse(X11),X11)))))),double_divide(multiply(inverse(X12),X12),multiply(inverse(X13),X13))) = X10]. % 2.73/3.12 [3619=param(1093,3122),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(inverse(multiply(inverse(X11),X11)),inverse(X12))),multiply(multiply(double_divide(X13,X14),X14),X10)) = double_divide(X12,inverse(X13))]. % 2.73/3.12 [3644=param(3077,861),[], % 2.73/3.12 multiply(double_divide(X10,inverse(X10)),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 2.73/3.12 [3673=param(3077,1299),[], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),double_divide(double_divide(X11,inverse(X11)),multiply(multiply(multiply(double_divide(X12,X13),X13),inverse(X14)),X14))) = inverse(inverse(X12))]. % 2.73/3.12 [3739=param(40,3644),[1], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),multiply(double_divide(X12,inverse(X12)),multiply(inverse(X13),X13))),X14) = multiply(X15,double_divide(X15,multiply(X14,double_divide(X11,X10))))]. % 2.73/3.12 [3740=param(78,3644),[1,2109], % 2.73/3.12 multiply(multiply(double_divide(X10,inverse(X10)),multiply(inverse(X11),X11)),multiply(X12,X13)) = multiply(multiply(inverse(X14),X14),multiply(X12,X13))]. % 2.73/3.12 [3972=param(152,3073),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(inverse(multiply(inverse(X12),X12))),X13),X13)),double_divide(X14,inverse(X14)))),X10) = X11]. % 2.73/3.12 [4023=param(3073,459),[], % 2.73/3.12 multiply(double_divide(X10,double_divide(X11,inverse(X11))),inverse(multiply(inverse(X12),X12))) = multiply(double_divide(X13,double_divide(X14,X13)),double_divide(X14,X10))]. % 2.73/3.12 [4039=param(3073,3122),[], % 2.73/3.12 multiply(double_divide(X10,double_divide(X11,inverse(X11))),inverse(multiply(inverse(X12),X12))) = multiply(inverse(multiply(inverse(X13),X13)),inverse(X10))]. % 2.73/3.12 [4084=param(83,3061),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),inverse(multiply(inverse(X12),X12))),double_divide(X11,X13))),double_divide(inverse(X14),multiply(double_divide(X10,X15),X15))) = double_divide(X13,X14)]. % 2.73/3.12 [4154=param(2966,1663),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),inverse(X11)) = multiply(double_divide(inverse(X11),X12),X12)]. % 2.73/3.12 [4185=param(2966,3284),[], % 2.73/3.12 double_divide(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(X11)) = multiply(double_divide(inverse(X11),X12),X12)]. % 2.73/3.12 [4269=param(1530,4154),[1], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(multiply(inverse(X11),X11),X12),X12)) = double_divide(inverse(X10),double_divide(X13,inverse(X13)))]. % 2.73/3.12 [4270=param(4154,1663),[1], % 2.73/3.12 multiply(double_divide(multiply(inverse(X10),X10),X11),X11) = double_divide(X12,inverse(X12))]. % 2.73/3.12 [4303=param(83,4154),[], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(double_divide(X11,X12),X12)),double_divide(inverse(X13),double_divide(double_divide(X14,inverse(X14)),inverse(X10)))) = double_divide(X11,X13)]. % 2.73/3.12 [4309=param(152,4154),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),double_divide(double_divide(X12,inverse(X12)),inverse(X13))),X13)),X10) = X11]. % 2.73/3.12 [4365=param(83,4270),[], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(double_divide(X11,X12),X12)),double_divide(inverse(X13),double_divide(X14,inverse(X14)))) = double_divide(X11,X13)]. % 2.73/3.12 [4379=param(4270,490),[1], % 2.73/3.12 double_divide(X10,inverse(X10)) = inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))]. % 2.73/3.12 [4389=param(1093,4270),[], % 2.73/3.12 double_divide(double_divide(X10,double_divide(X11,inverse(X11))),multiply(multiply(double_divide(X12,X13),X13),X10)) = double_divide(multiply(inverse(X14),X14),inverse(X12))]. % 2.73/3.12 [4394=param(1801,4270),[], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(multiply(X11,X12),double_divide(X12,X11))),double_divide(X13,double_divide(X14,inverse(X14)))) = X13]. % 2.73/3.12 [4465=param(71,4379),[-71], % 2.73/3.12 double_divide(inverse(multiply(X10,multiply(double_divide(X10,X11),X11))),X12) = double_divide(double_divide(multiply(X13,X14),inverse(multiply(X13,X14))),X12)]. % 2.73/3.12 [4497=param(2445,4379),[], % 2.73/3.12 double_divide(X10,inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))) = double_divide(X10,double_divide(X13,inverse(X13)))]. % 2.73/3.12 [4499=param(2653,4379),[], % 2.73/3.12 multiply(multiply(inverse(multiply(X10,multiply(double_divide(X10,X11),X11))),inverse(X12)),X13) = multiply(multiply(double_divide(X12,X14),X14),X13)]. % 2.73/3.12 [4501=param(4379,2976),[], % 2.73/3.12 inverse(multiply(X10,multiply(double_divide(X10,X11),X11))) = inverse(multiply(inverse(X12),X12))]. % 2.73/3.12 [4503=param(3076,4379),[], % 2.73/3.12 double_divide(X10,inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))) = double_divide(X10,inverse(multiply(inverse(X13),X13)))]. % 2.73/3.12 [4505=param(3109,4379),[], % 2.73/3.12 multiply(double_divide(X10,multiply(inverse(X11),X11)),inverse(multiply(X12,multiply(double_divide(X12,X13),X13)))) = inverse(X10)]. % 2.73/3.12 [4513=param(152,4379),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(double_divide(X12,inverse(X12)),X13),X13)),multiply(X14,multiply(double_divide(X14,X15),X15)))),X10) = X11]. % 2.73/3.12 [4539=param(152,4501),[152], % 2.73/3.12 multiply(inverse(X10),X10) = multiply(X11,multiply(double_divide(X11,X12),X12))]. % 2.73/3.12 [4540=param(152,4501),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(inverse(X11),multiply(double_divide(inverse(multiply(inverse(X12),X12)),X13),X13)),multiply(X14,multiply(double_divide(X14,X15),X15)))),X10) = X11]. % 2.73/3.12 [4570=param(839,4501),[], % 2.73/3.12 multiply(X10,inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))) = multiply(X10,inverse(multiply(inverse(X13),X13)))]. % 2.73/3.12 [4582=param(3105,4501),[], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),double_divide(X11,multiply(inverse(multiply(X12,multiply(double_divide(X12,X13),X13))),multiply(inverse(X14),X14)))) = X11]. % 2.73/3.12 [4588=param(6,4539),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X12,inverse(X12)))),double_divide(multiply(X13,multiply(double_divide(X13,X14),X14)),multiply(double_divide(X10,X15),X15))) = X11]. % 2.73/3.12 [4611=param(891,4539),[], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,multiply(double_divide(X11,X12),X12))),multiply(multiply(double_divide(X13,inverse(X13)),X14),X10)) = inverse(X14)]. % 2.73/3.12 [4636=param(2,4539),[1817], % 2.73/3.12 inverse(multiply(double_divide(X10,X11),X11)) = X10]. % 2.73/3.12 [4637=demod(1256),[4636], % 2.73/3.12 double_divide(multiply(double_divide(inverse(X10),X11),X11),double_divide(inverse(X12),X13)) = double_divide(X10,multiply(X12,inverse(X13)))]. % 2.73/3.12 [4644=demod(760),[4637], % 2.73/3.12 double_divide(multiply(X12,X10),multiply(double_divide(inverse(X11),multiply(double_divide(inverse(X13),X14),X14)),X13)) = double_divide(X10,multiply(X11,inverse(inverse(X12))))]. % 2.73/3.12 [4665=demod(934),[4644], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,inverse(inverse(inverse(X10))))),multiply(inverse(X12),X12)) = X11]. % 2.73/3.12 [4675=demod(1473),[4637], % 2.73/3.12 double_divide(multiply(X12,X10),multiply(multiply(multiply(double_divide(X11,X13),X13),inverse(X14)),X14)) = double_divide(X10,multiply(inverse(X11),inverse(inverse(X12))))]. % 2.73/3.12 [4685=demod(819),[4636], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(inverse(multiply(inverse(X11),X11)),X12),X12)) = X10]. % 2.73/3.12 [4686=demod(4540),[4685], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,multiply(X12,multiply(double_divide(X12,X13),X13)))),X10) = X11]. % 2.73/3.12 [4687=demod(4513),[4686], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(double_divide(X11,inverse(X11)),X12),X12)) = X10]. % 2.73/3.12 [4688=demod(3318),[4687], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,inverse(inverse(multiply(inverse(X12),X12))))),X10) = X11]. % 2.73/3.12 [4689=demod(1384),[4688], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(inverse(inverse(inverse(multiply(inverse(X11),X11)))),X12),X12)) = X10]. % 2.73/3.12 [4690=demod(3255),[4689], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,multiply(inverse(X12),X12))),X10) = X11]. % 2.73/3.12 [4692=demod(1901),[4690], % 2.73/3.12 double_divide(inverse(X10),multiply(X11,double_divide(X11,multiply(inverse(X12),X12)))) = X10]. % 2.73/3.12 [4693=demod(2385),[4692], % 2.73/3.12 multiply(X10,double_divide(multiply(double_divide(X11,X12),X12),X11)) = X10]. % 2.73/3.12 [4694=demod(546),[4693], % 2.73/3.12 multiply(double_divide(X10,double_divide(X11,X10)),double_divide(X11,X12)) = inverse(X12)]. % 2.73/3.12 [4708=demod(4023),[4694], % 2.73/3.12 multiply(double_divide(X10,double_divide(X11,inverse(X11))),inverse(multiply(inverse(X12),X12))) = inverse(X10)]. % 2.73/3.12 [4709=demod(4039),[4708], % 2.73/3.12 multiply(inverse(multiply(inverse(X11),X11)),inverse(X10)) = inverse(X10)]. % 2.73/3.12 [4712=demod(3619),[4709], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),multiply(multiply(double_divide(X12,X13),X13),X10)) = double_divide(X11,inverse(X12))]. % 2.73/3.12 [4713=demod(2316),[4712], % 2.73/3.12 double_divide(X10,multiply(inverse(X11),multiply(multiply(X12,X13),double_divide(X13,X12)))) = double_divide(X10,inverse(X11))]. % 2.73/3.12 [4717=demod(2014),[4713], % 2.73/3.12 double_divide(inverse(multiply(inverse(X10),X10)),double_divide(X11,inverse(multiply(inverse(X12),X12)))) = X11]. % 2.73/3.12 [4718=demod(2585),[4717], % 2.73/3.12 double_divide(X10,double_divide(X12,double_divide(X11,X12))) = double_divide(X10,X11)]. % 2.73/3.12 [4840=demod(2456),[4718], % 2.73/3.12 double_divide(X10,double_divide(inverse(X11),double_divide(X12,inverse(X12)))) = double_divide(X10,X11)]. % 2.73/3.12 [4843=demod(4365),[4840], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(double_divide(X11,X12),X12)),X13) = double_divide(X11,X13)]. % 2.73/3.12 [4844=demod(2457),[4843], % 2.73/3.12 double_divide(X10,double_divide(multiply(X11,X12),multiply(double_divide(multiply(inverse(X13),X13),X14),X14))) = double_divide(X10,double_divide(X12,X11))]. % 2.73/3.12 [4846=demod(2360),[4844,4718], % 2.73/3.12 double_divide(X10,double_divide(X11,X10)) = X11]. % 2.73/3.12 [4847=demod(286),[4846], % 2.73/3.12 double_divide(multiply(X11,multiply(double_divide(X11,X12),X12)),multiply(double_divide(X10,X13),X13)) = X10]. % 2.73/3.12 [4848=demod(4588),[4847], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X12,inverse(X12)))),X10) = X11]. % 2.73/3.12 [4849=demod(3972),[4848], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(inverse(inverse(multiply(inverse(X11),X11))),X12),X12)) = X10]. % 2.73/3.12 [4850=demod(1007),[4849], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,inverse(multiply(inverse(X12),X12)))),X10) = X11]. % 2.73/3.12 [4851=demod(3125),[4850], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(multiply(inverse(X11),X11),X12),X12)) = X10]. % 2.73/3.12 [4855=demod(4269),[4851], % 2.73/3.12 double_divide(inverse(X10),double_divide(X11,inverse(X11))) = X10]. % 2.73/3.12 [4856=demod(3380),[4855], % 2.73/3.12 double_divide(inverse(X10),inverse(inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 2.73/3.12 [4857=demod(3069),[4855], % 2.73/3.12 double_divide(inverse(X10),inverse(multiply(inverse(X11),X11))) = X10]. % 2.73/3.12 [4876=demod(4084),[4857], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(X11,X12))),double_divide(inverse(X13),multiply(double_divide(X10,X14),X14))) = double_divide(X12,X13)]. % 2.73/3.12 [4877=demod(1987),[4876], % 2.73/3.12 double_divide(multiply(X10,multiply(multiply(X11,X12),double_divide(X12,X11))),X13) = double_divide(X10,X13)]. % 2.73/3.12 [4878=demod(2907),[4877], % 2.73/3.12 double_divide(X10,multiply(X11,double_divide(double_divide(X12,multiply(inverse(X13),X13)),X12))) = double_divide(X10,X11)]. % 2.73/3.12 [4881=demod(1822),[4878], % 2.73/3.12 double_divide(double_divide(X10,X11),X10) = X11]. % 2.73/3.12 [4882=demod(154),[4881], % 2.73/3.12 multiply(double_divide(multiply(X10,X11),multiply(double_divide(inverse(X12),X13),X13)),X12) = double_divide(X11,X10)]. % 2.73/3.12 [4915=demod(4309),[4881], % 2.73/3.12 multiply(double_divide(inverse(X10),double_divide(double_divide(X11,inverse(X11)),inverse(X12))),X12) = X10]. % 2.73/3.12 [4933=demod(4848),[4881], % 2.73/3.12 multiply(X10,double_divide(X11,inverse(X11))) = X10]. % 2.73/3.12 [4934=demod(3384),[4933], % 2.73/3.12 multiply(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 2.73/3.12 [4935=demod(3408),[4934], % 2.73/3.12 double_divide(inverse(X10),double_divide(multiply(inverse(X11),X11),multiply(inverse(X12),X12))) = X10]. % 2.73/3.12 [4936=demod(3133),[4935], % 2.73/3.12 multiply(X10,inverse(multiply(inverse(X11),X11))) = X10]. % 2.73/3.12 [4938=demod(4570),[4936], % 2.73/3.12 multiply(X10,inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))) = X10]. % 2.73/3.12 [4939=demod(4505),[4938], % 2.73/3.12 double_divide(X10,multiply(inverse(X11),X11)) = inverse(X10)]. % 2.73/3.12 [4944=demod(4665),[4939,1], % 2.73/3.12 multiply(multiply(X10,inverse(inverse(inverse(X11)))),X11) = X10]. % 2.73/3.12 [4955=demod(3183),[4939], % 2.73/3.12 double_divide(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(X11)) = X11]. % 2.73/3.12 [4956=demod(4185),[4955], % 2.73/3.12 multiply(double_divide(inverse(X10),X11),X11) = X10]. % 2.73/3.12 [4957=demod(4882),[4956], % 2.73/3.12 multiply(double_divide(multiply(X10,X11),X12),X12) = double_divide(X11,X10)]. % 2.73/3.12 [4963=demod(624),[4957,4846,4846], % 2.73/3.12 double_divide(inverse(multiply(inverse(X11),X11)),X10) = inverse(X10)]. % 2.73/3.12 [4971=demod(3107),[4963,1], % 2.73/3.12 multiply(multiply(double_divide(X10,inverse(X10)),multiply(inverse(X11),X11)),X12) = X12]. % 2.73/3.12 [4972=demod(3740),[4971], % 2.73/3.12 multiply(multiply(inverse(X12),X12),multiply(X10,X11)) = multiply(X10,X11)]. % 2.73/3.12 [4976=demod(1842),[4972,4939], % 2.73/3.12 double_divide(multiply(inverse(X10),X10),inverse(X11)) = X11]. % 2.73/3.12 [4978=demod(4389),[4976], % 2.73/3.12 double_divide(double_divide(X10,double_divide(X11,inverse(X11))),multiply(multiply(double_divide(X12,X13),X13),X10)) = X12]. % 2.73/3.12 [4982=demod(2449),[4976,4939], % 2.73/3.12 double_divide(X10,double_divide(X11,inverse(X11))) = inverse(X10)]. % 2.73/3.12 [4984=demod(2469),[4982,1], % 2.73/3.12 double_divide(inverse(X12),multiply(double_divide(double_divide(multiply(X10,X12),multiply(double_divide(X13,inverse(X13)),X11)),X14),X14)) = multiply(inverse(X10),inverse(X11))]. % 2.73/3.12 [4993=demod(4394),[4982], % 2.73/3.12 double_divide(double_divide(multiply(inverse(X10),X10),multiply(multiply(X11,X12),double_divide(X12,X11))),inverse(X13)) = X13]. % 2.73/3.12 [4998=demod(4978),[4982], % 2.73/3.12 double_divide(inverse(X10),multiply(multiply(double_divide(X11,X12),X12),X10)) = X11]. % 2.73/3.12 [5004=demod(4497),[4982], % 2.73/3.12 double_divide(X10,inverse(multiply(X11,multiply(double_divide(X11,X12),X12)))) = inverse(X10)]. % 2.73/3.12 [5005=demod(4503),[5004], % 2.73/3.12 double_divide(X10,inverse(multiply(inverse(X11),X11))) = inverse(X10)]. % 2.73/3.12 [5006=demod(3269),[5005], % 2.73/3.12 double_divide(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = inverse(X10)]. % 2.73/3.12 [5007=demod(4856),[5006], % 2.73/3.12 inverse(inverse(X10)) = X10]. % 2.73/3.12 [5038=demod(4675),[5007], % 2.73/3.12 double_divide(multiply(X10,X11),multiply(multiply(multiply(double_divide(X12,X13),X13),inverse(X14)),X14)) = double_divide(X11,multiply(inverse(X12),X10))]. % 2.73/3.12 [5043=demod(3673),[5007], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),double_divide(double_divide(X11,inverse(X11)),multiply(multiply(multiply(double_divide(X12,X13),X13),inverse(X14)),X14))) = X12]. % 2.73/3.12 [5056=demod(4944),[5007], % 2.73/3.12 multiply(multiply(X10,inverse(X11)),X11) = X10]. % 2.73/3.12 [5062=demod(5043),[5056], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),double_divide(double_divide(X11,inverse(X11)),multiply(double_divide(X12,X13),X13))) = X12]. % 2.73/3.12 [5063=demod(5038),[5056], % 2.73/3.12 double_divide(multiply(X10,X11),multiply(double_divide(X12,X13),X13)) = double_divide(X11,multiply(inverse(X12),X10))]. % 2.73/3.12 [5089=demod(200),[5063], % 2.73/3.12 double_divide(X10,double_divide(X11,multiply(double_divide(X12,X13),X13))) = double_divide(X10,multiply(inverse(X11),X12))]. % 2.73/3.12 [5094=demod(182),[5089,5007], % 2.73/3.12 double_divide(double_divide(X10,multiply(X11,double_divide(inverse(X12),multiply(X13,multiply(X11,X12))))),multiply(X14,X10)) = double_divide(X13,X14)]. % 2.73/3.12 [5095=demod(1126),[5094], % 2.73/3.12 double_divide(X10,multiply(double_divide(X11,inverse(X11)),X12)) = double_divide(X10,X12)]. % 2.73/3.12 [5103=demod(3739),[5095,4939], % 2.73/3.12 double_divide(inverse(multiply(X10,X11)),X12) = multiply(X13,double_divide(X13,multiply(X12,double_divide(X11,X10))))]. % 2.73/3.12 [5106=demod(4984),[5095], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(double_divide(multiply(X11,X10),X12),X13),X13)) = multiply(inverse(X11),inverse(X12))]. % 2.73/3.12 [5110=demod(71),[5106], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),inverse(X12)),X13) = multiply(inverse(X12),inverse(multiply(X13,double_divide(X11,X10))))]. % 2.73/3.12 [5122=demod(1693),[5110], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),X11) = multiply(inverse(multiply(X12,X13)),inverse(multiply(X11,double_divide(X13,X12))))]. % 2.73/3.12 [5128=demod(4465),[5110], % 2.73/3.12 double_divide(inverse(multiply(X10,multiply(double_divide(X10,X11),X11))),X12) = multiply(inverse(multiply(X13,X14)),inverse(multiply(X12,double_divide(X14,X13))))]. % 2.73/3.12 [5129=demod(254),[5106,1], % 2.73/3.12 double_divide(double_divide(inverse(X10),multiply(X11,X12)),X13) = multiply(multiply(X11,X12),inverse(multiply(X13,X10)))]. % 2.73/3.12 [5137=demod(4303),[5129,4915], % 2.73/3.12 multiply(multiply(double_divide(X10,X11),X11),inverse(X12)) = double_divide(X10,X12)]. % 2.73/3.12 [5146=demod(1996),[5129], % 2.73/3.12 multiply(multiply(multiply(X10,X11),double_divide(X11,X10)),inverse(multiply(X12,X13))) = multiply(X14,double_divide(X14,multiply(X12,X13)))]. % 2.73/3.12 [5148=demod(132),[5129], % 2.73/3.12 double_divide(inverse(X10),multiply(double_divide(double_divide(multiply(double_divide(X11,X14),X14),multiply(X12,X13)),X15),X15)) = multiply(multiply(X10,X11),inverse(multiply(X12,X13)))]. % 2.73/3.12 [5149=demod(133),[5148], % 2.73/3.12 double_divide(double_divide(multiply(X10,X11),multiply(X12,X13)),X14) = multiply(multiply(X12,X13),inverse(multiply(X14,double_divide(X11,X10))))]. % 2.73/3.12 [5170=demod(4993),[5149,4933,5007], % 2.73/3.12 multiply(multiply(multiply(X10,X11),double_divide(X11,X10)),X12) = X12]. % 2.73/3.12 [5175=demod(5146),[5170], % 2.73/3.12 multiply(X12,double_divide(X12,multiply(X10,X11))) = inverse(multiply(X10,X11))]. % 2.73/3.12 [5210=demod(5103),[5175], % 2.73/3.12 double_divide(inverse(multiply(X10,X11)),X12) = inverse(multiply(X12,double_divide(X11,X10)))]. % 2.73/3.12 [5232=demod(5128),[5210,4693], % 2.73/3.12 multiply(inverse(multiply(X11,X12)),inverse(multiply(X10,double_divide(X12,X11)))) = inverse(X10)]. % 2.73/3.12 [5233=demod(5122),[5232], % 2.73/3.12 double_divide(double_divide(X10,inverse(X10)),X11) = inverse(X11)]. % 2.73/3.12 [5237=demod(4582),[5233,1], % 2.73/3.12 multiply(multiply(inverse(multiply(X10,multiply(double_divide(X10,X11),X11))),multiply(inverse(X12),X12)),X13) = X13]. % 2.73/3.12 [5244=demod(5062),[5233,4636], % 2.73/3.12 multiply(inverse(multiply(inverse(X10),X10)),X11) = X11]. % 2.73/3.12 [5250=demod(3197),[5244], % 2.73/3.12 double_divide(double_divide(X10,multiply(double_divide(X11,X12),X12)),multiply(X13,X10)) = double_divide(X11,X13)]. % 2.73/3.12 [5251=demod(1183),[5250], % 2.73/3.12 double_divide(X10,multiply(double_divide(X11,X12),X12)) = double_divide(X10,inverse(X11))]. % 2.73/3.12 [5262=demod(5106),[5251,1], % 2.73/3.12 double_divide(inverse(X10),multiply(X11,multiply(X12,X10))) = multiply(inverse(X12),inverse(X11))]. % 2.73/3.12 [5270=demod(947),[5262], % 2.73/3.12 double_divide(multiply(X12,X13),multiply(X11,multiply(X10,double_divide(X13,X12)))) = multiply(inverse(X10),inverse(X11))]. % 2.73/3.12 [5276=demod(1110),[5270], % 2.73/3.12 double_divide(double_divide(X10,inverse(X11)),multiply(multiply(double_divide(X12,inverse(X12)),X13),X10)) = multiply(inverse(X11),inverse(X13))]. % 2.73/3.12 [5277=demod(2314),[5276], % 2.73/3.12 double_divide(X10,multiply(X11,multiply(multiply(X12,X13),double_divide(X13,X12)))) = multiply(inverse(X10),inverse(X11))]. % 2.73/3.12 [5281=demod(4713),[5277,5007], % 2.73/3.12 double_divide(X10,inverse(X11)) = multiply(inverse(X10),X11)]. % 2.73/3.12 [5286=demod(5005),[5281], % 2.73/3.12 multiply(inverse(X10),multiply(inverse(X11),X11)) = inverse(X10)]. % 2.73/3.12 [5287=demod(5237),[5286], % 2.73/3.12 multiply(inverse(multiply(X10,multiply(double_divide(X10,X11),X11))),X12) = X12]. % 2.73/3.12 [5288=demod(4499),[5287], % 2.73/3.12 multiply(multiply(double_divide(X10,X12),X12),X11) = multiply(inverse(X10),X11)]. % 2.73/3.12 [5299=demod(4998),[5288], % 2.73/3.12 double_divide(inverse(X10),multiply(inverse(X11),X10)) = X11]. % 2.73/3.12 [5302=demod(5137),[5288], % 2.73/3.12 double_divide(X10,X11) = multiply(inverse(X10),inverse(X11))]. % 2.73/3.12 [5304=demod(1),[5302], % 2.73/3.12 inverse(multiply(inverse(X10),inverse(X11))) = multiply(X11,X10)]. % 2.73/3.12 [5327=demod(5299),[5302,5007], % 2.73/3.12 multiply(X10,inverse(multiply(inverse(X11),X10))) = X11]. % 2.73/3.12 [5380=demod(4693),[5302,-5304,5327,5302,5007], % 2.73/3.12 multiply(X10,multiply(X11,inverse(X11))) = X10]. % 2.73/3.12 [5388=demod(1844),[5302,-5304,5327,5302,5007,5302,5244], % 2.73/3.12 multiply(X10,inverse(X11)) = inverse(multiply(X11,inverse(X10)))]. % 2.73/3.12 [5404=demod(4971),[5302,5007,4972], % 2.73/3.12 multiply(multiply(inverse(X10),X10),X11) = X11]. % 2.73/3.12 [5458=demod(4611),[5302,-5304,5327,5302,-5388,5380,5302,5007,5404,5302,5007], % 2.73/3.12 multiply(X10,inverse(multiply(X11,X10))) = inverse(X11)]. % 2.73/3.12 [5480=demod(2103),[5302,5302,-5304,5458,5007,5302,-5304,5458,5007,5302,5007,5007], % 2.73/3.12 inverse(multiply(inverse(X10),inverse(multiply(X11,X12)))) = multiply(X11,multiply(X12,X10))]. % 2.73/3.12 [5770=param(4,5304),[5480,3], % 2.73/3.12 thmtrue = thmfalse]. % 2.73/3.12 % SZS output end CNFRefutation % 2.73/3.12 Space: 6330 KB %------------------------------------------------------------------------------