%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TIM019_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:32 PM UTC 2026
% Result : Theorem 74.35s 11.42s
% Output : Refutation 75.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 47
% Syntax : Number of formulae : 219 ( 40 unt; 0 typ; 22 def)
% Number of atoms : 733 ( 195 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 847 ( 333 ~; 392 |; 78 &)
% ( 22 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 11 ( 1 avg)
% Number arithmetic : 1758 ( 99 atm; 411 fun; 939 num; 309 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 : 38 ( 33 usr; 21 prp; 0-9 aty)
% Number of functors : 58 ( 11 usr; 50 con; 0-5 aty)
% Number of variables : 346 ( 334 !; 12 ?; 346 :)
% 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,
sF0: date ).
tff(func_def_68,type,
sF1: $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(f1,axiom,
! [X0: $int] :
( valid_day(X0)
<=> ( $greater(X0,0)
& $lesseq(X0,31) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trap_ax) ).
tff(f37,axiom,
! [X0: $int] : is_days_in_month(1,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m1) ).
tff(f38,axiom,
! [X0: $int] :
( ( ( ( ( $remainder_e(X0,400) = 0 )
| ( $remainder_e(X0,100) != 0 ) )
& ( $remainder_e(X0,4) = 0 ) )
=> is_days_in_month(2,X0,29) )
& ( ( ( $remainder_e(X0,4) != 0 )
| ( ( $remainder_e(X0,400) != 0 )
& ( $remainder_e(X0,100) = 0 ) ) )
=> is_days_in_month(2,X0,28) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m2) ).
tff(f39,axiom,
! [X0: $int] : is_days_in_month(3,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m3) ).
tff(f40,axiom,
! [X0: $int] : is_days_in_month(4,X0,30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m4) ).
tff(f41,axiom,
! [X0: $int] : is_days_in_month(5,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m5) ).
tff(f42,axiom,
! [X0: $int] : is_days_in_month(6,X0,30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m6) ).
tff(f43,axiom,
! [X0: $int] : is_days_in_month(7,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m7) ).
tff(f44,axiom,
! [X0: $int] : is_days_in_month(8,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m8) ).
tff(f45,axiom,
! [X0: $int] : is_days_in_month(9,X0,30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m9) ).
tff(f46,axiom,
! [X0: $int] : is_days_in_month(10,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m10) ).
tff(f47,axiom,
! [X0: $int] : is_days_in_month(11,X0,30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m11) ).
tff(f48,axiom,
! [X0: $int] : is_days_in_month(12,X0,31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m12) ).
tff(f49,axiom,
! [X0: $int,X1: $int,X2: $int,X3: $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/sandbox2/benchmark/theBenchmark.p',rule_base) ).
tff(f50,axiom,
! [X1: $int,X3: $int,X4: date,X2: $int,X0: $int] :
( ( is_days_in_month(X1,X2,X3)
& $greater(X0,X3)
& ( X1 != 12 ) )
=> ( calc_date($difference(X0,X3),$sum(X1,1),X2,X4)
=> calc_date(X0,X1,X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_fwd_std) ).
tff(f51,axiom,
! [X0: $int,X2: $int,X4: date,X1: $int,X3: $int] :
( ( $greater(X0,X3)
& is_days_in_month(X1,X2,X3)
& ( X1 = 12 ) )
=> ( calc_date($difference(X0,X3),1,$sum(X2,1),X4)
=> calc_date(X0,X1,X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_fwd_dec) ).
tff(f66,axiom,
! [X1: $int,X0: $int] :
( ( ( X0 != 1 )
& ( X0 != 2 ) )
=> zeller_prep(X0,X1,X0,X1,$remainder_e(X1,100),$quotient_e(X1,100)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zeller_adj_norm) ).
tff(f67,axiom,
! [X7: $int,X4: $int,X3: day_name,X6: $int,X8: $int,X10: $int,X9: $int,X1: $int,X0: $int,X2: $int,X5: $int] :
( ( ( X8 = $quotient_e($product(13,$sum(X4,1)),5) )
& ( X0 != 1776 )
& ( X0 != 2024 )
& ( X10 = $remainder_e($sum($remainder_e(X9,7),7),7) )
& $greater(X0,1582)
& ( X9 = $sum(X2,$sum(X8,$sum(X6,$sum($quotient_e(X6,4),$sum($quotient_e(X7,4),$product(5,X7)))))) )
& map_iso(X10,X3)
& ( X0 != 1969 )
& ( X0 != 2025 )
& zeller_prep(X1,X0,X4,X5,X6,X7)
& ( X0 != 1985 ) )
=> weekday(ymd(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',calc_weekday_zeller) ).
tff(f73,axiom,
map_iso(5,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map_5) ).
tff(f88,conjecture,
? [X2: $int,X0: $int,X3: day_name,X1: $int] :
( ( X1 = 11 )
& ( X0 = 2026 )
& ( X3 = thursday )
& calc_date($sum(19,365),11,2025,ymd(X0,X1,X2))
& valid_day(X2)
& ( X2 = 19 )
& weekday(ymd(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_next_year) ).
tff(f89,negated_conjecture,
~ ? [X2: $int,X0: $int,X3: day_name,X1: $int] :
( ( X1 = 11 )
& ( X0 = 2026 )
& ( X3 = thursday )
& calc_date($sum(19,365),11,2025,ymd(X0,X1,X2))
& valid_day(X2)
& ( X2 = 19 )
& weekday(ymd(X0,X1,X2),X3) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
tff(f93,plain,
! [X7: $int,X4: $int,X3: day_name,X6: $int,X8: $int,X10: $int,X9: $int,X1: $int,X0: $int,X2: $int,X5: $int] :
( ( ( X8 = $quotient_e($product(13,$sum(X4,1)),5) )
& ( X0 != 1776 )
& ( X0 != 2024 )
& ( X10 = $remainder_e($sum($remainder_e(X9,7),7),7) )
& $less(1582,X0)
& ( X9 = $sum(X2,$sum(X8,$sum(X6,$sum($quotient_e(X6,4),$sum($quotient_e(X7,4),$product(5,X7)))))) )
& map_iso(X10,X3)
& ( X0 != 1969 )
& ( X0 != 2025 )
& zeller_prep(X1,X0,X4,X5,X6,X7)
& ( X0 != 1985 ) )
=> weekday(ymd(X0,X1,X2),X3) ),
inference(theory_normalization,[],[f67]) ).
tff(f94,plain,
! [X0: $int] :
( valid_day(X0)
<=> ( $less(0,X0)
& ~ $less(31,X0) ) ),
inference(theory_normalization,[],[f1]) ).
tff(f95,plain,
! [X0: $int,X2: $int,X4: date,X1: $int,X3: $int] :
( ( $less(X3,X0)
& is_days_in_month(X1,X2,X3)
& ( X1 = 12 ) )
=> ( calc_date($sum(X0,$uminus(X3)),1,$sum(X2,1),X4)
=> calc_date(X0,X1,X2,X4) ) ),
inference(theory_normalization,[],[f51]) ).
tff(f99,plain,
! [X0: $int,X2: $int,X1: $int,X3: $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(f102,plain,
! [X1: $int,X3: $int,X4: date,X2: $int,X0: $int] :
( ( is_days_in_month(X1,X2,X3)
& $less(X3,X0)
& ( X1 != 12 ) )
=> ( calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X2,X4)
=> calc_date(X0,X1,X2,X4) ) ),
inference(theory_normalization,[],[f50]) ).
tff(f116,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f123,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f129,plain,
! [X0: $int] : ( $product(X0,1) = X0 ),
introduced(definition,[],[tha_right_identity]) ).
tff(f131,plain,
! [X2: $int,X0: $int,X1: $int] : ( $product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2)) ),
introduced(definition,[],[tha_distributivity]) ).
tff(f135,plain,
! [X2: $int,X1: $int] :
( ( $sum($remainder_e(X1,X2),$product(X2,$quotient_e(X1,X2))) = X1 )
| ( 0 = X2 ) ),
introduced(definition,[],[tha_modulo_multiply]) ).
tff(f145,plain,
! [X1: $int,X0: $int] :
( ( ( 2 != X1 )
& ( 1 != X1 ) )
=> zeller_prep(X1,X0,X1,X0,$remainder_e(X0,100),$quotient_e(X0,100)) ),
inference(rectify,[],[f66]) ).
tff(f146,plain,
! [X0: $int,X2: day_name,X10: $int,X8: $int,X9: $int,X4: $int,X7: $int,X3: $int,X1: $int,X5: $int,X6: $int] :
( ( ( $remainder_e($sum($remainder_e(X6,7),7),7) = X5 )
& ( $quotient_e($product(13,$sum(X1,1)),5) = X4 )
& ( 1969 != X8 )
& ( 1985 != X8 )
& ( 2024 != X8 )
& ( $sum(X9,$sum(X4,$sum(X3,$sum($quotient_e(X3,4),$sum($quotient_e(X0,4),$product(5,X0)))))) = X6 )
& map_iso(X5,X2)
& zeller_prep(X7,X8,X1,X10,X3,X0)
& $less(1582,X8)
& ( 1776 != X8 )
& ( 2025 != X8 ) )
=> weekday(ymd(X8,X7,X9),X2) ),
inference(rectify,[],[f93]) ).
tff(f147,plain,
! [X1: $int,X3: $int,X2: date,X4: $int,X0: $int] :
( ( $less(X4,X0)
& ( 12 = X3 )
& is_days_in_month(X3,X1,X4) )
=> ( calc_date($sum(X0,$uminus(X4)),1,$sum(X1,1),X2)
=> calc_date(X0,X3,X1,X2) ) ),
inference(rectify,[],[f95]) ).
tff(f156,plain,
! [X2: date,X4: $int,X0: $int,X3: $int,X1: $int] :
( ( is_days_in_month(X0,X3,X1)
& $less(X1,X4)
& ( 12 != X0 ) )
=> ( calc_date($sum(X4,$uminus(X1)),$sum(X0,1),X3,X2)
=> calc_date(X4,X0,X3,X2) ) ),
inference(rectify,[],[f102]) ).
tff(f160,plain,
~ ? [X2: day_name,X3: $int,X1: $int,X0: $int] :
( valid_day(X0)
& ( 11 = X3 )
& weekday(ymd(X1,X3,X0),X2)
& ( thursday = X2 )
& ( 2026 = X1 )
& calc_date($sum(19,365),11,2025,ymd(X1,X3,X0))
& ( 19 = X0 ) ),
inference(rectify,[],[f89]) ).
tff(f168,plain,
! [X0: $int] :
( ( $less(0,X0)
& ~ $less(31,X0) )
=> valid_day(X0) ),
inference(unused_predicate_definition_removal,[],[f94]) ).
tff(f177,plain,
! [X2: date,X4: $int,X0: $int,X3: $int,X1: $int] :
( calc_date(X4,X0,X3,X2)
| ~ calc_date($sum(X4,$uminus(X1)),$sum(X0,1),X3,X2)
| ~ is_days_in_month(X0,X3,X1)
| ~ $less(X1,X4)
| ( 12 = X0 ) ),
inference(ennf_transformation,[],[f156]) ).
tff(f178,plain,
! [X4: $int,X0: $int,X2: date,X1: $int,X3: $int] :
( ~ $less(X1,X4)
| ( 12 = X0 )
| calc_date(X4,X0,X3,X2)
| ~ is_days_in_month(X0,X3,X1)
| ~ calc_date($sum(X4,$uminus(X1)),$sum(X0,1),X3,X2) ),
inference(flattening,[],[f177]) ).
tff(f183,plain,
! [X0: $int,X2: $int,X1: $int,X3: $int] :
( calc_date(X0,X1,X2,ymd(X2,X1,X0))
| $less(X3,X0)
| ~ is_days_in_month(X1,X2,X3)
| ~ $less(0,X0) ),
inference(ennf_transformation,[],[f99]) ).
tff(f184,plain,
! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ~ is_days_in_month(X1,X2,X3)
| calc_date(X0,X1,X2,ymd(X2,X1,X0))
| ~ $less(0,X0)
| $less(X3,X0) ),
inference(flattening,[],[f183]) ).
tff(f195,plain,
! [X2: day_name,X1: $int,X3: $int,X0: $int] :
( ~ weekday(ymd(X1,X3,X0),X2)
| ( thursday != X2 )
| ~ calc_date($sum(19,365),11,2025,ymd(X1,X3,X0))
| ( 19 != X0 )
| ~ valid_day(X0)
| ( 2026 != X1 )
| ( 11 != X3 ) ),
inference(ennf_transformation,[],[f160]) ).
tff(f200,plain,
! [X0: $int] :
( ( is_days_in_month(2,X0,29)
| ( ( 0 != $remainder_e(X0,400) )
& ( 0 = $remainder_e(X0,100) ) )
| ( 0 != $remainder_e(X0,4) ) )
& ( is_days_in_month(2,X0,28)
| ( ( 0 = $remainder_e(X0,4) )
& ( ( 0 != $remainder_e(X0,100) )
| ( 0 = $remainder_e(X0,400) ) ) ) ) ),
inference(ennf_transformation,[],[f38]) ).
tff(f201,plain,
! [X0: $int] :
( ( is_days_in_month(2,X0,28)
| ( ( 0 = $remainder_e(X0,4) )
& ( ( 0 != $remainder_e(X0,100) )
| ( 0 = $remainder_e(X0,400) ) ) ) )
& ( ( ( 0 != $remainder_e(X0,400) )
& ( 0 = $remainder_e(X0,100) ) )
| is_days_in_month(2,X0,29)
| ( 0 != $remainder_e(X0,4) ) ) ),
inference(flattening,[],[f200]) ).
tff(f209,plain,
! [X1: $int,X0: $int] :
( zeller_prep(X1,X0,X1,X0,$remainder_e(X0,100),$quotient_e(X0,100))
| ( 2 = X1 )
| ( 1 = X1 ) ),
inference(ennf_transformation,[],[f145]) ).
tff(f210,plain,
! [X1: $int,X0: $int] :
( zeller_prep(X1,X0,X1,X0,$remainder_e(X0,100),$quotient_e(X0,100))
| ( 1 = X1 )
| ( 2 = X1 ) ),
inference(flattening,[],[f209]) ).
tff(f224,plain,
! [X0: $int,X2: day_name,X10: $int,X8: $int,X9: $int,X4: $int,X7: $int,X3: $int,X1: $int,X5: $int,X6: $int] :
( weekday(ymd(X8,X7,X9),X2)
| ( $remainder_e($sum($remainder_e(X6,7),7),7) != X5 )
| ( $quotient_e($product(13,$sum(X1,1)),5) != X4 )
| ( 1969 = X8 )
| ( 1985 = X8 )
| ( 2024 = X8 )
| ( $sum(X9,$sum(X4,$sum(X3,$sum($quotient_e(X3,4),$sum($quotient_e(X0,4),$product(5,X0)))))) != X6 )
| ~ map_iso(X5,X2)
| ~ zeller_prep(X7,X8,X1,X10,X3,X0)
| ~ $less(1582,X8)
| ( 1776 = X8 )
| ( 2025 = X8 ) ),
inference(ennf_transformation,[],[f146]) ).
tff(f225,plain,
! [X10: $int,X4: $int,X0: $int,X1: $int,X5: $int,X7: $int,X9: $int,X8: $int,X6: $int,X3: $int,X2: day_name] :
( ( 2024 = X8 )
| weekday(ymd(X8,X7,X9),X2)
| ( 1776 = X8 )
| ( $quotient_e($product(13,$sum(X1,1)),5) != X4 )
| ~ map_iso(X5,X2)
| ~ zeller_prep(X7,X8,X1,X10,X3,X0)
| ( 2025 = X8 )
| ~ $less(1582,X8)
| ( 1985 = X8 )
| ( 1969 = X8 )
| ( $remainder_e($sum($remainder_e(X6,7),7),7) != X5 )
| ( $sum(X9,$sum(X4,$sum(X3,$sum($quotient_e(X3,4),$sum($quotient_e(X0,4),$product(5,X0)))))) != X6 ) ),
inference(flattening,[],[f224]) ).
tff(f228,plain,
! [X0: $int] :
( valid_day(X0)
| ~ $less(0,X0)
| $less(31,X0) ),
inference(ennf_transformation,[],[f168]) ).
tff(f229,plain,
! [X0: $int] :
( $less(31,X0)
| valid_day(X0)
| ~ $less(0,X0) ),
inference(flattening,[],[f228]) ).
tff(f232,plain,
! [X1: $int,X3: $int,X2: date,X4: $int,X0: $int] :
( calc_date(X0,X3,X1,X2)
| ~ calc_date($sum(X0,$uminus(X4)),1,$sum(X1,1),X2)
| ~ $less(X4,X0)
| ( 12 != X3 )
| ~ is_days_in_month(X3,X1,X4) ),
inference(ennf_transformation,[],[f147]) ).
tff(f233,plain,
! [X3: $int,X4: $int,X2: date,X1: $int,X0: $int] :
( calc_date(X0,X3,X1,X2)
| ( 12 != X3 )
| ~ is_days_in_month(X3,X1,X4)
| ~ calc_date($sum(X0,$uminus(X4)),1,$sum(X1,1),X2)
| ~ $less(X4,X0) ),
inference(flattening,[],[f232]) ).
tff(f243,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int,X4: $int,X5: $int,X6: $int,X7: $int,X8: $int,X9: $int,X10: day_name] :
( ( 2024 = X7 )
| weekday(ymd(X7,X5,X6),X10)
| ( 1776 = X7 )
| ( $quotient_e($product(13,$sum(X3,1)),5) != X1 )
| ~ map_iso(X4,X10)
| ~ zeller_prep(X5,X7,X3,X0,X9,X2)
| ( 2025 = X7 )
| ~ $less(1582,X7)
| ( 1985 = X7 )
| ( 1969 = X7 )
| ( $remainder_e($sum($remainder_e(X8,7),7),7) != X4 )
| ( $sum(X6,$sum(X1,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X8 ) ),
inference(rectify,[],[f225]) ).
tff(f244,plain,
! [X0: $int,X1: $int,X2: date,X3: $int,X4: $int] :
( ~ $less(X3,X0)
| ( 12 = X1 )
| calc_date(X0,X1,X4,X2)
| ~ is_days_in_month(X1,X4,X3)
| ~ calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X4,X2) ),
inference(rectify,[],[f178]) ).
tff(f247,plain,
! [X0: $int,X1: $int] :
( zeller_prep(X0,X1,X0,X1,$remainder_e(X1,100),$quotient_e(X1,100))
| ( 1 = X0 )
| ( 2 = X0 ) ),
inference(rectify,[],[f210]) ).
tff(f251,plain,
! [X0: day_name,X1: $int,X2: $int,X3: $int] :
( ~ weekday(ymd(X1,X2,X3),X0)
| ( thursday != X0 )
| ~ calc_date($sum(19,365),11,2025,ymd(X1,X2,X3))
| ( 19 != X3 )
| ~ valid_day(X3)
| ( 2026 != X1 )
| ( 11 != X2 ) ),
inference(rectify,[],[f195]) ).
tff(f256,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int] :
( ~ is_days_in_month(X1,X0,X2)
| calc_date(X3,X1,X0,ymd(X0,X1,X3))
| ~ $less(0,X3)
| $less(X2,X3) ),
inference(rectify,[],[f184]) ).
tff(f261,plain,
! [X0: $int,X1: $int,X2: date,X3: $int,X4: $int] :
( calc_date(X4,X0,X3,X2)
| ( 12 != X0 )
| ~ is_days_in_month(X0,X3,X1)
| ~ calc_date($sum(X4,$uminus(X1)),1,$sum(X3,1),X2)
| ~ $less(X1,X4) ),
inference(rectify,[],[f233]) ).
tff(f266,plain,
! [X0: $int] : is_days_in_month(11,X0,30),
inference(cnf_transformation,[],[f47]) ).
tff(f276,plain,
map_iso(5,thursday),
inference(cnf_transformation,[],[f73]) ).
tff(f281,plain,
! [X2: $int,X3: $int,X10: day_name,X0: $int,X1: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: $int,X5: $int] :
( ( 2024 = X7 )
| weekday(ymd(X7,X5,X6),X10)
| ( 1776 = X7 )
| ( $quotient_e($product(13,$sum(X3,1)),5) != X1 )
| ~ map_iso(X4,X10)
| ~ zeller_prep(X5,X7,X3,X0,X9,X2)
| ( 2025 = X7 )
| ~ $less(1582,X7)
| ( 1985 = X7 )
| ( 1969 = X7 )
| ( $remainder_e($sum($remainder_e(X8,7),7),7) != X4 )
| ( $sum(X6,$sum(X1,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X8 ) ),
inference(cnf_transformation,[],[f243]) ).
tff(f282,plain,
! [X2: date,X3: $int,X0: $int,X1: $int,X4: $int] :
( calc_date(X0,X1,X4,X2)
| ( 12 = X1 )
| ~ $less(X3,X0)
| ~ is_days_in_month(X1,X4,X3)
| ~ calc_date($sum(X0,$uminus(X3)),$sum(X1,1),X4,X2) ),
inference(cnf_transformation,[],[f244]) ).
tff(f292,plain,
! [X0: $int,X1: $int] :
( zeller_prep(X0,X1,X0,X1,$remainder_e(X1,100),$quotient_e(X1,100))
| ( 2 = X0 )
| ( 1 = X0 ) ),
inference(cnf_transformation,[],[f247]) ).
tff(f293,plain,
! [X0: $int] : is_days_in_month(1,X0,31),
inference(cnf_transformation,[],[f37]) ).
tff(f306,plain,
! [X0: $int] : is_days_in_month(6,X0,30),
inference(cnf_transformation,[],[f42]) ).
tff(f307,plain,
! [X2: $int,X3: $int,X0: day_name,X1: $int] :
( ~ weekday(ymd(X1,X2,X3),X0)
| ( thursday != X0 )
| ~ calc_date($sum(19,365),11,2025,ymd(X1,X2,X3))
| ( 19 != X3 )
| ~ valid_day(X3)
| ( 2026 != X1 )
| ( 11 != X2 ) ),
inference(cnf_transformation,[],[f251]) ).
tff(f311,plain,
! [X0: $int] : is_days_in_month(8,X0,31),
inference(cnf_transformation,[],[f44]) ).
tff(f313,plain,
! [X0: $int] : is_days_in_month(4,X0,30),
inference(cnf_transformation,[],[f40]) ).
tff(f315,plain,
! [X0: $int] : is_days_in_month(3,X0,31),
inference(cnf_transformation,[],[f39]) ).
tff(f325,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( calc_date(X3,X1,X0,ymd(X0,X1,X3))
| ~ $less(0,X3)
| ~ is_days_in_month(X1,X0,X2)
| $less(X2,X3) ),
inference(cnf_transformation,[],[f256]) ).
tff(f328,plain,
! [X0: $int] : is_days_in_month(7,X0,31),
inference(cnf_transformation,[],[f43]) ).
tff(f329,plain,
! [X0: $int] : is_days_in_month(10,X0,31),
inference(cnf_transformation,[],[f46]) ).
tff(f331,plain,
! [X0: $int] : is_days_in_month(12,X0,31),
inference(cnf_transformation,[],[f48]) ).
tff(f338,plain,
! [X0: $int] :
( ( 0 = $remainder_e(X0,4) )
| is_days_in_month(2,X0,28) ),
inference(cnf_transformation,[],[f201]) ).
tff(f347,plain,
! [X0: $int] :
( ~ $less(0,X0)
| $less(31,X0)
| valid_day(X0) ),
inference(cnf_transformation,[],[f229]) ).
tff(f348,plain,
! [X2: date,X3: $int,X0: $int,X1: $int,X4: $int] :
( calc_date(X4,X0,X3,X2)
| ( 12 != X0 )
| ~ is_days_in_month(X0,X3,X1)
| ~ calc_date($sum(X4,$uminus(X1)),1,$sum(X3,1),X2)
| ~ $less(X1,X4) ),
inference(cnf_transformation,[],[f261]) ).
tff(f352,plain,
! [X0: $int] : is_days_in_month(5,X0,31),
inference(cnf_transformation,[],[f41]) ).
tff(f353,plain,
! [X0: $int] : is_days_in_month(9,X0,30),
inference(cnf_transformation,[],[f45]) ).
tff(f366,plain,
! [X2: $int,X3: $int,X10: day_name,X0: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: $int,X5: $int] :
( ( 2024 = X7 )
| weekday(ymd(X7,X5,X6),X10)
| ( 1776 = X7 )
| ~ map_iso(X4,X10)
| ~ zeller_prep(X5,X7,X3,X0,X9,X2)
| ( 2025 = X7 )
| ~ $less(1582,X7)
| ( 1985 = X7 )
| ( 1969 = X7 )
| ( $remainder_e($sum($remainder_e(X8,7),7),7) != X4 )
| ( $sum(X6,$sum($quotient_e($product(13,$sum(X3,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X8 ) ),
inference(equality_resolution,[],[f281]) ).
tff(f367,plain,
! [X2: $int,X3: $int,X10: day_name,X0: $int,X8: $int,X6: $int,X9: $int,X7: $int,X5: $int] :
( ( 2024 = X7 )
| weekday(ymd(X7,X5,X6),X10)
| ( 1776 = X7 )
| ~ map_iso($remainder_e($sum($remainder_e(X8,7),7),7),X10)
| ~ zeller_prep(X5,X7,X3,X0,X9,X2)
| ( 2025 = X7 )
| ~ $less(1582,X7)
| ( 1985 = X7 )
| ( 1969 = X7 )
| ( $sum(X6,$sum($quotient_e($product(13,$sum(X3,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X8 ) ),
inference(equality_resolution,[],[f366]) ).
tff(f368,plain,
! [X2: $int,X3: $int,X10: day_name,X0: $int,X6: $int,X9: $int,X7: $int,X5: $int] :
( ~ $less(1582,X7)
| ~ map_iso($remainder_e($sum($remainder_e($sum(X6,$sum($quotient_e($product(13,$sum(X3,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7),7),7),X10)
| ( 2025 = X7 )
| ( 1969 = X7 )
| ( 2024 = X7 )
| weekday(ymd(X7,X5,X6),X10)
| ( 1985 = X7 )
| ~ zeller_prep(X5,X7,X3,X0,X9,X2)
| ( 1776 = X7 ) ),
inference(equality_resolution,[],[f367]) ).
tff(f375,plain,
! [X2: $int,X3: $int,X1: $int] :
( ~ weekday(ymd(X1,X2,X3),thursday)
| ~ calc_date($sum(19,365),11,2025,ymd(X1,X2,X3))
| ( 19 != X3 )
| ~ valid_day(X3)
| ( 2026 != X1 )
| ( 11 != X2 ) ),
inference(equality_resolution,[],[f307]) ).
tff(f376,plain,
! [X2: $int,X1: $int] :
( ~ weekday(ymd(X1,X2,19),thursday)
| ~ calc_date($sum(19,365),11,2025,ymd(X1,X2,19))
| ~ valid_day(19)
| ( 2026 != X1 )
| ( 11 != X2 ) ),
inference(equality_resolution,[],[f375]) ).
tff(f377,plain,
! [X2: $int] :
( ~ weekday(ymd(2026,X2,19),thursday)
| ~ calc_date($sum(19,365),11,2025,ymd(2026,X2,19))
| ~ valid_day(19)
| ( 11 != X2 ) ),
inference(equality_resolution,[],[f376]) ).
tff(f378,plain,
( ~ weekday(ymd(2026,11,19),thursday)
| ~ calc_date($sum(19,365),11,2025,ymd(2026,11,19))
| ~ valid_day(19) ),
inference(equality_resolution,[],[f377]) ).
tff(f385,plain,
! [X2: date,X3: $int,X1: $int,X4: $int] :
( calc_date(X4,12,X3,X2)
| ~ is_days_in_month(12,X3,X1)
| ~ $less(X1,X4)
| ~ calc_date($sum(X4,$uminus(X1)),1,$sum(X3,1),X2) ),
inference(equality_resolution,[],[f348]) ).
tff(f387,definition,
sF0 = ymd(2026,11,19),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
tff(f388,plain,
ymd(2026,11,19) = sF0,
inference(reorient_equations,[],[f387]) ).
tff(f389,definition,
sF1 = $sum(19,365),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
tff(f390,plain,
$sum(19,365) = sF1,
inference(reorient_equations,[],[f389]) ).
tff(f391,plain,
( ~ calc_date(sF1,11,2025,sF0)
| ~ weekday(sF0,thursday)
| ~ valid_day(19) ),
inference(definition_folding,[],[f378,f388,f390,f388]) ).
tff(f402,plain,
384 = sF1,
inference(evaluation,[],[f390]) ).
tff(f521,definition,
( spl2_22
<=> ( ymd(2026,11,19) = sF0 ) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
tff(f523,plain,
( ( ymd(2026,11,19) = sF0 )
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f521]) ).
tff(f524,plain,
spl2_22,
inference(avatar_split_clause,[],[f388,f521]) ).
tff(f536,definition,
( spl2_25
<=> ( 384 = sF1 ) ),
introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition]) ).
tff(f538,plain,
( ( 384 = sF1 )
| ~ spl2_25 ),
inference(avatar_component_clause,[],[f536]) ).
tff(f539,plain,
spl2_25,
inference(avatar_split_clause,[],[f402,f536]) ).
tff(f576,definition,
( spl2_33
<=> weekday(sF0,thursday) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
tff(f580,definition,
( spl2_34
<=> calc_date(sF1,11,2025,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
tff(f582,plain,
( ~ calc_date(sF1,11,2025,sF0)
| spl2_34 ),
inference(avatar_component_clause,[],[f580]) ).
tff(f584,definition,
( spl2_35
<=> valid_day(19) ),
introduced(definition,[new_symbols(definition,[spl2_35])],[avatar_definition]) ).
tff(f586,plain,
( ~ valid_day(19)
| spl2_35 ),
inference(avatar_component_clause,[],[f584]) ).
tff(f587,plain,
( ~ spl2_33
| ~ spl2_34
| ~ spl2_35 ),
inference(avatar_split_clause,[],[f391,f584,f580,f576]) ).
tff(f624,definition,
( spl2_43
<=> map_iso(5,thursday) ),
introduced(definition,[new_symbols(definition,[spl2_43])],[avatar_definition]) ).
tff(f626,plain,
( map_iso(5,thursday)
| ~ spl2_43 ),
inference(avatar_component_clause,[],[f624]) ).
tff(f627,plain,
spl2_43,
inference(avatar_split_clause,[],[f276,f624]) ).
tff(f701,plain,
! [X0: $int] :
( valid_day(X0)
| $less(X0,0)
| ( 0 = X0 )
| $less(31,X0) ),
inference(resolution,[],[f123,f347]) ).
tff(f824,plain,
! [X0: $int,X1: $int] : ( $product(X0,$sum(X1,1)) = $sum($product(X0,X1),X0) ),
inference(superposition,[],[f131,f129]) ).
tff(f836,plain,
! [X0: $int,X1: $int] : ( $product(X0,$sum(X1,1)) = $sum(X0,$product(X0,X1)) ),
inference(forward_demodulation,[],[f824,f116]) ).
tff(f865,plain,
! [X0: $int] :
( ( 0 = 4 )
| ( $sum(0,$product(4,$quotient_e(X0,4))) = X0 )
| is_days_in_month(2,X0,28) ),
inference(superposition,[],[f135,f338]) ).
tff(f868,plain,
! [X0: $int] :
( is_days_in_month(2,X0,28)
| ( $product(4,$quotient_e(X0,4)) = X0 ) ),
inference(evaluation,[],[f865]) ).
tff(f916,plain,
( ! [X0: $int] :
( calc_date(19,11,2026,sF0)
| ~ is_days_in_month(11,2026,X0)
| ~ $less(0,19)
| $less(X0,19) )
| ~ spl2_22 ),
inference(superposition,[],[f325,f523]) ).
tff(f917,plain,
( ! [X0: $int] :
( calc_date(19,11,2026,sF0)
| $less(X0,19)
| ~ is_days_in_month(11,2026,X0) )
| ~ spl2_22 ),
inference(evaluation,[],[f916]) ).
tff(f919,definition,
( spl2_47
<=> ! [X0: $int] :
( $less(X0,19)
| ~ is_days_in_month(11,2026,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_47])],[avatar_definition]) ).
tff(f920,plain,
( ! [X0: $int] :
( ~ is_days_in_month(11,2026,X0)
| $less(X0,19) )
| ~ spl2_47 ),
inference(avatar_component_clause,[],[f919]) ).
tff(f922,definition,
( spl2_48
<=> calc_date(19,11,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_48])],[avatar_definition]) ).
tff(f925,plain,
( spl2_47
| spl2_48
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f917,f521,f922,f919]) ).
tff(f1124,plain,
! [X2: $int,X3: $int,X10: day_name,X0: $int,X6: $int,X9: $int,X7: $int,X5: $int] :
( weekday(ymd(X7,X5,X6),X10)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X6,$sum($quotient_e($product(13,$sum(X3,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7)),7),X10)
| ( 1985 = X7 )
| ( 2025 = X7 )
| ( 1776 = X7 )
| ( 1969 = X7 )
| ~ $less(1582,X7)
| ( 2024 = X7 )
| ~ zeller_prep(X5,X7,X3,X0,X9,X2) ),
inference(forward_demodulation,[],[f368,f116]) ).
tff(f1145,plain,
( ! [X2: $int,X3: $int,X0: day_name,X1: $int,X4: $int] :
( ( 2024 = 2026 )
| ( 1776 = 2026 )
| weekday(sF0,X0)
| ( 1969 = 2026 )
| ( 2025 = 2026 )
| ( 1985 = 2026 )
| ~ $less(1582,2026)
| ~ zeller_prep(11,2026,X1,X4,X2,X3)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(19,$sum($quotient_e($product(13,$sum(X1,1)),5),$sum(X2,$sum($quotient_e(X2,4),$sum($quotient_e(X3,4),$product(5,X3)))))),7)),7),X0) )
| ~ spl2_22 ),
inference(superposition,[],[f1124,f523]) ).
tff(f1146,plain,
( ! [X2: $int,X3: $int,X0: day_name,X1: $int,X4: $int] :
( weekday(sF0,X0)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(19,$sum($quotient_e($product(13,$sum(X1,1)),5),$sum(X2,$sum($quotient_e(X2,4),$sum($quotient_e(X3,4),$product(5,X3)))))),7)),7),X0)
| ~ zeller_prep(11,2026,X1,X4,X2,X3) )
| ~ spl2_22 ),
inference(evaluation,[],[f1145]) ).
tff(f1793,plain,
( ( 0 = 19 )
| $less(31,19)
| $less(19,0)
| spl2_35 ),
inference(resolution,[],[f701,f586]) ).
tff(f1794,plain,
( $false
| spl2_35 ),
inference(evaluation,[],[f1793]) ).
tff(f1795,plain,
spl2_35,
inference(avatar_contradiction_clause,[],[f1794]) ).
tff(f4637,plain,
( ! [X2: $int,X3: $int,X0: day_name,X1: $int,X4: $int] :
( ~ zeller_prep(11,2026,X1,X4,X2,X3)
| weekday(sF0,X0)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(19,$sum($quotient_e($sum(13,$product(13,X1)),5),$sum(X2,$sum($quotient_e(X2,4),$sum($quotient_e(X3,4),$product(5,X3)))))),7)),7),X0) )
| ~ spl2_22 ),
inference(forward_demodulation,[],[f1146,f836]) ).
tff(f4655,plain,
( ! [X0: day_name] :
( ~ map_iso($remainder_e($sum(7,$remainder_e($sum(19,$sum($quotient_e($sum(13,$product(13,11)),5),$sum($remainder_e(2026,100),$sum($quotient_e($remainder_e(2026,100),4),$sum($quotient_e($quotient_e(2026,100),4),$product(5,$quotient_e(2026,100))))))),7)),7),X0)
| weekday(sF0,X0)
| ( 2 = 11 )
| ( 1 = 11 ) )
| ~ spl2_22 ),
inference(resolution,[],[f4637,f292]) ).
tff(f4656,plain,
( ! [X0: day_name] :
( ~ map_iso(5,X0)
| weekday(sF0,X0) )
| ~ spl2_22 ),
inference(evaluation,[],[f4655]) ).
tff(f4657,plain,
( weekday(sF0,thursday)
| ~ spl2_22
| ~ spl2_43 ),
inference(resolution,[],[f4656,f626]) ).
tff(f4660,plain,
( ~ calc_date(384,11,2025,sF0)
| ~ spl2_25
| spl2_34 ),
inference(forward_demodulation,[],[f582,f538]) ).
tff(f4661,plain,
( spl2_33
| ~ spl2_22
| ~ spl2_43 ),
inference(avatar_split_clause,[],[f4657,f624,f521,f576]) ).
tff(f4663,definition,
( spl2_85
<=> calc_date(384,11,2025,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_85])],[avatar_definition]) ).
tff(f4665,plain,
( ~ calc_date(384,11,2025,sF0)
| spl2_85 ),
inference(avatar_component_clause,[],[f4663]) ).
tff(f4666,plain,
( ~ spl2_85
| ~ spl2_25
| spl2_34 ),
inference(avatar_split_clause,[],[f4660,f580,f536,f4663]) ).
tff(f4670,plain,
( ! [X0: $int] :
( ( 11 = 12 )
| ~ calc_date($sum(384,$uminus(X0)),$sum(11,1),2025,sF0)
| ~ $less(X0,384)
| ~ is_days_in_month(11,2025,X0) )
| spl2_85 ),
inference(resolution,[],[f4665,f282]) ).
tff(f4671,plain,
( ! [X0: $int] :
( ~ is_days_in_month(11,2025,X0)
| ~ $less(X0,384)
| ~ calc_date($sum(384,$uminus(X0)),12,2025,sF0) )
| spl2_85 ),
inference(evaluation,[],[f4670]) ).
tff(f4675,plain,
( ~ $less(30,384)
| ~ calc_date($sum(384,$uminus(30)),12,2025,sF0)
| spl2_85 ),
inference(resolution,[],[f4671,f266]) ).
tff(f4677,plain,
( ~ calc_date(354,12,2025,sF0)
| spl2_85 ),
inference(evaluation,[],[f4675]) ).
tff(f4679,definition,
( spl2_86
<=> calc_date(354,12,2025,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
tff(f4681,plain,
( ~ calc_date(354,12,2025,sF0)
| spl2_86 ),
inference(avatar_component_clause,[],[f4679]) ).
tff(f4682,plain,
( ~ spl2_86
| spl2_85 ),
inference(avatar_split_clause,[],[f4677,f4663,f4679]) ).
tff(f4703,plain,
( ! [X0: $int] :
( ~ calc_date($sum(354,$uminus(X0)),1,$sum(2025,1),sF0)
| ~ $less(X0,354)
| ~ is_days_in_month(12,2025,X0) )
| spl2_86 ),
inference(resolution,[],[f4681,f385]) ).
tff(f4706,plain,
( ! [X0: $int] :
( ~ is_days_in_month(12,2025,X0)
| ~ calc_date($sum(354,$uminus(X0)),1,2026,sF0)
| ~ $less(X0,354) )
| spl2_86 ),
inference(evaluation,[],[f4703]) ).
tff(f4769,plain,
( ~ $less(31,354)
| ~ calc_date($sum(354,$uminus(31)),1,2026,sF0)
| spl2_86 ),
inference(resolution,[],[f4706,f331]) ).
tff(f4771,plain,
( ~ calc_date(323,1,2026,sF0)
| spl2_86 ),
inference(evaluation,[],[f4769]) ).
tff(f4773,definition,
( spl2_90
<=> calc_date(323,1,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_90])],[avatar_definition]) ).
tff(f4775,plain,
( ~ calc_date(323,1,2026,sF0)
| spl2_90 ),
inference(avatar_component_clause,[],[f4773]) ).
tff(f4776,plain,
( ~ spl2_90
| spl2_86 ),
inference(avatar_split_clause,[],[f4771,f4679,f4773]) ).
tff(f4821,plain,
( ! [X0: $int] :
( ~ is_days_in_month(1,2026,X0)
| ( 1 = 12 )
| ~ calc_date($sum(323,$uminus(X0)),$sum(1,1),2026,sF0)
| ~ $less(X0,323) )
| spl2_90 ),
inference(resolution,[],[f4775,f282]) ).
tff(f4823,plain,
( ! [X0: $int] :
( ~ is_days_in_month(1,2026,X0)
| ~ calc_date($sum(323,$uminus(X0)),2,2026,sF0)
| ~ $less(X0,323) )
| spl2_90 ),
inference(evaluation,[],[f4821]) ).
tff(f4871,plain,
( ~ calc_date($sum(323,$uminus(31)),2,2026,sF0)
| ~ $less(31,323)
| spl2_90 ),
inference(resolution,[],[f4823,f293]) ).
tff(f4873,plain,
( ~ calc_date(292,2,2026,sF0)
| spl2_90 ),
inference(evaluation,[],[f4871]) ).
tff(f4875,definition,
( spl2_92
<=> calc_date(292,2,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_92])],[avatar_definition]) ).
tff(f4877,plain,
( ~ calc_date(292,2,2026,sF0)
| spl2_92 ),
inference(avatar_component_clause,[],[f4875]) ).
tff(f4878,plain,
( ~ spl2_92
| spl2_90 ),
inference(avatar_split_clause,[],[f4873,f4773,f4875]) ).
tff(f4893,plain,
( ! [X0: $int] :
( ~ calc_date($sum(292,$uminus(X0)),$sum(2,1),2026,sF0)
| ( 2 = 12 )
| ~ is_days_in_month(2,2026,X0)
| ~ $less(X0,292) )
| spl2_92 ),
inference(resolution,[],[f4877,f282]) ).
tff(f4894,plain,
( ! [X0: $int] :
( ~ is_days_in_month(2,2026,X0)
| ~ calc_date($sum(292,$uminus(X0)),3,2026,sF0)
| ~ $less(X0,292) )
| spl2_92 ),
inference(evaluation,[],[f4893]) ).
tff(f4928,plain,
( ( 2026 = $product(4,$quotient_e(2026,4)) )
| ~ calc_date($sum(292,$uminus(28)),3,2026,sF0)
| ~ $less(28,292)
| spl2_92 ),
inference(resolution,[],[f4894,f868]) ).
tff(f4930,plain,
( ~ calc_date(264,3,2026,sF0)
| spl2_92 ),
inference(evaluation,[],[f4928]) ).
tff(f4932,definition,
( spl2_93
<=> calc_date(264,3,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
tff(f4934,plain,
( ~ calc_date(264,3,2026,sF0)
| spl2_93 ),
inference(avatar_component_clause,[],[f4932]) ).
tff(f4935,plain,
( ~ spl2_93
| spl2_92 ),
inference(avatar_split_clause,[],[f4930,f4875,f4932]) ).
tff(f5407,plain,
( ! [X0: $int] :
( ~ is_days_in_month(3,2026,X0)
| ~ $less(X0,264)
| ( 3 = 12 )
| ~ calc_date($sum(264,$uminus(X0)),$sum(3,1),2026,sF0) )
| spl2_93 ),
inference(resolution,[],[f4934,f282]) ).
tff(f5408,plain,
( ! [X0: $int] :
( ~ is_days_in_month(3,2026,X0)
| ~ calc_date($sum(264,$uminus(X0)),4,2026,sF0)
| ~ $less(X0,264) )
| spl2_93 ),
inference(evaluation,[],[f5407]) ).
tff(f9516,plain,
( ~ $less(31,264)
| ~ calc_date($sum(264,$uminus(31)),4,2026,sF0)
| spl2_93 ),
inference(resolution,[],[f5408,f315]) ).
tff(f9518,plain,
( ~ calc_date(233,4,2026,sF0)
| spl2_93 ),
inference(evaluation,[],[f9516]) ).
tff(f9520,definition,
( spl2_178
<=> calc_date(233,4,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_178])],[avatar_definition]) ).
tff(f9522,plain,
( ~ calc_date(233,4,2026,sF0)
| spl2_178 ),
inference(avatar_component_clause,[],[f9520]) ).
tff(f9523,plain,
( ~ spl2_178
| spl2_93 ),
inference(avatar_split_clause,[],[f9518,f4932,f9520]) ).
tff(f9525,plain,
( ! [X0: $int] :
( ~ $less(X0,233)
| ~ is_days_in_month(4,2026,X0)
| ( 4 = 12 )
| ~ calc_date($sum(233,$uminus(X0)),$sum(4,1),2026,sF0) )
| spl2_178 ),
inference(resolution,[],[f9522,f282]) ).
tff(f9526,plain,
( ! [X0: $int] :
( ~ is_days_in_month(4,2026,X0)
| ~ calc_date($sum(233,$uminus(X0)),5,2026,sF0)
| ~ $less(X0,233) )
| spl2_178 ),
inference(evaluation,[],[f9525]) ).
tff(f9849,plain,
( ~ $less(30,233)
| ~ calc_date($sum(233,$uminus(30)),5,2026,sF0)
| spl2_178 ),
inference(resolution,[],[f9526,f313]) ).
tff(f9851,plain,
( ~ calc_date(203,5,2026,sF0)
| spl2_178 ),
inference(evaluation,[],[f9849]) ).
tff(f9853,definition,
( spl2_179
<=> calc_date(203,5,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_179])],[avatar_definition]) ).
tff(f9855,plain,
( ~ calc_date(203,5,2026,sF0)
| spl2_179 ),
inference(avatar_component_clause,[],[f9853]) ).
tff(f9856,plain,
( ~ spl2_179
| spl2_178 ),
inference(avatar_split_clause,[],[f9851,f9520,f9853]) ).
tff(f9858,plain,
( ! [X0: $int] :
( ~ is_days_in_month(5,2026,X0)
| ~ $less(X0,203)
| ~ calc_date($sum(203,$uminus(X0)),$sum(5,1),2026,sF0)
| ( 5 = 12 ) )
| spl2_179 ),
inference(resolution,[],[f9855,f282]) ).
tff(f9859,plain,
( ! [X0: $int] :
( ~ is_days_in_month(5,2026,X0)
| ~ $less(X0,203)
| ~ calc_date($sum(203,$uminus(X0)),6,2026,sF0) )
| spl2_179 ),
inference(evaluation,[],[f9858]) ).
tff(f9860,plain,
( ~ $less(31,203)
| ~ calc_date($sum(203,$uminus(31)),6,2026,sF0)
| spl2_179 ),
inference(resolution,[],[f9859,f352]) ).
tff(f9862,plain,
( ~ calc_date(172,6,2026,sF0)
| spl2_179 ),
inference(evaluation,[],[f9860]) ).
tff(f9864,definition,
( spl2_180
<=> calc_date(172,6,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_180])],[avatar_definition]) ).
tff(f9866,plain,
( ~ calc_date(172,6,2026,sF0)
| spl2_180 ),
inference(avatar_component_clause,[],[f9864]) ).
tff(f9867,plain,
( ~ spl2_180
| spl2_179 ),
inference(avatar_split_clause,[],[f9862,f9853,f9864]) ).
tff(f9869,plain,
( ! [X0: $int] :
( ~ $less(X0,172)
| ~ calc_date($sum(172,$uminus(X0)),$sum(6,1),2026,sF0)
| ( 12 = 6 )
| ~ is_days_in_month(6,2026,X0) )
| spl2_180 ),
inference(resolution,[],[f9866,f282]) ).
tff(f9870,plain,
( ! [X0: $int] :
( ~ is_days_in_month(6,2026,X0)
| ~ $less(X0,172)
| ~ calc_date($sum(172,$uminus(X0)),7,2026,sF0) )
| spl2_180 ),
inference(evaluation,[],[f9869]) ).
tff(f9871,plain,
( ~ calc_date($sum(172,$uminus(30)),7,2026,sF0)
| ~ $less(30,172)
| spl2_180 ),
inference(resolution,[],[f9870,f306]) ).
tff(f9873,plain,
( ~ calc_date(142,7,2026,sF0)
| spl2_180 ),
inference(evaluation,[],[f9871]) ).
tff(f9875,definition,
( spl2_181
<=> calc_date(142,7,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_181])],[avatar_definition]) ).
tff(f9877,plain,
( ~ calc_date(142,7,2026,sF0)
| spl2_181 ),
inference(avatar_component_clause,[],[f9875]) ).
tff(f9878,plain,
( ~ spl2_181
| spl2_180 ),
inference(avatar_split_clause,[],[f9873,f9864,f9875]) ).
tff(f9880,plain,
( ! [X0: $int] :
( ~ is_days_in_month(7,2026,X0)
| ~ calc_date($sum(142,$uminus(X0)),$sum(7,1),2026,sF0)
| ( 12 = 7 )
| ~ $less(X0,142) )
| spl2_181 ),
inference(resolution,[],[f9877,f282]) ).
tff(f9881,plain,
( ! [X0: $int] :
( ~ is_days_in_month(7,2026,X0)
| ~ $less(X0,142)
| ~ calc_date($sum(142,$uminus(X0)),8,2026,sF0) )
| spl2_181 ),
inference(evaluation,[],[f9880]) ).
tff(f9882,plain,
( ~ calc_date($sum(142,$uminus(31)),8,2026,sF0)
| ~ $less(31,142)
| spl2_181 ),
inference(resolution,[],[f9881,f328]) ).
tff(f9884,plain,
( ~ calc_date(111,8,2026,sF0)
| spl2_181 ),
inference(evaluation,[],[f9882]) ).
tff(f9886,definition,
( spl2_182
<=> calc_date(111,8,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_182])],[avatar_definition]) ).
tff(f9888,plain,
( ~ calc_date(111,8,2026,sF0)
| spl2_182 ),
inference(avatar_component_clause,[],[f9886]) ).
tff(f9889,plain,
( ~ spl2_182
| spl2_181 ),
inference(avatar_split_clause,[],[f9884,f9875,f9886]) ).
tff(f9891,plain,
( ! [X0: $int] :
( ( 12 = 8 )
| ~ $less(X0,111)
| ~ is_days_in_month(8,2026,X0)
| ~ calc_date($sum(111,$uminus(X0)),$sum(8,1),2026,sF0) )
| spl2_182 ),
inference(resolution,[],[f9888,f282]) ).
tff(f9892,plain,
( ! [X0: $int] :
( ~ is_days_in_month(8,2026,X0)
| ~ calc_date($sum(111,$uminus(X0)),9,2026,sF0)
| ~ $less(X0,111) )
| spl2_182 ),
inference(evaluation,[],[f9891]) ).
tff(f9893,plain,
( ~ calc_date($sum(111,$uminus(31)),9,2026,sF0)
| ~ $less(31,111)
| spl2_182 ),
inference(resolution,[],[f9892,f311]) ).
tff(f9895,plain,
( ~ calc_date(80,9,2026,sF0)
| spl2_182 ),
inference(evaluation,[],[f9893]) ).
tff(f9897,definition,
( spl2_183
<=> calc_date(80,9,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_183])],[avatar_definition]) ).
tff(f9899,plain,
( ~ calc_date(80,9,2026,sF0)
| spl2_183 ),
inference(avatar_component_clause,[],[f9897]) ).
tff(f9900,plain,
( ~ spl2_183
| spl2_182 ),
inference(avatar_split_clause,[],[f9895,f9886,f9897]) ).
tff(f10068,plain,
( ! [X0: $int] :
( ~ is_days_in_month(9,2026,X0)
| ( 12 = 9 )
| ~ $less(X0,80)
| ~ calc_date($sum(80,$uminus(X0)),$sum(9,1),2026,sF0) )
| spl2_183 ),
inference(resolution,[],[f9899,f282]) ).
tff(f10069,plain,
( ! [X0: $int] :
( ~ is_days_in_month(9,2026,X0)
| ~ $less(X0,80)
| ~ calc_date($sum(80,$uminus(X0)),10,2026,sF0) )
| spl2_183 ),
inference(evaluation,[],[f10068]) ).
tff(f10070,plain,
( ~ $less(30,80)
| ~ calc_date($sum(80,$uminus(30)),10,2026,sF0)
| spl2_183 ),
inference(resolution,[],[f10069,f353]) ).
tff(f10072,plain,
( ~ calc_date(50,10,2026,sF0)
| spl2_183 ),
inference(evaluation,[],[f10070]) ).
tff(f10074,definition,
( spl2_184
<=> calc_date(50,10,2026,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_184])],[avatar_definition]) ).
tff(f10076,plain,
( ~ calc_date(50,10,2026,sF0)
| spl2_184 ),
inference(avatar_component_clause,[],[f10074]) ).
tff(f10077,plain,
( ~ spl2_184
| spl2_183 ),
inference(avatar_split_clause,[],[f10072,f9897,f10074]) ).
tff(f10079,plain,
( ! [X0: $int] :
( ( 12 = 10 )
| ~ is_days_in_month(10,2026,X0)
| ~ $less(X0,50)
| ~ calc_date($sum(50,$uminus(X0)),$sum(10,1),2026,sF0) )
| spl2_184 ),
inference(resolution,[],[f10076,f282]) ).
tff(f10080,plain,
( ! [X0: $int] :
( ~ is_days_in_month(10,2026,X0)
| ~ $less(X0,50)
| ~ calc_date($sum(50,$uminus(X0)),11,2026,sF0) )
| spl2_184 ),
inference(evaluation,[],[f10079]) ).
tff(f10081,plain,
( ~ $less(31,50)
| ~ calc_date($sum(50,$uminus(31)),11,2026,sF0)
| spl2_184 ),
inference(resolution,[],[f10080,f329]) ).
tff(f10083,plain,
( ~ calc_date(19,11,2026,sF0)
| spl2_184 ),
inference(evaluation,[],[f10081]) ).
tff(f10086,plain,
( ~ spl2_48
| spl2_184 ),
inference(avatar_split_clause,[],[f10083,f10074,f922]) ).
tff(f10109,plain,
( $less(30,19)
| ~ spl2_47 ),
inference(resolution,[],[f920,f266]) ).
tff(f10111,plain,
( $false
| ~ spl2_47 ),
inference(evaluation,[],[f10109]) ).
tff(f10112,plain,
~ spl2_47,
inference(avatar_contradiction_clause,[],[f10111]) ).
tff(f10113,plain,
$false,
inference(avatar_smt_refutation,[],[f10112,f10086,f10077,f9900,f9889,f9878,f9867,f9856,f9523,f4935,f4878,f4776,f4682,f4666,f4661,f1795,f925,f627,f587,f539,f524]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TIM019_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.22 % Computer : n005.cluster.edu
% 0.12/0.22 % Model : x86_64 x86_64
% 0.12/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.22 % Memory : 8046.5625MB
% 0.12/0.22 % OS : Linux 6.8.0-71-generic
% 0.12/0.22 % CPULimit : 300
% 0.12/0.22 % WCLimit : 300
% 0.12/0.22 % DateTime : Mon Sep 28 18:47:32 UTC 2026
% 0.12/0.22 % CPUTime :
% 0.12/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.27 Running first-order theorem proving
% 0.12/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.61/1.62 % (1033850)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.61/1.62 % (1033902)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2961775360:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.61/1.62 % (1033903)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=122843794:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.61/1.62 % (1033897)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2283283527:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.61/1.62 % (1033898)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=683378826:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.61/1.62 % (1033899)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3758954726:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.61/1.62 % (1033896)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1423355934:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.61/1.62 % (1033902)Instruction limit reached!
% 4.61/1.62 % (1033902)------------------------------
% 4.61/1.62 % (1033902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.62 % (1033902)CaDiCaL version: 2.1.3
% 4.61/1.62 % (1033902)Termination reason: Instruction limit
% 4.61/1.62 % (1033902)Termination phase: Saturation
% 4.61/1.62 % (1033902)Time elapsed: 0.044 s
% 4.61/1.62 % (1033902)Peak memory usage: 115 MB
% 4.61/1.62 % (1033902)Instructions burned: 48 (million)
% 4.61/1.62 % (1033899)Instruction limit reached!
% 4.61/1.62 % (1033899)------------------------------
% 4.61/1.62 % (1033899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.62 % (1033899)CaDiCaL version: 2.1.3
% 4.61/1.62 % (1033899)Termination reason: Instruction limit
% 4.61/1.62 % (1033899)Termination phase: Property scanning
% 4.61/1.62 % (1033899)Time elapsed: 0.007 s
% 4.61/1.62 % (1033899)Peak memory usage: 86 MB
% 4.61/1.62 % (1033899)Instructions burned: 7 (million)
% 4.61/1.62 % (1033901)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=541794126:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.61/1.62 % (1033901)Instruction limit reached!
% 4.61/1.62 % (1033901)------------------------------
% 4.61/1.62 % (1033901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.62 % (1033901)CaDiCaL version: 2.1.3
% 4.61/1.62 % (1033901)Termination reason: Instruction limit
% 4.61/1.62 % (1033901)Termination phase: Preprocessing 3
% 4.61/1.62 % (1033901)Time elapsed: 0.003 s
% 4.61/1.62 % (1033901)Peak memory usage: 86 MB
% 4.61/1.62 % (1033901)Instructions burned: 4 (million)
% 4.61/1.62 % (1033896)Instruction limit reached!
% 4.61/1.62 % (1033896)------------------------------
% 4.61/1.62 % (1033896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.62 % (1033896)CaDiCaL version: 2.1.3
% 4.61/1.62 % (1033896)Termination reason: Instruction limit
% 4.61/1.62 % (1033896)Termination phase: Saturation
% 4.61/1.62 % (1033896)Time elapsed: 0.040 s
% 4.61/1.62 % (1033896)Peak memory usage: 115 MB
% 4.61/1.62 % (1033896)Instructions burned: 12 (million)
% 4.61/1.62 % (1033903)Instruction limit reached!
% 4.61/1.62 % (1033903)------------------------------
% 4.61/1.62 % (1033903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.62 % (1033903)CaDiCaL version: 2.1.3
% 4.61/1.62 % (1033903)Termination reason: Instruction limit
% 4.61/1.62 % (1033903)Termination phase: Saturation
% 4.61/1.62 % (1033903)Time elapsed: 0.063 s
% 4.61/1.62 % (1033903)Peak memory usage: 116 MB
% 4.61/1.62 % (1033903)Instructions burned: 33 (million)
% 4.61/1.62 % (1033898)Instruction limit reached!
% 4.61/1.62 % (1033898)------------------------------
% 4.61/1.62 % (1033898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.62 % (1033898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033898)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033898)Termination reason: Instruction limit
% 6.57/1.81 % (1033898)Termination phase: Saturation
% 6.57/1.81 % (1033898)Time elapsed: 0.124 s
% 6.57/1.81 % (1033898)Peak memory usage: 117 MB
% 6.57/1.81 % (1033898)Instructions burned: 201 (million)
% 6.57/1.81 % (1033916)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1769365043:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.57/1.81 % (1033919)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2532479922:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.57/1.81 % (1033917)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=4149533715:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.57/1.81 % (1033919)Instruction limit reached!
% 6.57/1.81 % (1033919)------------------------------
% 6.57/1.81 % (1033919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.57/1.81 % (1033919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033919)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033919)Termination reason: Instruction limit
% 6.57/1.81 % (1033919)Termination phase: Saturation
% 6.57/1.81 % (1033919)Time elapsed: 0.013 s
% 6.57/1.81 % (1033919)Peak memory usage: 88 MB
% 6.57/1.81 % (1033919)Instructions burned: 16 (million)
% 6.57/1.81 % (1033916)Instruction limit reached!
% 6.57/1.81 % (1033916)------------------------------
% 6.57/1.81 % (1033916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.57/1.81 % (1033916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033916)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033916)Termination reason: Instruction limit
% 6.57/1.81 % (1033916)Termination phase: Saturation
% 6.57/1.81 % (1033916)Time elapsed: 0.013 s
% 6.57/1.81 % (1033916)Peak memory usage: 88 MB
% 6.57/1.81 % (1033916)Instructions burned: 15 (million)
% 6.57/1.81 % (1033925)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1469620086:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.57/1.81 % (1033921)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1325273553:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.57/1.81 % (1033917)Instruction limit reached!
% 6.57/1.81 % (1033917)------------------------------
% 6.57/1.81 % (1033917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.57/1.81 % (1033917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033917)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033917)Termination reason: Instruction limit
% 6.57/1.81 % (1033917)Termination phase: Saturation
% 6.57/1.81 % (1033917)Time elapsed: 0.033 s
% 6.57/1.81 % (1033917)Peak memory usage: 89 MB
% 6.57/1.81 % (1033917)Instructions burned: 30 (million)
% 6.57/1.81 % (1033921)Instruction limit reached!
% 6.57/1.81 % (1033921)------------------------------
% 6.57/1.81 % (1033921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.57/1.81 % (1033921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033921)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033921)Termination reason: Instruction limit
% 6.57/1.81 % (1033921)Termination phase: Saturation
% 6.57/1.81 % (1033921)Time elapsed: 0.024 s
% 6.57/1.81 % (1033921)Peak memory usage: 89 MB
% 6.57/1.81 % (1033921)Instructions burned: 25 (million)
% 6.57/1.81 % (1033897)Instruction limit reached!
% 6.57/1.81 % (1033897)------------------------------
% 6.57/1.81 % (1033897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.57/1.81 % (1033897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.57/1.81 % (1033897)CaDiCaL version: 2.1.3
% 6.57/1.81 % (1033897)Termination reason: Instruction limit
% 6.57/1.81 % (1033897)Termination phase: Saturation
% 6.57/1.81 % (1033897)Time elapsed: 0.277 s
% 6.57/1.81 % (1033897)Peak memory usage: 118 MB
% 6.57/1.81 % (1033897)Instructions burned: 308 (million)
% 6.57/1.81 % (1033923)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=54250518:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 6.57/1.81 % (1033925)Instruction limit reached!
% 6.57/1.81 % (1033925)------------------------------
% 6.57/1.81 % (1033925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033925)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033925)Termination reason: Instruction limit
% 6.78/2.02 % (1033925)Termination phase: Saturation
% 6.78/2.02 % (1033925)Time elapsed: 0.039 s
% 6.78/2.02 % (1033925)Peak memory usage: 89 MB
% 6.78/2.02 % (1033925)Instructions burned: 86 (million)
% 6.78/2.02 % (1033923)Refutation not found, incomplete strategy
% 6.78/2.02 % (1033923)------------------------------
% 6.78/2.02 % (1033923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033923)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033923)Termination reason: Refutation not found, incomplete strategy
% 6.78/2.02 % (1033923)Time elapsed: 0.011 s
% 6.78/2.02 % (1033923)Peak memory usage: 89 MB
% 6.78/2.02 % (1033923)Instructions burned: 11 (million)
% 6.78/2.02 % (1033934)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1982966234:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 6.78/2.02 % (1033942)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=2816960923:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 6.78/2.02 % (1033934)Instruction limit reached!
% 6.78/2.02 % (1033934)------------------------------
% 6.78/2.02 % (1033934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033934)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033934)Termination reason: Instruction limit
% 6.78/2.02 % (1033934)Termination phase: Preprocessing 1
% 6.78/2.02 % (1033934)Time elapsed: 0.003 s
% 6.78/2.02 % (1033934)Peak memory usage: 85 MB
% 6.78/2.02 % (1033934)Instructions burned: 3 (million)
% 6.78/2.02 % (1033941)lrs+10_1_thi=all:si=on:fd=off:random_seed=3387137975:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 6.78/2.02 % (1033942)Instruction limit reached!
% 6.78/2.02 % (1033942)------------------------------
% 6.78/2.02 % (1033942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033942)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033942)Termination reason: Instruction limit
% 6.78/2.02 % (1033942)Termination phase: Property scanning
% 6.78/2.02 % (1033942)Time elapsed: 0.005 s
% 6.78/2.02 % (1033942)Peak memory usage: 87 MB
% 6.78/2.02 % (1033942)Instructions burned: 9 (million)
% 6.78/2.02 % (1033935)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=349041456:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 6.78/2.02 % (1033938)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3209168703:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 6.78/2.02 % (1033938)Instruction limit reached!
% 6.78/2.02 % (1033938)------------------------------
% 6.78/2.02 % (1033938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033938)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033938)Termination reason: Instruction limit
% 6.78/2.02 % (1033938)Termination phase: Preprocessing 3
% 6.78/2.02 % (1033938)Time elapsed: 0.004 s
% 6.78/2.02 % (1033938)Peak memory usage: 86 MB
% 6.78/2.02 % (1033938)Instructions burned: 4 (million)
% 6.78/2.02 % (1033940)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=318096153:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 6.78/2.02 % (1033941)Instruction limit reached!
% 6.78/2.02 % (1033941)------------------------------
% 6.78/2.02 % (1033941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.78/2.02 % (1033941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.78/2.02 % (1033941)CaDiCaL version: 2.1.3
% 6.78/2.02 % (1033941)Termination reason: Instruction limit
% 6.78/2.02 % (1033941)Termination phase: Saturation
% 6.78/2.02 % (1033941)Time elapsed: 0.078 s
% 6.78/2.02 % (1033941)Peak memory usage: 116 MB
% 6.78/2.02 % (1033941)Instructions burned: 54 (million)
% 6.78/2.02 % (1033940)Instruction limit reached!
% 10.42/2.42 % (1033940)------------------------------
% 10.42/2.42 % (1033940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033940)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033940)Termination reason: Instruction limit
% 10.42/2.42 % (1033940)Termination phase: Saturation
% 10.42/2.42 % (1033940)Time elapsed: 0.073 s
% 10.42/2.42 % (1033940)Peak memory usage: 134 MB
% 10.42/2.42 % (1033940)Instructions burned: 67 (million)
% 10.42/2.42 % (1033956)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1827737607:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.42/2.42 % (1033935)Instruction limit reached!
% 10.42/2.42 % (1033935)------------------------------
% 10.42/2.42 % (1033935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033935)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033935)Termination reason: Instruction limit
% 10.42/2.42 % (1033935)Termination phase: Saturation
% 10.42/2.42 % (1033935)Time elapsed: 0.177 s
% 10.42/2.42 % (1033935)Peak memory usage: 91 MB
% 10.42/2.42 % (1033935)Instructions burned: 181 (million)
% 10.42/2.42 % (1033952)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3563592418:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.42/2.42 % (1033952)Instruction limit reached!
% 10.42/2.42 % (1033952)------------------------------
% 10.42/2.42 % (1033952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033952)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033952)Termination reason: Instruction limit
% 10.42/2.42 % (1033952)Termination phase: Property scanning
% 10.42/2.42 % (1033952)Time elapsed: 0.002 s
% 10.42/2.42 % (1033952)Peak memory usage: 85 MB
% 10.42/2.42 % (1033952)Instructions burned: 2 (million)
% 10.42/2.42 % (1033951)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4015024545:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 10.42/2.42 % (1033951)Instruction limit reached!
% 10.42/2.42 % (1033951)------------------------------
% 10.42/2.42 % (1033951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033951)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033951)Termination reason: Instruction limit
% 10.42/2.42 % (1033951)Termination phase: Preprocessing 2
% 10.42/2.42 % (1033951)Time elapsed: 0.003 s
% 10.42/2.42 % (1033951)Peak memory usage: 85 MB
% 10.42/2.42 % (1033951)Instructions burned: 3 (million)
% 10.42/2.42 % (1033923)------------------------------
% 10.42/2.42 % (1033923)------------------------------
% 10.42/2.42 % (1033956)Instruction limit reached!
% 10.42/2.42 % (1033956)------------------------------
% 10.42/2.42 % (1033956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033956)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033956)Termination reason: Instruction limit
% 10.42/2.42 % (1033956)Termination phase: Saturation
% 10.42/2.42 % (1033956)Time elapsed: 0.088 s
% 10.42/2.42 % (1033956)Peak memory usage: 117 MB
% 10.42/2.42 % (1033956)Instructions burned: 127 (million)
% 10.42/2.42 % (1033961)dis+10_1_si=on:random_seed=1708141101:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.42/2.42 % (1033963)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=142688249:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.42/2.42 % (1033961)Instruction limit reached!
% 10.42/2.42 % (1033961)------------------------------
% 10.42/2.42 % (1033961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.42 % (1033961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.42 % (1033961)CaDiCaL version: 2.1.3
% 10.42/2.42 % (1033961)Termination reason: Instruction limit
% 10.42/2.42 % (1033961)Termination phase: Saturation
% 10.42/2.42 % (1033961)Time elapsed: 0.010 s
% 10.42/2.42 % (1033961)Peak memory usage: 88 MB
% 10.42/2.42 % (1033961)Instructions burned: 10 (million)
% 10.42/2.42 % (1033963)Refutation not found, incomplete strategy
% 10.42/2.42 % (1033963)------------------------------
% 10.42/2.42 % (1033963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033963)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033963)Termination reason: Refutation not found, incomplete strategy
% 11.79/2.70 % (1033963)Time elapsed: 0.013 s
% 11.79/2.70 % (1033963)Peak memory usage: 88 MB
% 11.79/2.70 % (1033963)Instructions burned: 11 (million)
% 11.79/2.70 % (1033970)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3108025296:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 11.79/2.70 % (1033965)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3028519449: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)
% 11.79/2.70 % (1033970)Refutation not found, incomplete strategy
% 11.79/2.70 % (1033970)------------------------------
% 11.79/2.70 % (1033970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033970)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033970)Termination reason: Refutation not found, incomplete strategy
% 11.79/2.70 % (1033970)Time elapsed: 0.007 s
% 11.79/2.70 % (1033970)Peak memory usage: 88 MB
% 11.79/2.70 % (1033970)Instructions burned: 10 (million)
% 11.79/2.70 % (1033968)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3226905744:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 11.79/2.70 % (1033968)Instruction limit reached!
% 11.79/2.70 % (1033968)------------------------------
% 11.79/2.70 % (1033968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033968)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033968)Termination reason: Instruction limit
% 11.79/2.70 % (1033968)Termination phase: Preprocessing 1
% 11.79/2.70 % (1033968)Time elapsed: 0.003 s
% 11.79/2.70 % (1033968)Peak memory usage: 85 MB
% 11.79/2.70 % (1033968)Instructions burned: 3 (million)
% 11.79/2.70 % (1033973)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2087585179:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 11.79/2.70 % (1033969)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=91355783:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 11.79/2.70 % (1033965)Instruction limit reached!
% 11.79/2.70 % (1033965)------------------------------
% 11.79/2.70 % (1033965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033965)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033965)Termination reason: Instruction limit
% 11.79/2.70 % (1033965)Termination phase: Saturation
% 11.79/2.70 % (1033965)Time elapsed: 0.044 s
% 11.79/2.70 % (1033965)Peak memory usage: 89 MB
% 11.79/2.70 % (1033965)Instructions burned: 35 (million)
% 11.79/2.70 % (1033969)Instruction limit reached!
% 11.79/2.70 % (1033969)------------------------------
% 11.79/2.70 % (1033969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033969)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033969)Termination reason: Instruction limit
% 11.79/2.70 % (1033969)Termination phase: Saturation
% 11.79/2.70 % (1033969)Time elapsed: 0.007 s
% 11.79/2.70 % (1033969)Peak memory usage: 87 MB
% 11.79/2.70 % (1033969)Instructions burned: 8 (million)
% 11.79/2.70 % (1033973)Instruction limit reached!
% 11.79/2.70 % (1033973)------------------------------
% 11.79/2.70 % (1033973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.79/2.70 % (1033973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.79/2.70 % (1033973)CaDiCaL version: 2.1.3
% 11.79/2.70 % (1033973)Termination reason: Instruction limit
% 11.79/2.70 % (1033973)Termination phase: Saturation
% 11.79/2.70 % (1033973)Time elapsed: 0.021 s
% 11.79/2.70 % (1033973)Peak memory usage: 111 MB
% 11.79/2.70 % (1033973)Instructions burned: 14 (million)
% 11.79/2.70 % (1033977)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3787561272:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 16.22/3.15 % (1033977)Refutation not found, incomplete strategy
% 16.22/3.15 % (1033977)------------------------------
% 16.22/3.15 % (1033977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.22/3.15 % (1033977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/3.15 % (1033977)CaDiCaL version: 2.1.3
% 16.22/3.15 % (1033977)Termination reason: Refutation not found, incomplete strategy
% 16.22/3.15 % (1033977)Time elapsed: 0.046 s
% 16.22/3.15 % (1033977)Peak memory usage: 115 MB
% 16.22/3.15 % (1033977)Instructions burned: 11 (million)
% 16.22/3.15 % (1033991)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=4035316407:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi)
% 16.22/3.15 % (1033989)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1300917771:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 16.22/3.15 % (1033990)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=4027539248:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 16.22/3.15 % (1033987)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2122054360:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 16.22/3.15 % (1033987)Instruction limit reached!
% 16.22/3.15 % (1033987)------------------------------
% 16.22/3.15 % (1033987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.22/3.15 % (1033987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/3.15 % (1033987)CaDiCaL version: 2.1.3
% 16.22/3.15 % (1033987)Termination reason: Instruction limit
% 16.22/3.15 % (1033987)Termination phase: Saturation
% 16.22/3.15 % (1033987)Time elapsed: 0.011 s
% 16.22/3.15 % (1033987)Peak memory usage: 88 MB
% 16.22/3.15 % (1033987)Instructions burned: 10 (million)
% 16.22/3.15 % (1033963)------------------------------
% 16.22/3.15 % (1033963)------------------------------
% 16.22/3.15 % (1033990)Instruction limit reached!
% 16.22/3.15 % (1033990)------------------------------
% 16.22/3.15 % (1033990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.22/3.15 % (1033990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/3.15 % (1033990)CaDiCaL version: 2.1.3
% 16.22/3.15 % (1033990)Termination reason: Instruction limit
% 16.22/3.15 % (1033990)Termination phase: Saturation
% 16.22/3.15 % (1033990)Time elapsed: 0.074 s
% 16.22/3.15 % (1033990)Peak memory usage: 90 MB
% 16.22/3.15 % (1033990)Instructions burned: 75 (million)
% 16.22/3.15 % (1033991)Instruction limit reached!
% 16.22/3.15 % (1033991)------------------------------
% 16.22/3.15 % (1033991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.22/3.15 % (1033989)Instruction limit reached!
% 16.22/3.15 % (1033989)------------------------------
% 16.22/3.15 % (1033989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.22/3.15 % (1033989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/3.15 % (1033989)CaDiCaL version: 2.1.3
% 16.22/3.15 % (1033991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.22/3.15 % (1033989)Termination reason: Instruction limit
% 16.22/3.16 % (1033989)Termination phase: Saturation
% 16.22/3.16 % (1033989)Time elapsed: 0.121 s
% 16.22/3.16 % (1033991)CaDiCaL version: 2.1.3
% 16.22/3.16 % (1033989)Peak memory usage: 133 MB
% 16.22/3.16 % (1033989)Instructions burned: 71 (million)
% 16.22/3.16 % (1033991)Termination reason: Instruction limit
% 16.22/3.16 % (1033991)Termination phase: Saturation
% 16.22/3.16 % (1033991)Time elapsed: 0.148 s
% 16.22/3.16 % (1033991)Peak memory usage: 90 MB
% 16.22/3.16 % (1033991)Instructions burned: 297 (million)
% 16.22/3.16 % (1033970)------------------------------
% 16.22/3.16 % (1033970)------------------------------
% 16.22/3.16 % (1034001)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=333397025:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 16.22/3.16 % (1034006)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3003394290:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi)
% 16.22/3.16 % (1034004)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2184199018:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 16.22/3.16 % (1034006)Instruction limit reached!
% 17.77/3.64 % (1034006)------------------------------
% 17.77/3.64 % (1034006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034006)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034006)Termination reason: Instruction limit
% 17.77/3.64 % (1034006)Termination phase: Saturation
% 17.77/3.64 % (1034006)Time elapsed: 0.058 s
% 17.77/3.64 % (1034006)Peak memory usage: 134 MB
% 17.77/3.64 % (1034006)Instructions burned: 41 (million)
% 17.77/3.64 % (1034008)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=923493665:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi)
% 17.77/3.64 % (1033977)------------------------------
% 17.77/3.64 % (1033977)------------------------------
% 17.77/3.64 % (1034008)Refutation not found, incomplete strategy
% 17.77/3.64 % (1034008)------------------------------
% 17.77/3.64 % (1034008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034008)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034008)Termination reason: Refutation not found, incomplete strategy
% 17.77/3.64 % (1034008)Time elapsed: 0.015 s
% 17.77/3.64 % (1034008)Peak memory usage: 89 MB
% 17.77/3.64 % (1034008)Instructions burned: 13 (million)
% 17.77/3.64 % (1034011)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=95027388:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 17.77/3.64 % (1034010)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2696876579:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi)
% 17.77/3.64 % (1034001)Instruction limit reached!
% 17.77/3.64 % (1034001)------------------------------
% 17.77/3.64 % (1034001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034001)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034001)Termination reason: Instruction limit
% 17.77/3.64 % (1034001)Termination phase: Saturation
% 17.77/3.64 % (1034001)Time elapsed: 0.133 s
% 17.77/3.64 % (1034001)Peak memory usage: 117 MB
% 17.77/3.64 % (1034001)Instructions burned: 130 (million)
% 17.77/3.64 % (1034020)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=3031293955:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi)
% 17.77/3.64 % (1034004)Instruction limit reached!
% 17.77/3.64 % (1034004)------------------------------
% 17.77/3.64 % (1034004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034004)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034004)Termination reason: Instruction limit
% 17.77/3.64 % (1034004)Termination phase: Saturation
% 17.77/3.64 % (1034004)Time elapsed: 0.201 s
% 17.77/3.64 % (1034004)Peak memory usage: 133 MB
% 17.77/3.64 % (1034004)Instructions burned: 131 (million)
% 17.77/3.64 % (1034011)Instruction limit reached!
% 17.77/3.64 % (1034011)------------------------------
% 17.77/3.64 % (1034011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034011)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034011)Termination reason: Instruction limit
% 17.77/3.64 % (1034011)Termination phase: Saturation
% 17.77/3.64 % (1034011)Time elapsed: 0.163 s
% 17.77/3.64 % (1034011)Peak memory usage: 118 MB
% 17.77/3.64 % (1034011)Instructions burned: 131 (million)
% 17.77/3.64 % (1034023)dis+10_1_si=on:random_seed=2189419997:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi)
% 17.77/3.64 % (1034026)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=721811210:i=383:fsr=off:rtra=on:ev=force_2983 on theBenchmark for (2983ds/383Mi)
% 17.77/3.64 % (1034020)Instruction limit reached!
% 17.77/3.64 % (1034020)------------------------------
% 17.77/3.64 % (1034020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/3.64 % (1034020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/3.64 % (1034020)CaDiCaL version: 2.1.3
% 17.77/3.64 % (1034020)Termination reason: Instruction limit
% 17.77/3.64 % (1034020)Termination phase: Saturation
% 20.23/3.92 % (1034020)Time elapsed: 0.121 s
% 20.23/3.92 % (1034020)Peak memory usage: 116 MB
% 20.23/3.92 % (1034020)Instructions burned: 262 (million)
% 20.23/3.92 % (1034028)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=21885828:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 20.23/3.92 % (1034008)------------------------------
% 20.23/3.92 % (1034008)------------------------------
% 20.23/3.92 % (1034030)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=418992361:i=65:nm=16:rtra=on_2982 on theBenchmark for (2982ds/65Mi)
% 20.23/3.92 % (1034034)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4219460114:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi)
% 20.23/3.92 % (1034030)Refutation not found, incomplete strategy
% 20.23/3.92 % (1034030)------------------------------
% 20.23/3.92 % (1034030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/3.92 % (1034030)CaDiCaL version: 2.1.3
% 20.23/3.92 % (1034030)Termination reason: Refutation not found, incomplete strategy
% 20.23/3.92 % (1034030)Time elapsed: 0.048 s
% 20.23/3.92 % (1034030)Peak memory usage: 115 MB
% 20.23/3.92 % (1034030)Instructions burned: 16 (million)
% 20.23/3.92 % (1034034)Instruction limit reached!
% 20.23/3.92 % (1034034)------------------------------
% 20.23/3.92 % (1034034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/3.92 % (1034034)CaDiCaL version: 2.1.3
% 20.23/3.92 % (1034034)Termination reason: Instruction limit
% 20.23/3.92 % (1034034)Termination phase: Saturation
% 20.23/3.92 % (1034034)Time elapsed: 0.051 s
% 20.23/3.92 % (1034034)Peak memory usage: 89 MB
% 20.23/3.92 % (1034034)Instructions burned: 123 (million)
% 20.23/3.92 % (1034028)Instruction limit reached!
% 20.23/3.92 % (1034028)------------------------------
% 20.23/3.92 % (1034028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/3.92 % (1034028)CaDiCaL version: 2.1.3
% 20.23/3.92 % (1034028)Termination reason: Instruction limit
% 20.23/3.92 % (1034028)Termination phase: Saturation
% 20.23/3.92 % (1034028)Time elapsed: 0.135 s
% 20.23/3.92 % (1034028)Peak memory usage: 90 MB
% 20.23/3.92 % (1034028)Instructions burned: 141 (million)
% 20.23/3.92 % (1034041)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=4232586719:s2a=on:i=128:s2at=5:ins=3:rtra=on_2980 on theBenchmark for (2980ds/128Mi)
% 20.23/3.92 % (1034026)Instruction limit reached!
% 20.23/3.92 % (1034026)------------------------------
% 20.23/3.92 % (1034026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/3.92 % (1034026)CaDiCaL version: 2.1.3
% 20.23/3.92 % (1034026)Termination reason: Instruction limit
% 20.23/3.92 % (1034026)Termination phase: Saturation
% 20.23/3.92 % (1034026)Time elapsed: 0.344 s
% 20.23/3.92 % (1034026)Peak memory usage: 95 MB
% 20.23/3.92 % (1034026)Instructions burned: 384 (million)
% 20.23/3.92 % (1034049)dis+1010_1_to=kbo:si=on:random_seed=2163160874:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/175Mi)
% 20.23/3.92 % (1034047)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=3648346703:i=39:ins=3:rtra=on_2979 on theBenchmark for (2979ds/39Mi)
% 20.23/3.92 % (1034041)Instruction limit reached!
% 20.23/3.92 % (1034041)------------------------------
% 20.23/3.92 % (1034041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.23/3.92 % (1034041)CaDiCaL version: 2.1.3
% 20.23/3.92 % (1034041)Termination reason: Instruction limit
% 20.23/3.92 % (1034041)Termination phase: Saturation
% 20.23/3.92 % (1034041)Time elapsed: 0.150 s
% 20.23/3.92 % (1034041)Peak memory usage: 116 MB
% 20.23/3.92 % (1034041)Instructions burned: 128 (million)
% 20.23/3.92 % (1034010)Instruction limit reached!
% 20.23/3.92 % (1034010)------------------------------
% 20.23/3.92 % (1034010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.23/3.92 % (1034010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034010)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034010)Termination reason: Instruction limit
% 24.02/4.40 % (1034010)Termination phase: Saturation
% 24.02/4.40 % (1034010)Time elapsed: 0.693 s
% 24.02/4.40 % (1034010)Peak memory usage: 139 MB
% 24.02/4.40 % (1034010)Instructions burned: 598 (million)
% 24.02/4.40 % (1034049)Instruction limit reached!
% 24.02/4.40 % (1034049)------------------------------
% 24.02/4.40 % (1034049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.40 % (1034049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034049)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034049)Termination reason: Instruction limit
% 24.02/4.40 % (1034049)Termination phase: Saturation
% 24.02/4.40 % (1034049)Time elapsed: 0.083 s
% 24.02/4.40 % (1034049)Peak memory usage: 92 MB
% 24.02/4.40 % (1034049)Instructions burned: 176 (million)
% 24.02/4.40 % (1034047)Instruction limit reached!
% 24.02/4.40 % (1034047)------------------------------
% 24.02/4.40 % (1034047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.40 % (1034047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034047)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034047)Termination reason: Instruction limit
% 24.02/4.40 % (1034047)Termination phase: Saturation
% 24.02/4.40 % (1034047)Time elapsed: 0.071 s
% 24.02/4.40 % (1034047)Peak memory usage: 116 MB
% 24.02/4.40 % (1034047)Instructions burned: 40 (million)
% 24.02/4.40 % (1034051)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=794329436:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi)
% 24.02/4.40 % (1034030)------------------------------
% 24.02/4.40 % (1034030)------------------------------
% 24.02/4.40 % (1034061)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3673335136:i=349:rtra=on_2976 on theBenchmark for (2976ds/349Mi)
% 24.02/4.40 % (1034061)Refutation not found, incomplete strategy
% 24.02/4.40 % (1034061)------------------------------
% 24.02/4.40 % (1034061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.40 % (1034061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034061)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034061)Termination reason: Refutation not found, incomplete strategy
% 24.02/4.40 % (1034061)Time elapsed: 0.032 s
% 24.02/4.40 % (1034061)Peak memory usage: 116 MB
% 24.02/4.40 % (1034061)Instructions burned: 28 (million)
% 24.02/4.40 % (1034058)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2669309012:s2a=on:i=483:doe=on:nm=32:rtra=on_2977 on theBenchmark for (2977ds/483Mi)
% 24.02/4.40 % (1034059)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4176699909:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi)
% 24.02/4.40 % (1034062)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3058235940:st=2:i=295:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/295Mi)
% 24.02/4.40 % (1034066)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3475315075:i=328:kws=inv_frequency:nm=20:rtra=on_2975 on theBenchmark for (2975ds/328Mi)
% 24.02/4.40 % (1034061)------------------------------
% 24.02/4.40 % (1034061)------------------------------
% 24.02/4.40 % (1034023)Instruction limit reached!
% 24.02/4.40 % (1034023)------------------------------
% 24.02/4.40 % (1034023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.40 % (1034023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034023)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034023)Termination reason: Instruction limit
% 24.02/4.40 % (1034023)Termination phase: Saturation
% 24.02/4.40 % (1034023)Time elapsed: 0.919 s
% 24.02/4.40 % (1034023)Peak memory usage: 94 MB
% 24.02/4.40 % (1034023)Instructions burned: 1001 (million)
% 24.02/4.40 % (1034051)Instruction limit reached!
% 24.02/4.40 % (1034051)------------------------------
% 24.02/4.40 % (1034051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.02/4.40 % (1034051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.02/4.40 % (1034051)CaDiCaL version: 2.1.3
% 24.02/4.40 % (1034051)Termination reason: Instruction limit
% 24.02/4.40 % (1034051)Termination phase: Saturation
% 24.02/4.40 % (1034051)Time elapsed: 0.383 s
% 24.02/4.40 % (1034051)Peak memory usage: 118 MB
% 25.97/4.72 % (1034051)Instructions burned: 329 (million)
% 25.97/4.72 % (1034059)Instruction limit reached!
% 25.97/4.72 % (1034059)------------------------------
% 25.97/4.72 % (1034059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034059)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034059)Termination reason: Instruction limit
% 25.97/4.72 % (1034059)Termination phase: Saturation
% 25.97/4.72 % (1034059)Time elapsed: 0.275 s
% 25.97/4.72 % (1034059)Peak memory usage: 136 MB
% 25.97/4.72 % (1034059)Instructions burned: 215 (million)
% 25.97/4.72 % (1034062)Instruction limit reached!
% 25.97/4.72 % (1034062)------------------------------
% 25.97/4.72 % (1034062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034062)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034062)Termination reason: Instruction limit
% 25.97/4.72 % (1034062)Termination phase: Saturation
% 25.97/4.72 % (1034062)Time elapsed: 0.270 s
% 25.97/4.72 % (1034062)Peak memory usage: 91 MB
% 25.97/4.72 % (1034062)Instructions burned: 295 (million)
% 25.97/4.72 % (1034079)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=208116119:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 25.97/4.72 % (1034081)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3712861527:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2972 on theBenchmark for (2972ds/484Mi)
% 25.97/4.72 % (1034081)Refutation not found, incomplete strategy
% 25.97/4.72 % (1034081)------------------------------
% 25.97/4.72 % (1034081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034081)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034081)Termination reason: Refutation not found, incomplete strategy
% 25.97/4.72 % (1034081)Time elapsed: 0.007 s
% 25.97/4.72 % (1034081)Peak memory usage: 89 MB
% 25.97/4.72 % (1034081)Instructions burned: 5 (million)
% 25.97/4.72 % (1034082)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=639398826:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2972 on theBenchmark for (2972ds/321Mi)
% 25.97/4.72 % (1034066)Instruction limit reached!
% 25.97/4.72 % (1034066)------------------------------
% 25.97/4.72 % (1034066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034066)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034066)Termination reason: Instruction limit
% 25.97/4.72 % (1034066)Termination phase: Saturation
% 25.97/4.72 % (1034066)Time elapsed: 0.330 s
% 25.97/4.72 % (1034066)Peak memory usage: 119 MB
% 25.97/4.72 % (1034066)Instructions burned: 328 (million)
% 25.97/4.72 % (1034079)Instruction limit reached!
% 25.97/4.72 % (1034079)------------------------------
% 25.97/4.72 % (1034079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034079)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034079)Termination reason: Instruction limit
% 25.97/4.72 % (1034079)Termination phase: Saturation
% 25.97/4.72 % (1034079)Time elapsed: 0.155 s
% 25.97/4.72 % (1034079)Peak memory usage: 117 MB
% 25.97/4.72 % (1034079)Instructions burned: 283 (million)
% 25.97/4.72 % (1034083)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3500540985:i=416:rtra=on:gtg=position:ss=axioms_2971 on theBenchmark for (2971ds/416Mi)
% 25.97/4.72 % (1034058)Instruction limit reached!
% 25.97/4.72 % (1034058)------------------------------
% 25.97/4.72 % (1034058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.97/4.72 % (1034058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.97/4.72 % (1034058)CaDiCaL version: 2.1.3
% 25.97/4.72 % (1034058)Termination reason: Instruction limit
% 25.97/4.72 % (1034058)Termination phase: Saturation
% 25.97/4.72 % (1034058)Time elapsed: 0.544 s
% 25.97/4.72 % (1034058)Peak memory usage: 137 MB
% 25.97/4.72 % (1034058)Instructions burned: 483 (million)
% 25.97/4.72 % (1034084)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1644153139:i=471:thf=on:kws=precedence:rtra=on_2971 on theBenchmark for (2971ds/471Mi)
% 25.97/4.72 % (1034083)Refutation not found, incomplete strategy
% 25.97/4.72 % (1034083)------------------------------
% 27.98/4.92 % (1034083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.92 % (1034083)CaDiCaL version: 2.1.3
% 27.98/4.92 % (1034083)Termination reason: Refutation not found, incomplete strategy
% 27.98/4.92 % (1034083)Time elapsed: 0.044 s
% 27.98/4.92 % (1034083)Peak memory usage: 115 MB
% 27.98/4.92 % (1034083)Instructions burned: 10 (million)
% 27.98/4.92 % (1034093)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=1517061379:avsq=on:i=276:avsqr=1,2:rtra=on_2970 on theBenchmark for (2970ds/276Mi)
% 27.98/4.92 % (1034094)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1911386617:i=375:kws=inv_arity_squared:rtra=on_2969 on theBenchmark for (2969ds/375Mi)
% 27.98/4.92 % (1034082)Instruction limit reached!
% 27.98/4.92 % (1034082)------------------------------
% 27.98/4.92 % (1034082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.92 % (1034082)CaDiCaL version: 2.1.3
% 27.98/4.92 % (1034082)Termination reason: Instruction limit
% 27.98/4.92 % (1034082)Termination phase: Saturation
% 27.98/4.92 % (1034082)Time elapsed: 0.293 s
% 27.98/4.92 % (1034082)Peak memory usage: 114 MB
% 27.98/4.92 % (1034082)Instructions burned: 321 (million)
% 27.98/4.92 % (1034096)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1180036783:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/387Mi)
% 27.98/4.92 % (1034081)------------------------------
% 27.98/4.92 % (1034081)------------------------------
% 27.98/4.92 % (1034094)Instruction limit reached!
% 27.98/4.92 % (1034094)------------------------------
% 27.98/4.92 % (1034094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.92 % (1034094)CaDiCaL version: 2.1.3
% 27.98/4.92 % (1034094)Termination reason: Instruction limit
% 27.98/4.92 % (1034094)Termination phase: Saturation
% 27.98/4.92 % (1034094)Time elapsed: 0.197 s
% 27.98/4.92 % (1034094)Peak memory usage: 120 MB
% 27.98/4.92 % (1034094)Instructions burned: 376 (million)
% 27.98/4.92 % (1034083)------------------------------
% 27.98/4.92 % (1034083)------------------------------
% 27.98/4.92 % (1034093)Instruction limit reached!
% 27.98/4.92 % (1034093)------------------------------
% 27.98/4.92 % (1034093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.92 % (1034093)CaDiCaL version: 2.1.3
% 27.98/4.92 % (1034093)Termination reason: Instruction limit
% 27.98/4.92 % (1034093)Termination phase: Saturation
% 27.98/4.92 % (1034093)Time elapsed: 0.319 s
% 27.98/4.92 % (1034093)Peak memory usage: 134 MB
% 27.98/4.92 % (1034093)Instructions burned: 276 (million)
% 27.98/4.92 % (1034084)Instruction limit reached!
% 27.98/4.92 % (1034084)------------------------------
% 27.98/4.92 % (1034084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.92 % (1034084)CaDiCaL version: 2.1.3
% 27.98/4.92 % (1034084)Termination reason: Instruction limit
% 27.98/4.92 % (1034084)Termination phase: Saturation
% 27.98/4.92 % (1034084)Time elapsed: 0.405 s
% 27.98/4.92 % (1034084)Peak memory usage: 118 MB
% 27.98/4.92 % (1034084)Instructions burned: 471 (million)
% 27.98/4.92 % (1034104)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3648853678:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2967 on theBenchmark for (2967ds/513Mi)
% 27.98/4.92 % (1034112)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2105401646:i=359:rtra=on:gtg=exists_top:ss=axioms_2966 on theBenchmark for (2966ds/359Mi)
% 27.98/4.92 % (1034110)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2816869282:i=334:rtra=on_2966 on theBenchmark for (2966ds/334Mi)
% 27.98/4.92 % (1034112)Refutation not found, incomplete strategy
% 27.98/4.92 % (1034112)------------------------------
% 27.98/4.92 % (1034112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.98/4.92 % (1034112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034112)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034112)Termination reason: Refutation not found, incomplete strategy
% 31.96/5.42 % (1034112)Time elapsed: 0.004 s
% 31.96/5.42 % (1034112)Peak memory usage: 89 MB
% 31.96/5.42 % (1034112)Instructions burned: 6 (million)
% 31.96/5.42 % (1034113)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=822434162:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2965 on theBenchmark for (2965ds/341Mi)
% 31.96/5.42 % (1034114)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=254085627:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/261Mi)
% 31.96/5.42 % (1034096)Instruction limit reached!
% 31.96/5.42 % (1034096)------------------------------
% 31.96/5.42 % (1034096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.96/5.42 % (1034096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034096)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034096)Termination reason: Instruction limit
% 31.96/5.42 % (1034096)Termination phase: Saturation
% 31.96/5.42 % (1034096)Time elapsed: 0.357 s
% 31.96/5.42 % (1034096)Peak memory usage: 118 MB
% 31.96/5.42 % (1034096)Instructions burned: 387 (million)
% 31.96/5.42 % (1034114)Refutation not found, incomplete strategy
% 31.96/5.42 % (1034114)------------------------------
% 31.96/5.42 % (1034114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.96/5.42 % (1034114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034114)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034114)Termination reason: Refutation not found, incomplete strategy
% 31.96/5.42 % (1034114)Time elapsed: 0.047 s
% 31.96/5.42 % (1034114)Peak memory usage: 116 MB
% 31.96/5.42 % (1034114)Instructions burned: 10 (million)
% 31.96/5.42 % (1034118)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=3764837936:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2965 on theBenchmark for (2965ds/235Mi)
% 31.96/5.42 % (1034112)------------------------------
% 31.96/5.42 % (1034112)------------------------------
% 31.96/5.42 % (1034126)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1744458186:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2963 on theBenchmark for (2963ds/273Mi)
% 31.96/5.42 % (1034128)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1831486596:i=146:doe=on:rtra=on_2962 on theBenchmark for (2962ds/146Mi)
% 31.96/5.42 % (1034118)Instruction limit reached!
% 31.96/5.42 % (1034118)------------------------------
% 31.96/5.42 % (1034118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.96/5.42 % (1034118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034118)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034118)Termination reason: Instruction limit
% 31.96/5.42 % (1034118)Termination phase: Saturation
% 31.96/5.42 % (1034118)Time elapsed: 0.153 s
% 31.96/5.42 % (1034118)Peak memory usage: 116 MB
% 31.96/5.42 % (1034118)Instructions burned: 235 (million)
% 31.96/5.42 % (1034110)Instruction limit reached!
% 31.96/5.42 % (1034110)------------------------------
% 31.96/5.42 % (1034110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.96/5.42 % (1034110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034110)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034110)Termination reason: Instruction limit
% 31.96/5.42 % (1034110)Termination phase: Saturation
% 31.96/5.42 % (1034110)Time elapsed: 0.291 s
% 31.96/5.42 % (1034110)Peak memory usage: 135 MB
% 31.96/5.42 % (1034110)Instructions burned: 334 (million)
% 31.96/5.42 % (1034113)Instruction limit reached!
% 31.96/5.42 % (1034113)------------------------------
% 31.96/5.42 % (1034113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.96/5.42 % (1034113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.96/5.42 % (1034113)CaDiCaL version: 2.1.3
% 31.96/5.42 % (1034113)Termination reason: Instruction limit
% 31.96/5.42 % (1034113)Termination phase: Saturation
% 31.96/5.42 % (1034113)Time elapsed: 0.254 s
% 31.96/5.42 % (1034113)Peak memory usage: 120 MB
% 31.96/5.42 % (1034113)Instructions burned: 346 (million)
% 31.96/5.42 % (1034128)Instruction limit reached!
% 31.96/5.42 % (1034128)------------------------------
% 31.96/5.42 % (1034128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034128)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034128)Termination reason: Instruction limit
% 34.01/5.85 % (1034128)Termination phase: Saturation
% 34.01/5.85 % (1034128)Time elapsed: 0.052 s
% 34.01/5.85 % (1034128)Peak memory usage: 90 MB
% 34.01/5.85 % (1034128)Instructions burned: 148 (million)
% 34.01/5.85 % (1034104)Instruction limit reached!
% 34.01/5.85 % (1034104)------------------------------
% 34.01/5.85 % (1034104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034104)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034104)Termination reason: Instruction limit
% 34.01/5.85 % (1034104)Termination phase: Saturation
% 34.01/5.85 % (1034104)Time elapsed: 0.416 s
% 34.01/5.85 % (1034104)Peak memory usage: 94 MB
% 34.01/5.85 % (1034104)Instructions burned: 514 (million)
% 34.01/5.85 % (1034114)------------------------------
% 34.01/5.85 % (1034114)------------------------------
% 34.01/5.85 % (1034134)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=795854365:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2961 on theBenchmark for (2961ds/655Mi)
% 34.01/5.85 % (1034134)Refutation not found, incomplete strategy
% 34.01/5.85 % (1034134)------------------------------
% 34.01/5.85 % (1034134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034134)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034134)Termination reason: Refutation not found, incomplete strategy
% 34.01/5.85 % (1034134)Time elapsed: 0.007 s
% 34.01/5.85 % (1034134)Peak memory usage: 89 MB
% 34.01/5.85 % (1034134)Instructions burned: 19 (million)
% 34.01/5.85 % (1034126)Instruction limit reached!
% 34.01/5.85 % (1034126)------------------------------
% 34.01/5.85 % (1034126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034126)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034126)Termination reason: Instruction limit
% 34.01/5.85 % (1034126)Termination phase: Saturation
% 34.01/5.85 % (1034126)Time elapsed: 0.186 s
% 34.01/5.85 % (1034126)Peak memory usage: 92 MB
% 34.01/5.85 % (1034126)Instructions burned: 274 (million)
% 34.01/5.85 % (1034131)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=929870860:i=4428:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/4428Mi)
% 34.01/5.85 % (1034132)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=3555930922:avsq=on:i=276:avsqr=1,2:rtra=on_2961 on theBenchmark for (2961ds/276Mi)
% 34.01/5.85 % (1034133)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=578532079:i=1052:rtra=on_2961 on theBenchmark for (2961ds/1052Mi)
% 34.01/5.85 % (1034135)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1907308711:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2961 on theBenchmark for (2961ds/1054Mi)
% 34.01/5.85 % (1034137)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3882377682:i=107:rtra=on_2961 on theBenchmark for (2961ds/107Mi)
% 34.01/5.85 % (1034135)Refutation not found, incomplete strategy
% 34.01/5.85 % (1034135)------------------------------
% 34.01/5.85 % (1034135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034135)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034135)Termination reason: Refutation not found, incomplete strategy
% 34.01/5.85 % (1034135)Time elapsed: 0.018 s
% 34.01/5.85 % (1034135)Peak memory usage: 89 MB
% 34.01/5.85 % (1034135)Instructions burned: 26 (million)
% 34.01/5.85 % (1034137)Refutation not found, incomplete strategy
% 34.01/5.85 % (1034137)------------------------------
% 34.01/5.85 % (1034137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.01/5.85 % (1034137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.01/5.85 % (1034137)CaDiCaL version: 2.1.3
% 34.01/5.85 % (1034137)Termination reason: Refutation not found, incomplete strategy
% 34.01/5.85 % (1034137)Time elapsed: 0.034 s
% 38.13/6.24 % (1034137)Peak memory usage: 115 MB
% 38.13/6.24 % (1034137)Instructions burned: 17 (million)
% 38.13/6.24 % (1034141)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=446511985:s2a=on:i=450:doe=on:nm=32:rtra=on_2960 on theBenchmark for (2960ds/450Mi)
% 38.13/6.24 % (1034134)------------------------------
% 38.13/6.24 % (1034134)------------------------------
% 38.13/6.24 % (1034150)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
% 38.13/6.24 % (1034150)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=438841528:i=1090:aac=none:nm=0:rtra=on:rawr=on_2958 on theBenchmark for (2958ds/1090Mi)
% 38.13/6.24 % (1034132)Instruction limit reached!
% 38.13/6.24 % (1034132)------------------------------
% 38.13/6.24 % (1034132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.13/6.24 % (1034132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.13/6.24 % (1034132)CaDiCaL version: 2.1.3
% 38.13/6.24 % (1034132)Termination reason: Instruction limit
% 38.13/6.24 % (1034132)Termination phase: Saturation
% 38.13/6.24 % (1034132)Time elapsed: 0.246 s
% 38.13/6.24 % (1034132)Peak memory usage: 134 MB
% 38.13/6.24 % (1034132)Instructions burned: 277 (million)
% 38.13/6.24 % (1034135)------------------------------
% 38.13/6.24 % (1034135)------------------------------
% 38.13/6.24 % (1034137)------------------------------
% 38.13/6.24 % (1034137)------------------------------
% 38.13/6.24 % (1034189)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4063447042:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2957 on theBenchmark for (2957ds/130Mi)
% 38.13/6.24 % (1034221)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2141432549:i=312:kws=inv_frequency:nm=20:rtra=on_2957 on theBenchmark for (2957ds/312Mi)
% 38.13/6.24 % (1034141)Instruction limit reached!
% 38.13/6.24 % (1034141)------------------------------
% 38.13/6.24 % (1034141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.13/6.24 % (1034141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.13/6.24 % (1034141)CaDiCaL version: 2.1.3
% 38.13/6.24 % (1034141)Termination reason: Instruction limit
% 38.13/6.24 % (1034141)Termination phase: Saturation
% 38.13/6.24 % (1034141)Time elapsed: 0.333 s
% 38.13/6.24 % (1034141)Peak memory usage: 136 MB
% 38.13/6.24 % (1034141)Instructions burned: 450 (million)
% 38.13/6.24 % (1034189)Instruction limit reached!
% 38.13/6.24 % (1034189)------------------------------
% 38.13/6.24 % (1034189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.13/6.24 % (1034189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.13/6.24 % (1034189)CaDiCaL version: 2.1.3
% 38.13/6.24 % (1034189)Termination reason: Instruction limit
% 38.13/6.24 % (1034189)Termination phase: Saturation
% 38.13/6.24 % (1034189)Time elapsed: 0.095 s
% 38.13/6.24 % (1034189)Peak memory usage: 117 MB
% 38.13/6.24 % (1034189)Instructions burned: 131 (million)
% 38.13/6.24 % (1034225)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2597125704:i=491:doe=on:rtra=on:gtg=position_2956 on theBenchmark for (2956ds/491Mi)
% 38.13/6.24 % (1034225)Refutation not found, incomplete strategy
% 38.13/6.24 % (1034225)------------------------------
% 38.13/6.24 % (1034225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.13/6.24 % (1034225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.13/6.24 % (1034225)CaDiCaL version: 2.1.3
% 38.13/6.24 % (1034225)Termination reason: Refutation not found, incomplete strategy
% 38.13/6.24 % (1034225)Time elapsed: 0.008 s
% 38.13/6.24 % (1034225)Peak memory usage: 89 MB
% 38.13/6.24 % (1034225)Instructions burned: 12 (million)
% 38.13/6.24 % (1034258)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3601863057:s2a=on:i=835:s2at=2:rtra=on_2955 on theBenchmark for (2955ds/835Mi)
% 38.13/6.24 % (1034150)Instruction limit reached!
% 38.13/6.24 % (1034150)------------------------------
% 38.13/6.24 % (1034150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.13/6.24 % (1034150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.13/6.24 % (1034150)CaDiCaL version: 2.1.3
% 38.13/6.24 % (1034150)Termination reason: Instruction limit
% 38.13/6.24 % (1034150)Termination phase: Saturation
% 40.07/6.83 % (1034150)Time elapsed: 0.358 s
% 40.07/6.83 % (1034150)Peak memory usage: 130 MB
% 40.07/6.83 % (1034150)Instructions burned: 1090 (million)
% 40.07/6.83 % (1034259)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2509396065:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2955 on theBenchmark for (2955ds/307Mi)
% 40.07/6.83 % (1034259)Refutation not found, incomplete strategy
% 40.07/6.83 % (1034259)------------------------------
% 40.07/6.83 % (1034259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.07/6.83 % (1034259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.07/6.83 % (1034259)CaDiCaL version: 2.1.3
% 40.07/6.83 % (1034259)Termination reason: Refutation not found, incomplete strategy
% 40.07/6.83 % (1034259)Time elapsed: 0.009 s
% 40.07/6.83 % (1034259)Peak memory usage: 89 MB
% 40.07/6.83 % (1034259)Instructions burned: 14 (million)
% 40.07/6.83 % (1034221)Instruction limit reached!
% 40.07/6.83 % (1034221)------------------------------
% 40.07/6.83 % (1034221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.07/6.83 % (1034221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.07/6.83 % (1034221)CaDiCaL version: 2.1.3
% 40.07/6.83 % (1034221)Termination reason: Instruction limit
% 40.07/6.83 % (1034221)Termination phase: Saturation
% 40.07/6.83 % (1034221)Time elapsed: 0.214 s
% 40.07/6.83 % (1034221)Peak memory usage: 119 MB
% 40.07/6.83 % (1034221)Instructions burned: 312 (million)
% 40.07/6.83 % (1034271)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2919245465:i=776:doe=on:rtra=on_2954 on theBenchmark for (2954ds/776Mi)
% 40.07/6.83 % (1034133)Instruction limit reached!
% 40.07/6.83 % (1034133)------------------------------
% 40.07/6.83 % (1034133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.07/6.83 % (1034133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.07/6.83 % (1034133)CaDiCaL version: 2.1.3
% 40.07/6.83 % (1034133)Termination reason: Instruction limit
% 40.07/6.83 % (1034133)Termination phase: Saturation
% 40.07/6.83 % (1034133)Time elapsed: 0.695 s
% 40.07/6.83 % (1034133)Peak memory usage: 93 MB
% 40.07/6.83 % (1034133)Instructions burned: 1053 (million)
% 40.07/6.83 % (1034225)------------------------------
% 40.07/6.83 % (1034225)------------------------------
% 40.07/6.83 % (1034307)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3548616773:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2953 on theBenchmark for (2953ds/646Mi)
% 40.07/6.83 % (1034313)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=1132705053:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2953 on theBenchmark for (2953ds/784Mi)
% 40.07/6.83 % (1034259)------------------------------
% 40.07/6.83 % (1034259)------------------------------
% 40.07/6.83 % (1034314)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=1781314773:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2953 on theBenchmark for (2953ds/1131Mi)
% 40.07/6.83 % (1034271)Instruction limit reached!
% 40.07/6.83 % (1034271)------------------------------
% 40.07/6.83 % (1034271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.07/6.83 % (1034271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.07/6.83 % (1034271)CaDiCaL version: 2.1.3
% 40.07/6.83 % (1034271)Termination reason: Instruction limit
% 40.07/6.83 % (1034271)Termination phase: Saturation
% 40.07/6.83 % (1034271)Time elapsed: 0.258 s
% 40.07/6.83 % (1034271)Peak memory usage: 120 MB
% 40.07/6.83 % (1034271)Instructions burned: 780 (million)
% 40.07/6.83 % (1034317)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=1903765037:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2951 on theBenchmark for (2951ds/246Mi)
% 40.07/6.83 % (1034258)Instruction limit reached!
% 40.07/6.83 % (1034258)------------------------------
% 40.07/6.83 % (1034258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.07/6.83 % (1034258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.07/6.83 % (1034258)CaDiCaL version: 2.1.3
% 40.07/6.83 % (1034258)Termination reason: Instruction limit
% 40.07/6.83 % (1034258)Termination phase: Saturation
% 40.07/6.83 % (1034258)Time elapsed: 0.449 s
% 40.07/6.83 % (1034258)Peak memory usage: 92 MB
% 47.38/7.68 % (1034258)Instructions burned: 835 (million)
% 47.38/7.68 % (1034319)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3917815337:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2950 on theBenchmark for (2950ds/775Mi)
% 47.38/7.68 % (1034317)Instruction limit reached!
% 47.38/7.68 % (1034317)------------------------------
% 47.38/7.68 % (1034317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034317)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034317)Termination reason: Instruction limit
% 47.38/7.68 % (1034317)Termination phase: Saturation
% 47.38/7.68 % (1034317)Time elapsed: 0.162 s
% 47.38/7.68 % (1034317)Peak memory usage: 115 MB
% 47.38/7.68 % (1034317)Instructions burned: 247 (million)
% 47.38/7.68 % (1034322)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=707054698:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2950 on theBenchmark for (2950ds/273Mi)
% 47.38/7.68 % (1034307)Instruction limit reached!
% 47.38/7.68 % (1034307)------------------------------
% 47.38/7.68 % (1034307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034307)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034307)Termination reason: Instruction limit
% 47.38/7.68 % (1034307)Termination phase: Saturation
% 47.38/7.68 % (1034307)Time elapsed: 0.472 s
% 47.38/7.68 % (1034307)Peak memory usage: 140 MB
% 47.38/7.68 % (1034307)Instructions burned: 646 (million)
% 47.38/7.68 % (1034324)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1626590471:i=102:nm=16:rtra=on_2948 on theBenchmark for (2948ds/102Mi)
% 47.38/7.68 % (1034319)Instruction limit reached!
% 47.38/7.68 % (1034319)------------------------------
% 47.38/7.68 % (1034319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034319)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034319)Termination reason: Instruction limit
% 47.38/7.68 % (1034319)Termination phase: Saturation
% 47.38/7.68 % (1034319)Time elapsed: 0.276 s
% 47.38/7.68 % (1034319)Peak memory usage: 95 MB
% 47.38/7.68 % (1034319)Instructions burned: 778 (million)
% 47.38/7.68 % (1034322)Instruction limit reached!
% 47.38/7.68 % (1034322)------------------------------
% 47.38/7.68 % (1034322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034322)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034322)Termination reason: Instruction limit
% 47.38/7.68 % (1034322)Termination phase: Saturation
% 47.38/7.68 % (1034322)Time elapsed: 0.179 s
% 47.38/7.68 % (1034322)Peak memory usage: 91 MB
% 47.38/7.68 % (1034322)Instructions burned: 274 (million)
% 47.38/7.68 % (1034324)Instruction limit reached!
% 47.38/7.68 % (1034324)------------------------------
% 47.38/7.68 % (1034324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034324)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034324)Termination reason: Instruction limit
% 47.38/7.68 % (1034324)Termination phase: Saturation
% 47.38/7.68 % (1034324)Time elapsed: 0.061 s
% 47.38/7.68 % (1034324)Peak memory usage: 89 MB
% 47.38/7.68 % (1034324)Instructions burned: 102 (million)
% 47.38/7.68 % (1034313)Instruction limit reached!
% 47.38/7.68 % (1034313)------------------------------
% 47.38/7.68 % (1034313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.38/7.68 % (1034313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.38/7.68 % (1034313)CaDiCaL version: 2.1.3
% 47.38/7.68 % (1034313)Termination reason: Instruction limit
% 47.38/7.68 % (1034313)Termination phase: Saturation
% 47.38/7.68 % (1034313)Time elapsed: 0.552 s
% 47.38/7.68 % (1034313)Peak memory usage: 122 MB
% 47.38/7.68 % (1034313)Instructions burned: 785 (million)
% 47.38/7.68 % (1034327)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3631971105:i=6400:doe=on:fsr=off:rtra=on_2947 on theBenchmark for (2947ds/6400Mi)
% 47.38/7.68 % (1034325)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3170930911:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2947 on theBenchmark for (2947ds/1094Mi)
% 62.25/9.60 % (1034328)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=1130987443:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2946 on theBenchmark for (2946ds/868Mi)
% 62.25/9.60 % (1034329)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=3199795100:i=1846:canc=cautious:fsr=off:rtra=on_2946 on theBenchmark for (2946ds/1846Mi)
% 62.25/9.60 % (1034329)Refutation not found, incomplete strategy
% 62.25/9.60 % (1034329)------------------------------
% 62.25/9.60 % (1034329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.25/9.60 % (1034329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.25/9.60 % (1034329)CaDiCaL version: 2.1.3
% 62.25/9.60 % (1034329)Termination reason: Refutation not found, incomplete strategy
% 62.25/9.60 % (1034329)Time elapsed: 0.007 s
% 62.25/9.60 % (1034329)Peak memory usage: 89 MB
% 62.25/9.60 % (1034329)Instructions burned: 11 (million)
% 62.25/9.60 % (1034330)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=788352875:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2946 on theBenchmark for (2946ds/36816Mi)
% 62.25/9.60 % (1034328)Refutation not found, incomplete strategy
% 62.25/9.60 % (1034328)------------------------------
% 62.25/9.60 % (1034328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.25/9.60 % (1034328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.25/9.60 % (1034328)CaDiCaL version: 2.1.3
% 62.25/9.60 % (1034328)Termination reason: Refutation not found, incomplete strategy
% 62.25/9.60 % (1034328)Time elapsed: 0.050 s
% 62.25/9.60 % (1034328)Peak memory usage: 116 MB
% 62.25/9.60 % (1034328)Instructions burned: 40 (million)
% 62.25/9.60 % (1034314)Instruction limit reached!
% 62.25/9.60 % (1034314)------------------------------
% 62.25/9.60 % (1034314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.25/9.60 % (1034314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.25/9.60 % (1034314)CaDiCaL version: 2.1.3
% 62.25/9.60 % (1034314)Termination reason: Instruction limit
% 62.25/9.60 % (1034314)Termination phase: Saturation
% 62.25/9.60 % (1034314)Time elapsed: 0.688 s
% 62.25/9.60 % (1034314)Peak memory usage: 124 MB
% 62.25/9.60 % (1034314)Instructions burned: 1132 (million)
% 62.25/9.60 % (1034336)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1905608555:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2944 on theBenchmark for (2944ds/273Mi)
% 62.25/9.60 % (1034329)------------------------------
% 62.25/9.60 % (1034329)------------------------------
% 62.25/9.60 % (1034328)------------------------------
% 62.25/9.60 % (1034328)------------------------------
% 62.25/9.60 % (1034338)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=2463020387:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2943 on theBenchmark for (2943ds/863Mi)
% 62.25/9.60 % (1034336)Instruction limit reached!
% 62.25/9.60 % (1034336)------------------------------
% 62.25/9.60 % (1034336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.25/9.60 % (1034336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.25/9.60 % (1034336)CaDiCaL version: 2.1.3
% 62.25/9.60 % (1034336)Termination reason: Instruction limit
% 62.25/9.60 % (1034336)Termination phase: Saturation
% 62.25/9.60 % (1034336)Time elapsed: 0.184 s
% 62.25/9.60 % (1034336)Peak memory usage: 92 MB
% 62.25/9.60 % (1034336)Instructions burned: 274 (million)
% 62.25/9.60 % (1034339)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=58854772:i=5811:kws=precedence:nm=0:rtra=on_2942 on theBenchmark for (2942ds/5811Mi)
% 62.25/9.60 % (1034338)Refutation not found, incomplete strategy
% 62.25/9.60 % (1034338)------------------------------
% 62.25/9.60 % (1034338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.25/9.60 % (1034338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.25/9.60 % (1034338)CaDiCaL version: 2.1.3
% 62.25/9.60 % (1034338)Termination reason: Refutation not found, incomplete strategy
% 62.25/9.60 % (1034338)Time elapsed: 0.056 s
% 62.25/9.60 % (1034338)Peak memory usage: 116 MB
% 62.25/9.60 % (1034338)Instructions burned: 49 (million)
% 62.25/9.60 % (1034341)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=1192257813:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2941 on theBenchmark for (2941ds/2216Mi)
% 74.35/11.42 % (1034325)Instruction limit reached!
% 74.35/11.42 % (1034325)------------------------------
% 74.35/11.42 % (1034325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034325)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034325)Termination reason: Instruction limit
% 74.35/11.42 % (1034325)Termination phase: Saturation
% 74.35/11.42 % (1034325)Time elapsed: 0.631 s
% 74.35/11.42 % (1034325)Peak memory usage: 100 MB
% 74.35/11.42 % (1034325)Instructions burned: 1094 (million)
% 74.35/11.42 % (1034338)------------------------------
% 74.35/11.42 % (1034338)------------------------------
% 74.35/11.42 % (1034344)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2412622721:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2939 on theBenchmark for (2939ds/801Mi)
% 74.35/11.42 % (1034344)Refutation not found, incomplete strategy
% 74.35/11.42 % (1034344)------------------------------
% 74.35/11.42 % (1034344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034344)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034344)Termination reason: Refutation not found, incomplete strategy
% 74.35/11.42 % (1034344)Time elapsed: 0.013 s
% 74.35/11.42 % (1034344)Peak memory usage: 89 MB
% 74.35/11.42 % (1034344)Instructions burned: 19 (million)
% 74.35/11.42 % (1034345)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=837534839:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2938 on theBenchmark for (2938ds/1026Mi)
% 74.35/11.42 % (1034345)Refutation not found, incomplete strategy
% 74.35/11.42 % (1034345)------------------------------
% 74.35/11.42 % (1034345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034345)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034345)Termination reason: Refutation not found, incomplete strategy
% 74.35/11.42 % (1034345)Time elapsed: 0.018 s
% 74.35/11.42 % (1034345)Peak memory usage: 89 MB
% 74.35/11.42 % (1034345)Instructions burned: 26 (million)
% 74.35/11.42 % (1034344)------------------------------
% 74.35/11.42 % (1034344)------------------------------
% 74.35/11.42 % (1034131)Instruction limit reached!
% 74.35/11.42 % (1034131)------------------------------
% 74.35/11.42 % (1034131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034131)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034131)Termination reason: Instruction limit
% 74.35/11.42 % (1034131)Termination phase: Saturation
% 74.35/11.42 % (1034131)Time elapsed: 2.464 s
% 74.35/11.42 % (1034131)Peak memory usage: 111 MB
% 74.35/11.42 % (1034131)Instructions burned: 4430 (million)
% 74.35/11.42 % (1034345)------------------------------
% 74.35/11.42 % (1034345)------------------------------
% 74.35/11.42 % (1034348)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2591222089:i=3509:rtra=on_2935 on theBenchmark for (2935ds/3509Mi)
% 74.35/11.42 % (1034349)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1039701022:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/2127Mi)
% 74.35/11.42 % (1034350)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=611706417:i=1959:rtra=on:fsd=on:proc=on_2934 on theBenchmark for (2934ds/1959Mi)
% 74.35/11.42 % (1034350)Refutation not found, incomplete strategy
% 74.35/11.42 % (1034350)------------------------------
% 74.35/11.42 % (1034350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034350)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034350)Termination reason: Refutation not found, incomplete strategy
% 74.35/11.42 % (1034350)Time elapsed: 0.042 s
% 74.35/11.42 % (1034350)Peak memory usage: 116 MB
% 74.35/11.42 % (1034350)Instructions burned: 28 (million)
% 74.35/11.42 % (1034327)Instruction limit reached!
% 74.35/11.42 % (1034327)------------------------------
% 74.35/11.42 % (1034327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034327)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034327)Termination reason: Instruction limit
% 74.35/11.42 % (1034327)Termination phase: Saturation
% 74.35/11.42 % (1034327)Time elapsed: 1.459 s
% 74.35/11.42 % (1034327)Peak memory usage: 119 MB
% 74.35/11.42 % (1034327)Instructions burned: 6404 (million)
% 74.35/11.42 % (1034354)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2484815550:s2a=on:i=3553:nm=0:rtra=on_2931 on theBenchmark for (2931ds/3553Mi)
% 74.35/11.42 % (1034350)------------------------------
% 74.35/11.42 % (1034350)------------------------------
% 74.35/11.42 % (1034356)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=776059278:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2930 on theBenchmark for (2930ds/3201Mi)
% 74.35/11.42 % (1034341)Instruction limit reached!
% 74.35/11.42 % (1034341)------------------------------
% 74.35/11.42 % (1034341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034341)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034341)Termination reason: Instruction limit
% 74.35/11.42 % (1034341)Termination phase: Saturation
% 74.35/11.42 % (1034341)Time elapsed: 1.279 s
% 74.35/11.42 % (1034341)Peak memory usage: 127 MB
% 74.35/11.42 % (1034341)Instructions burned: 2218 (million)
% 74.35/11.42 % (1034358)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=1652793876:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2927 on theBenchmark for (2927ds/4093Mi)
% 74.35/11.42 % (1034349)Instruction limit reached!
% 74.35/11.42 % (1034349)------------------------------
% 74.35/11.42 % (1034349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034349)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034349)Termination reason: Instruction limit
% 74.35/11.42 % (1034349)Termination phase: Saturation
% 74.35/11.42 % (1034349)Time elapsed: 1.105 s
% 74.35/11.42 % (1034349)Peak memory usage: 105 MB
% 74.35/11.42 % (1034349)Instructions burned: 2127 (million)
% 74.35/11.42 % (1034360)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=2845715831:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2923 on theBenchmark for (2923ds/21173Mi)
% 74.35/11.42 % (1034354)Instruction limit reached!
% 74.35/11.42 % (1034354)------------------------------
% 74.35/11.42 % (1034354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034354)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034354)Termination reason: Instruction limit
% 74.35/11.42 % (1034354)Termination phase: Saturation
% 74.35/11.42 % (1034354)Time elapsed: 1.200 s
% 74.35/11.42 % (1034354)Peak memory usage: 102 MB
% 74.35/11.42 % (1034354)Instructions burned: 3554 (million)
% 74.35/11.42 % (1034362)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=4152361896:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2918 on theBenchmark for (2918ds/10544Mi)
% 74.35/11.42 % (1034356)Instruction limit reached!
% 74.35/11.42 % (1034356)------------------------------
% 74.35/11.42 % (1034356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034356)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034356)Termination reason: Instruction limit
% 74.35/11.42 % (1034356)Termination phase: Saturation
% 74.35/11.42 % (1034356)Time elapsed: 1.514 s
% 74.35/11.42 % (1034356)Peak memory usage: 115 MB
% 74.35/11.42 % (1034356)Instructions burned: 3202 (million)
% 74.35/11.42 % (1034348)Instruction limit reached!
% 74.35/11.42 % (1034348)------------------------------
% 74.35/11.42 % (1034348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034348)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034348)Termination reason: Instruction limit
% 74.35/11.42 % (1034348)Termination phase: Saturation
% 74.35/11.42 % (1034348)Time elapsed: 2.159 s
% 74.35/11.42 % (1034348)Peak memory usage: 111 MB
% 74.35/11.42 % (1034348)Instructions burned: 3509 (million)
% 74.35/11.42 % (1034364)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4001462679:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2913 on theBenchmark for (2913ds/1262Mi)
% 74.35/11.42 % (1034365)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1198638254:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2912 on theBenchmark for (2912ds/775Mi)
% 74.35/11.42 % (1034339)Instruction limit reached!
% 74.35/11.42 % (1034339)------------------------------
% 74.35/11.42 % (1034339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034339)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034339)Termination reason: Instruction limit
% 74.35/11.42 % (1034339)Termination phase: Saturation
% 74.35/11.42 % (1034339)Time elapsed: 3.188 s
% 74.35/11.42 % (1034339)Peak memory usage: 135 MB
% 74.35/11.42 % (1034339)Instructions burned: 5813 (million)
% 74.35/11.42 % (1034368)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2812112672:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2909 on theBenchmark for (2909ds/270Mi)
% 74.35/11.42 % (1034368)Instruction limit reached!
% 74.35/11.42 % (1034368)------------------------------
% 74.35/11.42 % (1034368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034368)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034368)Termination reason: Instruction limit
% 74.35/11.42 % (1034368)Termination phase: Saturation
% 74.35/11.42 % (1034368)Time elapsed: 0.174 s
% 74.35/11.42 % (1034368)Peak memory usage: 91 MB
% 74.35/11.42 % (1034368)Instructions burned: 270 (million)
% 74.35/11.42 % (1034365)Instruction limit reached!
% 74.35/11.42 % (1034365)------------------------------
% 74.35/11.42 % (1034365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034365)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034365)Termination reason: Instruction limit
% 74.35/11.42 % (1034365)Termination phase: Saturation
% 74.35/11.42 % (1034365)Time elapsed: 0.508 s
% 74.35/11.42 % (1034365)Peak memory usage: 95 MB
% 74.35/11.42 % (1034365)Instructions burned: 775 (million)
% 74.35/11.42 % (1034364)Instruction limit reached!
% 74.35/11.42 % (1034364)------------------------------
% 74.35/11.42 % (1034364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034364)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034364)Termination reason: Instruction limit
% 74.35/11.42 % (1034364)Termination phase: Saturation
% 74.35/11.42 % (1034364)Time elapsed: 0.687 s
% 74.35/11.42 % (1034364)Peak memory usage: 122 MB
% 74.35/11.42 % (1034364)Instructions burned: 1263 (million)
% 74.35/11.42 % (1034370)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=69933143:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2906 on theBenchmark for (2906ds/17165Mi)
% 74.35/11.42 % (1034371)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2635771898:s2a=on:i=13094:s2at=-1:rtra=on_2906 on theBenchmark for (2906ds/13094Mi)
% 74.35/11.42 % (1034372)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1742599916:st=2:i=12633:rtra=on:ss=axioms_2905 on theBenchmark for (2905ds/12633Mi)
% 74.35/11.42 % (1034358)Instruction limit reached!
% 74.35/11.42 % (1034358)------------------------------
% 74.35/11.42 % (1034358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.35/11.42 % (1034358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.35/11.42 % (1034358)CaDiCaL version: 2.1.3
% 74.35/11.42 % (1034358)Termination reason: Instruction limit
% 74.35/11.42 % (1034358)Termination phase: Saturation
% 74.35/11.42 % (1034358)Time elapsed: 2.316 s
% 74.35/11.42 % (1034358)Peak memory usage: 149 MB
% 74.35/11.42 % (1034358)Instructions burned: 4093 (million)
% 74.35/11.42 % (1034376)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3965388390:i=1783:rtra=on:gtg=position_2902 on theBenchmark for (2902ds/1783Mi)
% 74.35/11.42 % (1034376)First to succeed.
% 74.35/11.42 % (1034376)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1033850"
% 74.35/11.42 % (1034376)Refutation found. Thanks to Tanya!
% 74.35/11.42 % SZS status Theorem for theBenchmark
% 74.35/11.42 % SZS output start Proof for theBenchmark
% See solution above
% 75.51/11.65 % (1034376)------------------------------
% 75.51/11.65 % (1034376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.51/11.65 % (1034376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.51/11.65 % (1034376)CaDiCaL version: 2.1.3
% 75.51/11.65 % (1034376)Termination reason: Refutation
% 75.51/11.65 % (1034376)Time elapsed: 0.453 s
% 75.51/11.65 % (1034376)Peak memory usage: 121 MB
% 75.51/11.65 % (1034376)Instructions burned: 731 (million)
% 75.51/11.65 % (1034376)------------------------------
% 75.51/11.65 % (1034376)------------------------------
% 75.51/11.65 % (1033850)Success in time 10.56 s
% 75.51/11.65 % Vampire exiting
%------------------------------------------------------------------------------