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

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

% Computer : n008.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 22.09s 7.02s
% Output   : Refutation 22.73s
% 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 :  163 (  23   ~;   7   |;   3   &; 125   @)
%                                         (   1 <=>;   4  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   12 (   6 avg)
%            Number of types       : 1463 (1462 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   12 (   9 usr;   5 con; 0-2 aty)
%            Number of variables   :   26 (   0   ^;  26   !;   0   ?;  26   :)

% Comments : 
%------------------------------------------------------------------------------
thf(fun_Pr2807179424667745021et_nat_type,type,
    fun_Pr2807179424667745021et_nat: $tType ).

thf(fun_fu6830720514880960057et_nat_type,type,
    fun_fu6830720514880960057et_nat: $tType ).

thf(set_Pr6041871929502663225et_nat_type,type,
    set_Pr6041871929502663225et_nat: $tType ).

thf(fun_se6718989106377285345et_nat_type,type,
    fun_se6718989106377285345et_nat: $tType ).

thf(fun_fu5506320456392376999t_bool_type,type,
    fun_fu5506320456392376999t_bool: $tType ).

thf(fun_fu5342292996005483693t_bool_type,type,
    fun_fu5342292996005483693t_bool: $tType ).

thf(fun_Pr6803231168968006865t_bool_type,type,
    fun_Pr6803231168968006865t_bool: $tType ).

thf(fun_se6721183374455628117t_bool_type,type,
    fun_se6721183374455628117t_bool: $tType ).

thf(produc8012095931379219673et_nat_type,type,
    produc8012095931379219673et_nat: $tType ).

thf(fun_Pr1543731576194525813et_nat_type,type,
    fun_Pr1543731576194525813et_nat: $tType ).

thf(fun_Pr6535039171404285501et_nat_type,type,
    fun_Pr6535039171404285501et_nat: $tType ).

thf(fun_fu6557779273964653145et_nat_type,type,
    fun_fu6557779273964653145et_nat: $tType ).

thf(fun_Pr6068767907340899895et_nat_type,type,
    fun_Pr6068767907340899895et_nat: $tType ).

thf(fun_Pr815178062494392389nteger_type,type,
    fun_Pr815178062494392389nteger: $tType ).

thf(fun_fu8117160030729213177nteger_type,type,
    fun_fu8117160030729213177nteger: $tType ).

thf(set_Pr617690850500594159nteger_type,type,
    set_Pr617690850500594159nteger: $tType ).

thf(fun_fu6062884189030247124et_nat_type,type,
    fun_fu6062884189030247124et_nat: $tType ).

thf(fun_se7809869488953130391nteger_type,type,
    fun_se7809869488953130391nteger: $tType ).

thf(fun_Pr1666087629320038414et_nat_type,type,
    fun_Pr1666087629320038414et_nat: $tType ).

thf(fun_fu8244261039515384701r_bool_type,type,
    fun_fu8244261039515384701r_bool: $tType ).

thf(fun_fu9137738613959528033r_bool_type,type,
    fun_fu9137738613959528033r_bool: $tType ).

thf(fun_se6148028026915889663r_bool_type,type,
    fun_se6148028026915889663r_bool: $tType ).

thf(produc3545778865006486671nteger_type,type,
    produc3545778865006486671nteger: $tType ).

thf(fun_Pr6859458860894228184et_nat_type,type,
    fun_Pr6859458860894228184et_nat: $tType ).

thf(fun_Pr8176305432000512344et_nat_type,type,
    fun_Pr8176305432000512344et_nat: $tType ).

thf(fun_Pr2446957282624100774et_nat_type,type,
    fun_Pr2446957282624100774et_nat: $tType ).

thf(fun_Pr4485270859031309117nt_int_type,type,
    fun_Pr4485270859031309117nt_int: $tType ).

thf(fun_Pr5378236496403346987nteger_type,type,
    fun_Pr5378236496403346987nteger: $tType ).

thf(fun_Pr3675547549916427543nteger_type,type,
    fun_Pr3675547549916427543nteger: $tType ).

thf(fun_fu7566577365572809253nteger_type,type,
    fun_fu7566577365572809253nteger: $tType ).

thf(fun_Pr4990231762125007739nteger_type,type,
    fun_Pr4990231762125007739nteger: $tType ).

thf(fun_fu1513955274505230777nt_int_type,type,
    fun_fu1513955274505230777nt_int: $tType ).

thf(set_Pr445502709953361865nt_int_type,type,
    set_Pr445502709953361865nt_int: $tType ).

thf(fun_se6660130108295884657nt_int_type,type,
    fun_se6660130108295884657nt_int: $tType ).

thf(fun_fu3411262949498040381t_bool_type,type,
    fun_fu3411262949498040381t_bool: $tType ).

thf(fun_fu6626674399359463303t_bool_type,type,
    fun_fu6626674399359463303t_bool: $tType ).

thf(fun_se5440134326651146559t_bool_type,type,
    fun_se5440134326651146559t_bool: $tType ).

thf(produc7524484978061485929nt_int_type,type,
    produc7524484978061485929nt_int: $tType ).

thf(fun_Pr7484837052886145285nt_int_type,type,
    fun_Pr7484837052886145285nt_int: $tType ).

thf(fun_Pr8758129639794321555nt_int_type,type,
    fun_Pr8758129639794321555nt_int: $tType ).

thf(fun_fu6705478841943783171nteger_type,type,
    fun_fu6705478841943783171nteger: $tType ).

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

thf(fun_fu5089991873703640569et_nat_type,type,
    fun_fu5089991873703640569et_nat: $tType ).

thf(fun_fu8051346760639647871nt_int_type,type,
    fun_fu8051346760639647871nt_int: $tType ).

thf(fun_fu1566933136005619827et_nat_type,type,
    fun_fu1566933136005619827et_nat: $tType ).

thf(fun_Pr31557271651610743nt_int_type,type,
    fun_Pr31557271651610743nt_int: $tType ).

thf(fun_fu6520206799837733709nteger_type,type,
    fun_fu6520206799837733709nteger: $tType ).

thf(fun_Pr3374013140141549901e_term_type,type,
    fun_Pr3374013140141549901e_term: $tType ).

thf(set_Pr4255865656320958847et_nat_type,type,
    set_Pr4255865656320958847et_nat: $tType ).

thf(fun_se3640837633174573095et_nat_type,type,
    fun_se3640837633174573095et_nat: $tType ).

thf(fun_fu5003113910669962087t_bool_type,type,
    fun_fu5003113910669962087t_bool: $tType ).

thf(fun_fu5052605875793943143t_bool_type,type,
    fun_fu5052605875793943143t_bool: $tType ).

thf(fun_fu6017850665423146429et_nat_type,type,
    fun_fu6017850665423146429et_nat: $tType ).

thf(fun_Pr6052842969455678475t_bool_type,type,
    fun_Pr6052842969455678475t_bool: $tType ).

thf(fun_se7483882374545735573t_bool_type,type,
    fun_se7483882374545735573t_bool: $tType ).

thf(produc586578377766392095et_nat_type,type,
    produc586578377766392095et_nat: $tType ).

thf(fun_Pr5123258793648662203et_nat_type,type,
    fun_Pr5123258793648662203et_nat: $tType ).

thf(fun_Pr3659704428484505341et_nat_type,type,
    fun_Pr3659704428484505341et_nat: $tType ).

thf(fun_fu41535106210742625nt_int_type,type,
    fun_fu41535106210742625nt_int: $tType ).

thf(fun_fu9083788306713281567et_nat_type,type,
    fun_fu9083788306713281567et_nat: $tType ).

thf(fun_Pr91909758419373431et_nat_type,type,
    fun_Pr91909758419373431et_nat: $tType ).

thf(fun_se1439950603930758947t_bool_type,type,
    fun_se1439950603930758947t_bool: $tType ).

thf(fun_fu5057520102127866923nt_int_type,type,
    fun_fu5057520102127866923nt_int: $tType ).

thf(fun_Pr8183925273605298603e_term_type,type,
    fun_Pr8183925273605298603e_term: $tType ).

thf(fun_Pr5666082323645954453nt_int_type,type,
    fun_Pr5666082323645954453nt_int: $tType ).

thf(fun_se410074049581437823t_bool_type,type,
    fun_se410074049581437823t_bool: $tType ).

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

thf(set_Pr2036385042155664947e_term_type,type,
    set_Pr2036385042155664947e_term: $tType ).

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

thf(produc6165324128657218515e_term_type,type,
    produc6165324128657218515e_term: $tType ).

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

thf(set_Pr4602751158188618133e_term_type,type,
    set_Pr4602751158188618133e_term: $tType ).

thf(fun_fu3129209171350298991e_term_type,type,
    fun_fu3129209171350298991e_term: $tType ).

thf(set_fu3020806088223967764t_bool_type,type,
    set_fu3020806088223967764t_bool: $tType ).

thf(fun_fu4391313403955021497nt_int_type,type,
    fun_fu4391313403955021497nt_int: $tType ).

thf(produc4772105275349516341e_term_type,type,
    produc4772105275349516341e_term: $tType ).

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

thf(set_se7638649912989706536et_nat_type,type,
    set_se7638649912989706536et_nat: $tType ).

thf(set_Pr2100580169568797217nt_int_type,type,
    set_Pr2100580169568797217nt_int: $tType ).

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

thf(fun_se3829259811004365257nt_int_type,type,
    fun_se3829259811004365257nt_int: $tType ).

thf(fun_fu460498724395885885t_bool_type,type,
    fun_fu460498724395885885t_bool: $tType ).

thf(fun_fu5339995725730582831t_bool_type,type,
    fun_fu5339995725730582831t_bool: $tType ).

thf(fun_Pr229822445725053876t_bool_type,type,
    fun_Pr229822445725053876t_bool: $tType ).

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

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

thf(set_fu9144750265070497052t_bool_type,type,
    set_fu9144750265070497052t_bool: $tType ).

thf(option7217372446798200844et_nat_type,type,
    option7217372446798200844et_nat: $tType ).

thf(fun_fu7892715005995238119nteger_type,type,
    fun_fu7892715005995238119nteger: $tType ).

thf(fun_Pr5173018050610649193t_bool_type,type,
    fun_Pr5173018050610649193t_bool: $tType ).

thf(fun_Pr5642303602281900219nteger_type,type,
    fun_Pr5642303602281900219nteger: $tType ).

thf(fun_Pr2941448120420799789t_bool_type,type,
    fun_Pr2941448120420799789t_bool: $tType ).

thf(fun_se5891774057180752959t_bool_type,type,
    fun_se5891774057180752959t_bool: $tType ).

thf(fun_Pr1839114978789310443t_bool_type,type,
    fun_Pr1839114978789310443t_bool: $tType ).

thf(fun_fu77927427245549009e_term_type,type,
    fun_fu77927427245549009e_term: $tType ).

thf(set_Pr9222568342844664434et_nat_type,type,
    set_Pr9222568342844664434et_nat: $tType ).

thf(set_Pr222142748458615354t_bool_type,type,
    set_Pr222142748458615354t_bool: $tType ).

thf(produc7823662180168248769nt_int_type,type,
    produc7823662180168248769nt_int: $tType ).

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

thf(fun_fu5758690788630904038t_bool_type,type,
    fun_fu5758690788630904038t_bool: $tType ).

thf(fun_Pr215885126604245128l_bool_type,type,
    fun_Pr215885126604245128l_bool: $tType ).

thf(fun_Pr2744799836182991581nteger_type,type,
    fun_Pr2744799836182991581nteger: $tType ).

thf(fun_Pr6784847270111311109nteger_type,type,
    fun_Pr6784847270111311109nteger: $tType ).

thf(fun_fu1965482174671583728et_nat_type,type,
    fun_fu1965482174671583728et_nat: $tType ).

thf(produc1542783094787327164et_nat_type,type,
    produc1542783094787327164et_nat: $tType ).

thf(produc6968460846966063236t_bool_type,type,
    produc6968460846966063236t_bool: $tType ).

thf(fun_fu4519763388929186643r_bool_type,type,
    fun_fu4519763388929186643r_bool: $tType ).

thf(fun_fu4654294921587638483r_bool_type,type,
    fun_fu4654294921587638483r_bool: $tType ).

thf(fun_fu7547279164713276502et_nat_type,type,
    fun_fu7547279164713276502et_nat: $tType ).

thf(fun_Pr4428780497284940104t_bool_type,type,
    fun_Pr4428780497284940104t_bool: $tType ).

thf(fun_Pr8817784564977180509nt_int_type,type,
    fun_Pr8817784564977180509nt_int: $tType ).

thf(fun_Pr7740151853985107347nt_int_type,type,
    fun_Pr7740151853985107347nt_int: $tType ).

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

thf(fun_se5827390231571168307t_bool_type,type,
    fun_se5827390231571168307t_bool: $tType ).

thf(fun_fu2885425669800053280et_nat_type,type,
    fun_fu2885425669800053280et_nat: $tType ).

thf(fun_Pr8311103421978789352t_bool_type,type,
    fun_Pr8311103421978789352t_bool: $tType ).

thf(fun_fu1987685234545457367nt_int_type,type,
    fun_fu1987685234545457367nt_int: $tType ).

thf(fun_Pr3770084164778801015nt_int_type,type,
    fun_Pr3770084164778801015nt_int: $tType ).

thf(fun_fu5777305227152776218et_nat_type,type,
    fun_fu5777305227152776218et_nat: $tType ).

thf(fun_Pr2756711131340254292et_nat_type,type,
    fun_Pr2756711131340254292et_nat: $tType ).

thf(fun_se1849273899464988991t_bool_type,type,
    fun_se1849273899464988991t_bool: $tType ).

thf(fun_fu8201824545032078335m_bool_type,type,
    fun_fu8201824545032078335m_bool: $tType ).

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

thf(fun_Pr2210758139564844958et_nat_type,type,
    fun_Pr2210758139564844958et_nat: $tType ).

thf(fun_Pr761831339830696478et_nat_type,type,
    fun_Pr761831339830696478et_nat: $tType ).

thf(fun_Pr4617804334418790189t_bool_type,type,
    fun_Pr4617804334418790189t_bool: $tType ).

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

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

thf(set_fu7455301249681563705r_bool_type,type,
    set_fu7455301249681563705r_bool: $tType ).

thf(fun_Pr8335005258140926131t_bool_type,type,
    fun_Pr8335005258140926131t_bool: $tType ).

thf(fun_fu5021597990576145078nt_int_type,type,
    fun_fu5021597990576145078nt_int: $tType ).

thf(fun_Pr8801321285129957574nt_int_type,type,
    fun_Pr8801321285129957574nt_int: $tType ).

thf(fun_fu5179508664593719725at_nat_type,type,
    fun_fu5179508664593719725at_nat: $tType ).

thf(set_se4861237852875603267nteger_type,type,
    set_se4861237852875603267nteger: $tType ).

thf(fun_op714873039799603609t_bool_type,type,
    fun_op714873039799603609t_bool: $tType ).

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

thf(fun_op5695908178767990053t_bool_type,type,
    fun_op5695908178767990053t_bool: $tType ).

thf(fun_op2795105856722530129t_bool_type,type,
    fun_op2795105856722530129t_bool: $tType ).

thf(fun_Pr5991498150630465241r_bool_type,type,
    fun_Pr5991498150630465241r_bool: $tType ).

thf(fun_op1881258161251107181t_bool_type,type,
    fun_op1881258161251107181t_bool: $tType ).

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

thf(fun_fu1840957874120405363t_bool_type,type,
    fun_fu1840957874120405363t_bool: $tType ).

thf(fun_fu9188068041668609877t_bool_type,type,
    fun_fu9188068041668609877t_bool: $tType ).

thf(set_fu5758910737289105323r_bool_type,type,
    set_fu5758910737289105323r_bool: $tType ).

thf(option9154429786015072807nteger_type,type,
    option9154429786015072807nteger: $tType ).

thf(fun_fu6475724375324676052et_nat_type,type,
    fun_fu6475724375324676052et_nat: $tType ).

thf(fun_fu1662175956536757296et_int_type,type,
    fun_fu1662175956536757296et_int: $tType ).

thf(fun_fu1667363907666229857nt_int_type,type,
    fun_fu1667363907666229857nt_int: $tType ).

thf(fun_Pr7144702500346731470nt_int_type,type,
    fun_Pr7144702500346731470nt_int: $tType ).

thf(fun_Pr3164600974287165328nt_int_type,type,
    fun_Pr3164600974287165328nt_int: $tType ).

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

thf(fun_Pr124437560471516333t_bool_type,type,
    fun_Pr124437560471516333t_bool: $tType ).

thf(set_Pr5663546166630115725nteger_type,type,
    set_Pr5663546166630115725nteger: $tType ).

thf(set_Pr2512414763863242873e_term_type,type,
    set_Pr2512414763863242873e_term: $tType ).

thf(fun_fu559770791806514597e_term_type,type,
    fun_fu559770791806514597e_term: $tType ).

thf(fun_fu2392079970875071397e_term_type,type,
    fun_fu2392079970875071397e_term: $tType ).

thf(fun_se5420953908473809257t_bool_type,type,
    fun_se5420953908473809257t_bool: $tType ).

thf(fun_fu288323284703510083t_bool_type,type,
    fun_fu288323284703510083t_bool: $tType ).

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

thf(fun_fu1674507805476766837r_bool_type,type,
    fun_fu1674507805476766837r_bool: $tType ).

thf(fun_Pr3079291148292310431m_bool_type,type,
    fun_Pr3079291148292310431m_bool: $tType ).

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

thf(fun_fu1322586181023640363nt_int_type,type,
    fun_fu1322586181023640363nt_int: $tType ).

thf(fun_Pr1761269348221162155e_term_type,type,
    fun_Pr1761269348221162155e_term: $tType ).

thf(fun_fu460979959883446785nteger_type,type,
    fun_fu460979959883446785nteger: $tType ).

thf(produc651309673056299192atural_type,type,
    produc651309673056299192atural: $tType ).

thf(produc1616345218596728535nteger_type,type,
    produc1616345218596728535nteger: $tType ).

thf(produc7630353427218314179e_term_type,type,
    produc7630353427218314179e_term: $tType ).

thf(fun_se4102533757149558089t_bool_type,type,
    fun_se4102533757149558089t_bool: $tType ).

thf(fun_fu2363360051551328923nteger_type,type,
    fun_fu2363360051551328923nteger: $tType ).

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

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

thf(fun_Pr8743693014225067613e_term_type,type,
    fun_Pr8743693014225067613e_term: $tType ).

thf(set_fu430091371078912524t_bool_type,type,
    set_fu430091371078912524t_bool: $tType ).

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

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

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

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

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

thf(set_se8601878649772475440nt_int_type,type,
    set_se8601878649772475440nt_int: $tType ).

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

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

thf(fun_se476553922966766403t_bool_type,type,
    fun_se476553922966766403t_bool: $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(fun_Pr6019674992625747500t_bool_type,type,
    fun_Pr6019674992625747500t_bool: $tType ).

thf(set_fu599982199386018686t_bool_type,type,
    set_fu599982199386018686t_bool: $tType ).

thf(option8369045977646850964nt_int_type,type,
    option8369045977646850964nt_int: $tType ).

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

thf(fun_fu8207889344993942070t_bool_type,type,
    fun_fu8207889344993942070t_bool: $tType ).

thf(fun_fu104655026003841100t_bool_type,type,
    fun_fu104655026003841100t_bool: $tType ).

thf(set_Pr233528076387193594nt_int_type,type,
    set_Pr233528076387193594nt_int: $tType ).

thf(set_Pr3306494517088666248e_term_type,type,
    set_Pr3306494517088666248e_term: $tType ).

thf(fun_fu914172361577146165r_bool_type,type,
    fun_fu914172361577146165r_bool: $tType ).

thf(fun_fu8712359873818342837r_bool_type,type,
    fun_fu8712359873818342837r_bool: $tType ).

thf(fun_se3294407966017900847t_bool_type,type,
    fun_se3294407966017900847t_bool: $tType ).

thf(set_fu5772817297505879153t_bool_type,type,
    set_fu5772817297505879153t_bool: $tType ).

thf(set_Pr2055239900342597383t_bool_type,type,
    set_Pr2055239900342597383t_bool: $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_fu4196931294019812808t_bool_type,type,
    fun_fu4196931294019812808t_bool: $tType ).

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

thf(fun_Pr4770605958729007056m_bool_type,type,
    fun_Pr4770605958729007056m_bool: $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_fu4756305112005770350nt_int_type,type,
    fun_fu4756305112005770350nt_int: $tType ).

thf(set_se3623507840239494155et_nat_type,type,
    set_se3623507840239494155et_nat: $tType ).

thf(set_Pr1054393349331465021e_term_type,type,
    set_Pr1054393349331465021e_term: $tType ).

thf(produc4441460161354545860nt_int_type,type,
    produc4441460161354545860nt_int: $tType ).

thf(produc58788776713507154e_term_type,type,
    produc58788776713507154e_term: $tType ).

thf(fun_fu7484445891136787336nt_int_type,type,
    fun_fu7484445891136787336nt_int: $tType ).

thf(fun_fu651862883045798072r_bool_type,type,
    fun_fu651862883045798072r_bool: $tType ).

thf(fun_fu2707451377710855992r_bool_type,type,
    fun_fu2707451377710855992r_bool: $tType ).

thf(fun_Pr5239940216409749356e_term_type,type,
    fun_Pr5239940216409749356e_term: $tType ).

thf(fun_Pr3073222722562426257t_bool_type,type,
    fun_Pr3073222722562426257t_bool: $tType ).

thf(produc1469476007717053223t_bool_type,type,
    produc1469476007717053223t_bool: $tType ).

thf(fun_fu950101255003131299t_bool_type,type,
    fun_fu950101255003131299t_bool: $tType ).

thf(fun_se1432960176876588069t_bool_type,type,
    fun_se1432960176876588069t_bool: $tType ).

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

thf(set_fu4707872845232295289t_bool_type,type,
    set_fu4707872845232295289t_bool: $tType ).

thf(option6601582610923217263et_nat_type,type,
    option6601582610923217263et_nat: $tType ).

thf(fun_fu1643940435916084742et_nat_type,type,
    fun_fu1643940435916084742et_nat: $tType ).

thf(fun_fu6053764053982941794et_int_type,type,
    fun_fu6053764053982941794et_int: $tType ).

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

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

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

thf(produc3633599497793833399nteger_type,type,
    produc3633599497793833399nteger: $tType ).

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

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

thf(fun_fu3065787814506259139l_bool_type,type,
    fun_fu3065787814506259139l_bool: $tType ).

thf(fun_fu3361945992317226875l_bool_type,type,
    fun_fu3361945992317226875l_bool: $tType ).

thf(fun_fu8102205367403595787l_bool_type,type,
    fun_fu8102205367403595787l_bool: $tType ).

thf(fun_fu8398363545214563523l_bool_type,type,
    fun_fu8398363545214563523l_bool: $tType ).

thf(fun_fu7697223484234057186nt_int_type,type,
    fun_fu7697223484234057186nt_int: $tType ).

thf(fun_Pr836001258840238578nt_int_type,type,
    fun_Pr836001258840238578nt_int: $tType ).

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

thf(fun_Pr3377396784085331203atural_type,type,
    fun_Pr3377396784085331203atural: $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(set_Pr1106803562331729365et_nat_type,type,
    set_Pr1106803562331729365et_nat: $tType ).

thf(set_Pr8919652553310308119t_bool_type,type,
    set_Pr8919652553310308119t_bool: $tType ).

thf(fun_fu4380655706055240813t_bool_type,type,
    fun_fu4380655706055240813t_bool: $tType ).

thf(fun_fu5684592866614294253l_bool_type,type,
    fun_fu5684592866614294253l_bool: $tType ).

thf(fun_fu1400926039381987309l_bool_type,type,
    fun_fu1400926039381987309l_bool: $tType ).

thf(fun_fu5452874025675261293t_bool_type,type,
    fun_fu5452874025675261293t_bool: $tType ).

thf(produc1612822581565466077e_term_type,type,
    produc1612822581565466077e_term: $tType ).

thf(fun_fu4727260872910924933m_bool_type,type,
    fun_fu4727260872910924933m_bool: $tType ).

thf(fun_fu6604189505928284969m_bool_type,type,
    fun_fu6604189505928284969m_bool: $tType ).

thf(fun_fu162221323889317536t_bool_type,type,
    fun_fu162221323889317536t_bool: $tType ).

thf(fun_fu7398481913972163267t_bool_type,type,
    fun_fu7398481913972163267t_bool: $tType ).

thf(fun_Pr979140477516945259l_bool_type,type,
    fun_Pr979140477516945259l_bool: $tType ).

thf(fun_fu4948367345633731229t_bool_type,type,
    fun_fu4948367345633731229t_bool: $tType ).

thf(fun_fu6675107418524772179et_nat_type,type,
    fun_fu6675107418524772179et_nat: $tType ).

thf(produc9029942977526534568nteger_type,type,
    produc9029942977526534568nteger: $tType ).

thf(produc6326149649888671750rm_int_type,type,
    produc6326149649888671750rm_int: $tType ).

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

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

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

thf(fun_Pr5516775990684837794nt_int_type,type,
    fun_Pr5516775990684837794nt_int: $tType ).

thf(fun_Pr7875579814169730748nt_int_type,type,
    fun_Pr7875579814169730748nt_int: $tType ).

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

thf(fun_Co7167173454658490195e_term_type,type,
    fun_Co7167173454658490195e_term: $tType ).

thf(produc6108883039684432031et_nat_type,type,
    produc6108883039684432031et_nat: $tType ).

thf(produc2123963014314306273t_bool_type,type,
    produc2123963014314306273t_bool: $tType ).

thf(fun_fu3348679225844166803t_bool_type,type,
    fun_fu3348679225844166803t_bool: $tType ).

thf(fun_fu6555626273176734310at_nat_type,type,
    fun_fu6555626273176734310at_nat: $tType ).

thf(fun_fu1426818202555147193et_nat_type,type,
    fun_fu1426818202555147193et_nat: $tType ).

thf(fun_Pr6497481519160918949t_bool_type,type,
    fun_Pr6497481519160918949t_bool: $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(fun_fu2477166813681994617e_term_type,type,
    fun_fu2477166813681994617e_term: $tType ).

thf(fun_Pr2277466061178473465t_bool_type,type,
    fun_Pr2277466061178473465t_bool: $tType ).

thf(fun_Pr770811015315158701t_bool_type,type,
    fun_Pr770811015315158701t_bool: $tType ).

thf(fun_fu4272674133525273539t_bool_type,type,
    fun_fu4272674133525273539t_bool: $tType ).

thf(fun_fu2754956555950464963t_bool_type,type,
    fun_fu2754956555950464963t_bool: $tType ).

thf(fun_se1920051578875018791t_bool_type,type,
    fun_se1920051578875018791t_bool: $tType ).

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

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

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

thf(produc1686132544488752119rm_int_type,type,
    produc1686132544488752119rm_int: $tType ).

thf(fun_fu3684477910254590263m_bool_type,type,
    fun_fu3684477910254590263m_bool: $tType ).

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

thf(fun_in6001120578269527074e_term_type,type,
    fun_in6001120578269527074e_term: $tType ).

thf(fun_Co5047008555471425220e_term_type,type,
    fun_Co5047008555471425220e_term: $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(produc6284619029570389740atural_type,type,
    produc6284619029570389740atural: $tType ).

thf(produc5207004643709237345nteger_type,type,
    produc5207004643709237345nteger: $tType ).

thf(fun_fu145699692494531967r_bool_type,type,
    fun_fu145699692494531967r_bool: $tType ).

thf(fun_Pr8933696392609397829t_bool_type,type,
    fun_Pr8933696392609397829t_bool: $tType ).

thf(fun_fu365010997111080675t_bool_type,type,
    fun_fu365010997111080675t_bool: $tType ).

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

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

thf(fun_Pr265694008056721289t_bool_type,type,
    fun_Pr265694008056721289t_bool: $tType ).

thf(fun_Pr5808802887211738685t_bool_type,type,
    fun_Pr5808802887211738685t_bool: $tType ).

thf(set_fu2883028153058477999e_term_type,type,
    set_fu2883028153058477999e_term: $tType ).

thf(set_fu7756500965152462304t_bool_type,type,
    set_fu7756500965152462304t_bool: $tType ).

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

thf(fun_se5090489388428745551t_bool_type,type,
    fun_se5090489388428745551t_bool: $tType ).

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

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

thf(fun_fu3889648052272912774m_bool_type,type,
    fun_fu3889648052272912774m_bool: $tType ).

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

thf(fun_in4543820613646645139e_term_type,type,
    fun_in4543820613646645139e_term: $tType ).

thf(fun_fu3067104787903415085l_bool_type,type,
    fun_fu3067104787903415085l_bool: $tType ).

thf(fun_fu7729223165963301933l_bool_type,type,
    fun_fu7729223165963301933l_bool: $tType ).

thf(produc4503464469895592971e_term_type,type,
    produc4503464469895592971e_term: $tType ).

thf(set_se1111200241945062748nt_int_type,type,
    set_se1111200241945062748nt_int: $tType ).

thf(produc5008273676354626024atural_type,type,
    produc5008273676354626024atural: $tType ).

thf(fun_fu5740879047348081577t_bool_type,type,
    fun_fu5740879047348081577t_bool: $tType ).

thf(fun_fu3728406814708807017r_bool_type,type,
    fun_fu3728406814708807017r_bool: $tType ).

thf(fun_Co6521367752074460393r_bool_type,type,
    fun_Co6521367752074460393r_bool: $tType ).

thf(fun_op4621176226433041415m_bool_type,type,
    fun_op4621176226433041415m_bool: $tType ).

thf(fun_op2573228148205091335t_bool_type,type,
    fun_op2573228148205091335t_bool: $tType ).

thf(fun_fu1384700656636806920t_bool_type,type,
    fun_fu1384700656636806920t_bool: $tType ).

thf(fun_Pr8336614522058983534e_term_type,type,
    fun_Pr8336614522058983534e_term: $tType ).

thf(fun_Pr272337284026993017e_term_type,type,
    fun_Pr272337284026993017e_term: $tType ).

thf(fun_op4713120309324841407m_bool_type,type,
    fun_op4713120309324841407m_bool: $tType ).

thf(fun_op3309915021702834487t_bool_type,type,
    fun_op3309915021702834487t_bool: $tType ).

thf(set_fu8544203214900410144e_term_type,type,
    set_fu8544203214900410144e_term: $tType ).

thf(fun_Pr5504123824928244736t_bool_type,type,
    fun_Pr5504123824928244736t_bool: $tType ).

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

thf(fun_se1674533851335260987t_bool_type,type,
    fun_se1674533851335260987t_bool: $tType ).

thf(fun_na3031409785987805145t_bool_type,type,
    fun_na3031409785987805145t_bool: $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_fu7778341886357639804t_bool_type,type,
    fun_fu7778341886357639804t_bool: $tType ).

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

thf(set_fu5020361207429046098t_bool_type,type,
    set_fu5020361207429046098t_bool: $tType ).

thf(option3896775892727155392nt_int_type,type,
    option3896775892727155392nt_int: $tType ).

thf(fun_fu4770337263308229357et_nat_type,type,
    fun_fu4770337263308229357et_nat: $tType ).

thf(fun_fu9180160881375086409et_int_type,type,
    fun_fu9180160881375086409et_int: $tType ).

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

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

thf(set_Pr5033440245338114598nt_int_type,type,
    set_Pr5033440245338114598nt_int: $tType ).

thf(set_Pr327627314929616988e_term_type,type,
    set_Pr327627314929616988e_term: $tType ).

thf(fun_fu4098021334547386539m_bool_type,type,
    fun_fu4098021334547386539m_bool: $tType ).

thf(fun_fu1598022910586281643r_bool_type,type,
    fun_fu1598022910586281643r_bool: $tType ).

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

thf(fun_fu7001881159509891436m_bool_type,type,
    fun_fu7001881159509891436m_bool: $tType ).

thf(fun_fu227840033125495216t_bool_type,type,
    fun_fu227840033125495216t_bool: $tType ).

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

thf(fun_fu2277959939282174915t_bool_type,type,
    fun_fu2277959939282174915t_bool: $tType ).

thf(fun_fu3636461085284164363t_bool_type,type,
    fun_fu3636461085284164363t_bool: $tType ).

thf(fun_fu8570572252482796155t_bool_type,type,
    fun_fu8570572252482796155t_bool: $tType ).

thf(fun_fu705701361630009795t_bool_type,type,
    fun_fu705701361630009795t_bool: $tType ).

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

thf(fun_Pr9164807099015279978e_term_type,type,
    fun_Pr9164807099015279978e_term: $tType ).

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

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

thf(fun_fu4393453706068901145nt_int_type,type,
    fun_fu4393453706068901145nt_int: $tType ).

thf(fun_fu2398795396165620743t_bool_type,type,
    fun_fu2398795396165620743t_bool: $tType ).

thf(fun_fu6482193285690073351t_bool_type,type,
    fun_fu6482193285690073351t_bool: $tType ).

thf(fun_fu1669044704203846169nt_int_type,type,
    fun_fu1669044704203846169nt_int: $tType ).

thf(fun_Pr6683648610538735667t_bool_type,type,
    fun_Pr6683648610538735667t_bool: $tType ).

thf(fun_fu5117548769634986908t_bool_type,type,
    fun_fu5117548769634986908t_bool: $tType ).

thf(fun_Pr1869630247880246524m_bool_type,type,
    fun_Pr1869630247880246524m_bool: $tType ).

thf(fun_se7080226292506856579t_bool_type,type,
    fun_se7080226292506856579t_bool: $tType ).

thf(fun_na1368090206904050563t_bool_type,type,
    fun_na1368090206904050563t_bool: $tType ).

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

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

thf(fun_fu3249470265263746970nt_int_type,type,
    fun_fu3249470265263746970nt_int: $tType ).

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

thf(fun_Pr5059958867285579810t_bool_type,type,
    fun_Pr5059958867285579810t_bool: $tType ).

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

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

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

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

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

thf(fun_se6536842313551395852t_bool_type,type,
    fun_se6536842313551395852t_bool: $tType ).

thf(produc6768802789813714928nt_int_type,type,
    produc6768802789813714928nt_int: $tType ).

thf(produc6449747366704183590e_term_type,type,
    produc6449747366704183590e_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(produc2867611627572283311it_nat_type,type,
    produc2867611627572283311it_nat: $tType ).

thf(fun_fu4948051095633561780nt_int_type,type,
    fun_fu4948051095633561780nt_int: $tType ).

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

thf(fun_Pr738545119279701312e_term_type,type,
    fun_Pr738545119279701312e_term: $tType ).

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

thf(fun_fu7832787587439741972t_bool_type,type,
    fun_fu7832787587439741972t_bool: $tType ).

thf(set_Pr1755120295921311620it_nat_type,type,
    set_Pr1755120295921311620it_nat: $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(set_fu6121089819231310569t_bool_type,type,
    set_fu6121089819231310569t_bool: $tType ).

thf(fun_fu5036059946722339607r_bool_type,type,
    fun_fu5036059946722339607r_bool: $tType ).

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

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

thf(fun_se5512055894501965997t_bool_type,type,
    fun_se5512055894501965997t_bool: $tType ).

thf(fun_se5485459612626037543t_bool_type,type,
    fun_se5485459612626037543t_bool: $tType ).

thf(fun_Pr4637083014979798189l_bool_type,type,
    fun_Pr4637083014979798189l_bool: $tType ).

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

thf(option1583680563626158861at_nat_type,type,
    option1583680563626158861at_nat: $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_fu5891520417612471363l_bool_type,type,
    fun_fu5891520417612471363l_bool: $tType ).

thf(fun_fu4742933721375295171l_bool_type,type,
    fun_fu4742933721375295171l_bool: $tType ).

thf(fun_fu8257149337340458235l_bool_type,type,
    fun_fu8257149337340458235l_bool: $tType ).

thf(fun_fu4149843117682001291l_bool_type,type,
    fun_fu4149843117682001291l_bool: $tType ).

thf(fun_fu6515472037409988163l_bool_type,type,
    fun_fu6515472037409988163l_bool: $tType ).

thf(fun_fu280261775932326083l_bool_type,type,
    fun_fu280261775932326083l_bool: $tType ).

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

thf(fun_fu3399262604606875836l_bool_type,type,
    fun_fu3399262604606875836l_bool: $tType ).

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

thf(fun_fu3050087747365015277t_bool_type,type,
    fun_fu3050087747365015277t_bool: $tType ).

thf(fun_fu7425989562788193773l_bool_type,type,
    fun_fu7425989562788193773l_bool: $tType ).

thf(fun_fu2173003187950939885l_bool_type,type,
    fun_fu2173003187950939885l_bool: $tType ).

thf(fun_fu6090742429400225773t_bool_type,type,
    fun_fu6090742429400225773t_bool: $tType ).

thf(fun_fu3533317036915336195t_bool_type,type,
    fun_fu3533317036915336195t_bool: $tType ).

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

thf(fun_fu3554580122256925143m_bool_type,type,
    fun_fu3554580122256925143m_bool: $tType ).

thf(fun_fu6575396949002572433t_bool_type,type,
    fun_fu6575396949002572433t_bool: $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(fun_se1647539797697457274t_bool_type,type,
    fun_se1647539797697457274t_bool: $tType ).

thf(fun_op5902475268499868568t_bool_type,type,
    fun_op5902475268499868568t_bool: $tType ).

thf(fun_bo550434615056539650it_nat_type,type,
    fun_bo550434615056539650it_nat: $tType ).

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

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

thf(fun_op5103028270430080336t_bool_type,type,
    fun_op5103028270430080336t_bool: $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_Pr2994431579521131585on_num_type,type,
    fun_Pr2994431579521131585on_num: $tType ).

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

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

thf(fun_fu7993321427942571930at_nat_type,type,
    fun_fu7993321427942571930at_nat: $tType ).

thf(fun_fu5855118699552457754t_bool_type,type,
    fun_fu5855118699552457754t_bool: $tType ).

thf(fun_fu6917712468085671990t_bool_type,type,
    fun_fu6917712468085671990t_bool: $tType ).

thf(produc5957510377907115898nteger_type,type,
    produc5957510377907115898nteger: $tType ).

thf(produc9181805145352861646it_nat_type,type,
    produc9181805145352861646it_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_Pr1607443439640623155t_bool_type,type,
    fun_Pr1607443439640623155t_bool: $tType ).

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

thf(fun_fu8778301040783821591l_bool_type,type,
    fun_fu8778301040783821591l_bool: $tType ).

thf(fun_fu4086510383517613953r_bool_type,type,
    fun_fu4086510383517613953r_bool: $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_fu4671764723984660721t_bool_type,type,
    fun_fu4671764723984660721t_bool: $tType ).

thf(fun_fu2749353902725170073t_bool_type,type,
    fun_fu2749353902725170073t_bool: $tType ).

thf(fun_fu1979049787525044581l_bool_type,type,
    fun_fu1979049787525044581l_bool: $tType ).

thf(fun_fu2194082084716825453t_bool_type,type,
    fun_fu2194082084716825453t_bool: $tType ).

thf(fun_fu6378668127007986697l_bool_type,type,
    fun_fu6378668127007986697l_bool: $tType ).

thf(set_fu233259321029537037t_bool_type,type,
    set_fu233259321029537037t_bool: $tType ).

thf(produc7253712600438629244nteger_type,type,
    produc7253712600438629244nteger: $tType ).

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

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

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

thf(set_Pr4407170740510854343l_bool_type,type,
    set_Pr4407170740510854343l_bool: $tType ).

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

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

thf(fun_se2235623607936449885t_bool_type,type,
    fun_se2235623607936449885t_bool: $tType ).

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

thf(set_Pr2764432955389651297at_nat_type,type,
    set_Pr2764432955389651297at_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_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(produc2721201938007151049ol_int_type,type,
    produc2721201938007151049ol_int: $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_fu8996758538364505415t_bool_type,type,
    fun_fu8996758538364505415t_bool: $tType ).

thf(fun_fu4222930702377173575t_bool_type,type,
    fun_fu4222930702377173575t_bool: $tType ).

thf(fun_fu1204527555220168225r_bool_type,type,
    fun_fu1204527555220168225r_bool: $tType ).

thf(fun_Pr7669129556548838760t_bool_type,type,
    fun_Pr7669129556548838760t_bool: $tType ).

thf(fun_Co6452804698976577951t_bool_type,type,
    fun_Co6452804698976577951t_bool: $tType ).

thf(fun_Co4766851469660149930t_bool_type,type,
    fun_Co4766851469660149930t_bool: $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_Pr1120495937353221654t_bool_type,type,
    fun_Pr1120495937353221654t_bool: $tType ).

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

thf(fun_se1534075524646452397t_bool_type,type,
    fun_se1534075524646452397t_bool: $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(produc3355007534958536139rm_int_type,type,
    produc3355007534958536139rm_int: $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(produc1429801123241496295l_bool_type,type,
    produc1429801123241496295l_bool: $tType ).

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

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

thf(fun_Co4057876674088285027e_term_type,type,
    fun_Co4057876674088285027e_term: $tType ).

thf(fun_Co6144393223146317464e_term_type,type,
    fun_Co6144393223146317464e_term: $tType ).

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

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

thf(produc8196147696116026881at_nat_type,type,
    produc8196147696116026881at_nat: $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(fun_fu6671593931043511003r_bool_type,type,
    fun_fu6671593931043511003r_bool: $tType ).

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

thf(fun_fu6897202038601531823t_bool_type,type,
    fun_fu6897202038601531823t_bool: $tType ).

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

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

thf(fun_Pr3593591750522180850l_bool_type,type,
    fun_Pr3593591750522180850l_bool: $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_fu2993381634879179267t_bool_type,type,
    fun_fu2993381634879179267t_bool: $tType ).

thf(fun_fu5815484198005934595t_bool_type,type,
    fun_fu5815484198005934595t_bool: $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_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_Pr2419607445322970330t_unit_type,type,
    fun_Pr2419607445322970330t_unit: $tType ).

thf(fun_fu4087525139388848025l_bool_type,type,
    fun_fu4087525139388848025l_bool: $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_fu7770211804340478819nteger_type,type,
    fun_fu7770211804340478819nteger: $tType ).

thf(fun_fu9160419385450930796l_bool_type,type,
    fun_fu9160419385450930796l_bool: $tType ).

thf(fun_Pr446604468264085555t_bool_type,type,
    fun_Pr446604468264085555t_bool: $tType ).

thf(fun_fu8715438531829836670t_bool_type,type,
    fun_fu8715438531829836670t_bool: $tType ).

thf(fun_fu5963139849246984042t_bool_type,type,
    fun_fu5963139849246984042t_bool: $tType ).

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

thf(fun_in3344392145425689243t_bool_type,type,
    fun_in3344392145425689243t_bool: $tType ).

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

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

thf(fun_fu7632120996380099260t_bool_type,type,
    fun_fu7632120996380099260t_bool: $tType ).

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

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

thf(fun_fu1860369457029301217at_nat_type,type,
    fun_fu1860369457029301217at_nat: $tType ).

thf(fun_na1334428713786062489t_bool_type,type,
    fun_na1334428713786062489t_bool: $tType ).

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

thf(fun_fu4917883025340107954m_bool_type,type,
    fun_fu4917883025340107954m_bool: $tType ).

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

thf(fun_in5459610092078544743e_term_type,type,
    fun_in5459610092078544743e_term: $tType ).

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

thf(fun_fu4935782767973721645l_bool_type,type,
    fun_fu4935782767973721645l_bool: $tType ).

thf(fun_fu618149979094779693l_bool_type,type,
    fun_fu618149979094779693l_bool: $tType ).

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

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

thf(fun_fu2880708205787085918r_bool_type,type,
    fun_fu2880708205787085918r_bool: $tType ).

thf(fun_fu7736802664756497485t_bool_type,type,
    fun_fu7736802664756497485t_bool: $tType ).

thf(fun_fu7943159151423750878r_bool_type,type,
    fun_fu7943159151423750878r_bool: $tType ).

thf(fun_fu263519691223904581n_bool_type,type,
    fun_fu263519691223904581n_bool: $tType ).

thf(fun_fu7255687391835202117r_bool_type,type,
    fun_fu7255687391835202117r_bool: $tType ).

thf(fun_Pr6921370099244678862t_bool_type,type,
    fun_Pr6921370099244678862t_bool: $tType ).

thf(set_fu6080891106736489294t_bool_type,type,
    set_fu6080891106736489294t_bool: $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_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(produc6714399278180371524it_nat_type,type,
    produc6714399278180371524it_nat: $tType ).

thf(fun_fu813382667476268716l_bool_type,type,
    fun_fu813382667476268716l_bool: $tType ).

thf(fun_fu9147942314745297866t_bool_type,type,
    fun_fu9147942314745297866t_bool: $tType ).

thf(fun_fu7718499123964418566l_bool_type,type,
    fun_fu7718499123964418566l_bool: $tType ).

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

thf(fun_Pr998545308806241276t_bool_type,type,
    fun_Pr998545308806241276t_bool: $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_fu3475476537176103381t_bool_type,type,
    fun_fu3475476537176103381t_bool: $tType ).

thf(fun_fu8159772421396582028t_bool_type,type,
    fun_fu8159772421396582028t_bool: $tType ).

thf(fun_fu7888190625410830553l_bool_type,type,
    fun_fu7888190625410830553l_bool: $tType ).

thf(fun_Pr9149712721152451482l_bool_type,type,
    fun_Pr9149712721152451482l_bool: $tType ).

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

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

thf(fun_Co8475707966591157134l_bool_type,type,
    fun_Co8475707966591157134l_bool: $tType ).

thf(fun_Co621691207274083130e_term_type,type,
    fun_Co621691207274083130e_term: $tType ).

thf(fun_Co3025358997185726883r_bool_type,type,
    fun_Co3025358997185726883r_bool: $tType ).

thf(fun_Co6545587727236015215e_term_type,type,
    fun_Co6545587727236015215e_term: $tType ).

thf(set_fu6991988656872959732e_term_type,type,
    set_fu6991988656872959732e_term: $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_fu4738270438141978787l_assn_type,type,
    fun_fu4738270438141978787l_assn: $tType ).

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

thf(fun_fu5583808879883784863r_bool_type,type,
    fun_fu5583808879883784863r_bool: $tType ).

thf(fun_fu3910677444521609704t_bool_type,type,
    fun_fu3910677444521609704t_bool: $tType ).

thf(fun_fu656925638523502036t_bool_type,type,
    fun_fu656925638523502036t_bool: $tType ).

thf(fun_fu3327874110432564095r_bool_type,type,
    fun_fu3327874110432564095r_bool: $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_fu7919257609373989805t_bool_type,type,
    fun_fu7919257609373989805t_bool: $tType ).

thf(fun_fu4802881585551670701t_bool_type,type,
    fun_fu4802881585551670701t_bool: $tType ).

thf(fun_Pr5837708615769641901m_bool_type,type,
    fun_Pr5837708615769641901m_bool: $tType ).

thf(fun_Pr248683899324676269t_bool_type,type,
    fun_Pr248683899324676269t_bool: $tType ).

thf(fun_Pr3099820731930151597t_bool_type,type,
    fun_Pr3099820731930151597t_bool: $tType ).

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

thf(fun_fu7550065535558868812t_bool_type,type,
    fun_fu7550065535558868812t_bool: $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(set_fu7420319347937486900t_bool_type,type,
    set_fu7420319347937486900t_bool: $tType ).

thf(fun_se2759736925585322443t_bool_type,type,
    fun_se2759736925585322443t_bool: $tType ).

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

thf(fun_na137915827363482383t_bool_type,type,
    fun_na137915827363482383t_bool: $tType ).

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

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

thf(fun_fu2407094525611807055l_bool_type,type,
    fun_fu2407094525611807055l_bool: $tType ).

thf(fun_fu103463476997428965r_bool_type,type,
    fun_fu103463476997428965r_bool: $tType ).

thf(fun_fu1953483166330056801r_bool_type,type,
    fun_fu1953483166330056801r_bool: $tType ).

thf(fun_fu2848896328290156587r_bool_type,type,
    fun_fu2848896328290156587r_bool: $tType ).

thf(fun_fu3307002049327355231l_bool_type,type,
    fun_fu3307002049327355231l_bool: $tType ).

thf(fun_fu1003371000712977141r_bool_type,type,
    fun_fu1003371000712977141r_bool: $tType ).

thf(fun_fu8654101865418439413r_bool_type,type,
    fun_fu8654101865418439413r_bool: $tType ).

thf(fun_fu9053932460070868135l_bool_type,type,
    fun_fu9053932460070868135l_bool: $tType ).

thf(fun_fu6750301411456490045r_bool_type,type,
    fun_fu6750301411456490045r_bool: $tType ).

thf(fun_fu4182656818893402597t_bool_type,type,
    fun_fu4182656818893402597t_bool: $tType ).

thf(fun_fu5383964687713931307m_bool_type,type,
    fun_fu5383964687713931307m_bool: $tType ).

thf(fun_fu4485664519118269941t_bool_type,type,
    fun_fu4485664519118269941t_bool: $tType ).

thf(fun_fu6362593152135629977t_bool_type,type,
    fun_fu6362593152135629977t_bool: $tType ).

thf(fun_fu8666999061116250429t_bool_type,type,
    fun_fu8666999061116250429t_bool: $tType ).

thf(fun_fu7173567273244385455n_bool_type,type,
    fun_fu7173567273244385455n_bool: $tType ).

thf(fun_Pr6001797050664311790t_bool_type,type,
    fun_Pr6001797050664311790t_bool: $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_Pr7622143378746182288t_bool_type,type,
    fun_Pr7622143378746182288t_bool: $tType ).

thf(fun_Pr1256881249384793578t_bool_type,type,
    fun_Pr1256881249384793578t_bool: $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_se2987382683605331715t_bool_type,type,
    fun_se2987382683605331715t_bool: $tType ).

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

thf(fun_fu1169456446961829174r_bool_type,type,
    fun_fu1169456446961829174r_bool: $tType ).

thf(fun_fu8671195345830221714r_bool_type,type,
    fun_fu8671195345830221714r_bool: $tType ).

thf(fun_fu8303122171908583641l_bool_type,type,
    fun_fu8303122171908583641l_bool: $tType ).

thf(fun_fu6470717055334781657l_bool_type,type,
    fun_fu6470717055334781657l_bool: $tType ).

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

thf(fun_in6429348457993719614e_term_type,type,
    fun_in6429348457993719614e_term: $tType ).

thf(fun_fu6757280373297557336ol_rat_type,type,
    fun_fu6757280373297557336ol_rat: $tType ).

thf(fun_fu6077215957461099344ol_nat_type,type,
    fun_fu6077215957461099344ol_nat: $tType ).

thf(fun_fu2549468117332453036ol_int_type,type,
    fun_fu2549468117332453036ol_int: $tType ).

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

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

thf(fun_fu2497601190693114531ol_rat_type,type,
    fun_fu2497601190693114531ol_rat: $tType ).

thf(fun_fu7012545734135022755ol_nat_type,type,
    fun_fu7012545734135022755ol_nat: $tType ).

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

thf(fun_fu4970875099359191043t_bool_type,type,
    fun_fu4970875099359191043t_bool: $tType ).

thf(fun_fu2583778531842586371t_bool_type,type,
    fun_fu2583778531842586371t_bool: $tType ).

thf(fun_fu691032689367502339t_bool_type,type,
    fun_fu691032689367502339t_bool: $tType ).

thf(fun_fu8657826108284254051nteger_type,type,
    fun_fu8657826108284254051nteger: $tType ).

thf(fun_fu911555637408580596l_assn_type,type,
    fun_fu911555637408580596l_assn: $tType ).

thf(fun_fu2971308621445215880t_bool_type,type,
    fun_fu2971308621445215880t_bool: $tType ).

thf(fun_fu9131882981303784088t_bool_type,type,
    fun_fu9131882981303784088t_bool: $tType ).

thf(fun_fu6608941571832801770n_bool_type,type,
    fun_fu6608941571832801770n_bool: $tType ).

thf(fun_fu2517660059135048810r_bool_type,type,
    fun_fu2517660059135048810r_bool: $tType ).

thf(fun_fu163127709195666036t_bool_type,type,
    fun_fu163127709195666036t_bool: $tType ).

thf(fun_fu3332619399063632157nteger_type,type,
    fun_fu3332619399063632157nteger: $tType ).

thf(fun_fu4454055256145563701r_bool_type,type,
    fun_fu4454055256145563701r_bool: $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_Pr4146916812029406451l_bool_type,type,
    fun_Pr4146916812029406451l_bool: $tType ).

thf(fun_op7552378328454751299t_bool_type,type,
    fun_op7552378328454751299t_bool: $tType ).

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

thf(fun_fu2868497722653781188t_bool_type,type,
    fun_fu2868497722653781188t_bool: $tType ).

thf(fun_in8019652204411901140t_bool_type,type,
    fun_in8019652204411901140t_bool: $tType ).

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

thf(fun_fu7205475995011387452t_bool_type,type,
    fun_fu7205475995011387452t_bool: $tType ).

thf(fun_Pr5765855711896469291t_bool_type,type,
    fun_Pr5765855711896469291t_bool: $tType ).

thf(fun_Pr7102264977413650527t_bool_type,type,
    fun_Pr7102264977413650527t_bool: $tType ).

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

thf(fun_na4786964484885125043t_bool_type,type,
    fun_na4786964484885125043t_bool: $tType ).

thf(fun_fu1432019548987072325l_bool_type,type,
    fun_fu1432019548987072325l_bool: $tType ).

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

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

thf(fun_fu2005298298577998622l_bool_type,type,
    fun_fu2005298298577998622l_bool: $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_fu8172925815900240338r_bool_type,type,
    fun_fu8172925815900240338r_bool: $tType ).

thf(fun_fu4845481189500184658m_bool_type,type,
    fun_fu4845481189500184658m_bool: $tType ).

thf(fun_fu3947181020904523292t_bool_type,type,
    fun_fu3947181020904523292t_bool: $tType ).

thf(fun_fu3841477750346251066t_bool_type,type,
    fun_fu3841477750346251066t_bool: $tType ).

thf(fun_fu8801565281860781890t_bool_type,type,
    fun_fu8801565281860781890t_bool: $tType ).

thf(fun_fu1882599153986626534t_bool_type,type,
    fun_fu1882599153986626534t_bool: $tType ).

thf(fun_fu4602447751791859039n_bool_type,type,
    fun_fu4602447751791859039n_bool: $tType ).

thf(fun_fu7935292571462080722r_bool_type,type,
    fun_fu7935292571462080722r_bool: $tType ).

thf(fun_fu2505595494136404892r_bool_type,type,
    fun_fu2505595494136404892r_bool: $tType ).

thf(fun_fu5114706524692223720r_assn_type,type,
    fun_fu5114706524692223720r_assn: $tType ).

thf(fun_fu2342990897131189674r_bool_type,type,
    fun_fu2342990897131189674r_bool: $tType ).

thf(fun_fu8023496675954067791t_bool_type,type,
    fun_fu8023496675954067791t_bool: $tType ).

thf(fun_fu8326504376178935135t_bool_type,type,
    fun_fu8326504376178935135t_bool: $tType ).

thf(fun_fu3284466881322139815t_bool_type,type,
    fun_fu3284466881322139815t_bool: $tType ).

thf(fun_se4340818509347730467r_bool_type,type,
    fun_se4340818509347730467r_bool: $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_Pr4343998633453697049at_nat_type,type,
    fun_Pr4343998633453697049at_nat: $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(set_Pr5877625034052425863t_bool_type,type,
    set_Pr5877625034052425863t_bool: $tType ).

thf(fun_se4502155409561472834t_bool_type,type,
    fun_se4502155409561472834t_bool: $tType ).

thf(fun_na2866682563581395078t_bool_type,type,
    fun_na2866682563581395078t_bool: $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_fu624093908337759363nteger_type,type,
    fun_fu624093908337759363nteger: $tType ).

thf(fun_fu3065856773340909731l_assn_type,type,
    fun_fu3065856773340909731l_assn: $tType ).

thf(fun_fu9052069482527730051r_bool_type,type,
    fun_fu9052069482527730051r_bool: $tType ).

thf(fun_se8003769888451347523t_bool_type,type,
    fun_se8003769888451347523t_bool: $tType ).

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

thf(fun_fu1628656120428507393t_bool_type,type,
    fun_fu1628656120428507393t_bool: $tType ).

thf(fun_fu9206144150172078255t_bool_type,type,
    fun_fu9206144150172078255t_bool: $tType ).

thf(fun_fu4942859644831833271t_bool_type,type,
    fun_fu4942859644831833271t_bool: $tType ).

thf(fun_fu7247265553812453723t_bool_type,type,
    fun_fu7247265553812453723t_bool: $tType ).

thf(fun_fu1107212216887061754r_bool_type,type,
    fun_fu1107212216887061754r_bool: $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_Pr8936557182701289977t_bool_type,type,
    fun_Pr8936557182701289977t_bool: $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(set_Pr3900213285448270941t_bool_type,type,
    set_Pr3900213285448270941t_bool: $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_se4380561871771826905t_bool_type,type,
    fun_se4380561871771826905t_bool: $tType ).

thf(fun_Pr5591635095200564269t_bool_type,type,
    fun_Pr5591635095200564269t_bool: $tType ).

thf(fun_Pr6106755111087548649l_bool_type,type,
    fun_Pr6106755111087548649l_bool: $tType ).

thf(fun_Pr3195429412498512255r_bool_type,type,
    fun_Pr3195429412498512255r_bool: $tType ).

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

thf(fun_Co7333321365496032713r_bool_type,type,
    fun_Co7333321365496032713r_bool: $tType ).

thf(option2888707425368387221e_term_type,type,
    option2888707425368387221e_term: $tType ).

thf(fun_fu2423223891319671405l_bool_type,type,
    fun_fu2423223891319671405l_bool: $tType ).

thf(fun_fu4271301222718411977l_bool_type,type,
    fun_fu4271301222718411977l_bool: $tType ).

thf(fun_fu4183260555072782609l_bool_type,type,
    fun_fu4183260555072782609l_bool: $tType ).

thf(fun_fu6031337886471523181l_bool_type,type,
    fun_fu6031337886471523181l_bool: $tType ).

thf(fun_fu5827305053654988013l_bool_type,type,
    fun_fu5827305053654988013l_bool: $tType ).

thf(fun_fu7925731147167280621l_bool_type,type,
    fun_fu7925731147167280621l_bool: $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_fu3661257360345122130t_bool_type,type,
    fun_fu3661257360345122130t_bool: $tType ).

thf(fun_fu415885379153147766l_bool_type,type,
    fun_fu415885379153147766l_bool: $tType ).

thf(fun_fu2263962710551888338l_bool_type,type,
    fun_fu2263962710551888338l_bool: $tType ).

thf(fun_fu2066853804478883246t_bool_type,type,
    fun_fu2066853804478883246t_bool: $tType ).

thf(fun_fu4978346893710585036t_bool_type,type,
    fun_fu4978346893710585036t_bool: $tType ).

thf(fun_fu5021329701880750916ol_rat_type,type,
    fun_fu5021329701880750916ol_rat: $tType ).

thf(fun_fu7591486775136386543t_bool_type,type,
    fun_fu7591486775136386543t_bool: $tType ).

thf(fun_fu7894494475361253887t_bool_type,type,
    fun_fu7894494475361253887t_bool: $tType ).

thf(fun_fu2852456980504458567t_bool_type,type,
    fun_fu2852456980504458567t_bool: $tType ).

thf(fun_fu9051297857939674819t_bool_type,type,
    fun_fu9051297857939674819t_bool: $tType ).

thf(fun_fu2152406035679163771m_bool_type,type,
    fun_fu2152406035679163771m_bool: $tType ).

thf(fun_fu5667648569235554815t_bool_type,type,
    fun_fu5667648569235554815t_bool: $tType ).

thf(fun_fu5970656269460422159t_bool_type,type,
    fun_fu5970656269460422159t_bool: $tType ).

thf(fun_fu928618774603626839t_bool_type,type,
    fun_fu928618774603626839t_bool: $tType ).

thf(fun_fu3517420029717861571m_bool_type,type,
    fun_fu3517420029717861571m_bool: $tType ).

thf(fun_fu7335670263499119959t_bool_type,type,
    fun_fu7335670263499119959t_bool: $tType ).

thf(fun_fu3983462749191356743t_bool_type,type,
    fun_fu3983462749191356743t_bool: $tType ).

thf(fun_fu4286470449416224087t_bool_type,type,
    fun_fu4286470449416224087t_bool: $tType ).

thf(fun_fu8467804991414204575t_bool_type,type,
    fun_fu8467804991414204575t_bool: $tType ).

thf(fun_na5642534631560016699t_bool_type,type,
    fun_na5642534631560016699t_bool: $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_fu8238123566048827017t_bool_type,type,
    fun_fu8238123566048827017t_bool: $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_op5700337305840942333t_bool_type,type,
    fun_op5700337305840942333t_bool: $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(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_fu5641360819561228055l_bool_type,type,
    fun_fu5641360819561228055l_bool: $tType ).

thf(fun_op1962577433978643573m_bool_type,type,
    fun_op1962577433978643573m_bool: $tType ).

thf(fun_na2338080690716861136at_nat_type,type,
    fun_na2338080690716861136at_nat: $tType ).

thf(fun_he5369522480449343229at_nat_type,type,
    fun_he5369522480449343229at_nat: $tType ).

thf(set_Pr3642346839158376647t_bool_type,type,
    set_Pr3642346839158376647t_bool: $tType ).

thf(produc311630390117187751t_bool_type,type,
    produc311630390117187751t_bool: $tType ).

thf(fun_fu4450724535874491238ol_nat_type,type,
    fun_fu4450724535874491238ol_nat: $tType ).

thf(fun_fu440503751160241048t_bool_type,type,
    fun_fu440503751160241048t_bool: $tType ).

thf(fun_fu8137823980273323508t_bool_type,type,
    fun_fu8137823980273323508t_bool: $tType ).

thf(fun_fu7290527928208356451l_bool_type,type,
    fun_fu7290527928208356451l_bool: $tType ).

thf(fun_Pr5932607294251420486t_bool_type,type,
    fun_Pr5932607294251420486t_bool: $tType ).

thf(fun_Pr3145601080792579042t_bool_type,type,
    fun_Pr3145601080792579042t_bool: $tType ).

thf(fun_op3323321805596408808on_num_type,type,
    fun_op3323321805596408808on_num: $tType ).

thf(fun_na4827981024643048934t_bool_type,type,
    fun_na4827981024643048934t_bool: $tType ).

thf(fun_fu6596549469508991942l_bool_type,type,
    fun_fu6596549469508991942l_bool: $tType ).

thf(fun_fu7491883331029180450l_bool_type,type,
    fun_fu7491883331029180450l_bool: $tType ).

thf(fun_fu1925869420691536157nteger_type,type,
    fun_fu1925869420691536157nteger: $tType ).

thf(fun_fu3953527911151619997l_bool_type,type,
    fun_fu3953527911151619997l_bool: $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_fu4239984933745482083t_bool_type,type,
    fun_fu4239984933745482083t_bool: $tType ).

thf(fun_fu4708731997093370859l_bool_type,type,
    fun_fu4708731997093370859l_bool: $tType ).

thf(fun_fu2185298426232596579t_bool_type,type,
    fun_fu2185298426232596579t_bool: $tType ).

thf(fun_fu3561611792623449554r_bool_type,type,
    fun_fu3561611792623449554r_bool: $tType ).

thf(fun_fu6099815659852790435ol_rat_type,type,
    fun_fu6099815659852790435ol_rat: $tType ).

thf(fun_fu9149972526633946275ol_nat_type,type,
    fun_fu9149972526633946275ol_nat: $tType ).

thf(fun_fu574094095068873155l_assn_type,type,
    fun_fu574094095068873155l_assn: $tType ).

thf(fun_fu4744316281005729766t_bool_type,type,
    fun_fu4744316281005729766t_bool: $tType ).

thf(fun_fu8578555381889756298t_bool_type,type,
    fun_fu8578555381889756298t_bool: $tType ).

thf(fun_fu3002462811980898909nteger_type,type,
    fun_fu3002462811980898909nteger: $tType ).

thf(fun_fu9135849066224463439t_bool_type,type,
    fun_fu9135849066224463439t_bool: $tType ).

thf(fun_fu43864654242307886t_bool_type,type,
    fun_fu43864654242307886t_bool: $tType ).

thf(fun_fu3878103755126334418t_bool_type,type,
    fun_fu3878103755126334418t_bool: $tType ).

thf(fun_fu4771103787859698525nteger_type,type,
    fun_fu4771103787859698525nteger: $tType ).

thf(fun_fu4435397439461041559t_bool_type,type,
    fun_fu4435397439461041559t_bool: $tType ).

thf(fun_Pr7397166214287566974on_num_type,type,
    fun_Pr7397166214287566974on_num: $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(produc6653097349344004940it_nat_type,type,
    produc6653097349344004940it_nat: $tType ).

thf(produc2215549255670290429t_bool_type,type,
    produc2215549255670290429t_bool: $tType ).

thf(fun_Pr1511622319146086153t_bool_type,type,
    fun_Pr1511622319146086153t_bool: $tType ).

thf(fun_Pr7588271929612197001t_bool_type,type,
    fun_Pr7588271929612197001t_bool: $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_Pr292408699144966967t_unit_type,type,
    fun_Pr292408699144966967t_unit: $tType ).

thf(fun_li8598321315282354825t_bool_type,type,
    fun_li8598321315282354825t_bool: $tType ).

thf(set_Pr5094982260447487303t_unit_type,type,
    set_Pr5094982260447487303t_unit: $tType ).

thf(set_mu2057375006010111271at_nat_type,type,
    set_mu2057375006010111271at_nat: $tType ).

thf(fun_se8074476271188067385t_bool_type,type,
    fun_se8074476271188067385t_bool: $tType ).

thf(fun_Pr5924905948197006361rray_a_type,type,
    fun_Pr5924905948197006361rray_a: $tType ).

thf(fun_Pr5897280058523175033t_bool_type,type,
    fun_Pr5897280058523175033t_bool: $tType ).

thf(fun_Pr7583502776308271041t_bool_type,type,
    fun_Pr7583502776308271041t_bool: $tType ).

thf(fun_op4521932154746760340nteger_type,type,
    fun_op4521932154746760340nteger: $tType ).

thf(fun_ar1074044450438384043t_unit_type,type,
    fun_ar1074044450438384043t_unit: $tType ).

thf(set_fu1284235700437306831t_bool_type,type,
    set_fu1284235700437306831t_bool: $tType ).

thf(fun_fu2358325754833327848l_assn_type,type,
    fun_fu2358325754833327848l_assn: $tType ).

thf(fun_fu8340641457845911400l_bool_type,type,
    fun_fu8340641457845911400l_bool: $tType ).

thf(fun_se4097146774670233028at_nat_type,type,
    fun_se4097146774670233028at_nat: $tType ).

thf(fun_se9142667792015812128at_int_type,type,
    fun_se9142667792015812128at_int: $tType ).

thf(fun_se7698381193922241133t_bool_type,type,
    fun_se7698381193922241133t_bool: $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_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_se6063655520620159884t_bool_type,type,
    fun_se6063655520620159884t_bool: $tType ).

thf(fun_se7940584153637519920t_bool_type,type,
    fun_se7940584153637519920t_bool: $tType ).

thf(fun_he5123621388056232515t_unit_type,type,
    fun_he5123621388056232515t_unit: $tType ).

thf(fun_fu6395640590628241448t_assn_type,type,
    fun_fu6395640590628241448t_assn: $tType ).

thf(fun_fu6838017323210031556t_bool_type,type,
    fun_fu6838017323210031556t_bool: $tType ).

thf(fun_fu4854284890850328872t_assn_type,type,
    fun_fu4854284890850328872t_assn: $tType ).

thf(fun_fu420584378438320396t_bool_type,type,
    fun_fu420584378438320396t_bool: $tType ).

thf(fun_fu1032279790925302627l_bool_type,type,
    fun_fu1032279790925302627l_bool: $tType ).

thf(fun_fu7344326129191042041r_bool_type,type,
    fun_fu7344326129191042041r_bool: $tType ).

thf(fun_se707272970763642173t_bool_type,type,
    fun_se707272970763642173t_bool: $tType ).

thf(fun_se8186231001398342275et_nat_type,type,
    fun_se8186231001398342275et_nat: $tType ).

thf(fun_se6049520964208396421t_bool_type,type,
    fun_se6049520964208396421t_bool: $tType ).

thf(fun_se6410524667074557315et_int_type,type,
    fun_se6410524667074557315et_int: $tType ).

thf(fun_he7369252872201260279rray_a_type,type,
    fun_he7369252872201260279rray_a: $tType ).

thf(fun_Co9170264581657726457l_bool_type,type,
    fun_Co9170264581657726457l_bool: $tType ).

thf(fun_Co8310303586393106575r_bool_type,type,
    fun_Co8310303586393106575r_bool: $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_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(produc6172120975061646567t_bool_type,type,
    produc6172120975061646567t_bool: $tType ).

thf(fun_fu7925023953348749699l_bool_type,type,
    fun_fu7925023953348749699l_bool: $tType ).

thf(fun_li1191372448985611379st_nat_type,type,
    fun_li1191372448985611379st_nat: $tType ).

thf(fun_fu6678276313180071960l_bool_type,type,
    fun_fu6678276313180071960l_bool: $tType ).

thf(fun_fu913567913430682128l_bool_type,type,
    fun_fu913567913430682128l_bool: $tType ).

thf(fun_fu7923017422675304344ol_rat_type,type,
    fun_fu7923017422675304344ol_rat: $tType ).

thf(fun_se5063566521941538468t_bool_type,type,
    fun_se5063566521941538468t_bool: $tType ).

thf(fun_Pr5562079387306038061t_bool_type,type,
    fun_Pr5562079387306038061t_bool: $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_fu3889889255038636099t_bool_type,type,
    fun_fu3889889255038636099t_bool: $tType ).

thf(fun_fu3429606303391989479t_bool_type,type,
    fun_fu3429606303391989479t_bool: $tType ).

thf(fun_fu7812315824552436429l_bool_type,type,
    fun_fu7812315824552436429l_bool: $tType ).

thf(fun_fu437021119096401193l_bool_type,type,
    fun_fu437021119096401193l_bool: $tType ).

thf(fun_fu8282352254069530783t_bool_type,type,
    fun_fu8282352254069530783t_bool: $tType ).

thf(fun_fu7822069302422884163t_bool_type,type,
    fun_fu7822069302422884163t_bool: $tType ).

thf(fun_fu7257246399608679363ol_rat_type,type,
    fun_fu7257246399608679363ol_rat: $tType ).

thf(fun_fu560003646518074819ol_nat_type,type,
    fun_fu560003646518074819ol_nat: $tType ).

thf(fun_fu4461748213934612163ol_int_type,type,
    fun_fu4461748213934612163ol_int: $tType ).

thf(fun_se1018900654481025269at_int_type,type,
    fun_se1018900654481025269at_int: $tType ).

thf(fun_fu3052598110916186900t_bool_type,type,
    fun_fu3052598110916186900t_bool: $tType ).

thf(fun_fu8422113094057456412t_bool_type,type,
    fun_fu8422113094057456412t_bool: $tType ).

thf(fun_fu2739651132436891864at_rat_type,type,
    fun_fu2739651132436891864at_rat: $tType ).

thf(fun_fu8816475899675864456nt_int_type,type,
    fun_fu8816475899675864456nt_int: $tType ).

thf(fun_fu2537230888636918854t_bool_type,type,
    fun_fu2537230888636918854t_bool: $tType ).

thf(fun_fu578352292277294322t_bool_type,type,
    fun_fu578352292277294322t_bool: $tType ).

thf(fun_fu337402001079966300t_bool_type,type,
    fun_fu337402001079966300t_bool: $tType ).

thf(fun_fu3335655611361370724t_bool_type,type,
    fun_fu3335655611361370724t_bool: $tType ).

thf(fun_fu2875372659714724104t_bool_type,type,
    fun_fu2875372659714724104t_bool: $tType ).

thf(fun_fu6561562741486290476nt_int_type,type,
    fun_fu6561562741486290476nt_int: $tType ).

thf(fun_se1079088094581925575nteger_type,type,
    fun_se1079088094581925575nteger: $tType ).

thf(fun_se1983639173573402599r_bool_type,type,
    fun_se1983639173573402599r_bool: $tType ).

thf(fun_na3408937105440547634t_bool_type,type,
    fun_na3408937105440547634t_bool: $tType ).

thf(fun_Co7255140290867716100n_bool_type,type,
    fun_Co7255140290867716100n_bool: $tType ).

thf(fun_as8999054211979400836r_bool_type,type,
    fun_as8999054211979400836r_bool: $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_se4632457686525064013t_bool_type,type,
    fun_se4632457686525064013t_bool: $tType ).

thf(fun_Pr4298194452408323251l_bool_type,type,
    fun_Pr4298194452408323251l_bool: $tType ).

thf(fun_op8268937810890488579n_bool_type,type,
    fun_op8268937810890488579n_bool: $tType ).

thf(fun_nu1049378303802735384on_num_type,type,
    fun_nu1049378303802735384on_num: $tType ).

thf(fun_na7595719129879163854on_num_type,type,
    fun_na7595719129879163854on_num: $tType ).

thf(fun_he6201055237484778573t_bool_type,type,
    fun_he6201055237484778573t_bool: $tType ).

thf(fun_bo8995055541810095699l_bool_type,type,
    fun_bo8995055541810095699l_bool: $tType ).

thf(fun_se1823139391991869964it_int_type,type,
    fun_se1823139391991869964it_int: $tType ).

thf(fun_Pr7964958863114788660l_bool_type,type,
    fun_Pr7964958863114788660l_bool: $tType ).

thf(fun_Pr4750396477255587728l_bool_type,type,
    fun_Pr4750396477255587728l_bool: $tType ).

thf(fun_Pr5871044560531976592m_bool_type,type,
    fun_Pr5871044560531976592m_bool: $tType ).

thf(fun_Pr2676864523822355546t_bool_type,type,
    fun_Pr2676864523822355546t_bool: $tType ).

thf(fun_Pr2216581572175708926t_bool_type,type,
    fun_Pr2216581572175708926t_bool: $tType ).

thf(fun_na8669532458821385046t_unit_type,type,
    fun_na8669532458821385046t_unit: $tType ).

thf(multis2468970476368604999at_nat_type,type,
    multis2468970476368604999at_nat: $tType ).

thf(fun_Pr7757163693017731481t_bool_type,type,
    fun_Pr7757163693017731481t_bool: $tType ).

thf(fun_Pr6621378678513976329ol_nat_type,type,
    fun_Pr6621378678513976329ol_nat: $tType ).

thf(fun_Pr803113274115125473t_bool_type,type,
    fun_Pr803113274115125473t_bool: $tType ).

thf(fun_Pr5173132228603596041ol_int_type,type,
    fun_Pr5173132228603596041ol_int: $tType ).

thf(fun_Pr3947323014689170787at_nat_type,type,
    fun_Pr3947323014689170787at_nat: $tType ).

thf(fun_Pr1956393569872995867nt_int_type,type,
    fun_Pr1956393569872995867nt_int: $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_se689384475314470797l_bool_type,type,
    fun_se689384475314470797l_bool: $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_na5614638261385347865t_bool_type,type,
    fun_na5614638261385347865t_bool: $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_li4440390755235668505t_bool_type,type,
    fun_li4440390755235668505t_bool: $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_fu6037878657194187132r_bool_type,type,
    fun_fu6037878657194187132r_bool: $tType ).

thf(fun_fu5996436995312922950r_bool_type,type,
    fun_fu5996436995312922950r_bool: $tType ).

thf(fun_se5532715864020165650l_assn_type,type,
    fun_se5532715864020165650l_assn: $tType ).

thf(fun_se680526843285281907t_bool_type,type,
    fun_se680526843285281907t_bool: $tType ).

thf(fun_se6612071603986899387t_bool_type,type,
    fun_se6612071603986899387t_bool: $tType ).

thf(fun_ra3472770382387731017l_bool_type,type,
    fun_ra3472770382387731017l_bool: $tType ).

thf(fun_ra3920053733784048596r_bool_type,type,
    fun_ra3920053733784048596r_bool: $tType ).

thf(fun_nu7693283004202570770r_bool_type,type,
    fun_nu7693283004202570770r_bool: $tType ).

thf(fun_na7327111457444404817l_bool_type,type,
    fun_na7327111457444404817l_bool: $tType ).

thf(fun_na7774394808840722396r_bool_type,type,
    fun_na7774394808840722396r_bool: $tType ).

thf(fun_in5072198299254830837l_bool_type,type,
    fun_in5072198299254830837l_bool: $tType ).

thf(fun_in5519481650651148416r_bool_type,type,
    fun_in5519481650651148416r_bool: $tType ).

thf(fun_Co6299454908631939665t_bool_type,type,
    fun_Co6299454908631939665t_bool: $tType ).

thf(fun_Co1273160911715153748t_bool_type,type,
    fun_Co1273160911715153748t_bool: $tType ).

thf(fun_Co2628172630834177170m_bool_type,type,
    fun_Co2628172630834177170m_bool: $tType ).

thf(fun_Co8657364630979331932t_bool_type,type,
    fun_Co8657364630979331932t_bool: $tType ).

thf(fun_Co8197081679332685312t_bool_type,type,
    fun_Co8197081679332685312t_bool: $tType ).

thf(fun_as6968651184343528707l_assn_type,type,
    fun_as6968651184343528707l_assn: $tType ).

thf(fun_as7903617535776176121n_bool_type,type,
    fun_as7903617535776176121n_bool: $tType ).

thf(set_fu8461242576058140809t_bool_type,type,
    set_fu8461242576058140809t_bool: $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_Pr2016573684049775267l_bool_type,type,
    fun_Pr2016573684049775267l_bool: $tType ).

thf(fun_bo5015163935410701111t_bool_type,type,
    fun_bo5015163935410701111t_bool: $tType ).

thf(fun_bo6580201250007910272et_nat_type,type,
    fun_bo6580201250007910272et_nat: $tType ).

thf(fun_na8554444051656733274t_bool_type,type,
    fun_na8554444051656733274t_bool: $tType ).

thf(fun_na896109329399166627et_nat_type,type,
    fun_na896109329399166627et_nat: $tType ).

thf(fun_in539189147730337462t_bool_type,type,
    fun_in539189147730337462t_bool: $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_ra5613769993463817465it_rat_type,type,
    fun_ra5613769993463817465it_rat: $tType ).

thf(set_se7118615804146677933t_unit_type,type,
    set_se7118615804146677933t_unit: $tType ).

thf(set_Pr8621012493645324487l_bool_type,type,
    set_Pr8621012493645324487l_bool: $tType ).

thf(fun_bo7981523287216768959t_unit_type,type,
    fun_bo7981523287216768959t_unit: $tType ).

thf(set_Pr4681767519595310322t_bool_type,type,
    set_Pr4681767519595310322t_bool: $tType ).

thf(set_Pr4221484567948663702t_bool_type,type,
    set_Pr4221484567948663702t_bool: $tType ).

thf(set_Pr2857216852229407126ol_num_type,type,
    set_Pr2857216852229407126ol_num: $tType ).

thf(set_Pr7141997262790060364ol_nat_type,type,
    set_Pr7141997262790060364ol_nat: $tType ).

thf(set_Pr4651914117858333608ol_int_type,type,
    set_Pr4651914117858333608ol_int: $tType ).

thf(produc7417142470700560111r_bool_type,type,
    produc7417142470700560111r_bool: $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_se1093428521897753731t_bool_type,type,
    fun_se1093428521897753731t_bool: $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_set_set_nat_bool_type,type,
    fun_set_set_nat_bool: $tType ).

thf(fun_set_set_int_bool_type,type,
    fun_set_set_int_bool: $tType ).

thf(fun_set_set_bool_rat_type,type,
    fun_set_set_bool_rat: $tType ).

thf(fun_set_set_bool_nat_type,type,
    fun_set_set_bool_nat: $tType ).

thf(fun_se5060747272260719591nteger_type,type,
    fun_se5060747272260719591nteger: $tType ).

thf(fun_se2712834123562403997r_bool_type,type,
    fun_se2712834123562403997r_bool: $tType ).

thf(fun_bo8700639080905871165nteger_type,type,
    fun_bo8700639080905871165nteger: $tType ).

thf(fun_as5024076178902890825t_bool_type,type,
    fun_as5024076178902890825t_bool: $tType ).

thf(fun_as3184907861312293201t_bool_type,type,
    fun_as3184907861312293201t_bool: $tType ).

thf(fun_as2724624909665646581t_bool_type,type,
    fun_as2724624909665646581t_bool: $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(set_option_set_nat_type,type,
    set_option_set_nat: $tType ).

thf(set_op687863988967635939nteger_type,type,
    set_op687863988967635939nteger: $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_bo1841576699660343469l_bool_type,type,
    fun_bo1841576699660343469l_bool: $tType ).

thf(set_op3165557761946182707t_unit_type,type,
    set_op3165557761946182707t_unit: $tType ).

thf(option8137458692691377843t_unit_type,type,
    option8137458692691377843t_unit: $tType ).

thf(fun_fu7168253649841883962l_bool_type,type,
    fun_fu7168253649841883962l_bool: $tType ).

thf(fun_fu3953691263982683030l_bool_type,type,
    fun_fu3953691263982683030l_bool: $tType ).

thf(fun_Pr2191293291710260995t_unit_type,type,
    fun_Pr2191293291710260995t_unit: $tType ).

thf(fun_na9137082442855928016l_bool_type,type,
    fun_na9137082442855928016l_bool: $tType ).

thf(fun_in3865155034416861484l_bool_type,type,
    fun_in3865155034416861484l_bool: $tType ).

thf(fun_bo3288154511880838028t_bool_type,type,
    fun_bo3288154511880838028t_bool: $tType ).

thf(set_set_list_nat_type,type,
    set_set_list_nat: $tType ).

thf(fun_fun_rat_rat_bool_type,type,
    fun_fun_rat_rat_bool: $tType ).

thf(fun_fun_num_int_bool_type,type,
    fun_fun_num_int_bool: $tType ).

thf(fun_fun_nat_num_bool_type,type,
    fun_fun_nat_num_bool: $tType ).

thf(fun_fun_nat_nat_bool_type,type,
    fun_fun_nat_nat_bool: $tType ).

thf(fun_fun_int_rat_bool_type,type,
    fun_fun_int_rat_bool: $tType ).

thf(fun_fun_int_num_bool_type,type,
    fun_fun_int_num_bool: $tType ).

thf(fun_fun_int_nat_bool_type,type,
    fun_fun_int_nat_bool: $tType ).

thf(fun_fun_int_int_bool_type,type,
    fun_fun_int_int_bool: $tType ).

thf(fun_set_bool_assn_type,type,
    fun_set_bool_assn: $tType ).

thf(fun_rat_fun_rat_bool_type,type,
    fun_rat_fun_rat_bool: $tType ).

thf(fun_rat_fun_nat_bool_type,type,
    fun_rat_fun_nat_bool: $tType ).

thf(fun_rat_fun_int_bool_type,type,
    fun_rat_fun_int_bool: $tType ).

thf(fun_rat_fun_bool_rat_type,type,
    fun_rat_fun_bool_rat: $tType ).

thf(fun_num_fun_num_bool_type,type,
    fun_num_fun_num_bool: $tType ).

thf(fun_num_fun_int_bool_type,type,
    fun_num_fun_int_bool: $tType ).

thf(fun_nat_fun_rat_bool_type,type,
    fun_nat_fun_rat_bool: $tType ).

thf(fun_nat_fun_nat_bool_type,type,
    fun_nat_fun_nat_bool: $tType ).

thf(fun_nat_fun_int_bool_type,type,
    fun_nat_fun_int_bool: $tType ).

thf(fun_int_fun_rat_bool_type,type,
    fun_int_fun_rat_bool: $tType ).

thf(fun_int_fun_num_bool_type,type,
    fun_int_fun_num_bool: $tType ).

thf(fun_int_fun_nat_bool_type,type,
    fun_int_fun_nat_bool: $tType ).

thf(fun_int_fun_int_bool_type,type,
    fun_int_fun_int_bool: $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_option_bool_bool_type,type,
    fun_option_bool_bool: $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_bool_option_bool_type,type,
    fun_bool_option_bool: $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_option_num_bool_type,type,
    fun_option_num_bool: $tType ).

thf(fun_bool_option_num_type,type,
    fun_bool_option_num: $tType ).

thf(option_fun_nat_bool_type,type,
    option_fun_nat_bool: $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_Pr6626665806141890376t_assn_type,type,
    fun_Pr6626665806141890376t_assn: $tType ).

thf(set_set_Product_unit_type,type,
    set_set_Product_unit: $tType ).

thf(produc2804947525362035943l_bool_type,type,
    produc2804947525362035943l_bool: $tType ).

thf(heap_e7401611519738050253t_unit_type,type,
    heap_e7401611519738050253t_unit: $tType ).

thf(produc8000372497851584572t_bool_type,type,
    produc8000372497851584572t_bool: $tType ).

thf(produc4876081531382960352t_bool_type,type,
    produc4876081531382960352t_bool: $tType ).

thf(produc1275348365150041824ol_num_type,type,
    produc1275348365150041824ol_num: $tType ).

thf(produc567104428201204118ol_nat_type,type,
    produc567104428201204118ol_nat: $tType ).

thf(produc5612625445546783218ol_int_type,type,
    produc5612625445546783218ol_int: $tType ).

thf(fun_list_nat_bool_type,type,
    fun_list_nat_bool: $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(fun_bool_set_bool_type,type,
    fun_bool_set_bool: $tType ).

thf(fun_set_nat_bool_type,type,
    fun_set_nat_bool: $tType ).

thf(fun_set_int_bool_type,type,
    fun_set_int_bool: $tType ).

thf(fun_set_bool_rat_type,type,
    fun_set_bool_rat: $tType ).

thf(fun_set_bool_nat_type,type,
    fun_set_bool_nat: $tType ).

thf(fun_nat_set_bool_type,type,
    fun_nat_set_bool: $tType ).

thf(fun_int_set_bool_type,type,
    fun_int_set_bool: $tType ).

thf(fun_bool_set_nat_type,type,
    fun_bool_set_nat: $tType ).

thf(fun_bool_set_int_type,type,
    fun_bool_set_int: $tType ).

thf(fun_bo7282069421189217543nteger_type,type,
    fun_bo7282069421189217543nteger: $tType ).

thf(fun_Co7175331531449502024l_bool_type,type,
    fun_Co7175331531449502024l_bool: $tType ).

thf(fun_Co8822979462182099027r_bool_type,type,
    fun_Co8822979462182099027r_bool: $tType ).

thf(set_fun_nat_bool_type,type,
    set_fun_nat_bool: $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_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(set_option_bool_type,type,
    set_option_bool: $tType ).

thf(option_set_bool_type,type,
    option_set_bool: $tType ).

thf(fun_Pr1572506220757514509t_bool_type,type,
    fun_Pr1572506220757514509t_bool: $tType ).

thf(fun_bo1891391082718140537t_unit_type,type,
    fun_bo1891391082718140537t_unit: $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_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_nat_Product_unit_type,type,
    fun_nat_Product_unit: $tType ).

thf(fun_int_Product_unit_type,type,
    fun_int_Product_unit: $tType ).

thf(fun_array_a_bool_type,type,
    fun_array_a_bool: $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(fun_bool_assn_type,type,
    fun_bool_assn: $tType ).

thf(fun_assn_bool_type,type,
    fun_assn_bool: $tType ).

thf(set_set_bool_type,type,
    set_set_bool: $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(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(ref_array_a_type,type,
    ref_array_a: $tType ).

thf(fun_bool_bool_type,type,
    fun_bool_bool: $tType ).

thf(fun_rat_bool_type,type,
    fun_rat_bool: $tType ).

thf(fun_num_bool_type,type,
    fun_num_bool: $tType ).

thf(fun_nat_bool_type,type,
    fun_nat_bool: $tType ).

thf(fun_int_bool_type,type,
    fun_int_bool: $tType ).

thf(fun_bool_rat_type,type,
    fun_bool_rat: $tType ).

thf(fun_bool_nat_type,type,
    fun_bool_nat: $tType ).

thf(fun_bool_int_type,type,
    fun_bool_int: $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(option_bool_type,type,
    option_bool: $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(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_bool_type,type,
    set_bool: $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(product_unit_type,type,
    product_unit: $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(char_type,type,
    char: $tType ).

thf(bool_type,type,
    bool: $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_he6201055237484778573t_bool ).

thf(none_P2587165478634041381it_nat_decl,type,
    none_P2587165478634041381it_nat: option3216581401566546698it_nat ).

thf(aa_hea1793595068369496646t_bool_decl,type,
    aa_hea1793595068369496646t_bool: fun_he6201055237484778573t_bool > heap_e7401611519738050253t_unit > bool ).

thf(aa_hea5936688510613671481it_nat_decl,type,
    aa_hea5936688510613671481it_nat: fun_he1504492240061592256it_nat > heap_e7401611519738050253t_unit > option3216581401566546698it_nat ).

thf(pp_decl,type,
    pp: bool > $o ).

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/sandbox2/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(60,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(61,plain,
    ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
    = none_P2587165478634041381it_nat ),
    inference(polarity_switch,[status(thm)],[60]) ).

thf(62,plain,
    ( ( h @ ( xs @ array_of_list_a @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
    = none_P2587165478634041381it_nat ),
    inference(lifteq,[status(thm)],[61]) ).

thf(6,axiom,
    ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
      ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp )
    <=> ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_success__def) ).

thf(87,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_hea1793595068369496646t_bool ) @ pp ) )
      & ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp )
       => ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).

thf(88,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_hea1793595068369496646t_bool ) @ pp ) )
    & ! [A: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit] :
        ( ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp )
       => ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
         != none_P2587165478634041381it_nat ) ) ),
    inference(miniscope,[status(thm)],[87]) ).

thf(89,plain,
    ! [D: heap_e7401611519738050253t_unit,C: heap_T6362127782908069795rray_a,B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ( ( D @ ( C @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp )
        | ( ( 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_hea1793595068369496646t_bool ) @ pp ) ) ),
    inference(cnf,[status(esa)],[88]) ).

thf(90,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_hea1793595068369496646t_bool ) @ pp ) ),
    inference(cnfConj,[status(thm)],[89]) ).

thf(92,plain,
    ! [B: heap_e7401611519738050253t_unit,A: heap_T6362127782908069795rray_a] :
      ( ~ ( B @ ( A @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp )
      | ( ( B @ ( A @ heap_T5591663578999710211rray_a @ aa_hea5936688510613671481it_nat ) )
       != none_P2587165478634041381it_nat ) ),
    inference(lifteq,[status(thm)],[90]) ).

thf(399,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_hea1793595068369496646t_bool ) @ pp )
      | ( none_P2587165478634041381it_nat != none_P2587165478634041381it_nat ) ),
    inference(paramod_ordered,[status(thm)],[62,92]) ).

thf(400,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_hea1793595068369496646t_bool ) @ pp ) ),
    inference(simp,[status(thm)],[399]) ).

thf(401,plain,
    ~ ( h @ ( xs @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp ),
    inference(pattern_uni,[status(thm)],[400:[bind(A,$thf( xs @ array_of_list_a )),bind(B,$thf( h ))]]) ).

thf(15,axiom,
    ! [A: list_a,B: heap_e7401611519738050253t_unit] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_success__of__listI) ).

thf(160,plain,
    ! [A: list_a,B: heap_e7401611519738050253t_unit] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).

thf(161,plain,
    ! [B: heap_e7401611519738050253t_unit,A: list_a] : ( B @ ( A @ array_of_list_a @ heap_T6932021131025641745rray_a @ aa_hea1793595068369496646t_bool ) @ pp ),
    inference(cnf,[status(esa)],[160]) ).

thf(417,plain,
    ~ $true,
    inference(rewrite,[status(thm)],[401,161]) ).

thf(418,plain,
    $false,
    inference(simp,[status(thm)],[417]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP216_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.14/0.40  % Computer : n008.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:12:24 UTC 2026
% 0.14/0.40  % CPUTime  : 
% 0.14/0.40  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.99  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 7.42/2.73  % [INFO] 	 Parsing done (1735ms). 
% 7.42/2.75  % [INFO] 	 Running in sequential loop mode. 
% 8.30/3.14  % [INFO] 	 eprover registered as external prover. 
% 8.30/3.15  % [INFO] 	 Scanning for conjecture ... 
% 12.37/4.25  % [INFO] 	 Found a conjecture (or negated_conjecture) and 8801 axioms. Running axiom selection ... 
% 13.97/4.84  % [INFO] 	 Axiom selection finished. Selected 57 axioms (removed 8744 axioms). 
% 14.37/4.94  % [INFO] 	 Problem is typed first-order (TPTP TFF). 
% 14.37/4.95  % [INFO] 	 Type checking passed. 
% 14.37/4.96  % [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 ... 
% 22.09/7.01  % [INFO] 	 Killing All external provers ... 
% 22.09/7.01  % Time passed: 6466ms (effective reasoning time: 4256ms)
% 22.09/7.02  % 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)>
% 22.09/7.02  % Axioms used in derivation (2): fact_12_success__def, fact_45_success__of__listI
% 22.09/7.02  % No. of inferences in proof: 19
% 22.09/7.02  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 6466 ms resp. 4256 ms w/o parsing
% 22.73/7.12  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 22.73/7.13  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------