%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n016.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 07:07:59 PM UTC 2026
% Result : Unsatisfiable 87.17s 86.82s
% Output : CNFRefutation 87.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 17
% Syntax : Number of formulae : 41 ( 40 unt; 0 def)
% Number of atoms : 43 ( 42 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 5 ( 3 ~; 0 |; 2 &)
% ( 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 : 22 ( 22 usr; 6 con; 0-4 aty)
% Number of variables : 64 ( 14 sgn 2 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
eq2(prop_same(X,Y),bfalse) != btrue,
file('theBenchmark.p',goal) ).
fof(e,plain,
! [X,Y] :
( true != false
& eq0(X,X) = true
& eq0(eq2(prop_same(X,Y),bfalse),btrue) = false ),
inference(encode_existential,[status(esa)],[g0]) ).
cnf(g1,plain,
true != false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c2,axiom,
notb(btrue) = bfalse,
file('theBenchmark.p',axiom_071) ).
cnf(c4,axiom,
eps2(eps) = btrue,
file('theBenchmark.p',axiom_075) ).
cnf(c6,axiom,
eq(X,X) = btrue,
file('theBenchmark.p',axiom_110) ).
cnf(c7,plain,
eq0(X,X) = true,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c8,axiom,
eq2(X,X) = btrue,
file('theBenchmark.p',axiom_111) ).
cnf(c11,axiom,
andb(btrue,X) = X,
file('theBenchmark.p',axiom_073) ).
cnf(c20,axiom,
eps2(star(X)) = btrue,
file('theBenchmark.p',axiom_078) ).
cnf(c26,axiom,
eq2(btrue,bfalse) = bfalse,
file('theBenchmark.p',axiom_109) ).
cnf(c32,axiom,
rec(X,nil2) = eps2(X),
file('theBenchmark.p',axiom_087) ).
cnf(c37,axiom,
aux(X,Y,btrue) = eps,
file('theBenchmark.p',axiom) ).
cnf(c51,axiom,
aux3(X,Y,Z,bfalse) = bfalse,
file('theBenchmark.p',axiom_005) ).
cnf(c77,axiom,
eps2(y(X,Y)) = andb(eps2(X),eps2(Y)),
file('theBenchmark.p',axiom_077) ).
cnf(c78,plain,
andb(eps2(X),eps2(Y)) = eps2(y(X,Y)),
inference(equational,[status(thm)],[c77]) ).
cnf(c80,plain,
eps2(y(eps,X)) = eps2(X),
inference(equational,[status(thm)],[c4,c11,c78]) ).
cnf(c84,axiom,
rec(X,cons2(Y,Z)) = rec(step(X,Y),Z),
file('theBenchmark.p',axiom_088) ).
cnf(c85,plain,
rec(step(X,Y),Z) = rec(X,cons2(Y,Z)),
inference(equational,[status(thm)],[c84]) ).
cnf(c115,plain,
rec(X,cons2(Y,nil2)) = eps2(step(X,Y)),
inference(equational,[status(thm)],[c32,c85]) ).
cnf(c120,plain,
eps2(y(X,star(Y))) = andb(eps2(X),btrue),
inference(equational,[status(thm)],[c20,c78]) ).
cnf(c126,axiom,
step(atom(X),Y) = aux(Y,X,eq(X,Y)),
file('theBenchmark.p',axiom_081) ).
cnf(c127,plain,
aux(X,Y,eq(Y,X)) = step(atom(Y),X),
inference(equational,[status(thm)],[c126]) ).
cnf(c128,plain,
step(atom(X),X) = eps,
inference(equational,[status(thm)],[c6,c37,c127]) ).
cnf(c136,axiom,
step(star(X),Y) = y(step(X,Y),star(X)),
file('theBenchmark.p',axiom_084) ).
cnf(c137,plain,
y(step(X,Y),star(X)) = step(star(X),Y),
inference(equational,[status(thm)],[c136]) ).
cnf(c185,plain,
eq0(eq2(prop_same(X,Y),bfalse),btrue) = false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c200,axiom,
prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)),
file('theBenchmark.p',axiom_101) ).
cnf(c201,plain,
eq2(rec(X,Y),reck2(X,Y)) = prop_same(X,Y),
inference(equational,[status(thm)],[c200]) ).
cnf(c212,plain,
y(eps,star(atom(X))) = step(star(atom(X)),X),
inference(equational,[status(thm)],[c128,c137]) ).
cnf(c314,axiom,
reck2(star(X),cons2(Y,Z)) = aux3(X,Y,Z,notb(eps2(X))),
file('theBenchmark.p',axiom_100) ).
cnf(c315,plain,
aux3(X,Y,Z,notb(eps2(X))) = reck2(star(X),cons2(Y,Z)),
inference(equational,[status(thm)],[c314]) ).
cnf(c317,plain,
reck2(star(star(X)),cons2(Y,Z)) = bfalse,
inference(equational,[status(thm)],[c2,c20,c51,c315]) ).
cnf(c369,plain,
andb(eps2(step(X,Y)),btrue) = eps2(step(star(X),Y)),
inference(equational,[status(thm)],[c120,c137]) ).
cnf(c538,plain,
eps2(step(star(star(atom(X))),X)) = btrue,
inference(equational,[status(thm)],[c11,c20,c80,c212,c369]) ).
cnf(c4109,plain,
eq2(rec(star(star(X)),cons2(Y,Z)),bfalse) = prop_same(star(star(X)),cons2(Y,Z)),
inference(equational,[status(thm)],[c201,c317]) ).
cnf(c4110,plain,
eq2(eps2(step(star(star(X)),Y)),bfalse) = prop_same(star(star(X)),cons2(Y,nil2)),
inference(equational,[status(thm)],[c115,c4109]) ).
cnf(c4113,plain,
prop_same(star(star(atom(X))),cons2(X,nil2)) = bfalse,
inference(equational,[status(thm)],[c26,c538,c4110]) ).
cnf(c4114,plain,
true = false,
inference(equational,[status(thm)],[c7,c8,c185,c4113]) ).
cnf(g2,plain,
true = false,
inference(equational,[status(thm)],[c4114]) ).
cnf(g3,plain,
$false,
inference(resolution,[status(thm)],[g1,g2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_Leo-III %s %d THM
% 0.15/0.33 % Computer : n016.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 13:20:51 EDT 2026
% 0.15/0.33 % CPUTime :
% 87.17/86.82 % SZS status Unsatisfiable
% 87.17/86.82 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------