%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TIM029_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 : n009.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:33 PM UTC 2026
% Result : Theorem 30.76s 5.04s
% Output : Refutation 31.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 7
% Syntax : Number of formulae : 38 ( 9 unt; 0 typ; 0 def)
% Number of atoms : 224 ( 134 equ)
% Maximal formula atoms : 12 ( 5 avg)
% Number of connectives : 266 ( 80 ~; 147 |; 33 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 11 avg)
% Maximal term depth : 12 ( 2 avg)
% Number arithmetic : 924 ( 21 atm; 350 fun; 394 num; 159 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 : 17 ( 13 usr; 1 prp; 0-9 aty)
% Number of functors : 36 ( 11 usr; 28 con; 0-5 aty)
% Number of variables : 181 ( 179 !; 2 ?; 181 :)
% 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_79,type,
'$inst0': $int ).
tff(func_def_80,type,
'$inst1': $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(f65,axiom,
! [X1: $int,X0: $int] :
( ( ( X0 = 1 )
| ( X0 = 2 ) )
=> zeller_prep(X0,X1,$sum(X0,12),$difference(X1,1),$remainder_e($difference(X1,1),100),$quotient_e($difference(X1,1),100)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zeller_adj_janfeb) ).
tff(f67,negated_conjecture,
! [X3: day_name,X6: $int,X1: $int,X0: $int,X9: $int,X5: $int,X8: $int,X7: $int,X2: $int,X10: $int,X4: $int] :
( ( $greater(X0,1582)
& ( X10 = $remainder_e($sum($remainder_e(X9,7),7),7) )
& ( X0 != 1776 )
& ( X0 != 2025 )
& map_iso(X10,X3)
& ( X0 != 2024 )
& ( X0 != 1969 )
& ( X0 != 1985 )
& ( X9 = $sum(X2,$sum(X8,$sum(X6,$sum($quotient_e(X6,4),$sum($quotient_e(X7,4),$product(5,X7)))))) )
& ( X8 = $quotient_e($product(13,$sum(X4,1)),5) )
& zeller_prep(X1,X0,X4,X5,X6,X7) )
=> weekday(ymd(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',calc_weekday_zeller) ).
tff(f71,axiom,
map_iso(3,tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',map_3) ).
tff(f88,conjecture,
? [X0: day_name] :
( weekday(ymd(2030,1,1),X0)
& ( X0 = tuesday ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_2030) ).
tff(f89,negated_conjecture,
~ ? [X0: day_name] :
( weekday(ymd(2030,1,1),X0)
& ( X0 = tuesday ) ),
inference(negated_conjecture,[status(cth)],[f88]) ).
tff(f109,plain,
! [X1: $int,X0: $int] :
( ( ( X0 = 1 )
| ( X0 = 2 ) )
=> zeller_prep(X0,X1,$sum(X0,12),$sum(X1,$uminus(1)),$remainder_e($sum(X1,$uminus(1)),100),$quotient_e($sum(X1,$uminus(1)),100)) ),
inference(theory_normalization,[],[f65]) ).
tff(f110,plain,
! [X3: day_name,X6: $int,X1: $int,X0: $int,X9: $int,X5: $int,X8: $int,X7: $int,X2: $int,X10: $int,X4: $int] :
( ( $less(1582,X0)
& ( X10 = $remainder_e($sum($remainder_e(X9,7),7),7) )
& ( X0 != 1776 )
& ( X0 != 2025 )
& map_iso(X10,X3)
& ( X0 != 2024 )
& ( X0 != 1969 )
& ( X0 != 1985 )
& ( X9 = $sum(X2,$sum(X8,$sum(X6,$sum($quotient_e(X6,4),$sum($quotient_e(X7,4),$product(5,X7)))))) )
& ( X8 = $quotient_e($product(13,$sum(X4,1)),5) )
& zeller_prep(X1,X0,X4,X5,X6,X7) )
=> weekday(ymd(X0,X1,X2),X3) ),
inference(theory_normalization,[],[f67]) ).
tff(f116,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f125,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,$sum(X0,1)) ),
introduced(definition,[],[tha_order_plus_one_dichotomy]) ).
tff(f131,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum($product(X0,X1),$product(X0,X2)) = $product(X0,$sum(X1,X2)) ),
introduced(definition,[],[tha_distributivity]) ).
tff(f158,plain,
! [X0: $int,X1: $int] :
( ( ( 2 = X1 )
| ( 1 = X1 ) )
=> zeller_prep(X1,X0,$sum(X1,12),$sum(X0,$uminus(1)),$remainder_e($sum(X0,$uminus(1)),100),$quotient_e($sum(X0,$uminus(1)),100)) ),
inference(rectify,[],[f109]) ).
tff(f159,plain,
! [X3: $int,X6: $int,X7: $int,X10: $int,X8: $int,X4: $int,X5: $int,X9: $int,X1: $int,X2: $int,X0: day_name] :
( ( ( 1985 != X3 )
& $less(1582,X3)
& ( 1969 != X3 )
& ( 2025 != X3 )
& zeller_prep(X2,X3,X10,X5,X1,X7)
& ( $remainder_e($sum($remainder_e(X4,7),7),7) = X9 )
& map_iso(X9,X0)
& ( 2024 != X3 )
& ( $quotient_e($product(13,$sum(X10,1)),5) = X6 )
& ( 1776 != X3 )
& ( $sum(X8,$sum(X6,$sum(X1,$sum($quotient_e(X1,4),$sum($quotient_e(X7,4),$product(5,X7)))))) = X4 ) )
=> weekday(ymd(X3,X2,X8),X0) ),
inference(rectify,[],[f110]) ).
tff(f175,plain,
! [X3: $int,X6: $int,X7: $int,X10: $int,X8: $int,X4: $int,X5: $int,X9: $int,X1: $int,X2: $int,X0: day_name] :
( weekday(ymd(X3,X2,X8),X0)
| ( 1985 = X3 )
| ~ $less(1582,X3)
| ( 1969 = X3 )
| ( 2025 = X3 )
| ~ zeller_prep(X2,X3,X10,X5,X1,X7)
| ( $remainder_e($sum($remainder_e(X4,7),7),7) != X9 )
| ~ map_iso(X9,X0)
| ( 2024 = X3 )
| ( $quotient_e($product(13,$sum(X10,1)),5) != X6 )
| ( 1776 = X3 )
| ( $sum(X8,$sum(X6,$sum(X1,$sum($quotient_e(X1,4),$sum($quotient_e(X7,4),$product(5,X7)))))) != X4 ) ),
inference(ennf_transformation,[],[f159]) ).
tff(f176,plain,
! [X8: $int,X4: $int,X7: $int,X6: $int,X0: day_name,X3: $int,X10: $int,X9: $int,X2: $int,X1: $int,X5: $int] :
( weekday(ymd(X3,X2,X8),X0)
| ~ $less(1582,X3)
| ( $remainder_e($sum($remainder_e(X4,7),7),7) != X9 )
| ( 1969 = X3 )
| ~ map_iso(X9,X0)
| ( 2024 = X3 )
| ( 2025 = X3 )
| ( 1776 = X3 )
| ( $sum(X8,$sum(X6,$sum(X1,$sum($quotient_e(X1,4),$sum($quotient_e(X7,4),$product(5,X7)))))) != X4 )
| ( 1985 = X3 )
| ( $quotient_e($product(13,$sum(X10,1)),5) != X6 )
| ~ zeller_prep(X2,X3,X10,X5,X1,X7) ),
inference(flattening,[],[f175]) ).
tff(f190,plain,
! [X0: day_name] :
( ~ weekday(ymd(2030,1,1),X0)
| ( tuesday != X0 ) ),
inference(ennf_transformation,[],[f89]) ).
tff(f216,plain,
! [X0: $int,X1: $int] :
( zeller_prep(X1,X0,$sum(X1,12),$sum(X0,$uminus(1)),$remainder_e($sum(X0,$uminus(1)),100),$quotient_e($sum(X0,$uminus(1)),100))
| ( ( 1 != X1 )
& ( 2 != X1 ) ) ),
inference(ennf_transformation,[],[f158]) ).
tff(f244,plain,
! [X0: $int,X1: $int,X2: $int,X3: $int,X4: day_name,X5: $int,X6: $int,X7: $int,X8: $int,X9: $int,X10: $int] :
( weekday(ymd(X5,X8,X0),X4)
| ~ $less(1582,X5)
| ( $remainder_e($sum($remainder_e(X1,7),7),7) != X7 )
| ( 1969 = X5 )
| ~ map_iso(X7,X4)
| ( 2024 = X5 )
| ( 2025 = X5 )
| ( 1776 = X5 )
| ( $sum(X0,$sum(X3,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X1 )
| ( 1985 = X5 )
| ( $quotient_e($product(13,$sum(X6,1)),5) != X3 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2) ),
inference(rectify,[],[f176]) ).
tff(f283,plain,
! [X0: $int,X1: $int] :
( zeller_prep(X1,X0,$sum(X1,12),$sum(X0,$uminus(1)),$remainder_e($sum(X0,$uminus(1)),100),$quotient_e($sum(X0,$uminus(1)),100))
| ( 1 != X1 ) ),
inference(cnf_transformation,[],[f216]) ).
tff(f302,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X1: $int,X8: $int,X6: $int,X9: $int,X7: $int,X4: day_name,X5: $int] :
( weekday(ymd(X5,X8,X0),X4)
| ~ $less(1582,X5)
| ( $remainder_e($sum($remainder_e(X1,7),7),7) != X7 )
| ( 1969 = X5 )
| ~ map_iso(X7,X4)
| ( 2024 = X5 )
| ( 2025 = X5 )
| ( 1776 = X5 )
| ( $sum(X0,$sum(X3,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X1 )
| ( 1985 = X5 )
| ( $quotient_e($product(13,$sum(X6,1)),5) != X3 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2) ),
inference(cnf_transformation,[],[f244]) ).
tff(f337,plain,
! [X0: day_name] :
( ~ weekday(ymd(2030,1,1),X0)
| ( tuesday != X0 ) ),
inference(cnf_transformation,[],[f190]) ).
tff(f343,plain,
map_iso(3,tuesday),
inference(cnf_transformation,[],[f71]) ).
tff(f359,plain,
! [X0: $int] : zeller_prep(1,X0,$sum(1,12),$sum(X0,$uminus(1)),$remainder_e($sum(X0,$uminus(1)),100),$quotient_e($sum(X0,$uminus(1)),100)),
inference(equality_resolution,[],[f283]) ).
tff(f361,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X1: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( weekday(ymd(X5,X8,X0),X4)
| ~ $less(1582,X5)
| ( 1969 = X5 )
| ~ map_iso($remainder_e($sum($remainder_e(X1,7),7),7),X4)
| ( 2024 = X5 )
| ( 2025 = X5 )
| ( 1776 = X5 )
| ( $sum(X0,$sum(X3,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))) != X1 )
| ( 1985 = X5 )
| ( $quotient_e($product(13,$sum(X6,1)),5) != X3 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2) ),
inference(equality_resolution,[],[f302]) ).
tff(f362,plain,
! [X2: $int,X3: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( weekday(ymd(X5,X8,X0),X4)
| ~ $less(1582,X5)
| ( 1969 = X5 )
| ~ map_iso($remainder_e($sum($remainder_e($sum(X0,$sum(X3,$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7),7),7),X4)
| ( 2024 = X5 )
| ( 2025 = X5 )
| ( 1776 = X5 )
| ( 1985 = X5 )
| ( $quotient_e($product(13,$sum(X6,1)),5) != X3 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2) ),
inference(equality_resolution,[],[f361]) ).
tff(f363,plain,
! [X2: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( ~ zeller_prep(X8,X5,X6,X10,X9,X2)
| ( 1969 = X5 )
| ( 2024 = X5 )
| ~ map_iso($remainder_e($sum($remainder_e($sum(X0,$sum($quotient_e($product(13,$sum(X6,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7),7),7),X4)
| weekday(ymd(X5,X8,X0),X4)
| ( 1776 = X5 )
| ( 2025 = X5 )
| ( 1985 = X5 )
| ~ $less(1582,X5) ),
inference(equality_resolution,[],[f362]) ).
tff(f373,plain,
~ weekday(ymd(2030,1,1),tuesday),
inference(equality_resolution,[],[f337]) ).
tff(f394,plain,
! [X0: $int] : zeller_prep(1,X0,13,$sum(X0,-1),$remainder_e($sum(X0,-1),100),$quotient_e($sum(X0,-1),100)),
inference(evaluation,[],[f359]) ).
tff(f399,plain,
! [X2: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( ( 1969 = X5 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2)
| ( 1776 = X5 )
| ( 1985 = X5 )
| ~ $less(1582,X5)
| ( 2025 = X5 )
| ( 2024 = X5 )
| weekday(ymd(X5,X8,X0),X4)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X0,$sum($quotient_e($product(13,$sum(X6,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7)),7),X4) ),
inference(forward_demodulation,[],[f363,f116]) ).
tff(f401,plain,
! [X2: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( ( 2025 = X5 )
| ( 1985 = X5 )
| ( 2024 = X5 )
| ( 1969 = X5 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X0,$sum($quotient_e($sum($product(13,X6),$product(13,1)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7)),7),X4)
| ( 1776 = X5 )
| weekday(ymd(X5,X8,X0),X4)
| ~ zeller_prep(X8,X5,X6,X10,X9,X2)
| ~ $less(1582,X5) ),
inference(forward_demodulation,[],[f399,f131]) ).
tff(f402,plain,
! [X2: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( weekday(ymd(X5,X8,X0),X4)
| ( 1969 = X5 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2)
| ~ $less(1582,X5)
| ( 2025 = X5 )
| ( 2024 = X5 )
| ( 1776 = X5 )
| ( 1985 = X5 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X0,$sum($quotient_e($sum($product(13,X6),13),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7)),7),X4) ),
inference(evaluation,[],[f401]) ).
tff(f404,plain,
! [X2: $int,X10: $int,X0: $int,X8: $int,X6: $int,X9: $int,X4: day_name,X5: $int] :
( ~ $less(1582,X5)
| weekday(ymd(X5,X8,X0),X4)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X0,$sum($quotient_e($sum(13,$product(13,X6)),5),$sum(X9,$sum($quotient_e(X9,4),$sum($quotient_e(X2,4),$product(5,X2)))))),7)),7),X4)
| ( 1969 = X5 )
| ~ zeller_prep(X8,X5,X6,X10,X9,X2)
| ( 2024 = X5 )
| ( 1985 = X5 )
| ( 2025 = X5 )
| ( 1776 = X5 ) ),
inference(forward_demodulation,[],[f402,f116]) ).
tff(f430,plain,
! [X2: $int,X3: day_name,X0: $int,X1: $int,X6: $int,X7: $int,X4: $int,X5: $int] :
( ( 2024 = X0 )
| ( 1776 = X0 )
| ( 1969 = X0 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X2,$sum($quotient_e($sum(13,$product(13,X4)),5),$sum(X5,$sum($quotient_e(X5,4),$sum($quotient_e(X6,4),$product(5,X6)))))),7)),7),X3)
| weekday(ymd(X0,X1,X2),X3)
| $less(X0,$sum(1582,1))
| ( 2025 = X0 )
| ~ zeller_prep(X1,X0,X4,X7,X5,X6)
| ( 1985 = X0 ) ),
inference(resolution,[],[f125,f404]) ).
tff(f432,plain,
! [X2: $int,X3: day_name,X0: $int,X1: $int,X6: $int,X7: $int,X4: $int,X5: $int] :
( ~ zeller_prep(X1,X0,X4,X7,X5,X6)
| ( 1985 = X0 )
| weekday(ymd(X0,X1,X2),X3)
| ( 1776 = X0 )
| ( 1969 = X0 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X2,$sum($quotient_e($sum(13,$product(13,X4)),5),$sum(X5,$sum($quotient_e(X5,4),$sum($quotient_e(X6,4),$product(5,X6)))))),7)),7),X3)
| ( 2024 = X0 )
| $less(X0,1583)
| ( 2025 = X0 ) ),
inference(evaluation,[],[f430]) ).
tff(f804,plain,
! [X2: day_name,X0: $int,X1: $int] :
( ( 1776 = X0 )
| ( 2025 = X0 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X1,$sum($quotient_e($sum(13,$product(13,13)),5),$sum($remainder_e($sum(X0,-1),100),$sum($quotient_e($remainder_e($sum(X0,-1),100),4),$sum($quotient_e($quotient_e($sum(X0,-1),100),4),$product(5,$quotient_e($sum(X0,-1),100))))))),7)),7),X2)
| weekday(ymd(X0,1,X1),X2)
| ( 2024 = X0 )
| $less(X0,1583)
| ( 1969 = X0 )
| ( 1985 = X0 ) ),
inference(resolution,[],[f394,f432]) ).
tff(f816,plain,
! [X2: day_name,X0: $int,X1: $int] :
( weekday(ymd(X0,1,X1),X2)
| $less(X0,1583)
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(X1,$sum(36,$sum($remainder_e($sum(X0,-1),100),$sum($quotient_e($remainder_e($sum(X0,-1),100),4),$sum($quotient_e($quotient_e($sum(X0,-1),100),4),$product(5,$quotient_e($sum(X0,-1),100))))))),7)),7),X2)
| ( 2025 = X0 )
| ( 1969 = X0 )
| ( 1776 = X0 )
| ( 1985 = X0 )
| ( 2024 = X0 ) ),
inference(evaluation,[],[f804]) ).
tff(f822,plain,
( ( 1985 = 2030 )
| ~ map_iso($remainder_e($sum(7,$remainder_e($sum(1,$sum(36,$sum($remainder_e($sum(2030,-1),100),$sum($quotient_e($remainder_e($sum(2030,-1),100),4),$sum($quotient_e($quotient_e($sum(2030,-1),100),4),$product(5,$quotient_e($sum(2030,-1),100))))))),7)),7),tuesday)
| ( 2024 = 2030 )
| ( 1969 = 2030 )
| $less(2030,1583)
| ( 1776 = 2030 )
| ( 2025 = 2030 ) ),
inference(resolution,[],[f816,f373]) ).
tff(f825,plain,
~ map_iso(3,tuesday),
inference(evaluation,[],[f822]) ).
tff(f828,plain,
$false,
inference(forward_subsumption_resolution,[],[f825,f343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TIM029_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 18:48:00 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 3.80/1.27 % (3344937)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.80/1.27 % (3345070)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2173642508:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.80/1.27 % (3345075)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2180427443:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.80/1.27 % (3345069)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1477877918:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.80/1.27 % (3345073)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3331084600:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.80/1.27 % (3345071)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=933969913:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.80/1.27 % (3345072)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1552996105:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.80/1.27 % (3345074)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3740132146:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.80/1.27 % (3345073)Instruction limit reached!
% 3.80/1.27 % (3345073)------------------------------
% 3.80/1.27 % (3345073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.27 % (3345073)CaDiCaL version: 2.1.3
% 3.80/1.27 % (3345073)Termination reason: Instruction limit
% 3.80/1.27 % (3345073)Termination phase: Property scanning
% 3.80/1.27 % (3345073)Time elapsed: 0.003 s
% 3.80/1.27 % (3345073)Peak memory usage: 85 MB
% 3.80/1.27 % (3345073)Instructions burned: 5 (million)
% 3.80/1.27 % (3345072)Instruction limit reached!
% 3.80/1.27 % (3345072)------------------------------
% 3.80/1.27 % (3345072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.27 % (3345072)CaDiCaL version: 2.1.3
% 3.80/1.27 % (3345072)Termination reason: Instruction limit
% 3.80/1.27 % (3345072)Termination phase: Property scanning
% 3.80/1.27 % (3345072)Time elapsed: 0.004 s
% 3.80/1.27 % (3345072)Peak memory usage: 86 MB
% 3.80/1.27 % (3345072)Instructions burned: 7 (million)
% 3.80/1.27 % (3345069)Instruction limit reached!
% 3.80/1.27 % (3345069)------------------------------
% 3.80/1.27 % (3345069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.27 % (3345069)CaDiCaL version: 2.1.3
% 3.80/1.27 % (3345069)Termination reason: Instruction limit
% 3.80/1.27 % (3345069)Termination phase: Saturation
% 3.80/1.27 % (3345069)Time elapsed: 0.031 s
% 3.80/1.27 % (3345069)Peak memory usage: 115 MB
% 3.80/1.27 % (3345069)Instructions burned: 13 (million)
% 3.80/1.27 % (3345075)Instruction limit reached!
% 3.80/1.27 % (3345075)------------------------------
% 3.80/1.27 % (3345075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.27 % (3345075)CaDiCaL version: 2.1.3
% 3.80/1.27 % (3345075)Termination reason: Instruction limit
% 3.80/1.27 % (3345075)Termination phase: Saturation
% 3.80/1.27 % (3345075)Time elapsed: 0.043 s
% 3.80/1.27 % (3345075)Peak memory usage: 115 MB
% 3.80/1.27 % (3345075)Instructions burned: 33 (million)
% 3.80/1.27 % (3345074)Instruction limit reached!
% 3.80/1.27 % (3345074)------------------------------
% 3.80/1.27 % (3345074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.27 % (3345074)CaDiCaL version: 2.1.3
% 3.80/1.27 % (3345074)Termination reason: Instruction limit
% 3.80/1.27 % (3345074)Termination phase: Saturation
% 3.80/1.27 % (3345074)Time elapsed: 0.051 s
% 3.80/1.27 % (3345074)Peak memory usage: 115 MB
% 3.80/1.27 % (3345074)Instructions burned: 47 (million)
% 3.80/1.27 % (3345070)Instruction limit reached!
% 3.80/1.27 % (3345070)------------------------------
% 3.80/1.27 % (3345070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.27 % (3345070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345070)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345070)Termination reason: Instruction limit
% 4.61/1.41 % (3345070)Termination phase: Saturation
% 4.61/1.41 % (3345070)Time elapsed: 0.112 s
% 4.61/1.41 % (3345070)Peak memory usage: 118 MB
% 4.61/1.41 % (3345070)Instructions burned: 309 (million)
% 4.61/1.41 % (3345123)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=3858017812:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.61/1.41 % (3345122)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3884803235:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.61/1.41 % (3345122)Refutation not found, incomplete strategy
% 4.61/1.41 % (3345122)------------------------------
% 4.61/1.41 % (3345122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.41 % (3345122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345122)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345122)Termination reason: Refutation not found, incomplete strategy
% 4.61/1.41 % (3345122)Time elapsed: 0.012 s
% 4.61/1.41 % (3345122)Peak memory usage: 89 MB
% 4.61/1.41 % (3345122)Instructions burned: 17 (million)
% 4.61/1.41 % (3345152)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=85805731:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.61/1.41 % (3345133)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2547370009:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.61/1.41 % (3345123)Instruction limit reached!
% 4.61/1.41 % (3345123)------------------------------
% 4.61/1.41 % (3345123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.41 % (3345123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345123)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345123)Termination reason: Instruction limit
% 4.61/1.41 % (3345123)Termination phase: Saturation
% 4.61/1.41 % (3345123)Time elapsed: 0.021 s
% 4.61/1.41 % (3345123)Peak memory usage: 88 MB
% 4.61/1.41 % (3345123)Instructions burned: 29 (million)
% 4.61/1.41 % (3345071)Instruction limit reached!
% 4.61/1.41 % (3345071)------------------------------
% 4.61/1.41 % (3345071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.41 % (3345071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345071)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345071)Termination reason: Instruction limit
% 4.61/1.41 % (3345071)Termination phase: Saturation
% 4.61/1.41 % (3345071)Time elapsed: 0.172 s
% 4.61/1.41 % (3345071)Peak memory usage: 117 MB
% 4.61/1.41 % (3345071)Instructions burned: 201 (million)
% 4.61/1.41 % (3345133)Instruction limit reached!
% 4.61/1.41 % (3345133)------------------------------
% 4.61/1.41 % (3345133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.41 % (3345133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345133)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345133)Termination reason: Instruction limit
% 4.61/1.41 % (3345133)Termination phase: Saturation
% 4.61/1.41 % (3345133)Time elapsed: 0.009 s
% 4.61/1.41 % (3345133)Peak memory usage: 88 MB
% 4.61/1.41 % (3345133)Instructions burned: 16 (million)
% 4.61/1.41 % (3345144)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=352218907:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.61/1.41 % (3345139)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=735656458:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.61/1.41 % (3345152)Instruction limit reached!
% 4.61/1.41 % (3345152)------------------------------
% 4.61/1.41 % (3345152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.61/1.41 % (3345152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.61/1.41 % (3345152)CaDiCaL version: 2.1.3
% 4.61/1.41 % (3345152)Termination reason: Instruction limit
% 4.61/1.41 % (3345152)Termination phase: Saturation
% 4.61/1.41 % (3345152)Time elapsed: 0.031 s
% 4.61/1.41 % (3345152)Peak memory usage: 89 MB
% 4.61/1.41 % (3345152)Instructions burned: 86 (million)
% 4.61/1.41 % (3345144)Refutation not found, incomplete strategy
% 4.61/1.41 % (3345144)------------------------------
% 5.56/1.57 % (3345144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345144)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345144)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.57 % (3345144)Time elapsed: 0.007 s
% 5.56/1.57 % (3345144)Peak memory usage: 89 MB
% 5.56/1.57 % (3345144)Instructions burned: 11 (million)
% 5.56/1.57 % (3345139)Instruction limit reached!
% 5.56/1.57 % (3345139)------------------------------
% 5.56/1.57 % (3345139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345139)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345139)Termination reason: Instruction limit
% 5.56/1.57 % (3345139)Termination phase: Saturation
% 5.56/1.57 % (3345139)Time elapsed: 0.018 s
% 5.56/1.57 % (3345139)Peak memory usage: 89 MB
% 5.56/1.57 % (3345139)Instructions burned: 24 (million)
% 5.56/1.57 % (3345196)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2020622762:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.56/1.57 % (3345188)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4263588106:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.56/1.57 % (3345189)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=694148069:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.56/1.57 % (3345187)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2352586447:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.56/1.57 % (3345187)Instruction limit reached!
% 5.56/1.57 % (3345187)------------------------------
% 5.56/1.57 % (3345187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345187)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345187)Termination reason: Instruction limit
% 5.56/1.57 % (3345187)Termination phase: Preprocessing 2
% 5.56/1.57 % (3345187)Time elapsed: 0.002 s
% 5.56/1.57 % (3345187)Peak memory usage: 86 MB
% 5.56/1.57 % (3345187)Instructions burned: 3 (million)
% 5.56/1.57 % (3345188)Refutation not found, incomplete strategy
% 5.56/1.57 % (3345188)------------------------------
% 5.56/1.57 % (3345188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345188)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345188)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.57 % (3345188)Time elapsed: 0.002 s
% 5.56/1.57 % (3345188)Peak memory usage: 89 MB
% 5.56/1.57 % (3345188)Instructions burned: 2 (million)
% 5.56/1.57 % (3345189)Instruction limit reached!
% 5.56/1.57 % (3345189)------------------------------
% 5.56/1.57 % (3345189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345189)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345189)Termination reason: Instruction limit
% 5.56/1.57 % (3345189)Termination phase: Property scanning
% 5.56/1.57 % (3345189)Time elapsed: 0.003 s
% 5.56/1.57 % (3345189)Peak memory usage: 86 MB
% 5.56/1.57 % (3345189)Instructions burned: 5 (million)
% 5.56/1.57 % (3345196)Instruction limit reached!
% 5.56/1.57 % (3345196)------------------------------
% 5.56/1.57 % (3345196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.57 % (3345196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.57 % (3345196)CaDiCaL version: 2.1.3
% 5.56/1.57 % (3345196)Termination reason: Instruction limit
% 5.56/1.57 % (3345196)Termination phase: Saturation
% 5.56/1.57 % (3345196)Time elapsed: 0.052 s
% 5.56/1.57 % (3345196)Peak memory usage: 134 MB
% 5.56/1.57 % (3345196)Instructions burned: 66 (million)
% 5.56/1.57 % (3345204)lrs+10_1_thi=all:si=on:fd=off:random_seed=2735223984:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.56/1.57 % (3345122)------------------------------
% 5.56/1.57 % (3345122)------------------------------
% 5.56/1.57 % (3345204)Instruction limit reached!
% 5.56/1.57 % (3345204)------------------------------
% 5.56/1.57 % (3345204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345204)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345204)Termination reason: Instruction limit
% 7.19/1.84 % (3345204)Termination phase: Saturation
% 7.19/1.84 % (3345204)Time elapsed: 0.059 s
% 7.19/1.84 % (3345204)Peak memory usage: 116 MB
% 7.19/1.84 % (3345204)Instructions burned: 53 (million)
% 7.19/1.84 % (3345144)------------------------------
% 7.19/1.84 % (3345144)------------------------------
% 7.19/1.84 % (3345209)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=3581083358:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 7.19/1.84 % (3345209)Instruction limit reached!
% 7.19/1.84 % (3345209)------------------------------
% 7.19/1.84 % (3345209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345209)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345209)Termination reason: Instruction limit
% 7.19/1.84 % (3345209)Termination phase: Property scanning
% 7.19/1.84 % (3345209)Time elapsed: 0.005 s
% 7.19/1.84 % (3345209)Peak memory usage: 87 MB
% 7.19/1.84 % (3345209)Instructions burned: 9 (million)
% 7.19/1.84 % (3345210)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2791457650:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 7.19/1.84 % (3345216)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1352075166:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.19/1.84 % (3345210)Instruction limit reached!
% 7.19/1.84 % (3345210)------------------------------
% 7.19/1.84 % (3345210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345210)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345210)Termination reason: Instruction limit
% 7.19/1.84 % (3345210)Termination phase: Preprocessing 2
% 7.19/1.84 % (3345210)Time elapsed: 0.002 s
% 7.19/1.84 % (3345210)Peak memory usage: 85 MB
% 7.19/1.84 % (3345210)Instructions burned: 3 (million)
% 7.19/1.84 % (3345216)Instruction limit reached!
% 7.19/1.84 % (3345216)------------------------------
% 7.19/1.84 % (3345216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345216)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345216)Termination reason: Instruction limit
% 7.19/1.84 % (3345216)Termination phase: Preprocessing 2
% 7.19/1.84 % (3345216)Time elapsed: 0.001 s
% 7.19/1.84 % (3345216)Peak memory usage: 86 MB
% 7.19/1.84 % (3345216)Instructions burned: 3 (million)
% 7.19/1.84 % (3345188)------------------------------
% 7.19/1.84 % (3345188)------------------------------
% 7.19/1.84 % (3345267)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4160278314:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 7.19/1.84 % (3345241)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2134153316:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.19/1.84 % (3345267)Instruction limit reached!
% 7.19/1.84 % (3345267)------------------------------
% 7.19/1.84 % (3345267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345267)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345267)Termination reason: Instruction limit
% 7.19/1.84 % (3345267)Termination phase: Preprocessing 1
% 7.19/1.84 % (3345267)Time elapsed: 0.001 s
% 7.19/1.84 % (3345267)Peak memory usage: 85 MB
% 7.19/1.84 % (3345267)Instructions burned: 3 (million)
% 7.19/1.84 % (3345253)dis+10_1_si=on:random_seed=3536816181:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.19/1.84 % (3345253)Instruction limit reached!
% 7.19/1.84 % (3345253)------------------------------
% 7.19/1.84 % (3345253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.19/1.84 % (3345253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.84 % (3345253)CaDiCaL version: 2.1.3
% 7.19/1.84 % (3345253)Termination reason: Instruction limit
% 7.19/1.84 % (3345253)Termination phase: Saturation
% 7.19/1.84 % (3345253)Time elapsed: 0.006 s
% 7.19/1.84 % (3345253)Peak memory usage: 88 MB
% 7.19/1.84 % (3345253)Instructions burned: 10 (million)
% 10.00/2.08 % (3345259)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=337288255:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 10.00/2.08 % (3345259)Refutation not found, incomplete strategy
% 10.00/2.08 % (3345259)------------------------------
% 10.00/2.08 % (3345259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345259)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345259)Termination reason: Refutation not found, incomplete strategy
% 10.00/2.08 % (3345259)Time elapsed: 0.008 s
% 10.00/2.08 % (3345259)Peak memory usage: 88 MB
% 10.00/2.08 % (3345259)Instructions burned: 11 (million)
% 10.00/2.08 % (3345262)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4202726788:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi)
% 10.00/2.08 % (3345268)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=64771738:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.00/2.08 % (3345262)Instruction limit reached!
% 10.00/2.08 % (3345262)------------------------------
% 10.00/2.08 % (3345262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345262)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345262)Termination reason: Instruction limit
% 10.00/2.08 % (3345262)Termination phase: Saturation
% 10.00/2.08 % (3345262)Time elapsed: 0.028 s
% 10.00/2.08 % (3345262)Peak memory usage: 89 MB
% 10.00/2.08 % (3345262)Instructions burned: 36 (million)
% 10.00/2.08 % (3345268)Instruction limit reached!
% 10.00/2.08 % (3345268)------------------------------
% 10.00/2.08 % (3345268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345268)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345268)Termination reason: Instruction limit
% 10.00/2.08 % (3345268)Termination phase: Saturation
% 10.00/2.08 % (3345268)Time elapsed: 0.005 s
% 10.00/2.08 % (3345268)Peak memory usage: 87 MB
% 10.00/2.08 % (3345268)Instructions burned: 8 (million)
% 10.00/2.08 % (3345241)Instruction limit reached!
% 10.00/2.08 % (3345241)------------------------------
% 10.00/2.08 % (3345241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345241)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345241)Termination reason: Instruction limit
% 10.00/2.08 % (3345241)Termination phase: Saturation
% 10.00/2.08 % (3345241)Time elapsed: 0.104 s
% 10.00/2.08 % (3345241)Peak memory usage: 117 MB
% 10.00/2.08 % (3345241)Instructions burned: 128 (million)
% 10.00/2.08 % (3345273)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2223062903:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 10.00/2.08 % (3345273)Instruction limit reached!
% 10.00/2.08 % (3345273)------------------------------
% 10.00/2.08 % (3345273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345273)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345273)Termination reason: Instruction limit
% 10.00/2.08 % (3345273)Termination phase: Saturation
% 10.00/2.08 % (3345273)Time elapsed: 0.017 s
% 10.00/2.08 % (3345273)Peak memory usage: 111 MB
% 10.00/2.08 % (3345273)Instructions burned: 14 (million)
% 10.00/2.08 % (3345271)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1109274950:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi)
% 10.00/2.08 % (3345271)Refutation not found, incomplete strategy
% 10.00/2.08 % (3345271)------------------------------
% 10.00/2.08 % (3345271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.08 % (3345271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.08 % (3345271)CaDiCaL version: 2.1.3
% 10.00/2.08 % (3345271)Termination reason: Refutation not found, incomplete strategy
% 10.00/2.08 % (3345271)Time elapsed: 0.007 s
% 10.00/2.08 % (3345271)Peak memory usage: 88 MB
% 10.00/2.08 % (3345271)Instructions burned: 9 (million)
% 10.00/2.08 % (3345274)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3279066918:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 11.10/2.37 % (3345274)Refutation not found, incomplete strategy
% 11.10/2.37 % (3345274)------------------------------
% 11.10/2.37 % (3345274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.37 % (3345274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.37 % (3345274)CaDiCaL version: 2.1.3
% 11.10/2.37 % (3345274)Termination reason: Refutation not found, incomplete strategy
% 11.10/2.37 % (3345274)Time elapsed: 0.029 s
% 11.10/2.37 % (3345274)Peak memory usage: 112 MB
% 11.10/2.37 % (3345274)Instructions burned: 8 (million)
% 11.10/2.37 % (3345279)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3800014291:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 11.10/2.37 % (3345278)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1387080191:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.10/2.37 % (3345278)Instruction limit reached!
% 11.10/2.37 % (3345278)------------------------------
% 11.10/2.37 % (3345278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.37 % (3345278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.37 % (3345278)CaDiCaL version: 2.1.3
% 11.10/2.37 % (3345278)Termination reason: Instruction limit
% 11.10/2.37 % (3345278)Termination phase: Saturation
% 11.10/2.37 % (3345278)Time elapsed: 0.007 s
% 11.10/2.37 % (3345278)Peak memory usage: 88 MB
% 11.10/2.37 % (3345278)Instructions burned: 11 (million)
% 11.10/2.37 % (3345282)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=1413162396:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 11.10/2.37 % (3345281)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=2147218461:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi)
% 11.10/2.37 % (3345259)------------------------------
% 11.10/2.37 % (3345259)------------------------------
% 11.10/2.37 % (3345281)Instruction limit reached!
% 11.10/2.37 % (3345281)------------------------------
% 11.10/2.37 % (3345281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.37 % (3345281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.37 % (3345281)CaDiCaL version: 2.1.3
% 11.10/2.37 % (3345281)Termination reason: Instruction limit
% 11.10/2.37 % (3345281)Termination phase: Saturation
% 11.10/2.37 % (3345281)Time elapsed: 0.045 s
% 11.10/2.37 % (3345281)Peak memory usage: 90 MB
% 11.10/2.37 % (3345281)Instructions burned: 76 (million)
% 11.10/2.37 % (3345279)Instruction limit reached!
% 11.10/2.37 % (3345279)------------------------------
% 11.10/2.37 % (3345279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.37 % (3345279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.37 % (3345279)CaDiCaL version: 2.1.3
% 11.10/2.37 % (3345279)Termination reason: Instruction limit
% 11.10/2.37 % (3345279)Termination phase: Saturation
% 11.10/2.37 % (3345279)Time elapsed: 0.095 s
% 11.10/2.37 % (3345279)Peak memory usage: 133 MB
% 11.10/2.37 % (3345279)Instructions burned: 72 (million)
% 11.10/2.37 % (3345282)Instruction limit reached!
% 11.10/2.37 % (3345282)------------------------------
% 11.10/2.37 % (3345282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.37 % (3345282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.37 % (3345282)CaDiCaL version: 2.1.3
% 11.10/2.37 % (3345282)Termination reason: Instruction limit
% 11.10/2.37 % (3345282)Termination phase: Saturation
% 11.10/2.37 % (3345282)Time elapsed: 0.101 s
% 11.10/2.37 % (3345282)Peak memory usage: 90 MB
% 11.10/2.37 % (3345282)Instructions burned: 294 (million)
% 11.10/2.37 % (3345287)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2680026536:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 11.10/2.37 % (3345271)------------------------------
% 11.10/2.37 % (3345271)------------------------------
% 11.10/2.37 % (3345290)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3654443427:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.10/2.37 % (3345274)------------------------------
% 12.88/2.65 % (3345274)------------------------------
% 12.88/2.65 % (3345293)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3927345282:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 12.88/2.65 % (3345292)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=551112693:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 12.88/2.65 % (3345291)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1205362026:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 12.88/2.65 % (3345292)Refutation not found, incomplete strategy
% 12.88/2.65 % (3345292)------------------------------
% 12.88/2.65 % (3345292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345292)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345292)Termination reason: Refutation not found, incomplete strategy
% 12.88/2.65 % (3345292)Time elapsed: 0.009 s
% 12.88/2.65 % (3345292)Peak memory usage: 89 MB
% 12.88/2.65 % (3345292)Instructions burned: 13 (million)
% 12.88/2.65 % (3345287)Instruction limit reached!
% 12.88/2.65 % (3345287)------------------------------
% 12.88/2.65 % (3345287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345287)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345287)Termination reason: Instruction limit
% 12.88/2.65 % (3345287)Termination phase: Saturation
% 12.88/2.65 % (3345287)Time elapsed: 0.096 s
% 12.88/2.65 % (3345287)Peak memory usage: 117 MB
% 12.88/2.65 % (3345287)Instructions burned: 131 (million)
% 12.88/2.65 % (3345291)Instruction limit reached!
% 12.88/2.65 % (3345291)------------------------------
% 12.88/2.65 % (3345291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345291)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345291)Termination reason: Instruction limit
% 12.88/2.65 % (3345291)Termination phase: Saturation
% 12.88/2.65 % (3345291)Time elapsed: 0.067 s
% 12.88/2.65 % (3345291)Peak memory usage: 133 MB
% 12.88/2.65 % (3345291)Instructions burned: 41 (million)
% 12.88/2.65 % (3345290)Instruction limit reached!
% 12.88/2.65 % (3345290)------------------------------
% 12.88/2.65 % (3345290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345290)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345290)Termination reason: Instruction limit
% 12.88/2.65 % (3345290)Termination phase: Saturation
% 12.88/2.65 % (3345290)Time elapsed: 0.134 s
% 12.88/2.65 % (3345290)Peak memory usage: 134 MB
% 12.88/2.65 % (3345290)Instructions burned: 131 (million)
% 12.88/2.65 % (3345295)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3222861250:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 12.88/2.65 % (3345297)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=3626292534:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi)
% 12.88/2.65 % (3345301)dis+10_1_si=on:random_seed=1057889022:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 12.88/2.65 % (3345297)Refutation not found, incomplete strategy
% 12.88/2.65 % (3345297)------------------------------
% 12.88/2.65 % (3345297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345297)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345297)Termination reason: Refutation not found, incomplete strategy
% 12.88/2.65 % (3345297)Time elapsed: 0.030 s
% 12.88/2.65 % (3345297)Peak memory usage: 115 MB
% 12.88/2.65 % (3345297)Instructions burned: 10 (million)
% 12.88/2.65 % (3345295)Instruction limit reached!
% 12.88/2.65 % (3345295)------------------------------
% 12.88/2.65 % (3345295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.65 % (3345295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.65 % (3345295)CaDiCaL version: 2.1.3
% 12.88/2.65 % (3345295)Termination reason: Instruction limit
% 12.88/2.65 % (3345295)Termination phase: Saturation
% 12.88/2.65 % (3345295)Time elapsed: 0.113 s
% 14.90/2.92 % (3345295)Peak memory usage: 118 MB
% 14.90/2.92 % (3345295)Instructions burned: 131 (million)
% 14.90/2.92 % (3345302)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1293543692:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 14.90/2.92 % (3345293)Instruction limit reached!
% 14.90/2.92 % (3345293)------------------------------
% 14.90/2.92 % (3345293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345293)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345293)Termination reason: Instruction limit
% 14.90/2.92 % (3345293)Termination phase: Saturation
% 14.90/2.92 % (3345293)Time elapsed: 0.250 s
% 14.90/2.92 % (3345293)Peak memory usage: 140 MB
% 14.90/2.92 % (3345293)Instructions burned: 600 (million)
% 14.90/2.92 % (3345292)------------------------------
% 14.90/2.92 % (3345292)------------------------------
% 14.90/2.92 % (3345304)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3605166037:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 14.90/2.92 % (3345304)Instruction limit reached!
% 14.90/2.92 % (3345304)------------------------------
% 14.90/2.92 % (3345304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345304)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345304)Termination reason: Instruction limit
% 14.90/2.92 % (3345304)Termination phase: Saturation
% 14.90/2.92 % (3345304)Time elapsed: 0.095 s
% 14.90/2.92 % (3345304)Peak memory usage: 90 MB
% 14.90/2.92 % (3345304)Instructions burned: 142 (million)
% 14.90/2.92 % (3345309)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1993206477:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi)
% 14.90/2.92 % (3345308)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=420937163:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi)
% 14.90/2.92 % (3345308)Refutation not found, incomplete strategy
% 14.90/2.92 % (3345308)------------------------------
% 14.90/2.92 % (3345308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345308)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345308)Termination reason: Refutation not found, incomplete strategy
% 14.90/2.92 % (3345308)Time elapsed: 0.034 s
% 14.90/2.92 % (3345308)Peak memory usage: 115 MB
% 14.90/2.92 % (3345308)Instructions burned: 15 (million)
% 14.90/2.92 % (3345309)Instruction limit reached!
% 14.90/2.92 % (3345309)------------------------------
% 14.90/2.92 % (3345309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345309)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345309)Termination reason: Instruction limit
% 14.90/2.92 % (3345309)Termination phase: Saturation
% 14.90/2.92 % (3345309)Time elapsed: 0.039 s
% 14.90/2.92 % (3345309)Peak memory usage: 89 MB
% 14.90/2.92 % (3345309)Instructions burned: 124 (million)
% 14.90/2.92 % (3345310)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=3318499364:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi)
% 14.90/2.92 % (3345297)------------------------------
% 14.90/2.92 % (3345297)------------------------------
% 14.90/2.92 % (3345302)Instruction limit reached!
% 14.90/2.92 % (3345302)------------------------------
% 14.90/2.92 % (3345302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345302)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345302)Termination reason: Instruction limit
% 14.90/2.92 % (3345302)Termination phase: Saturation
% 14.90/2.92 % (3345302)Time elapsed: 0.212 s
% 14.90/2.92 % (3345302)Peak memory usage: 95 MB
% 14.90/2.92 % (3345302)Instructions burned: 384 (million)
% 14.90/2.92 % (3345310)Instruction limit reached!
% 14.90/2.92 % (3345310)------------------------------
% 14.90/2.92 % (3345310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/2.92 % (3345310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/2.92 % (3345310)CaDiCaL version: 2.1.3
% 14.90/2.92 % (3345310)Termination reason: Instruction limit
% 18.28/3.31 % (3345310)Termination phase: Saturation
% 18.28/3.31 % (3345310)Time elapsed: 0.106 s
% 18.28/3.31 % (3345310)Peak memory usage: 117 MB
% 18.28/3.31 % (3345310)Instructions burned: 129 (million)
% 18.28/3.31 % (3345315)dis+1010_1_to=kbo:si=on:random_seed=1941761618:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 18.28/3.31 % (3345313)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=1969712495:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi)
% 18.28/3.31 % (3345313)Instruction limit reached!
% 18.28/3.31 % (3345313)------------------------------
% 18.28/3.31 % (3345313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.31 % (3345313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.31 % (3345313)CaDiCaL version: 2.1.3
% 18.28/3.31 % (3345313)Termination reason: Instruction limit
% 18.28/3.31 % (3345313)Termination phase: Saturation
% 18.28/3.31 % (3345313)Time elapsed: 0.046 s
% 18.28/3.31 % (3345313)Peak memory usage: 116 MB
% 18.28/3.31 % (3345313)Instructions burned: 39 (million)
% 18.28/3.31 % (3345315)Instruction limit reached!
% 18.28/3.31 % (3345315)------------------------------
% 18.28/3.31 % (3345315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.31 % (3345315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.31 % (3345315)CaDiCaL version: 2.1.3
% 18.28/3.31 % (3345315)Termination reason: Instruction limit
% 18.28/3.31 % (3345315)Termination phase: Saturation
% 18.28/3.31 % (3345315)Time elapsed: 0.069 s
% 18.28/3.31 % (3345315)Peak memory usage: 92 MB
% 18.28/3.31 % (3345315)Instructions burned: 176 (million)
% 18.28/3.31 % (3345317)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2974776392:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi)
% 18.28/3.31 % (3345318)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1332809227:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi)
% 18.28/3.31 % (3345308)------------------------------
% 18.28/3.31 % (3345308)------------------------------
% 18.28/3.31 % (3345321)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1427368044:thitd=on:i=215:nm=0:rtra=on:ev=force_2982 on theBenchmark for (2982ds/215Mi)
% 18.28/3.31 % (3345323)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1754729790:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi)
% 18.28/3.31 % (3345322)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1661870354:i=349:rtra=on_2982 on theBenchmark for (2982ds/349Mi)
% 18.28/3.31 % (3345322)Refutation not found, incomplete strategy
% 18.28/3.31 % (3345322)------------------------------
% 18.28/3.31 % (3345322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.31 % (3345322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.31 % (3345322)CaDiCaL version: 2.1.3
% 18.28/3.31 % (3345322)Termination reason: Refutation not found, incomplete strategy
% 18.28/3.31 % (3345322)Time elapsed: 0.040 s
% 18.28/3.31 % (3345322)Peak memory usage: 116 MB
% 18.28/3.31 % (3345322)Instructions burned: 27 (million)
% 18.28/3.31 % (3345301)Instruction limit reached!
% 18.28/3.31 % (3345301)------------------------------
% 18.28/3.31 % (3345301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.31 % (3345301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.31 % (3345301)CaDiCaL version: 2.1.3
% 18.28/3.31 % (3345301)Termination reason: Instruction limit
% 18.28/3.31 % (3345301)Termination phase: Saturation
% 18.28/3.31 % (3345301)Time elapsed: 0.608 s
% 18.28/3.31 % (3345301)Peak memory usage: 94 MB
% 18.28/3.31 % (3345301)Instructions burned: 1002 (million)
% 18.28/3.31 % (3345323)Instruction limit reached!
% 18.28/3.31 % (3345323)------------------------------
% 18.28/3.31 % (3345323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.31 % (3345323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.31 % (3345323)CaDiCaL version: 2.1.3
% 18.28/3.31 % (3345323)Termination reason: Instruction limit
% 18.28/3.31 % (3345323)Termination phase: Saturation
% 18.28/3.31 % (3345323)Time elapsed: 0.087 s
% 18.28/3.31 % (3345323)Peak memory usage: 90 MB
% 18.28/3.31 % (3345323)Instructions burned: 295 (million)
% 18.98/3.51 % (3345326)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=743699893:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi)
% 18.98/3.51 % (3345321)Instruction limit reached!
% 18.98/3.51 % (3345321)------------------------------
% 18.98/3.51 % (3345321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345321)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345321)Termination reason: Instruction limit
% 18.98/3.51 % (3345321)Termination phase: Saturation
% 18.98/3.51 % (3345321)Time elapsed: 0.171 s
% 18.98/3.51 % (3345321)Peak memory usage: 136 MB
% 18.98/3.51 % (3345321)Instructions burned: 216 (million)
% 18.98/3.51 % (3345317)Instruction limit reached!
% 18.98/3.51 % (3345317)------------------------------
% 18.98/3.51 % (3345317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345317)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345317)Termination reason: Instruction limit
% 18.98/3.51 % (3345317)Termination phase: Saturation
% 18.98/3.51 % (3345317)Time elapsed: 0.252 s
% 18.98/3.51 % (3345317)Peak memory usage: 118 MB
% 18.98/3.51 % (3345317)Instructions burned: 329 (million)
% 18.98/3.51 % (3345331)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2482207310:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi)
% 18.98/3.51 % (3345331)Refutation not found, incomplete strategy
% 18.98/3.51 % (3345331)------------------------------
% 18.98/3.51 % (3345331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345331)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345331)Termination reason: Refutation not found, incomplete strategy
% 18.98/3.51 % (3345331)Time elapsed: 0.002 s
% 18.98/3.51 % (3345331)Peak memory usage: 88 MB
% 18.98/3.51 % (3345331)Instructions burned: 4 (million)
% 18.98/3.51 % (3345330)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3410460330:i=281:gtgl=2:rtra=on:gtg=all_2980 on theBenchmark for (2980ds/281Mi)
% 18.98/3.51 % (3345318)Instruction limit reached!
% 18.98/3.51 % (3345318)------------------------------
% 18.98/3.51 % (3345318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345318)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345318)Termination reason: Instruction limit
% 18.98/3.51 % (3345318)Termination phase: Saturation
% 18.98/3.51 % (3345318)Time elapsed: 0.374 s
% 18.98/3.51 % (3345318)Peak memory usage: 136 MB
% 18.98/3.51 % (3345318)Instructions burned: 483 (million)
% 18.98/3.51 % (3345333)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2480280047:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2979 on theBenchmark for (2979ds/321Mi)
% 18.98/3.51 % (3345322)------------------------------
% 18.98/3.51 % (3345322)------------------------------
% 18.98/3.51 % (3345334)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3191896849:i=416:rtra=on:gtg=position:ss=axioms_2979 on theBenchmark for (2979ds/416Mi)
% 18.98/3.51 % (3345334)Refutation not found, incomplete strategy
% 18.98/3.51 % (3345334)------------------------------
% 18.98/3.51 % (3345334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345334)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345334)Termination reason: Refutation not found, incomplete strategy
% 18.98/3.51 % (3345334)Time elapsed: 0.028 s
% 18.98/3.51 % (3345334)Peak memory usage: 112 MB
% 18.98/3.51 % (3345334)Instructions burned: 8 (million)
% 18.98/3.51 % (3345326)Instruction limit reached!
% 18.98/3.51 % (3345326)------------------------------
% 18.98/3.51 % (3345326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.51 % (3345326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.51 % (3345326)CaDiCaL version: 2.1.3
% 18.98/3.51 % (3345326)Termination reason: Instruction limit
% 18.98/3.51 % (3345326)Termination phase: Saturation
% 18.98/3.51 % (3345326)Time elapsed: 0.228 s
% 18.98/3.51 % (3345326)Peak memory usage: 118 MB
% 18.98/3.51 % (3345326)Instructions burned: 328 (million)
% 18.98/3.51 % (3345331)------------------------------
% 21.37/3.88 % (3345331)------------------------------
% 21.37/3.88 % (3345337)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1682665370:i=471:thf=on:kws=precedence:rtra=on_2978 on theBenchmark for (2978ds/471Mi)
% 21.37/3.88 % (3345330)Instruction limit reached!
% 21.37/3.88 % (3345330)------------------------------
% 21.37/3.88 % (3345330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.88 % (3345330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.88 % (3345330)CaDiCaL version: 2.1.3
% 21.37/3.88 % (3345330)Termination reason: Instruction limit
% 21.37/3.88 % (3345330)Termination phase: Saturation
% 21.37/3.88 % (3345330)Time elapsed: 0.197 s
% 21.37/3.88 % (3345330)Peak memory usage: 117 MB
% 21.37/3.88 % (3345330)Instructions burned: 282 (million)
% 21.37/3.88 % (3345339)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=105194278:avsq=on:i=276:avsqr=1,2:rtra=on_2978 on theBenchmark for (2978ds/276Mi)
% 21.37/3.88 % (3345333)Instruction limit reached!
% 21.37/3.88 % (3345333)------------------------------
% 21.37/3.88 % (3345333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.88 % (3345333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.88 % (3345333)CaDiCaL version: 2.1.3
% 21.37/3.88 % (3345333)Termination reason: Instruction limit
% 21.37/3.88 % (3345333)Termination phase: Saturation
% 21.37/3.88 % (3345333)Time elapsed: 0.197 s
% 21.37/3.88 % (3345333)Peak memory usage: 114 MB
% 21.37/3.88 % (3345333)Instructions burned: 323 (million)
% 21.37/3.88 % (3345342)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=376648205:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/387Mi)
% 21.37/3.88 % (3345341)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=710255446:i=375:kws=inv_arity_squared:rtra=on_2977 on theBenchmark for (2977ds/375Mi)
% 21.37/3.88 % (3345334)------------------------------
% 21.37/3.88 % (3345334)------------------------------
% 21.37/3.88 % (3345344)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2693739726:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2976 on theBenchmark for (2976ds/513Mi)
% 21.37/3.88 % (3345346)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1405205517:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi)
% 21.37/3.88 % (3345342)Instruction limit reached!
% 21.37/3.88 % (3345342)------------------------------
% 21.37/3.88 % (3345342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.88 % (3345342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.88 % (3345342)CaDiCaL version: 2.1.3
% 21.37/3.88 % (3345342)Termination reason: Instruction limit
% 21.37/3.88 % (3345342)Termination phase: Saturation
% 21.37/3.88 % (3345342)Time elapsed: 0.162 s
% 21.37/3.88 % (3345342)Peak memory usage: 120 MB
% 21.37/3.88 % (3345342)Instructions burned: 387 (million)
% 21.37/3.88 % (3345339)Instruction limit reached!
% 21.37/3.88 % (3345339)------------------------------
% 21.37/3.88 % (3345339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.88 % (3345339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.88 % (3345339)CaDiCaL version: 2.1.3
% 21.37/3.88 % (3345339)Termination reason: Instruction limit
% 21.37/3.88 % (3345339)Termination phase: Saturation
% 21.37/3.88 % (3345339)Time elapsed: 0.246 s
% 21.37/3.88 % (3345339)Peak memory usage: 134 MB
% 21.37/3.88 % (3345339)Instructions burned: 277 (million)
% 21.37/3.88 % (3345337)Instruction limit reached!
% 21.37/3.88 % (3345337)------------------------------
% 21.37/3.88 % (3345337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.88 % (3345337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.88 % (3345337)CaDiCaL version: 2.1.3
% 21.37/3.88 % (3345337)Termination reason: Instruction limit
% 21.37/3.88 % (3345337)Termination phase: Saturation
% 21.37/3.88 % (3345337)Time elapsed: 0.279 s
% 21.37/3.88 % (3345337)Peak memory usage: 118 MB
% 21.37/3.88 % (3345337)Instructions burned: 471 (million)
% 21.37/3.88 % (3345341)Instruction limit reached!
% 21.37/3.88 % (3345341)------------------------------
% 21.37/3.88 % (3345341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345341)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345341)Termination reason: Instruction limit
% 25.47/4.35 % (3345341)Termination phase: Saturation
% 25.47/4.35 % (3345341)Time elapsed: 0.242 s
% 25.47/4.35 % (3345341)Peak memory usage: 120 MB
% 25.47/4.35 % (3345341)Instructions burned: 376 (million)
% 25.47/4.35 % (3345349)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=881473443:i=359:rtra=on:gtg=exists_top:ss=axioms_2975 on theBenchmark for (2975ds/359Mi)
% 25.47/4.35 % (3345349)Refutation not found, incomplete strategy
% 25.47/4.35 % (3345349)------------------------------
% 25.47/4.35 % (3345349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345349)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345349)Termination reason: Refutation not found, incomplete strategy
% 25.47/4.35 % (3345349)Time elapsed: 0.004 s
% 25.47/4.35 % (3345349)Peak memory usage: 89 MB
% 25.47/4.35 % (3345349)Instructions burned: 5 (million)
% 25.47/4.35 % (3345352)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=4166269339:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2974 on theBenchmark for (2974ds/341Mi)
% 25.47/4.35 % (3345354)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=435558860:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/235Mi)
% 25.47/4.35 % (3345353)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=910073007:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/261Mi)
% 25.47/4.35 % (3345353)Refutation not found, incomplete strategy
% 25.47/4.35 % (3345353)------------------------------
% 25.47/4.35 % (3345353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345353)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345353)Termination reason: Refutation not found, incomplete strategy
% 25.47/4.35 % (3345353)Time elapsed: 0.028 s
% 25.47/4.35 % (3345353)Peak memory usage: 111 MB
% 25.47/4.35 % (3345353)Instructions burned: 7 (million)
% 25.47/4.35 % (3345354)Refutation not found, incomplete strategy
% 25.47/4.35 % (3345354)------------------------------
% 25.47/4.35 % (3345354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345354)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345354)Termination reason: Refutation not found, incomplete strategy
% 25.47/4.35 % (3345354)Time elapsed: 0.030 s
% 25.47/4.35 % (3345354)Peak memory usage: 115 MB
% 25.47/4.35 % (3345354)Instructions burned: 10 (million)
% 25.47/4.35 % (3345356)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=394119638:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2973 on theBenchmark for (2973ds/273Mi)
% 25.47/4.35 % (3345346)Instruction limit reached!
% 25.47/4.35 % (3345346)------------------------------
% 25.47/4.35 % (3345346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345346)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345346)Termination reason: Instruction limit
% 25.47/4.35 % (3345346)Termination phase: Saturation
% 25.47/4.35 % (3345346)Time elapsed: 0.264 s
% 25.47/4.35 % (3345346)Peak memory usage: 135 MB
% 25.47/4.35 % (3345346)Instructions burned: 334 (million)
% 25.47/4.35 % (3345352)Instruction limit reached!
% 25.47/4.35 % (3345352)------------------------------
% 25.47/4.35 % (3345352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/4.35 % (3345352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/4.35 % (3345352)CaDiCaL version: 2.1.3
% 25.47/4.35 % (3345352)Termination reason: Instruction limit
% 25.47/4.35 % (3345352)Termination phase: Saturation
% 25.47/4.35 % (3345352)Time elapsed: 0.135 s
% 25.47/4.35 % (3345352)Peak memory usage: 120 MB
% 25.47/4.35 % (3345352)Instructions burned: 343 (million)
% 25.47/4.35 % (3345344)Instruction limit reached!
% 25.47/4.35 % (3345344)------------------------------
% 25.47/4.35 % (3345344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.91 % (3345344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.91 % (3345344)CaDiCaL version: 2.1.3
% 28.62/4.91 % (3345344)Termination reason: Instruction limit
% 28.62/4.91 % (3345344)Termination phase: Saturation
% 28.62/4.91 % (3345344)Time elapsed: 0.330 s
% 28.62/4.91 % (3345344)Peak memory usage: 93 MB
% 28.62/4.91 % (3345344)Instructions burned: 514 (million)
% 28.62/4.91 % (3345349)------------------------------
% 28.62/4.91 % (3345349)------------------------------
% 28.62/4.91 % (3345362)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2813327593:i=4428:doe=on:fsr=off:rtra=on_2971 on theBenchmark for (2971ds/4428Mi)
% 28.62/4.91 % (3345361)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2772679362:i=146:doe=on:rtra=on_2971 on theBenchmark for (2971ds/146Mi)
% 28.62/4.91 % (3345356)Instruction limit reached!
% 28.62/4.91 % (3345356)------------------------------
% 28.62/4.91 % (3345356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.91 % (3345356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.91 % (3345356)CaDiCaL version: 2.1.3
% 28.62/4.91 % (3345356)Termination reason: Instruction limit
% 28.62/4.91 % (3345356)Termination phase: Saturation
% 28.62/4.91 % (3345356)Time elapsed: 0.186 s
% 28.62/4.91 % (3345356)Peak memory usage: 91 MB
% 28.62/4.91 % (3345356)Instructions burned: 273 (million)
% 28.62/4.91 % (3345363)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=236157235:avsq=on:i=276:avsqr=1,2:rtra=on_2971 on theBenchmark for (2971ds/276Mi)
% 28.62/4.91 % (3345354)------------------------------
% 28.62/4.91 % (3345354)------------------------------
% 28.62/4.91 % (3345353)------------------------------
% 28.62/4.91 % (3345353)------------------------------
% 28.62/4.91 % (3345361)Instruction limit reached!
% 28.62/4.91 % (3345361)------------------------------
% 28.62/4.91 % (3345361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.91 % (3345361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.91 % (3345361)CaDiCaL version: 2.1.3
% 28.62/4.91 % (3345361)Termination reason: Instruction limit
% 28.62/4.91 % (3345361)Termination phase: Saturation
% 28.62/4.91 % (3345361)Time elapsed: 0.097 s
% 28.62/4.91 % (3345361)Peak memory usage: 90 MB
% 28.62/4.91 % (3345361)Instructions burned: 147 (million)
% 28.62/4.91 % (3345364)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=704732383:i=1052:rtra=on_2970 on theBenchmark for (2970ds/1052Mi)
% 28.62/4.91 % (3345367)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=19010230:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2970 on theBenchmark for (2970ds/655Mi)
% 28.62/4.91 % (3345367)Refutation not found, incomplete strategy
% 28.62/4.91 % (3345367)------------------------------
% 28.62/4.91 % (3345367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.91 % (3345367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.91 % (3345367)CaDiCaL version: 2.1.3
% 28.62/4.91 % (3345367)Termination reason: Refutation not found, incomplete strategy
% 28.62/4.91 % (3345367)Time elapsed: 0.013 s
% 28.62/4.91 % (3345367)Peak memory usage: 89 MB
% 28.62/4.91 % (3345367)Instructions burned: 19 (million)
% 28.62/4.91 % (3345370)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3189584156:i=107:rtra=on_2969 on theBenchmark for (2969ds/107Mi)
% 28.62/4.91 % (3345369)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1712275617:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2969 on theBenchmark for (2969ds/1054Mi)
% 28.62/4.91 % (3345371)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=749825065:s2a=on:i=450:doe=on:nm=32:rtra=on_2969 on theBenchmark for (2969ds/450Mi)
% 28.62/4.91 % (3345369)Refutation not found, incomplete strategy
% 28.62/4.91 % (3345369)------------------------------
% 28.62/4.91 % (3345369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.62/4.91 % (3345369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.62/4.91 % (3345369)CaDiCaL version: 2.1.3
% 28.62/4.91 % (3345369)Termination reason: Refutation not found, incomplete strategy
% 28.62/4.91 % (3345369)Time elapsed: 0.018 s
% 30.76/5.04 % (3345369)Peak memory usage: 89 MB
% 30.76/5.04 % (3345369)Instructions burned: 26 (million)
% 30.76/5.04 % (3345370)Refutation not found, incomplete strategy
% 30.76/5.04 % (3345370)------------------------------
% 30.76/5.04 % (3345370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345370)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345370)Termination reason: Refutation not found, incomplete strategy
% 30.76/5.04 % (3345370)Time elapsed: 0.034 s
% 30.76/5.04 % (3345370)Peak memory usage: 115 MB
% 30.76/5.04 % (3345370)Instructions burned: 17 (million)
% 30.76/5.04 % (3345363)Instruction limit reached!
% 30.76/5.04 % (3345363)------------------------------
% 30.76/5.04 % (3345363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345363)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345363)Termination reason: Instruction limit
% 30.76/5.04 % (3345363)Termination phase: Saturation
% 30.76/5.04 % (3345363)Time elapsed: 0.245 s
% 30.76/5.04 % (3345363)Peak memory usage: 134 MB
% 30.76/5.04 % (3345363)Instructions burned: 276 (million)
% 30.76/5.04 % (3345367)------------------------------
% 30.76/5.04 % (3345367)------------------------------
% 30.76/5.04 % (3345377)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
% 30.76/5.04 % (3345377)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1375638217:i=1090:aac=none:nm=0:rtra=on:rawr=on_2967 on theBenchmark for (2967ds/1090Mi)
% 30.76/5.04 % (3345369)------------------------------
% 30.76/5.04 % (3345369)------------------------------
% 30.76/5.04 % (3345370)------------------------------
% 30.76/5.04 % (3345370)------------------------------
% 30.76/5.04 % (3345378)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3681154480:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2966 on theBenchmark for (2966ds/130Mi)
% 30.76/5.04 % (3345371)Instruction limit reached!
% 30.76/5.04 % (3345371)------------------------------
% 30.76/5.04 % (3345371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345371)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345371)Termination reason: Instruction limit
% 30.76/5.04 % (3345371)Termination phase: Saturation
% 30.76/5.04 % (3345371)Time elapsed: 0.347 s
% 30.76/5.04 % (3345371)Peak memory usage: 136 MB
% 30.76/5.04 % (3345371)Instructions burned: 450 (million)
% 30.76/5.04 % (3345381)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3150384473:i=491:doe=on:rtra=on:gtg=position_2965 on theBenchmark for (2965ds/491Mi)
% 30.76/5.04 % (3345380)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=723749220:i=312:kws=inv_frequency:nm=20:rtra=on_2965 on theBenchmark for (2965ds/312Mi)
% 30.76/5.04 % (3345381)Refutation not found, incomplete strategy
% 30.76/5.04 % (3345381)------------------------------
% 30.76/5.04 % (3345381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345381)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345381)Termination reason: Refutation not found, incomplete strategy
% 30.76/5.04 % (3345381)Time elapsed: 0.008 s
% 30.76/5.04 % (3345381)Peak memory usage: 88 MB
% 30.76/5.04 % (3345381)Instructions burned: 12 (million)
% 30.76/5.04 % (3345378)Instruction limit reached!
% 30.76/5.04 % (3345378)------------------------------
% 30.76/5.04 % (3345378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345378)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345378)Termination reason: Instruction limit
% 30.76/5.04 % (3345378)Termination phase: Saturation
% 30.76/5.04 % (3345378)Time elapsed: 0.098 s
% 30.76/5.04 % (3345378)Peak memory usage: 117 MB
% 30.76/5.04 % (3345378)Instructions burned: 132 (million)
% 30.76/5.04 % (3345364)Instruction limit reached!
% 30.76/5.04 % (3345364)------------------------------
% 30.76/5.04 % (3345364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345364)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345364)Termination reason: Instruction limit
% 30.76/5.04 % (3345364)Termination phase: Saturation
% 30.76/5.04 % (3345364)Time elapsed: 0.614 s
% 30.76/5.04 % (3345364)Peak memory usage: 91 MB
% 30.76/5.04 % (3345364)Instructions burned: 1052 (million)
% 30.76/5.04 % (3345383)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2119766831:s2a=on:i=835:s2at=2:rtra=on_2964 on theBenchmark for (2964ds/835Mi)
% 30.76/5.04 % (3345386)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2156704311:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2963 on theBenchmark for (2963ds/307Mi)
% 30.76/5.04 % (3345380)Instruction limit reached!
% 30.76/5.04 % (3345380)------------------------------
% 30.76/5.04 % (3345380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345380)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345380)Termination reason: Instruction limit
% 30.76/5.04 % (3345380)Termination phase: Saturation
% 30.76/5.04 % (3345380)Time elapsed: 0.216 s
% 30.76/5.04 % (3345380)Peak memory usage: 118 MB
% 30.76/5.04 % (3345380)Instructions burned: 313 (million)
% 30.76/5.04 % (3345387)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1218045753:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi)
% 30.76/5.04 % (3345381)------------------------------
% 30.76/5.04 % (3345381)------------------------------
% 30.76/5.04 % (3345390)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3384403050:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/646Mi)
% 30.76/5.04 % (3345386)Instruction limit reached!
% 30.76/5.04 % (3345386)------------------------------
% 30.76/5.04 % (3345386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345386)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345386)Termination reason: Instruction limit
% 30.76/5.04 % (3345386)Termination phase: Saturation
% 30.76/5.04 % (3345386)Time elapsed: 0.195 s
% 30.76/5.04 % (3345386)Peak memory usage: 92 MB
% 30.76/5.04 % (3345386)Instructions burned: 307 (million)
% 30.76/5.04 % (3345392)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=3645500182:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2961 on theBenchmark for (2961ds/784Mi)
% 30.76/5.04 % (3345377)Instruction limit reached!
% 30.76/5.04 % (3345377)------------------------------
% 30.76/5.04 % (3345377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345377)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345377)Termination reason: Instruction limit
% 30.76/5.04 % (3345377)Termination phase: Saturation
% 30.76/5.04 % (3345377)Time elapsed: 0.650 s
% 30.76/5.04 % (3345377)Peak memory usage: 131 MB
% 30.76/5.04 % (3345377)Instructions burned: 1092 (million)
% 30.76/5.04 % (3345392)First to succeed.
% 30.76/5.04 % (3345392)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3344937"
% 30.76/5.04 % (3345394)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=3747264750:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2959 on theBenchmark for (2959ds/1131Mi)
% 30.76/5.04 % (3345383)Instruction limit reached!
% 30.76/5.04 % (3345383)------------------------------
% 30.76/5.04 % (3345383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345383)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345383)Termination reason: Instruction limit
% 30.76/5.04 % (3345383)Termination phase: Saturation
% 30.76/5.04 % (3345383)Time elapsed: 0.441 s
% 30.76/5.04 % (3345383)Peak memory usage: 92 MB
% 30.76/5.04 % (3345383)Instructions burned: 835 (million)
% 30.76/5.04 % (3345396)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=150619814:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2959 on theBenchmark for (2959ds/246Mi)
% 30.76/5.04 % (3345396)Refutation not found, incomplete strategy
% 30.76/5.04 % (3345396)------------------------------
% 30.76/5.04 % (3345396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345396)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345396)Termination reason: Refutation not found, incomplete strategy
% 30.76/5.04 % (3345396)Time elapsed: 0.030 s
% 30.76/5.04 % (3345396)Peak memory usage: 115 MB
% 30.76/5.04 % (3345396)Instructions burned: 9 (million)
% 30.76/5.04 % (3345362)Instruction limit reached!
% 30.76/5.04 % (3345362)------------------------------
% 30.76/5.04 % (3345362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345362)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345362)Termination reason: Instruction limit
% 30.76/5.04 % (3345362)Termination phase: Saturation
% 30.76/5.04 % (3345362)Time elapsed: 1.322 s
% 30.76/5.04 % (3345362)Peak memory usage: 112 MB
% 30.76/5.04 % (3345362)Instructions burned: 4430 (million)
% 30.76/5.04 % (3345398)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2536785693:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2958 on theBenchmark for (2958ds/775Mi)
% 30.76/5.04 % (3345387)Instruction limit reached!
% 30.76/5.04 % (3345387)------------------------------
% 30.76/5.04 % (3345387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.76/5.04 % (3345387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.76/5.04 % (3345387)CaDiCaL version: 2.1.3
% 30.76/5.04 % (3345387)Termination reason: Instruction limit
% 30.76/5.04 % (3345387)Termination phase: Saturation
% 30.76/5.04 % (3345387)Time elapsed: 0.478 s
% 30.76/5.04 % (3345387)Peak memory usage: 120 MB
% 30.76/5.04 % (3345387)Instructions burned: 777 (million)
% 30.76/5.04 % (3345392)Refutation found. Thanks to Tanya!
% 30.76/5.04 % SZS status Theorem for theBenchmark
% 30.76/5.04 % SZS output start Proof for theBenchmark
% See solution above
% 31.51/5.24 % (3345392)------------------------------
% 31.51/5.24 % (3345392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.24 % (3345392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.24 % (3345392)CaDiCaL version: 2.1.3
% 31.51/5.24 % (3345392)Termination reason: Refutation
% 31.51/5.24 % (3345392)Time elapsed: 0.079 s
% 31.51/5.24 % (3345392)Peak memory usage: 117 MB
% 31.51/5.24 % (3345392)Instructions burned: 78 (million)
% 31.51/5.24 % (3345392)------------------------------
% 31.51/5.24 % (3345392)------------------------------
% 31.51/5.24 % (3344937)Success in time 4.37 s
% 31.51/5.24 % Vampire exiting
%------------------------------------------------------------------------------