%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP093^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:24:05 AM UTC 2026
% Result : Theorem 3.64s 0.84s
% Output : CNFRefutation 3.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 30
% Syntax : Number of formulae : 396 ( 157 unt; 0 typ; 0 def)
% Number of atoms : 2791 ( 972 equ; 0 cnn)
% Maximal formula atoms : 5 ( 7 avg)
% Number of connectives : 3895 ( 871 ~; 804 |; 15 &;2088 @)
% ( 0 <=>; 117 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 32 ( 31 usr)
% Number of type conns : 117 ( 117 >; 0 *; 0 +; 0 <<)
% Number of symbols : 112 ( 109 usr; 8 con; 0-3 aty)
% Number of variables : 929 ( 239 ^; 687 !; 3 ?; 929 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_nat,type,
nat: $tType ).
thf(tp_pair_p125712459t_unit,type,
pair_p125712459t_unit: $tType ).
thf(tp_pair_p1593840546t_unit,type,
pair_p1593840546t_unit: $tType ).
thf(tp_pair_p1765063010t_unit,type,
pair_p1765063010t_unit: $tType ).
thf(tp_pair_p1914262621t_unit,type,
pair_p1914262621t_unit: $tType ).
thf(tp_pair_p2041852168t_unit,type,
pair_p2041852168t_unit: $tType ).
thf(tp_produc1572603623od_a_a,type,
produc1572603623od_a_a: $tType ).
thf(tp_product_prod_a_a,type,
product_prod_a_a: $tType ).
thf(tp_product_prod_nat_nat,type,
product_prod_nat_nat: $tType ).
thf(tp_product_unit,type,
product_unit: $tType ).
thf(tp_set_Pr1295299783od_a_a,type,
set_Pr1295299783od_a_a: $tType ).
thf(tp_set_Pr1490359111at_nat,type,
set_Pr1490359111at_nat: $tType ).
thf(tp_set_Pr1689873822_a_a_a,type,
set_Pr1689873822_a_a_a: $tType ).
thf(tp_set_Pr1746169692at_nat,type,
set_Pr1746169692at_nat: $tType ).
thf(tp_set_Pr1948701895od_a_a,type,
set_Pr1948701895od_a_a: $tType ).
thf(tp_set_Pr1986765409at_nat,type,
set_Pr1986765409at_nat: $tType ).
thf(tp_set_Pr339609346od_a_a,type,
set_Pr339609346od_a_a: $tType ).
thf(tp_set_Pr548851891_a_nat,type,
set_Pr548851891_a_nat: $tType ).
thf(tp_set_Pr681306928od_a_a,type,
set_Pr681306928od_a_a: $tType ).
thf(tp_set_Pr7688842at_nat,type,
set_Pr7688842at_nat: $tType ).
thf(tp_set_Pr894832732_a_nat,type,
set_Pr894832732_a_nat: $tType ).
thf(tp_set_Pr967348953_nat_a,type,
set_Pr967348953_nat_a: $tType ).
thf(tp_set_Product_prod_a_a,type,
set_Product_prod_a_a: $tType ).
thf(tp_set_a,type,
set_a: $tType ).
thf(tp_set_nat,type,
set_nat: $tType ).
thf(tp_set_se1596668135od_a_a,type,
set_se1596668135od_a_a: $tType ).
thf(tp_set_se1612935105at_nat,type,
set_se1612935105at_nat: $tType ).
thf(tp_set_se958357159od_a_a,type,
set_se958357159od_a_a: $tType ).
thf(tp_set_set_a,type,
set_set_a: $tType ).
thf(tp_set_set_nat,type,
set_set_nat: $tType ).
thf(tp_bot_bo2130386637at_nat,type,
bot_bo2130386637at_nat: set_Pr1986765409at_nat ).
thf(tp_bot_bo2131659635od_a_a,type,
bot_bo2131659635od_a_a: set_Product_prod_a_a ).
thf(tp_bot_bot_set_a,type,
bot_bot_set_a: set_a ).
thf(tp_bot_bot_set_nat,type,
bot_bot_set_nat: set_nat ).
thf(tp_collec1606769740at_nat,type,
collec1606769740at_nat: ( set_Pr1986765409at_nat > $o ) > set_se1612935105at_nat ).
thf(tp_collec1635618130od_a_a,type,
collec1635618130od_a_a: ( produc1572603623od_a_a > $o ) > set_Pr1948701895od_a_a ).
thf(tp_collec183727474od_a_a,type,
collec183727474od_a_a: ( set_Product_prod_a_a > $o ) > set_se1596668135od_a_a ).
thf(tp_collec453062450od_a_a,type,
collec453062450od_a_a: ( set_Pr1948701895od_a_a > $o ) > set_se958357159od_a_a ).
thf(tp_collec645855634od_a_a,type,
collec645855634od_a_a: ( product_prod_a_a > $o ) > set_Product_prod_a_a ).
thf(tp_collec7649004at_nat,type,
collec7649004at_nat: ( product_prod_nat_nat > $o ) > set_Pr1986765409at_nat ).
thf(tp_collect_a,type,
collect_a: ( a > $o ) > set_a ).
thf(tp_collect_nat,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(tp_collect_set_a,type,
collect_set_a: ( set_a > $o ) > set_set_a ).
thf(tp_collect_set_nat,type,
collect_set_nat: ( set_nat > $o ) > set_set_nat ).
thf(tp_finite1145471536od_a_a,type,
finite1145471536od_a_a: set_se1596668135od_a_a > $o ).
thf(tp_finite1297454819od_a_a,type,
finite1297454819od_a_a: set_Pr339609346od_a_a > $o ).
thf(tp_finite1457549322at_nat,type,
finite1457549322at_nat: set_se1612935105at_nat > $o ).
thf(tp_finite1664988688od_a_a,type,
finite1664988688od_a_a: set_Pr1948701895od_a_a > $o ).
thf(tp_finite1743148308_a_nat,type,
finite1743148308_a_nat: set_Pr548851891_a_nat > $o ).
thf(tp_finite179568208od_a_a,type,
finite179568208od_a_a: set_Product_prod_a_a > $o ).
thf(tp_finite1808550458_nat_a,type,
finite1808550458_nat_a: set_Pr967348953_nat_a > $o ).
thf(tp_finite1837575485_a_nat,type,
finite1837575485_a_nat: set_Pr894832732_a_nat > $o ).
thf(tp_finite1919032935_a_a_a,type,
finite1919032935_a_a_a: set_Pr1689873822_a_a_a > $o ).
thf(tp_finite2012248349et_nat,type,
finite2012248349et_nat: set_set_nat > $o ).
thf(tp_finite256329232od_a_a,type,
finite256329232od_a_a: set_Pr1295299783od_a_a > $o ).
thf(tp_finite277291581at_nat,type,
finite277291581at_nat: set_Pr1746169692at_nat > $o ).
thf(tp_finite323969008od_a_a,type,
finite323969008od_a_a: set_se958357159od_a_a > $o ).
thf(tp_finite351630733od_a_a,type,
finite351630733od_a_a: set_Product_prod_a_a > set_se1596668135od_a_a ).
thf(tp_finite361944167at_nat,type,
finite361944167at_nat: set_Pr1986765409at_nat > set_se1612935105at_nat ).
thf(tp_finite48957584at_nat,type,
finite48957584at_nat: set_Pr1490359111at_nat > $o ).
thf(tp_finite676513017od_a_a,type,
finite676513017od_a_a: set_Pr681306928od_a_a > $o ).
thf(tp_finite702915405od_a_a,type,
finite702915405od_a_a: set_Pr1948701895od_a_a > set_se958357159od_a_a ).
thf(tp_finite772653738at_nat,type,
finite772653738at_nat: set_Pr1986765409at_nat > $o ).
thf(tp_finite942416723at_nat,type,
finite942416723at_nat: set_Pr7688842at_nat > $o ).
thf(tp_finite_Fpow_a,type,
finite_Fpow_a: set_a > set_set_a ).
thf(tp_finite_Fpow_nat,type,
finite_Fpow_nat: set_nat > set_set_nat ).
thf(tp_finite_card_a,type,
finite_card_a: set_a > nat ).
thf(tp_finite_finite_a,type,
finite_finite_a: set_a > $o ).
thf(tp_finite_finite_nat,type,
finite_finite_nat: set_nat > $o ).
thf(tp_finite_finite_set_a,type,
finite_finite_set_a: set_set_a > $o ).
thf(tp_g,type,
g: pair_p125712459t_unit ).
thf(tp_member1838126896od_a_a,type,
member1838126896od_a_a: set_Product_prod_a_a > set_se1596668135od_a_a > $o ).
thf(tp_member449909584od_a_a,type,
member449909584od_a_a: product_prod_a_a > set_Product_prod_a_a > $o ).
thf(tp_member701585322at_nat,type,
member701585322at_nat: product_prod_nat_nat > set_Pr1986765409at_nat > $o ).
thf(tp_member_a,type,
member_a: a > set_a > $o ).
thf(tp_member_nat,type,
member_nat: nat > set_nat > $o ).
thf(tp_member_set_a,type,
member_set_a: set_a > set_set_a > $o ).
thf(tp_member_set_nat,type,
member_set_nat: set_nat > set_set_nat > $o ).
thf(tp_n,type,
n: nat ).
thf(tp_ord_le1347718902_a_a_o,type,
ord_le1347718902_a_a_o: ( product_prod_a_a > $o ) > ( product_prod_a_a > $o ) > $o ).
thf(tp_ord_le1816232656od_a_a,type,
ord_le1816232656od_a_a: set_Pr681306928od_a_a > set_Pr681306928od_a_a > $o ).
thf(tp_ord_le1824328871od_a_a,type,
ord_le1824328871od_a_a: set_Product_prod_a_a > set_Product_prod_a_a > $o ).
thf(tp_ord_le2073555219_a_nat,type,
ord_le2073555219_a_nat: set_Pr548851891_a_nat > set_Pr548851891_a_nat > $o ).
thf(tp_ord_le2084554594od_a_a,type,
ord_le2084554594od_a_a: set_Pr339609346od_a_a > set_Pr339609346od_a_a > $o ).
thf(tp_ord_le344568633_nat_a,type,
ord_le344568633_nat_a: set_Pr967348953_nat_a > set_Pr967348953_nat_a > $o ).
thf(tp_ord_le456379495od_a_a,type,
ord_le456379495od_a_a: set_Pr1948701895od_a_a > set_Pr1948701895od_a_a > $o ).
thf(tp_ord_le492294332_a_nat,type,
ord_le492294332_a_nat: set_Pr894832732_a_nat > set_Pr894832732_a_nat > $o ).
thf(tp_ord_le677315902_a_a_a,type,
ord_le677315902_a_a_a: set_Pr1689873822_a_a_a > set_Pr1689873822_a_a_a > $o ).
thf(tp_ord_le841296385at_nat,type,
ord_le841296385at_nat: set_Pr1986765409at_nat > set_Pr1986765409at_nat > $o ).
thf(tp_ord_less_eq_a_o,type,
ord_less_eq_a_o: ( a > $o ) > ( a > $o ) > $o ).
thf(tp_ord_less_eq_nat,type,
ord_less_eq_nat: nat > nat > $o ).
thf(tp_ord_less_eq_nat_o,type,
ord_less_eq_nat_o: ( nat > $o ) > ( nat > $o ) > $o ).
thf(tp_ord_less_eq_set_a,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(tp_ord_less_eq_set_nat,type,
ord_less_eq_set_nat: set_nat > set_nat > $o ).
thf(tp_pair_p1027063983ms_nat,type,
pair_p1027063983ms_nat: pair_p1914262621t_unit > $o ).
thf(tp_pair_p1047056820t_unit,type,
pair_p1047056820t_unit: pair_p125712459t_unit > set_a ).
thf(tp_pair_p1167410509t_unit,type,
pair_p1167410509t_unit: set_nat > set_Pr1986765409at_nat > product_unit > pair_p1914262621t_unit ).
thf(tp_pair_p128415500ph_nat,type,
pair_p128415500ph_nat: pair_p1914262621t_unit > $o ).
thf(tp_pair_p133601421t_unit,type,
pair_p133601421t_unit: pair_p125712459t_unit > set_Product_prod_a_a ).
thf(tp_pair_p1515597646ph_nat,type,
pair_p1515597646ph_nat: pair_p1914262621t_unit > $o ).
thf(tp_pair_p1559300324t_unit,type,
pair_p1559300324t_unit: pair_p1593840546t_unit > set_Pr1295299783od_a_a ).
thf(tp_pair_p159207083od_a_a,type,
pair_p159207083od_a_a: pair_p1593840546t_unit > $o ).
thf(tp_pair_p1621517565t_unit,type,
pair_p1621517565t_unit: set_a > set_Product_prod_a_a > product_unit > pair_p125712459t_unit ).
thf(tp_pair_p1652294923t_unit,type,
pair_p1652294923t_unit: pair_p1593840546t_unit > set_Pr1948701895od_a_a ).
thf(tp_pair_p1677060310t_unit,type,
pair_p1677060310t_unit: pair_p1914262621t_unit > set_nat ).
thf(tp_pair_p1783210148t_unit,type,
pair_p1783210148t_unit: pair_p1765063010t_unit > set_Pr1948701895od_a_a ).
thf(tp_pair_p1802376898raph_a,type,
pair_p1802376898raph_a: pair_p125712459t_unit > $o ).
thf(tp_pair_p1864019935ioms_a,type,
pair_p1864019935ioms_a: pair_p125712459t_unit > $o ).
thf(tp_pair_p1896222615t_unit,type,
pair_p1896222615t_unit: pair_p125712459t_unit > product_unit ).
thf(tp_pair_p1906342088od_a_a,type,
pair_p1906342088od_a_a: pair_p1593840546t_unit > $o ).
thf(tp_pair_p1984658862t_unit,type,
pair_p1984658862t_unit: pair_p1765063010t_unit > product_unit ).
thf(tp_pair_p210955889t_unit,type,
pair_p210955889t_unit: pair_p2041852168t_unit > set_Pr1986765409at_nat ).
thf(tp_pair_p374947051od_a_a,type,
pair_p374947051od_a_a: pair_p1765063010t_unit > $o ).
thf(tp_pair_p398687508t_unit,type,
pair_p398687508t_unit: set_Product_prod_a_a > set_Pr1948701895od_a_a > product_unit > pair_p1765063010t_unit ).
thf(tp_pair_p447552203t_unit,type,
pair_p447552203t_unit: pair_p1765063010t_unit > set_Product_prod_a_a ).
thf(tp_pair_p504738056od_a_a,type,
pair_p504738056od_a_a: pair_p1765063010t_unit > $o ).
thf(tp_pair_p56914274at_nat,type,
pair_p56914274at_nat: pair_p2041852168t_unit > $o ).
thf(tp_pair_p646030121od_a_a,type,
pair_p646030121od_a_a: pair_p1765063010t_unit > $o ).
thf(tp_pair_p68905728raph_a,type,
pair_p68905728raph_a: pair_p125712459t_unit > $o ).
thf(tp_pair_p69470259t_unit,type,
pair_p69470259t_unit: pair_p1914262621t_unit > product_unit ).
thf(tp_pair_p715279805t_unit,type,
pair_p715279805t_unit: pair_p1914262621t_unit > set_Pr1986765409at_nat ).
thf(tp_pair_p752841413at_nat,type,
pair_p752841413at_nat: pair_p2041852168t_unit > $o ).
thf(tp_pair_p806300874t_unit,type,
pair_p806300874t_unit: pair_p2041852168t_unit > set_Pr1490359111at_nat ).
thf(tp_produc1182842125od_a_a,type,
produc1182842125od_a_a: set_nat > ( nat > set_Product_prod_a_a ) > set_Pr339609346od_a_a ).
thf(tp_produc1282482655_a_a_a,type,
produc1282482655_a_a_a: set_Product_prod_a_a > ( product_prod_a_a > set_a ) > set_Pr1689873822_a_a_a ).
thf(tp_produc1833107820_a_a_o,type,
produc1833107820_a_a_o: ( a > a > $o ) > product_prod_a_a > $o ).
thf(tp_produc292491723at_nat,type,
produc292491723at_nat: set_a > ( a > set_Pr1986765409at_nat ) > set_Pr7688842at_nat ).
thf(tp_produc304751368od_a_a,type,
produc304751368od_a_a: set_Product_prod_a_a > ( product_prod_a_a > set_Product_prod_a_a ) > set_Pr1948701895od_a_a ).
thf(tp_produc45129834at_nat,type,
produc45129834at_nat: set_nat > ( nat > set_nat ) > set_Pr1986765409at_nat ).
thf(tp_produc520147185od_a_a,type,
produc520147185od_a_a: set_a > ( a > set_Product_prod_a_a ) > set_Pr681306928od_a_a ).
thf(tp_produc894163943at_nat,type,
produc894163943at_nat: set_nat > ( nat > set_Pr1986765409at_nat ) > set_Pr1746169692at_nat ).
thf(tp_produc931712687_a_nat,type,
produc931712687_a_nat: set_Product_prod_a_a > ( product_prod_a_a > set_nat ) > set_Pr894832732_a_nat ).
thf(tp_product_Pair_a_a,type,
product_Pair_a_a: a > a > product_prod_a_a ).
thf(tp_product_Sigma_a_a,type,
product_Sigma_a_a: set_a > ( a > set_a ) > set_Product_prod_a_a ).
thf(tp_product_Sigma_a_nat,type,
product_Sigma_a_nat: set_a > ( a > set_nat ) > set_Pr548851891_a_nat ).
thf(tp_product_Sigma_nat_a,type,
product_Sigma_nat_a: set_nat > ( nat > set_a ) > set_Pr967348953_nat_a ).
thf(tp_product_product_a_a,type,
product_product_a_a: set_a > set_a > set_Product_prod_a_a ).
thf(tp_sK1_SY89,type,
sK1_SY89: ( product_prod_a_a > $o ) > product_prod_a_a ).
thf(tp_sK2_SY115,type,
sK2_SY115: ( a > set_a ) > set_a > a ).
thf(25,axiom,
! [A: set_a,B: set_a] :
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) )
= ( ( A = bot_bot_set_a )
| ( B = bot_bot_set_a )
| ( ( finite_finite_a @ A )
& ( finite_finite_a @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_329_finite__cartesian__product__iff) ).
thf(37,axiom,
( finite351630733od_a_a
= ( ^ [A5: set_Product_prod_a_a] :
( collec183727474od_a_a
@ ^ [X5: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ X5 @ A5 )
& ( finite179568208od_a_a @ X5 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_317_Fpow__def) ).
thf(45,axiom,
! [Pverts: set_a,Parcs: set_Product_prod_a_a,More: product_unit] :
( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ Pverts @ Parcs @ More ) )
= Parcs ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_309_pair__pre__digraph_Oselect__convs_I2_J) ).
thf(65,axiom,
! [R2: pair_p125712459t_unit] :
( R2
= ( pair_p1621517565t_unit @ ( pair_p1047056820t_unit @ R2 ) @ ( pair_p133601421t_unit @ R2 ) @ ( pair_p1896222615t_unit @ R2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_289_pair__pre__digraph_Osurjective) ).
thf(221,axiom,
! [R2: pair_p125712459t_unit,R3: pair_p125712459t_unit] :
( ( ( pair_p1047056820t_unit @ R2 )
= ( pair_p1047056820t_unit @ R3 ) )
=> ( ( ( pair_p133601421t_unit @ R2 )
= ( pair_p133601421t_unit @ R3 ) )
=> ( ( ( pair_p1896222615t_unit @ R2 )
= ( pair_p1896222615t_unit @ R3 ) )
=> ( R2 = R3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_pair__pre__digraph_Oequality) ).
thf(249,axiom,
! [A: set_nat,B: set_Product_prod_a_a] :
( ~ ( finite_finite_nat @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_infinite__cartesian__product) ).
thf(251,axiom,
! [A: set_a,B: set_Product_prod_a_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_infinite__cartesian__product) ).
thf(252,axiom,
! [A: set_Product_prod_a_a,B: set_nat] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_nat @ B )
=> ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_infinite__cartesian__product) ).
thf(253,axiom,
! [A: set_Product_prod_a_a,B: set_a] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_infinite__cartesian__product) ).
thf(254,axiom,
! [A: set_a,B: set_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_infinite__cartesian__product) ).
thf(262,axiom,
! [G2: pair_p1765063010t_unit] :
( ( pair_p374947051od_a_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p447552203t_unit @ G2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_pair__fin__digraph_Opair__finite__verts) ).
thf(268,axiom,
! [A: set_nat,B: set_Product_prod_a_a] :
( ( finite_finite_nat @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_finite__cartesian__product) ).
thf(270,axiom,
! [A: set_a,B: set_Product_prod_a_a] :
( ( finite_finite_a @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_finite__cartesian__product) ).
thf(271,axiom,
! [A: set_Product_prod_a_a,B: set_nat] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_nat @ B )
=> ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_finite__cartesian__product) ).
thf(272,axiom,
! [A: set_Product_prod_a_a,B: set_a] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_finite__cartesian__product) ).
thf(273,axiom,
! [A: set_a,B: set_a] :
( ( finite_finite_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_finite__cartesian__product) ).
thf(292,axiom,
! [P: product_prod_a_a > $o] :
( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
=> ? [X_1: product_prod_a_a] : ( P @ X_1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_not__finite__existsD) ).
thf(302,axiom,
! [A: set_a,B: a > set_a] :
( ( finite_finite_a @ A )
=> ( ! [A3: a] :
( ( member_a @ A3 @ A )
=> ( finite_finite_a @ ( B @ A3 ) ) )
=> ( finite179568208od_a_a @ ( product_Sigma_a_a @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_finite__SigmaI) ).
thf(308,axiom,
! [A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ A )
=> ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [B2: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ B2 @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_finite__Collect__subsets) ).
thf(315,axiom,
! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
| ( Q @ X2 ) ) ) )
= ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
& ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_finite__Collect__disjI) ).
thf(320,axiom,
! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) )
=> ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
& ( Q @ X2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_finite__Collect__conjI) ).
thf(327,axiom,
! [B: set_Product_prod_a_a,A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ B )
=> ( ( ord_le1824328871od_a_a @ A @ B )
=> ( finite179568208od_a_a @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_rev__finite__subset) ).
thf(330,axiom,
! [S: set_Product_prod_a_a,T: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ S @ T )
=> ( ~ ( finite179568208od_a_a @ S )
=> ~ ( finite179568208od_a_a @ T ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_infinite__super) ).
thf(335,axiom,
! [A: set_Product_prod_a_a,B: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ A @ B )
=> ( ( finite179568208od_a_a @ B )
=> ( finite179568208od_a_a @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_finite__subset) ).
thf(340,axiom,
! [G2: pair_p125712459t_unit] :
( ( pair_p1802376898raph_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_pair__fin__digraph_Opair__finite__arcs) ).
thf(343,axiom,
! [G2: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G2 ) )
=> ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) )
=> ( pair_p1864019935ioms_a @ G2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_pair__fin__digraph__axioms_Ointro) ).
thf(348,axiom,
( pair_p1864019935ioms_a
= ( ^ [G: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G ) )
& ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_pair__fin__digraph__axioms__def) ).
thf(353,axiom,
( ord_le1824328871od_a_a @ ( pair_p133601421t_unit @ g )
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062parcs_AG_A_092_060subseteq_062_Apverts_AG_A_092_060times_062_Apverts_AG_092_060close_062) ).
thf(354,axiom,
( finite179568208od_a_a
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062finite_A_Ipverts_AG_A_092_060times_062_Apverts_AG_J_092_060close_062) ).
thf(355,conjecture,
finite179568208od_a_a @ ( pair_p133601421t_unit @ g ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(356,negated_conjecture,
( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ g ) )
= $false ),
inference(negate_conjecture,[status(cth)],[355]) ).
thf(357,plain,
( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ g ) )
= $false ),
inference(unfold_def,[status(thm)],[356]) ).
thf(358,plain,
( ( ! [A: set_a,B: set_a] :
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) )
= ( ( A = bot_bot_set_a )
| ( B = bot_bot_set_a )
| ( ( finite_finite_a @ A )
& ( finite_finite_a @ B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[25]) ).
thf(359,plain,
( ( finite351630733od_a_a
= ( ^ [A5: set_Product_prod_a_a] :
( collec183727474od_a_a
@ ^ [X5: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ X5 @ A5 )
& ( finite179568208od_a_a @ X5 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[37]) ).
thf(360,plain,
( ( ! [Pverts: set_a,Parcs: set_Product_prod_a_a,More: product_unit] :
( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ Pverts @ Parcs @ More ) )
= Parcs ) )
= $true ),
inference(unfold_def,[status(thm)],[45]) ).
thf(361,plain,
( ( ! [R2: pair_p125712459t_unit] :
( R2
= ( pair_p1621517565t_unit @ ( pair_p1047056820t_unit @ R2 ) @ ( pair_p133601421t_unit @ R2 ) @ ( pair_p1896222615t_unit @ R2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[65]) ).
thf(362,plain,
( ( ! [R2: pair_p125712459t_unit,R3: pair_p125712459t_unit] :
( ( ( pair_p1047056820t_unit @ R2 )
= ( pair_p1047056820t_unit @ R3 ) )
=> ( ( ( pair_p133601421t_unit @ R2 )
= ( pair_p133601421t_unit @ R3 ) )
=> ( ( ( pair_p1896222615t_unit @ R2 )
= ( pair_p1896222615t_unit @ R3 ) )
=> ( R2 = R3 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[221]) ).
thf(363,plain,
( ( ! [A: set_nat,B: set_Product_prod_a_a] :
( ~ ( finite_finite_nat @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[249]) ).
thf(364,plain,
( ( ! [A: set_a,B: set_Product_prod_a_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[251]) ).
thf(365,plain,
( ( ! [A: set_Product_prod_a_a,B: set_nat] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_nat @ B )
=> ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[252]) ).
thf(366,plain,
( ( ! [A: set_Product_prod_a_a,B: set_a] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[253]) ).
thf(367,plain,
( ( ! [A: set_a,B: set_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[254]) ).
thf(368,plain,
( ( ! [G2: pair_p1765063010t_unit] :
( ( pair_p374947051od_a_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p447552203t_unit @ G2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[262]) ).
thf(369,plain,
( ( ! [A: set_nat,B: set_Product_prod_a_a] :
( ( finite_finite_nat @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[268]) ).
thf(370,plain,
( ( ! [A: set_a,B: set_Product_prod_a_a] :
( ( finite_finite_a @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[270]) ).
thf(371,plain,
( ( ! [A: set_Product_prod_a_a,B: set_nat] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_nat @ B )
=> ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[271]) ).
thf(372,plain,
( ( ! [A: set_Product_prod_a_a,B: set_a] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[272]) ).
thf(373,plain,
( ( ! [A: set_a,B: set_a] :
( ( finite_finite_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[273]) ).
thf(374,plain,
( ( ! [P: product_prod_a_a > $o] :
( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
=> ? [X_1: product_prod_a_a] : ( P @ X_1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[292]) ).
thf(375,plain,
( ( ! [A: set_a,B: a > set_a] :
( ( finite_finite_a @ A )
=> ( ! [A3: a] :
( ( member_a @ A3 @ A )
=> ( finite_finite_a @ ( B @ A3 ) ) )
=> ( finite179568208od_a_a @ ( product_Sigma_a_a @ A @ B ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[302]) ).
thf(376,plain,
( ( ! [A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ A )
=> ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [B2: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ B2 @ A ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[308]) ).
thf(377,plain,
( ( ! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
| ( Q @ X2 ) ) ) )
= ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
& ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[315]) ).
thf(378,plain,
( ( ! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) )
=> ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
& ( Q @ X2 ) ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[320]) ).
thf(379,plain,
( ( ! [B: set_Product_prod_a_a,A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ B )
=> ( ( ord_le1824328871od_a_a @ A @ B )
=> ( finite179568208od_a_a @ A ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[327]) ).
thf(380,plain,
( ( ! [S: set_Product_prod_a_a,T: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ S @ T )
=> ( ~ ( finite179568208od_a_a @ S )
=> ~ ( finite179568208od_a_a @ T ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[330]) ).
thf(381,plain,
( ( ! [A: set_Product_prod_a_a,B: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ A @ B )
=> ( ( finite179568208od_a_a @ B )
=> ( finite179568208od_a_a @ A ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[335]) ).
thf(382,plain,
( ( ! [G2: pair_p125712459t_unit] :
( ( pair_p1802376898raph_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[340]) ).
thf(383,plain,
( ( ! [G2: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G2 ) )
=> ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) )
=> ( pair_p1864019935ioms_a @ G2 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[343]) ).
thf(384,plain,
( ( pair_p1864019935ioms_a
= ( ^ [G: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G ) )
& ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[348]) ).
thf(385,plain,
( ( ord_le1824328871od_a_a @ ( pair_p133601421t_unit @ g )
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) )
= $true ),
inference(unfold_def,[status(thm)],[353]) ).
thf(386,plain,
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(387,plain,
( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ g ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[357]) ).
thf(388,plain,
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) )
= $true ),
inference(copy,[status(thm)],[386]) ).
thf(389,plain,
( ( ord_le1824328871od_a_a @ ( pair_p133601421t_unit @ g )
@ ( product_Sigma_a_a @ ( pair_p1047056820t_unit @ g )
@ ^ [Uu: a] : ( pair_p1047056820t_unit @ g ) ) )
= $true ),
inference(copy,[status(thm)],[385]) ).
thf(390,plain,
( ( pair_p1864019935ioms_a
= ( ^ [G: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G ) )
& ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[384]) ).
thf(391,plain,
( ( ! [G2: pair_p125712459t_unit] :
( ( finite_finite_a @ ( pair_p1047056820t_unit @ G2 ) )
=> ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) )
=> ( pair_p1864019935ioms_a @ G2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[383]) ).
thf(392,plain,
( ( ! [G2: pair_p125712459t_unit] :
( ( pair_p1802376898raph_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p133601421t_unit @ G2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[382]) ).
thf(393,plain,
( ( ! [A: set_Product_prod_a_a,B: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ A @ B )
=> ( ( finite179568208od_a_a @ B )
=> ( finite179568208od_a_a @ A ) ) ) )
= $true ),
inference(copy,[status(thm)],[381]) ).
thf(394,plain,
( ( ! [S: set_Product_prod_a_a,T: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ S @ T )
=> ( ~ ( finite179568208od_a_a @ S )
=> ~ ( finite179568208od_a_a @ T ) ) ) )
= $true ),
inference(copy,[status(thm)],[380]) ).
thf(395,plain,
( ( ! [B: set_Product_prod_a_a,A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ B )
=> ( ( ord_le1824328871od_a_a @ A @ B )
=> ( finite179568208od_a_a @ A ) ) ) )
= $true ),
inference(copy,[status(thm)],[379]) ).
thf(396,plain,
( ( ! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) )
=> ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
& ( Q @ X2 ) ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[378]) ).
thf(397,plain,
( ( ! [P: product_prod_a_a > $o,Q: product_prod_a_a > $o] :
( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [X2: product_prod_a_a] :
( ( P @ X2 )
| ( Q @ X2 ) ) ) )
= ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
& ( finite179568208od_a_a @ ( collec645855634od_a_a @ Q ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[377]) ).
thf(398,plain,
( ( ! [A: set_Product_prod_a_a] :
( ( finite179568208od_a_a @ A )
=> ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [B2: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ B2 @ A ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[376]) ).
thf(399,plain,
( ( ! [A: set_a,B: a > set_a] :
( ( finite_finite_a @ A )
=> ( ! [A3: a] :
( ( member_a @ A3 @ A )
=> ( finite_finite_a @ ( B @ A3 ) ) )
=> ( finite179568208od_a_a @ ( product_Sigma_a_a @ A @ B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[375]) ).
thf(400,plain,
( ( ! [P: product_prod_a_a > $o] :
( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ P ) )
=> ? [X_1: product_prod_a_a] : ( P @ X_1 ) ) )
= $true ),
inference(copy,[status(thm)],[374]) ).
thf(401,plain,
( ( ! [A: set_a,B: set_a] :
( ( finite_finite_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[373]) ).
thf(402,plain,
( ( ! [A: set_Product_prod_a_a,B: set_a] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_a @ B )
=> ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[372]) ).
thf(403,plain,
( ( ! [A: set_Product_prod_a_a,B: set_nat] :
( ( finite179568208od_a_a @ A )
=> ( ( finite_finite_nat @ B )
=> ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[371]) ).
thf(404,plain,
( ( ! [A: set_a,B: set_Product_prod_a_a] :
( ( finite_finite_a @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[370]) ).
thf(405,plain,
( ( ! [A: set_nat,B: set_Product_prod_a_a] :
( ( finite_finite_nat @ A )
=> ( ( finite179568208od_a_a @ B )
=> ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(406,plain,
( ( ! [G2: pair_p1765063010t_unit] :
( ( pair_p374947051od_a_a @ G2 )
=> ( finite179568208od_a_a @ ( pair_p447552203t_unit @ G2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(407,plain,
( ( ! [A: set_a,B: set_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(408,plain,
( ( ! [A: set_Product_prod_a_a,B: set_a] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_a @ B )
=> ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(409,plain,
( ( ! [A: set_Product_prod_a_a,B: set_nat] :
( ~ ( finite179568208od_a_a @ A )
=> ( ~ ( finite_finite_nat @ B )
=> ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ A
@ ^ [Uu: product_prod_a_a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(410,plain,
( ( ! [A: set_a,B: set_Product_prod_a_a] :
( ~ ( finite_finite_a @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ A
@ ^ [Uu: a] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(411,plain,
( ( ! [A: set_nat,B: set_Product_prod_a_a] :
( ~ ( finite_finite_nat @ A )
=> ( ~ ( finite179568208od_a_a @ B )
=> ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ A
@ ^ [Uu: nat] : B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(412,plain,
( ( ! [R2: pair_p125712459t_unit,R3: pair_p125712459t_unit] :
( ( ( pair_p1047056820t_unit @ R2 )
= ( pair_p1047056820t_unit @ R3 ) )
=> ( ( ( pair_p133601421t_unit @ R2 )
= ( pair_p133601421t_unit @ R3 ) )
=> ( ( ( pair_p1896222615t_unit @ R2 )
= ( pair_p1896222615t_unit @ R3 ) )
=> ( R2 = R3 ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(413,plain,
( ( ! [R2: pair_p125712459t_unit] :
( R2
= ( pair_p1621517565t_unit @ ( pair_p1047056820t_unit @ R2 ) @ ( pair_p133601421t_unit @ R2 ) @ ( pair_p1896222615t_unit @ R2 ) ) ) )
= $true ),
inference(copy,[status(thm)],[361]) ).
thf(414,plain,
( ( ! [Pverts: set_a,Parcs: set_Product_prod_a_a,More: product_unit] :
( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ Pverts @ Parcs @ More ) )
= Parcs ) )
= $true ),
inference(copy,[status(thm)],[360]) ).
thf(415,plain,
( ( finite351630733od_a_a
= ( ^ [A5: set_Product_prod_a_a] :
( collec183727474od_a_a
@ ^ [X5: set_Product_prod_a_a] :
( ( ord_le1824328871od_a_a @ X5 @ A5 )
& ( finite179568208od_a_a @ X5 ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[359]) ).
thf(416,plain,
( ( ! [A: set_a,B: set_a] :
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ A
@ ^ [Uu: a] : B ) )
= ( ( A = bot_bot_set_a )
| ( B = bot_bot_set_a )
| ( ( finite_finite_a @ A )
& ( finite_finite_a @ B ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[358]) ).
thf(417,plain,
( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ g ) ) )
= $true ),
inference(copy,[status(thm)],[387]) ).
thf(418,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_a] :
( ~ ~ ( finite179568208od_a_a @ SX0 )
| ~ ~ ( finite_finite_a @ SX1 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SX0
@ ^ [SX2: product_prod_a_a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[408]) ).
thf(419,plain,
( ( ! [SX0: pair_p1765063010t_unit] :
( ~ ( pair_p374947051od_a_a @ SX0 )
| ( finite179568208od_a_a @ ( pair_p447552203t_unit @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[406]) ).
thf(420,plain,
( ( ! [SX0: set_a,SX1: set_Product_prod_a_a] :
( ~ ~ ( finite_finite_a @ SX0 )
| ~ ~ ( finite179568208od_a_a @ SX1 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SX0
@ ^ [SX2: a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[410]) ).
thf(421,plain,
( ( ! [SX0: set_a,SX1: set_a] :
( ~ ( finite_finite_a @ SX0 )
| ~ ( finite_finite_a @ SX1 )
| ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SX0
@ ^ [SX2: a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[401]) ).
thf(422,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_Product_prod_a_a] :
( ~ ( ord_le1824328871od_a_a @ SX0 @ SX1 )
| ~ ( finite179568208od_a_a @ SX1 )
| ( finite179568208od_a_a @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[393]) ).
thf(423,plain,
( ( ! [SX0: set_nat,SX1: set_Product_prod_a_a] :
( ~ ~ ( finite_finite_nat @ SX0 )
| ~ ~ ( finite179568208od_a_a @ SX1 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SX0
@ ^ [SX2: nat] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[411]) ).
thf(424,plain,
( ( ! [SX0: product_prod_a_a > $o,SX1: product_prod_a_a > $o] :
( ~ ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SX0 ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ SX1 ) ) )
| ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SX2: product_prod_a_a] :
~ ( ~ ( SX0 @ SX2 )
| ~ ( SX1 @ SX2 ) ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[396]) ).
thf(425,plain,
( ( ! [SX0: product_prod_a_a > $o,SX1: product_prod_a_a > $o] :
( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SX2: product_prod_a_a] :
( ( SX0 @ SX2 )
| ( SX1 @ SX2 ) ) ) )
= ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SX0 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SX1 ) ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[397]) ).
thf(426,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_nat] :
( ~ ~ ( finite179568208od_a_a @ SX0 )
| ~ ~ ( finite_finite_nat @ SX1 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SX0
@ ^ [SX2: product_prod_a_a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[409]) ).
thf(427,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_Product_prod_a_a] :
( ~ ( ord_le1824328871od_a_a @ SX0 @ SX1 )
| ~ ~ ( finite179568208od_a_a @ SX0 )
| ~ ( finite179568208od_a_a @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[394]) ).
thf(428,plain,
( ( ! [SX0: set_nat,SX1: set_Product_prod_a_a] :
( ~ ( finite_finite_nat @ SX0 )
| ~ ( finite179568208od_a_a @ SX1 )
| ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SX0
@ ^ [SX2: nat] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[405]) ).
thf(429,plain,
( ( ! [SX0: pair_p125712459t_unit,SX1: pair_p125712459t_unit] :
( ( ( pair_p1047056820t_unit @ SX0 )
!= ( pair_p1047056820t_unit @ SX1 ) )
| ( ( pair_p133601421t_unit @ SX0 )
!= ( pair_p133601421t_unit @ SX1 ) )
| ( ( pair_p1896222615t_unit @ SX0 )
!= ( pair_p1896222615t_unit @ SX1 ) )
| ( SX0 = SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[412]) ).
thf(430,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_a] :
( ~ ( finite179568208od_a_a @ SX0 )
| ~ ( finite_finite_a @ SX1 )
| ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SX0
@ ^ [SX2: product_prod_a_a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[402]) ).
thf(431,plain,
( ( ! [SX0: product_prod_a_a > $o] :
( ~ ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SX0 ) )
| ~ ! [SX1: product_prod_a_a] :
~ ( SX0 @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[400]) ).
thf(432,plain,
( ( pair_p1864019935ioms_a
= ( ^ [SX0: pair_p125712459t_unit] :
~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SX0 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SX0 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[390]) ).
thf(433,plain,
( ( finite351630733od_a_a
= ( ^ [SX0: set_Product_prod_a_a] :
( collec183727474od_a_a
@ ^ [SX1: set_Product_prod_a_a] :
~ ( ~ ( ord_le1824328871od_a_a @ SX1 @ SX0 )
| ~ ( finite179568208od_a_a @ SX1 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[415]) ).
thf(434,plain,
( ( ! [SX0: set_a,SX1: set_a] :
( ~ ~ ( finite_finite_a @ SX0 )
| ~ ~ ( finite_finite_a @ SX1 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SX0
@ ^ [SX2: a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[407]) ).
thf(435,plain,
( ( ! [SX0: set_a,SX1: a > set_a] :
( ~ ( finite_finite_a @ SX0 )
| ~ ! [SX2: a] :
( ~ ( member_a @ SX2 @ SX0 )
| ( finite_finite_a @ ( SX1 @ SX2 ) ) )
| ( finite179568208od_a_a @ ( product_Sigma_a_a @ SX0 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[399]) ).
thf(436,plain,
( ( ! [SX0: set_Product_prod_a_a] :
( ~ ( finite179568208od_a_a @ SX0 )
| ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [SX1: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ SX1 @ SX0 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[398]) ).
thf(437,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_Product_prod_a_a] :
( ~ ( finite179568208od_a_a @ SX0 )
| ~ ( ord_le1824328871od_a_a @ SX1 @ SX0 )
| ( finite179568208od_a_a @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[395]) ).
thf(438,plain,
( ( ! [SX0: set_a,SX1: set_a] :
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SX0
@ ^ [SX2: a] : SX1 ) )
= ( ( SX0 = bot_bot_set_a )
| ( SX1 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SX0 )
| ~ ( finite_finite_a @ SX1 ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[416]) ).
thf(439,plain,
( ( ! [SX0: set_a,SX1: set_Product_prod_a_a] :
( ~ ( finite_finite_a @ SX0 )
| ~ ( finite179568208od_a_a @ SX1 )
| ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SX0
@ ^ [SX2: a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[404]) ).
thf(440,plain,
( ( ! [SX0: pair_p125712459t_unit] :
( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SX0 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SX0 ) )
| ( pair_p1864019935ioms_a @ SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[391]) ).
thf(441,plain,
( ( ! [SX0: pair_p125712459t_unit] :
( ~ ( pair_p1802376898raph_a @ SX0 )
| ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[392]) ).
thf(442,plain,
( ( ! [SX0: set_Product_prod_a_a,SX1: set_nat] :
( ~ ( finite179568208od_a_a @ SX0 )
| ~ ( finite_finite_nat @ SX1 )
| ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SX0
@ ^ [SX2: product_prod_a_a] : SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[403]) ).
thf(443,plain,
! [SV1: pair_p125712459t_unit] :
( ( SV1
= ( pair_p1621517565t_unit @ ( pair_p1047056820t_unit @ SV1 ) @ ( pair_p133601421t_unit @ SV1 ) @ ( pair_p1896222615t_unit @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[413]) ).
thf(444,plain,
! [SV2: set_a] :
( ( ! [SY66: set_Product_prod_a_a,SY67: product_unit] :
( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ SV2 @ SY66 @ SY67 ) )
= SY66 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[414]) ).
thf(445,plain,
( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ g ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[417]) ).
thf(446,plain,
! [SV3: set_Product_prod_a_a] :
( ( ! [SY68: set_a] :
( ~ ~ ( finite179568208od_a_a @ SV3 )
| ~ ~ ( finite_finite_a @ SY68 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SX2: product_prod_a_a] : SY68 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[418]) ).
thf(447,plain,
! [SV4: pair_p1765063010t_unit] :
( ( ~ ( pair_p374947051od_a_a @ SV4 )
| ( finite179568208od_a_a @ ( pair_p447552203t_unit @ SV4 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[419]) ).
thf(448,plain,
! [SV5: set_a] :
( ( ! [SY70: set_Product_prod_a_a] :
( ~ ~ ( finite_finite_a @ SV5 )
| ~ ~ ( finite179568208od_a_a @ SY70 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SX2: a] : SY70 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[420]) ).
thf(449,plain,
! [SV6: set_a] :
( ( ! [SY72: set_a] :
( ~ ( finite_finite_a @ SV6 )
| ~ ( finite_finite_a @ SY72 )
| ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SX2: a] : SY72 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[421]) ).
thf(450,plain,
! [SV7: set_Product_prod_a_a] :
( ( ! [SY74: set_Product_prod_a_a] :
( ~ ( ord_le1824328871od_a_a @ SV7 @ SY74 )
| ~ ( finite179568208od_a_a @ SY74 )
| ( finite179568208od_a_a @ SV7 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[422]) ).
thf(451,plain,
! [SV8: set_nat] :
( ( ! [SY75: set_Product_prod_a_a] :
( ~ ~ ( finite_finite_nat @ SV8 )
| ~ ~ ( finite179568208od_a_a @ SY75 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SX2: nat] : SY75 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[423]) ).
thf(452,plain,
! [SV9: product_prod_a_a > $o] :
( ( ! [SY77: product_prod_a_a > $o] :
( ~ ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV9 ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ SY77 ) ) )
| ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY78: product_prod_a_a] :
~ ( ~ ( SV9 @ SY78 )
| ~ ( SY77 @ SY78 ) ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[424]) ).
thf(453,plain,
! [SV10: product_prod_a_a > $o] :
( ( ! [SY79: product_prod_a_a > $o] :
( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY80: product_prod_a_a] :
( ( SV10 @ SY80 )
| ( SY79 @ SY80 ) ) ) )
= ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SY79 ) ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[425]) ).
thf(454,plain,
! [SV11: set_Product_prod_a_a] :
( ( ! [SY81: set_nat] :
( ~ ~ ( finite179568208od_a_a @ SV11 )
| ~ ~ ( finite_finite_nat @ SY81 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SX2: product_prod_a_a] : SY81 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[426]) ).
thf(455,plain,
! [SV12: set_Product_prod_a_a] :
( ( ! [SY83: set_Product_prod_a_a] :
( ~ ( ord_le1824328871od_a_a @ SV12 @ SY83 )
| ~ ~ ( finite179568208od_a_a @ SV12 )
| ~ ( finite179568208od_a_a @ SY83 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[427]) ).
thf(456,plain,
! [SV13: set_nat] :
( ( ! [SY84: set_Product_prod_a_a] :
( ~ ( finite_finite_nat @ SV13 )
| ~ ( finite179568208od_a_a @ SY84 )
| ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SX2: nat] : SY84 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[428]) ).
thf(457,plain,
! [SV14: pair_p125712459t_unit] :
( ( ! [SY86: pair_p125712459t_unit] :
( ( ( pair_p1047056820t_unit @ SV14 )
!= ( pair_p1047056820t_unit @ SY86 ) )
| ( ( pair_p133601421t_unit @ SV14 )
!= ( pair_p133601421t_unit @ SY86 ) )
| ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SY86 ) )
| ( SV14 = SY86 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[429]) ).
thf(458,plain,
! [SV15: set_Product_prod_a_a] :
( ( ! [SY87: set_a] :
( ~ ( finite179568208od_a_a @ SV15 )
| ~ ( finite_finite_a @ SY87 )
| ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SX2: product_prod_a_a] : SY87 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[430]) ).
thf(459,plain,
! [SV16: product_prod_a_a > $o] :
( ( ~ ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) )
| ~ ! [SY89: product_prod_a_a] :
~ ( SV16 @ SY89 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[431]) ).
thf(460,plain,
( ( ! [SV17: pair_p125712459t_unit] :
( ( pair_p1864019935ioms_a @ SV17 )
= ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV17 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV17 ) ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[432]) ).
thf(461,plain,
( ( pair_p1864019935ioms_a
= ( ^ [SX0: pair_p125712459t_unit] :
~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SX0 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SX0 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[432]) ).
thf(462,plain,
( ( ! [SV18: set_Product_prod_a_a] :
( ( finite351630733od_a_a @ SV18 )
= ( collec183727474od_a_a
@ ^ [SY90: set_Product_prod_a_a] :
~ ( ~ ( ord_le1824328871od_a_a @ SY90 @ SV18 )
| ~ ( finite179568208od_a_a @ SY90 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[433]) ).
thf(463,plain,
( ( finite351630733od_a_a
= ( ^ [SX0: set_Product_prod_a_a] :
( collec183727474od_a_a
@ ^ [SX1: set_Product_prod_a_a] :
~ ( ~ ( ord_le1824328871od_a_a @ SX1 @ SX0 )
| ~ ( finite179568208od_a_a @ SX1 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[433]) ).
thf(464,plain,
! [SV19: set_a] :
( ( ! [SY91: set_a] :
( ~ ~ ( finite_finite_a @ SV19 )
| ~ ~ ( finite_finite_a @ SY91 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SX2: a] : SY91 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[434]) ).
thf(465,plain,
! [SV20: set_a] :
( ( ! [SY93: a > set_a] :
( ~ ( finite_finite_a @ SV20 )
| ~ ! [SY94: a] :
( ~ ( member_a @ SY94 @ SV20 )
| ( finite_finite_a @ ( SY93 @ SY94 ) ) )
| ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SY93 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[435]) ).
thf(466,plain,
! [SV21: set_Product_prod_a_a] :
( ( ~ ( finite179568208od_a_a @ SV21 )
| ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [SY95: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ SY95 @ SV21 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[436]) ).
thf(467,plain,
! [SV22: set_Product_prod_a_a] :
( ( ! [SY96: set_Product_prod_a_a] :
( ~ ( finite179568208od_a_a @ SV22 )
| ~ ( ord_le1824328871od_a_a @ SY96 @ SV22 )
| ( finite179568208od_a_a @ SY96 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[437]) ).
thf(468,plain,
! [SV23: set_a] :
( ( ! [SY97: set_a] :
( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SX2: a] : SY97 ) )
= ( ( SV23 = bot_bot_set_a )
| ( SY97 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SY97 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[438]) ).
thf(469,plain,
! [SV24: set_a] :
( ( ! [SY99: set_Product_prod_a_a] :
( ~ ( finite_finite_a @ SV24 )
| ~ ( finite179568208od_a_a @ SY99 )
| ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SX2: a] : SY99 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[439]) ).
thf(470,plain,
! [SV25: pair_p125712459t_unit] :
( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV25 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV25 ) )
| ( pair_p1864019935ioms_a @ SV25 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[440]) ).
thf(471,plain,
! [SV26: pair_p125712459t_unit] :
( ( ~ ( pair_p1802376898raph_a @ SV26 )
| ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV26 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[441]) ).
thf(472,plain,
! [SV27: set_Product_prod_a_a] :
( ( ! [SY101: set_nat] :
( ~ ( finite179568208od_a_a @ SV27 )
| ~ ( finite_finite_nat @ SY101 )
| ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SX2: product_prod_a_a] : SY101 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[442]) ).
thf(473,plain,
! [SV28: set_Product_prod_a_a,SV2: set_a] :
( ( ! [SY103: product_unit] :
( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ SV2 @ SV28 @ SY103 ) )
= SV28 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[444]) ).
thf(474,plain,
! [SV29: set_a,SV3: set_Product_prod_a_a] :
( ( ~ ~ ( finite179568208od_a_a @ SV3 )
| ~ ~ ( finite_finite_a @ SV29 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[446]) ).
thf(475,plain,
! [SV4: pair_p1765063010t_unit] :
( ( ( ~ ( pair_p374947051od_a_a @ SV4 ) )
= $true )
| ( ( finite179568208od_a_a @ ( pair_p447552203t_unit @ SV4 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[447]) ).
thf(476,plain,
! [SV30: set_Product_prod_a_a,SV5: set_a] :
( ( ~ ~ ( finite_finite_a @ SV5 )
| ~ ~ ( finite179568208od_a_a @ SV30 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[448]) ).
thf(477,plain,
! [SV31: set_a,SV6: set_a] :
( ( ~ ( finite_finite_a @ SV6 )
| ~ ( finite_finite_a @ SV31 )
| ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SY106: a] : SV31 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[449]) ).
thf(478,plain,
! [SV32: set_Product_prod_a_a,SV7: set_Product_prod_a_a] :
( ( ~ ( ord_le1824328871od_a_a @ SV7 @ SV32 )
| ~ ( finite179568208od_a_a @ SV32 )
| ( finite179568208od_a_a @ SV7 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[450]) ).
thf(479,plain,
! [SV33: set_Product_prod_a_a,SV8: set_nat] :
( ( ~ ~ ( finite_finite_nat @ SV8 )
| ~ ~ ( finite179568208od_a_a @ SV33 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[451]) ).
thf(480,plain,
! [SV34: product_prod_a_a > $o,SV9: product_prod_a_a > $o] :
( ( ~ ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV9 ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV34 ) ) )
| ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY108: product_prod_a_a] :
~ ( ~ ( SV9 @ SY108 )
| ~ ( SV34 @ SY108 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[452]) ).
thf(481,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[453]) ).
thf(482,plain,
! [SV36: set_nat,SV11: set_Product_prod_a_a] :
( ( ~ ~ ( finite179568208od_a_a @ SV11 )
| ~ ~ ( finite_finite_nat @ SV36 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[454]) ).
thf(483,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ~ ( ord_le1824328871od_a_a @ SV12 @ SV37 )
| ~ ~ ( finite179568208od_a_a @ SV12 )
| ~ ( finite179568208od_a_a @ SV37 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[455]) ).
thf(484,plain,
! [SV38: set_Product_prod_a_a,SV13: set_nat] :
( ( ~ ( finite_finite_nat @ SV13 )
| ~ ( finite179568208od_a_a @ SV38 )
| ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SY111: nat] : SV38 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[456]) ).
thf(485,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p1047056820t_unit @ SV14 )
!= ( pair_p1047056820t_unit @ SV39 ) )
| ( ( pair_p133601421t_unit @ SV14 )
!= ( pair_p133601421t_unit @ SV39 ) )
| ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
| ( SV14 = SV39 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[457]) ).
thf(486,plain,
! [SV40: set_a,SV15: set_Product_prod_a_a] :
( ( ~ ( finite179568208od_a_a @ SV15 )
| ~ ( finite_finite_a @ SV40 )
| ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SY112: product_prod_a_a] : SV40 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[458]) ).
thf(487,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( ~ ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) ) )
= $true )
| ( ( ~ ! [SY89: product_prod_a_a] :
~ ( SV16 @ SY89 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[459]) ).
thf(488,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( pair_p1864019935ioms_a @ SV41 )
= ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[460]) ).
thf(489,plain,
! [SV42: set_Product_prod_a_a] :
( ( ( finite351630733od_a_a @ SV42 )
= ( collec183727474od_a_a
@ ^ [SY113: set_Product_prod_a_a] :
~ ( ~ ( ord_le1824328871od_a_a @ SY113 @ SV42 )
| ~ ( finite179568208od_a_a @ SY113 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[462]) ).
thf(490,plain,
! [SV43: set_a,SV19: set_a] :
( ( ~ ~ ( finite_finite_a @ SV19 )
| ~ ~ ( finite_finite_a @ SV43 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[464]) ).
thf(491,plain,
! [SV44: a > set_a,SV20: set_a] :
( ( ~ ( finite_finite_a @ SV20 )
| ~ ! [SY115: a] :
( ~ ( member_a @ SY115 @ SV20 )
| ( finite_finite_a @ ( SV44 @ SY115 ) ) )
| ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[465]) ).
thf(492,plain,
! [SV21: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV21 ) )
= $true )
| ( ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [SY95: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ SY95 @ SV21 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[466]) ).
thf(493,plain,
! [SV45: set_Product_prod_a_a,SV22: set_Product_prod_a_a] :
( ( ~ ( finite179568208od_a_a @ SV22 )
| ~ ( ord_le1824328871od_a_a @ SV45 @ SV22 )
| ( finite179568208od_a_a @ SV45 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[467]) ).
thf(494,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[468]) ).
thf(495,plain,
! [SV47: set_Product_prod_a_a,SV24: set_a] :
( ( ~ ( finite_finite_a @ SV24 )
| ~ ( finite179568208od_a_a @ SV47 )
| ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SY117: a] : SV47 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[469]) ).
thf(496,plain,
! [SV25: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV25 ) ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV25 ) )
| ( pair_p1864019935ioms_a @ SV25 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[470]) ).
thf(497,plain,
! [SV26: pair_p125712459t_unit] :
( ( ( ~ ( pair_p1802376898raph_a @ SV26 ) )
= $true )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV26 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[471]) ).
thf(498,plain,
! [SV48: set_nat,SV27: set_Product_prod_a_a] :
( ( ~ ( finite179568208od_a_a @ SV27 )
| ~ ( finite_finite_nat @ SV48 )
| ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SY118: product_prod_a_a] : SV48 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[472]) ).
thf(499,plain,
! [SV49: product_unit,SV28: set_Product_prod_a_a,SV2: set_a] :
( ( ( pair_p133601421t_unit @ ( pair_p1621517565t_unit @ SV2 @ SV28 @ SV49 ) )
= SV28 )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[473]) ).
thf(500,plain,
! [SV29: set_a,SV3: set_Product_prod_a_a] :
( ( ( ~ ~ ( finite179568208od_a_a @ SV3 ) )
= $true )
| ( ( ~ ~ ( finite_finite_a @ SV29 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[474]) ).
thf(501,plain,
! [SV4: pair_p1765063010t_unit] :
( ( ( pair_p374947051od_a_a @ SV4 )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p447552203t_unit @ SV4 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[475]) ).
thf(502,plain,
! [SV30: set_Product_prod_a_a,SV5: set_a] :
( ( ( ~ ~ ( finite_finite_a @ SV5 ) )
= $true )
| ( ( ~ ~ ( finite179568208od_a_a @ SV30 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[476]) ).
thf(503,plain,
! [SV31: set_a,SV6: set_a] :
( ( ( ~ ( finite_finite_a @ SV6 ) )
= $true )
| ( ( ~ ( finite_finite_a @ SV31 )
| ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SY106: a] : SV31 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[477]) ).
thf(504,plain,
! [SV32: set_Product_prod_a_a,SV7: set_Product_prod_a_a] :
( ( ( ~ ( ord_le1824328871od_a_a @ SV7 @ SV32 ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ SV32 )
| ( finite179568208od_a_a @ SV7 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[478]) ).
thf(505,plain,
! [SV33: set_Product_prod_a_a,SV8: set_nat] :
( ( ( ~ ~ ( finite_finite_nat @ SV8 ) )
= $true )
| ( ( ~ ~ ( finite179568208od_a_a @ SV33 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[479]) ).
thf(506,plain,
! [SV34: product_prod_a_a > $o,SV9: product_prod_a_a > $o] :
( ( ( ~ ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV9 ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV34 ) ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY108: product_prod_a_a] :
~ ( ~ ( SV9 @ SY108 )
| ~ ( SV34 @ SY108 ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[480]) ).
thf(507,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ~ ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
| ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[481]) ).
thf(508,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[481]) ).
thf(509,plain,
! [SV36: set_nat,SV11: set_Product_prod_a_a] :
( ( ( ~ ~ ( finite179568208od_a_a @ SV11 ) )
= $true )
| ( ( ~ ~ ( finite_finite_nat @ SV36 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[482]) ).
thf(510,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ( ~ ( ord_le1824328871od_a_a @ SV12 @ SV37 ) )
= $true )
| ( ( ~ ~ ( finite179568208od_a_a @ SV12 )
| ~ ( finite179568208od_a_a @ SV37 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[483]) ).
thf(511,plain,
! [SV38: set_Product_prod_a_a,SV13: set_nat] :
( ( ( ~ ( finite_finite_nat @ SV13 ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ SV38 )
| ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SY111: nat] : SV38 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[484]) ).
thf(512,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p1047056820t_unit @ SV14 )
!= ( pair_p1047056820t_unit @ SV39 ) )
= $true )
| ( ( ( ( pair_p133601421t_unit @ SV14 )
!= ( pair_p133601421t_unit @ SV39 ) )
| ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
| ( SV14 = SV39 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[485]) ).
thf(513,plain,
! [SV40: set_a,SV15: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV15 ) )
= $true )
| ( ( ~ ( finite_finite_a @ SV40 )
| ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SY112: product_prod_a_a] : SV40 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[486]) ).
thf(514,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) ) )
= $false )
| ( ( ~ ! [SY89: product_prod_a_a] :
~ ( SV16 @ SY89 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[487]) ).
thf(515,plain,
! [SV41: pair_p125712459t_unit] :
( ( ~ ( ( pair_p1864019935ioms_a @ SV41 )
| ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
| ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[488]) ).
thf(516,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( pair_p1864019935ioms_a @ SV41 )
= ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[488]) ).
thf(517,plain,
! [SV43: set_a,SV19: set_a] :
( ( ( ~ ~ ( finite_finite_a @ SV19 ) )
= $true )
| ( ( ~ ~ ( finite_finite_a @ SV43 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[490]) ).
thf(518,plain,
! [SV44: a > set_a,SV20: set_a] :
( ( ( ~ ( finite_finite_a @ SV20 ) )
= $true )
| ( ( ~ ! [SY115: a] :
( ~ ( member_a @ SY115 @ SV20 )
| ( finite_finite_a @ ( SV44 @ SY115 ) ) )
| ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[491]) ).
thf(519,plain,
! [SV21: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV21 )
= $false )
| ( ( finite1145471536od_a_a
@ ( collec183727474od_a_a
@ ^ [SY95: set_Product_prod_a_a] : ( ord_le1824328871od_a_a @ SY95 @ SV21 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[492]) ).
thf(520,plain,
! [SV45: set_Product_prod_a_a,SV22: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV22 ) )
= $true )
| ( ( ~ ( ord_le1824328871od_a_a @ SV45 @ SV22 )
| ( finite179568208od_a_a @ SV45 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[493]) ).
thf(521,plain,
! [SV46: set_a,SV23: set_a] :
( ( ~ ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
| ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[494]) ).
thf(522,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[494]) ).
thf(523,plain,
! [SV47: set_Product_prod_a_a,SV24: set_a] :
( ( ( ~ ( finite_finite_a @ SV24 ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ SV47 )
| ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SY117: a] : SV47 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[495]) ).
thf(524,plain,
! [SV25: pair_p125712459t_unit] :
( ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV25 ) )
= $false )
| ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV25 ) )
| ( pair_p1864019935ioms_a @ SV25 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[496]) ).
thf(525,plain,
! [SV26: pair_p125712459t_unit] :
( ( ( pair_p1802376898raph_a @ SV26 )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV26 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[497]) ).
thf(526,plain,
! [SV48: set_nat,SV27: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV27 ) )
= $true )
| ( ( ~ ( finite_finite_nat @ SV48 )
| ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SY118: product_prod_a_a] : SV48 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[498]) ).
thf(527,plain,
! [SV29: set_a,SV3: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV3 ) )
= $false )
| ( ( ~ ~ ( finite_finite_a @ SV29 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[500]) ).
thf(528,plain,
! [SV30: set_Product_prod_a_a,SV5: set_a] :
( ( ( ~ ( finite_finite_a @ SV5 ) )
= $false )
| ( ( ~ ~ ( finite179568208od_a_a @ SV30 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[502]) ).
thf(529,plain,
! [SV31: set_a,SV6: set_a] :
( ( ( finite_finite_a @ SV6 )
= $false )
| ( ( ~ ( finite_finite_a @ SV31 )
| ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SY106: a] : SV31 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[503]) ).
thf(530,plain,
! [SV32: set_Product_prod_a_a,SV7: set_Product_prod_a_a] :
( ( ( ord_le1824328871od_a_a @ SV7 @ SV32 )
= $false )
| ( ( ~ ( finite179568208od_a_a @ SV32 )
| ( finite179568208od_a_a @ SV7 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[504]) ).
thf(531,plain,
! [SV33: set_Product_prod_a_a,SV8: set_nat] :
( ( ( ~ ( finite_finite_nat @ SV8 ) )
= $false )
| ( ( ~ ~ ( finite179568208od_a_a @ SV33 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[505]) ).
thf(532,plain,
! [SV34: product_prod_a_a > $o,SV9: product_prod_a_a > $o] :
( ( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV9 ) )
| ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV34 ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY108: product_prod_a_a] :
~ ( ~ ( SV9 @ SY108 )
| ~ ( SV34 @ SY108 ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[506]) ).
thf(533,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[507]) ).
thf(534,plain,
! [SV36: set_nat,SV11: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV11 ) )
= $false )
| ( ( ~ ~ ( finite_finite_nat @ SV36 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[509]) ).
thf(535,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ( ord_le1824328871od_a_a @ SV12 @ SV37 )
= $false )
| ( ( ~ ~ ( finite179568208od_a_a @ SV12 )
| ~ ( finite179568208od_a_a @ SV37 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[510]) ).
thf(536,plain,
! [SV38: set_Product_prod_a_a,SV13: set_nat] :
( ( ( finite_finite_nat @ SV13 )
= $false )
| ( ( ~ ( finite179568208od_a_a @ SV38 )
| ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SY111: nat] : SV38 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[511]) ).
thf(537,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p1047056820t_unit @ SV14 )
= ( pair_p1047056820t_unit @ SV39 ) )
= $false )
| ( ( ( ( pair_p133601421t_unit @ SV14 )
!= ( pair_p133601421t_unit @ SV39 ) )
| ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
| ( SV14 = SV39 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[512]) ).
thf(538,plain,
! [SV40: set_a,SV15: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV15 )
= $false )
| ( ( ~ ( finite_finite_a @ SV40 )
| ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SY112: product_prod_a_a] : SV40 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[513]) ).
thf(539,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) )
= $true )
| ( ( ~ ! [SY89: product_prod_a_a] :
~ ( SV16 @ SY89 ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[514]) ).
thf(540,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( ( pair_p1864019935ioms_a @ SV41 )
| ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[515]) ).
thf(541,plain,
! [SV43: set_a,SV19: set_a] :
( ( ( ~ ( finite_finite_a @ SV19 ) )
= $false )
| ( ( ~ ~ ( finite_finite_a @ SV43 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[517]) ).
thf(542,plain,
! [SV44: a > set_a,SV20: set_a] :
( ( ( finite_finite_a @ SV20 )
= $false )
| ( ( ~ ! [SY115: a] :
( ~ ( member_a @ SY115 @ SV20 )
| ( finite_finite_a @ ( SV44 @ SY115 ) ) )
| ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[518]) ).
thf(543,plain,
! [SV45: set_Product_prod_a_a,SV22: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV22 )
= $false )
| ( ( ~ ( ord_le1824328871od_a_a @ SV45 @ SV22 )
| ( finite179568208od_a_a @ SV45 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[520]) ).
thf(544,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[521]) ).
thf(545,plain,
! [SV47: set_Product_prod_a_a,SV24: set_a] :
( ( ( finite_finite_a @ SV24 )
= $false )
| ( ( ~ ( finite179568208od_a_a @ SV47 )
| ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SY117: a] : SV47 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[523]) ).
thf(546,plain,
! [SV25: pair_p125712459t_unit] :
( ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV25 ) ) )
= $true )
| ( ( pair_p1864019935ioms_a @ SV25 )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV25 ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[524]) ).
thf(547,plain,
! [SV48: set_nat,SV27: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV27 )
= $false )
| ( ( ~ ( finite_finite_nat @ SV48 )
| ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SY118: product_prod_a_a] : SV48 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[526]) ).
thf(548,plain,
! [SV29: set_a,SV3: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV3 )
= $true )
| ( ( ~ ~ ( finite_finite_a @ SV29 )
| ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[527]) ).
thf(549,plain,
! [SV30: set_Product_prod_a_a,SV5: set_a] :
( ( ( finite_finite_a @ SV5 )
= $true )
| ( ( ~ ~ ( finite179568208od_a_a @ SV30 )
| ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[528]) ).
thf(550,plain,
! [SV6: set_a,SV31: set_a] :
( ( ( ~ ( finite_finite_a @ SV31 ) )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SY106: a] : SV31 ) )
= $true )
| ( ( finite_finite_a @ SV6 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[529]) ).
thf(551,plain,
! [SV7: set_Product_prod_a_a,SV32: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV32 ) )
= $true )
| ( ( finite179568208od_a_a @ SV7 )
= $true )
| ( ( ord_le1824328871od_a_a @ SV7 @ SV32 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[530]) ).
thf(552,plain,
! [SV33: set_Product_prod_a_a,SV8: set_nat] :
( ( ( finite_finite_nat @ SV8 )
= $true )
| ( ( ~ ~ ( finite179568208od_a_a @ SV33 )
| ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[531]) ).
thf(553,plain,
! [SV34: product_prod_a_a > $o,SV9: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV9 ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY108: product_prod_a_a] :
~ ( ~ ( SV9 @ SY108 )
| ~ ( SV34 @ SY108 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[532]) ).
thf(554,plain,
! [SV9: product_prod_a_a > $o,SV34: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV34 ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY108: product_prod_a_a] :
~ ( ~ ( SV9 @ SY108 )
| ~ ( SV34 @ SY108 ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[532]) ).
thf(555,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[533]) ).
thf(556,plain,
! [SV36: set_nat,SV11: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV11 )
= $true )
| ( ( ~ ~ ( finite_finite_nat @ SV36 )
| ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[534]) ).
thf(557,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ( ~ ~ ( finite179568208od_a_a @ SV12 ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ SV37 ) )
= $true )
| ( ( ord_le1824328871od_a_a @ SV12 @ SV37 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[535]) ).
thf(558,plain,
! [SV13: set_nat,SV38: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV38 ) )
= $true )
| ( ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SY111: nat] : SV38 ) )
= $true )
| ( ( finite_finite_nat @ SV13 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[536]) ).
thf(559,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p133601421t_unit @ SV14 )
!= ( pair_p133601421t_unit @ SV39 ) )
= $true )
| ( ( ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
| ( SV14 = SV39 ) )
= $true )
| ( ( ( pair_p1047056820t_unit @ SV14 )
= ( pair_p1047056820t_unit @ SV39 ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[537]) ).
thf(560,plain,
! [SV15: set_Product_prod_a_a,SV40: set_a] :
( ( ( ~ ( finite_finite_a @ SV40 ) )
= $true )
| ( ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SY112: product_prod_a_a] : SV40 ) )
= $true )
| ( ( finite179568208od_a_a @ SV15 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[538]) ).
thf(561,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( ! [SY89: product_prod_a_a] :
~ ( SV16 @ SY89 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[539]) ).
thf(562,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ( pair_p1864019935ioms_a @ SV41 )
| ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[540]) ).
thf(563,plain,
! [SV43: set_a,SV19: set_a] :
( ( ( finite_finite_a @ SV19 )
= $true )
| ( ( ~ ~ ( finite_finite_a @ SV43 )
| ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[541]) ).
thf(564,plain,
! [SV44: a > set_a,SV20: set_a] :
( ( ( ~ ! [SY115: a] :
( ~ ( member_a @ SY115 @ SV20 )
| ( finite_finite_a @ ( SV44 @ SY115 ) ) ) )
= $true )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[542]) ).
thf(565,plain,
! [SV22: set_Product_prod_a_a,SV45: set_Product_prod_a_a] :
( ( ( ~ ( ord_le1824328871od_a_a @ SV45 @ SV22 ) )
= $true )
| ( ( finite179568208od_a_a @ SV45 )
= $true )
| ( ( finite179568208od_a_a @ SV22 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[543]) ).
thf(566,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[544]) ).
thf(567,plain,
! [SV24: set_a,SV47: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV47 ) )
= $true )
| ( ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SY117: a] : SV47 ) )
= $true )
| ( ( finite_finite_a @ SV24 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[545]) ).
thf(568,plain,
! [SV25: pair_p125712459t_unit] :
( ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV25 ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV25 )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV25 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[546]) ).
thf(569,plain,
! [SV27: set_Product_prod_a_a,SV48: set_nat] :
( ( ( ~ ( finite_finite_nat @ SV48 ) )
= $true )
| ( ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SY118: product_prod_a_a] : SV48 ) )
= $true )
| ( ( finite179568208od_a_a @ SV27 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[547]) ).
thf(570,plain,
! [SV3: set_Product_prod_a_a,SV29: set_a] :
( ( ( ~ ~ ( finite_finite_a @ SV29 ) )
= $true )
| ( ( ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV3 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[548]) ).
thf(571,plain,
! [SV5: set_a,SV30: set_Product_prod_a_a] :
( ( ( ~ ~ ( finite179568208od_a_a @ SV30 ) )
= $true )
| ( ( ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true )
| ( ( finite_finite_a @ SV5 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[549]) ).
thf(572,plain,
! [SV6: set_a,SV31: set_a] :
( ( ( finite_finite_a @ SV31 )
= $false )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV6
@ ^ [SY106: a] : SV31 ) )
= $true )
| ( ( finite_finite_a @ SV6 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[550]) ).
thf(573,plain,
! [SV7: set_Product_prod_a_a,SV32: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV32 )
= $false )
| ( ( finite179568208od_a_a @ SV7 )
= $true )
| ( ( ord_le1824328871od_a_a @ SV7 @ SV32 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[551]) ).
thf(574,plain,
! [SV8: set_nat,SV33: set_Product_prod_a_a] :
( ( ( ~ ~ ( finite179568208od_a_a @ SV33 ) )
= $true )
| ( ( ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true )
| ( ( finite_finite_nat @ SV8 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[552]) ).
thf(575,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[555]) ).
thf(576,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[555]) ).
thf(577,plain,
! [SV11: set_Product_prod_a_a,SV36: set_nat] :
( ( ( ~ ~ ( finite_finite_nat @ SV36 ) )
= $true )
| ( ( ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV11 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[556]) ).
thf(578,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV12 ) )
= $false )
| ( ( ~ ( finite179568208od_a_a @ SV37 ) )
= $true )
| ( ( ord_le1824328871od_a_a @ SV12 @ SV37 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[557]) ).
thf(579,plain,
! [SV13: set_nat,SV38: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV38 )
= $false )
| ( ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV13
@ ^ [SY111: nat] : SV38 ) )
= $true )
| ( ( finite_finite_nat @ SV13 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[558]) ).
thf(580,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p133601421t_unit @ SV14 )
= ( pair_p133601421t_unit @ SV39 ) )
= $false )
| ( ( ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
| ( SV14 = SV39 ) )
= $true )
| ( ( ( pair_p1047056820t_unit @ SV14 )
= ( pair_p1047056820t_unit @ SV39 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[559]) ).
thf(581,plain,
! [SV15: set_Product_prod_a_a,SV40: set_a] :
( ( ( finite_finite_a @ SV40 )
= $false )
| ( ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV15
@ ^ [SY112: product_prod_a_a] : SV40 ) )
= $true )
| ( ( finite179568208od_a_a @ SV15 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[560]) ).
thf(582,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( ~ ( SV16 @ ( sK1_SY89 @ SV16 ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[561]) ).
thf(583,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( pair_p1864019935ioms_a @ SV41 )
= $false )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[562]) ).
thf(584,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[562]) ).
thf(585,plain,
! [SV19: set_a,SV43: set_a] :
( ( ( ~ ~ ( finite_finite_a @ SV43 ) )
= $true )
| ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true )
| ( ( finite_finite_a @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[563]) ).
thf(586,plain,
! [SV44: a > set_a,SV20: set_a] :
( ( ( ! [SY115: a] :
( ~ ( member_a @ SY115 @ SV20 )
| ( finite_finite_a @ ( SV44 @ SY115 ) ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[564]) ).
thf(587,plain,
! [SV22: set_Product_prod_a_a,SV45: set_Product_prod_a_a] :
( ( ( ord_le1824328871od_a_a @ SV45 @ SV22 )
= $false )
| ( ( finite179568208od_a_a @ SV45 )
= $true )
| ( ( finite179568208od_a_a @ SV22 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[565]) ).
thf(588,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[566]) ).
thf(589,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[566]) ).
thf(590,plain,
! [SV24: set_a,SV47: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV47 )
= $false )
| ( ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV24
@ ^ [SY117: a] : SV47 ) )
= $true )
| ( ( finite_finite_a @ SV24 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[567]) ).
thf(591,plain,
! [SV27: set_Product_prod_a_a,SV48: set_nat] :
( ( ( finite_finite_nat @ SV48 )
= $false )
| ( ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV27
@ ^ [SY118: product_prod_a_a] : SV48 ) )
= $true )
| ( ( finite179568208od_a_a @ SV27 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[569]) ).
thf(592,plain,
! [SV3: set_Product_prod_a_a,SV29: set_a] :
( ( ( ~ ( finite_finite_a @ SV29 ) )
= $false )
| ( ( ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV3 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[570]) ).
thf(593,plain,
! [SV5: set_a,SV30: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV30 ) )
= $false )
| ( ( ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true )
| ( ( finite_finite_a @ SV5 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[571]) ).
thf(594,plain,
! [SV8: set_nat,SV33: set_Product_prod_a_a] :
( ( ( ~ ( finite179568208od_a_a @ SV33 ) )
= $false )
| ( ( ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true )
| ( ( finite_finite_nat @ SV8 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[574]) ).
thf(595,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[575]) ).
thf(596,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[576]) ).
thf(597,plain,
! [SV11: set_Product_prod_a_a,SV36: set_nat] :
( ( ( ~ ( finite_finite_nat @ SV36 ) )
= $false )
| ( ( ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV11 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[577]) ).
thf(598,plain,
! [SV37: set_Product_prod_a_a,SV12: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV12 )
= $true )
| ( ( ~ ( finite179568208od_a_a @ SV37 ) )
= $true )
| ( ( ord_le1824328871od_a_a @ SV12 @ SV37 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[578]) ).
thf(599,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p1896222615t_unit @ SV14 )
!= ( pair_p1896222615t_unit @ SV39 ) )
= $true )
| ( ( SV14 = SV39 )
= $true )
| ( ( ( pair_p133601421t_unit @ SV14 )
= ( pair_p133601421t_unit @ SV39 ) )
= $false )
| ( ( ( pair_p1047056820t_unit @ SV14 )
= ( pair_p1047056820t_unit @ SV39 ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[580]) ).
thf(600,plain,
! [SV16: product_prod_a_a > $o] :
( ( ( SV16 @ ( sK1_SY89 @ SV16 ) )
= $true )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV16 ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[582]) ).
thf(601,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[583]) ).
thf(602,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $true )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[584]) ).
thf(603,plain,
! [SV19: set_a,SV43: set_a] :
( ( ( ~ ( finite_finite_a @ SV43 ) )
= $false )
| ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true )
| ( ( finite_finite_a @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[585]) ).
thf(604,plain,
! [SV20: set_a,SV44: a > set_a] :
( ( ( ~ ( member_a @ ( sK2_SY115 @ SV44 @ SV20 ) @ SV20 )
| ( finite_finite_a @ ( SV44 @ ( sK2_SY115 @ SV44 @ SV20 ) ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_forall_neg,[status(esa)],[586]) ).
thf(605,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[588]) ).
thf(606,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[589]) ).
thf(607,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[589]) ).
thf(608,plain,
! [SV3: set_Product_prod_a_a,SV29: set_a] :
( ( ( finite_finite_a @ SV29 )
= $true )
| ( ( ~ ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV3 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[592]) ).
thf(609,plain,
! [SV5: set_a,SV30: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV30 )
= $true )
| ( ( ~ ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) ) )
= $true )
| ( ( finite_finite_a @ SV5 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[593]) ).
thf(610,plain,
! [SV8: set_nat,SV33: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV33 )
= $true )
| ( ( ~ ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) ) )
= $true )
| ( ( finite_finite_nat @ SV8 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[594]) ).
thf(611,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[595]) ).
thf(612,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[595]) ).
thf(613,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[596]) ).
thf(614,plain,
! [SV11: set_Product_prod_a_a,SV36: set_nat] :
( ( ( finite_finite_nat @ SV36 )
= $true )
| ( ( ~ ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) ) )
= $true )
| ( ( finite179568208od_a_a @ SV11 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[597]) ).
thf(615,plain,
! [SV12: set_Product_prod_a_a,SV37: set_Product_prod_a_a] :
( ( ( finite179568208od_a_a @ SV37 )
= $false )
| ( ( finite179568208od_a_a @ SV12 )
= $true )
| ( ( ord_le1824328871od_a_a @ SV12 @ SV37 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[598]) ).
thf(616,plain,
! [SV39: pair_p125712459t_unit,SV14: pair_p125712459t_unit] :
( ( ( ( pair_p1896222615t_unit @ SV14 )
= ( pair_p1896222615t_unit @ SV39 ) )
= $false )
| ( ( SV14 = SV39 )
= $true )
| ( ( ( pair_p133601421t_unit @ SV14 )
= ( pair_p133601421t_unit @ SV39 ) )
= $false )
| ( ( ( pair_p1047056820t_unit @ SV14 )
= ( pair_p1047056820t_unit @ SV39 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[599]) ).
thf(617,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( pair_p1864019935ioms_a @ SV41 ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[601]) ).
thf(618,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[601]) ).
thf(619,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) ) )
= $true )
| ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $true )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[602]) ).
thf(620,plain,
! [SV19: set_a,SV43: set_a] :
( ( ( finite_finite_a @ SV43 )
= $true )
| ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) ) )
= $true )
| ( ( finite_finite_a @ SV19 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[603]) ).
thf(621,plain,
! [SV20: set_a,SV44: a > set_a] :
( ( ( ~ ( member_a @ ( sK2_SY115 @ SV44 @ SV20 ) @ SV20 ) )
= $false )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[604]) ).
thf(622,plain,
! [SV20: set_a,SV44: a > set_a] :
( ( ( finite_finite_a @ ( SV44 @ ( sK2_SY115 @ SV44 @ SV20 ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[604]) ).
thf(623,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[605]) ).
thf(624,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[605]) ).
thf(625,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( SV23 = bot_bot_set_a )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[606]) ).
thf(626,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( SV46 = bot_bot_set_a )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[606]) ).
thf(627,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[607]) ).
thf(628,plain,
! [SV29: set_a,SV3: set_Product_prod_a_a] :
( ( ( finite1919032935_a_a_a
@ ( produc1282482655_a_a_a @ SV3
@ ^ [SY104: product_prod_a_a] : SV29 ) )
= $false )
| ( ( finite_finite_a @ SV29 )
= $true )
| ( ( finite179568208od_a_a @ SV3 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[608]) ).
thf(629,plain,
! [SV30: set_Product_prod_a_a,SV5: set_a] :
( ( ( finite676513017od_a_a
@ ( produc520147185od_a_a @ SV5
@ ^ [SY105: a] : SV30 ) )
= $false )
| ( ( finite179568208od_a_a @ SV30 )
= $true )
| ( ( finite_finite_a @ SV5 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[609]) ).
thf(630,plain,
! [SV33: set_Product_prod_a_a,SV8: set_nat] :
( ( ( finite1297454819od_a_a
@ ( produc1182842125od_a_a @ SV8
@ ^ [SY107: nat] : SV33 ) )
= $false )
| ( ( finite179568208od_a_a @ SV33 )
= $true )
| ( ( finite_finite_nat @ SV8 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[610]) ).
thf(631,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[611]) ).
thf(632,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[612]) ).
thf(633,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[613]) ).
thf(634,plain,
! [SV36: set_nat,SV11: set_Product_prod_a_a] :
( ( ( finite1837575485_a_nat
@ ( produc931712687_a_nat @ SV11
@ ^ [SY110: product_prod_a_a] : SV36 ) )
= $false )
| ( ( finite_finite_nat @ SV36 )
= $true )
| ( ( finite179568208od_a_a @ SV11 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[614]) ).
thf(635,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( pair_p1864019935ioms_a @ SV41 )
= $true )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[617]) ).
thf(636,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $true )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[618]) ).
thf(637,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $true )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[619]) ).
thf(638,plain,
! [SV43: set_a,SV19: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV19
@ ^ [SY114: a] : SV43 ) )
= $false )
| ( ( finite_finite_a @ SV43 )
= $true )
| ( ( finite_finite_a @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[620]) ).
thf(639,plain,
! [SV20: set_a,SV44: a > set_a] :
( ( ( member_a @ ( sK2_SY115 @ SV44 @ SV20 ) @ SV20 )
= $true )
| ( ( finite179568208od_a_a @ ( product_Sigma_a_a @ SV20 @ SV44 ) )
= $true )
| ( ( finite_finite_a @ SV20 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[621]) ).
thf(640,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[623]) ).
thf(641,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[624]) ).
thf(642,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[625]) ).
thf(643,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[626]) ).
thf(644,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 ) )
= $true )
| ( ( ~ ( finite_finite_a @ SV46 ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[627]) ).
thf(645,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[632]) ).
thf(646,plain,
! [SV10: product_prod_a_a > $o,SV35: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[633]) ).
thf(647,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[636]) ).
thf(648,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( ~ ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[637]) ).
thf(649,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a ) )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[641]) ).
thf(650,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) ) )
= $false )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[642]) ).
thf(651,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[642]) ).
thf(652,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[643]) ).
thf(653,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[643]) ).
thf(654,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite_finite_a @ SV23 )
= $false )
| ( ( ~ ( finite_finite_a @ SV46 ) )
= $true )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[644]) ).
thf(655,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[645]) ).
thf(656,plain,
! [SV10: product_prod_a_a > $o,SV35: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $false )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[645]) ).
thf(657,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
| ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[646]) ).
thf(658,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[647]) ).
thf(659,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $false )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[647]) ).
thf(660,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( pair_p1864019935ioms_a @ SV41 )
| ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[648]) ).
thf(661,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[649]) ).
thf(662,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[650]) ).
thf(663,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[651]) ).
thf(664,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[652]) ).
thf(665,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[653]) ).
thf(666,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( finite_finite_a @ SV46 )
= $false )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( ~ ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[654]) ).
thf(667,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $true )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[655]) ).
thf(668,plain,
! [SV10: product_prod_a_a > $o,SV35: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $true )
| ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[656]) ).
thf(669,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[657]) ).
thf(670,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[657]) ).
thf(671,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $true )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[658]) ).
thf(672,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $true )
| ( ( pair_p1864019935ioms_a @ SV41 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[659]) ).
thf(673,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( pair_p1864019935ioms_a @ SV41 ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[660]) ).
thf(674,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[660]) ).
thf(675,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[661]) ).
thf(676,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a ) )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[663]) ).
thf(677,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a ) )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[665]) ).
thf(678,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
| ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[666]) ).
thf(679,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a
@ ( collec645855634od_a_a
@ ^ [SY109: product_prod_a_a] :
( ( SV10 @ SY109 )
| ( SV35 @ SY109 ) ) ) )
= $true )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[669]) ).
thf(680,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) ) )
= $true )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[670]) ).
thf(681,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( pair_p1864019935ioms_a @ SV41 )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[673]) ).
thf(682,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) ) )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[674]) ).
thf(683,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[675]) ).
thf(684,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[675]) ).
thf(685,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[676]) ).
thf(686,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[677]) ).
thf(687,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) ) )
= $false )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[678]) ).
thf(688,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) ) )
= $false )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[678]) ).
thf(689,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
| ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[680]) ).
thf(690,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
| ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[682]) ).
thf(691,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite_finite_a @ SV23 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[683]) ).
thf(692,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( finite_finite_a @ SV46 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[684]) ).
thf(693,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[685]) ).
thf(694,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[686]) ).
thf(695,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite179568208od_a_a
@ ( product_Sigma_a_a @ SV23
@ ^ [SY116: a] : SV46 ) )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[687]) ).
thf(696,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a )
| ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[688]) ).
thf(697,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[689]) ).
thf(698,plain,
! [SV10: product_prod_a_a > $o,SV35: product_prod_a_a > $o] :
( ( ( ~ ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[689]) ).
thf(699,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[690]) ).
thf(700,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( ~ ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) ) )
= $false )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[690]) ).
thf(701,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[693]) ).
thf(702,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[693]) ).
thf(703,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[694]) ).
thf(704,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[694]) ).
thf(705,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ( SV23 = bot_bot_set_a )
| ( SV46 = bot_bot_set_a ) )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[696]) ).
thf(706,plain,
! [SV35: product_prod_a_a > $o,SV10: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $true )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[697]) ).
thf(707,plain,
! [SV10: product_prod_a_a > $o,SV35: product_prod_a_a > $o] :
( ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $true )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV10 ) )
= $false )
| ( ( finite179568208od_a_a @ ( collec645855634od_a_a @ SV35 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[698]) ).
thf(708,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[699]) ).
thf(709,plain,
! [SV41: pair_p125712459t_unit] :
( ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $true )
| ( ( finite_finite_a @ ( pair_p1047056820t_unit @ SV41 ) )
= $false )
| ( ( finite179568208od_a_a @ ( pair_p133601421t_unit @ SV41 ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[700]) ).
thf(710,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite_finite_a @ SV23 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[701]) ).
thf(711,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( finite_finite_a @ SV46 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[702]) ).
thf(712,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite_finite_a @ SV23 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[703]) ).
thf(713,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( finite_finite_a @ SV46 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[704]) ).
thf(714,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( ~ ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) ) )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[705]) ).
thf(715,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 )
| ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[714]) ).
thf(716,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( ~ ( finite_finite_a @ SV23 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[715]) ).
thf(717,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( ~ ( finite_finite_a @ SV46 ) )
= $false )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[715]) ).
thf(718,plain,
! [SV46: set_a,SV23: set_a] :
( ( ( finite_finite_a @ SV23 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[716]) ).
thf(719,plain,
! [SV23: set_a,SV46: set_a] :
( ( ( finite_finite_a @ SV46 )
= $true )
| ( ( SV46 = bot_bot_set_a )
= $true )
| ( ( SV23 = bot_bot_set_a )
= $true )
| ( ( finite_finite_a @ SV23 )
= $false )
| ( ( finite_finite_a @ SV46 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[717]) ).
thf(720,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[388,719,718,713,712,711,710,709,708,707,706,695,692,691,681,679,672,671,668,667,664,662,640,639,638,635,634,631,630,629,628,622,616,615,600,591,590,587,581,579,573,572,568,554,553,525,522,519,516,508,501,499,489,463,461,445,443,389]) ).
thf(721,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[720]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP093^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.18 % Computer : n009.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Oct 6 11:17:20 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.64/0.84 ..
% 3.64/0.84
% 3.64/0.84 No.of.Axioms: 29
% 3.64/0.84
% 3.64/0.84 Length.of.Defs: 0
% 3.64/0.84
% 3.64/0.84 Contains.Choice.Funs: false
% 3.64/0.84 ...........
% 3.64/0.84
% 3.64/0.84 ********************************
% 3.64/0.84 * All subproblems solved! *
% 3.64/0.84 ********************************
% 3.64/0.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:29,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:720,loop_count:0,foatp_calls:1,translation:fof_full)
% 3.64/0.84
% 3.64/0.84 %**** Beginning of derivation protocol ****
% 3.64/0.84 % SZS output start CNFRefutation
% See solution above
% 3.64/0.84
% 3.64/0.84 %**** End of derivation protocol ****
% 3.64/0.84 %**** no. of clauses in derivation: 396 ****
% 3.64/0.84 %**** clause counter: 720 ****
% 3.64/0.84
% 3.64/0.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:29,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:720,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------