%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO007-4 : TPTP v8.1.0. Released v1.1.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n022.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:46 EDT 2022 % Result : Unsatisfiable 1.29s 1.70s % Output : CNFRefutation 1.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : BOO007-4 : TPTP v8.1.0. Released v1.1.0. % 0.13/0.14 % Command : fiesta-wrapper %s % 0.14/0.35 % Computer : n022.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 : Wed Jun 1 17:49:22 EDT 2022 % 0.14/0.35 % CPUTime : % 1.29/1.70 Theorem Proved. % 1.29/1.70 % SZS status Unsatisfiable % 1.29/1.70 % SZS output start CNFRefutation % 1.29/1.70 [1=axiom,[], % 1.29/1.70 multiply(X10,inverse(X10)) = additive_identity]. % 1.29/1.70 [2=axiom,[], % 1.29/1.70 add(X10,inverse(X10)) = multiplicative_identity]. % 1.29/1.70 [3=axiom,[], % 1.29/1.70 multiply(X10,multiplicative_identity) = X10]. % 1.29/1.70 [4=axiom,[], % 1.29/1.70 add(X10,additive_identity) = X10]. % 1.29/1.70 [5=axiom,[], % 1.29/1.70 add(multiply(X10,X11),multiply(X10,X12)) = multiply(X10,add(X11,X12))]. % 1.29/1.70 [6=axiom,[], % 1.29/1.70 add(X10,multiply(X11,X12)) = multiply(add(X10,X11),add(X10,X12))]. % 1.29/1.70 [7=demod(5),[6], % 1.29/1.70 multiply(add(multiply(X10,X11),X10),add(multiply(X10,X11),X12)) = multiply(X10,add(X11,X12))]. % 1.29/1.70 [8=axiom,[], % 1.29/1.70 multiply(X10,X11) = multiply(X11,X10)]. % 1.29/1.70 [9=axiom,[], % 1.29/1.70 add(X10,X11) = add(X11,X10)]. % 1.29/1.70 [10=demod(7),[9,6], % 1.29/1.70 multiply(multiply(add(X10,X10),add(X10,X11)),add(multiply(X10,X11),X12)) = multiply(X10,add(X11,X12))]. % 1.29/1.70 [11=axiom,[], % 1.29/1.70 thtop(X10,X10) = thmfalse]. % 1.29/1.70 [12=axiom,[8,8,8], % 1.29/1.70 thtop(multiply(a,multiply(c,b)),multiply(c,multiply(b,a))) = thmtrue]. % 1.29/1.70 [13=param(9,4),[], % 1.29/1.70 add(additive_identity,X10) = X10]. % 1.29/1.70 [14=param(13,2),[], % 1.29/1.70 inverse(additive_identity) = multiplicative_identity]. % 1.29/1.70 [15=param(6,1),[4], % 1.29/1.70 multiply(add(X10,X11),add(X10,inverse(X11))) = X10]. % 1.29/1.70 [16=param(6,3),[], % 1.29/1.70 multiply(add(X10,X11),add(X10,multiplicative_identity)) = add(X10,X11)]. % 1.29/1.70 [17=param(6,9),[], % 1.29/1.70 multiply(add(X10,X11),add(X10,X12)) = add(multiply(X11,X12),X10)]. % 1.29/1.70 [18=param(8,3),[], % 1.29/1.70 multiply(multiplicative_identity,X10) = X10]. % 1.29/1.70 [19=param(10,1),[2,3,13], % 1.29/1.70 multiply(X10,add(inverse(X10),X11)) = multiply(add(X10,X10),X11)]. % 1.29/1.70 [20=param(10,3),[16], % 1.29/1.70 multiply(add(X10,X10),add(X10,X11)) = multiply(X10,add(multiplicative_identity,X11))]. % 1.29/1.70 [27=param(15,2),[18], % 1.29/1.70 add(X10,inverse(inverse(X10))) = X10]. % 1.29/1.70 [28=param(15,2),[3], % 1.29/1.70 add(X10,X10) = X10]. % 1.29/1.70 [31=demod(20),[28], % 1.29/1.70 multiply(X10,add(X10,X11)) = multiply(X10,add(multiplicative_identity,X11))]. % 1.29/1.70 [33=demod(19),[28], % 1.29/1.70 multiply(X10,add(inverse(X10),X11)) = multiply(X10,X11)]. % 1.29/1.70 [34=demod(10),[28], % 1.29/1.70 multiply(multiply(X10,add(X10,X11)),add(multiply(X10,X11),X12)) = multiply(X10,add(X11,X12))]. % 1.29/1.70 [36=param(15,9),[], % 1.29/1.70 multiply(add(X10,X11),add(X11,inverse(X10))) = X11]. % 1.29/1.70 [37=param(15,9),[], % 1.29/1.70 multiply(add(X10,X11),add(inverse(X11),X10)) = X10]. % 1.29/1.70 [41=param(16,2),[18,2], % 1.29/1.70 add(X10,multiplicative_identity) = multiplicative_identity]. % 1.29/1.70 [42=param(41,9),[], % 1.29/1.70 add(multiplicative_identity,X10) = multiplicative_identity]. % 1.29/1.70 [44=demod(31),[42,3], % 1.29/1.70 multiply(X10,add(X10,X11)) = X10]. % 1.29/1.70 [45=demod(34),[44], % 1.29/1.70 multiply(X10,add(multiply(X10,X11),X12)) = multiply(X10,add(X11,X12))]. % 1.29/1.70 [51=param(17,9),[], % 1.29/1.70 multiply(add(X10,X11),add(X11,X12)) = add(multiply(X10,X12),X11)]. % 1.29/1.70 [53=param(17,2),[9,9], % 1.29/1.70 multiply(add(X10,inverse(multiply(X10,X11))),add(X11,inverse(multiply(X10,X11)))) = multiplicative_identity]. % 1.29/1.70 [59=param(6,44),[], % 1.29/1.70 multiply(add(X10,X11),add(X10,add(X11,X12))) = add(X10,X11)]. % 1.29/1.70 [60=param(44,9),[], % 1.29/1.70 multiply(X10,add(X11,X10)) = X10]. % 1.29/1.70 [61=param(44,17),[], % 1.29/1.70 multiply(multiply(X10,X11),multiply(add(X12,X10),add(X12,X11))) = multiply(X10,X11)]. % 1.29/1.70 [68=param(36,27),[9,2,3], % 1.29/1.70 inverse(inverse(X10)) = X10]. % 1.29/1.70 [69=param(6,60),[], % 1.29/1.70 multiply(add(X10,X11),add(X10,add(X12,X11))) = add(X10,X11)]. % 1.29/1.70 [73=param(45,9),[6], % 1.29/1.70 multiply(X10,multiply(add(X11,X10),add(X11,X12))) = multiply(X10,add(X12,X11))]. % 1.29/1.70 [95=param(51,9),[], % 1.29/1.70 add(multiply(X10,X12),X11) = multiply(add(X10,X11),add(X12,X11))]. % 1.29/1.70 [101=demod(45),[95], % 1.29/1.70 multiply(X10,multiply(add(X10,X11),add(X12,X11))) = multiply(X10,add(X12,X11))]. % 1.29/1.70 [104=param(44,95),[], % 1.29/1.70 multiply(multiply(X10,X11),multiply(add(X10,X12),add(X11,X12))) = multiply(X10,X11)]. % 1.29/1.70 [119=param(59,2),[18,2], % 1.29/1.70 add(X10,add(inverse(X10),X11)) = multiplicative_identity]. % 1.29/1.70 [122=param(59,28),[9,8,60,9], % 1.29/1.70 add(X10,add(X10,X11)) = add(X10,X11)]. % 1.29/1.70 [123=param(15,119),[18], % 1.29/1.70 add(X10,inverse(add(inverse(X10),X11))) = X10]. % 1.29/1.70 [124=param(59,119),[18,119], % 1.29/1.70 add(X10,add(add(inverse(X10),X11),X12)) = multiplicative_identity]. % 1.29/1.70 [129=param(61,28),[8,44,8], % 1.29/1.70 multiply(X10,multiply(X11,X10)) = multiply(X11,X10)]. % 1.29/1.70 [134=param(69,2),[18,2], % 1.29/1.70 add(X10,add(X11,inverse(X10))) = multiplicative_identity]. % 1.29/1.70 [138=param(69,119),[18,119], % 1.29/1.70 add(X10,add(X11,add(inverse(X10),X12))) = multiplicative_identity]. % 1.29/1.70 [140=param(15,134),[18], % 1.29/1.70 add(X10,inverse(add(X11,inverse(X10)))) = X10]. % 1.29/1.70 [145=param(73,9),[], % 1.29/1.70 multiply(X10,multiply(add(X11,X10),add(X12,X11))) = multiply(X10,add(X12,X11))]. % 1.29/1.70 [154=param(33,140),[1,68], % 1.29/1.70 multiply(X10,inverse(add(X11,X10))) = additive_identity]. % 1.29/1.70 [155=param(36,140),[9,33], % 1.29/1.70 multiply(X10,inverse(add(X11,inverse(X10)))) = inverse(add(X11,inverse(X10)))]. % 1.29/1.70 [161=param(154,6),[], % 1.29/1.70 multiply(multiply(X10,X11),inverse(multiply(add(X12,X10),add(X12,X11)))) = additive_identity]. % 1.29/1.70 [190=param(37,124),[68,9,3,68], % 1.29/1.70 add(X10,add(add(X10,X11),X12)) = add(add(X10,X11),X12)]. % 1.29/1.70 [201=param(190,134),[9], % 1.29/1.70 add(inverse(X10),add(X10,X11)) = multiplicative_identity]. % 1.29/1.70 [202=param(190,138),[], % 1.29/1.70 add(add(X10,X11),add(inverse(X10),X12)) = multiplicative_identity]. % 1.29/1.70 [204=param(201,9),[], % 1.29/1.70 add(inverse(X10),add(X11,X10)) = multiplicative_identity]. % 1.29/1.70 [211=param(15,204),[18], % 1.29/1.70 add(inverse(X10),inverse(add(X11,X10))) = inverse(X10)]. % 1.29/1.70 [368=param(104,122),[60], % 1.29/1.70 multiply(multiply(X10,X11),add(X10,X12)) = multiply(X10,X11)]. % 1.29/1.70 [561=param(145,123),[8,123], % 1.29/1.70 multiply(X10,multiply(X11,add(inverse(add(inverse(X11),X12)),X10))) = multiply(X10,X11)]. % 1.29/1.70 [702=param(161,211),[8,44,68,8], % 1.29/1.70 multiply(X10,multiply(X11,inverse(add(X12,X10)))) = additive_identity]. % 1.29/1.70 [778=param(702,211),[68], % 1.29/1.70 multiply(inverse(add(X10,X11)),multiply(X12,X11)) = additive_identity]. % 1.29/1.70 [786=param(778,8),[], % 1.29/1.70 multiply(multiply(X10,X11),inverse(add(X12,X11))) = additive_identity]. % 1.29/1.70 [787=param(778,8),[], % 1.29/1.70 multiply(inverse(add(X10,X11)),multiply(X11,X12)) = additive_identity]. % 1.29/1.70 [829=param(787,9),[], % 1.29/1.70 multiply(inverse(add(X10,X11)),multiply(X10,X12)) = additive_identity]. % 1.29/1.70 [840=param(829,8),[], % 1.29/1.70 multiply(multiply(X10,X11),inverse(add(X10,X12))) = additive_identity]. % 1.29/1.70 [856=param(840,155),[], % 1.29/1.70 inverse(add(X10,inverse(multiply(X10,X11)))) = additive_identity]. % 1.29/1.70 [857=param(2,856),[4], % 1.29/1.70 add(X10,inverse(multiply(X10,X11))) = multiplicative_identity]. % 1.29/1.70 [858=demod(53),[857,18], % 1.29/1.70 add(X10,inverse(multiply(X11,X10))) = multiplicative_identity]. % 1.29/1.70 [863=param(36,858),[9,18], % 1.29/1.70 add(inverse(X10),inverse(multiply(X11,X10))) = inverse(multiply(X11,X10))]. % 1.29/1.70 [929=param(36,857),[9,18], % 1.29/1.70 add(inverse(X10),inverse(multiply(X10,X11))) = inverse(multiply(X10,X11))]. % 1.29/1.70 [930=param(37,857),[9,3], % 1.29/1.70 add(X10,inverse(multiply(inverse(X10),X11))) = inverse(multiply(inverse(X10),X11))]. % 1.29/1.70 [1160=param(786,9),[], % 1.29/1.70 multiply(multiply(X10,X11),inverse(add(X11,X12))) = additive_identity]. % 1.29/1.70 [1218=param(1160,929),[68], % 1.29/1.70 multiply(multiply(X10,inverse(X11)),multiply(X11,X12)) = additive_identity]. % 1.29/1.70 [1222=param(1218,8),[], % 1.29/1.70 multiply(multiply(X10,inverse(X11)),multiply(X12,X11)) = additive_identity]. % 1.29/1.70 [1485=param(15,930),[68,6,2,18], % 1.29/1.70 multiply(inverse(multiply(inverse(X10),X11)),add(X10,X11)) = X10]. % 1.29/1.70 [1492=param(104,930),[60], % 1.29/1.70 multiply(multiply(X10,X11),inverse(multiply(inverse(X10),X12))) = multiply(X10,X11)]. % 1.29/1.70 [1512=param(1485,9),[], % 1.29/1.70 multiply(inverse(multiply(inverse(X10),X11)),add(X11,X10)) = X10]. % 1.29/1.70 [1517=param(1485,863),[68,8], % 1.29/1.70 multiply(inverse(multiply(X10,X11)),inverse(multiply(X11,inverse(multiply(X10,X11))))) = inverse(X11)]. % 1.29/1.70 [1518=param(1485,929),[68,8], % 1.29/1.70 multiply(inverse(multiply(X10,X11)),inverse(multiply(X10,inverse(multiply(X10,X11))))) = inverse(X10)]. % 1.29/1.70 [1520=param(1512,123),[68,8,33,8], % 1.29/1.70 inverse(add(inverse(X10),X11)) = multiply(X10,inverse(multiply(X10,X11)))]. % 1.29/1.70 [1522=demod(561),[1520,95,101], % 1.29/1.70 multiply(X10,multiply(X11,add(inverse(multiply(X11,X12)),X10))) = multiply(X10,X11)]. % 1.29/1.70 [1532=param(1512,202),[1520,368,3], % 1.29/1.70 add(inverse(X10),X11) = inverse(multiply(X10,inverse(multiply(X10,X11))))]. % 1.29/1.70 [1551=demod(1522),[1532], % 1.29/1.70 multiply(X10,multiply(X11,inverse(multiply(multiply(X11,X12),inverse(multiply(multiply(X11,X12),X10)))))) = multiply(X10,X11)]. % 1.29/1.70 [1685=demod(33),[1532], % 1.29/1.70 multiply(X10,inverse(multiply(X10,inverse(multiply(X10,X11))))) = multiply(X10,X11)]. % 1.29/1.70 [2553=param(1492,8),[], % 1.29/1.70 multiply(inverse(multiply(inverse(X10),X12)),multiply(X10,X11)) = multiply(X10,X11)]. % 1.29/1.70 [2591=param(2553,1517),[68], % 1.29/1.70 multiply(X10,multiply(multiply(X11,X10),X12)) = multiply(multiply(X11,X10),X12)]. % 1.29/1.70 [2594=param(2591,8),[], % 1.29/1.70 multiply(X10,multiply(multiply(X10,X11),X12)) = multiply(multiply(X11,X10),X12)]. % 1.29/1.70 [2595=param(2591,129),[129], % 1.29/1.70 multiply(X10,multiply(X11,multiply(X12,X10))) = multiply(X11,multiply(X12,X10))]. % 1.29/1.70 [2608=param(2595,8),[], % 1.29/1.70 multiply(X10,multiply(X11,multiply(X10,X12))) = multiply(X11,multiply(X12,X10))]. % 1.29/1.70 [2620=param(2553,1518),[68], % 1.29/1.70 multiply(X10,multiply(multiply(X10,X11),X12)) = multiply(multiply(X10,X11),X12)]. % 1.29/1.70 [2621=demod(2594),[2620], % 1.29/1.70 multiply(multiply(X10,X11),X12) = multiply(multiply(X11,X10),X12)]. % 1.29/1.70 [2623=param(2620,129),[129], % 1.29/1.70 multiply(X10,multiply(X11,multiply(X10,X12))) = multiply(X11,multiply(X10,X12))]. % 1.29/1.70 [2624=demod(2608),[2623], % 1.29/1.70 multiply(X10,multiply(X11,X12)) = multiply(X10,multiply(X12,X11))]. % 1.29/1.70 [2639=param(2624,8),[], % 1.29/1.70 multiply(X10,multiply(X11,X12)) = multiply(multiply(X12,X11),X10)]. % 1.29/1.70 [2650=param(1551,18),[18,18,3], % 1.29/1.70 multiply(X10,inverse(multiply(X11,inverse(multiply(X11,X10))))) = X10]. % 1.29/1.70 [2652=param(2650,8),[], % 1.29/1.70 multiply(X10,inverse(multiply(X11,inverse(multiply(X10,X11))))) = X10]. % 1.29/1.70 [2670=param(1222,2652),[], % 1.29/1.70 multiply(X10,multiply(X11,multiply(X12,inverse(multiply(X10,X12))))) = additive_identity]. % 1.29/1.70 [2720=param(1685,8),[], % 1.29/1.70 multiply(X10,inverse(multiply(X10,inverse(multiply(X11,X10))))) = multiply(X10,X11)]. % 1.29/1.70 [2740=param(2670,2620),[], % 1.29/1.70 multiply(multiply(X10,X11),multiply(X12,inverse(multiply(X10,X12)))) = additive_identity]. % 1.29/1.70 [2750=param(2740,2639),[], % 1.29/1.70 multiply(multiply(X10,inverse(multiply(X11,X10))),multiply(X12,X11)) = additive_identity]. % 1.29/1.70 [2755=param(1551,2750),[14,3,2720], % 1.29/1.70 multiply(multiply(X10,X11),multiply(X12,X11)) = multiply(multiply(X10,X11),X12)]. % 1.29/1.70 [2757=param(2755,8),[2755], % 1.29/1.70 multiply(multiply(X10,X11),X12) = multiply(multiply(X12,X11),X10)]. % 1.29/1.70 [2817=param(2757,2639),[], % 1.29/1.70 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 1.29/1.70 [3098=demod(2621),[2817,2817], % 1.29/1.70 multiply(X10,multiply(X11,X12)) = multiply(X11,multiply(X10,X12))]. % 1.29/1.70 [3182=param(12,3098),[8,11], % 1.29/1.70 thmtrue = thmfalse]. % 1.29/1.70 % SZS output end CNFRefutation % 1.29/1.70 Space: 5091 KB %------------------------------------------------------------------------------