%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV097+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:38 PM UTC 2026
% Result : Theorem 0.15s 0.62s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 59
% Syntax : Number of formulae : 305 ( 73 unt; 53 def)
% Number of atoms : 1319 ( 587 equ)
% Maximal formula atoms : 82 ( 4 avg)
% Number of connectives : 1639 ( 625 ~; 667 |; 283 &)
% ( 53 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 57 ( 55 usr; 53 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-3 aty)
% Number of variables : 80 ( 72 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( gt(Y,X)
=> leq(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( ! [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 ) )
& ! [A,B] :
( ( leq(B,pv5)
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv5,minus(n999,n1))
& 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 )
=> ( ! [G,H] :
( ( leq(H,minus(pv5,n1))
& leq(G,n2)
& leq(n0,H)
& leq(n0,G) )
=> ( a_select3(z_defuse,G,H) = use
& a_select3(u_defuse,G,H) = use ) )
& ! [E,F] :
( ( leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& leq(pv5,minus(n999,n1))
& 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/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( ! [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 ) )
& ! [A,B] :
( ( leq(B,pv5)
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv5,minus(n999,n1))
& 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 )
=> ( ! [G,H] :
( ( leq(H,minus(pv5,n1))
& leq(G,n2)
& leq(n0,H)
& leq(n0,G) )
=> ( a_select3(z_defuse,G,H) = use
& a_select3(u_defuse,G,H) = use ) )
& ! [E,F] :
( ( leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& leq(pv5,minus(n999,n1))
& 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(f69,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
gt(n2,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f111,plain,
! [X,Y] :
( leq(X,Y)
| ~ gt(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f112,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f217,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f251,plain,
( ( ? [G,H] :
( ( a_select3(z_defuse,G,H) != use
| a_select3(u_defuse,G,H) != use )
& leq(H,minus(pv5,n1))
& leq(G,n2)
& leq(n0,H)
& leq(n0,G) )
| ? [E,F] :
( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| ~ leq(pv5,minus(n999,n1))
| ~ 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 )
& ! [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) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& 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(f252,definition,
! [E,F] :
( sP3_prd(F,E)
<=> ( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f253,plain,
( ( ? [G,H] :
( ( a_select3(z_defuse,G,H) != use
| a_select3(u_defuse,G,H) != use )
& leq(H,minus(pv5,n1))
& leq(G,n2)
& leq(n0,H)
& leq(n0,G) )
| ? [E,F] : sP3_prd(F,E)
| ~ leq(pv5,minus(n999,n1))
| ~ 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 )
& ! [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) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& 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)],[f251,f252]) ).
fof(f254,plain,
( ( ( ( a_select3(z_defuse,sK25_skl,sK26_skl) != use
| a_select3(u_defuse,sK25_skl,sK26_skl) != use )
& leq(sK26_skl,minus(pv5,n1))
& leq(sK25_skl,n2)
& leq(n0,sK26_skl)
& leq(n0,sK25_skl) )
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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 )
& ! [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) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& 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,sK25_skl,sK26_skl]),skolemize(E,sK23_skl),skolemize(F,sK24_skl),skolemize(G,sK25_skl),skolemize(H,sK26_skl)],[f253]) ).
fof(f255,plain,
a_select2(rho_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f256,plain,
a_select2(rho_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f257,plain,
a_select2(rho_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f258,plain,
a_select2(sigma_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f259,plain,
a_select2(sigma_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f260,plain,
a_select2(sigma_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f261,plain,
a_select2(sigma_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f262,plain,
a_select2(sigma_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f263,plain,
a_select2(sigma_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f264,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f265,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f266,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f267,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f268,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f269,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f270,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f271,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f272,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f273,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f274,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f275,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f276,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f277,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f278,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f279,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f280,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f281,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f282,plain,
leq(n0,pv5),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f283,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f284,plain,
! [X0,X1] :
( a_select3(u_defuse,X0,X1) = use
| ~ leq(X1,pv5)
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f285,plain,
! [X0,X1] :
( a_select3(z_defuse,X0,X1) = use
| ~ leq(X1,pv5)
| ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f286,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)],[f254]) ).
fof(f287,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)],[f254]) ).
fof(f288,plain,
( leq(n0,sK25_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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(cnf_transformation,[status(thm)],[f254]) ).
fof(f289,plain,
( leq(n0,sK26_skl)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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(cnf_transformation,[status(thm)],[f254]) ).
fof(f290,plain,
( leq(sK25_skl,n2)
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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(cnf_transformation,[status(thm)],[f254]) ).
fof(f291,plain,
( leq(sK26_skl,minus(pv5,n1))
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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(cnf_transformation,[status(thm)],[f254]) ).
fof(f292,plain,
( a_select3(z_defuse,sK25_skl,sK26_skl) != use
| a_select3(u_defuse,sK25_skl,sK26_skl) != use
| sP3_prd(sK24_skl,sK23_skl)
| ~ leq(pv5,minus(n999,n1))
| ~ 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(cnf_transformation,[status(thm)],[f254]) ).
fof(f307,plain,
gt(n2,n0),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f312,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f366,plain,
! [E,F] :
( ( ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use )
| ~ leq(F,pv5)
| ~ leq(E,n2)
| ~ leq(n0,F)
| ~ leq(n0,E)
| sP3_prd(F,E) )
& ( ( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| ~ sP3_prd(F,E) ) ),
inference(NNF_transformation,[status(thm)],[f252]) ).
fof(f367,plain,
( ! [E,F] :
( ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use )
| ~ leq(F,pv5)
| ~ leq(E,n2)
| ~ leq(n0,F)
| ~ leq(n0,E)
| sP3_prd(F,E) )
& ! [E,F] :
( ( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,pv5)
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| ~ sP3_prd(F,E) ) ),
inference(miniscoping,[status(thm)],[f366]) ).
fof(f368,plain,
! [X0,X1] :
( leq(n0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f369,plain,
! [X0,X1] :
( leq(n0,X0)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f370,plain,
! [X0,X1] :
( leq(X1,n2)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f371,plain,
! [X0,X1] :
( leq(X0,pv5)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f372,plain,
! [X0,X1] :
( a_select3(z_defuse,X1,X0) != use
| a_select3(u_defuse,X1,X0) != use
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f383,definition,
( sQ0_spl
<=> a_select2(rho_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ0_spl
| a_select2(rho_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,definition,
( sQ1_spl
<=> a_select2(rho_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f388,plain,
( sQ1_spl
| a_select2(rho_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f389,definition,
( sQ2_spl
<=> a_select2(rho_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f391,plain,
( sQ2_spl
| a_select2(rho_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f389]) ).
fof(f392,definition,
( sQ3_spl
<=> a_select2(sigma_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( sQ3_spl
| a_select2(sigma_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f395,definition,
( sQ4_spl
<=> a_select2(sigma_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( sQ4_spl
| a_select2(sigma_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f395]) ).
fof(f398,definition,
( sQ5_spl
<=> a_select2(sigma_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ5_spl
| a_select2(sigma_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ6_spl
<=> a_select2(sigma_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( sQ6_spl
| a_select2(sigma_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,definition,
( sQ7_spl
<=> a_select2(sigma_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( sQ7_spl
| a_select2(sigma_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,definition,
( sQ8_spl
<=> a_select2(sigma_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( sQ8_spl
| a_select2(sigma_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,definition,
( sQ9_spl
<=> a_select3(u_defuse,n0,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( sQ9_spl
| a_select3(u_defuse,n0,n0) != use ),
inference(component_clause,[status(thm)],[f410]) ).
fof(f413,definition,
( sQ10_spl
<=> a_select3(u_defuse,n1,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ10_spl
| a_select3(u_defuse,n1,n0) != use ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f416,definition,
( sQ11_spl
<=> a_select3(u_defuse,n2,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( sQ11_spl
| a_select3(u_defuse,n2,n0) != use ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f419,definition,
( sQ12_spl
<=> a_select2(xinit_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( sQ12_spl
| a_select2(xinit_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f419]) ).
fof(f422,definition,
( sQ13_spl
<=> a_select2(xinit_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( sQ13_spl
| a_select2(xinit_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,definition,
( sQ14_spl
<=> a_select2(xinit_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( sQ14_spl
| a_select2(xinit_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f425]) ).
fof(f428,definition,
( sQ15_spl
<=> a_select2(xinit_mean_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( sQ15_spl
| a_select2(xinit_mean_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,definition,
( sQ16_spl
<=> a_select2(xinit_mean_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( sQ16_spl
| a_select2(xinit_mean_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,definition,
( sQ17_spl
<=> a_select2(xinit_mean_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f436,plain,
( sQ17_spl
| a_select2(xinit_mean_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f437,definition,
( sQ18_spl
<=> a_select2(xinit_mean_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ18_spl
| a_select2(xinit_mean_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f440,definition,
( sQ19_spl
<=> a_select2(xinit_mean_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ19_spl
| a_select2(xinit_mean_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,definition,
( sQ20_spl
<=> a_select2(xinit_mean_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f445,plain,
( sQ20_spl
| a_select2(xinit_mean_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
( sQ21_spl
<=> a_select2(xinit_noise_defuse,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ21_spl
| a_select2(xinit_noise_defuse,n0) != use ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ22_spl
<=> a_select2(xinit_noise_defuse,n1) = use ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ22_spl
| a_select2(xinit_noise_defuse,n1) != use ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,definition,
( sQ23_spl
<=> a_select2(xinit_noise_defuse,n2) = use ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f454,plain,
( sQ23_spl
| a_select2(xinit_noise_defuse,n2) != use ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,definition,
( sQ24_spl
<=> a_select2(xinit_noise_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ24_spl
| a_select2(xinit_noise_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,definition,
( sQ25_spl
<=> a_select2(xinit_noise_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ25_spl
| a_select2(xinit_noise_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,definition,
( sQ26_spl
<=> a_select2(xinit_noise_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( sQ26_spl
| a_select2(xinit_noise_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ27_spl
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ27_spl
| ~ leq(n0,pv5) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,definition,
( sQ28_spl
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( sQ28_spl
| ~ leq(pv5,minus(n999,n1)) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f470,definition,
( sQ29_spl
<=> sP3_prd(sK24_skl,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( ~ sQ29_spl
| sP3_prd(sK24_skl,sK23_skl) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,definition,
( sQ30_spl
<=> leq(n0,sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( 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
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f288,f383,f386,f389,f392,f395,f398,f401,f404,f407,f410,f413,f416,f419,f422,f425,f428,f431,f434,f437,f440,f443,f446,f449,f452,f455,f458,f461,f464,f467,f470,f473]) ).
fof(f477,definition,
( sQ31_spl
<=> leq(n0,sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f480,plain,
( sQ31_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
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f289,f383,f386,f389,f392,f395,f398,f401,f404,f407,f410,f413,f416,f419,f422,f425,f428,f431,f434,f437,f440,f443,f446,f449,f452,f455,f458,f461,f464,f467,f470,f477]) ).
fof(f481,definition,
( sQ32_spl
<=> leq(sK25_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( sQ32_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
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f290,f383,f386,f389,f392,f395,f398,f401,f404,f407,f410,f413,f416,f419,f422,f425,f428,f431,f434,f437,f440,f443,f446,f449,f452,f455,f458,f461,f464,f467,f470,f481]) ).
fof(f485,definition,
( sQ33_spl
<=> leq(sK26_skl,minus(pv5,n1)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( ~ sQ33_spl
| leq(sK26_skl,minus(pv5,n1)) ),
inference(component_clause,[status(thm)],[f485]) ).
fof(f488,plain,
( sQ33_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
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f291,f383,f386,f389,f392,f395,f398,f401,f404,f407,f410,f413,f416,f419,f422,f425,f428,f431,f434,f437,f440,f443,f446,f449,f452,f455,f458,f461,f464,f467,f470,f485]) ).
fof(f489,definition,
( sQ34_spl
<=> a_select3(u_defuse,sK25_skl,sK26_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( sQ34_spl
| a_select3(u_defuse,sK25_skl,sK26_skl) != use ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f492,definition,
( sQ35_spl
<=> a_select3(z_defuse,sK25_skl,sK26_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ35_spl
| a_select3(z_defuse,sK25_skl,sK26_skl) != use ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f495,plain,
( ~ sQ35_spl
| ~ sQ34_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
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f292,f383,f386,f389,f392,f395,f398,f401,f404,f407,f410,f413,f416,f419,f422,f425,f428,f431,f434,f437,f440,f443,f446,f449,f452,f455,f458,f461,f464,f467,f470,f489,f492]) ).
fof(f508,plain,
leq(pv5,pred(n999)),
inference(forward_demodulation,[status(thm)],[f217,f283]) ).
fof(f509,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)],[f217,f286]) ).
fof(f510,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)],[f217,f287]) ).
fof(f688,definition,
( sQ61_spl
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( sQ61_spl
| ~ leq(n0,n0) ),
inference(component_clause,[status(thm)],[f688]) ).
fof(f698,plain,
( sQ28_spl
| ~ leq(pv5,pred(n999)) ),
inference(forward_demodulation,[status(thm)],[f217,f469]) ).
fof(f699,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f698,f508]) ).
fof(f700,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f699]) ).
fof(f701,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f466,f282]) ).
fof(f702,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f701]) ).
fof(f703,plain,
( sQ26_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f281,f463]) ).
fof(f704,plain,
( sQ26_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f703]) ).
fof(f705,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f704]) ).
fof(f706,plain,
( sQ25_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f280,f460]) ).
fof(f707,plain,
( sQ25_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f706]) ).
fof(f708,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f707]) ).
fof(f709,plain,
( sQ24_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f279,f457]) ).
fof(f710,plain,
( sQ24_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f709]) ).
fof(f711,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f710]) ).
fof(f712,plain,
( sQ23_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f278,f454]) ).
fof(f713,plain,
( sQ23_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f712]) ).
fof(f714,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f713]) ).
fof(f715,plain,
( sQ22_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f277,f451]) ).
fof(f716,plain,
( sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f715]) ).
fof(f717,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f716]) ).
fof(f718,plain,
( sQ21_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f276,f448]) ).
fof(f719,plain,
( sQ21_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f718]) ).
fof(f720,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f719]) ).
fof(f721,plain,
( sQ20_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f275,f445]) ).
fof(f722,plain,
( sQ20_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f721]) ).
fof(f723,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f724,plain,
( sQ19_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f274,f442]) ).
fof(f725,plain,
( sQ19_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f724]) ).
fof(f726,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f725]) ).
fof(f727,plain,
( sQ18_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f273,f439]) ).
fof(f728,plain,
( sQ18_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f727]) ).
fof(f729,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f728]) ).
fof(f730,plain,
( sQ17_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f272,f436]) ).
fof(f731,plain,
( sQ17_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f730]) ).
fof(f732,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f731]) ).
fof(f733,plain,
( sQ16_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f271,f433]) ).
fof(f734,plain,
( sQ16_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f733]) ).
fof(f735,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f734]) ).
fof(f736,plain,
( sQ15_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f270,f430]) ).
fof(f737,plain,
( sQ15_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f736]) ).
fof(f738,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f737]) ).
fof(f739,plain,
( sQ14_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f269,f427]) ).
fof(f740,plain,
( sQ14_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f739]) ).
fof(f741,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f740]) ).
fof(f742,plain,
( sQ13_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f268,f424]) ).
fof(f743,plain,
( sQ13_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f742]) ).
fof(f744,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f743]) ).
fof(f745,plain,
( sQ12_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f267,f421]) ).
fof(f746,plain,
( sQ12_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f745]) ).
fof(f747,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f746]) ).
fof(f748,plain,
( sQ11_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f266,f418]) ).
fof(f749,plain,
( sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f748]) ).
fof(f750,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f749]) ).
fof(f751,plain,
( sQ10_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f265,f415]) ).
fof(f752,plain,
( sQ10_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f751]) ).
fof(f753,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f752]) ).
fof(f754,plain,
( sQ9_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f264,f412]) ).
fof(f755,plain,
( sQ9_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f754]) ).
fof(f756,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f755]) ).
fof(f757,plain,
( sQ8_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f263,f409]) ).
fof(f758,plain,
( sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f757]) ).
fof(f759,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f758]) ).
fof(f760,plain,
( sQ7_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f262,f406]) ).
fof(f761,plain,
( sQ7_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f760]) ).
fof(f762,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f761]) ).
fof(f763,plain,
( sQ6_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f261,f403]) ).
fof(f764,plain,
( sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f763]) ).
fof(f765,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f764]) ).
fof(f766,plain,
( sQ5_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f260,f400]) ).
fof(f767,plain,
( sQ5_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f766]) ).
fof(f768,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f767]) ).
fof(f769,plain,
( sQ4_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f259,f397]) ).
fof(f770,plain,
( sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f769]) ).
fof(f771,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f770]) ).
fof(f772,plain,
( sQ3_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f258,f394]) ).
fof(f773,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f772]) ).
fof(f774,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f773]) ).
fof(f775,plain,
( sQ2_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f257,f391]) ).
fof(f776,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f775]) ).
fof(f777,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f776]) ).
fof(f778,plain,
( sQ1_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f256,f388]) ).
fof(f779,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f778]) ).
fof(f780,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f779]) ).
fof(f781,plain,
( sQ0_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f255,f385]) ).
fof(f782,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f781]) ).
fof(f783,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f784,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f690,f99]) ).
fof(f785,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f784]) ).
fof(f793,definition,
( sQ65_spl
<=> leq(n3,n3) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f795,plain,
( sQ65_spl
| ~ leq(n3,n3) ),
inference(component_clause,[status(thm)],[f793]) ).
fof(f801,plain,
( sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f99]) ).
fof(f802,plain,
sQ65_spl,
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f821,plain,
( ~ sQ33_spl
| leq(sK26_skl,pred(pv5)) ),
inference(forward_demodulation,[status(thm)],[f217,f486]) ).
fof(f842,plain,
( use = use
| ~ leq(n0,pv5)
| ~ leq(n0,n2)
| ~ leq(n0,n0)
| ~ leq(n0,n0) ),
inference(paramodulation,[status(thm)],[f264,f284]) ).
fof(f843,definition,
( sQ72_spl
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( sQ72_spl
| ~ leq(n0,n2) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,definition,
( sQ73_spl
<=> leq(n2,n2) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f848,plain,
( sQ73_spl
| ~ leq(n2,n2) ),
inference(component_clause,[status(thm)],[f846]) ).
fof(f849,definition,
( sQ74_spl
<=> use = use ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f853,definition,
( sQ75_spl
<=> leq(n1,n2) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( sQ75_spl
| ~ leq(n1,n2) ),
inference(component_clause,[status(thm)],[f853]) ).
fof(f857,plain,
( sQ74_spl
| ~ sQ27_spl
| ~ sQ72_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f842,f688,f843,f464,f849]) ).
fof(f858,plain,
( sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f848,f99]) ).
fof(f859,plain,
sQ73_spl,
inference(contradiction_clause,[status(thm)],[f858]) ).
fof(f870,plain,
( sQ72_spl
| ~ gt(n2,n0) ),
inference(resolution,[status(thm)],[f845,f112]) ).
fof(f873,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f870,f307]) ).
fof(f874,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f873]) ).
fof(f875,plain,
( sQ75_spl
| ~ gt(n2,n1) ),
inference(resolution,[status(thm)],[f855,f112]) ).
fof(f878,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f875,f312]) ).
fof(f879,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f878]) ).
fof(f916,plain,
( ~ sQ29_spl
| a_select3(z_defuse,sK23_skl,sK24_skl) != use
| a_select3(u_defuse,sK23_skl,sK24_skl) != use ),
inference(resolution,[status(thm)],[f372,f471]) ).
fof(f917,definition,
( sQ79_spl
<=> a_select3(u_defuse,sK23_skl,sK24_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f919,plain,
( sQ79_spl
| a_select3(u_defuse,sK23_skl,sK24_skl) != use ),
inference(component_clause,[status(thm)],[f917]) ).
fof(f920,definition,
( sQ80_spl
<=> a_select3(z_defuse,sK23_skl,sK24_skl) = use ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f922,plain,
( sQ80_spl
| a_select3(z_defuse,sK23_skl,sK24_skl) != use ),
inference(component_clause,[status(thm)],[f920]) ).
fof(f923,plain,
( ~ sQ29_spl
| ~ sQ80_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f916,f917,f920,f470]) ).
fof(f937,definition,
( sQ82_spl
<=> sK26_skl = n0 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( ~ sQ82_spl
| sK26_skl = n0 ),
inference(component_clause,[status(thm)],[f937]) ).
fof(f951,definition,
( sQ84_spl
<=> leq(n0,sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f953,plain,
( sQ84_spl
| ~ leq(n0,sK23_skl) ),
inference(component_clause,[status(thm)],[f951]) ).
fof(f954,definition,
( sQ85_spl
<=> leq(n0,sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( sQ85_spl
| ~ leq(n0,sK24_skl) ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f957,definition,
( sQ86_spl
<=> leq(sK23_skl,n2) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( sQ86_spl
| ~ leq(sK23_skl,n2) ),
inference(component_clause,[status(thm)],[f957]) ).
fof(f972,plain,
( sQ79_spl
| ~ leq(sK24_skl,pv5)
| ~ leq(sK23_skl,n2)
| ~ leq(n0,sK24_skl)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f284,f919]) ).
fof(f976,definition,
( sQ88_spl
<=> leq(sK24_skl,pv5) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f978,plain,
( sQ88_spl
| ~ leq(sK24_skl,pv5) ),
inference(component_clause,[status(thm)],[f976]) ).
fof(f979,plain,
( sQ79_spl
| ~ sQ88_spl
| ~ sQ86_spl
| ~ sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f972,f951,f954,f957,f976,f917]) ).
fof(f983,plain,
( sQ34_spl
| ~ leq(sK26_skl,pv5)
| ~ leq(sK25_skl,n2)
| ~ leq(n0,sK26_skl)
| ~ leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f491,f284]) ).
fof(f984,plain,
( sQ34_spl
| ~ leq(sK26_skl,pred(pv5))
| ~ leq(sK25_skl,n2)
| ~ leq(n0,sK26_skl)
| ~ leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f491,f509]) ).
fof(f985,definition,
( sQ89_spl
<=> leq(sK26_skl,pv5) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f987,plain,
( sQ89_spl
| ~ leq(sK26_skl,pv5) ),
inference(component_clause,[status(thm)],[f985]) ).
fof(f988,plain,
( sQ34_spl
| ~ sQ89_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f983,f473,f477,f481,f985,f489]) ).
fof(f989,definition,
( sQ90_spl
<=> leq(sK26_skl,pred(pv5)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f991,plain,
( sQ90_spl
| ~ leq(sK26_skl,pred(pv5)) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f992,plain,
( sQ34_spl
| ~ sQ90_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f984,f473,f477,f481,f989,f489]) ).
fof(f993,plain,
( sQ90_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f991,f821]) ).
fof(f994,plain,
( sQ90_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f993]) ).
fof(f1017,plain,
( sQ89_spl
| ~ sQ82_spl
| ~ leq(n0,pv5) ),
inference(backward_demodulation,[status(thm)],[f938,f987]) ).
fof(f1020,plain,
( sQ89_spl
| ~ sQ82_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1017,f464,f937,f985]) ).
fof(f1073,plain,
! [X0] :
( sQ86_spl
| ~ sP3_prd(X0,sK23_skl) ),
inference(resolution,[status(thm)],[f959,f370]) ).
fof(f1078,plain,
( ~ sQ29_spl
| sQ86_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f471,f1073]) ).
fof(f1079,plain,
( ~ sQ29_spl
| sQ86_spl ),
inference(contradiction_clause,[status(thm)],[f1078]) ).
fof(f1086,plain,
! [X0] :
( sQ85_spl
| ~ sP3_prd(sK24_skl,X0) ),
inference(resolution,[status(thm)],[f956,f369]) ).
fof(f1093,plain,
( ~ sQ29_spl
| sQ85_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f471,f1086]) ).
fof(f1094,plain,
( ~ sQ29_spl
| sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f1093]) ).
fof(f1096,plain,
! [X0] :
( sQ84_spl
| ~ sP3_prd(X0,sK23_skl) ),
inference(resolution,[status(thm)],[f953,f368]) ).
fof(f1102,plain,
( ~ sQ29_spl
| sQ84_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f471,f1096]) ).
fof(f1103,plain,
( ~ sQ29_spl
| sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f1102]) ).
fof(f1104,plain,
! [X0] :
( sQ88_spl
| ~ sP3_prd(sK24_skl,X0) ),
inference(resolution,[status(thm)],[f978,f371]) ).
fof(f1109,plain,
( ~ sQ29_spl
| sQ88_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f471,f1104]) ).
fof(f1110,plain,
( ~ sQ29_spl
| sQ88_spl ),
inference(contradiction_clause,[status(thm)],[f1109]) ).
fof(f1116,definition,
( sQ93_spl
<=> sK26_skl = pv5 ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1117,plain,
( ~ sQ93_spl
| sK26_skl = pv5 ),
inference(component_clause,[status(thm)],[f1116]) ).
fof(f1132,plain,
( sQ89_spl
| ~ sQ93_spl
| ~ leq(pv5,pv5) ),
inference(backward_demodulation,[status(thm)],[f1117,f987]) ).
fof(f1139,plain,
( sQ89_spl
| ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1132,f99]) ).
fof(f1140,plain,
( sQ89_spl
| ~ sQ93_spl ),
inference(contradiction_clause,[status(thm)],[f1139]) ).
fof(f1151,plain,
( sQ80_spl
| ~ leq(sK24_skl,pv5)
| ~ leq(sK23_skl,n2)
| ~ leq(n0,sK24_skl)
| ~ leq(n0,sK23_skl) ),
inference(resolution,[status(thm)],[f922,f285]) ).
fof(f1153,plain,
( sQ80_spl
| ~ sQ88_spl
| ~ sQ86_spl
| ~ sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1151,f951,f954,f957,f976,f920]) ).
fof(f1155,plain,
( sQ35_spl
| ~ leq(sK26_skl,pv5)
| ~ leq(sK25_skl,n2)
| ~ leq(n0,sK26_skl)
| ~ leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f494,f285]) ).
fof(f1156,plain,
( sQ35_spl
| ~ leq(sK26_skl,pred(pv5))
| ~ leq(sK25_skl,n2)
| ~ leq(n0,sK26_skl)
| ~ leq(n0,sK25_skl) ),
inference(resolution,[status(thm)],[f494,f510]) ).
fof(f1157,plain,
( sQ35_spl
| ~ sQ89_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1155,f473,f477,f481,f985,f492]) ).
fof(f1158,plain,
( sQ35_spl
| ~ sQ90_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1156,f473,f477,f481,f989,f492]) ).
fof(f1159,plain,
$false,
inference(sat_refutation,[status(thm)],[f476,f480,f484,f488,f495,f700,f702,f705,f708,f711,f714,f717,f720,f723,f726,f729,f732,f735,f738,f741,f744,f747,f750,f753,f756,f759,f762,f765,f768,f771,f774,f777,f780,f783,f785,f802,f857,f859,f874,f879,f923,f979,f988,f992,f994,f1020,f1079,f1094,f1103,f1110,f1140,f1153,f1157,f1158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV097+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.55 % Computer : n010.cluster.edu
% 0.10/0.55 % Model : x86_64 x86_64
% 0.10/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.55 % Memory : 8046.5625MB
% 0.10/0.55 % OS : Linux 6.8.0-71-generic
% 0.10/0.55 % CPULimit : 300
% 0.10/0.55 % WCLimit : 300
% 0.10/0.55 % DateTime : Mon Sep 21 08:31:15 UTC 2026
% 0.10/0.55 % CPUTime :
% 0.15/0.57 % Drodi V4.1.1
% 0.15/0.62 % Refutation found
% 0.15/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.65 % Elapsed time: 0.090864 seconds
% 0.15/0.65 % CPU time: 0.405585 seconds
% 0.15/0.65 % Total memory used: 117.104 MB
% 0.15/0.65 % Net memory used: 116.402 MB
%------------------------------------------------------------------------------