%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.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:50 EDT 2022
% Result : Theorem 0.45s 0.61s
% Output : Refutation 0.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 20
% Syntax : Number of clauses : 39 ( 14 unt; 7 nHn; 39 RR)
% Number of literals : 121 ( 0 equ; 81 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 : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
aNaturalNumber0(xn),
file('NUM500+1.p',unknown),
[] ).
cnf(4,axiom,
aNaturalNumber0(xm),
file('NUM500+1.p',unknown),
[] ).
cnf(5,axiom,
aNaturalNumber0(xp),
file('NUM500+1.p',unknown),
[] ).
cnf(6,axiom,
isPrime0(xp),
file('NUM500+1.p',unknown),
[] ).
cnf(8,axiom,
aNaturalNumber0(skf7(u)),
file('NUM500+1.p',unknown),
[] ).
cnf(12,axiom,
aNaturalNumber0(skf4(u,v)),
file('NUM500+1.p',unknown),
[] ).
cnf(20,axiom,
~ equal(xk,sz00),
file('NUM500+1.p',unknown),
[] ).
cnf(21,axiom,
~ equal(xk,sz10),
file('NUM500+1.p',unknown),
[] ).
cnf(22,axiom,
doDivides0(xp,sdtasdt0(xn,xm)),
file('NUM500+1.p',unknown),
[] ).
cnf(24,axiom,
equal(sdtsldt0(sdtasdt0(xn,xm),xp),xk),
file('NUM500+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ isPrime0(u)
| ~ aNaturalNumber0(u)
| ~ doDivides0(u,xk) ),
file('NUM500+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| aNaturalNumber0(sdtpldt0(v,u)) ),
file('NUM500+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| aNaturalNumber0(sdtasdt0(v,u)) ),
file('NUM500+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ aNaturalNumber0(u)
| ~ isPrime0(u)
| ~ equal(u,sz00) ),
file('NUM500+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ aNaturalNumber0(u)
| isPrime0(skf7(u))
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM500+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ aNaturalNumber0(u)
| equal(u,sz10)
| equal(u,sz00)
| doDivides0(skf7(u),u) ),
file('NUM500+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ equal(sdtpldt0(v,w),u)
| sdtlseqdt0(v,u) ),
file('NUM500+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,u)
| ~ equal(w,sdtmndt0(u,v))
| aNaturalNumber0(w) ),
file('NUM500+1.p',unknown),
[] ).
cnf(66,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ doDivides0(v,u)
| ~ equal(w,sdtsldt0(u,v))
| aNaturalNumber0(w)
| equal(v,sz00) ),
file('NUM500+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ sdtlseqdt0(v,w)
| ~ equal(sdtpldt0(v,u),w)
| equal(u,sdtmndt0(w,v)) ),
file('NUM500+1.p',unknown),
[] ).
cnf(87,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ equal(sdtpldt0(v,w),u)
| equal(w,sdtmndt0(u,v)) ),
inference(mrr,[status(thm)],[79,56]),
[iquote('0:MRR:79.3,56.4')] ).
cnf(114,plain,
~ equal(xp,sz00),
inference(ems,[status(thm)],[34,5,6]),
[iquote('0:EmS:34.0,34.1,5.0,6.0')] ).
cnf(141,plain,
( ~ aNaturalNumber0(xk)
| ~ isPrime0(skf7(xk))
| ~ aNaturalNumber0(skf7(xk))
| equal(xk,sz10)
| equal(xk,sz00) ),
inference(res,[status(thm),theory(equality)],[43,31]),
[iquote('0:Res:43.3,31.2')] ).
cnf(142,plain,
( ~ aNaturalNumber0(xk)
| ~ isPrime0(skf7(xk))
| equal(xk,sz10)
| equal(xk,sz00) ),
inference(ssi,[status(thm)],[141,8]),
[iquote('0:SSi:141.2,8.0')] ).
cnf(143,plain,
~ aNaturalNumber0(xk),
inference(mrr,[status(thm)],[142,38,21,20]),
[iquote('0:MRR:142.1,142.2,142.3,38.1,21.0,20.0')] ).
cnf(429,plain,
( ~ aNaturalNumber0(sdtpldt0(u,v))
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| sdtlseqdt0(u,sdtpldt0(u,v)) ),
inference(eqr,[status(thm),theory(equality)],[56]),
[iquote('0:EqR:56.3')] ).
cnf(435,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| sdtlseqdt0(u,sdtpldt0(u,v)) ),
inference(ssi,[status(thm)],[429,32]),
[iquote('0:SSi:429.0,32.2')] ).
cnf(929,plain,
( ~ aNaturalNumber0(sdtpldt0(u,v))
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| equal(sdtmndt0(sdtpldt0(u,v),u),v) ),
inference(eqr,[status(thm),theory(equality)],[87]),
[iquote('0:EqR:87.3')] ).
cnf(937,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| equal(sdtmndt0(sdtpldt0(u,v),u),v) ),
inference(ssi,[status(thm)],[929,32]),
[iquote('0:SSi:929.0,32.2')] ).
cnf(957,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(sdtpldt0(u,v))
| ~ aNaturalNumber0(u)
| ~ sdtlseqdt0(u,sdtpldt0(u,v))
| ~ equal(w,v)
| aNaturalNumber0(w) ),
inference(spl,[status(thm),theory(equality)],[937,57]),
[iquote('0:SpL:937.2,57.3')] ).
cnf(972,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(sdtpldt0(v,u))
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,sdtpldt0(v,u))
| ~ equal(w,u)
| aNaturalNumber0(w) ),
inference(obv,[status(thm),theory(equality)],[957]),
[iquote('0:Obv:957.0')] ).
cnf(973,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,sdtpldt0(v,u))
| ~ equal(w,u)
| aNaturalNumber0(w) ),
inference(ssi,[status(thm)],[972,32]),
[iquote('0:SSi:972.1,32.2')] ).
cnf(974,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ equal(w,u)
| aNaturalNumber0(w) ),
inference(mrr,[status(thm)],[973,435]),
[iquote('0:MRR:973.2,435.2')] ).
cnf(1081,plain,
( ~ aNaturalNumber0(u)
| ~ equal(v,u)
| aNaturalNumber0(v) ),
inference(ems,[status(thm)],[974,12]),
[iquote('0:EmS:974.1,12.0')] ).
cnf(1103,plain,
( ~ aNaturalNumber0(u)
| ~ equal(xk,u) ),
inference(sor,[status(thm)],[143,1081]),
[iquote('0:SoR:143.0,1081.2')] ).
cnf(1379,plain,
( ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| ~ equal(u,xk)
| aNaturalNumber0(u)
| equal(xp,sz00) ),
inference(spl,[status(thm),theory(equality)],[24,66]),
[iquote('0:SpL:24.0,66.3')] ).
cnf(1380,plain,
( ~ doDivides0(xp,sdtasdt0(xn,xm))
| ~ equal(u,xk)
| aNaturalNumber0(u)
| equal(xp,sz00) ),
inference(ssi,[status(thm)],[1379,6,5,33,3,4]),
[iquote('0:SSi:1379.1,1379.0,6.0,5.0,33.2,3.0,4.0')] ).
cnf(1381,plain,
~ equal(u,xk),
inference(mrr,[status(thm)],[1380,22,1103,114]),
[iquote('0:MRR:1380.0,1380.2,1380.3,22.0,1103.0,114.0')] ).
cnf(1382,plain,
$false,
inference(unc,[status(thm)],[1381,24]),
[iquote('0:UnC:1381.0,24.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Thu Jul 7 14:12:09 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.45/0.61
% 0.45/0.61 SPASS V 3.9
% 0.45/0.61 SPASS beiseite: Proof found.
% 0.45/0.61 % SZS status Theorem
% 0.45/0.61 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.61 SPASS derived 828 clauses, backtracked 19 clauses, performed 3 splits and kept 369 clauses.
% 0.45/0.61 SPASS allocated 98850 KBytes.
% 0.45/0.61 SPASS spent 0:00:00.24 on the problem.
% 0.45/0.61 0:00:00.04 for the input.
% 0.45/0.61 0:00:00.04 for the FLOTTER CNF translation.
% 0.45/0.61 0:00:00.01 for inferences.
% 0.45/0.61 0:00:00.00 for the backtracking.
% 0.45/0.61 0:00:00.13 for the reduction.
% 0.45/0.61
% 0.45/0.61
% 0.45/0.61 Here is a proof with depth 4, length 39 :
% 0.45/0.61 % SZS output start Refutation
% See solution above
% 0.45/0.61 Formulae used in the proof : m__1837 m__1860 mPrimDiv mDefLE m__2327 m__2306 m__ mSortsB mSortsB_02 mDefPrime mDefDiff mDefQuot
% 0.45/0.61
%------------------------------------------------------------------------------