%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV032+1 : TPTP v5.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art04.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 11:52:52 EST 2010
% Result : Theorem 0.32s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 7
% Syntax : Number of formulae : 410 ( 26 unt; 0 def)
% Number of atoms : 3143 (1109 equ)
% Maximal formula atoms : 180 ( 7 avg)
% Number of connectives : 4612 (1879 ~;2583 |; 134 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 8 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-3 aty)
% Number of variables : 75 ( 0 sgn 56 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(6,axiom,
! [X1,X2] :
( gt(X2,X1)
=> leq(X1,X2) ),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',leq_gt1) ).
fof(20,axiom,
! [X1] : leq(X1,X1),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',reflexivity_leq) ).
fof(22,axiom,
! [X4,X5,X6,X7,X8,X9,X10] :
( ( leq(X5,X4)
& leq(X4,X6)
& leq(X8,X7)
& leq(X7,X9) )
=> a_select3(tptp_const_array2(dim(X5,X6),dim(X8,X9),X10),X4,X7) = X10 ),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',const_array2_select) ).
fof(51,axiom,
gt(n1,n0),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',gt_1_0) ).
fof(52,axiom,
gt(n2,n1),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',gt_2_1) ).
fof(53,axiom,
gt(n2,n0),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',gt_2_0) ).
fof(74,conjecture,
( ( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> ! [X12] :
( ( leq(n0,X12)
& leq(X12,n3) )
=> a_select3(simplex7_init,X12,X11) = init ) )
& ! [X13] :
( ( leq(n0,X13)
& leq(X13,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X13) = init ) )
=> ( init = init
& a_select3(simplex7_init,pv1376,n0) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& leq(n0,pv19)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv1376,n3)
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n2) )
=> ! [X15] :
( ( leq(n0,X15)
& leq(X15,n3) )
=> a_select3(simplex7_init,X15,X14) = init ) )
& ! [X16] :
( ( leq(n0,X16)
& leq(X16,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X16) = init ) ) ),
file('/tmp/tmpsMelfD/sel_SWV032+1.p_1',gauss_init_0041) ).
fof(78,negated_conjecture,
~ ( ( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> ! [X12] :
( ( leq(n0,X12)
& leq(X12,n3) )
=> a_select3(simplex7_init,X12,X11) = init ) )
& ! [X13] :
( ( leq(n0,X13)
& leq(X13,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X13) = init ) )
=> ( init = init
& a_select3(simplex7_init,pv1376,n0) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& leq(n0,pv19)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv1376,n3)
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n2) )
=> ! [X15] :
( ( leq(n0,X15)
& leq(X15,n3) )
=> a_select3(simplex7_init,X15,X14) = init ) )
& ! [X16] :
( ( leq(n0,X16)
& leq(X16,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X16) = init ) ) ),
inference(assume_negation,[status(cth)],[74]) ).
fof(94,plain,
! [X1,X2] :
( ~ gt(X2,X1)
| leq(X1,X2) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(95,plain,
! [X3,X4] :
( ~ gt(X4,X3)
| leq(X3,X4) ),
inference(variable_rename,[status(thm)],[94]) ).
cnf(96,plain,
( leq(X1,X2)
| ~ gt(X2,X1) ),
inference(split_conjunct,[status(thm)],[95]) ).
fof(124,plain,
! [X2] : leq(X2,X2),
inference(variable_rename,[status(thm)],[20]) ).
cnf(125,plain,
leq(X1,X1),
inference(split_conjunct,[status(thm)],[124]) ).
fof(128,plain,
! [X4,X5,X6,X7,X8,X9,X10] :
( ~ leq(X5,X4)
| ~ leq(X4,X6)
| ~ leq(X8,X7)
| ~ leq(X7,X9)
| a_select3(tptp_const_array2(dim(X5,X6),dim(X8,X9),X10),X4,X7) = X10 ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(129,plain,
! [X11,X12,X13,X14,X15,X16,X17] :
( ~ leq(X12,X11)
| ~ leq(X11,X13)
| ~ leq(X15,X14)
| ~ leq(X14,X16)
| a_select3(tptp_const_array2(dim(X12,X13),dim(X15,X16),X17),X11,X14) = X17 ),
inference(variable_rename,[status(thm)],[128]) ).
cnf(130,plain,
( a_select3(tptp_const_array2(dim(X1,X2),dim(X3,X4),X5),X6,X7) = X5
| ~ leq(X7,X4)
| ~ leq(X3,X7)
| ~ leq(X6,X2)
| ~ leq(X1,X6) ),
inference(split_conjunct,[status(thm)],[129]) ).
cnf(172,plain,
gt(n1,n0),
inference(split_conjunct,[status(thm)],[51]) ).
cnf(173,plain,
gt(n2,n1),
inference(split_conjunct,[status(thm)],[52]) ).
cnf(174,plain,
gt(n2,n0),
inference(split_conjunct,[status(thm)],[53]) ).
fof(205,negated_conjecture,
( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X11] :
( ~ leq(n0,X11)
| ~ leq(X11,n2)
| ! [X12] :
( ~ leq(n0,X12)
| ~ leq(X12,n3)
| a_select3(simplex7_init,X12,X11) = init ) )
& ! [X13] :
( ~ leq(n0,X13)
| ~ leq(X13,minus(pv1376,n1))
| a_select2(s_values7_init,X13) = init )
& ( init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ? [X14] :
( leq(n0,X14)
& leq(X14,n2)
& ? [X15] :
( leq(n0,X15)
& leq(X15,n3)
& a_select3(simplex7_init,X15,X14) != init ) )
| ? [X16] :
( leq(n0,X16)
& leq(X16,minus(pv1376,n1))
& a_select2(s_values7_init,X16) != init ) ) ),
inference(fof_nnf,[status(thm)],[78]) ).
fof(206,negated_conjecture,
( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X17] :
( ~ leq(n0,X17)
| ~ leq(X17,n2)
| ! [X18] :
( ~ leq(n0,X18)
| ~ leq(X18,n3)
| a_select3(simplex7_init,X18,X17) = init ) )
& ! [X19] :
( ~ leq(n0,X19)
| ~ leq(X19,minus(pv1376,n1))
| a_select2(s_values7_init,X19) = init )
& ( init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ? [X20] :
( leq(n0,X20)
& leq(X20,n2)
& ? [X21] :
( leq(n0,X21)
& leq(X21,n3)
& a_select3(simplex7_init,X21,X20) != init ) )
| ? [X22] :
( leq(n0,X22)
& leq(X22,minus(pv1376,n1))
& a_select2(s_values7_init,X22) != init ) ) ),
inference(variable_rename,[status(thm)],[205]) ).
fof(207,negated_conjecture,
( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X17] :
( ~ leq(n0,X17)
| ~ leq(X17,n2)
| ! [X18] :
( ~ leq(n0,X18)
| ~ leq(X18,n3)
| a_select3(simplex7_init,X18,X17) = init ) )
& ! [X19] :
( ~ leq(n0,X19)
| ~ leq(X19,minus(pv1376,n1))
| a_select2(s_values7_init,X19) = init )
& ( init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ( leq(n0,esk1_0)
& leq(esk1_0,n2)
& leq(n0,esk2_0)
& leq(esk2_0,n3)
& a_select3(simplex7_init,esk2_0,esk1_0) != init )
| ( leq(n0,esk3_0)
& leq(esk3_0,minus(pv1376,n1))
& a_select2(s_values7_init,esk3_0) != init ) ) ),
inference(skolemize,[status(esa)],[206]) ).
fof(208,negated_conjecture,
! [X17,X18,X19] :
( ( ~ leq(n0,X19)
| ~ leq(X19,minus(pv1376,n1))
| a_select2(s_values7_init,X19) = init )
& ( ~ leq(n0,X18)
| ~ leq(X18,n3)
| a_select3(simplex7_init,X18,X17) = init
| ~ leq(n0,X17)
| ~ leq(X17,n2) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ( init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ( leq(n0,esk1_0)
& leq(esk1_0,n2)
& leq(n0,esk2_0)
& leq(esk2_0,n3)
& a_select3(simplex7_init,esk2_0,esk1_0) != init )
| ( leq(n0,esk3_0)
& leq(esk3_0,minus(pv1376,n1))
& a_select2(s_values7_init,esk3_0) != init ) ) ),
inference(shift_quantors,[status(thm)],[207]) ).
fof(209,negated_conjecture,
! [X17,X18,X19] :
( ( ~ leq(n0,X19)
| ~ leq(X19,minus(pv1376,n1))
| a_select2(s_values7_init,X19) = init )
& ( ~ leq(n0,X18)
| ~ leq(X18,n3)
| a_select3(simplex7_init,X18,X17) = init
| ~ leq(n0,X17)
| ~ leq(X17,n2) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ( leq(n0,esk3_0)
| leq(n0,esk1_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( a_select2(s_values7_init,esk3_0) != init
| leq(n0,esk1_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(n0,esk3_0)
| leq(esk1_0,n2)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( a_select2(s_values7_init,esk3_0) != init
| leq(esk1_0,n2)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(n0,esk3_0)
| leq(n0,esk2_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( a_select2(s_values7_init,esk3_0) != init
| leq(n0,esk2_0)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(n0,esk3_0)
| leq(esk2_0,n3)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( a_select2(s_values7_init,esk3_0) != init
| leq(esk2_0,n3)
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(n0,esk3_0)
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) )
& ( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| init != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3) ) ),
inference(distribute,[status(thm)],[208]) ).
cnf(210,negated_conjecture,
( ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(211,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select3(simplex7_init,esk2_0,esk1_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(212,negated_conjecture,
( leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select3(simplex7_init,esk2_0,esk1_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(213,negated_conjecture,
( leq(esk2_0,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select2(s_values7_init,esk3_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(214,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(215,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(216,negated_conjecture,
( leq(n0,esk2_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select2(s_values7_init,esk3_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(217,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(218,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(219,negated_conjecture,
( leq(esk1_0,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select2(s_values7_init,esk3_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(220,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(221,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(222,negated_conjecture,
( leq(n0,esk1_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false
| a_select2(s_values7_init,esk3_0) != init ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(223,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(224,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv19)
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,pv1376,n0) != init
| $false ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(225,negated_conjecture,
leq(pv1376,n3),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(226,negated_conjecture,
leq(pv20,minus(n330,n1)),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(227,negated_conjecture,
leq(pv19,minus(n410,n1)),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(228,negated_conjecture,
leq(n0,pv1376),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(229,negated_conjecture,
leq(n0,pv20),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(230,negated_conjecture,
leq(n0,pv19),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(232,negated_conjecture,
( a_select3(simplex7_init,X2,X1) = init
| ~ leq(X1,n2)
| ~ leq(n0,X1)
| ~ leq(X2,n3)
| ~ leq(n0,X2) ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(233,negated_conjecture,
( a_select2(s_values7_init,X1) = init
| ~ leq(X1,minus(pv1376,n1))
| ~ leq(n0,X1) ),
inference(split_conjunct,[status(thm)],[209]) ).
cnf(274,negated_conjecture,
( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[210,230,theory(equality)]) ).
cnf(275,negated_conjecture,
( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[274,228,theory(equality)]) ).
cnf(276,negated_conjecture,
( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[275,225,theory(equality)]) ).
cnf(277,negated_conjecture,
( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[276,227,theory(equality)]) ).
cnf(278,negated_conjecture,
( a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[277,theory(equality)]) ).
cnf(279,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[222,230,theory(equality)]) ).
cnf(280,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[279,228,theory(equality)]) ).
cnf(281,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[280,225,theory(equality)]) ).
cnf(282,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[281,227,theory(equality)]) ).
cnf(283,negated_conjecture,
( leq(n0,esk1_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[282,theory(equality)]) ).
cnf(284,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[216,230,theory(equality)]) ).
cnf(285,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[284,228,theory(equality)]) ).
cnf(286,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[285,225,theory(equality)]) ).
cnf(287,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[286,227,theory(equality)]) ).
cnf(288,negated_conjecture,
( leq(n0,esk2_0)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[287,theory(equality)]) ).
cnf(289,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[219,230,theory(equality)]) ).
cnf(290,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[289,228,theory(equality)]) ).
cnf(291,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[290,225,theory(equality)]) ).
cnf(292,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[291,227,theory(equality)]) ).
cnf(293,negated_conjecture,
( leq(esk1_0,n2)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[292,theory(equality)]) ).
cnf(294,negated_conjecture,
( leq(esk2_0,n3)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[213,230,theory(equality)]) ).
cnf(295,negated_conjecture,
( leq(esk2_0,n3)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[294,228,theory(equality)]) ).
cnf(296,negated_conjecture,
( leq(esk2_0,n3)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[295,225,theory(equality)]) ).
cnf(297,negated_conjecture,
( leq(esk2_0,n3)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[296,227,theory(equality)]) ).
cnf(298,negated_conjecture,
( leq(esk2_0,n3)
| a_select2(s_values7_init,esk3_0) != init
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[297,theory(equality)]) ).
cnf(299,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[212,230,theory(equality)]) ).
cnf(300,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[299,228,theory(equality)]) ).
cnf(301,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[300,225,theory(equality)]) ).
cnf(302,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[301,227,theory(equality)]) ).
cnf(303,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[302,theory(equality)]) ).
cnf(304,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[224,230,theory(equality)]) ).
cnf(305,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[304,228,theory(equality)]) ).
cnf(306,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[305,225,theory(equality)]) ).
cnf(307,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[306,227,theory(equality)]) ).
cnf(308,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[307,theory(equality)]) ).
cnf(309,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[218,230,theory(equality)]) ).
cnf(310,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[309,228,theory(equality)]) ).
cnf(311,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[310,225,theory(equality)]) ).
cnf(312,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[311,227,theory(equality)]) ).
cnf(313,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[312,theory(equality)]) ).
cnf(314,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[221,230,theory(equality)]) ).
cnf(315,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[314,228,theory(equality)]) ).
cnf(316,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[315,225,theory(equality)]) ).
cnf(317,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[316,227,theory(equality)]) ).
cnf(318,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[317,theory(equality)]) ).
cnf(319,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[215,230,theory(equality)]) ).
cnf(320,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[319,228,theory(equality)]) ).
cnf(321,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[320,225,theory(equality)]) ).
cnf(322,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[321,227,theory(equality)]) ).
cnf(323,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[322,theory(equality)]) ).
cnf(327,plain,
leq(n0,n2),
inference(spm,[status(thm)],[96,174,theory(equality)]) ).
cnf(328,plain,
leq(n1,n2),
inference(spm,[status(thm)],[96,173,theory(equality)]) ).
cnf(329,plain,
leq(n0,n1),
inference(spm,[status(thm)],[96,172,theory(equality)]) ).
cnf(377,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[211,230,theory(equality)]) ).
cnf(378,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[377,228,theory(equality)]) ).
cnf(379,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[378,225,theory(equality)]) ).
cnf(380,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[379,227,theory(equality)]) ).
cnf(381,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[380,theory(equality)]) ).
cnf(382,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[223,230,theory(equality)]) ).
cnf(383,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[382,228,theory(equality)]) ).
cnf(384,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[383,225,theory(equality)]) ).
cnf(385,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[384,227,theory(equality)]) ).
cnf(386,negated_conjecture,
( leq(n0,esk1_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[385,theory(equality)]) ).
cnf(387,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[217,230,theory(equality)]) ).
cnf(388,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[387,228,theory(equality)]) ).
cnf(389,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[388,225,theory(equality)]) ).
cnf(390,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[389,227,theory(equality)]) ).
cnf(391,negated_conjecture,
( leq(n0,esk2_0)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[390,theory(equality)]) ).
cnf(392,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[220,230,theory(equality)]) ).
cnf(393,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[392,228,theory(equality)]) ).
cnf(394,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[393,225,theory(equality)]) ).
cnf(395,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[394,227,theory(equality)]) ).
cnf(396,negated_conjecture,
( leq(esk1_0,n2)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[395,theory(equality)]) ).
cnf(397,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[214,230,theory(equality)]) ).
cnf(398,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| ~ leq(pv1376,n3)
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[397,228,theory(equality)]) ).
cnf(399,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| ~ leq(pv19,minus(n410,n1)) ),
inference(rw,[status(thm)],[398,225,theory(equality)]) ).
cnf(400,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[399,227,theory(equality)]) ).
cnf(401,negated_conjecture,
( leq(esk2_0,n3)
| leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) != init ),
inference(cn,[status(thm)],[400,theory(equality)]) ).
cnf(611,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[278,130,theory(equality)]) ).
cnf(612,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[283,130,theory(equality)]) ).
cnf(613,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[288,130,theory(equality)]) ).
cnf(614,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[293,130,theory(equality)]) ).
cnf(615,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[298,130,theory(equality)]) ).
cnf(616,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[303,130,theory(equality)]) ).
cnf(617,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[308,130,theory(equality)]) ).
cnf(618,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[313,130,theory(equality)]) ).
cnf(619,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[318,130,theory(equality)]) ).
cnf(620,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[323,130,theory(equality)]) ).
cnf(621,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[381,130,theory(equality)]) ).
cnf(622,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[386,130,theory(equality)]) ).
cnf(623,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[391,130,theory(equality)]) ).
cnf(624,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[396,130,theory(equality)]) ).
cnf(625,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(spm,[status(thm)],[401,130,theory(equality)]) ).
cnf(626,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[611,226,theory(equality)]) ).
cnf(627,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[626,227,theory(equality)]) ).
cnf(628,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[627,229,theory(equality)]) ).
cnf(629,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[628,230,theory(equality)]) ).
cnf(630,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(cn,[status(thm)],[629,theory(equality)]) ).
cnf(631,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[612,226,theory(equality)]) ).
cnf(632,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[631,227,theory(equality)]) ).
cnf(633,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[632,229,theory(equality)]) ).
cnf(634,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[633,230,theory(equality)]) ).
cnf(635,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(cn,[status(thm)],[634,theory(equality)]) ).
cnf(636,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[613,226,theory(equality)]) ).
cnf(637,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[636,227,theory(equality)]) ).
cnf(638,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[637,229,theory(equality)]) ).
cnf(639,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[638,230,theory(equality)]) ).
cnf(640,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(cn,[status(thm)],[639,theory(equality)]) ).
cnf(641,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[614,226,theory(equality)]) ).
cnf(642,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[641,227,theory(equality)]) ).
cnf(643,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[642,229,theory(equality)]) ).
cnf(644,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[643,230,theory(equality)]) ).
cnf(645,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(cn,[status(thm)],[644,theory(equality)]) ).
cnf(646,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[615,226,theory(equality)]) ).
cnf(647,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[646,227,theory(equality)]) ).
cnf(648,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[647,229,theory(equality)]) ).
cnf(649,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[648,230,theory(equality)]) ).
cnf(650,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select2(s_values7_init,esk3_0) != init ),
inference(cn,[status(thm)],[649,theory(equality)]) ).
cnf(651,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[616,226,theory(equality)]) ).
cnf(652,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[651,227,theory(equality)]) ).
cnf(653,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[652,229,theory(equality)]) ).
cnf(654,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[653,230,theory(equality)]) ).
cnf(655,negated_conjecture,
( leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init ),
inference(cn,[status(thm)],[654,theory(equality)]) ).
cnf(656,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[617,226,theory(equality)]) ).
cnf(657,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[656,227,theory(equality)]) ).
cnf(658,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[657,229,theory(equality)]) ).
cnf(659,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[658,230,theory(equality)]) ).
cnf(660,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[659,theory(equality)]) ).
cnf(661,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[618,226,theory(equality)]) ).
cnf(662,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[661,227,theory(equality)]) ).
cnf(663,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[662,229,theory(equality)]) ).
cnf(664,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[663,230,theory(equality)]) ).
cnf(665,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[664,theory(equality)]) ).
cnf(666,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[619,226,theory(equality)]) ).
cnf(667,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[666,227,theory(equality)]) ).
cnf(668,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[667,229,theory(equality)]) ).
cnf(669,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[668,230,theory(equality)]) ).
cnf(670,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[669,theory(equality)]) ).
cnf(671,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[620,226,theory(equality)]) ).
cnf(672,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[671,227,theory(equality)]) ).
cnf(673,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[672,229,theory(equality)]) ).
cnf(674,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[673,230,theory(equality)]) ).
cnf(675,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[674,theory(equality)]) ).
cnf(676,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[621,226,theory(equality)]) ).
cnf(677,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[676,227,theory(equality)]) ).
cnf(678,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[677,229,theory(equality)]) ).
cnf(679,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[678,230,theory(equality)]) ).
cnf(680,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init ),
inference(cn,[status(thm)],[679,theory(equality)]) ).
cnf(681,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[622,226,theory(equality)]) ).
cnf(682,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[681,227,theory(equality)]) ).
cnf(683,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[682,229,theory(equality)]) ).
cnf(684,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[683,230,theory(equality)]) ).
cnf(685,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[684,theory(equality)]) ).
cnf(686,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[623,226,theory(equality)]) ).
cnf(687,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[686,227,theory(equality)]) ).
cnf(688,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[687,229,theory(equality)]) ).
cnf(689,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[688,230,theory(equality)]) ).
cnf(690,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[689,theory(equality)]) ).
cnf(691,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[624,226,theory(equality)]) ).
cnf(692,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[691,227,theory(equality)]) ).
cnf(693,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[692,229,theory(equality)]) ).
cnf(694,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[693,230,theory(equality)]) ).
cnf(695,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[694,theory(equality)]) ).
cnf(696,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[625,226,theory(equality)]) ).
cnf(697,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[696,227,theory(equality)]) ).
cnf(698,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,pv19) ),
inference(rw,[status(thm)],[697,229,theory(equality)]) ).
cnf(699,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[698,230,theory(equality)]) ).
cnf(700,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[699,theory(equality)]) ).
cnf(781,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| ~ leq(n0,esk3_0) ),
inference(spm,[status(thm)],[630,233,theory(equality)]) ).
cnf(782,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| ~ leq(n0,esk3_0) ),
inference(spm,[status(thm)],[635,233,theory(equality)]) ).
cnf(783,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| ~ leq(n0,esk3_0) ),
inference(spm,[status(thm)],[640,233,theory(equality)]) ).
cnf(784,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| ~ leq(n0,esk3_0) ),
inference(spm,[status(thm)],[645,233,theory(equality)]) ).
cnf(785,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| ~ leq(n0,esk3_0) ),
inference(spm,[status(thm)],[650,233,theory(equality)]) ).
cnf(787,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[660,232,theory(equality)]) ).
cnf(789,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[787,225,theory(equality)]) ).
cnf(790,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[789,125,theory(equality)]) ).
cnf(791,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[790,228,theory(equality)]) ).
cnf(792,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[791,327,theory(equality)]) ).
cnf(793,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[792,theory(equality)]) ).
cnf(797,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[793,232,theory(equality)]) ).
cnf(798,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[797,225,theory(equality)]) ).
cnf(799,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[798,327,theory(equality)]) ).
cnf(800,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[799,228,theory(equality)]) ).
cnf(801,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[800,125,theory(equality)]) ).
cnf(802,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[801,theory(equality)]) ).
cnf(803,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[802,232,theory(equality)]) ).
cnf(804,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[803,225,theory(equality)]) ).
cnf(805,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[804,328,theory(equality)]) ).
cnf(806,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[805,228,theory(equality)]) ).
cnf(807,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[806,329,theory(equality)]) ).
cnf(808,negated_conjecture,
( leq(n0,esk1_0)
| leq(n0,esk3_0) ),
inference(cn,[status(thm)],[807,theory(equality)]) ).
cnf(810,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[665,232,theory(equality)]) ).
cnf(812,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[810,225,theory(equality)]) ).
cnf(813,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[812,125,theory(equality)]) ).
cnf(814,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[813,228,theory(equality)]) ).
cnf(815,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[814,327,theory(equality)]) ).
cnf(816,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[815,theory(equality)]) ).
cnf(817,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[816,232,theory(equality)]) ).
cnf(818,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[817,225,theory(equality)]) ).
cnf(819,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[818,327,theory(equality)]) ).
cnf(820,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[819,228,theory(equality)]) ).
cnf(821,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[820,125,theory(equality)]) ).
cnf(822,negated_conjecture,
( leq(n0,esk3_0)
| leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[821,theory(equality)]) ).
cnf(823,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[822,232,theory(equality)]) ).
cnf(824,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[823,225,theory(equality)]) ).
cnf(825,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[824,328,theory(equality)]) ).
cnf(826,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[825,228,theory(equality)]) ).
cnf(827,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[826,329,theory(equality)]) ).
cnf(828,negated_conjecture,
( leq(n0,esk2_0)
| leq(n0,esk3_0) ),
inference(cn,[status(thm)],[827,theory(equality)]) ).
cnf(830,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[670,232,theory(equality)]) ).
cnf(832,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[830,225,theory(equality)]) ).
cnf(833,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[832,125,theory(equality)]) ).
cnf(834,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[833,228,theory(equality)]) ).
cnf(835,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[834,327,theory(equality)]) ).
cnf(836,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[835,theory(equality)]) ).
cnf(837,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[836,232,theory(equality)]) ).
cnf(838,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[837,225,theory(equality)]) ).
cnf(839,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[838,327,theory(equality)]) ).
cnf(840,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[839,228,theory(equality)]) ).
cnf(841,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[840,125,theory(equality)]) ).
cnf(842,negated_conjecture,
( leq(esk1_0,n2)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[841,theory(equality)]) ).
cnf(843,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[842,232,theory(equality)]) ).
cnf(844,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[843,225,theory(equality)]) ).
cnf(845,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[844,328,theory(equality)]) ).
cnf(846,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[845,228,theory(equality)]) ).
cnf(847,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[846,329,theory(equality)]) ).
cnf(848,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk1_0,n2) ),
inference(cn,[status(thm)],[847,theory(equality)]) ).
cnf(855,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[675,232,theory(equality)]) ).
cnf(857,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[855,225,theory(equality)]) ).
cnf(858,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[857,125,theory(equality)]) ).
cnf(859,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[858,228,theory(equality)]) ).
cnf(860,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[859,327,theory(equality)]) ).
cnf(861,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[860,theory(equality)]) ).
cnf(862,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[861,232,theory(equality)]) ).
cnf(863,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[862,225,theory(equality)]) ).
cnf(864,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[863,327,theory(equality)]) ).
cnf(865,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[864,228,theory(equality)]) ).
cnf(866,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[865,125,theory(equality)]) ).
cnf(867,negated_conjecture,
( leq(esk2_0,n3)
| leq(n0,esk3_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[866,theory(equality)]) ).
cnf(868,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[867,232,theory(equality)]) ).
cnf(869,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[868,225,theory(equality)]) ).
cnf(870,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[869,328,theory(equality)]) ).
cnf(871,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[870,228,theory(equality)]) ).
cnf(872,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[871,329,theory(equality)]) ).
cnf(873,negated_conjecture,
( leq(n0,esk3_0)
| leq(esk2_0,n3) ),
inference(cn,[status(thm)],[872,theory(equality)]) ).
cnf(887,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init
| ~ leq(esk3_0,minus(pv1376,n1)) ),
inference(csr,[status(thm)],[781,655]) ).
cnf(890,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| a_select3(simplex7_init,esk2_0,esk1_0) != init ),
inference(csr,[status(thm)],[680,887]) ).
cnf(891,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0) ),
inference(spm,[status(thm)],[890,232,theory(equality)]) ).
cnf(892,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[891,232,theory(equality)]) ).
cnf(894,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[892,225,theory(equality)]) ).
cnf(895,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[894,125,theory(equality)]) ).
cnf(896,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[895,228,theory(equality)]) ).
cnf(897,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[896,327,theory(equality)]) ).
cnf(898,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0) ),
inference(cn,[status(thm)],[897,theory(equality)]) ).
cnf(899,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[898,232,theory(equality)]) ).
cnf(900,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[899,225,theory(equality)]) ).
cnf(901,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[900,327,theory(equality)]) ).
cnf(902,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[901,228,theory(equality)]) ).
cnf(903,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[902,125,theory(equality)]) ).
cnf(904,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0) ),
inference(cn,[status(thm)],[903,theory(equality)]) ).
cnf(905,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[904,232,theory(equality)]) ).
cnf(906,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[905,225,theory(equality)]) ).
cnf(907,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[906,328,theory(equality)]) ).
cnf(908,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[907,228,theory(equality)]) ).
cnf(909,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[908,329,theory(equality)]) ).
cnf(910,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0) ),
inference(cn,[status(thm)],[909,theory(equality)]) ).
cnf(911,negated_conjecture,
( leq(n0,esk3_0)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| ~ leq(n0,esk1_0) ),
inference(spm,[status(thm)],[910,873,theory(equality)]) ).
cnf(912,negated_conjecture,
( leq(n0,esk3_0)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0) ),
inference(csr,[status(thm)],[911,808]) ).
cnf(913,negated_conjecture,
( leq(n0,esk3_0)
| ~ leq(esk1_0,n2) ),
inference(csr,[status(thm)],[912,828]) ).
cnf(914,negated_conjecture,
leq(n0,esk3_0),
inference(csr,[status(thm)],[913,848]) ).
cnf(923,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| $false ),
inference(rw,[status(thm)],[782,914,theory(equality)]) ).
cnf(924,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1)) ),
inference(cn,[status(thm)],[923,theory(equality)]) ).
cnf(927,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| $false ),
inference(rw,[status(thm)],[783,914,theory(equality)]) ).
cnf(928,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1)) ),
inference(cn,[status(thm)],[927,theory(equality)]) ).
cnf(931,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| $false ),
inference(rw,[status(thm)],[784,914,theory(equality)]) ).
cnf(932,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1)) ),
inference(cn,[status(thm)],[931,theory(equality)]) ).
cnf(935,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1))
| $false ),
inference(rw,[status(thm)],[785,914,theory(equality)]) ).
cnf(936,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(esk3_0,minus(pv1376,n1)) ),
inference(cn,[status(thm)],[935,theory(equality)]) ).
cnf(939,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(csr,[status(thm)],[685,924]) ).
cnf(940,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[939,232,theory(equality)]) ).
cnf(942,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[940,225,theory(equality)]) ).
cnf(943,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[942,125,theory(equality)]) ).
cnf(944,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[943,228,theory(equality)]) ).
cnf(945,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[944,327,theory(equality)]) ).
cnf(946,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[945,theory(equality)]) ).
cnf(947,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[946,232,theory(equality)]) ).
cnf(948,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[947,225,theory(equality)]) ).
cnf(949,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[948,327,theory(equality)]) ).
cnf(950,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[949,228,theory(equality)]) ).
cnf(951,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[950,125,theory(equality)]) ).
cnf(952,negated_conjecture,
( leq(n0,esk1_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[951,theory(equality)]) ).
cnf(953,negated_conjecture,
( leq(n0,esk1_0)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[952,232,theory(equality)]) ).
cnf(954,negated_conjecture,
( leq(n0,esk1_0)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[953,225,theory(equality)]) ).
cnf(955,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[954,328,theory(equality)]) ).
cnf(956,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[955,228,theory(equality)]) ).
cnf(957,negated_conjecture,
( leq(n0,esk1_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[956,329,theory(equality)]) ).
cnf(958,negated_conjecture,
leq(n0,esk1_0),
inference(cn,[status(thm)],[957,theory(equality)]) ).
cnf(961,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0)
| $false ),
inference(rw,[status(thm)],[910,958,theory(equality)]) ).
cnf(962,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| ~ leq(n0,esk2_0) ),
inference(cn,[status(thm)],[961,theory(equality)]) ).
cnf(963,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(csr,[status(thm)],[690,928]) ).
cnf(964,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[963,232,theory(equality)]) ).
cnf(966,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[964,225,theory(equality)]) ).
cnf(967,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[966,125,theory(equality)]) ).
cnf(968,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[967,228,theory(equality)]) ).
cnf(969,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[968,327,theory(equality)]) ).
cnf(970,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[969,theory(equality)]) ).
cnf(971,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[970,232,theory(equality)]) ).
cnf(972,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[971,225,theory(equality)]) ).
cnf(973,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[972,327,theory(equality)]) ).
cnf(974,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[973,228,theory(equality)]) ).
cnf(975,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[974,125,theory(equality)]) ).
cnf(976,negated_conjecture,
( leq(n0,esk2_0)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[975,theory(equality)]) ).
cnf(977,negated_conjecture,
( leq(n0,esk2_0)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[976,232,theory(equality)]) ).
cnf(978,negated_conjecture,
( leq(n0,esk2_0)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[977,225,theory(equality)]) ).
cnf(979,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[978,328,theory(equality)]) ).
cnf(980,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[979,228,theory(equality)]) ).
cnf(981,negated_conjecture,
( leq(n0,esk2_0)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[980,329,theory(equality)]) ).
cnf(982,negated_conjecture,
leq(n0,esk2_0),
inference(cn,[status(thm)],[981,theory(equality)]) ).
cnf(985,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2)
| $false ),
inference(rw,[status(thm)],[962,982,theory(equality)]) ).
cnf(986,negated_conjecture,
( ~ leq(esk2_0,n3)
| ~ leq(esk1_0,n2) ),
inference(cn,[status(thm)],[985,theory(equality)]) ).
cnf(987,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(csr,[status(thm)],[695,932]) ).
cnf(988,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[987,232,theory(equality)]) ).
cnf(990,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[988,225,theory(equality)]) ).
cnf(991,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[990,125,theory(equality)]) ).
cnf(992,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[991,228,theory(equality)]) ).
cnf(993,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[992,327,theory(equality)]) ).
cnf(994,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[993,theory(equality)]) ).
cnf(995,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[994,232,theory(equality)]) ).
cnf(996,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[995,225,theory(equality)]) ).
cnf(997,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[996,327,theory(equality)]) ).
cnf(998,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[997,228,theory(equality)]) ).
cnf(999,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[998,125,theory(equality)]) ).
cnf(1000,negated_conjecture,
( leq(esk1_0,n2)
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[999,theory(equality)]) ).
cnf(1001,negated_conjecture,
( leq(esk1_0,n2)
| ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[1000,232,theory(equality)]) ).
cnf(1002,negated_conjecture,
( leq(esk1_0,n2)
| $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1001,225,theory(equality)]) ).
cnf(1003,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1002,328,theory(equality)]) ).
cnf(1004,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1003,228,theory(equality)]) ).
cnf(1005,negated_conjecture,
( leq(esk1_0,n2)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1004,329,theory(equality)]) ).
cnf(1006,negated_conjecture,
leq(esk1_0,n2),
inference(cn,[status(thm)],[1005,theory(equality)]) ).
cnf(1011,negated_conjecture,
( ~ leq(esk2_0,n3)
| $false ),
inference(rw,[status(thm)],[986,1006,theory(equality)]) ).
cnf(1012,negated_conjecture,
~ leq(esk2_0,n3),
inference(cn,[status(thm)],[1011,theory(equality)]) ).
cnf(1133,negated_conjecture,
( leq(esk3_0,minus(pv1376,n1))
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(sr,[status(thm)],[700,1012,theory(equality)]) ).
cnf(1137,negated_conjecture,
( leq(esk2_0,n3)
| a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(spm,[status(thm)],[936,1133,theory(equality)]) ).
cnf(1138,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n2) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(sr,[status(thm)],[1137,1012,theory(equality)]) ).
cnf(1139,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(spm,[status(thm)],[1138,232,theory(equality)]) ).
cnf(1141,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n2,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[1139,225,theory(equality)]) ).
cnf(1142,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[1141,125,theory(equality)]) ).
cnf(1143,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n2) ),
inference(rw,[status(thm)],[1142,228,theory(equality)]) ).
cnf(1144,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1143,327,theory(equality)]) ).
cnf(1145,negated_conjecture,
( a_select3(simplex7_init,pv1376,n0) != init
| a_select3(simplex7_init,pv1376,n1) != init ),
inference(cn,[status(thm)],[1144,theory(equality)]) ).
cnf(1146,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| ~ leq(pv1376,n3)
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(spm,[status(thm)],[1145,232,theory(equality)]) ).
cnf(1147,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| $false
| ~ leq(n0,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[1146,225,theory(equality)]) ).
cnf(1148,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[1147,327,theory(equality)]) ).
cnf(1149,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| ~ leq(n0,n0) ),
inference(rw,[status(thm)],[1148,228,theory(equality)]) ).
cnf(1150,negated_conjecture,
( a_select3(simplex7_init,pv1376,n1) != init
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1149,125,theory(equality)]) ).
cnf(1151,negated_conjecture,
a_select3(simplex7_init,pv1376,n1) != init,
inference(cn,[status(thm)],[1150,theory(equality)]) ).
cnf(1152,negated_conjecture,
( ~ leq(pv1376,n3)
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(spm,[status(thm)],[1151,232,theory(equality)]) ).
cnf(1153,negated_conjecture,
( $false
| ~ leq(n1,n2)
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1152,225,theory(equality)]) ).
cnf(1154,negated_conjecture,
( $false
| $false
| ~ leq(n0,pv1376)
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1153,328,theory(equality)]) ).
cnf(1155,negated_conjecture,
( $false
| $false
| $false
| ~ leq(n0,n1) ),
inference(rw,[status(thm)],[1154,228,theory(equality)]) ).
cnf(1156,negated_conjecture,
( $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1155,329,theory(equality)]) ).
cnf(1157,negated_conjecture,
$false,
inference(cn,[status(thm)],[1156,theory(equality)]) ).
cnf(1158,negated_conjecture,
$false,
1157,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV032+1.p
% --creating new selector for [SWV003+0.ax]
% -running prover on /tmp/tmpsMelfD/sel_SWV032+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWV032+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV032+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV032+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
%
%------------------------------------------------------------------------------