%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM521+3 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n066.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:38 EST 2018
% Result : Theorem 0.06s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 12 unt; 0 def)
% Number of atoms : 227 ( 24 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 294 ( 127 ~; 118 |; 47 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 32 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(11,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( sdtlseqdt0(X1,X2)
| ( ~ equal(X2,X1)
& sdtlseqdt0(X2,X1) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',mLETotal) ).
fof(14,axiom,
~ ( ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(xp,X1),xn) )
| sdtlseqdt0(xp,xn) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m__1870) ).
fof(16,axiom,
~ ( ~ equal(xn,xp)
& ( ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(xn,X1),xp) )
| sdtlseqdt0(xn,xp) )
& ~ equal(xm,xp)
& ( ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(xm,X1),xp) )
| sdtlseqdt0(xm,xp) ) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m__2287) ).
fof(17,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m__1837) ).
fof(28,axiom,
( aNaturalNumber0(sz10)
& ~ equal(sz10,sz00) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',mSortsC_01) ).
fof(29,conjecture,
( ? [X1] :
( aNaturalNumber0(X1)
& equal(xn,sdtasdt0(xp,X1)) )
| doDivides0(xp,xn)
| ? [X1] :
( aNaturalNumber0(X1)
& equal(xm,sdtasdt0(xp,X1)) )
| doDivides0(xp,xm) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m__) ).
fof(42,axiom,
~ ( ? [X1] :
( aNaturalNumber0(X1)
& equal(sdtpldt0(xp,X1),xm) )
| sdtlseqdt0(xp,xm) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m__2075) ).
fof(45,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1',m_MulUnit) ).
fof(46,negated_conjecture,
~ ( ? [X1] :
( aNaturalNumber0(X1)
& equal(xn,sdtasdt0(xp,X1)) )
| doDivides0(xp,xn)
| ? [X1] :
( aNaturalNumber0(X1)
& equal(xm,sdtasdt0(xp,X1)) )
| doDivides0(xp,xm) ),
inference(assume_negation,[status(cth)],[29]) ).
fof(227,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X1,X2)
| ( ~ equal(X2,X1)
& sdtlseqdt0(X2,X1) ) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(228,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| sdtlseqdt0(X3,X4)
| ( ~ equal(X4,X3)
& sdtlseqdt0(X4,X3) ) ),
inference(variable_rename,[status(thm)],[227]) ).
fof(229,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)],[228]) ).
cnf(230,plain,
( sdtlseqdt0(X2,X1)
| sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(split_conjunct,[status(thm)],[229]) ).
fof(238,plain,
( ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(sdtpldt0(xp,X1),xn) )
& ~ sdtlseqdt0(xp,xn) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(239,plain,
( ! [X2] :
( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xp,X2),xn) )
& ~ sdtlseqdt0(xp,xn) ),
inference(variable_rename,[status(thm)],[238]) ).
fof(240,plain,
! [X2] :
( ( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xp,X2),xn) )
& ~ sdtlseqdt0(xp,xn) ),
inference(shift_quantors,[status(thm)],[239]) ).
cnf(241,plain,
~ sdtlseqdt0(xp,xn),
inference(split_conjunct,[status(thm)],[240]) ).
fof(246,plain,
( equal(xn,xp)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(sdtpldt0(xn,X1),xp) )
& ~ sdtlseqdt0(xn,xp) )
| equal(xm,xp)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(sdtpldt0(xm,X1),xp) )
& ~ sdtlseqdt0(xm,xp) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(247,plain,
( equal(xn,xp)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xn,X2),xp) )
& ~ sdtlseqdt0(xn,xp) )
| equal(xm,xp)
| ( ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(xm,X3),xp) )
& ~ sdtlseqdt0(xm,xp) ) ),
inference(variable_rename,[status(thm)],[246]) ).
fof(248,plain,
! [X2,X3] :
( ( ( ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(xm,X3),xp) )
& ~ sdtlseqdt0(xm,xp) )
| ( ( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xn,X2),xp) )
& ~ sdtlseqdt0(xn,xp) )
| equal(xn,xp)
| equal(xm,xp) ),
inference(shift_quantors,[status(thm)],[247]) ).
fof(249,plain,
! [X2,X3] :
( ( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xn,X2),xp)
| equal(xn,xp)
| equal(xm,xp)
| ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(xm,X3),xp) )
& ( ~ sdtlseqdt0(xn,xp)
| equal(xn,xp)
| equal(xm,xp)
| ~ aNaturalNumber0(X3)
| ~ equal(sdtpldt0(xm,X3),xp) )
& ( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xn,X2),xp)
| equal(xn,xp)
| equal(xm,xp)
| ~ sdtlseqdt0(xm,xp) )
& ( ~ sdtlseqdt0(xn,xp)
| equal(xn,xp)
| equal(xm,xp)
| ~ sdtlseqdt0(xm,xp) ) ),
inference(distribute,[status(thm)],[248]) ).
cnf(250,plain,
( xm = xp
| xn = xp
| ~ sdtlseqdt0(xm,xp)
| ~ sdtlseqdt0(xn,xp) ),
inference(split_conjunct,[status(thm)],[249]) ).
cnf(254,plain,
aNaturalNumber0(xp),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(255,plain,
aNaturalNumber0(xm),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(256,plain,
aNaturalNumber0(xn),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(308,plain,
aNaturalNumber0(sz10),
inference(split_conjunct,[status(thm)],[28]) ).
fof(309,negated_conjecture,
( ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(xn,sdtasdt0(xp,X1)) )
& ~ doDivides0(xp,xn)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(xm,sdtasdt0(xp,X1)) )
& ~ doDivides0(xp,xm) ),
inference(fof_nnf,[status(thm)],[46]) ).
fof(310,negated_conjecture,
( ! [X2] :
( ~ aNaturalNumber0(X2)
| ~ equal(xn,sdtasdt0(xp,X2)) )
& ~ doDivides0(xp,xn)
& ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ equal(xm,sdtasdt0(xp,X3)) )
& ~ doDivides0(xp,xm) ),
inference(variable_rename,[status(thm)],[309]) ).
fof(311,negated_conjecture,
! [X2,X3] :
( ( ~ aNaturalNumber0(X3)
| ~ equal(xm,sdtasdt0(xp,X3)) )
& ( ~ aNaturalNumber0(X2)
| ~ equal(xn,sdtasdt0(xp,X2)) )
& ~ doDivides0(xp,xn)
& ~ doDivides0(xp,xm) ),
inference(shift_quantors,[status(thm)],[310]) ).
cnf(314,negated_conjecture,
( xn != sdtasdt0(xp,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[311]) ).
cnf(315,negated_conjecture,
( xm != sdtasdt0(xp,X1)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[311]) ).
fof(371,plain,
( ! [X1] :
( ~ aNaturalNumber0(X1)
| ~ equal(sdtpldt0(xp,X1),xm) )
& ~ sdtlseqdt0(xp,xm) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(372,plain,
( ! [X2] :
( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xp,X2),xm) )
& ~ sdtlseqdt0(xp,xm) ),
inference(variable_rename,[status(thm)],[371]) ).
fof(373,plain,
! [X2] :
( ( ~ aNaturalNumber0(X2)
| ~ equal(sdtpldt0(xp,X2),xm) )
& ~ sdtlseqdt0(xp,xm) ),
inference(shift_quantors,[status(thm)],[372]) ).
cnf(374,plain,
~ sdtlseqdt0(xp,xm),
inference(split_conjunct,[status(thm)],[373]) ).
fof(385,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
inference(fof_nnf,[status(thm)],[45]) ).
fof(386,plain,
! [X2] :
( ~ aNaturalNumber0(X2)
| ( equal(sdtasdt0(X2,sz10),X2)
& equal(X2,sdtasdt0(sz10,X2)) ) ),
inference(variable_rename,[status(thm)],[385]) ).
fof(387,plain,
! [X2] :
( ( equal(sdtasdt0(X2,sz10),X2)
| ~ aNaturalNumber0(X2) )
& ( equal(X2,sdtasdt0(sz10,X2))
| ~ aNaturalNumber0(X2) ) ),
inference(distribute,[status(thm)],[386]) ).
cnf(389,plain,
( sdtasdt0(X1,sz10) = X1
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[387]) ).
cnf(402,negated_conjecture,
( xp != xn
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xp) ),
inference(spm,[status(thm)],[314,389,theory(equality)]) ).
cnf(403,negated_conjecture,
( xp != xm
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xp) ),
inference(spm,[status(thm)],[315,389,theory(equality)]) ).
cnf(404,negated_conjecture,
( xp != xn
| $false
| ~ aNaturalNumber0(xp) ),
inference(rw,[status(thm)],[402,308,theory(equality)]) ).
cnf(405,negated_conjecture,
( xp != xn
| $false
| $false ),
inference(rw,[status(thm)],[404,254,theory(equality)]) ).
cnf(406,negated_conjecture,
xp != xn,
inference(cn,[status(thm)],[405,theory(equality)]) ).
cnf(407,negated_conjecture,
( xp != xm
| $false
| ~ aNaturalNumber0(xp) ),
inference(rw,[status(thm)],[403,308,theory(equality)]) ).
cnf(408,negated_conjecture,
( xp != xm
| $false
| $false ),
inference(rw,[status(thm)],[407,254,theory(equality)]) ).
cnf(409,negated_conjecture,
xp != xm,
inference(cn,[status(thm)],[408,theory(equality)]) ).
cnf(533,plain,
( xm = xp
| xn = xp
| sdtlseqdt0(xp,xn)
| ~ sdtlseqdt0(xm,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn) ),
inference(spm,[status(thm)],[250,230,theory(equality)]) ).
cnf(535,plain,
( xm = xp
| xn = xp
| sdtlseqdt0(xp,xn)
| ~ sdtlseqdt0(xm,xp)
| $false
| ~ aNaturalNumber0(xn) ),
inference(rw,[status(thm)],[533,254,theory(equality)]) ).
cnf(536,plain,
( xm = xp
| xn = xp
| sdtlseqdt0(xp,xn)
| ~ sdtlseqdt0(xm,xp)
| $false
| $false ),
inference(rw,[status(thm)],[535,256,theory(equality)]) ).
cnf(537,plain,
( xm = xp
| xn = xp
| sdtlseqdt0(xp,xn)
| ~ sdtlseqdt0(xm,xp) ),
inference(cn,[status(thm)],[536,theory(equality)]) ).
cnf(538,plain,
( xm = xp
| xn = xp
| ~ sdtlseqdt0(xm,xp) ),
inference(sr,[status(thm)],[537,241,theory(equality)]) ).
cnf(4551,plain,
( xn = xp
| ~ sdtlseqdt0(xm,xp) ),
inference(sr,[status(thm)],[538,409,theory(equality)]) ).
cnf(4552,plain,
~ sdtlseqdt0(xm,xp),
inference(sr,[status(thm)],[4551,406,theory(equality)]) ).
cnf(4553,plain,
( sdtlseqdt0(xp,xm)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm) ),
inference(spm,[status(thm)],[4552,230,theory(equality)]) ).
cnf(4555,plain,
( sdtlseqdt0(xp,xm)
| $false
| ~ aNaturalNumber0(xm) ),
inference(rw,[status(thm)],[4553,254,theory(equality)]) ).
cnf(4556,plain,
( sdtlseqdt0(xp,xm)
| $false
| $false ),
inference(rw,[status(thm)],[4555,255,theory(equality)]) ).
cnf(4557,plain,
sdtlseqdt0(xp,xm),
inference(cn,[status(thm)],[4556,theory(equality)]) ).
cnf(4558,plain,
$false,
inference(sr,[status(thm)],[4557,374,theory(equality)]) ).
cnf(4559,plain,
$false,
4558,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM521+3 : TPTP v7.0.0. Released v4.0.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n066.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 08:29:59 CST 2018
% 0.02/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 []
% 0.06/0.47 -running prover on /export/starexec/sandbox2/tmp/tmp0RsUBM/sel_theBenchmark.p_1 with time limit 29
% 0.06/0.47 -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/tmp0RsUBM/sel_theBenchmark.p_1']
% 0.06/0.47 -prover status Theorem
% 0.06/0.47 Problem theBenchmark.p solved in phase 0.
% 0.06/0.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.47 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.47 Solved 1 out of 1.
% 0.06/0.47 # Problem is unsatisfiable (or provable), constructing proof object
% 0.06/0.47 # SZS status Theorem
% 0.06/0.47 # SZS output start CNFRefutation.
% See solution above
% 0.06/0.47 # SZS output end CNFRefutation
%------------------------------------------------------------------------------