%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:34:48 PM UTC 2026
% Result : Unsatisfiable 1.73s 1.86s
% Output : CNFRefutation 1.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 24
% Syntax : Number of clauses : 70 ( 70 unt; 0 nHn; 16 RR)
% Number of literals : 70 ( 69 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-4 aty)
% Number of variables : 106 ( 31 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_076,axiom,
eps2(x(X1,X2)) = orb(eps2(X1),eps2(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_076) ).
cnf(axiom_087,axiom,
rec(X1,nil2) = eps2(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_087) ).
cnf(axiom_075,axiom,
eps2(eps) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_075) ).
cnf(axiom_077,axiom,
eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_077) ).
cnf(axiom_100,axiom,
reck2(star(X1),cons2(X2,X3)) = aux3(X1,X2,X3,notb(eps2(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_100) ).
cnf(axiom_067,axiom,
orb(btrue,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_067) ).
cnf(axiom_078,axiom,
eps2(star(X1)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_078) ).
cnf(axiom_079,axiom,
eps2(nil4) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_079) ).
cnf(goal,negated_conjecture,
eq2(prop_same(X1,X2),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
cnf(axiom_101,axiom,
prop_same(X1,X2) = eq2(rec(X1,X2),reck2(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_101) ).
cnf(axiom_071,axiom,
notb(btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_005,axiom,
aux3(X1,X2,X3,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
cnf(axiom_068,axiom,
orb(bfalse,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_068) ).
cnf(axiom_088,axiom,
rec(X1,cons2(X2,X3)) = rec(step(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_088) ).
cnf(axiom_084,axiom,
step(star(X1),X2) = y(step(X1,X2),star(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_084) ).
cnf(axiom_082,axiom,
step(x(X1,X2),X3) = x(step(X1,X3),step(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_082) ).
cnf(axiom_086,axiom,
step(eps,X1) = nil4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_086) ).
cnf(axiom_081,axiom,
step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_081) ).
cnf(axiom_095,axiom,
reck2(atom(X1),cons2(X2,nil2)) = eq(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_095) ).
cnf(axiom_110,axiom,
eq(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
cnf(axiom,axiom,
aux(X1,X2,btrue) = eps,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom) ).
cnf(axiom_073,axiom,
andb(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_073) ).
cnf(axiom_109,axiom,
eq2(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_109) ).
cnf(axiom_111,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_111) ).
cnf(c_0_24,axiom,
eps2(x(X1,X2)) = orb(eps2(X1),eps2(X2)),
axiom_076 ).
cnf(c_0_25,axiom,
rec(X1,nil2) = eps2(X1),
axiom_087 ).
cnf(c_0_26,axiom,
eps2(eps) = btrue,
axiom_075 ).
cnf(c_0_27,axiom,
eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)),
axiom_077 ).
cnf(c_0_28,axiom,
reck2(star(X1),cons2(X2,X3)) = aux3(X1,X2,X3,notb(eps2(X1))),
axiom_100 ).
cnf(c_0_29,plain,
rec(x(X1,X2),nil2) = orb(rec(X1,nil2),rec(X2,nil2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_24,c_0_25]),c_0_25]),c_0_25]) ).
cnf(c_0_30,plain,
rec(eps,nil2) = btrue,
inference(rw,[status(thm)],[c_0_26,c_0_25]) ).
cnf(c_0_31,axiom,
orb(btrue,X1) = btrue,
axiom_067 ).
cnf(c_0_32,axiom,
eps2(star(X1)) = btrue,
axiom_078 ).
cnf(c_0_33,plain,
rec(y(X1,X2),nil2) = andb(rec(X1,nil2),rec(X2,nil2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_25]),c_0_25]),c_0_25]) ).
cnf(c_0_34,axiom,
eps2(nil4) = bfalse,
axiom_079 ).
cnf(c_0_35,negated_conjecture,
eq2(prop_same(X1,X2),bfalse) != btrue,
goal ).
cnf(c_0_36,axiom,
prop_same(X1,X2) = eq2(rec(X1,X2),reck2(X1,X2)),
axiom_101 ).
cnf(c_0_37,plain,
reck2(star(X1),cons2(X2,X3)) = aux3(X1,X2,X3,notb(rec(X1,nil2))),
inference(rw,[status(thm)],[c_0_28,c_0_25]) ).
cnf(c_0_38,plain,
rec(x(eps,X1),nil2) = btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31]) ).
cnf(c_0_39,axiom,
notb(btrue) = bfalse,
axiom_071 ).
cnf(c_0_40,axiom,
aux3(X1,X2,X3,bfalse) = bfalse,
axiom_005 ).
cnf(c_0_41,plain,
rec(star(X1),nil2) = btrue,
inference(rw,[status(thm)],[c_0_32,c_0_25]) ).
cnf(c_0_42,plain,
andb(rec(X1,nil2),btrue) = rec(y(X1,eps),nil2),
inference(spm,[status(thm)],[c_0_33,c_0_30]) ).
cnf(c_0_43,plain,
rec(nil4,nil2) = bfalse,
inference(rw,[status(thm)],[c_0_34,c_0_25]) ).
cnf(c_0_44,axiom,
orb(bfalse,X1) = X1,
axiom_068 ).
cnf(c_0_45,negated_conjecture,
eq2(eq2(rec(X1,X2),reck2(X1,X2)),bfalse) != btrue,
inference(rw,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_46,plain,
reck2(star(x(eps,X1)),cons2(X2,X3)) = bfalse,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_39]),c_0_40]) ).
cnf(c_0_47,axiom,
rec(X1,cons2(X2,X3)) = rec(step(X1,X2),X3),
axiom_088 ).
cnf(c_0_48,plain,
rec(y(X1,star(X2)),nil2) = rec(y(X1,eps),nil2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_41]),c_0_42]) ).
cnf(c_0_49,axiom,
step(star(X1),X2) = y(step(X1,X2),star(X1)),
axiom_084 ).
cnf(c_0_50,axiom,
step(x(X1,X2),X3) = x(step(X1,X3),step(X2,X3)),
axiom_082 ).
cnf(c_0_51,axiom,
step(eps,X1) = nil4,
axiom_086 ).
cnf(c_0_52,plain,
rec(x(nil4,X1),nil2) = rec(X1,nil2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_43]),c_0_44]) ).
cnf(c_0_53,axiom,
step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)),
axiom_081 ).
cnf(c_0_54,axiom,
reck2(atom(X1),cons2(X2,nil2)) = eq(X1,X2),
axiom_095 ).
cnf(c_0_55,axiom,
eq(X1,X1) = btrue,
axiom_110 ).
cnf(c_0_56,negated_conjecture,
eq2(eq2(rec(step(star(x(eps,X1)),X2),X3),bfalse),bfalse) != btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47]) ).
cnf(c_0_57,plain,
rec(step(star(X1),X2),nil2) = rec(y(step(X1,X2),eps),nil2),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
cnf(c_0_58,plain,
step(x(eps,X1),X2) = x(nil4,step(X1,X2)),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_59,plain,
rec(y(x(nil4,X1),X2),nil2) = rec(y(X1,X2),nil2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_52]),c_0_33]) ).
cnf(c_0_60,plain,
step(atom(X1),X2) = aux(X2,X1,reck2(atom(X1),cons2(X2,nil2))),
inference(rw,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_61,plain,
reck2(atom(X1),cons2(X1,nil2)) = btrue,
inference(rw,[status(thm)],[c_0_55,c_0_54]) ).
cnf(c_0_62,axiom,
aux(X1,X2,btrue) = eps,
axiom ).
cnf(c_0_63,axiom,
andb(btrue,X1) = X1,
axiom_073 ).
cnf(c_0_64,negated_conjecture,
eq2(eq2(rec(y(step(X1,X2),eps),nil2),bfalse),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_58]),c_0_59]) ).
cnf(c_0_65,plain,
step(atom(X1),X1) = eps,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_61]),c_0_62]) ).
cnf(c_0_66,plain,
rec(y(eps,X1),nil2) = rec(X1,nil2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_30]),c_0_63]) ).
cnf(c_0_67,axiom,
eq2(btrue,bfalse) = bfalse,
axiom_109 ).
cnf(c_0_68,axiom,
eq2(X1,X1) = btrue,
axiom_111 ).
cnf(c_0_69,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_66]),c_0_30]),c_0_67]),c_0_68])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n017.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 08:00:57 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.73/1.86 % Version : CSE_E---1.7
% 1.73/1.86 % Problem : theBenchmark.p
% 1.73/1.86 % SZS status Unsatisfiable for theBenchmark.p
% 1.73/1.86 % SZS output start CNFRefutation
% See solution above
% 1.73/1.86 % Total time : 1.372s
%------------------------------------------------------------------------------