%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP405-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:54 EDT 2022 % Result : Unsatisfiable 4.58s 4.97s % Output : CNFRefutation 4.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP405-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 : Tue Jun 14 06:55:04 EDT 2022 % 0.13/0.34 % CPUTime : % 4.58/4.97 Theorem Proved. % 4.58/4.97 % SZS status Unsatisfiable % 4.58/4.97 % SZS output start CNFRefutation % 4.58/4.97 [1=axiom,[], % 4.58/4.97 multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),X12)),inverse(multiply(X11,multiply(inverse(X11),X11)))))) = X12]. % 4.58/4.97 [2=axiom,[], % 4.58/4.97 thtop(X10,X10) = thmfalse]. % 4.58/4.97 [3=axiom,[], % 4.58/4.97 thtop(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) = thmtrue]. % 4.58/4.97 [4=param(1,1),[], % 4.58/4.97 inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X10,X12)),X13)),X11)),inverse(multiply(X13,multiply(inverse(X13),X13))))) = multiply(X10,inverse(multiply(inverse(X11),inverse(multiply(X12,multiply(inverse(X12),X12))))))]. % 4.58/4.97 [5=param(1,4),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),inverse(multiply(X11,multiply(inverse(X11),X11))))))) = X12]. % 4.58/4.97 [6=param(5,4),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(X12,inverse(multiply(inverse(X13),inverse(multiply(X14,multiply(inverse(X14),X14)))))))) = multiply(inverse(multiply(inverse(multiply(X12,X14)),X11)),X13)]. % 4.58/4.97 [7=param(6,1),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(multiply(inverse(multiply(X13,X14)),X11)),multiply(inverse(multiply(X13,X14)),X12))]. % 4.58/4.97 [10=param(7,6),[1], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(multiply(X13,X11)),multiply(X13,X12))]. % 4.58/4.97 [12=param(1,10),[], % 4.58/4.97 multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X13))),inverse(multiply(X12,multiply(inverse(X12),X12)))))) = multiply(X10,X13)]. % 4.58/4.97 [13=param(1,10),[], % 4.58/4.97 multiply(X10,inverse(multiply(inverse(multiply(inverse(multiply(X10,multiply(X11,X12))),X13)),inverse(multiply(multiply(X11,X12),multiply(inverse(multiply(X14,X12)),multiply(X14,X12))))))) = X13]. % 4.58/4.97 [17=param(10,7),[], % 4.58/4.97 multiply(inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),X12)),X13)),multiply(inverse(multiply(X14,X12)),multiply(X14,X15))) = multiply(inverse(multiply(X16,X13)),multiply(X16,multiply(inverse(multiply(X10,X11)),X15)))]. % 4.58/4.97 [18=param(10,10),[], % 4.58/4.97 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)))]. % 4.58/4.97 [19=param(1,12),[1], % 4.58/4.97 inverse(multiply(inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X10))),inverse(multiply(X12,multiply(inverse(X12),X12))))) = X10]. % 4.58/4.97 [21=param(1,19),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),inverse(multiply(X12,inverse(multiply(multiply(X10,X12),multiply(inverse(multiply(X10,X12)),multiply(X10,X12))))))) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.97 [23=param(19,10),[], % 4.58/4.97 inverse(multiply(inverse(multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,X13))),inverse(multiply(multiply(X11,X12),multiply(inverse(multiply(X14,X12)),multiply(X14,X12)))))) = X13]. % 4.58/4.97 [25=param(5,21),[], % 4.58/4.97 multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(X12)))),inverse(multiply(X11,multiply(inverse(X11),X11)))) = X12]. % 4.58/4.97 [27=param(21,10),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),inverse(multiply(X12,inverse(multiply(multiply(X10,X12),multiply(inverse(multiply(X13,X12)),multiply(X13,X12))))))) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.97 [28=param(25,6),[], % 4.58/4.97 multiply(inverse(multiply(X11,multiply(X12,inverse(X10)))),multiply(X11,multiply(X12,inverse(multiply(inverse(inverse(multiply(X13,multiply(inverse(X13),X13)))),inverse(multiply(X13,multiply(inverse(X13),X13)))))))) = X10]. % 4.58/4.97 [31=param(1,23),[27], % 4.58/4.97 inverse(multiply(multiply(X10,X11),multiply(inverse(multiply(X10,X11)),multiply(X10,X11)))) = inverse(multiply(multiply(X10,X11),multiply(inverse(multiply(X12,X11)),multiply(X12,X11))))]. % 4.58/4.97 [35=param(31,10),[], % 4.58/4.97 inverse(multiply(multiply(X10,X11),multiply(inverse(multiply(X12,X11)),multiply(X12,X11)))) = inverse(multiply(multiply(X10,X11),multiply(inverse(multiply(X13,X11)),multiply(X13,X11))))]. % 4.58/4.97 [36=param(5,35),[5], % 4.58/4.97 multiply(multiply(X10,X11),multiply(inverse(multiply(X12,X11)),multiply(X12,X11))) = multiply(multiply(X10,X11),multiply(inverse(multiply(X13,X11)),multiply(X13,X11)))]. % 4.58/4.97 [41=param(5,19),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X12,inverse(multiply(X11,multiply(inverse(X11),X11))))))) = multiply(inverse(multiply(inverse(multiply(X13,X14)),multiply(X13,X12))),inverse(multiply(X14,multiply(inverse(X14),X14))))]. % 4.58/4.97 [42=param(10,36),[], % 4.58/4.97 multiply(inverse(multiply(multiply(X10,X11),X12)),multiply(multiply(X10,X11),multiply(inverse(multiply(X13,X11)),multiply(X13,X11)))) = multiply(inverse(multiply(X14,X12)),multiply(X14,multiply(inverse(multiply(X15,X11)),multiply(X15,X11))))]. % 4.58/4.97 [45=param(13,10),[], % 4.58/4.97 multiply(inverse(multiply(X10,X11)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X12,X11)),multiply(X12,X13))),X14)),inverse(multiply(multiply(X10,X13),multiply(inverse(multiply(X15,X13)),multiply(X15,X13))))))) = X14]. % 4.58/4.97 [48=param(5,45),[], % 4.58/4.97 multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),X13) = multiply(inverse(multiply(inverse(multiply(X14,X11)),multiply(X14,X12))),X13)]. % 4.58/4.97 [53=param(48,7),[], % 4.58/4.97 multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),multiply(inverse(multiply(X13,X11)),X14)) = multiply(inverse(multiply(X15,multiply(X13,X12))),multiply(X15,X14))]. % 4.58/4.97 [63=param(19,41),[], % 4.58/4.97 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(X12,inverse(multiply(X11,multiply(inverse(X11),X11)))))))) = X12]. % 4.58/4.97 [70=param(63,19),[], % 4.58/4.97 inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))]. % 4.58/4.97 [85=param(70,41),[19], % 4.58/4.97 inverse(multiply(inverse(multiply(X14,multiply(X11,inverse(multiply(X10,inverse(multiply(X12,multiply(inverse(X12),X12)))))))),multiply(X14,X13))) = inverse(multiply(X10,multiply(inverse(multiply(X11,X12)),X13)))]. % 4.58/4.97 [89=param(1,42),[19], % 4.58/4.97 multiply(X10,multiply(inverse(multiply(X11,X12)),multiply(X11,X12))) = multiply(X10,multiply(inverse(multiply(X13,X12)),multiply(X13,X12)))]. % 4.58/4.97 [99=param(5,85),[5], % 4.58/4.97 multiply(inverse(multiply(X14,multiply(X11,inverse(multiply(X10,inverse(multiply(X12,multiply(inverse(X12),X12)))))))),multiply(X14,X13)) = multiply(X10,multiply(inverse(multiply(X11,X12)),X13))]. % 4.58/4.98 [101=param(99,27),[], % 4.58/4.98 multiply(inverse(multiply(X10,inverse(multiply(X11,multiply(inverse(X11),X11))))),multiply(X10,X12)) = multiply(X13,multiply(inverse(multiply(inverse(multiply(X14,X11)),multiply(X14,X13))),X12))]. % 4.58/4.98 [110=param(53,18),[], % 4.58/4.98 multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X13))) = multiply(inverse(multiply(X14,multiply(X15,X12))),multiply(X14,multiply(X15,X13)))]. % 4.58/4.98 [114=param(70,110),[], % 4.58/4.98 inverse(multiply(inverse(multiply(X10,multiply(X11,X12))),multiply(X10,multiply(X11,X13)))) = inverse(multiply(inverse(multiply(X14,multiply(X15,X12))),multiply(X14,multiply(X15,X13))))]. % 4.58/4.98 [117=param(110,99),[99], % 4.58/4.98 multiply(X10,multiply(inverse(multiply(X11,X12)),multiply(X11,X13))) = multiply(X10,multiply(inverse(multiply(X14,X12)),multiply(X14,X13)))]. % 4.58/4.98 [138=param(114,99),[99], % 4.58/4.98 inverse(multiply(X10,multiply(inverse(multiply(X11,X12)),multiply(X11,X13)))) = inverse(multiply(X10,multiply(inverse(multiply(X14,X12)),multiply(X14,X13))))]. % 4.58/4.98 [149=param(101,25),[], % 4.58/4.98 multiply(inverse(X10),X10) = multiply(inverse(multiply(X11,inverse(multiply(X12,multiply(inverse(X12),X12))))),multiply(X11,inverse(multiply(X12,multiply(inverse(X12),X12)))))]. % 4.58/4.98 [160=param(149,25),[25], % 4.58/4.98 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 4.58/4.98 [169=param(5,160),[], % 4.58/4.98 multiply(inverse(multiply(X10,X11)),multiply(X10,inverse(multiply(inverse(X12),X12)))) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.98 [172=param(6,160),[], % 4.58/4.98 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X13),inverse(multiply(X14,multiply(inverse(X14),X14)))))),X14)),X11)),X13)]. % 4.58/4.98 [189=param(19,160),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,multiply(inverse(X11),X11))))) = X11]. % 4.58/4.98 [192=param(19,160),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(multiply(X10,X11)),multiply(X10,X12))),inverse(multiply(X11,multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [204=param(28,160),[], % 4.58/4.98 multiply(inverse(multiply(X10,multiply(X11,inverse(X12)))),multiply(X10,multiply(X11,inverse(multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [237=param(63,160),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(inverse(multiply(X10,inverse(multiply(X11,multiply(inverse(X11),X11)))))),X11)),multiply(inverse(X12),X12))) = X10]. % 4.58/4.98 [239=param(70,160),[], % 4.58/4.98 inverse(multiply(inverse(X10),X10)) = inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X12)))]. % 4.58/4.98 [244=param(89,160),[], % 4.58/4.98 multiply(X10,multiply(inverse(X11),X11)) = multiply(X10,multiply(inverse(multiply(X12,X13)),multiply(X12,X13)))]. % 4.58/4.98 [247=param(99,160),[], % 4.58/4.98 multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,X12)) = multiply(X13,multiply(inverse(multiply(inverse(inverse(multiply(X13,inverse(multiply(X14,multiply(inverse(X14),X14)))))),X14)),X12))]. % 4.58/4.98 [258=param(117,160),[], % 4.58/4.98 multiply(X10,multiply(inverse(multiply(inverse(X11),X11)),multiply(inverse(X12),X13))) = multiply(X10,multiply(inverse(multiply(X14,X12)),multiply(X14,X13)))]. % 4.58/4.98 [261=param(138,160),[], % 4.58/4.98 inverse(multiply(X10,multiply(inverse(multiply(inverse(X11),X11)),multiply(inverse(X12),X13)))) = inverse(multiply(X10,multiply(inverse(multiply(X14,X12)),multiply(X14,X13))))]. % 4.58/4.98 [287=param(189,160),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 4.58/4.98 [291=param(287,10),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(inverse(multiply(X11,X12)),multiply(X11,X13))))) = inverse(multiply(inverse(X13),X12))]. % 4.58/4.98 [314=param(287,160),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(inverse(X11),X11)))) = inverse(multiply(inverse(X12),X12))]. % 4.58/4.98 [317=param(287,239),[291], % 4.58/4.98 inverse(multiply(inverse(X10),X10)) = inverse(multiply(inverse(X11),X11))]. % 4.58/4.98 [339=param(160,317),[], % 4.58/4.98 multiply(inverse(multiply(inverse(X10),X10)),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 4.58/4.98 [352=param(18,339),[], % 4.58/4.98 multiply(inverse(multiply(inverse(multiply(inverse(X10),X10)),X11)),multiply(inverse(X12),X12)) = multiply(inverse(multiply(inverse(multiply(inverse(X13),X14)),X11)),multiply(inverse(multiply(X15,X14)),multiply(X15,X13)))]. % 4.58/4.98 [457=param(17,244),[], % 4.58/4.98 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X13,X14)),X15)),X11)),multiply(inverse(multiply(X16,X15)),multiply(X16,multiply(X13,X14))))]. % 4.58/4.98 [534=param(204,160),[169], % 4.58/4.98 multiply(inverse(multiply(inverse(X10),X10)),inverse(multiply(inverse(X11),multiply(inverse(inverse(X11)),inverse(X11))))) = X11]. % 4.58/4.98 [545=param(204,314),[204], % 4.58/4.98 multiply(inverse(X10),X10) = multiply(inverse(multiply(inverse(X11),X11)),inverse(multiply(inverse(X12),X12)))]. % 4.58/4.98 [589=param(7,545),[169], % 4.58/4.98 multiply(inverse(multiply(inverse(multiply(inverse(X10),X10)),X11)),multiply(inverse(X12),X12)) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.98 [601=demod(352),[589], % 4.58/4.98 multiply(inverse(multiply(inverse(multiply(inverse(X11),X12)),X10)),multiply(inverse(multiply(X13,X12)),multiply(X13,X11))) = inverse(multiply(X10,multiply(inverse(X10),X10)))]. % 4.58/4.98 [602=demod(457),[601], % 4.58/4.98 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(inverse(X12),X12))) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.98 [604=demod(172),[602], % 4.58/4.98 multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X11),inverse(multiply(X12,multiply(inverse(X12),X12)))))),X12)),X10)),X11) = inverse(multiply(X10,multiply(inverse(X10),X10)))]. % 4.58/4.98 [638=param(114,602),[192], % 4.58/4.98 inverse(multiply(inverse(multiply(X11,multiply(X12,X10))),multiply(X11,multiply(X12,multiply(inverse(X13),X13))))) = X10]. % 4.58/4.98 [669=param(101,638),[], % 4.58/4.98 multiply(multiply(X10,multiply(inverse(X11),X11)),multiply(X12,X13)) = multiply(inverse(multiply(X14,inverse(multiply(multiply(X10,X12),multiply(inverse(multiply(X10,X12)),multiply(X10,X12)))))),multiply(X14,X13))]. % 4.58/4.98 [678=param(638,239),[], % 4.58/4.98 multiply(inverse(X10),X10) = inverse(multiply(inverse(X11),X11))]. % 4.58/4.98 [679=param(287,638),[], % 4.58/4.98 inverse(multiply(multiply(inverse(X10),X10),inverse(multiply(X11,multiply(inverse(X12),X12))))) = X11]. % 4.58/4.98 [738=param(204,678),[], % 4.58/4.98 multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,multiply(inverse(inverse(X12)),inverse(multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [747=param(317,678),[], % 4.58/4.98 inverse(inverse(multiply(inverse(X10),X10))) = inverse(multiply(inverse(X11),X11))]. % 4.58/4.98 [748=param(678,339),[], % 4.58/4.98 inverse(multiply(inverse(X10),X10)) = multiply(inverse(multiply(inverse(X11),X11)),multiply(inverse(X12),X12))]. % 4.58/4.98 [755=param(678,678),[], % 4.58/4.98 inverse(inverse(multiply(inverse(X10),X10))) = multiply(inverse(X11),X11)]. % 4.58/4.98 [764=param(70,678),[], % 4.58/4.98 inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X12))) = inverse(multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))]. % 4.58/4.98 [770=param(117,678),[], % 4.58/4.98 multiply(X10,multiply(multiply(inverse(X11),X11),multiply(inverse(X12),X13))) = multiply(X10,multiply(inverse(multiply(X14,X12)),multiply(X14,X13)))]. % 4.58/4.98 [773=param(160,678),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 4.58/4.98 [777=param(204,678),[169], % 4.58/4.98 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),multiply(inverse(inverse(X11)),inverse(X11))))) = X11]. % 4.58/4.98 [812=param(602,755),[], % 4.58/4.98 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(multiply(inverse(X12),X12),inverse(multiply(inverse(X13),X13))))) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.98 [997=param(160,747),[], % 4.58/4.98 multiply(inverse(inverse(multiply(inverse(X10),X10))),multiply(inverse(X11),X11)) = multiply(inverse(X12),X12)]. % 4.58/4.98 [1288=param(6,773),[604], % 4.58/4.98 multiply(inverse(multiply(multiply(inverse(X10),X10),X11)),multiply(inverse(X12),X12)) = inverse(multiply(X11,multiply(inverse(X11),X11)))]. % 4.58/4.98 [1351=param(773,678),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11)) = inverse(multiply(inverse(X12),X12))]. % 4.58/4.98 [1352=param(678,773),[], % 4.58/4.98 inverse(multiply(multiply(inverse(X10),X10),multiply(inverse(X11),X11))) = multiply(inverse(X12),X12)]. % 4.58/4.98 [1439=param(679,755),[], % 4.58/4.98 inverse(multiply(multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X11))),inverse(multiply(X12,multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [1487=param(204,1352),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),multiply(multiply(inverse(X11),X11),multiply(inverse(inverse(X12)),inverse(multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [1579=param(204,1351),[], % 4.58/4.98 multiply(inverse(inverse(multiply(inverse(X10),X10))),multiply(multiply(inverse(X11),X11),multiply(inverse(inverse(X12)),inverse(multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [2630=param(101,997),[], % 4.58/4.98 multiply(X10,multiply(inverse(multiply(inverse(inverse(multiply(inverse(X11),X11))),multiply(inverse(X12),X12))),X13)) = multiply(inverse(multiply(X14,inverse(multiply(X10,multiply(inverse(X10),X10))))),multiply(X14,X13))]. % 4.58/4.98 [2852=param(204,748),[], % 4.58/4.98 multiply(inverse(inverse(multiply(inverse(X10),X10))),multiply(inverse(multiply(inverse(X11),X11)),multiply(inverse(inverse(X12)),inverse(multiply(inverse(X13),X13))))) = X12]. % 4.58/4.98 [3716=param(287,1288),[], % 4.58/4.98 inverse(multiply(inverse(multiply(inverse(X10),X10)),inverse(inverse(multiply(X11,multiply(inverse(X11),X11)))))) = inverse(multiply(multiply(inverse(X12),X12),X11))]. % 4.58/4.98 [3749=param(777,160),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),multiply(inverse(X12),X12)))) = X11]. % 4.58/4.98 [3751=param(3749,7),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(multiply(inverse(multiply(X11,X12)),X13)),multiply(inverse(multiply(X11,X12)),X14)))) = multiply(inverse(X14),X13)]. % 4.58/4.98 [3763=param(3749,41),[192], % 4.58/4.98 multiply(multiply(inverse(X10),X10),X11) = multiply(inverse(inverse(multiply(X11,inverse(multiply(X12,multiply(inverse(X12),X12)))))),X12)]. % 4.58/4.98 [3788=param(3749,204),[], % 4.58/4.98 multiply(multiply(inverse(X10),X10),inverse(X11)) = multiply(inverse(multiply(X12,inverse(multiply(inverse(X13),X13)))),multiply(X12,inverse(X11)))]. % 4.58/4.98 [3789=param(204,3749),[812], % 4.62/4.98 inverse(multiply(X10,multiply(inverse(X10),X10))) = multiply(inverse(X10),multiply(inverse(X11),X11))]. % 4.62/4.98 [3813=demod(534),[-3789], % 4.62/4.98 multiply(inverse(multiply(inverse(X10),X10)),inverse(inverse(multiply(X11,multiply(inverse(X11),X11))))) = X11]. % 4.62/4.98 [3814=demod(3716),[3813], % 4.62/4.98 inverse(multiply(multiply(inverse(X11),X11),X10)) = inverse(X10)]. % 4.62/4.98 [3819=demod(764),[3814], % 4.62/4.98 inverse(multiply(inverse(multiply(X12,X10)),multiply(X12,X11))) = inverse(multiply(inverse(X10),X11))]. % 4.62/4.98 [3820=demod(3751),[3819], % 4.62/4.98 multiply(multiply(inverse(X10),X10),inverse(multiply(inverse(X11),X12))) = multiply(inverse(X12),X11)]. % 4.62/4.98 [3824=demod(1439),[3820,3814], % 4.62/4.98 inverse(inverse(multiply(X10,multiply(inverse(X11),X11)))) = X10]. % 4.62/4.98 [3842=demod(3813),[3824], % 4.62/4.98 multiply(inverse(multiply(inverse(X10),X10)),X11) = X11]. % 4.62/4.98 [3925=demod(261),[3842], % 4.62/4.98 inverse(multiply(X10,multiply(inverse(multiply(X13,X11)),multiply(X13,X12)))) = inverse(multiply(X10,multiply(inverse(X11),X12)))]. % 4.62/4.98 [3949=demod(669),[3925], % 4.62/4.98 multiply(multiply(X10,multiply(inverse(X11),X11)),multiply(X12,X13)) = multiply(inverse(multiply(X14,inverse(multiply(multiply(X10,X12),multiply(inverse(X12),X12))))),multiply(X14,X13))]. % 4.62/4.98 [4023=demod(258),[3842], % 4.62/4.98 multiply(X10,multiply(inverse(multiply(X13,X11)),multiply(X13,X12))) = multiply(X10,multiply(inverse(X11),X12))]. % 4.62/4.98 [4033=demod(770),[4023], % 4.62/4.98 multiply(X10,multiply(multiply(inverse(X11),X11),multiply(inverse(X12),X13))) = multiply(X10,multiply(inverse(X12),X13))]. % 4.62/4.98 [4034=demod(1487),[4033], % 4.62/4.98 multiply(multiply(inverse(X10),X10),multiply(inverse(inverse(X11)),inverse(multiply(inverse(X12),X12)))) = X11]. % 4.62/4.98 [4035=demod(1579),[4034], % 4.62/4.98 multiply(inverse(inverse(multiply(inverse(X10),X10))),X11) = X11]. % 4.62/4.98 [4036=demod(2630),[4035,3842], % 4.62/4.98 multiply(inverse(multiply(X12,inverse(multiply(X10,multiply(inverse(X10),X10))))),multiply(X12,X11)) = multiply(X10,X11)]. % 4.62/4.98 [4116=demod(2852),[3842,4035], % 4.62/4.98 multiply(inverse(inverse(X10)),inverse(multiply(inverse(X11),X11))) = X10]. % 4.62/4.98 [4123=demod(738),[4116], % 4.62/4.98 multiply(inverse(multiply(X10,inverse(multiply(inverse(X11),X11)))),multiply(X10,X12)) = X12]. % 4.62/4.98 [4124=demod(3788),[4123], % 4.62/4.98 multiply(multiply(inverse(X10),X10),inverse(X11)) = inverse(X11)]. % 4.62/4.98 [4127=demod(3749),[4124], % 4.62/4.98 inverse(multiply(inverse(X10),multiply(inverse(X11),X11))) = X10]. % 4.62/4.98 [4130=demod(237),[4127], % 4.62/4.98 multiply(inverse(inverse(multiply(X10,inverse(multiply(X11,multiply(inverse(X11),X11)))))),X11) = X10]. % 4.62/4.98 [4133=demod(3763),[4130], % 4.62/4.98 multiply(multiply(inverse(X10),X10),X11) = X11]. % 4.62/4.98 [4134=demod(247),[4130], % 4.62/4.98 multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,X12)) = multiply(X13,multiply(inverse(X13),X12))]. % 4.62/4.98 [4139=demod(3820),[4133], % 4.62/4.98 inverse(multiply(inverse(X10),X11)) = multiply(inverse(X11),X10)]. % 4.62/4.98 [4140=demod(4123),[4139], % 4.62/4.98 multiply(inverse(multiply(X10,multiply(inverse(X11),X11))),multiply(X10,X12)) = X12]. % 4.62/4.98 [4142=demod(4134),[4140], % 4.62/4.98 multiply(X11,multiply(inverse(X11),X10)) = X10]. % 4.62/4.98 [4176=demod(4036),[4142], % 4.62/4.98 multiply(inverse(multiply(X10,inverse(X11))),multiply(X10,X12)) = multiply(X11,X12)]. % 4.62/4.98 [4178=demod(3949),[4176], % 4.62/4.98 multiply(multiply(X10,multiply(inverse(X11),X11)),multiply(X12,X13)) = multiply(multiply(multiply(X10,X12),multiply(inverse(X12),X12)),X13)]. % 4.62/4.98 [4181=demod(3789),[4142], % 4.62/4.98 multiply(inverse(X10),multiply(inverse(X11),X11)) = inverse(X10)]. % 4.62/4.98 [4182=demod(4127),[4181], % 4.62/4.98 inverse(inverse(X10)) = X10]. % 4.62/4.98 [4183=demod(3824),[4182], % 4.62/4.98 multiply(X10,multiply(inverse(X11),X11)) = X10]. % 4.62/4.98 [4197=demod(4178),[4183,4183], % 4.62/4.98 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 4.62/4.98 [4308=param(3,4197),[2], % 4.62/4.98 thmtrue = thmfalse]. % 4.62/4.98 % SZS output end CNFRefutation % 4.62/4.98 Space: 6635 KB %------------------------------------------------------------------------------