Vampire-SAT---5.0.1.CSA-FMo.s

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

% Computer : n014.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 01:40:13 PM UTC 2026

% Result   : CounterSatisfiable 1.17s 0.43s
% Output   : FiniteModel 1.17s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
tff('declare_$i1',type,
    'fmb_$i_1': $i ).

tff('finite_domain_$i',axiom,
    ! [X: $i] : ( X = 'fmb_$i_1' ) ).

tff(declare_exp_list_char,type,
    exp_list_char: $tType ).

tff(declare_exp_list_char1,type,
    fmb_exp_list_char_1: exp_list_char ).

tff(finite_domain_exp_list_char,axiom,
    ! [X: exp_list_char] : ( X = fmb_exp_list_char_1 ) ).

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

tff(declare_bool1,type,
    fmb_bool_1: bool ).

tff(declare_bool2,type,
    fmb_bool_2: bool ).

tff(finite_domain_bool,axiom,
    ! [X: bool] :
      ( ( X = fmb_bool_1 )
      | ( X = fmb_bool_2 ) ) ).

tff(distinct_domain_bool,axiom,
    fmb_bool_1 != fmb_bool_2 ).

tff(declare_list_exp_list_char,type,
    list_exp_list_char: $tType ).

tff(declare_list_exp_list_char1,type,
    fmb_list_exp_list_char_1: list_exp_list_char ).

tff(finite_domain_list_exp_list_char,axiom,
    ! [X: list_exp_list_char] : ( X = fmb_list_exp_list_char_1 ) ).

tff(declare_list_list_char,type,
    list_list_char: $tType ).

tff(declare_list_list_char1,type,
    fmb_list_list_char_1: list_list_char ).

tff(finite_domain_list_list_char,axiom,
    ! [X: list_list_char] : ( X = fmb_list_list_char_1 ) ).

tff(declare_list_option_ty,type,
    list_option_ty: $tType ).

tff(declare_list_option_ty1,type,
    fmb_list_option_ty_1: list_option_ty ).

tff(finite_domain_list_option_ty,axiom,
    ! [X: list_option_ty] : ( X = fmb_list_option_ty_1 ) ).

tff(declare_list_option_val,type,
    list_option_val: $tType ).

tff(declare_list_option_val1,type,
    fmb_list_option_val_1: list_option_val ).

tff(declare_list_option_val2,type,
    fmb_list_option_val_2: list_option_val ).

tff(finite_domain_list_option_val,axiom,
    ! [X: list_option_val] :
      ( ( X = fmb_list_option_val_1 )
      | ( X = fmb_list_option_val_2 ) ) ).

tff(distinct_domain_list_option_val,axiom,
    fmb_list_option_val_1 != fmb_list_option_val_2 ).

tff(declare_list_char,type,
    list_char: $tType ).

tff(declare_list_char1,type,
    fmb_list_char_1: list_char ).

tff(finite_domain_list_char,axiom,
    ! [X: list_char] : ( X = fmb_list_char_1 ) ).

tff(declare_list_ty,type,
    list_ty: $tType ).

tff(declare_list_ty1,type,
    fmb_list_ty_1: list_ty ).

tff(declare_list_ty2,type,
    fmb_list_ty_2: list_ty ).

tff(finite_domain_list_ty,axiom,
    ! [X: list_ty] :
      ( ( X = fmb_list_ty_1 )
      | ( X = fmb_list_ty_2 ) ) ).

tff(distinct_domain_list_ty,axiom,
    fmb_list_ty_1 != fmb_list_ty_2 ).

tff(declare_list_val,type,
    list_val: $tType ).

tff(declare_list_val1,type,
    fmb_list_val_1: list_val ).

tff(finite_domain_list_val,axiom,
    ! [X: list_val] : ( X = fmb_list_val_1 ) ).

tff(declare_list_P1999446415t_char,type,
    list_P1999446415t_char: $tType ).

tff(declare_list_P1999446415t_char1,type,
    fmb_list_P1999446415t_char_1: list_P1999446415t_char ).

tff(declare_list_P1999446415t_char2,type,
    fmb_list_P1999446415t_char_2: list_P1999446415t_char ).

tff(finite_domain_list_P1999446415t_char,axiom,
    ! [X: list_P1999446415t_char] :
      ( ( X = fmb_list_P1999446415t_char_1 )
      | ( X = fmb_list_P1999446415t_char_2 ) ) ).

tff(distinct_domain_list_P1999446415t_char,axiom,
    fmb_list_P1999446415t_char_1 != fmb_list_P1999446415t_char_2 ).

tff(declare_list_P1439941640on_val,type,
    list_P1439941640on_val: $tType ).

tff(declare_list_P1439941640on_val1,type,
    fmb_list_P1439941640on_val_1: list_P1439941640on_val ).

tff(declare_list_P1439941640on_val2,type,
    fmb_list_P1439941640on_val_2: list_P1439941640on_val ).

tff(finite_domain_list_P1439941640on_val,axiom,
    ! [X: list_P1439941640on_val] :
      ( ( X = fmb_list_P1439941640on_val_1 )
      | ( X = fmb_list_P1439941640on_val_2 ) ) ).

tff(distinct_domain_list_P1439941640on_val,axiom,
    fmb_list_P1439941640on_val_1 != fmb_list_P1439941640on_val_2 ).

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

tff(declare_nat1,type,
    fmb_nat_1: nat ).

tff(finite_domain_nat,axiom,
    ! [X: nat] : ( X = fmb_nat_1 ) ).

tff(declare_option_ty,type,
    option_ty: $tType ).

tff(declare_option_ty1,type,
    fmb_option_ty_1: option_ty ).

tff(declare_option_ty2,type,
    fmb_option_ty_2: option_ty ).

tff(finite_domain_option_ty,axiom,
    ! [X: option_ty] :
      ( ( X = fmb_option_ty_1 )
      | ( X = fmb_option_ty_2 ) ) ).

tff(distinct_domain_option_ty,axiom,
    fmb_option_ty_1 != fmb_option_ty_2 ).

tff(declare_option_val,type,
    option_val: $tType ).

tff(declare_option_val1,type,
    fmb_option_val_1: option_val ).

tff(declare_option_val2,type,
    fmb_option_val_2: option_val ).

tff(finite_domain_option_val,axiom,
    ! [X: option_val] :
      ( ( X = fmb_option_val_1 )
      | ( X = fmb_option_val_2 ) ) ).

tff(distinct_domain_option_val,axiom,
    fmb_option_val_1 != fmb_option_val_2 ).

tff(declare_option1479284511on_val,type,
    option1479284511on_val: $tType ).

tff(declare_option1479284511on_val1,type,
    fmb_option1479284511on_val_1: option1479284511on_val ).

tff(declare_option1479284511on_val2,type,
    fmb_option1479284511on_val_2: option1479284511on_val ).

tff(finite_domain_option1479284511on_val,axiom,
    ! [X: option1479284511on_val] :
      ( ( X = fmb_option1479284511on_val_1 )
      | ( X = fmb_option1479284511on_val_2 ) ) ).

tff(distinct_domain_option1479284511on_val,axiom,
    fmb_option1479284511on_val_1 != fmb_option1479284511on_val_2 ).

tff(declare_ty,type,
    ty: $tType ).

tff(declare_ty1,type,
    fmb_ty_1: ty ).

tff(declare_ty2,type,
    fmb_ty_2: ty ).

tff(finite_domain_ty,axiom,
    ! [X: ty] :
      ( ( X = fmb_ty_1 )
      | ( X = fmb_ty_2 ) ) ).

tff(distinct_domain_ty,axiom,
    fmb_ty_1 != fmb_ty_2 ).

tff(declare_val,type,
    val: $tType ).

tff(declare_val1,type,
    fmb_val_1: val ).

tff(declare_val2,type,
    fmb_val_2: val ).

tff(finite_domain_val,axiom,
    ! [X: val] :
      ( ( X = fmb_val_1 )
      | ( X = fmb_val_2 ) ) ).

tff(distinct_domain_val,axiom,
    fmb_val_1 != fmb_val_2 ).

tff(declare_fun_ex1654222579t_char,type,
    fun_ex1654222579t_char: $tType ).

tff(declare_fun_ex1654222579t_char1,type,
    fmb_fun_ex1654222579t_char_1: fun_ex1654222579t_char ).

tff(declare_fun_ex1654222579t_char2,type,
    fmb_fun_ex1654222579t_char_2: fun_ex1654222579t_char ).

tff(finite_domain_fun_ex1654222579t_char,axiom,
    ! [X: fun_ex1654222579t_char] :
      ( ( X = fmb_fun_ex1654222579t_char_1 )
      | ( X = fmb_fun_ex1654222579t_char_2 ) ) ).

tff(distinct_domain_fun_ex1654222579t_char,axiom,
    fmb_fun_ex1654222579t_char_1 != fmb_fun_ex1654222579t_char_2 ).

tff(declare_fun_ex736065929r_bool,type,
    fun_ex736065929r_bool: $tType ).

tff(declare_fun_ex736065929r_bool1,type,
    fmb_fun_ex736065929r_bool_1: fun_ex736065929r_bool ).

tff(declare_fun_ex736065929r_bool2,type,
    fmb_fun_ex736065929r_bool_2: fun_ex736065929r_bool ).

tff(finite_domain_fun_ex736065929r_bool,axiom,
    ! [X: fun_ex736065929r_bool] :
      ( ( X = fmb_fun_ex736065929r_bool_1 )
      | ( X = fmb_fun_ex736065929r_bool_2 ) ) ).

tff(distinct_domain_fun_ex736065929r_bool,axiom,
    fmb_fun_ex736065929r_bool_1 != fmb_fun_ex736065929r_bool_2 ).

tff(declare_fun_ex1075505132t_char,type,
    fun_ex1075505132t_char: $tType ).

tff(declare_fun_ex1075505132t_char1,type,
    fmb_fun_ex1075505132t_char_1: fun_ex1075505132t_char ).

tff(declare_fun_ex1075505132t_char2,type,
    fmb_fun_ex1075505132t_char_2: fun_ex1075505132t_char ).

tff(finite_domain_fun_ex1075505132t_char,axiom,
    ! [X: fun_ex1075505132t_char] :
      ( ( X = fmb_fun_ex1075505132t_char_1 )
      | ( X = fmb_fun_ex1075505132t_char_2 ) ) ).

tff(distinct_domain_fun_ex1075505132t_char,axiom,
    fmb_fun_ex1075505132t_char_1 != fmb_fun_ex1075505132t_char_2 ).

tff(declare_fun_ex12316946ion_ty,type,
    fun_ex12316946ion_ty: $tType ).

tff(declare_fun_ex12316946ion_ty1,type,
    fmb_fun_ex12316946ion_ty_1: fun_ex12316946ion_ty ).

tff(declare_fun_ex12316946ion_ty2,type,
    fmb_fun_ex12316946ion_ty_2: fun_ex12316946ion_ty ).

tff(finite_domain_fun_ex12316946ion_ty,axiom,
    ! [X: fun_ex12316946ion_ty] :
      ( ( X = fmb_fun_ex12316946ion_ty_1 )
      | ( X = fmb_fun_ex12316946ion_ty_2 ) ) ).

tff(distinct_domain_fun_ex12316946ion_ty,axiom,
    fmb_fun_ex12316946ion_ty_1 != fmb_fun_ex12316946ion_ty_2 ).

tff(declare_fun_ex1158871131on_val,type,
    fun_ex1158871131on_val: $tType ).

tff(declare_fun_ex1158871131on_val1,type,
    fmb_fun_ex1158871131on_val_1: fun_ex1158871131on_val ).

tff(declare_fun_ex1158871131on_val2,type,
    fmb_fun_ex1158871131on_val_2: fun_ex1158871131on_val ).

tff(finite_domain_fun_ex1158871131on_val,axiom,
    ! [X: fun_ex1158871131on_val] :
      ( ( X = fmb_fun_ex1158871131on_val_1 )
      | ( X = fmb_fun_ex1158871131on_val_2 ) ) ).

tff(distinct_domain_fun_ex1158871131on_val,axiom,
    fmb_fun_ex1158871131on_val_1 != fmb_fun_ex1158871131on_val_2 ).

tff(declare_fun_exp_list_char_ty,type,
    fun_exp_list_char_ty: $tType ).

tff(declare_fun_exp_list_char_ty1,type,
    fmb_fun_exp_list_char_ty_1: fun_exp_list_char_ty ).

tff(declare_fun_exp_list_char_ty2,type,
    fmb_fun_exp_list_char_ty_2: fun_exp_list_char_ty ).

tff(finite_domain_fun_exp_list_char_ty,axiom,
    ! [X: fun_exp_list_char_ty] :
      ( ( X = fmb_fun_exp_list_char_ty_1 )
      | ( X = fmb_fun_exp_list_char_ty_2 ) ) ).

tff(distinct_domain_fun_exp_list_char_ty,axiom,
    fmb_fun_exp_list_char_ty_1 != fmb_fun_exp_list_char_ty_2 ).

tff(declare_fun_ex793263652ar_val,type,
    fun_ex793263652ar_val: $tType ).

tff(declare_fun_ex793263652ar_val1,type,
    fmb_fun_ex793263652ar_val_1: fun_ex793263652ar_val ).

tff(declare_fun_ex793263652ar_val2,type,
    fmb_fun_ex793263652ar_val_2: fun_ex793263652ar_val ).

tff(finite_domain_fun_ex793263652ar_val,axiom,
    ! [X: fun_ex793263652ar_val] :
      ( ( X = fmb_fun_ex793263652ar_val_1 )
      | ( X = fmb_fun_ex793263652ar_val_2 ) ) ).

tff(distinct_domain_fun_ex793263652ar_val,axiom,
    fmb_fun_ex793263652ar_val_1 != fmb_fun_ex793263652ar_val_2 ).

tff(declare_fun_ex1708156690y_bool,type,
    fun_ex1708156690y_bool: $tType ).

tff(declare_fun_ex1708156690y_bool1,type,
    fmb_fun_ex1708156690y_bool_1: fun_ex1708156690y_bool ).

tff(declare_fun_ex1708156690y_bool2,type,
    fmb_fun_ex1708156690y_bool_2: fun_ex1708156690y_bool ).

tff(finite_domain_fun_ex1708156690y_bool,axiom,
    ! [X: fun_ex1708156690y_bool] :
      ( ( X = fmb_fun_ex1708156690y_bool_1 )
      | ( X = fmb_fun_ex1708156690y_bool_2 ) ) ).

tff(distinct_domain_fun_ex1708156690y_bool,axiom,
    fmb_fun_ex1708156690y_bool_1 != fmb_fun_ex1708156690y_bool_2 ).

tff(declare_fun_ex1201926843l_bool,type,
    fun_ex1201926843l_bool: $tType ).

tff(declare_fun_ex1201926843l_bool1,type,
    fmb_fun_ex1201926843l_bool_1: fun_ex1201926843l_bool ).

tff(declare_fun_ex1201926843l_bool2,type,
    fmb_fun_ex1201926843l_bool_2: fun_ex1201926843l_bool ).

tff(finite_domain_fun_ex1201926843l_bool,axiom,
    ! [X: fun_ex1201926843l_bool] :
      ( ( X = fmb_fun_ex1201926843l_bool_1 )
      | ( X = fmb_fun_ex1201926843l_bool_2 ) ) ).

tff(distinct_domain_fun_ex1201926843l_bool,axiom,
    fmb_fun_ex1201926843l_bool_1 != fmb_fun_ex1201926843l_bool_2 ).

tff(declare_fun_ex1732915347on_val,type,
    fun_ex1732915347on_val: $tType ).

tff(declare_fun_ex1732915347on_val1,type,
    fmb_fun_ex1732915347on_val_1: fun_ex1732915347on_val ).

tff(declare_fun_ex1732915347on_val2,type,
    fmb_fun_ex1732915347on_val_2: fun_ex1732915347on_val ).

tff(finite_domain_fun_ex1732915347on_val,axiom,
    ! [X: fun_ex1732915347on_val] :
      ( ( X = fmb_fun_ex1732915347on_val_1 )
      | ( X = fmb_fun_ex1732915347on_val_2 ) ) ).

tff(distinct_domain_fun_ex1732915347on_val,axiom,
    fmb_fun_ex1732915347on_val_1 != fmb_fun_ex1732915347on_val_2 ).

tff(declare_fun_li1279027773t_char,type,
    fun_li1279027773t_char: $tType ).

tff(declare_fun_li1279027773t_char1,type,
    fmb_fun_li1279027773t_char_1: fun_li1279027773t_char ).

tff(declare_fun_li1279027773t_char2,type,
    fmb_fun_li1279027773t_char_2: fun_li1279027773t_char ).

tff(finite_domain_fun_li1279027773t_char,axiom,
    ! [X: fun_li1279027773t_char] :
      ( ( X = fmb_fun_li1279027773t_char_1 )
      | ( X = fmb_fun_li1279027773t_char_2 ) ) ).

tff(distinct_domain_fun_li1279027773t_char,axiom,
    fmb_fun_li1279027773t_char_1 != fmb_fun_li1279027773t_char_2 ).

tff(declare_fun_li218321462t_char,type,
    fun_li218321462t_char: $tType ).

tff(declare_fun_li218321462t_char1,type,
    fmb_fun_li218321462t_char_1: fun_li218321462t_char ).

tff(declare_fun_li218321462t_char2,type,
    fmb_fun_li218321462t_char_2: fun_li218321462t_char ).

tff(finite_domain_fun_li218321462t_char,axiom,
    ! [X: fun_li218321462t_char] :
      ( ( X = fmb_fun_li218321462t_char_1 )
      | ( X = fmb_fun_li218321462t_char_2 ) ) ).

tff(distinct_domain_fun_li218321462t_char,axiom,
    fmb_fun_li218321462t_char_1 != fmb_fun_li218321462t_char_2 ).

tff(declare_fun_li241576028ion_ty,type,
    fun_li241576028ion_ty: $tType ).

tff(declare_fun_li241576028ion_ty1,type,
    fmb_fun_li241576028ion_ty_1: fun_li241576028ion_ty ).

tff(declare_fun_li241576028ion_ty2,type,
    fmb_fun_li241576028ion_ty_2: fun_li241576028ion_ty ).

tff(finite_domain_fun_li241576028ion_ty,axiom,
    ! [X: fun_li241576028ion_ty] :
      ( ( X = fmb_fun_li241576028ion_ty_1 )
      | ( X = fmb_fun_li241576028ion_ty_2 ) ) ).

tff(distinct_domain_fun_li241576028ion_ty,axiom,
    fmb_fun_li241576028ion_ty_1 != fmb_fun_li241576028ion_ty_2 ).

tff(declare_fun_li690207653on_val,type,
    fun_li690207653on_val: $tType ).

tff(declare_fun_li690207653on_val1,type,
    fmb_fun_li690207653on_val_1: fun_li690207653on_val ).

tff(declare_fun_li690207653on_val2,type,
    fmb_fun_li690207653on_val_2: fun_li690207653on_val ).

tff(finite_domain_fun_li690207653on_val,axiom,
    ! [X: fun_li690207653on_val] :
      ( ( X = fmb_fun_li690207653on_val_1 )
      | ( X = fmb_fun_li690207653on_val_2 ) ) ).

tff(distinct_domain_fun_li690207653on_val,axiom,
    fmb_fun_li690207653on_val_1 != fmb_fun_li690207653on_val_2 ).

tff(declare_fun_li1055333287ist_ty,type,
    fun_li1055333287ist_ty: $tType ).

tff(declare_fun_li1055333287ist_ty1,type,
    fmb_fun_li1055333287ist_ty_1: fun_li1055333287ist_ty ).

tff(declare_fun_li1055333287ist_ty2,type,
    fmb_fun_li1055333287ist_ty_2: fun_li1055333287ist_ty ).

tff(finite_domain_fun_li1055333287ist_ty,axiom,
    ! [X: fun_li1055333287ist_ty] :
      ( ( X = fmb_fun_li1055333287ist_ty_1 )
      | ( X = fmb_fun_li1055333287ist_ty_2 ) ) ).

tff(distinct_domain_fun_li1055333287ist_ty,axiom,
    fmb_fun_li1055333287ist_ty_1 != fmb_fun_li1055333287ist_ty_2 ).

tff(declare_fun_li363341936st_val,type,
    fun_li363341936st_val: $tType ).

tff(declare_fun_li363341936st_val1,type,
    fmb_fun_li363341936st_val_1: fun_li363341936st_val ).

tff(declare_fun_li363341936st_val2,type,
    fmb_fun_li363341936st_val_2: fun_li363341936st_val ).

tff(finite_domain_fun_li363341936st_val,axiom,
    ! [X: fun_li363341936st_val] :
      ( ( X = fmb_fun_li363341936st_val_1 )
      | ( X = fmb_fun_li363341936st_val_2 ) ) ).

tff(distinct_domain_fun_li363341936st_val,axiom,
    fmb_fun_li363341936st_val_1 != fmb_fun_li363341936st_val_2 ).

tff(declare_fun_li1581546589on_val,type,
    fun_li1581546589on_val: $tType ).

tff(declare_fun_li1581546589on_val1,type,
    fmb_fun_li1581546589on_val_1: fun_li1581546589on_val ).

tff(declare_fun_li1581546589on_val2,type,
    fmb_fun_li1581546589on_val_2: fun_li1581546589on_val ).

tff(finite_domain_fun_li1581546589on_val,axiom,
    ! [X: fun_li1581546589on_val] :
      ( ( X = fmb_fun_li1581546589on_val_1 )
      | ( X = fmb_fun_li1581546589on_val_2 ) ) ).

tff(distinct_domain_fun_li1581546589on_val,axiom,
    fmb_fun_li1581546589on_val_1 != fmb_fun_li1581546589on_val_2 ).

tff(declare_fun_li567129860t_char,type,
    fun_li567129860t_char: $tType ).

tff(declare_fun_li567129860t_char1,type,
    fmb_fun_li567129860t_char_1: fun_li567129860t_char ).

tff(declare_fun_li567129860t_char2,type,
    fmb_fun_li567129860t_char_2: fun_li567129860t_char ).

tff(finite_domain_fun_li567129860t_char,axiom,
    ! [X: fun_li567129860t_char] :
      ( ( X = fmb_fun_li567129860t_char_1 )
      | ( X = fmb_fun_li567129860t_char_2 ) ) ).

tff(distinct_domain_fun_li567129860t_char,axiom,
    fmb_fun_li567129860t_char_1 != fmb_fun_li567129860t_char_2 ).

tff(declare_fun_li1898638973t_char,type,
    fun_li1898638973t_char: $tType ).

tff(declare_fun_li1898638973t_char1,type,
    fmb_fun_li1898638973t_char_1: fun_li1898638973t_char ).

tff(declare_fun_li1898638973t_char2,type,
    fmb_fun_li1898638973t_char_2: fun_li1898638973t_char ).

tff(finite_domain_fun_li1898638973t_char,axiom,
    ! [X: fun_li1898638973t_char] :
      ( ( X = fmb_fun_li1898638973t_char_1 )
      | ( X = fmb_fun_li1898638973t_char_2 ) ) ).

tff(distinct_domain_fun_li1898638973t_char,axiom,
    fmb_fun_li1898638973t_char_1 != fmb_fun_li1898638973t_char_2 ).

tff(declare_fun_li1921893539ion_ty,type,
    fun_li1921893539ion_ty: $tType ).

tff(declare_fun_li1921893539ion_ty1,type,
    fmb_fun_li1921893539ion_ty_1: fun_li1921893539ion_ty ).

tff(declare_fun_li1921893539ion_ty2,type,
    fmb_fun_li1921893539ion_ty_2: fun_li1921893539ion_ty ).

tff(finite_domain_fun_li1921893539ion_ty,axiom,
    ! [X: fun_li1921893539ion_ty] :
      ( ( X = fmb_fun_li1921893539ion_ty_1 )
      | ( X = fmb_fun_li1921893539ion_ty_2 ) ) ).

tff(distinct_domain_fun_li1921893539ion_ty,axiom,
    fmb_fun_li1921893539ion_ty_1 != fmb_fun_li1921893539ion_ty_2 ).

tff(declare_fun_li1580442732on_val,type,
    fun_li1580442732on_val: $tType ).

tff(declare_fun_li1580442732on_val1,type,
    fmb_fun_li1580442732on_val_1: fun_li1580442732on_val ).

tff(declare_fun_li1580442732on_val2,type,
    fmb_fun_li1580442732on_val_2: fun_li1580442732on_val ).

tff(finite_domain_fun_li1580442732on_val,axiom,
    ! [X: fun_li1580442732on_val] :
      ( ( X = fmb_fun_li1580442732on_val_1 )
      | ( X = fmb_fun_li1580442732on_val_2 ) ) ).

tff(distinct_domain_fun_li1580442732on_val,axiom,
    fmb_fun_li1580442732on_val_1 != fmb_fun_li1580442732on_val_2 ).

tff(declare_fun_li490940192ist_ty,type,
    fun_li490940192ist_ty: $tType ).

tff(declare_fun_li490940192ist_ty1,type,
    fmb_fun_li490940192ist_ty_1: fun_li490940192ist_ty ).

tff(declare_fun_li490940192ist_ty2,type,
    fmb_fun_li490940192ist_ty_2: fun_li490940192ist_ty ).

tff(finite_domain_fun_li490940192ist_ty,axiom,
    ! [X: fun_li490940192ist_ty] :
      ( ( X = fmb_fun_li490940192ist_ty_1 )
      | ( X = fmb_fun_li490940192ist_ty_2 ) ) ).

tff(distinct_domain_fun_li490940192ist_ty,axiom,
    fmb_fun_li490940192ist_ty_1 != fmb_fun_li490940192ist_ty_2 ).

tff(declare_fun_li742655849st_val,type,
    fun_li742655849st_val: $tType ).

tff(declare_fun_li742655849st_val1,type,
    fmb_fun_li742655849st_val_1: fun_li742655849st_val ).

tff(declare_fun_li742655849st_val2,type,
    fmb_fun_li742655849st_val_2: fun_li742655849st_val ).

tff(finite_domain_fun_li742655849st_val,axiom,
    ! [X: fun_li742655849st_val] :
      ( ( X = fmb_fun_li742655849st_val_1 )
      | ( X = fmb_fun_li742655849st_val_2 ) ) ).

tff(distinct_domain_fun_li742655849st_val,axiom,
    fmb_fun_li742655849st_val_1 != fmb_fun_li742655849st_val_2 ).

tff(declare_fun_li1867552164on_val,type,
    fun_li1867552164on_val: $tType ).

tff(declare_fun_li1867552164on_val1,type,
    fmb_fun_li1867552164on_val_1: fun_li1867552164on_val ).

tff(declare_fun_li1867552164on_val2,type,
    fmb_fun_li1867552164on_val_2: fun_li1867552164on_val ).

tff(finite_domain_fun_li1867552164on_val,axiom,
    ! [X: fun_li1867552164on_val] :
      ( ( X = fmb_fun_li1867552164on_val_1 )
      | ( X = fmb_fun_li1867552164on_val_2 ) ) ).

tff(distinct_domain_fun_li1867552164on_val,axiom,
    fmb_fun_li1867552164on_val_1 != fmb_fun_li1867552164on_val_2 ).

tff(declare_fun_li1024794712r_bool,type,
    fun_li1024794712r_bool: $tType ).

tff(declare_fun_li1024794712r_bool1,type,
    fmb_fun_li1024794712r_bool_1: fun_li1024794712r_bool ).

tff(declare_fun_li1024794712r_bool2,type,
    fmb_fun_li1024794712r_bool_2: fun_li1024794712r_bool ).

tff(finite_domain_fun_li1024794712r_bool,axiom,
    ! [X: fun_li1024794712r_bool] :
      ( ( X = fmb_fun_li1024794712r_bool_1 )
      | ( X = fmb_fun_li1024794712r_bool_2 ) ) ).

tff(distinct_domain_fun_li1024794712r_bool,axiom,
    fmb_fun_li1024794712r_bool_1 != fmb_fun_li1024794712r_bool_2 ).

tff(declare_fun_li156600670t_char,type,
    fun_li156600670t_char: $tType ).

tff(declare_fun_li156600670t_char1,type,
    fmb_fun_li156600670t_char_1: fun_li156600670t_char ).

tff(declare_fun_li156600670t_char2,type,
    fmb_fun_li156600670t_char_2: fun_li156600670t_char ).

tff(finite_domain_fun_li156600670t_char,axiom,
    ! [X: fun_li156600670t_char] :
      ( ( X = fmb_fun_li156600670t_char_1 )
      | ( X = fmb_fun_li156600670t_char_2 ) ) ).

tff(distinct_domain_fun_li156600670t_char,axiom,
    fmb_fun_li156600670t_char_1 != fmb_fun_li156600670t_char_2 ).

tff(declare_fun_li712717783t_char,type,
    fun_li712717783t_char: $tType ).

tff(declare_fun_li712717783t_char1,type,
    fmb_fun_li712717783t_char_1: fun_li712717783t_char ).

tff(declare_fun_li712717783t_char2,type,
    fmb_fun_li712717783t_char_2: fun_li712717783t_char ).

tff(finite_domain_fun_li712717783t_char,axiom,
    ! [X: fun_li712717783t_char] :
      ( ( X = fmb_fun_li712717783t_char_1 )
      | ( X = fmb_fun_li712717783t_char_2 ) ) ).

tff(distinct_domain_fun_li712717783t_char,axiom,
    fmb_fun_li712717783t_char_1 != fmb_fun_li712717783t_char_2 ).

tff(declare_fun_li735972349ion_ty,type,
    fun_li735972349ion_ty: $tType ).

tff(declare_fun_li735972349ion_ty1,type,
    fmb_fun_li735972349ion_ty_1: fun_li735972349ion_ty ).

tff(declare_fun_li735972349ion_ty2,type,
    fmb_fun_li735972349ion_ty_2: fun_li735972349ion_ty ).

tff(finite_domain_fun_li735972349ion_ty,axiom,
    ! [X: fun_li735972349ion_ty] :
      ( ( X = fmb_fun_li735972349ion_ty_1 )
      | ( X = fmb_fun_li735972349ion_ty_2 ) ) ).

tff(distinct_domain_fun_li735972349ion_ty,axiom,
    fmb_fun_li735972349ion_ty_1 != fmb_fun_li735972349ion_ty_2 ).

tff(declare_fun_li202512966ist_ty,type,
    fun_li202512966ist_ty: $tType ).

tff(declare_fun_li202512966ist_ty1,type,
    fmb_fun_li202512966ist_ty_1: fun_li202512966ist_ty ).

tff(declare_fun_li202512966ist_ty2,type,
    fmb_fun_li202512966ist_ty_2: fun_li202512966ist_ty ).

tff(finite_domain_fun_li202512966ist_ty,axiom,
    ! [X: fun_li202512966ist_ty] :
      ( ( X = fmb_fun_li202512966ist_ty_1 )
      | ( X = fmb_fun_li202512966ist_ty_2 ) ) ).

tff(distinct_domain_fun_li202512966ist_ty,axiom,
    fmb_fun_li202512966ist_ty_1 != fmb_fun_li202512966ist_ty_2 ).

tff(declare_fun_li1333774223st_val,type,
    fun_li1333774223st_val: $tType ).

tff(declare_fun_li1333774223st_val1,type,
    fmb_fun_li1333774223st_val_1: fun_li1333774223st_val ).

tff(declare_fun_li1333774223st_val2,type,
    fmb_fun_li1333774223st_val_2: fun_li1333774223st_val ).

tff(finite_domain_fun_li1333774223st_val,axiom,
    ! [X: fun_li1333774223st_val] :
      ( ( X = fmb_fun_li1333774223st_val_1 )
      | ( X = fmb_fun_li1333774223st_val_2 ) ) ).

tff(distinct_domain_fun_li1333774223st_val,axiom,
    fmb_fun_li1333774223st_val_1 != fmb_fun_li1333774223st_val_2 ).

tff(declare_fun_li1459524056st_val,type,
    fun_li1459524056st_val: $tType ).

tff(declare_fun_li1459524056st_val1,type,
    fmb_fun_li1459524056st_val_1: fun_li1459524056st_val ).

tff(declare_fun_li1459524056st_val2,type,
    fmb_fun_li1459524056st_val_2: fun_li1459524056st_val ).

tff(finite_domain_fun_li1459524056st_val,axiom,
    ! [X: fun_li1459524056st_val] :
      ( ( X = fmb_fun_li1459524056st_val_1 )
      | ( X = fmb_fun_li1459524056st_val_2 ) ) ).

tff(distinct_domain_fun_li1459524056st_val,axiom,
    fmb_fun_li1459524056st_val_1 != fmb_fun_li1459524056st_val_2 ).

tff(declare_fun_li978641004t_char,type,
    fun_li978641004t_char: $tType ).

tff(declare_fun_li978641004t_char1,type,
    fmb_fun_li978641004t_char_1: fun_li978641004t_char ).

tff(declare_fun_li978641004t_char2,type,
    fmb_fun_li978641004t_char_2: fun_li978641004t_char ).

tff(finite_domain_fun_li978641004t_char,axiom,
    ! [X: fun_li978641004t_char] :
      ( ( X = fmb_fun_li978641004t_char_1 )
      | ( X = fmb_fun_li978641004t_char_2 ) ) ).

tff(distinct_domain_fun_li978641004t_char,axiom,
    fmb_fun_li978641004t_char_1 != fmb_fun_li978641004t_char_2 ).

tff(declare_fun_list_char_bool,type,
    fun_list_char_bool: $tType ).

tff(declare_fun_list_char_bool1,type,
    fmb_fun_list_char_bool_1: fun_list_char_bool ).

tff(declare_fun_list_char_bool2,type,
    fmb_fun_list_char_bool_2: fun_list_char_bool ).

tff(finite_domain_fun_list_char_bool,axiom,
    ! [X: fun_list_char_bool] :
      ( ( X = fmb_fun_list_char_bool_1 )
      | ( X = fmb_fun_list_char_bool_2 ) ) ).

tff(distinct_domain_fun_list_char_bool,axiom,
    fmb_fun_list_char_bool_1 != fmb_fun_list_char_bool_2 ).

tff(declare_fun_li1751394789t_char,type,
    fun_li1751394789t_char: $tType ).

tff(declare_fun_li1751394789t_char1,type,
    fmb_fun_li1751394789t_char_1: fun_li1751394789t_char ).

tff(declare_fun_li1751394789t_char2,type,
    fmb_fun_li1751394789t_char_2: fun_li1751394789t_char ).

tff(finite_domain_fun_li1751394789t_char,axiom,
    ! [X: fun_li1751394789t_char] :
      ( ( X = fmb_fun_li1751394789t_char_1 )
      | ( X = fmb_fun_li1751394789t_char_2 ) ) ).

tff(distinct_domain_fun_li1751394789t_char,axiom,
    fmb_fun_li1751394789t_char_1 != fmb_fun_li1751394789t_char_2 ).

tff(declare_fun_li688206603ion_ty,type,
    fun_li688206603ion_ty: $tType ).

tff(declare_fun_li688206603ion_ty1,type,
    fmb_fun_li688206603ion_ty_1: fun_li688206603ion_ty ).

tff(declare_fun_li688206603ion_ty2,type,
    fmb_fun_li688206603ion_ty_2: fun_li688206603ion_ty ).

tff(finite_domain_fun_li688206603ion_ty,axiom,
    ! [X: fun_li688206603ion_ty] :
      ( ( X = fmb_fun_li688206603ion_ty_1 )
      | ( X = fmb_fun_li688206603ion_ty_2 ) ) ).

tff(distinct_domain_fun_li688206603ion_ty,axiom,
    fmb_fun_li688206603ion_ty_1 != fmb_fun_li688206603ion_ty_2 ).

tff(declare_fun_li1432931796on_val,type,
    fun_li1432931796on_val: $tType ).

tff(declare_fun_li1432931796on_val1,type,
    fmb_fun_li1432931796on_val_1: fun_li1432931796on_val ).

tff(finite_domain_fun_li1432931796on_val,axiom,
    ! [X: fun_li1432931796on_val] : ( X = fmb_fun_li1432931796on_val_1 ) ).

tff(declare_fun_list_char_ty,type,
    fun_list_char_ty: $tType ).

tff(declare_fun_list_char_ty1,type,
    fmb_fun_list_char_ty_1: fun_list_char_ty ).

tff(declare_fun_list_char_ty2,type,
    fmb_fun_list_char_ty_2: fun_list_char_ty ).

tff(finite_domain_fun_list_char_ty,axiom,
    ! [X: fun_list_char_ty] :
      ( ( X = fmb_fun_list_char_ty_1 )
      | ( X = fmb_fun_list_char_ty_2 ) ) ).

tff(distinct_domain_fun_list_char_ty,axiom,
    fmb_fun_list_char_ty_1 != fmb_fun_list_char_ty_2 ).

tff(declare_fun_list_char_val,type,
    fun_list_char_val: $tType ).

tff(declare_fun_list_char_val1,type,
    fmb_fun_list_char_val_1: fun_list_char_val ).

tff(declare_fun_list_char_val2,type,
    fmb_fun_list_char_val_2: fun_list_char_val ).

tff(finite_domain_fun_list_char_val,axiom,
    ! [X: fun_list_char_val] :
      ( ( X = fmb_fun_list_char_val_1 )
      | ( X = fmb_fun_list_char_val_2 ) ) ).

tff(distinct_domain_fun_list_char_val,axiom,
    fmb_fun_list_char_val_1 != fmb_fun_list_char_val_2 ).

tff(declare_fun_li1351943641y_bool,type,
    fun_li1351943641y_bool: $tType ).

tff(declare_fun_li1351943641y_bool1,type,
    fmb_fun_li1351943641y_bool_1: fun_li1351943641y_bool ).

tff(declare_fun_li1351943641y_bool2,type,
    fmb_fun_li1351943641y_bool_2: fun_li1351943641y_bool ).

tff(finite_domain_fun_li1351943641y_bool,axiom,
    ! [X: fun_li1351943641y_bool] :
      ( ( X = fmb_fun_li1351943641y_bool_1 )
      | ( X = fmb_fun_li1351943641y_bool_2 ) ) ).

tff(distinct_domain_fun_li1351943641y_bool,axiom,
    fmb_fun_li1351943641y_bool_1 != fmb_fun_li1351943641y_bool_2 ).

tff(declare_fun_li823162622l_bool,type,
    fun_li823162622l_bool: $tType ).

tff(declare_fun_li823162622l_bool1,type,
    fmb_fun_li823162622l_bool_1: fun_li823162622l_bool ).

tff(declare_fun_li823162622l_bool2,type,
    fmb_fun_li823162622l_bool_2: fun_li823162622l_bool ).

tff(finite_domain_fun_li823162622l_bool,axiom,
    ! [X: fun_li823162622l_bool] :
      ( ( X = fmb_fun_li823162622l_bool_1 )
      | ( X = fmb_fun_li823162622l_bool_2 ) ) ).

tff(distinct_domain_fun_li823162622l_bool,axiom,
    fmb_fun_li823162622l_bool_1 != fmb_fun_li823162622l_bool_2 ).

tff(declare_fun_li2145367436on_val,type,
    fun_li2145367436on_val: $tType ).

tff(declare_fun_li2145367436on_val1,type,
    fmb_fun_li2145367436on_val_1: fun_li2145367436on_val ).

tff(declare_fun_li2145367436on_val2,type,
    fmb_fun_li2145367436on_val_2: fun_li2145367436on_val ).

tff(finite_domain_fun_li2145367436on_val,axiom,
    ! [X: fun_li2145367436on_val] :
      ( ( X = fmb_fun_li2145367436on_val_1 )
      | ( X = fmb_fun_li2145367436on_val_2 ) ) ).

tff(distinct_domain_fun_li2145367436on_val,axiom,
    fmb_fun_li2145367436on_val_1 != fmb_fun_li2145367436on_val_2 ).

tff(declare_fun_li1975737011t_char,type,
    fun_li1975737011t_char: $tType ).

tff(declare_fun_li1975737011t_char1,type,
    fmb_fun_li1975737011t_char_1: fun_li1975737011t_char ).

tff(declare_fun_li1975737011t_char2,type,
    fmb_fun_li1975737011t_char_2: fun_li1975737011t_char ).

tff(finite_domain_fun_li1975737011t_char,axiom,
    ! [X: fun_li1975737011t_char] :
      ( ( X = fmb_fun_li1975737011t_char_1 )
      | ( X = fmb_fun_li1975737011t_char_2 ) ) ).

tff(distinct_domain_fun_li1975737011t_char,axiom,
    fmb_fun_li1975737011t_char_1 != fmb_fun_li1975737011t_char_2 ).

tff(declare_fun_li2094888364t_char,type,
    fun_li2094888364t_char: $tType ).

tff(declare_fun_li2094888364t_char1,type,
    fmb_fun_li2094888364t_char_1: fun_li2094888364t_char ).

tff(declare_fun_li2094888364t_char2,type,
    fmb_fun_li2094888364t_char_2: fun_li2094888364t_char ).

tff(finite_domain_fun_li2094888364t_char,axiom,
    ! [X: fun_li2094888364t_char] :
      ( ( X = fmb_fun_li2094888364t_char_1 )
      | ( X = fmb_fun_li2094888364t_char_2 ) ) ).

tff(distinct_domain_fun_li2094888364t_char,axiom,
    fmb_fun_li2094888364t_char_1 != fmb_fun_li2094888364t_char_2 ).

tff(declare_fun_li2118142930ion_ty,type,
    fun_li2118142930ion_ty: $tType ).

tff(declare_fun_li2118142930ion_ty1,type,
    fmb_fun_li2118142930ion_ty_1: fun_li2118142930ion_ty ).

tff(declare_fun_li2118142930ion_ty2,type,
    fmb_fun_li2118142930ion_ty_2: fun_li2118142930ion_ty ).

tff(finite_domain_fun_li2118142930ion_ty,axiom,
    ! [X: fun_li2118142930ion_ty] :
      ( ( X = fmb_fun_li2118142930ion_ty_1 )
      | ( X = fmb_fun_li2118142930ion_ty_2 ) ) ).

tff(distinct_domain_fun_li2118142930ion_ty,axiom,
    fmb_fun_li2118142930ion_ty_1 != fmb_fun_li2118142930ion_ty_2 ).

tff(declare_fun_li1110934555on_val,type,
    fun_li1110934555on_val: $tType ).

tff(declare_fun_li1110934555on_val1,type,
    fmb_fun_li1110934555on_val_1: fun_li1110934555on_val ).

tff(declare_fun_li1110934555on_val2,type,
    fmb_fun_li1110934555on_val_2: fun_li1110934555on_val ).

tff(finite_domain_fun_li1110934555on_val,axiom,
    ! [X: fun_li1110934555on_val] :
      ( ( X = fmb_fun_li1110934555on_val_1 )
      | ( X = fmb_fun_li1110934555on_val_2 ) ) ).

tff(distinct_domain_fun_li1110934555on_val,axiom,
    fmb_fun_li1110934555on_val_1 != fmb_fun_li1110934555on_val_2 ).

tff(declare_fun_list_ty_list_ty,type,
    fun_list_ty_list_ty: $tType ).

tff(declare_fun_list_ty_list_ty1,type,
    fmb_fun_list_ty_list_ty_1: fun_list_ty_list_ty ).

tff(declare_fun_list_ty_list_ty2,type,
    fmb_fun_list_ty_list_ty_2: fun_list_ty_list_ty ).

tff(finite_domain_fun_list_ty_list_ty,axiom,
    ! [X: fun_list_ty_list_ty] :
      ( ( X = fmb_fun_list_ty_list_ty_1 )
      | ( X = fmb_fun_list_ty_list_ty_2 ) ) ).

tff(distinct_domain_fun_list_ty_list_ty,axiom,
    fmb_fun_list_ty_list_ty_1 != fmb_fun_list_ty_list_ty_2 ).

tff(declare_fun_list_ty_list_val,type,
    fun_list_ty_list_val: $tType ).

tff(declare_fun_list_ty_list_val1,type,
    fmb_fun_list_ty_list_val_1: fun_list_ty_list_val ).

tff(declare_fun_list_ty_list_val2,type,
    fmb_fun_list_ty_list_val_2: fun_list_ty_list_val ).

tff(finite_domain_fun_list_ty_list_val,axiom,
    ! [X: fun_list_ty_list_val] :
      ( ( X = fmb_fun_list_ty_list_val_1 )
      | ( X = fmb_fun_list_ty_list_val_2 ) ) ).

tff(distinct_domain_fun_list_ty_list_val,axiom,
    fmb_fun_list_ty_list_val_1 != fmb_fun_list_ty_list_val_2 ).

tff(declare_fun_li1883640275on_val,type,
    fun_li1883640275on_val: $tType ).

tff(declare_fun_li1883640275on_val1,type,
    fmb_fun_li1883640275on_val_1: fun_li1883640275on_val ).

tff(declare_fun_li1883640275on_val2,type,
    fmb_fun_li1883640275on_val_2: fun_li1883640275on_val ).

tff(finite_domain_fun_li1883640275on_val,axiom,
    ! [X: fun_li1883640275on_val] :
      ( ( X = fmb_fun_li1883640275on_val_1 )
      | ( X = fmb_fun_li1883640275on_val_2 ) ) ).

tff(distinct_domain_fun_li1883640275on_val,axiom,
    fmb_fun_li1883640275on_val_1 != fmb_fun_li1883640275on_val_2 ).

tff(declare_fun_li887890578r_bool,type,
    fun_li887890578r_bool: $tType ).

tff(declare_fun_li887890578r_bool1,type,
    fmb_fun_li887890578r_bool_1: fun_li887890578r_bool ).

tff(declare_fun_li887890578r_bool2,type,
    fmb_fun_li887890578r_bool_2: fun_li887890578r_bool ).

tff(finite_domain_fun_li887890578r_bool,axiom,
    ! [X: fun_li887890578r_bool] :
      ( ( X = fmb_fun_li887890578r_bool_1 )
      | ( X = fmb_fun_li887890578r_bool_2 ) ) ).

tff(distinct_domain_fun_li887890578r_bool,axiom,
    fmb_fun_li887890578r_bool_1 != fmb_fun_li887890578r_bool_2 ).

tff(declare_fun_li430210730t_char,type,
    fun_li430210730t_char: $tType ).

tff(declare_fun_li430210730t_char1,type,
    fmb_fun_li430210730t_char_1: fun_li430210730t_char ).

tff(declare_fun_li430210730t_char2,type,
    fmb_fun_li430210730t_char_2: fun_li430210730t_char ).

tff(finite_domain_fun_li430210730t_char,axiom,
    ! [X: fun_li430210730t_char] :
      ( ( X = fmb_fun_li430210730t_char_1 )
      | ( X = fmb_fun_li430210730t_char_2 ) ) ).

tff(distinct_domain_fun_li430210730t_char,axiom,
    fmb_fun_li430210730t_char_1 != fmb_fun_li430210730t_char_2 ).

tff(declare_fun_li1120813347t_char,type,
    fun_li1120813347t_char: $tType ).

tff(declare_fun_li1120813347t_char1,type,
    fmb_fun_li1120813347t_char_1: fun_li1120813347t_char ).

tff(declare_fun_li1120813347t_char2,type,
    fmb_fun_li1120813347t_char_2: fun_li1120813347t_char ).

tff(finite_domain_fun_li1120813347t_char,axiom,
    ! [X: fun_li1120813347t_char] :
      ( ( X = fmb_fun_li1120813347t_char_1 )
      | ( X = fmb_fun_li1120813347t_char_2 ) ) ).

tff(distinct_domain_fun_li1120813347t_char,axiom,
    fmb_fun_li1120813347t_char_1 != fmb_fun_li1120813347t_char_2 ).

tff(declare_fun_li1144067913ion_ty,type,
    fun_li1144067913ion_ty: $tType ).

tff(declare_fun_li1144067913ion_ty1,type,
    fmb_fun_li1144067913ion_ty_1: fun_li1144067913ion_ty ).

tff(declare_fun_li1144067913ion_ty2,type,
    fmb_fun_li1144067913ion_ty_2: fun_li1144067913ion_ty ).

tff(finite_domain_fun_li1144067913ion_ty,axiom,
    ! [X: fun_li1144067913ion_ty] :
      ( ( X = fmb_fun_li1144067913ion_ty_1 )
      | ( X = fmb_fun_li1144067913ion_ty_2 ) ) ).

tff(distinct_domain_fun_li1144067913ion_ty,axiom,
    fmb_fun_li1144067913ion_ty_1 != fmb_fun_li1144067913ion_ty_2 ).

tff(declare_fun_li1091306514on_val,type,
    fun_li1091306514on_val: $tType ).

tff(declare_fun_li1091306514on_val1,type,
    fmb_fun_li1091306514on_val_1: fun_li1091306514on_val ).

tff(declare_fun_li1091306514on_val2,type,
    fmb_fun_li1091306514on_val_2: fun_li1091306514on_val ).

tff(finite_domain_fun_li1091306514on_val,axiom,
    ! [X: fun_li1091306514on_val] :
      ( ( X = fmb_fun_li1091306514on_val_1 )
      | ( X = fmb_fun_li1091306514on_val_2 ) ) ).

tff(distinct_domain_fun_li1091306514on_val,axiom,
    fmb_fun_li1091306514on_val_1 != fmb_fun_li1091306514on_val_2 ).

tff(declare_fun_list_val_list_ty,type,
    fun_list_val_list_ty: $tType ).

tff(declare_fun_list_val_list_ty1,type,
    fmb_fun_list_val_list_ty_1: fun_list_val_list_ty ).

tff(declare_fun_list_val_list_ty2,type,
    fmb_fun_list_val_list_ty_2: fun_list_val_list_ty ).

tff(finite_domain_fun_list_val_list_ty,axiom,
    ! [X: fun_list_val_list_ty] :
      ( ( X = fmb_fun_list_val_list_ty_1 )
      | ( X = fmb_fun_list_val_list_ty_2 ) ) ).

tff(distinct_domain_fun_list_val_list_ty,axiom,
    fmb_fun_list_val_list_ty_1 != fmb_fun_list_val_list_ty_2 ).

tff(declare_fun_li1707879747st_val,type,
    fun_li1707879747st_val: $tType ).

tff(declare_fun_li1707879747st_val1,type,
    fmb_fun_li1707879747st_val_1: fun_li1707879747st_val ).

tff(declare_fun_li1707879747st_val2,type,
    fmb_fun_li1707879747st_val_2: fun_li1707879747st_val ).

tff(finite_domain_fun_li1707879747st_val,axiom,
    ! [X: fun_li1707879747st_val] :
      ( ( X = fmb_fun_li1707879747st_val_1 )
      | ( X = fmb_fun_li1707879747st_val_2 ) ) ).

tff(distinct_domain_fun_li1707879747st_val,axiom,
    fmb_fun_li1707879747st_val_1 != fmb_fun_li1707879747st_val_2 ).

tff(declare_fun_li1659202122on_val,type,
    fun_li1659202122on_val: $tType ).

tff(declare_fun_li1659202122on_val1,type,
    fmb_fun_li1659202122on_val_1: fun_li1659202122on_val ).

tff(declare_fun_li1659202122on_val2,type,
    fmb_fun_li1659202122on_val_2: fun_li1659202122on_val ).

tff(finite_domain_fun_li1659202122on_val,axiom,
    ! [X: fun_li1659202122on_val] :
      ( ( X = fmb_fun_li1659202122on_val_1 )
      | ( X = fmb_fun_li1659202122on_val_2 ) ) ).

tff(distinct_domain_fun_li1659202122on_val,axiom,
    fmb_fun_li1659202122on_val_1 != fmb_fun_li1659202122on_val_2 ).

tff(declare_fun_li826105035r_bool,type,
    fun_li826105035r_bool: $tType ).

tff(declare_fun_li826105035r_bool1,type,
    fmb_fun_li826105035r_bool_1: fun_li826105035r_bool ).

tff(declare_fun_li826105035r_bool2,type,
    fmb_fun_li826105035r_bool_2: fun_li826105035r_bool ).

tff(finite_domain_fun_li826105035r_bool,axiom,
    ! [X: fun_li826105035r_bool] :
      ( ( X = fmb_fun_li826105035r_bool_1 )
      | ( X = fmb_fun_li826105035r_bool_2 ) ) ).

tff(distinct_domain_fun_li826105035r_bool,axiom,
    fmb_fun_li826105035r_bool_1 != fmb_fun_li826105035r_bool_2 ).

tff(declare_fun_li1479469629on_val,type,
    fun_li1479469629on_val: $tType ).

tff(declare_fun_li1479469629on_val1,type,
    fmb_fun_li1479469629on_val_1: fun_li1479469629on_val ).

tff(declare_fun_li1479469629on_val2,type,
    fmb_fun_li1479469629on_val_2: fun_li1479469629on_val ).

tff(finite_domain_fun_li1479469629on_val,axiom,
    ! [X: fun_li1479469629on_val] :
      ( ( X = fmb_fun_li1479469629on_val_1 )
      | ( X = fmb_fun_li1479469629on_val_2 ) ) ).

tff(distinct_domain_fun_li1479469629on_val,axiom,
    fmb_fun_li1479469629on_val_1 != fmb_fun_li1479469629on_val_2 ).

tff(declare_fun_na939144002on_val,type,
    fun_na939144002on_val: $tType ).

tff(declare_fun_na939144002on_val1,type,
    fmb_fun_na939144002on_val_1: fun_na939144002on_val ).

tff(finite_domain_fun_na939144002on_val,axiom,
    ! [X: fun_na939144002on_val] : ( X = fmb_fun_na939144002on_val_1 ) ).

tff(declare_fun_op1508857234t_char,type,
    fun_op1508857234t_char: $tType ).

tff(declare_fun_op1508857234t_char1,type,
    fmb_fun_op1508857234t_char_1: fun_op1508857234t_char ).

tff(declare_fun_op1508857234t_char2,type,
    fmb_fun_op1508857234t_char_2: fun_op1508857234t_char ).

tff(finite_domain_fun_op1508857234t_char,axiom,
    ! [X: fun_op1508857234t_char] :
      ( ( X = fmb_fun_op1508857234t_char_1 )
      | ( X = fmb_fun_op1508857234t_char_2 ) ) ).

tff(distinct_domain_fun_op1508857234t_char,axiom,
    fmb_fun_op1508857234t_char_1 != fmb_fun_op1508857234t_char_2 ).

tff(declare_fun_option_ty_bool,type,
    fun_option_ty_bool: $tType ).

tff(declare_fun_option_ty_bool1,type,
    fmb_fun_option_ty_bool_1: fun_option_ty_bool ).

tff(declare_fun_option_ty_bool2,type,
    fmb_fun_option_ty_bool_2: fun_option_ty_bool ).

tff(finite_domain_fun_option_ty_bool,axiom,
    ! [X: fun_option_ty_bool] :
      ( ( X = fmb_fun_option_ty_bool_1 )
      | ( X = fmb_fun_option_ty_bool_2 ) ) ).

tff(distinct_domain_fun_option_ty_bool,axiom,
    fmb_fun_option_ty_bool_1 != fmb_fun_option_ty_bool_2 ).

tff(declare_fun_op195029515t_char,type,
    fun_op195029515t_char: $tType ).

tff(declare_fun_op195029515t_char1,type,
    fmb_fun_op195029515t_char_1: fun_op195029515t_char ).

tff(declare_fun_op195029515t_char2,type,
    fmb_fun_op195029515t_char_2: fun_op195029515t_char ).

tff(finite_domain_fun_op195029515t_char,axiom,
    ! [X: fun_op195029515t_char] :
      ( ( X = fmb_fun_op195029515t_char_1 )
      | ( X = fmb_fun_op195029515t_char_2 ) ) ).

tff(distinct_domain_fun_op195029515t_char,axiom,
    fmb_fun_op195029515t_char_1 != fmb_fun_op195029515t_char_2 ).

tff(declare_fun_op1279324977ion_ty,type,
    fun_op1279324977ion_ty: $tType ).

tff(declare_fun_op1279324977ion_ty1,type,
    fmb_fun_op1279324977ion_ty_1: fun_op1279324977ion_ty ).

tff(declare_fun_op1279324977ion_ty2,type,
    fmb_fun_op1279324977ion_ty_2: fun_op1279324977ion_ty ).

tff(finite_domain_fun_op1279324977ion_ty,axiom,
    ! [X: fun_op1279324977ion_ty] :
      ( ( X = fmb_fun_op1279324977ion_ty_1 )
      | ( X = fmb_fun_op1279324977ion_ty_2 ) ) ).

tff(distinct_domain_fun_op1279324977ion_ty,axiom,
    fmb_fun_op1279324977ion_ty_1 != fmb_fun_op1279324977ion_ty_2 ).

tff(declare_fun_option_ty_ty,type,
    fun_option_ty_ty: $tType ).

tff(declare_fun_option_ty_ty1,type,
    fmb_fun_option_ty_ty_1: fun_option_ty_ty ).

tff(declare_fun_option_ty_ty2,type,
    fmb_fun_option_ty_ty_2: fun_option_ty_ty ).

tff(finite_domain_fun_option_ty_ty,axiom,
    ! [X: fun_option_ty_ty] :
      ( ( X = fmb_fun_option_ty_ty_1 )
      | ( X = fmb_fun_option_ty_ty_2 ) ) ).

tff(distinct_domain_fun_option_ty_ty,axiom,
    fmb_fun_option_ty_ty_1 != fmb_fun_option_ty_ty_2 ).

tff(declare_fun_option_ty_val,type,
    fun_option_ty_val: $tType ).

tff(declare_fun_option_ty_val1,type,
    fmb_fun_option_ty_val_1: fun_option_ty_val ).

tff(declare_fun_option_ty_val2,type,
    fmb_fun_option_ty_val_2: fun_option_ty_val ).

tff(finite_domain_fun_option_ty_val,axiom,
    ! [X: fun_option_ty_val] :
      ( ( X = fmb_fun_option_ty_val_1 )
      | ( X = fmb_fun_option_ty_val_2 ) ) ).

tff(distinct_domain_fun_option_ty_val,axiom,
    fmb_fun_option_ty_val_1 != fmb_fun_option_ty_val_2 ).

tff(declare_fun_op14579988r_bool,type,
    fun_op14579988r_bool: $tType ).

tff(declare_fun_op14579988r_bool1,type,
    fmb_fun_op14579988r_bool_1: fun_op14579988r_bool ).

tff(declare_fun_op14579988r_bool2,type,
    fmb_fun_op14579988r_bool_2: fun_op14579988r_bool ).

tff(finite_domain_fun_op14579988r_bool,axiom,
    ! [X: fun_op14579988r_bool] :
      ( ( X = fmb_fun_op14579988r_bool_1 )
      | ( X = fmb_fun_op14579988r_bool_2 ) ) ).

tff(distinct_domain_fun_op14579988r_bool,axiom,
    fmb_fun_op14579988r_bool_1 != fmb_fun_op14579988r_bool_2 ).

tff(declare_fun_op668690445r_bool,type,
    fun_op668690445r_bool: $tType ).

tff(declare_fun_op668690445r_bool1,type,
    fmb_fun_op668690445r_bool_1: fun_op668690445r_bool ).

tff(declare_fun_op668690445r_bool2,type,
    fmb_fun_op668690445r_bool_2: fun_op668690445r_bool ).

tff(finite_domain_fun_op668690445r_bool,axiom,
    ! [X: fun_op668690445r_bool] :
      ( ( X = fmb_fun_op668690445r_bool_1 )
      | ( X = fmb_fun_op668690445r_bool_2 ) ) ).

tff(distinct_domain_fun_op668690445r_bool,axiom,
    fmb_fun_op668690445r_bool_1 != fmb_fun_op668690445r_bool_2 ).

tff(declare_fun_op174240306y_bool,type,
    fun_op174240306y_bool: $tType ).

tff(declare_fun_op174240306y_bool1,type,
    fmb_fun_op174240306y_bool_1: fun_op174240306y_bool ).

tff(declare_fun_op174240306y_bool2,type,
    fmb_fun_op174240306y_bool_2: fun_op174240306y_bool ).

tff(finite_domain_fun_op174240306y_bool,axiom,
    ! [X: fun_op174240306y_bool] :
      ( ( X = fmb_fun_op174240306y_bool_1 )
      | ( X = fmb_fun_op174240306y_bool_2 ) ) ).

tff(distinct_domain_fun_op174240306y_bool,axiom,
    fmb_fun_op174240306y_bool_1 != fmb_fun_op174240306y_bool_2 ).

tff(declare_fun_op1696804347l_bool,type,
    fun_op1696804347l_bool: $tType ).

tff(declare_fun_op1696804347l_bool1,type,
    fmb_fun_op1696804347l_bool_1: fun_op1696804347l_bool ).

tff(declare_fun_op1696804347l_bool2,type,
    fmb_fun_op1696804347l_bool_2: fun_op1696804347l_bool ).

tff(finite_domain_fun_op1696804347l_bool,axiom,
    ! [X: fun_op1696804347l_bool] :
      ( ( X = fmb_fun_op1696804347l_bool_1 )
      | ( X = fmb_fun_op1696804347l_bool_2 ) ) ).

tff(distinct_domain_fun_op1696804347l_bool,axiom,
    fmb_fun_op1696804347l_bool_1 != fmb_fun_op1696804347l_bool_2 ).

tff(declare_fun_option_val_val,type,
    fun_option_val_val: $tType ).

tff(declare_fun_option_val_val1,type,
    fmb_fun_option_val_val_1: fun_option_val_val ).

tff(declare_fun_option_val_val2,type,
    fmb_fun_option_val_val_2: fun_option_val_val ).

tff(finite_domain_fun_option_val_val,axiom,
    ! [X: fun_option_val_val] :
      ( ( X = fmb_fun_option_val_val_1 )
      | ( X = fmb_fun_option_val_val_2 ) ) ).

tff(distinct_domain_fun_option_val_val,axiom,
    fmb_fun_option_val_val_1 != fmb_fun_option_val_val_2 ).

tff(declare_fun_op498348476on_val,type,
    fun_op498348476on_val: $tType ).

tff(declare_fun_op498348476on_val1,type,
    fmb_fun_op498348476on_val_1: fun_op498348476on_val ).

tff(declare_fun_op498348476on_val2,type,
    fmb_fun_op498348476on_val_2: fun_op498348476on_val ).

tff(finite_domain_fun_op498348476on_val,axiom,
    ! [X: fun_op498348476on_val] :
      ( ( X = fmb_fun_op498348476on_val_1 )
      | ( X = fmb_fun_op498348476on_val_2 ) ) ).

tff(distinct_domain_fun_op498348476on_val,axiom,
    fmb_fun_op498348476on_val_1 != fmb_fun_op498348476on_val_2 ).

tff(declare_fun_ty_exp_list_char,type,
    fun_ty_exp_list_char: $tType ).

tff(declare_fun_ty_exp_list_char1,type,
    fmb_fun_ty_exp_list_char_1: fun_ty_exp_list_char ).

tff(declare_fun_ty_exp_list_char2,type,
    fmb_fun_ty_exp_list_char_2: fun_ty_exp_list_char ).

tff(finite_domain_fun_ty_exp_list_char,axiom,
    ! [X: fun_ty_exp_list_char] :
      ( ( X = fmb_fun_ty_exp_list_char_1 )
      | ( X = fmb_fun_ty_exp_list_char_2 ) ) ).

tff(distinct_domain_fun_ty_exp_list_char,axiom,
    fmb_fun_ty_exp_list_char_1 != fmb_fun_ty_exp_list_char_2 ).

tff(declare_fun_ty_bool,type,
    fun_ty_bool: $tType ).

tff(declare_fun_ty_bool1,type,
    fmb_fun_ty_bool_1: fun_ty_bool ).

tff(declare_fun_ty_bool2,type,
    fmb_fun_ty_bool_2: fun_ty_bool ).

tff(finite_domain_fun_ty_bool,axiom,
    ! [X: fun_ty_bool] :
      ( ( X = fmb_fun_ty_bool_1 )
      | ( X = fmb_fun_ty_bool_2 ) ) ).

tff(distinct_domain_fun_ty_bool,axiom,
    fmb_fun_ty_bool_1 != fmb_fun_ty_bool_2 ).

tff(declare_fun_ty_list_char,type,
    fun_ty_list_char: $tType ).

tff(declare_fun_ty_list_char1,type,
    fmb_fun_ty_list_char_1: fun_ty_list_char ).

tff(declare_fun_ty_list_char2,type,
    fmb_fun_ty_list_char_2: fun_ty_list_char ).

tff(finite_domain_fun_ty_list_char,axiom,
    ! [X: fun_ty_list_char] :
      ( ( X = fmb_fun_ty_list_char_1 )
      | ( X = fmb_fun_ty_list_char_2 ) ) ).

tff(distinct_domain_fun_ty_list_char,axiom,
    fmb_fun_ty_list_char_1 != fmb_fun_ty_list_char_2 ).

tff(declare_fun_ty_option_ty,type,
    fun_ty_option_ty: $tType ).

tff(declare_fun_ty_option_ty1,type,
    fmb_fun_ty_option_ty_1: fun_ty_option_ty ).

tff(declare_fun_ty_option_ty2,type,
    fmb_fun_ty_option_ty_2: fun_ty_option_ty ).

tff(finite_domain_fun_ty_option_ty,axiom,
    ! [X: fun_ty_option_ty] :
      ( ( X = fmb_fun_ty_option_ty_1 )
      | ( X = fmb_fun_ty_option_ty_2 ) ) ).

tff(distinct_domain_fun_ty_option_ty,axiom,
    fmb_fun_ty_option_ty_1 != fmb_fun_ty_option_ty_2 ).

tff(declare_fun_ty_option_val,type,
    fun_ty_option_val: $tType ).

tff(declare_fun_ty_option_val1,type,
    fmb_fun_ty_option_val_1: fun_ty_option_val ).

tff(declare_fun_ty_option_val2,type,
    fmb_fun_ty_option_val_2: fun_ty_option_val ).

tff(finite_domain_fun_ty_option_val,axiom,
    ! [X: fun_ty_option_val] :
      ( ( X = fmb_fun_ty_option_val_1 )
      | ( X = fmb_fun_ty_option_val_2 ) ) ).

tff(distinct_domain_fun_ty_option_val,axiom,
    fmb_fun_ty_option_val_1 != fmb_fun_ty_option_val_2 ).

tff(declare_fun_ty_ty,type,
    fun_ty_ty: $tType ).

tff(declare_fun_ty_ty1,type,
    fmb_fun_ty_ty_1: fun_ty_ty ).

tff(declare_fun_ty_ty2,type,
    fmb_fun_ty_ty_2: fun_ty_ty ).

tff(finite_domain_fun_ty_ty,axiom,
    ! [X: fun_ty_ty] :
      ( ( X = fmb_fun_ty_ty_1 )
      | ( X = fmb_fun_ty_ty_2 ) ) ).

tff(distinct_domain_fun_ty_ty,axiom,
    fmb_fun_ty_ty_1 != fmb_fun_ty_ty_2 ).

tff(declare_fun_ty_val,type,
    fun_ty_val: $tType ).

tff(declare_fun_ty_val1,type,
    fmb_fun_ty_val_1: fun_ty_val ).

tff(declare_fun_ty_val2,type,
    fmb_fun_ty_val_2: fun_ty_val ).

tff(finite_domain_fun_ty_val,axiom,
    ! [X: fun_ty_val] :
      ( ( X = fmb_fun_ty_val_1 )
      | ( X = fmb_fun_ty_val_2 ) ) ).

tff(distinct_domain_fun_ty_val,axiom,
    fmb_fun_ty_val_1 != fmb_fun_ty_val_2 ).

tff(declare_fun_ty1580608948y_bool,type,
    fun_ty1580608948y_bool: $tType ).

tff(declare_fun_ty1580608948y_bool1,type,
    fmb_fun_ty1580608948y_bool_1: fun_ty1580608948y_bool ).

tff(declare_fun_ty1580608948y_bool2,type,
    fmb_fun_ty1580608948y_bool_2: fun_ty1580608948y_bool ).

tff(finite_domain_fun_ty1580608948y_bool,axiom,
    ! [X: fun_ty1580608948y_bool] :
      ( ( X = fmb_fun_ty1580608948y_bool_1 )
      | ( X = fmb_fun_ty1580608948y_bool_2 ) ) ).

tff(distinct_domain_fun_ty1580608948y_bool,axiom,
    fmb_fun_ty1580608948y_bool_1 != fmb_fun_ty1580608948y_bool_2 ).

tff(declare_fun_ty_fun_ty_bool,type,
    fun_ty_fun_ty_bool: $tType ).

tff(declare_fun_ty_fun_ty_bool1,type,
    fmb_fun_ty_fun_ty_bool_1: fun_ty_fun_ty_bool ).

tff(declare_fun_ty_fun_ty_bool2,type,
    fmb_fun_ty_fun_ty_bool_2: fun_ty_fun_ty_bool ).

tff(finite_domain_fun_ty_fun_ty_bool,axiom,
    ! [X: fun_ty_fun_ty_bool] :
      ( ( X = fmb_fun_ty_fun_ty_bool_1 )
      | ( X = fmb_fun_ty_fun_ty_bool_2 ) ) ).

tff(distinct_domain_fun_ty_fun_ty_bool,axiom,
    fmb_fun_ty_fun_ty_bool_1 != fmb_fun_ty_fun_ty_bool_2 ).

tff(declare_fun_ty2028523121on_val,type,
    fun_ty2028523121on_val: $tType ).

tff(declare_fun_ty2028523121on_val1,type,
    fmb_fun_ty2028523121on_val_1: fun_ty2028523121on_val ).

tff(declare_fun_ty2028523121on_val2,type,
    fmb_fun_ty2028523121on_val_2: fun_ty2028523121on_val ).

tff(finite_domain_fun_ty2028523121on_val,axiom,
    ! [X: fun_ty2028523121on_val] :
      ( ( X = fmb_fun_ty2028523121on_val_1 )
      | ( X = fmb_fun_ty2028523121on_val_2 ) ) ).

tff(distinct_domain_fun_ty2028523121on_val,axiom,
    fmb_fun_ty2028523121on_val_1 != fmb_fun_ty2028523121on_val_2 ).

tff(declare_fun_va223928858t_char,type,
    fun_va223928858t_char: $tType ).

tff(declare_fun_va223928858t_char1,type,
    fmb_fun_va223928858t_char_1: fun_va223928858t_char ).

tff(declare_fun_va223928858t_char2,type,
    fmb_fun_va223928858t_char_2: fun_va223928858t_char ).

tff(finite_domain_fun_va223928858t_char,axiom,
    ! [X: fun_va223928858t_char] :
      ( ( X = fmb_fun_va223928858t_char_1 )
      | ( X = fmb_fun_va223928858t_char_2 ) ) ).

tff(distinct_domain_fun_va223928858t_char,axiom,
    fmb_fun_va223928858t_char_1 != fmb_fun_va223928858t_char_2 ).

tff(declare_fun_val_bool,type,
    fun_val_bool: $tType ).

tff(declare_fun_val_bool1,type,
    fmb_fun_val_bool_1: fun_val_bool ).

tff(declare_fun_val_bool2,type,
    fmb_fun_val_bool_2: fun_val_bool ).

tff(finite_domain_fun_val_bool,axiom,
    ! [X: fun_val_bool] :
      ( ( X = fmb_fun_val_bool_1 )
      | ( X = fmb_fun_val_bool_2 ) ) ).

tff(distinct_domain_fun_val_bool,axiom,
    fmb_fun_val_bool_1 != fmb_fun_val_bool_2 ).

tff(declare_fun_val_list_char,type,
    fun_val_list_char: $tType ).

tff(declare_fun_val_list_char1,type,
    fmb_fun_val_list_char_1: fun_val_list_char ).

tff(declare_fun_val_list_char2,type,
    fmb_fun_val_list_char_2: fun_val_list_char ).

tff(finite_domain_fun_val_list_char,axiom,
    ! [X: fun_val_list_char] :
      ( ( X = fmb_fun_val_list_char_1 )
      | ( X = fmb_fun_val_list_char_2 ) ) ).

tff(distinct_domain_fun_val_list_char,axiom,
    fmb_fun_val_list_char_1 != fmb_fun_val_list_char_2 ).

tff(declare_fun_val_option_ty,type,
    fun_val_option_ty: $tType ).

tff(declare_fun_val_option_ty1,type,
    fmb_fun_val_option_ty_1: fun_val_option_ty ).

tff(declare_fun_val_option_ty2,type,
    fmb_fun_val_option_ty_2: fun_val_option_ty ).

tff(finite_domain_fun_val_option_ty,axiom,
    ! [X: fun_val_option_ty] :
      ( ( X = fmb_fun_val_option_ty_1 )
      | ( X = fmb_fun_val_option_ty_2 ) ) ).

tff(distinct_domain_fun_val_option_ty,axiom,
    fmb_fun_val_option_ty_1 != fmb_fun_val_option_ty_2 ).

tff(declare_fun_val_option_val,type,
    fun_val_option_val: $tType ).

tff(declare_fun_val_option_val1,type,
    fmb_fun_val_option_val_1: fun_val_option_val ).

tff(declare_fun_val_option_val2,type,
    fmb_fun_val_option_val_2: fun_val_option_val ).

tff(finite_domain_fun_val_option_val,axiom,
    ! [X: fun_val_option_val] :
      ( ( X = fmb_fun_val_option_val_1 )
      | ( X = fmb_fun_val_option_val_2 ) ) ).

tff(distinct_domain_fun_val_option_val,axiom,
    fmb_fun_val_option_val_1 != fmb_fun_val_option_val_2 ).

tff(declare_fun_val_ty,type,
    fun_val_ty: $tType ).

tff(declare_fun_val_ty1,type,
    fmb_fun_val_ty_1: fun_val_ty ).

tff(declare_fun_val_ty2,type,
    fmb_fun_val_ty_2: fun_val_ty ).

tff(finite_domain_fun_val_ty,axiom,
    ! [X: fun_val_ty] :
      ( ( X = fmb_fun_val_ty_1 )
      | ( X = fmb_fun_val_ty_2 ) ) ).

tff(distinct_domain_fun_val_ty,axiom,
    fmb_fun_val_ty_1 != fmb_fun_val_ty_2 ).

tff(declare_fun_val_val,type,
    fun_val_val: $tType ).

tff(declare_fun_val_val1,type,
    fmb_fun_val_val_1: fun_val_val ).

tff(declare_fun_val_val2,type,
    fmb_fun_val_val_2: fun_val_val ).

tff(finite_domain_fun_val_val,axiom,
    ! [X: fun_val_val] :
      ( ( X = fmb_fun_val_val_1 )
      | ( X = fmb_fun_val_val_2 ) ) ).

tff(distinct_domain_fun_val_val,axiom,
    fmb_fun_val_val_1 != fmb_fun_val_val_2 ).

tff(declare_fun_va642468779y_bool,type,
    fun_va642468779y_bool: $tType ).

tff(declare_fun_va642468779y_bool1,type,
    fmb_fun_va642468779y_bool_1: fun_va642468779y_bool ).

tff(declare_fun_va642468779y_bool2,type,
    fmb_fun_va642468779y_bool_2: fun_va642468779y_bool ).

tff(finite_domain_fun_va642468779y_bool,axiom,
    ! [X: fun_va642468779y_bool] :
      ( ( X = fmb_fun_va642468779y_bool_1 )
      | ( X = fmb_fun_va642468779y_bool_2 ) ) ).

tff(distinct_domain_fun_va642468779y_bool,axiom,
    fmb_fun_va642468779y_bool_1 != fmb_fun_va642468779y_bool_2 ).

tff(declare_fun_val_fun_ty_bool,type,
    fun_val_fun_ty_bool: $tType ).

tff(declare_fun_val_fun_ty_bool1,type,
    fmb_fun_val_fun_ty_bool_1: fun_val_fun_ty_bool ).

tff(declare_fun_val_fun_ty_bool2,type,
    fmb_fun_val_fun_ty_bool_2: fun_val_fun_ty_bool ).

tff(finite_domain_fun_val_fun_ty_bool,axiom,
    ! [X: fun_val_fun_ty_bool] :
      ( ( X = fmb_fun_val_fun_ty_bool_1 )
      | ( X = fmb_fun_val_fun_ty_bool_2 ) ) ).

tff(distinct_domain_fun_val_fun_ty_bool,axiom,
    fmb_fun_val_fun_ty_bool_1 != fmb_fun_val_fun_ty_bool_2 ).

tff(declare_fun_va172965946on_val,type,
    fun_va172965946on_val: $tType ).

tff(declare_fun_va172965946on_val1,type,
    fmb_fun_va172965946on_val_1: fun_va172965946on_val ).

tff(declare_fun_va172965946on_val2,type,
    fmb_fun_va172965946on_val_2: fun_va172965946on_val ).

tff(finite_domain_fun_va172965946on_val,axiom,
    ! [X: fun_va172965946on_val] :
      ( ( X = fmb_fun_va172965946on_val_1 )
      | ( X = fmb_fun_va172965946on_val_2 ) ) ).

tff(distinct_domain_fun_va172965946on_val,axiom,
    fmb_fun_va172965946on_val_1 != fmb_fun_va172965946on_val_2 ).

tff(declare_fun_fu1693644106l_bool,type,
    fun_fu1693644106l_bool: $tType ).

tff(declare_fun_fu1693644106l_bool1,type,
    fmb_fun_fu1693644106l_bool_1: fun_fu1693644106l_bool ).

tff(declare_fun_fu1693644106l_bool2,type,
    fmb_fun_fu1693644106l_bool_2: fun_fu1693644106l_bool ).

tff(finite_domain_fun_fu1693644106l_bool,axiom,
    ! [X: fun_fu1693644106l_bool] :
      ( ( X = fmb_fun_fu1693644106l_bool_1 )
      | ( X = fmb_fun_fu1693644106l_bool_2 ) ) ).

tff(distinct_domain_fun_fu1693644106l_bool,axiom,
    fmb_fun_fu1693644106l_bool_1 != fmb_fun_fu1693644106l_bool_2 ).

tff(declare_fun_fu100249073l_bool,type,
    fun_fu100249073l_bool: $tType ).

tff(declare_fun_fu100249073l_bool1,type,
    fmb_fun_fu100249073l_bool_1: fun_fu100249073l_bool ).

tff(declare_fun_fu100249073l_bool2,type,
    fmb_fun_fu100249073l_bool_2: fun_fu100249073l_bool ).

tff(finite_domain_fun_fu100249073l_bool,axiom,
    ! [X: fun_fu100249073l_bool] :
      ( ( X = fmb_fun_fu100249073l_bool_1 )
      | ( X = fmb_fun_fu100249073l_bool_2 ) ) ).

tff(distinct_domain_fun_fu100249073l_bool,axiom,
    fmb_fun_fu100249073l_bool_1 != fmb_fun_fu100249073l_bool_2 ).

tff(declare_fun_fu177229913l_bool,type,
    fun_fu177229913l_bool: $tType ).

tff(declare_fun_fu177229913l_bool1,type,
    fmb_fun_fu177229913l_bool_1: fun_fu177229913l_bool ).

tff(declare_fun_fu177229913l_bool2,type,
    fmb_fun_fu177229913l_bool_2: fun_fu177229913l_bool ).

tff(finite_domain_fun_fu177229913l_bool,axiom,
    ! [X: fun_fu177229913l_bool] :
      ( ( X = fmb_fun_fu177229913l_bool_1 )
      | ( X = fmb_fun_fu177229913l_bool_2 ) ) ).

tff(distinct_domain_fun_fu177229913l_bool,axiom,
    fmb_fun_fu177229913l_bool_1 != fmb_fun_fu177229913l_bool_2 ).

tff(declare_fun_Pr680585871l_bool,type,
    fun_Pr680585871l_bool: $tType ).

tff(declare_fun_Pr680585871l_bool1,type,
    fmb_fun_Pr680585871l_bool_1: fun_Pr680585871l_bool ).

tff(declare_fun_Pr680585871l_bool2,type,
    fmb_fun_Pr680585871l_bool_2: fun_Pr680585871l_bool ).

tff(finite_domain_fun_Pr680585871l_bool,axiom,
    ! [X: fun_Pr680585871l_bool] :
      ( ( X = fmb_fun_Pr680585871l_bool_1 )
      | ( X = fmb_fun_Pr680585871l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr680585871l_bool,axiom,
    fmb_fun_Pr680585871l_bool_1 != fmb_fun_Pr680585871l_bool_2 ).

tff(declare_fun_Pr633696065l_bool,type,
    fun_Pr633696065l_bool: $tType ).

tff(declare_fun_Pr633696065l_bool1,type,
    fmb_fun_Pr633696065l_bool_1: fun_Pr633696065l_bool ).

tff(declare_fun_Pr633696065l_bool2,type,
    fmb_fun_Pr633696065l_bool_2: fun_Pr633696065l_bool ).

tff(finite_domain_fun_Pr633696065l_bool,axiom,
    ! [X: fun_Pr633696065l_bool] :
      ( ( X = fmb_fun_Pr633696065l_bool_1 )
      | ( X = fmb_fun_Pr633696065l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr633696065l_bool,axiom,
    fmb_fun_Pr633696065l_bool_1 != fmb_fun_Pr633696065l_bool_2 ).

tff(declare_fun_Pr227936640r_bool,type,
    fun_Pr227936640r_bool: $tType ).

tff(declare_fun_Pr227936640r_bool1,type,
    fmb_fun_Pr227936640r_bool_1: fun_Pr227936640r_bool ).

tff(declare_fun_Pr227936640r_bool2,type,
    fmb_fun_Pr227936640r_bool_2: fun_Pr227936640r_bool ).

tff(finite_domain_fun_Pr227936640r_bool,axiom,
    ! [X: fun_Pr227936640r_bool] :
      ( ( X = fmb_fun_Pr227936640r_bool_1 )
      | ( X = fmb_fun_Pr227936640r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr227936640r_bool,axiom,
    fmb_fun_Pr227936640r_bool_1 != fmb_fun_Pr227936640r_bool_2 ).

tff(declare_fun_Pr806764899on_val,type,
    fun_Pr806764899on_val: $tType ).

tff(declare_fun_Pr806764899on_val1,type,
    fmb_fun_Pr806764899on_val_1: fun_Pr806764899on_val ).

tff(declare_fun_Pr806764899on_val2,type,
    fmb_fun_Pr806764899on_val_2: fun_Pr806764899on_val ).

tff(finite_domain_fun_Pr806764899on_val,axiom,
    ! [X: fun_Pr806764899on_val] :
      ( ( X = fmb_fun_Pr806764899on_val_1 )
      | ( X = fmb_fun_Pr806764899on_val_2 ) ) ).

tff(distinct_domain_fun_Pr806764899on_val,axiom,
    fmb_fun_Pr806764899on_val_1 != fmb_fun_Pr806764899on_val_2 ).

tff(declare_fun_Pr315804320l_bool,type,
    fun_Pr315804320l_bool: $tType ).

tff(declare_fun_Pr315804320l_bool1,type,
    fmb_fun_Pr315804320l_bool_1: fun_Pr315804320l_bool ).

tff(declare_fun_Pr315804320l_bool2,type,
    fmb_fun_Pr315804320l_bool_2: fun_Pr315804320l_bool ).

tff(finite_domain_fun_Pr315804320l_bool,axiom,
    ! [X: fun_Pr315804320l_bool] :
      ( ( X = fmb_fun_Pr315804320l_bool_1 )
      | ( X = fmb_fun_Pr315804320l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr315804320l_bool,axiom,
    fmb_fun_Pr315804320l_bool_1 != fmb_fun_Pr315804320l_bool_2 ).

tff(declare_fun_Pr357631842on_val,type,
    fun_Pr357631842on_val: $tType ).

tff(declare_fun_Pr357631842on_val1,type,
    fmb_fun_Pr357631842on_val_1: fun_Pr357631842on_val ).

tff(declare_fun_Pr357631842on_val2,type,
    fmb_fun_Pr357631842on_val_2: fun_Pr357631842on_val ).

tff(finite_domain_fun_Pr357631842on_val,axiom,
    ! [X: fun_Pr357631842on_val] :
      ( ( X = fmb_fun_Pr357631842on_val_1 )
      | ( X = fmb_fun_Pr357631842on_val_2 ) ) ).

tff(distinct_domain_fun_Pr357631842on_val,axiom,
    fmb_fun_Pr357631842on_val_1 != fmb_fun_Pr357631842on_val_2 ).

tff(declare_fun_Pr46158268r_bool,type,
    fun_Pr46158268r_bool: $tType ).

tff(declare_fun_Pr46158268r_bool1,type,
    fmb_fun_Pr46158268r_bool_1: fun_Pr46158268r_bool ).

tff(declare_fun_Pr46158268r_bool2,type,
    fmb_fun_Pr46158268r_bool_2: fun_Pr46158268r_bool ).

tff(finite_domain_fun_Pr46158268r_bool,axiom,
    ! [X: fun_Pr46158268r_bool] :
      ( ( X = fmb_fun_Pr46158268r_bool_1 )
      | ( X = fmb_fun_Pr46158268r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr46158268r_bool,axiom,
    fmb_fun_Pr46158268r_bool_1 != fmb_fun_Pr46158268r_bool_2 ).

tff(declare_fun_Pr827765831r_bool,type,
    fun_Pr827765831r_bool: $tType ).

tff(declare_fun_Pr827765831r_bool1,type,
    fmb_fun_Pr827765831r_bool_1: fun_Pr827765831r_bool ).

tff(declare_fun_Pr827765831r_bool2,type,
    fmb_fun_Pr827765831r_bool_2: fun_Pr827765831r_bool ).

tff(finite_domain_fun_Pr827765831r_bool,axiom,
    ! [X: fun_Pr827765831r_bool] :
      ( ( X = fmb_fun_Pr827765831r_bool_1 )
      | ( X = fmb_fun_Pr827765831r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr827765831r_bool,axiom,
    fmb_fun_Pr827765831r_bool_1 != fmb_fun_Pr827765831r_bool_2 ).

tff(declare_fun_Pr1696029455l_bool,type,
    fun_Pr1696029455l_bool: $tType ).

tff(declare_fun_Pr1696029455l_bool1,type,
    fmb_fun_Pr1696029455l_bool_1: fun_Pr1696029455l_bool ).

tff(declare_fun_Pr1696029455l_bool2,type,
    fmb_fun_Pr1696029455l_bool_2: fun_Pr1696029455l_bool ).

tff(finite_domain_fun_Pr1696029455l_bool,axiom,
    ! [X: fun_Pr1696029455l_bool] :
      ( ( X = fmb_fun_Pr1696029455l_bool_1 )
      | ( X = fmb_fun_Pr1696029455l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr1696029455l_bool,axiom,
    fmb_fun_Pr1696029455l_bool_1 != fmb_fun_Pr1696029455l_bool_2 ).

tff(declare_fun_Pr691271849l_bool,type,
    fun_Pr691271849l_bool: $tType ).

tff(declare_fun_Pr691271849l_bool1,type,
    fmb_fun_Pr691271849l_bool_1: fun_Pr691271849l_bool ).

tff(declare_fun_Pr691271849l_bool2,type,
    fmb_fun_Pr691271849l_bool_2: fun_Pr691271849l_bool ).

tff(finite_domain_fun_Pr691271849l_bool,axiom,
    ! [X: fun_Pr691271849l_bool] :
      ( ( X = fmb_fun_Pr691271849l_bool_1 )
      | ( X = fmb_fun_Pr691271849l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr691271849l_bool,axiom,
    fmb_fun_Pr691271849l_bool_1 != fmb_fun_Pr691271849l_bool_2 ).

tff(declare_fun_Pr12181427on_val,type,
    fun_Pr12181427on_val: $tType ).

tff(declare_fun_Pr12181427on_val1,type,
    fmb_fun_Pr12181427on_val_1: fun_Pr12181427on_val ).

tff(declare_fun_Pr12181427on_val2,type,
    fmb_fun_Pr12181427on_val_2: fun_Pr12181427on_val ).

tff(finite_domain_fun_Pr12181427on_val,axiom,
    ! [X: fun_Pr12181427on_val] :
      ( ( X = fmb_fun_Pr12181427on_val_1 )
      | ( X = fmb_fun_Pr12181427on_val_2 ) ) ).

tff(distinct_domain_fun_Pr12181427on_val,axiom,
    fmb_fun_Pr12181427on_val_1 != fmb_fun_Pr12181427on_val_2 ).

tff(declare_fun_Pr1895638121r_bool,type,
    fun_Pr1895638121r_bool: $tType ).

tff(declare_fun_Pr1895638121r_bool1,type,
    fmb_fun_Pr1895638121r_bool_1: fun_Pr1895638121r_bool ).

tff(declare_fun_Pr1895638121r_bool2,type,
    fmb_fun_Pr1895638121r_bool_2: fun_Pr1895638121r_bool ).

tff(finite_domain_fun_Pr1895638121r_bool,axiom,
    ! [X: fun_Pr1895638121r_bool] :
      ( ( X = fmb_fun_Pr1895638121r_bool_1 )
      | ( X = fmb_fun_Pr1895638121r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr1895638121r_bool,axiom,
    fmb_fun_Pr1895638121r_bool_1 != fmb_fun_Pr1895638121r_bool_2 ).

tff(declare_fun_Pr235369833l_bool,type,
    fun_Pr235369833l_bool: $tType ).

tff(declare_fun_Pr235369833l_bool1,type,
    fmb_fun_Pr235369833l_bool_1: fun_Pr235369833l_bool ).

tff(declare_fun_Pr235369833l_bool2,type,
    fmb_fun_Pr235369833l_bool_2: fun_Pr235369833l_bool ).

tff(finite_domain_fun_Pr235369833l_bool,axiom,
    ! [X: fun_Pr235369833l_bool] :
      ( ( X = fmb_fun_Pr235369833l_bool_1 )
      | ( X = fmb_fun_Pr235369833l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr235369833l_bool,axiom,
    fmb_fun_Pr235369833l_bool_1 != fmb_fun_Pr235369833l_bool_2 ).

tff(declare_fun_Pr1728267013r_bool,type,
    fun_Pr1728267013r_bool: $tType ).

tff(declare_fun_Pr1728267013r_bool1,type,
    fmb_fun_Pr1728267013r_bool_1: fun_Pr1728267013r_bool ).

tff(declare_fun_Pr1728267013r_bool2,type,
    fmb_fun_Pr1728267013r_bool_2: fun_Pr1728267013r_bool ).

tff(finite_domain_fun_Pr1728267013r_bool,axiom,
    ! [X: fun_Pr1728267013r_bool] :
      ( ( X = fmb_fun_Pr1728267013r_bool_1 )
      | ( X = fmb_fun_Pr1728267013r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr1728267013r_bool,axiom,
    fmb_fun_Pr1728267013r_bool_1 != fmb_fun_Pr1728267013r_bool_2 ).

tff(declare_fun_Pr1890037787r_bool,type,
    fun_Pr1890037787r_bool: $tType ).

tff(declare_fun_Pr1890037787r_bool1,type,
    fmb_fun_Pr1890037787r_bool_1: fun_Pr1890037787r_bool ).

tff(declare_fun_Pr1890037787r_bool2,type,
    fmb_fun_Pr1890037787r_bool_2: fun_Pr1890037787r_bool ).

tff(finite_domain_fun_Pr1890037787r_bool,axiom,
    ! [X: fun_Pr1890037787r_bool] :
      ( ( X = fmb_fun_Pr1890037787r_bool_1 )
      | ( X = fmb_fun_Pr1890037787r_bool_2 ) ) ).

tff(distinct_domain_fun_Pr1890037787r_bool,axiom,
    fmb_fun_Pr1890037787r_bool_1 != fmb_fun_Pr1890037787r_bool_2 ).

tff(declare_fun_Pr693020585l_bool,type,
    fun_Pr693020585l_bool: $tType ).

tff(declare_fun_Pr693020585l_bool1,type,
    fmb_fun_Pr693020585l_bool_1: fun_Pr693020585l_bool ).

tff(declare_fun_Pr693020585l_bool2,type,
    fmb_fun_Pr693020585l_bool_2: fun_Pr693020585l_bool ).

tff(finite_domain_fun_Pr693020585l_bool,axiom,
    ! [X: fun_Pr693020585l_bool] :
      ( ( X = fmb_fun_Pr693020585l_bool_1 )
      | ( X = fmb_fun_Pr693020585l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr693020585l_bool,axiom,
    fmb_fun_Pr693020585l_bool_1 != fmb_fun_Pr693020585l_bool_2 ).

tff(declare_fun_Pr903661919l_bool,type,
    fun_Pr903661919l_bool: $tType ).

tff(declare_fun_Pr903661919l_bool1,type,
    fmb_fun_Pr903661919l_bool_1: fun_Pr903661919l_bool ).

tff(declare_fun_Pr903661919l_bool2,type,
    fmb_fun_Pr903661919l_bool_2: fun_Pr903661919l_bool ).

tff(finite_domain_fun_Pr903661919l_bool,axiom,
    ! [X: fun_Pr903661919l_bool] :
      ( ( X = fmb_fun_Pr903661919l_bool_1 )
      | ( X = fmb_fun_Pr903661919l_bool_2 ) ) ).

tff(distinct_domain_fun_Pr903661919l_bool,axiom,
    fmb_fun_Pr903661919l_bool_1 != fmb_fun_Pr903661919l_bool_2 ).

tff(declare_produc124828825on_val,type,
    produc124828825on_val: $tType ).

tff(declare_produc124828825on_val1,type,
    fmb_produc124828825on_val_1: produc124828825on_val ).

tff(finite_domain_produc124828825on_val,axiom,
    ! [X: produc124828825on_val] : ( X = fmb_produc124828825on_val_1 ) ).

tff(declare_produc1285161482t_char,type,
    produc1285161482t_char: $tType ).

tff(declare_produc1285161482t_char1,type,
    fmb_produc1285161482t_char_1: produc1285161482t_char ).

tff(declare_produc1285161482t_char2,type,
    fmb_produc1285161482t_char_2: produc1285161482t_char ).

tff(finite_domain_produc1285161482t_char,axiom,
    ! [X: produc1285161482t_char] :
      ( ( X = fmb_produc1285161482t_char_1 )
      | ( X = fmb_produc1285161482t_char_2 ) ) ).

tff(distinct_domain_produc1285161482t_char,axiom,
    fmb_produc1285161482t_char_1 != fmb_produc1285161482t_char_2 ).

tff(declare_produc639455274on_val,type,
    produc639455274on_val: $tType ).

tff(declare_produc639455274on_val1,type,
    fmb_produc639455274on_val_1: produc639455274on_val ).

tff(declare_produc639455274on_val2,type,
    fmb_produc639455274on_val_2: produc639455274on_val ).

tff(finite_domain_produc639455274on_val,axiom,
    ! [X: produc639455274on_val] :
      ( ( X = fmb_produc639455274on_val_1 )
      | ( X = fmb_produc639455274on_val_2 ) ) ).

tff(distinct_domain_produc639455274on_val,axiom,
    fmb_produc639455274on_val_1 != fmb_produc639455274on_val_2 ).

tff(declare_produc220283002t_char,type,
    produc220283002t_char: $tType ).

tff(declare_produc220283002t_char1,type,
    fmb_produc220283002t_char_1: produc220283002t_char ).

tff(declare_produc220283002t_char2,type,
    fmb_produc220283002t_char_2: produc220283002t_char ).

tff(finite_domain_produc220283002t_char,axiom,
    ! [X: produc220283002t_char] :
      ( ( X = fmb_produc220283002t_char_1 )
      | ( X = fmb_produc220283002t_char_2 ) ) ).

tff(distinct_domain_produc220283002t_char,axiom,
    fmb_produc220283002t_char_1 != fmb_produc220283002t_char_2 ).

tff(declare_produc662261637t_char,type,
    produc662261637t_char: $tType ).

tff(declare_produc662261637t_char1,type,
    fmb_produc662261637t_char_1: produc662261637t_char ).

tff(finite_domain_produc662261637t_char,axiom,
    ! [X: produc662261637t_char] : ( X = fmb_produc662261637t_char_1 ) ).

tff(declare_produc12694297on_val,type,
    produc12694297on_val: $tType ).

tff(declare_produc12694297on_val1,type,
    fmb_produc12694297on_val_1: produc12694297on_val ).

tff(finite_domain_produc12694297on_val,axiom,
    ! [X: produc12694297on_val] : ( X = fmb_produc12694297on_val_1 ) ).

tff(declare_produc1102272487on_val,type,
    produc1102272487on_val: $tType ).

tff(declare_produc1102272487on_val1,type,
    fmb_produc1102272487on_val_1: produc1102272487on_val ).

tff(finite_domain_produc1102272487on_val,axiom,
    ! [X: produc1102272487on_val] : ( X = fmb_produc1102272487on_val_1 ) ).

tff(declare_produc349695911t_char,type,
    produc349695911t_char: $tType ).

tff(declare_produc349695911t_char1,type,
    fmb_produc349695911t_char_1: produc349695911t_char ).

tff(declare_produc349695911t_char2,type,
    fmb_produc349695911t_char_2: produc349695911t_char ).

tff(finite_domain_produc349695911t_char,axiom,
    ! [X: produc349695911t_char] :
      ( ( X = fmb_produc349695911t_char_1 )
      | ( X = fmb_produc349695911t_char_2 ) ) ).

tff(distinct_domain_produc349695911t_char,axiom,
    fmb_produc349695911t_char_1 != fmb_produc349695911t_char_2 ).

tff(declare_produc87279271on_val,type,
    produc87279271on_val: $tType ).

tff(declare_produc87279271on_val1,type,
    fmb_produc87279271on_val_1: produc87279271on_val ).

tff(declare_produc87279271on_val2,type,
    fmb_produc87279271on_val_2: produc87279271on_val ).

tff(finite_domain_produc87279271on_val,axiom,
    ! [X: produc87279271on_val] :
      ( ( X = fmb_produc87279271on_val_1 )
      | ( X = fmb_produc87279271on_val_2 ) ) ).

tff(distinct_domain_produc87279271on_val,axiom,
    fmb_produc87279271on_val_1 != fmb_produc87279271on_val_2 ).

tff(declare_produc1406897475t_char,type,
    produc1406897475t_char: $tType ).

tff(declare_produc1406897475t_char1,type,
    fmb_produc1406897475t_char_1: produc1406897475t_char ).

tff(declare_produc1406897475t_char2,type,
    fmb_produc1406897475t_char_2: produc1406897475t_char ).

tff(finite_domain_produc1406897475t_char,axiom,
    ! [X: produc1406897475t_char] :
      ( ( X = fmb_produc1406897475t_char_1 )
      | ( X = fmb_produc1406897475t_char_2 ) ) ).

tff(distinct_domain_produc1406897475t_char,axiom,
    fmb_produc1406897475t_char_1 != fmb_produc1406897475t_char_2 ).

tff(declare_produc1826280281t_char,type,
    produc1826280281t_char: $tType ).

tff(declare_produc1826280281t_char1,type,
    fmb_produc1826280281t_char_1: produc1826280281t_char ).

tff(declare_produc1826280281t_char2,type,
    fmb_produc1826280281t_char_2: produc1826280281t_char ).

tff(finite_domain_produc1826280281t_char,axiom,
    ! [X: produc1826280281t_char] :
      ( ( X = fmb_produc1826280281t_char_1 )
      | ( X = fmb_produc1826280281t_char_2 ) ) ).

tff(distinct_domain_produc1826280281t_char,axiom,
    fmb_produc1826280281t_char_1 != fmb_produc1826280281t_char_2 ).

tff(declare_produc409205479on_val,type,
    produc409205479on_val: $tType ).

tff(declare_produc409205479on_val1,type,
    fmb_produc409205479on_val_1: produc409205479on_val ).

tff(declare_produc409205479on_val2,type,
    fmb_produc409205479on_val_2: produc409205479on_val ).

tff(finite_domain_produc409205479on_val,axiom,
    ! [X: produc409205479on_val] :
      ( ( X = fmb_produc409205479on_val_1 )
      | ( X = fmb_produc409205479on_val_2 ) ) ).

tff(distinct_domain_produc409205479on_val,axiom,
    fmb_produc409205479on_val_1 != fmb_produc409205479on_val_2 ).

tff(declare_produc231486621on_val,type,
    produc231486621on_val: $tType ).

tff(declare_produc231486621on_val1,type,
    fmb_produc231486621on_val_1: produc231486621on_val ).

tff(declare_produc231486621on_val2,type,
    fmb_produc231486621on_val_2: produc231486621on_val ).

tff(finite_domain_produc231486621on_val,axiom,
    ! [X: produc231486621on_val] :
      ( ( X = fmb_produc231486621on_val_1 )
      | ( X = fmb_produc231486621on_val_2 ) ) ).

tff(distinct_domain_produc231486621on_val,axiom,
    fmb_produc231486621on_val_1 != fmb_produc231486621on_val_2 ).

tff(declare_val_list_char,type,
    val_list_char: fun_va223928858t_char ).

tff(val_list_char_definition,axiom,
    val_list_char = fmb_fun_va223928858t_char_1 ).

tff(declare_some_ty,type,
    some_ty: fun_ty_option_ty ).

tff(some_ty_definition,axiom,
    some_ty = fmb_fun_ty_option_ty_1 ).

tff(declare_some_val,type,
    some_val: fun_val_option_val ).

tff(some_val_definition,axiom,
    some_val = fmb_fun_val_option_val_1 ).

tff(declare_some_P948696889on_val,type,
    some_P948696889on_val: fun_Pr357631842on_val ).

tff(some_P948696889on_val_definition,axiom,
    some_P948696889on_val = fmb_fun_Pr357631842on_val_1 ).

tff(declare_the_ty,type,
    the_ty: fun_option_ty_ty ).

tff(the_ty_definition,axiom,
    the_ty = fmb_fun_option_ty_ty_1 ).

tff(declare_the_val,type,
    the_val: fun_option_val_val ).

tff(the_val_definition,axiom,
    the_val = fmb_fun_option_val_val_1 ).

tff(declare_the_Pr431167171on_val,type,
    the_Pr431167171on_val: fun_op498348476on_val ).

tff(the_Pr431167171on_val_definition,axiom,
    the_Pr431167171on_val = fmb_fun_op498348476on_val_1 ).

tff(declare_fequal_ty,type,
    fequal_ty: fun_ty_fun_ty_bool ).

tff(fequal_ty_definition,axiom,
    fequal_ty = fmb_fun_ty_fun_ty_bool_1 ).

tff(declare_e_1,type,
    e_1: fun_li688206603ion_ty ).

tff(e_1_definition,axiom,
    e_1 = fmb_fun_li688206603ion_ty_1 ).

tff(declare_p,type,
    p: list_P1999446415t_char ).

tff(p_definition,axiom,
    p = fmb_list_P1999446415t_char_1 ).

tff(declare_t,type,
    t: ty ).

tff(t_definition,axiom,
    t = fmb_ty_1 ).

tff(declare_ts,type,
    ts: list_ty ).

tff(ts_definition,axiom,
    ts = fmb_list_ty_1 ).

tff(declare_vs_1,type,
    vs_1: list_list_char ).

tff(vs_1_definition,axiom,
    vs_1 = fmb_list_list_char_1 ).

tff(declare_e,type,
    e: exp_list_char ).

tff(e_definition,axiom,
    e = fmb_exp_list_char_1 ).

tff(declare_h,type,
    h: fun_na939144002on_val ).

tff(h_definition,axiom,
    h = fmb_fun_na939144002on_val_1 ).

tff(declare_vs,type,
    vs: list_val ).

tff(vs_definition,axiom,
    vs = fmb_list_val_1 ).

tff(declare_eval,type,
    eval: ( list_P1999446415t_char * exp_list_char * produc12694297on_val ) > fun_ex1201926843l_bool ).

tff(function_eval,axiom,
    ( ( eval(fmb_list_P1999446415t_char_1,fmb_exp_list_char_1,fmb_produc12694297on_val_1) = fmb_fun_ex1201926843l_bool_2 )
    & ( eval(fmb_list_P1999446415t_char_2,fmb_exp_list_char_1,fmb_produc12694297on_val_1) = fmb_fun_ex1201926843l_bool_2 ) ) ).

tff(declare_final_list_char,type,
    final_list_char: exp_list_char > bool ).

tff(function_final_list_char,axiom,
    final_list_char(fmb_exp_list_char_1) = fmb_bool_2 ).

tff(declare_conf_P373316194t_char,type,
    conf_P373316194t_char: ( list_P1999446415t_char * fun_na939144002on_val ) > fun_val_fun_ty_bool ).

tff(function_conf_P373316194t_char,axiom,
    ( ( conf_P373316194t_char(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1) = fmb_fun_val_fun_ty_bool_2 )
    & ( conf_P373316194t_char(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1) = fmb_fun_val_fun_ty_bool_2 ) ) ).

tff(declare_hconf_97414254t_char,type,
    hconf_97414254t_char: ( list_P1999446415t_char * fun_na939144002on_val ) > bool ).

tff(function_hconf_97414254t_char,axiom,
    ( ( hconf_97414254t_char(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1) = fmb_bool_2 )
    & ( hconf_97414254t_char(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1) = fmb_bool_2 ) ) ).

tff(declare_lconf_496643946t_char,type,
    lconf_496643946t_char: ( list_P1999446415t_char * fun_na939144002on_val * fun_li1432931796on_val * fun_li688206603ion_ty ) > bool ).

tff(function_lconf_496643946t_char,axiom,
    ( ( lconf_496643946t_char(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_li688206603ion_ty_1) = fmb_bool_2 )
    & ( lconf_496643946t_char(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_li688206603ion_ty_2) = fmb_bool_2 )
    & ( lconf_496643946t_char(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_li688206603ion_ty_1) = fmb_bool_2 )
    & ( lconf_496643946t_char(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_li688206603ion_ty_2) = fmb_bool_2 ) ) ).

tff(declare_tryCatch_list_char,type,
    tryCatch_list_char: ( exp_list_char * list_char * list_char ) > fun_ex1654222579t_char ).

tff(function_tryCatch_list_char,axiom,
    tryCatch_list_char(fmb_exp_list_char_1,fmb_list_char_1,fmb_list_char_1) = fmb_fun_ex1654222579t_char_2 ).

tff(declare_comp_l1825390573t_char,type,
    comp_l1825390573t_char: ( fun_li1459524056st_val * fun_li1580442732on_val ) > fun_li742655849st_val ).

tff(function_comp_l1825390573t_char,axiom,
    ( ( comp_l1825390573t_char(fmb_fun_li1459524056st_val_1,fmb_fun_li1580442732on_val_1) = fmb_fun_li742655849st_val_2 )
    & ( comp_l1825390573t_char(fmb_fun_li1459524056st_val_1,fmb_fun_li1580442732on_val_2) = fmb_fun_li742655849st_val_2 )
    & ( comp_l1825390573t_char(fmb_fun_li1459524056st_val_2,fmb_fun_li1580442732on_val_1) = fmb_fun_li742655849st_val_2 )
    & ( comp_l1825390573t_char(fmb_fun_li1459524056st_val_2,fmb_fun_li1580442732on_val_2) = fmb_fun_li742655849st_val_2 ) ) ).

tff(declare_comp_o1129292306t_char,type,
    comp_o1129292306t_char: ( fun_option_val_val * fun_li1432931796on_val ) > fun_list_char_val ).

tff(function_comp_o1129292306t_char,axiom,
    ( ( comp_o1129292306t_char(fmb_fun_option_val_val_1,fmb_fun_li1432931796on_val_1) = fmb_fun_list_char_val_2 )
    & ( comp_o1129292306t_char(fmb_fun_option_val_val_2,fmb_fun_li1432931796on_val_1) = fmb_fun_list_char_val_2 ) ) ).

tff(declare_overri2012515291on_val,type,
    overri2012515291on_val: ( fun_li1432931796on_val * fun_li1432931796on_val * fun_list_char_bool ) > fun_li1432931796on_val ).

tff(function_overri2012515291on_val,axiom,
    ( ( overri2012515291on_val(fmb_fun_li1432931796on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_list_char_bool_1) = fmb_fun_li1432931796on_val_1 )
    & ( overri2012515291on_val(fmb_fun_li1432931796on_val_1,fmb_fun_li1432931796on_val_1,fmb_fun_list_char_bool_2) = fmb_fun_li1432931796on_val_1 ) ) ).

tff(declare_distinct_list_char,type,
    distinct_list_char: list_list_char > bool ).

tff(function_distinct_list_char,axiom,
    distinct_list_char(fmb_list_list_char_1) = fmb_bool_2 ).

tff(declare_list_a52822260ion_ty,type,
    list_a52822260ion_ty: ( fun_ex1708156690y_bool * list_exp_list_char * list_option_ty ) > bool ).

tff(function_list_a52822260ion_ty,axiom,
    ( ( list_a52822260ion_ty(fmb_fun_ex1708156690y_bool_1,fmb_list_exp_list_char_1,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a52822260ion_ty(fmb_fun_ex1708156690y_bool_2,fmb_list_exp_list_char_1,fmb_list_option_ty_1) = fmb_bool_2 ) ) ).

tff(declare_list_a1834344429ion_ty,type,
    list_a1834344429ion_ty: ( fun_li1351943641y_bool * list_list_char * list_option_ty ) > bool ).

tff(function_list_a1834344429ion_ty,axiom,
    ( ( list_a1834344429ion_ty(fmb_fun_li1351943641y_bool_1,fmb_list_list_char_1,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a1834344429ion_ty(fmb_fun_li1351943641y_bool_2,fmb_list_list_char_1,fmb_list_option_ty_1) = fmb_bool_2 ) ) ).

tff(declare_list_a283687028t_char,type,
    list_a283687028t_char: ( fun_op14579988r_bool * list_option_ty * list_exp_list_char ) > bool ).

tff(function_list_a283687028t_char,axiom,
    ( ( list_a283687028t_char(fmb_fun_op14579988r_bool_1,fmb_list_option_ty_1,fmb_list_exp_list_char_1) = fmb_bool_2 )
    & ( list_a283687028t_char(fmb_fun_op14579988r_bool_2,fmb_list_option_ty_1,fmb_list_exp_list_char_1) = fmb_bool_2 ) ) ).

tff(declare_list_a839443437t_char,type,
    list_a839443437t_char: ( fun_op668690445r_bool * list_option_ty * list_list_char ) > bool ).

tff(function_list_a839443437t_char,axiom,
    ( ( list_a839443437t_char(fmb_fun_op668690445r_bool_1,fmb_list_option_ty_1,fmb_list_list_char_1) = fmb_bool_2 )
    & ( list_a839443437t_char(fmb_fun_op668690445r_bool_2,fmb_list_option_ty_1,fmb_list_list_char_1) = fmb_bool_2 ) ) ).

tff(declare_list_a2039389316_ty_ty,type,
    list_a2039389316_ty_ty: ( fun_op174240306y_bool * list_option_ty * list_ty ) > bool ).

tff(function_list_a2039389316_ty_ty,axiom,
    ( ( list_a2039389316_ty_ty(fmb_fun_op174240306y_bool_1,fmb_list_option_ty_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_a2039389316_ty_ty(fmb_fun_op174240306y_bool_1,fmb_list_option_ty_1,fmb_list_ty_2) = fmb_bool_2 )
    & ( list_a2039389316_ty_ty(fmb_fun_op174240306y_bool_2,fmb_list_option_ty_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_a2039389316_ty_ty(fmb_fun_op174240306y_bool_2,fmb_list_option_ty_1,fmb_list_ty_2) = fmb_bool_2 ) ) ).

tff(declare_list_a1073113293ty_val,type,
    list_a1073113293ty_val: ( fun_op1696804347l_bool * list_option_ty * list_val ) > bool ).

tff(function_list_a1073113293ty_val,axiom,
    ( ( list_a1073113293ty_val(fmb_fun_op1696804347l_bool_1,fmb_list_option_ty_1,fmb_list_val_1) = fmb_bool_2 )
    & ( list_a1073113293ty_val(fmb_fun_op1696804347l_bool_2,fmb_list_option_ty_1,fmb_list_val_1) = fmb_bool_2 ) ) ).

tff(declare_list_a1880637950ion_ty,type,
    list_a1880637950ion_ty: ( fun_ty1580608948y_bool * list_ty * list_option_ty ) > bool ).

tff(function_list_a1880637950ion_ty,axiom,
    ( ( list_a1880637950ion_ty(fmb_fun_ty1580608948y_bool_1,fmb_list_ty_1,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a1880637950ion_ty(fmb_fun_ty1580608948y_bool_1,fmb_list_ty_2,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a1880637950ion_ty(fmb_fun_ty1580608948y_bool_2,fmb_list_ty_1,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a1880637950ion_ty(fmb_fun_ty1580608948y_bool_2,fmb_list_ty_2,fmb_list_option_ty_1) = fmb_bool_2 ) ) ).

tff(declare_list_all2_ty_ty,type,
    list_all2_ty_ty: ( fun_ty_fun_ty_bool * list_ty * list_ty ) > bool ).

tff(function_list_all2_ty_ty,axiom,
    ( ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_1,fmb_list_ty_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_1,fmb_list_ty_1,fmb_list_ty_2) = fmb_bool_1 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_1,fmb_list_ty_2,fmb_list_ty_1) = fmb_bool_1 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_1,fmb_list_ty_2,fmb_list_ty_2) = fmb_bool_2 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_2,fmb_list_ty_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_2,fmb_list_ty_1,fmb_list_ty_2) = fmb_bool_1 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_2,fmb_list_ty_2,fmb_list_ty_1) = fmb_bool_1 )
    & ( list_all2_ty_ty(fmb_fun_ty_fun_ty_bool_2,fmb_list_ty_2,fmb_list_ty_2) = fmb_bool_2 ) ) ).

tff(declare_list_a1462908359ion_ty,type,
    list_a1462908359ion_ty: ( fun_va642468779y_bool * list_val * list_option_ty ) > bool ).

tff(function_list_a1462908359ion_ty,axiom,
    ( ( list_a1462908359ion_ty(fmb_fun_va642468779y_bool_1,fmb_list_val_1,fmb_list_option_ty_1) = fmb_bool_2 )
    & ( list_a1462908359ion_ty(fmb_fun_va642468779y_bool_2,fmb_list_val_1,fmb_list_option_ty_1) = fmb_bool_2 ) ) ).

tff(declare_list_all2_val_ty,type,
    list_all2_val_ty: ( fun_val_fun_ty_bool * list_val * list_ty ) > bool ).

tff(function_list_all2_val_ty,axiom,
    ( ( list_all2_val_ty(fmb_fun_val_fun_ty_bool_1,fmb_list_val_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_all2_val_ty(fmb_fun_val_fun_ty_bool_1,fmb_list_val_1,fmb_list_ty_2) = fmb_bool_2 )
    & ( list_all2_val_ty(fmb_fun_val_fun_ty_bool_2,fmb_list_val_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( list_all2_val_ty(fmb_fun_val_fun_ty_bool_2,fmb_list_val_1,fmb_list_ty_2) = fmb_bool_2 ) ) ).

tff(declare_map_ex101166958t_char,type,
    map_ex101166958t_char: fun_ex1654222579t_char > fun_li1279027773t_char ).

tff(function_map_ex101166958t_char,axiom,
    ( ( map_ex101166958t_char(fmb_fun_ex1654222579t_char_1) = fmb_fun_li1279027773t_char_2 )
    & ( map_ex101166958t_char(fmb_fun_ex1654222579t_char_2) = fmb_fun_li1279027773t_char_2 ) ) ).

tff(declare_map_ex2109939687t_char,type,
    map_ex2109939687t_char: fun_ex1075505132t_char > fun_li218321462t_char ).

tff(function_map_ex2109939687t_char,axiom,
    ( ( map_ex2109939687t_char(fmb_fun_ex1075505132t_char_1) = fmb_fun_li218321462t_char_2 )
    & ( map_ex2109939687t_char(fmb_fun_ex1075505132t_char_2) = fmb_fun_li218321462t_char_2 ) ) ).

tff(declare_map_ex1548475405ion_ty,type,
    map_ex1548475405ion_ty: fun_ex12316946ion_ty > fun_li241576028ion_ty ).

tff(function_map_ex1548475405ion_ty,axiom,
    ( ( map_ex1548475405ion_ty(fmb_fun_ex12316946ion_ty_1) = fmb_fun_li241576028ion_ty_2 )
    & ( map_ex1548475405ion_ty(fmb_fun_ex12316946ion_ty_2) = fmb_fun_li241576028ion_ty_2 ) ) ).

tff(declare_map_ex1598883030on_val,type,
    map_ex1598883030on_val: fun_ex1158871131on_val > fun_li690207653on_val ).

tff(function_map_ex1598883030on_val,axiom,
    ( ( map_ex1598883030on_val(fmb_fun_ex1158871131on_val_1) = fmb_fun_li690207653on_val_2 )
    & ( map_ex1598883030on_val(fmb_fun_ex1158871131on_val_2) = fmb_fun_li690207653on_val_2 ) ) ).

tff(declare_map_exp_list_char_ty,type,
    map_exp_list_char_ty: fun_exp_list_char_ty > fun_li1055333287ist_ty ).

tff(function_map_exp_list_char_ty,axiom,
    ( ( map_exp_list_char_ty(fmb_fun_exp_list_char_ty_1) = fmb_fun_li1055333287ist_ty_2 )
    & ( map_exp_list_char_ty(fmb_fun_exp_list_char_ty_2) = fmb_fun_li1055333287ist_ty_2 ) ) ).

tff(declare_map_ex740158547ar_val,type,
    map_ex740158547ar_val: fun_ex793263652ar_val > fun_li363341936st_val ).

tff(function_map_ex740158547ar_val,axiom,
    ( ( map_ex740158547ar_val(fmb_fun_ex793263652ar_val_1) = fmb_fun_li363341936st_val_2 )
    & ( map_ex740158547ar_val(fmb_fun_ex793263652ar_val_2) = fmb_fun_li363341936st_val_2 ) ) ).

tff(declare_map_ex840371726on_val,type,
    map_ex840371726on_val: fun_ex1732915347on_val > fun_li1581546589on_val ).

tff(function_map_ex840371726on_val,axiom,
    ( ( map_ex840371726on_val(fmb_fun_ex1732915347on_val_1) = fmb_fun_li1581546589on_val_2 )
    & ( map_ex840371726on_val(fmb_fun_ex1732915347on_val_2) = fmb_fun_li1581546589on_val_2 ) ) ).

tff(declare_map_li1249123943t_char,type,
    map_li1249123943t_char: fun_li978641004t_char > fun_li567129860t_char ).

tff(function_map_li1249123943t_char,axiom,
    ( ( map_li1249123943t_char(fmb_fun_li978641004t_char_1) = fmb_fun_li567129860t_char_2 )
    & ( map_li1249123943t_char(fmb_fun_li978641004t_char_2) = fmb_fun_li567129860t_char_2 ) ) ).

tff(declare_map_li1333403488t_char,type,
    map_li1333403488t_char: fun_li1751394789t_char > fun_li1898638973t_char ).

tff(function_map_li1333403488t_char,axiom,
    ( ( map_li1333403488t_char(fmb_fun_li1751394789t_char_1) = fmb_fun_li1898638973t_char_2 )
    & ( map_li1333403488t_char(fmb_fun_li1751394789t_char_2) = fmb_fun_li1898638973t_char_2 ) ) ).

tff(declare_map_li771939206ion_ty,type,
    map_li771939206ion_ty: fun_li688206603ion_ty > fun_li1921893539ion_ty ).

tff(function_map_li771939206ion_ty,axiom,
    ( ( map_li771939206ion_ty(fmb_fun_li688206603ion_ty_1) = fmb_fun_li1921893539ion_ty_2 )
    & ( map_li771939206ion_ty(fmb_fun_li688206603ion_ty_2) = fmb_fun_li1921893539ion_ty_2 ) ) ).

tff(declare_map_li50976719on_val,type,
    map_li50976719on_val: fun_li1432931796on_val > fun_li1580442732on_val ).

tff(function_map_li50976719on_val,axiom,
    map_li50976719on_val(fmb_fun_li1432931796on_val_1) = fmb_fun_li1580442732on_val_2 ).

tff(declare_map_list_char_ty,type,
    map_list_char_ty: fun_list_char_ty > fun_li490940192ist_ty ).

tff(function_map_list_char_ty,axiom,
    ( ( map_list_char_ty(fmb_fun_list_char_ty_1) = fmb_fun_li490940192ist_ty_2 )
    & ( map_list_char_ty(fmb_fun_list_char_ty_2) = fmb_fun_li490940192ist_ty_2 ) ) ).

tff(declare_map_list_char_val,type,
    map_list_char_val: fun_list_char_val > fun_li742655849st_val ).

tff(function_map_list_char_val,axiom,
    ( ( map_list_char_val(fmb_fun_list_char_val_1) = fmb_fun_li742655849st_val_2 )
    & ( map_list_char_val(fmb_fun_list_char_val_2) = fmb_fun_li742655849st_val_2 ) ) ).

tff(declare_map_li1100402823on_val,type,
    map_li1100402823on_val: fun_li2145367436on_val > fun_li1867552164on_val ).

tff(function_map_li1100402823on_val,axiom,
    ( ( map_li1100402823on_val(fmb_fun_li2145367436on_val_1) = fmb_fun_li1867552164on_val_2 )
    & ( map_li1100402823on_val(fmb_fun_li2145367436on_val_2) = fmb_fun_li1867552164on_val_2 ) ) ).

tff(declare_map_op1779340173t_char,type,
    map_op1779340173t_char: fun_op1508857234t_char > fun_li156600670t_char ).

tff(function_map_op1779340173t_char,axiom,
    ( ( map_op1779340173t_char(fmb_fun_op1508857234t_char_1) = fmb_fun_li156600670t_char_2 )
    & ( map_op1779340173t_char(fmb_fun_op1508857234t_char_2) = fmb_fun_li156600670t_char_2 ) ) ).

tff(declare_map_op1924521862t_char,type,
    map_op1924521862t_char: fun_op195029515t_char > fun_li712717783t_char ).

tff(function_map_op1924521862t_char,axiom,
    ( ( map_op1924521862t_char(fmb_fun_op195029515t_char_1) = fmb_fun_li712717783t_char_2 )
    & ( map_op1924521862t_char(fmb_fun_op195029515t_char_2) = fmb_fun_li712717783t_char_2 ) ) ).

tff(declare_map_op1363057580ion_ty,type,
    map_op1363057580ion_ty: fun_op1279324977ion_ty > fun_li735972349ion_ty ).

tff(function_map_op1363057580ion_ty,axiom,
    ( ( map_op1363057580ion_ty(fmb_fun_op1279324977ion_ty_1) = fmb_fun_li735972349ion_ty_2 )
    & ( map_op1363057580ion_ty(fmb_fun_op1279324977ion_ty_2) = fmb_fun_li735972349ion_ty_2 ) ) ).

tff(declare_map_option_ty_ty,type,
    map_option_ty_ty: fun_option_ty_ty > fun_li202512966ist_ty ).

tff(function_map_option_ty_ty,axiom,
    ( ( map_option_ty_ty(fmb_fun_option_ty_ty_1) = fmb_fun_li202512966ist_ty_2 )
    & ( map_option_ty_ty(fmb_fun_option_ty_ty_2) = fmb_fun_li202512966ist_ty_2 ) ) ).

tff(declare_map_option_ty_val,type,
    map_option_ty_val: fun_option_ty_val > fun_li1333774223st_val ).

tff(function_map_option_ty_val,axiom,
    ( ( map_option_ty_val(fmb_fun_option_ty_val_1) = fmb_fun_li1333774223st_val_2 )
    & ( map_option_ty_val(fmb_fun_option_ty_val_2) = fmb_fun_li1333774223st_val_2 ) ) ).

tff(declare_map_option_val_val,type,
    map_option_val_val: fun_option_val_val > fun_li1459524056st_val ).

tff(function_map_option_val_val,axiom,
    ( ( map_option_val_val(fmb_fun_option_val_val_1) = fmb_fun_li1459524056st_val_2 )
    & ( map_option_val_val(fmb_fun_option_val_val_2) = fmb_fun_li1459524056st_val_2 ) ) ).

tff(declare_map_ty_exp_list_char,type,
    map_ty_exp_list_char: fun_ty_exp_list_char > fun_li1975737011t_char ).

tff(function_map_ty_exp_list_char,axiom,
    ( ( map_ty_exp_list_char(fmb_fun_ty_exp_list_char_1) = fmb_fun_li1975737011t_char_2 )
    & ( map_ty_exp_list_char(fmb_fun_ty_exp_list_char_2) = fmb_fun_li1975737011t_char_2 ) ) ).

tff(declare_map_ty_list_char,type,
    map_ty_list_char: fun_ty_list_char > fun_li2094888364t_char ).

tff(function_map_ty_list_char,axiom,
    ( ( map_ty_list_char(fmb_fun_ty_list_char_1) = fmb_fun_li2094888364t_char_2 )
    & ( map_ty_list_char(fmb_fun_ty_list_char_2) = fmb_fun_li2094888364t_char_2 ) ) ).

tff(declare_map_ty_option_ty,type,
    map_ty_option_ty: fun_ty_option_ty > fun_li2118142930ion_ty ).

tff(function_map_ty_option_ty,axiom,
    ( ( map_ty_option_ty(fmb_fun_ty_option_ty_1) = fmb_fun_li2118142930ion_ty_1 )
    & ( map_ty_option_ty(fmb_fun_ty_option_ty_2) = fmb_fun_li2118142930ion_ty_1 ) ) ).

tff(declare_map_ty_option_val,type,
    map_ty_option_val: fun_ty_option_val > fun_li1110934555on_val ).

tff(function_map_ty_option_val,axiom,
    ( ( map_ty_option_val(fmb_fun_ty_option_val_1) = fmb_fun_li1110934555on_val_2 )
    & ( map_ty_option_val(fmb_fun_ty_option_val_2) = fmb_fun_li1110934555on_val_2 ) ) ).

tff(declare_map_ty_ty,type,
    map_ty_ty: fun_ty_ty > fun_list_ty_list_ty ).

tff(function_map_ty_ty,axiom,
    ( ( map_ty_ty(fmb_fun_ty_ty_1) = fmb_fun_list_ty_list_ty_2 )
    & ( map_ty_ty(fmb_fun_ty_ty_2) = fmb_fun_list_ty_list_ty_2 ) ) ).

tff(declare_map_ty_val,type,
    map_ty_val: fun_ty_val > fun_list_ty_list_val ).

tff(function_map_ty_val,axiom,
    ( ( map_ty_val(fmb_fun_ty_val_1) = fmb_fun_list_ty_list_val_2 )
    & ( map_ty_val(fmb_fun_ty_val_2) = fmb_fun_list_ty_list_val_2 ) ) ).

tff(declare_map_ty891785382on_val,type,
    map_ty891785382on_val: fun_ty2028523121on_val > fun_li1883640275on_val ).

tff(function_map_ty891785382on_val,axiom,
    ( ( map_ty891785382on_val(fmb_fun_ty2028523121on_val_1) = fmb_fun_li1883640275on_val_2 )
    & ( map_ty891785382on_val(fmb_fun_ty2028523121on_val_2) = fmb_fun_li1883640275on_val_2 ) ) ).

tff(declare_map_va1934808527t_char,type,
    map_va1934808527t_char: fun_va223928858t_char > fun_li430210730t_char ).

tff(function_map_va1934808527t_char,axiom,
    ( ( map_va1934808527t_char(fmb_fun_va223928858t_char_1) = fmb_fun_li430210730t_char_2 )
    & ( map_va1934808527t_char(fmb_fun_va223928858t_char_2) = fmb_fun_li430210730t_char_2 ) ) ).

tff(declare_map_val_list_char,type,
    map_val_list_char: fun_val_list_char > fun_li1120813347t_char ).

tff(function_map_val_list_char,axiom,
    ( ( map_val_list_char(fmb_fun_val_list_char_1) = fmb_fun_li1120813347t_char_2 )
    & ( map_val_list_char(fmb_fun_val_list_char_2) = fmb_fun_li1120813347t_char_2 ) ) ).

tff(declare_map_val_option_ty,type,
    map_val_option_ty: fun_val_option_ty > fun_li1144067913ion_ty ).

tff(function_map_val_option_ty,axiom,
    ( ( map_val_option_ty(fmb_fun_val_option_ty_1) = fmb_fun_li1144067913ion_ty_1 )
    & ( map_val_option_ty(fmb_fun_val_option_ty_2) = fmb_fun_li1144067913ion_ty_2 ) ) ).

tff(declare_map_val_option_val,type,
    map_val_option_val: fun_val_option_val > fun_li1091306514on_val ).

tff(function_map_val_option_val,axiom,
    ( ( map_val_option_val(fmb_fun_val_option_val_1) = fmb_fun_li1091306514on_val_2 )
    & ( map_val_option_val(fmb_fun_val_option_val_2) = fmb_fun_li1091306514on_val_2 ) ) ).

tff(declare_map_val_ty,type,
    map_val_ty: fun_val_ty > fun_list_val_list_ty ).

tff(function_map_val_ty,axiom,
    ( ( map_val_ty(fmb_fun_val_ty_1) = fmb_fun_list_val_list_ty_2 )
    & ( map_val_ty(fmb_fun_val_ty_2) = fmb_fun_list_val_list_ty_2 ) ) ).

tff(declare_map_val_val,type,
    map_val_val: fun_val_val > fun_li1707879747st_val ).

tff(function_map_val_val,axiom,
    ( ( map_val_val(fmb_fun_val_val_1) = fmb_fun_li1707879747st_val_2 )
    & ( map_val_val(fmb_fun_val_val_2) = fmb_fun_li1707879747st_val_2 ) ) ).

tff(declare_map_va527586287on_val,type,
    map_va527586287on_val: fun_va172965946on_val > fun_li1659202122on_val ).

tff(function_map_va527586287on_val,axiom,
    ( ( map_va527586287on_val(fmb_fun_va172965946on_val_1) = fmb_fun_li1659202122on_val_2 )
    & ( map_va527586287on_val(fmb_fun_va172965946on_val_2) = fmb_fun_li1659202122on_val_2 ) ) ).

tff(declare_map_Pr1655409582on_val,type,
    map_Pr1655409582on_val: fun_Pr12181427on_val > fun_li1479469629on_val ).

tff(function_map_Pr1655409582on_val,axiom,
    ( ( map_Pr1655409582on_val(fmb_fun_Pr12181427on_val_1) = fmb_fun_li1479469629on_val_2 )
    & ( map_Pr1655409582on_val(fmb_fun_Pr12181427on_val_2) = fmb_fun_li1479469629on_val_2 ) ) ).

tff(declare_set_exp_list_char,type,
    set_exp_list_char: list_exp_list_char > fun_ex736065929r_bool ).

tff(function_set_exp_list_char,axiom,
    set_exp_list_char(fmb_list_exp_list_char_1) = fmb_fun_ex736065929r_bool_2 ).

tff(declare_set_list_char,type,
    set_list_char: list_list_char > fun_list_char_bool ).

tff(function_set_list_char,axiom,
    set_list_char(fmb_list_list_char_1) = fmb_fun_list_char_bool_2 ).

tff(declare_set_option_ty,type,
    set_option_ty: list_option_ty > fun_option_ty_bool ).

tff(function_set_option_ty,axiom,
    set_option_ty(fmb_list_option_ty_1) = fmb_fun_option_ty_bool_2 ).

tff(declare_set_ty,type,
    set_ty: list_ty > fun_ty_bool ).

tff(function_set_ty,axiom,
    ( ( set_ty(fmb_list_ty_1) = fmb_fun_ty_bool_2 )
    & ( set_ty(fmb_list_ty_2) = fmb_fun_ty_bool_2 ) ) ).

tff(declare_set_val,type,
    set_val: list_val > fun_val_bool ).

tff(function_set_val,axiom,
    set_val(fmb_list_val_1) = fmb_fun_val_bool_2 ).

tff(declare_set_Pr1921835862on_val,type,
    set_Pr1921835862on_val: list_P1439941640on_val > fun_Pr691271849l_bool ).

tff(function_set_Pr1921835862on_val,axiom,
    ( ( set_Pr1921835862on_val(fmb_list_P1439941640on_val_1) = fmb_fun_Pr691271849l_bool_2 )
    & ( set_Pr1921835862on_val(fmb_list_P1439941640on_val_2) = fmb_fun_Pr691271849l_bool_2 ) ) ).

tff(declare_map_add_list_char_ty,type,
    map_add_list_char_ty: ( fun_li688206603ion_ty * fun_li688206603ion_ty ) > fun_li688206603ion_ty ).

tff(function_map_add_list_char_ty,axiom,
    ( ( map_add_list_char_ty(fmb_fun_li688206603ion_ty_1,fmb_fun_li688206603ion_ty_1) = fmb_fun_li688206603ion_ty_2 )
    & ( map_add_list_char_ty(fmb_fun_li688206603ion_ty_1,fmb_fun_li688206603ion_ty_2) = fmb_fun_li688206603ion_ty_2 )
    & ( map_add_list_char_ty(fmb_fun_li688206603ion_ty_2,fmb_fun_li688206603ion_ty_1) = fmb_fun_li688206603ion_ty_2 )
    & ( map_add_list_char_ty(fmb_fun_li688206603ion_ty_2,fmb_fun_li688206603ion_ty_2) = fmb_fun_li688206603ion_ty_2 ) ) ).

tff(declare_map_ad325961431ar_val,type,
    map_ad325961431ar_val: ( fun_li1432931796on_val * fun_li1432931796on_val ) > fun_li1432931796on_val ).

tff(function_map_ad325961431ar_val,axiom,
    map_ad325961431ar_val(fmb_fun_li1432931796on_val_1,fmb_fun_li1432931796on_val_1) = fmb_fun_li1432931796on_val_1 ).

tff(declare_map_up891053837har_ty,type,
    map_up891053837har_ty: ( fun_li688206603ion_ty * list_list_char * list_ty ) > fun_li688206603ion_ty ).

tff(function_map_up891053837har_ty,axiom,
    ( ( map_up891053837har_ty(fmb_fun_li688206603ion_ty_1,fmb_list_list_char_1,fmb_list_ty_1) = fmb_fun_li688206603ion_ty_2 )
    & ( map_up891053837har_ty(fmb_fun_li688206603ion_ty_1,fmb_list_list_char_1,fmb_list_ty_2) = fmb_fun_li688206603ion_ty_2 )
    & ( map_up891053837har_ty(fmb_fun_li688206603ion_ty_2,fmb_list_list_char_1,fmb_list_ty_1) = fmb_fun_li688206603ion_ty_2 )
    & ( map_up891053837har_ty(fmb_fun_li688206603ion_ty_2,fmb_list_list_char_1,fmb_list_ty_2) = fmb_fun_li688206603ion_ty_2 ) ) ).

tff(declare_map_up1085636310ar_val,type,
    map_up1085636310ar_val: ( fun_li1432931796on_val * list_list_char * list_val ) > fun_li1432931796on_val ).

tff(function_map_up1085636310ar_val,axiom,
    map_up1085636310ar_val(fmb_fun_li1432931796on_val_1,fmb_list_list_char_1,fmb_list_val_1) = fmb_fun_li1432931796on_val_1 ).

tff(declare_size_s1143674878t_char,type,
    size_s1143674878t_char: list_exp_list_char > nat ).

tff(function_size_s1143674878t_char,axiom,
    size_s1143674878t_char(fmb_list_exp_list_char_1) = fmb_nat_1 ).

tff(declare_size_s2113983095t_char,type,
    size_s2113983095t_char: list_list_char > nat ).

tff(function_size_s2113983095t_char,axiom,
    size_s2113983095t_char(fmb_list_list_char_1) = fmb_nat_1 ).

tff(declare_size_s1050794909ion_ty,type,
    size_s1050794909ion_ty: list_option_ty > nat ).

tff(function_size_s1050794909ion_ty,axiom,
    size_s1050794909ion_ty(fmb_list_option_ty_1) = fmb_nat_1 ).

tff(declare_size_s1595297126on_val,type,
    size_s1595297126on_val: list_option_val > nat ).

tff(function_size_s1595297126on_val,axiom,
    ( ( size_s1595297126on_val(fmb_list_option_val_1) = fmb_nat_1 )
    & ( size_s1595297126on_val(fmb_list_option_val_2) = fmb_nat_1 ) ) ).

tff(declare_size_size_list_ty,type,
    size_size_list_ty: list_ty > nat ).

tff(function_size_size_list_ty,axiom,
    ( ( size_size_list_ty(fmb_list_ty_1) = fmb_nat_1 )
    & ( size_size_list_ty(fmb_list_ty_2) = fmb_nat_1 ) ) ).

tff(declare_size_size_list_val,type,
    size_size_list_val: list_val > nat ).

tff(function_size_size_list_val,axiom,
    size_size_list_val(fmb_list_val_1) = fmb_nat_1 ).

tff(declare_size_s1699857438on_val,type,
    size_s1699857438on_val: list_P1439941640on_val > nat ).

tff(function_size_s1699857438on_val,axiom,
    ( ( size_s1699857438on_val(fmb_list_P1439941640on_val_1) = fmb_nat_1 )
    & ( size_s1699857438on_val(fmb_list_P1439941640on_val_2) = fmb_nat_1 ) ) ).

tff(declare_hext,type,
    hext: ( fun_na939144002on_val * fun_na939144002on_val ) > bool ).

tff(function_hext,axiom,
    hext(fmb_fun_na939144002on_val_1,fmb_fun_na939144002on_val_1) = fmb_bool_2 ).

tff(declare_typeof_h,type,
    typeof_h: fun_na939144002on_val > fun_val_option_ty ).

tff(function_typeof_h,axiom,
    typeof_h(fmb_fun_na939144002on_val_1) = fmb_fun_val_option_ty_1 ).

tff(declare_produc1259058957on_val,type,
    produc1259058957on_val: ( exp_list_char * produc12694297on_val ) > produc124828825on_val ).

tff(function_produc1259058957on_val,axiom,
    produc1259058957on_val(fmb_exp_list_char_1,fmb_produc12694297on_val_1) = fmb_produc124828825on_val_1 ).

tff(declare_produc921874948t_char,type,
    produc921874948t_char: ( list_list_char * produc220283002t_char ) > produc1285161482t_char ).

tff(function_produc921874948t_char,axiom,
    ( ( produc921874948t_char(fmb_list_list_char_1,fmb_produc220283002t_char_1) = fmb_produc1285161482t_char_2 )
    & ( produc921874948t_char(fmb_list_list_char_1,fmb_produc220283002t_char_2) = fmb_produc1285161482t_char_1 ) ) ).

tff(declare_produc823076510on_val,type,
    produc823076510on_val: ( list_char * fun_Pr806764899on_val ) > produc639455274on_val ).

tff(function_produc823076510on_val,axiom,
    ( ( produc823076510on_val(fmb_list_char_1,fmb_fun_Pr806764899on_val_1) = fmb_produc639455274on_val_2 )
    & ( produc823076510on_val(fmb_list_char_1,fmb_fun_Pr806764899on_val_2) = fmb_produc639455274on_val_1 ) ) ).

tff(declare_produc1909267824t_char,type,
    produc1909267824t_char: ( list_ty * produc662261637t_char ) > produc220283002t_char ).

tff(function_produc1909267824t_char,axiom,
    ( ( produc1909267824t_char(fmb_list_ty_1,fmb_produc662261637t_char_1) = fmb_produc220283002t_char_2 )
    & ( produc1909267824t_char(fmb_list_ty_2,fmb_produc662261637t_char_1) = fmb_produc220283002t_char_1 ) ) ).

tff(declare_produc1916172923t_char,type,
    produc1916172923t_char: ( list_val * exp_list_char ) > produc662261637t_char ).

tff(function_produc1916172923t_char,axiom,
    produc1916172923t_char(fmb_list_val_1,fmb_exp_list_char_1) = fmb_produc662261637t_char_1 ).

tff(declare_produc899768717on_val,type,
    produc899768717on_val: ( fun_na939144002on_val * fun_li1432931796on_val ) > produc12694297on_val ).

tff(function_produc899768717on_val,axiom,
    produc899768717on_val(fmb_fun_na939144002on_val_1,fmb_fun_li1432931796on_val_1) = fmb_produc12694297on_val_1 ).

tff(declare_produc1441475159on_val,type,
    produc1441475159on_val: ( produc124828825on_val * produc124828825on_val ) > produc1102272487on_val ).

tff(function_produc1441475159on_val,axiom,
    produc1441475159on_val(fmb_produc124828825on_val_1,fmb_produc124828825on_val_1) = fmb_produc1102272487on_val_1 ).

tff(declare_produc24551831t_char,type,
    produc24551831t_char: ( produc1285161482t_char * produc1285161482t_char ) > produc349695911t_char ).

tff(function_produc24551831t_char,axiom,
    ( ( produc24551831t_char(fmb_produc1285161482t_char_1,fmb_produc1285161482t_char_1) = fmb_produc349695911t_char_2 )
    & ( produc24551831t_char(fmb_produc1285161482t_char_1,fmb_produc1285161482t_char_2) = fmb_produc349695911t_char_2 )
    & ( produc24551831t_char(fmb_produc1285161482t_char_2,fmb_produc1285161482t_char_1) = fmb_produc349695911t_char_2 )
    & ( produc24551831t_char(fmb_produc1285161482t_char_2,fmb_produc1285161482t_char_2) = fmb_produc349695911t_char_2 ) ) ).

tff(declare_produc499151895on_val,type,
    produc499151895on_val: ( produc639455274on_val * produc639455274on_val ) > produc87279271on_val ).

tff(function_produc499151895on_val,axiom,
    ( ( produc499151895on_val(fmb_produc639455274on_val_1,fmb_produc639455274on_val_1) = fmb_produc87279271on_val_2 )
    & ( produc499151895on_val(fmb_produc639455274on_val_1,fmb_produc639455274on_val_2) = fmb_produc87279271on_val_2 )
    & ( produc499151895on_val(fmb_produc639455274on_val_2,fmb_produc639455274on_val_1) = fmb_produc87279271on_val_2 )
    & ( produc499151895on_val(fmb_produc639455274on_val_2,fmb_produc639455274on_val_2) = fmb_produc87279271on_val_2 ) ) ).

tff(declare_produc57279289t_char,type,
    produc57279289t_char: ( produc220283002t_char * produc220283002t_char ) > produc1406897475t_char ).

tff(function_produc57279289t_char,axiom,
    ( ( produc57279289t_char(fmb_produc220283002t_char_1,fmb_produc220283002t_char_1) = fmb_produc1406897475t_char_2 )
    & ( produc57279289t_char(fmb_produc220283002t_char_1,fmb_produc220283002t_char_2) = fmb_produc1406897475t_char_2 )
    & ( produc57279289t_char(fmb_produc220283002t_char_2,fmb_produc220283002t_char_1) = fmb_produc1406897475t_char_2 )
    & ( produc57279289t_char(fmb_produc220283002t_char_2,fmb_produc220283002t_char_2) = fmb_produc1406897475t_char_2 ) ) ).

tff(declare_produc1299387215t_char,type,
    produc1299387215t_char: ( produc662261637t_char * produc662261637t_char ) > produc1826280281t_char ).

tff(function_produc1299387215t_char,axiom,
    produc1299387215t_char(fmb_produc662261637t_char_1,fmb_produc662261637t_char_1) = fmb_produc1826280281t_char_2 ).

tff(declare_produc870913623on_val,type,
    produc870913623on_val: ( produc12694297on_val * produc12694297on_val ) > produc409205479on_val ).

tff(function_produc870913623on_val,axiom,
    produc870913623on_val(fmb_produc12694297on_val_1,fmb_produc12694297on_val_1) = fmb_produc409205479on_val_2 ).

tff(declare_produc1564932627on_val,type,
    produc1564932627on_val: ( produc1102272487on_val * produc1102272487on_val ) > produc231486621on_val ).

tff(function_produc1564932627on_val,axiom,
    produc1564932627on_val(fmb_produc1102272487on_val_1,fmb_produc1102272487on_val_1) = fmb_produc231486621on_val_2 ).

tff(declare_produc1911975310l_bool,type,
    produc1911975310l_bool: fun_Pr680585871l_bool > fun_ex1201926843l_bool ).

tff(function_produc1911975310l_bool,axiom,
    ( ( produc1911975310l_bool(fmb_fun_Pr680585871l_bool_1) = fmb_fun_ex1201926843l_bool_2 )
    & ( produc1911975310l_bool(fmb_fun_Pr680585871l_bool_2) = fmb_fun_ex1201926843l_bool_2 ) ) ).

tff(declare_produc1574020101r_bool,type,
    produc1574020101r_bool: fun_Pr227936640r_bool > fun_li1024794712r_bool ).

tff(function_produc1574020101r_bool,axiom,
    ( ( produc1574020101r_bool(fmb_fun_Pr227936640r_bool_1) = fmb_fun_li1024794712r_bool_2 )
    & ( produc1574020101r_bool(fmb_fun_Pr227936640r_bool_2) = fmb_fun_li1024794712r_bool_2 ) ) ).

tff(declare_produc481748255l_bool,type,
    produc481748255l_bool: fun_Pr315804320l_bool > fun_li823162622l_bool ).

tff(function_produc481748255l_bool,axiom,
    ( ( produc481748255l_bool(fmb_fun_Pr315804320l_bool_1) = fmb_fun_li823162622l_bool_2 )
    & ( produc481748255l_bool(fmb_fun_Pr315804320l_bool_2) = fmb_fun_li823162622l_bool_2 ) ) ).

tff(declare_produc156891095r_bool,type,
    produc156891095r_bool: fun_Pr46158268r_bool > fun_li887890578r_bool ).

tff(function_produc156891095r_bool,axiom,
    ( ( produc156891095r_bool(fmb_fun_Pr46158268r_bool_1) = fmb_fun_li887890578r_bool_2 )
    & ( produc156891095r_bool(fmb_fun_Pr46158268r_bool_2) = fmb_fun_li887890578r_bool_2 ) ) ).

tff(declare_produc550034914r_bool,type,
    produc550034914r_bool: fun_Pr827765831r_bool > fun_li826105035r_bool ).

tff(function_produc550034914r_bool,axiom,
    ( ( produc550034914r_bool(fmb_fun_Pr827765831r_bool_1) = fmb_fun_li826105035r_bool_2 )
    & ( produc550034914r_bool(fmb_fun_Pr827765831r_bool_2) = fmb_fun_li826105035r_bool_2 ) ) ).

tff(declare_produc2062775566l_bool,type,
    produc2062775566l_bool: fun_Pr1696029455l_bool > fun_fu100249073l_bool ).

tff(function_produc2062775566l_bool,axiom,
    ( ( produc2062775566l_bool(fmb_fun_Pr1696029455l_bool_1) = fmb_fun_fu100249073l_bool_2 )
    & ( produc2062775566l_bool(fmb_fun_Pr1696029455l_bool_2) = fmb_fun_fu100249073l_bool_2 ) ) ).

tff(declare_produc1159035454l_bool,type,
    produc1159035454l_bool: fun_Pr691271849l_bool > fun_Pr633696065l_bool ).

tff(function_produc1159035454l_bool,axiom,
    ( ( produc1159035454l_bool(fmb_fun_Pr691271849l_bool_1) = fmb_fun_Pr633696065l_bool_2 )
    & ( produc1159035454l_bool(fmb_fun_Pr691271849l_bool_2) = fmb_fun_Pr633696065l_bool_2 ) ) ).

tff(declare_blocks,type,
    blocks: produc1285161482t_char > exp_list_char ).

tff(function_blocks,axiom,
    ( ( blocks(fmb_produc1285161482t_char_1) = fmb_exp_list_char_1 )
    & ( blocks(fmb_produc1285161482t_char_2) = fmb_exp_list_char_1 ) ) ).

tff(declare_red,type,
    red: list_P1999446415t_char > fun_Pr691271849l_bool ).

tff(function_red,axiom,
    ( ( red(fmb_list_P1999446415t_char_1) = fmb_fun_Pr691271849l_bool_2 )
    & ( red(fmb_list_P1999446415t_char_2) = fmb_fun_Pr691271849l_bool_2 ) ) ).

tff(declare_transi2024712006on_val,type,
    transi2024712006on_val: fun_Pr691271849l_bool > fun_Pr691271849l_bool ).

tff(function_transi2024712006on_val,axiom,
    ( ( transi2024712006on_val(fmb_fun_Pr691271849l_bool_1) = fmb_fun_Pr691271849l_bool_2 )
    & ( transi2024712006on_val(fmb_fun_Pr691271849l_bool_2) = fmb_fun_Pr691271849l_bool_2 ) ) ).

tff(declare_transi122195895t_char,type,
    transi122195895t_char: fun_Pr1895638121r_bool > fun_Pr1895638121r_bool ).

tff(function_transi122195895t_char,axiom,
    ( ( transi122195895t_char(fmb_fun_Pr1895638121r_bool_1) = fmb_fun_Pr1895638121r_bool_2 )
    & ( transi122195895t_char(fmb_fun_Pr1895638121r_bool_2) = fmb_fun_Pr1895638121r_bool_2 ) ) ).

tff(declare_transi61620055on_val,type,
    transi61620055on_val: fun_Pr235369833l_bool > fun_Pr235369833l_bool ).

tff(function_transi61620055on_val,axiom,
    ( ( transi61620055on_val(fmb_fun_Pr235369833l_bool_1) = fmb_fun_Pr235369833l_bool_2 )
    & ( transi61620055on_val(fmb_fun_Pr235369833l_bool_2) = fmb_fun_Pr235369833l_bool_2 ) ) ).

tff(declare_transi1257872013t_char,type,
    transi1257872013t_char: fun_Pr1728267013r_bool > fun_Pr1728267013r_bool ).

tff(function_transi1257872013t_char,axiom,
    ( ( transi1257872013t_char(fmb_fun_Pr1728267013r_bool_1) = fmb_fun_Pr1728267013r_bool_2 )
    & ( transi1257872013t_char(fmb_fun_Pr1728267013r_bool_2) = fmb_fun_Pr1728267013r_bool_2 ) ) ).

tff(declare_transi1789604888t_char,type,
    transi1789604888t_char: fun_Pr1890037787r_bool > fun_Pr1890037787r_bool ).

tff(function_transi1789604888t_char,axiom,
    ( ( transi1789604888t_char(fmb_fun_Pr1890037787r_bool_1) = fmb_fun_Pr1890037787r_bool_2 )
    & ( transi1789604888t_char(fmb_fun_Pr1890037787r_bool_2) = fmb_fun_Pr1890037787r_bool_2 ) ) ).

tff(declare_transi921647814on_val,type,
    transi921647814on_val: fun_Pr693020585l_bool > fun_Pr693020585l_bool ).

tff(function_transi921647814on_val,axiom,
    ( ( transi921647814on_val(fmb_fun_Pr693020585l_bool_1) = fmb_fun_Pr693020585l_bool_2 )
    & ( transi921647814on_val(fmb_fun_Pr693020585l_bool_2) = fmb_fun_Pr693020585l_bool_2 ) ) ).

tff(declare_transi910771962on_val,type,
    transi910771962on_val: fun_Pr903661919l_bool > fun_Pr903661919l_bool ).

tff(function_transi910771962on_val,axiom,
    ( ( transi910771962on_val(fmb_fun_Pr903661919l_bool_1) = fmb_fun_Pr903661919l_bool_2 )
    & ( transi910771962on_val(fmb_fun_Pr903661919l_bool_2) = fmb_fun_Pr903661919l_bool_2 ) ) ).

tff(declare_widen_2090681816t_char,type,
    widen_2090681816t_char: list_P1999446415t_char > fun_ty_fun_ty_bool ).

tff(function_widen_2090681816t_char,axiom,
    ( ( widen_2090681816t_char(fmb_list_P1999446415t_char_1) = fmb_fun_ty_fun_ty_bool_2 )
    & ( widen_2090681816t_char(fmb_list_P1999446415t_char_2) = fmb_fun_ty_fun_ty_bool_2 ) ) ).

tff(declare_wTrt,type,
    wTrt: ( list_P1999446415t_char * fun_na939144002on_val * fun_li688206603ion_ty * exp_list_char * ty ) > bool ).

tff(function_wTrt,axiom,
    ( ( wTrt(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_exp_list_char_1,fmb_ty_1) = fmb_bool_2 )
    & ( wTrt(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_exp_list_char_1,fmb_ty_2) = fmb_bool_2 )
    & ( wTrt(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_exp_list_char_1,fmb_ty_1) = fmb_bool_1 )
    & ( wTrt(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_exp_list_char_1,fmb_ty_2) = fmb_bool_2 )
    & ( wTrt(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_exp_list_char_1,fmb_ty_1) = fmb_bool_2 )
    & ( wTrt(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_exp_list_char_1,fmb_ty_2) = fmb_bool_2 )
    & ( wTrt(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_exp_list_char_1,fmb_ty_1) = fmb_bool_1 )
    & ( wTrt(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_exp_list_char_1,fmb_ty_2) = fmb_bool_2 ) ) ).

tff(declare_wTrts,type,
    wTrts: ( list_P1999446415t_char * fun_na939144002on_val * fun_li688206603ion_ty * list_exp_list_char * list_ty ) > bool ).

tff(function_wTrts,axiom,
    ( ( wTrts(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_list_exp_list_char_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_list_exp_list_char_1,fmb_list_ty_2) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_list_exp_list_char_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_1,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_list_exp_list_char_1,fmb_list_ty_2) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_list_exp_list_char_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_1,fmb_list_exp_list_char_1,fmb_list_ty_2) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_list_exp_list_char_1,fmb_list_ty_1) = fmb_bool_2 )
    & ( wTrts(fmb_list_P1999446415t_char_2,fmb_fun_na939144002on_val_1,fmb_fun_li688206603ion_ty_2,fmb_list_exp_list_char_1,fmb_list_ty_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_e1353749905t_char,type,
    hAPP_e1353749905t_char: ( fun_ex1654222579t_char * exp_list_char ) > exp_list_char ).

tff(function_hAPP_e1353749905t_char,axiom,
    ( ( hAPP_e1353749905t_char(fmb_fun_ex1654222579t_char_1,fmb_exp_list_char_1) = fmb_exp_list_char_1 )
    & ( hAPP_e1353749905t_char(fmb_fun_ex1654222579t_char_2,fmb_exp_list_char_1) = fmb_exp_list_char_1 ) ) ).

tff(declare_hAPP_e544220455r_bool,type,
    hAPP_e544220455r_bool: ( fun_ex736065929r_bool * exp_list_char ) > bool ).

tff(function_hAPP_e544220455r_bool,axiom,
    ( ( hAPP_e544220455r_bool(fmb_fun_ex736065929r_bool_1,fmb_exp_list_char_1) = fmb_bool_2 )
    & ( hAPP_e544220455r_bool(fmb_fun_ex736065929r_bool_2,fmb_exp_list_char_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_e1833980889l_bool,type,
    hAPP_e1833980889l_bool: ( fun_ex1201926843l_bool * exp_list_char ) > fun_Pr1696029455l_bool ).

tff(function_hAPP_e1833980889l_bool,axiom,
    ( ( hAPP_e1833980889l_bool(fmb_fun_ex1201926843l_bool_1,fmb_exp_list_char_1) = fmb_fun_Pr1696029455l_bool_2 )
    & ( hAPP_e1833980889l_bool(fmb_fun_ex1201926843l_bool_2,fmb_exp_list_char_1) = fmb_fun_Pr1696029455l_bool_2 ) ) ).

tff(declare_hAPP_l2011456725t_char,type,
    hAPP_l2011456725t_char: ( fun_li1279027773t_char * list_exp_list_char ) > list_exp_list_char ).

tff(function_hAPP_l2011456725t_char,axiom,
    ( ( hAPP_l2011456725t_char(fmb_fun_li1279027773t_char_1,fmb_list_exp_list_char_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l2011456725t_char(fmb_fun_li1279027773t_char_2,fmb_list_exp_list_char_1) = fmb_list_exp_list_char_1 ) ) ).

tff(declare_hAPP_l2065413838t_char,type,
    hAPP_l2065413838t_char: ( fun_li218321462t_char * list_exp_list_char ) > list_list_char ).

tff(function_hAPP_l2065413838t_char,axiom,
    ( ( hAPP_l2065413838t_char(fmb_fun_li218321462t_char_1,fmb_list_exp_list_char_1) = fmb_list_list_char_1 )
    & ( hAPP_l2065413838t_char(fmb_fun_li218321462t_char_2,fmb_list_exp_list_char_1) = fmb_list_list_char_1 ) ) ).

tff(declare_hAPP_l1002225652ion_ty,type,
    hAPP_l1002225652ion_ty: ( fun_li241576028ion_ty * list_exp_list_char ) > list_option_ty ).

tff(function_hAPP_l1002225652ion_ty,axiom,
    ( ( hAPP_l1002225652ion_ty(fmb_fun_li241576028ion_ty_1,fmb_list_exp_list_char_1) = fmb_list_option_ty_1 )
    & ( hAPP_l1002225652ion_ty(fmb_fun_li241576028ion_ty_2,fmb_list_exp_list_char_1) = fmb_list_option_ty_1 ) ) ).

tff(declare_hAPP_l1607890493on_val,type,
    hAPP_l1607890493on_val: ( fun_li690207653on_val * list_exp_list_char ) > list_option_val ).

tff(function_hAPP_l1607890493on_val,axiom,
    ( ( hAPP_l1607890493on_val(fmb_fun_li690207653on_val_1,fmb_list_exp_list_char_1) = fmb_list_option_val_2 )
    & ( hAPP_l1607890493on_val(fmb_fun_li690207653on_val_2,fmb_list_exp_list_char_1) = fmb_list_option_val_2 ) ) ).

tff(declare_hAPP_l110066169ist_ty,type,
    hAPP_l110066169ist_ty: ( fun_li1055333287ist_ty * list_exp_list_char ) > list_ty ).

tff(function_hAPP_l110066169ist_ty,axiom,
    ( ( hAPP_l110066169ist_ty(fmb_fun_li1055333287ist_ty_1,fmb_list_exp_list_char_1) = fmb_list_ty_1 )
    & ( hAPP_l110066169ist_ty(fmb_fun_li1055333287ist_ty_2,fmb_list_exp_list_char_1) = fmb_list_ty_1 ) ) ).

tff(declare_hAPP_l1539861698st_val,type,
    hAPP_l1539861698st_val: ( fun_li363341936st_val * list_exp_list_char ) > list_val ).

tff(function_hAPP_l1539861698st_val,axiom,
    ( ( hAPP_l1539861698st_val(fmb_fun_li363341936st_val_1,fmb_list_exp_list_char_1) = fmb_list_val_1 )
    & ( hAPP_l1539861698st_val(fmb_fun_li363341936st_val_2,fmb_list_exp_list_char_1) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l1557845365on_val,type,
    hAPP_l1557845365on_val: ( fun_li1581546589on_val * list_exp_list_char ) > list_P1439941640on_val ).

tff(function_hAPP_l1557845365on_val,axiom,
    ( ( hAPP_l1557845365on_val(fmb_fun_li1581546589on_val_1,fmb_list_exp_list_char_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1557845365on_val(fmb_fun_li1581546589on_val_2,fmb_list_exp_list_char_1) = fmb_list_P1439941640on_val_2 ) ) ).

tff(declare_hAPP_l740678812t_char,type,
    hAPP_l740678812t_char: ( fun_li567129860t_char * list_list_char ) > list_exp_list_char ).

tff(function_hAPP_l740678812t_char,axiom,
    ( ( hAPP_l740678812t_char(fmb_fun_li567129860t_char_1,fmb_list_list_char_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l740678812t_char(fmb_fun_li567129860t_char_2,fmb_list_list_char_1) = fmb_list_exp_list_char_1 ) ) ).

tff(declare_hAPP_l407174677t_char,type,
    hAPP_l407174677t_char: ( fun_li1898638973t_char * list_list_char ) > list_list_char ).

tff(function_hAPP_l407174677t_char,axiom,
    ( ( hAPP_l407174677t_char(fmb_fun_li1898638973t_char_1,fmb_list_list_char_1) = fmb_list_list_char_1 )
    & ( hAPP_l407174677t_char(fmb_fun_li1898638973t_char_2,fmb_list_list_char_1) = fmb_list_list_char_1 ) ) ).

tff(declare_hAPP_l1491470139ion_ty,type,
    hAPP_l1491470139ion_ty: ( fun_li1921893539ion_ty * list_list_char ) > list_option_ty ).

tff(function_hAPP_l1491470139ion_ty,axiom,
    ( ( hAPP_l1491470139ion_ty(fmb_fun_li1921893539ion_ty_1,fmb_list_list_char_1) = fmb_list_option_ty_1 )
    & ( hAPP_l1491470139ion_ty(fmb_fun_li1921893539ion_ty_2,fmb_list_list_char_1) = fmb_list_option_ty_1 ) ) ).

tff(declare_hAPP_l297961988on_val,type,
    hAPP_l297961988on_val: ( fun_li1580442732on_val * list_list_char ) > list_option_val ).

tff(function_hAPP_l297961988on_val,axiom,
    ( ( hAPP_l297961988on_val(fmb_fun_li1580442732on_val_1,fmb_list_list_char_1) = fmb_list_option_val_2 )
    & ( hAPP_l297961988on_val(fmb_fun_li1580442732on_val_2,fmb_list_list_char_1) = fmb_list_option_val_2 ) ) ).

tff(declare_hAPP_l1871878770ist_ty,type,
    hAPP_l1871878770ist_ty: ( fun_li490940192ist_ty * list_list_char ) > list_ty ).

tff(function_hAPP_l1871878770ist_ty,axiom,
    ( ( hAPP_l1871878770ist_ty(fmb_fun_li490940192ist_ty_1,fmb_list_list_char_1) = fmb_list_ty_1 )
    & ( hAPP_l1871878770ist_ty(fmb_fun_li490940192ist_ty_2,fmb_list_list_char_1) = fmb_list_ty_1 ) ) ).

tff(declare_hAPP_l1892737211st_val,type,
    hAPP_l1892737211st_val: ( fun_li742655849st_val * list_list_char ) > list_val ).

tff(function_hAPP_l1892737211st_val,axiom,
    ( ( hAPP_l1892737211st_val(fmb_fun_li742655849st_val_1,fmb_list_list_char_1) = fmb_list_val_1 )
    & ( hAPP_l1892737211st_val(fmb_fun_li742655849st_val_2,fmb_list_list_char_1) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l418486716on_val,type,
    hAPP_l418486716on_val: ( fun_li1867552164on_val * list_list_char ) > list_P1439941640on_val ).

tff(function_hAPP_l418486716on_val,axiom,
    ( ( hAPP_l418486716on_val(fmb_fun_li1867552164on_val_1,fmb_list_list_char_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l418486716on_val(fmb_fun_li1867552164on_val_2,fmb_list_list_char_1) = fmb_list_P1439941640on_val_2 ) ) ).

tff(declare_hAPP_l217977712r_bool,type,
    hAPP_l217977712r_bool: ( fun_li1024794712r_bool * list_list_char ) > fun_Pr46158268r_bool ).

tff(function_hAPP_l217977712r_bool,axiom,
    ( ( hAPP_l217977712r_bool(fmb_fun_li1024794712r_bool_1,fmb_list_list_char_1) = fmb_fun_Pr46158268r_bool_2 )
    & ( hAPP_l217977712r_bool(fmb_fun_li1024794712r_bool_2,fmb_list_list_char_1) = fmb_fun_Pr46158268r_bool_2 ) ) ).

tff(declare_hAPP_l330149622t_char,type,
    hAPP_l330149622t_char: ( fun_li156600670t_char * list_option_ty ) > list_exp_list_char ).

tff(function_hAPP_l330149622t_char,axiom,
    ( ( hAPP_l330149622t_char(fmb_fun_li156600670t_char_1,fmb_list_option_ty_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l330149622t_char(fmb_fun_li156600670t_char_2,fmb_list_option_ty_1) = fmb_list_exp_list_char_1 ) ) ).

tff(declare_hAPP_l1368737135t_char,type,
    hAPP_l1368737135t_char: ( fun_li712717783t_char * list_option_ty ) > list_list_char ).

tff(function_hAPP_l1368737135t_char,axiom,
    ( ( hAPP_l1368737135t_char(fmb_fun_li712717783t_char_1,fmb_list_option_ty_1) = fmb_list_list_char_1 )
    & ( hAPP_l1368737135t_char(fmb_fun_li712717783t_char_2,fmb_list_option_ty_1) = fmb_list_list_char_1 ) ) ).

tff(declare_hAPP_l305548949ion_ty,type,
    hAPP_l305548949ion_ty: ( fun_li735972349ion_ty * list_option_ty ) > list_option_ty ).

tff(function_hAPP_l305548949ion_ty,axiom,
    ( ( hAPP_l305548949ion_ty(fmb_fun_li735972349ion_ty_1,fmb_list_option_ty_1) = fmb_list_option_ty_1 )
    & ( hAPP_l305548949ion_ty(fmb_fun_li735972349ion_ty_2,fmb_list_option_ty_1) = fmb_list_option_ty_1 ) ) ).

tff(declare_hAPP_l1583451544ist_ty,type,
    hAPP_l1583451544ist_ty: ( fun_li202512966ist_ty * list_option_ty ) > list_ty ).

tff(function_hAPP_l1583451544ist_ty,axiom,
    ( ( hAPP_l1583451544ist_ty(fmb_fun_li202512966ist_ty_1,fmb_list_option_ty_1) = fmb_list_ty_1 )
    & ( hAPP_l1583451544ist_ty(fmb_fun_li202512966ist_ty_2,fmb_list_option_ty_1) = fmb_list_ty_1 ) ) ).

tff(declare_hAPP_l336371937st_val,type,
    hAPP_l336371937st_val: ( fun_li1333774223st_val * list_option_ty ) > list_val ).

tff(function_hAPP_l336371937st_val,axiom,
    ( ( hAPP_l336371937st_val(fmb_fun_li1333774223st_val_1,fmb_list_option_ty_1) = fmb_list_val_1 )
    & ( hAPP_l336371937st_val(fmb_fun_li1333774223st_val_2,fmb_list_option_ty_1) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l228474410st_val,type,
    hAPP_l228474410st_val: ( fun_li1459524056st_val * list_option_val ) > list_val ).

tff(function_hAPP_l228474410st_val,axiom,
    ( ( hAPP_l228474410st_val(fmb_fun_li1459524056st_val_1,fmb_list_option_val_1) = fmb_list_val_1 )
    & ( hAPP_l228474410st_val(fmb_fun_li1459524056st_val_1,fmb_list_option_val_2) = fmb_list_val_1 )
    & ( hAPP_l228474410st_val(fmb_fun_li1459524056st_val_2,fmb_list_option_val_1) = fmb_list_val_1 )
    & ( hAPP_l228474410st_val(fmb_fun_li1459524056st_val_2,fmb_list_option_val_2) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l1074208899t_char,type,
    hAPP_l1074208899t_char: ( fun_li1751394789t_char * list_char ) > list_char ).

tff(function_hAPP_l1074208899t_char,axiom,
    ( ( hAPP_l1074208899t_char(fmb_fun_li1751394789t_char_1,fmb_list_char_1) = fmb_list_char_1 )
    & ( hAPP_l1074208899t_char(fmb_fun_li1751394789t_char_2,fmb_list_char_1) = fmb_list_char_1 ) ) ).

tff(declare_hAPP_l512744617ion_ty,type,
    hAPP_l512744617ion_ty: ( fun_li688206603ion_ty * list_char ) > option_ty ).

tff(function_hAPP_l512744617ion_ty,axiom,
    ( ( hAPP_l512744617ion_ty(fmb_fun_li688206603ion_ty_1,fmb_list_char_1) = fmb_option_ty_1 )
    & ( hAPP_l512744617ion_ty(fmb_fun_li688206603ion_ty_2,fmb_list_char_1) = fmb_option_ty_1 ) ) ).

tff(declare_hAPP_l207779698on_val,type,
    hAPP_l207779698on_val: ( fun_li1432931796on_val * list_char ) > option_val ).

tff(function_hAPP_l207779698on_val,axiom,
    hAPP_l207779698on_val(fmb_fun_li1432931796on_val_1,fmb_list_char_1) = fmb_option_val_2 ).

tff(declare_hAPP_list_char_val,type,
    hAPP_list_char_val: ( fun_list_char_val * list_char ) > val ).

tff(function_hAPP_list_char_val,axiom,
    ( ( hAPP_list_char_val(fmb_fun_list_char_val_1,fmb_list_char_1) = fmb_val_2 )
    & ( hAPP_list_char_val(fmb_fun_list_char_val_2,fmb_list_char_1) = fmb_val_2 ) ) ).

tff(declare_hAPP_l465799708l_bool,type,
    hAPP_l465799708l_bool: ( fun_li823162622l_bool * list_char ) > fun_fu177229913l_bool ).

tff(function_hAPP_l465799708l_bool,axiom,
    ( ( hAPP_l465799708l_bool(fmb_fun_li823162622l_bool_1,fmb_list_char_1) = fmb_fun_fu177229913l_bool_2 )
    & ( hAPP_l465799708l_bool(fmb_fun_li823162622l_bool_2,fmb_list_char_1) = fmb_fun_fu177229913l_bool_2 ) ) ).

tff(declare_hAPP_l578807295t_char,type,
    hAPP_l578807295t_char: ( fun_li1975737011t_char * list_ty ) > list_exp_list_char ).

tff(function_hAPP_l578807295t_char,axiom,
    ( ( hAPP_l578807295t_char(fmb_fun_li1975737011t_char_1,fmb_list_ty_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l578807295t_char(fmb_fun_li1975737011t_char_1,fmb_list_ty_2) = fmb_list_exp_list_char_1 )
    & ( hAPP_l578807295t_char(fmb_fun_li1975737011t_char_2,fmb_list_ty_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l578807295t_char(fmb_fun_li1975737011t_char_2,fmb_list_ty_2) = fmb_list_exp_list_char_1 ) ) ).

tff(declare_hAPP_l402740472t_char,type,
    hAPP_l402740472t_char: ( fun_li2094888364t_char * list_ty ) > list_list_char ).

tff(function_hAPP_l402740472t_char,axiom,
    ( ( hAPP_l402740472t_char(fmb_fun_li2094888364t_char_1,fmb_list_ty_1) = fmb_list_list_char_1 )
    & ( hAPP_l402740472t_char(fmb_fun_li2094888364t_char_1,fmb_list_ty_2) = fmb_list_list_char_1 )
    & ( hAPP_l402740472t_char(fmb_fun_li2094888364t_char_2,fmb_list_ty_1) = fmb_list_list_char_1 )
    & ( hAPP_l402740472t_char(fmb_fun_li2094888364t_char_2,fmb_list_ty_2) = fmb_list_list_char_1 ) ) ).

tff(declare_hAPP_l1487035934ion_ty,type,
    hAPP_l1487035934ion_ty: ( fun_li2118142930ion_ty * list_ty ) > list_option_ty ).

tff(function_hAPP_l1487035934ion_ty,axiom,
    ( ( hAPP_l1487035934ion_ty(fmb_fun_li2118142930ion_ty_1,fmb_list_ty_1) = fmb_list_option_ty_1 )
    & ( hAPP_l1487035934ion_ty(fmb_fun_li2118142930ion_ty_1,fmb_list_ty_2) = fmb_list_option_ty_1 )
    & ( hAPP_l1487035934ion_ty(fmb_fun_li2118142930ion_ty_2,fmb_list_ty_1) = fmb_list_option_ty_1 )
    & ( hAPP_l1487035934ion_ty(fmb_fun_li2118142930ion_ty_2,fmb_list_ty_2) = fmb_list_option_ty_1 ) ) ).

tff(declare_hAPP_l1014734695on_val,type,
    hAPP_l1014734695on_val: ( fun_li1110934555on_val * list_ty ) > list_option_val ).

tff(function_hAPP_l1014734695on_val,axiom,
    ( ( hAPP_l1014734695on_val(fmb_fun_li1110934555on_val_1,fmb_list_ty_1) = fmb_list_option_val_2 )
    & ( hAPP_l1014734695on_val(fmb_fun_li1110934555on_val_1,fmb_list_ty_2) = fmb_list_option_val_2 )
    & ( hAPP_l1014734695on_val(fmb_fun_li1110934555on_val_2,fmb_list_ty_1) = fmb_list_option_val_2 )
    & ( hAPP_l1014734695on_val(fmb_fun_li1110934555on_val_2,fmb_list_ty_2) = fmb_list_option_val_2 ) ) ).

tff(declare_hAPP_list_ty_list_ty,type,
    hAPP_list_ty_list_ty: ( fun_list_ty_list_ty * list_ty ) > list_ty ).

tff(function_hAPP_list_ty_list_ty,axiom,
    ( ( hAPP_list_ty_list_ty(fmb_fun_list_ty_list_ty_1,fmb_list_ty_1) = fmb_list_ty_1 )
    & ( hAPP_list_ty_list_ty(fmb_fun_list_ty_list_ty_1,fmb_list_ty_2) = fmb_list_ty_1 )
    & ( hAPP_list_ty_list_ty(fmb_fun_list_ty_list_ty_2,fmb_list_ty_1) = fmb_list_ty_1 )
    & ( hAPP_list_ty_list_ty(fmb_fun_list_ty_list_ty_2,fmb_list_ty_2) = fmb_list_ty_1 ) ) ).

tff(declare_hAPP_l1530663448st_val,type,
    hAPP_l1530663448st_val: ( fun_list_ty_list_val * list_ty ) > list_val ).

tff(function_hAPP_l1530663448st_val,axiom,
    ( ( hAPP_l1530663448st_val(fmb_fun_list_ty_list_val_1,fmb_list_ty_1) = fmb_list_val_1 )
    & ( hAPP_l1530663448st_val(fmb_fun_list_ty_list_val_1,fmb_list_ty_2) = fmb_list_val_1 )
    & ( hAPP_l1530663448st_val(fmb_fun_list_ty_list_val_2,fmb_list_ty_1) = fmb_list_val_1 )
    & ( hAPP_l1530663448st_val(fmb_fun_list_ty_list_val_2,fmb_list_ty_2) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l1634001311on_val,type,
    hAPP_l1634001311on_val: ( fun_li1883640275on_val * list_ty ) > list_P1439941640on_val ).

tff(function_hAPP_l1634001311on_val,axiom,
    ( ( hAPP_l1634001311on_val(fmb_fun_li1883640275on_val_1,fmb_list_ty_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1634001311on_val(fmb_fun_li1883640275on_val_1,fmb_list_ty_2) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1634001311on_val(fmb_fun_li1883640275on_val_2,fmb_list_ty_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1634001311on_val(fmb_fun_li1883640275on_val_2,fmb_list_ty_2) = fmb_list_P1439941640on_val_2 ) ) ).

tff(declare_hAPP_l1987619678r_bool,type,
    hAPP_l1987619678r_bool: ( fun_li887890578r_bool * list_ty ) > fun_Pr827765831r_bool ).

tff(function_hAPP_l1987619678r_bool,axiom,
    ( ( hAPP_l1987619678r_bool(fmb_fun_li887890578r_bool_1,fmb_list_ty_1) = fmb_fun_Pr827765831r_bool_2 )
    & ( hAPP_l1987619678r_bool(fmb_fun_li887890578r_bool_1,fmb_list_ty_2) = fmb_fun_Pr827765831r_bool_2 )
    & ( hAPP_l1987619678r_bool(fmb_fun_li887890578r_bool_2,fmb_list_ty_1) = fmb_fun_Pr827765831r_bool_2 )
    & ( hAPP_l1987619678r_bool(fmb_fun_li887890578r_bool_2,fmb_list_ty_2) = fmb_fun_Pr827765831r_bool_2 ) ) ).

tff(declare_hAPP_l732421366t_char,type,
    hAPP_l732421366t_char: ( fun_li430210730t_char * list_val ) > list_exp_list_char ).

tff(function_hAPP_l732421366t_char,axiom,
    ( ( hAPP_l732421366t_char(fmb_fun_li430210730t_char_1,fmb_list_val_1) = fmb_list_exp_list_char_1 )
    & ( hAPP_l732421366t_char(fmb_fun_li430210730t_char_2,fmb_list_val_1) = fmb_list_exp_list_char_1 ) ) ).

tff(declare_hAPP_l922645359t_char,type,
    hAPP_l922645359t_char: ( fun_li1120813347t_char * list_val ) > list_list_char ).

tff(function_hAPP_l922645359t_char,axiom,
    ( ( hAPP_l922645359t_char(fmb_fun_li1120813347t_char_1,fmb_list_val_1) = fmb_list_list_char_1 )
    & ( hAPP_l922645359t_char(fmb_fun_li1120813347t_char_2,fmb_list_val_1) = fmb_list_list_char_1 ) ) ).

tff(declare_hAPP_l2006940821ion_ty,type,
    hAPP_l2006940821ion_ty: ( fun_li1144067913ion_ty * list_val ) > list_option_ty ).

tff(function_hAPP_l2006940821ion_ty,axiom,
    ( ( hAPP_l2006940821ion_ty(fmb_fun_li1144067913ion_ty_1,fmb_list_val_1) = fmb_list_option_ty_1 )
    & ( hAPP_l2006940821ion_ty(fmb_fun_li1144067913ion_ty_2,fmb_list_val_1) = fmb_list_option_ty_1 ) ) ).

tff(declare_hAPP_l761459294on_val,type,
    hAPP_l761459294on_val: ( fun_li1091306514on_val * list_val ) > list_option_val ).

tff(function_hAPP_l761459294on_val,axiom,
    ( ( hAPP_l761459294on_val(fmb_fun_li1091306514on_val_1,fmb_list_val_1) = fmb_list_option_val_2 )
    & ( hAPP_l761459294on_val(fmb_fun_li1091306514on_val_2,fmb_list_val_1) = fmb_list_option_val_2 ) ) ).

tff(declare_hAPP_l1085267864ist_ty,type,
    hAPP_l1085267864ist_ty: ( fun_list_val_list_ty * list_val ) > list_ty ).

tff(function_hAPP_l1085267864ist_ty,axiom,
    ( ( hAPP_l1085267864ist_ty(fmb_fun_list_val_list_ty_1,fmb_list_val_1) = fmb_list_ty_1 )
    & ( hAPP_l1085267864ist_ty(fmb_fun_list_val_list_ty_2,fmb_list_val_1) = fmb_list_ty_1 ) ) ).

tff(declare_hAPP_l273806049st_val,type,
    hAPP_l273806049st_val: ( fun_li1707879747st_val * list_val ) > list_val ).

tff(function_hAPP_l273806049st_val,axiom,
    ( ( hAPP_l273806049st_val(fmb_fun_li1707879747st_val_1,fmb_list_val_1) = fmb_list_val_1 )
    & ( hAPP_l273806049st_val(fmb_fun_li1707879747st_val_2,fmb_list_val_1) = fmb_list_val_1 ) ) ).

tff(declare_hAPP_l382831894on_val,type,
    hAPP_l382831894on_val: ( fun_li1659202122on_val * list_val ) > list_P1439941640on_val ).

tff(function_hAPP_l382831894on_val,axiom,
    ( ( hAPP_l382831894on_val(fmb_fun_li1659202122on_val_1,fmb_list_val_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l382831894on_val(fmb_fun_li1659202122on_val_2,fmb_list_val_1) = fmb_list_P1439941640on_val_2 ) ) ).

tff(declare_hAPP_l1062423959r_bool,type,
    hAPP_l1062423959r_bool: ( fun_li826105035r_bool * list_val ) > fun_ex736065929r_bool ).

tff(function_hAPP_l1062423959r_bool,axiom,
    ( ( hAPP_l1062423959r_bool(fmb_fun_li826105035r_bool_1,fmb_list_val_1) = fmb_fun_ex736065929r_bool_2 )
    & ( hAPP_l1062423959r_bool(fmb_fun_li826105035r_bool_2,fmb_list_val_1) = fmb_fun_ex736065929r_bool_2 ) ) ).

tff(declare_hAPP_l1695428693on_val,type,
    hAPP_l1695428693on_val: ( fun_li1479469629on_val * list_P1439941640on_val ) > list_P1439941640on_val ).

tff(function_hAPP_l1695428693on_val,axiom,
    ( ( hAPP_l1695428693on_val(fmb_fun_li1479469629on_val_1,fmb_list_P1439941640on_val_1) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1695428693on_val(fmb_fun_li1479469629on_val_1,fmb_list_P1439941640on_val_2) = fmb_list_P1439941640on_val_2 )
    & ( hAPP_l1695428693on_val(fmb_fun_li1479469629on_val_2,fmb_list_P1439941640on_val_1) = fmb_list_P1439941640on_val_1 )
    & ( hAPP_l1695428693on_val(fmb_fun_li1479469629on_val_2,fmb_list_P1439941640on_val_2) = fmb_list_P1439941640on_val_2 ) ) ).

tff(declare_hAPP_n546249108on_val,type,
    hAPP_n546249108on_val: ( fun_na939144002on_val * nat ) > option1479284511on_val ).

tff(function_hAPP_n546249108on_val,axiom,
    hAPP_n546249108on_val(fmb_fun_na939144002on_val_1,fmb_nat_1) = fmb_option1479284511on_val_2 ).

tff(declare_hAPP_option_ty_ty,type,
    hAPP_option_ty_ty: ( fun_option_ty_ty * option_ty ) > ty ).

tff(function_hAPP_option_ty_ty,axiom,
    ( ( hAPP_option_ty_ty(fmb_fun_option_ty_ty_1,fmb_option_ty_1) = fmb_ty_2 )
    & ( hAPP_option_ty_ty(fmb_fun_option_ty_ty_1,fmb_option_ty_2) = fmb_ty_1 )
    & ( hAPP_option_ty_ty(fmb_fun_option_ty_ty_2,fmb_option_ty_1) = fmb_ty_2 )
    & ( hAPP_option_ty_ty(fmb_fun_option_ty_ty_2,fmb_option_ty_2) = fmb_ty_1 ) ) ).

tff(declare_hAPP_option_val_val,type,
    hAPP_option_val_val: ( fun_option_val_val * option_val ) > val ).

tff(function_hAPP_option_val_val,axiom,
    ( ( hAPP_option_val_val(fmb_fun_option_val_val_1,fmb_option_val_1) = fmb_val_1 )
    & ( hAPP_option_val_val(fmb_fun_option_val_val_1,fmb_option_val_2) = fmb_val_2 )
    & ( hAPP_option_val_val(fmb_fun_option_val_val_2,fmb_option_val_1) = fmb_val_1 )
    & ( hAPP_option_val_val(fmb_fun_option_val_val_2,fmb_option_val_2) = fmb_val_2 ) ) ).

tff(declare_hAPP_o1977518472on_val,type,
    hAPP_o1977518472on_val: ( fun_op498348476on_val * option1479284511on_val ) > produc639455274on_val ).

tff(function_hAPP_o1977518472on_val,axiom,
    ( ( hAPP_o1977518472on_val(fmb_fun_op498348476on_val_1,fmb_option1479284511on_val_1) = fmb_produc639455274on_val_2 )
    & ( hAPP_o1977518472on_val(fmb_fun_op498348476on_val_1,fmb_option1479284511on_val_2) = fmb_produc639455274on_val_1 )
    & ( hAPP_o1977518472on_val(fmb_fun_op498348476on_val_2,fmb_option1479284511on_val_1) = fmb_produc639455274on_val_2 )
    & ( hAPP_o1977518472on_val(fmb_fun_op498348476on_val_2,fmb_option1479284511on_val_2) = fmb_produc639455274on_val_1 ) ) ).

tff(declare_hAPP_ty_bool,type,
    hAPP_ty_bool: ( fun_ty_bool * ty ) > bool ).

tff(function_hAPP_ty_bool,axiom,
    ( ( hAPP_ty_bool(fmb_fun_ty_bool_1,fmb_ty_1) = fmb_bool_2 )
    & ( hAPP_ty_bool(fmb_fun_ty_bool_1,fmb_ty_2) = fmb_bool_1 )
    & ( hAPP_ty_bool(fmb_fun_ty_bool_2,fmb_ty_1) = fmb_bool_1 )
    & ( hAPP_ty_bool(fmb_fun_ty_bool_2,fmb_ty_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_ty_option_ty,type,
    hAPP_ty_option_ty: ( fun_ty_option_ty * ty ) > option_ty ).

tff(function_hAPP_ty_option_ty,axiom,
    ( ( hAPP_ty_option_ty(fmb_fun_ty_option_ty_1,fmb_ty_1) = fmb_option_ty_2 )
    & ( hAPP_ty_option_ty(fmb_fun_ty_option_ty_1,fmb_ty_2) = fmb_option_ty_1 )
    & ( hAPP_ty_option_ty(fmb_fun_ty_option_ty_2,fmb_ty_1) = fmb_option_ty_2 )
    & ( hAPP_ty_option_ty(fmb_fun_ty_option_ty_2,fmb_ty_2) = fmb_option_ty_1 ) ) ).

tff(declare_hAPP_ty_fun_ty_bool,type,
    hAPP_ty_fun_ty_bool: ( fun_ty_fun_ty_bool * ty ) > fun_ty_bool ).

tff(function_hAPP_ty_fun_ty_bool,axiom,
    ( ( hAPP_ty_fun_ty_bool(fmb_fun_ty_fun_ty_bool_1,fmb_ty_1) = fmb_fun_ty_bool_1 )
    & ( hAPP_ty_fun_ty_bool(fmb_fun_ty_fun_ty_bool_1,fmb_ty_2) = fmb_fun_ty_bool_2 )
    & ( hAPP_ty_fun_ty_bool(fmb_fun_ty_fun_ty_bool_2,fmb_ty_1) = fmb_fun_ty_bool_1 )
    & ( hAPP_ty_fun_ty_bool(fmb_fun_ty_fun_ty_bool_2,fmb_ty_2) = fmb_fun_ty_bool_2 ) ) ).

tff(declare_hAPP_v834067052t_char,type,
    hAPP_v834067052t_char: ( fun_va223928858t_char * val ) > exp_list_char ).

tff(function_hAPP_v834067052t_char,axiom,
    ( ( hAPP_v834067052t_char(fmb_fun_va223928858t_char_1,fmb_val_1) = fmb_exp_list_char_1 )
    & ( hAPP_v834067052t_char(fmb_fun_va223928858t_char_1,fmb_val_2) = fmb_exp_list_char_1 )
    & ( hAPP_v834067052t_char(fmb_fun_va223928858t_char_2,fmb_val_1) = fmb_exp_list_char_1 )
    & ( hAPP_v834067052t_char(fmb_fun_va223928858t_char_2,fmb_val_2) = fmb_exp_list_char_1 ) ) ).

tff(declare_hAPP_val_option_ty,type,
    hAPP_val_option_ty: ( fun_val_option_ty * val ) > option_ty ).

tff(function_hAPP_val_option_ty,axiom,
    ( ( hAPP_val_option_ty(fmb_fun_val_option_ty_1,fmb_val_1) = fmb_option_ty_1 )
    & ( hAPP_val_option_ty(fmb_fun_val_option_ty_1,fmb_val_2) = fmb_option_ty_1 )
    & ( hAPP_val_option_ty(fmb_fun_val_option_ty_2,fmb_val_1) = fmb_option_ty_2 )
    & ( hAPP_val_option_ty(fmb_fun_val_option_ty_2,fmb_val_2) = fmb_option_ty_1 ) ) ).

tff(declare_hAPP_val_option_val,type,
    hAPP_val_option_val: ( fun_val_option_val * val ) > option_val ).

tff(function_hAPP_val_option_val,axiom,
    ( ( hAPP_val_option_val(fmb_fun_val_option_val_1,fmb_val_1) = fmb_option_val_1 )
    & ( hAPP_val_option_val(fmb_fun_val_option_val_1,fmb_val_2) = fmb_option_val_2 )
    & ( hAPP_val_option_val(fmb_fun_val_option_val_2,fmb_val_1) = fmb_option_val_1 )
    & ( hAPP_val_option_val(fmb_fun_val_option_val_2,fmb_val_2) = fmb_option_val_2 ) ) ).

tff(declare_hAPP_val_fun_ty_bool,type,
    hAPP_val_fun_ty_bool: ( fun_val_fun_ty_bool * val ) > fun_ty_bool ).

tff(function_hAPP_val_fun_ty_bool,axiom,
    ( ( hAPP_val_fun_ty_bool(fmb_fun_val_fun_ty_bool_1,fmb_val_1) = fmb_fun_ty_bool_2 )
    & ( hAPP_val_fun_ty_bool(fmb_fun_val_fun_ty_bool_1,fmb_val_2) = fmb_fun_ty_bool_2 )
    & ( hAPP_val_fun_ty_bool(fmb_fun_val_fun_ty_bool_2,fmb_val_1) = fmb_fun_ty_bool_2 )
    & ( hAPP_val_fun_ty_bool(fmb_fun_val_fun_ty_bool_2,fmb_val_2) = fmb_fun_ty_bool_2 ) ) ).

tff(declare_hAPP_f1033709212l_bool,type,
    hAPP_f1033709212l_bool: ( fun_fu1693644106l_bool * fun_li1432931796on_val ) > bool ).

tff(function_hAPP_f1033709212l_bool,axiom,
    ( ( hAPP_f1033709212l_bool(fmb_fun_fu1693644106l_bool_1,fmb_fun_li1432931796on_val_1) = fmb_bool_2 )
    & ( hAPP_f1033709212l_bool(fmb_fun_fu1693644106l_bool_2,fmb_fun_li1432931796on_val_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_f1175813647l_bool,type,
    hAPP_f1175813647l_bool: ( fun_fu100249073l_bool * fun_na939144002on_val ) > fun_fu1693644106l_bool ).

tff(function_hAPP_f1175813647l_bool,axiom,
    ( ( hAPP_f1175813647l_bool(fmb_fun_fu100249073l_bool_1,fmb_fun_na939144002on_val_1) = fmb_fun_fu1693644106l_bool_2 )
    & ( hAPP_f1175813647l_bool(fmb_fun_fu100249073l_bool_2,fmb_fun_na939144002on_val_1) = fmb_fun_fu1693644106l_bool_2 ) ) ).

tff(declare_hAPP_f1715346603l_bool,type,
    hAPP_f1715346603l_bool: ( fun_fu177229913l_bool * fun_Pr806764899on_val ) > bool ).

tff(function_hAPP_f1715346603l_bool,axiom,
    ( ( hAPP_f1715346603l_bool(fmb_fun_fu177229913l_bool_1,fmb_fun_Pr806764899on_val_1) = fmb_bool_2 )
    & ( hAPP_f1715346603l_bool(fmb_fun_fu177229913l_bool_1,fmb_fun_Pr806764899on_val_2) = fmb_bool_2 )
    & ( hAPP_f1715346603l_bool(fmb_fun_fu177229913l_bool_2,fmb_fun_Pr806764899on_val_1) = fmb_bool_2 )
    & ( hAPP_f1715346603l_bool(fmb_fun_fu177229913l_bool_2,fmb_fun_Pr806764899on_val_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P1708370145l_bool,type,
    hAPP_P1708370145l_bool: ( fun_Pr680585871l_bool * produc124828825on_val ) > bool ).

tff(function_hAPP_P1708370145l_bool,axiom,
    ( ( hAPP_P1708370145l_bool(fmb_fun_Pr680585871l_bool_1,fmb_produc124828825on_val_1) = fmb_bool_2 )
    & ( hAPP_P1708370145l_bool(fmb_fun_Pr680585871l_bool_2,fmb_produc124828825on_val_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P1116729363l_bool,type,
    hAPP_P1116729363l_bool: ( fun_Pr633696065l_bool * produc124828825on_val ) > fun_Pr680585871l_bool ).

tff(function_hAPP_P1116729363l_bool,axiom,
    ( ( hAPP_P1116729363l_bool(fmb_fun_Pr633696065l_bool_1,fmb_produc124828825on_val_1) = fmb_fun_Pr680585871l_bool_2 )
    & ( hAPP_P1116729363l_bool(fmb_fun_Pr633696065l_bool_2,fmb_produc124828825on_val_1) = fmb_fun_Pr680585871l_bool_2 ) ) ).

tff(declare_hAPP_P92196306r_bool,type,
    hAPP_P92196306r_bool: ( fun_Pr227936640r_bool * produc1285161482t_char ) > bool ).

tff(function_hAPP_P92196306r_bool,axiom,
    ( ( hAPP_P92196306r_bool(fmb_fun_Pr227936640r_bool_1,fmb_produc1285161482t_char_1) = fmb_bool_2 )
    & ( hAPP_P92196306r_bool(fmb_fun_Pr227936640r_bool_1,fmb_produc1285161482t_char_2) = fmb_bool_2 )
    & ( hAPP_P92196306r_bool(fmb_fun_Pr227936640r_bool_2,fmb_produc1285161482t_char_1) = fmb_bool_2 )
    & ( hAPP_P92196306r_bool(fmb_fun_Pr227936640r_bool_2,fmb_produc1285161482t_char_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P1235399154l_bool,type,
    hAPP_P1235399154l_bool: ( fun_Pr315804320l_bool * produc639455274on_val ) > bool ).

tff(function_hAPP_P1235399154l_bool,axiom,
    ( ( hAPP_P1235399154l_bool(fmb_fun_Pr315804320l_bool_1,fmb_produc639455274on_val_1) = fmb_bool_2 )
    & ( hAPP_P1235399154l_bool(fmb_fun_Pr315804320l_bool_1,fmb_produc639455274on_val_2) = fmb_bool_2 )
    & ( hAPP_P1235399154l_bool(fmb_fun_Pr315804320l_bool_2,fmb_produc639455274on_val_1) = fmb_bool_2 )
    & ( hAPP_P1235399154l_bool(fmb_fun_Pr315804320l_bool_2,fmb_produc639455274on_val_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P1510515380on_val,type,
    hAPP_P1510515380on_val: ( fun_Pr357631842on_val * produc639455274on_val ) > option1479284511on_val ).

tff(function_hAPP_P1510515380on_val,axiom,
    ( ( hAPP_P1510515380on_val(fmb_fun_Pr357631842on_val_1,fmb_produc639455274on_val_1) = fmb_option1479284511on_val_2 )
    & ( hAPP_P1510515380on_val(fmb_fun_Pr357631842on_val_1,fmb_produc639455274on_val_2) = fmb_option1479284511on_val_1 )
    & ( hAPP_P1510515380on_val(fmb_fun_Pr357631842on_val_2,fmb_produc639455274on_val_1) = fmb_option1479284511on_val_2 )
    & ( hAPP_P1510515380on_val(fmb_fun_Pr357631842on_val_2,fmb_produc639455274on_val_2) = fmb_option1479284511on_val_1 ) ) ).

tff(declare_hAPP_P1907982426r_bool,type,
    hAPP_P1907982426r_bool: ( fun_Pr46158268r_bool * produc220283002t_char ) > bool ).

tff(function_hAPP_P1907982426r_bool,axiom,
    ( ( hAPP_P1907982426r_bool(fmb_fun_Pr46158268r_bool_1,fmb_produc220283002t_char_1) = fmb_bool_2 )
    & ( hAPP_P1907982426r_bool(fmb_fun_Pr46158268r_bool_1,fmb_produc220283002t_char_2) = fmb_bool_2 )
    & ( hAPP_P1907982426r_bool(fmb_fun_Pr46158268r_bool_2,fmb_produc220283002t_char_1) = fmb_bool_2 )
    & ( hAPP_P1907982426r_bool(fmb_fun_Pr46158268r_bool_2,fmb_produc220283002t_char_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P2118621157r_bool,type,
    hAPP_P2118621157r_bool: ( fun_Pr827765831r_bool * produc662261637t_char ) > bool ).

tff(function_hAPP_P2118621157r_bool,axiom,
    ( ( hAPP_P2118621157r_bool(fmb_fun_Pr827765831r_bool_1,fmb_produc662261637t_char_1) = fmb_bool_2 )
    & ( hAPP_P2118621157r_bool(fmb_fun_Pr827765831r_bool_2,fmb_produc662261637t_char_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P159683425l_bool,type,
    hAPP_P159683425l_bool: ( fun_Pr1696029455l_bool * produc12694297on_val ) > bool ).

tff(function_hAPP_P159683425l_bool,axiom,
    ( ( hAPP_P159683425l_bool(fmb_fun_Pr1696029455l_bool_1,fmb_produc12694297on_val_1) = fmb_bool_2 )
    & ( hAPP_P159683425l_bool(fmb_fun_Pr1696029455l_bool_2,fmb_produc12694297on_val_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P282169671l_bool,type,
    hAPP_P282169671l_bool: ( fun_Pr691271849l_bool * produc1102272487on_val ) > bool ).

tff(function_hAPP_P282169671l_bool,axiom,
    ( ( hAPP_P282169671l_bool(fmb_fun_Pr691271849l_bool_1,fmb_produc1102272487on_val_1) = fmb_bool_2 )
    & ( hAPP_P282169671l_bool(fmb_fun_Pr691271849l_bool_2,fmb_produc1102272487on_val_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_P918220497on_val,type,
    hAPP_P918220497on_val: ( fun_Pr12181427on_val * produc1102272487on_val ) > produc1102272487on_val ).

tff(function_hAPP_P918220497on_val,axiom,
    ( ( hAPP_P918220497on_val(fmb_fun_Pr12181427on_val_1,fmb_produc1102272487on_val_1) = fmb_produc1102272487on_val_1 )
    & ( hAPP_P918220497on_val(fmb_fun_Pr12181427on_val_2,fmb_produc1102272487on_val_1) = fmb_produc1102272487on_val_1 ) ) ).

tff(declare_member_exp_list_char,type,
    member_exp_list_char: ( exp_list_char * fun_ex736065929r_bool ) > bool ).

tff(function_member_exp_list_char,axiom,
    ( ( member_exp_list_char(fmb_exp_list_char_1,fmb_fun_ex736065929r_bool_1) = fmb_bool_2 )
    & ( member_exp_list_char(fmb_exp_list_char_1,fmb_fun_ex736065929r_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member_list_char,type,
    member_list_char: ( list_char * fun_list_char_bool ) > bool ).

tff(function_member_list_char,axiom,
    ( ( member_list_char(fmb_list_char_1,fmb_fun_list_char_bool_1) = fmb_bool_2 )
    & ( member_list_char(fmb_list_char_1,fmb_fun_list_char_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member_option_ty,type,
    member_option_ty: ( option_ty * fun_option_ty_bool ) > bool ).

tff(function_member_option_ty,axiom,
    ( ( member_option_ty(fmb_option_ty_1,fmb_fun_option_ty_bool_1) = fmb_bool_2 )
    & ( member_option_ty(fmb_option_ty_1,fmb_fun_option_ty_bool_2) = fmb_bool_2 )
    & ( member_option_ty(fmb_option_ty_2,fmb_fun_option_ty_bool_1) = fmb_bool_2 )
    & ( member_option_ty(fmb_option_ty_2,fmb_fun_option_ty_bool_2) = fmb_bool_1 ) ) ).

tff(declare_member_ty,type,
    member_ty: ( ty * fun_ty_bool ) > bool ).

tff(function_member_ty,axiom,
    ( ( member_ty(fmb_ty_1,fmb_fun_ty_bool_1) = fmb_bool_2 )
    & ( member_ty(fmb_ty_1,fmb_fun_ty_bool_2) = fmb_bool_2 )
    & ( member_ty(fmb_ty_2,fmb_fun_ty_bool_1) = fmb_bool_2 )
    & ( member_ty(fmb_ty_2,fmb_fun_ty_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member_val,type,
    member_val: ( val * fun_val_bool ) > bool ).

tff(function_member_val,axiom,
    ( ( member_val(fmb_val_1,fmb_fun_val_bool_1) = fmb_bool_2 )
    & ( member_val(fmb_val_1,fmb_fun_val_bool_2) = fmb_bool_1 )
    & ( member_val(fmb_val_2,fmb_fun_val_bool_1) = fmb_bool_2 )
    & ( member_val(fmb_val_2,fmb_fun_val_bool_2) = fmb_bool_1 ) ) ).

tff(declare_member773094996on_val,type,
    member773094996on_val: ( produc1102272487on_val * fun_Pr691271849l_bool ) > bool ).

tff(function_member773094996on_val,axiom,
    ( ( member773094996on_val(fmb_produc1102272487on_val_1,fmb_fun_Pr691271849l_bool_1) = fmb_bool_2 )
    & ( member773094996on_val(fmb_produc1102272487on_val_1,fmb_fun_Pr691271849l_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member1420286996t_char,type,
    member1420286996t_char: ( produc349695911t_char * fun_Pr1895638121r_bool ) > bool ).

tff(function_member1420286996t_char,axiom,
    ( ( member1420286996t_char(fmb_produc349695911t_char_1,fmb_fun_Pr1895638121r_bool_1) = fmb_bool_2 )
    & ( member1420286996t_char(fmb_produc349695911t_char_1,fmb_fun_Pr1895638121r_bool_2) = fmb_bool_2 )
    & ( member1420286996t_char(fmb_produc349695911t_char_2,fmb_fun_Pr1895638121r_bool_1) = fmb_bool_2 )
    & ( member1420286996t_char(fmb_produc349695911t_char_2,fmb_fun_Pr1895638121r_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member1322055188on_val,type,
    member1322055188on_val: ( produc87279271on_val * fun_Pr235369833l_bool ) > bool ).

tff(function_member1322055188on_val,axiom,
    ( ( member1322055188on_val(fmb_produc87279271on_val_1,fmb_fun_Pr235369833l_bool_1) = fmb_bool_2 )
    & ( member1322055188on_val(fmb_produc87279271on_val_1,fmb_fun_Pr235369833l_bool_2) = fmb_bool_2 )
    & ( member1322055188on_val(fmb_produc87279271on_val_2,fmb_fun_Pr235369833l_bool_1) = fmb_bool_2 )
    & ( member1322055188on_val(fmb_produc87279271on_val_2,fmb_fun_Pr235369833l_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member125098544t_char,type,
    member125098544t_char: ( produc1406897475t_char * fun_Pr1728267013r_bool ) > bool ).

tff(function_member125098544t_char,axiom,
    ( ( member125098544t_char(fmb_produc1406897475t_char_1,fmb_fun_Pr1728267013r_bool_1) = fmb_bool_2 )
    & ( member125098544t_char(fmb_produc1406897475t_char_1,fmb_fun_Pr1728267013r_bool_2) = fmb_bool_2 )
    & ( member125098544t_char(fmb_produc1406897475t_char_2,fmb_fun_Pr1728267013r_bool_1) = fmb_bool_2 )
    & ( member125098544t_char(fmb_produc1406897475t_char_2,fmb_fun_Pr1728267013r_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member1161907014t_char,type,
    member1161907014t_char: ( produc1826280281t_char * fun_Pr1890037787r_bool ) > bool ).

tff(function_member1161907014t_char,axiom,
    ( ( member1161907014t_char(fmb_produc1826280281t_char_1,fmb_fun_Pr1890037787r_bool_1) = fmb_bool_2 )
    & ( member1161907014t_char(fmb_produc1826280281t_char_1,fmb_fun_Pr1890037787r_bool_2) = fmb_bool_2 )
    & ( member1161907014t_char(fmb_produc1826280281t_char_2,fmb_fun_Pr1890037787r_bool_1) = fmb_bool_2 )
    & ( member1161907014t_char(fmb_produc1826280281t_char_2,fmb_fun_Pr1890037787r_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member563141460on_val,type,
    member563141460on_val: ( produc409205479on_val * fun_Pr693020585l_bool ) > bool ).

tff(function_member563141460on_val,axiom,
    ( ( member563141460on_val(fmb_produc409205479on_val_1,fmb_fun_Pr693020585l_bool_1) = fmb_bool_2 )
    & ( member563141460on_val(fmb_produc409205479on_val_1,fmb_fun_Pr693020585l_bool_2) = fmb_bool_2 )
    & ( member563141460on_val(fmb_produc409205479on_val_2,fmb_fun_Pr693020585l_bool_1) = fmb_bool_2 )
    & ( member563141460on_val(fmb_produc409205479on_val_2,fmb_fun_Pr693020585l_bool_2) = fmb_bool_2 ) ) ).

tff(declare_member808015754on_val,type,
    member808015754on_val: ( produc231486621on_val * fun_Pr903661919l_bool ) > bool ).

tff(function_member808015754on_val,axiom,
    ( ( member808015754on_val(fmb_produc231486621on_val_1,fmb_fun_Pr903661919l_bool_1) = fmb_bool_2 )
    & ( member808015754on_val(fmb_produc231486621on_val_1,fmb_fun_Pr903661919l_bool_2) = fmb_bool_2 )
    & ( member808015754on_val(fmb_produc231486621on_val_2,fmb_fun_Pr903661919l_bool_1) = fmb_bool_2 )
    & ( member808015754on_val(fmb_produc231486621on_val_2,fmb_fun_Pr903661919l_bool_2) = fmb_bool_2 ) ) ).

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

tff(predicate_hBOOL,axiom,
    ( ~ hBOOL(fmb_bool_1)
    & hBOOL(fmb_bool_2) ) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWW476_1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16  % Computer : n014.cluster.edu
% 0.10/0.16  % Model    : x86_64 x86_64
% 0.10/0.16  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16  % Memory   : 8046.5625MB
% 0.10/0.16  % OS       : Linux 6.8.0-71-generic
% 0.10/0.16  % CPULimit : 300
% 0.10/0.16  % WCLimit  : 300
% 0.10/0.16  % DateTime : Mon Sep 28 14:10:16 UTC 2026
% 0.10/0.17  % CPUTime  : 
% 0.10/0.17  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19  Running first-order model finding
% 0.10/0.19  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.17/0.43  % (1792056)Will run a generic schedule for satisfiability detection.
% 1.17/0.43  % (1792064)dis+10_1_sil=32000:sp=arity:random_seed=676165317:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.17/0.43  % (1792061)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1324666640_2999 on theBenchmark for (2999ds/0Mi)
% 1.17/0.43  % (1792063)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2200968930:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.17/0.43  % (1792065)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=603376765:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.17/0.43  % (1792066)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3436427695:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.17/0.43  % (1792067)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2049890077:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.17/0.43  % (1792062)% WARNING: option uhcvi not known.
% 1.17/0.43  % (1792062)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2199389504:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.17/0.43  % (1792064)Instruction limit reached! 
% 1.17/0.43  % (1792064)------------------------------
% 1.17/0.43  % (1792064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792064)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792064)Termination reason: Instruction limit
% 1.17/0.43  % (1792064)Termination phase: Saturation
% 1.17/0.43  % (1792064)Time elapsed: 0.032 s
% 1.17/0.43  % (1792064)Peak memory usage: 13 MB
% 1.17/0.43  % (1792064)Instructions burned: 103 (million)
% 1.17/0.43  % (1792075)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4181916542:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.17/0.43  % (1792065)Instruction limit reached! 
% 1.17/0.43  % (1792065)------------------------------
% 1.17/0.43  % (1792065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792065)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792065)Termination reason: Instruction limit
% 1.17/0.43  % (1792065)Termination phase: Saturation
% 1.17/0.43  % (1792065)Time elapsed: 0.065 s
% 1.17/0.43  % (1792065)Peak memory usage: 13 MB
% 1.17/0.43  % (1792065)Instructions burned: 116 (million)
% 1.17/0.43  % (1792066)Instruction limit reached! 
% 1.17/0.43  % (1792066)------------------------------
% 1.17/0.43  % (1792066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792066)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792066)Termination reason: Instruction limit
% 1.17/0.43  % (1792066)Termination phase: Saturation
% 1.17/0.43  % (1792066)Time elapsed: 0.076 s
% 1.17/0.43  % (1792066)Peak memory usage: 13 MB
% 1.17/0.43  % (1792066)Instructions burned: 131 (million)
% 1.17/0.43  % (1792077)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=592751881:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.17/0.43  % (1792067)Instruction limit reached! 
% 1.17/0.43  % (1792067)------------------------------
% 1.17/0.43  % (1792067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792067)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792067)Termination reason: Instruction limit
% 1.17/0.43  % (1792067)Termination phase: Saturation
% 1.17/0.43  % (1792067)Time elapsed: 0.092 s
% 1.17/0.43  % (1792067)Peak memory usage: 14 MB
% 1.17/0.43  % (1792067)Instructions burned: 160 (million)
% 1.17/0.43  % (1792078)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1873421877:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.17/0.43  % TRYING [1]
% 1.17/0.43  % TRYING [2]
% 1.17/0.43  % (1792080)ott-21_1_sil=16000:fs=off:random_seed=3796863247:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.17/0.43  % Finite Model Found!
% 1.17/0.43  % SZS status CounterSatisfiable for theBenchmark
% 1.17/0.43  % (1792077)Instruction limit reached! 
% 1.17/0.43  % (1792077)------------------------------
% 1.17/0.43  % (1792077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792077)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792077)Termination reason: Instruction limit
% 1.17/0.43  % (1792077)Termination phase: Saturation
% 1.17/0.43  % (1792077)Time elapsed: 0.081 s
% 1.17/0.43  % (1792077)Peak memory usage: 14 MB
% 1.17/0.43  % (1792077)Instructions burned: 132 (million)
% 1.17/0.43  % (1792075) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1792056-1792075"...
% 1.17/0.43  % (1792075)...printing done.
% 1.17/0.43  % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.17/0.43  % (1792075)------------------------------
% 1.17/0.43  % (1792075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.17/0.43  % (1792075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.17/0.43  % (1792075)CaDiCaL version: 2.1.3
% 1.17/0.43  % (1792075)Termination reason: Satisfiable
% 1.17/0.43  % (1792075)Time elapsed: 0.137 s
% 1.17/0.43  % (1792075)Peak memory usage: 28 MB
% 1.17/0.43  % (1792075)Instructions burned: 585 (million)
% 1.17/0.43  % (1792056)Success in time 0.229 s
% 1.17/0.43  % Vampire exiting
%------------------------------------------------------------------------------