%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP327_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:53:39 PM UTC 2025
% Result : Theorem 16.28s 5.27s
% Output : CNFRefutation 16.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ITP327_1 : TPTP v9.0.0. Released v8.0.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 02:17:09 EDT 2025
% 0.12/0.34 % CPUTime :
% 16.28/5.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.28/5.28
% 16.28/5.28 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.28/5.29 %$ member$e > member$d > member$c > member$b > member$a > less_eq$c > less_eq$a > is_zero_row$ > fun_app$p > fun_app$o > fun_app$g > fun_app$e > fun_app$c > fun_app$ > dependent$b > dependent$a > reduced_row_echelon_form$e > reduced_row_echelon_form$d > reduced_row_echelon_form$c > reduced_row_echelon_form$b > reduced_row_echelon_form$a > reduced_row_echelon_form$ > finite$b > finite$a > uww$ > uwv$ > uwb$ > uwa$ > uvz$ > uvy$ > uvx$ > uvw$ > uvv$ > uvu$ > uym$ > uyc$ > uxx$ > uxi$ > uxh$ > uxg$ > uwq$ > uwo$ > uwm$ > uwk$ > uwi$ > uwg$ > uwe$ > uwc$ > uuu$ > mult_row_row$c > mult_row_row$b > mult_row_row$a > mult_row_row$ > mult_row$ > mult_column_row$c > mult_column_row$b > mult_column_row$a > mult_column_row$ > mult_column$ > interchange_rows_row$ > interchange_rows$ > interchange_columns_row$ > interchange_columns$ > vector_scalar_mult$b > vec_nth$k > vec_nth$j > vec_nth$i > vec_nth$h > vec_nth$g > vec_nth$f > uyl$ > uyk$ > uyj$ > uyi$ > uyh$ > uyg$ > uyf$ > uyb$ > uya$ > uxz$ > uxy$ > uxw$ > uxv$ > uxu$ > uxt$ > uxs$ > uxp$ > uxn$ > uxm$ > uxl$ > uxk$ > uxj$ > uxe$ > uxc$ > uxa$ > uwy$ > uwr$ > uwp$ > uwn$ > uwl$ > uwj$ > uwh$ > uwf$ > uwd$ > uvq$ > uvp$ > uvo$ > uvn$ > uvm$ > uvl$ > uvi$ > uvh$ > uvg$ > uvf$ > uve$ > uvd$ > uut$ > times$l > times$k > times$j > times$i > times$h > times$g > times$f > sum$a > sum$ > row$c > row$b > row$a > row$ > minus$e > minus$d > map_matrix$k > map_matrix$j > map_matrix$i > map_matrix$h > map_matrix$g > map_matrix$f > map_matrix$e > map_matrix$d > map_matrix$c > map_matrix$b > map_matrix$a > map_matrix$ > insert$c > insert$b > insert$a > fun_app$z > fun_app$y > fun_app$x > fun_app$w > fun_app$v > fun_app$u > fun_app$t > fun_app$s > fun_app$r > fun_app$q > fun_app$n > fun_app$m > fun_app$l > fun_app$k > fun_app$j > fun_app$i > fun_app$h > fun_app$f > fun_app$d > fun_app$b > fun_app$ah > fun_app$ag > fun_app$af > fun_app$ae > fun_app$ad > fun_app$ac > fun_app$ab > fun_app$aa > fun_app$a > column$g > column$f > column$e > column$d > column$c > column$b > column$a > column$ > #nlpp > vec_nth$e > vec_nth$d > vec_nth$c > vec_nth$b > vec_nth$a > vec_nth$ > vec_lambda$g > vec_lambda$f > vec_lambda$e > vec_lambda$d > vec_lambda$c > vec_lambda$b > vec_lambda$a > vec_lambda$ > uye$ > uyd$ > uxq$ > uxo$ > uxf$ > uxd$ > uxb$ > uwz$ > uwx$ > uvj$ > uvc$ > uvb$ > uva$ > uuy$ > uux$ > uum$ > uul$ > uuk$ > uuj$ > uui$ > uug$ > times$d > times$c > times$b > times$ > the_elem$a > the_elem$ > the$a > the$ > minus$b > minus$a > minus$ > member$ > less_eq$b > less_eq$ > less$b > less$a > less$ > least$b > least$a > least$ > insert$ > dependent$ > columns$ > collect$c > collect$b > collect$a > collect$ > col_space$ > zero$k > zero$j > zero$i > zero$h > zero$g > zero$f > zero$e > zero$d > zero$c > zero$b > zero$a > zero$ > y$ > xa$ > x$ > vector_scalar_mult$a > vector_scalar_mult$ > v$ > uxr$ > uwu$ > uwt$ > uws$ > uvt$ > uvs$ > uvr$ > uvk$ > uuz$ > uuw$ > uuv$ > uus$ > uur$ > uuq$ > uup$ > uuo$ > uun$ > uuh$ > uuf$ > uue$ > uud$ > uuc$ > uub$ > uua$ > uu$ > tltrue > tlfalse > times$e > times$a > one$h > one$g > one$f > one$e > one$d > one$c > one$b > one$a > one$ > minus$c > is_singleton$ > i$ > finite$ > bot$e > bot$d > bot$c > bot$b > bot$a > bot$ > b$ > a$ > #skF_68 > #skF_82 > #skF_92 > #skF_59 > #skF_127 > #skF_115 > #skF_167 > #skF_166 > #skF_13 > #skF_103 > #skF_144 > #skF_9 > #skF_168 > #skF_118 > #skF_142 > #skF_27 > #skF_169 > #skF_116 > #skF_105 > #skF_81 > #skF_125 > #skF_100 > #skF_30 > #skF_102 > #skF_126 > #skF_60 > #skF_94 > #skF_124 > #skF_97 > #skF_149 > #skF_147 > #skF_71 > #skF_19 > #skF_163 > #skF_141 > #skF_74 > #skF_151 > #skF_154 > #skF_51 > #skF_89 > #skF_58 > #skF_150 > #skF_84 > #skF_146 > #skF_101 > #skF_80 > #skF_136 > #skF_2 > #skF_37 > #skF_1 > #skF_90 > #skF_72 > #skF_8 > #skF_48 > #skF_135 > #skF_133 > #skF_113 > #skF_114 > #skF_85 > #skF_121 > #skF_87 > #skF_44 > #skF_63 > #skF_66 > #skF_159 > #skF_78 > #skF_32 > #skF_123 > #skF_50 > #skF_155 > #skF_7 > #skF_34 > #skF_22 > #skF_40 > #skF_33 > #skF_49 > #skF_119 > #skF_17 > #skF_139 > #skF_107 > #skF_46 > #skF_86 > #skF_91 > #skF_109 > #skF_38 > #skF_79 > #skF_132 > #skF_128 > #skF_65 > #skF_106 > #skF_73 > #skF_45 > #skF_4 > #skF_161 > #skF_41 > #skF_15 > #skF_62 > #skF_21 > #skF_29 > #skF_120 > #skF_143 > #skF_43 > #skF_164 > #skF_18 > #skF_39 > #skF_111 > #skF_172 > #skF_129 > #skF_55 > #skF_110 > #skF_16 > #skF_14 > #skF_26 > #skF_108 > #skF_28 > #skF_75 > #skF_104 > #skF_148 > #skF_42 > #skF_47 > #skF_117 > #skF_96 > #skF_95 > #skF_12 > #skF_152 > #skF_54 > #skF_31 > #skF_24 > #skF_145 > #skF_20 > #skF_157 > #skF_11 > #skF_137 > #skF_67 > #skF_23 > #skF_57 > #skF_138 > #skF_35 > #skF_140 > #skF_3 > #skF_158 > #skF_170 > #skF_160 > #skF_36 > #skF_134 > #skF_162 > #skF_153 > #skF_56 > #skF_99 > #skF_76 > #skF_70 > #skF_53 > #skF_93 > #skF_98 > #skF_25 > #skF_5 > #skF_77 > #skF_122 > #skF_52 > #skF_88 > #skF_69 > #skF_10 > #skF_171 > #skF_61 > #skF_83 > #skF_6 > #skF_156 > #skF_131 > #skF_112 > #skF_165 > #skF_130 > #skF_64
% 16.28/5.29
% 16.28/5.29 %Foreground sorts:
% 16.28/5.29 tff(A$, type, A$: $tType ).
% 16.28/5.29 tff(A_a_fun$, type, A_a_fun$: $tType ).
% 16.28/5.29 tff(A_set_set$, type, A_set_set$: $tType ).
% 16.28/5.29 tff(A_a_m_vec_fun$, type, A_a_m_vec_fun$: $tType ).
% 16.28/5.29 tff(N_a_m_vec_n_vec_fun$, type, N_a_m_vec_n_vec_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_n_vec_m_vec$, type, A_m_vec_n_vec_m_vec$: $tType ).
% 16.28/5.29 tff(N_a_n_vec_bool_fun_fun$, type, N_a_n_vec_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_a_n_vec_bool_fun_fun$, type, A_n_vec_a_n_vec_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec$, type, A_m_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_a_m_vec_fun$, type, A_n_vec_a_m_vec_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_n_vec$, type, A_m_vec_n_vec$: $tType ).
% 16.28/5.29 tff(A_a_m_vec_a_m_vec_fun_fun$, type, A_a_m_vec_a_m_vec_fun_fun$: $tType ).
% 16.28/5.29 tff(A_set_a_set_fun$, type, A_set_a_set_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_m_vec$, type, A_m_vec_m_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_n_vec$, type, A_n_vec_n_vec$: $tType ).
% 16.28/5.29 tff(A_set$, type, A_set$: $tType ).
% 16.28/5.29 tff(N$, type, N$: $tType ).
% 16.28/5.29 tff(tlbool, type, tlbool: $tType ).
% 16.28/5.29 tff(A_m_vec_a_fun$, type, A_m_vec_a_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_n_vec_set$, type, A_m_vec_n_vec_set$: $tType ).
% 16.28/5.29 tff(A_bool_fun$, type, A_bool_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_a_n_vec_fun$, type, A_n_vec_a_n_vec_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_n_vec_a_m_vec_n_vec_fun$, type, A_m_vec_n_vec_a_m_vec_n_vec_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_a_fun$, type, A_n_vec_a_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_n_vec_n_vec$, type, A_m_vec_n_vec_n_vec$: $tType ).
% 16.28/5.29 tff(M_a_m_vec_bool_fun_fun$, type, M_a_m_vec_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_set_a_n_vec_set_fun$, type, A_n_vec_set_a_n_vec_set_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec$, type, A_n_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_bool_fun$, type, A_n_vec_bool_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_set_bool_fun$, type, A_n_vec_set_bool_fun$: $tType ).
% 16.28/5.29 tff(M_a_n_vec_fun$, type, M_a_n_vec_fun$: $tType ).
% 16.28/5.29 tff(M$, type, M$: $tType ).
% 16.28/5.29 tff(A_a_a_fun_fun$, type, A_a_a_fun_fun$: $tType ).
% 16.28/5.29 tff(M_a_m_vec_fun$, type, M_a_m_vec_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_m_vec_n_vec$, type, A_m_vec_m_vec_n_vec$: $tType ).
% 16.28/5.29 tff(N_a_fun$, type, N_a_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_bool_fun$, type, A_m_vec_bool_fun$: $tType ).
% 16.28/5.29 tff(N_set$, type, N_set$: $tType ).
% 16.28/5.29 tff(A_n_vec_set$, type, A_n_vec_set$: $tType ).
% 16.28/5.29 tff(A_a_n_vec_a_n_vec_fun_fun$, type, A_a_n_vec_a_n_vec_fun_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_n_vec_n_vec$, type, A_n_vec_n_vec_n_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_set_set$, type, A_n_vec_set_set$: $tType ).
% 16.28/5.29 tff(N_bool_fun$, type, N_bool_fun$: $tType ).
% 16.28/5.29 tff(M_a_fun$, type, M_a_fun$: $tType ).
% 16.28/5.29 tff(A_m_vec_set$, type, A_m_vec_set$: $tType ).
% 16.28/5.29 tff(M_a_m_vec_n_vec_fun$, type, M_a_m_vec_n_vec_fun$: $tType ).
% 16.28/5.29 tff(M_bool_fun$, type, M_bool_fun$: $tType ).
% 16.28/5.29 tff(N_a_m_vec_fun$, type, N_a_m_vec_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_n_vec_m_vec$, type, A_n_vec_n_vec_m_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_a_n_vec_a_n_vec_fun_fun$, type, A_n_vec_a_n_vec_a_n_vec_fun_fun$: $tType ).
% 16.28/5.29 tff(N_a_m_vec_bool_fun_fun$, type, N_a_m_vec_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(N_a_n_vec_fun$, type, N_a_n_vec_fun$: $tType ).
% 16.28/5.29 tff(N_a_bool_fun_fun$, type, N_a_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(A_n_vec_m_vec_n_vec$, type, A_n_vec_m_vec_n_vec$: $tType ).
% 16.28/5.29 tff(A_n_vec_m_vec$, type, A_n_vec_m_vec$: $tType ).
% 16.28/5.29 tff(A_m_vec_a_m_vec_fun$, type, A_m_vec_a_m_vec_fun$: $tType ).
% 16.28/5.29 tff(M_a_bool_fun_fun$, type, M_a_bool_fun_fun$: $tType ).
% 16.28/5.29 tff(M_a_n_vec_bool_fun_fun$, type, M_a_n_vec_bool_fun_fun$: $tType ).
% 16.28/5.29
% 16.28/5.29 %Background operators:
% 16.28/5.29
% 16.28/5.29
% 16.28/5.29 %Foreground operators:
% 16.28/5.29 tff(fun_app$s, type, fun_app$s: (M_a_n_vec_fun$ * M$) > A_n_vec$).
% 16.28/5.29 tff(zero$a, type, zero$a: A_m_vec$).
% 16.28/5.29 tff(uvm$, type, uvm$: (M$ * A_m_vec_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.29 tff('#skF_68', type, '#skF_68': (A_n_vec_bool_fun$ * A_n_vec$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.29 tff(times$j, type, times$j: (A_m_vec_set$ * A_m_vec_set$) > A_m_vec_set$).
% 16.28/5.29 tff(zero$, type, zero$: A$).
% 16.28/5.29 tff(map_matrix$, type, map_matrix$: (A_a_fun$ * A_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.29 tff(interchange_rows_row$, type, interchange_rows_row$: (A_m_vec_n_vec$ * N$ * N$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(reduced_row_echelon_form$, type, reduced_row_echelon_form$: A_m_vec_n_vec$ > $o).
% 16.28/5.29 tff(uye$, type, uye$: A_n_vec_set$ > A_n_vec_bool_fun$).
% 16.28/5.29 tff('#skF_82', type, '#skF_82': (A_m_vec$ * M_a_fun$) > M$).
% 16.28/5.29 tff(fun_app$e, type, fun_app$e: (A_n_vec_bool_fun$ * A_n_vec$) > $o).
% 16.28/5.29 tff(less$a, type, less$a: M$ > M_bool_fun$).
% 16.28/5.29 tff(i$, type, i$: N$).
% 16.28/5.29 tff(uuy$, type, uuy$: A_m_vec$ > A_m_vec_a_m_vec_fun$).
% 16.28/5.29 tff(uwv$, type, uwv$: (A_m_vec_n_vec$ * M$ * M$ * N$) > M_a_fun$).
% 16.28/5.29 tff(dependent$, type, dependent$: A_a_n_vec_a_n_vec_fun_fun$ > A_n_vec_set_bool_fun$).
% 16.28/5.29 tff(uyc$, type, uyc$: (A_n_vec_set$ * A_n_vec_a_fun$ * A_n_vec_a_fun$) > A_n_vec_bool_fun$).
% 16.28/5.29 tff(uwd$, type, uwd$: (A_a_m_vec_fun$ * A_n_vec_m_vec$) > M_a_m_vec_n_vec_fun$).
% 16.28/5.29 tff(vector_scalar_mult$, type, vector_scalar_mult$: A_a_n_vec_a_n_vec_fun_fun$).
% 16.28/5.29 tff('#skF_92', type, '#skF_92': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.29 tff(columns$, type, columns$: A_m_vec_n_vec$ > A_n_vec_set$).
% 16.28/5.29 tff(uvb$, type, uvb$: A_n_vec_set$ > A_n_vec_set_a_n_vec_set_fun$).
% 16.28/5.29 tff('#skF_59', type, '#skF_59': (A_n_vec$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.29 tff(fun_app$ab, type, fun_app$ab: (M_a_n_vec_bool_fun_fun$ * M$) > A_n_vec_bool_fun$).
% 16.28/5.29 tff(uyb$, type, uyb$: (A_n_vec_set$ * A_n_vec_a_fun$) > A_n_vec_bool_fun$).
% 16.28/5.29 tff(one$a, type, one$a: A_m_vec$).
% 16.28/5.29 tff(uxh$, type, uxh$: (A_m_vec_n_vec$ * N$ * A$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(uwx$, type, uwx$: A_m_vec_n_vec$ > A_m_vec_bool_fun$).
% 16.28/5.29 tff(fun_app$q, type, fun_app$q: (A_n_vec_a_n_vec_bool_fun_fun$ * A_n_vec$) > A_n_vec_bool_fun$).
% 16.28/5.29 tff(uvl$, type, uvl$: (N$ * A_m_vec_n_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(member$b, type, member$b: (A_n_vec_set$ * A_n_vec_set_set$) > $o).
% 16.28/5.29 tff(map_matrix$j, type, map_matrix$j: (A_a_m_vec_fun$ * A_n_vec_m_vec$) > A_m_vec_n_vec_m_vec$).
% 16.28/5.29 tff('#skF_127', type, '#skF_127': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.29 tff(uvi$, type, uvi$: (A_m_vec_n_vec$ * A_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(vec_lambda$b, type, vec_lambda$b: N_a_m_vec_fun$ > A_m_vec_n_vec$).
% 16.28/5.29 tff(uuh$, type, uuh$: A_n_vec_a_n_vec_bool_fun_fun$).
% 16.28/5.29 tff('#skF_115', type, '#skF_115': A_n_vec_set$ > A_n_vec$).
% 16.28/5.29 tff(uug$, type, uug$: N$ > N_bool_fun$).
% 16.28/5.29 tff(uuk$, type, uuk$: A_m_vec_set$ > A_m_vec_bool_fun$).
% 16.28/5.29 tff('#skF_167', type, '#skF_167': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.29 tff(uyg$, type, uyg$: (A_m_vec$ * A_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(fun_app$ah, type, fun_app$ah: (A_a_m_vec_a_m_vec_fun_fun$ * A$) > A_m_vec_a_m_vec_fun$).
% 16.28/5.29 tff('#skF_166', type, '#skF_166': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.29 tff(uvy$, type, uvy$: (A_m_vec_m_vec$ * M$ * A$ * M$) > M_a_fun$).
% 16.28/5.29 tff('#skF_13', type, '#skF_13': (A_n_vec_n_vec$ * A_n_vec_n_vec$) > N$).
% 16.28/5.29 tff(mult_column_row$a, type, mult_column_row$a: (A_n_vec_n_vec$ * N$ * A$) > N_a_n_vec_fun$).
% 16.28/5.29 tff(member$, type, member$: A_n_vec$ > A_n_vec_set_bool_fun$).
% 16.28/5.29 tff(uxc$, type, uxc$: (A_m_vec_m_vec$ * M$) > M_bool_fun$).
% 16.28/5.29 tff('#skF_103', type, '#skF_103': (A_n_vec_set_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.29 tff(map_matrix$e, type, map_matrix$e: (A_n_vec_a_fun$ * A_n_vec_n_vec_m_vec$) > A_n_vec_m_vec$).
% 16.28/5.29 tff('#skF_144', type, '#skF_144': (A_n_vec_set_bool_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.29 tff(uub$, type, uub$: A_m_vec_n_vec_a_m_vec_n_vec_fun$).
% 16.28/5.29 tff(fun_app$h, 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$).
% 16.28/5.29 tff(uui$, type, uui$: N$ > N_bool_fun$).
% 16.28/5.29 tff(uvo$, type, uvo$: (M$ * A_m_vec_m_vec$) > M_a_fun$).
% 16.28/5.29 tff(uww$, type, uww$: (A_m_vec_n_vec$ * N$ * N$ * N$) > M_a_fun$).
% 16.28/5.29 tff(sum$, type, sum$: (A_n_vec_a_fun$ * A_n_vec_set$) > A$).
% 16.28/5.29 tff(uuv$, type, uuv$: M_bool_fun$).
% 16.28/5.29 tff('#skF_9', type, '#skF_9': (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$).
% 16.28/5.29 tff(mult_column_row$c, type, mult_column_row$c: (A_m_vec_n_vec$ * M$ * A$) > N_a_m_vec_fun$).
% 16.28/5.29 tff(uvv$, type, uvv$: (A_n_vec_m_vec$ * N$ * A$ * M$) > N_a_fun$).
% 16.28/5.29 tff(fun_app$ad, type, fun_app$ad: (N_a_bool_fun_fun$ * N$) > A_bool_fun$).
% 16.28/5.29 tff('#skF_168', type, '#skF_168': A_n_vec_set$ > A_n_vec$).
% 16.28/5.29 tff('#skF_118', type, '#skF_118': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.29 tff('#skF_142', type, '#skF_142': (M_bool_fun$ * M$ * M$) > M$).
% 16.28/5.29 tff(fun_app$u, type, fun_app$u: (A_n_vec_a_m_vec_fun$ * A_n_vec$) > A_m_vec$).
% 16.28/5.29 tff(uue$, type, uue$: A_a_fun$).
% 16.28/5.29 tff('#skF_27', type, '#skF_27': N_a_n_vec_bool_fun_fun$ > N$).
% 16.28/5.29 tff('#skF_169', type, '#skF_169': A_n_vec_set$ > A_n_vec$).
% 16.28/5.29 tff('#skF_116', type, '#skF_116': A_n_vec_set$ > A_n_vec_set$).
% 16.28/5.29 tff('#skF_105', type, '#skF_105': A_n_vec_set_set$ > A_n_vec_set$).
% 16.28/5.29 tff('#skF_81', type, '#skF_81': (A_n_vec$ * N_a_fun$) > N$).
% 16.28/5.29 tff(map_matrix$a, type, map_matrix$a: (A_a_fun$ * A_n_vec_m_vec$) > A_n_vec_m_vec$).
% 16.28/5.29 tff('#skF_125', type, '#skF_125': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.29 tff('#skF_100', type, '#skF_100': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_n_vec_bool_fun_fun$) > A_n_vec$).
% 16.28/5.29 tff(vec_nth$h, type, vec_nth$h: (A_n_vec_m_vec_n_vec$ * N$) > A_n_vec_m_vec$).
% 16.28/5.29 tff(fun_app$t, type, fun_app$t: (M_a_m_vec_fun$ * M$) > A_m_vec$).
% 16.28/5.29 tff(bot$a, type, bot$a: N_set$).
% 16.28/5.29 tff(less_eq$, type, less_eq$: A_n_vec_set$ > A_n_vec_set_bool_fun$).
% 16.28/5.29 tff(uyd$, type, uyd$: N_set$ > N_bool_fun$).
% 16.28/5.29 tff(uwa$, type, uwa$: (A_n_vec_n_vec$ * N$ * A$ * N$) > N_a_fun$).
% 16.28/5.29 tff(fun_app$v, type, fun_app$v: (A_n_vec_a_fun$ * A_n_vec$) > A$).
% 16.28/5.29 tff('#skF_30', type, '#skF_30': (N_a_bool_fun_fun$ * N$) > A$).
% 16.28/5.30 tff('#skF_102', type, '#skF_102': (A_n_vec_set_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(uwe$, type, uwe$: (A_a_m_vec_fun$ * A_n_vec_n_vec$ * N$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(uvw$, type, uvw$: (A_n_vec_n_vec$ * N$ * A$ * N$) > N_a_fun$).
% 16.28/5.30 tff('#skF_126', type, '#skF_126': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(bot$, type, bot$: A_n_vec_set$).
% 16.28/5.30 tff(one$c, type, one$c: A_n_vec$).
% 16.28/5.30 tff(uwk$, type, uwk$: (A_a_fun$ * A_n_vec_n_vec$ * N$) > N_a_fun$).
% 16.28/5.30 tff(the$, type, the$: N_bool_fun$ > N$).
% 16.28/5.30 tff(uxy$, type, uxy$: (A_n_vec_bool_fun$ * A_n_vec_a_n_vec_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(uwy$, type, uwy$: (A_n_vec_n_vec$ * N$) > N_bool_fun$).
% 16.28/5.30 tff(uvt$, type, uvt$: N_a_fun$).
% 16.28/5.30 tff(uus$, type, uus$: A_a_fun$).
% 16.28/5.30 tff('#skF_60', type, '#skF_60': (A_n_vec$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff(bot$e, type, bot$e: A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_94', type, '#skF_94': (A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff('#skF_124', type, '#skF_124': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(times$e, type, times$e: A_a_a_fun_fun$).
% 16.28/5.30 tff(less$, type, less$: N$ > N_bool_fun$).
% 16.28/5.30 tff('#skF_97', type, '#skF_97': (A_n_vec$ * A_n_vec_set$ * A_n_vec$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_149', type, '#skF_149': (M_bool_fun$ * M$) > M$).
% 16.28/5.30 tff('#skF_147', type, '#skF_147': (A_n_vec_set_bool_fun$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(uxq$, type, uxq$: A_n_vec_a_n_vec_bool_fun_fun$ > A_n_vec_a_n_vec_bool_fun_fun$).
% 16.28/5.30 tff(uxj$, type, uxj$: (A_n_vec$ * A_n_vec$) > N_a_fun$).
% 16.28/5.30 tff(vec_nth$b, type, vec_nth$b: A_n_vec$ > N_a_fun$).
% 16.28/5.30 tff(uvn$, type, uvn$: (N$ * A_n_vec_m_vec$) > M_a_fun$).
% 16.28/5.30 tff('#skF_71', type, '#skF_71': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff('#skF_19', type, '#skF_19': M_a_m_vec_bool_fun_fun$ > M$).
% 16.28/5.30 tff(xa$, type, xa$: A_n_vec$).
% 16.28/5.30 tff('#skF_163', type, '#skF_163': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_141', type, '#skF_141': (M_bool_fun$ * M$ * M$) > M$).
% 16.28/5.30 tff(uxb$, type, uxb$: A_n_vec_m_vec$ > A_m_vec_bool_fun$).
% 16.28/5.30 tff(times$, type, times$: A_m_vec_n_vec$ > A_m_vec_n_vec_a_m_vec_n_vec_fun$).
% 16.28/5.30 tff('#skF_74', type, '#skF_74': (N_bool_fun$ * N_bool_fun$) > N$).
% 16.28/5.30 tff('#skF_151', type, '#skF_151': (M_bool_fun$ * M$ * M_bool_fun$) > M$).
% 16.28/5.30 tff(uvc$, type, uvc$: A$ > A_a_fun$).
% 16.28/5.30 tff('#skF_154', type, '#skF_154': (A_n_vec$ * A_n_vec_set$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(interchange_columns_row$, type, interchange_columns_row$: (A_m_vec_n_vec$ * M$ * M$) > N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_51', type, '#skF_51': (A_m_vec_n_vec$ * A_m_vec_n_vec_set$ * A_m_vec_n_vec_set$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(zero$i, type, zero$i: A_set$).
% 16.28/5.30 tff('#skF_89', type, '#skF_89': (A_n_vec_bool_fun$ * A_n_vec_a_n_vec_bool_fun_fun$) > A_n_vec$).
% 16.28/5.30 tff(map_matrix$k, type, map_matrix$k: (A_a_m_vec_fun$ * A_n_vec_n_vec$) > A_m_vec_n_vec_n_vec$).
% 16.28/5.30 tff(least$b, type, least$b: A_n_vec_set_bool_fun$ > A_n_vec_set$).
% 16.28/5.30 tff('#skF_58', type, '#skF_58': (A_n_vec_set$ * A_n_vec_set_set$ * A_n_vec_set_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_150', type, '#skF_150': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_84', type, '#skF_84': A_n_vec$).
% 16.28/5.30 tff('#skF_146', type, '#skF_146': (M_bool_fun$ * M$ * M_bool_fun$) > M$).
% 16.28/5.30 tff('#skF_101', type, '#skF_101': A_n_vec_bool_fun$ > A_n_vec$).
% 16.28/5.30 tff(uwh$, type, uwh$: (A_a_fun$ * A_m_vec_m_vec$) > M_a_m_vec_fun$).
% 16.28/5.30 tff(one$b, type, one$b: A_m_vec_n_vec$).
% 16.28/5.30 tff(map_matrix$f, type, map_matrix$f: (A_m_vec_a_fun$ * A_m_vec_n_vec_n_vec$) > A_n_vec_n_vec$).
% 16.28/5.30 tff(vec_nth$d, type, vec_nth$d: A_n_vec_m_vec$ > M_a_n_vec_fun$).
% 16.28/5.30 tff(one$d, type, one$d: A_set$).
% 16.28/5.30 tff(fun_app$k, type, fun_app$k: (A_m_vec_a_m_vec_fun$ * A_m_vec$) > A_m_vec$).
% 16.28/5.30 tff(uxo$, type, uxo$: A_n_vec_set$ > A_n_vec_set_bool_fun$).
% 16.28/5.30 tff('#skF_80', type, '#skF_80': (A_n_vec_n_vec$ * N_a_n_vec_fun$) > N$).
% 16.28/5.30 tff('#skF_136', type, '#skF_136': (M_bool_fun$ * M$ * M_bool_fun$) > M$).
% 16.28/5.30 tff('#skF_2', type, '#skF_2': (A_m_vec_n_vec$ * A_n_vec$) > N$).
% 16.28/5.30 tff(uwm$, type, uwm$: (A_a_fun$ * A_m_vec_n_vec$ * N$) > M_a_fun$).
% 16.28/5.30 tff(uxl$, type, uxl$: (A_m_vec_n_vec$ * A_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(tlfalse, type, tlfalse: tlbool).
% 16.28/5.30 tff('#skF_37', type, '#skF_37': (N_a_m_vec_bool_fun_fun$ * A_m_vec_n_vec$) > N$).
% 16.28/5.30 tff(uxt$, type, uxt$: (A_n_vec_set$ * A_n_vec_a_n_vec_bool_fun_fun$) > A_n_vec_a_n_vec_bool_fun_fun$).
% 16.28/5.30 tff(uwb$, type, uwb$: (A_m_vec_n_vec$ * N$ * A$ * N$) > M_a_fun$).
% 16.28/5.30 tff('#skF_1', type, '#skF_1': A_n_vec$ > N$).
% 16.28/5.30 tff(reduced_row_echelon_form$a, type, reduced_row_echelon_form$a: A_n_vec_n_vec_n_vec$ > $o).
% 16.28/5.30 tff(uvg$, type, uvg$: (A_n_vec$ * A_n_vec$) > N_a_fun$).
% 16.28/5.30 tff(uvx$, type, uvx$: (A_m_vec_n_vec$ * M$ * A$ * N$) > M_a_fun$).
% 16.28/5.30 tff(y$, type, y$: N$).
% 16.28/5.30 tff(row$a, type, row$a: (M$ * A_m_vec_m_vec$) > A_m_vec$).
% 16.28/5.30 tff(dependent$a, type, dependent$a: (A_a_a_fun_fun$ * A_set$) > $o).
% 16.28/5.30 tff(uud$, type, uud$: A_m_vec_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_90', type, '#skF_90': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff('#skF_72', type, '#skF_72': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(uup$, type, uup$: A_n_vec_a_n_vec_fun$).
% 16.28/5.30 tff(one$g, type, one$g: A_n_vec_m_vec$).
% 16.28/5.30 tff('#skF_8', type, '#skF_8': (A_n_vec_bool_fun$ * A_n_vec_a_n_vec_bool_fun_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(uuq$, type, uuq$: A_set_a_set_fun$).
% 16.28/5.30 tff('#skF_48', type, '#skF_48': (A_n_vec_set_bool_fun$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(uum$, type, uum$: A_n_vec_set$ > A_n_vec_bool_fun$).
% 16.28/5.30 tff(fun_app$, type, fun_app$: (M_bool_fun$ * M$) > $o).
% 16.28/5.30 tff('#skF_135', type, '#skF_135': (M_bool_fun$ * M_bool_fun$) > M$).
% 16.28/5.30 tff(col_space$, type, col_space$: A_m_vec_n_vec$ > A_n_vec_set$).
% 16.28/5.30 tff('#skF_133', type, '#skF_133': (A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(minus$d, type, minus$d: (A_m_vec_n_vec$ * A_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_113', type, '#skF_113': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(mult_row_row$b, type, mult_row_row$b: (A_m_vec_m_vec$ * M$ * A$) > M_a_m_vec_fun$).
% 16.28/5.30 tff(bot$d, type, bot$d: A_n_vec_set_set$).
% 16.28/5.30 tff('#skF_114', type, '#skF_114': A_n_vec_set$ > A_n_vec_set$).
% 16.28/5.30 tff(least$, type, least$: M_bool_fun$ > M$).
% 16.28/5.30 tff(uwz$, type, uwz$: A_n_vec_n_vec$ > A_n_vec_bool_fun$).
% 16.28/5.30 tff(dependent$b, type, dependent$b: (A_a_m_vec_a_m_vec_fun_fun$ * A_m_vec_set$) > $o).
% 16.28/5.30 tff(map_matrix$d, type, map_matrix$d: (A_m_vec_a_fun$ * A_m_vec_n_vec_m_vec$) > A_n_vec_m_vec$).
% 16.28/5.30 tff('#skF_85', type, '#skF_85': A_n_vec_bool_fun$ > A_n_vec$).
% 16.28/5.30 tff(member$a, type, member$a: (A_m_vec$ * A_m_vec_set$) > $o).
% 16.28/5.30 tff('#skF_121', type, '#skF_121': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(uws$, type, uws$: N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_87', type, '#skF_87': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff(vec_lambda$d, type, vec_lambda$d: M_a_n_vec_fun$ > A_n_vec_m_vec$).
% 16.28/5.30 tff(uur$, type, uur$: A_n_vec_set_a_n_vec_set_fun$).
% 16.28/5.30 tff(zero$g, type, zero$g: A_n_vec_set$).
% 16.28/5.30 tff(uvz$, type, uvz$: (A_n_vec_m_vec$ * M$ * A$ * M$) > N_a_fun$).
% 16.28/5.30 tff(uyj$, type, uyj$: (A_n_vec_set$ * A_n_vec_a_m_vec_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_44', type, '#skF_44': (N_bool_fun$ * N$ * N$) > N$).
% 16.28/5.30 tff('#skF_63', type, '#skF_63': (A_n_vec_bool_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(fun_app$f, type, fun_app$f: (A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_66', type, '#skF_66': (N_bool_fun$ * N$) > N$).
% 16.28/5.30 tff(uxd$, type, uxd$: A_m_vec_m_vec$ > A_m_vec_bool_fun$).
% 16.28/5.30 tff(vec_lambda$a, type, vec_lambda$a: N_a_fun$ > A_n_vec$).
% 16.28/5.30 tff('#skF_159', type, '#skF_159': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_78', type, '#skF_78': (A_m_vec_m_vec$ * M_a_m_vec_fun$) > M$).
% 16.28/5.30 tff(mult_row_row$a, type, mult_row_row$a: (A_n_vec_n_vec$ * N$ * A$) > N_a_n_vec_fun$).
% 16.28/5.30 tff(less$b, type, less$b: A_n_vec_set$ > A_n_vec_set_bool_fun$).
% 16.28/5.30 tff(collect$, type, collect$: A_bool_fun$ > A_set$).
% 16.28/5.30 tff('#skF_32', type, '#skF_32': N_a_bool_fun_fun$ > A_n_vec$).
% 16.28/5.30 tff(uuc$, type, uuc$: A_n_vec_a_n_vec_fun$).
% 16.28/5.30 tff(fun_app$g, type, fun_app$g: (A_n_vec_set_bool_fun$ * A_n_vec_set$) > $o).
% 16.28/5.30 tff(uwp$, type, uwp$: (A_m_vec_a_fun$ * A_m_vec_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(zero$b, type, zero$b: A_n_vec$).
% 16.28/5.30 tff('#skF_123', type, '#skF_123': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_50', type, '#skF_50': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(insert$c, type, insert$c: (A_m_vec$ * A_m_vec_set$) > A_m_vec_set$).
% 16.28/5.30 tff('#skF_155', type, '#skF_155': (A_n_vec$ * A_n_vec_set$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(v$, type, v$: A_n_vec$).
% 16.28/5.30 tff(zero$f, type, zero$f: A_n_vec_n_vec$).
% 16.28/5.30 tff(times$f, type, times$f: (A_m_vec_m_vec$ * A_m_vec_m_vec$) > A_m_vec_m_vec$).
% 16.28/5.30 tff(uxi$, type, uxi$: (A_m_vec_n_vec$ * M$ * M$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(uvk$, type, uvk$: A_n_vec_bool_fun$).
% 16.28/5.30 tff(map_matrix$g, type, map_matrix$g: (A_n_vec_a_fun$ * A_n_vec_n_vec_n_vec$) > A_n_vec_n_vec$).
% 16.28/5.30 tff(finite$b, type, finite$b: A_n_vec_set_set$ > $o).
% 16.28/5.30 tff('#skF_7', type, '#skF_7': (A_n_vec_bool_fun$ * A_n_vec_a_n_vec_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(uvp$, type, uvp$: (N$ * A_n_vec_n_vec$) > N_a_fun$).
% 16.28/5.30 tff('#skF_34', type, '#skF_34': (M_a_bool_fun_fun$ * M$) > A$).
% 16.28/5.30 tff('#skF_22', type, '#skF_22': (M_a_n_vec_bool_fun_fun$ * M$) > A_n_vec$).
% 16.28/5.30 tff('#skF_40', type, '#skF_40': N_a_m_vec_bool_fun_fun$ > A_m_vec_n_vec$).
% 16.28/5.30 tff(uua$, type, uua$: N_bool_fun$).
% 16.28/5.30 tff(mult_row$, type, mult_row$: (A_m_vec_n_vec$ * N$ * A$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_33', type, '#skF_33': (M_a_bool_fun_fun$ * A_m_vec$) > M$).
% 16.28/5.30 tff('#skF_49', type, '#skF_49': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_119', type, '#skF_119': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_17', type, '#skF_17': (M_a_m_vec_bool_fun_fun$ * A_m_vec_m_vec$) > M$).
% 16.28/5.30 tff(times$l, type, times$l: (A_n_vec_set_set$ * A_n_vec_set_set$) > A_n_vec_set_set$).
% 16.28/5.30 tff(collect$c, type, collect$c: A_n_vec_bool_fun$ > A_n_vec_set$).
% 16.28/5.30 tff(reduced_row_echelon_form$c, type, reduced_row_echelon_form$c: A_n_vec_m_vec$ > $o).
% 16.28/5.30 tff(insert$b, type, insert$b: (A$ * A_set$) > A_set$).
% 16.28/5.30 tff('#skF_139', type, '#skF_139': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(vec_nth$a, type, vec_nth$a: A_m_vec_n_vec$ > N_a_m_vec_fun$).
% 16.28/5.30 tff(times$i, type, times$i: (A_m_vec_n_vec_set$ * A_m_vec_n_vec_set$) > A_m_vec_n_vec_set$).
% 16.28/5.30 tff(vec_nth$c, type, vec_nth$c: A_n_vec_n_vec$ > N_a_n_vec_fun$).
% 16.28/5.30 tff(vec_nth$f, type, vec_nth$f: (A_m_vec_n_vec_n_vec$ * N$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(column$a, type, column$a: (M$ * A_m_vec_m_vec$) > A_m_vec$).
% 16.28/5.30 tff(uuo$, type, uuo$: A_m_vec_a_m_vec_fun$).
% 16.28/5.30 tff(reduced_row_echelon_form$e, type, reduced_row_echelon_form$e: A_n_vec_n_vec$ > $o).
% 16.28/5.30 tff('#skF_107', type, '#skF_107': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff('#skF_46', type, '#skF_46': (A_m_vec_bool_fun$ * A_m_vec_bool_fun$) > A_m_vec$).
% 16.28/5.30 tff(map_matrix$b, type, map_matrix$b: (A_a_fun$ * A_n_vec_n_vec$) > A_n_vec_n_vec$).
% 16.28/5.30 tff(uxw$, type, uxw$: (A_n_vec_set$ * A_n_vec_set$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_86', type, '#skF_86': A_n_vec_bool_fun$ > A_n_vec$).
% 16.28/5.30 tff('#skF_91', type, '#skF_91': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff('#skF_109', type, '#skF_109': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(uxm$, type, uxm$: (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(uuu$, type, uuu$: (tlbool * N$ * N$) > N_bool_fun$).
% 16.28/5.30 tff('#skF_38', type, '#skF_38': (N_a_m_vec_bool_fun_fun$ * N$) > A_m_vec$).
% 16.28/5.30 tff(row$, type, row$: (N$ * A_m_vec_n_vec$) > A_m_vec$).
% 16.28/5.30 tff(map_matrix$c, type, map_matrix$c: (A_a_fun$ * A_m_vec_m_vec$) > A_m_vec_m_vec$).
% 16.28/5.30 tff(fun_app$y, type, fun_app$y: (A_m_vec_a_fun$ * A_m_vec$) > A$).
% 16.28/5.30 tff(column$e, type, column$e: (M$ * A_m_vec_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(member$d, type, member$d: (A_m_vec_n_vec$ * A_m_vec_n_vec_set$) > $o).
% 16.28/5.30 tff('#skF_79', type, '#skF_79': (A_n_vec_m_vec$ * M_a_n_vec_fun$) > M$).
% 16.28/5.30 tff(fun_app$x, type, fun_app$x: (M_a_m_vec_n_vec_fun$ * M$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(fun_app$ac, type, fun_app$ac: (N_a_n_vec_bool_fun_fun$ * N$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_132', type, '#skF_132': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(fun_app$r, type, fun_app$r: (N_a_n_vec_fun$ * N$) > A_n_vec$).
% 16.28/5.30 tff(uyh$, type, uyh$: (A$ * A_n_vec$) > N_a_fun$).
% 16.28/5.30 tff(zero$h, type, zero$h: A_m_vec_set$).
% 16.28/5.30 tff(mult_column_row$, type, mult_column_row$: (A_n_vec_m_vec$ * N$ * A$) > M_a_n_vec_fun$).
% 16.28/5.30 tff(uyf$, type, uyf$: (A$ * A_m_vec$) > M_a_fun$).
% 16.28/5.30 tff(column$c, type, column$c: (N$ * A_n_vec_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(member$e, type, member$e: (A_set$ * A_set_set$) > $o).
% 16.28/5.30 tff(vec_nth$j, type, vec_nth$j: (A_n_vec_n_vec_m_vec$ * M$) > A_n_vec_n_vec$).
% 16.28/5.30 tff('#skF_128', type, '#skF_128': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(uut$, type, uut$: (tlbool * A_n_vec$) > A_n_vec_a_n_vec_bool_fun_fun$).
% 16.28/5.30 tff('#skF_65', type, '#skF_65': (A_n_vec_bool_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(uvs$, type, uvs$: M_a_fun$).
% 16.28/5.30 tff(fun_app$j, 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$).
% 16.28/5.30 tff(mult_column_row$b, type, mult_column_row$b: (A_m_vec_m_vec$ * M$ * A$) > M_a_m_vec_fun$).
% 16.28/5.30 tff(uxf$, type, uxf$: A_m_vec_n_vec$ > A_n_vec_bool_fun$).
% 16.28/5.30 tff(uu$, type, uu$: N_bool_fun$).
% 16.28/5.30 tff('#skF_106', type, '#skF_106': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(fun_app$m, type, fun_app$m: (A_a_fun$ * A$) > A$).
% 16.28/5.30 tff(b$, type, b$: N$).
% 16.28/5.30 tff(uxv$, type, uxv$: (A_n_vec$ * A_n_vec_set$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(fun_app$aa, type, fun_app$aa: (M_a_m_vec_bool_fun_fun$ * M$) > A_m_vec_bool_fun$).
% 16.28/5.30 tff(zero$c, type, zero$c: A_m_vec_n_vec$).
% 16.28/5.30 tff(fun_app$ag, type, fun_app$ag: (A_a_n_vec_a_n_vec_fun_fun$ * A$) > A_n_vec_a_n_vec_fun$).
% 16.28/5.30 tff('#skF_73', type, '#skF_73': (N_bool_fun$ * N_bool_fun$ * N$) > N$).
% 16.28/5.30 tff(uwo$, type, uwo$: (A_m_vec_a_fun$ * A_m_vec_m_vec_n_vec$ * N$) > M_a_fun$).
% 16.28/5.30 tff('#skF_45', type, '#skF_45': (A_m_vec_bool_fun$ * A_m_vec_bool_fun$) > A_m_vec$).
% 16.28/5.30 tff('#skF_4', type, '#skF_4': (A_n_vec_m_vec$ * A_m_vec$) > M$).
% 16.28/5.30 tff('#skF_161', type, '#skF_161': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_41', type, '#skF_41': (A_n_vec_bool_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(x$, type, x$: A_n_vec$).
% 16.28/5.30 tff('#skF_15', type, '#skF_15': (A_m_vec$ * A_m_vec$) > M$).
% 16.28/5.30 tff(uxn$, type, uxn$: (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_62', type, '#skF_62': (A$ * A_set$ * A_set$) > A$).
% 16.28/5.30 tff(fun_app$c, type, fun_app$c: (N_bool_fun$ * N$) > $o).
% 16.28/5.30 tff(uuj$, type, uuj$: A_set$ > A_bool_fun$).
% 16.28/5.30 tff('#skF_21', type, '#skF_21': (M_a_n_vec_bool_fun_fun$ * A_n_vec_m_vec$) > M$).
% 16.28/5.30 tff(times$a, type, times$a: A_n_vec_a_n_vec_a_n_vec_fun_fun$).
% 16.28/5.30 tff(uvh$, type, uvh$: (A_m_vec$ * A_m_vec$) > M_a_fun$).
% 16.28/5.30 tff('#skF_29', type, '#skF_29': (N_a_bool_fun_fun$ * A_n_vec$) > N$).
% 16.28/5.30 tff('#skF_120', type, '#skF_120': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(vec_nth$k, type, vec_nth$k: (A_n_vec_n_vec_n_vec$ * N$) > A_n_vec_n_vec$).
% 16.28/5.30 tff('#skF_143', type, '#skF_143': (A_n_vec_set_bool_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(uwl$, type, uwl$: (A_a_fun$ * A_n_vec_n_vec$) > N_a_n_vec_fun$).
% 16.28/5.30 tff(uvu$, type, uvu$: (A_m_vec_m_vec$ * M$ * A$ * M$) > M_a_fun$).
% 16.28/5.30 tff(fun_app$ae, type, fun_app$ae: (M_a_bool_fun_fun$ * M$) > A_bool_fun$).
% 16.28/5.30 tff(uxa$, type, uxa$: (A_n_vec_m_vec$ * M$) > N_bool_fun$).
% 16.28/5.30 tff(reduced_row_echelon_form$d, type, reduced_row_echelon_form$d: A_m_vec_m_vec$ > $o).
% 16.28/5.30 tff(fun_app$n, type, fun_app$n: (A_a_a_fun_fun$ * A$) > A_a_fun$).
% 16.28/5.30 tff(vec_nth$i, type, vec_nth$i: (A_m_vec_n_vec_m_vec$ * M$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(reduced_row_echelon_form$b, type, reduced_row_echelon_form$b: A_n_vec_n_vec_m_vec$ > $o).
% 16.28/5.30 tff(vec_nth$, type, vec_nth$: A_m_vec$ > M_a_fun$).
% 16.28/5.30 tff('#skF_43', type, '#skF_43': (A_n_vec_bool_fun$ * A_n_vec$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(uxp$, type, uxp$: (A_n_vec_bool_fun$ * A_n_vec_a_n_vec_bool_fun_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_164', type, '#skF_164': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_18', type, '#skF_18': (M_a_m_vec_bool_fun_fun$ * M$) > A_m_vec$).
% 16.28/5.30 tff(one$, type, one$: A$).
% 16.28/5.30 tff(vec_nth$g, type, vec_nth$g: (A_m_vec_m_vec_n_vec$ * N$) > A_m_vec_m_vec$).
% 16.28/5.30 tff(mult_column$, type, mult_column$: (A_m_vec_n_vec$ * M$ * A$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_39', type, '#skF_39': N_a_m_vec_bool_fun_fun$ > N$).
% 16.28/5.30 tff('#skF_111', type, '#skF_111': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(minus$e, type, minus$e: (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(column$, type, column$: (M$ * A_m_vec_n_vec$) > A_n_vec$).
% 16.28/5.30 tff('#skF_172', type, '#skF_172': (A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff(the$a, type, the$a: A_n_vec_bool_fun$ > A_n_vec$).
% 16.28/5.30 tff('#skF_129', type, '#skF_129': (A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(minus$a, type, minus$a: A$ > A_a_fun$).
% 16.28/5.30 tff(column$f, type, column$f: (N$ * A_n_vec_n_vec_n_vec$) > A_n_vec_n_vec$).
% 16.28/5.30 tff('#skF_55', type, '#skF_55': (A_set$ * A_set_set$ * A_set_set$) > A_set$).
% 16.28/5.30 tff(is_zero_row$, type, is_zero_row$: (N$ * A_m_vec_n_vec$) > $o).
% 16.28/5.30 tff(uux$, type, uux$: A_m_vec_n_vec$ > A_m_vec_n_vec_a_m_vec_n_vec_fun$).
% 16.28/5.30 tff('#skF_110', type, '#skF_110': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(column$d, type, column$d: (N$ * A_m_vec_n_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(uuz$, type, uuz$: A_n_vec_a_n_vec_a_n_vec_fun_fun$).
% 16.28/5.30 tff('#skF_16', type, '#skF_16': (A_m_vec_n_vec$ * A_m_vec_n_vec$) > N$).
% 16.28/5.30 tff('#skF_14', type, '#skF_14': (A_n_vec$ * A_n_vec$) > N$).
% 16.28/5.30 tff('#skF_26', type, '#skF_26': (N_a_n_vec_bool_fun_fun$ * N$) > A_n_vec$).
% 16.28/5.30 tff('#skF_108', type, '#skF_108': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_28', type, '#skF_28': N_a_n_vec_bool_fun_fun$ > A_n_vec_n_vec$).
% 16.28/5.30 tff(bot$b, type, bot$b: A_set$).
% 16.28/5.30 tff(uwq$, type, uwq$: (A_n_vec_a_fun$ * A_n_vec_m_vec_n_vec$ * N$) > M_a_fun$).
% 16.28/5.30 tff(zero$k, type, zero$k: M$).
% 16.28/5.30 tff('#skF_75', type, '#skF_75': N$).
% 16.28/5.30 tff(fun_app$a, type, fun_app$a: (M_a_fun$ * M$) > A$).
% 16.28/5.30 tff(interchange_rows$, type, interchange_rows$: (A_m_vec_n_vec$ * N$ * N$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_104', type, '#skF_104': A_n_vec_set_set$ > A_n_vec_set$).
% 16.28/5.30 tff('#skF_148', type, '#skF_148': (A_n_vec_set_bool_fun$ * A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(uul$, type, uul$: A_n_vec_set_set$ > A_n_vec_set_bool_fun$).
% 16.28/5.30 tff(fun_app$b, type, fun_app$b: (N_a_m_vec_fun$ * N$) > A_m_vec$).
% 16.28/5.30 tff(one$h, type, one$h: A_n_vec_n_vec$).
% 16.28/5.30 tff(uym$, type, uym$: (A_m_vec_n_vec$ * N$ * N$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(times$b, type, times$b: A_m_vec$ > A_m_vec_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_42', type, '#skF_42': (N_bool_fun$ * N$) > N$).
% 16.28/5.30 tff('#skF_47', type, '#skF_47': (A_n_vec_set_bool_fun$ * A_n_vec_set_bool_fun$) > A_n_vec_set$).
% 16.28/5.30 tff(fun_app$z, type, fun_app$z: (A_a_m_vec_fun$ * A$) > A_m_vec$).
% 16.28/5.30 tff(insert$a, type, insert$a: (N$ * N_set$) > N_set$).
% 16.28/5.30 tff(column$g, type, column$g: (N$ * A_n_vec_n_vec_m_vec$) > A_n_vec_m_vec$).
% 16.28/5.30 tff(interchange_columns$, type, interchange_columns$: (A_m_vec_n_vec$ * M$ * M$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(uxe$, type, uxe$: (A_m_vec_n_vec$ * N$) > M_bool_fun$).
% 16.28/5.30 tff(less_eq$a, type, less_eq$a: (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > $o).
% 16.28/5.30 tff(vec_lambda$c, type, vec_lambda$c: M_a_m_vec_fun$ > A_m_vec_m_vec$).
% 16.28/5.30 tff('#skF_117', type, '#skF_117': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff('#skF_96', type, '#skF_96': (A_n_vec$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(less_eq$c, type, less_eq$c: (A_set$ * A_set$) > $o).
% 16.28/5.30 tff('#skF_95', type, '#skF_95': (A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff(a$, type, a$: A_m_vec_n_vec$).
% 16.28/5.30 tff(uvd$, type, uvd$: (A_m_vec_m_vec$ * A_m_vec_m_vec$) > M_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_12', type, '#skF_12': (A_n_vec_m_vec$ * A_n_vec_m_vec$) > M$).
% 16.28/5.30 tff(map_matrix$h, type, map_matrix$h: (A_m_vec_a_fun$ * A_m_vec_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_152', type, '#skF_152': (M_bool_fun$ * M_bool_fun$) > M$).
% 16.28/5.30 tff('#skF_54', type, '#skF_54': (A_m_vec$ * A_m_vec_set$ * A_m_vec_set$) > A_m_vec$).
% 16.28/5.30 tff('#skF_31', type, '#skF_31': N_a_bool_fun_fun$ > N$).
% 16.28/5.30 tff(one$f, type, one$f: A_m_vec_m_vec$).
% 16.28/5.30 tff('#skF_24', type, '#skF_24': M_a_n_vec_bool_fun_fun$ > A_n_vec_m_vec$).
% 16.28/5.30 tff('#skF_145', type, '#skF_145': (M_bool_fun$ * M$ * M_bool_fun$) > M$).
% 16.28/5.30 tff(the_elem$a, type, the_elem$a: A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff(times$d, type, times$d: A_set$ > A_set_a_set_fun$).
% 16.28/5.30 tff('#skF_20', type, '#skF_20': M_a_m_vec_bool_fun_fun$ > A_m_vec_m_vec$).
% 16.28/5.30 tff('#skF_157', type, '#skF_157': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_11', type, '#skF_11': (A_m_vec_m_vec$ * A_m_vec_m_vec$) > M$).
% 16.28/5.30 tff('#skF_137', type, '#skF_137': (M_bool_fun$ * M$) > M$).
% 16.28/5.30 tff(uyk$, type, uyk$: (A_n_vec_a_fun$ * A_n_vec_set$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(fun_app$p, type, fun_app$p: (A_bool_fun$ * A$) > $o).
% 16.28/5.30 tff(times$g, type, times$g: (A_n_vec_m_vec$ * A_n_vec_m_vec$) > A_n_vec_m_vec$).
% 16.28/5.30 tff(uxx$, 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$).
% 16.28/5.30 tff(uuf$, type, uuf$: A_n_vec_a_n_vec_bool_fun_fun$).
% 16.28/5.30 tff(uuw$, type, uuw$: M_bool_fun$).
% 16.28/5.30 tff(minus$c, type, minus$c: A_n_vec_a_n_vec_a_n_vec_fun_fun$).
% 16.28/5.30 tff(fun_app$af, type, fun_app$af: (N_a_m_vec_bool_fun_fun$ * N$) > A_m_vec_bool_fun$).
% 16.28/5.30 tff(uwu$, type, uwu$: M_a_fun$).
% 16.28/5.30 tff(zero$e, type, zero$e: A_n_vec_m_vec$).
% 16.28/5.30 tff(uya$, type, uya$: (A_n_vec$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(collect$b, type, collect$b: A_n_vec_set_bool_fun$ > A_n_vec_set_set$).
% 16.28/5.30 tff(mult_row_row$c, type, mult_row_row$c: (A_m_vec_n_vec$ * N$ * A$) > N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_67', type, '#skF_67': (A_n_vec_bool_fun$ * A_n_vec$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(uun$, type, uun$: A_m_vec_n_vec_a_m_vec_n_vec_fun$).
% 16.28/5.30 tff(uwi$, type, uwi$: (A_a_fun$ * A_n_vec_m_vec$ * M$) > N_a_fun$).
% 16.28/5.30 tff(uxu$, type, uxu$: (A_n_vec$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(zero$d, type, zero$d: A_m_vec_m_vec$).
% 16.28/5.30 tff(uyl$, type, uyl$: (A_n_vec_a_m_vec_fun$ * A_n_vec_set$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff('#skF_23', type, '#skF_23': M_a_n_vec_bool_fun_fun$ > M$).
% 16.28/5.30 tff(uxs$, type, uxs$: (A_n_vec_set$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(fun_app$i, type, fun_app$i: (A_n_vec_a_n_vec_fun$ * A_n_vec$) > A_n_vec$).
% 16.28/5.30 tff('#skF_57', type, '#skF_57': (A_n_vec_set$ * A_n_vec_set_set$ * A_n_vec_set_set$) > A_n_vec_set$).
% 16.28/5.30 tff(is_singleton$, type, is_singleton$: A_n_vec_set_bool_fun$).
% 16.28/5.30 tff('#skF_138', type, '#skF_138': (M_bool_fun$ * M$) > M$).
% 16.28/5.30 tff(map_matrix$i, type, map_matrix$i: (A_n_vec_a_fun$ * A_n_vec_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_35', type, '#skF_35': M_a_bool_fun_fun$ > M$).
% 16.28/5.30 tff(uvj$, type, uvj$: N$ > M_bool_fun$).
% 16.28/5.30 tff('#skF_140', type, '#skF_140': (A_n_vec_set_bool_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(fun_app$d, type, fun_app$d: (N_a_fun$ * N$) > A$).
% 16.28/5.30 tff(times$k, type, times$k: (A_set_set$ * A_set_set$) > A_set_set$).
% 16.28/5.30 tff('#skF_3', type, '#skF_3': (A_m_vec_m_vec$ * A_m_vec$) > M$).
% 16.28/5.30 tff(uva$, type, uva$: A_set$ > A_set_a_set_fun$).
% 16.28/5.30 tff(uwg$, type, uwg$: (A_a_fun$ * A_m_vec_m_vec$ * M$) > M_a_fun$).
% 16.28/5.30 tff('#skF_158', type, '#skF_158': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_170', type, '#skF_170': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff('#skF_160', type, '#skF_160': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.30 tff(column$b, type, column$b: (N$ * A_n_vec_m_vec$) > A_m_vec$).
% 16.28/5.30 tff(uwf$, type, uwf$: (A_a_m_vec_fun$ * A_n_vec_n_vec$) > N_a_m_vec_n_vec_fun$).
% 16.28/5.30 tff(vec_nth$e, type, vec_nth$e: A_m_vec_m_vec$ > M_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_36', type, '#skF_36': M_a_bool_fun_fun$ > A_m_vec$).
% 16.28/5.30 tff('#skF_134', type, '#skF_134': (A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(finite$, type, finite$: A_n_vec_set_bool_fun$).
% 16.28/5.30 tff('#skF_162', type, '#skF_162': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.30 tff(uvr$, type, uvr$: N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_153', type, '#skF_153': (N$ * A_m_vec_n_vec$) > M$).
% 16.28/5.30 tff(uyi$, type, uyi$: (A_n_vec_set$ * A_n_vec_a_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(tltrue, type, tltrue: tlbool).
% 16.28/5.30 tff(least$a, type, least$a: N_bool_fun$ > N$).
% 16.28/5.30 tff(uxz$, type, uxz$: (A_n_vec$ * A_n_vec_bool_fun$) > A_n_vec_bool_fun$).
% 16.28/5.30 tff(one$e, type, one$e: A_n_vec_set$).
% 16.28/5.30 tff(uxr$, type, uxr$: A_n_vec_bool_fun$).
% 16.28/5.30 tff(uwj$, type, uwj$: (A_a_fun$ * A_n_vec_m_vec$) > M_a_n_vec_fun$).
% 16.28/5.30 tff('#skF_56', type, '#skF_56': (A_set$ * A_set_set$ * A_set_set$) > A_set$).
% 16.28/5.30 tff('#skF_99', type, '#skF_99': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_n_vec_bool_fun_fun$) > A_n_vec$).
% 16.28/5.30 tff(the_elem$, type, the_elem$: N_set$ > N$).
% 16.28/5.30 tff(fun_app$w, type, fun_app$w: (N_a_m_vec_n_vec_fun$ * N$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(times$h, type, times$h: (A_n_vec_n_vec$ * A_n_vec_n_vec$) > A_n_vec_n_vec$).
% 16.28/5.30 tff(uvq$, type, uvq$: (M$ * A_m_vec_n_vec$) > N_a_fun$).
% 16.28/5.30 tff(uwn$, type, uwn$: (A_a_fun$ * A_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(uwr$, type, uwr$: (A_n_vec_a_fun$ * A_n_vec_m_vec_n_vec$) > N_a_m_vec_fun$).
% 16.28/5.30 tff(vec_lambda$g, type, vec_lambda$g: N_a_m_vec_n_vec_fun$ > A_m_vec_n_vec_n_vec$).
% 16.28/5.30 tff('#skF_76', type, '#skF_76': N$).
% 16.28/5.30 tff('#skF_70', type, '#skF_70': (N_bool_fun$ * N$ * N_bool_fun$) > N$).
% 16.28/5.30 tff(sum$a, type, sum$a: (A_n_vec_a_m_vec_fun$ * A_n_vec_set$) > A_m_vec$).
% 16.28/5.30 tff('#skF_53', type, '#skF_53': (A_m_vec$ * A_m_vec_set$ * A_m_vec_set$) > A_m_vec$).
% 16.28/5.30 tff(fun_app$o, type, fun_app$o: (A_m_vec_bool_fun$ * A_m_vec$) > $o).
% 16.28/5.30 tff('#skF_93', type, '#skF_93': (A_n_vec_bool_fun$ * A_n_vec_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff(vec_lambda$f, type, vec_lambda$f: M_a_m_vec_n_vec_fun$ > A_m_vec_n_vec_m_vec$).
% 16.28/5.30 tff(mult_row_row$, type, mult_row_row$: (A_n_vec_m_vec$ * M$ * A$) > M_a_n_vec_fun$).
% 16.28/5.30 tff(uve$, type, uve$: (A_n_vec_m_vec$ * A_n_vec_m_vec$) > M_a_n_vec_fun$).
% 16.28/5.30 tff('#skF_98', type, '#skF_98': (A_n_vec$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_25', type, '#skF_25': (N_a_n_vec_bool_fun_fun$ * A_n_vec_n_vec$) > N$).
% 16.28/5.30 tff('#skF_5', type, '#skF_5': (A_n_vec_n_vec$ * A_n_vec$) > N$).
% 16.28/5.30 tff('#skF_77', type, '#skF_77': A_n_vec$).
% 16.28/5.30 tff(less_eq$b, type, less_eq$b: M$ > M_bool_fun$).
% 16.28/5.30 tff('#skF_122', type, '#skF_122': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_52', type, '#skF_52': (A_m_vec_n_vec$ * A_m_vec_n_vec_set$ * A_m_vec_n_vec_set$) > A_m_vec_n_vec$).
% 16.28/5.30 tff(vec_lambda$, type, vec_lambda$: M_a_fun$ > A_m_vec$).
% 16.28/5.30 tff(uxg$, type, uxg$: (A_m_vec_n_vec$ * M$ * A$) > N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_88', type, '#skF_88': (A_n_vec_set$ * A_n_vec_set$) > A_n_vec$).
% 16.28/5.30 tff(times$c, type, times$c: A_n_vec_set$ > A_n_vec_set_a_n_vec_set_fun$).
% 16.28/5.30 tff(insert$, type, insert$: A_n_vec$ > A_n_vec_set_a_n_vec_set_fun$).
% 16.28/5.30 tff('#skF_69', type, '#skF_69': (N_bool_fun$ * N$ * N_bool_fun$) > N$).
% 16.28/5.30 tff(vector_scalar_mult$a, type, vector_scalar_mult$a: A_a_m_vec_a_m_vec_fun_fun$).
% 16.28/5.30 tff(vec_lambda$e, type, vec_lambda$e: N_a_n_vec_fun$ > A_n_vec_n_vec$).
% 16.28/5.30 tff(zero$j, type, zero$j: N$).
% 16.28/5.30 tff('#skF_10', type, '#skF_10': (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$).
% 16.28/5.30 tff(collect$a, type, collect$a: A_m_vec_bool_fun$ > A_m_vec_set$).
% 16.28/5.30 tff(row$c, type, row$c: (N$ * A_n_vec_n_vec$) > A_n_vec$).
% 16.28/5.30 tff(minus$b, type, minus$b: A_n_vec_set$ > A_n_vec_set_a_n_vec_set_fun$).
% 16.28/5.30 tff('#skF_171', type, '#skF_171': A_n_vec_set$ > A_n_vec$).
% 16.28/5.30 tff('#skF_61', type, '#skF_61': (A$ * A_set$ * A_set$) > A$).
% 16.28/5.30 tff(uxk$, type, uxk$: (A_m_vec$ * A_m_vec$) > M_a_fun$).
% 16.28/5.30 tff(member$c, type, member$c: (A$ * A_set$) > $o).
% 16.28/5.30 tff(uwc$, type, uwc$: (A_a_m_vec_fun$ * A_n_vec_m_vec$ * M$) > N_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_83', type, '#skF_83': (A_m_vec_n_vec$ * N_a_m_vec_fun$) > N$).
% 16.28/5.30 tff('#skF_6', type, '#skF_6': (A_m_vec_n_vec$ * A_m_vec$) > N$).
% 16.28/5.30 tff(fun_app$l, type, fun_app$l: (A_set_a_set_fun$ * A_set$) > A_set$).
% 16.28/5.30 tff(row$b, type, row$b: (M$ * A_n_vec_m_vec$) > A_n_vec$).
% 16.28/5.30 tff(bot$c, type, bot$c: A_m_vec_set$).
% 16.28/5.30 tff(uvf$, type, uvf$: (A_n_vec_n_vec$ * A_n_vec_n_vec$) > N_a_n_vec_fun$).
% 16.28/5.30 tff(finite$a, type, finite$a: A_set$ > $o).
% 16.28/5.30 tff(uwt$, type, uwt$: N_a_fun$).
% 16.28/5.30 tff('#skF_156', type, '#skF_156': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_fun$ * A_n_vec_a_fun$) > A_n_vec$).
% 16.28/5.30 tff(vector_scalar_mult$b, type, vector_scalar_mult$b: (A_m_vec$ * A_m_vec_n_vec$) > A_m_vec_n_vec$).
% 16.28/5.30 tff('#skF_131', type, '#skF_131': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff('#skF_112', type, '#skF_112': (A_n_vec_set$ * A_n_vec_set_bool_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_165', type, '#skF_165': (A_n_vec_set$ * A_n_vec_set$ * A_n_vec_a_m_vec_fun$) > A_n_vec$).
% 16.28/5.30 tff('#skF_130', type, '#skF_130': (A_n_vec_set$ * A_n_vec_set_a_n_vec_set_fun$ * A_n_vec_set$ * A_n_vec_set$) > A_n_vec_set$).
% 16.28/5.30 tff(minus$, type, minus$: A_m_vec$ > A_m_vec_a_m_vec_fun$).
% 16.28/5.30 tff('#skF_64', type, '#skF_64': (N_bool_fun$ * N$) > N$).
% 16.28/5.30
% 16.28/5.30 tff(f_2025, axiom, (![A__questionmark_v0:A$]: (uvc$(A__questionmark_v0) = fun_app$n(times$e, A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom348)).
% 16.28/5.30 tff(f_1417, axiom, (![A__questionmark_v0:A$, A__questionmark_v1:A$]: ((fun_app$m(fun_app$n(times$e, A__questionmark_v0), A__questionmark_v1) = A__questionmark_v0) <=> ((A__questionmark_v0 = zero$) | (A__questionmark_v1 = one$)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom250)).
% 16.28/5.30 tff(f_674, axiom, (b$ = i$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom121)).
% 16.28/5.30 tff(f_669, axiom, (fun_app$d(vec_nth$b(xa$), i$) = zero$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom119)).
% 16.28/5.30 tff(f_1610, axiom, (![A__questionmark_v0:A$, A__questionmark_v1:A$]: (fun_app$m(fun_app$n(times$e, A__questionmark_v0), A__questionmark_v1) = fun_app$m(fun_app$n(times$e, A__questionmark_v1), A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom305)).
% 16.28/5.30 tff(f_667, negated_conjecture, ~(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$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture118)).
% 16.28/5.30 tff(c_1248, plain, (![A__questionmark_v0_987:A$]: (fun_app$n(times$e, A__questionmark_v0_987)=uvc$(A__questionmark_v0_987))), inference(cnfTransformation, [status(thm)], [f_2025])).
% 16.28/5.30 tff(c_880, plain, (![A__questionmark_v1_758:A$]: (fun_app$m(fun_app$n(times$e, zero$), A__questionmark_v1_758)=zero$)), inference(cnfTransformation, [status(thm)], [f_1417])).
% 16.28/5.30 tff(c_2921, plain, (![A__questionmark_v1_758:A$]: (fun_app$m(uvc$(zero$), A__questionmark_v1_758)=zero$)), inference(demodulation, [status(thm), theory('equality')], [c_1248, c_880])).
% 16.28/5.30 tff(c_430, plain, (i$=b$), inference(cnfTransformation, [status(thm)], [f_674])).
% 16.28/5.30 tff(c_426, plain, (fun_app$d(vec_nth$b(xa$), i$)=zero$), inference(cnfTransformation, [status(thm)], [f_669])).
% 16.28/5.30 tff(c_2991, plain, (fun_app$d(vec_nth$b(xa$), b$)=zero$), inference(demodulation, [status(thm), theory('equality')], [c_430, c_426])).
% 16.28/5.30 tff(c_1050, plain, (![A__questionmark_v1_835:A$, A__questionmark_v0_834:A$]: (fun_app$m(fun_app$n(times$e, A__questionmark_v1_835), A__questionmark_v0_834)=fun_app$m(fun_app$n(times$e, A__questionmark_v0_834), A__questionmark_v1_835))), inference(cnfTransformation, [status(thm)], [f_1610])).
% 16.28/5.30 tff(c_2888, plain, (![A__questionmark_v1_835:A$, A__questionmark_v0_834:A$]: (fun_app$m(uvc$(A__questionmark_v1_835), A__questionmark_v0_834)=fun_app$m(uvc$(A__questionmark_v0_834), A__questionmark_v1_835))), inference(demodulation, [status(thm), theory('equality')], [c_1248, c_1248, c_1050])).
% 16.28/5.30 tff(c_424, plain, (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$), inference(cnfTransformation, [status(thm)], [f_667])).
% 16.28/5.30 tff(c_2993, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_2921, c_2991, c_2888, c_1248, c_430, c_424])).
% 16.28/5.30 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------