%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX203+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:13:25 PM UTC 2026
% Result : Theorem 0.12s 0.42s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 36
% Syntax : Number of formulae : 184 ( 50 unt; 18 def)
% Number of atoms : 609 ( 167 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 708 ( 283 ~; 383 |; 16 &)
% ( 22 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 19 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 290 ( 288 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : proj1S(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : z != s(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Y] : leqNat(z,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Z] : ~ leqNat(s(Z),z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Z,M] :
( leqNat(s(Z),s(M))
<=> leqNat(Z,M) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y] : sorted(cons(Y,nil)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Y,Y2,Xs] :
( sorted(cons(Y,cons(Y2,Xs)))
<=> ( sorted(cons(Y2,Xs))
& leqNat(Y,Y2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
lengthNat(nil) = z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Y,Xs] : lengthNat(cons(Y,Xs)) = s(lengthNat(Xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : ~ elemNat(X,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Z,Xs] :
( elemNat(X,cons(Z,Xs))
<=> ( elemNat(X,Xs)
| X = Z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
unique(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [Y,Xs] :
( unique(cons(Y,Xs))
<=> ( unique(Xs)
& ~ elemNat(Y,Xs) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Y] : append(nil,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
rev(nil) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Y,Xs] : rev(cons(Y,Xs)) = append(rev(Xs),cons(Y,nil)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,conjecture,
? [Xs] :
~ ( sorted(rev(Xs))
=> ( unique(Xs)
=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ ? [Xs] :
~ ( sorted(rev(Xs))
=> ( unique(Xs)
=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
fof(f27,plain,
! [X0] : proj1S(s(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f28,plain,
! [X0] : z != s(X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f29,plain,
! [X0] : leqNat(z,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f30,plain,
! [X0] : ~ leqNat(s(X0),z),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f31,plain,
! [Z,M] :
( ( ~ leqNat(Z,M)
| leqNat(s(Z),s(M)) )
& ( leqNat(Z,M)
| ~ leqNat(s(Z),s(M)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f32,plain,
( ! [Z,M] :
( ~ leqNat(Z,M)
| leqNat(s(Z),s(M)) )
& ! [Z,M] :
( leqNat(Z,M)
| ~ leqNat(s(Z),s(M)) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( leqNat(X0,X1)
| ~ leqNat(s(X0),s(X1)) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f36,plain,
! [X0] : sorted(cons(X0,nil)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f37,plain,
! [Y,Y2,Xs] :
( ( ~ sorted(cons(Y2,Xs))
| ~ leqNat(Y,Y2)
| sorted(cons(Y,cons(Y2,Xs))) )
& ( ( sorted(cons(Y2,Xs))
& leqNat(Y,Y2) )
| ~ sorted(cons(Y,cons(Y2,Xs))) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f38,plain,
( ! [Y,Y2,Xs] :
( ~ sorted(cons(Y2,Xs))
| ~ leqNat(Y,Y2)
| sorted(cons(Y,cons(Y2,Xs))) )
& ! [Y,Y2,Xs] :
( ( sorted(cons(Y2,Xs))
& leqNat(Y,Y2) )
| ~ sorted(cons(Y,cons(Y2,Xs))) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ~ sorted(cons(X1,X2))
| ~ leqNat(X0,X1)
| sorted(cons(X0,cons(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f42,plain,
lengthNat(nil) = z,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1] : lengthNat(cons(X0,X1)) = s(lengthNat(X1)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f44,plain,
! [X0] : ~ elemNat(X0,nil),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f45,plain,
! [X,Z,Xs] :
( ( ( ~ elemNat(X,Xs)
& X != Z )
| elemNat(X,cons(Z,Xs)) )
& ( elemNat(X,Xs)
| X = Z
| ~ elemNat(X,cons(Z,Xs)) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f46,plain,
( ! [X,Z,Xs] :
( ( ~ elemNat(X,Xs)
& X != Z )
| elemNat(X,cons(Z,Xs)) )
& ! [X,Z,Xs] :
( elemNat(X,Xs)
| X = Z
| ~ elemNat(X,cons(Z,Xs)) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0,X1,X2] :
( elemNat(X0,X2)
| X0 = X1
| ~ elemNat(X0,cons(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
unique(nil),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f51,plain,
! [Y,Xs] :
( ( ~ unique(Xs)
| elemNat(Y,Xs)
| unique(cons(Y,Xs)) )
& ( ( unique(Xs)
& ~ elemNat(Y,Xs) )
| ~ unique(cons(Y,Xs)) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f52,plain,
( ! [Y,Xs] :
( ~ unique(Xs)
| elemNat(Y,Xs)
| unique(cons(Y,Xs)) )
& ! [Y,Xs] :
( ( unique(Xs)
& ~ elemNat(Y,Xs) )
| ~ unique(cons(Y,Xs)) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f55,plain,
! [X0,X1] :
( ~ unique(X1)
| elemNat(X0,X1)
| unique(cons(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f57,plain,
! [X0,X1,X2] : append(cons(X0,X1),X2) = cons(X0,append(X1,X2)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f58,plain,
rev(nil) = nil,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f59,plain,
! [X0,X1] : rev(cons(X0,X1)) = append(rev(X1),cons(X0,nil)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f60,plain,
! [Xs] :
( leqNat(lengthNat(Xs),s(s(s(z))))
| ~ unique(Xs)
| ~ sorted(rev(Xs)) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f61,plain,
! [X0] :
( leqNat(lengthNat(X0),s(s(s(z))))
| ~ unique(X0)
| ~ sorted(rev(X0)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f67,definition,
( sQ1_spl
<=> unique(nil) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f69,plain,
( sQ1_spl
| ~ unique(nil) ),
inference(component_clause,[status(thm)],[f67]) ).
fof(f77,plain,
! [X0,X1] :
( leqNat(s(lengthNat(X1)),s(s(s(z))))
| ~ unique(cons(X0,X1))
| ~ sorted(rev(cons(X0,X1))) ),
inference(paramodulation,[status(thm)],[f43,f61]) ).
fof(f79,plain,
! [X0,X1] :
( leqNat(lengthNat(X1),s(s(z)))
| ~ unique(cons(X0,X1))
| ~ sorted(rev(cons(X0,X1))) ),
inference(resolution,[status(thm)],[f77,f33]) ).
fof(f80,plain,
! [X0,X1,X2] :
( leqNat(s(s(lengthNat(X2))),s(s(s(z))))
| ~ unique(cons(X0,cons(X1,X2)))
| ~ sorted(rev(cons(X0,cons(X1,X2)))) ),
inference(paramodulation,[status(thm)],[f43,f77]) ).
fof(f89,plain,
! [X0,X1,X2] :
( leqNat(s(lengthNat(X2)),s(s(z)))
| ~ unique(cons(X0,cons(X1,X2)))
| ~ sorted(rev(cons(X0,cons(X1,X2)))) ),
inference(paramodulation,[status(thm)],[f43,f79]) ).
fof(f97,plain,
! [X0] : rev(cons(X0,nil)) = append(nil,cons(X0,nil)),
inference(paramodulation,[status(thm)],[f58,f59]) ).
fof(f98,plain,
! [X0] : rev(cons(X0,nil)) = cons(X0,nil),
inference(forward_demodulation,[status(thm)],[f56,f97]) ).
fof(f99,plain,
! [X0,X1] : rev(cons(X0,cons(X1,nil))) = append(cons(X1,nil),cons(X0,nil)),
inference(paramodulation,[status(thm)],[f98,f59]) ).
fof(f104,plain,
! [X0,X1] :
( leqNat(s(s(z)),s(s(s(z))))
| ~ unique(cons(X0,cons(X1,nil)))
| ~ sorted(rev(cons(X0,cons(X1,nil)))) ),
inference(paramodulation,[status(thm)],[f42,f80]) ).
fof(f105,definition,
! [X0,X1] :
( sQ6_spl
<=> ( ~ unique(cons(X0,cons(X1,nil)))
| ~ sorted(rev(cons(X0,cons(X1,nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f106,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ unique(cons(X0,cons(X1,nil)))
| ~ sorted(rev(cons(X0,cons(X1,nil)))) ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f108,definition,
( sQ7_spl
<=> leqNat(s(s(z)),s(s(s(z)))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f109,plain,
( ~ sQ7_spl
| leqNat(s(s(z)),s(s(s(z)))) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,plain,
( sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f104,f105,f108]) ).
fof(f119,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f69,f50]) ).
fof(f120,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f119]) ).
fof(f127,plain,
! [X0,X1] : rev(cons(X0,cons(X1,nil))) = cons(X1,append(nil,cons(X0,nil))),
inference(forward_demodulation,[status(thm)],[f57,f99]) ).
fof(f128,plain,
! [X0,X1] : rev(cons(X0,cons(X1,nil))) = cons(X1,cons(X0,nil)),
inference(forward_demodulation,[status(thm)],[f56,f127]) ).
fof(f129,plain,
! [X0,X1,X2] : rev(cons(X0,cons(X1,cons(X2,nil)))) = append(cons(X2,cons(X1,nil)),cons(X0,nil)),
inference(paramodulation,[status(thm)],[f128,f59]) ).
fof(f130,plain,
! [X0,X1,X2] : rev(cons(X0,cons(X1,cons(X2,nil)))) = cons(X2,append(cons(X1,nil),cons(X0,nil))),
inference(forward_demodulation,[status(thm)],[f57,f129]) ).
fof(f131,plain,
! [X0,X1,X2] : rev(cons(X0,cons(X1,cons(X2,nil)))) = cons(X2,cons(X1,append(nil,cons(X0,nil)))),
inference(forward_demodulation,[status(thm)],[f57,f130]) ).
fof(f132,plain,
! [X0,X1,X2] : rev(cons(X0,cons(X1,cons(X2,nil)))) = cons(X2,cons(X1,cons(X0,nil))),
inference(forward_demodulation,[status(thm)],[f56,f131]) ).
fof(f134,plain,
! [X0,X1] :
( leqNat(s(lengthNat(nil)),s(s(z)))
| ~ unique(cons(X1,cons(X0,nil)))
| ~ sorted(cons(X0,cons(X1,nil))) ),
inference(paramodulation,[status(thm)],[f128,f89]) ).
fof(f135,definition,
! [X0,X1] :
( sQ9_spl
<=> ( ~ unique(cons(X1,cons(X0,nil)))
| ~ sorted(cons(X0,cons(X1,nil))) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f136,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ unique(cons(X1,cons(X0,nil)))
| ~ sorted(cons(X0,cons(X1,nil))) ),
inference(component_clause,[status(thm)],[f135]) ).
fof(f138,definition,
( sQ10_spl
<=> leqNat(s(lengthNat(nil)),s(s(z))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( ~ sQ10_spl
| leqNat(s(lengthNat(nil)),s(s(z))) ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f141,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f134,f135,f138]) ).
fof(f142,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| ~ sorted(cons(X0,cons(X1,nil))) ),
inference(resolution,[status(thm)],[f136,f55]) ).
fof(f143,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ unique(cons(X1,cons(X0,nil)))
| ~ sorted(cons(X0,cons(X1,nil))) ),
inference(forward_demodulation,[status(thm)],[f128,f106]) ).
fof(f155,plain,
! [X0,X1,X2,X3] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = append(cons(X3,cons(X2,cons(X1,nil))),cons(X0,nil)),
inference(paramodulation,[status(thm)],[f132,f59]) ).
fof(f158,plain,
! [X0,X1,X2,X3] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = cons(X3,append(cons(X2,cons(X1,nil)),cons(X0,nil))),
inference(forward_demodulation,[status(thm)],[f57,f155]) ).
fof(f159,plain,
! [X0,X1,X2,X3] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = cons(X3,cons(X2,append(cons(X1,nil),cons(X0,nil)))),
inference(forward_demodulation,[status(thm)],[f57,f158]) ).
fof(f160,plain,
! [X0,X1,X2,X3] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = cons(X3,cons(X2,cons(X1,append(nil,cons(X0,nil))))),
inference(forward_demodulation,[status(thm)],[f57,f159]) ).
fof(f161,plain,
! [X0,X1,X2,X3] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = cons(X3,cons(X2,cons(X1,cons(X0,nil)))),
inference(forward_demodulation,[status(thm)],[f56,f160]) ).
fof(f162,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ sorted(cons(X0,nil))
| ~ leqNat(X1,X0)
| ~ unique(cons(X1,nil))
| elemNat(X0,cons(X1,nil)) ),
inference(resolution,[status(thm)],[f142,f41]) ).
fof(f163,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ leqNat(X1,X0)
| ~ unique(cons(X1,nil))
| elemNat(X0,cons(X1,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f162,f36]) ).
fof(f164,plain,
! [X0,X1] :
( ~ sQ9_spl
| elemNat(X1,nil)
| X1 = X0
| ~ leqNat(X0,X1)
| ~ unique(cons(X0,nil)) ),
inference(resolution,[status(thm)],[f163,f47]) ).
fof(f165,plain,
! [X0,X1] :
( ~ sQ9_spl
| X1 = X0
| ~ leqNat(X0,X1)
| ~ unique(cons(X0,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f44]) ).
fof(f176,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ unique(nil)
| elemNat(X0,nil)
| X1 = X0
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f165,f55]) ).
fof(f177,definition,
! [X0,X1] :
( sQ15_spl
<=> ( elemNat(X0,nil)
| X1 = X0
| ~ leqNat(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f178,plain,
! [X0,X1] :
( ~ sQ15_spl
| elemNat(X0,nil)
| X1 = X0
| ~ leqNat(X0,X1) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,plain,
( ~ sQ9_spl
| ~ sQ1_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f176,f177,f67,f135]) ).
fof(f181,plain,
! [X0,X1] :
( ~ sQ15_spl
| X1 = X0
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f44]) ).
fof(f182,plain,
( ~ sQ10_spl
| leqNat(s(z),s(s(z))) ),
inference(forward_demodulation,[status(thm)],[f42,f139]) ).
fof(f183,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| ~ sorted(cons(X0,cons(X1,nil))) ),
inference(resolution,[status(thm)],[f143,f55]) ).
fof(f189,plain,
! [X0] :
( ~ sQ15_spl
| X0 = z ),
inference(resolution,[status(thm)],[f181,f29]) ).
fof(f192,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f28,f189]) ).
fof(f203,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f192]) ).
fof(f215,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sorted(cons(X0,nil))
| ~ leqNat(X1,X0)
| ~ unique(cons(X1,nil))
| elemNat(X0,cons(X1,nil)) ),
inference(resolution,[status(thm)],[f183,f41]) ).
fof(f216,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ leqNat(X1,X0)
| ~ unique(cons(X1,nil))
| elemNat(X0,cons(X1,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f215,f36]) ).
fof(f217,plain,
! [X0,X1] :
( ~ sQ6_spl
| elemNat(X1,nil)
| X1 = X0
| ~ leqNat(X0,X1)
| ~ unique(cons(X0,nil)) ),
inference(resolution,[status(thm)],[f216,f47]) ).
fof(f218,plain,
! [X0,X1] :
( ~ sQ6_spl
| X1 = X0
| ~ leqNat(X0,X1)
| ~ unique(cons(X0,nil)) ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f44]) ).
fof(f221,plain,
! [X0,X1,X2,X3] :
( leqNat(s(lengthNat(cons(X1,cons(X0,nil)))),s(s(z)))
| ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(paramodulation,[status(thm)],[f161,f89]) ).
fof(f223,definition,
! [X0,X1,X2,X3] :
( sQ16_spl
<=> ( ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f224,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f232,plain,
! [X0,X1,X2,X3] :
( leqNat(s(s(lengthNat(cons(X0,nil)))),s(s(z)))
| ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(forward_demodulation,[status(thm)],[f43,f221]) ).
fof(f233,plain,
! [X0,X1,X2,X3] :
( leqNat(s(s(s(lengthNat(nil)))),s(s(z)))
| ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(forward_demodulation,[status(thm)],[f43,f232]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
( leqNat(s(s(s(z))),s(s(z)))
| ~ unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(forward_demodulation,[status(thm)],[f42,f233]) ).
fof(f240,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ unique(nil)
| elemNat(X0,nil)
| X1 = X0
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f218,f55]) ).
fof(f241,plain,
( ~ sQ6_spl
| ~ sQ1_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f240,f177,f67,f105]) ).
fof(f243,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ unique(cons(X2,cons(X1,cons(X0,nil))))
| elemNat(X3,cons(X2,cons(X1,cons(X0,nil))))
| ~ sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) ),
inference(resolution,[status(thm)],[f224,f55]) ).
fof(f266,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ sorted(cons(X2,cons(X1,cons(X0,nil))))
| ~ leqNat(X3,X2)
| ~ unique(cons(X1,cons(X2,cons(X3,nil))))
| elemNat(X0,cons(X1,cons(X2,cons(X3,nil)))) ),
inference(resolution,[status(thm)],[f243,f41]) ).
fof(f309,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X3,cons(X1,cons(X2,nil)))
| X3 = X0
| ~ sorted(cons(X1,cons(X0,cons(X3,nil))))
| ~ leqNat(X2,X1)
| ~ unique(cons(X0,cons(X1,cons(X2,nil)))) ),
inference(resolution,[status(thm)],[f266,f47]) ).
fof(f333,definition,
( sQ24_spl
<=> s(s(z)) = s(z) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ24_spl
| s(s(z)) = s(z) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f335,plain,
( sQ24_spl
| s(s(z)) != s(z) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f340,definition,
( sQ26_spl
<=> s(s(s(z))) = s(z) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( ~ sQ26_spl
| s(s(s(z))) = s(z) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f347,definition,
( sQ28_spl
<=> s(s(s(z))) = s(s(z)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ28_spl
| s(s(s(z))) = s(s(z)) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f402,definition,
( sQ33_spl
<=> s(s(z)) = z ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( ~ sQ33_spl
| s(s(z)) = z ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f405,definition,
( sQ34_spl
<=> s(z) = z ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( ~ sQ34_spl
| s(z) = z ),
inference(component_clause,[status(thm)],[f405]) ).
fof(f409,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f406,f28]) ).
fof(f410,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f409]) ).
fof(f411,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f403,f28]) ).
fof(f412,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f411]) ).
fof(f467,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ unique(cons(X1,cons(X0,nil)))
| elemNat(X2,cons(X1,cons(X0,nil)))
| elemNat(X3,cons(X1,cons(X0,nil)))
| X3 = X2
| ~ sorted(cons(X1,cons(X2,cons(X3,nil))))
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f309,f55]) ).
fof(f472,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ sorted(cons(X3,cons(X2,nil)))
| ~ leqNat(X1,X3)
| ~ unique(cons(X1,cons(X0,nil)))
| elemNat(X3,cons(X1,cons(X0,nil)))
| elemNat(X2,cons(X1,cons(X0,nil)))
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f467,f41]) ).
fof(f483,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X3,cons(X0,nil))
| X3 = X1
| ~ sorted(cons(X3,cons(X2,nil)))
| ~ leqNat(X1,X3)
| ~ unique(cons(X1,cons(X0,nil)))
| elemNat(X2,cons(X1,cons(X0,nil)))
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f472,f47]) ).
fof(f484,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X2,cons(X0,nil))
| X2 = X1
| elemNat(X3,cons(X0,nil))
| X3 = X1
| ~ sorted(cons(X3,cons(X2,nil)))
| ~ leqNat(X1,X3)
| ~ unique(cons(X1,cons(X0,nil)))
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f483,f47]) ).
fof(f485,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| elemNat(X2,cons(X0,nil))
| X2 = X1
| elemNat(X3,cons(X0,nil))
| X3 = X1
| ~ sorted(cons(X3,cons(X2,nil)))
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f484,f55]) ).
fof(f522,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ sorted(cons(X2,nil))
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| elemNat(X2,cons(X0,nil))
| X2 = X1
| elemNat(X3,cons(X0,nil))
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f485,f41]) ).
fof(f523,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| elemNat(X2,cons(X0,nil))
| X2 = X1
| elemNat(X3,cons(X0,nil))
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f522,f36]) ).
fof(f525,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X3,nil)
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| elemNat(X2,cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f523,f47]) ).
fof(f526,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| elemNat(X2,cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f525,f44]) ).
fof(f527,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X2,nil)
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f526,f47]) ).
fof(f528,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| elemNat(X1,cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f44]) ).
fof(f538,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| elemNat(X1,nil)
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f528,f47]) ).
fof(f539,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| ~ unique(cons(X0,nil))
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f44]) ).
fof(f540,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| ~ unique(nil)
| elemNat(X0,nil)
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(resolution,[status(thm)],[f539,f55]) ).
fof(f541,definition,
! [X0,X1,X2,X3] :
( sQ43_spl
<=> ( elemNat(X0,nil)
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f542,plain,
! [X0,X1,X2,X3] :
( ~ sQ43_spl
| elemNat(X0,nil)
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f544,plain,
( ~ sQ16_spl
| ~ sQ1_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f540,f541,f67,f223]) ).
fof(f545,plain,
! [X0,X1,X2,X3] :
( ~ sQ43_spl
| X1 = X0
| X2 = X0
| X3 = X0
| ~ leqNat(X3,X2)
| X2 = X1
| X3 = X1
| ~ leqNat(X1,X3)
| X2 = X3
| ~ leqNat(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f44]) ).
fof(f547,definition,
( sQ44_spl
<=> leqNat(s(s(s(z))),s(s(z))) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( ~ sQ44_spl
| leqNat(s(s(s(z))),s(s(z))) ),
inference(component_clause,[status(thm)],[f547]) ).
fof(f550,plain,
( sQ44_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f234,f223,f547]) ).
fof(f554,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ sQ43_spl
| s(z) = X0
| X1 = X0
| s(s(z)) = X0
| ~ leqNat(s(s(z)),X1)
| X1 = s(z)
| s(s(z)) = s(z)
| X1 = s(s(z))
| ~ leqNat(X0,s(z)) ),
inference(resolution,[status(thm)],[f545,f182]) ).
fof(f595,definition,
! [X0,X1] :
( sQ48_spl
<=> ( s(z) = X0
| X1 = X0
| s(s(z)) = X0
| ~ leqNat(s(s(z)),X1)
| X1 = s(z)
| X1 = s(s(z))
| ~ leqNat(X0,s(z)) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f596,plain,
! [X0,X1] :
( ~ sQ48_spl
| s(z) = X0
| X1 = X0
| s(s(z)) = X0
| ~ leqNat(s(s(z)),X1)
| X1 = s(z)
| X1 = s(s(z))
| ~ leqNat(X0,s(z)) ),
inference(component_clause,[status(thm)],[f595]) ).
fof(f598,plain,
( ~ sQ10_spl
| ~ sQ43_spl
| sQ24_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f554,f595,f333,f541,f138]) ).
fof(f682,plain,
( ~ sQ24_spl
| proj1S(s(z)) = s(z) ),
inference(paramodulation,[status(thm)],[f334,f27]) ).
fof(f730,plain,
( ~ sQ24_spl
| z = s(z) ),
inference(forward_demodulation,[status(thm)],[f27,f682]) ).
fof(f731,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f730,f28]) ).
fof(f732,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f731]) ).
fof(f750,plain,
( ~ sQ44_spl
| leqNat(s(s(z)),s(z)) ),
inference(resolution,[status(thm)],[f548,f33]) ).
fof(f758,plain,
( ~ sQ44_spl
| leqNat(s(z),z) ),
inference(resolution,[status(thm)],[f750,f33]) ).
fof(f759,plain,
( ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f30]) ).
fof(f760,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f759]) ).
fof(f770,plain,
( ~ sQ26_spl
| proj1S(s(z)) = s(s(z)) ),
inference(paramodulation,[status(thm)],[f341,f27]) ).
fof(f772,plain,
( ~ sQ26_spl
| z = s(s(z)) ),
inference(forward_demodulation,[status(thm)],[f27,f770]) ).
fof(f773,plain,
( ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f772,f28]) ).
fof(f774,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f773]) ).
fof(f790,plain,
( ~ sQ28_spl
| proj1S(s(s(z))) = s(s(z)) ),
inference(paramodulation,[status(thm)],[f348,f27]) ).
fof(f792,plain,
( ~ sQ28_spl
| s(z) = s(s(z)) ),
inference(forward_demodulation,[status(thm)],[f27,f790]) ).
fof(f793,plain,
( ~ sQ28_spl
| sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f792,f335]) ).
fof(f794,plain,
( ~ sQ28_spl
| sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f793]) ).
fof(f1262,definition,
( sQ115_spl
<=> leqNat(z,s(z)) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1264,plain,
( sQ115_spl
| ~ leqNat(z,s(z)) ),
inference(component_clause,[status(thm)],[f1262]) ).
fof(f1302,definition,
( sQ123_spl
<=> s(z) = s(s(s(s(s(s(s(s(z)))))))) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ123_spl
| s(z) = s(s(s(s(s(s(s(s(z)))))))) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1495,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1264,f29]) ).
fof(f1496,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f1495]) ).
fof(f1544,plain,
( ~ sQ123_spl
| proj1S(s(z)) = s(s(s(s(s(s(s(z))))))) ),
inference(paramodulation,[status(thm)],[f1303,f27]) ).
fof(f1554,plain,
( ~ sQ123_spl
| z = s(s(s(s(s(s(s(z))))))) ),
inference(forward_demodulation,[status(thm)],[f27,f1544]) ).
fof(f1555,plain,
( ~ sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1554,f28]) ).
fof(f1556,plain,
~ sQ123_spl,
inference(contradiction_clause,[status(thm)],[f1555]) ).
fof(f1694,plain,
! [X0] :
( ~ sQ7_spl
| ~ sQ48_spl
| s(z) = X0
| s(s(s(z))) = X0
| s(s(z)) = X0
| s(s(s(z))) = s(z)
| s(s(s(z))) = s(s(z))
| ~ leqNat(X0,s(z)) ),
inference(resolution,[status(thm)],[f596,f109]) ).
fof(f1697,definition,
! [X0] :
( sQ149_spl
<=> ( s(z) = X0
| s(s(s(z))) = X0
| s(s(z)) = X0
| ~ leqNat(X0,s(z)) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1698,plain,
! [X0] :
( ~ sQ149_spl
| s(z) = X0
| s(s(s(z))) = X0
| s(s(z)) = X0
| ~ leqNat(X0,s(z)) ),
inference(component_clause,[status(thm)],[f1697]) ).
fof(f1700,plain,
( ~ sQ7_spl
| ~ sQ48_spl
| sQ26_spl
| sQ28_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1694,f1697,f347,f340,f595,f108]) ).
fof(f1710,plain,
( ~ sQ149_spl
| s(z) = z
| s(s(z)) = z
| ~ leqNat(z,s(z)) ),
inference(resolution,[status(thm)],[f1698,f28]) ).
fof(f1716,plain,
( ~ sQ149_spl
| sQ34_spl
| sQ33_spl
| ~ sQ115_spl ),
inference(split_clause,[status(thm)],[f1710,f1262,f402,f405,f1697]) ).
fof(f1719,plain,
$false,
inference(sat_refutation,[status(thm)],[f111,f120,f141,f180,f203,f241,f410,f412,f544,f550,f598,f732,f760,f774,f794,f1496,f1556,f1700,f1716]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX203+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n007.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 10:31:36 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 0.12/0.42 % Refutation found
% 0.12/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.44 % Elapsed time: 0.093097 seconds
% 0.12/0.44 % CPU time: 0.503655 seconds
% 0.12/0.44 % Total memory used: 114.302 MB
% 0.12/0.44 % Net memory used: 113.514 MB
%------------------------------------------------------------------------------