%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV053+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:59 PM UTC 2026
% Result : Theorem 0.30s 6.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV053+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/6.28 % Computer : n008.cluster.edu
% 0.18/6.28 % Model : x86_64 x86_64
% 0.18/6.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/6.28 % Memory : 8046.5625MB
% 0.18/6.28 % OS : Linux 6.8.0-71-generic
% 0.18/6.28 % CPULimit : 300
% 0.18/6.28 % WCLimit : 300
% 0.18/6.28 % DateTime : Mon Sep 21 08:30:16 UTC 2026
% 0.18/6.28 % CPUTime :
% 0.22/6.31 % Drodi V4.1.1
% 0.30/6.65 % Refutation found
% 0.30/6.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.30/6.65 % SZS output start CNFRefutation for theBenchmark
% 0.30/6.65 fof(f26,axiom,(
% 0.30/6.65 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f27,axiom,(
% 0.30/6.65 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f28,axiom,(
% 0.30/6.65 succ(tptp_minus_1) = n0 ),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f39,axiom,(
% 0.30/6.65 (! [X] : minus(X,n1) = pred(X) )),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f40,axiom,(
% 0.30/6.65 (! [X] : pred(succ(X)) = X )),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f53,conjecture,(
% 0.30/6.65 ( ( leq(n0,pv10)& leq(n0,pv12)& leq(pv10,minus(n135300,n1))& leq(pv12,minus(n5,n1))& (! [A,B] :( ( leq(n0,A)& leq(A,minus(pv12,n1)) )=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))) ))& (! [C,D] :( ( leq(n0,C)& leq(C,minus(pv10,n1)) )=> sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1 ) ))=> ( n0 = sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))& leq(n0,pv10)& leq(n0,pv12)& leq(pv10,minus(n135300,n1))& leq(pv12,minus(n5,n1))& (! [E,F] :( ( leq(n0,E)& leq(E,minus(pv12,n1)) )=> a_select3(q,pv10,E) = divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))) ))& (! [G,H] :( ( leq(n0,G)& leq(G,minus(pv10,n1)) )=> sum(n0,minus(n5,n1),a_select3(q,G,H)) = n1 ) )) ) ),
% 0.30/6.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/6.65 fof(f54,negated_conjecture,(
% 0.30/6.65 ~(( ( leq(n0,pv10)& leq(n0,pv12)& leq(pv10,minus(n135300,n1))& leq(pv12,minus(n5,n1))& (! [A,B] :( ( leq(n0,A)& leq(A,minus(pv12,n1)) )=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))) ))& (! [C,D] :( ( leq(n0,C)& leq(C,minus(pv10,n1)) )=> sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1 ) ))=> ( n0 = sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))& leq(n0,pv10)& leq(n0,pv12)& leq(pv10,minus(n135300,n1))& leq(pv12,minus(n5,n1))& (! [E,F] :( ( leq(n0,E)& leq(E,minus(pv12,n1)) )=> a_select3(q,pv10,E) = divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))) ))& (! [G,H] :( ( leq(n0,G)& leq(G,minus(pv10,n1)) )=> sum(n0,minus(n5,n1),a_select3(q,G,H)) = n1 ) )) ) )),
% 0.30/6.65 inference(negated_conjecture,[status(cth)],[f53])).
% 0.30/6.65 fof(f204,plain,(
% 0.30/6.65 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f26])).
% 0.30/6.65 fof(f205,plain,(
% 0.30/6.65 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f27])).
% 0.30/6.65 fof(f206,plain,(
% 0.30/6.65 succ(tptp_minus_1)=n0),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f28])).
% 0.30/6.65 fof(f217,plain,(
% 0.30/6.65 ![X0]: (minus(X0,n1)=pred(X0))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f39])).
% 0.30/6.65 fof(f218,plain,(
% 0.30/6.65 ![X0]: (pred(succ(X0))=X0)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f40])).
% 0.30/6.65 fof(f251,plain,(
% 0.30/6.65 ((((((leq(n0,pv10)&leq(n0,pv12))&leq(pv10,minus(n135300,n1)))&leq(pv12,minus(n5,n1)))&(![A,B]: ((~leq(n0,A)|~leq(A,minus(pv12,n1)))|a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))))))&(![C,D]: ((~leq(n0,C)|~leq(C,minus(pv10,n1)))|sum(n0,minus(n5,n1),a_select3(q,C,D))=n1)))&((((((~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10))|~leq(n0,pv12))|~leq(pv10,minus(n135300,n1)))|~leq(pv12,minus(n5,n1)))|(?[E,F]: ((leq(n0,E)&leq(E,minus(pv12,n1)))&~a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))))))|(?[G,H]: ((leq(n0,G)&leq(G,minus(pv10,n1)))&~sum(n0,minus(n5,n1),a_select3(q,G,H))=n1))))),
% 0.30/6.65 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.30/6.65 fof(f252,definition,(
% 0.30/6.65 ![E,F]: (sP3_prd(F,E)<=>((leq(n0,E)&leq(E,minus(pv12,n1)))&~a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10))))))))),
% 0.30/6.65 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.30/6.65 fof(f253,plain,(
% 0.30/6.65 (((((leq(n0,pv10)&leq(n0,pv12))&leq(pv10,minus(n135300,n1)))&leq(pv12,minus(n5,n1)))&(![A,B]: ((~leq(n0,A)|~leq(A,minus(pv12,n1)))|a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))))))&(![C,D]: ((~leq(n0,C)|~leq(C,minus(pv10,n1)))|sum(n0,minus(n5,n1),a_select3(q,C,D))=n1)))&((((((~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10))|~leq(n0,pv12))|~leq(pv10,minus(n135300,n1)))|~leq(pv12,minus(n5,n1)))|(?[E,F]: sP3_prd(F,E)))|(?[G,H]: ((leq(n0,G)&leq(G,minus(pv10,n1)))&~sum(n0,minus(n5,n1),a_select3(q,G,H))=n1)))),
% 0.30/6.65 inference(formula_renaming,[status(thm)],[f251,f252])).
% 0.30/6.65 fof(f254,plain,(
% 0.30/6.65 (((((leq(n0,pv10)&leq(n0,pv12))&leq(pv10,minus(n135300,n1)))&leq(pv12,minus(n5,n1)))&(![A]: ((~leq(n0,A)|~leq(A,minus(pv12,n1)))|(![B]: a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10))))))))))&(![C]: ((~leq(n0,C)|~leq(C,minus(pv10,n1)))|(![D]: sum(n0,minus(n5,n1),a_select3(q,C,D))=n1))))&((((((~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10))|~leq(n0,pv12))|~leq(pv10,minus(n135300,n1)))|~leq(pv12,minus(n5,n1)))|(?[E,F]: sP3_prd(F,E)))|(?[G]: ((leq(n0,G)&leq(G,minus(pv10,n1)))&(?[H]: ~sum(n0,minus(n5,n1),a_select3(q,G,H))=n1))))),
% 0.30/6.65 inference(miniscoping,[status(thm)],[f253])).
% 0.30/6.65 fof(f255,plain,(
% 0.30/6.65 (((((leq(n0,pv10)&leq(n0,pv12))&leq(pv10,minus(n135300,n1)))&leq(pv12,minus(n5,n1)))&(![A]: ((~leq(n0,A)|~leq(A,minus(pv12,n1)))|(![B]: a_select3(q,pv10,A)=divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10))))))))))&(![C]: ((~leq(n0,C)|~leq(C,minus(pv10,n1)))|(![D]: sum(n0,minus(n5,n1),a_select3(q,C,D))=n1))))&((((((~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10))|~leq(n0,pv12))|~leq(pv10,minus(n135300,n1)))|~leq(pv12,minus(n5,n1)))|sP3_prd(sK24_skl,sK23_skl))|((leq(n0,sK25_skl)&leq(sK25_skl,minus(pv10,n1)))&~sum(n0,minus(n5,n1),a_select3(q,sK25_skl,sK26_skl))=n1))),
% 0.30/6.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(E,sK23_skl),skolemize(F,sK24_skl),skolemize(G,sK25_skl),skolemize(H,sK26_skl)],[f254])).
% 0.30/6.65 fof(f256,plain,(
% 0.30/6.65 leq(n0,pv10)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f257,plain,(
% 0.30/6.65 leq(n0,pv12)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f258,plain,(
% 0.30/6.65 leq(pv10,minus(n135300,n1))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f259,plain,(
% 0.30/6.65 leq(pv12,minus(n5,n1))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f260,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,minus(pv12,n1))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f261,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,minus(pv10,n1))|sum(n0,minus(n5,n1),a_select3(q,X0,X1))=n1)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f262,plain,(
% 0.30/6.65 ~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(n0,sK25_skl)),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f263,plain,(
% 0.30/6.65 ~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,minus(pv10,n1))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f264,plain,(
% 0.30/6.65 ~n0=sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,minus(n5,n1),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f255])).
% 0.30/6.65 fof(f338,plain,(
% 0.30/6.65 ![E,F]: ((~sP3_prd(F,E)|((leq(n0,E)&leq(E,minus(pv12,n1)))&~a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10))))))))&(sP3_prd(F,E)|((~leq(n0,E)|~leq(E,minus(pv12,n1)))|a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))))))),
% 0.30/6.65 inference(NNF_transformation,[status(thm)],[f252])).
% 0.30/6.65 fof(f339,plain,(
% 0.30/6.65 (![E,F]: (~sP3_prd(F,E)|((leq(n0,E)&leq(E,minus(pv12,n1)))&~a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))))))&(![E,F]: (sP3_prd(F,E)|((~leq(n0,E)|~leq(E,minus(pv12,n1)))|a_select3(q,pv10,E)=divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))))))),
% 0.30/6.65 inference(miniscoping,[status(thm)],[f338])).
% 0.30/6.65 fof(f340,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|leq(n0,X1))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f339])).
% 0.30/6.65 fof(f341,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|leq(X1,minus(pv12,n1)))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f339])).
% 0.30/6.65 fof(f342,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(cnf_transformation,[status(thm)],[f339])).
% 0.30/6.65 fof(f352,plain,(
% 0.30/6.65 tptp_float_0_0=n0),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f205,f204])).
% 0.30/6.65 fof(f367,plain,(
% 0.30/6.65 leq(pv10,pred(n135300))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f258])).
% 0.30/6.65 fof(f368,plain,(
% 0.30/6.65 leq(pv12,pred(n5))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f259])).
% 0.30/6.65 fof(f369,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f260])).
% 0.30/6.65 fof(f370,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f369])).
% 0.30/6.65 fof(f371,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv10))|sum(n0,minus(n5,n1),a_select3(q,X0,X1))=n1)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f261])).
% 0.30/6.65 fof(f372,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv10))|sum(n0,pred(n5),a_select3(q,X0,X1))=n1)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f371])).
% 0.30/6.65 fof(f373,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(n0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f262])).
% 0.30/6.65 fof(f374,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(n0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f373])).
% 0.30/6.65 fof(f375,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(n0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f374])).
% 0.30/6.65 fof(f376,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(n0,sK25_skl)),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f375,f256])).
% 0.30/6.65 fof(f377,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,minus(pv10,n1))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f263])).
% 0.30/6.65 fof(f378,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,minus(pv10,n1))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f377])).
% 0.30/6.65 fof(f379,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,minus(pv10,n1))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f378])).
% 0.30/6.65 fof(f380,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f379])).
% 0.30/6.65 fof(f381,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f380,f256])).
% 0.30/6.65 fof(f382,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,minus(n135300,n1))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,minus(n5,n1),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f264])).
% 0.30/6.65 fof(f383,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,minus(n5,n1))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,minus(n5,n1),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f382])).
% 0.30/6.65 fof(f384,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,minus(n5,n1),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f383])).
% 0.30/6.65 fof(f385,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv10)|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f384])).
% 0.30/6.65 fof(f386,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(n0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f385,f256])).
% 0.30/6.65 fof(f397,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|leq(X1,pred(pv12)))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f341])).
% 0.30/6.65 fof(f398,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f217,f342])).
% 0.30/6.65 fof(f404,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f398])).
% 0.30/6.65 fof(f405,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|leq(tptp_float_0_0,X1))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f340])).
% 0.30/6.65 fof(f433,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f386])).
% 0.30/6.65 fof(f434,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f381])).
% 0.30/6.65 fof(f435,plain,(
% 0.30/6.65 ~n0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f376])).
% 0.30/6.65 fof(f436,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv10))|sum(tptp_float_0_0,pred(n5),a_select3(q,X0,X1))=n1)),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f372])).
% 0.30/6.65 fof(f437,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(n0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f370])).
% 0.30/6.65 fof(f438,plain,(
% 0.30/6.65 leq(tptp_float_0_0,pv12)),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f257])).
% 0.30/6.65 fof(f449,plain,(
% 0.30/6.65 succ(tptp_minus_1)=tptp_float_0_0),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f206])).
% 0.30/6.65 fof(f450,plain,(
% 0.30/6.65 ![X0]: (tptp_float_0_0=sum(tptp_float_0_0,tptp_minus_1,X0))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f352,f205])).
% 0.30/6.65 fof(f494,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f404])).
% 0.30/6.65 fof(f495,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f494])).
% 0.30/6.65 fof(f496,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f495])).
% 0.30/6.65 fof(f497,plain,(
% 0.30/6.65 ![X0,X1]: (~sP3_prd(X0,X1)|~a_select3(q,pv10,X1)=divide(sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f496])).
% 0.30/6.65 fof(f508,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f433])).
% 0.30/6.65 fof(f509,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f508])).
% 0.30/6.65 fof(f510,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f509])).
% 0.30/6.65 fof(f511,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f510])).
% 0.30/6.65 fof(f512,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f511])).
% 0.30/6.65 fof(f513,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f512])).
% 0.30/6.65 fof(f514,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f513,f367])).
% 0.30/6.65 fof(f515,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f434])).
% 0.30/6.65 fof(f516,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f515])).
% 0.30/6.65 fof(f517,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f516])).
% 0.30/6.65 fof(f518,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f517])).
% 0.30/6.65 fof(f519,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f518])).
% 0.30/6.65 fof(f520,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f519,f367])).
% 0.30/6.65 fof(f521,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(n0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f435])).
% 0.30/6.65 fof(f522,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(n0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f521])).
% 0.30/6.65 fof(f523,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f522])).
% 0.30/6.65 fof(f524,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f523])).
% 0.30/6.65 fof(f525,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(n0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f524])).
% 0.30/6.65 fof(f526,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv10,pred(n135300))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f525])).
% 0.30/6.65 fof(f527,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(tptp_float_0_0,pv12)|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f526,f367])).
% 0.30/6.65 fof(f528,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv10))|sum(tptp_float_0_0,pred(n5),a_select3(q,X0,X1))=n1)),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f436])).
% 0.30/6.65 fof(f529,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f437])).
% 0.30/6.65 fof(f530,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f529])).
% 0.30/6.65 fof(f531,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f530])).
% 0.30/6.65 fof(f532,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f531])).
% 0.30/6.65 fof(f533,plain,(
% 0.30/6.65 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv12))|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)))))))),
% 0.30/6.65 inference(forward_demodulation,[status(thm)],[f352,f532])).
% 0.30/6.65 fof(f534,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(backward_subsumption_resolution,[status(thm)],[f527,f438])).
% 0.30/6.65 fof(f535,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(backward_subsumption_resolution,[status(thm)],[f520,f438])).
% 0.30/6.65 fof(f536,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|~leq(pv12,pred(n5))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(backward_subsumption_resolution,[status(thm)],[f514,f438])).
% 0.30/6.65 fof(f607,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f534,f368])).
% 0.30/6.65 fof(f608,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f535,f368])).
% 0.30/6.65 fof(f609,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,pred(tptp_float_0_0),sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(forward_subsumption_resolution,[status(thm)],[f536,f368])).
% 0.30/6.65 fof(f627,plain,(
% 0.30/6.65 pred(tptp_float_0_0)=tptp_minus_1),
% 0.30/6.65 inference(paramodulation,[status(thm)],[f449,f218])).
% 0.30/6.65 fof(f629,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,tptp_minus_1,sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f627,f609])).
% 0.30/6.65 fof(f630,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,tptp_minus_1,sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.65 inference(backward_demodulation,[status(thm)],[f627,f608])).
% 0.30/6.65 fof(f631,plain,(
% 0.30/6.65 ~tptp_float_0_0=sum(tptp_float_0_0,tptp_minus_1,sqrt(times(minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,pv71,tptp_float_0_0),a_select2(x,pv10)))))|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.67 inference(backward_demodulation,[status(thm)],[f627,f607])).
% 0.30/6.67 fof(f632,plain,(
% 0.30/6.67 ~tptp_float_0_0=tptp_float_0_0|sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.67 inference(forward_demodulation,[status(thm)],[f450,f629])).
% 0.30/6.67 fof(f633,plain,(
% 0.30/6.67 sP3_prd(sK24_skl,sK23_skl)|~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.67 inference(trivial_equality_resolution,[status(thm)],[f632])).
% 0.30/6.67 fof(f634,plain,(
% 0.30/6.67 ~tptp_float_0_0=tptp_float_0_0|sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.67 inference(forward_demodulation,[status(thm)],[f450,f630])).
% 0.30/6.67 fof(f635,plain,(
% 0.30/6.67 sP3_prd(sK24_skl,sK23_skl)|leq(sK25_skl,pred(pv10))),
% 0.30/6.67 inference(trivial_equality_resolution,[status(thm)],[f634])).
% 0.30/6.67 fof(f636,plain,(
% 0.30/6.67 ~tptp_float_0_0=tptp_float_0_0|sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.67 inference(forward_demodulation,[status(thm)],[f450,f631])).
% 0.30/6.67 fof(f637,plain,(
% 0.30/6.67 sP3_prd(sK24_skl,sK23_skl)|leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.67 inference(trivial_equality_resolution,[status(thm)],[f636])).
% 0.30/6.67 fof(f689,plain,(
% 0.30/6.67 ![X0,X1,X2]: (~leq(tptp_float_0_0,X0)|a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10))))))|~sP3_prd(X2,X0))),
% 0.30/6.67 inference(resolution,[status(thm)],[f533,f397])).
% 0.30/6.67 fof(f693,plain,(
% 0.30/6.67 ![X0,X1]: (~sP3_prd(X0,X1))),
% 0.30/6.67 inference(backward_subsumption_resolution,[status(thm)],[f497,f694])).
% 0.30/6.67 fof(f694,plain,(
% 0.30/6.67 ![X0,X1,X2]: (a_select3(q,pv10,X0)=divide(sqrt(times(minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X0,tptp_float_0_0),a_select2(x,pv10)))),sum(tptp_float_0_0,pred(n5),sqrt(times(minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10)),minus(a_select3(center,X1,tptp_float_0_0),a_select2(x,pv10))))))|~sP3_prd(X2,X0))),
% 0.30/6.67 inference(forward_subsumption_resolution,[status(thm)],[f689,f405])).
% 0.30/6.67 fof(f695,plain,(
% 0.30/6.67 leq(tptp_float_0_0,sK25_skl)),
% 0.30/6.67 inference(backward_subsumption_resolution,[status(thm)],[f637,f693])).
% 0.30/6.67 fof(f696,plain,(
% 0.30/6.67 leq(sK25_skl,pred(pv10))),
% 0.30/6.67 inference(backward_subsumption_resolution,[status(thm)],[f635,f693])).
% 0.30/6.67 fof(f697,plain,(
% 0.30/6.67 ~sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,sK26_skl))=n1),
% 0.30/6.67 inference(backward_subsumption_resolution,[status(thm)],[f633,f693])).
% 0.30/6.67 fof(f773,plain,(
% 0.30/6.67 ![X0]: (~leq(tptp_float_0_0,sK25_skl)|sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,X0))=n1)),
% 0.30/6.67 inference(resolution,[status(thm)],[f696,f528])).
% 0.30/6.67 fof(f776,plain,(
% 0.30/6.67 ~n1=n1),
% 0.30/6.67 inference(backward_demodulation,[status(thm)],[f777,f697])).
% 0.30/6.67 fof(f777,plain,(
% 0.30/6.67 ![X0]: (sum(tptp_float_0_0,pred(n5),a_select3(q,sK25_skl,X0))=n1)),
% 0.30/6.67 inference(forward_subsumption_resolution,[status(thm)],[f773,f695])).
% 0.30/6.67 fof(f778,plain,(
% 0.30/6.67 $false),
% 0.30/6.67 inference(trivial_equality_resolution,[status(thm)],[f776])).
% 0.30/6.67 % SZS output end CNFRefutation for theBenchmark.p
% 0.30/6.68 % Elapsed time: 0.380514 seconds
% 0.30/6.68 % CPU time: 2.681788 seconds
% 0.30/6.68 % Total memory used: 131.735 MB
% 0.30/6.68 % Net memory used: 128.686 MB
%------------------------------------------------------------------------------