%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP327_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 : n012.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:26 PM UTC 2026
% Result : Theorem 3.80s 6.09s
% Output : CNFRefutation 3.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP327_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.05/5.32 % Computer : n012.cluster.edu
% 0.05/5.32 % Model : x86_64 x86_64
% 0.05/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.32 % Memory : 8046.5625MB
% 0.05/5.32 % OS : Linux 6.8.0-71-generic
% 0.05/5.32 % CPULimit : 300
% 0.05/5.32 % WCLimit : 300
% 0.05/5.32 % DateTime : Wed Sep 23 18:23:41 UTC 2026
% 0.05/5.32 % CPUTime :
% 0.05/5.32 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.05/5.34 Running first-order theorem proving
% 0.05/5.34 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.05/5.35
% 0.05/5.35 % ======== iProver multi-core TPTP/SMT =========
% 0.05/5.35
% 0.05/5.35 % Detected problem language: tptp
% 0.05/5.36 % Proving...
% 3.80/6.09 % SZS status Started for theBenchmark.p
% 3.80/6.09 % SZS status Theorem for theBenchmark.p
% 3.80/6.09
% 3.80/6.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.80/6.09
% 3.80/6.09 % ------ iProver source info
% 3.80/6.09
% 3.80/6.09 % git: date: 2026-07-19 20:42:38 +0200
% 3.80/6.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.80/6.09 % git: non_committed_changes: false
% 3.80/6.09
% 3.80/6.09 % ------ Parsing...
% 3.80/6.09 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 3.80/6.09 %
% 3.80/6.09
% 3.80/6.09 % ------ Preprocessing...%
% 3.80/6.09
% 3.80/6.09 % SZS status Theorem for theBenchmark.p
% 3.80/6.09
% 3.80/6.09 % SZS output start CNFRefutation for theBenchmark.p
% 3.80/6.09
% 3.80/6.09 tff(func_def_0, type, 'uwc$': ('A_a_m_vec_fun$' * 'A_n_vec_m_vec$' * 'M$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(pred_def_1, type, 'fun_app$p': ('A_bool_fun$' * 'A$') > $o).
% 3.80/6.09 tff(pred_def_2, type, 'fun_app$e': ('A_n_vec_bool_fun$' * 'A_n_vec$') > $o).
% 3.80/6.09 tff(pred_def_3, type, 'dependent$b': ('A_a_m_vec_a_m_vec_fun_fun$' * 'A_m_vec_set$') > $o).
% 3.80/6.09 tff(pred_def_4, type, 'member$a': ('A_m_vec$' * 'A_m_vec_set$') > $o).
% 3.80/6.09 tff(pred_def_5, type, 'reduced_row_echelon_form$': 'A_m_vec_n_vec$' > $o).
% 3.80/6.09 tff(pred_def_6, type, 'member$b': ('A_n_vec_set$' * 'A_n_vec_set_set$') > $o).
% 3.80/6.09 tff(pred_def_7, type, 'member$e': ('A_set$' * 'A_set_set$') > $o).
% 3.80/6.09 tff(pred_def_8, type, 'is_zero_row$': ('N$' * 'A_m_vec_n_vec$') > $o).
% 3.80/6.09 tff(pred_def_9, type, 'less_eq$c': ('A_set$' * 'A_set$') > $o).
% 3.80/6.09 tff(pred_def_10, type, 'fun_app$g': ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > $o).
% 3.80/6.09 tff(pred_def_11, type, 'fun_app$o': ('A_m_vec_bool_fun$' * 'A_m_vec$') > $o).
% 3.80/6.09 tff(pred_def_12, type, 'reduced_row_echelon_form$c': 'A_n_vec_m_vec$' > $o).
% 3.80/6.09 tff(pred_def_13, type, 'less_eq$a': ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > $o).
% 3.80/6.09 tff(pred_def_14, type, 'finite$b': 'A_n_vec_set_set$' > $o).
% 3.80/6.09 tff(pred_def_15, type, 'member$c': ('A$' * 'A_set$') > $o).
% 3.80/6.09 tff(pred_def_16, type, 'reduced_row_echelon_form$a': 'A_n_vec_n_vec_n_vec$' > $o).
% 3.80/6.09 tff(pred_def_17, type, 'reduced_row_echelon_form$b': 'A_n_vec_n_vec_m_vec$' > $o).
% 3.80/6.09 tff(pred_def_18, type, 'reduced_row_echelon_form$e': 'A_n_vec_n_vec$' > $o).
% 3.80/6.09 tff(pred_def_19, type, 'dependent$a': ('A_a_a_fun_fun$' * 'A_set$') > $o).
% 3.80/6.09 tff(pred_def_20, type, 'fun_app$c': ('N_bool_fun$' * 'N$') > $o).
% 3.80/6.09 tff(pred_def_21, type, 'fun_app$': ('M_bool_fun$' * 'M$') > $o).
% 3.80/6.09 tff(pred_def_22, type, 'finite$a': 'A_set$' > $o).
% 3.80/6.09 tff(pred_def_23, type, 'member$d': ('A_m_vec_n_vec$' * 'A_m_vec_n_vec_set$') > $o).
% 3.80/6.09 tff(pred_def_24, type, 'reduced_row_echelon_form$d': 'A_m_vec_m_vec$' > $o).
% 3.80/6.09 tff(pred_def_25, type, sP0: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec$' * 'A_n_vec$') > $o).
% 3.80/6.09 tff(pred_def_26, type, sP1: ('A_n_vec$' * 'A_n_vec$' * 'A_n_vec_set$' * 'A_n_vec_set$') > $o).
% 3.80/6.09 tff(pred_def_27, type, sP2: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > $o).
% 3.80/6.09 tff(func_def_28, type, 'uxs$': ('A_n_vec_set$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_29, type, 'fun_app$l': ('A_set_a_set_fun$' * 'A_set$') > 'A_set$').
% 3.80/6.09 tff(func_def_30, type, 'uvp$': ('N$' * 'A_n_vec_n_vec$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_31, type, 'uvt$': 'N_a_fun$').
% 3.80/6.09 tff(func_def_32, type, 'uvs$': 'M_a_fun$').
% 3.80/6.09 tff(func_def_33, type, 'bot$b': 'A_set$').
% 3.80/6.09 tff(func_def_34, type, 'collect$b': 'A_n_vec_set_bool_fun$' > 'A_n_vec_set_set$').
% 3.80/6.09 tff(func_def_35, type, 'collect$c': 'A_n_vec_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_36, type, 'bot$': 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_37, type, 'column$b': ('N$' * 'A_n_vec_m_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_38, type, 'one$c': 'A_n_vec$').
% 3.80/6.09 tff(func_def_39, type, 'vec_nth$i': ('A_m_vec_n_vec_m_vec$' * 'M$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_40, type, 'minus$c': 'A_n_vec_a_n_vec_a_n_vec_fun_fun$').
% 3.80/6.09 tff(func_def_41, type, 'fun_app$t': ('M_a_m_vec_fun$' * 'M$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_42, type, 'uvo$': ('M$' * 'A_m_vec_m_vec$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_43, type, 'uyd$': 'N_set$' > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_44, type, 'map_matrix$e': ('A_n_vec_a_fun$' * 'A_n_vec_n_vec_m_vec$') > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_45, type, 'zero$e': 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_46, type, 'uwq$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_47, type, 'zero$d': 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_48, type, 'uxm$': ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_49, type, 'times$l': ('A_n_vec_set_set$' * 'A_n_vec_set_set$') > 'A_n_vec_set_set$').
% 3.80/6.09 tff(func_def_50, type, 'uvd$': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_51, type, 'one$h': 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_52, type, 'a$': 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_53, type, 'uwm$': ('A_a_fun$' * 'A_m_vec_n_vec$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_54, type, 'uvl$': ('N$' * 'A_m_vec_n_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_55, type, 'mult_row_row$b': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_56, type, 'minus$e': ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_57, type, 'uwd$': ('A_a_m_vec_fun$' * 'A_n_vec_m_vec$') > 'M_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_58, type, 'map_matrix$g': ('A_n_vec_a_fun$' * 'A_n_vec_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_59, type, 'insert$a': ('N$' * 'N_set$') > 'N_set$').
% 3.80/6.09 tff(func_def_60, type, 'vec_nth$c': 'A_n_vec_n_vec$' > 'N_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_61, type, 'vec_nth$j': ('A_n_vec_n_vec_m_vec$' * 'M$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_62, type, 'uvj$': 'N$' > 'M_bool_fun$').
% 3.80/6.09 tff(func_def_63, type, 'vec_lambda$f': 'M_a_m_vec_n_vec_fun$' > 'A_m_vec_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_64, type, 'vec_lambda$e': 'N_a_n_vec_fun$' > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_65, type, 'uuf$': 'A_n_vec_a_n_vec_bool_fun_fun$').
% 3.80/6.09 tff(func_def_66, type, 'less_eq$': 'A_n_vec_set$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_67, type, 'uvv$': ('A_n_vec_m_vec$' * 'N$' * 'A$' * 'M$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_68, type, 'times$h': ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_69, type, 'bot$c': 'A_m_vec_set$').
% 3.80/6.09 tff(func_def_70, type, 'row$c': ('N$' * 'A_n_vec_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_71, type, 'uwg$': ('A_a_fun$' * 'A_m_vec_m_vec$' * 'M$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_72, type, 'insert$': 'A_n_vec$' > 'A_n_vec_set_a_n_vec_set_fun$').
% 3.80/6.09 tff(func_def_73, type, 'the$': 'N_bool_fun$' > 'N$').
% 3.80/6.09 tff(func_def_74, type, 'times$a': 'A_n_vec_a_n_vec_a_n_vec_fun_fun$').
% 3.80/6.09 tff(func_def_75, type, 'i$': 'N$').
% 3.80/6.09 tff(func_def_76, type, 'vec_lambda$': 'M_a_fun$' > 'A_m_vec$').
% 3.80/6.09 tff(func_def_77, type, 'uxf$': 'A_m_vec_n_vec$' > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_78, type, 'fun_app$j': ('A_n_vec_a_n_vec_a_n_vec_fun_fun$' * 'A_n_vec$') > 'A_n_vec_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_79, type, 'vec_nth$h': ('A_n_vec_m_vec_n_vec$' * 'N$') > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_80, type, 'minus$b': 'A_n_vec_set$' > 'A_n_vec_set_a_n_vec_set_fun$').
% 3.80/6.09 tff(func_def_81, type, 'uuh$': 'A_n_vec_a_n_vec_bool_fun_fun$').
% 3.80/6.09 tff(func_def_82, type, 'finite$': 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_83, type, 'vec_nth$e': 'A_m_vec_m_vec$' > 'M_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_84, type, 'vec_lambda$c': 'M_a_m_vec_fun$' > 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_85, type, 'uub$': 'A_m_vec_n_vec_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_86, type, 'vec_lambda$b': 'N_a_m_vec_fun$' > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_87, type, 'map_matrix$i': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_88, type, 'collect$': 'A_bool_fun$' > 'A_set$').
% 3.80/6.09 tff(func_def_89, type, 'y$': 'N$').
% 3.80/6.09 tff(func_def_90, type, 'fun_app$r': ('N_a_n_vec_fun$' * 'N$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_91, type, 'vec_nth$b': 'A_n_vec$' > 'N_a_fun$').
% 3.80/6.09 tff(func_def_92, type, 'uul$': 'A_n_vec_set_set$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_93, type, 'uxe$': ('A_m_vec_n_vec$' * 'N$') > 'M_bool_fun$').
% 3.80/6.09 tff(func_def_94, type, 'one$': 'A$').
% 3.80/6.09 tff(func_def_95, type, 'least$a': 'N_bool_fun$' > 'N$').
% 3.80/6.09 tff(func_def_96, type, 'mult_column_row$': ('A_n_vec_m_vec$' * 'N$' * 'A$') > 'M_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_97, type, 'times$f': ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_98, type, 'uut$': (tlbool * 'A_n_vec$') > 'A_n_vec_a_n_vec_bool_fun_fun$').
% 3.80/6.09 tff(func_def_99, type, 'fun_app$ac': ('N_a_n_vec_bool_fun_fun$' * 'N$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_100, type, 'row$b': ('M$' * 'A_n_vec_m_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_101, type, 'uxy$': ('A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_102, type, 'one$e': 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_103, type, 'times$e': 'A_a_a_fun_fun$').
% 3.80/6.09 tff(func_def_104, type, 'vec_nth$': 'A_m_vec$' > 'M_a_fun$').
% 3.80/6.09 tff(func_def_105, type, 'times$g': ('A_n_vec_m_vec$' * 'A_n_vec_m_vec$') > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_106, type, 'uyk$': ('A_n_vec_a_fun$' * 'A_n_vec_set$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_107, type, 'uws$': 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_108, type, 'vec_nth$a': 'A_m_vec_n_vec$' > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_109, type, 'uux$': 'A_m_vec_n_vec$' > 'A_m_vec_n_vec_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_110, type, 'uxt$': ('A_n_vec_set$' * 'A_n_vec_a_n_vec_bool_fun_fun$') > 'A_n_vec_a_n_vec_bool_fun_fun$').
% 3.80/6.09 tff(func_def_111, type, 'fun_app$h': ('A_m_vec_n_vec_a_m_vec_n_vec_fun$' * 'A_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_112, type, 'uxi$': ('A_m_vec_n_vec$' * 'M$' * 'M$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_113, type, 'fun_app$s': ('M_a_n_vec_fun$' * 'M$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_114, type, tltrue: tlbool).
% 3.80/6.09 tff(func_def_115, type, 'vector_scalar_mult$a': 'A_a_m_vec_a_m_vec_fun_fun$').
% 3.80/6.09 tff(func_def_116, type, 'uuu$': (tlbool * 'N$' * 'N$') > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_117, type, 'uvg$': ('A_n_vec$' * 'A_n_vec$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_118, type, 'uwr$': ('A_n_vec_a_fun$' * 'A_n_vec_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_119, type, 'map_matrix$h': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_120, type, 'uxg$': ('A_m_vec_n_vec$' * 'M$' * 'A$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_121, type, 'uwb$': ('A_m_vec_n_vec$' * 'N$' * 'A$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_122, type, 'uvn$': ('N$' * 'A_n_vec_m_vec$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_123, type, 'uxl$': ('A_m_vec_n_vec$' * 'A_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_124, type, 'uus$': 'A_a_fun$').
% 3.80/6.09 tff(func_def_125, type, 'bot$d': 'A_n_vec_set_set$').
% 3.80/6.09 tff(func_def_126, type, 'uwt$': 'N_a_fun$').
% 3.80/6.09 tff(func_def_127, type, 'zero$c': 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_128, type, 'uyj$': ('A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_129, type, 'uyh$': ('A$' * 'A_n_vec$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_130, type, 'map_matrix$j': ('A_a_m_vec_fun$' * 'A_n_vec_m_vec$') > 'A_m_vec_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_131, type, 'uxz$': ('A_n_vec$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_132, type, 'one$b': 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_133, type, 'uxo$': 'A_n_vec_set$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_134, type, 'collect$a': 'A_m_vec_bool_fun$' > 'A_m_vec_set$').
% 3.80/6.09 tff(func_def_135, type, 'map_matrix$': ('A_a_fun$' * 'A_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_136, type, 'column$a': ('M$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_137, type, 'less$b': 'A_n_vec_set$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_138, type, 'map_matrix$f': ('A_m_vec_a_fun$' * 'A_m_vec_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_139, type, 'uua$': 'N_bool_fun$').
% 3.80/6.09 tff(func_def_140, type, 'dependent$': 'A_a_n_vec_a_n_vec_fun_fun$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_141, type, 'uwv$': ('A_m_vec_n_vec$' * 'M$' * 'M$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_142, type, 'uvk$': 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_143, type, 'fun_app$f': ('A_n_vec_set_a_n_vec_set_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_144, type, 'uxp$': ('A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_bool_fun_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_145, type, 'times$d': 'A_set$' > 'A_set_a_set_fun$').
% 3.80/6.09 tff(func_def_146, type, 'the_elem$a': 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_147, type, 'least$b': 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_148, type, 'zero$f': 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_149, type, 'uu$': 'N_bool_fun$').
% 3.80/6.09 tff(func_def_150, type, 'fun_app$ad': ('N_a_bool_fun_fun$' * 'N$') > 'A_bool_fun$').
% 3.80/6.09 tff(func_def_151, type, 'column$': ('M$' * 'A_m_vec_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_152, type, 'map_matrix$k': ('A_a_m_vec_fun$' * 'A_n_vec_n_vec$') > 'A_m_vec_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_153, type, 'uvr$': 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_154, type, 'uye$': 'A_n_vec_set$' > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_155, type, 'uyl$': ('A_n_vec_a_m_vec_fun$' * 'A_n_vec_set$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_156, type, 'uwn$': ('A_a_fun$' * 'A_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_157, type, 'uwf$': ('A_a_m_vec_fun$' * 'A_n_vec_n_vec$') > 'N_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_158, type, 'uug$': 'N$' > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_159, type, 'one$f': 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_160, type, 'mult_column_row$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_161, type, 'uwi$': ('A_a_fun$' * 'A_n_vec_m_vec$' * 'M$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_162, type, 'uwy$': ('A_n_vec_n_vec$' * 'N$') > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_163, type, 'fun_app$m': ('A_a_fun$' * 'A$') > 'A$').
% 3.80/6.09 tff(func_def_164, type, 'fun_app$u': ('A_n_vec_a_m_vec_fun$' * 'A_n_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_165, type, 'mult_column$': ('A_m_vec_n_vec$' * 'M$' * 'A$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_166, type, 'zero$k': 'M$').
% 3.80/6.09 tff(func_def_167, type, 'uwz$': 'A_n_vec_n_vec$' > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_168, type, 'fun_app$w': ('N_a_m_vec_n_vec_fun$' * 'N$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_169, type, 'uwh$': ('A_a_fun$' * 'A_m_vec_m_vec$') > 'M_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_170, type, 'uxk$': ('A_m_vec$' * 'A_m_vec$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_171, type, 'bot$a': 'N_set$').
% 3.80/6.09 tff(func_def_172, type, 'zero$j': 'N$').
% 3.80/6.09 tff(func_def_173, type, 'mult_row$': ('A_m_vec_n_vec$' * 'N$' * 'A$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_174, type, 'less_eq$b': 'M$' > 'M_bool_fun$').
% 3.80/6.09 tff(func_def_175, type, 'xa$': 'A_n_vec$').
% 3.80/6.09 tff(func_def_176, type, 'mult_column_row$c': ('A_m_vec_n_vec$' * 'M$' * 'A$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_177, type, 'uwu$': 'M_a_fun$').
% 3.80/6.09 tff(func_def_178, type, 'uvw$': ('A_n_vec_n_vec$' * 'N$' * 'A$' * 'N$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_179, type, 'uwp$': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_180, type, 'fun_app$af': ('N_a_m_vec_bool_fun_fun$' * 'N$') > 'A_m_vec_bool_fun$').
% 3.80/6.09 tff(func_def_181, type, 'uya$': ('A_n_vec$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_182, type, 'fun_app$ag': ('A_a_n_vec_a_n_vec_fun_fun$' * 'A$') > 'A_n_vec_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_183, type, 'uuy$': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_184, type, 'fun_app$v': ('A_n_vec_a_fun$' * 'A_n_vec$') > 'A$').
% 3.80/6.09 tff(func_def_185, type, 'vector_scalar_mult$': 'A_a_n_vec_a_n_vec_fun_fun$').
% 3.80/6.09 tff(func_def_186, type, 'fun_app$q': ('A_n_vec_a_n_vec_bool_fun_fun$' * 'A_n_vec$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_187, type, 'uwk$': ('A_a_fun$' * 'A_n_vec_n_vec$' * 'N$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_188, type, 'uwl$': ('A_a_fun$' * 'A_n_vec_n_vec$') > 'N_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_189, type, 'uvq$': ('M$' * 'A_m_vec_n_vec$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_190, type, 'times$': 'A_m_vec_n_vec$' > 'A_m_vec_n_vec_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_191, type, 'uvx$': ('A_m_vec_n_vec$' * 'M$' * 'A$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_192, type, 'uur$': 'A_n_vec_set_a_n_vec_set_fun$').
% 3.80/6.09 tff(func_def_193, type, 'fun_app$z': ('A_a_m_vec_fun$' * 'A$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_194, type, 'fun_app$ab': ('M_a_n_vec_bool_fun_fun$' * 'M$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_195, type, 'column$f': ('N$' * 'A_n_vec_n_vec_n_vec$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_196, type, 'interchange_columns$': ('A_m_vec_n_vec$' * 'M$' * 'M$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_197, type, 'columns$': 'A_m_vec_n_vec$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_198, type, 'uxq$': 'A_n_vec_a_n_vec_bool_fun_fun$' > 'A_n_vec_a_n_vec_bool_fun_fun$').
% 3.80/6.09 tff(func_def_199, type, 'uwe$': ('A_a_m_vec_fun$' * 'A_n_vec_n_vec$' * 'N$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_200, type, 'fun_app$a': ('M_a_fun$' * 'M$') > 'A$').
% 3.80/6.09 tff(func_def_201, type, 'mult_row_row$c': ('A_m_vec_n_vec$' * 'N$' * 'A$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_202, type, 'minus$d': ('A_m_vec_n_vec$' * 'A_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_203, type, 'mult_row_row$a': ('A_n_vec_n_vec$' * 'N$' * 'A$') > 'N_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_204, type, 'is_singleton$': 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_205, type, 'uww$': ('A_m_vec_n_vec$' * 'N$' * 'N$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_206, type, 'uxd$': 'A_m_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 3.80/6.09 tff(func_def_207, type, 'column$d': ('N$' * 'A_m_vec_n_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_208, type, 'vec_nth$k': ('A_n_vec_n_vec_n_vec$' * 'N$') > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_209, type, 'uvi$': ('A_m_vec_n_vec$' * 'A_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_210, type, 'b$': 'N$').
% 3.80/6.09 tff(func_def_211, type, 'interchange_rows$': ('A_m_vec_n_vec$' * 'N$' * 'N$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_212, type, 'map_matrix$a': ('A_a_fun$' * 'A_n_vec_m_vec$') > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_213, type, 'uxj$': ('A_n_vec$' * 'A_n_vec$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_214, type, 'zero$h': 'A_m_vec_set$').
% 3.80/6.09 tff(func_def_215, type, 'zero$': 'A$').
% 3.80/6.09 tff(func_def_216, type, 'zero$g': 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_217, type, 'column$e': ('M$' * 'A_m_vec_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_218, type, 'col_space$': 'A_m_vec_n_vec$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_219, type, 'column$c': ('N$' * 'A_n_vec_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_220, type, tlfalse: tlbool).
% 3.80/6.09 tff(func_def_221, type, 'uve$': ('A_n_vec_m_vec$' * 'A_n_vec_m_vec$') > 'M_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_222, type, 'uuc$': 'A_n_vec_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_223, type, 'uun$': 'A_m_vec_n_vec_a_m_vec_n_vec_fun$').
% 3.80/6.09 tff(func_def_224, type, 'fun_app$d': ('N_a_fun$' * 'N$') > 'A$').
% 3.80/6.09 tff(func_def_225, type, 'one$a': 'A_m_vec$').
% 3.80/6.09 tff(func_def_226, type, 'uyc$': ('A_n_vec_set$' * 'A_n_vec_a_fun$' * 'A_n_vec_a_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_227, type, 'times$b': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_228, type, 'minus$': 'A_m_vec$' > 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_229, type, 'zero$i': 'A_set$').
% 3.80/6.09 tff(func_def_230, type, 'vec_lambda$g': 'N_a_m_vec_n_vec_fun$' > 'A_m_vec_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_231, type, 'uwx$': 'A_m_vec_n_vec$' > 'A_m_vec_bool_fun$').
% 3.80/6.09 tff(func_def_232, type, 'minus$a': 'A$' > 'A_a_fun$').
% 3.80/6.09 tff(func_def_233, type, 'uxx$': ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_a_n_vec_fun_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_234, type, 'uuo$': 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_235, type, 'fun_app$b': ('N_a_m_vec_fun$' * 'N$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_236, type, 'x$': 'A_n_vec$').
% 3.80/6.09 tff(func_def_237, type, 'uxw$': ('A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_238, type, 'times$j': ('A_m_vec_set$' * 'A_m_vec_set$') > 'A_m_vec_set$').
% 3.80/6.09 tff(func_def_239, type, 'insert$b': ('A$' * 'A_set$') > 'A_set$').
% 3.80/6.09 tff(func_def_240, type, 'uyb$': ('A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_241, type, 'uui$': 'N$' > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_242, type, 'row$': ('N$' * 'A_m_vec_n_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_243, type, 'row$a': ('M$' * 'A_m_vec_m_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_244, type, 'uvb$': 'A_n_vec_set$' > 'A_n_vec_set_a_n_vec_set_fun$').
% 3.80/6.09 tff(func_def_245, type, 'less$a': 'M$' > 'M_bool_fun$').
% 3.80/6.09 tff(func_def_246, type, 'map_matrix$d': ('A_m_vec_a_fun$' * 'A_m_vec_n_vec_m_vec$') > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_247, type, 'fun_app$i': ('A_n_vec_a_n_vec_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_248, type, 'sum$': ('A_n_vec_a_fun$' * 'A_n_vec_set$') > 'A$').
% 3.80/6.09 tff(func_def_249, type, 'uvu$': ('A_m_vec_m_vec$' * 'M$' * 'A$' * 'M$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_250, type, 'uwo$': ('A_m_vec_a_fun$' * 'A_m_vec_m_vec_n_vec$' * 'N$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_251, type, 'the_elem$': 'N_set$' > 'N$').
% 3.80/6.09 tff(func_def_252, type, 'uym$': ('A_m_vec_n_vec$' * 'N$' * 'N$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_253, type, 'insert$c': ('A_m_vec$' * 'A_m_vec_set$') > 'A_m_vec_set$').
% 3.80/6.09 tff(func_def_254, type, 'v$': 'A_n_vec$').
% 3.80/6.09 tff(func_def_255, type, 'vec_nth$f': ('A_m_vec_n_vec_n_vec$' * 'N$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_256, type, 'member$': 'A_n_vec$' > 'A_n_vec_set_bool_fun$').
% 3.80/6.09 tff(func_def_257, type, 'uvc$': 'A$' > 'A_a_fun$').
% 3.80/6.09 tff(func_def_258, type, 'uva$': 'A_set$' > 'A_set_a_set_fun$').
% 3.80/6.09 tff(func_def_259, type, 'vec_lambda$d': 'M_a_n_vec_fun$' > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_260, type, 'fun_app$aa': ('M_a_m_vec_bool_fun_fun$' * 'M$') > 'A_m_vec_bool_fun$').
% 3.80/6.09 tff(func_def_261, type, 'mult_column_row$b': ('A_m_vec_m_vec$' * 'M$' * 'A$') > 'M_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_262, type, 'uxa$': ('A_n_vec_m_vec$' * 'M$') > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_263, type, 'uyf$': ('A$' * 'A_m_vec$') > 'M_a_fun$').
% 3.80/6.09 tff(func_def_264, type, 'sum$a': ('A_n_vec_a_m_vec_fun$' * 'A_n_vec_set$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_265, type, 'uxh$': ('A_m_vec_n_vec$' * 'N$' * 'A$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_266, type, 'uxb$': 'A_n_vec_m_vec$' > 'A_m_vec_bool_fun$').
% 3.80/6.09 tff(func_def_267, type, 'uwj$': ('A_a_fun$' * 'A_n_vec_m_vec$') > 'M_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_268, type, 'the$a': 'A_n_vec_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_269, type, 'uyg$': ('A_m_vec$' * 'A_m_vec_n_vec$') > 'N_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_270, type, 'times$c': 'A_n_vec_set$' > 'A_n_vec_set_a_n_vec_set_fun$').
% 3.80/6.09 tff(func_def_271, type, 'fun_app$k': ('A_m_vec_a_m_vec_fun$' * 'A_m_vec$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_272, type, 'one$g': 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_273, type, 'uvz$': ('A_n_vec_m_vec$' * 'M$' * 'A$' * 'M$') > 'N_a_fun$').
% 3.80/6.09 tff(func_def_274, type, 'uud$': 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_275, type, 'uxn$': ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_276, type, 'uuz$': 'A_n_vec_a_n_vec_a_n_vec_fun_fun$').
% 3.80/6.09 tff(func_def_277, type, 'vec_nth$g': ('A_m_vec_m_vec_n_vec$' * 'N$') > 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_278, type, 'fun_app$ah': ('A_a_m_vec_a_m_vec_fun_fun$' * 'A$') > 'A_m_vec_a_m_vec_fun$').
% 3.80/6.09 tff(func_def_279, type, 'less$': 'N$' > 'N_bool_fun$').
% 3.80/6.09 tff(func_def_280, type, 'vec_lambda$a': 'N_a_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_281, type, 'uuj$': 'A_set$' > 'A_bool_fun$').
% 3.80/6.09 tff(func_def_282, type, 'mult_row_row$': ('A_n_vec_m_vec$' * 'M$' * 'A$') > 'M_a_n_vec_fun$').
% 3.80/6.09 tff(func_def_283, type, 'uyi$': ('A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec_bool_fun$').
% 3.80/6.09 tff(func_def_284, type, 'uuv$': 'M_bool_fun$').
% 3.80/6.09 tff(func_def_285, type, 'uuq$': 'A_set_a_set_fun$').
% 3.80/6.09 tff(func_def_286, type, 'vector_scalar_mult$b': ('A_m_vec$' * 'A_m_vec_n_vec$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_287, type, 'fun_app$x': ('M_a_m_vec_n_vec_fun$' * 'M$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_288, type, 'fun_app$ae': ('M_a_bool_fun_fun$' * 'M$') > 'A_bool_fun$').
% 3.80/6.09 tff(func_def_289, type, 'times$i': ('A_m_vec_n_vec_set$' * 'A_m_vec_n_vec_set$') > 'A_m_vec_n_vec_set$').
% 3.80/6.09 tff(func_def_290, type, 'zero$a': 'A_m_vec$').
% 3.80/6.09 tff(func_def_291, type, sK3: 'A_n_vec$' > 'N$').
% 3.80/6.09 tff(func_def_292, type, sK4: ('A_m_vec_n_vec$' * 'A_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_293, type, sK5: ('A_m_vec_m_vec$' * 'A_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_294, type, sK6: ('A_n_vec_m_vec$' * 'A_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_295, type, sK7: ('A_n_vec_n_vec$' * 'A_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_296, type, sK8: ('A_m_vec_n_vec$' * 'A_m_vec$') > 'N$').
% 3.80/6.09 tff(func_def_297, type, sK9: ('A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_298, type, sK10: ('A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_bool_fun_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_299, type, sK11: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_a_n_vec_fun_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_300, type, sK12: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_a_n_vec_fun_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_301, type, sK13: ('A_m_vec_m_vec$' * 'A_m_vec_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_302, type, sK14: ('A_n_vec_m_vec$' * 'A_n_vec_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_303, type, sK15: ('A_n_vec_n_vec$' * 'A_n_vec_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_304, type, sK16: ('A_n_vec$' * 'A_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_305, type, sK17: ('A_m_vec$' * 'A_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_306, type, sK18: ('A_m_vec_n_vec$' * 'A_m_vec_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_307, type, sK19: ('M_a_m_vec_bool_fun_fun$' * 'M$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_308, type, sK20: ('M_a_m_vec_bool_fun_fun$' * 'A_m_vec_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_309, type, sK21: 'M_a_m_vec_bool_fun_fun$' > 'A_m_vec_m_vec$').
% 3.80/6.09 tff(func_def_310, type, sK22: 'M_a_m_vec_bool_fun_fun$' > 'M$').
% 3.80/6.09 tff(func_def_311, type, sK23: ('M_a_n_vec_bool_fun_fun$' * 'M$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_312, type, sK24: ('M_a_n_vec_bool_fun_fun$' * 'A_n_vec_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_313, type, sK25: 'M_a_n_vec_bool_fun_fun$' > 'A_n_vec_m_vec$').
% 3.80/6.09 tff(func_def_314, type, sK26: 'M_a_n_vec_bool_fun_fun$' > 'M$').
% 3.80/6.09 tff(func_def_315, type, sK27: ('N_a_n_vec_bool_fun_fun$' * 'N$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_316, type, sK28: ('N_a_n_vec_bool_fun_fun$' * 'A_n_vec_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_317, type, sK29: 'N_a_n_vec_bool_fun_fun$' > 'A_n_vec_n_vec$').
% 3.80/6.09 tff(func_def_318, type, sK30: 'N_a_n_vec_bool_fun_fun$' > 'N$').
% 3.80/6.09 tff(func_def_319, type, sK31: ('N_a_bool_fun_fun$' * 'N$') > 'A$').
% 3.80/6.09 tff(func_def_320, type, sK32: ('N_a_bool_fun_fun$' * 'A_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_321, type, sK33: 'N_a_bool_fun_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_322, type, sK34: 'N_a_bool_fun_fun$' > 'N$').
% 3.80/6.09 tff(func_def_323, type, sK35: ('M_a_bool_fun_fun$' * 'M$') > 'A$').
% 3.80/6.09 tff(func_def_324, type, sK36: ('M_a_bool_fun_fun$' * 'A_m_vec$') > 'M$').
% 3.80/6.09 tff(func_def_325, type, sK37: 'M_a_bool_fun_fun$' > 'A_m_vec$').
% 3.80/6.09 tff(func_def_326, type, sK38: 'M_a_bool_fun_fun$' > 'M$').
% 3.80/6.09 tff(func_def_327, type, sK39: ('N_a_m_vec_bool_fun_fun$' * 'N$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_328, type, sK40: ('N_a_m_vec_bool_fun_fun$' * 'A_m_vec_n_vec$') > 'N$').
% 3.80/6.09 tff(func_def_329, type, sK41: 'N_a_m_vec_bool_fun_fun$' > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_330, type, sK42: 'N_a_m_vec_bool_fun_fun$' > 'N$').
% 3.80/6.09 tff(func_def_331, type, sK43: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_332, type, sK44: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_333, type, sK45: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_334, type, sK46: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_335, type, sK47: ('A_m_vec_bool_fun$' * 'A_m_vec_bool_fun$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_336, type, sK48: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_337, type, sK49: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_338, type, sK50: ('A_m_vec_n_vec$' * 'A_m_vec_n_vec_set$' * 'A_m_vec_n_vec_set$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_339, type, sK51: ('A_m_vec_n_vec$' * 'A_m_vec_n_vec_set$' * 'A_m_vec_n_vec_set$') > 'A_m_vec_n_vec$').
% 3.80/6.09 tff(func_def_340, type, sK52: ('A_m_vec$' * 'A_m_vec_set$' * 'A_m_vec_set$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_341, type, sK53: ('A_m_vec$' * 'A_m_vec_set$' * 'A_m_vec_set$') > 'A_m_vec$').
% 3.80/6.09 tff(func_def_342, type, sK54: ('A_set$' * 'A_set_set$' * 'A_set_set$') > 'A_set$').
% 3.80/6.09 tff(func_def_343, type, sK55: ('A_set$' * 'A_set_set$' * 'A_set_set$') > 'A_set$').
% 3.80/6.09 tff(func_def_344, type, sK56: ('A_n_vec_set$' * 'A_n_vec_set_set$' * 'A_n_vec_set_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_345, type, sK57: ('A_n_vec_set$' * 'A_n_vec_set_set$' * 'A_n_vec_set_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_346, type, sK58: ('A_n_vec$' * 'A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_347, type, sK59: ('A_n_vec$' * 'A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_348, type, sK60: ('A$' * 'A_set$' * 'A_set$') > 'A$').
% 3.80/6.09 tff(func_def_349, type, sK61: ('A$' * 'A_set$' * 'A_set$') > 'A$').
% 3.80/6.09 tff(func_def_350, type, sK62: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_351, type, sK63: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_352, type, sK64: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_353, type, sK65: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_354, type, sK66: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_355, type, sK67: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_356, type, sK68: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_357, type, sK69: ('N_bool_fun$' * 'N_bool_fun$') > 'N$').
% 3.80/6.09 tff(func_def_358, type, sK70: ('A_n_vec_bool_fun$' * 'A_n_vec$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_359, type, sK71: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_360, type, sK72: ('N_bool_fun$' * 'N$') > 'N$').
% 3.80/6.09 tff(func_def_361, type, sK73: ('N_bool_fun$' * 'N_bool_fun$') > 'N$').
% 3.80/6.09 tff(func_def_362, type, sK74: 'N$').
% 3.80/6.09 tff(func_def_363, type, sK75: 'N$').
% 3.80/6.09 tff(func_def_364, type, sK76: 'A_n_vec$').
% 3.80/6.09 tff(func_def_365, type, sK77: ('A_m_vec_m_vec$' * 'M_a_m_vec_fun$') > 'M$').
% 3.80/6.09 tff(func_def_366, type, sK78: ('A_n_vec_m_vec$' * 'M_a_n_vec_fun$') > 'M$').
% 3.80/6.09 tff(func_def_367, type, sK79: ('A_n_vec_n_vec$' * 'N_a_n_vec_fun$') > 'N$').
% 3.80/6.09 tff(func_def_368, type, sK80: ('A_n_vec$' * 'N_a_fun$') > 'N$').
% 3.80/6.09 tff(func_def_369, type, sK81: ('A_m_vec$' * 'M_a_fun$') > 'M$').
% 3.80/6.09 tff(func_def_370, type, sK82: ('A_m_vec_n_vec$' * 'N_a_m_vec_fun$') > 'N$').
% 3.80/6.09 tff(func_def_371, type, sK83: 'A_n_vec$').
% 3.80/6.09 tff(func_def_372, type, sK84: 'A_n_vec_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_373, type, sK85: 'A_n_vec_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_374, type, sK86: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_375, type, sK87: ('A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_376, type, sK88: ('A_n_vec_bool_fun$' * 'A_n_vec_a_n_vec_bool_fun_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_377, type, sK89: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_378, type, sK90: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_379, type, sK91: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_380, type, sK92: ('A_n_vec_bool_fun$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_381, type, sK93: ('A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_382, type, sK94: ('A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_383, type, sK95: ('A_n_vec$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_384, type, sK96: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec$' * 'A_n_vec$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_385, type, sK97: ('A_n_vec$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_386, type, sK98: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_n_vec_bool_fun_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_387, type, sK99: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_n_vec_bool_fun_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_388, type, sK100: 'A_n_vec_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_389, type, sK101: ('A_n_vec_set_set$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_390, type, sK102: ('A_n_vec_set_set$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_391, type, sK103: 'A_n_vec_set_set$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_392, type, sK104: 'A_n_vec_set_set$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_393, type, sK105: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_394, type, sK106: 'A_n_vec_set_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_395, type, sK107: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_396, type, sK108: 'A_n_vec_set_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_397, type, sK109: 'A_n_vec_set_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_398, type, sK110: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_399, type, sK111: 'A_n_vec_set_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_400, type, sK112: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_401, type, sK113: 'A_n_vec_set$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_402, type, sK114: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_403, type, sK115: 'A_n_vec_set$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_404, type, sK116: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_405, type, sK117: ('A_n_vec_set$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_406, type, sK118: ('A_n_vec_set$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_407, type, sK119: ('A_n_vec_set$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_408, type, sK120: ('A_n_vec_set$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_409, type, sK121: 'A_n_vec_set_bool_fun$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_410, type, sK122: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_411, type, sK123: 'A_n_vec_set_bool_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_412, type, sK124: ('A_n_vec_set$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_413, type, sK125: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_414, type, sK126: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_415, type, sK127: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_416, type, sK128: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_417, type, sK129: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_418, type, sK130: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_419, type, sK131: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_420, type, sK132: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_421, type, sK133: 'A_n_vec_set_a_n_vec_set_fun$' > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_422, type, sK134: ('M_bool_fun$' * 'M_bool_fun$') > 'M$').
% 3.80/6.09 tff(func_def_423, type, sK135: ('M_bool_fun$' * 'M_bool_fun$') > 'M$').
% 3.80/6.09 tff(func_def_424, type, sK136: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_425, type, sK137: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_426, type, sK138: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_427, type, sK139: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_428, type, sK140: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_429, type, sK141: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_430, type, sK142: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_431, type, sK143: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_432, type, sK144: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_433, type, sK145: ('M_bool_fun$' * 'M_bool_fun$') > 'M$').
% 3.80/6.09 tff(func_def_434, type, sK146: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_435, type, sK147: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set_bool_fun$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_436, type, sK148: ('M_bool_fun$' * 'M$') > 'M$').
% 3.80/6.09 tff(func_def_437, type, sK149: ('A_n_vec_set_bool_fun$' * 'A_n_vec_set$') > 'A_n_vec_set$').
% 3.80/6.09 tff(func_def_438, type, sK150: ('M_bool_fun$' * 'M_bool_fun$') > 'M$').
% 3.80/6.09 tff(func_def_439, type, sK151: ('M_bool_fun$' * 'M_bool_fun$') > 'M$').
% 3.80/6.09 tff(func_def_440, type, sK152: ('N$' * 'A_m_vec_n_vec$') > 'M$').
% 3.80/6.09 tff(func_def_441, type, sK153: ('A_n_vec_set$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_442, type, sK154: ('A_n_vec$' * 'A_n_vec_set$' * 'A_n_vec_bool_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_443, type, sK155: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_444, type, sK156: ('A_n_vec_set$' * 'A_n_vec_a_fun$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_445, type, sK157: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_446, type, sK158: ('A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_447, type, sK159: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_448, type, sK160: ('A_n_vec_set$' * 'A_n_vec_a_fun$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_449, type, sK161: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_450, type, sK162: ('A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_451, type, sK163: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_452, type, sK164: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_453, type, sK165: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_454, type, sK166: ('A_n_vec_set$' * 'A_n_vec_set$' * 'A_n_vec_a_m_vec_fun$') > 'A_n_vec$').
% 3.80/6.09 tff(func_def_455, type, sK167: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_456, type, sK168: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_457, type, sK169: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_458, type, sK170: 'A_n_vec_set$' > 'A_n_vec$').
% 3.80/6.09 tff(func_def_459, type, sK171: ('A_n_vec_set$' * 'A_n_vec_set$') > 'A_n_vec$').
% 3.80/6.09 tff(f119,conjecture,(
% 3.80/6.09 'fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'fun_app$d'('vec_nth$b'('xa$'),'i$')) = 'zero$'),
% 3.80/6.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture118)).
% 3.80/6.09
% 3.80/6.09 tff(f120,negated_conjecture,(
% 3.80/6.09 ~ 'fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'fun_app$d'('vec_nth$b'('xa$'),'i$')) = 'zero$'),
% 3.80/6.09 inference(negated_conjecture,[status(cth)],[f119])).
% 3.80/6.09
% 3.80/6.09 tff(f121,axiom,(
% 3.80/6.09 'fun_app$d'('vec_nth$b'('xa$'),'i$') = 'zero$'),
% 3.80/6.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom119)).
% 3.80/6.09
% 3.80/6.09 tff(f144,axiom,(
% 3.80/6.09 ! [X0 : 'A$'] : 'fun_app$m'('fun_app$n'('times$e',X0),'zero$') = 'zero$'),
% 3.80/6.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom142)).
% 3.80/6.09
% 3.80/6.09 tff(f763,plain,(
% 3.80/6.09 'zero$' != 'fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'fun_app$d'('vec_nth$b'('xa$'),'i$'))),
% 3.80/6.09 inference(flattening,[],[f120])).
% 3.80/6.09
% 3.80/6.09 tff(f1768,plain,(
% 3.80/6.09 'zero$' != 'fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'fun_app$d'('vec_nth$b'('xa$'),'i$'))),
% 3.80/6.09 inference(cnf_transformation,[],[f763])).
% 3.80/6.09
% 3.80/6.09 tff(f1769,plain,(
% 3.80/6.09 'zero$' = 'fun_app$d'('vec_nth$b'('xa$'),'i$')),
% 3.80/6.09 inference(cnf_transformation,[],[f121])).
% 3.80/6.09
% 3.80/6.09 tff(f1792,plain,(
% 3.80/6.09 ( ! [X0 : 'A$'] : ('zero$' = 'fun_app$m'('fun_app$n'('times$e',X0),'zero$')) )),
% 3.80/6.09 inference(cnf_transformation,[],[f144])).
% 3.80/6.09
% 3.80/6.09 tcf(c_257,negated_conjecture,
% 3.80/6.09 ('fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'fun_app$d'('vec_nth$b'('xa$'),'i$')) != 'zero$'),
% 3.80/6.09 inference(cnf_transformation,[],[f1768])).
% 3.80/6.09
% 3.80/6.09 tcf(c_258,plain,
% 3.80/6.09 ('fun_app$d'('vec_nth$b'('xa$'),'i$') = 'zero$'),
% 3.80/6.09 inference(cnf_transformation,[],[f1769])).
% 3.80/6.09
% 3.80/6.09 tcf(c_280,plain,![X0_'A':'A$']:
% 3.80/6.09 ('fun_app$m'('fun_app$n'('times$e',X0_'A'),'zero$') = 'zero$'),
% 3.80/6.09 inference(cnf_transformation,[],[f1792])).
% 3.80/6.09
% 3.80/6.09 tcf(c_8994,plain,
% 3.80/6.09 ('fun_app$m'('fun_app$n'('times$e','fun_app$d'('vec_nth$b'('x$'),'the$'('uu$'))),'zero$') != 'zero$'),
% 3.80/6.09 inference(light_normalisation,[status(thm)],[c_257,c_258])).
% 3.80/6.09
% 3.80/6.09 tcf(c_8995,plain,
% 3.80/6.09 ('zero$' != 'zero$'),
% 3.80/6.09 inference(demodulation,[status(thm)],[c_8994,c_280])).
% 3.80/6.09
% 3.80/6.09 tcf(c_8996,plain,
% 3.80/6.09 ($false),
% 3.80/6.09 inference(equality_resolution_simp,[status(thm)],[c_8995])).
% 3.80/6.09
% 3.80/6.09
% 3.80/6.09 % SZS output end CNFRefutation for theBenchmark.p
% 3.80/6.09
% 3.80/6.09
%------------------------------------------------------------------------------