%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM476+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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:35 EDT 2022
% Result : Theorem 0.47s 0.63s
% Output : Refutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of clauses : 28 ( 19 unt; 3 nHn; 28 RR)
% Number of literals : 37 ( 0 equ; 12 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 3 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(6,axiom,
aNaturalNumber0(xn),
file('NUM476+2.p',unknown),
[] ).
cnf(8,axiom,
aNaturalNumber0(skc4),
file('NUM476+2.p',unknown),
[] ).
cnf(10,axiom,
~ doDivides0(xl,xn),
file('NUM476+2.p',unknown),
[] ).
cnf(14,axiom,
equal(sdtasdt0(xl,skc4),xm),
file('NUM476+2.p',unknown),
[] ).
cnf(15,axiom,
doDivides0(xl,sdtpldt0(xm,xn)),
file('NUM476+2.p',unknown),
[] ).
cnf(17,axiom,
( aNaturalNumber0(sdtsldt0(xm,xl))
| equal(xl,sz00) ),
file('NUM476+2.p',unknown),
[] ).
cnf(20,axiom,
( ~ aNaturalNumber0(u)
| equal(sdtpldt0(sz00,u),u) ),
file('NUM476+2.p',unknown),
[] ).
cnf(24,axiom,
( ~ aNaturalNumber0(u)
| equal(sdtasdt0(sz00,u),sz00) ),
file('NUM476+2.p',unknown),
[] ).
cnf(26,axiom,
( ~ aNaturalNumber0(u)
| ~ equal(sdtasdt0(xl,u),xn) ),
file('NUM476+2.p',unknown),
[] ).
cnf(33,axiom,
( aNaturalNumber0(sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl)))
| equal(xl,sz00) ),
file('NUM476+2.p',unknown),
[] ).
cnf(43,axiom,
( equal(xl,sz00)
| equal(sdtasdt0(xl,sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl))),xn) ),
file('NUM476+2.p',unknown),
[] ).
cnf(577,plain,
equal(xl,sz00),
inference(spt,[spt(split,[position(s1)])],[17]),
[iquote('1:Spt:17.1')] ).
cnf(581,plain,
~ doDivides0(sz00,xn),
inference(rew,[status(thm),theory(equality)],[577,10]),
[iquote('1:Rew:577.0,10.0')] ).
cnf(582,plain,
doDivides0(sz00,sdtpldt0(xm,xn)),
inference(rew,[status(thm),theory(equality)],[577,15]),
[iquote('1:Rew:577.0,15.0')] ).
cnf(583,plain,
equal(sdtasdt0(sz00,skc4),xm),
inference(rew,[status(thm),theory(equality)],[577,14]),
[iquote('1:Rew:577.0,14.0')] ).
cnf(606,plain,
( ~ aNaturalNumber0(skc4)
| equal(xm,sz00) ),
inference(spr,[status(thm),theory(equality)],[583,24]),
[iquote('1:SpR:583.0,24.1')] ).
cnf(608,plain,
equal(xm,sz00),
inference(ssi,[status(thm)],[606,8]),
[iquote('1:SSi:606.0,8.0')] ).
cnf(612,plain,
doDivides0(sz00,sdtpldt0(sz00,xn)),
inference(rew,[status(thm),theory(equality)],[608,582]),
[iquote('1:Rew:608.0,582.0')] ).
cnf(617,plain,
( ~ aNaturalNumber0(xn)
| doDivides0(sz00,xn) ),
inference(spr,[status(thm),theory(equality)],[20,612]),
[iquote('1:SpR:20.1,612.0')] ).
cnf(618,plain,
doDivides0(sz00,xn),
inference(ssi,[status(thm)],[617,6]),
[iquote('1:SSi:617.0,6.0')] ).
cnf(619,plain,
$false,
inference(mrr,[status(thm)],[618,581]),
[iquote('1:MRR:618.0,581.0')] ).
cnf(620,plain,
~ equal(xl,sz00),
inference(spt,[spt(split,[position(sa)])],[619,577]),
[iquote('1:Spt:619.0,17.1,577.0')] ).
cnf(621,plain,
aNaturalNumber0(sdtsldt0(xm,xl)),
inference(spt,[spt(split,[position(s2)])],[17]),
[iquote('1:Spt:619.0,17.0')] ).
cnf(625,plain,
aNaturalNumber0(sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl))),
inference(mrr,[status(thm)],[33,620]),
[iquote('1:MRR:33.1,620.0')] ).
cnf(628,plain,
equal(sdtasdt0(xl,sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl))),xn),
inference(mrr,[status(thm)],[43,620]),
[iquote('1:MRR:43.0,620.0')] ).
cnf(1058,plain,
( ~ aNaturalNumber0(sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl)))
| ~ equal(xn,xn) ),
inference(spl,[status(thm),theory(equality)],[628,26]),
[iquote('1:SpL:628.0,26.1')] ).
cnf(1059,plain,
~ aNaturalNumber0(sdtmndt0(sdtsldt0(sdtpldt0(xm,xn),xl),sdtsldt0(xm,xl))),
inference(obv,[status(thm),theory(equality)],[1058]),
[iquote('1:Obv:1058.1')] ).
cnf(1060,plain,
$false,
inference(ssi,[status(thm)],[1059,625]),
[iquote('1:SSi:1059.0,625.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NUM476+2 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Thu Jul 7 09:14:56 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.47/0.63
% 0.47/0.63 SPASS V 3.9
% 0.47/0.63 SPASS beiseite: Proof found.
% 0.47/0.63 % SZS status Theorem
% 0.47/0.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.63 SPASS derived 673 clauses, backtracked 291 clauses, performed 6 splits and kept 698 clauses.
% 0.47/0.63 SPASS allocated 98420 KBytes.
% 0.47/0.63 SPASS spent 0:00:00.28 on the problem.
% 0.47/0.63 0:00:00.04 for the input.
% 0.47/0.63 0:00:00.04 for the FLOTTER CNF translation.
% 0.47/0.63 0:00:00.01 for inferences.
% 0.47/0.63 0:00:00.00 for the backtracking.
% 0.47/0.63 0:00:00.14 for the reduction.
% 0.47/0.63
% 0.47/0.63
% 0.47/0.63 Here is a proof with depth 1, length 28 :
% 0.47/0.63 % SZS output start Refutation
% See solution above
% 0.47/0.63 Formulae used in the proof : m__1324 m__1324_04 m__ m_AddZero m_MulZero
% 0.47/0.63
%------------------------------------------------------------------------------