%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n003.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:55 PM UTC 2026
% Result : Unsatisfiable 149.89s 149.70s
% Output : CNFRefutation 149.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 25
% Syntax : Number of formulae : 74 ( 73 unt; 0 def)
% Number of atoms : 76 ( 75 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 5 ( 3 ~; 0 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-3 aty)
% Number of variables : 137 ( 14 sgn 1 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
eq2(psorted_rev(X),bfalse) != btrue,
file('theBenchmark.p',goal) ).
fof(e,plain,
! [X] :
( true != false
& eq0(X,X) = true
& eq0(eq2(psorted_rev(X),bfalse),btrue) = false ),
inference(encode_existential,[status(esa)],[g0]) ).
cnf(g1,plain,
true != false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c1,axiom,
lengthNat(nil) = z,
file('theBenchmark.p',axiom_007) ).
cnf(c2,axiom,
unique(nil) = btrue,
file('theBenchmark.p',axiom_013) ).
cnf(c3,axiom,
rev(nil) = nil,
file('theBenchmark.p',axiom_017) ).
cnf(c6,axiom,
eq2(X,X) = btrue,
file('theBenchmark.p',axiom_031) ).
cnf(c7,plain,
eq0(X,X) = true,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c8,axiom,
orb(bfalse,X) = X,
file('theBenchmark.p',axiom_003) ).
cnf(c9,axiom,
impl(btrue,X) = X,
file('theBenchmark.p',axiom_009) ).
cnf(c10,axiom,
andb(btrue,X) = X,
file('theBenchmark.p',axiom_019) ).
cnf(c11,axiom,
append(nil,X) = X,
file('theBenchmark.p',axiom_015) ).
cnf(c13,axiom,
elemNat(X,nil) = bfalse,
file('theBenchmark.p',axiom_011) ).
cnf(c16,axiom,
leqNat(z,X) = btrue,
file('theBenchmark.p',axiom_004) ).
cnf(c18,axiom,
eq2(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_025) ).
cnf(c20,axiom,
eq(s(X),z) = bfalse,
file('theBenchmark.p',axiom_029) ).
cnf(c22,axiom,
sorted(cons(X,nil)) = btrue,
file('theBenchmark.p',axiom_022) ).
cnf(c23,axiom,
leqNat(s(X),z) = bfalse,
file('theBenchmark.p',axiom_005) ).
cnf(c24,axiom,
aux(X,Y,bfalse) = unique(Y),
file('theBenchmark.p',axiom_001) ).
cnf(c25,axiom,
lengthNat(cons(X,Y)) = s(lengthNat(Y)),
file('theBenchmark.p',axiom_008) ).
cnf(c26,axiom,
eq(s(X),s(Y)) = eq(X,Y),
file('theBenchmark.p',axiom_027) ).
cnf(c27,axiom,
leqNat(s(X),s(Y)) = leqNat(X,Y),
file('theBenchmark.p',axiom_006) ).
cnf(c28,axiom,
append(cons(X,Y),Z) = cons(X,append(Y,Z)),
file('theBenchmark.p',axiom_016) ).
cnf(c29,plain,
cons(X,append(Y,Z)) = append(cons(X,Y),Z),
inference(equational,[status(thm)],[c28]) ).
cnf(c30,plain,
append(cons(X,nil),Y) = cons(X,Y),
inference(equational,[status(thm)],[c11,c29]) ).
cnf(c31,plain,
eq0(eq2(psorted_rev(X),bfalse),btrue) = false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c32,axiom,
unique(cons(X,Y)) = aux(X,Y,elemNat(X,Y)),
file('theBenchmark.p',axiom_014) ).
cnf(c33,plain,
aux(X,Y,elemNat(X,Y)) = unique(cons(X,Y)),
inference(equational,[status(thm)],[c32]) ).
cnf(c34,plain,
unique(cons(X,nil)) = btrue,
inference(equational,[status(thm)],[c2,c13,c24,c33]) ).
cnf(c35,axiom,
rev(cons(X,Y)) = append(rev(Y),cons(X,nil)),
file('theBenchmark.p',axiom_018) ).
cnf(c36,plain,
append(rev(X),cons(Y,nil)) = rev(cons(Y,X)),
inference(equational,[status(thm)],[c35]) ).
cnf(c37,plain,
rev(cons(X,nil)) = cons(X,nil),
inference(equational,[status(thm)],[c3,c11,c36]) ).
cnf(c39,axiom,
elemNat(X,cons(Y,Z)) = orb(eq(X,Y),elemNat(X,Z)),
file('theBenchmark.p',axiom_012) ).
cnf(c40,plain,
orb(eq(X,Y),elemNat(X,Z)) = elemNat(X,cons(Y,Z)),
inference(equational,[status(thm)],[c39]) ).
cnf(c42,plain,
elemNat(X,cons(Y,nil)) = orb(eq(X,Y),bfalse),
inference(equational,[status(thm)],[c13,c40]) ).
cnf(c45,plain,
elemNat(s(X),cons(z,Y)) = elemNat(s(X),Y),
inference(equational,[status(thm)],[c8,c20,c40]) ).
cnf(c47,plain,
rev(cons(X,cons(Y,nil))) = cons(Y,cons(X,nil)),
inference(equational,[status(thm)],[c30,c36,c37]) ).
cnf(c49,axiom,
sorted(cons(X,cons(Y,Z))) = andb(leqNat(X,Y),sorted(cons(Y,Z))),
file('theBenchmark.p',axiom_023) ).
cnf(c50,plain,
andb(leqNat(X,Y),sorted(cons(Y,Z))) = sorted(cons(X,cons(Y,Z))),
inference(equational,[status(thm)],[c49]) ).
cnf(c51,plain,
sorted(cons(z,cons(X,Y))) = sorted(cons(X,Y)),
inference(equational,[status(thm)],[c10,c16,c50]) ).
cnf(c52,plain,
sorted(cons(X,cons(Y,nil))) = andb(leqNat(X,Y),btrue),
inference(equational,[status(thm)],[c22,c50]) ).
cnf(c54,plain,
append(cons(X,cons(Y,nil)),Z) = cons(X,cons(Y,Z)),
inference(equational,[status(thm)],[c29,c30]) ).
cnf(c57,plain,
orb(eq(X,Y),elemNat(s(X),Z)) = elemNat(s(X),cons(s(Y),Z)),
inference(equational,[status(thm)],[c26,c40]) ).
cnf(c64,plain,
elemNat(s(X),cons(Y,cons(z,Z))) = elemNat(s(X),cons(Y,Z)),
inference(equational,[status(thm)],[c40,c45]) ).
cnf(c69,plain,
andb(leqNat(X,Y),sorted(cons(s(Y),Z))) = sorted(cons(s(X),cons(s(Y),Z))),
inference(equational,[status(thm)],[c27,c50]) ).
cnf(c70,plain,
sorted(cons(s(z),cons(s(X),Y))) = sorted(cons(s(X),Y)),
inference(equational,[status(thm)],[c10,c16,c69]) ).
cnf(c74,plain,
orb(eq(X,Y),orb(eq(X,Z),bfalse)) = elemNat(X,cons(Y,cons(Z,nil))),
inference(equational,[status(thm)],[c40,c42]) ).
cnf(c78,plain,
andb(leqNat(X,Y),andb(leqNat(Y,Z),btrue)) = sorted(cons(X,cons(Y,cons(Z,nil)))),
inference(equational,[status(thm)],[c50,c52]) ).
cnf(c80,plain,
append(cons(X,cons(Y,cons(Z,nil))),W) = cons(X,cons(Y,cons(Z,W))),
inference(equational,[status(thm)],[c29,c54]) ).
cnf(c83,plain,
aux(X,cons(Y,nil),orb(eq(X,Y),bfalse)) = unique(cons(X,cons(Y,nil))),
inference(equational,[status(thm)],[c33,c42]) ).
cnf(c84,plain,
unique(cons(s(X),cons(z,nil))) = btrue,
inference(equational,[status(thm)],[c8,c20,c24,c34,c83]) ).
cnf(c85,plain,
rev(cons(X,cons(Y,cons(Z,nil)))) = cons(Z,cons(Y,cons(X,nil))),
inference(equational,[status(thm)],[c36,c47,c54]) ).
cnf(c94,plain,
orb(eq(X,Y),orb(eq(s(X),Z),bfalse)) = elemNat(s(X),cons(s(Y),cons(Z,nil))),
inference(equational,[status(thm)],[c42,c57]) ).
cnf(c104,plain,
elemNat(s(X),cons(s(Y),cons(s(Z),nil))) = elemNat(X,cons(Y,cons(Z,nil))),
inference(equational,[status(thm)],[c26,c74,c94]) ).
cnf(c105,plain,
elemNat(s(X),cons(Y,cons(Z,cons(z,W)))) = elemNat(s(X),cons(Y,cons(Z,W))),
inference(equational,[status(thm)],[c40,c64]) ).
cnf(c109,plain,
andb(leqNat(X,Y),andb(leqNat(s(Y),Z),btrue)) = sorted(cons(s(X),cons(s(Y),cons(Z,nil)))),
inference(equational,[status(thm)],[c52,c69]) ).
cnf(c121,plain,
rev(cons(X,cons(Y,cons(Z,cons(W,nil))))) = cons(W,cons(Z,cons(Y,cons(X,nil)))),
inference(equational,[status(thm)],[c36,c80,c85]) ).
cnf(c123,plain,
sorted(cons(s(X),cons(s(Y),cons(s(Z),nil)))) = sorted(cons(X,cons(Y,cons(Z,nil)))),
inference(equational,[status(thm)],[c27,c78,c109]) ).
cnf(c210,plain,
aux(s(X),cons(Y,cons(z,Z)),elemNat(s(X),cons(Y,Z))) = unique(cons(s(X),cons(Y,cons(z,Z)))),
inference(equational,[status(thm)],[c33,c64]) ).
cnf(c237,plain,
aux(s(X),cons(Y,cons(z,nil)),orb(eq(s(X),Y),bfalse)) = unique(cons(s(X),cons(Y,cons(z,nil)))),
inference(equational,[status(thm)],[c42,c210]) ).
cnf(c313,plain,
aux(s(X),cons(s(Y),cons(z,nil)),orb(eq(X,Y),bfalse)) = unique(cons(s(X),cons(s(Y),cons(z,nil)))),
inference(equational,[status(thm)],[c26,c237]) ).
cnf(c314,plain,
unique(cons(s(s(X)),cons(s(z),cons(z,nil)))) = btrue,
inference(equational,[status(thm)],[c8,c20,c24,c84,c313]) ).
cnf(c400,axiom,
psorted_rev(X) = impl(eq2(sorted(rev(X)),btrue),impl(eq2(unique(X),btrue),eq2(leqNat(lengthNat(X),s(s(s(z)))),btrue))),
file('theBenchmark.p',axiom_024) ).
cnf(c401,plain,
impl(eq2(sorted(rev(X)),btrue),impl(eq2(unique(X),btrue),eq2(leqNat(lengthNat(X),s(s(s(z)))),btrue))) = psorted_rev(X),
inference(equational,[status(thm)],[c400]) ).
cnf(c785,plain,
aux(s(X),cons(Y,cons(Z,cons(z,W))),elemNat(s(X),cons(Y,cons(Z,W)))) = unique(cons(s(X),cons(Y,cons(Z,cons(z,W))))),
inference(equational,[status(thm)],[c33,c105]) ).
cnf(c1268,plain,
impl(eq2(sorted(rev(cons(X,Y))),btrue),impl(eq2(unique(cons(X,Y)),btrue),eq2(leqNat(lengthNat(Y),s(s(z))),btrue))) = psorted_rev(cons(X,Y)),
inference(equational,[status(thm)],[c25,c27,c401]) ).
cnf(c1422,plain,
aux(s(X),cons(s(Y),cons(s(Z),cons(z,nil))),elemNat(X,cons(Y,cons(Z,nil)))) = unique(cons(s(X),cons(s(Y),cons(s(Z),cons(z,nil))))),
inference(equational,[status(thm)],[c104,c785]) ).
cnf(c2124,plain,
aux(s(s(X)),cons(s(Y),cons(s(z),cons(z,nil))),orb(eq(s(X),Y),bfalse)) = unique(cons(s(s(X)),cons(s(Y),cons(s(z),cons(z,nil))))),
inference(equational,[status(thm)],[c42,c64,c1422]) ).
cnf(c2707,plain,
aux(s(s(X)),cons(s(s(Y)),cons(s(z),cons(z,nil))),orb(eq(X,Y),bfalse)) = unique(cons(s(s(X)),cons(s(s(Y)),cons(s(z),cons(z,nil))))),
inference(equational,[status(thm)],[c26,c2124]) ).
cnf(c2708,plain,
unique(cons(s(s(s(X))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = btrue,
inference(equational,[status(thm)],[c8,c20,c24,c314,c2707]) ).
cnf(c2711,plain,
psorted_rev(cons(s(s(s(X))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = bfalse,
inference(equational,[status(thm)],[c1,c6,c9,c18,c22,c23,c25,c27,c51,c70,c121,c123,c1268,c2708]) ).
cnf(c2712,plain,
true = false,
inference(equational,[status(thm)],[c6,c7,c31,c2711]) ).
cnf(g2,plain,
true = false,
inference(equational,[status(thm)],[c2712]) ).
cnf(g3,plain,
$false,
inference(resolution,[status(thm)],[g1,g2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : run_Leo-III %s %d THM
% 0.15/0.34 % Computer : n003.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 11:27:41 EDT 2026
% 0.15/0.34 % CPUTime :
% 149.89/149.70 % SZS status Unsatisfiable
% 149.89/149.70 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------