%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV098+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:05:02 EST 2010
% Result : Theorem 0.24s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 6
% Syntax : Number of formulae : 274 ( 52 unt; 0 def)
% Number of atoms : 4858 (2584 equ)
% Maximal formula atoms : 142 ( 17 avg)
% Number of connectives : 6914 (2330 ~;4216 |; 355 &)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 18 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-3 aty)
% Number of variables : 66 ( 0 sgn 42 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(17,axiom,
! [X1] : plus(X1,n1) = succ(X1),
file('/tmp/tmpmd5_Ab/sel_SWV098+1.p_1',succ_plus_1_r) ).
fof(22,axiom,
! [X1] : minus(X1,n1) = pred(X1),
file('/tmp/tmpmd5_Ab/sel_SWV098+1.p_1',pred_minus_1) ).
fof(23,axiom,
! [X1] : plus(n1,X1) = succ(X1),
file('/tmp/tmpmd5_Ab/sel_SWV098+1.p_1',succ_plus_1_l) ).
fof(27,axiom,
! [X1] : pred(succ(X1)) = X1,
file('/tmp/tmpmd5_Ab/sel_SWV098+1.p_1',pred_succ) ).
fof(50,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(pv5,minus(n999,n1))
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,n2)
& leq(X5,pv5) )
=> ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) )
& ! [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 ) ) )
=> ( 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
& ! [X8,X9] :
( ( leq(n0,X8)
& leq(n0,X9)
& leq(X8,n2)
& leq(X9,minus(plus(n1,pv5),n1)) )
=> ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) ) ) ),
file('/tmp/tmpmd5_Ab/sel_SWV098+1.p_1',quaternion_ds1_inuse_0010) ).
fof(70,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(pv5,minus(n999,n1))
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,n2)
& leq(X5,pv5) )
=> ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) )
& ! [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 ) ) )
=> ( 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
& ! [X8,X9] :
( ( leq(n0,X8)
& leq(n0,X9)
& leq(X8,n2)
& leq(X9,minus(plus(n1,pv5),n1)) )
=> ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) ) ) ),
inference(assume_negation,[status(cth)],[50]) ).
fof(72,plain,
( epred1_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(pv5,minus(n999,n1))
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,n2)
& leq(X5,pv5) )
=> ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) )
& ! [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 ) ) ) ),
introduced(definition) ).
fof(73,negated_conjecture,
~ ( epred1_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
& ! [X8,X9] :
( ( leq(n0,X8)
& leq(n0,X9)
& leq(X8,n2)
& leq(X9,minus(plus(n1,pv5),n1)) )
=> ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) ) ) ),
inference(apply_def,[status(esa)],[70,72,theory(equality)]) ).
fof(111,plain,
! [X2] : plus(X2,n1) = succ(X2),
inference(variable_rename,[status(thm)],[17]) ).
cnf(112,plain,
plus(X1,n1) = succ(X1),
inference(split_conjunct,[status(thm)],[111]) ).
fof(121,plain,
! [X2] : minus(X2,n1) = pred(X2),
inference(variable_rename,[status(thm)],[22]) ).
cnf(122,plain,
minus(X1,n1) = pred(X1),
inference(split_conjunct,[status(thm)],[121]) ).
fof(123,plain,
! [X2] : plus(n1,X2) = succ(X2),
inference(variable_rename,[status(thm)],[23]) ).
cnf(124,plain,
plus(n1,X1) = succ(X1),
inference(split_conjunct,[status(thm)],[123]) ).
fof(136,plain,
! [X2] : pred(succ(X2)) = X2,
inference(variable_rename,[status(thm)],[27]) ).
cnf(137,plain,
pred(succ(X1)) = X1,
inference(split_conjunct,[status(thm)],[136]) ).
fof(167,negated_conjecture,
( epred1_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
| ? [X8,X9] :
( leq(n0,X8)
& leq(n0,X9)
& leq(X8,n2)
& leq(X9,minus(plus(n1,pv5),n1))
& ( a_select3(u_defuse,X8,X9) != use
| a_select3(z_defuse,X8,X9) != use ) ) ) ),
inference(fof_nnf,[status(thm)],[73]) ).
fof(168,negated_conjecture,
( epred1_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
| ? [X10,X11] :
( leq(n0,X10)
& leq(n0,X11)
& leq(X10,n2)
& leq(X11,minus(plus(n1,pv5),n1))
& ( a_select3(u_defuse,X10,X11) != use
| a_select3(z_defuse,X10,X11) != use ) ) ) ),
inference(variable_rename,[status(thm)],[167]) ).
fof(169,negated_conjecture,
( epred1_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,esk1_0)
& leq(n0,esk2_0)
& leq(esk1_0,n2)
& leq(esk2_0,minus(plus(n1,pv5),n1))
& ( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use ) ) ) ),
inference(skolemize,[status(esa)],[168]) ).
fof(170,negated_conjecture,
( epred1_0
& ( 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,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(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(esk2_0,minus(plus(n1,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 )
& ( 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 ) ),
inference(distribute,[status(thm)],[169]) ).
cnf(171,negated_conjecture,
( a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use
| a_select3(u_defuse,esk1_0,esk2_0) != use ),
inference(split_conjunct,[status(thm)],[170]) ).
cnf(172,negated_conjecture,
( leq(esk2_0,minus(plus(n1,pv5),n1))
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[170]) ).
cnf(173,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(rho_defuse,n0) != use ),
inference(split_conjunct,[status(thm)],[170]) ).
cnf(174,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_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)],[170]) ).
cnf(175,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_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)],[170]) ).
cnf(176,negated_conjecture,
epred1_0,
inference(split_conjunct,[status(thm)],[170]) ).
fof(204,plain,
( ~ epred1_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(pv5,minus(n999,n1))
& ! [X4,X5] :
( ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,n2)
| ~ leq(X5,pv5)
| ( a_select3(u_defuse,X4,X5) = use
& a_select3(z_defuse,X4,X5) = use ) )
& ! [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)],[72]) ).
fof(205,plain,
( ~ epred1_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(pv5,minus(n999,n1))
& ! [X8,X9] :
( ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,pv5)
| ( a_select3(u_defuse,X8,X9) = use
& a_select3(z_defuse,X8,X9) = use ) )
& ! [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)],[204]) ).
fof(206,plain,
! [X8,X9,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 ) )
& ( ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,pv5)
| ( 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(pv5,minus(n999,n1)) )
| ~ epred1_0 ),
inference(shift_quantors,[status(thm)],[205]) ).
fof(207,plain,
! [X8,X9,X10,X11] :
( ( a_select3(u_defuse,X10,X11) = use
| ~ leq(n0,X10)
| ~ leq(n0,X11)
| ~ leq(X10,n2)
| ~ leq(X11,minus(pv5,n1))
| ~ epred1_0 )
& ( a_select3(z_defuse,X10,X11) = use
| ~ leq(n0,X10)
| ~ leq(n0,X11)
| ~ leq(X10,n2)
| ~ leq(X11,minus(pv5,n1))
| ~ epred1_0 )
& ( a_select3(u_defuse,X8,X9) = use
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,pv5)
| ~ epred1_0 )
& ( a_select3(z_defuse,X8,X9) = use
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,n2)
| ~ leq(X9,pv5)
| ~ epred1_0 )
& ( a_select2(rho_defuse,n0) = use
| ~ epred1_0 )
& ( a_select2(rho_defuse,n1) = use
| ~ epred1_0 )
& ( a_select2(rho_defuse,n2) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n0) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n1) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n2) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n3) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n4) = use
| ~ epred1_0 )
& ( a_select2(sigma_defuse,n5) = use
| ~ epred1_0 )
& ( a_select3(u_defuse,n0,n0) = use
| ~ epred1_0 )
& ( a_select3(u_defuse,n1,n0) = use
| ~ epred1_0 )
& ( a_select3(u_defuse,n2,n0) = use
| ~ epred1_0 )
& ( a_select2(xinit_defuse,n3) = use
| ~ epred1_0 )
& ( a_select2(xinit_defuse,n4) = use
| ~ epred1_0 )
& ( a_select2(xinit_defuse,n5) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n0) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n1) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n2) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n3) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n4) = use
| ~ epred1_0 )
& ( a_select2(xinit_mean_defuse,n5) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n0) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n1) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n2) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n3) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n4) = use
| ~ epred1_0 )
& ( a_select2(xinit_noise_defuse,n5) = use
| ~ epred1_0 )
& ( leq(n0,pv5)
| ~ epred1_0 )
& ( leq(pv5,minus(n999,n1))
| ~ epred1_0 ) ),
inference(distribute,[status(thm)],[206]) ).
cnf(210,plain,
( a_select2(xinit_noise_defuse,n5) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(211,plain,
( a_select2(xinit_noise_defuse,n4) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(212,plain,
( a_select2(xinit_noise_defuse,n3) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(213,plain,
( a_select2(xinit_noise_defuse,n2) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(214,plain,
( a_select2(xinit_noise_defuse,n1) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(215,plain,
( a_select2(xinit_noise_defuse,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(216,plain,
( a_select2(xinit_mean_defuse,n5) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(217,plain,
( a_select2(xinit_mean_defuse,n4) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(218,plain,
( a_select2(xinit_mean_defuse,n3) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(219,plain,
( a_select2(xinit_mean_defuse,n2) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(220,plain,
( a_select2(xinit_mean_defuse,n1) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(221,plain,
( a_select2(xinit_mean_defuse,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(222,plain,
( a_select2(xinit_defuse,n5) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(223,plain,
( a_select2(xinit_defuse,n4) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(224,plain,
( a_select2(xinit_defuse,n3) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(225,plain,
( a_select3(u_defuse,n2,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(226,plain,
( a_select3(u_defuse,n1,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(227,plain,
( a_select3(u_defuse,n0,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(228,plain,
( a_select2(sigma_defuse,n5) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(229,plain,
( a_select2(sigma_defuse,n4) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(230,plain,
( a_select2(sigma_defuse,n3) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(231,plain,
( a_select2(sigma_defuse,n2) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(232,plain,
( a_select2(sigma_defuse,n1) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(233,plain,
( a_select2(sigma_defuse,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(234,plain,
( a_select2(rho_defuse,n2) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(235,plain,
( a_select2(rho_defuse,n1) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(236,plain,
( a_select2(rho_defuse,n0) = use
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(237,plain,
( a_select3(z_defuse,X2,X1) = use
| ~ epred1_0
| ~ leq(X1,pv5)
| ~ leq(X2,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2) ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(238,plain,
( a_select3(u_defuse,X2,X1) = use
| ~ epred1_0
| ~ leq(X1,pv5)
| ~ leq(X2,n2)
| ~ leq(n0,X1)
| ~ leq(n0,X2) ),
inference(split_conjunct,[status(thm)],[207]) ).
cnf(244,plain,
pred(plus(X1,n1)) = X1,
inference(rw,[status(thm)],[137,112,theory(equality)]),
[unfolding] ).
cnf(245,plain,
plus(n1,X1) = plus(X1,n1),
inference(rw,[status(thm)],[124,112,theory(equality)]),
[unfolding] ).
cnf(266,plain,
minus(plus(X1,n1),n1) = X1,
inference(rw,[status(thm)],[244,122,theory(equality)]),
[unfolding] ).
cnf(269,plain,
( a_select2(rho_defuse,n0) = use
| $false ),
inference(rw,[status(thm)],[236,176,theory(equality)]) ).
cnf(270,plain,
a_select2(rho_defuse,n0) = use,
inference(cn,[status(thm)],[269,theory(equality)]) ).
cnf(271,plain,
( a_select2(rho_defuse,n2) = use
| $false ),
inference(rw,[status(thm)],[234,176,theory(equality)]) ).
cnf(272,plain,
a_select2(rho_defuse,n2) = use,
inference(cn,[status(thm)],[271,theory(equality)]) ).
cnf(273,plain,
( a_select2(rho_defuse,n1) = use
| $false ),
inference(rw,[status(thm)],[235,176,theory(equality)]) ).
cnf(274,plain,
a_select2(rho_defuse,n1) = use,
inference(cn,[status(thm)],[273,theory(equality)]) ).
cnf(275,plain,
( a_select2(sigma_defuse,n4) = use
| $false ),
inference(rw,[status(thm)],[229,176,theory(equality)]) ).
cnf(276,plain,
a_select2(sigma_defuse,n4) = use,
inference(cn,[status(thm)],[275,theory(equality)]) ).
cnf(277,plain,
( a_select2(sigma_defuse,n0) = use
| $false ),
inference(rw,[status(thm)],[233,176,theory(equality)]) ).
cnf(278,plain,
a_select2(sigma_defuse,n0) = use,
inference(cn,[status(thm)],[277,theory(equality)]) ).
cnf(279,plain,
( a_select2(sigma_defuse,n3) = use
| $false ),
inference(rw,[status(thm)],[230,176,theory(equality)]) ).
cnf(280,plain,
a_select2(sigma_defuse,n3) = use,
inference(cn,[status(thm)],[279,theory(equality)]) ).
cnf(281,plain,
( a_select2(sigma_defuse,n5) = use
| $false ),
inference(rw,[status(thm)],[228,176,theory(equality)]) ).
cnf(282,plain,
a_select2(sigma_defuse,n5) = use,
inference(cn,[status(thm)],[281,theory(equality)]) ).
cnf(283,plain,
( a_select2(sigma_defuse,n2) = use
| $false ),
inference(rw,[status(thm)],[231,176,theory(equality)]) ).
cnf(284,plain,
a_select2(sigma_defuse,n2) = use,
inference(cn,[status(thm)],[283,theory(equality)]) ).
cnf(285,plain,
( a_select2(sigma_defuse,n1) = use
| $false ),
inference(rw,[status(thm)],[232,176,theory(equality)]) ).
cnf(286,plain,
a_select2(sigma_defuse,n1) = use,
inference(cn,[status(thm)],[285,theory(equality)]) ).
cnf(287,plain,
( a_select2(xinit_defuse,n4) = use
| $false ),
inference(rw,[status(thm)],[223,176,theory(equality)]) ).
cnf(288,plain,
a_select2(xinit_defuse,n4) = use,
inference(cn,[status(thm)],[287,theory(equality)]) ).
cnf(289,plain,
( a_select2(xinit_defuse,n3) = use
| $false ),
inference(rw,[status(thm)],[224,176,theory(equality)]) ).
cnf(290,plain,
a_select2(xinit_defuse,n3) = use,
inference(cn,[status(thm)],[289,theory(equality)]) ).
cnf(291,plain,
( a_select2(xinit_defuse,n5) = use
| $false ),
inference(rw,[status(thm)],[222,176,theory(equality)]) ).
cnf(292,plain,
a_select2(xinit_defuse,n5) = use,
inference(cn,[status(thm)],[291,theory(equality)]) ).
cnf(293,plain,
( a_select2(xinit_mean_defuse,n4) = use
| $false ),
inference(rw,[status(thm)],[217,176,theory(equality)]) ).
cnf(294,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(cn,[status(thm)],[293,theory(equality)]) ).
cnf(295,plain,
( a_select2(xinit_mean_defuse,n0) = use
| $false ),
inference(rw,[status(thm)],[221,176,theory(equality)]) ).
cnf(296,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(cn,[status(thm)],[295,theory(equality)]) ).
cnf(297,plain,
( a_select2(xinit_mean_defuse,n3) = use
| $false ),
inference(rw,[status(thm)],[218,176,theory(equality)]) ).
cnf(298,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(cn,[status(thm)],[297,theory(equality)]) ).
cnf(299,plain,
( a_select2(xinit_mean_defuse,n5) = use
| $false ),
inference(rw,[status(thm)],[216,176,theory(equality)]) ).
cnf(300,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(cn,[status(thm)],[299,theory(equality)]) ).
cnf(301,plain,
( a_select2(xinit_mean_defuse,n2) = use
| $false ),
inference(rw,[status(thm)],[219,176,theory(equality)]) ).
cnf(302,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(cn,[status(thm)],[301,theory(equality)]) ).
cnf(303,plain,
( a_select2(xinit_mean_defuse,n1) = use
| $false ),
inference(rw,[status(thm)],[220,176,theory(equality)]) ).
cnf(304,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(cn,[status(thm)],[303,theory(equality)]) ).
cnf(305,plain,
( a_select2(xinit_noise_defuse,n4) = use
| $false ),
inference(rw,[status(thm)],[211,176,theory(equality)]) ).
cnf(306,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(cn,[status(thm)],[305,theory(equality)]) ).
cnf(307,plain,
( a_select2(xinit_noise_defuse,n0) = use
| $false ),
inference(rw,[status(thm)],[215,176,theory(equality)]) ).
cnf(308,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(cn,[status(thm)],[307,theory(equality)]) ).
cnf(309,plain,
( a_select2(xinit_noise_defuse,n3) = use
| $false ),
inference(rw,[status(thm)],[212,176,theory(equality)]) ).
cnf(310,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(cn,[status(thm)],[309,theory(equality)]) ).
cnf(311,plain,
( a_select2(xinit_noise_defuse,n5) = use
| $false ),
inference(rw,[status(thm)],[210,176,theory(equality)]) ).
cnf(312,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(cn,[status(thm)],[311,theory(equality)]) ).
cnf(313,plain,
( a_select2(xinit_noise_defuse,n2) = use
| $false ),
inference(rw,[status(thm)],[213,176,theory(equality)]) ).
cnf(314,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(cn,[status(thm)],[313,theory(equality)]) ).
cnf(315,plain,
( a_select2(xinit_noise_defuse,n1) = use
| $false ),
inference(rw,[status(thm)],[214,176,theory(equality)]) ).
cnf(316,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(cn,[status(thm)],[315,theory(equality)]) ).
cnf(320,plain,
( a_select3(u_defuse,n0,n0) = use
| $false ),
inference(rw,[status(thm)],[227,176,theory(equality)]) ).
cnf(321,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cn,[status(thm)],[320,theory(equality)]) ).
cnf(322,plain,
( a_select3(u_defuse,n2,n0) = use
| $false ),
inference(rw,[status(thm)],[225,176,theory(equality)]) ).
cnf(323,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cn,[status(thm)],[322,theory(equality)]) ).
cnf(324,plain,
( a_select3(u_defuse,n1,n0) = use
| $false ),
inference(rw,[status(thm)],[226,176,theory(equality)]) ).
cnf(325,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cn,[status(thm)],[324,theory(equality)]) ).
cnf(344,plain,
minus(plus(n1,X1),n1) = X1,
inference(spm,[status(thm)],[266,245,theory(equality)]) ).
cnf(527,plain,
( a_select3(u_defuse,X2,X1) = use
| $false
| ~ leq(X2,n2)
| ~ leq(X1,pv5)
| ~ leq(n0,X2)
| ~ leq(n0,X1) ),
inference(rw,[status(thm)],[238,176,theory(equality)]) ).
cnf(528,plain,
( a_select3(u_defuse,X2,X1) = use
| ~ leq(X2,n2)
| ~ leq(X1,pv5)
| ~ leq(n0,X2)
| ~ leq(n0,X1) ),
inference(cn,[status(thm)],[527,theory(equality)]) ).
cnf(529,plain,
( a_select3(z_defuse,X2,X1) = use
| $false
| ~ leq(X2,n2)
| ~ leq(X1,pv5)
| ~ leq(n0,X2)
| ~ leq(n0,X1) ),
inference(rw,[status(thm)],[237,176,theory(equality)]) ).
cnf(530,plain,
( a_select3(z_defuse,X2,X1) = use
| ~ leq(X2,n2)
| ~ leq(X1,pv5)
| ~ leq(n0,X2)
| ~ leq(n0,X1) ),
inference(cn,[status(thm)],[529,theory(equality)]) ).
cnf(572,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 ),
inference(rw,[status(thm)],[175,270,theory(equality)]) ).
cnf(573,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 ),
inference(rw,[status(thm)],[572,272,theory(equality)]) ).
cnf(574,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 ),
inference(rw,[status(thm)],[573,274,theory(equality)]) ).
cnf(575,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 ),
inference(rw,[status(thm)],[574,276,theory(equality)]) ).
cnf(576,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 ),
inference(rw,[status(thm)],[575,278,theory(equality)]) ).
cnf(577,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 ),
inference(rw,[status(thm)],[576,280,theory(equality)]) ).
cnf(578,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 ),
inference(rw,[status(thm)],[577,282,theory(equality)]) ).
cnf(579,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 ),
inference(rw,[status(thm)],[578,284,theory(equality)]) ).
cnf(580,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 ),
inference(rw,[status(thm)],[579,286,theory(equality)]) ).
cnf(581,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 ),
inference(rw,[status(thm)],[580,288,theory(equality)]) ).
cnf(582,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 ),
inference(rw,[status(thm)],[581,290,theory(equality)]) ).
cnf(583,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 ),
inference(rw,[status(thm)],[582,292,theory(equality)]) ).
cnf(584,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 ),
inference(rw,[status(thm)],[583,294,theory(equality)]) ).
cnf(585,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 ),
inference(rw,[status(thm)],[584,296,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
| 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 ),
inference(rw,[status(thm)],[585,298,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
| 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 ),
inference(rw,[status(thm)],[586,300,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
| 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 ),
inference(rw,[status(thm)],[587,302,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
| 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 ),
inference(rw,[status(thm)],[588,304,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
| 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 ),
inference(rw,[status(thm)],[589,306,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
| 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 ),
inference(rw,[status(thm)],[590,308,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
| 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 ),
inference(rw,[status(thm)],[591,310,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
| 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 ),
inference(rw,[status(thm)],[592,312,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
| 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 ),
inference(rw,[status(thm)],[593,314,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
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[594,316,theory(equality)]) ).
cnf(596,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 ),
inference(rw,[status(thm)],[595,321,theory(equality)]) ).
cnf(597,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 ),
inference(rw,[status(thm)],[596,323,theory(equality)]) ).
cnf(598,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 ),
inference(rw,[status(thm)],[597,325,theory(equality)]) ).
cnf(599,negated_conjecture,
leq(n0,esk1_0),
inference(cn,[status(thm)],[598,theory(equality)]) ).
cnf(601,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 ),
inference(rw,[status(thm)],[174,270,theory(equality)]) ).
cnf(602,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 ),
inference(rw,[status(thm)],[601,272,theory(equality)]) ).
cnf(603,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 ),
inference(rw,[status(thm)],[602,274,theory(equality)]) ).
cnf(604,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 ),
inference(rw,[status(thm)],[603,276,theory(equality)]) ).
cnf(605,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 ),
inference(rw,[status(thm)],[604,278,theory(equality)]) ).
cnf(606,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 ),
inference(rw,[status(thm)],[605,280,theory(equality)]) ).
cnf(607,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 ),
inference(rw,[status(thm)],[606,282,theory(equality)]) ).
cnf(608,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 ),
inference(rw,[status(thm)],[607,284,theory(equality)]) ).
cnf(609,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 ),
inference(rw,[status(thm)],[608,286,theory(equality)]) ).
cnf(610,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 ),
inference(rw,[status(thm)],[609,288,theory(equality)]) ).
cnf(611,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 ),
inference(rw,[status(thm)],[610,290,theory(equality)]) ).
cnf(612,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 ),
inference(rw,[status(thm)],[611,292,theory(equality)]) ).
cnf(613,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 ),
inference(rw,[status(thm)],[612,294,theory(equality)]) ).
cnf(614,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 ),
inference(rw,[status(thm)],[613,296,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
| 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 ),
inference(rw,[status(thm)],[614,298,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
| 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 ),
inference(rw,[status(thm)],[615,300,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
| 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 ),
inference(rw,[status(thm)],[616,302,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
| 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 ),
inference(rw,[status(thm)],[617,304,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
| 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 ),
inference(rw,[status(thm)],[618,306,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
| 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 ),
inference(rw,[status(thm)],[619,308,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
| 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 ),
inference(rw,[status(thm)],[620,310,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
| 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 ),
inference(rw,[status(thm)],[621,312,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
| 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 ),
inference(rw,[status(thm)],[622,314,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
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[623,316,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
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[624,321,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
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[625,323,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 ),
inference(rw,[status(thm)],[626,325,theory(equality)]) ).
cnf(628,negated_conjecture,
leq(n0,esk2_0),
inference(cn,[status(thm)],[627,theory(equality)]) ).
cnf(630,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 ),
inference(rw,[status(thm)],[173,270,theory(equality)]) ).
cnf(631,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 ),
inference(rw,[status(thm)],[630,272,theory(equality)]) ).
cnf(632,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 ),
inference(rw,[status(thm)],[631,274,theory(equality)]) ).
cnf(633,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 ),
inference(rw,[status(thm)],[632,276,theory(equality)]) ).
cnf(634,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 ),
inference(rw,[status(thm)],[633,278,theory(equality)]) ).
cnf(635,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 ),
inference(rw,[status(thm)],[634,280,theory(equality)]) ).
cnf(636,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 ),
inference(rw,[status(thm)],[635,282,theory(equality)]) ).
cnf(637,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 ),
inference(rw,[status(thm)],[636,284,theory(equality)]) ).
cnf(638,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 ),
inference(rw,[status(thm)],[637,286,theory(equality)]) ).
cnf(639,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 ),
inference(rw,[status(thm)],[638,288,theory(equality)]) ).
cnf(640,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 ),
inference(rw,[status(thm)],[639,290,theory(equality)]) ).
cnf(641,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 ),
inference(rw,[status(thm)],[640,292,theory(equality)]) ).
cnf(642,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 ),
inference(rw,[status(thm)],[641,294,theory(equality)]) ).
cnf(643,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 ),
inference(rw,[status(thm)],[642,296,theory(equality)]) ).
cnf(644,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 ),
inference(rw,[status(thm)],[643,298,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
| $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 ),
inference(rw,[status(thm)],[644,300,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
| $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 ),
inference(rw,[status(thm)],[645,302,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
| $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 ),
inference(rw,[status(thm)],[646,304,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
| $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 ),
inference(rw,[status(thm)],[647,306,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
| $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 ),
inference(rw,[status(thm)],[648,308,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
| $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 ),
inference(rw,[status(thm)],[649,310,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
| $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 ),
inference(rw,[status(thm)],[650,312,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
| $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 ),
inference(rw,[status(thm)],[651,314,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
| $false
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[652,316,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
| $false
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[653,321,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
| $false
| a_select3(u_defuse,n1,n0) != use ),
inference(rw,[status(thm)],[654,323,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
| $false ),
inference(rw,[status(thm)],[655,325,theory(equality)]) ).
cnf(657,negated_conjecture,
leq(esk1_0,n2),
inference(cn,[status(thm)],[656,theory(equality)]) ).
cnf(662,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 ),
inference(rw,[status(thm)],[171,270,theory(equality)]) ).
cnf(663,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 ),
inference(rw,[status(thm)],[662,272,theory(equality)]) ).
cnf(664,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 ),
inference(rw,[status(thm)],[663,274,theory(equality)]) ).
cnf(665,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 ),
inference(rw,[status(thm)],[664,276,theory(equality)]) ).
cnf(666,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 ),
inference(rw,[status(thm)],[665,278,theory(equality)]) ).
cnf(667,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 ),
inference(rw,[status(thm)],[666,280,theory(equality)]) ).
cnf(668,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 ),
inference(rw,[status(thm)],[667,282,theory(equality)]) ).
cnf(669,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 ),
inference(rw,[status(thm)],[668,284,theory(equality)]) ).
cnf(670,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 ),
inference(rw,[status(thm)],[669,286,theory(equality)]) ).
cnf(671,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 ),
inference(rw,[status(thm)],[670,288,theory(equality)]) ).
cnf(672,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 ),
inference(rw,[status(thm)],[671,290,theory(equality)]) ).
cnf(673,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 ),
inference(rw,[status(thm)],[672,292,theory(equality)]) ).
cnf(674,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 ),
inference(rw,[status(thm)],[673,294,theory(equality)]) ).
cnf(675,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 ),
inference(rw,[status(thm)],[674,296,theory(equality)]) ).
cnf(676,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 ),
inference(rw,[status(thm)],[675,298,theory(equality)]) ).
cnf(677,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 ),
inference(rw,[status(thm)],[676,300,theory(equality)]) ).
cnf(678,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 ),
inference(rw,[status(thm)],[677,302,theory(equality)]) ).
cnf(679,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 ),
inference(rw,[status(thm)],[678,304,theory(equality)]) ).
cnf(680,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 ),
inference(rw,[status(thm)],[679,306,theory(equality)]) ).
cnf(681,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 ),
inference(rw,[status(thm)],[680,308,theory(equality)]) ).
cnf(682,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 ),
inference(rw,[status(thm)],[681,310,theory(equality)]) ).
cnf(683,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 ),
inference(rw,[status(thm)],[682,312,theory(equality)]) ).
cnf(684,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 ),
inference(rw,[status(thm)],[683,314,theory(equality)]) ).
cnf(685,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 ),
inference(rw,[status(thm)],[684,316,theory(equality)]) ).
cnf(686,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 ),
inference(rw,[status(thm)],[685,321,theory(equality)]) ).
cnf(687,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 ),
inference(rw,[status(thm)],[686,323,theory(equality)]) ).
cnf(688,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 ),
inference(rw,[status(thm)],[687,325,theory(equality)]) ).
cnf(689,negated_conjecture,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| a_select3(z_defuse,esk1_0,esk2_0) != use ),
inference(cn,[status(thm)],[688,theory(equality)]) ).
cnf(690,plain,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| ~ leq(esk1_0,n2)
| ~ leq(esk2_0,pv5)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(spm,[status(thm)],[689,530,theory(equality)]) ).
cnf(691,plain,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| ~ leq(esk2_0,pv5)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[690,657,theory(equality)]) ).
cnf(692,plain,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| ~ leq(esk2_0,pv5)
| $false
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[691,599,theory(equality)]) ).
cnf(693,plain,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| $false
| ~ leq(esk2_0,pv5)
| $false
| $false ),
inference(rw,[status(thm)],[692,628,theory(equality)]) ).
cnf(694,plain,
( a_select3(u_defuse,esk1_0,esk2_0) != use
| ~ leq(esk2_0,pv5) ),
inference(cn,[status(thm)],[693,theory(equality)]) ).
cnf(695,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[172,270,theory(equality)]) ).
cnf(696,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[695,272,theory(equality)]) ).
cnf(697,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[696,274,theory(equality)]) ).
cnf(698,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[697,276,theory(equality)]) ).
cnf(699,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[698,278,theory(equality)]) ).
cnf(700,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[699,280,theory(equality)]) ).
cnf(701,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[700,282,theory(equality)]) ).
cnf(702,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[701,284,theory(equality)]) ).
cnf(703,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[702,286,theory(equality)]) ).
cnf(704,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[703,288,theory(equality)]) ).
cnf(705,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[704,290,theory(equality)]) ).
cnf(706,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[705,292,theory(equality)]) ).
cnf(707,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[706,294,theory(equality)]) ).
cnf(708,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[707,296,theory(equality)]) ).
cnf(709,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[708,298,theory(equality)]) ).
cnf(710,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[709,300,theory(equality)]) ).
cnf(711,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[710,302,theory(equality)]) ).
cnf(712,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[711,304,theory(equality)]) ).
cnf(713,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[712,306,theory(equality)]) ).
cnf(714,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[713,308,theory(equality)]) ).
cnf(715,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[714,310,theory(equality)]) ).
cnf(716,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[715,312,theory(equality)]) ).
cnf(717,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[716,314,theory(equality)]) ).
cnf(718,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[717,316,theory(equality)]) ).
cnf(719,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[718,321,theory(equality)]) ).
cnf(720,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[719,323,theory(equality)]) ).
cnf(721,negated_conjecture,
( leq(esk2_0,minus(plus(n1,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 ),
inference(rw,[status(thm)],[720,325,theory(equality)]) ).
cnf(722,negated_conjecture,
leq(esk2_0,minus(plus(n1,pv5),n1)),
inference(cn,[status(thm)],[721,theory(equality)]) ).
cnf(781,plain,
( ~ leq(esk2_0,pv5)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(spm,[status(thm)],[694,528,theory(equality)]) ).
cnf(787,plain,
( ~ leq(esk2_0,pv5)
| $false
| ~ leq(n0,esk1_0)
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[781,657,theory(equality)]) ).
cnf(788,plain,
( ~ leq(esk2_0,pv5)
| $false
| $false
| ~ leq(n0,esk2_0) ),
inference(rw,[status(thm)],[787,599,theory(equality)]) ).
cnf(789,plain,
( ~ leq(esk2_0,pv5)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[788,628,theory(equality)]) ).
cnf(790,plain,
~ leq(esk2_0,pv5),
inference(cn,[status(thm)],[789,theory(equality)]) ).
cnf(905,negated_conjecture,
leq(esk2_0,pv5),
inference(rw,[status(thm)],[722,344,theory(equality)]) ).
cnf(906,negated_conjecture,
$false,
inference(sr,[status(thm)],[905,790,theory(equality)]) ).
cnf(907,negated_conjecture,
$false,
906,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV098+1.p
% --creating new selector for [SWV003+0.ax]
% -running prover on /tmp/tmpmd5_Ab/sel_SWV098+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWV098+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV098+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV098+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
%
%------------------------------------------------------------------------------