%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW827_1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:37:54 PM UTC 2026
% Result : Unsatisfiable 24.00s 4.08s
% Output : Refutation 24.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 33 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 45 ( 44 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 25 ( 13 ~; 0 |; 12 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 3 avg)
% Number arithmetic : 6 ( 0 atm; 0 fun; 0 num; 6 var)
% Number of types : 72 ( 69 usr; 2 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-4 aty)
% Number of functors : 451 ( 451 usr; 95 con; 0-5 aty)
% Number of variables : 43 ( 36 !; 7 ?; 43 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'S2': $tType ).
tff(type_def_6,type,
'S31': $tType ).
tff(type_def_7,type,
'S8': $tType ).
tff(type_def_8,type,
'S35': $tType ).
tff(type_def_9,type,
'S9': $tType ).
tff(type_def_10,type,
'S10': $tType ).
tff(type_def_11,type,
'S42': $tType ).
tff(type_def_12,type,
'S65': $tType ).
tff(type_def_13,type,
'S43': $tType ).
tff(type_def_14,type,
'S12': $tType ).
tff(type_def_15,type,
'S47': $tType ).
tff(type_def_16,type,
'S55': $tType ).
tff(type_def_17,type,
'S4': $tType ).
tff(type_def_18,type,
'S54': $tType ).
tff(type_def_19,type,
'S50': $tType ).
tff(type_def_20,type,
'S6': $tType ).
tff(type_def_21,type,
'S20': $tType ).
tff(type_def_22,type,
'S41': $tType ).
tff(type_def_23,type,
'S23': $tType ).
tff(type_def_24,type,
'S5': $tType ).
tff(type_def_25,type,
'S64': $tType ).
tff(type_def_26,type,
'S25': $tType ).
tff(type_def_27,type,
'S28': $tType ).
tff(type_def_28,type,
'S32': $tType ).
tff(type_def_29,type,
'S1': $tType ).
tff(type_def_30,type,
'S3': $tType ).
tff(type_def_31,type,
'S49': $tType ).
tff(type_def_32,type,
'S52': $tType ).
tff(type_def_33,type,
'S69': $tType ).
tff(type_def_34,type,
'S68': $tType ).
tff(type_def_35,type,
'S19': $tType ).
tff(type_def_36,type,
'S39': $tType ).
tff(type_def_37,type,
'S13': $tType ).
tff(type_def_38,type,
'S33': $tType ).
tff(type_def_39,type,
'S40': $tType ).
tff(type_def_40,type,
'S22': $tType ).
tff(type_def_41,type,
'S37': $tType ).
tff(type_def_42,type,
'S67': $tType ).
tff(type_def_43,type,
'S38': $tType ).
tff(type_def_44,type,
'S30': $tType ).
tff(type_def_45,type,
'S60': $tType ).
tff(type_def_46,type,
'S46': $tType ).
tff(type_def_47,type,
'S53': $tType ).
tff(type_def_48,type,
'S59': $tType ).
tff(type_def_49,type,
'S45': $tType ).
tff(type_def_50,type,
'S24': $tType ).
tff(type_def_51,type,
'S56': $tType ).
tff(type_def_52,type,
'S14': $tType ).
tff(type_def_53,type,
'S51': $tType ).
tff(type_def_54,type,
'S16': $tType ).
tff(type_def_55,type,
'S58': $tType ).
tff(type_def_56,type,
'S62': $tType ).
tff(type_def_57,type,
'S63': $tType ).
tff(type_def_58,type,
'S48': $tType ).
tff(type_def_59,type,
'S36': $tType ).
tff(type_def_60,type,
'S7': $tType ).
tff(type_def_61,type,
'S66': $tType ).
tff(type_def_62,type,
'S34': $tType ).
tff(type_def_63,type,
'S17': $tType ).
tff(type_def_64,type,
'S18': $tType ).
tff(type_def_65,type,
'S15': $tType ).
tff(type_def_66,type,
'S26': $tType ).
tff(type_def_67,type,
'S27': $tType ).
tff(type_def_68,type,
'S61': $tType ).
tff(type_def_69,type,
'S29': $tType ).
tff(type_def_70,type,
'S57': $tType ).
tff(type_def_71,type,
'S11': $tType ).
tff(type_def_72,type,
'S21': $tType ).
tff(type_def_73,type,
'S44': $tType ).
tff(func_def_0,type,
f4: 'S3' ).
tff(func_def_1,type,
f74: ( 'S39' * 'S6' ) > 'S38' ).
tff(func_def_2,type,
f116: 'S55' ).
tff(func_def_3,type,
f24: 'S7' ).
tff(func_def_4,type,
f137: ( 'S60' * 'S29' ) > 'S2' ).
tff(func_def_5,type,
f132: 'S11' ).
tff(func_def_6,type,
f49: 'S24' ).
tff(func_def_7,type,
f16: 'S9' ).
tff(func_def_8,type,
f23: 'S7' ).
tff(func_def_9,type,
f6: 'S4' ).
tff(func_def_10,type,
f131: 'S9' ).
tff(func_def_11,type,
f149: 'S67' ).
tff(func_def_12,type,
f7: ( 'S5' * $int ) > 'S2' ).
tff(func_def_13,type,
f125: 'S2' ).
tff(func_def_14,type,
f81: 'S23' ).
tff(func_def_15,type,
f14: ( 'S9' * $real ) > 'S8' ).
tff(func_def_16,type,
f141: ( 'S62' * 'S9' ) > 'S4' ).
tff(func_def_17,type,
f88: ( 'S47' * $int ) > 'S6' ).
tff(func_def_18,type,
f100: 'S42' ).
tff(func_def_19,type,
f79: ( 'S42' * 'S13' ) > 'S41' ).
tff(func_def_20,type,
f127: 'S2' ).
tff(func_def_21,type,
f51: 'S25' ).
tff(func_def_22,type,
f44: ( 'S23' * 'S13' ) > 'S12' ).
tff(func_def_23,type,
f150: ( 'S68' * 'S49' ) > 'S49' ).
tff(func_def_24,type,
f120: 'S12' ).
tff(func_def_25,type,
f103: 'S42' ).
tff(func_def_26,type,
f32: ( 'S19' * 'S8' ) > 'S8' ).
tff(func_def_27,type,
f114: ( 'S54' * 'S2' ) > 'S4' ).
tff(func_def_28,type,
f53: ( 'S27' * 'S12' ) > 'S26' ).
tff(func_def_29,type,
f8: 'S5' ).
tff(func_def_30,type,
f66: 'S35' ).
tff(func_def_31,type,
f47: ( 'S25' * 'S3' ) > 'S4' ).
tff(func_def_32,type,
f50: 'S18' ).
tff(func_def_33,type,
f75: 'S39' ).
tff(func_def_34,type,
f76: ( 'S40' * 'S2' ) > 'S7' ).
tff(func_def_35,type,
f139: 'S61' ).
tff(func_def_36,type,
f106: 'S46' ).
tff(func_def_37,type,
f119: 'S57' ).
tff(func_def_38,type,
f147: ( 'S66' * 'S18' ) > 'S23' ).
tff(func_def_39,type,
f39: ( 'S22' * 'S3' ) > 'S7' ).
tff(func_def_40,type,
f152: 'S69' ).
tff(func_def_41,type,
f64: ( 'S34' * 'S29' ) > $real ).
tff(func_def_42,type,
f45: ( 'S24' * 'S12' ) > 'S23' ).
tff(func_def_43,type,
f70: 'S37' ).
tff(func_def_44,type,
f146: 'S65' ).
tff(func_def_45,type,
f42: 'S18' ).
tff(func_def_46,type,
f155: ( 'S15' * 'S13' * 'S13' ) > 'S1' ).
tff(func_def_47,type,
f26: ( 'S15' * 'S13' ) > 'S13' ).
tff(func_def_48,type,
f98: 'S49' ).
tff(func_def_49,type,
f37: 'S21' ).
tff(func_def_50,type,
f40: 'S22' ).
tff(func_def_51,type,
f126: 'S2' ).
tff(func_def_52,type,
f117: ( 'S56' * 'S2' ) > 'S47' ).
tff(func_def_53,type,
f67: ( 'S36' * 'S13' ) > 'S14' ).
tff(func_def_54,type,
f133: 'S2' ).
tff(func_def_55,type,
f144: ( 'S64' * 'S11' ) > 'S47' ).
tff(func_def_56,type,
f61: ( 'S32' * 'S2' ) > 'S3' ).
tff(func_def_57,type,
f60: 'S11' ).
tff(func_def_58,type,
f83: ( 'S44' * $real ) > 'S43' ).
tff(func_def_59,type,
f124: 'S12' ).
tff(func_def_60,type,
f28: ( 'S17' * 'S15' ) > 'S16' ).
tff(func_def_61,type,
f118: ( 'S57' * $int ) > 'S56' ).
tff(func_def_62,type,
f9: ( 'S6' * 'S2' ) > $int ).
tff(func_def_63,type,
f56: ( 'S30' * 'S12' ) > 'S28' ).
tff(func_def_64,type,
f101: 'S44' ).
tff(func_def_65,type,
f59: 'S2' > 'S31' ).
tff(func_def_66,type,
f73: ( 'S38' * 'S2' ) > 'S6' ).
tff(func_def_67,type,
f82: ( 'S43' * $real ) > 'S32' ).
tff(func_def_68,type,
f68: 'S36' ).
tff(func_def_69,type,
f87: 'S46' ).
tff(func_def_70,type,
f78: ( 'S41' * 'S13' ) > 'S26' ).
tff(func_def_71,type,
f97: 'S49' ).
tff(func_def_72,type,
f134: ( 'S58' * 'S29' ) > $int ).
tff(func_def_73,type,
f84: 'S44' ).
tff(func_def_74,type,
f52: ( 'S26' * 'S2' ) > 'S12' ).
tff(func_def_75,type,
f36: ( 'S21' * 'S12' ) > 'S14' ).
tff(func_def_76,type,
f99: 'S46' ).
tff(func_def_77,type,
f105: 'S51' ).
tff(func_def_78,type,
f95: ( 'S51' * 'S2' ) > 'S50' ).
tff(func_def_79,type,
f138: ( 'S61' * 'S48' ) > 'S60' ).
tff(func_def_80,type,
f3: ( 'S3' * 'S2' ) > $real ).
tff(func_def_81,type,
f123: 'S13' ).
tff(func_def_82,type,
f35: 'S9' ).
tff(func_def_83,type,
f135: ( 'S59' * 'S6' ) > 'S58' ).
tff(func_def_84,type,
f57: 'S30' ).
tff(func_def_85,type,
f27: ( 'S16' * 'S15' ) > 'S15' ).
tff(func_def_86,type,
f63: 'S33' ).
tff(func_def_87,type,
f90: 'S42' ).
tff(func_def_88,type,
f72: 'S33' ).
tff(func_def_89,type,
f58: ( 'S31' * 'S2' ) > 'S29' ).
tff(func_def_90,type,
f30: ( 'S18' * 'S13' ) > 'S15' ).
tff(func_def_91,type,
f86: ( 'S46' * $int ) > 'S45' ).
tff(func_def_92,type,
f19: 'S11' ).
tff(func_def_93,type,
f111: ( 'S52' * 'S2' ) > 'S23' ).
tff(func_def_94,type,
f12: 'S7' ).
tff(func_def_95,type,
f109: 'S51' ).
tff(func_def_96,type,
f1: 'S1' ).
tff(func_def_97,type,
f128: 'S10' ).
tff(func_def_98,type,
f29: 'S17' ).
tff(func_def_99,type,
f13: ( 'S8' * $real ) > $real ).
tff(func_def_100,type,
f25: 'S8' ).
tff(func_def_101,type,
f96: 'S51' ).
tff(func_def_102,type,
f140: ( 'S2' * 'S29' ) > 'S1' ).
tff(func_def_103,type,
f92: ( 'S48' * 'S2' ) > 'S2' ).
tff(func_def_104,type,
f113: 'S53' ).
tff(func_def_105,type,
f153: 'S15' ).
tff(func_def_106,type,
f54: 'S27' ).
tff(func_def_107,type,
f15: 'S9' ).
tff(func_def_108,type,
f69: ( 'S37' * $real ) > 'S7' ).
tff(func_def_109,type,
f38: 'S18' ).
tff(func_def_110,type,
f148: ( 'S67' * 'S13' ) > 'S66' ).
tff(func_def_111,type,
f48: 'S25' ).
tff(func_def_112,type,
f46: 'S24' ).
tff(func_def_113,type,
f80: 'S42' ).
tff(func_def_114,type,
f110: 'S46' ).
tff(func_def_115,type,
f145: ( 'S65' * $int ) > 'S64' ).
tff(func_def_116,type,
f91: 'S44' ).
tff(func_def_117,type,
f93: ( 'S49' * 'S2' ) > 'S48' ).
tff(func_def_118,type,
f18: ( 'S11' * $int ) > 'S10' ).
tff(func_def_119,type,
f43: 'S22' ).
tff(func_def_120,type,
f2: 'S1' ).
tff(func_def_121,type,
f130: 'S11' ).
tff(func_def_122,type,
f11: ( 'S7' * 'S3' ) > 'S3' ).
tff(func_def_123,type,
f104: 'S44' ).
tff(func_def_124,type,
f33: ( 'S20' * 'S8' ) > 'S19' ).
tff(func_def_125,type,
f129: 'S9' ).
tff(func_def_126,type,
f94: ( 'S50' * 'S2' ) > 'S49' ).
tff(func_def_127,type,
f34: 'S20' ).
tff(func_def_128,type,
f22: 'S14' ).
tff(func_def_129,type,
f17: ( 'S10' * $int ) > $int ).
tff(func_def_130,type,
f10: 'S6' ).
tff(func_def_131,type,
f151: ( 'S69' * 'S2' ) > 'S68' ).
tff(func_def_132,type,
f142: ( 'S63' * $real ) > 'S62' ).
tff(func_def_133,type,
f112: ( 'S53' * 'S13' ) > 'S52' ).
tff(func_def_134,type,
f136: 'S59' ).
tff(func_def_135,type,
f102: 'S46' ).
tff(func_def_136,type,
f122: 'S3' ).
tff(func_def_137,type,
f65: ( 'S35' * 'S3' ) > 'S34' ).
tff(func_def_138,type,
f115: ( 'S55' * $real ) > 'S54' ).
tff(func_def_139,type,
f20: ( 'S12' * 'S2' ) > 'S13' ).
tff(func_def_140,type,
f107: 'S42' ).
tff(func_def_141,type,
f71: 'S27' ).
tff(func_def_142,type,
f108: 'S44' ).
tff(func_def_143,type,
f143: 'S63' ).
tff(func_def_144,type,
f55: ( 'S28' * 'S29' ) > 'S13' ).
tff(func_def_145,type,
f154: ( 'S8' * $real * $real ) > 'S1' ).
tff(func_def_146,type,
f21: ( 'S14' * 'S12' ) > 'S12' ).
tff(func_def_147,type,
f62: ( 'S33' * 'S3' ) > 'S32' ).
tff(func_def_148,type,
f85: ( 'S45' * $int ) > 'S38' ).
tff(func_def_149,type,
f89: 'S47' ).
tff(func_def_150,type,
f5: ( 'S4' * $real ) > 'S3' ).
tff(func_def_151,type,
f121: 'S13' ).
tff(func_def_152,type,
f77: 'S40' ).
tff(func_def_153,type,
f41: 'S21' ).
tff(func_def_154,type,
f31: 'S18' ).
tff(func_def_171,type,
sK1: ( $real * $real ) > $real ).
tff(func_def_172,type,
sK2: ( $real * $real ) > 'S2' ).
tff(func_def_173,type,
sK3: ( 'S2' * 'S13' ) > 'S12' ).
tff(func_def_174,type,
sK4: ( $real * $real ) > $real ).
tff(func_def_175,type,
sK5: ( 'S2' * 'S13' ) > 'S12' ).
tff(func_def_176,type,
sK6: ( 'S2' * 'S13' ) > $int ).
tff(func_def_177,type,
sK7: ( $int * $int * 'S2' ) > 'S29' ).
tff(func_def_178,type,
sK8: ( $real * $real ) > $real ).
tff(func_def_179,type,
sK9: $real > 'S2' ).
tff(func_def_180,type,
sK10: ( 'S2' * $real * 'S2' ) > 'S3' ).
tff(func_def_181,type,
sK11: ( 'S6' * 'S2' ) > 'S2' ).
tff(func_def_182,type,
sK12: ( 'S6' * 'S2' ) > 'S58' ).
tff(func_def_183,type,
sK13: ( $real * $real * $real ) > 'S8' ).
tff(func_def_184,type,
sK14: ( $real * $real * $real * $real ) > $real ).
tff(func_def_185,type,
sK15: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_186,type,
sK16: $real > $real ).
tff(func_def_187,type,
sK17: ( $real * $real * $real ) > 'S8' ).
tff(func_def_188,type,
sK18: ( 'S12' * 'S2' * 'S2' ) > $int ).
tff(func_def_189,type,
sK19: ( 'S12' * 'S2' * 'S2' ) > $int ).
tff(func_def_190,type,
sK20: 'S2' > $int ).
tff(func_def_191,type,
sK21: ( $int * $int * $int ) > 'S10' ).
tff(func_def_192,type,
sK22: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_193,type,
sK23: ( $int * $int * $int * $int ) > $int ).
tff(func_def_194,type,
sK24: ( 'S2' * $real ) > 'S3' ).
tff(func_def_195,type,
sK25: $real > $real ).
tff(func_def_196,type,
sK26: $real > $real ).
tff(func_def_197,type,
sK27: ( 'S2' * $int ) > 'S6' ).
tff(func_def_198,type,
sK28: $real > $real ).
tff(func_def_199,type,
sK29: ( $real * $real ) > 'S8' ).
tff(func_def_200,type,
sK30: ( 'S2' * 'S2' * 'S6' * 'S2' ) > 'S31' ).
tff(func_def_201,type,
sK31: ( 'S2' * 'S2' * 'S6' * 'S2' ) > 'S58' ).
tff(func_def_202,type,
sK32: ( 'S2' * 'S2' * 'S6' * 'S2' ) > $int ).
tff(func_def_203,type,
sK33: $real > $real ).
tff(func_def_204,type,
sK34: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_205,type,
sK35: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_206,type,
sK36: $real > $real ).
tff(func_def_207,type,
sK37: 'S13' ).
tff(func_def_208,type,
sK38: 'S12' ).
tff(func_def_209,type,
sK39: ( 'S2' * $real ) > 'S3' ).
tff(func_def_210,type,
sK40: ( 'S2' * $real ) > $real ).
tff(func_def_211,type,
sK41: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S13' ).
tff(func_def_212,type,
sK42: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_213,type,
sK43: ( 'S2' * $real * 'S2' * $real ) > 'S3' ).
tff(func_def_214,type,
sK44: ( 'S2' * $real * 'S2' * $real ) > 'S2' ).
tff(func_def_215,type,
sK45: ( $real * $real * $real * $real * $real ) > 'S8' ).
tff(func_def_216,type,
sK46: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_217,type,
sK47: ( 'S2' * 'S2' ) > 'S2' ).
tff(func_def_218,type,
sK48: ( $int * $int * 'S2' ) > 'S29' ).
tff(func_def_219,type,
sK49: ( 'S2' * 'S12' * 'S2' ) > 'S31' ).
tff(func_def_220,type,
sK50: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_221,type,
sK51: ( 'S2' * 'S2' * 'S2' ) > 'S29' ).
tff(func_def_222,type,
sK52: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_223,type,
sK53: ( 'S2' * 'S2' * 'S12' * 'S2' ) > $int ).
tff(func_def_224,type,
sK54: ( $real * $real * $real ) > 'S8' ).
tff(func_def_225,type,
sK55: ( 'S2' * 'S2' * $int * $int ) > 'S6' ).
tff(func_def_226,type,
sK56: ( $int * $int * $int ) > 'S10' ).
tff(func_def_227,type,
sK57: ( 'S2' * 'S13' ) > 'S12' ).
tff(func_def_228,type,
sK58: ( 'S2' * 'S13' * 'S13' ) > 'S29' ).
tff(func_def_229,type,
sK59: ( $real * 'S2' * 'S2' ) > $int ).
tff(func_def_230,type,
sK60: ( $real * 'S2' * 'S2' ) > $int ).
tff(func_def_231,type,
sK61: ( $real * 'S2' * 'S2' ) > 'S3' ).
tff(func_def_232,type,
sK62: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_233,type,
sK63: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_234,type,
sK64: ( $real * 'S2' ) > 'S3' ).
tff(func_def_235,type,
sK65: ( 'S13' * 'S2' * 'S2' ) > 'S12' ).
tff(func_def_236,type,
sK66: 'S12' ).
tff(func_def_237,type,
sK67: 'S13' ).
tff(func_def_238,type,
sK68: 'S13' ).
tff(func_def_239,type,
sK69: ( $real * $real ) > $real ).
tff(func_def_240,type,
sK70: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_241,type,
sK71: $real ).
tff(func_def_242,type,
sK72: 'S2' > $real ).
tff(func_def_243,type,
sK73: $real > $real ).
tff(func_def_244,type,
sK74: ( $real * $real * $real ) > 'S8' ).
tff(func_def_245,type,
sK75: ( 'S2' * 'S2' * 'S2' ) > $int ).
tff(func_def_246,type,
sK76: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_247,type,
sK77: ( 'S2' * 'S2' * 'S2' ) > $int ).
tff(func_def_248,type,
sK78: ( 'S2' * 'S12' ) > 'S2' ).
tff(func_def_249,type,
sK79: ( 'S2' * 'S12' ) > 'S28' ).
tff(func_def_250,type,
sK80: ( 'S2' * 'S2' * 'S2' ) > 'S29' ).
tff(func_def_251,type,
sK81: ( $real * 'S2' * 'S2' ) > 'S3' ).
tff(func_def_252,type,
sK82: 'S2' > 'S2' ).
tff(func_def_253,type,
sK83: $real > $real ).
tff(func_def_254,type,
sK84: ( 'S2' * 'S2' * 'S2' ) > $int ).
tff(func_def_255,type,
sK85: ( 'S2' * 'S2' * 'S2' ) > 'S10' ).
tff(func_def_256,type,
sK86: ( $real * $real * $real ) > $real ).
tff(func_def_257,type,
sK87: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_258,type,
sK88: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_259,type,
sK89: ( 'S13' * 'S2' * 'S2' ) > $int ).
tff(func_def_260,type,
sK90: ( 'S13' * 'S2' * 'S2' ) > 'S12' ).
tff(func_def_261,type,
sK91: ( 'S13' * 'S2' * 'S2' ) > $int ).
tff(func_def_262,type,
sK92: ( $real * $real * $real ) > $real ).
tff(func_def_263,type,
sK93: 'S2' > $int ).
tff(func_def_264,type,
sK94: $real > $real ).
tff(func_def_265,type,
sK95: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_266,type,
sK96: ( $real * $real * 'S2' * 'S2' ) > 'S3' ).
tff(func_def_267,type,
sK97: ( 'S2' * 'S13' ) > 'S12' ).
tff(func_def_268,type,
sK98: $real > $real ).
tff(func_def_269,type,
sK99: ( $int * 'S2' ) > 'S6' ).
tff(func_def_270,type,
sK100: ( $real * $real ) > $real ).
tff(func_def_271,type,
sK101: ( $real * $real * $real ) > $real ).
tff(func_def_272,type,
sK102: ( 'S13' * 'S15' * 'S13' * 'S13' * 'S15' ) > 'S13' ).
tff(func_def_273,type,
sK103: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_274,type,
sK104: ( 'S2' * 'S13' ) > 'S12' ).
tff(func_def_275,type,
sK105: ( 'S2' * 'S13' ) > 'S13' ).
tff(func_def_276,type,
sK106: ( 'S2' * 'S2' * 'S3' * 'S2' ) > $int ).
tff(func_def_277,type,
sK107: ( 'S2' * 'S2' * 'S3' * 'S2' ) > 'S34' ).
tff(func_def_278,type,
sK108: ( 'S2' * 'S2' * 'S3' * 'S2' ) > 'S31' ).
tff(func_def_279,type,
sK109: ( 'S3' * 'S2' * 'S2' ) > 'S31' ).
tff(func_def_280,type,
sK110: ( 'S3' * 'S2' * 'S2' ) > 'S34' ).
tff(func_def_281,type,
sK111: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_282,type,
sK112: ( 'S13' * 'S2' ) > 'S13' ).
tff(func_def_283,type,
sK113: ( 'S3' * 'S2' * 'S2' ) > 'S31' ).
tff(func_def_284,type,
sK114: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_285,type,
sK115: ( $int * $int * $int ) > 'S10' ).
tff(func_def_286,type,
sK116: ( $int * $int * $int ) > 'S10' ).
tff(func_def_287,type,
sK117: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_288,type,
sK118: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_289,type,
sK119: ( 'S2' * $real ) > 'S3' ).
tff(func_def_290,type,
sK120: ( $real * $real ) > $real ).
tff(func_def_291,type,
sK121: ( $int * $int * $int * $int * $int ) > 'S10' ).
tff(func_def_292,type,
sK122: ( $int * 'S2' ) > 'S6' ).
tff(func_def_293,type,
sK123: ( $int * $int ) > 'S2' ).
tff(func_def_294,type,
sK124: ( $real * $real * $real ) > 'S8' ).
tff(func_def_295,type,
sK125: ( $real * $real * $real ) > 'S8' ).
tff(func_def_296,type,
sK126: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_297,type,
sK127: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_298,type,
sK128: ( 'S2' * 'S3' ) > 'S2' ).
tff(func_def_299,type,
sK129: ( 'S2' * 'S3' ) > 'S34' ).
tff(func_def_300,type,
sK130: ( $real * $real ) > $real ).
tff(func_def_301,type,
sK131: $real > 'S2' ).
tff(func_def_302,type,
sK132: 'S2' > $real ).
tff(func_def_303,type,
sK133: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_304,type,
sK134: ( 'S13' * 'S13' * 'S2' * 'S2' ) > 'S2' ).
tff(func_def_305,type,
sK135: ( 'S13' * 'S13' * 'S2' * 'S2' ) > 'S12' ).
tff(func_def_306,type,
sK136: ( 'S3' * 'S2' * 'S2' ) > 'S34' ).
tff(func_def_307,type,
sK137: ( 'S3' * 'S2' * 'S2' ) > 'S31' ).
tff(func_def_308,type,
sK138: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_309,type,
sK139: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_310,type,
sK140: ( $int * $int * $int ) > 'S10' ).
tff(func_def_311,type,
sK141: 'S2' > $real ).
tff(func_def_312,type,
sK142: ( 'S2' * $int * $int * 'S2' ) > 'S2' ).
tff(func_def_313,type,
sK143: ( 'S2' * $int * $int * 'S2' ) > 'S6' ).
tff(func_def_314,type,
sK144: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_315,type,
sK145: ( 'S2' * 'S13' * 'S2' * 'S13' ) > 'S12' ).
tff(func_def_316,type,
sK146: ( $int * 'S2' * 'S2' ) > 'S6' ).
tff(func_def_317,type,
sK147: ( 'S2' * 'S2' ) > 'S2' ).
tff(func_def_318,type,
sK148: ( 'S2' * 'S2' ) > $int ).
tff(func_def_319,type,
sK149: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_320,type,
sK150: ( $real * 'S2' ) > 'S3' ).
tff(func_def_321,type,
sK151: ( 'S2' * 'S2' ) > $int ).
tff(func_def_322,type,
sK152: ( $real * $real * 'S2' ) > 'S2' ).
tff(func_def_323,type,
sK153: ( 'S2' * $real * $real ) > 'S29' ).
tff(func_def_324,type,
sK154: ( $int * 'S2' ) > 'S6' ).
tff(func_def_325,type,
sK155: ( $real * $real * $real ) > 'S8' ).
tff(func_def_326,type,
sK156: $real ).
tff(func_def_327,type,
sK157: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_328,type,
sK158: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S13' ).
tff(func_def_329,type,
sK159: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_330,type,
sK160: ( 'S2' * 'S6' * 'S2' ) > 'S31' ).
tff(func_def_331,type,
sK161: ( 'S2' * 'S6' * 'S2' ) > 'S58' ).
tff(func_def_332,type,
sK162: ( 'S2' * $int ) > 'S6' ).
tff(func_def_333,type,
sK163: ( 'S2' * $int ) > $int ).
tff(func_def_334,type,
sK164: ( 'S2' * 'S2' * 'S3' ) > $int ).
tff(func_def_335,type,
sK165: ( 'S2' * 'S2' * 'S3' ) > $int ).
tff(func_def_336,type,
sK166: ( 'S2' * $int * $int ) > 'S29' ).
tff(func_def_337,type,
sK167: ( 'S2' * $real * $real ) > 'S29' ).
tff(func_def_338,type,
sK168: ( $real * $real * $real ) > $real ).
tff(func_def_339,type,
sK169: ( $real * $real * $real ) > 'S8' ).
tff(func_def_340,type,
sK170: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_341,type,
sK171: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_342,type,
sK172: ( 'S2' * 'S13' * 'S2' ) > 'S12' ).
tff(func_def_343,type,
sK173: ( $real * $real ) > $real ).
tff(func_def_344,type,
sK174: $real > $real ).
tff(func_def_345,type,
sK175: ( $real * $real * 'S2' ) > 'S29' ).
tff(func_def_346,type,
sK176: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_347,type,
sK177: ( $int * $int * $int ) > 'S10' ).
tff(func_def_348,type,
sK178: ( $real * $real * $real * $real ) > $real ).
tff(func_def_349,type,
sK179: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_350,type,
sK180: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_351,type,
sK181: ( $int * $int * 'S2' ) > 'S2' ).
tff(func_def_352,type,
sK182: ( $real * $real * $real ) > 'S8' ).
tff(func_def_353,type,
sK183: ( $real * $real * $real ) > 'S8' ).
tff(func_def_354,type,
sK184: $real > $real ).
tff(func_def_355,type,
sK185: ( 'S2' * 'S2' * 'S2' ) > 'S48' ).
tff(func_def_356,type,
sK186: ( 'S3' * 'S29' ) > 'S2' ).
tff(func_def_357,type,
sK187: ( 'S2' * 'S2' * $int ) > $int ).
tff(func_def_358,type,
sK188: ( 'S2' * 'S2' * $int ) > $int ).
tff(func_def_359,type,
sK189: ( 'S2' * 'S2' * $int ) > 'S6' ).
tff(func_def_360,type,
sK190: ( 'S13' * 'S2' * 'S2' ) > 'S12' ).
tff(func_def_361,type,
sK191: ( 'S2' * 'S3' * 'S2' ) > 'S34' ).
tff(func_def_362,type,
sK192: ( 'S2' * 'S3' * 'S2' ) > 'S31' ).
tff(func_def_363,type,
sK193: ( 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_364,type,
sK194: ( $real * $real * $real ) > 'S8' ).
tff(func_def_365,type,
sK195: ( $real * 'S2' ) > $real ).
tff(func_def_366,type,
sK196: ( $real * 'S2' ) > $real ).
tff(func_def_367,type,
sK197: $real ).
tff(func_def_368,type,
sK198: ( $real * 'S2' ) > $real ).
tff(func_def_369,type,
sK199: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_370,type,
sK200: ( $real * $real * $real ) > 'S8' ).
tff(func_def_371,type,
sK201: ( $real * $real * $real ) > 'S8' ).
tff(func_def_372,type,
sK202: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_373,type,
sK203: ( 'S2' * 'S13' ) > 'S15' ).
tff(func_def_374,type,
sK204: $real > $real ).
tff(func_def_375,type,
sK205: ( 'S13' * 'S13' * 'S2' ) > 'S29' ).
tff(func_def_376,type,
sK206: $real > $real ).
tff(func_def_377,type,
sK207: ( 'S8' * $real * 'S8' * $real * $real ) > $real ).
tff(func_def_378,type,
sK208: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_379,type,
sK209: ( $real * $real ) > 'S2' ).
tff(func_def_380,type,
sK210: ( $real * $real ) > $real ).
tff(func_def_381,type,
sK211: ( 'S2' * 'S13' ) > 'S13' ).
tff(func_def_382,type,
sK212: ( 'S2' * $int ) > 'S6' ).
tff(func_def_383,type,
sK213: ( 'S2' * $int ) > $int ).
tff(func_def_384,type,
sK214: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_385,type,
sK215: ( $real * $real * $real * $real ) > $real ).
tff(func_def_386,type,
sK216: ( $int * 'S2' ) > 'S6' ).
tff(func_def_387,type,
sK217: ( 'S2' * $real * 'S2' ) > 'S3' ).
tff(func_def_388,type,
sK218: $int > $int ).
tff(func_def_389,type,
sK219: ( $real * 'S2' ) > 'S3' ).
tff(func_def_390,type,
sK220: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_391,type,
sK221: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_392,type,
sK222: ( $real * $real ) > $real ).
tff(func_def_393,type,
sK223: $real ).
tff(func_def_394,type,
sK224: ( 'S2' * 'S2' ) > 'S2' ).
tff(func_def_395,type,
sK225: ( $int * 'S2' ) > 'S6' ).
tff(func_def_396,type,
sK226: ( 'S2' * 'S2' ) > 'S2' ).
tff(func_def_397,type,
sK227: ( 'S2' * 'S2' ) > $int ).
tff(func_def_398,type,
sK228: ( 'S2' * 'S2' ) > $int ).
tff(func_def_399,type,
sK229: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_400,type,
sK230: ( $int * $int * $int * $int ) > 'S10' ).
tff(func_def_401,type,
sK231: ( $real * 'S2' ) > 'S3' ).
tff(func_def_402,type,
sK232: ( $real * $real ) > 'S2' ).
tff(func_def_403,type,
sK233: ( $real * $real * $real ) > 'S8' ).
tff(func_def_404,type,
sK234: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_405,type,
sK235: ( 'S2' * 'S2' ) > $int ).
tff(func_def_406,type,
sK236: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_407,type,
sK237: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_408,type,
sK238: ( $int * 'S2' ) > 'S6' ).
tff(func_def_409,type,
sK239: ( 'S2' * $real ) > 'S3' ).
tff(func_def_410,type,
sK240: ( $real * $real ) > $real ).
tff(func_def_411,type,
sK241: ( $real * 'S2' ) > $real ).
tff(func_def_412,type,
sK242: ( $real * 'S2' ) > 'S3' ).
tff(func_def_413,type,
sK243: ( 'S29' * 'S12' ) > 'S2' ).
tff(func_def_414,type,
sK244: ( 'S13' * 'S13' * 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_415,type,
sK245: ( 'S12' * 'S2' * 'S2' ) > 'S31' ).
tff(func_def_416,type,
sK246: ( 'S12' * 'S2' * 'S2' ) > 'S28' ).
tff(func_def_417,type,
sK247: ( 'S2' * 'S13' * 'S2' ) > $int ).
tff(func_def_418,type,
sK248: ( 'S2' * 'S13' * 'S2' ) > 'S12' ).
tff(func_def_419,type,
sK249: ( 'S2' * 'S13' * 'S2' ) > $int ).
tff(func_def_420,type,
sK250: ( 'S2' * $real ) > 'S3' ).
tff(func_def_421,type,
sK251: ( 'S2' * $real ) > $real ).
tff(func_def_422,type,
sK252: ( $real * $real ) > 'S2' ).
tff(func_def_423,type,
sK253: ( $real * 'S2' ) > $int ).
tff(func_def_424,type,
sK254: ( $real * 'S2' ) > 'S3' ).
tff(func_def_425,type,
sK255: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_426,type,
sK256: ( 'S29' * 'S3' ) > $real ).
tff(func_def_427,type,
sK257: $real > $real ).
tff(func_def_428,type,
sK258: ( 'S2' * $real * 'S2' ) > 'S3' ).
tff(func_def_429,type,
sK259: ( 'S2' * $real * 'S2' ) > $int ).
tff(func_def_430,type,
sK260: ( 'S2' * $real * 'S2' ) > $int ).
tff(func_def_431,type,
sK261: ( $real * $real * $real ) > 'S8' ).
tff(func_def_432,type,
sK262: ( $real * 'S8' * $real ) > $real ).
tff(func_def_433,type,
sK263: ( $real * 'S8' * $real ) > $real ).
tff(func_def_434,type,
sK264: ( $real * 'S8' * $real ) > 'S8' ).
tff(func_def_435,type,
sK265: $real > $real ).
tff(func_def_436,type,
sK266: ( 'S13' * 'S2' * 'S2' ) > 'S12' ).
tff(func_def_437,type,
sK267: ( 'S2' * $real ) > 'S3' ).
tff(func_def_438,type,
sK268: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_439,type,
sK269: $real > $real ).
tff(func_def_440,type,
sK270: ( 'S2' * 'S13' * 'S13' ) > 'S29' ).
tff(func_def_441,type,
sK271: $real > $real ).
tff(func_def_442,type,
sK272: ( 'S2' * 'S2' * 'S2' * 'S3' ) > $int ).
tff(func_def_443,type,
sK273: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_444,type,
sK274: ( $real * $real * $real * $real ) > $real ).
tff(func_def_445,type,
sK275: ( 'S2' * $real * 'S2' ) > 'S3' ).
tff(func_def_446,type,
sK276: $real > $real ).
tff(func_def_447,type,
sK277: ( $int * 'S2' ) > $int ).
tff(func_def_448,type,
sK278: ( 'S2' * 'S12' * 'S2' * 'S2' ) > 'S31' ).
tff(func_def_449,type,
sK279: ( 'S2' * 'S12' * 'S2' * 'S2' ) > $int ).
tff(func_def_450,type,
sK280: ( 'S2' * 'S12' * 'S2' * 'S2' ) > 'S28' ).
tff(func_def_451,type,
sK281: ( 'S2' * $real ) > 'S3' ).
tff(func_def_452,type,
sK282: ( 'S2' * $real ) > $real ).
tff(func_def_453,type,
sK283: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_454,type,
sK284: ( 'S2' * 'S2' ) > 'S2' ).
tff(func_def_455,type,
sK285: $real > $real ).
tff(func_def_456,type,
sK286: ( 'S2' * 'S2' ) > 'S48' ).
tff(func_def_457,type,
sK287: ( $int * 'S2' * 'S2' ) > 'S6' ).
tff(func_def_458,type,
sK288: $real > $real ).
tff(func_def_459,type,
sK289: ( 'S2' * $real ) > 'S8' ).
tff(func_def_460,type,
sK290: ( 'S13' * 'S2' ) > 'S12' ).
tff(func_def_461,type,
sK291: ( $real * $real * $real * $real ) > 'S8' ).
tff(func_def_462,type,
sK292: ( 'S2' * $int ) > $int ).
tff(func_def_463,type,
sK293: ( 'S2' * $int ) > 'S6' ).
tff(func_def_464,type,
sK294: ( 'S2' * 'S13' * 'S13' ) > 'S2' ).
tff(func_def_465,type,
sK295: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(func_def_466,type,
sK296: ( 'S13' * 'S13' * 'S13' ) > 'S15' ).
tff(pred_def_5,type,
sP0: ( $real * $real * $real * $real ) > $o ).
tff(f50,axiom,
? [X0: 'S12'] :
( ( X0 = f44(f81,f26(f30(f31,f123),f20(f124,f125))) )
& ? [X1: 'S13'] :
( ? [X2: 'S13'] :
( ( X2 = f26(f30(f38,X1),f123) )
& ( f26(f30(f31,f26(f30(f38,f20(f44(f81,X1),f125)),f123)),X2) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(X0,f125)),f126)),f123)),X2) ) )
& ( X1 = f20(X0,f126) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_50) ).
tff(f55,axiom,
! [X1: 'S2',X0: 'S13'] :
? [X2: 'S15'] :
( ( X2 = f30(f31,f123) )
& ( f26(X2,f20(f44(f81,X0),X1)) = f20(f44(f81,f26(X2,X0)),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_55) ).
tff(f132,axiom,
! [X1: $int,X0: $int] : ( f17(f18(f60,X0),X1) = f17(f18(f60,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_132) ).
tff(f324,axiom,
! [X0: 'S13',X2: 'S2',X1: 'S2'] :
? [X3: 'S12'] :
( ( f20(f44(f81,f20(X3,X1)),X2) = f20(X3,f7(f8,f17(f18(f60,f9(f10,X1)),f9(f10,X2)))) )
& ( X3 = f44(f81,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_324) ).
tff(f636,plain,
! [X0: 'S13',X1: 'S2',X2: 'S2'] :
? [X3: 'S12'] :
( ( f20(X3,f7(f8,f17(f18(f60,f9(f10,X2)),f9(f10,X1)))) = f20(f44(f81,f20(X3,X2)),X1) )
& ( X3 = f44(f81,X0) ) ),
inference(rectify,[],[f324]) ).
tff(f808,plain,
! [X0: $int,X1: $int] : ( f17(f18(f60,X0),X1) = f17(f18(f60,X1),X0) ),
inference(rectify,[],[f132]) ).
tff(f889,plain,
! [X0: 'S2',X1: 'S13'] :
? [X2: 'S15'] :
( ( X2 = f30(f31,f123) )
& ( f20(f44(f81,f26(X2,X1)),X0) = f26(X2,f20(f44(f81,X1),X0)) ) ),
inference(rectify,[],[f55]) ).
tff(f1145,plain,
( ( f44(f81,f26(f30(f31,f123),f20(f124,f125))) = sK66 )
& ( f26(f30(f38,sK67),f123) = sK68 )
& ( f26(f30(f31,f26(f30(f38,f20(f44(f81,sK67),f125)),f123)),sK68) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(sK66,f125)),f126)),f123)),sK68) )
& ( sK67 = f20(sK66,f126) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66,sK67,sK68]),skolemize(X0,sK66),skolemize(X1,sK67),skolemize(X2,sK68)],[f50]) ).
tff(f1388,plain,
! [X0: 'S13',X1: 'S2',X2: 'S2'] :
( ( f20(f44(f81,f20(sK190(X0,X1,X2),X2)),X1) = f20(sK190(X0,X1,X2),f7(f8,f17(f18(f60,f9(f10,X2)),f9(f10,X1)))) )
& ( f44(f81,X0) = sK190(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK190]),skolemize(X3,sK190(X0,X1,X2))],[f636]) ).
tff(f1408,plain,
! [X0: 'S2',X1: 'S13'] :
( ( f30(f31,f123) = sK203(X0,X1) )
& ( f20(f44(f81,f26(sK203(X0,X1),X1)),X0) = f26(sK203(X0,X1),f20(f44(f81,X1),X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK203]),skolemize(X2,sK203(X0,X1))],[f889]) ).
tff(f1621,plain,
! [X0: $int,X1: $int] : ( f17(f18(f60,X0),X1) = f17(f18(f60,X1),X0) ),
inference(cnf_transformation,[],[f808]) ).
tff(f1802,plain,
sK67 = f20(sK66,f126),
inference(cnf_transformation,[],[f1145]) ).
tff(f1803,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,sK67),f125)),f123)),sK68) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(sK66,f125)),f126)),f123)),sK68),
inference(cnf_transformation,[],[f1145]) ).
tff(f1804,plain,
f26(f30(f38,sK67),f123) = sK68,
inference(cnf_transformation,[],[f1145]) ).
tff(f1805,plain,
f44(f81,f26(f30(f31,f123),f20(f124,f125))) = sK66,
inference(cnf_transformation,[],[f1145]) ).
tff(f2197,plain,
! [X2: 'S2',X0: 'S13',X1: 'S2'] : ( f44(f81,X0) = sK190(X0,X1,X2) ),
inference(cnf_transformation,[],[f1388]) ).
tff(f2198,plain,
! [X2: 'S2',X0: 'S13',X1: 'S2'] : ( f20(f44(f81,f20(sK190(X0,X1,X2),X2)),X1) = f20(sK190(X0,X1,X2),f7(f8,f17(f18(f60,f9(f10,X2)),f9(f10,X1)))) ),
inference(cnf_transformation,[],[f1388]) ).
tff(f2227,plain,
! [X0: 'S2',X1: 'S13'] : ( f20(f44(f81,f26(sK203(X0,X1),X1)),X0) = f26(sK203(X0,X1),f20(f44(f81,X1),X0)) ),
inference(cnf_transformation,[],[f1408]) ).
tff(f2228,plain,
! [X0: 'S2',X1: 'S13'] : ( f30(f31,f123) = sK203(X0,X1) ),
inference(cnf_transformation,[],[f1408]) ).
tff(f2708,plain,
! [X2: 'S2',X0: 'S13',X1: 'S2'] : ( f20(f44(f81,X0),f7(f8,f17(f18(f60,f9(f10,X2)),f9(f10,X1)))) = f20(f44(f81,f20(f44(f81,X0),X2)),X1) ),
inference(definition_unfolding,[],[f2198,f2197,f2197]) ).
tff(f2721,plain,
! [X0: 'S2',X1: 'S13'] : ( f26(f30(f31,f123),f20(f44(f81,X1),X0)) = f20(f44(f81,f26(f30(f31,f123),X1)),X0) ),
inference(definition_unfolding,[],[f2227,f2228,f2228]) ).
tff(f3062,plain,
sK68 = f26(f30(f38,f20(sK66,f126)),f123),
inference(forward_demodulation,[],[f1804,f1802]) ).
tff(f3069,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(sK66,f126)),f125)),f123)),sK68) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(sK66,f125)),f126)),f123)),sK68),
inference(forward_demodulation,[],[f1803,f1802]) ).
tff(f3940,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f125)),f123)),sK68) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),sK68),
inference(superposition,[],[f3069,f1805]) ).
tff(f3942,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f20(sK66,f126)),f123)) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f125)),f123)),f26(f30(f38,f20(sK66,f126)),f123)),
inference(forward_demodulation,[],[f3940,f3062]) ).
tff(f3944,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f123)) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f125)),f123)),f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f123)),
inference(forward_demodulation,[],[f3942,f1805]) ).
tff(f13434,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f123)) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f7(f8,f17(f18(f60,f9(f10,f126)),f9(f10,f125))))),f123)),f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f126)),f123)),
inference(superposition,[],[f3944,f2708]) ).
tff(f13436,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)) != f26(f30(f31,f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f7(f8,f17(f18(f60,f9(f10,f126)),f9(f10,f125))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)),
inference(forward_demodulation,[],[f13434,f2721]) ).
tff(f13459,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)) != f26(f30(f31,f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f7(f8,f17(f18(f60,f9(f10,f126)),f9(f10,f125)))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)),
inference(forward_demodulation,[],[f13436,f2721]) ).
tff(f13477,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f125)),f126)),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)) != f26(f30(f31,f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f7(f8,f17(f18(f60,f9(f10,f125)),f9(f10,f126)))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)),
inference(forward_demodulation,[],[f13459,f1621]) ).
tff(f13482,plain,
f26(f30(f31,f26(f30(f38,f20(f44(f81,f26(f30(f31,f123),f20(f124,f125))),f7(f8,f17(f18(f60,f9(f10,f125)),f9(f10,f126))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)) != f26(f30(f31,f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f7(f8,f17(f18(f60,f9(f10,f125)),f9(f10,f126)))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)),
inference(forward_demodulation,[],[f13477,f2708]) ).
tff(f13485,plain,
f26(f30(f31,f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f7(f8,f17(f18(f60,f9(f10,f125)),f9(f10,f126)))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)) != f26(f30(f31,f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f7(f8,f17(f18(f60,f9(f10,f125)),f9(f10,f126)))))),f123)),f26(f30(f38,f26(f30(f31,f123),f20(f44(f81,f20(f124,f125)),f126))),f123)),
inference(forward_demodulation,[],[f13482,f2721]) ).
tff(f13486,plain,
$false,
inference(trivial_inequality_removal,[],[f13485]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW827_1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 14:32:42 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 3.39/1.21 % (1634936)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.39/1.21 % (1634967)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3685057822:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.39/1.21 % (1634967)Instruction limit reached!
% 3.39/1.21 % (1634967)------------------------------
% 3.39/1.21 % (1634967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.21 % (1634967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.21 % (1634967)CaDiCaL version: 2.1.3
% 3.39/1.21 % (1634967)Termination reason: Instruction limit
% 3.39/1.21 % (1634967)Termination phase: Property scanning
% 3.39/1.21 % (1634967)Time elapsed: 0.002 s
% 3.39/1.21 % (1634967)Peak memory usage: 86 MB
% 3.39/1.21 % (1634967)Instructions burned: 5 (million)
% 3.39/1.21 % (1634969)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2565085284:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.39/1.21 % (1634966)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2788418009:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.39/1.21 % (1634963)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1242430111:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.39/1.21 % (1634965)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=821545502:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.39/1.21 % (1634968)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2297459941:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.39/1.21 % (1634964)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2758306037:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.39/1.21 % (1634966)Instruction limit reached!
% 3.39/1.21 % (1634966)------------------------------
% 3.39/1.21 % (1634966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.21 % (1634966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.21 % (1634966)CaDiCaL version: 2.1.3
% 3.39/1.21 % (1634966)Termination reason: Instruction limit
% 3.39/1.21 % (1634966)Termination phase: Property scanning
% 3.39/1.21 % (1634966)Time elapsed: 0.004 s
% 3.39/1.21 % (1634966)Peak memory usage: 85 MB
% 3.39/1.21 % (1634966)Instructions burned: 7 (million)
% 3.39/1.21 % (1634963)Instruction limit reached!
% 3.39/1.21 % (1634963)------------------------------
% 3.39/1.21 % (1634963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.21 % (1634963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.21 % (1634963)CaDiCaL version: 2.1.3
% 3.39/1.21 % (1634963)Termination reason: Instruction limit
% 3.39/1.21 % (1634963)Termination phase: Property scanning
% 3.39/1.21 % (1634963)Time elapsed: 0.006 s
% 3.39/1.21 % (1634963)Peak memory usage: 85 MB
% 3.39/1.21 % (1634963)Instructions burned: 14 (million)
% 3.39/1.21 % (1634969)Instruction limit reached!
% 3.39/1.21 % (1634969)------------------------------
% 3.39/1.21 % (1634969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.21 % (1634969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.21 % (1634969)CaDiCaL version: 2.1.3
% 3.39/1.21 % (1634969)Termination reason: Instruction limit
% 3.39/1.21 % (1634969)Termination phase: Preprocessing 3
% 3.39/1.21 % (1634969)Time elapsed: 0.017 s
% 3.39/1.21 % (1634969)Peak memory usage: 87 MB
% 3.39/1.21 % (1634969)Instructions burned: 34 (million)
% 3.39/1.21 % (1634968)Instruction limit reached!
% 3.39/1.21 % (1634968)------------------------------
% 3.39/1.21 % (1634968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.39/1.21 % (1634968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.39/1.21 % (1634968)CaDiCaL version: 2.1.3
% 3.39/1.21 % (1634968)Termination reason: Instruction limit
% 3.39/1.21 % (1634968)Termination phase: Property scanning
% 3.39/1.21 % (1634968)Time elapsed: 0.024 s
% 3.39/1.21 % (1634968)Peak memory usage: 87 MB
% 3.39/1.21 % (1634968)Instructions burned: 46 (million)
% 3.39/1.21 % (1634971)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1413223449:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.39/1.21 % (1634971)Instruction limit reached!
% 3.39/1.21 % (1634971)------------------------------
% 4.00/1.36 % (1634971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634971)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634971)Termination reason: Instruction limit
% 4.00/1.36 % (1634971)Termination phase: SInE selection
% 4.00/1.36 % (1634971)Time elapsed: 0.004 s
% 4.00/1.36 % (1634971)Peak memory usage: 86 MB
% 4.00/1.36 % (1634971)Instructions burned: 14 (million)
% 4.00/1.36 % (1634978)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=47554041:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 4.00/1.36 % (1634979)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2272503073:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.00/1.36 % (1634965)Instruction limit reached!
% 4.00/1.36 % (1634965)------------------------------
% 4.00/1.36 % (1634965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634965)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634965)Termination reason: Instruction limit
% 4.00/1.36 % (1634965)Termination phase: Saturation
% 4.00/1.36 % (1634965)Time elapsed: 0.148 s
% 4.00/1.36 % (1634965)Peak memory usage: 119 MB
% 4.00/1.36 % (1634965)Instructions burned: 202 (million)
% 4.00/1.36 % (1634979)Instruction limit reached!
% 4.00/1.36 % (1634979)------------------------------
% 4.00/1.36 % (1634979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634979)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634979)Termination reason: Instruction limit
% 4.00/1.36 % (1634979)Termination phase: Preprocessing 1
% 4.00/1.36 % (1634979)Time elapsed: 0.009 s
% 4.00/1.36 % (1634979)Peak memory usage: 86 MB
% 4.00/1.36 % (1634979)Instructions burned: 16 (million)
% 4.00/1.36 % (1634978)Instruction limit reached!
% 4.00/1.36 % (1634978)------------------------------
% 4.00/1.36 % (1634978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634978)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634978)Termination reason: Instruction limit
% 4.00/1.36 % (1634978)Termination phase: Preprocessing 3
% 4.00/1.36 % (1634978)Time elapsed: 0.016 s
% 4.00/1.36 % (1634978)Peak memory usage: 87 MB
% 4.00/1.36 % (1634978)Instructions burned: 30 (million)
% 4.00/1.36 % (1634981)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=43915377:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.00/1.36 % (1634980)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3605965307:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.00/1.36 % (1634980)Instruction limit reached!
% 4.00/1.36 % (1634980)------------------------------
% 4.00/1.36 % (1634980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634980)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634980)Termination reason: Instruction limit
% 4.00/1.36 % (1634980)Termination phase: Preprocessing 1
% 4.00/1.36 % (1634980)Time elapsed: 0.013 s
% 4.00/1.36 % (1634980)Peak memory usage: 86 MB
% 4.00/1.36 % (1634980)Instructions burned: 26 (million)
% 4.00/1.36 % (1634981)Instruction limit reached!
% 4.00/1.36 % (1634981)------------------------------
% 4.00/1.36 % (1634981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.36 % (1634981)CaDiCaL version: 2.1.3
% 4.00/1.36 % (1634981)Termination reason: Instruction limit
% 4.00/1.36 % (1634981)Termination phase: shuffling
% 4.00/1.36 % (1634981)Time elapsed: 0.014 s
% 4.00/1.36 % (1634981)Peak memory usage: 86 MB
% 4.00/1.36 % (1634981)Instructions burned: 28 (million)
% 4.00/1.36 % (1634964)Instruction limit reached!
% 4.00/1.36 % (1634964)------------------------------
% 4.00/1.36 % (1634964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.36 % (1634964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634964)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634964)Termination reason: Instruction limit
% 5.52/1.55 % (1634964)Termination phase: Saturation
% 5.52/1.55 % (1634964)Time elapsed: 0.208 s
% 5.52/1.55 % (1634964)Peak memory usage: 119 MB
% 5.52/1.55 % (1634964)Instructions burned: 308 (million)
% 5.52/1.55 % (1634983)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=477402585:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.52/1.55 % (1634983)Instruction limit reached!
% 5.52/1.55 % (1634983)------------------------------
% 5.52/1.55 % (1634983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.55 % (1634983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634983)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634983)Termination reason: Instruction limit
% 5.52/1.55 % (1634983)Termination phase: Property scanning
% 5.52/1.55 % (1634983)Time elapsed: 0.024 s
% 5.52/1.55 % (1634983)Peak memory usage: 88 MB
% 5.52/1.55 % (1634983)Instructions burned: 89 (million)
% 5.52/1.55 % (1634989)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1586034284:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.52/1.55 % (1634986)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=722882314:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.52/1.55 % (1634986)Instruction limit reached!
% 5.52/1.55 % (1634986)------------------------------
% 5.52/1.55 % (1634986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.55 % (1634986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634986)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634986)Termination reason: Instruction limit
% 5.52/1.55 % (1634986)Termination phase: shuffling
% 5.52/1.55 % (1634986)Time elapsed: 0.002 s
% 5.52/1.55 % (1634986)Peak memory usage: 85 MB
% 5.52/1.55 % (1634986)Instructions burned: 2 (million)
% 5.52/1.55 % (1634989)Refutation not found, incomplete strategy
% 5.52/1.55 % (1634989)------------------------------
% 5.52/1.55 % (1634989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.55 % (1634989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634989)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634989)Termination reason: Refutation not found, incomplete strategy
% 5.52/1.55 % (1634989)Time elapsed: 0.010 s
% 5.52/1.55 % (1634989)Peak memory usage: 88 MB
% 5.52/1.55 % (1634989)Instructions burned: 17 (million)
% 5.52/1.55 % (1634990)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=313168512:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.52/1.55 % (1634991)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3967654948:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.52/1.55 % (1634992)lrs+10_1_thi=all:si=on:fd=off:random_seed=2872837481:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.52/1.55 % (1634990)Instruction limit reached!
% 5.52/1.55 % (1634990)------------------------------
% 5.52/1.55 % (1634990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.55 % (1634990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634990)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634990)Termination reason: Instruction limit
% 5.52/1.55 % (1634990)Termination phase: Property scanning
% 5.52/1.55 % (1634990)Time elapsed: 0.004 s
% 5.52/1.55 % (1634990)Peak memory usage: 86 MB
% 5.52/1.55 % (1634990)Instructions burned: 6 (million)
% 5.52/1.55 % (1634995)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2916923653:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.52/1.55 % (1634995)Instruction limit reached!
% 5.52/1.55 % (1634995)------------------------------
% 5.52/1.55 % (1634995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.52/1.55 % (1634995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.55 % (1634995)CaDiCaL version: 2.1.3
% 5.52/1.55 % (1634995)Termination reason: Instruction limit
% 5.52/1.55 % (1634995)Termination phase: Property scanning
% 5.52/1.55 % (1634995)Time elapsed: 0.002 s
% 5.52/1.55 % (1634995)Peak memory usage: 86 MB
% 5.52/1.55 % (1634995)Instructions burned: 6 (million)
% 5.52/1.55 % (1634992)Instruction limit reached!
% 6.44/1.73 % (1634992)------------------------------
% 6.44/1.73 % (1634992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1634992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1634992)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1634992)Termination reason: Instruction limit
% 6.44/1.73 % (1634992)Termination phase: Preprocessing 3
% 6.44/1.73 % (1634992)Time elapsed: 0.026 s
% 6.44/1.73 % (1634992)Peak memory usage: 87 MB
% 6.44/1.73 % (1634992)Instructions burned: 53 (million)
% 6.44/1.73 % (1634991)Instruction limit reached!
% 6.44/1.73 % (1634991)------------------------------
% 6.44/1.73 % (1634991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1634991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1634991)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1634991)Termination reason: Instruction limit
% 6.44/1.73 % (1634991)Termination phase: Property scanning
% 6.44/1.73 % (1634991)Time elapsed: 0.034 s
% 6.44/1.73 % (1634991)Peak memory usage: 88 MB
% 6.44/1.73 % (1634991)Instructions burned: 67 (million)
% 6.44/1.73 % (1634994)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=2585149991:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 6.44/1.73 % (1634994)Instruction limit reached!
% 6.44/1.73 % (1634994)------------------------------
% 6.44/1.73 % (1634994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1634994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1634994)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1634994)Termination reason: Instruction limit
% 6.44/1.73 % (1634994)Termination phase: Property scanning
% 6.44/1.73 % (1634994)Time elapsed: 0.004 s
% 6.44/1.73 % (1634994)Peak memory usage: 85 MB
% 6.44/1.73 % (1634994)Instructions burned: 8 (million)
% 6.44/1.73 % (1635005)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3310566416:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.44/1.73 % (1635002)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2512348386:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 6.44/1.73 % (1634998)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2040754876:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 6.44/1.73 % (1634998)Instruction limit reached!
% 6.44/1.73 % (1634998)------------------------------
% 6.44/1.73 % (1634998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1634998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1634998)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1634998)Termination reason: Instruction limit
% 6.44/1.73 % (1634998)Termination phase: shuffling
% 6.44/1.73 % (1634998)Time elapsed: 0.002 s
% 6.44/1.73 % (1634998)Peak memory usage: 85 MB
% 6.44/1.73 % (1634998)Instructions burned: 2 (million)
% 6.44/1.73 % (1635005)Instruction limit reached!
% 6.44/1.73 % (1635005)------------------------------
% 6.44/1.73 % (1635005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1635005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1635005)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1635005)Termination reason: Instruction limit
% 6.44/1.73 % (1635005)Termination phase: Unused predicate definition removal
% 6.44/1.73 % (1635005)Time elapsed: 0.007 s
% 6.44/1.73 % (1635005)Peak memory usage: 86 MB
% 6.44/1.73 % (1635005)Instructions burned: 28 (million)
% 6.44/1.73 % (1635004)dis+10_1_si=on:random_seed=3308913354:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.44/1.73 % (1635004)Instruction limit reached!
% 6.44/1.73 % (1635004)------------------------------
% 6.44/1.73 % (1635004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.44/1.73 % (1635004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.73 % (1635004)CaDiCaL version: 2.1.3
% 6.44/1.73 % (1635004)Termination reason: Instruction limit
% 6.44/1.73 % (1635004)Termination phase: Property scanning
% 6.44/1.73 % (1635004)Time elapsed: 0.006 s
% 6.44/1.73 % (1635004)Peak memory usage: 86 MB
% 6.44/1.73 % (1635004)Instructions burned: 12 (million)
% 6.44/1.73 % (1635006)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=448481258: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_2994 on theBenchmark for (2994ds/35Mi)
% 7.84/1.98 % (1635006)Instruction limit reached!
% 7.84/1.98 % (1635006)------------------------------
% 7.84/1.98 % (1635006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.98 % (1635006)CaDiCaL version: 2.1.3
% 7.84/1.98 % (1635006)Termination reason: Instruction limit
% 7.84/1.98 % (1635006)Termination phase: Preprocessing 3
% 7.84/1.98 % (1635006)Time elapsed: 0.019 s
% 7.84/1.98 % (1635006)Peak memory usage: 87 MB
% 7.84/1.98 % (1635006)Instructions burned: 35 (million)
% 7.84/1.98 % (1635008)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1478155309:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.84/1.98 % (1635008)Instruction limit reached!
% 7.84/1.98 % (1635008)------------------------------
% 7.84/1.98 % (1635008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.98 % (1635008)CaDiCaL version: 2.1.3
% 7.84/1.98 % (1635008)Termination reason: Instruction limit
% 7.84/1.98 % (1635008)Termination phase: shuffling
% 7.84/1.98 % (1635008)Time elapsed: 0.002 s
% 7.84/1.98 % (1635008)Peak memory usage: 85 MB
% 7.84/1.98 % (1635008)Instructions burned: 2 (million)
% 7.84/1.98 % (1635002)Instruction limit reached!
% 7.84/1.98 % (1635002)------------------------------
% 7.84/1.98 % (1635002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.98 % (1635002)CaDiCaL version: 2.1.3
% 7.84/1.98 % (1635002)Termination reason: Instruction limit
% 7.84/1.98 % (1635002)Termination phase: Saturation
% 7.84/1.98 % (1635002)Time elapsed: 0.093 s
% 7.84/1.98 % (1635002)Peak memory usage: 118 MB
% 7.84/1.98 % (1635002)Instructions burned: 127 (million)
% 7.84/1.98 % (1634989)------------------------------
% 7.84/1.98 % (1634989)------------------------------
% 7.84/1.98 % (1635013)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1966400146:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.84/1.98 % (1635012)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1207881103:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 7.84/1.98 % (1635012)Instruction limit reached!
% 7.84/1.98 % (1635012)------------------------------
% 7.84/1.98 % (1635012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.98 % (1635012)CaDiCaL version: 2.1.3
% 7.84/1.98 % (1635012)Termination reason: Instruction limit
% 7.84/1.98 % (1635012)Termination phase: Property scanning
% 7.84/1.98 % (1635012)Time elapsed: 0.005 s
% 7.84/1.98 % (1635012)Peak memory usage: 86 MB
% 7.84/1.98 % (1635012)Instructions burned: 9 (million)
% 7.84/1.98 % (1635015)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2230908436:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 7.84/1.98 % (1635015)Instruction limit reached!
% 7.84/1.98 % (1635015)------------------------------
% 7.84/1.98 % (1635015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.84/1.98 % (1635015)CaDiCaL version: 2.1.3
% 7.84/1.98 % (1635015)Termination reason: Instruction limit
% 7.84/1.98 % (1635015)Termination phase: Property scanning
% 7.84/1.98 % (1635015)Time elapsed: 0.006 s
% 7.84/1.98 % (1635015)Peak memory usage: 85 MB
% 7.84/1.98 % (1635015)Instructions burned: 13 (million)
% 7.84/1.98 % (1635017)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=434447369:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 7.84/1.98 % (1635019)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3894474437:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 7.84/1.98 % (1635013)Instruction limit reached!
% 7.84/1.98 % (1635013)------------------------------
% 7.84/1.98 % (1635013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.84/1.98 % (1635013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635013)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635013)Termination reason: Instruction limit
% 10.73/2.23 % (1635013)Termination phase: Saturation
% 10.73/2.23 % (1635013)Time elapsed: 0.117 s
% 10.73/2.23 % (1635013)Peak memory usage: 93 MB
% 10.73/2.23 % (1635013)Instructions burned: 371 (million)
% 10.73/2.23 % (1635019)Instruction limit reached!
% 10.73/2.23 % (1635019)------------------------------
% 10.73/2.23 % (1635019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.23 % (1635019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635019)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635019)Termination reason: Instruction limit
% 10.73/2.23 % (1635019)Termination phase: Property scanning
% 10.73/2.23 % (1635019)Time elapsed: 0.006 s
% 10.73/2.23 % (1635019)Peak memory usage: 86 MB
% 10.73/2.23 % (1635019)Instructions burned: 12 (million)
% 10.73/2.23 % (1635021)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=1236772233:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.73/2.23 % (1635020)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3838460789:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.73/2.23 % (1635017)Refutation not found, incomplete strategy
% 10.73/2.23 % (1635017)------------------------------
% 10.73/2.23 % (1635017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.23 % (1635017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635017)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635017)Termination reason: Refutation not found, incomplete strategy
% 10.73/2.23 % (1635017)Time elapsed: 0.040 s
% 10.73/2.23 % (1635017)Peak memory usage: 112 MB
% 10.73/2.23 % (1635017)Instructions burned: 31 (million)
% 10.73/2.23 % (1635020)Instruction limit reached!
% 10.73/2.23 % (1635020)------------------------------
% 10.73/2.23 % (1635020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.23 % (1635020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635020)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635020)Termination reason: Instruction limit
% 10.73/2.23 % (1635020)Termination phase: Function definition elimination
% 10.73/2.23 % (1635020)Time elapsed: 0.037 s
% 10.73/2.23 % (1635020)Peak memory usage: 88 MB
% 10.73/2.23 % (1635020)Instructions burned: 72 (million)
% 10.73/2.23 % (1635021)Instruction limit reached!
% 10.73/2.23 % (1635021)------------------------------
% 10.73/2.23 % (1635021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.23 % (1635021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635021)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635021)Termination reason: Instruction limit
% 10.73/2.23 % (1635021)Termination phase: Saturation
% 10.73/2.23 % (1635021)Time elapsed: 0.038 s
% 10.73/2.23 % (1635021)Peak memory usage: 88 MB
% 10.73/2.23 % (1635021)Instructions burned: 76 (million)
% 10.73/2.23 % (1635024)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=1071203116:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 10.73/2.23 % (1635029)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1430147856:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.73/2.23 % (1635026)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4090172768:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.73/2.23 % (1635030)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=52965829:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 10.73/2.23 % (1635029)Instruction limit reached!
% 10.73/2.23 % (1635029)------------------------------
% 10.73/2.23 % (1635029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.23 % (1635029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.23 % (1635029)CaDiCaL version: 2.1.3
% 10.73/2.23 % (1635029)Termination reason: Instruction limit
% 10.73/2.23 % (1635029)Termination phase: Saturation
% 10.73/2.23 % (1635029)Time elapsed: 0.066 s
% 10.73/2.23 % (1635029)Peak memory usage: 135 MB
% 10.73/2.23 % (1635029)Instructions burned: 132 (million)
% 10.73/2.23 % (1635030)Instruction limit reached!
% 10.73/2.23 % (1635030)------------------------------
% 11.58/2.49 % (1635030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635030)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635030)Termination reason: Instruction limit
% 11.58/2.49 % (1635030)Termination phase: Property scanning
% 11.58/2.49 % (1635030)Time elapsed: 0.018 s
% 11.58/2.49 % (1635030)Peak memory usage: 86 MB
% 11.58/2.49 % (1635030)Instructions burned: 41 (million)
% 11.58/2.49 % (1635026)Instruction limit reached!
% 11.58/2.49 % (1635026)------------------------------
% 11.58/2.49 % (1635026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635026)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635026)Termination reason: Instruction limit
% 11.58/2.49 % (1635026)Termination phase: Saturation
% 11.58/2.49 % (1635026)Time elapsed: 0.091 s
% 11.58/2.49 % (1635026)Peak memory usage: 115 MB
% 11.58/2.49 % (1635026)Instructions burned: 130 (million)
% 11.58/2.49 % (1635033)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1023790147:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 11.58/2.49 % (1635034)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3317669339:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 11.58/2.49 % (1635017)------------------------------
% 11.58/2.49 % (1635017)------------------------------
% 11.58/2.49 % (1635024)Instruction limit reached!
% 11.58/2.49 % (1635024)------------------------------
% 11.58/2.49 % (1635024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635024)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635024)Termination reason: Instruction limit
% 11.58/2.49 % (1635024)Termination phase: Saturation
% 11.58/2.49 % (1635024)Time elapsed: 0.183 s
% 11.58/2.49 % (1635024)Peak memory usage: 93 MB
% 11.58/2.49 % (1635024)Instructions burned: 294 (million)
% 11.58/2.49 % (1635039)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1084973489:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.58/2.49 % (1635040)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=597721564:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 11.58/2.49 % (1635039)Instruction limit reached!
% 11.58/2.49 % (1635039)------------------------------
% 11.58/2.49 % (1635039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635039)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635039)Termination reason: Instruction limit
% 11.58/2.49 % (1635039)Termination phase: Saturation
% 11.58/2.49 % (1635039)Time elapsed: 0.051 s
% 11.58/2.49 % (1635039)Peak memory usage: 118 MB
% 11.58/2.49 % (1635039)Instructions burned: 132 (million)
% 11.58/2.49 % (1635033)Instruction limit reached!
% 11.58/2.49 % (1635033)------------------------------
% 11.58/2.49 % (1635033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635033)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635033)Termination reason: Instruction limit
% 11.58/2.49 % (1635033)Termination phase: Saturation
% 11.58/2.49 % (1635033)Time elapsed: 0.160 s
% 11.58/2.49 % (1635033)Peak memory usage: 93 MB
% 11.58/2.49 % (1635033)Instructions burned: 308 (million)
% 11.58/2.49 % (1635043)dis+10_1_si=on:random_seed=16221144:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 11.58/2.49 % (1635040)Refutation not found, incomplete strategy
% 11.58/2.49 % (1635040)------------------------------
% 11.58/2.49 % (1635040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.58/2.49 % (1635040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.58/2.49 % (1635040)CaDiCaL version: 2.1.3
% 11.58/2.49 % (1635040)Termination reason: Refutation not found, incomplete strategy
% 11.58/2.49 % (1635040)Time elapsed: 0.041 s
% 11.58/2.49 % (1635040)Peak memory usage: 112 MB
% 11.58/2.49 % (1635040)Instructions burned: 34 (million)
% 11.58/2.49 % (1635045)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2873071047:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 13.77/2.76 % (1635044)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=404987765:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 13.77/2.76 % (1635048)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2077962782:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 13.77/2.76 % (1635048)Instruction limit reached!
% 13.77/2.76 % (1635048)------------------------------
% 13.77/2.76 % (1635048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635048)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635048)Termination reason: Instruction limit
% 13.77/2.76 % (1635048)Termination phase: Saturation
% 13.77/2.76 % (1635048)Time elapsed: 0.017 s
% 13.77/2.76 % (1635048)Peak memory usage: 88 MB
% 13.77/2.76 % (1635048)Instructions burned: 65 (million)
% 13.77/2.76 % (1635045)Instruction limit reached!
% 13.77/2.76 % (1635045)------------------------------
% 13.77/2.76 % (1635045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635045)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635045)Termination reason: Instruction limit
% 13.77/2.76 % (1635045)Termination phase: Saturation
% 13.77/2.76 % (1635045)Time elapsed: 0.079 s
% 13.77/2.76 % (1635045)Peak memory usage: 91 MB
% 13.77/2.76 % (1635045)Instructions burned: 142 (million)
% 13.77/2.76 % (1635050)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1303891786:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 13.77/2.76 % (1635050)Instruction limit reached!
% 13.77/2.76 % (1635050)------------------------------
% 13.77/2.76 % (1635050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635050)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635050)Termination reason: Instruction limit
% 13.77/2.76 % (1635050)Termination phase: Saturation
% 13.77/2.76 % (1635050)Time elapsed: 0.063 s
% 13.77/2.76 % (1635050)Peak memory usage: 90 MB
% 13.77/2.76 % (1635050)Instructions burned: 121 (million)
% 13.77/2.76 % (1635040)------------------------------
% 13.77/2.76 % (1635040)------------------------------
% 13.77/2.76 % (1635054)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=3282191891:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 13.77/2.76 % (1635034)Instruction limit reached!
% 13.77/2.76 % (1635034)------------------------------
% 13.77/2.76 % (1635034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635034)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635034)Termination reason: Instruction limit
% 13.77/2.76 % (1635034)Termination phase: Saturation
% 13.77/2.76 % (1635034)Time elapsed: 0.428 s
% 13.77/2.76 % (1635034)Peak memory usage: 139 MB
% 13.77/2.76 % (1635034)Instructions burned: 598 (million)
% 13.77/2.76 % (1635044)Instruction limit reached!
% 13.77/2.76 % (1635044)------------------------------
% 13.77/2.76 % (1635044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635044)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635044)Termination reason: Instruction limit
% 13.77/2.76 % (1635044)Termination phase: Saturation
% 13.77/2.76 % (1635044)Time elapsed: 0.225 s
% 13.77/2.76 % (1635044)Peak memory usage: 97 MB
% 13.77/2.76 % (1635044)Instructions burned: 384 (million)
% 13.77/2.76 % (1635056)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2586060276:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 13.77/2.76 % (1635054)Instruction limit reached!
% 13.77/2.76 % (1635054)------------------------------
% 13.77/2.76 % (1635054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.77/2.76 % (1635054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.77/2.76 % (1635054)CaDiCaL version: 2.1.3
% 13.77/2.76 % (1635054)Termination reason: Instruction limit
% 13.77/2.76 % (1635054)Termination phase: Saturation
% 13.77/2.76 % (1635054)Time elapsed: 0.048 s
% 13.77/2.76 % (1635054)Peak memory usage: 91 MB
% 16.57/3.12 % (1635054)Instructions burned: 129 (million)
% 16.57/3.12 % (1635056)Instruction limit reached!
% 16.57/3.12 % (1635056)------------------------------
% 16.57/3.12 % (1635056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635056)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635056)Termination reason: Instruction limit
% 16.57/3.12 % (1635056)Termination phase: Preprocessing 3
% 16.57/3.12 % (1635056)Time elapsed: 0.021 s
% 16.57/3.12 % (1635056)Peak memory usage: 87 MB
% 16.57/3.12 % (1635056)Instructions burned: 40 (million)
% 16.57/3.12 % (1635057)dis+1010_1_to=kbo:si=on:random_seed=3191860236:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 16.57/3.12 % (1635058)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1162543924:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 16.57/3.12 % (1635060)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=626579488:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 16.57/3.12 % (1635063)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1072836487:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi)
% 16.57/3.12 % (1635062)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3039995569:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 16.57/3.12 % (1635057)Instruction limit reached!
% 16.57/3.12 % (1635057)------------------------------
% 16.57/3.12 % (1635057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635057)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635057)Termination reason: Instruction limit
% 16.57/3.12 % (1635057)Termination phase: Saturation
% 16.57/3.12 % (1635057)Time elapsed: 0.098 s
% 16.57/3.12 % (1635057)Peak memory usage: 91 MB
% 16.57/3.12 % (1635057)Instructions burned: 175 (million)
% 16.57/3.12 % (1635064)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3284460365:st=2:i=295:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/295Mi)
% 16.57/3.12 % (1635064)Refutation not found, incomplete strategy
% 16.57/3.12 % (1635064)------------------------------
% 16.57/3.12 % (1635064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635064)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635064)Termination reason: Refutation not found, incomplete strategy
% 16.57/3.12 % (1635064)Time elapsed: 0.014 s
% 16.57/3.12 % (1635064)Peak memory usage: 88 MB
% 16.57/3.12 % (1635064)Instructions burned: 28 (million)
% 16.57/3.12 % (1635063)Instruction limit reached!
% 16.57/3.12 % (1635063)------------------------------
% 16.57/3.12 % (1635063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635063)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635063)Termination reason: Instruction limit
% 16.57/3.12 % (1635063)Termination phase: Saturation
% 16.57/3.12 % (1635063)Time elapsed: 0.125 s
% 16.57/3.12 % (1635063)Peak memory usage: 120 MB
% 16.57/3.12 % (1635063)Instructions burned: 350 (million)
% 16.57/3.12 % (1635043)Instruction limit reached!
% 16.57/3.12 % (1635043)------------------------------
% 16.57/3.12 % (1635043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635043)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635043)Termination reason: Instruction limit
% 16.57/3.12 % (1635043)Termination phase: Saturation
% 16.57/3.12 % (1635043)Time elapsed: 0.562 s
% 16.57/3.12 % (1635043)Peak memory usage: 98 MB
% 16.57/3.12 % (1635043)Instructions burned: 1001 (million)
% 16.57/3.12 % (1635062)Instruction limit reached!
% 16.57/3.12 % (1635062)------------------------------
% 16.57/3.12 % (1635062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.57/3.12 % (1635062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/3.12 % (1635062)CaDiCaL version: 2.1.3
% 16.57/3.12 % (1635062)Termination reason: Instruction limit
% 18.31/3.37 % (1635062)Termination phase: Saturation
% 18.31/3.37 % (1635062)Time elapsed: 0.157 s
% 18.31/3.37 % (1635062)Peak memory usage: 139 MB
% 18.31/3.37 % (1635062)Instructions burned: 215 (million)
% 18.31/3.37 % (1635070)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2217001018:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.31/3.37 % (1635058)Instruction limit reached!
% 18.31/3.37 % (1635058)------------------------------
% 18.31/3.37 % (1635058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635058)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635058)Termination reason: Instruction limit
% 18.31/3.37 % (1635058)Termination phase: Saturation
% 18.31/3.37 % (1635058)Time elapsed: 0.239 s
% 18.31/3.37 % (1635058)Peak memory usage: 119 MB
% 18.31/3.37 % (1635058)Instructions burned: 330 (million)
% 18.31/3.37 % (1635072)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3758287659:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 18.31/3.37 % (1635073)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=590641711:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 18.31/3.37 % (1635073)Refutation not found, incomplete strategy
% 18.31/3.37 % (1635073)------------------------------
% 18.31/3.37 % (1635073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635073)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635073)Termination reason: Refutation not found, incomplete strategy
% 18.31/3.37 % (1635073)Time elapsed: 0.014 s
% 18.31/3.37 % (1635073)Peak memory usage: 88 MB
% 18.31/3.37 % (1635073)Instructions burned: 27 (million)
% 18.31/3.37 % (1635064)------------------------------
% 18.31/3.37 % (1635064)------------------------------
% 18.31/3.37 % (1635074)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1259710223:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 18.31/3.37 % (1635060)Instruction limit reached!
% 18.31/3.37 % (1635060)------------------------------
% 18.31/3.37 % (1635060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635060)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635060)Termination reason: Instruction limit
% 18.31/3.37 % (1635060)Termination phase: Saturation
% 18.31/3.37 % (1635060)Time elapsed: 0.345 s
% 18.31/3.37 % (1635060)Peak memory usage: 137 MB
% 18.31/3.37 % (1635060)Instructions burned: 484 (million)
% 18.31/3.37 % (1635072)Instruction limit reached!
% 18.31/3.37 % (1635072)------------------------------
% 18.31/3.37 % (1635072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635072)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635072)Termination reason: Instruction limit
% 18.31/3.37 % (1635072)Termination phase: Saturation
% 18.31/3.37 % (1635072)Time elapsed: 0.099 s
% 18.31/3.37 % (1635072)Peak memory usage: 119 MB
% 18.31/3.37 % (1635072)Instructions burned: 283 (million)
% 18.31/3.37 % (1635074)Refutation not found, incomplete strategy
% 18.31/3.37 % (1635074)------------------------------
% 18.31/3.37 % (1635074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635074)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635074)Termination reason: Refutation not found, incomplete strategy
% 18.31/3.37 % (1635074)Time elapsed: 0.040 s
% 18.31/3.37 % (1635074)Peak memory usage: 112 MB
% 18.31/3.37 % (1635074)Instructions burned: 32 (million)
% 18.31/3.37 % (1635076)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1097237247:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi)
% 18.31/3.37 % (1635076)Refutation not found, incomplete strategy
% 18.31/3.37 % (1635076)------------------------------
% 18.31/3.37 % (1635076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.37 % (1635076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.37 % (1635076)CaDiCaL version: 2.1.3
% 18.31/3.37 % (1635076)Termination reason: Refutation not found, incomplete strategy
% 19.90/3.77 % (1635076)Time elapsed: 0.039 s
% 19.90/3.77 % (1635076)Peak memory usage: 112 MB
% 19.90/3.77 % (1635076)Instructions burned: 31 (million)
% 19.90/3.77 % (1635070)Instruction limit reached!
% 19.90/3.77 % (1635070)------------------------------
% 19.90/3.77 % (1635070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.77 % (1635070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.77 % (1635070)CaDiCaL version: 2.1.3
% 19.90/3.77 % (1635070)Termination reason: Instruction limit
% 19.90/3.77 % (1635070)Termination phase: Saturation
% 19.90/3.77 % (1635070)Time elapsed: 0.225 s
% 19.90/3.77 % (1635070)Peak memory usage: 120 MB
% 19.90/3.77 % (1635070)Instructions burned: 330 (million)
% 19.90/3.77 % (1635080)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3052733632:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 19.90/3.77 % (1635082)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2955746073:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 19.90/3.77 % (1635081)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=242074994:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 19.90/3.77 % (1635073)------------------------------
% 19.90/3.77 % (1635073)------------------------------
% 19.90/3.77 % (1635084)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1207256546:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 19.90/3.77 % (1635082)Instruction limit reached!
% 19.90/3.77 % (1635082)------------------------------
% 19.90/3.77 % (1635082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.77 % (1635082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.77 % (1635082)CaDiCaL version: 2.1.3
% 19.90/3.77 % (1635082)Termination reason: Instruction limit
% 19.90/3.77 % (1635082)Termination phase: Saturation
% 19.90/3.77 % (1635082)Time elapsed: 0.131 s
% 19.90/3.77 % (1635082)Peak memory usage: 121 MB
% 19.90/3.77 % (1635082)Instructions burned: 376 (million)
% 19.90/3.77 % (1635074)------------------------------
% 19.90/3.77 % (1635074)------------------------------
% 19.90/3.77 % (1635084)Refutation not found, incomplete strategy
% 19.90/3.77 % (1635084)------------------------------
% 19.90/3.77 % (1635084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.77 % (1635084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.77 % (1635084)CaDiCaL version: 2.1.3
% 19.90/3.77 % (1635084)Termination reason: Refutation not found, incomplete strategy
% 19.90/3.77 % (1635084)Time elapsed: 0.040 s
% 19.90/3.77 % (1635084)Peak memory usage: 112 MB
% 19.90/3.77 % (1635084)Instructions burned: 35 (million)
% 19.90/3.77 % (1635076)------------------------------
% 19.90/3.77 % (1635076)------------------------------
% 19.90/3.77 % (1635081)Instruction limit reached!
% 19.90/3.77 % (1635081)------------------------------
% 19.90/3.77 % (1635081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.77 % (1635081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.77 % (1635081)CaDiCaL version: 2.1.3
% 19.90/3.77 % (1635081)Termination reason: Instruction limit
% 19.90/3.77 % (1635081)Termination phase: Saturation
% 19.90/3.77 % (1635081)Time elapsed: 0.210 s
% 19.90/3.77 % (1635081)Peak memory usage: 136 MB
% 19.90/3.77 % (1635081)Instructions burned: 277 (million)
% 19.90/3.77 % (1635088)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3258980311:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 19.90/3.77 % (1635090)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1968499473:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 19.90/3.77 % (1635091)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1445519981:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 19.90/3.77 % (1635092)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=571784427:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 19.90/3.77 % (1635080)Instruction limit reached!
% 19.90/3.77 % (1635080)------------------------------
% 24.00/4.08 % (1635080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635080)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635080)Termination reason: Instruction limit
% 24.00/4.08 % (1635080)Termination phase: Saturation
% 24.00/4.08 % (1635080)Time elapsed: 0.315 s
% 24.00/4.08 % (1635080)Peak memory usage: 122 MB
% 24.00/4.08 % (1635080)Instructions burned: 472 (million)
% 24.00/4.08 % (1635093)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2393346111:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi)
% 24.00/4.08 % (1635093)Refutation not found, incomplete strategy
% 24.00/4.08 % (1635093)------------------------------
% 24.00/4.08 % (1635093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635093)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635093)Termination reason: Refutation not found, incomplete strategy
% 24.00/4.08 % (1635093)Time elapsed: 0.035 s
% 24.00/4.08 % (1635093)Peak memory usage: 111 MB
% 24.00/4.08 % (1635093)Instructions burned: 23 (million)
% 24.00/4.08 % (1635084)------------------------------
% 24.00/4.08 % (1635084)------------------------------
% 24.00/4.08 % (1635092)Instruction limit reached!
% 24.00/4.08 % (1635092)------------------------------
% 24.00/4.08 % (1635092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635092)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635092)Termination reason: Instruction limit
% 24.00/4.08 % (1635092)Termination phase: Saturation
% 24.00/4.08 % (1635092)Time elapsed: 0.120 s
% 24.00/4.08 % (1635092)Peak memory usage: 123 MB
% 24.00/4.08 % (1635092)Instructions burned: 342 (million)
% 24.00/4.08 % (1635098)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1405048484:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 24.00/4.08 % (1635091)Instruction limit reached!
% 24.00/4.08 % (1635091)------------------------------
% 24.00/4.08 % (1635091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635091)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635091)Termination reason: Instruction limit
% 24.00/4.08 % (1635091)Termination phase: Saturation
% 24.00/4.08 % (1635091)Time elapsed: 0.199 s
% 24.00/4.08 % (1635091)Peak memory usage: 93 MB
% 24.00/4.08 % (1635091)Instructions burned: 359 (million)
% 24.00/4.08 % (1635098)Refutation not found, incomplete strategy
% 24.00/4.08 % (1635098)------------------------------
% 24.00/4.08 % (1635098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635098)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635098)Termination reason: Refutation not found, incomplete strategy
% 24.00/4.08 % (1635098)Time elapsed: 0.041 s
% 24.00/4.08 % (1635098)Peak memory usage: 112 MB
% 24.00/4.08 % (1635098)Instructions burned: 34 (million)
% 24.00/4.08 % (1635101)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3626154612:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 24.00/4.08 % (1635090)Instruction limit reached!
% 24.00/4.08 % (1635090)------------------------------
% 24.00/4.08 % (1635090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635090)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635090)Termination reason: Instruction limit
% 24.00/4.08 % (1635090)Termination phase: Saturation
% 24.00/4.08 % (1635090)Time elapsed: 0.253 s
% 24.00/4.08 % (1635090)Peak memory usage: 136 MB
% 24.00/4.08 % (1635090)Instructions burned: 335 (million)
% 24.00/4.08 % (1635088)Instruction limit reached!
% 24.00/4.08 % (1635088)------------------------------
% 24.00/4.08 % (1635088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635088)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635088)Termination reason: Instruction limit
% 24.00/4.08 % (1635088)Termination phase: Saturation
% 24.00/4.08 % (1635088)Time elapsed: 0.312 s
% 24.00/4.08 % (1635088)Peak memory usage: 95 MB
% 24.00/4.08 % (1635088)Instructions burned: 513 (million)
% 24.00/4.08 % (1635100)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=401228393:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 24.00/4.08 % (1635101)Instruction limit reached!
% 24.00/4.08 % (1635101)------------------------------
% 24.00/4.08 % (1635101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635101)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635101)Termination reason: Instruction limit
% 24.00/4.08 % (1635101)Termination phase: Saturation
% 24.00/4.08 % (1635101)Time elapsed: 0.045 s
% 24.00/4.08 % (1635101)Peak memory usage: 92 MB
% 24.00/4.08 % (1635101)Instructions burned: 146 (million)
% 24.00/4.08 % (1635103)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2044945791:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 24.00/4.08 % (1635093)------------------------------
% 24.00/4.08 % (1635093)------------------------------
% 24.00/4.08 % (1635105)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=4096907235:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 24.00/4.08 % (1635106)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2849095445:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 24.00/4.08 % (1635108)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=306142757:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi)
% 24.00/4.08 % (1635100)Instruction limit reached!
% 24.00/4.08 % (1635100)------------------------------
% 24.00/4.08 % (1635100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635100)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635100)Termination reason: Instruction limit
% 24.00/4.08 % (1635100)Termination phase: Saturation
% 24.00/4.08 % (1635100)Time elapsed: 0.174 s
% 24.00/4.08 % (1635100)Peak memory usage: 93 MB
% 24.00/4.08 % (1635100)Instructions burned: 273 (million)
% 24.00/4.08 % (1635098)------------------------------
% 24.00/4.08 % (1635098)------------------------------
% 24.00/4.08 % (1635110)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4268763107:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi)
% 24.00/4.08 % (1635110)Refutation not found, incomplete strategy
% 24.00/4.08 % (1635110)------------------------------
% 24.00/4.08 % (1635110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635110)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635110)Termination reason: Refutation not found, incomplete strategy
% 24.00/4.08 % (1635110)Time elapsed: 0.010 s
% 24.00/4.08 % (1635110)Peak memory usage: 88 MB
% 24.00/4.08 % (1635110)Instructions burned: 18 (million)
% 24.00/4.08 % (1635115)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=638515400:s2a=on:i=450:doe=on:nm=32:rtra=on_2970 on theBenchmark for (2970ds/450Mi)
% 24.00/4.08 % (1635114)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3545559052:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 24.00/4.08 % (1635105)Instruction limit reached!
% 24.00/4.08 % (1635105)------------------------------
% 24.00/4.08 % (1635105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635105)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635105)Termination reason: Instruction limit
% 24.00/4.08 % (1635105)Termination phase: Saturation
% 24.00/4.08 % (1635105)Time elapsed: 0.211 s
% 24.00/4.08 % (1635105)Peak memory usage: 136 MB
% 24.00/4.08 % (1635105)Instructions burned: 277 (million)
% 24.00/4.08 % (1635108)Instruction limit reached!
% 24.00/4.08 % (1635108)------------------------------
% 24.00/4.08 % (1635108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635108)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635108)Termination reason: Instruction limit
% 24.00/4.08 % (1635108)Termination phase: Saturation
% 24.00/4.08 % (1635108)Time elapsed: 0.219 s
% 24.00/4.08 % (1635108)Peak memory usage: 99 MB
% 24.00/4.08 % (1635108)Instructions burned: 657 (million)
% 24.00/4.08 % (1635114)Instruction limit reached!
% 24.00/4.08 % (1635114)------------------------------
% 24.00/4.08 % (1635114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635114)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635114)Termination reason: Instruction limit
% 24.00/4.08 % (1635114)Termination phase: Saturation
% 24.00/4.08 % (1635114)Time elapsed: 0.056 s
% 24.00/4.08 % (1635114)Peak memory usage: 90 MB
% 24.00/4.08 % (1635114)Instructions burned: 108 (million)
% 24.00/4.08 % (1635103)First to succeed.
% 24.00/4.08 % (1635103)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1634936"
% 24.00/4.08 % (1635110)------------------------------
% 24.00/4.08 % (1635110)------------------------------
% 24.00/4.08 % (1635119)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 24.00/4.08 % (1635119)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4137053032:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi)
% 24.00/4.08 % (1635120)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3129069038:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi)
% 24.00/4.08 % (1635121)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2347041699:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi)
% 24.00/4.08 % (1635120)Instruction limit reached!
% 24.00/4.08 % (1635120)------------------------------
% 24.00/4.08 % (1635120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635120)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635120)Termination reason: Instruction limit
% 24.00/4.08 % (1635120)Termination phase: Saturation
% 24.00/4.08 % (1635120)Time elapsed: 0.051 s
% 24.00/4.08 % (1635120)Peak memory usage: 115 MB
% 24.00/4.08 % (1635120)Instructions burned: 131 (million)
% 24.00/4.08 % (1635122)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=913860481:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi)
% 24.00/4.08 % (1635115)Instruction limit reached!
% 24.00/4.08 % (1635115)------------------------------
% 24.00/4.08 % (1635115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.00/4.08 % (1635115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.00/4.08 % (1635115)CaDiCaL version: 2.1.3
% 24.00/4.08 % (1635115)Termination reason: Instruction limit
% 24.00/4.08 % (1635115)Termination phase: Saturation
% 24.00/4.08 % (1635115)Time elapsed: 0.323 s
% 24.00/4.08 % (1635115)Peak memory usage: 136 MB
% 24.00/4.08 % (1635115)Instructions burned: 451 (million)
% 24.00/4.08 % (1635103)Refutation found. Thanks to Tanya!
% 24.00/4.08 % SZS status Unsatisfiable for theBenchmark
% 24.00/4.08 % SZS output start Proof for theBenchmark
% See solution above
% 24.53/4.28 % (1635103)------------------------------
% 24.53/4.28 % (1635103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.28 % (1635103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.28 % (1635103)CaDiCaL version: 2.1.3
% 24.53/4.28 % (1635103)Termination reason: Refutation
% 24.53/4.28 % (1635103)Time elapsed: 0.372 s
% 24.53/4.28 % (1635103)Peak memory usage: 95 MB
% 24.53/4.28 % (1635103)Instructions burned: 622 (million)
% 24.53/4.28 % (1635103)------------------------------
% 24.53/4.28 % (1635103)------------------------------
% 24.53/4.28 % (1634936)Success in time 3.416 s
% 24.53/4.28 % Vampire exiting
%------------------------------------------------------------------------------