%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW478^3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:23 AM UTC 2026
% Result : Theorem 2.22s 0.73s
% Output : Refutation 2.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 2
% Syntax : Number of formulae : 11 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 31 ( 5 equ; 0 cnn)
% Maximal formula atoms : 2 ( 2 avg)
% Number of connectives : 175 ( 5 ~; 0 |; 0 &; 170 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Number of types : 67 ( 66 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 1311 (1308 usr; 25 con; 0-9 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
bop: $tType ).
thf(type_def_6,type,
exp_list_char: $tType ).
thf(type_def_7,type,
list_exp_list_char: $tType ).
thf(type_def_8,type,
list_list_char: $tType ).
thf(type_def_9,type,
list_option_ty: $tType ).
thf(type_def_10,type,
list_char: $tType ).
thf(type_def_11,type,
list_ty: $tType ).
thf(type_def_12,type,
list_val: $tType ).
thf(type_def_13,type,
list_P1940453997har_ty: $tType ).
thf(type_def_14,type,
list_P1999446415t_char: $tType ).
thf(type_def_15,type,
list_P341299826t_char: $tType ).
thf(type_def_16,type,
list_P2023964830har_ty: $tType ).
thf(type_def_17,type,
nat: $tType ).
thf(type_def_18,type,
option_list_char_o: $tType ).
thf(type_def_19,type,
option_nat: $tType ).
thf(type_def_20,type,
option_ty: $tType ).
thf(type_def_21,type,
option_val: $tType ).
thf(type_def_22,type,
option1728594148on_val: $tType ).
thf(type_def_23,type,
ty: $tType ).
thf(type_def_24,type,
val: $tType ).
thf(type_def_25,type,
produc774316953on_val: $tType ).
thf(type_def_26,type,
produc2090907612on_val: $tType ).
thf(type_def_27,type,
produc1287081631on_val: $tType ).
thf(type_def_28,type,
produc688860215on_val: $tType ).
thf(type_def_29,type,
product_prod_bop_bop: $tType ).
thf(type_def_30,type,
produc1645268488al_val: $tType ).
thf(type_def_31,type,
produc2048519645t_char: $tType ).
thf(type_def_32,type,
produc1282892786on_val: $tType ).
thf(type_def_33,type,
produc91527719t_char: $tType ).
thf(type_def_34,type,
produc1180562163on_val: $tType ).
thf(type_def_35,type,
produc809539159t_char: $tType ).
thf(type_def_36,type,
produc1200003175t_char: $tType ).
thf(type_def_37,type,
produc1285161482t_char: $tType ).
thf(type_def_38,type,
produc2088785539on_val: $tType ).
thf(type_def_39,type,
produc1278157519t_char: $tType ).
thf(type_def_40,type,
produc917948472har_ty: $tType ).
thf(type_def_41,type,
produc1971331930t_char: $tType ).
thf(type_def_42,type,
produc1013743697t_char: $tType ).
thf(type_def_43,type,
produc952412819t_char: $tType ).
thf(type_def_44,type,
produc1420746395ist_ty: $tType ).
thf(type_def_45,type,
produc220283002t_char: $tType ).
thf(type_def_46,type,
produc1025221954t_char: $tType ).
thf(type_def_47,type,
produc662261637t_char: $tType ).
thf(type_def_48,type,
produc753553453st_val: $tType ).
thf(type_def_49,type,
produc450000425har_ty: $tType ).
thf(type_def_50,type,
produc2146869324t_char: $tType ).
thf(type_def_51,type,
produc244676007t_char: $tType ).
thf(type_def_52,type,
produc1059328077t_char: $tType ).
thf(type_def_53,type,
product_prod_val_val: $tType ).
thf(type_def_54,type,
produc1581780743on_val: $tType ).
thf(type_def_55,type,
produc630464863al_val: $tType ).
thf(type_def_56,type,
produc1746408499on_val: $tType ).
thf(type_def_57,type,
produc618524391on_val: $tType ).
thf(type_def_58,type,
produc1534059751t_char: $tType ).
thf(type_def_59,type,
produc349695911t_char: $tType ).
thf(type_def_60,type,
produc1368416213on_val: $tType ).
thf(type_def_61,type,
produc245756905har_ty: $tType ).
thf(type_def_62,type,
produc1350825965t_char: $tType ).
thf(type_def_63,type,
produc84451751t_char: $tType ).
thf(type_def_64,type,
produc740765671t_char: $tType ).
thf(type_def_65,type,
produc1406897475t_char: $tType ).
thf(type_def_66,type,
produc1826280281t_char: $tType ).
thf(type_def_67,type,
produc494726439t_char: $tType ).
thf(type_def_68,type,
produc800118557al_val: $tType ).
thf(type_def_69,type,
produc652964533on_val: $tType ).
thf(type_def_70,type,
produc1250491293on_val: $tType ).
thf(type_def_71,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
eval: list_P1999446415t_char > exp_list_char > produc2090907612on_val > exp_list_char > produc2090907612on_val > $o ).
thf(func_def_1,type,
evals: list_P1999446415t_char > list_exp_list_char > produc2090907612on_val > list_exp_list_char > produc2090907612on_val > $o ).
thf(func_def_2,type,
final_list_char: exp_list_char > $o ).
thf(func_def_3,type,
finals_list_char: list_exp_list_char > $o ).
thf(func_def_4,type,
conf_P373316194t_char: list_P1999446415t_char > ( nat > option1728594148on_val ) > val > ty > $o ).
thf(func_def_5,type,
hconf_97414254t_char: list_P1999446415t_char > ( nat > option1728594148on_val ) > $o ).
thf(func_def_6,type,
lconf_496643946t_char: list_P1999446415t_char > ( nat > option1728594148on_val ) > ( list_char > option_val ) > ( list_char > option_ty ) > $o ).
thf(func_def_7,type,
oconf_1869808039t_char: list_P1999446415t_char > ( nat > option1728594148on_val ) > produc2088785539on_val > $o ).
thf(func_def_8,type,
is_cla570604648t_char: list_P1999446415t_char > list_char > $o ).
thf(func_def_9,type,
d_list_char: exp_list_char > option_list_char_o > $o ).
thf(func_def_10,type,
classCast: list_char ).
thf(func_def_11,type,
nullPointer: list_char ).
thf(func_def_12,type,
outOfMemory: list_char ).
thf(func_def_13,type,
addr_of_sys_xcpt: list_char > nat ).
thf(func_def_14,type,
preallocated: ( nat > option1728594148on_val ) > $o ).
thf(func_def_15,type,
sys_xcpts: list_char > $o ).
thf(func_def_16,type,
binop: produc1645268488al_val > option_val ).
thf(func_def_17,type,
add: bop ).
thf(func_def_18,type,
c_Expr_Obop_OEq: bop ).
thf(func_def_19,type,
binOp_list_char: exp_list_char > bop > exp_list_char > exp_list_char ).
thf(func_def_20,type,
block_list_char: list_char > ty > exp_list_char > exp_list_char ).
thf(func_def_21,type,
call_list_char: exp_list_char > list_char > list_exp_list_char > exp_list_char ).
thf(func_def_22,type,
cast_list_char: list_char > exp_list_char > exp_list_char ).
thf(func_def_23,type,
cond_list_char: exp_list_char > exp_list_char > exp_list_char > exp_list_char ).
thf(func_def_24,type,
fAcc_list_char: exp_list_char > list_char > list_char > exp_list_char ).
thf(func_def_25,type,
fAss_list_char: exp_list_char > list_char > list_char > exp_list_char > exp_list_char ).
thf(func_def_26,type,
lAss_list_char: list_char > exp_list_char > exp_list_char ).
thf(func_def_27,type,
seq_list_char: exp_list_char > exp_list_char > exp_list_char ).
thf(func_def_28,type,
tryCatch_list_char: exp_list_char > list_char > list_char > exp_list_char > exp_list_char ).
thf(func_def_29,type,
val_list_char: val > exp_list_char ).
thf(func_def_30,type,
while_list_char: exp_list_char > exp_list_char > exp_list_char ).
thf(func_def_31,type,
new_list_char: list_char > exp_list_char ).
thf(func_def_32,type,
throw_list_char: exp_list_char > exp_list_char ).
thf(func_def_33,type,
fv: exp_list_char > list_char > $o ).
thf(func_def_34,type,
fvs: list_exp_list_char > list_char > $o ).
thf(func_def_35,type,
comp_o1129292306t_char: ( option_val > val ) > ( list_char > option_val ) > list_char > val ).
thf(func_def_36,type,
fun_up424764369ion_ty: ( list_char > option_ty ) > list_char > option_ty > list_char > option_ty ).
thf(func_def_37,type,
fun_up1149430426on_val: ( list_char > option_val ) > list_char > option_val > list_char > option_val ).
thf(func_def_38,type,
fun_up1472480727on_val: ( nat > option1728594148on_val ) > nat > option1728594148on_val > nat > option1728594148on_val ).
thf(func_def_39,type,
fun_up204312361on_val: ( produc1278157519t_char > option_val ) > produc1278157519t_char > option_val > produc1278157519t_char > option_val ).
thf(func_def_40,type,
overri2012515291on_val: ( list_char > option_val ) > ( list_char > option_val ) > ( list_char > $o ) > list_char > option_val ).
thf(func_def_41,type,
wf_J_mdecl: list_P1999446415t_char > list_char > produc1013743697t_char > $o ).
thf(func_def_42,type,
semila2134664963char_o: ( list_char > $o ) > ( list_char > $o ) > list_char > $o ).
thf(func_def_43,type,
semila848761471_nat_o: ( nat > $o ) > ( nat > $o ) > nat > $o ).
thf(func_def_44,type,
semila880700084char_o: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > produc1278157519t_char > $o ).
thf(func_def_45,type,
semila690474031char_o: ( produc1971331930t_char > $o ) > ( produc1971331930t_char > $o ) > produc1971331930t_char > $o ).
thf(func_def_46,type,
semila1228900530char_o: ( produc1013743697t_char > $o ) > ( produc1013743697t_char > $o ) > produc1013743697t_char > $o ).
thf(func_def_47,type,
semila1505903696_val_o: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > produc1746408499on_val > $o ).
thf(func_def_48,type,
semila1566912796_val_o: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > produc618524391on_val > $o ).
thf(func_def_49,type,
append_exp_list_char: list_exp_list_char > list_exp_list_char > list_exp_list_char ).
thf(func_def_50,type,
distinct_list_char: list_list_char > $o ).
thf(func_def_51,type,
cons_exp_list_char: exp_list_char > list_exp_list_char > list_exp_list_char ).
thf(func_def_52,type,
cons_list_char: list_char > list_list_char > list_list_char ).
thf(func_def_53,type,
cons_ty: ty > list_ty > list_ty ).
thf(func_def_54,type,
cons_val: val > list_val > list_val ).
thf(func_def_55,type,
list_all2_ty_ty: ( ty > ty > $o ) > list_ty > list_ty > $o ).
thf(func_def_56,type,
map_list_char_val: ( list_char > val ) > list_list_char > list_val ).
thf(func_def_57,type,
map_ty_option_ty: ( ty > option_ty ) > list_ty > list_option_ty ).
thf(func_def_58,type,
map_va1934808527t_char: ( val > exp_list_char ) > list_val > list_exp_list_char ).
thf(func_def_59,type,
map_val_option_ty: ( val > option_ty ) > list_val > list_option_ty ).
thf(func_def_60,type,
set_list_char: list_list_char > list_char > $o ).
thf(func_def_61,type,
set_Pr1494163115t_char: list_P1999446415t_char > produc1971331930t_char > $o ).
thf(func_def_62,type,
set_Pr2033386304t_char: list_P341299826t_char > produc1013743697t_char > $o ).
thf(func_def_63,type,
dom_list_char_ty: ( list_char > option_ty ) > list_char > $o ).
thf(func_def_64,type,
dom_list_char_val: ( list_char > option_val ) > list_char > $o ).
thf(func_def_65,type,
dom_na2045926843on_val: ( nat > option1728594148on_val ) > nat > $o ).
thf(func_def_66,type,
dom_Pr695701035ar_val: ( produc1278157519t_char > option_val ) > produc1278157519t_char > $o ).
thf(func_def_67,type,
map_add_list_char_ty: ( list_char > option_ty ) > ( list_char > option_ty ) > list_char > option_ty ).
thf(func_def_68,type,
map_ad325961431ar_val: ( list_char > option_val ) > ( list_char > option_val ) > list_char > option_val ).
thf(func_def_69,type,
map_ad1851375512on_val: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > nat > option1728594148on_val ).
thf(func_def_70,type,
map_ad1185064968ar_val: ( produc1278157519t_char > option_val ) > ( produc1278157519t_char > option_val ) > produc1278157519t_char > option_val ).
thf(func_def_71,type,
map_up891053837har_ty: ( list_char > option_ty ) > list_list_char > list_ty > list_char > option_ty ).
thf(func_def_72,type,
map_up1085636310ar_val: ( list_char > option_val ) > list_list_char > list_val > list_char > option_val ).
thf(func_def_73,type,
restri761823004ar_val: ( list_char > option_val ) > ( list_char > $o ) > list_char > option_val ).
thf(func_def_74,type,
size_s1143674878t_char: list_exp_list_char > nat ).
thf(func_def_75,type,
size_s2113983095t_char: list_list_char > nat ).
thf(func_def_76,type,
size_size_list_ty: list_ty > nat ).
thf(func_def_77,type,
size_size_list_val: list_val > nat ).
thf(func_def_78,type,
hext: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > $o ).
thf(func_def_79,type,
init_fields: list_P2023964830har_ty > produc1278157519t_char > option_val ).
thf(func_def_80,type,
new_Addr: ( nat > option1728594148on_val ) > option_nat ).
thf(func_def_81,type,
typeof_h: ( nat > option1728594148on_val ) > val > option_ty ).
thf(func_def_82,type,
none_list_char_o: option_list_char_o ).
thf(func_def_83,type,
none_nat: option_nat ).
thf(func_def_84,type,
none_ty: option_ty ).
thf(func_def_85,type,
none_val: option_val ).
thf(func_def_86,type,
none_P1260844216on_val: option1728594148on_val ).
thf(func_def_87,type,
some_list_char_o: ( list_char > $o ) > option_list_char_o ).
thf(func_def_88,type,
some_nat: nat > option_nat ).
thf(func_def_89,type,
some_ty: ty > option_ty ).
thf(func_def_90,type,
some_val: val > option_val ).
thf(func_def_91,type,
some_P451527732on_val: produc2088785539on_val > option1728594148on_val ).
thf(func_def_92,type,
option857204770on_val: option_ty > ( produc2088785539on_val > option_ty ) > option1728594148on_val > option_ty ).
thf(func_def_93,type,
the_list_char_o: option_list_char_o > list_char > $o ).
thf(func_def_94,type,
the_nat: option_nat > nat ).
thf(func_def_95,type,
the_ty: option_ty > ty ).
thf(func_def_96,type,
the_val: option_val > val ).
thf(func_def_97,type,
the_Pr1885945130on_val: option1728594148on_val > produc2088785539on_val ).
thf(func_def_98,type,
ord_le1145603820_val_o: ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > $o ).
thf(func_def_99,type,
ord_le1352079040_val_o: ( bop > product_prod_val_val > $o ) > ( bop > product_prod_val_val > $o ) > $o ).
thf(func_def_100,type,
ord_le1792911318_val_o: ( exp_list_char > produc2090907612on_val > $o ) > ( exp_list_char > produc2090907612on_val > $o ) > $o ).
thf(func_def_101,type,
ord_le636719503_val_o: ( list_exp_list_char > produc2090907612on_val > $o ) > ( list_exp_list_char > produc2090907612on_val > $o ) > $o ).
thf(func_def_102,type,
ord_le84164651char_o: ( list_list_char > exp_list_char > $o ) > ( list_list_char > exp_list_char > $o ) > $o ).
thf(func_def_103,type,
ord_le424140984char_o: ( list_list_char > produc220283002t_char > $o ) > ( list_list_char > produc220283002t_char > $o ) > $o ).
thf(func_def_104,type,
ord_le1726974981_val_o: ( list_char > ( produc1278157519t_char > option_val ) > $o ) > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > $o ).
thf(func_def_105,type,
ord_le237460153char_o: ( list_char > list_char > $o ) > ( list_char > list_char > $o ) > $o ).
thf(func_def_106,type,
ord_le1501926550char_o: ( list_char > produc952412819t_char > $o ) > ( list_char > produc952412819t_char > $o ) > $o ).
thf(func_def_107,type,
ord_le694689975char_o: ( list_char > produc1025221954t_char > $o ) > ( list_char > produc1025221954t_char > $o ) > $o ).
thf(func_def_108,type,
ord_le1073847069char_o: ( list_char > produc2146869324t_char > $o ) > ( list_char > produc2146869324t_char > $o ) > $o ).
thf(func_def_109,type,
ord_le1777678169char_o: ( list_char > $o ) > ( list_char > $o ) > $o ).
thf(func_def_110,type,
ord_le1975270990char_o: ( list_ty > produc662261637t_char > $o ) > ( list_ty > produc662261637t_char > $o ) > $o ).
thf(func_def_111,type,
ord_le1480834691char_o: ( list_val > exp_list_char > $o ) > ( list_val > exp_list_char > $o ) > $o ).
thf(func_def_112,type,
ord_le1015080996char_o: ( list_P1940453997har_ty > list_P341299826t_char > $o ) > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > $o ).
thf(func_def_113,type,
ord_less_eq_nat_o: ( nat > $o ) > ( nat > $o ) > $o ).
thf(func_def_114,type,
ord_le946822159_val_o: ( val > val > $o ) > ( val > val > $o ) > $o ).
thf(func_def_115,type,
ord_le290925629_val_o: ( produc2090907612on_val > $o ) > ( produc2090907612on_val > $o ) > $o ).
thf(func_def_116,type,
ord_le1019536145_val_o: ( produc1645268488al_val > $o ) > ( produc1645268488al_val > $o ) > $o ).
thf(func_def_117,type,
ord_le166837589_val_o: ( produc1282892786on_val > produc1282892786on_val > $o ) > ( produc1282892786on_val > produc1282892786on_val > $o ) > $o ).
thf(func_def_118,type,
ord_le900129703_val_o: ( produc1282892786on_val > $o ) > ( produc1282892786on_val > $o ) > $o ).
thf(func_def_119,type,
ord_le1294853199_val_o: ( produc1180562163on_val > produc1180562163on_val > $o ) > ( produc1180562163on_val > produc1180562163on_val > $o ) > $o ).
thf(func_def_120,type,
ord_le941641472_val_o: ( produc1180562163on_val > $o ) > ( produc1180562163on_val > $o ) > $o ).
thf(func_def_121,type,
ord_le1754369948char_o: ( produc809539159t_char > $o ) > ( produc809539159t_char > $o ) > $o ).
thf(func_def_122,type,
ord_le1356274601char_o: ( produc1285161482t_char > $o ) > ( produc1285161482t_char > $o ) > $o ).
thf(func_def_123,type,
ord_le719203798_val_o: ( produc2088785539on_val > $o ) > ( produc2088785539on_val > $o ) > $o ).
thf(func_def_124,type,
ord_le7825418char_o: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > $o ).
thf(func_def_125,type,
ord_le139275609char_o: ( produc1971331930t_char > $o ) > ( produc1971331930t_char > $o ) > $o ).
thf(func_def_126,type,
ord_le1156912648char_o: ( produc1013743697t_char > $o ) > ( produc1013743697t_char > $o ) > $o ).
thf(func_def_127,type,
ord_le1844608096char_o: ( produc952412819t_char > $o ) > ( produc952412819t_char > $o ) > $o ).
thf(func_def_128,type,
ord_le1234751263char_o: ( produc220283002t_char > $o ) > ( produc220283002t_char > $o ) > $o ).
thf(func_def_129,type,
ord_le1298648532char_o: ( produc662261637t_char > $o ) > ( produc662261637t_char > $o ) > $o ).
thf(func_def_130,type,
ord_le2021326055char_o: ( produc2146869324t_char > $o ) > ( produc2146869324t_char > $o ) > $o ).
thf(func_def_131,type,
ord_le1101577138_val_o: ( product_prod_val_val > $o ) > ( product_prod_val_val > $o ) > $o ).
thf(func_def_132,type,
ord_le1364969894_val_o: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > $o ).
thf(func_def_133,type,
ord_le559588722_val_o: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > $o ).
thf(func_def_134,type,
ord_less_eq_o: $o > $o > $o ).
thf(func_def_135,type,
produc1338265359on_val: ( list_char > option_val ) > ( list_char > option_val ) > produc774316953on_val ).
thf(func_def_136,type,
produc755559506on_val: ( nat > option1728594148on_val ) > ( list_char > option_val ) > produc2090907612on_val ).
thf(func_def_137,type,
produc1208913941on_val: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > produc1287081631on_val ).
thf(func_def_138,type,
produc253229997on_val: ( produc1278157519t_char > option_val ) > ( produc1278157519t_char > option_val ) > produc688860215on_val ).
thf(func_def_139,type,
product_Pair_bop_bop: bop > bop > product_prod_bop_bop ).
thf(func_def_140,type,
produc621191550al_val: bop > product_prod_val_val > produc1645268488al_val ).
thf(func_def_141,type,
produc943465171t_char: exp_list_char > exp_list_char > produc2048519645t_char ).
thf(func_def_142,type,
produc235638504on_val: exp_list_char > produc2090907612on_val > produc1282892786on_val ).
thf(func_def_143,type,
produc1237966615t_char: list_exp_list_char > list_exp_list_char > produc91527719t_char ).
thf(func_def_144,type,
produc1302104557on_val: list_exp_list_char > produc2090907612on_val > produc1180562163on_val ).
thf(func_def_145,type,
produc1147572817t_char: list_list_char > exp_list_char > produc809539159t_char ).
thf(func_def_146,type,
produc2035944023t_char: list_list_char > list_list_char > produc1200003175t_char ).
thf(func_def_147,type,
produc921874948t_char: list_list_char > produc220283002t_char > produc1285161482t_char ).
thf(func_def_148,type,
produc926070009on_val: list_char > ( produc1278157519t_char > option_val ) > produc2088785539on_val ).
thf(func_def_149,type,
produc5062597t_char: list_char > list_char > produc1278157519t_char ).
thf(func_def_150,type,
produc251930284har_ty: list_char > ty > produc917948472har_ty ).
thf(func_def_151,type,
produc822965838t_char: list_char > produc952412819t_char > produc1971331930t_char ).
thf(func_def_152,type,
produc1331140167t_char: list_char > produc1025221954t_char > produc1013743697t_char ).
thf(func_def_153,type,
produc1483578759t_char: list_char > produc2146869324t_char > produc952412819t_char ).
thf(func_def_154,type,
produc512429457ist_ty: list_ty > list_ty > produc1420746395ist_ty ).
thf(func_def_155,type,
produc1909267824t_char: list_ty > produc662261637t_char > produc220283002t_char ).
thf(func_def_156,type,
produc2016959032t_char: list_ty > produc1059328077t_char > produc1025221954t_char ).
thf(func_def_157,type,
produc1916172923t_char: list_val > exp_list_char > produc662261637t_char ).
thf(func_def_158,type,
produc2078839843st_val: list_val > list_val > produc753553453st_val ).
thf(func_def_159,type,
produc1860789535har_ty: list_P1940453997har_ty > list_P1940453997har_ty > produc450000425har_ty ).
thf(func_def_160,type,
produc1152259904t_char: list_P1940453997har_ty > list_P341299826t_char > produc2146869324t_char ).
thf(func_def_161,type,
produc436875159t_char: list_P341299826t_char > list_P341299826t_char > produc244676007t_char ).
thf(func_def_162,type,
produc1545444669t_char: ty > produc809539159t_char > produc1059328077t_char ).
thf(func_def_163,type,
product_Pair_val_val: val > val > product_prod_val_val ).
thf(func_def_164,type,
produc259392253on_val: produc2090907612on_val > produc2090907612on_val > produc1581780743on_val ).
thf(func_def_165,type,
produc1924279125al_val: produc1645268488al_val > produc1645268488al_val > produc630464863al_val ).
thf(func_def_166,type,
produc833389609on_val: produc1282892786on_val > produc1282892786on_val > produc1746408499on_val ).
thf(func_def_167,type,
produc747700183on_val: produc1180562163on_val > produc1180562163on_val > produc618524391on_val ).
thf(func_def_168,type,
produc1897818327t_char: produc809539159t_char > produc809539159t_char > produc1534059751t_char ).
thf(func_def_169,type,
produc24551831t_char: produc1285161482t_char > produc1285161482t_char > produc349695911t_char ).
thf(func_def_170,type,
produc1773146955on_val: produc2088785539on_val > produc2088785539on_val > produc1368416213on_val ).
thf(func_def_171,type,
produc1265154397har_ty: produc1278157519t_char > ty > produc245756905har_ty ).
thf(func_def_172,type,
produc2080520419t_char: produc1278157519t_char > produc1278157519t_char > produc1350825965t_char ).
thf(func_def_173,type,
produc1641293463t_char: produc1971331930t_char > produc1971331930t_char > produc84451751t_char ).
thf(func_def_174,type,
produc1431439831t_char: produc952412819t_char > produc952412819t_char > produc740765671t_char ).
thf(func_def_175,type,
produc57279289t_char: produc220283002t_char > produc220283002t_char > produc1406897475t_char ).
thf(func_def_176,type,
produc1299387215t_char: produc662261637t_char > produc662261637t_char > produc1826280281t_char ).
thf(func_def_177,type,
produc635935767t_char: produc2146869324t_char > produc2146869324t_char > produc494726439t_char ).
thf(func_def_178,type,
produc1244920211al_val: product_prod_val_val > product_prod_val_val > produc800118557al_val ).
thf(func_def_179,type,
produc345758123on_val: produc1746408499on_val > produc1746408499on_val > produc652964533on_val ).
thf(func_def_180,type,
produc1347028499on_val: produc618524391on_val > produc618524391on_val > produc1250491293on_val ).
thf(func_def_181,type,
produc1402621651_val_o: ( produc2090907612on_val > $o ) > ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ).
thf(func_def_182,type,
produc275195559_val_o: ( produc1645268488al_val > $o ) > bop > product_prod_val_val > $o ).
thf(func_def_183,type,
produc1287763389_val_o: ( produc1282892786on_val > $o ) > exp_list_char > produc2090907612on_val > $o ).
thf(func_def_184,type,
produc618849246_val_o: ( produc1180562163on_val > $o ) > list_exp_list_char > produc2090907612on_val > $o ).
thf(func_def_185,type,
produc1404278138char_o: ( produc809539159t_char > $o ) > list_list_char > exp_list_char > $o ).
thf(func_def_186,type,
produc193646727char_o: ( produc1285161482t_char > $o ) > list_list_char > produc220283002t_char > $o ).
thf(func_def_187,type,
produc1177570924_val_o: ( produc2088785539on_val > $o ) > list_char > ( produc1278157519t_char > option_val ) > $o ).
thf(func_def_188,type,
produc1673424105ion_ty: ( produc2088785539on_val > option_ty ) > list_char > ( produc1278157519t_char > option_val ) > option_ty ).
thf(func_def_189,type,
produc1709467424char_o: ( produc1278157519t_char > $o ) > list_char > list_char > $o ).
thf(func_def_190,type,
produc1383007933char_o: ( produc1971331930t_char > $o ) > list_char > produc952412819t_char > $o ).
thf(func_def_191,type,
produc325775556char_o: ( produc952412819t_char > $o ) > list_char > produc2146869324t_char > $o ).
thf(func_def_192,type,
produc786676533char_o: ( produc220283002t_char > $o ) > list_ty > produc662261637t_char > $o ).
thf(func_def_193,type,
produc1072551658char_o: ( produc662261637t_char > $o ) > list_val > exp_list_char > $o ).
thf(func_def_194,type,
produc2107091019char_o: ( produc2146869324t_char > $o ) > list_P1940453997har_ty > list_P341299826t_char > $o ).
thf(func_def_195,type,
produc575837646_val_o: ( product_prod_val_val > $o ) > val > val > $o ).
thf(func_def_196,type,
produc803302844_val_o: ( produc1746408499on_val > $o ) > produc1282892786on_val > produc1282892786on_val > $o ).
thf(func_def_197,type,
produc551782158_val_o: ( produc618524391on_val > $o ) > produc1180562163on_val > produc1180562163on_val > $o ).
thf(func_def_198,type,
produc575577405_val_o: ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > produc2090907612on_val > $o ).
thf(func_def_199,type,
produc1576476927ion_ty: ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > produc2088785539on_val > option_ty ).
thf(func_def_200,type,
produc252486962_val_o: ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > produc2090907612on_val > $o ).
thf(func_def_201,type,
produc1063861510_val_o: ( bop > product_prod_val_val > $o ) > produc1645268488al_val > $o ).
thf(func_def_202,type,
produc1835097372_val_o: ( exp_list_char > produc2090907612on_val > $o ) > produc1282892786on_val > $o ).
thf(func_def_203,type,
produc1841295295_val_o: ( list_exp_list_char > produc2090907612on_val > $o ) > produc1180562163on_val > $o ).
thf(func_def_204,type,
produc1596287579char_o: ( list_list_char > exp_list_char > $o ) > produc809539159t_char > $o ).
thf(func_def_205,type,
produc1530867176char_o: ( list_list_char > produc220283002t_char > $o ) > produc1285161482t_char > $o ).
thf(func_def_206,type,
produc765165771_val_o: ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc2088785539on_val > $o ).
thf(func_def_207,type,
produc863160906ion_ty: ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > produc2088785539on_val > option_ty ).
thf(func_def_208,type,
produc282231039char_o: ( list_char > list_char > $o ) > produc1278157519t_char > $o ).
thf(func_def_209,type,
produc1519396638char_o: ( list_char > produc952412819t_char > $o ) > produc1971331930t_char > $o ).
thf(func_def_210,type,
produc781483429char_o: ( list_char > produc2146869324t_char > $o ) > produc952412819t_char > $o ).
thf(func_def_211,type,
produc861054100char_o: ( list_ty > produc662261637t_char > $o ) > produc220283002t_char > $o ).
thf(func_def_212,type,
produc525137097char_o: ( list_val > exp_list_char > $o ) > produc662261637t_char > $o ).
thf(func_def_213,type,
produc875422124char_o: ( list_P1940453997har_ty > list_P341299826t_char > $o ) > produc2146869324t_char > $o ).
thf(func_def_214,type,
produc9430317_val_o: ( val > val > $o ) > product_prod_val_val > $o ).
thf(func_def_215,type,
produc1624062875_val_o: ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1746408499on_val > $o ).
thf(func_def_216,type,
produc2136448621_val_o: ( produc1180562163on_val > produc1180562163on_val > $o ) > produc618524391on_val > $o ).
thf(func_def_217,type,
wTrt: list_P1999446415t_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > ty > $o ).
thf(func_def_218,type,
wTrts: list_P1999446415t_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > list_exp_list_char > list_ty > $o ).
thf(func_def_219,type,
collect_list_char: ( list_char > $o ) > list_char > $o ).
thf(func_def_220,type,
collect_nat: ( nat > $o ) > nat > $o ).
thf(func_def_221,type,
collec1797130234t_char: ( produc1278157519t_char > $o ) > produc1278157519t_char > $o ).
thf(func_def_222,type,
collec1583467887t_char: ( produc1971331930t_char > $o ) > produc1971331930t_char > $o ).
thf(func_def_223,type,
collec1387638140t_char: ( produc1013743697t_char > $o ) > produc1013743697t_char > $o ).
thf(func_def_224,type,
collec1451572574on_val: ( produc1746408499on_val > $o ) > produc1746408499on_val > $o ).
thf(func_def_225,type,
collec507727762on_val: ( produc618524391on_val > $o ) > produc618524391on_val > $o ).
thf(func_def_226,type,
assigned: list_char > exp_list_char > $o ).
thf(func_def_227,type,
blocks: produc1285161482t_char > exp_list_char ).
thf(func_def_228,type,
red: list_P1999446415t_char > produc1746408499on_val > $o ).
thf(func_def_229,type,
redp: list_P1999446415t_char > exp_list_char > produc2090907612on_val > exp_list_char > produc2090907612on_val > $o ).
thf(func_def_230,type,
reds: list_P1999446415t_char > produc618524391on_val > $o ).
thf(func_def_231,type,
redsp: list_P1999446415t_char > list_exp_list_char > produc2090907612on_val > list_exp_list_char > produc2090907612on_val > $o ).
thf(func_def_232,type,
hp: produc2090907612on_val > nat > option1728594148on_val ).
thf(func_def_233,type,
transi1395422419t_char: ( produc1278157519t_char > $o ) > produc1278157519t_char > $o ).
thf(func_def_234,type,
transi935034983cl_val: ( product_prod_val_val > $o ) > product_prod_val_val > $o ).
thf(func_def_235,type,
transi466770671on_val: ( produc1581780743on_val > $o ) > produc1581780743on_val > $o ).
thf(func_def_236,type,
transi1906258203al_val: ( produc630464863al_val > $o ) > produc630464863al_val > $o ).
thf(func_def_237,type,
transi2118771717on_val: ( produc1746408499on_val > $o ) > produc1746408499on_val > $o ).
thf(func_def_238,type,
transi808828192on_val: ( produc618524391on_val > $o ) > produc618524391on_val > $o ).
thf(func_def_239,type,
transi198989188t_char: ( produc1534059751t_char > $o ) > produc1534059751t_char > $o ).
thf(func_def_240,type,
transi122195895t_char: ( produc349695911t_char > $o ) > produc349695911t_char > $o ).
thf(func_def_241,type,
transi1669211542on_val: ( produc1368416213on_val > $o ) > produc1368416213on_val > $o ).
thf(func_def_242,type,
transi1095029602t_char: ( produc1350825965t_char > $o ) > produc1350825965t_char > $o ).
thf(func_def_243,type,
transi1123801095t_char: ( produc84451751t_char > $o ) > produc84451751t_char > $o ).
thf(func_def_244,type,
transi2005320128t_char: ( produc740765671t_char > $o ) > produc740765671t_char > $o ).
thf(func_def_245,type,
transi1257872013t_char: ( produc1406897475t_char > $o ) > produc1406897475t_char > $o ).
thf(func_def_246,type,
transi1789604888t_char: ( produc1826280281t_char > $o ) > produc1826280281t_char > $o ).
thf(func_def_247,type,
transi772168185t_char: ( produc494726439t_char > $o ) > produc494726439t_char > $o ).
thf(func_def_248,type,
transi1423755450al_val: ( produc800118557al_val > $o ) > produc800118557al_val > $o ).
thf(func_def_249,type,
transi130214086on_val: ( produc652964533on_val > $o ) > produc652964533on_val > $o ).
thf(func_def_250,type,
transi1457397498on_val: ( produc1250491293on_val > $o ) > produc1250491293on_val > $o ).
thf(func_def_251,type,
transi1065307915t_char: ( list_char > list_char > $o ) > list_char > list_char > $o ).
thf(func_def_252,type,
fields1147507508t_char: list_P1999446415t_char > list_char > list_P2023964830har_ty > $o ).
thf(func_def_253,type,
method1809630380t_char: list_P1999446415t_char > list_char > list_char > list_ty > ty > produc809539159t_char > list_char > $o ).
thf(func_def_254,type,
has_fi1183600461t_char: list_P1999446415t_char > list_char > list_char > ty > list_char > $o ).
thf(func_def_255,type,
subcls851966956t_char: list_P1999446415t_char > produc1278157519t_char > $o ).
thf(func_def_256,type,
subcls744239332t_char: list_P1999446415t_char > list_char > list_char > $o ).
thf(func_def_257,type,
widen_2090681816t_char: list_P1999446415t_char > ty > ty > $o ).
thf(func_def_258,type,
typeSa816273224_sconf: list_P1999446415t_char > ( list_char > option_ty ) > produc2090907612on_val > $o ).
thf(func_def_259,type,
is_refT: ty > $o ).
thf(func_def_260,type,
this: list_char ).
thf(func_def_261,type,
class: list_char > ty ).
thf(func_def_262,type,
nt: ty ).
thf(func_def_263,type,
void: ty ).
thf(func_def_264,type,
addr: nat > val ).
thf(func_def_265,type,
bool: $o > val ).
thf(func_def_266,type,
null: val ).
thf(func_def_267,type,
unit: val ).
thf(func_def_268,type,
wwf_J_mdecl: list_P1999446415t_char > list_char > produc1013743697t_char > $o ).
thf(func_def_269,type,
wf_pro755087577t_char: ( list_P1999446415t_char > list_char > produc1013743697t_char > $o ) > list_P1999446415t_char > $o ).
thf(func_def_270,type,
wTrt_1: list_P1999446415t_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > ty > $o ).
thf(func_def_271,type,
wTrts_1: list_P1999446415t_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > list_exp_list_char > list_ty > $o ).
thf(func_def_272,type,
lex_pr359407722on_val: ( produc1287081631on_val > $o ) > ( produc774316953on_val > $o ) > produc1581780743on_val > $o ).
thf(func_def_273,type,
lex_pr1932514710al_val: ( product_prod_bop_bop > $o ) > ( produc800118557al_val > $o ) > produc630464863al_val > $o ).
thf(func_def_274,type,
lex_pr1492265728on_val: ( produc2048519645t_char > $o ) > ( produc1581780743on_val > $o ) > produc1746408499on_val > $o ).
thf(func_def_275,type,
lex_pr855826389on_val: ( produc91527719t_char > $o ) > ( produc1581780743on_val > $o ) > produc618524391on_val > $o ).
thf(func_def_276,type,
lex_pr1787105337t_char: ( produc1200003175t_char > $o ) > ( produc2048519645t_char > $o ) > produc1534059751t_char > $o ).
thf(func_def_277,type,
lex_pr1876288492t_char: ( produc1200003175t_char > $o ) > ( produc1406897475t_char > $o ) > produc349695911t_char > $o ).
thf(func_def_278,type,
lex_pr697649425on_val: ( produc1278157519t_char > $o ) > ( produc688860215on_val > $o ) > produc1368416213on_val > $o ).
thf(func_def_279,type,
lex_pr280535005t_char: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > produc1350825965t_char > $o ).
thf(func_def_280,type,
lex_pr1668767798t_char: ( produc1278157519t_char > $o ) > ( produc740765671t_char > $o ) > produc84451751t_char > $o ).
thf(func_def_281,type,
lex_pr167435119t_char: ( produc1278157519t_char > $o ) > ( produc494726439t_char > $o ) > produc740765671t_char > $o ).
thf(func_def_282,type,
lex_pr1588300168t_char: ( produc1420746395ist_ty > $o ) > ( produc1826280281t_char > $o ) > produc1406897475t_char > $o ).
thf(func_def_283,type,
lex_pr307591827t_char: ( produc753553453st_val > $o ) > ( produc2048519645t_char > $o ) > produc1826280281t_char > $o ).
thf(func_def_284,type,
lex_pr213428520t_char: ( produc450000425har_ty > $o ) > ( produc244676007t_char > $o ) > produc494726439t_char > $o ).
thf(func_def_285,type,
lex_prod_val_val: ( product_prod_val_val > $o ) > ( product_prod_val_val > $o ) > produc800118557al_val > $o ).
thf(func_def_286,type,
lex_pr296420417on_val: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > produc652964533on_val > $o ).
thf(func_def_287,type,
lex_pr1943870447on_val: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > produc1250491293on_val > $o ).
thf(func_def_288,type,
member_list_char: list_char > ( list_char > $o ) > $o ).
thf(func_def_289,type,
member_nat: nat > ( nat > $o ) > $o ).
thf(func_def_290,type,
member1838289030on_val: produc774316953on_val > ( produc774316953on_val > $o ) > $o ).
thf(func_def_291,type,
member1846553161on_val: produc2090907612on_val > ( produc2090907612on_val > $o ) > $o ).
thf(func_def_292,type,
member112887436on_val: produc1287081631on_val > ( produc1287081631on_val > $o ) > $o ).
thf(func_def_293,type,
member1448924196on_val: produc688860215on_val > ( produc688860215on_val > $o ) > $o ).
thf(func_def_294,type,
member978285664op_bop: product_prod_bop_bop > ( product_prod_bop_bop > $o ) > $o ).
thf(func_def_295,type,
member1417904245al_val: produc1645268488al_val > ( produc1645268488al_val > $o ) > $o ).
thf(func_def_296,type,
member1199939018t_char: produc2048519645t_char > ( produc2048519645t_char > $o ) > $o ).
thf(func_def_297,type,
member1072200031on_val: produc1282892786on_val > ( produc1282892786on_val > $o ) > $o ).
thf(func_def_298,type,
member894971540t_char: produc91527719t_char > ( produc91527719t_char > $o ) > $o ).
thf(func_def_299,type,
member1224782662on_val: produc1180562163on_val > ( produc1180562163on_val > $o ) > $o ).
thf(func_def_300,type,
member1840112042t_char: produc809539159t_char > ( produc809539159t_char > $o ) > $o ).
thf(func_def_301,type,
member817832404t_char: produc1200003175t_char > ( produc1200003175t_char > $o ) > $o ).
thf(func_def_302,type,
member133545693t_char: produc1285161482t_char > ( produc1285161482t_char > $o ) > $o ).
thf(func_def_303,type,
member1374264560on_val: produc2088785539on_val > ( produc2088785539on_val > $o ) > $o ).
thf(func_def_304,type,
member1251428284t_char: produc1278157519t_char > ( produc1278157519t_char > $o ) > $o ).
thf(func_def_305,type,
member1467889965t_char: produc1971331930t_char > ( produc1971331930t_char > $o ) > $o ).
thf(func_def_306,type,
member1601084734t_char: produc1013743697t_char > ( produc1013743697t_char > $o ) > $o ).
thf(func_def_307,type,
member1771544038t_char: produc952412819t_char > ( produc952412819t_char > $o ) > $o ).
thf(func_def_308,type,
member104734088ist_ty: produc1420746395ist_ty > ( produc1420746395ist_ty > $o ) > $o ).
thf(func_def_309,type,
member140606439t_char: produc220283002t_char > ( produc220283002t_char > $o ) > $o ).
thf(func_def_310,type,
member699351154t_char: produc662261637t_char > ( produc662261637t_char > $o ) > $o ).
thf(func_def_311,type,
member273646106st_val: produc753553453st_val > ( produc753553453st_val > $o ) > $o ).
thf(func_def_312,type,
member520253462har_ty: produc450000425har_ty > ( produc450000425har_ty > $o ) > $o ).
thf(func_def_313,type,
member1379348767t_char: produc2146869324t_char > ( produc2146869324t_char > $o ) > $o ).
thf(func_def_314,type,
member1580476948t_char: produc244676007t_char > ( produc244676007t_char > $o ) > $o ).
thf(func_def_315,type,
member649088532al_val: product_prod_val_val > ( product_prod_val_val > $o ) > $o ).
thf(func_def_316,type,
member565037556on_val: produc1581780743on_val > ( produc1581780743on_val > $o ) > $o ).
thf(func_def_317,type,
member1732271180al_val: produc630464863al_val > ( produc630464863al_val > $o ) > $o ).
thf(func_def_318,type,
member1913460000on_val: produc1746408499on_val > ( produc1746408499on_val > $o ) > $o ).
thf(func_def_319,type,
member2042188884on_val: produc618524391on_val > ( produc618524391on_val > $o ) > $o ).
thf(func_def_320,type,
member1999287380t_char: produc1534059751t_char > ( produc1534059751t_char > $o ) > $o ).
thf(func_def_321,type,
member1420286996t_char: produc349695911t_char > ( produc349695911t_char > $o ) > $o ).
thf(func_def_322,type,
member1235075778on_val: produc1368416213on_val > ( produc1368416213on_val > $o ) > $o ).
thf(func_def_323,type,
member794220506t_char: produc1350825965t_char > ( produc1350825965t_char > $o ) > $o ).
thf(func_def_324,type,
member162552852t_char: produc84451751t_char > ( produc84451751t_char > $o ) > $o ).
thf(func_def_325,type,
member1607118676t_char: produc740765671t_char > ( produc740765671t_char > $o ) > $o ).
thf(func_def_326,type,
member125098544t_char: produc1406897475t_char > ( produc1406897475t_char > $o ) > $o ).
thf(func_def_327,type,
member1161907014t_char: produc1826280281t_char > ( produc1826280281t_char > $o ) > $o ).
thf(func_def_328,type,
member1551446420t_char: produc494726439t_char > ( produc494726439t_char > $o ) > $o ).
thf(func_def_329,type,
member837208074al_val: produc800118557al_val > ( produc800118557al_val > $o ) > $o ).
thf(func_def_330,type,
member1714424482on_val: produc652964533on_val > ( produc652964533on_val > $o ) > $o ).
thf(func_def_331,type,
member1145216138on_val: produc1250491293on_val > ( produc1250491293on_val > $o ) > $o ).
thf(func_def_332,type,
e: list_char > option_ty ).
thf(func_def_333,type,
p: list_P1999446415t_char ).
thf(func_def_334,type,
t: ty ).
thf(func_def_335,type,
t_1: ty ).
thf(func_def_336,type,
v_1: list_char ).
thf(func_def_337,type,
e_a: exp_list_char ).
thf(func_def_338,type,
ea: exp_list_char ).
thf(func_def_339,type,
h_a: nat > option1728594148on_val ).
thf(func_def_340,type,
ha: nat > option1728594148on_val ).
thf(func_def_341,type,
l_a: list_char > option_val ).
thf(func_def_342,type,
la: list_char > option_val ).
thf(func_def_343,type,
v_2: val ).
thf(func_def_344,type,
v: val ).
thf(func_def_346,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_347,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_348,type,
vAND: $o > $o > $o ).
thf(func_def_349,type,
vNOT: $o > $o ).
thf(func_def_350,type,
vOR: $o > $o > $o ).
thf(func_def_353,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_354,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_355,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_356,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_357,type,
sP0: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > bop > $o ).
thf(func_def_358,type,
sP1: produc2090907612on_val > list_P1999446415t_char > exp_list_char > exp_list_char > exp_list_char > produc2090907612on_val > $o ).
thf(func_def_359,type,
sP2: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > $o ).
thf(func_def_360,type,
sP3: ty > exp_list_char > list_char > list_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > list_P1999446415t_char > $o ).
thf(func_def_361,type,
sK4: ( list_char > option_ty ) > ty > ty ).
thf(func_def_362,type,
sK5: ( produc1250491293on_val > $o ) > produc618524391on_val ).
thf(func_def_363,type,
sK6: ( produc1250491293on_val > $o ) > produc1180562163on_val ).
thf(func_def_364,type,
sK7: ( produc1250491293on_val > $o ) > list_exp_list_char ).
thf(func_def_365,type,
sK8: ( produc1250491293on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_366,type,
sK9: ( produc1250491293on_val > $o ) > list_char > option_val ).
thf(func_def_367,type,
sK10: ( produc652964533on_val > $o ) > produc1746408499on_val ).
thf(func_def_368,type,
sK11: ( produc652964533on_val > $o ) > produc1282892786on_val ).
thf(func_def_369,type,
sK12: ( produc652964533on_val > $o ) > exp_list_char ).
thf(func_def_370,type,
sK13: ( produc652964533on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_371,type,
sK14: ( produc652964533on_val > $o ) > list_char > option_val ).
thf(func_def_372,type,
sK15: ( produc349695911t_char > $o ) > produc1285161482t_char ).
thf(func_def_373,type,
sK16: ( produc349695911t_char > $o ) > list_list_char ).
thf(func_def_374,type,
sK17: ( produc349695911t_char > $o ) > list_ty ).
thf(func_def_375,type,
sK18: ( produc349695911t_char > $o ) > list_val ).
thf(func_def_376,type,
sK19: ( produc349695911t_char > $o ) > exp_list_char ).
thf(func_def_377,type,
sK20: ( produc84451751t_char > $o ) > produc1971331930t_char ).
thf(func_def_378,type,
sK21: ( produc84451751t_char > $o ) > list_char ).
thf(func_def_379,type,
sK22: ( produc84451751t_char > $o ) > list_char ).
thf(func_def_380,type,
sK23: ( produc84451751t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_381,type,
sK24: ( produc84451751t_char > $o ) > list_P341299826t_char ).
thf(func_def_382,type,
sK25: ( produc1013743697t_char > $o ) > list_char ).
thf(func_def_383,type,
sK26: ( produc1013743697t_char > $o ) > list_ty ).
thf(func_def_384,type,
sK27: ( produc1013743697t_char > $o ) > ty ).
thf(func_def_385,type,
sK28: ( produc1013743697t_char > $o ) > list_list_char ).
thf(func_def_386,type,
sK29: ( produc1013743697t_char > $o ) > exp_list_char ).
thf(func_def_387,type,
sK30: produc1250491293on_val > produc618524391on_val ).
thf(func_def_388,type,
sK31: produc1250491293on_val > produc1180562163on_val ).
thf(func_def_389,type,
sK32: produc1250491293on_val > list_exp_list_char ).
thf(func_def_390,type,
sK33: produc1250491293on_val > nat > option1728594148on_val ).
thf(func_def_391,type,
sK34: produc1250491293on_val > list_char > option_val ).
thf(func_def_392,type,
sK35: produc652964533on_val > produc1746408499on_val ).
thf(func_def_393,type,
sK36: produc652964533on_val > produc1282892786on_val ).
thf(func_def_394,type,
sK37: produc652964533on_val > exp_list_char ).
thf(func_def_395,type,
sK38: produc652964533on_val > nat > option1728594148on_val ).
thf(func_def_396,type,
sK39: produc652964533on_val > list_char > option_val ).
thf(func_def_397,type,
sK40: produc349695911t_char > produc1285161482t_char ).
thf(func_def_398,type,
sK41: produc349695911t_char > list_list_char ).
thf(func_def_399,type,
sK42: produc349695911t_char > list_ty ).
thf(func_def_400,type,
sK43: produc349695911t_char > list_val ).
thf(func_def_401,type,
sK44: produc349695911t_char > exp_list_char ).
thf(func_def_402,type,
sK45: produc84451751t_char > produc1971331930t_char ).
thf(func_def_403,type,
sK46: produc84451751t_char > list_char ).
thf(func_def_404,type,
sK47: produc84451751t_char > list_char ).
thf(func_def_405,type,
sK48: produc84451751t_char > list_P1940453997har_ty ).
thf(func_def_406,type,
sK49: produc84451751t_char > list_P341299826t_char ).
thf(func_def_407,type,
sK50: produc1013743697t_char > list_char ).
thf(func_def_408,type,
sK51: produc1013743697t_char > list_ty ).
thf(func_def_409,type,
sK52: produc1013743697t_char > ty ).
thf(func_def_410,type,
sK53: produc1013743697t_char > list_list_char ).
thf(func_def_411,type,
sK54: produc1013743697t_char > exp_list_char ).
thf(func_def_412,type,
sK55: ( produc1013743697t_char > $o ) > list_char ).
thf(func_def_413,type,
sK56: ( produc1013743697t_char > $o ) > list_ty ).
thf(func_def_414,type,
sK57: ( produc1013743697t_char > $o ) > ty ).
thf(func_def_415,type,
sK58: ( produc1013743697t_char > $o ) > produc809539159t_char ).
thf(func_def_416,type,
sK59: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_417,type,
sK60: ( produc1746408499on_val > $o ) > exp_list_char ).
thf(func_def_418,type,
sK61: ( produc1746408499on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_419,type,
sK62: ( produc1746408499on_val > $o ) > list_char > option_val ).
thf(func_def_420,type,
sK63: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_421,type,
sK64: ( produc618524391on_val > $o ) > list_exp_list_char ).
thf(func_def_422,type,
sK65: ( produc618524391on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_423,type,
sK66: ( produc618524391on_val > $o ) > list_char > option_val ).
thf(func_def_424,type,
sK67: ( produc1285161482t_char > $o ) > list_list_char ).
thf(func_def_425,type,
sK68: ( produc1285161482t_char > $o ) > list_ty ).
thf(func_def_426,type,
sK69: ( produc1285161482t_char > $o ) > list_val ).
thf(func_def_427,type,
sK70: ( produc1285161482t_char > $o ) > exp_list_char ).
thf(func_def_428,type,
sK71: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_429,type,
sK72: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_430,type,
sK73: ( produc1971331930t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_431,type,
sK74: ( produc1971331930t_char > $o ) > list_P341299826t_char ).
thf(func_def_432,type,
sK75: ( produc652964533on_val > $o ) > produc1746408499on_val ).
thf(func_def_433,type,
sK76: ( produc652964533on_val > $o ) > produc1282892786on_val ).
thf(func_def_434,type,
sK77: ( produc652964533on_val > $o ) > exp_list_char ).
thf(func_def_435,type,
sK78: ( produc652964533on_val > $o ) > produc2090907612on_val ).
thf(func_def_436,type,
sK79: ( produc630464863al_val > $o ) > produc1645268488al_val ).
thf(func_def_437,type,
sK80: ( produc630464863al_val > $o ) > bop ).
thf(func_def_438,type,
sK81: ( produc630464863al_val > $o ) > val ).
thf(func_def_439,type,
sK82: ( produc630464863al_val > $o ) > val ).
thf(func_def_440,type,
sK83: ( produc1250491293on_val > $o ) > produc618524391on_val ).
thf(func_def_441,type,
sK84: ( produc1250491293on_val > $o ) > produc1180562163on_val ).
thf(func_def_442,type,
sK85: ( produc1250491293on_val > $o ) > list_exp_list_char ).
thf(func_def_443,type,
sK86: ( produc1250491293on_val > $o ) > produc2090907612on_val ).
thf(func_def_444,type,
sK87: ( produc349695911t_char > $o ) > produc1285161482t_char ).
thf(func_def_445,type,
sK88: ( produc349695911t_char > $o ) > list_list_char ).
thf(func_def_446,type,
sK89: ( produc349695911t_char > $o ) > list_ty ).
thf(func_def_447,type,
sK90: ( produc349695911t_char > $o ) > produc662261637t_char ).
thf(func_def_448,type,
sK91: ( produc1406897475t_char > $o ) > produc220283002t_char ).
thf(func_def_449,type,
sK92: ( produc1406897475t_char > $o ) > list_ty ).
thf(func_def_450,type,
sK93: ( produc1406897475t_char > $o ) > list_val ).
thf(func_def_451,type,
sK94: ( produc1406897475t_char > $o ) > exp_list_char ).
thf(func_def_452,type,
sK95: ( produc84451751t_char > $o ) > produc1971331930t_char ).
thf(func_def_453,type,
sK96: ( produc84451751t_char > $o ) > list_char ).
thf(func_def_454,type,
sK97: ( produc84451751t_char > $o ) > list_char ).
thf(func_def_455,type,
sK98: ( produc84451751t_char > $o ) > produc2146869324t_char ).
thf(func_def_456,type,
sK99: ( produc740765671t_char > $o ) > produc952412819t_char ).
thf(func_def_457,type,
sK100: ( produc740765671t_char > $o ) > list_char ).
thf(func_def_458,type,
sK101: ( produc740765671t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_459,type,
sK102: ( produc740765671t_char > $o ) > list_P341299826t_char ).
thf(func_def_460,type,
sK103: produc1013743697t_char > list_char ).
thf(func_def_461,type,
sK104: produc1013743697t_char > list_ty ).
thf(func_def_462,type,
sK105: produc1013743697t_char > ty ).
thf(func_def_463,type,
sK106: produc1013743697t_char > produc809539159t_char ).
thf(func_def_464,type,
sK107: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_465,type,
sK108: produc1746408499on_val > exp_list_char ).
thf(func_def_466,type,
sK109: produc1746408499on_val > nat > option1728594148on_val ).
thf(func_def_467,type,
sK110: produc1746408499on_val > list_char > option_val ).
thf(func_def_468,type,
sK111: produc618524391on_val > produc1180562163on_val ).
thf(func_def_469,type,
sK112: produc618524391on_val > list_exp_list_char ).
thf(func_def_470,type,
sK113: produc618524391on_val > nat > option1728594148on_val ).
thf(func_def_471,type,
sK114: produc618524391on_val > list_char > option_val ).
thf(func_def_472,type,
sK115: produc1285161482t_char > list_list_char ).
thf(func_def_473,type,
sK116: produc1285161482t_char > list_ty ).
thf(func_def_474,type,
sK117: produc1285161482t_char > list_val ).
thf(func_def_475,type,
sK118: produc1285161482t_char > exp_list_char ).
thf(func_def_476,type,
sK119: produc1971331930t_char > list_char ).
thf(func_def_477,type,
sK120: produc1971331930t_char > list_char ).
thf(func_def_478,type,
sK121: produc1971331930t_char > list_P1940453997har_ty ).
thf(func_def_479,type,
sK122: produc1971331930t_char > list_P341299826t_char ).
thf(func_def_480,type,
sK123: produc652964533on_val > produc1746408499on_val ).
thf(func_def_481,type,
sK124: produc652964533on_val > produc1282892786on_val ).
thf(func_def_482,type,
sK125: produc652964533on_val > exp_list_char ).
thf(func_def_483,type,
sK126: produc652964533on_val > produc2090907612on_val ).
thf(func_def_484,type,
sK127: produc630464863al_val > produc1645268488al_val ).
thf(func_def_485,type,
sK128: produc630464863al_val > bop ).
thf(func_def_486,type,
sK129: produc630464863al_val > val ).
thf(func_def_487,type,
sK130: produc630464863al_val > val ).
thf(func_def_488,type,
sK131: produc1250491293on_val > produc618524391on_val ).
thf(func_def_489,type,
sK132: produc1250491293on_val > produc1180562163on_val ).
thf(func_def_490,type,
sK133: produc1250491293on_val > list_exp_list_char ).
thf(func_def_491,type,
sK134: produc1250491293on_val > produc2090907612on_val ).
thf(func_def_492,type,
sK135: produc349695911t_char > produc1285161482t_char ).
thf(func_def_493,type,
sK136: produc349695911t_char > list_list_char ).
thf(func_def_494,type,
sK137: produc349695911t_char > list_ty ).
thf(func_def_495,type,
sK138: produc349695911t_char > produc662261637t_char ).
thf(func_def_496,type,
sK139: produc1406897475t_char > produc220283002t_char ).
thf(func_def_497,type,
sK140: produc1406897475t_char > list_ty ).
thf(func_def_498,type,
sK141: produc1406897475t_char > list_val ).
thf(func_def_499,type,
sK142: produc1406897475t_char > exp_list_char ).
thf(func_def_500,type,
sK143: produc84451751t_char > produc1971331930t_char ).
thf(func_def_501,type,
sK144: produc84451751t_char > list_char ).
thf(func_def_502,type,
sK145: produc84451751t_char > list_char ).
thf(func_def_503,type,
sK146: produc84451751t_char > produc2146869324t_char ).
thf(func_def_504,type,
sK147: produc740765671t_char > produc952412819t_char ).
thf(func_def_505,type,
sK148: produc740765671t_char > list_char ).
thf(func_def_506,type,
sK149: produc740765671t_char > list_P1940453997har_ty ).
thf(func_def_507,type,
sK150: produc740765671t_char > list_P341299826t_char ).
thf(func_def_508,type,
sK151: ( produc917948472har_ty > $o ) > list_char ).
thf(func_def_509,type,
sK152: ( produc917948472har_ty > $o ) > ty ).
thf(func_def_510,type,
sK153: ( produc245756905har_ty > $o ) > produc1278157519t_char ).
thf(func_def_511,type,
sK154: ( produc245756905har_ty > $o ) > ty ).
thf(func_def_512,type,
sK155: ( produc1013743697t_char > $o ) > list_char ).
thf(func_def_513,type,
sK156: ( produc1013743697t_char > $o ) > produc1025221954t_char ).
thf(func_def_514,type,
sK157: ( produc1534059751t_char > $o ) > produc809539159t_char ).
thf(func_def_515,type,
sK158: ( produc1534059751t_char > $o ) > produc809539159t_char ).
thf(func_def_516,type,
sK159: ( produc494726439t_char > $o ) > produc2146869324t_char ).
thf(func_def_517,type,
sK160: ( produc494726439t_char > $o ) > produc2146869324t_char ).
thf(func_def_518,type,
sK161: ( produc740765671t_char > $o ) > produc952412819t_char ).
thf(func_def_519,type,
sK162: ( produc740765671t_char > $o ) > produc952412819t_char ).
thf(func_def_520,type,
sK163: ( produc84451751t_char > $o ) > produc1971331930t_char ).
thf(func_def_521,type,
sK164: ( produc84451751t_char > $o ) > produc1971331930t_char ).
thf(func_def_522,type,
sK165: ( produc1826280281t_char > $o ) > produc662261637t_char ).
thf(func_def_523,type,
sK166: ( produc1826280281t_char > $o ) > produc662261637t_char ).
thf(func_def_524,type,
sK167: ( produc1406897475t_char > $o ) > produc220283002t_char ).
thf(func_def_525,type,
sK168: ( produc1406897475t_char > $o ) > produc220283002t_char ).
thf(func_def_526,type,
sK169: ( produc349695911t_char > $o ) > produc1285161482t_char ).
thf(func_def_527,type,
sK170: ( produc349695911t_char > $o ) > produc1285161482t_char ).
thf(func_def_528,type,
sK171: ( produc1250491293on_val > $o ) > produc618524391on_val ).
thf(func_def_529,type,
sK172: ( produc1250491293on_val > $o ) > produc618524391on_val ).
thf(func_def_530,type,
sK173: ( produc800118557al_val > $o ) > product_prod_val_val ).
thf(func_def_531,type,
sK174: ( produc800118557al_val > $o ) > product_prod_val_val ).
thf(func_def_532,type,
sK175: ( produc630464863al_val > $o ) > produc1645268488al_val ).
thf(func_def_533,type,
sK176: ( produc630464863al_val > $o ) > produc1645268488al_val ).
thf(func_def_534,type,
sK177: ( produc1350825965t_char > $o ) > produc1278157519t_char ).
thf(func_def_535,type,
sK178: ( produc1350825965t_char > $o ) > produc1278157519t_char ).
thf(func_def_536,type,
sK179: ( produc1368416213on_val > $o ) > produc2088785539on_val ).
thf(func_def_537,type,
sK180: ( produc1368416213on_val > $o ) > produc2088785539on_val ).
thf(func_def_538,type,
sK181: ( produc1581780743on_val > $o ) > produc2090907612on_val ).
thf(func_def_539,type,
sK182: ( produc1581780743on_val > $o ) > produc2090907612on_val ).
thf(func_def_540,type,
sK183: ( produc652964533on_val > $o ) > produc1746408499on_val ).
thf(func_def_541,type,
sK184: ( produc652964533on_val > $o ) > produc1746408499on_val ).
thf(func_def_542,type,
sK185: ( produc91527719t_char > $o ) > list_exp_list_char ).
thf(func_def_543,type,
sK186: ( produc91527719t_char > $o ) > list_exp_list_char ).
thf(func_def_544,type,
sK187: ( produc2048519645t_char > $o ) > exp_list_char ).
thf(func_def_545,type,
sK188: ( produc2048519645t_char > $o ) > exp_list_char ).
thf(func_def_546,type,
sK189: ( produc1200003175t_char > $o ) > list_list_char ).
thf(func_def_547,type,
sK190: ( produc1200003175t_char > $o ) > list_list_char ).
thf(func_def_548,type,
sK191: ( produc450000425har_ty > $o ) > list_P1940453997har_ty ).
thf(func_def_549,type,
sK192: ( produc450000425har_ty > $o ) > list_P1940453997har_ty ).
thf(func_def_550,type,
sK193: ( produc244676007t_char > $o ) > list_P341299826t_char ).
thf(func_def_551,type,
sK194: ( produc244676007t_char > $o ) > list_P341299826t_char ).
thf(func_def_552,type,
sK195: ( produc753553453st_val > $o ) > list_val ).
thf(func_def_553,type,
sK196: ( produc753553453st_val > $o ) > list_val ).
thf(func_def_554,type,
sK197: ( produc1420746395ist_ty > $o ) > list_ty ).
thf(func_def_555,type,
sK198: ( produc1420746395ist_ty > $o ) > list_ty ).
thf(func_def_556,type,
sK199: ( product_prod_bop_bop > $o ) > bop ).
thf(func_def_557,type,
sK200: ( product_prod_bop_bop > $o ) > bop ).
thf(func_def_558,type,
sK201: ( produc688860215on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_559,type,
sK202: ( produc688860215on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_560,type,
sK203: ( produc1287081631on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_561,type,
sK204: ( produc1287081631on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_562,type,
sK205: ( produc774316953on_val > $o ) > list_char > option_val ).
thf(func_def_563,type,
sK206: ( produc774316953on_val > $o ) > list_char > option_val ).
thf(func_def_564,type,
sK207: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_565,type,
sK208: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_566,type,
sK209: ( produc1282892786on_val > $o ) > exp_list_char ).
thf(func_def_567,type,
sK210: ( produc1282892786on_val > $o ) > produc2090907612on_val ).
thf(func_def_568,type,
sK211: ( produc2090907612on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_569,type,
sK212: ( produc2090907612on_val > $o ) > list_char > option_val ).
thf(func_def_570,type,
sK213: ( produc2088785539on_val > $o ) > list_char ).
thf(func_def_571,type,
sK214: ( produc2088785539on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_572,type,
sK215: ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_573,type,
sK216: ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_574,type,
sK217: ( produc1645268488al_val > $o ) > bop ).
thf(func_def_575,type,
sK218: ( produc1645268488al_val > $o ) > product_prod_val_val ).
thf(func_def_576,type,
sK219: ( product_prod_val_val > $o ) > val ).
thf(func_def_577,type,
sK220: ( product_prod_val_val > $o ) > val ).
thf(func_def_578,type,
sK221: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_579,type,
sK222: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_580,type,
sK223: ( produc1180562163on_val > $o ) > list_exp_list_char ).
thf(func_def_581,type,
sK224: ( produc1180562163on_val > $o ) > produc2090907612on_val ).
thf(func_def_582,type,
sK225: ( produc1285161482t_char > $o ) > list_list_char ).
thf(func_def_583,type,
sK226: ( produc1285161482t_char > $o ) > produc220283002t_char ).
thf(func_def_584,type,
sK227: ( produc220283002t_char > $o ) > list_ty ).
thf(func_def_585,type,
sK228: ( produc220283002t_char > $o ) > produc662261637t_char ).
thf(func_def_586,type,
sK229: ( produc662261637t_char > $o ) > list_val ).
thf(func_def_587,type,
sK230: ( produc662261637t_char > $o ) > exp_list_char ).
thf(func_def_588,type,
sK231: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_589,type,
sK232: ( produc1971331930t_char > $o ) > produc952412819t_char ).
thf(func_def_590,type,
sK233: ( produc952412819t_char > $o ) > list_char ).
thf(func_def_591,type,
sK234: ( produc952412819t_char > $o ) > produc2146869324t_char ).
thf(func_def_592,type,
sK235: ( produc2146869324t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_593,type,
sK236: ( produc2146869324t_char > $o ) > list_P341299826t_char ).
thf(func_def_594,type,
sK237: ( produc809539159t_char > $o ) > list_list_char ).
thf(func_def_595,type,
sK238: ( produc809539159t_char > $o ) > exp_list_char ).
thf(func_def_596,type,
sK239: produc1013743697t_char > list_char ).
thf(func_def_597,type,
sK240: produc1013743697t_char > list_ty ).
thf(func_def_598,type,
sK241: produc1013743697t_char > produc1059328077t_char ).
thf(func_def_599,type,
sK242: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_600,type,
sK243: produc1746408499on_val > exp_list_char ).
thf(func_def_601,type,
sK244: produc1746408499on_val > produc2090907612on_val ).
thf(func_def_602,type,
sK245: produc1282892786on_val > exp_list_char ).
thf(func_def_603,type,
sK246: produc1282892786on_val > nat > option1728594148on_val ).
thf(func_def_604,type,
sK247: produc1282892786on_val > list_char > option_val ).
thf(func_def_605,type,
sK248: produc1645268488al_val > bop ).
thf(func_def_606,type,
sK249: produc1645268488al_val > val ).
thf(func_def_607,type,
sK250: produc1645268488al_val > val ).
thf(func_def_608,type,
sK251: produc618524391on_val > produc1180562163on_val ).
thf(func_def_609,type,
sK252: produc618524391on_val > list_exp_list_char ).
thf(func_def_610,type,
sK253: produc618524391on_val > produc2090907612on_val ).
thf(func_def_611,type,
sK254: produc1180562163on_val > list_exp_list_char ).
thf(func_def_612,type,
sK255: produc1180562163on_val > nat > option1728594148on_val ).
thf(func_def_613,type,
sK256: produc1180562163on_val > list_char > option_val ).
thf(func_def_614,type,
sK257: produc1285161482t_char > list_list_char ).
thf(func_def_615,type,
sK258: produc1285161482t_char > list_ty ).
thf(func_def_616,type,
sK259: produc1285161482t_char > produc662261637t_char ).
thf(func_def_617,type,
sK260: produc220283002t_char > list_ty ).
thf(func_def_618,type,
sK261: produc220283002t_char > list_val ).
thf(func_def_619,type,
sK262: produc220283002t_char > exp_list_char ).
thf(func_def_620,type,
sK263: produc1971331930t_char > list_char ).
thf(func_def_621,type,
sK264: produc1971331930t_char > list_char ).
thf(func_def_622,type,
sK265: produc1971331930t_char > produc2146869324t_char ).
thf(func_def_623,type,
sK266: produc952412819t_char > list_char ).
thf(func_def_624,type,
sK267: produc952412819t_char > list_P1940453997har_ty ).
thf(func_def_625,type,
sK268: produc952412819t_char > list_P341299826t_char ).
thf(func_def_626,type,
sK269: produc652964533on_val > produc1746408499on_val ).
thf(func_def_627,type,
sK270: produc652964533on_val > produc1282892786on_val ).
thf(func_def_628,type,
sK271: produc652964533on_val > produc1282892786on_val ).
thf(func_def_629,type,
sK272: produc1581780743on_val > produc2090907612on_val ).
thf(func_def_630,type,
sK273: produc1581780743on_val > nat > option1728594148on_val ).
thf(func_def_631,type,
sK274: produc1581780743on_val > list_char > option_val ).
thf(func_def_632,type,
sK275: produc1368416213on_val > produc2088785539on_val ).
thf(func_def_633,type,
sK276: produc1368416213on_val > list_char ).
thf(func_def_634,type,
sK277: produc1368416213on_val > produc1278157519t_char > option_val ).
thf(func_def_635,type,
sK278: produc1350825965t_char > produc1278157519t_char ).
thf(func_def_636,type,
sK279: produc1350825965t_char > list_char ).
thf(func_def_637,type,
sK280: produc1350825965t_char > list_char ).
thf(func_def_638,type,
sK281: produc630464863al_val > produc1645268488al_val ).
thf(func_def_639,type,
sK282: produc630464863al_val > bop ).
thf(func_def_640,type,
sK283: produc630464863al_val > product_prod_val_val ).
thf(func_def_641,type,
sK284: produc800118557al_val > product_prod_val_val ).
thf(func_def_642,type,
sK285: produc800118557al_val > val ).
thf(func_def_643,type,
sK286: produc800118557al_val > val ).
thf(func_def_644,type,
sK287: produc1250491293on_val > produc618524391on_val ).
thf(func_def_645,type,
sK288: produc1250491293on_val > produc1180562163on_val ).
thf(func_def_646,type,
sK289: produc1250491293on_val > produc1180562163on_val ).
thf(func_def_647,type,
sK290: produc349695911t_char > produc1285161482t_char ).
thf(func_def_648,type,
sK291: produc349695911t_char > list_list_char ).
thf(func_def_649,type,
sK292: produc349695911t_char > produc220283002t_char ).
thf(func_def_650,type,
sK293: produc1406897475t_char > produc220283002t_char ).
thf(func_def_651,type,
sK294: produc1406897475t_char > list_ty ).
thf(func_def_652,type,
sK295: produc1406897475t_char > produc662261637t_char ).
thf(func_def_653,type,
sK296: produc1826280281t_char > produc662261637t_char ).
thf(func_def_654,type,
sK297: produc1826280281t_char > list_val ).
thf(func_def_655,type,
sK298: produc1826280281t_char > exp_list_char ).
thf(func_def_656,type,
sK299: produc84451751t_char > produc1971331930t_char ).
thf(func_def_657,type,
sK300: produc84451751t_char > list_char ).
thf(func_def_658,type,
sK301: produc84451751t_char > produc952412819t_char ).
thf(func_def_659,type,
sK302: produc740765671t_char > produc952412819t_char ).
thf(func_def_660,type,
sK303: produc740765671t_char > list_char ).
thf(func_def_661,type,
sK304: produc740765671t_char > produc2146869324t_char ).
thf(func_def_662,type,
sK305: produc494726439t_char > produc2146869324t_char ).
thf(func_def_663,type,
sK306: produc494726439t_char > list_P1940453997har_ty ).
thf(func_def_664,type,
sK307: produc494726439t_char > list_P341299826t_char ).
thf(func_def_665,type,
sK308: produc1534059751t_char > produc809539159t_char ).
thf(func_def_666,type,
sK309: produc1534059751t_char > list_list_char ).
thf(func_def_667,type,
sK310: produc1534059751t_char > exp_list_char ).
thf(func_def_668,type,
sK311: ( produc1013743697t_char > $o ) > list_char ).
thf(func_def_669,type,
sK312: ( produc1013743697t_char > $o ) > list_ty ).
thf(func_def_670,type,
sK313: ( produc1013743697t_char > $o ) > produc1059328077t_char ).
thf(func_def_671,type,
sK314: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_672,type,
sK315: ( produc1746408499on_val > $o ) > exp_list_char ).
thf(func_def_673,type,
sK316: ( produc1746408499on_val > $o ) > produc2090907612on_val ).
thf(func_def_674,type,
sK317: ( produc1282892786on_val > $o ) > exp_list_char ).
thf(func_def_675,type,
sK318: ( produc1282892786on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_676,type,
sK319: ( produc1282892786on_val > $o ) > list_char > option_val ).
thf(func_def_677,type,
sK320: ( produc1645268488al_val > $o ) > bop ).
thf(func_def_678,type,
sK321: ( produc1645268488al_val > $o ) > val ).
thf(func_def_679,type,
sK322: ( produc1645268488al_val > $o ) > val ).
thf(func_def_680,type,
sK323: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_681,type,
sK324: ( produc618524391on_val > $o ) > list_exp_list_char ).
thf(func_def_682,type,
sK325: ( produc618524391on_val > $o ) > produc2090907612on_val ).
thf(func_def_683,type,
sK326: ( produc1180562163on_val > $o ) > list_exp_list_char ).
thf(func_def_684,type,
sK327: ( produc1180562163on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_685,type,
sK328: ( produc1180562163on_val > $o ) > list_char > option_val ).
thf(func_def_686,type,
sK329: ( produc1285161482t_char > $o ) > list_list_char ).
thf(func_def_687,type,
sK330: ( produc1285161482t_char > $o ) > list_ty ).
thf(func_def_688,type,
sK331: ( produc1285161482t_char > $o ) > produc662261637t_char ).
thf(func_def_689,type,
sK332: ( produc220283002t_char > $o ) > list_ty ).
thf(func_def_690,type,
sK333: ( produc220283002t_char > $o ) > list_val ).
thf(func_def_691,type,
sK334: ( produc220283002t_char > $o ) > exp_list_char ).
thf(func_def_692,type,
sK335: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_693,type,
sK336: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_694,type,
sK337: ( produc1971331930t_char > $o ) > produc2146869324t_char ).
thf(func_def_695,type,
sK338: ( produc952412819t_char > $o ) > list_char ).
thf(func_def_696,type,
sK339: ( produc952412819t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_697,type,
sK340: ( produc952412819t_char > $o ) > list_P341299826t_char ).
thf(func_def_698,type,
sK341: ( produc652964533on_val > $o ) > produc1746408499on_val ).
thf(func_def_699,type,
sK342: ( produc652964533on_val > $o ) > produc1282892786on_val ).
thf(func_def_700,type,
sK343: ( produc652964533on_val > $o ) > produc1282892786on_val ).
thf(func_def_701,type,
sK344: ( produc1581780743on_val > $o ) > produc2090907612on_val ).
thf(func_def_702,type,
sK345: ( produc1581780743on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_703,type,
sK346: ( produc1581780743on_val > $o ) > list_char > option_val ).
thf(func_def_704,type,
sK347: ( produc1368416213on_val > $o ) > produc2088785539on_val ).
thf(func_def_705,type,
sK348: ( produc1368416213on_val > $o ) > list_char ).
thf(func_def_706,type,
sK349: ( produc1368416213on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_707,type,
sK350: ( produc1350825965t_char > $o ) > produc1278157519t_char ).
thf(func_def_708,type,
sK351: ( produc1350825965t_char > $o ) > list_char ).
thf(func_def_709,type,
sK352: ( produc1350825965t_char > $o ) > list_char ).
thf(func_def_710,type,
sK353: ( produc630464863al_val > $o ) > produc1645268488al_val ).
thf(func_def_711,type,
sK354: ( produc630464863al_val > $o ) > bop ).
thf(func_def_712,type,
sK355: ( produc630464863al_val > $o ) > product_prod_val_val ).
thf(func_def_713,type,
sK356: ( produc800118557al_val > $o ) > product_prod_val_val ).
thf(func_def_714,type,
sK357: ( produc800118557al_val > $o ) > val ).
thf(func_def_715,type,
sK358: ( produc800118557al_val > $o ) > val ).
thf(func_def_716,type,
sK359: ( produc1250491293on_val > $o ) > produc618524391on_val ).
thf(func_def_717,type,
sK360: ( produc1250491293on_val > $o ) > produc1180562163on_val ).
thf(func_def_718,type,
sK361: ( produc1250491293on_val > $o ) > produc1180562163on_val ).
thf(func_def_719,type,
sK362: ( produc349695911t_char > $o ) > produc1285161482t_char ).
thf(func_def_720,type,
sK363: ( produc349695911t_char > $o ) > list_list_char ).
thf(func_def_721,type,
sK364: ( produc349695911t_char > $o ) > produc220283002t_char ).
thf(func_def_722,type,
sK365: ( produc1406897475t_char > $o ) > produc220283002t_char ).
thf(func_def_723,type,
sK366: ( produc1406897475t_char > $o ) > list_ty ).
thf(func_def_724,type,
sK367: ( produc1406897475t_char > $o ) > produc662261637t_char ).
thf(func_def_725,type,
sK368: ( produc1826280281t_char > $o ) > produc662261637t_char ).
thf(func_def_726,type,
sK369: ( produc1826280281t_char > $o ) > list_val ).
thf(func_def_727,type,
sK370: ( produc1826280281t_char > $o ) > exp_list_char ).
thf(func_def_728,type,
sK371: ( produc84451751t_char > $o ) > produc1971331930t_char ).
thf(func_def_729,type,
sK372: ( produc84451751t_char > $o ) > list_char ).
thf(func_def_730,type,
sK373: ( produc84451751t_char > $o ) > produc952412819t_char ).
thf(func_def_731,type,
sK374: ( produc740765671t_char > $o ) > produc952412819t_char ).
thf(func_def_732,type,
sK375: ( produc740765671t_char > $o ) > list_char ).
thf(func_def_733,type,
sK376: ( produc740765671t_char > $o ) > produc2146869324t_char ).
thf(func_def_734,type,
sK377: ( produc494726439t_char > $o ) > produc2146869324t_char ).
thf(func_def_735,type,
sK378: ( produc494726439t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_736,type,
sK379: ( produc494726439t_char > $o ) > list_P341299826t_char ).
thf(func_def_737,type,
sK380: ( produc1534059751t_char > $o ) > produc809539159t_char ).
thf(func_def_738,type,
sK381: ( produc1534059751t_char > $o ) > list_list_char ).
thf(func_def_739,type,
sK382: ( produc1534059751t_char > $o ) > exp_list_char ).
thf(func_def_740,type,
sK383: ( produc91527719t_char > $o ) > ( produc91527719t_char > $o ) > list_exp_list_char ).
thf(func_def_741,type,
sK384: ( produc91527719t_char > $o ) > ( produc91527719t_char > $o ) > list_exp_list_char ).
thf(func_def_742,type,
sK385: ( produc2048519645t_char > $o ) > ( produc2048519645t_char > $o ) > exp_list_char ).
thf(func_def_743,type,
sK386: ( produc2048519645t_char > $o ) > ( produc2048519645t_char > $o ) > exp_list_char ).
thf(func_def_744,type,
sK387: ( produc1200003175t_char > $o ) > ( produc1200003175t_char > $o ) > list_list_char ).
thf(func_def_745,type,
sK388: ( produc1200003175t_char > $o ) > ( produc1200003175t_char > $o ) > list_list_char ).
thf(func_def_746,type,
sK389: ( produc450000425har_ty > $o ) > ( produc450000425har_ty > $o ) > list_P1940453997har_ty ).
thf(func_def_747,type,
sK390: ( produc450000425har_ty > $o ) > ( produc450000425har_ty > $o ) > list_P1940453997har_ty ).
thf(func_def_748,type,
sK391: ( produc244676007t_char > $o ) > ( produc244676007t_char > $o ) > list_P341299826t_char ).
thf(func_def_749,type,
sK392: ( produc244676007t_char > $o ) > ( produc244676007t_char > $o ) > list_P341299826t_char ).
thf(func_def_750,type,
sK393: ( produc753553453st_val > $o ) > ( produc753553453st_val > $o ) > list_val ).
thf(func_def_751,type,
sK394: ( produc753553453st_val > $o ) > ( produc753553453st_val > $o ) > list_val ).
thf(func_def_752,type,
sK395: ( produc1420746395ist_ty > $o ) > ( produc1420746395ist_ty > $o ) > list_ty ).
thf(func_def_753,type,
sK396: ( produc1420746395ist_ty > $o ) > ( produc1420746395ist_ty > $o ) > list_ty ).
thf(func_def_754,type,
sK397: ( product_prod_bop_bop > $o ) > ( product_prod_bop_bop > $o ) > bop ).
thf(func_def_755,type,
sK398: ( product_prod_bop_bop > $o ) > ( product_prod_bop_bop > $o ) > bop ).
thf(func_def_756,type,
sK399: ( produc688860215on_val > $o ) > ( produc688860215on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_757,type,
sK400: ( produc688860215on_val > $o ) > ( produc688860215on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_758,type,
sK401: ( produc1287081631on_val > $o ) > ( produc1287081631on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_759,type,
sK402: ( produc1287081631on_val > $o ) > ( produc1287081631on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_760,type,
sK403: ( produc774316953on_val > $o ) > ( produc774316953on_val > $o ) > list_char > option_val ).
thf(func_def_761,type,
sK404: ( produc774316953on_val > $o ) > ( produc774316953on_val > $o ) > list_char > option_val ).
thf(func_def_762,type,
sK405: ( produc1282892786on_val > $o ) > ( produc1282892786on_val > $o ) > exp_list_char ).
thf(func_def_763,type,
sK406: ( produc1282892786on_val > $o ) > ( produc1282892786on_val > $o ) > produc2090907612on_val ).
thf(func_def_764,type,
sK407: ( produc2090907612on_val > $o ) > ( produc2090907612on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_765,type,
sK408: ( produc2090907612on_val > $o ) > ( produc2090907612on_val > $o ) > list_char > option_val ).
thf(func_def_766,type,
sK409: ( produc2088785539on_val > $o ) > ( produc2088785539on_val > $o ) > list_char ).
thf(func_def_767,type,
sK410: ( produc2088785539on_val > $o ) > ( produc2088785539on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_768,type,
sK411: ( produc1645268488al_val > $o ) > ( produc1645268488al_val > $o ) > bop ).
thf(func_def_769,type,
sK412: ( produc1645268488al_val > $o ) > ( produc1645268488al_val > $o ) > product_prod_val_val ).
thf(func_def_770,type,
sK413: ( product_prod_val_val > $o ) > ( product_prod_val_val > $o ) > val ).
thf(func_def_771,type,
sK414: ( product_prod_val_val > $o ) > ( product_prod_val_val > $o ) > val ).
thf(func_def_772,type,
sK415: ( produc1180562163on_val > $o ) > ( produc1180562163on_val > $o ) > list_exp_list_char ).
thf(func_def_773,type,
sK416: ( produc1180562163on_val > $o ) > ( produc1180562163on_val > $o ) > produc2090907612on_val ).
thf(func_def_774,type,
sK417: ( produc1285161482t_char > $o ) > ( produc1285161482t_char > $o ) > list_list_char ).
thf(func_def_775,type,
sK418: ( produc1285161482t_char > $o ) > ( produc1285161482t_char > $o ) > produc220283002t_char ).
thf(func_def_776,type,
sK419: ( produc220283002t_char > $o ) > ( produc220283002t_char > $o ) > list_ty ).
thf(func_def_777,type,
sK420: ( produc220283002t_char > $o ) > ( produc220283002t_char > $o ) > produc662261637t_char ).
thf(func_def_778,type,
sK421: ( produc662261637t_char > $o ) > ( produc662261637t_char > $o ) > list_val ).
thf(func_def_779,type,
sK422: ( produc662261637t_char > $o ) > ( produc662261637t_char > $o ) > exp_list_char ).
thf(func_def_780,type,
sK423: ( produc952412819t_char > $o ) > ( produc952412819t_char > $o ) > list_char ).
thf(func_def_781,type,
sK424: ( produc952412819t_char > $o ) > ( produc952412819t_char > $o ) > produc2146869324t_char ).
thf(func_def_782,type,
sK425: ( produc2146869324t_char > $o ) > ( produc2146869324t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_783,type,
sK426: ( produc2146869324t_char > $o ) > ( produc2146869324t_char > $o ) > list_P341299826t_char ).
thf(func_def_784,type,
sK427: ( produc809539159t_char > $o ) > ( produc809539159t_char > $o ) > list_list_char ).
thf(func_def_785,type,
sK428: ( produc809539159t_char > $o ) > ( produc809539159t_char > $o ) > exp_list_char ).
thf(func_def_786,type,
sK429: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_787,type,
sK430: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_788,type,
sK431: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_789,type,
sK432: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_790,type,
sK433: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_791,type,
sK434: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_792,type,
sK435: ( produc1971331930t_char > $o ) > ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_793,type,
sK436: ( produc1971331930t_char > $o ) > ( produc1971331930t_char > $o ) > produc952412819t_char ).
thf(func_def_794,type,
sK437: ( produc1013743697t_char > $o ) > ( produc1013743697t_char > $o ) > list_char ).
thf(func_def_795,type,
sK438: ( produc1013743697t_char > $o ) > ( produc1013743697t_char > $o ) > produc1025221954t_char ).
thf(func_def_796,type,
sK439: produc809539159t_char > list_list_char ).
thf(func_def_797,type,
sK440: produc809539159t_char > exp_list_char ).
thf(func_def_798,type,
sK441: produc2146869324t_char > list_P1940453997har_ty ).
thf(func_def_799,type,
sK442: produc2146869324t_char > list_P341299826t_char ).
thf(func_def_800,type,
sK443: produc952412819t_char > list_char ).
thf(func_def_801,type,
sK444: produc952412819t_char > produc2146869324t_char ).
thf(func_def_802,type,
sK445: produc1971331930t_char > list_char ).
thf(func_def_803,type,
sK446: produc1971331930t_char > produc952412819t_char ).
thf(func_def_804,type,
sK447: produc662261637t_char > list_val ).
thf(func_def_805,type,
sK448: produc662261637t_char > exp_list_char ).
thf(func_def_806,type,
sK449: produc220283002t_char > list_ty ).
thf(func_def_807,type,
sK450: produc220283002t_char > produc662261637t_char ).
thf(func_def_808,type,
sK451: produc1285161482t_char > list_list_char ).
thf(func_def_809,type,
sK452: produc1285161482t_char > produc220283002t_char ).
thf(func_def_810,type,
sK453: produc1180562163on_val > list_exp_list_char ).
thf(func_def_811,type,
sK454: produc1180562163on_val > produc2090907612on_val ).
thf(func_def_812,type,
sK455: produc618524391on_val > produc1180562163on_val ).
thf(func_def_813,type,
sK456: produc618524391on_val > produc1180562163on_val ).
thf(func_def_814,type,
sK457: product_prod_val_val > val ).
thf(func_def_815,type,
sK458: product_prod_val_val > val ).
thf(func_def_816,type,
sK459: produc1645268488al_val > bop ).
thf(func_def_817,type,
sK460: produc1645268488al_val > product_prod_val_val ).
thf(func_def_818,type,
sK461: produc1278157519t_char > list_char ).
thf(func_def_819,type,
sK462: produc1278157519t_char > list_char ).
thf(func_def_820,type,
sK463: produc2088785539on_val > list_char ).
thf(func_def_821,type,
sK464: produc2088785539on_val > produc1278157519t_char > option_val ).
thf(func_def_822,type,
sK465: produc2090907612on_val > nat > option1728594148on_val ).
thf(func_def_823,type,
sK466: produc2090907612on_val > list_char > option_val ).
thf(func_def_824,type,
sK467: produc1282892786on_val > exp_list_char ).
thf(func_def_825,type,
sK468: produc1282892786on_val > produc2090907612on_val ).
thf(func_def_826,type,
sK469: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_827,type,
sK470: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_828,type,
sK471: produc809539159t_char > list_list_char ).
thf(func_def_829,type,
sK472: produc809539159t_char > exp_list_char ).
thf(func_def_830,type,
sK473: produc2146869324t_char > list_P1940453997har_ty ).
thf(func_def_831,type,
sK474: produc2146869324t_char > list_P341299826t_char ).
thf(func_def_832,type,
sK475: produc952412819t_char > list_char ).
thf(func_def_833,type,
sK476: produc952412819t_char > produc2146869324t_char ).
thf(func_def_834,type,
sK477: produc1971331930t_char > list_char ).
thf(func_def_835,type,
sK478: produc1971331930t_char > produc952412819t_char ).
thf(func_def_836,type,
sK479: produc662261637t_char > list_val ).
thf(func_def_837,type,
sK480: produc662261637t_char > exp_list_char ).
thf(func_def_838,type,
sK481: produc220283002t_char > list_ty ).
thf(func_def_839,type,
sK482: produc220283002t_char > produc662261637t_char ).
thf(func_def_840,type,
sK483: produc1285161482t_char > list_list_char ).
thf(func_def_841,type,
sK484: produc1285161482t_char > produc220283002t_char ).
thf(func_def_842,type,
sK485: produc1180562163on_val > list_exp_list_char ).
thf(func_def_843,type,
sK486: produc1180562163on_val > produc2090907612on_val ).
thf(func_def_844,type,
sK487: produc618524391on_val > produc1180562163on_val ).
thf(func_def_845,type,
sK488: produc618524391on_val > produc1180562163on_val ).
thf(func_def_846,type,
sK489: product_prod_val_val > val ).
thf(func_def_847,type,
sK490: product_prod_val_val > val ).
thf(func_def_848,type,
sK491: produc1645268488al_val > bop ).
thf(func_def_849,type,
sK492: produc1645268488al_val > product_prod_val_val ).
thf(func_def_850,type,
sK493: produc1278157519t_char > list_char ).
thf(func_def_851,type,
sK494: produc1278157519t_char > list_char ).
thf(func_def_852,type,
sK495: produc2088785539on_val > list_char ).
thf(func_def_853,type,
sK496: produc2088785539on_val > produc1278157519t_char > option_val ).
thf(func_def_854,type,
sK497: produc2090907612on_val > nat > option1728594148on_val ).
thf(func_def_855,type,
sK498: produc2090907612on_val > list_char > option_val ).
thf(func_def_856,type,
sK499: produc1282892786on_val > exp_list_char ).
thf(func_def_857,type,
sK500: produc1282892786on_val > produc2090907612on_val ).
thf(func_def_858,type,
sK501: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_859,type,
sK502: produc1746408499on_val > produc1282892786on_val ).
thf(func_def_860,type,
sK503: ( produc809539159t_char > $o ) > list_list_char ).
thf(func_def_861,type,
sK504: ( produc809539159t_char > $o ) > exp_list_char ).
thf(func_def_862,type,
sK505: ( produc2146869324t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_863,type,
sK506: ( produc2146869324t_char > $o ) > list_P341299826t_char ).
thf(func_def_864,type,
sK507: ( produc952412819t_char > $o ) > list_char ).
thf(func_def_865,type,
sK508: ( produc952412819t_char > $o ) > produc2146869324t_char ).
thf(func_def_866,type,
sK509: ( produc1971331930t_char > $o ) > list_char ).
thf(func_def_867,type,
sK510: ( produc1971331930t_char > $o ) > produc952412819t_char ).
thf(func_def_868,type,
sK511: ( produc662261637t_char > $o ) > list_val ).
thf(func_def_869,type,
sK512: ( produc662261637t_char > $o ) > exp_list_char ).
thf(func_def_870,type,
sK513: ( produc220283002t_char > $o ) > list_ty ).
thf(func_def_871,type,
sK514: ( produc220283002t_char > $o ) > produc662261637t_char ).
thf(func_def_872,type,
sK515: ( produc1285161482t_char > $o ) > list_list_char ).
thf(func_def_873,type,
sK516: ( produc1285161482t_char > $o ) > produc220283002t_char ).
thf(func_def_874,type,
sK517: ( produc1180562163on_val > $o ) > list_exp_list_char ).
thf(func_def_875,type,
sK518: ( produc1180562163on_val > $o ) > produc2090907612on_val ).
thf(func_def_876,type,
sK519: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_877,type,
sK520: ( produc618524391on_val > $o ) > produc1180562163on_val ).
thf(func_def_878,type,
sK521: ( product_prod_val_val > $o ) > val ).
thf(func_def_879,type,
sK522: ( product_prod_val_val > $o ) > val ).
thf(func_def_880,type,
sK523: ( produc1645268488al_val > $o ) > bop ).
thf(func_def_881,type,
sK524: ( produc1645268488al_val > $o ) > product_prod_val_val ).
thf(func_def_882,type,
sK525: ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_883,type,
sK526: ( produc1278157519t_char > $o ) > list_char ).
thf(func_def_884,type,
sK527: ( produc2088785539on_val > $o ) > list_char ).
thf(func_def_885,type,
sK528: ( produc2088785539on_val > $o ) > produc1278157519t_char > option_val ).
thf(func_def_886,type,
sK529: ( produc2090907612on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_887,type,
sK530: ( produc2090907612on_val > $o ) > list_char > option_val ).
thf(func_def_888,type,
sK531: ( produc1282892786on_val > $o ) > exp_list_char ).
thf(func_def_889,type,
sK532: ( produc1282892786on_val > $o ) > produc2090907612on_val ).
thf(func_def_890,type,
sK533: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_891,type,
sK534: ( produc1746408499on_val > $o ) > produc1282892786on_val ).
thf(func_def_892,type,
sK535: produc809539159t_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_893,type,
sK536: produc809539159t_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_894,type,
sK537: produc2146869324t_char > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_895,type,
sK538: produc2146869324t_char > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_896,type,
sK539: produc952412819t_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_897,type,
sK540: produc952412819t_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_898,type,
sK541: produc1971331930t_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_899,type,
sK542: produc1971331930t_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_900,type,
sK543: produc662261637t_char > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_901,type,
sK544: produc662261637t_char > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_902,type,
sK545: produc220283002t_char > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_903,type,
sK546: produc220283002t_char > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_904,type,
sK547: produc1285161482t_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_905,type,
sK548: produc1285161482t_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_906,type,
sK549: produc1180562163on_val > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_907,type,
sK550: produc1180562163on_val > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_908,type,
sK551: produc618524391on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_909,type,
sK552: produc618524391on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_910,type,
sK553: product_prod_val_val > ( val > val > $o ) > val ).
thf(func_def_911,type,
sK554: product_prod_val_val > ( val > val > $o ) > val ).
thf(func_def_912,type,
sK555: produc1645268488al_val > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_913,type,
sK556: produc1645268488al_val > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_914,type,
sK557: produc1278157519t_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_915,type,
sK558: produc1278157519t_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_916,type,
sK559: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_917,type,
sK560: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_918,type,
sK561: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_919,type,
sK562: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_920,type,
sK563: produc1282892786on_val > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_921,type,
sK564: produc1282892786on_val > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_922,type,
sK565: produc1746408499on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_923,type,
sK566: produc1746408499on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_924,type,
sK567: produc809539159t_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_925,type,
sK568: produc809539159t_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_926,type,
sK569: produc2146869324t_char > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_927,type,
sK570: produc2146869324t_char > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_928,type,
sK571: produc952412819t_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_929,type,
sK572: produc952412819t_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_930,type,
sK573: produc1971331930t_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_931,type,
sK574: produc1971331930t_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_932,type,
sK575: produc662261637t_char > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_933,type,
sK576: produc662261637t_char > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_934,type,
sK577: produc220283002t_char > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_935,type,
sK578: produc220283002t_char > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_936,type,
sK579: produc1285161482t_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_937,type,
sK580: produc1285161482t_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_938,type,
sK581: produc1180562163on_val > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_939,type,
sK582: produc1180562163on_val > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_940,type,
sK583: produc618524391on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_941,type,
sK584: produc618524391on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_942,type,
sK585: product_prod_val_val > ( val > val > $o ) > val ).
thf(func_def_943,type,
sK586: product_prod_val_val > ( val > val > $o ) > val ).
thf(func_def_944,type,
sK587: produc1645268488al_val > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_945,type,
sK588: produc1645268488al_val > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_946,type,
sK589: produc1278157519t_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_947,type,
sK590: produc1278157519t_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_948,type,
sK591: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_949,type,
sK592: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_950,type,
sK593: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_951,type,
sK594: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_952,type,
sK595: produc1282892786on_val > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_953,type,
sK596: produc1282892786on_val > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_954,type,
sK597: produc1746408499on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_955,type,
sK598: produc1746408499on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_956,type,
sK599: ( list_char > option_ty ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > list_char ).
thf(func_def_957,type,
sK600: ( list_char > option_ty ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > val ).
thf(func_def_958,type,
sK601: val > list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_959,type,
sK602: ( produc2088785539on_val > option_ty ) > ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > list_char ).
thf(func_def_960,type,
sK603: ( produc2088785539on_val > option_ty ) > ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > produc1278157519t_char > option_val ).
thf(func_def_961,type,
sK604: ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > ( produc2090907612on_val > $o ) > nat > option1728594148on_val ).
thf(func_def_962,type,
sK605: ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > ( produc2090907612on_val > $o ) > list_char > option_val ).
thf(func_def_963,type,
sK606: ( nat > option1728594148on_val ) > nat > produc2088785539on_val ).
thf(func_def_964,type,
sK607: ( list_char > option_val ) > list_char > val ).
thf(func_def_965,type,
sK608: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > ( option_ty > $o ) > list_char ).
thf(func_def_966,type,
sK609: produc2088785539on_val > ( list_char > ( produc1278157519t_char > option_val ) > option_ty ) > ( option_ty > $o ) > produc1278157519t_char > option_val ).
thf(func_def_967,type,
sK610: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > ( $o > $o ) > nat > option1728594148on_val ).
thf(func_def_968,type,
sK611: produc2090907612on_val > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > ( $o > $o ) > list_char > option_val ).
thf(func_def_969,type,
sK612: ( nat > option1728594148on_val ) > list_char > nat > produc1278157519t_char > option_val ).
thf(func_def_970,type,
sK613: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > nat ).
thf(func_def_971,type,
sK614: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > list_char ).
thf(func_def_972,type,
sK615: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > produc1278157519t_char > option_val ).
thf(func_def_973,type,
sK616: list_char > nat > ( nat > option1728594148on_val ) > produc1278157519t_char > option_val ).
thf(func_def_974,type,
sK617: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > nat ).
thf(func_def_975,type,
sK618: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > list_char ).
thf(func_def_976,type,
sK619: ( nat > option1728594148on_val ) > ( nat > option1728594148on_val ) > produc1278157519t_char > option_val ).
thf(func_def_977,type,
sK620: option_nat > nat ).
thf(func_def_978,type,
sK621: option_ty > ty ).
thf(func_def_979,type,
sK622: option1728594148on_val > produc2088785539on_val ).
thf(func_def_980,type,
sK623: option_val > val ).
thf(func_def_981,type,
sK624: option_list_char_o > list_char > $o ).
thf(func_def_982,type,
sK625: option_nat > nat ).
thf(func_def_983,type,
sK626: option_ty > ty ).
thf(func_def_984,type,
sK627: option1728594148on_val > produc2088785539on_val ).
thf(func_def_985,type,
sK628: option_val > val ).
thf(func_def_986,type,
sK629: option_list_char_o > list_char > $o ).
thf(func_def_987,type,
sK630: val > produc1278157519t_char > ( produc1278157519t_char > option_val ) > produc1278157519t_char ).
thf(func_def_988,type,
sK631: produc2088785539on_val > nat > ( nat > option1728594148on_val ) > nat ).
thf(func_def_989,type,
sK632: ty > list_char > ( list_char > option_ty ) > list_char ).
thf(func_def_990,type,
sK633: val > list_char > ( list_char > option_val ) > list_char ).
thf(func_def_991,type,
sK634: exp_list_char > list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_992,type,
sK635: exp_list_char > list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_993,type,
sK636: exp_list_char > list_char > val ).
thf(func_def_994,type,
sK637: exp_list_char > list_char > exp_list_char ).
thf(func_def_995,type,
sK638: ( produc1013743697t_char > $o ) > ( produc1013743697t_char > $o ) > produc1013743697t_char ).
thf(func_def_996,type,
sK639: ( produc1971331930t_char > $o ) > ( produc1971331930t_char > $o ) > produc1971331930t_char ).
thf(func_def_997,type,
sK640: ( produc618524391on_val > $o ) > ( produc618524391on_val > $o ) > produc618524391on_val ).
thf(func_def_998,type,
sK641: ( nat > $o ) > ( nat > $o ) > nat ).
thf(func_def_999,type,
sK642: ( produc1278157519t_char > $o ) > ( produc1278157519t_char > $o ) > produc1278157519t_char ).
thf(func_def_1000,type,
sK643: ( list_char > $o ) > ( list_char > $o ) > list_char ).
thf(func_def_1001,type,
sK644: ( produc1746408499on_val > $o ) > ( produc1746408499on_val > $o ) > produc1746408499on_val ).
thf(func_def_1002,type,
sK645: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > list_exp_list_char ).
thf(func_def_1003,type,
sK646: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > produc2090907612on_val ).
thf(func_def_1004,type,
sK647: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char ).
thf(func_def_1005,type,
sK648: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > produc2090907612on_val ).
thf(func_def_1006,type,
sK649: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > exp_list_char > list_list_char > list_list_char ).
thf(func_def_1007,type,
sK650: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > exp_list_char > list_list_char > exp_list_char ).
thf(func_def_1008,type,
sK651: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > list_P341299826t_char > list_P1940453997har_ty > list_P1940453997har_ty ).
thf(func_def_1009,type,
sK652: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > list_P341299826t_char > list_P1940453997har_ty > list_P341299826t_char ).
thf(func_def_1010,type,
sK653: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > produc2146869324t_char > list_char > list_char ).
thf(func_def_1011,type,
sK654: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > produc2146869324t_char > list_char > produc2146869324t_char ).
thf(func_def_1012,type,
sK655: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > produc952412819t_char > list_char > list_char ).
thf(func_def_1013,type,
sK656: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > produc952412819t_char > list_char > produc952412819t_char ).
thf(func_def_1014,type,
sK657: ( produc1826280281t_char > $o ) > exp_list_char > list_val > exp_list_char > list_val > list_val ).
thf(func_def_1015,type,
sK658: ( produc1826280281t_char > $o ) > exp_list_char > list_val > exp_list_char > list_val > exp_list_char ).
thf(func_def_1016,type,
sK659: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > produc662261637t_char > list_ty > list_ty ).
thf(func_def_1017,type,
sK660: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > produc662261637t_char > list_ty > produc662261637t_char ).
thf(func_def_1018,type,
sK661: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > produc220283002t_char > list_list_char > list_list_char ).
thf(func_def_1019,type,
sK662: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > produc220283002t_char > list_list_char > produc220283002t_char ).
thf(func_def_1020,type,
sK663: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val ).
thf(func_def_1021,type,
sK664: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val ).
thf(func_def_1022,type,
sK665: ( produc800118557al_val > $o ) > val > val > val > val > val ).
thf(func_def_1023,type,
sK666: ( produc800118557al_val > $o ) > val > val > val > val > val ).
thf(func_def_1024,type,
sK667: ( produc630464863al_val > $o ) > product_prod_val_val > bop > product_prod_val_val > bop > bop ).
thf(func_def_1025,type,
sK668: ( produc630464863al_val > $o ) > product_prod_val_val > bop > product_prod_val_val > bop > product_prod_val_val ).
thf(func_def_1026,type,
sK669: ( produc1350825965t_char > $o ) > list_char > list_char > list_char > list_char > list_char ).
thf(func_def_1027,type,
sK670: ( produc1350825965t_char > $o ) > list_char > list_char > list_char > list_char > list_char ).
thf(func_def_1028,type,
sK671: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( produc1278157519t_char > option_val ) > list_char > list_char ).
thf(func_def_1029,type,
sK672: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( produc1278157519t_char > option_val ) > list_char > produc1278157519t_char > option_val ).
thf(func_def_1030,type,
sK673: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > nat > option1728594148on_val ).
thf(func_def_1031,type,
sK674: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > list_char > option_val ).
thf(func_def_1032,type,
sK675: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val ).
thf(func_def_1033,type,
sK676: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val ).
thf(func_def_1034,type,
sK677: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_1035,type,
sK678: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1036,type,
sK679: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_1037,type,
sK680: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1038,type,
sK681: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_1039,type,
sK682: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1040,type,
sK683: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_1041,type,
sK684: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1042,type,
sK685: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_1043,type,
sK686: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1044,type,
sK687: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_1045,type,
sK688: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1046,type,
sK689: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_1047,type,
sK690: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_1048,type,
sK691: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_1049,type,
sK692: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_1050,type,
sK693: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_1051,type,
sK694: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1052,type,
sK695: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_1053,type,
sK696: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1054,type,
sK697: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_1055,type,
sK698: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1056,type,
sK699: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_1057,type,
sK700: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1058,type,
sK701: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_1059,type,
sK702: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1060,type,
sK703: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_1061,type,
sK704: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1062,type,
sK705: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_1063,type,
sK706: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1064,type,
sK707: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_1065,type,
sK708: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1066,type,
sK709: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_1067,type,
sK710: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1068,type,
sK711: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_1069,type,
sK712: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1070,type,
sK713: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1071,type,
sK714: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1072,type,
sK715: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1073,type,
sK716: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1074,type,
sK717: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1075,type,
sK718: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1076,type,
sK719: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1077,type,
sK720: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1078,type,
sK721: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_1079,type,
sK722: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1080,type,
sK723: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_1081,type,
sK724: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1082,type,
sK725: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1083,type,
sK726: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1084,type,
sK727: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1085,type,
sK728: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1086,type,
sK729: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_1087,type,
sK730: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_1088,type,
sK731: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_1089,type,
sK732: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_1090,type,
sK733: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_1091,type,
sK734: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_1092,type,
sK735: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_1093,type,
sK736: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_1094,type,
sK737: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1095,type,
sK738: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1096,type,
sK739: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1097,type,
sK740: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1098,type,
sK741: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_1099,type,
sK742: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1100,type,
sK743: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > list_exp_list_char ).
thf(func_def_1101,type,
sK744: ( produc618524391on_val > $o ) > produc2090907612on_val > list_exp_list_char > ( list_exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1102,type,
sK745: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_1103,type,
sK746: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1104,type,
sK747: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > exp_list_char ).
thf(func_def_1105,type,
sK748: ( produc1746408499on_val > $o ) > produc2090907612on_val > exp_list_char > ( exp_list_char > produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1106,type,
sK749: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_1107,type,
sK750: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1108,type,
sK751: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > list_list_char ).
thf(func_def_1109,type,
sK752: ( produc1534059751t_char > $o ) > exp_list_char > list_list_char > ( list_list_char > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1110,type,
sK753: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_1111,type,
sK754: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_1112,type,
sK755: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P1940453997har_ty ).
thf(func_def_1113,type,
sK756: ( produc494726439t_char > $o ) > list_P341299826t_char > list_P1940453997har_ty > ( list_P1940453997har_ty > list_P341299826t_char > $o ) > list_P341299826t_char ).
thf(func_def_1114,type,
sK757: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_1115,type,
sK758: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1116,type,
sK759: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > list_char ).
thf(func_def_1117,type,
sK760: ( produc740765671t_char > $o ) > produc2146869324t_char > list_char > ( list_char > produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1118,type,
sK761: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_1119,type,
sK762: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1120,type,
sK763: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > list_char ).
thf(func_def_1121,type,
sK764: ( produc84451751t_char > $o ) > produc952412819t_char > list_char > ( list_char > produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1122,type,
sK765: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_1123,type,
sK766: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1124,type,
sK767: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > list_val ).
thf(func_def_1125,type,
sK768: ( produc1826280281t_char > $o ) > exp_list_char > list_val > ( list_val > exp_list_char > $o ) > exp_list_char ).
thf(func_def_1126,type,
sK769: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_1127,type,
sK770: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1128,type,
sK771: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > list_ty ).
thf(func_def_1129,type,
sK772: ( produc1406897475t_char > $o ) > produc662261637t_char > list_ty > ( list_ty > produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1130,type,
sK773: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_1131,type,
sK774: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1132,type,
sK775: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > list_list_char ).
thf(func_def_1133,type,
sK776: ( produc349695911t_char > $o ) > produc220283002t_char > list_list_char > ( list_list_char > produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1134,type,
sK777: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1135,type,
sK778: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1136,type,
sK779: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1137,type,
sK780: ( produc1250491293on_val > $o ) > produc1180562163on_val > produc1180562163on_val > ( produc1180562163on_val > produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1138,type,
sK781: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1139,type,
sK782: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1140,type,
sK783: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1141,type,
sK784: ( produc800118557al_val > $o ) > val > val > ( val > val > $o ) > val ).
thf(func_def_1142,type,
sK785: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_1143,type,
sK786: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1144,type,
sK787: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > bop ).
thf(func_def_1145,type,
sK788: ( produc630464863al_val > $o ) > product_prod_val_val > bop > ( bop > product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1146,type,
sK789: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1147,type,
sK790: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1148,type,
sK791: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1149,type,
sK792: ( produc1350825965t_char > $o ) > list_char > list_char > ( list_char > list_char > $o ) > list_char ).
thf(func_def_1150,type,
sK793: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_1151,type,
sK794: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_1152,type,
sK795: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > list_char ).
thf(func_def_1153,type,
sK796: ( produc1368416213on_val > $o ) > ( produc1278157519t_char > option_val ) > list_char > ( list_char > ( produc1278157519t_char > option_val ) > $o ) > produc1278157519t_char > option_val ).
thf(func_def_1154,type,
sK797: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_1155,type,
sK798: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_1156,type,
sK799: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > nat > option1728594148on_val ).
thf(func_def_1157,type,
sK800: ( produc1581780743on_val > $o ) > ( list_char > option_val ) > ( nat > option1728594148on_val ) > ( ( nat > option1728594148on_val ) > ( list_char > option_val ) > $o ) > list_char > option_val ).
thf(func_def_1158,type,
sK801: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1159,type,
sK802: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1160,type,
sK803: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1161,type,
sK804: ( produc652964533on_val > $o ) > produc1282892786on_val > produc1282892786on_val > ( produc1282892786on_val > produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1162,type,
sK805: list_P1999446415t_char > ( nat > option1728594148on_val ) > exp_list_char > ( list_char > option_val ) > exp_list_char ).
thf(func_def_1163,type,
sK806: list_P1999446415t_char > ( nat > option1728594148on_val ) > exp_list_char > ( list_char > option_val ) > produc2090907612on_val ).
thf(func_def_1164,type,
sK807: option_nat > nat ).
thf(func_def_1165,type,
sK808: option_ty > ty ).
thf(func_def_1166,type,
sK809: option1728594148on_val > produc2088785539on_val ).
thf(func_def_1167,type,
sK810: option_val > val ).
thf(func_def_1168,type,
sK811: option_list_char_o > list_char > $o ).
thf(func_def_1169,type,
sK812: ( produc618524391on_val > $o ) > produc1180562163on_val > ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1170,type,
sK813: ( produc618524391on_val > $o ) > produc1180562163on_val > ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1171,type,
sK814: ( produc1278157519t_char > $o ) > list_char > ( list_char > $o ) > list_char ).
thf(func_def_1172,type,
sK815: ( produc1278157519t_char > $o ) > list_char > ( list_char > $o ) > list_char ).
thf(func_def_1173,type,
sK816: ( produc1746408499on_val > $o ) > produc1282892786on_val > ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1174,type,
sK817: ( produc1746408499on_val > $o ) > produc1282892786on_val > ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1175,type,
sK818: ( product_prod_val_val > $o ) > val > ( val > $o ) > val ).
thf(func_def_1176,type,
sK819: ( product_prod_val_val > $o ) > val > ( val > $o ) > val ).
thf(func_def_1177,type,
sK820: ( list_char > $o ) > ( list_char > $o ) > list_char ).
thf(func_def_1178,type,
sK821: ( produc618524391on_val > $o ) > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val ).
thf(func_def_1179,type,
sK822: ( produc1278157519t_char > $o ) > list_char > list_char > list_char ).
thf(func_def_1180,type,
sK823: ( produc1746408499on_val > $o ) > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val ).
thf(func_def_1181,type,
sK824: ( product_prod_val_val > $o ) > val > val > val ).
thf(func_def_1182,type,
sK825: ( produc618524391on_val > $o ) > produc1180562163on_val > produc1180562163on_val > produc1180562163on_val ).
thf(func_def_1183,type,
sK826: ( produc1278157519t_char > $o ) > list_char > list_char > list_char ).
thf(func_def_1184,type,
sK827: ( produc1746408499on_val > $o ) > produc1282892786on_val > produc1282892786on_val > produc1282892786on_val ).
thf(func_def_1185,type,
sK828: ( product_prod_val_val > $o ) > val > val > val ).
thf(func_def_1186,type,
sK829: ( produc618524391on_val > $o ) > produc1180562163on_val > ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1187,type,
sK830: ( produc618524391on_val > $o ) > produc1180562163on_val > ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1188,type,
sK831: ( produc1278157519t_char > $o ) > list_char > ( list_char > $o ) > list_char ).
thf(func_def_1189,type,
sK832: ( produc1278157519t_char > $o ) > list_char > ( list_char > $o ) > list_char ).
thf(func_def_1190,type,
sK833: ( produc1746408499on_val > $o ) > produc1282892786on_val > ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1191,type,
sK834: ( produc1746408499on_val > $o ) > produc1282892786on_val > ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1192,type,
sK835: ( product_prod_val_val > $o ) > val > ( val > $o ) > val ).
thf(func_def_1193,type,
sK836: ( product_prod_val_val > $o ) > val > ( val > $o ) > val ).
thf(func_def_1194,type,
sK837: ( list_char > $o ) > ( list_char > $o ) > list_char ).
thf(func_def_1195,type,
sK838: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > nat > option1728594148on_val ).
thf(func_def_1196,type,
sK839: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > list_char > option_val ).
thf(func_def_1197,type,
sK840: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > nat > option1728594148on_val ).
thf(func_def_1198,type,
sK841: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > list_char > option_val ).
thf(func_def_1199,type,
sK842: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1200,type,
sK843: produc2090907612on_val > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > val ).
thf(func_def_1201,type,
sK844: produc2090907612on_val > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > nat > option1728594148on_val ).
thf(func_def_1202,type,
sK845: produc2090907612on_val > produc2090907612on_val > exp_list_char > list_char > list_P1999446415t_char > list_char > option_val ).
thf(func_def_1203,type,
sK846: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1204,type,
sK847: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > val ).
thf(func_def_1205,type,
sK848: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > produc2090907612on_val ).
thf(func_def_1206,type,
sK849: exp_list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_1207,type,
sK850: ty > exp_list_char > list_char > list_char > exp_list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_1208,type,
sK851: exp_list_char > nat ).
thf(func_def_1209,type,
sK852: exp_list_char > nat ).
thf(func_def_1210,type,
sK853: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > bop > val ).
thf(func_def_1211,type,
sK854: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > bop > produc2090907612on_val ).
thf(func_def_1212,type,
sK855: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > bop > val ).
thf(func_def_1213,type,
sK856: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > bop > val ).
thf(func_def_1214,type,
sK857: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > val ).
thf(func_def_1215,type,
sK858: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > produc2090907612on_val ).
thf(func_def_1216,type,
sK859: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1217,type,
sK860: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1218,type,
sK861: exp_list_char > nat ).
thf(func_def_1219,type,
sK862: ty > list_char ).
thf(func_def_1220,type,
sK863: exp_list_char > nat ).
thf(func_def_1221,type,
sK864: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1222,type,
sK865: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > nat ).
thf(func_def_1223,type,
sK866: exp_list_char > list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_1224,type,
sK867: ( nat > option1728594148on_val ) > list_char > ( ( nat > option1728594148on_val ) > list_char > $o ) > produc1278157519t_char > option_val ).
thf(func_def_1225,type,
sK868: ( nat > option1728594148on_val ) > list_char > produc1278157519t_char > option_val ).
thf(func_def_1226,type,
sK869: ( nat > option1728594148on_val ) > list_char ).
thf(func_def_1227,type,
sK870: list_char > ( nat > option1728594148on_val ) > produc1278157519t_char > option_val ).
thf(func_def_1228,type,
sK871: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > produc2090907612on_val ).
thf(func_def_1229,type,
sK872: exp_list_char > exp_list_char > produc2090907612on_val > list_P1999446415t_char > exp_list_char > produc2090907612on_val > exp_list_char ).
thf(func_def_1230,type,
sK873: produc2090907612on_val > list_P1999446415t_char > exp_list_char > exp_list_char > exp_list_char > produc2090907612on_val > produc2090907612on_val ).
thf(func_def_1231,type,
sK874: produc2090907612on_val > list_P1999446415t_char > exp_list_char > exp_list_char > exp_list_char > produc2090907612on_val > val ).
thf(func_def_1232,type,
sK875: produc2090907612on_val > list_P1999446415t_char > exp_list_char > exp_list_char > exp_list_char > produc2090907612on_val > produc2090907612on_val ).
thf(func_def_1233,type,
sK876: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1234,type,
sK877: ty > list_char ).
thf(func_def_1235,type,
sK878: ty > list_char > list_char > exp_list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > list_char ).
thf(func_def_1236,type,
sK879: exp_list_char > list_char > list_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > list_P1999446415t_char > list_char ).
thf(func_def_1237,type,
sK880: exp_list_char > list_char > list_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > list_P1999446415t_char > ty ).
thf(func_def_1238,type,
sK881: exp_list_char > list_char > list_char > ( nat > option1728594148on_val ) > ( list_char > option_ty ) > exp_list_char > list_P1999446415t_char > ty ).
thf(func_def_1239,type,
sK882: exp_list_char > ( list_char > option_ty ) > ( nat > option1728594148on_val ) > list_P1999446415t_char > ty ).
thf(func_def_1240,type,
sK883: ty > list_char ).
thf(func_def_1241,type,
sK884: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1242,type,
sK885: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > produc2090907612on_val ).
thf(func_def_1243,type,
sK886: produc2090907612on_val > exp_list_char > produc2090907612on_val > exp_list_char > exp_list_char > list_P1999446415t_char > produc2090907612on_val ).
thf(func_def_1244,type,
sK887: produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > exp_list_char > list_P1999446415t_char > exp_list_char ).
thf(func_def_1245,type,
sK888: produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > exp_list_char > list_P1999446415t_char > val ).
thf(func_def_1246,type,
sK889: produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > exp_list_char > list_P1999446415t_char > produc2090907612on_val ).
thf(func_def_1247,type,
sK890: produc2090907612on_val > list_exp_list_char > produc2090907612on_val > list_exp_list_char > exp_list_char > list_P1999446415t_char > list_exp_list_char ).
thf(func_def_1248,type,
sK891: list_list_char > list_val > ( nat > option1728594148on_val ) > exp_list_char > ( list_char > option_val ) > ( nat > option1728594148on_val ) > exp_list_char > list_P1999446415t_char > list_char > option_val ).
thf(func_def_1249,type,
sK892: list_ty > list_val > ( nat > option1728594148on_val ) > list_P1999446415t_char > list_ty ).
thf(func_def_1250,type,
sK893: ( produc1746408499on_val > $o ) > produc1746408499on_val ).
thf(func_def_1251,type,
sK894: ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1252,type,
sK895: ( produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1253,type,
sK896: ( produc2088785539on_val > $o ) > produc2088785539on_val ).
thf(func_def_1254,type,
sK897: ( produc1278157519t_char > $o ) > produc1278157519t_char ).
thf(func_def_1255,type,
sK898: ( produc1645268488al_val > $o ) > produc1645268488al_val ).
thf(func_def_1256,type,
sK899: ( product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1257,type,
sK900: ( produc618524391on_val > $o ) > produc618524391on_val ).
thf(func_def_1258,type,
sK901: ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1259,type,
sK902: ( produc1285161482t_char > $o ) > produc1285161482t_char ).
thf(func_def_1260,type,
sK903: ( produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1261,type,
sK904: ( produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1262,type,
sK905: ( produc1971331930t_char > $o ) > produc1971331930t_char ).
thf(func_def_1263,type,
sK906: ( produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1264,type,
sK907: ( produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1265,type,
sK908: ( produc809539159t_char > $o ) > produc809539159t_char ).
thf(func_def_1266,type,
sK909: ( produc809539159t_char > $o ) > produc809539159t_char ).
thf(func_def_1267,type,
sK910: ( produc2146869324t_char > $o ) > produc2146869324t_char ).
thf(func_def_1268,type,
sK911: ( produc952412819t_char > $o ) > produc952412819t_char ).
thf(func_def_1269,type,
sK912: ( produc1971331930t_char > $o ) > produc1971331930t_char ).
thf(func_def_1270,type,
sK913: ( produc662261637t_char > $o ) > produc662261637t_char ).
thf(func_def_1271,type,
sK914: ( produc220283002t_char > $o ) > produc220283002t_char ).
thf(func_def_1272,type,
sK915: ( produc1285161482t_char > $o ) > produc1285161482t_char ).
thf(func_def_1273,type,
sK916: ( produc1180562163on_val > $o ) > produc1180562163on_val ).
thf(func_def_1274,type,
sK917: ( produc618524391on_val > $o ) > produc618524391on_val ).
thf(func_def_1275,type,
sK918: ( product_prod_val_val > $o ) > product_prod_val_val ).
thf(func_def_1276,type,
sK919: ( produc1645268488al_val > $o ) > produc1645268488al_val ).
thf(func_def_1277,type,
sK920: ( produc1278157519t_char > $o ) > produc1278157519t_char ).
thf(func_def_1278,type,
sK921: ( produc2088785539on_val > $o ) > produc2088785539on_val ).
thf(func_def_1279,type,
sK922: ( produc2090907612on_val > $o ) > produc2090907612on_val ).
thf(func_def_1280,type,
sK923: ( produc1282892786on_val > $o ) > produc1282892786on_val ).
thf(func_def_1281,type,
sK924: ( produc1746408499on_val > $o ) > produc1746408499on_val ).
thf(func_def_1282,type,
sK925: ( produc774316953on_val > $o ) > produc774316953on_val ).
thf(func_def_1283,type,
sK926: ( produc1287081631on_val > $o ) > produc1287081631on_val ).
thf(func_def_1284,type,
sK927: ( produc688860215on_val > $o ) > produc688860215on_val ).
thf(func_def_1285,type,
sK928: ( product_prod_bop_bop > $o ) > product_prod_bop_bop ).
thf(func_def_1286,type,
sK929: ( produc1420746395ist_ty > $o ) > produc1420746395ist_ty ).
thf(func_def_1287,type,
sK930: ( produc753553453st_val > $o ) > produc753553453st_val ).
thf(func_def_1288,type,
sK931: ( produc244676007t_char > $o ) > produc244676007t_char ).
thf(func_def_1289,type,
sK932: ( produc450000425har_ty > $o ) > produc450000425har_ty ).
thf(func_def_1290,type,
sK933: ( produc1200003175t_char > $o ) > produc1200003175t_char ).
thf(func_def_1291,type,
sK934: ( produc2048519645t_char > $o ) > produc2048519645t_char ).
thf(func_def_1292,type,
sK935: ( produc91527719t_char > $o ) > produc91527719t_char ).
thf(func_def_1293,type,
sK936: ( produc652964533on_val > $o ) > produc652964533on_val ).
thf(func_def_1294,type,
sK937: ( produc1581780743on_val > $o ) > produc1581780743on_val ).
thf(func_def_1295,type,
sK938: ( produc1368416213on_val > $o ) > produc1368416213on_val ).
thf(func_def_1296,type,
sK939: ( produc1350825965t_char > $o ) > produc1350825965t_char ).
thf(func_def_1297,type,
sK940: ( produc630464863al_val > $o ) > produc630464863al_val ).
thf(func_def_1298,type,
sK941: ( produc800118557al_val > $o ) > produc800118557al_val ).
thf(func_def_1299,type,
sK942: ( produc1250491293on_val > $o ) > produc1250491293on_val ).
thf(func_def_1300,type,
sK943: ( produc349695911t_char > $o ) > produc349695911t_char ).
thf(func_def_1301,type,
sK944: ( produc1406897475t_char > $o ) > produc1406897475t_char ).
thf(func_def_1302,type,
sK945: ( produc1826280281t_char > $o ) > produc1826280281t_char ).
thf(func_def_1303,type,
sK946: ( produc84451751t_char > $o ) > produc84451751t_char ).
thf(func_def_1304,type,
sK947: ( produc740765671t_char > $o ) > produc740765671t_char ).
thf(func_def_1305,type,
sK948: ( produc494726439t_char > $o ) > produc494726439t_char ).
thf(func_def_1306,type,
sK949: ( produc1534059751t_char > $o ) > produc1534059751t_char ).
thf(func_def_1307,type,
sK950: ( produc1013743697t_char > $o ) > produc1013743697t_char ).
thf(func_def_1308,type,
sK951: ( produc245756905har_ty > $o ) > produc245756905har_ty ).
thf(func_def_1309,type,
sK952: ( produc917948472har_ty > $o ) > produc917948472har_ty ).
thf(f2,axiom,
member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_InitBlockRed_I1_J) ).
thf(f1201,conjecture,
member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(f1202,negated_conjecture,
~ ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) ),
inference(negated_conjecture,[status(cth)],[f1201]) ).
thf(f1203,plain,
member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ),
inference(rectify,[],[f2]) ).
thf(f1204,plain,
( ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) )
= $true ),
inference(fool_elimination,[],[f1203]) ).
thf(f2935,plain,
~ ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) ),
inference(rectify,[],[f1202]) ).
thf(f2936,plain,
( ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) )
!= $true ),
inference(fool_elimination,[],[f2935]) ).
thf(f3034,plain,
( ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) )
!= $true ),
inference(flattening,[],[f2936]) ).
thf(f4862,plain,
( ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) )
= $true ),
inference(cnf_transformation,[],[f1204]) ).
thf(f6683,plain,
( ( member1913460000on_val @ ( produc833389609on_val @ ( produc235638504on_val @ ea @ ( produc755559506on_val @ ha @ ( fun_up1149430426on_val @ la @ v_1 @ ( some_val @ v ) ) ) ) @ ( produc235638504on_val @ e_a @ ( produc755559506on_val @ h_a @ l_a ) ) ) @ ( red @ p ) )
!= $true ),
inference(cnf_transformation,[],[f3034]) ).
thf(f7259,plain,
$false,
inference(global_subsumption,[],[f4862,f6683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW478^3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.24 % Computer : n008.cluster.edu
% 0.12/0.24 % Model : x86_64 x86_64
% 0.12/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.24 % Memory : 8046.5625MB
% 0.12/0.24 % OS : Linux 6.8.0-71-generic
% 0.12/0.24 % CPULimit : 300
% 0.12/0.24 % WCLimit : 300
% 0.12/0.24 % DateTime : Tue Sep 29 16:08:46 UTC 2026
% 0.12/0.24 % CPUTime :
% 0.12/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.29 Running first-order model finding
% 0.25/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.22/0.73 % (3348865)Will run a generic schedule for satisfiability detection.
% 2.22/0.73 % (3348874)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3855752608:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.22/0.73 % (3348873)% WARNING: option uhcvi not known.
% 2.22/0.73 % (3348873)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=851133075:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.22/0.73 % (3348875)dis+10_1_sil=32000:sp=arity:random_seed=734704706:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.22/0.73 % (3348876)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4145543211:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.22/0.73 % (3348877)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3913589902:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.22/0.73 % (3348872)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3090910543_2999 on theBenchmark for (2999ds/0Mi)
% 2.22/0.73 % (3348878)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1894011027:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.22/0.73 % (3348875)Instruction limit reached!
% 2.22/0.73 % (3348875)------------------------------
% 2.22/0.73 % (3348875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.73 % (3348875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.73 % (3348875)CaDiCaL version: 2.1.3
% 2.22/0.73 % (3348875)Termination reason: Instruction limit
% 2.22/0.73 % (3348875)Termination phase: Initialization
% 2.22/0.73 % (3348875)Time elapsed: 0.079 s
% 2.22/0.73 % (3348875)Peak memory usage: 13 MB
% 2.22/0.73 % (3348875)Instructions burned: 103 (million)
% 2.22/0.73 % (3348876)Instruction limit reached!
% 2.22/0.73 % (3348876)------------------------------
% 2.22/0.73 % (3348876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.73 % (3348876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.73 % (3348876)CaDiCaL version: 2.1.3
% 2.22/0.73 % (3348876)Termination reason: Instruction limit
% 2.22/0.73 % (3348876)Termination phase: Initialization
% 2.22/0.73 % (3348876)Time elapsed: 0.088 s
% 2.22/0.73 % (3348876)Peak memory usage: 13 MB
% 2.22/0.73 % (3348876)Instructions burned: 117 (million)
% 2.22/0.73 % (3348877)Instruction limit reached!
% 2.22/0.73 % (3348877)------------------------------
% 2.22/0.73 % (3348877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.73 % (3348877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.73 % (3348877)CaDiCaL version: 2.1.3
% 2.22/0.73 % (3348877)Termination reason: Instruction limit
% 2.22/0.73 % (3348877)Termination phase: Initialization
% 2.22/0.73 % (3348877)Time elapsed: 0.100 s
% 2.22/0.73 % (3348877)Peak memory usage: 13 MB
% 2.22/0.73 % (3348877)Instructions burned: 132 (million)
% 2.22/0.73 % (3348886)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3262427252:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 2.22/0.73 % (3348887)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3020264109:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 2.22/0.73 % (3348878)Instruction limit reached!
% 2.22/0.73 % (3348878)------------------------------
% 2.22/0.73 % (3348878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.73 % (3348878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.73 % (3348878)CaDiCaL version: 2.1.3
% 2.22/0.73 % (3348878)Termination reason: Instruction limit
% 2.22/0.73 % (3348878)Termination phase: Property scanning
% 2.22/0.73 % (3348878)Time elapsed: 0.123 s
% 2.22/0.73 % (3348878)Peak memory usage: 13 MB
% 2.22/0.73 % (3348878)Instructions burned: 160 (million)
% 2.22/0.73 % (3348889)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1641116152:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 2.22/0.73 % (3348891)ott-21_1_sil=16000:fs=off:random_seed=2349773252:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 2.22/0.73 % (3348873)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.22/0.73 % (3348887)Instruction limit reached!
% 2.22/0.73 % (3348887)------------------------------
% 2.22/0.73 % (3348887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.73 % (3348887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.73 % (3348887)CaDiCaL version: 2.1.3
% 2.22/0.73 % (3348887)Termination reason: Instruction limit
% 2.22/0.73 % (3348887)Termination phase: Initialization
% 2.22/0.73 % (3348887)Time elapsed: 0.100 s
% 2.22/0.73 % (3348887)Peak memory usage: 13 MB
% 2.22/0.73 % (3348887)Instructions burned: 131 (million)
% 2.22/0.73 % (3348894)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2213982047:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 2.22/0.73 % (3348874) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3348865-3348874"...
% 2.22/0.73 % (3348874)...printing done.
% 2.22/0.73 % (3348874)Refutation found. Thanks to Tanya!
% 2.22/0.73 % SZS status Theorem for theBenchmark
% 2.22/0.73 % SZS output start Proof for theBenchmark
% See solution above
% 2.22/0.74 % (3348874)------------------------------
% 2.22/0.74 % (3348874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.74 % (3348874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.74 % (3348874)CaDiCaL version: 2.1.3
% 2.22/0.74 % (3348874)Termination reason: Refutation
% 2.22/0.74 % (3348874)Time elapsed: 0.298 s
% 2.22/0.74 % (3348874)Peak memory usage: 19 MB
% 2.22/0.74 % (3348874)Instructions burned: 708 (million)
% 2.22/0.74 % (3348865)Success in time 0.432 s
% 2.22/0.74 % Vampire exiting
%------------------------------------------------------------------------------