%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP420-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n026.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:58 EDT 2022 % Result : Unsatisfiable 4.27s 4.67s % Output : CNFRefutation 4.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP420-1 : TPTP v8.1.0. Released v2.6.0. % 0.12/0.14 % Command : fiesta-wrapper %s % 0.14/0.35 % Computer : n026.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Tue Jun 14 03:52:06 EDT 2022 % 0.14/0.35 % CPUTime : % 4.27/4.67 Theorem Proved. % 4.27/4.67 % SZS status Unsatisfiable % 4.27/4.67 % SZS output start CNFRefutation % 4.27/4.67 [1=axiom,[], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12))) = X11]. % 4.27/4.67 [2=axiom,[], % 4.27/4.67 thtop(X10,X10) = thmfalse]. % 4.27/4.67 [3=axiom,[], % 4.27/4.67 thtop(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) = thmtrue]. % 4.27/4.67 [4=param(1,1),[], % 4.27/4.67 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))]. % 4.27/4.67 [5=param(4,1),[], % 4.27/4.67 multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X11)),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12)) = X11]. % 4.27/4.67 [6=param(4,4),[5], % 4.27/4.67 inverse(inverse(multiply(inverse(multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),multiply(X10,X12)))) = X11]. % 4.27/4.67 [7=param(1,6),[], % 4.27/4.67 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)))]. % 4.27/4.67 [8=param(1,7),[1], % 4.27/4.67 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))]. % 4.27/4.67 [9=param(1,5),[], % 4.27/4.67 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]. % 4.27/4.67 [11=param(1,9),[], % 4.27/4.67 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))))))))]. % 4.27/4.67 [12=param(1,11),[5], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [13=param(8,11),[5], % 4.27/4.67 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))]. % 4.27/4.67 [14=param(12,1),[], % 4.27/4.67 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)]. % 4.27/4.67 [15=param(1,12),[], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))]. % 4.27/4.67 [18=param(12,5),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X11)),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),X13)),X11))),inverse(multiply(multiply(X10,X12),inverse(multiply(inverse(multiply(X10,X12)),multiply(X10,X12))))))) = X13]. % 4.27/4.67 [19=param(6,12),[], % 4.27/4.67 inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))) = inverse(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12))))]. % 4.27/4.67 [21=param(8,12),[5], % 4.27/4.67 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 4.27/4.67 [22=param(9,12),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X11)),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),X13)),X11)) = inverse(multiply(inverse(multiply(X14,X13)),multiply(X14,multiply(X10,X12))))]. % 4.27/4.67 [27=param(13,5),[], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [45=param(9,21),[], % 4.27/4.67 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(X14,X12)),multiply(X14,X12))))))))),X11)) = X13]. % 4.27/4.67 [47=param(21,12),[], % 4.27/4.67 multiply(X10,multiply(inverse(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12)))),X13)) = multiply(inverse(multiply(X14,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))),multiply(X14,X13))]. % 4.27/4.67 [70=param(14,5),[], % 4.27/4.67 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)]. % 4.27/4.67 [83=param(19,12),[], % 4.27/4.67 inverse(inverse(multiply(X10,multiply(inverse(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12)))),X13)))) = inverse(inverse(multiply(inverse(multiply(X14,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))),multiply(X14,X13))))]. % 4.27/4.67 [110=param(8,70),[5], % 4.27/4.67 multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X12))) = multiply(inverse(X13),X13)]. % 4.27/4.67 [118=param(1,110),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(X10,multiply(X11,X12))),inverse(multiply(inverse(X13),inverse(multiply(multiply(X10,multiply(X11,X12)),inverse(multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X12)))))))))),multiply(inverse(X14),X14))) = X13]. % 4.27/4.67 [122=param(110,5),[5], % 4.27/4.67 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 4.27/4.67 [155=param(6,110),[], % 4.27/4.67 inverse(inverse(multiply(inverse(multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))))))),multiply(inverse(multiply(X12,multiply(X13,X14))),multiply(X12,multiply(X13,X14)))))) = X11]. % 4.27/4.67 [198=param(12,122),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))) = X11]. % 4.27/4.67 [205=param(15,122),[], % 4.27/4.67 inverse(multiply(inverse(X10),X10)) = inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X12)))]. % 4.27/4.67 [215=param(21,122),[], % 4.27/4.67 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 4.27/4.67 [237=param(13,198),[5], % 4.27/4.67 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)))]. % 4.27/4.67 [250=param(198,122),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [258=param(13,250),[237,5], % 4.27/4.67 multiply(X10,inverse(multiply(inverse(X10),X10))) = multiply(X10,inverse(multiply(inverse(X11),X11)))]. % 4.27/4.67 [272=param(250,122),[], % 4.27/4.67 inverse(multiply(inverse(X10),X10)) = inverse(inverse(multiply(inverse(X11),X11)))]. % 4.27/4.67 [284=param(250,250),[], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(multiply(inverse(X10),X10)))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [287=param(250,250),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,inverse(inverse(multiply(inverse(X12),X12))))))) = X11]. % 4.27/4.67 [323=param(250,272),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [348=param(22,205),[5], % 4.27/4.67 inverse(multiply(inverse(X10),X10)) = inverse(multiply(inverse(X11),X11))]. % 4.27/4.67 [457=param(258,19),[], % 4.27/4.67 multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))),inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12)))))) = multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),inverse(multiply(inverse(X14),X14)))]. % 4.27/4.67 [466=param(258,122),[], % 4.27/4.67 multiply(X10,inverse(multiply(inverse(X11),X11))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [473=param(258,272),[], % 4.27/4.67 multiply(X10,inverse(inverse(multiply(inverse(X11),X11)))) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [493=param(250,258),[287], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [495=param(348,258),[287], % 4.27/4.67 inverse(inverse(inverse(multiply(inverse(X10),X10)))) = inverse(multiply(inverse(X11),X11))]. % 4.27/4.67 [595=param(27,466),[323], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(inverse(multiply(inverse(X13),X13)))) = X11]. % 4.27/4.67 [601=param(12,473),[287], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(inverse(inverse(multiply(inverse(X13),X13)))))) = X11]. % 4.27/4.67 [612=param(27,473),[27], % 4.27/4.67 multiply(inverse(X10),X10) = inverse(multiply(inverse(X11),X11))]. % 4.27/4.67 [695=param(612,348),[], % 4.27/4.67 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11)) = inverse(multiply(inverse(X12),X12))]. % 4.27/4.67 [727=param(122,612),[], % 4.27/4.67 multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 4.27/4.67 [728=param(612,250),[], % 4.27/4.67 multiply(inverse(X10),X10) = inverse(inverse(multiply(inverse(X11),X11)))]. % 4.27/4.67 [731=param(250,612),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(X10),X10))),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [733=param(258,612),[], % 4.27/4.67 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [736=param(612,495),[], % 4.27/4.67 multiply(inverse(X10),X10) = inverse(inverse(inverse(multiply(inverse(X11),X11))))]. % 4.27/4.67 [775=param(728,612),[], % 4.27/4.67 multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11)) = inverse(inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [784=param(122,728),[], % 4.27/4.67 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 4.27/4.67 [785=param(250,728),[], % 4.27/4.67 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(X11,inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [818=param(15,736),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(X10),X11)),inverse(inverse(inverse(multiply(inverse(X12),X12)))))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X10)))]. % 4.27/4.67 [859=param(348,736),[], % 4.27/4.67 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = inverse(multiply(inverse(X11),X11))]. % 4.27/4.67 [894=param(859,612),[], % 4.27/4.67 inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))) = multiply(inverse(X11),X11)]. % 4.27/4.67 [983=param(348,894),[], % 4.27/4.67 inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))) = inverse(multiply(inverse(X11),X11))]. % 4.27/4.67 [1004=param(12,733),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(multiply(multiply(inverse(X13),X13),inverse(multiply(inverse(multiply(inverse(X13),X13)),multiply(inverse(X13),X13))))))) = X11]. % 4.27/4.67 [1011=param(15,733),[], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12))))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,multiply(inverse(X14),X14))))]. % 4.27/4.67 [1026=param(27,733),[], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(multiply(multiply(inverse(X13),X13),inverse(multiply(inverse(multiply(inverse(X13),X13)),multiply(inverse(X13),X13)))))) = X11]. % 4.27/4.67 [1059=param(11,733),[323,493], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,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))))))))]. % 4.27/4.67 [1076=param(733,473),[], % 4.27/4.67 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))]. % 4.27/4.67 [1184=param(18,727),[], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))),X12))),inverse(multiply(multiply(X13,X14),inverse(multiply(inverse(multiply(X13,X14)),multiply(X13,X14))))))) = multiply(X13,inverse(multiply(inverse(inverse(X12)),inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))]. % 4.27/4.67 [1213=param(1076,5),[], % 4.27/4.67 multiply(inverse(multiply(inverse(X10),inverse(multiply(inverse(inverse(X11)),inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))))))),inverse(inverse(multiply(inverse(X12),X12)))) = X11]. % 4.27/4.67 [1220=param(12,1076),[], % 4.27/4.67 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]. % 4.27/4.67 [1234=param(19,1076),[], % 4.27/4.67 inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))))) = inverse(inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,multiply(inverse(X14),X14)))))]. % 4.27/4.67 [1281=param(12,1076),[287], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))))),inverse(inverse(inverse(multiply(inverse(X13),X13)))))) = X11]. % 4.27/4.67 [1288=param(27,1076),[287], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,multiply(inverse(X12),X12))))),inverse(inverse(inverse(multiply(inverse(X13),X13))))) = X11]. % 4.27/4.67 [1336=param(983,612),[], % 4.27/4.67 inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))) = multiply(inverse(X11),X11)]. % 4.27/4.67 [1868=param(785,612),[], % 4.27/4.67 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [1876=demod(1220),[1868], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12))))))),inverse(multiply(inverse(X13),X13)))) = X11]. % 4.27/4.67 [1880=demod(1026),[1868], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(multiply(inverse(X13),X13))) = X11]. % 4.27/4.67 [1882=demod(1004),[1868], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12)))))),inverse(multiply(inverse(X13),X13)))) = X11]. % 4.27/4.67 [1917=param(785,784),[], % 4.27/4.67 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))) = multiply(inverse(X12),X12)]. % 4.27/4.67 [1961=param(1868,15),[], % 4.27/4.67 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X13))))) = inverse(multiply(inverse(X13),X12))]. % 4.27/4.67 [2026=param(1868,612),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [2079=param(2026,11),[], % 4.27/4.67 inverse(multiply(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),inverse(multiply(inverse(X11),inverse(multiply(multiply(X10,X12),inverse(multiply(inverse(multiply(X10,X12)),multiply(X10,X12)))))))),inverse(multiply(X13,multiply(inverse(X14),X14))))) = X13]. % 4.27/4.67 [2281=param(1917,612),[], % 4.27/4.67 inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 4.27/4.67 [2320=param(4,1917),[5], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,inverse(inverse(multiply(multiply(inverse(X11),X11),inverse(multiply(inverse(X12),X12))))))),multiply(X10,X13))) = inverse(multiply(X13,inverse(multiply(inverse(X13),X13))))]. % 4.27/4.67 [2327=param(8,1917),[5], % 4.27/4.67 multiply(inverse(multiply(X10,inverse(inverse(multiply(multiply(inverse(X11),X11),inverse(multiply(inverse(X12),X12))))))),multiply(X10,X13)) = multiply(X13,inverse(multiply(inverse(X13),X13)))]. % 4.27/4.67 [2364=param(250,1917),[], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))))),inverse(multiply(X12,inverse(multiply(inverse(X13),X13)))))) = X12]. % 4.27/4.67 [2458=param(2281,612),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 4.27/4.67 [2515=param(4,2281),[5], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,inverse(inverse(multiply(multiply(inverse(X11),X11),multiply(inverse(X12),X12)))))),multiply(X10,X13))) = inverse(multiply(X13,inverse(multiply(inverse(X13),X13))))]. % 4.27/4.67 [2684=param(2458,1336),[], % 4.27/4.67 inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))) = multiply(inverse(X11),X11)]. % 4.27/4.67 [2885=param(2458,2684),[], % 4.27/4.67 inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10)))))))) = multiply(inverse(X11),X11)]. % 4.27/4.67 [2961=param(27,2885),[], % 4.27/4.67 multiply(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(X10),X10))))))))),multiply(inverse(inverse(X11)),X12)))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [3903=param(11,775),[1961,284], % 4.27/4.67 inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),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))))))))]. % 4.27/4.67 [4150=param(45,110),[1961], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(inverse(X10),inverse(multiply(inverse(inverse(X11)),inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))))))),inverse(multiply(inverse(X12),inverse(multiply(inverse(X10),X10)))))),X11)) = X12]. % 4.27/4.67 [4151=param(45,110),[], % 4.27/4.67 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(X14,multiply(X15,X16))),multiply(X14,multiply(X15,X16)))))))))),X11)) = X13]. % 4.27/4.67 [4159=param(11,695),[1961,284], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(inverse(X10),X10)),X11)),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))))))))]. % 4.27/4.67 [4609=param(47,47),[], % 4.27/4.67 multiply(X10,multiply(inverse(multiply(X11,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))),multiply(X11,X13))) = multiply(inverse(multiply(X14,inverse(multiply(X15,inverse(multiply(inverse(X15),X15)))))),multiply(X14,multiply(inverse(inverse(multiply(inverse(multiply(X16,inverse(inverse(multiply(inverse(multiply(X17,X10)),multiply(X17,X15)))))),multiply(X16,X12)))),X13)))]. % 4.27/4.67 [4630=param(47,733),[], % 4.27/4.67 multiply(X10,multiply(inverse(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12)))),multiply(inverse(X13),X13))) = multiply(inverse(multiply(X14,inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))),multiply(X14,inverse(multiply(inverse(X15),X15))))]. % 4.27/4.67 [4688=param(12,731),[237], % 4.27/4.67 inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))) = inverse(multiply(X10,multiply(inverse(X11),X11)))]. % 4.27/4.67 [4952=param(4688,22),[], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(X13)),inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))))),X12)),X13)) = inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),X12)),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),X12))),inverse(multiply(inverse(multiply(X10,X11)),X12))))))]. % 4.27/4.67 [4954=demod(4151),[4952], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),inverse(multiply(inverse(X12),inverse(multiply(multiply(X10,X11),inverse(multiply(inverse(multiply(X13,multiply(X14,X15))),multiply(X13,multiply(X14,X15)))))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X10,X11)),inverse(multiply(inverse(X12),inverse(multiply(multiply(X10,X11),inverse(multiply(inverse(multiply(X13,multiply(X14,X15))),multiply(X13,multiply(X14,X15))))))))))),inverse(multiply(inverse(multiply(X10,X11)),inverse(multiply(inverse(X12),inverse(multiply(multiply(X10,X11),inverse(multiply(inverse(multiply(X13,multiply(X14,X15))),multiply(X13,multiply(X14,X15)))))))))))))) = X12]. % 4.27/4.67 [4962=demod(4150),[4952,323,323,323], % 4.27/4.67 inverse(multiply(inverse(X10),inverse(multiply(inverse(inverse(X10)),inverse(X10))))) = X10]. % 4.27/4.67 [4963=demod(4954),[4962], % 4.27/4.67 multiply(inverse(multiply(X10,X11)),inverse(multiply(inverse(X12),inverse(multiply(multiply(X10,X11),inverse(multiply(inverse(multiply(X13,multiply(X14,X15))),multiply(X13,multiply(X14,X15))))))))) = X12]. % 4.27/4.67 [4964=demod(118),[4963], % 4.27/4.67 inverse(multiply(inverse(X10),multiply(inverse(X11),X11))) = X10]. % 4.27/4.67 [4968=demod(155),[4964], % 4.27/4.67 inverse(multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))))))) = X11]. % 4.27/4.67 [4974=demod(1213),[4968], % 4.27/4.67 multiply(inverse(inverse(X10)),inverse(inverse(multiply(inverse(X11),X11)))) = X10]. % 4.27/4.67 [4975=demod(595),[4974], % 4.27/4.67 multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,inverse(multiply(inverse(X12),X12)))) = X11]. % 4.27/4.67 [4980=demod(4630),[4975], % 4.27/4.67 multiply(X10,multiply(inverse(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,X12)))),multiply(inverse(X13),X13))) = multiply(X12,inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [5002=demod(1880),[4975], % 4.27/4.67 multiply(inverse(inverse(X10)),inverse(multiply(inverse(X11),X11))) = X10]. % 4.27/4.67 [5003=demod(1876),[5002], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(inverse(multiply(inverse(X12),X12)))))) = X11]. % 4.27/4.67 [5004=demod(1234),[5003], % 4.27/4.67 inverse(inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,multiply(inverse(X12),X12))))) = inverse(X10)]. % 4.27/4.67 [5005=demod(1288),[5004], % 4.27/4.67 multiply(inverse(inverse(X10)),inverse(inverse(inverse(multiply(inverse(X11),X11))))) = X10]. % 4.27/4.67 [5007=demod(601),[5005], % 4.27/4.67 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [5008=demod(1011),[5007], % 4.27/4.67 inverse(multiply(inverse(multiply(X11,X10)),multiply(X11,multiply(inverse(X12),X12)))) = X10]. % 4.27/4.67 [5021=demod(1059),[5008], % 4.27/4.67 multiply(inverse(multiply(X11,X12)),inverse(multiply(inverse(X10),inverse(multiply(multiply(X11,X12),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X12)))))))) = X10]. % 4.27/4.67 [5022=demod(4159),[5021], % 4.27/4.67 inverse(multiply(inverse(multiply(inverse(multiply(inverse(X10),X10)),X11)),inverse(multiply(inverse(X12),X12)))) = X11]. % 4.27/4.67 [5023=demod(3903),[5021], % 4.27/4.67 inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),inverse(inverse(multiply(inverse(X12),X12))))) = X11]. % 4.27/4.67 [5027=demod(1281),[5008], % 4.27/4.67 inverse(multiply(inverse(X10),inverse(inverse(inverse(multiply(inverse(X11),X11)))))) = X10]. % 4.27/4.67 [5066=demod(818),[5027], % 4.27/4.67 multiply(inverse(X10),X11) = inverse(multiply(inverse(multiply(X12,X11)),multiply(X12,X10)))]. % 4.27/4.67 [5335=demod(2079),[-5066], % 4.27/4.67 inverse(multiply(multiply(inverse(multiply(X10,inverse(multiply(inverse(inverse(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))),inverse(multiply(X12,inverse(multiply(inverse(X12),X12)))))))),inverse(multiply(inverse(X11),inverse(multiply(multiply(X10,X12),multiply(inverse(X12),X12)))))),inverse(multiply(X13,multiply(inverse(X14),X14))))) = X13]. % 4.27/4.67 [5361=demod(1184),[-5066], % 4.27/4.67 inverse(multiply(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))),X12))),inverse(multiply(multiply(X13,X14),multiply(inverse(X14),X14))))) = multiply(X13,inverse(multiply(inverse(inverse(X12)),inverse(multiply(X14,inverse(multiply(inverse(X14),X14)))))))]. % 4.27/4.67 [5363=demod(11),[-5066], % 4.27/4.67 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),multiply(inverse(X14),X14))))))]. % 4.27/4.67 [5636=demod(1882),[5007], % 4.27/4.67 inverse(multiply(inverse(X10),inverse(multiply(inverse(X11),X11)))) = X10]. % 4.27/4.67 [5637=demod(5022),[5636], % 4.27/4.67 multiply(inverse(multiply(inverse(X10),X10)),X11) = X11]. % 4.27/4.67 [5650=demod(215),[5637], % 4.27/4.67 multiply(inverse(multiply(X12,X10)),multiply(X12,X11)) = multiply(inverse(X10),X11)]. % 4.27/4.67 [6185=demod(2327),[5650], % 4.27/4.67 multiply(inverse(inverse(inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))))),X12) = multiply(X12,inverse(multiply(inverse(X12),X12)))]. % 4.27/4.67 [6186=demod(2320),[5650], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))))),X12)) = inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))]. % 4.27/4.67 [6188=demod(2515),[5650], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))))),X12)) = inverse(multiply(X12,inverse(multiply(inverse(X12),X12))))]. % 4.27/4.67 [6196=demod(5363),[5650], % 4.27/4.67 inverse(multiply(inverse(X10),X11)) = multiply(inverse(multiply(X12,inverse(multiply(inverse(inverse(inverse(multiply(X11,inverse(multiply(inverse(X11),X11)))))),inverse(multiply(X13,inverse(multiply(inverse(X13),X13)))))))),inverse(multiply(inverse(X10),inverse(multiply(multiply(X12,X13),multiply(inverse(X13),X13))))))]. % 4.27/4.67 [6197=demod(5335),[-6196,5637], % 4.27/4.67 inverse(inverse(multiply(X10,multiply(inverse(X11),X11)))) = X10]. % 4.27/4.67 [6198=demod(6188),[6197,5637], % 4.27/4.67 inverse(multiply(X10,inverse(multiply(inverse(X10),X10)))) = inverse(X10)]. % 4.27/4.67 [6199=demod(6186),[6198], % 4.27/4.67 inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11)))))),X12)) = inverse(X12)]. % 4.27/4.67 [6200=demod(2364),[6199], % 4.27/4.67 inverse(inverse(multiply(X10,inverse(multiply(inverse(X11),X11))))) = X10]. % 4.27/4.67 [6201=demod(6185),[6200,5637], % 4.27/4.67 multiply(X10,inverse(multiply(inverse(X10),X10))) = X10]. % 4.27/4.67 [6202=demod(258),[6201], % 4.27/4.67 multiply(X10,inverse(multiply(inverse(X11),X11))) = X10]. % 4.27/4.67 [6203=demod(5002),[6202], % 4.27/4.67 inverse(inverse(X10)) = X10]. % 4.27/4.67 [6210=demod(5023),[6203,4964], % 4.27/4.67 multiply(multiply(inverse(X10),X10),X11) = X11]. % 4.27/4.67 [6212=demod(1868),[6210,6203], % 4.27/4.67 multiply(X10,multiply(inverse(X11),X11)) = X10]. % 4.27/4.67 [6241=demod(2961),[6203,6203,6203,6203,6203,6210,6203,6202], % 4.27/4.67 multiply(multiply(X10,X11),inverse(X11)) = X10]. % 4.27/4.67 [6247=demod(5361),[6212,5637,6203,6212,6203,6202], % 4.27/4.67 inverse(multiply(X10,inverse(multiply(X11,X12)))) = multiply(X11,inverse(multiply(X10,inverse(X12))))]. % 4.27/4.67 [6266=demod(457),[5650,5650,6203,5650,6247,6241,6203,5650,5650,6202], % 4.27/4.67 multiply(inverse(X10),X11) = inverse(multiply(inverse(X11),X10))]. % 4.27/4.67 [6271=demod(4980),[5650,6203,6212,-6266,6212], % 4.27/4.67 multiply(X10,multiply(inverse(X10),X11)) = X11]. % 4.27/4.67 [6313=demod(83),[5650,6203,6203,-6266,6212,5650,6203,6203], % 4.27/4.67 multiply(X10,multiply(multiply(inverse(X10),X11),X12)) = multiply(X11,X12)]. % 4.27/4.67 [6348=demod(4609),[-6266,6212,5650,6203,-6266,6212,5650,6203,5650,6203,5650,6203], % 4.27/4.67 multiply(X13,multiply(multiply(inverse(multiply(inverse(X10),X13)),X11),X12)) = multiply(X10,multiply(X11,X12))]. % 4.27/4.67 [6358=param(5650,6271),[], % 4.27/4.67 multiply(inverse(multiply(inverse(X11),X10)),X12) = multiply(inverse(X10),multiply(X11,X12))]. % 4.27/4.67 [6371=demod(6348),[6358,6313], % 4.27/4.67 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 4.27/4.67 [6388=param(3,6371),[2], % 4.27/4.67 thmtrue = thmfalse]. % 4.27/4.67 % SZS output end CNFRefutation % 4.27/4.67 Space: 9777 KB %------------------------------------------------------------------------------