%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV571+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 1.22s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV571+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n012.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 07:27:36 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 1.22/0.70 % Refutation found
% 1.22/0.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.22/0.70 % SZS output start CNFRefutation for theBenchmark
% 1.22/0.70 fof(f1,axiom,(
% 1.22/0.70 (! [X,Y] :( subq(X,Y)<=> (! [Z] :( mem(Z,X)=> mem(Z,Y) ) )) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f2,axiom,(
% 1.22/0.70 (! [X,Y] :( subq(X,Y)=> ( subq(Y,X)=> X = Y ) ) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f4,axiom,(
% 1.22/0.70 (! [X] : ~ mem(X,e) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f5,axiom,(
% 1.22/0.70 (! [X,Y] :( mem(X,s(Y))<=> X = Y ) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f6,axiom,(
% 1.22/0.70 (! [X,Y,Z] :( mem(X,u(Y,Z))<=> ( mem(X,Y)| mem(X,Z) ) ) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f8,axiom,(
% 1.22/0.70 (! [X,Y] : a(X,Y) = u(X,s(Y)) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f9,axiom,(
% 1.22/0.70 (! [X] : n(X) = a(X,X) )),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f26,conjecture,(
% 1.22/0.70 ~ subq(u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),a(s(s(n(e))),n(n(n(e))))),u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),s(n(n(n(e)))))) ),
% 1.22/0.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.22/0.70 fof(f27,negated_conjecture,(
% 1.22/0.70 ~(~ subq(u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),a(s(s(n(e))),n(n(n(e))))),u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),s(n(n(n(e)))))) )),
% 1.22/0.70 inference(negated_conjecture,[status(cth)],[f26])).
% 1.22/0.70 fof(f28,plain,(
% 1.22/0.70 ![X,Y]: (subq(X,Y)<=>(![Z]: (~mem(Z,X)|mem(Z,Y))))),
% 1.22/0.70 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 1.22/0.70 fof(f29,plain,(
% 1.22/0.70 ![X,Y]: ((~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y))))&(subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 1.22/0.70 inference(NNF_transformation,[status(thm)],[f28])).
% 1.22/0.70 fof(f30,plain,(
% 1.22/0.70 (![X,Y]: (~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y)))))&(![X,Y]: (subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 1.22/0.70 inference(miniscoping,[status(thm)],[f29])).
% 1.22/0.70 fof(f31,plain,(
% 1.22/0.70 (![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))))),
% 1.22/0.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(Y,X))],[f30])).
% 1.22/0.70 fof(f32,plain,(
% 1.22/0.70 ![X0,X1,X2]: (~subq(X0,X1)|~mem(X2,X0)|mem(X2,X1))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f31])).
% 1.22/0.70 fof(f33,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,X1)|mem(sK0_skl(X1,X0),X0))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f31])).
% 1.22/0.70 fof(f34,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,X1)|~mem(sK0_skl(X1,X0),X1))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f31])).
% 1.22/0.70 fof(f35,plain,(
% 1.22/0.70 ![X,Y]: (~subq(X,Y)|(~subq(Y,X)|X=Y))),
% 1.22/0.70 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 1.22/0.70 fof(f36,plain,(
% 1.22/0.70 ![X0,X1]: (~subq(X0,X1)|~subq(X1,X0)|X0=X1)),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f35])).
% 1.22/0.70 fof(f44,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,e))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f4])).
% 1.22/0.70 fof(f45,plain,(
% 1.22/0.70 ![X,Y]: ((~mem(X,s(Y))|X=Y)&(mem(X,s(Y))|~X=Y))),
% 1.22/0.70 inference(NNF_transformation,[status(thm)],[f5])).
% 1.22/0.70 fof(f46,plain,(
% 1.22/0.70 (![X,Y]: (~mem(X,s(Y))|X=Y))&(![X,Y]: (mem(X,s(Y))|~X=Y))),
% 1.22/0.70 inference(miniscoping,[status(thm)],[f45])).
% 1.22/0.70 fof(f47,plain,(
% 1.22/0.70 ![X0,X1]: (~mem(X0,s(X1))|X0=X1)),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f46])).
% 1.22/0.70 fof(f48,plain,(
% 1.22/0.70 ![X0,X1]: (mem(X0,s(X1))|~X0=X1)),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f46])).
% 1.22/0.70 fof(f49,plain,(
% 1.22/0.70 ![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))))),
% 1.22/0.70 inference(NNF_transformation,[status(thm)],[f6])).
% 1.22/0.70 fof(f50,plain,(
% 1.22/0.70 (![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))))),
% 1.22/0.70 inference(miniscoping,[status(thm)],[f49])).
% 1.22/0.70 fof(f51,plain,(
% 1.22/0.70 ![X0,X1,X2]: (~mem(X0,u(X1,X2))|mem(X0,X1)|mem(X0,X2))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f50])).
% 1.22/0.70 fof(f52,plain,(
% 1.22/0.70 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X1))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f50])).
% 1.22/0.70 fof(f53,plain,(
% 1.22/0.70 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X2))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f50])).
% 1.22/0.70 fof(f59,plain,(
% 1.22/0.70 ![X0,X1]: (a(X0,X1)=u(X0,s(X1)))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f8])).
% 1.22/0.70 fof(f60,plain,(
% 1.22/0.70 ![X0]: (n(X0)=a(X0,X0))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f9])).
% 1.22/0.70 fof(f169,plain,(
% 1.22/0.70 subq(u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),a(s(s(n(e))),n(n(n(e))))),u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),s(n(n(n(e))))))),
% 1.22/0.70 inference(cnf_transformation,[status(thm)],[f27])).
% 1.22/0.70 fof(f170,plain,(
% 1.22/0.70 ![X0]: (mem(X0,s(X0)))),
% 1.22/0.70 inference(destructive_equality_resolution,[status(thm)],[f48])).
% 1.22/0.70 fof(f171,plain,(
% 1.22/0.70 subq(u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),a(s(s(n(e))),n(n(n(e))))),a(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),n(n(n(e)))))),
% 1.22/0.70 inference(backward_demodulation,[status(thm)],[f59,f169])).
% 1.22/0.70 fof(f181,plain,(
% 1.22/0.70 ![X0,X1,X2]: (mem(X0,a(X1,X2))|~mem(X0,X1))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f52])).
% 1.22/0.70 fof(f182,plain,(
% 1.22/0.70 ![X0,X1,X2]: (mem(X0,a(X1,X2))|~mem(X0,s(X2)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f53])).
% 1.22/0.70 fof(f184,plain,(
% 1.22/0.70 ![X0,X1]: (mem(X0,a(X1,X0)))),
% 1.22/0.70 inference(resolution,[status(thm)],[f182,f170])).
% 1.22/0.70 fof(f185,plain,(
% 1.22/0.70 ![X0]: (mem(X0,n(X0)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f184])).
% 1.22/0.70 fof(f188,plain,(
% 1.22/0.70 ![X0,X1,X2]: (~mem(X0,a(X1,X2))|mem(X0,X1)|mem(X0,s(X2)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f51])).
% 1.22/0.70 fof(f191,plain,(
% 1.22/0.70 ![X0,X1]: (~mem(X0,n(X1))|mem(X0,X1)|mem(X0,s(X1)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f188])).
% 1.22/0.70 fof(f194,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,u(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),a(s(s(n(e))),n(n(n(e))))))|mem(X0,a(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),n(n(n(e))))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f32,f171])).
% 1.22/0.70 fof(f195,plain,(
% 1.22/0.70 ![X0]: (mem(X0,a(u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))),n(n(n(e)))))|~mem(X0,a(s(s(n(e))),n(n(n(e))))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f194,f53])).
% 1.22/0.70 fof(f203,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(u(X0,X1),X2)|mem(sK0_skl(X2,u(X0,X1)),X0)|mem(sK0_skl(X2,u(X0,X1)),X1))),
% 1.22/0.70 inference(resolution,[status(thm)],[f33,f51])).
% 1.22/0.70 fof(f207,plain,(
% 1.22/0.70 ![X0]: (subq(X0,X0)|subq(X0,X0))),
% 1.22/0.70 inference(resolution,[status(thm)],[f34,f33])).
% 1.22/0.70 fof(f210,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X2))),
% 1.22/0.70 inference(resolution,[status(thm)],[f34,f53])).
% 1.22/0.70 fof(f211,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X1))),
% 1.22/0.70 inference(resolution,[status(thm)],[f34,f52])).
% 1.22/0.70 fof(f212,plain,(
% 1.22/0.70 ![X0]: (subq(X0,X0))),
% 1.22/0.70 inference(duplicate_literals_removal,[status(thm)],[f207])).
% 1.22/0.70 fof(f214,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,a(s(s(n(e))),n(n(n(e)))))|mem(X0,u(s(u(n(e),n(s(n(e))))),u(s(n(s(n(e)))),n(s(n(n(e)))))))|mem(X0,s(n(n(n(e))))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f195,f188])).
% 1.22/0.70 fof(f216,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,a(s(s(n(e))),n(n(n(e)))))|mem(X0,s(n(n(n(e)))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,u(s(n(s(n(e)))),n(s(n(n(e)))))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f214,f51])).
% 1.22/0.70 fof(f218,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,a(s(s(n(e))),n(n(n(e)))))|mem(X0,s(n(n(n(e)))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(n(s(n(e)))))|mem(X0,n(s(n(n(e))))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f216,f51])).
% 1.22/0.70 fof(f221,plain,(
% 1.22/0.70 ![X0]: (mem(X0,s(n(n(n(e)))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(n(s(n(e)))))|mem(X0,n(s(n(n(e)))))|~mem(X0,s(s(n(e)))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f218,f181])).
% 1.22/0.70 fof(f277,definition,(
% 1.22/0.70 sQ10_spl <=> (mem(n(n(e)),s(n(e))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f278,plain,(
% 1.22/0.70 mem(n(n(e)),s(n(e)))|~sQ10_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f277])).
% 1.22/0.70 fof(f300,plain,(
% 1.22/0.70 n(n(e))=n(e)|~sQ10_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f278,f47])).
% 1.22/0.70 fof(f303,plain,(
% 1.22/0.70 mem(n(e),n(e))|~sQ10_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f300,f185])).
% 1.22/0.70 fof(f305,plain,(
% 1.22/0.70 mem(n(e),e)|mem(n(e),s(e))|~sQ10_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f303,f191])).
% 1.22/0.70 fof(f306,definition,(
% 1.22/0.70 sQ13_spl <=> (mem(n(e),e))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f307,plain,(
% 1.22/0.70 mem(n(e),e)|~sQ13_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f306])).
% 1.22/0.70 fof(f309,definition,(
% 1.22/0.70 sQ14_spl <=> (mem(n(e),s(e)))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f310,plain,(
% 1.22/0.70 mem(n(e),s(e))|~sQ14_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f309])).
% 1.22/0.70 fof(f311,plain,(
% 1.22/0.70 ~mem(n(e),s(e))|sQ14_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f309])).
% 1.22/0.70 fof(f312,plain,(
% 1.22/0.70 sQ13_spl|sQ14_spl|~sQ10_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f305,f306,f309,f277])).
% 1.22/0.70 fof(f313,plain,(
% 1.22/0.70 $false|~sQ13_spl),
% 1.22/0.70 inference(forward_subsumption_resolution,[status(thm)],[f307,f44])).
% 1.22/0.70 fof(f314,plain,(
% 1.22/0.70 ~sQ13_spl),
% 1.22/0.70 inference(contradiction_clause,[status(thm)],[f313])).
% 1.22/0.70 fof(f316,plain,(
% 1.22/0.70 n(e)=e|~sQ14_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f310,f47])).
% 1.22/0.70 fof(f321,plain,(
% 1.22/0.70 mem(e,e)|~sQ14_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f316,f185])).
% 1.22/0.70 fof(f325,plain,(
% 1.22/0.70 $false|~sQ14_spl),
% 1.22/0.70 inference(forward_subsumption_resolution,[status(thm)],[f321,f44])).
% 1.22/0.70 fof(f326,plain,(
% 1.22/0.70 ~sQ14_spl),
% 1.22/0.70 inference(contradiction_clause,[status(thm)],[f325])).
% 1.22/0.70 fof(f344,plain,(
% 1.22/0.70 ![X0]: (subq(u(X0,X0),X0)|subq(u(X0,X0),X0))),
% 1.22/0.70 inference(resolution,[status(thm)],[f203,f34])).
% 1.22/0.70 fof(f371,plain,(
% 1.22/0.70 ![X0]: (subq(u(X0,X0),X0))),
% 1.22/0.70 inference(duplicate_literals_removal,[status(thm)],[f344])).
% 1.22/0.70 fof(f445,plain,(
% 1.22/0.70 ![X0]: (~subq(X0,u(X0,X0))|X0=u(X0,X0))),
% 1.22/0.70 inference(resolution,[status(thm)],[f371,f36])).
% 1.22/0.70 fof(f817,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,u(X1,X0))|subq(X0,u(X1,X0)))),
% 1.22/0.70 inference(resolution,[status(thm)],[f210,f33])).
% 1.22/0.70 fof(f832,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,u(X1,X0)))),
% 1.22/0.70 inference(duplicate_literals_removal,[status(thm)],[f817])).
% 1.22/0.70 fof(f1227,plain,(
% 1.22/0.70 ![X0]: (X0=u(X0,X0))),
% 1.22/0.70 inference(backward_subsumption_resolution,[status(thm)],[f445,f832])).
% 1.22/0.70 fof(f1229,plain,(
% 1.22/0.70 ![X0,X1]: (~subq(u(X0,X1),X1)|u(X0,X1)=X1)),
% 1.22/0.70 inference(resolution,[status(thm)],[f832,f36])).
% 1.22/0.70 fof(f1231,plain,(
% 1.22/0.70 ![X0,X1]: (subq(s(X0),a(X1,X0)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f832])).
% 1.22/0.70 fof(f1260,plain,(
% 1.22/0.70 ![X0]: (s(X0)=a(s(X0),X0))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f1227])).
% 1.22/0.70 fof(f1315,plain,(
% 1.22/0.70 ![X0]: (subq(s(X0),n(X0)))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f1231])).
% 1.22/0.70 fof(f1317,plain,(
% 1.22/0.70 ![X0]: (~subq(n(X0),s(X0))|n(X0)=s(X0))),
% 1.22/0.70 inference(resolution,[status(thm)],[f1315,f36])).
% 1.22/0.70 fof(f1336,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,u(a(X1,X2),X3))|~mem(sK0_skl(u(a(X1,X2),X3),X0),X1))),
% 1.22/0.70 inference(resolution,[status(thm)],[f211,f181])).
% 1.22/0.70 fof(f1337,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,u(u(X1,X2),X3))|~mem(sK0_skl(u(u(X1,X2),X3),X0),X2))),
% 1.22/0.70 inference(resolution,[status(thm)],[f211,f53])).
% 1.22/0.70 fof(f1389,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,u(a(X1,X2),s(X3)))|~mem(sK0_skl(a(a(X1,X2),X3),X0),X1))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f1336])).
% 1.22/0.70 fof(f1402,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,a(a(X1,X2),X3))|~mem(sK0_skl(a(a(X1,X2),X3),X0),X1))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f59,f1389])).
% 1.22/0.70 fof(f1417,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,u(u(X1,X2),s(X3)))|~mem(sK0_skl(a(u(X1,X2),X3),X0),X2))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f59,f1337])).
% 1.22/0.70 fof(f1430,plain,(
% 1.22/0.70 ![X0,X1,X2,X3]: (subq(X0,a(u(X1,X2),X3))|~mem(sK0_skl(a(u(X1,X2),X3),X0),X2))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f59,f1417])).
% 1.22/0.70 fof(f1473,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,a(a(X1,X2),a(X1,X2)))|~mem(sK0_skl(n(a(X1,X2)),X0),X1))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f1402])).
% 1.22/0.70 fof(f1485,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,n(a(X1,X2)))|~mem(sK0_skl(n(a(X1,X2)),X0),X1))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f60,f1473])).
% 1.22/0.70 fof(f1488,plain,(
% 1.22/0.70 ![X0,X1]: (subq(u(X0,X0),n(a(X0,X1)))|subq(u(X0,X0),n(a(X0,X1))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f1485,f203])).
% 1.22/0.70 fof(f1501,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(a(X0,X1)))|subq(u(X0,X0),n(a(X0,X1))))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f1227,f1488])).
% 1.22/0.70 fof(f1502,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(a(X0,X1)))|subq(X0,n(a(X0,X1))))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f1227,f1501])).
% 1.22/0.70 fof(f1503,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(a(X0,X1))))),
% 1.22/0.70 inference(duplicate_literals_removal,[status(thm)],[f1502])).
% 1.22/0.70 fof(f1514,plain,(
% 1.22/0.70 ![X0]: (subq(s(X0),n(s(X0))))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1260,f1503])).
% 1.22/0.70 fof(f1515,plain,(
% 1.22/0.70 ![X0]: (subq(X0,n(n(X0))))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f1503])).
% 1.22/0.70 fof(f1519,plain,(
% 1.22/0.70 ![X0]: (~subq(n(s(X0)),s(X0))|n(s(X0))=s(X0))),
% 1.22/0.70 inference(resolution,[status(thm)],[f1514,f36])).
% 1.22/0.70 fof(f1536,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(n(n(e)))))|mem(s(n(e)),s(u(n(e),n(s(n(e))))))|mem(s(n(e)),s(n(s(n(e)))))|mem(s(n(e)),n(s(n(n(e)))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f221,f170])).
% 1.22/0.70 fof(f1563,definition,(
% 1.22/0.70 sQ26_spl <=> (mem(s(n(e)),s(n(n(n(e))))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1564,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(n(n(e)))))|~sQ26_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1563])).
% 1.22/0.70 fof(f1566,definition,(
% 1.22/0.70 sQ27_spl <=> (mem(s(n(e)),s(u(n(e),n(s(n(e)))))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1567,plain,(
% 1.22/0.70 mem(s(n(e)),s(u(n(e),n(s(n(e))))))|~sQ27_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1566])).
% 1.22/0.70 fof(f1569,definition,(
% 1.22/0.70 sQ28_spl <=> (mem(s(n(e)),s(n(s(n(e))))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1570,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(s(n(e)))))|~sQ28_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1569])).
% 1.22/0.70 fof(f1572,definition,(
% 1.22/0.70 sQ29_spl <=> (mem(s(n(e)),n(s(n(n(e))))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1573,plain,(
% 1.22/0.70 mem(s(n(e)),n(s(n(n(e)))))|~sQ29_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1572])).
% 1.22/0.70 fof(f1575,plain,(
% 1.22/0.70 sQ26_spl|sQ27_spl|sQ28_spl|sQ29_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1536,f1563,f1566,f1569,f1572])).
% 1.22/0.70 fof(f1576,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(n(e))))|mem(s(n(e)),s(s(n(n(e)))))|~sQ29_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1573,f191])).
% 1.22/0.70 fof(f1577,definition,(
% 1.22/0.70 sQ30_spl <=> (mem(s(n(e)),s(n(n(e)))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1578,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(n(e))))|~sQ30_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1577])).
% 1.22/0.70 fof(f1580,definition,(
% 1.22/0.70 sQ31_spl <=> (mem(s(n(e)),s(s(n(n(e))))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1581,plain,(
% 1.22/0.70 mem(s(n(e)),s(s(n(n(e)))))|~sQ31_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1580])).
% 1.22/0.70 fof(f1583,plain,(
% 1.22/0.70 sQ30_spl|sQ31_spl|~sQ29_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1576,f1577,f1580,f1572])).
% 1.22/0.70 fof(f1586,plain,(
% 1.22/0.70 s(n(e))=n(n(e))|~sQ30_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1578,f47])).
% 1.22/0.70 fof(f1600,plain,(
% 1.22/0.70 ~subq(s(n(e)),s(n(e)))|n(n(e))=s(n(e))|~sQ30_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1586,f1317])).
% 1.22/0.70 fof(f1620,definition,(
% 1.22/0.70 sQ32_spl <=> (subq(s(n(e)),s(n(e))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1622,plain,(
% 1.22/0.70 ~subq(s(n(e)),s(n(e)))|sQ32_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1620])).
% 1.22/0.70 fof(f1623,definition,(
% 1.22/0.70 sQ33_spl <=> (n(n(e))=s(n(e)))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1624,plain,(
% 1.22/0.70 n(n(e))=s(n(e))|~sQ33_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1623])).
% 1.22/0.70 fof(f1626,plain,(
% 1.22/0.70 ~sQ32_spl|sQ33_spl|~sQ30_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1600,f1620,f1623,f1577])).
% 1.22/0.70 fof(f1627,plain,(
% 1.22/0.70 $false|sQ32_spl),
% 1.22/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1622,f212])).
% 1.22/0.70 fof(f1628,plain,(
% 1.22/0.70 sQ32_spl),
% 1.22/0.70 inference(contradiction_clause,[status(thm)],[f1627])).
% 1.22/0.70 fof(f1630,plain,(
% 1.22/0.70 subq(n(e),n(s(n(e))))|~sQ33_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1624,f1515])).
% 1.22/0.70 fof(f1637,plain,(
% 1.22/0.70 ![X0]: (~mem(X0,n(e))|mem(X0,n(s(n(e))))|~sQ33_spl)),
% 1.22/0.70 inference(resolution,[status(thm)],[f1630,f32])).
% 1.22/0.70 fof(f1658,definition,(
% 1.22/0.70 sQ37_spl <=> (n(s(n(e)))=s(n(e)))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f1659,plain,(
% 1.22/0.70 n(s(n(e)))=s(n(e))|~sQ37_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f1658])).
% 1.22/0.70 fof(f1676,plain,(
% 1.22/0.70 mem(s(n(e)),s(n(e)))|~sQ37_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1659,f185])).
% 1.22/0.70 fof(f1709,plain,(
% 1.22/0.70 s(n(e))=n(s(n(e)))|~sQ28_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1570,f47])).
% 1.22/0.70 fof(f1712,plain,(
% 1.22/0.70 ~subq(s(n(e)),s(n(e)))|n(s(n(e)))=s(n(e))|~sQ28_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1709,f1519])).
% 1.22/0.70 fof(f1720,plain,(
% 1.22/0.70 ~sQ32_spl|sQ37_spl|~sQ28_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1712,f1620,f1658,f1569])).
% 1.22/0.70 fof(f1736,plain,(
% 1.22/0.70 s(n(e))=n(e)|~sQ37_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1676,f47])).
% 1.22/0.70 fof(f1805,plain,(
% 1.22/0.70 mem(s(n(e)),n(e))|~sQ37_spl),
% 1.22/0.70 inference(backward_demodulation,[status(thm)],[f1736,f1676])).
% 1.22/0.70 fof(f1823,plain,(
% 1.22/0.70 mem(n(e),n(e))|~sQ37_spl),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f1736,f1805])).
% 1.22/0.70 fof(f1896,plain,(
% 1.22/0.70 mem(n(e),e)|mem(n(e),s(e))|~sQ37_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1823,f191])).
% 1.22/0.70 fof(f1897,plain,(
% 1.22/0.70 sQ13_spl|sQ14_spl|~sQ37_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1896,f306,f309,f1658])).
% 1.22/0.70 fof(f1900,plain,(
% 1.22/0.70 s(n(e))=s(n(n(e)))|~sQ31_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1581,f47])).
% 1.22/0.70 fof(f1916,plain,(
% 1.22/0.70 mem(n(n(e)),s(n(e)))|~sQ31_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f1900,f170])).
% 1.22/0.70 fof(f1941,plain,(
% 1.22/0.70 sQ10_spl|~sQ31_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f1916,f277,f1580])).
% 1.22/0.70 fof(f2014,plain,(
% 1.22/0.70 s(n(e))=n(n(n(e)))|~sQ26_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1564,f47])).
% 1.22/0.70 fof(f2021,plain,(
% 1.22/0.70 mem(n(n(e)),s(n(e)))|~sQ26_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f2014,f185])).
% 1.22/0.70 fof(f2027,plain,(
% 1.22/0.70 sQ10_spl|~sQ26_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f2021,f277,f1563])).
% 1.22/0.70 fof(f2051,plain,(
% 1.22/0.70 mem(e,n(s(n(e))))|~sQ33_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f1637,f185])).
% 1.22/0.70 fof(f2070,plain,(
% 1.22/0.70 mem(e,s(n(e)))|mem(e,s(s(n(e))))|~sQ33_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f2051,f191])).
% 1.22/0.70 fof(f2071,definition,(
% 1.22/0.70 sQ63_spl <=> (mem(e,s(n(e))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f2072,plain,(
% 1.22/0.70 mem(e,s(n(e)))|~sQ63_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f2071])).
% 1.22/0.70 fof(f2074,definition,(
% 1.22/0.70 sQ64_spl <=> (mem(e,s(s(n(e)))))),
% 1.22/0.70 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 1.22/0.70 fof(f2075,plain,(
% 1.22/0.70 mem(e,s(s(n(e))))|~sQ64_spl),
% 1.22/0.70 inference(component_clause,[status(thm)],[f2074])).
% 1.22/0.70 fof(f2077,plain,(
% 1.22/0.70 sQ63_spl|sQ64_spl|~sQ33_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f2070,f2071,f2074,f1623])).
% 1.22/0.70 fof(f2080,plain,(
% 1.22/0.70 e=n(e)|~sQ63_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f2072,f47])).
% 1.22/0.70 fof(f2088,plain,(
% 1.22/0.70 ~mem(e,s(e))|~sQ63_spl|sQ14_spl),
% 1.22/0.70 inference(backward_demodulation,[status(thm)],[f2080,f311])).
% 1.22/0.70 fof(f2109,plain,(
% 1.22/0.70 $false|~sQ63_spl|sQ14_spl),
% 1.22/0.70 inference(forward_subsumption_resolution,[status(thm)],[f2088,f170])).
% 1.22/0.70 fof(f2110,plain,(
% 1.22/0.70 ~sQ63_spl|sQ14_spl),
% 1.22/0.70 inference(contradiction_clause,[status(thm)],[f2109])).
% 1.22/0.70 fof(f2113,plain,(
% 1.22/0.70 e=s(n(e))|~sQ64_spl),
% 1.22/0.70 inference(resolution,[status(thm)],[f2075,f47])).
% 1.22/0.70 fof(f2129,plain,(
% 1.22/0.70 mem(n(e),e)|~sQ64_spl),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f2113,f170])).
% 1.22/0.70 fof(f2144,plain,(
% 1.22/0.70 sQ13_spl|~sQ64_spl),
% 1.22/0.70 inference(split_clause,[status(thm)],[f2129,f306,f2074])).
% 1.22/0.70 fof(f2172,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,a(u(X1,X2),u(X1,X2)))|~mem(sK0_skl(n(u(X1,X2)),X0),X2))),
% 1.22/0.70 inference(paramodulation,[status(thm)],[f60,f1430])).
% 1.22/0.70 fof(f2184,plain,(
% 1.22/0.70 ![X0,X1,X2]: (subq(X0,n(u(X1,X2)))|~mem(sK0_skl(n(u(X1,X2)),X0),X2))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f60,f2172])).
% 1.22/0.70 fof(f2187,plain,(
% 1.22/0.70 ![X0,X1]: (subq(u(X0,X0),n(u(X1,X0)))|subq(u(X0,X0),n(u(X1,X0))))),
% 1.22/0.70 inference(resolution,[status(thm)],[f2184,f203])).
% 1.22/0.70 fof(f2200,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(u(X1,X0)))|subq(u(X0,X0),n(u(X1,X0))))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f1227,f2187])).
% 1.22/0.70 fof(f2201,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(u(X1,X0)))|subq(X0,n(u(X1,X0))))),
% 1.22/0.70 inference(forward_demodulation,[status(thm)],[f1227,f2200])).
% 1.22/0.70 fof(f2202,plain,(
% 1.22/0.70 ![X0,X1]: (subq(X0,n(u(X1,X0))))),
% 1.22/0.70 inference(duplicate_literals_removal,[status(thm)],[f2201])).
% 1.22/0.71 fof(f2214,plain,(
% 1.22/0.71 ![X0]: (subq(X0,n(X0)))),
% 1.22/0.71 inference(paramodulation,[status(thm)],[f1227,f2202])).
% 1.22/0.71 fof(f2216,plain,(
% 1.22/0.71 ![X0]: (~subq(n(X0),X0)|n(X0)=X0)),
% 1.22/0.71 inference(resolution,[status(thm)],[f2214,f36])).
% 1.22/0.71 fof(f2421,plain,(
% 1.22/0.71 s(n(e))=u(n(e),n(s(n(e))))|~sQ27_spl),
% 1.22/0.71 inference(resolution,[status(thm)],[f1567,f47])).
% 1.22/0.71 fof(f2438,plain,(
% 1.22/0.71 ~subq(s(n(e)),n(s(n(e))))|u(n(e),n(s(n(e))))=n(s(n(e)))|~sQ27_spl),
% 1.22/0.71 inference(paramodulation,[status(thm)],[f2421,f1229])).
% 1.22/0.71 fof(f2478,definition,(
% 1.22/0.71 sQ74_spl <=> (subq(s(n(e)),n(s(n(e)))))),
% 1.22/0.71 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 1.22/0.71 fof(f2480,plain,(
% 1.22/0.71 ~subq(s(n(e)),n(s(n(e))))|sQ74_spl),
% 1.22/0.71 inference(component_clause,[status(thm)],[f2478])).
% 1.22/0.71 fof(f2481,definition,(
% 1.22/0.71 sQ75_spl <=> (u(n(e),n(s(n(e))))=n(s(n(e))))),
% 1.22/0.71 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 1.22/0.71 fof(f2482,plain,(
% 1.22/0.71 u(n(e),n(s(n(e))))=n(s(n(e)))|~sQ75_spl),
% 1.22/0.71 inference(component_clause,[status(thm)],[f2481])).
% 1.22/0.71 fof(f2484,plain,(
% 1.22/0.71 ~sQ74_spl|sQ75_spl|~sQ27_spl),
% 1.22/0.71 inference(split_clause,[status(thm)],[f2438,f2478,f2481,f1566])).
% 1.22/0.71 fof(f2499,plain,(
% 1.22/0.71 $false|sQ74_spl),
% 1.22/0.71 inference(forward_subsumption_resolution,[status(thm)],[f2480,f2214])).
% 1.22/0.71 fof(f2500,plain,(
% 1.22/0.71 sQ74_spl),
% 1.22/0.71 inference(contradiction_clause,[status(thm)],[f2499])).
% 1.22/0.71 fof(f2501,plain,(
% 1.22/0.71 s(n(e))=n(s(n(e)))|~sQ27_spl|~sQ75_spl),
% 1.22/0.71 inference(forward_demodulation,[status(thm)],[f2421,f2482])).
% 1.22/0.71 fof(f2576,plain,(
% 1.22/0.71 ~subq(s(n(e)),s(n(e)))|n(s(n(e)))=s(n(e))|~sQ27_spl|~sQ75_spl),
% 1.22/0.71 inference(paramodulation,[status(thm)],[f2501,f2216])).
% 1.22/0.71 fof(f2590,plain,(
% 1.22/0.71 ~sQ32_spl|sQ37_spl|~sQ27_spl|~sQ75_spl),
% 1.22/0.71 inference(split_clause,[status(thm)],[f2576,f1620,f1658,f1566,f2481])).
% 1.22/0.71 fof(f2593,plain,(
% 1.22/0.71 $false),
% 1.22/0.71 inference(sat_refutation,[status(thm)],[f312,f314,f326,f1575,f1583,f1626,f1628,f1720,f1897,f1941,f2027,f2077,f2110,f2144,f2484,f2500,f2590])).
% 1.22/0.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.22/0.74 % Elapsed time: 0.361412 seconds
% 1.22/0.74 % CPU time: 2.431763 seconds
% 1.22/0.74 % Total memory used: 162.043 MB
% 1.22/0.74 % Net memory used: 159.288 MB
%------------------------------------------------------------------------------