%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM473+1 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n121.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:28 EST 2018
% Result : Theorem 1.61s
% Output : CNFRefutation 1.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 24
% Syntax : Number of formulae : 248 ( 35 unt; 0 def)
% Number of atoms : 1070 ( 244 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 1381 ( 559 ~; 705 |; 92 &)
% ( 4 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 312 ( 1 sgn 143 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( doDivides0(X1,X2)
& doDivides0(X2,X3) )
=> doDivides0(X1,X3) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mDivTrans) ).
fof(7,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( doDivides0(X1,X2)
<=> ? [X3] :
( aNaturalNumber0(X3)
& equal(X2,sdtasdt0(X1,X3)) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mDefDiv) ).
fof(9,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
| ( ~ equal(X2,X1)
& sdtlseqdt0(X2,X1) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mLETotal) ).
fof(10,axiom,
~ equal(xl,sz00),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1347) ).
fof(12,axiom,
sdtlseqdt0(xm,sdtpldt0(xm,xn)),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1409) ).
fof(16,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( ~ equal(X1,sz00)
& ~ equal(X2,X3)
& sdtlseqdt0(X2,X3) )
=> ( ~ equal(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& ~ equal(sdtasdt0(X2,X1),sdtasdt0(X3,X1))
& sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mMonMul) ).
fof(17,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
<=> ? [X3] :
( aNaturalNumber0(X3)
& equal(sdtpldt0(X1,X3),X2) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mDefLE) ).
fof(19,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> equal(X1,X2) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mLEAsym) ).
fof(20,axiom,
equal(xp,sdtsldt0(xm,xl)),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1360) ).
fof(21,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( ~ equal(X1,sz00)
& doDivides0(X1,X2) )
=> ! [X3] :
( equal(X3,sdtsldt0(X2,X1))
<=> ( aNaturalNumber0(X3)
& equal(X2,sdtasdt0(X1,X3)) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mDefQuot) ).
fof(22,axiom,
( doDivides0(xl,xm)
& doDivides0(xl,sdtpldt0(xm,xn)) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1324_04) ).
fof(24,axiom,
( aNaturalNumber0(xl)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1324) ).
fof(26,axiom,
( aNaturalNumber0(sz10)
& ~ equal(sz10,sz00) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mSortsC_01) ).
fof(27,axiom,
equal(xq,sdtsldt0(sdtpldt0(xm,xn),xl)),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__1379) ).
fof(28,conjecture,
sdtlseqdt0(xp,xq),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m__) ).
fof(29,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> equal(sdtasdt0(sdtasdt0(X1,X2),X3),sdtasdt0(X1,sdtasdt0(X2,X3))) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mMulAsso) ).
fof(31,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mLERefl) ).
fof(32,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
=> ! [X3] :
( equal(X3,sdtmndt0(X2,X1))
<=> ( aNaturalNumber0(X3)
& equal(sdtpldt0(X1,X3),X2) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mDefDiff) ).
fof(33,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> aNaturalNumber0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mSortsB_02) ).
fof(34,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mSortsC) ).
fof(35,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> aNaturalNumber0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mSortsB) ).
fof(36,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( equal(sdtpldt0(X1,X2),sdtpldt0(X1,X3))
| equal(sdtpldt0(X2,X1),sdtpldt0(X3,X1)) )
=> equal(X2,X3) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',mAddCanc) ).
fof(39,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( equal(sdtpldt0(X1,sz00),X1)
& equal(X1,sdtpldt0(sz00,X1)) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m_AddZero) ).
fof(40,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
file('/export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1',m_MulUnit) ).
fof(41,negated_conjecture,
~ sdtlseqdt0(xp,xq),
inference(assume_negation,[status(cth)],[28]) ).
fof(42,negated_conjecture,
~ sdtlseqdt0(xp,xq),
inference(fof_simplification,[status(thm)],[41,theory(equality)]) ).
fof(48,plain,
! [X1,X2,X3] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X2,X3)
| doDivides0(X1,X3) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(49,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| ~ doDivides0(X4,X5)
| ~ doDivides0(X5,X6)
| doDivides0(X4,X6) ),
inference(variable_rename,[status(thm)],[48]) ).
cnf(50,plain,
( doDivides0(X1,X2)
| ~ doDivides0(X3,X2)
| ~ doDivides0(X1,X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[49]) ).
fof(68,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ( ( ~ doDivides0(X1,X2)
| ? [X3] :
( aNaturalNumber0(X3)
& equal(X2,sdtasdt0(X1,X3)) ) )
& ( ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ equal(X2,sdtasdt0(X1,X3)) )
| doDivides0(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(69,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ( ( ~ doDivides0(X4,X5)
| ? [X6] :
( aNaturalNumber0(X6)
& equal(X5,sdtasdt0(X4,X6)) ) )
& ( ! [X7] :
( ~ aNaturalNumber0(X7)
| ~ equal(X5,sdtasdt0(X4,X7)) )
| doDivides0(X4,X5) ) ) ),
inference(variable_rename,[status(thm)],[68]) ).
fof(70,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ( ( ~ doDivides0(X4,X5)
| ( aNaturalNumber0(esk1_2(X4,X5))
& equal(X5,sdtasdt0(X4,esk1_2(X4,X5))) ) )
& ( ! [X7] :
( ~ aNaturalNumber0(X7)
| ~ equal(X5,sdtasdt0(X4,X7)) )
| doDivides0(X4,X5) ) ) ),
inference(skolemize,[status(esa)],[69]) ).
fof(71,plain,
! [X4,X5,X7] :
( ( ( ~ aNaturalNumber0(X7)
| ~ equal(X5,sdtasdt0(X4,X7))
| doDivides0(X4,X5) )
& ( ~ doDivides0(X4,X5)
| ( aNaturalNumber0(esk1_2(X4,X5))
& equal(X5,sdtasdt0(X4,esk1_2(X4,X5))) ) ) )
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ),
inference(shift_quantors,[status(thm)],[70]) ).
fof(72,plain,
! [X4,X5,X7] :
( ( ~ aNaturalNumber0(X7)
| ~ equal(X5,sdtasdt0(X4,X7))
| doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( aNaturalNumber0(esk1_2(X4,X5))
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( equal(X5,sdtasdt0(X4,esk1_2(X4,X5)))
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ) ),
inference(distribute,[status(thm)],[71]) ).
cnf(75,plain,
( doDivides0(X2,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| X1 != sdtasdt0(X2,X3)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[72]) ).
fof(79,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X1,X2)
| ( ~ equal(X2,X1)
& sdtlseqdt0(X2,X1) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(80,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| sdtlseqdt0(X3,X4)
| ( ~ equal(X4,X3)
& sdtlseqdt0(X4,X3) ) ),
inference(variable_rename,[status(thm)],[79]) ).
fof(81,plain,
! [X3,X4] :
( ( ~ equal(X4,X3)
| sdtlseqdt0(X3,X4)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4) )
& ( sdtlseqdt0(X4,X3)
| sdtlseqdt0(X3,X4)
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4) ) ),
inference(distribute,[status(thm)],[80]) ).
cnf(82,plain,
( sdtlseqdt0(X2,X1)
| sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[81]) ).
cnf(84,plain,
xl != sz00,
inference(split_conjunct,[status(thm)],[10]) ).
cnf(88,plain,
sdtlseqdt0(xm,sdtpldt0(xm,xn)),
inference(split_conjunct,[status(thm)],[12]) ).
fof(103,plain,
! [X1,X2,X3] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| equal(X1,sz00)
| equal(X2,X3)
| ~ sdtlseqdt0(X2,X3)
| ( ~ equal(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& ~ equal(sdtasdt0(X2,X1),sdtasdt0(X3,X1))
& sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(104,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| equal(X4,sz00)
| equal(X5,X6)
| ~ sdtlseqdt0(X5,X6)
| ( ~ equal(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
& sdtlseqdt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
& ~ equal(sdtasdt0(X5,X4),sdtasdt0(X6,X4))
& sdtlseqdt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4)) ) ),
inference(variable_rename,[status(thm)],[103]) ).
fof(105,plain,
! [X4,X5,X6] :
( ( ~ equal(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
| equal(X4,sz00)
| equal(X5,X6)
| ~ sdtlseqdt0(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) )
& ( sdtlseqdt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
| equal(X4,sz00)
| equal(X5,X6)
| ~ sdtlseqdt0(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) )
& ( ~ equal(sdtasdt0(X5,X4),sdtasdt0(X6,X4))
| equal(X4,sz00)
| equal(X5,X6)
| ~ sdtlseqdt0(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) )
& ( sdtlseqdt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4))
| equal(X4,sz00)
| equal(X5,X6)
| ~ sdtlseqdt0(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) ) ),
inference(distribute,[status(thm)],[104]) ).
cnf(108,plain,
( X2 = X1
| X3 = sz00
| sdtlseqdt0(sdtasdt0(X3,X2),sdtasdt0(X3,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[105]) ).
fof(110,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ( ( ~ sdtlseqdt0(X1,X2)
| ? [X3] :
( aNaturalNumber0(X3)
& equal(sdtpldt0(X1,X3),X2) ) )
& ( ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(X1,X3),X2) )
| sdtlseqdt0(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(111,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ( ( ~ sdtlseqdt0(X4,X5)
| ? [X6] :
( aNaturalNumber0(X6)
& equal(sdtpldt0(X4,X6),X5) ) )
& ( ! [X7] :
( ~ aNaturalNumber0(X7)
| ~ equal(sdtpldt0(X4,X7),X5) )
| sdtlseqdt0(X4,X5) ) ) ),
inference(variable_rename,[status(thm)],[110]) ).
fof(112,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ( ( ~ sdtlseqdt0(X4,X5)
| ( aNaturalNumber0(esk2_2(X4,X5))
& equal(sdtpldt0(X4,esk2_2(X4,X5)),X5) ) )
& ( ! [X7] :
( ~ aNaturalNumber0(X7)
| ~ equal(sdtpldt0(X4,X7),X5) )
| sdtlseqdt0(X4,X5) ) ) ),
inference(skolemize,[status(esa)],[111]) ).
fof(113,plain,
! [X4,X5,X7] :
( ( ( ~ aNaturalNumber0(X7)
| ~ equal(sdtpldt0(X4,X7),X5)
| sdtlseqdt0(X4,X5) )
& ( ~ sdtlseqdt0(X4,X5)
| ( aNaturalNumber0(esk2_2(X4,X5))
& equal(sdtpldt0(X4,esk2_2(X4,X5)),X5) ) ) )
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ),
inference(shift_quantors,[status(thm)],[112]) ).
fof(114,plain,
! [X4,X5,X7] :
( ( ~ aNaturalNumber0(X7)
| ~ equal(sdtpldt0(X4,X7),X5)
| sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( aNaturalNumber0(esk2_2(X4,X5))
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( equal(sdtpldt0(X4,esk2_2(X4,X5)),X5)
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ) ),
inference(distribute,[status(thm)],[113]) ).
cnf(117,plain,
( sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X2,X3) != X1
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[114]) ).
fof(121,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1)
| equal(X1,X2) ),
inference(fof_nnf,[status(thm)],[19]) ).
fof(122,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| ~ sdtlseqdt0(X3,X4)
| ~ sdtlseqdt0(X4,X3)
| equal(X3,X4) ),
inference(variable_rename,[status(thm)],[121]) ).
cnf(123,plain,
( X1 = X2
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[122]) ).
cnf(124,plain,
xp = sdtsldt0(xm,xl),
inference(split_conjunct,[status(thm)],[20]) ).
fof(125,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| equal(X1,sz00)
| ~ doDivides0(X1,X2)
| ! [X3] :
( ( ~ equal(X3,sdtsldt0(X2,X1))
| ( aNaturalNumber0(X3)
& equal(X2,sdtasdt0(X1,X3)) ) )
& ( ~ aNaturalNumber0(X3)
| ~ equal(X2,sdtasdt0(X1,X3))
| equal(X3,sdtsldt0(X2,X1)) ) ) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(126,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ! [X6] :
( ( ~ equal(X6,sdtsldt0(X5,X4))
| ( aNaturalNumber0(X6)
& equal(X5,sdtasdt0(X4,X6)) ) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(X5,sdtasdt0(X4,X6))
| equal(X6,sdtsldt0(X5,X4)) ) ) ),
inference(variable_rename,[status(thm)],[125]) ).
fof(127,plain,
! [X4,X5,X6] :
( ( ( ~ equal(X6,sdtsldt0(X5,X4))
| ( aNaturalNumber0(X6)
& equal(X5,sdtasdt0(X4,X6)) ) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(X5,sdtasdt0(X4,X6))
| equal(X6,sdtsldt0(X5,X4)) ) )
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ),
inference(shift_quantors,[status(thm)],[126]) ).
fof(128,plain,
! [X4,X5,X6] :
( ( aNaturalNumber0(X6)
| ~ equal(X6,sdtsldt0(X5,X4))
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( equal(X5,sdtasdt0(X4,X6))
| ~ equal(X6,sdtsldt0(X5,X4))
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(X5,sdtasdt0(X4,X6))
| equal(X6,sdtsldt0(X5,X4))
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ) ),
inference(distribute,[status(thm)],[127]) ).
cnf(129,plain,
( X2 = sz00
| X3 = sdtsldt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X1)
| X1 != sdtasdt0(X2,X3)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[128]) ).
cnf(130,plain,
( X2 = sz00
| X1 = sdtasdt0(X2,X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X1)
| X3 != sdtsldt0(X1,X2) ),
inference(split_conjunct,[status(thm)],[128]) ).
cnf(131,plain,
( X2 = sz00
| aNaturalNumber0(X3)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X1)
| X3 != sdtsldt0(X1,X2) ),
inference(split_conjunct,[status(thm)],[128]) ).
cnf(132,plain,
doDivides0(xl,sdtpldt0(xm,xn)),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(133,plain,
doDivides0(xl,xm),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(139,plain,
aNaturalNumber0(xn),
inference(split_conjunct,[status(thm)],[24]) ).
cnf(140,plain,
aNaturalNumber0(xm),
inference(split_conjunct,[status(thm)],[24]) ).
cnf(141,plain,
aNaturalNumber0(xl),
inference(split_conjunct,[status(thm)],[24]) ).
cnf(145,plain,
sz10 != sz00,
inference(split_conjunct,[status(thm)],[26]) ).
cnf(146,plain,
aNaturalNumber0(sz10),
inference(split_conjunct,[status(thm)],[26]) ).
cnf(147,plain,
xq = sdtsldt0(sdtpldt0(xm,xn),xl),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(148,negated_conjecture,
~ sdtlseqdt0(xp,xq),
inference(split_conjunct,[status(thm)],[42]) ).
fof(149,plain,
! [X1,X2,X3] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| equal(sdtasdt0(sdtasdt0(X1,X2),X3),sdtasdt0(X1,sdtasdt0(X2,X3))) ),
inference(fof_nnf,[status(thm)],[29]) ).
fof(150,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| equal(sdtasdt0(sdtasdt0(X4,X5),X6),sdtasdt0(X4,sdtasdt0(X5,X6))) ),
inference(variable_rename,[status(thm)],[149]) ).
cnf(151,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[150]) ).
fof(157,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| sdtlseqdt0(X1,X1) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(158,plain,
! [X2] :
( ~ aNaturalNumber0(X2)
| sdtlseqdt0(X2,X2) ),
inference(variable_rename,[status(thm)],[157]) ).
cnf(159,plain,
( sdtlseqdt0(X1,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[158]) ).
fof(160,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X1,X2)
| ! [X3] :
( ( ~ equal(X3,sdtmndt0(X2,X1))
| ( aNaturalNumber0(X3)
& equal(sdtpldt0(X1,X3),X2) ) )
& ( ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(X1,X3),X2)
| equal(X3,sdtmndt0(X2,X1)) ) ) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(161,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ sdtlseqdt0(X4,X5)
| ! [X6] :
( ( ~ equal(X6,sdtmndt0(X5,X4))
| ( aNaturalNumber0(X6)
& equal(sdtpldt0(X4,X6),X5) ) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(sdtpldt0(X4,X6),X5)
| equal(X6,sdtmndt0(X5,X4)) ) ) ),
inference(variable_rename,[status(thm)],[160]) ).
fof(162,plain,
! [X4,X5,X6] :
( ( ( ~ equal(X6,sdtmndt0(X5,X4))
| ( aNaturalNumber0(X6)
& equal(sdtpldt0(X4,X6),X5) ) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(sdtpldt0(X4,X6),X5)
| equal(X6,sdtmndt0(X5,X4)) ) )
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ),
inference(shift_quantors,[status(thm)],[161]) ).
fof(163,plain,
! [X4,X5,X6] :
( ( aNaturalNumber0(X6)
| ~ equal(X6,sdtmndt0(X5,X4))
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( equal(sdtpldt0(X4,X6),X5)
| ~ equal(X6,sdtmndt0(X5,X4))
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) )
& ( ~ aNaturalNumber0(X6)
| ~ equal(sdtpldt0(X4,X6),X5)
| equal(X6,sdtmndt0(X5,X4))
| ~ sdtlseqdt0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ) ),
inference(distribute,[status(thm)],[162]) ).
cnf(164,plain,
( X3 = sdtmndt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X2,X1)
| sdtpldt0(X2,X3) != X1
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[163]) ).
cnf(165,plain,
( sdtpldt0(X2,X3) = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X2,X1)
| X3 != sdtmndt0(X1,X2) ),
inference(split_conjunct,[status(thm)],[163]) ).
fof(167,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtasdt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(168,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| aNaturalNumber0(sdtasdt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[167]) ).
cnf(169,plain,
( aNaturalNumber0(sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(170,plain,
aNaturalNumber0(sz00),
inference(split_conjunct,[status(thm)],[34]) ).
fof(171,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtpldt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(172,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| aNaturalNumber0(sdtpldt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[171]) ).
cnf(173,plain,
( aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[172]) ).
fof(174,plain,
! [X1,X2,X3] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ( ~ equal(sdtpldt0(X1,X2),sdtpldt0(X1,X3))
& ~ equal(sdtpldt0(X2,X1),sdtpldt0(X3,X1)) )
| equal(X2,X3) ),
inference(fof_nnf,[status(thm)],[36]) ).
fof(175,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| ( ~ equal(sdtpldt0(X4,X5),sdtpldt0(X4,X6))
& ~ equal(sdtpldt0(X5,X4),sdtpldt0(X6,X4)) )
| equal(X5,X6) ),
inference(variable_rename,[status(thm)],[174]) ).
fof(176,plain,
! [X4,X5,X6] :
( ( ~ equal(sdtpldt0(X4,X5),sdtpldt0(X4,X6))
| equal(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) )
& ( ~ equal(sdtpldt0(X5,X4),sdtpldt0(X6,X4))
| equal(X5,X6)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6) ) ),
inference(distribute,[status(thm)],[175]) ).
cnf(178,plain,
( X2 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| sdtpldt0(X3,X2) != sdtpldt0(X3,X1) ),
inference(split_conjunct,[status(thm)],[176]) ).
fof(185,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| ( equal(sdtpldt0(X1,sz00),X1)
& equal(X1,sdtpldt0(sz00,X1)) ) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(186,plain,
! [X2] :
( ~ aNaturalNumber0(X2)
| ( equal(sdtpldt0(X2,sz00),X2)
& equal(X2,sdtpldt0(sz00,X2)) ) ),
inference(variable_rename,[status(thm)],[185]) ).
fof(187,plain,
! [X2] :
( ( equal(sdtpldt0(X2,sz00),X2)
| ~ aNaturalNumber0(X2) )
& ( equal(X2,sdtpldt0(sz00,X2))
| ~ aNaturalNumber0(X2) ) ),
inference(distribute,[status(thm)],[186]) ).
cnf(189,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[187]) ).
fof(190,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
inference(fof_nnf,[status(thm)],[40]) ).
fof(191,plain,
! [X2] :
( ~ aNaturalNumber0(X2)
| ( equal(sdtasdt0(X2,sz10),X2)
& equal(X2,sdtasdt0(sz10,X2)) ) ),
inference(variable_rename,[status(thm)],[190]) ).
fof(192,plain,
! [X2] :
( ( equal(sdtasdt0(X2,sz10),X2)
| ~ aNaturalNumber0(X2) )
& ( equal(X2,sdtasdt0(sz10,X2))
| ~ aNaturalNumber0(X2) ) ),
inference(distribute,[status(thm)],[191]) ).
cnf(193,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[192]) ).
cnf(252,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(spm,[status(thm)],[123,88,theory(equality)]) ).
cnf(254,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| $false
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[252,140,theory(equality)]) ).
cnf(255,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(cn,[status(thm)],[254,theory(equality)]) ).
cnf(306,plain,
( doDivides0(sz10,X1)
| X2 != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X1) ),
inference(spm,[status(thm)],[75,193,theory(equality)]) ).
cnf(316,plain,
( doDivides0(sz10,X1)
| X2 != X1
| ~ aNaturalNumber0(X2)
| $false
| ~ aNaturalNumber0(X1) ),
inference(rw,[status(thm)],[306,146,theory(equality)]) ).
cnf(317,plain,
( doDivides0(sz10,X1)
| X2 != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[316,theory(equality)]) ).
cnf(318,plain,
( doDivides0(sz10,X1)
| ~ aNaturalNumber0(X1) ),
inference(er,[status(thm)],[317,theory(equality)]) ).
cnf(360,plain,
( sz00 = X1
| X2 != sdtpldt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sz00) ),
inference(spm,[status(thm)],[178,189,theory(equality)]) ).
cnf(370,plain,
( sz00 = X1
| X2 != sdtpldt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| $false ),
inference(rw,[status(thm)],[360,170,theory(equality)]) ).
cnf(371,plain,
( sz00 = X1
| X2 != sdtpldt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[370,theory(equality)]) ).
cnf(378,plain,
( doDivides0(X1,xm)
| ~ doDivides0(X1,xl)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X1) ),
inference(spm,[status(thm)],[50,133,theory(equality)]) ).
cnf(380,plain,
( doDivides0(X1,xm)
| ~ doDivides0(X1,xl)
| $false
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X1) ),
inference(rw,[status(thm)],[378,141,theory(equality)]) ).
cnf(381,plain,
( doDivides0(X1,xm)
| ~ doDivides0(X1,xl)
| $false
| $false
| ~ aNaturalNumber0(X1) ),
inference(rw,[status(thm)],[380,140,theory(equality)]) ).
cnf(382,plain,
( doDivides0(X1,xm)
| ~ doDivides0(X1,xl)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[381,theory(equality)]) ).
cnf(385,plain,
( sz00 = X1
| aNaturalNumber0(sdtsldt0(X2,X1))
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(er,[status(thm)],[131,theory(equality)]) ).
cnf(386,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xp != X1
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[131,124,theory(equality)]) ).
cnf(387,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xq != X1
| ~ doDivides0(xl,sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(spm,[status(thm)],[131,147,theory(equality)]) ).
cnf(388,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xp != X1
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[386,133,theory(equality)]) ).
cnf(389,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xp != X1
| $false
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[388,141,theory(equality)]) ).
cnf(390,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xp != X1
| $false
| $false
| $false ),
inference(rw,[status(thm)],[389,140,theory(equality)]) ).
cnf(391,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xp != X1 ),
inference(cn,[status(thm)],[390,theory(equality)]) ).
cnf(392,plain,
( aNaturalNumber0(X1)
| xp != X1 ),
inference(sr,[status(thm)],[391,84,theory(equality)]) ).
cnf(393,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xq != X1
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[387,132,theory(equality)]) ).
cnf(394,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xq != X1
| $false
| $false
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[393,141,theory(equality)]) ).
cnf(395,plain,
( sz00 = xl
| aNaturalNumber0(X1)
| xq != X1
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(cn,[status(thm)],[394,theory(equality)]) ).
cnf(396,plain,
( aNaturalNumber0(X1)
| xq != X1
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(sr,[status(thm)],[395,84,theory(equality)]) ).
cnf(416,plain,
( sdtmndt0(X1,X2) = X3
| sdtpldt0(X2,X3) != X1
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(csr,[status(thm)],[164,117]) ).
cnf(418,plain,
( sdtmndt0(X1,X2) = sz00
| X2 != X1
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(spm,[status(thm)],[416,189,theory(equality)]) ).
cnf(423,plain,
( sdtmndt0(X1,X2) = sz00
| X2 != X1
| $false
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(rw,[status(thm)],[418,170,theory(equality)]) ).
cnf(424,plain,
( sdtmndt0(X1,X2) = sz00
| X2 != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[423,theory(equality)]) ).
cnf(425,plain,
( sdtmndt0(X1,X1) = sz00
| ~ aNaturalNumber0(X1) ),
inference(er,[status(thm)],[424,theory(equality)]) ).
cnf(511,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sz10) ),
inference(spm,[status(thm)],[151,193,theory(equality)]) ).
cnf(538,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| $false ),
inference(rw,[status(thm)],[511,146,theory(equality)]) ).
cnf(539,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[538,theory(equality)]) ).
cnf(540,plain,
( sdtasdt0(X1,sdtsldt0(X2,X1)) = X2
| sz00 = X1
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(er,[status(thm)],[130,theory(equality)]) ).
cnf(541,plain,
( sdtasdt0(xl,X1) = xm
| sz00 = xl
| xp != X1
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[130,124,theory(equality)]) ).
cnf(542,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| sz00 = xl
| xq != X1
| ~ doDivides0(xl,sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(spm,[status(thm)],[130,147,theory(equality)]) ).
cnf(543,plain,
( sdtasdt0(xl,X1) = xm
| sz00 = xl
| xp != X1
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[541,133,theory(equality)]) ).
cnf(544,plain,
( sdtasdt0(xl,X1) = xm
| sz00 = xl
| xp != X1
| $false
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[543,141,theory(equality)]) ).
cnf(545,plain,
( sdtasdt0(xl,X1) = xm
| sz00 = xl
| xp != X1
| $false
| $false
| $false ),
inference(rw,[status(thm)],[544,140,theory(equality)]) ).
cnf(546,plain,
( sdtasdt0(xl,X1) = xm
| sz00 = xl
| xp != X1 ),
inference(cn,[status(thm)],[545,theory(equality)]) ).
cnf(547,plain,
( sdtasdt0(xl,X1) = xm
| xp != X1 ),
inference(sr,[status(thm)],[546,84,theory(equality)]) ).
cnf(548,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| sz00 = xl
| xq != X1
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[542,132,theory(equality)]) ).
cnf(549,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| sz00 = xl
| xq != X1
| $false
| $false
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[548,141,theory(equality)]) ).
cnf(550,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| sz00 = xl
| xq != X1
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(cn,[status(thm)],[549,theory(equality)]) ).
cnf(551,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| xq != X1
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(sr,[status(thm)],[550,84,theory(equality)]) ).
cnf(724,plain,
( sdtsldt0(X1,X2) = X3
| sz00 = X2
| sdtasdt0(X2,X3) != X1
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(csr,[status(thm)],[129,75]) ).
cnf(725,plain,
( sdtsldt0(sdtasdt0(X1,X2),X1) = X2
| sz00 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtasdt0(X1,X2)) ),
inference(er,[status(thm)],[724,theory(equality)]) ).
cnf(793,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X1)
| xp != X2 ),
inference(spm,[status(thm)],[82,392,theory(equality)]) ).
cnf(809,plain,
( sz00 = xl
| X1 = X2
| sdtlseqdt0(sdtasdt0(xl,X2),xm)
| ~ sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X1 ),
inference(spm,[status(thm)],[108,547,theory(equality)]) ).
cnf(814,plain,
( sdtsldt0(X1,xl) = X2
| sz00 = xl
| xm != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(X1)
| xp != X2 ),
inference(spm,[status(thm)],[724,547,theory(equality)]) ).
cnf(852,plain,
( sz00 = xl
| X1 = X2
| sdtlseqdt0(sdtasdt0(xl,X2),xm)
| ~ sdtlseqdt0(X2,X1)
| $false
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X1 ),
inference(rw,[status(thm)],[809,141,theory(equality)]) ).
cnf(853,plain,
( sz00 = xl
| X1 = X2
| sdtlseqdt0(sdtasdt0(xl,X2),xm)
| ~ sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X1 ),
inference(cn,[status(thm)],[852,theory(equality)]) ).
cnf(854,plain,
( X1 = X2
| sdtlseqdt0(sdtasdt0(xl,X2),xm)
| ~ sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X1 ),
inference(sr,[status(thm)],[853,84,theory(equality)]) ).
cnf(863,plain,
( sdtsldt0(X1,xl) = X2
| sz00 = xl
| xm != X1
| ~ aNaturalNumber0(X2)
| $false
| ~ aNaturalNumber0(X1)
| xp != X2 ),
inference(rw,[status(thm)],[814,141,theory(equality)]) ).
cnf(864,plain,
( sdtsldt0(X1,xl) = X2
| sz00 = xl
| xm != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X2 ),
inference(cn,[status(thm)],[863,theory(equality)]) ).
cnf(865,plain,
( sdtsldt0(X1,xl) = X2
| xm != X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| xp != X2 ),
inference(sr,[status(thm)],[864,84,theory(equality)]) ).
cnf(907,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| xp != X1
| xp != X2 ),
inference(spm,[status(thm)],[793,392,theory(equality)]) ).
cnf(940,plain,
( sdtlseqdt0(X1,xp)
| sdtlseqdt0(xp,X1)
| xp != X1 ),
inference(er,[status(thm)],[907,theory(equality)]) ).
cnf(941,plain,
sdtlseqdt0(xp,xp),
inference(er,[status(thm)],[940,theory(equality)]) ).
cnf(1450,plain,
( sdtpldt0(X1,X2) = X1
| sz00 != X2
| ~ sdtlseqdt0(X1,X1)
| ~ aNaturalNumber0(X1) ),
inference(spm,[status(thm)],[165,425,theory(equality)]) ).
cnf(1558,plain,
( doDivides0(sz10,xm)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xl) ),
inference(spm,[status(thm)],[382,318,theory(equality)]) ).
cnf(1562,plain,
( doDivides0(sz10,xm)
| $false
| ~ aNaturalNumber0(xl) ),
inference(rw,[status(thm)],[1558,146,theory(equality)]) ).
cnf(1563,plain,
( doDivides0(sz10,xm)
| $false
| $false ),
inference(rw,[status(thm)],[1562,141,theory(equality)]) ).
cnf(1564,plain,
doDivides0(sz10,xm),
inference(cn,[status(thm)],[1563,theory(equality)]) ).
cnf(1671,plain,
( aNaturalNumber0(X1)
| xq != X1
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[396,173,theory(equality)]) ).
cnf(1673,plain,
( aNaturalNumber0(X1)
| xq != X1
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[1671,139,theory(equality)]) ).
cnf(1674,plain,
( aNaturalNumber0(X1)
| xq != X1
| $false
| $false ),
inference(rw,[status(thm)],[1673,140,theory(equality)]) ).
cnf(1675,plain,
( aNaturalNumber0(X1)
| xq != X1 ),
inference(cn,[status(thm)],[1674,theory(equality)]) ).
cnf(1677,plain,
( sdtlseqdt0(X1,X2)
| sdtlseqdt0(X2,X1)
| xp != X1
| xq != X2 ),
inference(spm,[status(thm)],[793,1675,theory(equality)]) ).
cnf(1685,plain,
( sdtlseqdt0(X1,xp)
| sdtlseqdt0(xp,X1)
| xq != X1 ),
inference(er,[status(thm)],[1677,theory(equality)]) ).
cnf(1687,plain,
( sdtlseqdt0(xp,xq)
| sdtlseqdt0(xq,xp) ),
inference(er,[status(thm)],[1685,theory(equality)]) ).
cnf(1688,plain,
sdtlseqdt0(xq,xp),
inference(sr,[status(thm)],[1687,148,theory(equality)]) ).
cnf(3587,plain,
( sz00 = xl
| aNaturalNumber0(xp)
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[385,124,theory(equality)]) ).
cnf(3588,plain,
( sz00 = xl
| aNaturalNumber0(xq)
| ~ doDivides0(xl,sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(spm,[status(thm)],[385,147,theory(equality)]) ).
cnf(3600,plain,
( sz00 = xl
| aNaturalNumber0(xp)
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[3587,133,theory(equality)]) ).
cnf(3601,plain,
( sz00 = xl
| aNaturalNumber0(xp)
| $false
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[3600,141,theory(equality)]) ).
cnf(3602,plain,
( sz00 = xl
| aNaturalNumber0(xp)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[3601,140,theory(equality)]) ).
cnf(3603,plain,
( sz00 = xl
| aNaturalNumber0(xp) ),
inference(cn,[status(thm)],[3602,theory(equality)]) ).
cnf(3604,plain,
aNaturalNumber0(xp),
inference(sr,[status(thm)],[3603,84,theory(equality)]) ).
cnf(3605,plain,
( sz00 = xl
| aNaturalNumber0(xq)
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[3588,132,theory(equality)]) ).
cnf(3606,plain,
( sz00 = xl
| aNaturalNumber0(xq)
| $false
| $false
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(rw,[status(thm)],[3605,141,theory(equality)]) ).
cnf(3607,plain,
( sz00 = xl
| aNaturalNumber0(xq)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(cn,[status(thm)],[3606,theory(equality)]) ).
cnf(3608,plain,
( aNaturalNumber0(xq)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(sr,[status(thm)],[3607,84,theory(equality)]) ).
cnf(3918,plain,
( aNaturalNumber0(xq)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[3608,173,theory(equality)]) ).
cnf(3921,plain,
( aNaturalNumber0(xq)
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[3918,139,theory(equality)]) ).
cnf(3922,plain,
( aNaturalNumber0(xq)
| $false
| $false ),
inference(rw,[status(thm)],[3921,140,theory(equality)]) ).
cnf(3923,plain,
aNaturalNumber0(xq),
inference(cn,[status(thm)],[3922,theory(equality)]) ).
cnf(10249,plain,
( sdtasdt0(xl,xp) = xm
| sz00 = xl
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[540,124,theory(equality)]) ).
cnf(10311,plain,
( sdtasdt0(xl,xp) = xm
| sz00 = xl
| $false
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[10249,133,theory(equality)]) ).
cnf(10312,plain,
( sdtasdt0(xl,xp) = xm
| sz00 = xl
| $false
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[10311,141,theory(equality)]) ).
cnf(10313,plain,
( sdtasdt0(xl,xp) = xm
| sz00 = xl
| $false
| $false
| $false ),
inference(rw,[status(thm)],[10312,140,theory(equality)]) ).
cnf(10314,plain,
( sdtasdt0(xl,xp) = xm
| sz00 = xl ),
inference(cn,[status(thm)],[10313,theory(equality)]) ).
cnf(10315,plain,
sdtasdt0(xl,xp) = xm,
inference(sr,[status(thm)],[10314,84,theory(equality)]) ).
cnf(10381,plain,
( sdtasdt0(sz10,xm) = xm
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xl) ),
inference(spm,[status(thm)],[539,10315,theory(equality)]) ).
cnf(10498,plain,
( sdtasdt0(sz10,xm) = xm
| $false
| ~ aNaturalNumber0(xl) ),
inference(rw,[status(thm)],[10381,3604,theory(equality)]) ).
cnf(10499,plain,
( sdtasdt0(sz10,xm) = xm
| $false
| $false ),
inference(rw,[status(thm)],[10498,141,theory(equality)]) ).
cnf(10500,plain,
sdtasdt0(sz10,xm) = xm,
inference(cn,[status(thm)],[10499,theory(equality)]) ).
cnf(10750,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| xq != X1
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[551,173,theory(equality)]) ).
cnf(10754,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| xq != X1
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[10750,139,theory(equality)]) ).
cnf(10755,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| xq != X1
| $false
| $false ),
inference(rw,[status(thm)],[10754,140,theory(equality)]) ).
cnf(10756,plain,
( sdtasdt0(xl,X1) = sdtpldt0(xm,xn)
| xq != X1 ),
inference(cn,[status(thm)],[10755,theory(equality)]) ).
cnf(13050,plain,
( sdtpldt0(xm,xn) = xm
| xq != xp ),
inference(spm,[status(thm)],[10315,10756,theory(equality)]) ).
cnf(13053,plain,
( aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(xl)
| xq != X1 ),
inference(spm,[status(thm)],[169,10756,theory(equality)]) ).
cnf(13134,plain,
( aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(X1)
| $false
| xq != X1 ),
inference(rw,[status(thm)],[13053,141,theory(equality)]) ).
cnf(13135,plain,
( aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(X1)
| xq != X1 ),
inference(cn,[status(thm)],[13134,theory(equality)]) ).
cnf(30395,plain,
( sdtsldt0(sdtasdt0(X1,X2),X1) = X2
| sz00 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(csr,[status(thm)],[725,169]) ).
cnf(30398,plain,
( sdtsldt0(xm,sz10) = xm
| sz00 = sz10
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sz10) ),
inference(spm,[status(thm)],[30395,10500,theory(equality)]) ).
cnf(30446,plain,
( sdtsldt0(xm,sz10) = xm
| sz00 = sz10
| $false
| ~ aNaturalNumber0(sz10) ),
inference(rw,[status(thm)],[30398,140,theory(equality)]) ).
cnf(30447,plain,
( sdtsldt0(xm,sz10) = xm
| sz00 = sz10
| $false
| $false ),
inference(rw,[status(thm)],[30446,146,theory(equality)]) ).
cnf(30448,plain,
( sdtsldt0(xm,sz10) = xm
| sz00 = sz10 ),
inference(cn,[status(thm)],[30447,theory(equality)]) ).
cnf(30449,plain,
sdtsldt0(xm,sz10) = xm,
inference(sr,[status(thm)],[30448,145,theory(equality)]) ).
cnf(30523,plain,
( sz00 = sz10
| aNaturalNumber0(X1)
| xm != X1
| ~ doDivides0(sz10,xm)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[131,30449,theory(equality)]) ).
cnf(30527,plain,
( sz00 = sz10
| aNaturalNumber0(X1)
| xm != X1
| $false
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[30523,1564,theory(equality)]) ).
cnf(30528,plain,
( sz00 = sz10
| aNaturalNumber0(X1)
| xm != X1
| $false
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[30527,146,theory(equality)]) ).
cnf(30529,plain,
( sz00 = sz10
| aNaturalNumber0(X1)
| xm != X1
| $false
| $false
| $false ),
inference(rw,[status(thm)],[30528,140,theory(equality)]) ).
cnf(30530,plain,
( sz00 = sz10
| aNaturalNumber0(X1)
| xm != X1 ),
inference(cn,[status(thm)],[30529,theory(equality)]) ).
cnf(30531,plain,
( aNaturalNumber0(X1)
| xm != X1 ),
inference(sr,[status(thm)],[30530,145,theory(equality)]) ).
cnf(44641,plain,
( X1 = X2
| sdtlseqdt0(sdtasdt0(xl,X2),xm)
| xp != X1
| ~ sdtlseqdt0(X2,X1)
| ~ aNaturalNumber0(X2) ),
inference(csr,[status(thm)],[854,392]) ).
cnf(44646,plain,
( xp = xq
| sdtlseqdt0(sdtasdt0(xl,xq),xm)
| ~ aNaturalNumber0(xq) ),
inference(spm,[status(thm)],[44641,1688,theory(equality)]) ).
cnf(44807,plain,
( xp = xq
| sdtlseqdt0(sdtasdt0(xl,xq),xm)
| $false ),
inference(rw,[status(thm)],[44646,3923,theory(equality)]) ).
cnf(44808,plain,
( xp = xq
| sdtlseqdt0(sdtasdt0(xl,xq),xm) ),
inference(cn,[status(thm)],[44807,theory(equality)]) ).
cnf(45016,plain,
( xq = xp
| sdtlseqdt0(sdtpldt0(xm,xn),xm) ),
inference(spm,[status(thm)],[44808,10756,theory(equality)]) ).
cnf(46389,plain,
( sdtsldt0(X1,xl) = X2
| xp != X2
| xm != X1
| ~ aNaturalNumber0(X2) ),
inference(csr,[status(thm)],[865,30531]) ).
cnf(46390,plain,
( sdtsldt0(X1,xl) = X2
| xp != X2
| xm != X1 ),
inference(csr,[status(thm)],[46389,392]) ).
cnf(46391,plain,
( sdtsldt0(X1,xl) = xp
| xm != X1 ),
inference(er,[status(thm)],[46390,theory(equality)]) ).
cnf(46396,plain,
( xp = xq
| xm != sdtpldt0(xm,xn) ),
inference(spm,[status(thm)],[147,46391,theory(equality)]) ).
cnf(58681,plain,
( sdtpldt0(X1,X2) = X1
| sz00 != X2
| ~ aNaturalNumber0(X1) ),
inference(csr,[status(thm)],[1450,159]) ).
cnf(58876,plain,
( xq = xp
| sz00 != xn
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[46396,58681,theory(equality)]) ).
cnf(58949,plain,
( xq = xp
| sz00 != xn
| $false ),
inference(rw,[status(thm)],[58876,140,theory(equality)]) ).
cnf(58950,plain,
( xq = xp
| sz00 != xn ),
inference(cn,[status(thm)],[58949,theory(equality)]) ).
cnf(58968,plain,
( ~ sdtlseqdt0(xp,xp)
| xn != sz00 ),
inference(spm,[status(thm)],[148,58950,theory(equality)]) ).
cnf(59043,plain,
( $false
| xn != sz00 ),
inference(rw,[status(thm)],[58968,941,theory(equality)]) ).
cnf(59044,plain,
xn != sz00,
inference(cn,[status(thm)],[59043,theory(equality)]) ).
cnf(75728,plain,
( aNaturalNumber0(sdtpldt0(xm,xn))
| xq != X1 ),
inference(csr,[status(thm)],[13135,1675]) ).
cnf(75729,plain,
aNaturalNumber0(sdtpldt0(xm,xn)),
inference(er,[status(thm)],[75728,theory(equality)]) ).
cnf(75808,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| $false ),
inference(rw,[status(thm)],[255,75729,theory(equality)]) ).
cnf(75809,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm) ),
inference(cn,[status(thm)],[75808,theory(equality)]) ).
cnf(76341,plain,
( sdtpldt0(xm,xn) = xm
| xq = xp ),
inference(spm,[status(thm)],[75809,45016,theory(equality)]) ).
cnf(76398,plain,
sdtpldt0(xm,xn) = xm,
inference(csr,[status(thm)],[76341,13050]) ).
cnf(76416,plain,
( sz00 = xn
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn) ),
inference(spm,[status(thm)],[371,76398,theory(equality)]) ).
cnf(76588,plain,
( sz00 = xn
| $false
| ~ aNaturalNumber0(xn) ),
inference(rw,[status(thm)],[76416,140,theory(equality)]) ).
cnf(76589,plain,
( sz00 = xn
| $false
| $false ),
inference(rw,[status(thm)],[76588,139,theory(equality)]) ).
cnf(76590,plain,
sz00 = xn,
inference(cn,[status(thm)],[76589,theory(equality)]) ).
cnf(76591,plain,
$false,
inference(sr,[status(thm)],[76590,59044,theory(equality)]) ).
cnf(76592,plain,
$false,
76591,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM473+1 : TPTP v7.0.0. Released v4.0.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.03/0.23 % Computer : n121.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.625MB
% 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Fri Jan 5 05:01:00 CST 2018
% 0.03/0.23 % CPUTime :
% 0.03/0.27 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.28 --creating new selector for []
% 1.61/1.85 -running prover on /export/starexec/sandbox/tmp/tmp168nTy/sel_theBenchmark.p_1 with time limit 29
% 1.61/1.85 -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/tmp168nTy/sel_theBenchmark.p_1']
% 1.61/1.85 -prover status Theorem
% 1.61/1.85 Problem theBenchmark.p solved in phase 0.
% 1.61/1.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.61/1.85 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.61/1.85 Solved 1 out of 1.
% 1.61/1.85 # Problem is unsatisfiable (or provable), constructing proof object
% 1.61/1.85 # SZS status Theorem
% 1.61/1.85 # SZS output start CNFRefutation.
% See solution above
% 1.61/1.86 # SZS output end CNFRefutation
%------------------------------------------------------------------------------