%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC450_1 : TPTP v9.0.0. Released v9.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 : n013.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 09:20:28 PM UTC 2025
% Result : Timeout 287.28s 213.75s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC450_1 : TPTP v9.0.0. Released v9.0.0.
% 0.03/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.13/0.34 % Computer : n013.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 02:31:02 EDT 2025
% 0.13/0.34 % CPUTime :
% 128.25/101.58 ***********************************************************************
% 128.25/101.58 After 99.8 sec it's time to try something different, got 99.7 sec left
% 128.25/101.58 ***********************************************************************
% 273.33/203.01 ***********************************************************************
% 273.33/203.02 After 201.2 sec it's time to try something different, got 98.0 sec left
% 273.33/203.02 ***********************************************************************
% 287.28/213.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 287.28/213.76
% 287.28/213.76 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 287.28/213.77 %$ v3 > v1 > u5 > u4 > u3 > u2 > u1 > u0 > mod:(Int*Int)>Int > h3 > g1 > f2 > f1 > f0 > div:(Int*Int)>Int > #nlpp > v5 > v4 > v2 > v0 > small > h4 > g5 > g4 > g2 > g0 > fast > f5 > f4 > f3
% 287.28/213.77
% 287.28/213.77 %Foreground sorts:
% 287.28/213.77
% 287.28/213.77
% 287.28/213.77 %Background operators:
% 287.28/213.77 tff('#skE_217', type, '#skE_217': $int).
% 287.28/213.77 tff('#skE_46', type, '#skE_46': $int).
% 287.28/213.77 tff('#skE_120', type, '#skE_120': $int).
% 287.28/213.77 tff('#skE_203', type, '#skE_203': $int).
% 287.28/213.77 tff('#skE_189', type, '#skE_189': $int).
% 287.28/213.77 tff('#skE_208', type, '#skE_208': $int).
% 287.28/213.77 tff('#skE_74', type, '#skE_74': $int).
% 287.28/213.77 tff('#skE_7', type, '#skE_7': $int).
% 287.28/213.77 tff('#skE_90', type, '#skE_90': $int).
% 287.28/213.77 tff('#skE_105', type, '#skE_105': $int).
% 287.28/213.77 tff('#skE_213', type, '#skE_213': $int).
% 287.28/213.77 tff('#skE_187', type, '#skE_187': $int).
% 287.28/213.77 tff('#skE_88', type, '#skE_88': $int).
% 287.28/213.77 tff('#skE_121', type, '#skE_121': $int).
% 287.28/213.77 tff('#skE_135', type, '#skE_135': $int).
% 287.28/213.77 tff('#skE_158', type, '#skE_158': $int).
% 287.28/213.77 tff('#skE_95', type, '#skE_95': $int).
% 287.28/213.77 tff('#skE_21', type, '#skE_21': $int).
% 287.28/213.77 tff('#skE_179', type, '#skE_179': $int).
% 287.28/213.77 tff('#skE_62', type, '#skE_62': $int).
% 287.28/213.77 tff('#skE_146', type, '#skE_146': $int).
% 287.28/213.77 tff('#skE_30', type, '#skE_30': $int).
% 287.28/213.77 tff('#skE_128', type, '#skE_128': $int).
% 287.28/213.77 tff('#skE_11', type, '#skE_11': $int).
% 287.28/213.77 tff('#skE_185', type, '#skE_185': $int).
% 287.28/213.77 tff('#skE_25', type, '#skE_25': $int).
% 287.28/213.77 tff('#skE_52', type, '#skE_52': $int).
% 287.28/213.77 tff('#skE_28', type, '#skE_28': $int).
% 287.28/213.77 tff('#skE_109', type, '#skE_109': $int).
% 287.28/213.77 tff('#skE_48', type, '#skE_48': $int).
% 287.28/213.77 tff('#skE_155', type, '#skE_155': $int).
% 287.28/213.77 tff('#skE_23', type, '#skE_23': $int).
% 287.28/213.77 tff('#skE_12', type, '#skE_12': $int).
% 287.28/213.77 tff('#skE_41', type, '#skE_41': $int).
% 287.28/213.77 tff('#skE_156', type, '#skE_156': $int).
% 287.28/213.77 tff('#skE_43', type, '#skE_43': $int).
% 287.28/213.77 tff('#skE_162', type, '#skE_162': $int).
% 287.28/213.77 tff('#skE_37', type, '#skE_37': $int).
% 287.28/213.77 tff('#skE_73', type, '#skE_73': $int).
% 287.28/213.77 tff('#skE_80', type, '#skE_80': $int).
% 287.28/213.77 tff('#skE_188', type, '#skE_188': $int).
% 287.28/213.77 tff('#skE_180', type, '#skE_180': $int).
% 287.28/213.77 tff('#skE_174', type, '#skE_174': $int).
% 287.28/213.77 tff('#skE_173', type, '#skE_173': $int).
% 287.28/213.77 tff('#skE_144', type, '#skE_144': $int).
% 287.28/213.77 tff('#skE_211', type, '#skE_211': $int).
% 287.28/213.77 tff('#skE_85', type, '#skE_85': $int).
% 287.28/213.77 tff('#skE_101', type, '#skE_101': $int).
% 287.28/213.77 tff('#skE_154', type, '#skE_154': $int).
% 287.28/213.77 tff('#skE_210', type, '#skE_210': $int).
% 287.28/213.77 tff('#skE_84', type, '#skE_84': $int).
% 287.28/213.77 tff('#skE_216', type, '#skE_216': $int).
% 287.28/213.77 tff(h2, type, h2: $int).
% 287.28/213.77 tff('#skE_42', type, '#skE_42': $int).
% 287.28/213.77 tff('#skE_143', type, '#skE_143': $int).
% 287.28/213.77 tff('#skE_57', type, '#skE_57': $int).
% 287.28/213.77 tff('#skE_86', type, '#skE_86': $int).
% 287.28/213.77 tff('#skE_133', type, '#skE_133': $int).
% 287.28/213.77 tff('#skE_142', type, '#skE_142': $int).
% 287.28/213.77 tff('#skE_201', type, '#skE_201': $int).
% 287.28/213.77 tff('#skE_111', type, '#skE_111': $int).
% 287.28/213.77 tff('#skE_215', type, '#skE_215': $int).
% 287.28/213.77 tff('#skE_200', type, '#skE_200': $int).
% 287.28/213.77 tff('#skE_192', type, '#skE_192': $int).
% 287.28/213.77 tff('#skE_63', type, '#skE_63': $int).
% 287.28/213.77 tff('#skE_102', type, '#skE_102': $int).
% 287.28/213.77 tff('#skE_2', type, '#skE_2': $int).
% 287.28/213.77 tff('#skE_170', type, '#skE_170': $int).
% 287.28/213.77 tff('#skE_1', type, '#skE_1': $int).
% 287.28/213.77 tff('#skE_33', type, '#skE_33': $int).
% 287.28/213.77 tff('#skE_209', type, '#skE_209': $int).
% 287.28/213.77 tff('#skE_97', type, '#skE_97': $int).
% 287.28/213.77 tff('#skE_20', type, '#skE_20': $int).
% 287.28/213.77 tff('#skE_78', type, '#skE_78': $int).
% 287.28/213.77 tff('#skE_159', type, '#skE_159': $int).
% 287.28/213.77 tff('#skE_6', type, '#skE_6': $int).
% 287.28/213.77 tff('#skE_116', type, '#skE_116': $int).
% 287.28/213.77 tff('#skE_196', type, '#skE_196': $int).
% 287.28/213.77 tff('#skE_13', type, '#skE_13': $int).
% 287.28/213.77 tff('#skE_130', type, '#skE_130': $int).
% 287.28/213.77 tff('#skE_118', type, '#skE_118': $int).
% 287.28/213.77 tff('#skE_26', type, '#skE_26': $int).
% 287.28/213.77 tff('#skE_32', type, '#skE_32': $int).
% 287.28/213.77 tff('#skE_92', type, '#skE_92': $int).
% 287.28/213.77 tff('#skE_199', type, '#skE_199': $int).
% 287.28/213.77 tff('#skE_10', type, '#skE_10': $int).
% 287.28/213.77 tff('#skE_184', type, '#skE_184': $int).
% 287.28/213.77 tff('#skE_24', type, '#skE_24': $int).
% 287.28/213.77 tff('#skE_114', type, '#skE_114': $int).
% 287.28/213.77 tff('#skE_212', type, '#skE_212': $int).
% 287.28/213.77 tff('#skE_191', type, '#skE_191': $int).
% 287.28/213.77 tff('#skE_5', type, '#skE_5': $int).
% 287.28/213.77 tff('#skE_138', type, '#skE_138': $int).
% 287.28/213.77 tff('#skE_110', type, '#skE_110': $int).
% 287.28/213.77 tff('#skE_38', type, '#skE_38': $int).
% 287.28/213.77 tff('#skE_31', type, '#skE_31': $int).
% 287.28/213.77 tff('#skE_122', type, '#skE_122': $int).
% 287.28/213.77 tff('#skE_157', type, '#skE_157': $int).
% 287.28/213.77 tff('#skE_51', type, '#skE_51': $int).
% 287.28/213.77 tff('#skE_15', type, '#skE_15': $int).
% 287.28/213.77 tff('#skE_151', type, '#skE_151': $int).
% 287.28/213.77 tff('#skE_8', type, '#skE_8': $int).
% 287.28/213.77 tff('#skE_165', type, '#skE_165': $int).
% 287.28/213.77 tff('#skE_36', type, '#skE_36': $int).
% 287.28/213.77 tff('#skE_69', type, '#skE_69': $int).
% 287.28/213.77 tff('#skE_4', type, '#skE_4': $int).
% 287.28/213.77 tff('#skE_149', type, '#skE_149': $int).
% 287.28/213.77 tff('#skE_54', type, '#skE_54': $int).
% 287.28/213.77 tff('#skE_197', type, '#skE_197': $int).
% 287.28/213.77 tff('#skE_164', type, '#skE_164': $int).
% 287.28/213.77 tff('#skE_76', type, '#skE_76': $int).
% 287.28/213.77 tff('#skE_70', type, '#skE_70': $int).
% 287.28/213.77 tff('#skE_64', type, '#skE_64': $int).
% 287.28/213.77 tff('#skE_82', type, '#skE_82': $int).
% 287.28/213.77 tff('#skE_103', type, '#skE_103': $int).
% 287.28/213.77 tff('#skE_60', type, '#skE_60': $int).
% 287.28/213.77 tff('#skE_50', type, '#skE_50': $int).
% 287.28/213.77 tff('#skE_104', type, '#skE_104': $int).
% 287.28/213.77 tff('#skE_150', type, '#skE_150': $int).
% 287.28/213.77 tff('#skE_137', type, '#skE_137': $int).
% 287.28/213.77 tff('#skE_113', type, '#skE_113': $int).
% 287.28/213.77 tff('#skE_190', type, '#skE_190': $int).
% 287.28/213.77 tff('#skE_129', type, '#skE_129': $int).
% 287.28/213.77 tff('#skE_22', type, '#skE_22': $int).
% 287.28/213.77 tff('#skE_16', type, '#skE_16': $int).
% 287.28/213.77 tff('#skE_17', type, '#skE_17': $int).
% 287.28/213.77 tff('#skE_3', type, '#skE_3': $int).
% 287.28/213.77 tff('#skE_183', type, '#skE_183': $int).
% 287.28/213.77 tff('#skE_55', type, '#skE_55': $int).
% 287.28/213.77 tff('#skE_123', type, '#skE_123': $int).
% 287.28/213.77 tff('#skE_204', type, '#skE_204': $int).
% 287.28/213.77 tff('#skF_1', type, '#skF_1': $int).
% 287.28/213.77 tff('#skE_77', type, '#skE_77': $int).
% 287.28/213.77 tff('#skE_163', type, '#skE_163': $int).
% 287.28/213.77 tff('#skE_195', type, '#skE_195': $int).
% 287.28/213.77 tff('#skE_79', type, '#skE_79': $int).
% 287.28/213.77 tff('#skE_161', type, '#skE_161': $int).
% 287.28/213.77 tff('#skE_127', type, '#skE_127': $int).
% 287.28/213.77 tff('#skE_181', type, '#skE_181': $int).
% 287.28/213.77 tff('#skE_124', type, '#skE_124': $int).
% 287.28/213.77 tff(g3, type, g3: $int).
% 287.28/213.77 tff('#skE_171', type, '#skE_171': $int).
% 287.28/213.77 tff('#skE_71', type, '#skE_71': $int).
% 287.28/213.77 tff('#skE_198', type, '#skE_198': $int).
% 287.28/213.77 tff('#skE_134', type, '#skE_134': $int).
% 287.28/213.77 tff('#skE_178', type, '#skE_178': $int).
% 287.28/213.77 tff('#skE_175', type, '#skE_175': $int).
% 287.28/213.77 tff('#skE_91', type, '#skE_91': $int).
% 287.28/213.77 tff('#skE_67', type, '#skE_67': $int).
% 287.28/213.77 tff('#skE_58', type, '#skE_58': $int).
% 287.28/213.77 tff('#skE_87', type, '#skE_87': $int).
% 287.28/213.77 tff('#skE_47', type, '#skE_47': $int).
% 287.28/213.77 tff('#skE_68', type, '#skE_68': $int).
% 287.28/213.77 tff('#skE_40', type, '#skE_40': $int).
% 287.28/213.77 tff('#skE_9', type, '#skE_9': $int).
% 287.28/213.77 tff('#skE_75', type, '#skE_75': $int).
% 287.28/213.77 tff('#skE_117', type, '#skE_117': $int).
% 287.28/213.77 tff('#skE_29', type, '#skE_29': $int).
% 287.28/213.77 tff('#skE_44', type, '#skE_44': $int).
% 287.28/213.77 tff('#skE_49', type, '#skE_49': $int).
% 287.28/213.77 tff('#skE_34', type, '#skE_34': $int).
% 287.28/213.77 tff('#skE_45', type, '#skE_45': $int).
% 287.28/213.77 tff('#skE_169', type, '#skE_169': $int).
% 287.28/213.77 tff('#skE_96', type, '#skE_96': $int).
% 287.28/213.77 tff(h5, type, h5: $int).
% 287.28/213.77 tff('#skE_168', type, '#skE_168': $int).
% 287.28/213.77 tff('#skE_27', type, '#skE_27': $int).
% 287.28/213.77 tff('#skE_147', type, '#skE_147': $int).
% 287.28/213.77 tff('#skE_115', type, '#skE_115': $int).
% 287.28/213.77 tff('#skE_176', type, '#skE_176': $int).
% 287.28/213.77 tff('#skE_100', type, '#skE_100': $int).
% 287.28/213.77 tff('#skE_152', type, '#skE_152': $int).
% 287.28/213.77 tff('#skE_141', type, '#skE_141': $int).
% 287.28/213.77 tff('#skE_59', type, '#skE_59': $int).
% 287.28/213.77 tff('#skE_18', type, '#skE_18': $int).
% 287.28/213.77 tff('#skE_194', type, '#skE_194': $int).
% 287.28/213.77 tff('#skE_218', type, '#skE_218': $int).
% 287.28/213.77 tff('#skE_140', type, '#skE_140': $int).
% 287.28/213.77 tff('#skE_83', type, '#skE_83': $int).
% 287.28/213.77 tff('#skE_206', type, '#skE_206': $int).
% 287.28/213.77 tff('#skE_131', type, '#skE_131': $int).
% 287.28/213.77 tff('#skE_93', type, '#skE_93': $int).
% 287.28/213.77 tff('#skE_214', type, '#skE_214': $int).
% 287.28/213.77 tff('#skE_125', type, '#skE_125': $int).
% 287.28/213.77 tff('#skE_167', type, '#skE_167': $int).
% 287.28/213.77 tff('#skE_136', type, '#skE_136': $int).
% 287.28/213.77 tff('#skE_132', type, '#skE_132': $int).
% 287.28/213.77 tff('#skE_107', type, '#skE_107': $int).
% 287.28/213.77 tff('#skE_219', type, '#skE_219': $int).
% 287.28/213.77 tff('#skE_119', type, '#skE_119': $int).
% 287.28/213.77 tff('#skE_94', type, '#skE_94': $int).
% 287.28/213.77 tff('#skE_182', type, '#skE_182': $int).
% 287.28/213.77 tff('#skE_186', type, '#skE_186': $int).
% 287.28/213.77 tff(h1, type, h1: $int).
% 287.28/213.77 tff('#skE_106', type, '#skE_106': $int).
% 287.28/213.77 tff('#skE_126', type, '#skE_126': $int).
% 287.28/213.77 tff('#skE_153', type, '#skE_153': $int).
% 287.28/213.77 tff('#skE_81', type, '#skE_81': $int).
% 287.28/213.77 tff('#skE_177', type, '#skE_177': $int).
% 287.28/213.77 tff('#skE_112', type, '#skE_112': $int).
% 287.28/213.77 tff('#skE_148', type, '#skE_148': $int).
% 287.28/213.77 tff('#skE_193', type, '#skE_193': $int).
% 287.28/213.77 tff('#skE_145', type, '#skE_145': $int).
% 287.28/213.77 tff('#skE_35', type, '#skE_35': $int).
% 287.28/213.77 tff(h0, type, h0: $int).
% 287.28/213.77 tff('#skE_207', type, '#skE_207': $int).
% 287.28/213.77 tff('#skE_172', type, '#skE_172': $int).
% 287.28/213.77 tff('#skE_108', type, '#skE_108': $int).
% 287.28/213.77 tff('#skE_166', type, '#skE_166': $int).
% 287.28/213.77 tff('#skE_61', type, '#skE_61': $int).
% 287.28/213.77 tff('#skE_99', type, '#skE_99': $int).
% 287.28/213.77 tff('#skE_98', type, '#skE_98': $int).
% 287.28/213.77 tff('#skE_160', type, '#skE_160': $int).
% 287.28/213.77 tff('#skE_39', type, '#skE_39': $int).
% 287.28/213.77 tff('#skE_66', type, '#skE_66': $int).
% 287.28/213.77 tff('#skE_89', type, '#skE_89': $int).
% 287.28/213.77 tff('#skE_19', type, '#skE_19': $int).
% 287.28/213.77 tff('#skE_205', type, '#skE_205': $int).
% 287.28/213.77 tff('#skE_53', type, '#skE_53': $int).
% 287.28/213.77 tff('#skE_65', type, '#skE_65': $int).
% 287.28/213.77 tff('#skE_139', type, '#skE_139': $int).
% 287.28/213.77 tff('#skE_14', type, '#skE_14': $int).
% 287.28/213.77 tff('#skE_202', type, '#skE_202': $int).
% 287.28/213.77 tff('#skE_72', type, '#skE_72': $int).
% 287.28/213.77 tff('#skE_56', type, '#skE_56': $int).
% 287.28/213.77
% 287.28/213.77 %Foreground operators:
% 287.28/213.77 tff(mod:(Int*Int)>Int, type, mod:(Int*Int)>Int: ($int * $int) > $int).
% 287.28/213.77 tff(fast, type, fast: $int > $int).
% 287.28/213.77 tff(f4, type, f4: $int > $int).
% 287.28/213.77 tff(small, type, small: $int > $int).
% 287.28/213.77 tff(f2, type, f2: ($int * $int) > $int).
% 287.28/213.77 tff(v5, type, v5: $int > $int).
% 287.28/213.77 tff(h4, type, h4: $int > $int).
% 287.28/213.77 tff(v3, type, v3: ($int * $int) > $int).
% 287.28/213.77 tff(u5, type, u5: ($int * $int) > $int).
% 287.28/213.77 tff(f3, type, f3: $int > $int).
% 287.28/213.77 tff(u4, type, u4: ($int * $int) > $int).
% 287.28/213.77 tff(g1, type, g1: ($int * $int) > $int).
% 287.28/213.77 tff(u2, type, u2: ($int * $int) > $int).
% 287.28/213.77 tff(u1, type, u1: ($int * $int) > $int).
% 287.28/213.77 tff(u0, type, u0: ($int * $int) > $int).
% 287.28/213.77 tff(g4, type, g4: $int > $int).
% 287.28/213.77 tff(v0, type, v0: $int > $int).
% 287.28/213.77 tff(f5, type, f5: $int > $int).
% 287.28/213.77 tff(div:(Int*Int)>Int, type, div:(Int*Int)>Int: ($int * $int) > $int).
% 287.28/213.77 tff(u3, type, u3: ($int * $int) > $int).
% 287.28/213.77 tff(f0, type, f0: ($int * $int) > $int).
% 287.28/213.77 tff(g0, type, g0: $int > $int).
% 287.28/213.77 tff(v2, type, v2: $int > $int).
% 287.28/213.77 tff(h3, type, h3: ($int * $int) > $int).
% 287.28/213.77 tff(g5, type, g5: $int > $int).
% 287.28/213.77 tff(v1, type, v1: ($int * $int) > $int).
% 287.28/213.77 tff(v4, type, v4: $int > $int).
% 287.28/213.77 tff(g2, type, g2: $int > $int).
% 287.28/213.77 tff(f1, type, f1: ($int * $int) > $int).
% 287.28/213.77
% 287.49/213.79 tff(f_1079, axiom, (![C:$int, B:$int]: (($product(C, B) = C) <=> ((C = 0) | (B = 1)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_cancel_right1)).
% 287.49/213.79 tff(f_151, axiom, (![Xa:$int, Ya:$int]: (f2(Xa, Ya) = $sum($sum(v3(Xa, Ya), Xa), Xa))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_27)).
% 287.49/213.79 tff(f_1063, axiom, (![A:$int, B:$int]: ($product(A, B) = $product(B, A))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_comm)).
% 287.49/213.79 tff(f_1065, axiom, (![A:$int, B:$int, C:$int]: ($product(A, $sum(B, C)) = $sum($product(A, B), $product(A, C)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_dist)).
% 287.49/213.79 tff(f_1071, axiom, (![A:$int, B:$int]: ($uminus($product(A, B)) = $product($uminus(A), B))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', minus_mult_left)).
% 287.49/213.79 tff(f_50, axiom, (![Xa:$int, Ya:$int]: (($lesseq(Xa, 0) => (u1(Xa, Ya) = Ya)) & (~$lesseq(Xa, 0) => (u1(Xa, Ya) = f1(u1($difference(Xa, 1), Ya), Xa))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_4)).
% 287.49/213.79 tff(f_35, axiom, (![Xa:$int, Ya:$int]: (f1(Xa, Ya) = $product($product(Xa, Ya), Ya))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_1)).
% 287.49/213.79 tff(f_1060, axiom, (![M:$int, N:$int]: ($product($sum(1, M), N) = $sum(N, $product(M, N)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_def_2)).
% 287.49/213.79 tff(f_1088, axiom, (![A:$int, B:$int]: (($less(0, A) & $less(0, B)) => $less(0, $product(A, B)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_nonneg_nonneg)).
% 287.49/213.79 tff(c_196, plain, (![C_63:$int]: ($product(C_63, 1)=C_63)), inference(cnfTransformation, [status(thm)], [f_1079])).
% 287.49/213.79 tff(c_195, plain, (![B_64:$int]: ($product(0, B_64)=0)), inference(cnfTransformation, [status(thm)], [f_1079])).
% 287.49/213.79 tff(c_68, plain, (![X_34a:$int, Y_35a:$int]: ($sum($sum(X_34a, v3(X_34a, Y_35a)), X_34a)=f2(X_34a, Y_35a))), inference(cnfTransformation, [status(thm)], [f_151])).
% 287.49/213.79 tff(c_390646, plain, (![X_7809:$int, Y_7810:$int, X_7811:$int]: (v3(X_7809, Y_7810)=$sum(X_7811, f2(X_7809, Y_7810)) | X_7811!=$product($uminus(2), X_7809))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_68])).
% 287.49/213.79 tff(c_390079, plain, (![X_7687:$int, Y_7688:$int, X_7689:$int]: (v3(X_7687, Y_7688)=$sum(X_7689, f2(X_7687, Y_7688)) | X_7689!=$product($uminus(2), X_7687))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_68])).
% 287.49/213.79 tff(c_390652, plain, (![X_7811:$int, X_7809:$int, Y_7810:$int, X_7689:$int]: ($sum(X_7811, f2(X_7809, Y_7810))=$sum(X_7689, f2(X_7809, Y_7810)) | X_7689!=$product($uminus(2), X_7809) | X_7811!=$product($uminus(2), X_7809))), inference(superposition, [status(thm), theory('equality')], [c_390646, c_390079])).
% 287.49/213.79 tff(c_390687, plain, (![X_7815:$int, X_7814:$int, X_7816:$int]: (X_7815=X_7814 | X_7815!=$product($uminus(2), X_7816) | X_7814!=$product($uminus(2), X_7816))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_390652])).
% 287.49/213.79 tff(c_203, plain, (![B_47:$int, A_48:$int]: ($product(B_47, A_48)=$product(A_48, B_47))), inference(cnfTransformation, [status(thm)], [f_1063])).
% 287.49/213.79 tff(c_396124, plain, (![X_8220:$int, B_8221:$int, A_8222:$int, X_8223:$int]: (X_8220=$product(B_8221, A_8222) | $product(A_8222, B_8221)!=$product($uminus(2), X_8223) | X_8220!=$product($uminus(2), X_8223))), inference(superposition, [status(thm), theory('equality')], [c_390687, c_203])).
% 287.49/213.79 tff(c_396170, plain, (![X_8220:$int, B_64:$int, X_8223:$int]: (X_8220=$product(B_64, 0) | $product($uminus(2), X_8223)!=0 | X_8220!=$product($uminus(2), X_8223))), inference(superposition, [status(thm), theory('equality')], [c_195, c_396124])).
% 287.49/213.79 tff(c_396201, plain, (![B_64:$int]: ($product(B_64, 0)=$product($uminus(2), 0))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396170])).
% 287.49/213.79 tff(c_396204, plain, (![B_8227:$int]: ($product(B_8227, 0)=0)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396201])).
% 287.49/213.79 tff(c_92, plain, (![A_49:$int, C_51:$int, B_50:$int]: ($product(A_49, $sum(C_51, B_50))=$sum($product(A_49, B_50), $product(A_49, C_51)))), inference(cnfTransformation, [status(thm)], [f_1065])).
% 287.49/213.79 tff(c_202, plain, (![A_52:$int, X_104:$int, B_53:$int, C_54:$int]: ($product(A_52, X_104)=$sum($product(A_52, B_53), $product(A_52, C_54)) | X_104!=$sum(B_53, C_54))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_92])).
% 287.49/213.79 tff(c_396230, plain, (![B_8227:$int, B_53:$int, C_54:$int]: ($sum($product(B_8227, B_53), $product(B_8227, C_54))=0 | $sum(B_53, C_54)!=0)), inference(superposition, [status(thm), theory('equality')], [c_396204, c_202])).
% 287.49/213.79 tff(c_396356, plain, (![B_8228:$int, C_8229:$int, B_8230:$int]: ($uminus($product(B_8228, C_8229))=$product(B_8228, B_8230) | B_8230!=$uminus(C_8229))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396230])).
% 287.49/213.79 tff(c_396428, plain, (![B_8228:$int, C_8229:$int]: ($uminus($product(B_8228, C_8229))=B_8228 | $uminus(C_8229)!=1)), inference(superposition, [status(thm), theory('equality')], [c_396356, c_196])).
% 287.49/213.79 tff(c_396705, plain, (![B_8235:$int]: ($product(B_8235, $uminus(1))=$uminus(B_8235))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396428])).
% 287.49/213.79 tff(c_396933, plain, (![B_8247:$int]: ($product($uminus(1), B_8247)=$uminus(B_8247))), inference(superposition, [status(thm), theory('equality')], [c_396705, c_203])).
% 287.49/213.79 tff(c_198, plain, (![A_57:$int, B_58:$int, X_103:$int]: ($uminus($product(A_57, B_58))=$product(X_103, B_58) | X_103!=$uminus(A_57))), inference(cnfTransformation, [status(thm)], [f_1071])).
% 287.49/213.79 tff(c_200, plain, (![X_103:$int, B_58:$int, A_57:$int]: ($uminus($product(X_103, B_58))=$product(A_57, B_58) | X_103!=$uminus(A_57))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_198])).
% 287.49/213.79 tff(c_396986, plain, (![A_57:$int, B_8247:$int]: ($product(A_57, B_8247)=$uminus($uminus(B_8247)) | $uminus(A_57)!=$uminus(1))), inference(superposition, [status(thm), theory('equality')], [c_396933, c_200])).
% 287.49/213.79 tff(c_397106, plain, (![B_8247:$int]: ($product(1, B_8247)=B_8247)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396986])).
% 287.49/213.79 tff(c_6, plain, (![X_5a:$int, Y_6a:$int]: (u1(X_5a, Y_6a)=Y_6a | ~$lesseq(X_5a, 0))), inference(cnfTransformation, [status(thm)], [f_50])).
% 287.49/213.79 tff(c_390105, plain, (![X_7740:$int, Y_7741:$int]: (u1(X_7740, Y_7741)=Y_7741 | $less(0, X_7740))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_6])).
% 287.49/213.79 tff(c_390107, plain, (![X_7744:$int, Y_7745:$int]: (f1(X_7744, Y_7745)=$product($product(X_7744, Y_7745), Y_7745))), inference(cnfTransformation, [status(thm)], [f_35])).
% 287.49/213.79 tff(c_8, plain, (![X_5a:$int, Y_6a:$int]: (f1(u1($sum($uminus(1), X_5a), Y_6a), X_5a)=u1(X_5a, Y_6a) | $lesseq(X_5a, 0))), inference(cnfTransformation, [status(thm)], [f_50])).
% 287.49/213.79 tff(c_390104, plain, (![X_7737:$int, Y_7738:$int, X_7739:$int]: (u1(X_7737, Y_7738)=f1(u1(X_7739, Y_7738), X_7737) | X_7739!=$sum($uminus(1), X_7737) | ~$less(0, X_7737))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_8])).
% 287.49/213.79 tff(c_390190, plain, (![X_7737:$int, Y_7738:$int, X_7739:$int]: (u1(X_7737, Y_7738)=$product($product(u1(X_7739, Y_7738), X_7737), X_7737) | X_7739!=$sum($uminus(1), X_7737) | ~$less(0, X_7737))), inference(demodulation, [status(thm), theory('equality')], [c_390107, c_390104])).
% 287.49/213.79 tff(c_394888, plain, (![X_8160:$int, Y_8161:$int, X_8162:$int]: (u1(X_8160, Y_8161)=$product(X_8160, $product(u1(X_8162, Y_8161), X_8160)) | X_8162!=$sum($uminus(1), X_8160) | ~$less(0, X_8160))), inference(demodulation, [status(thm), theory('equality')], [c_203, c_390190])).
% 287.49/213.79 tff(c_409099, plain, (![X_8962:$int, Y_8963:$int, X_8964:$int]: (u1(X_8962, Y_8963)=$product(X_8962, $product(Y_8963, X_8962)) | X_8964!=$sum($uminus(1), X_8962) | ~$less(0, X_8962) | $less(0, X_8964))), inference(superposition, [status(thm), theory('equality')], [c_390105, c_394888])).
% 287.49/213.79 tff(c_395115, plain, (![Y_8161:$int]: ($product(1, u1($sum($uminus(1), 1), Y_8161))=u1(1, Y_8161) | ~$less(0, 1))), inference(superposition, [status(thm), theory('equality')], [c_196, c_394888])).
% 287.49/213.79 tff(c_395117, plain, (![Y_8161:$int]: (u1(1, Y_8161)=$product(1, u1(0, Y_8161)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_395115])).
% 287.49/213.79 tff(c_397158, plain, (![Y_8161:$int]: (u1(1, Y_8161)=u1(0, Y_8161))), inference(demodulation, [status(thm), theory('equality')], [c_397106, c_395117])).
% 287.49/213.79 tff(c_409119, plain, (![Y_8963:$int]: (u1(0, Y_8963)=$product(1, $product(Y_8963, 1)) | ~$less(0, 1) | $less(0, $sum($uminus(1), 1)))), inference(superposition, [status(thm), theory('equality')], [c_409099, c_397158])).
% 287.49/213.79 tff(c_409250, plain, (![Y_8963:$int]: (u1(0, Y_8963)=Y_8963 | ~$less(0, 1) | $less(0, $sum($uminus(1), 1)))), inference(demodulation, [status(thm), theory('equality')], [c_196, c_397106, c_409119])).
% 287.49/213.79 tff(c_409252, plain, (![Y_8963:$int]: (u1(0, Y_8963)=Y_8963)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_409250])).
% 287.49/213.79 tff(c_397159, plain, (![B_8268:$int]: ($product(1, B_8268)=B_8268)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_396986])).
% 287.49/213.79 tff(c_205, plain, (![X_105:$int, N_44:$int, M_43:$int]: ($product(X_105, N_44)=$sum(N_44, $product(M_43, N_44)) | X_105!=$sum(1, M_43))), inference(cnfTransformation, [status(thm)], [f_1060])).
% 287.49/213.79 tff(c_397301, plain, (![B_8268:$int]: ($product($sum(1, 1), B_8268)=$sum(B_8268, B_8268))), inference(superposition, [status(thm), theory('equality')], [c_397159, c_205])).
% 287.49/213.79 tff(c_397303, plain, (![B_8268:$int]: ($product(2, B_8268)=$product(2, B_8268))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_397301])).
% 287.49/213.79 tff(c_408236, plain, (![A_8890:$int, Y_8891:$int, X_8892:$int]: (u1(A_8890, Y_8891)=$product(A_8890, $product(A_8890, u1(X_8892, Y_8891))) | X_8892!=$sum($uminus(1), A_8890) | ~$less(0, A_8890))), inference(superposition, [status(thm), theory('equality')], [c_203, c_394888])).
% 287.49/213.79 tff(c_408471, plain, (![Y_8891:$int]: ($product(2, $product(2, u1($sum($uminus(1), 2), Y_8891)))=u1(2, Y_8891) | ~$less(0, 2))), inference(superposition, [status(thm), theory('equality')], [c_397303, c_408236])).
% 287.49/213.79 tff(c_408843, plain, (![Y_8891:$int]: ($product(2, $product(2, u1($sum($uminus(1), 2), Y_8891)))=u1(2, Y_8891) | ~$less(0, 2))), inference(demodulation, [status(thm), theory('equality')], [c_397303, c_408471])).
% 287.49/213.79 tff(c_408845, plain, (![Y_8891:$int]: (u1(2, Y_8891)=$product(4, u1(1, Y_8891)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_408843])).
% 287.49/213.79 tff(c_408943, plain, (![Y_8891:$int]: (u1(2, Y_8891)=$product(4, u1(0, Y_8891)))), inference(demodulation, [status(thm), theory('equality')], [c_397158, c_408845])).
% 287.49/213.79 tff(c_409336, plain, (![Y_8891:$int]: (u1(2, Y_8891)=$product(4, Y_8891))), inference(demodulation, [status(thm), theory('equality')], [c_409252, c_408943])).
% 287.49/213.79 tff(c_397037, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$uminus(N_44) | $sum(1, M_43)!=$uminus(1))), inference(superposition, [status(thm), theory('equality')], [c_205, c_396933])).
% 287.49/213.79 tff(c_399047, plain, (![N_8383:$int]: ($product($uminus(2), N_8383)=$product($uminus(2), N_8383))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_397037])).
% 287.49/213.79 tff(c_399162, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(2), N_44) | $sum(1, M_43)!=$uminus(2))), inference(superposition, [status(thm), theory('equality')], [c_205, c_399047])).
% 287.49/213.79 tff(c_404783, plain, (![N_8626:$int]: ($product($uminus(3), N_8626)=$product($uminus(3), N_8626))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_399162])).
% 287.49/213.79 tff(c_404844, plain, (![A_57:$int, N_8626:$int]: ($product(A_57, N_8626)=$uminus($product($uminus(3), N_8626)) | $uminus(A_57)!=$uminus(3))), inference(superposition, [status(thm), theory('equality')], [c_404783, c_200])).
% 287.49/213.79 tff(c_404998, plain, (![N_8626:$int]: ($product(3, N_8626)=$product(3, N_8626))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_404844])).
% 287.49/213.79 tff(c_405141, plain, (![N_8649:$int]: ($product(3, N_8649)=$product(3, N_8649))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_404844])).
% 287.49/213.79 tff(c_394886, plain, (![X_7737:$int, Y_7738:$int, X_7739:$int]: (u1(X_7737, Y_7738)=$product(X_7737, $product(u1(X_7739, Y_7738), X_7737)) | X_7739!=$sum($uminus(1), X_7737) | ~$less(0, X_7737))), inference(demodulation, [status(thm), theory('equality')], [c_203, c_390190])).
% 287.49/213.79 tff(c_405175, plain, (![Y_7738:$int]: ($product(3, $product(u1($sum($uminus(1), 3), Y_7738), 3))=u1(3, Y_7738) | ~$less(0, 3))), inference(superposition, [status(thm), theory('equality')], [c_405141, c_394886])).
% 287.49/213.79 tff(c_405325, plain, (![Y_7738:$int]: ($product(3, $product(3, u1($sum($uminus(1), 3), Y_7738)))=u1(3, Y_7738) | ~$less(0, 3))), inference(demodulation, [status(thm), theory('equality')], [c_404998, c_203, c_405175])).
% 287.49/213.79 tff(c_405327, plain, (![Y_7738:$int]: (u1(3, Y_7738)=$product(9, u1(2, Y_7738)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_405325])).
% 287.49/213.79 tff(c_410297, plain, (![Y_7738:$int]: (u1(3, Y_7738)=$product(9, $product(4, Y_7738)))), inference(demodulation, [status(thm), theory('equality')], [c_409336, c_405327])).
% 287.49/213.79 tff(c_410299, plain, (![Y_7738:$int]: (u1(3, Y_7738)=$product(36, Y_7738))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_410297])).
% 287.49/213.79 tff(c_404820, plain, (![N_8626:$int, M_43:$int]: ($sum(N_8626, $product(M_43, N_8626))=$product($uminus(3), N_8626) | $sum(1, M_43)!=$uminus(3))), inference(superposition, [status(thm), theory('equality')], [c_404783, c_205])).
% 287.49/213.79 tff(c_406957, plain, (![N_8795:$int]: ($product($uminus(4), N_8795)=$product($uminus(4), N_8795))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_404820])).
% 287.49/213.79 tff(c_407026, plain, (![A_57:$int, N_8795:$int]: ($product(A_57, N_8795)=$uminus($product($uminus(4), N_8795)) | $uminus(A_57)!=$uminus(4))), inference(superposition, [status(thm), theory('equality')], [c_406957, c_200])).
% 287.49/213.79 tff(c_407196, plain, (![N_8795:$int]: ($product(4, N_8795)=$product(4, N_8795))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_407026])).
% 287.49/213.79 tff(c_408356, plain, (![Y_8891:$int]: ($product(4, $product(4, u1($sum($uminus(1), 4), Y_8891)))=u1(4, Y_8891) | ~$less(0, 4))), inference(superposition, [status(thm), theory('equality')], [c_407196, c_408236])).
% 287.49/213.79 tff(c_408742, plain, (![Y_8891:$int]: ($product(4, $product(4, u1($sum($uminus(1), 4), Y_8891)))=u1(4, Y_8891) | ~$less(0, 4))), inference(demodulation, [status(thm), theory('equality')], [c_407196, c_408356])).
% 287.49/213.79 tff(c_408744, plain, (![Y_8891:$int]: (u1(4, Y_8891)=$product(16, u1(3, Y_8891)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_408742])).
% 287.49/213.79 tff(c_443290, plain, (![Y_8891:$int]: (u1(4, Y_8891)=$product(16, $product(36, Y_8891)))), inference(demodulation, [status(thm), theory('equality')], [c_410299, c_408744])).
% 287.49/213.79 tff(c_443292, plain, (![Y_8891:$int]: (u1(4, Y_8891)=$product(576, Y_8891))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_443290])).
% 287.49/213.79 tff(c_407114, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(4), N_44) | $sum(1, M_43)!=$uminus(4))), inference(superposition, [status(thm), theory('equality')], [c_205, c_406957])).
% 287.49/213.79 tff(c_417277, plain, (![N_9644:$int]: ($product($uminus(5), N_9644)=$product($uminus(5), N_9644))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_407114])).
% 287.49/213.79 tff(c_417623, plain, (![B_58:$int]: ($uminus($product($uminus($uminus(5)), B_58))=$product($uminus(5), B_58))), inference(superposition, [status(thm), theory('equality')], [c_200, c_417277])).
% 287.49/213.79 tff(c_417625, plain, (![B_58:$int]: ($product(5, B_58)=$product(5, B_58))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_417623])).
% 287.49/213.79 tff(c_417778, plain, (![B_9681:$int]: ($product(5, B_9681)=$product(5, B_9681))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_417623])).
% 287.49/213.79 tff(c_395106, plain, (![A_48:$int, Y_8161:$int, X_8162:$int]: (u1(A_48, Y_8161)=$product(A_48, $product(A_48, u1(X_8162, Y_8161))) | X_8162!=$sum($uminus(1), A_48) | ~$less(0, A_48))), inference(superposition, [status(thm), theory('equality')], [c_203, c_394888])).
% 287.49/213.79 tff(c_417793, plain, (![Y_8161:$int]: ($product(5, $product(5, u1($sum($uminus(1), 5), Y_8161)))=u1(5, Y_8161) | ~$less(0, 5))), inference(superposition, [status(thm), theory('equality')], [c_417778, c_395106])).
% 287.49/213.79 tff(c_417997, plain, (![Y_8161:$int]: ($product(5, $product(5, u1($sum($uminus(1), 5), Y_8161)))=u1(5, Y_8161) | ~$less(0, 5))), inference(demodulation, [status(thm), theory('equality')], [c_417625, c_417793])).
% 287.49/213.79 tff(c_417999, plain, (![Y_8161:$int]: (u1(5, Y_8161)=$product(25, u1(4, Y_8161)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_417997])).
% 287.49/213.79 tff(c_444388, plain, (![Y_8161:$int]: (u1(5, Y_8161)=$product(25, $product(576, Y_8161)))), inference(demodulation, [status(thm), theory('equality')], [c_443292, c_417999])).
% 287.49/213.79 tff(c_444390, plain, (![Y_8161:$int]: (u1(5, Y_8161)=$product(14400, Y_8161))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_444388])).
% 287.49/213.79 tff(c_417462, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(5), N_44) | $sum(1, M_43)!=$uminus(5))), inference(superposition, [status(thm), theory('equality')], [c_205, c_417277])).
% 287.49/213.79 tff(c_422604, plain, (![N_10115:$int]: ($product($uminus(6), N_10115)=$product($uminus(6), N_10115))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_417462])).
% 287.49/213.79 tff(c_422701, plain, (![A_57:$int, N_10115:$int]: ($product(A_57, N_10115)=$uminus($product($uminus(6), N_10115)) | $uminus(A_57)!=$uminus(6))), inference(superposition, [status(thm), theory('equality')], [c_422604, c_200])).
% 287.49/213.79 tff(c_422918, plain, (![N_10115:$int]: ($product(6, N_10115)=$product(6, N_10115))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_422701])).
% 287.49/213.79 tff(c_423988, plain, (![N_10216:$int]: ($product(6, N_10216)=$product(6, N_10216))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_422701])).
% 287.49/213.79 tff(c_424181, plain, (![Y_7738:$int]: ($product(6, $product(u1($sum($uminus(1), 6), Y_7738), 6))=u1(6, Y_7738) | ~$less(0, 6))), inference(superposition, [status(thm), theory('equality')], [c_394886, c_423988])).
% 287.49/213.79 tff(c_424366, plain, (![Y_7738:$int]: ($product(6, $product(6, u1($sum($uminus(1), 6), Y_7738)))=u1(6, Y_7738) | ~$less(0, 6))), inference(demodulation, [status(thm), theory('equality')], [c_422918, c_203, c_424181])).
% 287.54/213.79 tff(c_424368, plain, (![Y_7738:$int]: (u1(6, Y_7738)=$product(36, u1(5, Y_7738)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_424366])).
% 287.54/213.79 tff(c_444883, plain, (![Y_7738:$int]: (u1(6, Y_7738)=$product(36, $product(14400, Y_7738)))), inference(demodulation, [status(thm), theory('equality')], [c_444390, c_424368])).
% 287.54/213.79 tff(c_444885, plain, (![Y_7738:$int]: (u1(6, Y_7738)=$product(518400, Y_7738))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_444883])).
% 287.54/213.79 tff(c_422812, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(6), N_44) | $sum(1, M_43)!=$uminus(6))), inference(superposition, [status(thm), theory('equality')], [c_205, c_422604])).
% 287.54/213.79 tff(c_425698, plain, (![N_10266:$int]: ($product($uminus(7), N_10266)=$product($uminus(7), N_10266))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_422812])).
% 287.54/213.79 tff(c_425803, plain, (![A_57:$int, N_10266:$int]: ($product(A_57, N_10266)=$uminus($product($uminus(7), N_10266)) | $uminus(A_57)!=$uminus(7))), inference(superposition, [status(thm), theory('equality')], [c_425698, c_200])).
% 287.54/213.79 tff(c_426028, plain, (![N_10266:$int]: ($product(7, N_10266)=$product(7, N_10266))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_425803])).
% 287.54/213.79 tff(c_426235, plain, (![N_10294:$int]: ($product(7, N_10294)=$product(7, N_10294))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_425803])).
% 287.54/213.79 tff(c_426436, plain, (![Y_7738:$int]: ($product(7, $product(u1($sum($uminus(1), 7), Y_7738), 7))=u1(7, Y_7738) | ~$less(0, 7))), inference(superposition, [status(thm), theory('equality')], [c_394886, c_426235])).
% 287.54/213.79 tff(c_426620, plain, (![Y_7738:$int]: ($product(7, $product(7, u1($sum($uminus(1), 7), Y_7738)))=u1(7, Y_7738) | ~$less(0, 7))), inference(demodulation, [status(thm), theory('equality')], [c_426028, c_203, c_426436])).
% 287.54/213.79 tff(c_426622, plain, (![Y_7738:$int]: (u1(7, Y_7738)=$product(49, u1(6, Y_7738)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_426620])).
% 287.54/213.79 tff(c_445152, plain, (![Y_7738:$int]: (u1(7, Y_7738)=$product(49, $product(518400, Y_7738)))), inference(demodulation, [status(thm), theory('equality')], [c_444885, c_426622])).
% 287.54/213.79 tff(c_445154, plain, (![Y_7738:$int]: (u1(7, Y_7738)=$product(25401600, Y_7738))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_445152])).
% 287.54/213.79 tff(c_425918, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(7), N_44) | $sum(1, M_43)!=$uminus(7))), inference(superposition, [status(thm), theory('equality')], [c_205, c_425698])).
% 287.54/213.79 tff(c_428296, plain, (![N_10355:$int]: ($product($uminus(8), N_10355)=$product($uminus(8), N_10355))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_425918])).
% 287.54/213.79 tff(c_428413, plain, (![A_57:$int, N_10355:$int]: ($product(A_57, N_10355)=$uminus($product($uminus(8), N_10355)) | $uminus(A_57)!=$uminus(8))), inference(superposition, [status(thm), theory('equality')], [c_428296, c_200])).
% 287.54/213.79 tff(c_428660, plain, (![N_10355:$int]: ($product(8, N_10355)=$product(8, N_10355))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_428413])).
% 287.54/213.79 tff(c_428745, plain, (![N_10382:$int]: ($product(8, N_10382)=$product(8, N_10382))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_428413])).
% 287.54/213.79 tff(c_428970, plain, (![Y_7738:$int]: ($product(8, $product(u1($sum($uminus(1), 8), Y_7738), 8))=u1(8, Y_7738) | ~$less(0, 8))), inference(superposition, [status(thm), theory('equality')], [c_394886, c_428745])).
% 287.54/213.79 tff(c_429171, plain, (![Y_7738:$int]: ($product(8, $product(8, u1($sum($uminus(1), 8), Y_7738)))=u1(8, Y_7738) | ~$less(0, 8))), inference(demodulation, [status(thm), theory('equality')], [c_428660, c_203, c_428970])).
% 287.54/213.79 tff(c_429173, plain, (![Y_7738:$int]: (u1(8, Y_7738)=$product(64, u1(7, Y_7738)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_429171])).
% 287.54/213.79 tff(c_445629, plain, (![Y_7738:$int]: (u1(8, Y_7738)=$product(64, $product(25401600, Y_7738)))), inference(demodulation, [status(thm), theory('equality')], [c_445154, c_429173])).
% 287.54/213.79 tff(c_445631, plain, (![Y_7738:$int]: (u1(8, Y_7738)=$product(1625702400, Y_7738))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_445629])).
% 287.54/213.79 tff(c_428540, plain, (![N_44:$int, M_43:$int]: ($sum(N_44, $product(M_43, N_44))=$product($uminus(8), N_44) | $sum(1, M_43)!=$uminus(8))), inference(superposition, [status(thm), theory('equality')], [c_205, c_428296])).
% 287.54/213.79 tff(c_434997, plain, (![N_10796:$int]: ($product($uminus(9), N_10796)=$product($uminus(9), N_10796))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_428540])).
% 287.54/213.79 tff(c_435469, plain, (![B_58:$int]: ($uminus($product($uminus($uminus(9)), B_58))=$product($uminus(9), B_58))), inference(superposition, [status(thm), theory('equality')], [c_200, c_434997])).
% 287.54/213.79 tff(c_435471, plain, (![B_58:$int]: ($product(9, B_58)=$product(9, B_58))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_435469])).
% 287.54/213.79 tff(c_435758, plain, (![B_10833:$int]: ($product(9, B_10833)=$product(9, B_10833))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_435469])).
% 287.54/213.79 tff(c_436005, plain, (![Y_7738:$int]: ($product(9, $product(u1($sum($uminus(1), 9), Y_7738), 9))=u1(9, Y_7738) | ~$less(0, 9))), inference(superposition, [status(thm), theory('equality')], [c_394886, c_435758])).
% 287.54/213.79 tff(c_436211, plain, (![Y_7738:$int]: ($product(9, $product(9, u1($sum($uminus(1), 9), Y_7738)))=u1(9, Y_7738) | ~$less(0, 9))), inference(demodulation, [status(thm), theory('equality')], [c_435471, c_203, c_436005])).
% 287.54/213.79 tff(c_436213, plain, (![Y_7738:$int]: (u1(9, Y_7738)=$product(81, u1(8, Y_7738)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_436211])).
% 287.54/213.79 tff(c_446120, plain, (![Y_7738:$int]: (u1(9, Y_7738)=$product(81, $product(1625702400, Y_7738)))), inference(demodulation, [status(thm), theory('equality')], [c_445631, c_436213])).
% 287.54/213.79 tff(c_446122, plain, (![Y_7738:$int]: (u1(9, Y_7738)=$product($uminus(1462091776), Y_7738))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_446120])).
% 287.54/213.79 tff(c_436553, plain, (![B_10869:$int]: ($product(B_10869, 9)=$product(9, B_10869))), inference(superposition, [status(thm), theory('equality')], [c_435758, c_203])).
% 287.54/213.79 tff(c_194, plain, (![A_67:$int, B_68:$int]: ($less(0, $product(A_67, B_68)) | ~$less(0, A_67) | ~$less(0, B_68))), inference(cnfTransformation, [status(thm)], [f_1088])).
% 287.54/213.79 tff(c_395073, plain, (![X_8160:$int, Y_8161:$int, X_8162:$int]: ($less(0, u1(X_8160, Y_8161)) | ~$less(0, X_8160) | ~$less(0, $product(u1(X_8162, Y_8161), X_8160)) | X_8162!=$sum($uminus(1), X_8160) | ~$less(0, X_8160))), inference(superposition, [status(thm), theory('equality')], [c_394888, c_194])).
% 287.54/213.79 tff(c_436851, plain, (![Y_8161:$int]: ($less(0, u1(9, Y_8161)) | ~$less(0, $product(9, u1($sum($uminus(1), 9), Y_8161))) | ~$less(0, 9))), inference(superposition, [status(thm), theory('equality')], [c_436553, c_395073])).
% 287.54/213.79 tff(c_436853, plain, (![Y_8161:$int]: ($less(0, u1(9, Y_8161)) | ~$less(0, u1(8, Y_8161)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_436851])).
% 287.54/213.79 tff(c_519012, plain, (![Y_8161:$int]: ($less(0, $product($uminus(1462091776), Y_8161)) | ~$less(0, $product(1625702400, Y_8161)))), inference(demodulation, [status(thm), theory('equality')], [c_445631, c_446122, c_436853])).
% 287.54/213.79 tff(c_519014, plain, (![Y_8161:$int]: ($less(Y_8161, 0) | ~$less(0, Y_8161))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_519012])).
% 287.54/213.79 tff(c_519016, plain, $false, inference(quantifierElimination, [status(thm), theory('LIA')], [c_519014])).
% 287.54/213.79 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------