%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:46:37 PM UTC 2026
% Result : Theorem 0.28s 0.78s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 25
% Syntax : Number of formulae : 168 ( 75 unt; 0 def)
% Number of atoms : 1122 (1031 equ)
% Maximal formula atoms : 36 ( 6 avg)
% Number of connectives : 1458 ( 504 ~; 859 |; 88 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 7 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-3 aty)
% Number of variables : 72 ( 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( gt(Y,X)
=> leq(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] :
( leq(X,pred(Y))
<=> gt(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y] :
( leq(X,Y)
=> leq(X,succ(Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] : succ(pred(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [I,U,X,VAL,VAL2] :
( ( a_select2(X,U) = VAL
& I != U )
=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,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),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),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),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),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),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),n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,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),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),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),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),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),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),n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,axiom,
gt(n5,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
gt(n5,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
gt(n3,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
gt(n5,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
gt(n3,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
gt(n4,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
gt(n5,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
gt(n5,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f92,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f104,plain,
! [X,Y] :
( leq(X,Y)
| ~ gt(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f105,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f108,plain,
! [X,Y] :
( ( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f109,plain,
( ! [X,Y] :
( ~ gt(Y,X)
| leq(X,pred(Y)) )
& ! [X,Y] :
( gt(Y,X)
| ~ leq(X,pred(Y)) ) ),
inference(miniscoping,[status(thm)],[f108]) ).
fof(f111,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f113,plain,
! [X,Y] :
( leq(X,succ(Y))
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f114,plain,
! [X0,X1] :
( leq(X0,succ(X1))
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X,Y] :
( ( ~ gt(succ(Y),X)
| leq(X,Y) )
& ( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f116,plain,
( ! [X,Y] :
( ~ gt(succ(Y),X)
| leq(X,Y) )
& ! [X,Y] :
( gt(succ(Y),X)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( gt(succ(X1),X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f212,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f233,plain,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f234,plain,
! [I,U,X,VAL,VAL2] :
( a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f235,plain,
! [I,U,X,VAL] :
( ! [VAL2] : a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f236,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| a_select2(X2,X1) != X3
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f244,plain,
( ( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use )
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f245,plain,
a_select2(rho_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f246,plain,
a_select2(rho_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f247,plain,
a_select2(rho_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f248,plain,
a_select2(sigma_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f249,plain,
a_select2(sigma_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f250,plain,
a_select2(sigma_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f251,plain,
a_select2(sigma_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f252,plain,
a_select2(sigma_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f253,plain,
a_select2(sigma_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f254,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f255,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f256,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f257,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f258,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f259,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f260,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f261,plain,
gt(n5,n4),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f269,plain,
gt(n5,n0),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f270,plain,
gt(n1,n0),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f271,plain,
gt(n2,n0),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f272,plain,
gt(n3,n0),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f274,plain,
gt(n5,n1),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f275,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f276,plain,
gt(n3,n1),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f277,plain,
gt(n4,n2),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f278,plain,
gt(n5,n2),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f281,plain,
gt(n5,n3),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f294,plain,
succ(succ(succ(succ(n0)))) = n4,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f296,plain,
succ(n0) = n1,
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f297,plain,
succ(succ(n0)) = n2,
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f298,plain,
succ(succ(succ(n0))) = n3,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f336,plain,
! [X0,X1,X2,X3] :
( a_select2(tptp_update2(X2,X0,X3),X1) = a_select2(X2,X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f236]) ).
fof(f372,plain,
succ(n1) = n2,
inference(forward_demodulation,[status(thm)],[f296,f297]) ).
fof(f376,plain,
succ(succ(n1)) = n3,
inference(forward_demodulation,[status(thm)],[f296,f298]) ).
fof(f377,plain,
succ(n2) = n3,
inference(forward_demodulation,[status(thm)],[f372,f376]) ).
fof(f396,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f245,f260]) ).
fof(f397,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f246,f396]) ).
fof(f398,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f247,f397]) ).
fof(f399,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f248,f398]) ).
fof(f400,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f249,f399]) ).
fof(f401,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f250,f400]) ).
fof(f402,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f251,f401]) ).
fof(f403,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f252,f402]) ).
fof(f404,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f253,f403]) ).
fof(f405,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f254,f404]) ).
fof(f406,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f255,f405]) ).
fof(f407,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f256,f406]) ).
fof(f408,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f257,f407]) ).
fof(f409,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f258,f408]) ).
fof(f410,plain,
( 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
| 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),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),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),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),n0) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f259,f409]) ).
fof(f411,plain,
( 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),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),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),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),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),n0) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f410]) ).
fof(f412,plain,
( 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),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),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),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),n0) != use
| use != use ),
inference(duplicate_literals_removal,[status(thm)],[f411]) ).
fof(f413,plain,
( 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),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),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),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),n0) != use ),
inference(trivial_equality_resolution,[status(thm)],[f412]) ).
fof(f414,plain,
( n5 = n1
| 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),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),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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f413]) ).
fof(f476,plain,
leq(n1,n3),
inference(resolution,[status(thm)],[f105,f276]) ).
fof(f477,plain,
leq(n0,n3),
inference(resolution,[status(thm)],[f105,f272]) ).
fof(f479,plain,
leq(n1,n2),
inference(resolution,[status(thm)],[f105,f275]) ).
fof(f480,plain,
leq(n0,n2),
inference(resolution,[status(thm)],[f105,f271]) ).
fof(f496,plain,
( n5 = n2
| n5 = n1
| 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),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),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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f414]) ).
fof(f497,plain,
( n5 = n3
| n5 = n2
| n5 = n1
| 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(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),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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f496]) ).
fof(f498,plain,
( n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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
| 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),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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f497]) ).
fof(f499,plain,
( n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| use != 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),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),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),n0) != use ),
inference(forward_demodulation,[status(thm)],[f233,f498]) ).
fof(f500,plain,
( n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),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),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),n0) != use ),
inference(trivial_equality_resolution,[status(thm)],[f499]) ).
fof(f501,plain,
( n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f500]) ).
fof(f502,plain,
( n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),n2) != 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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f501]) ).
fof(f503,plain,
( n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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(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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f502]) ).
fof(f504,plain,
( n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n3) != 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),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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f503]) ).
fof(f505,plain,
( n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| use != 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),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),n0) != use ),
inference(forward_demodulation,[status(thm)],[f233,f504]) ).
fof(f506,plain,
( n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),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),n0) != use ),
inference(trivial_equality_resolution,[status(thm)],[f505]) ).
fof(f612,plain,
( n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),n1) != use
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f506]) ).
fof(f613,plain,
( n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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(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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f612]) ).
fof(f614,plain,
( n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n2) != 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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f613]) ).
fof(f615,plain,
( n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| use != 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),n0) != use ),
inference(forward_demodulation,[status(thm)],[f233,f614]) ).
fof(f616,plain,
( n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),n0) != use ),
inference(trivial_equality_resolution,[status(thm)],[f615]) ).
fof(f617,plain,
( n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| 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),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f616]) ).
fof(f618,plain,
( n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n1) != use
| a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f617]) ).
fof(f619,plain,
( n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| use != use
| a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0) != use ),
inference(forward_demodulation,[status(thm)],[f233,f618]) ).
fof(f620,plain,
( n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n0) != use ),
inference(trivial_equality_resolution,[status(thm)],[f619]) ).
fof(f621,plain,
( n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f620]) ).
fof(f622,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| a_select2(tptp_update2(xinit_mean_defuse,n0,use),n0) != use ),
inference(paramodulation,[status(thm)],[f336,f621]) ).
fof(f623,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f622]) ).
fof(f624,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n2
| n5 = n1 ),
inference(trivial_equality_resolution,[status(thm)],[f623]) ).
fof(f724,plain,
! [X0] : ~ leq(succ(X0),X0),
inference(resolution,[status(thm)],[f117,f91]) ).
fof(f767,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n1
| gt(n2,n2) ),
inference(paramodulation,[status(thm)],[f624,f278]) ).
fof(f781,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n3
| n5 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f91]) ).
fof(f804,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n1
| gt(n3,n3) ),
inference(paramodulation,[status(thm)],[f781,f281]) ).
fof(f819,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n4
| n5 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f804,f91]) ).
fof(f847,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n1
| gt(n4,n4) ),
inference(paramodulation,[status(thm)],[f819,f261]) ).
fof(f856,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| n5 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f847,f91]) ).
fof(f882,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0
| gt(n1,n1) ),
inference(paramodulation,[status(thm)],[f856,f274]) ).
fof(f888,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| n5 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f882,f91]) ).
fof(f915,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1
| gt(n0,n0) ),
inference(paramodulation,[status(thm)],[f888,f269]) ).
fof(f919,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n2
| n4 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f915,f91]) ).
fof(f951,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n1
| gt(n2,n2) ),
inference(paramodulation,[status(thm)],[f919,f277]) ).
fof(f963,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n3
| n4 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f951,f91]) ).
fof(f999,plain,
succ(succ(succ(n1))) = n4,
inference(forward_demodulation,[status(thm)],[f296,f294]) ).
fof(f1000,plain,
succ(succ(n2)) = n4,
inference(forward_demodulation,[status(thm)],[f372,f999]) ).
fof(f1013,plain,
succ(n3) = n4,
inference(forward_demodulation,[status(thm)],[f377,f1000]) ).
fof(f1030,plain,
! [X0] : ~ leq(succ(succ(X0)),X0),
inference(resolution,[status(thm)],[f724,f114]) ).
fof(f1031,plain,
~ leq(n4,n3),
inference(paramodulation,[status(thm)],[f1013,f724]) ).
fof(f1032,plain,
~ leq(n3,n2),
inference(paramodulation,[status(thm)],[f377,f724]) ).
fof(f1033,plain,
~ leq(n2,n1),
inference(paramodulation,[status(thm)],[f372,f724]) ).
fof(f1034,plain,
~ leq(n1,n0),
inference(paramodulation,[status(thm)],[f296,f724]) ).
fof(f1074,plain,
! [X0] : ~ gt(X0,succ(succ(pred(X0)))),
inference(resolution,[status(thm)],[f1030,f111]) ).
fof(f1082,plain,
! [X0] : ~ gt(X0,succ(X0)),
inference(forward_demodulation,[status(thm)],[f212,f1074]) ).
fof(f1091,plain,
~ gt(n1,n2),
inference(paramodulation,[status(thm)],[f372,f1082]) ).
fof(f1108,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n1
| ~ leq(n3,n3) ),
inference(paramodulation,[status(thm)],[f963,f1031]) ).
fof(f1148,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| n4 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1108,f92]) ).
fof(f1157,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0
| ~ leq(n1,n3) ),
inference(paramodulation,[status(thm)],[f1148,f1031]) ).
fof(f1196,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| n4 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f476]) ).
fof(f1203,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1
| ~ leq(n0,n3) ),
inference(paramodulation,[status(thm)],[f1196,f1031]) ).
fof(f1241,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n2
| n3 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1203,f477]) ).
fof(f1248,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n1
| ~ leq(n2,n2) ),
inference(paramodulation,[status(thm)],[f1241,f1032]) ).
fof(f1297,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| n3 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1248,f92]) ).
fof(f1306,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0
| ~ leq(n1,n2) ),
inference(paramodulation,[status(thm)],[f1297,f1032]) ).
fof(f1354,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| n3 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1306,f479]) ).
fof(f1362,plain,
( n1 = n0
| n2 = n0
| n2 = n1
| ~ leq(n0,n2) ),
inference(paramodulation,[status(thm)],[f1354,f1032]) ).
fof(f1409,plain,
( n1 = n0
| n2 = n0
| n2 = n1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1362,f480]) ).
fof(f1652,plain,
( n1 = n0
| n2 = n0
| ~ leq(n1,n1) ),
inference(paramodulation,[status(thm)],[f1409,f1033]) ).
fof(f1701,plain,
( n1 = n0
| n2 = n0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1652,f92]) ).
fof(f1710,plain,
( n1 = n0
| ~ gt(n1,n0) ),
inference(paramodulation,[status(thm)],[f1701,f1091]) ).
fof(f1762,plain,
n1 = n0,
inference(forward_subsumption_resolution,[status(thm)],[f1710,f270]) ).
fof(f1785,plain,
~ leq(n0,n0),
inference(backward_demodulation,[status(thm)],[f1762,f1034]) ).
fof(f1839,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1785,f92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n018.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 08:32:13 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 0.28/0.78 % Refutation found
% 0.28/0.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.28/0.83 % Elapsed time: 0.362581 seconds
% 0.28/0.83 % CPU time: 2.271795 seconds
% 0.28/0.83 % Total memory used: 127.665 MB
% 0.28/0.83 % Net memory used: 125.306 MB
%------------------------------------------------------------------------------