%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV096+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 09:06:48 AM UTC 2026
% Result : Theorem 24.57s 8.18s
% Output : CNFRefutation 24.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 2
% Syntax : Number of formulae : 344 ( 40 unt; 0 def)
% Number of atoms : 7171 (6257 equ)
% Maximal formula atoms : 192 ( 20 avg)
% Number of connectives : 13466 (6639 ~;6574 |; 247 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 21 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-3 aty)
% Number of variables : 30 ( 0 sgn 17 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(pred_minus_1,axiom,
! [X] : minus(X,n1) = pred(X),
file('theBenchmark.p',pred_minus_1) ).
fof(quaternion_ds1_inuse_0008,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(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 )
=> ( ! [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(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('theBenchmark.p',quaternion_ds1_inuse_0008) ).
fof(quaternion_ds1_inuse_0008_neg,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(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 )
=> ( ! [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(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(assume_negation,[status(cth)],[quaternion_ds1_inuse_0008]) ).
cnf(c_301,plain,
minus(A,n1) = pred(A),
inference(clausify,[status(thm)],[pred_minus_1]) ).
fof(nnf_57,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(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 )
& ! [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(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(fof_nnf,[status(thm)],[quaternion_ds1_inuse_0008_neg]) ).
fof(sk_quaternion_ds1_inuse_0008_neg_sk,plain,
( ( ( ( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use )
& leq(sK1,minus(pv5,n1))
& leq(sK0,n2)
& leq(n0,sK1)
& leq(n0,sK0) )
| ~ 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 )
& ! [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(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(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(C,sK0),skolemize(D,sK1)],[nnf_57]) ).
fof(sk_quaternion_ds1_inuse_0008_neg,plain,
( ( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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 )
& ( leq(sK1,minus(pv5,n1))
| ~ 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 )
& ( leq(sK0,n2)
| ~ 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 )
& ( leq(n0,sK1)
| ~ 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 )
& ( leq(n0,sK0)
| ~ 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 )
& ! [VAR_0,VAR_1] :
( a_select3(z_defuse,VAR_0,VAR_1) = use
| ~ leq(VAR_1,minus(pv5,n1))
| ~ leq(VAR_0,n2)
| ~ leq(n0,VAR_1)
| ~ leq(n0,VAR_0) )
& ! [VAR_0,VAR_1] :
( a_select3(u_defuse,VAR_0,VAR_1) = use
| ~ leq(VAR_1,minus(pv5,n1))
| ~ leq(VAR_0,n2)
| ~ leq(n0,VAR_1)
| ~ leq(n0,VAR_0) )
& 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(cnf_transformation,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg_sk]) ).
cnf(c_376,negated_conjecture,
a_select2(rho_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_377,negated_conjecture,
a_select2(rho_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_378,negated_conjecture,
a_select2(rho_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_379,negated_conjecture,
a_select2(sigma_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_380,negated_conjecture,
a_select2(sigma_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_381,negated_conjecture,
a_select2(sigma_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_382,negated_conjecture,
a_select2(sigma_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_383,negated_conjecture,
a_select2(sigma_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_384,negated_conjecture,
a_select2(sigma_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_385,negated_conjecture,
a_select3(u_defuse,n0,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_386,negated_conjecture,
a_select3(u_defuse,n1,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_387,negated_conjecture,
a_select3(u_defuse,n2,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_388,negated_conjecture,
a_select2(xinit_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_389,negated_conjecture,
a_select2(xinit_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_390,negated_conjecture,
a_select2(xinit_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_391,negated_conjecture,
a_select2(xinit_mean_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_392,negated_conjecture,
a_select2(xinit_mean_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_393,negated_conjecture,
a_select2(xinit_mean_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_394,negated_conjecture,
a_select2(xinit_mean_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_395,negated_conjecture,
a_select2(xinit_mean_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_396,negated_conjecture,
a_select2(xinit_mean_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_397,negated_conjecture,
a_select2(xinit_noise_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_398,negated_conjecture,
a_select2(xinit_noise_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_399,negated_conjecture,
a_select2(xinit_noise_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_400,negated_conjecture,
a_select2(xinit_noise_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_401,negated_conjecture,
a_select2(xinit_noise_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_402,negated_conjecture,
a_select2(xinit_noise_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_403,negated_conjecture,
leq(n0,pv5),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_405,negated_conjecture,
leq(pv5,minus(n999,n1)),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_406,negated_conjecture,
leq(pv5,pred(n999)),
inference(paramod,[status(thm)],[c_301,c_405]) ).
cnf(c_409,negated_conjecture,
( a_select3(u_defuse,A,B) = use
| ~ leq(B,minus(pv5,n1))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_410,negated_conjecture,
( a_select3(u_defuse,A,B) = use
| ~ leq(B,pred(pv5))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(paramod,[status(thm)],[c_301,c_409]) ).
cnf(c_411,negated_conjecture,
( a_select3(z_defuse,A,B) = use
| ~ leq(B,minus(pv5,n1))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_412,negated_conjecture,
( a_select3(z_defuse,A,B) = use
| ~ leq(B,pred(pv5))
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(paramod,[status(thm)],[c_301,c_411]) ).
cnf(c_413,negated_conjecture,
( leq(n0,sK0)
| ~ 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(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_4604,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use ),
inference(paramod,[status(thm)],[c_376,c_413]) ).
cnf(c_4605,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_377,c_4604]) ).
cnf(c_4606,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_378,c_4605]) ).
cnf(c_4607,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_379,c_4606]) ).
cnf(c_4608,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_380,c_4607]) ).
cnf(c_4609,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_381,c_4608]) ).
cnf(c_4610,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_382,c_4609]) ).
cnf(c_4611,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_383,c_4610]) ).
cnf(c_4612,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_384,c_4611]) ).
cnf(c_4613,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_385,c_4612]) ).
cnf(c_4614,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_386,c_4613]) ).
cnf(c_4615,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_387,c_4614]) ).
cnf(c_4616,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_388,c_4615]) ).
cnf(c_4617,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_389,c_4616]) ).
cnf(c_4618,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4617]) ).
cnf(c_4619,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_391,c_4618]) ).
cnf(c_4620,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_392,c_4619]) ).
cnf(c_4621,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_393,c_4620]) ).
cnf(c_4622,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_394,c_4621]) ).
cnf(c_4623,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_395,c_4622]) ).
cnf(c_4624,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_396,c_4623]) ).
cnf(c_4625,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_397,c_4624]) ).
cnf(c_4626,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_398,c_4625]) ).
cnf(c_4627,negated_conjecture,
( leq(n0,sK0)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_399,c_4626]) ).
cnf(c_4628,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_400,c_4627]) ).
cnf(c_4629,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_401,c_4628]) ).
cnf(c_4630,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_402,c_4629]) ).
cnf(c_4631,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4630]) ).
cnf(c_4632,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4631]) ).
cnf(c_4633,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4632]) ).
cnf(c_4634,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4633]) ).
cnf(c_4635,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4634]) ).
cnf(c_4636,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4635]) ).
cnf(c_4637,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4636]) ).
cnf(c_4638,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4637]) ).
cnf(c_4639,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4638]) ).
cnf(c_4640,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4639]) ).
cnf(c_4641,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4640]) ).
cnf(c_4642,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4641]) ).
cnf(c_4643,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4642]) ).
cnf(c_4644,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4643]) ).
cnf(c_4645,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4644]) ).
cnf(c_4646,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4645]) ).
cnf(c_4647,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4646]) ).
cnf(c_4648,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4647]) ).
cnf(c_4649,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4648]) ).
cnf(c_4650,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4649]) ).
cnf(c_4651,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4650]) ).
cnf(c_4652,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4651]) ).
cnf(c_4653,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4652]) ).
cnf(c_4654,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4653]) ).
cnf(c_4655,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4654]) ).
cnf(c_4656,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4655]) ).
cnf(c_4657,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4656]) ).
cnf(c_4658,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(copy,[status(thm)],[c_4657]) ).
cnf(c_4659,negated_conjecture,
( leq(n0,sK0)
| ~ leq(pv5,pred(n999)) ),
inference(resolve,[status(thm)],[c_403,c_4658]) ).
cnf(c_414,negated_conjecture,
leq(n0,sK0),
inference(resolve,[status(thm)],[c_406,c_4659]) ).
cnf(c_415,negated_conjecture,
( leq(n0,sK1)
| ~ 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(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_4660,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use ),
inference(paramod,[status(thm)],[c_376,c_415]) ).
cnf(c_4661,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_377,c_4660]) ).
cnf(c_4662,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_378,c_4661]) ).
cnf(c_4663,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_379,c_4662]) ).
cnf(c_4664,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_380,c_4663]) ).
cnf(c_4665,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_381,c_4664]) ).
cnf(c_4666,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_382,c_4665]) ).
cnf(c_4667,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_383,c_4666]) ).
cnf(c_4668,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_384,c_4667]) ).
cnf(c_4669,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_385,c_4668]) ).
cnf(c_4670,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_386,c_4669]) ).
cnf(c_4671,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_387,c_4670]) ).
cnf(c_4672,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_388,c_4671]) ).
cnf(c_4673,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_389,c_4672]) ).
cnf(c_4674,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4673]) ).
cnf(c_4675,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_391,c_4674]) ).
cnf(c_4676,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_392,c_4675]) ).
cnf(c_4677,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_393,c_4676]) ).
cnf(c_4678,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_394,c_4677]) ).
cnf(c_4679,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_395,c_4678]) ).
cnf(c_4680,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_396,c_4679]) ).
cnf(c_4681,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_397,c_4680]) ).
cnf(c_4682,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_398,c_4681]) ).
cnf(c_4683,negated_conjecture,
( leq(n0,sK1)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_399,c_4682]) ).
cnf(c_4684,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_400,c_4683]) ).
cnf(c_4685,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_401,c_4684]) ).
cnf(c_4686,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_402,c_4685]) ).
cnf(c_4687,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4686]) ).
cnf(c_4688,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4687]) ).
cnf(c_4689,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4688]) ).
cnf(c_4690,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4689]) ).
cnf(c_4691,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4690]) ).
cnf(c_4692,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4691]) ).
cnf(c_4693,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4692]) ).
cnf(c_4694,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4693]) ).
cnf(c_4695,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4694]) ).
cnf(c_4696,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4695]) ).
cnf(c_4697,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4696]) ).
cnf(c_4698,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4697]) ).
cnf(c_4699,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4698]) ).
cnf(c_4700,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4699]) ).
cnf(c_4701,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4700]) ).
cnf(c_4702,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4701]) ).
cnf(c_4703,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4702]) ).
cnf(c_4704,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4703]) ).
cnf(c_4705,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4704]) ).
cnf(c_4706,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4705]) ).
cnf(c_4707,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4706]) ).
cnf(c_4708,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4707]) ).
cnf(c_4709,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4708]) ).
cnf(c_4710,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4709]) ).
cnf(c_4711,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4710]) ).
cnf(c_4712,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4711]) ).
cnf(c_4713,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4712]) ).
cnf(c_4714,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(copy,[status(thm)],[c_4713]) ).
cnf(c_4715,negated_conjecture,
( leq(n0,sK1)
| ~ leq(pv5,pred(n999)) ),
inference(resolve,[status(thm)],[c_403,c_4714]) ).
cnf(c_416,negated_conjecture,
leq(n0,sK1),
inference(resolve,[status(thm)],[c_406,c_4715]) ).
cnf(c_417,negated_conjecture,
( leq(sK0,n2)
| ~ 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(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_4716,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use ),
inference(paramod,[status(thm)],[c_376,c_417]) ).
cnf(c_4717,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_377,c_4716]) ).
cnf(c_4718,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_378,c_4717]) ).
cnf(c_4719,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_379,c_4718]) ).
cnf(c_4720,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_380,c_4719]) ).
cnf(c_4721,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_381,c_4720]) ).
cnf(c_4722,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_382,c_4721]) ).
cnf(c_4723,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_383,c_4722]) ).
cnf(c_4724,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_384,c_4723]) ).
cnf(c_4725,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_385,c_4724]) ).
cnf(c_4726,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_386,c_4725]) ).
cnf(c_4727,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_387,c_4726]) ).
cnf(c_4728,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_388,c_4727]) ).
cnf(c_4729,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_389,c_4728]) ).
cnf(c_4730,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4729]) ).
cnf(c_4731,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_391,c_4730]) ).
cnf(c_4732,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_392,c_4731]) ).
cnf(c_4733,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_393,c_4732]) ).
cnf(c_4734,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_394,c_4733]) ).
cnf(c_4735,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_395,c_4734]) ).
cnf(c_4736,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_396,c_4735]) ).
cnf(c_4737,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_397,c_4736]) ).
cnf(c_4738,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_398,c_4737]) ).
cnf(c_4739,negated_conjecture,
( leq(sK0,n2)
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_399,c_4738]) ).
cnf(c_4740,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_400,c_4739]) ).
cnf(c_4741,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_401,c_4740]) ).
cnf(c_4742,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_402,c_4741]) ).
cnf(c_4743,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4742]) ).
cnf(c_4744,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4743]) ).
cnf(c_4745,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4744]) ).
cnf(c_4746,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4745]) ).
cnf(c_4747,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4746]) ).
cnf(c_4748,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4747]) ).
cnf(c_4749,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4748]) ).
cnf(c_4750,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4749]) ).
cnf(c_4751,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4750]) ).
cnf(c_4752,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4751]) ).
cnf(c_4753,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4752]) ).
cnf(c_4754,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4753]) ).
cnf(c_4755,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4754]) ).
cnf(c_4756,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4755]) ).
cnf(c_4757,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4756]) ).
cnf(c_4758,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4757]) ).
cnf(c_4759,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4758]) ).
cnf(c_4760,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4759]) ).
cnf(c_4761,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4760]) ).
cnf(c_4762,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4761]) ).
cnf(c_4763,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4762]) ).
cnf(c_4764,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4763]) ).
cnf(c_4765,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4764]) ).
cnf(c_4766,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4765]) ).
cnf(c_4767,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4766]) ).
cnf(c_4768,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4767]) ).
cnf(c_4769,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4768]) ).
cnf(c_4770,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(copy,[status(thm)],[c_4769]) ).
cnf(c_4771,negated_conjecture,
( leq(sK0,n2)
| ~ leq(pv5,pred(n999)) ),
inference(resolve,[status(thm)],[c_403,c_4770]) ).
cnf(c_418,negated_conjecture,
leq(sK0,n2),
inference(resolve,[status(thm)],[c_406,c_4771]) ).
cnf(c_419,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_4772,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use ),
inference(paramod,[status(thm)],[c_376,c_419]) ).
cnf(c_4773,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_377,c_4772]) ).
cnf(c_4774,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_378,c_4773]) ).
cnf(c_4775,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_379,c_4774]) ).
cnf(c_4776,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_380,c_4775]) ).
cnf(c_4777,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_381,c_4776]) ).
cnf(c_4778,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_382,c_4777]) ).
cnf(c_4779,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_383,c_4778]) ).
cnf(c_4780,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_384,c_4779]) ).
cnf(c_4781,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_385,c_4780]) ).
cnf(c_4782,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_386,c_4781]) ).
cnf(c_4783,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_387,c_4782]) ).
cnf(c_4784,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_388,c_4783]) ).
cnf(c_4785,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_389,c_4784]) ).
cnf(c_4786,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4785]) ).
cnf(c_4787,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_391,c_4786]) ).
cnf(c_4788,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_392,c_4787]) ).
cnf(c_4789,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_393,c_4788]) ).
cnf(c_4790,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_394,c_4789]) ).
cnf(c_4791,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_395,c_4790]) ).
cnf(c_4792,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_396,c_4791]) ).
cnf(c_4793,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_397,c_4792]) ).
cnf(c_4794,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_398,c_4793]) ).
cnf(c_4795,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_399,c_4794]) ).
cnf(c_4796,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_400,c_4795]) ).
cnf(c_4797,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_401,c_4796]) ).
cnf(c_4798,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_402,c_4797]) ).
cnf(c_4799,negated_conjecture,
( leq(sK1,minus(pv5,n1))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4798]) ).
cnf(c_4800,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4799]) ).
cnf(c_4801,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4800]) ).
cnf(c_4802,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4801]) ).
cnf(c_4803,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4802]) ).
cnf(c_4804,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4803]) ).
cnf(c_4805,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4804]) ).
cnf(c_4806,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4805]) ).
cnf(c_4807,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4806]) ).
cnf(c_4808,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4807]) ).
cnf(c_4809,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4808]) ).
cnf(c_4810,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4809]) ).
cnf(c_4811,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4810]) ).
cnf(c_4812,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4811]) ).
cnf(c_4813,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4812]) ).
cnf(c_4814,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4813]) ).
cnf(c_4815,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4814]) ).
cnf(c_4816,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4815]) ).
cnf(c_4817,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4816]) ).
cnf(c_4818,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4817]) ).
cnf(c_4819,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4818]) ).
cnf(c_4820,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4819]) ).
cnf(c_4821,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4820]) ).
cnf(c_4822,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4821]) ).
cnf(c_4823,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4822]) ).
cnf(c_4824,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4823]) ).
cnf(c_4825,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4824]) ).
cnf(c_4826,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4825]) ).
cnf(c_4827,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(copy,[status(thm)],[c_4826]) ).
cnf(c_4828,negated_conjecture,
( leq(sK1,pred(pv5))
| ~ leq(pv5,pred(n999)) ),
inference(resolve,[status(thm)],[c_403,c_4827]) ).
cnf(c_420,negated_conjecture,
leq(sK1,pred(pv5)),
inference(resolve,[status(thm)],[c_406,c_4828]) ).
cnf(c_421,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0008_neg]) ).
cnf(c_4829,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use ),
inference(paramod,[status(thm)],[c_376,c_421]) ).
cnf(c_4830,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_377,c_4829]) ).
cnf(c_4831,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_378,c_4830]) ).
cnf(c_4832,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_379,c_4831]) ).
cnf(c_4833,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_380,c_4832]) ).
cnf(c_4834,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_381,c_4833]) ).
cnf(c_4835,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_382,c_4834]) ).
cnf(c_4836,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_383,c_4835]) ).
cnf(c_4837,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_384,c_4836]) ).
cnf(c_4838,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_385,c_4837]) ).
cnf(c_4839,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_386,c_4838]) ).
cnf(c_4840,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_387,c_4839]) ).
cnf(c_4841,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_388,c_4840]) ).
cnf(c_4842,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_389,c_4841]) ).
cnf(c_4843,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4842]) ).
cnf(c_4844,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_391,c_4843]) ).
cnf(c_4845,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_392,c_4844]) ).
cnf(c_4846,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_393,c_4845]) ).
cnf(c_4847,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_394,c_4846]) ).
cnf(c_4848,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_395,c_4847]) ).
cnf(c_4849,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_396,c_4848]) ).
cnf(c_4850,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_397,c_4849]) ).
cnf(c_4851,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_398,c_4850]) ).
cnf(c_4852,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_399,c_4851]) ).
cnf(c_4853,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_400,c_4852]) ).
cnf(c_4854,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_401,c_4853]) ).
cnf(c_4855,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_402,c_4854]) ).
cnf(c_4856,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_301,c_4855]) ).
cnf(c_4857,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4856]) ).
cnf(c_4858,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4857]) ).
cnf(c_4859,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4858]) ).
cnf(c_4860,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4859]) ).
cnf(c_4861,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4860]) ).
cnf(c_4862,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4861]) ).
cnf(c_4863,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4862]) ).
cnf(c_4864,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4863]) ).
cnf(c_4865,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4864]) ).
cnf(c_4866,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4865]) ).
cnf(c_4867,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4866]) ).
cnf(c_4868,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4867]) ).
cnf(c_4869,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4868]) ).
cnf(c_4870,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4869]) ).
cnf(c_4871,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4870]) ).
cnf(c_4872,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4871]) ).
cnf(c_4873,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4872]) ).
cnf(c_4874,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4873]) ).
cnf(c_4875,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4874]) ).
cnf(c_4876,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4875]) ).
cnf(c_4877,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4876]) ).
cnf(c_4878,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4877]) ).
cnf(c_4879,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4878]) ).
cnf(c_4880,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4879]) ).
cnf(c_4881,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4880]) ).
cnf(c_4882,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4881]) ).
cnf(c_4883,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999))
| ~ leq(n0,pv5) ),
inference(copy,[status(thm)],[c_4882]) ).
cnf(c_4884,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| ~ leq(pv5,pred(n999)) ),
inference(resolve,[status(thm)],[c_403,c_4883]) ).
cnf(c_422,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use ),
inference(resolve,[status(thm)],[c_406,c_4884]) ).
cnf(c_4885,negated_conjecture,
( a_select3(z_defuse,sK0,A) = use
| ~ leq(A,pred(pv5))
| ~ leq(sK0,n2)
| ~ leq(n0,A) ),
inference(resolve,[status(thm)],[c_412,c_414]) ).
cnf(c_4886,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) = use
| ~ leq(sK1,pred(pv5))
| ~ leq(sK0,n2) ),
inference(resolve,[status(thm)],[c_4885,c_416]) ).
cnf(c_4887,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) = use
| ~ leq(sK1,pred(pv5)) ),
inference(resolve,[status(thm)],[c_4886,c_418]) ).
cnf(c_4372,negated_conjecture,
a_select3(z_defuse,sK0,sK1) = use,
inference(resolve,[status(thm)],[c_4887,c_420]) ).
cnf(c_4888,negated_conjecture,
( a_select3(u_defuse,sK0,A) = use
| ~ leq(A,pred(pv5))
| ~ leq(sK0,n2)
| ~ leq(n0,A) ),
inference(resolve,[status(thm)],[c_410,c_414]) ).
cnf(c_4889,negated_conjecture,
( a_select3(u_defuse,sK0,sK1) = use
| ~ leq(sK1,pred(pv5))
| ~ leq(sK0,n2) ),
inference(resolve,[status(thm)],[c_4888,c_416]) ).
cnf(c_4890,negated_conjecture,
( a_select3(u_defuse,sK0,sK1) = use
| ~ leq(sK1,pred(pv5)) ),
inference(resolve,[status(thm)],[c_4889,c_418]) ).
cnf(c_4373,negated_conjecture,
a_select3(u_defuse,sK0,sK1) = use,
inference(resolve,[status(thm)],[c_4890,c_420]) ).
cnf(c_4891,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| use != use ),
inference(paramod,[status(thm)],[c_4373,c_422]) ).
cnf(c_4892,negated_conjecture,
( use != use
| use != use ),
inference(paramod,[status(thm)],[c_4372,c_4891]) ).
cnf(c_4893,negated_conjecture,
use != use,
inference(copy,[status(thm)],[c_4892]) ).
cnf(c_4603,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_4893]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV096+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.57 % Computer : n001.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Sat Sep 26 13:17:43 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.58 % Process 1886054 was started by sandbox on n001,
% 0.10/0.58 % Sat Sep 26 13:17:43 2026
% 0.10/0.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.63
% 0.10/0.63 % From the command line: assign(max_seconds, 300).
% 24.57/8.18
% 24.57/8.18 % SZS status Theorem for theBenchmark
% 24.57/8.18
% 24.57/8.18 % Proof 1 at 3.17 (+ 0.26) seconds.
% 24.57/8.18 % Length of proof is 50.
% 24.57/8.18 % Level of proof is 5.
% 24.57/8.18 % Maximum clause weight is 29.000.
% 24.57/8.18 % Given clauses 336.
% 24.57/8.18
% 24.57/8.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------