%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM496+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 14:26:48 EDT 2022
% Result : Theorem 3.85s 4.10s
% Output : Refutation 3.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 19
% Syntax : Number of clauses : 50 ( 14 unt; 1 nHn; 50 RR)
% Number of literals : 150 ( 0 equ; 102 neg)
% Maximal clause size : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
aNaturalNumber0(sz10),
file('NUM496+1.p',unknown),
[] ).
cnf(3,axiom,
aNaturalNumber0(xn),
file('NUM496+1.p',unknown),
[] ).
cnf(5,axiom,
aNaturalNumber0(xp),
file('NUM496+1.p',unknown),
[] ).
cnf(6,axiom,
isPrime0(xp),
file('NUM496+1.p',unknown),
[] ).
cnf(9,axiom,
sdtlseqdt0(xp,xn),
file('NUM496+1.p',unknown),
[] ).
cnf(11,axiom,
~ doDivides0(xp,xn),
file('NUM496+1.p',unknown),
[] ).
cnf(12,axiom,
~ doDivides0(xp,xm),
file('NUM496+1.p',unknown),
[] ).
cnf(13,axiom,
~ equal(sz10,sz00),
file('NUM496+1.p',unknown),
[] ).
cnf(15,axiom,
aNaturalNumber0(skf5(u,v)),
file('NUM496+1.p',unknown),
[] ).
cnf(18,axiom,
equal(sdtmndt0(xn,xp),xr),
file('NUM496+1.p',unknown),
[] ).
cnf(21,axiom,
( doDivides0(xp,xr)
| doDivides0(xp,xm) ),
file('NUM496+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ aNaturalNumber0(u)
| equal(sdtasdt0(u,sz10),u) ),
file('NUM496+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| aNaturalNumber0(sdtasdt0(v,u)) ),
file('NUM496+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ doDivides0(v,u)
| equal(sdtasdt0(v,skf5(v,u)),u) ),
file('NUM496+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,u)
| ~ equal(w,sdtmndt0(u,v))
| aNaturalNumber0(w) ),
file('NUM496+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ equal(u,sdtasdt0(v,w))
| doDivides0(v,u) ),
file('NUM496+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ doDivides0(v,u)
| ~ doDivides0(w,v)
| doDivides0(w,u) ),
file('NUM496+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,u)
| ~ equal(w,sdtmndt0(u,v))
| equal(sdtpldt0(v,w),u) ),
file('NUM496+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ doDivides0(w,u)
| ~ doDivides0(w,v)
| doDivides0(w,sdtpldt0(v,u)) ),
file('NUM496+1.p',unknown),
[] ).
cnf(83,plain,
doDivides0(xp,xr),
inference(mrr,[status(thm)],[21,12]),
[iquote('0:MRR:21.1,12.0')] ).
cnf(93,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| equal(sdtasdt0(xp,skf5(xp,xr)),xr) ),
inference(res,[status(thm),theory(equality)],[83,50]),
[iquote('0:Res:83.0,50.2')] ).
cnf(109,plain,
( ~ aNaturalNumber0(xr)
| equal(sdtasdt0(xp,skf5(xp,xr)),xr) ),
inference(mrr,[status(thm)],[93,5]),
[iquote('0:MRR:93.0,5.0')] ).
cnf(610,plain,
( ~ aNaturalNumber0(sdtasdt0(u,v))
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| doDivides0(u,sdtasdt0(u,v)) ),
inference(eqr,[status(thm),theory(equality)],[54]),
[iquote('0:EqR:54.3')] ).
cnf(618,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| doDivides0(u,sdtasdt0(u,v)) ),
inference(ssi,[status(thm)],[610,29]),
[iquote('0:SSi:610.0,29.2')] ).
cnf(655,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(sz10)
| doDivides0(u,u) ),
inference(spr,[status(thm),theory(equality)],[24,618]),
[iquote('0:SpR:24.1,618.2')] ).
cnf(670,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(sz10)
| doDivides0(u,u) ),
inference(obv,[status(thm),theory(equality)],[655]),
[iquote('0:Obv:655.0')] ).
cnf(671,plain,
( ~ aNaturalNumber0(u)
| doDivides0(u,u) ),
inference(ssi,[status(thm)],[670,2]),
[iquote('0:SSi:670.1,2.0')] ).
cnf(704,plain,
( ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xp,xn)
| ~ equal(u,xr)
| aNaturalNumber0(u) ),
inference(spl,[status(thm),theory(equality)],[18,53]),
[iquote('0:SpL:18.0,53.3')] ).
cnf(705,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ equal(u,xr)
| aNaturalNumber0(u) ),
inference(ssi,[status(thm)],[704,6,5,3]),
[iquote('0:SSi:704.1,704.0,6.0,5.0,3.0')] ).
cnf(706,plain,
( ~ equal(u,xr)
| aNaturalNumber0(u) ),
inference(mrr,[status(thm)],[705,9]),
[iquote('0:MRR:705.0,9.0')] ).
cnf(737,plain,
( ~ equal(xr,xr)
| equal(sdtasdt0(xp,skf5(xp,xr)),xr) ),
inference(sor,[status(thm)],[109,706]),
[iquote('0:SoR:109.0,706.1')] ).
cnf(751,plain,
equal(sdtasdt0(xp,skf5(xp,xr)),xr),
inference(obv,[status(thm),theory(equality)],[737]),
[iquote('0:Obv:737.0')] ).
cnf(1513,plain,
( ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xp,xn)
| ~ equal(u,xr)
| equal(sdtpldt0(xp,u),xn) ),
inference(spl,[status(thm),theory(equality)],[18,63]),
[iquote('0:SpL:18.0,63.3')] ).
cnf(1515,plain,
( ~ sdtlseqdt0(xp,xn)
| ~ equal(u,xr)
| equal(sdtpldt0(xp,u),xn) ),
inference(ssi,[status(thm)],[1513,6,5,3]),
[iquote('0:SSi:1513.1,1513.0,6.0,5.0,3.0')] ).
cnf(1516,plain,
( ~ equal(u,xr)
| equal(sdtpldt0(xp,u),xn) ),
inference(mrr,[status(thm)],[1515,9]),
[iquote('0:MRR:1515.0,9.0')] ).
cnf(1546,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(skf5(xp,xr))
| ~ equal(u,xr)
| doDivides0(xp,u) ),
inference(spl,[status(thm),theory(equality)],[751,54]),
[iquote('0:SpL:751.0,54.3')] ).
cnf(1555,plain,
( ~ aNaturalNumber0(u)
| ~ equal(u,xr)
| doDivides0(xp,u) ),
inference(ssi,[status(thm)],[1546,15,6,5]),
[iquote('0:SSi:1546.2,1546.1,15.0,6.0,5.0,6.0,5.0')] ).
cnf(1556,plain,
( ~ equal(u,xr)
| doDivides0(xp,u) ),
inference(mrr,[status(thm)],[1555,706]),
[iquote('0:MRR:1555.0,706.1')] ).
cnf(1616,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(v)
| ~ equal(u,xr)
| ~ doDivides0(v,xp)
| doDivides0(v,u) ),
inference(res,[status(thm),theory(equality)],[1556,56]),
[iquote('0:Res:1556.1,56.3')] ).
cnf(1625,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ equal(u,xr)
| ~ doDivides0(v,xp)
| doDivides0(v,u) ),
inference(ssi,[status(thm)],[1616,6,5]),
[iquote('0:SSi:1616.1,6.0,5.0')] ).
cnf(1626,plain,
( ~ aNaturalNumber0(u)
| ~ equal(v,xr)
| ~ doDivides0(u,xp)
| doDivides0(u,v) ),
inference(mrr,[status(thm)],[1625,706]),
[iquote('0:MRR:1625.0,706.1')] ).
cnf(1752,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(v)
| ~ equal(u,xr)
| ~ doDivides0(v,u)
| ~ doDivides0(v,xp)
| doDivides0(v,xn) ),
inference(spr,[status(thm),theory(equality)],[1516,65]),
[iquote('0:SpR:1516.1,65.5')] ).
cnf(1785,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ equal(u,xr)
| ~ doDivides0(v,u)
| ~ doDivides0(v,xp)
| doDivides0(v,xn) ),
inference(ssi,[status(thm)],[1752,6,5]),
[iquote('0:SSi:1752.1,6.0,5.0')] ).
cnf(1786,plain,
( ~ aNaturalNumber0(u)
| ~ equal(v,xr)
| ~ doDivides0(u,v)
| ~ doDivides0(u,xp)
| doDivides0(u,xn) ),
inference(mrr,[status(thm)],[1785,706]),
[iquote('0:MRR:1785.0,706.1')] ).
cnf(1787,plain,
( ~ aNaturalNumber0(u)
| ~ equal(v,xr)
| ~ doDivides0(u,xp)
| doDivides0(u,xn) ),
inference(mrr,[status(thm)],[1786,1626]),
[iquote('0:MRR:1786.2,1626.3')] ).
cnf(5257,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,xp)
| doDivides0(u,xn) ),
inference(aed,[status(thm),theory(equality)],[13,1787]),
[iquote('0:AED:13.0,1787.1')] ).
cnf(9617,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp)
| doDivides0(xp,xn) ),
inference(res,[status(thm),theory(equality)],[671,5257]),
[iquote('0:Res:671.1,5257.1')] ).
cnf(9620,plain,
( ~ aNaturalNumber0(xp)
| doDivides0(xp,xn) ),
inference(obv,[status(thm),theory(equality)],[9617]),
[iquote('0:Obv:9617.0')] ).
cnf(9621,plain,
doDivides0(xp,xn),
inference(ssi,[status(thm)],[9620,6,5]),
[iquote('0:SSi:9620.0,6.0,5.0')] ).
cnf(9622,plain,
$false,
inference(mrr,[status(thm)],[9621,11]),
[iquote('0:MRR:9621.0,11.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.07 % Problem : NUM496+1 : TPTP v8.1.0. Released v4.0.0.
% 0.02/0.07 % Command : run_spass %d %s
% 0.06/0.25 % Computer : n014.cluster.edu
% 0.06/0.25 % Model : x86_64 x86_64
% 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.25 % Memory : 8042.1875MB
% 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.25 % CPULimit : 300
% 0.06/0.25 % WCLimit : 600
% 0.06/0.25 % DateTime : Thu Jul 7 17:50:36 EDT 2022
% 0.06/0.25 % CPUTime :
% 3.85/4.10
% 3.85/4.10 SPASS V 3.9
% 3.85/4.10 SPASS beiseite: Proof found.
% 3.85/4.10 % SZS status Theorem
% 3.85/4.10 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.85/4.10 SPASS derived 5817 clauses, backtracked 382 clauses, performed 7 splits and kept 2396 clauses.
% 3.85/4.10 SPASS allocated 106325 KBytes.
% 3.85/4.10 SPASS spent 0:00:03.26 on the problem.
% 3.85/4.10 0:00:00.04 for the input.
% 3.85/4.10 0:00:00.04 for the FLOTTER CNF translation.
% 3.85/4.10 0:00:00.07 for inferences.
% 3.85/4.10 0:00:00.02 for the backtracking.
% 3.85/4.10 0:00:03.05 for the reduction.
% 3.85/4.10
% 3.85/4.10
% 3.85/4.10 Here is a proof with depth 4, length 50 :
% 3.85/4.10 % SZS output start Refutation
% See solution above
% 3.85/4.10 Formulae used in the proof : mSortsC_01 m__1837 m__1860 m__1870 m__ mDefDiv m__1883 m__2027 m_MulUnit mSortsB_02 mDefDiff mDivTrans mDivSum
% 3.85/4.10
%------------------------------------------------------------------------------