%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV569+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 : n006.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 0.27s 1.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV569+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n006.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 07:27:28 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.27/1.10 % Refutation found
% 0.27/1.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/1.10 % SZS output start CNFRefutation for theBenchmark
% 0.27/1.10 fof(f1,axiom,(
% 0.27/1.10 (! [X,Y] :( subq(X,Y)<=> (! [Z] :( mem(Z,X)=> mem(Z,Y) ) )) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f2,axiom,(
% 0.27/1.10 (! [X,Y] :( subq(X,Y)=> ( subq(Y,X)=> X = Y ) ) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f4,axiom,(
% 0.27/1.10 (! [X] : ~ mem(X,e) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f5,axiom,(
% 0.27/1.10 (! [X,Y] :( mem(X,s(Y))<=> X = Y ) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f6,axiom,(
% 0.27/1.10 (! [X,Y,Z] :( mem(X,u(Y,Z))<=> ( mem(X,Y)| mem(X,Z) ) ) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f8,axiom,(
% 0.27/1.10 (! [X,Y] : a(X,Y) = u(X,s(Y)) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f9,axiom,(
% 0.27/1.10 (! [X] : n(X) = a(X,X) )),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f26,conjecture,(
% 0.27/1.10 ~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))) ),
% 0.27/1.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.10 fof(f27,negated_conjecture,(
% 0.27/1.10 ~(~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))) )),
% 0.27/1.10 inference(negated_conjecture,[status(cth)],[f26])).
% 0.27/1.10 fof(f28,plain,(
% 0.27/1.10 ![X,Y]: (subq(X,Y)<=>(![Z]: (~mem(Z,X)|mem(Z,Y))))),
% 0.27/1.10 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.27/1.10 fof(f29,plain,(
% 0.27/1.10 ![X,Y]: ((~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y))))&(subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 0.27/1.10 inference(NNF_transformation,[status(thm)],[f28])).
% 0.27/1.10 fof(f30,plain,(
% 0.27/1.10 (![X,Y]: (~subq(X,Y)|(![Z]: (~mem(Z,X)|mem(Z,Y)))))&(![X,Y]: (subq(X,Y)|(?[Z]: (mem(Z,X)&~mem(Z,Y)))))),
% 0.27/1.10 inference(miniscoping,[status(thm)],[f29])).
% 0.27/1.10 fof(f31,plain,(
% 0.27/1.10 (![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))))),
% 0.27/1.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(Y,X))],[f30])).
% 0.27/1.10 fof(f32,plain,(
% 0.27/1.10 ![X0,X1,X2]: (~subq(X0,X1)|~mem(X2,X0)|mem(X2,X1))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f31])).
% 0.27/1.10 fof(f33,plain,(
% 0.27/1.10 ![X0,X1]: (subq(X0,X1)|mem(sK0_skl(X1,X0),X0))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f31])).
% 0.27/1.10 fof(f34,plain,(
% 0.27/1.10 ![X0,X1]: (subq(X0,X1)|~mem(sK0_skl(X1,X0),X1))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f31])).
% 0.27/1.10 fof(f35,plain,(
% 0.27/1.10 ![X,Y]: (~subq(X,Y)|(~subq(Y,X)|X=Y))),
% 0.27/1.10 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.27/1.10 fof(f36,plain,(
% 0.27/1.10 ![X0,X1]: (~subq(X0,X1)|~subq(X1,X0)|X0=X1)),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/1.10 fof(f44,plain,(
% 0.27/1.10 ![X0]: (~mem(X0,e))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f4])).
% 0.27/1.10 fof(f45,plain,(
% 0.27/1.10 ![X,Y]: ((~mem(X,s(Y))|X=Y)&(mem(X,s(Y))|~X=Y))),
% 0.27/1.10 inference(NNF_transformation,[status(thm)],[f5])).
% 0.27/1.10 fof(f46,plain,(
% 0.27/1.10 (![X,Y]: (~mem(X,s(Y))|X=Y))&(![X,Y]: (mem(X,s(Y))|~X=Y))),
% 0.27/1.10 inference(miniscoping,[status(thm)],[f45])).
% 0.27/1.10 fof(f47,plain,(
% 0.27/1.10 ![X0,X1]: (~mem(X0,s(X1))|X0=X1)),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f46])).
% 0.27/1.10 fof(f48,plain,(
% 0.27/1.10 ![X0,X1]: (mem(X0,s(X1))|~X0=X1)),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f46])).
% 0.27/1.10 fof(f49,plain,(
% 0.27/1.10 ![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))))),
% 0.27/1.10 inference(NNF_transformation,[status(thm)],[f6])).
% 0.27/1.10 fof(f50,plain,(
% 0.27/1.10 (![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))))),
% 0.27/1.10 inference(miniscoping,[status(thm)],[f49])).
% 0.27/1.10 fof(f51,plain,(
% 0.27/1.10 ![X0,X1,X2]: (~mem(X0,u(X1,X2))|mem(X0,X1)|mem(X0,X2))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f50])).
% 0.27/1.10 fof(f52,plain,(
% 0.27/1.10 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X1))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f50])).
% 0.27/1.10 fof(f53,plain,(
% 0.27/1.10 ![X0,X1,X2]: (mem(X0,u(X1,X2))|~mem(X0,X2))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f50])).
% 0.27/1.10 fof(f59,plain,(
% 0.27/1.10 ![X0,X1]: (a(X0,X1)=u(X0,s(X1)))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f8])).
% 0.27/1.10 fof(f60,plain,(
% 0.27/1.10 ![X0]: (n(X0)=a(X0,X0))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f9])).
% 0.27/1.10 fof(f169,plain,(
% 0.27/1.10 subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))),
% 0.27/1.10 inference(cnf_transformation,[status(thm)],[f27])).
% 0.27/1.10 fof(f170,plain,(
% 0.27/1.10 ![X0]: (mem(X0,s(X0)))),
% 0.27/1.10 inference(destructive_equality_resolution,[status(thm)],[f48])).
% 0.27/1.10 fof(f180,plain,(
% 0.27/1.10 ![X0,X1,X2]: (mem(X0,a(X1,X2))|~mem(X0,X1))),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f59,f52])).
% 0.27/1.10 fof(f181,plain,(
% 0.27/1.10 ![X0,X1,X2]: (mem(X0,a(X1,X2))|~mem(X0,s(X2)))),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f59,f53])).
% 0.27/1.10 fof(f183,plain,(
% 0.27/1.10 ![X0,X1]: (mem(X0,a(X1,X0)))),
% 0.27/1.10 inference(resolution,[status(thm)],[f181,f170])).
% 0.27/1.10 fof(f184,plain,(
% 0.27/1.10 ![X0]: (mem(X0,n(X0)))),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f60,f183])).
% 0.27/1.10 fof(f187,plain,(
% 0.27/1.10 ![X0,X1,X2]: (~mem(X0,a(X1,X2))|mem(X0,X1)|mem(X0,s(X2)))),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f59,f51])).
% 0.27/1.10 fof(f190,plain,(
% 0.27/1.10 ![X0,X1]: (~mem(X0,n(X1))|mem(X0,X1)|mem(X0,s(X1)))),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f60,f187])).
% 0.27/1.10 fof(f193,plain,(
% 0.27/1.10 ![X0]: (~mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))|mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f32,f169])).
% 0.27/1.10 fof(f194,plain,(
% 0.27/1.10 ![X0]: (mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))|~mem(X0,u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f193,f53])).
% 0.27/1.10 fof(f203,plain,(
% 0.27/1.10 ![X0,X1,X2]: (subq(u(X0,X1),X2)|mem(sK0_skl(X2,u(X0,X1)),X0)|mem(sK0_skl(X2,u(X0,X1)),X1))),
% 0.27/1.10 inference(resolution,[status(thm)],[f33,f51])).
% 0.27/1.10 fof(f206,plain,(
% 0.27/1.10 ![X0]: (subq(e,X0))),
% 0.27/1.10 inference(resolution,[status(thm)],[f33,f44])).
% 0.27/1.10 fof(f207,plain,(
% 0.27/1.10 ![X0]: (subq(X0,X0)|subq(X0,X0))),
% 0.27/1.10 inference(resolution,[status(thm)],[f34,f33])).
% 0.27/1.10 fof(f210,plain,(
% 0.27/1.10 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X2))),
% 0.27/1.10 inference(resolution,[status(thm)],[f34,f53])).
% 0.27/1.10 fof(f211,plain,(
% 0.27/1.10 ![X0,X1,X2]: (subq(X0,u(X1,X2))|~mem(sK0_skl(u(X1,X2),X0),X1))),
% 0.27/1.10 inference(resolution,[status(thm)],[f34,f52])).
% 0.27/1.10 fof(f212,plain,(
% 0.27/1.10 ![X0]: (subq(X0,X0))),
% 0.27/1.10 inference(duplicate_literals_removal,[status(thm)],[f207])).
% 0.27/1.10 fof(f214,plain,(
% 0.27/1.10 ![X0]: (~mem(X0,u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))|mem(X0,a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))))|mem(X0,u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f194,f51])).
% 0.27/1.10 fof(f217,plain,(
% 0.27/1.10 ![X0]: (mem(X0,a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))))|mem(X0,u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))|~mem(X0,a(s(n(e)),n(n(e)))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f214,f52])).
% 0.27/1.10 fof(f219,plain,(
% 0.27/1.10 ![X0]: (mem(X0,u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))|~mem(X0,a(s(n(e)),n(n(e))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(a(n(e),n(n(e))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f217,f187])).
% 0.27/1.10 fof(f221,plain,(
% 0.27/1.10 ![X0]: (~mem(X0,a(s(n(e)),n(n(e))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(a(n(e),n(n(e)))))|mem(X0,s(n(n(e))))|mem(X0,a(s(n(s(n(e)))),n(n(n(e))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f219,f51])).
% 0.27/1.10 fof(f223,plain,(
% 0.27/1.10 ![X0]: (~mem(X0,a(s(n(e)),n(n(e))))|mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(a(n(e),n(n(e)))))|mem(X0,s(n(n(e))))|mem(X0,s(n(s(n(e)))))|mem(X0,s(n(n(n(e))))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f221,f187])).
% 0.27/1.10 fof(f226,plain,(
% 0.27/1.10 ![X0]: (mem(X0,s(u(n(e),n(s(n(e))))))|mem(X0,s(a(n(e),n(n(e)))))|mem(X0,s(n(n(e))))|mem(X0,s(n(s(n(e)))))|mem(X0,s(n(n(n(e)))))|~mem(X0,s(n(e))))),
% 0.27/1.10 inference(resolution,[status(thm)],[f223,f180])).
% 0.27/1.10 fof(f239,definition,(
% 0.27/1.10 sQ6_spl <=> (mem(n(n(e)),s(n(n(n(e))))))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f240,plain,(
% 0.27/1.10 mem(n(n(e)),s(n(n(n(e)))))|~sQ6_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f239])).
% 0.27/1.10 fof(f241,plain,(
% 0.27/1.10 ~mem(n(n(e)),s(n(n(n(e)))))|sQ6_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f239])).
% 0.27/1.10 fof(f250,plain,(
% 0.27/1.10 n(n(e))=n(n(n(e)))|~sQ6_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f240,f47])).
% 0.27/1.10 fof(f263,plain,(
% 0.27/1.10 mem(n(n(e)),n(n(e)))|~sQ6_spl),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f250,f184])).
% 0.27/1.10 fof(f274,plain,(
% 0.27/1.10 mem(n(n(e)),n(e))|mem(n(n(e)),s(n(e)))|~sQ6_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f263,f190])).
% 0.27/1.10 fof(f275,definition,(
% 0.27/1.10 sQ8_spl <=> (mem(n(n(e)),n(e)))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f276,plain,(
% 0.27/1.10 mem(n(n(e)),n(e))|~sQ8_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f275])).
% 0.27/1.10 fof(f278,definition,(
% 0.27/1.10 sQ9_spl <=> (mem(n(n(e)),s(n(e))))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f279,plain,(
% 0.27/1.10 mem(n(n(e)),s(n(e)))|~sQ9_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f278])).
% 0.27/1.10 fof(f281,plain,(
% 0.27/1.10 sQ8_spl|sQ9_spl|~sQ6_spl),
% 0.27/1.10 inference(split_clause,[status(thm)],[f274,f275,f278,f239])).
% 0.27/1.10 fof(f282,plain,(
% 0.27/1.10 mem(n(n(e)),e)|mem(n(n(e)),s(e))|~sQ8_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f276,f190])).
% 0.27/1.10 fof(f283,definition,(
% 0.27/1.10 sQ10_spl <=> (mem(n(n(e)),e))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f284,plain,(
% 0.27/1.10 mem(n(n(e)),e)|~sQ10_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f283])).
% 0.27/1.10 fof(f286,definition,(
% 0.27/1.10 sQ11_spl <=> (mem(n(n(e)),s(e)))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f287,plain,(
% 0.27/1.10 mem(n(n(e)),s(e))|~sQ11_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f286])).
% 0.27/1.10 fof(f289,plain,(
% 0.27/1.10 sQ10_spl|sQ11_spl|~sQ8_spl),
% 0.27/1.10 inference(split_clause,[status(thm)],[f282,f283,f286,f275])).
% 0.27/1.10 fof(f290,plain,(
% 0.27/1.10 $false|~sQ10_spl),
% 0.27/1.10 inference(forward_subsumption_resolution,[status(thm)],[f284,f44])).
% 0.27/1.10 fof(f291,plain,(
% 0.27/1.10 ~sQ10_spl),
% 0.27/1.10 inference(contradiction_clause,[status(thm)],[f290])).
% 0.27/1.10 fof(f293,plain,(
% 0.27/1.10 n(n(e))=e|~sQ11_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f287,f47])).
% 0.27/1.10 fof(f296,plain,(
% 0.27/1.10 mem(n(e),e)|~sQ11_spl),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f293,f184])).
% 0.27/1.10 fof(f298,plain,(
% 0.27/1.10 $false|~sQ11_spl),
% 0.27/1.10 inference(forward_subsumption_resolution,[status(thm)],[f296,f44])).
% 0.27/1.10 fof(f299,plain,(
% 0.27/1.10 ~sQ11_spl),
% 0.27/1.10 inference(contradiction_clause,[status(thm)],[f298])).
% 0.27/1.10 fof(f301,plain,(
% 0.27/1.10 n(n(e))=n(e)|~sQ9_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f279,f47])).
% 0.27/1.10 fof(f304,plain,(
% 0.27/1.10 mem(n(e),n(e))|~sQ9_spl),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f301,f184])).
% 0.27/1.10 fof(f306,plain,(
% 0.27/1.10 mem(n(e),e)|mem(n(e),s(e))|~sQ9_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f304,f190])).
% 0.27/1.10 fof(f307,definition,(
% 0.27/1.10 sQ12_spl <=> (mem(n(e),e))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f308,plain,(
% 0.27/1.10 mem(n(e),e)|~sQ12_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f307])).
% 0.27/1.10 fof(f310,definition,(
% 0.27/1.10 sQ13_spl <=> (mem(n(e),s(e)))),
% 0.27/1.10 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.27/1.10 fof(f311,plain,(
% 0.27/1.10 mem(n(e),s(e))|~sQ13_spl),
% 0.27/1.10 inference(component_clause,[status(thm)],[f310])).
% 0.27/1.10 fof(f313,plain,(
% 0.27/1.10 sQ12_spl|sQ13_spl|~sQ9_spl),
% 0.27/1.10 inference(split_clause,[status(thm)],[f306,f307,f310,f278])).
% 0.27/1.10 fof(f314,plain,(
% 0.27/1.10 $false|~sQ12_spl),
% 0.27/1.10 inference(forward_subsumption_resolution,[status(thm)],[f308,f44])).
% 0.27/1.10 fof(f315,plain,(
% 0.27/1.10 ~sQ12_spl),
% 0.27/1.10 inference(contradiction_clause,[status(thm)],[f314])).
% 0.27/1.10 fof(f317,plain,(
% 0.27/1.10 n(e)=e|~sQ13_spl),
% 0.27/1.10 inference(resolution,[status(thm)],[f311,f47])).
% 0.27/1.10 fof(f322,plain,(
% 0.27/1.10 mem(e,e)|~sQ13_spl),
% 0.27/1.10 inference(paramodulation,[status(thm)],[f317,f184])).
% 0.27/1.10 fof(f326,plain,(
% 0.27/1.10 $false|~sQ13_spl),
% 0.27/1.10 inference(forward_subsumption_resolution,[status(thm)],[f322,f44])).
% 0.27/1.10 fof(f327,plain,(
% 0.27/1.10 ~sQ13_spl),
% 0.27/1.10 inference(contradiction_clause,[status(thm)],[f326])).
% 0.27/1.10 fof(f333,plain,(
% 0.27/1.10 ![X0]: (subq(u(X0,X0),X0)|subq(u(X0,X0),X0))),
% 0.27/1.10 inference(resolution,[status(thm)],[f203,f34])).
% 0.27/1.10 fof(f360,plain,(
% 0.27/1.10 ![X0]: (subq(u(X0,X0),X0))),
% 0.27/1.10 inference(duplicate_literals_removal,[status(thm)],[f333])).
% 0.27/1.10 fof(f391,definition,(
% 0.27/1.11 sQ14_spl <=> (mem(s(n(e)),n(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f392,plain,(
% 0.27/1.11 mem(s(n(e)),n(e))|~sQ14_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f391])).
% 0.27/1.11 fof(f398,plain,(
% 0.27/1.11 mem(s(n(e)),e)|mem(s(n(e)),s(e))|~sQ14_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f392,f190])).
% 0.27/1.11 fof(f399,definition,(
% 0.27/1.11 sQ16_spl <=> (mem(s(n(e)),e))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f400,plain,(
% 0.27/1.11 mem(s(n(e)),e)|~sQ16_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f399])).
% 0.27/1.11 fof(f402,definition,(
% 0.27/1.11 sQ17_spl <=> (mem(s(n(e)),s(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f403,plain,(
% 0.27/1.11 mem(s(n(e)),s(e))|~sQ17_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f402])).
% 0.27/1.11 fof(f405,plain,(
% 0.27/1.11 sQ16_spl|sQ17_spl|~sQ14_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f398,f399,f402,f391])).
% 0.27/1.11 fof(f406,plain,(
% 0.27/1.11 $false|~sQ16_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f400,f44])).
% 0.27/1.11 fof(f407,plain,(
% 0.27/1.11 ~sQ16_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f406])).
% 0.27/1.11 fof(f409,plain,(
% 0.27/1.11 s(n(e))=e|~sQ17_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f403,f47])).
% 0.27/1.11 fof(f414,plain,(
% 0.27/1.11 mem(n(e),e)|~sQ17_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f409,f170])).
% 0.27/1.11 fof(f415,plain,(
% 0.27/1.11 sQ12_spl|~sQ17_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f414,f307,f402])).
% 0.27/1.11 fof(f444,plain,(
% 0.27/1.11 ![X0,X1]: (~mem(X0,u(X1,X1))|mem(X0,X1))),
% 0.27/1.11 inference(resolution,[status(thm)],[f360,f32])).
% 0.27/1.11 fof(f445,plain,(
% 0.27/1.11 ![X0]: (~subq(X0,u(X0,X0))|X0=u(X0,X0))),
% 0.27/1.11 inference(resolution,[status(thm)],[f360,f36])).
% 0.27/1.11 fof(f453,definition,(
% 0.27/1.11 sQ18_spl <=> (subq(e,e))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f455,plain,(
% 0.27/1.11 ~subq(e,e)|sQ18_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f453])).
% 0.27/1.11 fof(f461,plain,(
% 0.27/1.11 $false|sQ18_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f455,f206])).
% 0.27/1.11 fof(f462,plain,(
% 0.27/1.11 sQ18_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f461])).
% 0.27/1.11 fof(f506,plain,(
% 0.27/1.11 ![X0,X1]: (mem(sK0_skl(X0,u(u(X1,X1),u(X1,X1))),X1)|subq(u(u(X1,X1),u(X1,X1)),X0))),
% 0.27/1.11 inference(resolution,[status(thm)],[f444,f203])).
% 0.27/1.11 fof(f606,plain,(
% 0.27/1.11 ![X0,X1]: (subq(X0,u(X1,X0))|subq(X0,u(X1,X0)))),
% 0.27/1.11 inference(resolution,[status(thm)],[f210,f33])).
% 0.27/1.11 fof(f609,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (subq(X0,u(X1,u(X2,X3)))|~mem(sK0_skl(u(X1,u(X2,X3)),X0),X3))),
% 0.27/1.11 inference(resolution,[status(thm)],[f210,f53])).
% 0.27/1.11 fof(f618,plain,(
% 0.27/1.11 ![X0,X1]: (subq(X0,u(X1,X0)))),
% 0.27/1.11 inference(duplicate_literals_removal,[status(thm)],[f606])).
% 0.27/1.11 fof(f769,plain,(
% 0.27/1.11 ![X0,X1,X2]: (subq(u(u(X0,X0),u(X0,X0)),u(X1,u(X2,X0)))|subq(u(u(X0,X0),u(X0,X0)),u(X1,u(X2,X0))))),
% 0.27/1.11 inference(resolution,[status(thm)],[f609,f506])).
% 0.27/1.11 fof(f783,plain,(
% 0.27/1.11 ![X0,X1,X2]: (subq(u(u(X0,X0),u(X0,X0)),u(X1,u(X2,X0))))),
% 0.27/1.11 inference(duplicate_literals_removal,[status(thm)],[f769])).
% 0.27/1.11 fof(f791,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (~mem(X0,u(u(X1,X1),u(X1,X1)))|mem(X0,u(X2,u(X3,X1))))),
% 0.27/1.11 inference(resolution,[status(thm)],[f783,f32])).
% 0.27/1.11 fof(f892,plain,(
% 0.27/1.11 mem(n(e),s(u(n(e),n(s(n(e))))))|mem(n(e),s(a(n(e),n(n(e)))))|mem(n(e),s(n(n(e))))|mem(n(e),s(n(s(n(e)))))|mem(n(e),s(n(n(n(e)))))),
% 0.27/1.11 inference(resolution,[status(thm)],[f226,f170])).
% 0.27/1.11 fof(f924,definition,(
% 0.27/1.11 sQ20_spl <=> (mem(n(e),s(u(n(e),n(s(n(e)))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f925,plain,(
% 0.27/1.11 mem(n(e),s(u(n(e),n(s(n(e))))))|~sQ20_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f924])).
% 0.27/1.11 fof(f927,definition,(
% 0.27/1.11 sQ21_spl <=> (mem(n(e),s(a(n(e),n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f928,plain,(
% 0.27/1.11 mem(n(e),s(a(n(e),n(n(e)))))|~sQ21_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f927])).
% 0.27/1.11 fof(f930,definition,(
% 0.27/1.11 sQ22_spl <=> (mem(n(e),s(n(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f931,plain,(
% 0.27/1.11 mem(n(e),s(n(n(e))))|~sQ22_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f930])).
% 0.27/1.11 fof(f933,definition,(
% 0.27/1.11 sQ23_spl <=> (mem(n(e),s(n(s(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f934,plain,(
% 0.27/1.11 mem(n(e),s(n(s(n(e)))))|~sQ23_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f933])).
% 0.27/1.11 fof(f936,definition,(
% 0.27/1.11 sQ24_spl <=> (mem(n(e),s(n(n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f937,plain,(
% 0.27/1.11 mem(n(e),s(n(n(n(e)))))|~sQ24_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f936])).
% 0.27/1.11 fof(f939,plain,(
% 0.27/1.11 sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl|sQ24_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f892,f924,f927,f930,f933,f936])).
% 0.27/1.11 fof(f941,plain,(
% 0.27/1.11 n(e)=n(n(e))|~sQ22_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f931,f47])).
% 0.27/1.11 fof(f945,plain,(
% 0.27/1.11 ~mem(n(n(e)),s(n(n(e))))|~sQ22_spl|sQ6_spl),
% 0.27/1.11 inference(backward_demodulation,[status(thm)],[f941,f241])).
% 0.27/1.11 fof(f957,plain,(
% 0.27/1.11 ~mem(n(e),s(n(n(e))))|~sQ22_spl|sQ6_spl),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f941,f945])).
% 0.27/1.11 fof(f958,plain,(
% 0.27/1.11 ~mem(n(e),s(n(e)))|~sQ22_spl|sQ6_spl),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f941,f957])).
% 0.27/1.11 fof(f959,plain,(
% 0.27/1.11 $false|~sQ22_spl|sQ6_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f958,f170])).
% 0.27/1.11 fof(f960,plain,(
% 0.27/1.11 ~sQ22_spl|sQ6_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f959])).
% 0.27/1.11 fof(f965,plain,(
% 0.27/1.11 n(e)=n(n(n(e)))|~sQ24_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f937,f47])).
% 0.27/1.11 fof(f971,plain,(
% 0.27/1.11 mem(n(n(e)),n(e))|~sQ24_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f965,f184])).
% 0.27/1.11 fof(f974,plain,(
% 0.27/1.11 sQ8_spl|~sQ24_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f971,f275,f936])).
% 0.27/1.11 fof(f976,plain,(
% 0.27/1.11 n(e)=n(s(n(e)))|~sQ23_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f934,f47])).
% 0.27/1.11 fof(f981,plain,(
% 0.27/1.11 mem(s(n(e)),n(e))|~sQ23_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f976,f184])).
% 0.27/1.11 fof(f987,plain,(
% 0.27/1.11 sQ14_spl|~sQ23_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f981,f391,f933])).
% 0.27/1.11 fof(f999,plain,(
% 0.27/1.11 n(e)=a(n(e),n(n(e)))|~sQ21_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f928,f47])).
% 0.27/1.11 fof(f1006,plain,(
% 0.27/1.11 mem(n(n(e)),n(e))|~sQ21_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f999,f183])).
% 0.27/1.11 fof(f1009,plain,(
% 0.27/1.11 sQ8_spl|~sQ21_spl),
% 0.27/1.11 inference(split_clause,[status(thm)],[f1006,f275,f927])).
% 0.27/1.11 fof(f1018,plain,(
% 0.27/1.11 n(e)=u(n(e),n(s(n(e))))|~sQ20_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f925,f47])).
% 0.27/1.11 fof(f1057,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (~mem(X0,u(a(s(X1),X1),u(s(X1),s(X1))))|mem(X0,u(X2,u(X3,s(X1)))))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f59,f791])).
% 0.27/1.11 fof(f1062,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (~mem(X0,u(a(s(X1),X1),a(s(X1),X1)))|mem(X0,u(X2,u(X3,s(X1)))))),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f59,f1057])).
% 0.27/1.11 fof(f1063,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (~mem(X0,u(a(s(X1),X1),a(s(X1),X1)))|mem(X0,u(X2,a(X3,X1))))),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f59,f1062])).
% 0.27/1.11 fof(f1079,plain,(
% 0.27/1.11 ![X0,X1]: (subq(u(u(X0,X0),u(X0,X0)),u(X0,X1))|subq(u(u(X0,X0),u(X0,X0)),u(X0,X1)))),
% 0.27/1.11 inference(resolution,[status(thm)],[f211,f506])).
% 0.27/1.11 fof(f1090,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (subq(X0,u(a(X1,X2),X3))|~mem(sK0_skl(u(a(X1,X2),X3),X0),X1))),
% 0.27/1.11 inference(resolution,[status(thm)],[f211,f180])).
% 0.27/1.11 fof(f1099,plain,(
% 0.27/1.11 ![X0,X1]: (subq(u(u(X0,X0),u(X0,X0)),u(X0,X1)))),
% 0.27/1.11 inference(duplicate_literals_removal,[status(thm)],[f1079])).
% 0.27/1.11 fof(f1116,plain,(
% 0.27/1.11 ![X0,X1]: (subq(u(u(X0,X0),u(X0,X0)),a(X0,X1)))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f59,f1099])).
% 0.27/1.11 fof(f1132,plain,(
% 0.27/1.11 ![X0]: (subq(u(u(X0,X0),u(X0,X0)),n(X0)))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f60,f1116])).
% 0.27/1.11 fof(f1213,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (subq(X0,u(a(X1,X2),s(X3)))|~mem(sK0_skl(a(a(X1,X2),X3),X0),X1))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f59,f1090])).
% 0.27/1.11 fof(f1221,plain,(
% 0.27/1.11 ![X0,X1,X2,X3]: (subq(X0,a(a(X1,X2),X3))|~mem(sK0_skl(a(a(X1,X2),X3),X0),X1))),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f59,f1213])).
% 0.27/1.11 fof(f1763,plain,(
% 0.27/1.11 ![X0,X1,X2]: (subq(X0,a(a(X1,X2),a(X1,X2)))|~mem(sK0_skl(n(a(X1,X2)),X0),X1))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f60,f1221])).
% 0.27/1.11 fof(f1771,plain,(
% 0.27/1.11 ![X0,X1,X2]: (subq(X0,n(a(X1,X2)))|~mem(sK0_skl(n(a(X1,X2)),X0),X1))),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f60,f1763])).
% 0.27/1.11 fof(f1778,plain,(
% 0.27/1.11 ![X0,X1]: (subq(X0,n(a(X0,X1)))|subq(X0,n(a(X0,X1))))),
% 0.27/1.11 inference(resolution,[status(thm)],[f1771,f33])).
% 0.27/1.11 fof(f1799,plain,(
% 0.27/1.11 ![X0,X1]: (subq(X0,n(a(X0,X1))))),
% 0.27/1.11 inference(duplicate_literals_removal,[status(thm)],[f1778])).
% 0.27/1.11 fof(f1807,plain,(
% 0.27/1.11 ![X0]: (subq(X0,n(n(X0))))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f60,f1799])).
% 0.27/1.11 fof(f2705,plain,(
% 0.27/1.11 ![X0]: (X0=u(X0,X0))),
% 0.27/1.11 inference(backward_subsumption_resolution,[status(thm)],[f445,f618])).
% 0.27/1.11 fof(f2710,plain,(
% 0.27/1.11 ![X0,X1]: (subq(s(X0),a(X1,X0)))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f59,f618])).
% 0.27/1.11 fof(f2735,plain,(
% 0.27/1.11 ![X0]: (subq(u(X0,X0),n(X0)))),
% 0.27/1.11 inference(backward_demodulation,[status(thm)],[f2705,f1132])).
% 0.27/1.11 fof(f2761,plain,(
% 0.27/1.11 ![X0]: (s(X0)=a(s(X0),X0))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f59,f2705])).
% 0.27/1.11 fof(f2815,plain,(
% 0.27/1.11 ![X0]: (subq(X0,n(X0)))),
% 0.27/1.11 inference(forward_demodulation,[status(thm)],[f2705,f2735])).
% 0.27/1.11 fof(f2870,plain,(
% 0.27/1.11 ![X0]: (subq(s(X0),n(X0)))),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f60,f2710])).
% 0.27/1.11 fof(f3204,definition,(
% 0.27/1.11 sQ72_spl <=> (subq(s(n(s(n(e)))),n(n(s(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3206,plain,(
% 0.27/1.11 ~subq(s(n(s(n(e)))),n(n(s(n(e)))))|sQ72_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3204])).
% 0.27/1.11 fof(f3218,plain,(
% 0.27/1.11 $false|sQ72_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3206,f2870])).
% 0.27/1.11 fof(f3219,plain,(
% 0.27/1.11 sQ72_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3218])).
% 0.27/1.11 fof(f3326,definition,(
% 0.27/1.11 sQ90_spl <=> (subq(n(s(n(e))),n(s(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3328,plain,(
% 0.27/1.11 ~subq(n(s(n(e))),n(s(n(e))))|sQ90_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3326])).
% 0.27/1.11 fof(f3355,definition,(
% 0.27/1.11 sQ92_spl <=> (subq(s(n(e)),n(s(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3357,plain,(
% 0.27/1.11 ~subq(s(n(e)),n(s(n(e))))|sQ92_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3355])).
% 0.27/1.11 fof(f3360,plain,(
% 0.27/1.11 $false|sQ92_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3357,f2815])).
% 0.27/1.11 fof(f3361,plain,(
% 0.27/1.11 sQ92_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3360])).
% 0.27/1.11 fof(f3484,plain,(
% 0.27/1.11 $false|sQ90_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3328,f212])).
% 0.27/1.11 fof(f3485,plain,(
% 0.27/1.11 sQ90_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3484])).
% 0.27/1.11 fof(f3495,definition,(
% 0.27/1.11 sQ99_spl <=> (subq(n(e),n(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3497,plain,(
% 0.27/1.11 ~subq(n(e),n(e))|sQ99_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3495])).
% 0.27/1.11 fof(f3503,plain,(
% 0.27/1.11 $false|sQ99_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3497,f212])).
% 0.27/1.11 fof(f3504,plain,(
% 0.27/1.11 sQ99_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3503])).
% 0.27/1.11 fof(f3844,definition,(
% 0.27/1.11 sQ114_spl <=> (subq(s(n(n(n(n(e))))),n(n(n(n(n(e)))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3846,plain,(
% 0.27/1.11 ~subq(s(n(n(n(n(e))))),n(n(n(n(n(e))))))|sQ114_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3844])).
% 0.27/1.11 fof(f3858,plain,(
% 0.27/1.11 $false|sQ114_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3846,f2870])).
% 0.27/1.11 fof(f3859,plain,(
% 0.27/1.11 sQ114_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3858])).
% 0.27/1.11 fof(f3887,definition,(
% 0.27/1.11 sQ120_spl <=> (subq(s(n(n(s(n(e))))),n(n(n(s(n(e)))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f3889,plain,(
% 0.27/1.11 ~subq(s(n(n(s(n(e))))),n(n(n(s(n(e))))))|sQ120_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f3887])).
% 0.27/1.11 fof(f3901,plain,(
% 0.27/1.11 $false|sQ120_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3889,f2870])).
% 0.27/1.11 fof(f3902,plain,(
% 0.27/1.11 sQ120_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f3901])).
% 0.27/1.11 fof(f4042,definition,(
% 0.27/1.11 sQ139_spl <=> (mem(n(n(n(n(n(e))))),e))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4043,plain,(
% 0.27/1.11 mem(n(n(n(n(n(e))))),e)|~sQ139_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4042])).
% 0.27/1.11 fof(f4045,definition,(
% 0.27/1.11 sQ140_spl <=> (mem(n(n(n(n(n(e))))),s(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4046,plain,(
% 0.27/1.11 mem(n(n(n(n(n(e))))),s(e))|~sQ140_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4045])).
% 0.27/1.11 fof(f4049,plain,(
% 0.27/1.11 $false|~sQ139_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4043,f44])).
% 0.27/1.11 fof(f4050,plain,(
% 0.27/1.11 ~sQ139_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4049])).
% 0.27/1.11 fof(f4053,plain,(
% 0.27/1.11 n(n(n(n(n(e)))))=e|~sQ140_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f4046,f47])).
% 0.27/1.11 fof(f4070,plain,(
% 0.27/1.11 mem(n(n(n(n(e)))),e)|~sQ140_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f4053,f184])).
% 0.27/1.11 fof(f4076,definition,(
% 0.27/1.11 sQ141_spl <=> (subq(e,s(n(n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4078,plain,(
% 0.27/1.11 ~subq(e,s(n(n(n(e)))))|sQ141_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4076])).
% 0.27/1.11 fof(f4081,definition,(
% 0.27/1.11 sQ142_spl <=> (subq(e,s(n(n(n(n(e)))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4083,plain,(
% 0.27/1.11 ~subq(e,s(n(n(n(n(e))))))|sQ142_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4081])).
% 0.27/1.11 fof(f4088,definition,(
% 0.27/1.11 sQ144_spl <=> (subq(e,n(n(n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4090,plain,(
% 0.27/1.11 ~subq(e,n(n(n(n(e)))))|sQ144_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4088])).
% 0.27/1.11 fof(f4099,plain,(
% 0.27/1.11 $false|~sQ140_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4070,f44])).
% 0.27/1.11 fof(f4100,plain,(
% 0.27/1.11 ~sQ140_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4099])).
% 0.27/1.11 fof(f4101,plain,(
% 0.27/1.11 $false|sQ144_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4090,f206])).
% 0.27/1.11 fof(f4102,plain,(
% 0.27/1.11 sQ144_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4101])).
% 0.27/1.11 fof(f4103,plain,(
% 0.27/1.11 $false|sQ142_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4083,f206])).
% 0.27/1.11 fof(f4104,plain,(
% 0.27/1.11 sQ142_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4103])).
% 0.27/1.11 fof(f4105,plain,(
% 0.27/1.11 $false|sQ141_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4078,f206])).
% 0.27/1.11 fof(f4106,plain,(
% 0.27/1.11 sQ141_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4105])).
% 0.27/1.11 fof(f4161,definition,(
% 0.27/1.11 sQ150_spl <=> (subq(n(e),n(n(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4163,plain,(
% 0.27/1.11 ~subq(n(e),n(n(n(e))))|sQ150_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4161])).
% 0.27/1.11 fof(f4168,plain,(
% 0.27/1.11 $false|sQ150_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4163,f1807])).
% 0.27/1.11 fof(f4169,plain,(
% 0.27/1.11 sQ150_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4168])).
% 0.27/1.11 fof(f4200,definition,(
% 0.27/1.11 sQ154_spl <=> (subq(n(e),n(n(e))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4202,plain,(
% 0.27/1.11 ~subq(n(e),n(n(e)))|sQ154_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4200])).
% 0.27/1.11 fof(f4212,plain,(
% 0.27/1.11 $false|sQ154_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4202,f2815])).
% 0.27/1.11 fof(f4213,plain,(
% 0.27/1.11 sQ154_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4212])).
% 0.27/1.11 fof(f4232,definition,(
% 0.27/1.11 sQ157_spl <=> (subq(n(n(e)),n(n(e))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4234,plain,(
% 0.27/1.11 ~subq(n(n(e)),n(n(e)))|sQ157_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4232])).
% 0.27/1.11 fof(f4337,definition,(
% 0.27/1.11 sQ163_spl <=> (subq(n(n(e)),n(n(n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4339,plain,(
% 0.27/1.11 ~subq(n(n(e)),n(n(n(n(e)))))|sQ163_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4337])).
% 0.27/1.11 fof(f4345,plain,(
% 0.27/1.11 $false|sQ163_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4339,f1807])).
% 0.27/1.11 fof(f4346,plain,(
% 0.27/1.11 sQ163_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4345])).
% 0.27/1.11 fof(f4361,definition,(
% 0.27/1.11 sQ165_spl <=> (subq(n(n(e)),n(n(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4363,plain,(
% 0.27/1.11 ~subq(n(n(e)),n(n(n(e))))|sQ165_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4361])).
% 0.27/1.11 fof(f4365,plain,(
% 0.27/1.11 $false|sQ165_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4363,f2815])).
% 0.27/1.11 fof(f4366,plain,(
% 0.27/1.11 sQ165_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4365])).
% 0.27/1.11 fof(f4410,plain,(
% 0.27/1.11 $false|sQ157_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4234,f212])).
% 0.27/1.11 fof(f4411,plain,(
% 0.27/1.11 sQ157_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4410])).
% 0.27/1.11 fof(f4470,definition,(
% 0.27/1.11 sQ170_spl <=> (subq(n(n(n(e))),n(n(n(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4472,plain,(
% 0.27/1.11 ~subq(n(n(n(e))),n(n(n(n(e)))))|sQ170_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4470])).
% 0.27/1.11 fof(f4475,plain,(
% 0.27/1.11 $false|sQ170_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4472,f2815])).
% 0.27/1.11 fof(f4476,plain,(
% 0.27/1.11 sQ170_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4475])).
% 0.27/1.11 fof(f4546,definition,(
% 0.27/1.11 sQ174_spl <=> (subq(n(n(n(e))),n(n(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4548,plain,(
% 0.27/1.11 ~subq(n(n(n(e))),n(n(n(e))))|sQ174_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4546])).
% 0.27/1.11 fof(f4558,plain,(
% 0.27/1.11 $false|sQ174_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4548,f212])).
% 0.27/1.11 fof(f4559,plain,(
% 0.27/1.11 sQ174_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4558])).
% 0.27/1.11 fof(f4633,definition,(
% 0.27/1.11 sQ183_spl <=> (mem(n(n(n(e))),e))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4634,plain,(
% 0.27/1.11 mem(n(n(n(e))),e)|~sQ183_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4633])).
% 0.27/1.11 fof(f4640,plain,(
% 0.27/1.11 $false|~sQ183_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4634,f44])).
% 0.27/1.11 fof(f4641,plain,(
% 0.27/1.11 ~sQ183_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4640])).
% 0.27/1.11 fof(f4667,definition,(
% 0.27/1.11 sQ185_spl <=> (subq(e,s(n(e))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4669,plain,(
% 0.27/1.11 ~subq(e,s(n(e)))|sQ185_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4667])).
% 0.27/1.11 fof(f4673,plain,(
% 0.27/1.11 $false|sQ185_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4669,f206])).
% 0.27/1.11 fof(f4674,plain,(
% 0.27/1.11 sQ185_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4673])).
% 0.27/1.11 fof(f4730,definition,(
% 0.27/1.11 sQ187_spl <=> (subq(s(n(n(e))),n(n(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4732,plain,(
% 0.27/1.11 ~subq(s(n(n(e))),n(n(n(e))))|sQ187_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4730])).
% 0.27/1.11 fof(f4735,plain,(
% 0.27/1.11 $false|sQ187_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4732,f2870])).
% 0.27/1.11 fof(f4736,plain,(
% 0.27/1.11 sQ187_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4735])).
% 0.27/1.11 fof(f4928,definition,(
% 0.27/1.11 sQ193_spl <=> (subq(s(e),n(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f4930,plain,(
% 0.27/1.11 ~subq(s(e),n(e))|sQ193_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f4928])).
% 0.27/1.11 fof(f4966,plain,(
% 0.27/1.11 $false|sQ193_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f4930,f2870])).
% 0.27/1.11 fof(f4967,plain,(
% 0.27/1.11 sQ193_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f4966])).
% 0.27/1.11 fof(f5310,definition,(
% 0.27/1.11 sQ207_spl <=> (subq(s(n(e)),n(n(s(n(e))))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f5312,plain,(
% 0.27/1.11 ~subq(s(n(e)),n(n(s(n(e)))))|sQ207_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f5310])).
% 0.27/1.11 fof(f5319,plain,(
% 0.27/1.11 $false|sQ207_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f5312,f1807])).
% 0.27/1.11 fof(f5320,plain,(
% 0.27/1.11 sQ207_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f5319])).
% 0.27/1.11 fof(f5458,definition,(
% 0.27/1.11 sQ212_spl <=> (mem(n(n(s(n(e)))),e))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f5459,plain,(
% 0.27/1.11 mem(n(n(s(n(e)))),e)|~sQ212_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f5458])).
% 0.27/1.11 fof(f5461,definition,(
% 0.27/1.11 sQ213_spl <=> (mem(n(n(s(n(e)))),s(e)))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f5462,plain,(
% 0.27/1.11 mem(n(n(s(n(e)))),s(e))|~sQ213_spl),
% 0.27/1.11 inference(component_clause,[status(thm)],[f5461])).
% 0.27/1.11 fof(f5465,plain,(
% 0.27/1.11 $false|~sQ212_spl),
% 0.27/1.11 inference(forward_subsumption_resolution,[status(thm)],[f5459,f44])).
% 0.27/1.11 fof(f5466,plain,(
% 0.27/1.11 ~sQ212_spl),
% 0.27/1.11 inference(contradiction_clause,[status(thm)],[f5465])).
% 0.27/1.11 fof(f5520,plain,(
% 0.27/1.11 n(n(s(n(e))))=e|~sQ213_spl),
% 0.27/1.11 inference(resolution,[status(thm)],[f5462,f47])).
% 0.27/1.11 fof(f5545,plain,(
% 0.27/1.11 mem(n(s(n(e))),e)|~sQ213_spl),
% 0.27/1.11 inference(paramodulation,[status(thm)],[f5520,f184])).
% 0.27/1.11 fof(f5547,definition,(
% 0.27/1.11 sQ214_spl <=> (subq(e,s(s(n(e)))))),
% 0.27/1.11 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 0.27/1.11 fof(f5549,plain,(
% 0.27/1.12 ~subq(e,s(s(n(e))))|sQ214_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5547])).
% 0.27/1.12 fof(f5557,definition,(
% 0.27/1.12 sQ215_spl <=> (subq(e,s(n(s(n(e))))))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5559,plain,(
% 0.27/1.12 ~subq(e,s(n(s(n(e)))))|sQ215_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5557])).
% 0.27/1.12 fof(f5561,definition,(
% 0.27/1.12 sQ216_spl <=> (subq(e,n(s(n(e)))))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5563,plain,(
% 0.27/1.12 ~subq(e,n(s(n(e))))|sQ216_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5561])).
% 0.27/1.12 fof(f5566,plain,(
% 0.27/1.12 $false|~sQ213_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5545,f44])).
% 0.27/1.12 fof(f5567,plain,(
% 0.27/1.12 ~sQ213_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5566])).
% 0.27/1.12 fof(f5568,plain,(
% 0.27/1.12 $false|sQ216_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5563,f206])).
% 0.27/1.12 fof(f5569,plain,(
% 0.27/1.12 sQ216_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5568])).
% 0.27/1.12 fof(f5570,plain,(
% 0.27/1.12 $false|sQ215_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5559,f206])).
% 0.27/1.12 fof(f5571,plain,(
% 0.27/1.12 sQ215_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5570])).
% 0.27/1.12 fof(f5572,plain,(
% 0.27/1.12 $false|sQ214_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5549,f206])).
% 0.27/1.12 fof(f5573,plain,(
% 0.27/1.12 sQ214_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5572])).
% 0.27/1.12 fof(f5608,definition,(
% 0.27/1.12 sQ217_spl <=> (subq(n(s(n(e))),n(n(s(n(e))))))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5610,plain,(
% 0.27/1.12 ~subq(n(s(n(e))),n(n(s(n(e)))))|sQ217_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5608])).
% 0.27/1.12 fof(f5614,plain,(
% 0.27/1.12 $false|sQ217_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5610,f2815])).
% 0.27/1.12 fof(f5615,plain,(
% 0.27/1.12 sQ217_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5614])).
% 0.27/1.12 fof(f5663,definition,(
% 0.27/1.12 sQ224_spl <=> (mem(n(n(n(n(e)))),e))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5664,plain,(
% 0.27/1.12 mem(n(n(n(n(e)))),e)|~sQ224_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5663])).
% 0.27/1.12 fof(f5670,plain,(
% 0.27/1.12 $false|~sQ224_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5664,f44])).
% 0.27/1.12 fof(f5671,plain,(
% 0.27/1.12 ~sQ224_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5670])).
% 0.27/1.12 fof(f5700,definition,(
% 0.27/1.12 sQ226_spl <=> (subq(e,s(n(n(e)))))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5702,plain,(
% 0.27/1.12 ~subq(e,s(n(n(e))))|sQ226_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5700])).
% 0.27/1.12 fof(f5712,definition,(
% 0.27/1.12 sQ227_spl <=> (subq(e,n(n(n(e)))))),
% 0.27/1.12 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 0.27/1.12 fof(f5714,plain,(
% 0.27/1.12 ~subq(e,n(n(n(e))))|sQ227_spl),
% 0.27/1.12 inference(component_clause,[status(thm)],[f5712])).
% 0.27/1.12 fof(f5719,plain,(
% 0.27/1.12 $false|sQ227_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5714,f206])).
% 0.27/1.12 fof(f5720,plain,(
% 0.27/1.12 sQ227_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5719])).
% 0.27/1.12 fof(f5721,plain,(
% 0.27/1.12 $false|sQ226_spl),
% 0.27/1.12 inference(forward_subsumption_resolution,[status(thm)],[f5702,f206])).
% 0.27/1.12 fof(f5722,plain,(
% 0.27/1.12 sQ226_spl),
% 0.27/1.12 inference(contradiction_clause,[status(thm)],[f5721])).
% 0.27/1.12 fof(f6864,plain,(
% 0.27/1.12 ![X0,X1,X2,X3]: (~mem(X0,a(s(X1),X1))|mem(X0,u(X2,a(X3,X1))))),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f2705,f1063])).
% 0.27/1.12 fof(f6865,plain,(
% 0.27/1.12 ![X0,X1,X2,X3]: (~mem(X0,s(X1))|mem(X0,u(X2,a(X3,X1))))),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f2761,f6864])).
% 0.27/1.12 fof(f6881,plain,(
% 0.27/1.12 ![X0,X1,X2]: (mem(X0,u(X1,a(X2,X0))))),
% 0.27/1.12 inference(resolution,[status(thm)],[f6865,f170])).
% 0.27/1.12 fof(f6918,plain,(
% 0.27/1.12 ![X0,X1]: (mem(X0,u(X1,n(X0))))),
% 0.27/1.12 inference(paramodulation,[status(thm)],[f60,f6881])).
% 0.27/1.12 fof(f6921,plain,(
% 0.27/1.12 mem(s(n(e)),n(e))|~sQ20_spl),
% 0.27/1.12 inference(paramodulation,[status(thm)],[f1018,f6918])).
% 0.27/1.12 fof(f6923,plain,(
% 0.27/1.12 sQ14_spl|~sQ20_spl),
% 0.27/1.12 inference(split_clause,[status(thm)],[f6921,f391,f924])).
% 0.27/1.12 fof(f6924,plain,(
% 0.27/1.12 $false),
% 0.27/1.12 inference(sat_refutation,[status(thm)],[f281,f289,f291,f299,f313,f315,f327,f405,f407,f415,f462,f939,f960,f974,f987,f1009,f3219,f3361,f3485,f3504,f3859,f3902,f4050,f4100,f4102,f4104,f4106,f4169,f4213,f4346,f4366,f4411,f4476,f4559,f4641,f4674,f4736,f4967,f5320,f5466,f5567,f5569,f5571,f5573,f5615,f5671,f5720,f5722,f6923])).
% 0.27/1.12 % SZS output end CNFRefutation for theBenchmark.p
% 5.10/1.17 % Elapsed time: 0.715540 seconds
% 5.10/1.17 % CPU time: 4.993751 seconds
% 5.10/1.17 % Total memory used: 172.203 MB
% 5.10/1.17 % Net memory used: 168.662 MB
%------------------------------------------------------------------------------