%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 03:32:09 PM UTC 2026
% Result : Theorem 5.16s 1.21s
% Output : Proof 5.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 27
% Syntax : Number of formulae : 242 ( 229 unt; 0 def)
% Number of atoms : 259 ( 233 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 45 ( 28 ~; 12 |; 2 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-4 aty)
% Number of variables : 166 ( 5 sgn 61 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [N] :
( evenNat(suc(N))
<=> ~ evenNat(N) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
fof(f10_nnf,plain,
! [N] :
( ( evenNat(N)
| evenNat(suc(N)) )
& ( ~ evenNat(N)
| ~ evenNat(suc(N)) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [N] :
( ( evenNat(N)
| evenNat(suc(N)) )
& ( ~ evenNat(N)
| ~ evenNat(suc(N)) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c11,plain,
( evenNat(X0)
| evenNat(suc(X0)) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t27,plain,
or(evenNat(suc(X1)),evenNat(X1)) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t56,plain,
or(evenNat(suc(X1)),evenNat(X1)) = true,
inference(orient,[status(thm)],[t27]) ).
fof(f17,axiom,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
fof(f17_nnf,plain,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [Z,Y] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c18,plain,
addNat(suc(X1),X0) = suc(addNat(X1,X0)),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t31,plain,
suc(addNat(X1,X2)) = addNat(suc(X1),X2),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t64,plain,
suc(addNat(X1,X2)) = addNat(suc(X1),X2),
inference(orient,[status(thm)],[t31]) ).
fof(f16,axiom,
! [Y] : addNat(zero,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_017) ).
fof(f16_nnf,plain,
! [Y] : addNat(zero,Y) = Y,
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Y] : addNat(zero,Y) = Y,
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
addNat(zero,X0) = X0,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t6,plain,
addNat(zero,X1) = X1,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t43,plain,
addNat(zero,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t65,plain,
addNat(suc(zero),X1) = suc(X1),
inference(cp,[status(thm)],[t64,t43]) ).
cnf(t110,plain,
addNat(suc(zero),X1) = suc(X1),
inference(orient,[status(thm)],[t65]) ).
cnf(t112,plain,
addNat(suc(suc(zero)),X1) = suc(suc(X1)),
inference(cp,[status(thm)],[t64,t110]) ).
cnf(t123,plain,
addNat(suc(suc(zero)),X1) = suc(suc(X1)),
inference(orient,[status(thm)],[t112]) ).
cnf(t125,plain,
addNat(suc(suc(suc(zero))),X1) = suc(suc(suc(X1))),
inference(cp,[status(thm)],[t64,t123]) ).
cnf(t302,plain,
addNat(suc(suc(suc(zero))),X1) = suc(suc(suc(X1))),
inference(orient,[status(thm)],[t125]) ).
fof(f18,axiom,
! [X] : double(X) = addNat(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(f18_nnf,plain,
! [X] : double(X) = addNat(X,X),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X] : double(X) = addNat(X,X),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c19,plain,
double(X0) = addNat(X0,X0),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t16,plain,
addNat(X1,X1) = double(X1),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t102,plain,
addNat(X1,X1) = double(X1),
inference(orient,[status(thm)],[t16]) ).
cnf(t303,plain,
suc(suc(suc(suc(suc(suc(zero)))))) = double(suc(suc(suc(zero)))),
inference(cp,[status(thm)],[t302,t102]) ).
cnf(t124,plain,
suc(suc(suc(suc(zero)))) = double(suc(suc(zero))),
inference(cp,[status(thm)],[t123,t102]) ).
cnf(t138,plain,
suc(suc(suc(suc(zero)))) = double(suc(suc(zero))),
inference(orient,[status(thm)],[t124]) ).
cnf(t718,plain,
suc(suc(double(suc(suc(zero))))) = double(suc(suc(suc(zero)))),
inference(step,[status(thm)],[t303,t138]) ).
cnf(t460,plain,
suc(suc(double(suc(suc(zero))))) = double(suc(suc(suc(zero)))),
inference(orient,[status(thm)],[t718]) ).
cnf(t471,plain,
true = or(evenNat(double(suc(suc(suc(zero))))),evenNat(suc(double(suc(suc(zero)))))),
inference(cp,[status(thm)],[t56,t460]) ).
cnf(t25,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t76,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t25]) ).
cnf(c10,plain,
( ~ evenNat(X0)
| ~ evenNat(suc(X0)) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t33,plain,
or(not(evenNat(suc(X1))),not(evenNat(X1))) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t58,plain,
or(not(evenNat(suc(X1))),not(evenNat(X1))) = true,
inference(orient,[status(thm)],[t33]) ).
fof(f9,axiom,
evenNat(zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_010) ).
fof(f9_nnf,plain,
evenNat(zero),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
evenNat(zero),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t0,plain,
evenNat(zero) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t48,plain,
evenNat(zero) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t59,plain,
true = or(not(evenNat(suc(zero))),not(true)),
inference(cp,[status(thm)],[t58,t48]) ).
cnf(t3,plain,
not(true) = false,
introduced(definition) ).
cnf(t84,plain,
not(true) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t669,plain,
true = or(not(evenNat(suc(zero))),false),
inference(step,[status(thm)],[t59,t84]) ).
cnf(t11,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t41,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t670,plain,
true = not(evenNat(suc(zero))),
inference(step,[status(thm)],[t669,t41]) ).
cnf(t166,plain,
not(evenNat(suc(zero))) = true,
inference(orient,[status(thm)],[t670]) ).
cnf(t167,plain,
false = ifeq(true,true,evenNat(suc(zero)),false),
inference(cp,[status(thm)],[t76,t166]) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t39,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t671,plain,
false = evenNat(suc(zero)),
inference(step,[status(thm)],[t167,t39]) ).
cnf(t168,plain,
evenNat(suc(zero)) = false,
inference(orient,[status(thm)],[t671]) ).
cnf(t171,plain,
true = or(evenNat(suc(suc(zero))),false),
inference(cp,[status(thm)],[t56,t168]) ).
cnf(t673,plain,
true = evenNat(suc(suc(zero))),
inference(step,[status(thm)],[t171,t41]) ).
cnf(t175,plain,
evenNat(suc(suc(zero))) = true,
inference(orient,[status(thm)],[t673]) ).
cnf(t178,plain,
true = or(not(evenNat(suc(suc(suc(zero))))),not(true)),
inference(cp,[status(thm)],[t58,t175]) ).
cnf(t676,plain,
true = or(not(evenNat(suc(suc(suc(zero))))),false),
inference(step,[status(thm)],[t178,t84]) ).
cnf(t677,plain,
true = not(evenNat(suc(suc(suc(zero))))),
inference(step,[status(thm)],[t676,t41]) ).
cnf(t181,plain,
not(evenNat(suc(suc(suc(zero))))) = true,
inference(orient,[status(thm)],[t677]) ).
cnf(t182,plain,
false = ifeq(true,true,evenNat(suc(suc(suc(zero)))),false),
inference(cp,[status(thm)],[t76,t181]) ).
cnf(t678,plain,
false = evenNat(suc(suc(suc(zero)))),
inference(step,[status(thm)],[t182,t39]) ).
cnf(t183,plain,
evenNat(suc(suc(suc(zero)))) = false,
inference(orient,[status(thm)],[t678]) ).
cnf(t185,plain,
true = or(evenNat(suc(suc(suc(suc(zero))))),false),
inference(cp,[status(thm)],[t56,t183]) ).
cnf(t679,plain,
true = evenNat(suc(suc(suc(suc(zero))))),
inference(step,[status(thm)],[t185,t41]) ).
cnf(t680,plain,
true = evenNat(double(suc(suc(zero)))),
inference(step,[status(thm)],[t679,t138]) ).
cnf(t188,plain,
evenNat(double(suc(suc(zero)))) = true,
inference(orient,[status(thm)],[t680]) ).
cnf(t190,plain,
true = or(not(evenNat(suc(double(suc(suc(zero)))))),not(true)),
inference(cp,[status(thm)],[t58,t188]) ).
cnf(t703,plain,
true = or(not(evenNat(suc(double(suc(suc(zero)))))),false),
inference(step,[status(thm)],[t190,t84]) ).
cnf(t704,plain,
true = not(evenNat(suc(double(suc(suc(zero)))))),
inference(step,[status(thm)],[t703,t41]) ).
cnf(t286,plain,
not(evenNat(suc(double(suc(suc(zero)))))) = true,
inference(orient,[status(thm)],[t704]) ).
cnf(t287,plain,
false = ifeq(true,true,evenNat(suc(double(suc(suc(zero))))),false),
inference(cp,[status(thm)],[t76,t286]) ).
cnf(t705,plain,
false = evenNat(suc(double(suc(suc(zero))))),
inference(step,[status(thm)],[t287,t39]) ).
cnf(t288,plain,
evenNat(suc(double(suc(suc(zero))))) = false,
inference(orient,[status(thm)],[t705]) ).
cnf(t720,plain,
true = or(evenNat(double(suc(suc(suc(zero))))),false),
inference(step,[status(thm)],[t471,t288]) ).
cnf(t721,plain,
true = evenNat(double(suc(suc(suc(zero))))),
inference(step,[status(thm)],[t720,t41]) ).
cnf(t494,plain,
evenNat(double(suc(suc(suc(zero))))) = true,
inference(orient,[status(thm)],[t721]) ).
fof(f22,axiom,
! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_023) ).
fof(f22_nnf,plain,
! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c23,plain,
x(X0,X1) = rd(append(shw(X0),shw(X1))),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t34,plain,
rd(append(shw(X1),shw(X2))) = x(X1,X2),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t99,plain,
rd(append(shw(X1),shw(X2))) = x(X1,X2),
inference(orient,[status(thm)],[t34]) ).
fof(f15,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(f15_nnf,plain,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Z,Xs,Y] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c16,plain,
append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t35,plain,
cons(X1,append(X2,X3)) = append(cons(X1,X2),X3),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t86,plain,
append(cons(X1,X2),X3) = cons(X1,append(X2,X3)),
inference(orient,[status(thm)],[t35]) ).
fof(f12,axiom,
! [Y] :
( evenNat(suc(Y))
=> shw(suc(Y)) = cons(o,shw(half(suc(Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_013) ).
fof(f12_nnf,plain,
! [Y] :
( shw(suc(Y)) = cons(o,shw(half(suc(Y))))
| ~ evenNat(suc(Y)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Y] :
( shw(suc(Y)) = cons(o,shw(half(suc(Y))))
| ~ evenNat(suc(Y)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
( shw(suc(X0)) = cons(o,shw(half(suc(X0))))
| ~ evenNat(suc(X0)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t38,plain,
ifeq(evenNat(suc(X1)),true,shw(suc(X1)),cons(o,shw(half(suc(X1))))) = cons(o,shw(half(suc(X1)))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t87,plain,
ifeq(evenNat(suc(X1)),true,shw(suc(X1)),cons(o,shw(half(suc(X1))))) = cons(o,shw(half(suc(X1)))),
inference(orient,[status(thm)],[t38]) ).
cnf(t179,plain,
cons(o,shw(half(suc(suc(zero))))) = ifeq(true,true,shw(suc(suc(zero))),cons(o,shw(half(suc(suc(zero)))))),
inference(cp,[status(thm)],[t87,t175]) ).
fof(f8,axiom,
! [N] : half(suc(suc(N))) = suc(half(N)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_009) ).
fof(f8_nnf,plain,
! [N] : half(suc(suc(N))) = suc(half(N)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [N] : half(suc(suc(N))) = suc(half(N)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
half(suc(suc(X0))) = suc(half(X0)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t24,plain,
half(suc(suc(X1))) = suc(half(X1)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t62,plain,
half(suc(suc(X1))) = suc(half(X1)),
inference(orient,[status(thm)],[t24]) ).
cnf(t681,plain,
cons(o,shw(suc(half(zero)))) = ifeq(true,true,shw(suc(suc(zero))),cons(o,shw(half(suc(suc(zero)))))),
inference(step,[status(thm)],[t179,t62]) ).
fof(f6,axiom,
half(zero) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
fof(f6_nnf,plain,
half(zero) = zero,
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
half(zero) = zero,
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t1,plain,
half(zero) = zero,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t95,plain,
half(zero) = zero,
inference(orient,[status(thm)],[t1]) ).
cnf(t682,plain,
cons(o,shw(suc(zero))) = ifeq(true,true,shw(suc(suc(zero))),cons(o,shw(half(suc(suc(zero)))))),
inference(step,[status(thm)],[t681,t95]) ).
cnf(t683,plain,
cons(o,shw(suc(zero))) = shw(suc(suc(zero))),
inference(step,[status(thm)],[t682,t39]) ).
cnf(t191,plain,
cons(o,shw(suc(zero))) = shw(suc(suc(zero))),
inference(orient,[status(thm)],[t683]) ).
cnf(t29,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t40,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t29]) ).
fof(f13,axiom,
! [Y] :
( ~ evenNat(suc(Y))
=> shw(suc(Y)) = cons(i,shw(half(suc(Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(f13_nnf,plain,
! [Y] :
( shw(suc(Y)) = cons(i,shw(half(suc(Y))))
| evenNat(suc(Y)) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Y] :
( shw(suc(Y)) = cons(i,shw(half(suc(Y))))
| evenNat(suc(Y)) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c14,plain,
( shw(suc(X0)) = cons(i,shw(half(suc(X0))))
| evenNat(suc(X0)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t37,plain,
or(evenNat(suc(X1)),eq(shw(suc(X1)),cons(i,shw(half(suc(X1)))))) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t57,plain,
or(evenNat(suc(X1)),eq(shw(suc(X1)),cons(i,shw(half(suc(X1)))))) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(t173,plain,
true = or(false,eq(shw(suc(zero)),cons(i,shw(half(suc(zero)))))),
inference(cp,[status(thm)],[t57,t168]) ).
cnf(t13,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t42,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t686,plain,
true = eq(shw(suc(zero)),cons(i,shw(half(suc(zero))))),
inference(step,[status(thm)],[t173,t42]) ).
fof(f7,axiom,
half(suc(zero)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
fof(f7_nnf,plain,
half(suc(zero)) = zero,
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
half(suc(zero)) = zero,
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t10,plain,
half(suc(zero)) = zero,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t92,plain,
half(suc(zero)) = zero,
inference(orient,[status(thm)],[t10]) ).
cnf(t687,plain,
true = eq(shw(suc(zero)),cons(i,shw(zero))),
inference(step,[status(thm)],[t686,t92]) ).
fof(f11,axiom,
shw(zero) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(f11_nnf,plain,
shw(zero) = nil,
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c12,plain,
shw(zero) = nil,
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t5,plain,
shw(zero) = nil,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t97,plain,
shw(zero) = nil,
inference(orient,[status(thm)],[t5]) ).
cnf(t688,plain,
true = eq(shw(suc(zero)),cons(i,nil)),
inference(step,[status(thm)],[t687,t97]) ).
cnf(t212,plain,
eq(shw(suc(zero)),cons(i,nil)) = true,
inference(orient,[status(thm)],[t688]) ).
cnf(t213,plain,
cons(i,nil) = ifeq(true,true,shw(suc(zero)),cons(i,nil)),
inference(cp,[status(thm)],[t40,t212]) ).
cnf(t689,plain,
cons(i,nil) = shw(suc(zero)),
inference(step,[status(thm)],[t213,t39]) ).
cnf(t214,plain,
shw(suc(zero)) = cons(i,nil),
inference(orient,[status(thm)],[t689]) ).
cnf(t692,plain,
cons(o,cons(i,nil)) = shw(suc(suc(zero))),
inference(step,[status(thm)],[t191,t214]) ).
cnf(t222,plain,
cons(o,cons(i,nil)) = shw(suc(suc(zero))),
inference(rw,[status(thm)],[t692]) ).
cnf(t257,plain,
cons(o,cons(i,nil)) = shw(suc(suc(zero))),
inference(orient,[status(thm)],[t222]) ).
cnf(t258,plain,
cons(o,append(cons(i,nil),X1)) = append(shw(suc(suc(zero))),X1),
inference(cp,[status(thm)],[t86,t257]) ).
cnf(t710,plain,
cons(o,cons(i,append(nil,X1))) = append(shw(suc(suc(zero))),X1),
inference(step,[status(thm)],[t258,t86]) ).
fof(f14,axiom,
! [Y] : append(nil,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
fof(f14_nnf,plain,
! [Y] : append(nil,Y) = Y,
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Y] : append(nil,Y) = Y,
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
append(nil,X0) = X0,
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t7,plain,
append(nil,X1) = X1,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t44,plain,
append(nil,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t711,plain,
cons(o,cons(i,X1)) = append(shw(suc(suc(zero))),X1),
inference(step,[status(thm)],[t710,t44]) ).
cnf(t423,plain,
append(shw(suc(suc(zero))),X1) = cons(o,cons(i,X1)),
inference(orient,[status(thm)],[t711]) ).
cnf(t425,plain,
x(suc(suc(zero)),X1) = rd(cons(o,cons(i,shw(X1)))),
inference(cp,[status(thm)],[t99,t423]) ).
fof(f21,axiom,
! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
fof(f21_nnf,plain,
! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c22,plain,
rd(cons(o,X0)) = double(rd(X0)),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t28,plain,
rd(cons(o,X1)) = double(rd(X1)),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t98,plain,
rd(cons(o,X1)) = double(rd(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t712,plain,
x(suc(suc(zero)),X1) = double(rd(cons(i,shw(X1)))),
inference(step,[status(thm)],[t425,t98]) ).
fof(f20,axiom,
! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_021) ).
fof(f20_nnf,plain,
! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c21,plain,
rd(cons(i,X0)) = suc(double(rd(X0))),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t32,plain,
suc(double(rd(X1))) = rd(cons(i,X1)),
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t75,plain,
rd(cons(i,X1)) = suc(double(rd(X1))),
inference(orient,[status(thm)],[t32]) ).
cnf(t713,plain,
x(suc(suc(zero)),X1) = double(suc(double(rd(shw(X1))))),
inference(step,[status(thm)],[t712,t75]) ).
cnf(t100,plain,
x(zero,X1) = rd(append(nil,shw(X1))),
inference(cp,[status(thm)],[t99,t97]) ).
cnf(t662,plain,
x(zero,X1) = rd(shw(X1)),
inference(step,[status(thm)],[t100,t44]) ).
cnf(t107,plain,
rd(shw(X1)) = x(zero,X1),
inference(orient,[status(thm)],[t662]) ).
cnf(t714,plain,
x(suc(suc(zero)),X1) = double(suc(double(x(zero,X1)))),
inference(step,[status(thm)],[t713,t107]) ).
cnf(t219,plain,
x(suc(zero),X1) = rd(append(cons(i,nil),shw(X1))),
inference(cp,[status(thm)],[t99,t214]) ).
cnf(t698,plain,
x(suc(zero),X1) = rd(cons(i,append(nil,shw(X1)))),
inference(step,[status(thm)],[t219,t86]) ).
cnf(t699,plain,
x(suc(zero),X1) = suc(double(rd(append(nil,shw(X1))))),
inference(step,[status(thm)],[t698,t75]) ).
cnf(t700,plain,
x(suc(zero),X1) = suc(double(rd(shw(X1)))),
inference(step,[status(thm)],[t699,t44]) ).
cnf(t701,plain,
x(suc(zero),X1) = suc(double(x(zero,X1))),
inference(step,[status(thm)],[t700,t107]) ).
cnf(t226,plain,
suc(double(x(zero,X1))) = x(suc(zero),X1),
inference(orient,[status(thm)],[t701]) ).
cnf(t715,plain,
x(suc(suc(zero)),X1) = double(x(suc(zero),X1)),
inference(step,[status(thm)],[t714,t226]) ).
cnf(t444,plain,
double(x(suc(zero),X1)) = x(suc(suc(zero)),X1),
inference(orient,[status(thm)],[t715]) ).
cnf(t217,plain,
x(zero,suc(zero)) = rd(cons(i,nil)),
inference(cp,[status(thm)],[t107,t214]) ).
cnf(t693,plain,
x(zero,suc(zero)) = suc(double(rd(nil))),
inference(step,[status(thm)],[t217,t75]) ).
fof(f19,axiom,
rd(nil) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
fof(f19_nnf,plain,
rd(nil) = zero,
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c20,plain,
rd(nil) = zero,
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(t4,plain,
rd(nil) = zero,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t96,plain,
rd(nil) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t694,plain,
x(zero,suc(zero)) = suc(double(zero)),
inference(step,[status(thm)],[t693,t96]) ).
cnf(t103,plain,
double(zero) = zero,
inference(cp,[status(thm)],[t102,t43]) ).
cnf(t106,plain,
double(zero) = zero,
inference(orient,[status(thm)],[t103]) ).
cnf(t695,plain,
x(zero,suc(zero)) = suc(zero),
inference(step,[status(thm)],[t694,t106]) ).
cnf(t223,plain,
x(zero,suc(zero)) = suc(zero),
inference(orient,[status(thm)],[t695]) ).
cnf(t228,plain,
x(suc(zero),suc(zero)) = suc(double(suc(zero))),
inference(cp,[status(thm)],[t226,t223]) ).
cnf(t111,plain,
suc(suc(zero)) = double(suc(zero)),
inference(cp,[status(thm)],[t110,t102]) ).
cnf(t113,plain,
double(suc(zero)) = suc(suc(zero)),
inference(orient,[status(thm)],[t111]) ).
cnf(t702,plain,
x(suc(zero),suc(zero)) = suc(suc(suc(zero))),
inference(step,[status(thm)],[t228,t113]) ).
cnf(t260,plain,
x(suc(zero),suc(zero)) = suc(suc(suc(zero))),
inference(orient,[status(thm)],[t702]) ).
cnf(t445,plain,
x(suc(suc(zero)),suc(zero)) = double(suc(suc(suc(zero)))),
inference(cp,[status(thm)],[t444,t260]) ).
fof(f23,conjecture,
? [X,Y] : x(X,Y) != x(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_024) ).
fof(f23_neg,negated_conjecture,
~ ? [X,Y] : x(X,Y) != x(Y,X),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f23_nnf,plain,
! [X,Y] : x(X,Y) = x(Y,X),
inference(nnf_transformation,[status(thm)],[f23_neg]) ).
fof(f23_sk,plain,
! [X,Y] : x(X,Y) = x(Y,X),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c24,plain,
x(X0,X1) = x(X1,X0),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t23,plain,
x(X1,X2) = x(X2,X1),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t105,plain,
x(X1,X2) = x(X2,X1),
inference(orient,[status(thm)],[t23]) ).
cnf(t725,plain,
x(suc(zero),suc(suc(zero))) = double(suc(suc(suc(zero)))),
inference(step,[status(thm)],[t445,t105]) ).
cnf(t192,plain,
double(rd(shw(suc(zero)))) = rd(shw(suc(suc(zero)))),
inference(cp,[status(thm)],[t98,t191]) ).
cnf(t684,plain,
double(x(zero,suc(zero))) = rd(shw(suc(suc(zero)))),
inference(step,[status(thm)],[t192,t107]) ).
cnf(t685,plain,
double(x(zero,suc(zero))) = x(zero,suc(suc(zero))),
inference(step,[status(thm)],[t684,t107]) ).
cnf(t202,plain,
double(x(zero,suc(zero))) = x(zero,suc(suc(zero))),
inference(orient,[status(thm)],[t685]) ).
cnf(t696,plain,
double(suc(zero)) = x(zero,suc(suc(zero))),
inference(step,[status(thm)],[t202,t223]) ).
cnf(t697,plain,
suc(suc(zero)) = x(zero,suc(suc(zero))),
inference(step,[status(thm)],[t696,t113]) ).
cnf(t224,plain,
suc(suc(zero)) = x(zero,suc(suc(zero))),
inference(rw,[status(thm)],[t697]) ).
cnf(t225,plain,
x(zero,suc(suc(zero))) = suc(suc(zero)),
inference(orient,[status(thm)],[t224]) ).
cnf(t229,plain,
x(suc(zero),suc(suc(zero))) = suc(double(suc(suc(zero)))),
inference(cp,[status(thm)],[t226,t225]) ).
cnf(t422,plain,
x(suc(zero),suc(suc(zero))) = suc(double(suc(suc(zero)))),
inference(orient,[status(thm)],[t229]) ).
cnf(t726,plain,
suc(double(suc(suc(zero)))) = double(suc(suc(suc(zero)))),
inference(step,[status(thm)],[t725,t422]) ).
cnf(t604,plain,
double(suc(suc(suc(zero)))) = suc(double(suc(suc(zero)))),
inference(orient,[status(thm)],[t726]) ).
cnf(t733,plain,
evenNat(suc(double(suc(suc(zero))))) = true,
inference(step,[status(thm)],[t494,t604]) ).
cnf(t734,plain,
false = true,
inference(step,[status(thm)],[t733,t288]) ).
cnf(t610,plain,
false = true,
inference(rw,[status(thm)],[t734]) ).
cnf(t611,plain,
false = true,
inference(orient,[status(thm)],[t610]) ).
fof(f2,axiom,
! [X,X2] : nil != cons(X,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_003) ).
fof(f2_nnf,plain,
! [X,X2] : nil != cons(X,X2),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,X2] : nil != cons(X,X2),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
nil != cons(X0,X1),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f4,axiom,
! [X] : zero != suc(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(f4_nnf,plain,
! [X] : zero != suc(X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : zero != suc(X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
zero != suc(X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f5,axiom,
i != o,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
fof(f5_nnf,plain,
i != o,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
i != o,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
i != o,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c4,c5,c10]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t611]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 23:41:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.16/1.21 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.16/1.21 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------