%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV092+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:06:47 AM UTC 2026
% Result : Theorem 7.97s 2.69s
% Output : CNFRefutation 7.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 8
% Syntax : Number of formulae : 168 ( 46 unt; 0 def)
% Number of atoms : 2822 (2668 equ)
% Maximal formula atoms : 168 ( 16 avg)
% Number of connectives : 5099 (2445 ~;2439 |; 208 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 17 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-3 aty)
% Number of variables : 22 ( 0 sgn 12 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(irreflexivity_gt,axiom,
! [X] : ~ gt(X,X),
file('theBenchmark.p',irreflexivity_gt) ).
fof(leq_succ,axiom,
! [X,Y] :
( leq(X,Y)
=> leq(X,succ(Y)) ),
file('theBenchmark.p',leq_succ) ).
fof(leq_succ_gt_equiv,axiom,
! [X,Y] :
( leq(X,Y)
<=> gt(succ(Y),X) ),
file('theBenchmark.p',leq_succ_gt_equiv) ).
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(finite_domain_0,axiom,
! [X] :
( ( leq(X,n0)
& leq(n0,X) )
=> X = n0 ),
file('theBenchmark.p',finite_domain_0) ).
fof(quaternion_ds1_inuse_0004,conjecture,
( ( a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use )
=> ( ! [A,B] :
( ( leq(B,minus(n0,n1))
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = 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_0004) ).
fof(quaternion_ds1_inuse_0004_neg,negated_conjecture,
~ ( ( a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use
& a_select2(sigma_defuse,n5) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(rho_defuse,n2) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n0) = use )
=> ( ! [A,B] :
( ( leq(B,minus(n0,n1))
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
=> ( a_select3(z_defuse,A,B) = use
& a_select3(u_defuse,A,B) = 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_0004]) ).
cnf(c_63,plain,
~ gt(A,A),
inference(clausify,[status(thm)],[irreflexivity_gt]) ).
cnf(c_71,plain,
( leq(A,succ(B))
| ~ leq(A,B) ),
inference(clausify,[status(thm)],[leq_succ]) ).
cnf(c_72,plain,
( gt(succ(B),A)
| ~ leq(A,B) ),
inference(clausify,[status(thm)],[leq_succ_gt_equiv]) ).
fof(succ_tptp_minus_1,axiom,
succ(tptp_minus_1) = n0,
file('theBenchmark.p',succ_tptp_minus_1) ).
cnf(c_281,plain,
succ(tptp_minus_1) = n0,
inference(clausify,[status(thm)],[succ_tptp_minus_1]) ).
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]) ).
cnf(c_344,plain,
( n0 = A
| ~ leq(A,n0)
| ~ leq(n0,A) ),
inference(clausify,[status(thm)],[finite_domain_0]) ).
fof(nnf_56,plain,
( ( ? [A,B] :
( ( a_select3(z_defuse,A,B) != use
| a_select3(u_defuse,A,B) != use )
& leq(B,minus(n0,n1))
& leq(A,n2)
& leq(n0,B)
& leq(n0,A) )
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use )
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_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_0004_neg]) ).
fof(sk_quaternion_ds1_inuse_0004_neg_sk,plain,
( ( ( ( a_select3(z_defuse,sK1,sK0) != use
| a_select3(u_defuse,sK1,sK0) != use )
& leq(sK0,minus(n0,n1))
& leq(sK1,n2)
& leq(n0,sK0)
& 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 )
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_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,[sK1,sK0]),skolemize(A,sK1),skolemize(B,sK0)],[nnf_56]) ).
fof(sk_quaternion_ds1_inuse_0004_neg,plain,
( ( a_select3(z_defuse,sK1,sK0) != use
| a_select3(u_defuse,sK1,sK0) != 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(sK0,minus(n0,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(sK1,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,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 )
& ( 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 )
& a_select2(xinit_noise_defuse,n5) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_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_0004_neg_sk]) ).
cnf(c_357,negated_conjecture,
a_select2(rho_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_358,negated_conjecture,
a_select2(rho_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_359,negated_conjecture,
a_select2(rho_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_360,negated_conjecture,
a_select2(sigma_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_361,negated_conjecture,
a_select2(sigma_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_362,negated_conjecture,
a_select2(sigma_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_363,negated_conjecture,
a_select2(sigma_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_364,negated_conjecture,
a_select2(sigma_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_365,negated_conjecture,
a_select2(sigma_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_366,negated_conjecture,
a_select3(u_defuse,n0,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_367,negated_conjecture,
a_select3(u_defuse,n1,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_368,negated_conjecture,
a_select3(u_defuse,n2,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_369,negated_conjecture,
a_select2(xinit_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_370,negated_conjecture,
a_select2(xinit_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_371,negated_conjecture,
a_select2(xinit_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_372,negated_conjecture,
a_select2(xinit_mean_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_373,negated_conjecture,
a_select2(xinit_mean_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_374,negated_conjecture,
a_select2(xinit_mean_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_375,negated_conjecture,
a_select2(xinit_mean_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_376,negated_conjecture,
a_select2(xinit_mean_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_377,negated_conjecture,
a_select2(xinit_mean_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_378,negated_conjecture,
a_select2(xinit_noise_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_379,negated_conjecture,
a_select2(xinit_noise_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_380,negated_conjecture,
a_select2(xinit_noise_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_381,negated_conjecture,
a_select2(xinit_noise_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_382,negated_conjecture,
a_select2(xinit_noise_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_383,negated_conjecture,
a_select2(xinit_noise_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[sk_quaternion_ds1_inuse_0004_neg]) ).
cnf(c_386,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_0004_neg]) ).
cnf(c_2923,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_357,c_386]) ).
cnf(c_2924,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_358,c_2923]) ).
cnf(c_2925,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_359,c_2924]) ).
cnf(c_2926,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_360,c_2925]) ).
cnf(c_2927,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_361,c_2926]) ).
cnf(c_2928,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_362,c_2927]) ).
cnf(c_2929,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_363,c_2928]) ).
cnf(c_2930,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_364,c_2929]) ).
cnf(c_2931,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_365,c_2930]) ).
cnf(c_2932,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_366,c_2931]) ).
cnf(c_2933,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_367,c_2932]) ).
cnf(c_2934,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_368,c_2933]) ).
cnf(c_2935,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_369,c_2934]) ).
cnf(c_2936,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_370,c_2935]) ).
cnf(c_2937,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_371,c_2936]) ).
cnf(c_2938,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_372,c_2937]) ).
cnf(c_2939,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_373,c_2938]) ).
cnf(c_2940,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_374,c_2939]) ).
cnf(c_2941,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_375,c_2940]) ).
cnf(c_2942,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_376,c_2941]) ).
cnf(c_2943,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_377,c_2942]) ).
cnf(c_2944,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_378,c_2943]) ).
cnf(c_2945,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_379,c_2944]) ).
cnf(c_2946,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_380,c_2945]) ).
cnf(c_2947,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_381,c_2946]) ).
cnf(c_2948,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_382,c_2947]) ).
cnf(c_2949,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_383,c_2948]) ).
cnf(c_2950,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_2949]) ).
cnf(c_2951,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_2950]) ).
cnf(c_2952,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_2951]) ).
cnf(c_2953,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_2952]) ).
cnf(c_2954,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_2953]) ).
cnf(c_2955,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_2954]) ).
cnf(c_2956,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_2955]) ).
cnf(c_2957,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_2956]) ).
cnf(c_2958,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_2957]) ).
cnf(c_2959,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_2958]) ).
cnf(c_2960,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_2959]) ).
cnf(c_2961,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_2960]) ).
cnf(c_2962,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_2961]) ).
cnf(c_2963,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_2962]) ).
cnf(c_2964,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_2963]) ).
cnf(c_2965,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_2964]) ).
cnf(c_2966,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_2965]) ).
cnf(c_2967,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_2966]) ).
cnf(c_2968,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_2967]) ).
cnf(c_2969,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2968]) ).
cnf(c_2970,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2969]) ).
cnf(c_2971,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2970]) ).
cnf(c_2972,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2971]) ).
cnf(c_2973,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2972]) ).
cnf(c_2974,negated_conjecture,
( leq(n0,sK0)
| use != use
| use != use ),
inference(copy,[status(thm)],[c_2973]) ).
cnf(c_2975,negated_conjecture,
( leq(n0,sK0)
| use != use ),
inference(copy,[status(thm)],[c_2974]) ).
cnf(c_387,negated_conjecture,
leq(n0,sK0),
inference(copy,[status(thm)],[c_2975]) ).
cnf(c_390,negated_conjecture,
( leq(sK0,minus(n0,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_0004_neg]) ).
cnf(c_2976,negated_conjecture,
( leq(sK0,minus(n0,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_357,c_390]) ).
cnf(c_2977,negated_conjecture,
( leq(sK0,minus(n0,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_358,c_2976]) ).
cnf(c_2978,negated_conjecture,
( leq(sK0,minus(n0,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_359,c_2977]) ).
cnf(c_2979,negated_conjecture,
( leq(sK0,minus(n0,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_360,c_2978]) ).
cnf(c_2980,negated_conjecture,
( leq(sK0,minus(n0,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_361,c_2979]) ).
cnf(c_2981,negated_conjecture,
( leq(sK0,minus(n0,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_362,c_2980]) ).
cnf(c_2982,negated_conjecture,
( leq(sK0,minus(n0,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_363,c_2981]) ).
cnf(c_2983,negated_conjecture,
( leq(sK0,minus(n0,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_364,c_2982]) ).
cnf(c_2984,negated_conjecture,
( leq(sK0,minus(n0,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_365,c_2983]) ).
cnf(c_2985,negated_conjecture,
( leq(sK0,minus(n0,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_366,c_2984]) ).
cnf(c_2986,negated_conjecture,
( leq(sK0,minus(n0,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_367,c_2985]) ).
cnf(c_2987,negated_conjecture,
( leq(sK0,minus(n0,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_368,c_2986]) ).
cnf(c_2988,negated_conjecture,
( leq(sK0,minus(n0,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_369,c_2987]) ).
cnf(c_2989,negated_conjecture,
( leq(sK0,minus(n0,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_370,c_2988]) ).
cnf(c_2990,negated_conjecture,
( leq(sK0,minus(n0,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_371,c_2989]) ).
cnf(c_2991,negated_conjecture,
( leq(sK0,minus(n0,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_372,c_2990]) ).
cnf(c_2992,negated_conjecture,
( leq(sK0,minus(n0,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_373,c_2991]) ).
cnf(c_2993,negated_conjecture,
( leq(sK0,minus(n0,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_374,c_2992]) ).
cnf(c_2994,negated_conjecture,
( leq(sK0,minus(n0,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_375,c_2993]) ).
cnf(c_2995,negated_conjecture,
( leq(sK0,minus(n0,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_376,c_2994]) ).
cnf(c_2996,negated_conjecture,
( leq(sK0,minus(n0,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_377,c_2995]) ).
cnf(c_2997,negated_conjecture,
( leq(sK0,minus(n0,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_378,c_2996]) ).
cnf(c_2998,negated_conjecture,
( leq(sK0,minus(n0,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_379,c_2997]) ).
cnf(c_2999,negated_conjecture,
( leq(sK0,minus(n0,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_380,c_2998]) ).
cnf(c_3000,negated_conjecture,
( leq(sK0,minus(n0,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_381,c_2999]) ).
cnf(c_3001,negated_conjecture,
( leq(sK0,minus(n0,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_382,c_3000]) ).
cnf(c_3002,negated_conjecture,
( leq(sK0,minus(n0,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_383,c_3001]) ).
cnf(c_3003,negated_conjecture,
( leq(sK0,pred(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 != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(paramod,[status(thm)],[c_300,c_3002]) ).
cnf(c_3004,negated_conjecture,
( leq(sK0,pred(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 != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3003]) ).
cnf(c_3005,negated_conjecture,
( leq(sK0,pred(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 != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3004]) ).
cnf(c_3006,negated_conjecture,
( leq(sK0,pred(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 != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3005]) ).
cnf(c_3007,negated_conjecture,
( leq(sK0,pred(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 != use
| use != use ),
inference(copy,[status(thm)],[c_3006]) ).
cnf(c_3008,negated_conjecture,
( leq(sK0,pred(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 != use ),
inference(copy,[status(thm)],[c_3007]) ).
cnf(c_3009,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3008]) ).
cnf(c_3010,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3009]) ).
cnf(c_3011,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3010]) ).
cnf(c_3012,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3011]) ).
cnf(c_3013,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3012]) ).
cnf(c_3014,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3013]) ).
cnf(c_3015,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3014]) ).
cnf(c_3016,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3015]) ).
cnf(c_3017,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3016]) ).
cnf(c_3018,negated_conjecture,
( leq(sK0,pred(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 ),
inference(copy,[status(thm)],[c_3017]) ).
cnf(c_3019,negated_conjecture,
( leq(sK0,pred(n0))
| 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_3018]) ).
cnf(c_3020,negated_conjecture,
( leq(sK0,pred(n0))
| 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_3019]) ).
cnf(c_3021,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3020]) ).
cnf(c_3022,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3021]) ).
cnf(c_3023,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3022]) ).
cnf(c_3024,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3023]) ).
cnf(c_3025,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3024]) ).
cnf(c_3026,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3025]) ).
cnf(c_3027,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3026]) ).
cnf(c_3028,negated_conjecture,
( leq(sK0,pred(n0))
| use != use
| use != use ),
inference(copy,[status(thm)],[c_3027]) ).
cnf(c_3029,negated_conjecture,
( leq(sK0,pred(n0))
| use != use ),
inference(copy,[status(thm)],[c_3028]) ).
cnf(c_391,negated_conjecture,
leq(sK0,pred(n0)),
inference(copy,[status(thm)],[c_3029]) ).
cnf(c_1200,plain,
pred(n0) = tptp_minus_1,
inference(paramod,[status(thm)],[c_281,c_301]) ).
cnf(c_1205,negated_conjecture,
leq(sK0,tptp_minus_1),
inference(paramod,[status(thm)],[c_1200,c_391]) ).
cnf(c_3030,negated_conjecture,
( n0 = sK0
| ~ leq(sK0,n0) ),
inference(resolve,[status(thm)],[c_387,c_344]) ).
cnf(c_1762,negated_conjecture,
( sK0 = n0
| ~ leq(sK0,n0) ),
inference(copy,[status(thm)],[c_3030]) ).
cnf(c_3031,negated_conjecture,
gt(succ(tptp_minus_1),sK0),
inference(resolve,[status(thm)],[c_1205,c_72]) ).
cnf(c_2808,negated_conjecture,
gt(n0,sK0),
inference(paramod,[status(thm)],[c_281,c_3031]) ).
cnf(c_3032,negated_conjecture,
leq(sK0,succ(tptp_minus_1)),
inference(resolve,[status(thm)],[c_1205,c_71]) ).
cnf(c_2809,negated_conjecture,
leq(sK0,n0),
inference(paramod,[status(thm)],[c_281,c_3032]) ).
cnf(c_2914,negated_conjecture,
sK0 = n0,
inference(resolve,[status(thm)],[c_2809,c_1762]) ).
cnf(c_3033,negated_conjecture,
gt(n0,n0),
inference(paramod,[status(thm)],[c_2914,c_2808]) ).
cnf(c_2922,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_63,c_3033]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV092+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42 % Computer : n001.cluster.edu
% 0.10/0.42 % Model : x86_64 x86_64
% 0.10/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.42 % Memory : 8046.5625MB
% 0.10/0.42 % OS : Linux 6.8.0-71-generic
% 0.10/0.42 % CPULimit : 300
% 0.10/0.42 % WCLimit : 300
% 0.10/0.42 % DateTime : Sat Sep 26 13:17:58 UTC 2026
% 0.10/0.43 % CPUTime :
% 0.10/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.43 % Process 1887458 was started by sandbox on n001,
% 0.10/0.43 % Sat Sep 26 13:17:58 2026
% 0.10/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.49
% 0.16/0.49 % From the command line: assign(max_seconds, 300).
% 7.97/2.69
% 7.97/2.69 % given #500 (I,wt=140): 579 leq(n0,f19(A,B,C,D,E,F,V6,V7)) | leq(n0,f21(A,B,C,D,E,F,V6,V7)) | leq(f23(A,B,C,D,E,F,V6,V7),V6) | -leq(n0,V6) | a_select3(tptp_madd(A,tptp_mmul(B,tptp_mmul(tptp_madd(tptp_mmul(C,tptp_mmul(D,trans(C))),tptp_mmul(E,tptp_mmul(F,trans(E)))),trans(B)))),n0,V6) = a_select3(tptp_madd(A,tptp_mmul(B,tptp_mmul(tptp_madd(tptp_mmul(C,tptp_mmul(D,trans(C))),tptp_mmul(E,tptp_mmul(F,trans(E)))),trans(B)))),V6,n0). [factor(154,d,g),unit_del(e,64),unit_del(f,64)].
% 7.97/2.69
% 7.97/2.69 % SZS status Theorem for theBenchmark
% 7.97/2.69
% 7.97/2.69 % Proof 1 at 0.97 (+ 0.12) seconds.
% 7.97/2.69 % Length of proof is 52.
% 7.97/2.69 % Level of proof is 6.
% 7.97/2.69 % Maximum clause weight is 20.000.
% 7.97/2.69 % Given clauses 811.
% 7.97/2.69
% 7.97/2.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------