%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n022.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:57 PM UTC 2026
% Result : Unsatisfiable 1.03s 1.45s
% Output : CNFRefutation 1.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 25
% Syntax : Number of formulae : 63 ( 62 unt; 0 def)
% Number of atoms : 65 ( 64 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 : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 8 con; 0-2 aty)
% Number of variables : 45 ( 8 sgn 2 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
eq2(sat_comm(X,Y),bfalse) != btrue,
file('theBenchmark.p',goal) ).
fof(e,plain,
! [X,Y] :
( true != false
& eq0(X,X) = true
& eq0(eq2(sat_comm(X,Y),bfalse),btrue) = false ),
inference(encode_existential,[status(esa)],[g0]) ).
cnf(g1,plain,
true != false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c1,axiom,
notb(btrue) = bfalse,
file('theBenchmark.p',axiom_002) ).
cnf(c2,axiom,
notb(bfalse) = btrue,
file('theBenchmark.p',axiom_003) ).
cnf(c3,axiom,
half(zero) = zero,
file('theBenchmark.p',axiom_004) ).
cnf(c4,axiom,
evenNat(zero) = btrue,
file('theBenchmark.p',axiom_007) ).
cnf(c5,axiom,
shw(zero) = nil,
file('theBenchmark.p',axiom_009) ).
cnf(c6,axiom,
rd(nil) = zero,
file('theBenchmark.p',axiom_016) ).
cnf(c7,plain,
eq0(X,X) = true,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c9,axiom,
eq2(X,X) = btrue,
file('theBenchmark.p',axiom_029) ).
cnf(c11,axiom,
addNat(zero,X) = X,
file('theBenchmark.p',axiom_013) ).
cnf(c12,axiom,
append(nil,X) = X,
file('theBenchmark.p',axiom_011) ).
cnf(c13,axiom,
double(X) = addNat(X,X),
file('theBenchmark.p',axiom_015) ).
cnf(c18,axiom,
half(suc(zero)) = zero,
file('theBenchmark.p',axiom_005) ).
cnf(c19,axiom,
evenNat(suc(X)) = notb(evenNat(X)),
file('theBenchmark.p',axiom_008) ).
cnf(c20,plain,
notb(evenNat(X)) = evenNat(suc(X)),
inference(equational,[status(thm)],[c19]) ).
cnf(c21,plain,
bfalse = evenNat(suc(zero)),
inference(equational,[status(thm)],[c1,c4,c20]) ).
cnf(c22,axiom,
eq(zero,suc(X)) = bfalse,
file('theBenchmark.p',axiom_026) ).
cnf(c23,plain,
eq(zero,suc(X)) = evenNat(suc(zero)),
inference(equational,[status(thm)],[c21,c22]) ).
cnf(c26,axiom,
rd(cons(o,X)) = double(rd(X)),
file('theBenchmark.p',axiom_018) ).
cnf(c27,plain,
rd(cons(o,X)) = addNat(rd(X),rd(X)),
inference(equational,[status(thm)],[c13,c26]) ).
cnf(c28,axiom,
half(suc(suc(X))) = suc(half(X)),
file('theBenchmark.p',axiom_006) ).
cnf(c29,axiom,
addNat(suc(X),Y) = suc(addNat(X,Y)),
file('theBenchmark.p',axiom_014) ).
cnf(c30,axiom,
rd(cons(i,X)) = suc(double(rd(X))),
file('theBenchmark.p',axiom_017) ).
cnf(c31,plain,
rd(cons(i,X)) = suc(addNat(rd(X),rd(X))),
inference(equational,[status(thm)],[c13,c30]) ).
cnf(c32,plain,
evenNat(suc(suc(zero))) = btrue,
inference(equational,[status(thm)],[c2,c20,c21]) ).
cnf(c33,axiom,
eq(suc(X),suc(Y)) = eq(X,Y),
file('theBenchmark.p',axiom_025) ).
cnf(c34,axiom,
shw(suc(X)) = aux(X,evenNat(suc(X))),
file('theBenchmark.p',axiom_010) ).
cnf(c35,plain,
aux(X,evenNat(suc(X))) = shw(suc(X)),
inference(equational,[status(thm)],[c34]) ).
cnf(c36,axiom,
append(cons(X,Y),Z) = cons(X,append(Y,Z)),
file('theBenchmark.p',axiom_012) ).
cnf(c37,axiom,
x(X,Y) = rd(append(shw(X),shw(Y))),
file('theBenchmark.p',axiom_019) ).
cnf(c38,axiom,
aux(X,btrue) = cons(o,shw(half(suc(X)))),
file('theBenchmark.p',axiom) ).
cnf(c39,axiom,
aux(X,bfalse) = cons(i,shw(half(suc(X)))),
file('theBenchmark.p',axiom_001) ).
cnf(c40,plain,
aux(X,evenNat(suc(zero))) = cons(i,shw(half(suc(X)))),
inference(equational,[status(thm)],[c21,c39]) ).
cnf(c41,plain,
shw(suc(zero)) = cons(i,nil),
inference(equational,[status(thm)],[c5,c18,c35,c40]) ).
cnf(c42,plain,
cons(o,cons(i,nil)) = shw(suc(suc(zero))),
inference(equational,[status(thm)],[c3,c28,c32,c35,c38,c41]) ).
cnf(c45,plain,
eq0(eq2(sat_comm(X,Y),bfalse),btrue) = false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c46,plain,
eq0(eq2(sat_comm(X,Y),evenNat(suc(zero))),btrue) = false,
inference(equational,[status(thm)],[c21,c45]) ).
cnf(c47,axiom,
sat_comm(X,Y) = eq(x(X,Y),x(Y,X)),
file('theBenchmark.p',axiom_020) ).
cnf(c48,plain,
sat_comm(X,Y) = eq(rd(append(shw(X),shw(Y))),rd(append(shw(Y),shw(X)))),
inference(equational,[status(thm)],[c37,c47]) ).
cnf(c49,plain,
evenNat(suc(suc(suc(zero)))) = evenNat(suc(zero)),
inference(equational,[status(thm)],[c1,c20,c21,c32]) ).
cnf(c50,plain,
rd(shw(suc(suc(zero)))) = suc(suc(zero)),
inference(equational,[status(thm)],[c6,c11,c27,c29,c31,c42]) ).
cnf(c51,plain,
shw(suc(suc(suc(zero)))) = cons(i,cons(i,nil)),
inference(equational,[status(thm)],[c18,c28,c35,c40,c41,c49]) ).
cnf(c52,plain,
evenNat(suc(suc(suc(suc(zero))))) = btrue,
inference(equational,[status(thm)],[c20,c32,c49]) ).
cnf(c53,plain,
append(shw(suc(suc(zero))),X) = cons(o,cons(i,X)),
inference(equational,[status(thm)],[c12,c36,c42]) ).
cnf(c55,plain,
evenNat(suc(suc(suc(suc(suc(zero)))))) = evenNat(suc(zero)),
inference(equational,[status(thm)],[c1,c20,c21,c52]) ).
cnf(c56,plain,
evenNat(suc(suc(suc(suc(suc(suc(zero))))))) = btrue,
inference(equational,[status(thm)],[c20,c32,c55]) ).
cnf(c58,plain,
shw(suc(suc(suc(suc(suc(zero)))))) = cons(i,shw(suc(suc(zero)))),
inference(equational,[status(thm)],[c18,c28,c35,c40,c55]) ).
cnf(c60,plain,
cons(o,cons(i,cons(i,nil))) = shw(suc(suc(suc(suc(suc(suc(zero))))))),
inference(equational,[status(thm)],[c3,c28,c35,c38,c51,c56]) ).
cnf(c61,plain,
evenNat(suc(suc(suc(suc(suc(suc(suc(zero)))))))) = evenNat(suc(zero)),
inference(equational,[status(thm)],[c1,c20,c21,c56]) ).
cnf(c62,plain,
evenNat(suc(suc(suc(suc(suc(suc(suc(suc(zero))))))))) = btrue,
inference(equational,[status(thm)],[c20,c32,c61]) ).
cnf(c64,plain,
rd(shw(suc(suc(suc(suc(suc(suc(zero)))))))) = suc(suc(suc(suc(suc(suc(zero)))))),
inference(equational,[status(thm)],[c6,c11,c27,c29,c31,c60]) ).
cnf(c66,plain,
evenNat(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))) = evenNat(suc(zero)),
inference(equational,[status(thm)],[c1,c20,c21,c62]) ).
cnf(c68,plain,
evenNat(suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero))))))))))) = btrue,
inference(equational,[status(thm)],[c20,c32,c66]) ).
cnf(c71,plain,
eq0(eq2(eq(rd(append(shw(X),shw(Y))),rd(append(shw(Y),shw(X)))),evenNat(suc(zero))),btrue) = false,
inference(equational,[status(thm)],[c46,c48]) ).
cnf(c77,plain,
cons(o,cons(i,shw(suc(suc(zero))))) = shw(suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero))))))))))),
inference(equational,[status(thm)],[c3,c28,c35,c38,c58,c68]) ).
cnf(c80,plain,
rd(shw(suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))))) = suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))),
inference(equational,[status(thm)],[c11,c27,c29,c31,c50,c77]) ).
cnf(c81,plain,
append(shw(suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero))))))))))),X) = cons(o,cons(i,cons(o,cons(i,X)))),
inference(equational,[status(thm)],[c36,c53,c77]) ).
cnf(c82,plain,
eq0(eq2(eq(suc(addNat(rd(shw(X)),rd(shw(X)))),rd(append(shw(X),cons(i,nil)))),evenNat(suc(zero))),btrue) = false,
inference(equational,[status(thm)],[c12,c31,c36,c41,c71]) ).
cnf(c83,plain,
true = false,
inference(equational,[status(thm)],[c7,c9,c11,c23,c27,c29,c31,c33,c60,c64,c80,c81,c82]) ).
cnf(g2,plain,
true = false,
inference(equational,[status(thm)],[c83]) ).
cnf(g3,plain,
$false,
inference(resolution,[status(thm)],[g1,g2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217-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 : n022.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 12:16:35 EDT 2026
% 0.15/0.33 % CPUTime :
% 1.03/1.45 % SZS status Unsatisfiable
% 1.03/1.45 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------