%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC522_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:04:10 PM UTC 2026
% Result : Theorem 9.06s 2.30s
% Output : Refutation 9.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 21
% Syntax : Number of formulae : 153 ( 31 unt; 0 typ; 16 def)
% Number of atoms : 620 ( 181 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 452 ( 168 ~; 165 |; 54 &)
% ( 41 <=>; 23 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 339 ( 196 fml; 143 var)
% Number arithmetic : 149 ( 0 atm; 31 fun; 31 num; 87 var)
% Number of types : 6 ( 4 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 32 usr; 15 prp; 0-4 aty)
% Number of functors : 459 ( 457 usr; 403 con; 0-2 aty)
% Number of variables : 147 ( 0 sgn 119 !; 28 ?; 147 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
set_0: $tType ).
tff(type_def_6,type,
set_2: $tType ).
tff(type_def_7,type,
set_3: $tType ).
tff(type_def_8,type,
set_4: $tType ).
tff(func_def_0,type,
min_int: $int ).
tff(func_def_1,type,
max_int: $int ).
tff(func_def_5,type,
divB: ( $int * $int ) > $int ).
tff(func_def_8,type,
g_s0_0: set_0 ).
tff(func_def_9,type,
g_s1_1: $int ).
tff(func_def_10,type,
g_s2_2: $int ).
tff(func_def_11,type,
g_s3_3: set_0 ).
tff(func_def_12,type,
g_s4_4: $int ).
tff(func_def_13,type,
g_s5_5: $int ).
tff(func_def_14,type,
g_s6_6: set_0 ).
tff(func_def_15,type,
g_s7_7: $int ).
tff(func_def_16,type,
g_s8_8: $int ).
tff(func_def_17,type,
g_s9_9: set_0 ).
tff(func_def_18,type,
g_s10_10: $int ).
tff(func_def_19,type,
g_s11_11: $int ).
tff(func_def_20,type,
g_s12_12: $int ).
tff(func_def_21,type,
g_s13_13: $int ).
tff(func_def_22,type,
g_s14_14: $int ).
tff(func_def_23,type,
g_s15_15: $int ).
tff(func_def_24,type,
g_s16_16: $int ).
tff(func_def_25,type,
g_s17_17: $int ).
tff(func_def_26,type,
g_s18_18: $int ).
tff(func_def_27,type,
g_s19_19: set_0 ).
tff(func_def_28,type,
g_s20_20: $int ).
tff(func_def_29,type,
g_s21_21: $int ).
tff(func_def_30,type,
g_s22_22: set_0 ).
tff(func_def_31,type,
g_s23_23: $int ).
tff(func_def_32,type,
g_s24_24: $int ).
tff(func_def_33,type,
g_s25_25: $int ).
tff(func_def_34,type,
g_s26_26: $int ).
tff(func_def_35,type,
g_s27_27: $int ).
tff(func_def_36,type,
g_s28_28: $int ).
tff(func_def_37,type,
g_s29_29: $int ).
tff(func_def_38,type,
g_s30_30: $int ).
tff(func_def_39,type,
g_s31_31: $int ).
tff(func_def_40,type,
g_s33_32: set_0 ).
tff(func_def_41,type,
g_s32_33: $int ).
tff(func_def_42,type,
g_s35_34: set_0 ).
tff(func_def_43,type,
g_s34_35: $int ).
tff(func_def_44,type,
g_s37_36: set_0 ).
tff(func_def_45,type,
g_s36_37: $int ).
tff(func_def_46,type,
g_s38_38: $int ).
tff(func_def_47,type,
g_s39_39: $int ).
tff(func_def_48,type,
g_s40_40: set_0 ).
tff(func_def_49,type,
set_2_empty: set_2 ).
tff(func_def_50,type,
set_2_insert: set_2 > set_2 ).
tff(func_def_51,type,
g_s41_41: set_2 ).
tff(func_def_52,type,
set_3_empty: set_3 ).
tff(func_def_53,type,
set_3_insert: set_3 > set_3 ).
tff(func_def_54,type,
g_s42_42: set_3 ).
tff(func_def_55,type,
set_4_empty: set_4 ).
tff(func_def_56,type,
set_4_insert: set_4 > set_4 ).
tff(func_def_57,type,
g_s43_43: set_4 ).
tff(func_def_58,type,
g_s44_44: set_4 ).
tff(func_def_59,type,
g_s45_45: set_3 ).
tff(func_def_60,type,
g_s46_46: set_4 ).
tff(func_def_61,type,
g_s47_47: set_4 ).
tff(func_def_62,type,
g_s48_48: set_3 ).
tff(func_def_63,type,
g_s49_49: set_4 ).
tff(func_def_64,type,
g_s50_50: set_4 ).
tff(func_def_65,type,
g_s51_51: set_4 ).
tff(func_def_66,type,
g_s52_52: set_4 ).
tff(func_def_67,type,
g_s53_53: set_4 ).
tff(func_def_68,type,
g_s54_54: set_4 ).
tff(func_def_69,type,
g_s55_55: set_4 ).
tff(func_def_70,type,
g_s56_56: set_4 ).
tff(func_def_71,type,
g_s57_57: set_4 ).
tff(func_def_72,type,
g_s58_58: set_4 ).
tff(func_def_73,type,
g_s59_59: set_4 ).
tff(func_def_74,type,
g_s60_60: set_4 ).
tff(func_def_75,type,
g_s66_61: $int ).
tff(func_def_76,type,
g_s67_62: $int ).
tff(func_def_77,type,
g_s68_63: $int ).
tff(func_def_78,type,
g_s69_64: $int ).
tff(func_def_79,type,
g_s70_65: $int ).
tff(func_def_80,type,
g_s71_66: $int ).
tff(func_def_81,type,
g_s72_67: $int ).
tff(func_def_82,type,
g_s73_68: $int ).
tff(func_def_83,type,
g_s74_69: $int ).
tff(func_def_84,type,
g_s75_70: $int ).
tff(func_def_85,type,
g_s76_71: $int ).
tff(func_def_86,type,
g_s77_72: $int ).
tff(func_def_87,type,
g_s78_73: $int ).
tff(func_def_88,type,
g_s79_74: $int ).
tff(func_def_89,type,
g_s80_75: $int ).
tff(func_def_90,type,
g_s81_76: $int ).
tff(func_def_91,type,
g_s82_77: $int ).
tff(func_def_92,type,
g_s83_78: $int ).
tff(func_def_93,type,
g_s84_79: $int ).
tff(func_def_94,type,
g_s85_80: $int ).
tff(func_def_95,type,
g_s86_81: $int ).
tff(func_def_96,type,
g_s87_82: $int ).
tff(func_def_97,type,
g_s88_83: $int ).
tff(func_def_98,type,
g_s89_84: $int ).
tff(func_def_99,type,
g_s90_85: $int ).
tff(func_def_100,type,
g_s91_86: $int ).
tff(func_def_101,type,
g_s92_87: $int ).
tff(func_def_102,type,
g_s93_88: $int ).
tff(func_def_103,type,
g_s94_89: $int ).
tff(func_def_104,type,
g_s95_90: $int ).
tff(func_def_105,type,
g_s96_91: $int ).
tff(func_def_106,type,
g_s97_92: $int ).
tff(func_def_107,type,
g_s98_93: $int ).
tff(func_def_108,type,
g_s99_94: $int ).
tff(func_def_109,type,
g_s100_95: $int ).
tff(func_def_110,type,
g_s101_96: $int ).
tff(func_def_111,type,
g_s102_97: $int ).
tff(func_def_112,type,
g_s103_98: $int ).
tff(func_def_113,type,
g_s104_99: $int ).
tff(func_def_114,type,
g_s105_100: $int ).
tff(func_def_115,type,
g_s106_101: $int ).
tff(func_def_116,type,
g_s107_102: $int ).
tff(func_def_117,type,
g_s108_103: $int ).
tff(func_def_118,type,
g_s109_104: $int ).
tff(func_def_119,type,
g_s110_105: $int ).
tff(func_def_120,type,
g_s111_106: $int ).
tff(func_def_121,type,
g_s112_107: $int ).
tff(func_def_122,type,
g_s113_108: $int ).
tff(func_def_123,type,
g_s114_109: $int ).
tff(func_def_124,type,
g_s115_110: $int ).
tff(func_def_125,type,
g_s116_111: $int ).
tff(func_def_126,type,
g_s117_112: $int ).
tff(func_def_127,type,
g_s118_113: $int ).
tff(func_def_128,type,
g_s119_114: $int ).
tff(func_def_129,type,
g_s120_115: $int ).
tff(func_def_130,type,
g_s121_116: $int ).
tff(func_def_131,type,
g_s122_117: $int ).
tff(func_def_132,type,
g_s123_118: $int ).
tff(func_def_133,type,
g_s124_119: $int ).
tff(func_def_134,type,
g_s125_120: $int ).
tff(func_def_135,type,
g_s126_121: $int ).
tff(func_def_136,type,
g_s127_122: $int ).
tff(func_def_137,type,
g_s128_123: $int ).
tff(func_def_138,type,
g_s129_124: $int ).
tff(func_def_139,type,
g_s130_125: $int ).
tff(func_def_140,type,
g_s131_126: $int ).
tff(func_def_141,type,
g_s132_127: $int ).
tff(func_def_142,type,
g_s133_128: $int ).
tff(func_def_143,type,
g_s134_129: $int ).
tff(func_def_144,type,
g_s135_130: $int ).
tff(func_def_145,type,
g_s136_131: $int ).
tff(func_def_146,type,
g_s137_132: $int ).
tff(func_def_147,type,
g_s138_133: $int ).
tff(func_def_148,type,
g_s139_134: $int ).
tff(func_def_149,type,
g_s140_135: $int ).
tff(func_def_150,type,
g_s141_136: $int ).
tff(func_def_151,type,
g_s142_137: $int ).
tff(func_def_152,type,
g_s143_138: $int ).
tff(func_def_153,type,
g_s144_139: $int ).
tff(func_def_154,type,
g_s145_140: $int ).
tff(func_def_155,type,
g_s146_141: $int ).
tff(func_def_156,type,
g_s147_142: $int ).
tff(func_def_157,type,
g_s148_143: $int ).
tff(func_def_158,type,
g_s149_144: $int ).
tff(func_def_159,type,
g_s150_145: $int ).
tff(func_def_160,type,
g_s151_146: $int ).
tff(func_def_161,type,
g_s152_147: $int ).
tff(func_def_162,type,
g_s153_148: $int ).
tff(func_def_163,type,
g_s154_149: $int ).
tff(func_def_164,type,
g_s155_150: $int ).
tff(func_def_165,type,
g_s156_151: $int ).
tff(func_def_166,type,
g_s157_152: $int ).
tff(func_def_167,type,
g_s158_153: $int ).
tff(func_def_168,type,
g_s159_154: $int ).
tff(func_def_169,type,
g_s160_155: $int ).
tff(func_def_170,type,
g_s161_156: $int ).
tff(func_def_171,type,
g_s162_157: $int ).
tff(func_def_172,type,
g_s163_158: $int ).
tff(func_def_173,type,
g_s164_159: $int ).
tff(func_def_174,type,
g_s165_160: $int ).
tff(func_def_175,type,
g_s166_161: $int ).
tff(func_def_176,type,
g_s167_162: $int ).
tff(func_def_177,type,
g_s168_163: $int ).
tff(func_def_178,type,
g_s169_164: $int ).
tff(func_def_179,type,
g_s170_165: $int ).
tff(func_def_180,type,
g_s171_166: $int ).
tff(func_def_181,type,
g_s172_167: $int ).
tff(func_def_182,type,
g_s173_168: $int ).
tff(func_def_183,type,
g_s174_169: $int ).
tff(func_def_184,type,
g_s175_170: $int ).
tff(func_def_185,type,
g_s176_171: $int ).
tff(func_def_186,type,
g_s177_172: $int ).
tff(func_def_187,type,
g_s178_173: $int ).
tff(func_def_188,type,
g_s179_174: $int ).
tff(func_def_189,type,
g_s180_175: $int ).
tff(func_def_190,type,
g_s181_176: $int ).
tff(func_def_191,type,
g_s182_177: $int ).
tff(func_def_192,type,
g_s183_178: $int ).
tff(func_def_193,type,
g_s184_179: $int ).
tff(func_def_194,type,
g_s185_180: set_0 ).
tff(func_def_195,type,
g_s186_181: set_0 ).
tff(func_def_196,type,
g_s187_182: $int ).
tff(func_def_197,type,
g_s188_183: $int ).
tff(func_def_198,type,
g_s189_184: $int ).
tff(func_def_199,type,
g_s190_185: $int ).
tff(func_def_200,type,
g_s191_186: $int ).
tff(func_def_201,type,
g_s192_187: $int ).
tff(func_def_202,type,
g_s193_188: $int ).
tff(func_def_203,type,
g_s194_189: $int ).
tff(func_def_204,type,
g_s195_190: $int ).
tff(func_def_205,type,
g_s196_191: $int ).
tff(func_def_206,type,
g_s197_192: $int ).
tff(func_def_207,type,
g_s198_193: $int ).
tff(func_def_208,type,
g_s199_194: $int ).
tff(func_def_209,type,
g_s200_195: $int ).
tff(func_def_210,type,
g_s201_196: $int ).
tff(func_def_211,type,
g_s202_197: $int ).
tff(func_def_212,type,
g_s203_198: $int ).
tff(func_def_213,type,
g_s204_199: $int ).
tff(func_def_214,type,
g_s205_200: $int ).
tff(func_def_215,type,
g_s206_201: $int ).
tff(func_def_216,type,
g_s207_202: $int ).
tff(func_def_217,type,
g_s208_203: $int ).
tff(func_def_218,type,
g_s209_204: $int ).
tff(func_def_219,type,
g_s210_205: $int ).
tff(func_def_220,type,
g_s211_206: $int ).
tff(func_def_221,type,
g_s212_207: $int ).
tff(func_def_222,type,
g_s213_208: $int ).
tff(func_def_223,type,
g_s214_209: $int ).
tff(func_def_224,type,
g_s215_210: $int ).
tff(func_def_225,type,
g_s216_211: $int ).
tff(func_def_226,type,
g_s217_212: $int ).
tff(func_def_227,type,
g_s218_213: $int ).
tff(func_def_228,type,
g_s219_214: $int ).
tff(func_def_229,type,
g_s220_215: $int ).
tff(func_def_230,type,
g_s221_216: $int ).
tff(func_def_231,type,
g_s222_217: $int ).
tff(func_def_232,type,
g_s223_218: $int ).
tff(func_def_233,type,
g_s224_219: $int ).
tff(func_def_234,type,
g_s225_220: $int ).
tff(func_def_235,type,
g_s226_221: $int ).
tff(func_def_236,type,
g_s227_222: $int ).
tff(func_def_237,type,
g_s228_223: $int ).
tff(func_def_238,type,
g_s229_224: $int ).
tff(func_def_239,type,
g_s230_225: $int ).
tff(func_def_240,type,
g_s231_226: $int ).
tff(func_def_241,type,
g_s232_227: $int ).
tff(func_def_242,type,
g_s233_228: $int ).
tff(func_def_243,type,
g_s234_229: $int ).
tff(func_def_244,type,
g_s235_230: $int ).
tff(func_def_245,type,
g_s236_231: $int ).
tff(func_def_246,type,
g_s237_232: $int ).
tff(func_def_247,type,
g_s238_233: $int ).
tff(func_def_248,type,
g_s239_234: $int ).
tff(func_def_249,type,
g_s240_235: $int ).
tff(func_def_250,type,
g_s241_236: $int ).
tff(func_def_251,type,
g_s242_237: $int ).
tff(func_def_252,type,
g_s243_238: $int ).
tff(func_def_253,type,
g_s244_239: $int ).
tff(func_def_254,type,
g_s245_240: $int ).
tff(func_def_255,type,
g_s246_241: $int ).
tff(func_def_256,type,
g_s247_242: $int ).
tff(func_def_257,type,
g_s248_243: $int ).
tff(func_def_258,type,
g_s249_244: $int ).
tff(func_def_259,type,
g_s250_245: $int ).
tff(func_def_260,type,
g_s251_246: $int ).
tff(func_def_261,type,
g_s252_247: $int ).
tff(func_def_262,type,
g_s253_248: $int ).
tff(func_def_263,type,
g_s254_249: $int ).
tff(func_def_264,type,
g_s255_250: $int ).
tff(func_def_265,type,
g_s256_251: $int ).
tff(func_def_266,type,
g_s257_252: $int ).
tff(func_def_267,type,
g_s258_253: $int ).
tff(func_def_268,type,
g_s259_254: $int ).
tff(func_def_269,type,
g_s260_255: $int ).
tff(func_def_270,type,
g_s261_256: $int ).
tff(func_def_271,type,
g_s262_257: $int ).
tff(func_def_272,type,
g_s263_258: $int ).
tff(func_def_273,type,
g_s264_259: $int ).
tff(func_def_274,type,
g_s265_260: $int ).
tff(func_def_275,type,
g_s266_261: $int ).
tff(func_def_276,type,
g_s267_262: $int ).
tff(func_def_277,type,
g_s268_263: $int ).
tff(func_def_278,type,
g_s269_264: $int ).
tff(func_def_279,type,
g_s270_265: $int ).
tff(func_def_280,type,
g_s271_266: $int ).
tff(func_def_281,type,
g_s272_267: $int ).
tff(func_def_282,type,
g_s273_268: $int ).
tff(func_def_283,type,
g_s274_269: $int ).
tff(func_def_284,type,
g_s275_270: $int ).
tff(func_def_285,type,
g_s276_271: $int ).
tff(func_def_286,type,
g_s277_272: $int ).
tff(func_def_287,type,
g_s278_273: $int ).
tff(func_def_288,type,
g_s279_274: $int ).
tff(func_def_289,type,
g_s280_275: $int ).
tff(func_def_290,type,
g_s281_276: $int ).
tff(func_def_291,type,
g_s282_277: $int ).
tff(func_def_292,type,
g_s283_278: $int ).
tff(func_def_293,type,
g_s284_279: $int ).
tff(func_def_294,type,
g_s285_280: $int ).
tff(func_def_295,type,
g_s286_281: $int ).
tff(func_def_296,type,
g_s287_282: $int ).
tff(func_def_297,type,
g_s288_283: $int ).
tff(func_def_298,type,
g_s289_284: $int ).
tff(func_def_299,type,
g_s290_285: $int ).
tff(func_def_300,type,
g_s291_286: $int ).
tff(func_def_301,type,
g_s292_287: $int ).
tff(func_def_302,type,
g_s293_288: $int ).
tff(func_def_303,type,
g_s294_289: $int ).
tff(func_def_304,type,
g_s295_290: $int ).
tff(func_def_305,type,
g_s296_291: $int ).
tff(func_def_306,type,
g_s297_292: $int ).
tff(func_def_307,type,
g_s298_293: $int ).
tff(func_def_308,type,
g_s299_294: $int ).
tff(func_def_309,type,
g_s300_295: $int ).
tff(func_def_310,type,
g_s301_296: set_4 ).
tff(func_def_311,type,
g_s302_297: set_3 ).
tff(func_def_312,type,
g_s303_298: set_4 ).
tff(func_def_313,type,
g_s304_299: set_3 ).
tff(func_def_314,type,
g_s305_300: set_4 ).
tff(func_def_315,type,
g_s322_301: set_4 ).
tff(func_def_316,type,
g_s323_302: set_4 ).
tff(func_def_317,type,
g_s328_1_336: set_4 ).
tff(func_def_318,type,
g_s329_1_337: set_4 ).
tff(func_def_319,type,
g_s331_1_338: set_4 ).
tff(func_def_320,type,
g_s332_1_339: set_4 ).
tff(func_def_321,type,
g_s339_1_340: set_0 ).
tff(func_def_322,type,
g_s340_1_341: set_0 ).
tff(func_def_323,type,
g_s326_1_342: $int ).
tff(func_def_324,type,
g_s335_1_343: set_3 ).
tff(func_def_325,type,
g_s336_1_344: set_3 ).
tff(func_def_326,type,
g_s337_1_345: set_3 ).
tff(func_def_327,type,
g_s338_1_346: set_3 ).
tff(func_def_328,type,
g_s306_303: set_0 ).
tff(func_def_329,type,
g_s307_304: set_0 ).
tff(func_def_330,type,
g_s308_305: set_0 ).
tff(func_def_331,type,
g_s309_306: set_0 ).
tff(func_def_332,type,
g_s310_307: set_3 ).
tff(func_def_333,type,
g_s311_308: set_3 ).
tff(func_def_334,type,
g_s312_309: set_3 ).
tff(func_def_335,type,
g_s313_310: set_3 ).
tff(func_def_336,type,
g_s314_311: set_0 ).
tff(func_def_337,type,
g_s315_312: set_0 ).
tff(func_def_338,type,
g_s316_313: set_0 ).
tff(func_def_339,type,
g_s317_314: set_0 ).
tff(func_def_340,type,
g_s318_315: set_3 ).
tff(func_def_341,type,
g_s319_316: set_3 ).
tff(func_def_342,type,
g_s320_317: set_0 ).
tff(func_def_343,type,
g_s321_318: set_3 ).
tff(func_def_344,type,
g_s326_325: $int ).
tff(func_def_345,type,
g_s328_319: set_4 ).
tff(func_def_346,type,
g_s329_320: set_4 ).
tff(func_def_347,type,
g_s331_321: set_4 ).
tff(func_def_348,type,
g_s332_322: set_4 ).
tff(func_def_349,type,
g_s335_326: set_3 ).
tff(func_def_350,type,
g_s336_327: set_3 ).
tff(func_def_351,type,
g_s337_328: set_3 ).
tff(func_def_352,type,
g_s338_329: set_3 ).
tff(func_def_353,type,
g_s339_323: set_0 ).
tff(func_def_354,type,
g_s340_324: set_0 ).
tff(func_def_355,type,
g_s358_335: $int ).
tff(func_def_356,type,
g_s369_361: $int ).
tff(func_def_357,type,
g_s369_1_362: $int ).
tff(func_def_358,type,
g_s375_364: $int ).
tff(func_def_372,type,
bG0: $o > $o ).
tff(func_def_373,type,
bG1: $o > $o ).
tff(func_def_374,type,
bG2: $o > $o ).
tff(func_def_375,type,
bG3: $o > $o ).
tff(func_def_376,type,
bG4: $o > $o ).
tff(func_def_377,type,
bG5: $o > $o ).
tff(func_def_378,type,
bG6: $o > $o ).
tff(func_def_379,type,
bG7: $o > $o ).
tff(func_def_380,type,
bG8: $o > $o ).
tff(func_def_381,type,
bG9: $o > $o ).
tff(func_def_382,type,
bG10: $o > $o ).
tff(func_def_383,type,
bG11: $o > $o ).
tff(func_def_384,type,
bG12: $o > $o ).
tff(func_def_385,type,
bG13: $o > $o ).
tff(func_def_386,type,
sK14: set_4 ).
tff(func_def_387,type,
sK15: ( $int * $int ) > $int ).
tff(func_def_388,type,
sK16: set_4 ).
tff(func_def_389,type,
sK17: ( $int * $int ) > $int ).
tff(func_def_390,type,
sK18: set_4 ).
tff(func_def_391,type,
sK19: ( $int * $int ) > $int ).
tff(func_def_392,type,
sK20: set_4 ).
tff(func_def_393,type,
sK21: ( $int * $int ) > $int ).
tff(func_def_394,type,
sK22: set_4 ).
tff(func_def_395,type,
sK23: ( $int * $int ) > $int ).
tff(func_def_396,type,
sK24: set_4 ).
tff(func_def_397,type,
sK25: ( $int * $int ) > $int ).
tff(func_def_398,type,
sK26: set_3 ).
tff(func_def_399,type,
sK27: $int > $int ).
tff(func_def_400,type,
sK28: set_4 ).
tff(func_def_401,type,
sK29: ( $int * $int ) > $int ).
tff(func_def_402,type,
sK30: set_4 ).
tff(func_def_403,type,
sK31: ( $int * $int ) > $int ).
tff(func_def_404,type,
sK32: set_4 ).
tff(func_def_405,type,
sK33: ( $int * $int ) > $int ).
tff(func_def_406,type,
sK34: $int ).
tff(func_def_407,type,
sK35: set_4 ).
tff(func_def_408,type,
sK36: ( $int * $int ) > $int ).
tff(func_def_409,type,
sK37: set_4 ).
tff(func_def_410,type,
sK38: ( $int * $int ) > $int ).
tff(func_def_411,type,
sK39: set_3 ).
tff(func_def_412,type,
sK40: $int > $int ).
tff(func_def_413,type,
sK41: set_4 ).
tff(func_def_414,type,
sK42: ( $int * $int ) > $int ).
tff(func_def_415,type,
sK43: set_4 ).
tff(func_def_416,type,
sK44: ( $int * $int ) > $int ).
tff(func_def_417,type,
sK45: set_3 ).
tff(func_def_418,type,
sK46: $int > $int ).
tff(func_def_419,type,
sK47: ( $int * $int ) > $int ).
tff(func_def_420,type,
sK48: set_4 ).
tff(func_def_421,type,
sK49: ( $int * $int ) > $int ).
tff(func_def_422,type,
sK50: set_3 ).
tff(func_def_423,type,
sK51: $int > $int ).
tff(func_def_424,type,
sK52: set_4 ).
tff(func_def_425,type,
sK53: ( $int * $int ) > $int ).
tff(func_def_426,type,
sK54: set_3 ).
tff(func_def_427,type,
sK55: $int > $int ).
tff(func_def_428,type,
sK56: set_4 ).
tff(func_def_429,type,
sK57: ( $int * $int ) > $int ).
tff(func_def_430,type,
sK58: set_4 ).
tff(func_def_431,type,
sK59: ( $int * $int ) > $int ).
tff(func_def_432,type,
sK60: set_4 ).
tff(func_def_433,type,
sK61: ( $int * $int ) > $int ).
tff(func_def_434,type,
sK62: set_4 ).
tff(func_def_435,type,
sK63: ( $int * $int ) > $int ).
tff(func_def_436,type,
sK64: set_3 ).
tff(func_def_437,type,
sK65: $int > $int ).
tff(func_def_438,type,
sK66: set_4 ).
tff(func_def_439,type,
sK67: ( $int * $int ) > $int ).
tff(func_def_440,type,
sK68: set_3 ).
tff(func_def_441,type,
sK69: $int > $int ).
tff(func_def_442,type,
sK70: set_3 ).
tff(func_def_443,type,
sK71: $int > $int ).
tff(func_def_444,type,
sK72: set_3 ).
tff(func_def_445,type,
sK73: $int > $int ).
tff(func_def_446,type,
sK74: set_4 ).
tff(func_def_447,type,
sK75: ( $int * $int ) > $int ).
tff(func_def_448,type,
sK76: set_4 ).
tff(func_def_449,type,
sK77: ( $int * $int ) > $int ).
tff(func_def_450,type,
sK78: set_4 ).
tff(func_def_451,type,
sK79: ( $int * $int ) > $int ).
tff(func_def_452,type,
sK80: set_3 ).
tff(func_def_453,type,
sK81: $int > $int ).
tff(func_def_454,type,
sK82: set_4 ).
tff(func_def_455,type,
sK83: ( $int * $int ) > $int ).
tff(func_def_456,type,
sK84: $int ).
tff(func_def_457,type,
sK85: $int > $int ).
tff(func_def_458,type,
sK86: $int ).
tff(func_def_459,type,
sK87: set_4 ).
tff(func_def_460,type,
sK88: ( $int * $int ) > $int ).
tff(func_def_461,type,
sK89: ( $int * $int ) > $int ).
tff(func_def_462,type,
sK90: set_4 ).
tff(func_def_463,type,
sK91: ( $int * $int ) > $int ).
tff(func_def_464,type,
sK92: set_4 ).
tff(func_def_465,type,
sK93: ( $int * $int ) > $int ).
tff(func_def_466,type,
sK94: set_4 ).
tff(func_def_467,type,
sK95: ( $int * $int ) > $int ).
tff(func_def_468,type,
sK96: set_3 ).
tff(func_def_469,type,
sK97: $int > $int ).
tff(func_def_470,type,
sK98: set_4 ).
tff(func_def_471,type,
sK99: ( $int * $int ) > $int ).
tff(func_def_472,type,
sK100: set_4 ).
tff(func_def_473,type,
sK101: ( $int * $int ) > $int ).
tff(func_def_474,type,
sK102: set_4 ).
tff(func_def_475,type,
sK103: ( $int * $int ) > $int ).
tff(func_def_476,type,
sK104: set_3 ).
tff(func_def_477,type,
sK105: $int > $int ).
tff(func_def_478,type,
sK106: set_4 ).
tff(func_def_479,type,
sK107: ( $int * $int ) > $int ).
tff(func_def_480,type,
sK108: set_3 ).
tff(func_def_481,type,
sK109: $int > $int ).
tff(func_def_482,type,
sK110: $int > $o ).
tff(func_def_483,type,
sK111: $int ).
tff(func_def_484,type,
sK112: ( $int * $int ) > $int ).
tff(func_def_485,type,
sK113: set_3 ).
tff(func_def_486,type,
sK114: $int > $int ).
tff(func_def_487,type,
sK115: $o ).
tff(func_def_488,type,
sK116: $int ).
tff(func_def_489,type,
sK117: $int > $int ).
tff(func_def_490,type,
sF118: $int ).
tff(func_def_491,type,
sF119: $o ).
tff(pred_def_1,type,
mem0: ( $int * set_0 ) > $o ).
tff(pred_def_4,type,
mem2: ( $o * $int * set_2 ) > $o ).
tff(pred_def_5,type,
mem3: ( $int * $int * set_3 ) > $o ).
tff(pred_def_6,type,
mem4: ( $int * $int * $int * set_4 ) > $o ).
tff(f110,axiom,
! [X0: $int] :
( ( ( X0 = g_s38_38 )
| ( X0 = g_s39_39 ) )
<=> mem0(X0,g_s40_40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:ctx:17') ).
tff(f121,axiom,
! [X0: $int,X1: $o] :
( mem2((X1),X0,g_s41_41)
<=> ( ( ( X0 = g_s38_38 )
& ( (X1)
<=> $true ) )
| ( ( X0 = g_s39_39 )
& ( (X1)
<=> $false ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:ctx:18') ).
tff(f505,axiom,
~ ! [X0: $o] :
( ( (X0)
<=> ? [X1: $int] :
! [X2: $int] :
( ( X2 = $sum(g_s358_335,1) )
=> mem3(X2,X1,g_s319_316) ) )
=> mem2((X0),g_s38_38,g_s41_41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Local_Hyp:12') ).
tff(f506,conjecture,
! [X0: $int] :
( ! [X1: $o] :
( ( ? [X2: $int] :
! [X3: $int] :
( ( X3 = $sum(g_s358_335,1) )
=> mem3(X3,X2,g_s319_316) )
<=> (X1) )
=> mem2((X1),X0,g_s41_41) )
=> mem0(X0,g_s40_40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal') ).
tff(f507,negated_conjecture,
~ ! [X0: $int] :
( ! [X1: $o] :
( ( ? [X2: $int] :
! [X3: $int] :
( ( X3 = $sum(g_s358_335,1) )
=> mem3(X3,X2,g_s319_316) )
<=> (X1) )
=> mem2((X1),X0,g_s41_41) )
=> mem0(X0,g_s40_40) ),
inference(negated_conjecture,[status(cth)],[f506]) ).
tff(f513,plain,
! [X0: $int,X1: $o] :
( mem2((X1),X0,g_s41_41)
<=> ( ( ( X0 = g_s38_38 )
& ( (X1)
<=> $true ) )
| ( ( X0 = g_s39_39 )
& ( (X1)
<=> $false ) ) ) ),
inference(theory_normalization,[],[f121]) ).
tff(f536,plain,
~ ! [X0: $o] :
( ( (X0)
<=> ? [X1: $int] :
! [X2: $int] :
( ( X2 = $sum(g_s358_335,1) )
=> mem3(X2,X1,g_s319_316) ) )
=> mem2((X0),g_s38_38,g_s41_41) ),
inference(theory_normalization,[],[f505]) ).
tff(f571,plain,
~ ! [X0: $int] :
( ! [X1: $o] :
( ( ? [X2: $int] :
! [X3: $int] :
( ( X3 = $sum(g_s358_335,1) )
=> mem3(X3,X2,g_s319_316) )
<=> (X1) )
=> mem2((X1),X0,g_s41_41) )
=> mem0(X0,g_s40_40) ),
inference(theory_normalization,[],[f507]) ).
tff(f691,plain,
! [X0: $int,X1: $o] :
( mem2((X1),X0,g_s41_41)
<=> ( ( ( X0 = g_s38_38 )
& ( (X1)
<=> $true ) )
| ( ( X0 = g_s39_39 )
& ( (X1)
<=> $false ) ) ) ),
inference(rectify,[],[f513]) ).
tff(f692,definition,
! [X1: $o] :
( ( $true = (X1) )
<=> ( bG0((X1)) = $true ) ),
introduced(definition,[new_symbols(definition,[bG0])],[fool_formula_definition]) ).
tff(f693,plain,
! [X0: $int,X1: $o] :
( mem2(bG0((X1)),X0,g_s41_41)
<=> ( ( ( g_s38_38 = X0 )
& ( ( $true = (X1) )
<=> $true ) )
| ( ( g_s39_39 = X0 )
& ( ( $true = (X1) )
<=> $false ) ) ) ),
inference(fool_elimination,[],[f691,f692]) ).
tff(f694,plain,
~ ! [X0: $o] :
( ( (X0)
<=> ? [X1: $int] :
! [X2: $int] :
( ( X2 = $sum(g_s358_335,1) )
=> mem3(X2,X1,g_s319_316) ) )
=> mem2((X0),g_s38_38,g_s41_41) ),
inference(rectify,[],[f536]) ).
tff(f695,definition,
! [X0: $o] :
( ( $true = (X0) )
<=> ( $true = bG1((X0)) ) ),
introduced(definition,[new_symbols(definition,[bG1])],[fool_formula_definition]) ).
tff(f696,plain,
~ ! [X0: $o] :
( ( ( $true = (X0) )
<=> ? [X1: $int] :
! [X2: $int] :
( ( $sum(g_s358_335,1) = X2 )
=> mem3(X2,X1,g_s319_316) ) )
=> mem2(bG1((X0)),g_s38_38,g_s41_41) ),
inference(fool_elimination,[],[f694,f695]) ).
tff(f707,plain,
~ ! [X0: $int] :
( ! [X1: $o] :
( ( ? [X2: $int] :
! [X3: $int] :
( ( X3 = $sum(g_s358_335,1) )
=> mem3(X3,X2,g_s319_316) )
<=> (X1) )
=> mem2((X1),X0,g_s41_41) )
=> mem0(X0,g_s40_40) ),
inference(rectify,[],[f571]) ).
tff(f708,definition,
! [X1: $o] :
( ( $true = (X1) )
<=> ( bG8((X1)) = $true ) ),
introduced(definition,[new_symbols(definition,[bG8])],[fool_formula_definition]) ).
tff(f709,plain,
~ ! [X0: $int] :
( ! [X1: $o] :
( ( ( $true = (X1) )
<=> ? [X2: $int] :
! [X3: $int] :
( ( $sum(g_s358_335,1) = X3 )
=> mem3(X3,X2,g_s319_316) ) )
=> mem2(bG8((X1)),X0,g_s41_41) )
=> mem0(X0,g_s40_40) ),
inference(fool_elimination,[],[f707,f708]) ).
tff(f725,plain,
! [X0: $o] :
( ( bG8((X0)) = $true )
<=> ( $true = (X0) ) ),
inference(rectify,[],[f708]) ).
tff(f731,plain,
! [X0: $o] :
( ( $true = bG0((X0)) )
<=> ( $true = (X0) ) ),
inference(rectify,[],[f692]) ).
tff(f734,plain,
! [X0: $int,X1: $o] :
( mem2(bG0((X1)),X0,g_s41_41)
<=> ( ( ( $true = (X1) )
& ( g_s38_38 = X0 ) )
| ( ( g_s39_39 = X0 )
& ( $true != (X1) ) ) ) ),
inference(true_and_false_elimination,[],[f693]) ).
tff(f735,plain,
! [X1: $o,X0: $int] :
( mem2(bG0((X1)),X0,g_s41_41)
<=> ( ( ( $true = (X1) )
& ( g_s38_38 = X0 ) )
| ( ( $true != (X1) )
& ( g_s39_39 = X0 ) ) ) ),
inference(flattening,[],[f734]) ).
tff(f830,plain,
? [X0: $int] :
( ~ mem0(X0,g_s40_40)
& ! [X1: $o] :
( ( ? [X2: $int] :
! [X3: $int] :
( ( $sum(g_s358_335,1) != X3 )
| mem3(X3,X2,g_s319_316) )
<~> ( $true = (X1) ) )
| mem2(bG8((X1)),X0,g_s41_41) ) ),
inference(ennf_transformation,[],[f709]) ).
tff(f844,plain,
? [X0: $o] :
( ~ mem2(bG1((X0)),g_s38_38,g_s41_41)
& ( ? [X1: $int] :
! [X2: $int] :
( mem3(X2,X1,g_s319_316)
| ( $sum(g_s358_335,1) != X2 ) )
<=> ( $true = (X0) ) ) ),
inference(ennf_transformation,[],[f696]) ).
tff(f1042,plain,
! [X0: $o] :
( ( ( bG8((X0)) = $true )
| ( $true != (X0) ) )
& ( ( $true = (X0) )
| ( bG8((X0)) != $true ) ) ),
inference(nnf_transformation,[],[f725]) ).
tff(f1079,plain,
! [X0: $o] :
( ( ( $true = (X0) )
| ( $true != bG1((X0)) ) )
& ( ( $true = bG1((X0)) )
| ( $true != (X0) ) ) ),
inference(nnf_transformation,[],[f695]) ).
tff(f1112,plain,
! [X0: $o] :
( ( ( $true = bG0((X0)) )
| ( $true != (X0) ) )
& ( ( $true = (X0) )
| ( $true != bG0((X0)) ) ) ),
inference(nnf_transformation,[],[f731]) ).
tff(f1161,plain,
? [X0: $int] :
( ~ mem0(X0,g_s40_40)
& ! [X1: $o] :
( ( ( ( $true != (X1) )
| ! [X2: $int] :
? [X3: $int] :
( ( $sum(g_s358_335,1) = X3 )
& ~ mem3(X3,X2,g_s319_316) ) )
& ( ( $true = (X1) )
| ? [X2: $int] :
! [X3: $int] :
( ( $sum(g_s358_335,1) != X3 )
| mem3(X3,X2,g_s319_316) ) ) )
| mem2(bG8((X1)),X0,g_s41_41) ) ),
inference(nnf_transformation,[],[f830]) ).
tff(f1162,plain,
? [X0: $int] :
( ~ mem0(X0,g_s40_40)
& ! [X1: $o] :
( ( ( ( $true != (X1) )
| ! [X2: $int] :
? [X3: $int] :
( ( $sum(g_s358_335,1) = X3 )
& ~ mem3(X3,X2,g_s319_316) ) )
& ( ( $true = (X1) )
| ? [X4: $int] :
! [X5: $int] :
( ( $sum(g_s358_335,1) != X5 )
| mem3(X5,X4,g_s319_316) ) ) )
| mem2(bG8((X1)),X0,g_s41_41) ) ),
inference(rectify,[],[f1161]) ).
tff(f1163,plain,
( ~ mem0(sK84,g_s40_40)
& ! [X1: $o] :
( ( ( ( $true != (X1) )
| ! [X2: $int] :
( ( $sum(g_s358_335,1) = sK85(X2) )
& ~ mem3(sK85(X2),X2,g_s319_316) ) )
& ( ( $true = (X1) )
| ! [X5: $int] :
( ( $sum(g_s358_335,1) != X5 )
| mem3(X5,sK86,g_s319_316) ) ) )
| mem2(bG8((X1)),sK84,g_s41_41) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84,sK85,sK86]),skolemize(X0,sK84),skolemize(X3,sK85(X2)),skolemize(X4,sK86)],[f1162]) ).
tff(f1183,plain,
! [X0: $int] :
( ( ( X0 = g_s38_38 )
| ( X0 = g_s39_39 )
| ~ mem0(X0,g_s40_40) )
& ( mem0(X0,g_s40_40)
| ( ( g_s38_38 != X0 )
& ( g_s39_39 != X0 ) ) ) ),
inference(nnf_transformation,[],[f110]) ).
tff(f1184,plain,
! [X0: $int] :
( ( ( X0 = g_s38_38 )
| ( X0 = g_s39_39 )
| ~ mem0(X0,g_s40_40) )
& ( mem0(X0,g_s40_40)
| ( ( g_s38_38 != X0 )
& ( g_s39_39 != X0 ) ) ) ),
inference(flattening,[],[f1183]) ).
tff(f1212,plain,
! [X1: $o,X0: $int] :
( ( mem2(bG0((X1)),X0,g_s41_41)
| ( ( ( $true != (X1) )
| ( g_s38_38 != X0 ) )
& ( ( $true = (X1) )
| ( g_s39_39 != X0 ) ) ) )
& ( ( ( $true = (X1) )
& ( g_s38_38 = X0 ) )
| ( ( $true != (X1) )
& ( g_s39_39 = X0 ) )
| ~ mem2(bG0((X1)),X0,g_s41_41) ) ),
inference(nnf_transformation,[],[f735]) ).
tff(f1213,plain,
! [X1: $o,X0: $int] :
( ( mem2(bG0((X1)),X0,g_s41_41)
| ( ( ( $true != (X1) )
| ( g_s38_38 != X0 ) )
& ( ( $true = (X1) )
| ( g_s39_39 != X0 ) ) ) )
& ( ( ( $true = (X1) )
& ( g_s38_38 = X0 ) )
| ( ( $true != (X1) )
& ( g_s39_39 = X0 ) )
| ~ mem2(bG0((X1)),X0,g_s41_41) ) ),
inference(flattening,[],[f1212]) ).
tff(f1214,plain,
! [X0: $o,X1: $int] :
( ( mem2(bG0((X0)),X1,g_s41_41)
| ( ( ( $true != (X0) )
| ( g_s38_38 != X1 ) )
& ( ( $true = (X0) )
| ( g_s39_39 != X1 ) ) ) )
& ( ( ( $true = (X0) )
& ( g_s38_38 = X1 ) )
| ( ( $true != (X0) )
& ( g_s39_39 = X1 ) )
| ~ mem2(bG0((X0)),X1,g_s41_41) ) ),
inference(rectify,[],[f1213]) ).
tff(f1251,plain,
? [X0: $o] :
( ~ mem2(bG1((X0)),g_s38_38,g_s41_41)
& ( ? [X1: $int] :
! [X2: $int] :
( mem3(X2,X1,g_s319_316)
| ( $sum(g_s358_335,1) != X2 ) )
| ( $true != (X0) ) )
& ( ( $true = (X0) )
| ! [X1: $int] :
? [X2: $int] :
( ~ mem3(X2,X1,g_s319_316)
& ( $sum(g_s358_335,1) = X2 ) ) ) ),
inference(nnf_transformation,[],[f844]) ).
tff(f1252,plain,
? [X0: $o] :
( ~ mem2(bG1((X0)),g_s38_38,g_s41_41)
& ( ? [X1: $int] :
! [X2: $int] :
( mem3(X2,X1,g_s319_316)
| ( $sum(g_s358_335,1) != X2 ) )
| ( $true != (X0) ) )
& ( ( $true = (X0) )
| ! [X1: $int] :
? [X2: $int] :
( ~ mem3(X2,X1,g_s319_316)
& ( $sum(g_s358_335,1) = X2 ) ) ) ),
inference(flattening,[],[f1251]) ).
tff(f1253,plain,
? [X0: $o] :
( ~ mem2(bG1((X0)),g_s38_38,g_s41_41)
& ( ? [X1: $int] :
! [X2: $int] :
( mem3(X2,X1,g_s319_316)
| ( $sum(g_s358_335,1) != X2 ) )
| ( $true != (X0) ) )
& ( ( $true = (X0) )
| ! [X3: $int] :
? [X4: $int] :
( ~ mem3(X4,X3,g_s319_316)
& ( $sum(g_s358_335,1) = X4 ) ) ) ),
inference(rectify,[],[f1252]) ).
tff(f1254,plain,
( ~ mem2(bG1(sK115),g_s38_38,g_s41_41)
& ( ! [X2: $int] :
( mem3(X2,sK116,g_s319_316)
| ( $sum(g_s358_335,1) != X2 ) )
| ( sK115 != $true ) )
& ( ( sK115 = $true )
| ! [X3: $int] :
( ~ mem3(sK117(X3),X3,g_s319_316)
& ( $sum(g_s358_335,1) = sK117(X3) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115,sK116,sK117]),skolemize(X0,sK115),skolemize(X1,sK116),skolemize(X4,sK117(X3))],[f1253]) ).
tff(f1549,plain,
! [X0: $o] :
( ( bG8((X0)) != $true )
| ( $true = (X0) ) ),
inference(cnf_transformation,[],[f1042]) ).
tff(f1550,plain,
! [X0: $o] :
( ( bG8((X0)) = $true )
| ( $true != (X0) ) ),
inference(cnf_transformation,[],[f1042]) ).
tff(f1663,plain,
! [X0: $o] :
( ( $true = bG1((X0)) )
| ( $true != (X0) ) ),
inference(cnf_transformation,[],[f1079]) ).
tff(f1791,plain,
! [X0: $o] :
( ( $true != bG0((X0)) )
| ( $true = (X0) ) ),
inference(cnf_transformation,[],[f1112]) ).
tff(f1792,plain,
! [X0: $o] :
( ( $true = bG0((X0)) )
| ( $true != (X0) ) ),
inference(cnf_transformation,[],[f1112]) ).
tff(f1955,plain,
! [X1: $o,X5: $int] :
( ( $true = (X1) )
| ( $sum(g_s358_335,1) != X5 )
| mem3(X5,sK86,g_s319_316)
| mem2(bG8((X1)),sK84,g_s41_41) ),
inference(cnf_transformation,[],[f1163]) ).
tff(f1956,plain,
! [X2: $int,X1: $o] :
( ( $true != (X1) )
| ~ mem3(sK85(X2),X2,g_s319_316)
| mem2(bG8((X1)),sK84,g_s41_41) ),
inference(cnf_transformation,[],[f1163]) ).
tff(f1957,plain,
! [X2: $int,X1: $o] :
( ( $true != (X1) )
| ( $sum(g_s358_335,1) = sK85(X2) )
| mem2(bG8((X1)),sK84,g_s41_41) ),
inference(cnf_transformation,[],[f1163]) ).
tff(f1958,plain,
~ mem0(sK84,g_s40_40),
inference(cnf_transformation,[],[f1163]) ).
tff(f2028,plain,
! [X0: $int] :
( mem0(X0,g_s40_40)
| ( g_s39_39 != X0 ) ),
inference(cnf_transformation,[],[f1184]) ).
tff(f2029,plain,
! [X0: $int] :
( mem0(X0,g_s40_40)
| ( g_s38_38 != X0 ) ),
inference(cnf_transformation,[],[f1184]) ).
tff(f2136,plain,
! [X0: $o,X1: $int] :
( ~ mem2(bG0((X0)),X1,g_s41_41)
| ( g_s39_39 = X1 )
| ( g_s38_38 = X1 ) ),
inference(cnf_transformation,[],[f1214]) ).
tff(f2137,plain,
! [X0: $o,X1: $int] :
( ( g_s38_38 = X1 )
| ( $true != (X0) )
| ~ mem2(bG0((X0)),X1,g_s41_41) ),
inference(cnf_transformation,[],[f1214]) ).
tff(f2141,plain,
! [X0: $o,X1: $int] :
( mem2(bG0((X0)),X1,g_s41_41)
| ( $true != (X0) )
| ( g_s38_38 != X1 ) ),
inference(cnf_transformation,[],[f1214]) ).
tff(f2253,plain,
~ mem2(bG1(sK115),g_s38_38,g_s41_41),
inference(cnf_transformation,[],[f1254]) ).
tff(f2255,plain,
! [X0: $o] :
( ( $false = (X0) )
| ( $true = (X0) ) ),
introduced(definition,[],[fool_exhaustiveness_axiom]) ).
tff(f2277,plain,
$true = bG8($true),
inference(equality_resolution,[],[f1550]) ).
tff(f2283,plain,
bG1($true) = $true,
inference(equality_resolution,[],[f1663]) ).
tff(f2301,plain,
bG0($true) = $true,
inference(equality_resolution,[],[f1792]) ).
tff(f2306,plain,
! [X2: $int] :
( ( $sum(g_s358_335,1) = sK85(X2) )
| mem2(bG8($true),sK84,g_s41_41) ),
inference(equality_resolution,[],[f1957]) ).
tff(f2307,plain,
! [X2: $int] :
( ~ mem3(sK85(X2),X2,g_s319_316)
| mem2(bG8($true),sK84,g_s41_41) ),
inference(equality_resolution,[],[f1956]) ).
tff(f2308,plain,
! [X1: $o] :
( ( $true = (X1) )
| mem3($sum(g_s358_335,1),sK86,g_s319_316)
| mem2(bG8((X1)),sK84,g_s41_41) ),
inference(equality_resolution,[],[f1955]) ).
tff(f2312,plain,
mem0(g_s38_38,g_s40_40),
inference(equality_resolution,[],[f2029]) ).
tff(f2313,plain,
mem0(g_s39_39,g_s40_40),
inference(equality_resolution,[],[f2028]) ).
tff(f2325,plain,
! [X1: $int] :
( mem2(bG0($true),X1,g_s41_41)
| ( g_s38_38 != X1 ) ),
inference(equality_resolution,[],[f2141]) ).
tff(f2326,plain,
mem2(bG0($true),g_s38_38,g_s41_41),
inference(equality_resolution,[],[f2325]) ).
tff(f2329,plain,
! [X1: $int] :
( ~ mem2(bG0($true),X1,g_s41_41)
| ( g_s38_38 = X1 ) ),
inference(equality_resolution,[],[f2137]) ).
tff(f2338,definition,
sF118 = $sum(g_s358_335,1),
introduced(definition,[new_symbols(definition,[sF118])],[function_definition]) ).
tff(f2339,plain,
$sum(g_s358_335,1) = sF118,
inference(reorient_equations,[],[f2338]) ).
tff(f2340,definition,
sF119 = bG8($true),
introduced(definition,[new_symbols(definition,[sF119])],[function_definition]) ).
tff(f2341,plain,
! [X2: $int] :
( ( sK85(X2) = sF118 )
| mem2(sF119,sK84,g_s41_41) ),
inference(definition_folding,[],[f2306,f2340,f2339]) ).
tff(f2342,plain,
! [X2: $int] :
( mem2(sF119,sK84,g_s41_41)
| ~ mem3(sK85(X2),X2,g_s319_316) ),
inference(definition_folding,[],[f2307,f2340]) ).
tff(f2343,plain,
! [X1: $o] :
( mem2(bG8((X1)),sK84,g_s41_41)
| ( $true = (X1) )
| mem3(sF118,sK86,g_s319_316) ),
inference(definition_folding,[],[f2308,f2339]) ).
tff(f2364,definition,
( spl120_1
<=> mem2(sF119,sK84,g_s41_41) ),
introduced(definition,[new_symbols(definition,[spl120_1])],[avatar_definition]) ).
tff(f2366,plain,
( mem2(sF119,sK84,g_s41_41)
| ~ spl120_1 ),
inference(avatar_component_clause,[],[f2364]) ).
tff(f2368,definition,
( spl120_2
<=> ! [X2: $int] : ( sK85(X2) = sF118 ) ),
introduced(definition,[new_symbols(definition,[spl120_2])],[avatar_definition]) ).
tff(f2369,plain,
( ! [X2: $int] : ( sK85(X2) = sF118 )
| ~ spl120_2 ),
inference(avatar_component_clause,[],[f2368]) ).
tff(f2370,plain,
( spl120_1
| spl120_2 ),
inference(avatar_split_clause,[],[f2341,f2368,f2364]) ).
tff(f2371,plain,
sF119 = $true,
inference(forward_demodulation,[],[f2340,f2277]) ).
tff(f2372,plain,
( ! [X2: $int] :
( ~ mem3(sF118,X2,g_s319_316)
| mem2(sF119,sK84,g_s41_41) )
| ~ spl120_2 ),
inference(forward_demodulation,[],[f2342,f2369]) ).
tff(f2373,plain,
( ! [X2: $int] :
( ~ mem3(sF118,X2,g_s319_316)
| mem2($true,sK84,g_s41_41) )
| ~ spl120_2 ),
inference(forward_demodulation,[],[f2372,f2371]) ).
tff(f2375,definition,
( spl120_3
<=> mem2($true,sK84,g_s41_41) ),
introduced(definition,[new_symbols(definition,[spl120_3])],[avatar_definition]) ).
tff(f2376,plain,
( ~ mem2($true,sK84,g_s41_41)
| spl120_3 ),
inference(avatar_component_clause,[],[f2375]) ).
tff(f2377,plain,
( mem2($true,sK84,g_s41_41)
| ~ spl120_3 ),
inference(avatar_component_clause,[],[f2375]) ).
tff(f2379,definition,
( spl120_4
<=> ! [X2: $int] : ~ mem3(sF118,X2,g_s319_316) ),
introduced(definition,[new_symbols(definition,[spl120_4])],[avatar_definition]) ).
tff(f2380,plain,
( ! [X2: $int] : ~ mem3(sF118,X2,g_s319_316)
| ~ spl120_4 ),
inference(avatar_component_clause,[],[f2379]) ).
tff(f2381,plain,
( spl120_3
| spl120_4
| ~ spl120_2 ),
inference(avatar_split_clause,[],[f2373,f2368,f2379,f2375]) ).
tff(f2387,plain,
mem2($true,g_s38_38,g_s41_41),
inference(forward_demodulation,[],[f2326,f2301]) ).
tff(f2392,definition,
( spl120_5
<=> ! [X1: $o] :
( mem2(bG8((X1)),sK84,g_s41_41)
| ( $true = (X1) ) ) ),
introduced(definition,[new_symbols(definition,[spl120_5])],[avatar_definition]) ).
tff(f2393,plain,
( ! [X1: $o] :
( mem2(bG8((X1)),sK84,g_s41_41)
| ( $true = (X1) ) )
| ~ spl120_5 ),
inference(avatar_component_clause,[],[f2392]) ).
tff(f2395,definition,
( spl120_6
<=> mem3(sF118,sK86,g_s319_316) ),
introduced(definition,[new_symbols(definition,[spl120_6])],[avatar_definition]) ).
tff(f2397,plain,
( mem3(sF118,sK86,g_s319_316)
| ~ spl120_6 ),
inference(avatar_component_clause,[],[f2395]) ).
tff(f2398,plain,
( spl120_5
| spl120_6 ),
inference(avatar_split_clause,[],[f2343,f2395,f2392]) ).
tff(f2410,plain,
( ! [X0: $o] :
( mem2($false,sK84,g_s41_41)
| ( bG8((X0)) = $true )
| ( $true = (X0) ) )
| ~ spl120_5 ),
inference(superposition,[],[f2393,f2255]) ).
tff(f2436,definition,
( spl120_7
<=> ! [X0: $o] :
( ( bG8((X0)) = $true )
| ( $true = (X0) ) ) ),
introduced(definition,[new_symbols(definition,[spl120_7])],[avatar_definition]) ).
tff(f2437,plain,
( ! [X0: $o] :
( ( bG8((X0)) = $true )
| ( $true = (X0) ) )
| ~ spl120_7 ),
inference(avatar_component_clause,[],[f2436]) ).
tff(f2439,definition,
( spl120_8
<=> mem2($false,sK84,g_s41_41) ),
introduced(definition,[new_symbols(definition,[spl120_8])],[avatar_definition]) ).
tff(f2441,plain,
( mem2($false,sK84,g_s41_41)
| ~ spl120_8 ),
inference(avatar_component_clause,[],[f2439]) ).
tff(f2442,plain,
( spl120_7
| spl120_8
| ~ spl120_5 ),
inference(avatar_split_clause,[],[f2410,f2392,f2439,f2436]) ).
tff(f2478,plain,
! [X1: $int] :
( ~ mem2($true,X1,g_s41_41)
| ( g_s38_38 = X1 ) ),
inference(forward_demodulation,[],[f2329,f2301]) ).
tff(f2479,plain,
( ( g_s38_38 = sK84 )
| ~ spl120_3 ),
inference(resolution,[],[f2478,f2377]) ).
tff(f2485,plain,
( ~ mem0(g_s38_38,g_s40_40)
| ~ spl120_3 ),
inference(superposition,[],[f1958,f2479]) ).
tff(f2486,plain,
( $false
| ~ spl120_3 ),
inference(forward_subsumption_resolution,[],[f2485,f2312]) ).
tff(f2487,plain,
~ spl120_3,
inference(avatar_contradiction_clause,[],[f2486]) ).
tff(f2488,plain,
( $false
| ~ spl120_4
| ~ spl120_6 ),
inference(resolution,[],[f2380,f2397]) ).
tff(f2489,plain,
( ~ spl120_4
| ~ spl120_6 ),
inference(avatar_contradiction_clause,[],[f2488]) ).
tff(f2490,plain,
( ! [X0: $o] : ( $true = (X0) )
| ~ spl120_7 ),
inference(forward_subsumption_resolution,[],[f2437,f1549]) ).
tff(f2554,plain,
( ~ mem2(bG1($true),g_s38_38,g_s41_41)
| ~ spl120_7 ),
inference(superposition,[],[f2253,f2490]) ).
tff(f2584,plain,
( ~ mem2($true,g_s38_38,g_s41_41)
| ~ spl120_7 ),
inference(forward_demodulation,[],[f2554,f2283]) ).
tff(f2588,plain,
( $false
| ~ spl120_7 ),
inference(forward_subsumption_resolution,[],[f2584,f2387]) ).
tff(f2589,plain,
~ spl120_7,
inference(avatar_contradiction_clause,[],[f2588]) ).
tff(f2834,plain,
( ! [X0: $o] :
( mem2((X0),sK84,g_s41_41)
| ( $true = (X0) ) )
| ~ spl120_8 ),
inference(superposition,[],[f2441,f2255]) ).
tff(f2984,plain,
( ! [X0: $o] :
( ( g_s38_38 = sK84 )
| ( g_s39_39 = sK84 )
| ( $true = bG0((X0)) ) )
| ~ spl120_8 ),
inference(resolution,[],[f2136,f2834]) ).
tff(f2990,definition,
( spl120_21
<=> ( g_s38_38 = sK84 ) ),
introduced(definition,[new_symbols(definition,[spl120_21])],[avatar_definition]) ).
tff(f2992,plain,
( ( g_s38_38 = sK84 )
| ~ spl120_21 ),
inference(avatar_component_clause,[],[f2990]) ).
tff(f2994,definition,
( spl120_22
<=> ( g_s39_39 = sK84 ) ),
introduced(definition,[new_symbols(definition,[spl120_22])],[avatar_definition]) ).
tff(f2996,plain,
( ( g_s39_39 = sK84 )
| ~ spl120_22 ),
inference(avatar_component_clause,[],[f2994]) ).
tff(f2998,definition,
( spl120_23
<=> ! [X0: $o] : ( $true = bG0((X0)) ) ),
introduced(definition,[new_symbols(definition,[spl120_23])],[avatar_definition]) ).
tff(f2999,plain,
( ! [X0: $o] : ( $true = bG0((X0)) )
| ~ spl120_23 ),
inference(avatar_component_clause,[],[f2998]) ).
tff(f3000,plain,
( spl120_21
| spl120_22
| spl120_23
| ~ spl120_8 ),
inference(avatar_split_clause,[],[f2984,f2439,f2998,f2994,f2990]) ).
tff(f3018,plain,
( ! [X0: $o] :
( ( $true != $true )
| ( $true = (X0) ) )
| ~ spl120_23 ),
inference(superposition,[],[f1791,f2999]) ).
tff(f3020,plain,
( ! [X0: $o] : ( $true = (X0) )
| ~ spl120_23 ),
inference(trivial_inequality_removal,[],[f3018]) ).
tff(f3065,plain,
( ~ mem2(bG1($true),g_s38_38,g_s41_41)
| ~ spl120_23 ),
inference(superposition,[],[f2253,f3020]) ).
tff(f3088,plain,
( ~ mem2($true,g_s38_38,g_s41_41)
| ~ spl120_23 ),
inference(forward_demodulation,[],[f3065,f2283]) ).
tff(f3099,plain,
( $false
| ~ spl120_23 ),
inference(forward_subsumption_resolution,[],[f3088,f2387]) ).
tff(f3100,plain,
~ spl120_23,
inference(avatar_contradiction_clause,[],[f3099]) ).
tff(f3118,plain,
( ~ mem0(g_s38_38,g_s40_40)
| ~ spl120_21 ),
inference(superposition,[],[f1958,f2992]) ).
tff(f3119,plain,
( $false
| ~ spl120_21 ),
inference(forward_subsumption_resolution,[],[f3118,f2312]) ).
tff(f3120,plain,
~ spl120_21,
inference(avatar_contradiction_clause,[],[f3119]) ).
tff(f3132,plain,
( ~ mem0(g_s39_39,g_s40_40)
| ~ spl120_22 ),
inference(superposition,[],[f1958,f2996]) ).
tff(f3138,plain,
( $false
| ~ spl120_22 ),
inference(forward_subsumption_resolution,[],[f3132,f2313]) ).
tff(f3139,plain,
~ spl120_22,
inference(avatar_contradiction_clause,[],[f3138]) ).
tff(f3140,plain,
( mem2($true,sK84,g_s41_41)
| ~ spl120_1 ),
inference(forward_demodulation,[],[f2366,f2371]) ).
tff(f3142,plain,
( $false
| ~ spl120_1
| spl120_3 ),
inference(forward_subsumption_resolution,[],[f3140,f2376]) ).
tff(f3143,plain,
( ~ spl120_1
| spl120_3 ),
inference(avatar_contradiction_clause,[],[f3142]) ).
cnf(s1,plain,
( spl120_1
| spl120_2 ),
inference(sat_conversion,[],[f2370]) ).
cnf(s2,plain,
( ~ spl120_2
| spl120_3
| spl120_4 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s3,plain,
( spl120_5
| spl120_6 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s4,plain,
( ~ spl120_5
| spl120_7
| spl120_8 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s7,plain,
~ spl120_3,
inference(sat_conversion,[],[f2487]) ).
cnf(s8,plain,
( ~ spl120_4
| ~ spl120_6 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s11,plain,
~ spl120_7,
inference(sat_conversion,[],[f2589]) ).
cnf(s19,plain,
( ~ spl120_8
| spl120_21
| spl120_22
| spl120_23 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s22,plain,
~ spl120_23,
inference(sat_conversion,[],[f3100]) ).
cnf(s25,plain,
~ spl120_21,
inference(sat_conversion,[],[f3120]) ).
cnf(s27,plain,
~ spl120_22,
inference(sat_conversion,[],[f3139]) ).
cnf(s28,plain,
( ~ spl120_1
| spl120_3 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s29,plain,
~ spl120_8,
inference(rat,[],[s19,s22,s27,s25]) ).
cnf(s30,plain,
~ spl120_1,
inference(rat,[],[s28,s7]) ).
cnf(s32,plain,
~ spl120_5,
inference(rat,[],[s4,s29,s11]) ).
cnf(s33,plain,
spl120_6,
inference(rat,[],[s3,s32]) ).
cnf(s34,plain,
~ spl120_4,
inference(rat,[],[s8,s33]) ).
cnf(s35,plain,
~ spl120_2,
inference(rat,[],[s2,s34,s7]) ).
cnf(s36,plain,
$false,
inference(rat,[],[s1,s35,s30]) ).
tff(f3145,plain,
$false,
inference(avatar_sat_refutation,[],[s36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC522_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n017.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 09:37:06 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.28/1.42 % (3435538)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.28/1.42 % (3435580)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2997857142:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.28/1.42 % (3435581)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2731481597:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.28/1.42 % (3435579)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3867895475:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.28/1.42 % (3435579)Instruction limit reached!
% 4.28/1.42 % (3435579)------------------------------
% 4.28/1.42 % (3435579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.42 % (3435579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.42 % (3435579)CaDiCaL version: 2.1.3
% 4.28/1.42 % (3435579)Termination reason: Instruction limit
% 4.28/1.42 % (3435579)Termination phase: Including theory axioms
% 4.28/1.42 % (3435579)Time elapsed: 0.004 s
% 4.28/1.42 % (3435579)Peak memory usage: 86 MB
% 4.28/1.42 % (3435579)Instructions burned: 5 (million)
% 4.28/1.42 % (3435581)Instruction limit reached!
% 4.28/1.42 % (3435581)------------------------------
% 4.28/1.42 % (3435581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.42 % (3435581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.42 % (3435581)CaDiCaL version: 2.1.3
% 4.28/1.42 % (3435581)Termination reason: Instruction limit
% 4.28/1.42 % (3435581)Termination phase: Property scanning
% 4.28/1.42 % (3435581)Time elapsed: 0.034 s
% 4.28/1.42 % (3435581)Peak memory usage: 88 MB
% 4.28/1.42 % (3435581)Instructions burned: 33 (million)
% 4.28/1.42 % (3435580)Instruction limit reached!
% 4.28/1.42 % (3435580)------------------------------
% 4.28/1.42 % (3435580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.42 % (3435580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.42 % (3435580)CaDiCaL version: 2.1.3
% 4.28/1.42 % (3435580)Termination reason: Instruction limit
% 4.28/1.42 % (3435580)Termination phase: Saturation
% 4.28/1.42 % (3435580)Time elapsed: 0.038 s
% 4.28/1.42 % (3435580)Peak memory usage: 113 MB
% 4.28/1.42 % (3435580)Instructions burned: 47 (million)
% 4.28/1.42 % (3435574)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=533933923:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.28/1.42 % (3435575)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1930538740:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.28/1.42 % (3435576)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4233002809:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.28/1.42 % (3435574)Instruction limit reached!
% 4.28/1.42 % (3435574)------------------------------
% 4.28/1.42 % (3435574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.42 % (3435574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.42 % (3435574)CaDiCaL version: 2.1.3
% 4.28/1.42 % (3435574)Termination reason: Instruction limit
% 4.28/1.42 % (3435574)Termination phase: Including theory axioms
% 4.28/1.42 % (3435574)Time elapsed: 0.010 s
% 4.28/1.42 % (3435574)Peak memory usage: 86 MB
% 4.28/1.42 % (3435574)Instructions burned: 12 (million)
% 4.28/1.42 % (3435578)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3889711028:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.28/1.42 % (3435578)Instruction limit reached!
% 4.28/1.42 % (3435578)------------------------------
% 4.28/1.42 % (3435578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.28/1.42 % (3435578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.28/1.42 % (3435578)CaDiCaL version: 2.1.3
% 4.28/1.42 % (3435578)Termination reason: Instruction limit
% 4.28/1.42 % (3435578)Termination phase: Property scanning
% 4.28/1.42 % (3435578)Time elapsed: 0.008 s
% 4.28/1.42 % (3435578)Peak memory usage: 86 MB
% 4.28/1.42 % (3435578)Instructions burned: 7 (million)
% 4.28/1.42 % (3435600)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4019389446:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.28/1.42 % (3435600)Instruction limit reached!
% 5.18/1.56 % (3435600)------------------------------
% 5.18/1.56 % (3435600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435600)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435600)Termination reason: Instruction limit
% 5.18/1.56 % (3435600)Termination phase: Preprocessing 3
% 5.18/1.56 % (3435600)Time elapsed: 0.005 s
% 5.18/1.56 % (3435600)Peak memory usage: 87 MB
% 5.18/1.56 % (3435600)Instructions burned: 16 (million)
% 5.18/1.56 % (3435596)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2879431032:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 5.18/1.56 % (3435603)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2629891557:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 5.18/1.56 % (3435610)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4273830131:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 5.18/1.56 % (3435604)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1834651677:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 5.18/1.56 % (3435596)Instruction limit reached!
% 5.18/1.56 % (3435596)------------------------------
% 5.18/1.56 % (3435596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435596)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435596)Termination reason: Instruction limit
% 5.18/1.56 % (3435596)Termination phase: Preprocessing 3
% 5.18/1.56 % (3435596)Time elapsed: 0.014 s
% 5.18/1.56 % (3435596)Peak memory usage: 87 MB
% 5.18/1.56 % (3435596)Instructions burned: 16 (million)
% 5.18/1.56 % (3435603)Instruction limit reached!
% 5.18/1.56 % (3435603)------------------------------
% 5.18/1.56 % (3435603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435603)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435603)Termination reason: Instruction limit
% 5.18/1.56 % (3435603)Termination phase: Property scanning
% 5.18/1.56 % (3435603)Time elapsed: 0.024 s
% 5.18/1.56 % (3435603)Peak memory usage: 87 MB
% 5.18/1.56 % (3435603)Instructions burned: 25 (million)
% 5.18/1.56 % (3435576)Instruction limit reached!
% 5.18/1.56 % (3435576)------------------------------
% 5.18/1.56 % (3435576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435576)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435576)Termination reason: Instruction limit
% 5.18/1.56 % (3435576)Termination phase: Saturation
% 5.18/1.56 % (3435576)Time elapsed: 0.235 s
% 5.18/1.56 % (3435576)Peak memory usage: 118 MB
% 5.18/1.56 % (3435576)Instructions burned: 201 (million)
% 5.18/1.56 % (3435604)Instruction limit reached!
% 5.18/1.56 % (3435604)------------------------------
% 5.18/1.56 % (3435604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435604)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435604)Termination reason: Instruction limit
% 5.18/1.56 % (3435604)Termination phase: Property scanning
% 5.18/1.56 % (3435604)Time elapsed: 0.024 s
% 5.18/1.56 % (3435604)Peak memory usage: 88 MB
% 5.18/1.56 % (3435604)Instructions burned: 29 (million)
% 5.18/1.56 % (3435598)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=4291623329:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 5.18/1.56 % (3435610)Instruction limit reached!
% 5.18/1.56 % (3435610)------------------------------
% 5.18/1.56 % (3435610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.18/1.56 % (3435610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.18/1.56 % (3435610)CaDiCaL version: 2.1.3
% 5.18/1.56 % (3435610)Termination reason: Instruction limit
% 5.18/1.56 % (3435610)Termination phase: Saturation
% 5.18/1.56 % (3435610)Time elapsed: 0.043 s
% 5.18/1.56 % (3435610)Peak memory usage: 91 MB
% 5.18/1.56 % (3435610)Instructions burned: 85 (million)
% 5.18/1.56 % (3435598)Instruction limit reached!
% 5.18/1.56 % (3435598)------------------------------
% 5.87/1.69 % (3435598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435598)CaDiCaL version: 2.1.3
% 5.87/1.69 % (3435598)Termination reason: Instruction limit
% 5.87/1.69 % (3435598)Termination phase: Property scanning
% 5.87/1.69 % (3435598)Time elapsed: 0.029 s
% 5.87/1.69 % (3435598)Peak memory usage: 88 MB
% 5.87/1.69 % (3435598)Instructions burned: 30 (million)
% 5.87/1.69 % (3435575)Instruction limit reached!
% 5.87/1.69 % (3435575)------------------------------
% 5.87/1.69 % (3435575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435575)CaDiCaL version: 2.1.3
% 5.87/1.69 % (3435575)Termination reason: Instruction limit
% 5.87/1.69 % (3435575)Termination phase: Saturation
% 5.87/1.69 % (3435575)Time elapsed: 0.308 s
% 5.87/1.69 % (3435575)Peak memory usage: 122 MB
% 5.87/1.69 % (3435575)Instructions burned: 308 (million)
% 5.87/1.69 % (3435619)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1401332555:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 5.87/1.69 % (3435618)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3859528212:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 5.87/1.69 % (3435618)Instruction limit reached!
% 5.87/1.69 % (3435618)------------------------------
% 5.87/1.69 % (3435618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435618)CaDiCaL version: 2.1.3
% 5.87/1.69 % (3435618)Termination reason: Instruction limit
% 5.87/1.69 % (3435618)Termination phase: Property scanning
% 5.87/1.69 % (3435618)Time elapsed: 0.002 s
% 5.87/1.69 % (3435618)Peak memory usage: 85 MB
% 5.87/1.69 % (3435618)Instructions burned: 3 (million)
% 5.87/1.69 % (3435626)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=922005083:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 5.87/1.69 % (3435620)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3408939628:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 5.87/1.69 % (3435622)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3479598078:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 5.87/1.69 % (3435620)Instruction limit reached!
% 5.87/1.69 % (3435620)------------------------------
% 5.87/1.69 % (3435620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435620)CaDiCaL version: 2.1.3
% 5.87/1.69 % (3435620)Termination reason: Instruction limit
% 5.87/1.69 % (3435620)Termination phase: Property scanning
% 5.87/1.69 % (3435620)Time elapsed: 0.003 s
% 5.87/1.69 % (3435620)Peak memory usage: 85 MB
% 5.87/1.69 % (3435620)Instructions burned: 4 (million)
% 5.87/1.69 % (3435626)Instruction limit reached!
% 5.87/1.69 % (3435626)------------------------------
% 5.87/1.69 % (3435626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435626)CaDiCaL version: 2.1.3
% 5.87/1.69 % (3435626)Termination reason: Instruction limit
% 5.87/1.69 % (3435626)Termination phase: Property scanning
% 5.87/1.69 % (3435626)Time elapsed: 0.005 s
% 5.87/1.69 % (3435626)Peak memory usage: 85 MB
% 5.87/1.69 % (3435626)Instructions burned: 10 (million)
% 5.87/1.69 % (3435624)lrs+10_1_thi=all:si=on:fd=off:random_seed=1734573230:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.87/1.69 % (3435627)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1206654669:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 5.87/1.69 % (3435627)Instruction limit reached!
% 5.87/1.69 % (3435627)------------------------------
% 5.87/1.69 % (3435627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.87/1.69 % (3435627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.69 % (3435627)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435627)Termination reason: Instruction limit
% 6.75/1.88 % (3435627)Termination phase: Property scanning
% 6.75/1.88 % (3435627)Time elapsed: 0.002 s
% 6.75/1.88 % (3435627)Peak memory usage: 86 MB
% 6.75/1.88 % (3435627)Instructions burned: 2 (million)
% 6.75/1.88 % (3435624)Instruction limit reached!
% 6.75/1.88 % (3435624)------------------------------
% 6.75/1.88 % (3435624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.88 % (3435624)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435624)Termination reason: Instruction limit
% 6.75/1.88 % (3435624)Termination phase: Saturation
% 6.75/1.88 % (3435624)Time elapsed: 0.049 s
% 6.75/1.88 % (3435624)Peak memory usage: 113 MB
% 6.75/1.88 % (3435624)Instructions burned: 54 (million)
% 6.75/1.88 % (3435619)Instruction limit reached!
% 6.75/1.88 % (3435619)------------------------------
% 6.75/1.88 % (3435619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.88 % (3435619)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435619)Termination reason: Instruction limit
% 6.75/1.88 % (3435619)Termination phase: Saturation
% 6.75/1.88 % (3435619)Time elapsed: 0.107 s
% 6.75/1.88 % (3435619)Peak memory usage: 91 MB
% 6.75/1.88 % (3435619)Instructions burned: 181 (million)
% 6.75/1.88 % (3435622)Instruction limit reached!
% 6.75/1.88 % (3435622)------------------------------
% 6.75/1.88 % (3435622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.88 % (3435622)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435622)Termination reason: Instruction limit
% 6.75/1.88 % (3435622)Termination phase: Saturation
% 6.75/1.88 % (3435622)Time elapsed: 0.076 s
% 6.75/1.88 % (3435622)Peak memory usage: 131 MB
% 6.75/1.88 % (3435622)Instructions burned: 68 (million)
% 6.75/1.88 % (3435630)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1590773535:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 6.75/1.88 % (3435630)Instruction limit reached!
% 6.75/1.88 % (3435630)------------------------------
% 6.75/1.88 % (3435630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.88 % (3435630)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435630)Termination reason: Instruction limit
% 6.75/1.88 % (3435630)Termination phase: Property scanning
% 6.75/1.88 % (3435630)Time elapsed: 0.002 s
% 6.75/1.88 % (3435630)Peak memory usage: 85 MB
% 6.75/1.88 % (3435630)Instructions burned: 2 (million)
% 6.75/1.88 % (3435634)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2780957227:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 6.75/1.88 % (3435635)dis+10_1_si=on:random_seed=2008066343:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 6.75/1.88 % (3435635)Instruction limit reached!
% 6.75/1.88 % (3435635)------------------------------
% 6.75/1.88 % (3435635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.88 % (3435635)CaDiCaL version: 2.1.3
% 6.75/1.88 % (3435635)Termination reason: Instruction limit
% 6.75/1.88 % (3435635)Termination phase: Preprocessing 1
% 6.75/1.88 % (3435635)Time elapsed: 0.006 s
% 6.75/1.88 % (3435635)Peak memory usage: 86 MB
% 6.75/1.88 % (3435635)Instructions burned: 11 (million)
% 6.75/1.88 % (3435639)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=401635316:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi)
% 6.75/1.88 % (3435638)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3996408850:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 6.75/1.88 % (3435640)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=958492695:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 6.75/1.88 % (3435640)Instruction limit reached!
% 6.75/1.88 % (3435640)------------------------------
% 6.75/1.88 % (3435640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.75/1.88 % (3435640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435640)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435640)Termination reason: Instruction limit
% 9.06/2.30 % (3435640)Termination phase: Property scanning
% 9.06/2.30 % (3435640)Time elapsed: 0.002 s
% 9.06/2.30 % (3435640)Peak memory usage: 85 MB
% 9.06/2.30 % (3435640)Instructions burned: 2 (million)
% 9.06/2.30 % (3435642)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3337785657:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 9.06/2.30 % (3435638)Instruction limit reached!
% 9.06/2.30 % (3435638)------------------------------
% 9.06/2.30 % (3435638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435638)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435638)Termination reason: Instruction limit
% 9.06/2.30 % (3435638)Termination phase: Function definition elimination
% 9.06/2.30 % (3435638)Time elapsed: 0.016 s
% 9.06/2.30 % (3435638)Peak memory usage: 87 MB
% 9.06/2.30 % (3435638)Instructions burned: 27 (million)
% 9.06/2.30 % (3435639)Instruction limit reached!
% 9.06/2.30 % (3435639)------------------------------
% 9.06/2.30 % (3435639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435639)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435639)Termination reason: Instruction limit
% 9.06/2.30 % (3435639)Termination phase: Saturation
% 9.06/2.30 % (3435639)Time elapsed: 0.020 s
% 9.06/2.30 % (3435639)Peak memory usage: 88 MB
% 9.06/2.30 % (3435639)Instructions burned: 37 (million)
% 9.06/2.30 % (3435642)Instruction limit reached!
% 9.06/2.30 % (3435642)------------------------------
% 9.06/2.30 % (3435642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435642)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435642)Termination reason: Instruction limit
% 9.06/2.30 % (3435642)Termination phase: SInE selection
% 9.06/2.30 % (3435642)Time elapsed: 0.005 s
% 9.06/2.30 % (3435642)Peak memory usage: 86 MB
% 9.06/2.30 % (3435642)Instructions burned: 9 (million)
% 9.06/2.30 % (3435644)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=654659322:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi)
% 9.06/2.30 % (3435634)Instruction limit reached!
% 9.06/2.30 % (3435634)------------------------------
% 9.06/2.30 % (3435634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435634)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435634)Termination reason: Instruction limit
% 9.06/2.30 % (3435634)Termination phase: Saturation
% 9.06/2.30 % (3435634)Time elapsed: 0.103 s
% 9.06/2.30 % (3435634)Peak memory usage: 121 MB
% 9.06/2.30 % (3435634)Instructions burned: 128 (million)
% 9.06/2.30 % (3435647)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2346359115:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 9.06/2.30 % (3435647)Instruction limit reached!
% 9.06/2.30 % (3435647)------------------------------
% 9.06/2.30 % (3435647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435647)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435647)Termination reason: Instruction limit
% 9.06/2.30 % (3435647)Termination phase: Property scanning
% 9.06/2.30 % (3435647)Time elapsed: 0.007 s
% 9.06/2.30 % (3435647)Peak memory usage: 86 MB
% 9.06/2.30 % (3435647)Instructions burned: 13 (million)
% 9.06/2.30 % (3435654)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=12901024:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi)
% 9.06/2.30 % (3435644)Instruction limit reached!
% 9.06/2.30 % (3435644)------------------------------
% 9.06/2.30 % (3435644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435644)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435644)Termination reason: Instruction limit
% 9.06/2.30 % (3435644)Termination phase: Saturation
% 9.06/2.30 % (3435644)Time elapsed: 0.109 s
% 9.06/2.30 % (3435644)Peak memory usage: 92 MB
% 9.06/2.30 % (3435644)Instructions burned: 373 (million)
% 9.06/2.30 % (3435660)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3318588751:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 9.06/2.30 % (3435660)Instruction limit reached!
% 9.06/2.30 % (3435660)------------------------------
% 9.06/2.30 % (3435660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435660)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435660)Termination reason: Instruction limit
% 9.06/2.30 % (3435660)Termination phase: Preprocessing 1
% 9.06/2.30 % (3435660)Time elapsed: 0.006 s
% 9.06/2.30 % (3435660)Peak memory usage: 86 MB
% 9.06/2.30 % (3435660)Instructions burned: 11 (million)
% 9.06/2.30 % (3435665)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=3662119677:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi)
% 9.06/2.30 % (3435664)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4153994779:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi)
% 9.06/2.30 % (3435654)Refutation not found, incomplete strategy
% 9.06/2.30 % (3435654)------------------------------
% 9.06/2.30 % (3435654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435654)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435654)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.30 % (3435654)Time elapsed: 0.037 s
% 9.06/2.30 % (3435654)Peak memory usage: 116 MB
% 9.06/2.30 % (3435654)Instructions burned: 26 (million)
% 9.06/2.30 % (3435677)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=1578838464:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 9.06/2.30 % (3435665)Instruction limit reached!
% 9.06/2.30 % (3435665)------------------------------
% 9.06/2.30 % (3435665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435665)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435665)Termination reason: Instruction limit
% 9.06/2.30 % (3435665)Termination phase: Saturation
% 9.06/2.30 % (3435665)Time elapsed: 0.043 s
% 9.06/2.30 % (3435665)Peak memory usage: 91 MB
% 9.06/2.30 % (3435665)Instructions burned: 76 (million)
% 9.06/2.30 % (3435664)Instruction limit reached!
% 9.06/2.30 % (3435664)------------------------------
% 9.06/2.30 % (3435664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435664)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435664)Termination reason: Instruction limit
% 9.06/2.30 % (3435664)Termination phase: Saturation
% 9.06/2.30 % (3435664)Time elapsed: 0.081 s
% 9.06/2.30 % (3435664)Peak memory usage: 131 MB
% 9.06/2.30 % (3435664)Instructions burned: 72 (million)
% 9.06/2.30 % (3435677)First to succeed.
% 9.06/2.30 % (3435677)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3435538"
% 9.06/2.30 % (3435698)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2468834978:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 9.06/2.30 % (3435705)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3475679665:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 9.06/2.30 % (3435710)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2237903755:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 9.06/2.30 % (3435710)Instruction limit reached!
% 9.06/2.30 % (3435710)------------------------------
% 9.06/2.30 % (3435710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435710)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435710)Termination reason: Instruction limit
% 9.06/2.30 % (3435710)Termination phase: Property scanning
% 9.06/2.30 % (3435710)Time elapsed: 0.021 s
% 9.06/2.30 % (3435710)Peak memory usage: 88 MB
% 9.06/2.30 % (3435710)Instructions burned: 41 (million)
% 9.06/2.30 % (3435734)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=275316135:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 9.06/2.30 % (3435698)Instruction limit reached!
% 9.06/2.30 % (3435698)------------------------------
% 9.06/2.30 % (3435698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435698)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435698)Termination reason: Instruction limit
% 9.06/2.30 % (3435698)Termination phase: Saturation
% 9.06/2.30 % (3435698)Time elapsed: 0.103 s
% 9.06/2.30 % (3435698)Peak memory usage: 121 MB
% 9.06/2.30 % (3435698)Instructions burned: 132 (million)
% 9.06/2.30 % (3435741)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1283850794:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 9.06/2.30 % (3435705)Instruction limit reached!
% 9.06/2.30 % (3435705)------------------------------
% 9.06/2.30 % (3435705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435705)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435705)Termination reason: Instruction limit
% 9.06/2.30 % (3435705)Termination phase: Saturation
% 9.06/2.30 % (3435705)Time elapsed: 0.124 s
% 9.06/2.30 % (3435705)Peak memory usage: 138 MB
% 9.06/2.30 % (3435705)Instructions burned: 132 (million)
% 9.06/2.30 % (3435754)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2598914548:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 9.06/2.30 % (3435654)------------------------------
% 9.06/2.30 % (3435654)------------------------------
% 9.06/2.30 % (3435754)Instruction limit reached!
% 9.06/2.30 % (3435754)------------------------------
% 9.06/2.30 % (3435754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435754)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435754)Termination reason: Instruction limit
% 9.06/2.30 % (3435754)Termination phase: Saturation
% 9.06/2.30 % (3435754)Time elapsed: 0.050 s
% 9.06/2.30 % (3435754)Peak memory usage: 115 MB
% 9.06/2.30 % (3435754)Instructions burned: 131 (million)
% 9.06/2.30 % (3435741)Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.06/2.30 % (3435741)------------------------------
% 9.06/2.30 % (3435741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.30 % (3435741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.30 % (3435741)CaDiCaL version: 2.1.3
% 9.06/2.30 % (3435741)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.06/2.30 % (3435741)Time elapsed: 0.132 s
% 9.06/2.30 % (3435741)Peak memory usage: 138 MB
% 9.06/2.30 % (3435741)Instructions burned: 132 (million)
% 9.06/2.30 % (3435741)------------------------------
% 9.06/2.30 % (3435741)------------------------------
% 9.06/2.30 % (3435677)Refutation found. Thanks to Tanya!
% 9.06/2.30 % SZS status Theorem for theBenchmark
% 9.06/2.30 % SZS output start Proof for theBenchmark
% See solution above
% 9.90/2.49 % (3435677)------------------------------
% 9.90/2.49 % (3435677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/2.49 % (3435677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/2.49 % (3435677)CaDiCaL version: 2.1.3
% 9.90/2.49 % (3435677)Termination reason: Refutation
% 9.90/2.49 % (3435677)Time elapsed: 0.072 s
% 9.90/2.49 % (3435677)Peak memory usage: 92 MB
% 9.90/2.49 % (3435677)Instructions burned: 113 (million)
% 9.90/2.49 % (3435677)------------------------------
% 9.90/2.49 % (3435677)------------------------------
% 9.90/2.49 % (3435538)Success in time 1.547 s
% 9.90/2.49 % Vampire exiting
%------------------------------------------------------------------------------