%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX224+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:10 PM UTC 2026
% Result : Theorem 66.74s 8.86s
% Output : Proof 66.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 21
% Syntax : Number of formulae : 132 ( 116 unt; 0 def)
% Number of atoms : 170 ( 124 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 120 ( 82 ~; 24 |; 9 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-4 aty)
% Number of variables : 308 ( 58 sgn 128 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,conjecture,
? [E] : tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_032) ).
fof(f31_neg,negated_conjecture,
~ ? [E] : tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f31_nnf,plain,
! [E] : ~ tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
inference(nnf_transformation,[status(thm)],[f31_neg]) ).
fof(f31_sk,plain,
! [E] : ~ tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c35,plain,
~ tc(nil,X0,arr(arr(a,arr(a,b)),arr(a,b))),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t158,plain,
ifeq(tc(nil,X1,arr(arr(a,arr(a,b)),arr(a,b))),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t315,plain,
ifeq(tc(nil,X1,arr(arr(a,arr(a,b)),arr(a,b))),true,false,true) = true,
inference(orient,[status(thm)],[t158]) ).
fof(f28,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
fof(f28_nnf,plain,
! [X,E,Tx2,T1] :
( ( ~ tc(cons(Tx2,X),E,T1)
| tc(X,lam(E),arr(Tx2,T1)) )
& ( tc(cons(Tx2,X),E,T1)
| ~ tc(X,lam(E),arr(Tx2,T1)) ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,E,Tx2,T1] :
( ( ~ tc(cons(Tx2,X),E,T1)
| tc(X,lam(E),arr(Tx2,T1)) )
& ( tc(cons(Tx2,X),E,T1)
| ~ tc(X,lam(E),arr(Tx2,T1)) ) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c31,plain,
( ~ tc(cons(X2,X0),X1,X3)
| tc(X0,lam(X1),arr(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t157,plain,
ifeq(tc(cons(X1,X2),X3,X4),true,tc(X2,lam(X3),arr(X1,X4)),true) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t310,plain,
ifeq(tc(cons(X1,X2),X3,X4),true,tc(X2,lam(X3),arr(X1,X4)),true) = true,
inference(orient,[status(thm)],[t157]) ).
fof(f26,axiom,
! [X,Z,F,X2,Tx] :
( tc(X,app(F,X2,Tx),Z)
<=> ( tc(X,X2,Tx)
& tc(X,F,arr(Tx,Z)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_027) ).
fof(f26_nnf,plain,
! [X,Z,F,X2,Tx] :
( ( ~ tc(X,X2,Tx)
| ~ tc(X,F,arr(Tx,Z))
| tc(X,app(F,X2,Tx),Z) )
& ( ( tc(X,X2,Tx)
& tc(X,F,arr(Tx,Z)) )
| ~ tc(X,app(F,X2,Tx),Z) ) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X,F,X2,Tx,Z] :
( ( ~ tc(X,X2,Tx)
| ~ tc(X,F,arr(Tx,Z))
| tc(X,app(F,X2,Tx),Z) )
& ( ( tc(X,X2,Tx)
& tc(X,F,arr(Tx,Z)) )
| ~ tc(X,app(F,X2,Tx),Z) ) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c28,plain,
( ~ tc(X0,X3,X4)
| ~ tc(X0,X2,arr(X4,X1))
| tc(X0,app(X2,X3,X4),X1) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t208,plain,
ifeq(tc(X1,X2,arr(X3,X4)),true,ifeq(tc(X1,X5,X3),true,tc(X1,app(X2,X5,X3),X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t283,plain,
ifeq(tc(X1,X2,arr(X3,X4)),true,ifeq(tc(X1,X5,X3),true,tc(X1,app(X2,X5,X3),X4),true),true) = true,
inference(orient,[status(thm)],[t208]) ).
fof(f30,axiom,
! [X,Z,X3,Tx3] :
( index(X,X3) = just(Tx3)
=> ( tc(X,var(X3),Z)
<=> Tx3 = Z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
fof(f30_nnf,plain,
! [X,Z,X3,Tx3] :
( ( ( Tx3 != Z
| tc(X,var(X3),Z) )
& ( Tx3 = Z
| ~ tc(X,var(X3),Z) ) )
| index(X,X3) != just(Tx3) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X,X3,Tx3,Z] :
( ( ( Tx3 != Z
| tc(X,var(X3),Z) )
& ( Tx3 = Z
| ~ tc(X,var(X3),Z) ) )
| index(X,X3) != just(Tx3) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c34,plain,
( X3 != X1
| tc(X0,var(X2),X1)
| index(X0,X2) != just(X3) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(hi21,axiom,
ifeq(index(X0,X1),just(X2),ifeq(X2,X3,tc(X0,var(X1),X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c34]) ).
fof(f24,axiom,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_025) ).
fof(f24_nnf,plain,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
index(cons(X0,X1),zero) = just(X0),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi12,axiom,
index(cons(X0,X1),zero) = just(X0),
inference(equality_encoding,[status(esa)],[c24]) ).
fof(f11,axiom,
! [X] : proj1Suc(suc(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
fof(f11_nnf,plain,
! [X] : proj1Suc(suc(X)) = X,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : proj1Suc(suc(X)) = X,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
proj1Suc(suc(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi4,axiom,
proj1Suc(suc(X0)) = X0,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t59,plain,
tc(cons(X1,X2),var(zero),proj1Suc(suc(X1))) = true,
inference(hyper_resolution,[status(thm)],[hi21,hi12,hi4]) ).
cnf(t4,plain,
proj1Suc(suc(X1)) = X1,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t256,plain,
proj1Suc(suc(X1)) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t31255,plain,
tc(cons(X1,X2),var(zero),X1) = true,
inference(step,[status(thm)],[t59,t256]) ).
cnf(t275,plain,
tc(cons(X1,X2),var(zero),X1) = true,
inference(orient,[status(thm)],[t31255]) ).
cnf(t292,plain,
true = ifeq(tc(cons(X1,X2),X3,arr(X1,X4)),true,ifeq(true,true,tc(cons(X1,X2),app(X3,var(zero),X1),X4),true),true),
inference(cp,[status(thm)],[t283,t275]) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t264,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t31334,plain,
true = ifeq(tc(cons(X1,X2),X3,arr(X1,X4)),true,tc(cons(X1,X2),app(X3,var(zero),X1),X4),true),
inference(step,[status(thm)],[t292,t264]) ).
cnf(t1467,plain,
ifeq(tc(cons(X1,X2),X3,arr(X1,X4)),true,tc(cons(X1,X2),app(X3,var(zero),X1),X4),true) = true,
inference(orient,[status(thm)],[t31334]) ).
cnf(t153,plain,
ifeq(index(X1,X2),just(X3),ifeq(X3,X4,tc(X1,var(X2),X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t317,plain,
ifeq(index(X1,X2),just(X3),ifeq(X3,X4,tc(X1,var(X2),X4),true),true) = true,
inference(orient,[status(thm)],[t153]) ).
cnf(t318,plain,
true = ifeq(index(X1,X2),just(X3),tc(X1,var(X2),X3),true),
inference(cp,[status(thm)],[t317,t264]) ).
cnf(t355,plain,
ifeq(index(X1,X2),just(X3),tc(X1,var(X2),X3),true) = true,
inference(orient,[status(thm)],[t318]) ).
fof(f25,axiom,
! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_026) ).
fof(f25_nnf,plain,
! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
index(cons(X0,X1),suc(X2)) = index(X1,X2),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t45,plain,
index(cons(X1,X2),suc(X3)) = index(X2,X3),
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t339,plain,
index(cons(X1,X2),suc(X3)) = index(X2,X3),
inference(orient,[status(thm)],[t45]) ).
cnf(t357,plain,
true = ifeq(index(X1,X2),just(X3),tc(cons(X4,X1),var(suc(X2)),X3),true),
inference(cp,[status(thm)],[t355,t339]) ).
cnf(t394,plain,
ifeq(index(X1,X2),just(X3),tc(cons(X4,X1),var(suc(X2)),X3),true) = true,
inference(orient,[status(thm)],[t357]) ).
cnf(t20,plain,
index(cons(X1,X2),zero) = just(X1),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t331,plain,
index(cons(X1,X2),zero) = just(X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t395,plain,
true = ifeq(just(X1),just(X2),tc(cons(X3,cons(X1,X4)),var(suc(zero)),X2),true),
inference(cp,[status(thm)],[t394,t331]) ).
cnf(t436,plain,
ifeq(just(X1),just(X2),tc(cons(X3,cons(X1,X4)),var(suc(zero)),X2),true) = true,
inference(orient,[status(thm)],[t395]) ).
cnf(t437,plain,
true = tc(cons(X1,cons(X2,X3)),var(suc(zero)),X2),
inference(cp,[status(thm)],[t436,t264]) ).
cnf(t438,plain,
tc(cons(X1,cons(X2,X3)),var(suc(zero)),X2) = true,
inference(orient,[status(thm)],[t437]) ).
cnf(t1485,plain,
true = ifeq(true,true,tc(cons(X1,cons(arr(X1,X2),X3)),app(var(suc(zero)),var(zero),X1),X2),true),
inference(cp,[status(thm)],[t1467,t438]) ).
cnf(t31338,plain,
true = tc(cons(X1,cons(arr(X1,X2),X3)),app(var(suc(zero)),var(zero),X1),X2),
inference(step,[status(thm)],[t1485,t264]) ).
cnf(t1560,plain,
tc(cons(X1,cons(arr(X1,X2),X3)),app(var(suc(zero)),var(zero),X1),X2) = true,
inference(orient,[status(thm)],[t31338]) ).
cnf(t1565,plain,
true = ifeq(true,true,tc(cons(X1,cons(arr(X1,arr(X1,X2)),X3)),app(app(var(suc(zero)),var(zero),X1),var(zero),X1),X2),true),
inference(cp,[status(thm)],[t1467,t1560]) ).
cnf(t31508,plain,
true = tc(cons(X1,cons(arr(X1,arr(X1,X2)),X3)),app(app(var(suc(zero)),var(zero),X1),var(zero),X1),X2),
inference(step,[status(thm)],[t1565,t264]) ).
cnf(t5429,plain,
tc(cons(X1,cons(arr(X1,arr(X1,X2)),X3)),app(app(var(suc(zero)),var(zero),X1),var(zero),X1),X2) = true,
inference(orient,[status(thm)],[t31508]) ).
cnf(t5430,plain,
true = ifeq(true,true,tc(cons(arr(X1,arr(X1,X2)),X3),lam(app(app(var(suc(zero)),var(zero),X1),var(zero),X1)),arr(X1,X2)),true),
inference(cp,[status(thm)],[t310,t5429]) ).
cnf(t31731,plain,
true = tc(cons(arr(X1,arr(X1,X2)),X3),lam(app(app(var(suc(zero)),var(zero),X1),var(zero),X1)),arr(X1,X2)),
inference(step,[status(thm)],[t5430,t264]) ).
cnf(t12585,plain,
tc(cons(arr(X1,arr(X1,X2)),X3),lam(app(app(var(suc(zero)),var(zero),X1),var(zero),X1)),arr(X1,X2)) = true,
inference(orient,[status(thm)],[t31731]) ).
cnf(t12586,plain,
true = ifeq(true,true,tc(X1,lam(lam(app(app(var(suc(zero)),var(zero),X2),var(zero),X2))),arr(arr(X2,arr(X2,X3)),arr(X2,X3))),true),
inference(cp,[status(thm)],[t310,t12585]) ).
cnf(t32142,plain,
true = tc(X1,lam(lam(app(app(var(suc(zero)),var(zero),X2),var(zero),X2))),arr(arr(X2,arr(X2,X3)),arr(X2,X3))),
inference(step,[status(thm)],[t12586,t264]) ).
cnf(t31170,plain,
tc(X1,lam(lam(app(app(var(suc(zero)),var(zero),X2),var(zero),X2))),arr(arr(X2,arr(X2,X3)),arr(X2,X3))) = true,
inference(orient,[status(thm)],[t32142]) ).
cnf(t31183,plain,
true = ifeq(true,true,false,true),
inference(cp,[status(thm)],[t315,t31170]) ).
cnf(t32143,plain,
true = false,
inference(step,[status(thm)],[t31183,t264]) ).
cnf(t31206,plain,
false = true,
inference(orient,[status(thm)],[t32143]) ).
fof(f2,axiom,
! [X,X2] : nil != cons(X,X2),
file('/export/starexec/sandbox2/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(f5,axiom,
! [X,X2] : arr(X,X2) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_006) ).
fof(f5_nnf,plain,
! [X,X2] : arr(X,X2) != a,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,X2] : arr(X,X2) != a,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
arr(X0,X1) != a,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f6,axiom,
! [X,X2] : arr(X,X2) != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
fof(f6_nnf,plain,
! [X,X2] : arr(X,X2) != b,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,X2] : arr(X,X2) != b,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
arr(X0,X1) != b,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f7,axiom,
! [X,X2] : arr(X,X2) != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
fof(f7_nnf,plain,
! [X,X2] : arr(X,X2) != c,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,X2] : arr(X,X2) != c,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
arr(X0,X1) != c,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f8,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
fof(f8_nnf,plain,
a != b,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
a != b,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
a != b,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f9,axiom,
a != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
fof(f9_nnf,plain,
a != c,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
a != c,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
a != c,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f10,axiom,
b != c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
fof(f10_nnf,plain,
b != c,
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
b != c,
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
b != c,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f12,axiom,
! [X] : zero != suc(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
fof(f12_nnf,plain,
! [X] : zero != suc(X),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] : zero != suc(X),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero != suc(X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f14,axiom,
! [X] : nothing != just(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
fof(f14_nnf,plain,
! [X] : nothing != just(X),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X] : nothing != just(X),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
nothing != just(X0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f20,axiom,
! [X,X2,X3,X4] : app(X,X2,X3) != lam(X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
fof(f20_nnf,plain,
! [X,X2,X3,X4] : app(X,X2,X3) != lam(X4),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,X2,X3,X4] : app(X,X2,X3) != lam(X4),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
app(X0,X1,X2) != lam(X3),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f21,axiom,
! [X,X2,X3,X4] : app(X,X2,X3) != var(X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
fof(f21_nnf,plain,
! [X,X2,X3,X4] : app(X,X2,X3) != var(X4),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X,X2,X3,X4] : app(X,X2,X3) != var(X4),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
app(X0,X1,X2) != var(X3),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f22,axiom,
! [X,X2] : lam(X) != var(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
fof(f22_nnf,plain,
! [X,X2] : lam(X) != var(X2),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X,X2] : lam(X) != var(X2),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
lam(X0) != var(X1),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f29,axiom,
! [X,Z,X3] :
( index(X,X3) = nothing
=> ~ tc(X,var(X3),Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
fof(f29_nnf,plain,
! [X,Z,X3] :
( ~ tc(X,var(X3),Z)
| index(X,X3) != nothing ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,X3,Z] :
( ~ tc(X,var(X3),Z)
| index(X,X3) != nothing ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c32,plain,
( ~ tc(X0,var(X2),X1)
| index(X0,X2) != nothing ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c5,c6,c7,c8,c9,c10,c12,c14,c20,c21,c22,c32,c35]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t31206]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX224+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n015.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:47:27 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 66.74/8.86 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.74/8.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------