%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM611+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:28:05 EDT 2022
% Result : Theorem 2.14s 2.36s
% Output : Refutation 2.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 35
% Syntax : Number of clauses : 86 ( 37 unt; 4 nHn; 86 RR)
% Number of literals : 182 ( 0 equ; 102 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 14 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
aSet0(szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(3,axiom,
isCountable0(szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(6,axiom,
isCountable0(xS),
file('NUM611+1.p',unknown),
[] ).
cnf(7,axiom,
aFunction0(xc),
file('NUM611+1.p',unknown),
[] ).
cnf(8,axiom,
aFunction0(xN),
file('NUM611+1.p',unknown),
[] ).
cnf(15,axiom,
aSet0(xP),
file('NUM611+1.p',unknown),
[] ).
cnf(16,axiom,
aElementOf0(sz00,szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(17,axiom,
aElementOf0(xK,szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(18,axiom,
aSubsetOf0(xS,szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(19,axiom,
aElementOf0(xk,szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(23,axiom,
aSubsetOf0(xQ,szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(24,axiom,
aElementOf0(xp,xQ),
file('NUM611+1.p',unknown),
[] ).
cnf(26,axiom,
aSubsetOf0(xP,xQ),
file('NUM611+1.p',unknown),
[] ).
cnf(33,axiom,
equal(szszuzczcdt0(xk),xK),
file('NUM611+1.p',unknown),
[] ).
cnf(34,axiom,
equal(szDzozmdt0(xN),szNzAzT0),
file('NUM611+1.p',unknown),
[] ).
cnf(43,axiom,
aElementOf0(xQ,szDzozmdt0(xc)),
file('NUM611+1.p',unknown),
[] ).
cnf(44,axiom,
equal(szmzizndt0(xQ),xp),
file('NUM611+1.p',unknown),
[] ).
cnf(45,axiom,
~ equal(sbrdtbr0(xP),xk),
file('NUM611+1.p',unknown),
[] ).
cnf(48,axiom,
equal(sdtlpdtrp0(xN,sz00),xS),
file('NUM611+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ aFunction0(u)
| aSet0(szDzozmdt0(u)) ),
file('NUM611+1.p',unknown),
[] ).
cnf(56,axiom,
equal(slbdtsldtrb0(xS,xK),szDzozmdt0(xc)),
file('NUM611+1.p',unknown),
[] ).
cnf(60,axiom,
equal(sdtmndt0(xQ,szmzizndt0(xQ)),xP),
file('NUM611+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(u)) ),
file('NUM611+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('NUM611+1.p',unknown),
[] ).
cnf(76,axiom,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| aSet0(v) ),
file('NUM611+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(szszuzczcdt0(u),u) ),
file('NUM611+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ aSet0(u)
| ~ aElementOf0(sbrdtbr0(u),szNzAzT0)
| isFinite0(u) ),
file('NUM611+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ aSet0(u)
| ~ isFinite0(u)
| aElementOf0(sbrdtbr0(u),szNzAzT0) ),
file('NUM611+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| isFinite0(v) ),
file('NUM611+1.p',unknown),
[] ).
cnf(97,axiom,
( ~ aFunction0(u)
| ~ aElementOf0(v,szDzozmdt0(u))
| aElement0(sdtlpdtrp0(u,v)) ),
file('NUM611+1.p',unknown),
[] ).
cnf(114,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(v,u)
| sdtlseqdt0(szszuzczcdt0(u),v) ),
file('NUM611+1.p',unknown),
[] ).
cnf(129,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(v),szszuzczcdt0(u))
| sdtlseqdt0(v,u) ),
file('NUM611+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElementOf0(v,u)
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
file('NUM611+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ sdtlseqdt0(u,v)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(v,u) ),
file('NUM611+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,w)
| ~ aElementOf0(x,szNzAzT0)
| ~ equal(w,slbdtsldtrb0(u,x))
| equal(sbrdtbr0(v),x) ),
file('NUM611+1.p',unknown),
[] ).
cnf(207,plain,
equal(sdtmndt0(xQ,xp),xP),
inference(rew,[status(thm),theory(equality)],[44,60]),
[iquote('0:Rew:44.0,60.0')] ).
cnf(232,plain,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ sdtlseqdt0(sbrdtbr0(xP),xk)
| ~ sdtlseqdt0(xk,sbrdtbr0(xP))
| ~ aElementOf0(xk,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[140,45]),
[iquote('0:Res:140.4,45.0')] ).
cnf(245,plain,
( ~ sdtlseqdt0(xk,sbrdtbr0(xP))
| ~ sdtlseqdt0(sbrdtbr0(xP),xk)
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(mrr,[status(thm)],[232,19]),
[iquote('0:MRR:232.3,19.0')] ).
cnf(273,plain,
( ~ aElementOf0(xk,szNzAzT0)
| sdtlseqdt0(xk,xK) ),
inference(spr,[status(thm),theory(equality)],[33,69]),
[iquote('0:SpR:33.0,69.1')] ).
cnf(274,plain,
sdtlseqdt0(xk,xK),
inference(mrr,[status(thm)],[273,19]),
[iquote('0:MRR:273.0,19.0')] ).
cnf(312,plain,
~ equal(szszuzczcdt0(xk),xk),
inference(res,[status(thm),theory(equality)],[19,79]),
[iquote('0:Res:19.0,79.0')] ).
cnf(319,plain,
~ equal(xk,xK),
inference(rew,[status(thm),theory(equality)],[33,312]),
[iquote('0:Rew:33.0,312.0')] ).
cnf(333,plain,
( ~ aSet0(szDzozmdt0(xc))
| aElement0(xQ) ),
inference(res,[status(thm),theory(equality)],[43,74]),
[iquote('0:Res:43.0,74.1')] ).
cnf(345,plain,
aElement0(xQ),
inference(ssi,[status(thm)],[333,55,7]),
[iquote('0:SSi:333.0,55.0,7.1')] ).
cnf(350,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xQ) ),
inference(res,[status(thm),theory(equality)],[23,76]),
[iquote('0:Res:23.0,76.1')] ).
cnf(353,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xS) ),
inference(res,[status(thm),theory(equality)],[18,76]),
[iquote('0:Res:18.0,76.1')] ).
cnf(358,plain,
aSet0(xQ),
inference(ssi,[status(thm)],[350,3,2]),
[iquote('0:SSi:350.0,3.0,2.0')] ).
cnf(359,plain,
aSet0(xS),
inference(ssi,[status(thm)],[353,3,2]),
[iquote('0:SSi:353.0,3.0,2.0')] ).
cnf(561,plain,
( ~ aFunction0(xN)
| ~ aElementOf0(u,szNzAzT0)
| aElement0(sdtlpdtrp0(xN,u)) ),
inference(spl,[status(thm),theory(equality)],[34,97]),
[iquote('0:SpL:34.0,97.1')] ).
cnf(568,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElement0(sdtlpdtrp0(xN,u)) ),
inference(ssi,[status(thm)],[561,8]),
[iquote('0:SSi:561.0,8.0')] ).
cnf(577,plain,
( ~ isFinite0(xQ)
| ~ aSet0(xQ)
| isFinite0(xP) ),
inference(res,[status(thm),theory(equality)],[26,94]),
[iquote('0:Res:26.0,94.2')] ).
cnf(593,plain,
( ~ isFinite0(xQ)
| isFinite0(xP) ),
inference(ssi,[status(thm)],[577,345,358]),
[iquote('0:SSi:577.1,345.0,358.0')] ).
cnf(628,plain,
( ~ aElementOf0(sz00,szNzAzT0)
| aElement0(xS) ),
inference(spr,[status(thm),theory(equality)],[48,568]),
[iquote('0:SpR:48.0,568.1')] ).
cnf(629,plain,
aElement0(xS),
inference(mrr,[status(thm)],[628,16]),
[iquote('0:MRR:628.0,16.0')] ).
cnf(1039,plain,
( ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,xk)
| sdtlseqdt0(xK,u) ),
inference(spr,[status(thm),theory(equality)],[33,114]),
[iquote('0:SpR:33.0,114.3')] ).
cnf(1043,plain,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,xk)
| sdtlseqdt0(xK,u) ),
inference(mrr,[status(thm)],[1039,19]),
[iquote('0:MRR:1039.0,19.0')] ).
cnf(2422,plain,
( ~ isFinite0(xQ)
| ~ aSet0(xQ)
| ~ aElementOf0(xp,xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),sbrdtbr0(xQ)) ),
inference(spr,[status(thm),theory(equality)],[207,135]),
[iquote('0:SpR:207.0,135.3')] ).
cnf(2434,plain,
( ~ isFinite0(xQ)
| ~ aElementOf0(xp,xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),sbrdtbr0(xQ)) ),
inference(ssi,[status(thm)],[2422,345,358]),
[iquote('0:SSi:2422.1,345.0,358.0')] ).
cnf(2435,plain,
( ~ isFinite0(xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),sbrdtbr0(xQ)) ),
inference(mrr,[status(thm)],[2434,24]),
[iquote('0:MRR:2434.1,24.0')] ).
cnf(3891,plain,
( ~ aSet0(xS)
| ~ aElementOf0(u,v)
| ~ aElementOf0(xK,szNzAzT0)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(spl,[status(thm),theory(equality)],[56,160]),
[iquote('0:SpL:56.0,160.3')] ).
cnf(3892,plain,
( ~ aElementOf0(u,v)
| ~ aElementOf0(xK,szNzAzT0)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(ssi,[status(thm)],[3891,359,6,629]),
[iquote('0:SSi:3891.0,359.0,6.0,629.0')] ).
cnf(3893,plain,
( ~ aElementOf0(u,v)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(mrr,[status(thm)],[3892,17]),
[iquote('0:MRR:3892.1,17.0')] ).
cnf(7315,plain,
( ~ equal(szDzozmdt0(xc),szDzozmdt0(xc))
| equal(sbrdtbr0(xQ),xK) ),
inference(res,[status(thm),theory(equality)],[43,3893]),
[iquote('0:Res:43.0,3893.0')] ).
cnf(7334,plain,
equal(sbrdtbr0(xQ),xK),
inference(obv,[status(thm),theory(equality)],[7315]),
[iquote('0:Obv:7315.0')] ).
cnf(7336,plain,
( ~ isFinite0(xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),xK) ),
inference(rew,[status(thm),theory(equality)],[7334,2435]),
[iquote('0:Rew:7334.0,2435.1')] ).
cnf(7363,plain,
( ~ aSet0(xQ)
| ~ aElementOf0(xK,szNzAzT0)
| isFinite0(xQ) ),
inference(spl,[status(thm),theory(equality)],[7334,84]),
[iquote('0:SpL:7334.0,84.1')] ).
cnf(7368,plain,
( ~ aElementOf0(xK,szNzAzT0)
| isFinite0(xQ) ),
inference(ssi,[status(thm)],[7363,345,358]),
[iquote('0:SSi:7363.0,345.0,358.0')] ).
cnf(7369,plain,
isFinite0(xQ),
inference(mrr,[status(thm)],[7368,17]),
[iquote('0:MRR:7368.0,17.0')] ).
cnf(7370,plain,
isFinite0(xP),
inference(mrr,[status(thm)],[593,7369]),
[iquote('0:MRR:593.0,7369.0')] ).
cnf(7373,plain,
equal(szszuzczcdt0(sbrdtbr0(xP)),xK),
inference(mrr,[status(thm)],[7336,7369]),
[iquote('0:MRR:7336.0,7369.0')] ).
cnf(7484,plain,
( ~ sdtlseqdt0(xK,xk)
| ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(xK,szNzAzT0)
| equal(xk,xK) ),
inference(res,[status(thm),theory(equality)],[274,140]),
[iquote('0:Res:274.0,140.0')] ).
cnf(7485,plain,
( ~ sdtlseqdt0(xK,xk)
| equal(xk,xK) ),
inference(mrr,[status(thm)],[7484,19,17]),
[iquote('0:MRR:7484.1,7484.2,19.0,17.0')] ).
cnf(7486,plain,
~ sdtlseqdt0(xK,xk),
inference(mrr,[status(thm)],[7485,319]),
[iquote('0:MRR:7485.1,319.0')] ).
cnf(7508,plain,
( ~ aElementOf0(xk,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(u),xK)
| sdtlseqdt0(u,xk) ),
inference(spl,[status(thm),theory(equality)],[33,129]),
[iquote('0:SpL:33.0,129.2')] ).
cnf(7512,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(xk,szNzAzT0)
| ~ sdtlseqdt0(xK,szszuzczcdt0(u))
| sdtlseqdt0(xk,u) ),
inference(spl,[status(thm),theory(equality)],[33,129]),
[iquote('0:SpL:33.0,129.2')] ).
cnf(7517,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(u),xK)
| sdtlseqdt0(u,xk) ),
inference(mrr,[status(thm)],[7508,19]),
[iquote('0:MRR:7508.0,19.0')] ).
cnf(7518,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(xK,szszuzczcdt0(u))
| sdtlseqdt0(xk,u) ),
inference(mrr,[status(thm)],[7512,19]),
[iquote('0:MRR:7512.1,19.0')] ).
cnf(7996,plain,
( sdtlseqdt0(xK,xk)
| sdtlseqdt0(xK,xK) ),
inference(res,[status(thm),theory(equality)],[17,1043]),
[iquote('0:Res:17.0,1043.0')] ).
cnf(8022,plain,
sdtlseqdt0(xK,xK),
inference(mrr,[status(thm)],[7996,7486]),
[iquote('0:MRR:7996.0,7486.0')] ).
cnf(8608,plain,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ sdtlseqdt0(xK,xK)
| sdtlseqdt0(sbrdtbr0(xP),xk) ),
inference(spl,[status(thm),theory(equality)],[7373,7517]),
[iquote('0:SpL:7373.0,7517.1')] ).
cnf(8613,plain,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| sdtlseqdt0(sbrdtbr0(xP),xk) ),
inference(mrr,[status(thm)],[8608,8022]),
[iquote('0:MRR:8608.1,8022.0')] ).
cnf(8614,plain,
( ~ sdtlseqdt0(xk,sbrdtbr0(xP))
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(mrr,[status(thm)],[245,8613]),
[iquote('0:MRR:245.1,8613.1')] ).
cnf(8636,plain,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ sdtlseqdt0(xK,xK)
| sdtlseqdt0(xk,sbrdtbr0(xP)) ),
inference(spl,[status(thm),theory(equality)],[7373,7518]),
[iquote('0:SpL:7373.0,7518.1')] ).
cnf(8642,plain,
~ aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(mrr,[status(thm)],[8636,8022,8614]),
[iquote('0:MRR:8636.1,8636.2,8022.0,8614.0')] ).
cnf(8645,plain,
( ~ aSet0(xP)
| ~ isFinite0(xP) ),
inference(res,[status(thm),theory(equality)],[85,8642]),
[iquote('0:Res:85.2,8642.0')] ).
cnf(8646,plain,
$false,
inference(ssi,[status(thm)],[8645,15,7370]),
[iquote('0:SSi:8645.1,8645.0,15.0,7370.0,15.0,7370.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM611+1 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jul 5 09:42:37 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.14/2.36
% 2.14/2.36 SPASS V 3.9
% 2.14/2.36 SPASS beiseite: Proof found.
% 2.14/2.36 % SZS status Theorem
% 2.14/2.36 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.14/2.36 SPASS derived 6371 clauses, backtracked 821 clauses, performed 15 splits and kept 3452 clauses.
% 2.14/2.36 SPASS allocated 104782 KBytes.
% 2.14/2.36 SPASS spent 0:00:01.96 on the problem.
% 2.14/2.36 0:00:00.04 for the input.
% 2.14/2.36 0:00:00.24 for the FLOTTER CNF translation.
% 2.14/2.36 0:00:00.10 for inferences.
% 2.14/2.36 0:00:00.03 for the backtracking.
% 2.14/2.36 0:00:01.48 for the reduction.
% 2.14/2.36
% 2.14/2.36
% 2.14/2.36 Here is a proof with depth 3, length 86 :
% 2.14/2.36 % SZS output start Refutation
% See solution above
% 2.14/2.36 Formulae used in the proof : mNATSet m__3435 m__3453 m__3623 m__5164 mZeroNum m__3418 m__3533 m__5106 m__5173 m__5195 m__5116 m__5147 m__ mDomSet mLessSucc mEOfElem mDefSub mNatNSucc mCardNum mSubFSet mImgElm mLessTotal mSuccLess mCardDiff mLessASymm mDefSel
% 2.14/2.36
%------------------------------------------------------------------------------