%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV099+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 : n002.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 10.33s 6.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV099+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.38 % Computer : n002.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 08:33:24 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 10.33/6.73 % Refutation found
% 10.33/6.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.33/6.73 % SZS output start CNFRefutation for theBenchmark
% 10.33/6.73 fof(f26,axiom,(
% 10.33/6.73 (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 10.33/6.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.33/6.73 fof(f27,axiom,(
% 10.33/6.73 (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 10.33/6.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.33/6.73 fof(f39,axiom,(
% 10.33/6.73 (! [X] : minus(X,n1) = pred(X) )),
% 10.33/6.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.33/6.73 fof(f53,conjecture,(
% 10.33/6.73 ( ( 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,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 ) ) )) ) ),
% 10.33/6.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.33/6.73 fof(f54,negated_conjecture,(
% 10.33/6.73 ~(( ( 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,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 ) ) )) ) )),
% 10.33/6.73 inference(negated_conjecture,[status(cth)],[f53])).
% 10.33/6.73 fof(f204,plain,(
% 10.33/6.73 ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f26])).
% 10.33/6.73 fof(f205,plain,(
% 10.33/6.73 ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f27])).
% 10.33/6.73 fof(f217,plain,(
% 10.33/6.73 ![X0]: (minus(X0,n1)=pred(X0))),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f39])).
% 10.33/6.73 fof(f251,plain,(
% 10.33/6.73 ((((((((((((((((((((((((((((((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,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)))))),
% 10.33/6.73 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 10.33/6.73 fof(f252,plain,(
% 10.33/6.73 (((((((((((((((((((((((((((((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,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)))),
% 10.33/6.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(C,sK23_skl),skolemize(D,sK24_skl)],[f251])).
% 10.33/6.73 fof(f253,plain,(
% 10.33/6.73 a_select2(rho_defuse,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f254,plain,(
% 10.33/6.73 a_select2(rho_defuse,n1)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f255,plain,(
% 10.33/6.73 a_select2(rho_defuse,n2)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f256,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f257,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n1)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f258,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n2)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f259,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n3)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f260,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n4)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f261,plain,(
% 10.33/6.73 a_select2(sigma_defuse,n5)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f262,plain,(
% 10.33/6.73 a_select3(u_defuse,n0,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f263,plain,(
% 10.33/6.73 a_select3(u_defuse,n1,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f264,plain,(
% 10.33/6.73 a_select3(u_defuse,n2,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f265,plain,(
% 10.33/6.73 a_select2(xinit_defuse,n3)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f266,plain,(
% 10.33/6.73 a_select2(xinit_defuse,n4)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f267,plain,(
% 10.33/6.73 a_select2(xinit_defuse,n5)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f268,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f269,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n1)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f270,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n2)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f271,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n3)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f272,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n4)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f273,plain,(
% 10.33/6.73 a_select2(xinit_mean_defuse,n5)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f274,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n0)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f275,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n1)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f276,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n2)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f277,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n3)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f278,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n4)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f279,plain,(
% 10.33/6.73 a_select2(xinit_noise_defuse,n5)=use),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f280,plain,(
% 10.33/6.73 leq(n0,pv5)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f281,plain,(
% 10.33/6.73 leq(pv5,minus(n999,n1))),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f282,plain,(
% 10.33/6.73 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(u_defuse,X0,X1)=use)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f283,plain,(
% 10.33/6.73 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,minus(pv5,n1))|a_select3(z_defuse,X0,X1)=use)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f284,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f285,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f286,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f287,plain,(
% 10.33/6.73 ~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))),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f288,plain,(
% 10.33/6.73 ~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),
% 10.33/6.73 inference(cnf_transformation,[status(thm)],[f252])).
% 10.33/6.73 fof(f370,plain,(
% 10.33/6.73 tptp_float_0_0=n0),
% 10.33/6.73 inference(backward_demodulation,[status(thm)],[f205,f204])).
% 10.33/6.73 fof(f385,plain,(
% 10.33/6.73 leq(pv5,pred(n999))),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f217,f281])).
% 10.33/6.73 fof(f386,plain,(
% 10.33/6.73 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(u_defuse,X0,X1)=use)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f217,f282])).
% 10.33/6.73 fof(f387,plain,(
% 10.33/6.73 ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pred(pv5))|a_select3(z_defuse,X0,X1)=use)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f217,f283])).
% 10.33/6.73 fof(f388,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f253,f284])).
% 10.33/6.73 fof(f389,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f254,f388])).
% 10.33/6.73 fof(f390,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f255,f389])).
% 10.33/6.73 fof(f391,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f256,f390])).
% 10.33/6.73 fof(f392,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f257,f391])).
% 10.33/6.73 fof(f393,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f258,f392])).
% 10.33/6.73 fof(f394,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f259,f393])).
% 10.33/6.73 fof(f395,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f260,f394])).
% 10.33/6.73 fof(f396,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f261,f395])).
% 10.33/6.73 fof(f397,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f262,f396])).
% 10.33/6.73 fof(f398,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f263,f397])).
% 10.33/6.73 fof(f399,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f264,f398])).
% 10.33/6.73 fof(f400,plain,(
% 10.33/6.73 ~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f265,f399])).
% 10.33/6.73 fof(f401,plain,(
% 10.33/6.73 ~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f266,f400])).
% 10.33/6.73 fof(f402,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f267,f401])).
% 10.33/6.73 fof(f403,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f268,f402])).
% 10.33/6.73 fof(f404,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f269,f403])).
% 10.33/6.73 fof(f405,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f270,f404])).
% 10.33/6.73 fof(f406,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f271,f405])).
% 10.33/6.73 fof(f407,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f272,f406])).
% 10.33/6.73 fof(f408,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f273,f407])).
% 10.33/6.73 fof(f409,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f274,f408])).
% 10.33/6.73 fof(f410,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f275,f409])).
% 10.33/6.73 fof(f411,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f276,f410])).
% 10.33/6.73 fof(f412,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f277,f411])).
% 10.33/6.73 fof(f413,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f278,f412])).
% 10.33/6.73 fof(f414,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f279,f413])).
% 10.33/6.73 fof(f415,plain,(
% 10.33/6.73 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f217,f414])).
% 10.33/6.73 fof(f416,plain,(
% 10.33/6.73 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 10.33/6.73 inference(duplicate_literals_removal,[status(thm)],[f415])).
% 10.33/6.73 fof(f417,plain,(
% 10.33/6.73 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 10.33/6.73 inference(trivial_equality_resolution,[status(thm)],[f416])).
% 10.33/6.73 fof(f418,plain,(
% 10.33/6.73 ~leq(pv5,pred(n999))|leq(n0,sK23_skl)),
% 10.33/6.73 inference(forward_subsumption_resolution,[status(thm)],[f417,f280])).
% 10.33/6.73 fof(f419,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.73 inference(forward_demodulation,[status(thm)],[f253,f285])).
% 10.33/6.73 fof(f420,plain,(
% 10.33/6.73 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f254,f419])).
% 10.33/6.74 fof(f421,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f255,f420])).
% 10.33/6.74 fof(f422,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f256,f421])).
% 10.33/6.74 fof(f423,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f257,f422])).
% 10.33/6.74 fof(f424,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f258,f423])).
% 10.33/6.74 fof(f425,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f259,f424])).
% 10.33/6.74 fof(f426,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f260,f425])).
% 10.33/6.74 fof(f427,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f261,f426])).
% 10.33/6.74 fof(f428,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f262,f427])).
% 10.33/6.74 fof(f429,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f263,f428])).
% 10.33/6.74 fof(f430,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f264,f429])).
% 10.33/6.74 fof(f431,plain,(
% 10.33/6.74 ~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f265,f430])).
% 10.33/6.74 fof(f432,plain,(
% 10.33/6.74 ~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f266,f431])).
% 10.33/6.74 fof(f433,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f267,f432])).
% 10.33/6.74 fof(f434,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f268,f433])).
% 10.33/6.74 fof(f435,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f269,f434])).
% 10.33/6.74 fof(f436,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f270,f435])).
% 10.33/6.74 fof(f437,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f271,f436])).
% 10.33/6.74 fof(f438,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f272,f437])).
% 10.33/6.74 fof(f439,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f273,f438])).
% 10.33/6.74 fof(f440,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f274,f439])).
% 10.33/6.74 fof(f441,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f275,f440])).
% 10.33/6.74 fof(f442,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f276,f441])).
% 10.33/6.74 fof(f443,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f277,f442])).
% 10.33/6.74 fof(f444,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f278,f443])).
% 10.33/6.74 fof(f445,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f279,f444])).
% 10.33/6.74 fof(f446,plain,(
% 10.33/6.74 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f217,f445])).
% 10.33/6.74 fof(f447,plain,(
% 10.33/6.74 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 10.33/6.74 inference(duplicate_literals_removal,[status(thm)],[f446])).
% 10.33/6.74 fof(f448,plain,(
% 10.33/6.74 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 10.33/6.74 inference(trivial_equality_resolution,[status(thm)],[f447])).
% 10.33/6.74 fof(f449,plain,(
% 10.33/6.74 ~leq(pv5,pred(n999))|leq(n0,sK24_skl)),
% 10.33/6.74 inference(forward_subsumption_resolution,[status(thm)],[f448,f280])).
% 10.33/6.74 fof(f450,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f253,f286])).
% 10.33/6.74 fof(f451,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f254,f450])).
% 10.33/6.74 fof(f452,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f255,f451])).
% 10.33/6.74 fof(f453,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.74 inference(forward_demodulation,[status(thm)],[f256,f452])).
% 10.33/6.74 fof(f454,plain,(
% 10.33/6.74 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f257,f453])).
% 10.33/6.75 fof(f455,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f258,f454])).
% 10.33/6.75 fof(f456,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f259,f455])).
% 10.33/6.75 fof(f457,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f260,f456])).
% 10.33/6.75 fof(f458,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f261,f457])).
% 10.33/6.75 fof(f459,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f262,f458])).
% 10.33/6.75 fof(f460,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f263,f459])).
% 10.33/6.75 fof(f461,plain,(
% 10.33/6.75 ~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f264,f460])).
% 10.33/6.75 fof(f462,plain,(
% 10.33/6.75 ~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f265,f461])).
% 10.33/6.75 fof(f463,plain,(
% 10.33/6.75 ~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f266,f462])).
% 10.33/6.75 fof(f464,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f267,f463])).
% 10.33/6.75 fof(f465,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f268,f464])).
% 10.33/6.75 fof(f466,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f269,f465])).
% 10.33/6.75 fof(f467,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f270,f466])).
% 10.33/6.75 fof(f468,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f271,f467])).
% 10.33/6.75 fof(f469,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f272,f468])).
% 10.33/6.75 fof(f470,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f273,f469])).
% 10.33/6.75 fof(f471,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f274,f470])).
% 10.33/6.75 fof(f472,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f275,f471])).
% 10.33/6.75 fof(f473,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f276,f472])).
% 10.33/6.75 fof(f474,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f277,f473])).
% 10.33/6.75 fof(f475,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f278,f474])).
% 10.33/6.75 fof(f476,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f279,f475])).
% 10.33/6.75 fof(f477,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f217,f476])).
% 10.33/6.75 fof(f478,plain,(
% 10.33/6.75 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 10.33/6.75 inference(duplicate_literals_removal,[status(thm)],[f477])).
% 10.33/6.75 fof(f479,plain,(
% 10.33/6.75 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 10.33/6.75 inference(trivial_equality_resolution,[status(thm)],[f478])).
% 10.33/6.75 fof(f480,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|leq(sK23_skl,n2)),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f479,f280])).
% 10.33/6.75 fof(f481,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f253,f287])).
% 10.33/6.75 fof(f482,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f254,f481])).
% 10.33/6.75 fof(f483,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f255,f482])).
% 10.33/6.75 fof(f484,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f256,f483])).
% 10.33/6.75 fof(f485,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f257,f484])).
% 10.33/6.75 fof(f486,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f258,f485])).
% 10.33/6.75 fof(f487,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f259,f486])).
% 10.33/6.75 fof(f488,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f260,f487])).
% 10.33/6.75 fof(f489,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f261,f488])).
% 10.33/6.75 fof(f490,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f262,f489])).
% 10.33/6.75 fof(f491,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f263,f490])).
% 10.33/6.75 fof(f492,plain,(
% 10.33/6.75 ~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f264,f491])).
% 10.33/6.75 fof(f493,plain,(
% 10.33/6.75 ~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f265,f492])).
% 10.33/6.75 fof(f494,plain,(
% 10.33/6.75 ~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f266,f493])).
% 10.33/6.75 fof(f495,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f267,f494])).
% 10.33/6.75 fof(f496,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f268,f495])).
% 10.33/6.75 fof(f497,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f269,f496])).
% 10.33/6.75 fof(f498,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f270,f497])).
% 10.33/6.75 fof(f499,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f271,f498])).
% 10.33/6.75 fof(f500,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f272,f499])).
% 10.33/6.75 fof(f501,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f273,f500])).
% 10.33/6.75 fof(f502,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f274,f501])).
% 10.33/6.75 fof(f503,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f275,f502])).
% 10.33/6.75 fof(f504,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f276,f503])).
% 10.33/6.75 fof(f505,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f277,f504])).
% 10.33/6.75 fof(f506,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f278,f505])).
% 10.33/6.75 fof(f507,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f279,f506])).
% 10.33/6.75 fof(f508,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f217,f507])).
% 10.33/6.75 fof(f509,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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))),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f217,f508])).
% 10.33/6.75 fof(f510,plain,(
% 10.33/6.75 ~use=use|~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 10.33/6.75 inference(duplicate_literals_removal,[status(thm)],[f509])).
% 10.33/6.75 fof(f511,plain,(
% 10.33/6.75 ~leq(n0,pv5)|~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 10.33/6.75 inference(trivial_equality_resolution,[status(thm)],[f510])).
% 10.33/6.75 fof(f512,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|leq(sK24_skl,pred(pv5))),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f511,f280])).
% 10.33/6.75 fof(f513,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f253,f288])).
% 10.33/6.75 fof(f514,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f254,f513])).
% 10.33/6.75 fof(f515,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f255,f514])).
% 10.33/6.75 fof(f516,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f256,f515])).
% 10.33/6.75 fof(f517,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f257,f516])).
% 10.33/6.75 fof(f518,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f258,f517])).
% 10.33/6.75 fof(f519,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f259,f518])).
% 10.33/6.75 fof(f520,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f260,f519])).
% 10.33/6.75 fof(f521,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f261,f520])).
% 10.33/6.75 fof(f522,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f262,f521])).
% 10.33/6.75 fof(f523,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f263,f522])).
% 10.33/6.75 fof(f524,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f264,f523])).
% 10.33/6.75 fof(f525,plain,(
% 10.33/6.75 ~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f265,f524])).
% 10.33/6.75 fof(f526,plain,(
% 10.33/6.75 ~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f266,f525])).
% 10.33/6.75 fof(f527,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f267,f526])).
% 10.33/6.75 fof(f528,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f268,f527])).
% 10.33/6.75 fof(f529,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f269,f528])).
% 10.33/6.75 fof(f530,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f270,f529])).
% 10.33/6.75 fof(f531,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f271,f530])).
% 10.33/6.75 fof(f532,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f272,f531])).
% 10.33/6.75 fof(f533,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f273,f532])).
% 10.33/6.75 fof(f534,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f274,f533])).
% 10.33/6.75 fof(f535,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f275,f534])).
% 10.33/6.75 fof(f536,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f276,f535])).
% 10.33/6.75 fof(f537,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f277,f536])).
% 10.33/6.75 fof(f538,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f278,f537])).
% 10.33/6.75 fof(f539,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f279,f538])).
% 10.33/6.75 fof(f540,plain,(
% 10.33/6.75 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f217,f539])).
% 10.33/6.75 fof(f541,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(duplicate_literals_removal,[status(thm)],[f540])).
% 10.33/6.75 fof(f542,plain,(
% 10.33/6.75 ~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),
% 10.33/6.75 inference(trivial_equality_resolution,[status(thm)],[f541])).
% 10.33/6.75 fof(f543,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f542,f280])).
% 10.33/6.75 fof(f584,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|leq(tptp_float_0_0,sK24_skl)),
% 10.33/6.75 inference(backward_demodulation,[status(thm)],[f370,f449])).
% 10.33/6.75 fof(f585,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|leq(tptp_float_0_0,sK23_skl)),
% 10.33/6.75 inference(backward_demodulation,[status(thm)],[f370,f418])).
% 10.33/6.75 fof(f586,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(backward_demodulation,[status(thm)],[f370,f387])).
% 10.33/6.75 fof(f587,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(backward_demodulation,[status(thm)],[f370,f386])).
% 10.33/6.75 fof(f660,plain,(
% 10.33/6.75 leq(tptp_float_0_0,sK24_skl)),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f584,f385])).
% 10.33/6.75 fof(f661,plain,(
% 10.33/6.75 leq(tptp_float_0_0,sK23_skl)),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f585,f385])).
% 10.33/6.75 fof(f662,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f370,f586])).
% 10.33/6.75 fof(f663,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(forward_demodulation,[status(thm)],[f370,f587])).
% 10.33/6.75 fof(f782,plain,(
% 10.33/6.75 leq(sK23_skl,n2)),
% 10.33/6.75 inference(resolution,[status(thm)],[f480,f385])).
% 10.33/6.75 fof(f915,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(resolution,[status(thm)],[f782,f663])).
% 10.33/6.75 fof(f916,plain,(
% 10.33/6.75 ![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)),
% 10.33/6.75 inference(resolution,[status(thm)],[f782,f662])).
% 10.33/6.75 fof(f920,plain,(
% 10.33/6.75 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(u_defuse,sK23_skl,X0)=use)),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f915,f661])).
% 10.33/6.75 fof(f921,plain,(
% 10.33/6.75 ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pred(pv5))|a_select3(z_defuse,sK23_skl,X0)=use)),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f916,f661])).
% 10.33/6.75 fof(f1061,plain,(
% 10.33/6.75 ~leq(tptp_float_0_0,sK24_skl)|a_select3(u_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 10.33/6.75 inference(resolution,[status(thm)],[f920,f512])).
% 10.33/6.75 fof(f1067,plain,(
% 10.33/6.75 ~leq(pv5,pred(n999))|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 10.33/6.75 inference(backward_subsumption_resolution,[status(thm)],[f543,f1068])).
% 10.33/6.75 fof(f1068,plain,(
% 10.33/6.75 a_select3(u_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f1061,f660])).
% 10.33/6.75 fof(f1069,plain,(
% 10.33/6.75 ~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f1067,f385])).
% 10.33/6.75 fof(f1070,plain,(
% 10.33/6.75 ~leq(tptp_float_0_0,sK24_skl)|a_select3(z_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 10.33/6.75 inference(resolution,[status(thm)],[f921,f512])).
% 10.33/6.75 fof(f1076,plain,(
% 10.33/6.75 a_select3(z_defuse,sK23_skl,sK24_skl)=use|~leq(pv5,pred(n999))),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f1070,f660])).
% 10.33/6.75 fof(f1315,plain,(
% 10.33/6.75 a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 10.33/6.75 inference(resolution,[status(thm)],[f1076,f385])).
% 10.33/6.75 fof(f1320,plain,(
% 10.33/6.75 $false),
% 10.33/6.75 inference(forward_subsumption_resolution,[status(thm)],[f1315,f1069])).
% 10.33/6.75 % SZS output end CNFRefutation for theBenchmark.p
% 10.33/6.77 % Elapsed time: 1.373127 seconds
% 10.33/6.77 % CPU time: 10.696090 seconds
% 10.33/6.77 % Total memory used: 185.892 MB
% 10.33/6.77 % Net memory used: 172.137 MB
%------------------------------------------------------------------------------