%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL949_4 : TPTP v9.3.1. Released v8.2.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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:13:01 AM UTC 2026
% Result : Theorem 39.09s 15.94s
% Output : CNFRefutation 39.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL949_4 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.04 % 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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 4 21:22:51 UTC 2026
% 0.10/0.36 % CPUTime :
% 39.09/15.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.09/15.95
% 39.09/15.95 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.09/15.97 %$ subclass > qmltpeq > member > disjoint > inductive > function > restrict > unordered_pair > union > ordered_pair > intersection > image > cross_product > compose > apply > #nlpp > sum_class > successor > singleton > second > rotate > range_of > power_class > inverse > flip > first > domain_of > complement > universal_class > successor_relation > null_class > identity_relation > element_relation > #skF_45 > #skF_120 > #skF_54 > #skF_98 > #skF_9 > #skF_40 > #skF_16 > #skF_91 > #skF_56 > #skF_30 > #skF_29 > #skF_112 > #skF_20 > #skF_41 > #skF_66 > #skF_67 > #skF_87 > #skF_1 > #skF_94 > #skF_19 > #skF_27 > #skF_107 > #skF_79 > #skF_60 > #skF_106 > #skF_59 > #skF_88 > #skF_52 > #skF_26 > #skF_73 > #skF_31 > #skF_17 > #skF_12 > #skF_21 > #skF_64 > #skF_95 > #skF_78 > #skF_127 > #skF_102 > #skF_28 > #skF_3 > #skF_80 > #skF_86 > #skF_53 > #skF_4 > #skF_105 > #skF_82 > #skF_39 > #skF_38 > #skF_7 > #skF_116 > #skF_13 > #skF_37 > #skF_24 > #skF_85 > #skF_32 > #skF_15 > #skF_35 > #skF_101 > #skF_42 > #skF_8 > #skF_62 > #skF_70 > #skF_115 > #skF_18 > #skF_48 > #skF_100 > #skF_44 > #skF_46 > #skF_43 > #skF_84 > #skF_10 > #skF_111 > #skF_34 > #skF_72 > #skF_109 > #skF_125 > #skF_119 > #skF_61 > #skF_57 > #skF_33 > #skF_75 > #skF_71 > #skF_36 > #skF_124 > #skF_103 > #skF_69 > #skF_58 > #skF_22 > #skF_117 > #skF_128 > #skF_25 > #skF_14 > #skF_93 > #skF_76 > #skF_126 > #skF_77 > #skF_92 > #skF_55 > #skF_81 > #skF_5 > #skF_96 > #skF_114 > #skF_122 > #skF_108 > #skF_47 > #skF_65 > #skF_118 > #skF_90 > #skF_123 > #skF_99 > #skF_50 > #skF_51 > #skF_63 > #skF_83 > #skF_113 > #skF_129 > #skF_104 > #skF_130 > #skF_121 > #skF_89 > #skF_68 > #skF_2 > #skF_11 > #skF_131 > #skF_6 > #skF_74 > #skF_97 > #skF_49 > #skF_23 > #skF_110
% 39.09/15.97
% 39.09/15.97 %Foreground sorts:
% 39.09/15.97 tff($ki_world, type, $ki_world: $tType ).
% 39.09/15.97
% 39.09/15.97 %Background operators:
% 39.09/15.97
% 39.09/15.97
% 39.09/15.97 %Foreground operators:
% 39.09/15.97 tff(null_class, type, null_class: $i).
% 39.09/15.97 tff('#skF_45', type, '#skF_45': ($i * $i * $ki_world * $ki_world * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_120', type, '#skF_120': ($ki_world * $ki_world * $i * $ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_54', type, '#skF_54': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_98', type, '#skF_98': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_9', type, '#skF_9': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_40', type, '#skF_40': ($i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_16', type, '#skF_16': ($i * $ki_world * $ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_91', type, '#skF_91': ($ki_world * $ki_world * $i * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_56', type, '#skF_56': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_30', type, '#skF_30': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_29', type, '#skF_29': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_112', type, '#skF_112': ($ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_20', type, '#skF_20': ($i * $ki_world * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_41', type, '#skF_41': ($i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_66', type, '#skF_66': ($ki_world * $ki_world * $ki_world * $i * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(rotate, type, rotate: $i > $i).
% 39.09/15.97 tff('#skF_67', type, '#skF_67': ($ki_world * $ki_world * $ki_world * $i * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_87', type, '#skF_87': ($ki_world * $i * $ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_1', type, '#skF_1': $ki_world > $i).
% 39.09/15.97 tff('#skF_94', type, '#skF_94': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(singleton, type, singleton: $i > $i).
% 39.09/15.97 tff('#skF_19', type, '#skF_19': ($ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(sum_class, type, sum_class: $i > $i).
% 39.09/15.97 tff('#skF_27', type, '#skF_27': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_107', type, '#skF_107': ($i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_79', type, '#skF_79': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_60', type, '#skF_60': ($ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_106', type, '#skF_106': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_59', type, '#skF_59': ($ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_88', type, '#skF_88': ($ki_world * $i * $ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_52', type, '#skF_52': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_26', type, '#skF_26': ($ki_world * $ki_world * $ki_world * $i * $i * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(apply, type, apply: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_73', type, '#skF_73': ($ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_31', type, '#skF_31': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_17', type, '#skF_17': ($ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff(member, type, member: ($ki_world * $i * $i) > $o).
% 39.09/15.97 tff(unordered_pair, type, unordered_pair: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_12', type, '#skF_12': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_21', type, '#skF_21': ($i * $ki_world * $i * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_64', type, '#skF_64': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_95', type, '#skF_95': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_78', type, '#skF_78': ($i * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_127', type, '#skF_127': $i).
% 39.09/15.97 tff('#skF_102', type, '#skF_102': ($ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_28', type, '#skF_28': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(inverse, type, inverse: $i > $i).
% 39.09/15.97 tff(ordered_pair, type, ordered_pair: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_3', type, '#skF_3': ($i * $i * $ki_world * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_80', type, '#skF_80': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_86', type, '#skF_86': ($ki_world * $i * $ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(element_relation, type, element_relation: $i).
% 39.09/15.97 tff(intersection, type, intersection: ($i * $i) > $i).
% 39.09/15.97 tff(second, type, second: $i > $i).
% 39.09/15.97 tff(inductive, type, inductive: ($ki_world * $i) > $o).
% 39.09/15.97 tff('#skF_53', type, '#skF_53': ($ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff(union, type, union: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_4', type, '#skF_4': ($i * $i * $ki_world * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_105', type, '#skF_105': ($ki_world * $i * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_82', type, '#skF_82': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(subclass, type, subclass: ($ki_world * $i * $i) > $o).
% 39.09/15.97 tff('#skF_39', type, '#skF_39': ($i * $ki_world * $ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_38', type, '#skF_38': ($i * $ki_world * $ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_7', type, '#skF_7': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(flip, type, flip: $i > $i).
% 39.09/15.97 tff('#skF_116', type, '#skF_116': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_13', type, '#skF_13': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_37', type, '#skF_37': ($i * $ki_world * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(power_class, type, power_class: $i > $i).
% 39.09/15.97 tff('#skF_24', type, '#skF_24': ($ki_world * $ki_world * $i * $i * $ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_85', type, '#skF_85': ($ki_world * $i * $ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_32', type, '#skF_32': ($ki_world * $ki_world * $i * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_15', type, '#skF_15': ($ki_world * $ki_world * $i * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_35', type, '#skF_35': ($i * $i * $ki_world * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_101', type, '#skF_101': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_42', type, '#skF_42': ($i * $ki_world * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(disjoint, type, disjoint: ($ki_world * $i * $i) > $o).
% 39.09/15.97 tff('#skF_8', type, '#skF_8': ($ki_world * $ki_world * $i * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_62', type, '#skF_62': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_70', type, '#skF_70': ($ki_world * $ki_world * $ki_world * $i * $i) > $ki_world).
% 39.09/15.97 tff(cross_product, type, cross_product: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_115', type, '#skF_115': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_18', type, '#skF_18': ($ki_world * $i * $ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_48', type, '#skF_48': ($i * $ki_world * $i * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_100', type, '#skF_100': $i).
% 39.09/15.97 tff('#skF_44', type, '#skF_44': ($i * $i * $ki_world * $ki_world * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(restrict, type, restrict: ($i * $i * $i) > $i).
% 39.09/15.97 tff('#skF_46', type, '#skF_46': ($i * $ki_world * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_43', type, '#skF_43': ($i * $ki_world * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_84', type, '#skF_84': ($ki_world * $i * $ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_10', type, '#skF_10': ($ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(complement, type, complement: $i > $i).
% 39.09/15.97 tff('#skF_111', type, '#skF_111': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_34', type, '#skF_34': ($ki_world * $ki_world * $i * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_72', type, '#skF_72': ($ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_109', type, '#skF_109': ($i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_125', type, '#skF_125': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_119', type, '#skF_119': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_61', type, '#skF_61': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_57', type, '#skF_57': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_33', type, '#skF_33': ($ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(first, type, first: $i > $i).
% 39.09/15.97 tff('#skF_75', type, '#skF_75': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_71', type, '#skF_71': ($ki_world * $ki_world * $ki_world * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_36', type, '#skF_36': ($i * $ki_world * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_124', type, '#skF_124': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_103', type, '#skF_103': ($ki_world * $i * $ki_world * $ki_world * $i) > $i).
% 39.09/15.97 tff(function, type, function: ($ki_world * $i) > $o).
% 39.09/15.97 tff('#skF_69', type, '#skF_69': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_58', type, '#skF_58': ($ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_22', type, '#skF_22': ($ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(image, type, image: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_117', type, '#skF_117': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_128', type, '#skF_128': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_25', type, '#skF_25': ($ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(range_of, type, range_of: $i > $i).
% 39.09/15.97 tff('#skF_14', type, '#skF_14': ($ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(qmltpeq, type, qmltpeq: ($ki_world * $i * $i) > $o).
% 39.09/15.97 tff('#skF_93', type, '#skF_93': ($ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_76', type, '#skF_76': ($i * $ki_world * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_126', type, '#skF_126': ($ki_world * $i * $ki_world) > $i).
% 39.09/15.97 tff('#skF_77', type, '#skF_77': ($i * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_92', type, '#skF_92': ($ki_world * $ki_world * $i * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_55', type, '#skF_55': ($ki_world * $ki_world * $i * $i * $ki_world) > $i).
% 39.09/15.97 tff('#skF_81', type, '#skF_81': ($ki_world * $ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff(compose, type, compose: ($i * $i) > $i).
% 39.09/15.97 tff('#skF_5', type, '#skF_5': ($ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_96', type, '#skF_96': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(domain_of, type, domain_of: $i > $i).
% 39.09/15.97 tff('#skF_114', type, '#skF_114': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_122', type, '#skF_122': ($ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_108', type, '#skF_108': ($i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_47', type, '#skF_47': ($i * $ki_world * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_65', type, '#skF_65': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_118', type, '#skF_118': ($ki_world * $ki_world * $i * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_90', type, '#skF_90': ($ki_world * $i * $ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_123', type, '#skF_123': ($ki_world * $i * $i * $ki_world * $ki_world) > $i).
% 39.09/15.97 tff('#skF_99', type, '#skF_99': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_50', type, '#skF_50': ($ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_51', type, '#skF_51': ($ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_63', type, '#skF_63': ($ki_world * $ki_world * $ki_world * $ki_world * $i * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_83', type, '#skF_83': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_113', type, '#skF_113': ($ki_world * $ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_129', type, '#skF_129': $ki_world).
% 39.09/15.97 tff(successor, type, successor: $i > $i).
% 39.09/15.97 tff('#skF_104', type, '#skF_104': ($ki_world * $i * $i * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_130', type, '#skF_130': $i).
% 39.09/15.97 tff('#skF_121', type, '#skF_121': ($ki_world * $ki_world * $i * $ki_world * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_89', type, '#skF_89': ($ki_world * $i * $ki_world * $i * $i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_68', type, '#skF_68': ($i * $ki_world * $ki_world * $ki_world * $ki_world * $i * $i) > $ki_world).
% 39.09/15.97 tff('#skF_2', type, '#skF_2': ($ki_world * $i * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff(successor_relation, type, successor_relation: $i).
% 39.09/15.97 tff('#skF_11', type, '#skF_11': ($i * $ki_world * $i * $i * $ki_world * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_131', type, '#skF_131': $ki_world).
% 39.09/15.97 tff(identity_relation, type, identity_relation: $i).
% 39.09/15.97 tff('#skF_6', type, '#skF_6': ($ki_world * $i * $i * $ki_world * $ki_world * $ki_world * $i) > $ki_world).
% 39.09/15.97 tff('#skF_74', type, '#skF_74': ($ki_world * $ki_world * $i * $i * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_97', type, '#skF_97': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff(universal_class, type, universal_class: $i).
% 39.09/15.97 tff('#skF_49', type, '#skF_49': ($i * $ki_world * $i * $ki_world * $i * $ki_world * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_23', type, '#skF_23': ($ki_world * $ki_world * $i * $i * $ki_world) > $ki_world).
% 39.09/15.97 tff('#skF_110', type, '#skF_110': ($ki_world * $i * $ki_world) > $ki_world).
% 39.09/15.97
% 39.09/15.99 tff(f_2631, negated_conjecture, ~(![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![X]: ($ki_exists_in_world_$i(W, X) => (![W0:$ki_world]: ($ki_accessible(W, W0) => subclass(W0, X, X))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', verify)).
% 39.09/15.99 tff(f_30, axiom, (![W:$ki_world]: $ki_accessible(W, W)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mrel_reflexive)).
% 39.09/15.99 tff(f_38, axiom, (![W:$ki_world, X]: $ki_exists_in_world_$i(W, X)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', $ki_exists_in_world_$i_const)).
% 39.09/15.99 tff(f_1376, axiom, (![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![X]: ($ki_exists_in_world_$i(W, X) => (![W0:$ki_world]: ($ki_accessible(W, W0) => (![Y]: ($ki_exists_in_world_$i(W0, Y) => ((![W1:$ki_world]: ($ki_accessible(W0, W1) => ((![W2:$ki_world]: ($ki_accessible(W1, W2) => qmltpeq(W2, X, Y))) => ((![W2:$ki_world]: ($ki_accessible(W1, W2) => subclass(W2, X, Y))) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => subclass(W2, Y, X))))))) & (![W1:$ki_world]: ($ki_accessible(W0, W1) => (((![W2:$ki_world]: ($ki_accessible(W1, W2) => subclass(W2, X, Y))) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => subclass(W2, Y, X)))) => (![W2:$ki_world]: ($ki_accessible(W1, W2) => qmltpeq(W2, X, Y))))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', extensionality)).
% 39.09/15.99 tff(f_51, axiom, (![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![X]: ($ki_exists_in_world_$i(W, X) => (![W0:$ki_world]: ($ki_accessible(W, W0) => qmltpeq(W0, X, X))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 39.09/15.99 tff(c_632, plain, ($ki_accessible('#skF_129', '#skF_131')), inference(cnfTransformation, [status(thm)], [f_2631])).
% 39.09/15.99 tff(c_636, plain, ($ki_accessible($ki_local_world, '#skF_129')), inference(cnfTransformation, [status(thm)], [f_2631])).
% 39.09/15.99 tff(c_2, plain, (![W_1:$ki_world]: ($ki_accessible(W_1, W_1))), inference(cnfTransformation, [status(thm)], [f_30])).
% 39.09/15.99 tff(c_6, plain, (![W_5:$ki_world, X_6]: ($ki_exists_in_world_$i(W_5, X_6))), inference(cnfTransformation, [status(thm)], [f_38])).
% 39.09/15.99 tff(c_248, plain, (![W1_17574:$ki_world, W0_17529:$ki_world, Y_17559, W_17349:$ki_world, W2_17578:$ki_world, X_17469]: ($ki_accessible(W1_17574, '#skF_58'(W0_17529, Y_17559, W_17349, X_17469, W1_17574)) | subclass(W2_17578, X_17469, Y_17559) | ~$ki_accessible(W1_17574, W2_17578) | ~$ki_accessible(W0_17529, W1_17574) | ~$ki_exists_in_world_$i(W0_17529, Y_17559) | ~$ki_accessible(W_17349, W0_17529) | ~$ki_exists_in_world_$i(W_17349, X_17469) | ~$ki_accessible($ki_local_world, W_17349))), inference(cnfTransformation, [status(thm)], [f_1376])).
% 39.09/15.99 tff(c_12553, plain, (![W0_41559:$ki_world, W_41562:$ki_world, W2_41560:$ki_world, Y_41561, W1_41564:$ki_world, X_41563]: ($ki_accessible(W1_41564, '#skF_58'(W0_41559, Y_41561, W_41562, X_41563, W1_41564)) | subclass(W2_41560, X_41563, Y_41561) | ~$ki_accessible(W1_41564, W2_41560) | ~$ki_accessible(W0_41559, W1_41564) | ~$ki_accessible(W_41562, W0_41559) | ~$ki_accessible($ki_local_world, W_41562))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_6, c_248])).
% 39.09/15.99 tff(c_15007, plain, (![W0_41666:$ki_world, Y_41667, W_41668:$ki_world, X_41669]: ($ki_accessible('#skF_129', '#skF_58'(W0_41666, Y_41667, W_41668, X_41669, '#skF_129')) | subclass('#skF_131', X_41669, Y_41667) | ~$ki_accessible(W0_41666, '#skF_129') | ~$ki_accessible(W_41668, W0_41666) | ~$ki_accessible($ki_local_world, W_41668))), inference(resolution, [status(thm)], [c_632, c_12553])).
% 39.09/15.99 tff(c_10, plain, (![W0_15:$ki_world, X_13, W_9:$ki_world]: (qmltpeq(W0_15, X_13, X_13) | ~$ki_accessible(W_9, W0_15) | ~$ki_exists_in_world_$i(W_9, X_13) | ~$ki_accessible($ki_local_world, W_9))), inference(cnfTransformation, [status(thm)], [f_51])).
% 39.09/15.99 tff(c_930, plain, (![W0_15:$ki_world, X_13, W_9:$ki_world]: (qmltpeq(W0_15, X_13, X_13) | ~$ki_accessible(W_9, W0_15) | ~$ki_accessible($ki_local_world, W_9))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_10])).
% 39.09/15.99 tff(c_15099, plain, (![W_41668:$ki_world, Y_41667, X_41669, X_13, W0_41666:$ki_world]: (qmltpeq('#skF_58'(W0_41666, Y_41667, W_41668, X_41669, '#skF_129'), X_13, X_13) | ~$ki_accessible($ki_local_world, '#skF_129') | subclass('#skF_131', X_41669, Y_41667) | ~$ki_accessible(W0_41666, '#skF_129') | ~$ki_accessible(W_41668, W0_41666) | ~$ki_accessible($ki_local_world, W_41668))), inference(resolution, [status(thm)], [c_15007, c_930])).
% 39.09/15.99 tff(c_35128, plain, (![X_42307, W_42309:$ki_world, Y_42310, W0_42308:$ki_world, X_42306]: (qmltpeq('#skF_58'(W0_42308, Y_42310, W_42309, X_42307, '#skF_129'), X_42306, X_42306) | subclass('#skF_131', X_42307, Y_42310) | ~$ki_accessible(W0_42308, '#skF_129') | ~$ki_accessible(W_42309, W0_42308) | ~$ki_accessible($ki_local_world, W_42309))), inference(demodulation, [status(thm), theory('equality')], [c_636, c_15099])).
% 39.09/15.99 tff(c_246, plain, (![W1_17574:$ki_world, W0_17529:$ki_world, Y_17559, W_17349:$ki_world, W2_17578:$ki_world, X_17469]: (~qmltpeq('#skF_58'(W0_17529, Y_17559, W_17349, X_17469, W1_17574), X_17469, Y_17559) | subclass(W2_17578, X_17469, Y_17559) | ~$ki_accessible(W1_17574, W2_17578) | ~$ki_accessible(W0_17529, W1_17574) | ~$ki_exists_in_world_$i(W0_17529, Y_17559) | ~$ki_accessible(W_17349, W0_17529) | ~$ki_exists_in_world_$i(W_17349, X_17469) | ~$ki_accessible($ki_local_world, W_17349))), inference(cnfTransformation, [status(thm)], [f_1376])).
% 39.09/15.99 tff(c_812, plain, (![W1_17574:$ki_world, W0_17529:$ki_world, Y_17559, W_17349:$ki_world, W2_17578:$ki_world, X_17469]: (~qmltpeq('#skF_58'(W0_17529, Y_17559, W_17349, X_17469, W1_17574), X_17469, Y_17559) | subclass(W2_17578, X_17469, Y_17559) | ~$ki_accessible(W1_17574, W2_17578) | ~$ki_accessible(W0_17529, W1_17574) | ~$ki_accessible(W_17349, W0_17529) | ~$ki_accessible($ki_local_world, W_17349))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_6, c_246])).
% 39.09/15.99 tff(c_35135, plain, (![W2_17578:$ki_world, X_42306, W0_42308:$ki_world, W_42309:$ki_world]: (subclass(W2_17578, X_42306, X_42306) | ~$ki_accessible('#skF_129', W2_17578) | subclass('#skF_131', X_42306, X_42306) | ~$ki_accessible(W0_42308, '#skF_129') | ~$ki_accessible(W_42309, W0_42308) | ~$ki_accessible($ki_local_world, W_42309))), inference(resolution, [status(thm)], [c_35128, c_812])).
% 39.09/15.99 tff(c_35355, plain, (![W0_42315:$ki_world, W_42316:$ki_world]: (~$ki_accessible(W0_42315, '#skF_129') | ~$ki_accessible(W_42316, W0_42315) | ~$ki_accessible($ki_local_world, W_42316))), inference(splitLeft, [status(thm)], [c_35135])).
% 39.09/15.99 tff(c_35363, plain, (![W_42317:$ki_world]: (~$ki_accessible(W_42317, '#skF_129') | ~$ki_accessible($ki_local_world, W_42317))), inference(resolution, [status(thm)], [c_2, c_35355])).
% 39.09/15.99 tff(c_35366, plain, (~$ki_accessible($ki_local_world, '#skF_129')), inference(resolution, [status(thm)], [c_2, c_35363])).
% 39.09/15.99 tff(c_35372, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_636, c_35366])).
% 39.09/15.99 tff(c_35373, plain, (![W2_17578:$ki_world, X_42306]: (subclass(W2_17578, X_42306, X_42306) | ~$ki_accessible('#skF_129', W2_17578) | subclass('#skF_131', X_42306, X_42306))), inference(splitRight, [status(thm)], [c_35135])).
% 39.09/15.99 tff(c_35385, plain, (![X_42306]: (~$ki_accessible('#skF_129', '#skF_131') | subclass('#skF_131', X_42306, X_42306))), inference(factorization, [status(thm), theory('equality')], [c_35373])).
% 39.09/15.99 tff(c_35388, plain, (![X_42306]: (subclass('#skF_131', X_42306, X_42306))), inference(demodulation, [status(thm), theory('equality')], [c_632, c_35385])).
% 39.09/15.99 tff(c_630, plain, (~subclass('#skF_131', '#skF_130', '#skF_130')), inference(cnfTransformation, [status(thm)], [f_2631])).
% 39.09/15.99 tff(c_35402, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_35388, c_630])).
% 39.09/15.99 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------