%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP476-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n032.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.03s 1.40s % Output : CNFRefutation 1.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.10 % Problem : GRP476-1 : TPTP v8.1.0. Released v2.6.0. % 0.10/0.10 % Command : fiesta-wrapper %s % 0.10/0.29 % Computer : n032.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 600 % 0.10/0.29 % DateTime : Mon Jun 13 18:48:27 EDT 2022 % 0.10/0.29 % CPUTime : % 1.03/1.40 Theorem Proved. % 1.03/1.40 % SZS status Unsatisfiable % 1.03/1.40 % SZS output start CNFRefutation % 1.03/1.40 [1=axiom,[], % 1.03/1.40 divide(X10,inverse(X11)) = multiply(X10,X11)]. % 1.03/1.40 [2=axiom,[], % 1.03/1.40 divide(inverse(divide(divide(divide(X10,X11),X12),divide(X13,X12))),divide(X11,X10)) = X13]. % 1.03/1.40 [3=axiom,[], % 1.03/1.40 thtop(X10,X10) = thmfalse]. % 1.03/1.40 [4=axiom,[], % 1.03/1.40 thtop(multiply(multiply(inverse(b2),b2),a2),a2) = thmtrue]. % 1.03/1.40 [5=param(2,1),[1], % 1.03/1.40 divide(inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))),divide(X11,X10)) = X13]. % 1.03/1.40 [6=param(2,1),[], % 1.03/1.40 divide(inverse(divide(divide(multiply(X10,X11),X12),divide(X13,X12))),divide(inverse(X11),X10)) = X13]. % 1.03/1.40 [7=param(2,1),[], % 1.03/1.40 divide(inverse(divide(divide(divide(inverse(X10),X11),X12),divide(X13,X12))),multiply(X11,X10)) = X13]. % 1.03/1.40 [11=param(6,1),[], % 1.03/1.40 divide(inverse(divide(divide(multiply(inverse(X10),X11),X12),divide(X13,X12))),multiply(inverse(X11),X10)) = X13]. % 1.03/1.40 [12=param(5,5),[1], % 1.03/1.40 divide(inverse(divide(multiply(multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(X13,X12))),X14),multiply(X15,X14))),X13) = X15]. % 1.03/1.40 [13=param(2,2),[1], % 1.03/1.40 divide(inverse(divide(divide(X10,X11),divide(X12,X11))),multiply(divide(X13,X14),divide(divide(divide(X14,X13),X15),divide(X10,X15)))) = X12]. % 1.03/1.40 [14=param(2,2),[], % 1.03/1.40 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.03/1.40 [16=param(2,5),[1], % 1.03/1.40 divide(inverse(divide(divide(X10,X11),divide(X12,X11))),multiply(divide(X13,X14),divide(multiply(divide(X14,X13),X15),multiply(X10,X15)))) = X12]. % 1.03/1.40 [17=param(2,5),[], % 1.03/1.40 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.03/1.40 [39=param(14,2),[], % 1.03/1.40 inverse(divide(divide(divide(X10,X11),X12),divide(divide(X13,divide(X11,X10)),X12))) = X13]. % 1.03/1.40 [40=param(14,14),[39], % 1.03/1.40 divide(divide(inverse(divide(divide(divide(X10,X11),divide(X12,X13)),X14)),divide(X11,X10)),divide(X12,X13)) = X14]. % 1.03/1.40 [43=param(13,39),[], % 1.03/1.40 divide(X10,multiply(divide(X11,X12),divide(divide(divide(X12,X11),X13),divide(divide(X14,X15),X13)))) = divide(X10,divide(X15,X14))]. % 1.03/1.40 [46=param(17,2),[], % 1.03/1.40 inverse(divide(multiply(divide(X10,X11),X12),multiply(divide(X13,divide(X11,X10)),X12))) = X13]. % 1.03/1.40 [47=param(17,14),[], % 1.03/1.40 inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))) = inverse(divide(divide(divide(X10,X11),X14),divide(X13,X14)))]. % 1.03/1.40 [48=param(1,46),[], % 1.03/1.40 divide(X10,X11) = multiply(X10,divide(multiply(divide(X12,X13),X14),multiply(divide(X11,divide(X13,X12)),X14)))]. % 1.03/1.40 [60=param(40,2),[2], % 1.03/1.40 divide(divide(inverse(divide(divide(divide(X10,X11),X12),X13)),divide(X11,X10)),X12) = X13]. % 1.03/1.40 [62=param(60,1),[], % 1.03/1.40 divide(divide(inverse(multiply(divide(divide(X10,X11),X12),X13)),divide(X11,X10)),X12) = inverse(X13)]. % 1.03/1.40 [63=param(60,1),[], % 1.03/1.40 divide(divide(inverse(divide(divide(multiply(X10,X11),X12),X13)),divide(inverse(X11),X10)),X12) = X13]. % 1.03/1.40 [64=param(60,1),[], % 1.03/1.40 divide(divide(inverse(divide(divide(divide(inverse(X10),X11),X12),X13)),multiply(X11,X10)),X12) = X13]. % 1.03/1.40 [72=param(60,5),[1], % 1.03/1.40 divide(divide(inverse(divide(divide(multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(X13,X12))),X14),X15)),X13),X14) = X15]. % 1.03/1.40 [82=param(60,60),[1], % 1.03/1.40 divide(divide(inverse(divide(X10,X11)),multiply(divide(X12,X13),divide(divide(divide(X13,X12),X14),X10))),X14) = X11]. % 1.03/1.40 [107=param(64,1),[], % 1.03/1.40 divide(divide(inverse(divide(divide(multiply(inverse(X10),X11),X12),X13)),multiply(inverse(X11),X10)),X12) = X13]. % 1.03/1.40 [171=param(60,43),[60], % 1.03/1.40 multiply(divide(X12,X13),divide(divide(divide(X13,X12),X14),divide(divide(X11,X10),X14))) = divide(X10,X11)]. % 1.03/1.40 [172=param(171,1),[], % 1.03/1.40 multiply(multiply(X10,X11),divide(divide(divide(inverse(X11),X10),X12),divide(divide(X13,X14),X12))) = divide(X14,X13)]. % 1.03/1.40 [173=param(171,1),[1], % 1.03/1.40 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(divide(X13,X14),X12))) = divide(X14,X13)]. % 1.03/1.40 [175=param(171,1),[], % 1.03/1.40 multiply(divide(X10,X11),divide(divide(divide(X11,X10),X12),divide(multiply(X13,X14),X12))) = divide(inverse(X14),X13)]. % 1.03/1.40 [211=param(12,172),[5], % 1.03/1.40 divide(inverse(divide(divide(X10,X11),multiply(X12,divide(divide(X13,X14),divide(divide(X11,X10),X14))))),X13) = X12]. % 1.03/1.40 [214=param(1,47),[1], % 1.03/1.40 multiply(X10,divide(divide(divide(X11,X12),X13),divide(X14,X13))) = multiply(X10,divide(multiply(divide(X11,X12),X15),multiply(X14,X15)))]. % 1.03/1.40 [233=param(173,1),[], % 1.03/1.40 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(divide(inverse(X13),X14),X12))) = multiply(X14,X13)]. % 1.03/1.40 [279=param(211,172),[], % 1.03/1.40 divide(inverse(divide(divide(X10,X11),divide(X10,X11))),divide(inverse(X12),X13)) = multiply(X13,X12)]. % 1.03/1.40 [284=param(279,2),[2], % 1.03/1.40 divide(inverse(divide(X10,X10)),divide(inverse(X11),X12)) = multiply(X12,X11)]. % 1.03/1.40 [318=param(82,284),[1], % 1.03/1.40 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.03/1.40 [331=param(171,284),[175,1], % 1.03/1.40 multiply(divide(inverse(X10),X11),divide(X12,X12)) = divide(inverse(X10),X11)]. % 1.03/1.40 [340=param(331,2),[2], % 1.03/1.40 multiply(X10,divide(X11,X11)) = X10]. % 1.03/1.40 [341=demod(318),[340], % 1.03/1.40 divide(divide(inverse(multiply(X10,X11)),multiply(divide(X12,X13),divide(divide(X13,X12),X14))),X14) = divide(inverse(X11),X10)]. % 1.03/1.40 [347=param(340,1),[], % 1.03/1.40 multiply(X10,multiply(inverse(X11),X11)) = X10]. % 1.03/1.40 [348=param(5,340),[340], % 1.03/1.40 divide(inverse(divide(divide(X10,X11),X12)),divide(X11,X10)) = X12]. % 1.03/1.40 [389=param(62,340),[348], % 1.03/1.40 divide(X10,X10) = inverse(divide(X11,X11))]. % 1.03/1.40 [450=param(347,340),[], % 1.03/1.40 multiply(X10,inverse(divide(X11,X11))) = X10]. % 1.03/1.40 [451=param(347,347),[], % 1.03/1.40 multiply(X10,inverse(multiply(inverse(X11),X11))) = X10]. % 1.03/1.40 [458=param(62,450),[348], % 1.03/1.40 divide(X10,X10) = inverse(inverse(divide(X11,X11)))]. % 1.03/1.40 [480=param(347,450),[], % 1.03/1.40 multiply(X10,inverse(inverse(divide(X11,X11)))) = X10]. % 1.03/1.40 [484=param(2,389),[], % 1.03/1.40 divide(inverse(divide(inverse(divide(X10,X10)),divide(X11,divide(X12,X13)))),divide(X13,X12)) = X11]. % 1.03/1.40 [485=param(2,389),[], % 1.03/1.40 divide(inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))),divide(X13,X13)) = X12]. % 1.03/1.40 [490=param(6,389),[1,340], % 1.03/1.40 inverse(divide(divide(multiply(inverse(X10),X10),X11),divide(X12,X11))) = X12]. % 1.03/1.40 [493=param(7,389),[], % 1.03/1.40 divide(inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))),multiply(inverse(X13),X13)) = X12]. % 1.03/1.40 [510=param(17,389),[1,340], % 1.03/1.40 inverse(divide(divide(divide(X10,X10),divide(X11,X12)),X13)) = inverse(divide(multiply(divide(X12,X11),X14),multiply(X13,X14)))]. % 1.03/1.40 [615=param(1,389),[340], % 1.03/1.40 divide(X10,divide(X11,X11)) = X10]. % 1.03/1.40 [616=demod(485),[615], % 1.03/1.40 inverse(divide(divide(inverse(divide(X10,X10)),X11),divide(X12,X11))) = X12]. % 1.03/1.40 [617=demod(493),[616], % 1.03/1.40 divide(X10,multiply(inverse(X11),X11)) = X10]. % 1.03/1.40 [620=param(2,389),[], % 1.03/1.40 divide(divide(X10,X10),divide(X11,X12)) = divide(X12,X11)]. % 1.03/1.40 [621=param(6,389),[], % 1.03/1.40 divide(divide(X10,X10),divide(inverse(X11),X12)) = multiply(X12,X11)]. % 1.03/1.40 [677=param(60,615),[348], % 1.03/1.40 divide(X10,X10) = divide(X11,X11)]. % 1.03/1.40 [688=param(82,615),[], % 1.03/1.40 divide(divide(inverse(divide(divide(X10,X10),X11)),multiply(divide(X12,X13),divide(divide(X13,X12),X14))),X14) = X11]. % 1.03/1.40 [706=param(615,173),[], % 1.03/1.40 multiply(divide(X11,X12),divide(multiply(divide(X12,X11),X13),multiply(divide(divide(X14,X14),X10),X13))) = X10]. % 1.03/1.40 [724=param(677,1),[], % 1.03/1.40 divide(X10,X10) = multiply(inverse(X11),X11)]. % 1.03/1.40 [768=param(60,677),[], % 1.03/1.40 divide(divide(inverse(divide(X10,X10)),divide(X11,X12)),X13) = divide(divide(X12,X11),X13)]. % 1.03/1.40 [797=param(107,677),[], % 1.03/1.40 divide(divide(inverse(divide(divide(X10,X10),X11)),multiply(inverse(X12),X13)),multiply(inverse(X13),X12)) = X11]. % 1.03/1.40 [910=param(233,617),[], % 1.03/1.40 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(inverse(X13),X12))) = multiply(multiply(inverse(X14),X14),X13)]. % 1.03/1.40 [915=param(284,617),[1], % 1.03/1.40 multiply(inverse(divide(X10,X10)),X11) = multiply(multiply(inverse(X12),X12),X11)]. % 1.03/1.40 [919=param(72,389),[], % 1.03/1.40 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.03/1.40 [924=param(724,1),[], % 1.03/1.40 multiply(inverse(X10),X10) = multiply(inverse(X11),X11)]. % 1.03/1.40 [943=param(16,724),[], % 1.03/1.40 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.03/1.40 [1028=param(62,480),[348], % 1.03/1.40 divide(X10,X10) = inverse(inverse(inverse(divide(X11,X11))))]. % 1.03/1.40 [1056=param(62,451),[348], % 1.03/1.40 divide(X10,X10) = inverse(inverse(multiply(inverse(X11),X11)))]. % 1.03/1.40 [1084=param(4,924),[], % 1.03/1.40 thtop(multiply(multiply(inverse(X10),X10),a2),a2) = thmtrue]. % 1.03/1.40 [1140=param(7,458),[], % 1.03/1.40 divide(inverse(divide(inverse(inverse(divide(X10,X10))),divide(X11,divide(inverse(X12),X13)))),multiply(X13,X12)) = X11]. % 1.03/1.40 [1160=param(60,458),[], % 1.03/1.40 divide(divide(inverse(divide(inverse(inverse(divide(X10,X10))),X11)),divide(X12,X13)),divide(X13,X12)) = X11]. % 1.03/1.40 [1409=param(6,1056),[], % 1.03/1.40 divide(inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),divide(X11,multiply(X12,X13)))),divide(inverse(X13),X12)) = X11]. % 1.03/1.40 [1433=param(63,1056),[], % 1.03/1.40 divide(divide(inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),X11)),divide(inverse(X12),X13)),multiply(X13,X12)) = X11]. % 1.03/1.40 [1498=param(11,1028),[], % 1.03/1.40 divide(inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),divide(X11,multiply(inverse(X12),X13)))),multiply(inverse(X13),X12)) = X11]. % 1.03/1.40 [1520=param(64,1028),[], % 1.03/1.40 divide(divide(inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),X11)),multiply(X12,X13)),divide(inverse(X13),X12)) = X11]. % 1.03/1.40 [1652=param(14,621),[615,1], % 1.03/1.40 inverse(divide(divide(multiply(X10,X11),X13),divide(X12,X13))) = inverse(divide(multiply(X10,X11),X12))]. % 1.03/1.40 [1664=demod(490),[1652], % 1.03/1.40 inverse(divide(multiply(inverse(X10),X10),X11)) = X11]. % 1.03/1.40 [1669=demod(943),[1664], % 1.03/1.40 divide(divide(X10,X11),multiply(divide(X12,X13),divide(multiply(divide(X13,X12),X14),multiply(X11,X14)))) = X10]. % 1.03/1.40 [1670=demod(919),[1669], % 1.03/1.40 inverse(divide(inverse(divide(X10,X10)),X11)) = X11]. % 1.03/1.40 [1671=demod(484),[1670], % 1.03/1.40 divide(divide(X10,divide(X11,X12)),divide(X12,X11)) = X10]. % 1.03/1.40 [1673=demod(1160),[1671], % 1.03/1.40 inverse(divide(inverse(inverse(divide(X10,X10))),X11)) = X11]. % 1.03/1.40 [1674=demod(1140),[1673], % 1.03/1.40 divide(divide(X10,divide(inverse(X11),X12)),multiply(X12,X11)) = X10]. % 1.03/1.40 [1682=demod(1433),[1674], % 1.03/1.40 inverse(divide(inverse(inverse(multiply(inverse(X10),X10))),X11)) = X11]. % 1.03/1.40 [1683=demod(1409),[1682], % 1.03/1.40 divide(divide(X10,multiply(X11,X12)),divide(inverse(X12),X11)) = X10]. % 1.03/1.40 [1684=demod(1520),[1683], % 1.03/1.40 inverse(divide(inverse(inverse(inverse(divide(X10,X10)))),X11)) = X11]. % 1.03/1.40 [1685=demod(1498),[1684], % 1.03/1.40 divide(divide(X10,multiply(inverse(X11),X12)),multiply(inverse(X12),X11)) = X10]. % 1.03/1.40 [1689=demod(797),[1685], % 1.03/1.40 inverse(divide(divide(X10,X10),X11)) = X11]. % 1.03/1.40 [1717=demod(688),[1689], % 1.03/1.40 divide(divide(X10,multiply(divide(X11,X12),divide(divide(X12,X11),X13))),X13) = X10]. % 1.03/1.40 [1718=demod(341),[1717], % 1.03/1.40 divide(inverse(X11),X10) = inverse(multiply(X10,X11))]. % 1.03/1.40 [1757=demod(768),[1718,340,1718], % 1.03/1.40 divide(divide(X12,X11),X10) = inverse(multiply(X10,divide(X11,X12)))]. % 1.03/1.40 [1761=demod(620),[1757,340], % 1.03/1.40 inverse(divide(X10,X11)) = divide(X11,X10)]. % 1.03/1.40 [1762=demod(915),[1761], % 1.03/1.40 multiply(divide(X10,X10),X11) = multiply(multiply(inverse(X12),X12),X11)]. % 1.03/1.40 [1777=demod(706),[1757,340], % 1.03/1.40 multiply(divide(X10,X11),divide(multiply(divide(X11,X10),X12),multiply(inverse(X13),X12))) = X13]. % 1.03/1.40 [1789=demod(910),[1777], % 1.03/1.40 multiply(multiply(inverse(X11),X11),X10) = X10]. % 1.03/1.40 [1791=demod(1762),[1789], % 1.03/1.40 multiply(divide(X10,X10),X11) = X11]. % 1.03/1.40 [1850=demod(47),[1757,1718], % 1.03/1.40 inverse(divide(multiply(divide(X10,X11),X12),multiply(X13,X12))) = inverse(inverse(multiply(divide(X13,X14),multiply(X14,divide(X11,X10)))))]. % 1.03/1.40 [1856=demod(510),[1757,340,1718], % 1.03/1.40 inverse(divide(multiply(divide(X12,X11),X13),multiply(X10,X13))) = inverse(inverse(multiply(X10,divide(X11,X12))))]. % 1.03/1.40 [1857=demod(46),[1856], % 1.03/1.40 inverse(inverse(multiply(divide(X10,divide(X11,X12)),divide(X11,X12)))) = X10]. % 1.03/1.40 [1858=demod(1850),[1856], % 1.03/1.40 inverse(inverse(multiply(divide(X10,X13),multiply(X13,divide(X11,X12))))) = inverse(inverse(multiply(X10,divide(X11,X12))))]. % 1.03/1.40 [1862=demod(615),[], % 1.03/1.40 divide(X10,divide(X11,X11)) = X10]. % 1.03/1.41 [1866=demod(214),[1757,1718], % 1.03/1.41 multiply(X10,inverse(multiply(divide(X11,X12),multiply(X12,divide(X13,X14))))) = multiply(X10,divide(multiply(divide(X14,X13),X15),multiply(X11,X15)))]. % 1.03/1.41 [1879=demod(1689),[1757,340], % 1.03/1.41 inverse(inverse(X10)) = X10]. % 1.03/1.41 [1881=demod(1857),[1879], % 1.03/1.41 multiply(divide(X10,divide(X11,X12)),divide(X11,X12)) = X10]. % 1.03/1.41 [1891=demod(1862),[], % 1.03/1.41 divide(X10,divide(X11,X11)) = X10]. % 1.03/1.41 [1893=demod(1858),[1879,1879], % 1.03/1.41 multiply(divide(X10,X11),multiply(X11,divide(X12,X13))) = multiply(X10,divide(X12,X13))]. % 1.03/1.41 [1900=demod(1866),[1893], % 1.03/1.41 multiply(X10,divide(multiply(divide(X13,X12),X14),multiply(X11,X14))) = multiply(X10,inverse(multiply(X11,divide(X12,X13))))]. % 1.03/1.41 [1909=demod(48),[1900,1881], % 1.03/1.41 divide(X10,X11) = multiply(X10,inverse(X11))]. % 1.03/1.41 [1915=demod(1791),[1909], % 1.03/1.41 multiply(multiply(X10,inverse(X10)),X11) = X11]. % 1.03/1.41 [1920=demod(1761),[1909,1909], % 1.03/1.41 inverse(multiply(X10,inverse(X11))) = multiply(X11,inverse(X10))]. % 1.03/1.41 [1966=demod(1891),[1909,1909,1920], % 1.03/1.41 multiply(X10,multiply(X11,inverse(X11))) = X10]. % 1.03/1.41 [2198=param(1084,1966),[1920,1915,3], % 1.03/1.41 thmtrue = thmfalse]. % 1.03/1.41 % SZS output end CNFRefutation % 1.03/1.41 Space: 3498 KB %------------------------------------------------------------------------------