%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT169_3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 12:37:05 PM UTC 2026
% Result : Theorem 51.98s 8.28s
% Output : Refutation 52.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 33
% Syntax : Number of formulae : 239 ( 92 unt; 0 typ; 9 def)
% Number of atoms : 520 ( 181 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 486 ( 205 ~; 222 |; 40 &)
% ( 15 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 89 ( 88 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 8 prp; 0-3 aty)
% Number of functors : 682 ( 682 usr; 92 con; 0-4 aty)
% Number of variables : 262 ( 0 sgn 247 !; 15 ?; 262 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
arrow_1893660431le_alt: $tType ).
tff(type_def_6,type,
bool: $tType ).
tff(type_def_7,type,
list_A114658244le_alt: $tType ).
tff(type_def_8,type,
list_bool: $tType ).
tff(type_def_9,type,
list_l2028444773le_alt: $tType ).
tff(type_def_10,type,
list_list_nat: $tType ).
tff(type_def_11,type,
list_nat: $tType ).
tff(type_def_12,type,
nat: $tType ).
tff(type_def_13,type,
option661581700le_alt: $tType ).
tff(type_def_14,type,
option_bool: $tType ).
tff(type_def_15,type,
option_nat: $tType ).
tff(type_def_16,type,
fun_Ar17477381t_bool: $tType ).
tff(type_def_17,type,
fun_Ar849108972le_alt: $tType ).
tff(type_def_18,type,
fun_Ar1091137528lt_nat: $tType ).
tff(type_def_19,type,
fun_Ar294405804le_alt: $tType ).
tff(type_def_20,type,
fun_Ar1450809516n_bool: $tType ).
tff(type_def_21,type,
fun_Ar63580199on_nat: $tType ).
tff(type_def_22,type,
fun_Ar331856045t_bool: $tType ).
tff(type_def_23,type,
fun_Ar1433468301l_bool: $tType ).
tff(type_def_24,type,
fun_Ar1448189019le_alt: $tType ).
tff(type_def_25,type,
fun_Ar569529141l_bool: $tType ).
tff(type_def_26,type,
fun_bool_bool: $tType ).
tff(type_def_27,type,
fun_bool_list_bool: $tType ).
tff(type_def_28,type,
fun_bool_list_nat: $tType ).
tff(type_def_29,type,
fun_bool_nat: $tType ).
tff(type_def_30,type,
fun_bo646066118le_alt: $tType ).
tff(type_def_31,type,
fun_bool_option_nat: $tType ).
tff(type_def_32,type,
fun_bo1549164019l_bool: $tType ).
tff(type_def_33,type,
fun_bo1175651857t_bool: $tType ).
tff(type_def_34,type,
fun_bo492988759l_bool: $tType ).
tff(type_def_35,type,
fun_li1641155132le_alt: $tType ).
tff(type_def_36,type,
fun_li1109619974t_bool: $tType ).
tff(type_def_37,type,
fun_li90789869le_alt: $tType ).
tff(type_def_38,type,
fun_li1574574519lt_nat: $tType ).
tff(type_def_39,type,
fun_li297692846t_bool: $tType ).
tff(type_def_40,type,
fun_li164935701le_alt: $tType ).
tff(type_def_41,type,
fun_li495175091t_bool: $tType ).
tff(type_def_42,type,
fun_li264309018le_alt: $tType ).
tff(type_def_43,type,
fun_li1957118493l_bool: $tType ).
tff(type_def_44,type,
fun_li638184490le_alt: $tType ).
tff(type_def_45,type,
fun_li20309264le_alt: $tType ).
tff(type_def_46,type,
fun_list_bool_bool: $tType ).
tff(type_def_47,type,
fun_li107039421t_bool: $tType ).
tff(type_def_48,type,
fun_list_bool_nat: $tType ).
tff(type_def_49,type,
fun_li229471966l_bool: $tType ).
tff(type_def_50,type,
fun_li85477609t_bool: $tType ).
tff(type_def_51,type,
fun_li1854140997t_bool: $tType ).
tff(type_def_52,type,
fun_li662746748t_bool: $tType ).
tff(type_def_53,type,
fun_li513084864t_bool: $tType ).
tff(type_def_54,type,
fun_li1101927920t_bool: $tType ).
tff(type_def_55,type,
fun_li397702653le_alt: $tType ).
tff(type_def_56,type,
fun_li420304957st_nat: $tType ).
tff(type_def_57,type,
fun_list_nat_bool: $tType ).
tff(type_def_58,type,
fun_li1155097699st_nat: $tType ).
tff(type_def_59,type,
fun_list_nat_nat: $tType ).
tff(type_def_60,type,
fun_li972600984l_bool: $tType ).
tff(type_def_61,type,
fun_li1325124399st_nat: $tType ).
tff(type_def_62,type,
fun_li981111539t_bool: $tType ).
tff(type_def_63,type,
fun_li511653589st_nat: $tType ).
tff(type_def_64,type,
fun_li123523364t_bool: $tType ).
tff(type_def_65,type,
fun_li1816930438st_nat: $tType ).
tff(type_def_66,type,
fun_na665391426le_alt: $tType ).
tff(type_def_67,type,
fun_nat_bool: $tType ).
tff(type_def_68,type,
fun_na86871399le_alt: $tType ).
tff(type_def_69,type,
fun_nat_list_bool: $tType ).
tff(type_def_70,type,
fun_nat_list_nat: $tType ).
tff(type_def_71,type,
fun_nat_nat: $tType ).
tff(type_def_72,type,
fun_na1650596135le_alt: $tType ).
tff(type_def_73,type,
fun_nat_option_bool: $tType ).
tff(type_def_74,type,
fun_nat_option_nat: $tType ).
tff(type_def_75,type,
fun_na2015178792t_bool: $tType ).
tff(type_def_76,type,
fun_na1469252690l_bool: $tType ).
tff(type_def_77,type,
fun_na960272160le_alt: $tType ).
tff(type_def_78,type,
fun_na1279735280t_bool: $tType ).
tff(type_def_79,type,
fun_na941842582st_nat: $tType ).
tff(type_def_80,type,
fun_nat_fun_nat_bool: $tType ).
tff(type_def_81,type,
fun_nat_fun_nat_nat: $tType ).
tff(type_def_82,type,
fun_na1436237685l_bool: $tType ).
tff(type_def_83,type,
fun_fu1618786247l_bool: $tType ).
tff(type_def_84,type,
fun_fu1537843567t_bool: $tType ).
tff(type_def_85,type,
fun_fu1085384691l_bool: $tType ).
tff(type_def_86,type,
fun_fu2100440475t_bool: $tType ).
tff(type_def_87,type,
fun_fu1255657237l_bool: $tType ).
tff(type_def_88,type,
fun_fu1393819981l_bool: $tType ).
tff(type_def_89,type,
fun_fu425979586l_bool: $tType ).
tff(type_def_90,type,
fun_fu821463397t_bool: $tType ).
tff(type_def_91,type,
fun_fu1217155507l_bool: $tType ).
tff(type_def_92,type,
fun_fu915923926t_bool: $tType ).
tff(func_def_0,type,
big_Sup_fin_nat: ( fun_nat_fun_nat_nat * fun_nat_bool ) > nat ).
tff(func_def_1,type,
big_linorder_Max_nat: fun_nat_bool > nat ).
tff(func_def_2,type,
cOMBB_388242475le_alt: ( fun_bool_bool * fun_Ar17477381t_bool ) > fun_Ar17477381t_bool ).
tff(func_def_3,type,
cOMBB_bool_bool_bool: ( fun_bool_bool * fun_bool_bool ) > fun_bool_bool ).
tff(func_def_4,type,
cOMBB_bool_bool_nat: ( fun_bool_bool * fun_nat_bool ) > fun_nat_bool ).
tff(func_def_5,type,
cOMBB_1234541833le_alt: ( fun_bo1549164019l_bool * fun_Ar17477381t_bool ) > fun_Ar1433468301l_bool ).
tff(func_def_6,type,
cOMBB_1914122979l_bool: ( fun_bo1549164019l_bool * fun_bool_bool ) > fun_bo1549164019l_bool ).
tff(func_def_7,type,
cOMBB_1015721476ol_nat: ( fun_bo1549164019l_bool * fun_nat_bool ) > fun_na1469252690l_bool ).
tff(func_def_8,type,
cOMBB_138440792lt_nat: ( fun_li90789869le_alt * fun_na86871399le_alt ) > fun_na86871399le_alt ).
tff(func_def_9,type,
cOMBB_1076781858le_alt: ( fun_li264309018le_alt * fun_Ar849108972le_alt ) > fun_Ar1448189019le_alt ).
tff(func_def_10,type,
cOMBB_1891801486ol_nat: ( fun_li107039421t_bool * fun_nat_list_bool ) > fun_nat_list_bool ).
tff(func_def_11,type,
cOMBB_1663860504l_bool: ( fun_li662746748t_bool * fun_bool_list_bool ) > fun_bo1175651857t_bool ).
tff(func_def_12,type,
cOMBB_850496866at_nat: ( fun_li1155097699st_nat * fun_nat_list_nat ) > fun_nat_list_nat ).
tff(func_def_13,type,
cOMBB_472649634at_nat: ( fun_li511653589st_nat * fun_nat_list_nat ) > fun_na941842582st_nat ).
tff(func_def_14,type,
cOMBB_nat_nat_nat: ( fun_nat_nat * fun_nat_nat ) > fun_nat_nat ).
tff(func_def_15,type,
cOMBB_1146692694ol_nat: ( fun_na1436237685l_bool * fun_nat_nat ) > fun_na1436237685l_bool ).
tff(func_def_16,type,
cOMBC_1826973210t_bool: fun_Ar331856045t_bool > fun_Ar331856045t_bool ).
tff(func_def_17,type,
cOMBC_673369480le_alt: fun_Ar1448189019le_alt > fun_li164935701le_alt ).
tff(func_def_18,type,
cOMBC_1310341090l_bool: fun_Ar569529141l_bool > fun_fu1537843567t_bool ).
tff(func_def_19,type,
cOMBC_bool_bool_bool: fun_bo1549164019l_bool > fun_bo1549164019l_bool ).
tff(func_def_20,type,
cOMBC_80330970t_bool: fun_bo1175651857t_bool > fun_li85477609t_bool ).
tff(func_def_21,type,
cOMBC_1833749623le_alt: fun_li264309018le_alt > fun_li264309018le_alt ).
tff(func_def_22,type,
cOMBC_1789016513t_bool: fun_li662746748t_bool > fun_li662746748t_bool ).
tff(func_def_23,type,
cOMBC_950362600st_nat: fun_li511653589st_nat > fun_li511653589st_nat ).
tff(func_def_24,type,
cOMBC_869637379le_alt: fun_na960272160le_alt > fun_li20309264le_alt ).
tff(func_def_25,type,
cOMBC_1038295629t_bool: fun_na1279735280t_bool > fun_li1101927920t_bool ).
tff(func_def_26,type,
cOMBC_1204473209st_nat: fun_na941842582st_nat > fun_li1816930438st_nat ).
tff(func_def_27,type,
cOMBC_nat_nat_bool: fun_nat_fun_nat_bool > fun_nat_fun_nat_bool ).
tff(func_def_28,type,
cOMBC_nat_nat_nat: fun_nat_fun_nat_nat > fun_nat_fun_nat_nat ).
tff(func_def_29,type,
cOMBC_226598744l_bool: fun_na1436237685l_bool > fun_fu821463397t_bool ).
tff(func_def_30,type,
cOMBI_nat: fun_nat_nat ).
tff(func_def_31,type,
cOMBK_930998768le_alt: fun_li90789869le_alt > fun_Ar1448189019le_alt ).
tff(func_def_32,type,
cOMBK_1717478773at_nat: fun_li1155097699st_nat > fun_na941842582st_nat ).
tff(func_def_33,type,
cOMBS_119208490l_bool: ( fun_Ar1433468301l_bool * fun_Ar17477381t_bool ) > fun_Ar17477381t_bool ).
tff(func_def_34,type,
cOMBS_bool_bool_bool: ( fun_bo1549164019l_bool * fun_bool_bool ) > fun_bool_bool ).
tff(func_def_35,type,
cOMBS_nat_bool_bool: ( fun_na1469252690l_bool * fun_nat_bool ) > fun_nat_bool ).
tff(func_def_36,type,
minus_minus_nat: fun_nat_fun_nat_nat ).
tff(func_def_37,type,
minus_1875147572t_bool: fun_fu2100440475t_bool ).
tff(func_def_38,type,
minus_2067140911t_bool: fun_fu915923926t_bool ).
tff(func_def_39,type,
plus_plus_nat: fun_nat_fun_nat_nat ).
tff(func_def_40,type,
zero_zero_nat: nat ).
tff(func_def_41,type,
bool_size: fun_bool_nat ).
tff(func_def_42,type,
equal_631514850le_alt: fun_li495175091t_bool ).
tff(func_def_43,type,
equal_equal_list_nat: fun_li981111539t_bool ).
tff(func_def_44,type,
if_lis1472843348le_alt: ( bool * list_A114658244le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_45,type,
if_list_bool: ( bool * list_bool * list_bool ) > list_bool ).
tff(func_def_46,type,
if_list_nat: ( bool * list_nat * list_nat ) > list_nat ).
tff(func_def_47,type,
listMe1496348587le_alt: arrow_1893660431le_alt > fun_li1109619974t_bool ).
tff(func_def_48,type,
listMem_bool: bool > fun_list_bool_bool ).
tff(func_def_49,type,
listMem_nat: nat > fun_list_nat_bool ).
tff(func_def_50,type,
append1597383892le_alt: fun_li264309018le_alt ).
tff(func_def_51,type,
append_bool: fun_li662746748t_bool ).
tff(func_def_52,type,
append_nat: fun_li511653589st_nat ).
tff(func_def_53,type,
butlas1693249291le_alt: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_54,type,
butlast_bool: list_bool > list_bool ).
tff(func_def_55,type,
butlast_nat: list_nat > list_nat ).
tff(func_def_56,type,
distin1654625714le_alt: fun_li1109619974t_bool ).
tff(func_def_57,type,
distinct_bool: fun_list_bool_bool ).
tff(func_def_58,type,
distinct_nat: fun_list_nat_bool ).
tff(func_def_59,type,
dropWh587599712le_alt: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_60,type,
dropWhile_bool: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_61,type,
dropWhile_nat: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_62,type,
drop_A617527551le_alt: fun_na960272160le_alt ).
tff(func_def_63,type,
drop_bool: fun_na1279735280t_bool ).
tff(func_def_64,type,
drop_nat: fun_na941842582st_nat ).
tff(func_def_65,type,
foldl_1844370748le_alt: ( fun_li164935701le_alt * list_A114658244le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_66,type,
foldl_list_bool_bool: ( fun_li85477609t_bool * list_bool * list_bool ) > list_bool ).
tff(func_def_67,type,
foldl_list_nat_nat: ( fun_li1816930438st_nat * list_nat * list_nat ) > list_nat ).
tff(func_def_68,type,
foldl_nat_nat: ( fun_nat_fun_nat_nat * nat * list_nat ) > nat ).
tff(func_def_69,type,
foldr_nat_nat: ( fun_nat_fun_nat_nat * list_nat ) > fun_nat_nat ).
tff(func_def_70,type,
hd_Arr1236501138le_alt: fun_li1641155132le_alt ).
tff(func_def_71,type,
hd_bool: fun_list_bool_bool ).
tff(func_def_72,type,
hd_nat: fun_list_nat_nat ).
tff(func_def_73,type,
insert1391384533le_alt: fun_Ar1448189019le_alt ).
tff(func_def_74,type,
insert_bool: fun_bo1175651857t_bool ).
tff(func_def_75,type,
insert_nat: fun_na941842582st_nat ).
tff(func_def_76,type,
last_A488133080le_alt: fun_li1641155132le_alt ).
tff(func_def_77,type,
last_bool: fun_list_bool_bool ).
tff(func_def_78,type,
last_nat: fun_list_nat_nat ).
tff(func_def_79,type,
linord297828738at_nat: fun_nat_nat > fun_na941842582st_nat ).
tff(func_def_80,type,
linord1850739451at_nat: fun_nat_nat > fun_na941842582st_nat ).
tff(func_def_81,type,
linord852754176at_nat: ( fun_nat_nat * list_nat ) > list_nat ).
tff(func_def_82,type,
linorder_sorted_nat: fun_list_nat_bool ).
tff(func_def_83,type,
cons_A1647044463le_alt: fun_Ar1448189019le_alt ).
tff(func_def_84,type,
cons_bool: fun_bo1175651857t_bool ).
tff(func_def_85,type,
cons_l782000996le_alt: fun_li638184490le_alt ).
tff(func_def_86,type,
cons_list_nat: fun_li1325124399st_nat ).
tff(func_def_87,type,
cons_nat: fun_na941842582st_nat ).
tff(func_def_88,type,
nil_Ar557011903le_alt: list_A114658244le_alt ).
tff(func_def_89,type,
nil_bool: list_bool ).
tff(func_def_90,type,
nil_nat: list_nat ).
tff(func_def_91,type,
list_c1024366775le_alt: ( list_A114658244le_alt * fun_Ar1448189019le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_92,type,
list_c1750880501l_bool: ( list_bool * fun_bo1175651857t_bool * list_bool ) > list_bool ).
tff(func_def_93,type,
list_c554461815at_nat: ( list_nat * fun_na941842582st_nat * list_nat ) > list_nat ).
tff(func_def_94,type,
list_s1668597313le_alt: ( fun_Ar1091137528lt_nat * list_A114658244le_alt ) > nat ).
tff(func_def_95,type,
list_size_bool: ( fun_bool_nat * list_bool ) > nat ).
tff(func_def_96,type,
list_size_nat: ( fun_nat_nat * list_nat ) > nat ).
tff(func_def_97,type,
list_a1988415615le_alt: fun_Ar17477381t_bool > fun_li1109619974t_bool ).
tff(func_def_98,type,
list_all_bool: fun_bool_bool > fun_list_bool_bool ).
tff(func_def_99,type,
list_all_nat: fun_nat_bool > fun_list_nat_bool ).
tff(func_def_100,type,
list_e1657546370le_alt: fun_Ar17477381t_bool > fun_li1109619974t_bool ).
tff(func_def_101,type,
list_ex1_bool: fun_bool_bool > fun_list_bool_bool ).
tff(func_def_102,type,
list_ex1_nat: fun_nat_bool > fun_list_nat_bool ).
tff(func_def_103,type,
listre483979801le_alt: ( fun_Ar331856045t_bool * list_A114658244le_alt ) > fun_li1109619974t_bool ).
tff(func_def_104,type,
listrelp_bool: ( fun_bo1549164019l_bool * list_bool ) > fun_list_bool_bool ).
tff(func_def_105,type,
listrelp_nat: ( fun_nat_fun_nat_bool * list_nat ) > fun_list_nat_bool ).
tff(func_def_106,type,
map_nat_nat: ( fun_nat_nat * list_nat ) > list_nat ).
tff(func_def_107,type,
map_fi886559370le_alt: ( fun_Ar294405804le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_108,type,
map_fi966861858t_bool: ( fun_Ar1450809516n_bool * list_A114658244le_alt ) > list_bool ).
tff(func_def_109,type,
map_fi1320516869lt_nat: ( fun_Ar63580199on_nat * list_A114658244le_alt ) > list_nat ).
tff(func_def_110,type,
map_fi280134778le_alt: ( fun_bo646066118le_alt * list_bool ) > list_A114658244le_alt ).
tff(func_def_111,type,
map_filter_bool_nat: ( fun_bool_option_nat * list_bool ) > list_nat ).
tff(func_def_112,type,
map_fi733515087le_alt: ( fun_na1650596135le_alt * list_nat ) > list_A114658244le_alt ).
tff(func_def_113,type,
map_filter_nat_bool: ( fun_nat_option_bool * list_nat ) > list_bool ).
tff(func_def_114,type,
map_filter_nat_nat: ( fun_nat_option_nat * list_nat ) > list_nat ).
tff(func_def_115,type,
maps_A652163713le_alt: ( fun_Ar849108972le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_116,type,
maps_bool_nat: ( fun_bool_list_nat * list_bool ) > list_nat ).
tff(func_def_117,type,
maps_n398774214le_alt: ( fun_na86871399le_alt * list_nat ) > list_A114658244le_alt ).
tff(func_def_118,type,
member775785940le_alt: fun_li297692846t_bool ).
tff(func_def_119,type,
member_bool_1: fun_li229471966l_bool ).
tff(func_def_120,type,
member_nat_1: fun_li123523364t_bool ).
tff(func_def_121,type,
nth_Ar1544180416le_alt: list_A114658244le_alt > fun_na665391426le_alt ).
tff(func_def_122,type,
nth_bool: list_bool > fun_nat_bool ).
tff(func_def_123,type,
nth_li103876819le_alt: list_l2028444773le_alt > fun_na86871399le_alt ).
tff(func_def_124,type,
nth_list_nat: list_list_nat > fun_nat_list_nat ).
tff(func_def_125,type,
nth_nat: list_nat > fun_nat_nat ).
tff(func_def_126,type,
null_A791782855le_alt: fun_li1109619974t_bool ).
tff(func_def_127,type,
null_bool: fun_list_bool_bool ).
tff(func_def_128,type,
null_nat: fun_list_nat_bool ).
tff(func_def_129,type,
remove861161045le_alt: fun_Ar1448189019le_alt ).
tff(func_def_130,type,
remove1_bool: fun_bo1175651857t_bool ).
tff(func_def_131,type,
remove1_nat: fun_na941842582st_nat ).
tff(func_def_132,type,
replic782356601le_alt: nat > fun_Ar849108972le_alt ).
tff(func_def_133,type,
replicate_bool: nat > fun_bool_list_bool ).
tff(func_def_134,type,
replicate_nat: nat > fun_nat_list_nat ).
tff(func_def_135,type,
rev_Ar377224735le_alt: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_136,type,
rev_bool: list_bool > list_bool ).
tff(func_def_137,type,
rev_nat: list_nat > list_nat ).
tff(func_def_138,type,
rotate1753650700le_alt: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_139,type,
rotate1_bool: list_bool > list_bool ).
tff(func_def_140,type,
rotate1_nat: list_nat > list_nat ).
tff(func_def_141,type,
set_Ar1995755744le_alt: fun_li297692846t_bool ).
tff(func_def_142,type,
set_bool: fun_li229471966l_bool ).
tff(func_def_143,type,
set_nat: fun_li123523364t_bool ).
tff(func_def_144,type,
splice791716242le_alt: ( list_A114658244le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_145,type,
splice_bool: ( list_bool * list_bool ) > list_bool ).
tff(func_def_146,type,
splice_nat: ( list_nat * list_nat ) > list_nat ).
tff(func_def_147,type,
sublis1318771396le_alt: ( list_A114658244le_alt * fun_nat_bool ) > list_A114658244le_alt ).
tff(func_def_148,type,
sublist_bool: ( list_bool * fun_nat_bool ) > list_bool ).
tff(func_def_149,type,
sublist_nat: ( list_nat * fun_nat_bool ) > list_nat ).
tff(func_def_150,type,
takeWh967109304le_alt: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_151,type,
takeWhile_bool: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_152,type,
takeWhile_nat: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_153,type,
take_A2032349095le_alt: fun_na960272160le_alt ).
tff(func_def_154,type,
take_bool: fun_na1279735280t_bool ).
tff(func_def_155,type,
take_nat: fun_na941842582st_nat ).
tff(func_def_156,type,
tl_Arr1883752598le_alt: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_157,type,
tl_bool: list_bool > list_bool ).
tff(func_def_158,type,
tl_nat: list_nat > list_nat ).
tff(func_def_159,type,
upt: nat > fun_nat_list_nat ).
tff(func_def_160,type,
suc: fun_nat_nat ).
tff(func_def_161,type,
nat_ca822049091le_alt: ( arrow_1893660431le_alt * fun_na665391426le_alt ) > fun_na665391426le_alt ).
tff(func_def_162,type,
nat_case_bool: ( bool * fun_nat_bool ) > fun_nat_bool ).
tff(func_def_163,type,
nat_ca146784400le_alt: ( list_A114658244le_alt * fun_na86871399le_alt ) > fun_na86871399le_alt ).
tff(func_def_164,type,
nat_case_list_bool: ( list_bool * fun_nat_list_bool ) > fun_nat_list_bool ).
tff(func_def_165,type,
nat_case_list_nat: ( list_nat * fun_nat_list_nat ) > fun_nat_list_nat ).
tff(func_def_166,type,
nat_case_nat: ( nat * fun_nat_nat ) > fun_nat_nat ).
tff(func_def_167,type,
nat_size: fun_nat_nat ).
tff(func_def_168,type,
size_s2005684270le_alt: fun_li1574574519lt_nat ).
tff(func_def_169,type,
size_size_list_bool: fun_list_bool_nat ).
tff(func_def_170,type,
size_size_list_nat: fun_list_nat_nat ).
tff(func_def_171,type,
size_size_nat: fun_nat_nat ).
tff(func_def_172,type,
option1112736594le_alt: ( list_A114658244le_alt * fun_Ar849108972le_alt * option661581700le_alt ) > list_A114658244le_alt ).
tff(func_def_173,type,
option718651152l_bool: ( list_bool * fun_bool_list_bool * option_bool ) > list_bool ).
tff(func_def_174,type,
option306705938at_nat: ( list_nat * fun_nat_list_nat * option_nat ) > list_nat ).
tff(func_def_175,type,
max_nat: fun_nat_fun_nat_bool > fun_nat_fun_nat_nat ).
tff(func_def_176,type,
min_nat: fun_nat_fun_nat_bool > fun_nat_fun_nat_nat ).
tff(func_def_177,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(func_def_178,type,
ord_le123846959t_bool: fun_fu1085384691l_bool ).
tff(func_def_179,type,
ord_le382113706t_bool: fun_fu1217155507l_bool ).
tff(func_def_180,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(func_def_181,type,
ord_le1779845435t_bool: fun_fu1085384691l_bool ).
tff(func_def_182,type,
ord_le742797417l_bool: fun_fu1393819981l_bool ).
tff(func_def_183,type,
ord_le1568362934t_bool: fun_fu1217155507l_bool ).
tff(func_def_184,type,
ord_max_nat: fun_nat_fun_nat_nat ).
tff(func_def_185,type,
ord_min_nat: fun_nat_fun_nat_nat ).
tff(func_def_186,type,
collec12892580le_alt: fun_Ar17477381t_bool > fun_Ar17477381t_bool ).
tff(func_def_187,type,
collect_nat: fun_nat_bool > fun_nat_bool ).
tff(func_def_188,type,
fFalse: bool ).
tff(func_def_189,type,
fNot: fun_bool_bool ).
tff(func_def_190,type,
fTrue: bool ).
tff(func_def_191,type,
fconj: fun_bo1549164019l_bool ).
tff(func_def_192,type,
fdisj: fun_bo1549164019l_bool ).
tff(func_def_193,type,
fequal1590852494le_alt: fun_Ar331856045t_bool ).
tff(func_def_194,type,
fequal_bool: fun_bo1549164019l_bool ).
tff(func_def_195,type,
fequal928191109le_alt: fun_li495175091t_bool ).
tff(func_def_196,type,
fequal_list_nat: fun_li981111539t_bool ).
tff(func_def_197,type,
fequal_nat: fun_nat_fun_nat_bool ).
tff(func_def_198,type,
hAPP_A1748732503t_bool: ( fun_Ar17477381t_bool * arrow_1893660431le_alt ) > bool ).
tff(func_def_199,type,
hAPP_A1382181054le_alt: ( fun_Ar849108972le_alt * arrow_1893660431le_alt ) > list_A114658244le_alt ).
tff(func_def_200,type,
hAPP_A1419065744lt_nat: ( fun_Ar1091137528lt_nat * arrow_1893660431le_alt ) > nat ).
tff(func_def_201,type,
hAPP_A1567920766le_alt: ( fun_Ar294405804le_alt * arrow_1893660431le_alt ) > option661581700le_alt ).
tff(func_def_202,type,
hAPP_A1193192004n_bool: ( fun_Ar1450809516n_bool * arrow_1893660431le_alt ) > option_bool ).
tff(func_def_203,type,
hAPP_A1602729209on_nat: ( fun_Ar63580199on_nat * arrow_1893660431le_alt ) > option_nat ).
tff(func_def_204,type,
hAPP_A2063800319t_bool: ( fun_Ar331856045t_bool * arrow_1893660431le_alt ) > fun_Ar17477381t_bool ).
tff(func_def_205,type,
hAPP_A463015077l_bool: ( fun_Ar1433468301l_bool * arrow_1893660431le_alt ) > fun_bool_bool ).
tff(func_def_206,type,
hAPP_A436723315le_alt: ( fun_Ar1448189019le_alt * arrow_1893660431le_alt ) > fun_li90789869le_alt ).
tff(func_def_207,type,
hAPP_A1501726285l_bool: ( fun_Ar569529141l_bool * arrow_1893660431le_alt ) > fun_fu1618786247l_bool ).
tff(func_def_208,type,
hAPP_bool_bool: ( fun_bool_bool * bool ) > bool ).
tff(func_def_209,type,
hAPP_bool_list_bool: ( fun_bool_list_bool * bool ) > list_bool ).
tff(func_def_210,type,
hAPP_bool_list_nat: ( fun_bool_list_nat * bool ) > list_nat ).
tff(func_def_211,type,
hAPP_bool_nat: ( fun_bool_nat * bool ) > nat ).
tff(func_def_212,type,
hAPP_b935842788le_alt: ( fun_bo646066118le_alt * bool ) > option661581700le_alt ).
tff(func_def_213,type,
hAPP_bool_option_nat: ( fun_bool_option_nat * bool ) > option_nat ).
tff(func_def_214,type,
hAPP_b589554111l_bool: ( fun_bo1549164019l_bool * bool ) > fun_bool_bool ).
tff(func_def_215,type,
hAPP_b994696797t_bool: ( fun_bo1175651857t_bool * bool ) > fun_li107039421t_bool ).
tff(func_def_216,type,
hAPP_b1787118453l_bool: ( fun_bo492988759l_bool * bool ) > fun_fu1255657237l_bool ).
tff(func_def_217,type,
hAPP_l1749541000le_alt: ( fun_li1641155132le_alt * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_218,type,
hAPP_l499746980t_bool: ( fun_li1109619974t_bool * list_A114658244le_alt ) > bool ).
tff(func_def_219,type,
hAPP_l84111627le_alt: ( fun_li90789869le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_220,type,
hAPP_l1084348419lt_nat: ( fun_li1574574519lt_nat * list_A114658244le_alt ) > nat ).
tff(func_def_221,type,
hAPP_l2018657868t_bool: ( fun_li297692846t_bool * list_A114658244le_alt ) > fun_Ar17477381t_bool ).
tff(func_def_222,type,
hAPP_l1822938419le_alt: ( fun_li164935701le_alt * list_A114658244le_alt ) > fun_Ar849108972le_alt ).
tff(func_def_223,type,
hAPP_l82091775t_bool: ( fun_li495175091t_bool * list_A114658244le_alt ) > fun_li1109619974t_bool ).
tff(func_def_224,type,
hAPP_l86320102le_alt: ( fun_li264309018le_alt * list_A114658244le_alt ) > fun_li90789869le_alt ).
tff(func_def_225,type,
hAPP_l2076432827l_bool: ( fun_li1957118493l_bool * list_A114658244le_alt ) > fun_list_bool_bool ).
tff(func_def_226,type,
hAPP_l1201992822le_alt: ( fun_li638184490le_alt * list_A114658244le_alt ) > fun_li397702653le_alt ).
tff(func_def_227,type,
hAPP_l1210406190le_alt: ( fun_li20309264le_alt * list_A114658244le_alt ) > fun_na86871399le_alt ).
tff(func_def_228,type,
hAPP_list_bool_bool: ( fun_list_bool_bool * list_bool ) > bool ).
tff(func_def_229,type,
hAPP_l1189022293t_bool: ( fun_li107039421t_bool * list_bool ) > list_bool ).
tff(func_def_230,type,
hAPP_list_bool_nat: ( fun_list_bool_nat * list_bool ) > nat ).
tff(func_def_231,type,
hAPP_l96088310l_bool: ( fun_li229471966l_bool * list_bool ) > fun_bool_bool ).
tff(func_def_232,type,
hAPP_l1045755451t_bool: ( fun_li85477609t_bool * list_bool ) > fun_bool_list_bool ).
tff(func_def_233,type,
hAPP_l799327709t_bool: ( fun_li1854140997t_bool * list_bool ) > fun_li1109619974t_bool ).
tff(func_def_234,type,
hAPP_l1947611924t_bool: ( fun_li662746748t_bool * list_bool ) > fun_li107039421t_bool ).
tff(func_def_235,type,
hAPP_l909187928t_bool: ( fun_li513084864t_bool * list_bool ) > fun_list_nat_bool ).
tff(func_def_236,type,
hAPP_l1656175496t_bool: ( fun_li1101927920t_bool * list_bool ) > fun_nat_list_bool ).
tff(func_def_237,type,
hAPP_l1913469717le_alt: ( fun_li397702653le_alt * list_l2028444773le_alt ) > list_l2028444773le_alt ).
tff(func_def_238,type,
hAPP_l1734754389st_nat: ( fun_li420304957st_nat * list_list_nat ) > list_list_nat ).
tff(func_def_239,type,
hAPP_list_nat_bool: ( fun_list_nat_bool * list_nat ) > bool ).
tff(func_def_240,type,
hAPP_l248265089st_nat: ( fun_li1155097699st_nat * list_nat ) > list_nat ).
tff(func_def_241,type,
hAPP_list_nat_nat: ( fun_list_nat_nat * list_nat ) > nat ).
tff(func_def_242,type,
hAPP_l1101248310l_bool: ( fun_li972600984l_bool * list_nat ) > fun_list_bool_bool ).
tff(func_def_243,type,
hAPP_l1872445307st_nat: ( fun_li1325124399st_nat * list_nat ) > fun_li420304957st_nat ).
tff(func_def_244,type,
hAPP_l120351551t_bool: ( fun_li981111539t_bool * list_nat ) > fun_list_nat_bool ).
tff(func_def_245,type,
hAPP_l710375585st_nat: ( fun_li511653589st_nat * list_nat ) > fun_li1155097699st_nat ).
tff(func_def_246,type,
hAPP_l1821533378t_bool: ( fun_li123523364t_bool * list_nat ) > fun_nat_bool ).
tff(func_def_247,type,
hAPP_l383341732st_nat: ( fun_li1816930438st_nat * list_nat ) > fun_nat_list_nat ).
tff(func_def_248,type,
hAPP_n832063962le_alt: ( fun_na665391426le_alt * nat ) > arrow_1893660431le_alt ).
tff(func_def_249,type,
hAPP_nat_bool: ( fun_nat_bool * nat ) > bool ).
tff(func_def_250,type,
hAPP_n2007559481le_alt: ( fun_na86871399le_alt * nat ) > list_A114658244le_alt ).
tff(func_def_251,type,
hAPP_nat_list_bool: ( fun_nat_list_bool * nat ) > list_bool ).
tff(func_def_252,type,
hAPP_nat_list_nat: ( fun_nat_list_nat * nat ) > list_nat ).
tff(func_def_253,type,
hAPP_nat_nat: ( fun_nat_nat * nat ) > nat ).
tff(func_def_254,type,
hAPP_n4766713le_alt: ( fun_na1650596135le_alt * nat ) > option661581700le_alt ).
tff(func_def_255,type,
hAPP_nat_option_bool: ( fun_nat_option_bool * nat ) > option_bool ).
tff(func_def_256,type,
hAPP_nat_option_nat: ( fun_nat_option_nat * nat ) > option_nat ).
tff(func_def_257,type,
hAPP_n1201661562t_bool: ( fun_na2015178792t_bool * nat ) > fun_Ar17477381t_bool ).
tff(func_def_258,type,
hAPP_n1006566506l_bool: ( fun_na1469252690l_bool * nat ) > fun_bool_bool ).
tff(func_def_259,type,
hAPP_n372949560le_alt: ( fun_na960272160le_alt * nat ) > fun_li90789869le_alt ).
tff(func_def_260,type,
hAPP_n479129736t_bool: ( fun_na1279735280t_bool * nat ) > fun_li107039421t_bool ).
tff(func_def_261,type,
hAPP_n280362926st_nat: ( fun_na941842582st_nat * nat ) > fun_li1155097699st_nat ).
tff(func_def_262,type,
hAPP_n1699378549t_bool: ( fun_nat_fun_nat_bool * nat ) > fun_nat_bool ).
tff(func_def_263,type,
hAPP_nat_fun_nat_nat: ( fun_nat_fun_nat_nat * nat ) > fun_nat_nat ).
tff(func_def_264,type,
hAPP_n215258509l_bool: ( fun_na1436237685l_bool * nat ) > fun_fu425979586l_bool ).
tff(func_def_265,type,
hAPP_f739344229l_bool: ( fun_fu1618786247l_bool * fun_Ar17477381t_bool ) > bool ).
tff(func_def_266,type,
hAPP_f1592536333t_bool: ( fun_fu1537843567t_bool * fun_Ar17477381t_bool ) > fun_Ar17477381t_bool ).
tff(func_def_267,type,
hAPP_f1549168575l_bool: ( fun_fu1085384691l_bool * fun_Ar17477381t_bool ) > fun_fu1618786247l_bool ).
tff(func_def_268,type,
hAPP_f571726183t_bool: ( fun_fu2100440475t_bool * fun_Ar17477381t_bool ) > fun_fu1537843567t_bool ).
tff(func_def_269,type,
hAPP_f387058535l_bool: ( fun_fu1255657237l_bool * fun_bool_bool ) > bool ).
tff(func_def_270,type,
hAPP_f612708895l_bool: ( fun_fu1393819981l_bool * fun_bool_bool ) > fun_fu1255657237l_bool ).
tff(func_def_271,type,
hAPP_f54304608l_bool: ( fun_fu425979586l_bool * fun_nat_bool ) > bool ).
tff(func_def_272,type,
hAPP_f800510211t_bool: ( fun_fu821463397t_bool * fun_nat_bool ) > fun_nat_bool ).
tff(func_def_273,type,
hAPP_f103356543l_bool: ( fun_fu1217155507l_bool * fun_nat_bool ) > fun_fu425979586l_bool ).
tff(func_def_274,type,
hAPP_f1730770594t_bool: ( fun_fu915923926t_bool * fun_nat_bool ) > fun_fu821463397t_bool ).
tff(func_def_275,type,
member1502664802le_alt: fun_Ar569529141l_bool ).
tff(func_def_276,type,
member_bool: fun_bo492988759l_bool ).
tff(func_def_277,type,
member_nat: fun_na1436237685l_bool ).
tff(func_def_278,type,
a: arrow_1893660431le_alt ).
tff(func_def_279,type,
b: arrow_1893660431le_alt ).
tff(func_def_280,type,
sK4: arrow_1893660431le_alt ).
tff(func_def_281,type,
sK5: arrow_1893660431le_alt ).
tff(func_def_282,type,
sK6: arrow_1893660431le_alt ).
tff(func_def_283,type,
sK7: list_bool > bool ).
tff(func_def_284,type,
sK8: list_bool > list_bool ).
tff(func_def_285,type,
sK9: list_A114658244le_alt > arrow_1893660431le_alt ).
tff(func_def_286,type,
sK10: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_287,type,
sK11: list_nat > nat ).
tff(func_def_288,type,
sK12: list_nat > list_nat ).
tff(func_def_289,type,
sK13: list_bool > bool ).
tff(func_def_290,type,
sK14: list_bool > list_bool ).
tff(func_def_291,type,
sK15: list_A114658244le_alt > arrow_1893660431le_alt ).
tff(func_def_292,type,
sK16: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_293,type,
sK17: list_nat > nat ).
tff(func_def_294,type,
sK18: list_nat > list_nat ).
tff(func_def_295,type,
sK19: fun_list_bool_bool > bool ).
tff(func_def_296,type,
sK20: fun_list_bool_bool > list_bool ).
tff(func_def_297,type,
sK21: fun_list_bool_bool > bool ).
tff(func_def_298,type,
sK22: fun_li1109619974t_bool > arrow_1893660431le_alt ).
tff(func_def_299,type,
sK23: fun_li1109619974t_bool > list_A114658244le_alt ).
tff(func_def_300,type,
sK24: fun_li1109619974t_bool > arrow_1893660431le_alt ).
tff(func_def_301,type,
sK25: fun_list_nat_bool > nat ).
tff(func_def_302,type,
sK26: fun_list_nat_bool > list_nat ).
tff(func_def_303,type,
sK27: fun_list_nat_bool > nat ).
tff(func_def_304,type,
sK28: ( list_A114658244le_alt * list_A114658244le_alt * list_A114658244le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_305,type,
sK29: ( list_nat * list_nat * list_nat * list_nat ) > list_nat ).
tff(func_def_306,type,
sK30: ( list_bool * list_bool * bool * list_bool ) > list_bool ).
tff(func_def_307,type,
sK31: ( list_A114658244le_alt * list_A114658244le_alt * arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_308,type,
sK32: ( list_nat * list_nat * nat * list_nat ) > list_nat ).
tff(func_def_309,type,
sK33: ( bool * list_bool * list_bool * list_bool ) > list_bool ).
tff(func_def_310,type,
sK34: ( arrow_1893660431le_alt * list_A114658244le_alt * list_A114658244le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_311,type,
sK35: ( nat * list_nat * list_nat * list_nat ) > list_nat ).
tff(func_def_312,type,
sK36: fun_list_bool_bool > bool ).
tff(func_def_313,type,
sK37: fun_list_bool_bool > list_bool ).
tff(func_def_314,type,
sK38: fun_li1109619974t_bool > arrow_1893660431le_alt ).
tff(func_def_315,type,
sK39: fun_li1109619974t_bool > list_A114658244le_alt ).
tff(func_def_316,type,
sK40: fun_list_nat_bool > nat ).
tff(func_def_317,type,
sK41: fun_list_nat_bool > list_nat ).
tff(func_def_318,type,
sK42: list_bool > list_bool ).
tff(func_def_319,type,
sK43: list_bool > bool ).
tff(func_def_320,type,
sK44: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_321,type,
sK45: list_A114658244le_alt > arrow_1893660431le_alt ).
tff(func_def_322,type,
sK46: list_nat > list_nat ).
tff(func_def_323,type,
sK47: list_nat > nat ).
tff(func_def_324,type,
sK48: list_bool > list_bool ).
tff(func_def_325,type,
sK49: list_bool > list_bool ).
tff(func_def_326,type,
sK50: list_bool > list_bool ).
tff(func_def_327,type,
sK51: list_bool > bool ).
tff(func_def_328,type,
sK52: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_329,type,
sK53: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_330,type,
sK54: list_A114658244le_alt > list_A114658244le_alt ).
tff(func_def_331,type,
sK55: list_A114658244le_alt > arrow_1893660431le_alt ).
tff(func_def_332,type,
sK56: list_nat > list_nat ).
tff(func_def_333,type,
sK57: list_nat > list_nat ).
tff(func_def_334,type,
sK58: list_nat > list_nat ).
tff(func_def_335,type,
sK59: list_nat > nat ).
tff(func_def_336,type,
sK60: ( bool * list_bool ) > bool ).
tff(func_def_337,type,
sK61: ( bool * list_bool ) > list_bool ).
tff(func_def_338,type,
sK62: ( bool * list_bool ) > bool ).
tff(func_def_339,type,
sK63: ( bool * list_bool ) > bool ).
tff(func_def_340,type,
sK64: ( bool * list_bool ) > list_bool ).
tff(func_def_341,type,
sK65: ( arrow_1893660431le_alt * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_342,type,
sK66: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_343,type,
sK67: ( arrow_1893660431le_alt * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_344,type,
sK68: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_345,type,
sK69: ( arrow_1893660431le_alt * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_346,type,
sK70: ( nat * list_nat ) > nat ).
tff(func_def_347,type,
sK71: ( nat * list_nat ) > list_nat ).
tff(func_def_348,type,
sK72: ( nat * list_nat ) > nat ).
tff(func_def_349,type,
sK73: ( nat * list_nat ) > list_nat ).
tff(func_def_350,type,
sK74: ( nat * list_nat ) > nat ).
tff(func_def_351,type,
sK75: fun_li1957118493l_bool > arrow_1893660431le_alt ).
tff(func_def_352,type,
sK76: fun_li1957118493l_bool > list_A114658244le_alt ).
tff(func_def_353,type,
sK77: fun_li1957118493l_bool > bool ).
tff(func_def_354,type,
sK78: fun_li1957118493l_bool > list_bool ).
tff(func_def_355,type,
sK79: fun_li1957118493l_bool > bool ).
tff(func_def_356,type,
sK80: fun_li1957118493l_bool > list_bool ).
tff(func_def_357,type,
sK81: fun_li1957118493l_bool > arrow_1893660431le_alt ).
tff(func_def_358,type,
sK82: fun_li1957118493l_bool > list_A114658244le_alt ).
tff(func_def_359,type,
sK83: fun_li972600984l_bool > nat ).
tff(func_def_360,type,
sK84: fun_li972600984l_bool > list_nat ).
tff(func_def_361,type,
sK85: fun_li972600984l_bool > bool ).
tff(func_def_362,type,
sK86: fun_li972600984l_bool > list_bool ).
tff(func_def_363,type,
sK87: fun_li972600984l_bool > bool ).
tff(func_def_364,type,
sK88: fun_li972600984l_bool > list_bool ).
tff(func_def_365,type,
sK89: fun_li972600984l_bool > nat ).
tff(func_def_366,type,
sK90: fun_li972600984l_bool > list_nat ).
tff(func_def_367,type,
sK91: fun_li1854140997t_bool > bool ).
tff(func_def_368,type,
sK92: fun_li1854140997t_bool > list_bool ).
tff(func_def_369,type,
sK93: fun_li1854140997t_bool > arrow_1893660431le_alt ).
tff(func_def_370,type,
sK94: fun_li1854140997t_bool > list_A114658244le_alt ).
tff(func_def_371,type,
sK95: fun_li1854140997t_bool > arrow_1893660431le_alt ).
tff(func_def_372,type,
sK96: fun_li1854140997t_bool > list_A114658244le_alt ).
tff(func_def_373,type,
sK97: fun_li1854140997t_bool > bool ).
tff(func_def_374,type,
sK98: fun_li1854140997t_bool > list_bool ).
tff(func_def_375,type,
sK99: fun_li513084864t_bool > bool ).
tff(func_def_376,type,
sK100: fun_li513084864t_bool > list_bool ).
tff(func_def_377,type,
sK101: fun_li513084864t_bool > nat ).
tff(func_def_378,type,
sK102: fun_li513084864t_bool > list_nat ).
tff(func_def_379,type,
sK103: fun_li513084864t_bool > nat ).
tff(func_def_380,type,
sK104: fun_li513084864t_bool > list_nat ).
tff(func_def_381,type,
sK105: fun_li513084864t_bool > bool ).
tff(func_def_382,type,
sK106: fun_li513084864t_bool > list_bool ).
tff(func_def_383,type,
sK107: ( list_bool * list_bool * fun_bo1549164019l_bool ) > bool ).
tff(func_def_384,type,
sK108: ( list_bool * list_bool * fun_bo1549164019l_bool ) > bool ).
tff(func_def_385,type,
sK109: ( list_bool * list_bool * fun_bo1549164019l_bool ) > list_bool ).
tff(func_def_386,type,
sK110: ( list_bool * list_bool * fun_bo1549164019l_bool ) > list_bool ).
tff(func_def_387,type,
sK111: ( list_A114658244le_alt * list_A114658244le_alt * fun_Ar331856045t_bool ) > arrow_1893660431le_alt ).
tff(func_def_388,type,
sK112: ( list_A114658244le_alt * list_A114658244le_alt * fun_Ar331856045t_bool ) > arrow_1893660431le_alt ).
tff(func_def_389,type,
sK113: ( list_A114658244le_alt * list_A114658244le_alt * fun_Ar331856045t_bool ) > list_A114658244le_alt ).
tff(func_def_390,type,
sK114: ( list_A114658244le_alt * list_A114658244le_alt * fun_Ar331856045t_bool ) > list_A114658244le_alt ).
tff(func_def_391,type,
sK115: ( list_nat * list_nat * fun_nat_fun_nat_bool ) > nat ).
tff(func_def_392,type,
sK116: ( list_nat * list_nat * fun_nat_fun_nat_bool ) > nat ).
tff(func_def_393,type,
sK117: ( list_nat * list_nat * fun_nat_fun_nat_bool ) > list_nat ).
tff(func_def_394,type,
sK118: ( list_nat * list_nat * fun_nat_fun_nat_bool ) > list_nat ).
tff(func_def_395,type,
sK119: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_396,type,
sK120: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_397,type,
sK121: ( fun_Ar17477381t_bool * list_A114658244le_alt * arrow_1893660431le_alt ) > arrow_1893660431le_alt ).
tff(func_def_398,type,
sK122: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_399,type,
sK123: ( fun_nat_bool * list_nat * nat ) > nat ).
tff(func_def_400,type,
sK124: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_401,type,
sK125: ( fun_Ar17477381t_bool * nat * arrow_1893660431le_alt ) > arrow_1893660431le_alt ).
tff(func_def_402,type,
sK126: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_403,type,
sK127: ( fun_Ar17477381t_bool * nat * arrow_1893660431le_alt ) > arrow_1893660431le_alt ).
tff(func_def_404,type,
sK128: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_405,type,
sK129: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_406,type,
sK130: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_407,type,
sK131: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_408,type,
sK132: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_409,type,
sK133: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_410,type,
sK134: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_411,type,
sK135: ( bool * list_bool ) > list_bool ).
tff(func_def_412,type,
sK136: ( bool * list_bool ) > list_bool ).
tff(func_def_413,type,
sK137: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_414,type,
sK138: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_415,type,
sK139: ( nat * list_nat ) > list_nat ).
tff(func_def_416,type,
sK140: ( nat * list_nat ) > list_nat ).
tff(func_def_417,type,
sK141: ( bool * list_bool ) > list_bool ).
tff(func_def_418,type,
sK142: ( bool * list_bool ) > list_bool ).
tff(func_def_419,type,
sK143: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_420,type,
sK144: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_421,type,
sK145: ( nat * list_nat ) > list_nat ).
tff(func_def_422,type,
sK146: ( nat * list_nat ) > list_nat ).
tff(func_def_423,type,
sK147: ( bool * list_bool ) > list_bool ).
tff(func_def_424,type,
sK148: ( bool * list_bool ) > list_bool ).
tff(func_def_425,type,
sK149: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_426,type,
sK150: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_427,type,
sK151: ( nat * list_nat ) > list_nat ).
tff(func_def_428,type,
sK152: ( nat * list_nat ) > list_nat ).
tff(func_def_429,type,
sK153: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_430,type,
sK154: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_431,type,
sK155: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_432,type,
sK156: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_433,type,
sK157: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_434,type,
sK158: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_435,type,
sK159: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_436,type,
sK160: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_437,type,
sK161: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_438,type,
sK162: ( fun_Ar17477381t_bool * fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_439,type,
sK163: ( fun_nat_bool * fun_nat_bool * list_nat ) > nat ).
tff(func_def_440,type,
sK164: ( fun_Ar17477381t_bool * fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_441,type,
sK165: ( fun_nat_bool * fun_nat_bool * list_nat ) > nat ).
tff(func_def_442,type,
sK166: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_443,type,
sK167: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_444,type,
sK168: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_445,type,
sK169: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_446,type,
sK170: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_447,type,
sK171: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_448,type,
sK172: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_449,type,
sK173: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_450,type,
sK174: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_451,type,
sK175: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_452,type,
sK176: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_453,type,
sK177: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_454,type,
sK178: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_455,type,
sK179: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_456,type,
sK180: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_457,type,
sK181: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_458,type,
sK182: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_459,type,
sK183: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_460,type,
sK184: ( bool * list_bool ) > list_bool ).
tff(func_def_461,type,
sK185: ( bool * list_bool ) > list_bool ).
tff(func_def_462,type,
sK186: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_463,type,
sK187: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_464,type,
sK188: ( nat * list_nat ) > list_nat ).
tff(func_def_465,type,
sK189: ( nat * list_nat ) > list_nat ).
tff(func_def_466,type,
sK190: ( bool * list_bool ) > list_bool ).
tff(func_def_467,type,
sK191: ( bool * list_bool ) > list_bool ).
tff(func_def_468,type,
sK192: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_469,type,
sK193: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_470,type,
sK194: ( nat * list_nat ) > list_nat ).
tff(func_def_471,type,
sK195: ( nat * list_nat ) > list_nat ).
tff(func_def_472,type,
sK196: ( bool * list_bool ) > list_bool ).
tff(func_def_473,type,
sK197: ( bool * list_bool ) > list_bool ).
tff(func_def_474,type,
sK198: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_475,type,
sK199: ( arrow_1893660431le_alt * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_476,type,
sK200: ( nat * list_nat ) > list_nat ).
tff(func_def_477,type,
sK201: ( nat * list_nat ) > list_nat ).
tff(func_def_478,type,
sK202: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_479,type,
sK203: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_480,type,
sK204: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_481,type,
sK205: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_482,type,
sK206: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_483,type,
sK207: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_484,type,
sK208: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_485,type,
sK209: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_486,type,
sK210: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_487,type,
sK211: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_488,type,
sK212: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_489,type,
sK213: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_490,type,
sK214: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_491,type,
sK215: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_492,type,
sK216: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_493,type,
sK217: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_494,type,
sK218: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_495,type,
sK219: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_496,type,
sK220: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_497,type,
sK221: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_498,type,
sK222: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_499,type,
sK223: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_500,type,
sK224: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_501,type,
sK225: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_502,type,
sK226: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_503,type,
sK227: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_504,type,
sK228: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_505,type,
sK229: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_506,type,
sK230: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_507,type,
sK231: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_508,type,
sK232: nat > nat ).
tff(func_def_509,type,
sK233: fun_nat_bool > nat ).
tff(func_def_510,type,
sK234: fun_nat_bool > nat ).
tff(func_def_511,type,
sK235: nat > nat ).
tff(func_def_512,type,
sK236: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_513,type,
sK237: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_514,type,
sK238: ( fun_Ar17477381t_bool * fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_515,type,
sK239: ( fun_nat_bool * fun_nat_bool * list_nat ) > nat ).
tff(func_def_516,type,
sK240: ( list_A114658244le_alt * list_A114658244le_alt ) > nat ).
tff(func_def_517,type,
sK241: ( list_nat * list_nat ) > nat ).
tff(func_def_518,type,
sK242: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_519,type,
sK243: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_520,type,
sK244: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_521,type,
sK245: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_522,type,
sK246: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_523,type,
sK247: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_524,type,
sK248: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_525,type,
sK249: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_526,type,
sK250: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_527,type,
sK251: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_528,type,
sK252: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_529,type,
sK253: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_530,type,
sK254: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_531,type,
sK255: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_532,type,
sK256: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_533,type,
sK257: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_534,type,
sK258: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_535,type,
sK259: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_536,type,
sK260: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_537,type,
sK261: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_538,type,
sK262: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_539,type,
sK263: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_540,type,
sK264: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_541,type,
sK265: ( fun_nat_bool * list_nat ) > list_nat ).
tff(func_def_542,type,
sK266: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_543,type,
sK267: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_544,type,
sK268: ( fun_bool_bool * list_bool ) > list_bool ).
tff(func_def_545,type,
sK269: fun_nat_fun_nat_nat > nat ).
tff(func_def_546,type,
sK270: fun_nat_fun_nat_nat > nat ).
tff(func_def_547,type,
sK271: fun_nat_fun_nat_nat > nat ).
tff(func_def_548,type,
sK272: ( fun_nat_fun_nat_nat * fun_nat_fun_nat_nat * list_nat ) > nat ).
tff(func_def_549,type,
sK273: ( fun_nat_fun_nat_nat * fun_nat_fun_nat_nat * list_nat ) > nat ).
tff(func_def_550,type,
sK274: ( fun_nat_fun_nat_nat * list_nat * fun_nat_bool ) > nat ).
tff(func_def_551,type,
sK275: ( fun_nat_fun_nat_nat * list_nat * fun_nat_bool ) > nat ).
tff(func_def_552,type,
sK276: list_nat > nat ).
tff(func_def_553,type,
sK277: fun_nat_fun_nat_nat > nat ).
tff(func_def_554,type,
sK278: fun_nat_fun_nat_nat > nat ).
tff(func_def_555,type,
sK279: fun_nat_fun_nat_nat > nat ).
tff(func_def_556,type,
sK280: ( fun_nat_fun_nat_nat * fun_nat_bool * fun_nat_bool ) > nat ).
tff(func_def_557,type,
sK281: ( fun_nat_fun_nat_nat * fun_nat_bool * fun_nat_bool ) > nat ).
tff(func_def_558,type,
sK282: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_559,type,
sK283: ( nat * nat ) > nat ).
tff(func_def_560,type,
sK284: ( nat * list_nat ) > nat ).
tff(func_def_561,type,
sK285: ( list_nat * list_nat ) > nat ).
tff(func_def_562,type,
sK286: ( list_nat * list_nat ) > nat ).
tff(func_def_563,type,
sK287: ( list_nat * nat ) > nat ).
tff(func_def_564,type,
sK288: list_nat > list_nat ).
tff(func_def_565,type,
sK289: list_nat > nat ).
tff(func_def_566,type,
sK290: ( fun_nat_nat * nat * list_nat ) > nat ).
tff(func_def_567,type,
sK291: ( nat * list_nat ) > nat ).
tff(func_def_568,type,
sK292: fun_nat_nat > nat ).
tff(func_def_569,type,
sK293: nat > nat ).
tff(func_def_570,type,
sK294: nat > nat ).
tff(func_def_571,type,
sK295: nat > nat ).
tff(func_def_572,type,
sK296: ( fun_Ar17477381t_bool * fun_Ar17477381t_bool ) > arrow_1893660431le_alt ).
tff(func_def_573,type,
sK297: ( fun_nat_bool * fun_nat_bool ) > nat ).
tff(func_def_574,type,
sK298: fun_nat_nat > nat ).
tff(func_def_575,type,
sK299: fun_nat_nat > nat ).
tff(func_def_576,type,
sK300: ( fun_nat_bool * fun_nat_bool ) > nat ).
tff(func_def_577,type,
sK301: fun_nat_nat > nat ).
tff(func_def_578,type,
sK302: fun_nat_nat > nat ).
tff(func_def_579,type,
sK303: fun_nat_nat > nat ).
tff(func_def_580,type,
sK304: fun_nat_nat > nat ).
tff(func_def_581,type,
sK305: fun_nat_bool > nat ).
tff(func_def_582,type,
sK306: ( nat * list_bool ) > bool ).
tff(func_def_583,type,
sK307: ( nat * list_bool ) > list_bool ).
tff(func_def_584,type,
sK308: ( nat * list_nat ) > nat ).
tff(func_def_585,type,
sK309: ( nat * list_nat ) > list_nat ).
tff(func_def_586,type,
sK310: ( nat * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_587,type,
sK311: ( nat * list_A114658244le_alt ) > list_A114658244le_alt ).
tff(func_def_588,type,
sK312: ( list_bool * nat ) > bool ).
tff(func_def_589,type,
sK313: ( list_bool * nat ) > list_bool ).
tff(func_def_590,type,
sK314: ( list_nat * nat ) > nat ).
tff(func_def_591,type,
sK315: ( list_nat * nat ) > list_nat ).
tff(func_def_592,type,
sK316: ( list_A114658244le_alt * nat ) > arrow_1893660431le_alt ).
tff(func_def_593,type,
sK317: ( list_A114658244le_alt * nat ) > list_A114658244le_alt ).
tff(func_def_594,type,
sK318: nat ).
tff(func_def_595,type,
sK319: nat ).
tff(func_def_596,type,
sK320: nat ).
tff(func_def_597,type,
sK321: nat ).
tff(func_def_598,type,
sK322: nat ).
tff(func_def_599,type,
sK323: nat ).
tff(func_def_600,type,
sK324: fun_nat_bool > nat ).
tff(func_def_601,type,
sK325: nat > nat ).
tff(func_def_602,type,
sK326: nat > nat ).
tff(func_def_603,type,
sK327: nat > nat ).
tff(func_def_604,type,
sK328: ( nat * nat ) > nat ).
tff(func_def_605,type,
sK329: ( nat * nat ) > nat ).
tff(func_def_606,type,
sK330: ( list_bool * list_bool ) > nat ).
tff(func_def_607,type,
sK331: ( list_A114658244le_alt * list_A114658244le_alt ) > nat ).
tff(func_def_608,type,
sK332: ( list_nat * list_nat ) > nat ).
tff(func_def_609,type,
sK333: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_610,type,
sK334: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_611,type,
sK335: ( bool * list_bool ) > nat ).
tff(func_def_612,type,
sK336: ( arrow_1893660431le_alt * list_A114658244le_alt ) > nat ).
tff(func_def_613,type,
sK337: ( nat * list_nat ) > nat ).
tff(func_def_614,type,
sK338: ( fun_bool_bool * list_bool ) > nat ).
tff(func_def_615,type,
sK339: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_616,type,
sK340: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > nat ).
tff(func_def_617,type,
sK341: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_618,type,
sK342: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_619,type,
sK343: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_620,type,
sK344: list_bool > nat ).
tff(func_def_621,type,
sK345: list_bool > nat ).
tff(func_def_622,type,
sK346: list_A114658244le_alt > nat ).
tff(func_def_623,type,
sK347: list_A114658244le_alt > nat ).
tff(func_def_624,type,
sK348: list_nat > nat ).
tff(func_def_625,type,
sK349: list_nat > nat ).
tff(func_def_626,type,
sK350: ( fun_bool_bool * list_bool ) > nat ).
tff(func_def_627,type,
sK351: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > nat ).
tff(func_def_628,type,
sK352: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_629,type,
sK353: list_nat > nat ).
tff(func_def_630,type,
sK354: list_nat > nat ).
tff(func_def_631,type,
sK355: list_nat > nat ).
tff(func_def_632,type,
sK356: list_nat > nat ).
tff(func_def_633,type,
sK357: ( fun_bool_bool * list_bool * nat ) > nat ).
tff(func_def_634,type,
sK358: ( fun_Ar17477381t_bool * list_A114658244le_alt * nat ) > nat ).
tff(func_def_635,type,
sK359: ( fun_nat_bool * list_nat * nat ) > nat ).
tff(func_def_636,type,
sK360: ( fun_bool_bool * list_bool * nat ) > nat ).
tff(func_def_637,type,
sK361: ( fun_Ar17477381t_bool * list_A114658244le_alt * nat ) > nat ).
tff(func_def_638,type,
sK362: ( fun_nat_bool * list_nat * nat ) > nat ).
tff(func_def_639,type,
sK363: ( list_bool * nat * list_bool ) > nat ).
tff(func_def_640,type,
sK364: ( list_A114658244le_alt * nat * list_A114658244le_alt ) > nat ).
tff(func_def_641,type,
sK365: ( list_nat * nat * list_nat ) > nat ).
tff(func_def_642,type,
sK366: ( fun_Ar1091137528lt_nat * fun_Ar1091137528lt_nat * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_643,type,
sK367: ( fun_nat_nat * fun_nat_nat * list_nat ) > nat ).
tff(func_def_644,type,
sK368: ( fun_bool_bool * list_bool ) > nat ).
tff(func_def_645,type,
sK369: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > nat ).
tff(func_def_646,type,
sK370: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_647,type,
sK371: ( fun_bool_bool * list_bool ) > bool ).
tff(func_def_648,type,
sK372: ( fun_Ar17477381t_bool * list_A114658244le_alt ) > arrow_1893660431le_alt ).
tff(func_def_649,type,
sK373: ( fun_nat_bool * list_nat ) > nat ).
tff(func_def_650,type,
sK374: ( list_bool * list_bool ) > nat ).
tff(func_def_651,type,
sK375: ( list_A114658244le_alt * list_A114658244le_alt ) > nat ).
tff(func_def_652,type,
sK376: ( list_nat * list_nat ) > nat ).
tff(func_def_653,type,
sK377: ( fun_na1469252690l_bool * nat ) > bool ).
tff(func_def_654,type,
sK378: ( fun_na1469252690l_bool * nat * list_bool ) > nat ).
tff(func_def_655,type,
sK379: ( fun_na1469252690l_bool * nat ) > list_bool ).
tff(func_def_656,type,
sK380: ( fun_na1469252690l_bool * nat ) > nat ).
tff(func_def_657,type,
sK381: ( fun_na2015178792t_bool * nat ) > arrow_1893660431le_alt ).
tff(func_def_658,type,
sK382: ( fun_na2015178792t_bool * nat * list_A114658244le_alt ) > nat ).
tff(func_def_659,type,
sK383: ( fun_na2015178792t_bool * nat ) > list_A114658244le_alt ).
tff(func_def_660,type,
sK384: ( fun_na2015178792t_bool * nat ) > nat ).
tff(func_def_661,type,
sK385: ( fun_nat_fun_nat_bool * nat ) > nat ).
tff(func_def_662,type,
sK386: ( fun_nat_fun_nat_bool * nat * list_nat ) > nat ).
tff(func_def_663,type,
sK387: ( fun_nat_fun_nat_bool * nat ) > list_nat ).
tff(func_def_664,type,
sK388: ( fun_nat_fun_nat_bool * nat ) > nat ).
tff(func_def_665,type,
sK389: fun_nat_nat > nat ).
tff(func_def_666,type,
sK390: fun_nat_nat > nat ).
tff(func_def_667,type,
sK391: ( fun_nat_bool * nat ) > nat ).
tff(func_def_668,type,
sK392: ( nat * nat ) > nat ).
tff(func_def_669,type,
sK393: ( nat * fun_nat_bool ) > nat ).
tff(func_def_670,type,
sK394: ( nat * nat ) > nat ).
tff(func_def_671,type,
sK395: nat > nat ).
tff(func_def_672,type,
sK396: fun_nat_nat > nat ).
tff(func_def_673,type,
sK397: fun_nat_nat > nat ).
tff(func_def_674,type,
sK398: ( fun_Ar17477381t_bool * fun_Ar17477381t_bool ) > arrow_1893660431le_alt ).
tff(func_def_675,type,
sK399: ( fun_nat_bool * fun_nat_bool ) > nat ).
tff(func_def_676,type,
sK400: fun_nat_nat > nat ).
tff(func_def_677,type,
sK401: fun_nat_nat > nat ).
tff(func_def_678,type,
sK402: ( nat * nat ) > nat ).
tff(func_def_679,type,
sK403: ( nat * nat ) > nat ).
tff(func_def_680,type,
sF404: fun_li90789869le_alt ).
tff(func_def_681,type,
sF405: fun_li90789869le_alt ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(pred_def_2,type,
sP0: ( bool * list_bool ) > $o ).
tff(pred_def_3,type,
sP1: ( list_bool * list_bool * fun_bo1549164019l_bool ) > $o ).
tff(pred_def_4,type,
sP2: ( list_A114658244le_alt * list_A114658244le_alt * fun_Ar331856045t_bool ) > $o ).
tff(pred_def_5,type,
sP3: ( list_nat * list_nat * fun_nat_fun_nat_bool ) > $o ).
tff(f1,axiom,
? [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt,X2: arrow_1893660431le_alt] : hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X2),nil_Ar557011903le_alt))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_alt3) ).
tff(f2,axiom,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,nil_Ar557011903le_alt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_distinct_Osimps_I1_J) ).
tff(f29,axiom,
! [X0: arrow_1893660431le_alt] : ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_insert__Nil) ).
tff(f38,axiom,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1))
=> hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_distinct__insert) ).
tff(f52,axiom,
! [X0: list_A114658244le_alt,X1: fun_Ar1448189019le_alt,X2: arrow_1893660431le_alt,X3: list_A114658244le_alt] : ( list_c1024366775le_alt(X0,X1,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X2),X3)) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_list_Osimps_I5_J) ).
tff(f115,axiom,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ( X0 = X1 )
=> ( X0 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,nil_Ar557011903le_alt),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_eq__Nil__appendI) ).
tff(f127,axiom,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt,X3: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
<=> ( ( ( X2 = nil_Ar557011903le_alt )
& ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = X3 ) )
| ? [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) = X2 )
& ( X1 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_Cons__eq__append__conv) ).
tff(f152,axiom,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( rotate1753650700le_alt(nil_Ar557011903le_alt) = nil_Ar557011903le_alt )
& ( rotate1753650700le_alt(hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_rotate__simps) ).
tff(f194,axiom,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rev_Ar377224735le_alt(X0)))
<=> hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_distinct__rev) ).
tff(f218,axiom,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rotate1753650700le_alt(X0)))
<=> hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_distinct1__rotate) ).
tff(f292,axiom,
! [X0: nat,X1: arrow_1893660431le_alt] :
( ( hAPP_A1382181054le_alt(replic782356601le_alt(X0),X1) = nil_Ar557011903le_alt )
<=> ( X0 = zero_zero_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_291_replicate__empty) ).
tff(f329,axiom,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt,X2: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),X2))))
=> ( ( X0 = X1 )
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_328_set__ConsD) ).
tff(f364,axiom,
! [X0: list_A114658244le_alt] : ( rotate1753650700le_alt(X0) = list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_363_rotate1__def) ).
tff(f370,axiom,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))
<=> ( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
& hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_369_distinct_Osimps_I2_J) ).
tff(f372,axiom,
! [X0: arrow_1893660431le_alt,X1: nat,X2: arrow_1893660431le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2))))
<=> ( ( X0 = X2 )
& ( X1 != zero_zero_nat ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_371_in__set__replicate) ).
tff(f399,axiom,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
<=> ? [X2: list_A114658244le_alt,X3: list_A114658244le_alt] : ( X1 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_398_in__set__conv__decomp) ).
tff(f558,axiom,
! [X0: list_A114658244le_alt] : ( rev_Ar377224735le_alt(X0) = foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_557_rev__foldl__cons) ).
tff(f1166,axiom,
! [X0: arrow_1893660431le_alt,X1: nat,X2: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,X1),X2))))
=> hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1165_in__set__dropD) ).
tff(f1182,axiom,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) = X2 )
<=> ( ( X0 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(take_A2032349095le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) )
& ( X1 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1181_append__eq__conv__conj) ).
tff(f1203,axiom,
hBOOL(fTrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).
tff(f1211,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
tff(f1238,axiom,
! [X0: bool] :
( ( X0 = fTrue )
| ( X0 = fFalse ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_If_000tc__List__Olist_Itc__Arrow____Order____Mirabelle____effngqiqbs) ).
tff(f1266,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f1267,conjecture,
? [X0: arrow_1893660431le_alt] : hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
tff(f1268,negated_conjecture,
~ ? [X0: arrow_1893660431le_alt] : hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt))))),
inference(negated_conjecture,[status(cth)],[f1267]) ).
tff(f1321,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) ),
inference(ennf_transformation,[],[f38]) ).
tff(f1345,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ( X0 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,nil_Ar557011903le_alt),X1) )
| ( X0 != X1 ) ),
inference(ennf_transformation,[],[f115]) ).
tff(f1448,plain,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt,X2: list_A114658244le_alt] :
( ( X0 = X1 )
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2)))
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),X2)))) ),
inference(ennf_transformation,[],[f329]) ).
tff(f1449,plain,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt,X2: list_A114658244le_alt] :
( ( X0 = X1 )
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2)))
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),X2)))) ),
inference(flattening,[],[f1448]) ).
tff(f2049,plain,
! [X0: arrow_1893660431le_alt,X1: nat,X2: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2)))
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,X1),X2)))) ),
inference(ennf_transformation,[],[f1166]) ).
tff(f2067,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt))))),
inference(ennf_transformation,[],[f1268]) ).
tff(f2076,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),nil_Ar557011903le_alt))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f1]) ).
tff(f2155,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt,X3: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
| ( ( ( nil_Ar557011903le_alt != X2 )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != X3 ) )
& ! [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) != X2 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ) ) )
& ( ( ( X2 = nil_Ar557011903le_alt )
& ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = X3 ) )
| ? [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) = X2 )
& ( X1 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) ) )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) ) ) ),
inference(nnf_transformation,[],[f127]) ).
tff(f2156,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt,X3: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
| ( ( ( nil_Ar557011903le_alt != X2 )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != X3 ) )
& ! [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) != X2 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ) ) )
& ( ( ( X2 = nil_Ar557011903le_alt )
& ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = X3 ) )
| ? [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) = X2 )
& ( X1 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) ) )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) ) ) ),
inference(flattening,[],[f2155]) ).
tff(f2157,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt,X3: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
| ( ( ( nil_Ar557011903le_alt != X2 )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != X3 ) )
& ! [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) != X2 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ) ) )
& ( ( ( X2 = nil_Ar557011903le_alt )
& ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = X3 ) )
| ? [X5: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X5) = X2 )
& ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X5),X3) = X1 ) )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) ) ) ),
inference(rectify,[],[f2156]) ).
tff(f2158,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt,X3: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
| ( ( ( nil_Ar557011903le_alt != X2 )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != X3 ) )
& ! [X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) != X2 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ) ) )
& ( ( ( X2 = nil_Ar557011903le_alt )
& ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = X3 ) )
| ( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),sK34(X0,X1,X2,X3)) = X2 )
& ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,sK34(X0,X1,X2,X3)),X3) = X1 ) )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) != hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X5,sK34(X0,X1,X2,X3))],[f2157]) ).
tff(f2198,plain,
! [X0: list_A114658244le_alt] :
( ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rev_Ar377224735le_alt(X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) )
& ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rev_Ar377224735le_alt(X0))) ) ),
inference(nnf_transformation,[],[f194]) ).
tff(f2203,plain,
! [X0: list_A114658244le_alt] :
( ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rotate1753650700le_alt(X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) )
& ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rotate1753650700le_alt(X0))) ) ),
inference(nnf_transformation,[],[f218]) ).
tff(f2255,plain,
! [X0: nat,X1: arrow_1893660431le_alt] :
( ( ( hAPP_A1382181054le_alt(replic782356601le_alt(X0),X1) = nil_Ar557011903le_alt )
| ( zero_zero_nat != X0 ) )
& ( ( X0 = zero_zero_nat )
| ( nil_Ar557011903le_alt != hAPP_A1382181054le_alt(replic782356601le_alt(X0),X1) ) ) ),
inference(nnf_transformation,[],[f292]) ).
tff(f2299,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
& hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))) ) ),
inference(nnf_transformation,[],[f370]) ).
tff(f2300,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) )
& ( ( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
& hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))) ) ),
inference(flattening,[],[f2299]) ).
tff(f2303,plain,
! [X0: arrow_1893660431le_alt,X1: nat,X2: arrow_1893660431le_alt] :
( ( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2))))
| ( X0 != X2 )
| ( zero_zero_nat = X1 ) )
& ( ( ( X0 = X2 )
& ( X1 != zero_zero_nat ) )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2)))) ) ),
inference(nnf_transformation,[],[f372]) ).
tff(f2304,plain,
! [X0: arrow_1893660431le_alt,X1: nat,X2: arrow_1893660431le_alt] :
( ( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2))))
| ( X0 != X2 )
| ( zero_zero_nat = X1 ) )
& ( ( ( X0 = X2 )
& ( X1 != zero_zero_nat ) )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2)))) ) ),
inference(flattening,[],[f2303]) ).
tff(f2336,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ! [X2: list_A114658244le_alt,X3: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) != X1 ) )
& ( ? [X2: list_A114658244le_alt,X3: list_A114658244le_alt] : ( X1 = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1))) ) ),
inference(nnf_transformation,[],[f399]) ).
tff(f2337,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ! [X2: list_A114658244le_alt,X3: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) != X1 ) )
& ( ? [X4: list_A114658244le_alt,X5: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X5)) = X1 )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1))) ) ),
inference(rectify,[],[f2336]) ).
tff(f2338,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ! [X2: list_A114658244le_alt,X3: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) != X1 ) )
& ( ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,sK137(X0,X1)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),sK138(X0,X1))) = X1 )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK137,sK138]),skolemize(X4,sK137(X0,X1)),skolemize(X5,sK138(X0,X1))],[f2337]) ).
tff(f2778,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) = X2 )
| ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(take_A2032349095le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) != X0 )
| ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) != X1 ) )
& ( ( ( X0 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(take_A2032349095le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) )
& ( X1 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) ) )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) != X2 ) ) ),
inference(nnf_transformation,[],[f1182]) ).
tff(f2779,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt,X2: list_A114658244le_alt] :
( ( ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) = X2 )
| ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(take_A2032349095le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) != X0 )
| ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) != X1 ) )
& ( ( ( X0 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(take_A2032349095le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) )
& ( X1 = hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) ) )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) != X2 ) ) ),
inference(flattening,[],[f2778]) ).
tff(f2784,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),nil_Ar557011903le_alt))))),
inference(cnf_transformation,[],[f2076]) ).
tff(f2785,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,nil_Ar557011903le_alt)),
inference(cnf_transformation,[],[f2]) ).
tff(f2823,plain,
! [X0: arrow_1893660431le_alt] : ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt) ),
inference(cnf_transformation,[],[f29]) ).
tff(f2838,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) ),
inference(cnf_transformation,[],[f1321]) ).
tff(f2855,plain,
! [X2: arrow_1893660431le_alt,X3: list_A114658244le_alt,X0: list_A114658244le_alt,X1: fun_Ar1448189019le_alt] : ( list_c1024366775le_alt(X0,X1,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X2),X3)) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(X1,X2),X3) ),
inference(cnf_transformation,[],[f52]) ).
tff(f2956,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,nil_Ar557011903le_alt),X1) = X0 )
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f1345]) ).
tff(f3003,plain,
! [X2: list_A114658244le_alt,X3: list_A114658244le_alt,X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),X3) )
| ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4) != X2 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ),
inference(cnf_transformation,[],[f2158]) ).
tff(f3060,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( rotate1753650700le_alt(hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt)) ),
inference(cnf_transformation,[],[f152]) ).
tff(f3122,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rev_Ar377224735le_alt(X0))) ),
inference(cnf_transformation,[],[f2198]) ).
tff(f3123,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rev_Ar377224735le_alt(X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
inference(cnf_transformation,[],[f2198]) ).
tff(f3152,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,rotate1753650700le_alt(X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
inference(cnf_transformation,[],[f2203]) ).
tff(f3290,plain,
! [X0: nat,X1: arrow_1893660431le_alt] :
( ( nil_Ar557011903le_alt = hAPP_A1382181054le_alt(replic782356601le_alt(X0),X1) )
| ( zero_zero_nat != X0 ) ),
inference(cnf_transformation,[],[f2255]) ).
tff(f3376,plain,
! [X2: list_A114658244le_alt,X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),X2))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2)))
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1449]) ).
tff(f3433,plain,
! [X0: list_A114658244le_alt] : ( rotate1753650700le_alt(X0) = list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0) ),
inference(cnf_transformation,[],[f364]) ).
tff(f3442,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) ),
inference(cnf_transformation,[],[f2300]) ).
tff(f3443,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))) ),
inference(cnf_transformation,[],[f2300]) ).
tff(f3444,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X1)) ),
inference(cnf_transformation,[],[f2300]) ).
tff(f3448,plain,
! [X2: arrow_1893660431le_alt,X0: arrow_1893660431le_alt,X1: nat] :
( ( zero_zero_nat != X1 )
| ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(X1),X2)))) ),
inference(cnf_transformation,[],[f2304]) ).
tff(f3503,plain,
! [X2: list_A114658244le_alt,X3: list_A114658244le_alt,X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3)) != X1 ) ),
inference(cnf_transformation,[],[f2338]) ).
tff(f3816,plain,
! [X0: list_A114658244le_alt] : ( rev_Ar377224735le_alt(X0) = foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,X0) ),
inference(cnf_transformation,[],[f558]) ).
tff(f4737,plain,
! [X2: list_A114658244le_alt,X0: arrow_1893660431le_alt,X1: nat] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,X1),X2))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X2))) ),
inference(cnf_transformation,[],[f2049]) ).
tff(f4755,plain,
! [X2: list_A114658244le_alt,X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),X2) = X1 )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1) != X2 ) ),
inference(cnf_transformation,[],[f2779]) ).
tff(f4784,plain,
hBOOL(fTrue),
inference(cnf_transformation,[],[f1203]) ).
tff(f4792,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f1211]) ).
tff(f4819,plain,
! [X0: bool] :
( ( fTrue = X0 )
| ( fFalse = X0 ) ),
inference(cnf_transformation,[],[f1238]) ).
tff(f4847,plain,
a != b,
inference(cnf_transformation,[],[f1266]) ).
tff(f4848,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt))))),
inference(cnf_transformation,[],[f2067]) ).
tff(f4861,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt)) = list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)) ),
inference(definition_unfolding,[],[f3060,f3433]) ).
tff(f4903,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
inference(definition_unfolding,[],[f3123,f3816]) ).
tff(f4904,plain,
! [X0: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,X0)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
inference(definition_unfolding,[],[f3122,f3816]) ).
tff(f4918,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,X0)) ),
inference(definition_unfolding,[],[f3152,f3433]) ).
tff(f5074,plain,
! [X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,nil_Ar557011903le_alt),X1) = X1 ),
inference(equality_resolution,[],[f2956]) ).
tff(f5110,plain,
! [X3: list_A114658244le_alt,X0: arrow_1893660431le_alt,X1: list_A114658244le_alt,X4: list_A114658244le_alt] :
( ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4)),X3) )
| ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3) != X1 ) ),
inference(equality_resolution,[],[f3003]) ).
tff(f5111,plain,
! [X3: list_A114658244le_alt,X0: arrow_1893660431le_alt,X4: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X4)),X3) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X4),X3)) ),
inference(equality_resolution,[],[f5110]) ).
tff(f5180,plain,
! [X1: arrow_1893660431le_alt] : ( nil_Ar557011903le_alt = hAPP_A1382181054le_alt(replic782356601le_alt(zero_zero_nat),X1) ),
inference(equality_resolution,[],[f3290]) ).
tff(f5197,plain,
! [X2: arrow_1893660431le_alt,X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_A1382181054le_alt(replic782356601le_alt(zero_zero_nat),X2)))),
inference(equality_resolution,[],[f3448]) ).
tff(f5205,plain,
! [X2: list_A114658244le_alt,X3: list_A114658244le_alt,X0: arrow_1893660431le_alt] : hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X2),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X3))))),
inference(equality_resolution,[],[f3503]) ).
tff(f5389,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,hAPP_l1084348419lt_nat(size_s2005684270le_alt,X0)),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1)) = X1 ),
inference(equality_resolution,[],[f4755]) ).
tff(f5396,definition,
sF404 = hAPP_A436723315le_alt(cons_A1647044463le_alt,a),
introduced(definition,[new_symbols(definition,[sF404])],[function_definition]) ).
tff(f5397,plain,
hAPP_A436723315le_alt(cons_A1647044463le_alt,a) = sF404,
inference(reorient_equations,[],[f5396]) ).
tff(f5398,definition,
sF405 = hAPP_A436723315le_alt(cons_A1647044463le_alt,b),
introduced(definition,[new_symbols(definition,[sF405])],[function_definition]) ).
tff(f5399,plain,
hAPP_A436723315le_alt(cons_A1647044463le_alt,b) = sF405,
inference(reorient_equations,[],[f5398]) ).
tff(f5400,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt))))),
inference(definition_folding,[],[f4848,f5399,f5397]) ).
tff(f5506,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,nil_Ar557011903le_alt))),
inference(backward_demodulation,[],[f5197,f5180]) ).
tff(f5539,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),nil_Ar557011903le_alt)) = hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0),X1) ),
inference(backward_demodulation,[],[f4861,f2855]) ).
tff(f5576,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))),
inference(backward_demodulation,[],[f5400,f2823]) ).
tff(f5614,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f2784,f2823]) ).
tff(f5651,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)) ),
inference(forward_demodulation,[],[f5539,f2823]) ).
tff(f5689,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)))),
inference(resolution,[],[f3442,f5614]) ).
tff(f5707,plain,
hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,a),nil_Ar557011903le_alt) = hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt),
inference(superposition,[],[f2823,f5397]) ).
tff(f5708,plain,
hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,b),nil_Ar557011903le_alt) = hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt),
inference(superposition,[],[f2823,f5399]) ).
tff(f5710,plain,
! [X0: arrow_1893660431le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))))),
inference(unit_resulting_resolution,[],[f4904,f5576]) ).
tff(f5921,plain,
! [X0: arrow_1893660431le_alt] :
( ~ hBOOL(fTrue)
| ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))) ) ),
inference(superposition,[],[f5710,f4819]) ).
tff(f5931,plain,
! [X0: arrow_1893660431le_alt] :
( ~ hBOOL(fTrue)
| ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))) ) ),
inference(superposition,[],[f5576,f4819]) ).
tff(f5966,plain,
! [X0: arrow_1893660431le_alt] : ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))) ),
inference(forward_subsumption_resolution,[],[f5931,f4784]) ).
tff(f5972,plain,
! [X0: arrow_1893660431le_alt] : ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))) ),
inference(forward_subsumption_resolution,[],[f5921,f4784]) ).
tff(f6226,plain,
! [X0: bool] :
( ( fFalse = X0 )
| hBOOL(X0) ),
inference(superposition,[],[f4784,f4819]) ).
tff(f6450,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(sF405,X1))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ( b = X0 ) ),
inference(superposition,[],[f3376,f5399]) ).
tff(f6451,plain,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X1),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X1),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,nil_Ar557011903le_alt)))
| ( X0 = X1 ) ),
inference(superposition,[],[f3376,f2823]) ).
tff(f6456,plain,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt] :
( ~ hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X1),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( X0 = X1 ) ),
inference(forward_subsumption_resolution,[],[f6451,f5506]) ).
tff(f6457,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF405,X1))))
| ( b = X0 )
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X1))) ),
inference(resolution,[],[f6450,f3444]) ).
tff(f6528,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,X0),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))),
inference(superposition,[],[f5205,f5074]) ).
tff(f6537,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))),
inference(resolution,[],[f6528,f3443]) ).
tff(f6597,plain,
! [X0: list_A114658244le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF404,X0)))),
inference(superposition,[],[f6537,f5397]) ).
tff(f6598,plain,
! [X0: list_A114658244le_alt] : ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(sF405,X0)))),
inference(superposition,[],[f6537,f5399]) ).
tff(f6625,plain,
! [X0: list_A114658244le_alt] : ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(sF405,X0))) ),
inference(unit_resulting_resolution,[],[f6226,f6598]) ).
tff(f6650,plain,
! [X0: list_A114658244le_alt] : ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF404,X0))) ),
inference(unit_resulting_resolution,[],[f6226,f6597]) ).
tff(f6690,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(sF404,X0)),X1) = hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),X1)) ),
inference(superposition,[],[f5111,f5397]) ).
tff(f6692,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,nil_Ar557011903le_alt),X1)) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)),X1) ),
inference(superposition,[],[f5111,f2823]) ).
tff(f6699,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] : ( hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1) = hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)),X1) ),
inference(forward_demodulation,[],[f6692,f5074]) ).
tff(f7122,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,X0))))
| ( a = b )
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X0)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X0))) ),
inference(superposition,[],[f6457,f5397]) ).
tff(f7129,plain,
! [X0: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X0)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,X0))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X0))) ),
inference(forward_subsumption_resolution,[],[f7122,f4847]) ).
tff(f7131,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1)))
| ( a = X0 ) ),
inference(resolution,[],[f7129,f3376]) ).
tff(f7133,plain,
! [X0: nat,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,X0),X1)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_n372949560le_alt(drop_A617527551le_alt,X0),X1))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,X1))) ),
inference(resolution,[],[f7129,f4737]) ).
tff(f7176,plain,
! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,nil_Ar557011903le_alt)))
| ( a = X0 ) ),
inference(superposition,[],[f7131,f2823]) ).
tff(f7183,plain,
! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( a = X0 ) ),
inference(forward_subsumption_resolution,[],[f7176,f5506]) ).
tff(f7186,plain,
! [X0: arrow_1893660431le_alt] :
( hBOOL(fFalse)
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( a = X0 ) ),
inference(forward_demodulation,[],[f7183,f5966]) ).
tff(f7189,plain,
! [X0: arrow_1893660431le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( a = X0 ) ),
inference(forward_subsumption_resolution,[],[f7186,f4792]) ).
tff(f7336,plain,
! [X0: arrow_1893660431le_alt,X1: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( X0 = X1 )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))) ),
inference(resolution,[],[f6456,f3444]) ).
tff(f7414,plain,
! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ( b = X0 )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))) ),
inference(superposition,[],[f7336,f5399]) ).
tff(f7415,plain,
! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ( a = X0 )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))) ),
inference(superposition,[],[f7336,f5707]) ).
tff(f7423,definition,
( spl406_11
<=> hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))) ),
introduced(definition,[new_symbols(definition,[spl406_11])],[avatar_definition]) ).
tff(f7425,plain,
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt)))
| spl406_11 ),
inference(avatar_component_clause,[],[f7423]) ).
tff(f7427,definition,
( spl406_12
<=> ! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ( a = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl406_12])],[avatar_definition]) ).
tff(f7428,plain,
( ! [X0: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ( a = X0 ) )
| ~ spl406_12 ),
inference(avatar_component_clause,[],[f7427]) ).
tff(f7429,plain,
( ~ spl406_11
| spl406_12 ),
inference(avatar_split_clause,[],[f7415,f7427,f7423]) ).
tff(f7447,plain,
( ( fFalse = hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt)) )
| spl406_11 ),
inference(unit_resulting_resolution,[],[f6226,f7425]) ).
tff(f7531,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)))))),
inference(unit_resulting_resolution,[],[f4918,f5614]) ).
tff(f7532,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))))),
inference(unit_resulting_resolution,[],[f4918,f5689]) ).
tff(f7539,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),X0),X1)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))) ),
inference(superposition,[],[f4918,f2855]) ).
tff(f7547,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),X1))) ),
inference(forward_demodulation,[],[f7539,f5651]) ).
tff(f7548,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7531,f2855]) ).
tff(f7549,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7532,f2855]) ).
tff(f7555,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7548,f5651]) ).
tff(f7556,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7549,f5651]) ).
tff(f7559,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7555,f5111]) ).
tff(f7560,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7556,f6699]) ).
tff(f7562,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7559,f6699]) ).
tff(f7567,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))))),
inference(unit_resulting_resolution,[],[f4918,f7562]) ).
tff(f7573,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))),
inference(resolution,[],[f7562,f3442]) ).
tff(f7579,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7567,f2855]) ).
tff(f7581,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt))),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7579,f5651]) ).
tff(f7582,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7581,f5111]) ).
tff(f7583,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))),
inference(forward_demodulation,[],[f7582,f6699]) ).
tff(f7588,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,list_c1024366775le_alt(nil_Ar557011903le_alt,cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt))))),
inference(unit_resulting_resolution,[],[f4918,f7573]) ).
tff(f7600,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cOMBB_1076781858le_alt(cOMBC_1833749623le_alt(append1597383892le_alt),hAPP_l1822938419le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt)),sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7588,f2855]) ).
tff(f7602,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7600,f5651]) ).
tff(f7603,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f7602,f6699]) ).
tff(f7614,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)))),
inference(resolution,[],[f7583,f3442]) ).
tff(f7668,plain,
! [X0: list_A114658244le_alt,X1: arrow_1893660431le_alt] :
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X0),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X1),nil_Ar557011903le_alt)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X1),hAPP_l84111627le_alt(sF404,X0)))) ),
inference(superposition,[],[f7547,f6690]) ).
tff(f8435,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))),
inference(unit_resulting_resolution,[],[f7547,f7614]) ).
tff(f8451,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK4),nil_Ar557011903le_alt)))),
inference(forward_demodulation,[],[f8435,f6699]) ).
tff(f9017,plain,
! [X0: arrow_1893660431le_alt] : hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))),
inference(unit_resulting_resolution,[],[f2838,f2785]) ).
tff(f9047,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt)))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,nil_Ar557011903le_alt)) ),
inference(superposition,[],[f2838,f5707]) ).
tff(f9053,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))),
inference(forward_subsumption_resolution,[],[f9047,f2785]) ).
tff(f9055,plain,
( hBOOL(fFalse)
| spl406_11 ),
inference(forward_demodulation,[],[f9053,f7447]) ).
tff(f9058,plain,
( $false
| spl406_11 ),
inference(forward_subsumption_resolution,[],[f9055,f4792]) ).
tff(f9059,plain,
spl406_11,
inference(avatar_contradiction_clause,[],[f9058]) ).
tff(f10275,plain,
hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK4),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt)))))),
inference(unit_resulting_resolution,[],[f4903,f7583]) ).
tff(f11821,definition,
( spl406_34
<=> ( a = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl406_34])],[avatar_definition]) ).
tff(f11823,plain,
( ( a = sK4 )
| ~ spl406_34 ),
inference(avatar_component_clause,[],[f11821]) ).
tff(f12147,definition,
( spl406_36
<=> ( b = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl406_36])],[avatar_definition]) ).
tff(f12148,plain,
( ( b != sK4 )
| spl406_36 ),
inference(avatar_component_clause,[],[f12147]) ).
tff(f12149,plain,
( ( b = sK4 )
| ~ spl406_36 ),
inference(avatar_component_clause,[],[f12147]) ).
tff(f12176,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))))
| ~ spl406_36 ),
inference(backward_demodulation,[],[f7603,f12149]) ).
tff(f12360,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))))
| ~ spl406_36 ),
inference(backward_demodulation,[],[f10275,f12149]) ).
tff(f12507,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))))
| ~ spl406_36 ),
inference(forward_demodulation,[],[f12360,f5399]) ).
tff(f12653,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK6),nil_Ar557011903le_alt))))
| ~ spl406_36 ),
inference(forward_demodulation,[],[f12176,f5399]) ).
tff(f12832,plain,
( ( a = sK6 )
| ~ spl406_36 ),
inference(resolution,[],[f12653,f7189]) ).
tff(f12991,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))))
| ~ spl406_36 ),
inference(backward_demodulation,[],[f12507,f12832]) ).
tff(f13273,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,foldl_1844370748le_alt(cOMBC_673369480le_alt(cons_A1647044463le_alt),nil_Ar557011903le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,sK5),nil_Ar557011903le_alt))))))
| ~ spl406_36 ),
inference(forward_demodulation,[],[f12991,f5397]) ).
tff(f13400,plain,
( hBOOL(fFalse)
| ~ spl406_36 ),
inference(forward_demodulation,[],[f13273,f5972]) ).
tff(f13409,plain,
( $false
| ~ spl406_36 ),
inference(forward_subsumption_resolution,[],[f13400,f4792]) ).
tff(f13410,plain,
~ spl406_36,
inference(avatar_contradiction_clause,[],[f13409]) ).
tff(f15780,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( hBOOL(hAPP_f739344229l_bool(hAPP_A1501726285l_bool(member1502664802le_alt,a),hAPP_l2018657868t_bool(set_Ar1995755744le_alt,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),X0))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X0)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,X0)))) ),
inference(superposition,[],[f7133,f5389]) ).
tff(f16062,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X0)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,X0))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),X0)))) ),
inference(resolution,[],[f15780,f3443]) ).
tff(f16076,plain,
! [X0: list_A114658244le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(hAPP_l86320102le_alt(append1597383892le_alt,X1),X0))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,X0)))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,X0)))) ),
inference(forward_demodulation,[],[f16062,f5397]) ).
tff(f16077,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt)))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,X1)))) ),
inference(resolution,[],[f16076,f7668]) ).
tff(f16096,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( hBOOL(fFalse)
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,X1)))) ),
inference(forward_demodulation,[],[f16077,f5966]) ).
tff(f16097,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))))
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,X1)))) ),
inference(forward_subsumption_resolution,[],[f16096,f4792]) ).
tff(f16098,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,X1))))
| ( b = X0 )
| ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,X0),nil_Ar557011903le_alt))) ),
inference(resolution,[],[f16097,f7414]) ).
tff(f16113,plain,
! [X0: arrow_1893660431le_alt,X1: list_A114658244le_alt] :
( ~ hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,X0),hAPP_l84111627le_alt(sF404,X1))))
| ( b = X0 ) ),
inference(forward_subsumption_resolution,[],[f16098,f9017]) ).
tff(f16124,plain,
( ! [X0: arrow_1893660431le_alt] :
( ( b = X0 )
| ( a = X0 ) )
| ~ spl406_12 ),
inference(resolution,[],[f16113,f7428]) ).
tff(f16188,plain,
( ( b != b )
| ( a = sK4 )
| ~ spl406_12
| spl406_36 ),
inference(superposition,[],[f12148,f16124]) ).
tff(f16191,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,b),nil_Ar557011903le_alt))))
| ( a = sK5 )
| ~ spl406_12 ),
inference(superposition,[],[f7560,f16124]) ).
tff(f16263,plain,
( ( a = sK4 )
| ~ spl406_12
| spl406_36 ),
inference(trivial_inequality_removal,[],[f16188]) ).
tff(f16279,definition,
( spl406_40
<=> ( a = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl406_40])],[avatar_definition]) ).
tff(f16280,plain,
( ( a != sK6 )
| spl406_40 ),
inference(avatar_component_clause,[],[f16279]) ).
tff(f16281,plain,
( ( a = sK6 )
| ~ spl406_40 ),
inference(avatar_component_clause,[],[f16279]) ).
tff(f16313,definition,
( spl406_44
<=> ( a = sK5 ) ),
introduced(definition,[new_symbols(definition,[spl406_44])],[avatar_definition]) ).
tff(f16315,plain,
( ( a = sK5 )
| ~ spl406_44 ),
inference(avatar_component_clause,[],[f16313]) ).
tff(f16369,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt))))
| ( a = sK5 )
| ~ spl406_12 ),
inference(forward_demodulation,[],[f16191,f5708]) ).
tff(f16376,plain,
( spl406_34
| ~ spl406_12
| spl406_36 ),
inference(avatar_split_clause,[],[f16263,f12147,f7427,f11821]) ).
tff(f16541,definition,
( spl406_85
<=> hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt)))) ),
introduced(definition,[new_symbols(definition,[spl406_85])],[avatar_definition]) ).
tff(f16543,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt))))
| ~ spl406_85 ),
inference(avatar_component_clause,[],[f16541]) ).
tff(f16544,plain,
( spl406_44
| spl406_85
| ~ spl406_12 ),
inference(avatar_split_clause,[],[f16369,f7427,f16541,f16313]) ).
tff(f16633,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,a),nil_Ar557011903le_alt))))
| ~ spl406_34 ),
inference(backward_demodulation,[],[f7573,f11823]) ).
tff(f16672,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(hAPP_A436723315le_alt(insert1391384533le_alt,a),nil_Ar557011903le_alt))))
| ~ spl406_34 ),
inference(backward_demodulation,[],[f8451,f11823]) ).
tff(f17321,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK5),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34 ),
inference(forward_demodulation,[],[f16672,f5707]) ).
tff(f17360,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,sK6),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34 ),
inference(forward_demodulation,[],[f16633,f5707]) ).
tff(f17706,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34
| ~ spl406_44 ),
inference(forward_demodulation,[],[f17321,f16315]) ).
tff(f17749,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,a),hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34
| ~ spl406_40 ),
inference(forward_demodulation,[],[f17360,f16281]) ).
tff(f18067,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34
| ~ spl406_44 ),
inference(forward_demodulation,[],[f17706,f5397]) ).
tff(f18095,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF404,hAPP_l84111627le_alt(sF404,nil_Ar557011903le_alt))))
| ~ spl406_34
| ~ spl406_40 ),
inference(forward_demodulation,[],[f17749,f5397]) ).
tff(f18308,plain,
( hBOOL(fFalse)
| ~ spl406_34
| ~ spl406_44 ),
inference(forward_demodulation,[],[f18067,f6650]) ).
tff(f18326,plain,
( hBOOL(fFalse)
| ~ spl406_34
| ~ spl406_40 ),
inference(forward_demodulation,[],[f18095,f6650]) ).
tff(f18566,plain,
( $false
| ~ spl406_34
| ~ spl406_44 ),
inference(forward_subsumption_resolution,[],[f18308,f4792]) ).
tff(f18567,plain,
( ~ spl406_34
| ~ spl406_44 ),
inference(avatar_contradiction_clause,[],[f18566]) ).
tff(f18580,plain,
( $false
| ~ spl406_34
| ~ spl406_40 ),
inference(forward_subsumption_resolution,[],[f18326,f4792]) ).
tff(f18581,plain,
( ~ spl406_34
| ~ spl406_40 ),
inference(avatar_contradiction_clause,[],[f18580]) ).
tff(f26229,plain,
( ( b = sK6 )
| ~ spl406_12
| spl406_40 ),
inference(unit_resulting_resolution,[],[f16124,f16280]) ).
tff(f26291,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(hAPP_A436723315le_alt(cons_A1647044463le_alt,b),hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt))))
| ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(backward_demodulation,[],[f16543,f26229]) ).
tff(f26770,plain,
( hBOOL(hAPP_l499746980t_bool(distin1654625714le_alt,hAPP_l84111627le_alt(sF405,hAPP_l84111627le_alt(sF405,nil_Ar557011903le_alt))))
| ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(forward_demodulation,[],[f26291,f5399]) ).
tff(f26817,plain,
( hBOOL(fFalse)
| ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(forward_demodulation,[],[f26770,f6625]) ).
tff(f26828,plain,
( $false
| ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(forward_subsumption_resolution,[],[f26817,f4792]) ).
tff(f26829,plain,
( ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(avatar_contradiction_clause,[],[f26828]) ).
cnf(s10,plain,
( ~ spl406_11
| spl406_12 ),
inference(sat_conversion,[],[f7429]) ).
cnf(s19,plain,
spl406_11,
inference(sat_conversion,[],[f9059]) ).
cnf(s31,plain,
~ spl406_36,
inference(sat_conversion,[],[f13410]) ).
cnf(s46,plain,
( ~ spl406_12
| spl406_34
| spl406_36 ),
inference(sat_conversion,[],[f16376]) ).
cnf(s78,plain,
( ~ spl406_12
| spl406_44
| spl406_85 ),
inference(sat_conversion,[],[f16544]) ).
cnf(s122,plain,
( ~ spl406_34
| ~ spl406_44 ),
inference(sat_conversion,[],[f18567]) ).
cnf(s127,plain,
( ~ spl406_34
| ~ spl406_40 ),
inference(sat_conversion,[],[f18581]) ).
cnf(s293,plain,
( ~ spl406_12
| spl406_40
| ~ spl406_85 ),
inference(sat_conversion,[],[f26829]) ).
cnf(s299,plain,
spl406_12,
inference(rat,[],[s10,s19]) ).
cnf(s301,plain,
spl406_34,
inference(rat,[],[s46,s31,s299]) ).
cnf(s302,plain,
~ spl406_40,
inference(rat,[],[s127,s301]) ).
cnf(s303,plain,
~ spl406_44,
inference(rat,[],[s122,s301]) ).
cnf(s306,plain,
~ spl406_85,
inference(rat,[],[s293,s299,s302]) ).
cnf(s327,plain,
$false,
inference(rat,[],[s78,s299,s306,s303]) ).
tff(f26830,plain,
$false,
inference(avatar_sat_refutation,[],[s327]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT169_3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:54:54 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.53/2.91 % (1735850)Detected formulas, will run a generic FOF schedule.
% 13.53/2.91 % (1735858)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=144678892:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.53/2.91 % (1735858)Refutation not found, incomplete strategy
% 13.53/2.91 % (1735858)------------------------------
% 13.53/2.91 % (1735858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.53/2.91 % (1735858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.53/2.91 % (1735858)CaDiCaL version: 2.1.3
% 13.53/2.91 % (1735858)Termination reason: Refutation not found, incomplete strategy
% 13.53/2.91 % (1735858)Time elapsed: 0.004 s
% 13.53/2.91 % (1735858)Peak memory usage: 89 MB
% 13.53/2.91 % (1735858)Instructions burned: 9 (million)
% 13.53/2.91 % (1735860)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=527905262:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.53/2.91 % (1735861)dis-21_1_sil=8000:lcm=predicate:random_seed=257786859:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.53/2.91 % (1735859)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4014798277:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.53/2.91 % (1735856)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3056261835:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.53/2.91 % (1735855)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2993741322:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.53/2.91 % (1735857)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1429933780:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.53/2.91 % (1735861)Instruction limit reached!
% 13.53/2.91 % (1735861)------------------------------
% 13.53/2.91 % (1735861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.53/2.91 % (1735861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.53/2.91 % (1735861)CaDiCaL version: 2.1.3
% 13.53/2.91 % (1735861)Termination reason: Instruction limit
% 13.53/2.91 % (1735861)Termination phase: Property scanning
% 13.53/2.91 % (1735861)Time elapsed: 0.059 s
% 13.53/2.91 % (1735861)Peak memory usage: 89 MB
% 13.53/2.91 % (1735861)Instructions burned: 130 (million)
% 13.53/2.91 % (1735860)Instruction limit reached!
% 13.53/2.91 % (1735860)------------------------------
% 13.53/2.91 % (1735860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.53/2.91 % (1735860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.53/2.91 % (1735860)CaDiCaL version: 2.1.3
% 13.53/2.91 % (1735860)Termination reason: Instruction limit
% 13.53/2.91 % (1735860)Termination phase: Saturation
% 13.53/2.91 % (1735860)Time elapsed: 0.065 s
% 13.53/2.91 % (1735860)Peak memory usage: 90 MB
% 13.53/2.91 % (1735860)Instructions burned: 141 (million)
% 13.53/2.91 % (1735859)Instruction limit reached!
% 13.53/2.91 % (1735859)------------------------------
% 13.53/2.91 % (1735859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.53/2.91 % (1735859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.53/2.91 % (1735859)CaDiCaL version: 2.1.3
% 13.53/2.91 % (1735859)Termination reason: Instruction limit
% 13.53/2.91 % (1735859)Termination phase: Saturation
% 13.53/2.91 % (1735859)Time elapsed: 0.069 s
% 13.53/2.91 % (1735859)Peak memory usage: 90 MB
% 13.53/2.91 % (1735859)Instructions burned: 119 (million)
% 13.53/2.91 % (1735858)------------------------------
% 13.53/2.91 % (1735858)------------------------------
% 13.53/2.91 % (1735869)lrs+10_1_sil=8000:sp=occurrence:random_seed=3633513312:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 13.53/2.91 % (1735872)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=244746649:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 13.53/2.91 % (1735871)lrs+1011_1_sil=32000:sp=occurrence:random_seed=897764235:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.53/2.91 % (1735870)lrs+10_1_sil=32000:urr=on:br=off:random_seed=606181362:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 20.31/3.83 % (1735872)Instruction limit reached!
% 20.31/3.83 % (1735872)------------------------------
% 20.31/3.83 % (1735872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735872)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735872)Termination reason: Instruction limit
% 20.31/3.83 % (1735872)Termination phase: Saturation
% 20.31/3.83 % (1735872)Time elapsed: 0.073 s
% 20.31/3.83 % (1735872)Peak memory usage: 92 MB
% 20.31/3.83 % (1735872)Instructions burned: 249 (million)
% 20.31/3.83 % (1735870)Instruction limit reached!
% 20.31/3.83 % (1735870)------------------------------
% 20.31/3.83 % (1735870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735870)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735870)Termination reason: Instruction limit
% 20.31/3.83 % (1735870)Termination phase: Saturation
% 20.31/3.83 % (1735870)Time elapsed: 0.091 s
% 20.31/3.83 % (1735870)Peak memory usage: 91 MB
% 20.31/3.83 % (1735870)Instructions burned: 158 (million)
% 20.31/3.83 % (1735869)Instruction limit reached!
% 20.31/3.83 % (1735869)------------------------------
% 20.31/3.83 % (1735869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735869)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735869)Termination reason: Instruction limit
% 20.31/3.83 % (1735869)Termination phase: Saturation
% 20.31/3.83 % (1735869)Time elapsed: 0.174 s
% 20.31/3.83 % (1735869)Peak memory usage: 92 MB
% 20.31/3.83 % (1735869)Instructions burned: 286 (million)
% 20.31/3.83 % (1735871)Instruction limit reached!
% 20.31/3.83 % (1735871)------------------------------
% 20.31/3.83 % (1735871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735871)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735871)Termination reason: Instruction limit
% 20.31/3.83 % (1735871)Termination phase: Saturation
% 20.31/3.83 % (1735871)Time elapsed: 0.178 s
% 20.31/3.83 % (1735871)Peak memory usage: 91 MB
% 20.31/3.83 % (1735871)Instructions burned: 326 (million)
% 20.31/3.83 % (1735877)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=976562590:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 20.31/3.83 % (1735877)Refutation not found, incomplete strategy
% 20.31/3.83 % (1735877)------------------------------
% 20.31/3.83 % (1735877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735877)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735877)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.83 % (1735877)Time elapsed: 0.023 s
% 20.31/3.83 % (1735877)Peak memory usage: 90 MB
% 20.31/3.83 % (1735877)Instructions burned: 78 (million)
% 20.31/3.83 % (1735878)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2234288939:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.31/3.83 % (1735879)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3430122307:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.31/3.83 % (1735880)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2274147685:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 20.31/3.83 % (1735877)------------------------------
% 20.31/3.83 % (1735877)------------------------------
% 20.31/3.83 % (1735879)Instruction limit reached!
% 20.31/3.83 % (1735879)------------------------------
% 20.31/3.83 % (1735879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.83 % (1735879)CaDiCaL version: 2.1.3
% 20.31/3.83 % (1735879)Termination reason: Instruction limit
% 20.31/3.83 % (1735879)Termination phase: Saturation
% 20.31/3.83 % (1735879)Time elapsed: 0.054 s
% 20.31/3.83 % (1735879)Peak memory usage: 90 MB
% 20.31/3.83 % (1735879)Instructions burned: 114 (million)
% 20.31/3.83 % (1735880)Instruction limit reached!
% 20.31/3.83 % (1735880)------------------------------
% 20.31/3.83 % (1735880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.83 % (1735880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735880)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735880)Termination reason: Instruction limit
% 43.67/7.07 % (1735880)Termination phase: Property scanning
% 43.67/7.07 % (1735880)Time elapsed: 0.059 s
% 43.67/7.07 % (1735880)Peak memory usage: 89 MB
% 43.67/7.07 % (1735880)Instructions burned: 129 (million)
% 43.67/7.07 % (1735885)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2468292082:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 43.67/7.07 % (1735886)lrs+10_1_sil=8000:sp=occurrence:random_seed=404686482:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 43.67/7.07 % (1735885)Instruction limit reached!
% 43.67/7.07 % (1735885)------------------------------
% 43.67/7.07 % (1735885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.67/7.07 % (1735885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735885)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735885)Termination reason: Instruction limit
% 43.67/7.07 % (1735885)Termination phase: Saturation
% 43.67/7.07 % (1735885)Time elapsed: 0.054 s
% 43.67/7.07 % (1735885)Peak memory usage: 90 MB
% 43.67/7.07 % (1735885)Instructions burned: 114 (million)
% 43.67/7.07 % (1735887)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=819741356:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 43.67/7.07 % (1735887)Refutation not found, incomplete strategy
% 43.67/7.07 % (1735887)------------------------------
% 43.67/7.07 % (1735887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.67/7.07 % (1735887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735887)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735887)Termination reason: Refutation not found, incomplete strategy
% 43.67/7.07 % (1735887)Time elapsed: 0.112 s
% 43.67/7.07 % (1735887)Peak memory usage: 93 MB
% 43.67/7.07 % (1735887)Instructions burned: 215 (million)
% 43.67/7.07 % (1735891)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3510561307:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 43.67/7.07 % (1735887)------------------------------
% 43.67/7.07 % (1735887)------------------------------
% 43.67/7.07 % (1735886)Instruction limit reached!
% 43.67/7.07 % (1735886)------------------------------
% 43.67/7.07 % (1735886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.67/7.07 % (1735886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735886)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735886)Termination reason: Instruction limit
% 43.67/7.07 % (1735886)Termination phase: Saturation
% 43.67/7.07 % (1735886)Time elapsed: 0.541 s
% 43.67/7.07 % (1735886)Peak memory usage: 97 MB
% 43.67/7.07 % (1735886)Instructions burned: 908 (million)
% 43.67/7.07 % (1735893)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2334184918:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 43.67/7.07 % (1735893)Instruction limit reached!
% 43.67/7.07 % (1735893)------------------------------
% 43.67/7.07 % (1735893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.67/7.07 % (1735893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735893)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735893)Termination reason: Instruction limit
% 43.67/7.07 % (1735893)Termination phase: Saturation
% 43.67/7.07 % (1735893)Time elapsed: 0.067 s
% 43.67/7.07 % (1735893)Peak memory usage: 91 MB
% 43.67/7.07 % (1735893)Instructions burned: 134 (million)
% 43.67/7.07 % (1735894)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2072600616:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 43.67/7.07 % (1735896)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2073583344:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 43.67/7.07 % (1735894)Instruction limit reached!
% 43.67/7.07 % (1735894)------------------------------
% 43.67/7.07 % (1735894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.67/7.07 % (1735894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.67/7.07 % (1735894)CaDiCaL version: 2.1.3
% 43.67/7.07 % (1735894)Termination reason: Instruction limit
% 43.67/7.07 % (1735894)Termination phase: Saturation
% 43.67/7.07 % (1735894)Time elapsed: 0.336 s
% 43.67/7.07 % (1735894)Peak memory usage: 96 MB
% 43.67/7.07 % (1735894)Instructions burned: 593 (million)
% 51.98/8.28 % (1735878)Instruction limit reached!
% 51.98/8.28 % (1735878)------------------------------
% 51.98/8.28 % (1735878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735878)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735878)Termination reason: Instruction limit
% 51.98/8.28 % (1735878)Termination phase: Saturation
% 51.98/8.28 % (1735878)Time elapsed: 1.378 s
% 51.98/8.28 % (1735878)Peak memory usage: 147 MB
% 51.98/8.28 % (1735878)Instructions burned: 2352 (million)
% 51.98/8.28 % (1735899)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2947271676:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 51.98/8.28 % (1735900)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=855518361:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 51.98/8.28 % (1735899)Instruction limit reached!
% 51.98/8.28 % (1735899)------------------------------
% 51.98/8.28 % (1735899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735899)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735899)Termination reason: Instruction limit
% 51.98/8.28 % (1735899)Termination phase: Saturation
% 51.98/8.28 % (1735899)Time elapsed: 0.067 s
% 51.98/8.28 % (1735899)Peak memory usage: 91 MB
% 51.98/8.28 % (1735899)Instructions burned: 126 (million)
% 51.98/8.28 % (1735900)Instruction limit reached!
% 51.98/8.28 % (1735900)------------------------------
% 51.98/8.28 % (1735900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735900)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735900)Termination reason: Instruction limit
% 51.98/8.28 % (1735900)Termination phase: Twee Goal Transformation
% 51.98/8.28 % (1735900)Time elapsed: 0.064 s
% 51.98/8.28 % (1735900)Peak memory usage: 89 MB
% 51.98/8.28 % (1735900)Instructions burned: 135 (million)
% 51.98/8.28 % (1735903)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2653452623:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 51.98/8.28 % (1735903)Refutation not found, incomplete strategy
% 51.98/8.28 % (1735903)------------------------------
% 51.98/8.28 % (1735903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735903)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735903)Termination reason: Refutation not found, incomplete strategy
% 51.98/8.28 % (1735903)Time elapsed: 0.007 s
% 51.98/8.28 % (1735903)Peak memory usage: 89 MB
% 51.98/8.28 % (1735903)Instructions burned: 8 (million)
% 51.98/8.28 % (1735904)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3655291259:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 51.98/8.28 % (1735903)------------------------------
% 51.98/8.28 % (1735903)------------------------------
% 51.98/8.28 % (1735904)Instruction limit reached!
% 51.98/8.28 % (1735904)------------------------------
% 51.98/8.28 % (1735904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735904)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735904)Termination reason: Instruction limit
% 51.98/8.28 % (1735904)Termination phase: Saturation
% 51.98/8.28 % (1735904)Time elapsed: 0.247 s
% 51.98/8.28 % (1735904)Peak memory usage: 92 MB
% 51.98/8.28 % (1735904)Instructions burned: 432 (million)
% 51.98/8.28 % (1735907)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=617907334:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 51.98/8.28 % (1735908)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=721383539:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 51.98/8.28 % (1735908)Instruction limit reached!
% 51.98/8.28 % (1735908)------------------------------
% 51.98/8.28 % (1735908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735908)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735908)Termination reason: Instruction limit
% 51.98/8.28 % (1735908)Termination phase: Saturation
% 51.98/8.28 % (1735908)Time elapsed: 0.070 s
% 51.98/8.28 % (1735908)Peak memory usage: 91 MB
% 51.98/8.28 % (1735908)Instructions burned: 150 (million)
% 51.98/8.28 % (1735911)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=894509711:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 51.98/8.28 % (1735891)Instruction limit reached!
% 51.98/8.28 % (1735891)------------------------------
% 51.98/8.28 % (1735891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735891)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735891)Termination reason: Instruction limit
% 51.98/8.28 % (1735891)Termination phase: Saturation
% 51.98/8.28 % (1735891)Time elapsed: 2.973 s
% 51.98/8.28 % (1735891)Peak memory usage: 144 MB
% 51.98/8.28 % (1735891)Instructions burned: 5204 (million)
% 51.98/8.28 % (1735913)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=774266630:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 51.98/8.28 % (1735913)Instruction limit reached!
% 51.98/8.28 % (1735913)------------------------------
% 51.98/8.28 % (1735913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735913)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735913)Termination reason: Instruction limit
% 51.98/8.28 % (1735913)Termination phase: Saturation
% 51.98/8.28 % (1735913)Time elapsed: 0.352 s
% 51.98/8.28 % (1735913)Peak memory usage: 114 MB
% 51.98/8.28 % (1735913)Instructions burned: 668 (million)
% 51.98/8.28 % (1735915)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2933787879:s2a=on:i=185:s2at=1.8:fdi=4_2952 on theBenchmark for (2952ds/185Mi)
% 51.98/8.28 % (1735915)Instruction limit reached!
% 51.98/8.28 % (1735915)------------------------------
% 51.98/8.28 % (1735915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735915)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735915)Termination reason: Instruction limit
% 51.98/8.28 % (1735915)Termination phase: Saturation
% 51.98/8.28 % (1735915)Time elapsed: 0.092 s
% 51.98/8.28 % (1735915)Peak memory usage: 92 MB
% 51.98/8.28 % (1735915)Instructions burned: 185 (million)
% 51.98/8.28 % (1735917)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3393986607:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 51.98/8.28 % (1735917)Instruction limit reached!
% 51.98/8.28 % (1735917)------------------------------
% 51.98/8.28 % (1735917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735917)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735917)Termination reason: Instruction limit
% 51.98/8.28 % (1735917)Termination phase: Saturation
% 51.98/8.28 % (1735917)Time elapsed: 0.109 s
% 51.98/8.28 % (1735917)Peak memory usage: 92 MB
% 51.98/8.28 % (1735917)Instructions burned: 193 (million)
% 51.98/8.28 % (1735919)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2695468213:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 51.98/8.28 % (1735907)Instruction limit reached!
% 51.98/8.28 % (1735907)------------------------------
% 51.98/8.28 % (1735907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.98/8.28 % (1735907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.98/8.28 % (1735907)CaDiCaL version: 2.1.3
% 51.98/8.28 % (1735907)Termination reason: Instruction limit
% 51.98/8.28 % (1735907)Termination phase: Saturation
% 51.98/8.28 % (1735907)Time elapsed: 3.198 s
% 51.98/8.28 % (1735907)Peak memory usage: 157 MB
% 51.98/8.28 % (1735907)Instructions burned: 6061 (million)
% 51.98/8.28 % (1735921)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1520454949:i=12111:sd=1:ss=included_2939 on theBenchmark for (2939ds/12111Mi)
% 51.98/8.28 % (1735911)First to succeed.
% 51.98/8.28 % (1735911)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1735850"
% 51.98/8.28 % (1735911)Refutation found. Thanks to Tanya!
% 51.98/8.28 % SZS status Theorem for theBenchmark
% 51.98/8.28 % SZS output start Proof for theBenchmark
% See solution above
% 52.50/8.38 % (1735911)------------------------------
% 52.50/8.38 % (1735911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.50/8.38 % (1735911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.50/8.38 % (1735911)CaDiCaL version: 2.1.3
% 52.50/8.38 % (1735911)Termination reason: Refutation
% 52.50/8.38 % (1735911)Time elapsed: 3.997 s
% 52.50/8.38 % (1735911)Peak memory usage: 173 MB
% 52.50/8.38 % (1735911)Instructions burned: 6516 (million)
% 52.50/8.38 % (1735911)------------------------------
% 52.50/8.38 % (1735911)------------------------------
% 52.50/8.38 % (1735850)Success in time 7.418 s
% 52.50/8.38 % Vampire exiting
%------------------------------------------------------------------------------