%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM539+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:16 EDT 2022
% Result : Theorem 0.77s 0.96s
% Output : Refutation 0.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 40
% Syntax : Number of clauses : 186 ( 45 unt; 35 nHn; 186 RR)
% Number of literals : 526 ( 0 equ; 331 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
isFinite0(slcrc0),
file('NUM539+1.p',unknown),
[] ).
cnf(2,axiom,
aSet0(szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(3,axiom,
isCountable0(szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(4,axiom,
aElementOf0(sz00,szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(5,axiom,
aSubsetOf0(xS,szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(6,axiom,
aSubsetOf0(xT,szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(7,axiom,
aElementOf0(skf12(u),szNzAzT0),
file('NUM539+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(xS,slcrc0),
file('NUM539+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(xT,slcrc0),
file('NUM539+1.p',unknown),
[] ).
cnf(10,axiom,
aElementOf0(szmzizndt0(xS),xT),
file('NUM539+1.p',unknown),
[] ).
cnf(11,axiom,
aElementOf0(szmzizndt0(xT),xS),
file('NUM539+1.p',unknown),
[] ).
cnf(12,axiom,
~ equal(szmzizndt0(xT),szmzizndt0(xS)),
file('NUM539+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ equal(u,slcrc0)
| aSet0(u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ aSet0(u)
| aSubsetOf0(u,u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ aElementOf0(u,v)
| ~ equal(v,slcrc0) ),
file('NUM539+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ aElementOf0(u,szNzAzT0)
| aElementOf0(szszuzczcdt0(u),szNzAzT0) ),
file('NUM539+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(u)) ),
file('NUM539+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| aSet0(v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(u),sz00) ),
file('NUM539+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ aSet0(u)
| equal(u,slcrc0)
| aElementOf0(skf8(u),u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ aSet0(u)
| ~ aElementOf0(sbrdtbr0(u),szNzAzT0)
| isFinite0(u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ aSet0(u)
| ~ isFinite0(u)
| aElementOf0(sbrdtbr0(u),szNzAzT0) ),
file('NUM539+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ aSet0(u)
| ~ equal(u,slcrc0)
| equal(sbrdtbr0(u),sz00) ),
file('NUM539+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00)
| equal(szszuzczcdt0(skf12(u)),u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElement0(v)
| isFinite0(sdtpldt0(u,v)) ),
file('NUM539+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,w)
| ~ aSubsetOf0(w,u)
| aElementOf0(v,u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ aSet0(u)
| ~ aSet0(v)
| aSubsetOf0(v,u)
| aElementOf0(skf9(v,w),v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ aElement0(u)
| ~ aSet0(v)
| ~ equal(w,sdtpldt0(v,u))
| aSet0(w) ),
file('NUM539+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(v,u)
| sdtlseqdt0(szszuzczcdt0(u),v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| sdtlseqdt0(sbrdtbr0(v),sbrdtbr0(u)) ),
file('NUM539+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ aSubsetOf0(v,u)
| ~ aSubsetOf0(u,v)
| equal(u,v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(v),szszuzczcdt0(u))
| sdtlseqdt0(v,u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ sdtlseqdt0(u,v)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(v,u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ aElementOf0(u,v)
| ~ equal(w,szmzizndt0(v))
| ~ aSubsetOf0(v,szNzAzT0)
| sdtlseqdt0(w,u)
| equal(v,slcrc0) ),
file('NUM539+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElementOf0(v,szNzAzT0)
| ~ sdtlseqdt0(v,sbrdtbr0(u))
| aSubsetOf0(skf13(u,w),u) ),
file('NUM539+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ aElement0(u)
| ~ isFinite0(v)
| ~ aSet0(v)
| aElementOf0(u,v)
| equal(sbrdtbr0(sdtpldt0(v,u)),szszuzczcdt0(sbrdtbr0(v))) ),
file('NUM539+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ aSet0(w)
| ~ aSubsetOf0(u,v)
| ~ aSubsetOf0(v,w)
| aSubsetOf0(u,w) ),
file('NUM539+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ sdtlseqdt0(u,v)
| ~ sdtlseqdt0(w,u)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(w,szNzAzT0)
| sdtlseqdt0(w,v) ),
file('NUM539+1.p',unknown),
[] ).
cnf(84,plain,
( ~ equal(u,slcrc0)
| equal(sbrdtbr0(u),sz00) ),
inference(mrr,[status(thm)],[40,13]),
[iquote('0:MRR:40.0,13.1')] ).
cnf(85,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| ~ aSubsetOf0(u,v)
| equal(v,u) ),
inference(mrr,[status(thm)],[58,28]),
[iquote('0:MRR:58.0,28.2')] ).
cnf(86,plain,
( ~ aElementOf0(u,v)
| ~ aSubsetOf0(v,szNzAzT0)
| ~ equal(w,szmzizndt0(v))
| sdtlseqdt0(w,u) ),
inference(mrr,[status(thm)],[65,21]),
[iquote('0:MRR:65.4,21.1')] ).
cnf(88,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| ~ aSubsetOf0(w,v)
| aSubsetOf0(w,u) ),
inference(mrr,[status(thm)],[73,28]),
[iquote('0:MRR:73.0,73.1,28.2,28.2')] ).
cnf(100,plain,
( ~ aElementOf0(szmzizndt0(xT),szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0)
| ~ sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS))
| ~ sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)) ),
inference(res,[status(thm),theory(equality)],[64,12]),
[iquote('0:Res:64.4,12.0')] ).
cnf(124,plain,
( ~ aSet0(szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| aElement0(szszuzczcdt0(u)) ),
inference(res,[status(thm),theory(equality)],[23,26]),
[iquote('0:Res:23.1,26.1')] ).
cnf(128,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElement0(szszuzczcdt0(u)) ),
inference(ssi,[status(thm)],[124,3,2]),
[iquote('0:SSi:124.0,3.0,2.0')] ).
cnf(130,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xT) ),
inference(res,[status(thm),theory(equality)],[6,28]),
[iquote('0:Res:6.0,28.1')] ).
cnf(131,plain,
( ~ aSet0(szNzAzT0)
| aSet0(xS) ),
inference(res,[status(thm),theory(equality)],[5,28]),
[iquote('0:Res:5.0,28.1')] ).
cnf(133,plain,
aSet0(xT),
inference(ssi,[status(thm)],[130,3,2]),
[iquote('0:SSi:130.0,3.0,2.0')] ).
cnf(136,plain,
aSet0(xS),
inference(ssi,[status(thm)],[131,3,2]),
[iquote('0:SSi:131.0,3.0,2.0')] ).
cnf(148,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0)
| ~ aElementOf0(sz00,szNzAzT0)
| isFinite0(u) ),
inference(spl,[status(thm),theory(equality)],[84,34]),
[iquote('0:SpL:84.1,34.1')] ).
cnf(150,plain,
( ~ equal(u,slcrc0)
| isFinite0(u) ),
inference(mrr,[status(thm)],[148,13,4]),
[iquote('0:MRR:148.0,148.2,13.1,4.0')] ).
cnf(189,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(skf12(u),szNzAzT0)
| ~ sdtlseqdt0(u,sz00)
| equal(u,sz00) ),
inference(spl,[status(thm),theory(equality)],[42,32]),
[iquote('0:SpL:42.2,32.1')] ).
cnf(196,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(u,sz00)
| equal(u,sz00) ),
inference(mrr,[status(thm)],[189,7]),
[iquote('0:MRR:189.1,7.0')] ).
cnf(247,plain,
( ~ aElement0(u)
| ~ aSet0(v)
| aSet0(sdtpldt0(v,u)) ),
inference(eqr,[status(thm),theory(equality)],[49]),
[iquote('0:EqR:49.2')] ).
cnf(298,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(szNzAzT0,xT)
| equal(xT,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[6,85]),
[iquote('0:Res:6.0,85.1')] ).
cnf(299,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(szNzAzT0,xS)
| equal(xS,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[5,85]),
[iquote('0:Res:5.0,85.1')] ).
cnf(301,plain,
( ~ aSubsetOf0(szNzAzT0,xT)
| equal(xT,szNzAzT0) ),
inference(ssi,[status(thm)],[298,3,2]),
[iquote('0:SSi:298.0,3.0,2.0')] ).
cnf(302,plain,
( ~ aSubsetOf0(szNzAzT0,xS)
| equal(xS,szNzAzT0) ),
inference(ssi,[status(thm)],[299,3,2]),
[iquote('0:SSi:299.0,3.0,2.0')] ).
cnf(323,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| aSubsetOf0(szNzAzT0,u)
| aElement0(szszuzczcdt0(skf9(szNzAzT0,v))) ),
inference(res,[status(thm),theory(equality)],[48,128]),
[iquote('0:Res:48.3,128.0')] ).
cnf(326,plain,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ equal(v,slcrc0)
| aSubsetOf0(v,u) ),
inference(res,[status(thm),theory(equality)],[48,21]),
[iquote('0:Res:48.3,21.0')] ).
cnf(329,plain,
( ~ aSet0(u)
| ~ equal(v,slcrc0)
| aSubsetOf0(v,u) ),
inference(mrr,[status(thm)],[326,13]),
[iquote('0:MRR:326.1,13.1')] ).
cnf(330,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u)
| aElement0(szszuzczcdt0(skf9(szNzAzT0,v))) ),
inference(ssi,[status(thm)],[323,3,2]),
[iquote('0:SSi:323.1,3.0,2.0')] ).
cnf(347,plain,
( ~ aSet0(u)
| aSubsetOf0(szNzAzT0,u) ),
inference(spt,[spt(split,[position(s1)])],[330]),
[iquote('1:Spt:330.0,330.1')] ).
cnf(351,plain,
( ~ aSet0(xT)
| equal(xT,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[347,301]),
[iquote('1:Res:347.1,301.0')] ).
cnf(352,plain,
( ~ aSet0(xS)
| equal(xS,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[347,302]),
[iquote('1:Res:347.1,302.0')] ).
cnf(353,plain,
equal(xT,szNzAzT0),
inference(ssi,[status(thm)],[351,133]),
[iquote('1:SSi:351.0,133.0')] ).
cnf(355,plain,
aElementOf0(szmzizndt0(szNzAzT0),xS),
inference(rew,[status(thm),theory(equality)],[353,11]),
[iquote('1:Rew:353.0,11.0')] ).
cnf(369,plain,
( ~ aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0)
| ~ sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS))
| ~ sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)) ),
inference(rew,[status(thm),theory(equality)],[353,100]),
[iquote('1:Rew:353.0,100.0')] ).
cnf(370,plain,
equal(xS,szNzAzT0),
inference(ssi,[status(thm)],[352,136]),
[iquote('1:SSi:352.0,136.0')] ).
cnf(377,plain,
aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0),
inference(rew,[status(thm),theory(equality)],[370,355]),
[iquote('1:Rew:370.0,355.0')] ).
cnf(392,plain,
( ~ aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)
| ~ aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)
| ~ sdtlseqdt0(szmzizndt0(szNzAzT0),szmzizndt0(szNzAzT0))
| ~ sdtlseqdt0(szmzizndt0(szNzAzT0),szmzizndt0(szNzAzT0)) ),
inference(rew,[status(thm),theory(equality)],[370,369,353]),
[iquote('1:Rew:370.0,369.3,353.0,369.3,353.0,369.2,370.0,369.2,370.0,369.1')] ).
cnf(393,plain,
( ~ aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0)
| ~ sdtlseqdt0(szmzizndt0(szNzAzT0),szmzizndt0(szNzAzT0)) ),
inference(obv,[status(thm),theory(equality)],[392]),
[iquote('1:Obv:392.2')] ).
cnf(394,plain,
~ aElementOf0(szmzizndt0(szNzAzT0),szNzAzT0),
inference(mrr,[status(thm)],[393,20]),
[iquote('1:MRR:393.1,20.1')] ).
cnf(395,plain,
$false,
inference(mrr,[status(thm)],[394,377]),
[iquote('1:MRR:394.0,377.0')] ).
cnf(396,plain,
aElement0(szszuzczcdt0(skf9(szNzAzT0,u))),
inference(spt,[spt(split,[position(s2)])],[330]),
[iquote('1:Spt:395.0,330.2')] ).
cnf(428,plain,
( ~ aSet0(u)
| ~ aSet0(u)
| ~ equal(v,slcrc0)
| ~ aSubsetOf0(w,v)
| aSubsetOf0(w,u) ),
inference(res,[status(thm),theory(equality)],[329,88]),
[iquote('0:Res:329.2,88.1')] ).
cnf(434,plain,
( ~ aSet0(u)
| ~ equal(v,slcrc0)
| ~ aSubsetOf0(w,v)
| aSubsetOf0(w,u) ),
inference(obv,[status(thm),theory(equality)],[428]),
[iquote('0:Obv:428.0')] ).
cnf(448,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(szNzAzT0,u)
| aElementOf0(sz00,u) ),
inference(res,[status(thm),theory(equality)],[4,47]),
[iquote('0:Res:4.0,47.1')] ).
cnf(452,plain,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ aSet0(w)
| ~ aSubsetOf0(v,w)
| aSubsetOf0(v,u)
| aElementOf0(skf9(v,x),w) ),
inference(res,[status(thm),theory(equality)],[48,47]),
[iquote('0:Res:48.3,47.1')] ).
cnf(453,plain,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ aSubsetOf0(u,v)
| equal(u,slcrc0)
| aElementOf0(skf8(u),v) ),
inference(res,[status(thm),theory(equality)],[33,47]),
[iquote('0:Res:33.2,47.1')] ).
cnf(454,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(xT,u)
| aElementOf0(szmzizndt0(xS),u) ),
inference(res,[status(thm),theory(equality)],[10,47]),
[iquote('0:Res:10.0,47.1')] ).
cnf(455,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(xS,u)
| aElementOf0(szmzizndt0(xT),u) ),
inference(res,[status(thm),theory(equality)],[11,47]),
[iquote('0:Res:11.0,47.1')] ).
cnf(456,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| equal(v,slcrc0)
| aElementOf0(skf8(v),u) ),
inference(mrr,[status(thm)],[453,28]),
[iquote('0:MRR:453.0,28.2')] ).
cnf(457,plain,
( ~ aSet0(u)
| ~ aSet0(v)
| ~ aSubsetOf0(w,v)
| aSubsetOf0(w,u)
| aElementOf0(skf9(w,x),v) ),
inference(mrr,[status(thm)],[452,28]),
[iquote('0:MRR:452.1,28.2')] ).
cnf(460,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| ~ aSet0(u)
| aElementOf0(skf9(szNzAzT0,v),szNzAzT0)
| aElementOf0(sz00,u) ),
inference(res,[status(thm),theory(equality)],[48,448]),
[iquote('0:Res:48.2,448.1')] ).
cnf(464,plain,
( ~ aSet0(szNzAzT0)
| ~ aSet0(u)
| aElementOf0(skf9(szNzAzT0,v),szNzAzT0)
| aElementOf0(sz00,u) ),
inference(obv,[status(thm),theory(equality)],[460]),
[iquote('0:Obv:460.0')] ).
cnf(465,plain,
( ~ aSet0(u)
| aElementOf0(skf9(szNzAzT0,v),szNzAzT0)
| aElementOf0(sz00,u) ),
inference(ssi,[status(thm)],[464,3,2]),
[iquote('0:SSi:464.0,3.0,2.0')] ).
cnf(497,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ equal(u,slcrc0)
| ~ aSubsetOf0(v,u)
| sdtlseqdt0(sbrdtbr0(v),sz00) ),
inference(spr,[status(thm),theory(equality)],[84,55]),
[iquote('0:SpR:84.1,55.3')] ).
cnf(498,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ equal(v,slcrc0)
| ~ aSubsetOf0(v,u)
| sdtlseqdt0(sz00,sbrdtbr0(u)) ),
inference(spr,[status(thm),theory(equality)],[84,55]),
[iquote('0:SpR:84.1,55.3')] ).
cnf(499,plain,
( ~ equal(u,slcrc0)
| ~ aSubsetOf0(v,u)
| sdtlseqdt0(sbrdtbr0(v),sz00) ),
inference(mrr,[status(thm)],[497,150,13]),
[iquote('0:MRR:497.0,497.1,150.1,13.1')] ).
cnf(500,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ equal(v,slcrc0)
| sdtlseqdt0(sz00,sbrdtbr0(u)) ),
inference(mrr,[status(thm)],[498,329]),
[iquote('0:MRR:498.3,329.2')] ).
cnf(561,plain,
( ~ aSet0(u)
| aElementOf0(sz00,u) ),
inference(spt,[spt(split,[position(s2s1)])],[465]),
[iquote('2:Spt:465.0,465.2')] ).
cnf(567,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0) ),
inference(res,[status(thm),theory(equality)],[561,21]),
[iquote('2:Res:561.1,21.0')] ).
cnf(571,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[567,13]),
[iquote('2:MRR:567.0,13.1')] ).
cnf(582,plain,
$false,
inference(eqr,[status(thm),theory(equality)],[571]),
[iquote('2:EqR:571.0')] ).
cnf(583,plain,
aElementOf0(skf9(szNzAzT0,u),szNzAzT0),
inference(spt,[spt(split,[position(s2s2)])],[465]),
[iquote('2:Spt:582.0,465.1')] ).
cnf(584,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| sdtlseqdt0(sz00,sbrdtbr0(u)) ),
inference(aed,[status(thm),theory(equality)],[8,500]),
[iquote('0:AED:8.0,500.2')] ).
cnf(751,plain,
( ~ aElementOf0(u,v)
| ~ aSubsetOf0(v,szNzAzT0)
| sdtlseqdt0(szmzizndt0(v),u) ),
inference(eqr,[status(thm),theory(equality)],[86]),
[iquote('0:EqR:86.2')] ).
cnf(818,plain,
( ~ aSubsetOf0(u,slcrc0)
| sdtlseqdt0(sbrdtbr0(u),sz00) ),
inference(eqr,[status(thm),theory(equality)],[499]),
[iquote('0:EqR:499.0')] ).
cnf(820,plain,
( ~ aSubsetOf0(u,slcrc0)
| ~ aElementOf0(sbrdtbr0(u),szNzAzT0)
| equal(sbrdtbr0(u),sz00) ),
inference(res,[status(thm),theory(equality)],[818,196]),
[iquote('0:Res:818.1,196.1')] ).
cnf(901,plain,
( ~ aSet0(u)
| ~ isFinite0(u)
| ~ aSubsetOf0(u,slcrc0)
| equal(sbrdtbr0(u),sz00) ),
inference(res,[status(thm),theory(equality)],[35,820]),
[iquote('0:Res:35.2,820.1')] ).
cnf(950,plain,
( ~ aSet0(slcrc0)
| ~ aSet0(slcrc0)
| ~ isFinite0(slcrc0)
| equal(sbrdtbr0(slcrc0),sz00) ),
inference(res,[status(thm),theory(equality)],[15,901]),
[iquote('0:Res:15.1,901.2')] ).
cnf(952,plain,
( ~ aSet0(slcrc0)
| ~ isFinite0(slcrc0)
| equal(sbrdtbr0(slcrc0),sz00) ),
inference(obv,[status(thm),theory(equality)],[950]),
[iquote('0:Obv:950.0')] ).
cnf(953,plain,
( ~ aSet0(slcrc0)
| equal(sbrdtbr0(slcrc0),sz00) ),
inference(ssi,[status(thm)],[952,1]),
[iquote('0:SSi:952.1,1.0')] ).
cnf(961,plain,
( ~ equal(slcrc0,slcrc0)
| equal(sbrdtbr0(slcrc0),sz00) ),
inference(sor,[status(thm)],[953,13]),
[iquote('0:SoR:953.0,13.1')] ).
cnf(962,plain,
equal(sbrdtbr0(slcrc0),sz00),
inference(obv,[status(thm),theory(equality)],[961]),
[iquote('0:Obv:961.0')] ).
cnf(1070,plain,
( ~ aElement0(u)
| ~ isFinite0(v)
| ~ aSet0(v)
| ~ aSet0(sdtpldt0(v,u))
| ~ isFinite0(sdtpldt0(v,u))
| aElementOf0(u,v)
| aElementOf0(szszuzczcdt0(sbrdtbr0(v)),szNzAzT0) ),
inference(spr,[status(thm),theory(equality)],[68,35]),
[iquote('0:SpR:68.4,35.2')] ).
cnf(1088,plain,
( ~ aElement0(u)
| ~ isFinite0(v)
| ~ aSet0(v)
| aElementOf0(u,v)
| aElementOf0(szszuzczcdt0(sbrdtbr0(v)),szNzAzT0) ),
inference(ssi,[status(thm)],[1070,247,45]),
[iquote('0:SSi:1070.4,1070.3,247.3,45.2,247.3,45.2')] ).
cnf(1098,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,slcrc0)
| aSubsetOf0(v,u) ),
inference(eqr,[status(thm),theory(equality)],[434]),
[iquote('0:EqR:434.1')] ).
cnf(1099,plain,
( ~ aSet0(slcrc0)
| ~ aSet0(u)
| aSubsetOf0(slcrc0,u) ),
inference(res,[status(thm),theory(equality)],[15,1098]),
[iquote('0:Res:15.1,1098.1')] ).
cnf(1107,plain,
( ~ aSet0(u)
| ~ equal(slcrc0,slcrc0)
| aSubsetOf0(slcrc0,u) ),
inference(sor,[status(thm)],[1099,13]),
[iquote('0:SoR:1099.0,13.1')] ).
cnf(1108,plain,
( ~ aSet0(u)
| aSubsetOf0(slcrc0,u) ),
inference(obv,[status(thm),theory(equality)],[1107]),
[iquote('0:Obv:1107.1')] ).
cnf(1118,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElementOf0(sz00,szNzAzT0)
| aSubsetOf0(skf13(u,v),u) ),
inference(res,[status(thm),theory(equality)],[584,67]),
[iquote('0:Res:584.2,67.3')] ).
cnf(1122,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElementOf0(sz00,szNzAzT0)
| aSubsetOf0(skf13(u,v),u) ),
inference(obv,[status(thm),theory(equality)],[1118]),
[iquote('0:Obv:1118.1')] ).
cnf(1123,plain,
( ~ isFinite0(u)
| ~ aSet0(u)
| aSubsetOf0(skf13(u,v),u) ),
inference(mrr,[status(thm)],[1122,4]),
[iquote('0:MRR:1122.2,4.0')] ).
cnf(1127,plain,
( ~ aSet0(u)
| ~ aSet0(u)
| ~ aSubsetOf0(u,slcrc0)
| equal(slcrc0,u) ),
inference(res,[status(thm),theory(equality)],[1108,85]),
[iquote('0:Res:1108.1,85.1')] ).
cnf(1129,plain,
( ~ aSet0(u)
| ~ aSet0(u)
| aSet0(slcrc0) ),
inference(res,[status(thm),theory(equality)],[1108,28]),
[iquote('0:Res:1108.1,28.1')] ).
cnf(1137,plain,
( ~ aSet0(u)
| aSet0(slcrc0) ),
inference(obv,[status(thm),theory(equality)],[1129]),
[iquote('0:Obv:1129.0')] ).
cnf(1140,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(u,slcrc0)
| equal(slcrc0,u) ),
inference(obv,[status(thm),theory(equality)],[1127]),
[iquote('0:Obv:1127.0')] ).
cnf(1148,plain,
aSet0(slcrc0),
inference(ems,[status(thm)],[1137,136]),
[iquote('0:EmS:1137.0,136.0')] ).
cnf(1183,plain,
( ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0)
| ~ aSet0(skf13(slcrc0,u))
| equal(skf13(slcrc0,u),slcrc0) ),
inference(res,[status(thm),theory(equality)],[1123,1140]),
[iquote('0:Res:1123.2,1140.1')] ).
cnf(1185,plain,
( ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0)
| ~ aSet0(u)
| aSubsetOf0(skf13(slcrc0,v),u) ),
inference(res,[status(thm),theory(equality)],[1123,1098]),
[iquote('0:Res:1123.2,1098.1')] ).
cnf(1189,plain,
( ~ aSet0(u)
| aSubsetOf0(skf13(slcrc0,v),u) ),
inference(ssi,[status(thm)],[1185,1,1148]),
[iquote('0:SSi:1185.1,1185.0,1.0,1148.0,1.0,1148.0')] ).
cnf(1191,plain,
( ~ aSet0(skf13(slcrc0,u))
| equal(skf13(slcrc0,u),slcrc0) ),
inference(ssi,[status(thm)],[1183,1,1148]),
[iquote('0:SSi:1183.1,1183.0,1.0,1148.0,1.0,1148.0')] ).
cnf(1211,plain,
( ~ aSet0(u)
| ~ aSet0(u)
| aSet0(skf13(slcrc0,v)) ),
inference(res,[status(thm),theory(equality)],[1189,28]),
[iquote('0:Res:1189.1,28.1')] ).
cnf(1220,plain,
( ~ aSet0(u)
| aSet0(skf13(slcrc0,v)) ),
inference(obv,[status(thm),theory(equality)],[1211]),
[iquote('0:Obv:1211.0')] ).
cnf(1232,plain,
aSet0(skf13(slcrc0,u)),
inference(ems,[status(thm)],[1220,1148]),
[iquote('0:EmS:1220.0,1148.0')] ).
cnf(1245,plain,
equal(skf13(slcrc0,u),slcrc0),
inference(mrr,[status(thm)],[1191,1232]),
[iquote('0:MRR:1191.0,1232.0')] ).
cnf(1442,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| ~ equal(u,slcrc0)
| equal(v,slcrc0) ),
inference(res,[status(thm),theory(equality)],[456,21]),
[iquote('0:Res:456.3,21.0')] ).
cnf(1443,plain,
( ~ aSet0(u)
| ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| equal(v,slcrc0)
| aElement0(skf8(v)) ),
inference(res,[status(thm),theory(equality)],[456,26]),
[iquote('0:Res:456.3,26.1')] ).
cnf(1446,plain,
( ~ aSubsetOf0(u,v)
| ~ equal(v,slcrc0)
| equal(u,slcrc0) ),
inference(mrr,[status(thm)],[1442,13]),
[iquote('0:MRR:1442.0,13.1')] ).
cnf(1448,plain,
( ~ aSet0(u)
| ~ aSubsetOf0(v,u)
| equal(v,slcrc0)
| aElement0(skf8(v)) ),
inference(obv,[status(thm),theory(equality)],[1443]),
[iquote('0:Obv:1443.0')] ).
cnf(1478,plain,
( ~ aSet0(szNzAzT0)
| equal(xS,slcrc0)
| aElement0(skf8(xS)) ),
inference(res,[status(thm),theory(equality)],[5,1448]),
[iquote('0:Res:5.0,1448.1')] ).
cnf(1486,plain,
( equal(xS,slcrc0)
| aElement0(skf8(xS)) ),
inference(ssi,[status(thm)],[1478,3,2]),
[iquote('0:SSi:1478.0,3.0,2.0')] ).
cnf(1487,plain,
aElement0(skf8(xS)),
inference(mrr,[status(thm)],[1486,8]),
[iquote('0:MRR:1486.0,8.0')] ).
cnf(1502,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(v,szszuzczcdt0(u)) ),
inference(res,[status(thm),theory(equality)],[24,78]),
[iquote('0:Res:24.1,78.0')] ).
cnf(1512,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(szszuzczcdt0(v),szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(v)) ),
inference(obv,[status(thm),theory(equality)],[1502]),
[iquote('0:Obv:1502.0')] ).
cnf(1513,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(v)) ),
inference(mrr,[status(thm)],[1512,23]),
[iquote('0:MRR:1512.1,23.1')] ).
cnf(1903,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,v) ),
inference(res,[status(thm),theory(equality)],[1513,61]),
[iquote('0:Res:1513.3,61.2')] ).
cnf(1908,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),v)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,v) ),
inference(obv,[status(thm),theory(equality)],[1903]),
[iquote('0:Obv:1903.1')] ).
cnf(1909,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,v) ),
inference(mrr,[status(thm)],[1908,23]),
[iquote('0:MRR:1908.1,23.1')] ).
cnf(2514,plain,
( ~ aElement0(u)
| ~ isFinite0(slcrc0)
| ~ aSet0(slcrc0)
| aElementOf0(u,slcrc0)
| aElementOf0(szszuzczcdt0(sz00),szNzAzT0) ),
inference(spr,[status(thm),theory(equality)],[962,1088]),
[iquote('0:SpR:962.0,1088.4')] ).
cnf(2541,plain,
( ~ aElement0(u)
| aElementOf0(u,slcrc0)
| aElementOf0(szszuzczcdt0(sz00),szNzAzT0) ),
inference(ssi,[status(thm)],[2514,1,1148]),
[iquote('0:SSi:2514.2,2514.1,1.0,1148.0,1.0,1148.0')] ).
cnf(2559,plain,
( ~ aElement0(u)
| aElementOf0(u,slcrc0) ),
inference(spt,[spt(split,[position(s2s2s1)])],[2541]),
[iquote('3:Spt:2541.0,2541.1')] ).
cnf(2560,plain,
( ~ aElement0(u)
| ~ equal(slcrc0,slcrc0) ),
inference(res,[status(thm),theory(equality)],[2559,21]),
[iquote('3:Res:2559.1,21.0')] ).
cnf(2564,plain,
~ aElement0(u),
inference(obv,[status(thm),theory(equality)],[2560]),
[iquote('3:Obv:2560.1')] ).
cnf(2565,plain,
$false,
inference(unc,[status(thm)],[2564,1487]),
[iquote('3:UnC:2564.0,1487.0')] ).
cnf(2568,plain,
aElementOf0(szszuzczcdt0(sz00),szNzAzT0),
inference(spt,[spt(split,[position(s2s2s2)])],[2541]),
[iquote('3:Spt:2565.0,2541.2')] ).
cnf(2990,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(v,u)
| sdtlseqdt0(u,v) ),
inference(res,[status(thm),theory(equality)],[54,1909]),
[iquote('0:Res:54.3,1909.0')] ).
cnf(2995,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(u,v)
| sdtlseqdt0(v,u) ),
inference(obv,[status(thm),theory(equality)],[2990]),
[iquote('0:Obv:2990.1')] ).
cnf(3036,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(xT,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(szmzizndt0(xS),u)
| sdtlseqdt0(u,szmzizndt0(xS)) ),
inference(res,[status(thm),theory(equality)],[454,2995]),
[iquote('0:Res:454.2,2995.0')] ).
cnf(3044,plain,
( ~ aSubsetOf0(xT,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(szmzizndt0(xS),u)
| sdtlseqdt0(u,szmzizndt0(xS)) ),
inference(ssi,[status(thm)],[3036,3,2]),
[iquote('0:SSi:3036.0,3.0,2.0')] ).
cnf(3045,plain,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(szmzizndt0(xS),u)
| sdtlseqdt0(u,szmzizndt0(xS)) ),
inference(mrr,[status(thm)],[3044,6]),
[iquote('0:MRR:3044.0,6.0')] ).
cnf(3318,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| aSubsetOf0(xT,u)
| aElementOf0(skf9(xT,v),szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[6,457]),
[iquote('0:Res:6.0,457.2')] ).
cnf(3319,plain,
( ~ aSet0(u)
| ~ aSet0(szNzAzT0)
| aSubsetOf0(xS,u)
| aElementOf0(skf9(xS,v),szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[5,457]),
[iquote('0:Res:5.0,457.2')] ).
cnf(3325,plain,
( ~ aSet0(u)
| aSubsetOf0(xT,u)
| aElementOf0(skf9(xT,v),szNzAzT0) ),
inference(ssi,[status(thm)],[3318,3,2]),
[iquote('0:SSi:3318.1,3.0,2.0')] ).
cnf(3326,plain,
( ~ aSet0(u)
| aSubsetOf0(xS,u)
| aElementOf0(skf9(xS,v),szNzAzT0) ),
inference(ssi,[status(thm)],[3319,3,2]),
[iquote('0:SSi:3319.1,3.0,2.0')] ).
cnf(3341,plain,
( ~ aSet0(u)
| aSubsetOf0(xT,u) ),
inference(spt,[spt(split,[position(s2s2s2s1)])],[3325]),
[iquote('4:Spt:3325.0,3325.1')] ).
cnf(3356,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0)
| equal(xT,slcrc0) ),
inference(res,[status(thm),theory(equality)],[3341,1446]),
[iquote('4:Res:3341.1,1446.0')] ).
cnf(3375,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[3356,13,9]),
[iquote('4:MRR:3356.0,3356.2,13.1,9.0')] ).
cnf(3376,plain,
$false,
inference(unc,[status(thm)],[3375,1245]),
[iquote('4:UnC:3375.0,1245.0')] ).
cnf(3392,plain,
aElementOf0(skf9(xT,u),szNzAzT0),
inference(spt,[spt(split,[position(s2s2s2s2)])],[3325]),
[iquote('4:Spt:3376.0,3325.2')] ).
cnf(3440,plain,
( ~ aSet0(u)
| aSubsetOf0(xS,u) ),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[3326]),
[iquote('5:Spt:3326.0,3326.1')] ).
cnf(3455,plain,
( ~ aSet0(u)
| ~ equal(u,slcrc0)
| equal(xS,slcrc0) ),
inference(res,[status(thm),theory(equality)],[3440,1446]),
[iquote('5:Res:3440.1,1446.0')] ).
cnf(3474,plain,
~ equal(u,slcrc0),
inference(mrr,[status(thm)],[3455,13,8]),
[iquote('5:MRR:3455.0,3455.2,13.1,8.0')] ).
cnf(3475,plain,
$false,
inference(unc,[status(thm)],[3474,1245]),
[iquote('5:UnC:3474.0,1245.0')] ).
cnf(3491,plain,
aElementOf0(skf9(xS,u),szNzAzT0),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[3326]),
[iquote('5:Spt:3475.0,3326.2')] ).
cnf(3703,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(xS,szNzAzT0)
| sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT))
| sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS)) ),
inference(res,[status(thm),theory(equality)],[455,3045]),
[iquote('0:Res:455.2,3045.0')] ).
cnf(3714,plain,
( ~ aSubsetOf0(xS,szNzAzT0)
| sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT))
| sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS)) ),
inference(ssi,[status(thm)],[3703,3,2]),
[iquote('0:SSi:3703.0,3.0,2.0')] ).
cnf(3715,plain,
( sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT))
| sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS)) ),
inference(mrr,[status(thm)],[3714,5]),
[iquote('0:MRR:3714.0,5.0')] ).
cnf(3728,plain,
sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)),
inference(spt,[spt(split,[position(s2s2s2s2s2s1)])],[3715]),
[iquote('6:Spt:3715.0')] ).
cnf(3729,plain,
( ~ aElementOf0(szmzizndt0(xT),szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0)
| ~ sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS)) ),
inference(mrr,[status(thm)],[100,3728]),
[iquote('6:MRR:100.3,3728.0')] ).
cnf(3745,plain,
( ~ aElementOf0(szmzizndt0(xS),xT)
| ~ aSubsetOf0(xT,szNzAzT0)
| ~ aElementOf0(szmzizndt0(xT),szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[751,3729]),
[iquote('6:Res:751.2,3729.2')] ).
cnf(3746,plain,
( ~ aElementOf0(szmzizndt0(xT),szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(mrr,[status(thm)],[3745,10,6]),
[iquote('6:MRR:3745.0,3745.1,10.0,6.0')] ).
cnf(3750,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(xS,szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[455,3746]),
[iquote('6:Res:455.2,3746.0')] ).
cnf(3752,plain,
( ~ aSubsetOf0(xS,szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(ssi,[status(thm)],[3750,3,2]),
[iquote('6:SSi:3750.0,3.0,2.0')] ).
cnf(3753,plain,
~ aElementOf0(szmzizndt0(xS),szNzAzT0),
inference(mrr,[status(thm)],[3752,5]),
[iquote('6:MRR:3752.0,5.0')] ).
cnf(3756,plain,
( ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(xT,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[454,3753]),
[iquote('6:Res:454.2,3753.0')] ).
cnf(3759,plain,
~ aSubsetOf0(xT,szNzAzT0),
inference(ssi,[status(thm)],[3756,3,2]),
[iquote('6:SSi:3756.0,3.0,2.0')] ).
cnf(3760,plain,
$false,
inference(mrr,[status(thm)],[3759,6]),
[iquote('6:MRR:3759.0,6.0')] ).
cnf(3761,plain,
~ sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)),
inference(spt,[spt(split,[position(s2s2s2s2s2sa)])],[3760,3728]),
[iquote('6:Spt:3760.0,3715.0,3728.0')] ).
cnf(3762,plain,
sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS)),
inference(spt,[spt(split,[position(s2s2s2s2s2s2)])],[3715]),
[iquote('6:Spt:3760.0,3715.1')] ).
cnf(3765,plain,
( ~ aElementOf0(szmzizndt0(xT),xS)
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[751,3761]),
[iquote('6:Res:751.2,3761.0')] ).
cnf(3766,plain,
$false,
inference(mrr,[status(thm)],[3765,11,5]),
[iquote('6:MRR:3765.0,3765.1,11.0,5.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUM539+1 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n024.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 : Thu Jul 7 01:33:14 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.77/0.96
% 0.77/0.96 SPASS V 3.9
% 0.77/0.96 SPASS beiseite: Proof found.
% 0.77/0.96 % SZS status Theorem
% 0.77/0.96 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.77/0.96 SPASS derived 2584 clauses, backtracked 165 clauses, performed 7 splits and kept 1055 clauses.
% 0.77/0.96 SPASS allocated 100745 KBytes.
% 0.77/0.96 SPASS spent 0:00:00.61 on the problem.
% 0.77/0.96 0:00:00.04 for the input.
% 0.77/0.96 0:00:00.09 for the FLOTTER CNF translation.
% 0.77/0.96 0:00:00.04 for inferences.
% 0.77/0.96 0:00:00.00 for the backtracking.
% 0.77/0.96 0:00:00.40 for the reduction.
% 0.77/0.96
% 0.77/0.96
% 0.77/0.96 Here is a proof with depth 9, length 186 :
% 0.77/0.96 % SZS output start Refutation
% See solution above
% 0.77/0.99 Formulae used in the proof : mEmpFin mNATSet mZeroNum m__1779 mNatExtra m__1802 m__ mDefEmp mSubRefl mLessRefl mSuccNum mLessSucc mEOfElem mDefSub mNoScLessZr mCardNum mCardEmpty mFConsSet mDefCons mLessTotal mCardSub mSubASymm mSuccLess mLessASymm mDefMin mCardSubEx mCardCons mSubTrans mLessTrans
% 0.77/0.99
%------------------------------------------------------------------------------