%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM496+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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 0.19s 0.51s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of clauses : 47 ( 19 unt; 21 nHn; 47 RR)
% Number of literals : 128 ( 0 equ; 35 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 2 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
aNaturalNumber0(sz10),
file('NUM496+3.p',unknown),
[] ).
cnf(5,axiom,
aNaturalNumber0(xp),
file('NUM496+3.p',unknown),
[] ).
cnf(7,axiom,
isPrime0(xp),
file('NUM496+3.p',unknown),
[] ).
cnf(9,axiom,
aNaturalNumber0(xr),
file('NUM496+3.p',unknown),
[] ).
cnf(15,axiom,
aNaturalNumber0(skf10(u)),
file('NUM496+3.p',unknown),
[] ).
cnf(17,axiom,
aNaturalNumber0(skf11(u)),
file('NUM496+3.p',unknown),
[] ).
cnf(20,axiom,
~ doDivides0(xp,xn),
file('NUM496+3.p',unknown),
[] ).
cnf(21,axiom,
~ doDivides0(xp,xm),
file('NUM496+3.p',unknown),
[] ).
cnf(26,axiom,
~ equal(xp,sz00),
file('NUM496+3.p',unknown),
[] ).
cnf(27,axiom,
~ equal(xp,sz10),
file('NUM496+3.p',unknown),
[] ).
cnf(29,axiom,
( doDivides0(xp,xm)
| skC0 ),
file('NUM496+3.p',unknown),
[] ).
cnf(33,axiom,
equal(sdtpldt0(xp,xr),xn),
file('NUM496+3.p',unknown),
[] ).
cnf(37,axiom,
( ~ skC0
| doDivides0(xp,xr) ),
file('NUM496+3.p',unknown),
[] ).
cnf(55,axiom,
( ~ aNaturalNumber0(u)
| ~ isPrime0(u)
| ~ equal(u,sz10) ),
file('NUM496+3.p',unknown),
[] ).
cnf(59,axiom,
( ~ aNaturalNumber0(u)
| isPrime0(skf10(u))
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM496+3.p',unknown),
[] ).
cnf(60,axiom,
( skP1(u)
| equal(u,sz10)
| equal(u,sz00)
| doDivides0(skf11(u),u) ),
file('NUM496+3.p',unknown),
[] ).
cnf(65,axiom,
( ~ aNaturalNumber0(u)
| equal(u,sz10)
| equal(u,sz00)
| doDivides0(skf10(u),u) ),
file('NUM496+3.p',unknown),
[] ).
cnf(67,axiom,
( ~ equal(skf11(u),sz10)
| skP1(u)
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM496+3.p',unknown),
[] ).
cnf(69,axiom,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,xp)
| equal(u,xp)
| equal(u,sz10) ),
file('NUM496+3.p',unknown),
[] ).
cnf(98,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ doDivides0(w,u)
| ~ doDivides0(w,v)
| doDivides0(w,sdtpldt0(v,u)) ),
file('NUM496+3.p',unknown),
[] ).
cnf(116,plain,
skC0,
inference(mrr,[status(thm)],[29,21]),
[iquote('0:MRR:29.0,21.0')] ).
cnf(117,plain,
doDivides0(xp,xr),
inference(mrr,[status(thm)],[37,116]),
[iquote('0:MRR:37.0,116.0')] ).
cnf(132,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(xr)
| ~ doDivides0(xp,u)
| doDivides0(xp,sdtpldt0(u,xr)) ),
inference(res,[status(thm),theory(equality)],[117,98]),
[iquote('0:Res:117.0,98.4')] ).
cnf(202,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(xp,u)
| doDivides0(xp,sdtpldt0(u,xr)) ),
inference(mrr,[status(thm)],[132,5,9]),
[iquote('0:MRR:132.0,132.2,5.0,9.0')] ).
cnf(471,plain,
( ~ aNaturalNumber0(xp)
| ~ doDivides0(xp,xp)
| doDivides0(xp,xn) ),
inference(spr,[status(thm),theory(equality)],[33,202]),
[iquote('0:SpR:33.0,202.2')] ).
cnf(473,plain,
( ~ doDivides0(xp,xp)
| doDivides0(xp,xn) ),
inference(ssi,[status(thm)],[471,7,5]),
[iquote('0:SSi:471.0,7.0,5.0')] ).
cnf(474,plain,
~ doDivides0(xp,xp),
inference(mrr,[status(thm)],[473,20]),
[iquote('0:MRR:473.1,20.0')] ).
cnf(667,plain,
( ~ aNaturalNumber0(skf11(xp))
| skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00)
| equal(skf11(xp),xp)
| equal(skf11(xp),sz10) ),
inference(res,[status(thm),theory(equality)],[60,69]),
[iquote('0:Res:60.3,69.1')] ).
cnf(668,plain,
( skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00)
| equal(skf11(xp),xp)
| equal(skf11(xp),sz10) ),
inference(ssi,[status(thm)],[667,17,7,5]),
[iquote('0:SSi:667.0,17.0,7.0,5.0')] ).
cnf(669,plain,
( skP1(xp)
| equal(skf11(xp),xp)
| equal(skf11(xp),sz10) ),
inference(mrr,[status(thm)],[668,27,26]),
[iquote('0:MRR:668.1,668.2,27.0,26.0')] ).
cnf(672,plain,
( skP1(xp)
| equal(skf11(xp),sz10)
| skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00)
| doDivides0(xp,xp) ),
inference(spr,[status(thm),theory(equality)],[669,60]),
[iquote('0:SpR:669.1,60.3')] ).
cnf(674,plain,
( equal(skf11(xp),sz10)
| skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00)
| doDivides0(xp,xp) ),
inference(obv,[status(thm),theory(equality)],[672]),
[iquote('0:Obv:672.0')] ).
cnf(675,plain,
( equal(skf11(xp),sz10)
| skP1(xp) ),
inference(mrr,[status(thm)],[674,27,26,474]),
[iquote('0:MRR:674.2,674.3,674.4,27.0,26.0,474.0')] ).
cnf(682,plain,
( ~ equal(sz10,sz10)
| skP1(xp)
| skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00) ),
inference(spl,[status(thm),theory(equality)],[675,67]),
[iquote('0:SpL:675.0,67.0')] ).
cnf(683,plain,
( skP1(xp)
| equal(xp,sz10)
| equal(xp,sz00) ),
inference(obv,[status(thm),theory(equality)],[682]),
[iquote('0:Obv:682.1')] ).
cnf(684,plain,
skP1(xp),
inference(mrr,[status(thm)],[683,27,26]),
[iquote('0:MRR:683.1,683.2,27.0,26.0')] ).
cnf(700,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(skf10(xp))
| equal(xp,sz10)
| equal(xp,sz00)
| equal(skf10(xp),xp)
| equal(skf10(xp),sz10) ),
inference(res,[status(thm),theory(equality)],[65,69]),
[iquote('0:Res:65.3,69.1')] ).
cnf(707,plain,
( equal(xp,sz10)
| equal(xp,sz00)
| equal(skf10(xp),xp)
| equal(skf10(xp),sz10) ),
inference(ssi,[status(thm)],[700,15,7,5,684]),
[iquote('0:SSi:700.1,700.0,15.0,7.0,5.0,684.0,7.0,5.0,684.0')] ).
cnf(708,plain,
( equal(skf10(xp),xp)
| equal(skf10(xp),sz10) ),
inference(mrr,[status(thm)],[707,27,26]),
[iquote('0:MRR:707.0,707.1,27.0,26.0')] ).
cnf(722,plain,
( ~ aNaturalNumber0(xp)
| equal(skf10(xp),sz10)
| equal(xp,sz10)
| equal(xp,sz00)
| doDivides0(xp,xp) ),
inference(spr,[status(thm),theory(equality)],[708,65]),
[iquote('0:SpR:708.0,65.3')] ).
cnf(724,plain,
( equal(skf10(xp),sz10)
| equal(xp,sz10)
| equal(xp,sz00)
| doDivides0(xp,xp) ),
inference(ssi,[status(thm)],[722,7,5,684]),
[iquote('0:SSi:722.0,7.0,5.0,684.0')] ).
cnf(725,plain,
equal(skf10(xp),sz10),
inference(mrr,[status(thm)],[724,27,26,474]),
[iquote('0:MRR:724.1,724.2,724.3,27.0,26.0,474.0')] ).
cnf(727,plain,
( ~ aNaturalNumber0(xp)
| isPrime0(sz10)
| equal(xp,sz10)
| equal(xp,sz00) ),
inference(spr,[status(thm),theory(equality)],[725,59]),
[iquote('0:SpR:725.0,59.1')] ).
cnf(730,plain,
( isPrime0(sz10)
| equal(xp,sz10)
| equal(xp,sz00) ),
inference(ssi,[status(thm)],[727,7,5,684]),
[iquote('0:SSi:727.0,7.0,5.0,684.0')] ).
cnf(731,plain,
isPrime0(sz10),
inference(mrr,[status(thm)],[730,27,26]),
[iquote('0:MRR:730.1,730.2,27.0,26.0')] ).
cnf(737,plain,
~ equal(sz10,sz10),
inference(ems,[status(thm)],[55,2,731]),
[iquote('0:EmS:55.0,55.1,2.0,731.0')] ).
cnf(738,plain,
$false,
inference(obv,[status(thm),theory(equality)],[737]),
[iquote('0:Obv:737.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM496+3 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Tue Jul 5 07:29:12 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.51
% 0.19/0.51 SPASS V 3.9
% 0.19/0.51 SPASS beiseite: Proof found.
% 0.19/0.51 % SZS status Theorem
% 0.19/0.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.51 SPASS derived 503 clauses, backtracked 112 clauses, performed 3 splits and kept 414 clauses.
% 0.19/0.51 SPASS allocated 98112 KBytes.
% 0.19/0.51 SPASS spent 0:00:00.15 on the problem.
% 0.19/0.51 0:00:00.04 for the input.
% 0.19/0.51 0:00:00.04 for the FLOTTER CNF translation.
% 0.19/0.51 0:00:00.01 for inferences.
% 0.19/0.51 0:00:00.00 for the backtracking.
% 0.19/0.51 0:00:00.04 for the reduction.
% 0.19/0.51
% 0.19/0.51
% 0.19/0.51 Here is a proof with depth 4, length 47 :
% 0.19/0.51 % SZS output start Refutation
% See solution above
% 0.19/0.51 Formulae used in the proof : mSortsC_01 m__1837 m__1860 m__1883 mPrimDiv m__1913 m__1799 m__ m__2027 mDefPrime mDivSum
% 0.19/0.51
%------------------------------------------------------------------------------