%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : ROB005-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n020.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 : Mon Jul 18 20:52:15 EDT 2022 % Result : Unsatisfiable 3.48s 3.85s % Output : CNFRefutation 3.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : ROB005-1 : TPTP v8.1.0. Released v1.0.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 14:37:36 EDT 2022 % 0.12/0.33 % CPUTime : % 3.48/3.85 Theorem Proved. % 3.48/3.85 % SZS status Unsatisfiable % 3.48/3.85 % SZS output start CNFRefutation % 3.48/3.85 [1=axiom,[], % 3.48/3.85 add(c,c) = c]. % 3.48/3.85 [2=axiom,[], % 3.48/3.85 negate(add(negate(add(X10,X11)),negate(add(X10,negate(X11))))) = X10]. % 3.48/3.85 [3=axiom,[], % 3.48/3.85 add(add(X10,X11),X12) = add(X10,add(X11,X12))]. % 3.48/3.85 [4=axiom,[], % 3.48/3.85 add(X10,X11) = add(X11,X10)]. % 3.48/3.85 [5=axiom,[], % 3.48/3.85 thtop(X10,X10) = thmfalse]. % 3.48/3.85 [6=axiom,[4], % 3.48/3.85 thtop(add(negate(add(a,negate(b))),negate(add(negate(b),negate(a)))),b) = thmtrue]. % 3.48/3.85 [7=param(3,1),[], % 3.48/3.85 add(c,add(c,X10)) = add(c,X10)]. % 3.48/3.85 [8=param(3,4),[], % 3.48/3.85 add(X10,add(X11,X12)) = add(X12,add(X10,X11))]. % 3.48/3.85 [9=param(3,4),[3], % 3.48/3.85 add(X10,add(X11,X12)) = add(X11,add(X10,X12))]. % 3.48/3.85 [10=param(2,1),[], % 3.48/3.85 negate(add(negate(c),negate(add(c,negate(c))))) = c]. % 3.48/3.85 [11=param(2,4),[], % 3.48/3.85 negate(add(negate(add(X10,X11)),negate(add(X11,negate(X10))))) = X11]. % 3.48/3.85 [12=param(2,4),[], % 3.48/3.85 negate(add(negate(add(X10,X11)),negate(add(negate(X11),X10)))) = X10]. % 3.48/3.85 [14=param(7,4),[3], % 3.48/3.85 add(c,add(X10,c)) = add(c,X10)]. % 3.48/3.85 [17=param(3,14),[3,3], % 3.48/3.85 add(c,add(X10,add(c,X11))) = add(c,add(X10,X11))]. % 3.48/3.85 [18=param(8,3),[3], % 3.48/3.85 add(X10,add(X11,add(X12,X13))) = add(X11,add(X12,add(X13,X10)))]. % 3.48/3.85 [19=param(3,8),[3,3,3], % 3.48/3.85 add(X10,add(X11,add(X12,X13))) = add(X11,add(X12,add(X10,X13)))]. % 3.48/3.85 [20=param(7,8),[17], % 3.48/3.85 add(c,add(X10,X11)) = add(c,add(X11,X10))]. % 3.48/3.85 [21=param(8,8),[3], % 3.48/3.85 add(X10,add(X11,add(X12,X13))) = add(X13,add(X11,add(X10,X12)))]. % 3.48/3.85 [25=param(9,4),[3], % 3.48/3.85 add(X10,add(X11,X12)) = add(X10,add(X12,X11))]. % 3.48/3.85 [26=param(9,8),[], % 3.48/3.85 add(X10,add(X11,X12)) = add(X12,add(X11,X10))]. % 3.48/3.85 [34=param(11,4),[], % 3.48/3.85 negate(add(negate(add(X10,X11)),negate(add(negate(X10),X11)))) = X11]. % 3.48/3.85 [35=param(11,10),[3,4], % 3.48/3.85 negate(add(c,negate(add(c,add(negate(c),negate(c)))))) = negate(c)]. % 3.48/3.85 [42=param(12,4),[], % 3.48/3.85 negate(add(negate(add(negate(X10),X11)),negate(add(X11,X10)))) = X11]. % 3.48/3.85 [45=param(2,35),[7,4], % 3.48/3.85 negate(add(negate(c),negate(add(c,add(negate(c),negate(c)))))) = c]. % 3.48/3.85 [48=param(17,3),[3], % 3.48/3.85 add(c,add(X10,add(X11,add(c,X12)))) = add(c,add(X10,add(X11,X12)))]. % 3.48/3.85 [53=param(2,9),[], % 3.48/3.85 negate(add(negate(add(X10,add(X11,X12))),negate(add(X11,negate(add(X10,X12)))))) = X11]. % 3.48/3.85 [54=param(2,26),[], % 3.48/3.85 negate(add(negate(add(X10,add(X11,X12))),negate(add(X12,negate(add(X11,X10)))))) = X12]. % 3.48/3.85 [56=param(11,7),[3], % 3.48/3.85 negate(add(negate(add(c,X10)),negate(add(c,add(X10,negate(c)))))) = add(c,X10)]. % 3.48/3.85 [65=param(34,7),[], % 3.48/3.85 negate(add(negate(add(c,X10)),negate(add(negate(c),add(c,X10))))) = add(c,X10)]. % 3.48/3.85 [67=param(11,35),[4,45,4], % 3.48/3.85 negate(add(c,add(negate(c),negate(c)))) = negate(add(c,negate(c)))]. % 3.48/3.85 [68=demod(35),[67], % 3.48/3.85 negate(add(c,negate(add(c,negate(c))))) = negate(c)]. % 3.48/3.85 [92=param(2,10),[4], % 3.48/3.85 negate(add(negate(add(X10,c)),negate(add(X10,add(negate(c),negate(add(c,negate(c)))))))) = X10]. % 3.48/3.85 [145=param(25,48),[3,3,3,14], % 3.48/3.85 add(X10,add(c,add(X11,add(X12,X13)))) = add(X10,add(X11,add(X12,add(c,X13))))]. % 3.48/3.85 [250=param(92,1),[], % 3.48/3.85 negate(add(negate(c),negate(add(c,add(negate(c),negate(add(c,negate(c)))))))) = c]. % 3.48/3.85 [254=param(250,4),[3,4], % 3.48/3.85 negate(add(negate(c),negate(add(negate(c),add(c,negate(add(c,negate(c)))))))) = c]. % 3.48/3.85 [387=demod(65),[], % 3.48/3.85 negate(add(negate(add(c,X10)),negate(add(negate(c),add(c,X10))))) = add(c,X10)]. % 3.48/3.85 [391=demod(254),[], % 3.48/3.85 negate(add(negate(c),negate(add(negate(c),add(c,negate(add(c,negate(c)))))))) = c]. % 3.48/3.85 [599=param(387,68),[391], % 3.48/3.85 add(c,negate(add(c,negate(c)))) = c]. % 3.48/3.85 [601=param(9,599),[], % 3.48/3.85 add(c,add(X10,negate(add(c,negate(c))))) = add(X10,c)]. % 3.48/3.85 [612=param(11,601),[3,4,92], % 3.48/3.85 add(X10,negate(add(c,negate(c)))) = X10]. % 3.48/3.85 [617=param(612,4),[], % 3.48/3.85 add(negate(add(c,negate(c))),X10) = X10]. % 3.48/3.85 [619=param(11,612),[617], % 3.48/3.85 negate(add(negate(X10),negate(negate(X10)))) = negate(add(c,negate(c)))]. % 3.48/3.85 [631=param(619,2),[2], % 3.48/3.85 negate(add(X10,negate(X10))) = negate(add(c,negate(c)))]. % 3.48/3.85 [633=param(2,631),[617], % 3.48/3.85 negate(negate(add(X10,negate(negate(X10))))) = X10]. % 3.48/3.85 [634=param(2,631),[612], % 3.48/3.85 negate(negate(add(X10,X10))) = X10]. % 3.48/3.85 [640=param(12,631),[4,612,633], % 3.48/3.85 negate(negate(X10)) = X10]. % 3.48/3.85 [642=demod(634),[640], % 3.48/3.85 add(X10,X10) = X10]. % 3.48/3.85 [654=param(53,631),[3,642,612,640], % 3.48/3.85 add(X10,add(X10,X11)) = add(X10,X11)]. % 3.48/3.85 [656=param(54,631),[654,612,640], % 3.48/3.85 add(X10,add(X11,X10)) = add(X11,X10)]. % 3.48/3.85 [682=param(56,631),[642,612,640], % 3.48/3.85 add(X10,negate(X10)) = add(c,negate(c))]. % 3.48/3.85 [684=param(617,631),[], % 3.48/3.85 add(negate(add(X10,negate(X10))),X11) = X11]. % 3.48/3.85 [699=param(640,11),[], % 3.48/3.85 add(negate(add(X11,X10)),negate(add(X10,negate(X11)))) = negate(X10)]. % 3.48/3.85 [704=param(640,42),[], % 3.48/3.85 add(negate(add(negate(X11),X10)),negate(add(X10,X11))) = negate(X10)]. % 3.48/3.85 [719=param(656,18),[3,3,654], % 3.48/3.85 add(X10,add(X11,add(X12,add(X13,add(X10,X11))))) = add(X13,add(X10,add(X11,X12)))]. % 3.48/3.85 [722=param(19,656),[], % 3.48/3.85 add(X13,add(X10,add(X11,add(X12,X13)))) = add(X10,add(X11,add(X12,X13)))]. % 3.48/3.85 [724=demod(719),[722], % 3.48/3.85 add(X10,add(X11,add(X12,add(X10,X13)))) = add(X12,add(X10,add(X13,X11)))]. % 3.48/3.85 [746=param(3,682),[3], % 3.48/3.85 add(c,add(negate(c),X10)) = add(X11,add(negate(X11),X10))]. % 3.48/3.85 [751=param(20,682),[654,4], % 3.48/3.85 add(c,add(X10,negate(X10))) = add(c,negate(c))]. % 3.48/3.85 [801=param(656,682),[], % 3.48/3.85 add(negate(c),add(X10,negate(X10))) = add(c,negate(c))]. % 3.48/3.85 [802=param(3,751),[3,3], % 3.48/3.85 add(c,add(negate(c),X10)) = add(c,add(X11,add(negate(X11),X10)))]. % 3.48/3.85 [810=param(21,751),[-724,-145,654], % 3.48/3.85 add(X10,add(c,negate(c))) = add(c,add(X11,add(negate(X11),X10)))]. % 3.48/3.85 [845=param(801,26),[], % 3.48/3.85 add(negate(X10),add(X10,negate(c))) = add(c,negate(c))]. % 3.48/3.85 [871=param(656,845),[3,656,845], % 3.48/3.85 add(X10,add(c,negate(c))) = add(c,negate(c))]. % 3.48/3.85 [896=demod(810),[871], % 3.48/3.85 add(c,add(X10,add(negate(X10),X11))) = add(c,negate(c))]. % 3.48/3.85 [897=demod(802),[896], % 3.48/3.85 add(c,add(negate(c),X10)) = add(c,negate(c))]. % 3.48/3.85 [902=demod(746),[897], % 3.48/3.85 add(X10,add(negate(X10),X11)) = add(c,negate(c))]. % 3.48/3.85 [1182=param(704,902),[640,3,656,684,640], % 3.48/3.85 negate(add(X10,X11)) = negate(add(X11,X10))]. % 3.48/3.85 [1192=param(6,1182),[4,699,640,5], % 3.48/3.85 thmtrue = thmfalse]. % 3.48/3.85 % SZS output end CNFRefutation % 3.48/3.85 Space: 16614 KB %------------------------------------------------------------------------------