%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV568+1 : TPTP v9.3.1. Released v9.1.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 02:33:44 PM UTC 2026
% Result : Theorem 99.53s 18.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV568+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/5.40 % Computer : n020.cluster.edu
% 0.13/5.40 % Model : x86_64 x86_64
% 0.13/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.40 % Memory : 8046.5625MB
% 0.13/5.40 % OS : Linux 6.8.0-71-generic
% 0.13/5.40 % CPULimit : 300
% 0.13/5.40 % WCLimit : 300
% 0.13/5.40 % DateTime : Mon Sep 21 07:28:38 UTC 2026
% 0.13/5.40 % CPUTime :
% 0.13/5.42 % Drodi V4.1.1
% 99.53/18.20 % Refutation found
% 99.53/18.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 99.53/18.20 % SZS output start CNFRefutation for theBenchmark
% 99.53/18.20 fof(f1,axiom,(
% 99.53/18.20 (! [X,Y] :( subq(X,Y)<=> (! [Z] :( mem(Z,X)=> mem(Z,Y) ) )) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f2,axiom,(
% 99.53/18.20 (! [X,Y] :( subq(X,Y)=> ( subq(Y,X)=> X = Y ) ) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f4,axiom,(
% 99.53/18.20 (! [X] : ~ mem(X,e) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f5,axiom,(
% 99.53/18.20 (! [X,Y] :( mem(X,s(Y))<=> X = Y ) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f6,axiom,(
% 99.53/18.20 (! [X,Y,Z] :( mem(X,u(Y,Z))<=> ( mem(X,Y)| mem(X,Z) ) ) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f7,axiom,(
% 99.53/18.20 (! [X,Y,Z] :( mem(X,m(Y,Z))<=> ( mem(X,Y)& ~ mem(X,Z) ) ) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f8,axiom,(
% 99.53/18.20 (! [X,Y] : a(X,Y) = u(X,s(Y)) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f9,axiom,(
% 99.53/18.20 (! [X] : n(X) = a(X,X) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f10,axiom,(
% 99.53/18.20 (! [X,Y] :( mem(X,p(Y))<=> subq(X,Y) ) )),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f26,conjecture,(
% 99.53/18.20 ~ subq(u(a(s(s(n(e))),p(s(n(e)))),u(s(s(n(n(e)))),n(n(n(n(e)))))),u(a(n(s(n(e))),p(s(n(e)))),a(n(s(n(n(e)))),n(n(n(e)))))) ),
% 99.53/18.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 99.53/18.20 fof(f27,negated_conjecture,(
% 99.53/18.20 ~(~ subq(u(a(s(s(n(e))),p(s(n(e)))),u(s(s(n(n(e)))),n(n(n(n(e)))))),u(a(n(s(n(e))),p(s(n(e)))),a(n(s(n(n(e)))),n(n(n(e)))))) )),
% 99.53/18.20 inference(negated_conjecture,[status(cth)],[f26])).
% 99.53/18.20 fof(f28,plain,(
% 99.53/18.20 ![X,Y]: (subq(X,Y)<=>(![Z]: (~mem(Z,X)|mem(Z,Y))))),
% 99.53/18.20 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 99.53/18.20 fof(f29,plain,(
% 99.53/18.20 ![X,Y]: ((~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y))))&(subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 99.53/18.20 inference(NNF_transformation,[status(thm)],[f28])).
% 99.53/18.20 fof(f30,plain,(
% 99.53/18.20 (![X,Y]: (~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y)))))&(![X,Y]: (subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 99.53/18.20 inference(miniscoping,[status(thm)],[f29])).
% 99.53/18.20 fof(f31,plain,(
% 99.53/18.20 (![X,Y]: (~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y)))))&(![X,Y]: (subq(X,Y)|(mem(sK0_skl(Y,X),X)&~mem(sK0_skl(Y,X),Y))))),
% 99.53/18.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(Y,X))],[f30])).
% 99.53/18.20 fof(f32,plain,(
% 99.53/18.20 ![X0,X1,X2]: (~subq(X0,X1)|~mem(X2,X0)|mem(X2,X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f31])).
% 99.53/18.20 fof(f33,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,X1)|mem(sK0_skl(X1,X0),X0))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f31])).
% 99.53/18.20 fof(f34,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,X1)|~mem(sK0_skl(X1,X0),X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f31])).
% 99.53/18.20 fof(f35,plain,(
% 99.53/18.20 ![X,Y]: (~subq(X,Y)|(~subq(Y,X)|X=Y))),
% 99.53/18.20 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 99.53/18.20 fof(f36,plain,(
% 99.53/18.20 ![X0,X1]: (~subq(X0,X1)|~subq(X1,X0)|X0=X1)),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f35])).
% 99.53/18.20 fof(f44,plain,(
% 99.53/18.20 ![X0]: (~mem(X0,e))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f4])).
% 99.53/18.20 fof(f45,plain,(
% 99.53/18.20 ![X,Y]: ((~mem(X,s(Y))|X=Y)&(mem(X,s(Y))|~X=Y))),
% 99.53/18.20 inference(NNF_transformation,[status(thm)],[f5])).
% 99.53/18.20 fof(f46,plain,(
% 99.53/18.20 (![X,Y]: (~mem(X,s(Y))|X=Y))&(![X,Y]: (mem(X,s(Y))|~X=Y))),
% 99.53/18.20 inference(miniscoping,[status(thm)],[f45])).
% 99.53/18.20 fof(f47,plain,(
% 99.53/18.20 ![X0,X1]: (~mem(X0,s(X1))|X0=X1)),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f46])).
% 99.53/18.20 fof(f48,plain,(
% 99.53/18.20 ![X0,X1]: (mem(X0,s(X1))|~X0=X1)),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f46])).
% 99.53/18.20 fof(f49,plain,(
% 99.53/18.20 ![X,Y,Z]: ((~mem(X,u(Y,Z))|(mem(X,Y)|mem(X,Z)))&(mem(X,u(Y,Z))|(~mem(X,Y)&~mem(X,Z))))),
% 99.53/18.20 inference(NNF_transformation,[status(thm)],[f6])).
% 99.53/18.20 fof(f50,plain,(
% 99.53/18.20 (![X,Y,Z]: (~mem(X,u(Y,Z))|(mem(X,Y)|mem(X,Z))))&(![X,Y,Z]: (mem(X,u(Y,Z))|(~mem(X,Y)&~mem(X,Z))))),
% 99.53/18.20 inference(miniscoping,[status(thm)],[f49])).
% 99.53/18.20 fof(f51,plain,(
% 99.53/18.20 ![X0,X1,X2]: (~mem(X0,u(X1,X2))|mem(X0,X1)|mem(X0,X2))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f50])).
% 99.53/18.20 fof(f52,plain,(
% 99.53/18.20 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f50])).
% 99.53/18.20 fof(f53,plain,(
% 99.53/18.20 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X2))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f50])).
% 99.53/18.20 fof(f54,plain,(
% 99.53/18.20 ![X,Y,Z]: ((~mem(X,m(Y,Z))|(mem(X,Y)&~mem(X,Z)))&(mem(X,m(Y,Z))|(~mem(X,Y)|mem(X,Z))))),
% 99.53/18.20 inference(NNF_transformation,[status(thm)],[f7])).
% 99.53/18.20 fof(f55,plain,(
% 99.53/18.20 (![X,Y,Z]: (~mem(X,m(Y,Z))|(mem(X,Y)&~mem(X,Z))))&(![X,Y,Z]: (mem(X,m(Y,Z))|(~mem(X,Y)|mem(X,Z))))),
% 99.53/18.20 inference(miniscoping,[status(thm)],[f54])).
% 99.53/18.20 fof(f56,plain,(
% 99.53/18.20 ![X0,X1,X2]: (~mem(X0,m(X1,X2))|mem(X0,X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f55])).
% 99.53/18.20 fof(f59,plain,(
% 99.53/18.20 ![X0,X1]: (a(X0,X1)=u(X0,s(X1)))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f8])).
% 99.53/18.20 fof(f60,plain,(
% 99.53/18.20 ![X0]: (n(X0)=a(X0,X0))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f9])).
% 99.53/18.20 fof(f61,plain,(
% 99.53/18.20 ![X,Y]: ((~mem(X,p(Y))|subq(X,Y))&(mem(X,p(Y))|~subq(X,Y)))),
% 99.53/18.20 inference(NNF_transformation,[status(thm)],[f10])).
% 99.53/18.20 fof(f62,plain,(
% 99.53/18.20 (![X,Y]: (~mem(X,p(Y))|subq(X,Y)))&(![X,Y]: (mem(X,p(Y))|~subq(X,Y)))),
% 99.53/18.20 inference(miniscoping,[status(thm)],[f61])).
% 99.53/18.20 fof(f63,plain,(
% 99.53/18.20 ![X0,X1]: (~mem(X0,p(X1))|subq(X0,X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f62])).
% 99.53/18.20 fof(f64,plain,(
% 99.53/18.20 ![X0,X1]: (mem(X0,p(X1))|~subq(X0,X1))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f62])).
% 99.53/18.20 fof(f169,plain,(
% 99.53/18.20 subq(u(a(s(s(n(e))),p(s(n(e)))),u(s(s(n(n(e)))),n(n(n(n(e)))))),u(a(n(s(n(e))),p(s(n(e)))),a(n(s(n(n(e)))),n(n(n(e))))))),
% 99.53/18.20 inference(cnf_transformation,[status(thm)],[f27])).
% 99.53/18.20 fof(f170,plain,(
% 99.53/18.20 ![X0]: (mem(X0,s(X0)))),
% 99.53/18.20 inference(destructive_equality_resolution,[status(thm)],[f48])).
% 99.53/18.20 fof(f173,plain,(
% 99.53/18.20 ![X0,X1,X2]: (mem(X0,a(X1,X2))|~mem(X0,X1))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f59,f52])).
% 99.53/18.20 fof(f177,plain,(
% 99.53/18.20 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X2))),
% 99.53/18.20 inference(resolution,[status(thm)],[f34,f53])).
% 99.53/18.20 fof(f178,plain,(
% 99.53/18.20 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X1))),
% 99.53/18.20 inference(resolution,[status(thm)],[f34,f52])).
% 99.53/18.20 fof(f179,plain,(
% 99.53/18.20 ![X0]: (~mem(X0,u(a(s(s(n(e))),p(s(n(e)))),u(s(s(n(n(e)))),n(n(n(n(e)))))))|mem(X0,u(a(n(s(n(e))),p(s(n(e)))),a(n(s(n(n(e)))),n(n(n(e)))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f32,f169])).
% 99.53/18.20 fof(f182,plain,(
% 99.53/18.20 ![X0,X1,X2]: (~mem(X0,a(X1,X2))|mem(X0,X1)|mem(X0,s(X2)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f59,f51])).
% 99.53/18.20 fof(f183,plain,(
% 99.53/18.20 ![X0,X1]: (~mem(X0,n(X1))|mem(X0,X1)|mem(X0,s(X1)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f60,f182])).
% 99.53/18.20 fof(f187,plain,(
% 99.53/18.20 ![X0,X1,X2]: (subq(u(X0,X1),X2)|mem(sK0_skl(X2,u(X0,X1)),X0)|mem(sK0_skl(X2,u(X0,X1)),X1))),
% 99.53/18.20 inference(resolution,[status(thm)],[f33,f51])).
% 99.53/18.20 fof(f189,plain,(
% 99.53/18.20 ![X0,X1,X2]: (subq(m(X0,X1),X2)|mem(sK0_skl(X2,m(X0,X1)),X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f33,f56])).
% 99.53/18.20 fof(f191,plain,(
% 99.53/18.20 ![X0,X1]: (subq(s(X0),X1)|sK0_skl(X1,s(X0))=X0)),
% 99.53/18.20 inference(resolution,[status(thm)],[f33,f47])).
% 99.53/18.20 fof(f192,plain,(
% 99.53/18.20 ![X0]: (subq(e,X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f33,f44])).
% 99.53/18.20 fof(f195,plain,(
% 99.53/18.20 ![X0,X1,X2]: (sK0_skl(X0,s(X1))=X1|~mem(X2,s(X1))|mem(X2,X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f191,f32])).
% 99.53/18.20 fof(f200,plain,(
% 99.53/18.20 ![X0,X1]: (sK0_skl(X0,s(X1))=X1|mem(X1,X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f195,f170])).
% 99.53/18.20 fof(f207,plain,(
% 99.53/18.20 ![X0,X1]: (sK0_skl(p(X0),s(X1))=X1|subq(X1,X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f200,f63])).
% 99.53/18.20 fof(f211,plain,(
% 99.53/18.20 ![X0]: (subq(u(X0,X0),X0)|subq(u(X0,X0),X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f187,f34])).
% 99.53/18.20 fof(f212,plain,(
% 99.53/18.20 ![X0,X1]: (subq(u(X0,X1),X0)|mem(sK0_skl(X0,u(X0,X1)),X1)|subq(u(X0,X1),X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f187,f34])).
% 99.53/18.20 fof(f218,plain,(
% 99.53/18.20 ![X0,X1,X2,X3]: (subq(u(u(X0,X1),X2),X3)|mem(sK0_skl(X3,u(u(X0,X1),X2)),X2)|mem(sK0_skl(X3,u(u(X0,X1),X2)),X0)|mem(sK0_skl(X3,u(u(X0,X1),X2)),X1))),
% 99.53/18.20 inference(resolution,[status(thm)],[f187,f51])).
% 99.53/18.20 fof(f243,plain,(
% 99.53/18.20 ![X0]: (subq(u(X0,X0),X0))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f211])).
% 99.53/18.20 fof(f244,plain,(
% 99.53/18.20 ![X0,X1]: (subq(u(X0,X1),X0)|mem(sK0_skl(X0,u(X0,X1)),X1))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f212])).
% 99.53/18.20 fof(f308,plain,(
% 99.53/18.20 ![X0,X1]: (sK0_skl(p(X0),s(X1))=X1|~subq(X0,X1)|X0=X1)),
% 99.53/18.20 inference(resolution,[status(thm)],[f207,f36])).
% 99.53/18.20 fof(f346,plain,(
% 99.53/18.20 ![X0,X1]: (subq(u(X0,s(X1)),X0)|sK0_skl(X0,u(X0,s(X1)))=X1)),
% 99.53/18.20 inference(resolution,[status(thm)],[f244,f47])).
% 99.53/18.20 fof(f352,plain,(
% 99.53/18.20 ![X0,X1]: (subq(a(X0,X1),X0)|sK0_skl(X0,u(X0,s(X1)))=X1)),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f59,f346])).
% 99.53/18.20 fof(f353,plain,(
% 99.53/18.20 ![X0,X1]: (subq(a(X0,X1),X0)|sK0_skl(X0,a(X0,X1))=X1)),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f59,f352])).
% 99.53/18.20 fof(f360,plain,(
% 99.53/18.20 ![X0]: (subq(n(X0),X0)|sK0_skl(X0,a(X0,X0))=X0)),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f60,f353])).
% 99.53/18.20 fof(f361,plain,(
% 99.53/18.20 ![X0]: (subq(n(X0),X0)|sK0_skl(X0,n(X0))=X0)),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f60,f360])).
% 99.53/18.20 fof(f840,plain,(
% 99.53/18.20 ![X0,X1]: (subq(m(X0,X1),X0)|subq(m(X0,X1),X0))),
% 99.53/18.20 inference(resolution,[status(thm)],[f189,f34])).
% 99.53/18.20 fof(f851,plain,(
% 99.53/18.20 ![X0,X1]: (subq(m(X0,X1),X0))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f840])).
% 99.53/18.20 fof(f1111,plain,(
% 99.53/18.20 ![X0]: (mem(X0,u(a(n(s(n(e))),p(s(n(e)))),a(n(s(n(n(e)))),n(n(n(e))))))|~mem(X0,u(s(s(n(n(e)))),n(n(n(n(e)))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f179,f53])).
% 99.53/18.20 fof(f1128,plain,(
% 99.53/18.20 ![X0]: (~subq(X0,e)|X0=e)),
% 99.53/18.20 inference(resolution,[status(thm)],[f192,f36])).
% 99.53/18.20 fof(f1132,plain,(
% 99.53/18.20 ![X0]: (sK0_skl(p(u(X0,X0)),s(X0))=X0|u(X0,X0)=X0)),
% 99.53/18.20 inference(resolution,[status(thm)],[f243,f308])).
% 99.53/18.20 fof(f1142,plain,(
% 99.53/18.20 ![X0,X1]: (mem(X0,n(X1))|~mem(X0,X1))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f60,f173])).
% 99.53/18.20 fof(f1164,plain,(
% 99.53/18.20 n(e)=e|sK0_skl(e,n(e))=e),
% 99.53/18.20 inference(resolution,[status(thm)],[f1128,f361])).
% 99.53/18.20 fof(f1297,plain,(
% 99.53/18.20 ![X0]: (subq(s(X0),p(u(X0,X0)))|~mem(X0,p(u(X0,X0)))|u(X0,X0)=X0)),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f1132,f34])).
% 99.53/18.20 fof(f1301,plain,(
% 99.53/18.20 ![X0,X1]: (~mem(X0,p(u(X0,X0)))|u(X0,X0)=X0|~mem(X1,s(X0))|mem(X1,p(u(X0,X0))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f1297,f32])).
% 99.53/18.20 fof(f1308,plain,(
% 99.53/18.20 ![X0,X1]: (~mem(X0,p(u(X0,X0)))|u(X0,X0)=X0|~mem(X1,s(X0))|subq(X1,u(X0,X0)))),
% 99.53/18.20 inference(resolution,[status(thm)],[f1301,f63])).
% 99.53/18.20 fof(f1314,plain,(
% 99.53/18.20 ![X0,X1]: (u(X0,X0)=X0|~mem(X1,s(X0))|subq(X1,u(X0,X0))|~subq(X0,u(X0,X0)))),
% 99.53/18.20 inference(resolution,[status(thm)],[f1308,f64])).
% 99.53/18.20 fof(f1325,plain,(
% 99.53/18.20 ![X0,X1]: (u(X0,X0)=X0|~mem(X1,s(X0))|~subq(X0,u(X0,X0))|~subq(u(X0,X0),X1)|u(X0,X0)=X1)),
% 99.53/18.20 inference(resolution,[status(thm)],[f1314,f36])).
% 99.53/18.20 fof(f1818,plain,(
% 99.53/18.20 subq(n(e),e)|mem(e,n(e))|n(e)=e),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f1164,f33])).
% 99.53/18.20 fof(f1820,plain,(
% 99.53/18.20 mem(e,n(e))|n(e)=e),
% 99.53/18.20 inference(forward_subsumption_resolution,[status(thm)],[f1818,f1128])).
% 99.53/18.20 fof(f2972,plain,(
% 99.53/18.20 ![X0]: (~mem(X0,u(s(s(n(n(e)))),n(n(n(n(e))))))|mem(X0,a(n(s(n(e))),p(s(n(e)))))|mem(X0,a(n(s(n(n(e)))),n(n(n(e))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f1111,f51])).
% 99.53/18.20 fof(f3450,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X1,X0))|subq(X0,u(X1,X0)))),
% 99.53/18.20 inference(resolution,[status(thm)],[f177,f33])).
% 99.53/18.20 fof(f3598,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X1,X0)))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f3450])).
% 99.53/18.20 fof(f3631,plain,(
% 99.53/18.20 ![X0,X1]: (u(X0,X0)=X0|~mem(X1,s(X0))|~subq(u(X0,X0),X1)|u(X0,X0)=X1)),
% 99.53/18.20 inference(backward_subsumption_resolution,[status(thm)],[f1325,f3598])).
% 99.53/18.20 fof(f3639,plain,(
% 99.53/18.20 ![X0,X1]: (subq(s(X0),a(X1,X0)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f59,f3598])).
% 99.53/18.20 fof(f3645,plain,(
% 99.53/18.20 ![X0]: (subq(s(X0),n(X0)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f60,f3639])).
% 99.53/18.20 fof(f3906,plain,(
% 99.53/18.20 ![X0]: (mem(X0,a(n(s(n(e))),p(s(n(e)))))|mem(X0,a(n(s(n(n(e)))),n(n(n(e)))))|~mem(X0,n(n(n(n(e))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f2972,f53])).
% 99.53/18.20 fof(f3930,plain,(
% 99.53/18.20 ![X0]: (mem(X0,a(n(s(n(e))),p(s(n(e)))))|~mem(X0,n(n(n(n(e)))))|mem(X0,n(s(n(n(e)))))|mem(X0,s(n(n(n(e))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f3906,f182])).
% 99.53/18.20 fof(f3948,plain,(
% 99.53/18.20 ![X0]: (~mem(X0,n(n(n(n(e)))))|mem(X0,n(s(n(n(e)))))|mem(X0,s(n(n(n(e)))))|mem(X0,n(s(n(e))))|mem(X0,s(p(s(n(e))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f3930,f182])).
% 99.53/18.20 fof(f4039,plain,(
% 99.53/18.20 ![X0]: (mem(X0,n(s(n(n(e)))))|mem(X0,s(n(n(n(e)))))|mem(X0,n(s(n(e))))|mem(X0,s(p(s(n(e)))))|~mem(X0,n(n(n(e)))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f3948,f1142])).
% 99.53/18.20 fof(f4067,plain,(
% 99.53/18.20 ![X0]: (mem(X0,s(n(n(n(e)))))|mem(X0,n(s(n(e))))|mem(X0,s(p(s(n(e)))))|~mem(X0,n(n(n(e))))|mem(X0,s(n(n(e))))|mem(X0,s(s(n(n(e))))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f4039,f183])).
% 99.53/18.20 fof(f4473,plain,(
% 99.53/18.20 ![X0]: (u(X0,X0)=X0|~mem(X0,s(X0))|u(X0,X0)=X0)),
% 99.53/18.20 inference(resolution,[status(thm)],[f3631,f243])).
% 99.53/18.20 fof(f4486,plain,(
% 99.53/18.20 ![X0]: (u(X0,X0)=X0|~mem(X0,s(X0)))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f4473])).
% 99.53/18.20 fof(f4487,plain,(
% 99.53/18.20 ![X0]: (u(X0,X0)=X0)),
% 99.53/18.20 inference(forward_subsumption_resolution,[status(thm)],[f4486,f170])).
% 99.53/18.20 fof(f7906,plain,(
% 99.53/18.20 ![X0,X1]: (subq(u(u(X0,X0),X0),u(X0,X1))|subq(u(u(X0,X0),X0),u(X0,X1)))),
% 99.53/18.20 inference(resolution,[status(thm)],[f178,f218])).
% 99.53/18.20 fof(f8007,plain,(
% 99.53/18.20 ![X0,X1]: (subq(u(X0,X0),u(X0,X1))|subq(u(u(X0,X0),X0),u(X0,X1)))),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f4487,f7906])).
% 99.53/18.20 fof(f8008,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X0,X1))|subq(u(u(X0,X0),X0),u(X0,X1)))),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f4487,f8007])).
% 99.53/18.20 fof(f8009,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X0,X1))|subq(u(X0,X0),u(X0,X1)))),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f4487,f8008])).
% 99.53/18.20 fof(f8010,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X0,X1))|subq(X0,u(X0,X1)))),
% 99.53/18.20 inference(forward_demodulation,[status(thm)],[f4487,f8009])).
% 99.53/18.20 fof(f8011,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,u(X0,X1)))),
% 99.53/18.20 inference(duplicate_literals_removal,[status(thm)],[f8010])).
% 99.53/18.20 fof(f8088,plain,(
% 99.53/18.20 ![X0,X1]: (subq(X0,a(X0,X1)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f59,f8011])).
% 99.53/18.20 fof(f10857,plain,(
% 99.53/18.20 ![X0]: (subq(X0,n(X0)))),
% 99.53/18.20 inference(paramodulation,[status(thm)],[f60,f8088])).
% 99.53/18.20 fof(f12538,plain,(
% 99.53/18.20 ![X0]: (mem(X0,n(s(n(e))))|mem(X0,s(p(s(n(e)))))|~mem(X0,n(n(n(e))))|mem(X0,s(n(n(e))))|mem(X0,s(s(n(n(e)))))|X0=n(n(n(e))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f4067,f47])).
% 99.53/18.20 fof(f12559,plain,(
% 99.53/18.20 ![X0]: (mem(X0,n(s(n(e))))|mem(X0,s(p(s(n(e)))))|~mem(X0,n(n(n(e))))|mem(X0,s(n(n(e))))|X0=n(n(n(e)))|X0=s(n(n(e))))),
% 99.53/18.20 inference(resolution,[status(thm)],[f12538,f47])).
% 99.53/18.20 fof(f12580,plain,(
% 99.53/18.21 ![X0]: (mem(X0,n(s(n(e))))|~mem(X0,n(n(n(e))))|mem(X0,s(n(n(e))))|X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e))))),
% 99.53/18.21 inference(resolution,[status(thm)],[f12559,f47])).
% 99.53/18.21 fof(f18523,plain,(
% 99.53/18.21 ![X0]: (mem(X0,n(s(n(e))))|mem(X0,s(n(n(e))))|X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|~mem(X0,n(n(e))))),
% 99.53/18.21 inference(resolution,[status(thm)],[f12580,f1142])).
% 99.53/18.21 fof(f18836,plain,(
% 99.53/18.21 ![X0]: (mem(X0,s(n(n(e))))|X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|~mem(X0,n(n(e)))|mem(X0,s(n(e)))|mem(X0,s(s(n(e)))))),
% 99.53/18.21 inference(resolution,[status(thm)],[f18523,f183])).
% 99.53/18.21 fof(f18901,plain,(
% 99.53/18.21 ![X0]: (X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|~mem(X0,n(n(e)))|mem(X0,s(n(e)))|mem(X0,s(s(n(e))))|X0=n(n(e)))),
% 99.53/18.21 inference(resolution,[status(thm)],[f18836,f47])).
% 99.53/18.21 fof(f22618,plain,(
% 99.53/18.21 ![X0]: (X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|~mem(X0,n(n(e)))|mem(X0,s(n(e)))|X0=n(n(e))|X0=s(n(e)))),
% 99.53/18.21 inference(resolution,[status(thm)],[f18901,f47])).
% 99.53/18.21 fof(f23438,plain,(
% 99.53/18.21 ![X0]: (X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|mem(X0,s(n(e)))|X0=n(n(e))|X0=s(n(e))|~mem(X0,n(e)))),
% 99.53/18.21 inference(resolution,[status(thm)],[f22618,f1142])).
% 99.53/18.21 fof(f23979,plain,(
% 99.53/18.21 ![X0]: (X0=n(n(n(e)))|X0=s(n(n(e)))|X0=p(s(n(e)))|X0=n(n(e))|X0=s(n(e))|~mem(X0,n(e))|X0=n(e))),
% 99.53/18.21 inference(resolution,[status(thm)],[f23438,f47])).
% 99.53/18.21 fof(f24003,plain,(
% 99.53/18.21 e=n(n(n(e)))|e=s(n(n(e)))|e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)|n(e)=e),
% 99.53/18.21 inference(resolution,[status(thm)],[f23979,f1820])).
% 99.53/18.21 fof(f24182,plain,(
% 99.53/18.21 e=n(n(n(e)))|e=s(n(n(e)))|e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.21 inference(duplicate_literals_removal,[status(thm)],[f24003])).
% 99.53/18.21 fof(f24820,plain,(
% 99.53/18.21 subq(n(n(e)),e)|e=s(n(n(e)))|e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.21 inference(paramodulation,[status(thm)],[f24182,f10857])).
% 99.53/18.21 fof(f24837,plain,(
% 99.53/18.21 e=s(n(n(e)))|e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.21 inference(forward_subsumption_resolution,[status(thm)],[f24820,f1128])).
% 99.53/18.21 fof(f24931,plain,(
% 99.53/18.21 mem(n(n(e)),e)|e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.21 inference(paramodulation,[status(thm)],[f24837,f170])).
% 99.53/18.21 fof(f24973,plain,(
% 99.53/18.26 e=p(s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.26 inference(forward_subsumption_resolution,[status(thm)],[f24931,f44])).
% 99.53/18.26 fof(f28499,plain,(
% 99.53/18.26 ![X0]: (mem(X0,e)|~subq(X0,s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e))),
% 99.53/18.26 inference(paramodulation,[status(thm)],[f24973,f64])).
% 99.53/18.26 fof(f28533,plain,(
% 99.53/18.26 ![X0]: (~subq(X0,s(n(e)))|e=n(n(e))|e=s(n(e))|e=n(e))),
% 99.53/18.26 inference(forward_subsumption_resolution,[status(thm)],[f28499,f44])).
% 99.53/18.26 fof(f28536,plain,(
% 99.53/18.26 e=n(n(e))|e=s(n(e))|e=n(e)),
% 99.53/18.26 inference(resolution,[status(thm)],[f28533,f851])).
% 99.53/18.26 fof(f28693,plain,(
% 99.53/18.26 subq(n(e),e)|e=s(n(e))|e=n(e)),
% 99.53/18.26 inference(paramodulation,[status(thm)],[f28536,f10857])).
% 99.53/18.26 fof(f28793,plain,(
% 99.53/18.26 e=s(n(e))|e=n(e)),
% 99.53/18.26 inference(forward_subsumption_resolution,[status(thm)],[f28693,f1128])).
% 99.53/18.26 fof(f29003,plain,(
% 99.53/18.26 mem(n(e),e)|e=n(e)),
% 99.53/18.26 inference(paramodulation,[status(thm)],[f28793,f170])).
% 99.53/18.26 fof(f29047,plain,(
% 99.53/18.26 e=n(e)),
% 99.53/18.26 inference(forward_subsumption_resolution,[status(thm)],[f29003,f44])).
% 99.53/18.26 fof(f32190,plain,(
% 99.53/18.26 subq(s(e),e)),
% 99.53/18.26 inference(paramodulation,[status(thm)],[f29047,f3645])).
% 99.53/18.26 fof(f33397,plain,(
% 99.53/18.26 ![X0]: (~mem(X0,s(e))|mem(X0,e))),
% 99.53/18.26 inference(resolution,[status(thm)],[f32190,f32])).
% 99.53/18.26 fof(f33399,plain,(
% 99.53/18.26 ![X0]: (~mem(X0,s(e)))),
% 99.53/18.26 inference(forward_subsumption_resolution,[status(thm)],[f33397,f44])).
% 99.53/18.26 fof(f33666,plain,(
% 99.53/18.26 $false),
% 99.53/18.26 inference(resolution,[status(thm)],[f33399,f170])).
% 99.53/18.26 % SZS output end CNFRefutation for theBenchmark.p
% 12.47/18.41 % Elapsed time: 12.985496 seconds
% 12.47/18.41 % CPU time: 101.973527 seconds
% 12.47/18.41 % Total memory used: 727.309 MB
% 12.47/18.41 % Net memory used: 689.264 MB
%------------------------------------------------------------------------------