%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP367_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 : n017.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:42 PM UTC 2025
% Result : Theorem 29.19s 10.20s
% Output : CNFRefutation 29.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ITP367_1 : TPTP v9.0.0. Released v8.0.0.
% 0.10/0.13 % 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.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 02:20:10 EDT 2025
% 0.12/0.33 % CPUTime :
% 29.19/10.20 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.19/10.20
% 29.19/10.20 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.24/10.23 %$ member$b > less_eq$b > fun_app$b > fun_app$a > fun_app$ > finite$b > comp_fun_idem$c > comp_fun_idem$b > comp_fun_idem$a > comp_fun_idem$ > sup$b > minus$ > insert$ > 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$c > fold$a > bind$c > bind$b > bind$a > bind$ > #nlpp > uua$ > uu$ > the_elem$ > sup_fin$ > member$a > member$ > less_eq$a > inf_fin$ > fold$ > filter$a > filter$ > disjnt$ > collect$a > collect$ > y$ > x$ > the_elem$a > sup_fin$a > sup$a > sup$ > subformulas_nu$ > subformulas_mu$ > remove$ > phi$ > minus$b > minus$a > max$ > less_eq$ > is_singleton$a > is_singleton$ > is_empty$a > is_empty$ > insert$b > insert$a > inf_fin$a > inf$a > inf$ > finite$a > finite$ > disjnt$a > bot$d > bot$c > bot$b > bot$a > bot$ > #skF_7 > #skF_37 > #skF_42 > #skF_123 > #skF_65 > #skF_59 > #skF_111 > #skF_84 > #skF_153 > #skF_33 > #skF_99 > #skF_9 > #skF_70 > #skF_101 > #skF_52 > #skF_138 > #skF_43 > #skF_68 > #skF_45 > #skF_71 > #skF_122 > #skF_149 > #skF_174 > #skF_25 > #skF_173 > #skF_32 > #skF_26 > #skF_64 > #skF_140 > #skF_156 > #skF_56 > #skF_69 > #skF_14 > #skF_1 > #skF_2 > #skF_129 > #skF_114 > #skF_20 > #skF_168 > #skF_177 > #skF_143 > #skF_18 > #skF_124 > #skF_157 > #skF_21 > #skF_121 > #skF_145 > #skF_12 > #skF_130 > #skF_6 > #skF_109 > #skF_167 > #skF_96 > #skF_105 > #skF_118 > #skF_63 > #skF_164 > #skF_58 > #skF_170 > #skF_139 > #skF_55 > #skF_80 > #skF_85 > #skF_93 > #skF_54 > #skF_112 > #skF_97 > #skF_83 > #skF_110 > #skF_67 > #skF_103 > #skF_117 > #skF_132 > #skF_165 > #skF_104 > #skF_152 > #skF_27 > #skF_87 > #skF_108 > #skF_76 > #skF_127 > #skF_89 > #skF_24 > #skF_5 > #skF_179 > #skF_148 > #skF_61 > #skF_46 > #skF_116 > #skF_142 > #skF_86 > #skF_169 > #skF_161 > #skF_125 > #skF_57 > #skF_28 > #skF_35 > #skF_134 > #skF_88 > #skF_154 > #skF_36 > #skF_95 > #skF_162 > #skF_178 > #skF_62 > #skF_22 > #skF_155 > #skF_44 > #skF_13 > #skF_92 > #skF_30 > #skF_60 > #skF_74 > #skF_48 > #skF_75 > #skF_66 > #skF_159 > #skF_141 > #skF_119 > #skF_128 > #skF_82 > #skF_41 > #skF_81 > #skF_146 > #skF_53 > #skF_171 > #skF_172 > #skF_72 > #skF_106 > #skF_19 > #skF_23 > #skF_100 > #skF_8 > #skF_73 > #skF_49 > #skF_40 > #skF_160 > #skF_47 > #skF_39 > #skF_147 > #skF_131 > #skF_135 > #skF_79 > #skF_90 > #skF_120 > #skF_50 > #skF_102 > #skF_10 > #skF_107 > #skF_31 > #skF_144 > #skF_4 > #skF_175 > #skF_126 > #skF_98 > #skF_150 > #skF_29 > #skF_15 > #skF_94 > #skF_38 > #skF_113 > #skF_16 > #skF_3 > #skF_136 > #skF_51 > #skF_151 > #skF_137 > #skF_34 > #skF_11 > #skF_115 > #skF_133 > #skF_78 > #skF_17 > #skF_176 > #skF_163 > #skF_158 > #skF_77 > #skF_166 > #skF_91
% 29.24/10.23
% 29.24/10.23 %Foreground sorts:
% 29.24/10.23 tff(A_ltln_a_ltln_set_fun$, type, A_ltln_a_ltln_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$, type, A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set_set$, type, A_ltln_set_set_set$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set_a_ltln_set_fun$, type, A_ltln_set_set_a_ltln_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set_bool_fun$, type, A_ltln_set_set_bool_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_bool_fun$, type, A_ltln_set_bool_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_bool_fun$, type, A_ltln_bool_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_a_ltln_set_bool_fun_fun$, type, A_ltln_set_a_ltln_set_bool_fun_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_a_ltln_set_set_fun$, type, A_ltln_set_a_ltln_set_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set$, type, A_ltln_set$: $tType ).
% 29.24/10.23 tff(A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$, type, A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_a_ltln_bool_fun_fun$, type, A_ltln_a_ltln_bool_fun_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_a_ltln_set_fun$, type, A_ltln_set_a_ltln_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_a_ltln_set_set_fun$, type, A_ltln_a_ltln_set_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln$, type, A_ltln$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set_a_ltln_set_set_fun$, type, A_ltln_set_set_a_ltln_set_set_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_a_ltln_set_a_ltln_set_fun_fun$, type, A_ltln_a_ltln_set_a_ltln_set_fun_fun$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set$, type, A_ltln_set_set$: $tType ).
% 29.24/10.23 tff(A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$, type, A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$: $tType ).
% 29.24/10.23
% 29.24/10.23 %Background operators:
% 29.24/10.23
% 29.24/10.23
% 29.24/10.23 %Foreground operators:
% 29.24/10.23 tff(the_elem$, type, the_elem$: A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff('#skF_7', type, '#skF_7': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_37', type, '#skF_37': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff(insert$, type, insert$: (A_ltln_set_set$ * A_ltln_set_set_set$) > A_ltln_set_set_set$).
% 29.24/10.23 tff('#skF_42', type, '#skF_42': (A_ltln_bool_fun$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff(is_empty$, type, is_empty$: A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_123', type, '#skF_123': (A_ltln$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(fun_app$g, type, fun_app$g: (A_ltln_set_a_ltln_set_bool_fun_fun$ * A_ltln_set$) > A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_65', type, '#skF_65': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_59', type, '#skF_59': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_111', type, '#skF_111': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_84', type, '#skF_84': (A_ltln_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(finite$b, type, finite$b: A_ltln_set_set_set$ > $o).
% 29.24/10.23 tff('#skF_153', type, '#skF_153': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(minus$, type, minus$: (A_ltln_set_set_set$ * A_ltln_set_set_set$) > A_ltln_set_set_set$).
% 29.24/10.23 tff('#skF_33', type, '#skF_33': (A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_99', type, '#skF_99': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(fun_app$c, type, fun_app$c: (A_ltln_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_9', type, '#skF_9': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_70', type, '#skF_70': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_101', type, '#skF_101': (A_ltln_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_52', type, '#skF_52': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(sup$b, type, sup$b: (A_ltln_set_set_set$ * A_ltln_set_set_set$) > A_ltln_set_set_set$).
% 29.24/10.23 tff('#skF_138', type, '#skF_138': (A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_43', type, '#skF_43': (A_ltln_set_bool_fun$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_68', type, '#skF_68': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(less_eq$b, type, less_eq$b: (A_ltln_set_set_set$ * A_ltln_set_set_set$) > $o).
% 29.24/10.23 tff('#skF_45', type, '#skF_45': A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_71', type, '#skF_71': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(inf$, type, inf$: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff('#skF_122', type, '#skF_122': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_149', type, '#skF_149': (A_ltln_set_set_bool_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_174', type, '#skF_174': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_25', type, '#skF_25': (A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff(bind$c, type, bind$c: (A_ltln_set$ * A_ltln_a_ltln_set_fun$) > A_ltln_set$).
% 29.24/10.23 tff(less_eq$, type, less_eq$: A_ltln_set_a_ltln_set_bool_fun_fun$).
% 29.24/10.23 tff(fun_app$a, type, fun_app$a: (A_ltln_set_bool_fun$ * A_ltln_set$) > $o).
% 29.24/10.23 tff(disjnt$, type, disjnt$: A_ltln_set_set$ > A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff('#skF_173', type, '#skF_173': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_32', type, '#skF_32': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_26', type, '#skF_26': (A_ltln_set$ * A_ltln_set$) > A_ltln$).
% 29.24/10.23 tff('#skF_64', type, '#skF_64': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_140', type, '#skF_140': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_156', type, '#skF_156': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_56', type, '#skF_56': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_69', type, '#skF_69': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(comp_fun_idem$a, type, comp_fun_idem$a: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ > $o).
% 29.24/10.23 tff('#skF_14', type, '#skF_14': (A_ltln_bool_fun$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff(bot$a, type, bot$a: A_ltln_set$).
% 29.24/10.23 tff('#skF_1', type, '#skF_1': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(fun_app$, type, fun_app$: (A_ltln_bool_fun$ * A_ltln$) > $o).
% 29.24/10.23 tff(filter$a, type, filter$a: A_ltln_bool_fun$ > A_ltln_set_a_ltln_set_fun$).
% 29.24/10.23 tff('#skF_2', type, '#skF_2': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_129', type, '#skF_129': A_ltln_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff(inf_fin$, type, inf_fin$: A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_114', type, '#skF_114': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_20', type, '#skF_20': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(finite$a, type, finite$a: A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff('#skF_168', type, '#skF_168': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_177', type, '#skF_177': (A_ltln_set_bool_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_143', type, '#skF_143': (A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_18', type, '#skF_18': (A_ltln_set$ * A_ltln_a_ltln_set_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_124', type, '#skF_124': (A_ltln_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_157', type, '#skF_157': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_21', type, '#skF_21': A_ltln_bool_fun$ > A_ltln$).
% 29.24/10.23 tff('#skF_121', type, '#skF_121': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(insert$a, type, insert$a: A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$).
% 29.24/10.23 tff('#skF_145', type, '#skF_145': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_12', type, '#skF_12': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_130', type, '#skF_130': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(fun_app$j, type, fun_app$j: (A_ltln_a_ltln_set_set_fun$ * A_ltln$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_6', type, '#skF_6': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_109', type, '#skF_109': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_167', type, '#skF_167': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(sup$a, type, sup$a: A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$).
% 29.24/10.23 tff(fun_app$l, type, fun_app$l: (A_ltln_a_ltln_bool_fun_fun$ * A_ltln$) > A_ltln_bool_fun$).
% 29.24/10.23 tff(sup$, type, sup$: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff('#skF_96', type, '#skF_96': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_105', type, '#skF_105': (A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(is_singleton$a, type, is_singleton$a: A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff(minus$b, type, minus$b: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff(bind$b, type, bind$b: (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_118', type, '#skF_118': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_63', type, '#skF_63': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_164', type, '#skF_164': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(is_singleton$, type, is_singleton$: A_ltln_set_bool_fun$).
% 29.24/10.23 tff(fold$, type, fold$: A_ltln_a_ltln_set_a_ltln_set_fun_fun$ > A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff('#skF_58', type, '#skF_58': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_170', type, '#skF_170': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_139', type, '#skF_139': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_55', type, '#skF_55': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_80', type, '#skF_80': (A_ltln_set$ * A_ltln_a_ltln_bool_fun_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_85', type, '#skF_85': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_93', type, '#skF_93': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_54', type, '#skF_54': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_112', type, '#skF_112': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(fun_app$k, type, fun_app$k: (A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_97', type, '#skF_97': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_83', type, '#skF_83': (A_ltln_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_110', type, '#skF_110': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(sup_fin$a, type, sup_fin$a: A_ltln_set_set_a_ltln_set_fun$).
% 29.24/10.23 tff(bot$b, type, bot$b: A_ltln_set_set_set$).
% 29.24/10.23 tff('#skF_67', type, '#skF_67': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_103', type, '#skF_103': (A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(fun_app$f, type, fun_app$f: (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$) > A_ltln_set_set_a_ltln_set_set_fun$).
% 29.24/10.23 tff('#skF_117', type, '#skF_117': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_132', type, '#skF_132': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff(is_empty$a, type, is_empty$a: A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff('#skF_165', type, '#skF_165': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_104', type, '#skF_104': (A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_152', type, '#skF_152': (A_ltln_set_bool_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_27', type, '#skF_27': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(fun_app$n, type, fun_app$n: (A_ltln_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln$) > A_ltln_set_a_ltln_set_fun$).
% 29.24/10.23 tff('#skF_87', type, '#skF_87': (A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_108', type, '#skF_108': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_76', type, '#skF_76': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_bool_fun_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_127', type, '#skF_127': (A_ltln$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_89', type, '#skF_89': (A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_24', type, '#skF_24': A_ltln_set_bool_fun$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_5', type, '#skF_5': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_179', type, '#skF_179': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(filter$, type, filter$: A_ltln_set_bool_fun$ > A_ltln_set_set_a_ltln_set_set_fun$).
% 29.24/10.23 tff(comp_fun_idem$b, type, comp_fun_idem$b: A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ > $o).
% 29.24/10.23 tff('#skF_148', type, '#skF_148': (A_ltln_set_set_bool_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_61', type, '#skF_61': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_46', type, '#skF_46': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(comp_fun_idem$c, type, comp_fun_idem$c: A_ltln_a_ltln_set_a_ltln_set_fun_fun$ > $o).
% 29.24/10.23 tff('#skF_116', type, '#skF_116': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_142', type, '#skF_142': (A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(fun_app$m, type, fun_app$m: (A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set$) > A_ltln_set_set_a_ltln_set_set_fun$).
% 29.24/10.23 tff('#skF_86', type, '#skF_86': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_169', type, '#skF_169': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(remove$, type, remove$: A_ltln_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff('#skF_161', type, '#skF_161': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff(uua$, type, uua$: A_ltln_set$ > A_ltln_bool_fun$).
% 29.24/10.23 tff('#skF_125', type, '#skF_125': (A_ltln$ * A_ltln_set$ * A_ltln$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_57', type, '#skF_57': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_28', type, '#skF_28': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(uu$, type, uu$: A_ltln_set_set$ > A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_35', type, '#skF_35': (A_ltln_set$ * A_ltln_set$) > A_ltln$).
% 29.24/10.23 tff('#skF_134', type, '#skF_134': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff(minus$a, type, minus$a: A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$).
% 29.24/10.23 tff(fold$a, type, fold$a: (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$) > A_ltln_set_set_a_ltln_set_fun$).
% 29.24/10.23 tff(sup_fin$, type, sup_fin$: A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_88', type, '#skF_88': (A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_154', type, '#skF_154': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_36', type, '#skF_36': (A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_95', type, '#skF_95': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_162', type, '#skF_162': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(bot$d, type, bot$d: A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_178', type, '#skF_178': (A_ltln_set_bool_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(less_eq$a, type, less_eq$a: A_ltln_set_set$ > A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff('#skF_62', type, '#skF_62': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_22', type, '#skF_22': A_ltln_set_bool_fun$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_155', type, '#skF_155': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_44', type, '#skF_44': (A_ltln_bool_fun$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff(member$a, type, member$a: A_ltln_set$ > A_ltln_set_set_bool_fun$).
% 29.24/10.23 tff(subformulas_nu$, type, subformulas_nu$: A_ltln_a_ltln_set_fun$).
% 29.24/10.23 tff(collect$, type, collect$: A_ltln_set_bool_fun$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_13', type, '#skF_13': (A_ltln_bool_fun$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_92', type, '#skF_92': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff(fun_app$e, type, fun_app$e: (A_ltln_set_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_30', type, '#skF_30': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(finite$, type, finite$: A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_60', type, '#skF_60': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_74', type, '#skF_74': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_bool_fun_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_48', type, '#skF_48': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_75', type, '#skF_75': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_bool_fun_fun$) > A_ltln_set$).
% 29.24/10.23 tff(inf$a, type, inf$a: A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$).
% 29.24/10.23 tff('#skF_66', type, '#skF_66': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_159', type, '#skF_159': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_141', type, '#skF_141': (A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_119', type, '#skF_119': A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_128', type, '#skF_128': (A_ltln_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_82', type, '#skF_82': (A_ltln_set$ * A_ltln_a_ltln_bool_fun_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_41', type, '#skF_41': (A_ltln_set_bool_fun$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_81', type, '#skF_81': (A_ltln_set$ * A_ltln_a_ltln_bool_fun_fun$) > A_ltln$).
% 29.24/10.23 tff(bind$, type, bind$: (A_ltln_set$ * A_ltln_a_ltln_set_set_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_146', type, '#skF_146': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(insert$b, type, insert$b: A_ltln_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff(fun_app$h, type, fun_app$h: (A_ltln_a_ltln_set_fun$ * A_ltln$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_53', type, '#skF_53': (A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_171', type, '#skF_171': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_172', type, '#skF_172': (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_72', type, '#skF_72': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff('#skF_106', type, '#skF_106': (A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(bot$, type, bot$: A_ltln_set_set$).
% 29.24/10.23 tff('#skF_19', type, '#skF_19': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff('#skF_23', type, '#skF_23': A_ltln_bool_fun$ > A_ltln$).
% 29.24/10.23 tff('#skF_100', type, '#skF_100': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_8', type, '#skF_8': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(the_elem$a, type, the_elem$a: A_ltln_set_set_a_ltln_set_fun$).
% 29.24/10.23 tff(disjnt$a, type, disjnt$a: A_ltln_set_a_ltln_set_bool_fun_fun$).
% 29.24/10.23 tff('#skF_73', type, '#skF_73': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_bool_fun_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_49', type, '#skF_49': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(fun_app$i, type, fun_app$i: (A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_40', type, '#skF_40': (A_ltln_set$ * A_ltln_set$) > A_ltln$).
% 29.24/10.23 tff('#skF_160', type, '#skF_160': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_47', type, '#skF_47': A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_39', type, '#skF_39': (A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_147', type, '#skF_147': (A_ltln_set_set_bool_fun$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_131', type, '#skF_131': A_ltln_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_135', type, '#skF_135': A_ltln_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_79', type, '#skF_79': (A_ltln_set$ * A_ltln_a_ltln_bool_fun_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_90', type, '#skF_90': (A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_120', type, '#skF_120': A_ltln_set_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_50', type, '#skF_50': (A_ltln_set_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_102', type, '#skF_102': (A_ltln_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_10', type, '#skF_10': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_107', type, '#skF_107': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_31', type, '#skF_31': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff(collect$a, type, collect$a: A_ltln_bool_fun$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_144', type, '#skF_144': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_4', type, '#skF_4': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_175', type, '#skF_175': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_126', type, '#skF_126': (A_ltln_set$ * A_ltln_set_set$ * A_ltln_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(fun_app$b, type, fun_app$b: (A_ltln_set_set_bool_fun$ * A_ltln_set_set$) > $o).
% 29.24/10.23 tff('#skF_98', type, '#skF_98': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_150', type, '#skF_150': (A_ltln_set_bool_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_29', type, '#skF_29': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_15', type, '#skF_15': (A_ltln_set$ * A_ltln_a_ltln_set_set_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_94', type, '#skF_94': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set_set$).
% 29.24/10.23 tff(member$, type, member$: A_ltln$ > A_ltln_set_bool_fun$).
% 29.24/10.23 tff('#skF_38', type, '#skF_38': A_ltln_set_set$ > A_ltln_set$).
% 29.24/10.23 tff('#skF_113', type, '#skF_113': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_fun$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_16', type, '#skF_16': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_3', type, '#skF_3': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(max$, type, max$: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$).
% 29.24/10.23 tff('#skF_136', type, '#skF_136': A_ltln_set$ > A_ltln$).
% 29.24/10.23 tff('#skF_51', type, '#skF_51': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_151', type, '#skF_151': (A_ltln_set_bool_fun$ * A_ltln_set$) > A_ltln$).
% 29.24/10.23 tff(fun_app$d, type, fun_app$d: (A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$ * A_ltln_set$) > A_ltln_set_a_ltln_set_fun$).
% 29.24/10.23 tff(bot$c, type, bot$c: A_ltln_bool_fun$).
% 29.24/10.23 tff(subformulas_mu$, type, subformulas_mu$: A_ltln_a_ltln_set_fun$).
% 29.24/10.23 tff('#skF_137', type, '#skF_137': (A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(member$b, type, member$b: (A_ltln_set_set$ * A_ltln_set_set_set$) > $o).
% 29.24/10.23 tff('#skF_34', type, '#skF_34': (A_ltln_set$ * A_ltln_set$) > A_ltln$).
% 29.24/10.23 tff('#skF_11', type, '#skF_11': (A_ltln_set$ * A_ltln_set$ * A_ltln_bool_fun$) > A_ltln$).
% 29.24/10.23 tff(phi$, type, phi$: A_ltln$).
% 29.24/10.23 tff('#skF_115', type, '#skF_115': (A_ltln_set_set_set$ * A_ltln_set_set$) > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_133', type, '#skF_133': A_ltln_set_set$ > A_ltln_set_set$).
% 29.24/10.23 tff('#skF_78', type, '#skF_78': (A_ltln_set$ * A_ltln_a_ltln_bool_fun_fun$) > A_ltln$).
% 29.24/10.23 tff('#skF_17', type, '#skF_17': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_set_fun$) > A_ltln_set$).
% 29.24/10.23 tff(x$, type, x$: A_ltln_set$).
% 29.24/10.23 tff('#skF_176', type, '#skF_176': (A_ltln_set$ * A_ltln_set_bool_fun$) > A_ltln_set$).
% 29.24/10.23 tff(y$, type, y$: A_ltln_set$).
% 29.24/10.23 tff('#skF_163', type, '#skF_163': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff(comp_fun_idem$, type, comp_fun_idem$: A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$ > $o).
% 29.24/10.23 tff('#skF_158', type, '#skF_158': (A_ltln_set_set$ * A_ltln_set_set$ * A_ltln_set_set_bool_fun$) > A_ltln_set_set$).
% 29.24/10.23 tff(inf_fin$a, type, inf_fin$a: A_ltln_set_set_a_ltln_set_fun$).
% 29.24/10.23 tff(bind$a, type, bind$a: (A_ltln_set_set$ * A_ltln_set_a_ltln_set_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_77', type, '#skF_77': (A_ltln_set_set$ * A_ltln_set_a_ltln_set_bool_fun_fun$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_166', type, '#skF_166': (A_ltln_set$ * A_ltln_set$ * A_ltln_set$) > A_ltln_set$).
% 29.24/10.23 tff('#skF_91', type, '#skF_91': (A_ltln_set$ * A_ltln_set$ * A_ltln_set_a_ltln_set_set_fun$ * A_ltln_set_set$) > A_ltln_set$).
% 29.24/10.23
% 29.24/10.24 tff(f_1793, axiom, (![A__questionmark_v0:A_ltln$]: fun_app$a(finite$, fun_app$h(subformulas_mu$, A__questionmark_v0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom287)).
% 29.24/10.24 tff(f_385, axiom, fun_app$a(fun_app$g(less_eq$, x$), fun_app$h(subformulas_mu$, phi$)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom70)).
% 29.24/10.24 tff(f_4007, axiom, (![A__questionmark_v0:A_ltln_set$, A__questionmark_v1:A_ltln_set$]: (fun_app$a(fun_app$g(less_eq$, A__questionmark_v0), A__questionmark_v1) => (fun_app$c(fun_app$d(inf$, A__questionmark_v1), A__questionmark_v0) = A__questionmark_v0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom604)).
% 29.24/10.24 tff(f_3438, axiom, (![A__questionmark_v0:A_ltln_set$, A__questionmark_v1:A_ltln_set$]: ((fun_app$a(finite$, A__questionmark_v0) | fun_app$a(finite$, A__questionmark_v1)) => fun_app$a(finite$, fun_app$c(fun_app$d(inf$, A__questionmark_v0), A__questionmark_v1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom479)).
% 29.24/10.24 tff(f_1796, axiom, (![A__questionmark_v0:A_ltln$]: fun_app$a(finite$, fun_app$h(subformulas_nu$, A__questionmark_v0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom288)).
% 29.24/10.24 tff(f_383, axiom, fun_app$a(fun_app$g(less_eq$, y$), fun_app$h(subformulas_nu$, phi$)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom69)).
% 29.24/10.24 tff(f_361, axiom, (![A__questionmark_v0:A_ltln_set$, A__questionmark_v1:A_ltln_set$]: (~fun_app$a(finite$, fun_app$c(fun_app$d(sup$, A__questionmark_v0), A__questionmark_v1)) <=> (~fun_app$a(finite$, A__questionmark_v0) | ~fun_app$a(finite$, A__questionmark_v1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom64)).
% 29.24/10.24 tff(f_44, negated_conjecture, ~fun_app$a(finite$, fun_app$c(fun_app$d(sup$, x$), y$)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conjecture2)).
% 29.24/10.24 tff(c_926, plain, (![A__questionmark_v0_764:A_ltln$]: (fun_app$a(finite$, fun_app$h(subformulas_mu$, A__questionmark_v0_764)))), inference(cnfTransformation, [status(thm)], [f_1793])).
% 29.24/10.24 tff(c_230, plain, (fun_app$a(fun_app$g(less_eq$, x$), fun_app$h(subformulas_mu$, phi$))), inference(cnfTransformation, [status(thm)], [f_385])).
% 29.24/10.24 tff(c_9086, plain, (![A__questionmark_v1_2135:A_ltln_set$, A__questionmark_v0_2136:A_ltln_set$]: (fun_app$c(fun_app$d(inf$, A__questionmark_v1_2135), A__questionmark_v0_2136)=A__questionmark_v0_2136 | ~fun_app$a(fun_app$g(less_eq$, A__questionmark_v0_2136), A__questionmark_v1_2135))), inference(cnfTransformation, [status(thm)], [f_4007])).
% 29.24/10.24 tff(c_9185, plain, (fun_app$c(fun_app$d(inf$, fun_app$h(subformulas_mu$, phi$)), x$)=x$), inference(resolution, [status(thm)], [c_230, c_9086])).
% 29.24/10.24 tff(c_1758, plain, (![A__questionmark_v0_1318:A_ltln_set$, A__questionmark_v1_1319:A_ltln_set$]: (~fun_app$a(finite$, A__questionmark_v0_1318) | fun_app$a(finite$, fun_app$c(fun_app$d(inf$, A__questionmark_v0_1318), A__questionmark_v1_1319)))), inference(cnfTransformation, [status(thm)], [f_3438])).
% 29.24/10.24 tff(c_9203, plain, (~fun_app$a(finite$, fun_app$h(subformulas_mu$, phi$)) | fun_app$a(finite$, x$)), inference(superposition, [status(thm), theory('equality')], [c_9185, c_1758])).
% 29.24/10.24 tff(c_9237, plain, (fun_app$a(finite$, x$)), inference(demodulation, [status(thm), theory('equality')], [c_926, c_9203])).
% 29.24/10.24 tff(c_928, plain, (![A__questionmark_v0_765:A_ltln$]: (fun_app$a(finite$, fun_app$h(subformulas_nu$, A__questionmark_v0_765)))), inference(cnfTransformation, [status(thm)], [f_1796])).
% 29.24/10.24 tff(c_228, plain, (fun_app$a(fun_app$g(less_eq$, y$), fun_app$h(subformulas_nu$, phi$))), inference(cnfTransformation, [status(thm)], [f_383])).
% 29.24/10.24 tff(c_9186, plain, (fun_app$c(fun_app$d(inf$, fun_app$h(subformulas_nu$, phi$)), y$)=y$), inference(resolution, [status(thm)], [c_228, c_9086])).
% 29.24/10.24 tff(c_9309, plain, (~fun_app$a(finite$, fun_app$h(subformulas_nu$, phi$)) | fun_app$a(finite$, y$)), inference(superposition, [status(thm), theory('equality')], [c_9186, c_1758])).
% 29.24/10.24 tff(c_9343, plain, (fun_app$a(finite$, y$)), inference(demodulation, [status(thm), theory('equality')], [c_928, c_9309])).
% 29.24/10.24 tff(c_21630, plain, (![A__questionmark_v1_2499:A_ltln_set$, A__questionmark_v0_2500:A_ltln_set$]: (~fun_app$a(finite$, A__questionmark_v1_2499) | ~fun_app$a(finite$, A__questionmark_v0_2500) | fun_app$a(finite$, fun_app$c(fun_app$d(sup$, A__questionmark_v0_2500), A__questionmark_v1_2499)))), inference(cnfTransformation, [status(thm)], [f_361])).
% 29.24/10.24 tff(c_10, plain, (~fun_app$a(finite$, fun_app$c(fun_app$d(sup$, x$), y$))), inference(cnfTransformation, [status(thm)], [f_44])).
% 29.24/10.24 tff(c_21644, plain, (~fun_app$a(finite$, y$) | ~fun_app$a(finite$, x$)), inference(resolution, [status(thm)], [c_21630, c_10])).
% 29.24/10.24 tff(c_21691, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_9237, c_9343, c_21644])).
% 29.24/10.24 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------