Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP216_3 : TPTP v9.3.1. Bugfixed v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n004.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 : Sun Sep 27 07:36:49 AM UTC 2026

% Result   : Theorem 85.45s 23.13s
% Output   : Refutation 85.64s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   10
%            Number of leaves      :    3
% Syntax   : Number of formulae    :   19 (  11 unt;   0 typ;   0 def)
%            Number of atoms       :   34 (  17 equ;   0 cnn)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :  148 (  23   ~;   7   |;   3   &; 110   @)
%                                         (   1 <=>;   4  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   11 (   6 avg)
%            Number of types       : 1463 (1462 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   11 (   8 usr;   5 con; 0-2 aty)
%            Number of variables   :   26 (   0   ^;  26   !;   0   ?;  26   :)

% Comments : 
%------------------------------------------------------------------------------
thf(fun_Pr386875378712213506et_nat_type,type,
    fun_Pr386875378712213506et_nat: $tType ).

thf(set_Pr7057080801110549565et_nat_type,type,
    set_Pr7057080801110549565et_nat: $tType ).

thf(fun_se2331804103973993189et_nat_type,type,
    fun_se2331804103973993189et_nat: $tType ).

thf(fun_fu3515393148397969210et_nat_type,type,
    fun_fu3515393148397969210et_nat: $tType ).

thf(produc505541996239113949et_nat_type,type,
    produc505541996239113949et_nat: $tType ).

thf(fun_Pr3358449090565925198_nat_o_type,type,
    fun_Pr3358449090565925198_nat_o: $tType ).

thf(fun_se4713689491525875926_nat_o_type,type,
    fun_se4713689491525875926_nat_o: $tType ).

thf(fun_fu5983609555712719719_nat_o_type,type,
    fun_fu5983609555712719719_nat_o: $tType ).

thf(fun_fu4927615759029954091_nat_o_type,type,
    fun_fu4927615759029954091_nat_o: $tType ).

thf(fun_Pr6662792608368940153et_nat_type,type,
    fun_Pr6662792608368940153et_nat: $tType ).

thf(fun_Pr8630787502178681855et_nat_type,type,
    fun_Pr8630787502178681855et_nat: $tType ).

thf(fun_fu3932451362284101085et_nat_type,type,
    fun_fu3932451362284101085et_nat: $tType ).

thf(fun_Pr8737872353715570297et_nat_type,type,
    fun_Pr8737872353715570297et_nat: $tType ).

thf(fun_Pr471679772948460611nteger_type,type,
    fun_Pr471679772948460611nteger: $tType ).

thf(set_Pr6949033248718891245nteger_type,type,
    set_Pr6949033248718891245nteger: $tType ).

thf(fun_se2190013347424485781nteger_type,type,
    fun_se2190013347424485781nteger: $tType ).

thf(fun_fu5535353563232763194nteger_type,type,
    fun_fu5535353563232763194nteger: $tType ).

thf(fun_fu951349246861503509et_nat_type,type,
    fun_fu951349246861503509et_nat: $tType ).

thf(fun_Pr4147293223664569617et_nat_type,type,
    fun_Pr4147293223664569617et_nat: $tType ).

thf(produc7379341420752632205nteger_type,type,
    produc7379341420752632205nteger: $tType ).

thf(fun_se6163777255337707072eger_o_type,type,
    fun_se6163777255337707072eger_o: $tType ).

thf(fun_fu7060041198443644797eger_o_type,type,
    fun_fu7060041198443644797eger_o: $tType ).

thf(fun_fu4530937843762191077eger_o_type,type,
    fun_fu4530937843762191077eger_o: $tType ).

thf(fun_Pr2953255705995765467et_nat_type,type,
    fun_Pr2953255705995765467et_nat: $tType ).

thf(fun_Pr3978243888342905947et_nat_type,type,
    fun_Pr3978243888342905947et_nat: $tType ).

thf(fun_Pr4459677240377800360et_nat_type,type,
    fun_Pr4459677240377800360et_nat: $tType ).

thf(fun_Pr7963917038216275131nt_int_type,type,
    fun_Pr7963917038216275131nt_int: $tType ).

thf(fun_Pr3905736301278533417nteger_type,type,
    fun_Pr3905736301278533417nteger: $tType ).

thf(fun_Pr6966570558394395095nteger_type,type,
    fun_Pr6966570558394395095nteger: $tType ).

thf(fun_fu8946524575271555235nteger_type,type,
    fun_fu8946524575271555235nteger: $tType ).

thf(fun_Pr8371818785129130299nteger_type,type,
    fun_Pr8371818785129130299nteger: $tType ).

thf(set_Pr3767905878465553991nt_int_type,type,
    set_Pr3767905878465553991nt_int: $tType ).

thf(fun_se1594822257893229295nt_int_type,type,
    fun_se1594822257893229295nt_int: $tType ).

thf(fun_fu4502062894868904186nt_int_type,type,
    fun_fu4502062894868904186nt_int: $tType ).

thf(produc881187336974765031nt_int_type,type,
    produc881187336974765031nt_int: $tType ).

thf(fun_se5710315616867461632_int_o_type,type,
    fun_se5710315616867461632_int_o: $tType ).

thf(fun_fu2458202332514215229_int_o_type,type,
    fun_fu2458202332514215229_int_o: $tType ).

thf(fun_fu4695829907076200203_int_o_type,type,
    fun_fu4695829907076200203_int_o: $tType ).

thf(fun_op291006984297869545at_nat_type,type,
    fun_op291006984297869545at_nat: $tType ).

thf(fun_Pr5846521507401124227nt_int_type,type,
    fun_Pr5846521507401124227nt_int: $tType ).

thf(fun_Pr5010838083610845651nt_int_type,type,
    fun_Pr5010838083610845651nt_int: $tType ).

thf(fun_fu4173945377279696323nteger_type,type,
    fun_fu4173945377279696323nteger: $tType ).

thf(fun_fu9160953773549289085nt_int_type,type,
    fun_fu9160953773549289085nt_int: $tType ).

thf(fun_Pr8826142978676617911nt_int_type,type,
    fun_Pr8826142978676617911nt_int: $tType ).

thf(fun_fu8902681562042749453nteger_type,type,
    fun_fu8902681562042749453nteger: $tType ).

thf(fun_Pr4557384415951816845e_term_type,type,
    fun_Pr4557384415951816845e_term: $tType ).

thf(set_Pr9066344408807579265et_nat_type,type,
    set_Pr9066344408807579265et_nat: $tType ).

thf(fun_se9157011578508667433et_nat_type,type,
    fun_se9157011578508667433et_nat: $tType ).

thf(fun_fu2239858650119588794et_nat_type,type,
    fun_fu2239858650119588794et_nat: $tType ).

thf(fun_fu5650763273978745334et_nat_type,type,
    fun_fu5650763273978745334et_nat: $tType ).

thf(produc8893060842726229537et_nat_type,type,
    produc8893060842726229537et_nat: $tType ).

thf(fun_fu6196531292930346304et_nat_type,type,
    fun_fu6196531292930346304et_nat: $tType ).

thf(fun_Pr7618159474455865098_nat_o_type,type,
    fun_Pr7618159474455865098_nat_o: $tType ).

thf(fun_se7509835969743050710_nat_o_type,type,
    fun_se7509835969743050710_nat_o: $tType ).

thf(fun_fu3464598166661278695_nat_o_type,type,
    fun_fu3464598166661278695_nat_o: $tType ).

thf(fun_fu7582738562687708775_nat_o_type,type,
    fun_fu7582738562687708775_nat_o: $tType ).

thf(fun_Pr836988951548913597et_nat_type,type,
    fun_Pr836988951548913597et_nat: $tType ).

thf(fun_Pr5416369060549219583et_nat_type,type,
    fun_Pr5416369060549219583et_nat: $tType ).

thf(fun_fu60724386564609697nt_int_type,type,
    fun_fu60724386564609697nt_int: $tType ).

thf(fun_se1700271160720914596_nat_o_type,type,
    fun_se1700271160720914596_nat_o: $tType ).

thf(fun_fu2265384587115734689et_nat_type,type,
    fun_fu2265384587115734689et_nat: $tType ).

thf(fun_Pr5259258551928531321et_nat_type,type,
    fun_Pr5259258551928531321et_nat: $tType ).

thf(fun_fu7234567020521114219nteger_type,type,
    fun_fu7234567020521114219nteger: $tType ).

thf(fun_fu5813366174458671467nt_int_type,type,
    fun_fu5813366174458671467nt_int: $tType ).

thf(fun_Pr5872836680101629291e_term_type,type,
    fun_Pr5872836680101629291e_term: $tType ).

thf(fun_se6980948925662697216_nat_o_type,type,
    fun_se6980948925662697216_nat_o: $tType ).

thf(fun_op4112804339236761266it_nat_type,type,
    fun_op4112804339236761266it_nat: $tType ).

thf(fun_Pr5088371826558493971nt_int_type,type,
    fun_Pr5088371826558493971nt_int: $tType ).

thf(set_Pr2514328457256655413e_term_type,type,
    set_Pr2514328457256655413e_term: $tType ).

thf(fun_Pr3631287881653221602it_nat_type,type,
    fun_Pr3631287881653221602it_nat: $tType ).

thf(produc8529534078076073941e_term_type,type,
    produc8529534078076073941e_term: $tType ).

thf(fun_Pr1003294667014919570it_nat_type,type,
    fun_Pr1003294667014919570it_nat: $tType ).

thf(set_Pr257197284073945367e_term_type,type,
    set_Pr257197284073945367e_term: $tType ).

thf(fun_Pr6442729728054246170it_nat_type,type,
    fun_Pr6442729728054246170it_nat: $tType ).

thf(fun_fu2505754153367914865e_term_type,type,
    fun_fu2505754153367914865e_term: $tType ).

thf(fun_fu2492676192234506515it_nat_type,type,
    fun_fu2492676192234506515it_nat: $tType ).

thf(fun_fu4233702620870981175it_nat_type,type,
    fun_fu4233702620870981175it_nat: $tType ).

thf(produc9065761207657906103e_term_type,type,
    produc9065761207657906103e_term: $tType ).

thf(fun_se636550882185307767at_nat_type,type,
    fun_se636550882185307767at_nat: $tType ).

thf(set_se6059149423757001258et_nat_type,type,
    set_se6059149423757001258et_nat: $tType ).

thf(fun_fu8543582513329703974nteger_type,type,
    fun_fu8543582513329703974nteger: $tType ).

thf(fun_Pr894914116851403386nteger_type,type,
    fun_Pr894914116851403386nteger: $tType ).

thf(set_fu4385504767878589843_nat_o_type,type,
    set_fu4385504767878589843_nat_o: $tType ).

thf(set_Pr3703873761940759199nt_int_type,type,
    set_Pr3703873761940759199nt_int: $tType ).

thf(fun_Pr6341106346053136302_nat_o_type,type,
    fun_Pr6341106346053136302_nat_o: $tType ).

thf(fun_se2900878183379320647nt_int_type,type,
    fun_se2900878183379320647nt_int: $tType ).

thf(fun_fu9132409297049680378nt_int_type,type,
    fun_fu9132409297049680378nt_int: $tType ).

thf(fun_Pr5911813565203289452_nat_o_type,type,
    fun_Pr5911813565203289452_nat_o: $tType ).

thf(option5899113203645146382et_nat_type,type,
    option5899113203645146382et_nat: $tType ).

thf(fun_fu836511555612062035e_term_type,type,
    fun_fu836511555612062035e_term: $tType ).

thf(set_Pr4040394263813967220et_nat_type,type,
    set_Pr4040394263813967220et_nat: $tType ).

thf(set_Pr7905283282039288826_nat_o_type,type,
    set_Pr7905283282039288826_nat_o: $tType ).

thf(fun_Pr1227177680593602867_nat_o_type,type,
    fun_Pr1227177680593602867_nat_o: $tType ).

thf(fun_Pr6160931176198666718nteger_type,type,
    fun_Pr6160931176198666718nteger: $tType ).

thf(fun_Pr2985126522952997572nteger_type,type,
    fun_Pr2985126522952997572nteger: $tType ).

thf(produc3192696172498486335nt_int_type,type,
    produc3192696172498486335nt_int: $tType ).

thf(set_fu5576194784986904859_nat_o_type,type,
    set_fu5576194784986904859_nat_o: $tType ).

thf(fun_Pr886604116968709228_int_o_type,type,
    fun_Pr886604116968709228_int_o: $tType ).

thf(fun_fu7865199641817216212eger_o_type,type,
    fun_fu7865199641817216212eger_o: $tType ).

thf(fun_fu8324349134136105556eger_o_type,type,
    fun_fu8324349134136105556eger_o: $tType ).

thf(produc4193628355235574503at_nat_type,type,
    produc4193628355235574503at_nat: $tType ).

thf(fun_se5644990602862975744_int_o_type,type,
    fun_se5644990602862975744_int_o: $tType ).

thf(fun_fu5894409982295737917_int_o_type,type,
    fun_fu5894409982295737917_int_o: $tType ).

thf(fun_fu6286765928754279603_int_o_type,type,
    fun_fu6286765928754279603_int_o: $tType ).

thf(fun_fu1905361174868762994et_nat_type,type,
    fun_fu1905361174868762994et_nat: $tType ).

thf(produc3112576180687729086et_nat_type,type,
    produc3112576180687729086et_nat: $tType ).

thf(produc6858501863712832324_nat_o_type,type,
    produc6858501863712832324_nat_o: $tType ).

thf(fun_fu8357309440898100312et_nat_type,type,
    fun_fu8357309440898100312et_nat: $tType ).

thf(fun_se3629081808164793780_nat_o_type,type,
    fun_se3629081808164793780_nat_o: $tType ).

thf(fun_Pr7968690803259750408_nat_o_type,type,
    fun_Pr7968690803259750408_nat_o: $tType ).

thf(fun_fu2611741329380808165_nat_o_type,type,
    fun_fu2611741329380808165_nat_o: $tType ).

thf(fun_Pr2647030239595059785at_o_o_type,type,
    fun_Pr2647030239595059785at_o_o: $tType ).

thf(fun_Pr5152393401594413531nt_int_type,type,
    fun_Pr5152393401594413531nt_int: $tType ).

thf(fun_Pr3284083897292419283nt_int_type,type,
    fun_Pr3284083897292419283nt_int: $tType ).

thf(set_Pr7459493094073627847at_nat_type,type,
    set_Pr7459493094073627847at_nat: $tType ).

thf(fun_fu5004560472337415769et_nat_type,type,
    fun_fu5004560472337415769et_nat: $tType ).

thf(fun_Pr3017356861961520469et_nat_type,type,
    fun_Pr3017356861961520469et_nat: $tType ).

thf(fun_fu8710561278413400866et_nat_type,type,
    fun_fu8710561278413400866et_nat: $tType ).

thf(fun_Pr3233114924583728296_nat_o_type,type,
    fun_Pr3233114924583728296_nat_o: $tType ).

thf(fun_se991814106188233920_nat_o_type,type,
    fun_se991814106188233920_nat_o: $tType ).

thf(fun_fu6437682067762269056_num_o_type,type,
    fun_fu6437682067762269056_num_o: $tType ).

thf(fun_fu465145433024125141nt_int_type,type,
    fun_fu465145433024125141nt_int: $tType ).

thf(fun_Pr4353654455642104759nt_int_type,type,
    fun_Pr4353654455642104759nt_int: $tType ).

thf(fun_se7901873761543946185at_nat_type,type,
    fun_se7901873761543946185at_nat: $tType ).

thf(produc1319942482725812455at_nat_type,type,
    produc1319942482725812455at_nat: $tType ).

thf(fun_Pr2813956079162534559et_nat_type,type,
    fun_Pr2813956079162534559et_nat: $tType ).

thf(fun_Pr4885567672785483807et_nat_type,type,
    fun_Pr4885567672785483807et_nat: $tType ).

thf(fun_Pr8463018485500633518_nat_o_type,type,
    fun_Pr8463018485500633518_nat_o: $tType ).

thf(set_Pr5564308138774400199at_nat_type,type,
    set_Pr5564308138774400199at_nat: $tType ).

thf(fun_Pr5502292500389099060_nat_o_type,type,
    fun_Pr5502292500389099060_nat_o: $tType ).

thf(fun_fu4812223801888690549nt_int_type,type,
    fun_fu4812223801888690549nt_int: $tType ).

thf(fun_Pr1547027809659849477nt_int_type,type,
    fun_Pr1547027809659849477nt_int: $tType ).

thf(fun_se6846035212209387651at_nat_type,type,
    fun_se6846035212209387651at_nat: $tType ).

thf(fun_fu5127092707984472044at_nat_type,type,
    fun_fu5127092707984472044at_nat: $tType ).

thf(set_se7873143835621700354nteger_type,type,
    set_se7873143835621700354nteger: $tType ).

thf(set_fu6463009222652410043eger_o_type,type,
    set_fu6463009222652410043eger_o: $tType ).

thf(fun_fu4688806437979560835nteger_type,type,
    fun_fu4688806437979560835nteger: $tType ).

thf(fun_op1633239139951409690_nat_o_type,type,
    fun_op1633239139951409690_nat_o: $tType ).

thf(fun_op8703326495438967718_nat_o_type,type,
    fun_op8703326495438967718_nat_o: $tType ).

thf(fun_op101698441058542546_nat_o_type,type,
    fun_op101698441058542546_nat_o: $tType ).

thf(fun_op2352717853092002798_nat_o_type,type,
    fun_op2352717853092002798_nat_o: $tType ).

thf(option983905398058327270nteger_type,type,
    option983905398058327270nteger: $tType ).

thf(fun_fu2531416508075921811et_nat_type,type,
    fun_fu2531416508075921811et_nat: $tType ).

thf(fun_fu6941240126142778863et_int_type,type,
    fun_fu6941240126142778863et_int: $tType ).

thf(produc1906917888121415911at_nat_type,type,
    produc1906917888121415911at_nat: $tType ).

thf(fun_Pr1987159835869338959nt_int_type,type,
    fun_Pr1987159835869338959nt_int: $tType ).

thf(fun_Pr4781553364444837327nt_int_type,type,
    fun_Pr4781553364444837327nt_int: $tType ).

thf(fun_Pr5947183769845927726_nat_o_type,type,
    fun_Pr5947183769845927726_nat_o: $tType ).

thf(set_Pr3486312109254157132nteger_type,type,
    set_Pr3486312109254157132nteger: $tType ).

thf(set_Pr3944325338781952762e_term_type,type,
    set_Pr3944325338781952762e_term: $tType ).

thf(fun_fu2716251949043459987at_nat_type,type,
    fun_fu2716251949043459987at_nat: $tType ).

thf(fun_Pr7015759342434529115eger_o_type,type,
    fun_Pr7015759342434529115eger_o: $tType ).

thf(fun_se8406536441587994090_nat_o_type,type,
    fun_se8406536441587994090_nat_o: $tType ).

thf(fun_fu3198693465525813493_nat_o_type,type,
    fun_fu3198693465525813493_nat_o: $tType ).

thf(fun_fu6788480576040630871_set_o_type,type,
    fun_fu6788480576040630871_set_o: $tType ).

thf(set_fu7224585531122448557eger_o_type,type,
    set_fu7224585531122448557eger_o: $tType ).

thf(fun_fu560856344546067396_int_o_type,type,
    fun_fu560856344546067396_int_o: $tType ).

thf(fun_fu6029888860018473377nt_int_type,type,
    fun_fu6029888860018473377nt_int: $tType ).

thf(fun_Pr6865292569827446866it_nat_type,type,
    fun_Pr6865292569827446866it_nat: $tType ).

thf(fun_Pr8741579136290173250atural_type,type,
    fun_Pr8741579136290173250atural: $tType ).

thf(fun_fu4835546211937200935e_term_type,type,
    fun_fu4835546211937200935e_term: $tType ).

thf(fun_fu1176768540439120679e_term_type,type,
    fun_fu1176768540439120679e_term: $tType ).

thf(fun_fu4810197545401214784nteger_type,type,
    fun_fu4810197545401214784nteger: $tType ).

thf(fun_fu2217603491152269828it_nat_type,type,
    fun_fu2217603491152269828it_nat: $tType ).

thf(produc9140211490168418807atural_type,type,
    produc9140211490168418807atural: $tType ).

thf(produc2453742332425399446nteger_type,type,
    produc2453742332425399446nteger: $tType ).

thf(produc592931078481472324e_term_type,type,
    produc592931078481472324e_term: $tType ).

thf(fun_fu5808343195260015654it_nat_type,type,
    fun_fu5808343195260015654it_nat: $tType ).

thf(fun_fu1080234963260751190it_nat_type,type,
    fun_fu1080234963260751190it_nat: $tType ).

thf(fun_se5316394792625908170_nat_o_type,type,
    fun_se5316394792625908170_nat_o: $tType ).

thf(fun_fu5971215405379524186nteger_type,type,
    fun_fu5971215405379524186nteger: $tType ).

thf(fun_fu7484024174323986552it_nat_type,type,
    fun_fu7484024174323986552it_nat: $tType ).

thf(fun_Pr5305228341155023582e_term_type,type,
    fun_Pr5305228341155023582e_term: $tType ).

thf(fun_fu7445151911848907075at_nat_type,type,
    fun_fu7445151911848907075at_nat: $tType ).

thf(fun_fu7695273699059480439eger_o_type,type,
    fun_fu7695273699059480439eger_o: $tType ).

thf(fun_Pr4680327687137491167term_o_type,type,
    fun_Pr4680327687137491167term_o: $tType ).

thf(fun_fu4545303443005895275nt_int_type,type,
    fun_fu4545303443005895275nt_int: $tType ).

thf(fun_Pr7653582204007996523e_term_type,type,
    fun_Pr7653582204007996523e_term: $tType ).

thf(fun_Pr7644814098969791837it_nat_type,type,
    fun_Pr7644814098969791837it_nat: $tType ).

thf(fun_op7765417307512062173it_nat_type,type,
    fun_op7765417307512062173it_nat: $tType ).

thf(fun_Pr7518090501403545819it_nat_type,type,
    fun_Pr7518090501403545819it_nat: $tType ).

thf(fun_Pr245379829043246639it_nat_type,type,
    fun_Pr245379829043246639it_nat: $tType ).

thf(fun_Pr8118912048244921225it_nat_type,type,
    fun_Pr8118912048244921225it_nat: $tType ).

thf(fun_op8917697677373047293it_nat_type,type,
    fun_op8917697677373047293it_nat: $tType ).

thf(set_se2743246391971219311nt_int_type,type,
    set_se2743246391971219311nt_int: $tType ).

thf(fun_fu695563712076452518at_nat_type,type,
    fun_fu695563712076452518at_nat: $tType ).

thf(set_fu5926610517471843470_int_o_type,type,
    set_fu5926610517471843470_int_o: $tType ).

thf(fun_se8716479205685501124_nat_o_type,type,
    fun_se8716479205685501124_nat_o: $tType ).

thf(option1544258867535432659nt_int_type,type,
    option1544258867535432659nt_int: $tType ).

thf(fun_Pr925140355916870337it_nat_type,type,
    fun_Pr925140355916870337it_nat: $tType ).

thf(fun_Pr2979129825601314957it_nat_type,type,
    fun_Pr2979129825601314957it_nat: $tType ).

thf(fun_ar4934926718671674165it_nat_type,type,
    fun_ar4934926718671674165it_nat: $tType ).

thf(fun_ar7427004957847640857it_nat_type,type,
    fun_ar7427004957847640857it_nat: $tType ).

thf(fun_Co9168753396221475450atural_type,type,
    fun_Co9168753396221475450atural: $tType ).

thf(fun_fu61188948249169719_int_o_type,type,
    fun_fu61188948249169719_int_o: $tType ).

thf(fun_fu3447610970239163469_rat_o_type,type,
    fun_fu3447610970239163469_rat_o: $tType ).

thf(fun_Pr1033138224055104269it_nat_type,type,
    fun_Pr1033138224055104269it_nat: $tType ).

thf(set_Pr6700895561065273913nt_int_type,type,
    set_Pr6700895561065273913nt_int: $tType ).

thf(set_Pr3640028372902554249e_term_type,type,
    set_Pr3640028372902554249e_term: $tType ).

thf(fun_Pr3540825087398332590_int_o_type,type,
    fun_Pr3540825087398332590_int_o: $tType ).

thf(fun_Pr3908927074708932117it_nat_type,type,
    fun_Pr3908927074708932117it_nat: $tType ).

thf(fun_Pr2014882013869309663it_nat_type,type,
    fun_Pr2014882013869309663it_nat: $tType ).

thf(fun_Pr3819237756034508227it_nat_type,type,
    fun_Pr3819237756034508227it_nat: $tType ).

thf(fun_fu865538946246809014eger_o_type,type,
    fun_fu865538946246809014eger_o: $tType ).

thf(fun_fu1909630106382427190eger_o_type,type,
    fun_fu1909630106382427190eger_o: $tType ).

thf(set_fu1179388718870097536_int_o_type,type,
    set_fu1179388718870097536_int_o: $tType ).

thf(fun_se9209729713313069232_nat_o_type,type,
    fun_se9209729713313069232_nat_o: $tType ).

thf(fun_fu4253467608928286509nt_int_type,type,
    fun_fu4253467608928286509nt_int: $tType ).

thf(fun_op7507520395135695063nteger_type,type,
    fun_op7507520395135695063nteger: $tType ).

thf(set_se3290278062343509644et_nat_type,type,
    set_se3290278062343509644et_nat: $tType ).

thf(set_fu6830718107662835377_nat_o_type,type,
    set_fu6830718107662835377_nat_o: $tType ).

thf(set_Pr2890355626087285447_nat_o_type,type,
    set_Pr2890355626087285447_nat_o: $tType ).

thf(fun_Pr5739084258597601403it_nat_type,type,
    fun_Pr5739084258597601403it_nat: $tType ).

thf(produc3043004577601930755nt_int_type,type,
    produc3043004577601930755nt_int: $tType ).

thf(produc4155239895104388691e_term_type,type,
    produc4155239895104388691e_term: $tType ).

thf(fun_Pr2439654876356241257it_nat_type,type,
    fun_Pr2439654876356241257it_nat: $tType ).

thf(fun_ar5851962999413977351it_nat_type,type,
    fun_ar5851962999413977351it_nat: $tType ).

thf(fun_fu2039158179202302481nteger_type,type,
    fun_fu2039158179202302481nteger: $tType ).

thf(fun_ar4667500465507062749it_nat_type,type,
    fun_ar4667500465507062749it_nat: $tType ).

thf(fun_fu4219362280553733319nt_int_type,type,
    fun_fu4219362280553733319nt_int: $tType ).

thf(fun_fu7605985262670345913eger_o_type,type,
    fun_fu7605985262670345913eger_o: $tType ).

thf(fun_fu5480185501004512569eger_o_type,type,
    fun_fu5480185501004512569eger_o: $tType ).

thf(fun_Pr4426623609552329069e_term_type,type,
    fun_Pr4426623609552329069e_term: $tType ).

thf(fun_fu6865642474282033866_int_o_type,type,
    fun_fu6865642474282033866_int_o: $tType ).

thf(fun_Pr6967485491430695501atural_type,type,
    fun_Pr6967485491430695501atural: $tType ).

thf(fun_Pr3377396784085331203atural_type,type,
    fun_Pr3377396784085331203atural: $tType ).

thf(fun_Pr5526332658708858896term_o_type,type,
    fun_Pr5526332658708858896term_o: $tType ).

thf(fun_Pr4028877673837371139atural_type,type,
    fun_Pr4028877673837371139atural: $tType ).

thf(fun_Pr6891710885006071673atural_type,type,
    fun_Pr6891710885006071673atural: $tType ).

thf(fun_Pr3133360822718887225atural_type,type,
    fun_Pr3133360822718887225atural: $tType ).

thf(fun_se7382040709525900966_nat_o_type,type,
    fun_se7382040709525900966_nat_o: $tType ).

thf(option4955102875562834416et_nat_type,type,
    option4955102875562834416et_nat: $tType ).

thf(fun_fu86038545275896455et_nat_type,type,
    fun_fu86038545275896455et_nat: $tType ).

thf(fun_fu4495862163342753507et_int_type,type,
    fun_fu4495862163342753507et_int: $tType ).

thf(set_Pr7847555563209246911e_term_type,type,
    set_Pr7847555563209246911e_term: $tType ).

thf(produc2402493665305094840nteger_type,type,
    produc2402493665305094840nteger: $tType ).

thf(fun_fu786557078278636193nt_int_type,type,
    fun_fu786557078278636193nt_int: $tType ).

thf(fun_Pr1951044811698827825nt_int_type,type,
    fun_Pr1951044811698827825nt_int: $tType ).

thf(set_Pr1312406793078187350et_nat_type,type,
    set_Pr1312406793078187350et_nat: $tType ).

thf(set_Pr3013394129895136920_nat_o_type,type,
    set_Pr3013394129895136920_nat_o: $tType ).

thf(fun_Pr2620521676128474833_nat_o_type,type,
    fun_Pr2620521676128474833_nat_o: $tType ).

thf(produc6671579610312156647_nat_o_type,type,
    produc6671579610312156647_nat_o: $tType ).

thf(fun_fu9089537617116752462nteger_type,type,
    fun_fu9089537617116752462nteger: $tType ).

thf(fun_fu4934440599869564003_set_o_type,type,
    fun_fu4934440599869564003_set_o: $tType ).

thf(fun_fu5629128276443140046nteger_type,type,
    fun_fu5629128276443140046nteger: $tType ).

thf(fun_Pr5651933991979716257it_nat_type,type,
    fun_Pr5651933991979716257it_nat: $tType ).

thf(set_fu3659417381080568633_nat_o_type,type,
    set_fu3659417381080568633_nat_o: $tType ).

thf(fun_fu5513256665162130182_num_o_type,type,
    fun_fu5513256665162130182_num_o: $tType ).

thf(fun_fu7909047026757000106_num_o_type,type,
    fun_fu7909047026757000106_num_o: $tType ).

thf(fun_Pr192538292188806807it_nat_type,type,
    fun_Pr192538292188806807it_nat: $tType ).

thf(fun_fu2931456868620722337_rat_o_type,type,
    fun_fu2931456868620722337_rat_o: $tType ).

thf(fun_Pr3688637647703109351atural_type,type,
    fun_Pr3688637647703109351atural: $tType ).

thf(fun_Co3643010573817537149atural_type,type,
    fun_Co3643010573817537149atural: $tType ).

thf(fun_Co1105491363547889651atural_type,type,
    fun_Co1105491363547889651atural: $tType ).

thf(fun_Co1890133979025130057atural_type,type,
    fun_Co1890133979025130057atural: $tType ).

thf(produc7249898413471085407e_term_type,type,
    produc7249898413471085407e_term: $tType ).

thf(fun_fu8216932157852985630_rat_o_type,type,
    fun_fu8216932157852985630_rat_o: $tType ).

thf(fun_fu2352890940381120596et_nat_type,type,
    fun_fu2352890940381120596et_nat: $tType ).

thf(produc1284174907132067113nteger_type,type,
    produc1284174907132067113nteger: $tType ).

thf(produc8574895079301897479rm_int_type,type,
    produc8574895079301897479rm_int: $tType ).

thf(fun_Pr1552678306225191715nt_int_type,type,
    fun_Pr1552678306225191715nt_int: $tType ).

thf(fun_Pr8696298990344678139nt_int_type,type,
    fun_Pr8696298990344678139nt_int: $tType ).

thf(set_Pr719794911490849221et_nat_type,type,
    set_Pr719794911490849221et_nat: $tType ).

thf(fun_Co3668495603736800980e_term_type,type,
    fun_Co3668495603736800980e_term: $tType ).

thf(produc8799533983703829792et_nat_type,type,
    produc8799533983703829792et_nat: $tType ).

thf(produc2739566037923759970_nat_o_type,type,
    produc2739566037923759970_nat_o: $tType ).

thf(fun_fu6029601804184707687at_nat_type,type,
    fun_fu6029601804184707687at_nat: $tType ).

thf(fun_fu2890809920214373946et_nat_type,type,
    fun_fu2890809920214373946et_nat: $tType ).

thf(fun_Pr8383423175210966566_nat_o_type,type,
    fun_Pr8383423175210966566_nat_o: $tType ).

thf(set_Pr5070339090747523585at_nat_type,type,
    set_Pr5070339090747523585at_nat: $tType ).

thf(set_Pr2072254264782222413at_nat_type,type,
    set_Pr2072254264782222413at_nat: $tType ).

thf(fun_fu8419763957888848259_nat_o_type,type,
    fun_fu8419763957888848259_nat_o: $tType ).

thf(fun_Pr2493370495569891450_nat_o_type,type,
    fun_Pr2493370495569891450_nat_o: $tType ).

thf(fun_Pr6861956506527726894_nat_o_type,type,
    fun_Pr6861956506527726894_nat_o: $tType ).

thf(fun_Pr5843349257357397163at_o_o_type,type,
    fun_Pr5843349257357397163at_o_o: $tType ).

thf(fun_fu6544435175084778670_int_o_type,type,
    fun_fu6544435175084778670_int_o: $tType ).

thf(fun_fu6282320651122755630at_o_o_type,type,
    fun_fu6282320651122755630at_o_o: $tType ).

thf(fun_fu783388071822146350nt_o_o_type,type,
    fun_fu783388071822146350nt_o_o: $tType ).

thf(fun_fu4429252470074529710_int_o_type,type,
    fun_fu4429252470074529710_int_o: $tType ).

thf(fun_se1551789852802198377at_nat_type,type,
    fun_se1551789852802198377at_nat: $tType ).

thf(fun_fu3373238862511017284_nat_o_type,type,
    fun_fu3373238862511017284_nat_o: $tType ).

thf(fun_fu5323616038969315652_int_o_type,type,
    fun_fu5323616038969315652_int_o: $tType ).

thf(fun_se1934056669979388328_nat_o_type,type,
    fun_se1934056669979388328_nat_o: $tType ).

thf(fun_he8369595706569872389it_nat_type,type,
    fun_he8369595706569872389it_nat: $tType ).

thf(fun_op3037383146056310525nteger_type,type,
    fun_op3037383146056310525nteger: $tType ).

thf(fun_he2390400765173608009it_nat_type,type,
    fun_he2390400765173608009it_nat: $tType ).

thf(fun_fu2847332191311216467_nat_o_type,type,
    fun_fu2847332191311216467_nat_o: $tType ).

thf(fun_fu3528811849556752711nt_int_type,type,
    fun_fu3528811849556752711nt_int: $tType ).

thf(fun_fu4800041728187187127nteger_type,type,
    fun_fu4800041728187187127nteger: $tType ).

thf(produc6693577919049233272rm_int_type,type,
    produc6693577919049233272rm_int: $tType ).

thf(fun_fu4810317505167811835e_term_type,type,
    fun_fu4810317505167811835e_term: $tType ).

thf(produc8111630337999740517et_nat_type,type,
    produc8111630337999740517et_nat: $tType ).

thf(fun_in7158797356850311459e_term_type,type,
    fun_in7158797356850311459e_term: $tType ).

thf(fun_Co4988957157240174789e_term_type,type,
    fun_Co4988957157240174789e_term: $tType ).

thf(produc7476732711998919211atural_type,type,
    produc7476732711998919211atural: $tType ).

thf(produc7509114972854644512nteger_type,type,
    produc7509114972854644512nteger: $tType ).

thf(fun_fu9208662316977796352eger_o_type,type,
    fun_fu9208662316977796352eger_o: $tType ).

thf(fun_Pr7920380315054183110_nat_o_type,type,
    fun_Pr7920380315054183110_nat_o: $tType ).

thf(produc2087150632810049441at_nat_type,type,
    produc2087150632810049441at_nat: $tType ).

thf(produc2714363965264676845at_nat_type,type,
    produc2714363965264676845at_nat: $tType ).

thf(fun_Pr6212429452034653949at_nat_type,type,
    fun_Pr6212429452034653949at_nat: $tType ).

thf(fun_fu7998330801112555204at_o_o_type,type,
    fun_fu7998330801112555204at_o_o: $tType ).

thf(fun_fu2720337172504440700nt_o_o_type,type,
    fun_fu2720337172504440700nt_o_o: $tType ).

thf(fun_fu3364590669033493516at_o_o_type,type,
    fun_fu3364590669033493516at_o_o: $tType ).

thf(fun_fu7309969077280154820nt_o_o_type,type,
    fun_fu7309969077280154820nt_o_o: $tType ).

thf(fun_Pr5440946310329839626_nat_o_type,type,
    fun_Pr5440946310329839626_nat_o: $tType ).

thf(fun_Pr4146420783962613950_nat_o_type,type,
    fun_Pr4146420783962613950_nat_o: $tType ).

thf(set_fu8280898353253485872e_term_type,type,
    set_fu8280898353253485872e_term: $tType ).

thf(fun_fu4736795817735658359term_o_type,type,
    fun_fu4736795817735658359term_o: $tType ).

thf(fun_se6502775985981750992_nat_o_type,type,
    fun_se6502775985981750992_nat_o: $tType ).

thf(fun_fu6384561554008368101_nat_o_type,type,
    fun_fu6384561554008368101_nat_o: $tType ).

thf(fun_he5234484606919320760it_nat_type,type,
    fun_he5234484606919320760it_nat: $tType ).

thf(fun_in237891044757944084e_term_type,type,
    fun_in237891044757944084e_term: $tType ).

thf(fun_he1504492240061592256it_nat_type,type,
    fun_he1504492240061592256it_nat: $tType ).

thf(fun_Pr7406272072912987266atural_type,type,
    fun_Pr7406272072912987266atural: $tType ).

thf(fun_Pr6624299372562097772it_nat_type,type,
    fun_Pr6624299372562097772it_nat: $tType ).

thf(fun_Pr2136124334875798924atural_type,type,
    fun_Pr2136124334875798924atural: $tType ).

thf(fun_Pr4906574453216509900atural_type,type,
    fun_Pr4906574453216509900atural: $tType ).

thf(fun_Pr7769407664385210434atural_type,type,
    fun_Pr7769407664385210434atural: $tType ).

thf(fun_Co5709460363461100952atural_type,type,
    fun_Co5709460363461100952atural: $tType ).

thf(produc8903623710181579841nteger_type,type,
    produc8903623710181579841nteger: $tType ).

thf(fun_Pr7091840695141096449et_nat_type,type,
    fun_Pr7091840695141096449et_nat: $tType ).

thf(set_se4391686895574802075nt_int_type,type,
    set_se4391686895574802075nt_int: $tType ).

thf(produc714035400761762599atural_type,type,
    produc714035400761762599atural: $tType ).

thf(fun_fu2657526370245387306_int_o_type,type,
    fun_fu2657526370245387306_int_o: $tType ).

thf(set_fu5828550712561173602_int_o_type,type,
    set_fu5828550712561173602_int_o: $tType ).

thf(fun_fu7448223259553364356at_nat_type,type,
    fun_fu7448223259553364356at_nat: $tType ).

thf(fun_fu1039311746440044420at_nat_type,type,
    fun_fu1039311746440044420at_nat: $tType ).

thf(fun_fu8559083954280392170eger_o_type,type,
    fun_fu8559083954280392170eger_o: $tType ).

thf(fun_Co2466309612238040426eger_o_type,type,
    fun_Co2466309612238040426eger_o: $tType ).

thf(fun_op6018817604785332104_num_o_type,type,
    fun_op6018817604785332104_num_o: $tType ).

thf(fun_op298641349230941576_nat_o_type,type,
    fun_op298641349230941576_nat_o: $tType ).

thf(fun_fu2427765959047162121_rat_o_type,type,
    fun_fu2427765959047162121_rat_o: $tType ).

thf(fun_Pr285225112257423215e_term_type,type,
    fun_Pr285225112257423215e_term: $tType ).

thf(fun_Pr5098669352780829690e_term_type,type,
    fun_Pr5098669352780829690e_term: $tType ).

thf(fun_op3129816456743790912_num_o_type,type,
    fun_op3129816456743790912_num_o: $tType ).

thf(fun_op261120641589640376_nat_o_type,type,
    fun_op261120641589640376_nat_o: $tType ).

thf(set_fu5653557704672872225e_term_type,type,
    set_fu5653557704672872225e_term: $tType ).

thf(fun_fu6378075912484669126term_o_type,type,
    fun_fu6378075912484669126term_o: $tType ).

thf(fun_fu6741006549690681129nt_int_type,type,
    fun_fu6741006549690681129nt_int: $tType ).

thf(fun_se7979130632333208764_nat_o_type,type,
    fun_se7979130632333208764_nat_o: $tType ).

thf(fun_na7109657165716327514_nat_o_type,type,
    fun_na7109657165716327514_nat_o: $tType ).

thf(fun_Pr6721000092112975824et_nat_type,type,
    fun_Pr6721000092112975824et_nat: $tType ).

thf(produc6576344331059438605e_term_type,type,
    produc6576344331059438605e_term: $tType ).

thf(option6186025235080601855nt_int_type,type,
    option6186025235080601855nt_int: $tType ).

thf(fun_fu9079770784915425324et_nat_type,type,
    fun_fu9079770784915425324et_nat: $tType ).

thf(fun_fu4266222366127506568et_int_type,type,
    fun_fu4266222366127506568et_int: $tType ).

thf(fun_Pr5508761798988831599t_unit_type,type,
    fun_Pr5508761798988831599t_unit: $tType ).

thf(set_Pr552903133987017116at_nat_type,type,
    set_Pr552903133987017116at_nat: $tType ).

thf(set_Pr1625285437083415874at_nat_type,type,
    set_Pr1625285437083415874at_nat: $tType ).

thf(set_Pr4166680992137330533nt_int_type,type,
    set_Pr4166680992137330533nt_int: $tType ).

thf(set_Pr4417106977106297437e_term_type,type,
    set_Pr4417106977106297437e_term: $tType ).

thf(fun_fu7828939442023433772_num_o_type,type,
    fun_fu7828939442023433772_num_o: $tType ).

thf(fun_fu867726335913497644eger_o_type,type,
    fun_fu867726335913497644eger_o: $tType ).

thf(fun_Pr1196100989263358594_int_o_type,type,
    fun_Pr1196100989263358594_int_o: $tType ).

thf(fun_Co1851440197950133416atural_type,type,
    fun_Co1851440197950133416atural: $tType ).

thf(fun_Co1561183069634336733nteger_type,type,
    fun_Co1561183069634336733nteger: $tType ).

thf(fun_fu3188400912490975470at_o_o_type,type,
    fun_fu3188400912490975470at_o_o: $tType ).

thf(fun_fu6738731901453605870nt_o_o_type,type,
    fun_fu6738731901453605870nt_o_o: $tType ).

thf(fun_fu7485687605903516013_num_o_type,type,
    fun_fu7485687605903516013_num_o: $tType ).

thf(fun_fu1617828088232643505_nat_o_type,type,
    fun_fu1617828088232643505_nat_o: $tType ).

thf(fun_Pr1970694993525554974t_unit_type,type,
    fun_Pr1970694993525554974t_unit: $tType ).

thf(fun_he4944555133437423336it_nat_type,type,
    fun_he4944555133437423336it_nat: $tType ).

thf(fun_fu4618385802829667198_set_o_type,type,
    fun_fu4618385802829667198_set_o: $tType ).

thf(fun_Pr3456093102767711692t_unit_type,type,
    fun_Pr3456093102767711692t_unit: $tType ).

thf(fun_he281446669002384250it_nat_type,type,
    fun_he281446669002384250it_nat: $tType ).

thf(set_fu804515216739278420_int_o_type,type,
    set_fu804515216739278420_int_o: $tType ).

thf(fun_Pr8519750050727906972at_nat_type,type,
    fun_Pr8519750050727906972at_nat: $tType ).

thf(fun_fu7433494735876822851at_nat_type,type,
    fun_fu7433494735876822851at_nat: $tType ).

thf(fun_Pr7763680713840462443e_term_type,type,
    fun_Pr7763680713840462443e_term: $tType ).

thf(set_Pr1604112560894399303at_nat_type,type,
    set_Pr1604112560894399303at_nat: $tType ).

thf(set_Pr5052581263052047815nteger_type,type,
    set_Pr5052581263052047815nteger: $tType ).

thf(produc3911288613690379145it_nat_type,type,
    produc3911288613690379145it_nat: $tType ).

thf(fun_Pr7663348063272484276_nat_o_type,type,
    fun_Pr7663348063272484276_nat_o: $tType ).

thf(produc2867611627572283311it_nat_type,type,
    produc2867611627572283311it_nat: $tType ).

thf(fun_Pr6553355248451873380on_num_type,type,
    fun_Pr6553355248451873380on_num: $tType ).

thf(fun_fu3898734532474705027nt_int_type,type,
    fun_fu3898734532474705027nt_int: $tType ).

thf(fun_se2918291395271296516_nat_o_type,type,
    fun_se2918291395271296516_nat_o: $tType ).

thf(fun_na7330042712434367748_nat_o_type,type,
    fun_na7330042712434367748_nat_o: $tType ).

thf(fun_fu5631754973857388633nt_int_type,type,
    fun_fu5631754973857388633nt_int: $tType ).

thf(fun_Pr6171258863536582648it_nat_type,type,
    fun_Pr6171258863536582648it_nat: $tType ).

thf(fun_Pr7425815736541306438et_nat_type,type,
    fun_Pr7425815736541306438et_nat: $tType ).

thf(set_Pr633603713510679705it_nat_type,type,
    set_Pr633603713510679705it_nat: $tType ).

thf(fun_Pr6764980218223570944et_nat_type,type,
    fun_Pr6764980218223570944et_nat: $tType ).

thf(fun_na5670658592214072528at_nat_type,type,
    fun_na5670658592214072528at_nat: $tType ).

thf(fun_se8417120708266284045_nat_o_type,type,
    fun_se8417120708266284045_nat_o: $tType ).

thf(produc4788131091073775919nt_int_type,type,
    produc4788131091073775919nt_int: $tType ).

thf(produc5464280974217902119e_term_type,type,
    produc5464280974217902119e_term: $tType ).

thf(set_op989438649584373901at_nat_type,type,
    set_op989438649584373901at_nat: $tType ).

thf(option1583680563626158861at_nat_type,type,
    option1583680563626158861at_nat: $tType ).

thf(fun_fu353361380671289177nt_int_type,type,
    fun_fu353361380671289177nt_int: $tType ).

thf(fun_fu2354122332637403079_nat_o_type,type,
    fun_fu2354122332637403079_nat_o: $tType ).

thf(fun_fu8897902691871853255_int_o_type,type,
    fun_fu8897902691871853255_int_o: $tType ).

thf(fun_fu4482892469221626457nt_int_type,type,
    fun_fu4482892469221626457nt_int: $tType ).

thf(fun_fu8347129338434488602er_num_type,type,
    fun_fu8347129338434488602er_num: $tType ).

thf(fun_Pr8319229360018371625t_unit_type,type,
    fun_Pr8319229360018371625t_unit: $tType ).

thf(fun_nu1379135015814352922nteger_type,type,
    fun_nu1379135015814352922nteger: $tType ).

thf(fun_fu3472058528428720115nt_int_type,type,
    fun_fu3472058528428720115nt_int: $tType ).

thf(fun_Pr9081111800474865985e_term_type,type,
    fun_Pr9081111800474865985e_term: $tType ).

thf(set_Pr8551490117392284871at_nat_type,type,
    set_Pr8551490117392284871at_nat: $tType ).

thf(fun_fu2978539155105838238_int_o_type,type,
    fun_fu2978539155105838238_int_o: $tType ).

thf(fun_Pr7145817153658775868term_o_type,type,
    fun_Pr7145817153658775868term_o: $tType ).

thf(option5210736251575913683nteger_type,type,
    option5210736251575913683nteger: $tType ).

thf(fun_fu2677729659939697685_nat_o_type,type,
    fun_fu2677729659939697685_nat_o: $tType ).

thf(fun_Pr7459525001844076368t_unit_type,type,
    fun_Pr7459525001844076368t_unit: $tType ).

thf(set_Pr6777250647868329861it_nat_type,type,
    set_Pr6777250647868329861it_nat: $tType ).

thf(fun_Pr914940982395022178_nat_o_type,type,
    fun_Pr914940982395022178_nat_o: $tType ).

thf(fun_ar121531768175530460t_unit_type,type,
    fun_ar121531768175530460t_unit: $tType ).

thf(set_se5479201105039950375at_nat_type,type,
    set_se5479201105039950375at_nat: $tType ).

thf(produc7299876168958306407at_nat_type,type,
    produc7299876168958306407at_nat: $tType ).

thf(produc6756470014200349799atural_type,type,
    produc6756470014200349799atural: $tType ).

thf(produc3334582477557816039nteger_type,type,
    produc3334582477557816039nteger: $tType ).

thf(set_fu1867049230074397546_nat_o_type,type,
    set_fu1867049230074397546_nat_o: $tType ).

thf(fun_fu4083202260958266008eger_o_type,type,
    fun_fu4083202260958266008eger_o: $tType ).

thf(fun_fu7390737412436561923nteger_type,type,
    fun_fu7390737412436561923nteger: $tType ).

thf(fun_Pr1661544312997278575on_num_type,type,
    fun_Pr1661544312997278575on_num: $tType ).

thf(fun_nu8356290101743979119it_nat_type,type,
    fun_nu8356290101743979119it_nat: $tType ).

thf(fun_na5667031169817407269it_nat_type,type,
    fun_na5667031169817407269it_nat: $tType ).

thf(fun_in8543325783774419841it_nat_type,type,
    fun_in8543325783774419841it_nat: $tType ).

thf(fun_se7001366092147120942_nat_o_type,type,
    fun_se7001366092147120942_nat_o: $tType ).

thf(fun_se218054151627931304_nat_o_type,type,
    fun_se218054151627931304_nat_o: $tType ).

thf(fun_Pr2994431579521131585on_num_type,type,
    fun_Pr2994431579521131585on_num: $tType ).

thf(fun_Pr3592279944642289454ural_o_type,type,
    fun_Pr3592279944642289454ural_o: $tType ).

thf(fun_nu5903705430729240393it_nat_type,type,
    fun_nu5903705430729240393it_nat: $tType ).

thf(fun_na4198017608689007891it_nat_type,type,
    fun_na4198017608689007891it_nat: $tType ).

thf(fun_fu6201336427292363868nteger_type,type,
    fun_fu6201336427292363868nteger: $tType ).

thf(set_fu2713250876831336446atural_type,type,
    set_fu2713250876831336446atural: $tType ).

thf(produc3839731585411834681it_nat_type,type,
    produc3839731585411834681it_nat: $tType ).

thf(fun_fu257250443624047805ural_o_type,type,
    fun_fu257250443624047805ural_o: $tType ).

thf(fun_na1945018436707187408at_nat_type,type,
    fun_na1945018436707187408at_nat: $tType ).

thf(fun_Pr1253225528153422666at_nat_type,type,
    fun_Pr1253225528153422666at_nat: $tType ).

thf(fun_Pr6298746545499001766at_int_type,type,
    fun_Pr6298746545499001766at_int: $tType ).

thf(fun_fu2392828822626117773nteger_type,type,
    fun_fu2392828822626117773nteger: $tType ).

thf(fun_fu5844746416483971737nteger_type,type,
    fun_fu5844746416483971737nteger: $tType ).

thf(fun_fu2275682760404419928_num_o_type,type,
    fun_fu2275682760404419928_num_o: $tType ).

thf(fun_fu1677024581061081874_int_o_type,type,
    fun_fu1677024581061081874_int_o: $tType ).

thf(option8699557107911914541at_nat_type,type,
    option8699557107911914541at_nat: $tType ).

thf(set_op239864471688321678it_nat_type,type,
    set_op239864471688321678it_nat: $tType ).

thf(fun_se5991283330978499451_nat_o_type,type,
    fun_se5991283330978499451_nat_o: $tType ).

thf(fun_Pr7475791014719349342t_unit_type,type,
    fun_Pr7475791014719349342t_unit: $tType ).

thf(fun_op479301348043730329_nat_o_type,type,
    fun_op479301348043730329_nat_o: $tType ).

thf(fun_o_7229649064035662211it_nat_type,type,
    fun_o_7229649064035662211it_nat: $tType ).

thf(set_op3940070208846178154it_nat_type,type,
    set_op3940070208846178154it_nat: $tType ).

thf(produc4166570645942440679at_nat_type,type,
    produc4166570645942440679at_nat: $tType ).

thf(fun_fu2253997797533952707_nat_o_type,type,
    fun_fu2253997797533952707_nat_o: $tType ).

thf(fun_fu8028891822603792907_int_o_type,type,
    fun_fu8028891822603792907_int_o: $tType ).

thf(fun_fu7618250142905304443_nat_o_type,type,
    fun_fu7618250142905304443_nat_o: $tType ).

thf(fun_fu4169772131120368835_int_o_type,type,
    fun_fu4169772131120368835_int_o: $tType ).

thf(fun_op4751157287140997969_nat_o_type,type,
    fun_op4751157287140997969_nat_o: $tType ).

thf(fun_Pr8833188457053967342rray_a_type,type,
    fun_Pr8833188457053967342rray_a: $tType ).

thf(fun_fu4228150600790569371at_nat_type,type,
    fun_fu4228150600790569371at_nat: $tType ).

thf(fun_fu484727072080742171_nat_o_type,type,
    fun_fu484727072080742171_nat_o: $tType ).

thf(fun_fu1057420046263839031_rat_o_type,type,
    fun_fu1057420046263839031_rat_o: $tType ).

thf(produc3954786194548828667nteger_type,type,
    produc3954786194548828667nteger: $tType ).

thf(produc2900562427881843919it_nat_type,type,
    produc2900562427881843919it_nat: $tType ).

thf(fun_Pr2477239776880934807at_nat_type,type,
    fun_Pr2477239776880934807at_nat: $tType ).

thf(fun_Pr1308109350235310159nt_int_type,type,
    fun_Pr1308109350235310159nt_int: $tType ).

thf(set_Pr4329608150637261639at_nat_type,type,
    set_Pr4329608150637261639at_nat: $tType ).

thf(produc9217583074051984497at_nat_type,type,
    produc9217583074051984497at_nat: $tType ).

thf(fun_Pr3059359313727237556_nat_o_type,type,
    fun_Pr3059359313727237556_nat_o: $tType ).

thf(fun_fu4735791719682850818eger_o_type,type,
    fun_fu4735791719682850818eger_o: $tType ).

thf(fun_fu4946532526548972611_nat_o_type,type,
    fun_fu4946532526548972611_nat_o: $tType ).

thf(fun_Pr5131589689703537955atural_type,type,
    fun_Pr5131589689703537955atural: $tType ).

thf(fun_Pr74676805955934211atural_type,type,
    fun_Pr74676805955934211atural: $tType ).

thf(fun_Pr5876161306168176259nteger_type,type,
    fun_Pr5876161306168176259nteger: $tType ).

thf(fun_Co4337079049361313443atural_type,type,
    fun_Co4337079049361313443atural: $tType ).

thf(set_fu3555100300013713409atural_type,type,
    set_fu3555100300013713409atural: $tType ).

thf(set_fu2445755650934904413atural_type,type,
    set_fu2445755650934904413atural: $tType ).

thf(fun_fu4638078822479986034_int_o_type,type,
    fun_fu4638078822479986034_int_o: $tType ).

thf(fun_fu4306744791715064858_rat_o_type,type,
    fun_fu4306744791715064858_rat_o: $tType ).

thf(fun_fu9211935013670480870ural_o_type,type,
    fun_fu9211935013670480870ural_o: $tType ).

thf(fun_fu6699046866436802030_int_o_type,type,
    fun_fu6699046866436802030_int_o: $tType ).

thf(fun_fu660488089777143946ural_o_type,type,
    fun_fu660488089777143946ural_o: $tType ).

thf(set_fu5472951507345886094_nat_o_type,type,
    set_fu5472951507345886094_nat_o: $tType ).

thf(produc2752406535750279421nteger_type,type,
    produc2752406535750279421nteger: $tType ).

thf(fun_fu7530206860547196985at_nat_type,type,
    fun_fu7530206860547196985at_nat: $tType ).

thf(fun_fu8284676920001830735nteger_type,type,
    fun_fu8284676920001830735nteger: $tType ).

thf(fun_fu1188671613149117355nteger_type,type,
    fun_fu1188671613149117355nteger: $tType ).

thf(fun_Pr2548841491397842206atural_type,type,
    fun_Pr2548841491397842206atural: $tType ).

thf(fun_se3165749655728557022_nat_o_type,type,
    fun_se3165749655728557022_nat_o: $tType ).

thf(fun_fu4821026654811345315r_assn_type,type,
    fun_fu4821026654811345315r_assn: $tType ).

thf(fun_fu6327154928193479288nteger_type,type,
    fun_fu6327154928193479288nteger: $tType ).

thf(fun_fu4582018930532246947nt_rat_type,type,
    fun_fu4582018930532246947nt_rat: $tType ).

thf(fun_fu3518228427392506443nt_int_type,type,
    fun_fu3518228427392506443nt_int: $tType ).

thf(fun_fu8767785434844327952er_rat_type,type,
    fun_fu8767785434844327952er_rat: $tType ).

thf(fun_fu2498091903632033272er_nat_type,type,
    fun_fu2498091903632033272er_nat: $tType ).

thf(fun_fu1007793439646807308er_int_type,type,
    fun_fu1007793439646807308er_int: $tType ).

thf(fun_Pr1075626608990047775at_num_type,type,
    fun_Pr1075626608990047775at_num: $tType ).

thf(fun_Pr367382672041210069at_nat_type,type,
    fun_Pr367382672041210069at_nat: $tType ).

thf(fun_nu5234077238548837151it_nat_type,type,
    fun_nu5234077238548837151it_nat: $tType ).

thf(fun_Pr1223581030874358257at_num_type,type,
    fun_Pr1223581030874358257at_num: $tType ).

thf(fun_Pr515337093925520551at_nat_type,type,
    fun_Pr515337093925520551at_nat: $tType ).

thf(fun_nu2241728722996109699it_nat_type,type,
    fun_nu2241728722996109699it_nat: $tType ).

thf(fun_se7776568131818451942at_nat_type,type,
    fun_se7776568131818451942at_nat: $tType ).

thf(fun_se5286484986886725186at_int_type,type,
    fun_se5286484986886725186at_int: $tType ).

thf(fun_na8167864584424996432at_nat_type,type,
    fun_na8167864584424996432at_nat: $tType ).

thf(option8956607266484857688it_nat_type,type,
    option8956607266484857688it_nat: $tType ).

thf(fun_fu7344996400627858478_int_o_type,type,
    fun_fu7344996400627858478_int_o: $tType ).

thf(fun_fu4899062771603708206at_o_o_type,type,
    fun_fu4899062771603708206at_o_o: $tType ).

thf(fun_fu7590976836756945966nt_o_o_type,type,
    fun_fu7590976836756945966nt_o_o: $tType ).

thf(fun_fu8074799898941972270_int_o_type,type,
    fun_fu8074799898941972270_int_o: $tType ).

thf(option3216581401566546698it_nat_type,type,
    option3216581401566546698it_nat: $tType ).

thf(fun_se5244420045238757833at_nat_type,type,
    fun_se5244420045238757833at_nat: $tType ).

thf(fun_fu717549361983437348nt_int_type,type,
    fun_fu717549361983437348nt_int: $tType ).

thf(fun_fu918106826131887214nt_int_type,type,
    fun_fu918106826131887214nt_int: $tType ).

thf(produc5111566536631596683et_nat_type,type,
    produc5111566536631596683et_nat: $tType ).

thf(produc8299537390109905600et_nat_type,type,
    produc8299537390109905600et_nat: $tType ).

thf(fun_Pr2049426570021530256t_unit_type,type,
    fun_Pr2049426570021530256t_unit: $tType ).

thf(fun_mu2328110650637990531at_nat_type,type,
    fun_mu2328110650637990531at_nat: $tType ).

thf(produc217860453747927114_o_int_type,type,
    produc217860453747927114_o_int: $tType ).

thf(produc3843707927480180839at_nat_type,type,
    produc3843707927480180839at_nat: $tType ).

thf(fun_ar6017029185804945652rray_a_type,type,
    fun_ar6017029185804945652rray_a: $tType ).

thf(set_Pr1354866905816374718it_nat_type,type,
    set_Pr1354866905816374718it_nat: $tType ).

thf(fun_fu7141499545569947298eger_o_type,type,
    fun_fu7141499545569947298eger_o: $tType ).

thf(fun_Pr8032424337255632745_nat_o_type,type,
    fun_Pr8032424337255632745_nat_o: $tType ).

thf(fun_Co2051191115980488992_nat_o_type,type,
    fun_Co2051191115980488992_nat_o: $tType ).

thf(fun_Co9016714620104711083_nat_o_type,type,
    fun_Co9016714620104711083_nat_o: $tType ).

thf(set_Pr457366540195662369at_nat_type,type,
    set_Pr457366540195662369at_nat: $tType ).

thf(set_Pr5142436192348053284it_nat_type,type,
    set_Pr5142436192348053284it_nat: $tType ).

thf(fun_fu3997796857297124035at_rat_type,type,
    fun_fu3997796857297124035at_rat: $tType ).

thf(fun_fu3064074204415222357nt_int_type,type,
    fun_fu3064074204415222357nt_int: $tType ).

thf(fun_fu1098312133097393581at_rat_type,type,
    fun_fu1098312133097393581at_rat: $tType ).

thf(fun_fu3661779633992098115nt_int_type,type,
    fun_fu3661779633992098115nt_int: $tType ).

thf(fun_se953073389798102371at_nat_type,type,
    fun_se953073389798102371at_nat: $tType ).

thf(fun_Pr557098546508347797at_nat_type,type,
    fun_Pr557098546508347797at_nat: $tType ).

thf(fun_Pr7068637894315934487_nat_o_type,type,
    fun_Pr7068637894315934487_nat_o: $tType ).

thf(fun_na1668100129766719005at_nat_type,type,
    fun_na1668100129766719005at_nat: $tType ).

thf(fun_na2094359461478415435atural_type,type,
    fun_na2094359461478415435atural: $tType ).

thf(fun_in4857920871562217639atural_type,type,
    fun_in4857920871562217639atural: $tType ).

thf(fun_se5639961202347202350_nat_o_type,type,
    fun_se5639961202347202350_nat_o: $tType ).

thf(fun_Pr2419607445322970330t_unit_type,type,
    fun_Pr2419607445322970330t_unit: $tType ).

thf(produc1164942017926883148rm_int_type,type,
    produc1164942017926883148rm_int: $tType ).

thf(fun_fu9045186299510176150at_o_o_type,type,
    fun_fu9045186299510176150at_o_o: $tType ).

thf(fun_fu1723132215250845724er_nat_type,type,
    fun_fu1723132215250845724er_nat: $tType ).

thf(fun_fu1491972344133157660er_int_type,type,
    fun_fu1491972344133157660er_int: $tType ).

thf(fun_fu1895414074638732388er_int_type,type,
    fun_fu1895414074638732388er_int: $tType ).

thf(fun_Co2470855966376689427nteger_type,type,
    fun_Co2470855966376689427nteger: $tType ).

thf(fun_Co298994598804093668e_term_type,type,
    fun_Co298994598804093668e_term: $tType ).

thf(fun_Co1966082167426949785e_term_type,type,
    fun_Co1966082167426949785e_term: $tType ).

thf(fun_Pr8866567302531502864at_nat_type,type,
    fun_Pr8866567302531502864at_nat: $tType ).

thf(fun_fu2310701194077331499nteger_type,type,
    fun_fu2310701194077331499nteger: $tType ).

thf(fun_fu6017686703198564611er_rat_type,type,
    fun_fu6017686703198564611er_rat: $tType ).

thf(fun_fu4961913266064405537nteger_type,type,
    fun_fu4961913266064405537nteger: $tType ).

thf(fun_fu717556231145110950r_assn_type,type,
    fun_fu717556231145110950r_assn: $tType ).

thf(fun_fu4788845708739168348eger_o_type,type,
    fun_fu4788845708739168348eger_o: $tType ).

thf(fun_fu6802859072977114247_nat_o_type,type,
    fun_fu6802859072977114247_nat_o: $tType ).

thf(fun_fu14259429304446855_int_o_type,type,
    fun_fu14259429304446855_int_o: $tType ).

thf(set_Pr2352657477744078772atural_type,type,
    set_Pr2352657477744078772atural: $tType ).

thf(fun_Pr3587966566883452857at_nat_type,type,
    fun_Pr3587966566883452857at_nat: $tType ).

thf(fun_Pr513970351136536563ural_o_type,type,
    fun_Pr513970351136536563ural_o: $tType ).

thf(fun_ar8857663332695973421at_nat_type,type,
    fun_ar8857663332695973421at_nat: $tType ).

thf(fun_fu7456240966027273028at_o_o_type,type,
    fun_fu7456240966027273028at_o_o: $tType ).

thf(fun_fu4957514873648614724at_o_o_type,type,
    fun_fu4957514873648614724at_o_o: $tType ).

thf(fun_fu6215369687776649212nt_o_o_type,type,
    fun_fu6215369687776649212nt_o_o: $tType ).

thf(fun_fu5378497120668327052at_o_o_type,type,
    fun_fu5378497120668327052at_o_o: $tType ).

thf(fun_fu4137625842417703236nt_o_o_type,type,
    fun_fu4137625842417703236nt_o_o: $tType ).

thf(fun_fu7129310890971069252nt_o_o_type,type,
    fun_fu7129310890971069252nt_o_o: $tType ).

thf(produc8065447618272157327et_nat_type,type,
    produc8065447618272157327et_nat: $tType ).

thf(fun_fu7405491065986884212t_assn_type,type,
    fun_fu7405491065986884212t_assn: $tType ).

thf(set_Pr8693737435421807431at_nat_type,type,
    set_Pr8693737435421807431at_nat: $tType ).

thf(set_Pr2560585780119916871nt_int_type,type,
    set_Pr2560585780119916871nt_int: $tType ).

thf(fun_fu3959123160307459545t_assn_type,type,
    fun_fu3959123160307459545t_assn: $tType ).

thf(fun_Pr363642936170290612_nat_o_type,type,
    fun_Pr363642936170290612_nat_o: $tType ).

thf(fun_Pr3337834798857116037et_nat_type,type,
    fun_Pr3337834798857116037et_nat: $tType ).

thf(fun_Pr847751653925389281et_int_type,type,
    fun_Pr847751653925389281et_int: $tType ).

thf(fun_Co4803750647967840348et_nat_type,type,
    fun_Co4803750647967840348et_nat: $tType ).

thf(produc8664842809031399944it_nat_type,type,
    produc8664842809031399944it_nat: $tType ).

thf(fun_fu8532066432991188095_nat_o_type,type,
    fun_fu8532066432991188095_nat_o: $tType ).

thf(fun_fu63825462011493995_int_o_type,type,
    fun_fu63825462011493995_int_o: $tType ).

thf(fun_in1927439276604979228_nat_o_type,type,
    fun_in1927439276604979228_nat_o: $tType ).

thf(produc732395585841259969at_nat_type,type,
    produc732395585841259969at_nat: $tType ).

thf(produc6714399278180371524it_nat_type,type,
    produc6714399278180371524it_nat: $tType ).

thf(fun_se320340636488258563at_nat_type,type,
    fun_se320340636488258563at_nat: $tType ).

thf(fun_Pr5733170697710890607et_nat_type,type,
    fun_Pr5733170697710890607et_nat: $tType ).

thf(fun_Pr5056853159479207325nteger_type,type,
    fun_Pr5056853159479207325nteger: $tType ).

thf(fun_Pr5596209257725365771nt_int_type,type,
    fun_Pr5596209257725365771nt_int: $tType ).

thf(fun_fu381918921314004384at_nat_type,type,
    fun_fu381918921314004384at_nat: $tType ).

thf(fun_na8508211072120413978_nat_o_type,type,
    fun_na8508211072120413978_nat_o: $tType ).

thf(set_Pr1932065953672099015od_o_o_type,type,
    set_Pr1932065953672099015od_o_o: $tType ).

thf(fun_fu3275390434952296369_nat_o_type,type,
    fun_fu3275390434952296369_nat_o: $tType ).

thf(fun_op386870758422531628et_nat_type,type,
    fun_op386870758422531628et_nat: $tType ).

thf(fun_op8756596739451609009nteger_type,type,
    fun_op8756596739451609009nteger: $tType ).

thf(fun_fu5660447535128473811at_nat_type,type,
    fun_fu5660447535128473811at_nat: $tType ).

thf(fun_fu7012516915885544207at_nat_type,type,
    fun_fu7012516915885544207at_nat: $tType ).

thf(fun_fu2668056085831081835nt_nat_type,type,
    fun_fu2668056085831081835nt_nat: $tType ).

thf(fun_fu3125320701163054607at_int_type,type,
    fun_fu3125320701163054607at_int: $tType ).

thf(fun_fu5207212825597307859nt_int_type,type,
    fun_fu5207212825597307859nt_int: $tType ).

thf(fun_fu4152238915952267095at_int_type,type,
    fun_fu4152238915952267095at_int: $tType ).

thf(fun_fu6714502955005156803_nat_o_type,type,
    fun_fu6714502955005156803_nat_o: $tType ).

thf(fun_fu4568065243339218371_nat_o_type,type,
    fun_fu4568065243339218371_nat_o: $tType ).

thf(fun_in94812177438132456e_term_type,type,
    fun_in94812177438132456e_term: $tType ).

thf(fun_he6845747896722556172t_unit_type,type,
    fun_he6845747896722556172t_unit: $tType ).

thf(fun_Co7921331830460615208atural_type,type,
    fun_Co7921331830460615208atural: $tType ).

thf(fun_fu7925354201654153025t_assn_type,type,
    fun_fu7925354201654153025t_assn: $tType ).

thf(fun_fu1763652423599918571nteger_type,type,
    fun_fu1763652423599918571nteger: $tType ).

thf(fun_fu727159081937814839r_assn_type,type,
    fun_fu727159081937814839r_assn: $tType ).

thf(fun_fu1832432239164473695eger_o_type,type,
    fun_fu1832432239164473695eger_o: $tType ).

thf(fun_fu6471771360118961870_int_o_type,type,
    fun_fu6471771360118961870_int_o: $tType ).

thf(fun_fu6011537917091710943eger_o_type,type,
    fun_fu6011537917091710943eger_o: $tType ).

thf(fun_fu8741070064424208326assn_o_type,type,
    fun_fu8741070064424208326assn_o: $tType ).

thf(fun_fu2770652263662631110eger_o_type,type,
    fun_fu2770652263662631110eger_o: $tType ).

thf(fun_Pr5633121574208248783_set_o_type,type,
    fun_Pr5633121574208248783_set_o: $tType ).

thf(set_fu3555266933746557007_nat_o_type,type,
    set_fu3555266933746557007_nat_o: $tType ).

thf(fun_fu1045876692016343459nteger_type,type,
    fun_fu1045876692016343459nteger: $tType ).

thf(fun_fu1413608398870722896at_nat_type,type,
    fun_fu1413608398870722896at_nat: $tType ).

thf(fun_fu5135969500543783852at_o_o_type,type,
    fun_fu5135969500543783852at_o_o: $tType ).

thf(fun_na8713714802964096592at_nat_type,type,
    fun_na8713714802964096592at_nat: $tType ).

thf(produc3981471736659609608atural_type,type,
    produc3981471736659609608atural: $tType ).

thf(produc5835291356934675326atural_type,type,
    produc5835291356934675326atural: $tType ).

thf(produc3346328345660746739nteger_type,type,
    produc3346328345660746739nteger: $tType ).

thf(fun_fu9062970525541950460_nat_o_type,type,
    fun_fu9062970525541950460_nat_o: $tType ).

thf(fun_Pr7804344347641417161at_nat_type,type,
    fun_Pr7804344347641417161at_nat: $tType ).

thf(fun_op5903753652030861359t_unit_type,type,
    fun_op5903753652030861359t_unit: $tType ).

thf(fun_Co2944084857415636034atural_type,type,
    fun_Co2944084857415636034atural: $tType ).

thf(fun_fu7677565902479959693_rat_o_type,type,
    fun_fu7677565902479959693_rat_o: $tType ).

thf(fun_Pr3928691295121555099ural_o_type,type,
    fun_Pr3928691295121555099ural_o: $tType ).

thf(fun_Co9066792663755620495ural_o_type,type,
    fun_Co9066792663755620495ural_o: $tType ).

thf(fun_Co6386927884524458043e_term_type,type,
    fun_Co6386927884524458043e_term: $tType ).

thf(fun_Co3544761417380347684eger_o_type,type,
    fun_Co3544761417380347684eger_o: $tType ).

thf(fun_Co3460408610320954864e_term_type,type,
    fun_Co3460408610320954864e_term: $tType ).

thf(set_fu3629540756087427317e_term_type,type,
    set_fu3629540756087427317e_term: $tType ).

thf(fun_fu3265955482920998386term_o_type,type,
    fun_fu3265955482920998386term_o: $tType ).

thf(produc859450856879609959at_nat_type,type,
    produc859450856879609959at_nat: $tType ).

thf(produc1219242969750017639nt_int_type,type,
    produc1219242969750017639nt_int: $tType ).

thf(fun_fu3744699754670041014er_rat_type,type,
    fun_fu3744699754670041014er_rat: $tType ).

thf(fun_in4666789911842550827et_nat_type,type,
    fun_in4666789911842550827et_nat: $tType ).

thf(set_fu2374436075715859015nteger_type,type,
    set_fu2374436075715859015nteger: $tType ).

thf(fun_fu4285281161728579104eger_o_type,type,
    fun_fu4285281161728579104eger_o: $tType ).

thf(fun_fu3109912920687205353_nat_o_type,type,
    fun_fu3109912920687205353_nat_o: $tType ).

thf(fun_fu607692679349591509_int_o_type,type,
    fun_fu607692679349591509_int_o: $tType ).

thf(fun_fu5766609707292941056eger_o_type,type,
    fun_fu5766609707292941056eger_o: $tType ).

thf(fun_Pr1469247711798767971at_nat_type,type,
    fun_Pr1469247711798767971at_nat: $tType ).

thf(fun_Pr5243970527273625488nteger_type,type,
    fun_Pr5243970527273625488nteger: $tType ).

thf(fun_Pr2029408141414424556nteger_type,type,
    fun_Pr2029408141414424556nteger: $tType ).

thf(fun_Pr2600655309230267920er_nat_type,type,
    fun_Pr2600655309230267920er_nat: $tType ).

thf(fun_Pr110572164298541164er_int_type,type,
    fun_Pr110572164298541164er_int: $tType ).

thf(fun_Pr3118124138693225744er_int_type,type,
    fun_Pr3118124138693225744er_int: $tType ).

thf(fun_Pr5398690294390750379at_nat_type,type,
    fun_Pr5398690294390750379at_nat: $tType ).

thf(option936205604648967762et_nat_type,type,
    option936205604648967762et_nat: $tType ).

thf(fun_fu8391177546919232046_nat_o_type,type,
    fun_fu8391177546919232046_nat_o: $tType ).

thf(fun_fu7503566767892366382_int_o_type,type,
    fun_fu7503566767892366382_int_o: $tType ).

thf(fun_Pr4799464687642144302_num_o_type,type,
    fun_Pr4799464687642144302_num_o: $tType ).

thf(fun_Pr2028404973800837934_nat_o_type,type,
    fun_Pr2028404973800837934_nat_o: $tType ).

thf(fun_Pr9018117161326028078_int_o_type,type,
    fun_Pr9018117161326028078_int_o: $tType ).

thf(fun_Pr9045474026565384218t_unit_type,type,
    fun_Pr9045474026565384218t_unit: $tType ).

thf(produc2934264451710624999od_o_o_type,type,
    produc2934264451710624999od_o_o: $tType ).

thf(fun_Pr8777304358194983264rray_a_type,type,
    fun_Pr8777304358194983264rray_a: $tType ).

thf(fun_na5644505769342238765nteger_type,type,
    fun_na5644505769342238765nteger: $tType ).

thf(set_Pr7577011563204128103nteger_type,type,
    set_Pr7577011563204128103nteger: $tType ).

thf(fun_fu1171974497074579908it_rat_type,type,
    fun_fu1171974497074579908it_rat: $tType ).

thf(fun_se4014881416909572940_nat_o_type,type,
    fun_se4014881416909572940_nat_o: $tType ).

thf(fun_na3424944204176166544_nat_o_type,type,
    fun_na3424944204176166544_nat_o: $tType ).

thf(fun_fu6778223257468740055_nat_o_type,type,
    fun_fu6778223257468740055_nat_o: $tType ).

thf(fun_fu8704076394632857761nt_rat_type,type,
    fun_fu8704076394632857761nt_rat: $tType ).

thf(fun_fu1217771548038759377at_nat_type,type,
    fun_fu1217771548038759377at_nat: $tType ).

thf(fun_fu6579618355643354601at_rat_type,type,
    fun_fu6579618355643354601at_rat: $tType ).

thf(fun_fu3670889464739865373nt_num_type,type,
    fun_fu3670889464739865373nt_num: $tType ).

thf(fun_fu5935951186182374353at_nat_type,type,
    fun_fu5935951186182374353at_nat: $tType ).

thf(fun_fu960360787657196261at_int_type,type,
    fun_fu960360787657196261at_int: $tType ).

thf(fun_fu1995072252941043084t_assn_type,type,
    fun_fu1995072252941043084t_assn: $tType ).

thf(fun_fu6092417073193843705nt_int_type,type,
    fun_fu6092417073193843705nt_int: $tType ).

thf(fun_fu1617438229336688381nt_rat_type,type,
    fun_fu1617438229336688381nt_rat: $tType ).

thf(fun_fu973771059875708133nt_nat_type,type,
    fun_fu973771059875708133nt_nat: $tType ).

thf(fun_fu7510501037550790335nteger_type,type,
    fun_fu7510501037550790335nteger: $tType ).

thf(fun_fu4482299812767249988t_assn_type,type,
    fun_fu4482299812767249988t_assn: $tType ).

thf(fun_fu8198789307943805079er_rat_type,type,
    fun_fu8198789307943805079er_rat: $tType ).

thf(fun_fu1714096010366225192nteger_type,type,
    fun_fu1714096010366225192nteger: $tType ).

thf(fun_fu2219603532186391848nteger_type,type,
    fun_fu2219603532186391848nteger: $tType ).

thf(fun_fu5082522747898945281r_assn_type,type,
    fun_fu5082522747898945281r_assn: $tType ).

thf(set_Pr3948176798113811640et_nat_type,type,
    set_Pr3948176798113811640et_nat: $tType ).

thf(fun_fu2627094579170320592ural_o_type,type,
    fun_fu2627094579170320592ural_o: $tType ).

thf(fun_fu841611025618976102eger_o_type,type,
    fun_fu841611025618976102eger_o: $tType ).

thf(fun_fu3131294797999541474eger_o_type,type,
    fun_fu3131294797999541474eger_o: $tType ).

thf(fun_fu5877413357861189036eger_o_type,type,
    fun_fu5877413357861189036eger_o: $tType ).

thf(fun_fu2034268335391280352ural_o_type,type,
    fun_fu2034268335391280352ural_o: $tType ).

thf(fun_fu248784781839935862eger_o_type,type,
    fun_fu248784781839935862eger_o: $tType ).

thf(fun_fu6536794386266229110eger_o_type,type,
    fun_fu6536794386266229110eger_o: $tType ).

thf(fun_fu2512357375982829608ural_o_type,type,
    fun_fu2512357375982829608ural_o: $tType ).

thf(fun_fu726873822431485118eger_o_type,type,
    fun_fu726873822431485118eger_o: $tType ).

thf(fun_fu1378022486368508006_rat_o_type,type,
    fun_fu1378022486368508006_rat_o: $tType ).

thf(fun_fu5250823318952805804_num_o_type,type,
    fun_fu5250823318952805804_num_o: $tType ).

thf(fun_fu4924233495492459638_nat_o_type,type,
    fun_fu4924233495492459638_nat_o: $tType ).

thf(fun_fu7320023857087329562_nat_o_type,type,
    fun_fu7320023857087329562_nat_o: $tType ).

thf(fun_fu7391974349310290878_int_o_type,type,
    fun_fu7391974349310290878_int_o: $tType ).

thf(fun_fu829217510089154608assn_o_type,type,
    fun_fu829217510089154608assn_o: $tType ).

thf(fun_Pr6460944699146269935_nat_o_type,type,
    fun_Pr6460944699146269935_nat_o: $tType ).

thf(fun_fu3743863873453506915o_assn_type,type,
    fun_fu3743863873453506915o_assn: $tType ).

thf(produc6162884466328367972nteger_type,type,
    produc6162884466328367972nteger: $tType ).

thf(fun_fu1853282479105234414at_o_o_type,type,
    fun_fu1853282479105234414at_o_o: $tType ).

thf(fun_fu3604077110225719534nt_o_o_type,type,
    fun_fu3604077110225719534nt_o_o: $tType ).

thf(fun_Pr1057819736042215569_nat_o_type,type,
    fun_Pr1057819736042215569_nat_o: $tType ).

thf(fun_Pr8338385031646565611_nat_o_type,type,
    fun_Pr8338385031646565611_nat_o: $tType ).

thf(fun_fu2987389051837124479on_num_type,type,
    fun_fu2987389051837124479on_num: $tType ).

thf(fun_fu8716660765737269145un_o_o_type,type,
    fun_fu8716660765737269145un_o_o: $tType ).

thf(fun_op4146996366486250514n_assn_type,type,
    fun_op4146996366486250514n_assn: $tType ).

thf(fun_fu4522195968571808382nt_int_type,type,
    fun_fu4522195968571808382nt_int: $tType ).

thf(fun_fu7460908759652350970nt_rat_type,type,
    fun_fu7460908759652350970nt_rat: $tType ).

thf(fun_Pr6405077315951356852et_nat_type,type,
    fun_Pr6405077315951356852et_nat: $tType ).

thf(fun_Pr3914994171019630096et_int_type,type,
    fun_Pr3914994171019630096et_int: $tType ).

thf(fun_Pr6596356882939945227nteger_type,type,
    fun_Pr6596356882939945227nteger: $tType ).

thf(fun_na4143055713577223196at_nat_type,type,
    fun_na4143055713577223196at_nat: $tType ).

thf(fun_in2204242111582549184nt_int_type,type,
    fun_in2204242111582549184nt_int: $tType ).

thf(fun_Co6597186368970283863nteger_type,type,
    fun_Co6597186368970283863nteger: $tType ).

thf(set_fu4273546686648440324nteger_type,type,
    set_fu4273546686648440324nteger: $tType ).

thf(set_fu2873095257816804008nteger_type,type,
    set_fu2873095257816804008nteger: $tType ).

thf(fun_fu5503004773767123511eger_o_type,type,
    fun_fu5503004773767123511eger_o: $tType ).

thf(fun_fu2721382957917623308_nat_o_type,type,
    fun_fu2721382957917623308_nat_o: $tType ).

thf(fun_fu7325869825756301971eger_o_type,type,
    fun_fu7325869825756301971eger_o: $tType ).

thf(fun_in5730379987311621695e_term_type,type,
    fun_in5730379987311621695e_term: $tType ).

thf(set_fu1437006448190940916_nat_o_type,type,
    set_fu1437006448190940916_nat_o: $tType ).

thf(fun_fu9090758901314268781nt_o_o_type,type,
    fun_fu9090758901314268781nt_o_o: $tType ).

thf(fun_fu5650529485467354185_nat_o_type,type,
    fun_fu5650529485467354185_nat_o: $tType ).

thf(fun_fu6749285349733798471at_o_o_type,type,
    fun_fu6749285349733798471at_o_o: $tType ).

thf(fun_se8125625266612218818et_nat_type,type,
    fun_se8125625266612218818et_nat: $tType ).

thf(fun_se3841591170510310256nteger_type,type,
    fun_se3841591170510310256nteger: $tType ).

thf(fun_Pr3616673511947161127atural_type,type,
    fun_Pr3616673511947161127atural: $tType ).

thf(fun_Pr864343514034809617nteger_type,type,
    fun_Pr864343514034809617nteger: $tType ).

thf(fun_Pr8136591464420530493_nat_o_type,type,
    fun_Pr8136591464420530493_nat_o: $tType ).

thf(fun_Pr4343998633453697049at_nat_type,type,
    fun_Pr4343998633453697049at_nat: $tType ).

thf(fun_fu1806770557662746761_nat_o_type,type,
    fun_fu1806770557662746761_nat_o: $tType ).

thf(fun_fu6075382464776002713_nat_o_type,type,
    fun_fu6075382464776002713_nat_o: $tType ).

thf(fun_fu4239617643652599019assn_o_type,type,
    fun_fu4239617643652599019assn_o: $tType ).

thf(fun_fu5719784276005855083eger_o_type,type,
    fun_fu5719784276005855083eger_o: $tType ).

thf(fun_fu7714913403879666293_int_o_type,type,
    fun_fu7714913403879666293_int_o: $tType ).

thf(fun_fu855086506144988854eger_o_type,type,
    fun_fu855086506144988854eger_o: $tType ).

thf(fun_fu2729256655946442782nteger_type,type,
    fun_fu2729256655946442782nteger: $tType ).

thf(fun_Pr2118491707810114563at_nat_type,type,
    fun_Pr2118491707810114563at_nat: $tType ).

thf(fun_Pr8851780599733163615at_int_type,type,
    fun_Pr8851780599733163615at_int: $tType ).

thf(fun_Pr4305413282503136351nt_nat_type,type,
    fun_Pr4305413282503136351nt_nat: $tType ).

thf(fun_Pr1815330137571409595nt_int_type,type,
    fun_Pr1815330137571409595nt_int: $tType ).

thf(fun_Pr7754697619089165059at_int_type,type,
    fun_Pr7754697619089165059at_int: $tType ).

thf(fun_Pr2478283820680522243nt_int_type,type,
    fun_Pr2478283820680522243nt_int: $tType ).

thf(fun_na1790740735814032627at_nat_type,type,
    fun_na1790740735814032627at_nat: $tType ).

thf(fun_na3504973565017656480nteger_type,type,
    fun_na3504973565017656480nteger: $tType ).

thf(fun_na5353050896416397052nteger_type,type,
    fun_na5353050896416397052nteger: $tType ).

thf(fun_na2743204842065625888er_nat_type,type,
    fun_na2743204842065625888er_nat: $tType ).

thf(fun_na7153028460132482940er_int_type,type,
    fun_na7153028460132482940er_int: $tType ).

thf(fun_na937208397672391712er_int_type,type,
    fun_na937208397672391712er_int: $tType ).

thf(set_se3372686590935047281atural_type,type,
    set_se3372686590935047281atural: $tType ).

thf(produc6491284506569428743nteger_type,type,
    produc6491284506569428743nteger: $tType ).

thf(fun_Pr3455331679158536364_nat_o_type,type,
    fun_Pr3455331679158536364_nat_o: $tType ).

thf(fun_Pr1817902730575146976_set_o_type,type,
    fun_Pr1817902730575146976_set_o: $tType ).

thf(fun_na5914473681949881652_nat_o_type,type,
    fun_na5914473681949881652_nat_o: $tType ).

thf(fun_he8708342781048922188t_unit_type,type,
    fun_he8708342781048922188t_unit: $tType ).

thf(fun_se7283963663803345157_set_o_type,type,
    fun_se7283963663803345157_set_o: $tType ).

thf(fun_Pr2088208266900590058et_nat_type,type,
    fun_Pr2088208266900590058et_nat: $tType ).

thf(fun_he4035479571739904452rray_a_type,type,
    fun_he4035479571739904452rray_a: $tType ).

thf(fun_fu552866168194876645nteger_type,type,
    fun_fu552866168194876645nteger: $tType ).

thf(fun_fu6924846375782198887atural_type,type,
    fun_fu6924846375782198887atural: $tType ).

thf(fun_fu2499394402704830801nteger_type,type,
    fun_fu2499394402704830801nteger: $tType ).

thf(fun_fu8508204053700405677nteger_type,type,
    fun_fu8508204053700405677nteger: $tType ).

thf(fun_fu6921880696561781257nteger_type,type,
    fun_fu6921880696561781257nteger: $tType ).

thf(fun_fu3628599891403802633nteger_type,type,
    fun_fu3628599891403802633nteger: $tType ).

thf(fun_fu6757290529232567765t_assn_type,type,
    fun_fu6757290529232567765t_assn: $tType ).

thf(fun_fu722387130092441185er_rat_type,type,
    fun_fu722387130092441185er_rat: $tType ).

thf(fun_fu9168018664657815141nteger_type,type,
    fun_fu9168018664657815141nteger: $tType ).

thf(fun_fu7724909810345500241er_nat_type,type,
    fun_fu7724909810345500241er_nat: $tType ).

thf(fun_fu2894000772521619117er_nat_type,type,
    fun_fu2894000772521619117er_nat: $tType ).

thf(fun_fu403917627589892361er_int_type,type,
    fun_fu403917627589892361er_int: $tType ).

thf(fun_na8856381646659805649nteger_type,type,
    fun_na8856381646659805649nteger: $tType ).

thf(fun_Co200561849269645671atural_type,type,
    fun_Co200561849269645671atural: $tType ).

thf(fun_Co5080488584548667985nteger_type,type,
    fun_Co5080488584548667985nteger: $tType ).

thf(produc3658429121746597890et_nat_type,type,
    produc3658429121746597890et_nat: $tType ).

thf(fun_fu6196024946523381971eger_o_type,type,
    fun_fu6196024946523381971eger_o: $tType ).

thf(fun_fu9167764846409469779_num_o_type,type,
    fun_fu9167764846409469779_num_o: $tType ).

thf(fun_fu8841175022949123613_nat_o_type,type,
    fun_fu8841175022949123613_nat_o: $tType ).

thf(fun_fu5056201337121744443_rat_o_type,type,
    fun_fu5056201337121744443_rat_o: $tType ).

thf(fun_fu3689012285533931075_nat_o_type,type,
    fun_fu3689012285533931075_nat_o: $tType ).

thf(fun_fu3760962777756892391_int_o_type,type,
    fun_fu3760962777756892391_int_o: $tType ).

thf(fun_fu6461175078876253408assn_o_type,type,
    fun_fu6461175078876253408assn_o: $tType ).

thf(fun_fu914036251014348755eger_o_type,type,
    fun_fu914036251014348755eger_o: $tType ).

thf(fun_fu5133016914843556765eger_o_type,type,
    fun_fu5133016914843556765eger_o: $tType ).

thf(fun_fu4844139638962010283eger_o_type,type,
    fun_fu4844139638962010283eger_o: $tType ).

thf(fun_fu1898041513128675305r_assn_type,type,
    fun_fu1898041513128675305r_assn: $tType ).

thf(fun_fu2448905236868045008_rat_o_type,type,
    fun_fu2448905236868045008_rat_o: $tType ).

thf(fun_fu5995116245991996640_nat_o_type,type,
    fun_fu5995116245991996640_nat_o: $tType ).

thf(fun_fu8462857099809827880_int_o_type,type,
    fun_fu8462857099809827880_int_o: $tType ).

thf(fun_se5529282185252607396eger_o_type,type,
    fun_se5529282185252607396eger_o: $tType ).

thf(fun_fu6849062756650152291_o_rat_type,type,
    fun_fu6849062756650152291_o_rat: $tType ).

thf(fun_fu1060865441899640675_o_nat_type,type,
    fun_fu1060865441899640675_o_nat: $tType ).

thf(fun_fu6436183194761443139_nat_o_type,type,
    fun_fu6436183194761443139_nat_o: $tType ).

thf(fun_fu927436805355353155_nat_o_type,type,
    fun_fu927436805355353155_nat_o: $tType ).

thf(fun_fu138107234227827011_int_o_type,type,
    fun_fu138107234227827011_int_o: $tType ).

thf(fun_fu6303754889700780451nteger_type,type,
    fun_fu6303754889700780451nteger: $tType ).

thf(fun_fu1324339541976909620o_assn_type,type,
    fun_fu1324339541976909620o_assn: $tType ).

thf(fun_Pr648072847990616533t_unit_type,type,
    fun_Pr648072847990616533t_unit: $tType ).

thf(set_Pr7477759153910077568at_num_type,type,
    set_Pr7477759153910077568at_num: $tType ).

thf(set_Pr2539167527615954998at_nat_type,type,
    set_Pr2539167527615954998at_nat: $tType ).

thf(set_Pr7717912310451564380at_nat_type,type,
    set_Pr7717912310451564380at_nat: $tType ).

thf(produc366245978424229472at_nat_type,type,
    produc366245978424229472at_nat: $tType ).

thf(produc3313772616054891654at_nat_type,type,
    produc3313772616054891654at_nat: $tType ).

thf(produc5665947927044467078nt_int_type,type,
    produc5665947927044467078nt_int: $tType ).

thf(produc382792921321436433nt_int_type,type,
    produc382792921321436433nt_int: $tType ).

thf(fun_fu5861359551626625881un_o_o_type,type,
    fun_fu5861359551626625881un_o_o: $tType ).

thf(fun_op1637087682669155543nteger_type,type,
    fun_op1637087682669155543nteger: $tType ).

thf(fun_se8575562297434572672at_int_type,type,
    fun_se8575562297434572672at_int: $tType ).

thf(fun_Pr4523587930069869694nteger_type,type,
    fun_Pr4523587930069869694nteger: $tType ).

thf(fun_Pr3662307866719382234nteger_type,type,
    fun_Pr3662307866719382234nteger: $tType ).

thf(fun_Pr2804840792690441492al_nat_type,type,
    fun_Pr2804840792690441492al_nat: $tType ).

thf(fun_Pr5940403383236205310nteger_type,type,
    fun_Pr5940403383236205310nteger: $tType ).

thf(fun_Pr2725840997377004378nteger_type,type,
    fun_Pr2725840997377004378nteger: $tType ).

thf(fun_na6574806417004769082atural_type,type,
    fun_na6574806417004769082atural: $tType ).

thf(fun_na3822476419092417572nteger_type,type,
    fun_na3822476419092417572nteger: $tType ).

thf(fun_in7496697025202066910atural_type,type,
    fun_in7496697025202066910atural: $tType ).

thf(fun_in4744367027289715400nteger_type,type,
    fun_in4744367027289715400nteger: $tType ).

thf(fun_se7755072775241076291_nat_o_type,type,
    fun_se7755072775241076291_nat_o: $tType ).

thf(fun_op3284592519439835779_nat_o_type,type,
    fun_op3284592519439835779_nat_o: $tType ).

thf(fun_na4518284863240432007_nat_o_type,type,
    fun_na4518284863240432007_nat_o: $tType ).

thf(fun_fu7075445697382584196_int_o_type,type,
    fun_fu7075445697382584196_int_o: $tType ).

thf(fun_in7664021439913478804_nat_o_type,type,
    fun_in7664021439913478804_nat_o: $tType ).

thf(option5403585828896915703atural_type,type,
    option5403585828896915703atural: $tType ).

thf(option2651255830984564193nteger_type,type,
    option2651255830984564193nteger: $tType ).

thf(fun_fu4710970720072501148at_rat_type,type,
    fun_fu4710970720072501148at_rat: $tType ).

thf(fun_fu2312272580554962172_nat_o_type,type,
    fun_fu2312272580554962172_nat_o: $tType ).

thf(fun_fu114989186063767636nt_rat_type,type,
    fun_fu114989186063767636nt_rat: $tType ).

thf(fun_fu5158109473865063676nt_rat_type,type,
    fun_fu5158109473865063676nt_rat: $tType ).

thf(fun_fu923337204662071120nt_int_type,type,
    fun_fu923337204662071120nt_int: $tType ).

thf(fun_fu5689865433563736081nteger_type,type,
    fun_fu5689865433563736081nteger: $tType ).

thf(fun_se2951167709562549603nteger_type,type,
    fun_se2951167709562549603nteger: $tType ).

thf(fun_se8949688400205348287nteger_type,type,
    fun_se8949688400205348287nteger: $tType ).

thf(fun_se8450096479846816355et_nat_type,type,
    fun_se8450096479846816355et_nat: $tType ).

thf(fun_se3636548061058897599et_int_type,type,
    fun_se3636548061058897599et_int: $tType ).

thf(fun_se2042144505192658715et_int_type,type,
    fun_se2042144505192658715et_int: $tType ).

thf(fun_ra8505079968215247908at_rat_type,type,
    fun_ra8505079968215247908at_rat: $tType ).

thf(fun_Co6813818151677833714atural_type,type,
    fun_Co6813818151677833714atural: $tType ).

thf(fun_Co1981900195452921617nteger_type,type,
    fun_Co1981900195452921617nteger: $tType ).

thf(set_fu6863465268813640805nt_int_type,type,
    set_fu6863465268813640805nt_int: $tType ).

thf(fun_fu4509100218321815938_int_o_type,type,
    fun_fu4509100218321815938_int_o: $tType ).

thf(fun_fu3204908904631799856_rat_o_type,type,
    fun_fu3204908904631799856_rat_o: $tType ).

thf(fun_fu1837719853043986488_nat_o_type,type,
    fun_fu1837719853043986488_nat_o: $tType ).

thf(fun_fu1909670345266947804_int_o_type,type,
    fun_fu1909670345266947804_int_o: $tType ).

thf(fun_fu4523568072766896123eger_o_type,type,
    fun_fu4523568072766896123eger_o: $tType ).

thf(set_Pr3451248702717554689st_nat_type,type,
    set_Pr3451248702717554689st_nat: $tType ).

thf(fun_fu152868422178311599um_num_type,type,
    fun_fu152868422178311599um_num: $tType ).

thf(fun_fu1947565687807238081um_int_type,type,
    fun_fu1947565687807238081um_int: $tType ).

thf(fun_fu4719417816141531311on_num_type,type,
    fun_fu4719417816141531311on_num: $tType ).

thf(fun_fu7964671872712412353on_num_type,type,
    fun_fu7964671872712412353on_num: $tType ).

thf(fun_Pr5375745717004158586_nat_o_type,type,
    fun_Pr5375745717004158586_nat_o: $tType ).

thf(fun_fu9039538216874201369_o_rat_type,type,
    fun_fu9039538216874201369_o_rat: $tType ).

thf(fun_fu3581538110357139729_o_nat_type,type,
    fun_fu3581538110357139729_o_nat: $tType ).

thf(fun_fu9026017786105829997_o_int_type,type,
    fun_fu9026017786105829997_o_int: $tType ).

thf(fun_na2338080690716861136at_nat_type,type,
    fun_na2338080690716861136at_nat: $tType ).

thf(fun_he5369522480449343229at_nat_type,type,
    fun_he5369522480449343229at_nat: $tType ).

thf(set_Pr6558897299634722526_nat_o_type,type,
    set_Pr6558897299634722526_nat_o: $tType ).

thf(fun_op3323321805596408808on_num_type,type,
    fun_op3323321805596408808on_num: $tType ).

thf(fun_Pr7267779425873451369nt_int_type,type,
    fun_Pr7267779425873451369nt_int: $tType ).

thf(fun_na4138050610385705875at_nat_type,type,
    fun_na4138050610385705875at_nat: $tType ).

thf(fun_na8547874228452562927at_int_type,type,
    fun_na8547874228452562927at_int: $tType ).

thf(fun_na7356754204550075887nt_nat_type,type,
    fun_na7356754204550075887nt_nat: $tType ).

thf(fun_na7450791247808564371at_int_type,type,
    fun_na7450791247808564371at_int: $tType ).

thf(fun_in1696471567231710611nt_int_type,type,
    fun_in1696471567231710611nt_int: $tType ).

thf(set_se5158245632345848097at_nat_type,type,
    set_se5158245632345848097at_nat: $tType ).

thf(set_Pr5488025237498180813et_nat_type,type,
    set_Pr5488025237498180813et_nat: $tType ).

thf(set_Pr2522554150109002629et_int_type,type,
    set_Pr2522554150109002629et_int: $tType ).

thf(set_Pr7564037697178849041atural_type,type,
    set_Pr7564037697178849041atural: $tType ).

thf(set_Pr4811707699266497531nteger_type,type,
    set_Pr4811707699266497531nteger: $tType ).

thf(fun_se7504237348027150170_nat_o_type,type,
    fun_se7504237348027150170_nat_o: $tType ).

thf(fun_Pr3947133745332865710_nat_o_type,type,
    fun_Pr3947133745332865710_nat_o: $tType ).

thf(fun_Pr8359263388657976682ural_o_type,type,
    fun_Pr8359263388657976682ural_o: $tType ).

thf(fun_Pr7211993375558241536eger_o_type,type,
    fun_Pr7211993375558241536eger_o: $tType ).

thf(fun_Co1766037875893669450eger_o_type,type,
    fun_Co1766037875893669450eger_o: $tType ).

thf(option6357759511663192854e_term_type,type,
    option6357759511663192854e_term: $tType ).

thf(fun_Pr7397166214287566974on_num_type,type,
    fun_Pr7397166214287566974on_num: $tType ).

thf(set_Pr2929610433303031111_nat_o_type,type,
    set_Pr2929610433303031111_nat_o: $tType ).

thf(fun_fu2252611666013297880nteger_type,type,
    fun_fu2252611666013297880nteger: $tType ).

thf(fun_fu8261421317008872756nteger_type,type,
    fun_fu8261421317008872756nteger: $tType ).

thf(fun_fu3380082687118895412nteger_type,type,
    fun_fu3380082687118895412nteger: $tType ).

thf(fun_fu2995346897264222311t_assn_type,type,
    fun_fu2995346897264222311t_assn: $tType ).

thf(fun_fu3579422585476231989nt_rat_type,type,
    fun_fu3579422585476231989nt_rat: $tType ).

thf(fun_fu6568868615275847455t_assn_type,type,
    fun_fu6568868615275847455t_assn: $tType ).

thf(fun_fu5315010139097431512um_num_type,type,
    fun_fu5315010139097431512um_num: $tType ).

thf(fun_fu43082730658364980um_num_type,type,
    fun_fu43082730658364980um_num: $tType ).

thf(fun_se1218973151702474915nteger_type,type,
    fun_se1218973151702474915nteger: $tType ).

thf(fun_Pr6629464623532871604at_o_o_type,type,
    fun_Pr6629464623532871604at_o_o: $tType ).

thf(produc6653097349344004940it_nat_type,type,
    produc6653097349344004940it_nat: $tType ).

thf(fun_fu4201227159558561136_rat_o_type,type,
    fun_fu4201227159558561136_rat_o: $tType ).

thf(fun_fu7747438168682512768_nat_o_type,type,
    fun_fu7747438168682512768_nat_o: $tType ).

thf(fun_fu991806985645568200_int_o_type,type,
    fun_fu991806985645568200_int_o: $tType ).

thf(fun_fu5908277796454533188_int_o_type,type,
    fun_fu5908277796454533188_int_o: $tType ).

thf(fun_fu223923076992463612_num_o_type,type,
    fun_fu223923076992463612_num_o: $tType ).

thf(fun_fu5655606085901093248_rat_o_type,type,
    fun_fu5655606085901093248_rat_o: $tType ).

thf(fun_fu9201817095025044880_nat_o_type,type,
    fun_fu9201817095025044880_nat_o: $tType ).

thf(fun_fu2446185911988100312_int_o_type,type,
    fun_fu2446185911988100312_int_o: $tType ).

thf(fun_fu6636849678353221188_num_o_type,type,
    fun_fu6636849678353221188_num_o: $tType ).

thf(fun_fu6391371659531026648_nat_o_type,type,
    fun_fu6391371659531026648_nat_o: $tType ).

thf(fun_fu7417829167477406920_rat_o_type,type,
    fun_fu7417829167477406920_rat_o: $tType ).

thf(fun_fu1740668139746582744_nat_o_type,type,
    fun_fu1740668139746582744_nat_o: $tType ).

thf(fun_fu4208408993564413984_int_o_type,type,
    fun_fu4208408993564413984_int_o: $tType ).

thf(fun_se4239619783102168410eger_o_type,type,
    fun_se4239619783102168410eger_o: $tType ).

thf(fun_na927404270896789692_nat_o_type,type,
    fun_na927404270896789692_nat_o: $tType ).

thf(fun_fu8094397175230428611eger_o_type,type,
    fun_fu8094397175230428611eger_o: $tType ).

thf(fun_fu2786480252100984515nteger_type,type,
    fun_fu2786480252100984515nteger: $tType ).

thf(fun_fu5561970054461773155o_assn_type,type,
    fun_fu5561970054461773155o_assn: $tType ).

thf(fun_se2106923200977956867_nat_o_type,type,
    fun_se2106923200977956867_nat_o: $tType ).

thf(produc9082142974458947146at_num_type,type,
    produc9082142974458947146at_num: $tType ).

thf(produc7248412053542808358at_nat_type,type,
    produc7248412053542808358at_nat: $tType ).

thf(produc759720530913461378nt_int_type,type,
    produc759720530913461378nt_int: $tType ).

thf(fun_fu1622112948621879430al_o_o_type,type,
    fun_fu1622112948621879430al_o_o: $tType ).

thf(fun_fu4168831735773172575er_o_o_type,type,
    fun_fu4168831735773172575er_o_o: $tType ).

thf(fun_Pr292408699144966967t_unit_type,type,
    fun_Pr292408699144966967t_unit: $tType ).

thf(set_Pr5094982260447487303t_unit_type,type,
    set_Pr5094982260447487303t_unit: $tType ).

thf(set_mu2057375006010111271at_nat_type,type,
    set_mu2057375006010111271at_nat: $tType ).

thf(fun_fu2641566564518291801un_o_o_type,type,
    fun_fu2641566564518291801un_o_o: $tType ).

thf(fun_fu5915781709770235737un_o_o_type,type,
    fun_fu5915781709770235737un_o_o: $tType ).

thf(fun_Pr5924905948197006361rray_a_type,type,
    fun_Pr5924905948197006361rray_a: $tType ).

thf(fun_op4521932154746760340nteger_type,type,
    fun_op4521932154746760340nteger: $tType ).

thf(fun_ar1074044450438384043t_unit_type,type,
    fun_ar1074044450438384043t_unit: $tType ).

thf(fun_se4097146774670233028at_nat_type,type,
    fun_se4097146774670233028at_nat: $tType ).

thf(fun_se9142667792015812128at_int_type,type,
    fun_se9142667792015812128at_int: $tType ).

thf(fun_Pr9038118721296872730et_nat_type,type,
    fun_Pr9038118721296872730et_nat: $tType ).

thf(fun_Pr6548035576365145974et_int_type,type,
    fun_Pr6548035576365145974et_int: $tType ).

thf(fun_Pr6026251430685297nteger_type,type,
    fun_Pr6026251430685297nteger: $tType ).

thf(fun_Pr7395487658768111217er_nat_type,type,
    fun_Pr7395487658768111217er_nat: $tType ).

thf(fun_Pr3513738403344720850et_nat_type,type,
    fun_Pr3513738403344720850et_nat: $tType ).

thf(fun_Pr1023655258412994094et_int_type,type,
    fun_Pr1023655258412994094et_int: $tType ).

thf(fun_Pr907818707165963561er_int_type,type,
    fun_Pr907818707165963561er_int: $tType ).

thf(fun_Pr1791375292569619697at_nat_type,type,
    fun_Pr1791375292569619697at_nat: $tType ).

thf(fun_Pr9023817884608220585nt_int_type,type,
    fun_Pr9023817884608220585nt_int: $tType ).

thf(fun_op493924057549976310_num_o_type,type,
    fun_op493924057549976310_num_o: $tType ).

thf(fun_na7044673412300895210at_nat_type,type,
    fun_na7044673412300895210at_nat: $tType ).

thf(fun_na1596024190920976919nteger_type,type,
    fun_na1596024190920976919nteger: $tType ).

thf(fun_na7604833841916551795nteger_type,type,
    fun_na7604833841916551795nteger: $tType ).

thf(fun_na8176081009732395159er_nat_type,type,
    fun_na8176081009732395159er_nat: $tType ).

thf(fun_na5685997864800668403er_int_type,type,
    fun_na5685997864800668403er_int: $tType ).

thf(fun_in7446034528553779607er_int_type,type,
    fun_in7446034528553779607er_int: $tType ).

thf(fun_ar3891948820113774757rray_a_type,type,
    fun_ar3891948820113774757rray_a: $tType ).

thf(fun_Co4113693717567439989nt_int_type,type,
    fun_Co4113693717567439989nt_int: $tType ).

thf(set_fu360863049907232802nt_int_type,type,
    set_fu360863049907232802nt_int: $tType ).

thf(set_fu8487152106118010054nt_int_type,type,
    set_fu8487152106118010054nt_int: $tType ).

thf(fun_fu1115759055147092071_o_nat_type,type,
    fun_fu1115759055147092071_o_nat: $tType ).

thf(fun_fu6598048713889201561_int_o_type,type,
    fun_fu6598048713889201561_int_o: $tType ).

thf(fun_fu8565479202776651253_int_o_type,type,
    fun_fu8565479202776651253_int_o: $tType ).

thf(fun_Pr4738963024209204295_int_o_type,type,
    fun_Pr4738963024209204295_int_o: $tType ).

thf(fun_Pr7537129237977221859_rat_o_type,type,
    fun_Pr7537129237977221859_rat_o: $tType ).

thf(fun_na3970208099681795815_nat_o_type,type,
    fun_na3970208099681795815_nat_o: $tType ).

thf(fun_he5123621388056232515t_unit_type,type,
    fun_he5123621388056232515t_unit: $tType ).

thf(fun_he7369252872201260279rray_a_type,type,
    fun_he7369252872201260279rray_a: $tType ).

thf(set_op4508134149509766951at_nat_type,type,
    set_op4508134149509766951at_nat: $tType ).

thf(option8963830502488799655at_nat_type,type,
    option8963830502488799655at_nat: $tType ).

thf(fun_se704019859950278126r_assn_type,type,
    fun_se704019859950278126r_assn: $tType ).

thf(fun_se3395149180098744406et_nat_type,type,
    fun_se3395149180098744406et_nat: $tType ).

thf(fun_se7804972798165601458et_int_type,type,
    fun_se7804972798165601458et_int: $tType ).

thf(fun_se180586794239543474et_nat_type,type,
    fun_se180586794239543474et_nat: $tType ).

thf(fun_se4590410412306400526et_int_type,type,
    fun_se4590410412306400526et_int: $tType ).

thf(fun_se2974063760341720334et_int_type,type,
    fun_se2974063760341720334et_int: $tType ).

thf(fun_se8982873411337295210et_int_type,type,
    fun_se8982873411337295210et_int: $tType ).

thf(fun_Pr7036769738611282295at_nat_type,type,
    fun_Pr7036769738611282295at_nat: $tType ).

thf(fun_Pr6733608168372577327nt_int_type,type,
    fun_Pr6733608168372577327nt_int: $tType ).

thf(fun_Pr2481279687482350479t_unit_type,type,
    fun_Pr2481279687482350479t_unit: $tType ).

thf(fun_nu1287335591331657422nteger_type,type,
    fun_nu1287335591331657422nteger: $tType ).

thf(fun_na607345901702507418atural_type,type,
    fun_na607345901702507418atural: $tType ).

thf(fun_na7078387940644931716nteger_type,type,
    fun_na7078387940644931716nteger: $tType ).

thf(fun_Co740390889742897050atural_type,type,
    fun_Co740390889742897050atural: $tType ).

thf(fun_Co6226381647958292740nteger_type,type,
    fun_Co6226381647958292740nteger: $tType ).

thf(fun_Co8521658056209057742er_num_type,type,
    fun_Co8521658056209057742er_num: $tType ).

thf(fun_Co3583066429914935172er_nat_type,type,
    fun_Co3583066429914935172er_nat: $tType ).

thf(fun_Co1092983284983208416er_int_type,type,
    fun_Co1092983284983208416er_int: $tType ).

thf(fun_as4904527345752988583r_assn_type,type,
    fun_as4904527345752988583r_assn: $tType ).

thf(fun_fu4467818495196037351_nat_o_type,type,
    fun_fu4467818495196037351_nat_o: $tType ).

thf(fun_fu6344747128213397387_nat_o_type,type,
    fun_fu6344747128213397387_nat_o: $tType ).

thf(fun_fu5838931486547983824_nat_o_type,type,
    fun_fu5838931486547983824_nat_o: $tType ).

thf(fun_fu7898940055406642654nteger_type,type,
    fun_fu7898940055406642654nteger: $tType ).

thf(fun_fu3900186759307340847_int_o_type,type,
    fun_fu3900186759307340847_int_o: $tType ).

thf(fun_fu5777115392324700883_int_o_type,type,
    fun_fu5777115392324700883_int_o: $tType ).

thf(fun_fu5271299750659287320_int_o_type,type,
    fun_fu5271299750659287320_int_o: $tType ).

thf(fun_fu6361890901329191134nteger_type,type,
    fun_fu6361890901329191134nteger: $tType ).

thf(fun_fu5852520550942320402_int_o_type,type,
    fun_fu5852520550942320402_int_o: $tType ).

thf(fun_fu325614617715050166at_o_o_type,type,
    fun_fu325614617715050166at_o_o: $tType ).

thf(fun_fu1324968329616104722nt_o_o_type,type,
    fun_fu1324968329616104722nt_o_o: $tType ).

thf(fun_fu7060637683870700398_int_o_type,type,
    fun_fu7060637683870700398_int_o: $tType ).

thf(fun_fu2106003848923686156_nat_o_type,type,
    fun_fu2106003848923686156_nat_o: $tType ).

thf(fun_fu8716238685137547908_o_rat_type,type,
    fun_fu8716238685137547908_o_rat: $tType ).

thf(fun_se7316093745529328985et_nat_type,type,
    fun_se7316093745529328985et_nat: $tType ).

thf(fun_Co8029881127924365703nteger_type,type,
    fun_Co8029881127924365703nteger: $tType ).

thf(option8886115935005447431nteger_type,type,
    option8886115935005447431nteger: $tType ).

thf(fun_as4019953064511417593t_assn_type,type,
    fun_as4019953064511417593t_assn: $tType ).

thf(set_Pr698032948827214833st_nat_type,type,
    set_Pr698032948827214833st_nat: $tType ).

thf(set_Pr7549493975000385137at_nat_type,type,
    set_Pr7549493975000385137at_nat: $tType ).

thf(produc652263959640188542_nat_o_type,type,
    produc652263959640188542_nat_o: $tType ).

thf(fun_fu5368785673109833417_nat_o_type,type,
    fun_fu5368785673109833417_nat_o: $tType ).

thf(fun_Pr961374740995693450_nat_o_type,type,
    fun_Pr961374740995693450_nat_o: $tType ).

thf(fun_Pr7575312783043447050_nat_o_type,type,
    fun_Pr7575312783043447050_nat_o: $tType ).

thf(fun_op9036024853803066045_nat_o_type,type,
    fun_op9036024853803066045_nat_o: $tType ).

thf(fun_li1191372448985611379st_nat_type,type,
    fun_li1191372448985611379st_nat: $tType ).

thf(fun_li1025265955262268170_nat_o_type,type,
    fun_li1025265955262268170_nat_o: $tType ).

thf(set_se7855581050983116737at_nat_type,type,
    set_se7855581050983116737at_nat: $tType ).

thf(set_Pr2406931829603198446nteger_type,type,
    set_Pr2406931829603198446nteger: $tType ).

thf(set_Pr8415741480598773322nteger_type,type,
    set_Pr8415741480598773322nteger: $tType ).

thf(set_Pr8986988648414616686er_nat_type,type,
    set_Pr8986988648414616686er_nat: $tType ).

thf(set_Pr6496905503482889930er_int_type,type,
    set_Pr6496905503482889930er_int: $tType ).

thf(produc7819656566062154093et_nat_type,type,
    produc7819656566062154093et_nat: $tType ).

thf(produc2115011035271226405et_int_type,type,
    produc2115011035271226405et_int: $tType ).

thf(produc7822875418678951345atural_type,type,
    produc7822875418678951345atural: $tType ).

thf(produc8923325533196201883nteger_type,type,
    produc8923325533196201883nteger: $tType ).

thf(fun_se1018900654481025269at_int_type,type,
    fun_se1018900654481025269at_int: $tType ).

thf(fun_se4782206882984618170_nat_o_type,type,
    fun_se4782206882984618170_nat_o: $tType ).

thf(fun_Pr8467005832278515962_set_o_type,type,
    fun_Pr8467005832278515962_set_o: $tType ).

thf(fun_Pr5150627949553849410_set_o_type,type,
    fun_Pr5150627949553849410_set_o: $tType ).

thf(set_fu8838435424971791696_nat_o_type,type,
    set_fu8838435424971791696_nat_o: $tType ).

thf(fun_fu6891447142836604759at_o_o_type,type,
    fun_fu6891447142836604759at_o_o: $tType ).

thf(set_Pr4577759397028426247_set_o_type,type,
    set_Pr4577759397028426247_set_o: $tType ).

thf(produc7704145150520151143_nat_o_type,type,
    produc7704145150520151143_nat_o: $tType ).

thf(fun_fu8155524643419131615um_num_type,type,
    fun_fu8155524643419131615um_num: $tType ).

thf(fun_fu726849872193282289um_int_type,type,
    fun_fu726849872193282289um_int: $tType ).

thf(fun_fu5322398707847370225um_num_type,type,
    fun_fu5322398707847370225um_num: $tType ).

thf(fun_fu7117095973476296707um_int_type,type,
    fun_fu7117095973476296707um_int: $tType ).

thf(fun_fu7588784024441849949at_nat_type,type,
    fun_fu7588784024441849949at_nat: $tType ).

thf(fun_fu5490925188574218499nt_num_type,type,
    fun_fu5490925188574218499nt_num: $tType ).

thf(fun_fu8328862064278946247at_rat_type,type,
    fun_fu8328862064278946247at_rat: $tType ).

thf(fun_fu7002938529518989751at_nat_type,type,
    fun_fu7002938529518989751at_nat: $tType ).

thf(fun_fu4905079693651358301nt_num_type,type,
    fun_fu4905079693651358301nt_num: $tType ).

thf(fun_fu8464300013002972271at_int_type,type,
    fun_fu8464300013002972271at_int: $tType ).

thf(fun_fu1008360527747082367nt_rat_type,type,
    fun_fu1008360527747082367nt_rat: $tType ).

thf(fun_fu4621028619281248441nt_num_type,type,
    fun_fu4621028619281248441nt_num: $tType ).

thf(fun_fu8905809029841901679nt_nat_type,type,
    fun_fu8905809029841901679nt_nat: $tType ).

thf(fun_fu1143798476471108391nt_int_type,type,
    fun_fu1143798476471108391nt_int: $tType ).

thf(fun_se8304080770522320754nteger_type,type,
    fun_se8304080770522320754nteger: $tType ).

thf(fun_se1173871648619632798er_rat_type,type,
    fun_se1173871648619632798er_rat: $tType ).

thf(fun_se504249187503832818er_int_type,type,
    fun_se504249187503832818er_int: $tType ).

thf(fun_se3362872515591026879et_nat_type,type,
    fun_se3362872515591026879et_nat: $tType ).

thf(fun_se3773019727686582893nteger_type,type,
    fun_se3773019727686582893nteger: $tType ).

thf(fun_ra3995598502166916815at_rat_type,type,
    fun_ra3995598502166916815at_rat: $tType ).

thf(fun_ra5513060666784058567at_rat_type,type,
    fun_ra5513060666784058567at_rat: $tType ).

thf(fun_Pr8303579546892975945t_unit_type,type,
    fun_Pr8303579546892975945t_unit: $tType ).

thf(fun_na1148497095348402375at_rat_type,type,
    fun_na1148497095348402375at_rat: $tType ).

thf(fun_na3244735409550470327at_nat_type,type,
    fun_na3244735409550470327at_nat: $tType ).

thf(fun_na7654559027617327379at_int_type,type,
    fun_na7654559027617327379at_int: $tType ).

thf(fun_na2382631619178260847at_int_type,type,
    fun_na2382631619178260847at_int: $tType ).

thf(fun_in6793278964266839919at_int_type,type,
    fun_in6793278964266839919at_int: $tType ).

thf(fun_Co744628173305925485nteger_type,type,
    fun_Co744628173305925485nteger: $tType ).

thf(fun_as3983628580203722482n_assn_type,type,
    fun_as3983628580203722482n_assn: $tType ).

thf(set_fu5818728815147633517nteger_type,type,
    set_fu5818728815147633517nteger: $tType ).

thf(set_Pr1763845938948868674it_nat_type,type,
    set_Pr1763845938948868674it_nat: $tType ).

thf(set_Pr8497134830871917726it_int_type,type,
    set_Pr8497134830871917726it_int: $tType ).

thf(set_Pr4334478416066269672t_unit_type,type,
    set_Pr4334478416066269672t_unit: $tType ).

thf(set_Pr5889264611543340172t_unit_type,type,
    set_Pr5889264611543340172t_unit: $tType ).

thf(fun_fu1116345184836134341_nat_o_type,type,
    fun_fu1116345184836134341_nat_o: $tType ).

thf(fun_fu2792963925203051945t_assn_type,type,
    fun_fu2792963925203051945t_assn: $tType ).

thf(fun_fu2934462529731303693_int_o_type,type,
    fun_fu2934462529731303693_int_o: $tType ).

thf(fun_fu2048648494261043369t_assn_type,type,
    fun_fu2048648494261043369t_assn: $tType ).

thf(fun_fu2916398056546941156ural_o_type,type,
    fun_fu2916398056546941156ural_o: $tType ).

thf(fun_fu1769128043447206010eger_o_type,type,
    fun_fu1769128043447206010eger_o: $tType ).

thf(fun_se2170385732985038782_nat_o_type,type,
    fun_se2170385732985038782_nat_o: $tType ).

thf(fun_se5245582867311637764et_nat_type,type,
    fun_se5245582867311637764et_nat: $tType ).

thf(fun_se2051630309975736070_int_o_type,type,
    fun_se2051630309975736070_int_o: $tType ).

thf(fun_se241328533291454980et_int_type,type,
    fun_se241328533291454980et_int: $tType ).

thf(fun_Co7302518231560758906ural_o_type,type,
    fun_Co7302518231560758906ural_o: $tType ).

thf(fun_Co2081214437782444048eger_o_type,type,
    fun_Co2081214437782444048eger_o: $tType ).

thf(fun_fu8708304106554588451_nat_o_type,type,
    fun_fu8708304106554588451_nat_o: $tType ).

thf(fun_fu2969420921405070251ural_o_type,type,
    fun_fu2969420921405070251ural_o: $tType ).

thf(fun_fu7671276271812522531_int_o_type,type,
    fun_fu7671276271812522531_int_o: $tType ).

thf(fun_fu8256284588060503314eger_o_type,type,
    fun_fu8256284588060503314eger_o: $tType ).

thf(fun_fu4803769369665013091_o_rat_type,type,
    fun_fu4803769369665013091_o_rat: $tType ).

thf(fun_fu8843157277860572003_o_nat_type,type,
    fun_fu8843157277860572003_o_nat: $tType ).

thf(fun_fu704708528062463619o_assn_type,type,
    fun_fu704708528062463619o_assn: $tType ).

thf(fun_nu1049378303802735384on_num_type,type,
    fun_nu1049378303802735384on_num: $tType ).

thf(fun_na7595719129879163854on_num_type,type,
    fun_na7595719129879163854on_num: $tType ).

thf(fun_fu182496756620222510at_o_o_type,type,
    fun_fu182496756620222510at_o_o: $tType ).

thf(fun_fu1181850468521277066nt_o_o_type,type,
    fun_fu1181850468521277066nt_o_o: $tType ).

thf(fun_fu4016735857504249042at_o_o_type,type,
    fun_fu4016735857504249042at_o_o: $tType ).

thf(fun_fu5016089569405303598nt_o_o_type,type,
    fun_fu5016089569405303598nt_o_o: $tType ).

thf(fun_fu7564235448449272366at_o_o_type,type,
    fun_fu7564235448449272366at_o_o: $tType ).

thf(fun_fu6971708032831053102nt_o_o_type,type,
    fun_fu6971708032831053102nt_o_o: $tType ).

thf(fun_se1823139391991869964it_int_type,type,
    fun_se1823139391991869964it_int: $tType ).

thf(fun_na8669532458821385046t_unit_type,type,
    fun_na8669532458821385046t_unit: $tType ).

thf(multis2468970476368604999at_nat_type,type,
    multis2468970476368604999at_nat: $tType ).

thf(fun_op8989173174992673105on_num_type,type,
    fun_op8989173174992673105on_num: $tType ).

thf(fun_op6210678640266353415on_num_type,type,
    fun_op6210678640266353415on_num: $tType ).

thf(fun_op1272087013972230845on_nat_type,type,
    fun_op1272087013972230845on_nat: $tType ).

thf(fun_op2398388785115040099on_num_type,type,
    fun_op2398388785115040099on_num: $tType ).

thf(fun_op6683169195675693337on_nat_type,type,
    fun_op6683169195675693337on_nat: $tType ).

thf(fun_op4193086050743966581on_int_type,type,
    fun_op4193086050743966581on_int: $tType ).

thf(fun_ra4503298312962071866nt_int_type,type,
    fun_ra4503298312962071866nt_int: $tType ).

thf(fun_Pr3269564255357226306um_num_type,type,
    fun_Pr3269564255357226306um_num: $tType ).

thf(fun_Pr4620512490437729710um_nat_type,type,
    fun_Pr4620512490437729710um_nat: $tType ).

thf(fun_Pr8317260874932935276at_rat_type,type,
    fun_Pr8317260874932935276at_rat: $tType ).

thf(fun_Pr2602117396471556196at_nat_type,type,
    fun_Pr2602117396471556196at_nat: $tType ).

thf(fun_Pr7647638413817135296at_int_type,type,
    fun_Pr7647638413817135296at_int: $tType ).

thf(fun_Pr4789038971164577984nt_nat_type,type,
    fun_Pr4789038971164577984nt_nat: $tType ).

thf(fun_Pr611187951655381276nt_int_type,type,
    fun_Pr611187951655381276nt_int: $tType ).

thf(fun_Pr814315031165377638um_int_type,type,
    fun_Pr814315031165377638um_int: $tType ).

thf(fun_Pr2973770956708400832at_nat_type,type,
    fun_Pr2973770956708400832at_nat: $tType ).

thf(fun_Pr8019291974053979932at_int_type,type,
    fun_Pr8019291974053979932at_int: $tType ).

thf(fun_Pr1652463973008025892nt_rat_type,type,
    fun_Pr1652463973008025892nt_rat: $tType ).

thf(fun_Pr982841511892225912nt_int_type,type,
    fun_Pr982841511892225912nt_int: $tType ).

thf(fun_nu5148503272595741012um_num_type,type,
    fun_nu5148503272595741012um_num: $tType ).

thf(fun_na1476630412504255114at_nat_type,type,
    fun_na1476630412504255114at_nat: $tType ).

thf(fun_na8209919304427304166at_int_type,type,
    fun_na8209919304427304166at_int: $tType ).

thf(fun_na3663551987197276902nt_nat_type,type,
    fun_na3663551987197276902nt_nat: $tType ).

thf(fun_na1173468842265550146nt_int_type,type,
    fun_na1173468842265550146nt_int: $tType ).

thf(fun_in4514472496968388910at_nat_type,type,
    fun_in4514472496968388910at_nat: $tType ).

thf(fun_in2024389352036662154at_int_type,type,
    fun_in2024389352036662154at_int: $tType ).

thf(fun_in4211310926729683942nt_int_type,type,
    fun_in4211310926729683942nt_int: $tType ).

thf(fun_Pr3013102738158121955t_unit_type,type,
    fun_Pr3013102738158121955t_unit: $tType ).

thf(fun_na819858167508000762st_nat_type,type,
    fun_na819858167508000762st_nat: $tType ).

thf(set_set_set_list_nat_type,type,
    set_set_set_list_nat: $tType ).

thf(fun_se5048694460222551717_nat_o_type,type,
    fun_se5048694460222551717_nat_o: $tType ).

thf(fun_Pr1520749766685617582unit_o_type,type,
    fun_Pr1520749766685617582unit_o: $tType ).

thf(option4927543243414619207at_nat_type,type,
    option4927543243414619207at_nat: $tType ).

thf(option4624381673175914239nt_int_type,type,
    option4624381673175914239nt_int: $tType ).

thf(fun_set_set_int_assn_type,type,
    fun_set_set_int_assn: $tType ).

thf(fun_se244736854054144952r_assn_type,type,
    fun_se244736854054144952r_assn: $tType ).

thf(fun_ra3321464020636160263er_rat_type,type,
    fun_ra3321464020636160263er_rat: $tType ).

thf(fun_nu2537414170016844299nteger_type,type,
    fun_nu2537414170016844299nteger: $tType ).

thf(fun_na6128946301132549280et_nat_type,type,
    fun_na6128946301132549280et_nat: $tType ).

thf(fun_na3365689438791330114atural_type,type,
    fun_na3365689438791330114atural: $tType ).

thf(fun_na8135612474337863287nteger_type,type,
    fun_na8135612474337863287nteger: $tType ).

thf(fun_na2454419004871237530n_assn_type,type,
    fun_na2454419004871237530n_assn: $tType ).

thf(fun_as8240436605320707994t_assn_type,type,
    fun_as8240436605320707994t_assn: $tType ).

thf(fun_as3432858861813084150t_assn_type,type,
    fun_as3432858861813084150t_assn: $tType ).

thf(set_se8531188866349061887nteger_type,type,
    set_se8531188866349061887nteger: $tType ).

thf(fun_fu7145897819039579925_nat_o_type,type,
    fun_fu7145897819039579925_nat_o: $tType ).

thf(fun_fu5477517762487726877_nat_o_type,type,
    fun_fu5477517762487726877_nat_o: $tType ).

thf(fun_fu3162257917499486297at_rat_type,type,
    fun_fu3162257917499486297at_rat: $tType ).

thf(fun_fu15710647883683081nt_int_type,type,
    fun_fu15710647883683081nt_int: $tType ).

thf(fun_fu8658704570366206279_rat_o_type,type,
    fun_fu8658704570366206279_rat_o: $tType ).

thf(fun_fu7363466011001354227_int_o_type,type,
    fun_fu7363466011001354227_int_o: $tType ).

thf(fun_fu3473604023002724957_int_o_type,type,
    fun_fu3473604023002724957_int_o: $tType ).

thf(fun_fu6779973503720134245_nat_o_type,type,
    fun_fu6779973503720134245_nat_o: $tType ).

thf(fun_fu4534828536049688329_int_o_type,type,
    fun_fu4534828536049688329_int_o: $tType ).

thf(fun_fu7811933856372049837nt_int_type,type,
    fun_fu7811933856372049837nt_int: $tType ).

thf(fun_se1103039064484435816eger_o_type,type,
    fun_se1103039064484435816eger_o: $tType ).

thf(fun_se5062308858318814664nteger_type,type,
    fun_se5062308858318814664nteger: $tType ).

thf(fun_na7928631014926962227_nat_o_type,type,
    fun_na7928631014926962227_nat_o: $tType ).

thf(fun_Co4819230592921789445assn_o_type,type,
    fun_Co4819230592921789445assn_o: $tType ).

thf(fun_as7521517929205406341eger_o_type,type,
    fun_as7521517929205406341eger_o: $tType ).

thf(fun_se5315385049746747468_set_o_type,type,
    fun_se5315385049746747468_set_o: $tType ).

thf(fun_se7711175411341617392_set_o_type,type,
    fun_se7711175411341617392_set_o: $tType ).

thf(fun_na896109329399166627et_nat_type,type,
    fun_na896109329399166627et_nat: $tType ).

thf(fun_in2104226462327546623et_nat_type,type,
    fun_in2104226462327546623et_nat: $tType ).

thf(fun_assn_option_assn_type,type,
    fun_assn_option_assn: $tType ).

thf(fun_fu4049601875756261639un_o_o_type,type,
    fun_fu4049601875756261639un_o_o: $tType ).

thf(fun_fu8465396169103413603un_o_o_type,type,
    fun_fu8465396169103413603un_o_o: $tType ).

thf(fun_fu3819205551299168222un_o_o_type,type,
    fun_fu3819205551299168222un_o_o: $tType ).

thf(fun_fu7181763470137098718nteger_type,type,
    fun_fu7181763470137098718nteger: $tType ).

thf(fun_ra5613769993463817465it_rat_type,type,
    fun_ra5613769993463817465it_rat: $tType ).

thf(set_se7118615804146677933t_unit_type,type,
    set_se7118615804146677933t_unit: $tType ).

thf(fun_se2288280263375636942unit_o_type,type,
    fun_se2288280263375636942unit_o: $tType ).

thf(fun_he8413527710729349838unit_o_type,type,
    fun_he8413527710729349838unit_o: $tType ).

thf(fun_Pr792663941044724234on_num_type,type,
    fun_Pr792663941044724234on_num: $tType ).

thf(fun_na5635918068280204892t_unit_type,type,
    fun_na5635918068280204892t_unit: $tType ).

thf(fun_in5873495209930779904t_unit_type,type,
    fun_in5873495209930779904t_unit: $tType ).

thf(set_Pr6200539531224447659at_num_type,type,
    set_Pr6200539531224447659at_num: $tType ).

thf(set_Pr1261947904930325089at_nat_type,type,
    set_Pr1261947904930325089at_nat: $tType ).

thf(set_Pr7995236796853374141at_int_type,type,
    set_Pr7995236796853374141at_int: $tType ).

thf(set_Pr8387461105917469447nt_num_type,type,
    set_Pr8387461105917469447nt_num: $tType ).

thf(set_Pr3448869479623346877nt_nat_type,type,
    set_Pr3448869479623346877nt_nat: $tType ).

thf(set_Pr958786334691620121nt_int_type,type,
    set_Pr958786334691620121nt_int: $tType ).

thf(produc2591615631378489102nteger_type,type,
    produc2591615631378489102nteger: $tType ).

thf(produc2963269191615333738nteger_type,type,
    produc2963269191615333738nteger: $tType ).

thf(produc7142191362829087448er_num_type,type,
    produc7142191362829087448er_num: $tType ).

thf(produc6433947425880249742er_nat_type,type,
    produc6433947425880249742er_nat: $tType ).

thf(produc2256096406371053034er_int_type,type,
    produc2256096406371053034er_int: $tType ).

thf(fun_Pr4796943543331071514_nat_o_type,type,
    fun_Pr4796943543331071514_nat_o: $tType ).

thf(fun_Pr103879662602641546_o_nat_type,type,
    fun_Pr103879662602641546_o_nat: $tType ).

thf(fun_Pr3238374608701176162_int_o_type,type,
    fun_Pr3238374608701176162_int_o: $tType ).

thf(fun_Pr5835976712988771210_o_int_type,type,
    fun_Pr5835976712988771210_o_int: $tType ).

thf(fun_Pr5585980272307166948at_nat_type,type,
    fun_Pr5585980272307166948at_nat: $tType ).

thf(fun_Pr3595050827490992028nt_int_type,type,
    fun_Pr3595050827490992028nt_int: $tType ).

thf(fun_nat_set_list_nat_type,type,
    fun_nat_set_list_nat: $tType ).

thf(fun_list_nat_set_nat_type,type,
    fun_list_nat_set_nat: $tType ).

thf(fun_na7234455742697417626_nat_o_type,type,
    fun_na7234455742697417626_nat_o: $tType ).

thf(fun_li2421049240157457050_nat_o_type,type,
    fun_li2421049240157457050_nat_o: $tType ).

thf(produc7369051934464679207_set_o_type,type,
    produc7369051934464679207_set_o: $tType ).

thf(fun_set_set_nat_int_type,type,
    fun_set_set_nat_int: $tType ).

thf(fun_set_set_int_rat_type,type,
    fun_set_set_int_rat: $tType ).

thf(fun_set_set_int_int_type,type,
    fun_set_set_int_int: $tType ).

thf(fun_set_num_set_num_type,type,
    fun_set_num_set_num: $tType ).

thf(fun_set_nat_set_nat_type,type,
    fun_set_nat_set_nat: $tType ).

thf(fun_set_int_set_int_type,type,
    fun_set_int_set_int: $tType ).

thf(fun_se4372286887653997756nteger_type,type,
    fun_se4372286887653997756nteger: $tType ).

thf(fun_se2244710085602452072er_rat_type,type,
    fun_se2244710085602452072er_rat: $tType ).

thf(fun_na9118744110877893344nteger_type,type,
    fun_na9118744110877893344nteger: $tType ).

thf(fun_in6808926178784942396nteger_type,type,
    fun_in6808926178784942396nteger: $tType ).

thf(fun_Co7398788559141407565atural_type,type,
    fun_Co7398788559141407565atural: $tType ).

thf(fun_Co2940338738630218498nteger_type,type,
    fun_Co2940338738630218498nteger: $tType ).

thf(fun_Co8307959106670069728et_nat_type,type,
    fun_Co8307959106670069728et_nat: $tType ).

thf(fun_Co5817875961738342972et_int_type,type,
    fun_Co5817875961738342972et_int: $tType ).

thf(fun_Co3734316457315071362atural_type,type,
    fun_Co3734316457315071362atural: $tType ).

thf(fun_Co8499238673658658103nteger_type,type,
    fun_Co8499238673658658103nteger: $tType ).

thf(fun_fu3961712701602788733eger_o_type,type,
    fun_fu3961712701602788733eger_o: $tType ).

thf(fun_fu2893655071357150791eger_o_type,type,
    fun_fu2893655071357150791eger_o: $tType ).

thf(fun_set_set_o_assn_type,type,
    fun_set_set_o_assn: $tType ).

thf(fun_se382663106265794036_nat_o_type,type,
    fun_se382663106265794036_nat_o: $tType ).

thf(fun_se867122708194164540_int_o_type,type,
    fun_se867122708194164540_int_o: $tType ).

thf(fun_ra6546579167043500746ural_o_type,type,
    fun_ra6546579167043500746ural_o: $tType ).

thf(fun_ra1401953663915778005eger_o_type,type,
    fun_ra1401953663915778005eger_o: $tType ).

thf(fun_nu5413996832991386387eger_o_type,type,
    fun_nu5413996832991386387eger_o: $tType ).

thf(fun_na2240068485812228818ural_o_type,type,
    fun_na2240068485812228818ural_o: $tType ).

thf(fun_na6318815019539281885eger_o_type,type,
    fun_na6318815019539281885eger_o: $tType ).

thf(fun_in812919657445819766ural_o_type,type,
    fun_in812919657445819766ural_o: $tType ).

thf(fun_in4891666191172872833eger_o_type,type,
    fun_in4891666191172872833eger_o: $tType ).

thf(fun_Co196715998180962002_nat_o_type,type,
    fun_Co196715998180962002_nat_o: $tType ).

thf(fun_Co625613742390903637_rat_o_type,type,
    fun_Co625613742390903637_rat_o: $tType ).

thf(fun_Co2133228800495250323_num_o_type,type,
    fun_Co2133228800495250323_num_o: $tType ).

thf(fun_Co1375048237525739357_nat_o_type,type,
    fun_Co1375048237525739357_nat_o: $tType ).

thf(fun_Co8353275306710069249_int_o_type,type,
    fun_Co8353275306710069249_int_o: $tType ).

thf(fun_assn_fun_assn_o_type,type,
    fun_assn_fun_assn_o: $tType ).

thf(fun_assn_fun_o_assn_type,type,
    fun_assn_fun_o_assn: $tType ).

thf(set_fu7727944524835118346_nat_o_type,type,
    set_fu7727944524835118346_nat_o: $tType ).

thf(fun_fu4001317426178549763_nat_o_type,type,
    fun_fu4001317426178549763_nat_o: $tType ).

thf(fun_fu1756172458508103847_int_o_type,type,
    fun_fu1756172458508103847_int_o: $tType ).

thf(fun_fu4354239228518319373at_o_o_type,type,
    fun_fu4354239228518319373at_o_o: $tType ).

thf(fun_fu5353592940419373929nt_o_o_type,type,
    fun_fu5353592940419373929nt_o_o: $tType ).

thf(fun_fu6128684156180612191_nat_o_type,type,
    fun_fu6128684156180612191_nat_o: $tType ).

thf(fun_fu3883539188510166275_int_o_type,type,
    fun_fu3883539188510166275_int_o: $tType ).

thf(fun_fu1989461620956114563_o_rat_type,type,
    fun_fu1989461620956114563_o_rat: $tType ).

thf(fun_fu6701067901881939075_o_nat_type,type,
    fun_fu6701067901881939075_o_nat: $tType ).

thf(fun_fu6940589326549028739_o_int_type,type,
    fun_fu6940589326549028739_o_int: $tType ).

thf(set_option_set_nat_type,type,
    set_option_set_nat: $tType ).

thf(set_op687863988967635939nteger_type,type,
    set_op687863988967635939nteger: $tType ).

thf(fun_fu3143923321121214633un_o_o_type,type,
    fun_fu3143923321121214633un_o_o: $tType ).

thf(fun_fu7714003655882793385o_assn_type,type,
    fun_fu7714003655882793385o_assn: $tType ).

thf(fun_se3315603611433934638_set_o_type,type,
    fun_se3315603611433934638_set_o: $tType ).

thf(fun_Pr1628945989756059814et_nat_type,type,
    fun_Pr1628945989756059814et_nat: $tType ).

thf(fun_Pr8362234881679108866et_int_type,type,
    fun_Pr8362234881679108866et_int: $tType ).

thf(fun_Pr6278675377255837256atural_type,type,
    fun_Pr6278675377255837256atural: $tType ).

thf(fun_Pr1820225556744648189nteger_type,type,
    fun_Pr1820225556744648189nteger: $tType ).

thf(fun_na896991816813928310t_unit_type,type,
    fun_na896991816813928310t_unit: $tType ).

thf(fun_in4731230917697954842t_unit_type,type,
    fun_in4731230917697954842t_unit: $tType ).

thf(fun_Co1365676809456677961t_unit_type,type,
    fun_Co1365676809456677961t_unit: $tType ).

thf(fun_o_option_set_nat_type,type,
    fun_o_option_set_nat: $tType ).

thf(fun_fu5370137289309429475un_o_o_type,type,
    fun_fu5370137289309429475un_o_o: $tType ).

thf(fun_na5971062356810558811unit_o_type,type,
    fun_na5971062356810558811unit_o: $tType ).

thf(fun_in8984369272479023031unit_o_type,type,
    fun_in8984369272479023031unit_o: $tType ).

thf(set_op3165557761946182707t_unit_type,type,
    set_op3165557761946182707t_unit: $tType ).

thf(option8137458692691377843t_unit_type,type,
    option8137458692691377843t_unit: $tType ).

thf(fun_Pr2191293291710260995t_unit_type,type,
    fun_Pr2191293291710260995t_unit: $tType ).

thf(fun_op5853259939270031811tion_o_type,type,
    fun_op5853259939270031811tion_o: $tType ).

thf(fun_o_6261137236491177342t_unit_type,type,
    fun_o_6261137236491177342t_unit: $tType ).

thf(set_set_list_nat_type,type,
    set_set_list_nat: $tType ).

thf(set_Pr3149072824959771635_nat_o_type,type,
    set_Pr3149072824959771635_nat_o: $tType ).

thf(set_Pr903927857289325719_int_o_type,type,
    set_Pr903927857289325719_int_o: $tType ).

thf(set_Pr7040061329075590551_o_num_type,type,
    set_Pr7040061329075590551_o_num: $tType ).

thf(set_Pr2101469702781467981_o_nat_type,type,
    set_Pr2101469702781467981_o_nat: $tType ).

thf(set_Pr8834758594704517033_o_int_type,type,
    set_Pr8834758594704517033_o_int: $tType ).

thf(produc6271795597528267376eger_o_type,type,
    produc6271795597528267376eger_o: $tType ).

thf(fun_Pr2976697613021001844at_o_o_type,type,
    fun_Pr2976697613021001844at_o_o: $tType ).

thf(fun_Pr1059884994059025616nt_o_o_type,type,
    fun_Pr1059884994059025616nt_o_o: $tType ).

thf(fun_Pr4362196099282670544_num_o_type,type,
    fun_Pr4362196099282670544_num_o: $tType ).

thf(fun_Pr3604015536313159578_nat_o_type,type,
    fun_Pr3604015536313159578_nat_o: $tType ).

thf(fun_Pr1358870568642713662_int_o_type,type,
    fun_Pr1358870568642713662_int_o: $tType ).

thf(fun_set_int_assn_type,type,
    fun_set_int_assn: $tType ).

thf(fun_rat_fun_rat_rat_type,type,
    fun_rat_fun_rat_rat: $tType ).

thf(fun_rat_fun_nat_rat_type,type,
    fun_rat_fun_nat_rat: $tType ).

thf(fun_rat_fun_int_rat_type,type,
    fun_rat_fun_int_rat: $tType ).

thf(fun_num_fun_num_num_type,type,
    fun_num_fun_num_num: $tType ).

thf(fun_num_fun_num_int_type,type,
    fun_num_fun_num_int: $tType ).

thf(fun_nat_fun_rat_rat_type,type,
    fun_nat_fun_rat_rat: $tType ).

thf(fun_nat_fun_nat_rat_type,type,
    fun_nat_fun_nat_rat: $tType ).

thf(fun_nat_fun_nat_nat_type,type,
    fun_nat_fun_nat_nat: $tType ).

thf(fun_nat_fun_nat_int_type,type,
    fun_nat_fun_nat_int: $tType ).

thf(fun_nat_fun_int_int_type,type,
    fun_nat_fun_int_int: $tType ).

thf(fun_int_fun_nat_int_type,type,
    fun_int_fun_nat_int: $tType ).

thf(fun_int_fun_int_rat_type,type,
    fun_int_fun_int_rat: $tType ).

thf(fun_int_fun_int_int_type,type,
    fun_int_fun_int_int: $tType ).

thf(fun_array_a_array_a_type,type,
    fun_array_a_array_a: $tType ).

thf(fun_Co4490034186337852034r_assn_type,type,
    fun_Co4490034186337852034r_assn: $tType ).

thf(set_set_set_nat_type,type,
    set_set_set_nat: $tType ).

thf(set_set_set_int_type,type,
    set_set_set_int: $tType ).

thf(set_set_Code_integer_type,type,
    set_set_Code_integer: $tType ).

thf(heap_T5738788834812785303t_unit_type,type,
    heap_T5738788834812785303t_unit: $tType ).

thf(fun_set_set_nat_o_type,type,
    fun_set_set_nat_o: $tType ).

thf(fun_set_set_int_o_type,type,
    fun_set_set_int_o: $tType ).

thf(fun_set_set_o_rat_type,type,
    fun_set_set_o_rat: $tType ).

thf(fun_set_set_o_nat_type,type,
    fun_set_set_o_nat: $tType ).

thf(fun_se7289222521248229150eger_o_type,type,
    fun_se7289222521248229150eger_o: $tType ).

thf(fun_se937664112047466216nteger_type,type,
    fun_se937664112047466216nteger: $tType ).

thf(fun_assn_fun_rat_o_type,type,
    fun_assn_fun_rat_o: $tType ).

thf(fun_assn_fun_nat_o_type,type,
    fun_assn_fun_nat_o: $tType ).

thf(fun_assn_fun_int_o_type,type,
    fun_assn_fun_int_o: $tType ).

thf(fun_o_5240169576699714110nteger_type,type,
    fun_o_5240169576699714110nteger: $tType ).

thf(heap_T6362127782908069795rray_a_type,type,
    heap_T6362127782908069795rray_a: $tType ).

thf(fun_option_num_num_type,type,
    fun_option_num_num: $tType ).

thf(fun_option_num_nat_type,type,
    fun_option_num_nat: $tType ).

thf(fun_option_num_int_type,type,
    fun_option_num_int: $tType ).

thf(fun_option_nat_nat_type,type,
    fun_option_nat_nat: $tType ).

thf(fun_option_int_int_type,type,
    fun_option_int_int: $tType ).

thf(fun_num_option_num_type,type,
    fun_num_option_num: $tType ).

thf(fun_nat_option_num_type,type,
    fun_nat_option_num: $tType ).

thf(fun_nat_option_nat_type,type,
    fun_nat_option_nat: $tType ).

thf(fun_int_option_num_type,type,
    fun_int_option_num: $tType ).

thf(fun_int_option_int_type,type,
    fun_int_option_int: $tType ).

thf(fun_fu6337961365400742745un_o_o_type,type,
    fun_fu6337961365400742745un_o_o: $tType ).

thf(fun_fu6781074197733401937un_o_o_type,type,
    fun_fu6781074197733401937un_o_o: $tType ).

thf(fun_fu830079035465870425_o_rat_type,type,
    fun_fu830079035465870425_o_rat: $tType ).

thf(fun_Pr6626665806141890376t_assn_type,type,
    fun_Pr6626665806141890376t_assn: $tType ).

thf(set_set_Product_unit_type,type,
    set_set_Product_unit: $tType ).

thf(heap_e7401611519738050253t_unit_type,type,
    heap_e7401611519738050253t_unit: $tType ).

thf(fun_Pr616739963666181091un_o_o_type,type,
    fun_Pr616739963666181091un_o_o: $tType ).

thf(fun_o_6763651944650080953unit_o_type,type,
    fun_o_6763651944650080953unit_o: $tType ).

thf(product_prod_num_num_type,type,
    product_prod_num_num: $tType ).

thf(product_prod_nat_num_type,type,
    product_prod_nat_num: $tType ).

thf(product_prod_nat_nat_type,type,
    product_prod_nat_nat: $tType ).

thf(product_prod_nat_int_type,type,
    product_prod_nat_int: $tType ).

thf(product_prod_int_num_type,type,
    product_prod_int_num: $tType ).

thf(product_prod_int_nat_type,type,
    product_prod_int_nat: $tType ).

thf(product_prod_int_int_type,type,
    product_prod_int_int: $tType ).

thf(fun_nat_list_nat_type,type,
    fun_nat_list_nat: $tType ).

thf(fun_list_nat_nat_type,type,
    fun_list_nat_nat: $tType ).

thf(set_Product_prod_o_o_type,type,
    set_Product_prod_o_o: $tType ).

thf(fun_set_num_num_type,type,
    fun_set_num_num: $tType ).

thf(fun_set_nat_nat_type,type,
    fun_set_nat_nat: $tType ).

thf(fun_set_int_rat_type,type,
    fun_set_int_rat: $tType ).

thf(fun_set_int_int_type,type,
    fun_set_int_int: $tType ).

thf(fun_Pr6984036127010467572_o_o_o_type,type,
    fun_Pr6984036127010467572_o_o_o: $tType ).

thf(fun_num_Code_natural_type,type,
    fun_num_Code_natural: $tType ).

thf(fun_num_Code_integer_type,type,
    fun_num_Code_integer: $tType ).

thf(fun_nat_set_nat_type,type,
    fun_nat_set_nat: $tType ).

thf(fun_nat_set_int_type,type,
    fun_nat_set_int: $tType ).

thf(fun_nat_Code_natural_type,type,
    fun_nat_Code_natural: $tType ).

thf(fun_nat_Code_integer_type,type,
    fun_nat_Code_integer: $tType ).

thf(fun_int_set_nat_type,type,
    fun_int_set_nat: $tType ).

thf(fun_int_set_int_type,type,
    fun_int_set_int: $tType ).

thf(fun_int_Code_natural_type,type,
    fun_int_Code_natural: $tType ).

thf(fun_int_Code_integer_type,type,
    fun_int_Code_integer: $tType ).

thf(fun_Code_natural_nat_type,type,
    fun_Code_natural_nat: $tType ).

thf(fun_Code_integer_rat_type,type,
    fun_Code_integer_rat: $tType ).

thf(fun_Code_integer_num_type,type,
    fun_Code_integer_num: $tType ).

thf(fun_Code_integer_nat_type,type,
    fun_Code_integer_nat: $tType ).

thf(fun_Code_integer_int_type,type,
    fun_Code_integer_int: $tType ).

thf(fun_assn_assn_type,type,
    fun_assn_assn: $tType ).

thf(fun_o_4732642864545671890od_o_o_type,type,
    fun_o_4732642864545671890od_o_o: $tType ).

thf(fun_fun_rat_rat_o_type,type,
    fun_fun_rat_rat_o: $tType ).

thf(fun_fun_num_int_o_type,type,
    fun_fun_num_int_o: $tType ).

thf(fun_fun_nat_num_o_type,type,
    fun_fun_nat_num_o: $tType ).

thf(fun_fun_nat_nat_o_type,type,
    fun_fun_nat_nat_o: $tType ).

thf(fun_fun_int_rat_o_type,type,
    fun_fun_int_rat_o: $tType ).

thf(fun_fun_int_num_o_type,type,
    fun_fun_int_num_o: $tType ).

thf(fun_fun_int_nat_o_type,type,
    fun_fun_int_nat_o: $tType ).

thf(fun_fun_int_int_o_type,type,
    fun_fun_int_int_o: $tType ).

thf(fun_set_o_assn_type,type,
    fun_set_o_assn: $tType ).

thf(fun_rat_fun_rat_o_type,type,
    fun_rat_fun_rat_o: $tType ).

thf(fun_rat_fun_nat_o_type,type,
    fun_rat_fun_nat_o: $tType ).

thf(fun_rat_fun_int_o_type,type,
    fun_rat_fun_int_o: $tType ).

thf(fun_rat_fun_o_rat_type,type,
    fun_rat_fun_o_rat: $tType ).

thf(fun_num_fun_num_o_type,type,
    fun_num_fun_num_o: $tType ).

thf(fun_num_fun_int_o_type,type,
    fun_num_fun_int_o: $tType ).

thf(fun_nat_fun_rat_o_type,type,
    fun_nat_fun_rat_o: $tType ).

thf(fun_nat_fun_nat_o_type,type,
    fun_nat_fun_nat_o: $tType ).

thf(fun_nat_fun_int_o_type,type,
    fun_nat_fun_int_o: $tType ).

thf(fun_int_fun_rat_o_type,type,
    fun_int_fun_rat_o: $tType ).

thf(fun_int_fun_num_o_type,type,
    fun_int_fun_num_o: $tType ).

thf(fun_int_fun_nat_o_type,type,
    fun_int_fun_nat_o: $tType ).

thf(fun_int_fun_int_o_type,type,
    fun_int_fun_int_o: $tType ).

thf(fun_set_o_set_o_type,type,
    fun_set_o_set_o: $tType ).

thf(sum_sum_nat_nat_type,type,
    sum_sum_nat_nat: $tType ).

thf(set_option_num_type,type,
    set_option_num: $tType ).

thf(set_option_nat_type,type,
    set_option_nat: $tType ).

thf(set_option_int_type,type,
    set_option_int: $tType ).

thf(option_set_nat_type,type,
    option_set_nat: $tType ).

thf(option_set_int_type,type,
    option_set_int: $tType ).

thf(option_Code_integer_type,type,
    option_Code_integer: $tType ).

thf(fun_set_o_fun_o_o_type,type,
    fun_set_o_fun_o_o: $tType ).

thf(fun_Product_unit_rat_type,type,
    fun_Product_unit_rat: $tType ).

thf(fun_Product_unit_nat_type,type,
    fun_Product_unit_nat: $tType ).

thf(fun_Product_unit_int_type,type,
    fun_Product_unit_int: $tType ).

thf(fun_option_num_o_type,type,
    fun_option_num_o: $tType ).

thf(fun_nat_Product_unit_type,type,
    fun_nat_Product_unit: $tType ).

thf(fun_int_Product_unit_type,type,
    fun_int_Product_unit: $tType ).

thf(fun_o_option_num_type,type,
    fun_o_option_num: $tType ).

thf(option_fun_nat_o_type,type,
    option_fun_nat_o: $tType ).

thf(fun_fun_o_o_fun_o_o_type,type,
    fun_fun_o_o_fun_o_o: $tType ).

thf(fun_nat_array_a_type,type,
    fun_nat_array_a: $tType ).

thf(option_Product_unit_type,type,
    option_Product_unit: $tType ).

thf(set_list_nat_type,type,
    set_list_nat: $tType ).

thf(product_prod_nat_o_type,type,
    product_prod_nat_o: $tType ).

thf(product_prod_int_o_type,type,
    product_prod_int_o: $tType ).

thf(product_prod_o_num_type,type,
    product_prod_o_num: $tType ).

thf(product_prod_o_nat_type,type,
    product_prod_o_nat: $tType ).

thf(product_prod_o_int_type,type,
    product_prod_o_int: $tType ).

thf(fun_list_nat_o_type,type,
    fun_list_nat_o: $tType ).

thf(fun_nat_assn_type,type,
    fun_nat_assn: $tType ).

thf(fun_int_assn_type,type,
    fun_int_assn: $tType ).

thf(set_set_nat_type,type,
    set_set_nat: $tType ).

thf(set_set_int_type,type,
    set_set_int: $tType ).

thf(set_Code_natural_type,type,
    set_Code_natural: $tType ).

thf(set_Code_integer_type,type,
    set_Code_integer: $tType ).

thf(fun_set_nat_o_type,type,
    fun_set_nat_o: $tType ).

thf(fun_set_int_o_type,type,
    fun_set_int_o: $tType ).

thf(fun_set_o_rat_type,type,
    fun_set_o_rat: $tType ).

thf(fun_set_o_nat_type,type,
    fun_set_o_nat: $tType ).

thf(fun_nat_set_o_type,type,
    fun_nat_set_o: $tType ).

thf(fun_int_set_o_type,type,
    fun_int_set_o: $tType ).

thf(fun_Code_natural_o_type,type,
    fun_Code_natural_o: $tType ).

thf(fun_Code_integer_o_type,type,
    fun_Code_integer_o: $tType ).

thf(fun_o_set_nat_type,type,
    fun_o_set_nat: $tType ).

thf(fun_o_set_int_type,type,
    fun_o_set_int: $tType ).

thf(fun_o_Code_integer_type,type,
    fun_o_Code_integer: $tType ).

thf(set_fun_nat_o_type,type,
    set_fun_nat_o: $tType ).

thf(fun_fun_nat_o_o_type,type,
    fun_fun_nat_o_o: $tType ).

thf(fun_fun_int_o_o_type,type,
    fun_fun_int_o_o: $tType ).

thf(fun_nat_fun_o_o_type,type,
    fun_nat_fun_o_o: $tType ).

thf(fun_int_fun_o_o_type,type,
    fun_int_fun_o_o: $tType ).

thf(fun_o_fun_nat_o_type,type,
    fun_o_fun_nat_o: $tType ).

thf(option_assn_type,type,
    option_assn: $tType ).

thf(ref_Product_unit_type,type,
    ref_Product_unit: $tType ).

thf(set_Product_unit_type,type,
    set_Product_unit: $tType ).

thf(set_option_o_type,type,
    set_option_o: $tType ).

thf(option_set_o_type,type,
    option_set_o: $tType ).

thf(ref_array_a_type,type,
    ref_array_a: $tType ).

thf(fun_Product_unit_o_type,type,
    fun_Product_unit_o: $tType ).

thf(fun_option_o_o_type,type,
    fun_option_o_o: $tType ).

thf(fun_o_Product_unit_type,type,
    fun_o_Product_unit: $tType ).

thf(fun_o_option_o_type,type,
    fun_o_option_o: $tType ).

thf(fun_array_a_o_type,type,
    fun_array_a_o: $tType ).

thf(product_prod_o_o_type,type,
    product_prod_o_o: $tType ).

thf(fun_rat_rat_type,type,
    fun_rat_rat: $tType ).

thf(fun_rat_nat_type,type,
    fun_rat_nat: $tType ).

thf(fun_num_rat_type,type,
    fun_num_rat: $tType ).

thf(fun_num_num_type,type,
    fun_num_num: $tType ).

thf(fun_num_nat_type,type,
    fun_num_nat: $tType ).

thf(fun_num_int_type,type,
    fun_num_int: $tType ).

thf(fun_nat_rat_type,type,
    fun_nat_rat: $tType ).

thf(fun_nat_num_type,type,
    fun_nat_num: $tType ).

thf(fun_nat_nat_type,type,
    fun_nat_nat: $tType ).

thf(fun_nat_int_type,type,
    fun_nat_int: $tType ).

thf(fun_int_rat_type,type,
    fun_int_rat: $tType ).

thf(fun_int_num_type,type,
    fun_int_num: $tType ).

thf(fun_int_nat_type,type,
    fun_int_nat: $tType ).

thf(fun_int_int_type,type,
    fun_int_int: $tType ).

thf(set_assn_type,type,
    set_assn: $tType ).

thf(fun_assn_o_type,type,
    fun_assn_o: $tType ).

thf(fun_o_assn_type,type,
    fun_o_assn: $tType ).

thf(set_set_o_type,type,
    set_set_o: $tType ).

thf(fun_o_set_o_type,type,
    fun_o_set_o: $tType ).

thf(option_rat_type,type,
    option_rat: $tType ).

thf(option_num_type,type,
    option_num: $tType ).

thf(option_nat_type,type,
    option_nat: $tType ).

thf(option_int_type,type,
    option_int: $tType ).

thf(list_char_type,type,
    list_char: $tType ).

thf(fun_o_fun_o_o_type,type,
    fun_o_fun_o_o: $tType ).

thf(list_nat_type,type,
    list_nat: $tType ).

thf(list_int_type,type,
    list_int: $tType ).

thf(fun_nat_a_type,type,
    fun_nat_a: $tType ).

thf(set_rat_type,type,
    set_rat: $tType ).

thf(set_num_type,type,
    set_num: $tType ).

thf(set_nat_type,type,
    set_nat: $tType ).

thf(set_int_type,type,
    set_int: $tType ).

thf(code_natural_type,type,
    code_natural: $tType ).

thf(code_integer_type,type,
    code_integer: $tType ).

thf(fun_rat_o_type,type,
    fun_rat_o: $tType ).

thf(fun_num_o_type,type,
    fun_num_o: $tType ).

thf(fun_nat_o_type,type,
    fun_nat_o: $tType ).

thf(fun_int_o_type,type,
    fun_int_o: $tType ).

thf(fun_o_rat_type,type,
    fun_o_rat: $tType ).

thf(fun_o_nat_type,type,
    fun_o_nat: $tType ).

thf(fun_o_int_type,type,
    fun_o_int: $tType ).

thf(product_unit_type,type,
    product_unit: $tType ).

thf(option_o_type,type,
    option_o: $tType ).

thf(array_a_type,type,
    array_a: $tType ).

thf(list_a_type,type,
    list_a: $tType ).

thf(typerep_type,type,
    typerep: $tType ).

thf(assn_type,type,
    assn: $tType ).

thf(set_o_type,type,
    set_o: $tType ).

thf(fun_o_o_type,type,
    fun_o_o: $tType ).

thf(char_type,type,
    char: $tType ).

thf(rat_type,type,
    rat: $tType ).

thf(num_type,type,
    num: $tType ).

thf(nat_type,type,
    nat: $tType ).

thf(int_type,type,
    int: $tType ).

thf(a_type,type,
    a: $tType ).

thf(array_of_list_a_decl,type,
    array_of_list_a: list_a > heap_T6362127782908069795rray_a ).

thf(heap_T5591663578999710211rray_a_decl,type,
    heap_T5591663578999710211rray_a: heap_T6362127782908069795rray_a > fun_he1504492240061592256it_nat ).

thf(heap_T6932021131025641745rray_a_decl,type,
    heap_T6932021131025641745rray_a: heap_T6362127782908069795rray_a > fun_he8413527710729349838unit_o ).

thf(none_P2587165478634041381it_nat_decl,type,
    none_P2587165478634041381it_nat: option3216581401566546698it_nat ).

thf(aa_hea7994211679605476167unit_o_decl,type,
    aa_hea7994211679605476167unit_o: fun_he8413527710729349838unit_o > heap_e7401611519738050253t_unit > $o ).

thf(aa_hea5936688510613671481it_nat_decl,type,
    aa_hea5936688510613671481it_nat: fun_he1504492240061592256it_nat > heap_e7401611519738050253t_unit > option3216581401566546698it_nat ).

thf(h_decl,type,
    h: heap_e7401611519738050253t_unit ).

thf(xs_decl,type,
    xs: list_a ).

thf(1,conjecture,
    ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
   != none_P2587165478634041381it_nat ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

thf(2,negated_conjecture,
    ~ ( ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    inference(neg_conjecture,[status(cth)],[1]) ).

thf(73,plain,
    ~ ( ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(74,plain,
    ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
    = none_P2587165478634041381it_nat ),
    inference(polarity_switch,[status(thm)],[73]) ).

thf(75,plain,
    ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
    = none_P2587165478634041381it_nat ),
    inference(lifteq,[status(thm)],[74]) ).

thf(57,axiom,
    ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
      ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
    <=> ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_success__def) ).

thf(321,plain,
    ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
      ( ( ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat )
       => ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ) )
      & ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
       => ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).

thf(322,plain,
    ( ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
        ( ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat )
       => ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ) )
    & ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
        ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
       => ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat ) ) ),
    inference(miniscope,[status(thm)],[321]) ).

thf(323,plain,
    ! [D: heap_e7401611519738050253t_unit,C: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ( ( D @ ( C @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
        | ( ( D @ ( C @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
          = none_P2587165478634041381it_nat ) )
      & ( ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat )
        | ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ) ) ),
    inference(cnf,[status(esa)],[322]) ).

thf(324,plain,
    ! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat )
      | ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ) ),
    inference(cnfConj,[status(thm)],[323]) ).

thf(326,plain,
    ! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
      | ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    inference(lifteq,[status(thm)],[324]) ).

thf(11798,plain,
    ! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) ) )
      | ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) )
      | ( none_P2587165478634041381it_nat != none_P2587165478634041381it_nat ) ),
    inference(paramod_ordered,[status(thm)],[75,326]) ).

thf(11799,plain,
    ! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) ) )
      | ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ) ),
    inference(simp,[status(thm)],[11798]) ).

thf(11800,plain,
    ~ ( h @ ( xs @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ),
    inference(pattern_uni,[status(thm)],[11799:[bind(A,$thf( xs @ array_of_list_a )),bind(B,$thf( h ))]]) ).

thf(42,axiom,
    ! [A: list_a,B: heap_e7401611519738050253t_unit] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_success__of__listI) ).

thf(271,plain,
    ! [A: list_a,B: heap_e7401611519738050253t_unit] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).

thf(272,plain,
    ! [B: heap_e7401611519738050253t_unit,A: list_a] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea7994211679605476167unit_o ) ),
    inference(cnf,[status(esa)],[271]) ).

thf(11859,plain,
    ~ $true,
    inference(rewrite,[status(thm)],[11800,272]) ).

thf(11860,plain,
    $false,
    inference(simp,[status(thm)],[11859]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP216_3 : TPTP v9.3.1. Bugfixed v9.3.0.
% 0.00/0.09  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.40  % Computer : n004.cluster.edu
% 0.14/0.40  % Model    : x86_64 x86_64
% 0.14/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40  % Memory   : 8046.5625MB
% 0.14/0.40  % OS       : Linux 6.8.0-71-generic
% 0.14/0.40  % CPULimit : 300
% 0.14/0.40  % WCLimit  : 300
% 0.14/0.40  % DateTime : Fri Sep 25 18:11:51 UTC 2026
% 0.14/0.41  % CPUTime  : 
% 0.14/0.41  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.89/1.00  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 7.50/2.64  % [INFO] 	 Parsing done (1640ms). 
% 7.50/2.67  % [INFO] 	 Running in sequential loop mode. 
% 8.82/3.07  % [INFO] 	 eprover registered as external prover. 
% 8.82/3.07  % [INFO] 	 Scanning for conjecture ... 
% 12.74/4.13  % [INFO] 	 Found a conjecture (or negated_conjecture) and 8764 axioms. Running axiom selection ... 
% 14.34/4.47  % [INFO] 	 Axiom selection finished. Selected 70 axioms (removed 8694 axioms). 
% 14.77/4.58  % [INFO] 	 Problem is typed first-order (TPTP TFF). 
% 14.77/4.59  % [INFO] 	 Type checking passed. 
% 15.19/4.60  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 85.25/23.13  % [INFO] 	 Killing All external provers ... 
% 85.45/23.13  % Time passed: 22577ms (effective reasoning time: 20454ms)
% 85.45/23.13  % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 85.45/23.13  % Axioms used in derivation (2): fact_12_success__def, fact_45_success__of__listI
% 85.45/23.13  % No. of inferences in proof: 19
% 85.45/23.13  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22577 ms resp. 20454 ms w/o parsing
% 85.64/23.22  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 85.64/23.23  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------