%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV095+1 : TPTP v5.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 12:04:40 EST 2010
% Result : Theorem 1.89s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 3
% Syntax : Number of formulae : 231 ( 42 unt; 0 def)
% Number of atoms : 5925 (2510 equ)
% Maximal formula atoms : 202 ( 25 avg)
% Number of connectives : 8604 (2910 ~;5360 |; 327 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 73 ( 26 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 20 con; 0-3 aty)
% Number of variables : 47 ( 0 sgn 26 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(22,axiom,
! [X1] : minus(X1,n1) = pred(X1),
file('/tmp/tmpO7AiNy/sel_SWV095+1.p_1',pred_minus_1) ).
fof(25,axiom,
! [X1,X2] :
( leq(X1,pred(X2))
<=> gt(X2,X1) ),
file('/tmp/tmpO7AiNy/sel_SWV095+1.p_1',leq_gt_pred) ).
fof(39,conjecture,
( ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,n2)
& leq(X5,minus(pv5,n1)) )
=> ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) ) )
=> ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X6,X7] :
( ( leq(n0,X6)
& leq(n0,X7)
& leq(X6,n2)
& leq(X7,minus(pv5,n1)) )
=> ( a_select3(u_defuse,X6,X7) = use
& a_select3(z_defuse,X6,X7) = use ) ) ) ),
file('/tmp/tmpO7AiNy/sel_SWV095+1.p_1',quaternion_ds1_inuse_0007) ).
fof(80,negated_conjecture,
~ ( ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,n2)
& leq(X5,minus(pv5,n1)) )
=> ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) ) )
=> ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X6,X7] :
( ( leq(n0,X6)
& leq(n0,X7)
& leq(X6,n2)
& leq(X7,minus(pv5,n1)) )
=> ( a_select3(u_defuse,X6,X7) = use
& a_select3(z_defuse,X6,X7) = use ) ) ) ),
inference(assume_negation,[status(cth)],[39]) ).
fof(129,plain,
! [X2] : minus(X2,n1) = pred(X2),
inference(variable_rename,[status(thm)],[22]) ).
cnf(130,plain,
minus(X1,n1) = pred(X1),
inference(split_conjunct,[status(thm)],[129]) ).
fof(137,plain,
! [X1,X2] :
( ( ~ leq(X1,pred(X2))
| gt(X2,X1) )
& ( ~ gt(X2,X1)
| leq(X1,pred(X2)) ) ),
inference(fof_nnf,[status(thm)],[25]) ).
fof(138,plain,
! [X3,X4] :
( ( ~ leq(X3,pred(X4))
| gt(X4,X3) )
& ( ~ gt(X4,X3)
| leq(X3,pred(X4)) ) ),
inference(variable_rename,[status(thm)],[137]) ).
cnf(139,plain,
( leq(X1,pred(X2))
| ~ gt(X2,X1) ),
inference(split_conjunct,[status(thm)],[138]) ).
cnf(140,plain,
( gt(X1,X2)
| ~ leq(X2,pred(X1)) ),
inference(split_conjunct,[status(thm)],[138]) ).
fof(160,negated_conjecture,
( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X4,X5] :
( ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,n2)
| ~ leq(X5,minus(pv5,n1))
| ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) )
& ( a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| ? [X6,X7] :
( leq(n0,X6)
& leq(n0,X7)
& leq(X6,n2)
& leq(X7,minus(pv5,n1))
& ( a_select3(u_defuse,X6,X7) != use
| a_select3(z_defuse,X6,X7) != use ) ) ) ),
inference(fof_nnf,[status(thm)],[80]) ).
fof(161,negated_conjecture,
( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X8,X9] :
( ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,minus(pv5,n1))
| ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) )
& ( a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| ? [X10,X11] :
( leq(n0,X10)
& leq(n0,X11)
& leq(X10,n2)
& leq(X11,minus(pv5,n1))
& ( a_select3(u_defuse,X10,X11) != use
| a_select3(z_defuse,X10,X11) != use ) ) ) ),
inference(variable_rename,[status(thm)],[160]) ).
fof(162,negated_conjecture,
( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [X8,X9] :
( ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,minus(pv5,n1))
| ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) )
& ( a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| ( leq(n0,esk1_0)
& leq(n0,esk2_0)
& leq(esk1_0,n2)
& leq(esk2_0,minus(pv5,n1))
& ( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use ) ) ) ),
inference(skolemize,[status(esa)],[161]) ).
fof(163,negated_conjecture,
! [X8,X9] :
( ( ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,minus(pv5,n1))
| ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) )
& a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ( a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| ( leq(n0,esk1_0)
& leq(n0,esk2_0)
& leq(esk1_0,n2)
& leq(esk2_0,minus(pv5,n1))
& ( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use ) ) ) ),
inference(shift_quantors,[status(thm)],[162]) ).
fof(164,negated_conjecture,
! [X8,X9] :
( ( a_select3(u_defuse,X8,X9) = use
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,minus(pv5,n1)) )
& ( a_select3(z_defuse,X8,X9) = use
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,minus(pv5,n1)) )
& a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ( leq(n0,esk1_0)
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) )
& ( leq(n0,esk2_0)
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) )
& ( leq(esk1_0,n2)
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) )
& ( leq(esk2_0,minus(pv5,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) )
& ( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n2) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n5) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n5) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ) ),
inference(distribute,[status(thm)],[163]) ).
cnf(165,negated_conjecture,
( ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(166,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(167,negated_conjecture,
( leq(esk1_0,n2)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(168,negated_conjecture,
( leq(n0,esk2_0)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(169,negated_conjecture,
( leq(n0,esk1_0)
| ~ leq(pv51,minus(n6,n1))
| ~ leq(pv5,minus(n999,n1))
| ~ leq(n0,pv51)
| ~ leq(n0,pv5)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(170,negated_conjecture,
leq(pv51,minus(n6,n1)),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(171,negated_conjecture,
leq(pv5,minus(n999,n1)),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(172,negated_conjecture,
leq(n0,pv51),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(173,negated_conjecture,
leq(n0,pv5),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(174,negated_conjecture,
a_select2(xinit_noise_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(175,negated_conjecture,
a_select2(xinit_noise_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(176,negated_conjecture,
a_select2(xinit_noise_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(177,negated_conjecture,
a_select2(xinit_noise_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(178,negated_conjecture,
a_select2(xinit_noise_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(179,negated_conjecture,
a_select2(xinit_noise_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(180,negated_conjecture,
a_select2(xinit_mean_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(181,negated_conjecture,
a_select2(xinit_mean_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(182,negated_conjecture,
a_select2(xinit_mean_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(183,negated_conjecture,
a_select2(xinit_mean_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(184,negated_conjecture,
a_select2(xinit_mean_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(185,negated_conjecture,
a_select2(xinit_mean_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(186,negated_conjecture,
a_select2(xinit_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(187,negated_conjecture,
a_select2(xinit_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(188,negated_conjecture,
a_select2(xinit_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(189,negated_conjecture,
a_select3(u_defuse,n2,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(190,negated_conjecture,
a_select3(u_defuse,n1,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(191,negated_conjecture,
a_select3(u_defuse,n0,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(192,negated_conjecture,
a_select2(sigma_defuse,n5) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(193,negated_conjecture,
a_select2(sigma_defuse,n4) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(194,negated_conjecture,
a_select2(sigma_defuse,n3) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(195,negated_conjecture,
a_select2(sigma_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(196,negated_conjecture,
a_select2(sigma_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(197,negated_conjecture,
a_select2(sigma_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(198,negated_conjecture,
a_select2(rho_defuse,n2) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(199,negated_conjecture,
a_select2(rho_defuse,n1) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(200,negated_conjecture,
a_select2(rho_defuse,n0) = use,
inference(split_conjunct,[status(thm)],[164]) ).
cnf(201,negated_conjecture,
( a_select3(z_defuse,X2,X1) = use
| ~ leq(X1,minus(pv5,n1))
| ~ leq(X2,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2) ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(202,negated_conjecture,
( a_select3(u_defuse,X2,X1) = use
| ~ leq(X1,minus(pv5,n1))
| ~ leq(X2,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2) ),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(284,plain,
( gt(X1,X2)
| ~ leq(X2,minus(X1,n1)) ),
inference(rw,[status(thm)],[140,130,theory(equality)]),
[unfolding] ).
cnf(285,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rw,[status(thm)],[139,130,theory(equality)]),
[unfolding] ).
cnf(438,negated_conjecture,
( a_select3(u_defuse,X1,X2) = use
| ~ leq(X1,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2)
| ~ gt(pv5,X2) ),
inference(spm,[status(thm)],[202,285,theory(equality)]) ).
cnf(440,negated_conjecture,
( a_select3(z_defuse,X1,X2) = use
| ~ leq(X1,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2)
| ~ gt(pv5,X2) ),
inference(spm,[status(thm)],[201,285,theory(equality)]) ).
cnf(565,negated_conjecture,
( leq(n0,esk1_0)
| $false
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[169,200,theory(equality)]) ).
cnf(566,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[565,198,theory(equality)]) ).
cnf(567,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[566,199,theory(equality)]) ).
cnf(568,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[567,193,theory(equality)]) ).
cnf(569,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[568,197,theory(equality)]) ).
cnf(570,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[569,194,theory(equality)]) ).
cnf(571,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[570,192,theory(equality)]) ).
cnf(572,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[571,195,theory(equality)]) ).
cnf(573,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[572,196,theory(equality)]) ).
cnf(574,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[573,187,theory(equality)]) ).
cnf(575,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[574,188,theory(equality)]) ).
cnf(576,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[575,186,theory(equality)]) ).
cnf(577,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[576,181,theory(equality)]) ).
cnf(578,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[577,185,theory(equality)]) ).
cnf(579,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[578,182,theory(equality)]) ).
cnf(580,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[579,180,theory(equality)]) ).
cnf(581,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[580,183,theory(equality)]) ).
cnf(582,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[581,184,theory(equality)]) ).
cnf(583,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[582,175,theory(equality)]) ).
cnf(584,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[583,179,theory(equality)]) ).
cnf(585,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[584,176,theory(equality)]) ).
cnf(586,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[585,174,theory(equality)]) ).
cnf(587,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[586,177,theory(equality)]) ).
cnf(588,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[587,178,theory(equality)]) ).
cnf(589,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[588,191,theory(equality)]) ).
cnf(590,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[589,189,theory(equality)]) ).
cnf(591,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[590,190,theory(equality)]) ).
cnf(592,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[591,173,theory(equality)]) ).
cnf(593,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[592,172,theory(equality)]) ).
cnf(594,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[593,171,theory(equality)]) ).
cnf(595,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[594,170,theory(equality)]) ).
cnf(596,negated_conjecture,
leq(n0,esk1_0),
inference(cn,[status(thm)],[595,theory(equality)]) ).
cnf(598,negated_conjecture,
( leq(n0,esk2_0)
| $false
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[168,200,theory(equality)]) ).
cnf(599,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[598,198,theory(equality)]) ).
cnf(600,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[599,199,theory(equality)]) ).
cnf(601,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[600,193,theory(equality)]) ).
cnf(602,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[601,197,theory(equality)]) ).
cnf(603,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[602,194,theory(equality)]) ).
cnf(604,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[603,192,theory(equality)]) ).
cnf(605,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[604,195,theory(equality)]) ).
cnf(606,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[605,196,theory(equality)]) ).
cnf(607,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[606,187,theory(equality)]) ).
cnf(608,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[607,188,theory(equality)]) ).
cnf(609,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[608,186,theory(equality)]) ).
cnf(610,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[609,181,theory(equality)]) ).
cnf(611,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[610,185,theory(equality)]) ).
cnf(612,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[611,182,theory(equality)]) ).
cnf(613,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[612,180,theory(equality)]) ).
cnf(614,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[613,183,theory(equality)]) ).
cnf(615,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[614,184,theory(equality)]) ).
cnf(616,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[615,175,theory(equality)]) ).
cnf(617,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[616,179,theory(equality)]) ).
cnf(618,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[617,176,theory(equality)]) ).
cnf(619,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[618,174,theory(equality)]) ).
cnf(620,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[619,177,theory(equality)]) ).
cnf(621,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[620,178,theory(equality)]) ).
cnf(622,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[621,191,theory(equality)]) ).
cnf(623,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[622,189,theory(equality)]) ).
cnf(624,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[623,190,theory(equality)]) ).
cnf(625,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[624,173,theory(equality)]) ).
cnf(626,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[625,172,theory(equality)]) ).
cnf(627,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[626,171,theory(equality)]) ).
cnf(628,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[627,170,theory(equality)]) ).
cnf(629,negated_conjecture,
leq(n0,esk2_0),
inference(cn,[status(thm)],[628,theory(equality)]) ).
cnf(631,negated_conjecture,
( leq(esk1_0,n2)
| $false
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[167,200,theory(equality)]) ).
cnf(632,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[631,198,theory(equality)]) ).
cnf(633,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[632,199,theory(equality)]) ).
cnf(634,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[633,193,theory(equality)]) ).
cnf(635,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[634,197,theory(equality)]) ).
cnf(636,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[635,194,theory(equality)]) ).
cnf(637,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[636,192,theory(equality)]) ).
cnf(638,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[637,195,theory(equality)]) ).
cnf(639,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[638,196,theory(equality)]) ).
cnf(640,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[639,187,theory(equality)]) ).
cnf(641,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[640,188,theory(equality)]) ).
cnf(642,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[641,186,theory(equality)]) ).
cnf(643,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[642,181,theory(equality)]) ).
cnf(644,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[643,185,theory(equality)]) ).
cnf(645,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[644,182,theory(equality)]) ).
cnf(646,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[645,180,theory(equality)]) ).
cnf(647,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[646,183,theory(equality)]) ).
cnf(648,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[647,184,theory(equality)]) ).
cnf(649,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[648,175,theory(equality)]) ).
cnf(650,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[649,179,theory(equality)]) ).
cnf(651,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[650,176,theory(equality)]) ).
cnf(652,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[651,174,theory(equality)]) ).
cnf(653,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[652,177,theory(equality)]) ).
cnf(654,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[653,178,theory(equality)]) ).
cnf(655,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[654,191,theory(equality)]) ).
cnf(656,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[655,189,theory(equality)]) ).
cnf(657,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[656,190,theory(equality)]) ).
cnf(658,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[657,173,theory(equality)]) ).
cnf(659,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[658,172,theory(equality)]) ).
cnf(660,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[659,171,theory(equality)]) ).
cnf(661,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[660,170,theory(equality)]) ).
cnf(662,negated_conjecture,
leq(esk1_0,n2),
inference(cn,[status(thm)],[661,theory(equality)]) ).
cnf(667,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[166,200,theory(equality)]) ).
cnf(668,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[667,198,theory(equality)]) ).
cnf(669,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[668,199,theory(equality)]) ).
cnf(670,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[669,193,theory(equality)]) ).
cnf(671,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[670,197,theory(equality)]) ).
cnf(672,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[671,194,theory(equality)]) ).
cnf(673,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[672,192,theory(equality)]) ).
cnf(674,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[673,195,theory(equality)]) ).
cnf(675,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[674,196,theory(equality)]) ).
cnf(676,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[675,187,theory(equality)]) ).
cnf(677,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[676,188,theory(equality)]) ).
cnf(678,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[677,186,theory(equality)]) ).
cnf(679,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[678,181,theory(equality)]) ).
cnf(680,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[679,185,theory(equality)]) ).
cnf(681,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[680,182,theory(equality)]) ).
cnf(682,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[681,180,theory(equality)]) ).
cnf(683,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[682,183,theory(equality)]) ).
cnf(684,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[683,184,theory(equality)]) ).
cnf(685,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[684,175,theory(equality)]) ).
cnf(686,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[685,179,theory(equality)]) ).
cnf(687,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[686,176,theory(equality)]) ).
cnf(688,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[687,174,theory(equality)]) ).
cnf(689,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[688,177,theory(equality)]) ).
cnf(690,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[689,178,theory(equality)]) ).
cnf(691,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[690,191,theory(equality)]) ).
cnf(692,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n1,n0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[691,189,theory(equality)]) ).
cnf(693,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[692,190,theory(equality)]) ).
cnf(694,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[693,173,theory(equality)]) ).
cnf(695,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[694,172,theory(equality)]) ).
cnf(696,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[695,171,theory(equality)]) ).
cnf(697,negated_conjecture,
( leq(esk2_0,minus(pv5,n1))
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[696,170,theory(equality)]) ).
cnf(698,negated_conjecture,
leq(esk2_0,minus(pv5,n1)),
inference(cn,[status(thm)],[697,theory(equality)]) ).
cnf(699,negated_conjecture,
gt(pv5,esk2_0),
inference(spm,[status(thm)],[284,698,theory(equality)]) ).
cnf(707,negated_conjecture,
( $false
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[165,200,theory(equality)]) ).
cnf(708,negated_conjecture,
( $false
| $false
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[707,198,theory(equality)]) ).
cnf(709,negated_conjecture,
( $false
| $false
| $false
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[708,199,theory(equality)]) ).
cnf(710,negated_conjecture,
( $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[709,193,theory(equality)]) ).
cnf(711,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[710,197,theory(equality)]) ).
cnf(712,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[711,194,theory(equality)]) ).
cnf(713,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[712,192,theory(equality)]) ).
cnf(714,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[713,195,theory(equality)]) ).
cnf(715,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[714,196,theory(equality)]) ).
cnf(716,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[715,187,theory(equality)]) ).
cnf(717,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[716,188,theory(equality)]) ).
cnf(718,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[717,186,theory(equality)]) ).
cnf(719,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[718,181,theory(equality)]) ).
cnf(720,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[719,185,theory(equality)]) ).
cnf(721,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[720,182,theory(equality)]) ).
cnf(722,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[721,180,theory(equality)]) ).
cnf(723,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[722,183,theory(equality)]) ).
cnf(724,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[723,184,theory(equality)]) ).
cnf(725,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[724,175,theory(equality)]) ).
cnf(726,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[725,179,theory(equality)]) ).
cnf(727,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[726,176,theory(equality)]) ).
cnf(728,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[727,174,theory(equality)]) ).
cnf(729,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select2(xinit_noise_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[728,177,theory(equality)]) ).
cnf(730,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[729,178,theory(equality)]) ).
cnf(731,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[730,191,theory(equality)]) ).
cnf(732,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[731,189,theory(equality)]) ).
cnf(733,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[732,190,theory(equality)]) ).
cnf(734,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| $false
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[733,173,theory(equality)]) ).
cnf(735,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| $false
| $false
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[734,172,theory(equality)]) ).
cnf(736,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| $false
| $false
| $false
| ~ leq(pv51,minus(n6,n1)) ),
inference(rw,[status(thm)],[735,171,theory(equality)]) ).
cnf(737,negated_conjecture,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[736,170,theory(equality)]) ).
cnf(738,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use ),
inference(cn,[status(thm)],[737,theory(equality)]) ).
cnf(24705,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| ~ gt(pv5,esk2_0)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(spm,[status(thm)],[738,440,theory(equality)]) ).
cnf(24711,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24705,699,theory(equality)]) ).
cnf(24712,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| $false
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24711,662,theory(equality)]) ).
cnf(24713,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| $false
| $false
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24712,596,theory(equality)]) ).
cnf(24714,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[24713,629,theory(equality)]) ).
cnf(24715,negated_conjecture,
a_select3(u_defuse,esk1_0,esk2_0) != use,
inference(cn,[status(thm)],[24714,theory(equality)]) ).
cnf(24746,negated_conjecture,
( ~ gt(pv5,esk2_0)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(spm,[status(thm)],[24715,438,theory(equality)]) ).
cnf(24747,negated_conjecture,
( $false
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24746,699,theory(equality)]) ).
cnf(24748,negated_conjecture,
( $false
| $false
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24747,662,theory(equality)]) ).
cnf(24749,negated_conjecture,
( $false
| $false
| $false
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[24748,596,theory(equality)]) ).
cnf(24750,negated_conjecture,
( $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[24749,629,theory(equality)]) ).
cnf(24751,negated_conjecture,
$false,
inference(cn,[status(thm)],[24750,theory(equality)]) ).
cnf(24752,negated_conjecture,
$false,
24751,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV095+1.p
% --creating new selector for [SWV003+0.ax]
% -running prover on /tmp/tmpO7AiNy/sel_SWV095+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWV095+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV095+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV095+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------