%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TIM001_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 02:33:29 PM UTC 2026
% Result : Theorem 274.29s 39.37s
% Output : Refutation 274.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 13
% Syntax : Number of formulae : 77 ( 15 unt; 0 typ; 7 def)
% Number of atoms : 302 ( 93 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 364 ( 139 ~; 172 |; 41 &)
% ( 4 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 9 avg)
% Maximal term depth : 7 ( 1 avg)
% Number arithmetic : 820 ( 41 atm; 161 fun; 294 num; 324 var)
% Number of types : 5 ( 3 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 53 ( 48 usr; 3 prp; 0-9 aty)
% Number of functors : 232 ( 9 usr; 16 con; 0-5 aty)
% Number of variables : 324 ( 0 sgn 309 !; 15 ?; 324 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
date: $tType ).
tff(type_def_6,type,
time: $tType ).
tff(type_def_7,type,
day_name: $tType ).
tff(func_def_0,type,
ymd: ( $int * $int * $int ) > date ).
tff(func_def_1,type,
dt: ( $int * $int * $int * $int * $int ) > time ).
tff(func_def_2,type,
sunday: day_name ).
tff(func_def_3,type,
monday: day_name ).
tff(func_def_4,type,
tuesday: day_name ).
tff(func_def_5,type,
wednesday: day_name ).
tff(func_def_6,type,
thursday: day_name ).
tff(func_def_7,type,
friday: day_name ).
tff(func_def_8,type,
saturday: day_name ).
tff(func_def_67,type,
-1: $int > $int ).
tff(func_def_85,type,
7: $int > $int ).
tff(func_def_92,type,
13: $int > $int ).
tff(func_def_93,type,
5: $int > $int ).
tff(func_def_97,type,
1625: $int > $int ).
tff(func_def_98,type,
1624: $int > $int ).
tff(func_def_103,type,
2026: $int > $int ).
tff(func_def_104,type,
2025: $int > $int ).
tff(func_def_105,type,
32: $int > $int ).
tff(func_def_106,type,
1461: $int > $int ).
tff(func_def_113,type,
-3652: $int > $int ).
tff(func_def_114,type,
2035: $int > $int ).
tff(func_def_115,type,
2034: $int > $int ).
tff(func_def_116,type,
-3620: $int > $int ).
tff(func_def_117,type,
-2191: $int > $int ).
tff(func_def_135,type,
2024: $int > $int ).
tff(func_def_136,type,
2023: $int > $int ).
tff(func_def_137,type,
2033: $int > $int ).
tff(func_def_145,type,
-1461: $int > $int ).
tff(func_def_146,type,
-1429: $int > $int ).
tff(func_def_147,type,
-5113: $int > $int ).
tff(func_def_148,type,
3652: $int > $int ).
tff(func_def_149,type,
3684: $int > $int ).
tff(func_def_150,type,
5113: $int > $int ).
tff(func_def_152,type,
-146097: $int > $int ).
tff(func_def_153,type,
2425: $int > $int ).
tff(func_def_154,type,
2424: $int > $int ).
tff(func_def_155,type,
-146065: $int > $int ).
tff(func_def_156,type,
-144636: $int > $int ).
tff(func_def_157,type,
144636: $int > $int ).
tff(func_def_158,type,
-149749: $int > $int ).
tff(func_def_159,type,
2435: $int > $int ).
tff(func_def_160,type,
2434: $int > $int ).
tff(func_def_179,type,
2: $int > $int ).
tff(func_def_180,type,
4: $int > $int ).
tff(func_def_281,type,
2021: $int > $int ).
tff(func_def_282,type,
2020: $int > $int ).
tff(func_def_283,type,
1493: $int > $int ).
tff(func_def_284,type,
2922: $int > $int ).
tff(func_def_285,type,
-2922: $int > $int ).
tff(func_def_286,type,
2031: $int > $int ).
tff(func_def_287,type,
2030: $int > $int ).
tff(func_def_288,type,
2421: $int > $int ).
tff(func_def_289,type,
2420: $int > $int ).
tff(func_def_290,type,
-148288: $int > $int ).
tff(func_def_291,type,
2431: $int > $int ).
tff(func_def_292,type,
2430: $int > $int ).
tff(func_def_450,type,
3: $int > $int ).
tff(func_def_451,type,
11: $int > $int ).
tff(func_def_452,type,
-147558: $int > $int ).
tff(func_def_453,type,
-143906: $int > $int ).
tff(func_def_454,type,
-140254: $int > $int ).
tff(func_def_455,type,
-136602: $int > $int ).
tff(func_def_456,type,
-132950: $int > $int ).
tff(func_def_457,type,
-129298: $int > $int ).
tff(func_def_458,type,
-125646: $int > $int ).
tff(func_def_459,type,
-121994: $int > $int ).
tff(func_def_460,type,
-118342: $int > $int ).
tff(func_def_461,type,
-114690: $int > $int ).
tff(func_def_462,type,
-111038: $int > $int ).
tff(func_def_463,type,
-107386: $int > $int ).
tff(func_def_464,type,
-103734: $int > $int ).
tff(func_def_465,type,
-100082: $int > $int ).
tff(func_def_466,type,
-96430: $int > $int ).
tff(func_def_467,type,
-92778: $int > $int ).
tff(func_def_468,type,
-89126: $int > $int ).
tff(func_def_469,type,
-85474: $int > $int ).
tff(func_def_470,type,
-81822: $int > $int ).
tff(func_def_471,type,
-78170: $int > $int ).
tff(func_def_472,type,
-74518: $int > $int ).
tff(func_def_473,type,
-70866: $int > $int ).
tff(func_def_474,type,
-67214: $int > $int ).
tff(func_def_475,type,
-63562: $int > $int ).
tff(func_def_476,type,
-59910: $int > $int ).
tff(func_def_477,type,
-56258: $int > $int ).
tff(func_def_478,type,
-52606: $int > $int ).
tff(func_def_479,type,
-48954: $int > $int ).
tff(func_def_480,type,
-45302: $int > $int ).
tff(func_def_481,type,
-41650: $int > $int ).
tff(func_def_482,type,
-37998: $int > $int ).
tff(func_def_483,type,
-34346: $int > $int ).
tff(func_def_484,type,
-30694: $int > $int ).
tff(func_def_485,type,
-27042: $int > $int ).
tff(func_def_486,type,
-23390: $int > $int ).
tff(func_def_518,type,
-32: $int > $int ).
tff(func_def_519,type,
1429: $int > $int ).
tff(func_def_520,type,
-3684: $int > $int ).
tff(func_def_521,type,
-146129: $int > $int ).
tff(func_def_522,type,
-142477: $int > $int ).
tff(func_def_523,type,
-138825: $int > $int ).
tff(func_def_524,type,
-135173: $int > $int ).
tff(func_def_525,type,
-131521: $int > $int ).
tff(func_def_526,type,
-127869: $int > $int ).
tff(func_def_527,type,
-124217: $int > $int ).
tff(func_def_528,type,
-120565: $int > $int ).
tff(func_def_529,type,
-116913: $int > $int ).
tff(func_def_530,type,
-113261: $int > $int ).
tff(func_def_531,type,
-109609: $int > $int ).
tff(func_def_532,type,
-105957: $int > $int ).
tff(func_def_533,type,
-102305: $int > $int ).
tff(func_def_534,type,
-98653: $int > $int ).
tff(func_def_535,type,
-95001: $int > $int ).
tff(func_def_536,type,
-91349: $int > $int ).
tff(func_def_537,type,
-87697: $int > $int ).
tff(func_def_538,type,
-84045: $int > $int ).
tff(func_def_539,type,
-80393: $int > $int ).
tff(func_def_540,type,
-76741: $int > $int ).
tff(func_def_541,type,
-73089: $int > $int ).
tff(func_def_542,type,
-69437: $int > $int ).
tff(func_def_543,type,
-65785: $int > $int ).
tff(func_def_544,type,
-62133: $int > $int ).
tff(func_def_545,type,
-58481: $int > $int ).
tff(func_def_546,type,
-54829: $int > $int ).
tff(func_def_547,type,
-51177: $int > $int ).
tff(func_def_548,type,
-47525: $int > $int ).
tff(func_def_549,type,
-43873: $int > $int ).
tff(func_def_550,type,
-40221: $int > $int ).
tff(func_def_551,type,
-36569: $int > $int ).
tff(func_def_552,type,
-32917: $int > $int ).
tff(func_def_553,type,
-29265: $int > $int ).
tff(func_def_554,type,
-25613: $int > $int ).
tff(func_def_555,type,
-21961: $int > $int ).
tff(func_def_556,type,
-18309: $int > $int ).
tff(func_def_557,type,
-14657: $int > $int ).
tff(func_def_558,type,
-11005: $int > $int ).
tff(func_def_559,type,
-7353: $int > $int ).
tff(func_def_560,type,
-3701: $int > $int ).
tff(func_def_561,type,
-49: $int > $int ).
tff(func_def_622,type,
-365: $int > $int ).
tff(func_def_623,type,
-333: $int > $int ).
tff(func_def_624,type,
365: $int > $int ).
tff(func_def_625,type,
1096: $int > $int ).
tff(func_def_626,type,
-4017: $int > $int ).
tff(func_def_627,type,
2036: $int > $int ).
tff(func_def_628,type,
-146462: $int > $int ).
tff(func_def_629,type,
2426: $int > $int ).
tff(func_def_630,type,
-150114: $int > $int ).
tff(func_def_631,type,
2436: $int > $int ).
tff(func_def_698,type,
-7304: $int > $int ).
tff(func_def_699,type,
2045: $int > $int ).
tff(func_def_700,type,
2044: $int > $int ).
tff(func_def_701,type,
-153401: $int > $int ).
tff(func_def_702,type,
2445: $int > $int ).
tff(func_def_703,type,
2444: $int > $int ).
tff(func_def_704,type,
-7669: $int > $int ).
tff(func_def_705,type,
2046: $int > $int ).
tff(func_def_706,type,
-153766: $int > $int ).
tff(func_def_707,type,
2446: $int > $int ).
tff(func_def_718,type,
-11: $int > $int ).
tff(func_def_722,type,
-10956: $int > $int ).
tff(func_def_723,type,
2054: $int > $int ).
tff(func_def_724,type,
2055: $int > $int ).
tff(func_def_725,type,
-157053: $int > $int ).
tff(func_def_726,type,
2454: $int > $int ).
tff(func_def_756,type,
146097: $int > $int ).
tff(func_def_757,type,
146129: $int > $int ).
tff(func_def_758,type,
147558: $int > $int ).
tff(func_def_759,type,
142445: $int > $int ).
tff(func_def_760,type,
1635: $int > $int ).
tff(func_def_761,type,
1634: $int > $int ).
tff(func_def_762,type,
142080: $int > $int ).
tff(func_def_763,type,
145732: $int > $int ).
tff(func_def_764,type,
138793: $int > $int ).
tff(func_def_765,type,
1644: $int > $int ).
tff(func_def_766,type,
1645: $int > $int ).
tff(func_def_767,type,
135141: $int > $int ).
tff(func_def_768,type,
1655: $int > $int ).
tff(func_def_988,type,
36524: $int > $int ).
tff(func_def_989,type,
1925: $int > $int ).
tff(func_def_990,type,
1924: $int > $int ).
tff(func_def_991,type,
36556: $int > $int ).
tff(func_def_992,type,
-36524: $int > $int ).
tff(func_def_993,type,
37985: $int > $int ).
tff(func_def_994,type,
32872: $int > $int ).
tff(func_def_995,type,
1935: $int > $int ).
tff(func_def_996,type,
1934: $int > $int ).
tff(func_def_997,type,
-109573: $int > $int ).
tff(func_def_998,type,
2325: $int > $int ).
tff(func_def_999,type,
2324: $int > $int ).
tff(func_def_1000,type,
-113225: $int > $int ).
tff(func_def_1001,type,
2335: $int > $int ).
tff(func_def_1002,type,
2334: $int > $int ).
tff(func_def_1003,type,
32507: $int > $int ).
tff(func_def_1004,type,
-113590: $int > $int ).
tff(func_def_1005,type,
36159: $int > $int ).
tff(func_def_1006,type,
29220: $int > $int ).
tff(func_def_1007,type,
1944: $int > $int ).
tff(func_def_1008,type,
1945: $int > $int ).
tff(func_def_1009,type,
-116877: $int > $int ).
tff(func_def_1010,type,
2344: $int > $int ).
tff(func_def_1011,type,
25568: $int > $int ).
tff(func_def_1012,type,
1955: $int > $int ).
tff(func_def_1144,type,
3653: $int > $int ).
tff(func_def_1145,type,
2015: $int > $int ).
tff(func_def_1146,type,
2014: $int > $int ).
tff(func_def_1147,type,
3685: $int > $int ).
tff(func_def_1148,type,
5114: $int > $int ).
tff(func_def_1149,type,
-142444: $int > $int ).
tff(func_def_1150,type,
2415: $int > $int ).
tff(func_def_1151,type,
2414: $int > $int ).
tff(func_def_1152,type,
151211: $int > $int ).
tff(func_def_1153,type,
1615: $int > $int ).
tff(func_def_1154,type,
-146096: $int > $int ).
tff(func_def_1155,type,
-364: $int > $int ).
tff(func_def_1156,type,
-146461: $int > $int ).
tff(func_def_1157,type,
3288: $int > $int ).
tff(func_def_1158,type,
-3651: $int > $int ).
tff(func_def_1159,type,
-149748: $int > $int ).
tff(func_def_1160,type,
-7303: $int > $int ).
tff(func_def_1161,type,
41638: $int > $int ).
tff(func_def_1162,type,
1915: $int > $int ).
tff(pred_def_1,type,
is_leap_year: $int > $o ).
tff(pred_def_2,type,
is_days_in_month: ( $int * $int * $int ) > $o ).
tff(pred_def_3,type,
is_days_in_year: ( $int * $int ) > $o ).
tff(pred_def_4,type,
calc_date: ( $int * $int * $int * date ) > $o ).
tff(pred_def_5,type,
calc_datetime: ( $int * $int * $int * $int * $int * $int * $int * $int * time ) > $o ).
tff(pred_def_6,type,
normalize_time: ( $int * $int * $int * $int * $int * $int * $int ) > $o ).
tff(pred_def_7,type,
weekday: ( date * day_name ) > $o ).
tff(pred_def_8,type,
zeller_prep: ( $int * $int * $int * $int * $int * $int ) > $o ).
tff(pred_def_9,type,
map_iso: ( $int * day_name ) > $o ).
tff(pred_def_10,type,
map_name_to_int: ( day_name * $int ) > $o ).
tff(pred_def_11,type,
nth_weekday_date: ( $int * day_name * $int * $int * date ) > $o ).
tff(pred_def_12,type,
calc_nth_offset: ( $int * $int * $int ) > $o ).
tff(pred_def_13,type,
valid_day: $int > $o ).
tff(pred_def_17,type,
sP0: $int > $o ).
tff(pred_def_18,type,
sP1: $int > $o ).
tff(pred_def_19,type,
sP2: $int > $o ).
tff(pred_def_20,type,
sP3: $int > $o ).
tff(pred_def_21,type,
sP4: $int > $o ).
tff(pred_def_22,type,
sP5: $int > $o ).
tff(pred_def_23,type,
sP6: $int > $o ).
tff(pred_def_24,type,
sP7: $int > $o ).
tff(pred_def_25,type,
sP8: $int > $o ).
tff(pred_def_26,type,
sP9: $int > $o ).
tff(pred_def_27,type,
sP10: $int > $o ).
tff(pred_def_28,type,
sP11: $int > $o ).
tff(pred_def_29,type,
sP12: $int > $o ).
tff(pred_def_30,type,
sP13: $int > $o ).
tff(pred_def_31,type,
sP14: $int > $o ).
tff(pred_def_32,type,
sP15: $int > $o ).
tff(pred_def_33,type,
sP16: $int > $o ).
tff(pred_def_34,type,
sP17: $int > $o ).
tff(pred_def_35,type,
sP18: $int > $o ).
tff(pred_def_36,type,
sP19: $int > $o ).
tff(pred_def_37,type,
sP20: $int > $o ).
tff(pred_def_38,type,
sP21: $int > $o ).
tff(pred_def_39,type,
sP22: $int > $o ).
tff(pred_def_40,type,
sP23: $int > $o ).
tff(pred_def_41,type,
sP24: $int > $o ).
tff(pred_def_42,type,
sP25: $int > $o ).
tff(pred_def_43,type,
sP26: $int > $o ).
tff(pred_def_44,type,
sP27: $int > $o ).
tff(pred_def_45,type,
sP28: $int > $o ).
tff(pred_def_46,type,
sP29: $int > $o ).
tff(pred_def_47,type,
sP30: $int > $o ).
tff(pred_def_48,type,
sP31: $int > $o ).
tff(pred_def_49,type,
sP32: $int > $o ).
tff(f1,axiom,
! [X0: $int] :
( ( $lesseq(X0,31)
& $greater(X0,0) )
<=> valid_day(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',trap_ax) ).
tff(f20,axiom,
! [X5: $int,X1: $int,X7: $int,X9: $int,X4: $int,X10: $int,X3: $int,X2: $int,X0: $int,X8: $int,X6: $int] :
( ( ( X7 = $sum(X1,X3) )
& ( X9 = $quotient_e(X7,60) )
& ( X6 = $quotient_e(X10,24) )
& ( X10 = $sum(X0,$sum(X2,X9)) )
& ( X8 = $remainder_e(X7,60) )
& ( X5 = X8 )
& ( X4 = $remainder_e(X10,24) ) )
=> normalize_time(X0,X1,X2,X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',time_logic) ).
tff(f21,axiom,
! [X11: $int,X3: $int,X5: $int,X8: $int,X9: $int,X0: $int,X12: $int,X13: $int,X4: $int,X1: $int,X7: $int,X2: $int,X6: $int,X10: $int] :
( ( normalize_time(X3,X4,X6,X7,X11,X12,X13)
& calc_date($sum(X2,$sum(X5,X13)),X1,X0,ymd(X8,X9,X10)) )
=> calc_datetime(X0,X1,X2,X3,X4,X5,X6,X7,dt(X8,X9,X10,X11,X12)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_logic) ).
tff(f37,axiom,
! [X0: $int] : is_days_in_month(1,X0,31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m1) ).
tff(f49,axiom,
! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ( $lesseq(X0,X3)
& is_days_in_month(X1,X2,X3)
& $greater(X0,0) )
=> calc_date(X0,X1,X2,ymd(X2,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_base) ).
tff(f88,conjecture,
? [X4: $int,X1: $int,X3: $int,X2: $int,X0: $int] :
( ( X2 = 2 )
& valid_day(X2)
& ( X1 = 1 )
& calc_datetime(2025,1,1,23,0,0,2,0,dt(X0,X1,X2,X3,X4))
& ( X0 = 2025 )
& ( X4 = 0 )
& ( X3 = 1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_time_overflow) ).
tff(f89,negated_conjecture,
~ ? [X4: $int,X1: $int,X3: $int,X2: $int,X0: $int] :
( ( X2 = 2 )
& valid_day(X2)
& ( X1 = 1 )
& calc_datetime(2025,1,1,23,0,0,2,0,dt(X0,X1,X2,X3,X4))
& ( X0 = 2025 )
& ( X4 = 0 )
& ( X3 = 1 ) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
tff(f108,plain,
! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ( ~ $less(X3,X0)
& is_days_in_month(X1,X2,X3)
& $less(0,X0) )
=> calc_date(X0,X1,X2,ymd(X2,X1,X0)) ),
inference(theory_normalization,[],[f49]) ).
tff(f110,plain,
! [X0: $int] :
( valid_day(X0)
<=> ( ~ $less(31,X0)
& $less(0,X0) ) ),
inference(theory_normalization,[],[f1]) ).
tff(f123,plain,
! [X8: $int,X5: $int,X2: $int,X1: $int,X9: $int,X7: $int,X6: $int,X3: $int,X0: $int,X4: $int,X10: $int] :
( ( ( X0 = X9 )
& ( $quotient_e(X5,24) = X10 )
& ( $remainder_e(X2,60) = X9 )
& ( $sum(X8,$sum(X7,X3)) = X5 )
& ( $quotient_e(X2,60) = X3 )
& ( $remainder_e(X5,24) = X4 )
& ( $sum(X1,X6) = X2 ) )
=> normalize_time(X8,X1,X7,X6,X4,X0,X10) ),
inference(rectify,[],[f20]) ).
tff(f135,plain,
! [X3: $int,X1: $int,X0: $int,X2: $int] :
( ( $less(0,X3)
& is_days_in_month(X1,X0,X2)
& ~ $less(X2,X3) )
=> calc_date(X3,X1,X0,ymd(X0,X1,X3)) ),
inference(rectify,[],[f108]) ).
tff(f137,plain,
! [X9: $int,X12: $int,X1: $int,X2: $int,X10: $int,X6: $int,X8: $int,X0: $int,X4: $int,X7: $int,X5: $int,X13: $int,X11: $int,X3: $int] :
( ( calc_date($sum(X11,$sum(X2,X7)),X9,X5,ymd(X3,X4,X13))
& normalize_time(X1,X8,X12,X10,X0,X6,X7) )
=> calc_datetime(X5,X9,X11,X1,X8,X2,X12,X10,dt(X3,X4,X13,X0,X6)) ),
inference(rectify,[],[f21]) ).
tff(f142,plain,
~ ? [X3: $int,X0: $int,X1: $int,X2: $int,X4: $int] :
( ( 2025 = X4 )
& ( 1 = X2 )
& ( 0 = X0 )
& ( 2 = X3 )
& valid_day(X3)
& ( X1 = 1 )
& calc_datetime(2025,1,1,23,0,0,2,0,dt(X4,X1,X3,X2,X0)) ),
inference(rectify,[],[f89]) ).
tff(f143,plain,
! [X0: $int] :
( ( ~ $less(31,X0)
& $less(0,X0) )
=> valid_day(X0) ),
inference(unused_predicate_definition_removal,[],[f110]) ).
tff(f152,plain,
! [X8: $int,X5: $int,X2: $int,X1: $int,X9: $int,X7: $int,X6: $int,X3: $int,X0: $int,X4: $int,X10: $int] :
( normalize_time(X8,X1,X7,X6,X4,X0,X10)
| ( X0 != X9 )
| ( $quotient_e(X5,24) != X10 )
| ( $remainder_e(X2,60) != X9 )
| ( $sum(X8,$sum(X7,X3)) != X5 )
| ( $quotient_e(X2,60) != X3 )
| ( $remainder_e(X5,24) != X4 )
| ( $sum(X1,X6) != X2 ) ),
inference(ennf_transformation,[],[f123]) ).
tff(f153,plain,
! [X5: $int,X6: $int,X10: $int,X7: $int,X8: $int,X3: $int,X9: $int,X1: $int,X0: $int,X4: $int,X2: $int] :
( ( $remainder_e(X5,24) != X4 )
| ( X0 != X9 )
| ( $sum(X1,X6) != X2 )
| normalize_time(X8,X1,X7,X6,X4,X0,X10)
| ( $quotient_e(X2,60) != X3 )
| ( $quotient_e(X5,24) != X10 )
| ( $sum(X8,$sum(X7,X3)) != X5 )
| ( $remainder_e(X2,60) != X9 ) ),
inference(flattening,[],[f152]) ).
tff(f158,plain,
! [X0: $int,X1: $int,X4: $int,X3: $int,X2: $int] :
( ( 1 != X1 )
| ( 2 != X3 )
| ~ calc_datetime(2025,1,1,23,0,0,2,0,dt(X4,X1,X3,X2,X0))
| ( 2025 != X4 )
| ( 0 != X0 )
| ( 1 != X2 )
| ~ valid_day(X3) ),
inference(ennf_transformation,[],[f142]) ).
tff(f178,plain,
! [X9: $int,X12: $int,X1: $int,X2: $int,X10: $int,X6: $int,X8: $int,X0: $int,X4: $int,X7: $int,X5: $int,X13: $int,X11: $int,X3: $int] :
( calc_datetime(X5,X9,X11,X1,X8,X2,X12,X10,dt(X3,X4,X13,X0,X6))
| ~ calc_date($sum(X11,$sum(X2,X7)),X9,X5,ymd(X3,X4,X13))
| ~ normalize_time(X1,X8,X12,X10,X0,X6,X7) ),
inference(ennf_transformation,[],[f137]) ).
tff(f179,plain,
! [X12: $int,X7: $int,X2: $int,X10: $int,X13: $int,X4: $int,X8: $int,X6: $int,X1: $int,X11: $int,X3: $int,X9: $int,X5: $int,X0: $int] :
( calc_datetime(X5,X9,X11,X1,X8,X2,X12,X10,dt(X3,X4,X13,X0,X6))
| ~ calc_date($sum(X11,$sum(X2,X7)),X9,X5,ymd(X3,X4,X13))
| ~ normalize_time(X1,X8,X12,X10,X0,X6,X7) ),
inference(flattening,[],[f178]) ).
tff(f180,plain,
! [X3: $int,X1: $int,X0: $int,X2: $int] :
( calc_date(X3,X1,X0,ymd(X0,X1,X3))
| ~ $less(0,X3)
| ~ is_days_in_month(X1,X0,X2)
| $less(X2,X3) ),
inference(ennf_transformation,[],[f135]) ).
tff(f181,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( $less(X2,X3)
| ~ is_days_in_month(X1,X0,X2)
| calc_date(X3,X1,X0,ymd(X0,X1,X3))
| ~ $less(0,X3) ),
inference(flattening,[],[f180]) ).
tff(f182,plain,
! [X0: $int] :
( valid_day(X0)
| $less(31,X0)
| ~ $less(0,X0) ),
inference(ennf_transformation,[],[f143]) ).
tff(f183,plain,
! [X0: $int] :
( $less(31,X0)
| valid_day(X0)
| ~ $less(0,X0) ),
inference(flattening,[],[f182]) ).
tff(f214,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int,X4: $int,X5: $int,X6: $int,X7: $int,X8: $int,X9: $int,X10: $int] :
( ( $remainder_e(X0,24) != X9 )
| ( X6 != X8 )
| ( $sum(X7,X1) != X10 )
| normalize_time(X4,X7,X3,X1,X9,X8,X2)
| ( $quotient_e(X10,60) != X5 )
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,X5)) != X0 )
| ( $remainder_e(X10,60) != X6 ) ),
inference(rectify,[],[f153]) ).
tff(f234,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int,X4: $int] :
( ( 1 != X1 )
| ( 2 != X3 )
| ~ calc_datetime(2025,1,1,23,0,0,2,0,dt(X2,X1,X3,X4,X0))
| ( 2025 != X2 )
| ( 0 != X0 )
| ( 1 != X4 )
| ~ valid_day(X3) ),
inference(rectify,[],[f158]) ).
tff(f238,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int] :
( $less(X0,X1)
| ~ is_days_in_month(X3,X2,X0)
| calc_date(X1,X3,X2,ymd(X2,X3,X1))
| ~ $less(0,X1) ),
inference(rectify,[],[f181]) ).
tff(f239,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int,X4: $int,X5: $int,X6: $int,X7: $int,X8: $int,X9: $int,X10: $int,X11: $int,X12: $int,X13: $int] :
( calc_datetime(X12,X11,X9,X8,X6,X2,X0,X3,dt(X10,X5,X4,X13,X7))
| ~ calc_date($sum(X9,$sum(X2,X1)),X11,X12,ymd(X10,X5,X4))
| ~ normalize_time(X8,X6,X0,X3,X13,X7,X1) ),
inference(rectify,[],[f179]) ).
tff(f246,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X1: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: $int,X5: $int] :
( ( $remainder_e(X0,24) != X9 )
| ( X6 != X8 )
| ( $sum(X7,X1) != X10 )
| normalize_time(X4,X7,X3,X1,X9,X8,X2)
| ( $quotient_e(X10,60) != X5 )
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,X5)) != X0 )
| ( $remainder_e(X10,60) != X6 ) ),
inference(cnf_transformation,[],[f214]) ).
tff(f284,plain,
! [X0: $int] : is_days_in_month(1,X0,31),
inference(cnf_transformation,[],[f37]) ).
tff(f309,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X4: $int] :
( ( 1 != X1 )
| ( 2 != X3 )
| ~ calc_datetime(2025,1,1,23,0,0,2,0,dt(X2,X1,X3,X4,X0))
| ( 2025 != X2 )
| ( 0 != X0 )
| ( 1 != X4 )
| ~ valid_day(X3) ),
inference(cnf_transformation,[],[f234]) ).
tff(f325,plain,
! [X0: $int] :
( ~ $less(0,X0)
| valid_day(X0)
| $less(31,X0) ),
inference(cnf_transformation,[],[f183]) ).
tff(f332,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ is_days_in_month(X3,X2,X0)
| calc_date(X1,X3,X2,ymd(X2,X3,X1))
| $less(X0,X1)
| ~ $less(0,X1) ),
inference(cnf_transformation,[],[f238]) ).
tff(f334,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X11: $int,X1: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: $int,X5: $int,X12: $int,X13: $int] :
( ~ normalize_time(X8,X6,X0,X3,X13,X7,X1)
| calc_datetime(X12,X11,X9,X8,X6,X2,X0,X3,dt(X10,X5,X4,X13,X7))
| ~ calc_date($sum(X9,$sum(X2,X1)),X11,X12,ymd(X10,X5,X4)) ),
inference(cnf_transformation,[],[f239]) ).
tff(f377,definition,
~ sP24(1),
introduced(definition,[new_symbols(definition,[sP24])],[inequality_splitting_name_introduction]) ).
tff(f378,definition,
~ sP25(2),
introduced(definition,[new_symbols(definition,[sP25])],[inequality_splitting_name_introduction]) ).
tff(f379,definition,
~ sP26(2025),
introduced(definition,[new_symbols(definition,[sP26])],[inequality_splitting_name_introduction]) ).
tff(f380,definition,
~ sP27(0),
introduced(definition,[new_symbols(definition,[sP27])],[inequality_splitting_name_introduction]) ).
tff(f381,definition,
~ sP28(1),
introduced(definition,[new_symbols(definition,[sP28])],[inequality_splitting_name_introduction]) ).
tff(f382,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X4: $int] :
( ~ calc_datetime(2025,1,1,23,0,0,2,0,dt(X2,X1,X3,X4,X0))
| sP27(X0)
| sP25(X3)
| ~ valid_day(X3)
| sP28(X4)
| sP24(X1)
| sP26(X2) ),
inference(inequality_splitting,[],[f309,f381,f380,f379,f378,f377]) ).
tff(f390,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X1: $int,X8: $int,X6: $int,X7: $int,X4: $int,X5: $int] :
( ( X6 != X8 )
| ( $sum(X7,X1) != X10 )
| normalize_time(X4,X7,X3,X1,$remainder_e(X0,24),X8,X2)
| ( $quotient_e(X10,60) != X5 )
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,X5)) != X0 )
| ( $remainder_e(X10,60) != X6 ) ),
inference(equality_resolution,[],[f246]) ).
tff(f391,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X1: $int,X8: $int,X7: $int,X4: $int,X5: $int] :
( ( $sum(X7,X1) != X10 )
| normalize_time(X4,X7,X3,X1,$remainder_e(X0,24),X8,X2)
| ( $quotient_e(X10,60) != X5 )
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,X5)) != X0 )
| ( $remainder_e(X10,60) != X8 ) ),
inference(equality_resolution,[],[f390]) ).
tff(f392,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X8: $int,X7: $int,X4: $int,X5: $int] :
( normalize_time(X4,X7,X3,X1,$remainder_e(X0,24),X8,X2)
| ( $quotient_e($sum(X7,X1),60) != X5 )
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,X5)) != X0 )
| ( $remainder_e($sum(X7,X1),60) != X8 ) ),
inference(equality_resolution,[],[f391]) ).
tff(f393,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X8: $int,X7: $int,X4: $int] :
( normalize_time(X4,X7,X3,X1,$remainder_e(X0,24),X8,X2)
| ( $quotient_e(X0,24) != X2 )
| ( $sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))) != X0 )
| ( $remainder_e($sum(X7,X1),60) != X8 ) ),
inference(equality_resolution,[],[f392]) ).
tff(f394,plain,
! [X3: $int,X0: $int,X1: $int,X8: $int,X7: $int,X4: $int] :
( normalize_time(X4,X7,X3,X1,$remainder_e(X0,24),X8,$quotient_e(X0,24))
| ( $sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))) != X0 )
| ( $remainder_e($sum(X7,X1),60) != X8 ) ),
inference(equality_resolution,[],[f393]) ).
tff(f395,plain,
! [X3: $int,X1: $int,X8: $int,X7: $int,X4: $int] :
( normalize_time(X4,X7,X3,X1,$remainder_e($sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))),24),X8,$quotient_e($sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))),24))
| ( $remainder_e($sum(X7,X1),60) != X8 ) ),
inference(equality_resolution,[],[f394]) ).
tff(f396,plain,
! [X3: $int,X1: $int,X7: $int,X4: $int] : normalize_time(X4,X7,X3,X1,$remainder_e($sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))),24),$remainder_e($sum(X7,X1),60),$quotient_e($sum(X4,$sum(X3,$quotient_e($sum(X7,X1),60))),24)),
inference(equality_resolution,[],[f395]) ).
tff(f408,plain,
! [X3: $int,X1: $int,X7: $int,X4: $int] : normalize_time(X4,X7,X3,X1,$remainder_e($sum(X3,$sum($quotient_e($sum(X1,X7),60),X4)),24),$remainder_e($sum(X1,X7),60),$quotient_e($sum(X3,$sum($quotient_e($sum(X1,X7),60),X4)),24)),
inference(alasca_normalization,[],[f396]) ).
tff(f412,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( calc_date(X1,X3,X2,ymd(X2,X3,X1))
| $greater($sum(1,-1(X1)),0)
| $greater($sum(-1(X0),X1),0)
| ~ is_days_in_month(X3,X2,X0) ),
inference(alasca_normalization,[],[f332]) ).
tff(f422,plain,
! [X0: $int] :
( valid_day(X0)
| $greater($sum(-31,X0),0)
| $greater($sum(1,-1(X0)),0) ),
inference(alasca_normalization,[],[f325]) ).
tff(f439,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X11: $int,X1: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: $int,X5: $int,X12: $int,X13: $int] :
( calc_datetime(X12,X11,X9,X8,X6,X2,X0,X3,dt(X10,X5,X4,X13,X7))
| ~ normalize_time(X8,X6,X0,X3,X13,X7,X1)
| ~ calc_date($sum(X1,$sum(X2,X9)),X11,X12,ymd(X10,X5,X4)) ),
inference(alasca_normalization,[],[f334]) ).
tff(f2145,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X4: $int,X5: $int] :
( sP25(X5)
| ~ calc_date($sum(X2,$sum(0,1)),1,2025,ymd(X3,X4,X5))
| ~ normalize_time(23,0,2,0,X0,X1,X2)
| sP27(X1)
| ~ valid_day(X5)
| sP24(X4)
| sP26(X3)
| sP28(X0) ),
inference(resolution,[],[f439,f382]) ).
tff(f2146,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X4: $int,X5: $int] :
( ~ normalize_time(23,0,2,0,X0,X1,X2)
| sP28(X0)
| sP26(X3)
| ~ valid_day(X5)
| sP27(X1)
| ~ calc_date($sum(1,X2),1,2025,ymd(X3,X4,X5))
| sP24(X4)
| sP25(X5) ),
inference(alasca_normalization,[],[f2145]) ).
tff(f5948,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ valid_day(X1)
| sP26(X0)
| sP24(X2)
| sP25(X1)
| sP28($remainder_e($sum(2,$sum($quotient_e($sum(0,0),60),23)),24))
| ~ calc_date($sum(1,$quotient_e($sum(2,$sum($quotient_e($sum(0,0),60),23)),24)),1,2025,ymd(X0,X2,X1))
| sP27($remainder_e($sum(0,0),60)) ),
inference(resolution,[],[f408,f2146]) ).
tff(f5949,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ valid_day(X1)
| sP24(X2)
| sP28(1)
| sP26(X0)
| ~ calc_date(2,1,2025,ymd(X0,X2,X1))
| sP27(0)
| sP25(X1) ),
inference(alasca_normalization,[],[f5948]) ).
tff(f5950,plain,
! [X2: $int,X0: $int,X1: $int] :
( sP26(X0)
| sP25(X1)
| ~ calc_date(2,1,2025,ymd(X0,X2,X1))
| ~ valid_day(X1)
| sP27(0)
| sP24(X2) ),
inference(forward_subsumption_resolution,[],[f5949,f381]) ).
tff(f5951,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ calc_date(2,1,2025,ymd(X0,X2,X1))
| ~ valid_day(X1)
| sP24(X2)
| sP25(X1)
| sP26(X0) ),
inference(forward_subsumption_resolution,[],[f5950,f380]) ).
tff(f5952,plain,
! [X0: $int] :
( sP26(2025)
| sP25(2)
| $greater($sum(1,-1(2)),0)
| ~ valid_day(2)
| $greater($sum(-1(X0),2),0)
| sP24(1)
| ~ is_days_in_month(1,2025,X0) ),
inference(resolution,[],[f5951,f412]) ).
tff(f5968,plain,
! [X0: $int] :
( $greater($sum(2,-1(X0)),0)
| ~ is_days_in_month(1,2025,X0)
| sP25(2)
| sP26(2025)
| ~ valid_day(2)
| sP24(1) ),
inference(alasca_normalization,[],[f5952]) ).
tff(f5969,plain,
! [X0: $int] :
( sP24(1)
| ~ is_days_in_month(1,2025,X0)
| $greater($sum(2,-1(X0)),0)
| ~ valid_day(2)
| sP26(2025) ),
inference(forward_subsumption_resolution,[],[f5968,f378]) ).
tff(f5970,plain,
! [X0: $int] :
( ~ valid_day(2)
| $greater($sum(2,-1(X0)),0)
| ~ is_days_in_month(1,2025,X0)
| sP26(2025) ),
inference(forward_subsumption_resolution,[],[f5969,f377]) ).
tff(f5971,plain,
! [X0: $int] :
( $greater($sum(2,-1(X0)),0)
| ~ is_days_in_month(1,2025,X0)
| ~ valid_day(2) ),
inference(forward_subsumption_resolution,[],[f5970,f379]) ).
tff(f5973,definition,
( spl33_38
<=> ! [X0: $int] :
( $greater($sum(2,-1(X0)),0)
| ~ is_days_in_month(1,2025,X0) ) ),
introduced(definition,[new_symbols(definition,[spl33_38])],[avatar_definition]) ).
tff(f5974,plain,
( ! [X0: $int] :
( ~ is_days_in_month(1,2025,X0)
| $greater($sum(2,-1(X0)),0) )
| ~ spl33_38 ),
inference(avatar_component_clause,[],[f5973]) ).
tff(f5976,definition,
( spl33_39
<=> valid_day(2) ),
introduced(definition,[new_symbols(definition,[spl33_39])],[avatar_definition]) ).
tff(f5978,plain,
( ~ valid_day(2)
| spl33_39 ),
inference(avatar_component_clause,[],[f5976]) ).
tff(f5979,plain,
( spl33_38
| ~ spl33_39 ),
inference(avatar_split_clause,[],[f5971,f5976,f5973]) ).
tff(f5980,plain,
( $greater($sum(1,-1(2)),0)
| $greater($sum(-31,2),0)
| spl33_39 ),
inference(resolution,[],[f5978,f422]) ).
tff(f5981,plain,
( $false
| spl33_39 ),
inference(alasca_normalization,[],[f5980]) ).
tff(f5982,plain,
spl33_39,
inference(avatar_contradiction_clause,[],[f5981]) ).
tff(f5983,plain,
( $greater($sum(2,-1(31)),0)
| ~ spl33_38 ),
inference(resolution,[],[f5974,f284]) ).
tff(f5984,plain,
( $false
| ~ spl33_38 ),
inference(alasca_normalization,[],[f5983]) ).
tff(f5985,plain,
~ spl33_38,
inference(avatar_contradiction_clause,[],[f5984]) ).
cnf(s27,plain,
( spl33_38
| ~ spl33_39 ),
inference(sat_conversion,[],[f5979]) ).
cnf(s28,plain,
spl33_39,
inference(sat_conversion,[],[f5982]) ).
cnf(s29,plain,
~ spl33_38,
inference(sat_conversion,[],[f5985]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s27,s28,s29]) ).
tff(f5986,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TIM001_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n001.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 18:53:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.81/1.54 % (622702)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.81/1.54 % (622777)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3250078114:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.81/1.54 % (622777)Instruction limit reached!
% 4.81/1.54 % (622777)------------------------------
% 4.81/1.54 % (622777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.81/1.54 % (622777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.81/1.54 % (622777)CaDiCaL version: 2.1.3
% 4.81/1.54 % (622777)Termination reason: Instruction limit
% 4.81/1.54 % (622777)Termination phase: Property scanning
% 4.81/1.54 % (622777)Time elapsed: 0.002 s
% 4.81/1.54 % (622777)Peak memory usage: 86 MB
% 4.81/1.54 % (622777)Instructions burned: 6 (million)
% 4.81/1.54 % (622773)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2978648273:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.81/1.54 % (622775)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2806832330:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.81/1.54 % (622776)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4015031395:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.81/1.54 % (622774)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2734700101:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.81/1.54 % (622776)Instruction limit reached!
% 4.81/1.54 % (622776)------------------------------
% 4.81/1.54 % (622776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.81/1.54 % (622776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.81/1.54 % (622776)CaDiCaL version: 2.1.3
% 4.81/1.54 % (622776)Termination reason: Instruction limit
% 4.81/1.54 % (622776)Termination phase: Saturation
% 4.81/1.54 % (622776)Time elapsed: 0.005 s
% 4.81/1.54 % (622776)Peak memory usage: 87 MB
% 4.81/1.54 % (622776)Instructions burned: 8 (million)
% 4.81/1.54 % (622779)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3369199543:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.81/1.54 % (622773)Instruction limit reached!
% 4.81/1.54 % (622773)------------------------------
% 4.81/1.54 % (622773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.81/1.54 % (622773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.81/1.54 % (622773)CaDiCaL version: 2.1.3
% 4.81/1.54 % (622773)Termination reason: Instruction limit
% 4.81/1.54 % (622773)Termination phase: Saturation
% 4.81/1.54 % (622773)Time elapsed: 0.031 s
% 4.81/1.54 % (622773)Peak memory usage: 112 MB
% 4.81/1.54 % (622773)Instructions burned: 13 (million)
% 4.81/1.54 % (622778)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3821418796:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.81/1.54 % (622779)Instruction limit reached!
% 4.81/1.54 % (622779)------------------------------
% 4.81/1.54 % (622779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.81/1.54 % (622779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.81/1.54 % (622779)CaDiCaL version: 2.1.3
% 4.81/1.54 % (622779)Termination reason: Instruction limit
% 4.81/1.54 % (622779)Termination phase: Saturation
% 4.81/1.54 % (622779)Time elapsed: 0.044 s
% 4.81/1.54 % (622779)Peak memory usage: 116 MB
% 4.81/1.54 % (622779)Instructions burned: 33 (million)
% 4.81/1.54 % (622778)Instruction limit reached!
% 4.81/1.54 % (622778)------------------------------
% 4.81/1.54 % (622778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.81/1.54 % (622778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.81/1.54 % (622778)CaDiCaL version: 2.1.3
% 4.81/1.54 % (622778)Termination reason: Instruction limit
% 4.81/1.54 % (622778)Termination phase: Saturation
% 4.81/1.54 % (622778)Time elapsed: 0.052 s
% 4.81/1.54 % (622778)Peak memory usage: 115 MB
% 4.81/1.54 % (622778)Instructions burned: 46 (million)
% 4.81/1.54 % (622814)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1084059771:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.81/1.54 % (622814)Instruction limit reached!
% 4.81/1.54 % (622814)------------------------------
% 4.81/1.54 % (622814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622814)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622814)Termination reason: Instruction limit
% 6.61/1.76 % (622814)Termination phase: Saturation
% 6.61/1.76 % (622814)Time elapsed: 0.005 s
% 6.61/1.76 % (622814)Peak memory usage: 88 MB
% 6.61/1.76 % (622814)Instructions burned: 15 (million)
% 6.61/1.76 % (622775)Instruction limit reached!
% 6.61/1.76 % (622775)------------------------------
% 6.61/1.76 % (622775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622775)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622775)Termination reason: Instruction limit
% 6.61/1.76 % (622775)Termination phase: Saturation
% 6.61/1.76 % (622775)Time elapsed: 0.193 s
% 6.61/1.76 % (622775)Peak memory usage: 117 MB
% 6.61/1.76 % (622775)Instructions burned: 201 (million)
% 6.61/1.76 % (622823)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=3595852146:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 6.61/1.76 % (622823)Instruction limit reached!
% 6.61/1.76 % (622823)------------------------------
% 6.61/1.76 % (622823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622823)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622823)Termination reason: Instruction limit
% 6.61/1.76 % (622823)Termination phase: Saturation
% 6.61/1.76 % (622823)Time elapsed: 0.035 s
% 6.61/1.76 % (622823)Peak memory usage: 89 MB
% 6.61/1.76 % (622823)Instructions burned: 30 (million)
% 6.61/1.76 % (622774)Instruction limit reached!
% 6.61/1.76 % (622774)------------------------------
% 6.61/1.76 % (622774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622774)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622774)Termination reason: Instruction limit
% 6.61/1.76 % (622774)Termination phase: Saturation
% 6.61/1.76 % (622774)Time elapsed: 0.251 s
% 6.61/1.76 % (622774)Peak memory usage: 117 MB
% 6.61/1.76 % (622774)Instructions burned: 307 (million)
% 6.61/1.76 % (622832)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=288839664:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 6.61/1.76 % (622832)Instruction limit reached!
% 6.61/1.76 % (622832)------------------------------
% 6.61/1.76 % (622832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622832)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622832)Termination reason: Instruction limit
% 6.61/1.76 % (622832)Termination phase: Saturation
% 6.61/1.76 % (622832)Time elapsed: 0.017 s
% 6.61/1.76 % (622832)Peak memory usage: 88 MB
% 6.61/1.76 % (622832)Instructions burned: 17 (million)
% 6.61/1.76 % (622846)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=3070215530:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 6.61/1.76 % (622843)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1139347952:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.61/1.76 % (622846)Refutation not found, incomplete strategy
% 6.61/1.76 % (622846)------------------------------
% 6.61/1.76 % (622846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622846)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622846)Termination reason: Refutation not found, incomplete strategy
% 6.61/1.76 % (622846)Time elapsed: 0.007 s
% 6.61/1.76 % (622846)Peak memory usage: 89 MB
% 6.61/1.76 % (622846)Instructions burned: 12 (million)
% 6.61/1.76 % (622843)Instruction limit reached!
% 6.61/1.76 % (622843)------------------------------
% 6.61/1.76 % (622843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.61/1.76 % (622843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.61/1.76 % (622843)CaDiCaL version: 2.1.3
% 6.61/1.76 % (622843)Termination reason: Instruction limit
% 6.61/1.76 % (622843)Termination phase: Saturation
% 7.66/1.98 % (622843)Time elapsed: 0.026 s
% 7.66/1.98 % (622843)Peak memory usage: 89 MB
% 7.66/1.98 % (622843)Instructions burned: 24 (million)
% 7.66/1.98 % (622851)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2561762203:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 7.66/1.98 % (622877)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1357455461:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.66/1.98 % (622877)Instruction limit reached!
% 7.66/1.98 % (622877)------------------------------
% 7.66/1.98 % (622877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622877)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622877)Termination reason: Instruction limit
% 7.66/1.98 % (622877)Termination phase: Preprocessing 1
% 7.66/1.98 % (622877)Time elapsed: 0.003 s
% 7.66/1.98 % (622877)Peak memory usage: 86 MB
% 7.66/1.98 % (622877)Instructions burned: 3 (million)
% 7.66/1.98 % (622851)Instruction limit reached!
% 7.66/1.98 % (622851)------------------------------
% 7.66/1.98 % (622851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622851)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622851)Termination reason: Instruction limit
% 7.66/1.98 % (622851)Termination phase: Saturation
% 7.66/1.98 % (622851)Time elapsed: 0.094 s
% 7.66/1.98 % (622851)Peak memory usage: 90 MB
% 7.66/1.98 % (622851)Instructions burned: 85 (million)
% 7.66/1.98 % (622879)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=600069280:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 7.66/1.98 % (622883)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2194134608:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.66/1.98 % (622883)Instruction limit reached!
% 7.66/1.98 % (622883)------------------------------
% 7.66/1.98 % (622883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622883)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622883)Termination reason: Instruction limit
% 7.66/1.98 % (622883)Termination phase: Property scanning
% 7.66/1.98 % (622883)Time elapsed: 0.005 s
% 7.66/1.98 % (622883)Peak memory usage: 86 MB
% 7.66/1.98 % (622883)Instructions burned: 5 (million)
% 7.66/1.98 % (622846)------------------------------
% 7.66/1.98 % (622846)------------------------------
% 7.66/1.98 % (622887)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=998173990:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.66/1.98 % (622895)lrs+10_1_thi=all:si=on:fd=off:random_seed=2994903387:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 7.66/1.98 % (622879)Instruction limit reached!
% 7.66/1.98 % (622879)------------------------------
% 7.66/1.98 % (622879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622879)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622879)Termination reason: Instruction limit
% 7.66/1.98 % (622879)Termination phase: Saturation
% 7.66/1.98 % (622879)Time elapsed: 0.176 s
% 7.66/1.98 % (622879)Peak memory usage: 91 MB
% 7.66/1.98 % (622879)Instructions burned: 181 (million)
% 7.66/1.98 % (622887)Instruction limit reached!
% 7.66/1.98 % (622887)------------------------------
% 7.66/1.98 % (622887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622887)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622887)Termination reason: Instruction limit
% 7.66/1.98 % (622887)Termination phase: Saturation
% 7.66/1.98 % (622887)Time elapsed: 0.132 s
% 7.66/1.98 % (622887)Peak memory usage: 134 MB
% 7.66/1.98 % (622887)Instructions burned: 66 (million)
% 7.66/1.98 % (622895)Instruction limit reached!
% 7.66/1.98 % (622895)------------------------------
% 7.66/1.98 % (622895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.66/1.98 % (622895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.66/1.98 % (622895)CaDiCaL version: 2.1.3
% 7.66/1.98 % (622895)Termination reason: Instruction limit
% 11.69/2.43 % (622895)Termination phase: Saturation
% 11.69/2.43 % (622895)Time elapsed: 0.092 s
% 11.69/2.43 % (622895)Peak memory usage: 116 MB
% 11.69/2.43 % (622895)Instructions burned: 53 (million)
% 11.69/2.43 % (622902)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=984908556:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 11.69/2.43 % (622902)Instruction limit reached!
% 11.69/2.43 % (622902)------------------------------
% 11.69/2.43 % (622902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.69/2.43 % (622902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.69/2.43 % (622902)CaDiCaL version: 2.1.3
% 11.69/2.43 % (622902)Termination reason: Instruction limit
% 11.69/2.43 % (622902)Termination phase: Saturation
% 11.69/2.43 % (622902)Time elapsed: 0.009 s
% 11.69/2.43 % (622902)Peak memory usage: 86 MB
% 11.69/2.43 % (622902)Instructions burned: 8 (million)
% 11.69/2.43 % (622906)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1333667623:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.69/2.43 % (622907)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2973421732:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 11.69/2.43 % (622906)Instruction limit reached!
% 11.69/2.43 % (622906)------------------------------
% 11.69/2.43 % (622906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.69/2.43 % (622907)Instruction limit reached!
% 11.69/2.43 % (622907)------------------------------
% 11.69/2.43 % (622907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.69/2.43 % (622906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.69/2.43 % (622907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.69/2.43 % (622906)CaDiCaL version: 2.1.3
% 11.69/2.43 % (622906)Termination reason: Instruction limit
% 11.69/2.43 % (622906)Termination phase: Preprocessing 1
% 11.69/2.43 % (622906)Time elapsed: 0.003 s
% 11.69/2.43 % (622906)Peak memory usage: 85 MB
% 11.69/2.43 % (622907)CaDiCaL version: 2.1.3
% 11.69/2.43 % (622906)Instructions burned: 2 (million)
% 11.69/2.43 % (622907)Termination reason: Instruction limit
% 11.69/2.43 % (622907)Termination phase: Property scanning
% 11.69/2.43 % (622907)Time elapsed: 0.003 s
% 11.69/2.43 % (622907)Peak memory usage: 85 MB
% 11.69/2.43 % (622907)Instructions burned: 2 (million)
% 11.69/2.43 % (622909)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3949161159:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.69/2.43 % (622914)dis+10_1_si=on:random_seed=188329224:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.69/2.43 % (622914)Instruction limit reached!
% 11.69/2.43 % (622914)------------------------------
% 11.69/2.43 % (622914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.69/2.43 % (622914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.69/2.43 % (622914)CaDiCaL version: 2.1.3
% 11.69/2.43 % (622914)Termination reason: Instruction limit
% 11.69/2.43 % (622914)Termination phase: Saturation
% 11.69/2.43 % (622914)Time elapsed: 0.006 s
% 11.69/2.43 % (622914)Peak memory usage: 88 MB
% 11.69/2.43 % (622914)Instructions burned: 11 (million)
% 11.69/2.43 % (622909)Instruction limit reached!
% 11.69/2.43 % (622909)------------------------------
% 11.69/2.43 % (622909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.69/2.43 % (622909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.69/2.43 % (622909)CaDiCaL version: 2.1.3
% 11.69/2.43 % (622909)Termination reason: Instruction limit
% 11.69/2.43 % (622909)Termination phase: Saturation
% 11.69/2.43 % (622909)Time elapsed: 0.143 s
% 11.69/2.43 % (622909)Peak memory usage: 116 MB
% 11.69/2.43 % (622909)Instructions burned: 127 (million)
% 11.69/2.43 % (622918)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3092056823:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.69/2.43 % (622927)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=411033029:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 11.69/2.43 % (622920)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=364173700: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_2991 on theBenchmark for (2991ds/35Mi)
% 12.83/2.87 % (622927)Instruction limit reached!
% 12.83/2.87 % (622927)------------------------------
% 12.83/2.87 % (622927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622927)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622927)Termination reason: Instruction limit
% 12.83/2.87 % (622927)Termination phase: Saturation
% 12.83/2.87 % (622927)Time elapsed: 0.005 s
% 12.83/2.87 % (622927)Peak memory usage: 86 MB
% 12.83/2.87 % (622927)Instructions burned: 8 (million)
% 12.83/2.87 % (622918)Refutation not found, incomplete strategy
% 12.83/2.87 % (622918)------------------------------
% 12.83/2.87 % (622918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622918)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622918)Termination reason: Refutation not found, incomplete strategy
% 12.83/2.87 % (622918)Time elapsed: 0.014 s
% 12.83/2.87 % (622918)Peak memory usage: 88 MB
% 12.83/2.87 % (622918)Instructions burned: 12 (million)
% 12.83/2.87 % (622920)Instruction limit reached!
% 12.83/2.87 % (622920)------------------------------
% 12.83/2.87 % (622920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622920)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622920)Termination reason: Instruction limit
% 12.83/2.87 % (622920)Termination phase: Saturation
% 12.83/2.87 % (622920)Time elapsed: 0.045 s
% 12.83/2.87 % (622920)Peak memory usage: 89 MB
% 12.83/2.87 % (622920)Instructions burned: 36 (million)
% 12.83/2.87 % (622928)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1595870727:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 12.83/2.87 % (622925)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2886824981:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 12.83/2.87 % (622925)Instruction limit reached!
% 12.83/2.87 % (622925)------------------------------
% 12.83/2.87 % (622925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622925)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622925)Termination reason: Instruction limit
% 12.83/2.87 % (622925)Termination phase: Preprocessing 1
% 12.83/2.87 % (622925)Time elapsed: 0.003 s
% 12.83/2.87 % (622925)Peak memory usage: 85 MB
% 12.83/2.87 % (622925)Instructions burned: 3 (million)
% 12.83/2.87 % (622928)Refutation not found, incomplete strategy
% 12.83/2.87 % (622928)------------------------------
% 12.83/2.87 % (622928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622928)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622928)Termination reason: Refutation not found, incomplete strategy
% 12.83/2.87 % (622928)Time elapsed: 0.012 s
% 12.83/2.87 % (622928)Peak memory usage: 88 MB
% 12.83/2.87 % (622928)Instructions burned: 10 (million)
% 12.83/2.87 % (622932)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2358570347:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 12.83/2.87 % (622932)Instruction limit reached!
% 12.83/2.87 % (622932)------------------------------
% 12.83/2.87 % (622932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.87 % (622932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.87 % (622932)CaDiCaL version: 2.1.3
% 12.83/2.87 % (622932)Termination reason: Instruction limit
% 12.83/2.87 % (622932)Termination phase: Saturation
% 12.83/2.87 % (622932)Time elapsed: 0.041 s
% 12.83/2.87 % (622932)Peak memory usage: 110 MB
% 12.83/2.87 % (622932)Instructions burned: 13 (million)
% 12.83/2.87 % (622940)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=587397534:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 12.83/2.87 % (622933)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3631839829:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 12.83/2.87 % (622940)Instruction limit reached!
% 12.83/2.87 % (622940)------------------------------
% 12.83/2.87 % (622940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622940)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622940)Termination reason: Instruction limit
% 18.08/3.39 % (622940)Termination phase: Saturation
% 18.08/3.39 % (622940)Time elapsed: 0.006 s
% 18.08/3.39 % (622940)Peak memory usage: 88 MB
% 18.08/3.39 % (622940)Instructions burned: 10 (million)
% 18.08/3.39 % (622933)Refutation not found, incomplete strategy
% 18.08/3.39 % (622933)------------------------------
% 18.08/3.39 % (622933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622933)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622933)Termination reason: Refutation not found, incomplete strategy
% 18.08/3.39 % (622933)Time elapsed: 0.041 s
% 18.08/3.39 % (622933)Peak memory usage: 112 MB
% 18.08/3.39 % (622933)Instructions burned: 8 (million)
% 18.08/3.39 % (622944)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=648779048:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 18.08/3.39 % (622947)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=1668347569:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 18.08/3.39 % (622918)------------------------------
% 18.08/3.39 % (622918)------------------------------
% 18.08/3.39 % (622947)Instruction limit reached!
% 18.08/3.39 % (622947)------------------------------
% 18.08/3.39 % (622947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622947)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622947)Termination reason: Instruction limit
% 18.08/3.39 % (622947)Termination phase: Saturation
% 18.08/3.39 % (622947)Time elapsed: 0.079 s
% 18.08/3.39 % (622947)Peak memory usage: 90 MB
% 18.08/3.39 % (622947)Instructions burned: 75 (million)
% 18.08/3.39 % (622953)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=1353727911:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 18.08/3.39 % (622928)------------------------------
% 18.08/3.39 % (622928)------------------------------
% 18.08/3.39 % (622944)Instruction limit reached!
% 18.08/3.39 % (622944)------------------------------
% 18.08/3.39 % (622944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622944)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622944)Termination reason: Instruction limit
% 18.08/3.39 % (622944)Termination phase: Saturation
% 18.08/3.39 % (622944)Time elapsed: 0.142 s
% 18.08/3.39 % (622944)Peak memory usage: 133 MB
% 18.08/3.39 % (622944)Instructions burned: 71 (million)
% 18.08/3.39 % (622954)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1938817468:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 18.08/3.39 % (622953)Instruction limit reached!
% 18.08/3.39 % (622953)------------------------------
% 18.08/3.39 % (622953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622953)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622953)Termination reason: Instruction limit
% 18.08/3.39 % (622953)Termination phase: Saturation
% 18.08/3.39 % (622953)Time elapsed: 0.106 s
% 18.08/3.39 % (622953)Peak memory usage: 90 MB
% 18.08/3.39 % (622953)Instructions burned: 295 (million)
% 18.08/3.39 % (622933)------------------------------
% 18.08/3.39 % (622933)------------------------------
% 18.08/3.39 % (622960)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1491068468:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 18.08/3.39 % (622958)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=674712544:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 18.08/3.39 % (622954)Instruction limit reached!
% 18.08/3.39 % (622954)------------------------------
% 18.08/3.39 % (622954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.08/3.39 % (622954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.08/3.39 % (622954)CaDiCaL version: 2.1.3
% 18.08/3.39 % (622954)Termination reason: Instruction limit
% 20.33/3.83 % (622954)Termination phase: Saturation
% 20.33/3.83 % (622954)Time elapsed: 0.160 s
% 20.33/3.83 % (622954)Peak memory usage: 117 MB
% 20.33/3.83 % (622954)Instructions burned: 130 (million)
% 20.33/3.83 % (622969)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3632710879:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 20.33/3.83 % (622965)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=702907303:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 20.33/3.83 % (622964)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=675868317:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 20.33/3.83 % (622964)Refutation not found, incomplete strategy
% 20.33/3.83 % (622964)------------------------------
% 20.33/3.83 % (622964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.83 % (622964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.83 % (622964)CaDiCaL version: 2.1.3
% 20.33/3.83 % (622964)Termination reason: Refutation not found, incomplete strategy
% 20.33/3.83 % (622964)Time elapsed: 0.015 s
% 20.33/3.83 % (622964)Peak memory usage: 89 MB
% 20.33/3.83 % (622964)Instructions burned: 14 (million)
% 20.33/3.83 % (622960)Instruction limit reached!
% 20.33/3.83 % (622960)------------------------------
% 20.33/3.83 % (622960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.83 % (622960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.83 % (622960)CaDiCaL version: 2.1.3
% 20.33/3.83 % (622960)Termination reason: Instruction limit
% 20.33/3.83 % (622960)Termination phase: Saturation
% 20.33/3.83 % (622960)Time elapsed: 0.075 s
% 20.33/3.83 % (622960)Peak memory usage: 134 MB
% 20.33/3.83 % (622960)Instructions burned: 40 (million)
% 20.33/3.83 % (622969)Instruction limit reached!
% 20.33/3.83 % (622969)------------------------------
% 20.33/3.83 % (622969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.83 % (622969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.83 % (622969)CaDiCaL version: 2.1.3
% 20.33/3.83 % (622969)Termination reason: Instruction limit
% 20.33/3.83 % (622969)Termination phase: Saturation
% 20.33/3.83 % (622969)Time elapsed: 0.097 s
% 20.33/3.83 % (622969)Peak memory usage: 118 MB
% 20.33/3.83 % (622969)Instructions burned: 131 (million)
% 20.33/3.83 % (622958)Instruction limit reached!
% 20.33/3.83 % (622958)------------------------------
% 20.33/3.83 % (622958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.83 % (622958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.83 % (622958)CaDiCaL version: 2.1.3
% 20.33/3.83 % (622958)Termination reason: Instruction limit
% 20.33/3.83 % (622958)Termination phase: Saturation
% 20.33/3.83 % (622958)Time elapsed: 0.203 s
% 20.33/3.83 % (622958)Peak memory usage: 134 MB
% 20.33/3.83 % (622958)Instructions burned: 131 (million)
% 20.33/3.83 % (622977)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=117611769:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 20.33/3.83 % (622972)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=3418975301:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 20.33/3.83 % (622974)dis+10_1_si=on:random_seed=1644091925:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 20.33/3.83 % (622972)Refutation not found, incomplete strategy
% 20.33/3.83 % (622972)------------------------------
% 20.33/3.83 % (622972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.83 % (622972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.83 % (622972)CaDiCaL version: 2.1.3
% 20.33/3.83 % (622972)Termination reason: Refutation not found, incomplete strategy
% 20.33/3.83 % (622972)Time elapsed: 0.042 s
% 20.33/3.83 % (622972)Peak memory usage: 112 MB
% 20.33/3.83 % (622972)Instructions burned: 9 (million)
% 20.33/3.83 % (622978)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3903159610:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi)
% 20.33/3.83 % (622964)------------------------------
% 20.33/3.83 % (622964)------------------------------
% 20.33/3.83 % (622979)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2751345409:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 25.11/4.33 % (622979)Refutation not found, incomplete strategy
% 25.11/4.33 % (622979)------------------------------
% 25.11/4.33 % (622979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622979)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622979)Termination reason: Refutation not found, incomplete strategy
% 25.11/4.33 % (622979)Time elapsed: 0.029 s
% 25.11/4.33 % (622979)Peak memory usage: 115 MB
% 25.11/4.33 % (622979)Instructions burned: 16 (million)
% 25.11/4.33 % (622977)Instruction limit reached!
% 25.11/4.33 % (622977)------------------------------
% 25.11/4.33 % (622977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622977)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622977)Termination reason: Instruction limit
% 25.11/4.33 % (622977)Termination phase: Saturation
% 25.11/4.33 % (622977)Time elapsed: 0.292 s
% 25.11/4.33 % (622977)Peak memory usage: 95 MB
% 25.11/4.33 % (622977)Instructions burned: 383 (million)
% 25.11/4.33 % (622978)Instruction limit reached!
% 25.11/4.33 % (622978)------------------------------
% 25.11/4.33 % (622978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622978)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622978)Termination reason: Instruction limit
% 25.11/4.33 % (622978)Termination phase: Saturation
% 25.11/4.33 % (622978)Time elapsed: 0.161 s
% 25.11/4.33 % (622978)Peak memory usage: 90 MB
% 25.11/4.33 % (622978)Instructions burned: 141 (million)
% 25.11/4.33 % (622972)------------------------------
% 25.11/4.33 % (622972)------------------------------
% 25.11/4.33 % (622979)------------------------------
% 25.11/4.33 % (622979)------------------------------
% 25.11/4.33 % (622987)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=557315636:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi)
% 25.11/4.33 % (622965)Instruction limit reached!
% 25.11/4.33 % (622965)------------------------------
% 25.11/4.33 % (622965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622965)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622965)Termination reason: Instruction limit
% 25.11/4.33 % (622965)Termination phase: Saturation
% 25.11/4.33 % (622965)Time elapsed: 0.730 s
% 25.11/4.33 % (622965)Peak memory usage: 139 MB
% 25.11/4.33 % (622965)Instructions burned: 598 (million)
% 25.11/4.33 % (622988)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=4095333589:s2a=on:i=128:s2at=5:ins=3:rtra=on_2976 on theBenchmark for (2976ds/128Mi)
% 25.11/4.33 % (622987)Instruction limit reached!
% 25.11/4.33 % (622987)------------------------------
% 25.11/4.33 % (622987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622987)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622987)Termination reason: Instruction limit
% 25.11/4.33 % (622987)Termination phase: Saturation
% 25.11/4.33 % (622987)Time elapsed: 0.116 s
% 25.11/4.33 % (622987)Peak memory usage: 89 MB
% 25.11/4.33 % (622987)Instructions burned: 122 (million)
% 25.11/4.33 % (622989)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=3415222925:i=39:ins=3:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 25.11/4.33 % (622991)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=596751696:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi)
% 25.11/4.33 % (622989)Refutation not found, incomplete strategy
% 25.11/4.33 % (622989)------------------------------
% 25.11/4.33 % (622989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.11/4.33 % (622989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.11/4.33 % (622989)CaDiCaL version: 2.1.3
% 25.11/4.33 % (622989)Termination reason: Refutation not found, incomplete strategy
% 25.11/4.33 % (622989)Time elapsed: 0.053 s
% 25.11/4.33 % (622989)Peak memory usage: 116 MB
% 25.11/4.33 % (622989)Instructions burned: 17 (million)
% 25.11/4.33 % (622990)dis+1010_1_to=kbo:si=on:random_seed=1151395791:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2975 on theBenchmark for (2975ds/175Mi)
% 26.92/4.84 % (622988)Instruction limit reached!
% 26.92/4.84 % (622988)------------------------------
% 26.92/4.84 % (622988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622988)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622988)Termination reason: Instruction limit
% 26.92/4.84 % (622988)Termination phase: Saturation
% 26.92/4.84 % (622988)Time elapsed: 0.159 s
% 26.92/4.84 % (622988)Peak memory usage: 116 MB
% 26.92/4.84 % (622988)Instructions burned: 128 (million)
% 26.92/4.84 % (622993)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=100696699:s2a=on:i=483:doe=on:nm=32:rtra=on_2974 on theBenchmark for (2974ds/483Mi)
% 26.92/4.84 % (622991)Instruction limit reached!
% 26.92/4.84 % (622991)------------------------------
% 26.92/4.84 % (622991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622991)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622991)Termination reason: Instruction limit
% 26.92/4.84 % (622991)Termination phase: Saturation
% 26.92/4.84 % (622991)Time elapsed: 0.217 s
% 26.92/4.84 % (622991)Peak memory usage: 118 MB
% 26.92/4.84 % (622991)Instructions burned: 330 (million)
% 26.92/4.84 % (622995)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1715026138:thitd=on:i=215:nm=0:rtra=on:ev=force_2974 on theBenchmark for (2974ds/215Mi)
% 26.92/4.84 % (622990)Instruction limit reached!
% 26.92/4.84 % (622990)------------------------------
% 26.92/4.84 % (622990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622990)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622990)Termination reason: Instruction limit
% 26.92/4.84 % (622990)Termination phase: Saturation
% 26.92/4.84 % (622990)Time elapsed: 0.204 s
% 26.92/4.84 % (622990)Peak memory usage: 92 MB
% 26.92/4.84 % (622990)Instructions burned: 175 (million)
% 26.92/4.84 % (622999)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=512546707:i=349:rtra=on_2972 on theBenchmark for (2972ds/349Mi)
% 26.92/4.84 % (622989)------------------------------
% 26.92/4.84 % (622989)------------------------------
% 26.92/4.84 % (622974)Instruction limit reached!
% 26.92/4.84 % (622974)------------------------------
% 26.92/4.84 % (622974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622974)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622974)Termination reason: Instruction limit
% 26.92/4.84 % (622974)Termination phase: Saturation
% 26.92/4.84 % (622974)Time elapsed: 1.017 s
% 26.92/4.84 % (622974)Peak memory usage: 96 MB
% 26.92/4.84 % (622974)Instructions burned: 1001 (million)
% 26.92/4.84 % (623002)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=249562878:st=2:i=295:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/295Mi)
% 26.92/4.84 % (622999)Refutation not found, incomplete strategy
% 26.92/4.84 % (622999)------------------------------
% 26.92/4.84 % (622999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622999)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622999)Termination reason: Refutation not found, incomplete strategy
% 26.92/4.84 % (622999)Time elapsed: 0.063 s
% 26.92/4.84 % (622999)Peak memory usage: 116 MB
% 26.92/4.84 % (622999)Instructions burned: 28 (million)
% 26.92/4.84 % (623003)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1773654332:i=328:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/328Mi)
% 26.92/4.84 % (622995)Instruction limit reached!
% 26.92/4.84 % (622995)------------------------------
% 26.92/4.84 % (622995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.92/4.84 % (622995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.92/4.84 % (622995)CaDiCaL version: 2.1.3
% 26.92/4.84 % (622995)Termination reason: Instruction limit
% 26.92/4.84 % (622995)Termination phase: Saturation
% 26.92/4.84 % (622995)Time elapsed: 0.274 s
% 26.92/4.84 % (622995)Peak memory usage: 136 MB
% 31.60/5.28 % (622995)Instructions burned: 216 (million)
% 31.60/5.28 % (623003)Instruction limit reached!
% 31.60/5.28 % (623003)------------------------------
% 31.60/5.28 % (623003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (623003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (623003)CaDiCaL version: 2.1.3
% 31.60/5.28 % (623003)Termination reason: Instruction limit
% 31.60/5.28 % (623003)Termination phase: Saturation
% 31.60/5.28 % (623003)Time elapsed: 0.145 s
% 31.60/5.28 % (623003)Peak memory usage: 119 MB
% 31.60/5.28 % (623003)Instructions burned: 335 (million)
% 31.60/5.28 % (622993)Instruction limit reached!
% 31.60/5.28 % (622993)------------------------------
% 31.60/5.28 % (622993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (622993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (622993)CaDiCaL version: 2.1.3
% 31.60/5.28 % (622993)Termination reason: Instruction limit
% 31.60/5.28 % (622993)Termination phase: Saturation
% 31.60/5.28 % (622993)Time elapsed: 0.512 s
% 31.60/5.28 % (622993)Peak memory usage: 136 MB
% 31.60/5.28 % (622993)Instructions burned: 483 (million)
% 31.60/5.28 % (623005)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1454955703:i=281:gtgl=2:rtra=on:gtg=all_2969 on theBenchmark for (2969ds/281Mi)
% 31.60/5.28 % (623002)Instruction limit reached!
% 31.60/5.28 % (623002)------------------------------
% 31.60/5.28 % (623002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (623002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (623002)CaDiCaL version: 2.1.3
% 31.60/5.28 % (623002)Termination reason: Instruction limit
% 31.60/5.28 % (623002)Termination phase: Saturation
% 31.60/5.28 % (623002)Time elapsed: 0.263 s
% 31.60/5.28 % (623002)Peak memory usage: 91 MB
% 31.60/5.28 % (623002)Instructions burned: 296 (million)
% 31.60/5.28 % (623006)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=251590995:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2969 on theBenchmark for (2969ds/484Mi)
% 31.60/5.28 % (623006)Refutation not found, incomplete strategy
% 31.60/5.28 % (623006)------------------------------
% 31.60/5.28 % (623006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (623006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (623006)CaDiCaL version: 2.1.3
% 31.60/5.28 % (623006)Termination reason: Refutation not found, incomplete strategy
% 31.60/5.28 % (623006)Time elapsed: 0.006 s
% 31.60/5.28 % (623006)Peak memory usage: 88 MB
% 31.60/5.28 % (623006)Instructions burned: 4 (million)
% 31.60/5.28 % (623009)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1320692942:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2968 on theBenchmark for (2968ds/321Mi)
% 31.60/5.28 % (622999)------------------------------
% 31.60/5.28 % (622999)------------------------------
% 31.60/5.28 % (623014)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3843220599:i=416:rtra=on:gtg=position:ss=axioms_2967 on theBenchmark for (2967ds/416Mi)
% 31.60/5.28 % (623018)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=2553242570:avsq=on:i=276:avsqr=1,2:rtra=on_2966 on theBenchmark for (2966ds/276Mi)
% 31.60/5.28 % (623015)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=33929430:i=471:thf=on:kws=precedence:rtra=on_2966 on theBenchmark for (2966ds/471Mi)
% 31.60/5.28 % (623014)Refutation not found, incomplete strategy
% 31.60/5.28 % (623014)------------------------------
% 31.60/5.28 % (623014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (623014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (623014)CaDiCaL version: 2.1.3
% 31.60/5.28 % (623014)Termination reason: Refutation not found, incomplete strategy
% 31.60/5.28 % (623014)Time elapsed: 0.041 s
% 31.60/5.28 % (623014)Peak memory usage: 112 MB
% 31.60/5.28 % (623014)Instructions burned: 8 (million)
% 31.60/5.28 % (623005)Instruction limit reached!
% 31.60/5.28 % (623005)------------------------------
% 31.60/5.28 % (623005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.60/5.28 % (623005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.60/5.28 % (623005)CaDiCaL version: 2.1.3
% 31.60/5.28 % (623005)Termination reason: Instruction limit
% 33.29/5.70 % (623005)Termination phase: Saturation
% 33.29/5.70 % (623005)Time elapsed: 0.322 s
% 33.29/5.70 % (623005)Peak memory usage: 118 MB
% 33.29/5.70 % (623005)Instructions burned: 281 (million)
% 33.29/5.70 % (623018)Instruction limit reached!
% 33.29/5.70 % (623018)------------------------------
% 33.29/5.70 % (623018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.29/5.70 % (623018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.29/5.70 % (623018)CaDiCaL version: 2.1.3
% 33.29/5.70 % (623018)Termination reason: Instruction limit
% 33.29/5.70 % (623018)Termination phase: Saturation
% 33.29/5.70 % (623018)Time elapsed: 0.207 s
% 33.29/5.70 % (623018)Peak memory usage: 134 MB
% 33.29/5.70 % (623018)Instructions burned: 277 (million)
% 33.29/5.70 % (623006)------------------------------
% 33.29/5.70 % (623006)------------------------------
% 33.29/5.70 % (623009)Instruction limit reached!
% 33.29/5.70 % (623009)------------------------------
% 33.29/5.70 % (623009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.29/5.70 % (623009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.29/5.70 % (623009)CaDiCaL version: 2.1.3
% 33.29/5.70 % (623009)Termination reason: Instruction limit
% 33.29/5.70 % (623009)Termination phase: Saturation
% 33.29/5.70 % (623009)Time elapsed: 0.289 s
% 33.29/5.70 % (623009)Peak memory usage: 113 MB
% 33.29/5.70 % (623009)Instructions burned: 322 (million)
% 33.29/5.70 % (623020)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2657802630:i=375:kws=inv_arity_squared:rtra=on_2965 on theBenchmark for (2965ds/375Mi)
% 33.29/5.70 % (623024)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=248543614:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/387Mi)
% 33.29/5.70 % (623027)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4249601844:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi)
% 33.29/5.70 % (623028)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=4275705184:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi)
% 33.29/5.70 % (623028)Refutation not found, incomplete strategy
% 33.29/5.70 % (623028)------------------------------
% 33.29/5.70 % (623028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.29/5.70 % (623028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.29/5.70 % (623028)CaDiCaL version: 2.1.3
% 33.29/5.70 % (623028)Termination reason: Refutation not found, incomplete strategy
% 33.29/5.70 % (623028)Time elapsed: 0.004 s
% 33.29/5.70 % (623028)Peak memory usage: 89 MB
% 33.29/5.70 % (623028)Instructions burned: 5 (million)
% 33.29/5.70 % (623014)------------------------------
% 33.29/5.70 % (623014)------------------------------
% 33.29/5.70 % (623025)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3422670836:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2962 on theBenchmark for (2962ds/513Mi)
% 33.29/5.70 % (623015)Instruction limit reached!
% 33.29/5.70 % (623015)------------------------------
% 33.29/5.70 % (623015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.29/5.70 % (623015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.29/5.70 % (623015)CaDiCaL version: 2.1.3
% 33.29/5.70 % (623015)Termination reason: Instruction limit
% 33.29/5.70 % (623015)Termination phase: Saturation
% 33.29/5.70 % (623015)Time elapsed: 0.439 s
% 33.29/5.70 % (623015)Peak memory usage: 118 MB
% 33.29/5.70 % (623015)Instructions burned: 471 (million)
% 33.29/5.70 % (623033)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=679407398:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2960 on theBenchmark for (2960ds/341Mi)
% 33.29/5.70 % (623020)Instruction limit reached!
% 33.29/5.70 % (623020)------------------------------
% 33.29/5.70 % (623020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.29/5.70 % (623020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.29/5.70 % (623020)CaDiCaL version: 2.1.3
% 33.29/5.70 % (623020)Termination reason: Instruction limit
% 33.29/5.70 % (623020)Termination phase: Saturation
% 33.29/5.70 % (623020)Time elapsed: 0.399 s
% 33.29/5.70 % (623020)Peak memory usage: 120 MB
% 33.29/5.70 % (623020)Instructions burned: 375 (million)
% 33.29/5.70 % (623027)Instruction limit reached!
% 33.29/5.70 % (623027)------------------------------
% 39.69/6.51 % (623027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623027)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623027)Termination reason: Instruction limit
% 39.69/6.51 % (623027)Termination phase: Saturation
% 39.69/6.51 % (623027)Time elapsed: 0.228 s
% 39.69/6.51 % (623027)Peak memory usage: 135 MB
% 39.69/6.51 % (623027)Instructions burned: 334 (million)
% 39.69/6.51 % (623034)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3936750382:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/261Mi)
% 39.69/6.51 % (623034)Refutation not found, incomplete strategy
% 39.69/6.51 % (623034)------------------------------
% 39.69/6.51 % (623034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623034)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623034)Termination reason: Refutation not found, incomplete strategy
% 39.69/6.51 % (623034)Time elapsed: 0.039 s
% 39.69/6.51 % (623034)Peak memory usage: 111 MB
% 39.69/6.51 % (623034)Instructions burned: 7 (million)
% 39.69/6.51 % (623028)------------------------------
% 39.69/6.51 % (623028)------------------------------
% 39.69/6.51 % (623024)Instruction limit reached!
% 39.69/6.51 % (623024)------------------------------
% 39.69/6.51 % (623024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623024)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623024)Termination reason: Instruction limit
% 39.69/6.51 % (623024)Termination phase: Saturation
% 39.69/6.51 % (623024)Time elapsed: 0.402 s
% 39.69/6.51 % (623024)Peak memory usage: 119 MB
% 39.69/6.51 % (623024)Instructions burned: 388 (million)
% 39.69/6.51 % (623033)Instruction limit reached!
% 39.69/6.51 % (623033)------------------------------
% 39.69/6.51 % (623033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623033)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623033)Termination reason: Instruction limit
% 39.69/6.51 % (623033)Termination phase: Saturation
% 39.69/6.51 % (623033)Time elapsed: 0.222 s
% 39.69/6.51 % (623033)Peak memory usage: 120 MB
% 39.69/6.51 % (623033)Instructions burned: 341 (million)
% 39.69/6.51 % (623036)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=896294525:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2958 on theBenchmark for (2958ds/235Mi)
% 39.69/6.51 % (623037)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2329413134:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi)
% 39.69/6.51 % (623036)Refutation not found, incomplete strategy
% 39.69/6.51 % (623036)------------------------------
% 39.69/6.51 % (623036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623036)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623036)Termination reason: Refutation not found, incomplete strategy
% 39.69/6.51 % (623036)Time elapsed: 0.043 s
% 39.69/6.51 % (623036)Peak memory usage: 112 MB
% 39.69/6.51 % (623036)Instructions burned: 9 (million)
% 39.69/6.51 % (623025)Instruction limit reached!
% 39.69/6.51 % (623025)------------------------------
% 39.69/6.51 % (623025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.69/6.51 % (623025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.69/6.51 % (623025)CaDiCaL version: 2.1.3
% 39.69/6.51 % (623025)Termination reason: Instruction limit
% 39.69/6.51 % (623025)Termination phase: Saturation
% 39.69/6.51 % (623025)Time elapsed: 0.549 s
% 39.69/6.51 % (623025)Peak memory usage: 94 MB
% 39.69/6.51 % (623025)Instructions burned: 513 (million)
% 39.69/6.51 % (623041)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2098868577:i=146:doe=on:rtra=on_2956 on theBenchmark for (2956ds/146Mi)
% 39.69/6.51 % (623042)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3743407598:i=4428:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/4428Mi)
% 39.69/6.51 % (623043)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=544361002:avsq=on:i=276:avsqr=1,2:rtra=on_2956 on theBenchmark for (2956ds/276Mi)
% 46.81/7.37 % (623034)------------------------------
% 46.81/7.37 % (623034)------------------------------
% 46.81/7.37 % (623046)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2862129979:i=1052:rtra=on_2954 on theBenchmark for (2954ds/1052Mi)
% 46.81/7.37 % (623041)Instruction limit reached!
% 46.81/7.37 % (623041)------------------------------
% 46.81/7.37 % (623041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623041)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623041)Termination reason: Instruction limit
% 46.81/7.37 % (623041)Termination phase: Saturation
% 46.81/7.37 % (623041)Time elapsed: 0.157 s
% 46.81/7.37 % (623041)Peak memory usage: 90 MB
% 46.81/7.37 % (623041)Instructions burned: 147 (million)
% 46.81/7.37 % (623037)Instruction limit reached!
% 46.81/7.37 % (623037)------------------------------
% 46.81/7.37 % (623037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623037)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623037)Termination reason: Instruction limit
% 46.81/7.37 % (623037)Termination phase: Saturation
% 46.81/7.37 % (623037)Time elapsed: 0.294 s
% 46.81/7.37 % (623037)Peak memory usage: 92 MB
% 46.81/7.37 % (623037)Instructions burned: 273 (million)
% 46.81/7.37 % (623043)Instruction limit reached!
% 46.81/7.37 % (623043)------------------------------
% 46.81/7.37 % (623043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623043)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623043)Termination reason: Instruction limit
% 46.81/7.37 % (623043)Termination phase: Saturation
% 46.81/7.37 % (623043)Time elapsed: 0.203 s
% 46.81/7.37 % (623043)Peak memory usage: 134 MB
% 46.81/7.37 % (623043)Instructions burned: 277 (million)
% 46.81/7.37 % (623036)------------------------------
% 46.81/7.37 % (623036)------------------------------
% 46.81/7.37 % (623052)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=119354471:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2952 on theBenchmark for (2952ds/1054Mi)
% 46.81/7.37 % (623051)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=404740527:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/655Mi)
% 46.81/7.37 % (623053)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3457983070:i=107:rtra=on_2952 on theBenchmark for (2952ds/107Mi)
% 46.81/7.37 % (623051)Refutation not found, incomplete strategy
% 46.81/7.37 % (623051)------------------------------
% 46.81/7.37 % (623051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623051)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623051)Termination reason: Refutation not found, incomplete strategy
% 46.81/7.37 % (623051)Time elapsed: 0.022 s
% 46.81/7.37 % (623051)Peak memory usage: 89 MB
% 46.81/7.37 % (623051)Instructions burned: 20 (million)
% 46.81/7.37 % (623052)Refutation not found, incomplete strategy
% 46.81/7.37 % (623052)------------------------------
% 46.81/7.37 % (623052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623052)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623052)Termination reason: Refutation not found, incomplete strategy
% 46.81/7.37 % (623052)Time elapsed: 0.031 s
% 46.81/7.37 % (623052)Peak memory usage: 89 MB
% 46.81/7.37 % (623052)Instructions burned: 26 (million)
% 46.81/7.37 % (623053)Refutation not found, incomplete strategy
% 46.81/7.37 % (623053)------------------------------
% 46.81/7.37 % (623053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.81/7.37 % (623053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.81/7.37 % (623053)CaDiCaL version: 2.1.3
% 46.81/7.37 % (623053)Termination reason: Refutation not found, incomplete strategy
% 46.81/7.37 % (623053)Time elapsed: 0.054 s
% 46.81/7.37 % (623053)Peak memory usage: 115 MB
% 46.81/7.37 % (623053)Instructions burned: 18 (million)
% 52.05/8.05 % (623056)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=482197850:s2a=on:i=450:doe=on:nm=32:rtra=on_2951 on theBenchmark for (2951ds/450Mi)
% 52.05/8.05 % (623057)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
% 52.05/8.05 % (623057)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3466075008:i=1090:aac=none:nm=0:rtra=on:rawr=on_2951 on theBenchmark for (2951ds/1090Mi)
% 52.05/8.05 % (623056)Instruction limit reached!
% 52.05/8.05 % (623056)------------------------------
% 52.05/8.05 % (623056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.05 % (623056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.05 % (623056)CaDiCaL version: 2.1.3
% 52.05/8.05 % (623056)Termination reason: Instruction limit
% 52.05/8.05 % (623056)Termination phase: Saturation
% 52.05/8.05 % (623056)Time elapsed: 0.263 s
% 52.05/8.05 % (623056)Peak memory usage: 136 MB
% 52.05/8.05 % (623056)Instructions burned: 453 (million)
% 52.05/8.05 % (623052)------------------------------
% 52.05/8.05 % (623052)------------------------------
% 52.05/8.05 % (623051)------------------------------
% 52.05/8.05 % (623051)------------------------------
% 52.05/8.05 % (623053)------------------------------
% 52.05/8.05 % (623053)------------------------------
% 52.05/8.05 % (623063)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=502903627:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2947 on theBenchmark for (2947ds/130Mi)
% 52.05/8.05 % (623063)Instruction limit reached!
% 52.05/8.05 % (623063)------------------------------
% 52.05/8.05 % (623063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.05 % (623063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.05 % (623063)CaDiCaL version: 2.1.3
% 52.05/8.05 % (623063)Termination reason: Instruction limit
% 52.05/8.05 % (623063)Termination phase: Saturation
% 52.05/8.05 % (623063)Time elapsed: 0.088 s
% 52.05/8.05 % (623063)Peak memory usage: 117 MB
% 52.05/8.05 % (623063)Instructions burned: 130 (million)
% 52.05/8.05 % (623064)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1116567828:i=312:kws=inv_frequency:nm=20:rtra=on_2946 on theBenchmark for (2946ds/312Mi)
% 52.05/8.05 % (623065)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=198009416:i=491:doe=on:rtra=on:gtg=position_2946 on theBenchmark for (2946ds/491Mi)
% 52.05/8.05 % (623066)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3156822998:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi)
% 52.05/8.05 % (623065)Refutation not found, incomplete strategy
% 52.05/8.05 % (623065)------------------------------
% 52.05/8.05 % (623065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.05 % (623065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.05 % (623065)CaDiCaL version: 2.1.3
% 52.05/8.05 % (623065)Termination reason: Refutation not found, incomplete strategy
% 52.05/8.05 % (623065)Time elapsed: 0.014 s
% 52.05/8.05 % (623065)Peak memory usage: 89 MB
% 52.05/8.05 % (623065)Instructions burned: 13 (million)
% 52.05/8.05 % (623046)Instruction limit reached!
% 52.05/8.05 % (623046)------------------------------
% 52.05/8.05 % (623046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.05 % (623046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.05 % (623046)CaDiCaL version: 2.1.3
% 52.05/8.05 % (623046)Termination reason: Instruction limit
% 52.05/8.05 % (623046)Termination phase: Saturation
% 52.05/8.05 % (623046)Time elapsed: 0.985 s
% 52.05/8.05 % (623046)Peak memory usage: 93 MB
% 52.05/8.05 % (623046)Instructions burned: 1052 (million)
% 52.05/8.05 % (623071)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1698004215:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2944 on theBenchmark for (2944ds/307Mi)
% 52.05/8.05 % (623071)Refutation not found, incomplete strategy
% 52.05/8.05 % (623071)------------------------------
% 52.05/8.05 % (623071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/8.05 % (623071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/8.05 % (623071)CaDiCaL version: 2.1.3
% 52.05/8.05 % (623071)Termination reason: Refutation not found, incomplete strategy
% 60.05/9.23 % (623071)Time elapsed: 0.009 s
% 60.05/9.23 % (623071)Peak memory usage: 89 MB
% 60.05/9.23 % (623071)Instructions burned: 14 (million)
% 60.05/9.23 % (623064)Instruction limit reached!
% 60.05/9.23 % (623064)------------------------------
% 60.05/9.23 % (623064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.23 % (623064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.23 % (623064)CaDiCaL version: 2.1.3
% 60.05/9.23 % (623064)Termination reason: Instruction limit
% 60.05/9.23 % (623064)Termination phase: Saturation
% 60.05/9.23 % (623064)Time elapsed: 0.310 s
% 60.05/9.23 % (623064)Peak memory usage: 119 MB
% 60.05/9.23 % (623064)Instructions burned: 312 (million)
% 60.05/9.23 % (623080)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4135058304:i=776:doe=on:rtra=on_2943 on theBenchmark for (2943ds/776Mi)
% 60.05/9.23 % (623065)------------------------------
% 60.05/9.23 % (623065)------------------------------
% 60.05/9.23 % (623071)------------------------------
% 60.05/9.23 % (623071)------------------------------
% 60.05/9.23 % (623084)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4228149720:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2940 on theBenchmark for (2940ds/646Mi)
% 60.05/9.23 % (623057)Instruction limit reached!
% 60.05/9.23 % (623057)------------------------------
% 60.05/9.23 % (623057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.23 % (623057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.23 % (623057)CaDiCaL version: 2.1.3
% 60.05/9.23 % (623057)Termination reason: Instruction limit
% 60.05/9.23 % (623057)Termination phase: Saturation
% 60.05/9.23 % (623057)Time elapsed: 1.080 s
% 60.05/9.23 % (623057)Peak memory usage: 130 MB
% 60.05/9.23 % (623057)Instructions burned: 1091 (million)
% 60.05/9.23 % (623089)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=287188520:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2939 on theBenchmark for (2939ds/1131Mi)
% 60.05/9.23 % (623088)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=315795360:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2939 on theBenchmark for (2939ds/784Mi)
% 60.05/9.23 % (623066)Instruction limit reached!
% 60.05/9.23 % (623066)------------------------------
% 60.05/9.23 % (623066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.23 % (623066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.23 % (623066)CaDiCaL version: 2.1.3
% 60.05/9.23 % (623066)Termination reason: Instruction limit
% 60.05/9.23 % (623066)Termination phase: Saturation
% 60.05/9.23 % (623066)Time elapsed: 0.634 s
% 60.05/9.23 % (623066)Peak memory usage: 92 MB
% 60.05/9.23 % (623066)Instructions burned: 836 (million)
% 60.05/9.23 % (623091)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=522254949:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi)
% 60.05/9.23 % (623094)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3462449900:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2937 on theBenchmark for (2937ds/775Mi)
% 60.05/9.23 % (623091)Refutation not found, incomplete strategy
% 60.05/9.23 % (623091)------------------------------
% 60.05/9.23 % (623091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.23 % (623091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.23 % (623091)CaDiCaL version: 2.1.3
% 60.05/9.23 % (623091)Termination reason: Refutation not found, incomplete strategy
% 60.05/9.23 % (623091)Time elapsed: 0.043 s
% 60.05/9.23 % (623091)Peak memory usage: 112 MB
% 60.05/9.23 % (623091)Instructions burned: 9 (million)
% 60.05/9.23 % (623080)Instruction limit reached!
% 60.05/9.23 % (623080)------------------------------
% 60.05/9.23 % (623080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.05/9.23 % (623080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.05/9.23 % (623080)CaDiCaL version: 2.1.3
% 60.05/9.23 % (623080)Termination reason: Instruction limit
% 60.05/9.23 % (623080)Termination phase: Saturation
% 60.05/9.23 % (623080)Time elapsed: 0.690 s
% 60.05/9.23 % (623080)Peak memory usage: 126 MB
% 60.05/9.23 % (623080)Instructions burned: 776 (million)
% 74.29/11.20 % (623089)Instruction limit reached!
% 74.29/11.20 % (623089)------------------------------
% 74.29/11.20 % (623089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.29/11.20 % (623089)CaDiCaL version: 2.1.3
% 74.29/11.20 % (623089)Termination reason: Instruction limit
% 74.29/11.20 % (623089)Termination phase: Saturation
% 74.29/11.20 % (623089)Time elapsed: 0.611 s
% 74.29/11.20 % (623089)Peak memory usage: 126 MB
% 74.29/11.20 % (623089)Instructions burned: 1131 (million)
% 74.29/11.20 % (623084)Instruction limit reached!
% 74.29/11.20 % (623084)------------------------------
% 74.29/11.20 % (623084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.29/11.20 % (623084)CaDiCaL version: 2.1.3
% 74.29/11.20 % (623084)Termination reason: Instruction limit
% 74.29/11.20 % (623084)Termination phase: Saturation
% 74.29/11.20 % (623084)Time elapsed: 0.751 s
% 74.29/11.20 % (623084)Peak memory usage: 141 MB
% 74.29/11.20 % (623084)Instructions burned: 646 (million)
% 74.29/11.20 % (623091)------------------------------
% 74.29/11.20 % (623091)------------------------------
% 74.29/11.20 % (623097)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1867951295:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2932 on theBenchmark for (2932ds/273Mi)
% 74.29/11.20 % (623098)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=786036207:i=102:nm=16:rtra=on_2931 on theBenchmark for (2931ds/102Mi)
% 74.29/11.20 % (623088)Instruction limit reached!
% 74.29/11.20 % (623088)------------------------------
% 74.29/11.20 % (623088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.29/11.20 % (623088)CaDiCaL version: 2.1.3
% 74.29/11.20 % (623088)Termination reason: Instruction limit
% 74.29/11.20 % (623088)Termination phase: Saturation
% 74.29/11.20 % (623088)Time elapsed: 0.820 s
% 74.29/11.20 % (623088)Peak memory usage: 125 MB
% 74.29/11.20 % (623088)Instructions burned: 784 (million)
% 74.29/11.20 % (623098)Instruction limit reached!
% 74.29/11.20 % (623098)------------------------------
% 74.29/11.20 % (623098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.29/11.20 % (623098)CaDiCaL version: 2.1.3
% 74.29/11.20 % (623098)Termination reason: Instruction limit
% 74.29/11.20 % (623098)Termination phase: Saturation
% 74.29/11.20 % (623098)Time elapsed: 0.051 s
% 74.29/11.20 % (623098)Peak memory usage: 89 MB
% 74.29/11.20 % (623098)Instructions burned: 102 (million)
% 74.29/11.20 % (623100)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4290404461:i=6400:doe=on:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/6400Mi)
% 74.29/11.20 % (623099)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=4278054170:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2930 on theBenchmark for (2930ds/1094Mi)
% 74.29/11.20 % (623097)Instruction limit reached!
% 74.29/11.20 % (623097)------------------------------
% 74.29/11.20 % (623097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.29/11.20 % (623097)CaDiCaL version: 2.1.3
% 74.29/11.20 % (623097)Termination reason: Instruction limit
% 74.29/11.20 % (623097)Termination phase: Saturation
% 74.29/11.20 % (623097)Time elapsed: 0.293 s
% 74.29/11.20 % (623097)Peak memory usage: 92 MB
% 74.29/11.20 % (623097)Instructions burned: 274 (million)
% 74.29/11.20 % (623105)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=1354310573:i=1846:canc=cautious:fsr=off:rtra=on_2928 on theBenchmark for (2928ds/1846Mi)
% 74.29/11.20 % (623103)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2588863365:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2928 on theBenchmark for (2928ds/868Mi)
% 74.29/11.20 % (623105)Refutation not found, incomplete strategy
% 74.29/11.20 % (623105)------------------------------
% 74.29/11.20 % (623105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.29/11.20 % (623105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623105)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623105)Termination reason: Refutation not found, incomplete strategy
% 98.00/14.69 % (623105)Time elapsed: 0.014 s
% 98.00/14.69 % (623105)Peak memory usage: 89 MB
% 98.00/14.69 % (623105)Instructions burned: 12 (million)
% 98.00/14.69 % (623094)Instruction limit reached!
% 98.00/14.69 % (623094)------------------------------
% 98.00/14.69 % (623094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.00/14.69 % (623094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623094)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623094)Termination reason: Instruction limit
% 98.00/14.69 % (623094)Termination phase: Saturation
% 98.00/14.69 % (623094)Time elapsed: 0.798 s
% 98.00/14.69 % (623094)Peak memory usage: 94 MB
% 98.00/14.69 % (623094)Instructions burned: 776 (million)
% 98.00/14.69 % (623107)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=689036817:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2927 on theBenchmark for (2927ds/36816Mi)
% 98.00/14.69 % (623110)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1410747826:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2926 on theBenchmark for (2926ds/273Mi)
% 98.00/14.69 % (623105)------------------------------
% 98.00/14.69 % (623105)------------------------------
% 98.00/14.69 % (623110)Instruction limit reached!
% 98.00/14.69 % (623110)------------------------------
% 98.00/14.69 % (623110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.00/14.69 % (623110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623110)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623110)Termination reason: Instruction limit
% 98.00/14.69 % (623110)Termination phase: Saturation
% 98.00/14.69 % (623110)Time elapsed: 0.296 s
% 98.00/14.69 % (623110)Peak memory usage: 92 MB
% 98.00/14.69 % (623110)Instructions burned: 273 (million)
% 98.00/14.69 % (623113)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1878852947:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2922 on theBenchmark for (2922ds/863Mi)
% 98.00/14.69 % (623114)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3322701285:i=5811:kws=precedence:nm=0:rtra=on_2920 on theBenchmark for (2920ds/5811Mi)
% 98.00/14.69 % (623099)Instruction limit reached!
% 98.00/14.69 % (623099)------------------------------
% 98.00/14.69 % (623099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.00/14.69 % (623099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623099)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623099)Termination reason: Instruction limit
% 98.00/14.69 % (623099)Termination phase: Saturation
% 98.00/14.69 % (623099)Time elapsed: 1.019 s
% 98.00/14.69 % (623099)Peak memory usage: 100 MB
% 98.00/14.69 % (623099)Instructions burned: 1094 (million)
% 98.00/14.69 % (623103)Instruction limit reached!
% 98.00/14.69 % (623103)------------------------------
% 98.00/14.69 % (623103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.00/14.69 % (623103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623103)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623103)Termination reason: Instruction limit
% 98.00/14.69 % (623103)Termination phase: Saturation
% 98.00/14.69 % (623103)Time elapsed: 0.921 s
% 98.00/14.69 % (623103)Peak memory usage: 122 MB
% 98.00/14.69 % (623103)Instructions burned: 868 (million)
% 98.00/14.69 % (623042)Instruction limit reached!
% 98.00/14.69 % (623042)------------------------------
% 98.00/14.69 % (623042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.00/14.69 % (623042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.00/14.69 % (623042)CaDiCaL version: 2.1.3
% 98.00/14.69 % (623042)Termination reason: Instruction limit
% 98.00/14.69 % (623042)Termination phase: Saturation
% 98.00/14.69 % (623042)Time elapsed: 3.728 s
% 98.00/14.69 % (623042)Peak memory usage: 109 MB
% 98.00/14.69 % (623042)Instructions burned: 4429 (million)
% 98.00/14.69 % (623117)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=4212841051:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2918 on theBenchmark for (2918ds/2216Mi)
% 98.00/14.69 % (623118)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2142422651:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2917 on theBenchmark for (2917ds/801Mi)
% 128.94/18.92 % (623118)Refutation not found, incomplete strategy
% 128.94/18.92 % (623118)------------------------------
% 128.94/18.92 % (623118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623118)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623118)Termination reason: Refutation not found, incomplete strategy
% 128.94/18.92 % (623118)Time elapsed: 0.022 s
% 128.94/18.92 % (623118)Peak memory usage: 89 MB
% 128.94/18.92 % (623118)Instructions burned: 20 (million)
% 128.94/18.92 % (623119)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4259339381:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2916 on theBenchmark for (2916ds/1026Mi)
% 128.94/18.92 % (623119)Refutation not found, incomplete strategy
% 128.94/18.92 % (623119)------------------------------
% 128.94/18.92 % (623119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623119)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623119)Termination reason: Refutation not found, incomplete strategy
% 128.94/18.92 % (623119)Time elapsed: 0.031 s
% 128.94/18.92 % (623119)Peak memory usage: 89 MB
% 128.94/18.92 % (623119)Instructions burned: 26 (million)
% 128.94/18.92 % (623118)------------------------------
% 128.94/18.92 % (623118)------------------------------
% 128.94/18.92 % (623113)Instruction limit reached!
% 128.94/18.92 % (623113)------------------------------
% 128.94/18.92 % (623113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623113)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623113)Termination reason: Instruction limit
% 128.94/18.92 % (623113)Termination phase: Saturation
% 128.94/18.92 % (623113)Time elapsed: 0.959 s
% 128.94/18.92 % (623113)Peak memory usage: 121 MB
% 128.94/18.92 % (623113)Instructions burned: 865 (million)
% 128.94/18.92 % (623119)------------------------------
% 128.94/18.92 % (623119)------------------------------
% 128.94/18.92 % (623123)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4050124587:i=3509:rtra=on_2910 on theBenchmark for (2910ds/3509Mi)
% 128.94/18.92 % (623124)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1197701085:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2909 on theBenchmark for (2909ds/2127Mi)
% 128.94/18.92 % (623125)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=4028408881:i=1959:rtra=on:fsd=on:proc=on_2909 on theBenchmark for (2909ds/1959Mi)
% 128.94/18.92 % (623125)Refutation not found, incomplete strategy
% 128.94/18.92 % (623125)------------------------------
% 128.94/18.92 % (623125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623125)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623125)Termination reason: Refutation not found, incomplete strategy
% 128.94/18.92 % (623125)Time elapsed: 0.066 s
% 128.94/18.92 % (623125)Peak memory usage: 116 MB
% 128.94/18.92 % (623125)Instructions burned: 29 (million)
% 128.94/18.92 % (623125)------------------------------
% 128.94/18.92 % (623125)------------------------------
% 128.94/18.92 % (623131)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=559799228:s2a=on:i=3553:nm=0:rtra=on_2901 on theBenchmark for (2901ds/3553Mi)
% 128.94/18.92 % (623100)Instruction limit reached!
% 128.94/18.92 % (623100)------------------------------
% 128.94/18.92 % (623100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623100)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623100)Termination reason: Instruction limit
% 128.94/18.92 % (623100)Termination phase: Saturation
% 128.94/18.92 % (623100)Time elapsed: 3.162 s
% 128.94/18.92 % (623100)Peak memory usage: 126 MB
% 128.94/18.92 % (623100)Instructions burned: 6401 (million)
% 128.94/18.92 % (623117)Instruction limit reached!
% 128.94/18.92 % (623117)------------------------------
% 128.94/18.92 % (623117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.94/18.92 % (623117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.94/18.92 % (623117)CaDiCaL version: 2.1.3
% 128.94/18.92 % (623117)Termination reason: Instruction limit
% 128.94/18.92 % (623117)Termination phase: Saturation
% 128.94/18.92 % (623117)Time elapsed: 2.068 s
% 128.94/18.92 % (623117)Peak memory usage: 133 MB
% 128.94/18.92 % (623117)Instructions burned: 2216 (million)
% 187.09/27.13 % (623133)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1702382348:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2896 on theBenchmark for (2896ds/3201Mi)
% 187.09/27.13 % (623134)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=2149763081:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2894 on theBenchmark for (2894ds/4093Mi)
% 187.09/27.13 % (623124)Instruction limit reached!
% 187.09/27.13 % (623124)------------------------------
% 187.09/27.13 % (623124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.09/27.13 % (623124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.09/27.13 % (623124)CaDiCaL version: 2.1.3
% 187.09/27.13 % (623124)Termination reason: Instruction limit
% 187.09/27.13 % (623124)Termination phase: Saturation
% 187.09/27.13 % (623124)Time elapsed: 1.920 s
% 187.09/27.13 % (623124)Peak memory usage: 105 MB
% 187.09/27.13 % (623124)Instructions burned: 2127 (million)
% 187.09/27.13 % (623137)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=3926707775:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2887 on theBenchmark for (2887ds/21173Mi)
% 187.09/27.13 % (623133)Instruction limit reached!
% 187.09/27.13 % (623133)------------------------------
% 187.09/27.13 % (623133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.09/27.13 % (623133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.09/27.13 % (623133)CaDiCaL version: 2.1.3
% 187.09/27.13 % (623133)Termination reason: Instruction limit
% 187.09/27.13 % (623133)Termination phase: Saturation
% 187.09/27.13 % (623133)Time elapsed: 1.490 s
% 187.09/27.13 % (623133)Peak memory usage: 111 MB
% 187.09/27.13 % (623133)Instructions burned: 3202 (million)
% 187.09/27.13 % (623139)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=399459276:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2879 on theBenchmark for (2879ds/10544Mi)
% 187.09/27.13 % (623123)Instruction limit reached!
% 187.09/27.13 % (623123)------------------------------
% 187.09/27.13 % (623123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.09/27.13 % (623123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.09/27.13 % (623123)CaDiCaL version: 2.1.3
% 187.09/27.13 % (623123)Termination reason: Instruction limit
% 187.09/27.13 % (623123)Termination phase: Saturation
% 187.09/27.13 % (623123)Time elapsed: 3.373 s
% 187.09/27.13 % (623123)Peak memory usage: 110 MB
% 187.09/27.13 % (623123)Instructions burned: 3509 (million)
% 187.09/27.13 % (623141)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3734662459:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2874 on theBenchmark for (2874ds/1262Mi)
% 187.09/27.13 % (623114)Instruction limit reached!
% 187.09/27.13 % (623114)------------------------------
% 187.09/27.13 % (623114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.09/27.13 % (623114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.09/27.13 % (623114)CaDiCaL version: 2.1.3
% 187.09/27.13 % (623114)Termination reason: Instruction limit
% 187.09/27.13 % (623114)Termination phase: Saturation
% 187.09/27.13 % (623114)Time elapsed: 5.263 s
% 187.09/27.13 % (623114)Peak memory usage: 135 MB
% 187.09/27.13 % (623114)Instructions burned: 5811 (million)
% 187.09/27.13 % (623131)Instruction limit reached!
% 187.09/27.13 % (623131)------------------------------
% 187.09/27.13 % (623131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.09/27.13 % (623131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.09/27.13 % (623131)CaDiCaL version: 2.1.3
% 187.09/27.13 % (623131)Termination reason: Instruction limit
% 187.09/27.13 % (623131)Termination phase: Saturation
% 187.09/27.13 % (623131)Time elapsed: 3.637 s
% 187.09/27.13 % (623131)Peak memory usage: 108 MB
% 187.09/27.13 % (623131)Instructions burned: 3554 (million)
% 187.09/27.13 % (623143)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2751852980:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2865 on theBenchmark for (2865ds/775Mi)
% 187.09/27.13 % (623144)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3550863640:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2862 on theBenchmark for (2862ds/270Mi)
% 224.49/32.33 % (623141)Instruction limit reached!
% 224.49/32.33 % (623141)------------------------------
% 224.49/32.33 % (623141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623141)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623141)Termination reason: Instruction limit
% 224.49/32.33 % (623141)Termination phase: Saturation
% 224.49/32.33 % (623141)Time elapsed: 1.163 s
% 224.49/32.33 % (623141)Peak memory usage: 122 MB
% 224.49/32.33 % (623141)Instructions burned: 1262 (million)
% 224.49/32.33 % (623144)Instruction limit reached!
% 224.49/32.33 % (623144)------------------------------
% 224.49/32.33 % (623144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623144)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623144)Termination reason: Instruction limit
% 224.49/32.33 % (623144)Termination phase: Saturation
% 224.49/32.33 % (623144)Time elapsed: 0.290 s
% 224.49/32.33 % (623144)Peak memory usage: 92 MB
% 224.49/32.33 % (623144)Instructions burned: 270 (million)
% 224.49/32.33 % (623150)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=937920473:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2859 on theBenchmark for (2859ds/17165Mi)
% 224.49/32.33 % (623143)Instruction limit reached!
% 224.49/32.33 % (623143)------------------------------
% 224.49/32.33 % (623143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623143)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623143)Termination reason: Instruction limit
% 224.49/32.33 % (623143)Termination phase: Saturation
% 224.49/32.33 % (623143)Time elapsed: 0.800 s
% 224.49/32.33 % (623143)Peak memory usage: 94 MB
% 224.49/32.33 % (623143)Instructions burned: 775 (million)
% 224.49/32.33 % (623154)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2215502194:s2a=on:i=13094:s2at=-1:rtra=on_2856 on theBenchmark for (2856ds/13094Mi)
% 224.49/32.33 % (623156)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=126913659:st=2:i=12633:rtra=on:ss=axioms_2854 on theBenchmark for (2854ds/12633Mi)
% 224.49/32.33 % (623134)Instruction limit reached!
% 224.49/32.33 % (623134)------------------------------
% 224.49/32.33 % (623134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623134)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623134)Termination reason: Instruction limit
% 224.49/32.33 % (623134)Termination phase: Saturation
% 224.49/32.33 % (623134)Time elapsed: 4.313 s
% 224.49/32.33 % (623134)Peak memory usage: 155 MB
% 224.49/32.33 % (623134)Instructions burned: 4094 (million)
% 224.49/32.33 % (623159)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1817217286:i=1783:rtra=on:gtg=position_2849 on theBenchmark for (2849ds/1783Mi)
% 224.49/32.33 % (623159)Instruction limit reached!
% 224.49/32.33 % (623159)------------------------------
% 224.49/32.33 % (623159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623159)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623159)Termination reason: Instruction limit
% 224.49/32.33 % (623159)Termination phase: Saturation
% 224.49/32.33 % (623159)Time elapsed: 1.830 s
% 224.49/32.33 % (623159)Peak memory usage: 130 MB
% 224.49/32.33 % (623159)Instructions burned: 1783 (million)
% 224.49/32.33 % (623161)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=1582782812:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2828 on theBenchmark for (2828ds/5451Mi)
% 224.49/32.33 % (623139)Instruction limit reached!
% 224.49/32.33 % (623139)------------------------------
% 224.49/32.33 % (623139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.49/32.33 % (623139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.49/32.33 % (623139)CaDiCaL version: 2.1.3
% 224.49/32.33 % (623139)Termination reason: Instruction limit
% 224.49/32.33 % (623139)Termination phase: Saturation
% 224.49/32.33 % (623139)Time elapsed: 5.693 s
% 224.49/32.33 % (623139)Peak memory usage: 188 MB
% 224.49/32.33 % (623139)Instructions burned: 10544 (million)
% 224.49/32.33 % (623165)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1581479445:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2820 on theBenchmark for (2820ds/4975Mi)
% 264.13/38.03 % (623165)Instruction limit reached!
% 264.13/38.03 % (623165)------------------------------
% 264.13/38.03 % (623165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623165)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623165)Termination reason: Instruction limit
% 264.13/38.03 % (623165)Termination phase: Saturation
% 264.13/38.03 % (623165)Time elapsed: 2.628 s
% 264.13/38.03 % (623165)Peak memory usage: 142 MB
% 264.13/38.03 % (623165)Instructions burned: 4975 (million)
% 264.13/38.03 % (623167)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3181129280:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2791 on theBenchmark for (2791ds/2076Mi)
% 264.13/38.03 % (623167)Instruction limit reached!
% 264.13/38.03 % (623167)------------------------------
% 264.13/38.03 % (623167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623167)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623167)Termination reason: Instruction limit
% 264.13/38.03 % (623167)Termination phase: Saturation
% 264.13/38.03 % (623167)Time elapsed: 1.052 s
% 264.13/38.03 % (623167)Peak memory usage: 127 MB
% 264.13/38.03 % (623167)Instructions burned: 2076 (million)
% 264.13/38.03 % (623171)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1689338473:i=5145:rtra=on_2778 on theBenchmark for (2778ds/5145Mi)
% 264.13/38.03 % (623161)Instruction limit reached!
% 264.13/38.03 % (623161)------------------------------
% 264.13/38.03 % (623161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623161)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623161)Termination reason: Instruction limit
% 264.13/38.03 % (623161)Termination phase: Saturation
% 264.13/38.03 % (623161)Time elapsed: 5.414 s
% 264.13/38.03 % (623161)Peak memory usage: 150 MB
% 264.13/38.03 % (623161)Instructions burned: 5451 (million)
% 264.13/38.03 % (623173)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1127459798:i=3509:rtra=on_2771 on theBenchmark for (2771ds/3509Mi)
% 264.13/38.03 % (623171)Instruction limit reached!
% 264.13/38.03 % (623171)------------------------------
% 264.13/38.03 % (623171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623171)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623171)Termination reason: Instruction limit
% 264.13/38.03 % (623171)Termination phase: Saturation
% 264.13/38.03 % (623171)Time elapsed: 2.324 s
% 264.13/38.03 % (623171)Peak memory usage: 101 MB
% 264.13/38.03 % (623171)Instructions burned: 5147 (million)
% 264.13/38.03 % (623177)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2460473280:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2752 on theBenchmark for (2752ds/13800Mi)
% 264.13/38.03 % (623154)Instruction limit reached!
% 264.13/38.03 % (623154)------------------------------
% 264.13/38.03 % (623154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623154)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623154)Termination reason: Instruction limit
% 264.13/38.03 % (623154)Termination phase: Saturation
% 264.13/38.03 % (623154)Time elapsed: 11.471 s
% 264.13/38.03 % (623154)Peak memory usage: 174 MB
% 264.13/38.03 % (623154)Instructions burned: 13094 (million)
% 264.13/38.03 % (623179)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3407176410:i=1412:rtra=on:fsd=on:proc=on_2739 on theBenchmark for (2739ds/1412Mi)
% 264.13/38.03 % (623179)Refutation not found, incomplete strategy
% 264.13/38.03 % (623179)------------------------------
% 264.13/38.03 % (623179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.13/38.03 % (623179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.13/38.03 % (623179)CaDiCaL version: 2.1.3
% 264.13/38.03 % (623179)Termination reason: Refutation not found, incomplete strategy
% 264.13/38.03 % (623179)Time elapsed: 0.065 s
% 264.13/38.03 % (623179)Peak memory usage: 116 MB
% 274.29/39.37 % (623179)Instructions burned: 28 (million)
% 274.29/39.37 % (623173)Instruction limit reached!
% 274.29/39.37 % (623173)------------------------------
% 274.29/39.37 % (623173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623173)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623173)Termination reason: Instruction limit
% 274.29/39.37 % (623173)Termination phase: Saturation
% 274.29/39.37 % (623173)Time elapsed: 3.497 s
% 274.29/39.37 % (623173)Peak memory usage: 110 MB
% 274.29/39.37 % (623173)Instructions burned: 3509 (million)
% 274.29/39.37 % (623179)------------------------------
% 274.29/39.37 % (623179)------------------------------
% 274.29/39.37 % (623185)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
% 274.29/39.37 % (623185)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3205828782:i=11747:aac=none:nm=0:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/11747Mi)
% 274.29/39.37 % (623186)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=609969229:s2a=on:i=3553:nm=0:rtra=on_2731 on theBenchmark for (2731ds/3553Mi)
% 274.29/39.37 % (623156)Instruction limit reached!
% 274.29/39.37 % (623156)------------------------------
% 274.29/39.37 % (623156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623156)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623156)Termination reason: Instruction limit
% 274.29/39.37 % (623156)Termination phase: Saturation
% 274.29/39.37 % (623156)Time elapsed: 13.874 s
% 274.29/39.37 % (623156)Peak memory usage: 137 MB
% 274.29/39.37 % (623156)Instructions burned: 12633 (million)
% 274.29/39.37 % (623107)Refutation not found, non-redundant clauses discarded
% 274.29/39.37 % (623107)------------------------------
% 274.29/39.37 % (623107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623107)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623107)Termination reason: Refutation not found, non-redundant clauses discarded
% 274.29/39.37 % (623107)Time elapsed: 21.216 s
% 274.29/39.37 % (623107)Peak memory usage: 274 MB
% 274.29/39.37 % (623107)Instructions burned: 25104 (million)
% 274.29/39.37 % (623189)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=305846007:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2712 on theBenchmark for (2712ds/3201Mi)
% 274.29/39.37 % (623107)------------------------------
% 274.29/39.37 % (623107)------------------------------
% 274.29/39.37 % (623203)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=866943066:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2707 on theBenchmark for (2707ds/4081Mi)
% 274.29/39.37 % (623186)Instruction limit reached!
% 274.29/39.37 % (623186)------------------------------
% 274.29/39.37 % (623186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623186)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623186)Termination reason: Instruction limit
% 274.29/39.37 % (623186)Termination phase: Saturation
% 274.29/39.37 % (623186)Time elapsed: 3.576 s
% 274.29/39.37 % (623186)Peak memory usage: 108 MB
% 274.29/39.37 % (623186)Instructions burned: 3554 (million)
% 274.29/39.37 % (623209)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=1350984023:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2693 on theBenchmark for (2693ds/20260Mi)
% 274.29/39.37 % (623177)Instruction limit reached!
% 274.29/39.37 % (623177)------------------------------
% 274.29/39.37 % (623177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623177)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623177)Termination reason: Instruction limit
% 274.29/39.37 % (623177)Termination phase: Saturation
% 274.29/39.37 % (623177)Time elapsed: 6.703 s
% 274.29/39.37 % (623177)Peak memory usage: 169 MB
% 274.29/39.37 % (623177)Instructions burned: 13801 (million)
% 274.29/39.37 % (623189)Instruction limit reached!
% 274.29/39.37 % (623189)------------------------------
% 274.29/39.37 % (623189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623189)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623189)Termination reason: Instruction limit
% 274.29/39.37 % (623189)Termination phase: Saturation
% 274.29/39.37 % (623189)Time elapsed: 2.742 s
% 274.29/39.37 % (623189)Peak memory usage: 112 MB
% 274.29/39.37 % (623189)Instructions burned: 3201 (million)
% 274.29/39.37 % (623211)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2435823620:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2683 on theBenchmark for (2683ds/58627Mi)
% 274.29/39.37 % (623150)Instruction limit reached!
% 274.29/39.37 % (623150)------------------------------
% 274.29/39.37 % (623150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623150)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623150)Termination reason: Instruction limit
% 274.29/39.37 % (623150)Termination phase: Saturation
% 274.29/39.37 % (623150)Time elapsed: 17.536 s
% 274.29/39.37 % (623150)Peak memory usage: 215 MB
% 274.29/39.37 % (623150)Instructions burned: 17166 (million)
% 274.29/39.37 % (623212)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4045843291:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2682 on theBenchmark for (2682ds/6258Mi)
% 274.29/39.37 % (623137)Instruction limit reached!
% 274.29/39.37 % (623137)------------------------------
% 274.29/39.37 % (623137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623137)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623137)Termination reason: Instruction limit
% 274.29/39.37 % (623137)Termination phase: Saturation
% 274.29/39.37 % (623137)Time elapsed: 20.517 s
% 274.29/39.37 % (623137)Peak memory usage: 189 MB
% 274.29/39.37 % (623137)Instructions burned: 21174 (million)
% 274.29/39.37 % (623214)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2532006612:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2680 on theBenchmark for (2680ds/34001Mi)
% 274.29/39.37 % (623216)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1977038510:s2a=on:i=71622:s2at=-1:rtra=on_2679 on theBenchmark for (2679ds/71622Mi)
% 274.29/39.37 % (623203)Instruction limit reached!
% 274.29/39.37 % (623203)------------------------------
% 274.29/39.37 % (623203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623203)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623203)Termination reason: Instruction limit
% 274.29/39.37 % (623203)Termination phase: Saturation
% 274.29/39.37 % (623203)Time elapsed: 4.167 s
% 274.29/39.37 % (623203)Peak memory usage: 154 MB
% 274.29/39.37 % (623203)Instructions burned: 4081 (million)
% 274.29/39.37 % (623219)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4210201093:i=24001:kws=precedence:nm=0:rtra=on_2662 on theBenchmark for (2662ds/24001Mi)
% 274.29/39.37 % (623212)Instruction limit reached!
% 274.29/39.37 % (623212)------------------------------
% 274.29/39.37 % (623212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623212)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623212)Termination reason: Instruction limit
% 274.29/39.37 % (623212)Termination phase: Saturation
% 274.29/39.37 % (623212)Time elapsed: 5.004 s
% 274.29/39.37 % (623212)Peak memory usage: 138 MB
% 274.29/39.37 % (623212)Instructions burned: 6258 (million)
% 274.29/39.37 % (623221)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=4161652960:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2630 on theBenchmark for (2630ds/2076Mi)
% 274.29/39.37 % (623185)Instruction limit reached!
% 274.29/39.37 % (623185)------------------------------
% 274.29/39.37 % (623185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.29/39.37 % (623185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.29/39.37 % (623185)CaDiCaL version: 2.1.3
% 274.29/39.37 % (623185)Termination reason: Instruction limit
% 274.29/39.37 % (623185)Termination phase: Saturation
% 274.29/39.37 % (623185)Time elapsed: 10.467 s
% 274.29/39.37 % (623185)Peak memory usage: 219 MB
% 274.29/39.37 % (623185)Instructions burned: 11748 (million)
% 274.29/39.37 % (623227)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3897136772:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2626 on theBenchmark for (2626ds/83971Mi)
% 274.29/39.37 % (623227)First to succeed.
% 274.29/39.37 % (623227)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-622702"
% 274.29/39.37 % (623227)Refutation found. Thanks to Tanya!
% 274.29/39.37 % SZS status Theorem for theBenchmark
% 274.29/39.37 % SZS output start Proof for theBenchmark
% See solution above
% 274.99/39.65 % (623227)------------------------------
% 274.99/39.65 % (623227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.99/39.65 % (623227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.99/39.65 % (623227)CaDiCaL version: 2.1.3
% 274.99/39.65 % (623227)Termination reason: Refutation
% 274.99/39.65 % (623227)Time elapsed: 0.566 s
% 274.99/39.65 % (623227)Peak memory usage: 99 MB
% 274.99/39.65 % (623227)Instructions burned: 552 (million)
% 274.99/39.65 % (623227)------------------------------
% 274.99/39.65 % (623227)------------------------------
% 274.99/39.65 % (622702)Success in time 38.688 s
% 274.99/39.65 % Vampire exiting
%------------------------------------------------------------------------------