Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWW470_3 : TPTP v9.3.1. Released v5.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n002.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 : Tue Sep 29 01:30:25 PM UTC 2026

% Result   : Theorem 4.22s 1.39s
% Output   : Refutation 5.18s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    7
%            Number of leaves      :    5
% Syntax   : Number of formulae    :   18 (  14 unt;   0 typ;   0 def)
%            Number of atoms       :   25 (   4 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   14 (   7   ~;   3   |;   2   &)
%                                         (   0 <=>;   2  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   3 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of types       :  315 ( 314 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :  612 ( 612 usr; 231 con; 0-4 aty)
%            Number of variables   :   28 (  26   !;   2   ?;  28   :)

% Comments : 
%------------------------------------------------------------------------------
tff(type_def_5,type,
    x_a: $tType ).

tff(type_def_6,type,
    com: $tType ).

tff(type_def_7,type,
    state: $tType ).

tff(type_def_8,type,
    vname: $tType ).

tff(type_def_9,type,
    bool: $tType ).

tff(type_def_10,type,
    hoare_2076525193iple_a: $tType ).

tff(type_def_11,type,
    int: $tType ).

tff(type_def_12,type,
    nat: $tType ).

tff(type_def_13,type,
    fun_a_fun_state_bool: $tType ).

tff(type_def_14,type,
    fun_a_1632297036l_bool: $tType ).

tff(type_def_15,type,
    fun_a_998512028e_bool: $tType ).

tff(type_def_16,type,
    fun_a_340690546e_bool: $tType ).

tff(type_def_17,type,
    fun_a_2117018159e_bool: $tType ).

tff(type_def_18,type,
    fun_state_state: $tType ).

tff(type_def_19,type,
    fun_state_bool: $tType ).

tff(type_def_20,type,
    fun_state_nat: $tType ).

tff(type_def_21,type,
    fun_st1506752259e_bool: $tType ).

tff(type_def_22,type,
    fun_st1816159843_state: $tType ).

tff(type_def_23,type,
    fun_st2063251938l_bool: $tType ).

tff(type_def_24,type,
    fun_st2072884720_state: $tType ).

tff(type_def_25,type,
    fun_vn299216483_state: $tType ).

tff(type_def_26,type,
    fun_vn774578976_state: $tType ).

tff(type_def_27,type,
    fun_bool_bool: $tType ).

tff(type_def_28,type,
    fun_bo675861616e_bool: $tType ).

tff(type_def_29,type,
    fun_bo1936561970e_bool: $tType ).

tff(type_def_30,type,
    fun_bo1549164019l_bool: $tType ).

tff(type_def_31,type,
    fun_bo840878273a_bool: $tType ).

tff(type_def_32,type,
    fun_bo1829594782t_bool: $tType ).

tff(type_def_33,type,
    fun_bo1570548802t_bool: $tType ).

tff(type_def_34,type,
    fun_Ho882550911a_bool: $tType ).

tff(type_def_35,type,
    fun_Ho1518252029iple_a: $tType ).

tff(type_def_36,type,
    fun_Ho1026035802_a_int: $tType ).

tff(type_def_37,type,
    fun_Ho864122878_a_nat: $tType ).

tff(type_def_38,type,
    fun_Ho2037816211l_bool: $tType ).

tff(type_def_39,type,
    fun_Ho943022881a_bool: $tType ).

tff(type_def_40,type,
    fun_Ho483360497iple_a: $tType ).

tff(type_def_41,type,
    fun_Ho1608761598t_bool: $tType ).

tff(type_def_42,type,
    fun_Ho1977546161nt_int: $tType ).

tff(type_def_43,type,
    fun_Ho1488374613nt_nat: $tType ).

tff(type_def_44,type,
    fun_Ho1349715618t_bool: $tType ).

tff(type_def_45,type,
    fun_Ho1036508337at_nat: $tType ).

tff(type_def_46,type,
    fun_Ho1910759733l_bool: $tType ).

tff(type_def_47,type,
    fun_Ho112928087a_bool: $tType ).

tff(type_def_48,type,
    fun_Ho1634634433ol_nat: $tType ).

tff(type_def_49,type,
    fun_Ho1345928733ol_nat: $tType ).

tff(type_def_50,type,
    fun_Ho755902321at_nat: $tType ).

tff(type_def_51,type,
    fun_int_bool: $tType ).

tff(type_def_52,type,
    fun_in1219646560iple_a: $tType ).

tff(type_def_53,type,
    fun_int_int: $tType ).

tff(type_def_54,type,
    fun_int_nat: $tType ).

tff(type_def_55,type,
    fun_in531499254l_bool: $tType ).

tff(type_def_56,type,
    fun_in451447550a_bool: $tType ).

tff(type_def_57,type,
    fun_in990358449_a_int: $tType ).

tff(type_def_58,type,
    fun_in501186901_a_nat: $tType ).

tff(type_def_59,type,
    fun_int_fun_int_bool: $tType ).

tff(type_def_60,type,
    fun_int_fun_int_int: $tType ).

tff(type_def_61,type,
    fun_int_fun_int_nat: $tType ).

tff(type_def_62,type,
    fun_int_fun_nat_bool: $tType ).

tff(type_def_63,type,
    fun_int_fun_nat_int: $tType ).

tff(type_def_64,type,
    fun_int_fun_nat_nat: $tType ).

tff(type_def_65,type,
    fun_in149899451ol_nat: $tType ).

tff(type_def_66,type,
    fun_in938817141l_bool: $tType ).

tff(type_def_67,type,
    fun_in1461553182ol_nat: $tType ).

tff(type_def_68,type,
    fun_in719570932t_bool: $tType ).

tff(type_def_69,type,
    fun_in1172847482ol_nat: $tType ).

tff(type_def_70,type,
    fun_in1791225684at_nat: $tType ).

tff(type_def_71,type,
    fun_nat_state: $tType ).

tff(type_def_72,type,
    fun_nat_bool: $tType ).

tff(type_def_73,type,
    fun_na1240513468iple_a: $tType ).

tff(type_def_74,type,
    fun_nat_int: $tType ).

tff(type_def_75,type,
    fun_nat_nat: $tType ).

tff(type_def_76,type,
    fun_na1469252690l_bool: $tType ).

tff(type_def_77,type,
    fun_na1758826658a_bool: $tType ).

tff(type_def_78,type,
    fun_na841142961_a_nat: $tType ).

tff(type_def_79,type,
    fun_nat_fun_int_bool: $tType ).

tff(type_def_80,type,
    fun_nat_fun_int_nat: $tType ).

tff(type_def_81,type,
    fun_nat_fun_nat_bool: $tType ).

tff(type_def_82,type,
    fun_nat_fun_nat_nat: $tType ).

tff(type_def_83,type,
    fun_na228779103ol_nat: $tType ).

tff(type_def_84,type,
    fun_na1588060912_a_nat: $tType ).

tff(type_def_85,type,
    fun_na1402637250ol_nat: $tType ).

tff(type_def_86,type,
    fun_na266550704nt_nat: $tType ).

tff(type_def_87,type,
    fun_na1436237685l_bool: $tType ).

tff(type_def_88,type,
    fun_na35521688t_bool: $tType ).

tff(type_def_89,type,
    fun_fu2118559873l_bool: $tType ).

tff(type_def_90,type,
    fun_fu278206227e_bool: $tType ).

tff(type_def_91,type,
    fun_fu1591723597e_bool: $tType ).

tff(type_def_92,type,
    fun_fu2008829792e_bool: $tType ).

tff(type_def_93,type,
    fun_fu222103665e_bool: $tType ).

tff(type_def_94,type,
    fun_fu1009378087e_bool: $tType ).

tff(type_def_95,type,
    fun_fu734682033e_bool: $tType ).

tff(type_def_96,type,
    fun_fu796809180e_bool: $tType ).

tff(type_def_97,type,
    fun_fu78956742e_bool: $tType ).

tff(type_def_98,type,
    fun_fu281355805e_bool: $tType ).

tff(type_def_99,type,
    fun_fu373216837e_bool: $tType ).

tff(type_def_100,type,
    fun_fu1658206819l_bool: $tType ).

tff(type_def_101,type,
    fun_fu2127278875e_bool: $tType ).

tff(type_def_102,type,
    fun_fu978939117_state: $tType ).

tff(type_def_103,type,
    fun_fu402792811e_bool: $tType ).

tff(type_def_104,type,
    fun_fu1067796093_state: $tType ).

tff(type_def_105,type,
    fun_fu1219323149e_bool: $tType ).

tff(type_def_106,type,
    fun_fu1047394976e_bool: $tType ).

tff(type_def_107,type,
    fun_fu227828410_state: $tType ).

tff(type_def_108,type,
    fun_fu88048803e_bool: $tType ).

tff(type_def_109,type,
    fun_fu372140353a_bool: $tType ).

tff(type_def_110,type,
    fun_fu1909738875t_bool: $tType ).

tff(type_def_111,type,
    fun_fu1509210819t_bool: $tType ).

tff(type_def_112,type,
    fun_fu1873708859l_bool: $tType ).

tff(type_def_113,type,
    fun_fu1022479645l_bool: $tType ).

tff(type_def_114,type,
    fun_fu531009635l_bool: $tType ).

tff(type_def_115,type,
    fun_fu1849968923l_bool: $tType ).

tff(type_def_116,type,
    fun_fu2026518849l_bool: $tType ).

tff(type_def_117,type,
    fun_fu253747899iple_a: $tType ).

tff(type_def_118,type,
    fun_fu490614552ol_int: $tType ).

tff(type_def_119,type,
    fun_fu328701628ol_nat: $tType ).

tff(type_def_120,type,
    fun_fu1663341283a_bool: $tType ).

tff(type_def_121,type,
    fun_fu1067550789l_bool: $tType ).

tff(type_def_122,type,
    fun_fu1725628421a_bool: $tType ).

tff(type_def_123,type,
    fun_fu662538351at_nat: $tType ).

tff(type_def_124,type,
    fun_fu1789210355l_bool: $tType ).

tff(type_def_125,type,
    fun_fu2051904533a_bool: $tType ).

tff(type_def_126,type,
    fun_fu2104275287l_bool: $tType ).

tff(type_def_127,type,
    fun_fu1040446391a_bool: $tType ).

tff(type_def_128,type,
    fun_fu1557526205_a_int: $tType ).

tff(type_def_129,type,
    fun_fu1733261297t_bool: $tType ).

tff(type_def_130,type,
    fun_fu1975973012nt_int: $tType ).

tff(type_def_131,type,
    fun_fu1327528203ol_int: $tType ).

tff(type_def_132,type,
    fun_fu1923493821_a_nat: $tType ).

tff(type_def_133,type,
    fun_fu1252406585t_bool: $tType ).

tff(type_def_134,type,
    fun_fu1300474096at_nat: $tType ).

tff(type_def_135,type,
    fun_fu1472438000_a_nat: $tType ).

tff(type_def_136,type,
    fun_fu827349075ol_nat: $tType ).

tff(type_def_137,type,
    fun_fu805217741a_bool: $tType ).

tff(type_def_138,type,
    fun_fu445247621a_bool: $tType ).

tff(type_def_139,type,
    fun_fu630820007a_bool: $tType ).

tff(type_def_140,type,
    fun_fu914297575a_bool: $tType ).

tff(type_def_141,type,
    fun_fu1381603133a_bool: $tType ).

tff(type_def_142,type,
    fun_fu1681956989a_bool: $tType ).

tff(type_def_143,type,
    fun_fu1682168189a_bool: $tType ).

tff(type_def_144,type,
    fun_fu602188273_a_nat: $tType ).

tff(type_def_145,type,
    fun_fu945366625t_bool: $tType ).

tff(type_def_146,type,
    fun_fu697888865a_bool: $tType ).

tff(type_def_147,type,
    fun_fu907920777_a_int: $tType ).

tff(type_def_148,type,
    fun_fu876640303ol_nat: $tType ).

tff(type_def_149,type,
    fun_fu1217459197_a_nat: $tType ).

tff(type_def_150,type,
    fun_fu197504845_a_nat: $tType ).

tff(type_def_151,type,
    fun_fu623690153t_bool: $tType ).

tff(type_def_152,type,
    fun_fu552225705a_bool: $tType ).

tff(type_def_153,type,
    fun_fu394467047ol_nat: $tType ).

tff(type_def_154,type,
    fun_fu2033973437at_nat: $tType ).

tff(type_def_155,type,
    fun_fu1305006333_a_nat: $tType ).

tff(type_def_156,type,
    fun_fu84072329_a_nat: $tType ).

tff(type_def_157,type,
    fun_fu1498271147a_bool: $tType ).

tff(type_def_158,type,
    fun_fu1585255851a_bool: $tType ).

tff(type_def_159,type,
    fun_fu1310697751_a_nat: $tType ).

tff(type_def_160,type,
    fun_fu1071091151_a_nat: $tType ).

tff(type_def_161,type,
    fun_fu728204273_a_nat: $tType ).

tff(type_def_162,type,
    fun_fu2109513853at_nat: $tType ).

tff(type_def_163,type,
    fun_fu819804446l_bool: $tType ).

tff(type_def_164,type,
    fun_fun_int_bool_int: $tType ).

tff(type_def_165,type,
    fun_fun_int_bool_nat: $tType ).

tff(type_def_166,type,
    fun_fu554825757t_bool: $tType ).

tff(type_def_167,type,
    fun_fu610077323l_bool: $tType ).

tff(type_def_168,type,
    fun_fu380257692t_bool: $tType ).

tff(type_def_169,type,
    fun_fu2071915986at_nat: $tType ).

tff(type_def_170,type,
    fun_fu1151772339l_bool: $tType ).

tff(type_def_171,type,
    fun_fu1075512626t_bool: $tType ).

tff(type_def_172,type,
    fun_fu1284533364l_bool: $tType ).

tff(type_def_173,type,
    fun_fu1017053431a_bool: $tType ).

tff(type_def_174,type,
    fun_fu215647537t_bool: $tType ).

tff(type_def_175,type,
    fun_fu1814991441ol_int: $tType ).

tff(type_def_176,type,
    fun_fu1887272509at_int: $tType ).

tff(type_def_177,type,
    fun_fu130970841nt_int: $tType ).

tff(type_def_178,type,
    fun_fu1789282941nt_nat: $tType ).

tff(type_def_179,type,
    fun_fu1237756537t_bool: $tType ).

tff(type_def_180,type,
    fun_fu1420944304at_nat: $tType ).

tff(type_def_181,type,
    fun_fu330349488nt_nat: $tType ).

tff(type_def_182,type,
    fun_fu670292377ol_nat: $tType ).

tff(type_def_183,type,
    fun_fu587508068t_bool: $tType ).

tff(type_def_184,type,
    fun_fu713748577t_bool: $tType ).

tff(type_def_185,type,
    fun_fu728395988nt_nat: $tType ).

tff(type_def_186,type,
    fun_fu466270817a_bool: $tType ).

tff(type_def_187,type,
    fun_fu224004093nt_nat: $tType ).

tff(type_def_188,type,
    fun_fu2076872489ol_nat: $tType ).

tff(type_def_189,type,
    fun_fu1221449756t_bool: $tType ).

tff(type_def_190,type,
    fun_fu1396640951nt_nat: $tType ).

tff(type_def_191,type,
    fun_fu257678363t_bool: $tType ).

tff(type_def_192,type,
    fun_fu1881253066t_bool: $tType ).

tff(type_def_193,type,
    fun_fu405047601t_bool: $tType ).

tff(type_def_194,type,
    fun_fu1997740657t_bool: $tType ).

tff(type_def_195,type,
    fun_fu1576332145t_bool: $tType ).

tff(type_def_196,type,
    fun_fu1831640381nt_int: $tType ).

tff(type_def_197,type,
    fun_fu214894141nt_nat: $tType ).

tff(type_def_198,type,
    fun_fu1243635695ol_nat: $tType ).

tff(type_def_199,type,
    fun_fu1424009747nt_nat: $tType ).

tff(type_def_200,type,
    fun_fu401661795t_bool: $tType ).

tff(type_def_201,type,
    fun_fu1890060131t_bool: $tType ).

tff(type_def_202,type,
    fun_fu1416337063ol_nat: $tType ).

tff(type_def_203,type,
    fun_fu199354621at_nat: $tType ).

tff(type_def_204,type,
    fun_fu652796733nt_nat: $tType ).

tff(type_def_205,type,
    fun_fu1650807462nt_nat: $tType ).

tff(type_def_206,type,
    fun_fu2087062900nt_nat: $tType ).

tff(type_def_207,type,
    fun_fu1374874789t_bool: $tType ).

tff(type_def_208,type,
    fun_fu1989253562nt_nat: $tType ).

tff(type_def_209,type,
    fun_fu407119589t_bool: $tType ).

tff(type_def_210,type,
    fun_fu776947314nt_nat: $tType ).

tff(type_def_211,type,
    fun_fu591799985nt_nat: $tType ).

tff(type_def_212,type,
    fun_fu1218916157at_nat: $tType ).

tff(type_def_213,type,
    fun_fu425979586l_bool: $tType ).

tff(type_def_214,type,
    fun_fun_nat_bool_int: $tType ).

tff(type_def_215,type,
    fun_fun_nat_bool_nat: $tType ).

tff(type_def_216,type,
    fun_fu219474671_a_nat: $tType ).

tff(type_def_217,type,
    fun_fu483878866nt_nat: $tType ).

tff(type_def_218,type,
    fun_fu821463397t_bool: $tType ).

tff(type_def_219,type,
    fun_fu2104074051l_bool: $tType ).

tff(type_def_220,type,
    fun_fu429110920t_bool: $tType ).

tff(type_def_221,type,
    fun_fu1217155507l_bool: $tType ).

tff(type_def_222,type,
    fun_fu915923926t_bool: $tType ).

tff(type_def_223,type,
    fun_fu1216549656l_bool: $tType ).

tff(type_def_224,type,
    fun_fu1525594615a_bool: $tType ).

tff(type_def_225,type,
    fun_fu2024564861at_int: $tType ).

tff(type_def_226,type,
    fun_fu1842665009t_bool: $tType ).

tff(type_def_227,type,
    fun_fu603924029nt_int: $tType ).

tff(type_def_228,type,
    fun_fu2134752009ol_int: $tType ).

tff(type_def_229,type,
    fun_fu300013553at_nat: $tType ).

tff(type_def_230,type,
    fun_fu1127110484at_nat: $tType ).

tff(type_def_231,type,
    fun_fu325663101at_nat: $tType ).

tff(type_def_232,type,
    fun_fu717290361t_bool: $tType ).

tff(type_def_233,type,
    fun_fu2064863920at_nat: $tType ).

tff(type_def_234,type,
    fun_fu1437424253_a_nat: $tType ).

tff(type_def_235,type,
    fun_fu773339453nt_nat: $tType ).

tff(type_def_236,type,
    fun_fu990052945ol_nat: $tType ).

tff(type_def_237,type,
    fun_fu1179887677at_nat: $tType ).

tff(type_def_238,type,
    fun_fu1901564496t_bool: $tType ).

tff(type_def_239,type,
    fun_fu1453083561t_bool: $tType ).

tff(type_def_240,type,
    fun_fu546267020at_nat: $tType ).

tff(type_def_241,type,
    fun_fu1381619113a_bool: $tType ).

tff(type_def_242,type,
    fun_fu1251828989at_nat: $tType ).

tff(type_def_243,type,
    fun_fu1428730409ol_nat: $tType ).

tff(type_def_244,type,
    fun_fu100665187t_bool: $tType ).

tff(type_def_245,type,
    fun_fu1553240943at_nat: $tType ).

tff(type_def_246,type,
    fun_fu1589063523t_bool: $tType ).

tff(type_def_247,type,
    fun_fu84751165at_nat: $tType ).

tff(type_def_248,type,
    fun_fu1544887023ol_nat: $tType ).

tff(type_def_249,type,
    fun_fu531872008t_bool: $tType ).

tff(type_def_250,type,
    fun_fu1733046955t_bool: $tType ).

tff(type_def_251,type,
    fun_fu2023981606t_bool: $tType ).

tff(type_def_252,type,
    fun_fu686268865t_bool: $tType ).

tff(type_def_253,type,
    fun_fu1109211905t_bool: $tType ).

tff(type_def_254,type,
    fun_fu687803393t_bool: $tType ).

tff(type_def_255,type,
    fun_fu522653757at_nat: $tType ).

tff(type_def_256,type,
    fun_fu927620157_a_nat: $tType ).

tff(type_def_257,type,
    fun_fu1086979837nt_nat: $tType ).

tff(type_def_258,type,
    fun_fu1755521597at_nat: $tType ).

tff(type_def_259,type,
    fun_fu1017488637at_nat: $tType ).

tff(type_def_260,type,
    fun_fu1382375754at_nat: $tType ).

tff(type_def_261,type,
    fun_fu1799328765at_nat: $tType ).

tff(type_def_262,type,
    fun_fu55165875at_nat: $tType ).

tff(type_def_263,type,
    fun_fu1446087120at_nat: $tType ).

tff(type_def_264,type,
    fun_fu1480131645_a_nat: $tType ).

tff(type_def_265,type,
    fun_fu1373519097at_nat: $tType ).

tff(type_def_266,type,
    fun_fu1081900566at_nat: $tType ).

tff(type_def_267,type,
    fun_fu1251161661nt_nat: $tType ).

tff(type_def_268,type,
    fun_fu80187629t_bool: $tType ).

tff(type_def_269,type,
    fun_fu1538037805t_bool: $tType ).

tff(type_def_270,type,
    fun_fu1340893257l_bool: $tType ).

tff(type_def_271,type,
    fun_fu817723125e_bool: $tType ).

tff(type_def_272,type,
    fun_fu1860059197e_bool: $tType ).

tff(type_def_273,type,
    fun_fu1631777789e_bool: $tType ).

tff(type_def_274,type,
    fun_fu1342882871l_bool: $tType ).

tff(type_def_275,type,
    fun_fu1819779801a_bool: $tType ).

tff(type_def_276,type,
    fun_fu1354972029l_bool: $tType ).

tff(type_def_277,type,
    fun_fu870629313a_bool: $tType ).

tff(type_def_278,type,
    fun_fu898837677at_nat: $tType ).

tff(type_def_279,type,
    fun_fu600978683a_bool: $tType ).

tff(type_def_280,type,
    fun_fu1912089667a_bool: $tType ).

tff(type_def_281,type,
    fun_fu1236051915l_bool: $tType ).

tff(type_def_282,type,
    fun_fu1595031695a_bool: $tType ).

tff(type_def_283,type,
    fun_fu743040865a_bool: $tType ).

tff(type_def_284,type,
    fun_fu1739618017ol_nat: $tType ).

tff(type_def_285,type,
    fun_fu774707681ol_nat: $tType ).

tff(type_def_286,type,
    fun_fu1540142484l_bool: $tType ).

tff(type_def_287,type,
    fun_fu1421432211t_bool: $tType ).

tff(type_def_288,type,
    fun_fu1070826941l_bool: $tType ).

tff(type_def_289,type,
    fun_fu1671602619t_bool: $tType ).

tff(type_def_290,type,
    fun_fu2017547765_a_nat: $tType ).

tff(type_def_291,type,
    fun_fu1795303867nt_nat: $tType ).

tff(type_def_292,type,
    fun_fu1888474227at_nat: $tType ).

tff(type_def_293,type,
    fun_fu763112513t_bool: $tType ).

tff(type_def_294,type,
    fun_fu1521371387t_bool: $tType ).

tff(type_def_295,type,
    fun_fu788822083t_bool: $tType ).

tff(type_def_296,type,
    fun_fu1276998475l_bool: $tType ).

tff(type_def_297,type,
    fun_fu680577737t_bool: $tType ).

tff(type_def_298,type,
    fun_fu873308769t_bool: $tType ).

tff(type_def_299,type,
    fun_fu651819309ol_nat: $tType ).

tff(type_def_300,type,
    fun_fu657063149ol_nat: $tType ).

tff(type_def_301,type,
    fun_fu342964205ol_nat: $tType ).

tff(type_def_302,type,
    fun_fu814369080l_bool: $tType ).

tff(type_def_303,type,
    fun_fu496092379t_bool: $tType ).

tff(type_def_304,type,
    fun_fu616551101l_bool: $tType ).

tff(type_def_305,type,
    fun_fu1402718723t_bool: $tType ).

tff(type_def_306,type,
    fun_fu1155082413_a_nat: $tType ).

tff(type_def_307,type,
    fun_fu523748467nt_nat: $tType ).

tff(type_def_308,type,
    fun_fu2137156673t_bool: $tType ).

tff(type_def_309,type,
    fun_fu719081723t_bool: $tType ).

tff(type_def_310,type,
    fun_fu820922699l_bool: $tType ).

tff(type_def_311,type,
    fun_fu257437713t_bool: $tType ).

tff(type_def_312,type,
    fun_fu1738364513t_bool: $tType ).

tff(type_def_313,type,
    fun_fu687095869_a_nat: $tType ).

tff(type_def_314,type,
    fun_fu504533053nt_nat: $tType ).

tff(type_def_315,type,
    fun_fu1838203037ol_nat: $tType ).

tff(type_def_316,type,
    fun_fu294108253ol_nat: $tType ).

tff(type_def_317,type,
    fun_fu477648637at_nat: $tType ).

tff(type_def_318,type,
    fun_fu633097021at_nat: $tType ).

tff(func_def_0,type,
    big_co1560107922_a_int: fun_fu1327528203ol_int ).

tff(func_def_1,type,
    big_co922834230_a_nat: fun_fu827349075ol_nat ).

tff(func_def_2,type,
    big_co230513141nt_int: fun_fu1814991441ol_int ).

tff(func_def_3,type,
    big_co1740723097nt_nat: fun_fu670292377ol_nat ).

tff(func_def_4,type,
    big_co1024481617at_int: fun_fu2134752009ol_int ).

tff(func_def_5,type,
    big_co387207925at_nat: fun_fu990052945ol_nat ).

tff(func_def_6,type,
    big_co2035489411_a_int: fun_Ho1026035802_a_int > fun_fu490614552ol_int ).

tff(func_def_7,type,
    big_co1398215719_a_nat: fun_Ho864122878_a_nat > fun_fu328701628ol_nat ).

tff(func_def_8,type,
    big_co1548731110nt_int: fun_int_int > fun_fun_int_bool_int ).

tff(func_def_9,type,
    big_co911457418nt_nat: fun_int_nat > fun_fun_int_bool_nat ).

tff(func_def_10,type,
    big_co195215938at_int: fun_nat_int > fun_fun_nat_bool_int ).

tff(func_def_11,type,
    big_co1705425894at_nat: fun_nat_nat > fun_fun_nat_bool_nat ).

tff(func_def_12,type,
    big_linorder_Max_int: fun_fun_int_bool_int ).

tff(func_def_13,type,
    big_linorder_Max_nat: fun_fun_nat_bool_nat ).

tff(func_def_14,type,
    big_linorder_Min_int: fun_fun_int_bool_int ).

tff(func_def_15,type,
    big_linorder_Min_nat: fun_fun_nat_bool_nat ).

tff(func_def_16,type,
    big_se82156639iple_a: ( fun_Ho483360497iple_a * fun_fu253747899iple_a ) > bool ).

tff(func_def_17,type,
    big_se913005884ig_int: ( fun_int_fun_int_int * fun_fun_int_bool_int ) > bool ).

tff(func_def_18,type,
    big_se275732192ig_nat: ( fun_nat_fun_nat_nat * fun_fun_nat_bool_nat ) > bool ).

tff(func_def_19,type,
    cOMBB_844853809_state: fun_fu2127278875e_bool ).

tff(func_def_20,type,
    cOMBB_160679318_state: fun_fu88048803e_bool ).

tff(func_def_21,type,
    cOMBB_361863589iple_a: fun_fu372140353a_bool ).

tff(func_def_22,type,
    cOMBB_bool_bool_int: fun_fu1909738875t_bool ).

tff(func_def_23,type,
    cOMBB_bool_bool_nat: fun_fu1509210819t_bool ).

tff(func_def_24,type,
    cOMBB_188601460_state: fun_fu1873708859l_bool ).

tff(func_def_25,type,
    cOMBB_345279363iple_a: fun_fu1022479645l_bool ).

tff(func_def_26,type,
    cOMBB_1652995168ol_int: fun_fu531009635l_bool ).

tff(func_def_27,type,
    cOMBB_1015721476ol_nat: fun_fu1849968923l_bool ).

tff(func_def_28,type,
    cOMBB_135702095iple_a: fun_fu1381603133a_bool ).

tff(func_def_29,type,
    cOMBB_952878892ol_int: fun_fu1681956989a_bool ).

tff(func_def_30,type,
    cOMBB_315605200ol_nat: fun_fu1682168189a_bool ).

tff(func_def_31,type,
    cOMBB_int_int_nat: fun_fu1887272509at_int ).

tff(func_def_32,type,
    cOMBB_2132063381iple_a: fun_fu405047601t_bool ).

tff(func_def_33,type,
    cOMBB_118231410ol_int: fun_fu1997740657t_bool ).

tff(func_def_34,type,
    cOMBB_1628441366ol_nat: fun_fu1576332145t_bool ).

tff(func_def_35,type,
    cOMBB_364359670iple_a: fun_fu1831640381nt_int ).

tff(func_def_36,type,
    cOMBB_nat_int_int: fun_fu603924029nt_int ).

tff(func_def_37,type,
    cOMBB_1877004557iple_a: fun_fu1437424253_a_nat ).

tff(func_def_38,type,
    cOMBB_nat_nat_int: fun_fu773339453nt_nat ).

tff(func_def_39,type,
    cOMBB_nat_nat_nat: fun_fu1179887677at_nat ).

tff(func_def_40,type,
    cOMBB_2017898829iple_a: fun_fu686268865t_bool ).

tff(func_def_41,type,
    cOMBB_1437810218ol_int: fun_fu1109211905t_bool ).

tff(func_def_42,type,
    cOMBB_800536526ol_nat: fun_fu687803393t_bool ).

tff(func_def_43,type,
    cOMBB_1416330906iple_a: fun_fu1755521597at_nat ).

tff(func_def_44,type,
    cOMBB_1601129847at_int: fun_fu1017488637at_nat ).

tff(func_def_45,type,
    cOMBB_963856155at_nat: fun_fu1799328765at_nat ).

tff(func_def_46,type,
    cOMBB_1355796797bool_a: fun_fu1340893257l_bool ).

tff(func_def_47,type,
    cOMBB_2139825703bool_a: fun_fu817723125e_bool ).

tff(func_def_48,type,
    cOMBB_1348041619bool_a: fun_fu1860059197e_bool ).

tff(func_def_49,type,
    cOMBB_145932198bool_a: fun_fu1631777789e_bool ).

tff(func_def_50,type,
    cOMBB_1676209667iple_a: fun_fu870629313a_bool ).

tff(func_def_51,type,
    cOMBB_605112827at_nat: fun_fu898837677at_nat ).

tff(func_def_52,type,
    cOMBB_1848875326ol_int: fun_fu600978683a_bool ).

tff(func_def_53,type,
    cOMBB_1211601634ol_nat: fun_fu1912089667a_bool ).

tff(func_def_54,type,
    cOMBB_2036667361iple_a: fun_fu743040865a_bool ).

tff(func_def_55,type,
    cOMBB_434376058at_int: fun_fu1739618017ol_nat ).

tff(func_def_56,type,
    cOMBB_1944586014at_nat: fun_fu774707681ol_nat ).

tff(func_def_57,type,
    cOMBB_1418110531ol_int: fun_fu1671602619t_bool ).

tff(func_def_58,type,
    cOMBB_1983399767iple_a: fun_fu2017547765_a_nat ).

tff(func_def_59,type,
    cOMBB_2018621492at_int: fun_fu1795303867nt_nat ).

tff(func_def_60,type,
    cOMBB_1381347800at_nat: fun_fu1888474227at_nat ).

tff(func_def_61,type,
    cOMBB_349652263iple_a: fun_fu763112513t_bool ).

tff(func_def_62,type,
    cOMBB_591320580ol_int: fun_fu1521371387t_bool ).

tff(func_def_63,type,
    cOMBB_2101530536ol_nat: fun_fu788822083t_bool ).

tff(func_def_64,type,
    cOMBB_765314529ol_int: fun_fu873308769t_bool ).

tff(func_def_65,type,
    cOMBB_1701789015iple_a: fun_fu651819309ol_nat ).

tff(func_def_66,type,
    cOMBB_2091167284at_int: fun_fu657063149ol_nat ).

tff(func_def_67,type,
    cOMBB_1453893592at_nat: fun_fu342964205ol_nat ).

tff(func_def_68,type,
    cOMBB_955900739ol_nat: fun_fu1402718723t_bool ).

tff(func_def_69,type,
    cOMBB_1733887227iple_a: fun_fu1155082413_a_nat ).

tff(func_def_70,type,
    cOMBB_1125113304at_int: fun_fu523748467nt_nat ).

tff(func_def_71,type,
    cOMBB_1063904223iple_a: fun_fu2137156673t_bool ).

tff(func_def_72,type,
    cOMBB_1746576572ol_int: fun_fu719081723t_bool ).

tff(func_def_73,type,
    cOMBB_1654519265ol_nat: fun_fu1738364513t_bool ).

tff(func_def_74,type,
    cOMBB_1353751246at_nat: fun_fu687095869_a_nat ).

tff(func_def_75,type,
    cOMBB_737513486at_nat: fun_fu504533053nt_nat ).

tff(func_def_76,type,
    cOMBB_636937375iple_a: fun_fu1838203037ol_nat ).

tff(func_def_77,type,
    cOMBB_1562322300at_int: fun_fu294108253ol_nat ).

tff(func_def_78,type,
    cOMBB_151870093iple_a: fun_fu477648637at_nat ).

tff(func_def_79,type,
    cOMBB_891709290at_int: fun_fu633097021at_nat ).

tff(func_def_80,type,
    cOMBC_41962815e_bool: fun_fu222103665e_bool ).

tff(func_def_81,type,
    cOMBC_524597097e_bool: fun_fu1009378087e_bool ).

tff(func_def_82,type,
    cOMBC_892787026e_bool: fun_fu734682033e_bool ).

tff(func_def_83,type,
    cOMBC_2027030106e_bool: fun_fu402792811e_bool ).

tff(func_def_84,type,
    cOMBC_1193272608_state: fun_fu1067796093_state ).

tff(func_def_85,type,
    cOMBC_231445413l_bool: fun_fu1219323149e_bool ).

tff(func_def_86,type,
    cOMBC_1047656090a_bool: fun_fu630820007a_bool ).

tff(func_def_87,type,
    cOMBC_1771170551t_bool: fun_fu697888865a_bool ).

tff(func_def_88,type,
    cOMBC_1149022448nt_nat: fun_fu1217459197_a_nat ).

tff(func_def_89,type,
    cOMBC_240829083t_bool: fun_fu552225705a_bool ).

tff(func_def_90,type,
    cOMBC_1942990924at_nat: fun_fu1305006333_a_nat ).

tff(func_def_91,type,
    cOMBC_1529670358l_bool: fun_fu1498271147a_bool ).

tff(func_def_92,type,
    cOMBC_175592824a_bool: fun_fu1585255851a_bool ).

tff(func_def_93,type,
    cOMBC_1664565648ol_nat: fun_fu728204273_a_nat ).

tff(func_def_94,type,
    cOMBC_340603916at_nat: fun_fu2109513853at_nat ).

tff(func_def_95,type,
    cOMBC_1135948669a_bool: fun_fu713748577t_bool ).

tff(func_def_96,type,
    cOMBC_1499522794_a_nat: fun_fu224004093nt_nat ).

tff(func_def_97,type,
    cOMBC_int_int_bool: fun_fu257678363t_bool ).

tff(func_def_98,type,
    cOMBC_int_int_nat: fun_fu214894141nt_nat ).

tff(func_def_99,type,
    cOMBC_int_nat_bool: fun_fu1890060131t_bool ).

tff(func_def_100,type,
    cOMBC_int_nat_nat: fun_fu652796733nt_nat ).

tff(func_def_101,type,
    cOMBC_94739984l_bool: fun_fu1374874789t_bool ).

tff(func_def_102,type,
    cOMBC_1683390479t_bool: fun_fu407119589t_bool ).

tff(func_def_103,type,
    cOMBC_462113011ol_nat: fun_fu591799985nt_nat ).

tff(func_def_104,type,
    cOMBC_1294079849at_nat: fun_fu1218916157at_nat ).

tff(func_def_105,type,
    cOMBC_2097822937a_bool: fun_fu1453083561t_bool ).

tff(func_def_106,type,
    cOMBC_23578254_a_nat: fun_fu1251828989at_nat ).

tff(func_def_107,type,
    cOMBC_nat_int_bool: fun_fu100665187t_bool ).

tff(func_def_108,type,
    cOMBC_nat_int_nat: fun_fu84751165at_nat ).

tff(func_def_109,type,
    cOMBC_nat_nat_bool: fun_fu1733046955t_bool ).

tff(func_def_110,type,
    cOMBC_nat_nat_nat: fun_fu522653757at_nat ).

tff(func_def_111,type,
    cOMBC_129115664ol_nat: fun_fu55165875at_nat ).

tff(func_def_112,type,
    cOMBC_130242509_a_nat: fun_fu1480131645_a_nat ).

tff(func_def_113,type,
    cOMBC_1505178355ol_nat: fun_fu1373519097at_nat ).

tff(func_def_114,type,
    cOMBC_1218031117nt_nat: fun_fu1251161661nt_nat ).

tff(func_def_115,type,
    cOMBC_226598744l_bool: fun_fu80187629t_bool ).

tff(func_def_116,type,
    cOMBC_178881787t_bool: fun_fu1538037805t_bool ).

tff(func_def_117,type,
    cOMBC_1515890438l_bool: fun_fu1236051915l_bool ).

tff(func_def_118,type,
    cOMBC_2005334440a_bool: fun_fu1595031695a_bool ).

tff(func_def_119,type,
    cOMBC_605892544l_bool: fun_fu1276998475l_bool ).

tff(func_def_120,type,
    cOMBC_922884543t_bool: fun_fu680577737t_bool ).

tff(func_def_121,type,
    cOMBC_1693257480l_bool: fun_fu820922699l_bool ).

tff(func_def_122,type,
    cOMBC_646315179t_bool: fun_fu257437713t_bool ).

tff(func_def_123,type,
    cOMBI_1928055558iple_a: fun_Ho1518252029iple_a ).

tff(func_def_124,type,
    cOMBI_int: fun_int_int ).

tff(func_def_125,type,
    cOMBI_nat: fun_nat_nat ).

tff(func_def_126,type,
    cOMBK_bool_state: fun_bo1936561970e_bool ).

tff(func_def_127,type,
    cOMBK_861658160iple_a: fun_bo840878273a_bool ).

tff(func_def_128,type,
    cOMBK_bool_int: fun_bo1829594782t_bool ).

tff(func_def_129,type,
    cOMBK_bool_nat: fun_bo1570548802t_bool ).

tff(func_def_130,type,
    cOMBK_788297294iple_a: fun_Ho483360497iple_a ).

tff(func_def_131,type,
    cOMBK_1633947825iple_a: fun_in990358449_a_int ).

tff(func_def_132,type,
    cOMBK_int_int: fun_int_fun_int_int ).

tff(func_def_133,type,
    cOMBK_int_nat: fun_int_fun_nat_int ).

tff(func_def_134,type,
    cOMBK_1654814733iple_a: fun_na841142961_a_nat ).

tff(func_def_135,type,
    cOMBK_nat_int: fun_nat_fun_int_nat ).

tff(func_def_136,type,
    cOMBK_nat_nat: fun_nat_fun_nat_nat ).

tff(func_def_137,type,
    cOMBK_1458035955bool_a: fun_fu281355805e_bool ).

tff(func_def_138,type,
    cOMBS_1378840469l_bool: fun_fu1047394976e_bool ).

tff(func_def_139,type,
    cOMBS_777315357_state: fun_fu227828410_state ).

tff(func_def_140,type,
    cOMBS_1108095524l_bool: fun_fu805217741a_bool ).

tff(func_def_141,type,
    cOMBS_728441660nt_int: fun_fu907920777_a_int ).

tff(func_def_142,type,
    cOMBS_885136444at_nat: fun_fu84072329_a_nat ).

tff(func_def_143,type,
    cOMBS_1838073924ol_nat: fun_fu1310697751_a_nat ).

tff(func_def_144,type,
    cOMBS_902588832ol_nat: fun_fu1071091151_a_nat ).

tff(func_def_145,type,
    cOMBS_int_bool_bool: fun_fu587508068t_bool ).

tff(func_def_146,type,
    cOMBS_int_nat_nat: fun_fu1650807462nt_nat ).

tff(func_def_147,type,
    cOMBS_443177668ol_nat: fun_fu2087062900nt_nat ).

tff(func_def_148,type,
    cOMBS_1999073191ol_nat: fun_fu1989253562nt_nat ).

tff(func_def_149,type,
    cOMBS_1063588099ol_nat: fun_fu776947314nt_nat ).

tff(func_def_150,type,
    cOMBS_nat_bool_bool: fun_fu1901564496t_bool ).

tff(func_def_151,type,
    cOMBS_nat_nat_nat: fun_fu1382375754at_nat ).

tff(func_def_152,type,
    cOMBS_1514622496ol_nat: fun_fu1446087120at_nat ).

tff(func_def_153,type,
    cOMBS_2106653443ol_nat: fun_fu1081900566at_nat ).

tff(func_def_154,type,
    ass: ( vname * fun_state_nat ) > com ).

tff(func_def_155,type,
    skip: com ).

tff(func_def_156,type,
    semi: ( com * com ) > com ).

tff(func_def_157,type,
    finite_card_int: fun_fun_int_bool_nat ).

tff(func_def_158,type,
    finite_card_nat: fun_fun_nat_bool_nat ).

tff(func_def_159,type,
    finite164030737iple_a: fun_Ho483360497iple_a > bool ).

tff(func_def_160,type,
    finite1617795063a_bool: fun_Ho112928087a_bool > bool ).

tff(func_def_161,type,
    finite1973466193nt_int: fun_int_fun_int_int > bool ).

tff(func_def_162,type,
    finite1321096241t_bool: fun_in719570932t_bool > bool ).

tff(func_def_163,type,
    finite2130160977at_nat: fun_nat_fun_nat_nat > bool ).

tff(func_def_164,type,
    finite1071749497t_bool: fun_na35521688t_bool > bool ).

tff(func_def_165,type,
    finite1532229644iple_a: fun_Ho483360497iple_a > bool ).

tff(func_def_166,type,
    finite1306023740a_bool: fun_Ho112928087a_bool > bool ).

tff(func_def_167,type,
    finite1704255308nt_int: fun_int_fun_int_int > bool ).

tff(func_def_168,type,
    finite58652534t_bool: fun_in719570932t_bool > bool ).

tff(func_def_169,type,
    finite1860950092at_nat: fun_nat_fun_nat_nat > bool ).

tff(func_def_170,type,
    finite1956789438t_bool: fun_na35521688t_bool > bool ).

tff(func_def_171,type,
    finite217552220iple_a: fun_fu2026518849l_bool ).

tff(func_def_172,type,
    finite_finite_int: fun_fu819804446l_bool ).

tff(func_def_173,type,
    finite_finite_nat: fun_fu425979586l_bool ).

tff(func_def_174,type,
    finite1832883692a_bool: fun_fu1342882871l_bool ).

tff(func_def_175,type,
    finite1395289673t_bool: fun_fu1540142484l_bool ).

tff(func_def_176,type,
    finite2012431853t_bool: fun_fu814369080l_bool ).

tff(func_def_177,type,
    finite100168025iple_a: ( fun_Ho483360497iple_a * fun_Ho882550911a_bool ) > fun_Ho882550911a_bool ).

tff(func_def_178,type,
    finite_fold1Set_int: ( fun_int_fun_int_int * fun_int_bool ) > fun_int_bool ).

tff(func_def_179,type,
    finite_fold1Set_nat: ( fun_nat_fun_nat_nat * fun_nat_bool ) > fun_nat_bool ).

tff(func_def_180,type,
    finite2092228073iple_a: fun_Ho483360497iple_a > fun_fu253747899iple_a ).

tff(func_def_181,type,
    finite_fold1_int: fun_int_fun_int_int > fun_fun_int_bool_int ).

tff(func_def_182,type,
    finite_fold1_nat: fun_nat_fun_nat_nat > fun_fun_nat_bool_nat ).

tff(func_def_183,type,
    finite2089344904iple_a: ( fun_Ho483360497iple_a * hoare_2076525193iple_a ) > fun_fu253747899iple_a ).

tff(func_def_184,type,
    finite718386368a_bool: ( fun_Ho112928087a_bool * fun_Ho882550911a_bool ) > fun_fu1663341283a_bool ).

tff(func_def_185,type,
    finite_fold_int_int: ( fun_int_fun_int_int * int ) > fun_fun_int_bool_int ).

tff(func_def_186,type,
    finite1827710202t_bool: ( fun_in719570932t_bool * fun_int_bool ) > fun_fu554825757t_bool ).

tff(func_def_187,type,
    finite_fold_nat_nat: ( fun_nat_fun_nat_nat * nat ) > fun_fun_nat_bool_nat ).

tff(func_def_188,type,
    finite1578363458t_bool: ( fun_na35521688t_bool * fun_nat_bool ) > fun_fu821463397t_bool ).

tff(func_def_189,type,
    finite974267142iple_a: fun_Ho483360497iple_a > fun_Ho112928087a_bool ).

tff(func_def_190,type,
    finite655745986a_bool: fun_Ho112928087a_bool > fun_fu2104275287l_bool ).

tff(func_def_191,type,
    finite772772422nt_int: fun_int_fun_int_int > fun_in719570932t_bool ).

tff(func_def_192,type,
    finite1008073724t_bool: fun_in719570932t_bool > fun_fu1284533364l_bool ).

tff(func_def_193,type,
    finite929467206at_nat: fun_nat_fun_nat_nat > fun_na35521688t_bool ).

tff(func_def_194,type,
    finite758726980t_bool: fun_na35521688t_bool > fun_fu1216549656l_bool ).

tff(func_def_195,type,
    finite232328454iple_a: ( fun_Ho483360497iple_a * fun_fu253747899iple_a ) > bool ).

tff(func_def_196,type,
    finite1626084323ne_int: ( fun_int_fun_int_int * fun_fun_int_bool_int ) > bool ).

tff(func_def_197,type,
    finite988810631ne_nat: ( fun_nat_fun_nat_nat * fun_fun_nat_bool_nat ) > bool ).

tff(func_def_198,type,
    finite1659845635iple_a: ( fun_Ho483360497iple_a * fun_fu253747899iple_a ) > bool ).

tff(func_def_199,type,
    finite1432773856em_int: ( fun_int_fun_int_int * fun_fun_int_bool_int ) > bool ).

tff(func_def_200,type,
    finite795500164em_nat: ( fun_nat_fun_nat_nat * fun_fun_nat_bool_nat ) > bool ).

tff(func_def_201,type,
    minus_minus_bool: fun_bo1549164019l_bool ).

tff(func_def_202,type,
    minus_minus_int: fun_int_fun_int_int ).

tff(func_def_203,type,
    minus_minus_nat: fun_nat_fun_nat_nat ).

tff(func_def_204,type,
    minus_1649626414a_bool: fun_fu2051904533a_bool ).

tff(func_def_205,type,
    minus_1449998731t_bool: fun_fu1075512626t_bool ).

tff(func_def_206,type,
    minus_2067140911t_bool: fun_fu915923926t_bool ).

tff(func_def_207,type,
    one_one_int: int ).

tff(func_def_208,type,
    one_one_nat: nat ).

tff(func_def_209,type,
    plus_plus_int: fun_int_fun_int_int ).

tff(func_def_210,type,
    plus_plus_nat: fun_nat_fun_nat_nat ).

tff(func_def_211,type,
    times_times_int: fun_int_fun_int_int ).

tff(func_def_212,type,
    times_times_nat: fun_nat_fun_nat_nat ).

tff(func_def_213,type,
    uminus_uminus_int: fun_int_int ).

tff(func_def_214,type,
    zero_zero_int: int ).

tff(func_def_215,type,
    zero_zero_nat: nat ).

tff(func_def_216,type,
    the_Ho1456473914iple_a: fun_fu253747899iple_a ).

tff(func_def_217,type,
    the_int: fun_fun_int_bool_int ).

tff(func_def_218,type,
    the_nat: fun_fun_nat_bool_nat ).

tff(func_def_219,type,
    the_fu972267150a_bool: fun_fu1819779801a_bool ).

tff(func_def_220,type,
    the_fun_int_bool: fun_fu1421432211t_bool ).

tff(func_def_221,type,
    the_fun_nat_bool: fun_fu496092379t_bool ).

tff(func_def_222,type,
    hoare_572465367rivs_a: fun_Ho882550911a_bool > fun_fu2026518849l_bool ).

tff(func_def_223,type,
    hoare_1876769875iple_a: ( fun_a_fun_state_bool * com * fun_a_fun_state_bool ) > hoare_2076525193iple_a ).

tff(func_def_224,type,
    if_nat: bool > fun_nat_fun_nat_nat ).

tff(func_def_225,type,
    semiri1621563631at_int: fun_nat_int ).

tff(func_def_226,type,
    update: fun_st1816159843_state ).

tff(func_def_227,type,
    bot_bot_bool: bool ).

tff(func_def_228,type,
    bot_bot_nat: nat ).

tff(func_def_229,type,
    bot_bo214064617a_bool: fun_Ho882550911a_bool ).

tff(func_def_230,type,
    bot_bot_fun_int_bool: fun_int_bool ).

tff(func_def_231,type,
    bot_bot_fun_nat_bool: fun_nat_bool ).

tff(func_def_232,type,
    ord_less_int: fun_int_fun_int_bool ).

tff(func_def_233,type,
    ord_less_nat: fun_nat_fun_nat_bool ).

tff(func_def_234,type,
    ord_le1912455174t_bool: fun_fu1151772339l_bool ).

tff(func_def_235,type,
    ord_le382113706t_bool: fun_fu1217155507l_bool ).

tff(func_def_236,type,
    ord_less_eq_bool: fun_bo1549164019l_bool ).

tff(func_def_237,type,
    ord_less_eq_int: fun_int_fun_int_bool ).

tff(func_def_238,type,
    ord_less_eq_nat: fun_nat_fun_nat_bool ).

tff(func_def_239,type,
    ord_le940607413a_bool: fun_fu1789210355l_bool ).

tff(func_def_240,type,
    ord_le951220754t_bool: fun_fu1151772339l_bool ).

tff(func_def_241,type,
    ord_le1568362934t_bool: fun_fu1217155507l_bool ).

tff(func_def_242,type,
    ord_max_nat: fun_nat_fun_nat_nat ).

tff(func_def_243,type,
    ord_min_int: fun_int_fun_int_int ).

tff(func_def_244,type,
    ord_min_nat: fun_nat_fun_nat_nat ).

tff(func_def_245,type,
    partia428461311iple_a: hoare_2076525193iple_a > fun_fu253747899iple_a ).

tff(func_def_246,type,
    partial_flat_lub_int: int > fun_fun_int_bool_int ).

tff(func_def_247,type,
    partial_flat_lub_nat: nat > fun_fun_nat_bool_nat ).

tff(func_def_248,type,
    power_power_int: fun_int_fun_nat_int ).

tff(func_def_249,type,
    power_power_nat: fun_nat_fun_nat_nat ).

tff(func_def_250,type,
    ord_at875362053st_int: int > fun_int_fun_int_bool ).

tff(func_def_251,type,
    ord_at238088361st_nat: nat > fun_nat_fun_nat_bool ).

tff(func_def_252,type,
    ord_gr375877188st_nat: nat > fun_nat_fun_nat_bool ).

tff(func_def_253,type,
    ord_lessThan_int: fun_int_fun_int_bool ).

tff(func_def_254,type,
    ord_lessThan_nat: fun_nat_fun_nat_bool ).

tff(func_def_255,type,
    collec977865374iple_a: fun_fu1663341283a_bool ).

tff(func_def_256,type,
    collect_int: fun_fu554825757t_bool ).

tff(func_def_257,type,
    collect_nat: fun_fu821463397t_bool ).

tff(func_def_258,type,
    collec416005674a_bool: fun_fu1354972029l_bool ).

tff(func_def_259,type,
    collect_fun_int_bool: fun_fu1070826941l_bool ).

tff(func_def_260,type,
    collect_fun_nat_bool: fun_fu616551101l_bool ).

tff(func_def_261,type,
    image_1416816325iple_a: ( fun_Ho1518252029iple_a * fun_Ho882550911a_bool ) > fun_Ho882550911a_bool ).

tff(func_def_262,type,
    image_268182434_a_int: ( fun_Ho1026035802_a_int * fun_Ho882550911a_bool ) > fun_int_bool ).

tff(func_def_263,type,
    image_1778392390_a_nat: ( fun_Ho864122878_a_nat * fun_Ho882550911a_bool ) > fun_nat_bool ).

tff(func_def_264,type,
    image_323610408iple_a: ( fun_in1219646560iple_a * fun_int_bool ) > fun_Ho882550911a_bool ).

tff(func_def_265,type,
    image_int_int: ( fun_int_int * fun_int_bool ) > fun_int_bool ).

tff(func_def_266,type,
    image_int_nat: ( fun_int_nat * fun_int_bool ) > fun_nat_bool ).

tff(func_def_267,type,
    image_344477316iple_a: ( fun_na1240513468iple_a * fun_nat_bool ) > fun_Ho882550911a_bool ).

tff(func_def_268,type,
    image_nat_int: ( fun_nat_int * fun_nat_bool ) > fun_int_bool ).

tff(func_def_269,type,
    image_nat_nat: ( fun_nat_nat * fun_nat_bool ) > fun_nat_bool ).

tff(func_def_270,type,
    insert1582918915iple_a: fun_Ho112928087a_bool ).

tff(func_def_271,type,
    insert_int: fun_in719570932t_bool ).

tff(func_def_272,type,
    insert_nat: fun_na35521688t_bool ).

tff(func_def_273,type,
    the_el2146174248iple_a: fun_fu253747899iple_a ).

tff(func_def_274,type,
    the_elem_int: fun_fun_int_bool_int ).

tff(func_def_275,type,
    the_elem_nat: fun_fun_nat_bool_nat ).

tff(func_def_276,type,
    fFalse: bool ).

tff(func_def_277,type,
    fNot: fun_bool_bool ).

tff(func_def_278,type,
    fTrue: bool ).

tff(func_def_279,type,
    fconj: fun_bo1549164019l_bool ).

tff(func_def_280,type,
    fdisj: fun_bo1549164019l_bool ).

tff(func_def_281,type,
    fequal_state: fun_st1506752259e_bool ).

tff(func_def_282,type,
    fequal1589671816iple_a: fun_Ho943022881a_bool ).

tff(func_def_283,type,
    fequal_int: fun_int_fun_int_bool ).

tff(func_def_284,type,
    fequal_nat: fun_nat_fun_nat_bool ).

tff(func_def_285,type,
    fequal291249344a_bool: fun_fu1789210355l_bool ).

tff(func_def_286,type,
    fequal_fun_int_bool: fun_fu1151772339l_bool ).

tff(func_def_287,type,
    fequal_fun_nat_bool: fun_fu1217155507l_bool ).

tff(func_def_288,type,
    fimplies: fun_bo1549164019l_bool ).

tff(func_def_289,type,
    hAPP_a2036067514e_bool: ( fun_a_fun_state_bool * x_a ) > fun_state_bool ).

tff(func_def_290,type,
    hAPP_a849909144l_bool: ( fun_a_1632297036l_bool * x_a ) > fun_st2063251938l_bool ).

tff(func_def_291,type,
    hAPP_a723219176e_bool: ( fun_a_998512028e_bool * x_a ) > fun_bo1936561970e_bool ).

tff(func_def_292,type,
    hAPP_a1224971408e_bool: ( fun_a_340690546e_bool * x_a ) > fun_fu78956742e_bool ).

tff(func_def_293,type,
    hAPP_a1200519163e_bool: ( fun_a_2117018159e_bool * x_a ) > fun_fu373216837e_bool ).

tff(func_def_294,type,
    hAPP_state_state: ( fun_state_state * state ) > state ).

tff(func_def_295,type,
    hAPP_state_bool: ( fun_state_bool * state ) > bool ).

tff(func_def_296,type,
    hAPP_state_nat: ( fun_state_nat * state ) > nat ).

tff(func_def_297,type,
    hAPP_s1806633685e_bool: ( fun_st1506752259e_bool * state ) > fun_state_bool ).

tff(func_def_298,type,
    hAPP_s712361723_state: ( fun_st1816159843_state * state ) > fun_vn774578976_state ).

tff(func_def_299,type,
    hAPP_s58564346l_bool: ( fun_st2063251938l_bool * state ) > fun_bool_bool ).

tff(func_def_300,type,
    hAPP_s1892499976_state: ( fun_st2072884720_state * state ) > fun_nat_state ).

tff(func_def_301,type,
    hAPP_v365393659_state: ( fun_vn299216483_state * vname ) > fun_st2072884720_state ).

tff(func_def_302,type,
    hAPP_v594194232_state: ( fun_vn774578976_state * vname ) > fun_nat_state ).

tff(func_def_303,type,
    hAPP_bool_bool: ( fun_bool_bool * bool ) > bool ).

tff(func_def_304,type,
    hAPP_b540892988e_bool: ( fun_bo675861616e_bool * bool ) > fun_a_fun_state_bool ).

tff(func_def_305,type,
    hAPP_b2019457360e_bool: ( fun_bo1936561970e_bool * bool ) > fun_state_bool ).

tff(func_def_306,type,
    hAPP_b589554111l_bool: ( fun_bo1549164019l_bool * bool ) > fun_bool_bool ).

tff(func_def_307,type,
    hAPP_b1299643615a_bool: ( fun_bo840878273a_bool * bool ) > fun_Ho882550911a_bool ).

tff(func_def_308,type,
    hAPP_b396694332t_bool: ( fun_bo1829594782t_bool * bool ) > fun_int_bool ).

tff(func_def_309,type,
    hAPP_b1013836512t_bool: ( fun_bo1570548802t_bool * bool ) > fun_nat_bool ).

tff(func_def_310,type,
    hAPP_H454055633a_bool: ( fun_Ho882550911a_bool * hoare_2076525193iple_a ) > bool ).

tff(func_def_311,type,
    hAPP_H1789220885iple_a: ( fun_Ho1518252029iple_a * hoare_2076525193iple_a ) > hoare_2076525193iple_a ).

tff(func_def_312,type,
    hAPP_H811578610_a_int: ( fun_Ho1026035802_a_int * hoare_2076525193iple_a ) > int ).

tff(func_def_313,type,
    hAPP_H174304918_a_nat: ( fun_Ho864122878_a_nat * hoare_2076525193iple_a ) > nat ).

tff(func_def_314,type,
    hAPP_H421140395l_bool: ( fun_Ho2037816211l_bool * hoare_2076525193iple_a ) > fun_bool_bool ).

tff(func_def_315,type,
    hAPP_H2077279219a_bool: ( fun_Ho943022881a_bool * hoare_2076525193iple_a ) > fun_Ho882550911a_bool ).

tff(func_def_316,type,
    hAPP_H1417936777iple_a: ( fun_Ho483360497iple_a * hoare_2076525193iple_a ) > fun_Ho1518252029iple_a ).

tff(func_def_317,type,
    hAPP_H287744592t_bool: ( fun_Ho1608761598t_bool * hoare_2076525193iple_a ) > fun_int_bool ).

tff(func_def_318,type,
    hAPP_H1936429641nt_int: ( fun_Ho1977546161nt_int * hoare_2076525193iple_a ) > fun_int_int ).

tff(func_def_319,type,
    hAPP_H1774516717nt_nat: ( fun_Ho1488374613nt_nat * hoare_2076525193iple_a ) > fun_int_nat ).

tff(func_def_320,type,
    hAPP_H904886772t_bool: ( fun_Ho1349715618t_bool * hoare_2076525193iple_a ) > fun_nat_bool ).

tff(func_def_321,type,
    hAPP_H421001545at_nat: ( fun_Ho1036508337at_nat * hoare_2076525193iple_a ) > fun_nat_nat ).

tff(func_def_322,type,
    hAPP_H1566092493l_bool: ( fun_Ho1910759733l_bool * hoare_2076525193iple_a ) > fun_fu2026518849l_bool ).

tff(func_def_323,type,
    hAPP_H1940471919a_bool: ( fun_Ho112928087a_bool * hoare_2076525193iple_a ) > fun_fu1663341283a_bool ).

tff(func_def_324,type,
    hAPP_H906838291ol_nat: ( fun_Ho1634634433ol_nat * hoare_2076525193iple_a ) > fun_fun_int_bool_nat ).

tff(func_def_325,type,
    hAPP_H2118836847ol_nat: ( fun_Ho1345928733ol_nat * hoare_2076525193iple_a ) > fun_fun_nat_bool_nat ).

tff(func_def_326,type,
    hAPP_H1504435465at_nat: ( fun_Ho755902321at_nat * hoare_2076525193iple_a ) > fun_fu325663101at_nat ).

tff(func_def_327,type,
    hAPP_int_bool: ( fun_int_bool * int ) > bool ).

tff(func_def_328,type,
    hAPP_i867006584iple_a: ( fun_in1219646560iple_a * int ) > hoare_2076525193iple_a ).

tff(func_def_329,type,
    hAPP_int_int: ( fun_int_int * int ) > int ).

tff(func_def_330,type,
    hAPP_int_nat: ( fun_int_nat * int ) > nat ).

tff(func_def_331,type,
    hAPP_i68813070l_bool: ( fun_in531499254l_bool * int ) > fun_bool_bool ).

tff(func_def_332,type,
    hAPP_i28602320a_bool: ( fun_in451447550a_bool * int ) > fun_Ho882550911a_bool ).

tff(func_def_333,type,
    hAPP_i1058170057_a_int: ( fun_in990358449_a_int * int ) > fun_Ho1026035802_a_int ).

tff(func_def_334,type,
    hAPP_i896257133_a_nat: ( fun_in501186901_a_nat * int ) > fun_Ho864122878_a_nat ).

tff(func_def_335,type,
    hAPP_i1948725293t_bool: ( fun_int_fun_int_bool * int ) > fun_int_bool ).

tff(func_def_336,type,
    hAPP_int_fun_int_int: ( fun_int_fun_int_int * int ) > fun_int_int ).

tff(func_def_337,type,
    hAPP_int_fun_int_nat: ( fun_int_fun_int_nat * int ) > fun_int_nat ).

tff(func_def_338,type,
    hAPP_i418383825t_bool: ( fun_int_fun_nat_bool * int ) > fun_nat_bool ).

tff(func_def_339,type,
    hAPP_int_fun_nat_int: ( fun_int_fun_nat_int * int ) > fun_nat_int ).

tff(func_def_340,type,
    hAPP_int_fun_nat_nat: ( fun_int_fun_nat_nat * int ) > fun_nat_nat ).

tff(func_def_341,type,
    hAPP_i291839885ol_nat: ( fun_in149899451ol_nat * int ) > fun_fu328701628ol_nat ).

tff(func_def_342,type,
    hAPP_i2112223885l_bool: ( fun_in938817141l_bool * int ) > fun_fu819804446l_bool ).

tff(func_def_343,type,
    hAPP_i318423664ol_nat: ( fun_in1461553182ol_nat * int ) > fun_fun_int_bool_nat ).

tff(func_def_344,type,
    hAPP_i1529485324t_bool: ( fun_in719570932t_bool * int ) > fun_fu554825757t_bool ).

tff(func_def_345,type,
    hAPP_i1530422220ol_nat: ( fun_in1172847482ol_nat * int ) > fun_fun_nat_bool_nat ).

tff(func_def_346,type,
    hAPP_i1876697324at_nat: ( fun_in1791225684at_nat * int ) > fun_fu325663101at_nat ).

tff(func_def_347,type,
    hAPP_nat_state: ( fun_nat_state * nat ) > state ).

tff(func_def_348,type,
    hAPP_nat_bool: ( fun_nat_bool * nat ) > bool ).

tff(func_def_349,type,
    hAPP_n887873492iple_a: ( fun_na1240513468iple_a * nat ) > hoare_2076525193iple_a ).

tff(func_def_350,type,
    hAPP_nat_int: ( fun_nat_int * nat ) > int ).

tff(func_def_351,type,
    hAPP_nat_nat: ( fun_nat_nat * nat ) > nat ).

tff(func_def_352,type,
    hAPP_n1006566506l_bool: ( fun_na1469252690l_bool * nat ) > fun_bool_bool ).

tff(func_def_353,type,
    hAPP_n1335981428a_bool: ( fun_na1758826658a_bool * nat ) > fun_Ho882550911a_bool ).

tff(func_def_354,type,
    hAPP_n1236213193_a_nat: ( fun_na841142961_a_nat * nat ) > fun_Ho864122878_a_nat ).

tff(func_def_355,type,
    hAPP_n1082236369t_bool: ( fun_nat_fun_int_bool * nat ) > fun_int_bool ).

tff(func_def_356,type,
    hAPP_nat_fun_int_nat: ( fun_nat_fun_int_nat * nat ) > fun_int_nat ).

tff(func_def_357,type,
    hAPP_n1699378549t_bool: ( fun_nat_fun_nat_bool * nat ) > fun_nat_bool ).

tff(func_def_358,type,
    hAPP_nat_fun_nat_nat: ( fun_nat_fun_nat_nat * nat ) > fun_nat_nat ).

tff(func_def_359,type,
    hAPP_n370719537ol_nat: ( fun_na228779103ol_nat * nat ) > fun_fu328701628ol_nat ).

tff(func_def_360,type,
    hAPP_n226523272_a_nat: ( fun_na1588060912_a_nat * nat ) > fun_fu1923493821_a_nat ).

tff(func_def_361,type,
    hAPP_n259507732ol_nat: ( fun_na1402637250ol_nat * nat ) > fun_fun_int_bool_nat ).

tff(func_def_362,type,
    hAPP_n74706760nt_nat: ( fun_na266550704nt_nat * nat ) > fun_fu1789282941nt_nat ).

tff(func_def_363,type,
    hAPP_n215258509l_bool: ( fun_na1436237685l_bool * nat ) > fun_fu425979586l_bool ).

tff(func_def_364,type,
    hAPP_n1512601776t_bool: ( fun_na35521688t_bool * nat ) > fun_fu821463397t_bool ).

tff(func_def_365,type,
    hAPP_f1509969235l_bool: ( fun_fu2118559873l_bool * fun_a_fun_state_bool ) > fun_a_1632297036l_bool ).

tff(func_def_366,type,
    hAPP_f1406200875e_bool: ( fun_fu278206227e_bool * fun_a_fun_state_bool ) > fun_a_340690546e_bool ).

tff(func_def_367,type,
    hAPP_f340725611e_bool: ( fun_fu1591723597e_bool * fun_a_1632297036l_bool ) > fun_a_998512028e_bool ).

tff(func_def_368,type,
    hAPP_f963367678e_bool: ( fun_fu2008829792e_bool * fun_a_1632297036l_bool ) > fun_a_2117018159e_bool ).

tff(func_def_369,type,
    hAPP_f1824947087e_bool: ( fun_fu222103665e_bool * fun_a_998512028e_bool ) > fun_bo675861616e_bool ).

tff(func_def_370,type,
    hAPP_f1460451647e_bool: ( fun_fu1009378087e_bool * fun_a_340690546e_bool ) > fun_fu796809180e_bool ).

tff(func_def_371,type,
    hAPP_f1261923407e_bool: ( fun_fu734682033e_bool * fun_a_2117018159e_bool ) > fun_fu281355805e_bool ).

tff(func_def_372,type,
    hAPP_f100967412e_bool: ( fun_fu796809180e_bool * fun_state_state ) > fun_a_fun_state_bool ).

tff(func_def_373,type,
    hAPP_f746301080e_bool: ( fun_fu78956742e_bool * fun_state_state ) > fun_state_bool ).

tff(func_def_374,type,
    hAPP_f762886889e_bool: ( fun_fu281355805e_bool * fun_state_bool ) > fun_a_fun_state_bool ).

tff(func_def_375,type,
    hAPP_f1759915619e_bool: ( fun_fu373216837e_bool * fun_state_bool ) > fun_state_bool ).

tff(func_def_376,type,
    hAPP_f1259673775l_bool: ( fun_fu1658206819l_bool * fun_state_bool ) > fun_st2063251938l_bool ).

tff(func_def_377,type,
    hAPP_f162060345e_bool: ( fun_fu2127278875e_bool * fun_state_bool ) > fun_fu78956742e_bool ).

tff(func_def_378,type,
    hAPP_f871651461_state: ( fun_fu978939117_state * fun_state_nat ) > fun_state_state ).

tff(func_def_379,type,
    hAPP_f817621513e_bool: ( fun_fu402792811e_bool * fun_st1506752259e_bool ) > fun_st1506752259e_bool ).

tff(func_def_380,type,
    hAPP_f1542232213_state: ( fun_fu1067796093_state * fun_st1816159843_state ) > fun_vn299216483_state ).

tff(func_def_381,type,
    hAPP_f167292325e_bool: ( fun_fu1219323149e_bool * fun_st2063251938l_bool ) > fun_bo1936561970e_bool ).

tff(func_def_382,type,
    hAPP_f644196280e_bool: ( fun_fu1047394976e_bool * fun_st2063251938l_bool ) > fun_fu373216837e_bool ).

tff(func_def_383,type,
    hAPP_f851239890_state: ( fun_fu227828410_state * fun_st2072884720_state ) > fun_fu978939117_state ).

tff(func_def_384,type,
    hAPP_f2073279419e_bool: ( fun_fu88048803e_bool * fun_bool_bool ) > fun_fu373216837e_bool ).

tff(func_def_385,type,
    hAPP_f629438041a_bool: ( fun_fu372140353a_bool * fun_bool_bool ) > fun_fu1663341283a_bool ).

tff(func_def_386,type,
    hAPP_f627970963t_bool: ( fun_fu1909738875t_bool * fun_bool_bool ) > fun_fu554825757t_bool ).

tff(func_def_387,type,
    hAPP_f894608603t_bool: ( fun_fu1509210819t_bool * fun_bool_bool ) > fun_fu821463397t_bool ).

tff(func_def_388,type,
    hAPP_f1561913689l_bool: ( fun_fu1873708859l_bool * fun_bo1549164019l_bool ) > fun_fu1658206819l_bool ).

tff(func_def_389,type,
    hAPP_f1261090107l_bool: ( fun_fu1022479645l_bool * fun_bo1549164019l_bool ) > fun_fu1067550789l_bool ).

tff(func_def_390,type,
    hAPP_f1734373249l_bool: ( fun_fu531009635l_bool * fun_bo1549164019l_bool ) > fun_fu610077323l_bool ).

tff(func_def_391,type,
    hAPP_f1080886329l_bool: ( fun_fu1849968923l_bool * fun_bo1549164019l_bool ) > fun_fu2104074051l_bool ).

tff(func_def_392,type,
    hAPP_f500854239l_bool: ( fun_fu2026518849l_bool * fun_Ho882550911a_bool ) > bool ).

tff(func_def_393,type,
    hAPP_f2009966983iple_a: ( fun_fu253747899iple_a * fun_Ho882550911a_bool ) > hoare_2076525193iple_a ).

tff(func_def_394,type,
    hAPP_f827914852ol_int: ( fun_fu490614552ol_int * fun_Ho882550911a_bool ) > int ).

tff(func_def_395,type,
    hAPP_f190641160ol_nat: ( fun_fu328701628ol_nat * fun_Ho882550911a_bool ) > nat ).

tff(func_def_396,type,
    hAPP_f642208769a_bool: ( fun_fu1663341283a_bool * fun_Ho882550911a_bool ) > fun_Ho882550911a_bool ).

tff(func_def_397,type,
    hAPP_f268025233l_bool: ( fun_fu1067550789l_bool * fun_Ho882550911a_bool ) > fun_Ho2037816211l_bool ).

tff(func_def_398,type,
    hAPP_f219434403a_bool: ( fun_fu1725628421a_bool * fun_Ho882550911a_bool ) > fun_Ho943022881a_bool ).

tff(func_def_399,type,
    hAPP_f479558075at_nat: ( fun_fu662538351at_nat * fun_Ho882550911a_bool ) > fun_nat_nat ).

tff(func_def_400,type,
    hAPP_f256727871l_bool: ( fun_fu1789210355l_bool * fun_Ho882550911a_bool ) > fun_fu2026518849l_bool ).

tff(func_def_401,type,
    hAPP_f1418638817a_bool: ( fun_fu2051904533a_bool * fun_Ho882550911a_bool ) > fun_fu1663341283a_bool ).

tff(func_def_402,type,
    hAPP_f845487733l_bool: ( fun_fu2104275287l_bool * fun_Ho882550911a_bool ) > fun_fu1789210355l_bool ).

tff(func_def_403,type,
    hAPP_f1075886601a_bool: ( fun_fu1040446391a_bool * fun_Ho1518252029iple_a ) > fun_Ho943022881a_bool ).

tff(func_def_404,type,
    hAPP_f1382137045_a_int: ( fun_fu1557526205_a_int * fun_Ho1026035802_a_int ) > fun_Ho1026035802_a_int ).

tff(func_def_405,type,
    hAPP_f841024195t_bool: ( fun_fu1733261297t_bool * fun_Ho1026035802_a_int ) > fun_Ho1608761598t_bool ).

tff(func_def_406,type,
    hAPP_f534508204nt_int: ( fun_fu1975973012nt_int * fun_Ho1026035802_a_int ) > fun_Ho1977546161nt_int ).

tff(func_def_407,type,
    hAPP_f1870360797ol_int: ( fun_fu1327528203ol_int * fun_Ho1026035802_a_int ) > fun_fu490614552ol_int ).

tff(func_def_408,type,
    hAPP_f2075363285_a_nat: ( fun_fu1923493821_a_nat * fun_Ho864122878_a_nat ) > fun_Ho864122878_a_nat ).

tff(func_def_409,type,
    hAPP_f570970635t_bool: ( fun_fu1252406585t_bool * fun_Ho864122878_a_nat ) > fun_Ho1349715618t_bool ).

tff(func_def_410,type,
    hAPP_f731653896at_nat: ( fun_fu1300474096at_nat * fun_Ho864122878_a_nat ) > fun_Ho1036508337at_nat ).

tff(func_def_411,type,
    hAPP_f536288520_a_nat: ( fun_fu1472438000_a_nat * fun_Ho864122878_a_nat ) > fun_na841142961_a_nat ).

tff(func_def_412,type,
    hAPP_f1697440293ol_nat: ( fun_fu827349075ol_nat * fun_Ho864122878_a_nat ) > fun_fu328701628ol_nat ).

tff(func_def_413,type,
    hAPP_f1004093413a_bool: ( fun_fu805217741a_bool * fun_Ho2037816211l_bool ) > fun_fu1663341283a_bool ).

tff(func_def_414,type,
    hAPP_f338738851a_bool: ( fun_fu445247621a_bool * fun_Ho943022881a_bool ) > fun_Ho882550911a_bool ).

tff(func_def_415,type,
    hAPP_f877684549a_bool: ( fun_fu630820007a_bool * fun_Ho943022881a_bool ) > fun_Ho943022881a_bool ).

tff(func_def_416,type,
    hAPP_f102426163a_bool: ( fun_fu914297575a_bool * fun_Ho943022881a_bool ) > fun_Ho112928087a_bool ).

tff(func_def_417,type,
    hAPP_f256103387a_bool: ( fun_fu1381603133a_bool * fun_Ho943022881a_bool ) > fun_fu1040446391a_bool ).

tff(func_def_418,type,
    hAPP_f438022427a_bool: ( fun_fu1681956989a_bool * fun_Ho943022881a_bool ) > fun_fu1017053431a_bool ).

tff(func_def_419,type,
    hAPP_f946563611a_bool: ( fun_fu1682168189a_bool * fun_Ho943022881a_bool ) > fun_fu1525594615a_bool ).

tff(func_def_420,type,
    hAPP_f10452157_a_nat: ( fun_fu602188273_a_nat * fun_Ho1608761598t_bool ) > fun_Ho864122878_a_nat ).

tff(func_def_421,type,
    hAPP_f741913983t_bool: ( fun_fu945366625t_bool * fun_Ho1608761598t_bool ) > fun_Ho1608761598t_bool ).

tff(func_def_422,type,
    hAPP_f1732083583a_bool: ( fun_fu697888865a_bool * fun_Ho1608761598t_bool ) > fun_in451447550a_bool ).

tff(func_def_423,type,
    hAPP_f1031139617_a_int: ( fun_fu907920777_a_int * fun_Ho1977546161nt_int ) > fun_fu1557526205_a_int ).

tff(func_def_424,type,
    hAPP_f1998933761ol_nat: ( fun_fu876640303ol_nat * fun_Ho1488374613nt_nat ) > fun_Ho1634634433ol_nat ).

tff(func_def_425,type,
    hAPP_f1096027413_a_nat: ( fun_fu1217459197_a_nat * fun_Ho1488374613nt_nat ) > fun_in501186901_a_nat ).

tff(func_def_426,type,
    hAPP_f1753252377_a_nat: ( fun_fu197504845_a_nat * fun_Ho1349715618t_bool ) > fun_Ho864122878_a_nat ).

tff(func_def_427,type,
    hAPP_f631038663t_bool: ( fun_fu623690153t_bool * fun_Ho1349715618t_bool ) > fun_Ho1349715618t_bool ).

tff(func_def_428,type,
    hAPP_f1040149703a_bool: ( fun_fu552225705a_bool * fun_Ho1349715618t_bool ) > fun_na1758826658a_bool ).

tff(func_def_429,type,
    hAPP_f1296292793ol_nat: ( fun_fu394467047ol_nat * fun_Ho1036508337at_nat ) > fun_Ho1345928733ol_nat ).

tff(func_def_430,type,
    hAPP_f564893909at_nat: ( fun_fu2033973437at_nat * fun_Ho1036508337at_nat ) > fun_Ho755902321at_nat ).

tff(func_def_431,type,
    hAPP_f668391445_a_nat: ( fun_fu1305006333_a_nat * fun_Ho1036508337at_nat ) > fun_na841142961_a_nat ).

tff(func_def_432,type,
    hAPP_f1659339553_a_nat: ( fun_fu84072329_a_nat * fun_Ho1036508337at_nat ) > fun_fu1923493821_a_nat ).

tff(func_def_433,type,
    hAPP_f325481667a_bool: ( fun_fu1498271147a_bool * fun_Ho1910759733l_bool ) > fun_fu1663341283a_bool ).

tff(func_def_434,type,
    hAPP_f1824299331a_bool: ( fun_fu1585255851a_bool * fun_Ho112928087a_bool ) > fun_fu1725628421a_bool ).

tff(func_def_435,type,
    hAPP_f209886133_a_nat: ( fun_fu1310697751_a_nat * fun_Ho1634634433ol_nat ) > fun_fu602188273_a_nat ).

tff(func_def_436,type,
    hAPP_f991915629_a_nat: ( fun_fu1071091151_a_nat * fun_Ho1345928733ol_nat ) > fun_fu197504845_a_nat ).

tff(func_def_437,type,
    hAPP_f1217804815_a_nat: ( fun_fu728204273_a_nat * fun_Ho1345928733ol_nat ) > fun_fu219474671_a_nat ).

tff(func_def_438,type,
    hAPP_f1112019605at_nat: ( fun_fu2109513853at_nat * fun_Ho755902321at_nat ) > fun_fu300013553at_nat ).

tff(func_def_439,type,
    hAPP_f448129468l_bool: ( fun_fu819804446l_bool * fun_int_bool ) > bool ).

tff(func_def_440,type,
    hAPP_f1594865479ol_int: ( fun_fun_int_bool_int * fun_int_bool ) > int ).

tff(func_def_441,type,
    hAPP_f957591787ol_nat: ( fun_fun_int_bool_nat * fun_int_bool ) > nat ).

tff(func_def_442,type,
    hAPP_f1805168059t_bool: ( fun_fu554825757t_bool * fun_int_bool ) > fun_int_bool ).

tff(func_def_443,type,
    hAPP_f2144054103l_bool: ( fun_fu610077323l_bool * fun_int_bool ) > fun_in531499254l_bool ).

tff(func_def_444,type,
    hAPP_f1048215610t_bool: ( fun_fu380257692t_bool * fun_int_bool ) > fun_int_fun_int_bool ).

tff(func_def_445,type,
    hAPP_f1473602334at_nat: ( fun_fu2071915986at_nat * fun_int_bool ) > fun_nat_nat ).

tff(func_def_446,type,
    hAPP_f284875647l_bool: ( fun_fu1151772339l_bool * fun_int_bool ) > fun_fu819804446l_bool ).

tff(func_def_447,type,
    hAPP_f1223193598t_bool: ( fun_fu1075512626t_bool * fun_int_bool ) > fun_fu554825757t_bool ).

tff(func_def_448,type,
    hAPP_f1634429330l_bool: ( fun_fu1284533364l_bool * fun_int_bool ) > fun_fu1151772339l_bool ).

tff(func_def_449,type,
    hAPP_f1362463689a_bool: ( fun_fu1017053431a_bool * fun_in1219646560iple_a ) > fun_in451447550a_bool ).

tff(func_def_450,type,
    hAPP_f1791153283t_bool: ( fun_fu215647537t_bool * fun_int_int ) > fun_int_fun_int_bool ).

tff(func_def_451,type,
    hAPP_f1926459811ol_int: ( fun_fu1814991441ol_int * fun_int_int ) > fun_fun_int_bool_int ).

tff(func_def_452,type,
    hAPP_f1431025877at_int: ( fun_fu1887272509at_int * fun_int_int ) > fun_fu2024564861at_int ).

tff(func_def_453,type,
    hAPP_f147134065nt_int: ( fun_fu130970841nt_int * fun_int_nat ) > fun_int_int ).

tff(func_def_454,type,
    hAPP_f2132704789nt_nat: ( fun_fu1789282941nt_nat * fun_int_nat ) > fun_int_nat ).

tff(func_def_455,type,
    hAPP_f876579787t_bool: ( fun_fu1237756537t_bool * fun_int_nat ) > fun_int_fun_nat_bool ).

tff(func_def_456,type,
    hAPP_f1463450952at_nat: ( fun_fu1420944304at_nat * fun_int_nat ) > fun_int_fun_nat_nat ).

tff(func_def_457,type,
    hAPP_f237327688nt_nat: ( fun_fu330349488nt_nat * fun_int_nat ) > fun_nat_fun_int_nat ).

tff(func_def_458,type,
    hAPP_f1109019371ol_nat: ( fun_fu670292377ol_nat * fun_int_nat ) > fun_fun_int_bool_nat ).

tff(func_def_459,type,
    hAPP_f727283836t_bool: ( fun_fu587508068t_bool * fun_in531499254l_bool ) > fun_fu554825757t_bool ).

tff(func_def_460,type,
    hAPP_f510295935t_bool: ( fun_fu713748577t_bool * fun_in451447550a_bool ) > fun_Ho1608761598t_bool ).

tff(func_def_461,type,
    hAPP_f1503898400nt_nat: ( fun_fu728395988nt_nat * fun_in451447550a_bool ) > fun_int_nat ).

tff(func_def_462,type,
    hAPP_f1500465535a_bool: ( fun_fu466270817a_bool * fun_in451447550a_bool ) > fun_in451447550a_bool ).

tff(func_def_463,type,
    hAPP_f287449365nt_nat: ( fun_fu224004093nt_nat * fun_in501186901_a_nat ) > fun_Ho1488374613nt_nat ).

tff(func_def_464,type,
    hAPP_f1914880763ol_nat: ( fun_fu2076872489ol_nat * fun_in501186901_a_nat ) > fun_in149899451ol_nat ).

tff(func_def_465,type,
    hAPP_f2119767738t_bool: ( fun_fu1221449756t_bool * fun_int_fun_int_bool ) > fun_int_bool ).

tff(func_def_466,type,
    hAPP_f1134349059nt_nat: ( fun_fu1396640951nt_nat * fun_int_fun_int_bool ) > fun_int_nat ).

tff(func_def_467,type,
    hAPP_f428220345t_bool: ( fun_fu257678363t_bool * fun_int_fun_int_bool ) > fun_int_fun_int_bool ).

tff(func_def_468,type,
    hAPP_f1468280982t_bool: ( fun_fu1881253066t_bool * fun_int_fun_int_bool ) > fun_in719570932t_bool ).

tff(func_def_469,type,
    hAPP_f1444703951t_bool: ( fun_fu405047601t_bool * fun_int_fun_int_bool ) > fun_fu1733261297t_bool ).

tff(func_def_470,type,
    hAPP_f1399575567t_bool: ( fun_fu1997740657t_bool * fun_int_fun_int_bool ) > fun_fu215647537t_bool ).

tff(func_def_471,type,
    hAPP_f879109391t_bool: ( fun_fu1576332145t_bool * fun_int_fun_int_bool ) > fun_fu1842665009t_bool ).

tff(func_def_472,type,
    hAPP_f1566620885nt_int: ( fun_fu1831640381nt_int * fun_int_fun_int_int ) > fun_fu1975973012nt_int ).

tff(func_def_473,type,
    hAPP_f909851349nt_nat: ( fun_fu214894141nt_nat * fun_int_fun_int_nat ) > fun_int_fun_int_nat ).

tff(func_def_474,type,
    hAPP_f1548925761ol_nat: ( fun_fu1243635695ol_nat * fun_int_fun_int_nat ) > fun_in1461553182ol_nat ).

tff(func_def_475,type,
    hAPP_f1161717855nt_nat: ( fun_fu1424009747nt_nat * fun_int_fun_nat_bool ) > fun_int_nat ).

tff(func_def_476,type,
    hAPP_f783004929t_bool: ( fun_fu401661795t_bool * fun_int_fun_nat_bool ) > fun_int_fun_nat_bool ).

tff(func_def_477,type,
    hAPP_f175561985t_bool: ( fun_fu1890060131t_bool * fun_int_fun_nat_bool ) > fun_nat_fun_int_bool ).

tff(func_def_478,type,
    hAPP_f1501159417ol_nat: ( fun_fu1416337063ol_nat * fun_int_fun_nat_nat ) > fun_in1172847482ol_nat ).

tff(func_def_479,type,
    hAPP_f1033905301at_nat: ( fun_fu199354621at_nat * fun_int_fun_nat_nat ) > fun_in1791225684at_nat ).

tff(func_def_480,type,
    hAPP_f879494613nt_nat: ( fun_fu652796733nt_nat * fun_int_fun_nat_nat ) > fun_nat_fun_int_nat ).

tff(func_def_481,type,
    hAPP_f1399363134nt_nat: ( fun_fu1650807462nt_nat * fun_int_fun_nat_nat ) > fun_fu1789282941nt_nat ).

tff(func_def_482,type,
    hAPP_f807099282nt_nat: ( fun_fu2087062900nt_nat * fun_in149899451ol_nat ) > fun_fu728395988nt_nat ).

tff(func_def_483,type,
    hAPP_f202917053t_bool: ( fun_fu1374874789t_bool * fun_in938817141l_bool ) > fun_fu554825757t_bool ).

tff(func_def_484,type,
    hAPP_f446447448nt_nat: ( fun_fu1989253562nt_nat * fun_in1461553182ol_nat ) > fun_fu1396640951nt_nat ).

tff(func_def_485,type,
    hAPP_f472159229t_bool: ( fun_fu407119589t_bool * fun_in719570932t_bool ) > fun_fu380257692t_bool ).

tff(func_def_486,type,
    hAPP_f369809936nt_nat: ( fun_fu776947314nt_nat * fun_in1172847482ol_nat ) > fun_fu1424009747nt_nat ).

tff(func_def_487,type,
    hAPP_f261731407nt_nat: ( fun_fu591799985nt_nat * fun_in1172847482ol_nat ) > fun_fu483878866nt_nat ).

tff(func_def_488,type,
    hAPP_f701299925at_nat: ( fun_fu1218916157at_nat * fun_in1791225684at_nat ) > fun_fu1127110484at_nat ).

tff(func_def_489,type,
    hAPP_f54304608l_bool: ( fun_fu425979586l_bool * fun_nat_bool ) > bool ).

tff(func_def_490,type,
    hAPP_f659380387ol_int: ( fun_fun_nat_bool_int * fun_nat_bool ) > int ).

tff(func_def_491,type,
    hAPP_f22106695ol_nat: ( fun_fun_nat_bool_nat * fun_nat_bool ) > nat ).

tff(func_def_492,type,
    hAPP_f1047071419_a_nat: ( fun_fu219474671_a_nat * fun_nat_bool ) > fun_Ho864122878_a_nat ).

tff(func_def_493,type,
    hAPP_f787214110nt_nat: ( fun_fu483878866nt_nat * fun_nat_bool ) > fun_int_nat ).

tff(func_def_494,type,
    hAPP_f800510211t_bool: ( fun_fu821463397t_bool * fun_nat_bool ) > fun_nat_bool ).

tff(func_def_495,type,
    hAPP_f1146629647l_bool: ( fun_fu2104074051l_bool * fun_nat_bool ) > fun_na1469252690l_bool ).

tff(func_def_496,type,
    hAPP_f1570313510t_bool: ( fun_fu429110920t_bool * fun_nat_bool ) > fun_nat_fun_nat_bool ).

tff(func_def_497,type,
    hAPP_f103356543l_bool: ( fun_fu1217155507l_bool * fun_nat_bool ) > fun_fu425979586l_bool ).

tff(func_def_498,type,
    hAPP_f1730770594t_bool: ( fun_fu915923926t_bool * fun_nat_bool ) > fun_fu821463397t_bool ).

tff(func_def_499,type,
    hAPP_f1266913334l_bool: ( fun_fu1216549656l_bool * fun_nat_bool ) > fun_fu1217155507l_bool ).

tff(func_def_500,type,
    hAPP_f1324734153a_bool: ( fun_fu1525594615a_bool * fun_na1240513468iple_a ) > fun_na1758826658a_bool ).

tff(func_def_501,type,
    hAPP_f1139079189at_int: ( fun_fu2024564861at_int * fun_nat_int ) > fun_nat_int ).

tff(func_def_502,type,
    hAPP_f1533130627t_bool: ( fun_fu1842665009t_bool * fun_nat_int ) > fun_nat_fun_int_bool ).

tff(func_def_503,type,
    hAPP_f1673907925nt_int: ( fun_fu603924029nt_int * fun_nat_int ) > fun_fu130970841nt_int ).

tff(func_def_504,type,
    hAPP_f1599440987ol_int: ( fun_fu2134752009ol_int * fun_nat_int ) > fun_fun_nat_bool_int ).

tff(func_def_505,type,
    hAPP_f1016910345at_nat: ( fun_fu300013553at_nat * fun_nat_nat ) > fun_Ho1036508337at_nat ).

tff(func_def_506,type,
    hAPP_f1169617132at_nat: ( fun_fu1127110484at_nat * fun_nat_nat ) > fun_int_fun_nat_nat ).

tff(func_def_507,type,
    hAPP_f1914919701at_nat: ( fun_fu325663101at_nat * fun_nat_nat ) > fun_nat_nat ).

tff(func_def_508,type,
    hAPP_f618557131t_bool: ( fun_fu717290361t_bool * fun_nat_nat ) > fun_nat_fun_nat_bool ).

tff(func_def_509,type,
    hAPP_f1639111240at_nat: ( fun_fu2064863920at_nat * fun_nat_nat ) > fun_nat_fun_nat_nat ).

tff(func_def_510,type,
    hAPP_f375421205_a_nat: ( fun_fu1437424253_a_nat * fun_nat_nat ) > fun_fu1923493821_a_nat ).

tff(func_def_511,type,
    hAPP_f901215189nt_nat: ( fun_fu773339453nt_nat * fun_nat_nat ) > fun_fu1789282941nt_nat ).

tff(func_def_512,type,
    hAPP_f782000547ol_nat: ( fun_fu990052945ol_nat * fun_nat_nat ) > fun_fun_nat_bool_nat ).

tff(func_def_513,type,
    hAPP_f1585078997at_nat: ( fun_fu1179887677at_nat * fun_nat_nat ) > fun_fu325663101at_nat ).

tff(func_def_514,type,
    hAPP_f561022312t_bool: ( fun_fu1901564496t_bool * fun_na1469252690l_bool ) > fun_fu821463397t_bool ).

tff(func_def_515,type,
    hAPP_f1460432071t_bool: ( fun_fu1453083561t_bool * fun_na1758826658a_bool ) > fun_Ho1349715618t_bool ).

tff(func_def_516,type,
    hAPP_f420120536at_nat: ( fun_fu546267020at_nat * fun_na1758826658a_bool ) > fun_nat_nat ).

tff(func_def_517,type,
    hAPP_f1869543111a_bool: ( fun_fu1381619113a_bool * fun_na1758826658a_bool ) > fun_na1758826658a_bool ).

tff(func_def_518,type,
    hAPP_f982543381at_nat: ( fun_fu1251828989at_nat * fun_na841142961_a_nat ) > fun_Ho1036508337at_nat ).

tff(func_def_519,type,
    hAPP_f1356625915ol_nat: ( fun_fu1428730409ol_nat * fun_na841142961_a_nat ) > fun_na228779103ol_nat ).

tff(func_def_520,type,
    hAPP_f482008321t_bool: ( fun_fu100665187t_bool * fun_nat_fun_int_bool ) > fun_int_fun_nat_bool ).

tff(func_def_521,type,
    hAPP_f389300155at_nat: ( fun_fu1553240943at_nat * fun_nat_fun_int_bool ) > fun_nat_nat ).

tff(func_def_522,type,
    hAPP_f2022049025t_bool: ( fun_fu1589063523t_bool * fun_nat_fun_int_bool ) > fun_nat_fun_int_bool ).

tff(func_def_523,type,
    hAPP_f446977493at_nat: ( fun_fu84751165at_nat * fun_nat_fun_int_nat ) > fun_int_fun_nat_nat ).

tff(func_def_524,type,
    hAPP_f299305025ol_nat: ( fun_fu1544887023ol_nat * fun_nat_fun_int_nat ) > fun_na1402637250ol_nat ).

tff(func_def_525,type,
    hAPP_f158894502t_bool: ( fun_fu531872008t_bool * fun_nat_fun_nat_bool ) > fun_nat_bool ).

tff(func_def_526,type,
    hAPP_f229349961t_bool: ( fun_fu1733046955t_bool * fun_nat_fun_nat_bool ) > fun_nat_fun_nat_bool ).

tff(func_def_527,type,
    hAPP_f10625010t_bool: ( fun_fu2023981606t_bool * fun_nat_fun_nat_bool ) > fun_na35521688t_bool ).

tff(func_def_528,type,
    hAPP_f2096737119t_bool: ( fun_fu686268865t_bool * fun_nat_fun_nat_bool ) > fun_fu1252406585t_bool ).

tff(func_def_529,type,
    hAPP_f2026117279t_bool: ( fun_fu1109211905t_bool * fun_nat_fun_nat_bool ) > fun_fu1237756537t_bool ).

tff(func_def_530,type,
    hAPP_f1505651103t_bool: ( fun_fu687803393t_bool * fun_nat_fun_nat_bool ) > fun_fu717290361t_bool ).

tff(func_def_531,type,
    hAPP_f416620757at_nat: ( fun_fu522653757at_nat * fun_nat_fun_nat_nat ) > fun_nat_fun_nat_nat ).

tff(func_def_532,type,
    hAPP_f935848405_a_nat: ( fun_fu927620157_a_nat * fun_nat_fun_nat_nat ) > fun_na1588060912_a_nat ).

tff(func_def_533,type,
    hAPP_f2080483477nt_nat: ( fun_fu1086979837nt_nat * fun_nat_fun_nat_nat ) > fun_na266550704nt_nat ).

tff(func_def_534,type,
    hAPP_f648261589at_nat: ( fun_fu1755521597at_nat * fun_nat_fun_nat_nat ) > fun_fu1300474096at_nat ).

tff(func_def_535,type,
    hAPP_f1087393429at_nat: ( fun_fu1017488637at_nat * fun_nat_fun_nat_nat ) > fun_fu1420944304at_nat ).

tff(func_def_536,type,
    hAPP_f1408247010at_nat: ( fun_fu1382375754at_nat * fun_nat_fun_nat_nat ) > fun_fu325663101at_nat ).

tff(func_def_537,type,
    hAPP_f1731313045at_nat: ( fun_fu1799328765at_nat * fun_nat_fun_nat_nat ) > fun_fu2064863920at_nat ).

tff(func_def_538,type,
    hAPP_f1173305809at_nat: ( fun_fu55165875at_nat * fun_na228779103ol_nat ) > fun_fu662538351at_nat ).

tff(func_def_539,type,
    hAPP_f1323480046at_nat: ( fun_fu1446087120at_nat * fun_na228779103ol_nat ) > fun_fu546267020at_nat ).

tff(func_def_540,type,
    hAPP_f928984021_a_nat: ( fun_fu1480131645_a_nat * fun_na1588060912_a_nat ) > fun_fu1472438000_a_nat ).

tff(func_def_541,type,
    hAPP_f630508183at_nat: ( fun_fu1373519097at_nat * fun_na1402637250ol_nat ) > fun_fu2071915986at_nat ).

tff(func_def_542,type,
    hAPP_f1750007732at_nat: ( fun_fu1081900566at_nat * fun_na1402637250ol_nat ) > fun_fu1553240943at_nat ).

tff(func_def_543,type,
    hAPP_f1633513941nt_nat: ( fun_fu1251161661nt_nat * fun_na266550704nt_nat ) > fun_fu330349488nt_nat ).

tff(func_def_544,type,
    hAPP_f1722879237t_bool: ( fun_fu80187629t_bool * fun_na1436237685l_bool ) > fun_fu821463397t_bool ).

tff(func_def_545,type,
    hAPP_f688831301t_bool: ( fun_fu1538037805t_bool * fun_na35521688t_bool ) > fun_fu429110920t_bool ).

tff(func_def_546,type,
    hAPP_f1178339559l_bool: ( fun_fu1340893257l_bool * fun_fu1658206819l_bool ) > fun_fu2118559873l_bool ).

tff(func_def_547,type,
    hAPP_f635443597e_bool: ( fun_fu817723125e_bool * fun_fu2127278875e_bool ) > fun_fu278206227e_bool ).

tff(func_def_548,type,
    hAPP_f1006724181e_bool: ( fun_fu1860059197e_bool * fun_fu1219323149e_bool ) > fun_fu1591723597e_bool ).

tff(func_def_549,type,
    hAPP_f375255701e_bool: ( fun_fu1631777789e_bool * fun_fu1047394976e_bool ) > fun_fu2008829792e_bool ).

tff(func_def_550,type,
    hAPP_f1490793353l_bool: ( fun_fu1342882871l_bool * fun_fu2026518849l_bool ) > bool ).

tff(func_def_551,type,
    hAPP_f1758315691a_bool: ( fun_fu1819779801a_bool * fun_fu2026518849l_bool ) > fun_Ho882550911a_bool ).

tff(func_def_552,type,
    hAPP_f354682389l_bool: ( fun_fu1354972029l_bool * fun_fu2026518849l_bool ) > fun_fu2026518849l_bool ).

tff(func_def_553,type,
    hAPP_f1827400025a_bool: ( fun_fu870629313a_bool * fun_fu2026518849l_bool ) > fun_fu445247621a_bool ).

tff(func_def_554,type,
    hAPP_f228445643at_nat: ( fun_fu898837677at_nat * fun_fu328701628ol_nat ) > fun_fu546267020at_nat ).

tff(func_def_555,type,
    hAPP_f967504915a_bool: ( fun_fu600978683a_bool * fun_fu1663341283a_bool ) > fun_fu466270817a_bool ).

tff(func_def_556,type,
    hAPP_f1882853211a_bool: ( fun_fu1912089667a_bool * fun_fu1663341283a_bool ) > fun_fu1381619113a_bool ).

tff(func_def_557,type,
    hAPP_f246259945l_bool: ( fun_fu1236051915l_bool * fun_fu1789210355l_bool ) > fun_fu1789210355l_bool ).

tff(func_def_558,type,
    hAPP_f86610733a_bool: ( fun_fu1595031695a_bool * fun_fu2051904533a_bool ) > fun_fu2051904533a_bool ).

tff(func_def_559,type,
    hAPP_f300022271a_bool: ( fun_fu743040865a_bool * fun_fu2051904533a_bool ) > fun_fu914297575a_bool ).

tff(func_def_560,type,
    hAPP_f534494591ol_nat: ( fun_fu1739618017ol_nat * fun_fu827349075ol_nat ) > fun_fu2076872489ol_nat ).

tff(func_def_561,type,
    hAPP_f2033836159ol_nat: ( fun_fu774707681ol_nat * fun_fu827349075ol_nat ) > fun_fu1428730409ol_nat ).

tff(func_def_562,type,
    hAPP_f215623910l_bool: ( fun_fu1540142484l_bool * fun_fu819804446l_bool ) > bool ).

tff(func_def_563,type,
    hAPP_f631471077t_bool: ( fun_fu1421432211t_bool * fun_fu819804446l_bool ) > fun_int_bool ).

tff(func_def_564,type,
    hAPP_f1948010709l_bool: ( fun_fu1070826941l_bool * fun_fu819804446l_bool ) > fun_fu819804446l_bool ).

tff(func_def_565,type,
    hAPP_f423804115t_bool: ( fun_fu1671602619t_bool * fun_fu819804446l_bool ) > fun_fu1221449756t_bool ).

tff(func_def_566,type,
    hAPP_f296893331_a_nat: ( fun_fu2017547765_a_nat * fun_fun_int_bool_nat ) > fun_fu602188273_a_nat ).

tff(func_def_567,type,
    hAPP_f2100446809nt_nat: ( fun_fu1795303867nt_nat * fun_fun_int_bool_nat ) > fun_fu1396640951nt_nat ).

tff(func_def_568,type,
    hAPP_f109563153at_nat: ( fun_fu1888474227at_nat * fun_fun_int_bool_nat ) > fun_fu1553240943at_nat ).

tff(func_def_569,type,
    hAPP_f1871962969t_bool: ( fun_fu763112513t_bool * fun_fu554825757t_bool ) > fun_fu945366625t_bool ).

tff(func_def_570,type,
    hAPP_f654702867t_bool: ( fun_fu1521371387t_bool * fun_fu554825757t_bool ) > fun_fu257678363t_bool ).

tff(func_def_571,type,
    hAPP_f1986088027t_bool: ( fun_fu788822083t_bool * fun_fu554825757t_bool ) > fun_fu1589063523t_bool ).

tff(func_def_572,type,
    hAPP_f1399552105l_bool: ( fun_fu1276998475l_bool * fun_fu1151772339l_bool ) > fun_fu1151772339l_bool ).

tff(func_def_573,type,
    hAPP_f194616807t_bool: ( fun_fu680577737t_bool * fun_fu1075512626t_bool ) > fun_fu1075512626t_bool ).

tff(func_def_574,type,
    hAPP_f1596157055t_bool: ( fun_fu873308769t_bool * fun_fu1075512626t_bool ) > fun_fu1881253066t_bool ).

tff(func_def_575,type,
    hAPP_f1772247755ol_nat: ( fun_fu651819309ol_nat * fun_fu670292377ol_nat ) > fun_fu876640303ol_nat ).

tff(func_def_576,type,
    hAPP_f1331458699ol_nat: ( fun_fu657063149ol_nat * fun_fu670292377ol_nat ) > fun_fu1243635695ol_nat ).

tff(func_def_577,type,
    hAPP_f1632710027ol_nat: ( fun_fu342964205ol_nat * fun_fu670292377ol_nat ) > fun_fu1544887023ol_nat ).

tff(func_def_578,type,
    hAPP_f1637334154l_bool: ( fun_fu814369080l_bool * fun_fu425979586l_bool ) > bool ).

tff(func_def_579,type,
    hAPP_f582319405t_bool: ( fun_fu496092379t_bool * fun_fu425979586l_bool ) > fun_nat_bool ).

tff(func_def_580,type,
    hAPP_f1246832597l_bool: ( fun_fu616551101l_bool * fun_fu425979586l_bool ) > fun_fu425979586l_bool ).

tff(func_def_581,type,
    hAPP_f1777703707t_bool: ( fun_fu1402718723t_bool * fun_fu425979586l_bool ) > fun_fu531872008t_bool ).

tff(func_def_582,type,
    hAPP_f456064075_a_nat: ( fun_fu1155082413_a_nat * fun_fun_nat_bool_nat ) > fun_fu197504845_a_nat ).

tff(func_def_583,type,
    hAPP_f1964560145nt_nat: ( fun_fu523748467nt_nat * fun_fun_nat_bool_nat ) > fun_fu1424009747nt_nat ).

tff(func_def_584,type,
    hAPP_f69420889t_bool: ( fun_fu2137156673t_bool * fun_fu821463397t_bool ) > fun_fu623690153t_bool ).

tff(func_def_585,type,
    hAPP_f1410409747t_bool: ( fun_fu719081723t_bool * fun_fu821463397t_bool ) > fun_fu401661795t_bool ).

tff(func_def_586,type,
    hAPP_f643944041l_bool: ( fun_fu820922699l_bool * fun_fu1217155507l_bool ) > fun_fu1217155507l_bool ).

tff(func_def_587,type,
    hAPP_f1311642927t_bool: ( fun_fu257437713t_bool * fun_fu915923926t_bool ) > fun_fu915923926t_bool ).

tff(func_def_588,type,
    hAPP_f1115950719t_bool: ( fun_fu1738364513t_bool * fun_fu915923926t_bool ) > fun_fu2023981606t_bool ).

tff(func_def_589,type,
    hAPP_f450378965_a_nat: ( fun_fu687095869_a_nat * fun_fu1437424253_a_nat ) > fun_fu927620157_a_nat ).

tff(func_def_590,type,
    hAPP_f1701814485nt_nat: ( fun_fu504533053nt_nat * fun_fu773339453nt_nat ) > fun_fu1086979837nt_nat ).

tff(func_def_591,type,
    hAPP_f153943611ol_nat: ( fun_fu1838203037ol_nat * fun_fu990052945ol_nat ) > fun_fu394467047ol_nat ).

tff(func_def_592,type,
    hAPP_f1029311995ol_nat: ( fun_fu294108253ol_nat * fun_fu990052945ol_nat ) > fun_fu1416337063ol_nat ).

tff(func_def_593,type,
    hAPP_f250842005at_nat: ( fun_fu477648637at_nat * fun_fu1179887677at_nat ) > fun_fu2033973437at_nat ).

tff(func_def_594,type,
    hAPP_f1315855317at_nat: ( fun_fu633097021at_nat * fun_fu1179887677at_nat ) > fun_fu199354621at_nat ).

tff(func_def_595,type,
    member276146780iple_a: fun_Ho1910759733l_bool ).

tff(func_def_596,type,
    member_int: fun_in938817141l_bool ).

tff(func_def_597,type,
    member_nat: fun_na1436237685l_bool ).

tff(func_def_598,type,
    g: fun_Ho882550911a_bool ).

tff(func_def_599,type,
    p: fun_a_fun_state_bool ).

tff(func_def_600,type,
    b: fun_state_bool ).

tff(func_def_601,type,
    c: com ).

tff(func_def_602,type,
    sK0: ( fun_Ho882550911a_bool * com * fun_a_fun_state_bool * fun_a_fun_state_bool ) > x_a ).

tff(func_def_603,type,
    sK1: ( fun_Ho882550911a_bool * com * fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).

tff(func_def_604,type,
    sK2: hoare_2076525193iple_a > fun_a_fun_state_bool ).

tff(func_def_605,type,
    sK3: hoare_2076525193iple_a > com ).

tff(func_def_606,type,
    sK4: hoare_2076525193iple_a > fun_a_fun_state_bool ).

tff(func_def_607,type,
    sK5: fun_Ho882550911a_bool > hoare_2076525193iple_a ).

tff(func_def_608,type,
    sK6: fun_Ho882550911a_bool > fun_Ho882550911a_bool ).

tff(func_def_609,type,
    sK7: fun_Ho882550911a_bool > hoare_2076525193iple_a ).

tff(func_def_610,type,
    sK8: fun_Ho882550911a_bool > hoare_2076525193iple_a ).

tff(func_def_611,type,
    sK9: fun_Ho882550911a_bool > hoare_2076525193iple_a ).

tff(pred_def_1,type,
    hBOOL: bool > $o ).

tff(f6,axiom,
    ! [X0: fun_Ho882550911a_bool,X1: com,X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool] :
      ( ! [X4: x_a,X5: state] :
          ( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5))
         => hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo214064617a_bool))) )
     => hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(X3,X1,X2)),bot_bo214064617a_bool))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_escape) ).

tff(f1207,axiom,
    ~ hBOOL(fFalse),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).

tff(f1229,axiom,
    ! [X0: bool,X1: state] : ( hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) ).

tff(f1252,axiom,
    ! [X0: fun_state_bool,X1: x_a] : ( hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) ).

tff(f1364,conjecture,
    hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(g),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo214064617a_bool))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

tff(f1365,negated_conjecture,
    ~ hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(g),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo214064617a_bool))),
    inference(negated_conjecture,[status(cth)],[f1364]) ).

tff(f1366,plain,
    ~ hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(g),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo214064617a_bool))),
    inference(flattening,[],[f1365]) ).

tff(f1368,plain,
    ! [X0: fun_Ho882550911a_bool,X1: com,X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool] :
      ( hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(X3,X1,X2)),bot_bo214064617a_bool)))
      | ? [X4: x_a,X5: state] :
          ( ~ hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo214064617a_bool)))
          & hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5)) ) ),
    inference(ennf_transformation,[],[f6]) ).

tff(f1381,plain,
    ! [X0: fun_Ho882550911a_bool,X1: com,X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool] :
      ( hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(X3,X1,X2)),bot_bo214064617a_bool)))
      | ( ~ hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),sK1(X0,X1,X2,X3))),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,sK0(X0,X1,X2,X3))))),bot_bo214064617a_bool)))
        & hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3))) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X4,sK0(X0,X1,X2,X3)),skolemize(X5,sK1(X0,X1,X2,X3))],[f1368]) ).

tff(f1398,plain,
    ~ hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(g),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo214064617a_bool))),
    inference(cnf_transformation,[],[f1366]) ).

tff(f1406,plain,
    ! [X0: bool,X1: state] : ( hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
    inference(cnf_transformation,[],[f1229]) ).

tff(f1407,plain,
    ! [X0: fun_state_bool,X1: x_a] : ( hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0 ),
    inference(cnf_transformation,[],[f1252]) ).

tff(f1408,plain,
    ! [X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool,X0: fun_Ho882550911a_bool,X1: com] :
      ( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3)))
      | hBOOL(hAPP_f500854239l_bool(hoare_572465367rivs_a(X0),hAPP_f642208769a_bool(hAPP_H1940471919a_bool(insert1582918915iple_a,hoare_1876769875iple_a(X3,X1,X2)),bot_bo214064617a_bool))) ),
    inference(cnf_transformation,[],[f1381]) ).

tff(f1449,plain,
    ~ hBOOL(fFalse),
    inference(cnf_transformation,[],[f1207]) ).

tff(f2569,plain,
    hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),sK0(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)))),sK1(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse))))),
    inference(unit_resulting_resolution,[],[f1408,f1398]) ).

tff(f2583,plain,
    hBOOL(hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),sK1(g,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse))))),
    inference(forward_demodulation,[],[f2569,f1407]) ).

tff(f2584,plain,
    hBOOL(fFalse),
    inference(forward_demodulation,[],[f2583,f1406]) ).

tff(f2585,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f2584,f1449]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWW470_3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18  % Computer : n002.cluster.edu
% 0.08/0.18  % Model    : x86_64 x86_64
% 0.08/0.18  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18  % Memory   : 8046.5625MB
% 0.08/0.18  % OS       : Linux 6.8.0-71-generic
% 0.08/0.18  % CPULimit : 300
% 0.08/0.18  % WCLimit  : 300
% 0.08/0.18  % DateTime : Mon Sep 28 14:05:22 UTC 2026
% 0.08/0.18  % CPUTime  : 
% 0.08/0.18  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22  Running first-order theorem proving
% 0.08/0.22  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.22/1.39  % (363391)Detected formulas, will run a generic FOF schedule.
% 4.22/1.39  % (363396)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=691368399:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.22/1.39  % (363401)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1360159063:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.22/1.39  % (363399)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1811910573:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.22/1.39  % (363400)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2607849817:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.22/1.39  % (363397)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2089941623:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.22/1.39  % (363398)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=663664055:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.22/1.39  % (363402)dis-21_1_sil=8000:lcm=predicate:random_seed=389961613:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.22/1.39  % (363399)Refutation not found, incomplete strategy
% 4.22/1.39  % (363399)------------------------------
% 4.22/1.39  % (363399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363399)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363399)Termination reason: Refutation not found, incomplete strategy
% 4.22/1.39  % (363399)Time elapsed: 0.009 s
% 4.22/1.39  % (363399)Peak memory usage: 90 MB
% 4.22/1.39  % (363399)Instructions burned: 13 (million)
% 4.22/1.39  % (363402)Instruction limit reached! 
% 4.22/1.39  % (363402)------------------------------
% 4.22/1.39  % (363402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363402)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363402)Termination reason: Instruction limit
% 4.22/1.39  % (363402)Termination phase: Property scanning
% 4.22/1.39  % (363402)Time elapsed: 0.057 s
% 4.22/1.39  % (363402)Peak memory usage: 89 MB
% 4.22/1.39  % (363402)Instructions burned: 130 (million)
% 4.22/1.39  % (363401)Instruction limit reached! 
% 4.22/1.39  % (363401)------------------------------
% 4.22/1.39  % (363401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363401)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363401)Termination reason: Instruction limit
% 4.22/1.39  % (363401)Termination phase: Property scanning
% 4.22/1.39  % (363401)Time elapsed: 0.061 s
% 4.22/1.39  % (363401)Peak memory usage: 89 MB
% 4.22/1.39  % (363401)Instructions burned: 140 (million)
% 4.22/1.39  % (363400)Instruction limit reached! 
% 4.22/1.39  % (363400)------------------------------
% 4.22/1.39  % (363400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363400)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363400)Termination reason: Instruction limit
% 4.22/1.39  % (363400)Termination phase: Saturation
% 4.22/1.39  % (363400)Time elapsed: 0.066 s
% 4.22/1.39  % (363400)Peak memory usage: 90 MB
% 4.22/1.39  % (363400)Instructions burned: 120 (million)
% 4.22/1.39  % (363411)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1574555795:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 4.22/1.39  % (363410)lrs+10_1_sil=8000:sp=occurrence:random_seed=1722381289:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.22/1.39  % (363412)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3410960087:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 4.22/1.39  % (363411)First to succeed.
% 4.22/1.39  % (363411)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-363391"
% 4.22/1.39  % (363399)------------------------------
% 4.22/1.39  % (363399)------------------------------
% 4.22/1.39  % (363410)Instruction limit reached! 
% 4.22/1.39  % (363410)------------------------------
% 4.22/1.39  % (363410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363410)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363410)Termination reason: Instruction limit
% 4.22/1.39  % (363410)Termination phase: Saturation
% 4.22/1.39  % (363410)Time elapsed: 0.150 s
% 4.22/1.39  % (363410)Peak memory usage: 91 MB
% 4.22/1.39  % (363410)Instructions burned: 287 (million)
% 4.22/1.39  % (363416)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=33023366:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.22/1.39  % (363412)Instruction limit reached! 
% 4.22/1.39  % (363412)------------------------------
% 4.22/1.39  % (363412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.39  % (363412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.39  % (363412)CaDiCaL version: 2.1.3
% 4.22/1.39  % (363412)Termination reason: Instruction limit
% 4.22/1.39  % (363412)Termination phase: Saturation
% 4.22/1.39  % (363412)Time elapsed: 0.196 s
% 4.22/1.39  % (363412)Peak memory usage: 92 MB
% 4.22/1.39  % (363412)Instructions burned: 325 (million)
% 4.22/1.39  % (363416)Also succeeded, but the first one will report.
% 4.22/1.39  % (363411)Refutation found. Thanks to Tanya!
% 4.22/1.39  % SZS status Theorem for theBenchmark
% 4.22/1.39  % SZS output start Proof for theBenchmark
% See solution above
% 5.18/1.59  % (363411)------------------------------
% 5.18/1.59  % (363411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.59  % (363411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.59  % (363411)CaDiCaL version: 2.1.3
% 5.18/1.59  % (363411)Termination reason: Refutation
% 5.18/1.59  % (363411)Time elapsed: 0.053 s
% 5.18/1.59  % (363411)Peak memory usage: 91 MB
% 5.18/1.59  % (363411)Instructions burned: 92 (million)
% 5.18/1.59  % (363411)------------------------------
% 5.18/1.59  % (363411)------------------------------
% 5.18/1.59  % (363391)Success in time 0.727 s
% 5.18/1.59  % Vampire exiting
%------------------------------------------------------------------------------