%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO024-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n017.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 : Thu Jul 14 23:38:50 EDT 2022 % Result : Unsatisfiable 0.82s 1.19s % Output : CNFRefutation 0.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : BOO024-1 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.12 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 1 19:16:42 EDT 2022 % 0.12/0.34 % CPUTime : % 0.82/1.19 Theorem Proved. % 0.82/1.19 % SZS status Unsatisfiable % 0.82/1.19 % SZS output start CNFRefutation % 0.82/1.19 [1=axiom,[], % 0.82/1.19 pixley(X10,X11,X10) = X10]. % 0.82/1.19 [2=axiom,[], % 0.82/1.19 pixley(X10,X11,X11) = X10]. % 0.82/1.19 [3=axiom,[], % 0.82/1.19 pixley(X10,X10,X11) = X11]. % 0.82/1.19 [4=axiom,[], % 0.82/1.19 pixley(X10,X11,X12) = add(multiply(X10,inverse(X11)),add(multiply(X10,X12),multiply(inverse(X11),X12)))]. % 0.82/1.19 [5=demod(1),[4], % 0.82/1.19 add(multiply(X10,inverse(X11)),add(multiply(X10,X10),multiply(inverse(X11),X10))) = X10]. % 0.82/1.19 [6=demod(2),[4], % 0.82/1.19 add(multiply(X10,inverse(X11)),add(multiply(X10,X11),multiply(inverse(X11),X11))) = X10]. % 0.82/1.19 [7=demod(3),[4], % 0.82/1.19 add(multiply(X10,inverse(X10)),add(multiply(X10,X11),multiply(inverse(X10),X11))) = X11]. % 0.82/1.19 [8=axiom,[], % 0.82/1.19 add(X10,inverse(X10)) = n1]. % 0.82/1.19 [9=axiom,[], % 0.82/1.19 add(multiply(X11,X10),multiply(X12,X10)) = multiply(X10,add(X11,X12))]. % 0.82/1.19 [11=demod(5),[9], % 0.82/1.19 add(multiply(X10,inverse(X11)),multiply(X10,add(X10,inverse(X11)))) = X10]. % 0.82/1.19 [12=demod(6),[9], % 0.82/1.19 add(multiply(X10,inverse(X11)),multiply(X11,add(X10,inverse(X11)))) = X10]. % 0.82/1.19 [13=demod(7),[9,8], % 0.82/1.19 add(multiply(X10,inverse(X10)),multiply(X11,n1)) = X11]. % 0.82/1.19 [14=axiom,[], % 0.82/1.19 multiply(add(X10,X11),X11) = X11]. % 0.82/1.19 [15=axiom,[], % 0.82/1.19 thtop(X10,X10) = thmfalse]. % 0.82/1.19 [16=axiom,[], % 0.82/1.19 thtop(add(multiply(a,b),b),b) = thmtrue]. % 0.82/1.19 [17=param(14,8),[], % 0.82/1.19 multiply(n1,inverse(X10)) = inverse(X10)]. % 0.82/1.19 [18=param(9,14),[], % 0.82/1.19 multiply(X10,add(add(X12,X10),X11)) = add(X10,multiply(X11,X10))]. % 0.82/1.19 [19=param(9,14),[], % 0.82/1.19 add(multiply(X10,X11),X11) = multiply(X11,add(X10,add(X12,X11)))]. % 0.82/1.19 [20=param(14,9),[], % 0.82/1.19 multiply(multiply(X10,add(X11,X12)),multiply(X12,X10)) = multiply(X12,X10)]. % 0.82/1.19 [22=param(9,17),[], % 0.82/1.19 add(multiply(X10,inverse(X11)),inverse(X11)) = multiply(inverse(X11),add(X10,n1))]. % 0.82/1.19 [24=param(14,13),[], % 0.82/1.19 multiply(X10,multiply(X10,n1)) = multiply(X10,n1)]. % 0.82/1.19 [25=param(13,17),[], % 0.82/1.19 add(inverse(n1),multiply(X10,n1)) = X10]. % 0.82/1.19 [26=param(25,14),[], % 0.82/1.19 add(inverse(n1),n1) = add(X10,n1)]. % 0.82/1.19 [30=param(18,26),[], % 0.82/1.19 multiply(X10,add(inverse(n1),n1)) = add(X10,multiply(n1,X10))]. % 0.82/1.19 [33=param(14,19),[], % 0.82/1.19 multiply(multiply(X10,add(X11,add(X12,X10))),X10) = X10]. % 0.82/1.19 [34=param(16,19),[], % 0.82/1.19 thtop(multiply(b,add(a,add(X10,b))),b) = thmtrue]. % 0.82/1.19 [36=param(19,26),[], % 0.82/1.19 multiply(n1,add(X10,add(X11,n1))) = add(inverse(n1),n1)]. % 0.82/1.19 [47=param(36,26),[], % 0.82/1.19 multiply(n1,add(X10,add(X11,n1))) = add(X12,n1)]. % 0.82/1.19 [48=param(30,26),[], % 0.82/1.19 multiply(X10,add(X11,n1)) = add(X10,multiply(n1,X10))]. % 0.82/1.19 [53=param(48,30),[], % 0.82/1.19 multiply(X10,add(X11,n1)) = multiply(X10,add(inverse(n1),n1))]. % 0.82/1.19 [54=param(47,18),[14], % 0.82/1.19 add(X10,n1) = add(n1,n1)]. % 0.82/1.19 [55=demod(53),[], % 0.82/1.19 multiply(X10,add(X11,n1)) = multiply(X10,add(inverse(n1),n1))]. % 0.82/1.19 [57=demod(26),[], % 0.82/1.19 add(inverse(n1),n1) = add(X10,n1)]. % 0.82/1.19 [61=param(55,54),[], % 0.82/1.19 multiply(X10,add(n1,n1)) = multiply(X10,add(X11,n1))]. % 0.82/1.19 [65=param(61,54),[], % 0.82/1.19 multiply(X10,add(X11,n1)) = multiply(X10,add(X12,n1))]. % 0.82/1.19 [67=param(65,14),[], % 0.82/1.19 multiply(add(X10,add(X11,n1)),add(X12,n1)) = add(X11,n1)]. % 0.82/1.19 [85=param(9,24),[], % 0.82/1.19 add(multiply(X10,n1),multiply(X11,multiply(X10,n1))) = multiply(multiply(X10,n1),add(X10,X11))]. % 0.82/1.19 [91=param(12,14),[], % 0.82/1.19 add(inverse(X10),multiply(X10,add(add(X11,inverse(X10)),inverse(X10)))) = add(X11,inverse(X10))]. % 0.82/1.19 [106=param(48,47),[67], % 0.82/1.19 add(add(X10,add(X11,n1)),add(X12,n1)) = add(X11,n1)]. % 0.82/1.19 [109=param(22,19),[], % 0.82/1.19 multiply(inverse(X10),add(X11,add(X12,inverse(X10)))) = multiply(inverse(X10),add(X11,n1))]. % 0.82/1.19 [113=param(33,106),[], % 0.82/1.19 multiply(multiply(n1,add(X10,n1)),n1) = n1]. % 0.82/1.19 [114=param(47,106),[], % 0.82/1.19 multiply(n1,add(X10,n1)) = add(X11,n1)]. % 0.82/1.19 [118=param(106,106),[], % 0.82/1.19 add(add(X10,n1),add(X11,n1)) = add(X12,n1)]. % 0.82/1.19 [121=param(113,18),[], % 0.82/1.19 multiply(add(n1,multiply(n1,n1)),n1) = n1]. % 0.82/1.19 [126=param(13,121),[-26], % 0.82/1.19 add(inverse(n1),n1) = add(n1,multiply(n1,n1))]. % 0.82/1.19 [132=demod(57),[126], % 0.82/1.19 add(n1,multiply(n1,n1)) = add(X10,n1)]. % 0.82/1.19 [152=param(114,19),[], % 0.82/1.19 multiply(n1,add(X10,n1)) = multiply(n1,add(X11,add(X12,n1)))]. % 0.82/1.19 [223=param(118,132),[], % 0.82/1.19 add(add(X10,n1),add(X11,n1)) = add(n1,multiply(n1,n1))]. % 0.82/1.19 [224=param(14,223),[], % 0.82/1.19 multiply(add(n1,multiply(n1,n1)),add(X10,n1)) = add(X10,n1)]. % 0.82/1.19 [236=param(224,48),[], % 0.82/1.19 multiply(multiply(n1,add(X10,n1)),add(X11,n1)) = add(X11,n1)]. % 0.82/1.19 [399=param(236,152),[], % 0.82/1.19 multiply(multiply(n1,add(X10,add(X11,n1))),add(X12,n1)) = add(X12,n1)]. % 0.82/1.19 [429=param(85,24),[9], % 0.82/1.19 multiply(multiply(X10,n1),add(X10,X10)) = multiply(n1,add(X10,X10))]. % 0.82/1.19 [431=param(9,429),[9], % 0.82/1.19 multiply(add(X10,X10),add(X11,multiply(X10,n1))) = multiply(add(X10,X10),add(X11,n1))]. % 0.82/1.19 [439=param(431,13),[14,-26], % 0.82/1.19 multiply(add(X10,X10),add(inverse(n1),n1)) = X10]. % 0.82/1.19 [449=param(20,439),[], % 0.82/1.19 multiply(X10,multiply(n1,add(X10,X10))) = multiply(n1,add(X10,X10))]. % 0.82/1.19 [452=param(439,65),[], % 0.82/1.19 multiply(add(X10,X10),add(X11,n1)) = X10]. % 0.82/1.19 [456=param(9,452),[], % 0.82/1.19 add(multiply(X10,add(X11,n1)),X12) = multiply(add(X11,n1),add(X10,add(X12,X12)))]. % 0.82/1.19 [457=param(452,47),[399], % 0.82/1.19 add(X10,n1) = n1]. % 0.82/1.19 [470=demod(456),[457,457], % 0.82/1.19 add(multiply(X10,n1),X11) = multiply(n1,add(X10,add(X11,X11)))]. % 0.82/1.19 [471=demod(452),[457], % 0.82/1.19 multiply(add(X10,X10),n1) = X10]. % 0.82/1.19 [472=demod(109),[457], % 0.82/1.19 multiply(inverse(X10),add(X11,add(X12,inverse(X10)))) = multiply(inverse(X10),n1)]. % 0.82/1.19 [478=param(13,471),[], % 0.82/1.19 add(multiply(X10,inverse(X10)),X11) = add(X11,X11)]. % 0.82/1.19 [479=param(25,471),[], % 0.82/1.19 add(inverse(n1),X10) = add(X10,X10)]. % 0.82/1.19 [489=param(479,25),[9], % 0.82/1.19 multiply(n1,add(X10,X10)) = X10]. % 0.82/1.19 [490=demod(449),[489,489], % 0.82/1.19 multiply(X10,X10) = X10]. % 0.82/1.19 [497=param(479,91),[9,457], % 0.82/1.19 multiply(add(add(X10,inverse(n1)),inverse(n1)),n1) = add(X10,inverse(n1))]. % 0.82/1.19 [499=param(479,9),[], % 0.82/1.19 add(inverse(n1),multiply(X10,X11)) = multiply(X11,add(X10,X10))]. % 0.82/1.19 [500=param(11,479),[490], % 0.82/1.19 add(inverse(X10),multiply(inverse(X10),add(inverse(n1),inverse(X10)))) = inverse(X10)]. % 0.82/1.19 [504=param(471,479),[], % 0.82/1.19 multiply(add(inverse(n1),X10),n1) = X10]. % 0.82/1.19 [515=param(9,490),[], % 0.82/1.19 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.82/1.19 [520=demod(19),[515], % 0.82/1.19 multiply(X10,add(X11,add(X12,X10))) = multiply(X10,add(X11,X10))]. % 0.82/1.19 [524=demod(472),[520], % 0.82/1.19 multiply(inverse(X10),add(X11,inverse(X10))) = multiply(inverse(X10),n1)]. % 0.82/1.19 [525=demod(500),[524], % 0.82/1.19 add(inverse(X10),multiply(inverse(X10),n1)) = inverse(X10)]. % 0.82/1.19 [534=param(489,479),[], % 0.82/1.19 multiply(n1,add(inverse(n1),X10)) = X10]. % 0.82/1.19 [538=param(534,8),[490], % 0.82/1.19 inverse(inverse(n1)) = n1]. % 0.82/1.19 [541=param(9,534),[457,504], % 0.82/1.19 add(multiply(X10,add(inverse(n1),X11)),X11) = X11]. % 0.82/1.19 [542=param(534,25),[], % 0.82/1.19 multiply(n1,X10) = multiply(X10,n1)]. % 0.82/1.19 [543=demod(525),[-542,17], % 0.82/1.19 add(inverse(X10),inverse(X10)) = inverse(X10)]. % 0.82/1.19 [551=demod(497),[-542], % 0.82/1.19 multiply(n1,add(add(X10,inverse(n1)),inverse(n1))) = add(X10,inverse(n1))]. % 0.82/1.19 [552=param(534,91),[551], % 0.82/1.19 multiply(n1,add(X10,inverse(n1))) = add(X10,inverse(n1))]. % 0.82/1.19 [554=param(12,538),[538,457,-542,17,470,543,552], % 0.82/1.19 add(X10,inverse(n1)) = X10]. % 0.82/1.19 [555=demod(552),[554,554], % 0.82/1.19 multiply(n1,X10) = X10]. % 0.82/1.19 [556=demod(542),[555], % 0.82/1.19 multiply(X10,n1) = X10]. % 0.82/1.19 [559=demod(13),[556], % 0.82/1.19 add(multiply(X10,inverse(X10)),X11) = X11]. % 0.82/1.19 [560=demod(478),[559], % 0.82/1.19 add(X10,X10) = X10]. % 0.82/1.19 [564=demod(499),[560], % 0.82/1.19 add(inverse(n1),multiply(X10,X11)) = multiply(X11,X10)]. % 0.82/1.19 [567=demod(479),[560], % 0.82/1.19 add(inverse(n1),X10) = X10]. % 0.82/1.19 [568=demod(541),[567,515], % 0.82/1.19 multiply(X10,add(X11,X10)) = X10]. % 0.82/1.19 [569=demod(520),[568], % 0.82/1.19 multiply(X10,add(X11,add(X12,X10))) = X10]. % 0.82/1.19 [571=demod(564),[567], % 0.82/1.19 multiply(X10,X11) = multiply(X11,X10)]. % 0.82/1.19 [614=param(34,571),[571,569,15], % 0.82/1.19 thmtrue = thmfalse]. % 0.82/1.19 % SZS output end CNFRefutation % 0.82/1.19 Space: 489 KB %------------------------------------------------------------------------------