%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP417-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n005.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:13:57 EDT 2022 % Result : Unsatisfiable 0.88s 1.25s % Output : CNFRefutation 0.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP417-1 : TPTP v8.1.0. Released v2.6.0. % 0.07/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n005.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 06:39:54 EDT 2022 % 0.12/0.33 % CPUTime : % 0.88/1.25 Theorem Proved. % 0.88/1.25 % SZS status Unsatisfiable % 0.88/1.25 % SZS output start CNFRefutation % 0.88/1.25 [1=axiom,[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,inverse(X12)))),inverse(multiply(inverse(X10),X10)))))) = X12]. % 0.88/1.25 [2=axiom,[], % 0.88/1.25 thtop(X10,X10) = thmfalse]. % 0.88/1.25 [3=axiom,[], % 0.88/1.25 thtop(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) = thmtrue]. % 0.88/1.25 [4=param(1,1),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12))),inverse(multiply(inverse(X10),X10)))))) = multiply(X13,inverse(multiply(inverse(multiply(inverse(multiply(X14,X13)),multiply(X14,inverse(X12)))),inverse(multiply(inverse(X13),X13)))))]. % 0.88/1.25 [5=param(4,1),[], % 0.88/1.25 multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,inverse(inverse(X12))))),inverse(multiply(inverse(X10),X10))))) = X12]. % 0.88/1.25 [6=param(4,4),[5], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12))),inverse(multiply(inverse(X10),X10))))))) = X12]. % 0.88/1.25 [7=param(1,6),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12))),inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(X13,inverse(multiply(inverse(multiply(inverse(multiply(X14,X13)),multiply(X14,X12))),inverse(multiply(inverse(X13),X13))))))]. % 0.88/1.25 [8=param(1,5),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(X11),X11)))]. % 0.88/1.25 [9=param(6,5),[], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X10),X10))))))) = inverse(multiply(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(X11),X11))))]. % 0.88/1.25 [10=param(8,1),[], % 0.88/1.25 multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(X12))))))),inverse(multiply(inverse(X11),X11))) = X12]. % 0.88/1.25 [13=param(8,8),[10], % 0.88/1.25 inverse(multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),X12)),inverse(multiply(inverse(X11),X11))))))))) = inverse(X12)]. % 0.88/1.25 [16=param(1,10),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,inverse(inverse(multiply(X12,inverse(X13))))))),X10)),X13)),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(X12),X12)]. % 0.88/1.25 [17=param(1,13),[1], % 0.88/1.25 multiply(X11,inverse(inverse(multiply(X12,inverse(multiply(inverse(multiply(inverse(multiply(X11,X12)),X10)),inverse(multiply(inverse(X12),X12)))))))) = X10]. % 0.88/1.25 [21=param(17,17),[], % 0.88/1.25 inverse(inverse(multiply(X13,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),X13)),X12)),inverse(multiply(inverse(X13),X13))))))) = multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),inverse(multiply(inverse(X11),X11))))))))]. % 0.88/1.25 [22=param(17,21),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),inverse(multiply(inverse(X11),X11))))))))) = X12]. % 0.88/1.25 [23=param(22,1),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(X12))) = multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(X12)))]. % 0.88/1.25 [25=param(22,4),[1], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 0.88/1.25 [27=param(22,8),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X12,X13)),multiply(X12,inverse(inverse(X14))))),inverse(multiply(inverse(X13),X13)))))) = multiply(inverse(multiply(X13,X11)),X14)]. % 0.88/1.25 [29=param(22,21),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(X12,inverse(inverse(multiply(X13,inverse(multiply(inverse(X14),inverse(multiply(inverse(X13),X13)))))))))) = multiply(inverse(multiply(inverse(multiply(X12,X13)),X11)),X14)]. % 0.88/1.25 [38=param(22,25),[], % 0.88/1.25 multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,inverse(inverse(multiply(multiply(X11,X12),inverse(multiply(inverse(X13),inverse(multiply(inverse(multiply(X14,X12)),multiply(X14,X12)))))))))) = X13]. % 0.88/1.25 [39=param(25,25),[], % 0.88/1.25 multiply(inverse(multiply(inverse(multiply(X10,X11)),X12)),multiply(inverse(multiply(X13,X11)),multiply(X13,X14))) = multiply(inverse(multiply(X15,X12)),multiply(X15,multiply(X10,X14)))]. % 0.88/1.25 [51=param(16,8),[1], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X10),X10)))))))) = multiply(inverse(X10),X10)]. % 0.88/1.25 [57=param(17,51),[], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(X10),inverse(inverse(multiply(X10,inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X10),X10))))))))]. % 0.88/1.25 [58=demod(51),[57], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X10),inverse(inverse(multiply(X10,inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X10),X10)))))))))) = multiply(inverse(X10),X10)]. % 0.88/1.25 [59=param(58,23),[], % 0.88/1.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(multiply(inverse(X11),X11),inverse(multiply(inverse(X11),X11)))))))))) = multiply(inverse(X11),X11)]. % 0.88/1.25 [60=param(22,57),[59], % 0.88/1.25 multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,inverse(multiply(inverse(X11),X11)))) = multiply(inverse(X12),X12)]. % 0.88/1.25 [63=param(60,10),[10], % 0.88/1.25 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 0.88/1.25 [85=param(22,60),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(multiply(X12,inverse(multiply(inverse(X13),X13)))),multiply(X12,inverse(multiply(inverse(X13),X13)))))))))) = inverse(multiply(inverse(X11),X11))]. % 0.88/1.25 [90=param(38,60),[85], % 0.88/1.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X11))) = inverse(multiply(inverse(multiply(X12,X11)),multiply(X12,X11)))]. % 0.88/1.25 [92=param(1,63),[], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(inverse(X10)),inverse(X10))))))) = X10]. % 0.88/1.25 [94=param(1,63),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X11)),X10)),multiply(inverse(X12),X12))),inverse(multiply(inverse(X10),X10)))))) = X11]. % 0.88/1.25 [98=param(6,63),[], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(X10),X10))))))) = X10]. % 0.88/1.25 [101=param(6,63),[], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12))),inverse(multiply(inverse(X13),X13))))))) = X12]. % 0.88/1.25 [105=param(8,63),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X11),X11)),X12)),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(multiply(inverse(multiply(X13,inverse(X10))),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(inverse(X10)),inverse(X10))))]. % 0.88/1.25 [106=param(8,63),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X13),X13)))))) = multiply(inverse(multiply(inverse(multiply(X14,X11)),multiply(X14,inverse(inverse(X12))))),inverse(multiply(inverse(X11),X11)))]. % 0.88/1.25 [114=param(17,63),[], % 0.88/1.25 multiply(inverse(X10),inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X11),X11)),X12)),inverse(multiply(inverse(X10),X10)))))))) = X12]. % 0.88/1.25 [121=param(22,63),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),X12))))))) = inverse(multiply(inverse(X11),X11))]. % 0.88/1.25 [122=param(22,63),[], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),inverse(multiply(inverse(X13),X13))))))))) = X12]. % 0.88/1.25 [124=param(25,63),[], % 0.88/1.25 multiply(inverse(multiply(inverse(X10),X11)),multiply(inverse(X12),X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X10))]. % 0.88/1.25 [142=param(98,63),[], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(X12),X12))))))) = X10]. % 0.88/1.25 [153=param(9,124),[101], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(multiply(X11,inverse(X10))),multiply(X11,inverse(inverse(multiply(inverse(X12),X12)))))),inverse(multiply(inverse(inverse(X10)),inverse(X10))))) = X10]. % 0.88/1.25 [159=param(124,63),[], % 0.88/1.25 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 0.88/1.25 [160=param(142,124),[], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X11),X11)),multiply(inverse(X12),X12))),inverse(multiply(inverse(X13),X13))))))) = X10]. % 0.88/1.25 [174=param(8,27),[122], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(X14),X14)))]. % 0.88/1.25 [175=param(9,27),[122], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X10),X10))))))) = inverse(multiply(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(X14),X14))))]. % 0.88/1.25 [176=param(27,63),[], % 0.88/1.25 multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(X12))))),inverse(multiply(inverse(X11),X11))))),X13)),multiply(inverse(X14),X14)) = multiply(inverse(multiply(X11,X13)),X12)]. % 0.88/1.25 [178=param(90,39),[], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))) = inverse(multiply(inverse(multiply(X14,multiply(X10,X12))),multiply(X14,multiply(X10,X12))))]. % 0.88/1.25 [182=param(90,124),[], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11))) = inverse(multiply(inverse(multiply(X12,X10)),multiply(X12,X10)))]. % 0.88/1.25 [188=param(9,121),[10], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X10),X10))))))) = inverse(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))))]. % 0.88/1.25 [196=param(121,63),[], % 0.88/1.25 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),X12))))))) = inverse(multiply(inverse(X11),X11))]. % 0.88/1.25 [203=param(121,159),[], % 0.88/1.25 multiply(inverse(multiply(inverse(inverse(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))))),X10)),multiply(inverse(multiply(inverse(X12),X12)),multiply(inverse(X13),X13))) = inverse(multiply(inverse(X10),X10))]. % 0.88/1.25 [207=param(92,63),[], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(X12),X12)))))) = X10]. % 0.88/1.25 [223=param(207,29),[], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(multiply(X11,multiply(X12,X13))),multiply(X11,multiply(X12,inverse(inverse(multiply(X13,inverse(multiply(inverse(inverse(multiply(inverse(X14),X14))),inverse(multiply(inverse(X13),X13))))))))))))) = X10]. % 0.88/1.25 [225=param(207,39),[], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(multiply(inverse(multiply(X12,X13)),multiply(X12,X14))),multiply(inverse(multiply(X15,X13)),multiply(X15,X14)))))))) = X10]. % 0.88/1.25 [229=param(121,207),[142], % 0.88/1.25 multiply(inverse(multiply(X10,X11)),multiply(X10,X11)) = inverse(multiply(inverse(X11),X11))]. % 0.88/1.25 [230=demod(182),[229], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11))) = inverse(inverse(multiply(inverse(X10),X10)))]. % 0.88/1.25 [234=demod(160),[230], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(inverse(multiply(inverse(X11),X11))),inverse(multiply(inverse(X12),X12))))))) = X10]. % 0.88/1.25 [235=demod(223),[234,229,229], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = X10]. % 0.88/1.25 [237=demod(188),[234], % 0.88/1.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(X11),X11))))) = X10]. % 0.88/1.25 [239=demod(196),[237], % 0.88/1.25 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11)) = inverse(multiply(inverse(X11),X11))]. % 0.88/1.25 [249=demod(176),[237], % 0.88/1.25 multiply(inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(X12))))),X13)),multiply(inverse(X14),X14)) = multiply(inverse(multiply(X11,X13)),X12)]. % 0.88/1.25 [250=demod(203),[237,239], % 0.88/1.25 multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(inverse(X11),X11))) = inverse(multiply(inverse(X10),X10))]. % 0.88/1.25 [258=demod(207),[250], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 0.88/1.25 [276=demod(178),[229,229], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))) = inverse(inverse(inverse(multiply(inverse(X12),X12))))]. % 0.88/1.25 [277=demod(225),[276,235], % 0.88/1.25 inverse(multiply(inverse(X10),multiply(inverse(X11),X11))) = X10]. % 0.88/1.25 [278=demod(94),[277], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(multiply(inverse(inverse(X11)),X10),inverse(multiply(inverse(X10),X10)))))) = X11]. % 0.88/1.25 [292=param(7,277),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(multiply(inverse(X11),X10),inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(X12,inverse(multiply(inverse(multiply(inverse(multiply(X13,X12)),multiply(X13,X11))),inverse(multiply(inverse(X12),X12))))))]. % 0.88/1.25 [293=param(7,277),[229,258], % 0.88/1.25 inverse(multiply(multiply(inverse(X10),X10),multiply(X11,multiply(inverse(X11),X12)))) = inverse(multiply(X13,inverse(multiply(inverse(multiply(inverse(multiply(X14,X13)),multiply(X14,X12))),inverse(multiply(inverse(X13),X13))))))]. % 0.88/1.25 [295=param(8,277),[], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(multiply(X11,X10),inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(multiply(inverse(multiply(X12,X11)),multiply(X12,inverse(inverse(multiply(inverse(X13),X13)))))),inverse(multiply(inverse(X11),X11)))]. % 0.88/1.25 [296=param(8,277),[229,258], % 0.88/1.25 inverse(multiply(multiply(inverse(X10),X10),multiply(X11,X12))) = multiply(inverse(multiply(inverse(multiply(X13,inverse(X11))),multiply(X13,inverse(inverse(X12))))),inverse(multiply(inverse(inverse(X11)),inverse(X11))))]. % 0.88/1.25 [298=param(277,9),[249], % 0.88/1.25 inverse(multiply(X12,inverse(multiply(inverse(multiply(inverse(multiply(X10,X12)),X11)),inverse(multiply(inverse(X12),X12)))))) = inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))),X11))]. % 0.88/1.25 [302=demod(293),[298], % 0.88/1.25 inverse(multiply(multiply(inverse(X10),X10),multiply(X11,multiply(inverse(X11),X12)))) = inverse(multiply(inverse(multiply(X13,inverse(multiply(inverse(X13),X13)))),multiply(X13,X12)))]. % 0.88/1.25 [309=demod(292),[298], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(multiply(inverse(X11),X10),inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))),multiply(X12,X11)))]. % 0.88/1.25 [310=demod(175),[298], % 0.88/1.25 inverse(multiply(inverse(multiply(inverse(multiply(X12,X10)),multiply(X12,inverse(inverse(X11))))),inverse(multiply(inverse(X13),X13)))) = inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))),X11)))]. % 0.88/1.25 [316=demod(153),[310,277], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(inverse(X10)),inverse(X10))))) = X10]. % 0.88/1.25 [318=demod(174),[298], % 0.88/1.25 multiply(inverse(multiply(inverse(multiply(X12,X10)),multiply(X12,inverse(inverse(X11))))),inverse(multiply(inverse(X13),X13))) = inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))),X11))]. % 0.88/1.25 [320=demod(106),[318], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X10)),X12)),inverse(multiply(inverse(X13),X13)))))) = inverse(multiply(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))),X12))]. % 0.88/1.25 [322=demod(295),[318,277], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(multiply(X11,X10),inverse(multiply(inverse(X10),X10)))))) = multiply(X11,inverse(multiply(inverse(X11),X11)))]. % 0.88/1.25 [323=demod(278),[322], % 0.88/1.25 multiply(inverse(inverse(X10)),inverse(multiply(inverse(inverse(inverse(X10))),inverse(inverse(X10))))) = X10]. % 0.88/1.25 [324=demod(309),[322], % 0.88/1.25 multiply(inverse(X10),inverse(multiply(inverse(inverse(X10)),inverse(X10)))) = inverse(multiply(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))),multiply(X11,X10)))]. % 0.88/1.25 [338=demod(105),[318,316], % 0.88/1.25 inverse(multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X11),X11)),X12)),inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(X10,X12))]. % 0.88/1.25 [341=demod(114),[338], % 0.88/1.25 multiply(inverse(X10),inverse(inverse(multiply(X10,X11)))) = X11]. % 0.88/1.25 [342=demod(296),[318,316], % 0.88/1.25 inverse(multiply(multiply(inverse(X10),X10),multiply(X11,X12))) = inverse(multiply(X11,X12))]. % 0.88/1.25 [347=demod(302),[342], % 0.88/1.25 inverse(multiply(X10,multiply(inverse(X10),X11))) = inverse(multiply(inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))),multiply(X12,X11)))]. % 0.88/1.25 [348=demod(21),[320,316], % 0.88/1.25 inverse(inverse(multiply(multiply(X10,X11),X12))) = multiply(X10,inverse(inverse(multiply(X11,inverse(multiply(inverse(X12),inverse(multiply(inverse(X11),X11))))))))]. % 0.88/1.25 [354=param(277,25),[229], % 0.88/1.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(X11),X11)))) = X10]. % 0.88/1.25 [368=demod(348),[354], % 0.88/1.25 inverse(inverse(multiply(multiply(X10,X11),X12))) = multiply(X10,inverse(inverse(multiply(X11,X12))))]. % 0.88/1.25 [408=param(341,277),[368,368,341], % 0.88/1.25 multiply(X10,multiply(inverse(X10),X11)) = X11]. % 0.88/1.25 [410=demod(347),[408], % 0.88/1.25 inverse(multiply(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))),multiply(X11,X10))) = inverse(X10)]. % 0.88/1.25 [412=demod(324),[410], % 0.88/1.25 multiply(inverse(X10),inverse(multiply(inverse(inverse(X10)),inverse(X10)))) = inverse(X10)]. % 0.88/1.25 [415=demod(323),[412], % 0.88/1.25 inverse(inverse(X10)) = X10]. % 0.88/1.25 [442=demod(368),[415,415], % 0.88/1.25 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 0.88/1.25 [518=param(3,442),[2], % 0.88/1.25 thmtrue = thmfalse]. % 0.88/1.25 % SZS output end CNFRefutation % 0.88/1.25 Space: 758 KB %------------------------------------------------------------------------------