%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ROB014-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:39:35 PM UTC 2026
% Result : Unsatisfiable 16.64s 2.51s
% Output : Proof 16.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 13
% Syntax : Number of formulae : 167 ( 167 unt; 0 def)
% Number of atoms : 167 ( 166 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 16 ( 16 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 90 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f3,axiom,
multiply(one,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',one_times_x) ).
fof(f3_nnf,plain,
! [X] : multiply(one,X) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] : multiply(one,X) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
multiply(one,X0) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t1,plain,
multiply(one,X1) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t20,plain,
multiply(one,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t9,axiom,
sFlat0 = negate(e),
introduced(definition) ).
cnf(t56,plain,
negate(e) = sFlat0,
inference(orient,[status(thm)],[t9]) ).
cnf(f0,axiom,
add(X,Y) = add(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_add) ).
fof(f0_nnf,plain,
! [X,Y] : add(X,Y) = add(Y,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : add(X,Y) = add(Y,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
add(X0,X1) = add(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,plain,
add(X1,X2) = add(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t22,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
sFlat1 = add(d,negate(e)),
introduced(definition) ).
cnf(t37,plain,
add(d,negate(e)) = sFlat1,
inference(orient,[status(thm)],[t10]) ).
cnf(t6380,plain,
add(d,sFlat0) = sFlat1,
inference(step,[status(thm)],[t37,t56]) ).
cnf(t58,plain,
add(d,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t6380]) ).
cnf(t6384,plain,
add(sFlat0,d) = sFlat1,
inference(step,[status(thm)],[t58,t22]) ).
cnf(t67,plain,
add(sFlat0,d) = sFlat1,
inference(orient,[status(thm)],[t6384]) ).
cnf(t11,axiom,
sFlat2 = negate(add(d,negate(e))),
introduced(definition) ).
cnf(t6373,plain,
sFlat2 = negate(sFlat1),
inference(step,[status(thm)],[t11,t37]) ).
cnf(t49,plain,
negate(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t6373]) ).
cnf(t13,axiom,
sFlat4 = multiply(one,add(d,negate(add(d,negate(e))))),
introduced(definition) ).
cnf(t6381,plain,
sFlat4 = add(d,negate(add(d,negate(e)))),
inference(step,[status(thm)],[t13,t20]) ).
cnf(t6382,plain,
sFlat4 = add(d,negate(add(d,sFlat0))),
inference(step,[status(thm)],[t6381,t56]) ).
cnf(t6383,plain,
sFlat4 = add(d,negate(add(sFlat0,d))),
inference(step,[status(thm)],[t6382,t22]) ).
cnf(t59,plain,
add(d,negate(add(sFlat0,d))) = sFlat4,
inference(orient,[status(thm)],[t6383]) ).
cnf(t6385,plain,
add(d,negate(sFlat1)) = sFlat4,
inference(step,[status(thm)],[t59,t67]) ).
cnf(t6386,plain,
add(d,sFlat2) = sFlat4,
inference(step,[status(thm)],[t6385,t49]) ).
cnf(t70,plain,
add(d,sFlat2) = sFlat4,
inference(rw,[status(thm)],[t6386]) ).
cnf(t6388,plain,
add(sFlat2,d) = sFlat4,
inference(step,[status(thm)],[t70,t22]) ).
cnf(t74,plain,
add(sFlat2,d) = sFlat4,
inference(orient,[status(thm)],[t6388]) ).
cnf(t12,axiom,
sFlat3 = add(d,negate(add(d,negate(e)))),
introduced(definition) ).
cnf(t33,plain,
add(d,negate(add(d,negate(e)))) = sFlat3,
inference(orient,[status(thm)],[t12]) ).
cnf(t6368,plain,
add(d,negate(sFlat1)) = sFlat3,
inference(step,[status(thm)],[t33,t37]) ).
cnf(t41,plain,
add(d,negate(sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t6368]) ).
cnf(t6390,plain,
add(d,sFlat2) = sFlat3,
inference(step,[status(thm)],[t41,t49]) ).
cnf(t6391,plain,
add(sFlat2,d) = sFlat3,
inference(step,[status(thm)],[t6390,t22]) ).
cnf(t6392,plain,
sFlat4 = sFlat3,
inference(step,[status(thm)],[t6391,t74]) ).
cnf(t78,plain,
sFlat4 = sFlat3,
inference(orient,[status(thm)],[t6392]) ).
cnf(t6393,plain,
add(sFlat2,d) = sFlat3,
inference(step,[status(thm)],[t74,t78]) ).
cnf(t79,plain,
add(sFlat2,d) = sFlat3,
inference(orient,[status(thm)],[t6393]) ).
cnf(t14,axiom,
sFlat5 = add(e,multiply(one,add(d,negate(add(d,negate(e)))))),
introduced(definition) ).
cnf(t6369,plain,
sFlat5 = add(e,add(d,negate(add(d,negate(e))))),
inference(step,[status(thm)],[t14,t20]) ).
cnf(t6370,plain,
sFlat5 = add(e,add(d,negate(sFlat1))),
inference(step,[status(thm)],[t6369,t37]) ).
cnf(t42,plain,
add(e,add(d,negate(sFlat1))) = sFlat5,
inference(orient,[status(thm)],[t6370]) ).
cnf(t6375,plain,
add(e,add(d,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t42,t49]) ).
cnf(t52,plain,
add(e,add(d,sFlat2)) = sFlat5,
inference(rw,[status(thm)],[t6375]) ).
cnf(t6400,plain,
add(e,add(sFlat2,d)) = sFlat5,
inference(step,[status(thm)],[t52,t22]) ).
cnf(t6401,plain,
add(e,sFlat3) = sFlat5,
inference(step,[status(thm)],[t6400,t79]) ).
cnf(t6402,plain,
add(sFlat3,e) = sFlat5,
inference(step,[status(thm)],[t6401,t22]) ).
cnf(t90,plain,
add(sFlat3,e) = sFlat5,
inference(orient,[status(thm)],[t6402]) ).
cnf(t15,axiom,
sFlat6 = negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))),
introduced(definition) ).
cnf(t6376,plain,
sFlat6 = negate(add(e,add(d,negate(add(d,negate(e)))))),
inference(step,[status(thm)],[t15,t20]) ).
cnf(t6377,plain,
sFlat6 = negate(add(e,add(d,negate(sFlat1)))),
inference(step,[status(thm)],[t6376,t37]) ).
cnf(t6378,plain,
sFlat6 = negate(add(e,add(d,sFlat2))),
inference(step,[status(thm)],[t6377,t49]) ).
cnf(t6379,plain,
sFlat6 = negate(add(e,add(sFlat2,d))),
inference(step,[status(thm)],[t6378,t22]) ).
cnf(t53,plain,
negate(add(e,add(sFlat2,d))) = sFlat6,
inference(orient,[status(thm)],[t6379]) ).
cnf(t6389,plain,
negate(add(e,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t53,t74]) ).
cnf(t77,plain,
negate(add(e,sFlat4)) = sFlat6,
inference(rw,[status(thm)],[t6389]) ).
cnf(t6396,plain,
negate(add(sFlat4,e)) = sFlat6,
inference(step,[status(thm)],[t77,t22]) ).
cnf(t6397,plain,
negate(add(sFlat3,e)) = sFlat6,
inference(step,[status(thm)],[t6396,t78]) ).
cnf(t84,plain,
negate(add(sFlat3,e)) = sFlat6,
inference(orient,[status(thm)],[t6397]) ).
cnf(t6403,plain,
negate(sFlat5) = sFlat6,
inference(step,[status(thm)],[t84,t90]) ).
cnf(t93,plain,
negate(sFlat5) = sFlat6,
inference(rw,[status(thm)],[t6403]) ).
cnf(t94,plain,
negate(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t93]) ).
cnf(f2,axiom,
negate(add(negate(add(X,Y)),negate(add(X,negate(Y))))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',robbins_axiom) ).
fof(f2_nnf,plain,
! [X,Y] : negate(add(negate(add(X,Y)),negate(add(X,negate(Y))))) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : negate(add(negate(add(X,Y)),negate(add(X,negate(Y))))) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
negate(add(negate(add(X0,X1)),negate(add(X0,negate(X1))))) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t7,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t16,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t57,plain,
X1 = negate(add(negate(add(X1,e)),negate(add(X1,sFlat0)))),
inference(cp,[status(thm)],[t16,t56]) ).
cnf(t6470,plain,
X1 = negate(add(negate(add(X1,sFlat0)),negate(add(X1,e)))),
inference(step,[status(thm)],[t57,t22]) ).
cnf(t1301,plain,
negate(add(negate(add(X1,sFlat0)),negate(add(X1,e)))) = X1,
inference(orient,[status(thm)],[t6470]) ).
cnf(t1305,plain,
X1 = negate(add(negate(add(sFlat0,X1)),negate(add(X1,e)))),
inference(cp,[status(thm)],[t1301,t22]) ).
cnf(t1517,plain,
negate(add(negate(add(sFlat0,X1)),negate(add(X1,e)))) = X1,
inference(orient,[status(thm)],[t1305]) ).
cnf(t1525,plain,
d = negate(add(negate(sFlat1),negate(add(d,e)))),
inference(cp,[status(thm)],[t1517,t67]) ).
cnf(t6482,plain,
d = negate(add(sFlat2,negate(add(d,e)))),
inference(step,[status(thm)],[t1525,t49]) ).
cnf(t6483,plain,
d = negate(add(sFlat2,negate(add(e,d)))),
inference(step,[status(thm)],[t6482,t22]) ).
cnf(t1556,plain,
negate(add(sFlat2,negate(add(e,d)))) = d,
inference(orient,[status(thm)],[t6483]) ).
cnf(t1559,plain,
sFlat2 = negate(add(negate(add(sFlat2,add(e,d))),d)),
inference(cp,[status(thm)],[t16,t1556]) ).
cnf(t6484,plain,
sFlat2 = negate(add(d,negate(add(sFlat2,add(e,d))))),
inference(step,[status(thm)],[t1559,t22]) ).
cnf(f1,axiom,
add(add(X,Y),Z) = add(X,add(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f1_nnf,plain,
! [X,Y,Z] : add(add(X,Y),Z) = add(X,add(Y,Z)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] : add(add(X,Y),Z) = add(X,add(Y,Z)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t5,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t25,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t75,plain,
add(sFlat2,add(d,X1)) = add(sFlat4,X1),
inference(cp,[status(thm)],[t25,t74]) ).
cnf(t6405,plain,
add(sFlat2,add(d,X1)) = add(sFlat3,X1),
inference(step,[status(thm)],[t75,t78]) ).
cnf(t102,plain,
add(sFlat2,add(d,X1)) = add(sFlat3,X1),
inference(orient,[status(thm)],[t6405]) ).
cnf(t103,plain,
add(sFlat3,X1) = add(sFlat2,add(X1,d)),
inference(cp,[status(thm)],[t102,t22]) ).
cnf(t117,plain,
add(sFlat2,add(X1,d)) = add(sFlat3,X1),
inference(orient,[status(thm)],[t103]) ).
cnf(t6485,plain,
sFlat2 = negate(add(d,negate(add(sFlat3,e)))),
inference(step,[status(thm)],[t6484,t117]) ).
cnf(t6486,plain,
sFlat2 = negate(add(d,negate(sFlat5))),
inference(step,[status(thm)],[t6485,t90]) ).
cnf(t6487,plain,
sFlat2 = negate(add(d,sFlat6)),
inference(step,[status(thm)],[t6486,t94]) ).
cnf(t6488,plain,
sFlat2 = negate(add(sFlat6,d)),
inference(step,[status(thm)],[t6487,t22]) ).
cnf(t1566,plain,
negate(add(sFlat6,d)) = sFlat2,
inference(orient,[status(thm)],[t6488]) ).
cnf(t1568,plain,
X1 = negate(add(negate(add(X1,add(sFlat6,d))),negate(add(X1,sFlat2)))),
inference(cp,[status(thm)],[t16,t1566]) ).
cnf(t6683,plain,
X1 = negate(add(negate(add(X1,sFlat2)),negate(add(X1,add(sFlat6,d))))),
inference(step,[status(thm)],[t1568,t22]) ).
cnf(t6306,plain,
negate(add(negate(add(X1,sFlat2)),negate(add(X1,add(sFlat6,d))))) = X1,
inference(orient,[status(thm)],[t6683]) ).
cnf(f7,hypothesis,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition) ).
fof(f7_nnf,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t6,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t6371,plain,
negate(add(negate(e),negate(sFlat1))) = d,
inference(step,[status(thm)],[t6,t37]) ).
cnf(t6372,plain,
negate(add(negate(sFlat1),negate(e))) = d,
inference(step,[status(thm)],[t6371,t22]) ).
cnf(t45,plain,
negate(add(negate(sFlat1),negate(e))) = d,
inference(orient,[status(thm)],[t6372]) ).
cnf(t6374,plain,
negate(add(sFlat2,negate(e))) = d,
inference(step,[status(thm)],[t45,t49]) ).
cnf(t51,plain,
negate(add(sFlat2,negate(e))) = d,
inference(rw,[status(thm)],[t6374]) ).
cnf(t6398,plain,
negate(add(sFlat2,sFlat0)) = d,
inference(step,[status(thm)],[t51,t56]) ).
cnf(t6399,plain,
negate(add(sFlat0,sFlat2)) = d,
inference(step,[status(thm)],[t6398,t22]) ).
cnf(t87,plain,
negate(add(sFlat0,sFlat2)) = d,
inference(orient,[status(thm)],[t6399]) ).
cnf(t6307,plain,
sFlat0 = negate(add(d,negate(add(sFlat0,add(sFlat6,d))))),
inference(cp,[status(thm)],[t6306,t87]) ).
cnf(t68,plain,
add(sFlat0,add(d,X1)) = add(sFlat1,X1),
inference(cp,[status(thm)],[t25,t67]) ).
cnf(t99,plain,
add(sFlat0,add(d,X1)) = add(sFlat1,X1),
inference(orient,[status(thm)],[t68]) ).
cnf(t100,plain,
add(sFlat1,X1) = add(sFlat0,add(X1,d)),
inference(cp,[status(thm)],[t99,t22]) ).
cnf(t108,plain,
add(sFlat0,add(X1,d)) = add(sFlat1,X1),
inference(orient,[status(thm)],[t100]) ).
cnf(t6684,plain,
sFlat0 = negate(add(d,negate(add(sFlat1,sFlat6)))),
inference(step,[status(thm)],[t6307,t108]) ).
cnf(t50,plain,
X1 = negate(add(negate(add(X1,sFlat1)),negate(add(X1,sFlat2)))),
inference(cp,[status(thm)],[t16,t49]) ).
cnf(t1263,plain,
negate(add(negate(add(X1,sFlat1)),negate(add(X1,sFlat2)))) = X1,
inference(orient,[status(thm)],[t50]) ).
cnf(t1273,plain,
X1 = negate(add(negate(add(X1,sFlat1)),negate(add(sFlat2,X1)))),
inference(cp,[status(thm)],[t1263,t22]) ).
cnf(t1380,plain,
negate(add(negate(add(X1,sFlat1)),negate(add(sFlat2,X1)))) = X1,
inference(orient,[status(thm)],[t1273]) ).
cnf(t1519,plain,
sFlat2 = negate(add(d,negate(add(sFlat2,e)))),
inference(cp,[status(thm)],[t1517,t87]) ).
cnf(t1547,plain,
negate(add(d,negate(add(sFlat2,e)))) = sFlat2,
inference(orient,[status(thm)],[t1519]) ).
cnf(t1549,plain,
d = negate(add(negate(add(d,add(sFlat2,e))),sFlat2)),
inference(cp,[status(thm)],[t16,t1547]) ).
cnf(t6497,plain,
d = negate(add(sFlat2,negate(add(d,add(sFlat2,e))))),
inference(step,[status(thm)],[t1549,t22]) ).
cnf(t26,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t25,t22]) ).
cnf(t579,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t26]) ).
cnf(t666,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(cp,[status(thm)],[t579,t22]) ).
cnf(t1168,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(orient,[status(thm)],[t666]) ).
cnf(t6498,plain,
d = negate(add(sFlat2,negate(add(e,add(sFlat2,d))))),
inference(step,[status(thm)],[t6497,t1168]) ).
cnf(t27,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t25,t22]) ).
cnf(t6463,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t27,t25]) ).
cnf(t1066,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t6463]) ).
cnf(t6499,plain,
d = negate(add(sFlat2,negate(add(sFlat2,add(e,d))))),
inference(step,[status(thm)],[t6498,t1066]) ).
cnf(t6500,plain,
d = negate(add(sFlat2,negate(add(sFlat3,e)))),
inference(step,[status(thm)],[t6499,t117]) ).
cnf(t6501,plain,
d = negate(add(sFlat2,negate(sFlat5))),
inference(step,[status(thm)],[t6500,t90]) ).
cnf(t6502,plain,
d = negate(add(sFlat2,sFlat6)),
inference(step,[status(thm)],[t6501,t94]) ).
cnf(t1583,plain,
negate(add(sFlat2,sFlat6)) = d,
inference(orient,[status(thm)],[t6502]) ).
cnf(t1584,plain,
sFlat6 = negate(add(negate(add(sFlat6,sFlat1)),d)),
inference(cp,[status(thm)],[t1380,t1583]) ).
cnf(t6503,plain,
sFlat6 = negate(add(d,negate(add(sFlat6,sFlat1)))),
inference(step,[status(thm)],[t1584,t22]) ).
cnf(t6504,plain,
sFlat6 = negate(add(d,negate(add(sFlat1,sFlat6)))),
inference(step,[status(thm)],[t6503,t22]) ).
cnf(t1592,plain,
negate(add(d,negate(add(sFlat1,sFlat6)))) = sFlat6,
inference(orient,[status(thm)],[t6504]) ).
cnf(t6685,plain,
sFlat0 = sFlat6,
inference(step,[status(thm)],[t6684,t1592]) ).
cnf(t6345,plain,
sFlat6 = sFlat0,
inference(orient,[status(thm)],[t6685]) ).
cnf(t6686,plain,
negate(sFlat5) = sFlat0,
inference(step,[status(thm)],[t94,t6345]) ).
cnf(t6346,plain,
negate(sFlat5) = sFlat0,
inference(orient,[status(thm)],[t6686]) ).
cnf(f8,negated_conjecture,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_base_step) ).
fof(f8_nnf,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(goal_0,negated_conjecture,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(g0_0,plain,
negate(add(e,add(d,negate(add(d,negate(e)))))) != negate(e),
inference(rw,[status(thm)],[goal_0,t20]) ).
cnf(g0_1,plain,
negate(add(e,add(d,negate(add(d,sFlat0))))) != negate(e),
inference(rw,[status(thm)],[g0_0,t56]) ).
cnf(g0_2,plain,
negate(add(e,add(d,negate(add(sFlat0,d))))) != negate(e),
inference(rw,[status(thm)],[g0_1,t22]) ).
cnf(g0_3,plain,
negate(add(e,add(d,negate(sFlat1)))) != negate(e),
inference(rw,[status(thm)],[g0_2,t67]) ).
cnf(g0_4,plain,
negate(add(e,add(d,sFlat2))) != negate(e),
inference(rw,[status(thm)],[g0_3,t49]) ).
cnf(g0_5,plain,
negate(add(e,add(sFlat2,d))) != negate(e),
inference(rw,[status(thm)],[g0_4,t22]) ).
cnf(g0_6,plain,
negate(add(e,sFlat3)) != negate(e),
inference(rw,[status(thm)],[g0_5,t79]) ).
cnf(g0_7,plain,
negate(add(sFlat3,e)) != negate(e),
inference(rw,[status(thm)],[g0_6,t22]) ).
cnf(g0_8,plain,
negate(sFlat5) != negate(e),
inference(rw,[status(thm)],[g0_7,t90]) ).
cnf(g0_9,plain,
sFlat0 != negate(e),
inference(rw,[status(thm)],[g0_8,t6346]) ).
cnf(g0_10,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_9,t56]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ROB014-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Thu Sep 24 08:27:12 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 16.64/2.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.64/2.51 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------