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