%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM481+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.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:39 EDT 2022
% Result : Theorem 0.56s 0.74s
% Output : Refutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 22
% Syntax : Number of clauses : 71 ( 22 unt; 18 nHn; 71 RR)
% Number of literals : 194 ( 0 equ; 106 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
aNaturalNumber0(skc1),
file('NUM481+1.p',unknown),
[] ).
cnf(2,axiom,
aNaturalNumber0(sz00),
file('NUM481+1.p',unknown),
[] ).
cnf(3,axiom,
aNaturalNumber0(sz10),
file('NUM481+1.p',unknown),
[] ).
cnf(4,axiom,
aNaturalNumber0(skf4(u)),
file('NUM481+1.p',unknown),
[] ).
cnf(5,axiom,
aNaturalNumber0(skf7(u)),
file('NUM481+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(skc1,sz00),
file('NUM481+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(skc1,sz10),
file('NUM481+1.p',unknown),
[] ).
cnf(10,axiom,
aNaturalNumber0(skf6(u,v)),
file('NUM481+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ aNaturalNumber0(u)
| equal(sdtasdt0(u,sz10),u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ aNaturalNumber0(u)
| equal(sdtasdt0(sz00,u),sz00) ),
file('NUM481+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ isPrime0(u)
| ~ aNaturalNumber0(u)
| ~ doDivides0(u,skc1) ),
file('NUM481+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| aNaturalNumber0(sdtasdt0(v,u)) ),
file('NUM481+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ aNaturalNumber0(u)
| isPrime0(u)
| equal(u,sz10)
| equal(u,sz00)
| doDivides0(skf7(u),u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ aNaturalNumber0(u)
| ~ iLess0(u,skc1)
| isPrime0(skf4(u))
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM481+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ sdtlseqdt0(v,u)
| iLess0(v,u)
| equal(v,u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ doDivides0(v,u)
| sdtlseqdt0(v,u)
| equal(u,sz00) ),
file('NUM481+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ aNaturalNumber0(u)
| ~ equal(skf7(u),sz10)
| isPrime0(u)
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM481+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ aNaturalNumber0(u)
| ~ equal(skf7(u),u)
| isPrime0(u)
| equal(u,sz10)
| equal(u,sz00) ),
file('NUM481+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ aNaturalNumber0(u)
| ~ iLess0(u,skc1)
| equal(u,sz10)
| equal(u,sz00)
| doDivides0(skf4(u),u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ doDivides0(v,u)
| equal(sdtasdt0(v,skf6(v,u)),u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ equal(u,sdtasdt0(v,w))
| doDivides0(v,u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ doDivides0(v,u)
| ~ doDivides0(w,v)
| doDivides0(w,u) ),
file('NUM481+1.p',unknown),
[] ).
cnf(109,plain,
( ~ equal(skf7(skc1),sz10)
| equal(skc1,sz00)
| equal(skc1,sz10)
| isPrime0(skc1) ),
inference(res,[status(thm),theory(equality)],[1,36]),
[iquote('0:Res:1.0,36.0')] ).
cnf(110,plain,
( ~ equal(skf7(skc1),skc1)
| equal(skc1,sz00)
| equal(skc1,sz10)
| isPrime0(skc1) ),
inference(res,[status(thm),theory(equality)],[1,37]),
[iquote('0:Res:1.0,37.0')] ).
cnf(113,plain,
( doDivides0(skf7(skc1),skc1)
| equal(skc1,sz00)
| equal(skc1,sz10)
| isPrime0(skc1) ),
inference(res,[status(thm),theory(equality)],[1,32]),
[iquote('0:Res:1.0,32.0')] ).
cnf(121,plain,
( ~ isPrime0(skc1)
| ~ doDivides0(skc1,skc1) ),
inference(res,[status(thm),theory(equality)],[1,18]),
[iquote('0:Res:1.0,18.0')] ).
cnf(123,plain,
( ~ aNaturalNumber0(u)
| aNaturalNumber0(sdtasdt0(skc1,u)) ),
inference(res,[status(thm),theory(equality)],[1,20]),
[iquote('0:Res:1.0,20.0')] ).
cnf(131,plain,
equal(sdtasdt0(sz00,skc1),sz00),
inference(res,[status(thm),theory(equality)],[1,17]),
[iquote('0:Res:1.0,17.0')] ).
cnf(159,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ equal(u,sdtasdt0(skc1,v))
| doDivides0(skc1,u) ),
inference(res,[status(thm),theory(equality)],[1,45]),
[iquote('0:Res:1.0,45.1')] ).
cnf(162,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,skc1)
| equal(sdtasdt0(u,skf6(u,skc1)),skc1) ),
inference(res,[status(thm),theory(equality)],[1,41]),
[iquote('0:Res:1.0,41.1')] ).
cnf(164,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,skc1)
| sdtlseqdt0(u,skc1)
| equal(skc1,sz00) ),
inference(res,[status(thm),theory(equality)],[1,35]),
[iquote('0:Res:1.0,35.1')] ).
cnf(198,plain,
( isPrime0(skc1)
| doDivides0(skf7(skc1),skc1) ),
inference(mrr,[status(thm)],[113,6,7]),
[iquote('0:MRR:113.1,113.2,6.0,7.0')] ).
cnf(201,plain,
( ~ equal(skf7(skc1),sz10)
| isPrime0(skc1) ),
inference(mrr,[status(thm)],[109,6,7]),
[iquote('0:MRR:109.1,109.2,6.0,7.0')] ).
cnf(202,plain,
( ~ equal(skf7(skc1),skc1)
| isPrime0(skc1) ),
inference(mrr,[status(thm)],[110,6,7]),
[iquote('0:MRR:110.1,110.2,6.0,7.0')] ).
cnf(203,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,skc1)
| sdtlseqdt0(u,skc1) ),
inference(mrr,[status(thm)],[164,6]),
[iquote('0:MRR:164.3,6.0')] ).
cnf(216,plain,
isPrime0(skc1),
inference(spt,[spt(split,[position(s1)])],[198]),
[iquote('1:Spt:198.0')] ).
cnf(217,plain,
~ doDivides0(skc1,skc1),
inference(mrr,[status(thm)],[121,216]),
[iquote('1:MRR:121.0,216.0')] ).
cnf(622,plain,
( ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(skf6(sz00,skc1))
| ~ doDivides0(sz00,skc1)
| equal(skc1,sz00) ),
inference(spr,[status(thm),theory(equality)],[162,17]),
[iquote('0:SpR:162.2,17.1')] ).
cnf(816,plain,
( ~ aNaturalNumber0(sdtasdt0(skc1,u))
| ~ aNaturalNumber0(u)
| doDivides0(skc1,sdtasdt0(skc1,u)) ),
inference(eqr,[status(thm),theory(equality)],[159]),
[iquote('0:EqR:159.2')] ).
cnf(827,plain,
( ~ aNaturalNumber0(u)
| doDivides0(skc1,sdtasdt0(skc1,u)) ),
inference(ssi,[status(thm)],[816,123]),
[iquote('0:SSi:816.0,123.1')] ).
cnf(843,plain,
( ~ aNaturalNumber0(skc1)
| ~ aNaturalNumber0(sz10)
| doDivides0(skc1,skc1) ),
inference(spr,[status(thm),theory(equality)],[14,827]),
[iquote('0:SpR:14.1,827.1')] ).
cnf(853,plain,
doDivides0(skc1,skc1),
inference(ssi,[status(thm)],[843,3,216,1]),
[iquote('1:SSi:843.1,843.0,3.0,216.0,1.0')] ).
cnf(854,plain,
$false,
inference(mrr,[status(thm)],[853,217]),
[iquote('1:MRR:853.0,217.0')] ).
cnf(863,plain,
~ isPrime0(skc1),
inference(spt,[spt(split,[position(sa)])],[854,216]),
[iquote('1:Spt:854.0,198.0,216.0')] ).
cnf(864,plain,
doDivides0(skf7(skc1),skc1),
inference(spt,[spt(split,[position(s2)])],[198]),
[iquote('1:Spt:854.0,198.1')] ).
cnf(865,plain,
~ equal(skf7(skc1),skc1),
inference(mrr,[status(thm)],[202,863]),
[iquote('1:MRR:202.1,863.0')] ).
cnf(866,plain,
~ equal(skf7(skc1),sz10),
inference(mrr,[status(thm)],[201,863]),
[iquote('1:MRR:201.1,863.0')] ).
cnf(870,plain,
( ~ doDivides0(sz00,skc1)
| equal(skc1,sz00) ),
inference(ssi,[status(thm)],[622,10,2,1]),
[iquote('0:SSi:622.1,622.0,10.0,2.0,1.0,2.0')] ).
cnf(871,plain,
~ doDivides0(sz00,skc1),
inference(mrr,[status(thm)],[870,6]),
[iquote('0:MRR:870.1,6.0')] ).
cnf(886,plain,
( ~ aNaturalNumber0(skf7(skc1))
| sdtlseqdt0(skf7(skc1),skc1) ),
inference(res,[status(thm),theory(equality)],[864,203]),
[iquote('1:Res:864.0,203.1')] ).
cnf(889,plain,
sdtlseqdt0(skf7(skc1),skc1),
inference(ssi,[status(thm)],[886,5,1]),
[iquote('1:SSi:886.0,5.0,1.0')] ).
cnf(1206,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(skc1)
| ~ equal(u,sz00)
| doDivides0(sz00,u) ),
inference(spl,[status(thm),theory(equality)],[131,45]),
[iquote('0:SpL:131.0,45.3')] ).
cnf(1222,plain,
( ~ aNaturalNumber0(u)
| ~ equal(u,sz00)
| doDivides0(sz00,u) ),
inference(ssi,[status(thm)],[1206,1,2]),
[iquote('0:SSi:1206.2,1206.1,1.0,2.0')] ).
cnf(2014,plain,
( ~ aNaturalNumber0(skc1)
| ~ aNaturalNumber0(skf7(skc1))
| ~ aNaturalNumber0(u)
| ~ doDivides0(u,skf7(skc1))
| doDivides0(u,skc1) ),
inference(res,[status(thm),theory(equality)],[864,47]),
[iquote('1:Res:864.0,47.3')] ).
cnf(2034,plain,
( ~ aNaturalNumber0(u)
| ~ doDivides0(u,skf7(skc1))
| doDivides0(u,skc1) ),
inference(ssi,[status(thm)],[2014,5,1]),
[iquote('1:SSi:2014.1,2014.0,5.0,1.0,1.0')] ).
cnf(2184,plain,
( ~ aNaturalNumber0(skf7(skc1))
| ~ aNaturalNumber0(skf4(skf7(skc1)))
| ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz10)
| equal(skf7(skc1),sz00)
| doDivides0(skf4(skf7(skc1)),skc1) ),
inference(res,[status(thm),theory(equality)],[38,2034]),
[iquote('1:Res:38.4,2034.1')] ).
cnf(2185,plain,
( ~ aNaturalNumber0(skf7(skc1))
| ~ aNaturalNumber0(sz00)
| ~ equal(skf7(skc1),sz00)
| doDivides0(sz00,skc1) ),
inference(res,[status(thm),theory(equality)],[1222,2034]),
[iquote('1:Res:1222.2,2034.1')] ).
cnf(2189,plain,
( ~ equal(skf7(skc1),sz00)
| doDivides0(sz00,skc1) ),
inference(ssi,[status(thm)],[2185,2,5,1]),
[iquote('1:SSi:2185.1,2185.0,2.0,5.0,1.0')] ).
cnf(2190,plain,
~ equal(skf7(skc1),sz00),
inference(mrr,[status(thm)],[2189,871]),
[iquote('1:MRR:2189.1,871.0')] ).
cnf(2194,plain,
( ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz10)
| equal(skf7(skc1),sz00)
| doDivides0(skf4(skf7(skc1)),skc1) ),
inference(ssi,[status(thm)],[2184,4,5,1]),
[iquote('1:SSi:2184.1,2184.0,4.0,5.0,1.0,5.0,1.0')] ).
cnf(2195,plain,
( ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz00)
| doDivides0(skf4(skf7(skc1)),skc1) ),
inference(mrr,[status(thm)],[2194,866]),
[iquote('1:MRR:2194.1,866.0')] ).
cnf(2196,plain,
( ~ iLess0(skf7(skc1),skc1)
| doDivides0(skf4(skf7(skc1)),skc1) ),
inference(mrr,[status(thm)],[2195,2190]),
[iquote('1:MRR:2195.1,2190.0')] ).
cnf(2218,plain,
( ~ isPrime0(skf4(skf7(skc1)))
| ~ aNaturalNumber0(skf4(skf7(skc1)))
| ~ iLess0(skf7(skc1),skc1) ),
inference(res,[status(thm),theory(equality)],[2196,18]),
[iquote('1:Res:2196.1,18.2')] ).
cnf(2223,plain,
( ~ isPrime0(skf4(skf7(skc1)))
| ~ iLess0(skf7(skc1),skc1) ),
inference(ssi,[status(thm)],[2218,4,5,1]),
[iquote('1:SSi:2218.1,4.0,5.0,1.0')] ).
cnf(2239,plain,
( ~ aNaturalNumber0(skf7(skc1))
| ~ iLess0(skf7(skc1),skc1)
| ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz00)
| equal(skf7(skc1),sz10) ),
inference(sor,[status(thm)],[2223,33]),
[iquote('1:SoR:2223.0,33.2')] ).
cnf(2240,plain,
( ~ aNaturalNumber0(skf7(skc1))
| ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz00)
| equal(skf7(skc1),sz10) ),
inference(obv,[status(thm),theory(equality)],[2239]),
[iquote('1:Obv:2239.1')] ).
cnf(2241,plain,
( ~ iLess0(skf7(skc1),skc1)
| equal(skf7(skc1),sz00)
| equal(skf7(skc1),sz10) ),
inference(ssi,[status(thm)],[2240,5,1]),
[iquote('1:SSi:2240.0,5.0,1.0')] ).
cnf(2242,plain,
~ iLess0(skf7(skc1),skc1),
inference(mrr,[status(thm)],[2241,2190,866]),
[iquote('1:MRR:2241.1,2241.2,2190.0,866.0')] ).
cnf(2243,plain,
( ~ aNaturalNumber0(skc1)
| ~ aNaturalNumber0(skf7(skc1))
| ~ sdtlseqdt0(skf7(skc1),skc1)
| equal(skf7(skc1),skc1) ),
inference(res,[status(thm),theory(equality)],[34,2242]),
[iquote('1:Res:34.3,2242.0')] ).
cnf(2247,plain,
( ~ sdtlseqdt0(skf7(skc1),skc1)
| equal(skf7(skc1),skc1) ),
inference(ssi,[status(thm)],[2243,5,1]),
[iquote('1:SSi:2243.1,2243.0,5.0,1.0,1.0')] ).
cnf(2248,plain,
$false,
inference(mrr,[status(thm)],[2247,889,865]),
[iquote('1:MRR:2247.0,2247.1,889.0,865.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NUM481+1 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : run_spass %d %s
% 0.12/0.31 % Computer : n006.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Thu Jul 7 18:25:51 EDT 2022
% 0.12/0.32 % CPUTime :
% 0.56/0.74
% 0.56/0.74 SPASS V 3.9
% 0.56/0.74 SPASS beiseite: Proof found.
% 0.56/0.74 % SZS status Theorem
% 0.56/0.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.56/0.74 SPASS derived 1334 clauses, backtracked 35 clauses, performed 1 splits and kept 506 clauses.
% 0.56/0.74 SPASS allocated 99467 KBytes.
% 0.56/0.74 SPASS spent 0:00:00.38 on the problem.
% 0.56/0.74 0:00:00.04 for the input.
% 0.56/0.74 0:00:00.04 for the FLOTTER CNF translation.
% 0.56/0.74 0:00:00.01 for inferences.
% 0.56/0.74 0:00:00.00 for the backtracking.
% 0.56/0.74 0:00:00.22 for the reduction.
% 0.56/0.74
% 0.56/0.74
% 0.56/0.74 Here is a proof with depth 7, length 71 :
% 0.56/0.74 % SZS output start Refutation
% See solution above
% 0.56/0.74 Formulae used in the proof : m__ mSortsC_01 mSortsC mDefPrime mDefDiv m_MulUnit m_MulZero mSortsB_02 mIH_03 mDivLE mDivTrans
% 0.56/0.74
%------------------------------------------------------------------------------