%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:50:03 PM UTC 2026
% Result : Theorem 0.27s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n019.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 08:30:19 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.49 % Drodi V4.1.1
% 0.27/1.12 % Refutation found
% 0.27/1.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/1.12 % SZS output start CNFRefutation for theBenchmark
% 0.27/1.12 fof(f2,axiom,(
% 0.27/1.12 (! [X,Y,Z] :( ( gt(X,Y)& gt(Y,Z) )=> gt(X,Z) ) )),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f3,axiom,(
% 0.27/1.12 (! [X] : ~ gt(X,X) )),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f48,axiom,(
% 0.27/1.12 (! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL )),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f49,axiom,(
% 0.27/1.12 (! [I,U,X,VAL,VAL2] :( ( I != U& a_select2(X,U) = VAL )=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ) )),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f53,conjecture,(
% 0.27/1.12 ( ( 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(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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f54,negated_conjecture,(
% 0.27/1.12 ~(( ( 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(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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ) )),
% 0.27/1.12 inference(negated_conjecture,[status(cth)],[f53])).
% 0.27/1.12 fof(f55,axiom,(
% 0.27/1.12 gt(n5,n4) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f63,axiom,(
% 0.27/1.12 gt(n5,n0) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f65,axiom,(
% 0.27/1.12 gt(n2,n0) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f66,axiom,(
% 0.27/1.12 gt(n3,n0) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f67,axiom,(
% 0.27/1.12 gt(n4,n1) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f69,axiom,(
% 0.27/1.12 gt(n2,n1) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f71,axiom,(
% 0.27/1.12 gt(n4,n2) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f73,axiom,(
% 0.27/1.12 gt(n3,n2) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f74,axiom,(
% 0.27/1.12 gt(n4,n3) ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f82,axiom,(
% 0.27/1.12 succ(succ(succ(succ(n0)))) = n4 ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f83,axiom,(
% 0.27/1.12 succ(succ(succ(succ(succ(n0))))) = n5 ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f84,axiom,(
% 0.27/1.12 succ(n0) = n1 ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f85,axiom,(
% 0.27/1.12 succ(succ(n0)) = n2 ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f86,axiom,(
% 0.27/1.12 succ(succ(succ(n0))) = n3 ),
% 0.27/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/1.12 fof(f88,plain,(
% 0.27/1.12 ![X,Y,Z]: ((~gt(X,Y)|~gt(Y,Z))|gt(X,Z))),
% 0.27/1.12 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.27/1.12 fof(f89,plain,(
% 0.27/1.12 ![X,Z]: ((![Y]: (~gt(X,Y)|~gt(Y,Z)))|gt(X,Z))),
% 0.27/1.12 inference(miniscoping,[status(thm)],[f88])).
% 0.27/1.12 fof(f90,plain,(
% 0.27/1.12 ![X0,X1,X2]: (~gt(X0,X1)|~gt(X1,X2)|gt(X0,X2))),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f89])).
% 0.27/1.12 fof(f91,plain,(
% 0.27/1.12 ![X0]: (~gt(X0,X0))),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f3])).
% 0.27/1.12 fof(f233,plain,(
% 0.27/1.12 ![X0,X1,X2]: (a_select2(tptp_update2(X0,X1,X2),X1)=X2)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f48])).
% 0.27/1.12 fof(f234,plain,(
% 0.27/1.12 ![I,U,X,VAL,VAL2]: ((I=U|~a_select2(X,U)=VAL)|a_select2(tptp_update2(X,I,VAL2),U)=VAL)),
% 0.27/1.12 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.27/1.12 fof(f235,plain,(
% 0.27/1.12 ![I,U,X,VAL]: ((I=U|~a_select2(X,U)=VAL)|(![VAL2]: a_select2(tptp_update2(X,I,VAL2),U)=VAL))),
% 0.27/1.12 inference(miniscoping,[status(thm)],[f234])).
% 0.27/1.12 fof(f236,plain,(
% 0.27/1.12 ![X0,X1,X2,X3,X4]: (X0=X1|~a_select2(X2,X1)=X3|a_select2(tptp_update2(X2,X0,X4),X1)=X3)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f235])).
% 0.27/1.12 fof(f244,plain,(
% 0.27/1.12 (((((((((((((((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(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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use))),
% 0.27/1.12 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.27/1.12 fof(f245,plain,(
% 0.27/1.12 a_select2(rho_defuse,n0)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f246,plain,(
% 0.27/1.12 a_select2(rho_defuse,n1)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f247,plain,(
% 0.27/1.12 a_select2(rho_defuse,n2)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f248,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n0)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f249,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n1)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f250,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n2)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f251,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n3)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f252,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n4)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f253,plain,(
% 0.27/1.12 a_select2(sigma_defuse,n5)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f254,plain,(
% 0.27/1.12 a_select3(u_defuse,n0,n0)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f255,plain,(
% 0.27/1.12 a_select3(u_defuse,n1,n0)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f256,plain,(
% 0.27/1.12 a_select3(u_defuse,n2,n0)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f257,plain,(
% 0.27/1.12 a_select2(xinit_defuse,n3)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f258,plain,(
% 0.27/1.12 a_select2(xinit_defuse,n4)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f259,plain,(
% 0.27/1.12 a_select2(xinit_defuse,n5)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f260,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f244])).
% 0.27/1.12 fof(f261,plain,(
% 0.27/1.12 gt(n5,n4)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f55])).
% 0.27/1.12 fof(f269,plain,(
% 0.27/1.12 gt(n5,n0)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f63])).
% 0.27/1.12 fof(f271,plain,(
% 0.27/1.12 gt(n2,n0)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f65])).
% 0.27/1.12 fof(f272,plain,(
% 0.27/1.12 gt(n3,n0)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f66])).
% 0.27/1.12 fof(f273,plain,(
% 0.27/1.12 gt(n4,n1)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f67])).
% 0.27/1.12 fof(f275,plain,(
% 0.27/1.12 gt(n2,n1)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f69])).
% 0.27/1.12 fof(f277,plain,(
% 0.27/1.12 gt(n4,n2)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f71])).
% 0.27/1.12 fof(f279,plain,(
% 0.27/1.12 gt(n3,n2)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f73])).
% 0.27/1.12 fof(f280,plain,(
% 0.27/1.12 gt(n4,n3)),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f74])).
% 0.27/1.12 fof(f294,plain,(
% 0.27/1.12 succ(succ(succ(succ(n0))))=n4),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f82])).
% 0.27/1.12 fof(f295,plain,(
% 0.27/1.12 succ(succ(succ(succ(succ(n0)))))=n5),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f83])).
% 0.27/1.12 fof(f296,plain,(
% 0.27/1.12 succ(n0)=n1),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f84])).
% 0.27/1.12 fof(f297,plain,(
% 0.27/1.12 succ(succ(n0))=n2),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f85])).
% 0.27/1.12 fof(f298,plain,(
% 0.27/1.12 succ(succ(succ(n0)))=n3),
% 0.27/1.12 inference(cnf_transformation,[status(thm)],[f86])).
% 0.27/1.12 fof(f336,plain,(
% 0.27/1.12 ![X0,X1,X2,X3]: (X0=X1|a_select2(tptp_update2(X2,X0,X3),X1)=a_select2(X2,X1))),
% 0.27/1.12 inference(destructive_equality_resolution,[status(thm)],[f236])).
% 0.27/1.12 fof(f367,plain,(
% 0.27/1.12 ![X0,X1]: (~gt(X0,X1)|~gt(X1,X0))),
% 0.27/1.12 inference(resolution,[status(thm)],[f90,f91])).
% 0.27/1.12 fof(f453,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f245,f260])).
% 0.27/1.12 fof(f454,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f246,f453])).
% 0.27/1.12 fof(f455,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f247,f454])).
% 0.27/1.12 fof(f456,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f248,f455])).
% 0.27/1.12 fof(f457,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f249,f456])).
% 0.27/1.12 fof(f458,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f250,f457])).
% 0.27/1.12 fof(f459,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f251,f458])).
% 0.27/1.12 fof(f460,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f252,f459])).
% 0.27/1.12 fof(f461,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.12 inference(forward_demodulation,[status(thm)],[f253,f460])).
% 0.27/1.12 fof(f462,plain,(
% 0.27/1.12 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f254,f461])).
% 0.27/1.13 fof(f463,plain,(
% 0.27/1.13 ~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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f255,f462])).
% 0.27/1.13 fof(f464,plain,(
% 0.27/1.13 ~use=use|~use=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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f256,f463])).
% 0.27/1.13 fof(f465,plain,(
% 0.27/1.13 ~use=use|~use=use|~use=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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f257,f464])).
% 0.27/1.13 fof(f466,plain,(
% 0.27/1.13 ~use=use|~use=use|~use=use|~use=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(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f258,f465])).
% 0.27/1.13 fof(f467,plain,(
% 0.27/1.13 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f259,f466])).
% 0.27/1.13 fof(f468,plain,(
% 0.27/1.13 ~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~use=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~use=use),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f467])).
% 0.27/1.13 fof(f469,plain,(
% 0.27/1.13 ~use=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use),
% 0.27/1.13 inference(duplicate_literals_removal,[status(thm)],[f468])).
% 0.27/1.13 fof(f470,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f469])).
% 0.27/1.13 fof(f471,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|n5=n0),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f470])).
% 0.27/1.13 fof(f472,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|n5=n0|n5=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f471])).
% 0.27/1.13 fof(f539,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|n5=n0|n5=n1|n5=n2),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f472])).
% 0.27/1.13 fof(f540,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|n5=n0|n5=n1|n5=n2|n5=n3),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f539])).
% 0.27/1.13 fof(f541,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n4)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f540])).
% 0.27/1.13 fof(f542,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f541])).
% 0.27/1.13 fof(f543,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f542])).
% 0.27/1.13 fof(f544,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f543])).
% 0.27/1.13 fof(f545,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f544])).
% 0.27/1.13 fof(f688,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f545])).
% 0.27/1.13 fof(f689,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n3)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f688])).
% 0.27/1.13 fof(f690,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f689])).
% 0.27/1.13 fof(f691,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f690])).
% 0.27/1.13 fof(f692,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f691])).
% 0.27/1.13 fof(f693,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f692])).
% 0.27/1.13 fof(f694,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n2)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f693])).
% 0.27/1.13 fof(f695,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n1)=use|~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f694])).
% 0.27/1.13 fof(f696,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n1)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f695])).
% 0.27/1.13 fof(f810,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n1)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f696])).
% 0.27/1.13 fof(f811,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n0)=use|~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n1)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f810])).
% 0.27/1.13 fof(f812,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n0)=use|~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f811])).
% 0.27/1.13 fof(f813,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n0)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f812])).
% 0.27/1.13 fof(f814,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(xinit_mean_defuse,n0,use),n0)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1|n1=n0),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f336,f813])).
% 0.27/1.13 fof(f815,plain,(
% 0.27/1.13 ~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1|n1=n0),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f814])).
% 0.27/1.13 fof(f816,plain,(
% 0.27/1.13 n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1|n1=n0),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f815])).
% 0.27/1.13 fof(f817,plain,(
% 0.27/1.13 ~a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n1)=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f816,f813])).
% 0.27/1.13 fof(f879,plain,(
% 0.27/1.13 ~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f233,f817])).
% 0.27/1.13 fof(f880,plain,(
% 0.27/1.13 ~use=use|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(duplicate_literals_removal,[status(thm)],[f879])).
% 0.27/1.13 fof(f881,plain,(
% 0.27/1.13 n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n0|n2=n1),
% 0.27/1.13 inference(trivial_equality_resolution,[status(thm)],[f880])).
% 0.27/1.13 fof(f952,plain,(
% 0.27/1.13 gt(n2,n2)|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f881,f271])).
% 0.27/1.13 fof(f980,plain,(
% 0.27/1.13 n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n0|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(forward_subsumption_resolution,[status(thm)],[f952,f91])).
% 0.27/1.13 fof(f990,plain,(
% 0.27/1.13 succ(n1)=n2),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f296,f297])).
% 0.27/1.13 fof(f997,plain,(
% 0.27/1.13 succ(succ(succ(n1)))=n4),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f296,f294])).
% 0.27/1.13 fof(f998,plain,(
% 0.27/1.13 succ(succ(n2))=n4),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f990,f997])).
% 0.27/1.13 fof(f1005,plain,(
% 0.27/1.13 succ(succ(succ(succ(n1))))=n5),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f296,f295])).
% 0.27/1.13 fof(f1006,plain,(
% 0.27/1.13 succ(succ(succ(n2)))=n5),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f990,f1005])).
% 0.27/1.13 fof(f1007,plain,(
% 0.27/1.13 succ(n4)=n5),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f998,f1006])).
% 0.27/1.13 fof(f1041,plain,(
% 0.27/1.13 ~gt(n1,n2)),
% 0.27/1.13 inference(resolution,[status(thm)],[f367,f275])).
% 0.27/1.13 fof(f1045,plain,(
% 0.27/1.13 ~gt(n3,n4)),
% 0.27/1.13 inference(resolution,[status(thm)],[f367,f280])).
% 0.27/1.13 fof(f1046,plain,(
% 0.27/1.13 ~gt(n2,n4)),
% 0.27/1.13 inference(resolution,[status(thm)],[f367,f277])).
% 0.27/1.13 fof(f1048,plain,(
% 0.27/1.13 ~gt(n1,n4)),
% 0.27/1.13 inference(resolution,[status(thm)],[f367,f273])).
% 0.27/1.13 fof(f1259,plain,(
% 0.27/1.13 gt(n3,n3)|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f980,f272])).
% 0.27/1.13 fof(f1287,plain,(
% 0.27/1.13 n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n0|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(forward_subsumption_resolution,[status(thm)],[f1259,f91])).
% 0.27/1.13 fof(f1338,plain,(
% 0.27/1.13 succ(n4)=n1|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(paramodulation,[status(thm)],[f1287,f296])).
% 0.27/1.13 fof(f1369,plain,(
% 0.27/1.13 n5=n1|n5=n0|n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(forward_demodulation,[status(thm)],[f1007,f1338])).
% 0.27/1.13 fof(f1370,plain,(
% 0.27/1.13 n5=n1|n5=n0|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.13 inference(duplicate_literals_removal,[status(thm)],[f1369])).
% 0.27/1.14 fof(f1429,plain,(
% 0.27/1.14 gt(n5,n5)|n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1370,f269])).
% 0.27/1.14 fof(f1451,plain,(
% 0.27/1.14 n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2|n2=n1),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f1429,f91])).
% 0.27/1.14 fof(f1495,plain,(
% 0.27/1.14 gt(n2,n2)|n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1451,f275])).
% 0.27/1.14 fof(f1524,plain,(
% 0.27/1.14 n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n1|n3=n2),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f1495,f91])).
% 0.27/1.14 fof(f1552,plain,(
% 0.27/1.14 succ(succ(n1))=n3),
% 0.27/1.14 inference(forward_demodulation,[status(thm)],[f296,f298])).
% 0.27/1.14 fof(f1553,plain,(
% 0.27/1.14 succ(n3)=n4),
% 0.27/1.14 inference(backward_demodulation,[status(thm)],[f1554,f998])).
% 0.27/1.14 fof(f1554,plain,(
% 0.27/1.14 succ(n2)=n3),
% 0.27/1.14 inference(forward_demodulation,[status(thm)],[f990,f1552])).
% 0.27/1.14 fof(f1636,plain,(
% 0.27/1.14 ~gt(n3,n2)|n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1524,f1041])).
% 0.27/1.14 fof(f1687,plain,(
% 0.27/1.14 n5=n1|n5=n2|n5=n3|n5=n4|n4=n1|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f1636,f279])).
% 0.27/1.14 fof(f1711,plain,(
% 0.27/1.14 ~gt(n4,n2)|n5=n1|n5=n2|n5=n3|n5=n4|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1687,f1041])).
% 0.27/1.14 fof(f1761,plain,(
% 0.27/1.14 n5=n1|n5=n2|n5=n3|n5=n4|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f1711,f277])).
% 0.27/1.14 fof(f1784,plain,(
% 0.27/1.14 ~gt(n5,n4)|n5=n2|n5=n3|n5=n4|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1761,f1048])).
% 0.27/1.14 fof(f1836,plain,(
% 0.27/1.14 n5=n2|n5=n3|n5=n4|n4=n2|n4=n3|n3=n2),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f1784,f261])).
% 0.27/1.14 fof(f1859,plain,(
% 0.27/1.14 succ(n3)=n3|n5=n2|n5=n3|n5=n4|n4=n2|n4=n3),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1836,f1554])).
% 0.27/1.14 fof(f1909,plain,(
% 0.27/1.14 n4=n3|n5=n2|n5=n3|n5=n4|n4=n2|n4=n3),
% 0.27/1.14 inference(forward_demodulation,[status(thm)],[f1553,f1859])).
% 0.27/1.14 fof(f1910,plain,(
% 0.27/1.14 n4=n3|n5=n2|n5=n3|n5=n4|n4=n2),
% 0.27/1.14 inference(duplicate_literals_removal,[status(thm)],[f1909])).
% 0.27/1.14 fof(f2020,plain,(
% 0.27/1.14 succ(n4)=n3|n4=n3|n5=n2|n5=n3|n5=n4),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f1910,f1554])).
% 0.27/1.14 fof(f2065,plain,(
% 0.27/1.14 n5=n3|n4=n3|n5=n2|n5=n3|n5=n4),
% 0.27/1.14 inference(forward_demodulation,[status(thm)],[f1007,f2020])).
% 0.27/1.14 fof(f2066,plain,(
% 0.27/1.14 n5=n3|n4=n3|n5=n2|n5=n4),
% 0.27/1.14 inference(duplicate_literals_removal,[status(thm)],[f2065])).
% 0.27/1.14 fof(f2085,plain,(
% 0.27/1.14 ~gt(n5,n4)|n5=n3|n4=n3|n5=n4),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f2066,f1046])).
% 0.27/1.14 fof(f2128,plain,(
% 0.27/1.14 n5=n3|n4=n3|n5=n4),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f2085,f261])).
% 0.27/1.14 fof(f2146,plain,(
% 0.27/1.14 succ(n4)=n4|n5=n3|n5=n4),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f2128,f1553])).
% 0.27/1.14 fof(f2190,plain,(
% 0.27/1.14 n5=n4|n5=n3|n5=n4),
% 0.27/1.14 inference(forward_demodulation,[status(thm)],[f1007,f2146])).
% 0.27/1.14 fof(f2191,plain,(
% 0.27/1.14 n5=n4|n5=n3),
% 0.27/1.14 inference(duplicate_literals_removal,[status(thm)],[f2190])).
% 0.27/1.14 fof(f2207,plain,(
% 0.27/1.14 ~gt(n5,n4)|n5=n4),
% 0.27/1.14 inference(paramodulation,[status(thm)],[f2191,f1045])).
% 0.27/1.14 fof(f2244,plain,(
% 0.27/1.14 n5=n4),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f2207,f261])).
% 0.27/1.14 fof(f2292,plain,(
% 0.27/1.14 gt(n5,n5)),
% 0.27/1.14 inference(backward_demodulation,[status(thm)],[f2244,f261])).
% 0.27/1.14 fof(f2325,plain,(
% 0.27/1.14 $false),
% 0.27/1.14 inference(forward_subsumption_resolution,[status(thm)],[f2292,f91])).
% 0.27/1.14 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/1.17 % Elapsed time: 0.702473 seconds
% 0.27/1.17 % CPU time: 4.949743 seconds
% 0.27/1.17 % Total memory used: 141.866 MB
% 0.27/1.17 % Net memory used: 136.281 MB
%------------------------------------------------------------------------------