%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM859+1 : TPTP v7.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n134.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Mon Jan 8 15:22:32 EST 2018
% Result : Theorem 20.80s
% Output : CNFRefutation 20.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 13
% Syntax : Number of formulae : 290 ( 15 unt; 0 def)
% Number of atoms : 864 ( 105 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 920 ( 346 ~; 503 |; 59 &)
% ( 8 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 468 ( 9 sgn 137 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1,X2,X3] :
( minsol_model_ub(X1,X2,X3)
<=> ( model_ub(X1,X2,X3)
& ! [X4] :
( model_ub(X1,X2,X4)
=> lesseq(X3,X4) ) ) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',minsol_model_ub) ).
fof(2,axiom,
! [X1,X2,X3] :
( minsol_model_max(X1,X2,X3)
<=> ( model_max(X1,X2,X3)
& ! [X4] :
( model_max(X1,X2,X4)
=> lesseq(X3,X4) ) ) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',minsol_model_max) ).
fof(3,axiom,
! [X1,X2,X4] :
( ( lesseq(X1,X2)
& lesseq(X2,X4) )
=> lesseq(X1,X4) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',lesseq_trans) ).
fof(5,axiom,
! [X1,X2] :
( lesseq(X1,X2)
| lesseq(X2,X1) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',lesseq_total) ).
fof(6,axiom,
! [X1,X2] :
( equal(max(X1,X2),X2)
| ~ lesseq(X1,X2) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',max_2) ).
fof(7,axiom,
! [X1] : lesseq(X1,X1),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',lesseq_ref) ).
fof(8,axiom,
! [X1,X2] :
( equal(max(X1,X2),X1)
| ~ lesseq(X2,X1) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',max_1) ).
fof(9,conjecture,
! [X1,X2,X4] :
( minsol_model_ub(X1,X2,X4)
<=> minsol_model_max(X1,X2,X4) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',max_is_ub_1) ).
fof(10,axiom,
! [X1,X2,X4] :
( ub(X1,X2,X4)
<=> ( lesseq(X1,X4)
& lesseq(X2,X4) ) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',ub) ).
fof(11,axiom,
! [X1,X2,X3] :
( model_max(X1,X2,X3)
<=> lesseq(max(X1,X2),X3) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',model_max_2) ).
fof(12,axiom,
! [X1,X2] :
( ( lesseq(X1,X2)
& lesseq(X2,X1) )
=> equal(X1,X2) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',lesseq_antisymmetric) ).
fof(13,axiom,
! [X1,X2,X3] :
( model_ub(X1,X2,X3)
<=> ? [X4] :
( ub(X1,X2,X4)
& lesseq(X4,X3) ) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',model_ub_2) ).
fof(14,axiom,
! [X1,X2] :
( lesseq(X1,X2)
<=> lesseq(summation(X1),summation(X2)) ),
file('/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1',summation_monotone) ).
fof(15,negated_conjecture,
~ ! [X1,X2,X4] :
( minsol_model_ub(X1,X2,X4)
<=> minsol_model_max(X1,X2,X4) ),
inference(assume_negation,[status(cth)],[9]) ).
fof(16,plain,
! [X1,X2] :
( equal(max(X1,X2),X2)
| ~ lesseq(X1,X2) ),
inference(fof_simplification,[status(thm)],[6,theory(equality)]) ).
fof(17,plain,
! [X1,X2] :
( equal(max(X1,X2),X1)
| ~ lesseq(X2,X1) ),
inference(fof_simplification,[status(thm)],[8,theory(equality)]) ).
fof(18,plain,
! [X1,X2,X3] :
( ( ~ minsol_model_ub(X1,X2,X3)
| ( model_ub(X1,X2,X3)
& ! [X4] :
( ~ model_ub(X1,X2,X4)
| lesseq(X3,X4) ) ) )
& ( ~ model_ub(X1,X2,X3)
| ? [X4] :
( model_ub(X1,X2,X4)
& ~ lesseq(X3,X4) )
| minsol_model_ub(X1,X2,X3) ) ),
inference(fof_nnf,[status(thm)],[1]) ).
fof(19,plain,
! [X5,X6,X7] :
( ( ~ minsol_model_ub(X5,X6,X7)
| ( model_ub(X5,X6,X7)
& ! [X8] :
( ~ model_ub(X5,X6,X8)
| lesseq(X7,X8) ) ) )
& ( ~ model_ub(X5,X6,X7)
| ? [X9] :
( model_ub(X5,X6,X9)
& ~ lesseq(X7,X9) )
| minsol_model_ub(X5,X6,X7) ) ),
inference(variable_rename,[status(thm)],[18]) ).
fof(20,plain,
! [X5,X6,X7] :
( ( ~ minsol_model_ub(X5,X6,X7)
| ( model_ub(X5,X6,X7)
& ! [X8] :
( ~ model_ub(X5,X6,X8)
| lesseq(X7,X8) ) ) )
& ( ~ model_ub(X5,X6,X7)
| ( model_ub(X5,X6,esk1_3(X5,X6,X7))
& ~ lesseq(X7,esk1_3(X5,X6,X7)) )
| minsol_model_ub(X5,X6,X7) ) ),
inference(skolemize,[status(esa)],[19]) ).
fof(21,plain,
! [X5,X6,X7,X8] :
( ( ( ( ~ model_ub(X5,X6,X8)
| lesseq(X7,X8) )
& model_ub(X5,X6,X7) )
| ~ minsol_model_ub(X5,X6,X7) )
& ( ~ model_ub(X5,X6,X7)
| ( model_ub(X5,X6,esk1_3(X5,X6,X7))
& ~ lesseq(X7,esk1_3(X5,X6,X7)) )
| minsol_model_ub(X5,X6,X7) ) ),
inference(shift_quantors,[status(thm)],[20]) ).
fof(22,plain,
! [X5,X6,X7,X8] :
( ( ~ model_ub(X5,X6,X8)
| lesseq(X7,X8)
| ~ minsol_model_ub(X5,X6,X7) )
& ( model_ub(X5,X6,X7)
| ~ minsol_model_ub(X5,X6,X7) )
& ( model_ub(X5,X6,esk1_3(X5,X6,X7))
| ~ model_ub(X5,X6,X7)
| minsol_model_ub(X5,X6,X7) )
& ( ~ lesseq(X7,esk1_3(X5,X6,X7))
| ~ model_ub(X5,X6,X7)
| minsol_model_ub(X5,X6,X7) ) ),
inference(distribute,[status(thm)],[21]) ).
cnf(23,plain,
( minsol_model_ub(X1,X2,X3)
| ~ model_ub(X1,X2,X3)
| ~ lesseq(X3,esk1_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(24,plain,
( minsol_model_ub(X1,X2,X3)
| model_ub(X1,X2,esk1_3(X1,X2,X3))
| ~ model_ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(25,plain,
( model_ub(X1,X2,X3)
| ~ minsol_model_ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(26,plain,
( lesseq(X3,X4)
| ~ minsol_model_ub(X1,X2,X3)
| ~ model_ub(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[22]) ).
fof(27,plain,
! [X1,X2,X3] :
( ( ~ minsol_model_max(X1,X2,X3)
| ( model_max(X1,X2,X3)
& ! [X4] :
( ~ model_max(X1,X2,X4)
| lesseq(X3,X4) ) ) )
& ( ~ model_max(X1,X2,X3)
| ? [X4] :
( model_max(X1,X2,X4)
& ~ lesseq(X3,X4) )
| minsol_model_max(X1,X2,X3) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(28,plain,
! [X5,X6,X7] :
( ( ~ minsol_model_max(X5,X6,X7)
| ( model_max(X5,X6,X7)
& ! [X8] :
( ~ model_max(X5,X6,X8)
| lesseq(X7,X8) ) ) )
& ( ~ model_max(X5,X6,X7)
| ? [X9] :
( model_max(X5,X6,X9)
& ~ lesseq(X7,X9) )
| minsol_model_max(X5,X6,X7) ) ),
inference(variable_rename,[status(thm)],[27]) ).
fof(29,plain,
! [X5,X6,X7] :
( ( ~ minsol_model_max(X5,X6,X7)
| ( model_max(X5,X6,X7)
& ! [X8] :
( ~ model_max(X5,X6,X8)
| lesseq(X7,X8) ) ) )
& ( ~ model_max(X5,X6,X7)
| ( model_max(X5,X6,esk2_3(X5,X6,X7))
& ~ lesseq(X7,esk2_3(X5,X6,X7)) )
| minsol_model_max(X5,X6,X7) ) ),
inference(skolemize,[status(esa)],[28]) ).
fof(30,plain,
! [X5,X6,X7,X8] :
( ( ( ( ~ model_max(X5,X6,X8)
| lesseq(X7,X8) )
& model_max(X5,X6,X7) )
| ~ minsol_model_max(X5,X6,X7) )
& ( ~ model_max(X5,X6,X7)
| ( model_max(X5,X6,esk2_3(X5,X6,X7))
& ~ lesseq(X7,esk2_3(X5,X6,X7)) )
| minsol_model_max(X5,X6,X7) ) ),
inference(shift_quantors,[status(thm)],[29]) ).
fof(31,plain,
! [X5,X6,X7,X8] :
( ( ~ model_max(X5,X6,X8)
| lesseq(X7,X8)
| ~ minsol_model_max(X5,X6,X7) )
& ( model_max(X5,X6,X7)
| ~ minsol_model_max(X5,X6,X7) )
& ( model_max(X5,X6,esk2_3(X5,X6,X7))
| ~ model_max(X5,X6,X7)
| minsol_model_max(X5,X6,X7) )
& ( ~ lesseq(X7,esk2_3(X5,X6,X7))
| ~ model_max(X5,X6,X7)
| minsol_model_max(X5,X6,X7) ) ),
inference(distribute,[status(thm)],[30]) ).
cnf(32,plain,
( minsol_model_max(X1,X2,X3)
| ~ model_max(X1,X2,X3)
| ~ lesseq(X3,esk2_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[31]) ).
cnf(33,plain,
( minsol_model_max(X1,X2,X3)
| model_max(X1,X2,esk2_3(X1,X2,X3))
| ~ model_max(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[31]) ).
cnf(34,plain,
( model_max(X1,X2,X3)
| ~ minsol_model_max(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[31]) ).
cnf(35,plain,
( lesseq(X3,X4)
| ~ minsol_model_max(X1,X2,X3)
| ~ model_max(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[31]) ).
fof(36,plain,
! [X1,X2,X4] :
( ~ lesseq(X1,X2)
| ~ lesseq(X2,X4)
| lesseq(X1,X4) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(37,plain,
! [X5,X6,X7] :
( ~ lesseq(X5,X6)
| ~ lesseq(X6,X7)
| lesseq(X5,X7) ),
inference(variable_rename,[status(thm)],[36]) ).
cnf(38,plain,
( lesseq(X1,X2)
| ~ lesseq(X3,X2)
| ~ lesseq(X1,X3) ),
inference(split_conjunct,[status(thm)],[37]) ).
fof(43,plain,
! [X3,X4] :
( lesseq(X3,X4)
| lesseq(X4,X3) ),
inference(variable_rename,[status(thm)],[5]) ).
cnf(44,plain,
( lesseq(X1,X2)
| lesseq(X2,X1) ),
inference(split_conjunct,[status(thm)],[43]) ).
fof(45,plain,
! [X3,X4] :
( equal(max(X3,X4),X4)
| ~ lesseq(X3,X4) ),
inference(variable_rename,[status(thm)],[16]) ).
cnf(46,plain,
( max(X1,X2) = X2
| ~ lesseq(X1,X2) ),
inference(split_conjunct,[status(thm)],[45]) ).
fof(47,plain,
! [X2] : lesseq(X2,X2),
inference(variable_rename,[status(thm)],[7]) ).
cnf(48,plain,
lesseq(X1,X1),
inference(split_conjunct,[status(thm)],[47]) ).
fof(49,plain,
! [X3,X4] :
( equal(max(X3,X4),X3)
| ~ lesseq(X4,X3) ),
inference(variable_rename,[status(thm)],[17]) ).
cnf(50,plain,
( max(X2,X1) = X2
| ~ lesseq(X1,X2) ),
inference(split_conjunct,[status(thm)],[49]) ).
fof(51,negated_conjecture,
? [X1,X2,X4] :
( ( ~ minsol_model_ub(X1,X2,X4)
| ~ minsol_model_max(X1,X2,X4) )
& ( minsol_model_ub(X1,X2,X4)
| minsol_model_max(X1,X2,X4) ) ),
inference(fof_nnf,[status(thm)],[15]) ).
fof(52,negated_conjecture,
? [X5,X6,X7] :
( ( ~ minsol_model_ub(X5,X6,X7)
| ~ minsol_model_max(X5,X6,X7) )
& ( minsol_model_ub(X5,X6,X7)
| minsol_model_max(X5,X6,X7) ) ),
inference(variable_rename,[status(thm)],[51]) ).
fof(53,negated_conjecture,
( ( ~ minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ minsol_model_max(esk3_0,esk4_0,esk5_0) )
& ( minsol_model_ub(esk3_0,esk4_0,esk5_0)
| minsol_model_max(esk3_0,esk4_0,esk5_0) ) ),
inference(skolemize,[status(esa)],[52]) ).
cnf(54,negated_conjecture,
( minsol_model_max(esk3_0,esk4_0,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(split_conjunct,[status(thm)],[53]) ).
cnf(55,negated_conjecture,
( ~ minsol_model_max(esk3_0,esk4_0,esk5_0)
| ~ minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(split_conjunct,[status(thm)],[53]) ).
fof(56,plain,
! [X1,X2,X4] :
( ( ~ ub(X1,X2,X4)
| ( lesseq(X1,X4)
& lesseq(X2,X4) ) )
& ( ~ lesseq(X1,X4)
| ~ lesseq(X2,X4)
| ub(X1,X2,X4) ) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(57,plain,
! [X5,X6,X7] :
( ( ~ ub(X5,X6,X7)
| ( lesseq(X5,X7)
& lesseq(X6,X7) ) )
& ( ~ lesseq(X5,X7)
| ~ lesseq(X6,X7)
| ub(X5,X6,X7) ) ),
inference(variable_rename,[status(thm)],[56]) ).
fof(58,plain,
! [X5,X6,X7] :
( ( lesseq(X5,X7)
| ~ ub(X5,X6,X7) )
& ( lesseq(X6,X7)
| ~ ub(X5,X6,X7) )
& ( ~ lesseq(X5,X7)
| ~ lesseq(X6,X7)
| ub(X5,X6,X7) ) ),
inference(distribute,[status(thm)],[57]) ).
cnf(59,plain,
( ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| ~ lesseq(X1,X3) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(60,plain,
( lesseq(X2,X3)
| ~ ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(61,plain,
( lesseq(X1,X3)
| ~ ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[58]) ).
fof(62,plain,
! [X1,X2,X3] :
( ( ~ model_max(X1,X2,X3)
| lesseq(max(X1,X2),X3) )
& ( ~ lesseq(max(X1,X2),X3)
| model_max(X1,X2,X3) ) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(63,plain,
! [X4,X5,X6] :
( ( ~ model_max(X4,X5,X6)
| lesseq(max(X4,X5),X6) )
& ( ~ lesseq(max(X4,X5),X6)
| model_max(X4,X5,X6) ) ),
inference(variable_rename,[status(thm)],[62]) ).
cnf(64,plain,
( model_max(X1,X2,X3)
| ~ lesseq(max(X1,X2),X3) ),
inference(split_conjunct,[status(thm)],[63]) ).
cnf(65,plain,
( lesseq(max(X1,X2),X3)
| ~ model_max(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[63]) ).
fof(66,plain,
! [X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X2,X1)
| equal(X1,X2) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(67,plain,
! [X3,X4] :
( ~ lesseq(X3,X4)
| ~ lesseq(X4,X3)
| equal(X3,X4) ),
inference(variable_rename,[status(thm)],[66]) ).
cnf(68,plain,
( X1 = X2
| ~ lesseq(X2,X1)
| ~ lesseq(X1,X2) ),
inference(split_conjunct,[status(thm)],[67]) ).
fof(69,plain,
! [X1,X2,X3] :
( ( ~ model_ub(X1,X2,X3)
| ? [X4] :
( ub(X1,X2,X4)
& lesseq(X4,X3) ) )
& ( ! [X4] :
( ~ ub(X1,X2,X4)
| ~ lesseq(X4,X3) )
| model_ub(X1,X2,X3) ) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(70,plain,
! [X5,X6,X7] :
( ( ~ model_ub(X5,X6,X7)
| ? [X8] :
( ub(X5,X6,X8)
& lesseq(X8,X7) ) )
& ( ! [X9] :
( ~ ub(X5,X6,X9)
| ~ lesseq(X9,X7) )
| model_ub(X5,X6,X7) ) ),
inference(variable_rename,[status(thm)],[69]) ).
fof(71,plain,
! [X5,X6,X7] :
( ( ~ model_ub(X5,X6,X7)
| ( ub(X5,X6,esk6_3(X5,X6,X7))
& lesseq(esk6_3(X5,X6,X7),X7) ) )
& ( ! [X9] :
( ~ ub(X5,X6,X9)
| ~ lesseq(X9,X7) )
| model_ub(X5,X6,X7) ) ),
inference(skolemize,[status(esa)],[70]) ).
fof(72,plain,
! [X5,X6,X7,X9] :
( ( ~ ub(X5,X6,X9)
| ~ lesseq(X9,X7)
| model_ub(X5,X6,X7) )
& ( ~ model_ub(X5,X6,X7)
| ( ub(X5,X6,esk6_3(X5,X6,X7))
& lesseq(esk6_3(X5,X6,X7),X7) ) ) ),
inference(shift_quantors,[status(thm)],[71]) ).
fof(73,plain,
! [X5,X6,X7,X9] :
( ( ~ ub(X5,X6,X9)
| ~ lesseq(X9,X7)
| model_ub(X5,X6,X7) )
& ( ub(X5,X6,esk6_3(X5,X6,X7))
| ~ model_ub(X5,X6,X7) )
& ( lesseq(esk6_3(X5,X6,X7),X7)
| ~ model_ub(X5,X6,X7) ) ),
inference(distribute,[status(thm)],[72]) ).
cnf(74,plain,
( lesseq(esk6_3(X1,X2,X3),X3)
| ~ model_ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[73]) ).
cnf(75,plain,
( ub(X1,X2,esk6_3(X1,X2,X3))
| ~ model_ub(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[73]) ).
cnf(76,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X4,X3)
| ~ ub(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[73]) ).
fof(77,plain,
! [X1,X2] :
( ( ~ lesseq(X1,X2)
| lesseq(summation(X1),summation(X2)) )
& ( ~ lesseq(summation(X1),summation(X2))
| lesseq(X1,X2) ) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(78,plain,
! [X3,X4] :
( ( ~ lesseq(X3,X4)
| lesseq(summation(X3),summation(X4)) )
& ( ~ lesseq(summation(X3),summation(X4))
| lesseq(X3,X4) ) ),
inference(variable_rename,[status(thm)],[77]) ).
cnf(79,plain,
( lesseq(X1,X2)
| ~ lesseq(summation(X1),summation(X2)) ),
inference(split_conjunct,[status(thm)],[78]) ).
cnf(80,plain,
( lesseq(summation(X1),summation(X2))
| ~ lesseq(X1,X2) ),
inference(split_conjunct,[status(thm)],[78]) ).
cnf(86,negated_conjecture,
( model_max(esk3_0,esk4_0,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[34,54,theory(equality)]) ).
cnf(90,plain,
( summation(X1) = summation(X2)
| ~ lesseq(summation(X1),summation(X2))
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[68,80,theory(equality)]) ).
cnf(92,plain,
( lesseq(X1,X2)
| lesseq(summation(X2),summation(X1)) ),
inference(spm,[status(thm)],[79,44,theory(equality)]) ).
cnf(96,plain,
model_max(X1,X2,max(X1,X2)),
inference(spm,[status(thm)],[64,48,theory(equality)]) ).
cnf(97,plain,
( model_max(X1,X2,X3)
| lesseq(X3,max(X1,X2)) ),
inference(spm,[status(thm)],[64,44,theory(equality)]) ).
cnf(99,plain,
( model_max(X1,X2,X3)
| ~ lesseq(X1,X3)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[64,50,theory(equality)]) ).
cnf(101,plain,
( lesseq(X1,X3)
| ~ model_max(X1,X2,X3)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[65,50,theory(equality)]) ).
cnf(102,plain,
( lesseq(X2,X3)
| ~ model_max(X1,X2,X3)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[65,46,theory(equality)]) ).
cnf(103,plain,
( X1 = max(X2,X3)
| ~ lesseq(X1,max(X2,X3))
| ~ model_max(X2,X3,X1) ),
inference(spm,[status(thm)],[68,65,theory(equality)]) ).
cnf(106,plain,
( lesseq(X1,X2)
| lesseq(X2,X3)
| ~ lesseq(X1,X3) ),
inference(spm,[status(thm)],[38,44,theory(equality)]) ).
cnf(108,plain,
( lesseq(X1,summation(X2))
| ~ lesseq(X1,summation(X3))
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[38,80,theory(equality)]) ).
cnf(109,plain,
( lesseq(X1,X2)
| ~ lesseq(X1,max(X3,X4))
| ~ model_max(X3,X4,X2) ),
inference(spm,[status(thm)],[38,65,theory(equality)]) ).
cnf(114,plain,
( X1 = esk6_3(X2,X3,X1)
| ~ lesseq(X1,esk6_3(X2,X3,X1))
| ~ model_ub(X2,X3,X1) ),
inference(spm,[status(thm)],[68,74,theory(equality)]) ).
cnf(115,plain,
( lesseq(X1,X2)
| ~ lesseq(X1,esk6_3(X3,X4,X2))
| ~ model_ub(X3,X4,X2) ),
inference(spm,[status(thm)],[38,74,theory(equality)]) ).
cnf(121,plain,
( lesseq(X1,esk6_3(X2,X1,X3))
| ~ model_ub(X2,X1,X3) ),
inference(spm,[status(thm)],[60,75,theory(equality)]) ).
cnf(122,plain,
( lesseq(X1,esk6_3(X1,X2,X3))
| ~ model_ub(X1,X2,X3) ),
inference(spm,[status(thm)],[61,75,theory(equality)]) ).
cnf(123,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X4,X3)
| ~ lesseq(X2,X4)
| ~ lesseq(X1,X4) ),
inference(spm,[status(thm)],[76,59,theory(equality)]) ).
cnf(126,plain,
( minsol_model_max(X1,X2,max(X3,X4))
| ~ model_max(X1,X2,max(X3,X4))
| ~ model_max(X3,X4,esk2_3(X1,X2,max(X3,X4))) ),
inference(spm,[status(thm)],[32,65,theory(equality)]) ).
cnf(129,plain,
( model_max(X1,X2,X1)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[96,50,theory(equality)]) ).
cnf(130,plain,
( model_max(X1,X2,X2)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[96,46,theory(equality)]) ).
cnf(131,plain,
( lesseq(X1,max(X2,X3))
| ~ minsol_model_max(X2,X3,X1) ),
inference(spm,[status(thm)],[35,96,theory(equality)]) ).
cnf(132,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk5_0)
| model_max(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[25,86,theory(equality)]) ).
cnf(136,plain,
( lesseq(X1,X2)
| ~ minsol_model_max(X2,X3,X1)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[35,129,theory(equality)]) ).
cnf(137,plain,
( lesseq(X1,X2)
| ~ minsol_model_max(X3,X2,X1)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[35,130,theory(equality)]) ).
cnf(149,plain,
( summation(X1) = summation(X2)
| ~ lesseq(X2,X1)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[90,80,theory(equality)]) ).
cnf(182,plain,
( lesseq(X1,max(X2,X3))
| lesseq(X4,X1)
| model_max(X2,X3,X4) ),
inference(spm,[status(thm)],[106,97,theory(equality)]) ).
cnf(224,plain,
( lesseq(X1,max(X1,X2))
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[101,96,theory(equality)]) ).
cnf(226,negated_conjecture,
( lesseq(esk3_0,esk5_0)
| model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[101,132,theory(equality)]) ).
cnf(243,plain,
( lesseq(X1,max(X2,X3))
| ~ lesseq(X1,X2)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[38,224,theory(equality)]) ).
cnf(246,plain,
( lesseq(X1,max(X2,X1))
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[102,96,theory(equality)]) ).
cnf(248,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[102,132,theory(equality)]) ).
cnf(258,plain,
( lesseq(X1,max(X2,X3))
| ~ lesseq(X1,X3)
| ~ lesseq(X2,X3) ),
inference(spm,[status(thm)],[38,246,theory(equality)]) ).
cnf(324,plain,
( X1 = max(X2,X3)
| ~ model_max(X2,X3,X1)
| ~ minsol_model_max(X2,X3,X1) ),
inference(spm,[status(thm)],[103,131,theory(equality)]) ).
cnf(335,plain,
( model_max(X1,X2,X3)
| lesseq(X4,X1)
| lesseq(X3,X4)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[182,50,theory(equality)]) ).
cnf(365,plain,
( esk6_3(X1,X2,X3) = X1
| ~ lesseq(esk6_3(X1,X2,X3),X1)
| ~ model_ub(X1,X2,X3) ),
inference(spm,[status(thm)],[68,122,theory(equality)]) ).
cnf(371,plain,
( X1 = max(X2,X3)
| ~ minsol_model_max(X2,X3,X1) ),
inference(csr,[status(thm)],[324,34]) ).
cnf(372,negated_conjecture,
( esk5_0 = max(esk3_0,esk4_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[371,54,theory(equality)]) ).
cnf(375,negated_conjecture,
( esk5_0 = esk4_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[46,372,theory(equality)]) ).
cnf(376,negated_conjecture,
( model_max(esk3_0,esk4_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[64,372,theory(equality)]) ).
cnf(377,negated_conjecture,
( lesseq(esk5_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ model_max(esk3_0,esk4_0,X1) ),
inference(spm,[status(thm)],[65,372,theory(equality)]) ).
cnf(378,negated_conjecture,
( lesseq(X1,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ minsol_model_max(esk3_0,esk4_0,X1) ),
inference(spm,[status(thm)],[131,372,theory(equality)]) ).
cnf(399,plain,
( lesseq(summation(X1),summation(X2))
| ~ lesseq(X3,X2)
| ~ lesseq(X1,X3) ),
inference(spm,[status(thm)],[108,80,theory(equality)]) ).
cnf(402,plain,
( lesseq(summation(X1),summation(X2))
| lesseq(X3,X1)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[108,92,theory(equality)]) ).
cnf(410,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk5_0)
| esk5_0 = esk4_0
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[25,375,theory(equality)]) ).
cnf(508,negated_conjecture,
( model_max(esk3_0,esk4_0,max(X1,X2))
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| model_max(X1,X2,esk5_0) ),
inference(spm,[status(thm)],[376,97,theory(equality)]) ).
cnf(527,negated_conjecture,
( lesseq(esk5_0,max(esk3_0,esk4_0))
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[377,96,theory(equality)]) ).
cnf(532,negated_conjecture,
( lesseq(esk5_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk3_0,X1)
| ~ lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[377,99,theory(equality)]) ).
cnf(594,plain,
( esk6_3(X1,X2,X2) = X2
| ~ model_ub(X1,X2,X2) ),
inference(spm,[status(thm)],[114,121,theory(equality)]) ).
cnf(597,plain,
( ub(X1,X2,X2)
| ~ model_ub(X1,X2,X2) ),
inference(spm,[status(thm)],[75,594,theory(equality)]) ).
cnf(604,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| ~ model_ub(X1,X2,X2) ),
inference(spm,[status(thm)],[76,597,theory(equality)]) ).
cnf(621,plain,
( lesseq(X1,X2)
| ~ model_ub(X3,X1,X2) ),
inference(spm,[status(thm)],[115,121,theory(equality)]) ).
cnf(622,plain,
( lesseq(X1,X2)
| ~ model_ub(X1,X3,X2) ),
inference(spm,[status(thm)],[115,122,theory(equality)]) ).
cnf(624,plain,
( lesseq(X1,esk1_3(X2,X1,X3))
| minsol_model_ub(X2,X1,X3)
| ~ model_ub(X2,X1,X3) ),
inference(spm,[status(thm)],[621,24,theory(equality)]) ).
cnf(628,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[621,248,theory(equality)]) ).
cnf(631,negated_conjecture,
( esk5_0 = esk4_0
| ~ lesseq(esk5_0,esk4_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[68,628,theory(equality)]) ).
cnf(634,plain,
( lesseq(X1,esk1_3(X1,X2,X3))
| minsol_model_ub(X1,X2,X3)
| ~ model_ub(X1,X2,X3) ),
inference(spm,[status(thm)],[622,24,theory(equality)]) ).
cnf(637,negated_conjecture,
( lesseq(esk3_0,esk5_0)
| ~ lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[622,226,theory(equality)]) ).
cnf(639,negated_conjecture,
( lesseq(esk3_0,esk5_0)
| esk5_0 = esk4_0
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[622,410,theory(equality)]) ).
cnf(640,negated_conjecture,
( lesseq(esk3_0,esk5_0)
| lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[637,44,theory(equality)]) ).
cnf(645,negated_conjecture,
( esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0)
| ~ lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[68,640,theory(equality)]) ).
cnf(651,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| ~ lesseq(X1,X3) ),
inference(spm,[status(thm)],[123,48,theory(equality)]) ).
cnf(680,negated_conjecture,
( esk5_0 = esk4_0
| lesseq(esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[631,44,theory(equality)]) ).
cnf(686,negated_conjecture,
( esk5_0 = esk4_0
| lesseq(esk3_0,esk5_0) ),
inference(csr,[status(thm)],[639,640]) ).
cnf(689,negated_conjecture,
( lesseq(X1,esk5_0)
| lesseq(esk3_0,X1)
| esk5_0 = esk4_0 ),
inference(spm,[status(thm)],[106,686,theory(equality)]) ).
cnf(734,negated_conjecture,
( esk5_0 = esk4_0
| lesseq(esk4_0,esk5_0) ),
inference(csr,[status(thm)],[680,689]) ).
cnf(735,negated_conjecture,
( esk5_0 = esk4_0
| ~ lesseq(esk5_0,esk4_0) ),
inference(spm,[status(thm)],[68,734,theory(equality)]) ).
cnf(790,plain,
( minsol_model_max(X1,X2,max(X1,X2))
| ~ model_max(X1,X2,max(X1,X2)) ),
inference(spm,[status(thm)],[126,33,theory(equality)]) ).
cnf(799,plain,
( minsol_model_max(X1,X2,max(X1,X2))
| $false ),
inference(rw,[status(thm)],[790,96,theory(equality)]) ).
cnf(800,plain,
minsol_model_max(X1,X2,max(X1,X2)),
inference(cn,[status(thm)],[799,theory(equality)]) ).
cnf(805,plain,
( lesseq(max(X1,X2),X1)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[136,800,theory(equality)]) ).
cnf(806,plain,
( lesseq(max(X1,X2),X2)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[137,800,theory(equality)]) ).
cnf(809,negated_conjecture,
( lesseq(max(esk3_0,esk4_0),esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[378,800,theory(equality)]) ).
cnf(835,negated_conjecture,
( model_ub(X1,X2,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(X2,max(esk3_0,esk4_0))
| ~ lesseq(X1,max(esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[123,809,theory(equality)]) ).
cnf(1574,plain,
( lesseq(X1,X2)
| ~ minsol_model_ub(X3,X4,X1)
| ~ lesseq(X4,X2)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[26,651,theory(equality)]) ).
cnf(1875,negated_conjecture,
( model_max(esk3_0,esk4_0,X1)
| model_max(X1,X2,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[508,50,theory(equality)]) ).
cnf(2197,plain,
( max(X1,X2) = X3
| ~ lesseq(max(X1,X2),X3)
| ~ lesseq(X3,X1)
| ~ lesseq(X2,X1) ),
inference(spm,[status(thm)],[68,243,theory(equality)]) ).
cnf(2201,plain,
( X1 = max(X2,X3)
| ~ model_max(X2,X3,X1)
| ~ lesseq(X1,X2)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[103,243,theory(equality)]) ).
cnf(2437,plain,
( max(X1,X2) = X3
| ~ lesseq(max(X1,X2),X3)
| ~ lesseq(X3,X2)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[68,258,theory(equality)]) ).
cnf(3169,negated_conjecture,
( lesseq(esk5_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| lesseq(esk3_0,esk4_0)
| ~ lesseq(esk3_0,X1) ),
inference(spm,[status(thm)],[532,44,theory(equality)]) ).
cnf(3219,plain,
( lesseq(summation(X1),summation(X2))
| lesseq(max(X2,X3),X1)
| ~ lesseq(X3,X2) ),
inference(spm,[status(thm)],[402,805,theory(equality)]) ).
cnf(3831,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| ~ lesseq(X2,X2)
| ~ lesseq(X1,X2) ),
inference(spm,[status(thm)],[604,651,theory(equality)]) ).
cnf(3834,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| $false
| ~ lesseq(X1,X2) ),
inference(rw,[status(thm)],[3831,48,theory(equality)]) ).
cnf(3835,plain,
( model_ub(X1,X2,X3)
| ~ lesseq(X2,X3)
| ~ lesseq(X1,X2) ),
inference(cn,[status(thm)],[3834,theory(equality)]) ).
cnf(3840,plain,
( lesseq(X1,X2)
| ~ minsol_model_ub(X3,X4,X1)
| ~ lesseq(X4,X2)
| ~ lesseq(X3,X4) ),
inference(spm,[status(thm)],[26,3835,theory(equality)]) ).
cnf(3973,negated_conjecture,
( lesseq(esk3_0,esk4_0)
| lesseq(esk5_0,esk3_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[3169,48,theory(equality)]) ).
cnf(3981,negated_conjecture,
( lesseq(esk3_0,esk4_0)
| lesseq(esk5_0,max(esk3_0,X1))
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[3169,224,theory(equality)]) ).
cnf(4043,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk5_0)
| lesseq(esk5_0,esk3_0)
| lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[25,3973,theory(equality)]) ).
cnf(4054,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| lesseq(esk3_0,esk4_0)
| lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[621,4043,theory(equality)]) ).
cnf(4056,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| lesseq(esk5_0,esk3_0) ),
inference(csr,[status(thm)],[4054,628]) ).
cnf(4058,negated_conjecture,
( lesseq(X1,esk3_0)
| lesseq(esk4_0,esk5_0)
| ~ lesseq(X1,esk5_0) ),
inference(spm,[status(thm)],[38,4056,theory(equality)]) ).
cnf(4060,negated_conjecture,
( model_max(esk3_0,esk4_0,esk3_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| lesseq(esk4_0,esk5_0) ),
inference(spm,[status(thm)],[376,4056,theory(equality)]) ).
cnf(4063,negated_conjecture,
( esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0)
| lesseq(esk4_0,esk5_0) ),
inference(spm,[status(thm)],[645,4056,theory(equality)]) ).
cnf(4084,negated_conjecture,
( esk5_0 = esk3_0
| lesseq(esk4_0,esk5_0) ),
inference(csr,[status(thm)],[4063,628]) ).
cnf(4087,negated_conjecture,
( lesseq(X1,esk5_0)
| lesseq(esk4_0,X1)
| esk5_0 = esk3_0 ),
inference(spm,[status(thm)],[106,4084,theory(equality)]) ).
cnf(4126,negated_conjecture,
( lesseq(esk3_0,esk5_0)
| esk5_0 = esk3_0 ),
inference(spm,[status(thm)],[637,4087,theory(equality)]) ).
cnf(4153,negated_conjecture,
( esk5_0 = esk3_0
| ~ lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[68,4126,theory(equality)]) ).
cnf(4270,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk5_0)
| model_max(esk3_0,esk4_0,esk3_0)
| lesseq(esk4_0,esk5_0) ),
inference(spm,[status(thm)],[25,4060,theory(equality)]) ).
cnf(4289,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| lesseq(esk4_0,esk3_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[4058,628,theory(equality)]) ).
cnf(4567,negated_conjecture,
( model_max(esk3_0,esk4_0,esk3_0)
| lesseq(esk4_0,esk5_0) ),
inference(csr,[status(thm)],[4270,621]) ).
cnf(4570,negated_conjecture,
( lesseq(esk4_0,esk3_0)
| lesseq(esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[102,4567,theory(equality)]) ).
cnf(4836,negated_conjecture,
( lesseq(esk4_0,esk5_0)
| lesseq(esk4_0,esk3_0) ),
inference(csr,[status(thm)],[4289,44]) ).
cnf(4839,negated_conjecture,
( lesseq(X1,esk5_0)
| lesseq(esk4_0,X1)
| lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[106,4836,theory(equality)]) ).
cnf(4867,negated_conjecture,
( lesseq(esk4_0,esk3_0)
| lesseq(esk3_0,esk5_0) ),
inference(ef,[status(thm)],[4839,theory(equality)]) ).
cnf(4918,negated_conjecture,
lesseq(esk3_0,esk5_0),
inference(csr,[status(thm)],[4867,637]) ).
cnf(4920,negated_conjecture,
( lesseq(X1,esk5_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[38,4918,theory(equality)]) ).
cnf(4923,negated_conjecture,
( summation(esk5_0) = summation(esk3_0)
| ~ lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[149,4918,theory(equality)]) ).
cnf(4928,negated_conjecture,
( lesseq(summation(X1),summation(esk5_0))
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[399,4918,theory(equality)]) ).
cnf(4993,negated_conjecture,
( model_max(X1,X2,esk5_0)
| ~ lesseq(max(X1,X2),esk3_0) ),
inference(spm,[status(thm)],[64,4920,theory(equality)]) ).
cnf(5151,negated_conjecture,
( lesseq(summation(esk3_0),summation(esk5_0))
| ~ lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[4928,4923,theory(equality)]) ).
cnf(5209,negated_conjecture,
( lesseq(esk4_0,esk3_0)
| lesseq(esk4_0,esk5_0) ),
inference(csr,[status(thm)],[4570,44]) ).
cnf(5210,negated_conjecture,
lesseq(esk4_0,esk5_0),
inference(csr,[status(thm)],[5209,4920]) ).
cnf(5212,negated_conjecture,
( lesseq(X1,esk5_0)
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[38,5210,theory(equality)]) ).
cnf(5215,negated_conjecture,
( summation(esk5_0) = summation(esk4_0)
| ~ lesseq(esk5_0,esk4_0) ),
inference(spm,[status(thm)],[149,5210,theory(equality)]) ).
cnf(5220,negated_conjecture,
( lesseq(summation(X1),summation(esk5_0))
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[399,5210,theory(equality)]) ).
cnf(5267,negated_conjecture,
( model_max(X1,X2,esk5_0)
| ~ lesseq(max(X1,X2),esk4_0) ),
inference(spm,[status(thm)],[64,5212,theory(equality)]) ).
cnf(5719,negated_conjecture,
lesseq(summation(esk3_0),summation(esk5_0)),
inference(csr,[status(thm)],[5151,92]) ).
cnf(5725,negated_conjecture,
( lesseq(summation(esk3_0),summation(X1))
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[108,5719,theory(equality)]) ).
cnf(5807,negated_conjecture,
( lesseq(summation(esk4_0),summation(esk5_0))
| ~ lesseq(esk5_0,esk4_0) ),
inference(spm,[status(thm)],[5220,5215,theory(equality)]) ).
cnf(5967,negated_conjecture,
( model_max(esk3_0,X1,esk5_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[4993,805,theory(equality)]) ).
cnf(5982,negated_conjecture,
( lesseq(X1,esk5_0)
| ~ minsol_model_max(esk3_0,X2,X1)
| ~ lesseq(X2,esk3_0) ),
inference(spm,[status(thm)],[35,5967,theory(equality)]) ).
cnf(6004,negated_conjecture,
( lesseq(max(esk3_0,X1),esk5_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[5982,800,theory(equality)]) ).
cnf(6015,negated_conjecture,
( lesseq(esk3_0,X1)
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[79,5725,theory(equality)]) ).
cnf(6042,negated_conjecture,
( lesseq(esk3_0,max(X1,X2))
| ~ minsol_model_max(X1,X2,esk5_0) ),
inference(spm,[status(thm)],[6015,131,theory(equality)]) ).
cnf(6052,negated_conjecture,
( lesseq(esk3_0,esk6_3(esk5_0,X1,X2))
| ~ model_ub(esk5_0,X1,X2) ),
inference(spm,[status(thm)],[6015,122,theory(equality)]) ).
cnf(6053,negated_conjecture,
( lesseq(esk3_0,max(esk3_0,esk4_0))
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[6015,527,theory(equality)]) ).
cnf(6277,negated_conjecture,
( max(X1,X2) = esk3_0
| ~ lesseq(max(X1,X2),esk3_0)
| ~ minsol_model_max(X1,X2,esk5_0) ),
inference(spm,[status(thm)],[68,6042,theory(equality)]) ).
cnf(6313,negated_conjecture,
lesseq(summation(esk4_0),summation(esk5_0)),
inference(csr,[status(thm)],[5807,92]) ).
cnf(6319,negated_conjecture,
( lesseq(summation(esk4_0),summation(X1))
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[108,6313,theory(equality)]) ).
cnf(7004,negated_conjecture,
( lesseq(esk4_0,X1)
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[79,6319,theory(equality)]) ).
cnf(7154,negated_conjecture,
( lesseq(esk4_0,max(esk3_0,esk4_0))
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[7004,527,theory(equality)]) ).
cnf(7207,negated_conjecture,
( lesseq(esk4_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ model_max(esk3_0,esk4_0,X1) ),
inference(spm,[status(thm)],[109,7154,theory(equality)]) ).
cnf(8128,negated_conjecture,
( model_max(X1,esk4_0,esk5_0)
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[5267,806,theory(equality)]) ).
cnf(8158,negated_conjecture,
( lesseq(X1,esk5_0)
| ~ minsol_model_max(X2,esk4_0,X1)
| ~ lesseq(X2,esk4_0) ),
inference(spm,[status(thm)],[35,8128,theory(equality)]) ).
cnf(8190,negated_conjecture,
( lesseq(max(X1,esk4_0),esk5_0)
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[8158,800,theory(equality)]) ).
cnf(10398,plain,
( model_max(X1,X1,X2)
| lesseq(X2,X3)
| lesseq(X3,X1) ),
inference(spm,[status(thm)],[335,48,theory(equality)]) ).
cnf(19848,negated_conjecture,
( esk6_3(esk5_0,X1,esk3_0) = esk3_0
| ~ model_ub(esk5_0,X1,esk3_0) ),
inference(spm,[status(thm)],[114,6052,theory(equality)]) ).
cnf(19974,negated_conjecture,
( esk3_0 = esk5_0
| ~ lesseq(esk3_0,esk5_0)
| ~ model_ub(esk5_0,X1,esk3_0) ),
inference(spm,[status(thm)],[365,19848,theory(equality)]) ).
cnf(19980,negated_conjecture,
( esk3_0 = esk5_0
| $false
| ~ model_ub(esk5_0,X1,esk3_0) ),
inference(rw,[status(thm)],[19974,4918,theory(equality)]) ).
cnf(19981,negated_conjecture,
( esk3_0 = esk5_0
| ~ model_ub(esk5_0,X1,esk3_0) ),
inference(cn,[status(thm)],[19980,theory(equality)]) ).
cnf(19985,negated_conjecture,
( esk5_0 = esk3_0
| ~ lesseq(X1,esk3_0)
| ~ lesseq(esk5_0,X1) ),
inference(spm,[status(thm)],[19981,3835,theory(equality)]) ).
cnf(20063,negated_conjecture,
( esk5_0 = esk3_0
| ~ lesseq(esk5_0,max(esk3_0,X1))
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[19985,805,theory(equality)]) ).
cnf(28254,plain,
( minsol_model_ub(X1,X2,X2)
| ~ model_ub(X1,X2,X2) ),
inference(spm,[status(thm)],[23,624,theory(equality)]) ).
cnf(28339,plain,
( minsol_model_ub(X1,X2,X1)
| ~ model_ub(X1,X2,X1) ),
inference(spm,[status(thm)],[23,634,theory(equality)]) ).
cnf(40685,negated_conjecture,
( model_ub(X1,esk5_0,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(X1,max(esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[835,527,theory(equality)]) ).
cnf(41780,negated_conjecture,
( model_ub(esk3_0,esk5_0,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[40685,6053,theory(equality)]) ).
cnf(41897,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk5_0)
| model_ub(esk3_0,esk5_0,esk5_0) ),
inference(spm,[status(thm)],[25,41780,theory(equality)]) ).
cnf(125612,negated_conjecture,
( model_max(esk3_0,esk4_0,X1)
| model_max(X1,X1,esk5_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(spm,[status(thm)],[1875,48,theory(equality)]) ).
cnf(126364,negated_conjecture,
( lesseq(esk4_0,X1)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| model_max(X1,X1,esk5_0) ),
inference(spm,[status(thm)],[7207,125612,theory(equality)]) ).
cnf(161837,negated_conjecture,
( max(esk3_0,X1) = esk5_0
| ~ lesseq(esk5_0,esk3_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[2197,6004,theory(equality)]) ).
cnf(162202,negated_conjecture,
( minsol_model_max(esk3_0,X1,esk5_0)
| ~ lesseq(esk5_0,esk3_0)
| ~ lesseq(X1,esk3_0) ),
inference(spm,[status(thm)],[800,161837,theory(equality)]) ).
cnf(162704,negated_conjecture,
( ~ minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk5_0,esk3_0)
| ~ lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[55,162202,theory(equality)]) ).
cnf(163641,negated_conjecture,
( ~ lesseq(esk5_0,esk3_0)
| ~ minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(csr,[status(thm)],[162704,7004]) ).
cnf(163642,negated_conjecture,
( model_max(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk5_0,esk3_0) ),
inference(spm,[status(thm)],[163641,86,theory(equality)]) ).
cnf(164900,negated_conjecture,
( esk5_0 = max(esk3_0,esk4_0)
| ~ lesseq(esk5_0,esk3_0)
| ~ lesseq(esk4_0,esk3_0) ),
inference(spm,[status(thm)],[2201,163642,theory(equality)]) ).
cnf(166070,negated_conjecture,
( max(esk3_0,esk4_0) = esk5_0
| ~ lesseq(esk5_0,esk3_0) ),
inference(csr,[status(thm)],[164900,7004]) ).
cnf(196117,negated_conjecture,
( max(X1,esk4_0) = esk5_0
| ~ lesseq(esk5_0,esk4_0)
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[2437,8190,theory(equality)]) ).
cnf(221436,negated_conjecture,
( minsol_model_max(X1,esk4_0,esk5_0)
| ~ lesseq(esk5_0,esk4_0)
| ~ lesseq(X1,esk4_0) ),
inference(spm,[status(thm)],[800,196117,theory(equality)]) ).
cnf(223022,negated_conjecture,
( ~ minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk5_0,esk4_0)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[55,221436,theory(equality)]) ).
cnf(223764,negated_conjecture,
( ~ lesseq(esk5_0,esk4_0)
| ~ minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(csr,[status(thm)],[223022,6015]) ).
cnf(223812,negated_conjecture,
( model_max(X1,X1,esk5_0)
| lesseq(esk4_0,X1)
| ~ lesseq(esk5_0,esk4_0) ),
inference(spm,[status(thm)],[223764,126364,theory(equality)]) ).
cnf(233708,negated_conjecture,
( model_max(X1,X1,esk5_0)
| lesseq(esk4_0,X1) ),
inference(csr,[status(thm)],[223812,10398]) ).
cnf(233709,negated_conjecture,
( lesseq(X1,esk5_0)
| lesseq(esk4_0,X2)
| ~ minsol_model_max(X2,X2,X1) ),
inference(spm,[status(thm)],[35,233708,theory(equality)]) ).
cnf(233784,negated_conjecture,
( lesseq(esk4_0,X1)
| lesseq(max(X1,X1),esk5_0) ),
inference(spm,[status(thm)],[233709,800,theory(equality)]) ).
cnf(233829,negated_conjecture,
( esk5_0 = max(X1,X1)
| lesseq(esk4_0,X1)
| ~ lesseq(esk5_0,max(X1,X1)) ),
inference(spm,[status(thm)],[68,233784,theory(equality)]) ).
cnf(233831,negated_conjecture,
( lesseq(X1,esk5_0)
| lesseq(esk4_0,X2)
| ~ lesseq(X1,max(X2,X2)) ),
inference(spm,[status(thm)],[38,233784,theory(equality)]) ).
cnf(305501,plain,
( lesseq(summation(X1),summation(X2))
| lesseq(max(X2,X2),X1) ),
inference(spm,[status(thm)],[3219,48,theory(equality)]) ).
cnf(309359,plain,
( lesseq(X1,X2)
| lesseq(max(X2,X2),X1) ),
inference(spm,[status(thm)],[79,305501,theory(equality)]) ).
cnf(310921,plain,
( model_max(X1,X1,X2)
| lesseq(X2,X1) ),
inference(spm,[status(thm)],[64,309359,theory(equality)]) ).
cnf(330057,negated_conjecture,
( lesseq(esk4_0,X1)
| lesseq(max(X2,X2),esk5_0)
| lesseq(max(X1,X1),X2) ),
inference(spm,[status(thm)],[233831,309359,theory(equality)]) ).
cnf(330300,negated_conjecture,
( model_max(X1,X1,esk5_0)
| lesseq(max(X2,X2),X1)
| lesseq(esk4_0,X2) ),
inference(spm,[status(thm)],[64,330057,theory(equality)]) ).
cnf(396730,negated_conjecture,
( lesseq(esk5_0,X1)
| esk5_0 = esk4_0
| ~ lesseq(esk4_0,X1)
| ~ lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[3840,375,theory(equality)]) ).
cnf(398865,negated_conjecture,
( esk5_0 = esk4_0
| ~ lesseq(esk3_0,esk4_0)
| ~ lesseq(esk4_0,esk4_0) ),
inference(spm,[status(thm)],[735,396730,theory(equality)]) ).
cnf(399161,negated_conjecture,
( esk5_0 = esk4_0
| ~ lesseq(esk3_0,esk4_0)
| $false ),
inference(rw,[status(thm)],[398865,48,theory(equality)]) ).
cnf(399162,negated_conjecture,
( esk5_0 = esk4_0
| ~ lesseq(esk3_0,esk4_0) ),
inference(cn,[status(thm)],[399161,theory(equality)]) ).
cnf(818313,negated_conjecture,
( max(X1,X1) = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| lesseq(esk4_0,X1)
| ~ minsol_model_max(X1,X1,esk5_0) ),
inference(spm,[status(thm)],[6277,330300,theory(equality)]) ).
cnf(827304,negated_conjecture,
( esk3_0 = esk5_0
| lesseq(esk4_0,X1)
| model_max(esk3_0,esk3_0,esk5_0)
| ~ lesseq(esk5_0,esk3_0)
| ~ minsol_model_max(X1,X1,esk5_0) ),
inference(spm,[status(thm)],[233829,818313,theory(equality)]) ).
cnf(837965,negated_conjecture,
( esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| lesseq(esk4_0,X1)
| ~ lesseq(esk5_0,esk3_0) ),
inference(csr,[status(thm)],[827304,4153]) ).
cnf(837966,negated_conjecture,
( esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| lesseq(esk4_0,X1) ),
inference(csr,[status(thm)],[837965,310921]) ).
cnf(837975,negated_conjecture,
( esk4_0 = max(X1,X2)
| esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| ~ model_max(X1,X2,esk4_0) ),
inference(spm,[status(thm)],[103,837966,theory(equality)]) ).
cnf(843375,negated_conjecture,
( esk4_0 = esk5_0
| esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| ~ lesseq(esk5_0,esk3_0)
| ~ model_max(esk3_0,esk4_0,esk4_0) ),
inference(spm,[status(thm)],[166070,837975,theory(equality)]) ).
cnf(843939,negated_conjecture,
( esk5_0 = esk4_0
| esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0)
| ~ lesseq(esk5_0,esk3_0) ),
inference(csr,[status(thm)],[843375,4153]) ).
cnf(843940,negated_conjecture,
( esk5_0 = esk4_0
| esk5_0 = esk3_0
| model_max(esk3_0,esk3_0,esk5_0) ),
inference(csr,[status(thm)],[843939,310921]) ).
cnf(843941,negated_conjecture,
( lesseq(X1,esk5_0)
| esk5_0 = esk3_0
| esk5_0 = esk4_0
| ~ minsol_model_max(esk3_0,esk3_0,X1) ),
inference(spm,[status(thm)],[35,843940,theory(equality)]) ).
cnf(845692,negated_conjecture,
( esk5_0 = esk4_0
| esk5_0 = esk3_0
| lesseq(max(esk3_0,esk3_0),esk5_0) ),
inference(spm,[status(thm)],[843941,800,theory(equality)]) ).
cnf(845743,negated_conjecture,
( esk5_0 = max(esk3_0,esk3_0)
| esk5_0 = esk3_0
| esk5_0 = esk4_0
| ~ lesseq(esk5_0,max(esk3_0,esk3_0)) ),
inference(spm,[status(thm)],[68,845692,theory(equality)]) ).
cnf(880372,negated_conjecture,
( max(esk3_0,esk3_0) = esk5_0
| esk5_0 = esk4_0
| esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk3_0,esk3_0) ),
inference(spm,[status(thm)],[845743,3981,theory(equality)]) ).
cnf(880411,negated_conjecture,
( max(esk3_0,esk3_0) = esk5_0
| esk5_0 = esk4_0
| esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| $false ),
inference(rw,[status(thm)],[880372,48,theory(equality)]) ).
cnf(880412,negated_conjecture,
( max(esk3_0,esk3_0) = esk5_0
| esk5_0 = esk4_0
| esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0)
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(cn,[status(thm)],[880411,theory(equality)]) ).
cnf(882408,negated_conjecture,
( max(esk3_0,esk3_0) = esk5_0
| esk5_0 = esk4_0
| esk5_0 = esk3_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(csr,[status(thm)],[880412,399162]) ).
cnf(882477,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| ~ lesseq(esk5_0,esk5_0)
| ~ lesseq(esk3_0,esk3_0) ),
inference(spm,[status(thm)],[20063,882408,theory(equality)]) ).
cnf(882822,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| $false
| ~ lesseq(esk3_0,esk3_0) ),
inference(rw,[status(thm)],[882477,48,theory(equality)]) ).
cnf(882823,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0)
| $false
| $false ),
inference(rw,[status(thm)],[882822,48,theory(equality)]) ).
cnf(882824,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(cn,[status(thm)],[882823,theory(equality)]) ).
cnf(883092,negated_conjecture,
( lesseq(esk5_0,X1)
| esk5_0 = esk4_0
| esk5_0 = esk3_0
| ~ lesseq(esk4_0,X1)
| ~ lesseq(esk3_0,X1) ),
inference(spm,[status(thm)],[1574,882824,theory(equality)]) ).
cnf(884425,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| ~ lesseq(esk4_0,esk3_0)
| ~ lesseq(esk3_0,esk3_0) ),
inference(spm,[status(thm)],[4153,883092,theory(equality)]) ).
cnf(884874,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| ~ lesseq(esk4_0,esk3_0)
| $false ),
inference(rw,[status(thm)],[884425,48,theory(equality)]) ).
cnf(884875,negated_conjecture,
( esk5_0 = esk3_0
| esk5_0 = esk4_0
| ~ lesseq(esk4_0,esk3_0) ),
inference(cn,[status(thm)],[884874,theory(equality)]) ).
cnf(885034,negated_conjecture,
( esk5_0 = esk4_0
| esk5_0 = esk3_0
| lesseq(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[884875,44,theory(equality)]) ).
cnf(885074,negated_conjecture,
( esk5_0 = esk4_0
| esk5_0 = esk3_0 ),
inference(csr,[status(thm)],[885034,399162]) ).
cnf(885364,negated_conjecture,
( model_ub(esk3_0,esk4_0,esk4_0)
| esk5_0 = esk3_0 ),
inference(spm,[status(thm)],[41897,885074,theory(equality)]) ).
cnf(885707,negated_conjecture,
( esk5_0 = esk3_0
| ~ lesseq(esk4_0,esk4_0)
| ~ minsol_model_ub(esk3_0,esk4_0,esk4_0) ),
inference(spm,[status(thm)],[223764,885074,theory(equality)]) ).
cnf(886276,negated_conjecture,
( esk5_0 = esk3_0
| $false
| ~ minsol_model_ub(esk3_0,esk4_0,esk4_0) ),
inference(rw,[status(thm)],[885707,48,theory(equality)]) ).
cnf(886277,negated_conjecture,
( esk5_0 = esk3_0
| ~ minsol_model_ub(esk3_0,esk4_0,esk4_0) ),
inference(cn,[status(thm)],[886276,theory(equality)]) ).
cnf(889135,negated_conjecture,
( esk5_0 = esk3_0
| ~ model_ub(esk3_0,esk4_0,esk4_0) ),
inference(spm,[status(thm)],[886277,28254,theory(equality)]) ).
cnf(902258,negated_conjecture,
esk5_0 = esk3_0,
inference(csr,[status(thm)],[889135,885364]) ).
cnf(902268,negated_conjecture,
lesseq(esk4_0,esk3_0),
inference(rw,[status(thm)],[5210,902258,theory(equality)]) ).
cnf(904768,negated_conjecture,
( $false
| ~ minsol_model_ub(esk3_0,esk4_0,esk5_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[163641,902258,theory(equality)]),48,theory(equality)]) ).
cnf(904769,negated_conjecture,
( $false
| ~ minsol_model_ub(esk3_0,esk4_0,esk3_0) ),
inference(rw,[status(thm)],[904768,902258,theory(equality)]) ).
cnf(904770,negated_conjecture,
~ minsol_model_ub(esk3_0,esk4_0,esk3_0),
inference(cn,[status(thm)],[904769,theory(equality)]) ).
cnf(907085,negated_conjecture,
~ model_ub(esk3_0,esk4_0,esk3_0),
inference(spm,[status(thm)],[904770,28339,theory(equality)]) ).
cnf(907638,negated_conjecture,
( ~ lesseq(esk4_0,esk3_0)
| ~ lesseq(esk3_0,esk3_0) ),
inference(spm,[status(thm)],[907085,651,theory(equality)]) ).
cnf(907642,negated_conjecture,
( $false
| ~ lesseq(esk3_0,esk3_0) ),
inference(rw,[status(thm)],[907638,902268,theory(equality)]) ).
cnf(907643,negated_conjecture,
( $false
| $false ),
inference(rw,[status(thm)],[907642,48,theory(equality)]) ).
cnf(907644,negated_conjecture,
$false,
inference(cn,[status(thm)],[907643,theory(equality)]) ).
cnf(907645,negated_conjecture,
$false,
907644,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM859+1 : TPTP v7.0.0. Released v4.1.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n134.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 15:04:34 CST 2018
% 0.02/0.23 % CPUTime :
% 0.02/0.28 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.28 --creating new selector for []
% 20.80/21.22 -running prover on /export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1 with time limit 29
% 20.80/21.22 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox/tmp/tmpdtstOn/sel_theBenchmark.p_1']
% 20.80/21.22 -prover status Theorem
% 20.80/21.22 Problem theBenchmark.p solved in phase 0.
% 20.80/21.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.80/21.22 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.80/21.22 Solved 1 out of 1.
% 20.80/21.22 # Problem is unsatisfiable (or provable), constructing proof object
% 20.80/21.22 # SZS status Theorem
% 20.80/21.22 # SZS output start CNFRefutation.
% See solution above
% 20.80/21.22 # SZS output end CNFRefutation
%------------------------------------------------------------------------------