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

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

% Computer : n001.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:48 AM UTC 2026

% Result   : Theorem 21.81s 6.89s
% Output   : Refutation 22.92s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    3
%            Number of leaves      :   76
% Syntax   : Number of formulae    :  154 (  56 unt;   0 typ;   0 def)
%            Number of atoms       :  374 (  69 equ;   0 cnn)
%            Maximal formula atoms :    6 (   2 avg)
%            Number of connectives : 1484 (  46   ~;   3   |;  40   &;1196   @)
%                                         (  18 <=>; 181  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   18 (   8 avg)
%            Number of types       : 1004 (1003 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   49 (  47 usr;  20 con; 0-4 aty)
%            Number of variables   :  414 (   0   ^; 396   !;  18   ?; 414   :)

% Comments : 
%------------------------------------------------------------------------------
thf(fun_Pr5467989252043799614at_o_o_type,type,
    fun_Pr5467989252043799614at_o_o: $tType ).

thf(fun_Pr8749598446483760582at_o_o_type,type,
    fun_Pr8749598446483760582at_o_o: $tType ).

thf(produc8646552449234976710_nat_o_type,type,
    produc8646552449234976710_nat_o: $tType ).

thf(produc3721170131464028153_nat_o_type,type,
    produc3721170131464028153_nat_o: $tType ).

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

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

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

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

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

thf(fun_Pr8903426527919313326ural_o_type,type,
    fun_Pr8903426527919313326ural_o: $tType ).

thf(produc2965453680857062146_nat_o_type,type,
    produc2965453680857062146_nat_o: $tType ).

thf(fun_Pr7691319399447915534at_b_o_type,type,
    fun_Pr7691319399447915534at_b_o: $tType ).

thf(fun_Pr7750674677602834956at_a_o_type,type,
    fun_Pr7750674677602834956at_a_o: $tType ).

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

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

thf(produc5926643658282055477_nat_o_type,type,
    produc5926643658282055477_nat_o: $tType ).

thf(fun_op3311566623873074537at_nat_type,type,
    fun_op3311566623873074537at_nat: $tType ).

thf(fun_se6682931024248017501at_nat_type,type,
    fun_se6682931024248017501at_nat: $tType ).

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

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

thf(fun_se177437144654672861at_nat_type,type,
    fun_se177437144654672861at_nat: $tType ).

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

thf(fun_fu8850208375822146947atural_type,type,
    fun_fu8850208375822146947atural: $tType ).

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

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

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

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

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

thf(fun_mu1615448358963118404_nat_o_type,type,
    fun_mu1615448358963118404_nat_o: $tType ).

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

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

thf(fun_op7235540884721919880it_nat_type,type,
    fun_op7235540884721919880it_nat: $tType ).

thf(fun_op5883308099655130629it_nat_type,type,
    fun_op5883308099655130629it_nat: $tType ).

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

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

thf(list_P4783563340545138382et_nat_type,type,
    list_P4783563340545138382et_nat: $tType ).

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

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

thf(fun_Pr6873217934956908984it_nat_type,type,
    fun_Pr6873217934956908984it_nat: $tType ).

thf(fun_Pr7916406164169562037it_nat_type,type,
    fun_Pr7916406164169562037it_nat: $tType ).

thf(fun_se4507453553354261854_nat_o_type,type,
    fun_se4507453553354261854_nat_o: $tType ).

thf(fun_se2186744213282142921at_nat_type,type,
    fun_se2186744213282142921at_nat: $tType ).

thf(fun_se5750412846314922030_nat_o_type,type,
    fun_se5750412846314922030_nat_o: $tType ).

thf(fun_fu2568544640974905491it_nat_type,type,
    fun_fu2568544640974905491it_nat: $tType ).

thf(fun_fu9056938625493858259it_nat_type,type,
    fun_fu9056938625493858259it_nat: $tType ).

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

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

thf(fun_Pr72924049037982510_int_o_type,type,
    fun_Pr72924049037982510_int_o: $tType ).

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

thf(fun_Pr774283325640823912it_nat_type,type,
    fun_Pr774283325640823912it_nat: $tType ).

thf(fun_Pr7750636411365408485it_nat_type,type,
    fun_Pr7750636411365408485it_nat: $tType ).

thf(fun_se4699893527908719235at_nat_type,type,
    fun_se4699893527908719235at_nat: $tType ).

thf(fun_se3981709065971081742_nat_o_type,type,
    fun_se3981709065971081742_nat_o: $tType ).

thf(fun_Pr3311134049912055598_nat_o_type,type,
    fun_Pr3311134049912055598_nat_o: $tType ).

thf(fun_Pr782666833218042862_nat_o_type,type,
    fun_Pr782666833218042862_nat_o: $tType ).

thf(fun_fu714798943701216869_nat_o_type,type,
    fun_fu714798943701216869_nat_o: $tType ).

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

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

thf(fun_se2737213715938160490_nat_o_type,type,
    fun_se2737213715938160490_nat_o: $tType ).

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

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

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

thf(fun_se5672428230568430382_nat_o_type,type,
    fun_se5672428230568430382_nat_o: $tType ).

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

thf(produc833397650935741523atural_type,type,
    produc833397650935741523atural: $tType ).

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

thf(fun_se5282722391638144526_nat_o_type,type,
    fun_se5282722391638144526_nat_o: $tType ).

thf(fun_fu1322491050725084261_nat_o_type,type,
    fun_fu1322491050725084261_nat_o: $tType ).

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

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

thf(fun_op2273118692420253608_nat_o_type,type,
    fun_op2273118692420253608_nat_o: $tType ).

thf(produc7243647663225551966_nat_b_type,type,
    produc7243647663225551966_nat_b: $tType ).

thf(produc8033090066717023711_nat_a_type,type,
    produc8033090066717023711_nat_a: $tType ).

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

thf(produc6963950461309505482atural_type,type,
    produc6963950461309505482atural: $tType ).

thf(fun_op1120011469960559414_nat_o_type,type,
    fun_op1120011469960559414_nat_o: $tType ).

thf(fun_op8739471410644078199_nat_o_type,type,
    fun_op8739471410644078199_nat_o: $tType ).

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

thf(fun_fu8161990777412754it_nat_type,type,
    fun_fu8161990777412754it_nat: $tType ).

thf(fun_fu6488529940522614227it_nat_type,type,
    fun_fu6488529940522614227it_nat: $tType ).

thf(fun_Pr8346683996641107384_nat_o_type,type,
    fun_Pr8346683996641107384_nat_o: $tType ).

thf(fun_Pr2992940411974564687it_nat_type,type,
    fun_Pr2992940411974564687it_nat: $tType ).

thf(fun_Pr8191437870481986254it_nat_type,type,
    fun_Pr8191437870481986254it_nat: $tType ).

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

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

thf(set_Pr5508209795250834101it_nat_type,type,
    set_Pr5508209795250834101it_nat: $tType ).

thf(set_Pr2819221443900773171it_nat_type,type,
    set_Pr2819221443900773171it_nat: $tType ).

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

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

thf(fun_b_3682875105831643059it_nat_type,type,
    fun_b_3682875105831643059it_nat: $tType ).

thf(fun_a_4942204877778174258it_nat_type,type,
    fun_a_4942204877778174258it_nat: $tType ).

thf(fun_Pr4959652356039452225it_nat_type,type,
    fun_Pr4959652356039452225it_nat: $tType ).

thf(fun_Pr7206221373966655808it_nat_type,type,
    fun_Pr7206221373966655808it_nat: $tType ).

thf(fun_Pr157300717155555520it_nat_type,type,
    fun_Pr157300717155555520it_nat: $tType ).

thf(fun_Pr2403869735082759103it_nat_type,type,
    fun_Pr2403869735082759103it_nat: $tType ).

thf(fun_Pr7387299081059808255it_nat_type,type,
    fun_Pr7387299081059808255it_nat: $tType ).

thf(fun_Pr7227498785783423999it_nat_type,type,
    fun_Pr7227498785783423999it_nat: $tType ).

thf(produc1273031398460193109it_nat_type,type,
    produc1273031398460193109it_nat: $tType ).

thf(produc9011797661310329043it_nat_type,type,
    produc9011797661310329043it_nat: $tType ).

thf(produc5048788716800215441_nat_b_type,type,
    produc5048788716800215441_nat_b: $tType ).

thf(produc778646029802724242_nat_a_type,type,
    produc778646029802724242_nat_a: $tType ).

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

thf(fun_fu400886066185544210it_nat_type,type,
    fun_fu400886066185544210it_nat: $tType ).

thf(fun_fu2643727258468172498it_nat_type,type,
    fun_fu2643727258468172498it_nat: $tType ).

thf(fun_fu2612457627315080531it_nat_type,type,
    fun_fu2612457627315080531it_nat: $tType ).

thf(fun_fu4855298819597708819it_nat_type,type,
    fun_fu4855298819597708819it_nat: $tType ).

thf(list_P8836981409019564976et_nat_type,type,
    list_P8836981409019564976et_nat: $tType ).

thf(fun_fu6044858605386232627_nat_o_type,type,
    fun_fu6044858605386232627_nat_o: $tType ).

thf(fun_fu4836394952439539509_nat_o_type,type,
    fun_fu4836394952439539509_nat_o: $tType ).

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

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

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

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

thf(fun_b_4161654760626720265it_nat_type,type,
    fun_b_4161654760626720265it_nat: $tType ).

thf(fun_a_6373226321756256586it_nat_type,type,
    fun_a_6373226321756256586it_nat: $tType ).

thf(fun_b_7697183073795684005it_nat_type,type,
    fun_b_7697183073795684005it_nat: $tType ).

thf(fun_b_4099525269183078948it_nat_type,type,
    fun_b_4099525269183078948it_nat: $tType ).

thf(fun_a_7024012846491921188it_nat_type,type,
    fun_a_7024012846491921188it_nat: $tType ).

thf(fun_a_3426355041879316131it_nat_type,type,
    fun_a_3426355041879316131it_nat: $tType ).

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

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

thf(fun_Pr2137375630576721649it_nat_type,type,
    fun_Pr2137375630576721649it_nat: $tType ).

thf(fun_Pr1634687943937911152it_nat_type,type,
    fun_Pr1634687943937911152it_nat: $tType ).

thf(fun_Pr1155457543210892272it_nat_type,type,
    fun_Pr1155457543210892272it_nat: $tType ).

thf(fun_Pr652769856572081775it_nat_type,type,
    fun_Pr652769856572081775it_nat: $tType ).

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

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

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

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

thf(fun_ar6592047341168336478it_nat_type,type,
    fun_ar6592047341168336478it_nat: $tType ).

thf(fun_ar554763049074313054it_nat_type,type,
    fun_ar554763049074313054it_nat: $tType ).

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

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

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

thf(fun_Pr5026674165934347155it_nat_type,type,
    fun_Pr5026674165934347155it_nat: $tType ).

thf(fun_Pr7273243183861550738it_nat_type,type,
    fun_Pr7273243183861550738it_nat: $tType ).

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

thf(fun_b_7001994053037931259it_nat_type,type,
    fun_b_7001994053037931259it_nat: $tType ).

thf(fun_b_989364880692008698it_nat_type,type,
    fun_b_989364880692008698it_nat: $tType ).

thf(fun_a_9184149311047732028it_nat_type,type,
    fun_a_9184149311047732028it_nat: $tType ).

thf(fun_a_3171520138701809467it_nat_type,type,
    fun_a_3171520138701809467it_nat: $tType ).

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

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

thf(fun_b_6809638951405183189it_nat_type,type,
    fun_b_6809638951405183189it_nat: $tType ).

thf(fun_a_576316402698418899it_nat_type,type,
    fun_a_576316402698418899it_nat: $tType ).

thf(fun_b_4666577566277263197it_nat_type,type,
    fun_b_4666577566277263197it_nat: $tType ).

thf(fun_a_728177123528609950it_nat_type,type,
    fun_a_728177123528609950it_nat: $tType ).

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

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

thf(fun_ar1474576826808783682it_nat_type,type,
    fun_ar1474576826808783682it_nat: $tType ).

thf(fun_he3223939975889911031it_nat_type,type,
    fun_he3223939975889911031it_nat: $tType ).

thf(fun_he8849654208132081782it_nat_type,type,
    fun_he8849654208132081782it_nat: $tType ).

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

thf(fun_Pr3216343399241953091it_nat_type,type,
    fun_Pr3216343399241953091it_nat: $tType ).

thf(fun_Pr2713655712603142594it_nat_type,type,
    fun_Pr2713655712603142594it_nat: $tType ).

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

thf(set_Pr4389693562480114009it_nat_type,type,
    set_Pr4389693562480114009it_nat: $tType ).

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

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

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

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

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

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

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

thf(fun_se3560235952666129655at_nat_type,type,
    fun_se3560235952666129655at_nat: $tType ).

thf(fun_fu959379683396315552_int_o_type,type,
    fun_fu959379683396315552_int_o: $tType ).

thf(fun_he986703168080474088it_nat_type,type,
    fun_he986703168080474088it_nat: $tType ).

thf(fun_he8488442066948866628it_nat_type,type,
    fun_he8488442066948866628it_nat: $tType ).

thf(produc8961450480463052793it_nat_type,type,
    produc8961450480463052793it_nat: $tType ).

thf(option2498585697089621389at_nat_type,type,
    option2498585697089621389at_nat: $tType ).

thf(fun_he8897818899970768042it_nat_type,type,
    fun_he8897818899970768042it_nat: $tType ).

thf(fun_he1921015881043195817it_nat_type,type,
    fun_he1921015881043195817it_nat: $tType ).

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

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

thf(fun_fu6703568167625668877_int_o_type,type,
    fun_fu6703568167625668877_int_o: $tType ).

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

thf(fun_se2185695799324892244_nat_o_type,type,
    fun_se2185695799324892244_nat_o: $tType ).

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

thf(fun_he2323575226933966612it_nat_type,type,
    fun_he2323575226933966612it_nat: $tType ).

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

thf(fun_fu792289584686185660er_nat_type,type,
    fun_fu792289584686185660er_nat: $tType ).

thf(fun_fu4176442768802536380er_nat_type,type,
    fun_fu4176442768802536380er_nat: $tType ).

thf(fun_fu202463024092729020er_int_type,type,
    fun_fu202463024092729020er_int: $tType ).

thf(fun_fu8759299743271765508er_int_type,type,
    fun_fu8759299743271765508er_int: $tType ).

thf(fun_op8852741442951501078_num_o_type,type,
    fun_op8852741442951501078_num_o: $tType ).

thf(fun_op8016730479996091735_num_o_type,type,
    fun_op8016730479996091735_num_o: $tType ).

thf(fun_op8645536343338973462_nat_o_type,type,
    fun_op8645536343338973462_nat_o: $tType ).

thf(fun_op7041624247167716439_nat_o_type,type,
    fun_op7041624247167716439_nat_o: $tType ).

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

thf(fun_Pr4065951289917319378at_rat_type,type,
    fun_Pr4065951289917319378at_rat: $tType ).

thf(fun_Pr7574179848310716106at_nat_type,type,
    fun_Pr7574179848310716106at_nat: $tType ).

thf(fun_Pr6333000437718031765it_nat_type,type,
    fun_Pr6333000437718031765it_nat: $tType ).

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

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

thf(fun_Pr1099658227000185396_nat_o_type,type,
    fun_Pr1099658227000185396_nat_o: $tType ).

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

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

thf(fun_fu8090991196261985865_int_o_type,type,
    fun_fu8090991196261985865_int_o: $tType ).

thf(fun_he168995381318928090it_nat_type,type,
    fun_he168995381318928090it_nat: $tType ).

thf(fun_he8889679731534893401it_nat_type,type,
    fun_he8889679731534893401it_nat: $tType ).

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

thf(produc7738239854019400055nt_int_type,type,
    produc7738239854019400055nt_int: $tType ).

thf(fun_fu4755565544374692864r_assn_type,type,
    fun_fu4755565544374692864r_assn: $tType ).

thf(fun_se7788542033685991124_nat_o_type,type,
    fun_se7788542033685991124_nat_o: $tType ).

thf(fun_fu8336550301028287791at_nat_type,type,
    fun_fu8336550301028287791at_nat: $tType ).

thf(fun_fu1095011443884336175at_nat_type,type,
    fun_fu1095011443884336175at_nat: $tType ).

thf(fun_fu4854240044958656303at_int_type,type,
    fun_fu4854240044958656303at_int: $tType ).

thf(fun_fu1493779525457017043nt_int_type,type,
    fun_fu1493779525457017043nt_int: $tType ).

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

thf(fun_fu8621421401018972867nt_nat_type,type,
    fun_fu8621421401018972867nt_nat: $tType ).

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

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

thf(fun_se4456751357192657760_int_o_type,type,
    fun_se4456751357192657760_int_o: $tType ).

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

thf(produc2207270350733924475it_nat_type,type,
    produc2207270350733924475it_nat: $tType ).

thf(produc4453839368661128058it_nat_type,type,
    produc4453839368661128058it_nat: $tType ).

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

thf(fun_Pr6968369006614801746at_rat_type,type,
    fun_Pr6968369006614801746at_rat: $tType ).

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

thf(fun_fu6634461749290962705_int_o_type,type,
    fun_fu6634461749290962705_int_o: $tType ).

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

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

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

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

thf(fun_mu7838234450475261998_nat_o_type,type,
    fun_mu7838234450475261998_nat_o: $tType ).

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

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

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

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

thf(fun_fu1597678101255499801at_rat_type,type,
    fun_fu1597678101255499801at_rat: $tType ).

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

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

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

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

thf(fun_se3135557758678015630_int_o_type,type,
    fun_se3135557758678015630_int_o: $tType ).

thf(fun_fu5088349107139067777_int_o_type,type,
    fun_fu5088349107139067777_int_o: $tType ).

thf(option4277301481530639448it_nat_type,type,
    option4277301481530639448it_nat: $tType ).

thf(option2555668343544256180it_nat_type,type,
    option2555668343544256180it_nat: $tType ).

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

thf(fun_se2817990011555733942_int_o_type,type,
    fun_se2817990011555733942_int_o: $tType ).

thf(fun_na3679441993588394007it_nat_type,type,
    fun_na3679441993588394007it_nat: $tType ).

thf(fun_na5926011011515597590it_nat_type,type,
    fun_na5926011011515597590it_nat: $tType ).

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

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

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

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

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

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

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

thf(fun_fu8958601512183576259eger_o_type,type,
    fun_fu8958601512183576259eger_o: $tType ).

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

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

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

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

thf(option1013472963438093988it_nat_type,type,
    option1013472963438093988it_nat: $tType ).

thf(fun_fu5399310930634420241_int_o_type,type,
    fun_fu5399310930634420241_int_o: $tType ).

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

thf(list_P626663023886443800it_nat_type,type,
    list_P626663023886443800it_nat: $tType ).

thf(fun_op3313016124244812839_nat_o_type,type,
    fun_op3313016124244812839_nat_o: $tType ).

thf(fun_op9133723461703387112_nat_o_type,type,
    fun_op9133723461703387112_nat_o: $tType ).

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

thf(fun_fu4073184632390761289at_nat_type,type,
    fun_fu4073184632390761289at_nat: $tType ).

thf(fun_fu9148247276982919825at_nat_type,type,
    fun_fu9148247276982919825at_nat: $tType ).

thf(fun_fu3143578834292514029nt_nat_type,type,
    fun_fu3143578834292514029nt_nat: $tType ).

thf(fun_fu4584101141160326545at_int_type,type,
    fun_fu4584101141160326545at_int: $tType ).

thf(fun_fu7802804735324696557nt_int_type,type,
    fun_fu7802804735324696557nt_int: $tType ).

thf(fun_fu3180206027003385489at_nat_type,type,
    fun_fu3180206027003385489at_nat: $tType ).

thf(fun_fu6398909621167755501nt_nat_type,type,
    fun_fu6398909621167755501nt_nat: $tType ).

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

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

thf(fun_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_Pr557098546508347797at_nat_type,type,
    fun_Pr557098546508347797at_nat: $tType ).

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

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

thf(fun_se2092758488442489134_int_o_type,type,
    fun_se2092758488442489134_int_o: $tType ).

thf(fun_li124330075790197867t_assn_type,type,
    fun_li124330075790197867t_assn: $tType ).

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

thf(fun_fu7503463384463898374nt_o_o_type,type,
    fun_fu7503463384463898374nt_o_o: $tType ).

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

thf(fun_fu4592178885959468770_int_o_type,type,
    fun_fu4592178885959468770_int_o: $tType ).

thf(fun_fu8427683764667544036nt_int_type,type,
    fun_fu8427683764667544036nt_int: $tType ).

thf(fun_as3747249873083764768_nat_o_type,type,
    fun_as3747249873083764768_nat_o: $tType ).

thf(produc6751673265320737416it_nat_type,type,
    produc6751673265320737416it_nat: $tType ).

thf(produc7196121022310644452it_nat_type,type,
    produc7196121022310644452it_nat: $tType ).

thf(fun_fu7237799034916548881_nat_o_type,type,
    fun_fu7237799034916548881_nat_o: $tType ).

thf(fun_Pr6180708418112149265at_num_type,type,
    fun_Pr6180708418112149265at_num: $tType ).

thf(fun_Pr5472464481163311559at_nat_type,type,
    fun_Pr5472464481163311559at_nat: $tType ).

thf(fun_Pr5112106203349071120at_num_type,type,
    fun_Pr5112106203349071120at_num: $tType ).

thf(fun_Pr4403862266400233414at_nat_type,type,
    fun_Pr4403862266400233414at_nat: $tType ).

thf(fun_nu147038076112158225it_nat_type,type,
    fun_nu147038076112158225it_nat: $tType ).

thf(fun_nu8867722426328123536it_nat_type,type,
    fun_nu8867722426328123536it_nat: $tType ).

thf(fun_na683342808802396953_nat_o_type,type,
    fun_na683342808802396953_nat_o: $tType ).

thf(fun_in7694643900704578053_int_o_type,type,
    fun_in7694643900704578053_int_o: $tType ).

thf(option4065278094766928714it_nat_type,type,
    option4065278094766928714it_nat: $tType ).

thf(option3562590408128118217it_nat_type,type,
    option3562590408128118217it_nat: $tType ).

thf(fun_b_7146180689985673569et_nat_type,type,
    fun_b_7146180689985673569et_nat: $tType ).

thf(fun_b_2332632271197754813et_int_type,type,
    fun_b_2332632271197754813et_int: $tType ).

thf(fun_a_8173838432492502368et_nat_type,type,
    fun_a_8173838432492502368et_nat: $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_fu5832215286117076717t_assn_type,type,
    fun_fu5832215286117076717t_assn: $tType ).

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

thf(fun_Pr8699404193998200756_int_o_type,type,
    fun_Pr8699404193998200756_int_o: $tType ).

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

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

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

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

thf(list_P7438302566501821706it_nat_type,type,
    list_P7438302566501821706it_nat: $tType ).

thf(list_P6935614879863011209it_nat_type,type,
    list_P6935614879863011209it_nat: $tType ).

thf(fun_fu4640364191220304065at_nat_type,type,
    fun_fu4640364191220304065at_nat: $tType ).

thf(fun_fu4422690180167752641at_nat_type,type,
    fun_fu4422690180167752641at_nat: $tType ).

thf(fun_fu1432006813369012345at_int_type,type,
    fun_fu1432006813369012345at_int: $tType ).

thf(fun_fu8188496484073410517nt_int_type,type,
    fun_fu8188496484073410517nt_int: $tType ).

thf(fun_se374060482380105870_nat_o_type,type,
    fun_se374060482380105870_nat_o: $tType ).

thf(produc8032495849646651230it_nat_type,type,
    produc8032495849646651230it_nat: $tType ).

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

thf(fun_fu3068557634114553409_int_o_type,type,
    fun_fu3068557634114553409_int_o: $tType ).

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

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

thf(set_Pr7600907837789447088it_nat_type,type,
    set_Pr7600907837789447088it_nat: $tType ).

thf(set_Pr7098220151150636591it_nat_type,type,
    set_Pr7098220151150636591it_nat: $tType ).

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

thf(fun_Pr856651894144386551_nat_o_type,type,
    fun_Pr856651894144386551_nat_o: $tType ).

thf(fun_Pr5746006151868627512_nat_o_type,type,
    fun_Pr5746006151868627512_nat_o: $tType ).

thf(produc6197004810343482825et_nat_type,type,
    produc6197004810343482825et_nat: $tType ).

thf(list_f5222602229612168821_nat_o_type,type,
    list_f5222602229612168821_nat_o: $tType ).

thf(fun_b_9192071537261429513_set_o_type,type,
    fun_b_9192071537261429513_set_o: $tType ).

thf(fun_a_6228866161775505738_set_o_type,type,
    fun_a_6228866161775505738_set_o: $tType ).

thf(fun_fu5510336631606277565nteger_type,type,
    fun_fu5510336631606277565nteger: $tType ).

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

thf(fun_Pr1029825253981700553at_nat_type,type,
    fun_Pr1029825253981700553at_nat: $tType ).

thf(fun_fu6385016345819965645er_nat_type,type,
    fun_fu6385016345819965645er_nat: $tType ).

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

thf(fun_fu7601192970096278275eger_o_type,type,
    fun_fu7601192970096278275eger_o: $tType ).

thf(fun_fu165634461008800387_nat_o_type,type,
    fun_fu165634461008800387_nat_o: $tType ).

thf(fun_fu5813846785102284803eger_o_type,type,
    fun_fu5813846785102284803eger_o: $tType ).

thf(fun_fu7864316720324808067_int_o_type,type,
    fun_fu7864316720324808067_int_o: $tType ).

thf(fun_fu6309186030181755779eger_o_type,type,
    fun_fu6309186030181755779eger_o: $tType ).

thf(fun_fu8096999557949053699_nat_o_type,type,
    fun_fu8096999557949053699_nat_o: $tType ).

thf(fun_fu7527167023631164035eger_o_type,type,
    fun_fu7527167023631164035eger_o: $tType ).

thf(fun_fu354264921998911491_int_o_type,type,
    fun_fu354264921998911491_int_o: $tType ).

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

thf(produc5504626439533210094nt_int_type,type,
    produc5504626439533210094nt_int: $tType ).

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

thf(fun_fu4618758991028193283_o_nat_type,type,
    fun_fu4618758991028193283_o_nat: $tType ).

thf(fun_fu5572043292636673283_o_nat_type,type,
    fun_fu5572043292636673283_o_nat: $tType ).

thf(fun_fu731591423980087811_o_int_type,type,
    fun_fu731591423980087811_o_int: $tType ).

thf(fun_fu5188028542856013059_o_int_type,type,
    fun_fu5188028542856013059_o_int: $tType ).

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

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

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

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

thf(fun_Pr4335030045194121423et_nat_type,type,
    fun_Pr4335030045194121423et_nat: $tType ).

thf(fun_Pr1844946900262394667et_int_type,type,
    fun_Pr1844946900262394667et_int: $tType ).

thf(fun_b_7832390750199427630it_nat_type,type,
    fun_b_7832390750199427630it_nat: $tType ).

thf(fun_a_1313742400928293293it_nat_type,type,
    fun_a_1313742400928293293it_nat: $tType ).

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

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

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

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

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

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

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

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

thf(produc7388388658123137530it_nat_type,type,
    produc7388388658123137530it_nat: $tType ).

thf(produc3260487557148687353it_nat_type,type,
    produc3260487557148687353it_nat: $tType ).

thf(fun_in217785400498748499nt_int_type,type,
    fun_in217785400498748499nt_int: $tType ).

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

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

thf(fun_se5614109888078709212_int_o_type,type,
    fun_se5614109888078709212_int_o: $tType ).

thf(fun_Pr494705684233454228eger_o_type,type,
    fun_Pr494705684233454228eger_o: $tType ).

thf(list_P9062070895058802706et_nat_type,type,
    list_P9062070895058802706et_nat: $tType ).

thf(fun_fu7409062071265970153_int_o_type,type,
    fun_fu7409062071265970153_int_o: $tType ).

thf(fun_fu1345883967705819239_int_o_type,type,
    fun_fu1345883967705819239_int_o: $tType ).

thf(fun_b_540864168722188329_nat_o_type,type,
    fun_b_540864168722188329_nat_o: $tType ).

thf(fun_a_2467521563176467050_nat_o_type,type,
    fun_a_2467521563176467050_nat_o: $tType ).

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

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

thf(fun_fu960360787657196261at_int_type,type,
    fun_fu960360787657196261at_int: $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_fu5221552698205305849nt_int_type,type,
    fun_fu5221552698205305849nt_int: $tType ).

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

thf(fun_fu1095064002760310426er_nat_type,type,
    fun_fu1095064002760310426er_nat: $tType ).

thf(fun_fu513762604956806682er_nat_type,type,
    fun_fu513762604956806682er_nat: $tType ).

thf(fun_fu7247051496879855734er_int_type,type,
    fun_fu7247051496879855734er_int: $tType ).

thf(fun_fu3779984648686517950er_nat_type,type,
    fun_fu3779984648686517950er_nat: $tType ).

thf(fun_fu1289901503754791194er_int_type,type,
    fun_fu1289901503754791194er_int: $tType ).

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

thf(fun_Pr8691148245588442629_set_o_type,type,
    fun_Pr8691148245588442629_set_o: $tType ).

thf(fun_fu556125837173103209o_assn_type,type,
    fun_fu556125837173103209o_assn: $tType ).

thf(fun_li6911922195568332558t_assn_type,type,
    fun_li6911922195568332558t_assn: $tType ).

thf(fun_li8672845860709154922t_assn_type,type,
    fun_li8672845860709154922t_assn: $tType ).

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

thf(fun_fu1574286537503582443on_num_type,type,
    fun_fu1574286537503582443on_num: $tType ).

thf(fun_fu5285309056923805367un_o_o_type,type,
    fun_fu5285309056923805367un_o_o: $tType ).

thf(fun_fu5848294987682527897eger_o_type,type,
    fun_fu5848294987682527897eger_o: $tType ).

thf(fun_fu5257111247350578329un_o_o_type,type,
    fun_fu5257111247350578329un_o_o: $tType ).

thf(fun_fu5820097178109300859eger_o_type,type,
    fun_fu5820097178109300859eger_o: $tType ).

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

thf(fun_fu7460908759652350970nt_rat_type,type,
    fun_fu7460908759652350970nt_rat: $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(fun_fu9090758901314268781nt_o_o_type,type,
    fun_fu9090758901314268781nt_o_o: $tType ).

thf(fun_fu2454420574033104442at_nat_type,type,
    fun_fu2454420574033104442at_nat: $tType ).

thf(fun_fu3739269683040691718nt_int_type,type,
    fun_fu3739269683040691718nt_int: $tType ).

thf(fun_se5087743179055239239nteger_type,type,
    fun_se5087743179055239239nteger: $tType ).

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

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

thf(fun_fu1481857817119020493_int_o_type,type,
    fun_fu1481857817119020493_int_o: $tType ).

thf(fun_fu6453395667394816515nt_int_type,type,
    fun_fu6453395667394816515nt_int: $tType ).

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

thf(fun_fu4213695556130342827eger_o_type,type,
    fun_fu4213695556130342827eger_o: $tType ).

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

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

thf(fun_fu2439999276549649860er_nat_type,type,
    fun_fu2439999276549649860er_nat: $tType ).

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

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

thf(option233860712434008220it_nat_type,type,
    option233860712434008220it_nat: $tType ).

thf(fun_fu551331151826482407at_rat_type,type,
    fun_fu551331151826482407at_rat: $tType ).

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

thf(produc1730305018825802663t_unit_type,type,
    produc1730305018825802663t_unit: $tType ).

thf(produc3407818250607552075t_unit_type,type,
    produc3407818250607552075t_unit: $tType ).

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

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

thf(fun_in7813510203222682420_int_o_type,type,
    fun_in7813510203222682420_int_o: $tType ).

thf(list_P131111800688179804it_nat_type,type,
    list_P131111800688179804it_nat: $tType ).

thf(fun_fu1590586450949517859at_nat_type,type,
    fun_fu1590586450949517859at_nat: $tType ).

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

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

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

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

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

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

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

thf(fun_se7799640332748030482r_assn_type,type,
    fun_se7799640332748030482r_assn: $tType ).

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

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

thf(fun_fu1076126395241477261at_nat_type,type,
    fun_fu1076126395241477261at_nat: $tType ).

thf(fun_fu716243638958221197nt_nat_type,type,
    fun_fu716243638958221197nt_nat: $tType ).

thf(fun_fu6473686551640679437at_nat_type,type,
    fun_fu6473686551640679437at_nat: $tType ).

thf(fun_fu3983603406708952681at_int_type,type,
    fun_fu3983603406708952681at_int: $tType ).

thf(fun_fu5979819066169710441nt_int_type,type,
    fun_fu5979819066169710441nt_int: $tType ).

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

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

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

thf(fun_Pr7971309923680890661_nat_o_type,type,
    fun_Pr7971309923680890661_nat_o: $tType ).

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

thf(fun_fu5646853623633916995_int_o_type,type,
    fun_fu5646853623633916995_int_o: $tType ).

thf(fun_fu8304507701009772099_nat_o_type,type,
    fun_fu8304507701009772099_nat_o: $tType ).

thf(fun_fu7493154764834273859_int_o_type,type,
    fun_fu7493154764834273859_int_o: $tType ).

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

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

thf(fun_ar7139816496917982587t_assn_type,type,
    fun_ar7139816496917982587t_assn: $tType ).

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

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

thf(fun_fu4472246792138249213_nat_o_type,type,
    fun_fu4472246792138249213_nat_o: $tType ).

thf(fun_in3304247434473118374nt_int_type,type,
    fun_in3304247434473118374nt_int: $tType ).

thf(fun_na4518284863240432007_nat_o_type,type,
    fun_na4518284863240432007_nat_o: $tType ).

thf(fun_na6120508140265747663_int_o_type,type,
    fun_na6120508140265747663_int_o: $tType ).

thf(produc5011041761010125393t_unit_type,type,
    produc5011041761010125393t_unit: $tType ).

thf(fun_fu7075445697382584196_int_o_type,type,
    fun_fu7075445697382584196_int_o: $tType ).

thf(fun_fu4413992040155564420at_nat_type,type,
    fun_fu4413992040155564420at_nat: $tType ).

thf(fun_fu923337204662071120nt_int_type,type,
    fun_fu923337204662071120nt_int: $tType ).

thf(fun_fu5689865433563736081nteger_type,type,
    fun_fu5689865433563736081nteger: $tType ).

thf(fun_se1909708154429037836et_nat_type,type,
    fun_se1909708154429037836et_nat: $tType ).

thf(fun_se6573205548028396576et_int_type,type,
    fun_se6573205548028396576et_int: $tType ).

thf(fun_se8983711159220854466er_rat_type,type,
    fun_se8983711159220854466er_rat: $tType ).

thf(fun_se6140325459843756218er_nat_type,type,
    fun_se6140325459843756218er_nat: $tType ).

thf(fun_ra8505079968215247908at_rat_type,type,
    fun_ra8505079968215247908at_rat: $tType ).

thf(fun_Co6813818151677833714atural_type,type,
    fun_Co6813818151677833714atural: $tType ).

thf(fun_Co8514937155073724839atural_type,type,
    fun_Co8514937155073724839atural: $tType ).

thf(fun_Co1981900195452921617nteger_type,type,
    fun_Co1981900195452921617nteger: $tType ).

thf(fun_fu1237770272497958833_nat_o_type,type,
    fun_fu1237770272497958833_nat_o: $tType ).

thf(fun_fu4523568072766896123eger_o_type,type,
    fun_fu4523568072766896123eger_o: $tType ).

thf(fun_fu2182969643484777475eger_o_type,type,
    fun_fu2182969643484777475eger_o: $tType ).

thf(fun_fu1992263728252513447eger_o_type,type,
    fun_fu1992263728252513447eger_o: $tType ).

thf(fun_fu991479512444375705er_rat_type,type,
    fun_fu991479512444375705er_rat: $tType ).

thf(fun_fu7371465849922053265er_nat_type,type,
    fun_fu7371465849922053265er_nat: $tType ).

thf(fun_fu4881382704990326509er_int_type,type,
    fun_fu4881382704990326509er_int: $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_fu1502755112258691281at_nat_type,type,
    fun_fu1502755112258691281at_nat: $tType ).

thf(fun_fu5130958774822480081on_num_type,type,
    fun_fu5130958774822480081on_num: $tType ).

thf(fun_fu9039538216874201369_o_rat_type,type,
    fun_fu9039538216874201369_o_rat: $tType ).

thf(fun_fu3581538110357139729_o_nat_type,type,
    fun_fu3581538110357139729_o_nat: $tType ).

thf(fun_fu9026017786105829997_o_int_type,type,
    fun_fu9026017786105829997_o_int: $tType ).

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

thf(fun_in259009099871059828at_nat_type,type,
    fun_in259009099871059828at_nat: $tType ).

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

thf(fun_op7680796716376270858on_nat_type,type,
    fun_op7680796716376270858on_nat: $tType ).

thf(fun_op7417050415941327134on_int_type,type,
    fun_op7417050415941327134on_int: $tType ).

thf(fun_se1865396762483378772_nat_o_type,type,
    fun_se1865396762483378772_nat_o: $tType ).

thf(fun_na4138050610385705875at_nat_type,type,
    fun_na4138050610385705875at_nat: $tType ).

thf(fun_in1696471567231710611nt_int_type,type,
    fun_in1696471567231710611nt_int: $tType ).

thf(set_Pr5488025237498180813et_nat_type,type,
    set_Pr5488025237498180813et_nat: $tType ).

thf(set_Pr2522554150109002629et_int_type,type,
    set_Pr2522554150109002629et_int: $tType ).

thf(fun_fu1994797156054922755_nat_o_type,type,
    fun_fu1994797156054922755_nat_o: $tType ).

thf(fun_se9106460625052465826_int_o_type,type,
    fun_se9106460625052465826_int_o: $tType ).

thf(fun_ra7317100687414072407at_rat_type,type,
    fun_ra7317100687414072407at_rat: $tType ).

thf(fun_ra1107035566227760819at_rat_type,type,
    fun_ra1107035566227760819at_rat: $tType ).

thf(fun_Pr3947133745332865710_nat_o_type,type,
    fun_Pr3947133745332865710_nat_o: $tType ).

thf(fun_Pr4126283446944868854_int_o_type,type,
    fun_Pr4126283446944868854_int_o: $tType ).

thf(fun_na6244580715232974919at_nat_type,type,
    fun_na6244580715232974919at_nat: $tType ).

thf(fun_na34515594046663331at_nat_type,type,
    fun_na34515594046663331at_nat: $tType ).

thf(fun_li4611866707255273568o_assn_type,type,
    fun_li4611866707255273568o_assn: $tType ).

thf(fun_in2640216123419753727at_int_type,type,
    fun_in2640216123419753727at_int: $tType ).

thf(fun_in5653523039088217947at_int_type,type,
    fun_in5653523039088217947at_int: $tType ).

thf(fun_Co1766037875893669450eger_o_type,type,
    fun_Co1766037875893669450eger_o: $tType ).

thf(fun_fu3380082687118895412nteger_type,type,
    fun_fu3380082687118895412nteger: $tType ).

thf(fun_fu2995346897264222311t_assn_type,type,
    fun_fu2995346897264222311t_assn: $tType ).

thf(fun_fu6568868615275847455t_assn_type,type,
    fun_fu6568868615275847455t_assn: $tType ).

thf(produc6653097349344004940it_nat_type,type,
    produc6653097349344004940it_nat: $tType ).

thf(fun_fu5908277796454533188_int_o_type,type,
    fun_fu5908277796454533188_int_o: $tType ).

thf(fun_fu5776950848406856154at_nat_type,type,
    fun_fu5776950848406856154at_nat: $tType ).

thf(fun_fu5586244933174592126at_nat_type,type,
    fun_fu5586244933174592126at_nat: $tType ).

thf(fun_fu3096161788242865370at_int_type,type,
    fun_fu3096161788242865370at_int: $tType ).

thf(fun_fu7773166507867613914nt_nat_type,type,
    fun_fu7773166507867613914nt_nat: $tType ).

thf(fun_fu5283083362935887158nt_int_type,type,
    fun_fu5283083362935887158nt_int: $tType ).

thf(fun_fu9201817095025044880_nat_o_type,type,
    fun_fu9201817095025044880_nat_o: $tType ).

thf(fun_fu570715051317967998at_nat_type,type,
    fun_fu570715051317967998at_nat: $tType ).

thf(fun_fu2757636626010989786nt_nat_type,type,
    fun_fu2757636626010989786nt_nat: $tType ).

thf(fun_fu2566930710778725758nt_nat_type,type,
    fun_fu2566930710778725758nt_nat: $tType ).

thf(fun_fu4208408993564413984_int_o_type,type,
    fun_fu4208408993564413984_int_o: $tType ).

thf(fun_se2389560805064864136_nat_o_type,type,
    fun_se2389560805064864136_nat_o: $tType ).

thf(fun_na927404270896789692_nat_o_type,type,
    fun_na927404270896789692_nat_o: $tType ).

thf(fun_in8471228297299470156_int_o_type,type,
    fun_in8471228297299470156_int_o: $tType ).

thf(fun_fu2408719596384163971_nat_o_type,type,
    fun_fu2408719596384163971_nat_o: $tType ).

thf(fun_fu8094397175230428611eger_o_type,type,
    fun_fu8094397175230428611eger_o: $tType ).

thf(fun_fu2786480252100984515nteger_type,type,
    fun_fu2786480252100984515nteger: $tType ).

thf(produc7248412053542808358at_nat_type,type,
    produc7248412053542808358at_nat: $tType ).

thf(fun_fu2897328509465618819_nat_o_type,type,
    fun_fu2897328509465618819_nat_o: $tType ).

thf(fun_fu2797749360310127211on_num_type,type,
    fun_fu2797749360310127211on_num: $tType ).

thf(fun_fu9082890457842154773_o_nat_type,type,
    fun_fu9082890457842154773_o_nat: $tType ).

thf(fun_Pr292408699144966967t_unit_type,type,
    fun_Pr292408699144966967t_unit: $tType ).

thf(fun_fu865690600344432797un_o_o_type,type,
    fun_fu865690600344432797un_o_o: $tType ).

thf(fun_fu2885402556529144793_nat_o_type,type,
    fun_fu2885402556529144793_nat_o: $tType ).

thf(fun_fu6500062642585991509un_o_o_type,type,
    fun_fu6500062642585991509un_o_o: $tType ).

thf(fun_fu7616189625787487449_int_o_type,type,
    fun_fu7616189625787487449_int_o: $tType ).

thf(fun_fu7066070072329265113un_o_o_type,type,
    fun_fu7066070072329265113un_o_o: $tType ).

thf(fun_fu9085782028513977109_nat_o_type,type,
    fun_fu9085782028513977109_nat_o: $tType ).

thf(fun_fu2881495813246281945un_o_o_type,type,
    fun_fu2881495813246281945un_o_o: $tType ).

thf(fun_fu3997622796447777885_int_o_type,type,
    fun_fu3997622796447777885_int_o: $tType ).

thf(fun_fu2641566564518291801un_o_o_type,type,
    fun_fu2641566564518291801un_o_o: $tType ).

thf(fun_fu5915781709770235737un_o_o_type,type,
    fun_fu5915781709770235737un_o_o: $tType ).

thf(fun_mu3043097228830271956_nat_o_type,type,
    fun_mu3043097228830271956_nat_o: $tType ).

thf(fun_he4135464443191253079_nat_o_type,type,
    fun_he4135464443191253079_nat_o: $tType ).

thf(fun_se593059424582005380nt_rat_type,type,
    fun_se593059424582005380nt_rat: $tType ).

thf(fun_se4101287982975402108nt_nat_type,type,
    fun_se4101287982975402108nt_nat: $tType ).

thf(fun_ra7314870381713115802nt_int_type,type,
    fun_ra7314870381713115802nt_int: $tType ).

thf(fun_Pr6026251430685297nteger_type,type,
    fun_Pr6026251430685297nteger: $tType ).

thf(fun_op493924057549976310_num_o_type,type,
    fun_op493924057549976310_num_o: $tType ).

thf(fun_na7044673412300895210at_nat_type,type,
    fun_na7044673412300895210at_nat: $tType ).

thf(fun_in7209865251430457670nt_int_type,type,
    fun_in7209865251430457670nt_int: $tType ).

thf(fun_Pr2477578491906815678t_assn_type,type,
    fun_Pr2477578491906815678t_assn: $tType ).

thf(fun_Pr4738963024209204295_int_o_type,type,
    fun_Pr4738963024209204295_int_o: $tType ).

thf(fun_Pr7537129237977221859_rat_o_type,type,
    fun_Pr7537129237977221859_rat_o: $tType ).

thf(fun_na3970208099681795815_nat_o_type,type,
    fun_na3970208099681795815_nat_o: $tType ).

thf(fun_in4843545397633388171_int_o_type,type,
    fun_in4843545397633388171_int_o: $tType ).

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

thf(fun_ra154387494674143703at_rat_type,type,
    fun_ra154387494674143703at_rat: $tType ).

thf(fun_na2977190036508382167at_nat_type,type,
    fun_na2977190036508382167at_nat: $tType ).

thf(fun_in3146844979458463959at_int_type,type,
    fun_in3146844979458463959at_int: $tType ).

thf(option8963830502488799655at_nat_type,type,
    option8963830502488799655at_nat: $tType ).

thf(fun_se6579715966475752165nteger_type,type,
    fun_se6579715966475752165nteger: $tType ).

thf(fun_na7078387940644931716nteger_type,type,
    fun_na7078387940644931716nteger: $tType ).

thf(fun_in7207726656141197838et_nat_type,type,
    fun_in7207726656141197838et_nat: $tType ).

thf(fun_Co740390889742897050atural_type,type,
    fun_Co740390889742897050atural: $tType ).

thf(fun_Co6749200540738471926atural_type,type,
    fun_Co6749200540738471926atural: $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(option2108551362046372146_int_o_type,type,
    option2108551362046372146_int_o: $tType ).

thf(fun_fu2798942646354680517_nat_o_type,type,
    fun_fu2798942646354680517_nat_o: $tType ).

thf(fun_fu5838931486547983824_nat_o_type,type,
    fun_fu5838931486547983824_nat_o: $tType ).

thf(fun_fu7898940055406642654nteger_type,type,
    fun_fu7898940055406642654nteger: $tType ).

thf(fun_fu2231310910465984013_int_o_type,type,
    fun_fu2231310910465984013_int_o: $tType ).

thf(fun_fu5271299750659287320_int_o_type,type,
    fun_fu5271299750659287320_int_o: $tType ).

thf(fun_fu6361890901329191134nteger_type,type,
    fun_fu6361890901329191134nteger: $tType ).

thf(fun_fu7006494623891191978at_nat_type,type,
    fun_fu7006494623891191978at_nat: $tType ).

thf(fun_fu2395600473883792738nt_nat_type,type,
    fun_fu2395600473883792738nt_nat: $tType ).

thf(fun_fu4655640274933727718at_nat_type,type,
    fun_fu4655640274933727718at_nat: $tType ).

thf(fun_fu2165557130002000962at_int_type,type,
    fun_fu2165557130002000962at_int: $tType ).

thf(fun_fu4161772789462758722nt_int_type,type,
    fun_fu4161772789462758722nt_int: $tType ).

thf(fun_se7316093745529328985et_nat_type,type,
    fun_se7316093745529328985et_nat: $tType ).

thf(option8886115935005447431nteger_type,type,
    option8886115935005447431nteger: $tType ).

thf(fun_as4019953064511417593t_assn_type,type,
    fun_as4019953064511417593t_assn: $tType ).

thf(fun_li1025265955262268170_nat_o_type,type,
    fun_li1025265955262268170_nat_o: $tType ).

thf(fun_ar8560675821539856405t_assn_type,type,
    fun_ar8560675821539856405t_assn: $tType ).

thf(fun_ar528246731820255437t_assn_type,type,
    fun_ar528246731820255437t_assn: $tType ).

thf(set_se7855581050983116737at_nat_type,type,
    set_se7855581050983116737at_nat: $tType ).

thf(set_se6260736226359567993nt_int_type,type,
    set_se6260736226359567993nt_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_se4782206882984618170_nat_o_type,type,
    fun_se4782206882984618170_nat_o: $tType ).

thf(fun_se7249947736802449410_int_o_type,type,
    fun_se7249947736802449410_int_o: $tType ).

thf(fun_li4928566814967809234t_assn_type,type,
    fun_li4928566814967809234t_assn: $tType ).

thf(fun_li1703715468755832110t_assn_type,type,
    fun_li1703715468755832110t_assn: $tType ).

thf(fun_fu6891447142836604759at_o_o_type,type,
    fun_fu6891447142836604759at_o_o: $tType ).

thf(fun_fu967847188302805519nt_o_o_type,type,
    fun_fu967847188302805519nt_o_o: $tType ).

thf(fun_na1108963418173300452_nat_o_type,type,
    fun_na1108963418173300452_nat_o: $tType ).

thf(fun_fu8155524643419131615um_num_type,type,
    fun_fu8155524643419131615um_num: $tType ).

thf(fun_fu726849872193282289um_int_type,type,
    fun_fu726849872193282289um_int: $tType ).

thf(fun_fu5322398707847370225um_num_type,type,
    fun_fu5322398707847370225um_num: $tType ).

thf(fun_fu7117095973476296707um_int_type,type,
    fun_fu7117095973476296707um_int: $tType ).

thf(fun_fu8328862064278946247at_rat_type,type,
    fun_fu8328862064278946247at_rat: $tType ).

thf(fun_fu7002938529518989751at_nat_type,type,
    fun_fu7002938529518989751at_nat: $tType ).

thf(fun_fu4512855384587262995at_int_type,type,
    fun_fu4512855384587262995at_int: $tType ).

thf(fun_fu8464300013002972271at_int_type,type,
    fun_fu8464300013002972271at_int: $tType ).

thf(fun_fu1008360527747082367nt_rat_type,type,
    fun_fu1008360527747082367nt_rat: $tType ).

thf(fun_fu8905809029841901679nt_nat_type,type,
    fun_fu8905809029841901679nt_nat: $tType ).

thf(fun_fu6415725884910174923nt_int_type,type,
    fun_fu6415725884910174923nt_int: $tType ).

thf(fun_fu1143798476471108391nt_int_type,type,
    fun_fu1143798476471108391nt_int: $tType ).

thf(fun_se6298406198028402864t_assn_type,type,
    fun_se6298406198028402864t_assn: $tType ).

thf(fun_ra3995598502166916815at_rat_type,type,
    fun_ra3995598502166916815at_rat: $tType ).

thf(fun_ra5513060666784058567at_rat_type,type,
    fun_ra5513060666784058567at_rat: $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_as3983628580203722482n_assn_type,type,
    fun_as3983628580203722482n_assn: $tType ).

thf(fun_fu1116345184836134341_nat_o_type,type,
    fun_fu1116345184836134341_nat_o: $tType ).

thf(fun_fu2792963925203051945t_assn_type,type,
    fun_fu2792963925203051945t_assn: $tType ).

thf(fun_fu2934462529731303693_int_o_type,type,
    fun_fu2934462529731303693_int_o: $tType ).

thf(fun_fu2048648494261043369t_assn_type,type,
    fun_fu2048648494261043369t_assn: $tType ).

thf(fun_se2170385732985038782_nat_o_type,type,
    fun_se2170385732985038782_nat_o: $tType ).

thf(fun_se2051630309975736070_int_o_type,type,
    fun_se2051630309975736070_int_o: $tType ).

thf(fun_na3711450577076729278_nat_o_type,type,
    fun_na3711450577076729278_nat_o: $tType ).

thf(fun_na7849980549906154535eger_o_type,type,
    fun_na7849980549906154535eger_o: $tType ).

thf(fun_Co7302518231560758906ural_o_type,type,
    fun_Co7302518231560758906ural_o: $tType ).

thf(fun_Co2157892728433036165eger_o_type,type,
    fun_Co2157892728433036165eger_o: $tType ).

thf(fun_Co2081214437782444048eger_o_type,type,
    fun_Co2081214437782444048eger_o: $tType ).

thf(fun_fu2969420921405070251ural_o_type,type,
    fun_fu2969420921405070251ural_o: $tType ).

thf(fun_fu8256284588060503314eger_o_type,type,
    fun_fu8256284588060503314eger_o: $tType ).

thf(fun_fu704708528062463619o_assn_type,type,
    fun_fu704708528062463619o_assn: $tType ).

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

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

thf(fun_fu5934294044791812804_o_nat_type,type,
    fun_fu5934294044791812804_o_nat: $tType ).

thf(fun_fu7564235448449272366at_o_o_type,type,
    fun_fu7564235448449272366at_o_o: $tType ).

thf(fun_fu6971708032831053102nt_o_o_type,type,
    fun_fu6971708032831053102nt_o_o: $tType ).

thf(fun_fu6443148758731022984_o_nat_type,type,
    fun_fu6443148758731022984_o_nat: $tType ).

thf(fun_fu3953065613799296228_o_int_type,type,
    fun_fu3953065613799296228_o_int: $tType ).

thf(fun_fu2630858903579709668_o_nat_type,type,
    fun_fu2630858903579709668_o_nat: $tType ).

thf(fun_fu140775758647982912_o_int_type,type,
    fun_fu140775758647982912_o_int: $tType ).

thf(fun_se2621318847353125966_set_o_type,type,
    fun_se2621318847353125966_set_o: $tType ).

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

thf(fun_op8989173174992673105on_num_type,type,
    fun_op8989173174992673105on_num: $tType ).

thf(fun_op6683169195675693337on_nat_type,type,
    fun_op6683169195675693337on_nat: $tType ).

thf(fun_op4193086050743966581on_int_type,type,
    fun_op4193086050743966581on_int: $tType ).

thf(fun_ra4503298312962071866nt_int_type,type,
    fun_ra4503298312962071866nt_int: $tType ).

thf(fun_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_Pr1652463973008025892nt_rat_type,type,
    fun_Pr1652463973008025892nt_rat: $tType ).

thf(fun_Pr982841511892225912nt_int_type,type,
    fun_Pr982841511892225912nt_int: $tType ).

thf(fun_na1476630412504255114at_nat_type,type,
    fun_na1476630412504255114at_nat: $tType ).

thf(fun_in4514472496968388910at_nat_type,type,
    fun_in4514472496968388910at_nat: $tType ).

thf(fun_in4211310926729683942nt_int_type,type,
    fun_in4211310926729683942nt_int: $tType ).

thf(fun_fu4605530428521801667un_o_o_type,type,
    fun_fu4605530428521801667un_o_o: $tType ).

thf(fun_na819858167508000762st_nat_type,type,
    fun_na819858167508000762st_nat: $tType ).

thf(fun_na7671319193681171066at_nat_type,type,
    fun_na7671319193681171066at_nat: $tType ).

thf(fun_li5614695903105753474at_rat_type,type,
    fun_li5614695903105753474at_rat: $tType ).

thf(fun_li2771310203728655226at_nat_type,type,
    fun_li2771310203728655226at_nat: $tType ).

thf(fun_li281227058796928470at_int_type,type,
    fun_li281227058796928470at_int: $tType ).

thf(fun_li342768494666686942at_rat_type,type,
    fun_li342768494666686942at_rat: $tType ).

thf(fun_li6722754832144364502at_nat_type,type,
    fun_li6722754832144364502at_nat: $tType ).

thf(fun_li4232671687212637746at_int_type,type,
    fun_li4232671687212637746at_int: $tType ).

thf(fun_b_6677255003012645673t_unit_type,type,
    fun_b_6677255003012645673t_unit: $tType ).

thf(fun_a_2990225006182978344t_unit_type,type,
    fun_a_2990225006182978344t_unit: $tType ).

thf(fun_Pr5286341546376896041Heap_b_type,type,
    fun_Pr5286341546376896041Heap_b: $tType ).

thf(fun_Pr5215307506330550056Heap_a_type,type,
    fun_Pr5215307506330550056Heap_a: $tType ).

thf(fun_li3807767012653957926t_assn_type,type,
    fun_li3807767012653957926t_assn: $tType ).

thf(option4624381673175914239nt_int_type,type,
    option4624381673175914239nt_int: $tType ).

thf(filter1242075044329608583at_nat_type,type,
    filter1242075044329608583at_nat: $tType ).

thf(fun_se1179353343636554400at_nat_type,type,
    fun_se1179353343636554400at_nat: $tType ).

thf(fun_se7912642235559603452at_int_type,type,
    fun_se7912642235559603452at_int: $tType ).

thf(fun_se876191773397849432nt_int_type,type,
    fun_se876191773397849432nt_int: $tType ).

thf(fun_se2640714827120536920at_int_type,type,
    fun_se2640714827120536920at_int: $tType ).

thf(fun_se937733209267607904nt_rat_type,type,
    fun_se937733209267607904nt_rat: $tType ).

thf(fun_se7317719546745285464nt_nat_type,type,
    fun_se7317719546745285464nt_nat: $tType ).

thf(fun_se4827636401813558708nt_int_type,type,
    fun_se4827636401813558708nt_int: $tType ).

thf(fun_nu2537414170016844299nteger_type,type,
    fun_nu2537414170016844299nteger: $tType ).

thf(fun_na8135612474337863287nteger_type,type,
    fun_na8135612474337863287nteger: $tType ).

thf(fun_na5492297256294505719er_nat_type,type,
    fun_na5492297256294505719er_nat: $tType ).

thf(fun_na3002214111362778963er_int_type,type,
    fun_na3002214111362778963er_int: $tType ).

thf(fun_na2454419004871237530n_assn_type,type,
    fun_na2454419004871237530n_assn: $tType ).

thf(fun_in2630332840903238488et_nat_type,type,
    fun_in2630332840903238488et_nat: $tType ).

thf(fun_in7040156458970095540et_int_type,type,
    fun_in7040156458970095540et_int: $tType ).

thf(fun_in2718163036992669103er_int_type,type,
    fun_in2718163036992669103er_int: $tType ).

thf(fun_Co3312552843764780407at_nat_type,type,
    fun_Co3312552843764780407at_nat: $tType ).

thf(fun_Co822469698833053651at_int_type,type,
    fun_Co822469698833053651at_int: $tType ).

thf(fun_Co3009391273526075439nt_int_type,type,
    fun_Co3009391273526075439nt_int: $tType ).

thf(set_He475150555083384525t_unit_type,type,
    set_He475150555083384525t_unit: $tType ).

thf(fun_fu7145897819039579925_nat_o_type,type,
    fun_fu7145897819039579925_nat_o: $tType ).

thf(fun_fu5477517762487726877_nat_o_type,type,
    fun_fu5477517762487726877_nat_o: $tType ).

thf(fun_fu8207122332086543297_nat_o_type,type,
    fun_fu8207122332086543297_nat_o: $tType ).

thf(fun_fu3162257917499486297at_rat_type,type,
    fun_fu3162257917499486297at_rat: $tType ).

thf(fun_fu318872218122388049at_nat_type,type,
    fun_fu318872218122388049at_nat: $tType ).

thf(fun_fu7052161110045437101at_int_type,type,
    fun_fu7052161110045437101at_int: $tType ).

thf(fun_fu3473604023002724957_int_o_type,type,
    fun_fu3473604023002724957_int_o: $tType ).

thf(fun_fu1805223966450871909_int_o_type,type,
    fun_fu1805223966450871909_int_o: $tType ).

thf(fun_fu3922030663826099033nt_rat_type,type,
    fun_fu3922030663826099033nt_rat: $tType ).

thf(fun_fu1078644964449000785nt_nat_type,type,
    fun_fu1078644964449000785nt_nat: $tType ).

thf(fun_na7928631014926962227_nat_o_type,type,
    fun_na7928631014926962227_nat_o: $tType ).

thf(fun_in5570076352459579423_int_o_type,type,
    fun_in5570076352459579423_int_o: $tType ).

thf(fun_se6637447080540490323nteger_type,type,
    fun_se6637447080540490323nteger: $tType ).

thf(fun_he6342020312717187381unit_b_type,type,
    fun_he6342020312717187381unit_b: $tType ).

thf(fun_he6342020308413958580unit_a_type,type,
    fun_he6342020308413958580unit_a: $tType ).

thf(fun_assn_option_assn_type,type,
    fun_assn_option_assn: $tType ).

thf(fun_fu7722316861827675049un_o_o_type,type,
    fun_fu7722316861827675049un_o_o: $tType ).

thf(fun_fu3819205551299168222un_o_o_type,type,
    fun_fu3819205551299168222un_o_o: $tType ).

thf(fun_fu7181763470137098718nteger_type,type,
    fun_fu7181763470137098718nteger: $tType ).

thf(list_P6011104703257516679at_nat_type,type,
    list_P6011104703257516679at_nat: $tType ).

thf(list_P3521021558325789923at_int_type,type,
    list_P3521021558325789923at_int: $tType ).

thf(list_P8198026277950538467nt_nat_type,type,
    list_P8198026277950538467nt_nat: $tType ).

thf(list_P5707943133018811711nt_int_type,type,
    list_P5707943133018811711nt_int: $tType ).

thf(fun_fu4625457934454704336_o_nat_type,type,
    fun_fu4625457934454704336_o_nat: $tType ).

thf(fun_he8413527710729349838unit_o_type,type,
    fun_he8413527710729349838unit_o: $tType ).

thf(set_Pr1261947904930325089at_nat_type,type,
    set_Pr1261947904930325089at_nat: $tType ).

thf(set_Pr958786334691620121nt_int_type,type,
    set_Pr958786334691620121nt_int: $tType ).

thf(fun_Pr6331313853612757382_num_o_type,type,
    fun_Pr6331313853612757382_num_o: $tType ).

thf(fun_Pr4796943543331071514_nat_o_type,type,
    fun_Pr4796943543331071514_nat_o: $tType ).

thf(fun_Pr3238374608701176162_int_o_type,type,
    fun_Pr3238374608701176162_int_o: $tType ).

thf(fun_o_8988054265482332260nt_int_type,type,
    fun_o_8988054265482332260nt_int: $tType ).

thf(fun_na7234455742697417626_nat_o_type,type,
    fun_na7234455742697417626_nat_o: $tType ).

thf(fun_li105789395169216470at_rat_type,type,
    fun_li105789395169216470at_rat: $tType ).

thf(fun_li6485775732646894030at_nat_type,type,
    fun_li6485775732646894030at_nat: $tType ).

thf(fun_li3995692587715167274at_int_type,type,
    fun_li3995692587715167274at_int: $tType ).

thf(fun_ar4866611483211206331o_assn_type,type,
    fun_ar4866611483211206331o_assn: $tType ).

thf(fun_assn_fun_b_assn_type,type,
    fun_assn_fun_b_assn: $tType ).

thf(fun_assn_fun_a_assn_type,type,
    fun_assn_fun_a_assn: $tType ).

thf(fun_set_nat_set_nat_type,type,
    fun_set_nat_set_nat: $tType ).

thf(fun_se7586849273513198688nteger_type,type,
    fun_se7586849273513198688nteger: $tType ).

thf(fun_set_int_set_int_type,type,
    fun_set_int_set_int: $tType ).

thf(fun_int_set_set_nat_type,type,
    fun_int_set_set_nat: $tType ).

thf(fun_Co7398788559141407565atural_type,type,
    fun_Co7398788559141407565atural: $tType ).

thf(fun_Co3734316457315071362atural_type,type,
    fun_Co3734316457315071362atural: $tType ).

thf(fun_Co8499238673658658103nteger_type,type,
    fun_Co8499238673658658103nteger: $tType ).

thf(fun_se382663106265794036_nat_o_type,type,
    fun_se382663106265794036_nat_o: $tType ).

thf(fun_se867122708194164540_int_o_type,type,
    fun_se867122708194164540_int_o: $tType ).

thf(fun_na8563630686737515764_nat_o_type,type,
    fun_na8563630686737515764_nat_o: $tType ).

thf(fun_na8635581178960477080_int_o_type,type,
    fun_na8635581178960477080_int_o: $tType ).

thf(fun_na6318815019539281885eger_o_type,type,
    fun_na6318815019539281885eger_o: $tType ).

thf(fun_in4068701459849370962_set_o_type,type,
    fun_in4068701459849370962_set_o: $tType ).

thf(fun_in4891666191172872833eger_o_type,type,
    fun_in4891666191172872833eger_o: $tType ).

thf(fun_Co196715998180962002_nat_o_type,type,
    fun_Co196715998180962002_nat_o: $tType ).

thf(fun_Co7174943067365291894_int_o_type,type,
    fun_Co7174943067365291894_int_o: $tType ).

thf(fun_Co1375048237525739357_nat_o_type,type,
    fun_Co1375048237525739357_nat_o: $tType ).

thf(fun_Co8353275306710069249_int_o_type,type,
    fun_Co8353275306710069249_int_o: $tType ).

thf(fun_assn_fun_assn_o_type,type,
    fun_assn_fun_assn_o: $tType ).

thf(fun_fu4001317426178549763_nat_o_type,type,
    fun_fu4001317426178549763_nat_o: $tType ).

thf(fun_fu3883539188510166275_int_o_type,type,
    fun_fu3883539188510166275_int_o: $tType ).

thf(fun_fu1989461620956114563_o_rat_type,type,
    fun_fu1989461620956114563_o_rat: $tType ).

thf(fun_fu6701067901881939075_o_nat_type,type,
    fun_fu6701067901881939075_o_nat: $tType ).

thf(fun_fu6940589326549028739_o_int_type,type,
    fun_fu6940589326549028739_o_int: $tType ).

thf(fun_set_o_fun_o_assn_type,type,
    fun_set_o_fun_o_assn: $tType ).

thf(heap_T3836121109492952855ay_nat_type,type,
    heap_T3836121109492952855ay_nat: $tType ).

thf(heap_T1346037964561226099ay_int_type,type,
    heap_T1346037964561226099ay_int: $tType ).

thf(fun_fu3143923321121214633un_o_o_type,type,
    fun_fu3143923321121214633un_o_o: $tType ).

thf(fun_fu7714003655882793385o_assn_type,type,
    fun_fu7714003655882793385o_assn: $tType ).

thf(fun_se5038631536132265326et_o_o_type,type,
    fun_se5038631536132265326et_o_o: $tType ).

thf(list_P7333126701944960589_nat_o_type,type,
    list_P7333126701944960589_nat_o: $tType ).

thf(list_P5087981734274514673_int_o_type,type,
    list_P5087981734274514673_int_o: $tType ).

thf(list_P6285523579766656935_o_nat_type,type,
    list_P6285523579766656935_o_nat: $tType ).

thf(list_P3795440434834930179_o_int_type,type,
    list_P3795440434834930179_o_int: $tType ).

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

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

thf(produc6271795597528267376eger_o_type,type,
    produc6271795597528267376eger_o: $tType ).

thf(fun_set_list_nat_o_type,type,
    fun_set_list_nat_o: $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_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_nat_type,type,
    fun_nat_fun_int_nat: $tType ).

thf(fun_nat_fun_int_int_type,type,
    fun_nat_fun_int_int: $tType ).

thf(fun_int_fun_nat_nat_type,type,
    fun_int_fun_nat_nat: $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_Co4490034186337852034r_assn_type,type,
    fun_Co4490034186337852034r_assn: $tType ).

thf(set_set_set_nat_type,type,
    set_set_set_nat: $tType ).

thf(set_set_Code_integer_type,type,
    set_set_Code_integer: $tType ).

thf(heap_T5738788834812785303t_unit_type,type,
    heap_T5738788834812785303t_unit: $tType ).

thf(fun_set_set_nat_o_type,type,
    fun_set_set_nat_o: $tType ).

thf(fun_se7289222521248229150eger_o_type,type,
    fun_se7289222521248229150eger_o: $tType ).

thf(fun_set_o_fun_o_rat_type,type,
    fun_set_o_fun_o_rat: $tType ).

thf(fun_set_o_fun_o_nat_type,type,
    fun_set_o_fun_o_nat: $tType ).

thf(fun_set_o_fun_o_int_type,type,
    fun_set_o_fun_o_int: $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_int_nat_type,type,
    fun_option_int_nat: $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_Co480733329897759773un_o_o_type,type,
    fun_Co480733329897759773un_o_o: $tType ).

thf(fun_o_4021313873839786239eger_o_type,type,
    fun_o_4021313873839786239eger_o: $tType ).

thf(fun_b_8426044978055006235Heap_b_type,type,
    fun_b_8426044978055006235Heap_b: $tType ).

thf(fun_b_8355010938008660250Heap_a_type,type,
    fun_b_8355010938008660250Heap_a: $tType ).

thf(fun_a_6164325696594227994Heap_b_type,type,
    fun_a_6164325696594227994Heap_b: $tType ).

thf(fun_a_6093291656547882009Heap_a_type,type,
    fun_a_6093291656547882009Heap_a: $tType ).

thf(fun_fu6337961365400742745un_o_o_type,type,
    fun_fu6337961365400742745un_o_o: $tType ).

thf(fun_fu6781074197733401937un_o_o_type,type,
    fun_fu6781074197733401937un_o_o: $tType ).

thf(fun_fu7756609662939579309un_o_o_type,type,
    fun_fu7756609662939579309un_o_o: $tType ).

thf(fun_fu830079035465870425_o_rat_type,type,
    fun_fu830079035465870425_o_rat: $tType ).

thf(fun_fu7210065372943547985_o_nat_type,type,
    fun_fu7210065372943547985_o_nat: $tType ).

thf(fun_Pr6626665806141890376t_assn_type,type,
    fun_Pr6626665806141890376t_assn: $tType ).

thf(set_Product_prod_b_b_type,type,
    set_Product_prod_b_b: $tType ).

thf(set_Product_prod_a_a_type,type,
    set_Product_prod_a_a: $tType ).

thf(heap_T5660665574680485309rray_o_type,type,
    heap_T5660665574680485309rray_o: $tType ).

thf(heap_e7401611519738050253t_unit_type,type,
    heap_e7401611519738050253t_unit: $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_nat_type,type,
    product_prod_int_nat: $tType ).

thf(product_prod_int_int_type,type,
    product_prod_int_int: $tType ).

thf(list_P4002435161011370285od_o_o_type,type,
    list_P4002435161011370285od_o_o: $tType ).

thf(fun_b_fun_b_assn_type,type,
    fun_b_fun_b_assn: $tType ).

thf(fun_a_fun_a_assn_type,type,
    fun_a_fun_a_assn: $tType ).

thf(fun_nat_list_nat_type,type,
    fun_nat_list_nat: $tType ).

thf(fun_list_nat_rat_type,type,
    fun_list_nat_rat: $tType ).

thf(fun_list_nat_nat_type,type,
    fun_list_nat_nat: $tType ).

thf(fun_list_nat_int_type,type,
    fun_list_nat_int: $tType ).

thf(set_Product_prod_o_o_type,type,
    set_Product_prod_o_o: $tType ).

thf(fun_set_nat_rat_type,type,
    fun_set_nat_rat: $tType ).

thf(fun_set_nat_nat_type,type,
    fun_set_nat_nat: $tType ).

thf(fun_set_nat_int_type,type,
    fun_set_nat_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(list_option_num_type,type,
    list_option_num: $tType ).

thf(fun_fun_rat_rat_o_type,type,
    fun_fun_rat_rat_o: $tType ).

thf(fun_fun_int_int_o_type,type,
    fun_fun_int_int_o: $tType ).

thf(fun_rat_fun_rat_o_type,type,
    fun_rat_fun_rat_o: $tType ).

thf(fun_num_fun_num_o_type,type,
    fun_num_fun_num_o: $tType ).

thf(fun_nat_fun_nat_o_type,type,
    fun_nat_fun_nat_o: $tType ).

thf(fun_nat_fun_int_o_type,type,
    fun_nat_fun_int_o: $tType ).

thf(fun_nat_fun_o_nat_type,type,
    fun_nat_fun_o_nat: $tType ).

thf(fun_nat_fun_o_int_type,type,
    fun_nat_fun_o_int: $tType ).

thf(fun_int_fun_nat_o_type,type,
    fun_int_fun_nat_o: $tType ).

thf(fun_int_fun_int_o_type,type,
    fun_int_fun_int_o: $tType ).

thf(fun_int_fun_o_int_type,type,
    fun_int_fun_o_int: $tType ).

thf(fun_o_fun_nat_nat_type,type,
    fun_o_fun_nat_nat: $tType ).

thf(fun_o_fun_nat_int_type,type,
    fun_o_fun_nat_int: $tType ).

thf(fun_o_fun_int_int_type,type,
    fun_o_fun_int_int: $tType ).

thf(fun_set_o_set_o_type,type,
    fun_set_o_set_o: $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(filter_set_nat_type,type,
    filter_set_nat: $tType ).

thf(fun_set_o_fun_o_o_type,type,
    fun_set_o_fun_o_o: $tType ).

thf(fun_Product_unit_nat_type,type,
    fun_Product_unit_nat: $tType ).

thf(fun_option_num_o_type,type,
    fun_option_num_o: $tType ).

thf(fun_o_option_num_type,type,
    fun_o_option_num: $tType ).

thf(fun_fun_o_o_fun_o_o_type,type,
    fun_fun_o_o_fun_o_o: $tType ).

thf(heap_Time_Heap_nat_type,type,
    heap_Time_Heap_nat: $tType ).

thf(heap_Time_Heap_int_type,type,
    heap_Time_Heap_int: $tType ).

thf(set_list_nat_type,type,
    set_list_nat: $tType ).

thf(set_list_int_type,type,
    set_list_int: $tType ).

thf(product_prod_nat_o_type,type,
    product_prod_nat_o: $tType ).

thf(product_prod_int_o_type,type,
    product_prod_int_o: $tType ).

thf(product_prod_o_nat_type,type,
    product_prod_o_nat: $tType ).

thf(product_prod_o_int_type,type,
    product_prod_o_int: $tType ).

thf(fun_list_nat_o_type,type,
    fun_list_nat_o: $tType ).

thf(fun_list_int_o_type,type,
    fun_list_int_o: $tType ).

thf(fun_rat_assn_type,type,
    fun_rat_assn: $tType ).

thf(fun_num_assn_type,type,
    fun_num_assn: $tType ).

thf(fun_nat_assn_type,type,
    fun_nat_assn: $tType ).

thf(fun_int_assn_type,type,
    fun_int_assn: $tType ).

thf(fun_assn_rat_type,type,
    fun_assn_rat: $tType ).

thf(fun_assn_num_type,type,
    fun_assn_num: $tType ).

thf(fun_assn_nat_type,type,
    fun_assn_nat: $tType ).

thf(fun_assn_int_type,type,
    fun_assn_int: $tType ).

thf(set_set_nat_type,type,
    set_set_nat: $tType ).

thf(set_set_int_type,type,
    set_set_int: $tType ).

thf(set_Code_integer_type,type,
    set_Code_integer: $tType ).

thf(array_Product_unit_type,type,
    array_Product_unit: $tType ).

thf(fun_set_rat_o_type,type,
    fun_set_rat_o: $tType ).

thf(fun_set_num_o_type,type,
    fun_set_num_o: $tType ).

thf(fun_set_nat_o_type,type,
    fun_set_nat_o: $tType ).

thf(fun_set_int_o_type,type,
    fun_set_int_o: $tType ).

thf(fun_int_set_o_type,type,
    fun_int_set_o: $tType ).

thf(fun_Code_natural_o_type,type,
    fun_Code_natural_o: $tType ).

thf(fun_Code_integer_o_type,type,
    fun_Code_integer_o: $tType ).

thf(fun_o_Code_natural_type,type,
    fun_o_Code_natural: $tType ).

thf(fun_o_Code_integer_type,type,
    fun_o_Code_integer: $tType ).

thf(list_Product_unit_type,type,
    list_Product_unit: $tType ).

thf(fun_nat_fun_o_o_type,type,
    fun_nat_fun_o_o: $tType ).

thf(fun_int_fun_o_o_type,type,
    fun_int_fun_o_o: $tType ).

thf(fun_o_fun_nat_o_type,type,
    fun_o_fun_nat_o: $tType ).

thf(fun_o_fun_int_o_type,type,
    fun_o_fun_int_o: $tType ).

thf(option_assn_type,type,
    option_assn: $tType ).

thf(ref_Product_unit_type,type,
    ref_Product_unit: $tType ).

thf(set_Product_unit_type,type,
    set_Product_unit: $tType ).

thf(product_prod_b_b_type,type,
    product_prod_b_b: $tType ).

thf(product_prod_a_a_type,type,
    product_prod_a_a: $tType ).

thf(option_set_o_type,type,
    option_set_o: $tType ).

thf(fun_Product_unit_o_type,type,
    fun_Product_unit_o: $tType ).

thf(fun_o_Product_unit_type,type,
    fun_o_Product_unit: $tType ).

thf(heap_Time_Heap_b_type,type,
    heap_Time_Heap_b: $tType ).

thf(heap_Time_Heap_a_type,type,
    heap_Time_Heap_a: $tType ).

thf(heap_Time_Heap_o_type,type,
    heap_Time_Heap_o: $tType ).

thf(fun_b_assn_type,type,
    fun_b_assn: $tType ).

thf(fun_a_assn_type,type,
    fun_a_assn: $tType ).

thf(set_list_o_type,type,
    set_list_o: $tType ).

thf(product_prod_o_o_type,type,
    product_prod_o_o: $tType ).

thf(fun_rat_rat_type,type,
    fun_rat_rat: $tType ).

thf(fun_rat_num_type,type,
    fun_rat_num: $tType ).

thf(fun_rat_nat_type,type,
    fun_rat_nat: $tType ).

thf(fun_rat_int_type,type,
    fun_rat_int: $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_list_o_o_type,type,
    fun_list_o_o: $tType ).

thf(fun_int_rat_type,type,
    fun_int_rat: $tType ).

thf(fun_int_num_type,type,
    fun_int_num: $tType ).

thf(fun_int_nat_type,type,
    fun_int_nat: $tType ).

thf(fun_int_int_type,type,
    fun_int_int: $tType ).

thf(set_assn_type,type,
    set_assn: $tType ).

thf(fun_assn_o_type,type,
    fun_assn_o: $tType ).

thf(fun_o_assn_type,type,
    fun_o_assn: $tType ).

thf(fun_set_o_o_type,type,
    fun_set_o_o: $tType ).

thf(option_rat_type,type,
    option_rat: $tType ).

thf(option_num_type,type,
    option_num: $tType ).

thf(option_nat_type,type,
    option_nat: $tType ).

thf(option_int_type,type,
    option_int: $tType ).

thf(list_char_type,type,
    list_char: $tType ).

thf(filter_nat_type,type,
    filter_nat: $tType ).

thf(fun_o_fun_o_o_type,type,
    fun_o_fun_o_o: $tType ).

thf(array_nat_type,type,
    array_nat: $tType ).

thf(array_int_type,type,
    array_int: $tType ).

thf(list_rat_type,type,
    list_rat: $tType ).

thf(list_num_type,type,
    list_num: $tType ).

thf(list_nat_type,type,
    list_nat: $tType ).

thf(list_int_type,type,
    list_int: $tType ).

thf(set_rat_type,type,
    set_rat: $tType ).

thf(set_num_type,type,
    set_num: $tType ).

thf(set_nat_type,type,
    set_nat: $tType ).

thf(set_int_type,type,
    set_int: $tType ).

thf(code_natural_type,type,
    code_natural: $tType ).

thf(code_integer_type,type,
    code_integer: $tType ).

thf(fun_rat_o_type,type,
    fun_rat_o: $tType ).

thf(fun_num_o_type,type,
    fun_num_o: $tType ).

thf(fun_nat_o_type,type,
    fun_nat_o: $tType ).

thf(fun_int_o_type,type,
    fun_int_o: $tType ).

thf(fun_o_rat_type,type,
    fun_o_rat: $tType ).

thf(fun_o_num_type,type,
    fun_o_num: $tType ).

thf(fun_o_nat_type,type,
    fun_o_nat: $tType ).

thf(fun_o_int_type,type,
    fun_o_int: $tType ).

thf(product_unit_type,type,
    product_unit: $tType ).

thf(option_o_type,type,
    option_o: $tType ).

thf(list_b_type,type,
    list_b: $tType ).

thf(list_a_type,type,
    list_a: $tType ).

thf(array_o_type,type,
    array_o: $tType ).

thf(list_o_type,type,
    list_o: $tType ).

thf(fun_b_o_type,type,
    fun_b_o: $tType ).

thf(fun_a_o_type,type,
    fun_a_o: $tType ).

thf(assn_type,type,
    assn: $tType ).

thf(set_o_type,type,
    set_o: $tType ).

thf(fun_o_o_type,type,
    fun_o_o: $tType ).

thf(char_type,type,
    char: $tType ).

thf(rat_type,type,
    rat: $tType ).

thf(num_type,type,
    num: $tType ).

thf(nat_type,type,
    nat: $tType ).

thf(int_type,type,
    int: $tType ).

thf(b_type,type,
    b: $tType ).

thf(a_type,type,
    a: $tType ).

thf(aTP_Lamm_ey_decl,type,
    aTP_Lamm_ey: fun_Pr6626665806141890376t_assn ).

thf(aTP_Lamm_gt_decl,type,
    aTP_Lamm_gt: fun_Pr6460944699146269935_nat_o ).

thf(aTP_Lamm_gu_decl,type,
    aTP_Lamm_gu: assn > fun_as3747249873083764768_nat_o ).

thf(aTP_Lamm_gv_decl,type,
    aTP_Lamm_gv: assn > fun_as3747249873083764768_nat_o ).

thf(aTP_Lamm_ho_decl,type,
    aTP_Lamm_ho: assn > fun_Pr6460944699146269935_nat_o ).

thf(abs_assn_decl,type,
    abs_assn: fun_Pr6460944699146269935_nat_o > assn ).

thf(rep_assn_decl,type,
    rep_assn: assn > fun_Pr6460944699146269935_nat_o ).

thf(entails_decl,type,
    entails: assn > assn > $o ).

thf(in_range_decl,type,
    in_range: fun_Pr6460944699146269935_nat_o ).

thf(one_assn_raw_decl,type,
    one_assn_raw: fun_Pr6460944699146269935_nat_o ).

thf(pure_a825153325127701367it_nat_decl,type,
    pure_a825153325127701367it_nat: $o > fun_Pr6460944699146269935_nat_o ).

thf(relH_decl,type,
    relH: set_nat > heap_e7401611519738050253t_unit > fun_he8413527710729349838unit_o ).

thf(one_one_assn_decl,type,
    one_one_assn: assn ).

thf(heap_T6553295506729943825t_unit_decl,type,
    heap_T6553295506729943825t_unit: heap_T5738788834812785303t_unit > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > product_unit > fun_nat_o ).

thf(heap_Time_effect_a_decl,type,
    heap_Time_effect_a: heap_Time_Heap_a > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > a > fun_nat_o ).

thf(heap_Time_effect_b_decl,type,
    heap_Time_effect_b: heap_Time_Heap_b > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > b > fun_nat_o ).

thf(heap_T584514906347983379t_unit_decl,type,
    heap_T584514906347983379t_unit: heap_T5738788834812785303t_unit > fun_he8413527710729349838unit_o ).

thf(heap_Time_success_a_decl,type,
    heap_Time_success_a: heap_Time_Heap_a > fun_he8413527710729349838unit_o ).

thf(heap_Time_success_b_decl,type,
    heap_Time_success_b: heap_Time_Heap_b > fun_he8413527710729349838unit_o ).

thf(hoare_8945653483474564448t_unit_decl,type,
    hoare_8945653483474564448t_unit: assn > heap_T5738788834812785303t_unit > fun_Pr6626665806141890376t_assn > $o ).

thf(hoare_hoare_triple_a_decl,type,
    hoare_hoare_triple_a: assn > heap_Time_Heap_a > fun_a_assn > $o ).

thf(hoare_hoare_triple_b_decl,type,
    hoare_hoare_triple_b: assn > heap_Time_Heap_b > fun_b_assn > $o ).

thf(hoare_new_addrs_decl,type,
    hoare_new_addrs: heap_e7401611519738050253t_unit > set_nat > heap_e7401611519738050253t_unit > set_nat ).

thf(bot_bot_assn_decl,type,
    bot_bot_assn: assn ).

thf(bot_bot_set_nat_decl,type,
    bot_bot_set_nat: set_nat ).

thf(top_top_assn_decl,type,
    top_top_assn: assn ).

thf(produc7507926704131184380et_nat_decl,type,
    produc7507926704131184380et_nat: heap_e7401611519738050253t_unit > set_nat > produc3658429121746597890et_nat ).

thf(produc8586169260539613262et_nat_decl,type,
    produc8586169260539613262et_nat: produc3658429121746597890et_nat > set_nat ).

thf(aa_ass4243947775541419017_nat_o_decl,type,
    aa_ass4243947775541419017_nat_o: fun_as3747249873083764768_nat_o > assn > fun_Pr6460944699146269935_nat_o ).

thf(aa_hea7994211679605476167unit_o_decl,type,
    aa_hea7994211679605476167unit_o: fun_he8413527710729349838unit_o > heap_e7401611519738050253t_unit > $o ).

thf(aa_nat_o_decl,type,
    aa_nat_o: fun_nat_o > nat > $o ).

thf(aa_Pro653082453696054616_nat_o_decl,type,
    aa_Pro653082453696054616_nat_o: fun_Pr6460944699146269935_nat_o > produc3658429121746597890et_nat > $o ).

thf(aa_Product_unit_assn_decl,type,
    aa_Product_unit_assn: fun_Pr6626665806141890376t_assn > product_unit > assn ).

thf(aa_a_assn_decl,type,
    aa_a_assn: fun_a_assn > a > assn ).

thf(aa_a_H8829438778223708363Heap_b_decl,type,
    aa_a_H8829438778223708363Heap_b: fun_a_6164325696594227994Heap_b > a > heap_Time_Heap_b ).

thf(aa_b_assn_decl,type,
    aa_b_assn: fun_b_assn > b > assn ).

thf(p_decl,type,
    p: assn ).

thf(q_decl,type,
    q: fun_b_assn ).

thf(r_decl,type,
    r: fun_a_assn ).

thf(as_decl,type,
    as: set_nat ).

thf(f_decl,type,
    f: heap_Time_Heap_a ).

thf(g_decl,type,
    g: fun_a_6164325696594227994Heap_b ).

thf(h_decl,type,
    h: heap_e7401611519738050253t_unit ).

thf(h2_decl,type,
    h2: heap_e7401611519738050253t_unit ).

thf(h3_decl,type,
    h3: heap_e7401611519738050253t_unit ).

thf(rf_decl,type,
    rf: a ).

thf(rg_decl,type,
    rg: b ).

thf(58,axiom,
    ! [A: produc3658429121746597890et_nat,B: $o] :
      ( ( ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
      <=> B )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( A
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ( B
            <=> ( D != bot_bot_set_nat ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10200_one__assn__raw_Oelims_I1_J) ).

thf(320,plain,
    ! [A: produc3658429121746597890et_nat,B: $o] :
      ( ( ( B
         => ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) ) )
        & ( ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
         => B ) )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( A
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ( ( ( D != bot_bot_set_nat )
               => B )
              & ( B
               => ( D != bot_bot_set_nat ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).

thf(70,axiom,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) )
     => ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_hoare__triple__preI) ).

thf(372,plain,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) )
     => ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).

thf(35,axiom,
    ! [A: heap_Time_Heap_b,B: fun_b_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_hoare_triple_b ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1995_false__rule) ).

thf(165,plain,
    ! [A: heap_Time_Heap_b,B: fun_b_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_hoare_triple_b ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).

thf(63,axiom,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) )
     => ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_hoare__triple__preI) ).

thf(343,plain,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) )
     => ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).

thf(6,axiom,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( A @ ( B @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3655_relH__in__rangeI_I1_J) ).

thf(86,plain,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( A @ ( B @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).

thf(31,axiom,
    ! [A: assn,B: assn,C: fun_Pr6626665806141890376t_assn,D: fun_Pr6626665806141890376t_assn,E: heap_T5738788834812785303t_unit] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: product_unit] : ( F @ ( D @ aa_Product_unit_assn ) @ ( F @ ( C @ aa_Product_unit_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_8945653483474564448t_unit ) ) )
         => ( D @ ( E @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2522_cons__rule) ).

thf(155,plain,
    ! [A: assn,B: assn,C: fun_Pr6626665806141890376t_assn,D: fun_Pr6626665806141890376t_assn,E: heap_T5738788834812785303t_unit] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: product_unit] : ( F @ ( D @ aa_Product_unit_assn ) @ ( F @ ( C @ aa_Product_unit_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_8945653483474564448t_unit ) ) )
         => ( D @ ( E @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).

thf(62,axiom,
    h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ produc7507926704131184380et_nat ) @ ( rf @ ( r @ aa_a_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_POST__F) ).

thf(342,plain,
    h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ produc7507926704131184380et_nat ) @ ( rf @ ( r @ aa_a_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).

thf(34,axiom,
    ! [A: heap_T5738788834812785303t_unit,B: fun_Pr6626665806141890376t_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_8945653483474564448t_unit ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1996_false__rule) ).

thf(163,plain,
    ! [A: heap_T5738788834812785303t_unit,B: fun_Pr6626665806141890376t_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_8945653483474564448t_unit ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).

thf(24,axiom,
    ! [A: assn,B: assn,C: assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( C @ ( B @ entails ) )
       => ( C @ ( A @ entails ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2311_ent__trans) ).

thf(138,plain,
    ! [A: assn,B: assn,C: assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( C @ ( B @ entails ) )
       => ( C @ ( A @ entails ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).

thf(12,axiom,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: fun_a_assn] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ! [E: a] : ( E @ ( D @ aa_a_assn ) @ ( E @ ( C @ aa_a_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2517_cons__post__rule) ).

thf(101,plain,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: fun_a_assn] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ! [E: a] : ( E @ ( D @ aa_a_assn ) @ ( E @ ( C @ aa_a_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_hoare_triple_a ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).

thf(43,axiom,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: product_unit,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_Product_unit_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_T6553295506729943825t_unit ) ) ) @ aa_nat_o ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_hoare__triple__effect) ).

thf(234,plain,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: product_unit,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_Product_unit_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_T6553295506729943825t_unit ) ) ) @ aa_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).

thf(76,axiom,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( C @ ( B @ ( A @ aTP_Lamm_gu @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) )
    <=> ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
        | ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10681_ATP_Olambda__475) ).

thf(408,plain,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          | ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
       => ( C @ ( B @ ( A @ aTP_Lamm_gu @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( C @ ( B @ ( A @ aTP_Lamm_gu @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) )
       => ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          | ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).

thf(39,axiom,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) )
     => ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_hoare__triple__preI) ).

thf(202,plain,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn] :
      ( ! [D: produc3658429121746597890et_nat] :
          ( ( D @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) )
     => ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).

thf(77,axiom,
    ! [A: assn,B: produc3658429121746597890et_nat,C: assn] :
      ( ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
     => ( ( C @ ( A @ entails ) )
       => ( B @ ( C @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2498_ent__fwd) ).

thf(416,plain,
    ! [A: assn,B: produc3658429121746597890et_nat,C: assn] :
      ( ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
     => ( ( C @ ( A @ entails ) )
       => ( B @ ( C @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).

thf(1,conjecture,
    h @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h @ produc7507926704131184380et_nat ) @ ( rg @ ( q @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

thf(2,negated_conjecture,
    ~ ( h @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h @ produc7507926704131184380et_nat ) @ ( rg @ ( q @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    inference(neg_conjecture,[status(cth)],[1]) ).

thf(78,plain,
    ~ ( h @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h @ produc7507926704131184380et_nat ) @ ( rg @ ( q @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(64,axiom,
    ! [A: assn,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( bot_bot_set_nat @ ( B @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
    <=> ( bot_bot_set_nat @ ( C @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1965_mod__h__bot__indep) ).

thf(348,plain,
    ! [A: assn,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( ( bot_bot_set_nat @ ( C @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( bot_bot_set_nat @ ( B @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( bot_bot_set_nat @ ( B @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( bot_bot_set_nat @ ( C @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).

thf(5,axiom,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( B @ ( C @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_332_relH__sym) ).

thf(84,plain,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( B @ ( C @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).

thf(75,axiom,
    ! [A: $o,B: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( B
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ~ ( A
                & ( D = bot_bot_set_nat ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2140_pure__assn__raw_Oelims_I2_J) ).

thf(396,plain,
    ! [A: $o,B: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( B
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ~ ( A
                & ( D = bot_bot_set_nat ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).

thf(7,axiom,
    ! [A: product_unit] :
      ( ( A @ ( aTP_Lamm_ey @ aa_Product_unit_assn ) )
      = one_one_assn ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11289_ATP_Olambda__1083) ).

thf(89,plain,
    ! [A: product_unit] :
      ( ( A @ ( aTP_Lamm_ey @ aa_Product_unit_assn ) )
      = one_one_assn ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).

thf(18,axiom,
    ! [A: assn,B: assn,C: heap_Time_Heap_a,D: fun_a_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_hoare_triple_a ) ) )
       => ( D @ ( C @ ( A @ hoare_hoare_triple_a ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2566_cons__pre__rule) ).

thf(116,plain,
    ! [A: assn,B: assn,C: heap_Time_Heap_a,D: fun_a_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_hoare_triple_a ) ) )
       => ( D @ ( C @ ( A @ hoare_hoare_triple_a ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).

thf(72,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ( ~ ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
            ( ( A
              = ( C @ ( B @ produc7507926704131184380et_nat ) ) )
           => ( C = bot_bot_set_nat ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10202_one__assn__raw_Oelims_I3_J) ).

thf(380,plain,
    ! [A: produc3658429121746597890et_nat] :
      ( ~ ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
            ( ( A
              = ( C @ ( B @ produc7507926704131184380et_nat ) ) )
           => ( C = bot_bot_set_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).

thf(38,axiom,
    h @ ( h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ hoare_new_addrs ) ) @ ( h @ produc7507926704131184380et_nat ) @ ( rg @ ( q @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_POST__G) ).

thf(201,plain,
    h @ ( h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ hoare_new_addrs ) ) @ ( h @ produc7507926704131184380et_nat ) @ ( rg @ ( q @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).

thf(8,axiom,
    top_top_assn != one_one_assn,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9956_assn__basic__inequalities_I1_J) ).

thf(92,plain,
    top_top_assn != one_one_assn,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).

thf(46,axiom,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( top_top_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9965_mod__h__bot__iff_I2_J) ).

thf(252,plain,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( top_top_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).

thf(10,axiom,
    ! [A: assn] : ( A @ ( bot_bot_assn @ entails ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2533_ent__false) ).

thf(97,plain,
    ! [A: assn] : ( A @ ( bot_bot_assn @ entails ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).

thf(53,axiom,
    ! [A: $o,B: produc3658429121746597890et_nat] :
      ( ~ ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( B
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ( A
              & ( D = bot_bot_set_nat ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2691_pure__assn__raw_Oelims_I3_J) ).

thf(285,plain,
    ! [A: $o,B: produc3658429121746597890et_nat] :
      ( ~ ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [C: heap_e7401611519738050253t_unit,D: set_nat] :
            ( ( B
              = ( D @ ( C @ produc7507926704131184380et_nat ) ) )
           => ( A
              & ( D = bot_bot_set_nat ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).

thf(42,axiom,
    ! [A: assn,B: assn] :
      ( ( ( A @ rep_assn )
        = ( B @ rep_assn ) )
    <=> ( A = B ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_Rep__assn__inject) ).

thf(224,plain,
    ! [A: assn,B: assn] :
      ( ( ( A = B )
       => ( ( A @ rep_assn )
          = ( B @ rep_assn ) ) )
      & ( ( ( A @ rep_assn )
          = ( B @ rep_assn ) )
       => ( A = B ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).

thf(74,axiom,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( B @ ( A @ produc7507926704131184380et_nat ) @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
    <=> ( B = bot_bot_set_nat ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10199_one__assn__raw_Osimps) ).

thf(388,plain,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( ( B = bot_bot_set_nat )
       => ( B @ ( A @ produc7507926704131184380et_nat ) @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( B @ ( A @ produc7507926704131184380et_nat ) @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
       => ( B = bot_bot_set_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).

thf(66,axiom,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( A @ ( B @ ( A @ hoare_new_addrs ) ) )
      = B ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_new__addr__refl) ).

thf(356,plain,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( A @ ( B @ ( A @ hoare_new_addrs ) ) )
      = B ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).

thf(25,axiom,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( B @ ( A @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) )
     => ( A @ ( A @ ( B @ relH ) @ aa_hea7994211679605476167unit_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3656_relH__refl) ).

thf(141,plain,
    ! [A: heap_e7401611519738050253t_unit,B: set_nat] :
      ( ( B @ ( A @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) )
     => ( A @ ( A @ ( B @ relH ) @ aa_hea7994211679605476167unit_o ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).

thf(15,axiom,
    ! [A: assn] : ( top_top_assn @ ( A @ entails ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9960_ent__true) ).

thf(109,plain,
    ! [A: assn] : ( top_top_assn @ ( A @ entails ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).

thf(21,axiom,
    ! [A: assn,B: assn,C: heap_T5738788834812785303t_unit,D: fun_Pr6626665806141890376t_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_8945653483474564448t_unit ) ) )
       => ( D @ ( C @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2568_cons__pre__rule) ).

thf(124,plain,
    ! [A: assn,B: assn,C: heap_T5738788834812785303t_unit,D: fun_Pr6626665806141890376t_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_8945653483474564448t_unit ) ) )
       => ( D @ ( C @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).

thf(54,axiom,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: a,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_a_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_Time_effect_a ) ) ) @ aa_nat_o ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_hoare__triple__effect) ).

thf(298,plain,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: a,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_a_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_Time_effect_a ) ) ) @ aa_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).

thf(28,axiom,
    top_top_assn != bot_bot_assn,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9957_assn__basic__inequalities_I5_J) ).

thf(148,plain,
    top_top_assn != bot_bot_assn,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).

thf(49,axiom,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_Time_success_b @ aa_hea7994211679605476167unit_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_hoare__triple__success) ).

thf(264,plain,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_Time_success_b @ aa_hea7994211679605476167unit_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).

thf(33,axiom,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( A @ ( C @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3654_relH__in__rangeI_I2_J) ).

thf(161,plain,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( A @ ( C @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).

thf(52,axiom,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: assn] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( ( A @ ( B @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
      <=> ( A @ ( C @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_548_mod__relH) ).

thf(279,plain,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: assn] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( ( ( A @ ( C @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( A @ ( B @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
        & ( ( A @ ( B @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( A @ ( C @ produc7507926704131184380et_nat ) @ ( D @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).

thf(51,axiom,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: b,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_Time_effect_b ) ) ) @ aa_nat_o ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_hoare__triple__effect) ).

thf(274,plain,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ? [F: heap_e7401611519738050253t_unit,G: b,H: nat] :
            ( ( F @ ( E @ ( D @ hoare_new_addrs ) ) @ ( F @ produc7507926704131184380et_nat ) @ ( G @ ( C @ aa_b_assn ) @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
            & ( H @ ( G @ ( F @ ( D @ ( B @ heap_Time_effect_b ) ) ) @ aa_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).

thf(4,axiom,
    ! [A: assn,B: assn,C: heap_Time_Heap_b,D: fun_b_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_hoare_triple_b ) ) )
       => ( D @ ( C @ ( A @ hoare_hoare_triple_b ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2567_cons__pre__rule) ).

thf(81,plain,
    ! [A: assn,B: assn,C: heap_Time_Heap_b,D: fun_b_assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( D @ ( C @ ( B @ hoare_hoare_triple_b ) ) )
       => ( D @ ( C @ ( A @ hoare_hoare_triple_b ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).

thf(71,axiom,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ entails ) )
     => ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2499_entailsD) ).

thf(377,plain,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ entails ) )
     => ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).

thf(68,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ( ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
            ( ( A
              = ( C @ ( B @ produc7507926704131184380et_nat ) ) )
           => ( C != bot_bot_set_nat ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10201_one__assn__raw_Oelims_I2_J) ).

thf(362,plain,
    ! [A: produc3658429121746597890et_nat] :
      ( ( A @ ( one_assn_raw @ aa_Pro653082453696054616_nat_o ) )
     => ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
            ( ( A
              = ( C @ ( B @ produc7507926704131184380et_nat ) ) )
           => ( C != bot_bot_set_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).

thf(55,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ~ ( A @ ( bot_bot_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2018_mod__false) ).

thf(303,plain,
    ! [A: produc3658429121746597890et_nat] :
      ~ ( A @ ( bot_bot_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).

thf(23,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ( ( A @ ( one_one_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
    <=> ( ( A @ produc8586169260539613262et_nat )
        = bot_bot_set_nat ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9815_mod__emp) ).

thf(130,plain,
    ! [A: produc3658429121746597890et_nat] :
      ( ( ( ( A @ produc8586169260539613262et_nat )
          = bot_bot_set_nat )
       => ( A @ ( one_one_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( A @ ( one_one_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( ( A @ produc8586169260539613262et_nat )
          = bot_bot_set_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).

thf(56,axiom,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_Time_success_a @ aa_hea7994211679605476167unit_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_hoare__triple__success) ).

thf(306,plain,
    ! [A: assn,B: heap_Time_Heap_a,C: fun_a_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_a ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_Time_success_a @ aa_hea7994211679605476167unit_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).

thf(50,axiom,
    ! [A: assn,B: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ aTP_Lamm_ho @ aa_Pro653082453696054616_nat_o ) )
    <=> ( ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
        & ( B @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10333_ATP_Olambda__127) ).

thf(267,plain,
    ! [A: assn,B: produc3658429121746597890et_nat] :
      ( ( ( ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          & ( B @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) )
       => ( B @ ( A @ aTP_Lamm_ho @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( B @ ( A @ aTP_Lamm_ho @ aa_Pro653082453696054616_nat_o ) )
       => ( ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          & ( B @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).

thf(36,axiom,
    ! [A: $o,B: produc3658429121746597890et_nat,C: $o] :
      ( ( ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
      <=> C )
     => ~ ! [D: heap_e7401611519738050253t_unit,E: set_nat] :
            ( ( B
              = ( E @ ( D @ produc7507926704131184380et_nat ) ) )
           => ( C
            <=> ~ ( A
                  & ( E = bot_bot_set_nat ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2139_pure__assn__raw_Oelims_I1_J) ).

thf(167,plain,
    ! [A: $o,B: produc3658429121746597890et_nat,C: $o] :
      ( ( ( C
         => ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) ) )
        & ( ( B @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
         => C ) )
     => ~ ! [D: heap_e7401611519738050253t_unit,E: set_nat] :
            ( ( B
              = ( E @ ( D @ produc7507926704131184380et_nat ) ) )
           => ( ( ~ ( A
                    & ( E = bot_bot_set_nat ) )
               => C )
              & ( C
               => ~ ( A
                    & ( E = bot_bot_set_nat ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).

thf(9,axiom,
    ( top_top_assn
    = ( in_range @ abs_assn ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9964_top__assn__def) ).

thf(95,plain,
    ( top_top_assn
    = ( in_range @ abs_assn ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).

thf(60,axiom,
    ! [A: fun_Pr6460944699146269935_nat_o,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( C @ ( A @ aa_Pro653082453696054616_nat_o ) )
        <=> ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
     => ( ( A @ abs_assn )
        = B ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3810_Abs__assn__eqI_I1_J) ).

thf(327,plain,
    ! [A: fun_Pr6460944699146269935_nat_o,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( A @ aa_Pro653082453696054616_nat_o ) ) )
          & ( ( C @ ( A @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) )
     => ( ( A @ abs_assn )
        = B ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).

thf(22,axiom,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: fun_Pr6626665806141890376t_assn] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ! [E: product_unit] : ( E @ ( D @ aa_Product_unit_assn ) @ ( E @ ( C @ aa_Product_unit_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2519_cons__post__rule) ).

thf(127,plain,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: fun_Pr6626665806141890376t_assn] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ! [E: product_unit] : ( E @ ( D @ aa_Product_unit_assn ) @ ( E @ ( C @ aa_Product_unit_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).

thf(61,axiom,
    ! [A: assn,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
     => ( B @ ( A @ entails ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2500_entailsI) ).

thf(338,plain,
    ! [A: assn,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
     => ( B @ ( A @ entails ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).

thf(67,axiom,
    ! [A: assn] :
      ( ( A @ rep_assn @ abs_assn )
      = A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3701_Rep__assn__inverse) ).

thf(359,plain,
    ! [A: assn] :
      ( ( A @ rep_assn @ abs_assn )
      = A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).

thf(30,axiom,
    r @ ( f @ ( p @ hoare_hoare_triple_a ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_T1) ).

thf(154,plain,
    r @ ( f @ ( p @ hoare_hoare_triple_a ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).

thf(73,axiom,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( one_one_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2058_mod__emp__simp) ).

thf(386,plain,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( one_one_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).

thf(26,axiom,
    bot_bot_assn != one_one_assn,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2050_assn__basic__inequalities_I3_J) ).

thf(143,plain,
    bot_bot_assn != one_one_assn,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).

thf(11,axiom,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3646_in__range__empty) ).

thf(99,plain,
    ! [A: heap_e7401611519738050253t_unit] : ( bot_bot_set_nat @ ( A @ produc7507926704131184380et_nat ) @ ( in_range @ aa_Pro653082453696054616_nat_o ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).

thf(13,axiom,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( ( D @ ( C @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
       => ( D @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_331_relH__trans) ).

thf(104,plain,
    ! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: heap_e7401611519738050253t_unit] :
      ( ( C @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
     => ( ( D @ ( C @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) )
       => ( D @ ( B @ ( A @ relH ) @ aa_hea7994211679605476167unit_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).

thf(69,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
          ( A
         != ( C @ ( B @ produc7507926704131184380et_nat ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_one__assn__raw_Ocases) ).

thf(368,plain,
    ! [A: produc3658429121746597890et_nat] :
      ~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
          ( A
         != ( C @ ( B @ produc7507926704131184380et_nat ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).

thf(32,axiom,
    ! [A: assn,B: assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( A @ ( B @ entails ) )
       => ( A = B ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2309_ent__iffI) ).

thf(158,plain,
    ! [A: assn,B: assn] :
      ( ( B @ ( A @ entails ) )
     => ( ( A @ ( B @ entails ) )
       => ( A = B ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).

thf(17,axiom,
    ( bot_bot_assn
    = ( aTP_Lamm_gt @ abs_assn ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3849_bot__assn__def) ).

thf(114,plain,
    ( bot_bot_assn
    = ( aTP_Lamm_gt @ abs_assn ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).

thf(19,axiom,
    ! [A: assn,B: assn,C: fun_b_assn,D: fun_b_assn,E: heap_Time_Heap_b] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: b] : ( F @ ( D @ aa_b_assn ) @ ( F @ ( C @ aa_b_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_hoare_triple_b ) ) )
         => ( D @ ( E @ ( A @ hoare_hoare_triple_b ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2521_cons__rule) ).

thf(119,plain,
    ! [A: assn,B: assn,C: fun_b_assn,D: fun_b_assn,E: heap_Time_Heap_b] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: b] : ( F @ ( D @ aa_b_assn ) @ ( F @ ( C @ aa_b_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_hoare_triple_b ) ) )
         => ( D @ ( E @ ( A @ hoare_hoare_triple_b ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).

thf(45,axiom,
    ! [A: assn] :
      ( ( bot_bot_assn @ ( A @ entails ) )
    <=> ! [B: produc3658429121746597890et_nat] :
          ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2239_ent__false__iff) ).

thf(246,plain,
    ! [A: assn] :
      ( ( ! [B: produc3658429121746597890et_nat] :
            ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( bot_bot_assn @ ( A @ entails ) ) )
      & ( ( bot_bot_assn @ ( A @ entails ) )
       => ! [B: produc3658429121746597890et_nat] :
            ~ ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).

thf(40,axiom,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_T584514906347983379t_unit @ aa_hea7994211679605476167unit_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_hoare__triple__success) ).

thf(207,plain,
    ! [A: assn,B: heap_T5738788834812785303t_unit,C: fun_Pr6626665806141890376t_assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
      ( ( C @ ( B @ ( A @ hoare_8945653483474564448t_unit ) ) )
     => ( ( E @ ( D @ produc7507926704131184380et_nat ) @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( D @ ( B @ heap_T584514906347983379t_unit @ aa_hea7994211679605476167unit_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).

thf(29,axiom,
    ! [A: assn,B: assn,C: fun_a_assn,D: fun_a_assn,E: heap_Time_Heap_a] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: a] : ( F @ ( D @ aa_a_assn ) @ ( F @ ( C @ aa_a_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_hoare_triple_a ) ) )
         => ( D @ ( E @ ( A @ hoare_hoare_triple_a ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2520_cons__rule) ).

thf(151,plain,
    ! [A: assn,B: assn,C: fun_a_assn,D: fun_a_assn,E: heap_Time_Heap_a] :
      ( ( B @ ( A @ entails ) )
     => ( ! [F: a] : ( F @ ( D @ aa_a_assn ) @ ( F @ ( C @ aa_a_assn ) @ entails ) )
       => ( ( C @ ( E @ ( B @ hoare_hoare_triple_a ) ) )
         => ( D @ ( E @ ( A @ hoare_hoare_triple_a ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).

thf(48,axiom,
    ( ( h @ ( h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ hoare_new_addrs ) ) )
    = ( h @ ( as @ ( h3 @ hoare_new_addrs ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062) ).

thf(262,plain,
    ( ( h @ ( h2 @ ( as @ ( h3 @ hoare_new_addrs ) ) @ ( h2 @ hoare_new_addrs ) ) )
    = ( h @ ( as @ ( h3 @ hoare_new_addrs ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).

thf(27,axiom,
    ( one_one_assn
    = ( one_assn_raw @ abs_assn ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10197_one__assn__def) ).

thf(146,plain,
    ( one_one_assn
    = ( one_assn_raw @ abs_assn ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).

thf(41,axiom,
    ! [A: $o,B: heap_e7401611519738050253t_unit,C: set_nat] :
      ( ( C @ ( B @ produc7507926704131184380et_nat ) @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
    <=> ( A
        & ( C = bot_bot_set_nat ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2138_pure__assn__raw_Osimps) ).

thf(210,plain,
    ! [A: $o,B: heap_e7401611519738050253t_unit,C: set_nat] :
      ( ( ( A
          & ( C = bot_bot_set_nat ) )
       => ( C @ ( B @ produc7507926704131184380et_nat ) @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( C @ ( B @ produc7507926704131184380et_nat ) @ ( A @ pure_a825153325127701367it_nat @ aa_Pro653082453696054616_nat_o ) )
       => ( A
          & ( C = bot_bot_set_nat ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).

thf(44,axiom,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( C @ ( B @ ( A @ aTP_Lamm_gv @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) )
    <=> ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
        & ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10704_ATP_Olambda__498) ).

thf(239,plain,
    ! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
      ( ( ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          & ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
       => ( C @ ( B @ ( A @ aTP_Lamm_gv @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( C @ ( B @ ( A @ aTP_Lamm_gv @ aa_ass4243947775541419017_nat_o ) @ aa_Pro653082453696054616_nat_o ) )
       => ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
          & ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).

thf(3,axiom,
    ! [A: assn] : ( A @ ( A @ entails ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2310_ent__refl) ).

thf(79,plain,
    ! [A: assn] : ( A @ ( A @ entails ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).

thf(37,axiom,
    ! [A: produc3658429121746597890et_nat] :
      ( ( A @ ( top_top_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
    <=> ( A @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9958_mod__true) ).

thf(195,plain,
    ! [A: produc3658429121746597890et_nat] :
      ( ( ( A @ ( in_range @ aa_Pro653082453696054616_nat_o ) )
       => ( A @ ( top_top_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
      & ( ( A @ ( top_top_assn @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
       => ( A @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).

thf(59,axiom,
    as @ ( h3 @ produc7507926704131184380et_nat ) @ ( p @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062_Ih_M_Aas_J_A_092_060Turnstile_062_AP_092_060close_062) ).

thf(326,plain,
    as @ ( h3 @ produc7507926704131184380et_nat ) @ ( p @ rep_assn @ aa_Pro653082453696054616_nat_o ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).

thf(14,axiom,
    ! [A: heap_Time_Heap_a,B: fun_a_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_hoare_triple_a ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1994_false__rule) ).

thf(107,plain,
    ! [A: heap_Time_Heap_a,B: fun_a_assn] : ( B @ ( A @ ( bot_bot_assn @ hoare_hoare_triple_a ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).

thf(16,axiom,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: fun_b_assn] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ! [E: b] : ( E @ ( D @ aa_b_assn ) @ ( E @ ( C @ aa_b_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2518_cons__post__rule) ).

thf(111,plain,
    ! [A: assn,B: heap_Time_Heap_b,C: fun_b_assn,D: fun_b_assn] :
      ( ( C @ ( B @ ( A @ hoare_hoare_triple_b ) ) )
     => ( ! [E: b] : ( E @ ( D @ aa_b_assn ) @ ( E @ ( C @ aa_b_assn ) @ entails ) )
       => ( D @ ( B @ ( A @ hoare_hoare_triple_b ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).

thf(47,axiom,
    ! [A: assn,B: assn] :
      ( ( B @ ( A @ entails ) )
    <=> ! [C: produc3658429121746597890et_nat] :
          ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
         => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2501_entails__def) ).

thf(254,plain,
    ! [A: assn,B: assn] :
      ( ( ! [C: produc3658429121746597890et_nat] :
            ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
       => ( B @ ( A @ entails ) ) )
      & ( ( B @ ( A @ entails ) )
       => ! [C: produc3658429121746597890et_nat] :
            ( ( C @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).

thf(20,axiom,
    ! [A: a] : ( q @ ( A @ ( g @ aa_a_H8829438778223708363Heap_b ) @ ( A @ ( r @ aa_a_assn ) @ hoare_hoare_triple_b ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_T2) ).

thf(122,plain,
    ! [A: a] : ( q @ ( A @ ( g @ aa_a_H8829438778223708363Heap_b ) @ ( A @ ( r @ aa_a_assn ) @ hoare_hoare_triple_b ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).

thf(65,axiom,
    ! [A: assn,B: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
     => ( B @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3653_models__in__range) ).

thf(354,plain,
    ! [A: assn,B: produc3658429121746597890et_nat] :
      ( ( B @ ( A @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
     => ( B @ ( in_range @ aa_Pro653082453696054616_nat_o ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).

thf(57,axiom,
    ! [A: fun_Pr6460944699146269935_nat_o,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( C @ ( A @ aa_Pro653082453696054616_nat_o ) )
        <=> ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) )
     => ( B
        = ( A @ abs_assn ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3811_Abs__assn__eqI_I2_J) ).

thf(309,plain,
    ! [A: fun_Pr6460944699146269935_nat_o,B: assn] :
      ( ! [C: produc3658429121746597890et_nat] :
          ( ( ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( A @ aa_Pro653082453696054616_nat_o ) ) )
          & ( ( C @ ( A @ aa_Pro653082453696054616_nat_o ) )
           => ( C @ ( B @ rep_assn @ aa_Pro653082453696054616_nat_o ) ) ) )
     => ( B
        = ( A @ abs_assn ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).

thf(419,plain,
    $false,
    inference(e,[status(thm)],[320,372,165,343,86,155,342,163,138,101,234,408,202,416,78,348,84,396,89,116,380,201,92,252,97,285,224,388,356,141,109,124,298,148,264,161,279,274,81,377,362,303,130,306,267,167,95,327,127,338,359,154,386,143,99,104,368,158,114,119,246,207,151,262,146,210,239,79,195,326,107,111,254,122,354,309]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP214_3 : TPTP v9.3.1. Bugfixed v9.3.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41  % Computer : n001.cluster.edu
% 0.14/0.41  % Model    : x86_64 x86_64
% 0.14/0.41  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41  % Memory   : 8046.5625MB
% 0.14/0.41  % OS       : Linux 6.8.0-71-generic
% 0.14/0.42  % CPULimit : 300
% 0.14/0.42  % WCLimit  : 300
% 0.14/0.42  % DateTime : Fri Sep 25 18:17:11 UTC 2026
% 0.14/0.42  % CPUTime  : 
% 0.14/0.42  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.98  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 9.36/3.15  % [INFO] 	 Parsing done (2159ms). 
% 9.36/3.17  % [INFO] 	 Running in sequential loop mode. 
% 10.10/3.53  % [INFO] 	 eprover registered as external prover. 
% 10.10/3.54  % [INFO] 	 Scanning for conjecture ... 
% 14.42/4.63  % [INFO] 	 Found a conjecture (or negated_conjecture) and 11337 axioms. Running axiom selection ... 
% 15.42/4.95  % [INFO] 	 Axiom selection finished. Selected 75 axioms (removed 11262 axioms). 
% 15.93/5.06  % [INFO] 	 Problem is typed first-order (TPTP TFF). 
% 15.93/5.08  % [INFO] 	 Type checking passed. 
% 15.93/5.08  % [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 ... 
% 21.81/6.88  % External prover 'e' found a proof!
% 21.81/6.88  % [INFO] 	 Killing All external provers ... 
% 21.81/6.89  % Time passed: 6327ms (effective reasoning time: 3710ms)
% 21.81/6.89  % 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)>
% 21.81/6.89  % Axioms used in derivation (75): fact_9957_assn__basic__inequalities_I5_J, fact_9956_assn__basic__inequalities_I1_J, fact_1995_false__rule, fact_2517_cons__post__rule, fact_1__092_060open_062_Ih_M_Aas_J_A_092_060Turnstile_062_AP_092_060close_062, fact_2519_cons__post__rule, fact_3701_Rep__assn__inverse, fact_2500_entailsI, fact_2520_cons__rule, fact_2_new__addr__refl, fact_1996_false__rule, fact_2050_assn__basic__inequalities_I3_J, fact_10200_one__assn__raw_Oelims_I1_J, fact_16_one__assn__raw_Ocases, fact_3654_relH__in__rangeI_I2_J, fact_2498_ent__fwd, fact_141_hoare__triple__effect, fact_139_hoare__triple__effect, fact_9965_mod__h__bot__iff_I2_J, fact_3849_bot__assn__def, fact_2499_entailsD, fact_101_hoare__triple__preI, fact_2518_cons__post__rule, fact_10201_one__assn__raw_Oelims_I2_J, fact_102_hoare__triple__preI, fact_11289_ATP_Olambda__1083, fact_10333_ATP_Olambda__127, fact_3646_in__range__empty, fact_2239_ent__false__iff, fact_2568_cons__pre__rule, fact_332_relH__sym, fact_2522_cons__rule, fact_9815_mod__emp, fact_54_T2, fact_2058_mod__emp__simp, fact_3_POST__G, fact_2310_ent__refl, fact_548_mod__relH, fact_9964_top__assn__def, fact_10199_one__assn__raw_Osimps, fact_3810_Abs__assn__eqI_I1_J, fact_2140_pure__assn__raw_Oelims_I2_J, fact_10197_one__assn__def, fact_144_hoare__triple__success, fact_3655_relH__in__rangeI_I1_J, fact_9958_mod__true, fact_331_relH__trans, fact_53_T1, fact_3811_Abs__assn__eqI_I2_J, fact_2566_cons__pre__rule, fact_2501_entails__def, fact_2139_pure__assn__raw_Oelims_I1_J, fact_1994_false__rule, fact_4_POST__F, fact_2567_cons__pre__rule, fact_2521_cons__rule, fact_9960_ent__true, fact_10202_one__assn__raw_Oelims_I3_J, fact_2309_ent__iffI, fact_2311_ent__trans, fact_5_Rep__assn__inject, fact_103_hoare__triple__preI, fact_142_hoare__triple__success, fact_2691_pure__assn__raw_Oelims_I3_J, fact_1965_mod__h__bot__indep, fact_140_hoare__triple__effect, fact_10704_ATP_Olambda__498, fact_2018_mod__false, fact_3653_models__in__range, fact_3656_relH__refl, fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062, fact_2138_pure__assn__raw_Osimps, fact_10681_ATP_Olambda__475, fact_143_hoare__triple__success, fact_2533_ent__false
% 21.81/6.89  % No. of inferences in proof: 154
% 21.81/6.89  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 6327 ms resp. 3710 ms w/o parsing
% 22.92/7.08  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 22.92/7.09  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------