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

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

% Computer : n009.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 11:39:22 AM UTC 2026

% Result   : Satisfiable 3.92s 1.09s
% Output   : FiniteModel 3.92s
% 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_B_a_b_vec_fun$',type,
    'B_a_b_vec_fun$': $tType ).

tff('declare_B_a_b_vec_fun$1',type,
    'fmb_B_a_b_vec_fun$_1': 'B_a_b_vec_fun$' ).

tff('declare_B_a_b_vec_fun$2',type,
    'fmb_B_a_b_vec_fun$_2': 'B_a_b_vec_fun$' ).

tff('finite_domain_B_a_b_vec_fun$',axiom,
    ! [X: 'B_a_b_vec_fun$'] :
      ( ( X = 'fmb_B_a_b_vec_fun$_1' )
      | ( X = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('distinct_domain_B_a_b_vec_fun$',axiom,
    'fmb_B_a_b_vec_fun$_1' != 'fmb_B_a_b_vec_fun$_2' ).

tff('declare_A_b_vec_n_vec_a_fun$',type,
    'A_b_vec_n_vec_a_fun$': $tType ).

tff('declare_A_b_vec_n_vec_a_fun$1',type,
    'fmb_A_b_vec_n_vec_a_fun$_1': 'A_b_vec_n_vec_a_fun$' ).

tff('declare_A_b_vec_n_vec_a_fun$2',type,
    'fmb_A_b_vec_n_vec_a_fun$_2': 'A_b_vec_n_vec_a_fun$' ).

tff('finite_domain_A_b_vec_n_vec_a_fun$',axiom,
    ! [X: 'A_b_vec_n_vec_a_fun$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_a_fun$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_a_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_a_fun$',axiom,
    'fmb_A_b_vec_n_vec_a_fun$_1' != 'fmb_A_b_vec_n_vec_a_fun$_2' ).

tff('declare_N_a_b_vec_n_vec_bool_fun_fun$',type,
    'N_a_b_vec_n_vec_bool_fun_fun$': $tType ).

tff('declare_N_a_b_vec_n_vec_bool_fun_fun$1',type,
    'fmb_N_a_b_vec_n_vec_bool_fun_fun$_1': 'N_a_b_vec_n_vec_bool_fun_fun$' ).

tff('declare_N_a_b_vec_n_vec_bool_fun_fun$2',type,
    'fmb_N_a_b_vec_n_vec_bool_fun_fun$_2': 'N_a_b_vec_n_vec_bool_fun_fun$' ).

tff('finite_domain_N_a_b_vec_n_vec_bool_fun_fun$',axiom,
    ! [X: 'N_a_b_vec_n_vec_bool_fun_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_n_vec_bool_fun_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_n_vec_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_n_vec_bool_fun_fun$',axiom,
    'fmb_N_a_b_vec_n_vec_bool_fun_fun$_1' != 'fmb_N_a_b_vec_n_vec_bool_fun_fun$_2' ).

tff('declare_A_b_vec_n_vec$',type,
    'A_b_vec_n_vec$': $tType ).

tff('declare_A_b_vec_n_vec$1',type,
    'fmb_A_b_vec_n_vec$_1': 'A_b_vec_n_vec$' ).

tff('declare_A_b_vec_n_vec$2',type,
    'fmb_A_b_vec_n_vec$_2': 'A_b_vec_n_vec$' ).

tff('finite_domain_A_b_vec_n_vec$',axiom,
    ! [X: 'A_b_vec_n_vec$'] :
      ( ( X = 'fmb_A_b_vec_n_vec$_1' )
      | ( X = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec$',axiom,
    'fmb_A_b_vec_n_vec$_1' != 'fmb_A_b_vec_n_vec$_2' ).

tff('declare_N_a_b_vec_n_vec_n_vec_fun$',type,
    'N_a_b_vec_n_vec_n_vec_fun$': $tType ).

tff('declare_N_a_b_vec_n_vec_n_vec_fun$1',type,
    'fmb_N_a_b_vec_n_vec_n_vec_fun$_1': 'N_a_b_vec_n_vec_n_vec_fun$' ).

tff('declare_N_a_b_vec_n_vec_n_vec_fun$2',type,
    'fmb_N_a_b_vec_n_vec_n_vec_fun$_2': 'N_a_b_vec_n_vec_n_vec_fun$' ).

tff('finite_domain_N_a_b_vec_n_vec_n_vec_fun$',axiom,
    ! [X: 'N_a_b_vec_n_vec_n_vec_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_n_vec_n_vec_fun$',axiom,
    'fmb_N_a_b_vec_n_vec_n_vec_fun$_1' != 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' ).

tff('declare_A_b_vec_a_b_vec_fun$',type,
    'A_b_vec_a_b_vec_fun$': $tType ).

tff('declare_A_b_vec_a_b_vec_fun$1',type,
    'fmb_A_b_vec_a_b_vec_fun$_1': 'A_b_vec_a_b_vec_fun$' ).

tff('declare_A_b_vec_a_b_vec_fun$2',type,
    'fmb_A_b_vec_a_b_vec_fun$_2': 'A_b_vec_a_b_vec_fun$' ).

tff('finite_domain_A_b_vec_a_b_vec_fun$',axiom,
    ! [X: 'A_b_vec_a_b_vec_fun$'] :
      ( ( X = 'fmb_A_b_vec_a_b_vec_fun$_1' )
      | ( X = 'fmb_A_b_vec_a_b_vec_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_a_b_vec_fun$',axiom,
    'fmb_A_b_vec_a_b_vec_fun$_1' != 'fmb_A_b_vec_a_b_vec_fun$_2' ).

tff('declare_A_a_n_vec_fun$',type,
    'A_a_n_vec_fun$': $tType ).

tff('declare_A_a_n_vec_fun$1',type,
    'fmb_A_a_n_vec_fun$_1': 'A_a_n_vec_fun$' ).

tff('declare_A_a_n_vec_fun$2',type,
    'fmb_A_a_n_vec_fun$_2': 'A_a_n_vec_fun$' ).

tff('finite_domain_A_a_n_vec_fun$',axiom,
    ! [X: 'A_a_n_vec_fun$'] :
      ( ( X = 'fmb_A_a_n_vec_fun$_1' )
      | ( X = 'fmb_A_a_n_vec_fun$_2' ) ) ).

tff('distinct_domain_A_a_n_vec_fun$',axiom,
    'fmb_A_a_n_vec_fun$_1' != 'fmb_A_a_n_vec_fun$_2' ).

tff('declare_N_a_b_vec_bool_fun_fun$',type,
    'N_a_b_vec_bool_fun_fun$': $tType ).

tff('declare_N_a_b_vec_bool_fun_fun$1',type,
    'fmb_N_a_b_vec_bool_fun_fun$_1': 'N_a_b_vec_bool_fun_fun$' ).

tff('declare_N_a_b_vec_bool_fun_fun$2',type,
    'fmb_N_a_b_vec_bool_fun_fun$_2': 'N_a_b_vec_bool_fun_fun$' ).

tff('finite_domain_N_a_b_vec_bool_fun_fun$',axiom,
    ! [X: 'N_a_b_vec_bool_fun_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_bool_fun_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_bool_fun_fun$',axiom,
    'fmb_N_a_b_vec_bool_fun_fun$_1' != 'fmb_N_a_b_vec_bool_fun_fun$_2' ).

tff('declare_A_n_vec_a_fun$',type,
    'A_n_vec_a_fun$': $tType ).

tff('declare_A_n_vec_a_fun$1',type,
    'fmb_A_n_vec_a_fun$_1': 'A_n_vec_a_fun$' ).

tff('declare_A_n_vec_a_fun$2',type,
    'fmb_A_n_vec_a_fun$_2': 'A_n_vec_a_fun$' ).

tff('finite_domain_A_n_vec_a_fun$',axiom,
    ! [X: 'A_n_vec_a_fun$'] :
      ( ( X = 'fmb_A_n_vec_a_fun$_1' )
      | ( X = 'fmb_A_n_vec_a_fun$_2' ) ) ).

tff('distinct_domain_A_n_vec_a_fun$',axiom,
    'fmb_A_n_vec_a_fun$_1' != 'fmb_A_n_vec_a_fun$_2' ).

tff('declare_A_n_vec_b_vec$',type,
    'A_n_vec_b_vec$': $tType ).

tff('declare_A_n_vec_b_vec$1',type,
    'fmb_A_n_vec_b_vec$_1': 'A_n_vec_b_vec$' ).

tff('finite_domain_A_n_vec_b_vec$',axiom,
    ! [X: 'A_n_vec_b_vec$'] : ( X = 'fmb_A_n_vec_b_vec$_1' ) ).

tff('declare_A_b_vec_n_vec_n_vec$',type,
    'A_b_vec_n_vec_n_vec$': $tType ).

tff('declare_A_b_vec_n_vec_n_vec$1',type,
    'fmb_A_b_vec_n_vec_n_vec$_1': 'A_b_vec_n_vec_n_vec$' ).

tff('declare_A_b_vec_n_vec_n_vec$2',type,
    'fmb_A_b_vec_n_vec_n_vec$_2': 'A_b_vec_n_vec_n_vec$' ).

tff('finite_domain_A_b_vec_n_vec_n_vec$',axiom,
    ! [X: 'A_b_vec_n_vec_n_vec$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_n_vec$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_n_vec$',axiom,
    'fmb_A_b_vec_n_vec_n_vec$_1' != 'fmb_A_b_vec_n_vec_n_vec$_2' ).

tff('declare_N_a_n_vec_fun$',type,
    'N_a_n_vec_fun$': $tType ).

tff('declare_N_a_n_vec_fun$1',type,
    'fmb_N_a_n_vec_fun$_1': 'N_a_n_vec_fun$' ).

tff('declare_N_a_n_vec_fun$2',type,
    'fmb_N_a_n_vec_fun$_2': 'N_a_n_vec_fun$' ).

tff('finite_domain_N_a_n_vec_fun$',axiom,
    ! [X: 'N_a_n_vec_fun$'] :
      ( ( X = 'fmb_N_a_n_vec_fun$_1' )
      | ( X = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_n_vec_fun$',axiom,
    'fmb_N_a_n_vec_fun$_1' != 'fmb_N_a_n_vec_fun$_2' ).

tff('declare_A_n_vec_a_b_vec_fun$',type,
    'A_n_vec_a_b_vec_fun$': $tType ).

tff('declare_A_n_vec_a_b_vec_fun$1',type,
    'fmb_A_n_vec_a_b_vec_fun$_1': 'A_n_vec_a_b_vec_fun$' ).

tff('declare_A_n_vec_a_b_vec_fun$2',type,
    'fmb_A_n_vec_a_b_vec_fun$_2': 'A_n_vec_a_b_vec_fun$' ).

tff('finite_domain_A_n_vec_a_b_vec_fun$',axiom,
    ! [X: 'A_n_vec_a_b_vec_fun$'] :
      ( ( X = 'fmb_A_n_vec_a_b_vec_fun$_1' )
      | ( X = 'fmb_A_n_vec_a_b_vec_fun$_2' ) ) ).

tff('distinct_domain_A_n_vec_a_b_vec_fun$',axiom,
    'fmb_A_n_vec_a_b_vec_fun$_1' != 'fmb_A_n_vec_a_b_vec_fun$_2' ).

tff('declare_A_a_b_vec_fun$',type,
    'A_a_b_vec_fun$': $tType ).

tff('declare_A_a_b_vec_fun$1',type,
    'fmb_A_a_b_vec_fun$_1': 'A_a_b_vec_fun$' ).

tff('declare_A_a_b_vec_fun$2',type,
    'fmb_A_a_b_vec_fun$_2': 'A_a_b_vec_fun$' ).

tff('finite_domain_A_a_b_vec_fun$',axiom,
    ! [X: 'A_a_b_vec_fun$'] :
      ( ( X = 'fmb_A_a_b_vec_fun$_1' )
      | ( X = 'fmb_A_a_b_vec_fun$_2' ) ) ).

tff('distinct_domain_A_a_b_vec_fun$',axiom,
    'fmb_A_a_b_vec_fun$_1' != 'fmb_A_a_b_vec_fun$_2' ).

tff('declare_A_b_vec_b_vec$',type,
    'A_b_vec_b_vec$': $tType ).

tff('declare_A_b_vec_b_vec$1',type,
    'fmb_A_b_vec_b_vec$_1': 'A_b_vec_b_vec$' ).

tff('declare_A_b_vec_b_vec$2',type,
    'fmb_A_b_vec_b_vec$_2': 'A_b_vec_b_vec$' ).

tff('finite_domain_A_b_vec_b_vec$',axiom,
    ! [X: 'A_b_vec_b_vec$'] :
      ( ( X = 'fmb_A_b_vec_b_vec$_1' )
      | ( X = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('distinct_domain_A_b_vec_b_vec$',axiom,
    'fmb_A_b_vec_b_vec$_1' != 'fmb_A_b_vec_b_vec$_2' ).

tff('declare_A_n_vec_n_vec$',type,
    'A_n_vec_n_vec$': $tType ).

tff('declare_A_n_vec_n_vec$1',type,
    'fmb_A_n_vec_n_vec$_1': 'A_n_vec_n_vec$' ).

tff('declare_A_n_vec_n_vec$2',type,
    'fmb_A_n_vec_n_vec$_2': 'A_n_vec_n_vec$' ).

tff('finite_domain_A_n_vec_n_vec$',axiom,
    ! [X: 'A_n_vec_n_vec$'] :
      ( ( X = 'fmb_A_n_vec_n_vec$_1' )
      | ( X = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('distinct_domain_A_n_vec_n_vec$',axiom,
    'fmb_A_n_vec_n_vec$_1' != 'fmb_A_n_vec_n_vec$_2' ).

tff('declare_N_a_n_vec_bool_fun_fun$',type,
    'N_a_n_vec_bool_fun_fun$': $tType ).

tff('declare_N_a_n_vec_bool_fun_fun$1',type,
    'fmb_N_a_n_vec_bool_fun_fun$_1': 'N_a_n_vec_bool_fun_fun$' ).

tff('declare_N_a_n_vec_bool_fun_fun$2',type,
    'fmb_N_a_n_vec_bool_fun_fun$_2': 'N_a_n_vec_bool_fun_fun$' ).

tff('finite_domain_N_a_n_vec_bool_fun_fun$',axiom,
    ! [X: 'N_a_n_vec_bool_fun_fun$'] :
      ( ( X = 'fmb_N_a_n_vec_bool_fun_fun$_1' )
      | ( X = 'fmb_N_a_n_vec_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_N_a_n_vec_bool_fun_fun$',axiom,
    'fmb_N_a_n_vec_bool_fun_fun$_1' != 'fmb_N_a_n_vec_bool_fun_fun$_2' ).

tff('declare_B$',type,
    'B$': $tType ).

tff('declare_B$1',type,
    'fmb_B$_1': 'B$' ).

tff('finite_domain_B$',axiom,
    ! [X: 'B$'] : ( X = 'fmb_B$_1' ) ).

tff('declare_A_a_b_vec_n_vec_fun$',type,
    'A_a_b_vec_n_vec_fun$': $tType ).

tff('declare_A_a_b_vec_n_vec_fun$1',type,
    'fmb_A_a_b_vec_n_vec_fun$_1': 'A_a_b_vec_n_vec_fun$' ).

tff('declare_A_a_b_vec_n_vec_fun$2',type,
    'fmb_A_a_b_vec_n_vec_fun$_2': 'A_a_b_vec_n_vec_fun$' ).

tff('finite_domain_A_a_b_vec_n_vec_fun$',axiom,
    ! [X: 'A_a_b_vec_n_vec_fun$'] :
      ( ( X = 'fmb_A_a_b_vec_n_vec_fun$_1' )
      | ( X = 'fmb_A_a_b_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_A_a_b_vec_n_vec_fun$',axiom,
    'fmb_A_a_b_vec_n_vec_fun$_1' != 'fmb_A_a_b_vec_n_vec_fun$_2' ).

tff('declare_A_b_vec$',type,
    'A_b_vec$': $tType ).

tff('declare_A_b_vec$1',type,
    'fmb_A_b_vec$_1': 'A_b_vec$' ).

tff('declare_A_b_vec$2',type,
    'fmb_A_b_vec$_2': 'A_b_vec$' ).

tff('finite_domain_A_b_vec$',axiom,
    ! [X: 'A_b_vec$'] :
      ( ( X = 'fmb_A_b_vec$_1' )
      | ( X = 'fmb_A_b_vec$_2' ) ) ).

tff('distinct_domain_A_b_vec$',axiom,
    'fmb_A_b_vec$_1' != 'fmb_A_b_vec$_2' ).

tff('declare_N$',type,
    'N$': $tType ).

tff('declare_N$1',type,
    'fmb_N$_1': 'N$' ).

tff('finite_domain_N$',axiom,
    ! [X: 'N$'] : ( X = 'fmb_N$_1' ) ).

tff('declare_N_a_b_vec_b_vec_fun$',type,
    'N_a_b_vec_b_vec_fun$': $tType ).

tff('declare_N_a_b_vec_b_vec_fun$1',type,
    'fmb_N_a_b_vec_b_vec_fun$_1': 'N_a_b_vec_b_vec_fun$' ).

tff('declare_N_a_b_vec_b_vec_fun$2',type,
    'fmb_N_a_b_vec_b_vec_fun$_2': 'N_a_b_vec_b_vec_fun$' ).

tff('finite_domain_N_a_b_vec_b_vec_fun$',axiom,
    ! [X: 'N_a_b_vec_b_vec_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_b_vec_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_b_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_b_vec_fun$',axiom,
    'fmb_N_a_b_vec_b_vec_fun$_1' != 'fmb_N_a_b_vec_b_vec_fun$_2' ).

tff('declare_A_b_vec_n_vec_bool_fun$',type,
    'A_b_vec_n_vec_bool_fun$': $tType ).

tff('declare_A_b_vec_n_vec_bool_fun$1',type,
    'fmb_A_b_vec_n_vec_bool_fun$_1': 'A_b_vec_n_vec_bool_fun$' ).

tff('declare_A_b_vec_n_vec_bool_fun$2',type,
    'fmb_A_b_vec_n_vec_bool_fun$_2': 'A_b_vec_n_vec_bool_fun$' ).

tff('finite_domain_A_b_vec_n_vec_bool_fun$',axiom,
    ! [X: 'A_b_vec_n_vec_bool_fun$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_bool_fun$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_bool_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_bool_fun$',axiom,
    'fmb_A_b_vec_n_vec_bool_fun$_1' != 'fmb_A_b_vec_n_vec_bool_fun$_2' ).

tff('declare_B_a_fun$',type,
    'B_a_fun$': $tType ).

tff('declare_B_a_fun$1',type,
    'fmb_B_a_fun$_1': 'B_a_fun$' ).

tff('declare_B_a_fun$2',type,
    'fmb_B_a_fun$_2': 'B_a_fun$' ).

tff('finite_domain_B_a_fun$',axiom,
    ! [X: 'B_a_fun$'] :
      ( ( X = 'fmb_B_a_fun$_1' )
      | ( X = 'fmb_B_a_fun$_2' ) ) ).

tff('distinct_domain_B_a_fun$',axiom,
    'fmb_B_a_fun$_1' != 'fmb_B_a_fun$_2' ).

tff(declare_tlbool,type,
    tlbool: $tType ).

tff(declare_tlbool1,type,
    fmb_tlbool_1: tlbool ).

tff(declare_tlbool2,type,
    fmb_tlbool_2: tlbool ).

tff(finite_domain_tlbool,axiom,
    ! [X: tlbool] :
      ( ( X = fmb_tlbool_1 )
      | ( X = fmb_tlbool_2 ) ) ).

tff(distinct_domain_tlbool,axiom,
    fmb_tlbool_1 != fmb_tlbool_2 ).

tff('declare_N_a_bool_fun_fun$',type,
    'N_a_bool_fun_fun$': $tType ).

tff('declare_N_a_bool_fun_fun$1',type,
    'fmb_N_a_bool_fun_fun$_1': 'N_a_bool_fun_fun$' ).

tff('declare_N_a_bool_fun_fun$2',type,
    'fmb_N_a_bool_fun_fun$_2': 'N_a_bool_fun_fun$' ).

tff('finite_domain_N_a_bool_fun_fun$',axiom,
    ! [X: 'N_a_bool_fun_fun$'] :
      ( ( X = 'fmb_N_a_bool_fun_fun$_1' )
      | ( X = 'fmb_N_a_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_N_a_bool_fun_fun$',axiom,
    'fmb_N_a_bool_fun_fun$_1' != 'fmb_N_a_bool_fun_fun$_2' ).

tff('declare_A_bool_fun$',type,
    'A_bool_fun$': $tType ).

tff('declare_A_bool_fun$1',type,
    'fmb_A_bool_fun$_1': 'A_bool_fun$' ).

tff('declare_A_bool_fun$2',type,
    'fmb_A_bool_fun$_2': 'A_bool_fun$' ).

tff('finite_domain_A_bool_fun$',axiom,
    ! [X: 'A_bool_fun$'] :
      ( ( X = 'fmb_A_bool_fun$_1' )
      | ( X = 'fmb_A_bool_fun$_2' ) ) ).

tff('distinct_domain_A_bool_fun$',axiom,
    'fmb_A_bool_fun$_1' != 'fmb_A_bool_fun$_2' ).

tff('declare_N_a_fun$',type,
    'N_a_fun$': $tType ).

tff('declare_N_a_fun$1',type,
    'fmb_N_a_fun$_1': 'N_a_fun$' ).

tff('declare_N_a_fun$2',type,
    'fmb_N_a_fun$_2': 'N_a_fun$' ).

tff('finite_domain_N_a_fun$',axiom,
    ! [X: 'N_a_fun$'] :
      ( ( X = 'fmb_N_a_fun$_1' )
      | ( X = 'fmb_N_a_fun$_2' ) ) ).

tff('distinct_domain_N_a_fun$',axiom,
    'fmb_N_a_fun$_1' != 'fmb_N_a_fun$_2' ).

tff('declare_N_a_b_vec_fun$',type,
    'N_a_b_vec_fun$': $tType ).

tff('declare_N_a_b_vec_fun$1',type,
    'fmb_N_a_b_vec_fun$_1': 'N_a_b_vec_fun$' ).

tff('declare_N_a_b_vec_fun$2',type,
    'fmb_N_a_b_vec_fun$_2': 'N_a_b_vec_fun$' ).

tff('finite_domain_N_a_b_vec_fun$',axiom,
    ! [X: 'N_a_b_vec_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_fun$',axiom,
    'fmb_N_a_b_vec_fun$_1' != 'fmb_N_a_b_vec_fun$_2' ).

tff('declare_A_b_vec_n_vec_a_b_vec_n_vec_fun$',type,
    'A_b_vec_n_vec_a_b_vec_n_vec_fun$': $tType ).

tff('declare_A_b_vec_n_vec_a_b_vec_n_vec_fun$1',type,
    'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1': 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' ).

tff('declare_A_b_vec_n_vec_a_b_vec_n_vec_fun$2',type,
    'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2': 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' ).

tff('finite_domain_A_b_vec_n_vec_a_b_vec_n_vec_fun$',axiom,
    ! [X: 'A_b_vec_n_vec_a_b_vec_n_vec_fun$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_a_b_vec_n_vec_fun$',axiom,
    'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1' != 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2' ).

tff('declare_A$',type,
    'A$': $tType ).

tff('declare_A$1',type,
    'fmb_A$_1': 'A$' ).

tff('declare_A$2',type,
    'fmb_A$_2': 'A$' ).

tff('finite_domain_A$',axiom,
    ! [X: 'A$'] :
      ( ( X = 'fmb_A$_1' )
      | ( X = 'fmb_A$_2' ) ) ).

tff('distinct_domain_A$',axiom,
    'fmb_A$_1' != 'fmb_A$_2' ).

tff('declare_N_n_fun$',type,
    'N_n_fun$': $tType ).

tff('declare_N_n_fun$1',type,
    'fmb_N_n_fun$_1': 'N_n_fun$' ).

tff('declare_N_n_fun$2',type,
    'fmb_N_n_fun$_2': 'N_n_fun$' ).

tff('finite_domain_N_n_fun$',axiom,
    ! [X: 'N_n_fun$'] :
      ( ( X = 'fmb_N_n_fun$_1' )
      | ( X = 'fmb_N_n_fun$_2' ) ) ).

tff('distinct_domain_N_n_fun$',axiom,
    'fmb_N_n_fun$_1' != 'fmb_N_n_fun$_2' ).

tff('declare_A_n_vec$',type,
    'A_n_vec$': $tType ).

tff('declare_A_n_vec$1',type,
    'fmb_A_n_vec$_1': 'A_n_vec$' ).

tff('declare_A_n_vec$2',type,
    'fmb_A_n_vec$_2': 'A_n_vec$' ).

tff('finite_domain_A_n_vec$',axiom,
    ! [X: 'A_n_vec$'] :
      ( ( X = 'fmb_A_n_vec$_1' )
      | ( X = 'fmb_A_n_vec$_2' ) ) ).

tff('distinct_domain_A_n_vec$',axiom,
    'fmb_A_n_vec$_1' != 'fmb_A_n_vec$_2' ).

tff('declare_A_b_vec_b_vec_n_vec$',type,
    'A_b_vec_b_vec_n_vec$': $tType ).

tff('declare_A_b_vec_b_vec_n_vec$1',type,
    'fmb_A_b_vec_b_vec_n_vec$_1': 'A_b_vec_b_vec_n_vec$' ).

tff('finite_domain_A_b_vec_b_vec_n_vec$',axiom,
    ! [X: 'A_b_vec_b_vec_n_vec$'] : ( X = 'fmb_A_b_vec_b_vec_n_vec$_1' ) ).

tff('declare_A_n_vec_a_n_vec_fun$',type,
    'A_n_vec_a_n_vec_fun$': $tType ).

tff('declare_A_n_vec_a_n_vec_fun$1',type,
    'fmb_A_n_vec_a_n_vec_fun$_1': 'A_n_vec_a_n_vec_fun$' ).

tff('declare_A_n_vec_a_n_vec_fun$2',type,
    'fmb_A_n_vec_a_n_vec_fun$_2': 'A_n_vec_a_n_vec_fun$' ).

tff('finite_domain_A_n_vec_a_n_vec_fun$',axiom,
    ! [X: 'A_n_vec_a_n_vec_fun$'] :
      ( ( X = 'fmb_A_n_vec_a_n_vec_fun$_1' )
      | ( X = 'fmb_A_n_vec_a_n_vec_fun$_2' ) ) ).

tff('distinct_domain_A_n_vec_a_n_vec_fun$',axiom,
    'fmb_A_n_vec_a_n_vec_fun$_1' != 'fmb_A_n_vec_a_n_vec_fun$_2' ).

tff('declare_B_a_n_vec_fun$',type,
    'B_a_n_vec_fun$': $tType ).

tff('declare_B_a_n_vec_fun$1',type,
    'fmb_B_a_n_vec_fun$_1': 'B_a_n_vec_fun$' ).

tff('declare_B_a_n_vec_fun$2',type,
    'fmb_B_a_n_vec_fun$_2': 'B_a_n_vec_fun$' ).

tff('finite_domain_B_a_n_vec_fun$',axiom,
    ! [X: 'B_a_n_vec_fun$'] :
      ( ( X = 'fmb_B_a_n_vec_fun$_1' )
      | ( X = 'fmb_B_a_n_vec_fun$_2' ) ) ).

tff('distinct_domain_B_a_n_vec_fun$',axiom,
    'fmb_B_a_n_vec_fun$_1' != 'fmb_B_a_n_vec_fun$_2' ).

tff('declare_A_a_fun$',type,
    'A_a_fun$': $tType ).

tff('declare_A_a_fun$1',type,
    'fmb_A_a_fun$_1': 'A_a_fun$' ).

tff('declare_A_a_fun$2',type,
    'fmb_A_a_fun$_2': 'A_a_fun$' ).

tff('finite_domain_A_a_fun$',axiom,
    ! [X: 'A_a_fun$'] :
      ( ( X = 'fmb_A_a_fun$_1' )
      | ( X = 'fmb_A_a_fun$_2' ) ) ).

tff('distinct_domain_A_a_fun$',axiom,
    'fmb_A_a_fun$_1' != 'fmb_A_a_fun$_2' ).

tff('declare_A_b_vec_n_vec_n_vec_n_vec$',type,
    'A_b_vec_n_vec_n_vec_n_vec$': $tType ).

tff('declare_A_b_vec_n_vec_n_vec_n_vec$1',type,
    'fmb_A_b_vec_n_vec_n_vec_n_vec$_1': 'A_b_vec_n_vec_n_vec_n_vec$' ).

tff('declare_A_b_vec_n_vec_n_vec_n_vec$2',type,
    'fmb_A_b_vec_n_vec_n_vec_n_vec$_2': 'A_b_vec_n_vec_n_vec_n_vec$' ).

tff('finite_domain_A_b_vec_n_vec_n_vec_n_vec$',axiom,
    ! [X: 'A_b_vec_n_vec_n_vec_n_vec$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_n_vec_n_vec$',axiom,
    'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' != 'fmb_A_b_vec_n_vec_n_vec_n_vec$_2' ).

tff('declare_A_n_vec_n_vec_n_vec$',type,
    'A_n_vec_n_vec_n_vec$': $tType ).

tff('declare_A_n_vec_n_vec_n_vec$1',type,
    'fmb_A_n_vec_n_vec_n_vec$_1': 'A_n_vec_n_vec_n_vec$' ).

tff('declare_A_n_vec_n_vec_n_vec$2',type,
    'fmb_A_n_vec_n_vec_n_vec$_2': 'A_n_vec_n_vec_n_vec$' ).

tff('finite_domain_A_n_vec_n_vec_n_vec$',axiom,
    ! [X: 'A_n_vec_n_vec_n_vec$'] :
      ( ( X = 'fmb_A_n_vec_n_vec_n_vec$_1' )
      | ( X = 'fmb_A_n_vec_n_vec_n_vec$_2' ) ) ).

tff('distinct_domain_A_n_vec_n_vec_n_vec$',axiom,
    'fmb_A_n_vec_n_vec_n_vec$_1' != 'fmb_A_n_vec_n_vec_n_vec$_2' ).

tff('declare_A_b_vec_a_fun$',type,
    'A_b_vec_a_fun$': $tType ).

tff('declare_A_b_vec_a_fun$1',type,
    'fmb_A_b_vec_a_fun$_1': 'A_b_vec_a_fun$' ).

tff('declare_A_b_vec_a_fun$2',type,
    'fmb_A_b_vec_a_fun$_2': 'A_b_vec_a_fun$' ).

tff('finite_domain_A_b_vec_a_fun$',axiom,
    ! [X: 'A_b_vec_a_fun$'] :
      ( ( X = 'fmb_A_b_vec_a_fun$_1' )
      | ( X = 'fmb_A_b_vec_a_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_a_fun$',axiom,
    'fmb_A_b_vec_a_fun$_1' != 'fmb_A_b_vec_a_fun$_2' ).

tff('declare_A_b_vec_bool_fun$',type,
    'A_b_vec_bool_fun$': $tType ).

tff('declare_A_b_vec_bool_fun$1',type,
    'fmb_A_b_vec_bool_fun$_1': 'A_b_vec_bool_fun$' ).

tff('declare_A_b_vec_bool_fun$2',type,
    'fmb_A_b_vec_bool_fun$_2': 'A_b_vec_bool_fun$' ).

tff('finite_domain_A_b_vec_bool_fun$',axiom,
    ! [X: 'A_b_vec_bool_fun$'] :
      ( ( X = 'fmb_A_b_vec_bool_fun$_1' )
      | ( X = 'fmb_A_b_vec_bool_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_bool_fun$',axiom,
    'fmb_A_b_vec_bool_fun$_1' != 'fmb_A_b_vec_bool_fun$_2' ).

tff('declare_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$',type,
    'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$': $tType ).

tff('declare_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$1',type,
    'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1': 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' ).

tff('declare_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$2',type,
    'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2': 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' ).

tff('finite_domain_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$',axiom,
    ! [X: 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$'] :
      ( ( X = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1' )
      | ( X = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$',axiom,
    'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1' != 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2' ).

tff('declare_A_n_vec_bool_fun$',type,
    'A_n_vec_bool_fun$': $tType ).

tff('declare_A_n_vec_bool_fun$1',type,
    'fmb_A_n_vec_bool_fun$_1': 'A_n_vec_bool_fun$' ).

tff('declare_A_n_vec_bool_fun$2',type,
    'fmb_A_n_vec_bool_fun$_2': 'A_n_vec_bool_fun$' ).

tff('finite_domain_A_n_vec_bool_fun$',axiom,
    ! [X: 'A_n_vec_bool_fun$'] :
      ( ( X = 'fmb_A_n_vec_bool_fun$_1' )
      | ( X = 'fmb_A_n_vec_bool_fun$_2' ) ) ).

tff('distinct_domain_A_n_vec_bool_fun$',axiom,
    'fmb_A_n_vec_bool_fun$_1' != 'fmb_A_n_vec_bool_fun$_2' ).

tff('declare_N_n_bool_fun_fun$',type,
    'N_n_bool_fun_fun$': $tType ).

tff('declare_N_n_bool_fun_fun$1',type,
    'fmb_N_n_bool_fun_fun$_1': 'N_n_bool_fun_fun$' ).

tff('declare_N_n_bool_fun_fun$2',type,
    'fmb_N_n_bool_fun_fun$_2': 'N_n_bool_fun_fun$' ).

tff('finite_domain_N_n_bool_fun_fun$',axiom,
    ! [X: 'N_n_bool_fun_fun$'] :
      ( ( X = 'fmb_N_n_bool_fun_fun$_1' )
      | ( X = 'fmb_N_n_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_N_n_bool_fun_fun$',axiom,
    'fmb_N_n_bool_fun_fun$_1' != 'fmb_N_n_bool_fun_fun$_2' ).

tff('declare_B_a_bool_fun_fun$',type,
    'B_a_bool_fun_fun$': $tType ).

tff('declare_B_a_bool_fun_fun$1',type,
    'fmb_B_a_bool_fun_fun$_1': 'B_a_bool_fun_fun$' ).

tff('declare_B_a_bool_fun_fun$2',type,
    'fmb_B_a_bool_fun_fun$_2': 'B_a_bool_fun_fun$' ).

tff('finite_domain_B_a_bool_fun_fun$',axiom,
    ! [X: 'B_a_bool_fun_fun$'] :
      ( ( X = 'fmb_B_a_bool_fun_fun$_1' )
      | ( X = 'fmb_B_a_bool_fun_fun$_2' ) ) ).

tff('distinct_domain_B_a_bool_fun_fun$',axiom,
    'fmb_B_a_bool_fun_fun$_1' != 'fmb_B_a_bool_fun_fun$_2' ).

tff('declare_N_bool_fun$',type,
    'N_bool_fun$': $tType ).

tff('declare_N_bool_fun$1',type,
    'fmb_N_bool_fun$_1': 'N_bool_fun$' ).

tff('declare_N_bool_fun$2',type,
    'fmb_N_bool_fun$_2': 'N_bool_fun$' ).

tff('finite_domain_N_bool_fun$',axiom,
    ! [X: 'N_bool_fun$'] :
      ( ( X = 'fmb_N_bool_fun$_1' )
      | ( X = 'fmb_N_bool_fun$_2' ) ) ).

tff('distinct_domain_N_bool_fun$',axiom,
    'fmb_N_bool_fun$_1' != 'fmb_N_bool_fun$_2' ).

tff('declare_N_a_b_vec_n_vec_fun$',type,
    'N_a_b_vec_n_vec_fun$': $tType ).

tff('declare_N_a_b_vec_n_vec_fun$1',type,
    'fmb_N_a_b_vec_n_vec_fun$_1': 'N_a_b_vec_n_vec_fun$' ).

tff('declare_N_a_b_vec_n_vec_fun$2',type,
    'fmb_N_a_b_vec_n_vec_fun$_2': 'N_a_b_vec_n_vec_fun$' ).

tff('finite_domain_N_a_b_vec_n_vec_fun$',axiom,
    ! [X: 'N_a_b_vec_n_vec_fun$'] :
      ( ( X = 'fmb_N_a_b_vec_n_vec_fun$_1' )
      | ( X = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_b_vec_n_vec_fun$',axiom,
    'fmb_N_a_b_vec_n_vec_fun$_1' != 'fmb_N_a_b_vec_n_vec_fun$_2' ).

tff('declare_N_a_n_vec_n_vec_fun$',type,
    'N_a_n_vec_n_vec_fun$': $tType ).

tff('declare_N_a_n_vec_n_vec_fun$1',type,
    'fmb_N_a_n_vec_n_vec_fun$_1': 'N_a_n_vec_n_vec_fun$' ).

tff('declare_N_a_n_vec_n_vec_fun$2',type,
    'fmb_N_a_n_vec_n_vec_fun$_2': 'N_a_n_vec_n_vec_fun$' ).

tff('finite_domain_N_a_n_vec_n_vec_fun$',axiom,
    ! [X: 'N_a_n_vec_n_vec_fun$'] :
      ( ( X = 'fmb_N_a_n_vec_n_vec_fun$_1' )
      | ( X = 'fmb_N_a_n_vec_n_vec_fun$_2' ) ) ).

tff('distinct_domain_N_a_n_vec_n_vec_fun$',axiom,
    'fmb_N_a_n_vec_n_vec_fun$_1' != 'fmb_N_a_n_vec_n_vec_fun$_2' ).

tff('declare_less$',type,
    'less$': 'N_n_bool_fun_fun$' ).

tff('less$_definition',axiom,
    'less$' = 'fmb_N_n_bool_fun_fun$_1' ).

tff('declare_one$c',type,
    'one$c': 'A_b_vec$' ).

tff('one$c_definition',axiom,
    'one$c' = 'fmb_A_b_vec$_1' ).

tff('declare_a$a',type,
    'a$a': 'A_b_vec_n_vec$' ).

tff('a$a_definition',axiom,
    'a$a' = 'fmb_A_b_vec_n_vec$_1' ).

tff('declare_uwc$',type,
    'uwc$': 'N_a_b_vec_fun$' ).

tff('uwc$_definition',axiom,
    'uwc$' = 'fmb_N_a_b_vec_fun$_1' ).

tff('declare_one$d',type,
    'one$d': 'A_b_vec_n_vec_n_vec$' ).

tff('one$d_definition',axiom,
    'one$d' = 'fmb_A_b_vec_n_vec_n_vec$_1' ).

tff('declare_m$',type,
    'm$': 'N$' ).

tff('m$_definition',axiom,
    'm$' = 'fmb_N$_1' ).

tff('declare_zero$b',type,
    'zero$b': 'A_b_vec_n_vec$' ).

tff('zero$b_definition',axiom,
    'zero$b' = 'fmb_A_b_vec_n_vec$_1' ).

tff('declare_zero$c',type,
    'zero$c': 'A_n_vec$' ).

tff('zero$c_definition',axiom,
    'zero$c' = 'fmb_A_n_vec$_1' ).

tff('declare_uvu$',type,
    'uvu$': 'B_a_fun$' ).

tff('uvu$_definition',axiom,
    'uvu$' = 'fmb_B_a_fun$_1' ).

tff('declare_zero$e',type,
    'zero$e': 'A_n_vec_n_vec$' ).

tff('zero$e_definition',axiom,
    'zero$e' = 'fmb_A_n_vec_n_vec$_1' ).

tff('declare_uvz$',type,
    'uvz$': 'B_a_b_vec_fun$' ).

tff('uvz$_definition',axiom,
    'uvz$' = 'fmb_B_a_b_vec_fun$_1' ).

tff('declare_uxu$',type,
    'uxu$': 'A_n_vec_a_n_vec_fun$' ).

tff('uxu$_definition',axiom,
    'uxu$' = 'fmb_A_n_vec_a_n_vec_fun$_1' ).

tff('declare_i$',type,
    'i$': 'N$' ).

tff('i$_definition',axiom,
    'i$' = 'fmb_N$_1' ).

tff('declare_n$',type,
    'n$': 'N$' ).

tff('n$_definition',axiom,
    'n$' = 'fmb_N$_1' ).

tff('declare_uxp$',type,
    'uxp$': 'A_n_vec_a_n_vec_fun$' ).

tff('uxp$_definition',axiom,
    'uxp$' = 'fmb_A_n_vec_a_n_vec_fun$_2' ).

tff('declare_zero$d',type,
    'zero$d': 'A_b_vec$' ).

tff('zero$d_definition',axiom,
    'zero$d' = 'fmb_A_b_vec$_2' ).

tff('declare_uxx$',type,
    'uxx$': 'A_b_vec_a_b_vec_fun$' ).

tff('uxx$_definition',axiom,
    'uxx$' = 'fmb_A_b_vec_a_b_vec_fun$_1' ).

tff('declare_uminus$c',type,
    'uminus$c': 'A_a_fun$' ).

tff('uminus$c_definition',axiom,
    'uminus$c' = 'fmb_A_a_fun$_1' ).

tff('declare_uxt$',type,
    'uxt$': 'A_a_fun$' ).

tff('uxt$_definition',axiom,
    'uxt$' = 'fmb_A_a_fun$_1' ).

tff('declare_one$',type,
    'one$': 'A$' ).

tff('one$_definition',axiom,
    'one$' = 'fmb_A$_1' ).

tff('declare_uvy$',type,
    'uvy$': 'N_a_n_vec_fun$' ).

tff('uvy$_definition',axiom,
    'uvy$' = 'fmb_N_a_n_vec_fun$_1' ).

tff('declare_uwa$',type,
    'uwa$': 'B_a_fun$' ).

tff('uwa$_definition',axiom,
    'uwa$' = 'fmb_B_a_fun$_2' ).

tff('declare_a$',type,
    'a$': 'A_b_vec_n_vec$' ).

tff('a$_definition',axiom,
    'a$' = 'fmb_A_b_vec_n_vec$_2' ).

tff('declare_uvv$',type,
    'uvv$': 'N_a_b_vec_n_vec_fun$' ).

tff('uvv$_definition',axiom,
    'uvv$' = 'fmb_N_a_b_vec_n_vec_fun$_1' ).

tff(declare_tltrue,type,
    tltrue: tlbool ).

tff(tltrue_definition,axiom,
    tltrue = fmb_tlbool_1 ).

tff('declare_less_eq$',type,
    'less_eq$': 'N_n_bool_fun_fun$' ).

tff('less_eq$_definition',axiom,
    'less_eq$' = 'fmb_N_n_bool_fun_fun$_2' ).

tff('declare_uwb$',type,
    'uwb$': 'N_a_b_vec_n_vec_fun$' ).

tff('uwb$_definition',axiom,
    'uwb$' = 'fmb_N_a_b_vec_n_vec_fun$_2' ).

tff('declare_j$',type,
    'j$': 'B$' ).

tff('j$_definition',axiom,
    'j$' = 'fmb_B$_1' ).

tff('declare_uvr$',type,
    'uvr$': 'N_a_fun$' ).

tff('uvr$_definition',axiom,
    'uvr$' = 'fmb_N_a_fun$_1' ).

tff('declare_uxs$',type,
    'uxs$': 'A_b_vec_a_b_vec_fun$' ).

tff('uxs$_definition',axiom,
    'uxs$' = 'fmb_A_b_vec_a_b_vec_fun$_2' ).

tff('declare_uvw$',type,
    'uvw$': 'N_a_b_vec_fun$' ).

tff('uvw$_definition',axiom,
    'uvw$' = 'fmb_N_a_b_vec_fun$_2' ).

tff('declare_one$b',type,
    'one$b': 'A_n_vec$' ).

tff('one$b_definition',axiom,
    'one$b' = 'fmb_A_n_vec$_2' ).

tff('declare_uu$',type,
    'uu$': 'N_bool_fun$' ).

tff('uu$_definition',axiom,
    'uu$' = 'fmb_N_bool_fun$_1' ).

tff('declare_uxy$',type,
    'uxy$': 'A_a_fun$' ).

tff('uxy$_definition',axiom,
    'uxy$' = 'fmb_A_a_fun$_2' ).

tff('declare_uvt$',type,
    'uvt$': 'B_a_b_vec_fun$' ).

tff('uvt$_definition',axiom,
    'uvt$' = 'fmb_B_a_b_vec_fun$_2' ).

tff('declare_uvs$',type,
    'uvs$': 'N_a_n_vec_fun$' ).

tff('uvs$_definition',axiom,
    'uvs$' = 'fmb_N_a_n_vec_fun$_2' ).

tff('declare_one$a',type,
    'one$a': 'A_b_vec_n_vec$' ).

tff('one$a_definition',axiom,
    'one$a' = 'fmb_A_b_vec_n_vec$_2' ).

tff('declare_uxv$',type,
    'uxv$': 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' ).

tff('uxv$_definition',axiom,
    'uxv$' = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1' ).

tff('declare_one$f',type,
    'one$f': 'A_b_vec_b_vec$' ).

tff('one$f_definition',axiom,
    'one$f' = 'fmb_A_b_vec_b_vec$_1' ).

tff('declare_zero$',type,
    'zero$': 'A$' ).

tff('zero$_definition',axiom,
    'zero$' = 'fmb_A$_2' ).

tff('declare_interchange_A$',type,
    'interchange_A$': 'A_b_vec_n_vec$' ).

tff('interchange_A$_definition',axiom,
    'interchange_A$' = 'fmb_A_b_vec_n_vec$_2' ).

tff('declare_uvx$',type,
    'uvx$': 'N_a_fun$' ).

tff('uvx$_definition',axiom,
    'uvx$' = 'fmb_N_a_fun$_2' ).

tff(declare_tlfalse,type,
    tlfalse: tlbool ).

tff(tlfalse_definition,axiom,
    tlfalse = fmb_tlbool_2 ).

tff('declare_zero$a',type,
    'zero$a': 'A_b_vec_n_vec_n_vec$' ).

tff('zero$a_definition',axiom,
    'zero$a' = 'fmb_A_b_vec_n_vec_n_vec$_2' ).

tff('declare_uminus$b',type,
    'uminus$b': 'A_b_vec_a_b_vec_fun$' ).

tff('uminus$b_definition',axiom,
    'uminus$b' = 'fmb_A_b_vec_a_b_vec_fun$_2' ).

tff('declare_uxr$',type,
    'uxr$': 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' ).

tff('uxr$_definition',axiom,
    'uxr$' = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1' ).

tff('declare_uxq$',type,
    'uxq$': 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' ).

tff('uxq$_definition',axiom,
    'uxq$' = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2' ).

tff('declare_zero$f',type,
    'zero$f': 'A_b_vec_b_vec$' ).

tff('zero$f_definition',axiom,
    'zero$f' = 'fmb_A_b_vec_b_vec$_2' ).

tff('declare_one$e',type,
    'one$e': 'A_n_vec_n_vec$' ).

tff('one$e_definition',axiom,
    'one$e' = 'fmb_A_n_vec_n_vec$_2' ).

tff('declare_uxw$',type,
    'uxw$': 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' ).

tff('uxw$_definition',axiom,
    'uxw$' = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2' ).

tff('declare_uul$',type,
    'uul$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uul$',axiom,
    ( ( 'uul$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uul$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_times$b',type,
    'times$b': 'A_b_vec$' > 'A_b_vec_a_b_vec_fun$' ).

tff('function_times$b',axiom,
    ( ( 'times$b'('fmb_A_b_vec$_1') = 'fmb_A_b_vec_a_b_vec_fun$_1' )
    & ( 'times$b'('fmb_A_b_vec$_2') = 'fmb_A_b_vec_a_b_vec_fun$_2' ) ) ).

tff('declare_uwy$',type,
    'uwy$': 'A_b_vec_n_vec$' > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uwy$',axiom,
    ( ( 'uwy$'('fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uwy$'('fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_interchange_columns$a',type,
    'interchange_columns$a': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_interchange_columns$a',axiom,
    ( ( 'interchange_columns$a'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'interchange_columns$a'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_uwg$',type,
    'uwg$': ( 'A_b_vec_n_vec$' * 'N$' * 'B$' ) > 'N_a_b_vec_fun$' ).

tff('function_uwg$',axiom,
    ( ( 'uwg$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uwg$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_fun_app$p',type,
    'fun_app$p': ( 'A_n_vec_a_n_vec_fun$' * 'A_n_vec$' ) > 'A_n_vec$' ).

tff('function_fun_app$p',axiom,
    ( ( 'fun_app$p'('fmb_A_n_vec_a_n_vec_fun$_1','fmb_A_n_vec$_1') = 'fmb_A_n_vec$_1' )
    & ( 'fun_app$p'('fmb_A_n_vec_a_n_vec_fun$_1','fmb_A_n_vec$_2') = 'fmb_A_n_vec$_2' )
    & ( 'fun_app$p'('fmb_A_n_vec_a_n_vec_fun$_2','fmb_A_n_vec$_1') = 'fmb_A_n_vec$_1' )
    & ( 'fun_app$p'('fmb_A_n_vec_a_n_vec_fun$_2','fmb_A_n_vec$_2') = 'fmb_A_n_vec$_1' ) ) ).

tff('declare_uxm$',type,
    'uxm$': ( 'A_b_vec_n_vec_n_vec$' * 'A_b_vec_n_vec_n_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uxm$',axiom,
    ( ( 'uxm$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uxm$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uxm$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uxm$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uvk$',type,
    'uvk$': ( 'A_a_b_vec_fun$' * 'A_b_vec_n_vec$' ) > 'N_a_b_vec_b_vec_fun$' ).

tff('function_uvk$',axiom,
    ( ( 'uvk$'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_b_vec_fun$_2' )
    & ( 'uvk$'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_b_vec_fun$_2' )
    & ( 'uvk$'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_b_vec_fun$_2' )
    & ( 'uvk$'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_b_vec_fun$_2' ) ) ).

tff('declare_uxg$',type,
    'uxg$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'A_b_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uxg$',axiom,
    ( ( 'uxg$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uxg$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uxg$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uxg$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uwl$',type,
    'uwl$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uwl$',axiom,
    ( ( 'uwl$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uwl$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uvm$',type,
    'uvm$': ( 'A_b_vec_a_fun$' * 'A_b_vec_n_vec_n_vec$' ) > 'N_a_n_vec_fun$' ).

tff('function_uvm$',axiom,
    ( ( 'uvm$'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvm$'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvm$'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvm$'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_uuk$',type,
    'uuk$': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' ) > 'B_a_b_vec_fun$' ).

tff('function_uuk$',axiom,
    ( ( 'uuk$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uuk$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_interchange_columns_row$',type,
    'interchange_columns_row$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_interchange_columns_row$',axiom,
    ( ( 'interchange_columns_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'interchange_columns_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uminus$e',type,
    'uminus$e': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).

tff('function_uminus$e',axiom,
    ( ( 'uminus$e'('fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'uminus$e'('fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_uub$',type,
    'uub$': 'A_n_vec_n_vec$' > 'N_a_n_vec_fun$' ).

tff('function_uub$',axiom,
    ( ( 'uub$'('fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uub$'('fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_uminus$f',type,
    'uminus$f': 'A_b_vec_b_vec$' > 'A_b_vec_b_vec$' ).

tff('function_uminus$f',axiom,
    ( ( 'uminus$f'('fmb_A_b_vec_b_vec$_1') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'uminus$f'('fmb_A_b_vec_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_uvq$',type,
    'uvq$': ( 'A_a_b_vec_n_vec_fun$' * 'A_n_vec_n_vec$' ) > 'N_a_b_vec_n_vec_n_vec_fun$' ).

tff('function_uvq$',axiom,
    ( ( 'uvq$'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' )
    & ( 'uvq$'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_1' )
    & ( 'uvq$'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' )
    & ( 'uvq$'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('declare_interchange_rows_row$b',type,
    'interchange_rows_row$b': ( 'A_b_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_interchange_rows_row$b',axiom,
    ( ( 'interchange_rows_row$b'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'interchange_rows_row$b'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uva$',type,
    'uva$': ( 'A_a_b_vec_fun$' * 'A_n_vec_n_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uva$',axiom,
    ( ( 'uva$'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uva$'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uva$'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uva$'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_uup$',type,
    'uup$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uup$',axiom,
    ( ( 'uup$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uup$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_fun_app$k',type,
    'fun_app$k': ( 'A_b_vec_a_b_vec_fun$' * 'A_b_vec$' ) > 'A_b_vec$' ).

tff('function_fun_app$k',axiom,
    ( ( 'fun_app$k'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec$_1') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$k'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec$_2') = 'fmb_A_b_vec$_2' )
    & ( 'fun_app$k'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec$_1') = 'fmb_A_b_vec$_2' )
    & ( 'fun_app$k'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec$_2') = 'fmb_A_b_vec$_2' ) ) ).

tff('declare_columnvector$g',type,
    'columnvector$g': 'A_n_vec$' > 'A_b_vec_n_vec$' ).

tff('function_columnvector$g',axiom,
    ( ( 'columnvector$g'('fmb_A_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'columnvector$g'('fmb_A_n_vec$_2') = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('declare_row_add_row$',type,
    'row_add_row$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' * 'A_b_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_row_add_row$',axiom,
    ( ( 'row_add_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'row_add_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'row_add_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'row_add_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_uxf$',type,
    'uxf$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'A_b_vec$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uxf$',axiom,
    ( ( 'uxf$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uxf$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxf$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxf$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_uuy$',type,
    'uuy$': ( 'A_a_fun$' * 'A_b_vec_n_vec$' ) > 'N_a_b_vec_fun$' ).

tff('function_uuy$',axiom,
    ( ( 'uuy$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uuy$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uuy$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uuy$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uwm$',type,
    'uwm$': 'A_b_vec_n_vec_n_vec$' > 'N_a_b_vec_n_vec_n_vec_fun$' ).

tff('function_uwm$',axiom,
    ( ( 'uwm$'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_1' )
    & ( 'uwm$'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('declare_least$',type,
    'least$': 'N_bool_fun$' > 'N$' ).

tff('function_least$',axiom,
    ( ( 'least$'('fmb_N_bool_fun$_1') = 'fmb_N$_1' )
    & ( 'least$'('fmb_N_bool_fun$_2') = 'fmb_N$_1' ) ) ).

tff('declare_fun_app$ad',type,
    'fun_app$ad': ( 'B_a_bool_fun_fun$' * 'B$' ) > 'A_bool_fun$' ).

tff('function_fun_app$ad',axiom,
    ( ( 'fun_app$ad'('fmb_B_a_bool_fun_fun$_1','fmb_B$_1') = 'fmb_A_bool_fun$_2' )
    & ( 'fun_app$ad'('fmb_B_a_bool_fun_fun$_2','fmb_B$_1') = 'fmb_A_bool_fun$_2' ) ) ).

tff('declare_map_matrix$h',type,
    'map_matrix$h': ( 'A_b_vec_n_vec_a_fun$' * 'A_b_vec_n_vec_n_vec_n_vec$' ) > 'A_n_vec_n_vec$' ).

tff('function_map_matrix$h',axiom,
    ( ( 'map_matrix$h'('fmb_A_b_vec_n_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$h'('fmb_A_b_vec_n_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$h'('fmb_A_b_vec_n_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$h'('fmb_A_b_vec_n_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_uwf$',type,
    'uwf$': ( 'A_b_vec_n_vec$' * 'N$' * 'B$' ) > 'N_bool_fun$' ).

tff('function_uwf$',axiom,
    ( ( 'uwf$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_B$_1') = 'fmb_N_bool_fun$_2' )
    & ( 'uwf$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_B$_1') = 'fmb_N_bool_fun$_1' ) ) ).

tff('declare_vec_lambda$f',type,
    'vec_lambda$f': 'N_a_n_vec_n_vec_fun$' > 'A_n_vec_n_vec_n_vec$' ).

tff('function_vec_lambda$f',axiom,
    ( ( 'vec_lambda$f'('fmb_N_a_n_vec_n_vec_fun$_1') = 'fmb_A_n_vec_n_vec_n_vec$_2' )
    & ( 'vec_lambda$f'('fmb_N_a_n_vec_n_vec_fun$_2') = 'fmb_A_n_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_mult_row$b',type,
    'mult_row$b': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'A_b_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_mult_row$b',axiom,
    ( ( 'mult_row$b'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'mult_row$b'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'mult_row$b'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'mult_row$b'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_uvg$',type,
    'uvg$': ( 'A_a_fun$' * 'A_b_vec_b_vec$' ) > 'B_a_b_vec_fun$' ).

tff('function_uvg$',axiom,
    ( ( 'uvg$'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uvg$'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uvg$'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uvg$'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_rowvector$b',type,
    'rowvector$b': 'A_b_vec_n_vec$' > 'A_b_vec_n_vec_n_vec$' ).

tff('function_rowvector$b',axiom,
    ( ( 'rowvector$b'('fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'rowvector$b'('fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_uum$',type,
    'uum$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uum$',axiom,
    ( ( 'uum$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uum$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uxl$',type,
    'uxl$': ( 'A_n_vec$' * 'A_n_vec$' ) > 'N_a_fun$' ).

tff('function_uxl$',axiom,
    ( ( 'uxl$'('fmb_A_n_vec$_1','fmb_A_n_vec$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uxl$'('fmb_A_n_vec$_1','fmb_A_n_vec$_2') = 'fmb_N_a_fun$_1' )
    & ( 'uxl$'('fmb_A_n_vec$_2','fmb_A_n_vec$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uxl$'('fmb_A_n_vec$_2','fmb_A_n_vec$_2') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_uux$',type,
    'uux$': ( 'A_a_fun$' * 'A_b_vec_n_vec$' * 'N$' ) > 'B_a_fun$' ).

tff('function_uux$',axiom,
    ( ( 'uux$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uux$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uux$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uux$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_B_a_fun$_2' ) ) ).

tff('declare_times$e',type,
    'times$e': ( 'A_n_vec_n_vec$' * 'A_n_vec_n_vec$' ) > 'A_n_vec_n_vec$' ).

tff('function_times$e',axiom,
    ( ( 'times$e'('fmb_A_n_vec_n_vec$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'times$e'('fmb_A_n_vec_n_vec$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'times$e'('fmb_A_n_vec_n_vec$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'times$e'('fmb_A_n_vec_n_vec$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_row_add_row$b',type,
    'row_add_row$b': ( 'A_b_vec_n_vec$' * 'N$' * 'N$' * 'A$' ) > 'N_a_b_vec_fun$' ).

tff('function_row_add_row$b',axiom,
    ( ( 'row_add_row$b'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'row_add_row$b'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'row_add_row$b'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'row_add_row$b'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_uud$',type,
    'uud$': 'A_n_vec$' > 'N_a_fun$' ).

tff('function_uud$',axiom,
    ( ( 'uud$'('fmb_A_n_vec$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uud$'('fmb_A_n_vec$_2') = 'fmb_N_a_fun$_1' ) ) ).

tff('declare_interchange_rows$',type,
    'interchange_rows$': ( 'A_b_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_interchange_rows$',axiom,
    ( ( 'interchange_rows$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'interchange_rows$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_fun_app$g',type,
    'fun_app$g': ( 'N_a_b_vec_b_vec_fun$' * 'N$' ) > 'A_b_vec_b_vec$' ).

tff('function_fun_app$g',axiom,
    ( ( 'fun_app$g'('fmb_N_a_b_vec_b_vec_fun$_1','fmb_N$_1') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'fun_app$g'('fmb_N_a_b_vec_b_vec_fun$_2','fmb_N$_1') = 'fmb_A_b_vec_b_vec$_1' ) ) ).

tff('declare_uvn$',type,
    'uvn$': ( 'A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uvn$',axiom,
    ( ( 'uvn$'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_2' )
    & ( 'uvn$'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_2' )
    & ( 'uvn$'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_2' )
    & ( 'uvn$'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_uuc$',type,
    'uuc$': 'A_b_vec_b_vec$' > 'B_a_b_vec_fun$' ).

tff('function_uuc$',axiom,
    ( ( 'uuc$'('fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uuc$'('fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_uue$',type,
    'uue$': 'A_b_vec_n_vec_n_vec$' > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uue$',axiom,
    ( ( 'uue$'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uue$'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uvp$',type,
    'uvp$': ( 'A_a_b_vec_n_vec_fun$' * 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uvp$',axiom,
    ( ( 'uvp$'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uvp$'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uvp$'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uvp$'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uua$',type,
    'uua$': ( 'A_b_vec_n_vec$' * 'A_b_vec_n_vec$' ) > 'N_a_b_vec_fun$' ).

tff('function_uua$',axiom,
    ( ( 'uua$'('fmb_A_b_vec_n_vec$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uua$'('fmb_A_b_vec_n_vec$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uua$'('fmb_A_b_vec_n_vec$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uua$'('fmb_A_b_vec_n_vec$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uvi$',type,
    'uvi$': ( 'A_a_n_vec_fun$' * 'A_n_vec_n_vec$' ) > 'N_a_n_vec_n_vec_fun$' ).

tff('function_uvi$',axiom,
    ( ( 'uvi$'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_n_vec_fun$_2' )
    & ( 'uvi$'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_n_vec_fun$_2' )
    & ( 'uvi$'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_n_vec_fun$_2' )
    & ( 'uvi$'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_n_vec_fun$_2' ) ) ).

tff('declare_interchange_columns_row$b',type,
    'interchange_columns_row$b': ( 'A_b_vec_n_vec$' * 'B$' * 'B$' ) > 'N_a_b_vec_fun$' ).

tff('function_interchange_columns_row$b',axiom,
    ( ( 'interchange_columns_row$b'('fmb_A_b_vec_n_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'interchange_columns_row$b'('fmb_A_b_vec_n_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uxo$',type,
    'uxo$': ( 'A_b_vec_n_vec$' * 'A_b_vec_n_vec$' ) > 'N_a_b_vec_fun$' ).

tff('function_uxo$',axiom,
    ( ( 'uxo$'('fmb_A_b_vec_n_vec$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxo$'('fmb_A_b_vec_n_vec$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxo$'('fmb_A_b_vec_n_vec$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxo$'('fmb_A_b_vec_n_vec$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uwn$',type,
    'uwn$': ( 'A_b_vec$' * 'B$' ) > 'N_a_fun$' ).

tff('function_uwn$',axiom,
    ( ( 'uwn$'('fmb_A_b_vec$_1','fmb_B$_1') = 'fmb_N_a_fun$_2' )
    & ( 'uwn$'('fmb_A_b_vec$_2','fmb_B$_1') = 'fmb_N_a_fun$_1' ) ) ).

tff('declare_columnvector$',type,
    'columnvector$': 'A_b_vec_n_vec_n_vec$' > 'A_b_vec_n_vec_n_vec_n_vec$' ).

tff('function_columnvector$',axiom,
    ( ( 'columnvector$'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_2' )
    & ( 'columnvector$'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_map_matrix$a',type,
    'map_matrix$a': ( 'A_a_fun$' * 'A_n_vec_n_vec$' ) > 'A_n_vec_n_vec$' ).

tff('function_map_matrix$a',axiom,
    ( ( 'map_matrix$a'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$a'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$a'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$a'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_uwi$',type,
    'uwi$': 'A_b_vec$' > 'B_a_b_vec_fun$' ).

tff('function_uwi$',axiom,
    ( ( 'uwi$'('fmb_A_b_vec$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uwi$'('fmb_A_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_map_matrix$e',type,
    'map_matrix$e': ( 'A_a_n_vec_fun$' * 'A_n_vec_n_vec$' ) > 'A_n_vec_n_vec_n_vec$' ).

tff('function_map_matrix$e',axiom,
    ( ( 'map_matrix$e'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$e'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$e'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$e'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_vec_nth$c',type,
    'vec_nth$c': 'A_n_vec_n_vec$' > 'N_a_n_vec_fun$' ).

tff('function_vec_nth$c',axiom,
    ( ( 'vec_nth$c'('fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'vec_nth$c'('fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_fun_app$f',type,
    'fun_app$f': ( 'N_a_n_vec_fun$' * 'N$' ) > 'A_n_vec$' ).

tff('function_fun_app$f',axiom,
    ( ( 'fun_app$f'('fmb_N_a_n_vec_fun$_1','fmb_N$_1') = 'fmb_A_n_vec$_2' )
    & ( 'fun_app$f'('fmb_N_a_n_vec_fun$_2','fmb_N$_1') = 'fmb_A_n_vec$_1' ) ) ).

tff('declare_uvh$',type,
    'uvh$': ( 'A_a_n_vec_fun$' * 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_uvh$',axiom,
    ( ( 'uvh$'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvh$'('fmb_A_a_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvh$'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uvh$'('fmb_A_a_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_vec_nth$a',type,
    'vec_nth$a': 'A_b_vec_n_vec$' > 'N_a_b_vec_fun$' ).

tff('function_vec_nth$a',axiom,
    ( ( 'vec_nth$a'('fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'vec_nth$a'('fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_vec_lambda$e',type,
    'vec_lambda$e': 'N_a_b_vec_n_vec_fun$' > 'A_b_vec_n_vec_n_vec$' ).

tff('function_vec_lambda$e',axiom,
    ( ( 'vec_lambda$e'('fmb_N_a_b_vec_n_vec_fun$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'vec_lambda$e'('fmb_N_a_b_vec_n_vec_fun$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_fun_app$a',type,
    'fun_app$a': ( 'B_a_fun$' * 'B$' ) > 'A$' ).

tff('function_fun_app$a',axiom,
    ( ( 'fun_app$a'('fmb_B_a_fun$_1','fmb_B$_1') = 'fmb_A$_2' )
    & ( 'fun_app$a'('fmb_B_a_fun$_2','fmb_B$_1') = 'fmb_A$_1' ) ) ).

tff('declare_vec_nth$b',type,
    'vec_nth$b': 'A_b_vec_n_vec_n_vec$' > 'N_a_b_vec_n_vec_fun$' ).

tff('function_vec_nth$b',axiom,
    ( ( 'vec_nth$b'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'vec_nth$b'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uxj$',type,
    'uxj$': ( 'A_n_vec_n_vec$' * 'A_n_vec_n_vec$' ) > 'N_a_n_vec_fun$' ).

tff('function_uxj$',axiom,
    ( ( 'uxj$'('fmb_A_n_vec_n_vec$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uxj$'('fmb_A_n_vec_n_vec$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uxj$'('fmb_A_n_vec_n_vec$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uxj$'('fmb_A_n_vec_n_vec$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_vec_lambda$a',type,
    'vec_lambda$a': 'N_a_b_vec_fun$' > 'A_b_vec_n_vec$' ).

tff('function_vec_lambda$a',axiom,
    ( ( 'vec_lambda$a'('fmb_N_a_b_vec_fun$_1') = 'fmb_A_b_vec_n_vec$_2' )
    & ( 'vec_lambda$a'('fmb_N_a_b_vec_fun$_2') = 'fmb_A_b_vec_n_vec$_1' ) ) ).

tff('declare_vec_lambda$',type,
    'vec_lambda$': 'B_a_fun$' > 'A_b_vec$' ).

tff('function_vec_lambda$',axiom,
    ( ( 'vec_lambda$'('fmb_B_a_fun$_1') = 'fmb_A_b_vec$_2' )
    & ( 'vec_lambda$'('fmb_B_a_fun$_2') = 'fmb_A_b_vec$_1' ) ) ).

tff('declare_vec_lambda$i',type,
    'vec_lambda$i': 'B_a_n_vec_fun$' > 'A_n_vec_b_vec$' ).

tff('function_vec_lambda$i',axiom,
    ( ( 'vec_lambda$i'('fmb_B_a_n_vec_fun$_1') = 'fmb_A_n_vec_b_vec$_1' )
    & ( 'vec_lambda$i'('fmb_B_a_n_vec_fun$_2') = 'fmb_A_n_vec_b_vec$_1' ) ) ).

tff('declare_uvo$',type,
    'uvo$': ( 'A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$' ) > 'N_a_n_vec_fun$' ).

tff('function_uvo$',axiom,
    ( ( 'uvo$'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'uvo$'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'uvo$'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'uvo$'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_columnvector$b',type,
    'columnvector$b': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec_n_vec$' ).

tff('function_columnvector$b',axiom,
    ( ( 'columnvector$b'('fmb_A_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec_n_vec$_2' )
    & ( 'columnvector$b'('fmb_A_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_fun_app$q',type,
    'fun_app$q': ( 'A_n_vec_a_fun$' * 'A_n_vec$' ) > 'A$' ).

tff('function_fun_app$q',axiom,
    ( ( 'fun_app$q'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec$_1') = 'fmb_A$_1' )
    & ( 'fun_app$q'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec$_2') = 'fmb_A$_2' )
    & ( 'fun_app$q'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec$_1') = 'fmb_A$_1' )
    & ( 'fun_app$q'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec$_2') = 'fmb_A$_2' ) ) ).

tff('declare_fun_app$j',type,
    'fun_app$j': ( 'N_a_b_vec_n_vec_n_vec_fun$' * 'N$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_fun_app$j',axiom,
    ( ( 'fun_app$j'('fmb_N_a_b_vec_n_vec_n_vec_fun$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'fun_app$j'('fmb_N_a_b_vec_n_vec_n_vec_fun$_2','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_uuv$',type,
    'uuv$': ( 'A_b_vec_n_vec$' * 'N$' * 'N$' * 'N$' ) > 'B_a_fun$' ).

tff('function_uuv$',axiom,
    ( ( 'uuv$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uuv$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_B_a_fun$_2' ) ) ).

tff('declare_fun_app$h',type,
    'fun_app$h': ( 'N_a_n_vec_n_vec_fun$' * 'N$' ) > 'A_n_vec_n_vec$' ).

tff('function_fun_app$h',axiom,
    ( ( 'fun_app$h'('fmb_N_a_n_vec_n_vec_fun$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'fun_app$h'('fmb_N_a_n_vec_n_vec_fun$_2','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_fun_app$o',type,
    'fun_app$o': ( 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' * 'A_b_vec_n_vec$' ) > 'A_b_vec_n_vec$' ).

tff('function_fun_app$o',axiom,
    ( ( 'fun_app$o'('fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$o'('fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$o'('fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$o'('fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('declare_uve$',type,
    'uve$': ( 'A_a_fun$' * 'A_n_vec_n_vec$' ) > 'N_a_n_vec_fun$' ).

tff('function_uve$',axiom,
    ( ( 'uve$'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uve$'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uve$'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uve$'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_times$d',type,
    'times$d': 'A_b_vec_n_vec_n_vec$' > 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' ).

tff('function_times$d',axiom,
    ( ( 'times$d'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1' )
    & ( 'times$d'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('declare_uvj$',type,
    'uvj$': ( 'A_a_b_vec_fun$' * 'A_b_vec_n_vec$' * 'N$' ) > 'B_a_b_vec_fun$' ).

tff('function_uvj$',axiom,
    ( ( 'uvj$'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uvj$'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uvj$'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uvj$'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_1' ) ) ).

tff('declare_uvb$',type,
    'uvb$': ( 'A_b_vec_a_b_vec_fun$' * 'A_b_vec_n_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uvb$',axiom,
    ( ( 'uvb$'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uvb$'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uvb$'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uvb$'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_columnvector$c',type,
    'columnvector$c': 'A_b_vec_n_vec$' > 'A_b_vec_b_vec_n_vec$' ).

tff('function_columnvector$c',axiom,
    ( ( 'columnvector$c'('fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_b_vec_n_vec$_1' )
    & ( 'columnvector$c'('fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_b_vec_n_vec$_1' ) ) ).

tff('declare_uuq$',type,
    'uuq$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_uuq$',axiom,
    ( ( 'uuq$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uuq$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_fun_app$r',type,
    'fun_app$r': ( 'A_b_vec_a_fun$' * 'A_b_vec$' ) > 'A$' ).

tff('function_fun_app$r',axiom,
    ( ( 'fun_app$r'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec$_1') = 'fmb_A$_2' )
    & ( 'fun_app$r'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec$_2') = 'fmb_A$_2' )
    & ( 'fun_app$r'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec$_1') = 'fmb_A$_2' )
    & ( 'fun_app$r'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec$_2') = 'fmb_A$_2' ) ) ).

tff('declare_interchange_rows$a',type,
    'interchange_rows$a': ( 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_n_vec_n_vec_fun$' ).

tff('function_interchange_rows$a',axiom,
    ( ( 'interchange_rows$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_n_vec_n_vec_fun$_2' )
    & ( 'interchange_rows$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_n_vec_n_vec_fun$_1' ) ) ).

tff('declare_map_matrix$i',type,
    'map_matrix$i': ( 'A_a_b_vec_n_vec_fun$' * 'A_n_vec_n_vec$' ) > 'A_b_vec_n_vec_n_vec_n_vec$' ).

tff('function_map_matrix$i',axiom,
    ( ( 'map_matrix$i'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$i'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$i'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$i'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_map_matrix$',type,
    'map_matrix$': ( 'A_a_fun$' * 'A_b_vec_n_vec$' ) > 'A_b_vec_n_vec$' ).

tff('function_map_matrix$',axiom,
    ( ( 'map_matrix$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'map_matrix$'('fmb_A_a_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'map_matrix$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'map_matrix$'('fmb_A_a_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('declare_fun_app$d',type,
    'fun_app$d': ( 'N_a_b_vec_n_vec_fun$' * 'N$' ) > 'A_b_vec_n_vec$' ).

tff('function_fun_app$d',axiom,
    ( ( 'fun_app$d'('fmb_N_a_b_vec_n_vec_fun$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$d'('fmb_N_a_b_vec_n_vec_fun$_2','fmb_N$_1') = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('declare_row_add$a',type,
    'row_add$a': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$' ) > 'A_n_vec_n_vec$' ).

tff('function_row_add$a',axiom,
    ( ( 'row_add$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'row_add$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'row_add$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'row_add$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_map_matrix$k',type,
    'map_matrix$k': ( 'A_a_b_vec_fun$' * 'A_b_vec_n_vec$' ) > 'A_b_vec_b_vec_n_vec$' ).

tff('function_map_matrix$k',axiom,
    ( ( 'map_matrix$k'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_b_vec_n_vec$_1' )
    & ( 'map_matrix$k'('fmb_A_a_b_vec_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_b_vec_n_vec$_1' )
    & ( 'map_matrix$k'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_b_vec_n_vec$_1' )
    & ( 'map_matrix$k'('fmb_A_a_b_vec_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_b_vec_n_vec$_1' ) ) ).

tff('declare_vec_lambda$b',type,
    'vec_lambda$b': 'N_a_fun$' > 'A_n_vec$' ).

tff('function_vec_lambda$b',axiom,
    ( ( 'vec_lambda$b'('fmb_N_a_fun$_1') = 'fmb_A_n_vec$_1' )
    & ( 'vec_lambda$b'('fmb_N_a_fun$_2') = 'fmb_A_n_vec$_2' ) ) ).

tff('declare_vec_nth$d',type,
    'vec_nth$d': 'A_b_vec_b_vec$' > 'B_a_b_vec_fun$' ).

tff('function_vec_nth$d',axiom,
    ( ( 'vec_nth$d'('fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'vec_nth$d'('fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_uun$',type,
    'uun$': ( 'A_b_vec_n_vec$' * 'B$' * 'B$' * 'N$' ) > 'B_a_fun$' ).

tff('function_uun$',axiom,
    ( ( 'uun$'('fmb_A_b_vec_n_vec$_1','fmb_B$_1','fmb_B$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uun$'('fmb_A_b_vec_n_vec$_2','fmb_B$_1','fmb_B$_1','fmb_N$_1') = 'fmb_B_a_fun$_2' ) ) ).

tff('declare_fun_app$ag',type,
    'fun_app$ag': ( 'N_n_fun$' * 'N$' ) > 'N$' ).

tff('function_fun_app$ag',axiom,
    ( ( 'fun_app$ag'('fmb_N_n_fun$_1','fmb_N$_1') = 'fmb_N$_1' )
    & ( 'fun_app$ag'('fmb_N_n_fun$_2','fmb_N$_1') = 'fmb_N$_1' ) ) ).

tff('declare_rowvector$',type,
    'rowvector$': 'A_n_vec$' > 'A_n_vec_n_vec$' ).

tff('function_rowvector$',axiom,
    ( ( 'rowvector$'('fmb_A_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'rowvector$'('fmb_A_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_uuf$',type,
    'uuf$': 'A_b_vec$' > 'B_a_fun$' ).

tff('function_uuf$',axiom,
    ( ( 'uuf$'('fmb_A_b_vec$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uuf$'('fmb_A_b_vec$_2') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uuw$',type,
    'uuw$': ( 'A_b_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uuw$',axiom,
    ( ( 'uuw$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uuw$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_fun_app$i',type,
    'fun_app$i': ( 'B_a_n_vec_fun$' * 'B$' ) > 'A_n_vec$' ).

tff('function_fun_app$i',axiom,
    ( ( 'fun_app$i'('fmb_B_a_n_vec_fun$_1','fmb_B$_1') = 'fmb_A_n_vec$_2' )
    & ( 'fun_app$i'('fmb_B_a_n_vec_fun$_2','fmb_B$_1') = 'fmb_A_n_vec$_1' ) ) ).

tff('declare_fun_app$af',type,
    'fun_app$af': ( 'N_a_b_vec_bool_fun_fun$' * 'N$' ) > 'A_b_vec_bool_fun$' ).

tff('function_fun_app$af',axiom,
    ( ( 'fun_app$af'('fmb_N_a_b_vec_bool_fun_fun$_1','fmb_N$_1') = 'fmb_A_b_vec_bool_fun$_2' )
    & ( 'fun_app$af'('fmb_N_a_b_vec_bool_fun_fun$_2','fmb_N$_1') = 'fmb_A_b_vec_bool_fun$_2' ) ) ).

tff('declare_interchange_rows_row$',type,
    'interchange_rows_row$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_interchange_rows_row$',axiom,
    ( ( 'interchange_rows_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'interchange_rows_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uwk$',type,
    'uwk$': 'A_b_vec$' > 'N_a_b_vec_fun$' ).

tff('function_uwk$',axiom,
    ( ( 'uwk$'('fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uwk$'('fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_uug$',type,
    'uug$': 'A_b_vec_n_vec$' > 'N_a_b_vec_fun$' ).

tff('function_uug$',axiom,
    ( ( 'uug$'('fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uug$'('fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_fun_app$v',type,
    'fun_app$v': ( 'A_n_vec_a_b_vec_fun$' * 'A_n_vec$' ) > 'A_b_vec$' ).

tff('function_fun_app$v',axiom,
    ( ( 'fun_app$v'('fmb_A_n_vec_a_b_vec_fun$_1','fmb_A_n_vec$_1') = 'fmb_A_b_vec$_2' )
    & ( 'fun_app$v'('fmb_A_n_vec_a_b_vec_fun$_1','fmb_A_n_vec$_2') = 'fmb_A_b_vec$_2' )
    & ( 'fun_app$v'('fmb_A_n_vec_a_b_vec_fun$_2','fmb_A_n_vec$_1') = 'fmb_A_b_vec$_2' )
    & ( 'fun_app$v'('fmb_A_n_vec_a_b_vec_fun$_2','fmb_A_n_vec$_2') = 'fmb_A_b_vec$_2' ) ) ).

tff('declare_uwv$',type,
    'uwv$': ( 'A_b_vec$' * 'B$' ) > 'B_a_fun$' ).

tff('function_uwv$',axiom,
    ( ( 'uwv$'('fmb_A_b_vec$_1','fmb_B$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uwv$'('fmb_A_b_vec$_2','fmb_B$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_vec_nth$g',type,
    'vec_nth$g': ( 'A_b_vec_n_vec_n_vec_n_vec$' * 'N$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_vec_nth$g',axiom,
    ( ( 'vec_nth$g'('fmb_A_b_vec_n_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'vec_nth$g'('fmb_A_b_vec_n_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_times$c',type,
    'times$c': 'A$' > 'A_a_fun$' ).

tff('function_times$c',axiom,
    ( ( 'times$c'('fmb_A$_1') = 'fmb_A_a_fun$_2' )
    & ( 'times$c'('fmb_A$_2') = 'fmb_A_a_fun$_1' ) ) ).

tff('declare_uxi$',type,
    'uxi$': ( 'A_b_vec_n_vec$' * 'N$' * 'A$' ) > 'N_a_b_vec_fun$' ).

tff('function_uxi$',axiom,
    ( ( 'uxi$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxi$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxi$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uxi$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_map_matrix$b',type,
    'map_matrix$b': ( 'A_a_b_vec_fun$' * 'A_n_vec_n_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_map_matrix$b',axiom,
    ( ( 'map_matrix$b'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$b'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$b'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$b'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_times$',type,
    'times$': 'A_b_vec_n_vec$' > 'A_b_vec_n_vec_a_b_vec_n_vec_fun$' ).

tff('function_times$',axiom,
    ( ( 'times$'('fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_1' )
    & ( 'times$'('fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_fun_app$t',type,
    'fun_app$t': ( 'A_a_b_vec_fun$' * 'A$' ) > 'A_b_vec$' ).

tff('function_fun_app$t',axiom,
    ( ( 'fun_app$t'('fmb_A_a_b_vec_fun$_1','fmb_A$_1') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$t'('fmb_A_a_b_vec_fun$_1','fmb_A$_2') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$t'('fmb_A_a_b_vec_fun$_2','fmb_A$_1') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$t'('fmb_A_a_b_vec_fun$_2','fmb_A$_2') = 'fmb_A_b_vec$_1' ) ) ).

tff('declare_uwx$',type,
    'uwx$': ( 'A_b_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uwx$',axiom,
    ( ( 'uwx$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uwx$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_vec_lambda$g',type,
    'vec_lambda$g': 'N_a_b_vec_b_vec_fun$' > 'A_b_vec_b_vec_n_vec$' ).

tff('function_vec_lambda$g',axiom,
    ( ( 'vec_lambda$g'('fmb_N_a_b_vec_b_vec_fun$_1') = 'fmb_A_b_vec_b_vec_n_vec$_1' )
    & ( 'vec_lambda$g'('fmb_N_a_b_vec_b_vec_fun$_2') = 'fmb_A_b_vec_b_vec_n_vec$_1' ) ) ).

tff('declare_interchange_rows$b',type,
    'interchange_rows$b': ( 'A_b_vec_n_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_n_vec_n_vec_fun$' ).

tff('function_interchange_rows$b',axiom,
    ( ( 'interchange_rows$b'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_1' )
    & ( 'interchange_rows$b'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_n_vec_fun$_2' ) ) ).

tff('declare_fun_app$s',type,
    'fun_app$s': ( 'A_a_n_vec_fun$' * 'A$' ) > 'A_n_vec$' ).

tff('function_fun_app$s',axiom,
    ( ( 'fun_app$s'('fmb_A_a_n_vec_fun$_1','fmb_A$_1') = 'fmb_A_n_vec$_1' )
    & ( 'fun_app$s'('fmb_A_a_n_vec_fun$_1','fmb_A$_2') = 'fmb_A_n_vec$_1' )
    & ( 'fun_app$s'('fmb_A_a_n_vec_fun$_2','fmb_A$_1') = 'fmb_A_n_vec$_1' )
    & ( 'fun_app$s'('fmb_A_a_n_vec_fun$_2','fmb_A$_2') = 'fmb_A_n_vec$_1' ) ) ).

tff('declare_divide$',type,
    'divide$': 'A$' > 'A_a_fun$' ).

tff('function_divide$',axiom,
    ( ( 'divide$'('fmb_A$_1') = 'fmb_A_a_fun$_1' )
    & ( 'divide$'('fmb_A$_2') = 'fmb_A_a_fun$_2' ) ) ).

tff('declare_columnvector$a',type,
    'columnvector$a': 'A_b_vec$' > 'A_n_vec_b_vec$' ).

tff('function_columnvector$a',axiom,
    ( ( 'columnvector$a'('fmb_A_b_vec$_1') = 'fmb_A_n_vec_b_vec$_1' )
    & ( 'columnvector$a'('fmb_A_b_vec$_2') = 'fmb_A_n_vec_b_vec$_1' ) ) ).

tff('declare_fun_app$m',type,
    'fun_app$m': ( 'A_a_fun$' * 'A$' ) > 'A$' ).

tff('function_fun_app$m',axiom,
    ( ( 'fun_app$m'('fmb_A_a_fun$_1','fmb_A$_1') = 'fmb_A$_2' )
    & ( 'fun_app$m'('fmb_A_a_fun$_1','fmb_A$_2') = 'fmb_A$_2' )
    & ( 'fun_app$m'('fmb_A_a_fun$_2','fmb_A$_1') = 'fmb_A$_1' )
    & ( 'fun_app$m'('fmb_A_a_fun$_2','fmb_A$_2') = 'fmb_A$_2' ) ) ).

tff('declare_uvd$',type,
    'uvd$': ( 'A_a_fun$' * 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uvd$',axiom,
    ( ( 'uvd$'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvd$'('fmb_A_a_fun$_1','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvd$'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvd$'('fmb_A_a_fun$_2','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_uwz$',type,
    'uwz$': ( 'A_n_vec$' * 'N$' ) > 'B_a_fun$' ).

tff('function_uwz$',axiom,
    ( ( 'uwz$'('fmb_A_n_vec$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uwz$'('fmb_A_n_vec$_2','fmb_N$_1') = 'fmb_B_a_fun$_2' ) ) ).

tff('declare_uwd$',type,
    'uwd$': ( 'A_n_vec_n_vec$' * 'N$' ) > 'N_n_bool_fun_fun$' ).

tff('function_uwd$',axiom,
    ( ( 'uwd$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_n_bool_fun_fun$_1' )
    & ( 'uwd$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_n_bool_fun_fun$_2' ) ) ).

tff('declare_interchange_rows_row$a',type,
    'interchange_rows_row$a': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_interchange_rows_row$a',axiom,
    ( ( 'interchange_rows_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'interchange_rows_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_times$a',type,
    'times$a': 'A_n_vec$' > 'A_n_vec_a_n_vec_fun$' ).

tff('function_times$a',axiom,
    ( ( 'times$a'('fmb_A_n_vec$_1') = 'fmb_A_n_vec_a_n_vec_fun$_2' )
    & ( 'times$a'('fmb_A_n_vec$_2') = 'fmb_A_n_vec_a_n_vec_fun$_1' ) ) ).

tff('declare_uur$',type,
    'uur$': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' * 'B$' ) > 'B_a_fun$' ).

tff('function_uur$',axiom,
    ( ( 'uur$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uur$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uuz$',type,
    'uuz$': ( 'A_a_b_vec_fun$' * 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uuz$',axiom,
    ( ( 'uuz$'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uuz$'('fmb_A_a_b_vec_fun$_1','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uuz$'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uuz$'('fmb_A_a_b_vec_fun$_2','fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_uwr$',type,
    'uwr$': ( 'A_b_vec_n_vec$' * 'N$' ) > 'B_a_b_vec_fun$' ).

tff('function_uwr$',axiom,
    ( ( 'uwr$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uwr$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_B_a_b_vec_fun$_1' ) ) ).

tff('declare_interchange_columns$c',type,
    'interchange_columns$c': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' ) > 'A_b_vec_b_vec$' ).

tff('function_interchange_columns$c',axiom,
    ( ( 'interchange_columns$c'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'interchange_columns$c'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_uuu$',type,
    'uuu$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uuu$',axiom,
    ( ( 'uuu$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uuu$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_row_add_row$a',type,
    'row_add_row$a': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$' ) > 'N_a_n_vec_fun$' ).

tff('function_row_add_row$a',axiom,
    ( ( 'row_add_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'row_add_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'row_add_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'row_add_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_fun_app$u',type,
    'fun_app$u': ( 'A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$' * 'A_b_vec_n_vec_n_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_fun_app$u',axiom,
    ( ( 'fun_app$u'('fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'fun_app$u'('fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'fun_app$u'('fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'fun_app$u'('fmb_A_b_vec_n_vec_n_vec_a_b_vec_n_vec_n_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_uxd$',type,
    'uxd$': ( 'A_b_vec_b_vec$' * 'B$' * 'A$' * 'B$' ) > 'B_a_fun$' ).

tff('function_uxd$',axiom,
    ( ( 'uxd$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uxd$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_2','fmb_B$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uxd$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uxd$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_2','fmb_B$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uvc$',type,
    'uvc$': ( 'A_b_vec_a_b_vec_fun$' * 'A_b_vec_n_vec_n_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uvc$',axiom,
    ( ( 'uvc$'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'uvc$'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uvc$'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uvc$'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uws$',type,
    'uws$': 'A_b_vec_n_vec$' > 'N_a_b_vec_b_vec_fun$' ).

tff('function_uws$',axiom,
    ( ( 'uws$'('fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_b_vec_fun$_1' )
    & ( 'uws$'('fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_b_vec_fun$_2' ) ) ).

tff('declare_fun_app$n',type,
    'fun_app$n': ( 'A_a_b_vec_n_vec_fun$' * 'A$' ) > 'A_b_vec_n_vec$' ).

tff('function_fun_app$n',axiom,
    ( ( 'fun_app$n'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A$_1') = 'fmb_A_b_vec_n_vec$_2' )
    & ( 'fun_app$n'('fmb_A_a_b_vec_n_vec_fun$_1','fmb_A$_2') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$n'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'fun_app$n'('fmb_A_a_b_vec_n_vec_fun$_2','fmb_A$_2') = 'fmb_A_b_vec_n_vec$_1' ) ) ).

tff('declare_rowvector$c',type,
    'rowvector$c': 'A_b_vec$' > 'A_b_vec_n_vec$' ).

tff('function_rowvector$c',axiom,
    ( ( 'rowvector$c'('fmb_A_b_vec$_1') = 'fmb_A_b_vec_n_vec$_2' )
    & ( 'rowvector$c'('fmb_A_b_vec$_2') = 'fmb_A_b_vec_n_vec$_1' ) ) ).

tff('declare_fun_app$e',type,
    'fun_app$e': ( 'B_a_b_vec_fun$' * 'B$' ) > 'A_b_vec$' ).

tff('function_fun_app$e',axiom,
    ( ( 'fun_app$e'('fmb_B_a_b_vec_fun$_1','fmb_B$_1') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$e'('fmb_B_a_b_vec_fun$_2','fmb_B$_1') = 'fmb_A_b_vec$_2' ) ) ).

tff('declare_mult_row$c',type,
    'mult_row$c': ( 'A_b_vec_b_vec$' * 'B$' * 'A$' ) > 'A_b_vec_b_vec$' ).

tff('function_mult_row$c',axiom,
    ( ( 'mult_row$c'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'mult_row$c'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_2') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'mult_row$c'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_1') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'mult_row$c'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_gauss_Jordan_in_ij$',type,
    'gauss_Jordan_in_ij$': ( 'A_b_vec_n_vec$' * 'N$' * 'B$' ) > 'A_b_vec_n_vec$' ).

tff('function_gauss_Jordan_in_ij$',axiom,
    ( ( 'gauss_Jordan_in_ij$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_B$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'gauss_Jordan_in_ij$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_B$_1') = 'fmb_A_b_vec_n_vec$_1' ) ) ).

tff('declare_columnvector$d',type,
    'columnvector$d': 'A_n_vec$' > 'A_n_vec_n_vec$' ).

tff('function_columnvector$d',axiom,
    ( ( 'columnvector$d'('fmb_A_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'columnvector$d'('fmb_A_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_times$f',type,
    'times$f': ( 'A_b_vec_b_vec$' * 'A_b_vec_b_vec$' ) > 'A_b_vec_b_vec$' ).

tff('function_times$f',axiom,
    ( ( 'times$f'('fmb_A_b_vec_b_vec$_1','fmb_A_b_vec_b_vec$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'times$f'('fmb_A_b_vec_b_vec$_1','fmb_A_b_vec_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'times$f'('fmb_A_b_vec_b_vec$_2','fmb_A_b_vec_b_vec$_1') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'times$f'('fmb_A_b_vec_b_vec$_2','fmb_A_b_vec_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_row_add$',type,
    'row_add$': ( 'A_b_vec_n_vec$' * 'N$' * 'N$' ) > 'A_a_b_vec_n_vec_fun$' ).

tff('function_row_add$',axiom,
    ( ( 'row_add$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_A_a_b_vec_n_vec_fun$_2' )
    & ( 'row_add$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_A_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_uxe$',type,
    'uxe$': ( 'A_b_vec_b_vec$' * 'B$' * 'A$' ) > 'B_a_b_vec_fun$' ).

tff('function_uxe$',axiom,
    ( ( 'uxe$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uxe$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_A$_2') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uxe$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_1') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uxe$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_A$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_fun_app$l',type,
    'fun_app$l': ( 'N_a_fun$' * 'N$' ) > 'A$' ).

tff('function_fun_app$l',axiom,
    ( ( 'fun_app$l'('fmb_N_a_fun$_1','fmb_N$_1') = 'fmb_A$_2' )
    & ( 'fun_app$l'('fmb_N_a_fun$_2','fmb_N$_1') = 'fmb_A$_1' ) ) ).

tff('declare_uminus$d',type,
    'uminus$d': 'A_b_vec_n_vec_n_vec$' > 'A_b_vec_n_vec_n_vec$' ).

tff('function_uminus$d',axiom,
    ( ( 'uminus$d'('fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'uminus$d'('fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_uxc$',type,
    'uxc$': ( 'A_n_vec_n_vec$' * 'N$' * 'A$' ) > 'N_a_n_vec_fun$' ).

tff('function_uxc$',axiom,
    ( ( 'uxc$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uxc$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uxc$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'uxc$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_mult_row_row$a',type,
    'mult_row_row$a': ( 'A_n_vec_n_vec$' * 'N$' * 'A$' ) > 'N_a_n_vec_fun$' ).

tff('function_mult_row_row$a',axiom,
    ( ( 'mult_row_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'mult_row_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'mult_row_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_n_vec_fun$_1' )
    & ( 'mult_row_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_interchange_columns_row$a',type,
    'interchange_columns_row$a': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_interchange_columns_row$a',axiom,
    ( ( 'interchange_columns_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'interchange_columns_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_row_add$b',type,
    'row_add$b': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' * 'A_b_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_row_add$b',axiom,
    ( ( 'row_add$b'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'row_add$b'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'row_add$b'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'row_add$b'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_uvf$',type,
    'uvf$': ( 'A_a_fun$' * 'A_b_vec_b_vec$' * 'B$' ) > 'B_a_fun$' ).

tff('function_uvf$',axiom,
    ( ( 'uvf$'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_1','fmb_B$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uvf$'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_2','fmb_B$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uvf$'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_1','fmb_B$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uvf$'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_2','fmb_B$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uwo$',type,
    'uwo$': 'A_b_vec$' > 'B_a_n_vec_fun$' ).

tff('function_uwo$',axiom,
    ( ( 'uwo$'('fmb_A_b_vec$_1') = 'fmb_B_a_n_vec_fun$_1' )
    & ( 'uwo$'('fmb_A_b_vec$_2') = 'fmb_B_a_n_vec_fun$_2' ) ) ).

tff('declare_mult_row_row$b',type,
    'mult_row_row$b': ( 'A_b_vec_n_vec$' * 'N$' * 'A$' ) > 'N_a_b_vec_fun$' ).

tff('function_mult_row_row$b',axiom,
    ( ( 'mult_row_row$b'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'mult_row_row$b'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'mult_row_row$b'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'mult_row_row$b'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_2') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_uwt$',type,
    'uwt$': ( 'A_n_vec$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uwt$',axiom,
    ( ( 'uwt$'('fmb_A_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uwt$'('fmb_A_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_columnvector$e',type,
    'columnvector$e': 'A_b_vec$' > 'A_b_vec_b_vec$' ).

tff('function_columnvector$e',axiom,
    ( ( 'columnvector$e'('fmb_A_b_vec$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'columnvector$e'('fmb_A_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_uvl$',type,
    'uvl$': ( 'A_b_vec_a_fun$' * 'A_b_vec_n_vec_n_vec$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uvl$',axiom,
    ( ( 'uvl$'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvl$'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvl$'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uvl$'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_fun$_1' ) ) ).

tff('declare_fun_app$b',type,
    'fun_app$b': ( 'N_a_b_vec_fun$' * 'N$' ) > 'A_b_vec$' ).

tff('function_fun_app$b',axiom,
    ( ( 'fun_app$b'('fmb_N_a_b_vec_fun$_1','fmb_N$_1') = 'fmb_A_b_vec$_1' )
    & ( 'fun_app$b'('fmb_N_a_b_vec_fun$_2','fmb_N$_1') = 'fmb_A_b_vec$_2' ) ) ).

tff('declare_mult_row$a',type,
    'mult_row$a': ( 'A_n_vec_n_vec$' * 'N$' * 'A$' ) > 'A_n_vec_n_vec$' ).

tff('function_mult_row$a',axiom,
    ( ( 'mult_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'mult_row$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_2') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'mult_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'mult_row$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_2') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_uxb$',type,
    'uxb$': ( 'A_n_vec_n_vec$' * 'N$' * 'A$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uxb$',axiom,
    ( ( 'uxb$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uxb$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_A$_2','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uxb$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_1','fmb_N$_1') = 'fmb_N_a_fun$_2' )
    & ( 'uxb$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_A$_2','fmb_N$_1') = 'fmb_N_a_fun$_1' ) ) ).

tff('declare_uwe$',type,
    'uwe$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_uwe$',axiom,
    ( ( 'uwe$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uwe$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' ) ) ).

tff('declare_vec_nth$',type,
    'vec_nth$': 'A_b_vec$' > 'B_a_fun$' ).

tff('function_vec_nth$',axiom,
    ( ( 'vec_nth$'('fmb_A_b_vec$_1') = 'fmb_B_a_fun$_2' )
    & ( 'vec_nth$'('fmb_A_b_vec$_2') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uminus$',type,
    'uminus$': 'A_b_vec_n_vec$' > 'A_b_vec_n_vec$' ).

tff('function_uminus$',axiom,
    ( ( 'uminus$'('fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'uminus$'('fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec$_1' ) ) ).

tff('declare_map_matrix$j',type,
    'map_matrix$j': ( 'A_a_fun$' * 'A_b_vec_b_vec$' ) > 'A_b_vec_b_vec$' ).

tff('function_map_matrix$j',axiom,
    ( ( 'map_matrix$j'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_1') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'map_matrix$j'('fmb_A_a_fun$_1','fmb_A_b_vec_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' )
    & ( 'map_matrix$j'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'map_matrix$j'('fmb_A_a_fun$_2','fmb_A_b_vec_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_fun_app$c',type,
    'fun_app$c': ( 'N_n_bool_fun_fun$' * 'N$' ) > 'N_bool_fun$' ).

tff('function_fun_app$c',axiom,
    ( ( 'fun_app$c'('fmb_N_n_bool_fun_fun$_1','fmb_N$_1') = 'fmb_N_bool_fun$_2' )
    & ( 'fun_app$c'('fmb_N_n_bool_fun_fun$_2','fmb_N$_1') = 'fmb_N_bool_fun$_1' ) ) ).

tff('declare_uwu$',type,
    'uwu$': 'A_n_vec$' > 'N_a_n_vec_fun$' ).

tff('function_uwu$',axiom,
    ( ( 'uwu$'('fmb_A_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uwu$'('fmb_A_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_mult_row$',type,
    'mult_row$': ( 'A_b_vec_n_vec$' * 'N$' ) > 'A_a_b_vec_n_vec_fun$' ).

tff('function_mult_row$',axiom,
    ( ( 'mult_row$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1') = 'fmb_A_a_b_vec_n_vec_fun$_2' )
    & ( 'mult_row$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1') = 'fmb_A_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uxn$',type,
    'uxn$': ( 'A_b_vec$' * 'A_b_vec$' ) > 'B_a_fun$' ).

tff('function_uxn$',axiom,
    ( ( 'uxn$'('fmb_A_b_vec$_1','fmb_A_b_vec$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uxn$'('fmb_A_b_vec$_1','fmb_A_b_vec$_2') = 'fmb_B_a_fun$_1' )
    & ( 'uxn$'('fmb_A_b_vec$_2','fmb_A_b_vec$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uxn$'('fmb_A_b_vec$_2','fmb_A_b_vec$_2') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uwp$',type,
    'uwp$': ( 'A_n_vec_n_vec$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_uwp$',axiom,
    ( ( 'uwp$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uwp$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_uuj$',type,
    'uuj$': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' * 'B$' ) > 'B_a_fun$' ).

tff('function_uuj$',axiom,
    ( ( 'uuj$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uuj$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_uxk$',type,
    'uxk$': ( 'A_b_vec_b_vec$' * 'A_b_vec_b_vec$' ) > 'B_a_b_vec_fun$' ).

tff('function_uxk$',axiom,
    ( ( 'uxk$'('fmb_A_b_vec_b_vec$_1','fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uxk$'('fmb_A_b_vec_b_vec$_1','fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uxk$'('fmb_A_b_vec_b_vec$_2','fmb_A_b_vec_b_vec$_1') = 'fmb_B_a_b_vec_fun$_2' )
    & ( 'uxk$'('fmb_A_b_vec_b_vec$_2','fmb_A_b_vec_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_gauss_Jordan_in_ij$a',type,
    'gauss_Jordan_in_ij$a': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'A_n_vec_n_vec$' ).

tff('function_gauss_Jordan_in_ij$a',axiom,
    ( ( 'gauss_Jordan_in_ij$a'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'gauss_Jordan_in_ij$a'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_uww$',type,
    'uww$': 'A_b_vec$' > 'B_a_b_vec_fun$' ).

tff('function_uww$',axiom,
    ( ( 'uww$'('fmb_A_b_vec$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uww$'('fmb_A_b_vec$_2') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_interchange_columns$b',type,
    'interchange_columns$b': ( 'A_b_vec_n_vec$' * 'B$' * 'B$' ) > 'A_b_vec_n_vec$' ).

tff('function_interchange_columns$b',axiom,
    ( ( 'interchange_columns$b'('fmb_A_b_vec_n_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_n_vec$_1' )
    & ( 'interchange_columns$b'('fmb_A_b_vec_n_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_n_vec$_2' ) ) ).

tff('declare_uuo$',type,
    'uuo$': ( 'A_b_vec_n_vec$' * 'B$' * 'B$' ) > 'N_a_b_vec_fun$' ).

tff('function_uuo$',axiom,
    ( ( 'uuo$'('fmb_A_b_vec_n_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uuo$'('fmb_A_b_vec_n_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_vec_nth$e',type,
    'vec_nth$e': 'A_n_vec$' > 'N_a_fun$' ).

tff('function_vec_nth$e',axiom,
    ( ( 'vec_nth$e'('fmb_A_n_vec$_1') = 'fmb_N_a_fun$_1' )
    & ( 'vec_nth$e'('fmb_A_n_vec$_2') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_map_matrix$f',type,
    'map_matrix$f': ( 'A_b_vec_a_b_vec_fun$' * 'A_b_vec_n_vec_n_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_map_matrix$f',axiom,
    ( ( 'map_matrix$f'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_1' )
    & ( 'map_matrix$f'('fmb_A_b_vec_a_b_vec_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$f'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$f'('fmb_A_b_vec_a_b_vec_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_interchange_columns$',type,
    'interchange_columns$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'A_n_vec_n_vec$' ).

tff('function_interchange_columns$',axiom,
    ( ( 'interchange_columns$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'interchange_columns$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_uut$',type,
    'uut$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'N$' * 'N$' ) > 'N_a_b_vec_fun$' ).

tff('function_uut$',axiom,
    ( ( 'uut$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_1' )
    & ( 'uut$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_b_vec_fun$_2' ) ) ).

tff('declare_uminus$a',type,
    'uminus$a': 'A_n_vec$' > 'A_n_vec$' ).

tff('function_uminus$a',axiom,
    ( ( 'uminus$a'('fmb_A_n_vec$_1') = 'fmb_A_n_vec$_1' )
    & ( 'uminus$a'('fmb_A_n_vec$_2') = 'fmb_A_n_vec$_1' ) ) ).

tff('declare_fun_app$y',type,
    'fun_app$y': ( 'N_a_b_vec_n_vec_bool_fun_fun$' * 'N$' ) > 'A_b_vec_n_vec_bool_fun$' ).

tff('function_fun_app$y',axiom,
    ( ( 'fun_app$y'('fmb_N_a_b_vec_n_vec_bool_fun_fun$_1','fmb_N$_1') = 'fmb_A_b_vec_n_vec_bool_fun$_2' )
    & ( 'fun_app$y'('fmb_N_a_b_vec_n_vec_bool_fun_fun$_2','fmb_N$_1') = 'fmb_A_b_vec_n_vec_bool_fun$_2' ) ) ).

tff('declare_uuh$',type,
    'uuh$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' * 'N$' ) > 'N_a_fun$' ).

tff('function_uuh$',axiom,
    ( ( 'uuh$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_fun$_1' )
    & ( 'uuh$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_fun$_2' ) ) ).

tff('declare_uwh$',type,
    'uwh$': 'A_n_vec$' > 'N_a_n_vec_fun$' ).

tff('function_uwh$',axiom,
    ( ( 'uwh$'('fmb_A_n_vec$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uwh$'('fmb_A_n_vec$_2') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_vec_lambda$h',type,
    'vec_lambda$h': 'N_a_b_vec_n_vec_n_vec_fun$' > 'A_b_vec_n_vec_n_vec_n_vec$' ).

tff('function_vec_lambda$h',axiom,
    ( ( 'vec_lambda$h'('fmb_N_a_b_vec_n_vec_n_vec_fun$_1') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_2' )
    & ( 'vec_lambda$h'('fmb_N_a_b_vec_n_vec_n_vec_fun$_2') = 'fmb_A_b_vec_n_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_vec_nth$f',type,
    'vec_nth$f': ( 'A_n_vec_n_vec_n_vec$' * 'N$' ) > 'A_n_vec_n_vec$' ).

tff('function_vec_nth$f',axiom,
    ( ( 'vec_nth$f'('fmb_A_n_vec_n_vec_n_vec$_1','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'vec_nth$f'('fmb_A_n_vec_n_vec_n_vec$_2','fmb_N$_1') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_uxa$',type,
    'uxa$': 'A_n_vec$' > 'N_a_b_vec_fun$' ).

tff('function_uxa$',axiom,
    ( ( 'uxa$'('fmb_A_n_vec$_1') = 'fmb_N_a_b_vec_fun$_2' )
    & ( 'uxa$'('fmb_A_n_vec$_2') = 'fmb_N_a_b_vec_fun$_1' ) ) ).

tff('declare_mult_row_row$',type,
    'mult_row_row$': ( 'A_b_vec_n_vec_n_vec$' * 'N$' * 'A_b_vec$' ) > 'N_a_b_vec_n_vec_fun$' ).

tff('function_mult_row_row$',axiom,
    ( ( 'mult_row_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_2' )
    & ( 'mult_row_row$'('fmb_A_b_vec_n_vec_n_vec$_1','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'mult_row_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'mult_row_row$'('fmb_A_b_vec_n_vec_n_vec$_2','fmb_N$_1','fmb_A_b_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_1' ) ) ).

tff('declare_uui$',type,
    'uui$': ( 'A_n_vec_n_vec$' * 'N$' * 'N$' ) > 'N_a_n_vec_fun$' ).

tff('function_uui$',axiom,
    ( ( 'uui$'('fmb_A_n_vec_n_vec$_1','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_2' )
    & ( 'uui$'('fmb_A_n_vec_n_vec$_2','fmb_N$_1','fmb_N$_1') = 'fmb_N_a_n_vec_fun$_1' ) ) ).

tff('declare_fun_app$aa',type,
    'fun_app$aa': ( 'N_a_n_vec_bool_fun_fun$' * 'N$' ) > 'A_n_vec_bool_fun$' ).

tff('function_fun_app$aa',axiom,
    ( ( 'fun_app$aa'('fmb_N_a_n_vec_bool_fun_fun$_1','fmb_N$_1') = 'fmb_A_n_vec_bool_fun$_2' )
    & ( 'fun_app$aa'('fmb_N_a_n_vec_bool_fun_fun$_2','fmb_N$_1') = 'fmb_A_n_vec_bool_fun$_2' ) ) ).

tff('declare_rowvector$a',type,
    'rowvector$a': 'A_b_vec$' > 'A_b_vec_b_vec$' ).

tff('function_rowvector$a',axiom,
    ( ( 'rowvector$a'('fmb_A_b_vec$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'rowvector$a'('fmb_A_b_vec$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_map_matrix$c',type,
    'map_matrix$c': ( 'A_b_vec_a_fun$' * 'A_b_vec_n_vec_n_vec$' ) > 'A_n_vec_n_vec$' ).

tff('function_map_matrix$c',axiom,
    ( ( 'map_matrix$c'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$c'('fmb_A_b_vec_a_fun$_1','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$c'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_1' )
    & ( 'map_matrix$c'('fmb_A_b_vec_a_fun$_2','fmb_A_b_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_uus$',type,
    'uus$': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' ) > 'B_a_b_vec_fun$' ).

tff('function_uus$',axiom,
    ( ( 'uus$'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_b_vec_fun$_1' )
    & ( 'uus$'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_B_a_b_vec_fun$_2' ) ) ).

tff('declare_map_matrix$g',type,
    'map_matrix$g': ( 'A_n_vec_a_b_vec_fun$' * 'A_n_vec_n_vec_n_vec$' ) > 'A_b_vec_n_vec_n_vec$' ).

tff('function_map_matrix$g',axiom,
    ( ( 'map_matrix$g'('fmb_A_n_vec_a_b_vec_fun$_1','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$g'('fmb_A_n_vec_a_b_vec_fun$_1','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$g'('fmb_A_n_vec_a_b_vec_fun$_2','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'map_matrix$g'('fmb_A_n_vec_a_b_vec_fun$_2','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_2' ) ) ).

tff('declare_map_matrix$d',type,
    'map_matrix$d': ( 'A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$' ) > 'A_n_vec_n_vec$' ).

tff('function_map_matrix$d',axiom,
    ( ( 'map_matrix$d'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$d'('fmb_A_n_vec_a_fun$_1','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$d'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'map_matrix$d'('fmb_A_n_vec_a_fun$_2','fmb_A_n_vec_n_vec_n_vec$_2') = 'fmb_A_n_vec_n_vec$_2' ) ) ).

tff('declare_uwj$',type,
    'uwj$': 'A_b_vec_n_vec$' > 'N_a_b_vec_n_vec_fun$' ).

tff('function_uwj$',axiom,
    ( ( 'uwj$'('fmb_A_b_vec_n_vec$_1') = 'fmb_N_a_b_vec_n_vec_fun$_1' )
    & ( 'uwj$'('fmb_A_b_vec_n_vec$_2') = 'fmb_N_a_b_vec_n_vec_fun$_2' ) ) ).

tff('declare_vec_lambda$c',type,
    'vec_lambda$c': 'B_a_b_vec_fun$' > 'A_b_vec_b_vec$' ).

tff('function_vec_lambda$c',axiom,
    ( ( 'vec_lambda$c'('fmb_B_a_b_vec_fun$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'vec_lambda$c'('fmb_B_a_b_vec_fun$_2') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_uwq$',type,
    'uwq$': 'A_n_vec_n_vec$' > 'N_a_n_vec_n_vec_fun$' ).

tff('function_uwq$',axiom,
    ( ( 'uwq$'('fmb_A_n_vec_n_vec$_1') = 'fmb_N_a_n_vec_n_vec_fun$_2' )
    & ( 'uwq$'('fmb_A_n_vec_n_vec$_2') = 'fmb_N_a_n_vec_n_vec_fun$_1' ) ) ).

tff('declare_uxh$',type,
    'uxh$': ( 'A_b_vec_n_vec$' * 'N$' * 'A$' * 'N$' ) > 'B_a_fun$' ).

tff('function_uxh$',axiom,
    ( ( 'uxh$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_1','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uxh$'('fmb_A_b_vec_n_vec$_1','fmb_N$_1','fmb_A$_2','fmb_N$_1') = 'fmb_B_a_fun$_1' )
    & ( 'uxh$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_1','fmb_N$_1') = 'fmb_B_a_fun$_2' )
    & ( 'uxh$'('fmb_A_b_vec_n_vec$_2','fmb_N$_1','fmb_A$_2','fmb_N$_1') = 'fmb_B_a_fun$_1' ) ) ).

tff('declare_columnvector$f',type,
    'columnvector$f': 'A_b_vec_n_vec$' > 'A_b_vec_n_vec_n_vec$' ).

tff('function_columnvector$f',axiom,
    ( ( 'columnvector$f'('fmb_A_b_vec_n_vec$_1') = 'fmb_A_b_vec_n_vec_n_vec$_2' )
    & ( 'columnvector$f'('fmb_A_b_vec_n_vec$_2') = 'fmb_A_b_vec_n_vec_n_vec$_1' ) ) ).

tff('declare_fun_app$ac',type,
    'fun_app$ac': ( 'N_a_bool_fun_fun$' * 'N$' ) > 'A_bool_fun$' ).

tff('function_fun_app$ac',axiom,
    ( ( 'fun_app$ac'('fmb_N_a_bool_fun_fun$_1','fmb_N$_1') = 'fmb_A_bool_fun$_2' )
    & ( 'fun_app$ac'('fmb_N_a_bool_fun_fun$_2','fmb_N$_1') = 'fmb_A_bool_fun$_2' ) ) ).

tff('declare_vec_lambda$d',type,
    'vec_lambda$d': 'N_a_n_vec_fun$' > 'A_n_vec_n_vec$' ).

tff('function_vec_lambda$d',axiom,
    ( ( 'vec_lambda$d'('fmb_N_a_n_vec_fun$_1') = 'fmb_A_n_vec_n_vec$_2' )
    & ( 'vec_lambda$d'('fmb_N_a_n_vec_fun$_2') = 'fmb_A_n_vec_n_vec$_1' ) ) ).

tff('declare_fun_app$w',type,
    'fun_app$w': ( 'A_b_vec_n_vec_a_fun$' * 'A_b_vec_n_vec$' ) > 'A$' ).

tff('function_fun_app$w',axiom,
    ( ( 'fun_app$w'('fmb_A_b_vec_n_vec_a_fun$_1','fmb_A_b_vec_n_vec$_1') = 'fmb_A$_1' )
    & ( 'fun_app$w'('fmb_A_b_vec_n_vec_a_fun$_1','fmb_A_b_vec_n_vec$_2') = 'fmb_A$_1' )
    & ( 'fun_app$w'('fmb_A_b_vec_n_vec_a_fun$_2','fmb_A_b_vec_n_vec$_1') = 'fmb_A$_1' )
    & ( 'fun_app$w'('fmb_A_b_vec_n_vec_a_fun$_2','fmb_A_b_vec_n_vec$_2') = 'fmb_A$_1' ) ) ).

tff('declare_interchange_rows$c',type,
    'interchange_rows$c': ( 'A_b_vec_b_vec$' * 'B$' * 'B$' ) > 'A_b_vec_b_vec$' ).

tff('function_interchange_rows$c',axiom,
    ( ( 'interchange_rows$c'('fmb_A_b_vec_b_vec$_1','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_b_vec$_1' )
    & ( 'interchange_rows$c'('fmb_A_b_vec_b_vec$_2','fmb_B$_1','fmb_B$_1') = 'fmb_A_b_vec_b_vec$_2' ) ) ).

tff('declare_thesis$',type,
    'thesis$': $o ).

tff('thesis$_definition',axiom,
    'thesis$' ).

tff('declare_fun_app$ae',type,
    'fun_app$ae': ( 'A_b_vec_bool_fun$' * 'A_b_vec$' ) > $o ).

tff('predicate_fun_app$ae',axiom,
    ( ~ 'fun_app$ae'('fmb_A_b_vec_bool_fun$_1','fmb_A_b_vec$_1')
    & ~ 'fun_app$ae'('fmb_A_b_vec_bool_fun$_1','fmb_A_b_vec$_2')
    & ~ 'fun_app$ae'('fmb_A_b_vec_bool_fun$_2','fmb_A_b_vec$_1')
    & ~ 'fun_app$ae'('fmb_A_b_vec_bool_fun$_2','fmb_A_b_vec$_2') ) ).

tff('declare_fun_app$ab',type,
    'fun_app$ab': ( 'A_bool_fun$' * 'A$' ) > $o ).

tff('predicate_fun_app$ab',axiom,
    ( ~ 'fun_app$ab'('fmb_A_bool_fun$_1','fmb_A$_1')
    & ~ 'fun_app$ab'('fmb_A_bool_fun$_1','fmb_A$_2')
    & ~ 'fun_app$ab'('fmb_A_bool_fun$_2','fmb_A$_1')
    & ~ 'fun_app$ab'('fmb_A_bool_fun$_2','fmb_A$_2') ) ).

tff('declare_fun_app$',type,
    'fun_app$': ( 'N_bool_fun$' * 'N$' ) > $o ).

tff('predicate_fun_app$',axiom,
    ( 'fun_app$'('fmb_N_bool_fun$_1','fmb_N$_1')
    & ~ 'fun_app$'('fmb_N_bool_fun$_2','fmb_N$_1') ) ).

tff('declare_fun_app$x',type,
    'fun_app$x': ( 'A_b_vec_n_vec_bool_fun$' * 'A_b_vec_n_vec$' ) > $o ).

tff('predicate_fun_app$x',axiom,
    ( ~ 'fun_app$x'('fmb_A_b_vec_n_vec_bool_fun$_1','fmb_A_b_vec_n_vec$_1')
    & ~ 'fun_app$x'('fmb_A_b_vec_n_vec_bool_fun$_1','fmb_A_b_vec_n_vec$_2')
    & ~ 'fun_app$x'('fmb_A_b_vec_n_vec_bool_fun$_2','fmb_A_b_vec_n_vec$_1')
    & ~ 'fun_app$x'('fmb_A_b_vec_n_vec_bool_fun$_2','fmb_A_b_vec_n_vec$_2') ) ).

tff('declare_fun_app$z',type,
    'fun_app$z': ( 'A_n_vec_bool_fun$' * 'A_n_vec$' ) > $o ).

tff('predicate_fun_app$z',axiom,
    ( ~ 'fun_app$z'('fmb_A_n_vec_bool_fun$_1','fmb_A_n_vec$_1')
    & ~ 'fun_app$z'('fmb_A_n_vec_bool_fun$_1','fmb_A_n_vec$_2')
    & ~ 'fun_app$z'('fmb_A_n_vec_bool_fun$_2','fmb_A_n_vec$_1')
    & ~ 'fun_app$z'('fmb_A_n_vec_bool_fun$_2','fmb_A_n_vec$_2') ) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : ITP325_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.08  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.43  % Computer : n009.cluster.edu
% 0.17/0.43  % Model    : x86_64 x86_64
% 0.17/0.43  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43  % Memory   : 8046.5625MB
% 0.17/0.43  % OS       : Linux 6.8.0-71-generic
% 0.17/0.44  % CPULimit : 300
% 0.17/0.44  % WCLimit  : 300
% 0.17/0.44  % DateTime : Sun Sep 27 12:54:15 UTC 2026
% 0.17/0.44  % CPUTime  : 
% 0.17/0.44  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.22/0.49  Running first-order model finding
% 0.22/0.49  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
% 3.92/1.09  % (2005398)Will run a generic schedule for satisfiability detection.
% 3.92/1.09  % (2005404)% WARNING: option uhcvi not known.
% 3.92/1.09  % (2005409)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3218601742:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.92/1.09  % (2005403)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2831178858_2999 on theBenchmark for (2999ds/0Mi)
% 3.92/1.09  % (2005408)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3992209333:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.92/1.09  % (2005404)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=300998601:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.92/1.09  % (2005405)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1024634063:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.92/1.09  % (2005407)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3351436:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.92/1.09  % (2005406)dis+10_1_sil=32000:sp=arity:random_seed=2572630674:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.92/1.09  % (2005407)Instruction limit reached! 
% 3.92/1.09  % (2005407)------------------------------
% 3.92/1.09  % (2005407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005407)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005407)Termination reason: Instruction limit
% 3.92/1.09  % (2005407)Termination phase: Saturation
% 3.92/1.09  % (2005407)Time elapsed: 0.115 s
% 3.92/1.09  % (2005407)Peak memory usage: 14 MB
% 3.92/1.09  % (2005407)Instructions burned: 116 (million)
% 3.92/1.09  % (2005406)Instruction limit reached! 
% 3.92/1.09  % (2005406)------------------------------
% 3.92/1.09  % (2005406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005406)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005406)Termination reason: Instruction limit
% 3.92/1.09  % (2005406)Termination phase: Saturation
% 3.92/1.09  % (2005406)Time elapsed: 0.113 s
% 3.92/1.09  % (2005406)Peak memory usage: 13 MB
% 3.92/1.09  % (2005406)Instructions burned: 104 (million)
% 3.92/1.09  % (2005408)Instruction limit reached! 
% 3.92/1.09  % (2005408)------------------------------
% 3.92/1.09  % (2005408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005408)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005408)Termination reason: Instruction limit
% 3.92/1.09  % (2005408)Termination phase: Saturation
% 3.92/1.09  % (2005408)Time elapsed: 0.133 s
% 3.92/1.09  % (2005408)Peak memory usage: 14 MB
% 3.92/1.09  % (2005408)Instructions burned: 131 (million)
% 3.92/1.09  % (2005418)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1520909140:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 3.92/1.09  % (2005409)Instruction limit reached! 
% 3.92/1.09  % (2005409)------------------------------
% 3.92/1.09  % (2005409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005409)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005409)Termination reason: Instruction limit
% 3.92/1.09  % (2005409)Termination phase: Saturation
% 3.92/1.09  % (2005409)Time elapsed: 0.153 s
% 3.92/1.09  % (2005409)Peak memory usage: 13 MB
% 3.92/1.09  % (2005409)Instructions burned: 159 (million)
% 3.92/1.09  % (2005417)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3485177336:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 3.92/1.09  % (2005419)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=3741094121:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.92/1.09  % (2005421)ott-21_1_sil=16000:fs=off:random_seed=3775867037:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 3.92/1.09  % (2005418)Instruction limit reached! 
% 3.92/1.09  % (2005418)------------------------------
% 3.92/1.09  % (2005418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005418)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005418)Termination reason: Instruction limit
% 3.92/1.09  % (2005418)Termination phase: Saturation
% 3.92/1.09  % (2005418)Time elapsed: 0.134 s
% 3.92/1.09  % (2005418)Peak memory usage: 14 MB
% 3.92/1.09  % (2005418)Instructions burned: 131 (million)
% 3.92/1.09  % (2005425)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2970414410:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 3.92/1.09  % (2005421)Instruction limit reached! 
% 3.92/1.09  % (2005421)------------------------------
% 3.92/1.09  % (2005421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.09  % (2005421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.09  % (2005421)CaDiCaL version: 2.1.3
% 3.92/1.09  % (2005421)Termination reason: Instruction limit
% 3.92/1.09  % (2005421)Termination phase: Saturation
% 3.92/1.09  % (2005421)Time elapsed: 0.156 s
% 3.92/1.09  % (2005421)Peak memory usage: 13 MB
% 3.92/1.09  % (2005421)Instructions burned: 180 (million)
% 3.92/1.09  % TRYING [1]
% 3.92/1.09  % (2005427)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1329560716:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 3.92/1.09  % TRYING [2]
% 3.92/1.09  % Finite Model Found!
% 3.92/1.09  % SZS status Satisfiable for theBenchmark
% 3.92/1.09  % (2005417) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2005398-2005417"...
% 3.92/1.09  % (2005417)...printing done.
% 3.92/1.09  % SZS output start FiniteModel for theBenchmark
% See solution above
% 3.92/1.10  % (2005417)------------------------------
% 3.92/1.10  % (2005417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.92/1.10  % (2005417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.10  % (2005417)CaDiCaL version: 2.1.3
% 3.92/1.10  % (2005417)Termination reason: Satisfiable
% 3.92/1.10  % (2005417)Time elapsed: 0.361 s
% 3.92/1.10  % (2005417)Peak memory usage: 24 MB
% 3.92/1.10  % (2005417)Instructions burned: 434 (million)
% 3.92/1.10  % (2005398)Success in time 0.591 s
% 3.92/1.10  % Vampire exiting
%------------------------------------------------------------------------------