Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SWV098+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 : n014.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 6.20s 11.67s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWV098+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.08/10.78  % Computer : n014.cluster.edu
% 0.08/10.78  % Model    : x86_64 x86_64
% 0.08/10.78  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.78  % Memory   : 8046.5625MB
% 0.08/10.78  % OS       : Linux 6.8.0-71-generic
% 0.08/10.78  % CPULimit : 300
% 0.08/10.78  % WCLimit  : 300
% 0.08/10.78  % DateTime : Mon Sep 21 08:30:46 UTC 2026
% 0.08/10.79  % CPUTime  : 
% 0.13/10.80  % Drodi V4.1.1
% 6.20/11.67  % Refutation found
% 6.20/11.67  % SZS status Theorem for theBenchmark: Theorem is valid
% 6.20/11.67  % SZS output start CNFRefutation for theBenchmark
% 6.20/11.67  fof(f26,axiom,(
% 6.20/11.67    (! [Body] : sum(n0,tptp_minus_1,Body) = n0 )),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f27,axiom,(
% 6.20/11.67    (! [Body] : tptp_float_0_0 = sum(n0,tptp_minus_1,Body) )),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f30,axiom,(
% 6.20/11.67    (! [X] : plus(n1,X) = succ(X) )),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f39,axiom,(
% 6.20/11.67    (! [X] : minus(X,n1) = pred(X) )),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f40,axiom,(
% 6.20/11.67    (! [X] : pred(succ(X)) = X )),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f53,conjecture,(
% 6.20/11.67    ( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(pv5,minus(n999,n1))& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,pv5) )=> ( a_select3(u_defuse,A,B) = use& a_select3(z_defuse,A,B) = use ) ))& (! [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 ) ) ))=> ( 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& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,n2)& leq(F,minus(plus(n1,pv5),n1)) )=> ( a_select3(u_defuse,E,F) = use& a_select3(z_defuse,E,F) = use ) ) )) ) ),
% 6.20/11.67    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.20/11.67  fof(f54,negated_conjecture,(
% 6.20/11.67    ~(( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = use& a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_defuse,n5) = use& a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& leq(n0,pv5)& leq(pv5,minus(n999,n1))& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,pv5) )=> ( a_select3(u_defuse,A,B) = use& a_select3(z_defuse,A,B) = use ) ))& (! [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 ) ) ))=> ( 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& (! [E,F] :( ( leq(n0,E)& leq(n0,F)& leq(E,n2)& leq(F,minus(plus(n1,pv5),n1)) )=> ( a_select3(u_defuse,E,F) = use& a_select3(z_defuse,E,F) = use ) ) )) ) )),
% 6.20/11.67    inference(negated_conjecture,[status(cth)],[f53])).
% 6.20/11.67  fof(f204,plain,(
% 6.20/11.67    ![X0]: (sum(n0,tptp_minus_1,X0)=n0)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f26])).
% 6.20/11.67  fof(f205,plain,(
% 6.20/11.67    ![X0]: (tptp_float_0_0=sum(n0,tptp_minus_1,X0))),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f27])).
% 6.20/11.67  fof(f208,plain,(
% 6.20/11.67    ![X0]: (plus(n1,X0)=succ(X0))),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f30])).
% 6.20/11.67  fof(f217,plain,(
% 6.20/11.67    ![X0]: (minus(X0,n1)=pred(X0))),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f39])).
% 6.20/11.67  fof(f218,plain,(
% 6.20/11.67    ![X0]: (pred(succ(X0))=X0)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f40])).
% 6.20/11.67  fof(f251,plain,(
% 6.20/11.67    (((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,minus(n999,n1)))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,pv5))|(a_select3(u_defuse,A,B)=use&a_select3(z_defuse,A,B)=use))))&(![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))))&(((((((((((((((((((((((((((~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)|(?[E,F]: ((((leq(n0,E)&leq(n0,F))&leq(E,n2))&leq(F,minus(plus(n1,pv5),n1)))&(~a_select3(u_defuse,E,F)=use|~a_select3(z_defuse,E,F)=use)))))),
% 6.20/11.67    inference(pre_NNF_transformation,[status(thm)],[f54])).
% 6.20/11.67  fof(f252,plain,(
% 6.20/11.67    ((((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=use)&a_select2(sigma_defuse,n0)=use)&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_defuse,n5)=use)&a_select3(u_defuse,n0,n0)=use)&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&a_select2(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&leq(n0,pv5))&leq(pv5,minus(n999,n1)))&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,pv5))|(a_select3(u_defuse,A,B)=use&a_select3(z_defuse,A,B)=use))))&(![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))))&(((((((((((((((((((((((((((~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,sK23_skl)&leq(n0,sK24_skl))&leq(sK23_skl,n2))&leq(sK24_skl,minus(plus(n1,pv5),n1)))&(~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use)))),
% 6.20/11.67    inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(E,sK23_skl),skolemize(F,sK24_skl)],[f251])).
% 6.20/11.67  fof(f253,plain,(
% 6.20/11.67    a_select2(rho_defuse,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f254,plain,(
% 6.20/11.67    a_select2(rho_defuse,n1)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f255,plain,(
% 6.20/11.67    a_select2(rho_defuse,n2)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f256,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f257,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n1)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f258,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n2)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f259,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n3)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f260,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n4)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f261,plain,(
% 6.20/11.67    a_select2(sigma_defuse,n5)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f262,plain,(
% 6.20/11.67    a_select3(u_defuse,n0,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f263,plain,(
% 6.20/11.67    a_select3(u_defuse,n1,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f264,plain,(
% 6.20/11.67    a_select3(u_defuse,n2,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f265,plain,(
% 6.20/11.67    a_select2(xinit_defuse,n3)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f266,plain,(
% 6.20/11.67    a_select2(xinit_defuse,n4)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f267,plain,(
% 6.20/11.67    a_select2(xinit_defuse,n5)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f268,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f269,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n1)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f270,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n2)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f271,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n3)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f272,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n4)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f273,plain,(
% 6.20/11.67    a_select2(xinit_mean_defuse,n5)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f274,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n0)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f275,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n1)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f276,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n2)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f277,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n3)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f278,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n4)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f279,plain,(
% 6.20/11.67    a_select2(xinit_noise_defuse,n5)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f282,plain,(
% 6.20/11.67    ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(u_defuse,X0,X1)=use)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f283,plain,(
% 6.20/11.67    ![X0,X1]: (~leq(n0,X0)|~leq(n0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(z_defuse,X0,X1)=use)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f286,plain,(
% 6.20/11.67    ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f287,plain,(
% 6.20/11.67    ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f288,plain,(
% 6.20/11.67    ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f289,plain,(
% 6.20/11.67    ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f290,plain,(
% 6.20/11.67    ~a_select2(rho_defuse,n0)=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.67    inference(cnf_transformation,[status(thm)],[f252])).
% 6.20/11.67  fof(f372,plain,(
% 6.20/11.67    tptp_float_0_0=n0),
% 6.20/11.67    inference(backward_demodulation,[status(thm)],[f205,f204])).
% 6.20/11.67  fof(f390,plain,(
% 6.20/11.67    ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f253,f286])).
% 6.20/11.67  fof(f391,plain,(
% 6.20/11.67    ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f254,f390])).
% 6.20/11.67  fof(f392,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f255,f391])).
% 6.20/11.67  fof(f393,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f256,f392])).
% 6.20/11.67  fof(f394,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f257,f393])).
% 6.20/11.67  fof(f395,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f258,f394])).
% 6.20/11.67  fof(f396,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f259,f395])).
% 6.20/11.67  fof(f397,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f260,f396])).
% 6.20/11.67  fof(f398,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f261,f397])).
% 6.20/11.67  fof(f399,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f262,f398])).
% 6.20/11.67  fof(f400,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f263,f399])).
% 6.20/11.67  fof(f401,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f264,f400])).
% 6.20/11.67  fof(f402,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f265,f401])).
% 6.20/11.67  fof(f403,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f266,f402])).
% 6.20/11.67  fof(f404,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f267,f403])).
% 6.20/11.67  fof(f405,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f268,f404])).
% 6.20/11.67  fof(f406,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f269,f405])).
% 6.20/11.67  fof(f407,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f270,f406])).
% 6.20/11.67  fof(f408,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f271,f407])).
% 6.20/11.67  fof(f409,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f272,f408])).
% 6.20/11.67  fof(f410,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f273,f409])).
% 6.20/11.67  fof(f411,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f274,f410])).
% 6.20/11.67  fof(f412,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f275,f411])).
% 6.20/11.67  fof(f413,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f276,f412])).
% 6.20/11.67  fof(f414,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f277,f413])).
% 6.20/11.67  fof(f415,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f278,f414])).
% 6.20/11.67  fof(f416,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f279,f415])).
% 6.20/11.67  fof(f417,plain,(
% 6.20/11.67    ~use=use|leq(n0,sK23_skl)),
% 6.20/11.67    inference(duplicate_literals_removal,[status(thm)],[f416])).
% 6.20/11.67  fof(f418,plain,(
% 6.20/11.67    leq(n0,sK23_skl)),
% 6.20/11.67    inference(trivial_equality_resolution,[status(thm)],[f417])).
% 6.20/11.67  fof(f419,plain,(
% 6.20/11.67    ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f253,f287])).
% 6.20/11.67  fof(f420,plain,(
% 6.20/11.67    ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f254,f419])).
% 6.20/11.67  fof(f421,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f255,f420])).
% 6.20/11.67  fof(f422,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f256,f421])).
% 6.20/11.67  fof(f423,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f257,f422])).
% 6.20/11.67  fof(f424,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f258,f423])).
% 6.20/11.67  fof(f425,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f259,f424])).
% 6.20/11.67  fof(f426,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f260,f425])).
% 6.20/11.67  fof(f427,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.67    inference(forward_demodulation,[status(thm)],[f261,f426])).
% 6.20/11.67  fof(f428,plain,(
% 6.20/11.67    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f262,f427])).
% 6.20/11.68  fof(f429,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f263,f428])).
% 6.20/11.68  fof(f430,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f264,f429])).
% 6.20/11.68  fof(f431,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f265,f430])).
% 6.20/11.68  fof(f432,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f266,f431])).
% 6.20/11.68  fof(f433,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f267,f432])).
% 6.20/11.68  fof(f434,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f268,f433])).
% 6.20/11.68  fof(f435,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f269,f434])).
% 6.20/11.68  fof(f436,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f270,f435])).
% 6.20/11.68  fof(f437,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f271,f436])).
% 6.20/11.68  fof(f438,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f272,f437])).
% 6.20/11.68  fof(f439,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f273,f438])).
% 6.20/11.68  fof(f440,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f274,f439])).
% 6.20/11.68  fof(f441,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f275,f440])).
% 6.20/11.68  fof(f442,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f276,f441])).
% 6.20/11.68  fof(f443,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f277,f442])).
% 6.20/11.68  fof(f444,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(xinit_noise_defuse,n5)=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f278,f443])).
% 6.20/11.68  fof(f445,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f279,f444])).
% 6.20/11.68  fof(f446,plain,(
% 6.20/11.68    ~use=use|leq(n0,sK24_skl)),
% 6.20/11.68    inference(duplicate_literals_removal,[status(thm)],[f445])).
% 6.20/11.68  fof(f447,plain,(
% 6.20/11.68    leq(n0,sK24_skl)),
% 6.20/11.68    inference(trivial_equality_resolution,[status(thm)],[f446])).
% 6.20/11.68  fof(f448,plain,(
% 6.20/11.68    ~use=use|~a_select2(rho_defuse,n1)=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f253,f288])).
% 6.20/11.68  fof(f449,plain,(
% 6.20/11.68    ~use=use|~use=use|~a_select2(rho_defuse,n2)=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f254,f448])).
% 6.20/11.68  fof(f450,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f255,f449])).
% 6.20/11.68  fof(f451,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f256,f450])).
% 6.20/11.68  fof(f452,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f257,f451])).
% 6.20/11.68  fof(f453,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f258,f452])).
% 6.20/11.68  fof(f454,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f259,f453])).
% 6.20/11.68  fof(f455,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(sigma_defuse,n5)=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.68    inference(forward_demodulation,[status(thm)],[f260,f454])).
% 6.20/11.68  fof(f456,plain,(
% 6.20/11.68    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(xinit_mean_defuse,n0)=use|~a_select2(xinit_mean_defuse,n1)=use|~a_select2(xinit_mean_defuse,n2)=use|~a_select2(xinit_mean_defuse,n3)=use|~a_select2(xinit_mean_defuse,n4)=use|~a_select2(xinit_mean_defuse,n5)=use|~a_select2(xinit_noise_defuse,n0)=use|~a_select2(xinit_noise_defuse,n1)=use|~a_select2(xinit_noise_defuse,n2)=use|~a_select2(xinit_noise_defuse,n3)=use|~a_select2(xinit_noise_defuse,n4)=use|~a_select2(xinit_noise_defuse,n5)=use|leq(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f261,f455])).
% 6.20/11.69  fof(f457,plain,(
% 6.20/11.69    ~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f262,f456])).
% 6.20/11.69  fof(f458,plain,(
% 6.20/11.69    ~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f263,f457])).
% 6.20/11.69  fof(f459,plain,(
% 6.20/11.69    ~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f264,f458])).
% 6.20/11.69  fof(f460,plain,(
% 6.20/11.69    ~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f265,f459])).
% 6.20/11.69  fof(f461,plain,(
% 6.20/11.69    ~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f266,f460])).
% 6.20/11.69  fof(f462,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f267,f461])).
% 6.20/11.69  fof(f463,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f268,f462])).
% 6.20/11.69  fof(f464,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f269,f463])).
% 6.20/11.69  fof(f465,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f270,f464])).
% 6.20/11.69  fof(f466,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f271,f465])).
% 6.20/11.69  fof(f467,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f272,f466])).
% 6.20/11.69  fof(f468,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f273,f467])).
% 6.20/11.69  fof(f469,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f274,f468])).
% 6.20/11.69  fof(f470,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f275,f469])).
% 6.20/11.69  fof(f471,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f276,f470])).
% 6.20/11.69  fof(f472,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f277,f471])).
% 6.20/11.69  fof(f473,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f278,f472])).
% 6.20/11.69  fof(f474,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK23_skl,n2)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f279,f473])).
% 6.20/11.69  fof(f475,plain,(
% 6.20/11.69    ~use=use|leq(sK23_skl,n2)),
% 6.20/11.69    inference(duplicate_literals_removal,[status(thm)],[f474])).
% 6.20/11.69  fof(f476,plain,(
% 6.20/11.69    leq(sK23_skl,n2)),
% 6.20/11.69    inference(trivial_equality_resolution,[status(thm)],[f475])).
% 6.20/11.69  fof(f477,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f253,f289])).
% 6.20/11.69  fof(f478,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f254,f477])).
% 6.20/11.69  fof(f479,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f255,f478])).
% 6.20/11.69  fof(f480,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f256,f479])).
% 6.20/11.69  fof(f481,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f257,f480])).
% 6.20/11.69  fof(f482,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f258,f481])).
% 6.20/11.69  fof(f483,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f259,f482])).
% 6.20/11.69  fof(f484,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f260,f483])).
% 6.20/11.69  fof(f485,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f261,f484])).
% 6.20/11.69  fof(f486,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f262,f485])).
% 6.20/11.69  fof(f487,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f263,f486])).
% 6.20/11.69  fof(f488,plain,(
% 6.20/11.69    ~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f264,f487])).
% 6.20/11.69  fof(f489,plain,(
% 6.20/11.69    ~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f265,f488])).
% 6.20/11.69  fof(f490,plain,(
% 6.20/11.69    ~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f266,f489])).
% 6.20/11.69  fof(f491,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f267,f490])).
% 6.20/11.69  fof(f492,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f268,f491])).
% 6.20/11.69  fof(f493,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f269,f492])).
% 6.20/11.69  fof(f494,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f270,f493])).
% 6.20/11.69  fof(f495,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f271,f494])).
% 6.20/11.69  fof(f496,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f272,f495])).
% 6.20/11.69  fof(f497,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f273,f496])).
% 6.20/11.69  fof(f498,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f274,f497])).
% 6.20/11.69  fof(f499,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f275,f498])).
% 6.20/11.69  fof(f500,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f276,f499])).
% 6.20/11.69  fof(f501,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f277,f500])).
% 6.20/11.69  fof(f502,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f278,f501])).
% 6.20/11.69  fof(f503,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,minus(plus(n1,pv5),n1))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f279,f502])).
% 6.20/11.69  fof(f504,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,pred(plus(n1,pv5)))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f217,f503])).
% 6.20/11.69  fof(f505,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,pred(succ(pv5)))),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f208,f504])).
% 6.20/11.69  fof(f506,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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(sK24_skl,pv5)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f218,f505])).
% 6.20/11.69  fof(f507,plain,(
% 6.20/11.69    ~use=use|leq(sK24_skl,pv5)),
% 6.20/11.69    inference(duplicate_literals_removal,[status(thm)],[f506])).
% 6.20/11.69  fof(f508,plain,(
% 6.20/11.69    leq(sK24_skl,pv5)),
% 6.20/11.69    inference(trivial_equality_resolution,[status(thm)],[f507])).
% 6.20/11.69  fof(f509,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f253,f290])).
% 6.20/11.69  fof(f510,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f254,f509])).
% 6.20/11.69  fof(f511,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f255,f510])).
% 6.20/11.69  fof(f512,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f256,f511])).
% 6.20/11.69  fof(f513,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f257,f512])).
% 6.20/11.69  fof(f514,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f258,f513])).
% 6.20/11.69  fof(f515,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f259,f514])).
% 6.20/11.69  fof(f516,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f260,f515])).
% 6.20/11.69  fof(f517,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f261,f516])).
% 6.20/11.69  fof(f518,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f262,f517])).
% 6.20/11.69  fof(f519,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f263,f518])).
% 6.20/11.69  fof(f520,plain,(
% 6.20/11.69    ~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f264,f519])).
% 6.20/11.69  fof(f521,plain,(
% 6.20/11.69    ~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f265,f520])).
% 6.20/11.69  fof(f522,plain,(
% 6.20/11.69    ~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f266,f521])).
% 6.20/11.69  fof(f523,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f267,f522])).
% 6.20/11.69  fof(f524,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f268,f523])).
% 6.20/11.69  fof(f525,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f269,f524])).
% 6.20/11.69  fof(f526,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f270,f525])).
% 6.20/11.69  fof(f527,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f271,f526])).
% 6.20/11.69  fof(f528,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f272,f527])).
% 6.20/11.69  fof(f529,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f273,f528])).
% 6.20/11.69  fof(f530,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f274,f529])).
% 6.20/11.69  fof(f531,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f275,f530])).
% 6.20/11.69  fof(f532,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f276,f531])).
% 6.20/11.69  fof(f533,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f277,f532])).
% 6.20/11.69  fof(f534,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f278,f533])).
% 6.20/11.69  fof(f535,plain,(
% 6.20/11.69    ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~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_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f279,f534])).
% 6.20/11.69  fof(f536,plain,(
% 6.20/11.69    ~use=use|~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(duplicate_literals_removal,[status(thm)],[f535])).
% 6.20/11.69  fof(f537,plain,(
% 6.20/11.69    ~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(trivial_equality_resolution,[status(thm)],[f536])).
% 6.20/11.69  fof(f578,plain,(
% 6.20/11.69    leq(tptp_float_0_0,sK24_skl)),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f372,f447])).
% 6.20/11.69  fof(f579,plain,(
% 6.20/11.69    leq(tptp_float_0_0,sK23_skl)),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f372,f418])).
% 6.20/11.69  fof(f582,plain,(
% 6.20/11.69    ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(z_defuse,X0,X1)=use)),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f372,f283])).
% 6.20/11.69  fof(f583,plain,(
% 6.20/11.69    ![X0,X1]: (~leq(n0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(u_defuse,X0,X1)=use)),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f372,f282])).
% 6.20/11.69  fof(f658,plain,(
% 6.20/11.69    ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(z_defuse,X0,X1)=use)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f372,f582])).
% 6.20/11.69  fof(f659,plain,(
% 6.20/11.69    ![X0,X1]: (~leq(tptp_float_0_0,X0)|~leq(tptp_float_0_0,X1)|~leq(X0,n2)|~leq(X1,pv5)|a_select3(u_defuse,X0,X1)=use)),
% 6.20/11.69    inference(forward_demodulation,[status(thm)],[f372,f583])).
% 6.20/11.69  fof(f897,plain,(
% 6.20/11.69    ![X0]: (~leq(tptp_float_0_0,sK23_skl)|~leq(tptp_float_0_0,X0)|~leq(X0,pv5)|a_select3(z_defuse,sK23_skl,X0)=use)),
% 6.20/11.69    inference(resolution,[status(thm)],[f658,f476])).
% 6.20/11.69  fof(f902,plain,(
% 6.20/11.69    ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pv5)|a_select3(z_defuse,sK23_skl,X0)=use)),
% 6.20/11.69    inference(forward_subsumption_resolution,[status(thm)],[f897,f579])).
% 6.20/11.69  fof(f903,plain,(
% 6.20/11.69    ![X0]: (~leq(tptp_float_0_0,sK23_skl)|~leq(tptp_float_0_0,X0)|~leq(X0,pv5)|a_select3(u_defuse,sK23_skl,X0)=use)),
% 6.20/11.69    inference(resolution,[status(thm)],[f659,f476])).
% 6.20/11.69  fof(f908,plain,(
% 6.20/11.69    ![X0]: (~leq(tptp_float_0_0,X0)|~leq(X0,pv5)|a_select3(u_defuse,sK23_skl,X0)=use)),
% 6.20/11.69    inference(forward_subsumption_resolution,[status(thm)],[f903,f579])).
% 6.20/11.69  fof(f1280,plain,(
% 6.20/11.69    ~leq(tptp_float_0_0,sK24_skl)|a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(resolution,[status(thm)],[f902,f508])).
% 6.20/11.69  fof(f1286,plain,(
% 6.20/11.69    ~a_select3(u_defuse,sK23_skl,sK24_skl)=use|~use=use),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f1287,f537])).
% 6.20/11.69  fof(f1287,plain,(
% 6.20/11.69    a_select3(z_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_subsumption_resolution,[status(thm)],[f1280,f578])).
% 6.20/11.69  fof(f1289,plain,(
% 6.20/11.69    ~a_select3(u_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(trivial_equality_resolution,[status(thm)],[f1286])).
% 6.20/11.69  fof(f1300,plain,(
% 6.20/11.69    ~leq(tptp_float_0_0,sK24_skl)|a_select3(u_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(resolution,[status(thm)],[f908,f508])).
% 6.20/11.69  fof(f1306,plain,(
% 6.20/11.69    ~use=use),
% 6.20/11.69    inference(backward_demodulation,[status(thm)],[f1307,f1289])).
% 6.20/11.69  fof(f1307,plain,(
% 6.20/11.69    a_select3(u_defuse,sK23_skl,sK24_skl)=use),
% 6.20/11.69    inference(forward_subsumption_resolution,[status(thm)],[f1300,f578])).
% 6.20/11.69  fof(f1309,plain,(
% 6.20/11.69    $false),
% 6.20/11.69    inference(trivial_equality_resolution,[status(thm)],[f1306])).
% 6.20/11.69  % SZS output end CNFRefutation for theBenchmark.p
% 6.73/11.70  % Elapsed time: 0.898827 seconds
% 6.73/11.70  % CPU time: 6.899344 seconds
% 6.73/11.70  % Total memory used: 170.626 MB
% 6.73/11.70  % Net memory used: 160.428 MB
%------------------------------------------------------------------------------