%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP386_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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n019.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:44 PM UTC 2025
% Result : Theorem 21.97s 7.53s
% Output : CNFRefutation 23.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP386_1 : TPTP v9.0.0. Released v8.0.0.
% 0.07/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.35 % Computer : n019.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Tue Apr 8 02:21:47 EDT 2025
% 0.12/0.35 % CPUTime :
% 21.97/7.53 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.97/7.53
% 21.97/7.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.08/7.73 %$ valid_getter_setter$d > valid_getter_setter$c > valid_getter_setter$b > valid_getter_setter$a > valid_getter_setter$ > member$d > member$c > member$b > member$a > member$ > inj_on$a > inj_on$ > fun_app$z > fun_app$c > fun_app$b > fun_app$aw > fun_app$ag > fun_app$a > fun_app$ > register$h > register$g > register$f > register$e > register$d > register$c > register$b > register$a > register$ > preregister$f > preregister$e > preregister$d > preregister$c > preregister$b > preregister$a > preregister$ > is_empty$c > is_empty$b > is_empty$a > is_empty$ > fun_upd$e > fun_upd$d > fun_upd$c > fun_upd$a > def_8 > def_6 > def_22 > def_20 > def_18 > def_16 > def_13 > def_12 > def_11 > case_option$m > case_option$l > case_option$i > case_option$h > case_option$b > uvz$ > uvy$ > uvx$ > uvw$ > uvv$ > uvu$ > uvr$ > uvq$ > uvb$ > uuz$ > uux$ > uuw$ > uuv$ > uuu$ > uuq$ > uup$ > uuo$ > uun$ > uum$ > uul$ > uuk$ > uuj$ > uui$ > uuh$ > uua$ > uu$ > update1$ > register_from_getter_setter$d > register_from_getter_setter$c > register_from_getter_setter$b > register_from_getter_setter$a > register_from_getter_setter$ > register_apply$a > register_apply$ > map_option$l > map_option$k > map_option$j > map_option$i > insert$c > insert$b > insert$a > insert$ > image$a > image$ > fun_upd$f > fun_upd$b > fun_upd$ > 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$p > fun_app$o > fun_app$n > fun_app$m > fun_app$l > 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$bp > fun_app$bo > fun_app$bn > fun_app$bm > fun_app$bl > fun_app$bk > fun_app$bj > fun_app$bi > fun_app$bh > fun_app$bg > fun_app$bf > fun_app$be > fun_app$bd > fun_app$bc > fun_app$bb > fun_app$ba > fun_app$az > fun_app$ay > fun_app$ax > fun_app$av > fun_app$au > fun_app$at > fun_app$as > fun_app$ar > fun_app$aq > fun_app$ap > fun_app$ao > fun_app$an > fun_app$am > fun_app$al > fun_app$ak > fun_app$aj > fun_app$ai > fun_app$ah > fun_app$af > fun_app$ae > fun_app$ad > fun_app$ac > fun_app$ab > fun_app$aa > def_9 > def_7 > def_5 > def_4 > def_3 > def_23 > def_21 > def_2 > def_19 > def_17 > def_15 > def_14 > def_10 > def_1 > comp$z > comp$y > comp$x > comp$w > comp$v > comp$u > comp$t > comp$s > comp$r > comp$q > comp$p > comp$o > comp$n > comp$m > comp$l > comp$k > comp$j > comp$i > comp$h > comp$g > comp$f > comp$e > comp$d > comp$c > comp$bm > comp$bl > comp$bk > comp$bj > comp$bi > comp$bh > comp$bg > comp$bf > comp$be > comp$bd > comp$bc > comp$bb > comp$ba > comp$b > comp$az > comp$ay > comp$aw > comp$av > comp$au > comp$at > comp$ar > comp$aq > comp$ap > comp$ao > comp$an > comp$am > comp$al > comp$ak > comp$aj > comp$ai > comp$ah > comp$ag > comp$af > comp$ae > comp$ad > comp$ac > comp$ab > comp$aa > comp$a > comp$ > combine_options$b > combine_options$a > combine_options$ > case_sum$f > case_sum$e > case_sum$d > case_sum$c > case_sum$b > case_sum$a > case_sum$ > case_option$k > case_option$j > case_option$g > case_option$f > case_option$e > case_option$d > case_option$c > case_option$a > case_option$ > bind$g > bind$f > bind$e > bind$d > bind$b > bind$a > #nlpp > uwq$ > uwp$ > uwm$ > uwl$ > uwk$ > uwj$ > uwi$ > uwh$ > uwa$ > uvt$ > uvl$ > uvk$ > uvj$ > uvi$ > uvh$ > uvg$ > uvf$ > uve$ > uvd$ > uvc$ > uva$ > uuy$ > uut$ > uus$ > uur$ > update1$b > update1$a > these$a > these$ > the$f > the$e > the$d > the$c > some$d > some$c > setter$a > setter$ > set_option$d > set_option$c > set_option$b > set_option$a > set_option$ > map_option$h > map_option$g > map_option$f > map_option$e > map_option$d > map_option$c > map_option$b > map_option$a > map_option$ > getter$a > getter$ > comp$ax > comp$as > collect$c > collect$b > collect$a > collect$ > bind$h > bind$c > bind$ > uws$ > uwr$ > uwo$ > uwn$ > uwg$ > uwf$ > uwe$ > uwd$ > uwc$ > uwb$ > uvs$ > uvp$ > uvo$ > uvn$ > uvm$ > uug$ > uuf$ > uue$ > uud$ > uuc$ > uub$ > undefined$b > undefined$a > undefined$ > top$c > top$b > top$a > top$ > tltrue > tlfalse > thesis$ > the$b > the$a > the$ > some$b > some$a > some$ > sF$ > none$d > none$c > none$b > none$a > none$ > is_none$b > is_none$a > is_none$ > id$g > id$f > id$e > id$d > id$c > id$b > id$a > id$ > gF$ > g$ > f$ > bot$h > bot$g > bot$f > bot$e > bot$d > bot$c > bot$b > bot$a > bot$ > #skF_17 > #skF_130 > #skF_178 > #skF_25 > #skF_124 > #skF_37 > #skF_66 > #skF_72 > #skF_189 > #skF_137 > #skF_180 > #skF_47 > #skF_184 > #skF_39 > #skF_91 > #skF_14 > #skF_41 > #skF_164 > #skF_111 > #skF_109 > #skF_169 > #skF_182 > #skF_13 > #skF_149 > #skF_136 > #skF_52 > #skF_142 > #skF_174 > #skF_23 > #skF_53 > #skF_176 > #skF_147 > #skF_73 > #skF_11 > #skF_204 > #skF_38 > #skF_156 > #skF_75 > #skF_108 > #skF_88 > #skF_165 > #skF_175 > #skF_138 > #skF_60 > #skF_70 > #skF_21 > #skF_146 > #skF_110 > #skF_203 > #skF_45 > #skF_207 > #skF_190 > #skF_192 > #skF_188 > #skF_46 > #skF_167 > #skF_8 > #skF_42 > #skF_157 > #skF_206 > #skF_15 > #skF_103 > #skF_27 > #skF_30 > #skF_141 > #skF_120 > #skF_113 > #skF_123 > #skF_84 > #skF_172 > #skF_83 > #skF_43 > #skF_125 > #skF_34 > #skF_102 > #skF_195 > #skF_140 > #skF_97 > #skF_191 > #skF_16 > #skF_63 > #skF_89 > #skF_144 > #skF_199 > #skF_85 > #skF_143 > #skF_205 > #skF_35 > #skF_10 > #skF_77 > #skF_121 > #skF_65 > #skF_112 > #skF_115 > #skF_154 > #skF_78 > #skF_202 > #skF_119 > #skF_48 > #skF_134 > #skF_159 > #skF_200 > #skF_86 > #skF_62 > #skF_106 > #skF_33 > #skF_40 > #skF_194 > #skF_2 > #skF_150 > #skF_186 > #skF_29 > #skF_158 > #skF_82 > #skF_129 > #skF_155 > #skF_163 > #skF_177 > #skF_44 > #skF_151 > #skF_98 > #skF_183 > #skF_196 > #skF_74 > #skF_18 > #skF_94 > #skF_139 > #skF_128 > #skF_135 > #skF_26 > #skF_59 > #skF_49 > #skF_5 > #skF_127 > #skF_92 > #skF_9 > #skF_19 > #skF_101 > #skF_58 > #skF_24 > #skF_71 > #skF_197 > #skF_79 > #skF_4 > #skF_28 > #skF_51 > #skF_161 > #skF_105 > #skF_133 > #skF_50 > #skF_132 > #skF_36 > #skF_12 > #skF_80 > #skF_170 > #skF_145 > #skF_99 > #skF_61 > #skF_1 > #skF_201 > #skF_107 > #skF_95 > #skF_76 > #skF_181 > #skF_162 > #skF_116 > #skF_69 > #skF_32 > #skF_87 > #skF_57 > #skF_90 > #skF_193 > #skF_122 > #skF_93 > #skF_3 > #skF_148 > #skF_179 > #skF_54 > #skF_81 > #skF_55 > #skF_171 > #skF_187 > #skF_173 > #skF_131 > #skF_68 > #skF_31 > #skF_168 > #skF_126 > #skF_104 > #skF_152 > #skF_117 > #skF_56 > #skF_20 > #skF_22 > #skF_96 > #skF_100 > #skF_118 > #skF_198 > #skF_64 > #skF_153 > #skF_166 > #skF_185 > #skF_7 > #skF_160 > #skF_67 > #skF_6 > #skF_114
% 23.08/7.73
% 23.08/7.73 %Foreground sorts:
% 23.08/7.73 tff(A$, type, A$: $tType ).
% 23.08/7.73 tff(A_a_fun$, type, A_a_fun$: $tType ).
% 23.08/7.73 tff(C_option_b_option_bool_fun_fun$, type, C_option_b_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(B_option_b_option_bool_fun_fun$, type, B_option_b_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(Bool_c_option_fun$, type, Bool_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_b_option_fun_fun$, type, B_b_b_option_fun_fun$: $tType ).
% 23.08/7.73 tff(A_option_bool_fun$, type, A_option_bool_fun$: $tType ).
% 23.08/7.73 tff(C_c_fun$, type, C_c_fun$: $tType ).
% 23.08/7.73 tff(A_c_option_fun$, type, A_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_sum_b_option_fun$, type, B_b_sum_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_option_c_option_bool_fun_fun$, type, A_option_c_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(C_option$, type, C_option$: $tType ).
% 23.08/7.73 tff(B_b_option_fun_c_c_option_fun_fun$, type, B_b_option_fun_c_c_option_fun_fun$: $tType ).
% 23.08/7.73 tff(A_set$, type, A_set$: $tType ).
% 23.08/7.73 tff(A_a_option_fun_b_b_option_fun_fun$, type, A_a_option_fun_b_b_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B$, type, B$: $tType ).
% 23.08/7.73 tff(B_option_set$, type, B_option_set$: $tType ).
% 23.08/7.73 tff(tlbool, type, tlbool: $tType ).
% 23.08/7.73 tff(C_a_option_fun$, type, C_a_option_fun$: $tType ).
% 23.08/7.73 tff(C_c_option_fun_b_b_option_fun_fun$, type, C_c_option_fun_b_b_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_b_option_fun_b_b_option_fun_fun$, type, B_b_option_fun_b_b_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_b_option_fun_a_a_option_fun_fun$, type, B_b_option_fun_a_a_option_fun_fun$: $tType ).
% 23.08/7.73 tff(C_option_b_option_fun$, type, C_option_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_option_b_option_bool_fun_fun$, type, A_option_b_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(A_option_c_option_fun$, type, A_option_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_b_fun_fun$, type, B_b_b_fun_fun$: $tType ).
% 23.08/7.73 tff(C_option_c_option_bool_fun_fun$, type, C_option_c_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(A_bool_fun$, type, A_bool_fun$: $tType ).
% 23.08/7.73 tff(C$, type, C$: $tType ).
% 23.08/7.73 tff(C_option_a_option_bool_fun_fun$, type, C_option_a_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(C_set$, type, C_set$: $tType ).
% 23.08/7.73 tff(B_c_fun$, type, B_c_fun$: $tType ).
% 23.08/7.73 tff(C_option_c_fun$, type, C_option_c_fun$: $tType ).
% 23.08/7.73 tff(B_bool_fun$, type, B_bool_fun$: $tType ).
% 23.08/7.73 tff(B_option_b_fun$, type, B_option_b_fun$: $tType ).
% 23.08/7.73 tff(B_c_c_option_fun_fun$, type, B_c_c_option_fun_fun$: $tType ).
% 23.08/7.73 tff(A_b_fun$, type, A_b_fun$: $tType ).
% 23.08/7.73 tff(C_c_sum_c_fun$, type, C_c_sum_c_fun$: $tType ).
% 23.08/7.73 tff(B_c_c_fun_fun$, type, B_c_c_fun_fun$: $tType ).
% 23.08/7.73 tff(B_option_a_option_bool_fun_fun$, type, B_option_a_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(C_a_fun$, type, C_a_fun$: $tType ).
% 23.08/7.73 tff(A_option_b_option_fun$, type, A_option_b_option_fun$: $tType ).
% 23.08/7.73 tff(C_c_option_fun_c_c_option_fun_fun$, type, C_c_option_fun_c_c_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_option$, type, B_option$: $tType ).
% 23.08/7.73 tff(C_option_c_option_fun$, type, C_option_c_option_fun$: $tType ).
% 23.08/7.73 tff(C_bool_fun$, type, C_bool_fun$: $tType ).
% 23.08/7.73 tff(B_a_option_fun$, type, B_a_option_fun$: $tType ).
% 23.08/7.73 tff(A_a_a_fun_fun$, type, A_a_a_fun_fun$: $tType ).
% 23.08/7.73 tff(C_c_sum_c_option_fun$, type, C_c_sum_c_option_fun$: $tType ).
% 23.08/7.73 tff(C_option_option$, type, C_option_option$: $tType ).
% 23.08/7.73 tff(A_b_b_option_fun_fun$, type, A_b_b_option_fun_fun$: $tType ).
% 23.08/7.73 tff(A_a_sum_a_fun$, type, A_a_sum_a_fun$: $tType ).
% 23.08/7.73 tff(C_c_option_fun_c_option_fun$, type, C_c_option_fun_c_option_fun$: $tType ).
% 23.08/7.73 tff(A_a_option_fun$, type, A_a_option_fun$: $tType ).
% 23.08/7.73 tff(B_option_c_option_fun$, type, B_option_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_option_c_option_bool_fun_fun$, type, B_option_c_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(C_option_a_option_fun$, type, C_option_a_option_fun$: $tType ).
% 23.08/7.73 tff(B_set$, type, B_set$: $tType ).
% 23.08/7.73 tff(A_a_option_fun_c_c_option_fun_fun$, type, A_a_option_fun_c_c_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_option_a_option_fun$, type, B_option_a_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_sum_b_fun$, type, B_b_sum_b_fun$: $tType ).
% 23.08/7.73 tff(Bool_bool_fun$, type, Bool_bool_fun$: $tType ).
% 23.08/7.73 tff(C_c_option_fun$, type, C_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_option_fun$, type, B_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_a_option_fun_a_option_fun$, type, A_a_option_fun_a_option_fun$: $tType ).
% 23.08/7.73 tff(Bool_b_option_fun$, type, Bool_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_option_a_fun$, type, A_option_a_fun$: $tType ).
% 23.08/7.73 tff(B_b_sum_c_option_fun$, type, B_b_sum_c_option_fun$: $tType ).
% 23.08/7.73 tff(B_b_fun$, type, B_b_fun$: $tType ).
% 23.08/7.73 tff(C_option_set$, type, C_option_set$: $tType ).
% 23.08/7.73 tff(C_option_bool_fun$, type, C_option_bool_fun$: $tType ).
% 23.08/7.73 tff(B_option_b_option_fun$, type, B_option_b_option_fun$: $tType ).
% 23.08/7.73 tff(C_c_c_option_fun_fun$, type, C_c_c_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_a_fun$, type, B_a_fun$: $tType ).
% 23.08/7.73 tff(A_option_a_option_fun$, type, A_option_a_option_fun$: $tType ).
% 23.08/7.73 tff(B_option_bool_fun$, type, B_option_bool_fun$: $tType ).
% 23.08/7.73 tff(B_b_option_fun_b_option_fun$, type, B_b_option_fun_b_option_fun$: $tType ).
% 23.08/7.73 tff(C_b_b_fun_fun$, type, C_b_b_fun_fun$: $tType ).
% 23.08/7.73 tff(A_a_option_fun_a_a_option_fun_fun$, type, A_a_option_fun_a_a_option_fun_fun$: $tType ).
% 23.08/7.73 tff(B_c_option_fun$, type, B_c_option_fun$: $tType ).
% 23.08/7.73 tff(C_c_option_fun_a_a_option_fun_fun$, type, C_c_option_fun_a_a_option_fun_fun$: $tType ).
% 23.08/7.73 tff(A_option$, type, A_option$: $tType ).
% 23.08/7.73 tff(C_b_fun$, type, C_b_fun$: $tType ).
% 23.08/7.73 tff(C_b_option_fun$, type, C_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_b_b_fun_fun$, type, A_b_b_fun_fun$: $tType ).
% 23.08/7.73 tff(A_a_sum_b_option_fun$, type, A_a_sum_b_option_fun$: $tType ).
% 23.08/7.73 tff(B_option_option$, type, B_option_option$: $tType ).
% 23.08/7.73 tff(A_c_fun$, type, A_c_fun$: $tType ).
% 23.08/7.73 tff(A_b_option_fun$, type, A_b_option_fun$: $tType ).
% 23.08/7.73 tff(A_option_a_option_bool_fun_fun$, type, A_option_a_option_bool_fun_fun$: $tType ).
% 23.08/7.73 tff(C_c_c_fun_fun$, type, C_c_c_fun_fun$: $tType ).
% 23.08/7.73
% 23.08/7.73 %Background operators:
% 23.08/7.73
% 23.08/7.73
% 23.08/7.73 %Foreground operators:
% 23.08/7.73 tff(member$b, type, member$b: (C$ * C_set$) > $o).
% 23.08/7.73 tff(comp$x, type, comp$x: (C_option_b_option_fun$ * B_option_c_option_fun$) > B_option_b_option_fun$).
% 23.08/7.73 tff('#skF_17', type, '#skF_17': B_option$ > B$).
% 23.08/7.73 tff(comp$av, type, comp$av: (B_option_c_option_fun$ * B_b_option_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(bind$f, type, bind$f: (C_option$ * C_a_option_fun$) > A_option$).
% 23.08/7.73 tff('#skF_130', type, '#skF_130': (C_option_bool_fun$ * B_option$ * B_c_option_fun$) > B$).
% 23.08/7.73 tff('#skF_178', type, '#skF_178': (C_option$ * C_option$ * C_b_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(image$a, type, image$a: (B_b_option_fun$ * B_set$) > B_option_set$).
% 23.08/7.73 tff(uwj$, type, uwj$: B$ > B_option_b_fun$).
% 23.08/7.73 tff('#skF_25', type, '#skF_25': A_option_bool_fun$ > A$).
% 23.08/7.73 tff(fun_app$av, type, fun_app$av: (A_option_b_option_fun$ * A_option$) > B_option$).
% 23.08/7.73 tff('#skF_124', type, '#skF_124': (A_option_bool_fun$ * B_option$ * B_a_option_fun$) > B$).
% 23.08/7.73 tff(is_none$a, type, is_none$a: C_option_bool_fun$).
% 23.08/7.73 tff('#skF_37', type, '#skF_37': C_c_option_fun_b_b_option_fun_fun$ > B_c_fun$).
% 23.08/7.73 tff(def_18, type, def_18: (tlbool * C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff(def_19, type, def_19: (C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff(the$a, type, the$a: C_option_c_fun$).
% 23.08/7.73 tff(none$a, type, none$a: B_option$).
% 23.08/7.73 tff(none$d, type, none$d: C_option_option$).
% 23.08/7.73 tff('#skF_66', type, '#skF_66': C_option_bool_fun$ > C_option$).
% 23.08/7.73 tff('#skF_72', type, '#skF_72': B_b_option_fun_b_b_option_fun_fun$ > B_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_189', type, '#skF_189': C_bool_fun$ > C$).
% 23.08/7.73 tff('#skF_137', type, '#skF_137': (A_option$ * A_b_option_fun$ * B$) > A$).
% 23.08/7.73 tff(valid_getter_setter$d, type, valid_getter_setter$d: (C_c_fun$ * C_c_c_fun_fun$) > $o).
% 23.08/7.73 tff('#skF_180', type, '#skF_180': (A_option_bool_fun$ * B_option$ * B_a_option_fun$) > B$).
% 23.08/7.73 tff(fun_app$am, type, fun_app$am: (B_b_option_fun_c_c_option_fun_fun$ * B_b_option_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(uwi$, type, uwi$: C_option$ > B_c_option_fun$).
% 23.08/7.73 tff(register_from_getter_setter$c, type, register_from_getter_setter$c: (B_c_fun$ * C_b_b_fun_fun$) > C_c_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_47', type, '#skF_47': (B_option$ * B_option_a_option_bool_fun_fun$ * A_option$) > B$).
% 23.08/7.73 tff(comp$f, type, comp$f: (B_c_option_fun$ * B_b_fun$) > B_c_option_fun$).
% 23.08/7.73 tff('#skF_184', type, '#skF_184': (C_option_bool_fun$ * C_option$ * C_c_option_fun$) > C$).
% 23.08/7.73 tff(uux$, type, uux$: (A_a_a_fun_fun$ * A_option$) > A_a_option_fun$).
% 23.08/7.73 tff(set_option$, type, set_option$: B_option_option$ > B_option_set$).
% 23.08/7.73 tff(fun_app$as, type, fun_app$as: (A_a_option_fun_a_a_option_fun_fun$ * A_a_option_fun$) > A_a_option_fun$).
% 23.08/7.73 tff(fun_app$au, type, fun_app$au: (A_a_option_fun_b_b_option_fun_fun$ * A_a_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_39', type, '#skF_39': C_c_option_fun_c_c_option_fun_fun$ > C_c_fun$).
% 23.08/7.73 tff('#skF_91', type, '#skF_91': (B_c_fun$ * B_option$ * C$) > B$).
% 23.08/7.73 tff(image$, type, image$: (C_c_option_fun$ * C_set$) > C_option_set$).
% 23.08/7.73 tff(bind$g, type, bind$g: (B_option$ * B_a_option_fun$) > A_option$).
% 23.08/7.73 tff(fun_app$al, type, fun_app$al: (B_option_b_fun$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_14', type, '#skF_14': (B_a_fun$ * A_b_b_fun_fun$) > B$).
% 23.08/7.73 tff(fun_app$aq, type, fun_app$aq: (B_b_option_fun_a_a_option_fun_fun$ * B_b_option_fun$) > A_a_option_fun$).
% 23.08/7.73 tff(bind$b, type, bind$b: (B_option$ * B_c_option_fun$) > C_option$).
% 23.08/7.73 tff('#skF_41', type, '#skF_41': B_b_option_fun_c_c_option_fun_fun$ > C_b_fun$).
% 23.08/7.73 tff(fun_app$aa, type, fun_app$aa: (C_c_option_fun_c_c_option_fun_fun$ * C_c_option_fun$) > C_c_option_fun$).
% 23.08/7.73 tff('#skF_164', type, '#skF_164': (B_option$ * B_option$ * B_c_fun$ * B_c_fun$) > B$).
% 23.08/7.73 tff(id$g, type, id$g: C_c_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff('#skF_111', type, '#skF_111': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(uwr$, type, uwr$: B_option_b_option_bool_fun_fun$).
% 23.08/7.73 tff('#skF_109', type, '#skF_109': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff('#skF_169', type, '#skF_169': (A_option$ * A_b_fun$ * A_b_fun$) > A$).
% 23.08/7.73 tff('#skF_182', type, '#skF_182': (B_option_bool_fun$ * A_option$ * A_b_option_fun$) > A$).
% 23.08/7.73 tff(insert$, type, insert$: (B$ * B_set$) > B_set$).
% 23.08/7.73 tff(bind$e, type, bind$e: (A_option$ * A_b_option_fun$) > B_option$).
% 23.08/7.73 tff(def_12, type, def_12: (tlbool * B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff(fun_app$ap, type, fun_app$ap: (C_c_option_fun_a_a_option_fun_fun$ * C_c_option_fun$) > A_a_option_fun$).
% 23.08/7.73 tff(fun_app$r, type, fun_app$r: (A_a_fun$ * A$) > A$).
% 23.08/7.73 tff('#skF_13', type, '#skF_13': (B_a_fun$ * A_b_b_fun_fun$) > A$).
% 23.08/7.73 tff('#skF_149', type, '#skF_149': (B_option_option$ * B_option_bool_fun$ * B_option$) > B_option$).
% 23.08/7.73 tff('#skF_136', type, '#skF_136': (A_option$ * A_c_option_fun$ * C$) > A$).
% 23.08/7.73 tff(bot$e, type, bot$e: B_bool_fun$).
% 23.08/7.73 tff(uwo$, type, uwo$: C_option_c_option_bool_fun_fun$).
% 23.08/7.73 tff('#skF_52', type, '#skF_52': (A_option$ * A_option_b_option_bool_fun_fun$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_142', type, '#skF_142': (B_option$ * B_c_option_fun$ * C$) > B$).
% 23.08/7.73 tff(member$c, type, member$c: (B$ * B_set$) > $o).
% 23.08/7.73 tff(sF$, type, sF$: A_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_174', type, '#skF_174': (A_option$ * A_option$ * A_b_fun$ * A_b_fun$) > A$).
% 23.08/7.73 tff(comp$bc, type, comp$bc: (C_c_fun$ * C_c_fun$) > C_c_fun$).
% 23.08/7.73 tff(fun_app$ac, type, fun_app$ac: (B_b_option_fun_b_option_fun$ * B_b_option_fun$) > B_option$).
% 23.08/7.73 tff('#skF_23', type, '#skF_23': B_option$ > B$).
% 23.08/7.73 tff(comp$bl, type, comp$bl: (B_option_b_fun$ * B_b_sum_b_option_fun$) > B_b_sum_b_fun$).
% 23.08/7.73 tff('#skF_53', type, '#skF_53': (A_option$ * A_option_a_option_bool_fun_fun$ * A_option$) > A$).
% 23.08/7.73 tff(uuo$, type, uuo$: (Bool_c_option_fun$ * C_bool_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(uva$, type, uva$: B_b_b_fun_fun$ > B_b_b_option_fun_fun$).
% 23.08/7.73 tff(uuv$, type, uuv$: (A_b_b_option_fun_fun$ * B$) > A_b_option_fun$).
% 23.08/7.73 tff('#skF_176', type, '#skF_176': (B_option$ * B_option$ * B_c_fun$ * B_c_fun$) > B$).
% 23.08/7.73 tff(fun_app$bk, type, fun_app$bk: (A_c_fun$ * A$) > C$).
% 23.08/7.73 tff(comp$e, type, comp$e: (A_a_option_fun$ * A_a_fun$) > A_a_option_fun$).
% 23.08/7.73 tff(case_option$b, type, case_option$b: (A_option$ * A_a_option_fun$ * A_option$) > A_option$).
% 23.08/7.73 tff('#skF_147', type, '#skF_147': (B_option$ * B_option$ * B_b_option_fun$ * B_b_option_fun$) > B$).
% 23.08/7.73 tff('#skF_73', type, '#skF_73': (C_c_option_fun_c_c_option_fun_fun$ * C_c_fun$ * C_c_c_option_fun_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(comp$bm, type, comp$bm: (C_option_c_fun$ * C_c_sum_c_option_fun$) > C_c_sum_c_fun$).
% 23.08/7.73 tff('#skF_11', type, '#skF_11': (B_a_fun$ * A_b_b_fun_fun$) > B$).
% 23.08/7.73 tff(comp$bd, type, comp$bd: (C_c_fun$ * C_option_c_fun$) > C_option_c_fun$).
% 23.08/7.73 tff('#skF_204', type, '#skF_204': B_set$ > B$).
% 23.08/7.73 tff(none$, type, none$: C_option$).
% 23.08/7.73 tff('#skF_38', type, '#skF_38': C_c_option_fun_b_b_option_fun_fun$ > C_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_156', type, '#skF_156': (A_option$ * A_a_fun$) > A$).
% 23.08/7.73 tff('#skF_75', type, '#skF_75': C_c_option_fun_c_c_option_fun_fun$ > C_c_fun$).
% 23.08/7.73 tff(register_from_getter_setter$d, type, register_from_getter_setter$d: (C_c_fun$ * C_c_c_fun_fun$) > C_c_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff('#skF_108', type, '#skF_108': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_88', type, '#skF_88': (A_b_fun$ * A_option$ * B$) > A$).
% 23.08/7.73 tff('#skF_165', type, '#skF_165': (B_option$ * B_option$ * B_b_fun$ * B_b_fun$) > B$).
% 23.08/7.73 tff('#skF_175', type, '#skF_175': (A_option$ * A_option$ * A_a_fun$ * A_a_fun$) > A$).
% 23.08/7.73 tff(fun_app$bj, type, fun_app$bj: (B_option_a_option_fun$ * B_option$) > A_option$).
% 23.08/7.73 tff(setter$, type, setter$: B_b_option_fun_c_c_option_fun_fun$ > B_c_c_fun_fun$).
% 23.08/7.73 tff(the$d, type, the$d: B_bool_fun$ > B$).
% 23.08/7.73 tff(uub$, type, uub$: A_bool_fun$).
% 23.08/7.73 tff(bot$b, type, bot$b: C_option_set$).
% 23.08/7.73 tff(register_apply$, type, register_apply$: (A_a_option_fun_b_b_option_fun_fun$ * A_a_fun$) > B_b_fun$).
% 23.08/7.73 tff(is_none$, type, is_none$: B_option_bool_fun$).
% 23.08/7.73 tff(is_none$b, type, is_none$b: A_option_bool_fun$).
% 23.08/7.73 tff('#skF_138', type, '#skF_138': (C_option$ * C_a_option_fun$ * A$) > C$).
% 23.08/7.73 tff(the$f, type, the$f: C_option_option$ > C_option$).
% 23.08/7.73 tff(fun_app$at, type, fun_app$at: (C_c_option_fun_b_b_option_fun_fun$ * C_c_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff(uvb$, type, uvb$: (B_b_b_fun_fun$ * B_option$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_60', type, '#skF_60': (B_option$ * B_option_c_option_bool_fun_fun$ * C_option$) > C$).
% 23.08/7.73 tff('#skF_70', type, '#skF_70': (B_b_option_fun_b_b_option_fun_fun$ * B_b_fun$ * B_b_b_option_fun_fun$) > B$).
% 23.08/7.73 tff('#skF_21', type, '#skF_21': A_option$ > A$).
% 23.08/7.73 tff(fun_app$k, type, fun_app$k: (C_c_fun$ * C$) > C$).
% 23.08/7.73 tff(def_9, type, def_9: (Bool_bool_fun$ * tlbool) > tlbool).
% 23.08/7.73 tff(uug$, type, uug$: B_bool_fun$).
% 23.08/7.73 tff(insert$a, type, insert$a: (C$ * C_set$) > C_set$).
% 23.08/7.73 tff(comp$s, type, comp$s: (B_a_fun$ * A_b_fun$) > A_a_fun$).
% 23.08/7.73 tff(fun_upd$, type, fun_upd$: (A_a_fun$ * A$) > A_a_a_fun_fun$).
% 23.08/7.73 tff(uuu$, type, uuu$: (B_c_c_option_fun_fun$ * C$) > B_c_option_fun$).
% 23.08/7.73 tff('#skF_146', type, '#skF_146': (C_option$ * C_option$ * C_c_option_fun$ * C_c_option_fun$) > C$).
% 23.08/7.73 tff(comp$az, type, comp$az: (A_option_b_option_fun$ * B_a_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff(preregister$b, type, preregister$b: B_b_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff(uuc$, type, uuc$: C_bool_fun$).
% 23.08/7.73 tff(uur$, type, uur$: B$ > A_b_option_fun$).
% 23.08/7.73 tff('#skF_110', type, '#skF_110': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(uua$, type, uua$: (A_b_b_fun_fun$ * B$) > A_b_option_fun$).
% 23.08/7.73 tff(fun_app$h, type, fun_app$h: (B_b_fun$ * B$) > B$).
% 23.08/7.73 tff(def_11, type, def_11: (tlbool * B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff(uvl$, type, uvl$: C_option_set$ > C_option_bool_fun$).
% 23.08/7.73 tff('#skF_203', type, '#skF_203': C_option_set$ > C_option$).
% 23.08/7.73 tff(register_from_getter_setter$, type, register_from_getter_setter$: (B_a_fun$ * A_b_b_fun_fun$) > A_a_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff(preregister$a, type, preregister$a: C_c_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_45', type, '#skF_45': (C_option$ * C_option_a_option_bool_fun_fun$ * A_option$) > C$).
% 23.08/7.73 tff(def_8, type, def_8: (tlbool * C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff('#skF_207', type, '#skF_207': C_option_set$ > C_option$).
% 23.08/7.73 tff('#skF_190', type, '#skF_190': B_option_bool_fun$ > B_option$).
% 23.08/7.73 tff('#skF_192', type, '#skF_192': B_bool_fun$ > B$).
% 23.08/7.73 tff(is_empty$b, type, is_empty$b: B_option_set$ > $o).
% 23.08/7.73 tff(uwg$, type, uwg$: C_option_bool_fun$).
% 23.08/7.73 tff(register$b, type, register$b: C_c_option_fun_a_a_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_188', type, '#skF_188': B_bool_fun$ > B$).
% 23.08/7.73 tff(collect$b, type, collect$b: B_option_bool_fun$ > B_option_set$).
% 23.08/7.73 tff(map_option$c, type, map_option$c: C_c_fun$ > C_option_c_option_fun$).
% 23.08/7.73 tff(fun_app$bi, type, fun_app$bi: (C_option_a_option_fun$ * C_option$) > A_option$).
% 23.08/7.73 tff(case_option$k, type, case_option$k: (C$ * C_c_fun$) > C_option_c_fun$).
% 23.08/7.73 tff('#skF_46', type, '#skF_46': (C_option$ * C_option_a_option_bool_fun_fun$ * A_option$) > A$).
% 23.08/7.73 tff(member$a, type, member$a: (B_option$ * B_option_set$) > $o).
% 23.08/7.73 tff(comp$ak, type, comp$ak: (B_b_option_fun_c_c_option_fun_fun$ * B_b_option_fun_b_b_option_fun_fun$) > B_b_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff('#skF_167', type, '#skF_167': (C_option$ * C_option$ * C_b_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(comp$l, type, comp$l: (C_bool_fun$ * C_c_fun$) > C_bool_fun$).
% 23.08/7.73 tff(combine_options$b, type, combine_options$b: (B_b_b_fun_fun$ * B_option$) > B_option_b_option_fun$).
% 23.08/7.73 tff(uvo$, type, uvo$: A_a_a_fun_fun$).
% 23.08/7.73 tff(uvx$, type, uvx$: (B_b_option_fun$ * B_c_option_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(case_sum$c, type, case_sum$c: (B_c_option_fun$ * B_c_option_fun$) > B_b_sum_c_option_fun$).
% 23.08/7.73 tff('#skF_8', type, '#skF_8': (C_b_fun$ * B_c_c_fun_fun$) > C$).
% 23.08/7.73 tff(register$d, type, register$d: A_a_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_42', type, '#skF_42': B_b_option_fun_c_c_option_fun_fun$ > B_c_c_fun_fun$).
% 23.08/7.73 tff(these$a, type, these$a: B_option_set$ > B_set$).
% 23.08/7.73 tff(uue$, type, uue$: A_bool_fun$).
% 23.08/7.73 tff(fun_app$bf, type, fun_app$bf: (A_option_a_fun$ * A_option$) > A$).
% 23.08/7.73 tff('#skF_157', type, '#skF_157': (B_option$ * B_b_fun$) > B$).
% 23.08/7.73 tff(case_option$j, type, case_option$j: (B$ * B_b_fun$) > B_option_b_fun$).
% 23.08/7.73 tff(def_21, type, def_21: (B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff('#skF_206', type, '#skF_206': B_option_set$ > B_option$).
% 23.08/7.73 tff(def_2, type, def_2: (B_bool_fun$ * B$) > tlbool).
% 23.08/7.73 tff(register$a, type, register$a: B_b_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_15', type, '#skF_15': A_option$ > A$).
% 23.08/7.73 tff(comp$al, type, comp$al: (B_b_option_fun_b_b_option_fun_fun$ * A_a_option_fun_b_b_option_fun_fun$) > A_a_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff(tlfalse, type, tlfalse: tlbool).
% 23.08/7.73 tff(fun_app$ag, type, fun_app$ag: (Bool_bool_fun$ * tlbool) > $o).
% 23.08/7.73 tff('#skF_103', type, '#skF_103': (C_c_c_fun_fun$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(fun_app$bh, type, fun_app$bh: (A_option_c_option_fun$ * A_option$) > C_option$).
% 23.08/7.73 tff(def_17, type, def_17: (B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff(uvi$, type, uvi$: B_set$ > B_bool_fun$).
% 23.08/7.73 tff('#skF_27', type, '#skF_27': C_option_bool_fun$ > C$).
% 23.08/7.73 tff('#skF_30', type, '#skF_30': A_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_141', type, '#skF_141': (C_option$ * C_c_option_fun$ * C$) > C$).
% 23.08/7.73 tff(uwl$, type, uwl$: B$ > B_bool_fun$).
% 23.08/7.73 tff(comp$n, type, comp$n: (C_option_c_fun$ * C_c_option_fun$) > C_c_fun$).
% 23.08/7.73 tff(uwh$, type, uwh$: B_option$ > A_b_option_fun$).
% 23.08/7.73 tff(map_option$l, type, map_option$l: (C_c_option_fun$ * C_option$) > C_option_option$).
% 23.08/7.73 tff(is_empty$a, type, is_empty$a: C_set$ > $o).
% 23.08/7.73 tff(register$c, type, register$c: B_b_option_fun_a_a_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_120', type, '#skF_120': (B_option$ * B_option$ * B_b_fun$ * B_b_fun$) > B$).
% 23.08/7.73 tff('#skF_113', type, '#skF_113': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(fun_app$bc, type, fun_app$bc: (C_option_b_option_bool_fun_fun$ * C_option$) > B_option_bool_fun$).
% 23.08/7.73 tff('#skF_123', type, '#skF_123': (A_option_bool_fun$ * C_option$ * C_a_option_fun$) > C$).
% 23.08/7.73 tff('#skF_84', type, '#skF_84': A_a_option_fun_b_b_option_fun_fun$ > A_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_172', type, '#skF_172': (B_option$ * B_b_fun$ * B_b_fun$) > B$).
% 23.08/7.73 tff(fun_app$v, type, fun_app$v: (C_c_c_option_fun_fun$ * C$) > C_c_option_fun$).
% 23.08/7.73 tff('#skF_83', type, '#skF_83': A_a_option_fun_b_b_option_fun_fun$ > B_a_fun$).
% 23.08/7.73 tff(uui$, type, uui$: (B_option_b_option_fun$ * A_b_option_fun$) > A_b_option_fun$).
% 23.08/7.73 tff(these$, type, these$: C_option_set$ > C_set$).
% 23.08/7.73 tff(comp$y, type, comp$y: (C_b_fun$ * B_c_fun$) > B_b_fun$).
% 23.08/7.73 tff(insert$c, type, insert$c: (C_option$ * C_option_set$) > C_option_set$).
% 23.08/7.73 tff(fun_app$y, type, fun_app$y: (B_c_c_fun_fun$ * B$) > C_c_fun$).
% 23.08/7.73 tff('#skF_43', type, '#skF_43': A_a_option_fun_b_b_option_fun_fun$ > B_a_fun$).
% 23.08/7.73 tff(def_20, type, def_20: (tlbool * B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff('#skF_125', type, '#skF_125': (C_option_bool_fun$ * A_option$ * A_c_option_fun$) > A$).
% 23.08/7.73 tff('#skF_34', type, '#skF_34': (tlbool * B_bool_fun$ * B_option$) > B$).
% 23.08/7.73 tff(comp$au, type, comp$au: (C_option_b_option_fun$ * C_c_option_fun$) > C_b_option_fun$).
% 23.08/7.73 tff('#skF_102', type, '#skF_102': (C_c_c_fun_fun$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(valid_getter_setter$c, type, valid_getter_setter$c: (B_c_fun$ * C_b_b_fun_fun$) > $o).
% 23.08/7.73 tff('#skF_195', type, '#skF_195': C_option_bool_fun$ > C_option$).
% 23.08/7.73 tff(register_apply$a, type, register_apply$a: (B_b_option_fun_c_c_option_fun_fun$ * B_b_fun$) > C_c_fun$).
% 23.08/7.73 tff('#skF_140', type, '#skF_140': (A_option$ * A_a_option_fun$ * A$) > A$).
% 23.08/7.73 tff(inj_on$a, type, inj_on$a: (B_b_option_fun$ * B_set$) > $o).
% 23.08/7.73 tff('#skF_97', type, '#skF_97': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(uvy$, type, uvy$: (C_b_option_fun$ * B_c_option_fun$) > C_c_option_fun$).
% 23.08/7.73 tff('#skF_191', type, '#skF_191': C_option_bool_fun$ > C_option$).
% 23.08/7.73 tff(fun_upd$a, type, fun_upd$a: (A_b_option_fun$ * A$ * B_option$) > A_b_option_fun$).
% 23.08/7.73 tff('#skF_16', type, '#skF_16': C_option$ > C$).
% 23.08/7.73 tff('#skF_63', type, '#skF_63': A_option_bool_fun$ > A$).
% 23.08/7.73 tff(uve$, type, uve$: B_b_fun$ > B_b_option_fun$).
% 23.08/7.73 tff('#skF_89', type, '#skF_89': (A_a_fun$ * A_option$ * A$) > A$).
% 23.08/7.73 tff(map_option$b, type, map_option$b: B_b_fun$ > B_option_b_option_fun$).
% 23.08/7.73 tff(bot$d, type, bot$d: B_set$).
% 23.08/7.73 tff(uud$, type, uud$: B_bool_fun$).
% 23.08/7.73 tff(fun_app$z, type, fun_app$z: (A_bool_fun$ * A$) > $o).
% 23.08/7.73 tff('#skF_144', type, '#skF_144': (B_option$ * B_b_option_fun$ * B$) > B$).
% 23.08/7.73 tff(case_option$g, type, case_option$g: (tlbool * A_bool_fun$) > A_option_bool_fun$).
% 23.08/7.73 tff(case_option$h, type, case_option$h: (B_option$ * C_b_option_fun$ * C_option$) > B_option$).
% 23.08/7.73 tff(uwc$, type, uwc$: C_c_option_fun$).
% 23.08/7.73 tff('#skF_199', type, '#skF_199': C_option_set$ > C_option$).
% 23.08/7.73 tff(bind$c, type, bind$c: B_option$ > B_b_option_fun_b_option_fun$).
% 23.08/7.73 tff('#skF_85', type, '#skF_85': (A_c_fun$ * A_option$ * C$) > A$).
% 23.08/7.73 tff('#skF_143', type, '#skF_143': (C_option$ * C_b_option_fun$ * B$) > C$).
% 23.08/7.73 tff(def_15, type, def_15: (C_option_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff(fun_app$ah, type, fun_app$ah: (C_c_c_fun_fun$ * C$) > C_c_fun$).
% 23.08/7.73 tff(id$d, type, id$d: B_option_b_option_fun$).
% 23.08/7.73 tff(fun_app$g, type, fun_app$g: (B_b_option_fun$ * B$) > B_option$).
% 23.08/7.73 tff(the$b, type, the$b: A_option_a_fun$).
% 23.08/7.73 tff(uuz$, type, uuz$: (C_c_c_fun_fun$ * C_option$) > C_c_option_fun$).
% 23.08/7.73 tff(none$c, type, none$c: B_option_option$).
% 23.08/7.73 tff('#skF_205', type, '#skF_205': C_set$ > C$).
% 23.08/7.73 tff('#skF_35', type, '#skF_35': B_b_option_fun_b_b_option_fun_fun$ > B_b_fun$).
% 23.08/7.73 tff(fun_app$b, type, fun_app$b: (C_bool_fun$ * C$) > $o).
% 23.08/7.73 tff(def_7, type, def_7: (Bool_bool_fun$ * tlbool) > tlbool).
% 23.08/7.73 tff(bind$h, type, bind$h: A_option$ > A_a_option_fun_a_option_fun$).
% 23.08/7.73 tff(comp$af, type, comp$af: (B_option_b_option_fun$ * C_option_b_option_fun$) > C_option_b_option_fun$).
% 23.08/7.73 tff(comp$j, type, comp$j: (B_bool_fun$ * C_b_fun$) > C_bool_fun$).
% 23.08/7.73 tff(comp$bb, type, comp$bb: (B_b_fun$ * B_option_b_fun$) > B_option_b_fun$).
% 23.08/7.73 tff(def_5, type, def_5: (B_bool_fun$ * B$) > tlbool).
% 23.08/7.73 tff(comp$ax, type, comp$ax: B_option_b_option_fun$ > B_b_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_10', type, '#skF_10': (B_a_fun$ * A_b_b_fun_fun$) > A$).
% 23.08/7.73 tff(bot$c, type, bot$c: C_set$).
% 23.08/7.73 tff('#skF_77', type, '#skF_77': (B_b_option_fun_c_c_option_fun_fun$ * C_b_fun$ * B_c_c_option_fun_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_121', type, '#skF_121': (A_option$ * A_option$ * A_b_fun$ * A_b_fun$) > A$).
% 23.08/7.73 tff(fun_app$bm, type, fun_app$bm: (A_c_option_fun$ * A$) > C_option$).
% 23.08/7.73 tff(id$, type, id$: A_a_fun$).
% 23.08/7.73 tff('#skF_65', type, '#skF_65': C_option_bool_fun$ > C$).
% 23.08/7.73 tff(comp$ay, type, comp$ay: (B_option_b_option_fun$ * C_b_option_fun$) > C_b_option_fun$).
% 23.08/7.73 tff(uwd$, type, uwd$: B_b_option_fun$).
% 23.08/7.73 tff(g$, type, g$: B_b_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff('#skF_112', type, '#skF_112': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(bot$, type, bot$: A_set$).
% 23.08/7.73 tff(case_sum$d, type, case_sum$d: (B_b_option_fun$ * B_b_option_fun$) > B_b_sum_b_option_fun$).
% 23.08/7.73 tff(map_option$a, type, map_option$a: A_a_fun$ > A_option_a_option_fun$).
% 23.08/7.73 tff(fun_upd$e, type, fun_upd$e: (C_c_option_fun$ * C$ * C_option$) > C_c_option_fun$).
% 23.08/7.73 tff('#skF_115', type, '#skF_115': (A_a_option_fun_b_b_option_fun_fun$ * A_a_option_fun_b_b_option_fun_fun$) > A$).
% 23.08/7.73 tff(uwn$, type, uwn$: B_option_b_option_bool_fun_fun$).
% 23.08/7.73 tff('#skF_154', type, '#skF_154': (B_option_option$ * B_option_b_option_fun$) > B_option$).
% 23.08/7.73 tff(fun_app$e, type, fun_app$e: (B_option_b_option_bool_fun_fun$ * B_option$) > B_option_bool_fun$).
% 23.08/7.73 tff('#skF_78', type, '#skF_78': (B_b_option_fun_c_c_option_fun_fun$ * C_b_fun$ * B_c_c_option_fun_fun$) > C$).
% 23.08/7.73 tff(top$, type, top$: C_option_set$).
% 23.08/7.73 tff(bot$f, type, bot$f: C_bool_fun$).
% 23.08/7.73 tff(collect$, type, collect$: B_bool_fun$ > B_set$).
% 23.08/7.73 tff(map_option$k, type, map_option$k: (B_b_option_fun$ * B_option$) > B_option_option$).
% 23.08/7.73 tff(uvw$, type, uvw$: (C_c_option_fun$ * C_b_option_fun$) > C_b_option_fun$).
% 23.08/7.73 tff('#skF_202', type, '#skF_202': B_option_set$ > B_option$).
% 23.08/7.73 tff('#skF_119', type, '#skF_119': (B_option$ * B_option$ * B_c_fun$ * B_c_fun$) > B$).
% 23.08/7.73 tff(case_option$, type, case_option$: (B_option$ * B_b_option_fun$) > B_option_b_option_fun$).
% 23.08/7.73 tff(uuy$, type, uuy$: C_c_c_fun_fun$ > C_c_c_option_fun_fun$).
% 23.08/7.73 tff(fun_app$bd, type, fun_app$bd: (B_option_c_option_bool_fun_fun$ * B_option$) > C_option_bool_fun$).
% 23.08/7.73 tff(uu$, type, uu$: (B_c_c_fun_fun$ * C$) > B_c_option_fun$).
% 23.08/7.73 tff(comp$h, type, comp$h: (B_bool_fun$ * A_b_fun$) > A_bool_fun$).
% 23.08/7.73 tff(comp$t, type, comp$t: (C_option_b_option_fun$ * C_option_c_option_fun$) > C_option_b_option_fun$).
% 23.08/7.73 tff(fun_app$ad, type, fun_app$ad: (B_b_option_fun_b_b_option_fun_fun$ * B_b_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_48', type, '#skF_48': (B_option$ * B_option_a_option_bool_fun_fun$ * A_option$) > A$).
% 23.08/7.73 tff('#skF_134', type, '#skF_134': (C_option$ * C_option$ * C_b_option_fun$ * C_b_option_fun$) > C$).
% 23.08/7.73 tff(def_13, type, def_13: (tlbool * C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff('#skF_159', type, '#skF_159': (A_option$ * A_option$ * A_b_fun$ * A_b_fun$) > A$).
% 23.08/7.73 tff(fun_app$ai, type, fun_app$ai: (B_b_b_fun_fun$ * B$) > B_b_fun$).
% 23.08/7.73 tff(comp$aw, type, comp$aw: (B_option_c_option_fun$ * C_b_option_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(case_option$c, type, case_option$c: (C_option$ * B_c_option_fun$) > B_option_c_option_fun$).
% 23.08/7.73 tff('#skF_200', type, '#skF_200': B_set$ > B$).
% 23.08/7.73 tff(def_16, type, def_16: (tlbool * B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff('#skF_86', type, '#skF_86': (C_a_fun$ * C_option$ * A$) > C$).
% 23.08/7.73 tff(fun_app$p, type, fun_app$p: (A_b_fun$ * A$) > B$).
% 23.08/7.73 tff(uvk$, type, uvk$: B_option_set$ > B_option_bool_fun$).
% 23.08/7.73 tff('#skF_62', type, '#skF_62': (B_option$ * B_option_b_option_bool_fun_fun$ * B_option$) > B$).
% 23.08/7.73 tff(fun_app$bp, type, fun_app$bp: (A_a_option_fun_a_option_fun$ * A_a_option_fun$) > A_option$).
% 23.08/7.73 tff('#skF_106', type, '#skF_106': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff(comp$bk, type, comp$bk: (B_c_option_fun$ * B_b_sum_b_fun$) > B_b_sum_c_option_fun$).
% 23.08/7.73 tff('#skF_33', type, '#skF_33': (tlbool * C_bool_fun$ * C_option$) > C$).
% 23.08/7.73 tff(register$f, type, register$f: C_c_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff(the$c, type, the$c: A_bool_fun$ > A$).
% 23.08/7.73 tff(comp$aa, type, comp$aa: (B_c_fun$ * C_b_fun$) > C_c_fun$).
% 23.08/7.73 tff(bot$g, type, bot$g: B_option_bool_fun$).
% 23.08/7.73 tff('#skF_40', type, '#skF_40': C_c_option_fun_c_c_option_fun_fun$ > C_c_c_fun_fun$).
% 23.08/7.73 tff(insert$b, type, insert$b: (B_option$ * B_option_set$) > B_option_set$).
% 23.08/7.73 tff(fun_app$ae, type, fun_app$ae: (Bool_c_option_fun$ * tlbool) > C_option$).
% 23.08/7.73 tff(preregister$, type, preregister$: B_b_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff(comp$a, type, comp$a: (B_b_option_fun$ * C_b_fun$) > C_b_option_fun$).
% 23.08/7.73 tff('#skF_194', type, '#skF_194': B_option_bool_fun$ > B_option$).
% 23.08/7.73 tff('#skF_2', type, '#skF_2': (B_c_c_fun_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(fun_app$bl, type, fun_app$bl: (C_a_fun$ * C$) > A$).
% 23.08/7.73 tff(top$b, type, top$b: B_option_set$).
% 23.08/7.73 tff('#skF_150', type, '#skF_150': (C_option_option$ * C_option_bool_fun$ * C_option$) > C_option$).
% 23.08/7.73 tff('#skF_186', type, '#skF_186': (C_option_bool_fun$ * B_option$ * B_c_option_fun$) > B$).
% 23.08/7.73 tff(def_4, type, def_4: (C_bool_fun$ * C$) > tlbool).
% 23.08/7.73 tff(f$, type, f$: A_a_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff(fun_app$l, type, fun_app$l: (C_b_option_fun$ * C$) > B_option$).
% 23.08/7.73 tff(uwk$, type, uwk$: C$ > C_option_c_fun$).
% 23.08/7.73 tff(comp$z, type, comp$z: (B_option_c_option_fun$ * C_option_b_option_fun$) > C_option_c_option_fun$).
% 23.08/7.73 tff(fun_app$an, type, fun_app$an: (B_option_c_option_fun$ * B_option$) > C_option$).
% 23.08/7.73 tff(comp$w, type, comp$w: (C_b_fun$ * A_c_fun$) > A_b_fun$).
% 23.08/7.73 tff(uum$, type, uum$: (Bool_c_option_fun$ * B_bool_fun$) > B_c_option_fun$).
% 23.08/7.73 tff('#skF_29', type, '#skF_29': B_option_bool_fun$ > B$).
% 23.08/7.73 tff(register$e, type, register$e: A_a_option_fun_a_a_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_158', type, '#skF_158': (C_option$ * C_c_fun$) > C$).
% 23.08/7.73 tff('#skF_82', type, '#skF_82': (A_a_option_fun_b_b_option_fun_fun$ * B_a_fun$ * A_b_b_option_fun_fun$) > B$).
% 23.08/7.73 tff(comp$bf, type, comp$bf: (B_option_b_option_fun$ * A_b_option_fun$) > A_b_option_fun$).
% 23.08/7.73 tff('#skF_129', type, '#skF_129': (B_option_bool_fun$ * C_option$ * C_b_option_fun$) > C$).
% 23.08/7.73 tff(id$b, type, id$b: B_b_fun$).
% 23.08/7.73 tff(none$b, type, none$b: A_option$).
% 23.08/7.73 tff(case_option$d, type, case_option$d: (B_option$ * A_b_option_fun$) > A_option_b_option_fun$).
% 23.08/7.73 tff(uvt$, type, uvt$: B_b_option_fun$ > B_b_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_155', type, '#skF_155': (C_option_option$ * C_option_c_option_fun$) > C_option$).
% 23.08/7.73 tff('#skF_163', type, '#skF_163': (B_option$ * B_option$ * B_c_fun$ * B_c_fun$) > B$).
% 23.08/7.73 tff('#skF_177', type, '#skF_177': (B_option$ * B_option$ * B_b_fun$ * B_b_fun$) > B$).
% 23.08/7.73 tff('#skF_44', type, '#skF_44': A_a_option_fun_b_b_option_fun_fun$ > A_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_151', type, '#skF_151': (A_option$ * A_bool_fun$ * A$) > A$).
% 23.08/7.73 tff(update1$b, type, update1$b: B$ > B_b_b_option_fun_fun$).
% 23.08/7.73 tff(collect$c, type, collect$c: C_option_bool_fun$ > C_option_set$).
% 23.08/7.73 tff('#skF_98', type, '#skF_98': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(uun$, type, uun$: (Bool_b_option_fun$ * B_bool_fun$) > B_b_option_fun$).
% 23.08/7.73 tff(uwb$, type, uwb$: B_c_option_fun$).
% 23.08/7.73 tff(comp$at, type, comp$at: (C_option_b_option_fun$ * B_c_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff(fun_app$j, type, fun_app$j: (C_c_option_fun$ * C$) > C_option$).
% 23.08/7.73 tff('#skF_183', type, '#skF_183': (A_option_bool_fun$ * A_option$ * A_a_option_fun$) > A$).
% 23.08/7.73 tff('#skF_196', type, '#skF_196': B_set$ > B$).
% 23.08/7.73 tff(top$c, type, top$c: B_set$).
% 23.08/7.73 tff(bind$a, type, bind$a: (C_option$ * C_b_option_fun$) > B_option$).
% 23.08/7.73 tff(comp$be, type, comp$be: (A_a_fun$ * A_a_fun$) > A_a_fun$).
% 23.08/7.73 tff('#skF_74', type, '#skF_74': (C_c_option_fun_c_c_option_fun_fun$ * C_c_fun$ * C_c_c_option_fun_fun$) > C$).
% 23.08/7.73 tff(bind$d, type, bind$d: (A_option$ * A_c_option_fun$) > C_option$).
% 23.08/7.73 tff(uvg$, type, uvg$: B_c_fun$ > B_c_option_fun$).
% 23.08/7.73 tff('#skF_18', type, '#skF_18': A_option$ > A$).
% 23.08/7.73 tff(fun_app$i, type, fun_app$i: (A_b_b_fun_fun$ * A$) > B_b_fun$).
% 23.08/7.73 tff(gF$, type, gF$: B_a_fun$).
% 23.08/7.73 tff(comp$m, type, comp$m: (B_option_b_fun$ * B_b_option_fun$) > B_b_fun$).
% 23.08/7.73 tff(fun_app$, type, fun_app$: (C_option_bool_fun$ * C_option$) > $o).
% 23.08/7.73 tff(some$, type, some$: B_b_option_fun$).
% 23.08/7.73 tff(combine_options$a, type, combine_options$a: (C_c_c_fun_fun$ * C_option$) > C_option_c_option_fun$).
% 23.08/7.73 tff(uuj$, type, uuj$: (Bool_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 23.08/7.73 tff(preregister$d, type, preregister$d: C_c_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff(case_sum$, type, case_sum$: (A_a_fun$ * A_a_fun$) > A_a_sum_a_fun$).
% 23.08/7.73 tff('#skF_94', type, '#skF_94': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_139', type, '#skF_139': (B_option$ * B_a_option_fun$ * A$) > B$).
% 23.08/7.73 tff('#skF_128', type, '#skF_128': (C_option_bool_fun$ * C_option$ * C_c_option_fun$) > C$).
% 23.08/7.73 tff(fun_app$u, type, fun_app$u: (C_option_c_option_fun$ * C_option$) > C_option$).
% 23.08/7.73 tff(comp$an, type, comp$an: (C_c_option_fun_c_c_option_fun_fun$ * B_b_option_fun_c_c_option_fun_fun$) > B_b_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff(register_from_getter_setter$a, type, register_from_getter_setter$a: (C_b_fun$ * B_c_c_fun_fun$) > B_b_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff('#skF_135', type, '#skF_135': (C_option$ * C_option$ * C_c_option_fun$ * C_c_option_fun$) > C$).
% 23.08/7.73 tff('#skF_26', type, '#skF_26': C_option_bool_fun$ > C_option$).
% 23.08/7.73 tff(comp$ar, type, comp$ar: (C_option_c_option_fun$ * B_c_option_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(case_sum$b, type, case_sum$b: (B_b_fun$ * B_b_fun$) > B_b_sum_b_fun$).
% 23.08/7.73 tff(case_option$l, type, case_option$l: (B$ * B_option_b_fun$ * B_option_option$) > B$).
% 23.08/7.73 tff(uvj$, type, uvj$: C_set$ > C_bool_fun$).
% 23.08/7.73 tff('#skF_59', type, '#skF_59': (B_option$ * B_option_c_option_bool_fun_fun$ * C_option$) > B$).
% 23.08/7.73 tff(fun_app$ar, type, fun_app$ar: (A_a_option_fun_c_c_option_fun_fun$ * A_a_option_fun$) > C_c_option_fun$).
% 23.08/7.73 tff('#skF_49', type, '#skF_49': (A_option$ * A_option_c_option_bool_fun_fun$ * C_option$) > A$).
% 23.08/7.73 tff(uup$, type, uup$: (B_option_bool_fun$ * B_b_option_fun$) > B_bool_fun$).
% 23.08/7.73 tff('#skF_5', type, '#skF_5': (C_b_fun$ * B_c_c_fun_fun$) > C$).
% 23.08/7.73 tff(uwf$, type, uwf$: B_option_bool_fun$).
% 23.08/7.73 tff('#skF_127', type, '#skF_127': (A_option_bool_fun$ * A_option$ * A_a_option_fun$) > A$).
% 23.08/7.73 tff(some$a, type, some$a: C_c_option_fun$).
% 23.08/7.73 tff('#skF_92', type, '#skF_92': (C_b_fun$ * C_option$ * B$) > C$).
% 23.08/7.73 tff(fun_app$x, type, fun_app$x: (A_b_b_option_fun_fun$ * A$) > B_b_option_fun$).
% 23.08/7.73 tff(comp$aq, type, comp$aq: (B_c_option_fun$ * A_b_fun$) > A_c_option_fun$).
% 23.08/7.73 tff(comp$u, type, comp$u: (C_b_fun$ * C_c_fun$) > C_b_fun$).
% 23.08/7.73 tff(fun_app$az, type, fun_app$az: (A_option_c_option_bool_fun_fun$ * A_option$) > C_option_bool_fun$).
% 23.08/7.73 tff(fun_app$t, type, fun_app$t: (B_b_b_option_fun_fun$ * B$) > B_b_option_fun$).
% 23.08/7.73 tff(uul$, type, uul$: (C_option_bool_fun$ * B_c_option_fun$) > B_bool_fun$).
% 23.08/7.73 tff(uwe$, type, uwe$: C_b_option_fun$).
% 23.08/7.73 tff(combine_options$, type, combine_options$: (A_a_a_fun_fun$ * A_option$) > A_option_a_option_fun$).
% 23.08/7.73 tff(uvr$, type, uvr$: (B_b_option_fun_c_c_option_fun_fun$ * C$) > B_bool_fun$).
% 23.08/7.73 tff('#skF_9', type, '#skF_9': (B_a_fun$ * A_b_b_fun_fun$) > B$).
% 23.08/7.73 tff(fun_app$q, type, fun_app$q: (A_a_option_fun$ * A$) > A_option$).
% 23.08/7.73 tff('#skF_19', type, '#skF_19': C_option$ > C$).
% 23.08/7.73 tff('#skF_101', type, '#skF_101': (B_b_b_fun_fun$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff(fun_app$f, type, fun_app$f: (A_b_option_fun$ * A$) > B_option$).
% 23.08/7.73 tff(comp$o, type, comp$o: (C_b_option_fun$ * B_c_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_58', type, '#skF_58': (C_option$ * C_option_b_option_bool_fun_fun$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_24', type, '#skF_24': A_option_bool_fun$ > A_option$).
% 23.08/7.73 tff(register$g, type, register$g: C_c_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff(uuh$, type, uuh$: (C_option_c_option_fun$ * B_c_option_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(comp$bh, type, comp$bh: (B_option_b_fun$ * B_option_b_option_fun$) > B_option_b_fun$).
% 23.08/7.73 tff(comp$aj, type, comp$aj: (A_a_option_fun_b_b_option_fun_fun$ * A_a_option_fun_a_a_option_fun_fun$) > A_a_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff(map_option$h, type, map_option$h: B_a_fun$ > B_option_a_option_fun$).
% 23.08/7.73 tff(fun_app$ba, type, fun_app$ba: (A_option_b_option_bool_fun_fun$ * A_option$) > B_option_bool_fun$).
% 23.08/7.73 tff('#skF_71', type, '#skF_71': B_b_option_fun_b_b_option_fun_fun$ > B_b_fun$).
% 23.08/7.73 tff('#skF_197', type, '#skF_197': C_set$ > C$).
% 23.08/7.73 tff(def_3, type, def_3: (B_bool_fun$ * B$) > tlbool).
% 23.08/7.73 tff(register$h, type, register$h: B_b_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_79', type, '#skF_79': B_b_option_fun_c_c_option_fun_fun$ > C_b_fun$).
% 23.08/7.73 tff(fun_app$bg, type, fun_app$bg: (C_option_b_option_fun$ * C_option$) > B_option$).
% 23.08/7.73 tff(collect$a, type, collect$a: C_bool_fun$ > C_set$).
% 23.08/7.73 tff('#skF_4', type, '#skF_4': (C_b_fun$ * B_c_c_fun_fun$) > B$).
% 23.08/7.73 tff(comp$ba, type, comp$ba: (A_option_b_option_fun$ * C_a_option_fun$) > C_b_option_fun$).
% 23.08/7.73 tff(set_option$a, type, set_option$a: C_option_option$ > C_option_set$).
% 23.08/7.73 tff('#skF_28', type, '#skF_28': B_option_bool_fun$ > B_option$).
% 23.08/7.73 tff(def_22, type, def_22: (tlbool * C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff(comp$, type, comp$: (C_c_option_fun$ * C_c_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(map_option$e, type, map_option$e: A_b_fun$ > A_option_b_option_fun$).
% 23.08/7.73 tff('#skF_51', type, '#skF_51': (A_option$ * A_option_b_option_bool_fun_fun$ * B_option$) > A$).
% 23.08/7.73 tff(uvf$, type, uvf$: C_c_fun$ > C_c_option_fun$).
% 23.08/7.73 tff(case_option$m, type, case_option$m: (C$ * C_option_c_fun$ * C_option_option$) > C$).
% 23.08/7.73 tff(update1$a, type, update1$a: C$ > C_c_c_option_fun_fun$).
% 23.08/7.73 tff(preregister$c, type, preregister$c: A_a_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff(fun_app$be, type, fun_app$be: (A_option_a_option_fun$ * A_option$) > A_option$).
% 23.08/7.73 tff('#skF_161', type, '#skF_161': (A_option$ * A_option$ * A_a_fun$ * A_a_fun$) > A$).
% 23.08/7.73 tff(getter$, type, getter$: B_b_option_fun_c_c_option_fun_fun$ > C_b_fun$).
% 23.08/7.73 tff(uuw$, type, uuw$: (A_a_a_fun_fun$ * A$) > A_a_option_fun$).
% 23.08/7.73 tff(comp$am, type, comp$am: (B_b_option_fun_c_c_option_fun_fun$ * A_a_option_fun_b_b_option_fun_fun$) > A_a_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff(uuk$, type, uuk$: (Bool_bool_fun$ * C_bool_fun$) > C_bool_fun$).
% 23.08/7.73 tff(update1$, type, update1$: (A$ * A$) > A_a_option_fun$).
% 23.08/7.73 tff('#skF_105', type, '#skF_105': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_133', type, '#skF_133': (B_option$ * B_option$ * B_c_option_fun$ * B_c_option_fun$) > B$).
% 23.08/7.73 tff('#skF_50', type, '#skF_50': (A_option$ * A_option_c_option_bool_fun_fun$ * C_option$) > C$).
% 23.08/7.73 tff(is_empty$c, type, is_empty$c: C_option_set$ > $o).
% 23.08/7.73 tff(uuq$, type, uuq$: (C_option_bool_fun$ * C_c_option_fun$) > C_bool_fun$).
% 23.08/7.73 tff(case_sum$a, type, case_sum$a: (A_b_option_fun$ * A_b_option_fun$) > A_a_sum_b_option_fun$).
% 23.08/7.73 tff(uws$, type, uws$: C_option_c_option_bool_fun_fun$).
% 23.08/7.73 tff(uvh$, type, uvh$: A_b_fun$ > A_b_option_fun$).
% 23.08/7.73 tff('#skF_132', type, '#skF_132': (B_option$ * B_option$ * B_b_option_fun$ * B_b_option_fun$) > B$).
% 23.08/7.73 tff(comp$bi, type, comp$bi: (A_option_a_fun$ * A_a_option_fun$) > A_a_fun$).
% 23.08/7.73 tff('#skF_36', type, '#skF_36': B_b_option_fun_b_b_option_fun_fun$ > B_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_12', type, '#skF_12': (B_a_fun$ * A_b_b_fun_fun$) > A$).
% 23.08/7.73 tff(comp$ae, type, comp$ae: (B_c_fun$ * A_b_fun$) > A_c_fun$).
% 23.08/7.73 tff(fun_app$s, type, fun_app$s: (B_option_b_option_fun$ * B_option$) > B_option$).
% 23.08/7.73 tff(the$e, type, the$e: B_option_option$ > B_option$).
% 23.08/7.73 tff(preregister$e, type, preregister$e: A_a_option_fun_a_a_option_fun_fun$ > $o).
% 23.08/7.73 tff('#skF_80', type, '#skF_80': B_b_option_fun_c_c_option_fun_fun$ > B_c_c_option_fun_fun$).
% 23.08/7.73 tff(fun_app$ao, type, fun_app$ao: (B_a_fun$ * B$) > A$).
% 23.08/7.73 tff(member$d, type, member$d: (A$ * A_set$) > $o).
% 23.08/7.73 tff(map_option$i, type, map_option$i: (B_option_b_option_fun$ * B_option_option$) > B_option_option$).
% 23.08/7.73 tff('#skF_170', type, '#skF_170': (A_option$ * A_a_fun$ * A_a_fun$) > A$).
% 23.08/7.73 tff(def_23, type, def_23: (C_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff('#skF_145', type, '#skF_145': (C_option$ * C_option$ * C_b_option_fun$ * C_b_option_fun$) > C$).
% 23.08/7.73 tff('#skF_99', type, '#skF_99': (C_c_c_fun_fun$ * C_option$ * C_option$ * C_option$) > C$).
% 23.08/7.73 tff(comp$d, type, comp$d: (B_b_option_fun$ * A_b_fun$) > A_b_option_fun$).
% 23.08/7.73 tff('#skF_61', type, '#skF_61': (B_option$ * B_option_b_option_bool_fun_fun$ * B_option$) > B$).
% 23.08/7.73 tff(comp$ad, type, comp$ad: (B_option_c_option_fun$ * A_option_b_option_fun$) > A_option_c_option_fun$).
% 23.08/7.73 tff(fun_app$o, type, fun_app$o: (B_c_fun$ * B$) > C$).
% 23.08/7.73 tff('#skF_1', type, '#skF_1': (B_c_c_fun_fun$ * C_b_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_201', type, '#skF_201': C_set$ > C$).
% 23.08/7.73 tff(uvn$, type, uvn$: A_a_fun$).
% 23.08/7.73 tff(comp$i, type, comp$i: (B_bool_fun$ * B_b_fun$) > B_bool_fun$).
% 23.08/7.73 tff(fun_upd$d, type, fun_upd$d: (B_b_option_fun$ * B$ * B_option$) > B_b_option_fun$).
% 23.08/7.73 tff(comp$bj, type, comp$bj: (A_b_option_fun$ * A_a_sum_a_fun$) > A_a_sum_b_option_fun$).
% 23.08/7.73 tff(inj_on$, type, inj_on$: (C_c_option_fun$ * C_set$) > $o).
% 23.08/7.73 tff(uwp$, type, uwp$: B$ > B_bool_fun$).
% 23.08/7.73 tff('#skF_107', type, '#skF_107': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_95', type, '#skF_95': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_76', type, '#skF_76': C_c_option_fun_c_c_option_fun_fun$ > C_c_c_option_fun_fun$).
% 23.08/7.73 tff(comp$b, type, comp$b: (C_c_option_fun$ * B_c_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(uwm$, type, uwm$: C$ > C_bool_fun$).
% 23.08/7.73 tff(member$, type, member$: (C_option$ * C_option_set$) > $o).
% 23.08/7.73 tff(setter$a, type, setter$a: A_a_option_fun_b_b_option_fun_fun$ > A_b_b_fun_fun$).
% 23.08/7.73 tff(set_option$c, type, set_option$c: C_option$ > C_set$).
% 23.08/7.73 tff(uwq$, type, uwq$: C$ > C_bool_fun$).
% 23.08/7.73 tff(uut$, type, uut$: C_c_c_option_fun_fun$ > C_c_c_option_fun_fun$).
% 23.08/7.73 tff(uvu$, type, uvu$: (C_b_option_fun$ * B_b_option_fun$) > C_b_option_fun$).
% 23.08/7.73 tff(comp$r, type, comp$r: (B_option_a_option_fun$ * A_option_b_option_fun$) > A_option_a_option_fun$).
% 23.08/7.73 tff(comp$as, type, comp$as: C_option_c_option_fun$ > C_c_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff(bot$a, type, bot$a: B_option_set$).
% 23.08/7.73 tff('#skF_181', type, '#skF_181': (C_option_bool_fun$ * A_option$ * A_c_option_fun$) > A$).
% 23.08/7.73 tff(uvq$, type, uvq$: (A_a_option_fun_b_b_option_fun_fun$ * B$) > A_bool_fun$).
% 23.08/7.73 tff(uvp$, type, uvp$: B_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_162', type, '#skF_162': (A_option$ * A_option$ * A_a_fun$ * A_a_fun$) > A$).
% 23.08/7.73 tff(case_option$a, type, case_option$a: (C_option$ * C_c_option_fun$) > C_option_c_option_fun$).
% 23.08/7.73 tff('#skF_116', type, '#skF_116': (B_b_option_fun_c_c_option_fun_fun$ * B_b_option_fun_c_c_option_fun_fun$) > B$).
% 23.08/7.73 tff('#skF_69', type, '#skF_69': (B_b_option_fun_b_b_option_fun_fun$ * B_b_fun$ * B_b_b_option_fun_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_32', type, '#skF_32': (tlbool * A_bool_fun$ * A_option$) > A$).
% 23.08/7.73 tff('#skF_87', type, '#skF_87': (B_a_fun$ * B_option$ * A$) > B$).
% 23.08/7.73 tff(some$c, type, some$c: B_option$ > B_option_option$).
% 23.08/7.73 tff(fun_upd$c, type, fun_upd$c: (B_c_option_fun$ * B$ * C_option$) > B_c_option_fun$).
% 23.08/7.73 tff(undefined$a, type, undefined$a: B$).
% 23.08/7.73 tff(case_sum$f, type, case_sum$f: (C_c_fun$ * C_c_fun$) > C_c_sum_c_fun$).
% 23.08/7.73 tff('#skF_57', type, '#skF_57': (C_option$ * C_option_b_option_bool_fun_fun$ * B_option$) > C$).
% 23.08/7.73 tff(comp$ab, type, comp$ab: (B_option_c_option_fun$ * B_option_b_option_fun$) > B_option_c_option_fun$).
% 23.08/7.73 tff('#skF_90', type, '#skF_90': (C_c_fun$ * C_option$ * C$) > C$).
% 23.08/7.73 tff('#skF_193', type, '#skF_193': C_bool_fun$ > C$).
% 23.08/7.73 tff(comp$q, type, comp$q: (C_c_fun$ * B_c_fun$) > B_c_fun$).
% 23.08/7.73 tff(uvv$, type, uvv$: (B_c_option_fun$ * C_b_option_fun$) > B_b_option_fun$).
% 23.08/7.73 tff(fun_app$ay, type, fun_app$ay: (B_option_a_option_bool_fun_fun$ * B_option$) > A_option_bool_fun$).
% 23.08/7.73 tff(valid_getter_setter$, type, valid_getter_setter$: (C_b_fun$ * B_c_c_fun_fun$) > $o).
% 23.08/7.73 tff(some$d, type, some$d: C_option$ > C_option_option$).
% 23.08/7.73 tff(map_option$d, type, map_option$d: B_c_fun$ > B_option_c_option_fun$).
% 23.08/7.73 tff('#skF_122', type, '#skF_122': (A_option$ * A_option$ * A_a_fun$ * A_a_fun$) > A$).
% 23.08/7.73 tff('#skF_93', type, '#skF_93': (B_b_fun$ * B_option$ * B$) > B$).
% 23.08/7.73 tff(case_option$f, type, case_option$f: (tlbool * C_bool_fun$) > C_option_bool_fun$).
% 23.08/7.73 tff('#skF_3', type, '#skF_3': (C_b_fun$ * B_c_c_fun_fun$) > C$).
% 23.08/7.73 tff('#skF_148', type, '#skF_148': (B_option$ * B_option$ * B_c_option_fun$ * B_c_option_fun$) > B$).
% 23.08/7.73 tff(getter$a, type, getter$a: A_a_option_fun_b_b_option_fun_fun$ > B_a_fun$).
% 23.08/7.73 tff('#skF_179', type, '#skF_179': (A_option_bool_fun$ * C_option$ * C_a_option_fun$) > C$).
% 23.08/7.73 tff('#skF_54', type, '#skF_54': (A_option$ * A_option_a_option_bool_fun_fun$ * A_option$) > A$).
% 23.08/7.73 tff('#skF_81', type, '#skF_81': (A_a_option_fun_b_b_option_fun_fun$ * B_a_fun$ * A_b_b_option_fun_fun$) > A_a_option_fun$).
% 23.08/7.73 tff(preregister$f, type, preregister$f: A_a_option_fun_c_c_option_fun_fun$ > $o).
% 23.08/7.73 tff(id$e, type, id$e: A_option_a_option_fun$).
% 23.08/7.73 tff('#skF_55', type, '#skF_55': (C_option$ * C_option_c_option_bool_fun_fun$ * C_option$) > C$).
% 23.08/7.73 tff(register$, type, register$: A_a_option_fun_b_b_option_fun_fun$ > $o).
% 23.08/7.73 tff(top$a, type, top$a: C_set$).
% 23.08/7.73 tff(fun_app$af, type, fun_app$af: (Bool_b_option_fun$ * tlbool) > B_option$).
% 23.08/7.73 tff(uvs$, type, uvs$: C_c_fun$).
% 23.08/7.73 tff(fun_app$bo, type, fun_app$bo: (B_a_option_fun$ * B$) > A_option$).
% 23.08/7.73 tff(comp$bg, type, comp$bg: (B_c_option_fun$ * B_option_b_fun$) > B_option_c_option_fun$).
% 23.08/7.73 tff(tltrue, type, tltrue: tlbool).
% 23.08/7.73 tff('#skF_171', type, '#skF_171': (B_option$ * B_c_fun$ * B_c_fun$) > B$).
% 23.08/7.73 tff(uvc$, type, uvc$: C_b_fun$ > C_b_option_fun$).
% 23.08/7.73 tff(fun_app$m, type, fun_app$m: (C_b_fun$ * C$) > B$).
% 23.08/7.73 tff('#skF_187', type, '#skF_187': (B_option_bool_fun$ * B_option$ * B_b_option_fun$) > B$).
% 23.08/7.73 tff(fun_upd$b, type, fun_upd$b: (B_b_fun$ * B$) > B_b_b_fun_fun$).
% 23.08/7.73 tff('#skF_173', type, '#skF_173': (C_option$ * C_b_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(fun_app$c, type, fun_app$c: (B_bool_fun$ * B$) > $o).
% 23.08/7.73 tff(comp$p, type, comp$p: (C_option_c_option_fun$ * B_option_c_option_fun$) > B_option_c_option_fun$).
% 23.08/7.73 tff('#skF_131', type, '#skF_131': (B_option_bool_fun$ * B_option$ * B_b_option_fun$) > B$).
% 23.08/7.73 tff(def_1, type, def_1: (C_bool_fun$ * C$) > tlbool).
% 23.08/7.73 tff(comp$ap, type, comp$ap: (B_c_option_fun$ * C_b_fun$) > C_c_option_fun$).
% 23.08/7.73 tff(register_from_getter_setter$b, type, register_from_getter_setter$b: (B_b_fun$ * B_b_b_fun_fun$) > B_b_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_68', type, '#skF_68': B_option_bool_fun$ > B_option$).
% 23.08/7.73 tff(comp$v, type, comp$v: (C_option_b_option_fun$ * A_option_c_option_fun$) > A_option_b_option_fun$).
% 23.08/7.73 tff(map_option$, type, map_option$: C_b_fun$ > C_option_b_option_fun$).
% 23.08/7.73 tff('#skF_31', type, '#skF_31': B_a_fun$).
% 23.08/7.73 tff('#skF_168', type, '#skF_168': (C_option$ * C_option$ * C_b_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(fun_app$ax, type, fun_app$ax: (C_option_a_option_bool_fun_fun$ * C_option$) > A_option_bool_fun$).
% 23.08/7.73 tff('#skF_126', type, '#skF_126': (B_option_bool_fun$ * A_option$ * A_b_option_fun$) > A$).
% 23.08/7.73 tff(bot$h, type, bot$h: C_option_bool_fun$).
% 23.08/7.73 tff(fun_app$ak, type, fun_app$ak: (C_option_c_fun$ * C_option$) > C$).
% 23.08/7.73 tff(fun_app$bb, type, fun_app$bb: (A_option_a_option_bool_fun_fun$ * A_option$) > A_option_bool_fun$).
% 23.08/7.73 tff('#skF_104', type, '#skF_104': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_152', type, '#skF_152': (C_option$ * C_bool_fun$ * C$) > C$).
% 23.08/7.73 tff(def_14, type, def_14: (B_option_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff(comp$ah, type, comp$ah: (B_option_b_option_fun$ * B_option_b_option_fun$) > B_option_b_option_fun$).
% 23.08/7.73 tff(map_option$f, type, map_option$f: A_c_fun$ > A_option_c_option_fun$).
% 23.08/7.73 tff(fun_app$d, type, fun_app$d: (C_option_c_option_bool_fun_fun$ * C_option$) > C_option_bool_fun$).
% 23.08/7.73 tff(fun_upd$f, type, fun_upd$f: (C_c_fun$ * C$) > C_c_c_fun_fun$).
% 23.08/7.73 tff('#skF_117', type, '#skF_117': (B_b_option_fun_c_c_option_fun_fun$ * B_b_option_fun_c_c_option_fun_fun$) > B$).
% 23.08/7.73 tff(uvm$, type, uvm$: B_b_fun$).
% 23.08/7.73 tff(id$a, type, id$a: C_c_fun$).
% 23.08/7.73 tff('#skF_56', type, '#skF_56': (C_option$ * C_option_c_option_bool_fun_fun$ * C_option$) > C$).
% 23.08/7.73 tff(uwa$, type, uwa$: C_c_option_fun$ > C_c_option_fun_c_c_option_fun_fun$).
% 23.08/7.73 tff(def_10, type, def_10: (C_option_bool_fun$ * C_option$) > tlbool).
% 23.08/7.73 tff(comp$ac, type, comp$ac: (B_c_fun$ * B_b_fun$) > B_c_fun$).
% 23.08/7.73 tff('#skF_20', type, '#skF_20': B_option$ > B$).
% 23.08/7.73 tff('#skF_22', type, '#skF_22': C_option$ > C$).
% 23.08/7.73 tff(valid_getter_setter$b, type, valid_getter_setter$b: (B_b_fun$ * B_b_b_fun_fun$) > $o).
% 23.08/7.73 tff('#skF_96', type, '#skF_96': (B_b_b_fun_fun$ * B_option$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff('#skF_100', type, '#skF_100': (B_b_b_fun_fun$ * B_option$ * B_option$) > B$).
% 23.08/7.73 tff(fun_app$ab, type, fun_app$ab: (C_c_option_fun_c_option_fun$ * C_c_option_fun$) > C_option$).
% 23.08/7.73 tff(fun_app$aw, type, fun_app$aw: (A_option_bool_fun$ * A_option$) > $o).
% 23.08/7.73 tff(comp$g, type, comp$g: (A_b_option_fun$ * A_a_fun$) > A_b_option_fun$).
% 23.08/7.73 tff(is_empty$, type, is_empty$: B_set$ > $o).
% 23.08/7.73 tff(map_option$j, type, map_option$j: (C_option_c_option_fun$ * C_option_option$) > C_option_option$).
% 23.08/7.73 tff(comp$ai, type, comp$ai: (B_b_fun$ * B_b_fun$) > B_b_fun$).
% 23.08/7.73 tff(fun_app$aj, type, fun_app$aj: (A_a_a_fun_fun$ * A$) > A_a_fun$).
% 23.08/7.73 tff(thesis$, type, thesis$: $o).
% 23.08/7.73 tff('#skF_118', type, '#skF_118': (C_option$ * C_option$ * C_b_fun$ * C_b_fun$) > C$).
% 23.08/7.73 tff(uvd$, type, uvd$: A_a_fun$ > A_a_option_fun$).
% 23.08/7.73 tff(map_option$g, type, map_option$g: C_a_fun$ > C_option_a_option_fun$).
% 23.08/7.73 tff(fun_app$n, type, fun_app$n: (B_c_option_fun$ * B$) > C_option$).
% 23.08/7.73 tff(set_option$d, type, set_option$d: B_option$ > B_set$).
% 23.08/7.73 tff(comp$ag, type, comp$ag: (B_b_fun$ * C_b_fun$) > C_b_fun$).
% 23.08/7.73 tff('#skF_198', type, '#skF_198': B_option_set$ > B_option$).
% 23.08/7.73 tff(case_sum$e, type, case_sum$e: (C_c_option_fun$ * C_c_option_fun$) > C_c_sum_c_option_fun$).
% 23.08/7.73 tff(comp$ao, type, comp$ao: (C_b_option_fun$ * C_c_fun$) > C_b_option_fun$).
% 23.08/7.73 tff('#skF_64', type, '#skF_64': A_option_bool_fun$ > A_option$).
% 23.08/7.73 tff('#skF_153', type, '#skF_153': (B_option$ * B_bool_fun$ * B$) > B$).
% 23.08/7.73 tff(comp$c, type, comp$c: (B_b_option_fun$ * B_b_fun$) > B_b_option_fun$).
% 23.08/7.73 tff('#skF_166', type, '#skF_166': (B_option$ * B_option$ * B_b_fun$ * B_b_fun$) > B$).
% 23.08/7.73 tff('#skF_185', type, '#skF_185': (B_option_bool_fun$ * C_option$ * C_b_option_fun$) > C$).
% 23.08/7.73 tff(fun_app$w, type, fun_app$w: (B_c_c_option_fun_fun$ * B$) > C_c_option_fun$).
% 23.08/7.73 tff(undefined$, type, undefined$: A$).
% 23.08/7.73 tff('#skF_7', type, '#skF_7': (C_b_fun$ * B_c_c_fun_fun$) > B$).
% 23.08/7.73 tff(fun_app$a, type, fun_app$a: (B_option_bool_fun$ * B_option$) > $o).
% 23.08/7.73 tff(fun_app$bn, type, fun_app$bn: (C_a_option_fun$ * C$) > A_option$).
% 23.08/7.73 tff(comp$k, type, comp$k: (C_bool_fun$ * B_c_fun$) > B_bool_fun$).
% 23.08/7.73 tff(set_option$b, type, set_option$b: A_option$ > A_set$).
% 23.08/7.73 tff(uvz$, type, uvz$: (B_c_option_fun$ * C_c_option_fun$) > B_c_option_fun$).
% 23.08/7.73 tff(case_option$i, type, case_option$i: (A$ * A_a_fun$ * A_option$) > A$).
% 23.08/7.73 tff(id$f, type, id$f: B_b_option_fun_b_b_option_fun_fun$).
% 23.08/7.73 tff('#skF_160', type, '#skF_160': (A_option$ * A_option$ * A_b_fun$ * A_b_fun$) > A$).
% 23.08/7.73 tff(uus$, type, uus$: B_b_b_option_fun_fun$ > B_b_b_option_fun_fun$).
% 23.08/7.73 tff(uuf$, type, uuf$: C_bool_fun$).
% 23.08/7.73 tff(case_option$e, type, case_option$e: (tlbool * B_bool_fun$) > B_option_bool_fun$).
% 23.08/7.73 tff(some$b, type, some$b: A_a_option_fun$).
% 23.08/7.73 tff(bind$, type, bind$: C_option$ > C_c_option_fun_c_option_fun$).
% 23.08/7.73 tff(undefined$b, type, undefined$b: C$).
% 23.08/7.73 tff('#skF_67', type, '#skF_67': B_option_bool_fun$ > B$).
% 23.08/7.73 tff(valid_getter_setter$a, type, valid_getter_setter$a: (B_a_fun$ * A_b_b_fun_fun$) > $o).
% 23.08/7.73 tff(def_6, type, def_6: (tlbool * B_bool_fun$ * B_option$) > tlbool).
% 23.08/7.73 tff('#skF_6', type, '#skF_6': (C_b_fun$ * B_c_c_fun_fun$) > B$).
% 23.08/7.73 tff(id$c, type, id$c: C_option_c_option_fun$).
% 23.08/7.73 tff('#skF_114', type, '#skF_114': (A_a_option_fun_b_b_option_fun_fun$ * A_a_option_fun_b_b_option_fun_fun$) > A$).
% 23.08/7.73 tff(the$, type, the$: B_option_b_fun$).
% 23.08/7.73
% 23.08/7.74 tff(f_310, axiom, register$a(g$), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom75)).
% 23.08/7.74 tff(f_690, axiom, (![A__questionmark_v0:B_b_option_fun_c_c_option_fun_fun$]: (register$a(A__questionmark_v0) <=> (?[A__questionmark_v1:C_b_fun$, A__questionmark_v2:B_c_c_fun_fun$]: ((A__questionmark_v0 = register_from_getter_setter$a(A__questionmark_v1, A__questionmark_v2)) & valid_getter_setter$(A__questionmark_v1, A__questionmark_v2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom136)).
% 23.08/7.74 tff(f_298, negated_conjecture, ~thesis$, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conjecture72)).
% 23.08/7.74 tff(f_427, axiom, (![A__questionmark_v0:C_b_fun$, A__questionmark_v1:B_c_c_fun_fun$, A__questionmark_v2:B_b_option_fun$, A__questionmark_v3:C$]: (fun_app$j(fun_app$am(register_from_getter_setter$a(A__questionmark_v0, A__questionmark_v1), A__questionmark_v2), A__questionmark_v3) = fun_app$an(case_option$c(none$, uu$(A__questionmark_v1, A__questionmark_v3)), fun_app$g(A__questionmark_v2, fun_app$m(A__questionmark_v0, A__questionmark_v3))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom94)).
% 23.08/7.74 tff(f_306, hypothesis, (![A__questionmark_v0:B_c_c_fun_fun$, A__questionmark_v1:C_b_fun$]: (((![A__questionmark_v2:B_b_option_fun$, A__questionmark_v3:C$]: (fun_app$j(fun_app$am(g$, A__questionmark_v2), A__questionmark_v3) = fun_app$an(case_option$c(none$, uu$(A__questionmark_v0, A__questionmark_v3)), fun_app$g(A__questionmark_v2, fun_app$m(A__questionmark_v1, A__questionmark_v3))))) & valid_getter_setter$(A__questionmark_v1, A__questionmark_v0)) => thesis$)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', hypothesis73)).
% 23.08/7.74 tff(c_190, plain, (register$a(g$)), inference(cnfTransformation, [status(thm)], [f_310])).
% 23.08/7.74 tff(c_411, plain, (![A__questionmark_v0_362:B_b_option_fun_c_c_option_fun_fun$]: (valid_getter_setter$('#skF_41'(A__questionmark_v0_362), '#skF_42'(A__questionmark_v0_362)) | ~register$a(A__questionmark_v0_362))), inference(cnfTransformation, [status(thm)], [f_690])).
% 23.08/7.74 tff(c_10685, plain, (![A__questionmark_v0_34994:B_b_option_fun_c_c_option_fun_fun$]: (register_from_getter_setter$a('#skF_41'(A__questionmark_v0_34994), '#skF_42'(A__questionmark_v0_34994))=A__questionmark_v0_34994 | ~register$a(A__questionmark_v0_34994))), inference(cnfTransformation, [status(thm)], [f_690])).
% 23.08/7.74 tff(c_184, plain, (~thesis$), inference(cnfTransformation, [status(thm)], [f_298])).
% 23.08/7.74 tff(c_252, plain, (![A__questionmark_v1_244:B_c_c_fun_fun$, A__questionmark_v3_246:C$, A__questionmark_v2_245:B_b_option_fun$, A__questionmark_v0_243:C_b_fun$]: (fun_app$an(case_option$c(none$, uu$(A__questionmark_v1_244, A__questionmark_v3_246)), fun_app$g(A__questionmark_v2_245, fun_app$m(A__questionmark_v0_243, A__questionmark_v3_246)))=fun_app$j(fun_app$am(register_from_getter_setter$a(A__questionmark_v0_243, A__questionmark_v1_244), A__questionmark_v2_245), A__questionmark_v3_246))), inference(cnfTransformation, [status(thm)], [f_427])).
% 23.08/7.74 tff(c_186, plain, (![A__questionmark_v1_163:C_b_fun$, A__questionmark_v0_162:B_c_c_fun_fun$]: (thesis$ | ~valid_getter_setter$(A__questionmark_v1_163, A__questionmark_v0_162) | fun_app$an(case_option$c(none$, uu$(A__questionmark_v0_162, '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163))), fun_app$g('#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163), fun_app$m(A__questionmark_v1_163, '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163))))!=fun_app$j(fun_app$am(g$, '#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163)), '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163)))), inference(cnfTransformation, [status(thm)], [f_306])).
% 23.08/7.74 tff(c_2973, plain, (![A__questionmark_v1_163:C_b_fun$, A__questionmark_v0_162:B_c_c_fun_fun$]: (thesis$ | ~valid_getter_setter$(A__questionmark_v1_163, A__questionmark_v0_162) | fun_app$j(fun_app$am(register_from_getter_setter$a(A__questionmark_v1_163, A__questionmark_v0_162), '#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163)), '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163))!=fun_app$j(fun_app$am(g$, '#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163)), '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163)))), inference(demodulation, [status(thm), theory('equality')], [c_252, c_186])).
% 23.08/7.74 tff(c_2974, plain, (![A__questionmark_v1_163:C_b_fun$, A__questionmark_v0_162:B_c_c_fun_fun$]: (~valid_getter_setter$(A__questionmark_v1_163, A__questionmark_v0_162) | fun_app$j(fun_app$am(register_from_getter_setter$a(A__questionmark_v1_163, A__questionmark_v0_162), '#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163)), '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163))!=fun_app$j(fun_app$am(g$, '#skF_1'(A__questionmark_v0_162, A__questionmark_v1_163)), '#skF_2'(A__questionmark_v0_162, A__questionmark_v1_163)))), inference(negUnitSimplification, [status(thm)], [c_184, c_2973])).
% 23.08/7.74 tff(c_10697, plain, (![A__questionmark_v0_34994:B_b_option_fun_c_c_option_fun_fun$]: (~valid_getter_setter$('#skF_41'(A__questionmark_v0_34994), '#skF_42'(A__questionmark_v0_34994)) | fun_app$j(fun_app$am(g$, '#skF_1'('#skF_42'(A__questionmark_v0_34994), '#skF_41'(A__questionmark_v0_34994))), '#skF_2'('#skF_42'(A__questionmark_v0_34994), '#skF_41'(A__questionmark_v0_34994)))!=fun_app$j(fun_app$am(A__questionmark_v0_34994, '#skF_1'('#skF_42'(A__questionmark_v0_34994), '#skF_41'(A__questionmark_v0_34994))), '#skF_2'('#skF_42'(A__questionmark_v0_34994), '#skF_41'(A__questionmark_v0_34994))) | ~register$a(A__questionmark_v0_34994))), inference(superposition, [status(thm), theory('equality')], [c_10685, c_2974])).
% 23.08/7.74 tff(c_10824, plain, (~valid_getter_setter$('#skF_41'(g$), '#skF_42'(g$)) | ~register$a(g$)), inference(reflexivity, [status(thm), theory('equality')], [c_10697])).
% 23.08/7.74 tff(c_10826, plain, (~valid_getter_setter$('#skF_41'(g$), '#skF_42'(g$))), inference(demodulation, [status(thm), theory('equality')], [c_190, c_10824])).
% 23.08/7.74 tff(c_10830, plain, (~register$a(g$)), inference(resolution, [status(thm)], [c_411, c_10826])).
% 23.08/7.74 tff(c_10834, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_190, c_10830])).
% 23.08/7.74 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------