%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP477-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 09:14:11 EDT 2022 % Result : Unsatisfiable 1.35s 1.73s % Output : CNFRefutation 1.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP477-1 : TPTP v8.1.0. Released v2.6.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n018.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:35:43 EDT 2022 % 0.13/0.34 % CPUTime : % 1.35/1.73 Theorem Proved. % 1.35/1.73 % SZS status Unsatisfiable % 1.35/1.73 % SZS output start CNFRefutation % 1.35/1.73 [1=axiom,[], % 1.35/1.73 divide(X10,inverse(X11)) = multiply(X10,X11)]. % 1.35/1.73 [2=axiom,[], % 1.35/1.73 divide(inverse(divide(divide(divide(X10,X11),X12),divide(X13,X12))),divide(X11,X10)) = X13]. % 1.35/1.73 [3=axiom,[], % 1.35/1.73 thtop(X10,X10) = thmfalse]. % 1.35/1.73 [4=axiom,[], % 1.35/1.73 thtop(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) = thmtrue]. % 1.35/1.73 [5=param(2,1),[1], % 1.35/1.73 divide(inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))),divide(X11,X10)) = X13]. % 1.35/1.73 [6=param(2,1),[], % 1.35/1.73 divide(inverse(divide(divide(multiply(X10,X11),X12),divide(X13,X12))),divide(inverse(X11),X10)) = X13]. % 1.35/1.73 [7=param(2,1),[], % 1.35/1.73 divide(inverse(divide(divide(divide(inverse(X10),X11),X12),divide(X13,X12))),multiply(X11,X10)) = X13]. % 1.35/1.73 [9=param(6,1),[1], % 1.35/1.73 divide(inverse(divide(multiply(multiply(X10,X11),X12),multiply(X13,X12))),divide(inverse(X11),X10)) = X13]. % 1.35/1.73 [10=param(9,1),[], % 1.35/1.73 divide(inverse(divide(multiply(multiply(inverse(X10),X11),X12),multiply(X13,X12))),multiply(inverse(X11),X10)) = X13]. % 1.35/1.73 [11=param(6,1),[], % 1.35/1.73 divide(inverse(divide(divide(multiply(inverse(X10),X11),X12),divide(X13,X12))),multiply(inverse(X11),X10)) = X13]. % 1.35/1.73 [12=param(5,5),[1], % 1.35/1.73 divide(inverse(divide(multiply(multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(X13,X12))),X14),multiply(X15,X14))),X13) = X15]. % 1.35/1.73 [13=param(2,2),[1], % 1.35/1.73 divide(inverse(divide(divide(X10,X11),divide(X12,X11))),multiply(divide(X13,X14),divide(divide(divide(X14,X13),X15),divide(X10,X15)))) = X12]. % 1.35/1.73 [14=param(2,2),[], % 1.35/1.73 divide(inverse(divide(divide(divide(X10,X11),divide(X12,X13)),X14)),divide(X11,X10)) = inverse(divide(divide(divide(X13,X12),X15),divide(X14,X15)))]. % 1.35/1.73 [16=param(2,5),[1], % 1.35/1.73 divide(inverse(divide(divide(X10,X11),divide(X12,X11))),multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(X10,X15)))) = X12]. % 1.35/1.73 [17=param(2,5),[], % 1.35/1.73 divide(inverse(divide(divide(divide(X10,X11),divide(X12,X13)),X14)),divide(X11,X10)) = inverse(divide(multiply(divide(X13,X12),X15),multiply(X14,X15)))]. % 1.35/1.73 [18=param(2,5),[1], % 1.35/1.73 divide(inverse(divide(divide(multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(X13,X12))),X14),divide(X15,X14))),X13) = X15]. % 1.35/1.73 [39=param(14,2),[], % 1.35/1.73 inverse(divide(divide(divide(X10,X11),X12),divide(divide(X13,divide(X11,X10)),X12))) = X13]. % 1.35/1.73 [40=param(14,14),[39], % 1.35/1.73 divide(divide(inverse(divide(divide(divide(X10,X11),divide(X12,X13)),X14)),divide(X11,X10)),divide(X12,X13)) = X14]. % 1.35/1.73 [43=param(13,39),[], % 1.35/1.73 divide(X10,multiply(divide(X11,X12),divide(divide(divide(X12,X11),X13),divide(divide(X14,X15),X13)))) = divide(X10,divide(X15,X14))]. % 1.35/1.73 [44=param(16,39),[], % 1.35/1.73 divide(X10,multiply(divide(X11,X12),divide(multiply(divide(X12,X11),X13),multiply(divide(X14,X15),X13)))) = divide(X10,divide(X15,X14))]. % 1.35/1.73 [46=param(17,2),[], % 1.35/1.73 inverse(divide(multiply(divide(X10,X11),X12),multiply(divide(X13,divide(X11,X10)),X12))) = X13]. % 1.35/1.73 [47=param(17,14),[], % 1.35/1.73 inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))) = inverse(divide(divide(divide(X10,X11),X14),divide(X13,X14)))]. % 1.35/1.73 [48=param(1,46),[], % 1.35/1.73 divide(X10,X11) = multiply(X10,divide(multiply(divide(X12,X13),X14),multiply(divide(X11,divide(X13,X12)),X14)))]. % 1.35/1.73 [60=param(40,2),[2], % 1.35/1.73 divide(divide(inverse(divide(divide(divide(X10,X11),X12),X13)),divide(X11,X10)),X12) = X13]. % 1.35/1.73 [62=param(60,1),[], % 1.35/1.73 divide(divide(inverse(multiply(divide(divide(X10,X11),X12),X13)),divide(X11,X10)),X12) = inverse(X13)]. % 1.35/1.73 [63=param(60,1),[], % 1.35/1.73 divide(divide(inverse(divide(divide(multiply(X10,X11),X12),X13)),divide(inverse(X11),X10)),X12) = X13]. % 1.35/1.73 [64=param(60,1),[], % 1.35/1.73 divide(divide(inverse(divide(divide(divide(inverse(X10),X11),X12),X13)),multiply(X11,X10)),X12) = X13]. % 1.35/1.73 [72=param(60,5),[1], % 1.35/1.73 divide(divide(inverse(divide(divide(multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(X13,X12))),X14),X15)),X13),X14) = X15]. % 1.35/1.73 [82=param(60,60),[1], % 1.35/1.73 divide(divide(inverse(divide(X10,X11)),multiply(divide(X12,X13),divide(divide(divide(X13,X12),X14),X10))),X14) = X11]. % 1.35/1.73 [107=param(64,1),[], % 1.35/1.73 divide(divide(inverse(divide(divide(multiply(inverse(X10),X11),X12),X13)),multiply(inverse(X11),X10)),X12) = X13]. % 1.35/1.73 [171=param(60,43),[60], % 1.35/1.73 multiply(divide(X12,X13),divide(divide(divide(X13,X12),X14),divide(divide(X11,X10),X14))) = divide(X10,X11)]. % 1.35/1.73 [172=param(171,1),[], % 1.35/1.73 multiply(multiply(X10,X11),divide(divide(divide(inverse(X11),X10),X12),divide(divide(X13,X14),X12))) = divide(X14,X13)]. % 1.35/1.73 [173=param(171,1),[1], % 1.35/1.73 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(divide(X13,X14),X12))) = divide(X14,X13)]. % 1.35/1.73 [175=param(171,1),[], % 1.35/1.73 multiply(divide(X10,X11),divide(divide(divide(X11,X10),X12),divide(multiply(X13,X14),X12))) = divide(inverse(X14),X13)]. % 1.35/1.73 [211=param(12,172),[5], % 1.35/1.73 divide(inverse(divide(divide(X10,X11),multiply(X12,divide(divide(X13,X14),divide(divide(X11,X10),X14))))),X13) = X12]. % 1.35/1.73 [214=param(1,47),[1], % 1.35/1.73 multiply(X10,divide(divide(divide(X11,X12),X13),divide(X14,X13))) = multiply(X10,divide(multiply(divide(X11,X12),X15),multiply(X14,X15)))]. % 1.35/1.73 [233=param(173,1),[], % 1.35/1.73 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(divide(inverse(X13),X14),X12))) = multiply(X14,X13)]. % 1.35/1.73 [238=param(233,44),[233], % 1.35/1.73 multiply(divide(X10,X11),X12) = multiply(multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(divide(X11,X10),X15))),X12)]. % 1.35/1.73 [279=param(211,172),[], % 1.35/1.73 divide(inverse(divide(divide(X10,X11),divide(X10,X11))),divide(inverse(X12),X13)) = multiply(X13,X12)]. % 1.35/1.73 [284=param(279,2),[2], % 1.35/1.73 divide(inverse(divide(X10,X10)),divide(inverse(X11),X12)) = multiply(X12,X11)]. % 1.35/1.73 [318=param(82,284),[1], % 1.35/1.73 divide(divide(inverse(multiply(X10,X11)),multiply(divide(X12,X13),multiply(divide(divide(X13,X12),X14),divide(X15,X15)))),X14) = divide(inverse(X11),X10)]. % 1.35/1.73 [331=param(171,284),[175,1], % 1.35/1.73 multiply(divide(inverse(X10),X11),divide(X12,X12)) = divide(inverse(X10),X11)]. % 1.35/1.73 [340=param(331,2),[2], % 1.35/1.73 multiply(X10,divide(X11,X11)) = X10]. % 1.35/1.73 [341=demod(318),[340], % 1.35/1.73 divide(divide(inverse(multiply(X10,X11)),multiply(divide(X12,X13),divide(divide(X13,X12),X14))),X14) = divide(inverse(X11),X10)]. % 1.35/1.73 [347=param(340,1),[], % 1.35/1.73 multiply(X10,multiply(inverse(X11),X11)) = X10]. % 1.35/1.73 [348=param(5,340),[340], % 1.35/1.73 divide(inverse(divide(divide(X10,X11),X12)),divide(X11,X10)) = X12]. % 1.35/1.73 [389=param(62,340),[348], % 1.35/1.73 divide(X10,X10) = inverse(divide(X11,X11))]. % 1.35/1.73 [450=param(347,340),[], % 1.35/1.73 multiply(X10,inverse(divide(X11,X11))) = X10]. % 1.35/1.73 [451=param(347,347),[], % 1.35/1.73 multiply(X10,inverse(multiply(inverse(X11),X11))) = X10]. % 1.35/1.73 [458=param(62,450),[348], % 1.35/1.73 divide(X10,X10) = inverse(inverse(divide(X11,X11)))]. % 1.35/1.73 [480=param(347,450),[], % 1.35/1.73 multiply(X10,inverse(inverse(divide(X11,X11)))) = X10]. % 1.35/1.73 [482=param(389,1),[], % 1.35/1.73 inverse(divide(X10,X10)) = multiply(inverse(X11),X11)]. % 1.35/1.73 [484=param(2,389),[], % 1.35/1.73 divide(inverse(divide(inverse(divide(X10,X10)),divide(X11,divide(X12,X13)))),divide(X13,X12)) = X11]. % 1.35/1.73 [485=param(2,389),[], % 1.35/1.73 divide(inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))),divide(X13,X13)) = X12]. % 1.35/1.73 [490=param(6,389),[1,340], % 1.35/1.73 inverse(divide(divide(multiply(inverse(X10),X10),X11),divide(X12,X11))) = X12]. % 1.35/1.73 [493=param(7,389),[], % 1.35/1.73 divide(inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))),multiply(inverse(X13),X13)) = X12]. % 1.35/1.73 [510=param(17,389),[1,340], % 1.35/1.73 inverse(divide(divide(divide(X10,X10),divide(X11,X12)),X13)) = inverse(divide(multiply(divide(X12,X11),X14),multiply(X13,X14)))]. % 1.35/1.73 [615=param(1,389),[340], % 1.35/1.73 divide(X10,divide(X11,X11)) = X10]. % 1.35/1.73 [616=demod(485),[615], % 1.35/1.73 inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))) = X12]. % 1.35/1.73 [617=demod(493),[616], % 1.35/1.73 divide(X10,multiply(inverse(X11),X11)) = X10]. % 1.35/1.73 [620=param(2,389),[], % 1.35/1.73 divide(divide(X10,X10),divide(X11,X12)) = divide(X12,X11)]. % 1.35/1.73 [621=param(6,389),[], % 1.35/1.73 divide(divide(X10,X10),divide(inverse(X11),X12)) = multiply(X12,X11)]. % 1.35/1.73 [623=param(10,389),[], % 1.35/1.73 divide(divide(X10,X10),multiply(inverse(X11),X12)) = multiply(inverse(X12),X11)]. % 1.35/1.73 [677=param(60,615),[348], % 1.35/1.73 divide(X10,X10) = divide(X11,X11)]. % 1.35/1.73 [678=param(62,615),[], % 1.35/1.73 divide(divide(inverse(multiply(divide(X10,X11),X12)),divide(divide(X13,X13),X10)),X11) = inverse(X12)]. % 1.35/1.73 [688=param(82,615),[], % 1.35/1.73 divide(divide(inverse(divide(divide(X10,X10),X11)),multiply(divide(X12,X13),divide(divide(X13,X12),X14))),X14) = X11]. % 1.35/1.73 [706=param(615,173),[], % 1.35/1.73 multiply(divide(X11,X12),divide(multiply(divide(X12,X11),X13),multiply(divide(divide(X14,X14),X10),X13))) = X10]. % 1.35/1.73 [724=param(677,1),[], % 1.35/1.73 divide(X10,X10) = multiply(inverse(X11),X11)]. % 1.35/1.73 [741=param(18,677),[], % 1.35/1.73 divide(inverse(divide(divide(X10,X10),divide(X11,multiply(divide(X12,X13),divide(multiply(divide(X13,X12),X14),multiply(X15,X14)))))),X15) = X11]. % 1.35/1.73 [768=param(60,677),[], % 1.35/1.73 divide(divide(inverse(divide(X10,X10)),divide(X11,X12)),X13) = divide(divide(X12,X11),X13)]. % 1.35/1.73 [797=param(107,677),[], % 1.35/1.73 divide(divide(inverse(divide(divide(X10,X10),X11)),multiply(inverse(X12),X13)),multiply(inverse(X13),X12)) = X11]. % 1.35/1.73 [893=param(171,617),[], % 1.35/1.73 multiply(divide(X10,X11),divide(divide(divide(X11,X10),X12),divide(X13,X12))) = divide(multiply(inverse(X14),X14),X13)]. % 1.35/1.73 [910=param(233,617),[], % 1.35/1.73 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(inverse(X13),X12))) = multiply(multiply(inverse(X14),X14),X13)]. % 1.35/1.73 [915=param(284,617),[1], % 1.35/1.73 multiply(inverse(divide(X10,X10)),X11) = multiply(multiply(inverse(X12),X12),X11)]. % 1.35/1.73 [919=param(72,389),[], % 1.35/1.73 divide(divide(inverse(divide(inverse(divide(X10,X10)),X11)),X12),multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(X12,X15)))) = X11]. % 1.35/1.73 [943=param(16,724),[], % 1.35/1.73 divide(inverse(divide(multiply(inverse(X10),X10),divide(X11,X12))),multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(X12,X15)))) = X11]. % 1.35/1.73 [1025=param(62,480),[348], % 1.35/1.73 divide(X10,X10) = inverse(inverse(inverse(divide(X11,X11))))]. % 1.35/1.73 [1055=param(62,451),[348], % 1.35/1.73 divide(X10,X10) = inverse(inverse(multiply(inverse(X11),X11)))]. % 1.35/1.73 [1107=param(72,482),[], % 1.35/1.73 divide(divide(multiply(inverse(X10),X10),X11),X12) = divide(multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(X11,X15))),X12)]. % 1.35/1.73 [1142=param(7,458),[], % 1.35/1.73 divide(inverse(divide(inverse(inverse(divide(X10,X10))),divide(X11,divide(inverse(X12),X13)))),multiply(X13,X12)) = X11]. % 1.35/1.73 [1162=param(60,458),[], % 1.35/1.73 divide(divide(inverse(divide(inverse(inverse(divide(X10,X10))),X11)),divide(X12,X13)),divide(X13,X12)) = X11]. % 1.35/1.73 [1427=param(6,1055),[], % 1.35/1.73 divide(inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),divide(X11,multiply(X12,X13)))),divide(inverse(X13),X12)) = X11]. % 1.35/1.73 [1451=param(63,1055),[], % 1.35/1.73 divide(divide(inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),X11)),divide(inverse(X12),X13)),multiply(X13,X12)) = X11]. % 1.35/1.73 [1511=param(6,1025),[], % 1.35/1.73 divide(inverse(inverse(inverse(inverse(divide(X10,X10))))),divide(inverse(X11),X12)) = multiply(X12,X11)]. % 1.35/1.73 [1516=param(11,1025),[], % 1.35/1.73 divide(inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),divide(X11,multiply(inverse(X12),X13)))),multiply(inverse(X13),X12)) = X11]. % 1.35/1.73 [1538=param(64,1025),[], % 1.35/1.73 divide(divide(inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),X11)),multiply(X12,X13)),divide(inverse(X13),X12)) = X11]. % 1.35/1.73 [1677=param(14,621),[615,1], % 1.35/1.73 inverse(divide(divide(multiply(X10,X11),X13),divide(X12,X13))) = inverse(divide(multiply(X10,X11),X12))]. % 1.35/1.73 [1689=demod(490),[1677], % 1.35/1.73 inverse(divide(multiply(inverse(X10),X10),X11)) = X11]. % 1.35/1.73 [1694=demod(943),[1689], % 1.35/1.73 divide(divide(X10,X11),multiply(divide(X12,X13),divide(multiply(divide(X13,X12),X14),multiply(X11,X14)))) = X10]. % 1.35/1.73 [1695=demod(919),[1694], % 1.35/1.73 inverse(divide(inverse(divide(X10,X10)),X11)) = X11]. % 1.35/1.73 [1696=demod(484),[1695], % 1.35/1.73 divide(divide(X10,divide(X11,X12)),divide(X12,X11)) = X10]. % 1.35/1.73 [1698=demod(1162),[1696], % 1.35/1.73 inverse(divide(inverse(inverse(divide(X10,X10))),X11)) = X11]. % 1.35/1.73 [1699=demod(1142),[1698], % 1.35/1.73 divide(divide(X10,divide(inverse(X11),X12)),multiply(X12,X11)) = X10]. % 1.35/1.73 [1707=demod(1451),[1699], % 1.35/1.73 inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),X11)) = X11]. % 1.35/1.73 [1708=demod(1427),[1707], % 1.35/1.73 divide(divide(X10,multiply(X11,X12)),divide(inverse(X12),X11)) = X10]. % 1.35/1.73 [1709=demod(1538),[1708], % 1.35/1.73 inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),X11)) = X11]. % 1.35/1.73 [1710=demod(1516),[1709], % 1.35/1.73 divide(divide(X10,multiply(inverse(X11),X12)),multiply(inverse(X12),X11)) = X10]. % 1.35/1.73 [1714=demod(797),[1710], % 1.35/1.73 inverse(divide(divide(X10,X10),X11)) = X11]. % 1.35/1.73 [1726=demod(741),[1714], % 1.35/1.73 divide(divide(X10,multiply(divide(X11,X12),divide(multiply(divide(X12,X11),X13),multiply(X14,X13)))),X14) = X10]. % 1.35/1.73 [1742=demod(688),[1714], % 1.35/1.73 divide(divide(X10,multiply(divide(X11,X12),divide(divide(X12,X11),X13))),X13) = X10]. % 1.35/1.73 [1743=demod(341),[1742], % 1.35/1.73 divide(inverse(X11),X10) = inverse(multiply(X10,X11))]. % 1.35/1.73 [1757=demod(678),[1743,1743], % 1.35/1.73 inverse(multiply(X10,multiply(divide(divide(X11,X11),X12),multiply(divide(X12,X10),X13)))) = inverse(X13)]. % 1.35/1.73 [1782=demod(768),[1743,340,1743], % 1.35/1.73 divide(divide(X12,X11),X10) = inverse(multiply(X10,divide(X11,X12)))]. % 1.35/1.73 [1786=demod(620),[1782,340], % 1.35/1.73 inverse(divide(X10,X11)) = divide(X11,X10)]. % 1.35/1.73 [1787=demod(915),[1786], % 1.35/1.73 multiply(divide(X10,X10),X11) = multiply(multiply(inverse(X12),X12),X11)]. % 1.35/1.73 [1802=demod(706),[1782,340], % 1.35/1.73 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(inverse(X13),X12))) = X13]. % 1.35/1.73 [1814=demod(910),[1802], % 1.35/1.73 multiply(multiply(inverse(X11),X11),X10) = X10]. % 1.35/1.73 [1816=demod(1787),[1814], % 1.35/1.73 multiply(divide(X10,X10),X11) = X11]. % 1.35/1.73 [1832=demod(1107),[1782,617], % 1.35/1.73 divide(multiply(divide(X12,X13),divide(multiply(divide(X13,X12),X14),multiply(X11,X14))),X10) = inverse(multiply(X10,X11))]. % 1.35/1.73 [1833=demod(1757),[1782,340], % 1.35/1.73 inverse(multiply(X10,multiply(inverse(X11),multiply(divide(X11,X10),X12)))) = inverse(X12)]. % 1.35/1.73 [1835=demod(893),[1782,1743], % 1.35/1.73 multiply(divide(X10,X11),inverse(multiply(divide(X12,X13),multiply(X13,divide(X10,X11))))) = divide(multiply(inverse(X14),X14),X12)]. % 1.35/1.73 [1858=demod(623),[1782,340], % 1.35/1.73 inverse(multiply(inverse(X10),X11)) = multiply(inverse(X11),X10)]. % 1.35/1.73 [1875=demod(47),[1782,1743], % 1.35/1.73 inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))) = inverse(inverse(multiply(divide(X13,X14),multiply(X14,divide(X11,X10)))))]. % 1.35/1.73 [1877=demod(1726),[1782,1832], % 1.35/1.73 inverse(multiply(X10,inverse(multiply(X11,X10)))) = X11]. % 1.35/1.73 [1881=demod(510),[1782,340,1743], % 1.35/1.73 inverse(divide(multiply(divide(X12,X11),X13),multiply(X10,X13))) = inverse(inverse(multiply(X10,divide(X11,X12))))]. % 1.35/1.73 [1882=demod(46),[1881], % 1.35/1.73 inverse(inverse(multiply(divide(X10,divide(X11,X12)),divide(X11,X12)))) = X10]. % 1.35/1.73 [1883=demod(1875),[1881], % 1.35/1.73 inverse(inverse(multiply(divide(X10,X13),multiply(X13,divide(X11,X12))))) = inverse(inverse(multiply(X10,divide(X11,X12))))]. % 1.35/1.73 [1891=demod(214),[1782,1743], % 1.35/1.73 multiply(X10,inverse(multiply(divide(X11,X12),multiply(X12,divide(X13,X14))))) = multiply(X10,divide(multiply(divide(X14,X13),X15),multiply(X11,X15)))]. % 1.35/1.73 [1904=demod(1714),[1782,340], % 1.35/1.73 inverse(inverse(X10)) = X10]. % 1.35/1.73 [1906=demod(1882),[1904], % 1.35/1.73 multiply(divide(X10,divide(X11,X12)),divide(X11,X12)) = X10]. % 1.35/1.73 [1918=demod(1883),[1904,1904], % 1.35/1.73 multiply(divide(X10,X11),multiply(X11,divide(X12,X13))) = multiply(X10,divide(X12,X13))]. % 1.35/1.73 [1920=demod(1835),[1918], % 1.35/1.73 multiply(divide(X10,X11),inverse(multiply(X12,divide(X10,X11)))) = divide(multiply(inverse(X13),X13),X12)]. % 1.35/1.73 [1925=demod(1891),[1918], % 1.35/1.73 multiply(X10,divide(multiply(divide(X13,X12),X14),multiply(X11,X14))) = multiply(X10,inverse(multiply(X11,divide(X12,X13))))]. % 1.35/1.73 [1927=demod(238),[1925], % 1.35/1.73 multiply(divide(X10,X11),X12) = multiply(multiply(divide(X13,X14),inverse(multiply(divide(X11,X10),divide(X13,X14)))),X12)]. % 1.35/1.73 [1934=demod(48),[1925,1906], % 1.35/1.73 divide(X10,X11) = multiply(X10,inverse(X11))]. % 1.35/1.73 [1940=demod(1816),[1934], % 1.35/1.73 multiply(multiply(X10,inverse(X10)),X11) = X11]. % 1.35/1.73 [1943=demod(1833),[1934], % 1.35/1.73 inverse(multiply(X10,multiply(inverse(X11),multiply(multiply(X11,inverse(X10)),X12)))) = inverse(X12)]. % 1.35/1.73 [1945=demod(1786),[1934,1934], % 1.35/1.73 inverse(multiply(X10,inverse(X11))) = multiply(X11,inverse(X10))]. % 1.35/1.73 [1951=demod(1920),[1934,1934,1934,1814], % 1.35/1.73 multiply(multiply(X10,inverse(X11)),inverse(multiply(X12,multiply(X10,inverse(X11))))) = inverse(X12)]. % 1.35/1.73 [1977=demod(1927),[1934,1934,1934,1934,1951], % 1.35/1.73 multiply(multiply(X10,inverse(X11)),X12) = multiply(inverse(multiply(X11,inverse(X10))),X12)]. % 1.35/1.73 [2046=demod(1511),[1934,1945,1945,1945,1945,1934,1934,1940], % 1.35/1.73 inverse(multiply(inverse(X10),inverse(X11))) = multiply(X11,X10)]. % 1.35/1.73 [2238=param(1904,1877),[], % 1.35/1.73 multiply(X11,inverse(multiply(X10,X11))) = inverse(X10)]. % 1.35/1.73 [2248=param(2238,1858),[1904], % 1.35/1.73 multiply(X10,multiply(inverse(X10),X11)) = X11]. % 1.35/1.73 [2250=param(2248,1904),[], % 1.35/1.73 multiply(inverse(X10),multiply(X10,X11)) = X11]. % 1.35/1.73 [2259=param(1904,1943),[1904], % 1.35/1.73 multiply(X11,multiply(inverse(X12),multiply(multiply(X12,inverse(X11)),X10))) = X10]. % 1.35/1.73 [2270=param(2250,2046),[], % 1.35/1.73 multiply(multiply(X10,X11),multiply(multiply(inverse(X11),inverse(X10)),X12)) = X12]. % 1.35/1.73 [2335=param(2270,2248),[], % 1.35/1.73 multiply(multiply(X10,X11),X12) = multiply(inverse(multiply(inverse(X11),inverse(X10))),X12)]. % 1.35/1.73 [2336=param(2250,2270),[], % 1.35/1.73 multiply(inverse(multiply(X10,X11)),X12) = multiply(multiply(inverse(X11),inverse(X10)),X12)]. % 1.35/1.73 [2414=param(2259,2248),[], % 1.35/1.73 multiply(inverse(multiply(X11,inverse(X10))),X12) = multiply(X10,multiply(inverse(X11),X12))]. % 1.35/1.73 [2427=demod(1977),[2414], % 1.35/1.73 multiply(multiply(X10,inverse(X11)),X12) = multiply(X10,multiply(inverse(X11),X12))]. % 1.35/1.73 [2484=demod(2336),[2427], % 1.35/1.73 multiply(inverse(multiply(X10,X11)),X12) = multiply(inverse(X11),multiply(inverse(X10),X12))]. % 1.35/1.73 [2498=demod(2335),[2484,1904,1904], % 1.35/1.73 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 1.35/1.73 [2519=param(4,2498),[3], % 1.35/1.73 thmtrue = thmfalse]. % 1.35/1.73 % SZS output end CNFRefutation % 1.35/1.73 Space: 3853 KB %------------------------------------------------------------------------------