%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM612+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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:06 EDT 2022
% Result : Theorem 1.99s 2.21s
% Output : Refutation 1.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 44
% Syntax : Number of clauses : 111 ( 50 unt; 7 nHn; 111 RR)
% Number of literals : 218 ( 0 equ; 114 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 17 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
aSet0(szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(3,axiom,
isCountable0(szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(6,axiom,
isCountable0(xS),
file('NUM612+1.p',unknown),
[] ).
cnf(7,axiom,
aFunction0(xc),
file('NUM612+1.p',unknown),
[] ).
cnf(8,axiom,
aFunction0(xN),
file('NUM612+1.p',unknown),
[] ).
cnf(10,axiom,
aFunction0(xe),
file('NUM612+1.p',unknown),
[] ).
cnf(13,axiom,
aSet0(xO),
file('NUM612+1.p',unknown),
[] ).
cnf(14,axiom,
isCountable0(xO),
file('NUM612+1.p',unknown),
[] ).
cnf(15,axiom,
aSet0(xP),
file('NUM612+1.p',unknown),
[] ).
cnf(16,axiom,
aElementOf0(sz00,szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(17,axiom,
aElementOf0(xK,szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(18,axiom,
aSubsetOf0(xS,szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(19,axiom,
aElementOf0(xk,szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(23,axiom,
aSubsetOf0(xQ,szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(24,axiom,
aElementOf0(xp,xQ),
file('NUM612+1.p',unknown),
[] ).
cnf(25,axiom,
aElementOf0(xp,xO),
file('NUM612+1.p',unknown),
[] ).
cnf(26,axiom,
aSubsetOf0(xP,xQ),
file('NUM612+1.p',unknown),
[] ).
cnf(29,axiom,
equal(slbdtrb0(sz00),slcrc0),
file('NUM612+1.p',unknown),
[] ).
cnf(34,axiom,
equal(szDzozmdt0(xN),szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(38,axiom,
equal(szDzozmdt0(xe),szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(41,axiom,
aElementOf0(skf50(u),szNzAzT0),
file('NUM612+1.p',unknown),
[] ).
cnf(43,axiom,
aElementOf0(xQ,szDzozmdt0(xc)),
file('NUM612+1.p',unknown),
[] ).
cnf(44,axiom,
equal(szmzizndt0(xQ),xp),
file('NUM612+1.p',unknown),
[] ).
cnf(47,axiom,
equal(sdtlpdtrp0(xN,sz00),xS),
file('NUM612+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ equal(u,slcrc0)
| aSet0(u) ),
file('NUM612+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ aSet0(u)
| aElement0(sbrdtbr0(u)) ),
file('NUM612+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ aFunction0(u)
| aSet0(szDzozmdt0(u)) ),
file('NUM612+1.p',unknown),
[] ).
cnf(55,axiom,
equal(slbdtsldtrb0(xS,xK),szDzozmdt0(xc)),
file('NUM612+1.p',unknown),
[] ).
cnf(59,axiom,
equal(sdtmndt0(xQ,szmzizndt0(xQ)),xP),
file('NUM612+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ aElementOf0(u,v)
| ~ equal(v,slcrc0) ),
file('NUM612+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('NUM612+1.p',unknown),
[] ).
cnf(75,axiom,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| aSet0(v) ),
file('NUM612+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ aElementOf0(u,szNzAzT0)
| equal(sbrdtbr0(slbdtrb0(u)),u) ),
file('NUM612+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ aSet0(u)
| ~ aElementOf0(sbrdtbr0(u),szNzAzT0)
| isFinite0(u) ),
file('NUM612+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ aSet0(u)
| ~ isFinite0(u)
| aElementOf0(sbrdtbr0(u),szNzAzT0) ),
file('NUM612+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ aElementOf0(u,xO)
| equal(sdtlpdtrp0(xe,skf50(u)),u) ),
file('NUM612+1.p',unknown),
[] ).
cnf(91,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(v,slbdtrb0(u))
| aSet0(v) ),
file('NUM612+1.p',unknown),
[] ).
cnf(93,axiom,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ equal(szszuzczcdt0(sbrdtbr0(xP)),sbrdtbr0(xQ)) ),
file('NUM612+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| isFinite0(v) ),
file('NUM612+1.p',unknown),
[] ).
cnf(97,axiom,
( ~ aFunction0(u)
| ~ aElementOf0(v,szDzozmdt0(u))
| aElement0(sdtlpdtrp0(u,v)) ),
file('NUM612+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,w)
| ~ aSubsetOf0(w,u)
| aElementOf0(v,u) ),
file('NUM612+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ aSet0(u)
| ~ aSet0(v)
| aSubsetOf0(v,u)
| aElementOf0(skf26(v,w),v) ),
file('NUM612+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElementOf0(v,u)
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
file('NUM612+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,w)
| ~ aElementOf0(x,szNzAzT0)
| ~ equal(w,slbdtsldtrb0(u,x))
| equal(sbrdtbr0(v),x) ),
file('NUM612+1.p',unknown),
[] ).
cnf(207,plain,
equal(sdtmndt0(xQ,xp),xP),
inference(rew,[status(thm),theory(equality)],[44,59]),
[iquote('0:Rew:44.0,59.0')] ).
cnf(283,plain,
( ~ aSet0(slbdtrb0(u))
| ~ aElementOf0(u,szNzAzT0)
| aElement0(u) ),
inference(spr,[status(thm),theory(equality)],[80,53]),
[iquote('0:SpR:80.1,53.1')] ).
cnf(312,plain,
( ~ aSet0(szDzozmdt0(xc))
| aElement0(xQ) ),
inference(res,[status(thm),theory(equality)],[43,73]),
[iquote('0:Res:43.0,73.1')] ).
cnf(323,plain,
aElement0(xQ),
inference(ssi,[status(thm)],[312,54,7]),
[iquote('0:SSi:312.0,54.0,7.1')] ).
cnf(328,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xQ) ),
inference(res,[status(thm),theory(equality)],[23,75]),
[iquote('0:Res:23.0,75.1')] ).
cnf(331,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xS) ),
inference(res,[status(thm),theory(equality)],[18,75]),
[iquote('0:Res:18.0,75.1')] ).
cnf(336,plain,
aSet0(xQ),
inference(ssi,[status(thm)],[328,3,2]),
[iquote('0:SSi:328.0,3.0,2.0')] ).
cnf(337,plain,
aSet0(xS),
inference(ssi,[status(thm)],[331,3,2]),
[iquote('0:SSi:331.0,3.0,2.0')] ).
cnf(419,plain,
( ~ aElementOf0(u,szNzAzT0)
| aSet0(slbdtrb0(u)) ),
inference(eqr,[status(thm),theory(equality)],[91]),
[iquote('0:EqR:91.1')] ).
cnf(421,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElement0(u) ),
inference(mrr,[status(thm)],[283,419]),
[iquote('0:MRR:283.0,419.1')] ).
cnf(528,plain,
( ~ aFunction0(xe)
| ~ aElementOf0(u,szNzAzT0)
| aElement0(sdtlpdtrp0(xe,u)) ),
inference(spl,[status(thm),theory(equality)],[38,97]),
[iquote('0:SpL:38.0,97.1')] ).
cnf(530,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(535,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElement0(sdtlpdtrp0(xe,u)) ),
inference(ssi,[status(thm)],[528,10]),
[iquote('0:SSi:528.0,10.0')] ).
cnf(537,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElement0(sdtlpdtrp0(xN,u)) ),
inference(ssi,[status(thm)],[530,8]),
[iquote('0:SSi:530.0,8.0')] ).
cnf(546,plain,
( ~ isFinite0(xQ)
| ~ aSet0(xQ)
| isFinite0(xP) ),
inference(res,[status(thm),theory(equality)],[26,94]),
[iquote('0:Res:26.0,94.2')] ).
cnf(562,plain,
( ~ isFinite0(xQ)
| isFinite0(xP) ),
inference(ssi,[status(thm)],[546,323,336]),
[iquote('0:SSi:546.1,323.0,336.0')] ).
cnf(582,plain,
( ~ aElementOf0(u,xO)
| ~ aElementOf0(skf50(u),szNzAzT0)
| aElement0(u) ),
inference(spr,[status(thm),theory(equality)],[85,535]),
[iquote('0:SpR:85.1,535.1')] ).
cnf(585,plain,
( ~ aElementOf0(u,xO)
| aElement0(u) ),
inference(mrr,[status(thm)],[582,41]),
[iquote('0:MRR:582.1,41.0')] ).
cnf(597,plain,
( ~ aElementOf0(sz00,szNzAzT0)
| aElement0(xS) ),
inference(spr,[status(thm),theory(equality)],[47,537]),
[iquote('0:SpR:47.0,537.1')] ).
cnf(598,plain,
aElement0(xS),
inference(mrr,[status(thm)],[597,16]),
[iquote('0:MRR:597.0,16.0')] ).
cnf(864,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| aSubsetOf0(szNzAzT0,u)
| aSet0(slbdtrb0(skf26(szNzAzT0,v))) ),
inference(res,[status(thm),theory(equality)],[105,419]),
[iquote('0:Res:105.3,419.0')] ).
cnf(865,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| aSubsetOf0(szNzAzT0,u)
| aElement0(skf26(szNzAzT0,v)) ),
inference(res,[status(thm),theory(equality)],[105,421]),
[iquote('0:Res:105.3,421.0')] ).
cnf(871,plain,
( ~ aSet0(u)
| ~ aSet0(xO)
| aSubsetOf0(xO,u)
| aElement0(skf26(xO,v)) ),
inference(res,[status(thm),theory(equality)],[105,585]),
[iquote('0:Res:105.3,585.0')] ).
cnf(873,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u)
| aElement0(skf26(szNzAzT0,v)) ),
inference(ssi,[status(thm)],[865,3,2]),
[iquote('0:SSi:865.1,3.0,2.0')] ).
cnf(875,plain,
( ~ aSet0(u)
| aSubsetOf0(xO,u)
| aElement0(skf26(xO,v)) ),
inference(ssi,[status(thm)],[871,14,13]),
[iquote('0:SSi:871.1,14.0,13.0')] ).
cnf(876,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u)
| aSet0(slbdtrb0(skf26(szNzAzT0,v))) ),
inference(ssi,[status(thm)],[864,3,2]),
[iquote('0:SSi:864.1,3.0,2.0')] ).
cnf(938,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(xO,u)
| aElementOf0(xp,u) ),
inference(res,[status(thm),theory(equality)],[25,104]),
[iquote('0:Res:25.0,104.1')] ).
cnf(940,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(szNzAzT0,u)
| aElementOf0(xk,u) ),
inference(res,[status(thm),theory(equality)],[19,104]),
[iquote('0:Res:19.0,104.1')] ).
cnf(942,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(szNzAzT0,u)
| aElementOf0(sz00,u) ),
inference(res,[status(thm),theory(equality)],[16,104]),
[iquote('0:Res:16.0,104.1')] ).
cnf(1077,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u) ),
inference(spt,[spt(split,[position(s1)])],[873]),
[iquote('1:Spt:873.0,873.1')] ).
cnf(1078,plain,
( ~ aSet0(u)
| aElementOf0(xk,u) ),
inference(mrr,[status(thm)],[940,1077]),
[iquote('1:MRR:940.1,1077.1')] ).
cnf(1326,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0) ),
inference(res,[status(thm),theory(equality)],[1078,65]),
[iquote('1:Res:1078.1,65.0')] ).
cnf(1331,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[1326,50]),
[iquote('1:MRR:1326.0,50.1')] ).
cnf(1332,plain,
$false,
inference(unc,[status(thm)],[1331,29]),
[iquote('1:UnC:1331.0,29.0')] ).
cnf(1337,plain,
aElement0(skf26(szNzAzT0,u)),
inference(spt,[spt(split,[position(s2)])],[873]),
[iquote('1:Spt:1332.0,873.2')] ).
cnf(1951,plain,
( ~ aSet0(u)
| aSubsetOf0(xO,u) ),
inference(spt,[spt(split,[position(s2s1)])],[875]),
[iquote('2:Spt:875.0,875.1')] ).
cnf(1952,plain,
( ~ aSet0(u)
| aElementOf0(xp,u) ),
inference(mrr,[status(thm)],[938,1951]),
[iquote('2:MRR:938.1,1951.1')] ).
cnf(2101,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0) ),
inference(res,[status(thm),theory(equality)],[1952,65]),
[iquote('2:Res:1952.1,65.0')] ).
cnf(2107,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[2101,50]),
[iquote('2:MRR:2101.0,50.1')] ).
cnf(2108,plain,
$false,
inference(unc,[status(thm)],[2107,29]),
[iquote('2:UnC:2107.0,29.0')] ).
cnf(2111,plain,
aElement0(skf26(xO,u)),
inference(spt,[spt(split,[position(s2s2)])],[875]),
[iquote('2:Spt:2108.0,875.2')] ).
cnf(2958,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u) ),
inference(spt,[spt(split,[position(s2s2s1)])],[876]),
[iquote('3:Spt:876.0,876.1')] ).
cnf(2959,plain,
( ~ aSet0(u)
| aElementOf0(sz00,u) ),
inference(mrr,[status(thm)],[942,2958]),
[iquote('3:MRR:942.1,2958.1')] ).
cnf(3357,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0) ),
inference(res,[status(thm),theory(equality)],[2959,65]),
[iquote('3:Res:2959.1,65.0')] ).
cnf(3364,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[3357,50]),
[iquote('3:MRR:3357.0,50.1')] ).
cnf(3365,plain,
$false,
inference(unc,[status(thm)],[3364,29]),
[iquote('3:UnC:3364.0,29.0')] ).
cnf(3371,plain,
aSet0(slbdtrb0(skf26(szNzAzT0,u))),
inference(spt,[spt(split,[position(s2s2s2)])],[876]),
[iquote('3:Spt:3365.0,876.2')] ).
cnf(3603,plain,
~ aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(spt,[spt(split,[position(s2s2s2s1)])],[93]),
[iquote('4:Spt:93.0')] ).
cnf(3605,plain,
( ~ aSet0(xP)
| ~ isFinite0(xP) ),
inference(res,[status(thm),theory(equality)],[84,3603]),
[iquote('4:Res:84.2,3603.0')] ).
cnf(3606,plain,
~ isFinite0(xP),
inference(ssi,[status(thm)],[3605,15]),
[iquote('4:SSi:3605.0,15.0')] ).
cnf(3608,plain,
~ isFinite0(xQ),
inference(mrr,[status(thm)],[562,3606]),
[iquote('4:MRR:562.1,3606.0')] ).
cnf(3836,plain,
( ~ aSet0(xS)
| ~ aElementOf0(u,v)
| ~ aElementOf0(xK,szNzAzT0)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(spl,[status(thm),theory(equality)],[55,160]),
[iquote('0:SpL:55.0,160.3')] ).
cnf(3837,plain,
( ~ aElementOf0(u,v)
| ~ aElementOf0(xK,szNzAzT0)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(ssi,[status(thm)],[3836,6,337,598]),
[iquote('0:SSi:3836.0,6.0,337.0,598.0')] ).
cnf(3838,plain,
( ~ aElementOf0(u,v)
| ~ equal(v,szDzozmdt0(xc))
| equal(sbrdtbr0(u),xK) ),
inference(mrr,[status(thm)],[3837,17]),
[iquote('0:MRR:3837.1,17.0')] ).
cnf(5062,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(8061,plain,
( ~ equal(szDzozmdt0(xc),szDzozmdt0(xc))
| equal(sbrdtbr0(xQ),xK) ),
inference(res,[status(thm),theory(equality)],[43,3838]),
[iquote('0:Res:43.0,3838.0')] ).
cnf(8089,plain,
equal(sbrdtbr0(xQ),xK),
inference(obv,[status(thm),theory(equality)],[8061]),
[iquote('0:Obv:8061.0')] ).
cnf(8117,plain,
( ~ aSet0(xQ)
| ~ aElementOf0(xK,szNzAzT0)
| isFinite0(xQ) ),
inference(spl,[status(thm),theory(equality)],[8089,83]),
[iquote('0:SpL:8089.0,83.1')] ).
cnf(8120,plain,
( ~ aElementOf0(xK,szNzAzT0)
| isFinite0(xQ) ),
inference(ssi,[status(thm)],[8117,323,336]),
[iquote('0:SSi:8117.0,323.0,336.0')] ).
cnf(8121,plain,
$false,
inference(mrr,[status(thm)],[8120,17,3608]),
[iquote('4:MRR:8120.0,8120.1,17.0,3608.0')] ).
cnf(8122,plain,
aElementOf0(sbrdtbr0(xP),szNzAzT0),
inference(spt,[spt(split,[position(s2s2s2sa)])],[8121,3603]),
[iquote('4:Spt:8121.0,93.0,3603.0')] ).
cnf(8123,plain,
~ equal(szszuzczcdt0(sbrdtbr0(xP)),sbrdtbr0(xQ)),
inference(spt,[spt(split,[position(s2s2s2s2)])],[93]),
[iquote('4:Spt:8121.0,93.1')] ).
cnf(8124,plain,
isFinite0(xQ),
inference(mrr,[status(thm)],[8120,17]),
[iquote('0:MRR:8120.0,17.0')] ).
cnf(8127,plain,
~ equal(szszuzczcdt0(sbrdtbr0(xP)),xK),
inference(rew,[status(thm),theory(equality)],[8089,8123]),
[iquote('4:Rew:8089.0,8123.0')] ).
cnf(8172,plain,
( ~ isFinite0(xQ)
| ~ aSet0(xQ)
| ~ aElementOf0(xp,xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),xK) ),
inference(rew,[status(thm),theory(equality)],[8089,5062]),
[iquote('0:Rew:8089.0,5062.3')] ).
cnf(8173,plain,
( ~ isFinite0(xQ)
| ~ aElementOf0(xp,xQ)
| equal(szszuzczcdt0(sbrdtbr0(xP)),xK) ),
inference(ssi,[status(thm)],[8172,323,336]),
[iquote('0:SSi:8172.1,323.0,336.0')] ).
cnf(8174,plain,
$false,
inference(mrr,[status(thm)],[8173,8124,24,8127]),
[iquote('4:MRR:8173.0,8173.1,8173.2,8124.0,24.0,8127.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM612+1 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jul 5 03:17:12 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.99/2.21
% 1.99/2.21 SPASS V 3.9
% 1.99/2.21 SPASS beiseite: Proof found.
% 1.99/2.21 % SZS status Theorem
% 1.99/2.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.99/2.21 SPASS derived 5972 clauses, backtracked 956 clauses, performed 13 splits and kept 3112 clauses.
% 1.99/2.21 SPASS allocated 104506 KBytes.
% 1.99/2.21 SPASS spent 0:00:01.80 on the problem.
% 1.99/2.21 0:00:00.04 for the input.
% 1.99/2.21 0:00:00.29 for the FLOTTER CNF translation.
% 1.99/2.21 0:00:00.09 for inferences.
% 1.99/2.21 0:00:00.03 for the backtracking.
% 1.99/2.21 0:00:01.28 for the reduction.
% 1.99/2.21
% 1.99/2.21
% 1.99/2.21 Here is a proof with depth 4, length 111 :
% 1.99/2.21 % SZS output start Refutation
% See solution above
% 1.99/2.21 Formulae used in the proof : mNATSet m__3435 m__3453 m__3623 m__4660 m__4908 m__5164 mZeroNum m__3418 m__3533 m__5106 m__5173 m__5182 m__5195 mSegZero m__4982 m__5116 m__5147 mDefEmp mCardS mDomSet mEOfElem mDefSub mCardSeg mCardNum mDefSeg m__ mSubFSet mImgElm mCardDiff mDefSel
% 1.99/2.21
%------------------------------------------------------------------------------