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

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

% Computer : n007.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:23 AM UTC 2026

% Result   : CounterSatisfiable 7.49s 1.72s
% Output   : FiniteModel 7.49s
% 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_C_b_c_vec_a_vec_fun$',type,
    'C_b_c_vec_a_vec_fun$': $tType ).

tff('declare_C_b_c_vec_a_vec_fun$1',type,
    'fmb_C_b_c_vec_a_vec_fun$_1': 'C_b_c_vec_a_vec_fun$' ).

tff('finite_domain_C_b_c_vec_a_vec_fun$',axiom,
    ! [X: 'C_b_c_vec_a_vec_fun$'] : ( X = 'fmb_C_b_c_vec_a_vec_fun$_1' ) ).

tff('declare_B_a_vec_set$',type,
    'B_a_vec_set$': $tType ).

tff('declare_B_a_vec_set$1',type,
    'fmb_B_a_vec_set$_1': 'B_a_vec_set$' ).

tff('finite_domain_B_a_vec_set$',axiom,
    ! [X: 'B_a_vec_set$'] : ( X = 'fmb_B_a_vec_set$_1' ) ).

tff('declare_B_d_vec_b_fun$',type,
    'B_d_vec_b_fun$': $tType ).

tff('declare_B_d_vec_b_fun$1',type,
    'fmb_B_d_vec_b_fun$_1': 'B_d_vec_b_fun$' ).

tff('finite_domain_B_d_vec_b_fun$',axiom,
    ! [X: 'B_d_vec_b_fun$'] : ( X = 'fmb_B_d_vec_b_fun$_1' ) ).

tff('declare_B_d_vec_bool_fun$',type,
    'B_d_vec_bool_fun$': $tType ).

tff('declare_B_d_vec_bool_fun$1',type,
    'fmb_B_d_vec_bool_fun$_1': 'B_d_vec_bool_fun$' ).

tff('finite_domain_B_d_vec_bool_fun$',axiom,
    ! [X: 'B_d_vec_bool_fun$'] : ( X = 'fmb_B_d_vec_bool_fun$_1' ) ).

tff('declare_B_a_vec_a_vec$',type,
    'B_a_vec_a_vec$': $tType ).

tff('declare_B_a_vec_a_vec$1',type,
    'fmb_B_a_vec_a_vec$_1': 'B_a_vec_a_vec$' ).

tff('finite_domain_B_a_vec_a_vec$',axiom,
    ! [X: 'B_a_vec_a_vec$'] : ( X = 'fmb_B_a_vec_a_vec$_1' ) ).

tff('declare_B_c_vec_set$',type,
    'B_c_vec_set$': $tType ).

tff('declare_B_c_vec_set$1',type,
    'fmb_B_c_vec_set$_1': 'B_c_vec_set$' ).

tff('finite_domain_B_c_vec_set$',axiom,
    ! [X: 'B_c_vec_set$'] : ( X = 'fmb_B_c_vec_set$_1' ) ).

tff('declare_C_b_d_vec_fun$',type,
    'C_b_d_vec_fun$': $tType ).

tff('declare_C_b_d_vec_fun$1',type,
    'fmb_C_b_d_vec_fun$_1': 'C_b_d_vec_fun$' ).

tff('finite_domain_C_b_d_vec_fun$',axiom,
    ! [X: 'C_b_d_vec_fun$'] : ( X = 'fmb_C_b_d_vec_fun$_1' ) ).

tff('declare_B_d_vec_a_vec_c_vec$',type,
    'B_d_vec_a_vec_c_vec$': $tType ).

tff('declare_B_d_vec_a_vec_c_vec$1',type,
    'fmb_B_d_vec_a_vec_c_vec$_1': 'B_d_vec_a_vec_c_vec$' ).

tff('finite_domain_B_d_vec_a_vec_c_vec$',axiom,
    ! [X: 'B_d_vec_a_vec_c_vec$'] : ( X = 'fmb_B_d_vec_a_vec_c_vec$_1' ) ).

tff('declare_D_b_a_vec_fun$',type,
    'D_b_a_vec_fun$': $tType ).

tff('declare_D_b_a_vec_fun$1',type,
    'fmb_D_b_a_vec_fun$_1': 'D_b_a_vec_fun$' ).

tff('finite_domain_D_b_a_vec_fun$',axiom,
    ! [X: 'D_b_a_vec_fun$'] : ( X = 'fmb_D_b_a_vec_fun$_1' ) ).

tff('declare_B_c_vec_a_vec_c_vec$',type,
    'B_c_vec_a_vec_c_vec$': $tType ).

tff('declare_B_c_vec_a_vec_c_vec$1',type,
    'fmb_B_c_vec_a_vec_c_vec$_1': 'B_c_vec_a_vec_c_vec$' ).

tff('finite_domain_B_c_vec_a_vec_c_vec$',axiom,
    ! [X: 'B_c_vec_a_vec_c_vec$'] : ( X = 'fmb_B_c_vec_a_vec_c_vec$_1' ) ).

tff('declare_A_b_d_vec_bool_fun_fun$',type,
    'A_b_d_vec_bool_fun_fun$': $tType ).

tff('declare_A_b_d_vec_bool_fun_fun$1',type,
    'fmb_A_b_d_vec_bool_fun_fun$_1': 'A_b_d_vec_bool_fun_fun$' ).

tff('finite_domain_A_b_d_vec_bool_fun_fun$',axiom,
    ! [X: 'A_b_d_vec_bool_fun_fun$'] : ( X = 'fmb_A_b_d_vec_bool_fun_fun$_1' ) ).

tff('declare_C_b_a_vec_c_vec_fun$',type,
    'C_b_a_vec_c_vec_fun$': $tType ).

tff('declare_C_b_a_vec_c_vec_fun$1',type,
    'fmb_C_b_a_vec_c_vec_fun$_1': 'C_b_a_vec_c_vec_fun$' ).

tff('finite_domain_C_b_a_vec_c_vec_fun$',axiom,
    ! [X: 'C_b_a_vec_c_vec_fun$'] : ( X = 'fmb_C_b_a_vec_c_vec_fun$_1' ) ).

tff('declare_A_b_fun_set$',type,
    'A_b_fun_set$': $tType ).

tff('declare_A_b_fun_set$1',type,
    'fmb_A_b_fun_set$_1': 'A_b_fun_set$' ).

tff('finite_domain_A_b_fun_set$',axiom,
    ! [X: 'A_b_fun_set$'] : ( X = 'fmb_A_b_fun_set$_1' ) ).

tff('declare_B_b_fun$',type,
    'B_b_fun$': $tType ).

tff('declare_B_b_fun$1',type,
    'fmb_B_b_fun$_1': 'B_b_fun$' ).

tff('finite_domain_B_b_fun$',axiom,
    ! [X: 'B_b_fun$'] : ( X = 'fmb_B_b_fun$_1' ) ).

tff('declare_B_b_c_vec_fun$',type,
    'B_b_c_vec_fun$': $tType ).

tff('declare_B_b_c_vec_fun$1',type,
    'fmb_B_b_c_vec_fun$_1': 'B_b_c_vec_fun$' ).

tff('finite_domain_B_b_c_vec_fun$',axiom,
    ! [X: 'B_b_c_vec_fun$'] : ( X = 'fmb_B_b_c_vec_fun$_1' ) ).

tff('declare_A_b_a_vec_fun$',type,
    'A_b_a_vec_fun$': $tType ).

tff('declare_A_b_a_vec_fun$1',type,
    'fmb_A_b_a_vec_fun$_1': 'A_b_a_vec_fun$' ).

tff('finite_domain_A_b_a_vec_fun$',axiom,
    ! [X: 'A_b_a_vec_fun$'] : ( X = 'fmb_A_b_a_vec_fun$_1' ) ).

tff('declare_C_b_bool_fun_fun$',type,
    'C_b_bool_fun_fun$': $tType ).

tff('declare_C_b_bool_fun_fun$1',type,
    'fmb_C_b_bool_fun_fun$_1': 'C_b_bool_fun_fun$' ).

tff('finite_domain_C_b_bool_fun_fun$',axiom,
    ! [X: 'C_b_bool_fun_fun$'] : ( X = 'fmb_C_b_bool_fun_fun$_1' ) ).

tff('declare_D_b_fun$',type,
    'D_b_fun$': $tType ).

tff('declare_D_b_fun$1',type,
    'fmb_D_b_fun$_1': 'D_b_fun$' ).

tff('finite_domain_D_b_fun$',axiom,
    ! [X: 'D_b_fun$'] : ( X = 'fmb_D_b_fun$_1' ) ).

tff('declare_B_c_vec_bool_fun$',type,
    'B_c_vec_bool_fun$': $tType ).

tff('declare_B_c_vec_bool_fun$1',type,
    'fmb_B_c_vec_bool_fun$_1': 'B_c_vec_bool_fun$' ).

tff('finite_domain_B_c_vec_bool_fun$',axiom,
    ! [X: 'B_c_vec_bool_fun$'] : ( X = 'fmb_B_c_vec_bool_fun$_1' ) ).

tff('declare_A_b_d_vec_a_vec_fun$',type,
    'A_b_d_vec_a_vec_fun$': $tType ).

tff('declare_A_b_d_vec_a_vec_fun$1',type,
    'fmb_A_b_d_vec_a_vec_fun$_1': 'A_b_d_vec_a_vec_fun$' ).

tff('finite_domain_A_b_d_vec_a_vec_fun$',axiom,
    ! [X: 'A_b_d_vec_a_vec_fun$'] : ( X = 'fmb_A_b_d_vec_a_vec_fun$_1' ) ).

tff('declare_A_b_bool_fun_fun$',type,
    'A_b_bool_fun_fun$': $tType ).

tff('declare_A_b_bool_fun_fun$1',type,
    'fmb_A_b_bool_fun_fun$_1': 'A_b_bool_fun_fun$' ).

tff('finite_domain_A_b_bool_fun_fun$',axiom,
    ! [X: 'A_b_bool_fun_fun$'] : ( X = 'fmb_A_b_bool_fun_fun$_1' ) ).

tff('declare_C_b_a_vec_fun$',type,
    'C_b_a_vec_fun$': $tType ).

tff('declare_C_b_a_vec_fun$1',type,
    'fmb_C_b_a_vec_fun$_1': 'C_b_a_vec_fun$' ).

tff('finite_domain_C_b_a_vec_fun$',axiom,
    ! [X: 'C_b_a_vec_fun$'] : ( X = 'fmb_C_b_a_vec_fun$_1' ) ).

tff('declare_C_b_a_vec_fun_set$',type,
    'C_b_a_vec_fun_set$': $tType ).

tff('declare_C_b_a_vec_fun_set$1',type,
    'fmb_C_b_a_vec_fun_set$_1': 'C_b_a_vec_fun_set$' ).

tff('finite_domain_C_b_a_vec_fun_set$',axiom,
    ! [X: 'C_b_a_vec_fun_set$'] : ( X = 'fmb_C_b_a_vec_fun_set$_1' ) ).

tff('declare_B_a_vec_c_vec_c_vec$',type,
    'B_a_vec_c_vec_c_vec$': $tType ).

tff('declare_B_a_vec_c_vec_c_vec$1',type,
    'fmb_B_a_vec_c_vec_c_vec$_1': 'B_a_vec_c_vec_c_vec$' ).

tff('finite_domain_B_a_vec_c_vec_c_vec$',axiom,
    ! [X: 'B_a_vec_c_vec_c_vec$'] : ( X = 'fmb_B_a_vec_c_vec_c_vec$_1' ) ).

tff('declare_D$',type,
    'D$': $tType ).

tff('declare_D$1',type,
    'fmb_D$_1': 'D$' ).

tff('finite_domain_D$',axiom,
    ! [X: 'D$'] : ( X = 'fmb_D$_1' ) ).

tff('declare_C_b_a_vec_fun_bool_fun$',type,
    'C_b_a_vec_fun_bool_fun$': $tType ).

tff('declare_C_b_a_vec_fun_bool_fun$1',type,
    'fmb_C_b_a_vec_fun_bool_fun$_1': 'C_b_a_vec_fun_bool_fun$' ).

tff('finite_domain_C_b_a_vec_fun_bool_fun$',axiom,
    ! [X: 'C_b_a_vec_fun_bool_fun$'] : ( X = 'fmb_C_b_a_vec_fun_bool_fun$_1' ) ).

tff('declare_B_c_vec_b_fun$',type,
    'B_c_vec_b_fun$': $tType ).

tff('declare_B_c_vec_b_fun$1',type,
    'fmb_B_c_vec_b_fun$_1': 'B_c_vec_b_fun$' ).

tff('finite_domain_B_c_vec_b_fun$',axiom,
    ! [X: 'B_c_vec_b_fun$'] : ( X = 'fmb_B_c_vec_b_fun$_1' ) ).

tff('declare_B_d_vec_d_vec$',type,
    'B_d_vec_d_vec$': $tType ).

tff('declare_B_d_vec_d_vec$1',type,
    'fmb_B_d_vec_d_vec$_1': 'B_d_vec_d_vec$' ).

tff('finite_domain_B_d_vec_d_vec$',axiom,
    ! [X: 'B_d_vec_d_vec$'] : ( X = 'fmb_B_d_vec_d_vec$_1' ) ).

tff('declare_C_b_d_vec_a_vec_fun$',type,
    'C_b_d_vec_a_vec_fun$': $tType ).

tff('declare_C_b_d_vec_a_vec_fun$1',type,
    'fmb_C_b_d_vec_a_vec_fun$_1': 'C_b_d_vec_a_vec_fun$' ).

tff('finite_domain_C_b_d_vec_a_vec_fun$',axiom,
    ! [X: 'C_b_d_vec_a_vec_fun$'] : ( X = 'fmb_C_b_d_vec_a_vec_fun$_1' ) ).

tff('declare_A_b_d_vec_fun_bool_fun$',type,
    'A_b_d_vec_fun_bool_fun$': $tType ).

tff('declare_A_b_d_vec_fun_bool_fun$1',type,
    'fmb_A_b_d_vec_fun_bool_fun$_1': 'A_b_d_vec_fun_bool_fun$' ).

tff('finite_domain_A_b_d_vec_fun_bool_fun$',axiom,
    ! [X: 'A_b_d_vec_fun_bool_fun$'] : ( X = 'fmb_A_b_d_vec_fun_bool_fun$_1' ) ).

tff('declare_B_a_vec$',type,
    'B_a_vec$': $tType ).

tff('declare_B_a_vec$1',type,
    'fmb_B_a_vec$_1': 'B_a_vec$' ).

tff('finite_domain_B_a_vec$',axiom,
    ! [X: 'B_a_vec$'] : ( X = 'fmb_B_a_vec$_1' ) ).

tff('declare_B_c_vec_a_vec$',type,
    'B_c_vec_a_vec$': $tType ).

tff('declare_B_c_vec_a_vec$1',type,
    'fmb_B_c_vec_a_vec$_1': 'B_c_vec_a_vec$' ).

tff('finite_domain_B_c_vec_a_vec$',axiom,
    ! [X: 'B_c_vec_a_vec$'] : ( X = 'fmb_B_c_vec_a_vec$_1' ) ).

tff('declare_C_b_a_vec_bool_fun_fun$',type,
    'C_b_a_vec_bool_fun_fun$': $tType ).

tff('declare_C_b_a_vec_bool_fun_fun$1',type,
    'fmb_C_b_a_vec_bool_fun_fun$_1': 'C_b_a_vec_bool_fun_fun$' ).

tff('finite_domain_C_b_a_vec_bool_fun_fun$',axiom,
    ! [X: 'C_b_a_vec_bool_fun_fun$'] : ( X = 'fmb_C_b_a_vec_bool_fun_fun$_1' ) ).

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_B_a_vec_d_vec$',type,
    'B_a_vec_d_vec$': $tType ).

tff('declare_B_a_vec_d_vec$1',type,
    'fmb_B_a_vec_d_vec$_1': 'B_a_vec_d_vec$' ).

tff('finite_domain_B_a_vec_d_vec$',axiom,
    ! [X: 'B_a_vec_d_vec$'] : ( X = 'fmb_B_a_vec_d_vec$_1' ) ).

tff('declare_D_b_d_vec_fun$',type,
    'D_b_d_vec_fun$': $tType ).

tff('declare_D_b_d_vec_fun$1',type,
    'fmb_D_b_d_vec_fun$_1': 'D_b_d_vec_fun$' ).

tff('finite_domain_D_b_d_vec_fun$',axiom,
    ! [X: 'D_b_d_vec_fun$'] : ( X = 'fmb_D_b_d_vec_fun$_1' ) ).

tff('declare_B_d_vec_d_vec_a_vec$',type,
    'B_d_vec_d_vec_a_vec$': $tType ).

tff('declare_B_d_vec_d_vec_a_vec$1',type,
    'fmb_B_d_vec_d_vec_a_vec$_1': 'B_d_vec_d_vec_a_vec$' ).

tff('finite_domain_B_d_vec_d_vec_a_vec$',axiom,
    ! [X: 'B_d_vec_d_vec_a_vec$'] : ( X = 'fmb_B_d_vec_d_vec_a_vec$_1' ) ).

tff('declare_C$',type,
    'C$': $tType ).

tff('declare_C$1',type,
    'fmb_C$_1': 'C$' ).

tff('finite_domain_C$',axiom,
    ! [X: 'C$'] : ( X = 'fmb_C$_1' ) ).

tff('declare_B_c_vec_a_vec_set$',type,
    'B_c_vec_a_vec_set$': $tType ).

tff('declare_B_c_vec_a_vec_set$1',type,
    'fmb_B_c_vec_a_vec_set$_1': 'B_c_vec_a_vec_set$' ).

tff('finite_domain_B_c_vec_a_vec_set$',axiom,
    ! [X: 'B_c_vec_a_vec_set$'] : ( X = 'fmb_B_c_vec_a_vec_set$_1' ) ).

tff('declare_A_b_c_vec_fun_bool_fun$',type,
    'A_b_c_vec_fun_bool_fun$': $tType ).

tff('declare_A_b_c_vec_fun_bool_fun$1',type,
    'fmb_A_b_c_vec_fun_bool_fun$_1': 'A_b_c_vec_fun_bool_fun$' ).

tff('finite_domain_A_b_c_vec_fun_bool_fun$',axiom,
    ! [X: 'A_b_c_vec_fun_bool_fun$'] : ( X = 'fmb_A_b_c_vec_fun_bool_fun$_1' ) ).

tff('declare_D_b_d_vec_bool_fun_fun$',type,
    'D_b_d_vec_bool_fun_fun$': $tType ).

tff('declare_D_b_d_vec_bool_fun_fun$1',type,
    'fmb_D_b_d_vec_bool_fun_fun$_1': 'D_b_d_vec_bool_fun_fun$' ).

tff('finite_domain_D_b_d_vec_bool_fun_fun$',axiom,
    ! [X: 'D_b_d_vec_bool_fun_fun$'] : ( X = 'fmb_D_b_d_vec_bool_fun_fun$_1' ) ).

tff('declare_C_b_fun$',type,
    'C_b_fun$': $tType ).

tff('declare_C_b_fun$1',type,
    'fmb_C_b_fun$_1': 'C_b_fun$' ).

tff('finite_domain_C_b_fun$',axiom,
    ! [X: 'C_b_fun$'] : ( X = 'fmb_C_b_fun$_1' ) ).

tff('declare_A_b_a_vec_c_vec_fun$',type,
    'A_b_a_vec_c_vec_fun$': $tType ).

tff('declare_A_b_a_vec_c_vec_fun$1',type,
    'fmb_A_b_a_vec_c_vec_fun$_1': 'A_b_a_vec_c_vec_fun$' ).

tff('finite_domain_A_b_a_vec_c_vec_fun$',axiom,
    ! [X: 'A_b_a_vec_c_vec_fun$'] : ( X = 'fmb_A_b_a_vec_c_vec_fun$_1' ) ).

tff('declare_C_b_c_vec_fun$',type,
    'C_b_c_vec_fun$': $tType ).

tff('declare_C_b_c_vec_fun$1',type,
    'fmb_C_b_c_vec_fun$_1': 'C_b_c_vec_fun$' ).

tff('finite_domain_C_b_c_vec_fun$',axiom,
    ! [X: 'C_b_c_vec_fun$'] : ( X = 'fmb_C_b_c_vec_fun$_1' ) ).

tff('declare_B_a_vec_c_vec$',type,
    'B_a_vec_c_vec$': $tType ).

tff('declare_B_a_vec_c_vec$1',type,
    'fmb_B_a_vec_c_vec$_1': 'B_a_vec_c_vec$' ).

tff('finite_domain_B_a_vec_c_vec$',axiom,
    ! [X: 'B_a_vec_c_vec$'] : ( X = 'fmb_B_a_vec_c_vec$_1' ) ).

tff('declare_D_b_d_vec_fun_set$',type,
    'D_b_d_vec_fun_set$': $tType ).

tff('declare_D_b_d_vec_fun_set$1',type,
    'fmb_D_b_d_vec_fun_set$_1': 'D_b_d_vec_fun_set$' ).

tff('finite_domain_D_b_d_vec_fun_set$',axiom,
    ! [X: 'D_b_d_vec_fun_set$'] : ( X = 'fmb_D_b_d_vec_fun_set$_1' ) ).

tff('declare_B_d_vec_d_vec_d_vec$',type,
    'B_d_vec_d_vec_d_vec$': $tType ).

tff('declare_B_d_vec_d_vec_d_vec$1',type,
    'fmb_B_d_vec_d_vec_d_vec$_1': 'B_d_vec_d_vec_d_vec$' ).

tff('finite_domain_B_d_vec_d_vec_d_vec$',axiom,
    ! [X: 'B_d_vec_d_vec_d_vec$'] : ( X = 'fmb_B_d_vec_d_vec_d_vec$_1' ) ).

tff('declare_D_b_d_vec_fun_bool_fun$',type,
    'D_b_d_vec_fun_bool_fun$': $tType ).

tff('declare_D_b_d_vec_fun_bool_fun$1',type,
    'fmb_D_b_d_vec_fun_bool_fun$_1': 'D_b_d_vec_fun_bool_fun$' ).

tff('finite_domain_D_b_d_vec_fun_bool_fun$',axiom,
    ! [X: 'D_b_d_vec_fun_bool_fun$'] : ( X = 'fmb_D_b_d_vec_fun_bool_fun$_1' ) ).

tff('declare_A_b_d_vec_fun$',type,
    'A_b_d_vec_fun$': $tType ).

tff('declare_A_b_d_vec_fun$1',type,
    'fmb_A_b_d_vec_fun$_1': 'A_b_d_vec_fun$' ).

tff('finite_domain_A_b_d_vec_fun$',axiom,
    ! [X: 'A_b_d_vec_fun$'] : ( X = 'fmb_A_b_d_vec_fun$_1' ) ).

tff('declare_D_b_c_vec_fun$',type,
    'D_b_c_vec_fun$': $tType ).

tff('declare_D_b_c_vec_fun$1',type,
    'fmb_D_b_c_vec_fun$_1': 'D_b_c_vec_fun$' ).

tff('finite_domain_D_b_c_vec_fun$',axiom,
    ! [X: 'D_b_c_vec_fun$'] : ( X = 'fmb_D_b_c_vec_fun$_1' ) ).

tff('declare_D_b_fun_bool_fun$',type,
    'D_b_fun_bool_fun$': $tType ).

tff('declare_D_b_fun_bool_fun$1',type,
    'fmb_D_b_fun_bool_fun$_1': 'D_b_fun_bool_fun$' ).

tff('finite_domain_D_b_fun_bool_fun$',axiom,
    ! [X: 'D_b_fun_bool_fun$'] : ( X = 'fmb_D_b_fun_bool_fun$_1' ) ).

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_C_b_fun_set$',type,
    'C_b_fun_set$': $tType ).

tff('declare_C_b_fun_set$1',type,
    'fmb_C_b_fun_set$_1': 'C_b_fun_set$' ).

tff('finite_domain_C_b_fun_set$',axiom,
    ! [X: 'C_b_fun_set$'] : ( X = 'fmb_C_b_fun_set$_1' ) ).

tff('declare_B_d_vec_a_vec_set$',type,
    'B_d_vec_a_vec_set$': $tType ).

tff('declare_B_d_vec_a_vec_set$1',type,
    'fmb_B_d_vec_a_vec_set$_1': 'B_d_vec_a_vec_set$' ).

tff('finite_domain_B_d_vec_a_vec_set$',axiom,
    ! [X: 'B_d_vec_a_vec_set$'] : ( X = 'fmb_B_d_vec_a_vec_set$_1' ) ).

tff('declare_B_d_vec_a_vec_a_vec$',type,
    'B_d_vec_a_vec_a_vec$': $tType ).

tff('declare_B_d_vec_a_vec_a_vec$1',type,
    'fmb_B_d_vec_a_vec_a_vec$_1': 'B_d_vec_a_vec_a_vec$' ).

tff('finite_domain_B_d_vec_a_vec_a_vec$',axiom,
    ! [X: 'B_d_vec_a_vec_a_vec$'] : ( X = 'fmb_B_d_vec_a_vec_a_vec$_1' ) ).

tff('declare_A_b_c_vec_fun$',type,
    'A_b_c_vec_fun$': $tType ).

tff('declare_A_b_c_vec_fun$1',type,
    'fmb_A_b_c_vec_fun$_1': 'A_b_c_vec_fun$' ).

tff('declare_A_b_c_vec_fun$2',type,
    'fmb_A_b_c_vec_fun$_2': 'A_b_c_vec_fun$' ).

tff('finite_domain_A_b_c_vec_fun$',axiom,
    ! [X: 'A_b_c_vec_fun$'] :
      ( ( X = 'fmb_A_b_c_vec_fun$_1' )
      | ( X = 'fmb_A_b_c_vec_fun$_2' ) ) ).

tff('distinct_domain_A_b_c_vec_fun$',axiom,
    'fmb_A_b_c_vec_fun$_1' != 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_A_b_c_vec_a_vec_fun$',type,
    'A_b_c_vec_a_vec_fun$': $tType ).

tff('declare_A_b_c_vec_a_vec_fun$1',type,
    'fmb_A_b_c_vec_a_vec_fun$_1': 'A_b_c_vec_a_vec_fun$' ).

tff('finite_domain_A_b_c_vec_a_vec_fun$',axiom,
    ! [X: 'A_b_c_vec_a_vec_fun$'] : ( X = 'fmb_A_b_c_vec_a_vec_fun$_1' ) ).

tff('declare_B_d_vec_a_vec$',type,
    'B_d_vec_a_vec$': $tType ).

tff('declare_B_d_vec_a_vec$1',type,
    'fmb_B_d_vec_a_vec$_1': 'B_d_vec_a_vec$' ).

tff('finite_domain_B_d_vec_a_vec$',axiom,
    ! [X: 'B_d_vec_a_vec$'] : ( X = 'fmb_B_d_vec_a_vec$_1' ) ).

tff('declare_D_b_bool_fun_fun$',type,
    'D_b_bool_fun_fun$': $tType ).

tff('declare_D_b_bool_fun_fun$1',type,
    'fmb_D_b_bool_fun_fun$_1': 'D_b_bool_fun_fun$' ).

tff('finite_domain_D_b_bool_fun_fun$',axiom,
    ! [X: 'D_b_bool_fun_fun$'] : ( X = 'fmb_D_b_bool_fun_fun$_1' ) ).

tff('declare_A_b_c_vec_bool_fun_fun$',type,
    'A_b_c_vec_bool_fun_fun$': $tType ).

tff('declare_A_b_c_vec_bool_fun_fun$1',type,
    'fmb_A_b_c_vec_bool_fun_fun$_1': 'A_b_c_vec_bool_fun_fun$' ).

tff('finite_domain_A_b_c_vec_bool_fun_fun$',axiom,
    ! [X: 'A_b_c_vec_bool_fun_fun$'] : ( X = 'fmb_A_b_c_vec_bool_fun_fun$_1' ) ).

tff('declare_B_b_d_vec_fun$',type,
    'B_b_d_vec_fun$': $tType ).

tff('declare_B_b_d_vec_fun$1',type,
    'fmb_B_b_d_vec_fun$_1': 'B_b_d_vec_fun$' ).

tff('finite_domain_B_b_d_vec_fun$',axiom,
    ! [X: 'B_b_d_vec_fun$'] : ( X = 'fmb_B_b_d_vec_fun$_1' ) ).

tff('declare_B_d_vec_a_vec_bool_fun$',type,
    'B_d_vec_a_vec_bool_fun$': $tType ).

tff('declare_B_d_vec_a_vec_bool_fun$1',type,
    'fmb_B_d_vec_a_vec_bool_fun$_1': 'B_d_vec_a_vec_bool_fun$' ).

tff('finite_domain_B_d_vec_a_vec_bool_fun$',axiom,
    ! [X: 'B_d_vec_a_vec_bool_fun$'] : ( X = 'fmb_B_d_vec_a_vec_bool_fun$_1' ) ).

tff('declare_B_d_vec_c_vec$',type,
    'B_d_vec_c_vec$': $tType ).

tff('declare_B_d_vec_c_vec$1',type,
    'fmb_B_d_vec_c_vec$_1': 'B_d_vec_c_vec$' ).

tff('finite_domain_B_d_vec_c_vec$',axiom,
    ! [X: 'B_d_vec_c_vec$'] : ( X = 'fmb_B_d_vec_c_vec$_1' ) ).

tff('declare_A_b_c_vec_a_vec_bool_fun_fun$',type,
    'A_b_c_vec_a_vec_bool_fun_fun$': $tType ).

tff('declare_A_b_c_vec_a_vec_bool_fun_fun$1',type,
    'fmb_A_b_c_vec_a_vec_bool_fun_fun$_1': 'A_b_c_vec_a_vec_bool_fun_fun$' ).

tff('finite_domain_A_b_c_vec_a_vec_bool_fun_fun$',axiom,
    ! [X: 'A_b_c_vec_a_vec_bool_fun_fun$'] : ( X = 'fmb_A_b_c_vec_a_vec_bool_fun_fun$_1' ) ).

tff('declare_B_c_vec_a_vec_a_vec$',type,
    'B_c_vec_a_vec_a_vec$': $tType ).

tff('declare_B_c_vec_a_vec_a_vec$1',type,
    'fmb_B_c_vec_a_vec_a_vec$_1': 'B_c_vec_a_vec_a_vec$' ).

tff('finite_domain_B_c_vec_a_vec_a_vec$',axiom,
    ! [X: 'B_c_vec_a_vec_a_vec$'] : ( X = 'fmb_B_c_vec_a_vec_a_vec$_1' ) ).

tff('declare_A_b_fun$',type,
    'A_b_fun$': $tType ).

tff('declare_A_b_fun$1',type,
    'fmb_A_b_fun$_1': 'A_b_fun$' ).

tff('finite_domain_A_b_fun$',axiom,
    ! [X: 'A_b_fun$'] : ( X = 'fmb_A_b_fun$_1' ) ).

tff('declare_B_set$',type,
    'B_set$': $tType ).

tff('declare_B_set$1',type,
    'fmb_B_set$_1': 'B_set$' ).

tff('finite_domain_B_set$',axiom,
    ! [X: 'B_set$'] : ( X = 'fmb_B_set$_1' ) ).

tff('declare_A_b_fun_bool_fun$',type,
    'A_b_fun_bool_fun$': $tType ).

tff('declare_A_b_fun_bool_fun$1',type,
    'fmb_A_b_fun_bool_fun$_1': 'A_b_fun_bool_fun$' ).

tff('finite_domain_A_b_fun_bool_fun$',axiom,
    ! [X: 'A_b_fun_bool_fun$'] : ( X = 'fmb_A_b_fun_bool_fun$_1' ) ).

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

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

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

tff('declare_D_b_fun_set$',type,
    'D_b_fun_set$': $tType ).

tff('declare_D_b_fun_set$1',type,
    'fmb_D_b_fun_set$_1': 'D_b_fun_set$' ).

tff('finite_domain_D_b_fun_set$',axiom,
    ! [X: 'D_b_fun_set$'] : ( X = 'fmb_D_b_fun_set$_1' ) ).

tff('declare_C_b_fun_bool_fun$',type,
    'C_b_fun_bool_fun$': $tType ).

tff('declare_C_b_fun_bool_fun$1',type,
    'fmb_C_b_fun_bool_fun$_1': 'C_b_fun_bool_fun$' ).

tff('finite_domain_C_b_fun_bool_fun$',axiom,
    ! [X: 'C_b_fun_bool_fun$'] : ( X = 'fmb_C_b_fun_bool_fun$_1' ) ).

tff('declare_B_a_vec_b_fun$',type,
    'B_a_vec_b_fun$': $tType ).

tff('declare_B_a_vec_b_fun$1',type,
    'fmb_B_a_vec_b_fun$_1': 'B_a_vec_b_fun$' ).

tff('finite_domain_B_a_vec_b_fun$',axiom,
    ! [X: 'B_a_vec_b_fun$'] : ( X = 'fmb_B_a_vec_b_fun$_1' ) ).

tff('declare_B_c_vec_c_vec$',type,
    'B_c_vec_c_vec$': $tType ).

tff('declare_B_c_vec_c_vec$1',type,
    'fmb_B_c_vec_c_vec$_1': 'B_c_vec_c_vec$' ).

tff('finite_domain_B_c_vec_c_vec$',axiom,
    ! [X: 'B_c_vec_c_vec$'] : ( X = 'fmb_B_c_vec_c_vec$_1' ) ).

tff('declare_B_a_vec_c_vec_a_vec$',type,
    'B_a_vec_c_vec_a_vec$': $tType ).

tff('declare_B_a_vec_c_vec_a_vec$1',type,
    'fmb_B_a_vec_c_vec_a_vec$_1': 'B_a_vec_c_vec_a_vec$' ).

tff('finite_domain_B_a_vec_c_vec_a_vec$',axiom,
    ! [X: 'B_a_vec_c_vec_a_vec$'] : ( X = 'fmb_B_a_vec_c_vec_a_vec$_1' ) ).

tff('declare_A_b_c_vec_fun_set$',type,
    'A_b_c_vec_fun_set$': $tType ).

tff('declare_A_b_c_vec_fun_set$1',type,
    'fmb_A_b_c_vec_fun_set$_1': 'A_b_c_vec_fun_set$' ).

tff('finite_domain_A_b_c_vec_fun_set$',axiom,
    ! [X: 'A_b_c_vec_fun_set$'] : ( X = 'fmb_A_b_c_vec_fun_set$_1' ) ).

tff('declare_B_c_vec_a_vec_a_vec_bool_fun$',type,
    'B_c_vec_a_vec_a_vec_bool_fun$': $tType ).

tff('declare_B_c_vec_a_vec_a_vec_bool_fun$1',type,
    'fmb_B_c_vec_a_vec_a_vec_bool_fun$_1': 'B_c_vec_a_vec_a_vec_bool_fun$' ).

tff('finite_domain_B_c_vec_a_vec_a_vec_bool_fun$',axiom,
    ! [X: 'B_c_vec_a_vec_a_vec_bool_fun$'] : ( X = 'fmb_B_c_vec_a_vec_a_vec_bool_fun$_1' ) ).

tff('declare_B_d_vec$',type,
    'B_d_vec$': $tType ).

tff('declare_B_d_vec$1',type,
    'fmb_B_d_vec$_1': 'B_d_vec$' ).

tff('finite_domain_B_d_vec$',axiom,
    ! [X: 'B_d_vec$'] : ( X = 'fmb_B_d_vec$_1' ) ).

tff('declare_B_a_vec_bool_fun$',type,
    'B_a_vec_bool_fun$': $tType ).

tff('declare_B_a_vec_bool_fun$1',type,
    'fmb_B_a_vec_bool_fun$_1': 'B_a_vec_bool_fun$' ).

tff('finite_domain_B_a_vec_bool_fun$',axiom,
    ! [X: 'B_a_vec_bool_fun$'] : ( X = 'fmb_B_a_vec_bool_fun$_1' ) ).

tff('declare_B_c_vec_a_vec_bool_fun$',type,
    'B_c_vec_a_vec_bool_fun$': $tType ).

tff('declare_B_c_vec_a_vec_bool_fun$1',type,
    'fmb_B_c_vec_a_vec_bool_fun$_1': 'B_c_vec_a_vec_bool_fun$' ).

tff('finite_domain_B_c_vec_a_vec_bool_fun$',axiom,
    ! [X: 'B_c_vec_a_vec_bool_fun$'] : ( X = 'fmb_B_c_vec_a_vec_bool_fun$_1' ) ).

tff('declare_B_c_vec$',type,
    'B_c_vec$': $tType ).

tff('declare_B_c_vec$1',type,
    'fmb_B_c_vec$_1': 'B_c_vec$' ).

tff('finite_domain_B_c_vec$',axiom,
    ! [X: 'B_c_vec$'] : ( X = 'fmb_B_c_vec$_1' ) ).

tff('declare_A_b_c_vec_a_vec_fun_bool_fun$',type,
    'A_b_c_vec_a_vec_fun_bool_fun$': $tType ).

tff('declare_A_b_c_vec_a_vec_fun_bool_fun$1',type,
    'fmb_A_b_c_vec_a_vec_fun_bool_fun$_1': 'A_b_c_vec_a_vec_fun_bool_fun$' ).

tff('finite_domain_A_b_c_vec_a_vec_fun_bool_fun$',axiom,
    ! [X: 'A_b_c_vec_a_vec_fun_bool_fun$'] : ( X = 'fmb_A_b_c_vec_a_vec_fun_bool_fun$_1' ) ).

tff('declare_B_a_vec_c_vec_bool_fun$',type,
    'B_a_vec_c_vec_bool_fun$': $tType ).

tff('declare_B_a_vec_c_vec_bool_fun$1',type,
    'fmb_B_a_vec_c_vec_bool_fun$_1': 'B_a_vec_c_vec_bool_fun$' ).

tff('finite_domain_B_a_vec_c_vec_bool_fun$',axiom,
    ! [X: 'B_a_vec_c_vec_bool_fun$'] : ( X = 'fmb_B_a_vec_c_vec_bool_fun$_1' ) ).

tff('declare_A_b_c_vec_a_vec_fun_set$',type,
    'A_b_c_vec_a_vec_fun_set$': $tType ).

tff('declare_A_b_c_vec_a_vec_fun_set$1',type,
    'fmb_A_b_c_vec_a_vec_fun_set$_1': 'A_b_c_vec_a_vec_fun_set$' ).

tff('finite_domain_A_b_c_vec_a_vec_fun_set$',axiom,
    ! [X: 'A_b_c_vec_a_vec_fun_set$'] : ( X = 'fmb_A_b_c_vec_a_vec_fun_set$_1' ) ).

tff('declare_B_b_a_vec_fun$',type,
    'B_b_a_vec_fun$': $tType ).

tff('declare_B_b_a_vec_fun$1',type,
    'fmb_B_b_a_vec_fun$_1': 'B_b_a_vec_fun$' ).

tff('finite_domain_B_b_a_vec_fun$',axiom,
    ! [X: 'B_b_a_vec_fun$'] : ( X = 'fmb_B_b_a_vec_fun$_1' ) ).

tff('declare_B_d_vec_set$',type,
    'B_d_vec_set$': $tType ).

tff('declare_B_d_vec_set$1',type,
    'fmb_B_d_vec_set$_1': 'B_d_vec_set$' ).

tff('finite_domain_B_d_vec_set$',axiom,
    ! [X: 'B_d_vec_set$'] : ( X = 'fmb_B_d_vec_set$_1' ) ).

tff('declare_A_b_d_vec_fun_set$',type,
    'A_b_d_vec_fun_set$': $tType ).

tff('declare_A_b_d_vec_fun_set$1',type,
    'fmb_A_b_d_vec_fun_set$_1': 'A_b_d_vec_fun_set$' ).

tff('finite_domain_A_b_d_vec_fun_set$',axiom,
    ! [X: 'A_b_d_vec_fun_set$'] : ( X = 'fmb_A_b_d_vec_fun_set$_1' ) ).

tff('declare_B_c_vec_d_vec$',type,
    'B_c_vec_d_vec$': $tType ).

tff('declare_B_c_vec_d_vec$1',type,
    'fmb_B_c_vec_d_vec$_1': 'B_c_vec_d_vec$' ).

tff('finite_domain_B_c_vec_d_vec$',axiom,
    ! [X: 'B_c_vec_d_vec$'] : ( X = 'fmb_B_c_vec_d_vec$_1' ) ).

tff('declare_B_bool_fun$',type,
    'B_bool_fun$': $tType ).

tff('declare_B_bool_fun$1',type,
    'fmb_B_bool_fun$_1': 'B_bool_fun$' ).

tff('finite_domain_B_bool_fun$',axiom,
    ! [X: 'B_bool_fun$'] : ( X = 'fmb_B_bool_fun$_1' ) ).

tff('declare_uminus$',type,
    'uminus$': 'B_b_fun$' ).

tff('uminus$_definition',axiom,
    'uminus$' = 'fmb_B_b_fun$_1' ).

tff('declare_top$',type,
    'top$': 'A_b_c_vec_a_vec_fun_set$' ).

tff('top$_definition',axiom,
    'top$' = 'fmb_A_b_c_vec_a_vec_fun_set$_1' ).

tff('declare_top$e',type,
    'top$e': 'A_b_c_vec_fun_set$' ).

tff('top$e_definition',axiom,
    'top$e' = 'fmb_A_b_c_vec_fun_set$_1' ).

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

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

tff('declare_top$a',type,
    'top$a': 'D_b_d_vec_fun_set$' ).

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

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

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

tff('declare_vec$g',type,
    'vec$g': 'B_b_a_vec_fun$' ).

tff('vec$g_definition',axiom,
    'vec$g' = 'fmb_B_b_a_vec_fun$_1' ).

tff(declare_tltrue,type,
    tltrue: tlbool ).

tff(tltrue_definition,axiom,
    tltrue = fmb_tlbool_1 ).

tff('declare_vec$',type,
    'vec$': 'B_b_c_vec_fun$' ).

tff('vec$_definition',axiom,
    'vec$' = 'fmb_B_b_c_vec_fun$_1' ).

tff('declare_top$b',type,
    'top$b': 'C_b_a_vec_fun_set$' ).

tff('top$b_definition',axiom,
    'top$b' = 'fmb_C_b_a_vec_fun_set$_1' ).

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

tff('a$_definition',axiom,
    'a$' = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_b$',type,
    'b$': 'B_d_vec_a_vec$' ).

tff('b$_definition',axiom,
    'b$' = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_top$c',type,
    'top$c': 'C_b_fun_set$' ).

tff('top$c_definition',axiom,
    'top$c' = 'fmb_C_b_fun_set$_1' ).

tff('declare_vec$b',type,
    'vec$b': 'B_b_d_vec_fun$' ).

tff('vec$b_definition',axiom,
    'vec$b' = 'fmb_B_b_d_vec_fun$_1' ).

tff('declare_top$g',type,
    'top$g': 'A_b_d_vec_fun_set$' ).

tff('top$g_definition',axiom,
    'top$g' = 'fmb_A_b_d_vec_fun_set$_1' ).

tff(declare_tlfalse,type,
    tlfalse: tlbool ).

tff(tlfalse_definition,axiom,
    tlfalse = fmb_tlbool_2 ).

tff('declare_top$f',type,
    'top$f': 'D_b_fun_set$' ).

tff('top$f_definition',axiom,
    'top$f' = 'fmb_D_b_fun_set$_1' ).

tff('declare_top$d',type,
    'top$d': 'A_b_fun_set$' ).

tff('top$d_definition',axiom,
    'top$d' = 'fmb_A_b_fun_set$_1' ).

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

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

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

tff('function_uminus$h',axiom,
    'uminus$h'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_uxq$',type,
    'uxq$': ( 'B_d_vec$' * 'D$' ) > 'C_b_fun$' ).

tff('function_uxq$',axiom,
    'uxq$'('fmb_B_d_vec$_1','fmb_D$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$i',type,
    'gauss_Jordan_wrapper$i': ( 'C$' * 'C$' * 'B_a_vec_c_vec$' * 'B_c_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_gauss_Jordan_wrapper$i',axiom,
    'gauss_Jordan_wrapper$i'('fmb_C$_1','fmb_C$_1','fmb_B_a_vec_c_vec$_1','fmb_B_c_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_mult_column_row$d',type,
    'mult_column_row$d': ( 'B_d_vec_a_vec$' * 'D$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_mult_column_row$d',axiom,
    'mult_column_row$d'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uxd$',type,
    'uxd$': ( 'D$' * 'B_d_vec_a_vec$' ) > 'A_b_fun$' ).

tff('function_uxd$',axiom,
    'uxd$'('fmb_D$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_fun_app$z',type,
    'fun_app$z': ( 'B_b_c_vec_fun$' * 'B$' ) > 'B_c_vec$' ).

tff('function_fun_app$z',axiom,
    'fun_app$z'('fmb_B_b_c_vec_fun$_1','fmb_B$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_uvs$',type,
    'uvs$': 'B_c_vec$' > 'A_b_c_vec_fun$' ).

tff('function_uvs$',axiom,
    'uvs$'('fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uza$',type,
    'uza$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_uza$',axiom,
    'uza$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uys$',type,
    'uys$': ( 'B_a_vec_c_vec$' * 'A$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_uys$',axiom,
    'uys$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_columnvector$d',type,
    'columnvector$d': 'B_d_vec$' > 'B_a_vec_d_vec$' ).

tff('function_columnvector$d',axiom,
    'columnvector$d'('fmb_B_d_vec$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_vap$',type,
    'vap$': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_vap$',axiom,
    'vap$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uuf$',type,
    'uuf$': ( 'D$' * 'C$' * 'B_d_vec_d_vec$' * 'B_c_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_uuf$',axiom,
    'uuf$'('fmb_D$_1','fmb_C$_1','fmb_B_d_vec_d_vec$_1','fmb_B_c_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_transpose$g',type,
    'transpose$g': 'B_a_vec_a_vec$' > 'B_a_vec_a_vec$' ).

tff('function_transpose$g',axiom,
    'transpose$g'('fmb_B_a_vec_a_vec$_1') = 'fmb_B_a_vec_a_vec$_1' ).

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

tff('function_uminus$g',axiom,
    'uminus$g'('fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vec_lambda$f',type,
    'vec_lambda$f': 'D_b_d_vec_fun$' > 'B_d_vec_d_vec$' ).

tff('function_vec_lambda$f',axiom,
    'vec_lambda$f'('fmb_D_b_d_vec_fun$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uxw$',type,
    'uxw$': ( 'B_a_vec$' * 'A$' ) > 'A_b_fun$' ).

tff('function_uxw$',axiom,
    'uxw$'('fmb_B_a_vec$_1','fmb_A$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uug$',type,
    'uug$': ( 'D$' * 'A$' * 'B_d_vec_d_vec$' * 'B_a_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_uug$',axiom,
    'uug$'('fmb_D$_1','fmb_A$_1','fmb_B_d_vec_d_vec$_1','fmb_B_a_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uyh$',type,
    'uyh$': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' ) > 'C_b_a_vec_fun$' ).

tff('function_uyh$',axiom,
    'uyh$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$',type,
    'gauss_Jordan_wrapper$': ( 'A$' * 'C$' * 'B_d_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_gauss_Jordan_wrapper$',axiom,
    'gauss_Jordan_wrapper$'('fmb_A$_1','fmb_C$_1','fmb_B_d_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_column_add$a',type,
    'column_add$a': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' * 'B$' ) > 'B_a_vec_c_vec$' ).

tff('function_column_add$a',axiom,
    'column_add$a'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uww$',type,
    'uww$': 'B_d_vec_d_vec$' > 'D_b_d_vec_fun$' ).

tff('function_uww$',axiom,
    'uww$'('fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_fun_app$an',type,
    'fun_app$an': ( 'A_b_d_vec_bool_fun_fun$' * 'A$' ) > 'B_d_vec_bool_fun$' ).

tff('function_fun_app$an',axiom,
    'fun_app$an'('fmb_A_b_d_vec_bool_fun_fun$_1','fmb_A$_1') = 'fmb_B_d_vec_bool_fun$_1' ).

tff('declare_vaz$',type,
    'vaz$': ( 'B_d_vec$' * 'B_d_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_vaz$',axiom,
    'vaz$'('fmb_B_d_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_transpose$e',type,
    'transpose$e': 'B_d_vec_c_vec$' > 'B_c_vec_d_vec$' ).

tff('function_transpose$e',axiom,
    'transpose$e'('fmb_B_d_vec_c_vec$_1') = 'fmb_B_c_vec_d_vec$_1' ).

tff('declare_uyb$',type,
    'uyb$': 'B_a_vec$' > 'A_b_d_vec_fun$' ).

tff('function_uyb$',axiom,
    'uyb$'('fmb_B_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uzh$',type,
    'uzh$': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' * 'B$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uzh$',axiom,
    'uzh$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_plus$i',type,
    'plus$i': ( 'A_b_d_vec_fun$' * 'A_b_d_vec_fun$' ) > 'A_b_d_vec_fun$' ).

tff('function_plus$i',axiom,
    'plus$i'('fmb_A_b_d_vec_fun$_1','fmb_A_b_d_vec_fun$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_val$',type,
    'val$': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' * 'B$' * 'C$' ) > 'A_b_fun$' ).

tff('function_val$',axiom,
    'val$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_mult_column_row$c',type,
    'mult_column_row$c': ( 'B_c_vec_a_vec$' * 'C$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_mult_column_row$c',axiom,
    'mult_column_row$c'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uvw$',type,
    'uvw$': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uvw$',axiom,
    'uvw$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vec_nth$e',type,
    'vec_nth$e': 'B_d_vec_c_vec$' > 'C_b_d_vec_fun$' ).

tff('function_vec_nth$e',axiom,
    'vec_nth$e'('fmb_B_d_vec_c_vec$_1') = 'fmb_C_b_d_vec_fun$_1' ).

tff('declare_uuu$',type,
    'uuu$': ( 'B_b_fun$' * 'B_c_vec_a_vec$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uuu$',axiom,
    'uuu$'('fmb_B_b_fun$_1','fmb_B_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_plus$b',type,
    'plus$b': ( 'B_c_vec$' * 'B_c_vec$' ) > 'B_c_vec$' ).

tff('function_plus$b',axiom,
    'plus$b'('fmb_B_c_vec$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_uvh$',type,
    'uvh$': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_a_vec$' ) > 'A_b_a_vec_fun$' ).

tff('function_uvh$',axiom,
    'uvh$'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_a_vec_fun$_1' ).

tff('declare_uyw$',type,
    'uyw$': ( 'B_d_vec_a_vec$' * 'D$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_uyw$',axiom,
    'uyw$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_times$b',type,
    'times$b': ( 'B_c_vec$' * 'B_c_vec$' ) > 'B_c_vec$' ).

tff('function_times$b',axiom,
    'times$b'('fmb_B_c_vec$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_row$e',type,
    'row$e': ( 'D$' * 'B_a_vec_d_vec$' ) > 'B_a_vec$' ).

tff('function_row$e',axiom,
    'row$e'('fmb_D$_1','fmb_B_a_vec_d_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_gauss_Jordan_wrapper$f',type,
    'gauss_Jordan_wrapper$f': ( 'D$' * 'A$' * 'B_d_vec_d_vec$' * 'B_a_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_gauss_Jordan_wrapper$f',axiom,
    'gauss_Jordan_wrapper$f'('fmb_D$_1','fmb_A$_1','fmb_B_d_vec_d_vec$_1','fmb_B_a_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_elt_set_plus$e',type,
    'elt_set_plus$e': ( 'B_d_vec$' * 'B_d_vec_set$' ) > 'B_d_vec_set$' ).

tff('function_elt_set_plus$e',axiom,
    'elt_set_plus$e'('fmb_B_d_vec$_1','fmb_B_d_vec_set$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_fun_app$ac',type,
    'fun_app$ac': ( 'A_b_c_vec_a_vec_bool_fun_fun$' * 'A$' ) > 'B_c_vec_a_vec_bool_fun$' ).

tff('function_fun_app$ac',axiom,
    'fun_app$ac'('fmb_A_b_c_vec_a_vec_bool_fun_fun$_1','fmb_A$_1') = 'fmb_B_c_vec_a_vec_bool_fun$_1' ).

tff('declare_map_matrix$i',type,
    'map_matrix$i': ( 'B_d_vec_b_fun$' * 'B_d_vec_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_map_matrix$i',axiom,
    'map_matrix$i'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_columnvector$e',type,
    'columnvector$e': 'B_a_vec$' > 'B_a_vec_a_vec$' ).

tff('function_columnvector$e',axiom,
    'columnvector$e'('fmb_B_a_vec$_1') = 'fmb_B_a_vec_a_vec$_1' ).

tff('declare_uwd$',type,
    'uwd$': ( 'B_c_vec_a_vec$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uwd$',axiom,
    'uwd$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uyf$',type,
    'uyf$': 'B_d_vec_a_vec$' > 'A_b_d_vec_a_vec_fun$' ).

tff('function_uyf$',axiom,
    'uyf$'('fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_a_vec_fun$_1' ).

tff('declare_uxn$',type,
    'uxn$': 'B_a_vec$' > 'A_b_c_vec_fun$' ).

tff('function_uxn$',axiom,
    'uxn$'('fmb_B_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_times$k',type,
    'times$k': ( 'D_b_fun$' * 'D_b_fun$' ) > 'D_b_fun$' ).

tff('function_times$k',axiom,
    'times$k'('fmb_D_b_fun$_1','fmb_D_b_fun$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_columnvector_row$b',type,
    'columnvector_row$b': 'B_d_vec$' > 'D_b_c_vec_fun$' ).

tff('function_columnvector_row$b',axiom,
    'columnvector_row$b'('fmb_B_d_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_uyg$',type,
    'uyg$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'D_b_d_vec_fun$' ).

tff('function_uyg$',axiom,
    'uyg$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_vec_nth$o',type,
    'vec_nth$o': ( 'B_d_vec_a_vec_c_vec$' * 'C$' ) > 'B_d_vec_a_vec$' ).

tff('function_vec_nth$o',axiom,
    'vec_nth$o'('fmb_B_d_vec_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_plus$h',type,
    'plus$h': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_plus$h',axiom,
    'plus$h'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_plus$o',type,
    'plus$o': ( 'B_set$' * 'B_set$' ) > 'B_set$' ).

tff('function_plus$o',axiom,
    'plus$o'('fmb_B_set$_1','fmb_B_set$_1') = 'fmb_B_set$_1' ).

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

tff('function_mult_row$c',axiom,
    'mult_row$c'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vaj$',type,
    'vaj$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' * 'D$' ) > 'D_b_fun$' ).

tff('function_vaj$',axiom,
    'vaj$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_mult_row$d',type,
    'mult_row$d': ( 'B_c_vec_a_vec$' * 'A$' * 'B$' ) > 'B_c_vec_a_vec$' ).

tff('function_mult_row$d',axiom,
    'mult_row$d'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uxa$',type,
    'uxa$': 'B_a_vec_d_vec$' > 'A_b_d_vec_fun$' ).

tff('function_uxa$',axiom,
    'uxa$'('fmb_B_a_vec_d_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_plus$k',type,
    'plus$k': ( 'D_b_fun$' * 'D_b_fun$' ) > 'D_b_fun$' ).

tff('function_plus$k',axiom,
    'plus$k'('fmb_D_b_fun$_1','fmb_D_b_fun$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uuq$',type,
    'uuq$': 'B_a_vec_c_vec$' > 'C_b_a_vec_fun$' ).

tff('function_uuq$',axiom,
    'uuq$'('fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_column$a',type,
    'column$a': ( 'D$' * 'B_d_vec_a_vec$' ) > 'B_a_vec$' ).

tff('function_column$a',axiom,
    'column$a'('fmb_D$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uwf$',type,
    'uwf$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uwf$',axiom,
    'uwf$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

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

tff('function_uminus$j',axiom,
    'uminus$j'('fmb_B_c_vec_d_vec$_1') = 'fmb_B_c_vec_d_vec$_1' ).

tff('declare_uus$',type,
    'uus$': 'B_d_vec_c_vec$' > 'C_b_d_vec_fun$' ).

tff('function_uus$',axiom,
    'uus$'('fmb_B_d_vec_c_vec$_1') = 'fmb_C_b_d_vec_fun$_1' ).

tff('declare_uum$',type,
    'uum$': 'B_c_vec_a_vec$' > 'A_b_c_vec_fun$' ).

tff('function_uum$',axiom,
    'uum$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uve$',type,
    'uve$': ( 'B_b_d_vec_fun$' * 'B_a_vec_c_vec$' * 'C$' ) > 'A_b_d_vec_fun$' ).

tff('function_uve$',axiom,
    'uve$'('fmb_B_b_d_vec_fun$_1','fmb_B_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vec_lambda$l',type,
    'vec_lambda$l': 'C_b_d_vec_a_vec_fun$' > 'B_d_vec_a_vec_c_vec$' ).

tff('function_vec_lambda$l',axiom,
    'vec_lambda$l'('fmb_C_b_d_vec_a_vec_fun$_1') = 'fmb_B_d_vec_a_vec_c_vec$_1' ).

tff('declare_rowvector$b',type,
    'rowvector$b': 'B_c_vec_a_vec$' > 'B_c_vec_a_vec_a_vec$' ).

tff('function_rowvector$b',axiom,
    'rowvector$b'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_vec_lambda$j',type,
    'vec_lambda$j': 'C_b_c_vec_a_vec_fun$' > 'B_c_vec_a_vec_c_vec$' ).

tff('function_vec_lambda$j',axiom,
    'vec_lambda$j'('fmb_C_b_c_vec_a_vec_fun$_1') = 'fmb_B_c_vec_a_vec_c_vec$_1' ).

tff('declare_uzv$',type,
    'uzv$': ( 'B_c_vec$' * 'B_c_vec$' ) > 'C_b_fun$' ).

tff('function_uzv$',axiom,
    'uzv$'('fmb_B_c_vec$_1','fmb_B_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uua$',type,
    'uua$': ( 'A$' * 'C$' * 'B_d_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_uua$',axiom,
    'uua$'('fmb_A$_1','fmb_C$_1','fmb_B_d_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_fun_app$w',type,
    'fun_app$w': ( 'B_c_vec_b_fun$' * 'B_c_vec$' ) > 'B$' ).

tff('function_fun_app$w',axiom,
    'fun_app$w'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec$_1') = 'fmb_B$_1' ).

tff('declare_uzb$',type,
    'uzb$': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' * 'B$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uzb$',axiom,
    'uzb$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_fun_app$ag',type,
    'fun_app$ag': ( 'C_b_a_vec_bool_fun_fun$' * 'C$' ) > 'B_a_vec_bool_fun$' ).

tff('function_fun_app$ag',axiom,
    'fun_app$ag'('fmb_C_b_a_vec_bool_fun_fun$_1','fmb_C$_1') = 'fmb_B_a_vec_bool_fun$_1' ).

tff('declare_interchange_columns_row$c',type,
    'interchange_columns_row$c': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' ) > 'A_b_c_vec_fun$' ).

tff('function_interchange_columns_row$c',axiom,
    'interchange_columns_row$c'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_column$h',type,
    'column$h': ( 'C$' * 'B_a_vec_c_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_column$h',axiom,
    'column$h'('fmb_C$_1','fmb_B_a_vec_c_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_columnvector_row$',type,
    'columnvector_row$': 'B_c_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_columnvector_row$',axiom,
    'columnvector_row$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_uuz$',type,
    'uuz$': ( 'B_b_fun$' * 'B_d_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_uuz$',axiom,
    'uuz$'('fmb_B_b_fun$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_map_matrix$',type,
    'map_matrix$': ( 'B_b_fun$' * 'B_c_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_map_matrix$',axiom,
    'map_matrix$'('fmb_B_b_fun$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_fun_app$r',type,
    'fun_app$r': ( 'A_b_fun$' * 'A$' ) > 'B$' ).

tff('function_fun_app$r',axiom,
    'fun_app$r'('fmb_A_b_fun$_1','fmb_A$_1') = 'fmb_B$_1' ).

tff('declare_times$m',type,
    'times$m': ( 'A_b_c_vec_fun$' * 'A_b_c_vec_fun$' ) > 'A_b_c_vec_fun$' ).

tff('function_times$m',axiom,
    ( ( 'times$m'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun$_1') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'times$m'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun$_2') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'times$m'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun$_1') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'times$m'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun$_2') = 'fmb_A_b_c_vec_fun$_2' ) ) ).

tff('declare_interchange_columns_row$',type,
    'interchange_columns_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'D_b_d_vec_fun$' ).

tff('function_interchange_columns_row$',axiom,
    'interchange_columns_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_vec_nth$p',type,
    'vec_nth$p': ( 'B_c_vec_a_vec_c_vec$' * 'C$' ) > 'B_c_vec_a_vec$' ).

tff('function_vec_nth$p',axiom,
    'vec_nth$p'('fmb_B_c_vec_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_interchange_rows$e',type,
    'interchange_rows$e': ( 'B_a_vec_d_vec$' * 'D$' * 'D$' ) > 'B_a_vec_d_vec$' ).

tff('function_interchange_rows$e',axiom,
    'interchange_rows$e'('fmb_B_a_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_vec_lambda$b',type,
    'vec_lambda$b': 'D_b_fun$' > 'B_d_vec$' ).

tff('function_vec_lambda$b',axiom,
    'vec_lambda$b'('fmb_D_b_fun$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_columns$c',type,
    'columns$c': 'B_c_vec_a_vec$' > 'B_a_vec_set$' ).

tff('function_columns$c',axiom,
    'columns$c'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_a_vec_set$_1' ).

tff('declare_plus$d',type,
    'plus$d': 'B$' > 'B_b_fun$' ).

tff('function_plus$d',axiom,
    'plus$d'('fmb_B$_1') = 'fmb_B_b_fun$_1' ).

tff('declare_uuw$',type,
    'uuw$': ( 'B_b_fun$' * 'B_a_vec_c_vec$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uuw$',axiom,
    'uuw$'('fmb_B_b_fun$_1','fmb_B_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_fun_app$n',type,
    'fun_app$n': ( 'A_b_c_vec_a_vec_fun$' * 'A$' ) > 'B_c_vec_a_vec$' ).

tff('function_fun_app$n',axiom,
    'fun_app$n'('fmb_A_b_c_vec_a_vec_fun$_1','fmb_A$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uzx$',type,
    'uzx$': ( 'B_a_vec$' * 'B_a_vec$' ) > 'A_b_fun$' ).

tff('function_uzx$',axiom,
    'uzx$'('fmb_B_a_vec$_1','fmb_B_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_fun_app$u',type,
    'fun_app$u': ( 'C_b_c_vec_a_vec_fun$' * 'C$' ) > 'B_c_vec_a_vec$' ).

tff('function_fun_app$u',axiom,
    'fun_app$u'('fmb_C_b_c_vec_a_vec_fun$_1','fmb_C$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_vah$',type,
    'vah$': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_vah$',axiom,
    'vah$'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_fun_app$am',type,
    'fun_app$am': ( 'D_b_bool_fun_fun$' * 'D$' ) > 'B_bool_fun$' ).

tff('function_fun_app$am',axiom,
    'fun_app$am'('fmb_D_b_bool_fun_fun$_1','fmb_D$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_map_matrix$n',type,
    'map_matrix$n': ( 'B_b_d_vec_fun$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_d_vec_a_vec$' ).

tff('function_map_matrix$n',axiom,
    'map_matrix$n'('fmb_B_b_d_vec_fun$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_d_vec_a_vec$_1' ).

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

tff('function_uminus$e',axiom,
    'uminus$e'('fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_column$e',type,
    'column$e': ( 'C$' * 'B_c_vec_c_vec$' ) > 'B_c_vec$' ).

tff('function_column$e',axiom,
    'column$e'('fmb_C$_1','fmb_B_c_vec_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_vbh$',type,
    'vbh$': 'B_c_vec$' > 'A_b_c_vec_fun$' ).

tff('function_vbh$',axiom,
    'vbh$'('fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uwy$',type,
    'uwy$': 'B_c_vec_c_vec$' > 'C_b_c_vec_fun$' ).

tff('function_uwy$',axiom,
    'uwy$'('fmb_B_c_vec_c_vec$_1') = 'fmb_C_b_c_vec_fun$_1' ).

tff('declare_uvb$',type,
    'uvb$': ( 'B_b_c_vec_fun$' * 'B_a_vec_c_vec$' ) > 'C_b_c_vec_a_vec_fun$' ).

tff('function_uvb$',axiom,
    'uvb$'('fmb_B_b_c_vec_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_c_vec_a_vec_fun$_1' ).

tff('declare_uxz$',type,
    'uxz$': 'B_c_vec$' > 'C_b_a_vec_fun$' ).

tff('function_uxz$',axiom,
    'uxz$'('fmb_B_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_mult_row_row$d',type,
    'mult_row_row$d': ( 'B_d_vec_a_vec$' * 'A$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_mult_row_row$d',axiom,
    'mult_row_row$d'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_row_add_row$d',type,
    'row_add_row$d': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_row_add_row$d',axiom,
    'row_add_row$d'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_interchange_columns$b',type,
    'interchange_columns$b': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_interchange_columns$b',axiom,
    'interchange_columns$b'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_vam$',type,
    'vam$': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' * 'B$' * 'A$' ) > 'C_b_fun$' ).

tff('function_vam$',axiom,
    'vam$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uwu$',type,
    'uwu$': 'B_a_vec_c_vec$' > 'A_b_c_vec_fun$' ).

tff('function_uwu$',axiom,
    'uwu$'('fmb_B_a_vec_c_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_elt_set_plus$',type,
    'elt_set_plus$': ( 'A_b_d_vec_fun$' * 'A_b_d_vec_fun_set$' ) > 'A_b_d_vec_fun_set$' ).

tff('function_elt_set_plus$',axiom,
    'elt_set_plus$'('fmb_A_b_d_vec_fun$_1','fmb_A_b_d_vec_fun_set$_1') = 'fmb_A_b_d_vec_fun_set$_1' ).

tff('declare_transpose_row$d',type,
    'transpose_row$d': 'B_a_vec_d_vec$' > 'A_b_d_vec_fun$' ).

tff('function_transpose_row$d',axiom,
    'transpose_row$d'('fmb_B_a_vec_d_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uup$',type,
    'uup$': 'B_d_vec_d_vec$' > 'D_b_d_vec_fun$' ).

tff('function_uup$',axiom,
    'uup$'('fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uwa$',type,
    'uwa$': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uwa$',axiom,
    'uwa$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_plus$',type,
    'plus$': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_plus$',axiom,
    'plus$'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_vat$',type,
    'vat$': ( 'B_d_vec$' * 'B_d_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_vat$',axiom,
    'vat$'('fmb_B_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_transpose_row$f',type,
    'transpose_row$f': ( 'B_c_vec_c_vec$' * 'C$' ) > 'B_c_vec$' ).

tff('function_transpose_row$f',axiom,
    'transpose_row$f'('fmb_B_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_row$',type,
    'row$': ( 'D$' * 'B_d_vec_d_vec$' ) > 'B_d_vec$' ).

tff('function_row$',axiom,
    'row$'('fmb_D$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_fun_app$',type,
    'fun_app$': ( 'A_b_c_vec_fun$' * 'A$' ) > 'B_c_vec$' ).

tff('function_fun_app$',axiom,
    ( ( 'fun_app$'('fmb_A_b_c_vec_fun$_1','fmb_A$_1') = 'fmb_B_c_vec$_1' )
    & ( 'fun_app$'('fmb_A_b_c_vec_fun$_2','fmb_A$_1') = 'fmb_B_c_vec$_1' ) ) ).

tff('declare_gauss_Jordan_wrapper$e',type,
    'gauss_Jordan_wrapper$e': ( 'D$' * 'C$' * 'B_d_vec_d_vec$' * 'B_c_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_gauss_Jordan_wrapper$e',axiom,
    'gauss_Jordan_wrapper$e'('fmb_D$_1','fmb_C$_1','fmb_B_d_vec_d_vec$_1','fmb_B_c_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uul$',type,
    'uul$': 'B_d_vec_a_vec$' > 'A_b_d_vec_fun$' ).

tff('function_uul$',axiom,
    'uul$'('fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_columnvector$i',type,
    'columnvector$i': 'B_d_vec_a_vec$' > 'B_d_vec_a_vec_a_vec$' ).

tff('function_columnvector$i',axiom,
    'columnvector$i'('fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec_a_vec$_1' ).

tff('declare_uwm$',type,
    'uwm$': ( 'B_a_vec_c_vec_c_vec$' * 'C$' ) > 'C_b_a_vec_fun$' ).

tff('function_uwm$',axiom,
    'uwm$'('fmb_B_a_vec_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_column_add$c',type,
    'column_add$c': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' * 'B$' ) > 'B_d_vec_a_vec$' ).

tff('function_column_add$c',axiom,
    'column_add$c'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uun$',type,
    'uun$': 'B_c_vec$' > 'C_b_fun$' ).

tff('function_uun$',axiom,
    'uun$'('fmb_B_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_mult_column$d',type,
    'mult_column$d': ( 'B_c_vec_a_vec$' * 'C$' * 'B$' ) > 'B_c_vec_a_vec$' ).

tff('function_mult_column$d',axiom,
    'mult_column$d'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_collect$b',type,
    'collect$b': 'A_b_c_vec_fun_bool_fun$' > 'A_b_c_vec_fun_set$' ).

tff('function_collect$b',axiom,
    'collect$b'('fmb_A_b_c_vec_fun_bool_fun$_1') = 'fmb_A_b_c_vec_fun_set$_1' ).

tff('declare_plus$c',type,
    'plus$c': ( 'B_a_vec$' * 'B_a_vec$' ) > 'B_a_vec$' ).

tff('function_plus$c',axiom,
    'plus$c'('fmb_B_a_vec$_1','fmb_B_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uvo$',type,
    'uvo$': 'B_a_vec$' > 'A_b_a_vec_fun$' ).

tff('function_uvo$',axiom,
    'uvo$'('fmb_B_a_vec$_1') = 'fmb_A_b_a_vec_fun$_1' ).

tff('declare_plus$p',type,
    'plus$p': ( 'B_d_vec_a_vec_set$' * 'B_d_vec_a_vec_set$' ) > 'B_d_vec_a_vec_set$' ).

tff('function_plus$p',axiom,
    'plus$p'('fmb_B_d_vec_a_vec_set$_1','fmb_B_d_vec_a_vec_set$_1') = 'fmb_B_d_vec_a_vec_set$_1' ).

tff('declare_interchange_rows$c',type,
    'interchange_rows$c': ( 'B_d_vec_a_vec$' * 'A$' ) > 'A_b_d_vec_a_vec_fun$' ).

tff('function_interchange_rows$c',axiom,
    'interchange_rows$c'('fmb_B_d_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_d_vec_a_vec_fun$_1' ).

tff('declare_plus$j',type,
    'plus$j': ( 'A_b_d_vec_fun_set$' * 'A_b_d_vec_fun_set$' ) > 'A_b_d_vec_fun_set$' ).

tff('function_plus$j',axiom,
    'plus$j'('fmb_A_b_d_vec_fun_set$_1','fmb_A_b_d_vec_fun_set$_1') = 'fmb_A_b_d_vec_fun_set$_1' ).

tff('declare_vav$',type,
    'vav$': ( 'B$' * 'B_c_vec$' ) > 'C_b_fun$' ).

tff('function_vav$',axiom,
    'vav$'('fmb_B$_1','fmb_B_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uxo$',type,
    'uxo$': ( 'B_c_vec_a_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uxo$',axiom,
    'uxo$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_elt_set_plus$c',type,
    'elt_set_plus$c': ( 'B$' * 'B_set$' ) > 'B_set$' ).

tff('function_elt_set_plus$c',axiom,
    'elt_set_plus$c'('fmb_B$_1','fmb_B_set$_1') = 'fmb_B_set$_1' ).

tff('declare_map_matrix$j',type,
    'map_matrix$j': ( 'B_b_fun$' * 'B_d_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_map_matrix$j',axiom,
    'map_matrix$j'('fmb_B_b_fun$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_plus$q',type,
    'plus$q': ( 'B_d_vec_set$' * 'B_d_vec_set$' ) > 'B_d_vec_set$' ).

tff('function_plus$q',axiom,
    'plus$q'('fmb_B_d_vec_set$_1','fmb_B_d_vec_set$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_uzg$',type,
    'uzg$': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_uzg$',axiom,
    'uzg$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vec$f',type,
    'vec$f': 'B_a_vec$' > 'B_a_vec_c_vec$' ).

tff('function_vec$f',axiom,
    'vec$f'('fmb_B_a_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

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

tff('function_uminus$i',axiom,
    'uminus$i'('fmb_B_d_vec_c_vec$_1') = 'fmb_B_d_vec_c_vec$_1' ).

tff('declare_transpose_row$',type,
    'transpose_row$': 'B_c_vec_a_vec$' > 'C_b_a_vec_fun$' ).

tff('function_transpose_row$',axiom,
    'transpose_row$'('fmb_B_c_vec_a_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vec_lambda$m',type,
    'vec_lambda$m': 'A_b_a_vec_fun$' > 'B_a_vec_a_vec$' ).

tff('function_vec_lambda$m',axiom,
    'vec_lambda$m'('fmb_A_b_a_vec_fun$_1') = 'fmb_B_a_vec_a_vec$_1' ).

tff('declare_uzr$',type,
    'uzr$': ( 'B_c_vec_a_vec$' * 'A$' * 'B$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uzr$',axiom,
    'uzr$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_B$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_columnvector_row$h',type,
    'columnvector_row$h': ( 'B_a_vec_c_vec$' * 'C$' ) > 'B_a_vec_c_vec$' ).

tff('function_columnvector_row$h',axiom,
    'columnvector_row$h'('fmb_B_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vae$',type,
    'vae$': ( 'B_c_vec_a_vec_a_vec$' * 'B_c_vec_a_vec_a_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_vae$',axiom,
    'vae$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_column$i',type,
    'column$i': ( 'A$' * 'B_d_vec_a_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_column$i',axiom,
    'column$i'('fmb_A$_1','fmb_B_d_vec_a_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uzm$',type,
    'uzm$': ( 'B_a_vec_c_vec$' * 'C$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_uzm$',axiom,
    'uzm$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uzk$',type,
    'uzk$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_uzk$',axiom,
    'uzk$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_mult_column$a',type,
    'mult_column$a': ( 'B_a_vec_c_vec$' * 'A$' * 'B$' ) > 'B_a_vec_c_vec$' ).

tff('function_mult_column$a',axiom,
    'mult_column$a'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_mult_column$c',type,
    'mult_column$c': ( 'B_d_vec_a_vec$' * 'D$' * 'B$' ) > 'B_d_vec_a_vec$' ).

tff('function_mult_column$c',axiom,
    'mult_column$c'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uvt$',type,
    'uvt$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uvt$',axiom,
    'uvt$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_plus$g',type,
    'plus$g': ( 'B_a_vec_c_vec$' * 'B_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_plus$g',axiom,
    'plus$g'('fmb_B_a_vec_c_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uyi$',type,
    'uyi$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uyi$',axiom,
    'uyi$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_plus$r',type,
    'plus$r': ( 'B_c_vec_a_vec_set$' * 'B_c_vec_a_vec_set$' ) > 'B_c_vec_a_vec_set$' ).

tff('function_plus$r',axiom,
    'plus$r'('fmb_B_c_vec_a_vec_set$_1','fmb_B_c_vec_a_vec_set$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_columns$b',type,
    'columns$b': 'B_d_vec_a_vec$' > 'B_a_vec_set$' ).

tff('function_columns$b',axiom,
    'columns$b'('fmb_B_d_vec_a_vec$_1') = 'fmb_B_a_vec_set$_1' ).

tff('declare_column_add_row$c',type,
    'column_add_row$c': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_column_add_row$c',axiom,
    'column_add_row$c'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_elt_set_plus$a',type,
    'elt_set_plus$a': ( 'D_b_fun$' * 'D_b_fun_set$' ) > 'D_b_fun_set$' ).

tff('function_elt_set_plus$a',axiom,
    'elt_set_plus$a'('fmb_D_b_fun$_1','fmb_D_b_fun_set$_1') = 'fmb_D_b_fun_set$_1' ).

tff('declare_mult_column$b',type,
    'mult_column$b': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_mult_column$b',axiom,
    'mult_column$b'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_fun_app$h',type,
    'fun_app$h': ( 'C_b_a_vec_c_vec_fun$' * 'C$' ) > 'B_a_vec_c_vec$' ).

tff('function_fun_app$h',axiom,
    'fun_app$h'('fmb_C_b_a_vec_c_vec_fun$_1','fmb_C$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vec_lambda$k',type,
    'vec_lambda$k': 'A_b_a_vec_c_vec_fun$' > 'B_a_vec_c_vec_a_vec$' ).

tff('function_vec_lambda$k',axiom,
    'vec_lambda$k'('fmb_A_b_a_vec_c_vec_fun$_1') = 'fmb_B_a_vec_c_vec_a_vec$_1' ).

tff('declare_uxv$',type,
    'uxv$': 'B_d_vec$' > 'D_b_a_vec_fun$' ).

tff('function_uxv$',axiom,
    'uxv$'('fmb_B_d_vec$_1') = 'fmb_D_b_a_vec_fun$_1' ).

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

tff('function_times$',axiom,
    'times$'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_transpose_row$b',type,
    'transpose_row$b': 'B_c_vec_a_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_transpose_row$b',axiom,
    'transpose_row$b'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$g',type,
    'gauss_Jordan_wrapper$g': ( 'A$' * 'A$' * 'B_c_vec_a_vec$' * 'B_a_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_gauss_Jordan_wrapper$g',axiom,
    'gauss_Jordan_wrapper$g'('fmb_A$_1','fmb_A$_1','fmb_B_c_vec_a_vec$_1','fmb_B_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_elt_set_times$e',type,
    'elt_set_times$e': ( 'B_d_vec$' * 'B_d_vec_set$' ) > 'B_d_vec_set$' ).

tff('function_elt_set_times$e',axiom,
    'elt_set_times$e'('fmb_B_d_vec$_1','fmb_B_d_vec_set$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_uwp$',type,
    'uwp$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uwp$',axiom,
    'uwp$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_transpose_row$g',type,
    'transpose_row$g': 'B_a_vec_c_vec$' > 'A_b_c_vec_fun$' ).

tff('function_transpose_row$g',axiom,
    'transpose_row$g'('fmb_B_a_vec_c_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_column$j',type,
    'column$j': ( 'A$' * 'B_a_vec_d_vec$' ) > 'B_d_vec$' ).

tff('function_column$j',axiom,
    'column$j'('fmb_A$_1','fmb_B_a_vec_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_fun_app$o',type,
    'fun_app$o': ( 'D_b_d_vec_fun$' * 'D$' ) > 'B_d_vec$' ).

tff('function_fun_app$o',axiom,
    'fun_app$o'('fmb_D_b_d_vec_fun$_1','fmb_D$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_vec_nth$r',type,
    'vec_nth$r': ( 'B_d_vec_d_vec_a_vec$' * 'A$' ) > 'B_d_vec_d_vec$' ).

tff('function_vec_nth$r',axiom,
    'vec_nth$r'('fmb_B_d_vec_d_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_vector_scalar_mult$g',type,
    'vector_scalar_mult$g': ( 'B_c_vec$' * 'B_c_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_vector_scalar_mult$g',axiom,
    'vector_scalar_mult$g'('fmb_B_c_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uxm$',type,
    'uxm$': ( 'B_a_vec$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uxm$',axiom,
    'uxm$'('fmb_B_a_vec$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_columnvector$f',type,
    'columnvector$f': 'B_c_vec$' > 'B_a_vec_c_vec$' ).

tff('function_columnvector$f',axiom,
    'columnvector$f'('fmb_B_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uyl$',type,
    'uyl$': ( 'B_d_vec$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uyl$',axiom,
    'uyl$'('fmb_B_d_vec$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uyo$',type,
    'uyo$': 'A_b_c_vec_fun_set$' > 'A_b_c_vec_fun_bool_fun$' ).

tff('function_uyo$',axiom,
    'uyo$'('fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_bool_fun$_1' ).

tff('declare_vec_nth$b',type,
    'vec_nth$b': 'B_d_vec_a_vec$' > 'A_b_d_vec_fun$' ).

tff('function_vec_nth$b',axiom,
    'vec_nth$b'('fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uvz$',type,
    'uvz$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uvz$',axiom,
    'uvz$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_vaw$',type,
    'vaw$': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec_a_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_vaw$',axiom,
    'vaw$'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_columnvector$g',type,
    'columnvector$g': 'B_a_vec$' > 'B_d_vec_a_vec$' ).

tff('function_columnvector$g',axiom,
    'columnvector$g'('fmb_B_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uwx$',type,
    'uwx$': 'B_d_vec_c_vec$' > 'D_b_c_vec_fun$' ).

tff('function_uwx$',axiom,
    'uwx$'('fmb_B_d_vec_c_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_uzf$',type,
    'uzf$': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' * 'B$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uzf$',axiom,
    'uzf$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uyu$',type,
    'uyu$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uyu$',axiom,
    'uyu$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_rows$',type,
    'rows$': 'B_c_vec_a_vec$' > 'B_c_vec_set$' ).

tff('function_rows$',axiom,
    'rows$'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_set$_1' ).

tff('declare_fun_app$j',type,
    'fun_app$j': ( 'A_b_a_vec_fun$' * 'A$' ) > 'B_a_vec$' ).

tff('function_fun_app$j',axiom,
    'fun_app$j'('fmb_A_b_a_vec_fun$_1','fmb_A$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_columnvector_row$i',type,
    'columnvector_row$i': ( 'B_d_vec_a_vec$' * 'A$' ) > 'B_d_vec_a_vec$' ).

tff('function_columnvector_row$i',axiom,
    'columnvector_row$i'('fmb_B_d_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_plus$s',type,
    'plus$s': ( 'B_c_vec_set$' * 'B_c_vec_set$' ) > 'B_c_vec_set$' ).

tff('function_plus$s',axiom,
    'plus$s'('fmb_B_c_vec_set$_1','fmb_B_c_vec_set$_1') = 'fmb_B_c_vec_set$_1' ).

tff('declare_vec_nth$s',type,
    'vec_nth$s': ( 'B_d_vec_d_vec_d_vec$' * 'D$' ) > 'B_d_vec_d_vec$' ).

tff('function_vec_nth$s',axiom,
    'vec_nth$s'('fmb_B_d_vec_d_vec_d_vec$_1','fmb_D$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_elt_set_plus$g',type,
    'elt_set_plus$g': ( 'B_c_vec$' * 'B_c_vec_set$' ) > 'B_c_vec_set$' ).

tff('function_elt_set_plus$g',axiom,
    'elt_set_plus$g'('fmb_B_c_vec$_1','fmb_B_c_vec_set$_1') = 'fmb_B_c_vec_set$_1' ).

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

tff('function_uminus$d',axiom,
    'uminus$d'('fmb_B_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_map_matrix$b',type,
    'map_matrix$b': ( 'B_b_fun$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_map_matrix$b',axiom,
    'map_matrix$b'('fmb_B_b_fun$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vec_lambda$d',type,
    'vec_lambda$d': 'C_b_fun$' > 'B_c_vec$' ).

tff('function_vec_lambda$d',axiom,
    'vec_lambda$d'('fmb_C_b_fun$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_mult_column_row$b',type,
    'mult_column_row$b': ( 'B_a_vec_c_vec$' * 'A$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_mult_column_row$b',axiom,
    'mult_column_row$b'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uxy$',type,
    'uxy$': ( 'B_c_vec$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uxy$',axiom,
    'uxy$'('fmb_B_c_vec$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uyj$',type,
    'uyj$': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_d_vec_fun$' ).

tff('function_uyj$',axiom,
    'uyj$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vas$',type,
    'vas$': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_vas$',axiom,
    'vas$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_fun_app$x',type,
    'fun_app$x': ( 'B_a_vec_b_fun$' * 'B_a_vec$' ) > 'B$' ).

tff('function_fun_app$x',axiom,
    'fun_app$x'('fmb_B_a_vec_b_fun$_1','fmb_B_a_vec$_1') = 'fmb_B$_1' ).

tff('declare_mult_column$',type,
    'mult_column$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'B_d_vec_d_vec$' ).

tff('function_mult_column$',axiom,
    'mult_column$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_columnvector_row$e',type,
    'columnvector_row$e': ( 'B_d_vec$' * 'D$' ) > 'B_a_vec$' ).

tff('function_columnvector_row$e',axiom,
    'columnvector_row$e'('fmb_B_d_vec$_1','fmb_D$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_vbf$',type,
    'vbf$': 'B_d_vec$' > 'A_b_d_vec_fun$' ).

tff('function_vbf$',axiom,
    'vbf$'('fmb_B_d_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_elt_set_times$b',type,
    'elt_set_times$b': ( 'A_b_c_vec_fun$' * 'A_b_c_vec_fun_set$' ) > 'A_b_c_vec_fun_set$' ).

tff('function_elt_set_times$b',axiom,
    ( ( 'elt_set_times$b'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' )
    & ( 'elt_set_times$b'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' ) ) ).

tff('declare_interchange_columns_row$d',type,
    'interchange_columns_row$d': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' ) > 'A_b_d_vec_fun$' ).

tff('function_interchange_columns_row$d',axiom,
    'interchange_columns_row$d'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_rowvector$a',type,
    'rowvector$a': 'B_a_vec$' > 'B_a_vec_c_vec$' ).

tff('function_rowvector$a',axiom,
    'rowvector$a'('fmb_B_a_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uya$',type,
    'uya$': ( 'B_a_vec$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uya$',axiom,
    'uya$'('fmb_B_a_vec$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_row_add_row$a',type,
    'row_add_row$a': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_row_add_row$a',axiom,
    'row_add_row$a'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

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

tff('function_uminus$c',axiom,
    'uminus$c'('fmb_B_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_map_matrix$l',type,
    'map_matrix$l': ( 'B_d_vec_b_fun$' * 'B_d_vec_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_map_matrix$l',axiom,
    'map_matrix$l'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vbd$',type,
    'vbd$': 'B$' > 'C_b_fun$' ).

tff('function_vbd$',axiom,
    'vbd$'('fmb_B$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_columns$d',type,
    'columns$d': 'B_a_vec_d_vec$' > 'B_d_vec_set$' ).

tff('function_columns$d',axiom,
    'columns$d'('fmb_B_a_vec_d_vec$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_uvd$',type,
    'uvd$': ( 'B_b_a_vec_fun$' * 'B_c_vec_a_vec$' ) > 'A_b_a_vec_c_vec_fun$' ).

tff('function_uvd$',axiom,
    'uvd$'('fmb_B_b_a_vec_fun$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_a_vec_c_vec_fun$_1' ).

tff('declare_fun_app$p',type,
    'fun_app$p': ( 'C_b_d_vec_fun$' * 'C$' ) > 'B_d_vec$' ).

tff('function_fun_app$p',axiom,
    'fun_app$p'('fmb_C_b_d_vec_fun$_1','fmb_C$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_uym$',type,
    'uym$': 'A_b_d_vec_fun_set$' > 'A_b_d_vec_fun_bool_fun$' ).

tff('function_uym$',axiom,
    'uym$'('fmb_A_b_d_vec_fun_set$_1') = 'fmb_A_b_d_vec_fun_bool_fun$_1' ).

tff('declare_interchange_rows_row$c',type,
    'interchange_rows_row$c': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_interchange_rows_row$c',axiom,
    'interchange_rows_row$c'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_columnvector_row$g',type,
    'columnvector_row$g': ( 'B_a_vec$' * 'A$' ) > 'B_a_vec$' ).

tff('function_columnvector_row$g',axiom,
    'columnvector_row$g'('fmb_B_a_vec$_1','fmb_A$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_columnvector_row$c',type,
    'columnvector_row$c': ( 'B_c_vec$' * 'C$' ) > 'B_c_vec$' ).

tff('function_columnvector_row$c',axiom,
    'columnvector_row$c'('fmb_B_c_vec$_1','fmb_C$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_columnvector$',type,
    'columnvector$': 'B_a_vec$' > 'B_c_vec_a_vec$' ).

tff('function_columnvector$',axiom,
    'columnvector$'('fmb_B_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_plus$l',type,
    'plus$l': ( 'D_b_fun_set$' * 'D_b_fun_set$' ) > 'D_b_fun_set$' ).

tff('function_plus$l',axiom,
    'plus$l'('fmb_D_b_fun_set$_1','fmb_D_b_fun_set$_1') = 'fmb_D_b_fun_set$_1' ).

tff('declare_uyk$',type,
    'uyk$': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uyk$',axiom,
    'uyk$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

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

tff('function_fun_app$a',axiom,
    'fun_app$a'('fmb_B_b_fun$_1','fmb_B$_1') = 'fmb_B$_1' ).

tff('declare_transpose$c',type,
    'transpose$c': 'B_c_vec_a_vec_a_vec$' > 'B_c_vec_a_vec_a_vec$' ).

tff('function_transpose$c',axiom,
    'transpose$c'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_vec_lambda$a',type,
    'vec_lambda$a': 'C_b_a_vec_fun$' > 'B_a_vec_c_vec$' ).

tff('function_vec_lambda$a',axiom,
    'vec_lambda$a'('fmb_C_b_a_vec_fun$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vec$c',type,
    'vec$c': 'B_c_vec$' > 'B_c_vec_a_vec$' ).

tff('function_vec$c',axiom,
    'vec$c'('fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_fun_app$s',type,
    'fun_app$s': ( 'C_b_d_vec_a_vec_fun$' * 'C$' ) > 'B_d_vec_a_vec$' ).

tff('function_fun_app$s',axiom,
    'fun_app$s'('fmb_C_b_d_vec_a_vec_fun$_1','fmb_C$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vbg$',type,
    'vbg$': 'B$' > 'A_b_fun$' ).

tff('function_vbg$',axiom,
    'vbg$'('fmb_B$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_vector_scalar_mult$b',type,
    'vector_scalar_mult$b': ( 'B$' * 'B_c_vec$' ) > 'B_c_vec$' ).

tff('function_vector_scalar_mult$b',axiom,
    'vector_scalar_mult$b'('fmb_B$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_fun_app$aj',type,
    'fun_app$aj': ( 'A_b_bool_fun_fun$' * 'A$' ) > 'B_bool_fun$' ).

tff('function_fun_app$aj',axiom,
    'fun_app$aj'('fmb_A_b_bool_fun_fun$_1','fmb_A$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_mult_row_row$a',type,
    'mult_row_row$a': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_mult_row_row$a',axiom,
    'mult_row_row$a'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_columnvector$a',type,
    'columnvector$a': 'B_c_vec_a_vec$' > 'B_c_vec_a_vec_a_vec$' ).

tff('function_columnvector$a',axiom,
    'columnvector$a'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_column_add$d',type,
    'column_add$d': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' * 'B$' ) > 'B_c_vec_a_vec$' ).

tff('function_column_add$d',axiom,
    'column_add$d'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_map_matrix$d',type,
    'map_matrix$d': ( 'B_b_a_vec_fun$' * 'B_c_vec_a_vec$' ) > 'B_a_vec_c_vec_a_vec$' ).

tff('function_map_matrix$d',axiom,
    'map_matrix$d'('fmb_B_b_a_vec_fun$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_a_vec_c_vec_a_vec$_1' ).

tff('declare_rowvector$c',type,
    'rowvector$c': 'B_d_vec$' > 'B_d_vec_a_vec$' ).

tff('function_rowvector$c',axiom,
    'rowvector$c'('fmb_B_d_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uut$',type,
    'uut$': 'B_c_vec_d_vec$' > 'D_b_c_vec_fun$' ).

tff('function_uut$',axiom,
    'uut$'('fmb_B_c_vec_d_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_times$n',type,
    'times$n': ( 'A_b_c_vec_fun_set$' * 'A_b_c_vec_fun_set$' ) > 'A_b_c_vec_fun_set$' ).

tff('function_times$n',axiom,
    'times$n'('fmb_A_b_c_vec_fun_set$_1','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' ).

tff('declare_uvx$',type,
    'uvx$': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uvx$',axiom,
    'uvx$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_times$r',type,
    'times$r': ( 'B_c_vec_a_vec_set$' * 'B_c_vec_a_vec_set$' ) > 'B_c_vec_a_vec_set$' ).

tff('function_times$r',axiom,
    'times$r'('fmb_B_c_vec_a_vec_set$_1','fmb_B_c_vec_a_vec_set$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_plus$n',type,
    'plus$n': ( 'A_b_c_vec_fun_set$' * 'A_b_c_vec_fun_set$' ) > 'A_b_c_vec_fun_set$' ).

tff('function_plus$n',axiom,
    'plus$n'('fmb_A_b_c_vec_fun_set$_1','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' ).

tff('declare_uwq$',type,
    'uwq$': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' ) > 'A_b_d_vec_fun$' ).

tff('function_uwq$',axiom,
    'uwq$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_times$j',type,
    'times$j': ( 'A_b_d_vec_fun_set$' * 'A_b_d_vec_fun_set$' ) > 'A_b_d_vec_fun_set$' ).

tff('function_times$j',axiom,
    'times$j'('fmb_A_b_d_vec_fun_set$_1','fmb_A_b_d_vec_fun_set$_1') = 'fmb_A_b_d_vec_fun_set$_1' ).

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

tff('function_times$f',axiom,
    'times$f'('fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_times$s',type,
    'times$s': ( 'B_c_vec_set$' * 'B_c_vec_set$' ) > 'B_c_vec_set$' ).

tff('function_times$s',axiom,
    'times$s'('fmb_B_c_vec_set$_1','fmb_B_c_vec_set$_1') = 'fmb_B_c_vec_set$_1' ).

tff('declare_uwt$',type,
    'uwt$': 'B_d_vec_a_vec$' > 'D_b_a_vec_fun$' ).

tff('function_uwt$',axiom,
    'uwt$'('fmb_B_d_vec_a_vec$_1') = 'fmb_D_b_a_vec_fun$_1' ).

tff('declare_transpose$a',type,
    'transpose$a': 'B_d_vec_a_vec$' > 'B_a_vec_d_vec$' ).

tff('function_transpose$a',axiom,
    'transpose$a'('fmb_B_d_vec_a_vec$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_vec_lambda$q',type,
    'vec_lambda$q': 'A_b_d_vec_a_vec_fun$' > 'B_d_vec_a_vec_a_vec$' ).

tff('function_vec_lambda$q',axiom,
    'vec_lambda$q'('fmb_A_b_d_vec_a_vec_fun$_1') = 'fmb_B_d_vec_a_vec_a_vec$_1' ).

tff('declare_uvc$',type,
    'uvc$': ( 'B_b_a_vec_fun$' * 'B_c_vec_a_vec$' * 'A$' ) > 'C_b_a_vec_fun$' ).

tff('function_uvc$',axiom,
    'uvc$'('fmb_B_b_a_vec_fun$_1','fmb_B_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_rows$c',type,
    'rows$c': 'B_a_vec_c_vec$' > 'B_a_vec_set$' ).

tff('function_rows$c',axiom,
    'rows$c'('fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_set$_1' ).

tff('declare_vec_lambda$i',type,
    'vec_lambda$i': 'D_b_c_vec_fun$' > 'B_c_vec_d_vec$' ).

tff('function_vec_lambda$i',axiom,
    'vec_lambda$i'('fmb_D_b_c_vec_fun$_1') = 'fmb_B_c_vec_d_vec$_1' ).

tff('declare_uxk$',type,
    'uxk$': ( 'C$' * 'B_a_vec_c_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uxk$',axiom,
    'uxk$'('fmb_C$_1','fmb_B_a_vec_c_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vec_lambda$g',type,
    'vec_lambda$g': 'A_b_c_vec_a_vec_fun$' > 'B_c_vec_a_vec_a_vec$' ).

tff('function_vec_lambda$g',axiom,
    'vec_lambda$g'('fmb_A_b_c_vec_a_vec_fun$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_uyt$',type,
    'uyt$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uyt$',axiom,
    'uyt$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uux$',type,
    'uux$': ( 'B_b_fun$' * 'B_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uux$',axiom,
    'uux$'('fmb_B_b_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_elt_set_times$g',type,
    'elt_set_times$g': ( 'B_c_vec$' * 'B_c_vec_set$' ) > 'B_c_vec_set$' ).

tff('function_elt_set_times$g',axiom,
    'elt_set_times$g'('fmb_B_c_vec$_1','fmb_B_c_vec_set$_1') = 'fmb_B_c_vec_set$_1' ).

tff('declare_vaa$',type,
    'vaa$': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_vaa$',axiom,
    'vaa$'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_elt_set_times$f',type,
    'elt_set_times$f': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec_set$' ) > 'B_c_vec_a_vec_set$' ).

tff('function_elt_set_times$f',axiom,
    'elt_set_times$f'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec_set$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_column_add_row$d',type,
    'column_add_row$d': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_column_add_row$d',axiom,
    'column_add_row$d'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_interchange_rows_row$',type,
    'interchange_rows_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'D_b_d_vec_fun$' ).

tff('function_interchange_rows_row$',axiom,
    'interchange_rows_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_interchange_columns$c',type,
    'interchange_columns$c': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' ) > 'B_d_vec_a_vec$' ).

tff('function_interchange_columns$c',axiom,
    'interchange_columns$c'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uzu$',type,
    'uzu$': ( 'B_a_vec_c_vec$' * 'B_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uzu$',axiom,
    'uzu$'('fmb_B_a_vec_c_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vector_scalar_mult$e',type,
    'vector_scalar_mult$e': ( 'B$' * 'B_d_vec$' ) > 'B_d_vec$' ).

tff('function_vector_scalar_mult$e',axiom,
    'vector_scalar_mult$e'('fmb_B$_1','fmb_B_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_uzz$',type,
    'uzz$': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_uzz$',axiom,
    'uzz$'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_transpose$i',type,
    'transpose$i': 'B_a_vec_c_vec_c_vec$' > 'B_a_vec_c_vec_c_vec$' ).

tff('function_transpose$i',axiom,
    'transpose$i'('fmb_B_a_vec_c_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec_c_vec$_1' ).

tff('declare_uzo$',type,
    'uzo$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uzo$',axiom,
    'uzo$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_times$a',type,
    'times$a': ( 'B_d_vec$' * 'B_d_vec$' ) > 'B_d_vec$' ).

tff('function_times$a',axiom,
    'times$a'('fmb_B_d_vec$_1','fmb_B_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_vec_nth$a',type,
    'vec_nth$a': 'B_d_vec$' > 'D_b_fun$' ).

tff('function_vec_nth$a',axiom,
    'vec_nth$a'('fmb_B_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_fun_app$al',type,
    'fun_app$al': ( 'A_b_c_vec_bool_fun_fun$' * 'A$' ) > 'B_c_vec_bool_fun$' ).

tff('function_fun_app$al',axiom,
    'fun_app$al'('fmb_A_b_c_vec_bool_fun_fun$_1','fmb_A$_1') = 'fmb_B_c_vec_bool_fun$_1' ).

tff('declare_map_matrix$k',type,
    'map_matrix$k': ( 'B_b_c_vec_fun$' * 'B_a_vec_a_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_map_matrix$k',axiom,
    'map_matrix$k'('fmb_B_b_c_vec_fun$_1','fmb_B_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_interchange_columns$',type,
    'interchange_columns$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'B_d_vec_d_vec$' ).

tff('function_interchange_columns$',axiom,
    'interchange_columns$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uvj$',type,
    'uvj$': ( 'B_a_vec_b_fun$' * 'B_a_vec_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uvj$',axiom,
    'uvj$'('fmb_B_a_vec_b_fun$_1','fmb_B_a_vec_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uvi$',type,
    'uvi$': ( 'B_a_vec_b_fun$' * 'B_a_vec_c_vec_a_vec$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uvi$',axiom,
    'uvi$'('fmb_B_a_vec_b_fun$_1','fmb_B_a_vec_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vec_lambda$o',type,
    'vec_lambda$o': 'C_b_c_vec_fun$' > 'B_c_vec_c_vec$' ).

tff('function_vec_lambda$o',axiom,
    'vec_lambda$o'('fmb_C_b_c_vec_fun$_1') = 'fmb_B_c_vec_c_vec$_1' ).

tff('declare_vag$',type,
    'vag$': ( 'B_d_vec$' * 'B_d_vec$' ) > 'D_b_fun$' ).

tff('function_vag$',axiom,
    'vag$'('fmb_B_d_vec$_1','fmb_B_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uur$',type,
    'uur$': 'B_c_vec_a_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uur$',axiom,
    'uur$'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_interchange_rows$',type,
    'interchange_rows$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'B_d_vec_d_vec$' ).

tff('function_interchange_rows$',axiom,
    'interchange_rows$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uzc$',type,
    'uzc$': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_uzc$',axiom,
    'uzc$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uvr$',type,
    'uvr$': 'B_d_vec$' > 'A_b_d_vec_fun$' ).

tff('function_uvr$',axiom,
    'uvr$'('fmb_B_d_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vec_nth$q',type,
    'vec_nth$q': ( 'B_a_vec_c_vec_a_vec$' * 'A$' ) > 'B_a_vec_c_vec$' ).

tff('function_vec_nth$q',axiom,
    'vec_nth$q'('fmb_B_a_vec_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_transpose$f',type,
    'transpose$f': 'B_c_vec_c_vec$' > 'B_c_vec_c_vec$' ).

tff('function_transpose$f',axiom,
    'transpose$f'('fmb_B_c_vec_c_vec$_1') = 'fmb_B_c_vec_c_vec$_1' ).

tff('declare_columns$a',type,
    'columns$a': 'B_c_vec_a_vec_a_vec$' > 'B_c_vec_a_vec_set$' ).

tff('function_columns$a',axiom,
    'columns$a'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_vector_scalar_mult$d',type,
    'vector_scalar_mult$d': ( 'B$' * 'B_a_vec$' ) > 'B_a_vec$' ).

tff('function_vector_scalar_mult$d',axiom,
    'vector_scalar_mult$d'('fmb_B$_1','fmb_B_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_vector_scalar_mult$f',type,
    'vector_scalar_mult$f': ( 'B_d_vec$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_vector_scalar_mult$f',axiom,
    'vector_scalar_mult$f'('fmb_B_d_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vec_lambda$n',type,
    'vec_lambda$n': 'D_b_a_vec_fun$' > 'B_a_vec_d_vec$' ).

tff('function_vec_lambda$n',axiom,
    'vec_lambda$n'('fmb_D_b_a_vec_fun$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_fun_app$aa',type,
    'fun_app$aa': ( 'B_b_a_vec_fun$' * 'B$' ) > 'B_a_vec$' ).

tff('function_fun_app$aa',axiom,
    'fun_app$aa'('fmb_B_b_a_vec_fun$_1','fmb_B$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uxg$',type,
    'uxg$': ( 'D$' * 'B_d_vec_c_vec$' ) > 'C_b_fun$' ).

tff('function_uxg$',axiom,
    'uxg$'('fmb_D$_1','fmb_B_d_vec_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uuk$',type,
    'uuk$': 'B_d_vec$' > 'D_b_fun$' ).

tff('function_uuk$',axiom,
    'uuk$'('fmb_B_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_transpose_row$h',type,
    'transpose_row$h': ( 'B_a_vec_a_vec$' * 'A$' ) > 'B_a_vec$' ).

tff('function_transpose_row$h',axiom,
    'transpose_row$h'('fmb_B_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_times$l',type,
    'times$l': ( 'D_b_fun_set$' * 'D_b_fun_set$' ) > 'D_b_fun_set$' ).

tff('function_times$l',axiom,
    'times$l'('fmb_D_b_fun_set$_1','fmb_D_b_fun_set$_1') = 'fmb_D_b_fun_set$_1' ).

tff('declare_transpose_row$j',type,
    'transpose_row$j': ( 'B_d_vec_a_vec_a_vec$' * 'A$' ) > 'B_d_vec_a_vec$' ).

tff('function_transpose_row$j',axiom,
    'transpose_row$j'('fmb_B_d_vec_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uzy$',type,
    'uzy$': ( 'B_d_vec$' * 'B_d_vec$' ) > 'D_b_fun$' ).

tff('function_uzy$',axiom,
    'uzy$'('fmb_B_d_vec$_1','fmb_B_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_interchange_columns$e',type,
    'interchange_columns$e': ( 'B_a_vec_d_vec$' * 'A$' * 'A$' ) > 'B_a_vec_d_vec$' ).

tff('function_interchange_columns$e',axiom,
    'interchange_columns$e'('fmb_B_a_vec_d_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_uyx$',type,
    'uyx$': ( 'B_c_vec_a_vec$' * 'C$' * 'B$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uyx$',axiom,
    'uyx$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_B$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uyp$',type,
    'uyp$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uyp$',axiom,
    'uyp$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_times$i',type,
    'times$i': ( 'A_b_d_vec_fun$' * 'A_b_d_vec_fun$' ) > 'A_b_d_vec_fun$' ).

tff('function_times$i',axiom,
    'times$i'('fmb_A_b_d_vec_fun$_1','fmb_A_b_d_vec_fun$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_fun_app$i',type,
    'fun_app$i': ( 'C_b_a_vec_fun$' * 'C$' ) > 'B_a_vec$' ).

tff('function_fun_app$i',axiom,
    'fun_app$i'('fmb_C_b_a_vec_fun$_1','fmb_C$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_elt_set_times$d',type,
    'elt_set_times$d': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec_set$' ) > 'B_d_vec_a_vec_set$' ).

tff('function_elt_set_times$d',axiom,
    'elt_set_times$d'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec_set$_1') = 'fmb_B_d_vec_a_vec_set$_1' ).

tff('declare_row_add$d',type,
    'row_add$d': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_row_add$d',axiom,
    'row_add$d'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_gauss_Jordan_wrapper$h',type,
    'gauss_Jordan_wrapper$h': ( 'C$' * 'D$' * 'B_a_vec_c_vec$' * 'B_d_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_gauss_Jordan_wrapper$h',axiom,
    'gauss_Jordan_wrapper$h'('fmb_C$_1','fmb_D$_1','fmb_B_a_vec_c_vec$_1','fmb_B_d_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_fun_app$q',type,
    'fun_app$q': ( 'C_b_fun$' * 'C$' ) > 'B$' ).

tff('function_fun_app$q',axiom,
    'fun_app$q'('fmb_C_b_fun$_1','fmb_C$_1') = 'fmb_B$_1' ).

tff('declare_vec_nth$j',type,
    'vec_nth$j': ( 'B_a_vec_c_vec_c_vec$' * 'C$' ) > 'B_a_vec_c_vec$' ).

tff('function_vec_nth$j',axiom,
    'vec_nth$j'('fmb_B_a_vec_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_plus$m',type,
    'plus$m': ( 'A_b_c_vec_fun$' * 'A_b_c_vec_fun$' ) > 'A_b_c_vec_fun$' ).

tff('function_plus$m',axiom,
    ( ( 'plus$m'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun$_1') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'plus$m'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun$_2') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'plus$m'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun$_1') = 'fmb_A_b_c_vec_fun$_2' )
    & ( 'plus$m'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun$_2') = 'fmb_A_b_c_vec_fun$_2' ) ) ).

tff('declare_vec_nth$d',type,
    'vec_nth$d': 'B_d_vec_d_vec$' > 'D_b_d_vec_fun$' ).

tff('function_vec_nth$d',axiom,
    'vec_nth$d'('fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_times$h',type,
    'times$h': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_times$h',axiom,
    'times$h'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_column_add_row$',type,
    'column_add_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_column_add_row$',axiom,
    'column_add_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$d',type,
    'gauss_Jordan_wrapper$d': ( 'D$' * 'D$' * 'B_d_vec_d_vec$' * 'B_d_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_gauss_Jordan_wrapper$d',axiom,
    'gauss_Jordan_wrapper$d'('fmb_D$_1','fmb_D$_1','fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uxh$',type,
    'uxh$': ( 'C$' * 'B_c_vec_c_vec$' ) > 'C_b_fun$' ).

tff('function_uxh$',axiom,
    'uxh$'('fmb_C$_1','fmb_B_c_vec_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vec_nth$l',type,
    'vec_nth$l': 'B_a_vec_d_vec$' > 'D_b_a_vec_fun$' ).

tff('function_vec_nth$l',axiom,
    'vec_nth$l'('fmb_B_a_vec_d_vec$_1') = 'fmb_D_b_a_vec_fun$_1' ).

tff('declare_uxx$',type,
    'uxx$': 'B_a_vec$' > 'A_b_a_vec_fun$' ).

tff('function_uxx$',axiom,
    'uxx$'('fmb_B_a_vec$_1') = 'fmb_A_b_a_vec_fun$_1' ).

tff('declare_uvy$',type,
    'uvy$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uvy$',axiom,
    'uvy$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_column_add_row$a',type,
    'column_add_row$a': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_column_add_row$a',axiom,
    'column_add_row$a'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_vec_nth$n',type,
    'vec_nth$n': ( 'B_d_vec_a_vec_a_vec$' * 'A$' ) > 'B_d_vec_a_vec$' ).

tff('function_vec_nth$n',axiom,
    'vec_nth$n'('fmb_B_d_vec_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_columnvector_row$d',type,
    'columnvector_row$d': 'B_a_vec$' > 'A_b_c_vec_fun$' ).

tff('function_columnvector_row$d',axiom,
    'columnvector_row$d'('fmb_B_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_vec_nth$g',type,
    'vec_nth$g': 'B_a_vec_c_vec$' > 'C_b_a_vec_fun$' ).

tff('function_vec_nth$g',axiom,
    'vec_nth$g'('fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_column$b',type,
    'column$b': ( 'A$' * 'B_c_vec_a_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_column$b',axiom,
    'column$b'('fmb_A$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_times$d',type,
    'times$d': 'B$' > 'B_b_fun$' ).

tff('function_times$d',axiom,
    'times$d'('fmb_B$_1') = 'fmb_B_b_fun$_1' ).

tff('declare_transpose_row$c',type,
    'transpose_row$c': 'B_d_vec_d_vec$' > 'D_b_d_vec_fun$' ).

tff('function_transpose_row$c',axiom,
    'transpose_row$c'('fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uzt$',type,
    'uzt$': ( 'B_d_vec_d_vec$' * 'B_d_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_uzt$',axiom,
    'uzt$'('fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_vec_lambda$c',type,
    'vec_lambda$c': 'A_b_fun$' > 'B_a_vec$' ).

tff('function_vec_lambda$c',axiom,
    'vec_lambda$c'('fmb_A_b_fun$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uwe$',type,
    'uwe$': ( 'B_d_vec_a_vec$' * 'D$' ) > 'A_b_fun$' ).

tff('function_uwe$',axiom,
    'uwe$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_row_add_row$b',type,
    'row_add_row$b': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_row_add_row$b',axiom,
    'row_add_row$b'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_elt_set_times$',type,
    'elt_set_times$': ( 'A_b_d_vec_fun$' * 'A_b_d_vec_fun_set$' ) > 'A_b_d_vec_fun_set$' ).

tff('function_elt_set_times$',axiom,
    'elt_set_times$'('fmb_A_b_d_vec_fun$_1','fmb_A_b_d_vec_fun_set$_1') = 'fmb_A_b_d_vec_fun_set$_1' ).

tff('declare_uws$',type,
    'uws$': 'B_c_vec_a_vec$' > 'C_b_a_vec_fun$' ).

tff('function_uws$',axiom,
    'uws$'('fmb_B_c_vec_a_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uyc$',type,
    'uyc$': ( 'B_a_vec_c_vec$' * 'C$' ) > 'C_b_a_vec_fun$' ).

tff('function_uyc$',axiom,
    'uyc$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uzp$',type,
    'uzp$': ( 'B_d_vec_a_vec$' * 'A$' * 'B$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uzp$',axiom,
    'uzp$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_B$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uub$',type,
    'uub$': ( 'A$' * 'D$' * 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_uub$',axiom,
    'uub$'('fmb_A$_1','fmb_D$_1','fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vec$e',type,
    'vec$e': 'B_d_vec$' > 'B_d_vec_d_vec$' ).

tff('function_vec$e',axiom,
    'vec$e'('fmb_B_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_row$c',type,
    'row$c': ( 'A$' * 'B_c_vec_a_vec$' ) > 'B_c_vec$' ).

tff('function_row$c',axiom,
    'row$c'('fmb_A$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_column_add$',type,
    'column_add$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'B_d_vec_d_vec$' ).

tff('function_column_add$',axiom,
    'column_add$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_rows$d',type,
    'rows$d': 'B_d_vec_a_vec$' > 'B_d_vec_set$' ).

tff('function_rows$d',axiom,
    'rows$d'('fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_column$f',type,
    'column$f': ( 'A$' * 'B_a_vec_c_vec$' ) > 'B_c_vec$' ).

tff('function_column$f',axiom,
    'column$f'('fmb_A$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_uwo$',type,
    'uwo$': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' ) > 'C_b_a_vec_fun$' ).

tff('function_uwo$',axiom,
    'uwo$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uyn$',type,
    'uyn$': 'D_b_fun_set$' > 'D_b_fun_bool_fun$' ).

tff('function_uyn$',axiom,
    'uyn$'('fmb_D_b_fun_set$_1') = 'fmb_D_b_fun_bool_fun$_1' ).

tff('declare_times$g',type,
    'times$g': ( 'B_a_vec_c_vec$' * 'B_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_times$g',axiom,
    'times$g'('fmb_B_a_vec_c_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_plus$e',type,
    'plus$e': ( 'B_c_vec_a_vec_a_vec$' * 'B_c_vec_a_vec_a_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_plus$e',axiom,
    'plus$e'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_vbc$',type,
    'vbc$': 'B_a_vec$' > 'C_b_a_vec_fun$' ).

tff('function_vbc$',axiom,
    'vbc$'('fmb_B_a_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uyd$',type,
    'uyd$': 'B_a_vec_c_vec$' > 'C_b_a_vec_c_vec_fun$' ).

tff('function_uyd$',axiom,
    'uyd$'('fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_c_vec_fun$_1' ).

tff('declare_rows$a',type,
    'rows$a': 'B_c_vec_a_vec_a_vec$' > 'B_c_vec_a_vec_set$' ).

tff('function_rows$a',axiom,
    'rows$a'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_fun_app$c',type,
    'fun_app$c': ( 'A_b_d_vec_fun$' * 'A$' ) > 'B_d_vec$' ).

tff('function_fun_app$c',axiom,
    'fun_app$c'('fmb_A_b_d_vec_fun$_1','fmb_A$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_uwj$',type,
    'uwj$': ( 'B_c_vec_c_vec$' * 'C$' ) > 'C_b_fun$' ).

tff('function_uwj$',axiom,
    'uwj$'('fmb_B_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uuc$',type,
    'uuc$': ( 'A$' * 'C$' * 'B_c_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uuc$',axiom,
    'uuc$'('fmb_A$_1','fmb_C$_1','fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_fun_app$ai',type,
    'fun_app$ai': ( 'C_b_bool_fun_fun$' * 'C$' ) > 'B_bool_fun$' ).

tff('function_fun_app$ai',axiom,
    'fun_app$ai'('fmb_C_b_bool_fun_fun$_1','fmb_C$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$a',type,
    'gauss_Jordan_wrapper$a': ( 'A$' * 'D$' * 'B_d_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'B_d_vec_a_vec$' ).

tff('function_gauss_Jordan_wrapper$a',axiom,
    'gauss_Jordan_wrapper$a'('fmb_A$_1','fmb_D$_1','fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vec_lambda$',type,
    'vec_lambda$': 'A_b_d_vec_fun$' > 'B_d_vec_a_vec$' ).

tff('function_vec_lambda$',axiom,
    'vec_lambda$'('fmb_A_b_d_vec_fun$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_fun_app$m',type,
    'fun_app$m': ( 'D_b_c_vec_fun$' * 'D$' ) > 'B_c_vec$' ).

tff('function_fun_app$m',axiom,
    'fun_app$m'('fmb_D_b_c_vec_fun$_1','fmb_D$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_map_matrix$c',type,
    'map_matrix$c': ( 'B_b_c_vec_fun$' * 'B_a_vec_c_vec$' ) > 'B_c_vec_a_vec_c_vec$' ).

tff('function_map_matrix$c',axiom,
    'map_matrix$c'('fmb_B_b_c_vec_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_c_vec_a_vec_c_vec$_1' ).

tff('declare_columnvector$c',type,
    'columnvector$c': 'B_c_vec$' > 'B_c_vec_c_vec$' ).

tff('function_columnvector$c',axiom,
    'columnvector$c'('fmb_B_c_vec$_1') = 'fmb_B_c_vec_c_vec$_1' ).

tff('declare_uxc$',type,
    'uxc$': ( 'C$' * 'B_c_vec_a_vec$' ) > 'A_b_fun$' ).

tff('function_uxc$',axiom,
    'uxc$'('fmb_C$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_vaq$',type,
    'vaq$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_vaq$',axiom,
    'vaq$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

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

tff('function_uminus$f',axiom,
    'uminus$f'('fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_columnvector$b',type,
    'columnvector$b': 'B_d_vec$' > 'B_c_vec_d_vec$' ).

tff('function_columnvector$b',axiom,
    'columnvector$b'('fmb_B_d_vec$_1') = 'fmb_B_c_vec_d_vec$_1' ).

tff('declare_var$',type,
    'var$': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_var$',axiom,
    'var$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_vad$',type,
    'vad$': ( 'B_c_vec$' * 'B_c_vec$' ) > 'C_b_fun$' ).

tff('function_vad$',axiom,
    'vad$'('fmb_B_c_vec$_1','fmb_B_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_uuj$',type,
    'uuj$': ( 'C$' * 'C$' * 'B_a_vec_c_vec$' * 'B_c_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uuj$',axiom,
    'uuj$'('fmb_C$_1','fmb_C$_1','fmb_B_a_vec_c_vec$_1','fmb_B_c_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uuh$',type,
    'uuh$': ( 'A$' * 'A$' * 'B_c_vec_a_vec$' * 'B_a_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uuh$',axiom,
    'uuh$'('fmb_A$_1','fmb_A$_1','fmb_B_c_vec_a_vec$_1','fmb_B_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_collect$',type,
    'collect$': 'A_b_d_vec_fun_bool_fun$' > 'A_b_d_vec_fun_set$' ).

tff('function_collect$',axiom,
    'collect$'('fmb_A_b_d_vec_fun_bool_fun$_1') = 'fmb_A_b_d_vec_fun_set$_1' ).

tff('declare_vec_nth$',type,
    'vec_nth$': 'B_c_vec_a_vec$' > 'A_b_c_vec_fun$' ).

tff('function_vec_nth$',axiom,
    'vec_nth$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_interchange_columns$a',type,
    'interchange_columns$a': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' ) > 'B_a_vec_c_vec$' ).

tff('function_interchange_columns$a',axiom,
    'interchange_columns$a'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uwn$',type,
    'uwn$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' ) > 'D_b_d_vec_fun$' ).

tff('function_uwn$',axiom,
    'uwn$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_vec_nth$c',type,
    'vec_nth$c': 'B_c_vec_a_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_vec_nth$c',axiom,
    'vec_nth$c'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_vec_lambda$h',type,
    'vec_lambda$h': 'C_b_d_vec_fun$' > 'B_d_vec_c_vec$' ).

tff('function_vec_lambda$h',axiom,
    'vec_lambda$h'('fmb_C_b_d_vec_fun$_1') = 'fmb_B_d_vec_c_vec$_1' ).

tff('declare_vbe$',type,
    'vbe$': 'B_c_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_vbe$',axiom,
    'vbe$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_uuo$',type,
    'uuo$': 'B_a_vec$' > 'A_b_fun$' ).

tff('function_uuo$',axiom,
    'uuo$'('fmb_B_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uxs$',type,
    'uxs$': ( 'B_c_vec$' * 'C$' ) > 'C_b_fun$' ).

tff('function_uxs$',axiom,
    'uxs$'('fmb_B_c_vec$_1','fmb_C$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vector_scalar_mult$',type,
    'vector_scalar_mult$': ( 'B_d_vec$' * 'B_d_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_vector_scalar_mult$',axiom,
    'vector_scalar_mult$'('fmb_B_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_times$o',type,
    'times$o': ( 'B_set$' * 'B_set$' ) > 'B_set$' ).

tff('function_times$o',axiom,
    'times$o'('fmb_B_set$_1','fmb_B_set$_1') = 'fmb_B_set$_1' ).

tff('declare_vaf$',type,
    'vaf$': ( 'B_a_vec$' * 'B_a_vec$' ) > 'A_b_fun$' ).

tff('function_vaf$',axiom,
    'vaf$'('fmb_B_a_vec$_1','fmb_B_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uzs$',type,
    'uzs$': ( 'B_c_vec_a_vec$' * 'A$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_uzs$',axiom,
    'uzs$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_vec_lambda$p',type,
    'vec_lambda$p': 'C_b_a_vec_c_vec_fun$' > 'B_a_vec_c_vec_c_vec$' ).

tff('function_vec_lambda$p',axiom,
    'vec_lambda$p'('fmb_C_b_a_vec_c_vec_fun$_1') = 'fmb_B_a_vec_c_vec_c_vec$_1' ).

tff('declare_uxj$',type,
    'uxj$': ( 'A$' * 'B_a_vec_a_vec$' ) > 'A_b_fun$' ).

tff('function_uxj$',axiom,
    'uxj$'('fmb_A$_1','fmb_B_a_vec_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_mult_row_row$c',type,
    'mult_row_row$c': ( 'B_c_vec_a_vec$' * 'A$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_mult_row_row$c',axiom,
    'mult_row_row$c'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_plus$f',type,
    'plus$f': ( 'B_d_vec_d_vec$' * 'B_d_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_plus$f',axiom,
    'plus$f'('fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uwv$',type,
    'uwv$': 'B_c_vec_a_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uwv$',axiom,
    'uwv$'('fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_uud$',type,
    'uud$': ( 'A$' * 'D$' * 'B_c_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uud$',axiom,
    'uud$'('fmb_A$_1','fmb_D$_1','fmb_B_c_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_fun_app$g',type,
    'fun_app$g': ( 'A_b_d_vec_a_vec_fun$' * 'A$' ) > 'B_d_vec_a_vec$' ).

tff('function_fun_app$g',axiom,
    'fun_app$g'('fmb_A_b_d_vec_a_vec_fun$_1','fmb_A$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_vec$d',type,
    'vec$d': 'B_c_vec_a_vec$' > 'B_c_vec_a_vec_a_vec$' ).

tff('function_vec$d',axiom,
    'vec$d'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_rows$b',type,
    'rows$b': 'B_a_vec_d_vec$' > 'B_a_vec_set$' ).

tff('function_rows$b',axiom,
    'rows$b'('fmb_B_a_vec_d_vec$_1') = 'fmb_B_a_vec_set$_1' ).

tff('declare_vao$',type,
    'vao$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_vao$',axiom,
    'vao$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uuv$',type,
    'uuv$': ( 'B_b_fun$' * 'B_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uuv$',axiom,
    'uuv$'('fmb_B_b_fun$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uwi$',type,
    'uwi$': ( 'B_d_vec_c_vec$' * 'D$' ) > 'C_b_fun$' ).

tff('function_uwi$',axiom,
    'uwi$'('fmb_B_d_vec_c_vec$_1','fmb_D$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vba$',type,
    'vba$': ( 'B_c_vec$' * 'B_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_vba$',axiom,
    'vba$'('fmb_B_c_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_fun_app$t',type,
    'fun_app$t': ( 'A_b_a_vec_c_vec_fun$' * 'A$' ) > 'B_a_vec_c_vec$' ).

tff('function_fun_app$t',axiom,
    'fun_app$t'('fmb_A_b_a_vec_c_vec_fun$_1','fmb_A$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uwb$',type,
    'uwb$': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uwb$',axiom,
    'uwb$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_elt_set_plus$d',type,
    'elt_set_plus$d': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec_set$' ) > 'B_d_vec_a_vec_set$' ).

tff('function_elt_set_plus$d',axiom,
    'elt_set_plus$d'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec_set$_1') = 'fmb_B_d_vec_a_vec_set$_1' ).

tff('declare_elt_set_times$c',type,
    'elt_set_times$c': ( 'B$' * 'B_set$' ) > 'B_set$' ).

tff('function_elt_set_times$c',axiom,
    'elt_set_times$c'('fmb_B$_1','fmb_B_set$_1') = 'fmb_B_set$_1' ).

tff('declare_times$q',type,
    'times$q': ( 'B_d_vec_set$' * 'B_d_vec_set$' ) > 'B_d_vec_set$' ).

tff('function_times$q',axiom,
    'times$q'('fmb_B_d_vec_set$_1','fmb_B_d_vec_set$_1') = 'fmb_B_d_vec_set$_1' ).

tff('declare_elt_set_plus$f',type,
    'elt_set_plus$f': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec_set$' ) > 'B_c_vec_a_vec_set$' ).

tff('function_elt_set_plus$f',axiom,
    'elt_set_plus$f'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec_set$_1') = 'fmb_B_c_vec_a_vec_set$_1' ).

tff('declare_column$',type,
    'column$': ( 'C$' * 'B_c_vec_a_vec$' ) > 'B_a_vec$' ).

tff('function_column$',axiom,
    'column$'('fmb_C$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uvu$',type,
    'uvu$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uvu$',axiom,
    'uvu$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_column$g',type,
    'column$g': ( 'A$' * 'B_a_vec_a_vec$' ) > 'B_a_vec$' ).

tff('function_column$g',axiom,
    'column$g'('fmb_A$_1','fmb_B_a_vec_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_vbb$',type,
    'vbb$': 'B$' > 'D_b_fun$' ).

tff('function_vbb$',axiom,
    'vbb$'('fmb_B$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uvn$',type,
    'uvn$': ( 'B_d_vec_b_fun$' * 'B_d_vec_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uvn$',axiom,
    'uvn$'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uwc$',type,
    'uwc$': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uwc$',axiom,
    'uwc$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uzw$',type,
    'uzw$': ( 'B_c_vec_a_vec_a_vec$' * 'B_c_vec_a_vec_a_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uzw$',axiom,
    'uzw$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_vak$',type,
    'vak$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_vak$',axiom,
    'vak$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_row_add_row$c',type,
    'row_add_row$c': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_row_add_row$c',axiom,
    'row_add_row$c'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_columnvector_row$f',type,
    'columnvector_row$f': 'B_c_vec$' > 'C_b_a_vec_fun$' ).

tff('function_columnvector_row$f',axiom,
    'columnvector_row$f'('fmb_B_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vector_scalar_mult$c',type,
    'vector_scalar_mult$c': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec_a_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_vector_scalar_mult$c',axiom,
    'vector_scalar_mult$c'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_row_add$',type,
    'row_add$': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'B_c_vec_a_vec$' ).

tff('function_row_add$',axiom,
    'row_add$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_row_add$c',type,
    'row_add$c': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'B_d_vec_a_vec$' ).

tff('function_row_add$c',axiom,
    'row_add$c'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_uxi$',type,
    'uxi$': ( 'A$' * 'B_a_vec_c_vec$' ) > 'C_b_fun$' ).

tff('function_uxi$',axiom,
    'uxi$'('fmb_A$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_map_matrix$f',type,
    'map_matrix$f': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_a_vec$' ) > 'B_a_vec_a_vec$' ).

tff('function_map_matrix$f',axiom,
    'map_matrix$f'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_a_vec_a_vec$_1' ).

tff('declare_uze$',type,
    'uze$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uze$',axiom,
    'uze$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_interchange_columns_row$b',type,
    'interchange_columns_row$b': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' ) > 'C_b_a_vec_fun$' ).

tff('function_interchange_columns_row$b',axiom,
    'interchange_columns_row$b'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_times$p',type,
    'times$p': ( 'B_d_vec_a_vec_set$' * 'B_d_vec_a_vec_set$' ) > 'B_d_vec_a_vec_set$' ).

tff('function_times$p',axiom,
    'times$p'('fmb_B_d_vec_a_vec_set$_1','fmb_B_d_vec_a_vec_set$_1') = 'fmb_B_d_vec_a_vec_set$_1' ).

tff('declare_uvg$',type,
    'uvg$': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_a_vec$' * 'A$' ) > 'A_b_fun$' ).

tff('function_uvg$',axiom,
    'uvg$'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uue$',type,
    'uue$': ( 'D$' * 'D$' * 'B_d_vec_d_vec$' * 'B_d_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_uue$',axiom,
    'uue$'('fmb_D$_1','fmb_D$_1','fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_column_add$b',type,
    'column_add$b': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_column_add$b',axiom,
    'column_add$b'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_uvk$',type,
    'uvk$': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_c_vec$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uvk$',axiom,
    'uvk$'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_row_add$b',type,
    'row_add$b': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' * 'B$' ) > 'B_a_vec_c_vec$' ).

tff('function_row_add$b',axiom,
    'row_add$b'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1','fmb_B$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_column$c',type,
    'column$c': ( 'D$' * 'B_d_vec_d_vec$' ) > 'B_d_vec$' ).

tff('function_column$c',axiom,
    'column$c'('fmb_D$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_fun_app$y',type,
    'fun_app$y': ( 'B_b_d_vec_fun$' * 'B$' ) > 'B_d_vec$' ).

tff('function_fun_app$y',axiom,
    'fun_app$y'('fmb_B_b_d_vec_fun$_1','fmb_B$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_transpose_row$a',type,
    'transpose_row$a': 'B_d_vec_a_vec$' > 'D_b_a_vec_fun$' ).

tff('function_transpose_row$a',axiom,
    'transpose_row$a'('fmb_B_d_vec_a_vec$_1') = 'fmb_D_b_a_vec_fun$_1' ).

tff('declare_mult_column_row$',type,
    'mult_column_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_mult_column_row$',axiom,
    'mult_column_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_transpose_row$i',type,
    'transpose_row$i': ( 'B_a_vec_c_vec_c_vec$' * 'C$' ) > 'B_a_vec_c_vec$' ).

tff('function_transpose_row$i',axiom,
    'transpose_row$i'('fmb_B_a_vec_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uyz$',type,
    'uyz$': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uyz$',axiom,
    'uyz$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_row$d',type,
    'row$d': ( 'A$' * 'B_d_vec_a_vec$' ) > 'B_d_vec$' ).

tff('function_row$d',axiom,
    'row$d'('fmb_A$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_uyv$',type,
    'uyv$': ( 'B_d_vec_a_vec$' * 'D$' * 'B$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uyv$',axiom,
    'uyv$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_B$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_interchange_rows_row$d',type,
    'interchange_rows_row$d': ( 'B_d_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_d_vec_fun$' ).

tff('function_interchange_rows_row$d',axiom,
    'interchange_rows_row$d'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_interchange_columns_row$a',type,
    'interchange_columns_row$a': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_interchange_columns_row$a',axiom,
    'interchange_columns_row$a'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_times$c',type,
    'times$c': ( 'B_a_vec$' * 'B_a_vec$' ) > 'B_a_vec$' ).

tff('function_times$c',axiom,
    'times$c'('fmb_B_a_vec$_1','fmb_B_a_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_fun_app$v',type,
    'fun_app$v': ( 'B_d_vec_b_fun$' * 'B_d_vec$' ) > 'B$' ).

tff('function_fun_app$v',axiom,
    'fun_app$v'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec$_1') = 'fmb_B$_1' ).

tff('declare_uxu$',type,
    'uxu$': ( 'B_d_vec$' * 'D$' ) > 'A_b_fun$' ).

tff('function_uxu$',axiom,
    'uxu$'('fmb_B_d_vec$_1','fmb_D$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_fun_app$ae',type,
    'fun_app$ae': ( 'D_b_d_vec_bool_fun_fun$' * 'D$' ) > 'B_d_vec_bool_fun$' ).

tff('function_fun_app$ae',axiom,
    'fun_app$ae'('fmb_D_b_d_vec_bool_fun_fun$_1','fmb_D$_1') = 'fmb_B_d_vec_bool_fun$_1' ).

tff('declare_interchange_columns$d',type,
    'interchange_columns$d': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' ) > 'B_c_vec_a_vec$' ).

tff('function_interchange_columns$d',axiom,
    'interchange_columns$d'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_transpose$d',type,
    'transpose$d': 'B_d_vec_d_vec$' > 'B_d_vec_d_vec$' ).

tff('function_transpose$d',axiom,
    'transpose$d'('fmb_B_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_vac$',type,
    'vac$': ( 'B_a_vec_c_vec$' * 'B_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_vac$',axiom,
    'vac$'('fmb_B_a_vec_c_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vec_nth$f',type,
    'vec_nth$f': 'B_c_vec_d_vec$' > 'D_b_c_vec_fun$' ).

tff('function_vec_nth$f',axiom,
    'vec_nth$f'('fmb_B_c_vec_d_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_columnvector_row$a',type,
    'columnvector_row$a': 'B_d_vec$' > 'D_b_d_vec_fun$' ).

tff('function_columnvector_row$a',axiom,
    'columnvector_row$a'('fmb_B_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uzl$',type,
    'uzl$': ( 'B_a_vec_c_vec$' * 'C$' * 'B$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uzl$',axiom,
    'uzl$'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_B$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_columnvector_row$j',type,
    'columnvector_row$j': 'B_c_vec$' > 'C_b_d_vec_fun$' ).

tff('function_columnvector_row$j',axiom,
    'columnvector_row$j'('fmb_B_c_vec$_1') = 'fmb_C_b_d_vec_fun$_1' ).

tff('declare_column_add_row$b',type,
    'column_add_row$b': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_column_add_row$b',axiom,
    'column_add_row$b'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uzn$',type,
    'uzn$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uzn$',axiom,
    'uzn$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uzj$',type,
    'uzj$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uzj$',axiom,
    'uzj$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_transpose_row$k',type,
    'transpose_row$k': 'B_c_vec_d_vec$' > 'C_b_d_vec_fun$' ).

tff('function_transpose_row$k',axiom,
    'transpose_row$k'('fmb_B_c_vec_d_vec$_1') = 'fmb_C_b_d_vec_fun$_1' ).

tff('declare_interchange_rows_row$b',type,
    'interchange_rows_row$b': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' ) > 'C_b_a_vec_fun$' ).

tff('function_interchange_rows_row$b',axiom,
    'interchange_rows_row$b'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_rowvector$d',type,
    'rowvector$d': 'B_c_vec$' > 'B_c_vec_a_vec$' ).

tff('function_rowvector$d',axiom,
    'rowvector$d'('fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_vec_nth$k',type,
    'vec_nth$k': ( 'B_c_vec_c_vec$' * 'C$' ) > 'B_c_vec$' ).

tff('function_vec_nth$k',axiom,
    'vec_nth$k'('fmb_B_c_vec_c_vec$_1','fmb_C$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_row$b',type,
    'row$b': ( 'C$' * 'B_a_vec_c_vec$' ) > 'B_a_vec$' ).

tff('function_row$b',axiom,
    'row$b'('fmb_C$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_mult_row_row$b',type,
    'mult_row_row$b': ( 'B_a_vec_c_vec$' * 'C$' * 'B$' ) > 'C_b_a_vec_fun$' ).

tff('function_mult_row_row$b',axiom,
    'mult_row_row$b'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_interchange_rows$b',type,
    'interchange_rows$b': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_interchange_rows$b',axiom,
    'interchange_rows$b'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_mult_row$b',type,
    'mult_row$b': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'B_c_vec_a_vec_a_vec$' ).

tff('function_mult_row$b',axiom,
    'mult_row$b'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_uwl$',type,
    'uwl$': ( 'B_a_vec_a_vec$' * 'A$' ) > 'A_b_fun$' ).

tff('function_uwl$',axiom,
    'uwl$'('fmb_B_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_interchange_rows$d',type,
    'interchange_rows$d': ( 'B_c_vec_a_vec$' * 'A$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_interchange_rows$d',axiom,
    'interchange_rows$d'('fmb_B_c_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_vax$',type,
    'vax$': ( 'B$' * 'B_a_vec$' ) > 'A_b_fun$' ).

tff('function_vax$',axiom,
    'vax$'('fmb_B$_1','fmb_B_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uwk$',type,
    'uwk$': ( 'B_a_vec_c_vec$' * 'A$' ) > 'C_b_fun$' ).

tff('function_uwk$',axiom,
    'uwk$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_transpose_row$e',type,
    'transpose_row$e': 'B_d_vec_c_vec$' > 'D_b_c_vec_fun$' ).

tff('function_transpose_row$e',axiom,
    'transpose_row$e'('fmb_B_d_vec_c_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_columnvector_row$k',type,
    'columnvector_row$k': 'B_a_vec$' > 'A_b_d_vec_fun$' ).

tff('function_columnvector_row$k',axiom,
    'columnvector_row$k'('fmb_B_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_map_matrix$g',type,
    'map_matrix$g': ( 'B_a_vec_b_fun$' * 'B_a_vec_c_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_map_matrix$g',axiom,
    'map_matrix$g'('fmb_B_a_vec_b_fun$_1','fmb_B_a_vec_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_map_matrix$e',type,
    'map_matrix$e': ( 'B_b_d_vec_fun$' * 'B_a_vec_c_vec$' ) > 'B_d_vec_a_vec_c_vec$' ).

tff('function_map_matrix$e',axiom,
    'map_matrix$e'('fmb_B_b_d_vec_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_d_vec_a_vec_c_vec$_1' ).

tff('declare_elt_set_times$a',type,
    'elt_set_times$a': ( 'D_b_fun$' * 'D_b_fun_set$' ) > 'D_b_fun_set$' ).

tff('function_elt_set_times$a',axiom,
    'elt_set_times$a'('fmb_D_b_fun$_1','fmb_D_b_fun_set$_1') = 'fmb_D_b_fun_set$_1' ).

tff('declare_vec_lambda$e',type,
    'vec_lambda$e': 'A_b_c_vec_fun$' > 'B_c_vec_a_vec$' ).

tff('function_vec_lambda$e',axiom,
    ( ( 'vec_lambda$e'('fmb_A_b_c_vec_fun$_1') = 'fmb_B_c_vec_a_vec$_1' )
    & ( 'vec_lambda$e'('fmb_A_b_c_vec_fun$_2') = 'fmb_B_c_vec_a_vec$_1' ) ) ).

tff('declare_row$a',type,
    'row$a': ( 'A$' * 'B_c_vec_a_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_row$a',axiom,
    'row$a'('fmb_A$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uuy$',type,
    'uuy$': ( 'B_b_fun$' * 'B_d_vec_a_vec$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uuy$',axiom,
    'uuy$'('fmb_B_b_fun$_1','fmb_B_d_vec_a_vec$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uwh$',type,
    'uwh$': ( 'B_a_vec_d_vec$' * 'A$' ) > 'D_b_fun$' ).

tff('function_uwh$',axiom,
    'uwh$'('fmb_B_a_vec_d_vec$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_mult_row_row$',type,
    'mult_row_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_mult_row_row$',axiom,
    'mult_row_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_gauss_Jordan_wrapper$c',type,
    'gauss_Jordan_wrapper$c': ( 'A$' * 'D$' * 'B_c_vec_a_vec$' * 'B_d_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_gauss_Jordan_wrapper$c',axiom,
    'gauss_Jordan_wrapper$c'('fmb_A$_1','fmb_D$_1','fmb_B_c_vec_a_vec$_1','fmb_B_d_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_collect$a',type,
    'collect$a': 'D_b_fun_bool_fun$' > 'D_b_fun_set$' ).

tff('function_collect$a',axiom,
    'collect$a'('fmb_D_b_fun_bool_fun$_1') = 'fmb_D_b_fun_set$_1' ).

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

tff('function_times$e',axiom,
    'times$e'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec_a_vec$_1' ).

tff('declare_gauss_Jordan_wrapper$b',type,
    'gauss_Jordan_wrapper$b': ( 'A$' * 'C$' * 'B_c_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'B_c_vec_a_vec$' ).

tff('function_gauss_Jordan_wrapper$b',axiom,
    'gauss_Jordan_wrapper$b'('fmb_A$_1','fmb_C$_1','fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_vec_nth$i',type,
    'vec_nth$i': 'B_a_vec$' > 'A_b_fun$' ).

tff('function_vec_nth$i',axiom,
    'vec_nth$i'('fmb_B_a_vec$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_rowvector$e',type,
    'rowvector$e': 'B_a_vec$' > 'B_a_vec_d_vec$' ).

tff('function_rowvector$e',axiom,
    'rowvector$e'('fmb_B_a_vec$_1') = 'fmb_B_a_vec_d_vec$_1' ).

tff('declare_fun_app$l',type,
    'fun_app$l': ( 'C_b_c_vec_fun$' * 'C$' ) > 'B_c_vec$' ).

tff('function_fun_app$l',axiom,
    'fun_app$l'('fmb_C_b_c_vec_fun$_1','fmb_C$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_vab$',type,
    'vab$': ( 'B_d_vec_d_vec$' * 'B_d_vec_d_vec$' ) > 'D_b_d_vec_fun$' ).

tff('function_vab$',axiom,
    'vab$'('fmb_B_d_vec_d_vec$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uvl$',type,
    'uvl$': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uvl$',axiom,
    'uvl$'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_interchange_rows_row$a',type,
    'interchange_rows_row$a': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_interchange_rows_row$a',axiom,
    'interchange_rows_row$a'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_uzd$',type,
    'uzd$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' * 'A$' ) > 'A_b_c_vec_fun$' ).

tff('function_uzd$',axiom,
    'uzd$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1','fmb_A$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uyq$',type,
    'uyq$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'D_b_d_vec_fun$' ).

tff('function_uyq$',axiom,
    'uyq$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_D_b_d_vec_fun$_1' ).

tff('declare_uwg$',type,
    'uwg$': ( 'B_d_vec_d_vec$' * 'D$' ) > 'D_b_fun$' ).

tff('function_uwg$',axiom,
    'uwg$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_row_add$a',type,
    'row_add$a': ( 'B_d_vec_d_vec$' * 'D$' * 'D$' * 'B$' ) > 'B_d_vec_d_vec$' ).

tff('function_row_add$a',axiom,
    'row_add$a'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uxp$',type,
    'uxp$': 'B_c_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uxp$',axiom,
    'uxp$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_uwz$',type,
    'uwz$': 'B_a_vec_a_vec$' > 'A_b_a_vec_fun$' ).

tff('function_uwz$',axiom,
    'uwz$'('fmb_B_a_vec_a_vec$_1') = 'fmb_A_b_a_vec_fun$_1' ).

tff('declare_uxe$',type,
    'uxe$': ( 'A$' * 'B_c_vec_a_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_uxe$',axiom,
    'uxe$'('fmb_A$_1','fmb_B_c_vec_a_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uye$',type,
    'uye$': ( 'B_d_vec_a_vec$' * 'A$' ) > 'A_b_d_vec_fun$' ).

tff('function_uye$',axiom,
    'uye$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uvp$',type,
    'uvp$': 'B_a_vec$' > 'C_b_a_vec_fun$' ).

tff('function_uvp$',axiom,
    'uvp$'('fmb_B_a_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_rowvector$',type,
    'rowvector$': 'B_a_vec$' > 'B_a_vec_a_vec$' ).

tff('function_rowvector$',axiom,
    'rowvector$'('fmb_B_a_vec$_1') = 'fmb_B_a_vec_a_vec$_1' ).

tff('declare_elt_set_plus$b',type,
    'elt_set_plus$b': ( 'A_b_c_vec_fun$' * 'A_b_c_vec_fun_set$' ) > 'A_b_c_vec_fun_set$' ).

tff('function_elt_set_plus$b',axiom,
    ( ( 'elt_set_plus$b'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' )
    & ( 'elt_set_plus$b'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun_set$_1') = 'fmb_A_b_c_vec_fun_set$_1' ) ) ).

tff('declare_transpose$',type,
    'transpose$': 'B_c_vec_a_vec$' > 'B_a_vec_c_vec$' ).

tff('function_transpose$',axiom,
    'transpose$'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_transpose$h',type,
    'transpose$h': 'B_a_vec_d_vec$' > 'B_d_vec_a_vec$' ).

tff('function_transpose$h',axiom,
    'transpose$h'('fmb_B_a_vec_d_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_columns$',type,
    'columns$': 'B_a_vec_c_vec$' > 'B_c_vec_set$' ).

tff('function_columns$',axiom,
    'columns$'('fmb_B_a_vec_c_vec$_1') = 'fmb_B_c_vec_set$_1' ).

tff('declare_interchange_rows$a',type,
    'interchange_rows$a': ( 'B_a_vec_c_vec$' * 'C$' * 'C$' ) > 'B_a_vec_c_vec$' ).

tff('function_interchange_rows$a',axiom,
    'interchange_rows$a'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_map_matrix$m',type,
    'map_matrix$m': ( 'B_d_vec_b_fun$' * 'B_d_vec_d_vec_d_vec$' ) > 'B_d_vec_d_vec$' ).

tff('function_map_matrix$m',axiom,
    'map_matrix$m'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec_d_vec_d_vec$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_fun_app$k',type,
    'fun_app$k': ( 'D_b_a_vec_fun$' * 'D$' ) > 'B_a_vec$' ).

tff('function_fun_app$k',axiom,
    'fun_app$k'('fmb_D_b_a_vec_fun$_1','fmb_D$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_uva$',type,
    'uva$': ( 'B_b_c_vec_fun$' * 'B_a_vec_c_vec$' * 'C$' ) > 'A_b_c_vec_fun$' ).

tff('function_uva$',axiom,
    'uva$'('fmb_B_b_c_vec_fun$_1','fmb_B_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_A_b_c_vec_fun$_2' ).

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

tff('function_uminus$b',axiom,
    'uminus$b'('fmb_B_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_mult_row$a',type,
    'mult_row$a': ( 'B_a_vec_c_vec$' * 'C$' * 'B$' ) > 'B_a_vec_c_vec$' ).

tff('function_mult_row$a',axiom,
    'mult_row$a'('fmb_B_a_vec_c_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uui$',type,
    'uui$': ( 'C$' * 'D$' * 'B_a_vec_c_vec$' * 'B_d_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_uui$',axiom,
    'uui$'('fmb_C$_1','fmb_D$_1','fmb_B_a_vec_c_vec$_1','fmb_B_d_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_vau$',type,
    'vau$': ( 'B_a_vec$' * 'B_a_vec_c_vec$' ) > 'C_b_a_vec_fun$' ).

tff('function_vau$',axiom,
    'vau$'('fmb_B_a_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_a_vec_fun$_1' ).

tff('declare_uxt$',type,
    'uxt$': 'B_c_vec$' > 'C_b_c_vec_fun$' ).

tff('function_uxt$',axiom,
    'uxt$'('fmb_B_c_vec$_1') = 'fmb_C_b_c_vec_fun$_1' ).

tff('declare_mult_row$',type,
    'mult_row$': ( 'B_d_vec_d_vec$' * 'D$' * 'B$' ) > 'B_d_vec_d_vec$' ).

tff('function_mult_row$',axiom,
    'mult_row$'('fmb_B_d_vec_d_vec$_1','fmb_D$_1','fmb_B$_1') = 'fmb_B_d_vec_d_vec$_1' ).

tff('declare_uyr$',type,
    'uyr$': ( 'B_a_vec_c_vec$' * 'A$' * 'B$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uyr$',axiom,
    'uyr$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_B$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uzq$',type,
    'uzq$': ( 'B_d_vec_a_vec$' * 'A$' * 'B$' ) > 'A_b_d_vec_fun$' ).

tff('function_uzq$',axiom,
    'uzq$'('fmb_B_d_vec_a_vec$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_d_vec_fun$_1' ).

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

tff('function_uminus$a',axiom,
    'uminus$a'('fmb_B_c_vec_a_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uyy$',type,
    'uyy$': ( 'B_c_vec_a_vec$' * 'C$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_uyy$',axiom,
    'uyy$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_uvq$',type,
    'uvq$': 'B_c_vec_a_vec$' > 'A_b_c_vec_a_vec_fun$' ).

tff('function_uvq$',axiom,
    'uvq$'('fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_vector_scalar_mult$a',type,
    'vector_scalar_mult$a': ( 'B_a_vec$' * 'B_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_vector_scalar_mult$a',axiom,
    'vector_scalar_mult$a'('fmb_B_a_vec$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vec_nth$m',type,
    'vec_nth$m': ( 'B_a_vec_a_vec$' * 'A$' ) > 'B_a_vec$' ).

tff('function_vec_nth$m',axiom,
    'vec_nth$m'('fmb_B_a_vec_a_vec$_1','fmb_A$_1') = 'fmb_B_a_vec$_1' ).

tff('declare_map_matrix$a',type,
    'map_matrix$a': ( 'B_b_fun$' * 'B_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_map_matrix$a',axiom,
    'map_matrix$a'('fmb_B_b_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_uxf$',type,
    'uxf$': ( 'D$' * 'B_d_vec_d_vec$' ) > 'D_b_fun$' ).

tff('function_uxf$',axiom,
    'uxf$'('fmb_D$_1','fmb_B_d_vec_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_map_matrix$h',type,
    'map_matrix$h': ( 'B_c_vec_b_fun$' * 'B_c_vec_a_vec_c_vec$' ) > 'B_a_vec_c_vec$' ).

tff('function_map_matrix$h',axiom,
    'map_matrix$h'('fmb_B_c_vec_b_fun$_1','fmb_B_c_vec_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec$_1' ).

tff('declare_vay$',type,
    'vay$': ( 'B$' * 'B_d_vec$' ) > 'D_b_fun$' ).

tff('function_vay$',axiom,
    'vay$'('fmb_B$_1','fmb_B_d_vec$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_vai$',type,
    'vai$': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec$' ) > 'A_b_c_vec_fun$' ).

tff('function_vai$',axiom,
    'vai$'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_plus$a',type,
    'plus$a': ( 'B_d_vec$' * 'B_d_vec$' ) > 'B_d_vec$' ).

tff('function_plus$a',axiom,
    'plus$a'('fmb_B_d_vec$_1','fmb_B_d_vec$_1') = 'fmb_B_d_vec$_1' ).

tff('declare_row_add_row$',type,
    'row_add_row$': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_row_add_row$',axiom,
    'row_add_row$'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_mult_column_row$a',type,
    'mult_column_row$a': ( 'B_c_vec_a_vec_a_vec$' * 'A$' * 'B_c_vec$' ) > 'A_b_c_vec_a_vec_fun$' ).

tff('function_mult_column_row$a',axiom,
    'mult_column_row$a'('fmb_B_c_vec_a_vec_a_vec$_1','fmb_A$_1','fmb_B_c_vec$_1') = 'fmb_A_b_c_vec_a_vec_fun$_1' ).

tff('declare_columnvector$h',type,
    'columnvector$h': 'B_a_vec_c_vec$' > 'B_a_vec_c_vec_c_vec$' ).

tff('function_columnvector$h',axiom,
    'columnvector$h'('fmb_B_a_vec_c_vec$_1') = 'fmb_B_a_vec_c_vec_c_vec$_1' ).

tff('declare_transpose$b',type,
    'transpose$b': 'B_a_vec_c_vec$' > 'B_c_vec_a_vec$' ).

tff('function_transpose$b',axiom,
    'transpose$b'('fmb_B_a_vec_c_vec$_1') = 'fmb_B_c_vec_a_vec$_1' ).

tff('declare_uzi$',type,
    'uzi$': ( 'B_c_vec_a_vec$' * 'A$' * 'A$' * 'B$' ) > 'A_b_c_vec_fun$' ).

tff('function_uzi$',axiom,
    'uzi$'('fmb_B_c_vec_a_vec$_1','fmb_A$_1','fmb_A$_1','fmb_B$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_vec_nth$h',type,
    'vec_nth$h': 'B_c_vec$' > 'C_b_fun$' ).

tff('function_vec_nth$h',axiom,
    'vec_nth$h'('fmb_B_c_vec$_1') = 'fmb_C_b_fun$_1' ).

tff('declare_vec$a',type,
    'vec$a': 'B_d_vec$' > 'B_d_vec_a_vec$' ).

tff('function_vec$a',axiom,
    'vec$a'('fmb_B_d_vec$_1') = 'fmb_B_d_vec_a_vec$_1' ).

tff('declare_column$d',type,
    'column$d': ( 'D$' * 'B_d_vec_c_vec$' ) > 'B_c_vec$' ).

tff('function_column$d',axiom,
    'column$d'('fmb_D$_1','fmb_B_d_vec_c_vec$_1') = 'fmb_B_c_vec$_1' ).

tff('declare_uvf$',type,
    'uvf$': ( 'B_b_d_vec_fun$' * 'B_a_vec_c_vec$' ) > 'C_b_d_vec_a_vec_fun$' ).

tff('function_uvf$',axiom,
    'uvf$'('fmb_B_b_d_vec_fun$_1','fmb_B_a_vec_c_vec$_1') = 'fmb_C_b_d_vec_a_vec_fun$_1' ).

tff('declare_uvv$',type,
    'uvv$': ( 'B_a_vec_c_vec$' * 'A$' * 'A$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uvv$',axiom,
    'uvv$'('fmb_B_a_vec_c_vec$_1','fmb_A$_1','fmb_A$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_uxl$',type,
    'uxl$': ( 'A$' * 'B_d_vec_a_vec_a_vec$' ) > 'A_b_d_vec_fun$' ).

tff('function_uxl$',axiom,
    'uxl$'('fmb_A$_1','fmb_B_d_vec_a_vec_a_vec$_1') = 'fmb_A_b_d_vec_fun$_1' ).

tff('declare_uwr$',type,
    'uwr$': ( 'B_c_vec_a_vec$' * 'C$' * 'C$' ) > 'A_b_c_vec_fun$' ).

tff('function_uwr$',axiom,
    'uwr$'('fmb_B_c_vec_a_vec$_1','fmb_C$_1','fmb_C$_1') = 'fmb_A_b_c_vec_fun$_2' ).

tff('declare_fun_app$b',type,
    'fun_app$b': ( 'D_b_fun$' * 'D$' ) > 'B$' ).

tff('function_fun_app$b',axiom,
    'fun_app$b'('fmb_D_b_fun$_1','fmb_D$_1') = 'fmb_B$_1' ).

tff('declare_uxr$',type,
    'uxr$': 'B_d_vec$' > 'D_b_c_vec_fun$' ).

tff('function_uxr$',axiom,
    'uxr$'('fmb_B_d_vec$_1') = 'fmb_D_b_c_vec_fun$_1' ).

tff('declare_uvm$',type,
    'uvm$': ( 'B_d_vec_b_fun$' * 'B_d_vec_a_vec_c_vec$' * 'C$' ) > 'A_b_fun$' ).

tff('function_uvm$',axiom,
    'uvm$'('fmb_B_d_vec_b_fun$_1','fmb_B_d_vec_a_vec_c_vec$_1','fmb_C$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_van$',type,
    'van$': ( 'B_d_vec_a_vec$' * 'D$' * 'D$' * 'B$' * 'A$' ) > 'D_b_fun$' ).

tff('function_van$',axiom,
    'van$'('fmb_B_d_vec_a_vec$_1','fmb_D$_1','fmb_D$_1','fmb_B$_1','fmb_A$_1') = 'fmb_D_b_fun$_1' ).

tff('declare_uxb$',type,
    'uxb$': 'B_a_vec_c_vec_c_vec$' > 'C_b_a_vec_c_vec_fun$' ).

tff('function_uxb$',axiom,
    'uxb$'('fmb_B_a_vec_c_vec_c_vec$_1') = 'fmb_C_b_a_vec_c_vec_fun$_1' ).

tff('declare_member$f',type,
    'member$f': ( 'B_c_vec_a_vec$' * 'B_c_vec_a_vec_set$' ) > $o ).

tff('predicate_member$f',axiom,
    'member$f'('fmb_B_c_vec_a_vec$_1','fmb_B_c_vec_a_vec_set$_1') ).

tff('declare_member$',type,
    'member$': ( 'D_b_fun$' * 'D_b_fun_set$' ) > $o ).

tff('predicate_member$',axiom,
    'member$'('fmb_D_b_fun$_1','fmb_D_b_fun_set$_1') ).

tff('declare_member$j',type,
    'member$j': ( 'C_b_a_vec_fun$' * 'C_b_a_vec_fun_set$' ) > $o ).

tff('predicate_member$j',axiom,
    'member$j'('fmb_C_b_a_vec_fun$_1','fmb_C_b_a_vec_fun_set$_1') ).

tff('declare_fun_app$at',type,
    'fun_app$at': ( 'B_a_vec_c_vec_bool_fun$' * 'B_a_vec_c_vec$' ) > $o ).

tff('predicate_fun_app$at',axiom,
    'fun_app$at'('fmb_B_a_vec_c_vec_bool_fun$_1','fmb_B_a_vec_c_vec$_1') ).

tff('declare_member$c',type,
    'member$c': ( 'B$' * 'B_set$' ) > $o ).

tff('predicate_member$c',axiom,
    'member$c'('fmb_B$_1','fmb_B_set$_1') ).

tff('declare_fun_app$ab',type,
    'fun_app$ab': ( 'B_c_vec_a_vec_bool_fun$' * 'B_c_vec_a_vec$' ) > $o ).

tff('predicate_fun_app$ab',axiom,
    ~ 'fun_app$ab'('fmb_B_c_vec_a_vec_bool_fun$_1','fmb_B_c_vec_a_vec$_1') ).

tff('declare_less_eq$',type,
    'less_eq$': ( 'A_b_d_vec_fun_set$' * 'A_b_d_vec_fun_set$' ) > $o ).

tff('predicate_less_eq$',axiom,
    'less_eq$'('fmb_A_b_d_vec_fun_set$_1','fmb_A_b_d_vec_fun_set$_1') ).

tff('declare_fun_app$as',type,
    'fun_app$as': ( 'A_b_fun_bool_fun$' * 'A_b_fun$' ) > $o ).

tff('predicate_fun_app$as',axiom,
    'fun_app$as'('fmb_A_b_fun_bool_fun$_1','fmb_A_b_fun$_1') ).

tff('declare_member$k',type,
    'member$k': ( 'C_b_fun$' * 'C_b_fun_set$' ) > $o ).

tff('predicate_member$k',axiom,
    'member$k'('fmb_C_b_fun$_1','fmb_C_b_fun_set$_1') ).

tff('declare_member$a',type,
    'member$a': ( 'A_b_d_vec_fun$' * 'A_b_d_vec_fun_set$' ) > $o ).

tff('predicate_member$a',axiom,
    'member$a'('fmb_A_b_d_vec_fun$_1','fmb_A_b_d_vec_fun_set$_1') ).

tff('declare_less_eq$a',type,
    'less_eq$a': ( 'D_b_fun_set$' * 'D_b_fun_set$' ) > $o ).

tff('predicate_less_eq$a',axiom,
    'less_eq$a'('fmb_D_b_fun_set$_1','fmb_D_b_fun_set$_1') ).

tff('declare_fun_app$ao',type,
    'fun_app$ao': ( 'A_b_c_vec_a_vec_fun_bool_fun$' * 'A_b_c_vec_a_vec_fun$' ) > $o ).

tff('predicate_fun_app$ao',axiom,
    'fun_app$ao'('fmb_A_b_c_vec_a_vec_fun_bool_fun$_1','fmb_A_b_c_vec_a_vec_fun$_1') ).

tff('declare_fun_app$ap',type,
    'fun_app$ap': ( 'D_b_d_vec_fun_bool_fun$' * 'D_b_d_vec_fun$' ) > $o ).

tff('predicate_fun_app$ap',axiom,
    ~ 'fun_app$ap'('fmb_D_b_d_vec_fun_bool_fun$_1','fmb_D_b_d_vec_fun$_1') ).

tff('declare_member$e',type,
    'member$e': ( 'B_d_vec$' * 'B_d_vec_set$' ) > $o ).

tff('predicate_member$e',axiom,
    ~ 'member$e'('fmb_B_d_vec$_1','fmb_B_d_vec_set$_1') ).

tff('declare_member$d',type,
    'member$d': ( 'B_d_vec_a_vec$' * 'B_d_vec_a_vec_set$' ) > $o ).

tff('predicate_member$d',axiom,
    ~ 'member$d'('fmb_B_d_vec_a_vec$_1','fmb_B_d_vec_a_vec_set$_1') ).

tff('declare_member$b',type,
    'member$b': ( 'A_b_c_vec_fun$' * 'A_b_c_vec_fun_set$' ) > $o ).

tff('predicate_member$b',axiom,
    ( ~ 'member$b'('fmb_A_b_c_vec_fun$_1','fmb_A_b_c_vec_fun_set$_1')
    & 'member$b'('fmb_A_b_c_vec_fun$_2','fmb_A_b_c_vec_fun_set$_1') ) ).

tff('declare_fun_app$ad',type,
    'fun_app$ad': ( 'B_d_vec_bool_fun$' * 'B_d_vec$' ) > $o ).

tff('predicate_fun_app$ad',axiom,
    ~ 'fun_app$ad'('fmb_B_d_vec_bool_fun$_1','fmb_B_d_vec$_1') ).

tff('declare_fun_app$ar',type,
    'fun_app$ar': ( 'C_b_fun_bool_fun$' * 'C_b_fun$' ) > $o ).

tff('predicate_fun_app$ar',axiom,
    ~ 'fun_app$ar'('fmb_C_b_fun_bool_fun$_1','fmb_C_b_fun$_1') ).

tff('declare_member$g',type,
    'member$g': ( 'B_c_vec$' * 'B_c_vec_set$' ) > $o ).

tff('predicate_member$g',axiom,
    'member$g'('fmb_B_c_vec$_1','fmb_B_c_vec_set$_1') ).

tff('declare_fun_app$aq',type,
    'fun_app$aq': ( 'C_b_a_vec_fun_bool_fun$' * 'C_b_a_vec_fun$' ) > $o ).

tff('predicate_fun_app$aq',axiom,
    'fun_app$aq'('fmb_C_b_a_vec_fun_bool_fun$_1','fmb_C_b_a_vec_fun$_1') ).

tff('declare_member$i',type,
    'member$i': ( 'D_b_d_vec_fun$' * 'D_b_d_vec_fun_set$' ) > $o ).

tff('predicate_member$i',axiom,
    'member$i'('fmb_D_b_d_vec_fun$_1','fmb_D_b_d_vec_fun_set$_1') ).

tff('declare_fun_app$ak',type,
    'fun_app$ak': ( 'B_c_vec_bool_fun$' * 'B_c_vec$' ) > $o ).

tff('predicate_fun_app$ak',axiom,
    'fun_app$ak'('fmb_B_c_vec_bool_fun$_1','fmb_B_c_vec$_1') ).

tff('declare_fun_app$e',type,
    'fun_app$e': ( 'A_b_d_vec_fun_bool_fun$' * 'A_b_d_vec_fun$' ) > $o ).

tff('predicate_fun_app$e',axiom,
    'fun_app$e'('fmb_A_b_d_vec_fun_bool_fun$_1','fmb_A_b_d_vec_fun$_1') ).

tff('declare_member$l',type,
    'member$l': ( 'A_b_fun$' * 'A_b_fun_set$' ) > $o ).

tff('predicate_member$l',axiom,
    'member$l'('fmb_A_b_fun$_1','fmb_A_b_fun_set$_1') ).

tff('declare_member$h',type,
    'member$h': ( 'A_b_c_vec_a_vec_fun$' * 'A_b_c_vec_a_vec_fun_set$' ) > $o ).

tff('predicate_member$h',axiom,
    'member$h'('fmb_A_b_c_vec_a_vec_fun$_1','fmb_A_b_c_vec_a_vec_fun_set$_1') ).

tff('declare_fun_app$af',type,
    'fun_app$af': ( 'B_a_vec_bool_fun$' * 'B_a_vec$' ) > $o ).

tff('predicate_fun_app$af',axiom,
    'fun_app$af'('fmb_B_a_vec_bool_fun$_1','fmb_B_a_vec$_1') ).

tff('declare_fun_app$av',type,
    'fun_app$av': ( 'B_d_vec_a_vec_bool_fun$' * 'B_d_vec_a_vec$' ) > $o ).

tff('predicate_fun_app$av',axiom,
    ~ 'fun_app$av'('fmb_B_d_vec_a_vec_bool_fun$_1','fmb_B_d_vec_a_vec$_1') ).

tff('declare_fun_app$ah',type,
    'fun_app$ah': ( 'B_bool_fun$' * 'B$' ) > $o ).

tff('predicate_fun_app$ah',axiom,
    'fun_app$ah'('fmb_B_bool_fun$_1','fmb_B$_1') ).

tff('declare_fun_app$f',type,
    'fun_app$f': ( 'A_b_c_vec_fun_bool_fun$' * 'A_b_c_vec_fun$' ) > $o ).

tff('predicate_fun_app$f',axiom,
    ( ~ 'fun_app$f'('fmb_A_b_c_vec_fun_bool_fun$_1','fmb_A_b_c_vec_fun$_1')
    & 'fun_app$f'('fmb_A_b_c_vec_fun_bool_fun$_1','fmb_A_b_c_vec_fun$_2') ) ).

tff('declare_fun_app$d',type,
    'fun_app$d': ( 'D_b_fun_bool_fun$' * 'D_b_fun$' ) > $o ).

tff('predicate_fun_app$d',axiom,
    'fun_app$d'('fmb_D_b_fun_bool_fun$_1','fmb_D_b_fun$_1') ).

tff('declare_fun_app$au',type,
    'fun_app$au': ( 'B_c_vec_a_vec_a_vec_bool_fun$' * 'B_c_vec_a_vec_a_vec$' ) > $o ).

tff('predicate_fun_app$au',axiom,
    'fun_app$au'('fmb_B_c_vec_a_vec_a_vec_bool_fun$_1','fmb_B_c_vec_a_vec_a_vec$_1') ).

tff('declare_less_eq$b',type,
    'less_eq$b': ( 'A_b_c_vec_fun_set$' * 'A_b_c_vec_fun_set$' ) > $o ).

tff('predicate_less_eq$b',axiom,
    'less_eq$b'('fmb_A_b_c_vec_fun_set$_1','fmb_A_b_c_vec_fun_set$_1') ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP333_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37  % Computer : n007.cluster.edu
% 0.10/0.37  % Model    : x86_64 x86_64
% 0.10/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37  % Memory   : 8046.5625MB
% 0.10/0.37  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Sun Sep 27 12:52:40 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41  Running first-order model finding
% 0.10/0.41  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
% 7.49/1.72  % (1390656)Will run a generic schedule for satisfiability detection.
% 7.49/1.72  % (1390666)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=829850859:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.49/1.72  % (1390662)% WARNING: option uhcvi not known.
% 7.49/1.72  % (1390661)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1084818729_2999 on theBenchmark for (2999ds/0Mi)
% 7.49/1.72  % (1390662)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=865217282:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.49/1.72  % (1390663)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2959665052:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.49/1.72  % (1390664)dis+10_1_sil=32000:sp=arity:random_seed=3138403765:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.49/1.72  % (1390665)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2609823249:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.49/1.72  % (1390667)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=897968160:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.49/1.72  % (1390666)Instruction limit reached! 
% 7.49/1.72  % (1390666)------------------------------
% 7.49/1.72  % (1390666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390666)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390666)Termination reason: Instruction limit
% 7.49/1.72  % (1390666)Termination phase: Saturation
% 7.49/1.72  % (1390666)Time elapsed: 0.039 s
% 7.49/1.72  % (1390666)Peak memory usage: 15 MB
% 7.49/1.72  % (1390666)Instructions burned: 132 (million)
% 7.49/1.72  % (1390675)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=793315016:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.49/1.72  % (1390664)Instruction limit reached! 
% 7.49/1.72  % (1390664)------------------------------
% 7.49/1.72  % (1390664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390664)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390664)Termination reason: Instruction limit
% 7.49/1.72  % (1390664)Termination phase: Saturation
% 7.49/1.72  % (1390664)Time elapsed: 0.056 s
% 7.49/1.72  % (1390664)Peak memory usage: 14 MB
% 7.49/1.72  % (1390664)Instructions burned: 103 (million)
% 7.49/1.72  % (1390665)Instruction limit reached! 
% 7.49/1.72  % (1390665)------------------------------
% 7.49/1.72  % (1390665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390665)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390665)Termination reason: Instruction limit
% 7.49/1.72  % (1390665)Termination phase: Saturation
% 7.49/1.72  % (1390665)Time elapsed: 0.060 s
% 7.49/1.72  % (1390665)Peak memory usage: 14 MB
% 7.49/1.72  % (1390665)Instructions burned: 116 (million)
% 7.49/1.72  % (1390677)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2224791452:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.49/1.72  % (1390678)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=1169158292:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.49/1.72  % (1390667)Instruction limit reached! 
% 7.49/1.72  % (1390667)------------------------------
% 7.49/1.72  % (1390667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390667)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390667)Termination reason: Instruction limit
% 7.49/1.72  % (1390667)Termination phase: Saturation
% 7.49/1.72  % (1390667)Time elapsed: 0.090 s
% 7.49/1.72  % (1390667)Peak memory usage: 15 MB
% 7.49/1.72  % (1390667)Instructions burned: 159 (million)
% 7.49/1.72  % (1390681)ott-21_1_sil=16000:fs=off:random_seed=3024270900:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.49/1.72  % (1390677)Instruction limit reached! 
% 7.49/1.72  % (1390677)------------------------------
% 7.49/1.72  % (1390677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390677)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390677)Termination reason: Instruction limit
% 7.49/1.72  % (1390677)Termination phase: Saturation
% 7.49/1.72  % (1390677)Time elapsed: 0.070 s
% 7.49/1.72  % (1390677)Peak memory usage: 14 MB
% 7.49/1.72  % (1390677)Instructions burned: 131 (million)
% 7.49/1.72  % TRYING [1]
% 7.49/1.72  % TRYING [2]
% 7.49/1.72  % (1390683)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3570708344:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 7.49/1.72  % (1390681)Instruction limit reached! 
% 7.49/1.72  % (1390681)------------------------------
% 7.49/1.72  % (1390681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390681)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390681)Termination reason: Instruction limit
% 7.49/1.72  % (1390681)Termination phase: Saturation
% 7.49/1.72  % (1390681)Time elapsed: 0.100 s
% 7.49/1.72  % (1390681)Peak memory usage: 15 MB
% 7.49/1.72  % (1390681)Instructions burned: 181 (million)
% 7.49/1.72  % (1390675)Instruction limit reached! 
% 7.49/1.72  % (1390675)------------------------------
% 7.49/1.72  % (1390675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390675)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390675)Termination reason: Instruction limit
% 7.49/1.72  % (1390675)Termination phase: Finite model building SAT solving
% 7.49/1.72  % (1390675)Time elapsed: 0.179 s
% 7.49/1.72  % (1390675)Peak memory usage: 36 MB
% 7.49/1.72  % (1390675)Instructions burned: 715 (million)
% 7.49/1.72  % (1390685)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1503856208:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 7.49/1.72  % (1390686)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=760860533:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.49/1.72  % (1390678)Instruction limit reached! 
% 7.49/1.72  % (1390678)------------------------------
% 7.49/1.72  % (1390678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390678)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390678)Termination reason: Instruction limit
% 7.49/1.72  % (1390678)Termination phase: Saturation
% 7.49/1.72  % (1390678)Time elapsed: 0.351 s
% 7.49/1.72  % (1390678)Peak memory usage: 19 MB
% 7.49/1.72  % (1390678)Instructions burned: 686 (million)
% 7.49/1.72  % (1390689)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3701425585:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 7.49/1.72  % (1390683)Instruction limit reached! 
% 7.49/1.72  % (1390683)------------------------------
% 7.49/1.72  % (1390683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390683)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390683)Termination reason: Instruction limit
% 7.49/1.72  % (1390683)Termination phase: Saturation
% 7.49/1.72  % (1390683)Time elapsed: 0.293 s
% 7.49/1.72  % (1390683)Peak memory usage: 15 MB
% 7.49/1.72  % (1390683)Instructions burned: 477 (million)
% 7.49/1.72  % (1390691)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2809795318:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 7.49/1.72  % (1390686)Instruction limit reached! 
% 7.49/1.72  % (1390686)------------------------------
% 7.49/1.72  % (1390686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390686)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390686)Termination reason: Instruction limit
% 7.49/1.72  % (1390686)Termination phase: Saturation
% 7.49/1.72  % (1390686)Time elapsed: 0.367 s
% 7.49/1.72  % (1390686)Peak memory usage: 26 MB
% 7.49/1.72  % (1390686)Instructions burned: 1180 (million)
% 7.49/1.72  % (1390685)Instruction limit reached! 
% 7.49/1.72  % (1390685)------------------------------
% 7.49/1.72  % (1390685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390685)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390685)Termination reason: Instruction limit
% 7.49/1.72  % (1390685)Termination phase: Finite model building preprocessing
% 7.49/1.72  % (1390685)Time elapsed: 0.373 s
% 7.49/1.72  % (1390685)Peak memory usage: 21 MB
% 7.49/1.72  % (1390685)Instructions burned: 865 (million)
% 7.49/1.72  % (1390693)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2616532952:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 7.49/1.72  % (1390694)fmb+10_1_sil=64000:random_seed=2198073701:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 7.49/1.72  % (1390689)Instruction limit reached! 
% 7.49/1.72  % (1390689)------------------------------
% 7.49/1.72  % (1390689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390689)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390689)Termination reason: Instruction limit
% 7.49/1.72  % (1390689)Termination phase: Finite model building preprocessing
% 7.49/1.72  % (1390689)Time elapsed: 0.386 s
% 7.49/1.72  % (1390689)Peak memory usage: 21 MB
% 7.49/1.72  % (1390689)Instructions burned: 889 (million)
% 7.49/1.72  % (1390697)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3130309133:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 7.49/1.72  % (1390693)Instruction limit reached! 
% 7.49/1.72  % (1390693)------------------------------
% 7.49/1.72  % (1390693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390693)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390693)Termination reason: Instruction limit
% 7.49/1.72  % (1390693)Termination phase: Saturation
% 7.49/1.72  % (1390693)Time elapsed: 0.256 s
% 7.49/1.72  % (1390693)Peak memory usage: 19 MB
% 7.49/1.72  % (1390693)Instructions burned: 880 (million)
% 7.49/1.72  % (1390699)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2447784552:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 7.49/1.72  % (1390691)Instruction limit reached! 
% 7.49/1.72  % (1390691)------------------------------
% 7.49/1.72  % (1390691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390691)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390691)Termination reason: Instruction limit
% 7.49/1.72  % (1390691)Termination phase: Saturation
% 7.49/1.72  % (1390691)Time elapsed: 0.423 s
% 7.49/1.72  % (1390691)Peak memory usage: 23 MB
% 7.49/1.72  % (1390691)Instructions burned: 693 (million)
% 7.49/1.72  % (1390701)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2326720652:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 7.49/1.72  % (1390699)Instruction limit reached! 
% 7.49/1.72  % (1390699)------------------------------
% 7.49/1.72  % (1390699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.72  % (1390699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.72  % (1390699)CaDiCaL version: 2.1.3
% 7.49/1.72  % (1390699)Termination reason: Instruction limit
% 7.49/1.72  % (1390699)Termination phase: Finite model building preprocessing
% 7.49/1.72  % (1390699)Time elapsed: 0.208 s
% 7.49/1.72  % (1390699)Peak memory usage: 21 MB
% 7.49/1.72  % (1390699)Instructions burned: 923 (million)
% 7.49/1.72  % (1390703)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=56380250:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 7.49/1.72  % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.49/1.72  % Detected maximum model sizes of [max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,max,2]
% 7.49/1.72  % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.49/1.72  % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2]
% 7.49/1.72  % TRYING [1,1,1,1,1,1,2,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2]
% 7.49/1.72  % Finite Model Found!
% 7.49/1.72  % SZS status CounterSatisfiable for theBenchmark
% 7.49/1.72  % (1390661) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1390656-1390661"...
% 7.49/1.72  % (1390661)...printing done.
% 7.49/1.72  % SZS output start FiniteModel for theBenchmark
% See solution above
% 7.49/1.74  % (1390661)------------------------------
% 7.49/1.74  % (1390661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.49/1.74  % (1390661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.74  % (1390661)CaDiCaL version: 2.1.3
% 7.49/1.74  % (1390661)Termination reason: Satisfiable
% 7.49/1.74  % (1390661)Time elapsed: 1.216 s
% 7.49/1.74  % (1390661)Peak memory usage: 33 MB
% 7.49/1.74  % (1390661)Instructions burned: 2921 (million)
% 7.49/1.74  % (1390656)Success in time 1.301 s
% 7.49/1.74  % Vampire exiting
%------------------------------------------------------------------------------