%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV096+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 : n019.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 8.39s 6.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV096+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.36 % Computer : n019.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 08:30:58 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.40 % Drodi V4.1.1
% 8.39/6.51 % Refutation found
% 8.39/6.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.39/6.51 % SZS output start CNFRefutation for theBenchmark
% 8.39/6.51 fof(f26,axiom,(
% 8.39/6.51 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 8.39/6.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.39/6.51 fof(f27,axiom,(
% 8.39/6.51 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 8.39/6.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.39/6.51 fof(f39,axiom,(
% 8.39/6.51 (! [X] : minus(X,n1) = pred(X) )),
% 8.39/6.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.39/6.51 fof(f53,conjecture,(
% 8.39/6.51 ( ( 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(pv5,minus(n999,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 ) ) )) ) ),
% 8.39/6.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.39/6.51 fof(f54,negated_conjecture,(
% 8.39/6.51 ~(( ( 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(pv5,minus(n999,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 ) ) )) ) )),
% 8.39/6.51 inference(negated_conjecture,[status(cth)],[f53])).
% 8.39/6.51 fof(f214,plain,(
% 8.39/6.51 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f26])).
% 8.39/6.51 fof(f215,plain,(
% 8.39/6.51 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f27])).
% 8.39/6.51 fof(f227,plain,(
% 8.39/6.51 ![X0]: (minus(X0,n1)=pred(X0))),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f39])).
% 8.39/6.51 fof(f261,plain,(
% 8.39/6.51 ((((((((((((((((((((((((((((((((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(pv5,minus(n999,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)))))),
% 8.39/6.51 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 8.39/6.51 fof(f262,plain,(
% 8.39/6.51 (((((((((((((((((((((((((((((((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(pv5,minus(n999,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)))),
% 8.39/6.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(C,sK23_skl),skolemize(D,sK24_skl)],[f261])).
% 8.39/6.51 fof(f263,plain,(
% 8.39/6.51 a_select2(rho_defuse,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f264,plain,(
% 8.39/6.51 a_select2(rho_defuse,n1)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f265,plain,(
% 8.39/6.51 a_select2(rho_defuse,n2)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f266,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f267,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n1)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f268,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n2)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f269,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n3)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f270,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n4)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f271,plain,(
% 8.39/6.51 a_select2(sigma_defuse,n5)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f272,plain,(
% 8.39/6.51 a_select3(u_defuse,n0,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f273,plain,(
% 8.39/6.51 a_select3(u_defuse,n1,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f274,plain,(
% 8.39/6.51 a_select3(u_defuse,n2,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f275,plain,(
% 8.39/6.51 a_select2(xinit_defuse,n3)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f276,plain,(
% 8.39/6.51 a_select2(xinit_defuse,n4)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f277,plain,(
% 8.39/6.51 a_select2(xinit_defuse,n5)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f278,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f279,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n1)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f280,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n2)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f281,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n3)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f282,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n4)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f283,plain,(
% 8.39/6.51 a_select2(xinit_mean_defuse,n5)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f284,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n0)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f285,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n1)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f286,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n2)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f287,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n3)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f288,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n4)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f289,plain,(
% 8.39/6.51 a_select2(xinit_noise_defuse,n5)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f290,plain,(
% 8.39/6.51 leq(n0,pv5)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f292,plain,(
% 8.39/6.51 leq(pv5,minus(n999,n1))),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f294,plain,(
% 8.39/6.51 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(u_defuse,X0,X1)=use)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f295,plain,(
% 8.39/6.51 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(z_defuse,X0,X1)=use)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f296,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f297,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f298,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f299,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f300,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.51 inference(cnf_transformation,[status(thm)],[f262])).
% 8.39/6.51 fof(f393,plain,(
% 8.39/6.51 tptp_float_0_0=n0),
% 8.39/6.51 inference(backward_demodulation,[status(thm)],[f215,f214])).
% 8.39/6.51 fof(f408,plain,(
% 8.39/6.51 leq(pv5,pred(n999))),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f227,f292])).
% 8.39/6.51 fof(f410,plain,(
% 8.39/6.51 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(u_defuse,X0,X1)=use)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f227,f294])).
% 8.39/6.51 fof(f411,plain,(
% 8.39/6.51 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(z_defuse,X0,X1)=use)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f227,f295])).
% 8.39/6.51 fof(f412,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f263,f296])).
% 8.39/6.51 fof(f413,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f264,f412])).
% 8.39/6.51 fof(f414,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f265,f413])).
% 8.39/6.51 fof(f415,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f266,f414])).
% 8.39/6.51 fof(f416,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f267,f415])).
% 8.39/6.51 fof(f417,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f268,f416])).
% 8.39/6.51 fof(f418,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f269,f417])).
% 8.39/6.51 fof(f419,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f270,f418])).
% 8.39/6.51 fof(f420,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f271,f419])).
% 8.39/6.51 fof(f421,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f272,f420])).
% 8.39/6.51 fof(f422,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f273,f421])).
% 8.39/6.51 fof(f423,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f274,f422])).
% 8.39/6.51 fof(f424,plain,(
% 8.39/6.51 ~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f275,f423])).
% 8.39/6.51 fof(f425,plain,(
% 8.39/6.51 ~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f276,f424])).
% 8.39/6.51 fof(f426,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f277,f425])).
% 8.39/6.51 fof(f427,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f278,f426])).
% 8.39/6.51 fof(f428,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f279,f427])).
% 8.39/6.51 fof(f429,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f280,f428])).
% 8.39/6.51 fof(f430,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f281,f429])).
% 8.39/6.51 fof(f431,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f282,f430])).
% 8.39/6.51 fof(f432,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f283,f431])).
% 8.39/6.51 fof(f433,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f284,f432])).
% 8.39/6.51 fof(f434,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f285,f433])).
% 8.39/6.51 fof(f435,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f286,f434])).
% 8.39/6.51 fof(f436,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f287,f435])).
% 8.39/6.51 fof(f437,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f288,f436])).
% 8.39/6.51 fof(f438,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f289,f437])).
% 8.39/6.51 fof(f439,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f227,f438])).
% 8.39/6.51 fof(f440,plain,(
% 8.39/6.51 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(duplicate_literals_removal,[status(thm)],[f439])).
% 8.39/6.51 fof(f441,plain,(
% 8.39/6.51 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(trivial_equality_resolution,[status(thm)],[f440])).
% 8.39/6.51 fof(f442,plain,(
% 8.39/6.51 ~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 8.39/6.51 inference(forward_subsumption_resolution,[status(thm)],[f441,f290])).
% 8.39/6.51 fof(f443,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f263,f297])).
% 8.39/6.51 fof(f444,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f264,f443])).
% 8.39/6.51 fof(f445,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f265,f444])).
% 8.39/6.51 fof(f446,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f266,f445])).
% 8.39/6.51 fof(f447,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f267,f446])).
% 8.39/6.51 fof(f448,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f268,f447])).
% 8.39/6.51 fof(f449,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f269,f448])).
% 8.39/6.51 fof(f450,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f270,f449])).
% 8.39/6.51 fof(f451,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f271,f450])).
% 8.39/6.51 fof(f452,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f272,f451])).
% 8.39/6.51 fof(f453,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f273,f452])).
% 8.39/6.51 fof(f454,plain,(
% 8.39/6.51 ~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f274,f453])).
% 8.39/6.51 fof(f455,plain,(
% 8.39/6.51 ~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f275,f454])).
% 8.39/6.51 fof(f456,plain,(
% 8.39/6.51 ~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f276,f455])).
% 8.39/6.51 fof(f457,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f277,f456])).
% 8.39/6.51 fof(f458,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f278,f457])).
% 8.39/6.51 fof(f459,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f279,f458])).
% 8.39/6.51 fof(f460,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f280,f459])).
% 8.39/6.51 fof(f461,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f281,f460])).
% 8.39/6.51 fof(f462,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.51 inference(forward_demodulation,[status(thm)],[f282,f461])).
% 8.39/6.51 fof(f463,plain,(
% 8.39/6.51 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f283,f462])).
% 8.39/6.52 fof(f464,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f284,f463])).
% 8.39/6.52 fof(f465,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f285,f464])).
% 8.39/6.52 fof(f466,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f286,f465])).
% 8.39/6.52 fof(f467,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f287,f466])).
% 8.39/6.52 fof(f468,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f288,f467])).
% 8.39/6.52 fof(f469,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f289,f468])).
% 8.39/6.52 fof(f470,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f227,f469])).
% 8.39/6.52 fof(f471,plain,(
% 8.39/6.52 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(duplicate_literals_removal,[status(thm)],[f470])).
% 8.39/6.52 fof(f472,plain,(
% 8.39/6.52 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(trivial_equality_resolution,[status(thm)],[f471])).
% 8.39/6.52 fof(f473,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f472,f290])).
% 8.39/6.52 fof(f474,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f263,f298])).
% 8.39/6.52 fof(f475,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f264,f474])).
% 8.39/6.52 fof(f476,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f265,f475])).
% 8.39/6.52 fof(f477,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f266,f476])).
% 8.39/6.52 fof(f478,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f267,f477])).
% 8.39/6.52 fof(f479,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f268,f478])).
% 8.39/6.52 fof(f480,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f269,f479])).
% 8.39/6.52 fof(f481,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f270,f480])).
% 8.39/6.52 fof(f482,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f271,f481])).
% 8.39/6.52 fof(f483,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f272,f482])).
% 8.39/6.52 fof(f484,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f273,f483])).
% 8.39/6.52 fof(f485,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f274,f484])).
% 8.39/6.52 fof(f486,plain,(
% 8.39/6.52 ~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f275,f485])).
% 8.39/6.52 fof(f487,plain,(
% 8.39/6.52 ~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f276,f486])).
% 8.39/6.52 fof(f488,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f277,f487])).
% 8.39/6.52 fof(f489,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f278,f488])).
% 8.39/6.52 fof(f490,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f279,f489])).
% 8.39/6.52 fof(f491,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f280,f490])).
% 8.39/6.52 fof(f492,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f281,f491])).
% 8.39/6.52 fof(f493,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f282,f492])).
% 8.39/6.52 fof(f494,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f283,f493])).
% 8.39/6.52 fof(f495,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f284,f494])).
% 8.39/6.52 fof(f496,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f285,f495])).
% 8.39/6.52 fof(f497,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f286,f496])).
% 8.39/6.52 fof(f498,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f287,f497])).
% 8.39/6.52 fof(f499,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f288,f498])).
% 8.39/6.52 fof(f500,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f289,f499])).
% 8.39/6.52 fof(f501,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f227,f500])).
% 8.39/6.52 fof(f502,plain,(
% 8.39/6.52 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(duplicate_literals_removal,[status(thm)],[f501])).
% 8.39/6.52 fof(f503,plain,(
% 8.39/6.52 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(trivial_equality_resolution,[status(thm)],[f502])).
% 8.39/6.52 fof(f504,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f503,f290])).
% 8.39/6.52 fof(f505,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f263,f299])).
% 8.39/6.52 fof(f506,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f264,f505])).
% 8.39/6.52 fof(f507,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f265,f506])).
% 8.39/6.52 fof(f508,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f266,f507])).
% 8.39/6.52 fof(f509,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f267,f508])).
% 8.39/6.52 fof(f510,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f268,f509])).
% 8.39/6.52 fof(f511,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f269,f510])).
% 8.39/6.52 fof(f512,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f270,f511])).
% 8.39/6.52 fof(f513,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f271,f512])).
% 8.39/6.52 fof(f514,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f272,f513])).
% 8.39/6.52 fof(f515,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f273,f514])).
% 8.39/6.52 fof(f516,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f274,f515])).
% 8.39/6.52 fof(f517,plain,(
% 8.39/6.52 ~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f275,f516])).
% 8.39/6.52 fof(f518,plain,(
% 8.39/6.52 ~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f276,f517])).
% 8.39/6.52 fof(f519,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f277,f518])).
% 8.39/6.52 fof(f520,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f278,f519])).
% 8.39/6.52 fof(f521,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f279,f520])).
% 8.39/6.52 fof(f522,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f280,f521])).
% 8.39/6.52 fof(f523,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f281,f522])).
% 8.39/6.52 fof(f524,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f282,f523])).
% 8.39/6.52 fof(f525,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f283,f524])).
% 8.39/6.52 fof(f526,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f284,f525])).
% 8.39/6.52 fof(f527,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f285,f526])).
% 8.39/6.52 fof(f528,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f286,f527])).
% 8.39/6.52 fof(f529,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f287,f528])).
% 8.39/6.52 fof(f530,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f288,f529])).
% 8.39/6.52 fof(f531,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f289,f530])).
% 8.39/6.52 fof(f532,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|leq(sK24_skl,minus(pv5,n1))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f227,f531])).
% 8.39/6.52 fof(f533,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f227,f532])).
% 8.39/6.52 fof(f534,plain,(
% 8.39/6.52 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 8.39/6.52 inference(duplicate_literals_removal,[status(thm)],[f533])).
% 8.39/6.52 fof(f535,plain,(
% 8.39/6.52 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 8.39/6.52 inference(trivial_equality_resolution,[status(thm)],[f534])).
% 8.39/6.52 fof(f536,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f535,f290])).
% 8.39/6.52 fof(f537,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f263,f300])).
% 8.39/6.52 fof(f538,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f264,f537])).
% 8.39/6.52 fof(f539,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f265,f538])).
% 8.39/6.52 fof(f540,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f266,f539])).
% 8.39/6.52 fof(f541,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f267,f540])).
% 8.39/6.52 fof(f542,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f268,f541])).
% 8.39/6.52 fof(f543,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f269,f542])).
% 8.39/6.52 fof(f544,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f270,f543])).
% 8.39/6.52 fof(f545,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f271,f544])).
% 8.39/6.52 fof(f546,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f272,f545])).
% 8.39/6.52 fof(f547,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f273,f546])).
% 8.39/6.52 fof(f548,plain,(
% 8.39/6.52 ~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f274,f547])).
% 8.39/6.52 fof(f549,plain,(
% 8.39/6.52 ~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f275,f548])).
% 8.39/6.52 fof(f550,plain,(
% 8.39/6.52 ~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f276,f549])).
% 8.39/6.52 fof(f551,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f277,f550])).
% 8.39/6.52 fof(f552,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f278,f551])).
% 8.39/6.52 fof(f553,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f279,f552])).
% 8.39/6.52 fof(f554,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f280,f553])).
% 8.39/6.52 fof(f555,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f281,f554])).
% 8.39/6.52 fof(f556,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f282,f555])).
% 8.39/6.52 fof(f557,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f283,f556])).
% 8.39/6.52 fof(f558,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f284,f557])).
% 8.39/6.52 fof(f559,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f285,f558])).
% 8.39/6.52 fof(f560,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f286,f559])).
% 8.39/6.52 fof(f561,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f287,f560])).
% 8.39/6.52 fof(f562,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f288,f561])).
% 8.39/6.52 fof(f563,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,minus(n999,n1))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f289,f562])).
% 8.39/6.52 fof(f564,plain,(
% 8.39/6.52 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(pv5,pred(n999))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f227,f563])).
% 8.39/6.52 fof(f565,plain,(
% 8.39/6.52 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(duplicate_literals_removal,[status(thm)],[f564])).
% 8.39/6.52 fof(f566,plain,(
% 8.39/6.52 ~leq(n0,pv5)|~leq(pv5,pred(n999))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(trivial_equality_resolution,[status(thm)],[f565])).
% 8.39/6.52 fof(f567,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f566,f290])).
% 8.39/6.52 fof(f615,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|leq(tptp_float_0_0,sK24_skl)),
% 8.39/6.52 inference(backward_demodulation,[status(thm)],[f393,f473])).
% 8.39/6.52 fof(f616,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|leq(tptp_float_0_0,sK23_skl)),
% 8.39/6.52 inference(backward_demodulation,[status(thm)],[f393,f442])).
% 8.39/6.52 fof(f617,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(backward_demodulation,[status(thm)],[f393,f411])).
% 8.39/6.52 fof(f618,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(backward_demodulation,[status(thm)],[f393,f410])).
% 8.39/6.52 fof(f694,plain,(
% 8.39/6.52 leq(tptp_float_0_0,sK24_skl)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f615,f408])).
% 8.39/6.52 fof(f695,plain,(
% 8.39/6.52 leq(tptp_float_0_0,sK23_skl)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f616,f408])).
% 8.39/6.52 fof(f696,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f393,f617])).
% 8.39/6.52 fof(f697,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(forward_demodulation,[status(thm)],[f393,f618])).
% 8.39/6.52 fof(f817,plain,(
% 8.39/6.52 leq(sK23_skl,n2)),
% 8.39/6.52 inference(resolution,[status(thm)],[f504,f408])).
% 8.39/6.52 fof(f1011,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(resolution,[status(thm)],[f817,f697])).
% 8.39/6.52 fof(f1012,plain,(
% 8.39/6.52 ![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)),
% 8.39/6.52 inference(resolution,[status(thm)],[f817,f696])).
% 8.39/6.52 fof(f1022,plain,(
% 8.39/6.52 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(u_defuse,sK23_skl,X0)=use)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f1011,f695])).
% 8.39/6.52 fof(f1023,plain,(
% 8.39/6.52 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(z_defuse,sK23_skl,X0)=use)),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f1012,f695])).
% 8.39/6.52 fof(f1108,plain,(
% 8.39/6.52 ~leq(tptp_float_0_0,sK24_skl)|a_select3(u_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 8.39/6.52 inference(resolution,[status(thm)],[f1022,f536])).
% 8.39/6.52 fof(f1114,plain,(
% 8.39/6.52 ~leq(pv5,pred(n999))|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(backward_subsumption_resolution,[status(thm)],[f567,f1115])).
% 8.39/6.52 fof(f1115,plain,(
% 8.39/6.52 a_select3(u_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f1108,f694])).
% 8.39/6.52 fof(f1116,plain,(
% 8.39/6.52 ~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.52 inference(forward_subsumption_resolution,[status(thm)],[f1114,f408])).
% 8.39/6.53 fof(f1117,plain,(
% 8.39/6.53 ~leq(tptp_float_0_0,sK24_skl)|a_select3(z_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 8.39/6.53 inference(resolution,[status(thm)],[f1023,f536])).
% 8.39/6.53 fof(f1123,plain,(
% 8.39/6.53 a_select3(z_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 8.39/6.53 inference(forward_subsumption_resolution,[status(thm)],[f1117,f694])).
% 8.39/6.53 fof(f1302,plain,(
% 8.39/6.53 a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 8.39/6.53 inference(resolution,[status(thm)],[f1123,f408])).
% 8.39/6.53 fof(f1307,plain,(
% 8.39/6.53 $false),
% 8.39/6.53 inference(forward_subsumption_resolution,[status(thm)],[f1302,f1116])).
% 8.39/6.53 % SZS output end CNFRefutation for theBenchmark.p
% 8.39/6.54 % Elapsed time: 1.153192 seconds
% 8.39/6.54 % CPU time: 8.866628 seconds
% 8.39/6.54 % Total memory used: 177.392 MB
% 8.39/6.54 % Net memory used: 166.004 MB
%------------------------------------------------------------------------------