%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM587+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n013.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:27:49 EDT 2022
% Result : Theorem 2.05s 2.24s
% Output : Refutation 2.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 19
% Syntax : Number of clauses : 38 ( 17 unt; 0 nHn; 38 RR)
% Number of literals : 68 ( 0 equ; 32 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(8,axiom,
aFunction0(xc),
file('NUM587+3.p',unknown),
[] ).
cnf(11,axiom,
aSet0(xQ),
file('NUM587+3.p',unknown),
[] ).
cnf(15,axiom,
aElementOf0(xk,szNzAzT0),
file('NUM587+3.p',unknown),
[] ).
cnf(16,axiom,
aElementOf0(xi,szNzAzT0),
file('NUM587+3.p',unknown),
[] ).
cnf(17,axiom,
~ aElementOf0(xx,xT),
file('NUM587+3.p',unknown),
[] ).
cnf(26,axiom,
equal(sbrdtbr0(xQ),xk),
file('NUM587+3.p',unknown),
[] ).
cnf(27,axiom,
aElementOf0(skc85,szDzozmdt0(xc)),
file('NUM587+3.p',unknown),
[] ).
cnf(39,axiom,
( ~ aFunction0(u)
| aSet0(szDzozmdt0(u)) ),
file('NUM587+3.p',unknown),
[] ).
cnf(51,axiom,
equal(sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ),xx),
file('NUM587+3.p',unknown),
[] ).
cnf(61,axiom,
( ~ aElementOf0(u,szNzAzT0)
| aFunction0(sdtlpdtrp0(xC,u)) ),
file('NUM587+3.p',unknown),
[] ).
cnf(64,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('NUM587+3.p',unknown),
[] ).
cnf(78,axiom,
( ~ aSet0(u)
| ~ aElementOf0(sbrdtbr0(u),szNzAzT0)
| isFinite0(u) ),
file('NUM587+3.p',unknown),
[] ).
cnf(80,axiom,
( ~ aElementOf0(u,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(u,xT) ),
file('NUM587+3.p',unknown),
[] ).
cnf(102,axiom,
aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)),
file('NUM587+3.p',unknown),
[] ).
cnf(104,axiom,
equal(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),sdtlpdtrp0(xc,skc85)),
file('NUM587+3.p',unknown),
[] ).
cnf(144,axiom,
( ~ aFunction0(u)
| ~ aElementOf0(v,szDzozmdt0(u))
| aElementOf0(sdtlpdtrp0(u,v),sdtlcdtrc0(u,szDzozmdt0(u))) ),
file('NUM587+3.p',unknown),
[] ).
cnf(195,axiom,
( ~ aElementOf0(u,szNzAzT0)
| equal(slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,u),szmzizndt0(sdtlpdtrp0(xN,u))),xk),szDzozmdt0(sdtlpdtrp0(xC,u))) ),
file('NUM587+3.p',unknown),
[] ).
cnf(198,axiom,
( ~ aSet0(u)
| ~ aElementOf0(u,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,v),szmzizndt0(sdtlpdtrp0(xN,v))),xk))
| skP8(v,u) ),
file('NUM587+3.p',unknown),
[] ).
cnf(231,axiom,
( ~ skP8(u,v)
| ~ aElementOf0(u,szNzAzT0)
| equal(sdtlpdtrp0(xc,sdtpldt0(v,szmzizndt0(sdtlpdtrp0(xN,u)))),sdtlpdtrp0(sdtlpdtrp0(xC,u),v)) ),
file('NUM587+3.p',unknown),
[] ).
cnf(315,plain,
~ aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc))),
inference(res,[status(thm),theory(equality)],[80,17]),
[iquote('0:Res:80.1,17.0')] ).
cnf(479,plain,
( ~ aSet0(xQ)
| ~ aElementOf0(xk,szNzAzT0)
| isFinite0(xQ) ),
inference(spl,[status(thm),theory(equality)],[26,78]),
[iquote('0:SpL:26.0,78.1')] ).
cnf(486,plain,
( ~ aElementOf0(xk,szNzAzT0)
| isFinite0(xQ) ),
inference(ssi,[status(thm)],[479,11]),
[iquote('0:SSi:479.0,11.0')] ).
cnf(487,plain,
isFinite0(xQ),
inference(mrr,[status(thm)],[486,15]),
[iquote('0:MRR:486.0,15.0')] ).
cnf(5855,plain,
( ~ skP8(xi,xQ)
| ~ aElementOf0(xi,szNzAzT0)
| equal(sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ),sdtlpdtrp0(xc,skc85)) ),
inference(spr,[status(thm),theory(equality)],[231,104]),
[iquote('0:SpR:231.2,104.0')] ).
cnf(5862,plain,
( ~ skP8(xi,xQ)
| ~ aElementOf0(xi,szNzAzT0)
| equal(sdtlpdtrp0(xc,skc85),xx) ),
inference(rew,[status(thm),theory(equality)],[51,5855]),
[iquote('0:Rew:51.0,5855.2')] ).
cnf(5906,plain,
( ~ skP8(xi,xQ)
| equal(sdtlpdtrp0(xc,skc85),xx) ),
inference(mrr,[status(thm)],[5862,16]),
[iquote('0:MRR:5862.1,16.0')] ).
cnf(6669,plain,
( ~ aElementOf0(xi,szNzAzT0)
| aElementOf0(xQ,szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(spr,[status(thm),theory(equality)],[195,102]),
[iquote('0:SpR:195.1,102.0')] ).
cnf(6677,plain,
aElementOf0(xQ,szDzozmdt0(sdtlpdtrp0(xC,xi))),
inference(mrr,[status(thm)],[6669,16]),
[iquote('0:MRR:6669.0,16.0')] ).
cnf(6718,plain,
( ~ aSet0(szDzozmdt0(sdtlpdtrp0(xC,xi)))
| aElement0(xQ) ),
inference(res,[status(thm),theory(equality)],[6677,64]),
[iquote('0:Res:6677.0,64.1')] ).
cnf(6727,plain,
( ~ aFunction0(sdtlpdtrp0(xC,xi))
| aElement0(xQ) ),
inference(sor,[status(thm)],[6718,39]),
[iquote('0:SoR:6718.0,39.1')] ).
cnf(6732,plain,
( ~ aElementOf0(xi,szNzAzT0)
| aElement0(xQ) ),
inference(sor,[status(thm)],[6727,61]),
[iquote('0:SoR:6727.0,61.1')] ).
cnf(6733,plain,
aElement0(xQ),
inference(mrr,[status(thm)],[6732,16]),
[iquote('0:MRR:6732.0,16.0')] ).
cnf(6753,plain,
( ~ aSet0(xQ)
| skP8(xi,xQ) ),
inference(res,[status(thm),theory(equality)],[102,198]),
[iquote('0:Res:102.0,198.1')] ).
cnf(6754,plain,
skP8(xi,xQ),
inference(ssi,[status(thm)],[6753,11,487,6733]),
[iquote('0:SSi:6753.0,11.0,487.0,6733.0')] ).
cnf(6755,plain,
equal(sdtlpdtrp0(xc,skc85),xx),
inference(mrr,[status(thm)],[5906,6754]),
[iquote('0:MRR:5906.0,6754.0')] ).
cnf(6768,plain,
( ~ aFunction0(xc)
| ~ aElementOf0(skc85,szDzozmdt0(xc))
| aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(spr,[status(thm),theory(equality)],[6755,144]),
[iquote('0:SpR:6755.0,144.2')] ).
cnf(6771,plain,
( ~ aElementOf0(skc85,szDzozmdt0(xc))
| aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(ssi,[status(thm)],[6768,8]),
[iquote('0:SSi:6768.0,8.0')] ).
cnf(6772,plain,
$false,
inference(mrr,[status(thm)],[6771,27,315]),
[iquote('0:MRR:6771.0,6771.1,27.0,315.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUM587+3 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n013.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 : Tue Jul 5 21:57:29 EDT 2022
% 0.13/0.33 % CPUTime :
% 2.05/2.24
% 2.05/2.24 SPASS V 3.9
% 2.05/2.24 SPASS beiseite: Proof found.
% 2.05/2.24 % SZS status Theorem
% 2.05/2.24 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.05/2.24 SPASS derived 4961 clauses, backtracked 539 clauses, performed 9 splits and kept 2998 clauses.
% 2.05/2.24 SPASS allocated 103527 KBytes.
% 2.05/2.24 SPASS spent 0:00:01.86 on the problem.
% 2.05/2.24 0:00:00.04 for the input.
% 2.05/2.24 0:00:00.50 for the FLOTTER CNF translation.
% 2.05/2.24 0:00:00.07 for inferences.
% 2.05/2.24 0:00:00.03 for the backtracking.
% 2.05/2.24 0:00:01.15 for the reduction.
% 2.05/2.24
% 2.05/2.24
% 2.05/2.24 Here is a proof with depth 4, length 38 :
% 2.05/2.24 % SZS output start Refutation
% See solution above
% 2.05/2.24 Formulae used in the proof : m__3453 m__4263 m__4237 m__3533 m__4200 m__ mDomSet m__4151 mEOfElem mCardNum mImgRng
% 2.05/2.24
%------------------------------------------------------------------------------