%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM380+1 : TPTP v7.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n139.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:21:13 EST 2018
% Result : Theorem 99.41s
% Output : CNFRefutation 99.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 3
% Syntax : Number of formulae : 128 ( 18 unt; 0 def)
% Number of atoms : 524 ( 188 equ)
% Maximal formula atoms : 36 ( 4 avg)
% Number of connectives : 646 ( 250 ~; 323 |; 71 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-5 aty)
% Number of variables : 316 ( 36 sgn 63 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(5,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& ! [X3] :
~ ( in(X3,X2)
& ! [X4] :
~ ( in(X4,X2)
& in(X4,X3) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_2',t7_tarski) ).
fof(16,axiom,
! [X1,X2,X3,X4,X5] :
( equal(X5,unordered_quadruple(X1,X2,X3,X4))
<=> ! [X6] :
( in(X6,X5)
<=> ~ ( ~ equal(X6,X1)
& ~ equal(X6,X2)
& ~ equal(X6,X3)
& ~ equal(X6,X4) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_2',d2_enumset1) ).
fof(19,conjecture,
! [X1,X2,X3,X4] :
~ ( in(X1,X2)
& in(X2,X3)
& in(X3,X4)
& in(X4,X1) ),
file('/export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_2',t4_ordinal1) ).
fof(27,negated_conjecture,
~ ! [X1,X2,X3,X4] :
~ ( in(X1,X2)
& in(X2,X3)
& in(X3,X4)
& in(X4,X1) ),
inference(assume_negation,[status(cth)],[19]) ).
fof(45,plain,
! [X1,X2] :
( ~ in(X1,X2)
| ? [X3] :
( in(X3,X2)
& ! [X4] :
( ~ in(X4,X2)
| ~ in(X4,X3) ) ) ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(46,plain,
! [X5,X6] :
( ~ in(X5,X6)
| ? [X7] :
( in(X7,X6)
& ! [X8] :
( ~ in(X8,X6)
| ~ in(X8,X7) ) ) ),
inference(variable_rename,[status(thm)],[45]) ).
fof(47,plain,
! [X5,X6] :
( ~ in(X5,X6)
| ( in(esk4_2(X5,X6),X6)
& ! [X8] :
( ~ in(X8,X6)
| ~ in(X8,esk4_2(X5,X6)) ) ) ),
inference(skolemize,[status(esa)],[46]) ).
fof(48,plain,
! [X5,X6,X8] :
( ( ( ~ in(X8,X6)
| ~ in(X8,esk4_2(X5,X6)) )
& in(esk4_2(X5,X6),X6) )
| ~ in(X5,X6) ),
inference(shift_quantors,[status(thm)],[47]) ).
fof(49,plain,
! [X5,X6,X8] :
( ( ~ in(X8,X6)
| ~ in(X8,esk4_2(X5,X6))
| ~ in(X5,X6) )
& ( in(esk4_2(X5,X6),X6)
| ~ in(X5,X6) ) ),
inference(distribute,[status(thm)],[48]) ).
cnf(50,plain,
( in(esk4_2(X1,X2),X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[49]) ).
cnf(51,plain,
( ~ in(X1,X2)
| ~ in(X3,esk4_2(X1,X2))
| ~ in(X3,X2) ),
inference(split_conjunct,[status(thm)],[49]) ).
fof(91,plain,
! [X1,X2,X3,X4,X5] :
( ( ~ equal(X5,unordered_quadruple(X1,X2,X3,X4))
| ! [X6] :
( ( ~ in(X6,X5)
| equal(X6,X1)
| equal(X6,X2)
| equal(X6,X3)
| equal(X6,X4) )
& ( ( ~ equal(X6,X1)
& ~ equal(X6,X2)
& ~ equal(X6,X3)
& ~ equal(X6,X4) )
| in(X6,X5) ) ) )
& ( ? [X6] :
( ( ~ in(X6,X5)
| ( ~ equal(X6,X1)
& ~ equal(X6,X2)
& ~ equal(X6,X3)
& ~ equal(X6,X4) ) )
& ( in(X6,X5)
| equal(X6,X1)
| equal(X6,X2)
| equal(X6,X3)
| equal(X6,X4) ) )
| equal(X5,unordered_quadruple(X1,X2,X3,X4)) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(92,plain,
! [X7,X8,X9,X10,X11] :
( ( ~ equal(X11,unordered_quadruple(X7,X8,X9,X10))
| ! [X12] :
( ( ~ in(X12,X11)
| equal(X12,X7)
| equal(X12,X8)
| equal(X12,X9)
| equal(X12,X10) )
& ( ( ~ equal(X12,X7)
& ~ equal(X12,X8)
& ~ equal(X12,X9)
& ~ equal(X12,X10) )
| in(X12,X11) ) ) )
& ( ? [X13] :
( ( ~ in(X13,X11)
| ( ~ equal(X13,X7)
& ~ equal(X13,X8)
& ~ equal(X13,X9)
& ~ equal(X13,X10) ) )
& ( in(X13,X11)
| equal(X13,X7)
| equal(X13,X8)
| equal(X13,X9)
| equal(X13,X10) ) )
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) ) ),
inference(variable_rename,[status(thm)],[91]) ).
fof(93,plain,
! [X7,X8,X9,X10,X11] :
( ( ~ equal(X11,unordered_quadruple(X7,X8,X9,X10))
| ! [X12] :
( ( ~ in(X12,X11)
| equal(X12,X7)
| equal(X12,X8)
| equal(X12,X9)
| equal(X12,X10) )
& ( ( ~ equal(X12,X7)
& ~ equal(X12,X8)
& ~ equal(X12,X9)
& ~ equal(X12,X10) )
| in(X12,X11) ) ) )
& ( ( ( ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X7)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X8)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X9)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X10) ) )
& ( in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(esk9_5(X7,X8,X9,X10,X11),X7)
| equal(esk9_5(X7,X8,X9,X10,X11),X8)
| equal(esk9_5(X7,X8,X9,X10,X11),X9)
| equal(esk9_5(X7,X8,X9,X10,X11),X10) ) )
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) ) ),
inference(skolemize,[status(esa)],[92]) ).
fof(94,plain,
! [X7,X8,X9,X10,X11,X12] :
( ( ( ( ~ in(X12,X11)
| equal(X12,X7)
| equal(X12,X8)
| equal(X12,X9)
| equal(X12,X10) )
& ( ( ~ equal(X12,X7)
& ~ equal(X12,X8)
& ~ equal(X12,X9)
& ~ equal(X12,X10) )
| in(X12,X11) ) )
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ( ( ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X7)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X8)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X9)
& ~ equal(esk9_5(X7,X8,X9,X10,X11),X10) ) )
& ( in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(esk9_5(X7,X8,X9,X10,X11),X7)
| equal(esk9_5(X7,X8,X9,X10,X11),X8)
| equal(esk9_5(X7,X8,X9,X10,X11),X9)
| equal(esk9_5(X7,X8,X9,X10,X11),X10) ) )
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) ) ),
inference(shift_quantors,[status(thm)],[93]) ).
fof(95,plain,
! [X7,X8,X9,X10,X11,X12] :
( ( ~ in(X12,X11)
| equal(X12,X7)
| equal(X12,X8)
| equal(X12,X9)
| equal(X12,X10)
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(X12,X7)
| in(X12,X11)
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(X12,X8)
| in(X12,X11)
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(X12,X9)
| in(X12,X11)
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(X12,X10)
| in(X12,X11)
| ~ equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X7)
| ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X8)
| ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X9)
| ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( ~ equal(esk9_5(X7,X8,X9,X10,X11),X10)
| ~ in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) )
& ( in(esk9_5(X7,X8,X9,X10,X11),X11)
| equal(esk9_5(X7,X8,X9,X10,X11),X7)
| equal(esk9_5(X7,X8,X9,X10,X11),X8)
| equal(esk9_5(X7,X8,X9,X10,X11),X9)
| equal(esk9_5(X7,X8,X9,X10,X11),X10)
| equal(X11,unordered_quadruple(X7,X8,X9,X10)) ) ),
inference(distribute,[status(thm)],[94]) ).
cnf(101,plain,
( in(X6,X1)
| X1 != unordered_quadruple(X2,X3,X4,X5)
| X6 != X5 ),
inference(split_conjunct,[status(thm)],[95]) ).
cnf(102,plain,
( in(X6,X1)
| X1 != unordered_quadruple(X2,X3,X4,X5)
| X6 != X4 ),
inference(split_conjunct,[status(thm)],[95]) ).
cnf(103,plain,
( in(X6,X1)
| X1 != unordered_quadruple(X2,X3,X4,X5)
| X6 != X3 ),
inference(split_conjunct,[status(thm)],[95]) ).
cnf(104,plain,
( in(X6,X1)
| X1 != unordered_quadruple(X2,X3,X4,X5)
| X6 != X2 ),
inference(split_conjunct,[status(thm)],[95]) ).
cnf(105,plain,
( X6 = X5
| X6 = X4
| X6 = X3
| X6 = X2
| X1 != unordered_quadruple(X2,X3,X4,X5)
| ~ in(X6,X1) ),
inference(split_conjunct,[status(thm)],[95]) ).
fof(112,negated_conjecture,
? [X1,X2,X3,X4] :
( in(X1,X2)
& in(X2,X3)
& in(X3,X4)
& in(X4,X1) ),
inference(fof_nnf,[status(thm)],[27]) ).
fof(113,negated_conjecture,
? [X5,X6,X7,X8] :
( in(X5,X6)
& in(X6,X7)
& in(X7,X8)
& in(X8,X5) ),
inference(variable_rename,[status(thm)],[112]) ).
fof(114,negated_conjecture,
( in(esk11_0,esk12_0)
& in(esk12_0,esk13_0)
& in(esk13_0,esk14_0)
& in(esk14_0,esk11_0) ),
inference(skolemize,[status(esa)],[113]) ).
cnf(115,negated_conjecture,
in(esk14_0,esk11_0),
inference(split_conjunct,[status(thm)],[114]) ).
cnf(116,negated_conjecture,
in(esk13_0,esk14_0),
inference(split_conjunct,[status(thm)],[114]) ).
cnf(117,negated_conjecture,
in(esk12_0,esk13_0),
inference(split_conjunct,[status(thm)],[114]) ).
cnf(118,negated_conjecture,
in(esk11_0,esk12_0),
inference(split_conjunct,[status(thm)],[114]) ).
cnf(166,plain,
( in(X1,X2)
| unordered_quadruple(X3,X4,X5,X1) != X2 ),
inference(er,[status(thm)],[101,theory(equality)]) ).
cnf(167,plain,
( in(X1,X2)
| unordered_quadruple(X3,X4,X1,X5) != X2 ),
inference(er,[status(thm)],[102,theory(equality)]) ).
cnf(168,plain,
( in(X1,X2)
| unordered_quadruple(X3,X1,X4,X5) != X2 ),
inference(er,[status(thm)],[103,theory(equality)]) ).
cnf(169,plain,
( in(X1,X2)
| unordered_quadruple(X1,X3,X4,X5) != X2 ),
inference(er,[status(thm)],[104,theory(equality)]) ).
cnf(170,plain,
( X1 = X2
| X3 = X2
| X4 = X2
| X5 = X2
| ~ in(X2,unordered_quadruple(X1,X3,X4,X5)) ),
inference(er,[status(thm)],[105,theory(equality)]) ).
cnf(206,plain,
in(X1,unordered_quadruple(X2,X3,X4,X1)),
inference(er,[status(thm)],[166,theory(equality)]) ).
cnf(213,plain,
in(X1,unordered_quadruple(X2,X3,X1,X4)),
inference(er,[status(thm)],[167,theory(equality)]) ).
cnf(221,plain,
in(X1,unordered_quadruple(X2,X1,X3,X4)),
inference(er,[status(thm)],[168,theory(equality)]) ).
cnf(279,plain,
in(X1,unordered_quadruple(X1,X2,X3,X4)),
inference(er,[status(thm)],[169,theory(equality)]) ).
cnf(282,plain,
( X1 = esk4_2(X2,unordered_quadruple(X3,X4,X5,X1))
| X5 = esk4_2(X2,unordered_quadruple(X3,X4,X5,X1))
| X4 = esk4_2(X2,unordered_quadruple(X3,X4,X5,X1))
| X3 = esk4_2(X2,unordered_quadruple(X3,X4,X5,X1))
| ~ in(X2,unordered_quadruple(X3,X4,X5,X1)) ),
inference(spm,[status(thm)],[170,50,theory(equality)]) ).
cnf(1022,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X2
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X3
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X4
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X1 ),
inference(spm,[status(thm)],[282,206,theory(equality)]) ).
cnf(1962,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| ~ in(X2,unordered_quadruple(X3,X4,X5,X2)) ),
inference(spm,[status(thm)],[51,1022,theory(equality)]) ).
cnf(1963,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X5)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| ~ in(X2,unordered_quadruple(X3,X4,X5,X2)) ),
inference(spm,[status(thm)],[51,1022,theory(equality)]) ).
cnf(1964,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X4)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| ~ in(X2,unordered_quadruple(X3,X4,X5,X2)) ),
inference(spm,[status(thm)],[51,1022,theory(equality)]) ).
cnf(1965,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| ~ in(X1,X3)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| ~ in(X2,unordered_quadruple(X3,X4,X5,X2)) ),
inference(spm,[status(thm)],[51,1022,theory(equality)]) ).
cnf(2006,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| $false ),
inference(rw,[status(thm)],[1962,206,theory(equality)]) ).
cnf(2007,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2)) ),
inference(cn,[status(thm)],[2006,theory(equality)]) ).
cnf(2008,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X5)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| $false ),
inference(rw,[status(thm)],[1963,206,theory(equality)]) ).
cnf(2009,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X5)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2)) ),
inference(cn,[status(thm)],[2008,theory(equality)]) ).
cnf(2010,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X4)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| $false ),
inference(rw,[status(thm)],[1964,206,theory(equality)]) ).
cnf(2011,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X3
| ~ in(X1,X4)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2)) ),
inference(cn,[status(thm)],[2010,theory(equality)]) ).
cnf(2012,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| ~ in(X1,X3)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2))
| $false ),
inference(rw,[status(thm)],[1965,206,theory(equality)]) ).
cnf(2013,plain,
( esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X2
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X5
| esk4_2(X2,unordered_quadruple(X3,X4,X5,X2)) = X4
| ~ in(X1,X3)
| ~ in(X1,unordered_quadruple(X3,X4,X5,X2)) ),
inference(cn,[status(thm)],[2012,theory(equality)]) ).
cnf(18632,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X2
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X3
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X4
| ~ in(X4,X1) ),
inference(spm,[status(thm)],[2007,213,theory(equality)]) ).
cnf(18634,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X2
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X3
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X4
| ~ in(X2,X1) ),
inference(spm,[status(thm)],[2007,279,theory(equality)]) ).
cnf(18673,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X2
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X3
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X1
| ~ in(X3,X4) ),
inference(spm,[status(thm)],[2009,221,theory(equality)]) ).
cnf(18684,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X2
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X4
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X1
| ~ in(X1,X3) ),
inference(spm,[status(thm)],[2011,206,theory(equality)]) ).
cnf(18696,plain,
( esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X3
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X4
| esk4_2(X1,unordered_quadruple(X2,X3,X4,X1)) = X1
| ~ in(X4,X2) ),
inference(spm,[status(thm)],[2013,213,theory(equality)]) ).
cnf(798780,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X1,X2,esk11_0,esk12_0)) = esk11_0
| esk4_2(esk12_0,unordered_quadruple(X1,X2,esk11_0,esk12_0)) = X2
| esk4_2(esk12_0,unordered_quadruple(X1,X2,esk11_0,esk12_0)) = X1 ),
inference(spm,[status(thm)],[18632,118,theory(equality)]) ).
cnf(798781,negated_conjecture,
( esk4_2(esk13_0,unordered_quadruple(X1,X2,esk12_0,esk13_0)) = esk12_0
| esk4_2(esk13_0,unordered_quadruple(X1,X2,esk12_0,esk13_0)) = X2
| esk4_2(esk13_0,unordered_quadruple(X1,X2,esk12_0,esk13_0)) = X1 ),
inference(spm,[status(thm)],[18632,117,theory(equality)]) ).
cnf(798798,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X9,X10,esk11_0,esk12_0)) = esk11_0
| esk4_2(esk12_0,unordered_quadruple(X9,X10,esk11_0,esk12_0)) = X10
| X9 != X10 ),
inference(ef,[status(thm)],[798780,theory(equality)]) ).
cnf(799528,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X1,X1,esk11_0,esk12_0)) = esk11_0
| esk4_2(esk12_0,unordered_quadruple(X1,X1,esk11_0,esk12_0)) = X1 ),
inference(er,[status(thm)],[798798,theory(equality)]) ).
cnf(801731,negated_conjecture,
( esk4_2(esk14_0,unordered_quadruple(esk13_0,X1,X2,esk14_0)) = X2
| esk4_2(esk14_0,unordered_quadruple(esk13_0,X1,X2,esk14_0)) = X1
| esk4_2(esk14_0,unordered_quadruple(esk13_0,X1,X2,esk14_0)) = esk13_0 ),
inference(spm,[status(thm)],[18634,116,theory(equality)]) ).
cnf(805984,negated_conjecture,
( esk4_2(X1,unordered_quadruple(X2,esk11_0,esk12_0,X1)) = X1
| esk4_2(X1,unordered_quadruple(X2,esk11_0,esk12_0,X1)) = esk11_0
| esk4_2(X1,unordered_quadruple(X2,esk11_0,esk12_0,X1)) = X2 ),
inference(spm,[status(thm)],[18673,118,theory(equality)]) ).
cnf(811568,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X1,esk13_0,X2,esk12_0)) = esk12_0
| esk4_2(esk12_0,unordered_quadruple(X1,esk13_0,X2,esk12_0)) = X2
| esk4_2(esk12_0,unordered_quadruple(X1,esk13_0,X2,esk12_0)) = X1 ),
inference(spm,[status(thm)],[18684,117,theory(equality)]) ).
cnf(811570,negated_conjecture,
( esk4_2(esk14_0,unordered_quadruple(X1,esk11_0,X2,esk14_0)) = esk14_0
| esk4_2(esk14_0,unordered_quadruple(X1,esk11_0,X2,esk14_0)) = X2
| esk4_2(esk14_0,unordered_quadruple(X1,esk11_0,X2,esk14_0)) = X1 ),
inference(spm,[status(thm)],[18684,115,theory(equality)]) ).
cnf(814889,negated_conjecture,
( esk4_2(X1,unordered_quadruple(esk13_0,X2,esk12_0,X1)) = X1
| esk4_2(X1,unordered_quadruple(esk13_0,X2,esk12_0,X1)) = esk12_0
| esk4_2(X1,unordered_quadruple(esk13_0,X2,esk12_0,X1)) = X2 ),
inference(spm,[status(thm)],[18696,117,theory(equality)]) ).
cnf(851131,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = X2
| esk11_0 != X2 ),
inference(ef,[status(thm)],[799528,theory(equality)]) ).
cnf(851132,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X3,X3,esk11_0,esk12_0)) = esk11_0
| X3 != esk11_0 ),
inference(ef,[status(thm)],[799528,theory(equality)]) ).
cnf(851135,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = X2
| ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(spm,[status(thm)],[51,799528,theory(equality)]) ).
cnf(851136,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = esk11_0
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(spm,[status(thm)],[51,799528,theory(equality)]) ).
cnf(851629,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = X2
| ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false ),
inference(rw,[status(thm)],[851135,206,theory(equality)]) ).
cnf(851630,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = X2
| ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(cn,[status(thm)],[851629,theory(equality)]) ).
cnf(851631,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = esk11_0
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false ),
inference(rw,[status(thm)],[851136,206,theory(equality)]) ).
cnf(851632,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0)) = esk11_0
| ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(cn,[status(thm)],[851631,theory(equality)]) ).
cnf(852611,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| esk11_0 != X2 ),
inference(spm,[status(thm)],[51,851131,theory(equality)]) ).
cnf(852863,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false
| esk11_0 != X2 ),
inference(rw,[status(thm)],[852611,206,theory(equality)]) ).
cnf(852864,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| esk11_0 != X2 ),
inference(cn,[status(thm)],[852863,theory(equality)]) ).
cnf(854153,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| X2 != esk11_0 ),
inference(spm,[status(thm)],[51,851132,theory(equality)]) ).
cnf(854407,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false
| X2 != esk11_0 ),
inference(rw,[status(thm)],[854153,206,theory(equality)]) ).
cnf(854408,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| X2 != esk11_0 ),
inference(cn,[status(thm)],[854407,theory(equality)]) ).
cnf(854915,negated_conjecture,
( esk11_0 != X1
| ~ in(esk12_0,X1) ),
inference(spm,[status(thm)],[852864,206,theory(equality)]) ).
cnf(854916,negated_conjecture,
( esk11_0 != X1
| ~ in(esk11_0,X1) ),
inference(spm,[status(thm)],[852864,213,theory(equality)]) ).
cnf(854923,negated_conjecture,
esk11_0 != esk13_0,
inference(spm,[status(thm)],[854915,117,theory(equality)]) ).
cnf(854928,negated_conjecture,
esk11_0 != esk12_0,
inference(spm,[status(thm)],[854916,118,theory(equality)]) ).
cnf(857710,negated_conjecture,
( X1 != esk11_0
| ~ in(X1,esk11_0) ),
inference(spm,[status(thm)],[854408,221,theory(equality)]) ).
cnf(857716,negated_conjecture,
esk14_0 != esk11_0,
inference(spm,[status(thm)],[857710,115,theory(equality)]) ).
cnf(898788,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X1,X1,esk11_0,esk12_0)) = X1
| ~ in(X1,esk11_0) ),
inference(spm,[status(thm)],[851630,221,theory(equality)]) ).
cnf(898811,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(X2,esk11_0) ),
inference(spm,[status(thm)],[51,898788,theory(equality)]) ).
cnf(899089,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false
| ~ in(X2,esk11_0) ),
inference(rw,[status(thm)],[898811,206,theory(equality)]) ).
cnf(899090,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(X2,esk11_0) ),
inference(cn,[status(thm)],[899089,theory(equality)]) ).
cnf(900059,negated_conjecture,
( ~ in(X2,esk11_0)
| ~ in(esk4_2(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)),X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(spm,[status(thm)],[899090,50,theory(equality)]) ).
cnf(903498,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(X1,X1,esk11_0,esk12_0)) = esk11_0
| ~ in(esk12_0,X1) ),
inference(spm,[status(thm)],[851632,206,theory(equality)]) ).
cnf(903508,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,X2) ),
inference(spm,[status(thm)],[51,903498,theory(equality)]) ).
cnf(903771,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| $false
| ~ in(esk12_0,X2) ),
inference(rw,[status(thm)],[903508,206,theory(equality)]) ).
cnf(903772,negated_conjecture,
( ~ in(X1,esk11_0)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0))
| ~ in(esk12_0,X2) ),
inference(cn,[status(thm)],[903771,theory(equality)]) ).
cnf(906742,negated_conjecture,
( ~ in(esk4_2(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)),esk11_0)
| ~ in(esk12_0,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk11_0,esk12_0)) ),
inference(spm,[status(thm)],[903772,50,theory(equality)]) ).
cnf(955442,negated_conjecture,
( esk4_2(esk13_0,unordered_quadruple(X9,X10,esk12_0,esk13_0)) = esk12_0
| esk4_2(esk13_0,unordered_quadruple(X9,X10,esk12_0,esk13_0)) = X10
| X9 != X10 ),
inference(ef,[status(thm)],[798781,theory(equality)]) ).
cnf(956193,negated_conjecture,
( esk4_2(esk13_0,unordered_quadruple(X1,X1,esk12_0,esk13_0)) = esk12_0
| esk4_2(esk13_0,unordered_quadruple(X1,X1,esk12_0,esk13_0)) = X1 ),
inference(er,[status(thm)],[955442,theory(equality)]) ).
cnf(1070570,negated_conjecture,
( esk14_0 = esk13_0
| esk14_0 = esk11_0
| esk14_0 = esk12_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk13_0 ),
inference(spm,[status(thm)],[801731,805984,theory(equality)]) ).
cnf(1072087,negated_conjecture,
( esk14_0 = esk13_0
| esk14_0 = esk12_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk13_0 ),
inference(sr,[status(thm)],[1070570,857716,theory(equality)]) ).
cnf(1109615,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk12_0
| esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk13_0,esk11_0)
| ~ in(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0))
| ~ in(esk12_0,esk13_0) ),
inference(spm,[status(thm)],[906742,811568,theory(equality)]) ).
cnf(1111130,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk12_0
| esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk13_0,esk11_0)
| $false
| ~ in(esk12_0,esk13_0) ),
inference(rw,[status(thm)],[1109615,206,theory(equality)]) ).
cnf(1111131,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk12_0
| esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk13_0,esk11_0)
| $false
| $false ),
inference(rw,[status(thm)],[1111130,117,theory(equality)]) ).
cnf(1111132,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk12_0
| esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk13_0,esk11_0) ),
inference(cn,[status(thm)],[1111131,theory(equality)]) ).
cnf(1113193,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk12_0,esk13_0)
| ~ in(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0))
| ~ in(esk13_0,esk11_0) ),
inference(spm,[status(thm)],[900059,1111132,theory(equality)]) ).
cnf(1113706,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| $false
| ~ in(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0))
| ~ in(esk13_0,esk11_0) ),
inference(rw,[status(thm)],[1113193,117,theory(equality)]) ).
cnf(1113707,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| $false
| $false
| ~ in(esk13_0,esk11_0) ),
inference(rw,[status(thm)],[1113706,206,theory(equality)]) ).
cnf(1113708,negated_conjecture,
( esk4_2(esk12_0,unordered_quadruple(esk13_0,esk13_0,esk11_0,esk12_0)) = esk11_0
| ~ in(esk13_0,esk11_0) ),
inference(cn,[status(thm)],[1113707,theory(equality)]) ).
cnf(1113965,negated_conjecture,
( esk11_0 = esk13_0
| ~ in(esk13_0,esk11_0) ),
inference(spm,[status(thm)],[898788,1113708,theory(equality)]) ).
cnf(1114472,negated_conjecture,
~ in(esk13_0,esk11_0),
inference(sr,[status(thm)],[1113965,854923,theory(equality)]) ).
cnf(1191066,negated_conjecture,
( esk4_2(esk13_0,unordered_quadruple(X2,X2,esk12_0,esk13_0)) = X2
| esk12_0 != X2 ),
inference(ef,[status(thm)],[956193,theory(equality)]) ).
cnf(1192569,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk12_0,esk13_0))
| ~ in(esk13_0,unordered_quadruple(X2,X2,esk12_0,esk13_0))
| esk12_0 != X2 ),
inference(spm,[status(thm)],[51,1191066,theory(equality)]) ).
cnf(1192824,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk12_0,esk13_0))
| $false
| esk12_0 != X2 ),
inference(rw,[status(thm)],[1192569,206,theory(equality)]) ).
cnf(1192825,negated_conjecture,
( ~ in(X1,X2)
| ~ in(X1,unordered_quadruple(X2,X2,esk12_0,esk13_0))
| esk12_0 != X2 ),
inference(cn,[status(thm)],[1192824,theory(equality)]) ).
cnf(1194114,negated_conjecture,
( esk12_0 != X1
| ~ in(esk13_0,X1) ),
inference(spm,[status(thm)],[1192825,206,theory(equality)]) ).
cnf(1194115,negated_conjecture,
( esk12_0 != X1
| ~ in(esk12_0,X1) ),
inference(spm,[status(thm)],[1192825,213,theory(equality)]) ).
cnf(1194122,negated_conjecture,
esk12_0 != esk14_0,
inference(spm,[status(thm)],[1194114,116,theory(equality)]) ).
cnf(1194127,negated_conjecture,
esk12_0 != esk13_0,
inference(spm,[status(thm)],[1194115,117,theory(equality)]) ).
cnf(1812411,negated_conjecture,
( esk14_0 = esk13_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk13_0 ),
inference(sr,[status(thm)],[1072087,1194122,theory(equality)]) ).
cnf(1812659,negated_conjecture,
( esk13_0 = esk12_0
| esk13_0 = esk11_0
| esk13_0 = esk14_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0 ),
inference(spm,[status(thm)],[814889,1812411,theory(equality)]) ).
cnf(1813186,negated_conjecture,
( esk13_0 = esk11_0
| esk14_0 = esk13_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0 ),
inference(sr,[status(thm)],[1812659,1194127,theory(equality)]) ).
cnf(1813187,negated_conjecture,
( esk14_0 = esk13_0
| esk4_2(esk14_0,unordered_quadruple(esk13_0,esk11_0,esk12_0,esk14_0)) = esk11_0 ),
inference(sr,[status(thm)],[1813186,854923,theory(equality)]) ).
cnf(1813495,negated_conjecture,
( esk11_0 = esk14_0
| esk11_0 = esk13_0
| esk11_0 = esk12_0
| esk14_0 = esk13_0 ),
inference(spm,[status(thm)],[811570,1813187,theory(equality)]) ).
cnf(1814025,negated_conjecture,
( esk13_0 = esk11_0
| esk12_0 = esk11_0
| esk14_0 = esk13_0 ),
inference(sr,[status(thm)],[1813495,857716,theory(equality)]) ).
cnf(1814026,negated_conjecture,
( esk12_0 = esk11_0
| esk14_0 = esk13_0 ),
inference(sr,[status(thm)],[1814025,854923,theory(equality)]) ).
cnf(1814027,negated_conjecture,
esk14_0 = esk13_0,
inference(sr,[status(thm)],[1814026,854928,theory(equality)]) ).
cnf(1814086,negated_conjecture,
in(esk13_0,esk11_0),
inference(rw,[status(thm)],[115,1814027,theory(equality)]) ).
cnf(1814087,negated_conjecture,
$false,
inference(sr,[status(thm)],[1814086,1114472,theory(equality)]) ).
cnf(1814088,negated_conjecture,
$false,
1814087,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM380+1 : TPTP v7.0.0. Released v3.2.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.24 % Computer : n139.star.cs.uiowa.edu
% 0.02/0.24 % Model : x86_64 x86_64
% 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.24 % Memory : 32218.625MB
% 0.02/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.24 % CPULimit : 300
% 0.02/0.24 % DateTime : Fri Jan 5 03:50:15 CST 2018
% 0.02/0.24 % CPUTime :
% 0.02/0.29 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 --creating new selector for []
% 29.08/29.41 eprover: CPU time limit exceeded, terminating
% 99.41/100.59 -running prover on /export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_1 with time limit 29
% 99.41/100.59 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_1']
% 99.41/100.59 -prover status ResourceOut
% 99.41/100.59 -running prover on /export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_2 with time limit 81
% 99.41/100.59 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=81', '/export/starexec/sandbox2/tmp/tmpbhBQqI/sel_theBenchmark.p_2']
% 99.41/100.59 -prover status Theorem
% 99.41/100.59 Problem theBenchmark.p solved in phase 1.
% 99.41/100.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 99.41/100.59 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 99.41/100.59 Solved 1 out of 1.
% 99.41/100.59 # Problem is unsatisfiable (or provable), constructing proof object
% 99.41/100.59 # SZS status Theorem
% 99.41/100.59 # SZS output start CNFRefutation.
% See solution above
% 99.41/100.61 # SZS output end CNFRefutation
%------------------------------------------------------------------------------