%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM466+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:29 EDT 2022
% Result : Theorem 2.16s 2.34s
% Output : Refutation 2.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of clauses : 18 ( 8 unt; 0 nHn; 18 RR)
% Number of literals : 41 ( 0 equ; 24 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
aNaturalNumber0(skc3),
file('NUM466+2.p',unknown),
[] ).
cnf(2,axiom,
aNaturalNumber0(skc2),
file('NUM466+2.p',unknown),
[] ).
cnf(5,axiom,
aNaturalNumber0(xl),
file('NUM466+2.p',unknown),
[] ).
cnf(10,axiom,
~ doDivides0(xl,xn),
file('NUM466+2.p',unknown),
[] ).
cnf(14,axiom,
equal(sdtasdt0(xl,skc2),xm),
file('NUM466+2.p',unknown),
[] ).
cnf(15,axiom,
equal(sdtasdt0(xm,skc3),xn),
file('NUM466+2.p',unknown),
[] ).
cnf(25,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| aNaturalNumber0(sdtasdt0(v,u)) ),
file('NUM466+2.p',unknown),
[] ).
cnf(42,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| ~ equal(u,sdtasdt0(v,w))
| doDivides0(v,u) ),
file('NUM466+2.p',unknown),
[] ).
cnf(46,axiom,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| ~ aNaturalNumber0(w)
| equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u))) ),
file('NUM466+2.p',unknown),
[] ).
cnf(1395,plain,
( ~ aNaturalNumber0(sdtasdt0(u,v))
| ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| doDivides0(u,sdtasdt0(u,v)) ),
inference(eqr,[status(thm),theory(equality)],[42]),
[iquote('0:EqR:42.3')] ).
cnf(1413,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(v)
| doDivides0(u,sdtasdt0(u,v)) ),
inference(ssi,[status(thm)],[1395,25]),
[iquote('0:SSi:1395.0,25.2')] ).
cnf(1589,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(skc2)
| ~ aNaturalNumber0(xl)
| equal(sdtasdt0(xl,sdtasdt0(skc2,u)),sdtasdt0(xm,u)) ),
inference(spr,[status(thm),theory(equality)],[14,46]),
[iquote('0:SpR:14.0,46.3')] ).
cnf(1604,plain,
( ~ aNaturalNumber0(u)
| equal(sdtasdt0(xl,sdtasdt0(skc2,u)),sdtasdt0(xm,u)) ),
inference(ssi,[status(thm)],[1589,5,2]),
[iquote('0:SSi:1589.2,1589.1,5.0,2.0')] ).
cnf(7000,plain,
( ~ aNaturalNumber0(u)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(sdtasdt0(skc2,u))
| doDivides0(xl,sdtasdt0(xm,u)) ),
inference(spr,[status(thm),theory(equality)],[1604,1413]),
[iquote('0:SpR:1604.1,1413.2')] ).
cnf(7036,plain,
( ~ aNaturalNumber0(u)
| doDivides0(xl,sdtasdt0(xm,u)) ),
inference(ssi,[status(thm)],[7000,25,2,5]),
[iquote('0:SSi:7000.2,7000.1,25.0,2.0,5.2')] ).
cnf(7177,plain,
( ~ aNaturalNumber0(skc3)
| doDivides0(xl,xn) ),
inference(spr,[status(thm),theory(equality)],[15,7036]),
[iquote('0:SpR:15.0,7036.1')] ).
cnf(7193,plain,
doDivides0(xl,xn),
inference(ssi,[status(thm)],[7177,1]),
[iquote('0:SSi:7177.0,1.0')] ).
cnf(7194,plain,
$false,
inference(mrr,[status(thm)],[7193,10]),
[iquote('0:MRR:7193.0,10.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM466+2 : TPTP v8.1.0. Released v4.0.0.
% 0.07/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 : Wed Jul 6 08:10:27 EDT 2022
% 0.13/0.34 % CPUTime :
% 2.16/2.34
% 2.16/2.34 SPASS V 3.9
% 2.16/2.34 SPASS beiseite: Proof found.
% 2.16/2.34 % SZS status Theorem
% 2.16/2.34 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.16/2.34 SPASS derived 4632 clauses, backtracked 772 clauses, performed 11 splits and kept 2190 clauses.
% 2.16/2.34 SPASS allocated 103389 KBytes.
% 2.16/2.34 SPASS spent 0:00:01.70 on the problem.
% 2.16/2.34 0:00:00.04 for the input.
% 2.16/2.34 0:00:00.04 for the FLOTTER CNF translation.
% 2.16/2.34 0:00:00.04 for inferences.
% 2.16/2.34 0:00:00.03 for the backtracking.
% 2.16/2.34 0:00:01.49 for the reduction.
% 2.16/2.34
% 2.16/2.34
% 2.16/2.34 Here is a proof with depth 3, length 18 :
% 2.16/2.34 % SZS output start Refutation
% See solution above
% 2.16/2.34 Formulae used in the proof : m__ m__1218 mSortsB_02 mDefDiv mMulAsso
% 2.16/2.34
%------------------------------------------------------------------------------