%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP001_1 : TPTP v9.0.0. Released v8.1.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:40 PM UTC 2025
% Result : Theorem 13.07s 4.06s
% Output : CNFRefutation 13.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : ITP001_1 : TPTP v9.0.0. Released v8.1.0.
% 0.12/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.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 02:18:39 EDT 2025
% 0.13/0.34 % CPUTime :
% 13.07/4.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.80/4.17
% 13.80/4.17 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.87/4.19 %$ fun_app$x > fun_app$s > fun_app$p > fun_app$n > fun_app$k > fun_app$j > fun_app$i > fun_app$h > fun_app$g > fun_app$f > fun_app$e > fun_app$d > fun_app$c > gauss_Jordan_in_ij_iarrays_PA$ > foldl$a > foldl$ > upt$ > plus$l > plus$k > plus$j > plus$i > plus$h > plus$g > plus$f > plus$e > plus$d > plus$c > plus$b > plus$a > pair$l > pair$k > pair$j > pair$i > pair$h > pair$g > pair$f > pair$e > pair$d > pair$c > pair$b > pair$a > pair$ > mat_iarray$ > gauss_Jordan_upt_k_iarrays_PA$ > gauss_Jordan_upt_k_PA$ > gauss_Jordan_column_k_PA$a > fun_app$z > fun_app$y > fun_app$w > fun_app$v > fun_app$u > fun_app$t > fun_app$r > fun_app$q > fun_app$o > fun_app$m > fun_app$l > fun_app$b > fun_app$a > fun_app$ > column_iarray$ > #nlpp > snd$l > snd$k > snd$j > snd$i > snd$h > snd$g > snd$f > snd$e > snd$d > snd$c > snd$b > snd$a > snd$ > plus$ > nrows_iarray$ > nrows$a > nrows$ > ncols$a > ncols$ > nat$ > matrix_to_iarray$a > matrix_to_iarray$ > mat$ > fst$l > fst$k > fst$j > fst$i > fst$h > fst$g > fst$f > fst$e > fst$d > fst$c > fst$b > fst$a > fst$ > zero$j > zero$i > zero$h > zero$g > zero$f > zero$e > zero$d > zero$c > zero$b > zero$a > zero$ > vector_all_zero_from_index$ > tltrue > tlfalse > suc$ > one$a > one$ > of_nat$ > less_eq$ > less$ > ka$ > k$ > gauss_Jordan_column_k_iarrays_PA$ > gauss_Jordan_column_k_PA$ > divides_aux$ > b$ > a$a > a$ > #skF_123 > #skF_80 > #skF_95 > #skF_67 > #skF_140 > #skF_119 > #skF_92 > #skF_21 > #skF_124 > #skF_37 > #skF_18 > #skF_148 > #skF_40 > #skF_51 > #skF_59 > #skF_86 > #skF_58 > #skF_36 > #skF_33 > #skF_96 > #skF_112 > #skF_113 > #skF_146 > #skF_109 > #skF_35 > #skF_120 > #skF_10 > #skF_11 > #skF_149 > #skF_38 > #skF_1 > #skF_48 > #skF_3 > #skF_137 > #skF_57 > #skF_116 > #skF_56 > #skF_135 > #skF_15 > #skF_75 > #skF_90 > #skF_87 > #skF_31 > #skF_132 > #skF_139 > #skF_134 > #skF_54 > #skF_153 > #skF_12 > #skF_91 > #skF_23 > #skF_103 > #skF_130 > #skF_94 > #skF_32 > #skF_125 > #skF_126 > #skF_154 > #skF_73 > #skF_7 > #skF_129 > #skF_41 > #skF_19 > #skF_14 > #skF_53 > #skF_111 > #skF_78 > #skF_22 > #skF_6 > #skF_133 > #skF_84 > #skF_46 > #skF_72 > #skF_97 > #skF_45 > #skF_16 > #skF_70 > #skF_63 > #skF_102 > #skF_52 > #skF_93 > #skF_8 > #skF_152 > #skF_4 > #skF_17 > #skF_127 > #skF_5 > #skF_108 > #skF_151 > #skF_43 > #skF_110 > #skF_79 > #skF_114 > #skF_98 > #skF_62 > #skF_13 > #skF_117 > #skF_100 > #skF_150 > #skF_65 > #skF_34 > #skF_115 > #skF_42 > #skF_49 > #skF_89 > #skF_74 > #skF_106 > #skF_66 > #skF_47 > #skF_145 > #skF_55 > #skF_61 > #skF_141 > #skF_2 > #skF_83 > #skF_128 > #skF_64 > #skF_39 > #skF_122 > #skF_101 > #skF_82 > #skF_25 > #skF_105 > #skF_121 > #skF_81 > #skF_20 > #skF_27 > #skF_144 > #skF_69 > #skF_9 > #skF_88 > #skF_131 > #skF_29 > #skF_85 > #skF_104 > #skF_77 > #skF_24 > #skF_50 > #skF_138 > #skF_147 > #skF_136 > #skF_76 > #skF_28 > #skF_60 > #skF_107 > #skF_44 > #skF_99 > #skF_30 > #skF_143 > #skF_68 > #skF_26 > #skF_71 > #skF_142 > #skF_118
% 13.87/4.19
% 13.87/4.19 %Foreground sorts:
% 13.87/4.19 tff(A_iarray_iarray_nat_a_iarray_iarray_prod_bool_fun_fun$, type, A_iarray_iarray_nat_a_iarray_iarray_prod_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(A$, type, A$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$, type, A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$: $tType ).
% 13.87/4.19 tff(Nat_nat_bool_fun_fun$, type, Nat_nat_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_iarray_prod_bool_fun$, type, Nat_a_iarray_iarray_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat$, type, Nat$: $tType ).
% 13.87/4.19 tff(Nat_a_c_vec_c_vec_prod$, type, Nat_a_c_vec_c_vec_prod$: $tType ).
% 13.87/4.19 tff(Int_nat_prod$, type, Int_nat_prod$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$, type, A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$: $tType ).
% 13.87/4.19 tff(Nat_list$, type, Nat_list$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$, type, A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(tlbool, type, tlbool: $tType ).
% 13.87/4.19 tff(Int_int_prod$, type, Int_int_prod$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_iarray_bool_fun_fun$, type, Nat_a_iarray_iarray_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(Int_int_fun$, type, Int_int_fun$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_nat_a_iarray_iarray_prod_prod$, type, A_iarray_iarray_nat_a_iarray_iarray_prod_prod$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_a_iarray_iarray_prod$, type, A_iarray_iarray_a_iarray_iarray_prod$: $tType ).
% 13.87/4.19 tff(Nat_nat_fun$, type, Nat_nat_fun$: $tType ).
% 13.87/4.19 tff(Nat_int_fun$, type, Nat_int_fun$: $tType ).
% 13.87/4.19 tff(Int_int_prod_bool_fun$, type, Int_int_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(A_b_vec_c_vec_bool_fun$, type, A_b_vec_c_vec_bool_fun$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec$, type, A_c_vec_c_vec$: $tType ).
% 13.87/4.19 tff(A_iarray$, type, A_iarray$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_nat_a_iarray_iarray_prod_prod_nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun_fun$, type, A_iarray_iarray_nat_a_iarray_iarray_prod_prod_nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun_fun$: $tType ).
% 13.87/4.19 tff(Nat_nat_prod_bool_fun$, type, Nat_nat_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(Int_int_bool_fun_fun$, type, Int_int_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(A_b_vec_c_vec$, type, A_b_vec_c_vec$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_bool_fun$, type, A_iarray_iarray_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_b_vec_c_vec_prod$, type, Nat_a_b_vec_c_vec_prod$: $tType ).
% 13.87/4.19 tff(Nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun$, type, Nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun$: $tType ).
% 13.87/4.19 tff(Nat_bool_fun$, type, Nat_bool_fun$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray_a_iarray_iarray_bool_fun_fun$, type, A_iarray_iarray_a_iarray_iarray_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(Int_nat_prod_bool_fun$, type, Int_nat_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_iarray_prod$, type, Nat_a_iarray_iarray_prod$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_prod$, type, Nat_a_iarray_prod$: $tType ).
% 13.87/4.19 tff(A_iarray_iarray$, type, A_iarray_iarray$: $tType ).
% 13.87/4.19 tff(Nat_nat_prod$, type, Nat_nat_prod$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_bool_fun_fun$, type, A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_prod_bool_fun$, type, Nat_a_iarray_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun_fun$, type, A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun_fun$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_a_b_vec_c_vec_prod$, type, A_c_vec_c_vec_a_b_vec_c_vec_prod$: $tType ).
% 13.87/4.19 tff(Nat_a_b_vec_c_vec_bool_fun_fun$, type, Nat_a_b_vec_c_vec_bool_fun_fun$: $tType ).
% 13.87/4.19 tff(A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$, type, A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_b_vec_c_vec_prod_bool_fun$, type, Nat_a_b_vec_c_vec_prod_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun$, type, Nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun$: $tType ).
% 13.87/4.19 tff(Int_bool_fun$, type, Int_bool_fun$: $tType ).
% 13.87/4.19 tff(Nat_int_prod$, type, Nat_int_prod$: $tType ).
% 13.87/4.19 tff(Nat_int_prod_bool_fun$, type, Nat_int_prod_bool_fun$: $tType ).
% 13.87/4.19
% 13.87/4.19 %Background operators:
% 13.87/4.19
% 13.87/4.19
% 13.87/4.19 %Foreground operators:
% 13.87/4.19 tff(fun_app$p, type, fun_app$p: (A_b_vec_c_vec_bool_fun$ * A_b_vec_c_vec$) > $o).
% 13.87/4.19 tff(zero$, type, zero$: A$).
% 13.87/4.19 tff('#skF_123', type, '#skF_123': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_80', type, '#skF_80': (Nat$ * Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff(pair$j, type, pair$j: (A_c_vec_c_vec$ * Nat_a_c_vec_c_vec_prod$) > A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$).
% 13.87/4.19 tff('#skF_95', type, '#skF_95': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff(snd$l, type, snd$l: A_c_vec_c_vec_a_b_vec_c_vec_prod$ > A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_67', type, '#skF_67': (Nat$ * Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_140', type, '#skF_140': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_119', type, '#skF_119': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(zero$e, type, zero$e: Nat_nat_prod$).
% 13.87/4.19 tff('#skF_92', type, '#skF_92': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fun_app$x, type, fun_app$x: (Int_bool_fun$ * $int) > $o).
% 13.87/4.19 tff('#skF_21', type, '#skF_21': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff(pair$b, type, pair$b: (Nat$ * A_iarray_iarray$) > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff(zero$h, type, zero$h: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff(zero$a, type, zero$a: A_c_vec_c_vec$).
% 13.87/4.19 tff(zero$i, type, zero$i: Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_124', type, '#skF_124': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_37', type, '#skF_37': (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_18', type, '#skF_18': (Nat_a_iarray_iarray_prod_bool_fun$ * Nat_a_iarray_iarray_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_148', type, '#skF_148': (Nat_nat_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_40', type, '#skF_40': (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_51', type, '#skF_51': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(snd$e, type, snd$e: Nat_nat_prod$ > Nat$).
% 13.87/4.19 tff(fun_app$j, type, fun_app$j: (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > $o).
% 13.87/4.19 tff('#skF_59', type, '#skF_59': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_86', type, '#skF_86': (Nat_nat_bool_fun_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fun_app$e, type, fun_app$e: (Nat_int_prod_bool_fun$ * Nat_int_prod$) > $o).
% 13.87/4.19 tff(zero$j, type, zero$j: A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_58', type, '#skF_58': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_36', type, '#skF_36': Nat_a_iarray_iarray_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_33', type, '#skF_33': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_96', type, '#skF_96': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff('#skF_112', type, '#skF_112': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_113', type, '#skF_113': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_146', type, '#skF_146': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_109', type, '#skF_109': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_35', type, '#skF_35': Nat_a_iarray_iarray_prod$ > Nat$).
% 13.87/4.19 tff(gauss_Jordan_column_k_PA$, type, gauss_Jordan_column_k_PA$: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun_fun$).
% 13.87/4.19 tff('#skF_120', type, '#skF_120': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_10', type, '#skF_10': (Int_int_prod_bool_fun$ * Int_int_prod$) > $int).
% 13.87/4.19 tff(less_eq$, type, less_eq$: Nat_nat_bool_fun_fun$).
% 13.87/4.19 tff('#skF_11', type, '#skF_11': (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_149', type, '#skF_149': (Nat_nat_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(nrows_iarray$, type, nrows_iarray$: A_iarray_iarray$ > Nat$).
% 13.87/4.19 tff(fun_app$f, type, fun_app$f: (Int_nat_prod_bool_fun$ * Int_nat_prod$) > $o).
% 13.87/4.19 tff('#skF_38', type, '#skF_38': (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > Nat$).
% 13.87/4.19 tff('#skF_1', type, '#skF_1': (Nat_a_iarray_prod_bool_fun$ * Nat_a_iarray_prod$) > Nat$).
% 13.87/4.19 tff('#skF_48', type, '#skF_48': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff(plus$b, type, plus$b: (A_c_vec_c_vec$ * A_c_vec_c_vec$) > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_3', type, '#skF_3': (Nat_nat_prod_bool_fun$ * Nat_nat_prod$) > Nat$).
% 13.87/4.19 tff(plus$g, type, plus$g: (Int_int_prod$ * Int_int_prod$) > Int_int_prod$).
% 13.87/4.19 tff('#skF_137', type, '#skF_137': (Nat$ * Nat_a_b_vec_c_vec_prod$) > A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_57', type, '#skF_57': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_116', type, '#skF_116': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(fun_app$q, type, fun_app$q: (Nat_a_b_vec_c_vec_bool_fun_fun$ * Nat$) > A_b_vec_c_vec_bool_fun$).
% 13.87/4.19 tff('#skF_56', type, '#skF_56': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_135', type, '#skF_135': (A_iarray_iarray$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff(pair$a, type, pair$a: (Nat$ * A_b_vec_c_vec$) > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_15', type, '#skF_15': (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff(fst$l, type, fst$l: A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_75', type, '#skF_75': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_90', type, '#skF_90': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(plus$a, type, plus$a: (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff(nrows$, type, nrows$: A_b_vec_c_vec$ > Nat$).
% 13.87/4.19 tff('#skF_87', type, '#skF_87': (Nat_nat_bool_fun_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fst$j, type, fst$j: Nat_a_c_vec_c_vec_prod$ > Nat$).
% 13.87/4.19 tff('#skF_31', type, '#skF_31': Nat_a_b_vec_c_vec_prod$ > Nat$).
% 13.87/4.19 tff(snd$b, type, snd$b: Nat_a_iarray_iarray_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_132', type, '#skF_132': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_139', type, '#skF_139': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_134', type, '#skF_134': (A_c_vec_c_vec$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff(gauss_Jordan_column_k_PA$a, type, gauss_Jordan_column_k_PA$a: (A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$ * Nat$) > A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$).
% 13.87/4.19 tff(fun_app$h, type, fun_app$h: (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > $o).
% 13.87/4.19 tff(pair$k, type, pair$k: (Nat$ * A_c_vec_c_vec$) > Nat_a_c_vec_c_vec_prod$).
% 13.87/4.19 tff(tlfalse, type, tlfalse: tlbool).
% 13.87/4.19 tff(fun_app$t, type, fun_app$t: (Nat_nat_bool_fun_fun$ * Nat$) > Nat_bool_fun$).
% 13.87/4.19 tff('#skF_54', type, '#skF_54': (Nat_int_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_153', type, '#skF_153': (A_b_vec_c_vec$ * Nat_a_b_vec_c_vec_prod$) > Nat$).
% 13.87/4.19 tff(fst$f, type, fst$f: Nat_int_prod$ > Nat$).
% 13.87/4.19 tff('#skF_12', type, '#skF_12': (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_91', type, '#skF_91': Nat$ > Nat$).
% 13.87/4.19 tff('#skF_23', type, '#skF_23': Nat_a_b_vec_c_vec_prod$ > Nat$).
% 13.87/4.19 tff('#skF_103', type, '#skF_103': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(snd$c, type, snd$c: A_iarray_iarray_a_iarray_iarray_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff(ncols$a, type, ncols$a: A_c_vec_c_vec$ > Nat$).
% 13.87/4.19 tff('#skF_130', type, '#skF_130': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(divides_aux$, type, divides_aux$: Int_int_prod_bool_fun$).
% 13.87/4.19 tff('#skF_94', type, '#skF_94': (Nat$ * Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_32', type, '#skF_32': Nat_a_b_vec_c_vec_prod$ > A_b_vec_c_vec$).
% 13.87/4.19 tff(plus$k, type, plus$k: (Nat_nat_prod$ * Nat_nat_prod$) > Nat_nat_prod$).
% 13.87/4.19 tff('#skF_125', type, '#skF_125': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_126', type, '#skF_126': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_154', type, '#skF_154': (A_iarray_iarray$ * Nat_a_iarray_iarray_prod$) > Nat$).
% 13.87/4.19 tff(plus$e, type, plus$e: (A_iarray_iarray$ * A_iarray_iarray$) > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_73', type, '#skF_73': Nat$ > Nat$).
% 13.87/4.19 tff('#skF_7', type, '#skF_7': (Int_nat_prod_bool_fun$ * Int_nat_prod$) > $int).
% 13.87/4.19 tff('#skF_129', type, '#skF_129': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_41', type, '#skF_41': (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > Nat$).
% 13.87/4.19 tff('#skF_19', type, '#skF_19': Int_int_prod$ > $int).
% 13.87/4.19 tff('#skF_14', type, '#skF_14': (Nat_a_b_vec_c_vec_prod_bool_fun$ * Nat_a_b_vec_c_vec_prod$) > A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_53', type, '#skF_53': (Nat_int_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(plus$, type, plus$: Nat$ > Nat_nat_fun$).
% 13.87/4.19 tff(fun_app$a, type, fun_app$a: (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > Nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun$).
% 13.87/4.19 tff(b$, type, b$: A_iarray_iarray_nat_a_iarray_iarray_prod_prod$).
% 13.87/4.19 tff('#skF_111', type, '#skF_111': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_78', type, '#skF_78': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(nrows$a, type, nrows$a: A_c_vec_c_vec$ > Nat$).
% 13.87/4.19 tff(snd$k, type, snd$k: A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$ > Nat_a_c_vec_c_vec_prod$).
% 13.87/4.19 tff(pair$f, type, pair$f: (Nat$ * $int) > Nat_int_prod$).
% 13.87/4.19 tff(fun_app$r, type, fun_app$r: (Nat_a_iarray_iarray_bool_fun_fun$ * Nat$) > A_iarray_iarray_bool_fun$).
% 13.87/4.19 tff('#skF_22', type, '#skF_22': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_6', type, '#skF_6': (Nat_int_prod_bool_fun$ * Nat_int_prod$) > $int).
% 13.87/4.19 tff('#skF_133', type, '#skF_133': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff(pair$e, type, pair$e: (Nat$ * Nat$) > Nat_nat_prod$).
% 13.87/4.19 tff(plus$l, type, plus$l: (A_iarray_iarray_a_iarray_iarray_prod$ * A_iarray_iarray_a_iarray_iarray_prod$) > A_iarray_iarray_a_iarray_iarray_prod$).
% 13.87/4.19 tff(matrix_to_iarray$, type, matrix_to_iarray$: A_c_vec_c_vec$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_84', type, '#skF_84': Nat$ > Nat$).
% 13.87/4.19 tff(pair$c, type, pair$c: (A_iarray_iarray$ * A_iarray_iarray$) > A_iarray_iarray_a_iarray_iarray_prod$).
% 13.87/4.19 tff(vector_all_zero_from_index$, type, vector_all_zero_from_index$: Nat_a_iarray_prod_bool_fun$).
% 13.87/4.19 tff(fun_app$n, type, fun_app$n: (A_iarray_iarray_bool_fun$ * A_iarray_iarray$) > $o).
% 13.87/4.19 tff('#skF_46', type, '#skF_46': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_72', type, '#skF_72': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff(less$, type, less$: Nat_nat_bool_fun_fun$).
% 13.87/4.19 tff('#skF_97', type, '#skF_97': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff('#skF_45', type, '#skF_45': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > A_b_vec_c_vec$).
% 13.87/4.19 tff(gauss_Jordan_column_k_iarrays_PA$, type, gauss_Jordan_column_k_iarrays_PA$: A_iarray_iarray_nat_a_iarray_iarray_prod_prod_nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun_fun$).
% 13.87/4.19 tff('#skF_16', type, '#skF_16': (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff('#skF_70', type, '#skF_70': (Nat_nat_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fun_app$w, type, fun_app$w: (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > Nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun$).
% 13.87/4.19 tff(zero$g, type, zero$g: Int_int_prod$).
% 13.87/4.19 tff('#skF_63', type, '#skF_63': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff(of_nat$, type, of_nat$: Nat_int_fun$).
% 13.87/4.19 tff('#skF_102', type, '#skF_102': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_52', type, '#skF_52': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(snd$d, type, snd$d: A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff('#skF_93', type, '#skF_93': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(gauss_Jordan_upt_k_iarrays_PA$, type, gauss_Jordan_upt_k_iarrays_PA$: (A_iarray_iarray$ * Nat$) > A_iarray_iarray_a_iarray_iarray_prod$).
% 13.87/4.19 tff('#skF_8', type, '#skF_8': (Int_nat_prod_bool_fun$ * Int_nat_prod$) > Nat$).
% 13.87/4.19 tff('#skF_152', type, '#skF_152': (A_iarray_iarray$ * A_iarray_iarray_a_iarray_iarray_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff(fun_app$d, type, fun_app$d: (Nat_nat_prod_bool_fun$ * Nat_nat_prod$) > $o).
% 13.87/4.19 tff('#skF_4', type, '#skF_4': (Nat_nat_prod_bool_fun$ * Nat_nat_prod$) > Nat$).
% 13.87/4.19 tff('#skF_17', type, '#skF_17': (Nat_a_iarray_iarray_prod_bool_fun$ * Nat_a_iarray_iarray_prod$) > Nat$).
% 13.87/4.19 tff('#skF_127', type, '#skF_127': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(pair$g, type, pair$g: ($int * Nat$) > Int_nat_prod$).
% 13.87/4.19 tff('#skF_5', type, '#skF_5': (Nat_int_prod_bool_fun$ * Nat_int_prod$) > Nat$).
% 13.87/4.19 tff(fst$d, type, fst$d: A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_108', type, '#skF_108': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff(fun_app$, type, fun_app$: (Nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun$ * Nat$) > A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff('#skF_151', type, '#skF_151': (Nat_a_iarray_iarray_prod$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff(k$, type, k$: Nat$).
% 13.87/4.19 tff(zero$b, type, zero$b: Int_nat_prod$).
% 13.87/4.19 tff('#skF_43', type, '#skF_43': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff(pair$d, type, pair$d: (A_iarray_iarray$ * Nat_a_iarray_iarray_prod$) > A_iarray_iarray_nat_a_iarray_iarray_prod_prod$).
% 13.87/4.19 tff(gauss_Jordan_upt_k_PA$, type, gauss_Jordan_upt_k_PA$: (A_b_vec_c_vec$ * Nat$) > A_c_vec_c_vec_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_110', type, '#skF_110': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(mat_iarray$, type, mat_iarray$: (A$ * Nat$) > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_79', type, '#skF_79': (Nat$ * Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_114', type, '#skF_114': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(a$a, type, a$a: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff(pair$i, type, pair$i: (Nat$ * A_iarray$) > Nat_a_iarray_prod$).
% 13.87/4.19 tff(snd$, type, snd$: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff(snd$g, type, snd$g: Int_nat_prod$ > Nat$).
% 13.87/4.19 tff('#skF_98', type, '#skF_98': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff(fun_app$i, type, fun_app$i: (Nat_a_b_vec_c_vec_prod_bool_fun$ * Nat_a_b_vec_c_vec_prod$) > $o).
% 13.87/4.19 tff('#skF_62', type, '#skF_62': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(suc$, type, suc$: Nat_nat_fun$).
% 13.87/4.19 tff('#skF_13', type, '#skF_13': (Nat_a_b_vec_c_vec_prod_bool_fun$ * Nat_a_b_vec_c_vec_prod$) > Nat$).
% 13.87/4.19 tff('#skF_117', type, '#skF_117': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(one$, type, one$: A$).
% 13.87/4.19 tff('#skF_100', type, '#skF_100': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_150', type, '#skF_150': (Nat_a_b_vec_c_vec_prod$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > A_c_vec_c_vec$).
% 13.87/4.19 tff(plus$d, type, plus$d: (A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > A_iarray_iarray_nat_a_iarray_iarray_prod_prod$).
% 13.87/4.19 tff(upt$, type, upt$: (Nat$ * Nat$) > Nat_list$).
% 13.87/4.19 tff('#skF_65', type, '#skF_65': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff('#skF_34', type, '#skF_34': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff(pair$l, type, pair$l: (A_c_vec_c_vec$ * A_b_vec_c_vec$) > A_c_vec_c_vec_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_115', type, '#skF_115': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_42', type, '#skF_42': (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_bool_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff(snd$f, type, snd$f: Nat_int_prod$ > $int).
% 13.87/4.19 tff('#skF_49', type, '#skF_49': (Nat_int_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fst$, type, fst$: A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff(plus$j, type, plus$j: (Nat_int_prod$ * Nat_int_prod$) > Nat_int_prod$).
% 13.87/4.19 tff(plus$f, type, plus$f: (Nat_a_iarray_iarray_prod$ * Nat_a_iarray_iarray_prod$) > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff(snd$h, type, snd$h: Int_int_prod$ > $int).
% 13.87/4.19 tff(ncols$, type, ncols$: A_b_vec_c_vec$ > Nat$).
% 13.87/4.19 tff('#skF_89', type, '#skF_89': (Nat_nat_bool_fun_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_74', type, '#skF_74': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff(foldl$a, type, foldl$a: (A_iarray_iarray_nat_a_iarray_iarray_prod_prod_nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun_fun$ * A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ * Nat_list$) > A_iarray_iarray_nat_a_iarray_iarray_prod_prod$).
% 13.87/4.19 tff('#skF_106', type, '#skF_106': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(matrix_to_iarray$a, type, matrix_to_iarray$a: A_b_vec_c_vec$ > A_iarray_iarray$).
% 13.87/4.19 tff(fst$c, type, fst$c: A_iarray_iarray_a_iarray_iarray_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_66', type, '#skF_66': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff(foldl$, type, foldl$: (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_nat_a_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_fun_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ * Nat_list$) > A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff('#skF_47', type, '#skF_47': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > Nat$).
% 13.87/4.19 tff('#skF_145', type, '#skF_145': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_55', type, '#skF_55': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_61', type, '#skF_61': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff(plus$h, type, plus$h: (Int_nat_prod$ * Int_nat_prod$) > Int_nat_prod$).
% 13.87/4.19 tff('#skF_141', type, '#skF_141': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_2', type, '#skF_2': (Nat_a_iarray_prod_bool_fun$ * Nat_a_iarray_prod$) > A_iarray$).
% 13.87/4.19 tff(fun_app$y, type, fun_app$y: (Int_int_bool_fun_fun$ * $int) > Int_bool_fun$).
% 13.87/4.19 tff('#skF_83', type, '#skF_83': (Nat_bool_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_128', type, '#skF_128': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff(fst$e, type, fst$e: Nat_nat_prod$ > Nat$).
% 13.87/4.19 tff('#skF_64', type, '#skF_64': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff(a$, type, a$: A_b_vec_c_vec$).
% 13.87/4.19 tff(pair$, type, pair$: (A_c_vec_c_vec$ * Nat_a_b_vec_c_vec_prod$) > A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$).
% 13.87/4.19 tff(fst$b, type, fst$b: Nat_a_iarray_iarray_prod$ > Nat$).
% 13.87/4.19 tff(fun_app$b, type, fun_app$b: (Nat_int_fun$ * Nat$) > $int).
% 13.87/4.19 tff('#skF_39', type, '#skF_39': (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod_bool_fun$ * A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$) > A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_122', type, '#skF_122': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(fun_app$c, type, fun_app$c: (Nat_a_iarray_prod_bool_fun$ * Nat_a_iarray_prod$) > $o).
% 13.87/4.19 tff(fun_app$m, type, fun_app$m: (A_iarray_iarray_nat_a_iarray_iarray_prod_bool_fun_fun$ * A_iarray_iarray$) > Nat_a_iarray_iarray_prod_bool_fun$).
% 13.87/4.19 tff(fst$k, type, fst$k: A_c_vec_c_vec_a_b_vec_c_vec_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff(fun_app$g, type, fun_app$g: (Int_int_prod_bool_fun$ * Int_int_prod$) > $o).
% 13.87/4.19 tff('#skF_101', type, '#skF_101': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_82', type, '#skF_82': (Nat_bool_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_25', type, '#skF_25': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff(fst$h, type, fst$h: Int_int_prod$ > $int).
% 13.87/4.19 tff('#skF_105', type, '#skF_105': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(mat$, type, mat$: A$ > A_c_vec_c_vec$).
% 13.87/4.19 tff(fun_app$l, type, fun_app$l: (A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_bool_fun_fun$ * A_c_vec_c_vec$) > Nat_a_b_vec_c_vec_prod_bool_fun$).
% 13.87/4.19 tff('#skF_121', type, '#skF_121': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff(nat$, type, nat$: $int > Nat$).
% 13.87/4.19 tff(one$a, type, one$a: Nat$).
% 13.87/4.19 tff(zero$f, type, zero$f: Nat_int_prod$).
% 13.87/4.19 tff('#skF_81', type, '#skF_81': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_20', type, '#skF_20': Int_int_prod$ > $int).
% 13.87/4.19 tff(plus$i, type, plus$i: (A_b_vec_c_vec$ * A_b_vec_c_vec$) > A_b_vec_c_vec$).
% 13.87/4.19 tff('#skF_27', type, '#skF_27': Nat_a_iarray_iarray_prod$ > Nat$).
% 13.87/4.19 tff(fun_app$o, type, fun_app$o: (A_iarray_iarray_a_iarray_iarray_bool_fun_fun$ * A_iarray_iarray$) > A_iarray_iarray_bool_fun$).
% 13.87/4.19 tff('#skF_144', type, '#skF_144': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_69', type, '#skF_69': (Nat_nat_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(snd$a, type, snd$a: Nat_a_b_vec_c_vec_prod$ > A_b_vec_c_vec$).
% 13.87/4.19 tff(column_iarray$, type, column_iarray$: (Nat$ * A_iarray_iarray$) > A_iarray$).
% 13.87/4.19 tff('#skF_9', type, '#skF_9': (Int_int_prod_bool_fun$ * Int_int_prod$) > $int).
% 13.87/4.19 tff('#skF_88', type, '#skF_88': (Nat_nat_bool_fun_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_131', type, '#skF_131': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19 tff(gauss_Jordan_in_ij_iarrays_PA$, type, gauss_Jordan_in_ij_iarrays_PA$: (A_iarray_iarray_a_iarray_iarray_prod$ * Nat$ * Nat$) > A_iarray_iarray_a_iarray_iarray_prod$).
% 13.87/4.19 tff(fun_app$k, type, fun_app$k: (Nat_a_iarray_iarray_prod_bool_fun$ * Nat_a_iarray_iarray_prod$) > $o).
% 13.87/4.19 tff(tltrue, type, tltrue: tlbool).
% 13.87/4.19 tff(fst$a, type, fst$a: Nat_a_b_vec_c_vec_prod$ > Nat$).
% 13.87/4.19 tff('#skF_29', type, '#skF_29': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_85', type, '#skF_85': (Nat_bool_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_104', type, '#skF_104': (Int_int_bool_fun_fun$ * $int * $int) > $int).
% 13.87/4.19 tff('#skF_77', type, '#skF_77': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fun_app$v, type, fun_app$v: (Nat_a_iarray_iarray_nat_a_iarray_iarray_prod_prod_fun$ * Nat$) > A_iarray_iarray_nat_a_iarray_iarray_prod_prod$).
% 13.87/4.19 tff('#skF_24', type, '#skF_24': Nat_a_b_vec_c_vec_prod$ > A_b_vec_c_vec$).
% 13.87/4.19 tff(fun_app$s, type, fun_app$s: (Nat_bool_fun$ * Nat$) > $o).
% 13.87/4.19 tff('#skF_50', type, '#skF_50': (Nat_int_fun$ * Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_138', type, '#skF_138': (Nat$ * Nat_a_iarray_iarray_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff(fun_app$u, type, fun_app$u: (Nat_nat_fun$ * Nat$) > Nat$).
% 13.87/4.19 tff(pair$h, type, pair$h: ($int * $int) > Int_int_prod$).
% 13.87/4.19 tff(fun_app$z, type, fun_app$z: (Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_147', type, '#skF_147': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_136', type, '#skF_136': (A_iarray_iarray$ * A_iarray_iarray_a_iarray_iarray_prod$) > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_76', type, '#skF_76': Nat$ > Nat$).
% 13.87/4.19 tff('#skF_28', type, '#skF_28': Nat_a_iarray_iarray_prod$ > A_iarray_iarray$).
% 13.87/4.19 tff('#skF_60', type, '#skF_60': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_107', type, '#skF_107': ($int * $int * Int_int_fun$ * $int) > $int).
% 13.87/4.19 tff('#skF_44', type, '#skF_44': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > Nat$).
% 13.87/4.19 tff('#skF_99', type, '#skF_99': (Nat$ * Nat$ * Nat_nat_bool_fun_fun$) > Nat$).
% 13.87/4.19 tff('#skF_30', type, '#skF_30': A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$ > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff(fst$g, type, fst$g: Int_nat_prod$ > $int).
% 13.87/4.19 tff(ka$, type, ka$: Nat$).
% 13.87/4.19 tff('#skF_143', type, '#skF_143': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff(fst$i, type, fst$i: Nat_a_iarray_prod$ > Nat$).
% 13.87/4.19 tff(plus$c, type, plus$c: (Nat_a_b_vec_c_vec_prod$ * Nat_a_b_vec_c_vec_prod$) > Nat_a_b_vec_c_vec_prod$).
% 13.87/4.19 tff(zero$d, type, zero$d: Nat$).
% 13.87/4.19 tff(snd$j, type, snd$j: Nat_a_c_vec_c_vec_prod$ > A_c_vec_c_vec$).
% 13.87/4.19 tff('#skF_68', type, '#skF_68': (Nat$ * Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff('#skF_26', type, '#skF_26': A_iarray_iarray_nat_a_iarray_iarray_prod_prod$ > Nat_a_iarray_iarray_prod$).
% 13.87/4.19 tff(zero$c, type, zero$c: Nat_a_c_vec_c_vec_prod$).
% 13.87/4.19 tff('#skF_71', type, '#skF_71': (Nat$ * Nat_bool_fun$) > Nat$).
% 13.87/4.19 tff(snd$i, type, snd$i: Nat_a_iarray_prod$ > A_iarray$).
% 13.87/4.19 tff('#skF_142', type, '#skF_142': (Nat$ * Nat$) > Nat$).
% 13.87/4.19 tff('#skF_118', type, '#skF_118': ($int * Int_int_fun$ * $int * $int) > $int).
% 13.87/4.19
% 13.87/4.20 tff(f_685, axiom, (![A__questionmark_v0:A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$]: (A__questionmark_v0 = pair$(fst$(A__questionmark_v0), snd$(A__questionmark_v0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom131)).
% 13.87/4.20 tff(f_694, axiom, (![A__questionmark_v0:Nat_a_b_vec_c_vec_prod$]: (A__questionmark_v0 = pair$a(fst$a(A__questionmark_v0), snd$a(A__questionmark_v0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom134)).
% 13.87/4.20 tff(f_35, negated_conjecture, ~(matrix_to_iarray$(fst$(fun_app$(fun_app$a(gauss_Jordan_column_k_PA$, foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(fun_app$b(of_nat$, ka$), 1))))), nat$($sum(fun_app$b(of_nat$, ka$), 1))))) = matrix_to_iarray$(fst$(fun_app$(fun_app$a(gauss_Jordan_column_k_PA$, pair$(fst$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(fun_app$b(of_nat$, ka$), 1))))), pair$a(fst$a(snd$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(fun_app$b(of_nat$, ka$), 1)))))), snd$a(snd$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(fun_app$b(of_nat$, ka$), 1))))))))), nat$($sum(fun_app$b(of_nat$, ka$), 1)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture0)).
% 13.87/4.20 tff(c_391, plain, (![A__questionmark_v0_290:A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$]: (pair$(fst$(A__questionmark_v0_290), snd$(A__questionmark_v0_290))=A__questionmark_v0_290)), inference(cnfTransformation, [status(thm)], [f_685])).
% 13.87/4.20 tff(c_397, plain, (![A__questionmark_v0_293:Nat_a_b_vec_c_vec_prod$]: (pair$a(fst$a(A__questionmark_v0_293), snd$a(A__questionmark_v0_293))=A__questionmark_v0_293)), inference(cnfTransformation, [status(thm)], [f_694])).
% 13.87/4.20 tff(c_2236, plain, (matrix_to_iarray$(fst$(fun_app$(fun_app$a(gauss_Jordan_column_k_PA$, pair$(fst$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(1, fun_app$b(of_nat$, ka$)))))), pair$a(fst$a(snd$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(1, fun_app$b(of_nat$, ka$))))))), snd$a(snd$(foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(1, fun_app$b(of_nat$, ka$)))))))))), nat$($sum(1, fun_app$b(of_nat$, ka$))))))!=matrix_to_iarray$(fst$(fun_app$(fun_app$a(gauss_Jordan_column_k_PA$, foldl$(gauss_Jordan_column_k_PA$, pair$(mat$(one$), pair$a(nat$(0), a$)), upt$(nat$(0), nat$($sum(1, fun_app$b(of_nat$, ka$)))))), nat$($sum(1, fun_app$b(of_nat$, ka$))))))), inference(cnfTransformation, [status(thm)], [f_35])).
% 13.87/4.20 tff(c_2364, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_391, c_397, c_2236])).
% 13.87/4.20 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------