%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV094+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 : n009.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.13s 0.46s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 52
% Syntax : Number of formulae : 268 ( 71 unt; 49 def)
% Number of atoms : 1807 ( 931 equ)
% Maximal formula atoms : 115 ( 6 avg)
% Number of connectives : 2561 (1022 ~;1056 |; 422 &)
% ( 49 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 76 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 50 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 23 con; 0-3 aty)
% Number of variables : 44 ( 34 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [A,B] :
( ( leq(B,minus(pv5,n1))
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv52,minus(n6,n1))
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv52)
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 )
=> ( ( pv51 = pv52
=> ( ! [E,F] :
( ( leq(F,minus(pv5,n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 ) )
& ( pv51 != pv52
=> ( ! [C,D] :
( ( leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
=> ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use ) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [A,B] :
( ( leq(B,minus(pv5,n1))
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv52,minus(n6,n1))
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv52)
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 )
=> ( ( pv51 = pv52
=> ( ! [E,F] :
( ( leq(F,minus(pv5,n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 ) )
& ( pv51 != pv52
=> ( ! [C,D] :
( ( leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
=> ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use ) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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(negated_conjecture,[status(cth)],[f53]) ).
fof(f109,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f227,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f261,plain,
( ( ( ( ? [E,F] :
( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,minus(pv5,n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 = pv52 )
| ( ( ? [C,D] :
( ( a_select3(z_defuse,C,D) != use
| a_select3(u_defuse,C,D) != use )
& leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 != pv52 ) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,minus(pv5,n1))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv52,minus(n6,n1))
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv52)
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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(f262,definition,
( sP3_prd
<=> ( ( ? [C,D] :
( ( a_select3(z_defuse,C,D) != use
| a_select3(u_defuse,C,D) != use )
& leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 != pv52 ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f263,plain,
( ( ( ( ? [E,F] :
( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,minus(pv5,n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 = pv52 )
| sP3_prd )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,minus(pv5,n1))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv52,minus(n6,n1))
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv52)
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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(formula_renaming,[status(thm)],[f261,f262]) ).
fof(f264,plain,
( ( ( ( ( ( a_select3(z_defuse,sK23_skl,sK24_skl) != use
| a_select3(u_defuse,sK23_skl,sK24_skl) != use )
& leq(sK24_skl,minus(pv5,n1))
& leq(sK23_skl,n2)
& leq(n0,sK24_skl)
& leq(n0,sK23_skl) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 = pv52 )
| sP3_prd )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,minus(pv5,n1))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv52,minus(n6,n1))
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv52)
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(E,sK23_skl),skolemize(F,sK24_skl)],[f263]) ).
fof(f265,plain,
a_select2(rho_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f266,plain,
a_select2(rho_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f267,plain,
a_select2(rho_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f268,plain,
a_select2(sigma_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f269,plain,
a_select2(sigma_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f270,plain,
a_select2(sigma_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f271,plain,
a_select2(sigma_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f272,plain,
a_select2(sigma_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f273,plain,
a_select2(sigma_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f274,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f275,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f276,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f277,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f278,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f279,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f280,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f281,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f282,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f283,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f284,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f285,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f286,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f287,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f288,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f289,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f290,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f291,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f292,plain,
leq(n0,pv5),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f293,plain,
leq(n0,pv51),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f295,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f296,plain,
leq(pv51,minus(n6,n1)),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f298,plain,
! [X0,X1] :
( a_select3(u_defuse,X0,X1) = use
| ~ leq(X1,minus(pv5,n1))
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f299,plain,
! [X0,X1] :
( a_select3(z_defuse,X0,X1) = use
| ~ leq(X1,minus(pv5,n1))
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f301,plain,
( leq(n0,sK23_skl)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f302,plain,
( leq(n0,sK24_skl)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f303,plain,
( leq(sK23_skl,n2)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f304,plain,
( leq(sK24_skl,minus(pv5,n1))
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f305,plain,
( a_select3(z_defuse,sK23_skl,sK24_skl) != use
| a_select3(u_defuse,sK23_skl,sK24_skl) != use
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f390,plain,
( ( ( ! [C,D] :
( ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use )
| ~ leq(D,minus(pv5,n1))
| ~ leq(C,n2)
| ~ leq(n0,D)
| ~ leq(n0,C) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 )
| pv51 = pv52
| sP3_prd )
& ( ( ( ? [C,D] :
( ( a_select3(z_defuse,C,D) != use
| a_select3(u_defuse,C,D) != use )
& leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 != pv52 )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f262]) ).
fof(f391,plain,
( ( ( ! [C,D] :
( ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use )
| ~ leq(D,minus(pv5,n1))
| ~ leq(C,n2)
| ~ leq(n0,D)
| ~ leq(n0,C) )
& leq(pv51,minus(n6,n1))
& leq(pv5,minus(n999,n1))
& leq(n0,pv51)
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_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 )
| pv51 = pv52
| sP3_prd )
& ( ( ( ( ( a_select3(z_defuse,sK29_skl,sK30_skl) != use
| a_select3(u_defuse,sK29_skl,sK30_skl) != use )
& leq(sK30_skl,minus(pv5,n1))
& leq(sK29_skl,n2)
& leq(n0,sK30_skl)
& leq(n0,sK29_skl) )
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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 )
& pv51 != pv52 )
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl,sK30_skl]),skolemize(C,sK29_skl),skolemize(D,sK30_skl)],[f390]) ).
fof(f393,plain,
( leq(n0,sK29_skl)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f394,plain,
( leq(n0,sK30_skl)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f395,plain,
( leq(sK29_skl,n2)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f396,plain,
( leq(sK30_skl,minus(pv5,n1))
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f397,plain,
( a_select3(z_defuse,sK29_skl,sK30_skl) != use
| a_select3(u_defuse,sK29_skl,sK30_skl) != use
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_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
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f439,definition,
( sQ0_spl
<=> sP3_prd ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f446,definition,
( sQ2_spl
<=> a_select2(rho_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ2_spl
| a_select2(rho_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ3_spl
<=> a_select2(rho_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ3_spl
| a_select2(rho_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,definition,
( sQ4_spl
<=> a_select2(rho_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ4_spl
| a_select2(rho_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,definition,
( sQ5_spl
<=> a_select2(sigma_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ5_spl
| a_select2(sigma_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,definition,
( sQ6_spl
<=> a_select2(sigma_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ6_spl
| a_select2(sigma_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,definition,
( sQ7_spl
<=> a_select2(sigma_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( sQ7_spl
| a_select2(sigma_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ8_spl
<=> a_select2(sigma_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ8_spl
| a_select2(sigma_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,definition,
( sQ9_spl
<=> a_select2(sigma_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( sQ9_spl
| a_select2(sigma_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f470,definition,
( sQ10_spl
<=> a_select2(sigma_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ10_spl
| a_select2(sigma_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,definition,
( sQ11_spl
<=> a_select3(u_defuse,n0,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ11_spl
| a_select3(u_defuse,n0,n0) != use ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,definition,
( sQ12_spl
<=> a_select3(u_defuse,n1,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f478,plain,
( sQ12_spl
| a_select3(u_defuse,n1,n0) != use ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f479,definition,
( sQ13_spl
<=> a_select3(u_defuse,n2,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ13_spl
| a_select3(u_defuse,n2,n0) != use ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f482,definition,
( sQ14_spl
<=> a_select2(xinit_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( sQ14_spl
| a_select2(xinit_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f482]) ).
fof(f485,definition,
( sQ15_spl
<=> a_select2(xinit_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f487,plain,
( sQ15_spl
| a_select2(xinit_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f485]) ).
fof(f488,definition,
( sQ16_spl
<=> a_select2(xinit_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f490,plain,
( sQ16_spl
| a_select2(xinit_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f488]) ).
fof(f491,definition,
( sQ17_spl
<=> a_select2(xinit_mean_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ17_spl
| a_select2(xinit_mean_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,definition,
( sQ18_spl
<=> a_select2(xinit_mean_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f496,plain,
( sQ18_spl
| a_select2(xinit_mean_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,definition,
( sQ19_spl
<=> a_select2(xinit_mean_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ19_spl
| a_select2(xinit_mean_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,definition,
( sQ20_spl
<=> a_select2(xinit_mean_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ20_spl
| a_select2(xinit_mean_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
( sQ21_spl
<=> a_select2(xinit_mean_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( sQ21_spl
| a_select2(xinit_mean_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f506,definition,
( sQ22_spl
<=> a_select2(xinit_mean_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( sQ22_spl
| a_select2(xinit_mean_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,definition,
( sQ23_spl
<=> a_select2(xinit_noise_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( sQ23_spl
| a_select2(xinit_noise_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,definition,
( sQ24_spl
<=> a_select2(xinit_noise_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( sQ24_spl
| a_select2(xinit_noise_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,definition,
( sQ25_spl
<=> a_select2(xinit_noise_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( sQ25_spl
| a_select2(xinit_noise_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,definition,
( sQ26_spl
<=> a_select2(xinit_noise_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ26_spl
| a_select2(xinit_noise_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,definition,
( sQ27_spl
<=> a_select2(xinit_noise_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ27_spl
| a_select2(xinit_noise_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,definition,
( sQ28_spl
<=> a_select2(xinit_noise_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( sQ28_spl
| a_select2(xinit_noise_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,definition,
( sQ29_spl
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( sQ29_spl
| ~ leq(n0,pv5) ),
inference(component_clause,[status(thm)],[f527]) ).
fof(f530,definition,
( sQ30_spl
<=> leq(n0,pv51) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f532,plain,
( sQ30_spl
| ~ leq(n0,pv51) ),
inference(component_clause,[status(thm)],[f530]) ).
fof(f533,definition,
( sQ31_spl
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f535,plain,
( sQ31_spl
| ~ leq(pv5,minus(n999,n1)) ),
inference(component_clause,[status(thm)],[f533]) ).
fof(f536,definition,
( sQ32_spl
<=> leq(pv51,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( sQ32_spl
| ~ leq(pv51,minus(n6,n1)) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,definition,
( sQ33_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f301,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f539]) ).
fof(f543,definition,
( sQ34_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( sQ34_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f302,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f543]) ).
fof(f547,definition,
( sQ35_spl
<=> leq(sK23_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( sQ35_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f303,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f547]) ).
fof(f551,definition,
( sQ36_spl
<=> leq(sK24_skl,minus(pv5,n1)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( ~ sQ36_spl
| leq(sK24_skl,minus(pv5,n1)) ),
inference(component_clause,[status(thm)],[f551]) ).
fof(f554,plain,
( sQ36_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f304,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f551]) ).
fof(f555,definition,
( sQ37_spl
<=> a_select3(u_defuse,sK23_skl,sK24_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( sQ37_spl
| a_select3(u_defuse,sK23_skl,sK24_skl) != use ),
inference(component_clause,[status(thm)],[f555]) ).
fof(f558,definition,
( sQ38_spl
<=> a_select3(z_defuse,sK23_skl,sK24_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( sQ38_spl
| a_select3(z_defuse,sK23_skl,sK24_skl) != use ),
inference(component_clause,[status(thm)],[f558]) ).
fof(f561,plain,
( ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f305,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f555,f558]) ).
fof(f563,definition,
( sQ39_spl
<=> leq(n0,sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( sQ39_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f393,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f563]) ).
fof(f567,definition,
( sQ40_spl
<=> leq(n0,sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( sQ40_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f394,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f567]) ).
fof(f571,definition,
( sQ41_spl
<=> leq(sK29_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( sQ41_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f395,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f571]) ).
fof(f575,definition,
( sQ42_spl
<=> leq(sK30_skl,minus(pv5,n1)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( ~ sQ42_spl
| leq(sK30_skl,minus(pv5,n1)) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f578,plain,
( sQ42_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f396,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f575]) ).
fof(f579,definition,
( sQ43_spl
<=> a_select3(u_defuse,sK29_skl,sK30_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ43_spl
| a_select3(u_defuse,sK29_skl,sK30_skl) != use ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,definition,
( sQ44_spl
<=> a_select3(z_defuse,sK29_skl,sK30_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ44_spl
| a_select3(z_defuse,sK29_skl,sK30_skl) != use ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,plain,
( ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f397,f439,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473,f476,f479,f482,f485,f488,f491,f494,f497,f500,f503,f506,f509,f512,f515,f518,f521,f524,f527,f530,f533,f536,f579,f582]) ).
fof(f637,plain,
leq(pv5,pred(n999)),
inference(forward_demodulation,[status(thm)],[f227,f295]) ).
fof(f638,plain,
leq(pv51,pred(n6)),
inference(forward_demodulation,[status(thm)],[f227,f296]) ).
fof(f640,plain,
! [X0,X1] :
( a_select3(u_defuse,X0,X1) = use
| ~ leq(X1,pred(pv5))
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f298]) ).
fof(f641,plain,
! [X0,X1] :
( a_select3(z_defuse,X0,X1) = use
| ~ leq(X1,pred(pv5))
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(forward_demodulation,[status(thm)],[f227,f299]) ).
fof(f653,plain,
( sQ32_spl
| ~ leq(pv51,pred(n6)) ),
inference(forward_demodulation,[status(thm)],[f227,f538]) ).
fof(f654,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f653,f638]) ).
fof(f655,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f657,plain,
( sQ31_spl
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f227,f535]) ).
fof(f658,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f637]) ).
fof(f659,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f658]) ).
fof(f661,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f532,f293]) ).
fof(f662,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f661]) ).
fof(f664,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f292]) ).
fof(f665,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f664]) ).
fof(f666,plain,
( sQ28_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f291,f526]) ).
fof(f667,plain,
( sQ28_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f666]) ).
fof(f668,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f667]) ).
fof(f669,plain,
( sQ27_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f290,f523]) ).
fof(f670,plain,
( sQ27_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f669]) ).
fof(f671,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f670]) ).
fof(f672,plain,
( sQ26_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f289,f520]) ).
fof(f673,plain,
( sQ26_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f672]) ).
fof(f674,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f673]) ).
fof(f675,plain,
( sQ25_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f288,f517]) ).
fof(f676,plain,
( sQ25_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f675]) ).
fof(f677,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f676]) ).
fof(f678,plain,
( sQ24_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f287,f514]) ).
fof(f679,plain,
( sQ24_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f678]) ).
fof(f680,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f679]) ).
fof(f681,plain,
( sQ23_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f286,f511]) ).
fof(f682,plain,
( sQ23_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f681]) ).
fof(f683,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f682]) ).
fof(f684,plain,
( sQ22_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f285,f508]) ).
fof(f685,plain,
( sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f684]) ).
fof(f686,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f685]) ).
fof(f687,plain,
( sQ21_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f284,f505]) ).
fof(f688,plain,
( sQ21_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f687]) ).
fof(f689,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f688]) ).
fof(f690,plain,
( sQ20_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f283,f502]) ).
fof(f691,plain,
( sQ20_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f690]) ).
fof(f692,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f691]) ).
fof(f693,plain,
( sQ19_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f282,f499]) ).
fof(f694,plain,
( sQ19_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f693]) ).
fof(f695,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f694]) ).
fof(f696,plain,
( sQ18_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f281,f496]) ).
fof(f697,plain,
( sQ18_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f696]) ).
fof(f698,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f697]) ).
fof(f699,plain,
( sQ17_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f280,f493]) ).
fof(f700,plain,
( sQ17_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f699]) ).
fof(f701,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f702,plain,
( sQ16_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f279,f490]) ).
fof(f703,plain,
( sQ16_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f702]) ).
fof(f704,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f703]) ).
fof(f705,plain,
( sQ15_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f278,f487]) ).
fof(f706,plain,
( sQ15_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f705]) ).
fof(f707,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f706]) ).
fof(f708,plain,
( sQ14_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f277,f484]) ).
fof(f709,plain,
( sQ14_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f708]) ).
fof(f710,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f709]) ).
fof(f711,plain,
( sQ13_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f276,f481]) ).
fof(f712,plain,
( sQ13_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f711]) ).
fof(f713,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f712]) ).
fof(f714,plain,
( sQ12_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f275,f478]) ).
fof(f715,plain,
( sQ12_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f714]) ).
fof(f716,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f715]) ).
fof(f717,plain,
( sQ11_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f274,f475]) ).
fof(f718,plain,
( sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f717]) ).
fof(f719,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f720,plain,
( sQ10_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f273,f472]) ).
fof(f721,plain,
( sQ10_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f720]) ).
fof(f722,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f721]) ).
fof(f723,plain,
( sQ9_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f272,f469]) ).
fof(f724,plain,
( sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f723]) ).
fof(f725,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f726,plain,
( sQ8_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f271,f466]) ).
fof(f727,plain,
( sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f726]) ).
fof(f728,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f727]) ).
fof(f729,plain,
( sQ7_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f270,f463]) ).
fof(f730,plain,
( sQ7_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f729]) ).
fof(f731,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f732,plain,
( sQ6_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f269,f460]) ).
fof(f733,plain,
( sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f732]) ).
fof(f734,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f733]) ).
fof(f735,plain,
( sQ5_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f268,f457]) ).
fof(f736,plain,
( sQ5_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f735]) ).
fof(f737,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f736]) ).
fof(f738,plain,
( sQ4_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f267,f454]) ).
fof(f739,plain,
( sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f738]) ).
fof(f740,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f741,plain,
( sQ3_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f266,f451]) ).
fof(f742,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f741]) ).
fof(f743,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f742]) ).
fof(f744,plain,
( sQ2_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f265,f448]) ).
fof(f745,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f744]) ).
fof(f746,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f745]) ).
fof(f747,plain,
( ~ sQ36_spl
| leq(sK24_skl,pred(pv5)) ),
inference(forward_demodulation,[status(thm)],[f227,f552]) ).
fof(f748,plain,
( ~ sQ42_spl
| leq(sK30_skl,pred(pv5)) ),
inference(forward_demodulation,[status(thm)],[f227,f576]) ).
fof(f991,definition,
( sQ82_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f993,plain,
( sQ82_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f991]) ).
fof(f1006,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f993,f109]) ).
fof(f1007,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f1006]) ).
fof(f1086,definition,
( sQ99_spl
<=> leq(n2,n2) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1088,plain,
( sQ99_spl
| ~ leq(n2,n2) ),
inference(component_clause,[status(thm)],[f1086]) ).
fof(f1101,plain,
( sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f109]) ).
fof(f1102,plain,
sQ99_spl,
inference(contradiction_clause,[status(thm)],[f1101]) ).
fof(f1103,plain,
( sQ43_spl
| ~ leq(sK30_skl,pred(pv5))
| ~ leq(sK29_skl,n2)
| ~ leq(n0,sK30_skl)
| ~ leq(n0,sK29_skl) ),
inference(resolution,[status(thm)],[f581,f640]) ).
fof(f1104,definition,
( sQ103_spl
<=> leq(sK30_skl,pred(pv5)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1106,plain,
( sQ103_spl
| ~ leq(sK30_skl,pred(pv5)) ),
inference(component_clause,[status(thm)],[f1104]) ).
fof(f1107,plain,
( sQ43_spl
| ~ sQ103_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1103,f563,f567,f571,f1104,f579]) ).
fof(f1108,plain,
( sQ103_spl
| ~ sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1106,f748]) ).
fof(f1109,plain,
( sQ103_spl
| ~ sQ42_spl ),
inference(contradiction_clause,[status(thm)],[f1108]) ).
fof(f1115,plain,
( sQ44_spl
| ~ leq(sK30_skl,pred(pv5))
| ~ leq(sK29_skl,n2)
| ~ leq(n0,sK30_skl)
| ~ leq(n0,sK29_skl) ),
inference(resolution,[status(thm)],[f584,f641]) ).
fof(f1116,plain,
( sQ44_spl
| ~ sQ103_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1115,f563,f567,f571,f1104,f582]) ).
fof(f1117,plain,
( sQ38_spl
| ~ leq(sK24_skl,pred(pv5))
| ~ leq(sK23_skl,n2)
| ~ leq(n0,sK24_skl)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f560,f641]) ).
fof(f1118,definition,
( sQ104_spl
<=> leq(sK24_skl,pred(pv5)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( sQ104_spl
| ~ leq(sK24_skl,pred(pv5)) ),
inference(component_clause,[status(thm)],[f1118]) ).
fof(f1121,plain,
( sQ38_spl
| ~ sQ104_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1117,f539,f543,f547,f1118,f558]) ).
fof(f1122,plain,
( sQ104_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f747]) ).
fof(f1123,plain,
( sQ104_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f1122]) ).
fof(f1124,plain,
( sQ37_spl
| ~ leq(sK24_skl,pred(pv5))
| ~ leq(sK23_skl,n2)
| ~ leq(n0,sK24_skl)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f557,f640]) ).
fof(f1125,plain,
( sQ37_spl
| ~ sQ104_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1124,f539,f543,f547,f1118,f555]) ).
fof(f1126,plain,
$false,
inference(sat_refutation,[status(thm)],[f542,f546,f550,f554,f561,f566,f570,f574,f578,f585,f655,f659,f662,f665,f668,f671,f674,f677,f680,f683,f686,f689,f692,f695,f698,f701,f704,f707,f710,f713,f716,f719,f722,f725,f728,f731,f734,f737,f740,f743,f746,f1007,f1102,f1107,f1109,f1116,f1121,f1123,f1125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV094+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:30:29 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.48 % Elapsed time: 0.111495 seconds
% 0.13/0.48 % CPU time: 0.515717 seconds
% 0.13/0.48 % Total memory used: 122.290 MB
% 0.13/0.48 % Net memory used: 121.373 MB
%------------------------------------------------------------------------------