%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM513+3 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n079.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:36 EST 2018
% Result : Theorem 4.19s
% Output : CNFRefutation 4.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 13
% Syntax : Number of formulae : 126 ( 37 unt; 0 def)
% Number of atoms : 484 ( 105 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 544 ( 186 ~; 220 |; 122 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 59 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(5,axiom,
( aNaturalNumber0(xr)
& ? [X1] :
( aNaturalNumber0(X1)
& equal(xk,sdtasdt0(xr,X1)) )
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& ! [X1] :
( ( aNaturalNumber0(X1)
& ( ? [X2] :
( aNaturalNumber0(X2)
& equal(xr,sdtasdt0(X1,X2)) )
| doDivides0(X1,xr) ) )
=> ( equal(X1,sz10)
| equal(X1,xr) ) )
& isPrime0(xr) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2342) ).
fof(9,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( ~ equal(X1,sz00)
=> ! [X2,X3] :
( ( aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> ( ( equal(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
| equal(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) )
=> equal(X2,X3) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',mMulCanc) ).
fof(10,axiom,
( ? [X1] :
( aNaturalNumber0(X1)
& equal(xn,sdtasdt0(xr,X1)) )
& doDivides0(xr,xn) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2487) ).
fof(22,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__1837) ).
fof(26,axiom,
( ~ ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr))) )
=> equal(sdtsldt0(xn,xr),xn) )
& aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(sdtsldt0(xn,xr),X1),xn) )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2504) ).
fof(36,conjecture,
( ( aNaturalNumber0(sdtsldt0(xk,xr))
& equal(xk,sdtasdt0(xr,sdtsldt0(xk,xr))) )
=> ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr))) )
=> equal(sdtasdt0(xp,sdtsldt0(xk,xr)),sdtasdt0(sdtsldt0(xn,xr),xm)) ) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__) ).
fof(37,axiom,
! [X1,X2,X3] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2)
& aNaturalNumber0(X3) )
=> equal(sdtasdt0(sdtasdt0(X1,X2),X3),sdtasdt0(X1,sdtasdt0(X2,X3))) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',mMulAsso) ).
fof(39,axiom,
( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& equal(sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr),sdtasdt0(xn,xm))
& aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& equal(sdtasdt0(xp,xk),sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)))
& equal(sdtasdt0(xn,xm),sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2576) ).
fof(42,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> aNaturalNumber0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',mSortsB_02) ).
fof(49,axiom,
( aNaturalNumber0(xk)
& equal(sdtasdt0(xn,xm),sdtasdt0(xp,xk))
& equal(xk,sdtsldt0(sdtasdt0(xn,xm),xp)) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2306) ).
fof(50,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> equal(sdtasdt0(X1,X2),sdtasdt0(X2,X1)) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',mMulComm) ).
fof(52,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( ~ equal(X1,sz00)
& doDivides0(X1,X2) )
=> ! [X3] :
( aNaturalNumber0(X3)
=> equal(sdtasdt0(X3,sdtsldt0(X2,X1)),sdtsldt0(sdtasdt0(X3,X2),X1)) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',mDivAsso) ).
fof(54,axiom,
( ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(xr,X1),xk) )
& ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtasdt0(xn,xm),sdtasdt0(xr,X1)) )
& doDivides0(xr,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1',m__2362) ).
fof(56,negated_conjecture,
~ ( ( aNaturalNumber0(sdtsldt0(xk,xr))
& equal(xk,sdtasdt0(xr,sdtsldt0(xk,xr))) )
=> ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr))) )
=> equal(sdtasdt0(xp,sdtsldt0(xk,xr)),sdtasdt0(sdtsldt0(xn,xr),xm)) ) ),
inference(assume_negation,[status(cth)],[36]) ).
fof(90,plain,
( aNaturalNumber0(xr)
& ? [X1] :
( aNaturalNumber0(X1)
& equal(xk,sdtasdt0(xr,X1)) )
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| ~ equal(xr,sdtasdt0(X1,X2)) )
& ~ doDivides0(X1,xr) )
| equal(X1,sz10)
| equal(X1,xr) )
& isPrime0(xr) ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(91,plain,
( aNaturalNumber0(xr)
& ? [X3] :
( aNaturalNumber0(X3)
& equal(xk,sdtasdt0(xr,X3)) )
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& ! [X4] :
( ~ aNaturalNumber0(X4)
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| ~ equal(xr,sdtasdt0(X4,X5)) )
& ~ doDivides0(X4,xr) )
| equal(X4,sz10)
| equal(X4,xr) )
& isPrime0(xr) ),
inference(variable_rename,[status(thm)],[90]) ).
fof(92,plain,
( aNaturalNumber0(xr)
& aNaturalNumber0(esk4_0)
& equal(xk,sdtasdt0(xr,esk4_0))
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& ! [X4] :
( ~ aNaturalNumber0(X4)
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| ~ equal(xr,sdtasdt0(X4,X5)) )
& ~ doDivides0(X4,xr) )
| equal(X4,sz10)
| equal(X4,xr) )
& isPrime0(xr) ),
inference(skolemize,[status(esa)],[91]) ).
fof(93,plain,
! [X4,X5] :
( ( ( ( ~ aNaturalNumber0(X5)
| ~ equal(xr,sdtasdt0(X4,X5)) )
& ~ doDivides0(X4,xr) )
| ~ aNaturalNumber0(X4)
| equal(X4,sz10)
| equal(X4,xr) )
& aNaturalNumber0(xr)
& aNaturalNumber0(esk4_0)
& equal(xk,sdtasdt0(xr,esk4_0))
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& isPrime0(xr) ),
inference(shift_quantors,[status(thm)],[92]) ).
fof(94,plain,
! [X4,X5] :
( ( ~ aNaturalNumber0(X5)
| ~ equal(xr,sdtasdt0(X4,X5))
| ~ aNaturalNumber0(X4)
| equal(X4,sz10)
| equal(X4,xr) )
& ( ~ doDivides0(X4,xr)
| ~ aNaturalNumber0(X4)
| equal(X4,sz10)
| equal(X4,xr) )
& aNaturalNumber0(xr)
& aNaturalNumber0(esk4_0)
& equal(xk,sdtasdt0(xr,esk4_0))
& doDivides0(xr,xk)
& ~ equal(xr,sz00)
& ~ equal(xr,sz10)
& isPrime0(xr) ),
inference(distribute,[status(thm)],[93]) ).
cnf(97,plain,
xr != sz00,
inference(split_conjunct,[status(thm)],[94]) ).
cnf(98,plain,
doDivides0(xr,xk),
inference(split_conjunct,[status(thm)],[94]) ).
cnf(99,plain,
xk = sdtasdt0(xr,esk4_0),
inference(split_conjunct,[status(thm)],[94]) ).
cnf(100,plain,
aNaturalNumber0(esk4_0),
inference(split_conjunct,[status(thm)],[94]) ).
cnf(101,plain,
aNaturalNumber0(xr),
inference(split_conjunct,[status(thm)],[94]) ).
fof(113,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| equal(X1,sz00)
| ! [X2,X3] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| ( ~ equal(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& ~ equal(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) )
| equal(X2,X3) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(114,plain,
! [X4] :
( ~ aNaturalNumber0(X4)
| equal(X4,sz00)
| ! [X5,X6] :
( ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| ( ~ equal(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
& ~ equal(sdtasdt0(X5,X4),sdtasdt0(X6,X4)) )
| equal(X5,X6) ) ),
inference(variable_rename,[status(thm)],[113]) ).
fof(115,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| ( ~ equal(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
& ~ equal(sdtasdt0(X5,X4),sdtasdt0(X6,X4)) )
| equal(X5,X6)
| equal(X4,sz00)
| ~ aNaturalNumber0(X4) ),
inference(shift_quantors,[status(thm)],[114]) ).
fof(116,plain,
! [X4,X5,X6] :
( ( ~ equal(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
| equal(X5,X6)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| equal(X4,sz00)
| ~ aNaturalNumber0(X4) )
& ( ~ equal(sdtasdt0(X5,X4),sdtasdt0(X6,X4))
| equal(X5,X6)
| ~ aNaturalNumber0(X5)
| ~ aNaturalNumber0(X6)
| equal(X4,sz00)
| ~ aNaturalNumber0(X4) ) ),
inference(distribute,[status(thm)],[115]) ).
cnf(118,plain,
( X1 = sz00
| X3 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X3)
| sdtasdt0(X1,X3) != sdtasdt0(X1,X2) ),
inference(split_conjunct,[status(thm)],[116]) ).
fof(119,plain,
( ? [X2] :
( aNaturalNumber0(X2)
& equal(xn,sdtasdt0(xr,X2)) )
& doDivides0(xr,xn) ),
inference(variable_rename,[status(thm)],[10]) ).
fof(120,plain,
( aNaturalNumber0(esk5_0)
& equal(xn,sdtasdt0(xr,esk5_0))
& doDivides0(xr,xn) ),
inference(skolemize,[status(esa)],[119]) ).
cnf(122,plain,
xn = sdtasdt0(xr,esk5_0),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(123,plain,
aNaturalNumber0(esk5_0),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(302,plain,
aNaturalNumber0(xp),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(303,plain,
aNaturalNumber0(xm),
inference(split_conjunct,[status(thm)],[22]) ).
fof(322,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ~ equal(sdtsldt0(xn,xr),xn)
& aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(sdtsldt0(xn,xr),X1),xn) )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(fof_nnf,[status(thm)],[26]) ).
fof(323,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ~ equal(sdtsldt0(xn,xr),xn)
& aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ? [X2] :
( aNaturalNumber0(X2)
& equal(sdtpldt0(sdtsldt0(xn,xr),X2),xn) )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(variable_rename,[status(thm)],[322]) ).
fof(324,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ~ equal(sdtsldt0(xn,xr),xn)
& aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& aNaturalNumber0(esk14_0)
& equal(sdtpldt0(sdtsldt0(xn,xr),esk14_0),xn)
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(skolemize,[status(esa)],[323]) ).
cnf(328,plain,
xn = sdtasdt0(xr,sdtsldt0(xn,xr)),
inference(split_conjunct,[status(thm)],[324]) ).
cnf(329,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(split_conjunct,[status(thm)],[324]) ).
fof(374,negated_conjecture,
( aNaturalNumber0(sdtsldt0(xk,xr))
& equal(xk,sdtasdt0(xr,sdtsldt0(xk,xr)))
& aNaturalNumber0(sdtsldt0(xn,xr))
& equal(xn,sdtasdt0(xr,sdtsldt0(xn,xr)))
& ~ equal(sdtasdt0(xp,sdtsldt0(xk,xr)),sdtasdt0(sdtsldt0(xn,xr),xm)) ),
inference(fof_nnf,[status(thm)],[56]) ).
cnf(375,negated_conjecture,
sdtasdt0(xp,sdtsldt0(xk,xr)) != sdtasdt0(sdtsldt0(xn,xr),xm),
inference(split_conjunct,[status(thm)],[374]) ).
cnf(378,negated_conjecture,
xk = sdtasdt0(xr,sdtsldt0(xk,xr)),
inference(split_conjunct,[status(thm)],[374]) ).
cnf(379,negated_conjecture,
aNaturalNumber0(sdtsldt0(xk,xr)),
inference(split_conjunct,[status(thm)],[374]) ).
fof(380,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)],[37]) ).
fof(381,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)],[380]) ).
cnf(382,plain,
( sdtasdt0(sdtasdt0(X1,X2),X3) = sdtasdt0(X1,sdtasdt0(X2,X3))
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[381]) ).
cnf(389,plain,
sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)),
inference(split_conjunct,[status(thm)],[39]) ).
cnf(390,plain,
aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr)),
inference(split_conjunct,[status(thm)],[39]) ).
cnf(391,plain,
sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm),
inference(split_conjunct,[status(thm)],[39]) ).
fof(404,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| aNaturalNumber0(sdtasdt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(405,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| aNaturalNumber0(sdtasdt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[404]) ).
cnf(406,plain,
( aNaturalNumber0(sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[405]) ).
cnf(439,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(split_conjunct,[status(thm)],[49]) ).
cnf(440,plain,
aNaturalNumber0(xk),
inference(split_conjunct,[status(thm)],[49]) ).
fof(441,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| equal(sdtasdt0(X1,X2),sdtasdt0(X2,X1)) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(442,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| equal(sdtasdt0(X3,X4),sdtasdt0(X4,X3)) ),
inference(variable_rename,[status(thm)],[441]) ).
cnf(443,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[442]) ).
fof(449,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| equal(X1,sz00)
| ~ doDivides0(X1,X2)
| ! [X3] :
( ~ aNaturalNumber0(X3)
| equal(sdtasdt0(X3,sdtsldt0(X2,X1)),sdtsldt0(sdtasdt0(X3,X2),X1)) ) ),
inference(fof_nnf,[status(thm)],[52]) ).
fof(450,plain,
! [X4,X5] :
( ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5)
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ! [X6] :
( ~ aNaturalNumber0(X6)
| equal(sdtasdt0(X6,sdtsldt0(X5,X4)),sdtsldt0(sdtasdt0(X6,X5),X4)) ) ),
inference(variable_rename,[status(thm)],[449]) ).
fof(451,plain,
! [X4,X5,X6] :
( ~ aNaturalNumber0(X6)
| equal(sdtasdt0(X6,sdtsldt0(X5,X4)),sdtsldt0(sdtasdt0(X6,X5),X4))
| equal(X4,sz00)
| ~ doDivides0(X4,X5)
| ~ aNaturalNumber0(X4)
| ~ aNaturalNumber0(X5) ),
inference(shift_quantors,[status(thm)],[450]) ).
cnf(452,plain,
( X2 = sz00
| sdtasdt0(X3,sdtsldt0(X1,X2)) = sdtsldt0(sdtasdt0(X3,X1),X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X1)
| ~ aNaturalNumber0(X3) ),
inference(split_conjunct,[status(thm)],[451]) ).
fof(458,plain,
( ? [X2] :
( aNaturalNumber0(X2)
& equal(sdtpldt0(xr,X2),xk) )
& ? [X3] :
( aNaturalNumber0(X3)
& equal(sdtasdt0(xn,xm),sdtasdt0(xr,X3)) )
& doDivides0(xr,sdtasdt0(xn,xm)) ),
inference(variable_rename,[status(thm)],[54]) ).
fof(459,plain,
( aNaturalNumber0(esk18_0)
& equal(sdtpldt0(xr,esk18_0),xk)
& aNaturalNumber0(esk19_0)
& equal(sdtasdt0(xn,xm),sdtasdt0(xr,esk19_0))
& doDivides0(xr,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa)],[458]) ).
cnf(461,plain,
sdtasdt0(xn,xm) = sdtasdt0(xr,esk19_0),
inference(split_conjunct,[status(thm)],[459]) ).
cnf(462,plain,
aNaturalNumber0(esk19_0),
inference(split_conjunct,[status(thm)],[459]) ).
cnf(473,plain,
aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)),
inference(rw,[status(thm)],[390,439,theory(equality)]) ).
cnf(609,plain,
sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)) = sdtasdt0(xp,xk),
inference(rw,[status(thm)],[389,439,theory(equality)]) ).
cnf(610,plain,
sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr)) = sdtasdt0(xn,xm),
inference(rw,[status(thm)],[609,439,theory(equality)]) ).
cnf(1187,plain,
( sdtasdt0(X1,sdtasdt0(X2,X3)) = sdtasdt0(X3,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(spm,[status(thm)],[443,382,theory(equality)]) ).
cnf(1546,plain,
( sz00 = xr
| esk4_0 = X1
| xk != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(esk4_0)
| ~ aNaturalNumber0(xr) ),
inference(spm,[status(thm)],[118,99,theory(equality)]) ).
cnf(1548,plain,
( sz00 = xr
| esk5_0 = X1
| xn != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(esk5_0)
| ~ aNaturalNumber0(xr) ),
inference(spm,[status(thm)],[118,122,theory(equality)]) ).
cnf(1558,plain,
( sz00 = xr
| esk19_0 = X1
| sdtasdt0(xn,xm) != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(esk19_0)
| ~ aNaturalNumber0(xr) ),
inference(spm,[status(thm)],[118,461,theory(equality)]) ).
cnf(1584,plain,
( sz00 = xr
| esk4_0 = X1
| xk != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| ~ aNaturalNumber0(xr) ),
inference(rw,[status(thm)],[1546,100,theory(equality)]) ).
cnf(1585,plain,
( sz00 = xr
| esk4_0 = X1
| xk != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[1584,101,theory(equality)]) ).
cnf(1586,plain,
( sz00 = xr
| esk4_0 = X1
| xk != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[1585,theory(equality)]) ).
cnf(1587,plain,
( esk4_0 = X1
| sdtasdt0(xr,X1) != xk
| ~ aNaturalNumber0(X1) ),
inference(sr,[status(thm)],[1586,97,theory(equality)]) ).
cnf(1592,plain,
( sz00 = xr
| esk5_0 = X1
| xn != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| ~ aNaturalNumber0(xr) ),
inference(rw,[status(thm)],[1548,123,theory(equality)]) ).
cnf(1593,plain,
( sz00 = xr
| esk5_0 = X1
| xn != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[1592,101,theory(equality)]) ).
cnf(1594,plain,
( sz00 = xr
| esk5_0 = X1
| xn != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[1593,theory(equality)]) ).
cnf(1595,plain,
( esk5_0 = X1
| sdtasdt0(xr,X1) != xn
| ~ aNaturalNumber0(X1) ),
inference(sr,[status(thm)],[1594,97,theory(equality)]) ).
cnf(1632,plain,
( sz00 = xr
| esk19_0 = X1
| sdtasdt0(xn,xm) != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| ~ aNaturalNumber0(xr) ),
inference(rw,[status(thm)],[1558,462,theory(equality)]) ).
cnf(1633,plain,
( sz00 = xr
| esk19_0 = X1
| sdtasdt0(xn,xm) != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[1632,101,theory(equality)]) ).
cnf(1634,plain,
( sz00 = xr
| esk19_0 = X1
| sdtasdt0(xn,xm) != sdtasdt0(xr,X1)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[1633,theory(equality)]) ).
cnf(1635,plain,
( esk19_0 = X1
| sdtasdt0(xr,X1) != sdtasdt0(xn,xm)
| ~ aNaturalNumber0(X1) ),
inference(sr,[status(thm)],[1634,97,theory(equality)]) ).
cnf(2222,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,sdtsldt0(xk,xr))
| sz00 = xr
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk) ),
inference(spm,[status(thm)],[452,98,theory(equality)]) ).
cnf(2230,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,sdtsldt0(xk,xr))
| sz00 = xr
| ~ aNaturalNumber0(X1)
| $false
| ~ aNaturalNumber0(xk) ),
inference(rw,[status(thm)],[2222,101,theory(equality)]) ).
cnf(2231,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,sdtsldt0(xk,xr))
| sz00 = xr
| ~ aNaturalNumber0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[2230,440,theory(equality)]) ).
cnf(2232,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,sdtsldt0(xk,xr))
| sz00 = xr
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[2231,theory(equality)]) ).
cnf(2233,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,sdtsldt0(xk,xr))
| ~ aNaturalNumber0(X1) ),
inference(sr,[status(thm)],[2232,97,theory(equality)]) ).
cnf(16612,negated_conjecture,
( esk4_0 = sdtsldt0(xk,xr)
| ~ aNaturalNumber0(sdtsldt0(xk,xr)) ),
inference(spm,[status(thm)],[1587,378,theory(equality)]) ).
cnf(16627,negated_conjecture,
( esk4_0 = sdtsldt0(xk,xr)
| $false ),
inference(rw,[status(thm)],[16612,379,theory(equality)]) ).
cnf(16628,negated_conjecture,
esk4_0 = sdtsldt0(xk,xr),
inference(cn,[status(thm)],[16627,theory(equality)]) ).
cnf(16655,negated_conjecture,
sdtasdt0(sdtsldt0(xn,xr),xm) != sdtasdt0(xp,esk4_0),
inference(rw,[status(thm)],[375,16628,theory(equality)]) ).
cnf(16751,plain,
( esk5_0 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(spm,[status(thm)],[1595,328,theory(equality)]) ).
cnf(16764,plain,
( esk5_0 = sdtsldt0(xn,xr)
| $false ),
inference(rw,[status(thm)],[16751,329,theory(equality)]) ).
cnf(16765,plain,
esk5_0 = sdtsldt0(xn,xr),
inference(cn,[status(thm)],[16764,theory(equality)]) ).
cnf(16786,plain,
sdtasdt0(sdtasdt0(esk5_0,xm),xr) = sdtasdt0(xn,xm),
inference(rw,[status(thm)],[391,16765,theory(equality)]) ).
cnf(16792,negated_conjecture,
sdtasdt0(esk5_0,xm) != sdtasdt0(xp,esk4_0),
inference(rw,[status(thm)],[16655,16765,theory(equality)]) ).
cnf(17739,plain,
( sdtasdt0(xn,xm) = sdtasdt0(esk5_0,sdtasdt0(xm,xr))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(esk5_0) ),
inference(spm,[status(thm)],[382,16786,theory(equality)]) ).
cnf(17947,plain,
( sdtasdt0(xn,xm) = sdtasdt0(esk5_0,sdtasdt0(xm,xr))
| $false
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(esk5_0) ),
inference(rw,[status(thm)],[17739,101,theory(equality)]) ).
cnf(17948,plain,
( sdtasdt0(xn,xm) = sdtasdt0(esk5_0,sdtasdt0(xm,xr))
| $false
| $false
| ~ aNaturalNumber0(esk5_0) ),
inference(rw,[status(thm)],[17947,303,theory(equality)]) ).
cnf(17949,plain,
( sdtasdt0(xn,xm) = sdtasdt0(esk5_0,sdtasdt0(xm,xr))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[17948,123,theory(equality)]) ).
cnf(17950,plain,
sdtasdt0(xn,xm) = sdtasdt0(esk5_0,sdtasdt0(xm,xr)),
inference(cn,[status(thm)],[17949,theory(equality)]) ).
cnf(24239,plain,
( esk19_0 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr)) ),
inference(spm,[status(thm)],[1635,610,theory(equality)]) ).
cnf(24252,plain,
( esk19_0 = sdtsldt0(sdtasdt0(xn,xm),xr)
| $false ),
inference(rw,[status(thm)],[24239,473,theory(equality)]) ).
cnf(24253,plain,
esk19_0 = sdtsldt0(sdtasdt0(xn,xm),xr),
inference(cn,[status(thm)],[24252,theory(equality)]) ).
cnf(52465,plain,
( sdtasdt0(X1,sdtasdt0(X2,X3)) = sdtasdt0(X3,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X3) ),
inference(csr,[status(thm)],[1187,406]) ).
cnf(52476,plain,
( sdtasdt0(xr,sdtasdt0(esk5_0,xm)) = sdtasdt0(xn,xm)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(esk5_0) ),
inference(spm,[status(thm)],[17950,52465,theory(equality)]) ).
cnf(53070,plain,
( sdtasdt0(xr,sdtasdt0(esk5_0,xm)) = sdtasdt0(xn,xm)
| $false
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(esk5_0) ),
inference(rw,[status(thm)],[52476,101,theory(equality)]) ).
cnf(53071,plain,
( sdtasdt0(xr,sdtasdt0(esk5_0,xm)) = sdtasdt0(xn,xm)
| $false
| $false
| ~ aNaturalNumber0(esk5_0) ),
inference(rw,[status(thm)],[53070,303,theory(equality)]) ).
cnf(53072,plain,
( sdtasdt0(xr,sdtasdt0(esk5_0,xm)) = sdtasdt0(xn,xm)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[53071,123,theory(equality)]) ).
cnf(53073,plain,
sdtasdt0(xr,sdtasdt0(esk5_0,xm)) = sdtasdt0(xn,xm),
inference(cn,[status(thm)],[53072,theory(equality)]) ).
cnf(83417,plain,
( esk19_0 = sdtasdt0(esk5_0,xm)
| ~ aNaturalNumber0(sdtasdt0(esk5_0,xm)) ),
inference(spm,[status(thm)],[1635,53073,theory(equality)]) ).
cnf(84050,plain,
( sdtasdt0(esk5_0,xm) = esk19_0
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(esk5_0) ),
inference(spm,[status(thm)],[83417,406,theory(equality)]) ).
cnf(84054,plain,
( sdtasdt0(esk5_0,xm) = esk19_0
| $false
| ~ aNaturalNumber0(esk5_0) ),
inference(rw,[status(thm)],[84050,303,theory(equality)]) ).
cnf(84055,plain,
( sdtasdt0(esk5_0,xm) = esk19_0
| $false
| $false ),
inference(rw,[status(thm)],[84054,123,theory(equality)]) ).
cnf(84056,plain,
sdtasdt0(esk5_0,xm) = esk19_0,
inference(cn,[status(thm)],[84055,theory(equality)]) ).
cnf(84286,negated_conjecture,
esk19_0 != sdtasdt0(xp,esk4_0),
inference(rw,[status(thm)],[16792,84056,theory(equality)]) ).
cnf(206881,plain,
( sdtsldt0(sdtasdt0(X1,xk),xr) = sdtasdt0(X1,esk4_0)
| ~ aNaturalNumber0(X1) ),
inference(rw,[status(thm)],[2233,16628,theory(equality)]) ).
cnf(206882,plain,
( sdtsldt0(sdtasdt0(xn,xm),xr) = sdtasdt0(xp,esk4_0)
| ~ aNaturalNumber0(xp) ),
inference(spm,[status(thm)],[206881,439,theory(equality)]) ).
cnf(206901,plain,
( esk19_0 = sdtasdt0(xp,esk4_0)
| ~ aNaturalNumber0(xp) ),
inference(rw,[status(thm)],[206882,24253,theory(equality)]) ).
cnf(206902,plain,
( esk19_0 = sdtasdt0(xp,esk4_0)
| $false ),
inference(rw,[status(thm)],[206901,302,theory(equality)]) ).
cnf(206903,plain,
esk19_0 = sdtasdt0(xp,esk4_0),
inference(cn,[status(thm)],[206902,theory(equality)]) ).
cnf(206904,plain,
$false,
inference(sr,[status(thm)],[206903,84286,theory(equality)]) ).
cnf(206905,plain,
$false,
206904,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM513+3 : 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 : n079.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 06:31:15 CST 2018
% 0.03/0.23 % CPUTime :
% 0.06/0.27 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.27 --creating new selector for []
% 4.19/4.40 -running prover on /export/starexec/sandbox2/tmp/tmp_s_C_4/sel_theBenchmark.p_1 with time limit 29
% 4.19/4.40 -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/tmp_s_C_4/sel_theBenchmark.p_1']
% 4.19/4.40 -prover status Theorem
% 4.19/4.40 Problem theBenchmark.p solved in phase 0.
% 4.19/4.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.19/4.40 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.19/4.40 Solved 1 out of 1.
% 4.19/4.40 # Problem is unsatisfiable (or provable), constructing proof object
% 4.19/4.40 # SZS status Theorem
% 4.19/4.40 # SZS output start CNFRefutation.
% See solution above
% 4.19/4.40 # SZS output end CNFRefutation
%------------------------------------------------------------------------------