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

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

% Computer : n018.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:07 PM UTC 2026

% Result   : CounterSatisfiable 4.44s 1.01s
% Output   : FiniteModel 4.44s
% 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_com,type,
    com: $tType ).

tff(declare_com1,type,
    fmb_com_1: com ).

tff(finite_domain_com,axiom,
    ! [X: com] : ( X = fmb_com_1 ) ).

tff(declare_pname,type,
    pname: $tType ).

tff(declare_pname1,type,
    fmb_pname_1: pname ).

tff(finite_domain_pname,axiom,
    ! [X: pname] : ( X = fmb_pname_1 ) ).

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

tff(declare_state1,type,
    fmb_state_1: state ).

tff(finite_domain_state,axiom,
    ! [X: state] : ( X = fmb_state_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_hoare_1927711152iple_a,type,
    hoare_1927711152iple_a: $tType ).

tff(declare_hoare_1927711152iple_a1,type,
    fmb_hoare_1927711152iple_a_1: hoare_1927711152iple_a ).

tff(finite_domain_hoare_1927711152iple_a,axiom,
    ! [X: hoare_1927711152iple_a] : ( X = fmb_hoare_1927711152iple_a_1 ) ).

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

tff(declare_nat1,type,
    fmb_nat_1: nat ).

tff(declare_nat2,type,
    fmb_nat_2: nat ).

tff(declare_nat3,type,
    fmb_nat_3: nat ).

tff(declare_nat4,type,
    fmb_nat_4: nat ).

tff(finite_domain_nat,axiom,
    ! [X: nat] :
      ( ( X = fmb_nat_1 )
      | ( X = fmb_nat_2 )
      | ( X = fmb_nat_3 )
      | ( X = fmb_nat_4 ) ) ).

tff(distinct_domain_nat,axiom,
    ( ( fmb_nat_1 != fmb_nat_2 )
    & ( fmb_nat_1 != fmb_nat_3 )
    & ( fmb_nat_1 != fmb_nat_4 )
    & ( fmb_nat_2 != fmb_nat_3 )
    & ( fmb_nat_2 != fmb_nat_4 )
    & ( fmb_nat_3 != fmb_nat_4 ) ) ).

tff(declare_option_com,type,
    option_com: $tType ).

tff(declare_option_com1,type,
    fmb_option_com_1: option_com ).

tff(declare_option_com2,type,
    fmb_option_com_2: option_com ).

tff(declare_option_com3,type,
    fmb_option_com_3: option_com ).

tff(declare_option_com4,type,
    fmb_option_com_4: option_com ).

tff(finite_domain_option_com,axiom,
    ! [X: option_com] :
      ( ( X = fmb_option_com_1 )
      | ( X = fmb_option_com_2 )
      | ( X = fmb_option_com_3 )
      | ( X = fmb_option_com_4 ) ) ).

tff(distinct_domain_option_com,axiom,
    ( ( fmb_option_com_1 != fmb_option_com_2 )
    & ( fmb_option_com_1 != fmb_option_com_3 )
    & ( fmb_option_com_1 != fmb_option_com_4 )
    & ( fmb_option_com_2 != fmb_option_com_3 )
    & ( fmb_option_com_2 != fmb_option_com_4 )
    & ( fmb_option_com_3 != fmb_option_com_4 ) ) ).

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

tff(declare_fun_a_fun_state_bool1,type,
    fmb_fun_a_fun_state_bool_1: fun_a_fun_state_bool ).

tff(finite_domain_fun_a_fun_state_bool,axiom,
    ! [X: fun_a_fun_state_bool] : ( X = fmb_fun_a_fun_state_bool_1 ) ).

tff(declare_fun_co1155576772iple_a,type,
    fun_co1155576772iple_a: $tType ).

tff(declare_fun_co1155576772iple_a1,type,
    fmb_fun_co1155576772iple_a_1: fun_co1155576772iple_a ).

tff(declare_fun_co1155576772iple_a2,type,
    fmb_fun_co1155576772iple_a_2: fun_co1155576772iple_a ).

tff(declare_fun_co1155576772iple_a3,type,
    fmb_fun_co1155576772iple_a_3: fun_co1155576772iple_a ).

tff(declare_fun_co1155576772iple_a4,type,
    fmb_fun_co1155576772iple_a_4: fun_co1155576772iple_a ).

tff(finite_domain_fun_co1155576772iple_a,axiom,
    ! [X: fun_co1155576772iple_a] :
      ( ( X = fmb_fun_co1155576772iple_a_1 )
      | ( X = fmb_fun_co1155576772iple_a_2 )
      | ( X = fmb_fun_co1155576772iple_a_3 )
      | ( X = fmb_fun_co1155576772iple_a_4 ) ) ).

tff(distinct_domain_fun_co1155576772iple_a,axiom,
    ( ( fmb_fun_co1155576772iple_a_1 != fmb_fun_co1155576772iple_a_2 )
    & ( fmb_fun_co1155576772iple_a_1 != fmb_fun_co1155576772iple_a_3 )
    & ( fmb_fun_co1155576772iple_a_1 != fmb_fun_co1155576772iple_a_4 )
    & ( fmb_fun_co1155576772iple_a_2 != fmb_fun_co1155576772iple_a_3 )
    & ( fmb_fun_co1155576772iple_a_2 != fmb_fun_co1155576772iple_a_4 )
    & ( fmb_fun_co1155576772iple_a_3 != fmb_fun_co1155576772iple_a_4 ) ) ).

tff(declare_fun_pname_com,type,
    fun_pname_com: $tType ).

tff(declare_fun_pname_com1,type,
    fmb_fun_pname_com_1: fun_pname_com ).

tff(declare_fun_pname_com2,type,
    fmb_fun_pname_com_2: fun_pname_com ).

tff(declare_fun_pname_com3,type,
    fmb_fun_pname_com_3: fun_pname_com ).

tff(declare_fun_pname_com4,type,
    fmb_fun_pname_com_4: fun_pname_com ).

tff(finite_domain_fun_pname_com,axiom,
    ! [X: fun_pname_com] :
      ( ( X = fmb_fun_pname_com_1 )
      | ( X = fmb_fun_pname_com_2 )
      | ( X = fmb_fun_pname_com_3 )
      | ( X = fmb_fun_pname_com_4 ) ) ).

tff(distinct_domain_fun_pname_com,axiom,
    ( ( fmb_fun_pname_com_1 != fmb_fun_pname_com_2 )
    & ( fmb_fun_pname_com_1 != fmb_fun_pname_com_3 )
    & ( fmb_fun_pname_com_1 != fmb_fun_pname_com_4 )
    & ( fmb_fun_pname_com_2 != fmb_fun_pname_com_3 )
    & ( fmb_fun_pname_com_2 != fmb_fun_pname_com_4 )
    & ( fmb_fun_pname_com_3 != fmb_fun_pname_com_4 ) ) ).

tff(declare_fun_pname_pname,type,
    fun_pname_pname: $tType ).

tff(declare_fun_pname_pname1,type,
    fmb_fun_pname_pname_1: fun_pname_pname ).

tff(declare_fun_pname_pname2,type,
    fmb_fun_pname_pname_2: fun_pname_pname ).

tff(declare_fun_pname_pname3,type,
    fmb_fun_pname_pname_3: fun_pname_pname ).

tff(declare_fun_pname_pname4,type,
    fmb_fun_pname_pname_4: fun_pname_pname ).

tff(finite_domain_fun_pname_pname,axiom,
    ! [X: fun_pname_pname] :
      ( ( X = fmb_fun_pname_pname_1 )
      | ( X = fmb_fun_pname_pname_2 )
      | ( X = fmb_fun_pname_pname_3 )
      | ( X = fmb_fun_pname_pname_4 ) ) ).

tff(distinct_domain_fun_pname_pname,axiom,
    ( ( fmb_fun_pname_pname_1 != fmb_fun_pname_pname_2 )
    & ( fmb_fun_pname_pname_1 != fmb_fun_pname_pname_3 )
    & ( fmb_fun_pname_pname_1 != fmb_fun_pname_pname_4 )
    & ( fmb_fun_pname_pname_2 != fmb_fun_pname_pname_3 )
    & ( fmb_fun_pname_pname_2 != fmb_fun_pname_pname_4 )
    & ( fmb_fun_pname_pname_3 != fmb_fun_pname_pname_4 ) ) ).

tff(declare_fun_pname_bool,type,
    fun_pname_bool: $tType ).

tff(declare_fun_pname_bool1,type,
    fmb_fun_pname_bool_1: fun_pname_bool ).

tff(declare_fun_pname_bool2,type,
    fmb_fun_pname_bool_2: fun_pname_bool ).

tff(finite_domain_fun_pname_bool,axiom,
    ! [X: fun_pname_bool] :
      ( ( X = fmb_fun_pname_bool_1 )
      | ( X = fmb_fun_pname_bool_2 ) ) ).

tff(distinct_domain_fun_pname_bool,axiom,
    fmb_fun_pname_bool_1 != fmb_fun_pname_bool_2 ).

tff(declare_fun_pn708290217iple_a,type,
    fun_pn708290217iple_a: $tType ).

tff(declare_fun_pn708290217iple_a1,type,
    fmb_fun_pn708290217iple_a_1: fun_pn708290217iple_a ).

tff(declare_fun_pn708290217iple_a2,type,
    fmb_fun_pn708290217iple_a_2: fun_pn708290217iple_a ).

tff(declare_fun_pn708290217iple_a3,type,
    fmb_fun_pn708290217iple_a_3: fun_pn708290217iple_a ).

tff(declare_fun_pn708290217iple_a4,type,
    fmb_fun_pn708290217iple_a_4: fun_pn708290217iple_a ).

tff(finite_domain_fun_pn708290217iple_a,axiom,
    ! [X: fun_pn708290217iple_a] :
      ( ( X = fmb_fun_pn708290217iple_a_1 )
      | ( X = fmb_fun_pn708290217iple_a_2 )
      | ( X = fmb_fun_pn708290217iple_a_3 )
      | ( X = fmb_fun_pn708290217iple_a_4 ) ) ).

tff(distinct_domain_fun_pn708290217iple_a,axiom,
    ( ( fmb_fun_pn708290217iple_a_1 != fmb_fun_pn708290217iple_a_2 )
    & ( fmb_fun_pn708290217iple_a_1 != fmb_fun_pn708290217iple_a_3 )
    & ( fmb_fun_pn708290217iple_a_1 != fmb_fun_pn708290217iple_a_4 )
    & ( fmb_fun_pn708290217iple_a_2 != fmb_fun_pn708290217iple_a_3 )
    & ( fmb_fun_pn708290217iple_a_2 != fmb_fun_pn708290217iple_a_4 )
    & ( fmb_fun_pn708290217iple_a_3 != fmb_fun_pn708290217iple_a_4 ) ) ).

tff(declare_fun_pname_option_com,type,
    fun_pname_option_com: $tType ).

tff(declare_fun_pname_option_com1,type,
    fmb_fun_pname_option_com_1: fun_pname_option_com ).

tff(declare_fun_pname_option_com2,type,
    fmb_fun_pname_option_com_2: fun_pname_option_com ).

tff(declare_fun_pname_option_com3,type,
    fmb_fun_pname_option_com_3: fun_pname_option_com ).

tff(declare_fun_pname_option_com4,type,
    fmb_fun_pname_option_com_4: fun_pname_option_com ).

tff(finite_domain_fun_pname_option_com,axiom,
    ! [X: fun_pname_option_com] :
      ( ( X = fmb_fun_pname_option_com_1 )
      | ( X = fmb_fun_pname_option_com_2 )
      | ( X = fmb_fun_pname_option_com_3 )
      | ( X = fmb_fun_pname_option_com_4 ) ) ).

tff(distinct_domain_fun_pname_option_com,axiom,
    ( ( fmb_fun_pname_option_com_1 != fmb_fun_pname_option_com_2 )
    & ( fmb_fun_pname_option_com_1 != fmb_fun_pname_option_com_3 )
    & ( fmb_fun_pname_option_com_1 != fmb_fun_pname_option_com_4 )
    & ( fmb_fun_pname_option_com_2 != fmb_fun_pname_option_com_3 )
    & ( fmb_fun_pname_option_com_2 != fmb_fun_pname_option_com_4 )
    & ( fmb_fun_pname_option_com_3 != fmb_fun_pname_option_com_4 ) ) ).

tff(declare_fun_pn1683930517e_bool,type,
    fun_pn1683930517e_bool: $tType ).

tff(declare_fun_pn1683930517e_bool1,type,
    fmb_fun_pn1683930517e_bool_1: fun_pn1683930517e_bool ).

tff(declare_fun_pn1683930517e_bool2,type,
    fmb_fun_pn1683930517e_bool_2: fun_pn1683930517e_bool ).

tff(declare_fun_pn1683930517e_bool3,type,
    fmb_fun_pn1683930517e_bool_3: fun_pn1683930517e_bool ).

tff(declare_fun_pn1683930517e_bool4,type,
    fmb_fun_pn1683930517e_bool_4: fun_pn1683930517e_bool ).

tff(finite_domain_fun_pn1683930517e_bool,axiom,
    ! [X: fun_pn1683930517e_bool] :
      ( ( X = fmb_fun_pn1683930517e_bool_1 )
      | ( X = fmb_fun_pn1683930517e_bool_2 )
      | ( X = fmb_fun_pn1683930517e_bool_3 )
      | ( X = fmb_fun_pn1683930517e_bool_4 ) ) ).

tff(distinct_domain_fun_pn1683930517e_bool,axiom,
    ( ( fmb_fun_pn1683930517e_bool_1 != fmb_fun_pn1683930517e_bool_2 )
    & ( fmb_fun_pn1683930517e_bool_1 != fmb_fun_pn1683930517e_bool_3 )
    & ( fmb_fun_pn1683930517e_bool_1 != fmb_fun_pn1683930517e_bool_4 )
    & ( fmb_fun_pn1683930517e_bool_2 != fmb_fun_pn1683930517e_bool_3 )
    & ( fmb_fun_pn1683930517e_bool_2 != fmb_fun_pn1683930517e_bool_4 )
    & ( fmb_fun_pn1683930517e_bool_3 != fmb_fun_pn1683930517e_bool_4 ) ) ).

tff(declare_fun_pn308211645iple_a,type,
    fun_pn308211645iple_a: $tType ).

tff(declare_fun_pn308211645iple_a1,type,
    fmb_fun_pn308211645iple_a_1: fun_pn308211645iple_a ).

tff(declare_fun_pn308211645iple_a2,type,
    fmb_fun_pn308211645iple_a_2: fun_pn308211645iple_a ).

tff(declare_fun_pn308211645iple_a3,type,
    fmb_fun_pn308211645iple_a_3: fun_pn308211645iple_a ).

tff(declare_fun_pn308211645iple_a4,type,
    fmb_fun_pn308211645iple_a_4: fun_pn308211645iple_a ).

tff(finite_domain_fun_pn308211645iple_a,axiom,
    ! [X: fun_pn308211645iple_a] :
      ( ( X = fmb_fun_pn308211645iple_a_1 )
      | ( X = fmb_fun_pn308211645iple_a_2 )
      | ( X = fmb_fun_pn308211645iple_a_3 )
      | ( X = fmb_fun_pn308211645iple_a_4 ) ) ).

tff(distinct_domain_fun_pn308211645iple_a,axiom,
    ( ( fmb_fun_pn308211645iple_a_1 != fmb_fun_pn308211645iple_a_2 )
    & ( fmb_fun_pn308211645iple_a_1 != fmb_fun_pn308211645iple_a_3 )
    & ( fmb_fun_pn308211645iple_a_1 != fmb_fun_pn308211645iple_a_4 )
    & ( fmb_fun_pn308211645iple_a_2 != fmb_fun_pn308211645iple_a_3 )
    & ( fmb_fun_pn308211645iple_a_2 != fmb_fun_pn308211645iple_a_4 )
    & ( fmb_fun_pn308211645iple_a_3 != fmb_fun_pn308211645iple_a_4 ) ) ).

tff(declare_fun_pn800050071e_bool,type,
    fun_pn800050071e_bool: $tType ).

tff(declare_fun_pn800050071e_bool1,type,
    fmb_fun_pn800050071e_bool_1: fun_pn800050071e_bool ).

tff(declare_fun_pn800050071e_bool2,type,
    fmb_fun_pn800050071e_bool_2: fun_pn800050071e_bool ).

tff(declare_fun_pn800050071e_bool3,type,
    fmb_fun_pn800050071e_bool_3: fun_pn800050071e_bool ).

tff(declare_fun_pn800050071e_bool4,type,
    fmb_fun_pn800050071e_bool_4: fun_pn800050071e_bool ).

tff(finite_domain_fun_pn800050071e_bool,axiom,
    ! [X: fun_pn800050071e_bool] :
      ( ( X = fmb_fun_pn800050071e_bool_1 )
      | ( X = fmb_fun_pn800050071e_bool_2 )
      | ( X = fmb_fun_pn800050071e_bool_3 )
      | ( X = fmb_fun_pn800050071e_bool_4 ) ) ).

tff(distinct_domain_fun_pn800050071e_bool,axiom,
    ( ( fmb_fun_pn800050071e_bool_1 != fmb_fun_pn800050071e_bool_2 )
    & ( fmb_fun_pn800050071e_bool_1 != fmb_fun_pn800050071e_bool_3 )
    & ( fmb_fun_pn800050071e_bool_1 != fmb_fun_pn800050071e_bool_4 )
    & ( fmb_fun_pn800050071e_bool_2 != fmb_fun_pn800050071e_bool_3 )
    & ( fmb_fun_pn800050071e_bool_2 != fmb_fun_pn800050071e_bool_4 )
    & ( fmb_fun_pn800050071e_bool_3 != fmb_fun_pn800050071e_bool_4 ) ) ).

tff(declare_fun_pn250273176l_bool,type,
    fun_pn250273176l_bool: $tType ).

tff(declare_fun_pn250273176l_bool1,type,
    fmb_fun_pn250273176l_bool_1: fun_pn250273176l_bool ).

tff(declare_fun_pn250273176l_bool2,type,
    fmb_fun_pn250273176l_bool_2: fun_pn250273176l_bool ).

tff(declare_fun_pn250273176l_bool3,type,
    fmb_fun_pn250273176l_bool_3: fun_pn250273176l_bool ).

tff(declare_fun_pn250273176l_bool4,type,
    fmb_fun_pn250273176l_bool_4: fun_pn250273176l_bool ).

tff(finite_domain_fun_pn250273176l_bool,axiom,
    ! [X: fun_pn250273176l_bool] :
      ( ( X = fmb_fun_pn250273176l_bool_1 )
      | ( X = fmb_fun_pn250273176l_bool_2 )
      | ( X = fmb_fun_pn250273176l_bool_3 )
      | ( X = fmb_fun_pn250273176l_bool_4 ) ) ).

tff(distinct_domain_fun_pn250273176l_bool,axiom,
    ( ( fmb_fun_pn250273176l_bool_1 != fmb_fun_pn250273176l_bool_2 )
    & ( fmb_fun_pn250273176l_bool_1 != fmb_fun_pn250273176l_bool_3 )
    & ( fmb_fun_pn250273176l_bool_1 != fmb_fun_pn250273176l_bool_4 )
    & ( fmb_fun_pn250273176l_bool_2 != fmb_fun_pn250273176l_bool_3 )
    & ( fmb_fun_pn250273176l_bool_2 != fmb_fun_pn250273176l_bool_4 )
    & ( fmb_fun_pn250273176l_bool_3 != fmb_fun_pn250273176l_bool_4 ) ) ).

tff(declare_fun_pn579076298iple_a,type,
    fun_pn579076298iple_a: $tType ).

tff(declare_fun_pn579076298iple_a1,type,
    fmb_fun_pn579076298iple_a_1: fun_pn579076298iple_a ).

tff(declare_fun_pn579076298iple_a2,type,
    fmb_fun_pn579076298iple_a_2: fun_pn579076298iple_a ).

tff(declare_fun_pn579076298iple_a3,type,
    fmb_fun_pn579076298iple_a_3: fun_pn579076298iple_a ).

tff(declare_fun_pn579076298iple_a4,type,
    fmb_fun_pn579076298iple_a_4: fun_pn579076298iple_a ).

tff(finite_domain_fun_pn579076298iple_a,axiom,
    ! [X: fun_pn579076298iple_a] :
      ( ( X = fmb_fun_pn579076298iple_a_1 )
      | ( X = fmb_fun_pn579076298iple_a_2 )
      | ( X = fmb_fun_pn579076298iple_a_3 )
      | ( X = fmb_fun_pn579076298iple_a_4 ) ) ).

tff(distinct_domain_fun_pn579076298iple_a,axiom,
    ( ( fmb_fun_pn579076298iple_a_1 != fmb_fun_pn579076298iple_a_2 )
    & ( fmb_fun_pn579076298iple_a_1 != fmb_fun_pn579076298iple_a_3 )
    & ( fmb_fun_pn579076298iple_a_1 != fmb_fun_pn579076298iple_a_4 )
    & ( fmb_fun_pn579076298iple_a_2 != fmb_fun_pn579076298iple_a_3 )
    & ( fmb_fun_pn579076298iple_a_2 != fmb_fun_pn579076298iple_a_4 )
    & ( fmb_fun_pn579076298iple_a_3 != fmb_fun_pn579076298iple_a_4 ) ) ).

tff(declare_fun_pn422929397l_bool,type,
    fun_pn422929397l_bool: $tType ).

tff(declare_fun_pn422929397l_bool1,type,
    fmb_fun_pn422929397l_bool_1: fun_pn422929397l_bool ).

tff(declare_fun_pn422929397l_bool2,type,
    fmb_fun_pn422929397l_bool_2: fun_pn422929397l_bool ).

tff(declare_fun_pn422929397l_bool3,type,
    fmb_fun_pn422929397l_bool_3: fun_pn422929397l_bool ).

tff(declare_fun_pn422929397l_bool4,type,
    fmb_fun_pn422929397l_bool_4: fun_pn422929397l_bool ).

tff(finite_domain_fun_pn422929397l_bool,axiom,
    ! [X: fun_pn422929397l_bool] :
      ( ( X = fmb_fun_pn422929397l_bool_1 )
      | ( X = fmb_fun_pn422929397l_bool_2 )
      | ( X = fmb_fun_pn422929397l_bool_3 )
      | ( X = fmb_fun_pn422929397l_bool_4 ) ) ).

tff(distinct_domain_fun_pn422929397l_bool,axiom,
    ( ( fmb_fun_pn422929397l_bool_1 != fmb_fun_pn422929397l_bool_2 )
    & ( fmb_fun_pn422929397l_bool_1 != fmb_fun_pn422929397l_bool_3 )
    & ( fmb_fun_pn422929397l_bool_1 != fmb_fun_pn422929397l_bool_4 )
    & ( fmb_fun_pn422929397l_bool_2 != fmb_fun_pn422929397l_bool_3 )
    & ( fmb_fun_pn422929397l_bool_2 != fmb_fun_pn422929397l_bool_4 )
    & ( fmb_fun_pn422929397l_bool_3 != fmb_fun_pn422929397l_bool_4 ) ) ).

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

tff(declare_fun_bool_bool1,type,
    fmb_fun_bool_bool_1: fun_bool_bool ).

tff(declare_fun_bool_bool2,type,
    fmb_fun_bool_bool_2: fun_bool_bool ).

tff(declare_fun_bool_bool3,type,
    fmb_fun_bool_bool_3: fun_bool_bool ).

tff(declare_fun_bool_bool4,type,
    fmb_fun_bool_bool_4: fun_bool_bool ).

tff(finite_domain_fun_bool_bool,axiom,
    ! [X: fun_bool_bool] :
      ( ( X = fmb_fun_bool_bool_1 )
      | ( X = fmb_fun_bool_bool_2 )
      | ( X = fmb_fun_bool_bool_3 )
      | ( X = fmb_fun_bool_bool_4 ) ) ).

tff(distinct_domain_fun_bool_bool,axiom,
    ( ( fmb_fun_bool_bool_1 != fmb_fun_bool_bool_2 )
    & ( fmb_fun_bool_bool_1 != fmb_fun_bool_bool_3 )
    & ( fmb_fun_bool_bool_1 != fmb_fun_bool_bool_4 )
    & ( fmb_fun_bool_bool_2 != fmb_fun_bool_bool_3 )
    & ( fmb_fun_bool_bool_2 != fmb_fun_bool_bool_4 )
    & ( fmb_fun_bool_bool_3 != fmb_fun_bool_bool_4 ) ) ).

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

tff(declare_fun_bo1549164019l_bool1,type,
    fmb_fun_bo1549164019l_bool_1: fun_bo1549164019l_bool ).

tff(declare_fun_bo1549164019l_bool2,type,
    fmb_fun_bo1549164019l_bool_2: fun_bo1549164019l_bool ).

tff(declare_fun_bo1549164019l_bool3,type,
    fmb_fun_bo1549164019l_bool_3: fun_bo1549164019l_bool ).

tff(declare_fun_bo1549164019l_bool4,type,
    fmb_fun_bo1549164019l_bool_4: fun_bo1549164019l_bool ).

tff(finite_domain_fun_bo1549164019l_bool,axiom,
    ! [X: fun_bo1549164019l_bool] :
      ( ( X = fmb_fun_bo1549164019l_bool_1 )
      | ( X = fmb_fun_bo1549164019l_bool_2 )
      | ( X = fmb_fun_bo1549164019l_bool_3 )
      | ( X = fmb_fun_bo1549164019l_bool_4 ) ) ).

tff(distinct_domain_fun_bo1549164019l_bool,axiom,
    ( ( fmb_fun_bo1549164019l_bool_1 != fmb_fun_bo1549164019l_bool_2 )
    & ( fmb_fun_bo1549164019l_bool_1 != fmb_fun_bo1549164019l_bool_3 )
    & ( fmb_fun_bo1549164019l_bool_1 != fmb_fun_bo1549164019l_bool_4 )
    & ( fmb_fun_bo1549164019l_bool_2 != fmb_fun_bo1549164019l_bool_3 )
    & ( fmb_fun_bo1549164019l_bool_2 != fmb_fun_bo1549164019l_bool_4 )
    & ( fmb_fun_bo1549164019l_bool_3 != fmb_fun_bo1549164019l_bool_4 ) ) ).

tff(declare_fun_Ho842746065_pname,type,
    fun_Ho842746065_pname: $tType ).

tff(declare_fun_Ho842746065_pname1,type,
    fmb_fun_Ho842746065_pname_1: fun_Ho842746065_pname ).

tff(declare_fun_Ho842746065_pname2,type,
    fmb_fun_Ho842746065_pname_2: fun_Ho842746065_pname ).

tff(declare_fun_Ho842746065_pname3,type,
    fmb_fun_Ho842746065_pname_3: fun_Ho842746065_pname ).

tff(declare_fun_Ho842746065_pname4,type,
    fmb_fun_Ho842746065_pname_4: fun_Ho842746065_pname ).

tff(finite_domain_fun_Ho842746065_pname,axiom,
    ! [X: fun_Ho842746065_pname] :
      ( ( X = fmb_fun_Ho842746065_pname_1 )
      | ( X = fmb_fun_Ho842746065_pname_2 )
      | ( X = fmb_fun_Ho842746065_pname_3 )
      | ( X = fmb_fun_Ho842746065_pname_4 ) ) ).

tff(distinct_domain_fun_Ho842746065_pname,axiom,
    ( ( fmb_fun_Ho842746065_pname_1 != fmb_fun_Ho842746065_pname_2 )
    & ( fmb_fun_Ho842746065_pname_1 != fmb_fun_Ho842746065_pname_3 )
    & ( fmb_fun_Ho842746065_pname_1 != fmb_fun_Ho842746065_pname_4 )
    & ( fmb_fun_Ho842746065_pname_2 != fmb_fun_Ho842746065_pname_3 )
    & ( fmb_fun_Ho842746065_pname_2 != fmb_fun_Ho842746065_pname_4 )
    & ( fmb_fun_Ho842746065_pname_3 != fmb_fun_Ho842746065_pname_4 ) ) ).

tff(declare_fun_Ho1877127206a_bool,type,
    fun_Ho1877127206a_bool: $tType ).

tff(declare_fun_Ho1877127206a_bool1,type,
    fmb_fun_Ho1877127206a_bool_1: fun_Ho1877127206a_bool ).

tff(declare_fun_Ho1877127206a_bool2,type,
    fmb_fun_Ho1877127206a_bool_2: fun_Ho1877127206a_bool ).

tff(finite_domain_fun_Ho1877127206a_bool,axiom,
    ! [X: fun_Ho1877127206a_bool] :
      ( ( X = fmb_fun_Ho1877127206a_bool_1 )
      | ( X = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(distinct_domain_fun_Ho1877127206a_bool,axiom,
    fmb_fun_Ho1877127206a_bool_1 != fmb_fun_Ho1877127206a_bool_2 ).

tff(declare_fun_Ho843200573iple_a,type,
    fun_Ho843200573iple_a: $tType ).

tff(declare_fun_Ho843200573iple_a1,type,
    fmb_fun_Ho843200573iple_a_1: fun_Ho843200573iple_a ).

tff(declare_fun_Ho843200573iple_a2,type,
    fmb_fun_Ho843200573iple_a_2: fun_Ho843200573iple_a ).

tff(declare_fun_Ho843200573iple_a3,type,
    fmb_fun_Ho843200573iple_a_3: fun_Ho843200573iple_a ).

tff(declare_fun_Ho843200573iple_a4,type,
    fmb_fun_Ho843200573iple_a_4: fun_Ho843200573iple_a ).

tff(finite_domain_fun_Ho843200573iple_a,axiom,
    ! [X: fun_Ho843200573iple_a] :
      ( ( X = fmb_fun_Ho843200573iple_a_1 )
      | ( X = fmb_fun_Ho843200573iple_a_2 )
      | ( X = fmb_fun_Ho843200573iple_a_3 )
      | ( X = fmb_fun_Ho843200573iple_a_4 ) ) ).

tff(distinct_domain_fun_Ho843200573iple_a,axiom,
    ( ( fmb_fun_Ho843200573iple_a_1 != fmb_fun_Ho843200573iple_a_2 )
    & ( fmb_fun_Ho843200573iple_a_1 != fmb_fun_Ho843200573iple_a_3 )
    & ( fmb_fun_Ho843200573iple_a_1 != fmb_fun_Ho843200573iple_a_4 )
    & ( fmb_fun_Ho843200573iple_a_2 != fmb_fun_Ho843200573iple_a_3 )
    & ( fmb_fun_Ho843200573iple_a_2 != fmb_fun_Ho843200573iple_a_4 )
    & ( fmb_fun_Ho843200573iple_a_3 != fmb_fun_Ho843200573iple_a_4 ) ) ).

tff(declare_fun_Ho957066028l_bool,type,
    fun_Ho957066028l_bool: $tType ).

tff(declare_fun_Ho957066028l_bool1,type,
    fmb_fun_Ho957066028l_bool_1: fun_Ho957066028l_bool ).

tff(declare_fun_Ho957066028l_bool2,type,
    fmb_fun_Ho957066028l_bool_2: fun_Ho957066028l_bool ).

tff(declare_fun_Ho957066028l_bool3,type,
    fmb_fun_Ho957066028l_bool_3: fun_Ho957066028l_bool ).

tff(declare_fun_Ho957066028l_bool4,type,
    fmb_fun_Ho957066028l_bool_4: fun_Ho957066028l_bool ).

tff(finite_domain_fun_Ho957066028l_bool,axiom,
    ! [X: fun_Ho957066028l_bool] :
      ( ( X = fmb_fun_Ho957066028l_bool_1 )
      | ( X = fmb_fun_Ho957066028l_bool_2 )
      | ( X = fmb_fun_Ho957066028l_bool_3 )
      | ( X = fmb_fun_Ho957066028l_bool_4 ) ) ).

tff(distinct_domain_fun_Ho957066028l_bool,axiom,
    ( ( fmb_fun_Ho957066028l_bool_1 != fmb_fun_Ho957066028l_bool_2 )
    & ( fmb_fun_Ho957066028l_bool_1 != fmb_fun_Ho957066028l_bool_3 )
    & ( fmb_fun_Ho957066028l_bool_1 != fmb_fun_Ho957066028l_bool_4 )
    & ( fmb_fun_Ho957066028l_bool_2 != fmb_fun_Ho957066028l_bool_3 )
    & ( fmb_fun_Ho957066028l_bool_2 != fmb_fun_Ho957066028l_bool_4 )
    & ( fmb_fun_Ho957066028l_bool_3 != fmb_fun_Ho957066028l_bool_4 ) ) ).

tff(declare_fun_Ho440810351a_bool,type,
    fun_Ho440810351a_bool: $tType ).

tff(declare_fun_Ho440810351a_bool1,type,
    fmb_fun_Ho440810351a_bool_1: fun_Ho440810351a_bool ).

tff(declare_fun_Ho440810351a_bool2,type,
    fmb_fun_Ho440810351a_bool_2: fun_Ho440810351a_bool ).

tff(declare_fun_Ho440810351a_bool3,type,
    fmb_fun_Ho440810351a_bool_3: fun_Ho440810351a_bool ).

tff(declare_fun_Ho440810351a_bool4,type,
    fmb_fun_Ho440810351a_bool_4: fun_Ho440810351a_bool ).

tff(finite_domain_fun_Ho440810351a_bool,axiom,
    ! [X: fun_Ho440810351a_bool] :
      ( ( X = fmb_fun_Ho440810351a_bool_1 )
      | ( X = fmb_fun_Ho440810351a_bool_2 )
      | ( X = fmb_fun_Ho440810351a_bool_3 )
      | ( X = fmb_fun_Ho440810351a_bool_4 ) ) ).

tff(distinct_domain_fun_Ho440810351a_bool,axiom,
    ( ( fmb_fun_Ho440810351a_bool_1 != fmb_fun_Ho440810351a_bool_2 )
    & ( fmb_fun_Ho440810351a_bool_1 != fmb_fun_Ho440810351a_bool_3 )
    & ( fmb_fun_Ho440810351a_bool_1 != fmb_fun_Ho440810351a_bool_4 )
    & ( fmb_fun_Ho440810351a_bool_2 != fmb_fun_Ho440810351a_bool_3 )
    & ( fmb_fun_Ho440810351a_bool_2 != fmb_fun_Ho440810351a_bool_4 )
    & ( fmb_fun_Ho440810351a_bool_3 != fmb_fun_Ho440810351a_bool_4 ) ) ).

tff(declare_fun_Ho525994229l_bool,type,
    fun_Ho525994229l_bool: $tType ).

tff(declare_fun_Ho525994229l_bool1,type,
    fmb_fun_Ho525994229l_bool_1: fun_Ho525994229l_bool ).

tff(declare_fun_Ho525994229l_bool2,type,
    fmb_fun_Ho525994229l_bool_2: fun_Ho525994229l_bool ).

tff(declare_fun_Ho525994229l_bool3,type,
    fmb_fun_Ho525994229l_bool_3: fun_Ho525994229l_bool ).

tff(declare_fun_Ho525994229l_bool4,type,
    fmb_fun_Ho525994229l_bool_4: fun_Ho525994229l_bool ).

tff(finite_domain_fun_Ho525994229l_bool,axiom,
    ! [X: fun_Ho525994229l_bool] :
      ( ( X = fmb_fun_Ho525994229l_bool_1 )
      | ( X = fmb_fun_Ho525994229l_bool_2 )
      | ( X = fmb_fun_Ho525994229l_bool_3 )
      | ( X = fmb_fun_Ho525994229l_bool_4 ) ) ).

tff(distinct_domain_fun_Ho525994229l_bool,axiom,
    ( ( fmb_fun_Ho525994229l_bool_1 != fmb_fun_Ho525994229l_bool_2 )
    & ( fmb_fun_Ho525994229l_bool_1 != fmb_fun_Ho525994229l_bool_3 )
    & ( fmb_fun_Ho525994229l_bool_1 != fmb_fun_Ho525994229l_bool_4 )
    & ( fmb_fun_Ho525994229l_bool_2 != fmb_fun_Ho525994229l_bool_3 )
    & ( fmb_fun_Ho525994229l_bool_2 != fmb_fun_Ho525994229l_bool_4 )
    & ( fmb_fun_Ho525994229l_bool_3 != fmb_fun_Ho525994229l_bool_4 ) ) ).

tff(declare_fun_option_com_com,type,
    fun_option_com_com: $tType ).

tff(declare_fun_option_com_com1,type,
    fmb_fun_option_com_com_1: fun_option_com_com ).

tff(declare_fun_option_com_com2,type,
    fmb_fun_option_com_com_2: fun_option_com_com ).

tff(declare_fun_option_com_com3,type,
    fmb_fun_option_com_com_3: fun_option_com_com ).

tff(declare_fun_option_com_com4,type,
    fmb_fun_option_com_com_4: fun_option_com_com ).

tff(finite_domain_fun_option_com_com,axiom,
    ! [X: fun_option_com_com] :
      ( ( X = fmb_fun_option_com_com_1 )
      | ( X = fmb_fun_option_com_com_2 )
      | ( X = fmb_fun_option_com_com_3 )
      | ( X = fmb_fun_option_com_com_4 ) ) ).

tff(distinct_domain_fun_option_com_com,axiom,
    ( ( fmb_fun_option_com_com_1 != fmb_fun_option_com_com_2 )
    & ( fmb_fun_option_com_com_1 != fmb_fun_option_com_com_3 )
    & ( fmb_fun_option_com_com_1 != fmb_fun_option_com_com_4 )
    & ( fmb_fun_option_com_com_2 != fmb_fun_option_com_com_3 )
    & ( fmb_fun_option_com_com_2 != fmb_fun_option_com_com_4 )
    & ( fmb_fun_option_com_com_3 != fmb_fun_option_com_com_4 ) ) ).

tff(declare_fun_fu1344872529iple_a,type,
    fun_fu1344872529iple_a: $tType ).

tff(declare_fun_fu1344872529iple_a1,type,
    fmb_fun_fu1344872529iple_a_1: fun_fu1344872529iple_a ).

tff(declare_fun_fu1344872529iple_a2,type,
    fmb_fun_fu1344872529iple_a_2: fun_fu1344872529iple_a ).

tff(declare_fun_fu1344872529iple_a3,type,
    fmb_fun_fu1344872529iple_a_3: fun_fu1344872529iple_a ).

tff(declare_fun_fu1344872529iple_a4,type,
    fmb_fun_fu1344872529iple_a_4: fun_fu1344872529iple_a ).

tff(finite_domain_fun_fu1344872529iple_a,axiom,
    ! [X: fun_fu1344872529iple_a] :
      ( ( X = fmb_fun_fu1344872529iple_a_1 )
      | ( X = fmb_fun_fu1344872529iple_a_2 )
      | ( X = fmb_fun_fu1344872529iple_a_3 )
      | ( X = fmb_fun_fu1344872529iple_a_4 ) ) ).

tff(distinct_domain_fun_fu1344872529iple_a,axiom,
    ( ( fmb_fun_fu1344872529iple_a_1 != fmb_fun_fu1344872529iple_a_2 )
    & ( fmb_fun_fu1344872529iple_a_1 != fmb_fun_fu1344872529iple_a_3 )
    & ( fmb_fun_fu1344872529iple_a_1 != fmb_fun_fu1344872529iple_a_4 )
    & ( fmb_fun_fu1344872529iple_a_2 != fmb_fun_fu1344872529iple_a_3 )
    & ( fmb_fun_fu1344872529iple_a_2 != fmb_fun_fu1344872529iple_a_4 )
    & ( fmb_fun_fu1344872529iple_a_3 != fmb_fun_fu1344872529iple_a_4 ) ) ).

tff(declare_fun_fu90068325iple_a,type,
    fun_fu90068325iple_a: $tType ).

tff(declare_fun_fu90068325iple_a1,type,
    fmb_fun_fu90068325iple_a_1: fun_fu90068325iple_a ).

tff(declare_fun_fu90068325iple_a2,type,
    fmb_fun_fu90068325iple_a_2: fun_fu90068325iple_a ).

tff(declare_fun_fu90068325iple_a3,type,
    fmb_fun_fu90068325iple_a_3: fun_fu90068325iple_a ).

tff(declare_fun_fu90068325iple_a4,type,
    fmb_fun_fu90068325iple_a_4: fun_fu90068325iple_a ).

tff(finite_domain_fun_fu90068325iple_a,axiom,
    ! [X: fun_fu90068325iple_a] :
      ( ( X = fmb_fun_fu90068325iple_a_1 )
      | ( X = fmb_fun_fu90068325iple_a_2 )
      | ( X = fmb_fun_fu90068325iple_a_3 )
      | ( X = fmb_fun_fu90068325iple_a_4 ) ) ).

tff(distinct_domain_fun_fu90068325iple_a,axiom,
    ( ( fmb_fun_fu90068325iple_a_1 != fmb_fun_fu90068325iple_a_2 )
    & ( fmb_fun_fu90068325iple_a_1 != fmb_fun_fu90068325iple_a_3 )
    & ( fmb_fun_fu90068325iple_a_1 != fmb_fun_fu90068325iple_a_4 )
    & ( fmb_fun_fu90068325iple_a_2 != fmb_fun_fu90068325iple_a_3 )
    & ( fmb_fun_fu90068325iple_a_2 != fmb_fun_fu90068325iple_a_4 )
    & ( fmb_fun_fu90068325iple_a_3 != fmb_fun_fu90068325iple_a_4 ) ) ).

tff(declare_fun_fu1430349052l_bool,type,
    fun_fu1430349052l_bool: $tType ).

tff(declare_fun_fu1430349052l_bool1,type,
    fmb_fun_fu1430349052l_bool_1: fun_fu1430349052l_bool ).

tff(declare_fun_fu1430349052l_bool2,type,
    fmb_fun_fu1430349052l_bool_2: fun_fu1430349052l_bool ).

tff(declare_fun_fu1430349052l_bool3,type,
    fmb_fun_fu1430349052l_bool_3: fun_fu1430349052l_bool ).

tff(declare_fun_fu1430349052l_bool4,type,
    fmb_fun_fu1430349052l_bool_4: fun_fu1430349052l_bool ).

tff(finite_domain_fun_fu1430349052l_bool,axiom,
    ! [X: fun_fu1430349052l_bool] :
      ( ( X = fmb_fun_fu1430349052l_bool_1 )
      | ( X = fmb_fun_fu1430349052l_bool_2 )
      | ( X = fmb_fun_fu1430349052l_bool_3 )
      | ( X = fmb_fun_fu1430349052l_bool_4 ) ) ).

tff(distinct_domain_fun_fu1430349052l_bool,axiom,
    ( ( fmb_fun_fu1430349052l_bool_1 != fmb_fun_fu1430349052l_bool_2 )
    & ( fmb_fun_fu1430349052l_bool_1 != fmb_fun_fu1430349052l_bool_3 )
    & ( fmb_fun_fu1430349052l_bool_1 != fmb_fun_fu1430349052l_bool_4 )
    & ( fmb_fun_fu1430349052l_bool_2 != fmb_fun_fu1430349052l_bool_3 )
    & ( fmb_fun_fu1430349052l_bool_2 != fmb_fun_fu1430349052l_bool_4 )
    & ( fmb_fun_fu1430349052l_bool_3 != fmb_fun_fu1430349052l_bool_4 ) ) ).

tff(declare_fun_fu832487784l_bool,type,
    fun_fu832487784l_bool: $tType ).

tff(declare_fun_fu832487784l_bool1,type,
    fmb_fun_fu832487784l_bool_1: fun_fu832487784l_bool ).

tff(declare_fun_fu832487784l_bool2,type,
    fmb_fun_fu832487784l_bool_2: fun_fu832487784l_bool ).

tff(declare_fun_fu832487784l_bool3,type,
    fmb_fun_fu832487784l_bool_3: fun_fu832487784l_bool ).

tff(declare_fun_fu832487784l_bool4,type,
    fmb_fun_fu832487784l_bool_4: fun_fu832487784l_bool ).

tff(finite_domain_fun_fu832487784l_bool,axiom,
    ! [X: fun_fu832487784l_bool] :
      ( ( X = fmb_fun_fu832487784l_bool_1 )
      | ( X = fmb_fun_fu832487784l_bool_2 )
      | ( X = fmb_fun_fu832487784l_bool_3 )
      | ( X = fmb_fun_fu832487784l_bool_4 ) ) ).

tff(distinct_domain_fun_fu832487784l_bool,axiom,
    ( ( fmb_fun_fu832487784l_bool_1 != fmb_fun_fu832487784l_bool_2 )
    & ( fmb_fun_fu832487784l_bool_1 != fmb_fun_fu832487784l_bool_3 )
    & ( fmb_fun_fu832487784l_bool_1 != fmb_fun_fu832487784l_bool_4 )
    & ( fmb_fun_fu832487784l_bool_2 != fmb_fun_fu832487784l_bool_3 )
    & ( fmb_fun_fu832487784l_bool_2 != fmb_fun_fu832487784l_bool_4 )
    & ( fmb_fun_fu832487784l_bool_3 != fmb_fun_fu832487784l_bool_4 ) ) ).

tff(declare_body_1,type,
    body_1: fun_pname_option_com ).

tff(body_1_definition,axiom,
    body_1 = fmb_fun_pname_option_com_1 ).

tff(declare_body,type,
    body: fun_pname_com ).

tff(body_definition,axiom,
    body = fmb_fun_pname_com_1 ).

tff(declare_zero_zero_nat,type,
    zero_zero_nat: nat ).

tff(zero_zero_nat_definition,axiom,
    zero_zero_nat = fmb_nat_1 ).

tff(declare_hoare_1652181356iple_a,type,
    hoare_1652181356iple_a: fun_fu90068325iple_a ).

tff(hoare_1652181356iple_a_definition,axiom,
    hoare_1652181356iple_a = fmb_fun_fu90068325iple_a_1 ).

tff(declare_the_com,type,
    the_com: fun_option_com_com ).

tff(the_com_definition,axiom,
    the_com = fmb_fun_option_com_com_1 ).

tff(declare_bot_bo844097828e_bool,type,
    bot_bo844097828e_bool: fun_pname_bool ).

tff(bot_bo844097828e_bool_definition,axiom,
    bot_bo844097828e_bool = fmb_fun_pname_bool_1 ).

tff(declare_bot_bo1208640912a_bool,type,
    bot_bo1208640912a_bool: fun_Ho1877127206a_bool ).

tff(bot_bo1208640912a_bool_definition,axiom,
    bot_bo1208640912a_bool = fmb_fun_Ho1877127206a_bool_1 ).

tff(declare_fFalse,type,
    fFalse: bool ).

tff(fFalse_definition,axiom,
    fFalse = fmb_bool_1 ).

tff(declare_fNot,type,
    fNot: fun_bool_bool ).

tff(fNot_definition,axiom,
    fNot = fmb_fun_bool_bool_1 ).

tff(declare_fTrue,type,
    fTrue: bool ).

tff(fTrue_definition,axiom,
    fTrue = fmb_bool_2 ).

tff(declare_fconj,type,
    fconj: fun_bo1549164019l_bool ).

tff(fconj_definition,axiom,
    fconj = fmb_fun_bo1549164019l_bool_1 ).

tff(declare_fdisj,type,
    fdisj: fun_bo1549164019l_bool ).

tff(fdisj_definition,axiom,
    fdisj = fmb_fun_bo1549164019l_bool_2 ).

tff(declare_fequal_pname,type,
    fequal_pname: fun_pn800050071e_bool ).

tff(fequal_pname_definition,axiom,
    fequal_pname = fmb_fun_pn800050071e_bool_1 ).

tff(declare_fequal1440857775iple_a,type,
    fequal1440857775iple_a: fun_Ho440810351a_bool ).

tff(fequal1440857775iple_a_definition,axiom,
    fequal1440857775iple_a = fmb_fun_Ho440810351a_bool_1 ).

tff(declare_fimplies,type,
    fimplies: fun_bo1549164019l_bool ).

tff(fimplies_definition,axiom,
    fimplies = fmb_fun_bo1549164019l_bool_3 ).

tff(declare_member_pname,type,
    member_pname: fun_pn422929397l_bool ).

tff(member_pname_definition,axiom,
    member_pname = fmb_fun_pn422929397l_bool_1 ).

tff(declare_member127332739iple_a,type,
    member127332739iple_a: fun_Ho525994229l_bool ).

tff(member127332739iple_a_definition,axiom,
    member127332739iple_a = fmb_fun_Ho525994229l_bool_1 ).

tff(declare_g,type,
    g: fun_Ho1877127206a_bool ).

tff(g_definition,axiom,
    g = fmb_fun_Ho1877127206a_bool_1 ).

tff(declare_p,type,
    p: fun_pn1683930517e_bool ).

tff(p_definition,axiom,
    p = fmb_fun_pn1683930517e_bool_1 ).

tff(declare_procs,type,
    procs: fun_pname_bool ).

tff(procs_definition,axiom,
    procs = fmb_fun_pname_bool_2 ).

tff(declare_q,type,
    q: fun_pn1683930517e_bool ).

tff(q_definition,axiom,
    q = fmb_fun_pn1683930517e_bool_2 ).

tff(declare_n,type,
    n: nat ).

tff(n_definition,axiom,
    n = fmb_nat_2 ).

tff(declare_cOMBB_1110279240iple_a,type,
    cOMBB_1110279240iple_a: ( fun_pn708290217iple_a * fun_Ho842746065_pname ) > fun_Ho843200573iple_a ).

tff(function_cOMBB_1110279240iple_a,axiom,
    ( ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_Ho842746065_pname_1) = fmb_fun_Ho843200573iple_a_2 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_Ho842746065_pname_2) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_Ho842746065_pname_3) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_Ho842746065_pname_4) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_Ho842746065_pname_1) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_Ho842746065_pname_2) = fmb_fun_Ho843200573iple_a_3 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_Ho842746065_pname_3) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_Ho842746065_pname_4) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_Ho842746065_pname_1) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_Ho842746065_pname_2) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_Ho842746065_pname_3) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_Ho842746065_pname_4) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_Ho842746065_pname_1) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_Ho842746065_pname_2) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_Ho842746065_pname_3) = fmb_fun_Ho843200573iple_a_4 )
    & ( cOMBB_1110279240iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_Ho842746065_pname_4) = fmb_fun_Ho843200573iple_a_4 ) ) ).

tff(declare_cOMBB_647938656_pname,type,
    cOMBB_647938656_pname: ( fun_bool_bool * fun_pname_bool ) > fun_pname_bool ).

tff(function_cOMBB_647938656_pname,axiom,
    ( ( cOMBB_647938656_pname(fmb_fun_bool_bool_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_1 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_2,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_2,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_3,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_3,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_1 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_4,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBB_647938656_pname(fmb_fun_bool_bool_4,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_cOMBB_213049548iple_a,type,
    cOMBB_213049548iple_a: ( fun_bool_bool * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_cOMBB_213049548iple_a,axiom,
    ( ( cOMBB_213049548iple_a(fmb_fun_bool_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBB_213049548iple_a(fmb_fun_bool_bool_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_cOMBB_675860798_pname,type,
    cOMBB_675860798_pname: ( fun_bo1549164019l_bool * fun_pname_bool ) > fun_pn250273176l_bool ).

tff(function_cOMBB_675860798_pname,axiom,
    ( ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_1,fmb_fun_pname_bool_1) = fmb_fun_pn250273176l_bool_2 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_1,fmb_fun_pname_bool_2) = fmb_fun_pn250273176l_bool_4 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_2,fmb_fun_pname_bool_1) = fmb_fun_pn250273176l_bool_4 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_2,fmb_fun_pname_bool_2) = fmb_fun_pn250273176l_bool_3 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_3,fmb_fun_pname_bool_1) = fmb_fun_pn250273176l_bool_3 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_3,fmb_fun_pname_bool_2) = fmb_fun_pn250273176l_bool_4 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_4,fmb_fun_pname_bool_1) = fmb_fun_pn250273176l_bool_2 )
    & ( cOMBB_675860798_pname(fmb_fun_bo1549164019l_bool_4,fmb_fun_pname_bool_2) = fmb_fun_pn250273176l_bool_4 ) ) ).

tff(declare_cOMBB_196465322iple_a,type,
    cOMBB_196465322iple_a: ( fun_bo1549164019l_bool * fun_Ho1877127206a_bool ) > fun_Ho957066028l_bool ).

tff(function_cOMBB_196465322iple_a,axiom,
    ( ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho957066028l_bool_2 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho957066028l_bool_4 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho957066028l_bool_4 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho957066028l_bool_3 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho957066028l_bool_3 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho957066028l_bool_4 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho957066028l_bool_2 )
    & ( cOMBB_196465322iple_a(fmb_fun_bo1549164019l_bool_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho957066028l_bool_4 ) ) ).

tff(declare_cOMBB_1433562676_pname,type,
    cOMBB_1433562676_pname: ( fun_Ho842746065_pname * fun_pn708290217iple_a ) > fun_pname_pname ).

tff(function_cOMBB_1433562676_pname,axiom,
    ( ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_pn708290217iple_a_1) = fmb_fun_pname_pname_2 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_pn708290217iple_a_2) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_pn708290217iple_a_3) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_pn708290217iple_a_4) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_pn708290217iple_a_1) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_pn708290217iple_a_2) = fmb_fun_pname_pname_3 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_pn708290217iple_a_3) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_pn708290217iple_a_4) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_pn708290217iple_a_1) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_pn708290217iple_a_2) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_pn708290217iple_a_3) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_pn708290217iple_a_4) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_pn708290217iple_a_1) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_pn708290217iple_a_2) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_pn708290217iple_a_3) = fmb_fun_pname_pname_4 )
    & ( cOMBB_1433562676_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_pn708290217iple_a_4) = fmb_fun_pname_pname_4 ) ) ).

tff(declare_cOMBB_923936821_pname,type,
    cOMBB_923936821_pname: ( fun_option_com_com * fun_pname_option_com ) > fun_pname_com ).

tff(function_cOMBB_923936821_pname,axiom,
    ( ( cOMBB_923936821_pname(fmb_fun_option_com_com_1,fmb_fun_pname_option_com_1) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_1,fmb_fun_pname_option_com_2) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_1,fmb_fun_pname_option_com_3) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_1,fmb_fun_pname_option_com_4) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_2,fmb_fun_pname_option_com_1) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_2,fmb_fun_pname_option_com_2) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_2,fmb_fun_pname_option_com_3) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_2,fmb_fun_pname_option_com_4) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_3,fmb_fun_pname_option_com_1) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_3,fmb_fun_pname_option_com_2) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_3,fmb_fun_pname_option_com_3) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_3,fmb_fun_pname_option_com_4) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_4,fmb_fun_pname_option_com_1) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_4,fmb_fun_pname_option_com_2) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_4,fmb_fun_pname_option_com_3) = fmb_fun_pname_com_2 )
    & ( cOMBB_923936821_pname(fmb_fun_option_com_com_4,fmb_fun_pname_option_com_4) = fmb_fun_pname_com_2 ) ) ).

tff(declare_cOMBB_1515136928_pname,type,
    cOMBB_1515136928_pname: ( fun_fu90068325iple_a * fun_pn1683930517e_bool ) > fun_pn308211645iple_a ).

tff(function_cOMBB_1515136928_pname,axiom,
    ( ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_1,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_1,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn308211645iple_a_4 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_1,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_1,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_2,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_2,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn308211645iple_a_4 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_2,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_2,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_3,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_3,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn308211645iple_a_4 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_3,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_3,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_4,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_4,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn308211645iple_a_4 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_4,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn308211645iple_a_1 )
    & ( cOMBB_1515136928_pname(fmb_fun_fu90068325iple_a_4,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn308211645iple_a_1 ) ) ).

tff(declare_cOMBC_1149511130e_bool,type,
    cOMBC_1149511130e_bool: ( fun_pn800050071e_bool * pname ) > fun_pname_bool ).

tff(function_cOMBC_1149511130e_bool,axiom,
    ( ( cOMBC_1149511130e_bool(fmb_fun_pn800050071e_bool_1,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1149511130e_bool(fmb_fun_pn800050071e_bool_2,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1149511130e_bool(fmb_fun_pn800050071e_bool_3,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1149511130e_bool(fmb_fun_pn800050071e_bool_4,fmb_pname_1) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_cOMBC_1058051404l_bool,type,
    cOMBC_1058051404l_bool: ( fun_pn422929397l_bool * fun_pname_bool ) > fun_pname_bool ).

tff(function_cOMBC_1058051404l_bool,axiom,
    ( ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_2,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_2,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_3,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_3,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_4,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBC_1058051404l_bool(fmb_fun_pn422929397l_bool_4,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_cOMBC_671859290a_bool,type,
    cOMBC_671859290a_bool: ( fun_Ho440810351a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).

tff(function_cOMBC_671859290a_bool,axiom,
    ( ( cOMBC_671859290a_bool(fmb_fun_Ho440810351a_bool_1,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_671859290a_bool(fmb_fun_Ho440810351a_bool_2,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_671859290a_bool(fmb_fun_Ho440810351a_bool_3,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_671859290a_bool(fmb_fun_Ho440810351a_bool_4,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_cOMBC_862840740l_bool,type,
    cOMBC_862840740l_bool: ( fun_Ho525994229l_bool * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_cOMBC_862840740l_bool,axiom,
    ( ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBC_862840740l_bool(fmb_fun_Ho525994229l_bool_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_cOMBK_pname_pname,type,
    cOMBK_pname_pname: pname > fun_pname_pname ).

tff(function_cOMBK_pname_pname,axiom,
    cOMBK_pname_pname(fmb_pname_1) = fmb_fun_pname_pname_4 ).

tff(declare_cOMBK_1495131898iple_a,type,
    cOMBK_1495131898iple_a: pname > fun_Ho842746065_pname ).

tff(function_cOMBK_1495131898iple_a,axiom,
    cOMBK_1495131898iple_a(fmb_pname_1) = fmb_fun_Ho842746065_pname_2 ).

tff(declare_cOMBK_bool_pname,type,
    cOMBK_bool_pname: bool > fun_pname_bool ).

tff(function_cOMBK_bool_pname,axiom,
    ( ( cOMBK_bool_pname(fmb_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBK_bool_pname(fmb_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_cOMBK_712844119iple_a,type,
    cOMBK_712844119iple_a: bool > fun_Ho1877127206a_bool ).

tff(function_cOMBK_712844119iple_a,axiom,
    ( ( cOMBK_712844119iple_a(fmb_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBK_712844119iple_a(fmb_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_cOMBK_669226658_pname,type,
    cOMBK_669226658_pname: hoare_1927711152iple_a > fun_pn708290217iple_a ).

tff(function_cOMBK_669226658_pname,axiom,
    cOMBK_669226658_pname(fmb_hoare_1927711152iple_a_1) = fmb_fun_pn708290217iple_a_2 ).

tff(declare_cOMBK_2109678094iple_a,type,
    cOMBK_2109678094iple_a: hoare_1927711152iple_a > fun_Ho843200573iple_a ).

tff(function_cOMBK_2109678094iple_a,axiom,
    cOMBK_2109678094iple_a(fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho843200573iple_a_4 ).

tff(declare_cOMBS_1125763966iple_a,type,
    cOMBS_1125763966iple_a: ( fun_pn308211645iple_a * fun_pname_com ) > fun_pn579076298iple_a ).

tff(function_cOMBS_1125763966iple_a,axiom,
    ( ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_1,fmb_fun_pname_com_1) = fmb_fun_pn579076298iple_a_1 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_1,fmb_fun_pname_com_2) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_1,fmb_fun_pname_com_3) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_1,fmb_fun_pname_com_4) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_2,fmb_fun_pname_com_1) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_2,fmb_fun_pname_com_2) = fmb_fun_pn579076298iple_a_3 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_2,fmb_fun_pname_com_3) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_2,fmb_fun_pname_com_4) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_3,fmb_fun_pname_com_1) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_3,fmb_fun_pname_com_2) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_3,fmb_fun_pname_com_3) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_3,fmb_fun_pname_com_4) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_4,fmb_fun_pname_com_1) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_4,fmb_fun_pname_com_2) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_4,fmb_fun_pname_com_3) = fmb_fun_pn579076298iple_a_4 )
    & ( cOMBS_1125763966iple_a(fmb_fun_pn308211645iple_a_4,fmb_fun_pname_com_4) = fmb_fun_pn579076298iple_a_4 ) ) ).

tff(declare_cOMBS_568398431l_bool,type,
    cOMBS_568398431l_bool: ( fun_pn250273176l_bool * fun_pname_bool ) > fun_pname_bool ).

tff(function_cOMBS_568398431l_bool,axiom,
    ( ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_2,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_2,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_1 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_3,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_3,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_4,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( cOMBS_568398431l_bool(fmb_fun_pn250273176l_bool_4,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_cOMBS_821474699iple_a,type,
    cOMBS_821474699iple_a: ( fun_pn579076298iple_a * fun_pn1683930517e_bool ) > fun_pn708290217iple_a ).

tff(function_cOMBS_821474699iple_a,axiom,
    ( ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_1,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_1,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn708290217iple_a_1 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_1,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_1,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_2,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_2,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_2,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_2,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_3,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_3,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_3,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_3,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_4,fmb_fun_pn1683930517e_bool_1) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_4,fmb_fun_pn1683930517e_bool_2) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_4,fmb_fun_pn1683930517e_bool_3) = fmb_fun_pn708290217iple_a_4 )
    & ( cOMBS_821474699iple_a(fmb_fun_pn579076298iple_a_4,fmb_fun_pn1683930517e_bool_4) = fmb_fun_pn708290217iple_a_4 ) ) ).

tff(declare_cOMBS_2061548107l_bool,type,
    cOMBS_2061548107l_bool: ( fun_Ho957066028l_bool * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_cOMBS_2061548107l_bool,axiom,
    ( ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( cOMBS_2061548107l_bool(fmb_fun_Ho957066028l_bool_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_hoare_1617968510rivs_a,type,
    hoare_1617968510rivs_a: ( fun_Ho1877127206a_bool * fun_Ho1877127206a_bool ) > bool ).

tff(function_hoare_1617968510rivs_a,axiom,
    ( ( hoare_1617968510rivs_a(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hoare_1617968510rivs_a(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 )
    & ( hoare_1617968510rivs_a(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hoare_1617968510rivs_a(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 ) ) ).

tff(declare_hoare_1955801856lids_a,type,
    hoare_1955801856lids_a: ( fun_Ho1877127206a_bool * fun_Ho1877127206a_bool ) > bool ).

tff(function_hoare_1955801856lids_a,axiom,
    ( ( hoare_1955801856lids_a(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hoare_1955801856lids_a(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_1 )
    & ( hoare_1955801856lids_a(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hoare_1955801856lids_a(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 ) ) ).

tff(declare_hoare_1572001082alid_a,type,
    hoare_1572001082alid_a: nat > fun_Ho1877127206a_bool ).

tff(function_hoare_1572001082alid_a,axiom,
    ( ( hoare_1572001082alid_a(fmb_nat_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( hoare_1572001082alid_a(fmb_nat_2) = fmb_fun_Ho1877127206a_bool_1 )
    & ( hoare_1572001082alid_a(fmb_nat_3) = fmb_fun_Ho1877127206a_bool_2 )
    & ( hoare_1572001082alid_a(fmb_nat_4) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_semila1168014441p_bool,type,
    semila1168014441p_bool: ( bool * bool ) > bool ).

tff(function_semila1168014441p_bool,axiom,
    ( ( semila1168014441p_bool(fmb_bool_1,fmb_bool_1) = fmb_bool_1 )
    & ( semila1168014441p_bool(fmb_bool_1,fmb_bool_2) = fmb_bool_2 )
    & ( semila1168014441p_bool(fmb_bool_2,fmb_bool_1) = fmb_bool_2 )
    & ( semila1168014441p_bool(fmb_bool_2,fmb_bool_2) = fmb_bool_2 ) ) ).

tff(declare_semila278973382e_bool,type,
    semila278973382e_bool: ( fun_pname_bool * fun_pname_bool ) > fun_pname_bool ).

tff(function_semila278973382e_bool,axiom,
    ( ( semila278973382e_bool(fmb_fun_pname_bool_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( semila278973382e_bool(fmb_fun_pname_bool_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( semila278973382e_bool(fmb_fun_pname_bool_2,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( semila278973382e_bool(fmb_fun_pname_bool_2,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_semila1525949746a_bool,type,
    semila1525949746a_bool: ( fun_Ho1877127206a_bool * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_semila1525949746a_bool,axiom,
    ( ( semila1525949746a_bool(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( semila1525949746a_bool(fmb_fun_Ho1877127206a_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( semila1525949746a_bool(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( semila1525949746a_bool(fmb_fun_Ho1877127206a_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_suc,type,
    suc: nat > nat ).

tff(function_suc,axiom,
    ( ( suc(fmb_nat_1) = fmb_nat_3 )
    & ( suc(fmb_nat_2) = fmb_nat_2 )
    & ( suc(fmb_nat_3) = fmb_nat_4 )
    & ( suc(fmb_nat_4) = fmb_nat_4 ) ) ).

tff(declare_evalc,type,
    evalc: ( com * state * state ) > bool ).

tff(function_evalc,axiom,
    evalc(fmb_com_1,fmb_state_1,fmb_state_1) = fmb_bool_2 ).

tff(declare_collect_pname,type,
    collect_pname: fun_pname_bool > fun_pname_bool ).

tff(function_collect_pname,axiom,
    ( ( collect_pname(fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( collect_pname(fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_collec829051333iple_a,type,
    collec829051333iple_a: fun_Ho1877127206a_bool > fun_Ho1877127206a_bool ).

tff(function_collec829051333iple_a,axiom,
    ( ( collec829051333iple_a(fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( collec829051333iple_a(fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_image_pname_pname,type,
    image_pname_pname: ( fun_pname_pname * fun_pname_bool ) > fun_pname_bool ).

tff(function_image_pname_pname,axiom,
    ( ( image_pname_pname(fmb_fun_pname_pname_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( image_pname_pname(fmb_fun_pname_pname_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_pname_pname(fmb_fun_pname_pname_2,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_pname_pname(fmb_fun_pname_pname_2,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_pname_pname(fmb_fun_pname_pname_3,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_pname_pname(fmb_fun_pname_pname_3,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_pname_pname(fmb_fun_pname_pname_4,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_pname_pname(fmb_fun_pname_pname_4,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_image_68284913iple_a,type,
    image_68284913iple_a: ( fun_pn708290217iple_a * fun_pname_bool ) > fun_Ho1877127206a_bool ).

tff(function_image_68284913iple_a,axiom,
    ( ( image_68284913iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_pname_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_1,fmb_fun_pname_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_pname_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_2,fmb_fun_pname_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_pname_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_3,fmb_fun_pname_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_pname_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_68284913iple_a(fmb_fun_pn708290217iple_a_4,fmb_fun_pname_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_image_1389863321_pname,type,
    image_1389863321_pname: ( fun_Ho842746065_pname * fun_Ho1877127206a_bool ) > fun_pname_bool ).

tff(function_image_1389863321_pname,axiom,
    ( ( image_1389863321_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_pname_bool_2 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_pname_bool_1 )
    & ( image_1389863321_pname(fmb_fun_Ho842746065_pname_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_image_590713477iple_a,type,
    image_590713477iple_a: ( fun_Ho843200573iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_image_590713477iple_a,axiom,
    ( ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_2,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_2,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_3,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_3,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_4,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_1 )
    & ( image_590713477iple_a(fmb_fun_Ho843200573iple_a_4,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_insert_pname,type,
    insert_pname: ( pname * fun_pname_bool ) > fun_pname_bool ).

tff(function_insert_pname,axiom,
    ( ( insert_pname(fmb_pname_1,fmb_fun_pname_bool_1) = fmb_fun_pname_bool_2 )
    & ( insert_pname(fmb_pname_1,fmb_fun_pname_bool_2) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_insert1434104874iple_a,type,
    insert1434104874iple_a: ( hoare_1927711152iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).

tff(function_insert1434104874iple_a,axiom,
    ( ( insert1434104874iple_a(fmb_hoare_1927711152iple_a_1,fmb_fun_Ho1877127206a_bool_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( insert1434104874iple_a(fmb_hoare_1927711152iple_a_1,fmb_fun_Ho1877127206a_bool_2) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_hAPP_c429049308iple_a,type,
    hAPP_c429049308iple_a: ( fun_co1155576772iple_a * com ) > fun_fu1344872529iple_a ).

tff(function_hAPP_c429049308iple_a,axiom,
    ( ( hAPP_c429049308iple_a(fmb_fun_co1155576772iple_a_1,fmb_com_1) = fmb_fun_fu1344872529iple_a_2 )
    & ( hAPP_c429049308iple_a(fmb_fun_co1155576772iple_a_2,fmb_com_1) = fmb_fun_fu1344872529iple_a_3 )
    & ( hAPP_c429049308iple_a(fmb_fun_co1155576772iple_a_3,fmb_com_1) = fmb_fun_fu1344872529iple_a_4 )
    & ( hAPP_c429049308iple_a(fmb_fun_co1155576772iple_a_4,fmb_com_1) = fmb_fun_fu1344872529iple_a_4 ) ) ).

tff(declare_hAPP_pname_com,type,
    hAPP_pname_com: ( fun_pname_com * pname ) > com ).

tff(function_hAPP_pname_com,axiom,
    ( ( hAPP_pname_com(fmb_fun_pname_com_1,fmb_pname_1) = fmb_com_1 )
    & ( hAPP_pname_com(fmb_fun_pname_com_2,fmb_pname_1) = fmb_com_1 )
    & ( hAPP_pname_com(fmb_fun_pname_com_3,fmb_pname_1) = fmb_com_1 )
    & ( hAPP_pname_com(fmb_fun_pname_com_4,fmb_pname_1) = fmb_com_1 ) ) ).

tff(declare_hAPP_pname_pname,type,
    hAPP_pname_pname: ( fun_pname_pname * pname ) > pname ).

tff(function_hAPP_pname_pname,axiom,
    ( ( hAPP_pname_pname(fmb_fun_pname_pname_1,fmb_pname_1) = fmb_pname_1 )
    & ( hAPP_pname_pname(fmb_fun_pname_pname_2,fmb_pname_1) = fmb_pname_1 )
    & ( hAPP_pname_pname(fmb_fun_pname_pname_3,fmb_pname_1) = fmb_pname_1 )
    & ( hAPP_pname_pname(fmb_fun_pname_pname_4,fmb_pname_1) = fmb_pname_1 ) ) ).

tff(declare_hAPP_pname_bool,type,
    hAPP_pname_bool: ( fun_pname_bool * pname ) > bool ).

tff(function_hAPP_pname_bool,axiom,
    ( ( hAPP_pname_bool(fmb_fun_pname_bool_1,fmb_pname_1) = fmb_bool_1 )
    & ( hAPP_pname_bool(fmb_fun_pname_bool_2,fmb_pname_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_p824302401iple_a,type,
    hAPP_p824302401iple_a: ( fun_pn708290217iple_a * pname ) > hoare_1927711152iple_a ).

tff(function_hAPP_p824302401iple_a,axiom,
    ( ( hAPP_p824302401iple_a(fmb_fun_pn708290217iple_a_1,fmb_pname_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_p824302401iple_a(fmb_fun_pn708290217iple_a_2,fmb_pname_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_p824302401iple_a(fmb_fun_pn708290217iple_a_3,fmb_pname_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_p824302401iple_a(fmb_fun_pn708290217iple_a_4,fmb_pname_1) = fmb_hoare_1927711152iple_a_1 ) ) ).

tff(declare_hAPP_p799580910on_com,type,
    hAPP_p799580910on_com: ( fun_pname_option_com * pname ) > option_com ).

tff(function_hAPP_p799580910on_com,axiom,
    ( ( hAPP_p799580910on_com(fmb_fun_pname_option_com_1,fmb_pname_1) = fmb_option_com_2 )
    & ( hAPP_p799580910on_com(fmb_fun_pname_option_com_2,fmb_pname_1) = fmb_option_com_2 )
    & ( hAPP_p799580910on_com(fmb_fun_pname_option_com_3,fmb_pname_1) = fmb_option_com_2 )
    & ( hAPP_p799580910on_com(fmb_fun_pname_option_com_4,fmb_pname_1) = fmb_option_com_2 ) ) ).

tff(declare_hAPP_p635540397e_bool,type,
    hAPP_p635540397e_bool: ( fun_pn1683930517e_bool * pname ) > fun_a_fun_state_bool ).

tff(function_hAPP_p635540397e_bool,axiom,
    ( ( hAPP_p635540397e_bool(fmb_fun_pn1683930517e_bool_1,fmb_pname_1) = fmb_fun_a_fun_state_bool_1 )
    & ( hAPP_p635540397e_bool(fmb_fun_pn1683930517e_bool_2,fmb_pname_1) = fmb_fun_a_fun_state_bool_1 )
    & ( hAPP_p635540397e_bool(fmb_fun_pn1683930517e_bool_3,fmb_pname_1) = fmb_fun_a_fun_state_bool_1 )
    & ( hAPP_p635540397e_bool(fmb_fun_pn1683930517e_bool_4,fmb_pname_1) = fmb_fun_a_fun_state_bool_1 ) ) ).

tff(declare_hAPP_p1788720341iple_a,type,
    hAPP_p1788720341iple_a: ( fun_pn308211645iple_a * pname ) > fun_co1155576772iple_a ).

tff(function_hAPP_p1788720341iple_a,axiom,
    ( ( hAPP_p1788720341iple_a(fmb_fun_pn308211645iple_a_1,fmb_pname_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_p1788720341iple_a(fmb_fun_pn308211645iple_a_2,fmb_pname_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_p1788720341iple_a(fmb_fun_pn308211645iple_a_3,fmb_pname_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_p1788720341iple_a(fmb_fun_pn308211645iple_a_4,fmb_pname_1) = fmb_fun_co1155576772iple_a_2 ) ) ).

tff(declare_hAPP_p61793385e_bool,type,
    hAPP_p61793385e_bool: ( fun_pn800050071e_bool * pname ) > fun_pname_bool ).

tff(function_hAPP_p61793385e_bool,axiom,
    ( ( hAPP_p61793385e_bool(fmb_fun_pn800050071e_bool_1,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( hAPP_p61793385e_bool(fmb_fun_pn800050071e_bool_2,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( hAPP_p61793385e_bool(fmb_fun_pn800050071e_bool_3,fmb_pname_1) = fmb_fun_pname_bool_2 )
    & ( hAPP_p61793385e_bool(fmb_fun_pn800050071e_bool_4,fmb_pname_1) = fmb_fun_pname_bool_2 ) ) ).

tff(declare_hAPP_p393069232l_bool,type,
    hAPP_p393069232l_bool: ( fun_pn250273176l_bool * pname ) > fun_bool_bool ).

tff(function_hAPP_p393069232l_bool,axiom,
    ( ( hAPP_p393069232l_bool(fmb_fun_pn250273176l_bool_1,fmb_pname_1) = fmb_fun_bool_bool_2 )
    & ( hAPP_p393069232l_bool(fmb_fun_pn250273176l_bool_2,fmb_pname_1) = fmb_fun_bool_bool_3 )
    & ( hAPP_p393069232l_bool(fmb_fun_pn250273176l_bool_3,fmb_pname_1) = fmb_fun_bool_bool_2 )
    & ( hAPP_p393069232l_bool(fmb_fun_pn250273176l_bool_4,fmb_pname_1) = fmb_fun_bool_bool_4 ) ) ).

tff(declare_hAPP_p1513881570iple_a,type,
    hAPP_p1513881570iple_a: ( fun_pn579076298iple_a * pname ) > fun_fu1344872529iple_a ).

tff(function_hAPP_p1513881570iple_a,axiom,
    ( ( hAPP_p1513881570iple_a(fmb_fun_pn579076298iple_a_1,fmb_pname_1) = fmb_fun_fu1344872529iple_a_3 )
    & ( hAPP_p1513881570iple_a(fmb_fun_pn579076298iple_a_2,fmb_pname_1) = fmb_fun_fu1344872529iple_a_4 )
    & ( hAPP_p1513881570iple_a(fmb_fun_pn579076298iple_a_3,fmb_pname_1) = fmb_fun_fu1344872529iple_a_3 )
    & ( hAPP_p1513881570iple_a(fmb_fun_pn579076298iple_a_4,fmb_pname_1) = fmb_fun_fu1344872529iple_a_3 ) ) ).

tff(declare_hAPP_p338031245l_bool,type,
    hAPP_p338031245l_bool: ( fun_pn422929397l_bool * pname ) > fun_fu1430349052l_bool ).

tff(function_hAPP_p338031245l_bool,axiom,
    ( ( hAPP_p338031245l_bool(fmb_fun_pn422929397l_bool_1,fmb_pname_1) = fmb_fun_fu1430349052l_bool_2 )
    & ( hAPP_p338031245l_bool(fmb_fun_pn422929397l_bool_2,fmb_pname_1) = fmb_fun_fu1430349052l_bool_2 )
    & ( hAPP_p338031245l_bool(fmb_fun_pn422929397l_bool_3,fmb_pname_1) = fmb_fun_fu1430349052l_bool_2 )
    & ( hAPP_p338031245l_bool(fmb_fun_pn422929397l_bool_4,fmb_pname_1) = fmb_fun_fu1430349052l_bool_2 ) ) ).

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

tff(function_hAPP_bool_bool,axiom,
    ( ( hAPP_bool_bool(fmb_fun_bool_bool_1,fmb_bool_1) = fmb_bool_2 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_1,fmb_bool_2) = fmb_bool_1 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_2,fmb_bool_1) = fmb_bool_2 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_2,fmb_bool_2) = fmb_bool_2 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_3,fmb_bool_1) = fmb_bool_1 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_3,fmb_bool_2) = fmb_bool_1 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_4,fmb_bool_1) = fmb_bool_1 )
    & ( hAPP_bool_bool(fmb_fun_bool_bool_4,fmb_bool_2) = fmb_bool_2 ) ) ).

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

tff(function_hAPP_b589554111l_bool,axiom,
    ( ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_1,fmb_bool_1) = fmb_fun_bool_bool_3 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_1,fmb_bool_2) = fmb_fun_bool_bool_4 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_2,fmb_bool_1) = fmb_fun_bool_bool_4 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_2,fmb_bool_2) = fmb_fun_bool_bool_2 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_3,fmb_bool_1) = fmb_fun_bool_bool_2 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_3,fmb_bool_2) = fmb_fun_bool_bool_4 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_4,fmb_bool_1) = fmb_fun_bool_bool_3 )
    & ( hAPP_b589554111l_bool(fmb_fun_bo1549164019l_bool_4,fmb_bool_2) = fmb_fun_bool_bool_4 ) ) ).

tff(declare_hAPP_H2145880809_pname,type,
    hAPP_H2145880809_pname: ( fun_Ho842746065_pname * hoare_1927711152iple_a ) > pname ).

tff(function_hAPP_H2145880809_pname,axiom,
    ( ( hAPP_H2145880809_pname(fmb_fun_Ho842746065_pname_1,fmb_hoare_1927711152iple_a_1) = fmb_pname_1 )
    & ( hAPP_H2145880809_pname(fmb_fun_Ho842746065_pname_2,fmb_hoare_1927711152iple_a_1) = fmb_pname_1 )
    & ( hAPP_H2145880809_pname(fmb_fun_Ho842746065_pname_3,fmb_hoare_1927711152iple_a_1) = fmb_pname_1 )
    & ( hAPP_H2145880809_pname(fmb_fun_Ho842746065_pname_4,fmb_hoare_1927711152iple_a_1) = fmb_pname_1 ) ) ).

tff(declare_hAPP_H1448631928a_bool,type,
    hAPP_H1448631928a_bool: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > bool ).

tff(function_hAPP_H1448631928a_bool,axiom,
    ( ( hAPP_H1448631928a_bool(fmb_fun_Ho1877127206a_bool_1,fmb_hoare_1927711152iple_a_1) = fmb_bool_1 )
    & ( hAPP_H1448631928a_bool(fmb_fun_Ho1877127206a_bool_2,fmb_hoare_1927711152iple_a_1) = fmb_bool_2 ) ) ).

tff(declare_hAPP_H963118037iple_a,type,
    hAPP_H963118037iple_a: ( fun_Ho843200573iple_a * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).

tff(function_hAPP_H963118037iple_a,axiom,
    ( ( hAPP_H963118037iple_a(fmb_fun_Ho843200573iple_a_1,fmb_hoare_1927711152iple_a_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_H963118037iple_a(fmb_fun_Ho843200573iple_a_2,fmb_hoare_1927711152iple_a_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_H963118037iple_a(fmb_fun_Ho843200573iple_a_3,fmb_hoare_1927711152iple_a_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_H963118037iple_a(fmb_fun_Ho843200573iple_a_4,fmb_hoare_1927711152iple_a_1) = fmb_hoare_1927711152iple_a_1 ) ) ).

tff(declare_hAPP_H1487873860l_bool,type,
    hAPP_H1487873860l_bool: ( fun_Ho957066028l_bool * hoare_1927711152iple_a ) > fun_bool_bool ).

tff(function_hAPP_H1487873860l_bool,axiom,
    ( ( hAPP_H1487873860l_bool(fmb_fun_Ho957066028l_bool_1,fmb_hoare_1927711152iple_a_1) = fmb_fun_bool_bool_2 )
    & ( hAPP_H1487873860l_bool(fmb_fun_Ho957066028l_bool_2,fmb_hoare_1927711152iple_a_1) = fmb_fun_bool_bool_3 )
    & ( hAPP_H1487873860l_bool(fmb_fun_Ho957066028l_bool_3,fmb_hoare_1927711152iple_a_1) = fmb_fun_bool_bool_2 )
    & ( hAPP_H1487873860l_bool(fmb_fun_Ho957066028l_bool_4,fmb_hoare_1927711152iple_a_1) = fmb_fun_bool_bool_4 ) ) ).

tff(declare_hAPP_H1027145665a_bool,type,
    hAPP_H1027145665a_bool: ( fun_Ho440810351a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).

tff(function_hAPP_H1027145665a_bool,axiom,
    ( ( hAPP_H1027145665a_bool(fmb_fun_Ho440810351a_bool_1,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( hAPP_H1027145665a_bool(fmb_fun_Ho440810351a_bool_2,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( hAPP_H1027145665a_bool(fmb_fun_Ho440810351a_bool_3,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 )
    & ( hAPP_H1027145665a_bool(fmb_fun_Ho440810351a_bool_4,fmb_hoare_1927711152iple_a_1) = fmb_fun_Ho1877127206a_bool_2 ) ) ).

tff(declare_hAPP_H694056973l_bool,type,
    hAPP_H694056973l_bool: ( fun_Ho525994229l_bool * hoare_1927711152iple_a ) > fun_fu832487784l_bool ).

tff(function_hAPP_H694056973l_bool,axiom,
    ( ( hAPP_H694056973l_bool(fmb_fun_Ho525994229l_bool_1,fmb_hoare_1927711152iple_a_1) = fmb_fun_fu832487784l_bool_1 )
    & ( hAPP_H694056973l_bool(fmb_fun_Ho525994229l_bool_2,fmb_hoare_1927711152iple_a_1) = fmb_fun_fu832487784l_bool_1 )
    & ( hAPP_H694056973l_bool(fmb_fun_Ho525994229l_bool_3,fmb_hoare_1927711152iple_a_1) = fmb_fun_fu832487784l_bool_1 )
    & ( hAPP_H694056973l_bool(fmb_fun_Ho525994229l_bool_4,fmb_hoare_1927711152iple_a_1) = fmb_fun_fu832487784l_bool_1 ) ) ).

tff(declare_hAPP_option_com_com,type,
    hAPP_option_com_com: ( fun_option_com_com * option_com ) > com ).

tff(function_hAPP_option_com_com,axiom,
    ( ( hAPP_option_com_com(fmb_fun_option_com_com_1,fmb_option_com_1) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_1,fmb_option_com_2) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_1,fmb_option_com_3) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_1,fmb_option_com_4) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_2,fmb_option_com_1) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_2,fmb_option_com_2) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_2,fmb_option_com_3) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_2,fmb_option_com_4) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_3,fmb_option_com_1) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_3,fmb_option_com_2) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_3,fmb_option_com_3) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_3,fmb_option_com_4) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_4,fmb_option_com_1) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_4,fmb_option_com_2) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_4,fmb_option_com_3) = fmb_com_1 )
    & ( hAPP_option_com_com(fmb_fun_option_com_com_4,fmb_option_com_4) = fmb_com_1 ) ) ).

tff(declare_hAPP_f711275241iple_a,type,
    hAPP_f711275241iple_a: ( fun_fu1344872529iple_a * fun_a_fun_state_bool ) > hoare_1927711152iple_a ).

tff(function_hAPP_f711275241iple_a,axiom,
    ( ( hAPP_f711275241iple_a(fmb_fun_fu1344872529iple_a_1,fmb_fun_a_fun_state_bool_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_f711275241iple_a(fmb_fun_fu1344872529iple_a_2,fmb_fun_a_fun_state_bool_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_f711275241iple_a(fmb_fun_fu1344872529iple_a_3,fmb_fun_a_fun_state_bool_1) = fmb_hoare_1927711152iple_a_1 )
    & ( hAPP_f711275241iple_a(fmb_fun_fu1344872529iple_a_4,fmb_fun_a_fun_state_bool_1) = fmb_hoare_1927711152iple_a_1 ) ) ).

tff(declare_hAPP_f185596029iple_a,type,
    hAPP_f185596029iple_a: ( fun_fu90068325iple_a * fun_a_fun_state_bool ) > fun_co1155576772iple_a ).

tff(function_hAPP_f185596029iple_a,axiom,
    ( ( hAPP_f185596029iple_a(fmb_fun_fu90068325iple_a_1,fmb_fun_a_fun_state_bool_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_f185596029iple_a(fmb_fun_fu90068325iple_a_2,fmb_fun_a_fun_state_bool_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_f185596029iple_a(fmb_fun_fu90068325iple_a_3,fmb_fun_a_fun_state_bool_1) = fmb_fun_co1155576772iple_a_2 )
    & ( hAPP_f185596029iple_a(fmb_fun_fu90068325iple_a_4,fmb_fun_a_fun_state_bool_1) = fmb_fun_co1155576772iple_a_2 ) ) ).

tff(declare_hAPP_f1664156314l_bool,type,
    hAPP_f1664156314l_bool: ( fun_fu1430349052l_bool * fun_pname_bool ) > bool ).

tff(function_hAPP_f1664156314l_bool,axiom,
    ( ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_1,fmb_fun_pname_bool_1) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_1,fmb_fun_pname_bool_2) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_2,fmb_fun_pname_bool_1) = fmb_bool_1 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_2,fmb_fun_pname_bool_2) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_3,fmb_fun_pname_bool_1) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_3,fmb_fun_pname_bool_2) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_4,fmb_fun_pname_bool_1) = fmb_bool_2 )
    & ( hAPP_f1664156314l_bool(fmb_fun_fu1430349052l_bool_4,fmb_fun_pname_bool_2) = fmb_bool_2 ) ) ).

tff(declare_hAPP_f1454306822l_bool,type,
    hAPP_f1454306822l_bool: ( fun_fu832487784l_bool * fun_Ho1877127206a_bool ) > bool ).

tff(function_hAPP_f1454306822l_bool,axiom,
    ( ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_1,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_1 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_1,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_2,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_2,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_3,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_3,fmb_fun_Ho1877127206a_bool_2) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_4,fmb_fun_Ho1877127206a_bool_1) = fmb_bool_2 )
    & ( hAPP_f1454306822l_bool(fmb_fun_fu832487784l_bool_4,fmb_fun_Ho1877127206a_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.03  % Problem  : SWW471_1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16  % Computer : n018.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:05:10 UTC 2026
% 0.10/0.17  % CPUTime  : 
% 0.10/0.17  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19  Running first-order model finding
% 0.10/0.20  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.44/1.01  % (3398442)Will run a generic schedule for satisfiability detection.
% 4.44/1.01  % (3398448)% WARNING: option uhcvi not known.
% 4.44/1.01  % (3398447)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4161041710_2999 on theBenchmark for (2999ds/0Mi)
% 4.44/1.01  % (3398449)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3317000019:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.44/1.01  % (3398451)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1492632380:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.44/1.01  % (3398448)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4215748857:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.44/1.01  % (3398450)dis+10_1_sil=32000:sp=arity:random_seed=3271729660:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.44/1.01  % (3398452)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2039318695:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.44/1.01  % (3398453)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=509073304:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.44/1.01  % (3398451)Instruction limit reached! 
% 4.44/1.01  % (3398451)------------------------------
% 4.44/1.01  % (3398451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398451)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398451)Termination reason: Instruction limit
% 4.44/1.01  % (3398451)Termination phase: Saturation
% 4.44/1.01  % (3398451)Time elapsed: 0.037 s
% 4.44/1.01  % (3398451)Peak memory usage: 13 MB
% 4.44/1.01  % (3398451)Instructions burned: 118 (million)
% 4.44/1.01  % (3398461)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1643621713:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.44/1.01  % (3398450)Instruction limit reached! 
% 4.44/1.01  % (3398450)------------------------------
% 4.44/1.01  % (3398450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398450)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398450)Termination reason: Instruction limit
% 4.44/1.01  % (3398450)Termination phase: Saturation
% 4.44/1.01  % (3398450)Time elapsed: 0.064 s
% 4.44/1.01  % (3398450)Peak memory usage: 13 MB
% 4.44/1.01  % (3398450)Instructions burned: 103 (million)
% 4.44/1.01  % (3398452)Instruction limit reached! 
% 4.44/1.01  % (3398452)------------------------------
% 4.44/1.01  % (3398452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398452)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398452)Termination reason: Instruction limit
% 4.44/1.01  % (3398452)Termination phase: Saturation
% 4.44/1.01  % (3398452)Time elapsed: 0.079 s
% 4.44/1.01  % (3398452)Peak memory usage: 13 MB
% 4.44/1.01  % (3398452)Instructions burned: 132 (million)
% 4.44/1.01  % (3398463)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3208751828:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.44/1.01  % (3398453)Instruction limit reached! 
% 4.44/1.01  % (3398453)------------------------------
% 4.44/1.01  % (3398453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398453)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398453)Termination reason: Instruction limit
% 4.44/1.01  % (3398453)Termination phase: Saturation
% 4.44/1.01  % (3398453)Time elapsed: 0.092 s
% 4.44/1.01  % (3398453)Peak memory usage: 13 MB
% 4.44/1.01  % (3398453)Instructions burned: 161 (million)
% 4.44/1.01  % (3398464)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=136171411:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.44/1.01  % (3398466)ott-21_1_sil=16000:fs=off:random_seed=4173655636:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.44/1.01  % TRYING [1]
% 4.44/1.01  % TRYING [2]
% 4.44/1.01  % TRYING [3]
% 4.44/1.01  % (3398463)Instruction limit reached! 
% 4.44/1.01  % (3398463)------------------------------
% 4.44/1.01  % (3398463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398463)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398463)Termination reason: Instruction limit
% 4.44/1.01  % (3398463)Termination phase: Saturation
% 4.44/1.01  % (3398463)Time elapsed: 0.074 s
% 4.44/1.01  % (3398463)Peak memory usage: 13 MB
% 4.44/1.01  % (3398463)Instructions burned: 131 (million)
% 4.44/1.01  % (3398469)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2071588035:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.44/1.01  % (3398466)Instruction limit reached! 
% 4.44/1.01  % (3398466)------------------------------
% 4.44/1.01  % (3398466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398466)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398466)Termination reason: Instruction limit
% 4.44/1.01  % (3398466)Termination phase: Saturation
% 4.44/1.01  % (3398466)Time elapsed: 0.091 s
% 4.44/1.01  % (3398466)Peak memory usage: 13 MB
% 4.44/1.01  % (3398466)Instructions burned: 184 (million)
% 4.44/1.01  % (3398461)Instruction limit reached! 
% 4.44/1.01  % (3398461)------------------------------
% 4.44/1.01  % (3398461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398461)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398461)Termination reason: Instruction limit
% 4.44/1.01  % (3398461)Termination phase: Finite model building constraint generation
% 4.44/1.01  % (3398461)Time elapsed: 0.167 s
% 4.44/1.01  % (3398461)Peak memory usage: 37 MB
% 4.44/1.01  % (3398461)Instructions burned: 714 (million)
% 4.44/1.01  % (3398471)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1636836515:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.44/1.01  % (3398472)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2134374982:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.44/1.01  % (3398464)Instruction limit reached! 
% 4.44/1.01  % (3398464)------------------------------
% 4.44/1.01  % (3398464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398464)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398464)Termination reason: Instruction limit
% 4.44/1.01  % (3398464)Termination phase: Saturation
% 4.44/1.01  % (3398464)Time elapsed: 0.362 s
% 4.44/1.01  % (3398464)Peak memory usage: 17 MB
% 4.44/1.01  % (3398464)Instructions burned: 686 (million)
% 4.44/1.01  % (3398475)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=348770498:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.44/1.01  % (3398469)Instruction limit reached! 
% 4.44/1.01  % (3398469)------------------------------
% 4.44/1.01  % (3398469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398469)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398469)Termination reason: Instruction limit
% 4.44/1.01  % (3398469)Termination phase: Saturation
% 4.44/1.01  % (3398469)Time elapsed: 0.309 s
% 4.44/1.01  % (3398469)Peak memory usage: 14 MB
% 4.44/1.01  % (3398469)Instructions burned: 477 (million)
% 4.44/1.01  % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1]
% 4.44/1.01  % Detected maximum model sizes of [max,max,max,max,max,2,max,max,max]
% 4.44/1.01  % TRYING [1,1,1,1,1,1,1,1,1]
% 4.44/1.01  % (3398477)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2000115826:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.44/1.01  % TRYING [1,1,1,1,1,2,1,1,1]
% 4.44/1.01  % TRYING [1,1,2,1,1,2,1,1,1]
% 4.44/1.01  % TRYING [1,2,2,1,1,2,1,1,1]
% 4.44/1.01  % TRYING [2,2,2,1,1,2,1,1,1]
% 4.44/1.01  % (3398472)Instruction limit reached! 
% 4.44/1.01  % (3398472)------------------------------
% 4.44/1.01  % (3398472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398472)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398472)Termination reason: Instruction limit
% 4.44/1.01  % (3398472)Termination phase: Saturation
% 4.44/1.01  % (3398472)Time elapsed: 0.338 s
% 4.44/1.01  % (3398472)Peak memory usage: 18 MB
% 4.44/1.01  % (3398472)Instructions burned: 1182 (million)
% 4.44/1.01  % (3398479)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2847326822:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.44/1.01  % (3398471)Instruction limit reached! 
% 4.44/1.01  % (3398471)------------------------------
% 4.44/1.01  % (3398471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.01  % (3398471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.01  % (3398471)CaDiCaL version: 2.1.3
% 4.44/1.01  % (3398471)Termination reason: Instruction limit
% 4.44/1.01  % (3398471)Termination phase: Finite model building preprocessing
% 4.44/1.01  % (3398471)Time elapsed: 0.376 s
% 4.44/1.01  % (3398471)Peak memory usage: 20 MB
% 4.44/1.01  % (3398471)Instructions burned: 865 (million)
% 4.44/1.01  % TRYING [3,2,2,1,1,2,1,1,1]
% 4.44/1.01  % (3398481)fmb+10_1_sil=64000:random_seed=1295839378:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 4.44/1.01  % TRYING [4,2,2,1,1,2,1,1,1]
% 4.44/1.01  % Finite Model Found!
% 4.44/1.01  % SZS status CounterSatisfiable for theBenchmark
% 4.44/1.01  % (3398447) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3398442-3398447"...
% 4.44/1.01  % (3398447)...printing done.
% 4.44/1.01  % SZS output start FiniteModel for theBenchmark
% See solution above
% 4.44/1.02  % (3398447)------------------------------
% 4.44/1.02  % (3398447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.02  % (3398447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.02  % (3398447)CaDiCaL version: 2.1.3
% 4.44/1.02  % (3398447)Termination reason: Satisfiable
% 4.44/1.02  % (3398447)Time elapsed: 0.771 s
% 4.44/1.02  % (3398447)Peak memory usage: 37 MB
% 4.44/1.02  % (3398447)Instructions burned: 1874 (million)
% 4.44/1.02  % (3398442)Success in time 0.813 s
% 4.44/1.02  % Vampire exiting
%------------------------------------------------------------------------------