%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP330_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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 : Fri Sep 25 01:49:27 PM UTC 2026
% Result : Theorem 8.79s 2.22s
% Output : CNFRefutation 8.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP330_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.79 % Computer : n019.cluster.edu
% 0.12/0.79 % Model : x86_64 x86_64
% 0.12/0.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.79 % Memory : 8046.5625MB
% 0.12/0.79 % OS : Linux 6.8.0-71-generic
% 0.12/0.79 % CPULimit : 300
% 0.12/0.79 % WCLimit : 300
% 0.12/0.79 % DateTime : Wed Sep 23 18:23:35 UTC 2026
% 0.12/0.79 % CPUTime :
% 0.12/0.79 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.83 Running first-order theorem proving
% 0.15/0.83 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.84
% 0.15/0.84 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.84
% 0.15/0.84 % Detected problem language: tptp
% 0.15/0.85 % Proving...
% 8.79/2.22 % SZS status Started for theBenchmark.p
% 8.79/2.22 ERROR - "ProverProcess:heur/409474:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 4 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution true --res_lit_sel pos_max --res_lit_sel_side num_var --res_ordering kbo_pred --res_passive_queue_type priority_queues --res_passive_queues "[[-num_lits];[-conj_symb;-num_symb;+num_symb]]" --res_passive_queues_freq "[15;3]" --res_prop_simpl_given false --res_prop_simpl_new true --res_sim_input true --res_time_limit 202.80 --res_to_prop_solver passive --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/x13z49j3 2>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/x13z49j3_error
% 8.79/2.22 ERROR - "ProverProcess:heur/469571:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 6 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3.0 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 32 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp false --inst_learning_factor 10 --inst_learning_loop_flag true --inst_learning_start 256 --inst_lit_activity_flag true --inst_lit_sel "[+sign;-ground;-non_prol_conj_symb;-num_var]" --inst_lit_sel_side num_lit --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-ground;-epr]]" --inst_passive_queues_freq "[2]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 0.6939020527068606 --inst_solver_per_active 8 --inst_sos_flag false --inst_start_prop_sim_after_learn 9 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 128 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/b8u7g7c1 2>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/b8u7g7c1_error
% 8.79/2.22 ERROR - "ProverProcess:heur/346297:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 8.79/2.22 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_sup_deep_mult 6 --comb_sup_mult 32 --conj_cone_tolerance 2.7380125131254 --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red false --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 1024 --inst_lit_activity_flag true --inst_lit_sel "[+depth;+sign;+num_symb;-split;-eq]" --inst_lit_sel_side cnt --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-num_lits];[-max_atom_input_occur;-ground]]" --inst_passive_queues_freq "[8;50]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.21724605765256222 --inst_solver_per_active 256 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-depth;+non_prol_conj_symb;-split;-ground;+num_var]" --inst_start_prop_sim_after_learn 8 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl true --prep_def_merge_tr_cl true --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim false --prep_sem_filter none --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten false --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 32 --pure_diseq_elim false --resolution_flag false --schedule none --share_sel_clauses false --smt_ac_axioms full --smt_preprocessing true --splitting_cvd true --splitting_cvd_svl false --splitting_grd true --splitting_mode full --splitting_nvd 128 --stats_out none --sub_typing true --subs_bck_mult 0 --sup_full_bw "[Demod]" --sup_full_fw "[Subsumption;SubsumptionRes;UnitSubsAndRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_full_triv "[PropSubs;Unflattening]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability]" --sup_immed_fw_main "[SubsumptionRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_immed_triv "[]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm]" --sup_input_bw "[]" --sup_input_fw "[]" --sup_input_triv "[PropSubs;Unflattening]" --sup_iter_deepening 4 --sup_passive_queue_type queue --sup_passive_queues "[[+num_symb]]" --sup_passive_queues_freq "[5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.4432297345384799 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/elg6lpep 2>> /export/starexec/sandbox2/tmp/iprover_out_12hqohn2/elg6lpep_error
% 8.79/2.22 % SZS status Theorem for theBenchmark.p
% 8.79/2.22
% 8.79/2.22 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.79/2.22
% 8.79/2.22 % ------ iProver source info
% 8.79/2.22
% 8.79/2.22 % git: date: 2026-07-19 20:42:38 +0200
% 8.79/2.22 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.79/2.22 % git: non_committed_changes: false
% 8.79/2.22
% 8.79/2.22 % ------ Parsing...
% 8.79/2.22 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 8.79/2.22 %
% 8.79/2.22
% 8.79/2.22 % ------ Preprocessing... sup_sim: 2 pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 pe_s pe_e %
% 8.79/2.22
% 8.79/2.22 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 8.79/2.22 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 8.79/2.22 %
% 8.79/2.22
% 8.79/2.22 % ------ Preprocessing...
% 8.79/2.22 % ------ Proving...
% 8.79/2.22 % ------ Problem Properties
% 8.79/2.22
% 8.79/2.22 %
% 8.79/2.22 % clauses 78
% 8.79/2.22 % conjectures 0
% 8.79/2.22 % EPR 3
% 8.79/2.22 % Horn 57
% 8.79/2.22 % unary 21
% 8.79/2.22 % binary 50
% 8.79/2.22 % lits 142
% 8.79/2.22 % lits eq 110
% 8.79/2.22 % fd_pure 0
% 8.79/2.22 % fd_pseudo 0
% 8.79/2.22 % fd_cond 4
% 8.79/2.22 % fd_pseudo_cond 14
% 8.79/2.22 % AC symbols 0
% 8.79/2.22
% 8.79/2.22 % ------ Schedule dynamic 5 is on
% 8.79/2.22
% 8.79/2.22 % ------ no conjectures: strip conj schedule
% 8.79/2.22
% 8.79/2.22 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 8.79/2.22
% 8.79/2.22
% 8.79/2.22 % ------
% 8.79/2.22 % Current options:
% 8.79/2.22 % ------
% 8.79/2.22
% 8.79/2.22
% 8.79/2.22 %
% 8.79/2.22
% 8.79/2.22 % ------ Proving...
% 8.79/2.22 %
% 8.79/2.22
% 8.79/2.22 % SZS status Theorem for theBenchmark.p
% 8.79/2.22
% 8.79/2.22 % SZS output start CNFRefutation for theBenchmark.p
% 8.79/2.22
% 8.79/2.22 tff(func_def_0, type, 'column_add_row$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(pred_def_1, type, 'inj_on$e': ('N_a_n_vec_fun_n_a_fun_fun$' * 'N_a_n_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_2, type, 'inj_on$g': ('M_a_m_vec_fun_m_a_fun_fun$' * 'M_a_m_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_3, type, 'fun_app$aa': ('A_bool_fun$' * 'A$') > $o).
% 8.79/2.22 tff(pred_def_4, type, 'member$f': ('N_a_n_vec_m_vec_fun$' * 'N_a_n_vec_m_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_5, type, 'fun_app$au': ('M_a_m_vec_m_vec_fun_bool_fun$' * 'M_a_m_vec_m_vec_fun$') > $o).
% 8.79/2.22 tff(pred_def_6, type, 'member$i': ('N_a_fun$' * 'N_a_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_7, type, 'member$a': ('A_m_vec$' * 'A_m_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_8, type, 'member$g': ('M_a_m_vec_m_vec_fun$' * 'M_a_m_vec_m_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_9, type, 'fun_app$s': ('M_bool_fun$' * 'M$') > $o).
% 8.79/2.22 tff(pred_def_10, type, 'fun_app$at': ('N_a_n_vec_m_vec_fun_bool_fun$' * 'N_a_n_vec_m_vec_fun$') > $o).
% 8.79/2.22 tff(pred_def_11, type, 'fun_app$q': ('M_a_m_vec_fun_bool_fun$' * 'M_a_m_vec_fun$') > $o).
% 8.79/2.22 tff(pred_def_12, type, 'inj_on$a': ('N_a_n_vec_fun$' * 'N_set$') > $o).
% 8.79/2.22 tff(pred_def_13, type, 'inj_on$h': ('M_a_m_vec_fun_m_a_m_vec_fun_fun$' * 'M_a_m_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_14, type, 'fun_app$p': ('N_a_n_vec_fun_bool_fun$' * 'N_a_n_vec_fun$') > $o).
% 8.79/2.22 tff(pred_def_15, type, 'inj_on$': ('M_a_m_vec_fun$' * 'M_set$') > $o).
% 8.79/2.22 tff(pred_def_16, type, 'fun_app$r': ('N_bool_fun$' * 'N$') > $o).
% 8.79/2.22 tff(pred_def_17, type, 'fun_app$w': ('A_m_vec_m_vec_bool_fun$' * 'A_m_vec_m_vec$') > $o).
% 8.79/2.22 tff(pred_def_18, type, 'less$': ('M_set$' * 'M_set$') > $o).
% 8.79/2.22 tff(func_def_19, type, 'det$b': 'A_m_vec_m_vec_m_vec$' > 'A_m_vec$').
% 8.79/2.22 tff(pred_def_20, type, 'fun_app$bl': ('A_m_vec_m_vec_m_vec_bool_fun$' * 'A_m_vec_m_vec_m_vec$') > $o).
% 8.79/2.22 tff(pred_def_21, type, 'inj_on$c': ('A_m_vec_a_m_vec_fun$' * 'A_m_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_22, type, 'member$e': ('M$' * 'M_set$') > $o).
% 8.79/2.22 tff(pred_def_23, type, 'is_basis$a': 'A_m_vec_set$' > $o).
% 8.79/2.22 tff(pred_def_24, type, 'member$j': ('M_a_fun$' * 'M_a_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_25, type, 'fun_app$v': ('A_n_vec_m_vec_bool_fun$' * 'A_n_vec_m_vec$') > $o).
% 8.79/2.22 tff(pred_def_26, type, 'member$h': ('M_a_n_vec_fun$' * 'M_a_n_vec_fun_set$') > $o).
% 8.79/2.22 tff(func_def_27, type, 'plus$a': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(pred_def_28, type, 'inj_on$b': ('A_n_vec_a_n_vec_fun$' * 'A_n_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_29, type, 'member$d': ('N$' * 'N_set$') > $o).
% 8.79/2.22 tff(pred_def_30, type, 'member$c': ('M_a_m_vec_fun$' * 'M_a_m_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_31, type, 'is_basis$': 'A_n_vec_set$' > $o).
% 8.79/2.22 tff(pred_def_32, type, 'fun_app$o': ('A_n_vec_bool_fun$' * 'A_n_vec$') > $o).
% 8.79/2.22 tff(pred_def_33, type, 'less$a': ('A_m_vec_set$' * 'A_m_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_34, type, 'fun_app$bk': ('A_n_vec_n_vec_bool_fun$' * 'A_n_vec_n_vec$') > $o).
% 8.79/2.22 tff(pred_def_35, type, 'member$': ('A_n_vec$' * 'A_n_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_36, type, 'fun_app$an': ('M_a_fun_bool_fun$' * 'M_a_fun$') > $o).
% 8.79/2.22 tff(pred_def_37, type, 'inj_on$f': ('A_m_vec_a_fun$' * 'A_m_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_38, type, 'inj_on$d': ('A_n_vec_a_fun$' * 'A_n_vec_set$') > $o).
% 8.79/2.22 tff(pred_def_39, type, 'fun_app$': ('A_m_vec_bool_fun$' * 'A_m_vec$') > $o).
% 8.79/2.22 tff(pred_def_40, type, 'member$b': ('N_a_n_vec_fun$' * 'N_a_n_vec_fun_set$') > $o).
% 8.79/2.22 tff(pred_def_41, type, 'fun_app$av': ('M_a_n_vec_fun_bool_fun$' * 'M_a_n_vec_fun$') > $o).
% 8.79/2.22 tff(pred_def_42, type, 'fun_app$ao': ('N_a_fun_bool_fun$' * 'N_a_fun$') > $o).
% 8.79/2.22 tff(func_def_43, type, 'uzo$': 'A_n_vec_n_vec$' > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_44, type, 'cart_basis_Rn$': 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_45, type, 'uza$': 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_46, type, 'interchange_rows_row$a': ('A_n_vec_n_vec$' * 'N$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_47, type, 'uyj$': 'A_n_vec_set$' > 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_48, type, 'uwh$': ('N_m_a_n_vec_fun_fun$' * 'M_set$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_49, type, 'uyb$': ('N$' * 'N_a_fun$' * 'N_a_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_50, type, 'vec_lambda$g': 'N_a_n_vec_n_vec_fun$' > 'A_n_vec_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_51, type, 'comp$w': ('A_n_vec_a_m_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_52, type, 'uzy$': ('A_a_n_vec_fun$' * 'A_n_vec_m_vec$') > 'M_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_53, type, 'uxs$': ('M$' * 'M_a_fun$' * 'M_a_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_54, type, 'vba$': 'A_n_vec$' > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_55, type, 'uut$': 'N_a_fun$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_56, type, 'sum$n': ('A_m_vec_a_fun$' * 'A_m_vec_set$') > 'A$').
% 8.79/2.22 tff(func_def_57, type, 'fun_app$ar': ('A_n_vec_a_m_vec_fun$' * 'A_n_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_58, type, 'uwt$': ('M_n_a_n_vec_fun_fun$' * 'N_set$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_59, type, 'top$l': 'N_bool_fun$').
% 8.79/2.22 tff(func_def_60, type, 'comp$s': ('M_a_n_vec_fun$' * 'N_m_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_61, type, 'collect$d': 'A_n_vec_bool_fun$' > 'A_n_vec_set$').
% 8.79/2.22 tff(func_def_62, type, 'uul$': ('N_a_fun$' * 'A_m_vec$') > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_63, type, 'det$c': 'A_n_vec_n_vec_n_vec$' > 'A_n_vec$').
% 8.79/2.22 tff(func_def_64, type, 'uzm$': 'A_n_vec_m_vec$' > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_65, type, 'uuq$': 'A_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_66, type, 'vde$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_67, type, 'column$': ('M$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_68, type, 'uvc$': 'A_n_vec_m_vec_n_vec$' > 'A_n_vec_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_69, type, 'top$d': 'M_a_m_vec_fun_set$').
% 8.79/2.22 tff(func_def_70, type, 'top$i': 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_71, type, 'vap$': ('A_m_vec_m_vec$' * 'A_n_vec_n_vec$' * 'A_m_vec_a_n_vec_fun$') > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_72, type, 'vec_lambda$e': 'M_a_m_vec_m_vec_fun$' > 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_73, type, 'collect$b': 'A_n_vec_m_vec_bool_fun$' > 'A_n_vec_m_vec_set$').
% 8.79/2.22 tff(func_def_74, type, 'collect$': 'A_m_vec_bool_fun$' > 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_75, type, 'fun_app$ay': ('M_a_n_vec_bool_fun_fun$' * 'M$') > 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_76, type, 'the$a': 'M_a_fun_bool_fun$' > 'M_a_fun$').
% 8.79/2.22 tff(func_def_77, type, 'uzj$': 'A_m_vec_n_vec$' > 'M_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_78, type, 'uyd$': ('M$' * 'M_a_n_vec_fun$' * 'M_a_n_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_79, type, 'vector_matrix_mult$a': ('A_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_80, type, 'vep$': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_81, type, 'vbp$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$' * 'N$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_82, type, 'vec_nth$': 'A_n_vec$' > 'N_a_fun$').
% 8.79/2.22 tff(func_def_83, type, 'uvk$': 'N_a_n_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_84, type, 'uvg$': 'A_m_vec$' > 'A_bool_fun$').
% 8.79/2.22 tff(func_def_85, type, 'vdw$': ('M$' * 'A_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_86, type, 'fun_app$aq': ('A_a_m_vec_fun$' * 'A$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_87, type, 'uzt$': ('A_a_fun$' * 'A_m_vec_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_88, type, 'zero$b': 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_89, type, 'column_add$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_90, type, 'vec_lambda$h': 'M_a_n_vec_n_vec_fun$' > 'A_n_vec_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_91, type, 'uxr$': ('M$' * 'M_a_n_vec_fun$' * 'M_a_n_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_92, type, 'uwr$': 'M_m_a_m_vec_m_vec_fun_fun$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_93, type, 'uwd$': 'A_m_vec_m_vec_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_94, type, 'matrix_matrix_mult$c': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_95, type, 'uyt$': ('M_a_n_vec_fun$' * 'M_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_96, type, 'set_of_vector$c': 'A_n_vec_m_vec_n_vec$' > 'A_n_vec_m_vec_set$').
% 8.79/2.22 tff(func_def_97, type, 'map_matrix$b': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_98, type, 'fun_app$am': ('A_a_fun$' * 'A$') > 'A$').
% 8.79/2.22 tff(func_def_99, type, 'zero$': 'A_n_vec$').
% 8.79/2.22 tff(func_def_100, type, 'prod$c': ('N_a_n_vec_fun$' * 'N_set$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_101, type, 'trace$b': 'A_n_vec_m_vec_m_vec$' > 'A_n_vec$').
% 8.79/2.22 tff(func_def_102, type, 'vbw$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_103, type, 'uwb$': 'A_n_vec_n_vec$' > 'N_a_fun$').
% 8.79/2.22 tff(func_def_104, type, 'fun_app$h': ('M_a_m_vec_m_vec_fun$' * 'M$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_105, type, 'vec_nth$k': 'A_m_vec_n_vec$' > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_106, type, 'vdc$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_107, type, 'vaf$': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_108, type, 'uzs$': ('A_a_fun$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_109, type, 'vec_lambda$b': 'N_a_n_vec_fun$' > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_110, type, 'matrix_vector_mult$': 'A_m_vec_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_111, type, 'uwo$': 'N_m_a_fun_fun$' > 'M_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_112, type, 'vao$': ('A_n_vec_n_vec$' * 'A_m_vec_m_vec$' * 'A_n_vec_a_m_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_113, type, 'vby$': ('A_m_vec$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_114, type, 'vay$': 'A_m_vec_m_vec_m_vec$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_115, type, 'transpose_row$h': 'A_n_vec_m_vec_m_vec$' > 'M_a_n_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_116, type, 'columnvector_row$': 'A_n_vec_m_vec$' > 'M_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_117, type, 'comp$t': ('A_m_vec_a_fun$' * 'N_a_m_vec_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_118, type, 'interchange_columns_row$a': ('A_n_vec_n_vec$' * 'N$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_119, type, 'transpose_row$i': ('A_n_vec_m_vec_n_vec_n_vec$' * 'N$') > 'A_n_vec_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_120, type, 'row$': ('M$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_121, type, 'uzp$': ('A_a_fun$' * 'A_n_vec_m_vec$') > 'M_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_122, type, 'comp$n': ('M_a_fun$' * 'M_m_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_123, type, 'uwn$': ('N_m_a_fun_fun$' * 'M_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_124, type, 'vcb$': ('M_a_m_vec_fun$' * 'M_a_m_vec_fun$' * 'M_set$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_125, type, 'top$m': 'N_a_n_vec_m_vec_fun_set$').
% 8.79/2.22 tff(func_def_126, type, 'top$h': 'A_n_vec_set$').
% 8.79/2.22 tff(func_def_127, type, 'uva$': 'A_m_vec_n_vec$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_128, type, 'fun_app$ap': ('A_a_n_vec_fun$' * 'A$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_129, type, 'columnvector_row$c': 'A_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_130, type, 'zero$a': 'A$').
% 8.79/2.22 tff(func_def_131, type, 'cart_basis$': 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_132, type, 'columnvector_row$f': 'A_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_133, type, 'uvy$': 'A_m_vec_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_134, type, 'vdr$': 'A_n_vec_n_vec$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_135, type, 'fun_app$f': ('M_a_fun$' * 'M$') > 'A$').
% 8.79/2.22 tff(func_def_136, type, 'vbi$': ('A_n_vec_n_vec_n_vec$' * 'A_n_vec_n_vec_n_vec$' * 'N$') > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_137, type, 'trace$e': 'A_n_vec_n_vec_n_vec$' > 'A_n_vec$').
% 8.79/2.22 tff(func_def_138, type, 'vec_lambda$f': 'N_a_n_vec_m_vec_fun$' > 'A_n_vec_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_139, type, 'fun_app$az': ('N_a_bool_fun_fun$' * 'N$') > 'A_bool_fun$').
% 8.79/2.22 tff(func_def_140, type, 'uve$': 'A_n_vec_m_vec$' > 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_141, type, 'map_matrix$a': ('A_a_fun$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_142, type, 'uvo$': 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_143, type, 'map_matrix$e': ('A_a_n_vec_fun$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_144, type, 'top$g': 'M_bool_fun$').
% 8.79/2.22 tff(func_def_145, type, 'vec_nth$m': 'M_m_vec$' > 'M_m_fun$').
% 8.79/2.22 tff(func_def_146, type, 'matrix$b': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$' * 'A_n_vec_a_n_vec_fun$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_147, type, 'vee$': 'A_m_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_148, type, 'vcs$': ('A_n_vec_m_vec$' * 'A_n_vec_n_vec_m_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_149, type, 'ven$': ('M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_150, type, 'uwv$': ('M_n_a_n_vec_fun_fun$' * 'M_set$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_151, type, 'map_matrix$j': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_152, type, 'uxi$': ('N$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_153, type, 'zero$e': 'A_n_vec_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_154, type, 'ves$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_155, type, 'vas$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$' * 'A_n_vec_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_156, type, 'uxy$': ('M$' * 'M_a_fun$' * 'M_a_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_157, type, 'matrix$': ('A_n_vec_n_vec$' * 'A_m_vec_m_vec$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_158, type, 'uvh$': 'A_m_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_159, type, 'uuh$': 'N_a_n_vec_fun$' > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_160, type, 'transpose_row$e': 'A_n_vec_m_vec$' > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_161, type, 'comp$i': ('A_m_vec_a_fun$' * 'A_m_vec_a_m_vec_fun$') > 'A_m_vec_a_fun$').
% 8.79/2.22 tff(func_def_162, type, 'uwe$': ('N_n_a_n_vec_fun_fun$' * 'N_set$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_163, type, 'uyr$': ('M_a_n_vec_n_vec_fun$' * 'M_set$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_164, type, 'uuc$': 'N_a_n_vec_m_vec_fun$' > 'M_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_165, type, 'fun_app$n': ('A_m_vec_a_fun$' * 'A_m_vec$') > 'A$').
% 8.79/2.22 tff(func_def_166, type, 'vcp$': ('A_n_vec$' * 'A_n_vec_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_167, type, 'set_of_vector$d': 'A_m_vec_m_vec_m_vec$' > 'A_m_vec_m_vec_set$').
% 8.79/2.22 tff(func_def_168, type, 'uxf$': ('M_m_a_m_vec_fun_fun$' * 'M_set$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_169, type, 'fun_app$be': ('M_n_fun$' * 'M$') > 'N$').
% 8.79/2.22 tff(func_def_170, type, 'top$': 'M_set$').
% 8.79/2.22 tff(func_def_171, type, 'uuy$': ('A_m_vec$' * 'M_a_m_vec_m_vec_fun$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_172, type, 'set_of_vector$a': 'A_m_vec_n_vec$' > 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_173, type, 'uxp$': ('N$' * 'N_a_fun$' * 'N_a_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_174, type, 'vag$': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_175, type, 'sum$g': ('N_a_n_vec_m_vec_fun$' * 'N_set$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_176, type, 'uug$': 'M_a_n_vec_m_vec_fun$' > 'M_m_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_177, type, 'columnvector_row$g': 'A_n_vec_n_vec$' > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_178, type, 'vbn$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_179, type, 'fun_app$x': ('N_a_m_vec_fun$' * 'N$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_180, type, 'map_matrix$h': ('A_a_n_vec_fun$' * 'A_m_vec_m_vec$') > 'A_n_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_181, type, 'veq$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_182, type, 'transpose$a': 'A_m_vec_m_vec$' > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_183, type, 'uue$': 'M_a_m_vec_m_vec_m_vec_fun$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_184, type, 'uvn$': 'M_bool_fun$').
% 8.79/2.22 tff(func_def_185, type, 'vbx$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_186, type, 'vbl$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_187, type, 'transpose_row$a': 'A_n_vec_n_vec$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_188, type, 'coord$a': 'A_m_vec_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_189, type, 'vec_lambda$c': 'M_a_m_vec_fun$' > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_190, type, 'vea$': ('A_n_vec_n_vec$' * 'A_n_vec$' * 'N$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_191, type, 'interchange_columns$': 'A_m_vec_m_vec$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_192, type, 'fun_app$aw': ('N_a_n_vec_m_vec_bool_fun_fun$' * 'N$') > 'A_n_vec_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_193, type, 'vbc$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_a_fun_bool_fun$').
% 8.79/2.22 tff(func_def_194, type, 'comp$e': ('A_a_m_vec_fun$' * 'M_a_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_195, type, 'vec_nth$j': 'A_n_vec_m_vec_m_vec$' > 'M_a_n_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_196, type, 'vector_scalar_mult$c': ('A_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_197, type, 'comp$r': ('M_a_m_vec_fun$' * 'N_m_fun$') > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_198, type, 'uyy$': 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_199, type, 'fun_app$bd': ('N_n_fun$' * 'N$') > 'N$').
% 8.79/2.22 tff(func_def_200, type, 'zero$g': 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_201, type, 'top$p': 'N_a_fun_set$').
% 8.79/2.22 tff(func_def_202, type, 'fun_app$ac': ('M_n_a_n_vec_fun_fun$' * 'M$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_203, type, 'vbd$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_fun_bool_fun$').
% 8.79/2.22 tff(func_def_204, type, 'comp$k': ('A_n_vec_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_205, type, 'uzf$': 'A$' > 'A_n_vec_a_fun$').
% 8.79/2.22 tff(func_def_206, type, 'vdd$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_207, type, 'vec_nth$l': 'M_n_vec$' > 'N_m_fun$').
% 8.79/2.22 tff(func_def_208, type, 'uzv$': ('A_a_n_vec_fun$' * 'A_n_vec_n_vec$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_209, type, 'vch$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_210, type, 'uuv$': ('A$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_211, type, 'comp$y': ('M_a_fun$' * 'N_m_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_212, type, 'fun_app$y': ('N_m_fun$' * 'N$') > 'M$').
% 8.79/2.22 tff(func_def_213, type, 'vdg$': ('A_n_vec_m_vec_n_vec$' * 'A_n_vec_m_vec$') > 'N_m_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_214, type, 'uxd$': 'M_m_a_fun_fun$' > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_215, type, 'fun_app$af': ('N_m_a_fun_fun$' * 'N$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_216, type, 'uwj$': ('N_m_a_n_vec_fun_fun$' * 'N_set$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_217, type, 'vaa$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_218, type, 'vdk$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_219, type, 'vec_nth$g': 'A_m_vec_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_220, type, 'fun_app$bj': ('M_a_m_vec_fun_a_fun$' * 'M_a_m_vec_fun$') > 'A$').
% 8.79/2.22 tff(func_def_221, type, 'fun_app$bf': ('A_m_vec_n_fun$' * 'A_m_vec$') > 'N$').
% 8.79/2.22 tff(func_def_222, type, 'vector_scalar_mult$b': ('A_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_223, type, 'top$o': 'M_a_n_vec_fun_set$').
% 8.79/2.22 tff(func_def_224, type, 'uyi$': 'M_a_m_vec_fun_set$' > 'M_a_m_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_225, type, 'fun_app$l': ('M_a_n_vec_m_vec_fun$' * 'M$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_226, type, 'uyo$': ('N_a_n_vec_m_vec_fun$' * 'N_set$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_227, type, 'uyv$': ('N_a_m_vec_fun$' * 'N_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_228, type, 'map_matrix$c': ('A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_229, type, 'map_matrix$k': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_230, type, 'vec_nth$f': 'A_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_231, type, 'set_of_vector$i': 'A_n_vec_n_vec$' > 'A_n_vec_set$').
% 8.79/2.22 tff(func_def_232, type, 'transpose_row$b': 'A_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_233, type, 'sum$': ('M_a_m_vec_fun$' * 'M_set$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_234, type, 'cart_basis$c': 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_235, type, 'uzu$': ('A_a_fun$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_236, type, 'rows$': 'A_m_vec_m_vec$' > 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_237, type, 'uze$': 'A$' > 'A_m_vec_a_fun$').
% 8.79/2.22 tff(func_def_238, type, 'comp$d': ('A_a_m_vec_fun$' * 'A_m_vec_a_fun$') > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_239, type, 'interchange_rows$a': ('A_n_vec_n_vec$' * 'N$') > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_240, type, 'comp$v': ('N_a_m_vec_fun$' * 'M_n_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_241, type, 'vbz$': ('M_a_m_vec_fun$' * 'A_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_242, type, 'uvv$': 'A_m_vec_a_fun$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_243, type, tltrue: tlbool).
% 8.79/2.22 tff(func_def_244, type, 'transpose_row$g': 'A_n_vec_n_vec_m_vec$' > 'N_a_n_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_245, type, 'uzl$': 'A_m_vec_m_vec_m_vec$' > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_246, type, 'fun_app$al': ('M_a_n_vec_n_vec_fun$' * 'M$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_247, type, 'row_add$a': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_248, type, 'j$': 'N$').
% 8.79/2.22 tff(func_def_249, type, 'mult_column_row$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_250, type, 'vec_lambda$': 'N_a_fun$' > 'A_n_vec$').
% 8.79/2.22 tff(func_def_251, type, 'vdt$': ('M$' * 'A_m_vec_m_vec$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_252, type, 'uxb$': ('M_n_a_fun_fun$' * 'M_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_253, type, 'set_of_vector$g': 'A_m_vec$' > 'A_set$').
% 8.79/2.22 tff(func_def_254, type, 'vai$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_255, type, 'vdf$': ('A_m_vec_m_vec$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_256, type, 'vec_nth$i': 'A_n_vec_m_vec$' > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_257, type, 'sum$j': ('M_a_n_vec_n_vec_fun$' * 'M_set$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_258, type, 'uvj$': 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_259, type, 'van$': ('A_n_vec_n_vec$' * 'A_m_vec_m_vec$' * 'A_n_vec_a_m_vec_fun$') > 'M_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_260, type, 'uyw$': ('M_a_m_vec_m_vec_fun$' * 'M_set$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_261, type, 'sum$e': ('N_a_n_vec_n_vec_fun$' * 'N_set$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_262, type, 'vbh$': ('A_m_vec_m_vec_m_vec$' * 'A_m_vec_m_vec_m_vec$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_263, type, 'mult_column$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_264, type, 'vei$': ('A$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_265, type, 'top$c': 'N_a_n_vec_fun_set$').
% 8.79/2.22 tff(func_def_266, type, 'set_of_vector$f': 'A_n_vec$' > 'A_set$').
% 8.79/2.22 tff(func_def_267, type, 'trace$c': 'A_m_vec_m_vec$' > 'A$').
% 8.79/2.22 tff(func_def_268, type, 'vec_nth$e': ('A_n_vec_m_vec_n_vec_n_vec$' * 'N$') > 'A_n_vec_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_269, type, 'vau$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$' * 'A_m_vec_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_270, type, 'collect$e': 'A_bool_fun$' > 'A_set$').
% 8.79/2.22 tff(func_def_271, type, 'transpose_row$f': 'A_n_vec_m_vec_n_vec$' > 'M_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_272, type, 'comp$f': 'A_m_vec_a_m_vec_fun$' > 'M_a_m_vec_fun_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_273, type, 'uuk$': 'M_a_m_vec_fun$' > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_274, type, 'vec_nth$c': 'A_m_vec_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_275, type, 'vct$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec_n_vec$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_276, type, 'vector_scalar_mult$': 'A$' > 'A_n_vec_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_277, type, 'fun_app$t': ('N_n_a_fun_fun$' * 'N$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_278, type, 'uvx$': 'A_n_vec_m_vec_n_vec_n_vec$' > 'N_a_n_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_279, type, 'vdm$': ('M$' * 'A_m_vec_m_vec$' * 'A_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_280, type, 'uux$': ('A$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_281, type, 'vbe$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_282, type, 'fun_app$b': ('A_n_vec_a_n_vec_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_283, type, 'vcz$': ('A_m_vec_m_vec$' * 'M$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_284, type, 'uyl$': 'A_m_vec_set$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_285, type, 'uzc$': 'M_a_fun$').
% 8.79/2.22 tff(func_def_286, type, 'vdo$': ('N$' * 'A_n_vec_n_vec$' * 'A_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_287, type, 'uur$': 'A_n_vec_a_fun$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_288, type, 'uwx$': 'M_m_a_n_vec_fun_fun$' > 'M_m_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_289, type, 'veo$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_290, type, 'uxo$': ('N$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_291, type, 'var$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$' * 'A_n_vec_a_n_vec_fun$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_292, type, 'vcm$': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_293, type, 'vector_matrix_mult$': ('A_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_294, type, 'uup$': 'A_n_vec$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_295, type, 'comp$ab': ('N_a_fun$' * 'M_n_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_296, type, 'column_add_row$a': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_297, type, 'vah$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_298, type, 'matrix$a': ('A_m_vec_m_vec$' * 'A_n_vec_n_vec$' * 'A_m_vec_a_n_vec_fun$') > 'A_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_299, type, 'collect$a': 'M_bool_fun$' > 'M_set$').
% 8.79/2.22 tff(func_def_300, type, 'vec_lambda$a': 'M_a_fun$' > 'A_m_vec$').
% 8.79/2.22 tff(func_def_301, type, 'vector_matrix_mult$c': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_302, type, 'vcy$': ('A_n_vec_n_vec$' * 'N$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_303, type, 'vcd$': ('A_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_304, type, 'vdj$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_305, type, 'mat_mult_row$a': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_306, type, 'collect$h': 'N_bool_fun$' > 'N_set$').
% 8.79/2.22 tff(func_def_307, type, 'fun_app$ak': ('M_a_m_vec_fun_m_a_fun_fun$' * 'M_a_m_vec_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_308, type, 'uzd$': 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_309, type, 'comp$h': ('A_a_fun$' * 'N_a_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_310, type, 'row_add$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_311, type, 'times$': 'A_n_vec$' > 'A_n_vec_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_312, type, 'uyn$': ('A_m_vec_m_vec$' * 'A_m_vec_a_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_313, type, 'uxu$': ('N$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_314, type, 'vec_nth$n': 'A_n_vec_n_vec_m_vec$' > 'M_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_315, type, 'fun_app$j': ('N_a_n_vec_n_vec_fun$' * 'N$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_316, type, 'comp$q': ('A_n_vec_a_fun$' * 'M_a_n_vec_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_317, type, 'uyf$': ('M$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_318, type, 'divide$': 'A$' > 'A_a_fun$').
% 8.79/2.22 tff(func_def_319, type, 'uvd$': 'A_m_vec_m_vec_m_vec$' > 'A_m_vec_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_320, type, 'fun_app$bi': ('N_a_n_vec_fun_a_fun$' * 'N_a_n_vec_fun$') > 'A$').
% 8.79/2.22 tff(func_def_321, type, 'set_of_vector$e': 'A_n_vec_m_vec$' > 'A_n_vec_set$').
% 8.79/2.22 tff(func_def_322, type, 'trace$f': 'A_m_vec_m_vec_m_vec$' > 'A_m_vec$').
% 8.79/2.22 tff(func_def_323, type, 'uxz$': ('M$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_324, type, 'uuw$': ('A$' * 'M_a_n_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_325, type, 'times$d': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_326, type, 'uu$': 'M_a_fun$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_327, type, 'sum$d': ('M_a_n_vec_fun$' * 'M_set$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_328, type, 'mult_column_row$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_329, type, 'veg$': ('A$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_330, type, 'map_matrix$d': ('A_a_m_vec_fun$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_331, type, 'sum$o': ('N_a_n_vec_fun_a_fun$' * 'N_a_n_vec_fun_set$') > 'A$').
% 8.79/2.22 tff(func_def_332, type, 'matrix_vector_mult$b': ('A_n_vec_m_vec_n_vec$' * 'A_n_vec_m_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_333, type, 'matrix_matrix_mult$a': ('A_m_vec_m_vec_m_vec$' * 'A_m_vec_m_vec_m_vec$') > 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_334, type, 'mult_row_row$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_335, type, 'vac$': ('A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_336, type, 'vdq$': 'A_m_vec_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_337, type, 'zero$c': 'A_m_vec$').
% 8.79/2.22 tff(func_def_338, type, 'vad$': ('A_a_m_vec_fun$' * 'A_m_vec_m_vec$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_339, type, 'vce$': ('A$' * 'A_m_vec$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_340, type, 'sum$h': ('N_a_m_vec_fun$' * 'N_set$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_341, type, 'mat_mult_row$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_342, type, 'vev$': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_343, type, 'set_of_vector$h': 'A_m_vec_m_vec$' > 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_344, type, 'comp$m': ('M_a_m_vec_fun$' * 'M_m_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_345, type, 'uxg$': 'M_m_a_m_vec_fun_fun$' > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_346, type, 'comp$z': ('A_m_vec_a_n_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_347, type, 'fun_app$c': ('N_a_fun$' * 'N$') > 'A$').
% 8.79/2.22 tff(func_def_348, type, 'uxn$': ('M$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_349, type, 'row_add_row$a': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_350, type, 'matrix$c': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$' * 'A_m_vec_a_m_vec_fun$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_351, type, 'uvq$': 'A_n_vec_n_vec$' > 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_352, type, 'uzx$': ('A_a_n_vec_fun$' * 'A_n_vec_m_vec$') > 'M_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_353, type, 'vaq$': ('A_m_vec_m_vec$' * 'A_n_vec_n_vec$' * 'A_m_vec_a_n_vec_fun$') > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_354, type, 'vcv$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec_m_vec$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_355, type, 'uxh$': ('M_m_a_m_vec_fun_fun$' * 'M_set$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_356, type, 'matrix_matrix_mult$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_357, type, 'comp$': 'A_n_vec_a_fun$' > 'N_a_n_vec_fun_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_358, type, 'transpose$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_359, type, 'vdy$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_360, type, 'vdl$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_361, type, 'sum$p': ('M_a_m_vec_fun_a_fun$' * 'M_a_m_vec_fun_set$') > 'A$').
% 8.79/2.22 tff(func_def_362, type, 'uxt$': ('M$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_363, type, 'vbr$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_364, type, 'uvr$': ('A_m_vec_m_vec$' * 'M_a_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_365, type, 'collect$g': 'M_a_m_vec_fun_bool_fun$' > 'M_a_m_vec_fun_set$').
% 8.79/2.22 tff(func_def_366, type, 'veu$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_367, type, 'fun_app$a': ('N_a_n_vec_fun$' * 'N$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_368, type, 'column_add$a': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_369, type, 'uyc$': ('M$' * 'M_a_m_vec_m_vec_fun$' * 'M_a_m_vec_m_vec_fun$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_370, type, 'uxq$': ('M$' * 'M_a_m_vec_m_vec_fun$' * 'M_a_m_vec_m_vec_fun$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_371, type, 'prod$': ('M_a_fun$' * 'M_set$') > 'A$').
% 8.79/2.22 tff(func_def_372, type, 'fun_app$ad': ('N_m_a_n_vec_fun_fun$' * 'N$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_373, type, 'comp$c': ('A_a_fun$' * 'M_a_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_374, type, 'vcu$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_375, type, 'uyz$': 'N_a_fun$').
% 8.79/2.22 tff(func_def_376, type, 'uwg$': ('N_n_a_n_vec_fun_fun$' * 'N_set$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_377, type, 'vel$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_378, type, 'comp$j': ('A_n_vec_a_fun$' * 'A_n_vec_a_n_vec_fun$') > 'A_n_vec_a_fun$').
% 8.79/2.22 tff(func_def_379, type, 'vbq$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_380, type, 'fun_app$e': ('A_m_vec_a_m_vec_fun$' * 'A_m_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_381, type, 'uvl$': 'M_a_m_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_382, type, 'vdi$': ('A_m_vec_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_383, type, 'vec_nth$b': 'A_m_vec$' > 'M_a_fun$').
% 8.79/2.22 tff(func_def_384, type, 'fun_app$as': ('A_m_vec_a_n_vec_fun$' * 'A_m_vec$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_385, type, 'vdn$': ('M$' * 'A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_386, type, 'top$b': 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_387, type, 'cart_basis_Rm$': 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_388, type, 'trace$d': 'A_n_vec_n_vec$' > 'A$').
% 8.79/2.22 tff(func_def_389, type, 'vds$': ('M$' * 'A$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_390, type, 'vek$': ('M$' * 'M$' * 'A_m_vec_m_vec$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_391, type, 'interchange_columns$a': ('A_n_vec_n_vec$' * 'N$') > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_392, type, 'fun_app$ag': ('M_m_a_m_vec_m_vec_fun_fun$' * 'M$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_393, type, 'uwu$': 'M_n_a_n_vec_fun_fun$' > 'N_m_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_394, type, 'ved$': 'A_m_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_395, type, 'uum$': ('N_a_fun$' * 'A_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_396, type, 'matrix_vector_mult$d': ('A_m_vec_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_397, type, 'vab$': ('A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_398, type, 'vci$': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_399, type, 'uym$': ('A_n_vec_n_vec$' * 'A_n_vec_a_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_400, type, 'uui$': 'M_a_n_vec_fun$' > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_401, type, 'vbj$': ('A_n_vec_n_vec_n_vec$' * 'A_n_vec_n_vec_n_vec$') > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_402, type, 'mult_row_row$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_403, type, 'uuo$': ('M_a_fun$' * 'A_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_404, type, 'set_of_vector$': 'M_m_vec$' > 'M_set$').
% 8.79/2.22 tff(func_def_405, type, 'vector_scalar_mult$a': 'A$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_406, type, 'uyx$': ('M_a_m_vec_fun$' * 'M_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_407, type, 'uye$': ('M$' * 'M_a_fun$' * 'M_a_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_408, type, 'vca$': ('M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_409, type, 'ver$': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_410, type, 'row$a': ('N$' * 'A_n_vec_n_vec$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_411, type, 'times$b': 'A$' > 'A_a_fun$').
% 8.79/2.22 tff(func_def_412, type, 'vbm$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$' * 'M$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_413, type, 'vcj$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_414, type, 'plus$b': 'A$' > 'A_a_fun$').
% 8.79/2.22 tff(func_def_415, type, 'fun_app$bc': ('N_a_n_vec_bool_fun_fun$' * 'N$') > 'A_n_vec_bool_fun$').
% 8.79/2.22 tff(func_def_416, type, 'interchange_columns_row$': ('A_m_vec_m_vec$' * 'M$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_417, type, 'sum$c': ('M_a_fun$' * 'M_set$') > 'A$').
% 8.79/2.22 tff(func_def_418, type, 'vak$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_419, type, 'cart_basis$a': 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_420, type, 'set_of_vector$b': 'M_n_vec$' > 'M_set$').
% 8.79/2.22 tff(func_def_421, type, 'vec_nth$d': 'A_n_vec_m_vec_n_vec$' > 'N_a_n_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_422, type, 'vec$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_423, type, 'matrix_vector_mult$c': ('A_n_vec_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_424, type, 'uxe$': ('M_m_a_fun_fun$' * 'M_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_425, type, 'trace$a': 'A_m_vec_m_vec_m_vec_m_vec$' > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_426, type, 'fun_app$d': ('M_a_m_vec_fun$' * 'M$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_427, type, 'uvf$': 'A_n_vec$' > 'A_bool_fun$').
% 8.79/2.22 tff(func_def_428, type, tlfalse: tlbool).
% 8.79/2.22 tff(func_def_429, type, 'transpose_row$': 'A_m_vec_m_vec$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_430, type, 'map_matrix$f': ('A_a_fun$' * 'A_n_vec_m_vec$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_431, type, 'vbb$': 'A_m_vec$' > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_432, type, 'transpose_row$c': 'A_n_vec_n_vec_n_vec$' > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_433, type, 'vdh$': ('A_n_vec_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_434, type, 'vdp$': ('N$' * 'A_n_vec_n_vec$' * 'A_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_435, type, 'vec_lambda$i': 'N_a_m_vec_fun$' > 'A_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_436, type, 'matrix_scalar_mult$': ('A$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_437, type, 'mult_row$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_438, type, 'fun_app$z': ('M_m_fun$' * 'M$') > 'M$').
% 8.79/2.22 tff(func_def_439, type, 'vdz$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_440, type, 'plus$d': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_441, type, 'uzr$': ('A_a_fun$' * 'A_n_vec_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_442, type, 'comp$x': ('A_m_vec_a_fun$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec_a_fun$').
% 8.79/2.22 tff(func_def_443, type, 'uvz$': 'A_n_vec_m_vec_m_vec$' > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_444, type, 'fun_app$ax': ('M_a_m_vec_m_vec_bool_fun_fun$' * 'M$') > 'A_m_vec_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_445, type, 'transpose_row$j': 'A_m_vec_m_vec_m_vec_m_vec$' > 'M_a_m_vec_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_446, type, 'uzw$': ('A_a_n_vec_fun$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_447, type, 'interchange_rows_row$': ('A_m_vec_m_vec$' * 'M$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_448, type, 'uws$': ('M_m_a_m_vec_m_vec_fun_fun$' * 'M_set$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_449, type, 'vav$': 'A_n_vec_m_vec$' > 'M_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_450, type, 'scalar_product$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_451, type, 'scalar_product$a': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_452, type, 'fun_app$bb': ('M_a_m_vec_bool_fun_fun$' * 'M$') > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_453, type, 'vef$': ('A$' * 'A_m_vec_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_454, type, 'uyh$': 'N_a_n_vec_fun_set$' > 'N_a_n_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_455, type, 'uww$': ('M_m_a_n_vec_fun_fun$' * 'M_set$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_456, type, 'uys$': ('N_a_n_vec_fun$' * 'N_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_457, type, 'comp$u': ('N_a_n_vec_fun$' * 'M_n_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_458, type, 'uxa$': 'M_n_a_fun_fun$' > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_459, type, 'vbo$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_460, type, 'fun_app$i': ('M_a_m_vec_m_vec_m_vec_fun$' * 'M$') > 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_461, type, 'fun_app$ai': ('M_m_a_m_vec_fun_fun$' * 'M$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_462, type, 'top$e': 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_463, type, 'uwk$': ('N_n_a_fun_fun$' * 'N_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_464, type, 'uub$': 'N_a_n_vec_n_vec_fun$' > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_465, type, 'matrix_vector_mult$a': 'A_n_vec_n_vec$' > 'A_n_vec_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_466, type, 'fun_app$k': ('M_a_n_vec_fun$' * 'M$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_467, type, 'vcf$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_468, type, 'vet$': ('A_n_vec_n_vec$' * 'N$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_469, type, 'times$c': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_470, type, 'top$n': 'M_a_m_vec_m_vec_fun_set$').
% 8.79/2.22 tff(func_def_471, type, 'vcr$': ('A_n_vec_m_vec$' * 'A_n_vec_n_vec_m_vec$') > 'N_m_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_472, type, 'top$a': 'N_set$').
% 8.79/2.22 tff(func_def_473, type, 'comp$p': ('N_a_fun$' * 'N_n_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_474, type, 'uun$': ('M_a_fun$' * 'A_n_vec$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_475, type, 'sum$i': ('M_a_m_vec_m_vec_m_vec_fun$' * 'M_set$') > 'A_m_vec_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_476, type, 'mat_row$a': 'A_n_vec$' > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_477, type, 'uwi$': 'N_m_a_n_vec_fun_fun$' > 'M_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_478, type, 'comp$aa': ('A_n_vec_a_fun$' * 'A_m_vec_a_n_vec_fun$') > 'A_m_vec_a_fun$').
% 8.79/2.22 tff(func_def_479, type, 'uud$': 'N_a_m_vec_fun$' > 'M_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_480, type, 'vck$': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_481, type, 'uvs$': 'A_m_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_482, type, 'fun_app$ba': ('M_a_bool_fun_fun$' * 'M$') > 'A_bool_fun$').
% 8.79/2.22 tff(func_def_483, type, 'vej$': ('M_a_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_484, type, 'uwz$': ('M_n_a_fun_fun$' * 'N_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_485, type, 'vem$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_486, type, 'vcw$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_487, type, 'map_matrix$g': ('A_a_n_vec_fun$' * 'A_n_vec_m_vec$') > 'A_n_vec_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_488, type, 'mult_row$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_489, type, 'sum$b': ('N_a_fun$' * 'N_set$') > 'A$').
% 8.79/2.22 tff(func_def_490, type, 'zero$f': 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_491, type, 'fun_app$ae': ('M_n_a_fun_fun$' * 'M$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_492, type, 'uxv$': ('N$' * 'N_a_fun$' * 'N_a_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_493, type, 'fun_app$ab': ('N_n_a_n_vec_fun_fun$' * 'N$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_494, type, 'det$': 'A_n_vec_n_vec$' > 'A$').
% 8.79/2.22 tff(func_def_495, type, 'uxk$': ('M$' * 'M_a_m_vec_m_vec_fun$' * 'M_a_m_vec_m_vec_fun$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_496, type, 'vec_lambda$d': 'M_a_n_vec_fun$' > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_497, type, 'vbt$': ('A_n_vec_n_vec$' * 'N$' * 'N$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_498, type, 'comp$a': 'A_m_vec_a_fun$' > 'M_a_m_vec_fun_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_499, type, 'uwp$': ('N_m_a_fun_fun$' * 'N_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_500, type, 'the$': 'N_a_fun_bool_fun$' > 'N_a_fun$').
% 8.79/2.22 tff(func_def_501, type, 'vbk$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_502, type, 'val$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_503, type, 'vdx$': ('A_m_vec_m_vec$' * 'A_m_vec$' * 'M$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_504, type, 'transpose_row$d': 'A_m_vec_n_vec$' > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_505, type, 'columnvector_row$a': 'A_n_vec$' > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_506, type, 'fun_app$aj': ('N_a_n_vec_fun_n_a_fun_fun$' * 'N_a_n_vec_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_507, type, 'uvt$': 'A_n_vec_a_fun$' > 'A_n_vec_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_508, type, 'mat_row$': 'A_m_vec$' > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_509, type, 'vbf$': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_510, type, 'vdv$': ('A_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_511, type, 'sum$f': ('M_a_m_vec_m_vec_fun$' * 'M_set$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_512, type, 'uxx$': ('M$' * 'M_a_n_vec_fun$' * 'M_a_n_vec_fun$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_513, type, 'columnvector_row$b': 'A_m_vec$' > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_514, type, 'sum$k': ('M_a_n_vec_m_vec_fun$' * 'M_set$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_515, type, 'uuj$': 'M_a_m_vec_m_vec_fun$' > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_516, type, 'vcl$': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_517, type, 'interchange_rows$': 'A_m_vec_m_vec$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_518, type, 'comp$b': ('A_a_fun$' * 'A_m_vec_a_fun$') > 'A_m_vec_a_fun$').
% 8.79/2.22 tff(func_def_519, type, 'uwf$': 'N_n_a_n_vec_fun_fun$' > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_520, type, 'uuu$': 'M_a_fun$' > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_521, type, 'collect$c': 'A_m_vec_m_vec_bool_fun$' > 'A_m_vec_m_vec_set$').
% 8.79/2.22 tff(func_def_522, type, 'columnvector_row$d': 'A_m_vec_m_vec$' > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_523, type, 'uzn$': 'A_m_vec_m_vec$' > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_524, type, 'row_add_row$': ('A_m_vec_m_vec$' * 'M$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_525, type, 'zero$d': 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_526, type, 'uwl$': 'N_n_a_fun_fun$' > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_527, type, 'vector_matrix_mult$b': ('A_n_vec_m_vec$' * 'A_n_vec_n_vec_m_vec$') > 'A_n_vec_n_vec$').
% 8.79/2.22 tff(func_def_528, type, 'top$j': 'N_a_n_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_529, type, 'columnvector_row$e': 'A_n_vec$' > 'N_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_530, type, 'fun_app$u': ('M_m_a_fun_fun$' * 'M$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_531, type, 'vcq$': ('A_n_vec$' * 'A_n_vec_n_vec$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_532, type, 'uvu$': ('A_n_vec_n_vec$' * 'A_n_vec_a_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_533, type, 'plus$c': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_534, type, 'uzg$': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_535, type, 'columns$': 'A_m_vec_m_vec$' > 'A_m_vec_set$').
% 8.79/2.22 tff(func_def_536, type, 'map_matrix$i': ('A_a_n_vec_fun$' * 'A_m_vec_n_vec$') > 'A_n_vec_m_vec_n_vec$').
% 8.79/2.22 tff(func_def_537, type, 'veb$': ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_538, type, 'f$': 'A_n_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_539, type, 'uvb$': 'M_n_vec$' > 'M_bool_fun$').
% 8.79/2.22 tff(func_def_540, type, 'uyu$': ('M_a_m_vec_m_vec_m_vec_fun$' * 'M_set$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_541, type, 'collect$f': 'N_a_n_vec_fun_bool_fun$' > 'N_a_n_vec_fun_set$').
% 8.79/2.22 tff(func_def_542, type, 'vector_matrix_mult$d': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_543, type, 'uvw$': ('A_m_vec_m_vec$' * 'A_m_vec_a_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_544, type, 'top$q': 'M_a_fun_set$').
% 8.79/2.22 tff(func_def_545, type, 'uzb$': 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_546, type, 'comp$g': ('A_a_fun$' * 'A_n_vec_a_fun$') > 'A_n_vec_a_fun$').
% 8.79/2.22 tff(func_def_547, type, 'matrix_change_of_basis$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_548, type, 'vcg$': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_n_a_fun_fun$').
% 8.79/2.22 tff(func_def_549, type, 'uxj$': ('N$' * 'N_a_fun$' * 'N_a_fun$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_550, type, 'prod$a': ('N_a_fun$' * 'N_set$') > 'A$').
% 8.79/2.22 tff(func_def_551, type, 'uyp$': ('M_a_n_vec_m_vec_fun$' * 'M_set$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_552, type, 'fun_app$bg': ('A_m_vec_m_fun$' * 'A_m_vec$') > 'M$').
% 8.79/2.22 tff(func_def_553, type, 'uyk$': 'M_set$' > 'M_bool_fun$').
% 8.79/2.22 tff(func_def_554, type, 'uxc$': ('M_m_a_fun_fun$' * 'M_set$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_555, type, 'vdb$': ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_556, type, 'top$k': 'M_a_m_vec_fun_bool_fun$').
% 8.79/2.22 tff(func_def_557, type, 'uzk$': 'A_m_vec_m_vec_m_vec_m_vec$' > 'M_m_a_m_vec_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_558, type, 'fun_app$g': ('N_a_n_vec_m_vec_fun$' * 'N$') > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_559, type, 'vae$': ('A_a_m_vec_fun$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_560, type, 'uvp$': ('A_n_vec_n_vec$' * 'N_a_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_561, type, 'uua$': 'A_m_vec_bool_fun$').
% 8.79/2.22 tff(func_def_562, type, 'plus$': 'A_n_vec$' > 'A_n_vec_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_563, type, 'fun_app$bh': ('M_a_m_vec_fun_m_a_m_vec_fun_fun$' * 'M_a_m_vec_fun$') > 'M_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_564, type, 'vaz$': 'A_m_vec_m_vec$' > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_565, type, 'sum$l': ('A_n_vec_a_n_vec_fun$' * 'A_n_vec_set$') > 'A_n_vec$').
% 8.79/2.22 tff(func_def_566, type, 'vda$': ('A_n_vec_n_vec$' * 'N$') > 'N_n_a_n_vec_fun_fun$').
% 8.79/2.22 tff(func_def_567, type, 'fun_app$ah': ('M_m_a_n_vec_fun_fun$' * 'M$') > 'M_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_568, type, 'vat$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$' * 'A_m_vec_a_m_vec_fun$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_569, type, 'vec_nth$h': 'A_n_vec_n_vec_n_vec$' > 'N_a_n_vec_n_vec_fun$').
% 8.79/2.22 tff(func_def_570, type, 'comp$l': ('A_m_vec_a_m_vec_fun$' * 'A_m_vec_a_m_vec_fun$') > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_571, type, 'map_matrix$': ('A_a_fun$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 8.79/2.22 tff(func_def_572, type, 'vbu$': ('A_m_vec_m_vec$' * 'M$' * 'M$') > 'M_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_573, type, 'trace$': 'A_n_vec_m_vec_n_vec_n_vec$' > 'A_n_vec_m_vec$').
% 8.79/2.22 tff(func_def_574, type, 'vcx$': ('A_m_vec_m_vec$' * 'M$') > 'M_m_a_m_vec_fun_fun$').
% 8.79/2.22 tff(func_def_575, type, 'uyg$': 'N_set$' > 'N_bool_fun$').
% 8.79/2.22 tff(func_def_576, type, 'times$a': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 8.79/2.22 tff(func_def_577, type, 'uwm$': ('N_n_a_fun_fun$' * 'N_set$') > 'N_a_fun$').
% 8.79/2.22 tff(func_def_578, type, 'uxm$': ('M$' * 'M_a_fun$' * 'M_a_fun$') > 'M_a_fun$').
% 8.79/2.22 tff(func_def_579, type, 'uxw$': ('M$' * 'M_a_m_vec_m_vec_fun$' * 'M_a_m_vec_m_vec_fun$') > 'M_a_m_vec_m_vec_fun$').
% 8.79/2.22 tff(func_def_580, type, 'uya$': ('N$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N_a_n_vec_fun$').
% 8.79/2.22 tff(func_def_581, type, 'uzz$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$') > 'N_m_a_fun_fun$').
% 8.79/2.22 tff(func_def_582, type, sK0: ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N$').
% 8.79/2.22 tff(func_def_583, type, sK1: 'M_set$' > 'M$').
% 8.79/2.22 tff(func_def_584, type, sK2: 'M$').
% 8.79/2.22 tff(func_def_585, type, sK3: ('M_set$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M$').
% 8.79/2.22 tff(func_def_586, type, sK4: ('M_set$' * 'M_a_m_vec_fun$' * 'M_a_m_vec_fun$') > 'M$').
% 8.79/2.22 tff(func_def_587, type, sK5: 'A_m_vec$' > 'M_a_fun$').
% 8.79/2.22 tff(func_def_588, type, sK6: ('A_m_vec$' * 'M_a_fun$') > 'M$').
% 8.79/2.22 tff(func_def_589, type, sK7: ('A_m_vec$' * 'A_m_vec$') > 'M$').
% 8.79/2.22 tff(func_def_590, type, sK8: ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M$').
% 8.79/2.22 tff(func_def_591, type, sK9: ('A_n_vec$' * 'N_a_fun$') > 'N$').
% 8.79/2.22 tff(func_def_592, type, sK10: ('N_a_fun$' * 'N_a_fun$') > 'N$').
% 8.79/2.22 tff(func_def_593, type, sK11: ('M_a_fun$' * 'M_a_fun$') > 'M$').
% 8.79/2.22 tff(func_def_594, type, sK12: ('M_set$' * 'M_a_fun$') > 'M$').
% 8.79/2.22 tff(func_def_595, type, sK13: ('N_set$' * 'N_a_fun$') > 'N$').
% 8.79/2.22 tff(func_def_596, type, sK14: ('M_a_fun$' * 'M_set$') > 'M$').
% 8.79/2.22 tff(func_def_597, type, sK15: ('N_a_fun$' * 'N_set$') > 'N$').
% 8.79/2.22 tff(func_def_598, type, sK16: ('A_m_vec_bool_fun$' * 'A_m_vec_bool_fun$') > 'A_m_vec$').
% 8.79/2.22 tff(func_def_599, type, sK17: 'A_m_vec_set$' > 'A_m_vec$').
% 8.79/2.22 tff(func_def_600, type, sK18: 'A_m_vec$').
% 8.79/2.22 tff(func_def_601, type, sK19: ('A_n_vec$' * 'A_n_vec$') > 'N$').
% 8.79/2.22 tff(func_def_602, type, sK20: ('M_set$' * 'M_a_fun$' * 'M_a_fun$') > 'M$').
% 8.79/2.22 tff(func_def_603, type, sK21: ('M_set$' * 'M_a_fun$' * 'M_a_fun$') > 'M$').
% 8.79/2.22 tff(func_def_604, type, sK22: ('N_set$' * 'N_a_fun$' * 'N_a_fun$') > 'N$').
% 8.79/2.22 tff(func_def_605, type, sK23: ('N_set$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N$').
% 8.79/2.22 tff(func_def_606, type, sK24: ('N_set$' * 'N_a_fun$' * 'N_a_fun$') > 'N$').
% 8.79/2.22 tff(func_def_607, type, sK25: ('N_set$' * 'N_a_n_vec_fun$' * 'N_a_n_vec_fun$') > 'N$').
% 8.79/2.22 tff(func_def_608, type, sK26: 'N_set$' > 'N$').
% 8.79/2.22 tff(func_def_609, type, sK27: 'N$').
% 8.79/2.22 tff(func_def_610, type, sK28: ('M_set$' * 'M_a_n_vec_fun$') > 'M$').
% 8.79/2.22 tff(func_def_611, type, sK29: ('N_set$' * 'N_a_n_vec_fun$') > 'N$').
% 8.79/2.22 tff(func_def_612, type, sK30: ('M_a_n_vec_fun$' * 'M_set$') > 'M$').
% 8.79/2.22 tff(func_def_613, type, sK31: ('N_a_n_vec_fun$' * 'N_set$') > 'N$').
% 8.79/2.22 tff(f1,axiom,(
% 8.79/2.22 ! [X0 : 'A_m_vec$'] : ('fun_app$'('uua$',X0) <=> ? [X1 : 'M_a_fun$'] : 'sum$'('uu$'(X1),'top$') = X0)),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom0)).
% 8.79/2.22
% 8.79/2.22 tff(f284,conjecture,(
% 8.79/2.22 'thesis$'),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture283)).
% 8.79/2.22
% 8.79/2.22 tff(f285,negated_conjecture,(
% 8.79/2.22 ~ 'thesis$'),
% 8.79/2.22 inference(negated_conjecture,[status(cth)],[f284])).
% 8.79/2.22
% 8.79/2.22 tff(f286,axiom,(
% 8.79/2.22 ! [X0 : 'M_a_fun$'] : ('sum$'('uu$'(X0),'top$') = 'fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$')) => 'thesis$')),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis284)).
% 8.79/2.22
% 8.79/2.22 tff(f289,axiom,(
% 8.79/2.22 'top$b' = 'collect$'('uua$')),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom287)).
% 8.79/2.22
% 8.79/2.22 tff(f321,axiom,(
% 8.79/2.22 ! [X0 : 'A_m_vec$'] : 'member$a'(X0,'top$b')),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom319)).
% 8.79/2.22
% 8.79/2.22 tff(f522,axiom,(
% 8.79/2.22 ! [X0 : 'A_m_vec$',X1 : 'A_m_vec_bool_fun$'] : ('member$a'(X0,'collect$'(X1)) <=> 'fun_app$'(X1,X0))),
% 8.79/2.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom520)).
% 8.79/2.22
% 8.79/2.22 tff(f923,plain,(
% 8.79/2.22 ~'thesis$'),
% 8.79/2.22 inference(flattening,[],[f285])).
% 8.79/2.22
% 8.79/2.22 tff(f933,plain,(
% 8.79/2.22 ! [X0 : 'M_a_fun$'] : ('thesis$' | 'sum$'('uu$'(X0),'top$') != 'fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$')))),
% 8.79/2.22 inference(ennf_transformation,[],[f286])).
% 8.79/2.22
% 8.79/2.22 tff(f976,plain,(
% 8.79/2.22 ! [X0 : 'A_m_vec$'] : (('fun_app$'('uua$',X0) | ! [X1 : 'M_a_fun$'] : 'sum$'('uu$'(X1),'top$') != X0) & (? [X1 : 'M_a_fun$'] : 'sum$'('uu$'(X1),'top$') = X0 | ~'fun_app$'('uua$',X0)))),
% 8.79/2.22 inference(nnf_transformation,[],[f1])).
% 8.79/2.22
% 8.79/2.22 tff(f977,plain,(
% 8.79/2.22 ! [X0 : 'A_m_vec$'] : (('fun_app$'('uua$',X0) | ! [X1 : 'M_a_fun$'] : 'sum$'('uu$'(X1),'top$') != X0) & (? [X2 : 'M_a_fun$'] : 'sum$'('uu$'(X2),'top$') = X0 | ~'fun_app$'('uua$',X0)))),
% 8.79/2.22 inference(rectify,[],[f976])).
% 8.79/2.22
% 8.79/2.22 tff(f978,plain,(
% 8.79/2.22 ! [X0 : 'A_m_vec$'] : (('fun_app$'('uua$',X0) | ! [X1 : 'M_a_fun$'] : 'sum$'('uu$'(X1),'top$') != X0) & ('sum$'('uu$'(sK5(X0)),'top$') = X0 | ~'fun_app$'('uua$',X0)))),
% 8.79/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0))],[f977])).
% 8.79/2.22
% 8.79/2.22 tff(f1009,plain,(
% 8.79/2.22 ! [X0 : 'A_m_vec$',X1 : 'A_m_vec_bool_fun$'] : (('member$a'(X0,'collect$'(X1)) | ~'fun_app$'(X1,X0)) & ('fun_app$'(X1,X0) | ~'member$a'(X0,'collect$'(X1))))),
% 8.79/2.22 inference(nnf_transformation,[],[f522])).
% 8.79/2.22
% 8.79/2.22 tff(f1034,plain,(
% 8.79/2.22 ~'thesis$'),
% 8.79/2.22 inference(cnf_transformation,[],[f923])).
% 8.79/2.22
% 8.79/2.22 tff(f1035,plain,(
% 8.79/2.22 ( ! [X0 : 'M_a_fun$'] : ('thesis$' | 'sum$'('uu$'(X0),'top$') != 'fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$'))) )),
% 8.79/2.22 inference(cnf_transformation,[],[f933])).
% 8.79/2.22
% 8.79/2.22 tff(f1051,plain,(
% 8.79/2.22 ( ! [X0 : 'A_m_vec$'] : ('sum$'('uu$'(sK5(X0)),'top$') = X0 | ~'fun_app$'('uua$',X0)) )),
% 8.79/2.22 inference(cnf_transformation,[],[f978])).
% 8.79/2.22
% 8.79/2.22 tff(f1081,plain,(
% 8.79/2.22 'top$b' = 'collect$'('uua$')),
% 8.79/2.22 inference(cnf_transformation,[],[f289])).
% 8.79/2.22
% 8.79/2.22 tff(f1107,plain,(
% 8.79/2.22 ( ! [X0 : 'A_m_vec$',X1 : 'A_m_vec_bool_fun$'] : ('fun_app$'(X1,X0) | ~'member$a'(X0,'collect$'(X1))) )),
% 8.79/2.22 inference(cnf_transformation,[],[f1009])).
% 8.79/2.22
% 8.79/2.22 tff(f1112,plain,(
% 8.79/2.22 ( ! [X0 : 'A_m_vec$'] : ('member$a'(X0,'top$b')) )),
% 8.79/2.22 inference(cnf_transformation,[],[f321])).
% 8.79/2.22
% 8.79/2.22 tcf(c_49,negated_conjecture,
% 8.79/2.22 (~'thesis$'),
% 8.79/2.22 inference(cnf_transformation,[],[f1034])).
% 8.79/2.22
% 8.79/2.22 tcf(c_50,plain,![X0_'M_a_fun':'M_a_fun$']:
% 8.79/2.22 ('fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$')) != 'sum$'('uu$'(X0_'M_a_fun'),'top$')|
% 8.79/2.22 'thesis$'),
% 8.79/2.22 inference(cnf_transformation,[],[f1035])).
% 8.79/2.22
% 8.79/2.22 tcf(c_64,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 (~'fun_app$'('uua$',X0_'A_m_vec')|'sum$'('uu$'(sK5(X0_'A_m_vec')),'top$') = X0_'A_m_vec'),
% 8.79/2.22 inference(cnf_transformation,[],[f1051])).
% 8.79/2.22
% 8.79/2.22 tcf(c_86,plain,
% 8.79/2.22 ('collect$'('uua$') = 'top$b'),
% 8.79/2.22 inference(cnf_transformation,[],[f1081])).
% 8.79/2.22
% 8.79/2.22 tcf(c_111,plain,![X0_'A_m_vec_bool_fun':'A_m_vec_bool_fun$',X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 (~'member$a'(X0_'A_m_vec','collect$'(X0_'A_m_vec_bool_fun'))|'fun_app$'(X0_'A_m_vec_bool_fun',X0_'A_m_vec')),
% 8.79/2.22 inference(cnf_transformation,[],[f1107])).
% 8.79/2.22
% 8.79/2.22 tcf(c_115,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 ('member$a'(X0_'A_m_vec','top$b')),
% 8.79/2.22 inference(cnf_transformation,[],[f1112])).
% 8.79/2.22
% 8.79/2.22 tcf(c_233,plain,![X0_'M_a_fun':'M_a_fun$']:
% 8.79/2.22 ('fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$')) != 'sum$'('uu$'(X0_'M_a_fun'),'top$')),
% 8.79/2.22 inference(global_subsumption_just,[status(thm)],[c_50,c_49,c_50])).
% 8.79/2.22
% 8.79/2.22 tcf(c_3543,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 (~'member$a'(X0_'A_m_vec','top$b')|'fun_app$'('uua$',X0_'A_m_vec')),
% 8.79/2.22 inference(superposition,[status(thm)],[c_86,c_111])).
% 8.79/2.22
% 8.79/2.22 tcf(c_3544,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 ('fun_app$'('uua$',X0_'A_m_vec')),
% 8.79/2.22 inference(forward_subsumption_resolution,[status(thm)],[c_3543,c_115])).
% 8.79/2.22
% 8.79/2.22 tcf(c_3630,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 ('sum$'('uu$'(sK5(X0_'A_m_vec')),'top$') = X0_'A_m_vec'),
% 8.79/2.22 inference(global_subsumption_just,[status(thm)],[c_64,c_64,c_3544])).
% 8.79/2.22
% 8.79/2.22 tcf(c_3633,plain,![X0_'A_m_vec':'A_m_vec$']:
% 8.79/2.22 ('fun_app$ar'('f$','fun_app$a'('vec_nth$a'('cart_basis_Rn$'),'j$')) != X0_'A_m_vec'),
% 8.79/2.22 inference(superposition,[status(thm)],[c_3630,c_233])).
% 8.79/2.22
% 8.79/2.22 tcf(c_3635,plain,
% 8.79/2.22 ($false),
% 8.79/2.22 inference(equality_resolution,[status(thm)],[c_3633])).
% 8.79/2.22
% 8.79/2.22
% 8.79/2.22 % SZS output end CNFRefutation for theBenchmark.p
% 8.79/2.22
% 8.79/2.22
%------------------------------------------------------------------------------