%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX203+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:47 PM UTC 2026
% Result : Theorem 0.09s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX203+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:34:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.48 % Refutation found
% 0.09/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.48 fof(f4,axiom,(
% 0.09/0.48 (! [X] : proj1S(s(X)) = X )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f5,axiom,(
% 0.09/0.48 (! [X] : z != s(X) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f6,axiom,(
% 0.09/0.48 (! [Y] : leqNat(z,Y) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f7,axiom,(
% 0.09/0.48 (! [Z] : ~ leqNat(s(Z),z) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f8,axiom,(
% 0.09/0.48 (! [Z,M] :( leqNat(s(Z),s(M))<=> leqNat(Z,M) ) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f10,axiom,(
% 0.09/0.48 (! [Y] : sorted(cons(Y,nil)) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f11,axiom,(
% 0.09/0.48 (! [Y,Y2,Xs] :( sorted(cons(Y,cons(Y2,Xs)))<=> ( leqNat(Y,Y2)& sorted(cons(Y2,Xs)) ) ) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f12,axiom,(
% 0.09/0.48 lengthNat(nil) = z ),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f13,axiom,(
% 0.09/0.48 (! [Y,Xs] : lengthNat(cons(Y,Xs)) = s(lengthNat(Xs)) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f14,axiom,(
% 0.09/0.48 (! [X] : ~ elemNat(X,nil) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f15,axiom,(
% 0.09/0.48 (! [X,Z,Xs] :( elemNat(X,cons(Z,Xs))<=> ( X = Z| elemNat(X,Xs) ) ) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f16,axiom,(
% 0.09/0.48 unique(nil) ),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f17,axiom,(
% 0.09/0.48 (! [Y,Xs] :( unique(cons(Y,Xs))<=> ( ~ elemNat(Y,Xs)& unique(Xs) ) ) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f18,axiom,(
% 0.09/0.48 (! [Y] : append(nil,Y) = Y )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f19,axiom,(
% 0.09/0.48 (! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f20,axiom,(
% 0.09/0.48 rev(nil) = nil ),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f21,axiom,(
% 0.09/0.48 (! [Y,Xs] : rev(cons(Y,Xs)) = append(rev(Xs),cons(Y,nil)) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f22,conjecture,(
% 0.09/0.48 (? [Xs] :~ ( sorted(rev(Xs))=> ( unique(Xs)=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ) )),
% 0.09/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f23,negated_conjecture,(
% 0.09/0.48 ~((? [Xs] :~ ( sorted(rev(Xs))=> ( unique(Xs)=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ) ))),
% 0.09/0.48 inference(negated_conjecture,[status(cth)],[f22])).
% 0.09/0.48 fof(f27,plain,(
% 0.09/0.48 ![X0]: (proj1S(s(X0))=X0)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.48 fof(f28,plain,(
% 0.09/0.48 ![X0]: (~z=s(X0))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.48 fof(f29,plain,(
% 0.09/0.48 ![X0]: (leqNat(z,X0))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.48 fof(f30,plain,(
% 0.09/0.48 ![X0]: (~leqNat(s(X0),z))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f7])).
% 0.09/0.48 fof(f31,plain,(
% 0.09/0.48 ![Z,M]: ((~leqNat(s(Z),s(M))|leqNat(Z,M))&(leqNat(s(Z),s(M))|~leqNat(Z,M)))),
% 0.09/0.48 inference(NNF_transformation,[status(thm)],[f8])).
% 0.09/0.48 fof(f32,plain,(
% 0.09/0.48 (![Z,M]: (~leqNat(s(Z),s(M))|leqNat(Z,M)))&(![Z,M]: (leqNat(s(Z),s(M))|~leqNat(Z,M)))),
% 0.09/0.48 inference(miniscoping,[status(thm)],[f31])).
% 0.09/0.48 fof(f33,plain,(
% 0.09/0.48 ![X0,X1]: (~leqNat(s(X0),s(X1))|leqNat(X0,X1))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f32])).
% 0.09/0.48 fof(f34,plain,(
% 0.09/0.48 ![X0,X1]: (leqNat(s(X0),s(X1))|~leqNat(X0,X1))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f32])).
% 0.09/0.48 fof(f36,plain,(
% 0.09/0.48 ![X0]: (sorted(cons(X0,nil)))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/0.48 fof(f37,plain,(
% 0.09/0.48 ![Y,Y2,Xs]: ((~sorted(cons(Y,cons(Y2,Xs)))|(leqNat(Y,Y2)&sorted(cons(Y2,Xs))))&(sorted(cons(Y,cons(Y2,Xs)))|(~leqNat(Y,Y2)|~sorted(cons(Y2,Xs)))))),
% 0.09/0.48 inference(NNF_transformation,[status(thm)],[f11])).
% 0.09/0.48 fof(f38,plain,(
% 0.09/0.48 (![Y,Y2,Xs]: (~sorted(cons(Y,cons(Y2,Xs)))|(leqNat(Y,Y2)&sorted(cons(Y2,Xs)))))&(![Y,Y2,Xs]: (sorted(cons(Y,cons(Y2,Xs)))|(~leqNat(Y,Y2)|~sorted(cons(Y2,Xs)))))),
% 0.09/0.48 inference(miniscoping,[status(thm)],[f37])).
% 0.09/0.48 fof(f41,plain,(
% 0.09/0.48 ![X0,X1,X2]: (sorted(cons(X0,cons(X1,X2)))|~leqNat(X0,X1)|~sorted(cons(X1,X2)))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f38])).
% 0.09/0.48 fof(f42,plain,(
% 0.09/0.48 lengthNat(nil)=z),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f12])).
% 0.09/0.48 fof(f43,plain,(
% 0.09/0.48 ![X0,X1]: (lengthNat(cons(X0,X1))=s(lengthNat(X1)))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f13])).
% 0.09/0.48 fof(f44,plain,(
% 0.09/0.48 ![X0]: (~elemNat(X0,nil))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f14])).
% 0.09/0.48 fof(f45,plain,(
% 0.09/0.48 ![X,Z,Xs]: ((~elemNat(X,cons(Z,Xs))|(X=Z|elemNat(X,Xs)))&(elemNat(X,cons(Z,Xs))|(~X=Z&~elemNat(X,Xs))))),
% 0.09/0.48 inference(NNF_transformation,[status(thm)],[f15])).
% 0.09/0.48 fof(f46,plain,(
% 0.09/0.48 (![X,Z,Xs]: (~elemNat(X,cons(Z,Xs))|(X=Z|elemNat(X,Xs))))&(![X,Z,Xs]: (elemNat(X,cons(Z,Xs))|(~X=Z&~elemNat(X,Xs))))),
% 0.09/0.48 inference(miniscoping,[status(thm)],[f45])).
% 0.09/0.48 fof(f47,plain,(
% 0.09/0.48 ![X0,X1,X2]: (~elemNat(X0,cons(X1,X2))|X0=X1|elemNat(X0,X2))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f46])).
% 0.09/0.48 fof(f50,plain,(
% 0.09/0.48 unique(nil)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f16])).
% 0.09/0.48 fof(f51,plain,(
% 0.09/0.48 ![Y,Xs]: ((~unique(cons(Y,Xs))|(~elemNat(Y,Xs)&unique(Xs)))&(unique(cons(Y,Xs))|(elemNat(Y,Xs)|~unique(Xs))))),
% 0.09/0.48 inference(NNF_transformation,[status(thm)],[f17])).
% 0.09/0.48 fof(f52,plain,(
% 0.09/0.48 (![Y,Xs]: (~unique(cons(Y,Xs))|(~elemNat(Y,Xs)&unique(Xs))))&(![Y,Xs]: (unique(cons(Y,Xs))|(elemNat(Y,Xs)|~unique(Xs))))),
% 0.09/0.48 inference(miniscoping,[status(thm)],[f51])).
% 0.09/0.48 fof(f55,plain,(
% 0.09/0.48 ![X0,X1]: (unique(cons(X0,X1))|elemNat(X0,X1)|~unique(X1))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f52])).
% 0.09/0.48 fof(f56,plain,(
% 0.09/0.48 ![X0]: (append(nil,X0)=X0)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f18])).
% 0.09/0.48 fof(f57,plain,(
% 0.09/0.48 ![X0,X1,X2]: (append(cons(X0,X1),X2)=cons(X0,append(X1,X2)))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.09/0.48 fof(f58,plain,(
% 0.09/0.48 rev(nil)=nil),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f20])).
% 0.09/0.48 fof(f59,plain,(
% 0.09/0.48 ![X0,X1]: (rev(cons(X0,X1))=append(rev(X1),cons(X0,nil)))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f21])).
% 0.09/0.48 fof(f60,plain,(
% 0.09/0.48 (![Xs]: (~sorted(rev(Xs))|(~unique(Xs)|leqNat(lengthNat(Xs),s(s(s(z)))))))),
% 0.09/0.48 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.09/0.48 fof(f61,plain,(
% 0.09/0.48 ![X0]: (~sorted(rev(X0))|~unique(X0)|leqNat(lengthNat(X0),s(s(s(z)))))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f60])).
% 0.09/0.48 fof(f75,plain,(
% 0.09/0.48 ![X0]: (leqNat(s(z),s(X0)))),
% 0.09/0.48 inference(resolution,[status(thm)],[f34,f29])).
% 0.09/0.48 fof(f77,plain,(
% 0.09/0.48 ![X0]: (leqNat(s(s(z)),s(s(X0))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f75,f34])).
% 0.09/0.48 fof(f78,plain,(
% 0.09/0.48 ![X0,X1]: (sorted(cons(X0,cons(X1,nil)))|~leqNat(X0,X1))),
% 0.09/0.48 inference(resolution,[status(thm)],[f41,f36])).
% 0.09/0.48 fof(f83,plain,(
% 0.09/0.48 ![X0]: (unique(cons(X0,nil))|elemNat(X0,nil))),
% 0.09/0.48 inference(resolution,[status(thm)],[f55,f50])).
% 0.09/0.48 fof(f84,plain,(
% 0.09/0.48 ![X0]: (unique(cons(X0,nil)))),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f83,f44])).
% 0.09/0.48 fof(f87,plain,(
% 0.09/0.48 ![X0,X1]: (unique(cons(X0,cons(X1,nil)))|elemNat(X0,cons(X1,nil)))),
% 0.09/0.48 inference(resolution,[status(thm)],[f84,f55])).
% 0.09/0.48 fof(f89,plain,(
% 0.09/0.48 ![X0]: (leqNat(s(s(s(z))),s(s(s(X0)))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f77,f34])).
% 0.09/0.48 fof(f92,plain,(
% 0.09/0.48 ![X0,X1]: (append(cons(X0,nil),X1)=cons(X0,X1))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f56,f57])).
% 0.09/0.48 fof(f114,plain,(
% 0.09/0.48 ![X0]: (rev(cons(X0,nil))=append(nil,cons(X0,nil)))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f58,f59])).
% 0.09/0.48 fof(f116,plain,(
% 0.09/0.48 ![X0]: (rev(cons(X0,nil))=cons(X0,nil))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f56,f114])).
% 0.09/0.48 fof(f117,plain,(
% 0.09/0.48 ![X0]: (sorted(cons(s(s(z)),cons(s(s(X0)),nil))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f78,f77])).
% 0.09/0.48 fof(f120,plain,(
% 0.09/0.48 ![X0,X1,X2]: (append(cons(X0,cons(X1,nil)),X2)=cons(X0,cons(X1,X2)))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f92,f57])).
% 0.09/0.48 fof(f124,plain,(
% 0.09/0.48 ![X0,X1]: (rev(cons(X0,cons(X1,nil)))=append(cons(X1,nil),cons(X0,nil)))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f116,f59])).
% 0.09/0.48 fof(f126,plain,(
% 0.09/0.48 ![X0,X1]: (rev(cons(X0,cons(X1,nil)))=cons(X1,cons(X0,nil)))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f92,f124])).
% 0.09/0.48 fof(f146,plain,(
% 0.09/0.48 ![X0]: (leqNat(s(s(s(s(z)))),s(s(s(s(X0))))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f89,f34])).
% 0.09/0.48 fof(f152,plain,(
% 0.09/0.48 ![X0,X1,X2]: (elemNat(X0,cons(X1,nil))|unique(cons(X2,cons(X0,cons(X1,nil))))|elemNat(X2,cons(X0,cons(X1,nil))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f87,f55])).
% 0.09/0.48 fof(f153,plain,(
% 0.09/0.48 ![X0,X1,X2]: (rev(cons(X0,cons(X1,cons(X2,nil))))=append(cons(X2,cons(X1,nil)),cons(X0,nil)))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f126,f59])).
% 0.09/0.48 fof(f160,plain,(
% 0.09/0.48 ![X0,X1]: (sorted(cons(X0,cons(s(s(z)),cons(s(s(X1)),nil))))|~leqNat(X0,s(s(z))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f117,f41])).
% 0.09/0.48 fof(f266,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (append(cons(X0,cons(X1,cons(X2,nil))),X3)=cons(X0,cons(X1,cons(X2,X3))))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f120,f57])).
% 0.09/0.48 fof(f491,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (elemNat(X0,cons(X1,nil))|elemNat(X2,cons(X0,cons(X1,nil)))|unique(cons(X3,cons(X2,cons(X0,cons(X1,nil)))))|elemNat(X3,cons(X2,cons(X0,cons(X1,nil)))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f152,f55])).
% 0.09/0.48 fof(f492,plain,(
% 0.09/0.48 ![X0,X1,X2]: (rev(cons(X0,cons(X1,cons(X2,nil))))=cons(X2,cons(X1,cons(X0,nil))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f120,f153])).
% 0.09/0.48 fof(f495,plain,(
% 0.09/0.48 ![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)))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f492,f59])).
% 0.09/0.48 fof(f845,plain,(
% 0.09/0.48 ![X0]: (sorted(cons(s(z),cons(s(s(z)),cons(s(s(X0)),nil)))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f160,f75])).
% 0.09/0.48 fof(f852,plain,(
% 0.09/0.48 ![X0,X1]: (sorted(cons(X0,cons(s(z),cons(s(s(z)),cons(s(s(X1)),nil)))))|~leqNat(X0,s(z)))),
% 0.09/0.48 inference(resolution,[status(thm)],[f845,f41])).
% 0.09/0.48 fof(f1230,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (rev(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))=cons(X3,cons(X2,cons(X1,cons(X0,nil)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f266,f495])).
% 0.09/0.48 fof(f1235,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(lengthNat(cons(X3,cons(X2,cons(X1,cons(X0,nil))))),s(s(s(z)))))),
% 0.09/0.48 inference(paramodulation,[status(thm)],[f1230,f61])).
% 0.09/0.48 fof(f1237,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(s(lengthNat(cons(X2,cons(X1,cons(X0,nil))))),s(s(s(z)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f43,f1235])).
% 0.09/0.48 fof(f1238,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(s(s(lengthNat(cons(X1,cons(X0,nil))))),s(s(s(z)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f43,f1237])).
% 0.09/0.48 fof(f1239,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(s(s(s(lengthNat(cons(X0,nil))))),s(s(s(z)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f43,f1238])).
% 0.09/0.48 fof(f1240,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(s(s(s(s(lengthNat(nil))))),s(s(s(z)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f43,f1239])).
% 0.09/0.48 fof(f1241,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|leqNat(s(s(s(s(z)))),s(s(s(z)))))),
% 0.09/0.48 inference(forward_demodulation,[status(thm)],[f42,f1240])).
% 0.09/0.48 fof(f1637,definition,(
% 0.09/0.48 sQ4_spl <=> (leqNat(s(s(s(s(z)))),s(s(s(z)))))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f1638,plain,(
% 0.09/0.48 leqNat(s(s(s(s(z)))),s(s(s(z))))|~sQ4_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1637])).
% 0.09/0.48 fof(f1639,plain,(
% 0.09/0.48 ~leqNat(s(s(s(s(z)))),s(s(s(z))))|sQ4_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1637])).
% 0.09/0.48 fof(f1677,plain,(
% 0.09/0.48 leqNat(s(s(s(z))),s(s(z)))|~sQ4_spl),
% 0.09/0.48 inference(resolution,[status(thm)],[f1638,f33])).
% 0.09/0.48 fof(f1763,plain,(
% 0.09/0.48 leqNat(s(s(z)),s(z))|~sQ4_spl),
% 0.09/0.48 inference(resolution,[status(thm)],[f1677,f33])).
% 0.09/0.48 fof(f1767,plain,(
% 0.09/0.48 leqNat(s(z),z)|~sQ4_spl),
% 0.09/0.48 inference(resolution,[status(thm)],[f1763,f33])).
% 0.09/0.48 fof(f1772,plain,(
% 0.09/0.48 $false|~sQ4_spl),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1767,f30])).
% 0.09/0.48 fof(f1773,plain,(
% 0.09/0.48 ~sQ4_spl),
% 0.09/0.48 inference(contradiction_clause,[status(thm)],[f1772])).
% 0.09/0.48 fof(f1774,definition,(
% 0.09/0.48 ![X0,X1,X2,X3]: (sQ12_spl <=> (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f1775,plain,(
% 0.09/0.48 ![X0,X1,X2,X3]: (~sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))|~unique(cons(X3,cons(X2,cons(X1,cons(X0,nil)))))|~sQ12_spl)),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1774])).
% 0.09/0.48 fof(f1777,plain,(
% 0.09/0.48 sQ12_spl|sQ4_spl),
% 0.09/0.48 inference(split_clause,[status(thm)],[f1241,f1774,f1637])).
% 0.09/0.48 fof(f1790,definition,(
% 0.09/0.48 sQ15_spl <=> (s(z)=z)),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f1791,plain,(
% 0.09/0.48 s(z)=z|~sQ15_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1790])).
% 0.09/0.48 fof(f1793,definition,(
% 0.09/0.48 sQ16_spl <=> (elemNat(s(z),cons(z,nil)))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f1794,plain,(
% 0.09/0.48 elemNat(s(z),cons(z,nil))|~sQ16_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1793])).
% 0.09/0.48 fof(f1797,plain,(
% 0.09/0.48 $false|~sQ15_spl),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1791,f28])).
% 0.09/0.48 fof(f1798,plain,(
% 0.09/0.48 ~sQ15_spl),
% 0.09/0.48 inference(contradiction_clause,[status(thm)],[f1797])).
% 0.09/0.48 fof(f1799,plain,(
% 0.09/0.48 s(z)=z|elemNat(s(z),nil)|~sQ16_spl),
% 0.09/0.48 inference(resolution,[status(thm)],[f1794,f47])).
% 0.09/0.48 fof(f1801,definition,(
% 0.09/0.48 sQ17_spl <=> (elemNat(s(z),nil))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f1802,plain,(
% 0.09/0.48 elemNat(s(z),nil)|~sQ17_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f1801])).
% 0.09/0.48 fof(f1804,plain,(
% 0.09/0.48 sQ15_spl|sQ17_spl|~sQ16_spl),
% 0.09/0.48 inference(split_clause,[status(thm)],[f1799,f1790,f1801,f1793])).
% 0.09/0.48 fof(f1805,plain,(
% 0.09/0.48 $false|~sQ17_spl),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f1802,f44])).
% 0.09/0.48 fof(f1806,plain,(
% 0.09/0.48 ~sQ17_spl),
% 0.09/0.48 inference(contradiction_clause,[status(thm)],[f1805])).
% 0.09/0.48 fof(f2210,definition,(
% 0.09/0.48 sQ22_spl <=> (s(s(z))=z)),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f2211,plain,(
% 0.09/0.48 s(s(z))=z|~sQ22_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f2210])).
% 0.09/0.48 fof(f2213,definition,(
% 0.09/0.48 sQ23_spl <=> (elemNat(s(s(z)),cons(z,nil)))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f2214,plain,(
% 0.09/0.48 elemNat(s(s(z)),cons(z,nil))|~sQ23_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f2213])).
% 0.09/0.48 fof(f2217,plain,(
% 0.09/0.48 $false|~sQ22_spl),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2211,f28])).
% 0.09/0.48 fof(f2218,plain,(
% 0.09/0.48 ~sQ22_spl),
% 0.09/0.48 inference(contradiction_clause,[status(thm)],[f2217])).
% 0.09/0.48 fof(f2219,plain,(
% 0.09/0.48 s(s(z))=z|elemNat(s(s(z)),nil)|~sQ23_spl),
% 0.09/0.48 inference(resolution,[status(thm)],[f2214,f47])).
% 0.09/0.48 fof(f2221,definition,(
% 0.09/0.48 sQ24_spl <=> (elemNat(s(s(z)),nil))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.48 fof(f2222,plain,(
% 0.09/0.48 elemNat(s(s(z)),nil)|~sQ24_spl),
% 0.09/0.48 inference(component_clause,[status(thm)],[f2221])).
% 0.09/0.48 fof(f2224,plain,(
% 0.09/0.48 sQ22_spl|sQ24_spl|~sQ23_spl),
% 0.09/0.48 inference(split_clause,[status(thm)],[f2219,f2210,f2221,f2213])).
% 0.09/0.48 fof(f2225,plain,(
% 0.09/0.48 $false|~sQ24_spl),
% 0.09/0.48 inference(forward_subsumption_resolution,[status(thm)],[f2222,f44])).
% 0.09/0.48 fof(f2226,plain,(
% 0.09/0.48 ~sQ24_spl),
% 0.09/0.48 inference(contradiction_clause,[status(thm)],[f2225])).
% 0.09/0.48 fof(f2820,plain,(
% 0.09/0.48 ![X0]: (sorted(cons(z,cons(s(z),cons(s(s(z)),cons(s(s(X0)),nil))))))),
% 0.09/0.48 inference(resolution,[status(thm)],[f852,f29])).
% 0.09/0.48 fof(f2821,plain,(
% 0.09/0.48 ![X0]: (~unique(cons(s(s(X0)),cons(s(s(z)),cons(s(z),cons(z,nil)))))|~sQ12_spl)),
% 0.09/0.48 inference(resolution,[status(thm)],[f2820,f1775])).
% 0.09/0.48 fof(f2826,plain,(
% 0.09/0.48 ![X0]: (elemNat(s(z),cons(z,nil))|elemNat(s(s(z)),cons(s(z),cons(z,nil)))|elemNat(s(s(X0)),cons(s(s(z)),cons(s(z),cons(z,nil))))|~sQ12_spl)),
% 0.09/0.48 inference(resolution,[status(thm)],[f2821,f491])).
% 0.09/0.48 fof(f2827,definition,(
% 0.09/0.48 sQ28_spl <=> (elemNat(s(s(z)),cons(s(z),cons(z,nil))))),
% 0.09/0.48 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f2828,plain,(
% 0.09/0.49 elemNat(s(s(z)),cons(s(z),cons(z,nil)))|~sQ28_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f2827])).
% 0.09/0.49 fof(f2830,definition,(
% 0.09/0.49 ![X0]: (sQ29_spl <=> (elemNat(s(s(X0)),cons(s(s(z)),cons(s(z),cons(z,nil))))))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f2831,plain,(
% 0.09/0.49 ![X0]: (elemNat(s(s(X0)),cons(s(s(z)),cons(s(z),cons(z,nil))))|~sQ29_spl)),
% 0.09/0.49 inference(component_clause,[status(thm)],[f2830])).
% 0.09/0.49 fof(f2833,plain,(
% 0.09/0.49 sQ16_spl|sQ28_spl|sQ29_spl|~sQ12_spl),
% 0.09/0.49 inference(split_clause,[status(thm)],[f2826,f1793,f2827,f2830,f1774])).
% 0.09/0.49 fof(f2834,plain,(
% 0.09/0.49 s(s(z))=s(z)|elemNat(s(s(z)),cons(z,nil))|~sQ28_spl),
% 0.09/0.49 inference(resolution,[status(thm)],[f2828,f47])).
% 0.09/0.49 fof(f2836,definition,(
% 0.09/0.49 sQ30_spl <=> (s(s(z))=s(z))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f2837,plain,(
% 0.09/0.49 s(s(z))=s(z)|~sQ30_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f2836])).
% 0.09/0.49 fof(f2839,plain,(
% 0.09/0.49 sQ30_spl|sQ23_spl|~sQ28_spl),
% 0.09/0.49 inference(split_clause,[status(thm)],[f2834,f2836,f2213,f2827])).
% 0.09/0.49 fof(f2847,plain,(
% 0.09/0.49 ~leqNat(s(s(s(s(z)))),s(s(z)))|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(backward_demodulation,[status(thm)],[f2837,f1639])).
% 0.09/0.49 fof(f2886,plain,(
% 0.09/0.49 ~leqNat(s(s(s(z))),s(s(z)))|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f2837,f2847])).
% 0.09/0.49 fof(f2887,plain,(
% 0.09/0.49 ~leqNat(s(s(z)),s(s(z)))|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f2837,f2886])).
% 0.09/0.49 fof(f2888,plain,(
% 0.09/0.49 ~leqNat(s(z),s(s(z)))|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f2837,f2887])).
% 0.09/0.49 fof(f2889,plain,(
% 0.09/0.49 ~leqNat(s(z),s(z))|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f2837,f2888])).
% 0.09/0.49 fof(f2890,plain,(
% 0.09/0.49 $false|~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(forward_subsumption_resolution,[status(thm)],[f2889,f75])).
% 0.09/0.49 fof(f2891,plain,(
% 0.09/0.49 ~sQ30_spl|sQ4_spl),
% 0.09/0.49 inference(contradiction_clause,[status(thm)],[f2890])).
% 0.09/0.49 fof(f2937,plain,(
% 0.09/0.49 ![X0]: (s(s(X0))=s(s(z))|elemNat(s(s(X0)),cons(s(z),cons(z,nil)))|~sQ29_spl)),
% 0.09/0.49 inference(resolution,[status(thm)],[f2831,f47])).
% 0.09/0.49 fof(f2987,plain,(
% 0.09/0.49 ![X0]: (s(s(X0))=s(s(z))|s(s(X0))=s(z)|elemNat(s(s(X0)),cons(z,nil))|~sQ29_spl)),
% 0.09/0.49 inference(resolution,[status(thm)],[f2937,f47])).
% 0.09/0.49 fof(f2992,plain,(
% 0.09/0.49 ![X0]: (s(s(X0))=s(s(z))|s(s(X0))=s(z)|s(s(X0))=z|elemNat(s(s(X0)),nil)|~sQ29_spl)),
% 0.09/0.49 inference(resolution,[status(thm)],[f2987,f47])).
% 0.09/0.49 fof(f2998,plain,(
% 0.09/0.49 ![X0]: (s(s(X0))=s(s(z))|s(s(X0))=s(z)|elemNat(s(s(X0)),nil)|~sQ29_spl)),
% 0.09/0.49 inference(forward_subsumption_resolution,[status(thm)],[f2992,f28])).
% 0.09/0.49 fof(f2999,plain,(
% 0.09/0.49 ![X0]: (s(s(X0))=s(s(z))|s(s(X0))=s(z)|~sQ29_spl)),
% 0.09/0.49 inference(forward_subsumption_resolution,[status(thm)],[f2998,f44])).
% 0.09/0.49 fof(f3022,plain,(
% 0.09/0.49 ![X0]: (leqNat(s(s(s(s(z)))),s(s(s(z))))|s(s(s(X0)))=s(z)|~sQ29_spl)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f2999,f146])).
% 0.09/0.49 fof(f3235,definition,(
% 0.09/0.49 ![X0]: (sQ56_spl <=> (s(s(s(X0)))=s(z)))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f3236,plain,(
% 0.09/0.49 ![X0]: (s(s(s(X0)))=s(z)|~sQ56_spl)),
% 0.09/0.49 inference(component_clause,[status(thm)],[f3235])).
% 0.09/0.49 fof(f3247,plain,(
% 0.09/0.49 sQ4_spl|sQ56_spl|~sQ29_spl),
% 0.09/0.49 inference(split_clause,[status(thm)],[f3022,f1637,f3235,f2830])).
% 0.09/0.49 fof(f3536,plain,(
% 0.09/0.49 ![X0]: (proj1S(s(z))=s(s(X0))|~sQ56_spl)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3236,f27])).
% 0.09/0.49 fof(f3542,plain,(
% 0.09/0.49 ![X0]: (z=s(s(X0))|~sQ56_spl)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f27,f3536])).
% 0.09/0.49 fof(f3543,plain,(
% 0.09/0.49 $false|~sQ56_spl),
% 0.09/0.49 inference(forward_subsumption_resolution,[status(thm)],[f3542,f28])).
% 0.09/0.49 fof(f3544,plain,(
% 0.09/0.49 ~sQ56_spl),
% 0.09/0.49 inference(contradiction_clause,[status(thm)],[f3543])).
% 0.09/0.49 fof(f3545,plain,(
% 0.09/0.49 $false),
% 0.09/0.49 inference(sat_refutation,[status(thm)],[f1773,f1777,f1798,f1804,f1806,f2218,f2224,f2226,f2833,f2839,f2891,f3247,f3544])).
% 0.09/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.51 % Elapsed time: 0.130639 seconds
% 0.09/0.51 % CPU time: 0.832433 seconds
% 0.09/0.51 % Total memory used: 124.415 MB
% 0.09/0.51 % Net memory used: 123.031 MB
%------------------------------------------------------------------------------