%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP419-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n011.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 8.87s 9.25s % Output : CNFRefutation 8.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : GRP419-1 : TPTP v8.1.0. Released v2.6.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n011.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 23:28:34 EDT 2022 % 0.13/0.35 % CPUTime : % 8.87/9.25 Theorem Proved. % 8.87/9.25 % SZS status Unsatisfiable % 8.87/9.25 % SZS output start CNFRefutation % 8.87/9.25 [1=axiom,[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12))) = X11]. % 8.87/9.25 [2=axiom,[], % 8.87/9.25 thtop(X10,X10) = thmfalse]. % 8.87/9.25 [3=axiom,[], % 8.87/9.25 thtop(multiply(multiply(inverse(b2),b2),a2),a2) = thmtrue]. % 8.87/9.25 [4=param(1,1),[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12))) = multiply(inverse(multiply(X13,inverse(multiply(inverse(X11),inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))),multiply(X13,X14))]. % 8.87/9.25 [5=param(4,1),[], % 8.87/9.25 multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X11)),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12)) = X11]. % 8.87/9.25 [6=param(4,4),[5], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12)))) = X11]. % 8.87/9.25 [7=param(1,6),[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12))) = inverse(multiply(inverse(multiply(X13,inverse(multiply(X11,inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))),multiply(X13,X14)))]. % 8.87/9.25 [8=param(1,7),[1], % 8.87/9.25 multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12)) = multiply(inverse(multiply(X13,inverse(multiply(X11,inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))),multiply(X13,X14))]. % 8.87/9.25 [9=param(1,5),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X11)),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),inverse(multiply(inverse(X13),inverse(multiply(multiply(X10,X12),inverse(multiply(inverse(multiply(X10,X12)),multiply(X10,X12))))))))),X11)) = X13]. % 8.87/9.25 [11=param(1,9),[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))) = multiply(inverse(multiply(X13,inverse(multiply(inverse(inverse(inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))),inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))),inverse(multiply(inverse(X11),inverse(multiply(multiply(X13,X14),inverse(multiply(inverse(multiply(X13,X14)),multiply(X13,X14))))))))]. % 8.87/9.25 [12=param(1,11),[5], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [13=param(8,11),[5], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))) = multiply(inverse(multiply(X13,inverse(multiply(inverse(X11),inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))),multiply(X13,X14))]. % 8.87/9.25 [14=param(12,1),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(X10,multiply(inverse(multiply(X11,inverse(multiply(inverse(X10),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),X13)))),inverse(multiply(X13,inverse(multiply(inverse(X13),X13)))))) = multiply(X11,X12)]. % 8.87/9.25 [15=param(1,12),[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))]. % 8.87/9.25 [19=param(6,12),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))) = inverse(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12))))]. % 8.87/9.25 [21=param(8,12),[5], % 8.87/9.25 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 8.87/9.25 [27=param(13,5),[], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [70=param(14,5),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(multiply(X11,X12),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X12))))))) = multiply(X11,X12)]. % 8.87/9.25 [110=param(8,70),[5], % 8.87/9.25 multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X12))) = multiply(inverse(X13),X13)]. % 8.87/9.25 [122=param(110,5),[5], % 8.87/9.25 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 8.87/9.25 [149=param(3,110),[], % 8.87/9.25 thtop(multiply(multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X12))),a2),a2) = thmtrue]. % 8.87/9.25 [200=param(6,122),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,X12)))) = inverse(inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))]. % 8.87/9.25 [201=param(6,122),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X13),X13)))))))),multiply(X10,X12)))) = X11]. % 8.87/9.25 [210=param(12,122),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))) = X11]. % 8.87/9.25 [229=param(27,122),[], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X11),inverse(multiply(inverse(inverse(X11)),inverse(X11)))))) = X11]. % 8.87/9.25 [249=param(13,210),[5], % 8.87/9.25 multiply(inverse(inverse(multiply(X10,multiply(inverse(inverse(multiply(inverse(X11),X11))),X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))) = multiply(X10,inverse(multiply(inverse(X10),X10)))]. % 8.87/9.25 [262=param(210,122),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [270=param(12,262),[249], % 8.87/9.25 inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))) = inverse(multiply(X10,inverse(multiply(inverse(X11),X11))))]. % 8.87/9.25 [271=param(13,262),[249,5], % 8.87/9.25 multiply(X10,inverse(multiply(inverse(X10),X10))) = multiply(X10,inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [285=param(262,122),[], % 8.87/9.25 inverse(multiply(inverse(X10),X10)) = inverse(inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [301=param(262,262),[], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [304=param(262,262),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(inverse(multiply(inverse(X12),X12))))))) = X11]. % 8.87/9.25 [331=param(285,262),[], % 8.87/9.25 inverse(inverse(multiply(inverse(X10),X10))) = inverse(inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [340=param(262,285),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [350=param(122,331),[], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [353=param(12,271),[27], % 8.87/9.25 inverse(multiply(inverse(X10),X10)) = inverse(multiply(inverse(X11),X11))]. % 8.87/9.25 [368=param(271,122),[], % 8.87/9.25 multiply(X10,inverse(multiply(inverse(X11),X11))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 8.87/9.25 [375=param(271,285),[], % 8.87/9.25 multiply(X10,inverse(inverse(multiply(inverse(X11),X11)))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 8.87/9.25 [393=param(262,271),[304], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [415=param(353,271),[304], % 8.87/9.25 inverse(inverse(inverse(multiply(inverse(X10),X10)))) = inverse(multiply(inverse(X11),X11))]. % 8.87/9.25 [424=param(122,415),[], % 8.87/9.25 multiply(inverse(multiply(inverse(X10),X10)),inverse(inverse(multiply(inverse(X11),X11)))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [455=param(122,415),[], % 8.87/9.25 multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 8.87/9.25 [462=param(271,415),[], % 8.87/9.25 multiply(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 8.87/9.25 [541=param(12,368),[340], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(inverse(multiply(inverse(X13),X13))))) = X11]. % 8.87/9.25 [566=param(27,375),[27], % 8.87/9.25 multiply(inverse(X10),X10) = inverse(multiply(inverse(X11),X11))]. % 8.87/9.25 [567=param(27,375),[304], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(inverse(inverse(multiply(inverse(X13),X13))))) = X11]. % 8.87/9.25 [637=param(566,262),[], % 8.87/9.25 multiply(inverse(X10),X10) = inverse(inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [640=param(262,566),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [642=param(271,566),[], % 8.87/9.25 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 8.87/9.25 [646=param(566,415),[], % 8.87/9.25 multiply(inverse(X10),X10) = inverse(inverse(inverse(multiply(inverse(X11),X11))))]. % 8.87/9.25 [685=param(19,637),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X11)),inverse(inverse(multiply(inverse(X12),X12)))))) = inverse(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X10))))]. % 8.87/9.25 [711=param(122,637),[], % 8.87/9.25 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [712=param(262,637),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [805=param(353,646),[], % 8.87/9.25 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = inverse(multiply(inverse(X11),X11))]. % 8.87/9.25 [810=param(646,566),[], % 8.87/9.25 multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11)) = inverse(inverse(inverse(multiply(inverse(X12),X12))))]. % 8.87/9.25 [817=param(122,646),[], % 8.87/9.25 multiply(multiply(inverse(X10),X10),inverse(inverse(multiply(inverse(X11),X11)))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [844=param(805,415),[], % 8.87/9.25 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = inverse(inverse(inverse(multiply(inverse(X11),X11))))]. % 8.87/9.25 [846=param(805,566),[], % 8.87/9.25 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = multiply(inverse(X11),X11)]. % 8.87/9.25 [914=param(262,846),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))) = inverse(inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [924=param(353,846),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(inverse(X11),X11))]. % 8.87/9.25 [1004=param(642,375),[], % 8.87/9.25 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))]. % 8.87/9.25 [1134=param(12,1004),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))))),inverse(multiply(multiply(inverse(X13),X13),inverse(multiply(inverse(multiply(inverse(X13),X13)),multiply(inverse(X13),X13))))))) = X11]. % 8.87/9.25 [1176=param(1004,637),[], % 8.87/9.25 multiply(X10,inverse(inverse(multiply(inverse(X11),X11)))) = multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))]. % 8.87/9.25 [1221=param(924,566),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(X11),X11)]. % 8.87/9.25 [1411=param(12,711),[340], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),multiply(inverse(X12),X12)))),inverse(inverse(multiply(inverse(X13),X13))))) = X11]. % 8.87/9.25 [1416=param(15,711),[], % 8.87/9.25 inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),multiply(inverse(X12),X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(multiply(inverse(X14),X14)))))]. % 8.87/9.25 [1661=param(712,566),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [1667=demod(1134),[1661], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))))),inverse(multiply(inverse(X13),X13)))) = X11]. % 8.87/9.25 [1712=param(712,711),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [1715=param(712,712),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),inverse(inverse(multiply(inverse(X11),X11))))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [1762=param(1661,15),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X13))))) = inverse(multiply(inverse(X13),X12))]. % 8.87/9.25 [1807=param(1661,566),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [1822=param(1661,646),[], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [2014=param(1712,566),[], % 8.87/9.25 inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [2146=param(19,2014),[], % 8.87/9.25 inverse(inverse(multiply(multiply(inverse(X10),X10),multiply(multiply(inverse(X11),X11),X12)))) = inverse(inverse(multiply(inverse(multiply(X13,multiply(inverse(X14),X14))),multiply(X13,X12))))]. % 8.87/9.25 [2180=param(2014,566),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 8.87/9.25 [2462=param(2180,1221),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))) = multiply(inverse(X11),X11)]. % 8.87/9.25 [2667=param(2180,2462),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))))) = multiply(inverse(X11),X11)]. % 8.87/9.25 [2732=param(27,2667),[], % 8.87/9.25 multiply(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))))))),inverse(multiply(inverse(X11),inverse(multiply(inverse(inverse(X11)),inverse(X11)))))) = X11]. % 8.87/9.25 [2780=param(2180,2667),[], % 8.87/9.25 inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))))) = multiply(inverse(X11),X11)]. % 8.87/9.25 [3440=param(19,817),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(multiply(inverse(X11),X11),X12)))) = inverse(inverse(multiply(inverse(multiply(X13,inverse(inverse(multiply(inverse(X14),X14))))),multiply(X13,X12))))]. % 8.87/9.25 [4505=param(12,640),[249], % 8.87/9.25 inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))) = inverse(multiply(X10,multiply(inverse(X11),X11)))]. % 8.87/9.25 [4677=param(4505,285),[], % 8.87/9.25 inverse(multiply(X10,inverse(inverse(multiply(inverse(X11),X11))))) = inverse(multiply(X10,multiply(inverse(X12),X12)))]. % 8.87/9.25 [4681=param(4505,375),[262], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),multiply(inverse(X11),X11))) = inverse(inverse(inverse(multiply(inverse(X10),X10))))]. % 8.87/9.25 [4685=param(4505,566),[], % 8.87/9.25 inverse(multiply(X10,multiply(inverse(X11),X11))) = inverse(multiply(X10,multiply(inverse(X12),X12)))]. % 8.87/9.25 [4720=param(4505,914),[], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(inverse(inverse(multiply(inverse(X11),X11))),inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))))) = inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),multiply(inverse(X12),X12)))]. % 8.87/9.25 [4892=param(149,4685),[], % 8.87/9.25 thtop(multiply(multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,multiply(inverse(X12),X12))),a2),a2) = thmtrue]. % 8.87/9.25 [5205=param(4681,262),[262], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),multiply(inverse(X11),X11))) = inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))]. % 8.87/9.25 [5215=param(4681,271),[304], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),multiply(inverse(X11),X11))) = inverse(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X10),X10))))))]. % 8.87/9.25 [5218=demod(4720),[5215], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(inverse(inverse(multiply(inverse(X11),X11))),inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))))) = inverse(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X10),X10))))))]. % 8.87/9.25 [5236=param(4681,566),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(inverse(X11),X11)))) = inverse(inverse(inverse(multiply(inverse(X10),X10))))]. % 8.87/9.25 [5238=demod(5218),[5236], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(inverse(inverse(multiply(inverse(X11),X11))),inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))]. % 8.87/9.25 [5306=param(4681,846),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(inverse(inverse(inverse(multiply(inverse(X11),X11))))))) = inverse(inverse(inverse(multiply(inverse(X10),X10))))]. % 8.87/9.25 [5307=demod(5238),[5306], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))]. % 8.87/9.25 [5345=param(1807,4681),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = inverse(inverse(multiply(inverse(X11),X11)))]. % 8.87/9.25 [5414=param(21,340),[], % 8.87/9.25 multiply(X10,multiply(inverse(multiply(inverse(X11),X11)),X12)) = multiply(inverse(multiply(X13,inverse(multiply(X10,inverse(multiply(inverse(X14),X14)))))),multiply(X13,X12))]. % 8.87/9.25 [5652=param(4677,646),[5205], % 8.87/9.25 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = inverse(inverse(inverse(inverse(multiply(inverse(X11),X11)))))]. % 8.87/9.25 [5813=param(4505,5652),[5307,5205], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X11),X11)))))))) = inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))]. % 8.87/9.25 [6228=param(21,2780),[], % 8.87/9.25 multiply(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))))))),multiply(inverse(X11),X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 8.87/9.25 [7580=param(19,1715),[], % 8.87/9.25 inverse(inverse(multiply(multiply(inverse(X10),X10),multiply(multiply(inverse(X11),X11),X12)))) = inverse(inverse(multiply(inverse(multiply(X13,inverse(inverse(multiply(inverse(X14),X14))))),multiply(X13,X12))))]. % 8.87/9.25 [8292=param(27,1176),[304], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))))),inverse(inverse(inverse(multiply(inverse(X13),X13))))) = X11]. % 8.87/9.25 [10045=param(19,462),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,X12)))) = inverse(inverse(multiply(inverse(multiply(X13,inverse(inverse(inverse(multiply(inverse(X14),X14)))))),multiply(X13,X12))))]. % 8.87/9.25 [10049=param(27,462),[5307,5813], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))) = X11]. % 8.87/9.25 [10073=param(11,462),[5236,5345,393], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(inverse(multiply(inverse(X12),X12))))))) = multiply(inverse(multiply(X13,X14)),inverse(multiply(inverse(X11),inverse(multiply(multiply(X13,X14),inverse(multiply(inverse(multiply(X13,X14)),multiply(X13,X14))))))))]. % 8.87/9.25 [10078=param(27,462),[5236,5345], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(inverse(inverse(multiply(inverse(X12),X12)))))))),inverse(inverse(multiply(inverse(X13),X13)))) = X11]. % 8.87/9.25 [10083=param(462,642),[], % 8.87/9.25 multiply(X10,inverse(inverse(inverse(multiply(inverse(X11),X11))))) = multiply(X10,multiply(inverse(X12),X12))]. % 8.87/9.25 [10107=param(19,10083),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,X12)))) = inverse(inverse(multiply(inverse(multiply(X13,inverse(inverse(inverse(multiply(inverse(X14),X14)))))),multiply(X13,X12))))]. % 8.87/9.25 [10112=param(27,10083),[5307,5813], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,multiply(inverse(X12),X12))))),inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))) = X11]. % 8.87/9.25 [10119=param(10083,810),[], % 8.87/9.25 multiply(X10,multiply(multiply(inverse(X11),X11),multiply(inverse(X12),X12))) = multiply(X10,multiply(inverse(X13),X13))]. % 8.87/9.25 [10121=param(10083,844),[], % 8.87/9.25 multiply(X10,inverse(inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = multiply(X10,multiply(inverse(X12),X12))]. % 8.87/9.25 [10490=param(12,10121),[], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))))),inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13))))),inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))),inverse(inverse(inverse(inverse(multiply(inverse(X13),X13))))))))))) = X11]. % 8.87/9.25 [10499=param(27,10121),[], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,multiply(inverse(X12),X12))))),inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13))))),inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))),inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))))))) = X11]. % 8.87/9.25 [10665=param(11,455),[1762,301], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),X11)),multiply(inverse(X12),X12))) = multiply(inverse(multiply(X13,X14)),inverse(multiply(inverse(X11),inverse(multiply(multiply(X13,X14),inverse(multiply(inverse(multiply(X13,X14)),multiply(X13,X14))))))))]. % 8.87/9.25 [10706=param(19,424),[], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(multiply(inverse(X11),X11)),X12)))) = inverse(inverse(multiply(inverse(multiply(X13,inverse(inverse(multiply(inverse(X14),X14))))),multiply(X13,X12))))]. % 8.87/9.25 [10994=param(15,350),[], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),X11)),multiply(inverse(X12),X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,inverse(multiply(inverse(X14),X14)))))]. % 8.87/9.25 [11199=param(270,914),[5306,5307], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(inverse(X11),X11)))) = inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))]. % 8.87/9.25 [11200=demod(10499),[11199], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,multiply(inverse(X12),X12))))),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13))))))) = X11]. % 8.87/9.25 [11201=demod(10490),[11199], % 8.87/9.25 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))))),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X13),X13)))))))) = X11]. % 8.87/9.25 [11962=param(1822,4),[201], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),X11)) = inverse(multiply(inverse(X12),inverse(multiply(inverse(X11),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))))))]. % 8.87/9.25 [12934=param(10119,5),[1762,712], % 8.87/9.25 multiply(inverse(inverse(X10)),multiply(inverse(X11),X11)) = X10]. % 8.87/9.25 [12998=param(15,10119),[], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12)))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,multiply(multiply(inverse(X14),X14),multiply(inverse(X15),X15)))))]. % 8.87/9.25 [13124=param(11,10119),[1762,301], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(multiply(inverse(X12),X12),multiply(inverse(X13),X13))))) = multiply(inverse(multiply(X14,X15)),inverse(multiply(inverse(X11),inverse(multiply(multiply(X14,X15),inverse(multiply(inverse(multiply(X14,X15)),multiply(X14,X15))))))))]. % 8.87/9.25 [13297=param(12934,415),[12934], % 8.87/9.25 multiply(inverse(inverse(X10)),inverse(multiply(inverse(X11),X11))) = X10]. % 8.87/9.25 [13298=demod(1667),[13297], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12)))))) = X11]. % 8.87/9.25 [13308=demod(8292),[13298], % 8.87/9.25 multiply(inverse(inverse(X10)),inverse(inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 8.87/9.25 [13309=demod(567),[13308], % 8.87/9.25 multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))) = X11]. % 8.87/9.25 [13329=demod(10049),[13309], % 8.87/9.25 multiply(inverse(inverse(X10)),inverse(inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = X10]. % 8.87/9.25 [13330=demod(10112),[13329], % 8.87/9.25 multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,multiply(inverse(X12),X12))) = X11]. % 8.87/9.25 [13351=demod(11200),[13330], % 8.87/9.25 multiply(inverse(inverse(X10)),inverse(inverse(inverse(inverse(inverse(multiply(inverse(X11),X11))))))) = X10]. % 8.87/9.25 [13353=demod(11201),[13351], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12)))) = X11]. % 8.87/9.25 [13355=demod(12998),[13353], % 8.87/9.25 inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,multiply(multiply(inverse(X12),X12),multiply(inverse(X13),X13))))) = X10]. % 8.87/9.25 [13356=demod(13124),[13355], % 8.87/9.25 multiply(inverse(multiply(X11,X12)),inverse(multiply(inverse(X10),inverse(multiply(multiply(X11,X12),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X12)))))))) = X10]. % 8.87/9.25 [13358=demod(10665),[13356], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),X11)),multiply(inverse(X12),X12))) = X11]. % 8.87/9.25 [13360=demod(10073),[13356], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(inverse(multiply(inverse(X12),X12))))))) = X11]. % 8.87/9.25 [13361=demod(10078),[13360], % 8.87/9.25 multiply(inverse(inverse(X10)),inverse(inverse(multiply(inverse(X11),X11)))) = X10]. % 8.87/9.25 [13363=demod(541),[13361], % 8.87/9.25 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12))))) = X11]. % 8.87/9.25 [13365=demod(10994),[13363], % 8.87/9.25 inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),X11)),multiply(inverse(X12),X12))) = X11]. % 8.87/9.25 [13375=demod(1416),[13363], % 8.87/9.25 inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),multiply(inverse(X12),X12))) = X11]. % 8.87/9.25 [13376=demod(1411),[13375], % 8.87/9.25 inverse(multiply(inverse(X10),inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 8.87/9.25 [13381=demod(685),[13376], % 8.87/9.25 inverse(multiply(inverse(X10),X11)) = inverse(inverse(multiply(inverse(multiply(X12,X11)),multiply(X12,X10))))]. % 8.87/9.25 [13383=demod(201),[-13381], % 8.87/9.25 inverse(multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(X10,inverse(multiply(inverse(X12),X12)))))))) = X11]. % 8.87/9.25 [13449=demod(11962),[13383], % 8.87/9.25 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),X11)) = inverse(X11)]. % 8.87/9.25 [13450=demod(301),[13449], % 8.87/9.25 inverse(inverse(multiply(X10,inverse(multiply(inverse(X11),X11))))) = X10]. % 8.87/9.25 [13464=demod(200),[13450], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,X12)))) = X12]. % 8.87/9.25 [13465=demod(10045),[13464], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X11,inverse(inverse(inverse(multiply(inverse(X12),X12)))))),multiply(X11,X10)))) = X10]. % 8.87/9.25 [13466=demod(10107),[13465], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,X12)))) = X12]. % 8.87/9.25 [13483=demod(2146),[13466], % 8.87/9.25 inverse(inverse(multiply(multiply(inverse(X10),X10),multiply(multiply(inverse(X11),X11),X12)))) = X12]. % 8.87/9.25 [13484=demod(7580),[13483], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(X11,inverse(inverse(multiply(inverse(X12),X12))))),multiply(X11,X10)))) = X10]. % 8.87/9.25 [13485=demod(10706),[13484], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(multiply(inverse(X11),X11)),X12)))) = X12]. % 8.87/9.25 [13489=demod(3440),[13484], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(multiply(inverse(X11),X11),X12)))) = X12]. % 8.87/9.25 [13583=demod(13358),[13449], % 8.87/9.25 inverse(multiply(inverse(X10),multiply(inverse(X11),X11))) = X10]. % 8.87/9.25 [13809=demod(13365),[13583], % 8.87/9.25 multiply(inverse(inverse(multiply(inverse(X10),X10))),X11) = X11]. % 8.87/9.25 [13810=demod(229),[13809], % 8.87/9.25 inverse(multiply(inverse(X10),inverse(multiply(inverse(inverse(X10)),inverse(X10))))) = X10]. % 8.87/9.25 [13812=demod(2732),[13810], % 8.87/9.25 multiply(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))))))),X11) = X11]. % 8.87/9.25 [13813=demod(6228),[13812], % 8.87/9.25 multiply(inverse(multiply(X12,X10)),multiply(X12,X11)) = multiply(inverse(X10),X11)]. % 8.87/9.25 [14067=demod(5414),[13813,13450], % 8.87/9.25 multiply(X10,multiply(inverse(multiply(inverse(X11),X11)),X12)) = multiply(X10,X12)]. % 8.87/9.25 [14068=demod(13485),[14067], % 8.87/9.25 inverse(inverse(multiply(inverse(multiply(inverse(X10),X10)),X11))) = X11]. % 8.87/9.25 [14125=demod(13489),[14068], % 8.87/9.25 multiply(multiply(inverse(X10),X10),X11) = X11]. % 8.87/9.25 [14416=param(4892,122),[14125,2], % 8.87/9.25 thmtrue = thmfalse]. % 8.87/9.25 % SZS output end CNFRefutation % 8.87/9.25 Space: 17954 KB %------------------------------------------------------------------------------