%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX222-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 : Unsatisfiable 6.09s 1.30s
% Output : Proof 6.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 14
% Syntax : Number of formulae : 95 ( 95 unt; 0 def)
% Number of atoms : 95 ( 94 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 8 con; 0-4 aty)
% Number of variables : 137 ( 22 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f55,negated_conjecture,
eq4(sat_synth_nf_k(X),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f55_nnf,plain,
! [X] : eq4(sat_synth_nf_k(X),bfalse) != btrue,
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [X] : eq4(sat_synth_nf_k(X),bfalse) != btrue,
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
eq4(sat_synth_nf_k(X0),bfalse) != btrue,
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(t31,plain,
eqq(eq4(sat_synth_nf_k(X1),bfalse),btrue) = efalse,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t422,plain,
eqq(eq4(sat_synth_nf_k(X1),bfalse),btrue) = efalse,
inference(orient,[status(thm)],[t31]) ).
cnf(f20,axiom,
sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
fof(f20_nnf,plain,
! [X] : sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X] : sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
sat_synth_nf_k(X0) = notb(andb(nf(X0),tc(nil,X0,arr(a,arr(b,b))))),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t90,plain,
notb(andb(nf(X1),tc(nil,X1,arr(a,arr(b,b))))) = sat_synth_nf_k(X1),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t414,plain,
notb(andb(nf(X1),tc(nil,X1,arr(a,arr(b,b))))) = sat_synth_nf_k(X1),
inference(orient,[status(thm)],[t90]) ).
cnf(f12,axiom,
nf(lam(E)) = nf(E),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(f12_nnf,plain,
! [E] : nf(lam(E)) = nf(E),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [E] : nf(lam(E)) = nf(E),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
nf(lam(X0)) = nf(X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t18,plain,
nf(lam(X1)) = nf(X1),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t392,plain,
nf(lam(X1)) = nf(X1),
inference(orient,[status(thm)],[t18]) ).
cnf(t419,plain,
sat_synth_nf_k(lam(X1)) = notb(andb(nf(X1),tc(nil,lam(X1),arr(a,arr(b,b))))),
inference(cp,[status(thm)],[t414,t392]) ).
cnf(f15,axiom,
tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
fof(f15_nnf,plain,
! [X,E,Tx2,T1] : tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X,E,Tx2,T1] : tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
tc(X0,lam(X1),arr(X2,X3)) = tc(cons(X2,X0),X1,X3),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t71,plain,
tc(X1,lam(X2),arr(X3,X4)) = tc(cons(X3,X1),X2,X4),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t405,plain,
tc(X1,lam(X2),arr(X3,X4)) = tc(cons(X3,X1),X2,X4),
inference(orient,[status(thm)],[t71]) ).
cnf(t527,plain,
sat_synth_nf_k(lam(X1)) = notb(andb(nf(X1),tc(cons(a,nil),X1,arr(b,b)))),
inference(step,[status(thm)],[t419,t405]) ).
cnf(t457,plain,
notb(andb(nf(X1),tc(cons(a,nil),X1,arr(b,b)))) = sat_synth_nf_k(lam(X1)),
inference(orient,[status(thm)],[t527]) ).
cnf(t462,plain,
sat_synth_nf_k(lam(lam(X1))) = notb(andb(nf(X1),tc(cons(a,nil),lam(X1),arr(b,b)))),
inference(cp,[status(thm)],[t457,t392]) ).
cnf(t540,plain,
sat_synth_nf_k(lam(lam(X1))) = notb(andb(nf(X1),tc(cons(b,cons(a,nil)),X1,b))),
inference(step,[status(thm)],[t462,t405]) ).
cnf(t486,plain,
notb(andb(nf(X1),tc(cons(b,cons(a,nil)),X1,b))) = sat_synth_nf_k(lam(lam(X1))),
inference(orient,[status(thm)],[t540]) ).
cnf(f19,axiom,
tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(f19_nnf,plain,
! [X,X3,Z] : tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X,X3,Z] : tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
tc(X0,var(X1),X2) = aux(X0,X2,X1,index(X0,X1)),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t54,plain,
aux(X1,X2,X3,index(X1,X3)) = tc(X1,var(X3),X2),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t404,plain,
aux(X1,X2,X3,index(X1,X3)) = tc(X1,var(X3),X2),
inference(orient,[status(thm)],[t54]) ).
cnf(f5,axiom,
index(cons(Z,Xs),zero) = just(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(f5_nnf,plain,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
index(cons(X0,X1),zero) = just(X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t32,plain,
index(cons(X1,X2),zero) = just(X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t410,plain,
index(cons(X1,X2),zero) = just(X1),
inference(orient,[status(thm)],[t32]) ).
cnf(t411,plain,
tc(cons(X1,X2),var(zero),X3) = aux(cons(X1,X2),X3,zero,just(X1)),
inference(cp,[status(thm)],[t404,t410]) ).
cnf(f1,axiom,
aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_001) ).
fof(f1_nnf,plain,
! [X,Z,X3,Tx3] : aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Z,X3,Tx3] : aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
aux(X0,X1,X2,just(X3)) = eq(X3,X1),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t45,plain,
aux(X1,X2,X3,just(X4)) = eq(X4,X2),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t390,plain,
aux(X1,X2,X3,just(X4)) = eq(X4,X2),
inference(orient,[status(thm)],[t45]) ).
cnf(t521,plain,
tc(cons(X1,X2),var(zero),X3) = eq(X1,X3),
inference(step,[status(thm)],[t411,t390]) ).
cnf(t431,plain,
tc(cons(X1,X2),var(zero),X3) = eq(X1,X3),
inference(orient,[status(thm)],[t521]) ).
cnf(t493,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(nf(var(zero)),eq(b,b))),
inference(cp,[status(thm)],[t486,t431]) ).
cnf(f13,axiom,
nf(var(X4)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_013) ).
fof(f13_nnf,plain,
! [X4] : nf(var(X4)) = btrue,
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X4] : nf(var(X4)) = btrue,
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
nf(var(X0)) = btrue,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t17,plain,
nf(var(X1)) = btrue,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t395,plain,
nf(var(X1)) = btrue,
inference(orient,[status(thm)],[t17]) ).
cnf(t541,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(andb(btrue,eq(b,b))),
inference(step,[status(thm)],[t493,t395]) ).
cnf(f7,axiom,
andb(btrue,Q) = Q,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
fof(f7_nnf,plain,
! [Q] : andb(btrue,Q) = Q,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Q] : andb(btrue,Q) = Q,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
andb(btrue,X0) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t3,plain,
andb(btrue,X1) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t247,plain,
andb(btrue,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t542,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(eq(b,b)),
inference(step,[status(thm)],[t541,t247]) ).
cnf(f51,axiom,
eq(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_051) ).
fof(f51_nnf,plain,
! [X] : eq(X,X) = btrue,
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [X] : eq(X,X) = btrue,
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
eq(X0,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t4,plain,
eq(X1,X1) = btrue,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t391,plain,
eq(X1,X1) = btrue,
inference(orient,[status(thm)],[t4]) ).
cnf(t543,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = notb(btrue),
inference(step,[status(thm)],[t542,t391]) ).
cnf(f2,axiom,
notb(btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
fof(f2_nnf,plain,
notb(btrue) = bfalse,
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
notb(btrue) = bfalse,
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(t1,plain,
notb(btrue) = bfalse,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t383,plain,
notb(btrue) = bfalse,
inference(orient,[status(thm)],[t1]) ).
cnf(t544,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = bfalse,
inference(step,[status(thm)],[t543,t383]) ).
cnf(t495,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = bfalse,
inference(orient,[status(thm)],[t544]) ).
cnf(t496,plain,
efalse = eqq(eq4(bfalse,bfalse),btrue),
inference(cp,[status(thm)],[t422,t495]) ).
cnf(f54,axiom,
eq4(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_054) ).
fof(f54_nnf,plain,
! [X] : eq4(X,X) = btrue,
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [X] : eq4(X,X) = btrue,
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
eq4(X0,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(t12,plain,
eq4(X1,X1) = btrue,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t398,plain,
eq4(X1,X1) = btrue,
inference(orient,[status(thm)],[t12]) ).
cnf(t545,plain,
efalse = eqq(btrue,btrue),
inference(step,[status(thm)],[t496,t398]) ).
cnf(t15,plain,
eqq(X1,X1) = etrue,
introduced(definition) ).
cnf(t421,plain,
eqq(X1,X1) = etrue,
inference(orient,[status(thm)],[t15]) ).
cnf(t546,plain,
efalse = etrue,
inference(step,[status(thm)],[t545,t421]) ).
cnf(t497,plain,
efalse = etrue,
inference(orient,[status(thm)],[t546]) ).
cnf(goal_0,negated_conjecture,
etrue != efalse,
introduced(definition) ).
cnf(g0_0,plain,
etrue != etrue,
inference(rw,[status(thm)],[goal_0,t497]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX222-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.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 23:43:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.09/1.30 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.09/1.30 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------