%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:49:58 PM UTC 2026
% Result : Theorem 144.13s 18.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n010.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 08:28:10 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.50 % Drodi V4.1.1
% 144.13/18.76 % Refutation found
% 144.13/18.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 144.13/18.76 % SZS output start CNFRefutation for theBenchmark
% 144.13/18.76 fof(f3,axiom,(
% 144.13/18.76 (! [X] : ~ gt(X,X) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f4,axiom,(
% 144.13/18.76 (! [X] : leq(X,X) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f5,axiom,(
% 144.13/18.76 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f8,axiom,(
% 144.13/18.76 (! [X,Y] :( gt(Y,X)=> leq(X,Y) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f9,axiom,(
% 144.13/18.76 (! [X,Y] :( ( leq(X,Y)& X != Y )=> gt(Y,X) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f10,axiom,(
% 144.13/18.76 (! [X,Y] :( leq(X,pred(Y))<=> gt(Y,X) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f11,axiom,(
% 144.13/18.76 (! [X] : gt(succ(X),X) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f34,axiom,(
% 144.13/18.76 (! [X] : plus(n3,X) = succ(succ(succ(X))) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f36,axiom,(
% 144.13/18.76 (! [X] : plus(n4,X) = succ(succ(succ(succ(X)))) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f40,axiom,(
% 144.13/18.76 (! [X] : pred(succ(X)) = X )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f53,conjecture,(
% 144.13/18.76 ( ( init = init& leq(n0,pv7)& leq(n0,pv19)& leq(n0,pv20)& leq(n0,pv1376)& leq(pv7,minus(n410,n1))& leq(pv19,minus(n410,n1))& leq(pv20,minus(n330,n1))& leq(pv1376,n3)& (! [A] :( ( leq(n0,A)& leq(A,n2) )=> (! [B] :( ( leq(n0,B)& leq(B,n3) )=> a_select3(simplex7_init,B,A) = init ) )))& (! [C] :( ( leq(n0,C)& leq(C,minus(pv1376,n1)) )=> a_select2(s_values7_init,C) = init ) ))=> ( init = init& leq(n0,pv7)& leq(n0,pv19)& leq(n0,pv20)& leq(n0,pv1376)& leq(pv7,minus(n410,n1))& leq(pv19,minus(n410,n1))& leq(pv20,minus(n330,n1))& leq(pv1376,n3)& (! [D] :( ( leq(n0,D)& leq(D,n2) )=> (! [E] :( ( leq(n0,E)& leq(E,n3) )=> a_select3(simplex7_init,E,D) = init ) )))& (! [F] :( ( leq(n0,F)& leq(F,minus(pv1376,n1)) )=> a_select2(s_values7_init,F) = init ) )) ) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f54,negated_conjecture,(
% 144.13/18.76 ~(( ( init = init& leq(n0,pv7)& leq(n0,pv19)& leq(n0,pv20)& leq(n0,pv1376)& leq(pv7,minus(n410,n1))& leq(pv19,minus(n410,n1))& leq(pv20,minus(n330,n1))& leq(pv1376,n3)& (! [A] :( ( leq(n0,A)& leq(A,n2) )=> (! [B] :( ( leq(n0,B)& leq(B,n3) )=> a_select3(simplex7_init,B,A) = init ) )))& (! [C] :( ( leq(n0,C)& leq(C,minus(pv1376,n1)) )=> a_select2(s_values7_init,C) = init ) ))=> ( init = init& leq(n0,pv7)& leq(n0,pv19)& leq(n0,pv20)& leq(n0,pv1376)& leq(pv7,minus(n410,n1))& leq(pv19,minus(n410,n1))& leq(pv20,minus(n330,n1))& leq(pv1376,n3)& (! [D] :( ( leq(n0,D)& leq(D,n2) )=> (! [E] :( ( leq(n0,E)& leq(E,n3) )=> a_select3(simplex7_init,E,D) = init ) )))& (! [F] :( ( leq(n0,F)& leq(F,minus(pv1376,n1)) )=> a_select2(s_values7_init,F) = init ) )) ) )),
% 144.13/18.76 inference(negated_conjecture,[status(cth)],[f53])).
% 144.13/18.76 fof(f55,axiom,(
% 144.13/18.76 gt(n5,n4) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f60,axiom,(
% 144.13/18.76 gt(n410,n330) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f71,axiom,(
% 144.13/18.76 gt(n330,n0) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f72,axiom,(
% 144.13/18.76 gt(n410,n0) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f73,axiom,(
% 144.13/18.76 gt(n1,n0) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f74,axiom,(
% 144.13/18.76 gt(n2,n0) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f75,axiom,(
% 144.13/18.76 gt(n3,n0) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f78,axiom,(
% 144.13/18.76 gt(n330,n1) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f79,axiom,(
% 144.13/18.76 gt(n410,n1) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f80,axiom,(
% 144.13/18.76 gt(n2,n1) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f81,axiom,(
% 144.13/18.76 gt(n3,n1) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f84,axiom,(
% 144.13/18.76 gt(n330,n2) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f85,axiom,(
% 144.13/18.76 gt(n410,n2) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f86,axiom,(
% 144.13/18.76 gt(n3,n2) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f89,axiom,(
% 144.13/18.76 gt(n330,n3) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f90,axiom,(
% 144.13/18.76 gt(n410,n3) ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f93,axiom,(
% 144.13/18.76 (! [X] :( ( leq(n0,X)& leq(X,n0) )=> X = n0 ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f94,axiom,(
% 144.13/18.76 (! [X] :( ( leq(n0,X)& leq(X,n1) )=> ( X = n0| X = n1 ) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f95,axiom,(
% 144.13/18.76 (! [X] :( ( leq(n0,X)& leq(X,n2) )=> ( X = n0| X = n1| X = n2 ) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f96,axiom,(
% 144.13/18.76 (! [X] :( ( leq(n0,X)& leq(X,n3) )=> ( X = n0| X = n1| X = n2| X = n3 ) ) )),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f97,axiom,(
% 144.13/18.76 succ(succ(succ(succ(n0)))) = n4 ),
% 144.13/18.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 144.13/18.76 fof(f106,plain,(
% 144.13/18.76 ![X0]: (~gt(X0,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f3])).
% 144.13/18.76 fof(f107,plain,(
% 144.13/18.76 ![X0]: (leq(X0,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f4])).
% 144.13/18.76 fof(f108,plain,(
% 144.13/18.76 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 144.13/18.76 fof(f109,plain,(
% 144.13/18.76 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 144.13/18.76 inference(miniscoping,[status(thm)],[f108])).
% 144.13/18.76 fof(f110,plain,(
% 144.13/18.76 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f109])).
% 144.13/18.76 fof(f119,plain,(
% 144.13/18.76 ![X,Y]: (~gt(Y,X)|leq(X,Y))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 144.13/18.76 fof(f120,plain,(
% 144.13/18.76 ![X0,X1]: (~gt(X0,X1)|leq(X1,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f119])).
% 144.13/18.76 fof(f121,plain,(
% 144.13/18.76 ![X,Y]: ((~leq(X,Y)|X=Y)|gt(Y,X))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 144.13/18.76 fof(f122,plain,(
% 144.13/18.76 ![X0,X1]: (~leq(X0,X1)|X0=X1|gt(X1,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f121])).
% 144.13/18.76 fof(f123,plain,(
% 144.13/18.76 ![X,Y]: ((~leq(X,pred(Y))|gt(Y,X))&(leq(X,pred(Y))|~gt(Y,X)))),
% 144.13/18.76 inference(NNF_transformation,[status(thm)],[f10])).
% 144.13/18.76 fof(f124,plain,(
% 144.13/18.76 (![X,Y]: (~leq(X,pred(Y))|gt(Y,X)))&(![X,Y]: (leq(X,pred(Y))|~gt(Y,X)))),
% 144.13/18.76 inference(miniscoping,[status(thm)],[f123])).
% 144.13/18.76 fof(f125,plain,(
% 144.13/18.76 ![X0,X1]: (~leq(X0,pred(X1))|gt(X1,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f124])).
% 144.13/18.76 fof(f126,plain,(
% 144.13/18.76 ![X0,X1]: (leq(X0,pred(X1))|~gt(X1,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f124])).
% 144.13/18.76 fof(f127,plain,(
% 144.13/18.76 ![X0]: (gt(succ(X0),X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f11])).
% 144.13/18.76 fof(f220,plain,(
% 144.13/18.76 ![X0]: (plus(n3,X0)=succ(succ(succ(X0))))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f34])).
% 144.13/18.76 fof(f222,plain,(
% 144.13/18.76 ![X0]: (plus(n4,X0)=succ(succ(succ(succ(X0)))))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f36])).
% 144.13/18.76 fof(f226,plain,(
% 144.13/18.76 ![X0]: (pred(succ(X0))=X0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f40])).
% 144.13/18.76 fof(f259,plain,(
% 144.13/18.76 (((((((((((init=init&leq(n0,pv7))&leq(n0,pv19))&leq(n0,pv20))&leq(n0,pv1376))&leq(pv7,minus(n410,n1)))&leq(pv19,minus(n410,n1)))&leq(pv20,minus(n330,n1)))&leq(pv1376,n3))&(![A]: ((~leq(n0,A)|~leq(A,n2))|(![B]: ((~leq(n0,B)|~leq(B,n3))|a_select3(simplex7_init,B,A)=init)))))&(![C]: ((~leq(n0,C)|~leq(C,minus(pv1376,n1)))|a_select2(s_values7_init,C)=init)))&((((((((((~init=init|~leq(n0,pv7))|~leq(n0,pv19))|~leq(n0,pv20))|~leq(n0,pv1376))|~leq(pv7,minus(n410,n1)))|~leq(pv19,minus(n410,n1)))|~leq(pv20,minus(n330,n1)))|~leq(pv1376,n3))|(?[D]: ((leq(n0,D)&leq(D,n2))&(?[E]: ((leq(n0,E)&leq(E,n3))&~a_select3(simplex7_init,E,D)=init)))))|(?[F]: ((leq(n0,F)&leq(F,minus(pv1376,n1)))&~a_select2(s_values7_init,F)=init))))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 144.13/18.76 fof(f260,definition,(
% 144.13/18.76 ![D]: (sP3_prd(D)<=>((leq(n0,D)&leq(D,n2))&(?[E]: ((leq(n0,E)&leq(E,n3))&~a_select3(simplex7_init,E,D)=init))))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 144.13/18.76 fof(f261,plain,(
% 144.13/18.76 ((((((((((init=init&leq(n0,pv7))&leq(n0,pv19))&leq(n0,pv20))&leq(n0,pv1376))&leq(pv7,minus(n410,n1)))&leq(pv19,minus(n410,n1)))&leq(pv20,minus(n330,n1)))&leq(pv1376,n3))&(![A]: ((~leq(n0,A)|~leq(A,n2))|(![B]: ((~leq(n0,B)|~leq(B,n3))|a_select3(simplex7_init,B,A)=init)))))&(![C]: ((~leq(n0,C)|~leq(C,minus(pv1376,n1)))|a_select2(s_values7_init,C)=init)))&((((((((((~init=init|~leq(n0,pv7))|~leq(n0,pv19))|~leq(n0,pv20))|~leq(n0,pv1376))|~leq(pv7,minus(n410,n1)))|~leq(pv19,minus(n410,n1)))|~leq(pv20,minus(n330,n1)))|~leq(pv1376,n3))|(?[D]: sP3_prd(D)))|(?[F]: ((leq(n0,F)&leq(F,minus(pv1376,n1)))&~a_select2(s_values7_init,F)=init)))),
% 144.13/18.76 inference(formula_renaming,[status(thm)],[f259,f260])).
% 144.13/18.76 fof(f262,plain,(
% 144.13/18.76 ((((((((((init=init&leq(n0,pv7))&leq(n0,pv19))&leq(n0,pv20))&leq(n0,pv1376))&leq(pv7,minus(n410,n1)))&leq(pv19,minus(n410,n1)))&leq(pv20,minus(n330,n1)))&leq(pv1376,n3))&(![A]: ((~leq(n0,A)|~leq(A,n2))|(![B]: ((~leq(n0,B)|~leq(B,n3))|a_select3(simplex7_init,B,A)=init)))))&(![C]: ((~leq(n0,C)|~leq(C,minus(pv1376,n1)))|a_select2(s_values7_init,C)=init)))&((((((((((~init=init|~leq(n0,pv7))|~leq(n0,pv19))|~leq(n0,pv20))|~leq(n0,pv1376))|~leq(pv7,minus(n410,n1)))|~leq(pv19,minus(n410,n1)))|~leq(pv20,minus(n330,n1)))|~leq(pv1376,n3))|sP3_prd(sK23_skl))|((leq(n0,sK24_skl)&leq(sK24_skl,minus(pv1376,n1)))&~a_select2(s_values7_init,sK24_skl)=init))),
% 144.13/18.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(D,sK23_skl),skolemize(F,sK24_skl)],[f261])).
% 144.13/18.76 fof(f264,plain,(
% 144.13/18.76 leq(n0,pv7)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f265,plain,(
% 144.13/18.76 leq(n0,pv19)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f266,plain,(
% 144.13/18.76 leq(n0,pv20)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f267,plain,(
% 144.13/18.76 leq(n0,pv1376)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f268,plain,(
% 144.13/18.76 leq(pv7,minus(n410,n1))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f269,plain,(
% 144.13/18.76 leq(pv19,minus(n410,n1))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f270,plain,(
% 144.13/18.76 leq(pv20,minus(n330,n1))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f271,plain,(
% 144.13/18.76 leq(pv1376,n3)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f272,plain,(
% 144.13/18.76 ![X0,X1]: (~leq(n0,X0)|~leq(X0,n2)|~leq(n0,X1)|~leq(X1,n3)|a_select3(simplex7_init,X1,X0)=init)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f273,plain,(
% 144.13/18.76 ![X0]: (~leq(n0,X0)|~leq(X0,minus(pv1376,n1))|a_select2(s_values7_init,X0)=init)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f274,plain,(
% 144.13/18.76 ~init=init|~leq(n0,pv7)|~leq(n0,pv19)|~leq(n0,pv20)|~leq(n0,pv1376)|~leq(pv7,minus(n410,n1))|~leq(pv19,minus(n410,n1))|~leq(pv20,minus(n330,n1))|~leq(pv1376,n3)|sP3_prd(sK23_skl)|leq(n0,sK24_skl)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f275,plain,(
% 144.13/18.76 ~init=init|~leq(n0,pv7)|~leq(n0,pv19)|~leq(n0,pv20)|~leq(n0,pv1376)|~leq(pv7,minus(n410,n1))|~leq(pv19,minus(n410,n1))|~leq(pv20,minus(n330,n1))|~leq(pv1376,n3)|sP3_prd(sK23_skl)|leq(sK24_skl,minus(pv1376,n1))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f276,plain,(
% 144.13/18.76 ~init=init|~leq(n0,pv7)|~leq(n0,pv19)|~leq(n0,pv20)|~leq(n0,pv1376)|~leq(pv7,minus(n410,n1))|~leq(pv19,minus(n410,n1))|~leq(pv20,minus(n330,n1))|~leq(pv1376,n3)|sP3_prd(sK23_skl)|~a_select2(s_values7_init,sK24_skl)=init),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f262])).
% 144.13/18.76 fof(f277,plain,(
% 144.13/18.76 gt(n5,n4)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f55])).
% 144.13/18.76 fof(f282,plain,(
% 144.13/18.76 gt(n410,n330)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f60])).
% 144.13/18.76 fof(f293,plain,(
% 144.13/18.76 gt(n330,n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f71])).
% 144.13/18.76 fof(f294,plain,(
% 144.13/18.76 gt(n410,n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f72])).
% 144.13/18.76 fof(f295,plain,(
% 144.13/18.76 gt(n1,n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f73])).
% 144.13/18.76 fof(f296,plain,(
% 144.13/18.76 gt(n2,n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f74])).
% 144.13/18.76 fof(f297,plain,(
% 144.13/18.76 gt(n3,n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f75])).
% 144.13/18.76 fof(f300,plain,(
% 144.13/18.76 gt(n330,n1)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f78])).
% 144.13/18.76 fof(f301,plain,(
% 144.13/18.76 gt(n410,n1)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f79])).
% 144.13/18.76 fof(f302,plain,(
% 144.13/18.76 gt(n2,n1)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f80])).
% 144.13/18.76 fof(f303,plain,(
% 144.13/18.76 gt(n3,n1)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f81])).
% 144.13/18.76 fof(f306,plain,(
% 144.13/18.76 gt(n330,n2)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f84])).
% 144.13/18.76 fof(f307,plain,(
% 144.13/18.76 gt(n410,n2)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f85])).
% 144.13/18.76 fof(f308,plain,(
% 144.13/18.76 gt(n3,n2)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f86])).
% 144.13/18.76 fof(f311,plain,(
% 144.13/18.76 gt(n330,n3)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f89])).
% 144.13/18.76 fof(f312,plain,(
% 144.13/18.76 gt(n410,n3)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f90])).
% 144.13/18.76 fof(f317,plain,(
% 144.13/18.76 ![X]: ((~leq(n0,X)|~leq(X,n0))|X=n0)),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 144.13/18.76 fof(f318,plain,(
% 144.13/18.76 ![X0]: (~leq(n0,X0)|~leq(X0,n0)|X0=n0)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f317])).
% 144.13/18.76 fof(f319,plain,(
% 144.13/18.76 ![X]: ((~leq(n0,X)|~leq(X,n1))|(X=n0|X=n1))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 144.13/18.76 fof(f320,plain,(
% 144.13/18.76 ![X0]: (~leq(n0,X0)|~leq(X0,n1)|X0=n0|X0=n1)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f319])).
% 144.13/18.76 fof(f321,plain,(
% 144.13/18.76 ![X]: ((~leq(n0,X)|~leq(X,n2))|((X=n0|X=n1)|X=n2))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 144.13/18.76 fof(f322,plain,(
% 144.13/18.76 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|X0=n0|X0=n1|X0=n2)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f321])).
% 144.13/18.76 fof(f323,plain,(
% 144.13/18.76 ![X]: ((~leq(n0,X)|~leq(X,n3))|(((X=n0|X=n1)|X=n2)|X=n3))),
% 144.13/18.76 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 144.13/18.76 fof(f324,plain,(
% 144.13/18.76 ![X0]: (~leq(n0,X0)|~leq(X0,n3)|X0=n0|X0=n1|X0=n2|X0=n3)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f323])).
% 144.13/18.76 fof(f325,plain,(
% 144.13/18.76 succ(succ(succ(succ(n0))))=n4),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f97])).
% 144.13/18.76 fof(f358,plain,(
% 144.13/18.76 ![D]: ((~sP3_prd(D)|((leq(n0,D)&leq(D,n2))&(?[E]: ((leq(n0,E)&leq(E,n3))&~a_select3(simplex7_init,E,D)=init))))&(sP3_prd(D)|((~leq(n0,D)|~leq(D,n2))|(![E]: ((~leq(n0,E)|~leq(E,n3))|a_select3(simplex7_init,E,D)=init)))))),
% 144.13/18.76 inference(NNF_transformation,[status(thm)],[f260])).
% 144.13/18.76 fof(f359,plain,(
% 144.13/18.76 (![D]: (~sP3_prd(D)|((leq(n0,D)&leq(D,n2))&(?[E]: ((leq(n0,E)&leq(E,n3))&~a_select3(simplex7_init,E,D)=init)))))&(![D]: (sP3_prd(D)|((~leq(n0,D)|~leq(D,n2))|(![E]: ((~leq(n0,E)|~leq(E,n3))|a_select3(simplex7_init,E,D)=init)))))),
% 144.13/18.76 inference(miniscoping,[status(thm)],[f358])).
% 144.13/18.76 fof(f360,plain,(
% 144.13/18.76 (![D]: (~sP3_prd(D)|((leq(n0,D)&leq(D,n2))&((leq(n0,sK29_skl(D))&leq(sK29_skl(D),n3))&~a_select3(simplex7_init,sK29_skl(D),D)=init))))&(![D]: (sP3_prd(D)|((~leq(n0,D)|~leq(D,n2))|(![E]: ((~leq(n0,E)|~leq(E,n3))|a_select3(simplex7_init,E,D)=init)))))),
% 144.13/18.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(E,sK29_skl(D))],[f359])).
% 144.13/18.76 fof(f361,plain,(
% 144.13/18.76 ![X0]: (~sP3_prd(X0)|leq(n0,X0))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f360])).
% 144.13/18.76 fof(f362,plain,(
% 144.13/18.76 ![X0]: (~sP3_prd(X0)|leq(X0,n2))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f360])).
% 144.13/18.76 fof(f363,plain,(
% 144.13/18.76 ![X0]: (~sP3_prd(X0)|leq(n0,sK29_skl(X0)))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f360])).
% 144.13/18.76 fof(f364,plain,(
% 144.13/18.76 ![X0]: (~sP3_prd(X0)|leq(sK29_skl(X0),n3))),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f360])).
% 144.13/18.76 fof(f365,plain,(
% 144.13/18.76 ![X0]: (~sP3_prd(X0)|~a_select3(simplex7_init,sK29_skl(X0),X0)=init)),
% 144.13/18.76 inference(cnf_transformation,[status(thm)],[f360])).
% 144.13/18.76 fof(f375,definition,(
% 144.13/18.76 sQ0_spl <=> (init=init)),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f377,plain,(
% 144.13/18.76 ~init=init|sQ0_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f375])).
% 144.13/18.76 fof(f378,definition,(
% 144.13/18.76 sQ1_spl <=> (leq(n0,pv7))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f380,plain,(
% 144.13/18.76 ~leq(n0,pv7)|sQ1_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f378])).
% 144.13/18.76 fof(f381,definition,(
% 144.13/18.76 sQ2_spl <=> (leq(n0,pv19))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f383,plain,(
% 144.13/18.76 ~leq(n0,pv19)|sQ2_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f381])).
% 144.13/18.76 fof(f384,definition,(
% 144.13/18.76 sQ3_spl <=> (leq(n0,pv20))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f386,plain,(
% 144.13/18.76 ~leq(n0,pv20)|sQ3_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f384])).
% 144.13/18.76 fof(f387,definition,(
% 144.13/18.76 sQ4_spl <=> (leq(n0,pv1376))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f389,plain,(
% 144.13/18.76 ~leq(n0,pv1376)|sQ4_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f387])).
% 144.13/18.76 fof(f390,definition,(
% 144.13/18.76 sQ5_spl <=> (leq(pv7,minus(n410,n1)))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f392,plain,(
% 144.13/18.76 ~leq(pv7,minus(n410,n1))|sQ5_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f390])).
% 144.13/18.76 fof(f393,definition,(
% 144.13/18.76 sQ6_spl <=> (leq(pv19,minus(n410,n1)))),
% 144.13/18.76 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 144.13/18.76 fof(f395,plain,(
% 144.13/18.76 ~leq(pv19,minus(n410,n1))|sQ6_spl),
% 144.13/18.76 inference(component_clause,[status(thm)],[f393])).
% 144.13/18.76 fof(f396,definition,(
% 144.13/18.76 sQ7_spl <=> (leq(pv20,minus(n330,n1)))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f398,plain,(
% 144.13/18.77 ~leq(pv20,minus(n330,n1))|sQ7_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f396])).
% 144.13/18.77 fof(f399,definition,(
% 144.13/18.77 sQ8_spl <=> (leq(pv1376,n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f401,plain,(
% 144.13/18.77 ~leq(pv1376,n3)|sQ8_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f399])).
% 144.13/18.77 fof(f402,definition,(
% 144.13/18.77 sQ9_spl <=> (sP3_prd(sK23_skl))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f403,plain,(
% 144.13/18.77 sP3_prd(sK23_skl)|~sQ9_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f402])).
% 144.13/18.77 fof(f405,definition,(
% 144.13/18.77 sQ10_spl <=> (leq(n0,sK24_skl))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f408,plain,(
% 144.13/18.77 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ9_spl|sQ10_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f274,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f405])).
% 144.13/18.77 fof(f409,definition,(
% 144.13/18.77 sQ11_spl <=> (leq(sK24_skl,minus(pv1376,n1)))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f410,plain,(
% 144.13/18.77 leq(sK24_skl,minus(pv1376,n1))|~sQ11_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f409])).
% 144.13/18.77 fof(f412,plain,(
% 144.13/18.77 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ9_spl|sQ11_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f275,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f409])).
% 144.13/18.77 fof(f413,definition,(
% 144.13/18.77 sQ12_spl <=> (a_select2(s_values7_init,sK24_skl)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f416,plain,(
% 144.13/18.77 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ9_spl|~sQ12_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f276,f375,f378,f381,f384,f387,f390,f393,f396,f399,f402,f413])).
% 144.13/18.77 fof(f428,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|~leq(pv1376,n3)|a_select3(simplex7_init,pv1376,X0)=init)),
% 144.13/18.77 inference(resolution,[status(thm)],[f272,f267])).
% 144.13/18.77 fof(f432,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|~leq(n0,n3)|a_select3(simplex7_init,n0,X0)=init)),
% 144.13/18.77 inference(resolution,[status(thm)],[f272,f107])).
% 144.13/18.77 fof(f433,definition,(
% 144.13/18.77 ![X0]: (sQ13_spl <=> (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,pv1376,X0)=init))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f434,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,pv1376,X0)=init|~sQ13_spl)),
% 144.13/18.77 inference(component_clause,[status(thm)],[f433])).
% 144.13/18.77 fof(f436,plain,(
% 144.13/18.77 sQ13_spl|~sQ8_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f428,f433,f399])).
% 144.13/18.77 fof(f458,definition,(
% 144.13/18.77 ![X0]: (sQ20_spl <=> (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n0,X0)=init))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f459,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n0,X0)=init|~sQ20_spl)),
% 144.13/18.77 inference(component_clause,[status(thm)],[f458])).
% 144.13/18.77 fof(f461,definition,(
% 144.13/18.77 sQ21_spl <=> (leq(n0,n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f463,plain,(
% 144.13/18.77 ~leq(n0,n3)|sQ21_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f461])).
% 144.13/18.77 fof(f464,plain,(
% 144.13/18.77 sQ20_spl|~sQ21_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f432,f458,f461])).
% 144.13/18.77 fof(f465,plain,(
% 144.13/18.77 $false|sQ8_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f401,f271])).
% 144.13/18.77 fof(f466,plain,(
% 144.13/18.77 sQ8_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f465])).
% 144.13/18.77 fof(f594,plain,(
% 144.13/18.77 leq(n330,n410)),
% 144.13/18.77 inference(resolution,[status(thm)],[f120,f282])).
% 144.13/18.77 fof(f595,plain,(
% 144.13/18.77 leq(n0,n330)),
% 144.13/18.77 inference(resolution,[status(thm)],[f120,f293])).
% 144.13/18.77 fof(f626,plain,(
% 144.13/18.77 n330=n410|gt(n410,n330)),
% 144.13/18.77 inference(resolution,[status(thm)],[f122,f594])).
% 144.13/18.77 fof(f631,plain,(
% 144.13/18.77 n0=n330|gt(n330,n0)),
% 144.13/18.77 inference(resolution,[status(thm)],[f122,f595])).
% 144.13/18.77 fof(f639,definition,(
% 144.13/18.77 sQ30_spl <=> (n330=n410)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f640,plain,(
% 144.13/18.77 n330=n410|~sQ30_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f639])).
% 144.13/18.77 fof(f642,definition,(
% 144.13/18.77 sQ31_spl <=> (gt(n410,n330))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f645,plain,(
% 144.13/18.77 sQ30_spl|sQ31_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f626,f639,f642])).
% 144.13/18.77 fof(f674,definition,(
% 144.13/18.77 sQ40_spl <=> (n0=n330)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f675,plain,(
% 144.13/18.77 n0=n330|~sQ40_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f674])).
% 144.13/18.77 fof(f677,definition,(
% 144.13/18.77 sQ41_spl <=> (gt(n330,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f680,plain,(
% 144.13/18.77 sQ40_spl|sQ41_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f631,f674,f677])).
% 144.13/18.77 fof(f723,plain,(
% 144.13/18.77 $false|sQ7_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f398,f270])).
% 144.13/18.77 fof(f724,plain,(
% 144.13/18.77 sQ7_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f723])).
% 144.13/18.77 fof(f725,plain,(
% 144.13/18.77 $false|sQ4_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f389,f267])).
% 144.13/18.77 fof(f726,plain,(
% 144.13/18.77 sQ4_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f725])).
% 144.13/18.77 fof(f727,plain,(
% 144.13/18.77 $false|sQ3_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f386,f266])).
% 144.13/18.77 fof(f728,plain,(
% 144.13/18.77 sQ3_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f727])).
% 144.13/18.77 fof(f729,plain,(
% 144.13/18.77 $false|sQ2_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f383,f265])).
% 144.13/18.77 fof(f730,plain,(
% 144.13/18.77 sQ2_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f729])).
% 144.13/18.77 fof(f731,plain,(
% 144.13/18.77 $false|sQ1_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f380,f264])).
% 144.13/18.77 fof(f732,plain,(
% 144.13/18.77 sQ1_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f731])).
% 144.13/18.77 fof(f733,plain,(
% 144.13/18.77 $false|sQ0_spl),
% 144.13/18.77 inference(trivial_equality_resolution,[status(thm)],[f377])).
% 144.13/18.77 fof(f734,plain,(
% 144.13/18.77 sQ0_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f733])).
% 144.13/18.77 fof(f736,plain,(
% 144.13/18.77 leq(n330,pred(n410))),
% 144.13/18.77 inference(resolution,[status(thm)],[f126,f282])).
% 144.13/18.77 fof(f744,plain,(
% 144.13/18.77 ![X0]: (leq(X0,pred(succ(X0))))),
% 144.13/18.77 inference(resolution,[status(thm)],[f127,f126])).
% 144.13/18.77 fof(f771,definition,(
% 144.13/18.77 ![X0]: (sQ54_spl <=> (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n1,X0)=init))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f772,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n1,X0)=init|~sQ54_spl)),
% 144.13/18.77 inference(component_clause,[status(thm)],[f771])).
% 144.13/18.77 fof(f774,definition,(
% 144.13/18.77 sQ55_spl <=> (leq(n1,n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f776,plain,(
% 144.13/18.77 ~leq(n1,n3)|sQ55_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f774])).
% 144.13/18.77 fof(f778,definition,(
% 144.13/18.77 sQ56_spl <=> (n0=n1)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f779,plain,(
% 144.13/18.77 n0=n1|~sQ56_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f778])).
% 144.13/18.77 fof(f781,definition,(
% 144.13/18.77 sQ57_spl <=> (gt(n1,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f815,plain,(
% 144.13/18.77 $false|sQ6_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f395,f269])).
% 144.13/18.77 fof(f816,plain,(
% 144.13/18.77 sQ6_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f815])).
% 144.13/18.77 fof(f817,plain,(
% 144.13/18.77 $false|sQ5_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f392,f268])).
% 144.13/18.77 fof(f818,plain,(
% 144.13/18.77 sQ5_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f817])).
% 144.13/18.77 fof(f820,plain,(
% 144.13/18.77 leq(n0,n410)),
% 144.13/18.77 inference(resolution,[status(thm)],[f294,f120])).
% 144.13/18.77 fof(f824,plain,(
% 144.13/18.77 leq(n0,n1)),
% 144.13/18.77 inference(resolution,[status(thm)],[f295,f120])).
% 144.13/18.77 fof(f828,plain,(
% 144.13/18.77 leq(n0,n2)),
% 144.13/18.77 inference(resolution,[status(thm)],[f296,f120])).
% 144.13/18.77 fof(f841,plain,(
% 144.13/18.77 ![X0,X1]: (~leq(X0,X1)|leq(X0,pred(succ(X1))))),
% 144.13/18.77 inference(resolution,[status(thm)],[f744,f110])).
% 144.13/18.77 fof(f850,plain,(
% 144.13/18.77 n0=n410|gt(n410,n0)),
% 144.13/18.77 inference(resolution,[status(thm)],[f820,f122])).
% 144.13/18.77 fof(f866,definition,(
% 144.13/18.77 sQ62_spl <=> (n0=n410)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f867,plain,(
% 144.13/18.77 n0=n410|~sQ62_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f866])).
% 144.13/18.77 fof(f869,definition,(
% 144.13/18.77 sQ63_spl <=> (gt(n410,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f872,plain,(
% 144.13/18.77 sQ62_spl|sQ63_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f850,f866,f869])).
% 144.13/18.77 fof(f873,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|~leq(n1,n3)|a_select3(simplex7_init,n1,X0)=init)),
% 144.13/18.77 inference(resolution,[status(thm)],[f824,f272])).
% 144.13/18.77 fof(f874,plain,(
% 144.13/18.77 n0=n1|gt(n1,n0)),
% 144.13/18.77 inference(resolution,[status(thm)],[f824,f122])).
% 144.13/18.77 fof(f883,plain,(
% 144.13/18.77 sQ54_spl|~sQ55_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f873,f771,f774])).
% 144.13/18.77 fof(f884,plain,(
% 144.13/18.77 sQ56_spl|sQ57_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f874,f778,f781])).
% 144.13/18.77 fof(f885,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|~leq(n2,n3)|a_select3(simplex7_init,n2,X0)=init)),
% 144.13/18.77 inference(resolution,[status(thm)],[f828,f272])).
% 144.13/18.77 fof(f886,plain,(
% 144.13/18.77 n0=n2|gt(n2,n0)),
% 144.13/18.77 inference(resolution,[status(thm)],[f828,f122])).
% 144.13/18.77 fof(f895,definition,(
% 144.13/18.77 ![X0]: (sQ64_spl <=> (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n2,X0)=init))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f896,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n2,X0)=init|~sQ64_spl)),
% 144.13/18.77 inference(component_clause,[status(thm)],[f895])).
% 144.13/18.77 fof(f898,definition,(
% 144.13/18.77 sQ65_spl <=> (leq(n2,n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f900,plain,(
% 144.13/18.77 ~leq(n2,n3)|sQ65_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f898])).
% 144.13/18.77 fof(f901,plain,(
% 144.13/18.77 sQ64_spl|~sQ65_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f885,f895,f898])).
% 144.13/18.77 fof(f902,definition,(
% 144.13/18.77 sQ66_spl <=> (n0=n2)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f903,plain,(
% 144.13/18.77 n0=n2|~sQ66_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f902])).
% 144.13/18.77 fof(f905,definition,(
% 144.13/18.77 sQ67_spl <=> (gt(n2,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f908,plain,(
% 144.13/18.77 sQ66_spl|sQ67_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f886,f902,f905])).
% 144.13/18.77 fof(f1133,plain,(
% 144.13/18.77 leq(sK29_skl(sK23_skl),n3)|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f403,f364])).
% 144.13/18.77 fof(f1134,plain,(
% 144.13/18.77 leq(n0,sK29_skl(sK23_skl))|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f403,f363])).
% 144.13/18.77 fof(f1135,plain,(
% 144.13/18.77 leq(sK23_skl,n2)|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f403,f362])).
% 144.13/18.77 fof(f1136,plain,(
% 144.13/18.77 leq(n0,sK23_skl)|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f403,f361])).
% 144.13/18.77 fof(f1148,definition,(
% 144.13/18.77 sQ72_spl <=> (leq(n0,n410))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1150,plain,(
% 144.13/18.77 ~leq(n0,n410)|sQ72_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1148])).
% 144.13/18.77 fof(f1152,plain,(
% 144.13/18.77 $false|sQ72_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f1150,f820])).
% 144.13/18.77 fof(f1153,plain,(
% 144.13/18.77 sQ72_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f1152])).
% 144.13/18.77 fof(f1162,plain,(
% 144.13/18.77 sK23_skl=n2|gt(n2,sK23_skl)|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1135,f122])).
% 144.13/18.77 fof(f1171,definition,(
% 144.13/18.77 sQ73_spl <=> (sK23_skl=n2)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1172,plain,(
% 144.13/18.77 sK23_skl=n2|~sQ73_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1171])).
% 144.13/18.77 fof(f1174,definition,(
% 144.13/18.77 sQ74_spl <=> (gt(n2,sK23_skl))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1177,plain,(
% 144.13/18.77 sQ73_spl|sQ74_spl|~sQ9_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1162,f1171,f1174,f402])).
% 144.13/18.77 fof(f1193,plain,(
% 144.13/18.77 n0=sK23_skl|gt(sK23_skl,n0)|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1136,f122])).
% 144.13/18.77 fof(f1209,definition,(
% 144.13/18.77 sQ77_spl <=> (n0=sK23_skl)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1210,plain,(
% 144.13/18.77 n0=sK23_skl|~sQ77_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1209])).
% 144.13/18.77 fof(f1212,definition,(
% 144.13/18.77 sQ78_spl <=> (gt(sK23_skl,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1215,plain,(
% 144.13/18.77 sQ77_spl|sQ78_spl|~sQ9_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1193,f1209,f1212,f402])).
% 144.13/18.77 fof(f1279,plain,(
% 144.13/18.77 leq(n0,n3)),
% 144.13/18.77 inference(resolution,[status(thm)],[f297,f120])).
% 144.13/18.77 fof(f1283,plain,(
% 144.13/18.77 leq(n1,n330)),
% 144.13/18.77 inference(resolution,[status(thm)],[f300,f120])).
% 144.13/18.77 fof(f1324,plain,(
% 144.13/18.77 ~leq(n0,sK24_skl)|a_select2(s_values7_init,sK24_skl)=init|~sQ11_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f410,f273])).
% 144.13/18.77 fof(f1342,plain,(
% 144.13/18.77 ~sQ10_spl|sQ12_spl|~sQ11_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1324,f405,f413,f409])).
% 144.13/18.77 fof(f1350,plain,(
% 144.13/18.77 sP3_prd(n2)|~sQ73_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1172,f403])).
% 144.13/18.77 fof(f1351,plain,(
% 144.13/18.77 leq(sK29_skl(n2),n3)|~sQ73_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1172,f1133])).
% 144.13/18.77 fof(f1352,plain,(
% 144.13/18.77 leq(n0,sK29_skl(n2))|~sQ73_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1172,f1134])).
% 144.13/18.77 fof(f1426,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|~leq(n3,n3)|a_select3(simplex7_init,n3,X0)=init)),
% 144.13/18.77 inference(resolution,[status(thm)],[f1279,f272])).
% 144.13/18.77 fof(f1435,plain,(
% 144.13/18.77 n0=n3|gt(n3,n0)),
% 144.13/18.77 inference(resolution,[status(thm)],[f1279,f122])).
% 144.13/18.77 fof(f1444,definition,(
% 144.13/18.77 ![X0]: (sQ85_spl <=> (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n3,X0)=init))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1445,plain,(
% 144.13/18.77 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|a_select3(simplex7_init,n3,X0)=init|~sQ85_spl)),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1444])).
% 144.13/18.77 fof(f1447,definition,(
% 144.13/18.77 sQ86_spl <=> (leq(n3,n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1449,plain,(
% 144.13/18.77 ~leq(n3,n3)|sQ86_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1447])).
% 144.13/18.77 fof(f1450,plain,(
% 144.13/18.77 sQ85_spl|~sQ86_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1426,f1444,f1447])).
% 144.13/18.77 fof(f1451,definition,(
% 144.13/18.77 sQ87_spl <=> (n0=n3)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1452,plain,(
% 144.13/18.77 n0=n3|~sQ87_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1451])).
% 144.13/18.77 fof(f1454,definition,(
% 144.13/18.77 sQ88_spl <=> (gt(n3,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1457,plain,(
% 144.13/18.77 sQ87_spl|sQ88_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1435,f1451,f1454])).
% 144.13/18.77 fof(f1466,plain,(
% 144.13/18.77 n1=n330|gt(n330,n1)),
% 144.13/18.77 inference(resolution,[status(thm)],[f1283,f122])).
% 144.13/18.77 fof(f1475,definition,(
% 144.13/18.77 sQ89_spl <=> (n1=n330)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1476,plain,(
% 144.13/18.77 n1=n330|~sQ89_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1475])).
% 144.13/18.77 fof(f1478,definition,(
% 144.13/18.77 sQ90_spl <=> (gt(n330,n1))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1481,plain,(
% 144.13/18.77 sQ89_spl|sQ90_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1466,f1475,f1478])).
% 144.13/18.77 fof(f1510,plain,(
% 144.13/18.77 sK29_skl(n2)=n3|gt(n3,sK29_skl(n2))|~sQ73_spl|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1351,f122])).
% 144.13/18.77 fof(f1519,definition,(
% 144.13/18.77 sQ91_spl <=> (sK29_skl(n2)=n3)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1520,plain,(
% 144.13/18.77 sK29_skl(n2)=n3|~sQ91_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1519])).
% 144.13/18.77 fof(f1522,definition,(
% 144.13/18.77 sQ92_spl <=> (gt(n3,sK29_skl(n2)))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1523,plain,(
% 144.13/18.77 gt(n3,sK29_skl(n2))|~sQ92_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1522])).
% 144.13/18.77 fof(f1525,plain,(
% 144.13/18.77 sQ91_spl|sQ92_spl|~sQ73_spl|~sQ9_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1510,f1519,f1522,f1171,f402])).
% 144.13/18.77 fof(f1597,plain,(
% 144.13/18.77 leq(n0,sK29_skl(n0))|~sQ77_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1210,f1134])).
% 144.13/18.77 fof(f1598,plain,(
% 144.13/18.77 leq(sK29_skl(n0),n3)|~sQ77_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1210,f1133])).
% 144.13/18.77 fof(f1599,plain,(
% 144.13/18.77 sP3_prd(n0)|~sQ77_spl|~sQ9_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f1210,f403])).
% 144.13/18.77 fof(f1675,definition,(
% 144.13/18.77 sQ94_spl <=> (leq(sK29_skl(n0),n3))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1677,plain,(
% 144.13/18.77 ~leq(sK29_skl(n0),n3)|sQ94_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1675])).
% 144.13/18.77 fof(f1679,definition,(
% 144.13/18.77 sQ95_spl <=> (n0=sK29_skl(n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1680,plain,(
% 144.13/18.77 n0=sK29_skl(n0)|~sQ95_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1679])).
% 144.13/18.77 fof(f1686,plain,(
% 144.13/18.77 $false|sQ86_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f1449,f107])).
% 144.13/18.77 fof(f1687,plain,(
% 144.13/18.77 sQ86_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f1686])).
% 144.13/18.77 fof(f1710,definition,(
% 144.13/18.77 sQ97_spl <=> (sK29_skl(n0)=n3)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1711,plain,(
% 144.13/18.77 sK29_skl(n0)=n3|~sQ97_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1710])).
% 144.13/18.77 fof(f1719,plain,(
% 144.13/18.77 ~sP3_prd(n0)|~a_select3(simplex7_init,n0,n0)=init|~sQ95_spl),
% 144.13/18.77 inference(paramodulation,[status(thm)],[f1680,f365])).
% 144.13/18.77 fof(f1720,definition,(
% 144.13/18.77 sQ99_spl <=> (sP3_prd(n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1722,plain,(
% 144.13/18.77 ~sP3_prd(n0)|sQ99_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1720])).
% 144.13/18.77 fof(f1723,definition,(
% 144.13/18.77 sQ100_spl <=> (a_select3(simplex7_init,n0,n0)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1726,plain,(
% 144.13/18.77 ~sQ99_spl|~sQ100_spl|~sQ95_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1719,f1720,f1723,f1679])).
% 144.13/18.77 fof(f1727,plain,(
% 144.13/18.77 ~sP3_prd(n2)|~a_select3(simplex7_init,n3,n2)=init|~sQ91_spl),
% 144.13/18.77 inference(paramodulation,[status(thm)],[f1520,f365])).
% 144.13/18.77 fof(f1728,definition,(
% 144.13/18.77 sQ101_spl <=> (sP3_prd(n2))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1730,plain,(
% 144.13/18.77 ~sP3_prd(n2)|sQ101_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1728])).
% 144.13/18.77 fof(f1731,definition,(
% 144.13/18.77 sQ102_spl <=> (a_select3(simplex7_init,n3,n2)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1734,plain,(
% 144.13/18.77 ~sQ101_spl|~sQ102_spl|~sQ91_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1727,f1728,f1731,f1519])).
% 144.13/18.77 fof(f1739,plain,(
% 144.13/18.77 ~sP3_prd(n0)|~a_select3(simplex7_init,n3,n0)=init|~sQ97_spl),
% 144.13/18.77 inference(paramodulation,[status(thm)],[f1711,f365])).
% 144.13/18.77 fof(f1740,definition,(
% 144.13/18.77 sQ103_spl <=> (a_select3(simplex7_init,n3,n0)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1743,plain,(
% 144.13/18.77 ~sQ99_spl|~sQ103_spl|~sQ97_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1739,f1720,f1740,f1710])).
% 144.13/18.77 fof(f1751,plain,(
% 144.13/18.77 leq(sK29_skl(n0),pred(succ(n3)))|~sQ77_spl|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1598,f841])).
% 144.13/18.77 fof(f1779,plain,(
% 144.13/18.77 leq(n0,pred(succ(sK29_skl(n0))))|~sQ77_spl|~sQ9_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1597,f841])).
% 144.13/18.77 fof(f1792,plain,(
% 144.13/18.77 leq(n1,n410)),
% 144.13/18.77 inference(resolution,[status(thm)],[f301,f120])).
% 144.13/18.77 fof(f1803,plain,(
% 144.13/18.77 n1=n410|gt(n410,n1)),
% 144.13/18.77 inference(resolution,[status(thm)],[f1792,f122])).
% 144.13/18.77 fof(f1812,definition,(
% 144.13/18.77 sQ104_spl <=> (n1=n410)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1813,plain,(
% 144.13/18.77 n1=n410|~sQ104_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f1812])).
% 144.13/18.77 fof(f1815,definition,(
% 144.13/18.77 sQ105_spl <=> (gt(n410,n1))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f1818,plain,(
% 144.13/18.77 sQ104_spl|sQ105_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f1803,f1812,f1815])).
% 144.13/18.77 fof(f1820,plain,(
% 144.13/18.77 leq(n1,n2)),
% 144.13/18.77 inference(resolution,[status(thm)],[f302,f120])).
% 144.13/18.77 fof(f1824,plain,(
% 144.13/18.77 leq(n1,n3)),
% 144.13/18.77 inference(resolution,[status(thm)],[f303,f120])).
% 144.13/18.77 fof(f2291,plain,(
% 144.13/18.77 leq(n2,n330)),
% 144.13/18.77 inference(resolution,[status(thm)],[f306,f120])).
% 144.13/18.77 fof(f2319,plain,(
% 144.13/18.77 leq(n2,n410)),
% 144.13/18.77 inference(resolution,[status(thm)],[f307,f120])).
% 144.13/18.77 fof(f2347,plain,(
% 144.13/18.77 leq(n2,n3)),
% 144.13/18.77 inference(resolution,[status(thm)],[f308,f120])).
% 144.13/18.77 fof(f2375,plain,(
% 144.13/18.77 leq(n3,n330)),
% 144.13/18.77 inference(resolution,[status(thm)],[f311,f120])).
% 144.13/18.77 fof(f2403,plain,(
% 144.13/18.77 leq(n3,n410)),
% 144.13/18.77 inference(resolution,[status(thm)],[f312,f120])).
% 144.13/18.77 fof(f2407,plain,(
% 144.13/18.77 ~leq(n3,n0)|n3=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f1279])).
% 144.13/18.77 fof(f2409,plain,(
% 144.13/18.77 ~leq(n2,n0)|n2=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f828])).
% 144.13/18.77 fof(f2410,plain,(
% 144.13/18.77 ~leq(n1,n0)|n1=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f824])).
% 144.13/18.77 fof(f2411,plain,(
% 144.13/18.77 ~leq(n410,n0)|n410=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f820])).
% 144.13/18.77 fof(f2412,plain,(
% 144.13/18.77 ~leq(n330,n0)|n330=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f595])).
% 144.13/18.77 fof(f2420,plain,(
% 144.13/18.77 ~leq(n0,n0)|n0=n0),
% 144.13/18.77 inference(resolution,[status(thm)],[f318,f107])).
% 144.13/18.77 fof(f2425,definition,(
% 144.13/18.77 sQ119_spl <=> (leq(n3,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2428,plain,(
% 144.13/18.77 ~sQ119_spl|sQ87_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2407,f2425,f1451])).
% 144.13/18.77 fof(f2433,definition,(
% 144.13/18.77 sQ121_spl <=> (leq(n2,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2436,plain,(
% 144.13/18.77 ~sQ121_spl|sQ66_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2409,f2433,f902])).
% 144.13/18.77 fof(f2437,definition,(
% 144.13/18.77 sQ122_spl <=> (leq(n1,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2440,plain,(
% 144.13/18.77 ~sQ122_spl|sQ56_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2410,f2437,f778])).
% 144.13/18.77 fof(f2441,definition,(
% 144.13/18.77 sQ123_spl <=> (leq(n410,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2444,plain,(
% 144.13/18.77 ~sQ123_spl|sQ62_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2411,f2441,f866])).
% 144.13/18.77 fof(f2445,definition,(
% 144.13/18.77 sQ124_spl <=> (leq(n330,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2448,plain,(
% 144.13/18.77 ~sQ124_spl|sQ40_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2412,f2445,f674])).
% 144.13/18.77 fof(f2486,definition,(
% 144.13/18.77 sQ135_spl <=> (leq(n0,n0))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2488,plain,(
% 144.13/18.77 ~leq(n0,n0)|sQ135_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f2486])).
% 144.13/18.77 fof(f2489,definition,(
% 144.13/18.77 sQ136_spl <=> (n0=n0)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2492,plain,(
% 144.13/18.77 ~sQ135_spl|sQ136_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2420,f2486,f2489])).
% 144.13/18.77 fof(f2493,plain,(
% 144.13/18.77 $false|sQ135_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f2488,f107])).
% 144.13/18.77 fof(f2494,plain,(
% 144.13/18.77 sQ135_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f2493])).
% 144.13/18.77 fof(f2806,definition,(
% 144.13/18.77 sQ145_spl <=> (leq(n0,n330))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2808,plain,(
% 144.13/18.77 ~leq(n0,n330)|sQ145_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f2806])).
% 144.13/18.77 fof(f2810,plain,(
% 144.13/18.77 $false|sQ145_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f2808,f595])).
% 144.13/18.77 fof(f2811,plain,(
% 144.13/18.77 sQ145_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f2810])).
% 144.13/18.77 fof(f2929,plain,(
% 144.13/18.77 ~leq(n1,n1)|n1=n0|n1=n1),
% 144.13/18.77 inference(resolution,[status(thm)],[f320,f824])).
% 144.13/18.77 fof(f2930,plain,(
% 144.13/18.77 ~leq(n410,n1)|n410=n0|n410=n1),
% 144.13/18.77 inference(resolution,[status(thm)],[f320,f820])).
% 144.13/18.77 fof(f2931,plain,(
% 144.13/18.77 ~leq(n330,n1)|n330=n0|n330=n1),
% 144.13/18.77 inference(resolution,[status(thm)],[f320,f595])).
% 144.13/18.77 fof(f2962,definition,(
% 144.13/18.77 sQ153_spl <=> (leq(n1,n1))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2964,plain,(
% 144.13/18.77 ~leq(n1,n1)|sQ153_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f2962])).
% 144.13/18.77 fof(f2965,definition,(
% 144.13/18.77 sQ154_spl <=> (n1=n1)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2968,plain,(
% 144.13/18.77 ~sQ153_spl|sQ56_spl|sQ154_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2929,f2962,f778,f2965])).
% 144.13/18.77 fof(f2969,definition,(
% 144.13/18.77 sQ155_spl <=> (leq(n410,n1))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2972,plain,(
% 144.13/18.77 ~sQ155_spl|sQ62_spl|sQ104_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2930,f2969,f866,f1812])).
% 144.13/18.77 fof(f2973,definition,(
% 144.13/18.77 sQ156_spl <=> (leq(n330,n1))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f2976,plain,(
% 144.13/18.77 ~sQ156_spl|sQ40_spl|sQ89_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f2931,f2973,f674,f1475])).
% 144.13/18.77 fof(f3027,plain,(
% 144.13/18.77 $false|sQ153_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f2964,f107])).
% 144.13/18.77 fof(f3028,plain,(
% 144.13/18.77 sQ153_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3027])).
% 144.13/18.77 fof(f3062,definition,(
% 144.13/18.77 sQ176_spl <=> (leq(n2,n2))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3064,plain,(
% 144.13/18.77 ~leq(n2,n2)|sQ176_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3062])).
% 144.13/18.77 fof(f3069,definition,(
% 144.13/18.77 sQ178_spl <=> (leq(n1,n2))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3071,plain,(
% 144.13/18.77 ~leq(n1,n2)|sQ178_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3069])).
% 144.13/18.77 fof(f3130,definition,(
% 144.13/18.77 sQ195_spl <=> (leq(n0,n2))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3132,plain,(
% 144.13/18.77 ~leq(n0,n2)|sQ195_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3130])).
% 144.13/18.77 fof(f3134,plain,(
% 144.13/18.77 $false|sQ195_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3132,f828])).
% 144.13/18.77 fof(f3135,plain,(
% 144.13/18.77 sQ195_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3134])).
% 144.13/18.77 fof(f3136,plain,(
% 144.13/18.77 $false|sQ178_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3071,f1820])).
% 144.13/18.77 fof(f3137,plain,(
% 144.13/18.77 sQ178_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3136])).
% 144.13/18.77 fof(f3138,plain,(
% 144.13/18.77 $false|sQ176_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3064,f107])).
% 144.13/18.77 fof(f3139,plain,(
% 144.13/18.77 sQ176_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3138])).
% 144.13/18.77 fof(f3197,plain,(
% 144.13/18.77 $false|sQ65_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f900,f2347])).
% 144.13/18.77 fof(f3198,plain,(
% 144.13/18.77 sQ65_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3197])).
% 144.13/18.77 fof(f3199,plain,(
% 144.13/18.77 $false|sQ21_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f463,f1279])).
% 144.13/18.77 fof(f3200,plain,(
% 144.13/18.77 sQ21_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3199])).
% 144.13/18.77 fof(f3220,definition,(
% 144.13/18.77 sQ205_spl <=> (leq(n1,n410))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3222,plain,(
% 144.13/18.77 ~leq(n1,n410)|sQ205_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3220])).
% 144.13/18.77 fof(f3224,plain,(
% 144.13/18.77 $false|sQ205_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3222,f1792])).
% 144.13/18.77 fof(f3225,plain,(
% 144.13/18.77 sQ205_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3224])).
% 144.13/18.77 fof(f3233,definition,(
% 144.13/18.77 sQ206_spl <=> (leq(n1,n330))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3235,plain,(
% 144.13/18.77 ~leq(n1,n330)|sQ206_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3233])).
% 144.13/18.77 fof(f3237,plain,(
% 144.13/18.77 $false|sQ206_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3235,f1283])).
% 144.13/18.77 fof(f3238,plain,(
% 144.13/18.77 sQ206_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3237])).
% 144.13/18.77 fof(f3240,definition,(
% 144.13/18.77 sQ207_spl <=> (leq(n2,n410))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3242,plain,(
% 144.13/18.77 ~leq(n2,n410)|sQ207_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3240])).
% 144.13/18.77 fof(f3244,plain,(
% 144.13/18.77 $false|sQ207_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3242,f2319])).
% 144.13/18.77 fof(f3245,plain,(
% 144.13/18.77 sQ207_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3244])).
% 144.13/18.77 fof(f3247,definition,(
% 144.13/18.77 sQ208_spl <=> (leq(n2,n330))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3249,plain,(
% 144.13/18.77 ~leq(n2,n330)|sQ208_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3247])).
% 144.13/18.77 fof(f3251,plain,(
% 144.13/18.77 $false|sQ208_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3249,f2291])).
% 144.13/18.77 fof(f3252,plain,(
% 144.13/18.77 sQ208_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3251])).
% 144.13/18.77 fof(f3254,definition,(
% 144.13/18.77 sQ209_spl <=> (leq(n3,n410))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3256,plain,(
% 144.13/18.77 ~leq(n3,n410)|sQ209_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3254])).
% 144.13/18.77 fof(f3258,plain,(
% 144.13/18.77 $false|sQ209_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3256,f2403])).
% 144.13/18.77 fof(f3259,plain,(
% 144.13/18.77 sQ209_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3258])).
% 144.13/18.77 fof(f3261,definition,(
% 144.13/18.77 sQ210_spl <=> (leq(n3,n330))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f3263,plain,(
% 144.13/18.77 ~leq(n3,n330)|sQ210_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f3261])).
% 144.13/18.77 fof(f3265,plain,(
% 144.13/18.77 $false|sQ210_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f3263,f2375])).
% 144.13/18.77 fof(f3266,plain,(
% 144.13/18.77 sQ210_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f3265])).
% 144.13/18.77 fof(f3985,plain,(
% 144.13/18.77 ~leq(n2,n2)|a_select3(simplex7_init,n0,n2)=init|~sQ20_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f459,f828])).
% 144.13/18.77 fof(f3986,plain,(
% 144.13/18.77 ~leq(n1,n2)|a_select3(simplex7_init,n0,n1)=init|~sQ20_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f459,f824])).
% 144.13/18.77 fof(f3996,plain,(
% 144.13/18.77 ~leq(n0,n2)|a_select3(simplex7_init,n0,n0)=init|~sQ20_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f459,f107])).
% 144.13/18.77 fof(f4009,definition,(
% 144.13/18.77 sQ224_spl <=> (a_select3(simplex7_init,n0,n2)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f4012,plain,(
% 144.13/18.77 ~sQ176_spl|sQ224_spl|~sQ20_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f3985,f3062,f4009,f458])).
% 144.13/18.77 fof(f4013,definition,(
% 144.13/18.77 sQ225_spl <=> (a_select3(simplex7_init,n0,n1)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f4016,plain,(
% 144.13/18.77 ~sQ178_spl|sQ225_spl|~sQ20_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f3986,f3069,f4013,f458])).
% 144.13/18.77 fof(f4053,plain,(
% 144.13/18.77 ~sQ195_spl|sQ100_spl|~sQ20_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f3996,f3130,f1723,f458])).
% 144.13/18.77 fof(f4298,plain,(
% 144.13/18.77 ~leq(n2,n2)|a_select3(simplex7_init,pv1376,n2)=init|~sQ13_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f434,f828])).
% 144.13/18.77 fof(f4299,plain,(
% 144.13/18.77 ~leq(n1,n2)|a_select3(simplex7_init,pv1376,n1)=init|~sQ13_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f434,f824])).
% 144.13/18.77 fof(f4309,plain,(
% 144.13/18.77 ~leq(n0,n2)|a_select3(simplex7_init,pv1376,n0)=init|~sQ13_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f434,f107])).
% 144.13/18.77 fof(f4322,definition,(
% 144.13/18.77 sQ283_spl <=> (a_select3(simplex7_init,pv1376,n2)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f4325,plain,(
% 144.13/18.77 ~sQ176_spl|sQ283_spl|~sQ13_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f4298,f3062,f4322,f433])).
% 144.13/18.77 fof(f4326,definition,(
% 144.13/18.77 sQ284_spl <=> (a_select3(simplex7_init,pv1376,n1)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f4329,plain,(
% 144.13/18.77 ~sQ178_spl|sQ284_spl|~sQ13_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f4299,f3069,f4326,f433])).
% 144.13/18.77 fof(f4366,definition,(
% 144.13/18.77 sQ294_spl <=> (a_select3(simplex7_init,pv1376,n0)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f4369,plain,(
% 144.13/18.77 ~sQ195_spl|sQ294_spl|~sQ13_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f4309,f3130,f4366,f433])).
% 144.13/18.77 fof(f4579,plain,(
% 144.13/18.77 ![X0]: (plus(n4,X0)=plus(n3,succ(X0)))),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f220,f222])).
% 144.13/18.77 fof(f5920,definition,(
% 144.13/18.77 sQ384_spl <=> (a_select3(simplex7_init,n1,n2)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f5924,definition,(
% 144.13/18.77 sQ385_spl <=> (a_select3(simplex7_init,n1,n1)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f5960,definition,(
% 144.13/18.77 sQ394_spl <=> (a_select3(simplex7_init,n1,n0)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f6335,plain,(
% 144.13/18.77 plus(n3,succ(n0))=n4),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f220,f325])).
% 144.13/18.77 fof(f6336,plain,(
% 144.13/18.77 plus(n4,n0)=n4),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f4579,f6335])).
% 144.13/18.77 fof(f6737,definition,(
% 144.13/18.77 sQ481_spl <=> (a_select3(simplex7_init,n2,n2)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f6741,definition,(
% 144.13/18.77 sQ482_spl <=> (a_select3(simplex7_init,n2,n1)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f6777,definition,(
% 144.13/18.77 sQ491_spl <=> (a_select3(simplex7_init,n2,n0)=init)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f7747,definition,(
% 144.13/18.77 sQ568_spl <=> (plus(n4,n0)=n5)),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f7748,plain,(
% 144.13/18.77 plus(n4,n0)=n5|~sQ568_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f7747])).
% 144.13/18.77 fof(f7751,definition,(
% 144.13/18.77 sQ569_spl <=> (leq(plus(n4,n0),n4))),
% 144.13/18.77 introduced(definition,[new_symbols(definition,[sQ569_spl])],[split_symbol_definition])).
% 144.13/18.77 fof(f7753,plain,(
% 144.13/18.77 ~leq(plus(n4,n0),n4)|sQ569_spl),
% 144.13/18.77 inference(component_clause,[status(thm)],[f7751])).
% 144.13/18.77 fof(f8034,plain,(
% 144.13/18.77 ~leq(n4,n4)|sQ569_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f6336,f7753])).
% 144.13/18.77 fof(f8035,plain,(
% 144.13/18.77 $false|sQ569_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f8034,f107])).
% 144.13/18.77 fof(f8036,plain,(
% 144.13/18.77 sQ569_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f8035])).
% 144.13/18.77 fof(f8037,plain,(
% 144.13/18.77 n4=n5|~sQ568_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f6336,f7748])).
% 144.13/18.77 fof(f8048,plain,(
% 144.13/18.77 gt(n4,n4)|~sQ568_spl),
% 144.13/18.77 inference(backward_demodulation,[status(thm)],[f8037,f277])).
% 144.13/18.77 fof(f8056,plain,(
% 144.13/18.77 $false|~sQ568_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f8048,f106])).
% 144.13/18.77 fof(f8057,plain,(
% 144.13/18.77 ~sQ568_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f8056])).
% 144.13/18.77 fof(f8927,plain,(
% 144.13/18.77 gt(n0,n0)|~sQ56_spl),
% 144.13/18.77 inference(backward_demodulation,[status(thm)],[f779,f295])).
% 144.13/18.77 fof(f8933,plain,(
% 144.13/18.77 $false|~sQ56_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f8927,f106])).
% 144.13/18.77 fof(f8934,plain,(
% 144.13/18.77 ~sQ56_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f8933])).
% 144.13/18.77 fof(f9461,plain,(
% 144.13/18.77 ~leq(n1,n2)|a_select3(simplex7_init,n1,n1)=init|~sQ54_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f772,f824])).
% 144.13/18.77 fof(f9468,plain,(
% 144.13/18.77 ~leq(n2,n2)|a_select3(simplex7_init,n1,n2)=init|~sQ54_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f772,f828])).
% 144.13/18.77 fof(f9475,plain,(
% 144.13/18.77 ~leq(n0,n2)|a_select3(simplex7_init,n1,n0)=init|~sQ54_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f772,f107])).
% 144.13/18.77 fof(f9476,plain,(
% 144.13/18.77 ~sQ178_spl|sQ385_spl|~sQ54_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f9461,f3069,f5924,f771])).
% 144.13/18.77 fof(f9495,plain,(
% 144.13/18.77 ~sQ176_spl|sQ384_spl|~sQ54_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f9468,f3062,f5920,f771])).
% 144.13/18.77 fof(f9504,plain,(
% 144.13/18.77 ~sQ195_spl|sQ394_spl|~sQ54_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f9475,f3130,f5960,f771])).
% 144.13/18.77 fof(f9923,plain,(
% 144.13/18.77 gt(n0,n0)|~sQ40_spl),
% 144.13/18.77 inference(backward_demodulation,[status(thm)],[f675,f293])).
% 144.13/18.77 fof(f9929,plain,(
% 144.13/18.77 $false|~sQ40_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f9923,f106])).
% 144.13/18.77 fof(f9930,plain,(
% 144.13/18.77 ~sQ40_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f9929])).
% 144.13/18.77 fof(f10409,plain,(
% 144.13/18.77 leq(n410,pred(n410))|~sQ30_spl),
% 144.13/18.77 inference(forward_demodulation,[status(thm)],[f640,f736])).
% 144.13/18.77 fof(f10410,plain,(
% 144.13/18.77 gt(n410,n410)|~sQ30_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f10409,f125])).
% 144.13/18.77 fof(f10428,plain,(
% 144.13/18.77 $false|~sQ30_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f10410,f106])).
% 144.13/18.77 fof(f10429,plain,(
% 144.13/18.77 ~sQ30_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f10428])).
% 144.13/18.77 fof(f12383,plain,(
% 144.13/18.77 ~leq(n1,n2)|a_select3(simplex7_init,n2,n1)=init|~sQ64_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f896,f824])).
% 144.13/18.77 fof(f12390,plain,(
% 144.13/18.77 ~leq(n2,n2)|a_select3(simplex7_init,n2,n2)=init|~sQ64_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f896,f828])).
% 144.13/18.77 fof(f12397,plain,(
% 144.13/18.77 ~leq(n0,n2)|a_select3(simplex7_init,n2,n0)=init|~sQ64_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f896,f107])).
% 144.13/18.77 fof(f12404,plain,(
% 144.13/18.77 ~sQ178_spl|sQ482_spl|~sQ64_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f12383,f3069,f6741,f895])).
% 144.13/18.77 fof(f12423,plain,(
% 144.13/18.77 ~sQ176_spl|sQ481_spl|~sQ64_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f12390,f3062,f6737,f895])).
% 144.13/18.77 fof(f12431,plain,(
% 144.13/18.77 ~sQ195_spl|sQ491_spl|~sQ64_spl),
% 144.13/18.77 inference(split_clause,[status(thm)],[f12397,f3130,f6777,f895])).
% 144.13/18.77 fof(f13184,plain,(
% 144.13/18.77 gt(n0,n0)|~sQ62_spl),
% 144.13/18.77 inference(backward_demodulation,[status(thm)],[f867,f294])).
% 144.13/18.77 fof(f13192,plain,(
% 144.13/18.77 $false|~sQ62_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f13184,f106])).
% 144.13/18.77 fof(f13193,plain,(
% 144.13/18.77 ~sQ62_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f13192])).
% 144.13/18.77 fof(f13778,plain,(
% 144.13/18.77 gt(n0,n0)|~sQ66_spl),
% 144.13/18.77 inference(backward_demodulation,[status(thm)],[f903,f296])).
% 144.13/18.77 fof(f13788,plain,(
% 144.13/18.77 $false|~sQ66_spl),
% 144.13/18.77 inference(forward_subsumption_resolution,[status(thm)],[f13778,f106])).
% 144.13/18.77 fof(f13789,plain,(
% 144.13/18.77 ~sQ66_spl),
% 144.13/18.77 inference(contradiction_clause,[status(thm)],[f13788])).
% 144.13/18.77 fof(f19595,plain,(
% 144.13/18.77 ~leq(n2,n2)|a_select3(simplex7_init,n3,n2)=init|~sQ85_spl),
% 144.13/18.77 inference(resolution,[status(thm)],[f1445,f828])).
% 144.13/18.78 fof(f19601,plain,(
% 144.13/18.78 ~leq(n1,n2)|a_select3(simplex7_init,n3,n1)=init|~sQ85_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1445,f824])).
% 144.13/18.78 fof(f19613,plain,(
% 144.13/18.78 ~leq(n0,n2)|a_select3(simplex7_init,n3,n0)=init|~sQ85_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1445,f107])).
% 144.13/18.78 fof(f19615,plain,(
% 144.13/18.78 ~sQ176_spl|sQ102_spl|~sQ85_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f19595,f3062,f1731,f1444])).
% 144.13/18.78 fof(f19636,definition,(
% 144.13/18.78 sQ836_spl <=> (a_select3(simplex7_init,n3,n1)=init)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ836_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f19639,plain,(
% 144.13/18.78 ~sQ178_spl|sQ836_spl|~sQ85_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f19601,f3069,f19636,f1444])).
% 144.13/18.78 fof(f19676,plain,(
% 144.13/18.78 ~sQ195_spl|sQ103_spl|~sQ85_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f19613,f3130,f1740,f1444])).
% 144.13/18.78 fof(f19681,plain,(
% 144.13/18.78 $false|sQ55_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f776,f1824])).
% 144.13/18.78 fof(f19682,plain,(
% 144.13/18.78 sQ55_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f19681])).
% 144.13/18.78 fof(f19685,plain,(
% 144.13/18.78 leq(sK29_skl(n2),n3)|~sQ92_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1523,f120])).
% 144.13/18.78 fof(f20675,plain,(
% 144.13/18.78 gt(n0,n0)|~sQ87_spl),
% 144.13/18.78 inference(backward_demodulation,[status(thm)],[f1452,f297])).
% 144.13/18.78 fof(f20712,plain,(
% 144.13/18.78 $false|~sQ87_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f20675,f106])).
% 144.13/18.78 fof(f20713,plain,(
% 144.13/18.78 ~sQ87_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f20712])).
% 144.13/18.78 fof(f21908,plain,(
% 144.13/18.78 gt(n1,n1)|~sQ89_spl),
% 144.13/18.78 inference(backward_demodulation,[status(thm)],[f1476,f300])).
% 144.13/18.78 fof(f21948,plain,(
% 144.13/18.78 $false|~sQ89_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f21908,f106])).
% 144.13/18.78 fof(f21949,plain,(
% 144.13/18.78 ~sQ89_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f21948])).
% 144.13/18.78 fof(f23926,plain,(
% 144.13/18.78 $false|~sQ77_spl|~sQ9_spl|sQ99_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f1722,f1599])).
% 144.13/18.78 fof(f23927,plain,(
% 144.13/18.78 ~sQ77_spl|~sQ9_spl|sQ99_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f23926])).
% 144.13/18.78 fof(f24073,plain,(
% 144.13/18.78 ~leq(sK23_skl,n2)|sK23_skl=n0|sK23_skl=n1|sK23_skl=n2|~sQ9_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1136,f322])).
% 144.13/18.78 fof(f24103,plain,(
% 144.13/18.78 ~leq(sK23_skl,n0)|sK23_skl=n0|~sQ9_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1136,f318])).
% 144.13/18.78 fof(f24196,definition,(
% 144.13/18.78 sQ875_spl <=> (sK23_skl=n1)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ875_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24197,plain,(
% 144.13/18.78 sK23_skl=n1|~sQ875_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24196])).
% 144.13/18.78 fof(f24211,definition,(
% 144.13/18.78 sQ879_spl <=> (leq(sK23_skl,n2))),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ879_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24213,plain,(
% 144.13/18.78 ~leq(sK23_skl,n2)|sQ879_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24211])).
% 144.13/18.78 fof(f24214,plain,(
% 144.13/18.78 ~sQ879_spl|sQ77_spl|sQ875_spl|sQ73_spl|~sQ9_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f24073,f24211,f1209,f24196,f1171,f402])).
% 144.13/18.78 fof(f24219,definition,(
% 144.13/18.78 sQ881_spl <=> (leq(sK23_skl,n0))),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ881_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24222,plain,(
% 144.13/18.78 ~sQ881_spl|sQ77_spl|~sQ9_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f24103,f24219,f1209,f402])).
% 144.13/18.78 fof(f24235,plain,(
% 144.13/18.78 $false|~sQ9_spl|sQ879_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f24213,f1135])).
% 144.13/18.78 fof(f24236,plain,(
% 144.13/18.78 ~sQ9_spl|sQ879_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f24235])).
% 144.13/18.78 fof(f24373,plain,(
% 144.13/18.78 ~leq(sK29_skl(n2),n3)|sK29_skl(n2)=n0|sK29_skl(n2)=n1|sK29_skl(n2)=n2|sK29_skl(n2)=n3|~sQ73_spl|~sQ9_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f1352,f324])).
% 144.13/18.78 fof(f24502,definition,(
% 144.13/18.78 sQ883_spl <=> (leq(sK29_skl(n2),n3))),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ883_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24504,plain,(
% 144.13/18.78 ~leq(sK29_skl(n2),n3)|sQ883_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24502])).
% 144.13/18.78 fof(f24509,definition,(
% 144.13/18.78 sQ885_spl <=> (sK29_skl(n2)=n0)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ885_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24510,plain,(
% 144.13/18.78 sK29_skl(n2)=n0|~sQ885_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24509])).
% 144.13/18.78 fof(f24512,definition,(
% 144.13/18.78 sQ886_spl <=> (sK29_skl(n2)=n1)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ886_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24513,plain,(
% 144.13/18.78 sK29_skl(n2)=n1|~sQ886_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24512])).
% 144.13/18.78 fof(f24515,definition,(
% 144.13/18.78 sQ887_spl <=> (sK29_skl(n2)=n2)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ887_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f24516,plain,(
% 144.13/18.78 sK29_skl(n2)=n2|~sQ887_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f24515])).
% 144.13/18.78 fof(f24525,plain,(
% 144.13/18.78 ~sQ883_spl|sQ885_spl|sQ886_spl|sQ887_spl|sQ91_spl|~sQ73_spl|~sQ9_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f24373,f24502,f24509,f24512,f24515,f1519,f1171,f402])).
% 144.13/18.78 fof(f24557,plain,(
% 144.13/18.78 $false|~sQ92_spl|sQ883_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f24504,f19685])).
% 144.13/18.78 fof(f24558,plain,(
% 144.13/18.78 ~sQ92_spl|sQ883_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f24557])).
% 144.13/18.78 fof(f24821,plain,(
% 144.13/18.78 ~sP3_prd(n2)|~a_select3(simplex7_init,n0,n2)=init|~sQ885_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f24510,f365])).
% 144.13/18.78 fof(f24822,plain,(
% 144.13/18.78 ~sQ101_spl|~sQ224_spl|~sQ885_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f24821,f1728,f4009,f24509])).
% 144.13/18.78 fof(f24889,plain,(
% 144.13/18.78 sK29_skl(n0)=n0|~sQ887_spl|~sQ885_spl),
% 144.13/18.78 inference(backward_demodulation,[status(thm)],[f24891,f24510])).
% 144.13/18.78 fof(f24891,plain,(
% 144.13/18.78 n0=n2|~sQ885_spl|~sQ887_spl),
% 144.13/18.78 inference(forward_demodulation,[status(thm)],[f24510,f24516])).
% 144.13/18.78 fof(f24892,plain,(
% 144.13/18.78 sQ95_spl|~sQ887_spl|~sQ885_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f24889,f1679,f24515,f24509])).
% 144.13/18.78 fof(f26650,plain,(
% 144.13/18.78 ~sP3_prd(n2)|~a_select3(simplex7_init,n1,n2)=init|~sQ886_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f24513,f365])).
% 144.13/18.78 fof(f26651,plain,(
% 144.13/18.78 ~sQ101_spl|~sQ384_spl|~sQ886_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f26650,f1728,f5920,f24512])).
% 144.13/18.78 fof(f26796,plain,(
% 144.13/18.78 $false|~sQ73_spl|~sQ9_spl|sQ101_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f1730,f1350])).
% 144.13/18.78 fof(f26797,plain,(
% 144.13/18.78 ~sQ73_spl|~sQ9_spl|sQ101_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f26796])).
% 144.13/18.78 fof(f26931,plain,(
% 144.13/18.78 ~sP3_prd(n2)|~a_select3(simplex7_init,n2,n2)=init|~sQ887_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f24516,f365])).
% 144.13/18.78 fof(f26932,plain,(
% 144.13/18.78 ~sQ101_spl|~sQ481_spl|~sQ887_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f26931,f1728,f6737,f24515])).
% 144.13/18.78 fof(f26933,plain,(
% 144.13/18.78 leq(sK29_skl(n0),n3)|~sQ77_spl|~sQ9_spl),
% 144.13/18.78 inference(forward_demodulation,[status(thm)],[f226,f1751])).
% 144.13/18.78 fof(f26934,plain,(
% 144.13/18.78 leq(n0,sK29_skl(n0))|~sQ77_spl|~sQ9_spl),
% 144.13/18.78 inference(forward_demodulation,[status(thm)],[f226,f1779])).
% 144.13/18.78 fof(f27230,definition,(
% 144.13/18.78 sQ902_spl <=> (sK29_skl(n0)=n1)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ902_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f27231,plain,(
% 144.13/18.78 sK29_skl(n0)=n1|~sQ902_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f27230])).
% 144.13/18.78 fof(f27233,definition,(
% 144.13/18.78 sQ903_spl <=> (sK29_skl(n0)=n2)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ903_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f27234,plain,(
% 144.13/18.78 sK29_skl(n0)=n2|~sQ903_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f27233])).
% 144.13/18.78 fof(f27423,plain,(
% 144.13/18.78 ~sP3_prd(n0)|~a_select3(simplex7_init,n2,n0)=init|~sQ903_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f27234,f365])).
% 144.13/18.78 fof(f27424,plain,(
% 144.13/18.78 ~sQ99_spl|~sQ491_spl|~sQ903_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f27423,f1720,f6777,f27233])).
% 144.13/18.78 fof(f27425,plain,(
% 144.13/18.78 ~sP3_prd(n0)|~a_select3(simplex7_init,n1,n0)=init|~sQ902_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f27231,f365])).
% 144.13/18.78 fof(f27426,plain,(
% 144.13/18.78 ~sQ99_spl|~sQ394_spl|~sQ902_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f27425,f1720,f5960,f27230])).
% 144.13/18.78 fof(f28210,plain,(
% 144.13/18.78 sP3_prd(n1)|~sQ875_spl|~sQ9_spl),
% 144.13/18.78 inference(forward_demodulation,[status(thm)],[f24197,f403])).
% 144.13/18.78 fof(f28211,plain,(
% 144.13/18.78 leq(sK29_skl(n1),n3)|~sQ875_spl|~sQ9_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f28210,f364])).
% 144.13/18.78 fof(f28213,plain,(
% 144.13/18.78 leq(n0,sK29_skl(n1))|~sQ875_spl|~sQ9_spl),
% 144.13/18.78 inference(resolution,[status(thm)],[f28210,f363])).
% 144.13/18.78 fof(f28264,definition,(
% 144.13/18.78 sQ905_spl <=> (sK29_skl(n1)=n3)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ905_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f28265,plain,(
% 144.13/18.78 sK29_skl(n1)=n3|~sQ905_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f28264])).
% 144.13/18.78 fof(f28396,definition,(
% 144.13/18.78 sQ908_spl <=> (sK29_skl(n1)=n0)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ908_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f28397,plain,(
% 144.13/18.78 sK29_skl(n1)=n0|~sQ908_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f28396])).
% 144.13/18.78 fof(f28399,definition,(
% 144.13/18.78 sQ909_spl <=> (sK29_skl(n1)=n1)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ909_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f28400,plain,(
% 144.13/18.78 sK29_skl(n1)=n1|~sQ909_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f28399])).
% 144.13/18.78 fof(f28402,definition,(
% 144.13/18.78 sQ910_spl <=> (sK29_skl(n1)=n2)),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ910_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f28403,plain,(
% 144.13/18.78 sK29_skl(n1)=n2|~sQ910_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f28402])).
% 144.13/18.78 fof(f28426,plain,(
% 144.13/18.78 ~sP3_prd(n1)|~a_select3(simplex7_init,n3,n1)=init|~sQ905_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f28265,f365])).
% 144.13/18.78 fof(f28427,definition,(
% 144.13/18.78 sQ913_spl <=> (sP3_prd(n1))),
% 144.13/18.78 introduced(definition,[new_symbols(definition,[sQ913_spl])],[split_symbol_definition])).
% 144.13/18.78 fof(f28429,plain,(
% 144.13/18.78 ~sP3_prd(n1)|sQ913_spl),
% 144.13/18.78 inference(component_clause,[status(thm)],[f28427])).
% 144.13/18.78 fof(f28430,plain,(
% 144.13/18.78 ~sQ913_spl|~sQ836_spl|~sQ905_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f28426,f28427,f19636,f28264])).
% 144.13/18.78 fof(f28431,plain,(
% 144.13/18.78 $false|~sQ875_spl|~sQ9_spl|sQ913_spl),
% 144.13/18.78 inference(forward_subsumption_resolution,[status(thm)],[f28429,f28210])).
% 144.13/18.78 fof(f28432,plain,(
% 144.13/18.78 ~sQ875_spl|~sQ9_spl|sQ913_spl),
% 144.13/18.78 inference(contradiction_clause,[status(thm)],[f28431])).
% 144.13/18.78 fof(f28433,plain,(
% 144.13/18.78 ~sP3_prd(n1)|~a_select3(simplex7_init,n0,n1)=init|~sQ908_spl),
% 144.13/18.78 inference(paramodulation,[status(thm)],[f28397,f365])).
% 144.13/18.78 fof(f28434,plain,(
% 144.13/18.78 ~sQ913_spl|~sQ225_spl|~sQ908_spl),
% 144.13/18.78 inference(split_clause,[status(thm)],[f28433,f28427,f4013,f28396])).
% 144.13/18.78 fof(f28435,plain,(
% 144.13/18.78 ~sP3_prd(n1)|~a_select3(simplex7_init,n2,n1)=init|~sQ910_spl),
% 144.13/18.81 inference(paramodulation,[status(thm)],[f28403,f365])).
% 144.13/18.81 fof(f28436,plain,(
% 144.13/18.81 ~sQ913_spl|~sQ482_spl|~sQ910_spl),
% 144.13/18.81 inference(split_clause,[status(thm)],[f28435,f28427,f6741,f28402])).
% 144.13/18.81 fof(f28437,plain,(
% 144.13/18.81 ~sP3_prd(n1)|~a_select3(simplex7_init,n1,n1)=init|~sQ909_spl),
% 144.13/18.81 inference(paramodulation,[status(thm)],[f28400,f365])).
% 144.13/18.81 fof(f28438,plain,(
% 144.13/18.81 ~sQ913_spl|~sQ385_spl|~sQ909_spl),
% 144.13/18.81 inference(split_clause,[status(thm)],[f28437,f28427,f5924,f28399])).
% 144.13/18.81 fof(f29072,definition,(
% 144.13/18.81 sQ918_spl <=> (leq(sK29_skl(n1),n3))),
% 144.13/18.81 introduced(definition,[new_symbols(definition,[sQ918_spl])],[split_symbol_definition])).
% 144.13/18.81 fof(f29074,plain,(
% 144.13/18.81 ~leq(sK29_skl(n1),n3)|sQ918_spl),
% 144.13/18.81 inference(component_clause,[status(thm)],[f29072])).
% 144.13/18.81 fof(f29089,plain,(
% 144.13/18.81 $false|~sQ875_spl|~sQ9_spl|sQ918_spl),
% 144.13/18.81 inference(forward_subsumption_resolution,[status(thm)],[f29074,f28211])).
% 144.13/18.81 fof(f29090,plain,(
% 144.13/18.81 ~sQ875_spl|~sQ9_spl|sQ918_spl),
% 144.13/18.81 inference(contradiction_clause,[status(thm)],[f29089])).
% 144.13/18.81 fof(f29162,plain,(
% 144.13/18.81 gt(n1,n1)|~sQ104_spl),
% 144.13/18.81 inference(backward_demodulation,[status(thm)],[f1813,f301])).
% 144.13/18.81 fof(f29225,plain,(
% 144.13/18.81 $false|~sQ104_spl),
% 144.13/18.81 inference(forward_subsumption_resolution,[status(thm)],[f29162,f106])).
% 144.13/18.81 fof(f29226,plain,(
% 144.13/18.81 ~sQ104_spl),
% 144.13/18.81 inference(contradiction_clause,[status(thm)],[f29225])).
% 144.13/18.81 fof(f29824,plain,(
% 144.13/18.81 ~leq(sK29_skl(n1),n3)|sK29_skl(n1)=n0|sK29_skl(n1)=n1|sK29_skl(n1)=n2|sK29_skl(n1)=n3|~sQ875_spl|~sQ9_spl),
% 144.13/18.81 inference(resolution,[status(thm)],[f324,f28213])).
% 144.13/18.81 fof(f29841,plain,(
% 144.13/18.81 ~sQ918_spl|sQ908_spl|sQ909_spl|sQ910_spl|sQ905_spl|~sQ875_spl|~sQ9_spl),
% 144.13/18.81 inference(split_clause,[status(thm)],[f29824,f29072,f28396,f28399,f28402,f28264,f24196,f402])).
% 144.13/18.81 fof(f29911,plain,(
% 144.13/18.81 ~leq(sK29_skl(n0),n3)|sK29_skl(n0)=n0|sK29_skl(n0)=n1|sK29_skl(n0)=n2|sK29_skl(n0)=n3|~sQ77_spl|~sQ9_spl),
% 144.13/18.81 inference(resolution,[status(thm)],[f26934,f324])).
% 144.13/18.81 fof(f30036,plain,(
% 144.13/18.81 ~sQ94_spl|sQ95_spl|sQ902_spl|sQ903_spl|sQ97_spl|~sQ77_spl|~sQ9_spl),
% 144.13/18.81 inference(split_clause,[status(thm)],[f29911,f1675,f1679,f27230,f27233,f1710,f1209,f402])).
% 144.13/18.81 fof(f30056,plain,(
% 144.13/18.81 $false|~sQ77_spl|~sQ9_spl|sQ94_spl),
% 144.13/18.81 inference(forward_subsumption_resolution,[status(thm)],[f1677,f26933])).
% 144.13/18.81 fof(f30057,plain,(
% 144.13/18.81 ~sQ77_spl|~sQ9_spl|sQ94_spl),
% 144.13/18.81 inference(contradiction_clause,[status(thm)],[f30056])).
% 144.13/18.81 fof(f30058,plain,(
% 144.13/18.81 $false),
% 144.13/18.81 inference(sat_refutation,[status(thm)],[f408,f412,f416,f436,f464,f466,f645,f680,f724,f726,f728,f730,f732,f734,f816,f818,f872,f883,f884,f901,f908,f1153,f1177,f1215,f1342,f1450,f1457,f1481,f1525,f1687,f1726,f1734,f1743,f1818,f2428,f2436,f2440,f2444,f2448,f2492,f2494,f2811,f2968,f2972,f2976,f3028,f3135,f3137,f3139,f3198,f3200,f3225,f3238,f3245,f3252,f3259,f3266,f4012,f4016,f4053,f4325,f4329,f4369,f8036,f8057,f8934,f9476,f9495,f9504,f9930,f10429,f12404,f12423,f12431,f13193,f13789,f19615,f19639,f19676,f19682,f20713,f21949,f23927,f24214,f24222,f24236,f24525,f24558,f24822,f24892,f26651,f26797,f26932,f27424,f27426,f28430,f28432,f28434,f28436,f28438,f29090,f29226,f29841,f30036,f30057])).
% 144.13/18.81 % SZS output end CNFRefutation for theBenchmark.p
% 71.49/18.85 % Elapsed time: 18.376102 seconds
% 71.49/18.85 % CPU time: 145.063497 seconds
% 71.49/18.85 % Total memory used: 563.817 MB
% 71.49/18.85 % Net memory used: 483.010 MB
%------------------------------------------------------------------------------