%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP322_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n010.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:38 PM UTC 2025
% Result : Theorem 13.57s 4.32s
% Output : CNFRefutation 13.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP322_1 : TPTP v9.0.0. Released v8.0.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.33 % Computer : n010.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue Apr 8 02:17:02 EDT 2025
% 0.14/0.33 % CPUTime :
% 13.57/4.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.57/4.32
% 13.57/4.32 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.71/4.34 %$ ordering_top$a > ordering_top$ > semilattice_neutr$b > semilattice_neutr$a > semilattice_neutr$ > pairwise$ > ordering_top_axioms$ > minus$b > member$ > less_eq$b > fun_app$l > fun_app$i > fun_app$e > fun_app$ > uminus$b > is_singleton$ > is_empty$ > fun_app$m > fun_app$k > fun_app$j > fun_app$h > fun_app$g > fun_app$f > fun_app$d > fun_app$c > fun_app$b > fun_app$a > def_9 > def_8 > def_41 > def_38 > def_37 > def_33 > def_26 > def_25 > def_24 > def_23 > def_22 > def_21 > def_20 > def_19 > def_16 > def_15 > def_14 > def_13 > def_11 > def_10 > #nlpp > the_elem$ > remove$ > insert$ > def_42 > def_40 > def_39 > def_36 > uu$ > uminus$a > uminus$ > top$b > top$a > top$ > tltrue > tlfalse > sup$b > sup$a > sup$ > minus$a > minus$ > less_eq$a > less_eq$ > less$a > less$ > inf$a > inf$ > def_7 > def_6 > def_5 > def_4 > def_35 > def_34 > def_32 > def_31 > def_30 > def_3 > def_29 > def_28 > def_27 > def_2 > def_18 > def_17 > def_12 > def_1 > collect$ > bot$b > bot$a > bot$ > b$ > a$ > #skF_99 > #skF_14 > #skF_94 > #skF_129 > #skF_118 > #skF_33 > #skF_101 > #skF_123 > #skF_28 > #skF_108 > #skF_81 > #skF_18 > #skF_70 > #skF_46 > #skF_23 > #skF_48 > #skF_103 > #skF_24 > #skF_49 > #skF_37 > #skF_104 > #skF_52 > #skF_121 > #skF_4 > #skF_75 > #skF_39 > #skF_68 > #skF_112 > #skF_87 > #skF_107 > #skF_54 > #skF_77 > #skF_86 > #skF_22 > #skF_53 > #skF_41 > #skF_1 > #skF_21 > #skF_89 > #skF_64 > #skF_110 > #skF_135 > #skF_62 > #skF_124 > #skF_6 > #skF_74 > #skF_97 > #skF_65 > #skF_114 > #skF_69 > #skF_58 > #skF_78 > #skF_131 > #skF_55 > #skF_27 > #skF_19 > #skF_29 > #skF_40 > #skF_98 > #skF_16 > #skF_102 > #skF_13 > #skF_59 > #skF_115 > #skF_8 > #skF_2 > #skF_61 > #skF_133 > #skF_11 > #skF_119 > #skF_50 > #skF_7 > #skF_84 > #skF_125 > #skF_45 > #skF_88 > #skF_38 > #skF_3 > #skF_134 > #skF_132 > #skF_30 > #skF_26 > #skF_20 > #skF_36 > #skF_73 > #skF_71 > #skF_82 > #skF_116 > #skF_113 > #skF_32 > #skF_34 > #skF_96 > #skF_91 > #skF_109 > #skF_10 > #skF_47 > #skF_136 > #skF_56 > #skF_100 > #skF_43 > #skF_60 > #skF_130 > #skF_79 > #skF_63 > #skF_122 > #skF_105 > #skF_80 > #skF_17 > #skF_9 > #skF_111 > #skF_127 > #skF_93 > #skF_42 > #skF_5 > #skF_66 > #skF_85 > #skF_117 > #skF_15 > #skF_128 > #skF_83 > #skF_12 > #skF_67 > #skF_106 > #skF_76 > #skF_90 > #skF_120 > #skF_126 > #skF_31 > #skF_51 > #skF_72 > #skF_25 > #skF_44 > #skF_95 > #skF_35 > #skF_57 > #skF_92
% 13.71/4.34
% 13.71/4.34 %Foreground sorts:
% 13.71/4.34 tff(B_bool_fun_b_bool_fun_bool_fun_fun$, type, B_bool_fun_b_bool_fun_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(B_bool_fun_b_set_fun$, type, B_bool_fun_b_set_fun$: $tType ).
% 13.71/4.34 tff(B_b_bool_fun_fun$, type, B_b_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(B$, type, B$: $tType ).
% 13.71/4.34 tff(tlbool, type, tlbool: $tType ).
% 13.71/4.34 tff(B_set_bool_fun$, type, B_set_bool_fun$: $tType ).
% 13.71/4.34 tff(B_bool_fun$, type, B_bool_fun$: $tType ).
% 13.71/4.34 tff(B_bool_fun_bool_fun$, type, B_bool_fun_bool_fun$: $tType ).
% 13.71/4.34 tff(B_set_b_set_b_set_fun_fun$, type, B_set_b_set_b_set_fun_fun$: $tType ).
% 13.71/4.34 tff(B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$, type, B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$: $tType ).
% 13.71/4.34 tff(B_set$, type, B_set$: $tType ).
% 13.71/4.34 tff(B_set_b_bool_fun_fun$, type, B_set_b_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(Bool_bool_fun$, type, Bool_bool_fun$: $tType ).
% 13.71/4.34 tff(B_bool_fun_b_bool_fun_fun$, type, B_bool_fun_b_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(Bool_bool_bool_fun_fun$, type, Bool_bool_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(B_set_b_set_bool_fun_fun$, type, B_set_b_set_bool_fun_fun$: $tType ).
% 13.71/4.34 tff(B_set_b_set_fun$, type, B_set_b_set_fun$: $tType ).
% 13.71/4.34
% 13.71/4.34 %Background operators:
% 13.71/4.34
% 13.71/4.34
% 13.71/4.34 %Foreground operators:
% 13.71/4.34 tff('#skF_99', type, '#skF_99': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_14', type, '#skF_14': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_94', type, '#skF_94': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_129', type, '#skF_129': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_118', type, '#skF_118': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_33', type, '#skF_33': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(uu$, type, uu$: B_set_b_bool_fun_fun$).
% 13.71/4.34 tff('#skF_101', type, '#skF_101': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff(fun_app$h, type, fun_app$h: (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$) > B_bool_fun_b_bool_fun_fun$).
% 13.71/4.34 tff(def_18, type, def_18: tlbool).
% 13.71/4.34 tff('#skF_123', type, '#skF_123': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_28', type, '#skF_28': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(fun_app$j, type, fun_app$j: (B_set_b_set_bool_fun_fun$ * B_set$) > B_set_bool_fun$).
% 13.71/4.34 tff('#skF_108', type, '#skF_108': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_81', type, '#skF_81': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_18', type, '#skF_18': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(less$a, type, less$a: B_bool_fun_b_bool_fun_bool_fun_fun$).
% 13.71/4.34 tff('#skF_70', type, '#skF_70': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_46', type, '#skF_46': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_23', type, '#skF_23': B_set$ > B$).
% 13.71/4.34 tff('#skF_48', type, '#skF_48': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_32, type, def_32: tlbool).
% 13.71/4.34 tff(sup$, type, sup$: B_set_b_set_b_set_fun_fun$).
% 13.71/4.34 tff('#skF_103', type, '#skF_103': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(fun_app$f, type, fun_app$f: (Bool_bool_bool_fun_fun$ * tlbool) > Bool_bool_fun$).
% 13.71/4.34 tff('#skF_24', type, '#skF_24': B_set$ > B$).
% 13.71/4.34 tff(bot$a, type, bot$a: $o).
% 13.71/4.34 tff('#skF_49', type, '#skF_49': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_37', type, '#skF_37': (B_set$ * B_b_bool_fun_fun$) > B$).
% 13.71/4.34 tff('#skF_104', type, '#skF_104': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_30, type, def_30: tlbool).
% 13.71/4.34 tff(fun_app$c, type, fun_app$c: (B_set_b_set_b_set_fun_fun$ * B_set$) > B_set_b_set_fun$).
% 13.71/4.34 tff(def_11, type, def_11: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_52', type, '#skF_52': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_19, type, def_19: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(bot$, type, bot$: B_set$).
% 13.71/4.34 tff('#skF_121', type, '#skF_121': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_4', type, '#skF_4': B_set$ > B$).
% 13.71/4.34 tff(remove$, type, remove$: B$ > B_set_b_set_fun$).
% 13.71/4.34 tff('#skF_75', type, '#skF_75': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_39', type, '#skF_39': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_68', type, '#skF_68': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_112', type, '#skF_112': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_87', type, '#skF_87': (B_set$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(sup$b, type, sup$b: B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$).
% 13.71/4.34 tff('#skF_107', type, '#skF_107': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(inf$, type, inf$: B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$).
% 13.71/4.34 tff('#skF_54', type, '#skF_54': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_77', type, '#skF_77': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_86', type, '#skF_86': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_22', type, '#skF_22': B_set$ > B$).
% 13.71/4.34 tff('#skF_53', type, '#skF_53': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_6, type, def_6: tlbool).
% 13.71/4.34 tff('#skF_41', type, '#skF_41': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff(a$, type, a$: B$).
% 13.71/4.34 tff(def_35, type, def_35: tlbool).
% 13.71/4.34 tff(def_8, type, def_8: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_1', type, '#skF_1': B_bool_fun$ > B$).
% 13.71/4.34 tff('#skF_21', type, '#skF_21': B_set$ > B$).
% 13.71/4.34 tff(def_14, type, def_14: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(tlfalse, type, tlfalse: tlbool).
% 13.71/4.34 tff('#skF_89', type, '#skF_89': B_set$ > B$).
% 13.71/4.34 tff(uminus$a, type, uminus$a: B_bool_fun_b_bool_fun_fun$).
% 13.71/4.34 tff('#skF_64', type, '#skF_64': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(the_elem$, type, the_elem$: B_set$ > B$).
% 13.71/4.34 tff('#skF_110', type, '#skF_110': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(fun_app$a, type, fun_app$a: (B_set_b_bool_fun_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_135', type, '#skF_135': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(ordering_top_axioms$, type, ordering_top_axioms$: (B_set_b_set_bool_fun_fun$ * B_set$) > $o).
% 13.71/4.34 tff('#skF_62', type, '#skF_62': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_13, type, def_13: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(pairwise$, type, pairwise$: (B_b_bool_fun_fun$ * B_set$) > $o).
% 13.71/4.34 tff('#skF_124', type, '#skF_124': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_9, type, def_9: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(def_26, type, def_26: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(top$a, type, top$a: $o).
% 13.71/4.34 tff(def_7, type, def_7: tlbool).
% 13.71/4.34 tff('#skF_6', type, '#skF_6': B$).
% 13.71/4.34 tff(def_21, type, def_21: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(insert$, type, insert$: B$ > B_set_b_set_fun$).
% 13.71/4.34 tff('#skF_74', type, '#skF_74': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_28, type, def_28: tlbool).
% 13.71/4.34 tff('#skF_97', type, '#skF_97': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_65', type, '#skF_65': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_31, type, def_31: tlbool).
% 13.71/4.34 tff('#skF_114', type, '#skF_114': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_69', type, '#skF_69': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_34, type, def_34: tlbool).
% 13.71/4.34 tff('#skF_58', type, '#skF_58': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_33, type, def_33: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_78', type, '#skF_78': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_131', type, '#skF_131': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_20, type, def_20: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_55', type, '#skF_55': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_27', type, '#skF_27': (B_set$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_19', type, '#skF_19': (B$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_29', type, '#skF_29': (B_b_bool_fun_fun$ * B_set$ * B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff(def_25, type, def_25: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(uminus$, type, uminus$: B_set_b_set_fun$).
% 13.71/4.34 tff('#skF_40', type, '#skF_40': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_98', type, '#skF_98': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_16', type, '#skF_16': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(minus$b, type, minus$b: (tlbool * tlbool) > $o).
% 13.71/4.34 tff('#skF_102', type, '#skF_102': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_13', type, '#skF_13': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_59', type, '#skF_59': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_115', type, '#skF_115': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_8', type, '#skF_8': (B$ * B_set$) > B_set$).
% 13.71/4.34 tff(fun_app$, type, fun_app$: (B_bool_fun$ * B$) > $o).
% 13.71/4.34 tff(sup$a, type, sup$a: Bool_bool_bool_fun_fun$).
% 13.71/4.34 tff('#skF_2', type, '#skF_2': B_bool_fun$ > B$).
% 13.71/4.34 tff(def_24, type, def_24: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_61', type, '#skF_61': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_23, type, def_23: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(less_eq$, type, less_eq$: B_set_b_set_bool_fun_fun$).
% 13.71/4.34 tff(def_22, type, def_22: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_133', type, '#skF_133': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_11', type, '#skF_11': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_119', type, '#skF_119': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_29, type, def_29: tlbool).
% 13.71/4.34 tff(is_singleton$, type, is_singleton$: B_set$ > $o).
% 13.71/4.34 tff('#skF_50', type, '#skF_50': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_7', type, '#skF_7': B_set$ > B$).
% 13.71/4.34 tff('#skF_84', type, '#skF_84': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_125', type, '#skF_125': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_45', type, '#skF_45': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_36, type, def_36: tlbool > tlbool).
% 13.71/4.34 tff('#skF_88', type, '#skF_88': (B_set$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_38', type, '#skF_38': (B_set$ * B_set$ * B_set_b_bool_fun_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_3', type, '#skF_3': B_set$ > B$).
% 13.71/4.34 tff('#skF_134', type, '#skF_134': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_16, type, def_16: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(top$b, type, top$b: B_bool_fun$).
% 13.71/4.34 tff('#skF_132', type, '#skF_132': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_30', type, '#skF_30': (B_b_bool_fun_fun$ * B_set$ * B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_26', type, '#skF_26': (B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff(semilattice_neutr$, type, semilattice_neutr$: (Bool_bool_bool_fun_fun$ * tlbool) > $o).
% 13.71/4.34 tff('#skF_20', type, '#skF_20': (B$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(ordering_top$a, type, ordering_top$a: (B_set_b_set_bool_fun_fun$ * B_set_b_set_bool_fun_fun$ * B_set$) > $o).
% 13.71/4.34 tff(def_10, type, def_10: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(def_39, type, def_39: tlbool > tlbool).
% 13.71/4.34 tff(minus$a, type, minus$a: B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$).
% 13.71/4.34 tff(semilattice_neutr$b, type, semilattice_neutr$b: (B_set_b_set_b_set_fun_fun$ * B_set$) > $o).
% 13.71/4.34 tff('#skF_36', type, '#skF_36': (B_set$ * B_b_bool_fun_fun$) > B$).
% 13.71/4.34 tff(def_4, type, def_4: tlbool).
% 13.71/4.34 tff('#skF_73', type, '#skF_73': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_71', type, '#skF_71': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_82', type, '#skF_82': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_116', type, '#skF_116': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_113', type, '#skF_113': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_32', type, '#skF_32': (B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff(fun_app$e, type, fun_app$e: (Bool_bool_fun$ * tlbool) > $o).
% 13.71/4.34 tff(less_eq$b, type, less_eq$b: (tlbool * tlbool) > $o).
% 13.71/4.34 tff('#skF_34', type, '#skF_34': (B_set$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_96', type, '#skF_96': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff(fun_app$m, type, fun_app$m: (B_bool_fun_b_bool_fun_bool_fun_fun$ * B_bool_fun$) > B_bool_fun_bool_fun$).
% 13.71/4.34 tff(def_3, type, def_3: tlbool).
% 13.71/4.34 tff('#skF_91', type, '#skF_91': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_109', type, '#skF_109': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_10', type, '#skF_10': (B$ * B_set$) > B_set$).
% 13.71/4.34 tff(fun_app$d, type, fun_app$d: (B_bool_fun_b_set_fun$ * B_bool_fun$) > B_set$).
% 13.71/4.34 tff('#skF_47', type, '#skF_47': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_136', type, '#skF_136': (B_set$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_56', type, '#skF_56': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_100', type, '#skF_100': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff(semilattice_neutr$a, type, semilattice_neutr$a: (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$) > $o).
% 13.71/4.34 tff(member$, type, member$: (B$ * B_set$) > $o).
% 13.71/4.34 tff('#skF_43', type, '#skF_43': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(minus$, type, minus$: B_set_b_set_b_set_fun_fun$).
% 13.71/4.34 tff('#skF_60', type, '#skF_60': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_130', type, '#skF_130': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_79', type, '#skF_79': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_40, type, def_40: tlbool > tlbool).
% 13.71/4.34 tff('#skF_63', type, '#skF_63': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_15, type, def_15: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff(def_41, type, def_41: (B_bool_fun$ * B$) > tlbool).
% 13.71/4.34 tff('#skF_122', type, '#skF_122': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_105', type, '#skF_105': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(uminus$b, type, uminus$b: tlbool > $o).
% 13.71/4.34 tff('#skF_80', type, '#skF_80': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_17', type, '#skF_17': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_9', type, '#skF_9': (B$ * B_set$ * B$ * B_set$) > B_set$).
% 13.71/4.34 tff(fun_app$b, type, fun_app$b: (B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_111', type, '#skF_111': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(ordering_top$, type, ordering_top$: (B_bool_fun_b_bool_fun_bool_fun_fun$ * B_bool_fun_b_bool_fun_bool_fun_fun$ * B_bool_fun$) > $o).
% 13.71/4.34 tff(inf$a, type, inf$a: B_set_b_set_b_set_fun_fun$).
% 13.71/4.34 tff(fun_app$i, type, fun_app$i: (B_set_bool_fun$ * B_set$) > $o).
% 13.71/4.34 tff('#skF_127', type, '#skF_127': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(def_42, type, def_42: tlbool > tlbool).
% 13.71/4.34 tff(less_eq$a, type, less_eq$a: B_bool_fun_b_bool_fun_bool_fun_fun$).
% 13.71/4.34 tff(def_12, type, def_12: tlbool).
% 13.71/4.34 tff('#skF_93', type, '#skF_93': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_42', type, '#skF_42': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_5', type, '#skF_5': B_set$ > B$).
% 13.71/4.34 tff(def_38, type, def_38: (tlbool * tlbool) > tlbool).
% 13.71/4.34 tff(def_5, type, def_5: tlbool).
% 13.71/4.34 tff(top$, type, top$: B_set$).
% 13.71/4.34 tff(def_1, type, def_1: tlbool).
% 13.71/4.34 tff(def_37, type, def_37: (tlbool * tlbool) > tlbool).
% 13.71/4.34 tff(tltrue, type, tltrue: tlbool).
% 13.71/4.34 tff(fun_app$k, type, fun_app$k: (B_b_bool_fun_fun$ * B$) > B_bool_fun$).
% 13.71/4.34 tff(def_27, type, def_27: tlbool).
% 13.71/4.34 tff('#skF_66', type, '#skF_66': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_85', type, '#skF_85': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_117', type, '#skF_117': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_15', type, '#skF_15': (B_set$ * B_set$ * B_bool_fun$) > B$).
% 13.71/4.34 tff('#skF_128', type, '#skF_128': (B_set$ * B_set_b_set_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_83', type, '#skF_83': (B_set_b_set_b_set_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_12', type, '#skF_12': (B_bool_fun$ * B_bool_fun$) > B$).
% 13.71/4.34 tff(less$, type, less$: B_set_b_set_bool_fun_fun$).
% 13.71/4.34 tff(def_17, type, def_17: tlbool).
% 13.71/4.34 tff(fun_app$g, type, fun_app$g: (B_bool_fun_b_bool_fun_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(is_empty$, type, is_empty$: B_set$ > $o).
% 13.71/4.34 tff('#skF_67', type, '#skF_67': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_106', type, '#skF_106': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_76', type, '#skF_76': (B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff(collect$, type, collect$: B_bool_fun_b_set_fun$).
% 13.71/4.34 tff(fun_app$l, type, fun_app$l: (B_bool_fun_bool_fun$ * B_bool_fun$) > $o).
% 13.71/4.34 tff('#skF_90', type, '#skF_90': (B_bool_fun$ * B_set_b_bool_fun_fun$ * B_set$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_120', type, '#skF_120': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff('#skF_126', type, '#skF_126': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_31', type, '#skF_31': (B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff(b$, type, b$: B$).
% 13.71/4.34 tff('#skF_51', type, '#skF_51': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_72', type, '#skF_72': (B_b_bool_fun_fun$ * B$ * B_set$) > B$).
% 13.71/4.34 tff(bot$b, type, bot$b: B_bool_fun$).
% 13.71/4.34 tff('#skF_25', type, '#skF_25': (B_b_bool_fun_fun$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_44', type, '#skF_44': (B_set$ * B_set$ * B_set_b_set_fun$ * B_set$) > B_set$).
% 13.71/4.34 tff(def_2, type, def_2: tlbool).
% 13.71/4.34 tff('#skF_95', type, '#skF_95': (B_bool_fun$ * B_bool_fun_b_bool_fun_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_35', type, '#skF_35': (B_set$ * B_set$) > B$).
% 13.71/4.34 tff('#skF_57', type, '#skF_57': (B_bool_fun$ * B_bool_fun$ * B_bool_fun_b_set_fun$ * B_set$) > B_bool_fun$).
% 13.71/4.34 tff('#skF_92', type, '#skF_92': (B_set$ * B_bool_fun_b_set_fun$ * B_bool_fun$ * B_bool_fun$) > B_bool_fun$).
% 13.71/4.34
% 13.71/4.34 tff(f_3486, axiom, (![A__questionmark_v0:B_set$]: (fun_app$b(fun_app$c(sup$, fun_app$b(uminus$, A__questionmark_v0)), A__questionmark_v0) = top$)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom563)).
% 13.71/4.34 tff(f_3489, axiom, (![A__questionmark_v0:B_set$]: (fun_app$b(uminus$, A__questionmark_v0) = fun_app$b(fun_app$c(minus$, top$), A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom564)).
% 13.71/4.34 tff(f_39, negated_conjecture, ~(top$ = fun_app$b(fun_app$c(sup$, fun_app$b(fun_app$c(minus$, top$), fun_app$b(insert$(a$), bot$))), fun_app$b(insert$(a$), bot$))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture1)).
% 13.71/4.34 tff(c_2299, plain, (![A__questionmark_v0_1410:B_set$]: (fun_app$b(fun_app$c(sup$, fun_app$b(uminus$, A__questionmark_v0_1410)), A__questionmark_v0_1410)=top$)), inference(cnfTransformation, [status(thm)], [f_3486])).
% 13.71/4.34 tff(c_2301, plain, (![A__questionmark_v0_1411:B_set$]: (fun_app$b(fun_app$c(minus$, top$), A__questionmark_v0_1411)=fun_app$b(uminus$, A__questionmark_v0_1411))), inference(cnfTransformation, [status(thm)], [f_3489])).
% 13.71/4.34 tff(c_6, plain, (fun_app$b(fun_app$c(sup$, fun_app$b(fun_app$c(minus$, top$), fun_app$b(insert$(a$), bot$))), fun_app$b(insert$(a$), bot$))!=top$), inference(cnfTransformation, [status(thm)], [f_39])).
% 13.71/4.34 tff(c_3318, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_2299, c_2301, c_6])).
% 13.71/4.34 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------