%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW605_2 : TPTP v9.0.0. Released v6.1.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 : n026.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:53:03 PM UTC 2025
% Result : Theorem 201.26s 151.86s
% Output : CNFRefutation 201.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 9
% Syntax : Number of formulae : 101 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 214 ( 52 equ)
% Maximal formula atoms : 38 ( 2 avg)
% Number of connectives : 179 ( 66 ~; 70 |; 24 &)
% ( 4 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 287 ( 81 atm; 78 fun; 119 num; 9 var)
% Number of types : 14 ( 12 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 5 usr; 1 prp; 0-5 aty)
% Number of functors : 440 ( 435 usr; 380 con; 0-5 aty)
% Number of variables : 90 ( 90 !; 0 ?; 90 :)
% Comments :
%------------------------------------------------------------------------------
%$ good_data1 > in_data1 > mem > good_hash1 > sort1 > set > match_option1 > match_list1 > tuple21 > set2 > mk_t1 > match_bool1 > get > tuple2_proj_21 > tuple2_proj_11 > mk_array1 > make1 > get2 > const > cons > view > tuple2 > some_proj_11 > some > size1 > mod1 > map > length1 > elts > div1 > data > cons_proj_21 > cons_proj_11 > bucket1 > #nlpp > witness1 > tb2t8 > tb2t7 > tb2t6 > tb2t5 > tb2t4 > tb2t3 > tb2t2 > tb2t1 > tb2t > t2tb8 > t2tb7 > t2tb6 > t2tb5 > t2tb4 > t2tb3 > t2tb2 > t2tb1 > t2tb > t > option > none > nil > list > hash1 > array > abs1 > tuple03 > tuple0 > true1 > real > qtmark > key > int > false1 > bool > a > #skF_2 > #skF_5 > #skF_7 > #skF_11 > #skF_13 > #skF_9 > #skF_15 > #skF_1 > #skF_14 > #skF_12 > #skF_8 > #skF_4
%Foreground sorts:
tff(option_a1,type,
option_a1: $tType ).
tff(array_lplist_lpkeycm_a1rprp,type,
array_lplist_lpkeycm_a1rprp: $tType ).
tff(lpkeycm_a1rp,type,
lpkeycm_a1rp: $tType ).
tff(key1,type,
key1: $tType ).
tff(tuple02,type,
tuple02: $tType ).
tff(bool1,type,
bool1: $tType ).
tff(list_lpkeycm_a1rp,type,
list_lpkeycm_a1rp: $tType ).
tff(map_key_lpoption_a1rp,type,
map_key_lpoption_a1rp: $tType ).
tff(a1,type,
a1: $tType ).
tff(map_int_lplist_lpkeycm_a1rprp,type,
map_int_lplist_lpkeycm_a1rprp: $tType ).
tff(ty,type,
ty: $tType ).
tff(uni,type,
uni: $tType ).
%Background operators:
tff('#skE_279',type,
'#skE_279': $int ).
tff('#skE_217',type,
'#skE_217': $int ).
tff('#skE_46',type,
'#skE_46': $int ).
tff('#skE_269',type,
'#skE_269': $int ).
tff('#skE_120',type,
'#skE_120': $int ).
tff('#skE_331',type,
'#skE_331': $int ).
tff('#skE_251',type,
'#skE_251': $int ).
tff('#skE_203',type,
'#skE_203': $int ).
tff('#skE_189',type,
'#skE_189': $int ).
tff('#skE_324',type,
'#skE_324': $int ).
tff('#skE_240',type,
'#skE_240': $int ).
tff('#skE_208',type,
'#skE_208': $int ).
tff('#skE_226',type,
'#skE_226': $int ).
tff('#skE_74',type,
'#skE_74': $int ).
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_248',type,
'#skE_248': $int ).
tff('#skE_230',type,
'#skE_230': $int ).
tff('#skE_90',type,
'#skE_90': $int ).
tff('#skE_231',type,
'#skE_231': $int ).
tff('#skE_105',type,
'#skE_105': $int ).
tff('#skE_213',type,
'#skE_213': $int ).
tff('#skE_263',type,
'#skE_263': $int ).
tff('#skE_260',type,
'#skE_260': $int ).
tff('#skE_187',type,
'#skE_187': $int ).
tff('#skE_88',type,
'#skE_88': $int ).
tff('#skE_121',type,
'#skE_121': $int ).
tff('#skE_135',type,
'#skE_135': $int ).
tff('#skE_158',type,
'#skE_158': $int ).
tff('#skE_254',type,
'#skE_254': $int ).
tff('#skE_95',type,
'#skE_95': $int ).
tff('#skE_21',type,
'#skE_21': $int ).
tff('#skE_179',type,
'#skE_179': $int ).
tff('#skE_62',type,
'#skE_62': $int ).
tff('#skE_146',type,
'#skE_146': $int ).
tff('#skE_30',type,
'#skE_30': $int ).
tff('#skE_128',type,
'#skE_128': $int ).
tff('#skE_278',type,
'#skE_278': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_185',type,
'#skE_185': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_312',type,
'#skE_312': $int ).
tff('#skE_52',type,
'#skE_52': $int ).
tff('#skE_28',type,
'#skE_28': $int ).
tff('#skE_262',type,
'#skE_262': $int ).
tff('#skE_290',type,
'#skE_290': $int ).
tff('#skE_109',type,
'#skE_109': $int ).
tff('#skE_48',type,
'#skE_48': $int ).
tff('#skE_155',type,
'#skE_155': $int ).
tff('#skE_23',type,
'#skE_23': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_41',type,
'#skE_41': $int ).
tff('#skE_156',type,
'#skE_156': $int ).
tff('#skE_261',type,
'#skE_261': $int ).
tff('#skE_43',type,
'#skE_43': $int ).
tff('#skE_162',type,
'#skE_162': $int ).
tff('#skE_286',type,
'#skE_286': $int ).
tff('#skE_37',type,
'#skE_37': $int ).
tff('#skE_73',type,
'#skE_73': $int ).
tff('#skE_80',type,
'#skE_80': $int ).
tff('#skE_188',type,
'#skE_188': $int ).
tff('#skE_297',type,
'#skE_297': $int ).
tff('#skE_283',type,
'#skE_283': $int ).
tff('#skE_237',type,
'#skE_237': $int ).
tff('#skE_222',type,
'#skE_222': $int ).
tff('#skE_333',type,
'#skE_333': $int ).
tff('#skE_271',type,
'#skE_271': $int ).
tff('#skE_180',type,
'#skE_180': $int ).
tff('#skE_317',type,
'#skE_317': $int ).
tff('#skE_174',type,
'#skE_174': $int ).
tff('#skE_228',type,
'#skE_228': $int ).
tff('#skE_320',type,
'#skE_320': $int ).
tff('#skE_239',type,
'#skE_239': $int ).
tff('#skE_173',type,
'#skE_173': $int ).
tff('#skE_282',type,
'#skE_282': $int ).
tff('#skE_144',type,
'#skE_144': $int ).
tff('#skE_330',type,
'#skE_330': $int ).
tff('#skE_211',type,
'#skE_211': $int ).
tff('#skE_272',type,
'#skE_272': $int ).
tff('#skE_352',type,
'#skE_352': $int ).
tff('#skE_85',type,
'#skE_85': $int ).
tff('#skE_101',type,
'#skE_101': $int ).
tff('#skE_154',type,
'#skE_154': $int ).
tff('#skE_210',type,
'#skE_210': $int ).
tff('#skE_267',type,
'#skE_267': $int ).
tff('#skE_84',type,
'#skE_84': $int ).
tff('#skE_216',type,
'#skE_216': $int ).
tff('#skE_310',type,
'#skE_310': $int ).
tff('#skE_42',type,
'#skE_42': $int ).
tff('#skE_143',type,
'#skE_143': $int ).
tff('#skE_57',type,
'#skE_57': $int ).
tff('#skE_86',type,
'#skE_86': $int ).
tff('#skE_133',type,
'#skE_133': $int ).
tff('#skE_142',type,
'#skE_142': $int ).
tff('#skE_245',type,
'#skE_245': $int ).
tff('#skE_201',type,
'#skE_201': $int ).
tff('#skE_111',type,
'#skE_111': $int ).
tff('#skE_215',type,
'#skE_215': $int ).
tff('#skE_200',type,
'#skE_200': $int ).
tff('#skE_192',type,
'#skE_192': $int ).
tff('#skF_6',type,
'#skF_6': $int ).
tff('#skE_63',type,
'#skE_63': $int ).
tff('#skE_102',type,
'#skE_102': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_170',type,
'#skE_170': $int ).
tff('#skE_258',type,
'#skE_258': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_33',type,
'#skE_33': $int ).
tff('#skE_209',type,
'#skE_209': $int ).
tff('#skE_97',type,
'#skE_97': $int ).
tff('#skE_20',type,
'#skE_20': $int ).
tff('#skE_78',type,
'#skE_78': $int ).
tff('#skE_159',type,
'#skE_159': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_252',type,
'#skE_252': $int ).
tff('#skE_116',type,
'#skE_116': $int ).
tff('#skE_307',type,
'#skE_307': $int ).
tff('#skE_196',type,
'#skE_196': $int ).
tff('#skE_305',type,
'#skE_305': $int ).
tff('#skE_273',type,
'#skE_273': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_130',type,
'#skE_130': $int ).
tff('#skE_287',type,
'#skE_287': $int ).
tff('#skE_301',type,
'#skE_301': $int ).
tff('#skE_118',type,
'#skE_118': $int ).
tff('#skE_241',type,
'#skE_241': $int ).
tff('#skE_26',type,
'#skE_26': $int ).
tff('#skE_323',type,
'#skE_323': $int ).
tff('#skE_296',type,
'#skE_296': $int ).
tff('#skE_32',type,
'#skE_32': $int ).
tff('#skE_92',type,
'#skE_92': $int ).
tff('#skE_311',type,
'#skE_311': $int ).
tff('#skE_304',type,
'#skE_304': $int ).
tff('#skE_199',type,
'#skE_199': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_338',type,
'#skE_338': $int ).
tff('#skE_337',type,
'#skE_337': $int ).
tff('#skE_184',type,
'#skE_184': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_114',type,
'#skE_114': $int ).
tff('#skE_266',type,
'#skE_266': $int ).
tff('#skE_345',type,
'#skE_345': $int ).
tff('#skE_212',type,
'#skE_212': $int ).
tff('#skE_332',type,
'#skE_332': $int ).
tff('#skE_191',type,
'#skE_191': $int ).
tff('#skE_349',type,
'#skE_349': $int ).
tff('#skE_255',type,
'#skE_255': $int ).
tff('#skE_236',type,
'#skE_236': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_138',type,
'#skE_138': $int ).
tff('#skE_309',type,
'#skE_309': $int ).
tff('#skE_110',type,
'#skE_110': $int ).
tff('#skE_288',type,
'#skE_288': $int ).
tff('#skE_38',type,
'#skE_38': $int ).
tff('#skE_291',type,
'#skE_291': $int ).
tff('#skE_268',type,
'#skE_268': $int ).
tff('#skE_315',type,
'#skE_315': $int ).
tff('#skE_313',type,
'#skE_313': $int ).
tff('#skE_31',type,
'#skE_31': $int ).
tff('#skE_122',type,
'#skE_122': $int ).
tff('#skE_247',type,
'#skE_247': $int ).
tff('#skE_302',type,
'#skE_302': $int ).
tff('#skE_303',type,
'#skE_303': $int ).
tff('#skE_242',type,
'#skE_242': $int ).
tff('#skE_308',type,
'#skE_308': $int ).
tff('#skE_306',type,
'#skE_306': $int ).
tff('#skE_157',type,
'#skE_157': $int ).
tff('#skE_51',type,
'#skE_51': $int ).
tff('#skE_336',type,
'#skE_336': $int ).
tff('#skE_249',type,
'#skE_249': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_151',type,
'#skE_151': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_220',type,
'#skE_220': $int ).
tff('#skE_165',type,
'#skE_165': $int ).
tff('#skE_344',type,
'#skE_344': $int ).
tff('#skE_294',type,
'#skE_294': $int ).
tff('#skE_36',type,
'#skE_36': $int ).
tff('#skE_69',type,
'#skE_69': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_246',type,
'#skE_246': $int ).
tff('#skE_149',type,
'#skE_149': $int ).
tff('#skE_54',type,
'#skE_54': $int ).
tff('#skE_197',type,
'#skE_197': $int ).
tff('#skE_335',type,
'#skE_335': $int ).
tff('#skE_253',type,
'#skE_253': $int ).
tff('#skE_250',type,
'#skE_250': $int ).
tff('#skE_164',type,
'#skE_164': $int ).
tff('#skE_76',type,
'#skE_76': $int ).
tff('#skE_70',type,
'#skE_70': $int ).
tff('#skE_64',type,
'#skE_64': $int ).
tff('#skE_292',type,
'#skE_292': $int ).
tff('#skE_82',type,
'#skE_82': $int ).
tff('#skE_103',type,
'#skE_103': $int ).
tff('#skE_300',type,
'#skE_300': $int ).
tff('#skE_60',type,
'#skE_60': $int ).
tff('#skE_295',type,
'#skE_295': $int ).
tff('#skE_50',type,
'#skE_50': $int ).
tff('#skE_221',type,
'#skE_221': $int ).
tff('#skE_104',type,
'#skE_104': $int ).
tff('#skE_150',type,
'#skE_150': $int ).
tff('#skE_280',type,
'#skE_280': $int ).
tff('#skE_137',type,
'#skE_137': $int ).
tff('#skF_10',type,
'#skF_10': $int ).
tff('#skF_3',type,
'#skF_3': $int ).
tff('#skE_113',type,
'#skE_113': $int ).
tff('#skE_190',type,
'#skE_190': $int ).
tff('#skE_329',type,
'#skE_329': $int ).
tff('#skE_129',type,
'#skE_129': $int ).
tff('#skE_298',type,
'#skE_298': $int ).
tff('#skE_276',type,
'#skE_276': $int ).
tff('#skE_22',type,
'#skE_22': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_183',type,
'#skE_183': $int ).
tff('#skE_227',type,
'#skE_227': $int ).
tff('#skE_328',type,
'#skE_328': $int ).
tff('#skE_225',type,
'#skE_225': $int ).
tff('#skE_55',type,
'#skE_55': $int ).
tff('#skE_354',type,
'#skE_354': $int ).
tff('#skE_123',type,
'#skE_123': $int ).
tff('#skE_348',type,
'#skE_348': $int ).
tff('#skE_204',type,
'#skE_204': $int ).
tff('#skE_339',type,
'#skE_339': $int ).
tff('#skE_326',type,
'#skE_326': $int ).
tff('#skE_77',type,
'#skE_77': $int ).
tff('#skE_163',type,
'#skE_163': $int ).
tff('#skE_257',type,
'#skE_257': $int ).
tff('#skE_195',type,
'#skE_195': $int ).
tff('#skE_79',type,
'#skE_79': $int ).
tff('#skE_161',type,
'#skE_161': $int ).
tff('#skE_229',type,
'#skE_229': $int ).
tff('#skE_127',type,
'#skE_127': $int ).
tff('#skE_181',type,
'#skE_181': $int ).
tff('#skE_284',type,
'#skE_284': $int ).
tff('#skE_124',type,
'#skE_124': $int ).
tff('#skE_275',type,
'#skE_275': $int ).
tff('#skE_171',type,
'#skE_171': $int ).
tff('#skE_346',type,
'#skE_346': $int ).
tff('#skE_71',type,
'#skE_71': $int ).
tff('#skE_198',type,
'#skE_198': $int ).
tff('#skE_350',type,
'#skE_350': $int ).
tff('#skE_289',type,
'#skE_289': $int ).
tff('#skE_134',type,
'#skE_134': $int ).
tff('#skE_178',type,
'#skE_178': $int ).
tff('#skE_175',type,
'#skE_175': $int ).
tff('#skE_91',type,
'#skE_91': $int ).
tff('#skE_67',type,
'#skE_67': $int ).
tff('#skE_235',type,
'#skE_235': $int ).
tff('#skE_58',type,
'#skE_58': $int ).
tff('#skE_87',type,
'#skE_87': $int ).
tff('#skE_232',type,
'#skE_232': $int ).
tff('#skE_327',type,
'#skE_327': $int ).
tff('#skE_47',type,
'#skE_47': $int ).
tff('#skE_68',type,
'#skE_68': $int ).
tff('#skE_319',type,
'#skE_319': $int ).
tff('#skE_40',type,
'#skE_40': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_316',type,
'#skE_316': $int ).
tff('#skE_75',type,
'#skE_75': $int ).
tff('#skE_117',type,
'#skE_117': $int ).
tff('#skE_29',type,
'#skE_29': $int ).
tff('#skE_44',type,
'#skE_44': $int ).
tff('#skE_49',type,
'#skE_49': $int ).
tff('#skE_353',type,
'#skE_353': $int ).
tff('#skE_34',type,
'#skE_34': $int ).
tff('#skE_45',type,
'#skE_45': $int ).
tff('#skE_234',type,
'#skE_234': $int ).
tff('#skE_169',type,
'#skE_169': $int ).
tff('#skE_96',type,
'#skE_96': $int ).
tff('#skE_168',type,
'#skE_168': $int ).
tff('#skE_223',type,
'#skE_223': $int ).
tff('#skE_27',type,
'#skE_27': $int ).
tff('#skE_147',type,
'#skE_147': $int ).
tff('#skE_115',type,
'#skE_115': $int ).
tff('#skE_233',type,
'#skE_233': $int ).
tff('#skE_176',type,
'#skE_176': $int ).
tff('#skE_100',type,
'#skE_100': $int ).
tff('#skE_152',type,
'#skE_152': $int ).
tff('#skE_243',type,
'#skE_243': $int ).
tff('#skE_342',type,
'#skE_342': $int ).
tff('#skE_141',type,
'#skE_141': $int ).
tff('#skE_59',type,
'#skE_59': $int ).
tff('#skE_244',type,
'#skE_244': $int ).
tff('#skE_351',type,
'#skE_351': $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_194',type,
'#skE_194': $int ).
tff('#skE_218',type,
'#skE_218': $int ).
tff('#skE_299',type,
'#skE_299': $int ).
tff('#skE_318',type,
'#skE_318': $int ).
tff('#skE_140',type,
'#skE_140': $int ).
tff('#skE_83',type,
'#skE_83': $int ).
tff('#skE_206',type,
'#skE_206': $int ).
tff('#skE_256',type,
'#skE_256': $int ).
tff('#skE_131',type,
'#skE_131': $int ).
tff('#skE_265',type,
'#skE_265': $int ).
tff('#skE_93',type,
'#skE_93': $int ).
tff('#skE_214',type,
'#skE_214': $int ).
tff('#skE_125',type,
'#skE_125': $int ).
tff('#skE_264',type,
'#skE_264': $int ).
tff('#skE_167',type,
'#skE_167': $int ).
tff('#skE_325',type,
'#skE_325': $int ).
tff('#skE_136',type,
'#skE_136': $int ).
tff('#skE_132',type,
'#skE_132': $int ).
tff('#skE_107',type,
'#skE_107': $int ).
tff('#skE_219',type,
'#skE_219': $int ).
tff('#skE_119',type,
'#skE_119': $int ).
tff('#skE_94',type,
'#skE_94': $int ).
tff('#skE_182',type,
'#skE_182': $int ).
tff('#skE_347',type,
'#skE_347': $int ).
tff('#skE_186',type,
'#skE_186': $int ).
tff('#skE_106',type,
'#skE_106': $int ).
tff('#skE_270',type,
'#skE_270': $int ).
tff('#skE_126',type,
'#skE_126': $int ).
tff('#skE_153',type,
'#skE_153': $int ).
tff('#skE_81',type,
'#skE_81': $int ).
tff('#skE_322',type,
'#skE_322': $int ).
tff('#skE_285',type,
'#skE_285': $int ).
tff('#skE_177',type,
'#skE_177': $int ).
tff('#skE_293',type,
'#skE_293': $int ).
tff('#skE_112',type,
'#skE_112': $int ).
tff('#skE_148',type,
'#skE_148': $int ).
tff('#skE_193',type,
'#skE_193': $int ).
tff('#skE_145',type,
'#skE_145': $int ).
tff('#skE_35',type,
'#skE_35': $int ).
tff('#skE_274',type,
'#skE_274': $int ).
tff('#skE_207',type,
'#skE_207': $int ).
tff('#skE_314',type,
'#skE_314': $int ).
tff('#skE_172',type,
'#skE_172': $int ).
tff('#skE_108',type,
'#skE_108': $int ).
tff('#skE_166',type,
'#skE_166': $int ).
tff('#skE_61',type,
'#skE_61': $int ).
tff('#skE_99',type,
'#skE_99': $int ).
tff('#skE_98',type,
'#skE_98': $int ).
tff('#skE_334',type,
'#skE_334': $int ).
tff('#skE_160',type,
'#skE_160': $int ).
tff('#skE_343',type,
'#skE_343': $int ).
tff('#skE_39',type,
'#skE_39': $int ).
tff('#skE_224',type,
'#skE_224': $int ).
tff('#skE_66',type,
'#skE_66': $int ).
tff('#skE_89',type,
'#skE_89': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_321',type,
'#skE_321': $int ).
tff('#skE_340',type,
'#skE_340': $int ).
tff('#skE_205',type,
'#skE_205': $int ).
tff('#skE_53',type,
'#skE_53': $int ).
tff('#skE_341',type,
'#skE_341': $int ).
tff('#skE_65',type,
'#skE_65': $int ).
tff('#skE_238',type,
'#skE_238': $int ).
tff('#skE_281',type,
'#skE_281': $int ).
tff('#skE_139',type,
'#skE_139': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
tff('#skE_259',type,
'#skE_259': $int ).
tff('#skE_202',type,
'#skE_202': $int ).
tff('#skE_72',type,
'#skE_72': $int ).
tff('#skE_277',type,
'#skE_277': $int ).
tff('#skE_56',type,
'#skE_56': $int ).
%Foreground operators:
tff(list,type,
list: ty > ty ).
tff(mod1,type,
mod1: ( $int * $int ) > $int ).
tff(bucket1,type,
bucket1: ( key1 * $int ) > $int ).
tff(length1,type,
length1: ( ty * uni ) > $int ).
tff(view,type,
view: ( ty * uni ) > uni ).
tff(cons,type,
cons: ( ty * uni * uni ) > uni ).
tff(some_proj_11,type,
some_proj_11: ( ty * uni ) > uni ).
tff('#skF_2',type,
'#skF_2': ( ty * uni * $int ) > uni ).
tff(div1,type,
div1: ( $int * $int ) > $int ).
tff(t,type,
t: ty > ty ).
tff(nil,type,
nil: ty > uni ).
tff(get2,type,
get2: ( ty * uni * $int ) > uni ).
tff('#skF_5',type,
'#skF_5': map_key_lpoption_a1rp ).
tff(true1,type,
true1: bool1 ).
tff(const,type,
const: ( ty * ty * uni ) > uni ).
tff(tuple2,type,
tuple2: ( ty * ty ) > ty ).
tff(hash1,type,
hash1: key1 > $int ).
tff(match_list1,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_7',type,
'#skF_7': list_lpkeycm_a1rp ).
tff(elts,type,
elts: ( ty * uni ) > uni ).
tff(tb2t8,type,
tb2t8: uni > lpkeycm_a1rp ).
tff(int,type,
int: ty ).
tff(false1,type,
false1: bool1 ).
tff(good_data1,type,
good_data1: ( ty * key1 * uni * uni * uni ) > $o ).
tff(tb2t,type,
tb2t: uni > $int ).
tff(t2tb7,type,
t2tb7: a1 > uni ).
tff(sort1,type,
sort1: ( ty * uni ) > $o ).
tff('#skF_11',type,
'#skF_11': map_int_lplist_lpkeycm_a1rprp ).
tff(t2tb,type,
t2tb: $int > uni ).
tff(size1,type,
size1: ( ty * uni ) > $int ).
tff(witness1,type,
witness1: ty > uni ).
tff(tuple2_proj_21,type,
tuple2_proj_21: ( ty * ty * uni ) > uni ).
tff(real,type,
real: ty ).
tff(tb2t5,type,
tb2t5: uni > array_lplist_lpkeycm_a1rprp ).
tff(t2tb4,type,
t2tb4: option_a1 > uni ).
tff(set,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(tuple21,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(mk_t1,type,
mk_t1: ( ty * $int * uni * uni ) > uni ).
tff(match_bool1,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(array,type,
array: ty > ty ).
tff(tb2t7,type,
tb2t7: uni > a1 ).
tff('#skF_13',type,
'#skF_13': a1 ).
tff(t2tb2,type,
t2tb2: map_int_lplist_lpkeycm_a1rprp > uni ).
tff(key,type,
key: ty ).
tff(make1,type,
make1: ( ty * $int * uni ) > uni ).
tff(option,type,
option: ty > ty ).
tff(none,type,
none: ty > uni ).
tff(tb2t6,type,
tb2t6: uni > list_lpkeycm_a1rp ).
tff(tuple0,type,
tuple0: ty ).
tff(qtmark,type,
qtmark: ty ).
tff(t2tb5,type,
t2tb5: array_lplist_lpkeycm_a1rprp > uni ).
tff('#skF_9',type,
'#skF_9': map_key_lpoption_a1rp ).
tff('#skF_15',type,
'#skF_15': a1 ).
tff(bool,type,
bool: ty ).
tff(get,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(t2tb6,type,
t2tb6: list_lpkeycm_a1rp > uni ).
tff(some,type,
some: ( ty * uni ) > uni ).
tff(tuple2_proj_11,type,
tuple2_proj_11: ( ty * ty * uni ) > uni ).
tff(t2tb8,type,
t2tb8: lpkeycm_a1rp > uni ).
tff('#skF_1',type,
'#skF_1': ( ty * uni * $int ) > key1 ).
tff('#skF_14',type,
'#skF_14': key1 ).
tff(good_hash1,type,
good_hash1: ( ty * uni * $int ) > $o ).
tff(tb2t2,type,
tb2t2: uni > map_int_lplist_lpkeycm_a1rprp ).
tff(a,type,
a: ty ).
tff(tuple03,type,
tuple03: tuple02 ).
tff(t2tb1,type,
t2tb1: key1 > uni ).
tff(map,type,
map: ( ty * ty ) > ty ).
tff(cons_proj_11,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(tb2t3,type,
tb2t3: uni > map_key_lpoption_a1rp ).
tff(set2,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(in_data1,type,
in_data1: ( ty * key1 * uni * uni ) > $o ).
tff(data,type,
data: ( ty * uni ) > uni ).
tff(mem,type,
mem: ( ty * uni * uni ) > $o ).
tff(tb2t4,type,
tb2t4: uni > option_a1 ).
tff('#skF_12',type,
'#skF_12': key1 ).
tff(tb2t1,type,
tb2t1: uni > key1 ).
tff(mk_array1,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(cons_proj_21,type,
cons_proj_21: ( ty * uni ) > uni ).
tff('#skF_8',type,
'#skF_8': map_int_lplist_lpkeycm_a1rprp ).
tff(t2tb3,type,
t2tb3: map_key_lpoption_a1rp > uni ).
tff(match_option1,type,
match_option1: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_4',type,
'#skF_4': map_int_lplist_lpkeycm_a1rprp ).
tff(abs1,type,
abs1: $int > $int ).
tff(f_504,negated_conjecture,
~ ! [Ha: $int,H1: map_int_lplist_lpkeycm_a1rprp,H2: map_key_lpoption_a1rp] :
( ( $less(0,Ha)
& ! [Ia: $int] :
( ( $lesseq(0,Ia)
& $less(Ia,Ha) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),Ha,t2tb2(H1)),Ia) )
& ! [K: key1,V: a1] : good_data1(a,K,t2tb7(V),t2tb3(H2),mk_array1(list(tuple2(key,a)),Ha,t2tb2(H1)))
& $lesseq(0,Ha) )
=> ( $lesseq(0,$sum($product(2,Ha),1))
=> ( $lesseq(0,$sum($product(2,Ha),1))
=> ! [Ia: $int,L: list_lpkeycm_a1rp,Ndata: map_int_lplist_lpkeycm_a1rprp,Rho: map_key_lpoption_a1rp,Rho1a: $int,Rho2: map_int_lplist_lpkeycm_a1rprp] :
( ( $less(0,Rho1a)
& ! [I1a: $int] :
( ( $lesseq(0,I1a)
& $less(I1a,Rho1a) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),Rho1a,t2tb2(Rho2)),I1a) )
& ! [K: key1,V: a1] : good_data1(a,K,t2tb7(V),t2tb3(Rho),mk_array1(list(tuple2(key,a)),Rho1a,t2tb2(Rho2)))
& $lesseq(0,Rho1a)
& $lesseq(0,$sum($product(2,Ha),1))
& ! [K: key1,V: a1] :
( mem(tuple2(key,a),tuple21(key,a,t2tb1(K),t2tb7(V)),t2tb6(L))
=> ( bucket1(K,Ha) = Ia ) )
& ! [Ja: $int] :
( ( $lesseq(0,Ja)
& $less(Ja,$sum($product(2,Ha),1)) )
=> good_hash1(a,mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata)),Ja) )
& ! [K: key1,V: a1] :
( ( $lesseq(0,bucket1(K,Ha))
& $less(bucket1(K,Ha),Ia)
& good_data1(a,K,t2tb7(V),t2tb3(Rho),mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata))) )
| ( ~ ( $lesseq(0,bucket1(K,Ha))
& $less(bucket1(K,Ha),Ia) )
& ( ( ( bucket1(K,Ha) = Ia )
& ( ( tb2t4(get(option(a),key,t2tb3(Rho),t2tb1(K))) = tb2t4(some(a,t2tb7(V))) )
<=> ( mem(tuple2(key,a),tuple21(key,a,t2tb1(K),t2tb7(V)),t2tb6(L))
| in_data1(a,K,t2tb7(V),mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata))) ) ) )
| ( ( bucket1(K,Ha) != Ia )
& ~ in_data1(a,K,t2tb7(V),mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata))) ) ) ) ) )
=> ( ( L = tb2t6(nil(tuple2(key,a))) )
=> ! [K: key1,V: a1] :
( ( ( $lesseq(0,bucket1(K,Ha))
& $lesseq(bucket1(K,Ha),Ia) )
=> good_data1(a,K,t2tb7(V),t2tb3(Rho),mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata))) )
& ( ~ ( $lesseq(0,bucket1(K,Ha))
& $lesseq(bucket1(K,Ha),Ia) )
=> ~ in_data1(a,K,t2tb7(V),mk_array1(list(tuple2(key,a)),$sum($product(2,Ha),1),t2tb2(Ndata))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_resize) ).
tff(f_295,axiom,
! [Na: $int] :
( $less(0,Na)
=> ! [K: key1] :
( $lesseq(0,bucket1(K,Na))
& $less(bucket1(K,Na),Na) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bucket_bounds) ).
tff(f_297,axiom,
! [A: ty,A1: ty,X: uni,X1: uni] : sort1(tuple2(A1,A),tuple21(A1,A,X,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tuple2_sort2) ).
tff(f_331,axiom,
! [A: ty,K: key1,V: uni,M: uni,D: uni] :
( good_data1(A,K,V,M,D)
<=> ( ( get(option(A),key,M,t2tb1(K)) = some(A,V) )
<=> in_data1(A,K,V,D) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',good_data_def) ).
tff(f_397,axiom,
! [J: uni] : ( t2tb6(tb2t6(J)) = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR6) ).
tff(f_228,axiom,
! [A: ty,X: uni] :
( sort1(A,X)
=> ( ~ mem(A,X,nil(A))
& ! [X1: uni,X2: uni] :
( sort1(A,X1)
=> ( mem(A,X,cons(A,X1,X2))
<=> ( ( X = X1 )
| mem(A,X,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def) ).
tff(f_158,axiom,
! [A: ty,X: uni] : sort1(option(A),some(A,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',some_sort2) ).
tff(f_385,axiom,
! [J: uni] :
( sort1(option(a),J)
=> ( t2tb4(tb2t4(J)) = J ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR4) ).
tff(f_230,axiom,
! [A: ty,B: ty,X: uni,X1: uni] : sort1(B,get(B,A,X,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_sort4) ).
tff(c_510,plain,
$less(0,'#skF_3'),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_290,plain,
( ~ $lesseq(bucket1('#skF_12','#skF_3'),'#skF_6')
| ~ $lesseq(0,bucket1('#skF_12','#skF_3'))
| $lesseq(bucket1('#skF_14','#skF_3'),'#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_648,plain,
( $less('#skF_6',bucket1('#skF_12','#skF_3'))
| $less(bucket1('#skF_12','#skF_3'),0)
| ~ $less('#skF_6',bucket1('#skF_14','#skF_3')) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_290]) ).
tff(c_706250,plain,
bucket1('#skF_12','#skF_3') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_648]) ).
tff(c_154,plain,
! [K_184: key1,N_182a: $int] :
( $lesseq(0,bucket1(K_184,N_182a))
| ~ $less(0,N_182a) ),
inference(cnfTransformation,[status(thm)],[f_295]) ).
tff(c_553,plain,
! [K_184: key1,N_182a: $int] :
( ~ $less(bucket1(K_184,N_182a),0)
| ~ $less(0,N_182a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_154]) ).
tff(c_706259,plain,
( ~ $less('#skE_10',0)
| ~ $less(0,'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_706250,c_553]) ).
tff(c_706268,plain,
~ $less('#skE_10',0),
inference(demodulation,[status(thm),theory(equality)],[c_510,c_706259]) ).
tff(c_504134,plain,
bucket1('#skF_12','#skF_3') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_648]) ).
tff(c_158,plain,
! [A1_186: ty,A_185: ty,X_187: uni,X1_188: uni] : sort1(tuple2(A1_186,A_185),tuple21(A1_186,A_185,X_187,X1_188)),
inference(cnfTransformation,[status(thm)],[f_297]) ).
tff(c_642,plain,
! [K_318: key1,V_319: a1] :
( good_data1(a,K_318,t2tb7(V_319),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ( tb2t4(some(a,t2tb7(V_319))) = tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1(K_318))) )
| ~ in_data1(a,K_318,t2tb7(V_319),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_654,plain,
( in_data1(a,'#skF_12',t2tb7('#skF_13'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ~ good_data1(a,'#skF_14',t2tb7('#skF_15'),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_502677,plain,
~ good_data1(a,'#skF_14',t2tb7('#skF_15'),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(splitLeft,[status(thm)],[c_654]) ).
tff(c_508516,plain,
( ( tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14'))) = tb2t4(some(a,t2tb7('#skF_15'))) )
| ~ in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(resolution,[status(thm)],[c_642,c_502677]) ).
tff(c_518758,plain,
~ in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(splitLeft,[status(thm)],[c_508516]) ).
tff(c_504135,plain,
bucket1('#skF_14','#skF_3') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_648]) ).
tff(c_514485,plain,
! [V_36080: uni,M_36082: uni,K_36081: key1,D_36083: uni,A_36084: ty] :
( ( some(A_36084,V_36080) = get(option(A_36084),key,M_36082,t2tb1(K_36081)) )
| in_data1(A_36084,K_36081,V_36080,D_36083)
| good_data1(A_36084,K_36081,V_36080,M_36082,D_36083) ),
inference(cnfTransformation,[status(thm)],[f_331]) ).
tff(c_514490,plain,
( ( get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) = some(a,t2tb7('#skF_15')) )
| in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(resolution,[status(thm)],[c_514485,c_502677]) ).
tff(c_599004,plain,
get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) = some(a,t2tb7('#skF_15')),
inference(negUnitSimplification,[status(thm)],[c_518758,c_514490]) ).
tff(c_612,plain,
! [K_318: key1,V_319: a1] :
( good_data1(a,K_318,t2tb7(V_319),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| in_data1(a,K_318,t2tb7(V_319),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1(K_318),t2tb7(V_319)),t2tb6('#skF_7'))
| ( tb2t4(some(a,t2tb7(V_319))) != tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1(K_318))) )
| ( bucket1(K_318,'#skF_3') != '#skF_6' ) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_508501,plain,
( in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7'))
| ( tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14'))) != tb2t4(some(a,t2tb7('#skF_15'))) )
| ( bucket1('#skF_14','#skF_3') != '#skF_6' ) ),
inference(resolution,[status(thm)],[c_612,c_502677]) ).
tff(c_508515,plain,
( in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7'))
| ( tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14'))) != tb2t4(some(a,t2tb7('#skF_15'))) )
| ( '#skF_6' != '#skE_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_504135,c_508501]) ).
tff(c_630502,plain,
( in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7'))
| ( '#skF_6' != '#skE_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_599004,c_508515]) ).
tff(c_630504,plain,
( mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7'))
| ( '#skF_6' != '#skE_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_518758,c_630502]) ).
tff(c_630506,plain,
'#skF_6' != '#skE_11',
inference(splitLeft,[status(thm)],[c_630504]) ).
tff(c_504158,plain,
( ~ $less('#skE_11',0)
| ~ $less(0,'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_504135,c_553]) ).
tff(c_504167,plain,
~ $less('#skE_11',0),
inference(demodulation,[status(thm),theory(equality)],[c_510,c_504158]) ).
tff(c_355,plain,
! [K_318: key1,V_319: a1] :
( good_data1(a,K_318,t2tb7(V_319),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ~ $less(bucket1(K_318,'#skF_3'),'#skF_6')
| ~ $lesseq(0,bucket1(K_318,'#skF_3')) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_518148,plain,
! [K_36139: key1,V_36140: a1] :
( good_data1(a,K_36139,t2tb7(V_36140),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ~ $less(bucket1(K_36139,'#skF_3'),'#skF_6')
| $less(bucket1(K_36139,'#skF_3'),0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_355]) ).
tff(c_518160,plain,
( ~ $less(bucket1('#skF_14','#skF_3'),'#skF_6')
| $less(bucket1('#skF_14','#skF_3'),0) ),
inference(resolution,[status(thm)],[c_518148,c_502677]) ).
tff(c_518175,plain,
( ~ $less('#skE_11','#skF_6')
| $less('#skE_11',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_504135,c_504135,c_518160]) ).
tff(c_518177,plain,
~ $less('#skE_11','#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_504167,c_518175]) ).
tff(c_504140,plain,
( ~ $less('#skE_10',0)
| ~ $less(0,'#skF_3') ),
inference(superposition,[status(thm),theory(equality)],[c_504134,c_553]) ).
tff(c_504149,plain,
~ $less('#skE_10',0),
inference(demodulation,[status(thm),theory(equality)],[c_510,c_504140]) ).
tff(c_504131,plain,
bucket1('#skF_14','#skF_3') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_648]) ).
tff(c_504130,plain,
bucket1('#skF_12','#skF_3') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_648]) ).
tff(c_504136,plain,
( $less('#skF_6','#skE_10')
| $less('#skE_10',0)
| ~ $less('#skF_6','#skE_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_504131,c_504130,c_504130,c_648]) ).
tff(c_506481,plain,
( $less('#skF_6','#skE_10')
| ~ $less('#skF_6','#skE_11') ),
inference(negUnitSimplification,[status(thm)],[c_504149,c_504136]) ).
tff(c_506483,plain,
~ $less('#skF_6','#skE_11'),
inference(splitLeft,[status(thm)],[c_506481]) ).
tff(c_630507,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_630506,c_518177,c_506483]) ).
tff(c_630510,plain,
'#skF_6' = '#skE_11',
inference(splitRight,[status(thm)],[c_630504]) ).
tff(c_632827,plain,
! [K_56125: key1,V_56126: a1] :
( good_data1(a,K_56125,t2tb7(V_56126),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| in_data1(a,K_56125,t2tb7(V_56126),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1(K_56125),t2tb7(V_56126)),t2tb6('#skF_7'))
| ( tb2t4(some(a,t2tb7(V_56126))) != tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1(K_56125))) )
| ( bucket1(K_56125,'#skF_3') != '#skE_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_630510,c_612]) ).
tff(c_632839,plain,
( in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7'))
| ( tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14'))) != tb2t4(some(a,t2tb7('#skF_15'))) )
| ( bucket1('#skF_14','#skF_3') != '#skE_11' ) ),
inference(resolution,[status(thm)],[c_632827,c_502677]) ).
tff(c_632873,plain,
( in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_504135,c_599004,c_632839]) ).
tff(c_632874,plain,
mem(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15')),t2tb6('#skF_7')),
inference(negUnitSimplification,[status(thm)],[c_518758,c_632873]) ).
tff(c_256,plain,
tb2t6(nil(tuple2(key,a))) = '#skF_7',
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_502429,plain,
! [J_34918: uni] : ( t2tb6(tb2t6(J_34918)) = J_34918 ),
inference(cnfTransformation,[status(thm)],[f_397]) ).
tff(c_502438,plain,
nil(tuple2(key,a)) = t2tb6('#skF_7'),
inference(superposition,[status(thm),theory(equality)],[c_256,c_502429]) ).
tff(c_503061,plain,
! [A_35170: ty,X_35171: uni] :
( ~ mem(A_35170,X_35171,nil(A_35170))
| ~ sort1(A_35170,X_35171) ),
inference(cnfTransformation,[status(thm)],[f_228]) ).
tff(c_503064,plain,
! [X_35171: uni] :
( ~ mem(tuple2(key,a),X_35171,t2tb6('#skF_7'))
| ~ sort1(tuple2(key,a),X_35171) ),
inference(superposition,[status(thm),theory(equality)],[c_502438,c_503061]) ).
tff(c_667169,plain,
~ sort1(tuple2(key,a),tuple21(key,a,t2tb1('#skF_14'),t2tb7('#skF_15'))),
inference(resolution,[status(thm)],[c_632874,c_503064]) ).
tff(c_667179,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_158,c_667169]) ).
tff(c_667182,plain,
in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(splitRight,[status(thm)],[c_508516]) ).
tff(c_514455,plain,
! [M_36075: uni,K_36074: key1,V_36073: uni,A_36077: ty,D_36076: uni] :
( ~ in_data1(A_36077,K_36074,V_36073,D_36076)
| ( some(A_36077,V_36073) != get(option(A_36077),key,M_36075,t2tb1(K_36074)) )
| good_data1(A_36077,K_36074,V_36073,M_36075,D_36076) ),
inference(cnfTransformation,[status(thm)],[f_331]) ).
tff(c_514460,plain,
( ~ in_data1(a,'#skF_14',t2tb7('#skF_15'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ( get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) != some(a,t2tb7('#skF_15')) ) ),
inference(resolution,[status(thm)],[c_514455,c_502677]) ).
tff(c_696964,plain,
get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) != some(a,t2tb7('#skF_15')),
inference(demodulation,[status(thm),theory(equality)],[c_667182,c_514460]) ).
tff(c_64,plain,
! [A_50: ty,X_51: uni] : sort1(option(A_50),some(A_50,X_51)),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_502961,plain,
! [J_35152: uni] :
( ( t2tb4(tb2t4(J_35152)) = J_35152 )
| ~ sort1(option(a),J_35152) ),
inference(cnfTransformation,[status(thm)],[f_385]) ).
tff(c_502991,plain,
! [X_51: uni] : ( t2tb4(tb2t4(some(a,X_51))) = some(a,X_51) ),
inference(resolution,[status(thm)],[c_64,c_502961]) ).
tff(c_667180,plain,
tb2t4(get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14'))) = tb2t4(some(a,t2tb7('#skF_15'))),
inference(splitRight,[status(thm)],[c_508516]) ).
tff(c_110,plain,
! [B_115: ty,A_114: ty,X_116: uni,X1_117: uni] : sort1(B_115,get(B_115,A_114,X_116,X1_117)),
inference(cnfTransformation,[status(thm)],[f_230]) ).
tff(c_693631,plain,
! [A_57281: ty,X_57282: uni,X1_57283: uni] : ( t2tb4(tb2t4(get(option(a),A_57281,X_57282,X1_57283))) = get(option(a),A_57281,X_57282,X1_57283) ),
inference(resolution,[status(thm)],[c_110,c_502961]) ).
tff(c_693709,plain,
get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) = t2tb4(tb2t4(some(a,t2tb7('#skF_15')))),
inference(superposition,[status(thm),theory(equality)],[c_667180,c_693631]) ).
tff(c_693742,plain,
get(option(a),key,t2tb3('#skF_9'),t2tb1('#skF_14')) = some(a,t2tb7('#skF_15')),
inference(demodulation,[status(thm),theory(equality)],[c_502991,c_693709]) ).
tff(c_700159,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_696964,c_693742]) ).
tff(c_700163,plain,
$less('#skF_6','#skE_11'),
inference(splitRight,[status(thm)],[c_506481]) ).
tff(c_287,plain,
( in_data1(a,'#skF_12',t2tb7('#skF_13'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| $lesseq(bucket1('#skF_14','#skF_3'),'#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_650,plain,
( in_data1(a,'#skF_12',t2tb7('#skF_13'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8')))
| ~ $less('#skF_6',bucket1('#skF_14','#skF_3')) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_287]) ).
tff(c_704782,plain,
in_data1(a,'#skF_12',t2tb7('#skF_13'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(demodulation,[status(thm),theory(equality)],[c_700163,c_504135,c_650]) ).
tff(c_628,plain,
! [K_318: key1,V_319: a1] :
( $less(bucket1(K_318,'#skF_3'),'#skF_6')
| ( bucket1(K_318,'#skF_3') = '#skF_6' )
| ~ in_data1(a,K_318,t2tb7(V_319),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_704790,plain,
( $less(bucket1('#skF_12','#skF_3'),'#skF_6')
| ( bucket1('#skF_12','#skF_3') = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_704782,c_628]) ).
tff(c_704794,plain,
( $less('#skE_10','#skF_6')
| ( '#skF_6' = '#skE_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_504134,c_504134,c_704790]) ).
tff(c_704796,plain,
'#skF_6' = '#skE_10',
inference(splitLeft,[status(thm)],[c_704794]) ).
tff(c_700162,plain,
$less('#skF_6','#skE_10'),
inference(splitRight,[status(thm)],[c_506481]) ).
tff(c_704815,plain,
$less('#skE_10','#skE_10'),
inference(demodulation,[status(thm),theory(equality)],[c_704796,c_700162]) ).
tff(c_704843,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_704815]) ).
tff(c_704846,plain,
$less('#skE_10','#skF_6'),
inference(splitRight,[status(thm)],[c_704794]) ).
tff(c_704848,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_704846,c_700162]) ).
tff(c_704852,plain,
good_data1(a,'#skF_14',t2tb7('#skF_15'),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(splitRight,[status(thm)],[c_654]) ).
tff(c_284,plain,
( ~ $lesseq(bucket1('#skF_12','#skF_3'),'#skF_6')
| ~ $lesseq(0,bucket1('#skF_12','#skF_3'))
| ~ good_data1(a,'#skF_14',t2tb7('#skF_15'),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(cnfTransformation,[status(thm)],[f_504]) ).
tff(c_652,plain,
( $less('#skF_6',bucket1('#skF_12','#skF_3'))
| $less(bucket1('#skF_12','#skF_3'),0)
| ~ good_data1(a,'#skF_14',t2tb7('#skF_15'),t2tb3('#skF_9'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_284]) ).
tff(c_729309,plain,
( $less('#skF_6','#skE_10')
| $less('#skE_10',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_704852,c_706250,c_706250,c_652]) ).
tff(c_729311,plain,
$less('#skF_6','#skE_10'),
inference(negUnitSimplification,[status(thm)],[c_706268,c_729309]) ).
tff(c_704851,plain,
in_data1(a,'#skF_12',t2tb7('#skF_13'),mk_array1(list(tuple2(key,a)),$sum(1,$product(2,'#skF_3')),t2tb2('#skF_8'))),
inference(splitRight,[status(thm)],[c_654]) ).
tff(c_708418,plain,
( $less(bucket1('#skF_12','#skF_3'),'#skF_6')
| ( bucket1('#skF_12','#skF_3') = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_704851,c_628]) ).
tff(c_708422,plain,
( $less('#skE_10','#skF_6')
| ( '#skF_6' = '#skE_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_706250,c_706250,c_708418]) ).
tff(c_708424,plain,
'#skF_6' = '#skE_10',
inference(splitLeft,[status(thm)],[c_708422]) ).
tff(c_718818,plain,
( $less('#skE_10','#skE_10')
| $less('#skE_10',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_704852,c_706250,c_708424,c_706250,c_652]) ).
tff(c_718819,plain,
$less('#skE_10','#skE_10'),
inference(negUnitSimplification,[status(thm)],[c_706268,c_718818]) ).
tff(c_718821,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_718819]) ).
tff(c_718824,plain,
$less('#skE_10','#skF_6'),
inference(splitRight,[status(thm)],[c_708422]) ).
tff(c_729312,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_729311,c_718824]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.11 % Problem : SWW605_2 : TPTP v9.0.0. Released v6.1.0.
% 0.12/0.12 % 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.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Apr 9 06:17:08 EDT 2025
% 0.12/0.33 % CPUTime :
% 138.74/101.76 ***********************************************************************
% 138.74/101.77 After 99.7 sec it's time to try something different, got 99.6 sec left
% 138.74/101.77 ***********************************************************************
% 201.26/151.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 201.26/151.88
% 201.26/151.88 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------