%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : ALG005-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n023.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 16:54:00 EDT 2022 % Result : Unsatisfiable 1.00s 1.38s % Output : CNFRefutation 1.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : ALG005-1 : TPTP v8.1.0. Released v2.2.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.11/0.33 % Computer : n023.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Wed Jun 8 11:24:38 EDT 2022 % 0.11/0.33 % CPUTime : % 1.00/1.38 Theorem Proved. % 1.00/1.38 % SZS status Unsatisfiable % 1.00/1.38 % SZS output start CNFRefutation % 1.00/1.38 [1=axiom,[], % 1.00/1.38 difference(X10,difference(X10,X11)) = multiply(X10,X11)]. % 1.00/1.38 [2=axiom,[], % 1.00/1.38 difference(difference(X10,X11),X12) = difference(difference(X10,X12),difference(X11,X12))]. % 1.00/1.38 [3=axiom,[1,1], % 1.00/1.38 multiply(X10,X11) = multiply(X11,X10)]. % 1.00/1.38 [4=axiom,[], % 1.00/1.38 difference(X10,difference(X11,X10)) = X10]. % 1.00/1.38 [5=axiom,[], % 1.00/1.38 thtop(X10,X10) = thmfalse]. % 1.00/1.38 [6=axiom,[3,3,3], % 1.00/1.38 thtop(multiply(c,multiply(b,a)),multiply(a,multiply(c,b))) = thmtrue]. % 1.00/1.38 [7=param(4,4),[], % 1.00/1.38 difference(difference(X10,X11),X11) = difference(X10,X11)]. % 1.00/1.38 [8=param(1,1),[], % 1.00/1.38 difference(X10,multiply(X10,X11)) = multiply(X10,difference(X10,X11))]. % 1.00/1.38 [9=param(1,4),[], % 1.00/1.38 multiply(X10,X10) = X10]. % 1.00/1.38 [10=param(1,4),[], % 1.00/1.38 difference(X10,X10) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [11=param(4,1),[], % 1.00/1.38 difference(difference(X10,X11),multiply(X10,X11)) = difference(X10,X11)]. % 1.00/1.38 [12=param(1,7),[3], % 1.00/1.38 difference(difference(X10,X11),difference(X10,X11)) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [13=param(8,3),[], % 1.00/1.38 difference(X10,multiply(X11,X10)) = multiply(X10,difference(X10,X11))]. % 1.00/1.38 [15=param(2,1),[], % 1.00/1.38 difference(difference(X10,X12),difference(difference(X10,X11),X12)) = difference(multiply(X10,X11),X12)]. % 1.00/1.38 [16=param(2,4),[], % 1.00/1.38 difference(difference(X10,X11),difference(difference(X12,X10),X11)) = difference(X10,X11)]. % 1.00/1.38 [18=param(2,7),[], % 1.00/1.38 difference(difference(difference(X10,X11),X12),difference(X11,X12)) = difference(difference(X10,X11),X12)]. % 1.00/1.38 [19=param(2,1),[1,3], % 1.00/1.38 difference(multiply(X10,X11),X11) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [20=param(1,2),[15], % 1.00/1.38 difference(multiply(X10,X11),X12) = multiply(difference(X10,X12),difference(X11,X12))]. % 1.00/1.38 [22=demod(15),[20], % 1.00/1.38 difference(difference(X10,X11),difference(difference(X10,X12),X11)) = multiply(difference(X10,X11),difference(X12,X11))]. % 1.00/1.38 [23=demod(19),[20], % 1.00/1.38 multiply(difference(X10,X11),difference(X11,X11)) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [25=param(2,7),[], % 1.00/1.38 difference(difference(difference(X10,X11),X12),X11) = difference(difference(X10,X11),difference(X12,X11))]. % 1.00/1.38 [26=param(1,13),[8,1], % 1.00/1.38 multiply(X10,multiply(X10,X11)) = multiply(X10,multiply(X11,X10))]. % 1.00/1.38 [27=param(10,2),[1,4,20,23], % 1.00/1.38 multiply(difference(X10,X11),difference(X12,difference(X10,X11))) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [28=param(2,10),[20,12], % 1.00/1.38 multiply(difference(X10,X11),difference(difference(X12,X10),X11)) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [29=param(10,2),[27], % 1.00/1.38 difference(difference(X11,X11),X10) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [30=param(2,10),[20,4], % 1.00/1.38 multiply(X10,difference(difference(X11,X10),difference(X12,X10))) = difference(difference(X10,X12),X10)]. % 1.00/1.38 [31=param(2,10),[7], % 1.00/1.38 difference(difference(X10,X11),multiply(X11,difference(X12,X11))) = difference(X10,X11)]. % 1.00/1.38 [34=param(4,11),[20,1,4,3], % 1.00/1.38 multiply(X10,multiply(X11,X10)) = multiply(X11,X10)]. % 1.00/1.38 [35=demod(26),[34], % 1.00/1.38 multiply(X10,multiply(X10,X11)) = multiply(X11,X10)]. % 1.00/1.38 [38=param(2,29),[20,28,29,20,4], % 1.00/1.38 multiply(X10,difference(difference(X12,X10),difference(X11,X10))) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [39=demod(30),[38], % 1.00/1.38 difference(difference(X10,X11),X10) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [40=param(2,29),[31], % 1.00/1.38 difference(difference(X10,difference(X12,X12)),X11) = difference(X10,X11)]. % 1.00/1.38 [43=param(1,39),[3], % 1.00/1.38 difference(difference(X10,X11),multiply(X10,difference(X11,X10))) = multiply(X10,difference(X10,X11))]. % 1.00/1.38 [44=param(2,39),[20,28], % 1.00/1.38 difference(difference(difference(X11,X12),X10),difference(X11,X10)) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [48=param(34,35),[], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X11,X10)) = multiply(X10,multiply(X10,X11))]. % 1.00/1.38 [50=param(35,3),[], % 1.00/1.38 multiply(X10,multiply(X10,X11)) = multiply(X10,X11)]. % 1.00/1.38 [51=demod(48),[50], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X11,X10)) = multiply(X10,X11)]. % 1.00/1.38 [62=param(40,10),[1,27,27,-10], % 1.00/1.38 multiply(X10,difference(X11,X11)) = difference(X11,X11)]. % 1.00/1.38 [64=param(62,3),[], % 1.00/1.38 multiply(difference(X10,X10),X11) = difference(X10,X10)]. % 1.00/1.38 [69=param(64,62),[], % 1.00/1.38 difference(X10,X10) = difference(X11,X11)]. % 1.00/1.38 [70=param(1,69),[9], % 1.00/1.38 difference(X10,difference(X11,X11)) = X10]. % 1.00/1.38 [75=param(70,2),[29], % 1.00/1.38 difference(X10,multiply(X11,difference(X12,X11))) = X10]. % 1.00/1.38 [76=demod(43),[75], % 1.00/1.38 multiply(X10,difference(X10,X11)) = difference(X10,X11)]. % 1.00/1.38 [77=demod(13),[76], % 1.00/1.38 difference(X10,multiply(X11,X10)) = difference(X10,X11)]. % 1.00/1.38 [78=demod(8),[76], % 1.00/1.38 difference(X10,multiply(X10,X11)) = difference(X10,X11)]. % 1.00/1.38 [82=param(16,78),[78], % 1.00/1.38 difference(difference(X10,X11),difference(difference(X12,X10),multiply(X10,X11))) = difference(X10,X11)]. % 1.00/1.38 [83=param(22,11),[78,12,78,77], % 1.00/1.38 multiply(difference(X11,X10),difference(X10,X11)) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [119=param(75,82),[3], % 1.00/1.38 difference(X10,multiply(difference(X11,X12),difference(difference(X13,X11),multiply(X11,X12)))) = X10]. % 1.00/1.38 [122=param(119,1),[76], % 1.00/1.38 difference(X10,multiply(multiply(X11,X12),difference(difference(X13,X11),difference(X11,X12)))) = X10]. % 1.00/1.38 [123=param(122,3),[], % 1.00/1.38 difference(X10,multiply(multiply(X11,X12),difference(difference(X13,X12),difference(X12,X11)))) = X10]. % 1.00/1.38 [125=param(123,51),[20,77,78,83,75], % 1.00/1.38 difference(X10,multiply(multiply(X11,X12),difference(X13,multiply(X12,X11)))) = X10]. % 1.00/1.38 [133=param(125,77),[], % 1.00/1.38 difference(difference(X10,multiply(X11,X12)),multiply(X12,X11)) = difference(X10,multiply(X11,X12))]. % 1.00/1.38 [134=param(133,2),[20,77,78,83,75], % 1.00/1.38 difference(X10,multiply(X11,X12)) = difference(X10,multiply(X12,X11))]. % 1.00/1.38 [135=param(1,134),[1], % 1.00/1.38 multiply(X10,multiply(X11,X12)) = multiply(X10,multiply(X12,X11))]. % 1.00/1.38 [136=param(135,3),[], % 1.00/1.38 multiply(X10,multiply(X11,X12)) = multiply(multiply(X12,X11),X10)]. % 1.00/1.38 [138=param(136,3),[], % 1.00/1.38 multiply(multiply(X10,X11),X12) = multiply(multiply(X11,X10),X12)]. % 1.00/1.38 [143=param(136,135),[], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X12,X13)) = multiply(multiply(X13,X12),multiply(X11,X10))]. % 1.00/1.38 [147=param(1,2),[], % 1.00/1.38 difference(difference(X10,X11),difference(difference(X10,X12),difference(X11,X12))) = multiply(difference(X10,X11),X12)]. % 1.00/1.38 [148=param(2,1),[2,11], % 1.00/1.38 difference(difference(X10,multiply(X11,X12)),difference(X11,X12)) = difference(difference(X10,X11),difference(X11,X12))]. % 1.00/1.38 [150=param(2,78),[148], % 1.00/1.38 difference(difference(X10,X11),difference(X11,X12)) = difference(difference(X10,X11),multiply(X11,X12))]. % 1.00/1.38 [151=demod(148),[150], % 1.00/1.38 difference(difference(X10,multiply(X11,X12)),difference(X11,X12)) = difference(difference(X10,X11),multiply(X11,X12))]. % 1.00/1.38 [156=param(2,12),[20,4,3,39,27], % 1.00/1.38 multiply(difference(X10,X11),difference(X11,difference(X12,difference(X10,X11)))) = multiply(X11,difference(X10,X11))]. % 1.00/1.38 [157=param(16,1),[2,11,151,4], % 1.00/1.38 difference(X10,difference(difference(X11,X10),X12)) = difference(X10,multiply(difference(X11,X10),X12))]. % 1.00/1.38 [169=param(51,136),[], % 1.00/1.38 multiply(multiply(multiply(X10,X11),X12),multiply(multiply(X11,X10),X12)) = multiply(multiply(X10,X11),X12)]. % 1.00/1.38 [174=param(2,44),[20,4,3,156], % 1.00/1.38 difference(difference(difference(difference(X11,X12),X10),X13),difference(X11,X10)) = multiply(X10,difference(X11,X10))]. % 1.00/1.38 [244=param(157,174),[75,3], % 1.00/1.38 difference(X10,multiply(difference(X11,X12),difference(difference(difference(X11,X13),X12),X10))) = X10]. % 1.00/1.38 [247=param(244,25),[], % 1.00/1.38 difference(X10,multiply(difference(X11,X12),difference(difference(X11,X10),difference(X12,X10)))) = X10]. % 1.00/1.38 [252=param(247,39),[75,3], % 1.00/1.38 difference(X10,multiply(difference(X11,X10),difference(X11,difference(X10,X12)))) = X10]. % 1.00/1.38 [257=param(4,252),[20,7,2,39,75,9], % 1.00/1.38 multiply(difference(X10,X11),difference(X10,difference(X11,X12))) = difference(X10,X11)]. % 1.00/1.38 [276=param(257,18),[25,3,257,25], % 1.00/1.38 difference(difference(X10,X11),difference(X12,X11)) = difference(difference(X10,X11),X12)]. % 1.00/1.38 [277=demod(22),[276], % 1.00/1.38 difference(difference(X10,X11),difference(X10,X12)) = multiply(difference(X10,X11),difference(X12,X11))]. % 1.00/1.38 [280=demod(147),[276,276], % 1.00/1.38 difference(difference(X10,X11),difference(X10,X12)) = multiply(difference(X10,X11),X12)]. % 1.00/1.38 [281=demod(277),[280], % 1.00/1.38 multiply(difference(X10,X11),difference(X12,X11)) = multiply(difference(X10,X11),X12)]. % 1.00/1.38 [283=demod(20),[281], % 1.00/1.38 difference(multiply(X10,X11),X12) = multiply(difference(X10,X12),X11)]. % 1.00/1.38 [348=param(283,50),[283], % 1.00/1.38 multiply(difference(X10,X11),multiply(X10,X12)) = multiply(difference(X10,X11),X12)]. % 1.00/1.38 [512=param(348,1),[1], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X10,X12)) = multiply(multiply(X10,X11),X12)]. % 1.00/1.38 [515=param(348,135),[], % 1.00/1.38 multiply(difference(X10,X11),multiply(X12,X10)) = multiply(difference(X10,X11),X12)]. % 1.00/1.38 [518=param(515,1),[1], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X12,X10)) = multiply(multiply(X10,X11),X12)]. % 1.00/1.38 [530=param(169,76),[283,518,283,143,515,518,3,34,283,518], % 1.00/1.38 multiply(multiply(X10,X11),difference(X11,X12)) = multiply(X10,difference(X11,X12))]. % 1.00/1.38 [531=param(530,1),[1], % 1.00/1.38 multiply(multiply(X10,X11),multiply(X11,X12)) = multiply(X10,multiply(X11,X12))]. % 1.00/1.38 [535=param(531,3),[512], % 1.00/1.38 multiply(multiply(X10,X11),X12) = multiply(X11,multiply(X10,X12))]. % 1.00/1.38 [595=demod(138),[535,535], % 1.00/1.38 multiply(X10,multiply(X11,X12)) = multiply(X11,multiply(X10,X12))]. % 1.00/1.38 [690=param(6,595),[3,5], % 1.00/1.38 thmtrue = thmfalse]. % 1.00/1.38 % SZS output end CNFRefutation % 1.00/1.38 Space: 1832 KB %------------------------------------------------------------------------------