%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC526_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 : Tue Sep 29 01:06:11 PM UTC 2026
% Result : Theorem 0.19s 0.32s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC526_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 09:41:37 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.32 % (241880)Will run a generic schedule for satisfiability detection.
% 0.19/0.32 % (241895)% WARNING: option uhcvi not known.
% 0.19/0.32 % (241895)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3585100602:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.32 % (241896)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=454582201:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.32 % (241897)dis+10_1_sil=32000:sp=arity:random_seed=3908969109:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.32 % (241899)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3729394530:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.32 % (241894)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2124139139_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.32 % (241900)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3537293965:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.32 % (241901)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3700223379:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.32 % (241894)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.19/0.32 % (241894)Terminated due to inappropriate strategy.
% 0.19/0.32 % (241894)------------------------------
% 0.19/0.32 % (241894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.32 % (241894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.32 % (241894)CaDiCaL version: 2.1.3
% 0.19/0.32 % (241894)Termination reason: Inappropriate
% 0.19/0.32 % (241894)Time elapsed: 0.022 s
% 0.19/0.32 % (241894)Peak memory usage: 12 MB
% 0.19/0.32 % (241894)Instructions burned: 44 (million)
% 0.19/0.32 % (241894)------------------------------
% 0.19/0.32 % (241894)------------------------------
% 0.19/0.32 % (241895) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-241880-241895"...
% 0.19/0.32 % (241921)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=709207176:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.32 % (241895)...printing done.
% 0.19/0.32 % (241895)Refutation found. Thanks to Tanya!
% 0.19/0.32 % SZS status Theorem for theBenchmark
% 0.19/0.32 % SZS output start Proof for theBenchmark
% 0.19/0.32 tff(type_def_5, type, set_0: $tType).
% 0.19/0.32 tff(type_def_6, type, set_2: $tType).
% 0.19/0.32 tff(type_def_7, type, set_3: $tType).
% 0.19/0.32 tff(type_def_8, type, set_4: $tType).
% 0.19/0.32 tff(type_def_9, type, set_5: $tType).
% 0.19/0.32 tff(type_def_10, type, set_6: $tType).
% 0.19/0.32 tff(func_def_0, type, min_int: $int).
% 0.19/0.32 tff(func_def_1, type, max_int: $int).
% 0.19/0.32 tff(func_def_5, type, g_s0_0: set_0).
% 0.19/0.32 tff(func_def_6, type, g_s1_1: $int).
% 0.19/0.32 tff(func_def_7, type, g_s2_2: $int).
% 0.19/0.32 tff(func_def_8, type, g_s3_3: set_0).
% 0.19/0.32 tff(func_def_9, type, g_s4_4: $int).
% 0.19/0.32 tff(func_def_10, type, g_s5_5: $int).
% 0.19/0.32 tff(func_def_11, type, g_s6_6: set_0).
% 0.19/0.32 tff(func_def_12, type, g_s7_7: $int).
% 0.19/0.32 tff(func_def_13, type, g_s8_8: $int).
% 0.19/0.32 tff(func_def_14, type, g_s9_9: $int).
% 0.19/0.32 tff(func_def_15, type, g_s10_10: $int).
% 0.19/0.32 tff(func_def_16, type, g_s11_11: $int).
% 0.19/0.32 tff(func_def_17, type, g_s12_12: $int).
% 0.19/0.32 tff(func_def_18, type, g_s13_13: $int).
% 0.19/0.32 tff(func_def_19, type, g_s14_14: $int).
% 0.19/0.32 tff(func_def_20, type, g_s15_15: $int).
% 0.19/0.32 tff(func_def_21, type, g_s16_16: set_0).
% 0.19/0.32 tff(func_def_22, type, g_s17_17: $int).
% 0.19/0.32 tff(func_def_23, type, g_s18_18: $int).
% 0.19/0.32 tff(func_def_24, type, g_s19_19: $int).
% 0.19/0.32 tff(func_def_25, type, g_s20_20: $int).
% 0.19/0.32 tff(func_def_26, type, g_s21_21: $int).
% 0.19/0.32 tff(func_def_27, type, g_s22_22: $int).
% 0.19/0.32 tff(func_def_28, type, g_s23_23: $int).
% 0.19/0.32 tff(func_def_29, type, g_s24_24: $int).
% 0.19/0.32 tff(func_def_30, type, g_s25_25: $int).
% 0.19/0.32 tff(func_def_31, type, g_s26_26: $int).
% 0.19/0.32 tff(func_def_32, type, g_s27_27: $int).
% 0.19/0.32 tff(func_def_33, type, g_s28_28: $int).
% 0.19/0.32 tff(func_def_34, type, g_s29_29: $int).
% 0.19/0.32 tff(func_def_35, type, g_s30_30: $int).
% 0.19/0.32 tff(func_def_36, type, g_s31_31: $int).
% 0.19/0.32 tff(func_def_37, type, g_s32_32: $int).
% 0.19/0.32 tff(func_def_38, type, g_s33_33: $int).
% 0.19/0.32 tff(func_def_39, type, g_s34_34: set_0).
% 0.19/0.32 tff(func_def_40, type, g_s35_35: $int).
% 0.19/0.32 tff(func_def_41, type, g_s36_36: $int).
% 0.19/0.32 tff(func_def_42, type, g_s37_37: set_0).
% 0.19/0.32 tff(func_def_43, type, g_s38_38: $int).
% 0.19/0.32 tff(func_def_44, type, g_s39_39: $int).
% 0.19/0.32 tff(func_def_45, type, g_s40_40: set_0).
% 0.19/0.32 tff(func_def_46, type, g_s41_41: $int).
% 0.19/0.32 tff(func_def_47, type, g_s42_42: $int).
% 0.19/0.32 tff(func_def_48, type, g_s43_43: $int).
% 0.19/0.32 tff(func_def_49, type, g_s44_44: $int).
% 0.19/0.32 tff(func_def_50, type, g_s45_45: $int).
% 0.19/0.32 tff(func_def_51, type, g_s46_46: $int).
% 0.19/0.32 tff(func_def_52, type, g_s47_47: $int).
% 0.19/0.32 tff(func_def_53, type, g_s48_48: $int).
% 0.19/0.32 tff(func_def_54, type, g_s49_49: $int).
% 0.19/0.32 tff(func_def_55, type, g_s51_50: set_0).
% 0.19/0.32 tff(func_def_56, type, g_s50_51: $int).
% 0.19/0.32 tff(func_def_57, type, g_s53_52: set_0).
% 0.19/0.32 tff(func_def_58, type, g_s52_53: $int).
% 0.19/0.32 tff(func_def_59, type, g_s55_54: set_0).
% 0.19/0.32 tff(func_def_60, type, g_s54_55: $int).
% 0.19/0.32 tff(func_def_61, type, g_s56_56: $int).
% 0.19/0.32 tff(func_def_62, type, g_s57_57: $int).
% 0.19/0.32 tff(func_def_63, type, g_s58_58: set_0).
% 0.19/0.32 tff(func_def_64, type, set_2_empty: set_2).
% 0.19/0.32 tff(func_def_65, type, set_2_insert: set_2 > set_2).
% 0.19/0.32 tff(func_def_66, type, g_s59_59: set_2).
% 0.19/0.32 tff(func_def_67, type, g_s60_60: $int).
% 0.19/0.32 tff(func_def_68, type, g_s61_61: $int).
% 0.19/0.32 tff(func_def_69, type, g_s62_62: $int).
% 0.19/0.32 tff(func_def_70, type, g_s63_63: $int).
% 0.19/0.32 tff(func_def_71, type, g_s64_64: $int).
% 0.19/0.32 tff(func_def_72, type, g_s65_65: $int).
% 0.19/0.32 tff(func_def_73, type, g_s66_66: $int).
% 0.19/0.32 tff(func_def_74, type, g_s67_67: $int).
% 0.19/0.32 tff(func_def_75, type, g_s68_68: $int).
% 0.19/0.32 tff(func_def_76, type, g_s69_69: $int).
% 0.19/0.32 tff(func_def_77, type, g_s70_70: $int).
% 0.19/0.32 tff(func_def_78, type, g_s71_71: $int).
% 0.19/0.32 tff(func_def_79, type, g_s72_72: $int).
% 0.19/0.32 tff(func_def_80, type, g_s73_73: $int).
% 0.19/0.32 tff(func_def_81, type, g_s74_74: $int).
% 0.19/0.32 tff(func_def_82, type, g_s75_75: $int).
% 0.19/0.32 tff(func_def_83, type, g_s76_76: $int).
% 0.19/0.32 tff(func_def_84, type, g_s77_77: $int).
% 0.19/0.32 tff(func_def_85, type, g_s78_78: $int).
% 0.19/0.32 tff(func_def_86, type, g_s79_79: $int).
% 0.19/0.32 tff(func_def_87, type, g_s80_80: $int).
% 0.19/0.32 tff(func_def_88, type, g_s81_81: $int).
% 0.19/0.32 tff(func_def_89, type, g_s82_82: $int).
% 0.19/0.32 tff(func_def_90, type, g_s83_83: $int).
% 0.19/0.32 tff(func_def_91, type, g_s84_84: $int).
% 0.19/0.32 tff(func_def_92, type, g_s85_85: $int).
% 0.19/0.32 tff(func_def_93, type, g_s86_86: $int).
% 0.19/0.32 tff(func_def_94, type, g_s87_87: $int).
% 0.19/0.32 tff(func_def_95, type, g_s88_88: $int).
% 0.19/0.32 tff(func_def_96, type, g_s89_89: $int).
% 0.19/0.32 tff(func_def_97, type, g_s90_90: set_0).
% 0.19/0.32 tff(func_def_98, type, g_s91_91: set_0).
% 0.19/0.32 tff(func_def_99, type, g_s92_92: $int).
% 0.19/0.32 tff(func_def_100, type, g_s93_93: $int).
% 0.19/0.32 tff(func_def_101, type, g_s94_94: $int).
% 0.19/0.32 tff(func_def_102, type, g_s95_95: $int).
% 0.19/0.32 tff(func_def_103, type, g_s96_96: $int).
% 0.19/0.32 tff(func_def_104, type, g_s97_97: $int).
% 0.19/0.32 tff(func_def_105, type, g_s98_98: $int).
% 0.19/0.32 tff(func_def_106, type, g_s99_99: $int).
% 0.19/0.32 tff(func_def_107, type, g_s100_100: $int).
% 0.19/0.32 tff(func_def_108, type, g_s101_101: $int).
% 0.19/0.32 tff(func_def_109, type, g_s102_102: $int).
% 0.19/0.32 tff(func_def_110, type, g_s103_103: $int).
% 0.19/0.32 tff(func_def_111, type, g_s104_104: $int).
% 0.19/0.32 tff(func_def_112, type, g_s105_105: $int).
% 0.19/0.32 tff(func_def_113, type, g_s106_106: $int).
% 0.19/0.32 tff(func_def_114, type, g_s107_107: $int).
% 0.19/0.32 tff(func_def_115, type, g_s108_108: $int).
% 0.19/0.32 tff(func_def_116, type, g_s109_109: $int).
% 0.19/0.32 tff(func_def_117, type, g_s110_110: $int).
% 0.19/0.32 tff(func_def_118, type, g_s111_111: $int).
% 0.19/0.32 tff(func_def_119, type, g_s112_112: $int).
% 0.19/0.32 tff(func_def_120, type, g_s113_113: $int).
% 0.19/0.32 tff(func_def_121, type, g_s114_114: $int).
% 0.19/0.32 tff(func_def_122, type, g_s115_115: $int).
% 0.19/0.32 tff(func_def_123, type, g_s116_116: $int).
% 0.19/0.32 tff(func_def_124, type, g_s117_117: $int).
% 0.19/0.32 tff(func_def_125, type, g_s118_118: $int).
% 0.19/0.32 tff(func_def_126, type, g_s119_119: $int).
% 0.19/0.32 tff(func_def_127, type, g_s120_120: $int).
% 0.19/0.32 tff(func_def_128, type, g_s121_121: $int).
% 0.19/0.32 tff(func_def_129, type, g_s122_122: $int).
% 0.19/0.32 tff(func_def_130, type, g_s123_123: $int).
% 0.19/0.32 tff(func_def_131, type, g_s124_124: $int).
% 0.19/0.32 tff(func_def_132, type, g_s125_125: $int).
% 0.19/0.32 tff(func_def_133, type, g_s126_126: $int).
% 0.19/0.32 tff(func_def_134, type, g_s127_127: $int).
% 0.19/0.32 tff(func_def_135, type, g_s128_128: $int).
% 0.19/0.32 tff(func_def_136, type, g_s129_129: $int).
% 0.19/0.32 tff(func_def_137, type, g_s130_130: $int).
% 0.19/0.32 tff(func_def_138, type, g_s131_131: $int).
% 0.19/0.32 tff(func_def_139, type, g_s132_132: $int).
% 0.19/0.32 tff(func_def_140, type, g_s133_133: $int).
% 0.19/0.32 tff(func_def_141, type, g_s134_134: $int).
% 0.19/0.32 tff(func_def_142, type, g_s135_135: $int).
% 0.19/0.32 tff(func_def_143, type, g_s136_136: $int).
% 0.19/0.32 tff(func_def_144, type, g_s137_137: $int).
% 0.19/0.32 tff(func_def_145, type, g_s138_138: $int).
% 0.19/0.32 tff(func_def_146, type, g_s139_139: $int).
% 0.19/0.32 tff(func_def_147, type, g_s140_140: $int).
% 0.19/0.32 tff(func_def_148, type, g_s141_141: $int).
% 0.19/0.32 tff(func_def_149, type, g_s142_142: $int).
% 0.19/0.32 tff(func_def_150, type, g_s143_143: $int).
% 0.19/0.32 tff(func_def_151, type, g_s144_144: $int).
% 0.19/0.32 tff(func_def_152, type, g_s145_145: $int).
% 0.19/0.32 tff(func_def_153, type, g_s146_146: $int).
% 0.19/0.32 tff(func_def_154, type, g_s147_147: $int).
% 0.19/0.32 tff(func_def_155, type, g_s148_148: $int).
% 0.19/0.32 tff(func_def_156, type, g_s149_149: $int).
% 0.19/0.32 tff(func_def_157, type, g_s150_150: $int).
% 0.19/0.32 tff(func_def_158, type, g_s151_151: $int).
% 0.19/0.32 tff(func_def_159, type, g_s152_152: $int).
% 0.19/0.32 tff(func_def_160, type, g_s153_153: $int).
% 0.19/0.32 tff(func_def_161, type, g_s154_154: $int).
% 0.19/0.32 tff(func_def_162, type, g_s155_155: $int).
% 0.19/0.32 tff(func_def_163, type, g_s156_156: $int).
% 0.19/0.32 tff(func_def_164, type, g_s157_157: $int).
% 0.19/0.32 tff(func_def_165, type, g_s158_158: $int).
% 0.19/0.32 tff(func_def_166, type, g_s159_159: $int).
% 0.19/0.32 tff(func_def_167, type, g_s160_160: $int).
% 0.19/0.32 tff(func_def_168, type, g_s161_161: $int).
% 0.19/0.32 tff(func_def_169, type, g_s162_162: $int).
% 0.19/0.32 tff(func_def_170, type, g_s163_163: $int).
% 0.19/0.32 tff(func_def_171, type, g_s164_164: $int).
% 0.19/0.32 tff(func_def_172, type, g_s165_165: $int).
% 0.19/0.32 tff(func_def_173, type, g_s166_166: $int).
% 0.19/0.32 tff(func_def_174, type, g_s167_167: $int).
% 0.19/0.32 tff(func_def_175, type, g_s168_168: $int).
% 0.19/0.32 tff(func_def_176, type, g_s169_169: $int).
% 0.19/0.32 tff(func_def_177, type, g_s170_170: $int).
% 0.19/0.32 tff(func_def_178, type, g_s171_171: $int).
% 0.19/0.32 tff(func_def_179, type, g_s172_172: $int).
% 0.19/0.32 tff(func_def_180, type, g_s173_173: $int).
% 0.19/0.32 tff(func_def_181, type, g_s174_174: $int).
% 0.19/0.32 tff(func_def_182, type, g_s175_175: $int).
% 0.19/0.32 tff(func_def_183, type, g_s176_176: $int).
% 0.19/0.32 tff(func_def_184, type, g_s177_177: $int).
% 0.19/0.32 tff(func_def_185, type, g_s178_178: $int).
% 0.19/0.32 tff(func_def_186, type, g_s179_179: $int).
% 0.19/0.32 tff(func_def_187, type, g_s180_180: $int).
% 0.19/0.32 tff(func_def_188, type, g_s181_181: $int).
% 0.19/0.32 tff(func_def_189, type, g_s182_182: $int).
% 0.19/0.32 tff(func_def_190, type, g_s183_183: $int).
% 0.19/0.32 tff(func_def_191, type, g_s184_184: $int).
% 0.19/0.32 tff(func_def_192, type, g_s185_185: $int).
% 0.19/0.32 tff(func_def_193, type, g_s186_186: $int).
% 0.19/0.32 tff(func_def_194, type, g_s187_187: $int).
% 0.19/0.32 tff(func_def_195, type, g_s188_188: $int).
% 0.19/0.32 tff(func_def_196, type, g_s189_189: $int).
% 0.19/0.32 tff(func_def_197, type, g_s190_190: $int).
% 0.19/0.32 tff(func_def_198, type, g_s191_191: $int).
% 0.19/0.32 tff(func_def_199, type, g_s192_192: $int).
% 0.19/0.32 tff(func_def_200, type, g_s193_193: $int).
% 0.19/0.32 tff(func_def_201, type, g_s194_194: $int).
% 0.19/0.32 tff(func_def_202, type, g_s195_195: $int).
% 0.19/0.32 tff(func_def_203, type, g_s196_196: $int).
% 0.19/0.32 tff(func_def_204, type, g_s197_197: $int).
% 0.19/0.32 tff(func_def_205, type, g_s198_198: $int).
% 0.19/0.32 tff(func_def_206, type, g_s199_199: $int).
% 0.19/0.32 tff(func_def_207, type, g_s200_200: $int).
% 0.19/0.32 tff(func_def_208, type, g_s201_201: $int).
% 0.19/0.32 tff(func_def_209, type, g_s202_202: $int).
% 0.19/0.32 tff(func_def_210, type, g_s203_203: $int).
% 0.19/0.32 tff(func_def_211, type, g_s204_204: $int).
% 0.19/0.32 tff(func_def_212, type, g_s205_205: $int).
% 0.19/0.32 tff(func_def_213, type, set_3_empty: set_3).
% 0.19/0.32 tff(func_def_214, type, set_3_insert: set_3 > set_3).
% 0.19/0.32 tff(func_def_215, type, g_s206_206: set_3).
% 0.19/0.32 tff(func_def_216, type, set_4_empty: set_4).
% 0.19/0.32 tff(func_def_217, type, set_4_insert: set_4 > set_4).
% 0.19/0.32 tff(func_def_218, type, g_s207_207: set_4).
% 0.19/0.32 tff(func_def_219, type, g_s208_208: set_3).
% 0.19/0.32 tff(func_def_220, type, g_s209_209: set_4).
% 0.19/0.32 tff(func_def_221, type, g_s210_210: set_3).
% 0.19/0.32 tff(func_def_222, type, g_s211_211: $int).
% 0.19/0.32 tff(func_def_223, type, g_s212_212: $int).
% 0.19/0.32 tff(func_def_224, type, g_s213_213: $int).
% 0.19/0.32 tff(func_def_225, type, g_s214_214: $int).
% 0.19/0.32 tff(func_def_226, type, g_s215_215: $int).
% 0.19/0.32 tff(func_def_227, type, g_s216_216: $int).
% 0.19/0.32 tff(func_def_228, type, g_s217_217: $int).
% 0.19/0.32 tff(func_def_229, type, g_s218_218: $int).
% 0.19/0.32 tff(func_def_230, type, g_s219_219: $int).
% 0.19/0.32 tff(func_def_231, type, g_s220_220: $int).
% 0.19/0.32 tff(func_def_232, type, g_s221_221: $int).
% 0.19/0.32 tff(func_def_233, type, g_s222_222: $int).
% 0.19/0.32 tff(func_def_234, type, g_s223_223: $int).
% 0.19/0.32 tff(func_def_235, type, g_s224_224: $int).
% 0.19/0.32 tff(func_def_236, type, g_s225_225: $int).
% 0.19/0.32 tff(func_def_237, type, g_s226_226: $int).
% 0.19/0.32 tff(func_def_238, type, g_s227_227: $int).
% 0.19/0.32 tff(func_def_239, type, g_s228_228: $int).
% 0.19/0.32 tff(func_def_240, type, g_s229_229: $int).
% 0.19/0.32 tff(func_def_241, type, g_s230_230: $int).
% 0.19/0.32 tff(func_def_242, type, g_s231_231: $int).
% 0.19/0.32 tff(func_def_243, type, g_s232_232: $int).
% 0.19/0.32 tff(func_def_244, type, g_s233_233: $int).
% 0.19/0.32 tff(func_def_245, type, g_s234_234: $int).
% 0.19/0.32 tff(func_def_246, type, g_s235_235: $int).
% 0.19/0.32 tff(func_def_247, type, g_s236_236: $int).
% 0.19/0.32 tff(func_def_248, type, g_s237_237: $int).
% 0.19/0.32 tff(func_def_249, type, g_s238_238: $int).
% 0.19/0.32 tff(func_def_250, type, g_s239_239: $int).
% 0.19/0.32 tff(func_def_251, type, g_s240_240: $int).
% 0.19/0.32 tff(func_def_252, type, g_s241_241: $int).
% 0.19/0.32 tff(func_def_253, type, g_s242_242: $int).
% 0.19/0.32 tff(func_def_254, type, g_s243_243: $int).
% 0.19/0.32 tff(func_def_255, type, g_s244_244: $int).
% 0.19/0.32 tff(func_def_256, type, g_s245_245: $int).
% 0.19/0.32 tff(func_def_257, type, g_s246_246: $int).
% 0.19/0.32 tff(func_def_258, type, g_s247_247: $int).
% 0.19/0.32 tff(func_def_259, type, g_s248_248: $int).
% 0.19/0.32 tff(func_def_260, type, g_s249_249: $int).
% 0.19/0.32 tff(func_def_261, type, g_s250_250: $int).
% 0.19/0.32 tff(func_def_262, type, g_s251_251: $int).
% 0.19/0.32 tff(func_def_263, type, g_s252_252: $int).
% 0.19/0.32 tff(func_def_264, type, g_s253_253: $int).
% 0.19/0.32 tff(func_def_265, type, g_s254_254: $int).
% 0.19/0.32 tff(func_def_266, type, g_s255_255: $int).
% 0.19/0.32 tff(func_def_267, type, g_s256_256: $int).
% 0.19/0.32 tff(func_def_268, type, g_s257_257: $int).
% 0.19/0.32 tff(func_def_269, type, g_s258_258: $int).
% 0.19/0.32 tff(func_def_270, type, g_s259_259: $int).
% 0.19/0.32 tff(func_def_271, type, g_s260_260: $int).
% 0.19/0.32 tff(func_def_272, type, g_s261_261: $int).
% 0.19/0.32 tff(func_def_273, type, g_s262_262: $int).
% 0.19/0.32 tff(func_def_274, type, g_s263_263: $int).
% 0.19/0.32 tff(func_def_275, type, g_s264_264: $int).
% 0.19/0.32 tff(func_def_276, type, g_s265_265: $int).
% 0.19/0.32 tff(func_def_277, type, g_s266_266: $int).
% 0.19/0.32 tff(func_def_278, type, g_s267_267: $int).
% 0.19/0.32 tff(func_def_279, type, g_s268_268: $int).
% 0.19/0.32 tff(func_def_280, type, g_s269_269: $int).
% 0.19/0.32 tff(func_def_281, type, g_s270_270: $int).
% 0.19/0.32 tff(func_def_282, type, g_s271_271: $int).
% 0.19/0.32 tff(func_def_283, type, g_s272_272: $int).
% 0.19/0.32 tff(func_def_284, type, g_s273_273: $int).
% 0.19/0.32 tff(func_def_285, type, g_s274_274: $int).
% 0.19/0.32 tff(func_def_286, type, g_s275_275: $int).
% 0.19/0.32 tff(func_def_287, type, g_s276_276: $int).
% 0.19/0.32 tff(func_def_288, type, g_s277_277: $int).
% 0.19/0.32 tff(func_def_289, type, g_s278_278: $int).
% 0.19/0.32 tff(func_def_290, type, g_s279_279: $int).
% 0.19/0.32 tff(func_def_291, type, g_s280_280: $int).
% 0.19/0.32 tff(func_def_292, type, g_s281_281: $int).
% 0.19/0.32 tff(func_def_293, type, g_s282_282: $int).
% 0.19/0.32 tff(func_def_294, type, g_s283_283: $int).
% 0.19/0.32 tff(func_def_295, type, g_s284_284: $int).
% 0.19/0.32 tff(func_def_296, type, g_s285_285: $int).
% 0.19/0.32 tff(func_def_297, type, g_s286_286: $int).
% 0.19/0.32 tff(func_def_298, type, g_s287_287: $int).
% 0.19/0.32 tff(func_def_299, type, g_s288_288: $int).
% 0.19/0.32 tff(func_def_300, type, g_s289_289: $int).
% 0.19/0.32 tff(func_def_301, type, g_s290_290: $int).
% 0.19/0.32 tff(func_def_302, type, g_s291_291: $int).
% 0.19/0.32 tff(func_def_303, type, g_s292_292: $int).
% 0.19/0.32 tff(func_def_304, type, g_s293_293: $int).
% 0.19/0.32 tff(func_def_305, type, g_s294_294: $int).
% 0.19/0.32 tff(func_def_306, type, g_s295_295: $int).
% 0.19/0.32 tff(func_def_307, type, g_s296_296: $int).
% 0.19/0.32 tff(func_def_308, type, g_s297_297: $int).
% 0.19/0.32 tff(func_def_309, type, g_s298_298: $int).
% 0.19/0.32 tff(func_def_310, type, g_s299_299: $int).
% 0.19/0.32 tff(func_def_311, type, g_s301_300: set_0).
% 0.19/0.32 tff(func_def_312, type, g_s306_301: set_0).
% 0.19/0.32 tff(func_def_313, type, g_s307_302: set_0).
% 0.19/0.32 tff(func_def_314, type, g_s308_303: set_4).
% 0.19/0.32 tff(func_def_315, type, g_s309_304: set_4).
% 0.19/0.32 tff(func_def_316, type, set_5_empty: set_5).
% 0.19/0.32 tff(func_def_317, type, set_5_insert: set_5 > set_5).
% 0.19/0.32 tff(func_def_318, type, g_s310_305: set_5).
% 0.19/0.32 tff(func_def_319, type, g_s311_306: set_4).
% 0.19/0.32 tff(func_def_320, type, g_s312_307: set_4).
% 0.19/0.32 tff(func_def_321, type, g_s313_308: set_4).
% 0.19/0.32 tff(func_def_322, type, g_s314_309: set_4).
% 0.19/0.32 tff(func_def_323, type, g_s315_310: set_4).
% 0.19/0.32 tff(func_def_324, type, g_s316_311: set_4).
% 0.19/0.32 tff(func_def_325, type, g_s317_312: set_4).
% 0.19/0.32 tff(func_def_326, type, g_s318_313: set_4).
% 0.19/0.32 tff(func_def_327, type, g_s319_314: set_4).
% 0.19/0.32 tff(func_def_328, type, g_s320_315: set_4).
% 0.19/0.32 tff(func_def_329, type, g_s321_316: set_4).
% 0.19/0.32 tff(func_def_330, type, g_s322_317: set_4).
% 0.19/0.32 tff(func_def_331, type, g_s323_318: set_4).
% 0.19/0.32 tff(func_def_332, type, g_s324_319: set_4).
% 0.19/0.32 tff(func_def_333, type, g_s325_320: set_4).
% 0.19/0.32 tff(func_def_334, type, g_s326_321: set_4).
% 0.19/0.32 tff(func_def_335, type, g_s327_322: set_4).
% 0.19/0.32 tff(func_def_336, type, g_s328_323: set_4).
% 0.19/0.32 tff(func_def_337, type, g_s329_324: $int).
% 0.19/0.32 tff(func_def_338, type, g_s330_325: $int).
% 0.19/0.32 tff(func_def_339, type, g_s331_326: $int).
% 0.19/0.32 tff(func_def_340, type, g_s332_327: set_4).
% 0.19/0.32 tff(func_def_341, type, set_6_empty: set_6).
% 0.19/0.32 tff(func_def_342, type, set_6_insert: set_6 > set_6).
% 0.19/0.32 tff(func_def_343, type, g_s333_328: set_6).
% 0.19/0.32 tff(func_def_344, type, g_s334_329: set_5).
% 0.19/0.32 tff(func_def_345, type, g_s335_330: set_5).
% 0.19/0.32 tff(func_def_346, type, g_s336_331: set_5).
% 0.19/0.32 tff(func_def_347, type, g_s337_332: set_5).
% 0.19/0.32 tff(func_def_348, type, g_s338_333: set_5).
% 0.19/0.32 tff(func_def_349, type, g_s339_334: set_5).
% 0.19/0.32 tff(func_def_350, type, g_s340_335: set_5).
% 0.19/0.32 tff(func_def_351, type, g_s341_336: set_6).
% 0.19/0.32 tff(func_def_352, type, g_s342_337: set_6).
% 0.19/0.32 tff(func_def_353, type, g_s343_338: set_4).
% 0.19/0.32 tff(func_def_354, type, g_s344_339: set_5).
% 0.19/0.32 tff(func_def_355, type, g_s345_340: set_4).
% 0.19/0.32 tff(func_def_356, type, g_s346_341: set_4).
% 0.19/0.32 tff(func_def_357, type, g_s347_342: set_4).
% 0.19/0.32 tff(func_def_358, type, g_s348_343: set_4).
% 0.19/0.32 tff(func_def_359, type, g_s349_344: set_4).
% 0.19/0.32 tff(func_def_360, type, g_s350_345: set_4).
% 0.19/0.32 tff(func_def_361, type, g_s351_346: set_4).
% 0.19/0.32 tff(func_def_362, type, g_s352_347: set_5).
% 0.19/0.32 tff(func_def_363, type, g_s353_348: set_5).
% 0.19/0.32 tff(func_def_364, type, g_s354_349: $int).
% 0.19/0.32 tff(func_def_365, type, g_s355_350: $int).
% 0.19/0.32 tff(func_def_366, type, g_s356_351: $int).
% 0.19/0.32 tff(func_def_367, type, g_s357_352: $int).
% 0.19/0.32 tff(func_def_368, type, g_s358_353: $int).
% 0.19/0.32 tff(func_def_369, type, g_s363_354: $int).
% 0.19/0.32 tff(func_def_370, type, g_s363_1_361: $int).
% 0.19/0.32 tff(func_def_371, type, g_s364_1_362: $int).
% 0.19/0.32 tff(func_def_372, type, g_s365_1_363: $int).
% 0.19/0.32 tff(func_def_373, type, g_s366_1_364: $int).
% 0.19/0.32 tff(func_def_374, type, g_s367_1_365: set_0).
% 0.19/0.32 tff(func_def_375, type, g_s368_1_366: set_0).
% 0.19/0.32 tff(func_def_376, type, g_s369_1_367: set_0).
% 0.19/0.32 tff(func_def_377, type, g_s370_1_368: set_0).
% 0.19/0.32 tff(func_def_378, type, g_s371_1_369: set_0).
% 0.19/0.32 tff(func_def_379, type, g_s373_1_370: set_4).
% 0.19/0.32 tff(func_def_380, type, g_s374_1_371: set_0).
% 0.19/0.32 tff(func_def_381, type, g_s375_1_372: set_4).
% 0.19/0.32 tff(func_def_394, type, sK4: set_3).
% 0.19/0.32 tff(func_def_395, type, sK5: ($int * $int) > $int).
% 0.19/0.32 tff(func_def_396, type, sK6: ($int * $int) > $int).
% 0.19/0.32 tff(func_def_397, type, sK7: set_3).
% 0.19/0.32 tff(func_def_398, type, sK8: ($int * $int) > $int).
% 0.19/0.32 tff(func_def_399, type, sK9: set_3).
% 0.19/0.32 tff(func_def_400, type, sK10: ($int * $int) > $int).
% 0.19/0.32 tff(func_def_401, type, sK11: ($int * $int) > $int).
% 0.19/0.32 tff(func_def_402, type, sK12: set_4).
% 0.19/0.32 tff(func_def_403, type, sK13: $int > $int).
% 0.19/0.32 tff(func_def_404, type, sK14: set_5).
% 0.19/0.32 tff(func_def_405, type, sK15: set_4 > set_4).
% 0.19/0.32 tff(func_def_406, type, sK16: $int > set_4).
% 0.19/0.32 tff(func_def_407, type, sK17: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_408, type, sK18: set_4).
% 0.19/0.32 tff(func_def_409, type, sK19: $int > $int).
% 0.19/0.32 tff(func_def_410, type, sK20: set_4).
% 0.19/0.32 tff(func_def_411, type, sK21: $int > $int).
% 0.19/0.32 tff(func_def_412, type, sK22: set_4).
% 0.19/0.32 tff(func_def_413, type, sK23: $int > $int).
% 0.19/0.32 tff(func_def_414, type, sK24: set_4).
% 0.19/0.32 tff(func_def_415, type, sK25: $int > $int).
% 0.19/0.32 tff(func_def_416, type, sK26: set_4).
% 0.19/0.32 tff(func_def_417, type, sK27: $int > $int).
% 0.19/0.32 tff(func_def_418, type, sK28: set_4).
% 0.19/0.32 tff(func_def_419, type, sK29: $int > $int).
% 0.19/0.32 tff(func_def_420, type, sK30: set_4).
% 0.19/0.32 tff(func_def_421, type, sK31: $int > $int).
% 0.19/0.32 tff(func_def_422, type, sK32: set_4).
% 0.19/0.32 tff(func_def_423, type, sK33: $int > $int).
% 0.19/0.32 tff(func_def_424, type, sK34: set_4).
% 0.19/0.32 tff(func_def_425, type, sK35: $int > $int).
% 0.19/0.32 tff(func_def_426, type, sK36: set_4).
% 0.19/0.32 tff(func_def_427, type, sK37: $int > $int).
% 0.19/0.32 tff(func_def_428, type, sK38: set_4).
% 0.19/0.32 tff(func_def_429, type, sK39: $int > $int).
% 0.19/0.32 tff(func_def_430, type, sK40: set_4).
% 0.19/0.32 tff(func_def_431, type, sK41: $int > $int).
% 0.19/0.32 tff(func_def_432, type, sK42: set_4).
% 0.19/0.32 tff(func_def_433, type, sK43: $int > $int).
% 0.19/0.32 tff(func_def_434, type, sK44: set_4).
% 0.19/0.32 tff(func_def_435, type, sK45: $int > $int).
% 0.19/0.32 tff(func_def_436, type, sK46: set_4).
% 0.19/0.32 tff(func_def_437, type, sK47: $int > $int).
% 0.19/0.32 tff(func_def_438, type, sK48: set_4).
% 0.19/0.32 tff(func_def_439, type, sK49: $int > $int).
% 0.19/0.32 tff(func_def_440, type, sK50: set_4).
% 0.19/0.32 tff(func_def_441, type, sK51: $int > $int).
% 0.19/0.32 tff(func_def_442, type, sK52: set_4).
% 0.19/0.32 tff(func_def_443, type, sK53: $int > $int).
% 0.19/0.32 tff(func_def_444, type, sK54: set_4).
% 0.19/0.32 tff(func_def_445, type, sK55: $int > $int).
% 0.19/0.32 tff(func_def_446, type, sK56: set_6).
% 0.19/0.32 tff(func_def_447, type, sK57: set_5 > set_5).
% 0.19/0.32 tff(func_def_448, type, sK58: $int > set_5).
% 0.19/0.32 tff(func_def_449, type, sK59: set_4 > set_4).
% 0.19/0.32 tff(func_def_450, type, sK60: (set_5 * $int) > set_4).
% 0.19/0.32 tff(func_def_451, type, sK61: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_452, type, sK62: set_5).
% 0.19/0.32 tff(func_def_453, type, sK63: set_4 > set_4).
% 0.19/0.32 tff(func_def_454, type, sK64: $int > set_4).
% 0.19/0.32 tff(func_def_455, type, sK65: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_456, type, sK66: set_5).
% 0.19/0.32 tff(func_def_457, type, sK67: set_4 > set_4).
% 0.19/0.32 tff(func_def_458, type, sK68: $int > set_4).
% 0.19/0.32 tff(func_def_459, type, sK69: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_460, type, sK70: set_5).
% 0.19/0.32 tff(func_def_461, type, sK71: set_4 > set_4).
% 0.19/0.32 tff(func_def_462, type, sK72: $int > set_4).
% 0.19/0.32 tff(func_def_463, type, sK73: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_464, type, sK74: set_5).
% 0.19/0.32 tff(func_def_465, type, sK75: set_4 > set_4).
% 0.19/0.32 tff(func_def_466, type, sK76: $int > set_4).
% 0.19/0.32 tff(func_def_467, type, sK77: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_468, type, sK78: set_5).
% 0.19/0.32 tff(func_def_469, type, sK79: set_4 > set_4).
% 0.19/0.32 tff(func_def_470, type, sK80: $int > set_4).
% 0.19/0.32 tff(func_def_471, type, sK81: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_472, type, sK82: set_5).
% 0.19/0.32 tff(func_def_473, type, sK83: set_4 > set_4).
% 0.19/0.32 tff(func_def_474, type, sK84: $int > set_4).
% 0.19/0.32 tff(func_def_475, type, sK85: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_476, type, sK86: set_5).
% 0.19/0.32 tff(func_def_477, type, sK87: set_4 > set_4).
% 0.19/0.32 tff(func_def_478, type, sK88: $int > set_4).
% 0.19/0.32 tff(func_def_479, type, sK89: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_480, type, sK90: set_6).
% 0.19/0.32 tff(func_def_481, type, sK91: set_5 > set_5).
% 0.19/0.32 tff(func_def_482, type, sK92: $int > set_5).
% 0.19/0.32 tff(func_def_483, type, sK93: set_4 > set_4).
% 0.19/0.32 tff(func_def_484, type, sK94: (set_5 * $int) > set_4).
% 0.19/0.32 tff(func_def_485, type, sK95: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_486, type, sK96: set_6).
% 0.19/0.32 tff(func_def_487, type, sK97: set_5 > set_5).
% 0.19/0.32 tff(func_def_488, type, sK98: $int > set_5).
% 0.19/0.32 tff(func_def_489, type, sK99: set_4 > set_4).
% 0.19/0.32 tff(func_def_490, type, sK100: (set_5 * $int) > set_4).
% 0.19/0.32 tff(func_def_491, type, sK101: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_492, type, sK102: set_4).
% 0.19/0.32 tff(func_def_493, type, sK103: $int > $int).
% 0.19/0.32 tff(func_def_494, type, sK104: set_5).
% 0.19/0.32 tff(func_def_495, type, sK105: set_4 > set_4).
% 0.19/0.32 tff(func_def_496, type, sK106: $int > set_4).
% 0.19/0.32 tff(func_def_497, type, sK107: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_498, type, sK108: set_4).
% 0.19/0.32 tff(func_def_499, type, sK109: $int > $int).
% 0.19/0.32 tff(func_def_500, type, sK110: set_4).
% 0.19/0.32 tff(func_def_501, type, sK111: $int > $int).
% 0.19/0.32 tff(func_def_502, type, sK112: set_4).
% 0.19/0.32 tff(func_def_503, type, sK113: $int > $int).
% 0.19/0.32 tff(func_def_504, type, sK114: set_4).
% 0.19/0.32 tff(func_def_505, type, sK115: $int > $int).
% 0.19/0.32 tff(func_def_506, type, sK116: set_4).
% 0.19/0.32 tff(func_def_507, type, sK117: $int > $int).
% 0.19/0.32 tff(func_def_508, type, sK118: set_4).
% 0.19/0.32 tff(func_def_509, type, sK119: $int > $int).
% 0.19/0.32 tff(func_def_510, type, sK120: set_4).
% 0.19/0.32 tff(func_def_511, type, sK121: $int > $int).
% 0.19/0.32 tff(func_def_512, type, sK122: set_5).
% 0.19/0.32 tff(func_def_513, type, sK123: set_4 > set_4).
% 0.19/0.32 tff(func_def_514, type, sK124: $int > set_4).
% 0.19/0.32 tff(func_def_515, type, sK125: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_516, type, sK126: set_5).
% 0.19/0.32 tff(func_def_517, type, sK127: set_4 > set_4).
% 0.19/0.32 tff(func_def_518, type, sK128: $int > set_4).
% 0.19/0.32 tff(func_def_519, type, sK129: (set_4 * $int) > $int).
% 0.19/0.32 tff(func_def_520, type, sK130: set_4).
% 0.19/0.32 tff(func_def_521, type, sK131: $int > $int).
% 0.19/0.32 tff(func_def_522, type, sK132: set_4).
% 0.19/0.32 tff(func_def_523, type, sK133: $int > $int).
% 0.19/0.32 tff(func_def_524, type, sK134: $int).
% 0.19/0.32 tff(func_def_525, type, sK135: $int).
% 0.19/0.32 tff(func_def_526, type, sK136: $int).
% 0.19/0.32 tff(func_def_527, type, sK137: $int).
% 0.19/0.32 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 0.19/0.32 tff(pred_def_2, type, mem2: ($o * $int * set_2) > $o).
% 0.19/0.32 tff(pred_def_3, type, mem3: ($int * $int * $int * set_3) > $o).
% 0.19/0.32 tff(pred_def_4, type, mem4: ($int * $int * set_4) > $o).
% 0.19/0.32 tff(pred_def_5, type, mem5: ($int * set_4 * set_5) > $o).
% 0.19/0.32 tff(pred_def_6, type, mem6: ($int * set_5 * set_6) > $o).
% 0.19/0.32 tff(pred_def_17, type, sP0: $o > $o).
% 0.19/0.32 tff(pred_def_19, type, sP2: $o > $o).
% 0.19/0.32 tff(f393,axiom,(
% 0.19/0.32 ! [X0 : $int] : (mem0(X0,g_s371_1_369) => ($greatereq(X0,1) & $lesseq(X0,g_s365_1_363)))),
% 0.19/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:inv:11')).
% 0.19/0.32 tff(f403,axiom,(
% 0.19/0.32 $greatereq(g_s365_1_363,0)),
% 0.19/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:inv:5')).
% 0.19/0.32 tff(f477,axiom,(
% 0.19/0.32 ~ ! [X0 : $int] : (X0 = $sum(g_s365_1_363,1) => mem0(X0,g_s370_1_368))),
% 0.19/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:6')).
% 0.19/0.32 tff(f478,conjecture,(
% 0.19/0.32 ! [X0 : $int] : ((mem0(X0,g_s371_1_369) | X0 = $sum(g_s365_1_363,1)) => ($greatereq(X0,1) & $lesseq(X0,$sum(g_s365_1_363,1))))),
% 0.19/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Goal')).
% 0.19/0.32 tff(f479,negated_conjecture,(
% 0.19/0.32 ~ ! [X0 : $int] : ((mem0(X0,g_s371_1_369) | X0 = $sum(g_s365_1_363,1)) => ($greatereq(X0,1) & $lesseq(X0,$sum(g_s365_1_363,1))))),
% 0.19/0.32 inference(negated_conjecture,[status(cth)],[f478])).
% 0.19/0.32 tff(f587,plain,(
% 0.19/0.32 ! [X0 : $int] : (mem0(X0,g_s371_1_369) => (~$less(X0,1) & ~$less(g_s365_1_363,X0)))),
% 0.19/0.32 inference(theory_normalization,[],[f393])).
% 0.19/0.32 tff(f592,plain,(
% 0.19/0.32 ~$less(g_s365_1_363,0)),
% 0.19/0.32 inference(theory_normalization,[],[f403])).
% 0.19/0.32 tff(f649,plain,(
% 0.19/0.32 ~ ! [X0 : $int] : ((mem0(X0,g_s371_1_369) | X0 = $sum(g_s365_1_363,1)) => (~$less(X0,1) & ~$less($sum(g_s365_1_363,1),X0)))),
% 0.19/0.32 inference(theory_normalization,[],[f479])).
% 0.19/0.32 tff(f655,definition,(
% 0.19/0.32 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 0.19/0.32 introduced(theory,[tha_non-reflexivity])).
% 0.19/0.32 tff(f656,definition,(
% 0.19/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 0.19/0.32 introduced(theory,[tha_transitivity])).
% 0.19/0.32 tff(f658,definition,(
% 0.19/0.32 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 0.19/0.32 introduced(theory,[tha_order_monotonicity])).
% 0.19/0.32 tff(f659,definition,(
% 0.19/0.32 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 0.19/0.32 introduced(theory,[tha_order_plus_one_dichotomy])).
% 0.19/0.32 tff(f667,definition,(
% 0.19/0.32 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 0.19/0.32 introduced(theory,[tha_extra_integer_ordering])).
% 0.19/0.32 tff(f683,plain,(
% 0.19/0.32 ! [X0 : $int] : ((~$less(X0,1) & ~$less(g_s365_1_363,X0)) | ~mem0(X0,g_s371_1_369))),
% 0.19/0.32 inference(ennf_transformation,[],[f587])).
% 0.19/0.32 tff(f793,plain,(
% 0.19/0.32 ? [X0 : $int] : (~mem0(X0,g_s370_1_368) & X0 = $sum(g_s365_1_363,1))),
% 0.19/0.32 inference(ennf_transformation,[],[f477])).
% 0.19/0.32 tff(f794,plain,(
% 0.19/0.32 ? [X0 : $int] : (($less(X0,1) | $less($sum(g_s365_1_363,1),X0)) & (mem0(X0,g_s371_1_369) | X0 = $sum(g_s365_1_363,1)))),
% 0.19/0.32 inference(ennf_transformation,[],[f649])).
% 0.19/0.32 tff(f1350,plain,(
% 0.19/0.32 ( ! [X0 : $int] : (~$less(g_s365_1_363,X0) | ~mem0(X0,g_s371_1_369)) )),
% 0.19/0.32 inference(cnf_transformation,[],[f683])).
% 0.19/0.32 tff(f1351,plain,(
% 0.19/0.32 ( ! [X0 : $int] : (~$less(X0,1) | ~mem0(X0,g_s371_1_369)) )),
% 0.19/0.32 inference(cnf_transformation,[],[f683])).
% 0.19/0.32 tff(f1370,plain,(
% 0.19/0.32 ~$less(g_s365_1_363,0)),
% 0.19/0.32 inference(cnf_transformation,[],[f592])).
% 0.19/0.32 tff(f1834,plain,(
% 0.19/0.32 $sum(g_s365_1_363,1) = sK136),
% 0.19/0.32 inference(cnf_transformation,[],[f793])).
% 0.19/0.32 tff(f1836,plain,(
% 0.19/0.32 $less($sum(g_s365_1_363,1),sK137) | $less(sK137,1)),
% 0.19/0.32 inference(cnf_transformation,[],[f794])).
% 0.19/0.32 tff(f1837,plain,(
% 0.19/0.32 $sum(g_s365_1_363,1) = sK137 | mem0(sK137,g_s371_1_369)),
% 0.19/0.32 inference(cnf_transformation,[],[f794])).
% 0.19/0.32 tff(f2387,definition,(
% 0.19/0.32 spl138_1 <=> $less(sK137,1)),
% 0.19/0.32 introduced(definition,[new_symbols(definition,[spl138_1])],[avatar_definition])).
% 0.19/0.32 tff(f2389,plain,(
% 0.19/0.32 $less(sK137,1) | ~spl138_1),
% 0.19/0.32 inference(avatar_component_clause,[],[f2387])).
% 0.19/0.32 tff(f2391,definition,(
% 0.19/0.32 spl138_2 <=> $less($sum(g_s365_1_363,1),sK137)),
% 0.19/0.32 introduced(definition,[new_symbols(definition,[spl138_2])],[avatar_definition])).
% 0.19/0.32 tff(f2393,plain,(
% 0.19/0.32 $less($sum(g_s365_1_363,1),sK137) | ~spl138_2),
% 0.19/0.32 inference(avatar_component_clause,[],[f2391])).
% 0.19/0.32 tff(f2394,plain,(
% 0.19/0.32 spl138_1 | spl138_2),
% 0.19/0.32 inference(avatar_split_clause,[],[f1836,f2391,f2387])).
% 0.19/0.32 tff(f2396,definition,(
% 0.19/0.32 spl138_3 <=> mem0(sK137,g_s371_1_369)),
% 0.19/0.32 introduced(definition,[new_symbols(definition,[spl138_3])],[avatar_definition])).
% 0.19/0.32 tff(f2398,plain,(
% 0.19/0.32 mem0(sK137,g_s371_1_369) | ~spl138_3),
% 0.19/0.32 inference(avatar_component_clause,[],[f2396])).
% 0.19/0.32 tff(f2400,definition,(
% 0.19/0.32 spl138_4 <=> $sum(g_s365_1_363,1) = sK137),
% 0.19/0.32 introduced(definition,[new_symbols(definition,[spl138_4])],[avatar_definition])).
% 0.19/0.32 tff(f2402,plain,(
% 0.19/0.32 $sum(g_s365_1_363,1) = sK137 | ~spl138_4),
% 0.19/0.32 inference(avatar_component_clause,[],[f2400])).
% 0.19/0.32 tff(f2403,plain,(
% 0.19/0.32 spl138_3 | spl138_4),
% 0.19/0.32 inference(avatar_split_clause,[],[f1837,f2400,f2396])).
% 0.19/0.32 tff(f2697,plain,(
% 0.19/0.32 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 0.19/0.32 inference(resolution,[],[f659,f655])).
% 0.19/0.32 tff(f2849,plain,(
% 0.19/0.32 $less(g_s365_1_363,sK136)),
% 0.19/0.32 inference(superposition,[],[f2697,f1834])).
% 0.19/0.32 tff(f2946,plain,(
% 0.19/0.32 ( ! [X0 : $int] : (~$less(X0,$sum(g_s365_1_363,1)) | $less(X0,sK137)) ) | ~spl138_2),
% 0.19/0.32 inference(resolution,[],[f656,f2393])).
% 0.19/0.32 tff(f2950,plain,(
% 0.19/0.32 ( ! [X0 : $int] : (~$less(X0,sK136) | $less(X0,sK137)) ) | ~spl138_2),
% 0.19/0.32 inference(forward_demodulation,[],[f2946,f1834])).
% 0.19/0.32 tff(f4132,plain,(
% 0.19/0.32 $less(g_s365_1_363,sK137) | ~spl138_2),
% 0.19/0.32 inference(resolution,[],[f2950,f2849])).
% 0.19/0.32 tff(f4134,plain,(
% 0.19/0.32 ~mem0(sK137,g_s371_1_369) | ~spl138_2),
% 0.19/0.32 inference(resolution,[],[f4132,f1350])).
% 0.19/0.32 tff(f4141,plain,(
% 0.19/0.32 ~mem0(sK137,g_s371_1_369) | ~spl138_1),
% 0.19/0.32 inference(resolution,[],[f2389,f1351])).
% 0.19/0.32 tff(f4153,plain,(
% 0.19/0.32 $false | (~spl138_1 | ~spl138_3)),
% 0.19/0.32 inference(forward_subsumption_resolution,[],[f4141,f2398])).
% 0.19/0.32 tff(f4154,plain,(
% 0.19/0.32 ~spl138_1 | ~spl138_3),
% 0.19/0.32 inference(avatar_contradiction_clause,[],[f4153])).
% 0.19/0.32 tff(f4155,plain,(
% 0.19/0.32 $less(sK136,sK137) | ~spl138_2),
% 0.19/0.32 inference(forward_demodulation,[],[f2393,f1834])).
% 0.19/0.32 tff(f4157,plain,(
% 0.19/0.32 ~spl138_3 | ~spl138_2),
% 0.19/0.32 inference(avatar_split_clause,[],[f4134,f2391,f2396])).
% 0.19/0.32 tff(f4159,plain,(
% 0.19/0.32 sK136 = sK137 | ~spl138_4),
% 0.19/0.32 inference(superposition,[],[f2402,f1834])).
% 0.19/0.32 tff(f4166,plain,(
% 0.19/0.32 ( ! [X0 : $int] : ($less(X0,sK137) | $less(g_s365_1_363,X0)) ) | ~spl138_4),
% 0.19/0.32 inference(superposition,[],[f659,f2402])).
% 0.19/0.32 tff(f4197,plain,(
% 0.19/0.32 $less(sK137,sK137) | (~spl138_2 | ~spl138_4)),
% 0.19/0.32 inference(superposition,[],[f4155,f4159])).
% 0.19/0.32 tff(f4198,plain,(
% 0.19/0.32 $false | (~spl138_2 | ~spl138_4)),
% 0.19/0.32 inference(forward_subsumption_resolution,[],[f4197,f655])).
% 0.19/0.32 tff(f4199,plain,(
% 0.19/0.32 ~spl138_2 | ~spl138_4),
% 0.19/0.32 inference(avatar_contradiction_clause,[],[f4198])).
% 0.19/0.32 tff(f4732,plain,(
% 0.19/0.32 $less(0,sK137) | ~spl138_4),
% 0.19/0.32 inference(resolution,[],[f4166,f1370])).
% 0.19/0.32 tff(f4801,definition,(
% 0.19/0.32 spl138_188 <=> $less(0,sK137)),
% 0.19/0.32 introduced(definition,[new_symbols(definition,[spl138_188])],[avatar_definition])).
% 0.19/0.32 tff(f4803,plain,(
% 0.19/0.32 $less(0,sK137) | ~spl138_188),
% 0.19/0.32 inference(avatar_component_clause,[],[f4801])).
% 0.19/0.32 tff(f4992,plain,(
% 0.19/0.32 spl138_188 | ~spl138_4),
% 0.19/0.32 inference(avatar_split_clause,[],[f4732,f2400,f4801])).
% 0.19/0.32 tff(f5011,plain,(
% 0.19/0.32 ( ! [X0 : $int] : ($less($sum(0,X0),$sum(sK137,X0))) ) | ~spl138_188),
% 0.19/0.32 inference(resolution,[],[f4803,f658])).
% 0.19/0.32 tff(f5013,plain,(
% 0.19/0.32 ( ! [X0 : $int] : ($less(X0,$sum(sK137,X0))) ) | ~spl138_188),
% 0.19/0.32 inference(evaluation,[],[f5011])).
% 0.19/0.32 tff(f5059,plain,(
% 0.19/0.32 ~$less(sK137,1) | ~spl138_188),
% 0.19/0.32 inference(resolution,[],[f5013,f667])).
% 0.19/0.32 tff(f5179,plain,(
% 0.19/0.32 $false | (~spl138_1 | ~spl138_188)),
% 0.19/0.32 inference(forward_subsumption_resolution,[],[f5059,f2389])).
% 0.19/0.32 tff(f5180,plain,(
% 0.19/0.32 ~spl138_1 | ~spl138_188),
% 0.19/0.32 inference(avatar_contradiction_clause,[],[f5179])).
% 0.19/0.32 cnf(s1, plain, spl138_1 | spl138_2, inference(sat_conversion,[],[f2394])).
% 0.19/0.32 cnf(s2, plain, spl138_3 | spl138_4, inference(sat_conversion,[],[f2403])).
% 0.19/0.32 cnf(s201, plain, ~spl138_1 | ~spl138_3, inference(sat_conversion,[],[f4154])).
% 0.19/0.32 cnf(s202, plain, ~spl138_2 | ~spl138_3, inference(sat_conversion,[],[f4157])).
% 0.19/0.32 cnf(s204, plain, ~spl138_2 | ~spl138_4, inference(sat_conversion,[],[f4199])).
% 0.19/0.32 cnf(s254, plain, ~spl138_4 | spl138_188, inference(sat_conversion,[],[f4992])).
% 0.19/0.32 cnf(s259, plain, ~spl138_1 | ~spl138_188, inference(sat_conversion,[],[f5180])).
% 0.19/0.32 cnf(s266, plain, ~spl138_2, inference(rat,[],[s2,s202,s204])).
% 0.19/0.32 cnf(s267, plain, spl138_1, inference(rat,[],[s1,s266])).
% 0.19/0.32 cnf(s268, plain, ~spl138_188, inference(rat,[],[s259,s267])).
% 0.19/0.32 cnf(s269, plain, ~spl138_3, inference(rat,[],[s201,s267])).
% 0.19/0.32 cnf(s270, plain, ~spl138_4, inference(rat,[],[s254,s268])).
% 0.19/0.32 cnf(s271, plain, $false, inference(rat,[],[s2,s270,s269])).
% 0.19/0.32 tff(f5181,plain,(
% 0.19/0.32 $false),
% 0.19/0.32 inference(avatar_sat_refutation,[],[s271])).
% 0.19/0.32 % SZS output end Proof for theBenchmark
% 0.19/0.32 % (241895)------------------------------
% 0.19/0.32 % (241895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.32 % (241895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.32 % (241895)CaDiCaL version: 2.1.3
% 0.19/0.32 % (241895)Termination reason: Refutation
% 0.19/0.32 % (241895)Time elapsed: 0.052 s
% 0.19/0.32 % (241895)Peak memory usage: 16 MB
% 0.19/0.32 % (241895)Instructions burned: 171 (million)
% 0.19/0.32 % (241880)Success in time 0.098 s
% 0.19/0.32 % Vampire exiting
%------------------------------------------------------------------------------