%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV098+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:06:48 AM UTC 2026
% Result : Theorem 21.78s 3.29s
% Output : CNFRefutation 21.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 4
% Syntax : Number of formulae : 330 ( 41 unt; 0 def)
% Number of atoms : 6504 (6182 equ)
% Maximal formula atoms : 190 ( 19 avg)
% Number of connectives : 12153 (5979 ~;5917 |; 249 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 67 ( 20 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-3 aty)
% Number of variables : 42 ( 0 sgn 31 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(succ_plus_1_l,axiom,
! [X] : plus(n1,X) = succ(X),
file('theBenchmark.p',succ_plus_1_l) ).
fof(pred_minus_1,axiom,
! [X] : minus(X,n1) = pred(X),
file('theBenchmark.p',pred_minus_1) ).
fof(pred_succ,axiom,
! [X] : pred(succ(X)) = X,
file('theBenchmark.p',pred_succ) ).
fof(quaternion_ds1_inuse_0010,conjecture,
( ( ! [C,D] :
( ( leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
=> ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use ) )
& ! [A,B] :
( ( leq(B,pv5)
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use )
=> ( ! [E,F] :
( ( leq(F,minus(plus(n1,pv5),n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& 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_0010) ).
fof(quaternion_ds1_inuse_0010_neg,negated_conjecture,
~ ( ( ! [C,D] :
( ( leq(D,minus(pv5,n1))
& leq(C,n2)
& leq(n0,D)
& leq(n0,C) )
=> ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use ) )
& ! [A,B] :
( ( leq(B,pv5)
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use ) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use )
=> ( ! [E,F] :
( ( leq(F,minus(plus(n1,pv5),n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
=> ( a_select3(z_defuse,E,F) = use
& a_select3(u_defuse,E,F) = use ) )
& 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_0010]) ).
cnf(c_283,plain,
plus(n1,A) = succ(A),
inference(clausify,[status(thm)],[succ_plus_1_l]) ).
cnf(c_300,plain,
minus(A,n1) = pred(A),
inference(clausify,[status(thm)],[pred_minus_1]) ).
cnf(c_301,plain,
pred(succ(A)) = A,
inference(clausify,[status(thm)],[pred_succ]) ).
fof(nnf_56,plain,
( ( ? [E,F] :
( ( a_select3(z_defuse,E,F) != use
| a_select3(u_defuse,E,F) != use )
& leq(F,minus(plus(n1,pv5),n1))
& leq(E,n2)
& leq(n0,F)
& leq(n0,E) )
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use )
& ! [C,D] :
( ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use )
| ~ leq(D,minus(pv5,n1))
| ~ leq(C,n2)
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ),
inference(fof_nnf,[status(thm)],[quaternion_ds1_inuse_0010_neg]) ).
fof(sk_quaternion_ds1_inuse_0010_neg_sk,plain,
( ( ( ( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use )
& leq(sK1,minus(plus(n1,pv5),n1))
& leq(sK0,n2)
& leq(n0,sK1)
& leq(n0,sK0) )
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use )
& ! [C,D] :
( ( a_select3(z_defuse,C,D) = use
& a_select3(u_defuse,C,D) = use )
| ~ leq(D,minus(pv5,n1))
| ~ leq(C,n2)
| ~ leq(n0,D)
| ~ leq(n0,C) )
& ! [A,B] :
( ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = use )
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(E,sK0),skolemize(F,sK1)],[nnf_56]) ).
fof(sk_quaternion_ds1_inuse_0010_neg,plain,
( ( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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(plus(n1,pv5),n1))
| 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)
| 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)
| 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)
| 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) )
& ! [VAR_0,VAR_1] :
( a_select3(z_defuse,VAR_0,VAR_1) = use
| ~ leq(VAR_1,pv5)
| ~ 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,pv5)
| ~ leq(VAR_0,n2)
| ~ leq(n0,VAR_1)
| ~ leq(n0,VAR_0) )
& leq(pv5,minus(n999,n1))
& leq(n0,pv5)
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use ),
inference(cnf_transformation,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg_sk]) ).
cnf(c_364,negated_conjecture,
a_select2(rho_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_365,negated_conjecture,
a_select2(rho_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_366,negated_conjecture,
a_select2(rho_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_367,negated_conjecture,
a_select2(sigma_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_368,negated_conjecture,
a_select2(sigma_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_369,negated_conjecture,
a_select2(sigma_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_370,negated_conjecture,
a_select2(sigma_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_371,negated_conjecture,
a_select2(sigma_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_372,negated_conjecture,
a_select2(sigma_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_373,negated_conjecture,
a_select3(u_defuse,n0,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_374,negated_conjecture,
a_select3(u_defuse,n1,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_375,negated_conjecture,
a_select3(u_defuse,n2,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_376,negated_conjecture,
a_select2(xinit_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_377,negated_conjecture,
a_select2(xinit_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_378,negated_conjecture,
a_select2(xinit_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_379,negated_conjecture,
a_select2(xinit_mean_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_380,negated_conjecture,
a_select2(xinit_mean_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_381,negated_conjecture,
a_select2(xinit_mean_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_382,negated_conjecture,
a_select2(xinit_mean_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_383,negated_conjecture,
a_select2(xinit_mean_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_384,negated_conjecture,
a_select2(xinit_mean_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_385,negated_conjecture,
a_select2(xinit_noise_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_386,negated_conjecture,
a_select2(xinit_noise_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_387,negated_conjecture,
a_select2(xinit_noise_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_388,negated_conjecture,
a_select2(xinit_noise_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_389,negated_conjecture,
a_select2(xinit_noise_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_390,negated_conjecture,
a_select2(xinit_noise_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_394,negated_conjecture,
( a_select3(u_defuse,A,B) = use
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_395,negated_conjecture,
( a_select3(z_defuse,A,B) = use
| ~ leq(B,pv5)
| ~ leq(A,n2)
| ~ leq(n0,B)
| ~ leq(n0,A) ),
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0010_neg]) ).
cnf(c_400,negated_conjecture,
( leq(n0,sK0)
| 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_0010_neg]) ).
cnf(c_4073,negated_conjecture,
( leq(n0,sK0)
| 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_364,c_400]) ).
cnf(c_4074,negated_conjecture,
( leq(n0,sK0)
| 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_365,c_4073]) ).
cnf(c_4075,negated_conjecture,
( leq(n0,sK0)
| 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_366,c_4074]) ).
cnf(c_4076,negated_conjecture,
( leq(n0,sK0)
| 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_367,c_4075]) ).
cnf(c_4077,negated_conjecture,
( leq(n0,sK0)
| 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_368,c_4076]) ).
cnf(c_4078,negated_conjecture,
( leq(n0,sK0)
| 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_369,c_4077]) ).
cnf(c_4079,negated_conjecture,
( leq(n0,sK0)
| 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_370,c_4078]) ).
cnf(c_4080,negated_conjecture,
( leq(n0,sK0)
| 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_371,c_4079]) ).
cnf(c_4081,negated_conjecture,
( leq(n0,sK0)
| 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_372,c_4080]) ).
cnf(c_4082,negated_conjecture,
( leq(n0,sK0)
| 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_373,c_4081]) ).
cnf(c_4083,negated_conjecture,
( leq(n0,sK0)
| 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_374,c_4082]) ).
cnf(c_4084,negated_conjecture,
( leq(n0,sK0)
| 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_375,c_4083]) ).
cnf(c_4085,negated_conjecture,
( leq(n0,sK0)
| 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_376,c_4084]) ).
cnf(c_4086,negated_conjecture,
( leq(n0,sK0)
| 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_377,c_4085]) ).
cnf(c_4087,negated_conjecture,
( leq(n0,sK0)
| 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_378,c_4086]) ).
cnf(c_4088,negated_conjecture,
( leq(n0,sK0)
| 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_379,c_4087]) ).
cnf(c_4089,negated_conjecture,
( leq(n0,sK0)
| 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_380,c_4088]) ).
cnf(c_4090,negated_conjecture,
( leq(n0,sK0)
| 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_381,c_4089]) ).
cnf(c_4091,negated_conjecture,
( leq(n0,sK0)
| 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_382,c_4090]) ).
cnf(c_4092,negated_conjecture,
( leq(n0,sK0)
| 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_383,c_4091]) ).
cnf(c_4093,negated_conjecture,
( leq(n0,sK0)
| 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_384,c_4092]) ).
cnf(c_4094,negated_conjecture,
( leq(n0,sK0)
| 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_385,c_4093]) ).
cnf(c_4095,negated_conjecture,
( leq(n0,sK0)
| 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_386,c_4094]) ).
cnf(c_4096,negated_conjecture,
( leq(n0,sK0)
| 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_387,c_4095]) ).
cnf(c_4097,negated_conjecture,
( leq(n0,sK0)
| 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_388,c_4096]) ).
cnf(c_4098,negated_conjecture,
( leq(n0,sK0)
| 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_389,c_4097]) ).
cnf(c_4099,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4098]) ).
cnf(c_4100,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4099]) ).
cnf(c_4101,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4100]) ).
cnf(c_4102,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4101]) ).
cnf(c_4103,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4102]) ).
cnf(c_4104,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4103]) ).
cnf(c_4105,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4104]) ).
cnf(c_4106,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4105]) ).
cnf(c_4107,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4106]) ).
cnf(c_4108,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4107]) ).
cnf(c_4109,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4108]) ).
cnf(c_4110,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| 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_4109]) ).
cnf(c_4111,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| 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_4110]) ).
cnf(c_4112,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| 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_4111]) ).
cnf(c_4113,negated_conjecture,
( leq(n0,sK0)
| use != use
| 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_4112]) ).
cnf(c_4114,negated_conjecture,
( leq(n0,sK0)
| 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_4113]) ).
cnf(c_4115,negated_conjecture,
( leq(n0,sK0)
| 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_4114]) ).
cnf(c_4116,negated_conjecture,
( leq(n0,sK0)
| 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_4115]) ).
cnf(c_4117,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4116]) ).
cnf(c_4118,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4117]) ).
cnf(c_4119,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4118]) ).
cnf(c_4120,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4119]) ).
cnf(c_4121,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4120]) ).
cnf(c_4122,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4121]) ).
cnf(c_4123,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4122]) ).
cnf(c_4124,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4123]) ).
cnf(c_4125,negated_conjecture,
( leq(n0,sK0)
| use != use ),
inference(copy,[status(thm)],[c_4124]) ).
cnf(c_401,negated_conjecture,
leq(n0,sK0),
inference(copy,[status(thm)],[c_4125]) ).
cnf(c_402,negated_conjecture,
( leq(n0,sK1)
| 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_0010_neg]) ).
cnf(c_4126,negated_conjecture,
( leq(n0,sK1)
| 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_364,c_402]) ).
cnf(c_4127,negated_conjecture,
( leq(n0,sK1)
| 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_365,c_4126]) ).
cnf(c_4128,negated_conjecture,
( leq(n0,sK1)
| 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_366,c_4127]) ).
cnf(c_4129,negated_conjecture,
( leq(n0,sK1)
| 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_367,c_4128]) ).
cnf(c_4130,negated_conjecture,
( leq(n0,sK1)
| 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_368,c_4129]) ).
cnf(c_4131,negated_conjecture,
( leq(n0,sK1)
| 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_369,c_4130]) ).
cnf(c_4132,negated_conjecture,
( leq(n0,sK1)
| 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_370,c_4131]) ).
cnf(c_4133,negated_conjecture,
( leq(n0,sK1)
| 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_371,c_4132]) ).
cnf(c_4134,negated_conjecture,
( leq(n0,sK1)
| 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_372,c_4133]) ).
cnf(c_4135,negated_conjecture,
( leq(n0,sK1)
| 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_373,c_4134]) ).
cnf(c_4136,negated_conjecture,
( leq(n0,sK1)
| 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_374,c_4135]) ).
cnf(c_4137,negated_conjecture,
( leq(n0,sK1)
| 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_375,c_4136]) ).
cnf(c_4138,negated_conjecture,
( leq(n0,sK1)
| 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_376,c_4137]) ).
cnf(c_4139,negated_conjecture,
( leq(n0,sK1)
| 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_377,c_4138]) ).
cnf(c_4140,negated_conjecture,
( leq(n0,sK1)
| 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_378,c_4139]) ).
cnf(c_4141,negated_conjecture,
( leq(n0,sK1)
| 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_379,c_4140]) ).
cnf(c_4142,negated_conjecture,
( leq(n0,sK1)
| 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_380,c_4141]) ).
cnf(c_4143,negated_conjecture,
( leq(n0,sK1)
| 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_381,c_4142]) ).
cnf(c_4144,negated_conjecture,
( leq(n0,sK1)
| 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_382,c_4143]) ).
cnf(c_4145,negated_conjecture,
( leq(n0,sK1)
| 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_383,c_4144]) ).
cnf(c_4146,negated_conjecture,
( leq(n0,sK1)
| 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_384,c_4145]) ).
cnf(c_4147,negated_conjecture,
( leq(n0,sK1)
| 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_385,c_4146]) ).
cnf(c_4148,negated_conjecture,
( leq(n0,sK1)
| 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_386,c_4147]) ).
cnf(c_4149,negated_conjecture,
( leq(n0,sK1)
| 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_387,c_4148]) ).
cnf(c_4150,negated_conjecture,
( leq(n0,sK1)
| 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_388,c_4149]) ).
cnf(c_4151,negated_conjecture,
( leq(n0,sK1)
| 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_389,c_4150]) ).
cnf(c_4152,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4151]) ).
cnf(c_4153,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4152]) ).
cnf(c_4154,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4153]) ).
cnf(c_4155,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4154]) ).
cnf(c_4156,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4155]) ).
cnf(c_4157,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4156]) ).
cnf(c_4158,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4157]) ).
cnf(c_4159,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4158]) ).
cnf(c_4160,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4159]) ).
cnf(c_4161,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4160]) ).
cnf(c_4162,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4161]) ).
cnf(c_4163,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| 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_4162]) ).
cnf(c_4164,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| 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_4163]) ).
cnf(c_4165,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| 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_4164]) ).
cnf(c_4166,negated_conjecture,
( leq(n0,sK1)
| use != use
| 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_4165]) ).
cnf(c_4167,negated_conjecture,
( leq(n0,sK1)
| 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_4166]) ).
cnf(c_4168,negated_conjecture,
( leq(n0,sK1)
| 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_4167]) ).
cnf(c_4169,negated_conjecture,
( leq(n0,sK1)
| 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_4168]) ).
cnf(c_4170,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4169]) ).
cnf(c_4171,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4170]) ).
cnf(c_4172,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4171]) ).
cnf(c_4173,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4172]) ).
cnf(c_4174,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4173]) ).
cnf(c_4175,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4174]) ).
cnf(c_4176,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4175]) ).
cnf(c_4177,negated_conjecture,
( leq(n0,sK1)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4176]) ).
cnf(c_4178,negated_conjecture,
( leq(n0,sK1)
| use != use ),
inference(copy,[status(thm)],[c_4177]) ).
cnf(c_403,negated_conjecture,
leq(n0,sK1),
inference(copy,[status(thm)],[c_4178]) ).
cnf(c_404,negated_conjecture,
( leq(sK0,n2)
| 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_0010_neg]) ).
cnf(c_4179,negated_conjecture,
( leq(sK0,n2)
| 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_364,c_404]) ).
cnf(c_4180,negated_conjecture,
( leq(sK0,n2)
| 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_365,c_4179]) ).
cnf(c_4181,negated_conjecture,
( leq(sK0,n2)
| 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_366,c_4180]) ).
cnf(c_4182,negated_conjecture,
( leq(sK0,n2)
| 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_367,c_4181]) ).
cnf(c_4183,negated_conjecture,
( leq(sK0,n2)
| 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_368,c_4182]) ).
cnf(c_4184,negated_conjecture,
( leq(sK0,n2)
| 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_369,c_4183]) ).
cnf(c_4185,negated_conjecture,
( leq(sK0,n2)
| 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_370,c_4184]) ).
cnf(c_4186,negated_conjecture,
( leq(sK0,n2)
| 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_371,c_4185]) ).
cnf(c_4187,negated_conjecture,
( leq(sK0,n2)
| 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_372,c_4186]) ).
cnf(c_4188,negated_conjecture,
( leq(sK0,n2)
| 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_373,c_4187]) ).
cnf(c_4189,negated_conjecture,
( leq(sK0,n2)
| 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_374,c_4188]) ).
cnf(c_4190,negated_conjecture,
( leq(sK0,n2)
| 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_375,c_4189]) ).
cnf(c_4191,negated_conjecture,
( leq(sK0,n2)
| 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_376,c_4190]) ).
cnf(c_4192,negated_conjecture,
( leq(sK0,n2)
| 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_377,c_4191]) ).
cnf(c_4193,negated_conjecture,
( leq(sK0,n2)
| 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_378,c_4192]) ).
cnf(c_4194,negated_conjecture,
( leq(sK0,n2)
| 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_379,c_4193]) ).
cnf(c_4195,negated_conjecture,
( leq(sK0,n2)
| 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_380,c_4194]) ).
cnf(c_4196,negated_conjecture,
( leq(sK0,n2)
| 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_381,c_4195]) ).
cnf(c_4197,negated_conjecture,
( leq(sK0,n2)
| 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_382,c_4196]) ).
cnf(c_4198,negated_conjecture,
( leq(sK0,n2)
| 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_383,c_4197]) ).
cnf(c_4199,negated_conjecture,
( leq(sK0,n2)
| 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_384,c_4198]) ).
cnf(c_4200,negated_conjecture,
( leq(sK0,n2)
| 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_385,c_4199]) ).
cnf(c_4201,negated_conjecture,
( leq(sK0,n2)
| 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_386,c_4200]) ).
cnf(c_4202,negated_conjecture,
( leq(sK0,n2)
| 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_387,c_4201]) ).
cnf(c_4203,negated_conjecture,
( leq(sK0,n2)
| 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_388,c_4202]) ).
cnf(c_4204,negated_conjecture,
( leq(sK0,n2)
| 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_389,c_4203]) ).
cnf(c_4205,negated_conjecture,
( leq(sK0,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 != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4204]) ).
cnf(c_4206,negated_conjecture,
( leq(sK0,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 != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4205]) ).
cnf(c_4207,negated_conjecture,
( leq(sK0,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 != use
| use != use ),
inference(copy,[status(thm)],[c_4206]) ).
cnf(c_4208,negated_conjecture,
( leq(sK0,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 != use ),
inference(copy,[status(thm)],[c_4207]) ).
cnf(c_4209,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4208]) ).
cnf(c_4210,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4209]) ).
cnf(c_4211,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4210]) ).
cnf(c_4212,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4211]) ).
cnf(c_4213,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4212]) ).
cnf(c_4214,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4213]) ).
cnf(c_4215,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4214]) ).
cnf(c_4216,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4215]) ).
cnf(c_4217,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4216]) ).
cnf(c_4218,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4217]) ).
cnf(c_4219,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4218]) ).
cnf(c_4220,negated_conjecture,
( leq(sK0,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 ),
inference(copy,[status(thm)],[c_4219]) ).
cnf(c_4221,negated_conjecture,
( leq(sK0,n2)
| 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_4220]) ).
cnf(c_4222,negated_conjecture,
( leq(sK0,n2)
| 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_4221]) ).
cnf(c_4223,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4222]) ).
cnf(c_4224,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4223]) ).
cnf(c_4225,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4224]) ).
cnf(c_4226,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4225]) ).
cnf(c_4227,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4226]) ).
cnf(c_4228,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4227]) ).
cnf(c_4229,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4228]) ).
cnf(c_4230,negated_conjecture,
( leq(sK0,n2)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4229]) ).
cnf(c_4231,negated_conjecture,
( leq(sK0,n2)
| use != use ),
inference(copy,[status(thm)],[c_4230]) ).
cnf(c_405,negated_conjecture,
leq(sK0,n2),
inference(copy,[status(thm)],[c_4231]) ).
cnf(c_406,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_0010_neg]) ).
cnf(c_4232,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_364,c_406]) ).
cnf(c_4233,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_365,c_4232]) ).
cnf(c_4234,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_366,c_4233]) ).
cnf(c_4235,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_367,c_4234]) ).
cnf(c_4236,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_368,c_4235]) ).
cnf(c_4237,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_369,c_4236]) ).
cnf(c_4238,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_370,c_4237]) ).
cnf(c_4239,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_371,c_4238]) ).
cnf(c_4240,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_372,c_4239]) ).
cnf(c_4241,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_373,c_4240]) ).
cnf(c_4242,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_374,c_4241]) ).
cnf(c_4243,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_375,c_4242]) ).
cnf(c_4244,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_376,c_4243]) ).
cnf(c_4245,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_377,c_4244]) ).
cnf(c_4246,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_378,c_4245]) ).
cnf(c_4247,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_379,c_4246]) ).
cnf(c_4248,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_380,c_4247]) ).
cnf(c_4249,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_381,c_4248]) ).
cnf(c_4250,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_382,c_4249]) ).
cnf(c_4251,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_383,c_4250]) ).
cnf(c_4252,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_384,c_4251]) ).
cnf(c_4253,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_385,c_4252]) ).
cnf(c_4254,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_386,c_4253]) ).
cnf(c_4255,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_387,c_4254]) ).
cnf(c_4256,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_388,c_4255]) ).
cnf(c_4257,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),n1))
| 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_389,c_4256]) ).
cnf(c_4258,negated_conjecture,
( leq(sK1,minus(plus(n1,pv5),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 != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_390,c_4257]) ).
cnf(c_4259,negated_conjecture,
( leq(sK1,minus(succ(pv5),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 != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_283,c_4258]) ).
cnf(c_4260,negated_conjecture,
( leq(sK1,pred(succ(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_300,c_4259]) ).
cnf(c_4261,negated_conjecture,
( leq(sK1,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_4260]) ).
cnf(c_4262,negated_conjecture,
( leq(sK1,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_4261]) ).
cnf(c_4263,negated_conjecture,
( leq(sK1,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_4262]) ).
cnf(c_4264,negated_conjecture,
( leq(sK1,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_4263]) ).
cnf(c_4265,negated_conjecture,
( leq(sK1,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_4264]) ).
cnf(c_4266,negated_conjecture,
( leq(sK1,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_4265]) ).
cnf(c_4267,negated_conjecture,
( leq(sK1,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_4266]) ).
cnf(c_4268,negated_conjecture,
( leq(sK1,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_4267]) ).
cnf(c_4269,negated_conjecture,
( leq(sK1,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_4268]) ).
cnf(c_4270,negated_conjecture,
( leq(sK1,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_4269]) ).
cnf(c_4271,negated_conjecture,
( leq(sK1,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_4270]) ).
cnf(c_4272,negated_conjecture,
( leq(sK1,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_4271]) ).
cnf(c_4273,negated_conjecture,
( leq(sK1,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_4272]) ).
cnf(c_4274,negated_conjecture,
( leq(sK1,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_4273]) ).
cnf(c_4275,negated_conjecture,
( leq(sK1,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_4274]) ).
cnf(c_4276,negated_conjecture,
( leq(sK1,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_4275]) ).
cnf(c_4277,negated_conjecture,
( leq(sK1,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_4276]) ).
cnf(c_4278,negated_conjecture,
( leq(sK1,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_4277]) ).
cnf(c_4279,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4278]) ).
cnf(c_4280,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4279]) ).
cnf(c_4281,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4280]) ).
cnf(c_4282,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4281]) ).
cnf(c_4283,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4282]) ).
cnf(c_4284,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4283]) ).
cnf(c_4285,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4284]) ).
cnf(c_4286,negated_conjecture,
( leq(sK1,pv5)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4285]) ).
cnf(c_4287,negated_conjecture,
( leq(sK1,pv5)
| use != use ),
inference(copy,[status(thm)],[c_4286]) ).
cnf(c_407,negated_conjecture,
leq(sK1,pv5),
inference(copy,[status(thm)],[c_4287]) ).
cnf(c_408,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_0010_neg]) ).
cnf(c_4288,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_364,c_408]) ).
cnf(c_4289,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_365,c_4288]) ).
cnf(c_4290,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_366,c_4289]) ).
cnf(c_4291,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_367,c_4290]) ).
cnf(c_4292,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_368,c_4291]) ).
cnf(c_4293,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_369,c_4292]) ).
cnf(c_4294,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_370,c_4293]) ).
cnf(c_4295,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_371,c_4294]) ).
cnf(c_4296,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_372,c_4295]) ).
cnf(c_4297,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_373,c_4296]) ).
cnf(c_4298,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_374,c_4297]) ).
cnf(c_4299,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_375,c_4298]) ).
cnf(c_4300,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_376,c_4299]) ).
cnf(c_4301,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_377,c_4300]) ).
cnf(c_4302,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_378,c_4301]) ).
cnf(c_4303,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_379,c_4302]) ).
cnf(c_4304,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_380,c_4303]) ).
cnf(c_4305,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_381,c_4304]) ).
cnf(c_4306,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_382,c_4305]) ).
cnf(c_4307,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_383,c_4306]) ).
cnf(c_4308,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_384,c_4307]) ).
cnf(c_4309,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_385,c_4308]) ).
cnf(c_4310,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_386,c_4309]) ).
cnf(c_4311,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_387,c_4310]) ).
cnf(c_4312,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_388,c_4311]) ).
cnf(c_4313,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_389,c_4312]) ).
cnf(c_4314,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4313]) ).
cnf(c_4315,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4314]) ).
cnf(c_4316,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4315]) ).
cnf(c_4317,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4316]) ).
cnf(c_4318,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4317]) ).
cnf(c_4319,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4318]) ).
cnf(c_4320,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4319]) ).
cnf(c_4321,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4320]) ).
cnf(c_4322,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4321]) ).
cnf(c_4323,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4322]) ).
cnf(c_4324,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| 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_4323]) ).
cnf(c_4325,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| 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_4324]) ).
cnf(c_4326,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| 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_4325]) ).
cnf(c_4327,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| 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_4326]) ).
cnf(c_4328,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| 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_4327]) ).
cnf(c_4329,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| 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_4328]) ).
cnf(c_4330,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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_4329]) ).
cnf(c_4331,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != 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_4330]) ).
cnf(c_4332,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4331]) ).
cnf(c_4333,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4332]) ).
cnf(c_4334,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4333]) ).
cnf(c_4335,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4334]) ).
cnf(c_4336,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4335]) ).
cnf(c_4337,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4336]) ).
cnf(c_4338,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4337]) ).
cnf(c_4339,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_4338]) ).
cnf(c_4340,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use
| use != use ),
inference(copy,[status(thm)],[c_4339]) ).
cnf(c_409,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| a_select3(u_defuse,sK0,sK1) != use ),
inference(copy,[status(thm)],[c_4340]) ).
cnf(c_4341,negated_conjecture,
( a_select3(z_defuse,sK0,A) = use
| ~ leq(A,pv5)
| ~ leq(sK0,n2)
| ~ leq(n0,A) ),
inference(resolve,[status(thm)],[c_395,c_401]) ).
cnf(c_4342,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) = use
| ~ leq(sK1,pv5)
| ~ leq(sK0,n2) ),
inference(resolve,[status(thm)],[c_4341,c_403]) ).
cnf(c_4343,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) = use
| ~ leq(sK1,pv5) ),
inference(resolve,[status(thm)],[c_4342,c_405]) ).
cnf(c_3723,negated_conjecture,
a_select3(z_defuse,sK0,sK1) = use,
inference(resolve,[status(thm)],[c_4343,c_407]) ).
cnf(c_4344,negated_conjecture,
( a_select3(u_defuse,sK0,A) = use
| ~ leq(A,pv5)
| ~ leq(sK0,n2)
| ~ leq(n0,A) ),
inference(resolve,[status(thm)],[c_394,c_401]) ).
cnf(c_4345,negated_conjecture,
( a_select3(u_defuse,sK0,sK1) = use
| ~ leq(sK1,pv5)
| ~ leq(sK0,n2) ),
inference(resolve,[status(thm)],[c_4344,c_403]) ).
cnf(c_4346,negated_conjecture,
( a_select3(u_defuse,sK0,sK1) = use
| ~ leq(sK1,pv5) ),
inference(resolve,[status(thm)],[c_4345,c_405]) ).
cnf(c_3724,negated_conjecture,
a_select3(u_defuse,sK0,sK1) = use,
inference(resolve,[status(thm)],[c_4346,c_407]) ).
cnf(c_4347,negated_conjecture,
( a_select3(z_defuse,sK0,sK1) != use
| use != use ),
inference(paramod,[status(thm)],[c_3724,c_409]) ).
cnf(c_4348,negated_conjecture,
( use != use
| use != use ),
inference(paramod,[status(thm)],[c_3723,c_4347]) ).
cnf(c_4349,negated_conjecture,
use != use,
inference(copy,[status(thm)],[c_4348]) ).
cnf(c_4072,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_4349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV098+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.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 13:12:15 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 223747 was started by sandbox on n009,
% 0.08/0.36 % Sat Sep 26 13:12:15 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.42
% 0.13/0.42 % From the command line: assign(max_seconds, 300).
% 21.78/3.29
% 21.78/3.29 % SZS status Theorem for theBenchmark
% 21.78/3.29
% 21.78/3.29 % Proof 1 at 2.55 (+ 0.23) seconds.
% 21.78/3.29 % Length of proof is 49.
% 21.78/3.29 % Level of proof is 4.
% 21.78/3.29 % Maximum clause weight is 28.000.
% 21.78/3.29 % Given clauses 327.
% 21.78/3.29
% 21.78/3.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------