%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ROB014-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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:36 PM UTC 2026
% Result : Unsatisfiable 18.38s 2.85s
% Output : Proof 18.38s
% 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(t22,plain,
multiply(one,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t11,axiom,
sFlat0 = negate(e),
introduced(definition) ).
cnf(t102,plain,
negate(e) = sFlat0,
inference(orient,[status(thm)],[t11]) ).
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(t34,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,axiom,
sFlat1 = add(d,negate(e)),
introduced(definition) ).
cnf(t68,plain,
add(d,negate(e)) = sFlat1,
inference(orient,[status(thm)],[t12]) ).
cnf(t8265,plain,
add(d,sFlat0) = sFlat1,
inference(step,[status(thm)],[t68,t102]) ).
cnf(t105,plain,
add(d,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t8265]) ).
cnf(t8269,plain,
add(sFlat0,d) = sFlat1,
inference(step,[status(thm)],[t105,t34]) ).
cnf(t121,plain,
add(sFlat0,d) = sFlat1,
inference(orient,[status(thm)],[t8269]) ).
cnf(t13,axiom,
sFlat2 = negate(add(d,negate(e))),
introduced(definition) ).
cnf(t8258,plain,
sFlat2 = negate(sFlat1),
inference(step,[status(thm)],[t13,t68]) ).
cnf(t91,plain,
negate(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t8258]) ).
cnf(t15,axiom,
sFlat4 = multiply(one,add(d,negate(add(d,negate(e))))),
introduced(definition) ).
cnf(t8266,plain,
sFlat4 = add(d,negate(add(d,negate(e)))),
inference(step,[status(thm)],[t15,t22]) ).
cnf(t8267,plain,
sFlat4 = add(d,negate(add(d,sFlat0))),
inference(step,[status(thm)],[t8266,t102]) ).
cnf(t8268,plain,
sFlat4 = add(d,negate(add(sFlat0,d))),
inference(step,[status(thm)],[t8267,t34]) ).
cnf(t106,plain,
add(d,negate(add(sFlat0,d))) = sFlat4,
inference(orient,[status(thm)],[t8268]) ).
cnf(t8270,plain,
add(d,negate(sFlat1)) = sFlat4,
inference(step,[status(thm)],[t106,t121]) ).
cnf(t8271,plain,
add(d,sFlat2) = sFlat4,
inference(step,[status(thm)],[t8270,t91]) ).
cnf(t127,plain,
add(d,sFlat2) = sFlat4,
inference(rw,[status(thm)],[t8271]) ).
cnf(t8273,plain,
add(sFlat2,d) = sFlat4,
inference(step,[status(thm)],[t127,t34]) ).
cnf(t132,plain,
add(sFlat2,d) = sFlat4,
inference(orient,[status(thm)],[t8273]) ).
cnf(t14,axiom,
sFlat3 = add(d,negate(add(d,negate(e)))),
introduced(definition) ).
cnf(t60,plain,
add(d,negate(add(d,negate(e)))) = sFlat3,
inference(orient,[status(thm)],[t14]) ).
cnf(t8253,plain,
add(d,negate(sFlat1)) = sFlat3,
inference(step,[status(thm)],[t60,t68]) ).
cnf(t76,plain,
add(d,negate(sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t8253]) ).
cnf(t8275,plain,
add(d,sFlat2) = sFlat3,
inference(step,[status(thm)],[t76,t91]) ).
cnf(t8276,plain,
add(sFlat2,d) = sFlat3,
inference(step,[status(thm)],[t8275,t34]) ).
cnf(t8277,plain,
sFlat4 = sFlat3,
inference(step,[status(thm)],[t8276,t132]) ).
cnf(t139,plain,
sFlat4 = sFlat3,
inference(orient,[status(thm)],[t8277]) ).
cnf(t8278,plain,
add(sFlat2,d) = sFlat3,
inference(step,[status(thm)],[t132,t139]) ).
cnf(t140,plain,
add(sFlat2,d) = sFlat3,
inference(orient,[status(thm)],[t8278]) ).
cnf(t16,axiom,
sFlat5 = add(e,multiply(one,add(d,negate(add(d,negate(e)))))),
introduced(definition) ).
cnf(t8254,plain,
sFlat5 = add(e,add(d,negate(add(d,negate(e))))),
inference(step,[status(thm)],[t16,t22]) ).
cnf(t8255,plain,
sFlat5 = add(e,add(d,negate(sFlat1))),
inference(step,[status(thm)],[t8254,t68]) ).
cnf(t77,plain,
add(e,add(d,negate(sFlat1))) = sFlat5,
inference(orient,[status(thm)],[t8255]) ).
cnf(t8260,plain,
add(e,add(d,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t77,t91]) ).
cnf(t95,plain,
add(e,add(d,sFlat2)) = sFlat5,
inference(rw,[status(thm)],[t8260]) ).
cnf(t8285,plain,
add(e,add(sFlat2,d)) = sFlat5,
inference(step,[status(thm)],[t95,t34]) ).
cnf(t8286,plain,
add(e,sFlat3) = sFlat5,
inference(step,[status(thm)],[t8285,t140]) ).
cnf(t8287,plain,
add(sFlat3,e) = sFlat5,
inference(step,[status(thm)],[t8286,t34]) ).
cnf(t158,plain,
add(sFlat3,e) = sFlat5,
inference(orient,[status(thm)],[t8287]) ).
cnf(t17,axiom,
sFlat6 = negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))),
introduced(definition) ).
cnf(t8261,plain,
sFlat6 = negate(add(e,add(d,negate(add(d,negate(e)))))),
inference(step,[status(thm)],[t17,t22]) ).
cnf(t8262,plain,
sFlat6 = negate(add(e,add(d,negate(sFlat1)))),
inference(step,[status(thm)],[t8261,t68]) ).
cnf(t8263,plain,
sFlat6 = negate(add(e,add(d,sFlat2))),
inference(step,[status(thm)],[t8262,t91]) ).
cnf(t8264,plain,
sFlat6 = negate(add(e,add(sFlat2,d))),
inference(step,[status(thm)],[t8263,t34]) ).
cnf(t96,plain,
negate(add(e,add(sFlat2,d))) = sFlat6,
inference(orient,[status(thm)],[t8264]) ).
cnf(t8274,plain,
negate(add(e,sFlat4)) = sFlat6,
inference(step,[status(thm)],[t96,t132]) ).
cnf(t138,plain,
negate(add(e,sFlat4)) = sFlat6,
inference(rw,[status(thm)],[t8274]) ).
cnf(t8281,plain,
negate(add(sFlat4,e)) = sFlat6,
inference(step,[status(thm)],[t138,t34]) ).
cnf(t8282,plain,
negate(add(sFlat3,e)) = sFlat6,
inference(step,[status(thm)],[t8281,t139]) ).
cnf(t146,plain,
negate(add(sFlat3,e)) = sFlat6,
inference(orient,[status(thm)],[t8282]) ).
cnf(t8288,plain,
negate(sFlat5) = sFlat6,
inference(step,[status(thm)],[t146,t158]) ).
cnf(t164,plain,
negate(sFlat5) = sFlat6,
inference(rw,[status(thm)],[t8288]) ).
cnf(t165,plain,
negate(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t164]) ).
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(t18,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t103,plain,
X1 = negate(add(negate(add(X1,e)),negate(add(X1,sFlat0)))),
inference(cp,[status(thm)],[t18,t102]) ).
cnf(t8355,plain,
X1 = negate(add(negate(add(X1,sFlat0)),negate(add(X1,e)))),
inference(step,[status(thm)],[t103,t34]) ).
cnf(t1613,plain,
negate(add(negate(add(X1,sFlat0)),negate(add(X1,e)))) = X1,
inference(orient,[status(thm)],[t8355]) ).
cnf(t1617,plain,
X1 = negate(add(negate(add(sFlat0,X1)),negate(add(X1,e)))),
inference(cp,[status(thm)],[t1613,t34]) ).
cnf(t1882,plain,
negate(add(negate(add(sFlat0,X1)),negate(add(X1,e)))) = X1,
inference(orient,[status(thm)],[t1617]) ).
cnf(t1890,plain,
d = negate(add(negate(sFlat1),negate(add(d,e)))),
inference(cp,[status(thm)],[t1882,t121]) ).
cnf(t8367,plain,
d = negate(add(sFlat2,negate(add(d,e)))),
inference(step,[status(thm)],[t1890,t91]) ).
cnf(t8368,plain,
d = negate(add(sFlat2,negate(add(e,d)))),
inference(step,[status(thm)],[t8367,t34]) ).
cnf(t1933,plain,
negate(add(sFlat2,negate(add(e,d)))) = d,
inference(orient,[status(thm)],[t8368]) ).
cnf(t1936,plain,
sFlat2 = negate(add(negate(add(sFlat2,add(e,d))),d)),
inference(cp,[status(thm)],[t18,t1933]) ).
cnf(t8369,plain,
sFlat2 = negate(add(d,negate(add(sFlat2,add(e,d))))),
inference(step,[status(thm)],[t1936,t34]) ).
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(t44,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t133,plain,
add(sFlat2,add(d,X1)) = add(sFlat4,X1),
inference(cp,[status(thm)],[t44,t132]) ).
cnf(t8290,plain,
add(sFlat2,add(d,X1)) = add(sFlat3,X1),
inference(step,[status(thm)],[t133,t139]) ).
cnf(t178,plain,
add(sFlat2,add(d,X1)) = add(sFlat3,X1),
inference(orient,[status(thm)],[t8290]) ).
cnf(t179,plain,
add(sFlat3,X1) = add(sFlat2,add(X1,d)),
inference(cp,[status(thm)],[t178,t34]) ).
cnf(t205,plain,
add(sFlat2,add(X1,d)) = add(sFlat3,X1),
inference(orient,[status(thm)],[t179]) ).
cnf(t8370,plain,
sFlat2 = negate(add(d,negate(add(sFlat3,e)))),
inference(step,[status(thm)],[t8369,t205]) ).
cnf(t8371,plain,
sFlat2 = negate(add(d,negate(sFlat5))),
inference(step,[status(thm)],[t8370,t158]) ).
cnf(t8372,plain,
sFlat2 = negate(add(d,sFlat6)),
inference(step,[status(thm)],[t8371,t165]) ).
cnf(t8373,plain,
sFlat2 = negate(add(sFlat6,d)),
inference(step,[status(thm)],[t8372,t34]) ).
cnf(t1949,plain,
negate(add(sFlat6,d)) = sFlat2,
inference(orient,[status(thm)],[t8373]) ).
cnf(t1951,plain,
X1 = negate(add(negate(add(X1,add(sFlat6,d))),negate(add(X1,sFlat2)))),
inference(cp,[status(thm)],[t18,t1949]) ).
cnf(t8592,plain,
X1 = negate(add(negate(add(X1,sFlat2)),negate(add(X1,add(sFlat6,d))))),
inference(step,[status(thm)],[t1951,t34]) ).
cnf(t8175,plain,
negate(add(negate(add(X1,sFlat2)),negate(add(X1,add(sFlat6,d))))) = X1,
inference(orient,[status(thm)],[t8592]) ).
cnf(f9,hypothesis,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition) ).
fof(f9_nnf,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t6,plain,
negate(add(negate(e),negate(add(d,negate(e))))) = d,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t8256,plain,
negate(add(negate(e),negate(sFlat1))) = d,
inference(step,[status(thm)],[t6,t68]) ).
cnf(t8257,plain,
negate(add(negate(sFlat1),negate(e))) = d,
inference(step,[status(thm)],[t8256,t34]) ).
cnf(t83,plain,
negate(add(negate(sFlat1),negate(e))) = d,
inference(orient,[status(thm)],[t8257]) ).
cnf(t8259,plain,
negate(add(sFlat2,negate(e))) = d,
inference(step,[status(thm)],[t83,t91]) ).
cnf(t94,plain,
negate(add(sFlat2,negate(e))) = d,
inference(rw,[status(thm)],[t8259]) ).
cnf(t8283,plain,
negate(add(sFlat2,sFlat0)) = d,
inference(step,[status(thm)],[t94,t102]) ).
cnf(t8284,plain,
negate(add(sFlat0,sFlat2)) = d,
inference(step,[status(thm)],[t8283,t34]) ).
cnf(t152,plain,
negate(add(sFlat0,sFlat2)) = d,
inference(orient,[status(thm)],[t8284]) ).
cnf(t8176,plain,
sFlat0 = negate(add(d,negate(add(sFlat0,add(sFlat6,d))))),
inference(cp,[status(thm)],[t8175,t152]) ).
cnf(t122,plain,
add(sFlat0,add(d,X1)) = add(sFlat1,X1),
inference(cp,[status(thm)],[t44,t121]) ).
cnf(t172,plain,
add(sFlat0,add(d,X1)) = add(sFlat1,X1),
inference(orient,[status(thm)],[t122]) ).
cnf(t173,plain,
add(sFlat1,X1) = add(sFlat0,add(X1,d)),
inference(cp,[status(thm)],[t172,t34]) ).
cnf(t190,plain,
add(sFlat0,add(X1,d)) = add(sFlat1,X1),
inference(orient,[status(thm)],[t173]) ).
cnf(t8593,plain,
sFlat0 = negate(add(d,negate(add(sFlat1,sFlat6)))),
inference(step,[status(thm)],[t8176,t190]) ).
cnf(t92,plain,
X1 = negate(add(negate(add(X1,sFlat1)),negate(add(X1,sFlat2)))),
inference(cp,[status(thm)],[t18,t91]) ).
cnf(t1551,plain,
negate(add(negate(add(X1,sFlat1)),negate(add(X1,sFlat2)))) = X1,
inference(orient,[status(thm)],[t92]) ).
cnf(t1561,plain,
X1 = negate(add(negate(add(X1,sFlat1)),negate(add(sFlat2,X1)))),
inference(cp,[status(thm)],[t1551,t34]) ).
cnf(t1833,plain,
negate(add(negate(add(X1,sFlat1)),negate(add(sFlat2,X1)))) = X1,
inference(orient,[status(thm)],[t1561]) ).
cnf(t1884,plain,
sFlat2 = negate(add(d,negate(add(sFlat2,e)))),
inference(cp,[status(thm)],[t1882,t152]) ).
cnf(t1918,plain,
negate(add(d,negate(add(sFlat2,e)))) = sFlat2,
inference(orient,[status(thm)],[t1884]) ).
cnf(t1920,plain,
d = negate(add(negate(add(d,add(sFlat2,e))),sFlat2)),
inference(cp,[status(thm)],[t18,t1918]) ).
cnf(t8382,plain,
d = negate(add(sFlat2,negate(add(d,add(sFlat2,e))))),
inference(step,[status(thm)],[t1920,t34]) ).
cnf(t45,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t44,t34]) ).
cnf(t822,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t45]) ).
cnf(t912,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(cp,[status(thm)],[t822,t34]) ).
cnf(t1453,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(orient,[status(thm)],[t912]) ).
cnf(t8383,plain,
d = negate(add(sFlat2,negate(add(e,add(sFlat2,d))))),
inference(step,[status(thm)],[t8382,t1453]) ).
cnf(t46,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t44,t34]) ).
cnf(t8348,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t46,t44]) ).
cnf(t1348,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t8348]) ).
cnf(t8384,plain,
d = negate(add(sFlat2,negate(add(sFlat2,add(e,d))))),
inference(step,[status(thm)],[t8383,t1348]) ).
cnf(t8385,plain,
d = negate(add(sFlat2,negate(add(sFlat3,e)))),
inference(step,[status(thm)],[t8384,t205]) ).
cnf(t8386,plain,
d = negate(add(sFlat2,negate(sFlat5))),
inference(step,[status(thm)],[t8385,t158]) ).
cnf(t8387,plain,
d = negate(add(sFlat2,sFlat6)),
inference(step,[status(thm)],[t8386,t165]) ).
cnf(t1975,plain,
negate(add(sFlat2,sFlat6)) = d,
inference(orient,[status(thm)],[t8387]) ).
cnf(t1976,plain,
sFlat6 = negate(add(negate(add(sFlat6,sFlat1)),d)),
inference(cp,[status(thm)],[t1833,t1975]) ).
cnf(t8388,plain,
sFlat6 = negate(add(d,negate(add(sFlat6,sFlat1)))),
inference(step,[status(thm)],[t1976,t34]) ).
cnf(t8389,plain,
sFlat6 = negate(add(d,negate(add(sFlat1,sFlat6)))),
inference(step,[status(thm)],[t8388,t34]) ).
cnf(t1987,plain,
negate(add(d,negate(add(sFlat1,sFlat6)))) = sFlat6,
inference(orient,[status(thm)],[t8389]) ).
cnf(t8594,plain,
sFlat0 = sFlat6,
inference(step,[status(thm)],[t8593,t1987]) ).
cnf(t8226,plain,
sFlat6 = sFlat0,
inference(orient,[status(thm)],[t8594]) ).
cnf(t8595,plain,
negate(sFlat5) = sFlat0,
inference(step,[status(thm)],[t165,t8226]) ).
cnf(t8227,plain,
negate(sFlat5) = sFlat0,
inference(orient,[status(thm)],[t8595]) ).
cnf(f10,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(f10_nnf,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
negate(add(e,multiply(one,add(d,negate(add(d,negate(e))))))) != negate(e),
inference(cnf_transformation,[status(esa)],[f10_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)],[c10]) ).
cnf(g0_0,plain,
negate(add(e,add(d,negate(add(d,negate(e)))))) != negate(e),
inference(rw,[status(thm)],[goal_0,t22]) ).
cnf(g0_1,plain,
negate(add(e,add(d,negate(add(d,sFlat0))))) != negate(e),
inference(rw,[status(thm)],[g0_0,t102]) ).
cnf(g0_2,plain,
negate(add(e,add(d,negate(add(sFlat0,d))))) != negate(e),
inference(rw,[status(thm)],[g0_1,t34]) ).
cnf(g0_3,plain,
negate(add(e,add(d,negate(sFlat1)))) != negate(e),
inference(rw,[status(thm)],[g0_2,t121]) ).
cnf(g0_4,plain,
negate(add(e,add(d,sFlat2))) != negate(e),
inference(rw,[status(thm)],[g0_3,t91]) ).
cnf(g0_5,plain,
negate(add(e,add(sFlat2,d))) != negate(e),
inference(rw,[status(thm)],[g0_4,t34]) ).
cnf(g0_6,plain,
negate(add(e,sFlat3)) != negate(e),
inference(rw,[status(thm)],[g0_5,t140]) ).
cnf(g0_7,plain,
negate(add(sFlat3,e)) != negate(e),
inference(rw,[status(thm)],[g0_6,t34]) ).
cnf(g0_8,plain,
negate(sFlat5) != negate(e),
inference(rw,[status(thm)],[g0_7,t158]) ).
cnf(g0_9,plain,
sFlat0 != negate(e),
inference(rw,[status(thm)],[g0_8,t8227]) ).
cnf(g0_10,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_9,t102]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ROB014-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 08:26:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.38/2.85 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.38/2.85 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------