%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP437-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n025.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:02 EDT 2022 % Result : Unsatisfiable 1.30s 1.71s % Output : CNFRefutation 1.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP437-1 : TPTP v8.1.0. Released v2.6.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 21:03:54 EDT 2022 % 0.13/0.34 % CPUTime : % 1.30/1.71 Theorem Proved. % 1.30/1.71 % SZS status Unsatisfiable % 1.30/1.71 % SZS output start CNFRefutation % 1.30/1.71 [1=axiom,[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(X13,X11))),X10))))) = X13]. % 1.30/1.71 [2=axiom,[], % 1.30/1.71 thtop(X10,X10) = thmfalse]. % 1.30/1.71 [3=axiom,[], % 1.30/1.71 thtop(multiply(multiply(inverse(b2),b2),a2),a2) = thmtrue]. % 1.30/1.71 [4=param(1,1),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,X13))),inverse(X14))),multiply(X14,multiply(X12,X10))))) = X13]. % 1.30/1.71 [5=param(1,1),[], % 1.30/1.71 multiply(inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,X10))),multiply(inverse(X13),inverse(multiply(X14,X15))))))),inverse(multiply(X15,multiply(X13,X12)))) = X14]. % 1.30/1.71 [6=param(1,1),[], % 1.30/1.71 multiply(X10,inverse(multiply(inverse(multiply(X11,multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(X13,X11))),X14)))),multiply(X15,multiply(multiply(inverse(X15),inverse(X13)),X10))))) = X14]. % 1.30/1.71 [7=param(1,4),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(X12,inverse(X13))),multiply(X13,multiply(X14,X10))))) = multiply(X15,multiply(multiply(inverse(X15),inverse(multiply(X12,X14))),inverse(X11)))]. % 1.30/1.71 [9=param(7,4),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X12,X13))),X12))),inverse(X11))) = X13]. % 1.30/1.71 [10=param(1,7),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(X11,multiply(X12,inverse(multiply(multiply(X10,multiply(X13,inverse(X14))),multiply(X14,multiply(X11,X12)))))))) = X13]. % 1.30/1.71 [11=param(10,1),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X12,multiply(X10,multiply(X13,inverse(X11)))))),X12))) = X13]. % 1.30/1.71 [13=param(1,11),[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(X12,multiply(X13,X10))))) = multiply(inverse(X14),inverse(multiply(X11,multiply(X12,multiply(X13,inverse(X14))))))]. % 1.30/1.71 [15=param(1,13),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(X12,inverse(X13))),multiply(X13,multiply(multiply(X14,inverse(multiply(X15,multiply(X11,multiply(X12,X14))))),X10))))) = X15]. % 1.30/1.71 [16=param(15,7),[], % 1.30/1.71 multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,multiply(X13,inverse(multiply(X10,multiply(X14,multiply(X12,X13)))))))),inverse(X14))) = X10]. % 1.30/1.71 [17=param(10,15),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(multiply(X12,multiply(X10,multiply(X13,X11))))),X12))) = X13]. % 1.30/1.71 [19=param(1,17),[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(X12,multiply(X13,X10))))) = multiply(X14,inverse(multiply(X11,multiply(X12,multiply(X13,X14)))))]. % 1.30/1.71 [20=param(1,17),[], % 1.30/1.71 multiply(X10,inverse(multiply(inverse(multiply(multiply(X11,inverse(multiply(X12,multiply(X13,multiply(X14,X11))))),X12)),multiply(X15,multiply(multiply(inverse(X15),inverse(X14)),X10))))) = inverse(X13)]. % 1.30/1.71 [21=param(17,9),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X12,X13))),X12))) = multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X14,X13))),X14)))]. % 1.30/1.71 [23=param(16,4),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,X12))),inverse(X13))) = multiply(X14,multiply(multiply(inverse(X14),inverse(multiply(X11,X12))),inverse(X13)))]. % 1.30/1.71 [25=param(23,1),[1], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(X11)),inverse(X12))) = multiply(X13,multiply(multiply(inverse(X13),inverse(X11)),inverse(X12)))]. % 1.30/1.71 [35=param(19,9),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(X11,X12))) = multiply(X13,inverse(multiply(X11,multiply(X14,multiply(multiply(inverse(X14),inverse(multiply(multiply(inverse(X10),inverse(multiply(X15,X12))),X15))),X13)))))]. % 1.30/1.71 [39=param(16,6),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(X12)),X13))),inverse(X11))) = inverse(multiply(X14,multiply(X15,multiply(multiply(inverse(X15),inverse(multiply(X12,X14))),X13))))]. % 1.30/1.71 [47=param(16,20),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(X12)),inverse(X13)))),inverse(X11))) = inverse(multiply(multiply(X14,inverse(multiply(X15,multiply(X13,multiply(X12,X14))))),X15))]. % 1.30/1.71 [56=param(39,9),[], % 1.30/1.71 inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,X13),X10))),X12)))) = X13]. % 1.30/1.71 [58=param(1,39),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(inverse(X12),inverse(X13)),X10))),inverse(X12)))) = X13]. % 1.30/1.71 [61=param(56,1),[], % 1.30/1.71 inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,X10))),X13)))) = inverse(multiply(X14,multiply(X15,multiply(multiply(inverse(X15),inverse(multiply(X12,X14))),X13))))]. % 1.30/1.71 [62=param(1,56),[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(multiply(X12,multiply(X13,multiply(multiply(inverse(X13),inverse(multiply(multiply(X14,X15),X12))),X14))),multiply(multiply(X15,inverse(multiply(X16,X11))),X10))))) = X16]. % 1.30/1.71 [64=param(56,4),[], % 1.30/1.71 inverse(multiply(multiply(X10,multiply(X11,inverse(X12))),multiply(X12,multiply(X13,X14)))) = multiply(multiply(inverse(X14),inverse(multiply(X11,X13))),inverse(X10))]. % 1.30/1.71 [74=param(56,16),[], % 1.30/1.71 inverse(multiply(multiply(X10,inverse(multiply(X11,multiply(X12,multiply(multiply(inverse(X12),X13),X10))))),X11)) = X13]. % 1.30/1.71 [79=param(23,56),[56], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),X11),inverse(X12))) = multiply(X13,multiply(multiply(inverse(X13),X11),inverse(X12)))]. % 1.30/1.71 [82=param(25,56),[56], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(X11)),X12)) = multiply(X13,multiply(multiply(inverse(X13),inverse(X11)),X12))]. % 1.30/1.71 [113=param(82,10),[], % 1.30/1.71 multiply(X13,multiply(multiply(inverse(X13),inverse(multiply(X14,multiply(X15,inverse(multiply(multiply(X10,multiply(X11,inverse(X16))),multiply(X16,multiply(X14,X15)))))))),X12)) = multiply(X10,multiply(X11,X12))]. % 1.30/1.71 [170=param(58,16),[], % 1.30/1.71 multiply(multiply(X10,inverse(multiply(X11,multiply(X12,multiply(multiply(inverse(X12),inverse(X13)),X10))))),X11) = X13]. % 1.30/1.71 [175=param(58,56),[56], % 1.30/1.71 multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,inverse(X13)),X10))),X12))) = X13]. % 1.30/1.71 [219=param(1,170),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(X12)),inverse(X13))),multiply(X13,X12)))) = X10]. % 1.30/1.71 [229=param(1,219),[], % 1.30/1.71 multiply(X10,inverse(multiply(inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(X12)),inverse(X13))),multiply(X13,X12))),multiply(X14,multiply(multiply(inverse(X14),inverse(X15)),X10))))) = X15]. % 1.30/1.71 [232=param(17,219),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(multiply(inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(X12)),inverse(X13))),multiply(X13,X12))),inverse(multiply(X14,multiply(X10,X15)))),X14))) = X15]. % 1.30/1.71 [235=param(23,219),[219], % 1.30/1.71 multiply(X10,multiply(inverse(X10),inverse(X11))) = multiply(X12,multiply(inverse(X12),inverse(X11)))]. % 1.30/1.71 [239=param(35,219),[219], % 1.30/1.71 multiply(inverse(X10),inverse(X11)) = multiply(X12,inverse(multiply(X11,multiply(X13,multiply(multiply(inverse(X13),inverse(multiply(multiply(inverse(X10),inverse(X14)),X14))),X12)))))]. % 1.30/1.71 [241=param(39,219),[219], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(inverse(X11),inverse(X12)))),inverse(X11))) = inverse(multiply(X13,multiply(X14,multiply(inverse(X14),inverse(multiply(X12,X13))))))]. % 1.30/1.71 [244=param(56,219),[], % 1.30/1.71 inverse(multiply(X10,multiply(X11,multiply(inverse(X11),inverse(multiply(multiply(inverse(multiply(multiply(X12,multiply(multiply(inverse(X12),inverse(X13)),inverse(X14))),multiply(X14,X13))),X15),X10)))))) = X15]. % 1.30/1.71 [252=param(79,219),[219], % 1.30/1.71 multiply(X10,multiply(inverse(X10),X11)) = multiply(X12,multiply(inverse(X12),X11))]. % 1.30/1.71 [256=param(219,175),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(multiply(X13,inverse(X14)),X15))),X13)))),inverse(X15))),X14))) = X10]. % 1.30/1.71 [257=param(175,219),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(inverse(X11),inverse(multiply(multiply(inverse(multiply(multiply(X12,multiply(multiply(inverse(X12),inverse(X13)),inverse(X14))),multiply(X14,X13))),inverse(X15)),X10))))) = X15]. % 1.30/1.71 [261=param(1,252),[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(inverse(X11),multiply(multiply(inverse(inverse(X12)),inverse(multiply(X13,X12))),X10))))) = X13]. % 1.30/1.71 [266=param(5,252),[], % 1.30/1.71 multiply(inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,X10))),multiply(inverse(inverse(X13)),inverse(multiply(X14,X13))))))),inverse(multiply(X15,multiply(inverse(X15),X12)))) = X14]. % 1.30/1.71 [276=param(16,252),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,multiply(X12,inverse(multiply(X13,multiply(inverse(X13),multiply(X11,X12)))))))),inverse(inverse(X14)))) = X14]. % 1.30/1.71 [294=param(74,252),[], % 1.30/1.71 inverse(multiply(multiply(X10,inverse(multiply(X11,multiply(inverse(X11),multiply(multiply(inverse(inverse(X12)),X13),X10))))),X12)) = X13]. % 1.30/1.71 [306=param(235,10),[], % 1.30/1.71 multiply(X12,multiply(inverse(X12),inverse(multiply(X13,multiply(X14,inverse(multiply(multiply(X10,multiply(X11,inverse(X15))),multiply(X15,multiply(X13,X14))))))))) = multiply(X10,X11)]. % 1.30/1.71 [312=param(235,219),[219], % 1.30/1.71 multiply(X10,inverse(X10)) = multiply(X11,inverse(X11))]. % 1.30/1.71 [339=param(35,312),[-35], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(X11,inverse(X11)))) = multiply(inverse(X10),inverse(multiply(X12,inverse(X12))))]. % 1.30/1.71 [348=param(175,312),[], % 1.30/1.71 multiply(inverse(multiply(X10,inverse(X11))),multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(X13,inverse(X13)))),X10))) = X11]. % 1.30/1.71 [349=param(175,312),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,inverse(X12)),X10))),X13))) = X13]. % 1.30/1.71 [352=param(235,312),[], % 1.30/1.71 multiply(X10,multiply(X11,inverse(X11))) = multiply(X12,multiply(inverse(X12),inverse(inverse(X10))))]. % 1.30/1.71 [398=param(219,352),[], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(inverse(X11),inverse(inverse(multiply(X12,multiply(multiply(inverse(X12),inverse(inverse(X13))),inverse(X13))))))))) = X10]. % 1.30/1.71 [433=param(56,339),[175], % 1.30/1.71 inverse(multiply(X10,inverse(X10))) = inverse(multiply(X11,inverse(X11)))]. % 1.30/1.71 [451=param(79,433),[], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),multiply(multiply(inverse(multiply(X11,inverse(X11))),X12),inverse(X13))) = multiply(X14,multiply(multiply(inverse(X14),X12),inverse(X13)))]. % 1.30/1.71 [474=param(349,16),[], % 1.30/1.71 multiply(multiply(X10,inverse(multiply(X11,multiply(X12,multiply(multiply(X13,inverse(X13)),X10))))),X11) = inverse(X12)]. % 1.30/1.71 [489=param(74,349),[], % 1.30/1.71 inverse(multiply(multiply(X10,inverse(X10)),X11)) = inverse(multiply(multiply(X12,inverse(X12)),X11))]. % 1.30/1.71 [492=param(74,349),[], % 1.30/1.71 inverse(multiply(multiply(X10,inverse(multiply(X11,multiply(X12,multiply(X13,X10))))),X11)) = multiply(X14,multiply(multiply(inverse(X14),inverse(multiply(multiply(X15,inverse(X15)),inverse(X12)))),X13))]. % 1.30/1.71 [512=param(349,235),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(X12,multiply(inverse(X12),inverse(X13))))) = multiply(inverse(multiply(inverse(X11),inverse(multiply(multiply(X14,inverse(X14)),X10)))),inverse(X13))]. % 1.30/1.71 [525=param(349,352),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(X12,multiply(X13,inverse(X13))))) = multiply(inverse(multiply(inverse(X11),inverse(multiply(multiply(X14,inverse(X14)),X10)))),inverse(inverse(X12)))]. % 1.30/1.71 [532=param(61,312),[], % 1.30/1.71 inverse(multiply(inverse(X10),multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,inverse(X12)))),X13)))) = inverse(multiply(X14,multiply(X15,multiply(multiply(inverse(X15),inverse(multiply(X10,X14))),X13))))]. % 1.30/1.71 [566=param(175,489),[175], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),X11) = multiply(multiply(X12,inverse(X12)),X11)]. % 1.30/1.71 [591=param(566,19),[], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),inverse(multiply(X11,multiply(X12,multiply(X13,multiply(X14,inverse(X14))))))) = multiply(X15,inverse(multiply(X11,multiply(X12,multiply(X13,X15)))))]. % 1.30/1.71 [606=param(566,252),[], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),multiply(inverse(multiply(X11,inverse(X11))),X12)) = multiply(X13,multiply(inverse(X13),X12))]. % 1.30/1.71 [607=param(566,312),[], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),inverse(multiply(X11,inverse(X11)))) = multiply(X12,inverse(X12))]. % 1.30/1.71 [610=param(566,352),[], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),multiply(inverse(multiply(X11,inverse(X11))),inverse(inverse(X12)))) = multiply(X12,multiply(X13,inverse(X13)))]. % 1.30/1.71 [613=param(16,62),[56], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(multiply(X12,X13))),X12))),X11)) = X13]. % 1.30/1.71 [625=param(47,607),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,inverse(X11)))),inverse(X12))) = inverse(multiply(multiply(X13,inverse(multiply(X14,multiply(multiply(X15,inverse(X15)),multiply(inverse(X12),X13))))),X14))]. % 1.30/1.71 [739=param(474,566),[], % 1.30/1.71 multiply(multiply(multiply(X10,inverse(X10)),inverse(multiply(X11,multiply(X12,multiply(multiply(X13,inverse(X13)),multiply(X14,inverse(X14))))))),X11) = inverse(X12)]. % 1.30/1.71 [788=param(613,312),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(X11)),X12))),multiply(X12,X13))) = X13]. % 1.30/1.71 [810=param(613,613),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(X12)),X13))),X11)) = multiply(multiply(inverse(X13),inverse(multiply(multiply(X14,inverse(multiply(X15,X12))),X15))),X14)]. % 1.30/1.71 [815=param(219,64),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X11),inverse(multiply(multiply(inverse(X12),inverse(multiply(X13,X11))),X13))),inverse(X12))) = X10]. % 1.30/1.71 [827=param(74,64),[], % 1.30/1.71 inverse(inverse(multiply(multiply(X10,multiply(inverse(X10),inverse(X11))),multiply(X11,multiply(multiply(X12,multiply(multiply(inverse(X12),X13),inverse(X14))),X14))))) = X13]. % 1.30/1.71 [870=param(788,170),[], % 1.30/1.71 multiply(X10,X11) = inverse(multiply(X12,multiply(multiply(inverse(X12),inverse(X11)),inverse(X10))))]. % 1.30/1.71 [871=demod(398),[-870], % 1.30/1.71 multiply(X10,inverse(multiply(X11,multiply(inverse(X11),inverse(multiply(X12,inverse(X12))))))) = X10]. % 1.30/1.71 [900=param(871,5),[], % 1.30/1.71 inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(inverse(multiply(X12,inverse(X12))),X10))),multiply(inverse(inverse(X13)),inverse(multiply(X14,X13))))))) = X14]. % 1.30/1.71 [924=param(175,871),[], % 1.30/1.71 multiply(inverse(multiply(X10,multiply(inverse(X10),inverse(multiply(X11,inverse(X11)))))),multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(X13,inverse(X14)))),X13))) = X14]. % 1.30/1.71 [927=param(871,312),[], % 1.30/1.71 multiply(X10,multiply(inverse(X10),inverse(multiply(X11,inverse(X11))))) = multiply(X12,inverse(X12))]. % 1.30/1.71 [941=param(613,871),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(inverse(multiply(X12,multiply(inverse(X12),inverse(multiply(X13,inverse(X13)))))),X14))))),X11)) = X14]. % 1.30/1.71 [942=param(613,871),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,X12))),X11)) = multiply(inverse(X12),inverse(multiply(X13,inverse(X13))))]. % 1.30/1.71 [950=param(5,927),[900], % 1.30/1.71 multiply(X10,inverse(multiply(X11,inverse(X11)))) = X10]. % 1.30/1.71 [951=demod(942),[950], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,X12))),X11)) = inverse(X12)]. % 1.30/1.71 [956=demod(241),[951], % 1.30/1.71 inverse(multiply(X11,multiply(X12,multiply(inverse(X12),inverse(multiply(X10,X11)))))) = inverse(inverse(X10))]. % 1.30/1.71 [958=demod(244),[956], % 1.30/1.71 inverse(inverse(multiply(inverse(multiply(multiply(X10,multiply(multiply(inverse(X10),inverse(X11)),inverse(X12))),multiply(X12,X11))),X13))) = X13]. % 1.30/1.71 [966=demod(941),[950,951], % 1.30/1.71 inverse(inverse(multiply(inverse(multiply(X10,inverse(X10))),X11))) = X11]. % 1.30/1.71 [973=demod(348),[950], % 1.30/1.71 multiply(inverse(multiply(X10,inverse(X11))),multiply(X12,multiply(inverse(X12),X10))) = X11]. % 1.30/1.71 [982=demod(532),[950], % 1.30/1.71 inverse(multiply(inverse(X10),multiply(X11,multiply(inverse(X11),X12)))) = inverse(multiply(X13,multiply(X14,multiply(multiply(inverse(X14),inverse(multiply(X10,X13))),X12))))]. % 1.30/1.71 [986=demod(924),[950,951], % 1.30/1.71 multiply(inverse(multiply(X10,inverse(X10))),inverse(inverse(X11))) = X11]. % 1.30/1.71 [988=demod(610),[986], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),X11) = multiply(X11,multiply(X12,inverse(X12)))]. % 1.30/1.71 [997=demod(625),[950], % 1.30/1.71 multiply(X10,multiply(inverse(X10),inverse(X11))) = inverse(multiply(multiply(X12,inverse(multiply(X13,multiply(multiply(X14,inverse(X14)),multiply(inverse(X11),X12))))),X13))]. % 1.30/1.71 [1021=param(21,950),[], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(inverse(X11),inverse(multiply(inverse(multiply(X12,inverse(X12))),X13))))) = multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X14,X13))),X14)))]. % 1.30/1.71 [1029=param(47,950),[951], % 1.30/1.71 inverse(multiply(multiply(X11,inverse(multiply(X12,multiply(multiply(X13,inverse(X13)),multiply(X10,X11))))),X12)) = inverse(inverse(X10))]. % 1.30/1.71 [1030=demod(997),[1029], % 1.30/1.71 multiply(X10,multiply(inverse(X10),inverse(X11))) = inverse(inverse(inverse(X11)))]. % 1.30/1.71 [1031=demod(257),[1030], % 1.30/1.71 multiply(X10,inverse(inverse(inverse(multiply(multiply(inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(X12)),inverse(X13))),multiply(X13,X12))),inverse(X14)),X10))))) = X14]. % 1.30/1.71 [1078=demod(512),[1030], % 1.30/1.71 multiply(inverse(multiply(inverse(X11),inverse(multiply(multiply(X13,inverse(X13)),X10)))),inverse(X12)) = multiply(X10,multiply(X11,inverse(inverse(inverse(X12)))))]. % 1.30/1.71 [1084=demod(525),[1078], % 1.30/1.71 multiply(X10,multiply(X11,multiply(X12,multiply(X13,inverse(X13))))) = multiply(X10,multiply(X11,inverse(inverse(inverse(inverse(X12))))))]. % 1.30/1.71 [1091=demod(739),[1084], % 1.30/1.71 multiply(multiply(multiply(X10,inverse(X10)),inverse(multiply(X11,multiply(X12,inverse(inverse(inverse(inverse(multiply(X13,inverse(X13)))))))))),X11) = inverse(X12)]. % 1.30/1.71 [1093=demod(591),[1084], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),inverse(multiply(X11,multiply(X12,inverse(inverse(inverse(inverse(X13)))))))) = multiply(X14,inverse(multiply(X11,multiply(X12,multiply(X13,X14)))))]. % 1.30/1.71 [1116=demod(306),[1030], % 1.30/1.71 inverse(inverse(inverse(multiply(X10,multiply(X11,inverse(multiply(multiply(X12,multiply(X13,inverse(X14))),multiply(X14,multiply(X10,X11))))))))) = multiply(X12,X13)]. % 1.30/1.71 [1124=demod(827),[1030], % 1.30/1.71 inverse(inverse(multiply(inverse(inverse(inverse(X10))),multiply(X10,multiply(multiply(X11,multiply(multiply(inverse(X11),X12),inverse(X13))),X13))))) = X12]. % 1.30/1.71 [1126=demod(352),[1030], % 1.30/1.71 multiply(X10,multiply(X11,inverse(X11))) = inverse(inverse(inverse(inverse(X10))))]. % 1.30/1.71 [1128=demod(988),[1126], % 1.30/1.71 multiply(multiply(X10,inverse(X10)),X11) = inverse(inverse(inverse(inverse(X11))))]. % 1.30/1.71 [1140=demod(1093),[1128], % 1.30/1.71 multiply(X13,inverse(multiply(X10,multiply(X11,multiply(X12,X13))))) = inverse(inverse(inverse(inverse(inverse(multiply(X10,multiply(X11,inverse(inverse(inverse(inverse(X12)))))))))))]. % 1.30/1.71 [1144=demod(261),[1140,1030], % 1.30/1.71 inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(X10)),inverse(multiply(X11,X10)))))))))))))) = X11]. % 1.30/1.71 [1152=demod(229),[1140,958], % 1.30/1.71 inverse(inverse(inverse(multiply(X10,inverse(inverse(inverse(inverse(multiply(inverse(X10),inverse(X11)))))))))) = X11]. % 1.30/1.71 [1159=demod(294),[1140,1030], % 1.30/1.71 inverse(multiply(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(X10)),X11)))))))))))),X10)) = X11]. % 1.30/1.71 [1184=demod(1116),[1140], % 1.30/1.71 inverse(inverse(inverse(multiply(X10,inverse(inverse(inverse(inverse(inverse(multiply(multiply(X11,multiply(X12,inverse(X13))),multiply(X13,inverse(inverse(inverse(inverse(X10))))))))))))))) = multiply(X11,X12)]. % 1.30/1.71 [1245=demod(239),[1140], % 1.30/1.71 multiply(inverse(X10),inverse(X11)) = inverse(inverse(inverse(inverse(inverse(multiply(X11,multiply(X12,inverse(inverse(inverse(inverse(multiply(inverse(X12),inverse(multiply(multiply(inverse(X10),inverse(X13)),X13))))))))))))))]. % 1.30/1.71 [1254=demod(113),[1140], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,inverse(inverse(inverse(inverse(inverse(multiply(multiply(X12,multiply(X13,inverse(X14))),multiply(X14,inverse(inverse(inverse(inverse(X11)))))))))))))),X15)) = multiply(X12,multiply(X13,X15))]. % 1.30/1.71 [1263=demod(276),[1140,1030], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(X11)))))))))))))),inverse(inverse(X12)))) = X12]. % 1.30/1.71 [1268=demod(1091),[1128], % 1.30/1.71 multiply(inverse(inverse(inverse(inverse(inverse(multiply(X10,multiply(X11,inverse(inverse(inverse(inverse(multiply(X12,inverse(X12))))))))))))),X10) = inverse(X11)]. % 1.30/1.71 [1281=demod(492),[1140,1128], % 1.30/1.71 inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(X10,multiply(X11,inverse(inverse(inverse(inverse(X12))))))))))),X10)) = multiply(X13,multiply(multiply(inverse(X13),inverse(inverse(inverse(inverse(inverse(inverse(X11))))))),X12))]. % 1.30/1.71 [1290=demod(256),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,multiply(multiply(inverse(X12),inverse(multiply(multiply(X13,inverse(X14)),X15))),X13)))),inverse(X15))),X14))) = X10]. % 1.30/1.71 [1292=demod(815),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X11),inverse(multiply(multiply(inverse(X12),inverse(multiply(X13,X11))),X13))),inverse(X12))) = X10]. % 1.30/1.71 [1340=demod(451),[1128], % 1.30/1.71 inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(X10,inverse(X10))),X11),inverse(X12)))))) = multiply(X13,multiply(multiply(inverse(X13),X11),inverse(X12)))]. % 1.30/1.71 [1348=demod(606),[1128,966], % 1.30/1.71 multiply(X11,multiply(inverse(X11),X10)) = inverse(inverse(X10))]. % 1.30/1.71 [1353=demod(973),[1348], % 1.30/1.71 multiply(inverse(multiply(X10,inverse(X11))),inverse(inverse(X10))) = X11]. % 1.30/1.71 [1357=demod(266),[1348], % 1.30/1.71 multiply(inverse(multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(X12,X10))),multiply(inverse(inverse(X13)),inverse(multiply(X14,X13))))))),inverse(inverse(inverse(X12)))) = X14]. % 1.30/1.71 [1364=demod(982),[1348], % 1.30/1.71 inverse(multiply(X12,multiply(X13,multiply(multiply(inverse(X13),inverse(multiply(X10,X12))),X11)))) = inverse(multiply(inverse(X10),inverse(inverse(X11))))]. % 1.30/1.71 [1366=demod(1357),[1364,1353], % 1.30/1.71 inverse(multiply(inverse(inverse(X10)),inverse(multiply(X11,X10)))) = X11]. % 1.30/1.71 [1367=demod(1144),[1366], % 1.30/1.71 inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(X10)))))))))) = X10]. % 1.30/1.71 [1370=demod(1159),[1367], % 1.30/1.71 inverse(multiply(inverse(multiply(inverse(inverse(X10)),X11)),X10)) = X11]. % 1.30/1.71 [1372=demod(1263),[1367,950,1348], % 1.30/1.71 inverse(inverse(inverse(inverse(X10)))) = X10]. % 1.30/1.71 [1376=demod(1152),[1372,1348,1372], % 1.30/1.71 inverse(inverse(X10)) = X10]. % 1.30/1.71 [1382=demod(1370),[1376], % 1.30/1.71 inverse(multiply(inverse(multiply(X10,X11)),X10)) = X11]. % 1.30/1.71 [1385=demod(1348),[1376], % 1.30/1.71 multiply(X10,multiply(inverse(X10),X11)) = X11]. % 1.30/1.71 [1392=demod(958),[1376], % 1.30/1.71 multiply(inverse(multiply(multiply(X10,multiply(multiply(inverse(X10),inverse(X11)),inverse(X12))),multiply(X12,X11))),X13) = X13]. % 1.30/1.71 [1393=demod(232),[1392,1382], % 1.30/1.71 multiply(inverse(X10),multiply(X10,X11)) = X11]. % 1.30/1.71 [1394=demod(966),[1376], % 1.30/1.71 multiply(inverse(multiply(X10,inverse(X10))),X11) = X11]. % 1.30/1.71 [1406=demod(1021),[1394], % 1.30/1.71 multiply(inverse(X10),inverse(multiply(multiply(inverse(X11),inverse(multiply(X13,X12))),X13))) = multiply(inverse(X10),inverse(multiply(inverse(X11),inverse(X12))))]. % 1.30/1.71 [1408=demod(1292),[1406], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X11),inverse(multiply(inverse(X12),inverse(X11)))),inverse(X12))) = X10]. % 1.30/1.71 [1412=demod(1031),[1392,1376], % 1.30/1.71 multiply(X10,inverse(multiply(inverse(X11),X10))) = X11]. % 1.30/1.71 [1413=demod(1408),[1412], % 1.30/1.71 multiply(X10,multiply(X11,inverse(X11))) = X10]. % 1.30/1.71 [1417=demod(1124),[1376,1393,1376], % 1.30/1.71 multiply(multiply(X10,multiply(multiply(inverse(X10),X11),inverse(X12))),X12) = X11]. % 1.30/1.71 [1425=demod(1340),[1394,1376,1376], % 1.30/1.71 multiply(X12,multiply(multiply(inverse(X12),X10),inverse(X11))) = multiply(X10,inverse(X11))]. % 1.30/1.71 [1426=demod(1290),[1425], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(inverse(multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,inverse(X13)),X14))),X12))),inverse(X14)),X13))) = X10]. % 1.30/1.71 [1448=demod(870),[1425], % 1.30/1.71 multiply(X10,X11) = inverse(multiply(inverse(X11),inverse(X10)))]. % 1.30/1.71 [1458=demod(175),[], % 1.30/1.71 multiply(X10,multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,inverse(X13)),X10))),X12))) = X13]. % 1.30/1.71 [1486=demod(810),[], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(X12)),X13))),X11)) = multiply(multiply(inverse(X13),inverse(multiply(multiply(X14,inverse(multiply(X15,X12))),X15))),X14)]. % 1.30/1.71 [1515=demod(1426),[], % 1.30/1.71 multiply(X10,inverse(multiply(multiply(inverse(multiply(X11,multiply(multiply(inverse(X11),inverse(multiply(multiply(X12,inverse(X13)),X14))),X12))),inverse(X14)),X13))) = X10]. % 1.30/1.71 [1537=demod(1417),[1425], % 1.30/1.71 multiply(multiply(X10,inverse(X11)),X11) = X10]. % 1.30/1.71 [1575=demod(1268),[1376,1376,1413,1376,1376], % 1.30/1.71 multiply(inverse(multiply(X10,X11)),X10) = inverse(X11)]. % 1.30/1.71 [1591=demod(1245),[1537,1376,1376,1376,1385,1376,1376], % 1.30/1.71 multiply(inverse(X10),inverse(X11)) = inverse(multiply(X11,X10))]. % 1.30/1.71 [1599=demod(1486),[-1591], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(multiply(X11,inverse(X12)),X13))),X11)) = multiply(multiply(inverse(X13),multiply(inverse(X14),inverse(multiply(X15,inverse(multiply(X14,X12)))))),X15)]. % 1.30/1.71 [1604=demod(1515),[-1591,-1448,1458], % 1.30/1.71 multiply(X10,multiply(inverse(X11),X11)) = X10]. % 1.30/1.71 [1648=demod(1254),[1376,1376,1376,1376], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(multiply(X12,multiply(X13,inverse(X14))),multiply(X14,X11)))))),X15)) = multiply(X12,multiply(X13,X15))]. % 1.30/1.71 [1695=demod(1184),[1376,1376,1376,1376,1376], % 1.30/1.71 inverse(multiply(X10,inverse(multiply(multiply(X11,multiply(X12,inverse(X13))),multiply(X13,X10))))) = multiply(X11,X12)]. % 1.30/1.71 [1696=demod(1648),[1695], % 1.30/1.71 multiply(X10,multiply(multiply(inverse(X10),multiply(X11,X12)),X13)) = multiply(X11,multiply(X12,X13))]. % 1.30/1.71 [1724=demod(1281),[1376,1376,1376,1376,1575,1376,1376,1376,1376], % 1.30/1.71 multiply(X12,multiply(multiply(inverse(X12),X10),X11)) = multiply(X10,X11)]. % 1.30/1.71 [1764=demod(1696),[1724], % 1.30/1.71 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 1.30/1.71 [1801=demod(1599),[1764,1764,1575,1385,1764,1764,1575,1376,1393], % 1.30/1.71 inverse(multiply(inverse(X10),X11)) = multiply(inverse(X11),X10)]. % 1.30/1.71 [1834=param(3,1448),[1801,1604,1376,2], % 1.30/1.71 thmtrue = thmfalse]. % 1.30/1.71 % SZS output end CNFRefutation % 1.30/1.71 Space: 2019 KB %------------------------------------------------------------------------------