%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.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:44 PM UTC 2026
% Result : Unsatisfiable 78.90s 46.58s
% Output : CNFRefutation 79.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of clauses : 79 ( 79 unt; 0 nHn; 20 RR)
% Number of literals : 79 ( 78 equ; 8 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-4 aty)
% Number of variables : 134 ( 34 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal,negated_conjecture,
eq2(prop_koen(X1,X2,X3),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
cnf(axiom_079,axiom,
prop_koen(X1,X2,X3) = eq2(rec(y(X1,X2),X3),rec(y(X2,X1),X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_079) ).
cnf(axiom_073,axiom,
step(y(X1,X2),X3) = aux2(X3,X1,X2,eps2(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_073) ).
cnf(axiom_077,axiom,
rec(X1,nil) = eps2(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_077) ).
cnf(axiom_070,axiom,
eps2(atom(X1)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_070) ).
cnf(axiom_067,axiom,
eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_067) ).
cnf(axiom_069,axiom,
eps2(nil2) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_069) ).
cnf(axiom_065,axiom,
eps2(eps) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
cnf(axiom_078,axiom,
rec(X1,cons(X2,X3)) = rec(step(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_078) ).
cnf(axiom_003,axiom,
aux2(X1,X2,X3,bfalse) = x(y(step(X2,X1),X3),nil2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_003) ).
cnf(axiom_071,axiom,
step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_083,axiom,
eq(b,c) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_083) ).
cnf(axiom_001,axiom,
aux(X1,X2,bfalse) = nil2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_001) ).
cnf(axiom_066,axiom,
eps2(x(X1,X2)) = orb(eps2(X1),eps2(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_066) ).
cnf(axiom_064,axiom,
andb(bfalse,X1) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_064) ).
cnf(axiom_072,axiom,
step(x(X1,X2),X3) = x(step(X1,X3),step(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_072) ).
cnf(axiom_075,axiom,
step(nil2,X1) = nil2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_075) ).
cnf(axiom_062,axiom,
orb(bfalse,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_062) ).
cnf(axiom_002,axiom,
aux2(X1,X2,X3,btrue) = x(y(step(X2,X1),X3),step(X3,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_002) ).
cnf(axiom_076,axiom,
step(eps,X1) = nil2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_076) ).
cnf(axiom_088,axiom,
eq(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_088) ).
cnf(axiom,axiom,
aux(X1,X2,btrue) = eps,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom) ).
cnf(axiom_061,axiom,
orb(btrue,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_061) ).
cnf(axiom_087,axiom,
eq2(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_087) ).
cnf(axiom_089,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_089) ).
cnf(c_0_25,negated_conjecture,
eq2(prop_koen(X1,X2,X3),bfalse) != btrue,
goal ).
cnf(c_0_26,axiom,
prop_koen(X1,X2,X3) = eq2(rec(y(X1,X2),X3),rec(y(X2,X1),X3)),
axiom_079 ).
cnf(c_0_27,axiom,
step(y(X1,X2),X3) = aux2(X3,X1,X2,eps2(X1)),
axiom_073 ).
cnf(c_0_28,axiom,
rec(X1,nil) = eps2(X1),
axiom_077 ).
cnf(c_0_29,axiom,
eps2(atom(X1)) = bfalse,
axiom_070 ).
cnf(c_0_30,axiom,
eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)),
axiom_067 ).
cnf(c_0_31,axiom,
eps2(nil2) = bfalse,
axiom_069 ).
cnf(c_0_32,axiom,
eps2(eps) = btrue,
axiom_065 ).
cnf(c_0_33,negated_conjecture,
eq2(eq2(rec(y(X1,X2),X3),rec(y(X2,X1),X3)),bfalse) != btrue,
inference(rw,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_34,axiom,
rec(X1,cons(X2,X3)) = rec(step(X1,X2),X3),
axiom_078 ).
cnf(c_0_35,plain,
step(y(X1,X2),X3) = aux2(X3,X1,X2,rec(X1,nil)),
inference(rw,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_36,plain,
rec(atom(X1),nil) = bfalse,
inference(rw,[status(thm)],[c_0_29,c_0_28]) ).
cnf(c_0_37,axiom,
aux2(X1,X2,X3,bfalse) = x(y(step(X2,X1),X3),nil2),
axiom_003 ).
cnf(c_0_38,axiom,
step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)),
axiom_071 ).
cnf(c_0_39,axiom,
eq(b,c) = bfalse,
axiom_083 ).
cnf(c_0_40,axiom,
aux(X1,X2,bfalse) = nil2,
axiom_001 ).
cnf(c_0_41,axiom,
eps2(x(X1,X2)) = orb(eps2(X1),eps2(X2)),
axiom_066 ).
cnf(c_0_42,plain,
rec(y(X1,X2),nil) = andb(rec(X1,nil),rec(X2,nil)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30,c_0_28]),c_0_28]),c_0_28]) ).
cnf(c_0_43,plain,
rec(nil2,nil) = bfalse,
inference(rw,[status(thm)],[c_0_31,c_0_28]) ).
cnf(c_0_44,axiom,
andb(bfalse,X1) = bfalse,
axiom_064 ).
cnf(c_0_45,plain,
rec(eps,nil) = btrue,
inference(rw,[status(thm)],[c_0_32,c_0_28]) ).
cnf(c_0_46,negated_conjecture,
eq2(eq2(rec(step(y(X1,X2),X3),X4),rec(step(y(X2,X1),X3),X4)),bfalse) != btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_34]),c_0_34]) ).
cnf(c_0_47,plain,
x(y(step(atom(X1),X2),X3),nil2) = step(y(atom(X1),X3),X2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_37]) ).
cnf(c_0_48,plain,
step(atom(b),c) = nil2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40]) ).
cnf(c_0_49,axiom,
step(x(X1,X2),X3) = x(step(X1,X3),step(X2,X3)),
axiom_072 ).
cnf(c_0_50,axiom,
step(nil2,X1) = nil2,
axiom_075 ).
cnf(c_0_51,plain,
rec(x(X1,X2),nil) = orb(rec(X1,nil),rec(X2,nil)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41,c_0_28]),c_0_28]),c_0_28]) ).
cnf(c_0_52,plain,
rec(y(nil2,X1),nil) = bfalse,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_44]) ).
cnf(c_0_53,axiom,
orb(bfalse,X1) = X1,
axiom_062 ).
cnf(c_0_54,axiom,
aux2(X1,X2,X3,btrue) = x(y(step(X2,X1),X3),step(X3,X1)),
axiom_002 ).
cnf(c_0_55,axiom,
step(eps,X1) = nil2,
axiom_076 ).
cnf(c_0_56,plain,
aux2(X1,eps,X2,btrue) = step(y(eps,X2),X1),
inference(spm,[status(thm)],[c_0_35,c_0_45]) ).
cnf(c_0_57,negated_conjecture,
eq2(eq2(rec(step(step(y(X1,X2),X3),X4),X5),rec(step(step(y(X2,X1),X3),X4),X5)),bfalse) != btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_34]),c_0_34]) ).
cnf(c_0_58,plain,
step(y(atom(b),X1),c) = x(y(nil2,X1),nil2),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_59,plain,
step(x(X1,nil2),X2) = x(step(X1,X2),nil2),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_60,plain,
step(y(nil2,X1),X2) = x(y(nil2,X1),nil2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_43]),c_0_37]),c_0_50]) ).
cnf(c_0_61,plain,
rec(x(y(nil2,X1),X2),nil) = rec(X2,nil),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_53]) ).
cnf(c_0_62,axiom,
eq(X1,X1) = btrue,
axiom_088 ).
cnf(c_0_63,axiom,
aux(X1,X2,btrue) = eps,
axiom ).
cnf(c_0_64,plain,
x(y(nil2,X1),step(X1,X2)) = step(y(eps,X1),X2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56]) ).
cnf(c_0_65,negated_conjecture,
eq2(eq2(rec(step(step(y(X1,atom(b)),c),X2),X3),rec(x(x(y(nil2,X1),nil2),nil2),X3)),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_59]),c_0_60]) ).
cnf(c_0_66,plain,
rec(x(x(y(nil2,X1),X2),X3),nil) = rec(x(X2,X3),nil),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_61]),c_0_51]) ).
cnf(c_0_67,plain,
rec(x(nil2,X1),nil) = rec(X1,nil),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_43]),c_0_53]) ).
cnf(c_0_68,plain,
step(atom(X1),X1) = eps,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_62]),c_0_63]) ).
cnf(c_0_69,plain,
rec(step(y(eps,X1),X2),nil) = rec(step(X1,X2),nil),
inference(spm,[status(thm)],[c_0_61,c_0_64]) ).
cnf(c_0_70,negated_conjecture,
eq2(eq2(rec(step(step(y(X1,atom(b)),c),X2),nil),bfalse),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_66]),c_0_67]),c_0_43]) ).
cnf(c_0_71,plain,
step(y(atom(X1),X2),X1) = x(y(eps,X2),nil2),
inference(spm,[status(thm)],[c_0_47,c_0_68]) ).
cnf(c_0_72,plain,
rec(x(step(y(eps,X1),X2),X3),nil) = rec(x(step(X1,X2),X3),nil),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_69]),c_0_51]) ).
cnf(c_0_73,axiom,
orb(btrue,X1) = btrue,
axiom_061 ).
cnf(c_0_74,negated_conjecture,
eq2(eq2(rec(x(step(atom(b),X1),nil2),nil),bfalse),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70,c_0_71]),c_0_59]),c_0_72]) ).
cnf(c_0_75,plain,
rec(x(eps,X1),nil) = btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_45]),c_0_73]) ).
cnf(c_0_76,axiom,
eq2(btrue,bfalse) = bfalse,
axiom_087 ).
cnf(c_0_77,axiom,
eq2(X1,X1) = btrue,
axiom_089 ).
cnf(c_0_78,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_68]),c_0_75]),c_0_76]),c_0_77])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n005.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 07:57:00 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 78.90/46.58 % Version : CSE_E---1.7
% 78.90/46.58 % Problem : theBenchmark.p
% 78.90/46.58 % SZS status Unsatisfiable for theBenchmark.p
% 78.90/46.58 % SZS output start CNFRefutation
% See solution above
% 79.09/46.76 % Total time : 40.290s
%------------------------------------------------------------------------------