%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP012+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 12:51:54 PM UTC 2026
% Result : Theorem 39.75s 5.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ITP012+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n001.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sun Sep 20 21:51:13 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 39.75/5.61 % Refutation found
% 39.75/5.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.75/5.61 % SZS output start CNFRefutation for theBenchmark
% 39.75/5.61 fof(f1,axiom,(
% 39.75/5.61 ne(bool) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f4,axiom,(
% 39.75/5.61 (! [A,B,F] :( mem(F,arr(A,B))=> (! [X] :( mem(X,A)=> mem(ap(F,X),B) ) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f12,axiom,(
% 39.75/5.61 (! [A] :( ne(A)=> (! [Q] :( mem(Q,arr(A,bool))=> ( p(ap(c_2Ebool_2E_3F(A),Q))<=> (? [X] :( mem(X,A)& p(ap(Q,X)) ) )) ) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f13,axiom,(
% 39.75/5.61 ne(ty_2Einteger_2Eint) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f16,axiom,(
% 39.75/5.61 mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f18,axiom,(
% 39.75/5.61 mem(c_2Ebool_2EF,bool) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f19,axiom,(
% 39.75/5.61 ~ p(c_2Ebool_2EF) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f26,axiom,(
% 39.75/5.61 mem(c_2Ebool_2E_7E,arr(bool,bool)) ),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f27,axiom,(
% 39.75/5.61 (! [Q] :( mem(Q,bool)=> ( p(ap(c_2Ebool_2E_7E,Q))<=> ~ p(Q) ) ) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f44,axiom,(
% 39.75/5.61 (! [V0x] :( mem(V0x,ty_2Einteger_2Eint)=> (! [V1y] :( mem(V1y,ty_2Einteger_2Eint)=> ap(ap(c_2Einteger_2Eint__sub,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(c_2Einteger_2Eint__neg,V1y)) ) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f45,axiom,(
% 39.75/5.61 (! [V0p] :( mem(V0p,ty_2Einteger_2Eint)=> (! [V1q] :( mem(V1q,ty_2Einteger_2Eint)=> (! [V2r] :( mem(V2r,ty_2Einteger_2Eint)=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__add,V2r),V1q)))<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)) ) ) ) )) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f46,axiom,(
% 39.75/5.61 (! [V0p] :( mem(V0p,ty_2Einteger_2Eint)=> (! [V1q] :( mem(V1q,ty_2Einteger_2Eint)=> ( ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(c_2Einteger_2Eint__neg,V1q)))<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)) )& ( p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,V0p)),V1q))<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)) ) ) ) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f52,axiom,(
% 39.75/5.61 (! [V0p] :( mem(V0p,bool)=> (! [V1q] :( mem(V1q,bool)=> (! [V2r] :( mem(V2r,bool)=> ( ( p(V0p)<=> ( p(V1q)<=> p(V2r) ) )<=> ( ( p(V0p)| p(V1q)| p(V2r) )& ( p(V0p)| ~ p(V2r)| ~ p(V1q) )& ( p(V1q)| ~ p(V2r)| ~ p(V0p) )& ( p(V2r)| ~ p(V1q)| ~ p(V0p) ) ) ) ) )) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f56,axiom,(
% 39.75/5.61 (! [V0p] :( mem(V0p,bool)=> (! [V1q] :( mem(V1q,bool)=> ( ( p(V0p)<=> ~ p(V1q) )<=> ( ( p(V0p)| p(V1q) )& ( ~ p(V1q)| ~ p(V0p) ) ) ) ) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f57,conjecture,(
% 39.75/5.61 (! [V0p] :( mem(V0p,ty_2Einteger_2Eint)=> (! [V1q] :( mem(V1q,ty_2Einteger_2Eint)=> (! [V2r] :( mem(V2r,ty_2Einteger_2Eint)=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)) ) ) ) )) )) )),
% 39.75/5.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.75/5.61 fof(f58,negated_conjecture,(
% 39.75/5.61 ~((! [V0p] :( mem(V0p,ty_2Einteger_2Eint)=> (! [V1q] :( mem(V1q,ty_2Einteger_2Eint)=> (! [V2r] :( mem(V2r,ty_2Einteger_2Eint)=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))=> ( p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))<=> p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)) ) ) ) )) )) ))),
% 39.75/5.61 inference(negated_conjecture,[status(cth)],[f57])).
% 39.75/5.61 fof(f59,plain,(
% 39.75/5.61 ne(bool)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f1])).
% 39.75/5.61 fof(f63,plain,(
% 39.75/5.61 ![A,B,F]: (~mem(F,arr(A,B))|(![X]: (~mem(X,A)|mem(ap(F,X),B))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 39.75/5.61 fof(f64,plain,(
% 39.75/5.61 ![X0,X1,X2,X3]: (~mem(X0,arr(X1,X2))|~mem(X3,X1)|mem(ap(X0,X3),X2))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f63])).
% 39.75/5.61 fof(f82,plain,(
% 39.75/5.61 ![A]: (~ne(A)|(![Q]: (~mem(Q,arr(A,bool))|(p(ap(c_2Ebool_2E_3F(A),Q))<=>(?[X]: (mem(X,A)&p(ap(Q,X))))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 39.75/5.61 fof(f83,plain,(
% 39.75/5.61 ![A]: (~ne(A)|(![Q]: (~mem(Q,arr(A,bool))|((~p(ap(c_2Ebool_2E_3F(A),Q))|(?[X]: (mem(X,A)&p(ap(Q,X)))))&(p(ap(c_2Ebool_2E_3F(A),Q))|(![X]: (~mem(X,A)|~p(ap(Q,X)))))))))),
% 39.75/5.61 inference(NNF_transformation,[status(thm)],[f82])).
% 39.75/5.61 fof(f84,plain,(
% 39.75/5.61 ![A]: (~ne(A)|(![Q]: (~mem(Q,arr(A,bool))|((~p(ap(c_2Ebool_2E_3F(A),Q))|(mem(sK1_skl(Q,A),A)&p(ap(Q,sK1_skl(Q,A)))))&(p(ap(c_2Ebool_2E_3F(A),Q))|(![X]: (~mem(X,A)|~p(ap(Q,X)))))))))),
% 39.75/5.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(Q,A))],[f83])).
% 39.75/5.61 fof(f87,plain,(
% 39.75/5.61 ![X0,X1,X2]: (~ne(X0)|~mem(X1,arr(X0,bool))|p(ap(c_2Ebool_2E_3F(X0),X1))|~mem(X2,X0)|~p(ap(X1,X2)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f84])).
% 39.75/5.61 fof(f88,plain,(
% 39.75/5.61 ne(ty_2Einteger_2Eint)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f13])).
% 39.75/5.61 fof(f91,plain,(
% 39.75/5.61 mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f16])).
% 39.75/5.61 fof(f93,plain,(
% 39.75/5.61 mem(c_2Ebool_2EF,bool)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f18])).
% 39.75/5.61 fof(f94,plain,(
% 39.75/5.61 ~p(c_2Ebool_2EF)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f19])).
% 39.75/5.61 fof(f113,plain,(
% 39.75/5.61 mem(c_2Ebool_2E_7E,arr(bool,bool))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f26])).
% 39.75/5.61 fof(f114,plain,(
% 39.75/5.61 ![Q]: (~mem(Q,bool)|(p(ap(c_2Ebool_2E_7E,Q))<=>~p(Q)))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 39.75/5.61 fof(f115,plain,(
% 39.75/5.61 ![Q]: (~mem(Q,bool)|((~p(ap(c_2Ebool_2E_7E,Q))|~p(Q))&(p(ap(c_2Ebool_2E_7E,Q))|p(Q))))),
% 39.75/5.61 inference(NNF_transformation,[status(thm)],[f114])).
% 39.75/5.61 fof(f117,plain,(
% 39.75/5.61 ![X0]: (~mem(X0,bool)|p(ap(c_2Ebool_2E_7E,X0))|p(X0))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f115])).
% 39.75/5.61 fof(f210,plain,(
% 39.75/5.61 ![V0x]: (~mem(V0x,ty_2Einteger_2Eint)|(![V1y]: (~mem(V1y,ty_2Einteger_2Eint)|ap(ap(c_2Einteger_2Eint__sub,V0x),V1y)=ap(ap(c_2Einteger_2Eint__add,V0x),ap(c_2Einteger_2Eint__neg,V1y)))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 39.75/5.61 fof(f211,plain,(
% 39.75/5.61 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|ap(ap(c_2Einteger_2Eint__sub,X0),X1)=ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,X1)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f210])).
% 39.75/5.61 fof(f212,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,ty_2Einteger_2Eint)|(![V1q]: (~mem(V1q,ty_2Einteger_2Eint)|(![V2r]: (~mem(V2r,ty_2Einteger_2Eint)|(~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))|(p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__add,V2r),V1q)))<=>p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)))))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 39.75/5.61 fof(f213,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,ty_2Einteger_2Eint)|(![V1q]: (~mem(V1q,ty_2Einteger_2Eint)|(![V2r]: (~mem(V2r,ty_2Einteger_2Eint)|(~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))|((~p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__add,V2r),V1q)))|p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)))&(p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__add,V2r),V1q)))|~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r))))))))))),
% 39.75/5.61 inference(NNF_transformation,[status(thm)],[f212])).
% 39.75/5.61 fof(f214,plain,(
% 39.75/5.61 ![X0,X1,X2]: (~mem(X0,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~mem(X2,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,X0),X1))|~p(ap(ap(c_2Einteger_2Eint__divides,X0),ap(ap(c_2Einteger_2Eint__add,X2),X1)))|p(ap(ap(c_2Einteger_2Eint__divides,X0),X2)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f213])).
% 39.75/5.61 fof(f215,plain,(
% 39.75/5.61 ![X0,X1,X2]: (~mem(X0,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~mem(X2,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,X0),X1))|p(ap(ap(c_2Einteger_2Eint__divides,X0),ap(ap(c_2Einteger_2Eint__add,X2),X1)))|~p(ap(ap(c_2Einteger_2Eint__divides,X0),X2)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f213])).
% 39.75/5.61 fof(f216,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,ty_2Einteger_2Eint)|(![V1q]: (~mem(V1q,ty_2Einteger_2Eint)|((p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(c_2Einteger_2Eint__neg,V1q)))<=>p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)))&(p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,V0p)),V1q))<=>p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 39.75/5.61 fof(f217,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,ty_2Einteger_2Eint)|(![V1q]: (~mem(V1q,ty_2Einteger_2Eint)|(((~p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(c_2Einteger_2Eint__neg,V1q)))|p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)))&(p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(c_2Einteger_2Eint__neg,V1q)))|~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))))&((~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,V0p)),V1q))|p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q)))&(p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,V0p)),V1q))|~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))))))))),
% 39.75/5.61 inference(NNF_transformation,[status(thm)],[f216])).
% 39.75/5.61 fof(f219,plain,(
% 39.75/5.61 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,X0),ap(c_2Einteger_2Eint__neg,X1)))|~p(ap(ap(c_2Einteger_2Eint__divides,X0),X1)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f217])).
% 39.75/5.61 fof(f221,plain,(
% 39.75/5.61 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,X0)),X1))|~p(ap(ap(c_2Einteger_2Eint__divides,X0),X1)))),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f217])).
% 39.75/5.61 fof(f249,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,bool)|(![V1q]: (~mem(V1q,bool)|(![V2r]: (~mem(V2r,bool)|((p(V0p)<=>(p(V1q)<=>p(V2r)))<=>(((((p(V0p)|p(V1q))|p(V2r))&((p(V0p)|~p(V2r))|~p(V1q)))&((p(V1q)|~p(V2r))|~p(V0p)))&((p(V2r)|~p(V1q))|~p(V0p)))))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 39.75/5.61 fof(f250,definition,(
% 39.75/5.61 ![V0p,V1q,V2r]: (sP7_prd(V2r,V1q,V0p)<=>(p(V0p)<=>(p(V1q)<=>p(V2r))))),
% 39.75/5.61 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 39.75/5.61 fof(f292,plain,(
% 39.75/5.61 ![V0p]: (~mem(V0p,bool)|(![V1q]: (~mem(V1q,bool)|((p(V0p)<=>~p(V1q))<=>((p(V0p)|p(V1q))&(~p(V1q)|~p(V0p)))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 39.75/5.61 fof(f293,definition,(
% 39.75/5.61 ![V0p,V1q]: (sP15_prd(V1q,V0p)<=>(p(V0p)<=>~p(V1q)))),
% 39.75/5.61 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 39.75/5.61 fof(f302,plain,(
% 39.75/5.61 (?[V0p]: (mem(V0p,ty_2Einteger_2Eint)&(?[V1q]: (mem(V1q,ty_2Einteger_2Eint)&(?[V2r]: (mem(V2r,ty_2Einteger_2Eint)&(p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))&(p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))<~>p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r))))))))))),
% 39.75/5.61 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 39.75/5.61 fof(f303,plain,(
% 39.75/5.61 ?[V0p]: (mem(V0p,ty_2Einteger_2Eint)&(?[V1q]: (mem(V1q,ty_2Einteger_2Eint)&(?[V2r]: (mem(V2r,ty_2Einteger_2Eint)&(p(ap(ap(c_2Einteger_2Eint__divides,V0p),V1q))&((p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))|p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r)))&(~p(ap(ap(c_2Einteger_2Eint__divides,V0p),ap(ap(c_2Einteger_2Eint__sub,V2r),V1q)))|~p(ap(ap(c_2Einteger_2Eint__divides,V0p),V2r))))))))))),
% 39.75/5.61 inference(NNF_transformation,[status(thm)],[f302])).
% 39.75/5.61 fof(f304,plain,(
% 39.75/5.61 (mem(sK6_skl,ty_2Einteger_2Eint)&(mem(sK7_skl,ty_2Einteger_2Eint)&(mem(sK8_skl,ty_2Einteger_2Eint)&(p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK7_skl))&((p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl)))&(~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl))))))))),
% 39.75/5.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl]),skolemize(V0p,sK6_skl),skolemize(V1q,sK7_skl),skolemize(V2r,sK8_skl)],[f303])).
% 39.75/5.61 fof(f305,plain,(
% 39.75/5.61 mem(sK6_skl,ty_2Einteger_2Eint)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.61 fof(f306,plain,(
% 39.75/5.61 mem(sK7_skl,ty_2Einteger_2Eint)),
% 39.75/5.61 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.61 fof(f307,plain,(
% 39.75/5.61 mem(sK8_skl,ty_2Einteger_2Eint)),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.63 fof(f308,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK7_skl))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.63 fof(f309,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.63 fof(f310,plain,(
% 39.75/5.63 ~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f304])).
% 39.75/5.63 fof(f351,definition,(
% 39.75/5.63 ![V1q,V2r]: (sP16_prd(V2r,V1q)<=>(p(V1q)<=>p(V2r)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 39.75/5.63 fof(f352,plain,(
% 39.75/5.63 ![V0p,V1q,V2r]: (sP7_prd(V2r,V1q,V0p)<=>(p(V0p)<=>sP16_prd(V2r,V1q)))),
% 39.75/5.63 inference(formula_renaming,[status(thm)],[f250,f351])).
% 39.75/5.63 fof(f353,plain,(
% 39.75/5.63 ![V0p,V1q,V2r]: ((~sP7_prd(V2r,V1q,V0p)|((~p(V0p)|sP16_prd(V2r,V1q))&(p(V0p)|~sP16_prd(V2r,V1q))))&(sP7_prd(V2r,V1q,V0p)|((~p(V0p)|~sP16_prd(V2r,V1q))&(p(V0p)|sP16_prd(V2r,V1q)))))),
% 39.75/5.63 inference(NNF_transformation,[status(thm)],[f352])).
% 39.75/5.63 fof(f354,plain,(
% 39.75/5.63 (![V0p,V1q,V2r]: (~sP7_prd(V2r,V1q,V0p)|((~p(V0p)|sP16_prd(V2r,V1q))&(p(V0p)|~sP16_prd(V2r,V1q)))))&(![V0p,V1q,V2r]: (sP7_prd(V2r,V1q,V0p)|((~p(V0p)|~sP16_prd(V2r,V1q))&(p(V0p)|sP16_prd(V2r,V1q)))))),
% 39.75/5.63 inference(miniscoping,[status(thm)],[f353])).
% 39.75/5.63 fof(f356,plain,(
% 39.75/5.63 ![X0,X1,X2]: (~sP7_prd(X0,X1,X2)|p(X2)|~sP16_prd(X0,X1))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f354])).
% 39.75/5.63 fof(f358,plain,(
% 39.75/5.63 ![X0,X1,X2]: (sP7_prd(X0,X1,X2)|p(X2)|sP16_prd(X0,X1))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f354])).
% 39.75/5.63 fof(f416,plain,(
% 39.75/5.63 ![V0p,V1q]: ((~sP15_prd(V1q,V0p)|((~p(V0p)|~p(V1q))&(p(V0p)|p(V1q))))&(sP15_prd(V1q,V0p)|((~p(V0p)|p(V1q))&(p(V0p)|~p(V1q)))))),
% 39.75/5.63 inference(NNF_transformation,[status(thm)],[f293])).
% 39.75/5.63 fof(f417,plain,(
% 39.75/5.63 (![V0p,V1q]: (~sP15_prd(V1q,V0p)|((~p(V0p)|~p(V1q))&(p(V0p)|p(V1q)))))&(![V0p,V1q]: (sP15_prd(V1q,V0p)|((~p(V0p)|p(V1q))&(p(V0p)|~p(V1q)))))),
% 39.75/5.63 inference(miniscoping,[status(thm)],[f416])).
% 39.75/5.63 fof(f419,plain,(
% 39.75/5.63 ![X0,X1]: (~sP15_prd(X0,X1)|p(X1)|p(X0))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f417])).
% 39.75/5.63 fof(f420,plain,(
% 39.75/5.63 ![X0,X1]: (sP15_prd(X0,X1)|~p(X1)|p(X0))),
% 39.75/5.63 inference(cnf_transformation,[status(thm)],[f417])).
% 39.75/5.63 fof(f480,definition,(
% 39.75/5.63 sQ3_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f482,plain,(
% 39.75/5.63 ~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|sQ3_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f480])).
% 39.75/5.63 fof(f483,definition,(
% 39.75/5.63 sQ4_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f484,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl))|~sQ4_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f483])).
% 39.75/5.63 fof(f486,plain,(
% 39.75/5.63 sQ3_spl|sQ4_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f309,f480,f483])).
% 39.75/5.63 fof(f487,plain,(
% 39.75/5.63 ~sQ3_spl|~sQ4_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f310,f480,f483])).
% 39.75/5.63 fof(f495,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|ap(ap(c_2Einteger_2Eint__sub,X0),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl)))),
% 39.75/5.63 inference(resolution,[status(thm)],[f211,f306])).
% 39.75/5.63 fof(f496,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|ap(ap(c_2Einteger_2Eint__sub,X0),sK6_skl)=ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK6_skl)))),
% 39.75/5.63 inference(resolution,[status(thm)],[f211,f305])).
% 39.75/5.63 fof(f505,plain,(
% 39.75/5.63 ![X0,X1,X2]: (ap(ap(c_2Einteger_2Eint__sub,ap(X0,X1)),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,ap(X0,X1)),ap(c_2Einteger_2Eint__neg,sK7_skl))|~mem(X0,arr(X2,ty_2Einteger_2Eint))|~mem(X1,X2))),
% 39.75/5.63 inference(resolution,[status(thm)],[f495,f64])).
% 39.75/5.63 fof(f506,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,sK8_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f495,f307])).
% 39.75/5.63 fof(f507,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f495,f306])).
% 39.75/5.63 fof(f508,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,sK6_skl),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f495,f305])).
% 39.75/5.63 fof(f509,plain,(
% 39.75/5.63 ![X0,X1,X2]: (ap(ap(c_2Einteger_2Eint__sub,ap(X0,X1)),sK6_skl)=ap(ap(c_2Einteger_2Eint__add,ap(X0,X1)),ap(c_2Einteger_2Eint__neg,sK6_skl))|~mem(X0,arr(X2,ty_2Einteger_2Eint))|~mem(X1,X2))),
% 39.75/5.63 inference(resolution,[status(thm)],[f496,f64])).
% 39.75/5.63 fof(f511,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl)=ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK6_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f496,f306])).
% 39.75/5.63 fof(f599,plain,(
% 39.75/5.63 ![X0]: (ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,X0)),sK6_skl)=ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,X0)),ap(c_2Einteger_2Eint__neg,sK6_skl))|~mem(X0,ty_2Einteger_2Eint))),
% 39.75/5.63 inference(resolution,[status(thm)],[f91,f509])).
% 39.75/5.63 fof(f600,plain,(
% 39.75/5.63 ![X0]: (ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,X0)),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,X0)),ap(c_2Einteger_2Eint__neg,sK7_skl))|~mem(X0,ty_2Einteger_2Eint))),
% 39.75/5.63 inference(resolution,[status(thm)],[f91,f505])).
% 39.75/5.63 fof(f677,plain,(
% 39.75/5.63 ![X0]: (~ne(bool)|p(ap(c_2Ebool_2E_3F(bool),c_2Ebool_2E_7E))|~mem(X0,bool)|~p(ap(c_2Ebool_2E_7E,X0)))),
% 39.75/5.63 inference(resolution,[status(thm)],[f113,f87])).
% 39.75/5.63 fof(f681,definition,(
% 39.75/5.63 sQ20_spl <=> (ne(bool))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f683,plain,(
% 39.75/5.63 ~ne(bool)|sQ20_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f681])).
% 39.75/5.63 fof(f684,definition,(
% 39.75/5.63 sQ21_spl <=> (p(ap(c_2Ebool_2E_3F(bool),c_2Ebool_2E_7E)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f687,definition,(
% 39.75/5.63 ![X0]: (sQ22_spl <=> (~mem(X0,bool)|~p(ap(c_2Ebool_2E_7E,X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f688,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,bool)|~p(ap(c_2Ebool_2E_7E,X0))|~sQ22_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f687])).
% 39.75/5.63 fof(f690,plain,(
% 39.75/5.63 ~sQ20_spl|sQ21_spl|sQ22_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f677,f681,f684,f687])).
% 39.75/5.63 fof(f691,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,bool)|p(X0)|~sQ22_spl)),
% 39.75/5.63 inference(backward_subsumption_resolution,[status(thm)],[f117,f688])).
% 39.75/5.63 fof(f709,definition,(
% 39.75/5.63 sQ23_spl <=> (ne(ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f711,plain,(
% 39.75/5.63 ~ne(ty_2Einteger_2Eint)|sQ23_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f709])).
% 39.75/5.63 fof(f720,plain,(
% 39.75/5.63 $false|sQ23_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f711,f88])).
% 39.75/5.63 fof(f721,plain,(
% 39.75/5.63 sQ23_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f720])).
% 39.75/5.63 fof(f734,plain,(
% 39.75/5.63 p(c_2Ebool_2EF)|~sQ22_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f691,f93])).
% 39.75/5.63 fof(f737,plain,(
% 39.75/5.63 $false|~sQ22_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f734,f94])).
% 39.75/5.63 fof(f738,plain,(
% 39.75/5.63 ~sQ22_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f737])).
% 39.75/5.63 fof(f739,plain,(
% 39.75/5.63 $false|sQ20_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f683,f59])).
% 39.75/5.63 fof(f740,plain,(
% 39.75/5.63 sQ20_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f739])).
% 39.75/5.63 fof(f746,definition,(
% 39.75/5.63 ![X1]: (sQ27_spl <=> (p(X1)|~p(X1)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f796,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK6_skl)=ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),ap(c_2Einteger_2Eint__neg,sK6_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f599,f306])).
% 39.75/5.63 fof(f825,plain,(
% 39.75/5.63 ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK7_skl)=ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),ap(c_2Einteger_2Eint__neg,sK7_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f600,f306])).
% 39.75/5.63 fof(f889,plain,(
% 39.75/5.63 ![X0,X1]: (~p(X0)|p(X1)|p(X0)|p(X1))),
% 39.75/5.63 inference(resolution,[status(thm)],[f420,f419])).
% 39.75/5.63 fof(f891,definition,(
% 39.75/5.63 ![X1]: (sQ29_spl <=> (p(X1)|p(X1)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f892,plain,(
% 39.75/5.63 ![X0]: (p(X0)|p(X0)|~sQ29_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f891])).
% 39.75/5.63 fof(f894,plain,(
% 39.75/5.63 sQ27_spl|sQ29_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f889,f746,f891])).
% 39.75/5.63 fof(f900,plain,(
% 39.75/5.63 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0)))),
% 39.75/5.63 inference(resolution,[status(thm)],[f214,f308])).
% 39.75/5.63 fof(f901,definition,(
% 39.75/5.63 sQ31_spl <=> (mem(sK6_skl,ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f903,plain,(
% 39.75/5.63 ~mem(sK6_skl,ty_2Einteger_2Eint)|sQ31_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f901])).
% 39.75/5.63 fof(f911,definition,(
% 39.75/5.63 sQ34_spl <=> (mem(sK7_skl,ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f913,plain,(
% 39.75/5.63 ~mem(sK7_skl,ty_2Einteger_2Eint)|sQ34_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f911])).
% 39.75/5.63 fof(f914,definition,(
% 39.75/5.63 ![X0]: (sQ35_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f915,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ35_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f914])).
% 39.75/5.63 fof(f917,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ34_spl|sQ35_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f900,f901,f911,f914])).
% 39.75/5.63 fof(f918,plain,(
% 39.75/5.63 $false|sQ31_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f903,f305])).
% 39.75/5.63 fof(f919,plain,(
% 39.75/5.63 sQ31_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f918])).
% 39.75/5.63 fof(f920,plain,(
% 39.75/5.63 $false|sQ34_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f913,f306])).
% 39.75/5.63 fof(f921,plain,(
% 39.75/5.63 sQ34_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f920])).
% 39.75/5.63 fof(f923,plain,(
% 39.75/5.63 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0))))),
% 39.75/5.63 inference(resolution,[status(thm)],[f215,f308])).
% 39.75/5.63 fof(f928,definition,(
% 39.75/5.63 ![X0]: (sQ37_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f929,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)))|~sQ37_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f928])).
% 39.75/5.63 fof(f931,plain,(
% 39.75/5.63 ~sQ31_spl|sQ37_spl|~sQ34_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f923,f901,f928,f911])).
% 39.75/5.63 fof(f933,plain,(
% 39.75/5.63 ~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))),
% 39.75/5.63 inference(resolution,[status(thm)],[f219,f308])).
% 39.75/5.63 fof(f938,definition,(
% 39.75/5.63 sQ39_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f939,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))|~sQ39_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f938])).
% 39.75/5.63 fof(f941,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ34_spl|sQ39_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f933,f901,f911,f938])).
% 39.75/5.63 fof(f943,plain,(
% 39.75/5.63 ~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),sK7_skl))),
% 39.75/5.63 inference(resolution,[status(thm)],[f221,f308])).
% 39.75/5.63 fof(f948,definition,(
% 39.75/5.63 sQ41_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),sK7_skl)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f949,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),sK7_skl))|~sQ41_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f948])).
% 39.75/5.63 fof(f951,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ34_spl|sQ41_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f943,f901,f911,f948])).
% 39.75/5.63 fof(f954,plain,(
% 39.75/5.63 ~mem(sK7_skl,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),sK7_skl)))|~sQ37_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f929,f308])).
% 39.75/5.63 fof(f959,definition,(
% 39.75/5.63 sQ43_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),sK7_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f960,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),sK7_skl)))|~sQ43_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f959])).
% 39.75/5.63 fof(f962,plain,(
% 39.75/5.63 ~sQ34_spl|sQ43_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f954,f911,f959,f928])).
% 39.75/5.63 fof(f963,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))))|~sQ39_spl|~sQ37_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f939,f929])).
% 39.75/5.63 fof(f965,plain,(
% 39.75/5.63 ~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(c_2Einteger_2Eint__neg,sK7_skl)))|~sQ39_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f939,f221])).
% 39.75/5.63 fof(f966,plain,(
% 39.75/5.63 ~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__neg,sK7_skl))))|~sQ39_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f939,f219])).
% 39.75/5.63 fof(f967,plain,(
% 39.75/5.63 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)))|~sQ39_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f939,f215])).
% 39.75/5.63 fof(f968,plain,(
% 39.75/5.63 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ39_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f939,f214])).
% 39.75/5.63 fof(f969,definition,(
% 39.75/5.63 sQ44_spl <=> (mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f971,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|sQ44_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f969])).
% 39.75/5.63 fof(f972,definition,(
% 39.75/5.63 sQ45_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f975,plain,(
% 39.75/5.63 ~sQ44_spl|sQ45_spl|~sQ39_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f963,f969,f972,f938,f928])).
% 39.75/5.63 fof(f976,definition,(
% 39.75/5.63 sQ46_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK7_skl)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f980,definition,(
% 39.75/5.63 sQ47_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(c_2Einteger_2Eint__neg,sK7_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f981,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(c_2Einteger_2Eint__neg,sK7_skl)))|~sQ47_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f980])).
% 39.75/5.63 fof(f983,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ44_spl|sQ47_spl|~sQ39_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f965,f901,f969,f980,f938])).
% 39.75/5.63 fof(f984,definition,(
% 39.75/5.63 sQ48_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__neg,sK7_skl)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f987,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ44_spl|sQ48_spl|~sQ39_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f966,f901,f969,f984,f938])).
% 39.75/5.63 fof(f988,definition,(
% 39.75/5.63 ![X0]: (sQ49_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f989,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)))|~sQ49_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f988])).
% 39.75/5.63 fof(f991,plain,(
% 39.75/5.63 ~sQ31_spl|sQ49_spl|~sQ44_spl|~sQ39_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f967,f901,f988,f969,f938])).
% 39.75/5.63 fof(f992,definition,(
% 39.75/5.63 ![X0]: (sQ50_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f993,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ50_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f992])).
% 39.75/5.63 fof(f995,plain,(
% 39.75/5.63 ~sQ31_spl|~sQ44_spl|sQ50_spl|~sQ39_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f968,f901,f969,f992,f938])).
% 39.75/5.63 fof(f996,plain,(
% 39.75/5.63 ![X0]: (~mem(c_2Einteger_2Eint__neg,arr(X0,ty_2Einteger_2Eint))|~mem(sK7_skl,X0)|sQ44_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f971,f64])).
% 39.75/5.63 fof(f998,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__neg,sK6_skl))),sK7_skl))|~sQ41_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f949,f221])).
% 39.75/5.63 fof(f1000,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)))|~sQ41_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f949,f215])).
% 39.75/5.63 fof(f1001,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(sK7_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,X0),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|~sQ41_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f949,f214])).
% 39.75/5.63 fof(f1003,definition,(
% 39.75/5.63 sQ51_spl <=> (mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1006,definition,(
% 39.75/5.63 sQ52_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__neg,sK6_skl))),sK7_skl)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1009,plain,(
% 39.75/5.63 ~sQ51_spl|~sQ34_spl|sQ52_spl|~sQ41_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f998,f1003,f911,f1006,f948])).
% 39.75/5.63 fof(f1011,definition,(
% 39.75/5.63 ![X0]: (sQ53_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1014,plain,(
% 39.75/5.63 ~sQ51_spl|sQ53_spl|~sQ34_spl|~sQ41_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1000,f1003,f1011,f911,f948])).
% 39.75/5.63 fof(f1015,definition,(
% 39.75/5.63 ![X0]: (sQ54_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,X0),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1018,plain,(
% 39.75/5.63 ~sQ51_spl|~sQ34_spl|sQ54_spl|~sQ41_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1001,f1003,f911,f1015,f948])).
% 39.75/5.63 fof(f1020,plain,(
% 39.75/5.63 ~mem(sK7_skl,ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK7_skl))|~sQ43_spl|~sQ35_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f960,f915])).
% 39.75/5.63 fof(f1026,plain,(
% 39.75/5.63 ~sQ34_spl|sQ46_spl|~sQ43_spl|~sQ35_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1020,f911,f976,f959,f914])).
% 39.75/5.63 fof(f1402,plain,(
% 39.75/5.63 ![X0,X1,X2]: (p(X0)|sP16_prd(X1,X2)|p(X0)|~sP16_prd(X1,X2))),
% 39.75/5.63 inference(resolution,[status(thm)],[f358,f356])).
% 39.75/5.63 fof(f1404,definition,(
% 39.75/5.63 ![X1,X2]: (sQ61_spl <=> (sP16_prd(X1,X2)|~sP16_prd(X1,X2)))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1407,plain,(
% 39.75/5.63 sQ29_spl|sQ61_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1402,f891,f1404])).
% 39.75/5.63 fof(f1434,plain,(
% 39.75/5.63 $false|~sQ29_spl),
% 39.75/5.63 inference(backward_subsumption_resolution,[status(thm)],[f94,f1454])).
% 39.75/5.63 fof(f1454,plain,(
% 39.75/5.63 ![X0]: (p(X0)|~sQ29_spl)),
% 39.75/5.63 inference(duplicate_literals_removal,[status(thm)],[f892])).
% 39.75/5.63 fof(f1468,plain,(
% 39.75/5.63 ~sQ29_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f1434])).
% 39.75/5.63 fof(f1489,plain,(
% 39.75/5.63 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)),X1)))|~sQ37_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f929,f215])).
% 39.75/5.63 fof(f1490,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl)))|~sQ37_spl),
% 39.75/5.63 inference(paramodulation,[status(thm)],[f511,f929])).
% 39.75/5.63 fof(f1491,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK7_skl)))|~sQ37_spl),
% 39.75/5.63 inference(paramodulation,[status(thm)],[f507,f929])).
% 39.75/5.63 fof(f1493,definition,(
% 39.75/5.63 ![X0,X1]: (sQ63_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(X1,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)),X1)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1494,plain,(
% 39.75/5.63 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(X1,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0)),X1)))|~sQ63_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1493])).
% 39.75/5.63 fof(f1496,plain,(
% 39.75/5.63 sQ63_spl|~sQ31_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1489,f1493,f901,f928])).
% 39.75/5.63 fof(f1497,definition,(
% 39.75/5.63 sQ64_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1498,plain,(
% 39.75/5.63 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|~sQ64_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1497])).
% 39.75/5.63 fof(f1499,plain,(
% 39.75/5.63 ~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|sQ64_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1497])).
% 39.75/5.63 fof(f1500,definition,(
% 39.75/5.63 sQ65_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1503,plain,(
% 39.75/5.63 ~sQ51_spl|~sQ64_spl|sQ65_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1490,f1003,f1497,f1500,f928])).
% 39.75/5.63 fof(f1504,definition,(
% 39.75/5.63 sQ66_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK7_skl))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1507,plain,(
% 39.75/5.63 ~sQ44_spl|~sQ39_spl|sQ66_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1491,f969,f938,f1504,f928])).
% 39.75/5.63 fof(f1535,plain,(
% 39.75/5.63 ![X0,X1]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X1),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ37_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f214,f929])).
% 39.75/5.63 fof(f1543,definition,(
% 39.75/5.63 ![X0,X1]: (sQ70_spl <=> (~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X1),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1544,plain,(
% 39.75/5.63 ![X0,X1]: (~mem(ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0),ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X1),ap(ap(c_2Einteger_2Eint__add,sK7_skl),X0))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ70_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1543])).
% 39.75/5.63 fof(f1546,plain,(
% 39.75/5.63 ~sQ31_spl|sQ70_spl|~sQ37_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1535,f901,f1543,f928])).
% 39.75/5.63 fof(f1563,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|~sQ47_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f981,f214])).
% 39.75/5.63 fof(f1564,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)))|~sQ47_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f981,f215])).
% 39.75/5.63 fof(f1567,definition,(
% 39.75/5.63 ![X0]: (sQ71_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK7_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1570,plain,(
% 39.75/5.63 ~sQ51_spl|~sQ44_spl|sQ71_spl|~sQ47_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1563,f1003,f969,f1567,f980])).
% 39.75/5.63 fof(f1571,definition,(
% 39.75/5.63 ![X0]: (sQ72_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0))|p(ap(ap(c_2Einteger_2Eint__divides,ap(c_2Einteger_2Eint__neg,sK6_skl)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1574,plain,(
% 39.75/5.63 ~sQ51_spl|sQ72_spl|~sQ44_spl|~sQ47_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1564,f1003,f1571,f969,f980])).
% 39.75/5.63 fof(f1690,definition,(
% 39.75/5.63 sQ76_spl <=> (mem(sK8_skl,ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1692,plain,(
% 39.75/5.63 ~mem(sK8_skl,ty_2Einteger_2Eint)|sQ76_spl),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1690])).
% 39.75/5.63 fof(f1694,plain,(
% 39.75/5.63 $false|sQ76_spl),
% 39.75/5.63 inference(forward_subsumption_resolution,[status(thm)],[f1692,f307])).
% 39.75/5.63 fof(f1695,plain,(
% 39.75/5.63 sQ76_spl),
% 39.75/5.63 inference(contradiction_clause,[status(thm)],[f1694])).
% 39.75/5.63 fof(f1857,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|~mem(X0,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK6_skl))),X0)))|~sQ63_spl)),
% 39.75/5.63 inference(paramodulation,[status(thm)],[f511,f1494])).
% 39.75/5.63 fof(f1860,definition,(
% 39.75/5.63 ![X0]: (sQ77_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK6_skl))),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1863,definition,(
% 39.75/5.63 sQ78_spl <=> (mem(ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl),ty_2Einteger_2Eint))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1866,plain,(
% 39.75/5.63 ~sQ51_spl|~sQ64_spl|sQ77_spl|~sQ78_spl|~sQ63_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1857,f1003,f1497,f1860,f1863,f1493])).
% 39.75/5.63 fof(f1886,plain,(
% 39.75/5.63 ![X0]: (~mem(ap(ap(c_2Einteger_2Eint__sub,sK7_skl),sK6_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|~sQ70_spl)),
% 39.75/5.63 inference(paramodulation,[status(thm)],[f511,f1544])).
% 39.75/5.63 fof(f1889,definition,(
% 39.75/5.63 ![X0]: (sQ82_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(ap(c_2Einteger_2Eint__add,sK7_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1892,plain,(
% 39.75/5.63 ~sQ78_spl|sQ82_spl|~sQ51_spl|~sQ64_spl|~sQ70_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1886,f1863,f1889,f1003,f1497,f1543])).
% 39.75/5.63 fof(f1915,plain,(
% 39.75/5.63 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(sK8_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),X0)))|~sQ4_spl)),
% 39.75/5.63 inference(resolution,[status(thm)],[f484,f215])).
% 39.75/5.63 fof(f1920,definition,(
% 39.75/5.63 ![X0]: (sQ88_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),X0)))))),
% 39.75/5.63 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 39.75/5.63 fof(f1921,plain,(
% 39.75/5.63 ![X0]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),X0)))|~sQ88_spl)),
% 39.75/5.63 inference(component_clause,[status(thm)],[f1920])).
% 39.75/5.63 fof(f1923,plain,(
% 39.75/5.63 ~sQ31_spl|sQ88_spl|~sQ76_spl|~sQ4_spl),
% 39.75/5.63 inference(split_clause,[status(thm)],[f1915,f901,f1920,f1690,f483])).
% 39.75/5.63 fof(f1928,plain,(
% 39.75/5.63 ~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))))|~sQ88_spl|~sQ39_spl),
% 39.75/5.63 inference(resolution,[status(thm)],[f1921,f939])).
% 39.75/5.63 fof(f1941,definition,(
% 39.75/5.63 sQ91_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f1942,plain,(
% 40.49/5.65 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK8_skl),ap(c_2Einteger_2Eint__neg,sK7_skl))))|~sQ91_spl),
% 40.49/5.65 inference(component_clause,[status(thm)],[f1941])).
% 40.49/5.65 fof(f1944,plain,(
% 40.49/5.65 ~sQ44_spl|sQ91_spl|~sQ88_spl|~sQ39_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f1928,f969,f1941,f1920,f938])).
% 40.49/5.65 fof(f2130,plain,(
% 40.49/5.65 ~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(sK6_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK6_skl))|sQ64_spl),
% 40.49/5.65 inference(resolution,[status(thm)],[f1499,f219])).
% 40.49/5.65 fof(f2131,definition,(
% 40.49/5.65 sQ112_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK6_skl)))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2132,plain,(
% 40.49/5.65 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK6_skl))|~sQ112_spl),
% 40.49/5.65 inference(component_clause,[status(thm)],[f2131])).
% 40.49/5.65 fof(f2134,plain,(
% 40.49/5.65 ~sQ31_spl|~sQ112_spl|sQ64_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2130,f901,f2131,f1497])).
% 40.49/5.65 fof(f2159,plain,(
% 40.49/5.65 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK6_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ64_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f1498,f214])).
% 40.49/5.65 fof(f2160,plain,(
% 40.49/5.65 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0)))|~sQ64_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f1498,f215])).
% 40.49/5.65 fof(f2162,definition,(
% 40.49/5.65 ![X0]: (sQ113_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),ap(c_2Einteger_2Eint__neg,sK6_skl))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2165,plain,(
% 40.49/5.65 ~sQ31_spl|~sQ51_spl|sQ113_spl|~sQ64_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2159,f901,f1003,f2162,f1497])).
% 40.49/5.65 fof(f2166,definition,(
% 40.49/5.65 ![X0]: (sQ114_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK6_skl)),X0)))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2169,plain,(
% 40.49/5.65 ~sQ31_spl|sQ114_spl|~sQ51_spl|~sQ64_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2160,f901,f2166,f1003,f1497])).
% 40.49/5.65 fof(f2170,plain,(
% 40.49/5.65 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),sK6_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~sQ112_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f2132,f214])).
% 40.49/5.65 fof(f2171,plain,(
% 40.49/5.65 ![X0]: (~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X0,ty_2Einteger_2Eint)|~mem(sK6_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK6_skl),X0)))|~sQ112_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f2132,f215])).
% 40.49/5.65 fof(f2172,definition,(
% 40.49/5.65 ![X0]: (sQ115_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X0),sK6_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2175,plain,(
% 40.49/5.65 ~sQ31_spl|sQ115_spl|~sQ112_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2170,f901,f2172,f2131])).
% 40.49/5.65 fof(f2176,definition,(
% 40.49/5.65 ![X0]: (sQ116_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,sK6_skl),X0)))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2179,plain,(
% 40.49/5.65 ~sQ31_spl|sQ116_spl|~sQ112_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2171,f901,f2176,f2131])).
% 40.49/5.65 fof(f2368,plain,(
% 40.49/5.65 ~mem(sK7_skl,ty_2Einteger_2Eint)|sQ44_spl),
% 40.49/5.65 inference(resolution,[status(thm)],[f996,f91])).
% 40.49/5.65 fof(f2369,plain,(
% 40.49/5.65 ~sQ34_spl|sQ44_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2368,f911,f969])).
% 40.49/5.65 fof(f2391,plain,(
% 40.49/5.65 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0),ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X1),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|~sQ49_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f989,f214])).
% 40.49/5.65 fof(f2392,plain,(
% 40.49/5.65 ![X0,X1]: (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(sK6_skl,ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)),X1)))|~sQ49_spl)),
% 40.49/5.65 inference(resolution,[status(thm)],[f989,f215])).
% 40.49/5.65 fof(f2394,plain,(
% 40.49/5.65 ~mem(ap(c_2Einteger_2Eint__neg,sK7_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK7_skl)))|~sQ49_spl),
% 40.49/5.65 inference(paramodulation,[status(thm)],[f825,f989])).
% 40.49/5.65 fof(f2395,plain,(
% 40.49/5.65 ~mem(ap(c_2Einteger_2Eint__neg,sK6_skl),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(c_2Einteger_2Eint__neg,sK6_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK6_skl)))|~sQ49_spl),
% 40.49/5.65 inference(paramodulation,[status(thm)],[f796,f989])).
% 40.49/5.65 fof(f2397,definition,(
% 40.49/5.65 ![X0,X1]: (sQ125_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0),ty_2Einteger_2Eint)|~mem(X1,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,X1),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0))))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2400,plain,(
% 40.49/5.65 sQ125_spl|~sQ31_spl|~sQ49_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2391,f2397,f901,f988])).
% 40.49/5.65 fof(f2401,definition,(
% 40.49/5.65 ![X0,X1]: (sQ126_spl <=> (~mem(X0,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X0))|~mem(X1,ty_2Einteger_2Eint)|~mem(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0),ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),X1))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,sK7_skl)),X0)),X1)))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2404,plain,(
% 40.49/5.65 sQ126_spl|~sQ31_spl|~sQ49_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2392,f2401,f901,f988])).
% 40.49/5.65 fof(f2409,definition,(
% 40.49/5.65 sQ128_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK7_skl))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2412,plain,(
% 40.49/5.65 ~sQ44_spl|~sQ39_spl|sQ128_spl|~sQ49_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2394,f969,f938,f2409,f988])).
% 40.49/5.65 fof(f2413,definition,(
% 40.49/5.65 sQ129_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,sK7_skl)),sK6_skl))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2416,plain,(
% 40.49/5.65 ~sQ51_spl|~sQ64_spl|sQ129_spl|~sQ49_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2395,f1003,f1497,f2413,f988])).
% 40.49/5.65 fof(f2426,plain,(
% 40.49/5.65 ~mem(sK6_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK6_skl),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK6_skl))|~sQ50_spl),
% 40.49/5.65 inference(paramodulation,[status(thm)],[f508,f993])).
% 40.49/5.65 fof(f2428,plain,(
% 40.49/5.65 ~mem(sK8_skl,ty_2Einteger_2Eint)|~p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),sK8_skl))|~sQ50_spl),
% 40.49/5.65 inference(paramodulation,[status(thm)],[f506,f993])).
% 40.49/5.65 fof(f2468,definition,(
% 40.49/5.65 sQ140_spl <=> (p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK6_skl),sK7_skl))))),
% 40.49/5.65 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 40.49/5.65 fof(f2471,plain,(
% 40.49/5.65 ~sQ31_spl|~sQ140_spl|sQ112_spl|~sQ50_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2426,f901,f2468,f2131,f992])).
% 40.49/5.65 fof(f2473,plain,(
% 40.49/5.65 ~sQ76_spl|~sQ3_spl|sQ4_spl|~sQ50_spl),
% 40.49/5.65 inference(split_clause,[status(thm)],[f2428,f1690,f480,f483,f992])).
% 40.49/5.65 fof(f2474,plain,(
% 40.49/5.65 p(ap(ap(c_2Einteger_2Eint__divides,sK6_skl),ap(ap(c_2Einteger_2Eint__sub,sK8_skl),sK7_skl)))|~sQ91_spl),
% 40.49/5.65 inference(forward_demodulation,[status(thm)],[f506,f1942])).
% 40.49/5.65 fof(f2891,plain,(
% 40.49/5.65 $false|~sQ91_spl|sQ3_spl),
% 40.49/5.65 inference(forward_subsumption_resolution,[status(thm)],[f482,f2474])).
% 40.49/5.65 fof(f2892,plain,(
% 40.49/5.65 ~sQ91_spl|sQ3_spl),
% 40.49/5.65 inference(contradiction_clause,[status(thm)],[f2891])).
% 40.49/5.65 fof(f2893,plain,(
% 40.49/5.65 $false),
% 40.49/5.65 inference(sat_refutation,[status(thm)],[f486,f487,f690,f721,f738,f740,f894,f917,f919,f921,f931,f941,f951,f962,f975,f983,f987,f991,f995,f1009,f1014,f1018,f1026,f1407,f1468,f1496,f1503,f1507,f1546,f1570,f1574,f1695,f1866,f1892,f1923,f1944,f2134,f2165,f2169,f2175,f2179,f2369,f2400,f2404,f2412,f2416,f2471,f2473,f2892])).
% 40.49/5.65 % SZS output end CNFRefutation for theBenchmark.p
% 40.49/5.71 % Elapsed time: 5.235334 seconds
% 40.49/5.71 % CPU time: 40.920724 seconds
% 40.49/5.71 % Total memory used: 367.659 MB
% 40.49/5.71 % Net memory used: 348.190 MB
%------------------------------------------------------------------------------