%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV095+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:50:04 PM UTC 2026
% Result : Theorem 7.86s 1.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV095+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.17/0.45 % Computer : n006.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 08:30:43 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.51 % Drodi V4.1.1
% 7.86/1.67 % Refutation found
% 7.86/1.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.86/1.67 % SZS output start CNFRefutation for theBenchmark
% 7.86/1.67 fof(f26,axiom,(
% 7.86/1.67 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 7.86/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.86/1.67 fof(f27,axiom,(
% 7.86/1.67 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 7.86/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.86/1.67 fof(f39,axiom,(
% 7.86/1.67 (! [X] : minus(X,n1) = pred(X) )),
% 7.86/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.86/1.67 fof(f53,conjecture,(
% 7.86/1.67 ( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(n0,pv51)& leq(pv5,minus(n999,n1))& leq(pv51,minus(n6,n1))& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,minus(pv5,n1)) )=> ( a_select3(u_defuse,A,B) = use& a_select3(z_defuse,A,B) = use ) ) ))=> ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(n0,pv51)& leq(pv5,minus(n999,n1))& leq(pv51,minus(n6,n1))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,minus(pv5,n1)) )=> ( a_select3(u_defuse,C,D) = use& a_select3(z_defuse,C,D) = use ) ) )) ) ),
% 7.86/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.86/1.67 fof(f54,negated_conjecture,(
% 7.86/1.67 ~(( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(n0,pv51)& leq(pv5,minus(n999,n1))& leq(pv51,minus(n6,n1))& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,minus(pv5,n1)) )=> ( a_select3(u_defuse,A,B) = use& a_select3(z_defuse,A,B) = use ) ) ))=> ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(n0,pv51)& leq(pv5,minus(n999,n1))& leq(pv51,minus(n6,n1))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,minus(pv5,n1)) )=> ( a_select3(u_defuse,C,D) = use& a_select3(z_defuse,C,D) = use ) ) )) ) )),
% 7.86/1.67 inference(negated_conjecture,[status(cth)],[f53])).
% 7.86/1.67 fof(f214,plain,(
% 7.86/1.67 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f26])).
% 7.86/1.67 fof(f215,plain,(
% 7.86/1.67 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f27])).
% 7.86/1.67 fof(f227,plain,(
% 7.86/1.67 ![X0]: (minus(X0,n1)=pred(X0))),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f39])).
% 7.86/1.67 fof(f261,plain,(
% 7.86/1.67 ((((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(n0,pv51))&leq(pv5,minus(n999,n1)))&leq(pv51,minus(n6,n1)))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,minus(pv5,n1)))|(a_select3(u_defuse,A,B)=use&a_select3(z_defuse,A,B)=use))))&(((((((((((((((((((((((((((((((~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use)|~a_select2(rho_defuse,n2)=use)|~a_select2(sigma_defuse,n0)=use)|~a_select2(sigma_defuse,n1)=use)|~a_select2(sigma_defuse,n2)=use)|~a_select2(sigma_defuse,n3)=use)|~a_select2(sigma_defuse,n4)=use)|~a_select2(sigma_defuse,n5)=use)|~a_select3(u_defuse,n0,n0)=use)|~a_select3(u_defuse,n1,n0)=use)|~a_select3(u_defuse,n2,n0)=use)|~a_select2(xinit_defuse,n3)=use)|~a_select2(xinit_defuse,n4)=use)|~a_select2(xinit_defuse,n5)=use)|~a_select2(xinit_mean_defuse,n0)=use)|~a_select2(xinit_mean_defuse,n1)=use)|~a_select2(xinit_mean_defuse,n2)=use)|~a_select2(xinit_mean_defuse,n3)=use)|~a_select2(xinit_mean_defuse,n4)=use)|~a_select2(xinit_mean_defuse,n5)=use)|~a_select2(xinit_noise_defuse,n0)=use)|~a_select2(xinit_noise_defuse,n1)=use)|~a_select2(xinit_noise_defuse,n2)=use)|~a_select2(xinit_noise_defuse,n3)=use)|~a_select2(xinit_noise_defuse,n4)=use)|~a_select2(xinit_noise_defuse,n5)=use)|~leq(n0,pv5))|~leq(n0,pv51))|~leq(pv5,minus(n999,n1)))|~leq(pv51,minus(n6,n1)))|(?[C,D]: ((((leq(n0,C)&leq(n0,D))&leq(C,n2))&leq(D,minus(pv5,n1)))&(~a_select3(u_defuse,C,D)=use|~a_select3(z_defuse,C,D)=use)))))),
% 7.86/1.67 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 7.86/1.67 fof(f262,plain,(
% 7.86/1.67 (((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(n0,pv51))&leq(pv5,minus(n999,n1)))&leq(pv51,minus(n6,n1)))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,minus(pv5,n1)))|(a_select3(u_defuse,A,B)=use&a_select3(z_defuse,A,B)=use))))&(((((((((((((((((((((((((((((((~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use)|~a_select2(rho_defuse,n2)=use)|~a_select2(sigma_defuse,n0)=use)|~a_select2(sigma_defuse,n1)=use)|~a_select2(sigma_defuse,n2)=use)|~a_select2(sigma_defuse,n3)=use)|~a_select2(sigma_defuse,n4)=use)|~a_select2(sigma_defuse,n5)=use)|~a_select3(u_defuse,n0,n0)=use)|~a_select3(u_defuse,n1,n0)=use)|~a_select3(u_defuse,n2,n0)=use)|~a_select2(xinit_defuse,n3)=use)|~a_select2(xinit_defuse,n4)=use)|~a_select2(xinit_defuse,n5)=use)|~a_select2(xinit_mean_defuse,n0)=use)|~a_select2(xinit_mean_defuse,n1)=use)|~a_select2(xinit_mean_defuse,n2)=use)|~a_select2(xinit_mean_defuse,n3)=use)|~a_select2(xinit_mean_defuse,n4)=use)|~a_select2(xinit_mean_defuse,n5)=use)|~a_select2(xinit_noise_defuse,n0)=use)|~a_select2(xinit_noise_defuse,n1)=use)|~a_select2(xinit_noise_defuse,n2)=use)|~a_select2(xinit_noise_defuse,n3)=use)|~a_select2(xinit_noise_defuse,n4)=use)|~a_select2(xinit_noise_defuse,n5)=use)|~leq(n0,pv5))|~leq(n0,pv51))|~leq(pv5,minus(n999,n1)))|~leq(pv51,minus(n6,n1)))|((((leq(n0,sK23_skl)&leq(n0,sK24_skl))&leq(sK23_skl,n2))&leq(sK24_skl,minus(pv5,n1)))&(~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use)))),
% 7.86/1.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(C,sK23_skl),skolemize(D,sK24_skl)],[f261])).
% 7.86/1.67 fof(f263,plain,(
% 7.86/1.67 a_select2(rho_defuse,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f264,plain,(
% 7.86/1.67 a_select2(rho_defuse,n1)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f265,plain,(
% 7.86/1.67 a_select2(rho_defuse,n2)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f266,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f267,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n1)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f268,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n2)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f269,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n3)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f270,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n4)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f271,plain,(
% 7.86/1.67 a_select2(sigma_defuse,n5)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f272,plain,(
% 7.86/1.67 a_select3(u_defuse,n0,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f273,plain,(
% 7.86/1.67 a_select3(u_defuse,n1,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f274,plain,(
% 7.86/1.67 a_select3(u_defuse,n2,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f275,plain,(
% 7.86/1.67 a_select2(xinit_defuse,n3)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f276,plain,(
% 7.86/1.67 a_select2(xinit_defuse,n4)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f277,plain,(
% 7.86/1.67 a_select2(xinit_defuse,n5)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f278,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f279,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n1)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f280,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n2)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f281,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n3)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f282,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n4)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f283,plain,(
% 7.86/1.67 a_select2(xinit_mean_defuse,n5)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f284,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n0)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f285,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n1)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f286,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n2)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f287,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n3)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f288,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n4)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f289,plain,(
% 7.86/1.67 a_select2(xinit_noise_defuse,n5)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f290,plain,(
% 7.86/1.67 leq(n0,pv5)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f291,plain,(
% 7.86/1.67 leq(n0,pv51)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f292,plain,(
% 7.86/1.67 leq(pv5,minus(n999,n1))),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f293,plain,(
% 7.86/1.67 leq(pv51,minus(n6,n1))),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f294,plain,(
% 7.86/1.67 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(u_defuse,X0,X1)=use)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f295,plain,(
% 7.86/1.67 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(z_defuse,X0,X1)=use)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f296,plain,(
% 7.86/1.67 ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f297,plain,(
% 7.86/1.67 ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f298,plain,(
% 7.86/1.67 ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f299,plain,(
% 7.86/1.67 ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f300,plain,(
% 7.86/1.67 ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.67 inference(cnf_transformation,[status(thm)],[f262])).
% 7.86/1.67 fof(f393,plain,(
% 7.86/1.67 tptp_float_0_0=n0),
% 7.86/1.67 inference(backward_demodulation,[status(thm)],[f215,f214])).
% 7.86/1.67 fof(f408,plain,(
% 7.86/1.67 leq(pv5,pred(n999))),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f292])).
% 7.86/1.67 fof(f409,plain,(
% 7.86/1.67 leq(pv51,pred(n6))),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f293])).
% 7.86/1.67 fof(f410,plain,(
% 7.86/1.67 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(u_defuse,X0,X1)=use)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f294])).
% 7.86/1.67 fof(f411,plain,(
% 7.86/1.67 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(z_defuse,X0,X1)=use)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f295])).
% 7.86/1.67 fof(f412,plain,(
% 7.86/1.67 ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f263,f296])).
% 7.86/1.67 fof(f413,plain,(
% 7.86/1.67 ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f264,f412])).
% 7.86/1.67 fof(f414,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f265,f413])).
% 7.86/1.67 fof(f415,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f266,f414])).
% 7.86/1.67 fof(f416,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f267,f415])).
% 7.86/1.67 fof(f417,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f268,f416])).
% 7.86/1.67 fof(f418,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f269,f417])).
% 7.86/1.67 fof(f419,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f270,f418])).
% 7.86/1.67 fof(f420,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f271,f419])).
% 7.86/1.67 fof(f421,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f272,f420])).
% 7.86/1.67 fof(f422,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f273,f421])).
% 7.86/1.67 fof(f423,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f274,f422])).
% 7.86/1.67 fof(f424,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f275,f423])).
% 7.86/1.67 fof(f425,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f276,f424])).
% 7.86/1.67 fof(f426,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f277,f425])).
% 7.86/1.67 fof(f427,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f278,f426])).
% 7.86/1.67 fof(f428,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f279,f427])).
% 7.86/1.67 fof(f429,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f280,f428])).
% 7.86/1.67 fof(f430,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f281,f429])).
% 7.86/1.67 fof(f431,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f282,f430])).
% 7.86/1.67 fof(f432,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f283,f431])).
% 7.86/1.67 fof(f433,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f284,f432])).
% 7.86/1.67 fof(f434,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f285,f433])).
% 7.86/1.67 fof(f435,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f286,f434])).
% 7.86/1.67 fof(f436,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f287,f435])).
% 7.86/1.67 fof(f437,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f288,f436])).
% 7.86/1.67 fof(f438,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f289,f437])).
% 7.86/1.67 fof(f439,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,minus(n6,n1))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f438])).
% 7.86/1.67 fof(f440,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f439])).
% 7.86/1.67 fof(f441,plain,(
% 7.86/1.67 ~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(duplicate_literals_removal,[status(thm)],[f440])).
% 7.86/1.67 fof(f442,plain,(
% 7.86/1.67 ~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(trivial_equality_resolution,[status(thm)],[f441])).
% 7.86/1.67 fof(f443,plain,(
% 7.86/1.67 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK23_skl)),
% 7.86/1.67 inference(forward_subsumption_resolution,[status(thm)],[f442,f290])).
% 7.86/1.67 fof(f444,plain,(
% 7.86/1.67 ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f263,f297])).
% 7.86/1.67 fof(f445,plain,(
% 7.86/1.67 ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f264,f444])).
% 7.86/1.67 fof(f446,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f265,f445])).
% 7.86/1.67 fof(f447,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f266,f446])).
% 7.86/1.67 fof(f448,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f267,f447])).
% 7.86/1.67 fof(f449,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f268,f448])).
% 7.86/1.67 fof(f450,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f269,f449])).
% 7.86/1.67 fof(f451,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f270,f450])).
% 7.86/1.67 fof(f452,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f271,f451])).
% 7.86/1.67 fof(f453,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f272,f452])).
% 7.86/1.67 fof(f454,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f273,f453])).
% 7.86/1.67 fof(f455,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f274,f454])).
% 7.86/1.67 fof(f456,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f275,f455])).
% 7.86/1.67 fof(f457,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f276,f456])).
% 7.86/1.67 fof(f458,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f277,f457])).
% 7.86/1.67 fof(f459,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f278,f458])).
% 7.86/1.67 fof(f460,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f279,f459])).
% 7.86/1.67 fof(f461,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f280,f460])).
% 7.86/1.67 fof(f462,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f281,f461])).
% 7.86/1.67 fof(f463,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f282,f462])).
% 7.86/1.67 fof(f464,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f283,f463])).
% 7.86/1.67 fof(f465,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f284,f464])).
% 7.86/1.67 fof(f466,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f285,f465])).
% 7.86/1.67 fof(f467,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f286,f466])).
% 7.86/1.67 fof(f468,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f287,f467])).
% 7.86/1.67 fof(f469,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f288,f468])).
% 7.86/1.67 fof(f470,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f289,f469])).
% 7.86/1.67 fof(f471,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,minus(n6,n1))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f470])).
% 7.86/1.67 fof(f472,plain,(
% 7.86/1.67 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_demodulation,[status(thm)],[f227,f471])).
% 7.86/1.67 fof(f473,plain,(
% 7.86/1.67 ~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(duplicate_literals_removal,[status(thm)],[f472])).
% 7.86/1.67 fof(f474,plain,(
% 7.86/1.67 ~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(trivial_equality_resolution,[status(thm)],[f473])).
% 7.86/1.67 fof(f475,plain,(
% 7.86/1.67 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(n0,sK24_skl)),
% 7.86/1.67 inference(forward_subsumption_resolution,[status(thm)],[f474,f290])).
% 7.86/1.67 fof(f476,plain,(
% 7.86/1.67 ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f263,f298])).
% 7.86/1.68 fof(f477,plain,(
% 7.86/1.68 ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f264,f476])).
% 7.86/1.68 fof(f478,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f265,f477])).
% 7.86/1.68 fof(f479,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f266,f478])).
% 7.86/1.68 fof(f480,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f267,f479])).
% 7.86/1.68 fof(f481,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f268,f480])).
% 7.86/1.68 fof(f482,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f269,f481])).
% 7.86/1.68 fof(f483,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f270,f482])).
% 7.86/1.68 fof(f484,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f271,f483])).
% 7.86/1.68 fof(f485,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f272,f484])).
% 7.86/1.68 fof(f486,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f273,f485])).
% 7.86/1.68 fof(f487,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f274,f486])).
% 7.86/1.68 fof(f488,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f275,f487])).
% 7.86/1.68 fof(f489,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f276,f488])).
% 7.86/1.68 fof(f490,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f277,f489])).
% 7.86/1.68 fof(f491,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f278,f490])).
% 7.86/1.68 fof(f492,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f279,f491])).
% 7.86/1.68 fof(f493,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f280,f492])).
% 7.86/1.68 fof(f494,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f281,f493])).
% 7.86/1.68 fof(f495,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f282,f494])).
% 7.86/1.68 fof(f496,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f283,f495])).
% 7.86/1.68 fof(f497,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f284,f496])).
% 7.86/1.68 fof(f498,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f285,f497])).
% 7.86/1.68 fof(f499,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f286,f498])).
% 7.86/1.68 fof(f500,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f287,f499])).
% 7.86/1.68 fof(f501,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f288,f500])).
% 7.86/1.68 fof(f502,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f289,f501])).
% 7.86/1.68 fof(f503,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,minus(n6,n1))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f227,f502])).
% 7.86/1.68 fof(f504,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f227,f503])).
% 7.86/1.68 fof(f505,plain,(
% 7.86/1.68 ~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(duplicate_literals_removal,[status(thm)],[f504])).
% 7.86/1.68 fof(f506,plain,(
% 7.86/1.68 ~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(trivial_equality_resolution,[status(thm)],[f505])).
% 7.86/1.68 fof(f507,plain,(
% 7.86/1.68 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.68 inference(forward_subsumption_resolution,[status(thm)],[f506,f290])).
% 7.86/1.68 fof(f508,plain,(
% 7.86/1.68 ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f263,f299])).
% 7.86/1.68 fof(f509,plain,(
% 7.86/1.68 ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f264,f508])).
% 7.86/1.68 fof(f510,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f265,f509])).
% 7.86/1.68 fof(f511,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f266,f510])).
% 7.86/1.68 fof(f512,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f267,f511])).
% 7.86/1.68 fof(f513,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f268,f512])).
% 7.86/1.68 fof(f514,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f269,f513])).
% 7.86/1.68 fof(f515,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f270,f514])).
% 7.86/1.68 fof(f516,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f271,f515])).
% 7.86/1.68 fof(f517,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f272,f516])).
% 7.86/1.68 fof(f518,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f273,f517])).
% 7.86/1.68 fof(f519,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f274,f518])).
% 7.86/1.68 fof(f520,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f275,f519])).
% 7.86/1.68 fof(f521,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f276,f520])).
% 7.86/1.68 fof(f522,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f277,f521])).
% 7.86/1.68 fof(f523,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f278,f522])).
% 7.86/1.68 fof(f524,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f279,f523])).
% 7.86/1.68 fof(f525,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f280,f524])).
% 7.86/1.68 fof(f526,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f281,f525])).
% 7.86/1.68 fof(f527,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f282,f526])).
% 7.86/1.68 fof(f528,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f283,f527])).
% 7.86/1.68 fof(f529,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f284,f528])).
% 7.86/1.68 fof(f530,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f285,f529])).
% 7.86/1.68 fof(f531,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f286,f530])).
% 7.86/1.68 fof(f532,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f287,f531])).
% 7.86/1.68 fof(f533,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f288,f532])).
% 7.86/1.68 fof(f534,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f289,f533])).
% 7.86/1.68 fof(f535,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,minus(n6,n1))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f227,f534])).
% 7.86/1.68 fof(f536,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,minus(pv5,n1))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f227,f535])).
% 7.86/1.68 fof(f537,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f227,f536])).
% 7.86/1.68 fof(f538,plain,(
% 7.86/1.68 ~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.68 inference(duplicate_literals_removal,[status(thm)],[f537])).
% 7.86/1.68 fof(f539,plain,(
% 7.86/1.68 ~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.68 inference(trivial_equality_resolution,[status(thm)],[f538])).
% 7.86/1.68 fof(f540,plain,(
% 7.86/1.68 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.68 inference(forward_subsumption_resolution,[status(thm)],[f539,f290])).
% 7.86/1.68 fof(f541,plain,(
% 7.86/1.68 ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f263,f300])).
% 7.86/1.68 fof(f542,plain,(
% 7.86/1.68 ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f264,f541])).
% 7.86/1.68 fof(f543,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f265,f542])).
% 7.86/1.68 fof(f544,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f266,f543])).
% 7.86/1.68 fof(f545,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f267,f544])).
% 7.86/1.68 fof(f546,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f268,f545])).
% 7.86/1.68 fof(f547,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f269,f546])).
% 7.86/1.68 fof(f548,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f270,f547])).
% 7.86/1.68 fof(f549,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f271,f548])).
% 7.86/1.68 fof(f550,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f272,f549])).
% 7.86/1.68 fof(f551,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f273,f550])).
% 7.86/1.68 fof(f552,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f274,f551])).
% 7.86/1.68 fof(f553,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f275,f552])).
% 7.86/1.68 fof(f554,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f276,f553])).
% 7.86/1.68 fof(f555,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f277,f554])).
% 7.86/1.68 fof(f556,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f278,f555])).
% 7.86/1.68 fof(f557,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f279,f556])).
% 7.86/1.68 fof(f558,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f280,f557])).
% 7.86/1.68 fof(f559,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f281,f558])).
% 7.86/1.68 fof(f560,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f282,f559])).
% 7.86/1.68 fof(f561,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f283,f560])).
% 7.86/1.68 fof(f562,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f284,f561])).
% 7.86/1.68 fof(f563,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f285,f562])).
% 7.86/1.68 fof(f564,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.68 inference(forward_demodulation,[status(thm)],[f286,f563])).
% 7.86/1.68 fof(f565,plain,(
% 7.86/1.68 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f287,f564])).
% 7.86/1.70 fof(f566,plain,(
% 7.86/1.70 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f288,f565])).
% 7.86/1.70 fof(f567,plain,(
% 7.86/1.70 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,minus(n999,n1))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f289,f566])).
% 7.86/1.70 fof(f568,plain,(
% 7.86/1.70 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,minus(n6,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f227,f567])).
% 7.86/1.70 fof(f569,plain,(
% 7.86/1.70 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f227,f568])).
% 7.86/1.70 fof(f570,plain,(
% 7.86/1.70 ~use=use|~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(duplicate_literals_removal,[status(thm)],[f569])).
% 7.86/1.70 fof(f571,plain,(
% 7.86/1.70 ~leq(n0,pv5)|~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(trivial_equality_resolution,[status(thm)],[f570])).
% 7.86/1.70 fof(f572,plain,(
% 7.86/1.70 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f571,f290])).
% 7.86/1.70 fof(f620,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f572])).
% 7.86/1.70 fof(f621,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f540])).
% 7.86/1.70 fof(f622,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f507])).
% 7.86/1.70 fof(f623,plain,(
% 7.86/1.70 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK24_skl)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f475])).
% 7.86/1.70 fof(f624,plain,(
% 7.86/1.70 ~leq(n0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK23_skl)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f443])).
% 7.86/1.70 fof(f625,plain,(
% 7.86/1.70 ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(z_defuse,X0,X1)=use)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f411])).
% 7.86/1.70 fof(f626,plain,(
% 7.86/1.70 ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(u_defuse,X0,X1)=use)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f410])).
% 7.86/1.70 fof(f627,plain,(
% 7.86/1.70 leq(tptp_float_0_0,pv51)),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f393,f291])).
% 7.86/1.70 fof(f702,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f620,f408])).
% 7.86/1.70 fof(f703,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f621,f408])).
% 7.86/1.70 fof(f704,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f622,f408])).
% 7.86/1.70 fof(f705,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK24_skl)),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f393,f623])).
% 7.86/1.70 fof(f706,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK24_skl)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f705,f408])).
% 7.86/1.70 fof(f707,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv5,pred(n999))|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK23_skl)),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f393,f624])).
% 7.86/1.70 fof(f708,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,pv51)|~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK23_skl)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f707,f408])).
% 7.86/1.70 fof(f709,plain,(
% 7.86/1.70 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(z_defuse,X0,X1)=use)),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f393,f625])).
% 7.86/1.70 fof(f710,plain,(
% 7.86/1.70 ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(u_defuse,X0,X1)=use)),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f393,f626])).
% 7.86/1.70 fof(f711,plain,(
% 7.86/1.70 ~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK23_skl)),
% 7.86/1.70 inference(backward_subsumption_resolution,[status(thm)],[f708,f627])).
% 7.86/1.70 fof(f712,plain,(
% 7.86/1.70 ~leq(pv51,pred(n6))|leq(tptp_float_0_0,sK24_skl)),
% 7.86/1.70 inference(backward_subsumption_resolution,[status(thm)],[f706,f627])).
% 7.86/1.70 fof(f713,plain,(
% 7.86/1.70 ~leq(pv51,pred(n6))|leq(sK23_skl,n2)),
% 7.86/1.70 inference(backward_subsumption_resolution,[status(thm)],[f704,f627])).
% 7.86/1.70 fof(f714,plain,(
% 7.86/1.70 ~leq(pv51,pred(n6))|leq(sK24_skl,pred(pv5))),
% 7.86/1.70 inference(backward_subsumption_resolution,[status(thm)],[f703,f627])).
% 7.86/1.70 fof(f715,plain,(
% 7.86/1.70 ~leq(pv51,pred(n6))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(backward_subsumption_resolution,[status(thm)],[f702,f627])).
% 7.86/1.70 fof(f787,plain,(
% 7.86/1.70 leq(tptp_float_0_0,sK23_skl)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f711,f409])).
% 7.86/1.70 fof(f788,plain,(
% 7.86/1.70 leq(tptp_float_0_0,sK24_skl)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f712,f409])).
% 7.86/1.70 fof(f789,plain,(
% 7.86/1.70 leq(sK23_skl,n2)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f713,f409])).
% 7.86/1.70 fof(f790,plain,(
% 7.86/1.70 leq(sK24_skl,pred(pv5))),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f714,f409])).
% 7.86/1.70 fof(f791,plain,(
% 7.86/1.70 ~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f715,f409])).
% 7.86/1.70 fof(f918,plain,(
% 7.86/1.70 ![X0]: (~leq(tptp_float_0_0,sK23_skl)|~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(u_defuse,sK23_skl,X0)=use)),
% 7.86/1.70 inference(resolution,[status(thm)],[f789,f710])).
% 7.86/1.70 fof(f919,plain,(
% 7.86/1.70 ![X0]: (~leq(tptp_float_0_0,sK23_skl)|~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(z_defuse,sK23_skl,X0)=use)),
% 7.86/1.70 inference(resolution,[status(thm)],[f789,f709])).
% 7.86/1.70 fof(f923,plain,(
% 7.86/1.70 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(u_defuse,sK23_skl,X0)=use)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f918,f787])).
% 7.86/1.70 fof(f924,plain,(
% 7.86/1.70 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(z_defuse,sK23_skl,X0)=use)),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f919,f787])).
% 7.86/1.70 fof(f1203,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,sK24_skl)|a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(resolution,[status(thm)],[f790,f924])).
% 7.86/1.70 fof(f1204,plain,(
% 7.86/1.70 ~leq(tptp_float_0_0,sK24_skl)|a_select3(u_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(resolution,[status(thm)],[f790,f923])).
% 7.86/1.70 fof(f1217,plain,(
% 7.86/1.70 ~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~use=use),
% 7.86/1.70 inference(backward_demodulation,[status(thm)],[f1218,f791])).
% 7.86/1.70 fof(f1218,plain,(
% 7.86/1.70 a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f1203,f788])).
% 7.86/1.70 fof(f1219,plain,(
% 7.86/1.70 a_select3(u_defuse,sK23_skl,sK24_skl)=use),
% 7.86/1.70 inference(forward_subsumption_resolution,[status(thm)],[f1204,f788])).
% 7.86/1.70 fof(f1220,plain,(
% 7.86/1.70 ~use=use|~use=use),
% 7.86/1.70 inference(forward_demodulation,[status(thm)],[f1219,f1217])).
% 7.86/1.70 fof(f1221,plain,(
% 7.86/1.70 ~use=use),
% 7.86/1.70 inference(duplicate_literals_removal,[status(thm)],[f1220])).
% 7.86/1.70 fof(f1222,plain,(
% 7.86/1.70 $false),
% 7.86/1.70 inference(trivial_equality_resolution,[status(thm)],[f1221])).
% 7.86/1.70 % SZS output end CNFRefutation for theBenchmark.p
% 7.86/1.72 % Elapsed time: 1.238926 seconds
% 7.86/1.72 % CPU time: 9.081990 seconds
% 7.86/1.72 % Total memory used: 155.849 MB
% 7.86/1.72 % Net memory used: 148.468 MB
%------------------------------------------------------------------------------