%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX083_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:45:50 PM UTC 2026
% Result : Theorem 124.31s 18.36s
% Output : Refutation 124.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 17
% Syntax : Number of formulae : 90 ( 7 unt; 0 typ; 10 def)
% Number of atoms : 247 ( 49 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 243 ( 86 ~; 75 |; 47 &)
% ( 16 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 314 ( 40 atm; 78 fun; 94 num; 102 var)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 17 usr; 11 prp; 0-4 aty)
% Number of functors : 31 ( 24 usr; 9 con; 0-4 aty)
% Number of variables : 187 ( 135 !; 52 ?; 187 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
general: $tType ).
tff(type_def_6,type,
symbol: $tType ).
tff(func_def_0,type,
f__integer__: $int > general ).
tff(func_def_1,type,
f__symbolic__: symbol > general ).
tff(func_def_2,type,
c__infimum__: general ).
tff(func_def_3,type,
c__supremum__: general ).
tff(func_def_10,type,
sK0: general > symbol ).
tff(func_def_11,type,
sK1: $int ).
tff(func_def_12,type,
sK2: $int ).
tff(func_def_13,type,
sK3: $int ).
tff(func_def_14,type,
sK4: $int ).
tff(func_def_15,type,
sK5: general > $int ).
tff(func_def_16,type,
sK6: ( general * general * general * general ) > general ).
tff(func_def_17,type,
sK7: ( general * general * general * general ) > general ).
tff(func_def_18,type,
sK8: ( general * general * general * general ) > general ).
tff(func_def_19,type,
sK9: ( general * general * general * general ) > general ).
tff(func_def_20,type,
sK10: ( general * general * general * general ) > general ).
tff(func_def_21,type,
sK11: ( general * general * general * general ) > general ).
tff(func_def_22,type,
sK12: ( general * general * general * general ) > general ).
tff(func_def_23,type,
sK13: ( general * general * general * general ) > general ).
tff(func_def_24,type,
sK14: ( general * general * general * general ) > general ).
tff(func_def_25,type,
sK15: ( general * general * general * general ) > general ).
tff(func_def_26,type,
sK16: ( general * general * general * general ) > $int ).
tff(func_def_27,type,
sK17: ( general * general * general * general ) > $int ).
tff(func_def_28,type,
sK18: ( general * general * general * general ) > $int ).
tff(func_def_29,type,
sK19: ( general * general * general * general ) > $int ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
div: ( general * general * general * general ) > $o ).
tff(f6,axiom,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
<=> $lesseq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f7,axiom,
! [X1: general,X0: general] :
( ( p__less_equal__(X1,X0)
& p__less_equal__(X0,X1) )
=> ( X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetric_ordering_ax) ).
tff(f10,axiom,
! [X0: general,X1: general] :
( p__less__(X0,X1)
<=> ( p__less_equal__(X0,X1)
& ( X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p__less__def_ax) ).
tff(f16,axiom,
! [X1: general,X0: general,X2: general,X3: general] :
( ? [X6: general,X5: general,X7: general,X4: general] :
( ? [X9: general,X8: general] :
( ? [X10: $int,X11: $int] :
( ? [X12: $int,X11: $int] :
( ( X10 = $product(X12,X11) )
& ( f__integer__(X11) = X6 )
& ( f__integer__(X12) = X5 ) )
& ( f__integer__(X11) = X7 )
& ( X9 = f__integer__($sum(X10,X11)) ) )
& ( X8 = X9 )
& ( X8 = X4 ) )
& ( X0 = X4 )
& ( X1 = X5 )
& ? [X8: general,X9: general] :
( ( X8 = X7 )
& ( X9 = X5 )
& p__less__(X8,X9) )
& ( X3 = X7 )
& ( X2 = X6 )
& ? [X9: general,X8: general] :
( ( X9 = X7 )
& ( X8 = f__integer__(0) )
& p__less_equal__(X8,X9) ) )
<=> div(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_0_completed_definition_of_div_4) ).
tff(f17,axiom,
! [X1: $int,X3: $int,X2: $int,X0: $int] :
( ( $less(X3,$difference(X1,1))
& div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1_unnamed_formula) ).
tff(f18,axiom,
! [X2: $int,X0: $int,X1: $int] :
( div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($difference(X1,1)))
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_unnamed_formula) ).
tff(f19,conjecture,
! [X1: $int,X0: $int] :
( ( ( $greater(X1,0)
=> ? [X2: $int,X3: $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
& $greatereq(X0,0) )
=> ( $greater(X1,0)
=> ? [X3: $int,X2: $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_3_inductive_step) ).
tff(f20,negated_conjecture,
~ ! [X1: $int,X0: $int] :
( ( ( $greater(X1,0)
=> ? [X2: $int,X3: $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
& $greatereq(X0,0) )
=> ( $greater(X1,0)
=> ? [X3: $int,X2: $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3)) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
tff(f21,plain,
~ ! [X1: $int,X0: $int] :
( ( ( $less(0,X1)
=> ? [X2: $int,X3: $int] : div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
& ~ $less(X0,0) )
=> ( $less(0,X1)
=> ? [X3: $int,X2: $int] : div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__(X3)) ) ),
inference(theory_normalization,[],[f20]) ).
tff(f22,plain,
! [X2: $int,X0: $int,X1: $int] :
( div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__($sum(X1,$uminus(1))))
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__($sum(X2,1)),f__integer__(0)) ),
inference(theory_normalization,[],[f18]) ).
tff(f23,plain,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
<=> ~ $less(X1,X0) ),
inference(theory_normalization,[],[f6]) ).
tff(f24,plain,
! [X1: $int,X3: $int,X2: $int,X0: $int] :
( ( $less(X3,$sum(X1,$uminus(1)))
& div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) ),
inference(theory_normalization,[],[f17]) ).
tff(f25,plain,
~ ! [X0: $int,X1: $int] :
( ( ( $less(0,X0)
=> ? [X2: $int,X3: $int] : div(f__integer__(X1),f__integer__(X0),f__integer__(X2),f__integer__(X3)) )
& ~ $less(X1,0) )
=> ( $less(0,X0)
=> ? [X5: $int,X4: $int] : div(f__integer__($sum(X1,1)),f__integer__(X0),f__integer__(X5),f__integer__(X4)) ) ),
inference(rectify,[],[f21]) ).
tff(f26,plain,
! [X2: general,X1: general,X0: general,X3: general] :
( div(X1,X0,X2,X3)
<=> ? [X7: general,X6: general,X4: general,X5: general] :
( ? [X14: general,X15: general] :
( ( X5 = X15 )
& ( X6 = X14 )
& p__less__(X14,X15) )
& ( X0 = X5 )
& ( X2 = X4 )
& ( X3 = X6 )
& ? [X17: general,X16: general] :
( ( f__integer__(0) = X17 )
& p__less_equal__(X17,X16)
& ( X6 = X16 ) )
& ( X1 = X7 )
& ? [X9: general,X8: general] :
( ? [X10: $int,X11: $int] :
( ? [X12: $int,X13: $int] :
( ( f__integer__(X12) = X5 )
& ( $product(X12,X13) = X10 )
& ( f__integer__(X13) = X4 ) )
& ( f__integer__($sum(X10,X11)) = X8 )
& ( f__integer__(X11) = X6 ) )
& ( X7 = X9 )
& ( X8 = X9 ) ) ) ),
inference(rectify,[],[f16]) ).
tff(f27,plain,
! [X0: $int,X1: $int,X2: $int] :
( div(f__integer__(X1),f__integer__(X2),f__integer__(X0),f__integer__($sum(X2,$uminus(1))))
=> div(f__integer__($sum(X1,1)),f__integer__(X2),f__integer__($sum(X0,1)),f__integer__(0)) ),
inference(rectify,[],[f22]) ).
tff(f29,plain,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X1),f__integer__(X0))
<=> ~ $less(X0,X1) ),
inference(rectify,[],[f23]) ).
tff(f31,plain,
! [X2: $int,X0: $int,X3: $int,X1: $int] :
( ( $less(X1,$sum(X0,$uminus(1)))
& div(f__integer__(X3),f__integer__(X0),f__integer__(X2),f__integer__(X1)) )
=> div(f__integer__($sum(X3,1)),f__integer__(X0),f__integer__(X2),f__integer__($sum(X1,1))) ),
inference(rectify,[],[f24]) ).
tff(f34,plain,
? [X0: $int,X1: $int] :
( ! [X5: $int,X4: $int] : ~ div(f__integer__($sum(X1,1)),f__integer__(X0),f__integer__(X5),f__integer__(X4))
& $less(0,X0)
& ( ? [X2: $int,X3: $int] : div(f__integer__(X1),f__integer__(X0),f__integer__(X2),f__integer__(X3))
| ~ $less(0,X0) )
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f25]) ).
tff(f35,plain,
? [X1: $int,X0: $int] :
( ( ? [X2: $int,X3: $int] : div(f__integer__(X1),f__integer__(X0),f__integer__(X2),f__integer__(X3))
| ~ $less(0,X0) )
& ~ $less(X1,0)
& $less(0,X0)
& ! [X5: $int,X4: $int] : ~ div(f__integer__($sum(X1,1)),f__integer__(X0),f__integer__(X5),f__integer__(X4)) ),
inference(flattening,[],[f34]) ).
tff(f37,plain,
! [X2: $int,X0: $int,X3: $int,X1: $int] :
( div(f__integer__($sum(X3,1)),f__integer__(X0),f__integer__(X2),f__integer__($sum(X1,1)))
| ~ $less(X1,$sum(X0,$uminus(1)))
| ~ div(f__integer__(X3),f__integer__(X0),f__integer__(X2),f__integer__(X1)) ),
inference(ennf_transformation,[],[f31]) ).
tff(f38,plain,
! [X3: $int,X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,$sum(X0,$uminus(1)))
| ~ div(f__integer__(X3),f__integer__(X0),f__integer__(X2),f__integer__(X1))
| div(f__integer__($sum(X3,1)),f__integer__(X0),f__integer__(X2),f__integer__($sum(X1,1))) ),
inference(flattening,[],[f37]) ).
tff(f39,plain,
! [X1: $int,X2: $int,X0: $int] :
( div(f__integer__($sum(X1,1)),f__integer__(X2),f__integer__($sum(X0,1)),f__integer__(0))
| ~ div(f__integer__(X1),f__integer__(X2),f__integer__(X0),f__integer__($sum(X2,$uminus(1)))) ),
inference(ennf_transformation,[],[f27]) ).
tff(f40,plain,
! [X1: general,X0: general] :
( ( X0 = X1 )
| ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1) ),
inference(ennf_transformation,[],[f7]) ).
tff(f41,plain,
! [X0: general,X1: general] :
( ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) ),
inference(flattening,[],[f40]) ).
tff(f45,plain,
! [X2: $int,X0: $int,X1: $int] :
( div(f__integer__($sum(X1,1)),f__integer__(X2),f__integer__($sum(X0,1)),f__integer__(0))
| ~ div(f__integer__(X1),f__integer__(X2),f__integer__(X0),f__integer__($sum(X2,$uminus(1)))) ),
inference(cnf_transformation,[],[f39]) ).
tff(f46,plain,
! [X0: $int,X1: $int] :
( p__less_equal__(f__integer__(X1),f__integer__(X0))
| $less(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
tff(f52,plain,
( ~ $less(0,sK2)
| div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__(sK4)) ),
inference(cnf_transformation,[],[f35]) ).
tff(f53,plain,
! [X4: $int,X5: $int] : ~ div(f__integer__($sum(sK1,1)),f__integer__(sK2),f__integer__(X5),f__integer__(X4)),
inference(cnf_transformation,[],[f35]) ).
tff(f54,plain,
$less(0,sK2),
inference(cnf_transformation,[],[f35]) ).
tff(f56,plain,
! [X0: general,X1: general] :
( ( X0 != X1 )
| ~ p__less__(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tff(f57,plain,
! [X0: general,X1: general] :
( p__less_equal__(X0,X1)
| ~ p__less__(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tff(f59,plain,
! [X0: general,X1: general] :
( ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f41]) ).
tff(f72,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( p__less__(sK14(X0,X1,X2,X3),sK15(X0,X1,X2,X3))
| ~ div(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f73,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK14(X0,X1,X2,X3) = sK7(X0,X1,X2,X3) )
| ~ div(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f74,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X1,X0,X2,X3)
| ( sK15(X0,X1,X2,X3) = sK9(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f26]) ).
tff(f81,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK7(X0,X1,X2,X3) = X3 )
| ~ div(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f83,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK9(X0,X1,X2,X3) = X0 )
| ~ div(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f84,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ $less(X1,$sum(X0,$uminus(1)))
| div(f__integer__($sum(X3,1)),f__integer__(X0),f__integer__(X2),f__integer__($sum(X1,1)))
| ~ div(f__integer__(X3),f__integer__(X0),f__integer__(X2),f__integer__(X1)) ),
inference(cnf_transformation,[],[f38]) ).
tff(f88,plain,
! [X1: general] : ~ p__less__(X1,X1),
inference(equality_resolution,[],[f56]) ).
tff(f105,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ div(f__integer__(X1),f__integer__(X2),f__integer__(X0),f__integer__($sum(X2,-1)))
| div(f__integer__($sum(X1,1)),f__integer__(X2),f__integer__($sum(X0,1)),f__integer__(0)) ),
inference(evaluation,[],[f45]) ).
tff(f106,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ div(f__integer__(X3),f__integer__(X0),f__integer__(X2),f__integer__(X1))
| div(f__integer__($sum(X3,1)),f__integer__(X0),f__integer__(X2),f__integer__($sum(X1,1)))
| ~ $less(X1,$sum(X0,-1)) ),
inference(evaluation,[],[f84]) ).
tff(f107,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK14(X0,X1,X2,X3) = X3 )
| ~ div(X1,X0,X2,X3) ),
inference(forward_subsumption_demodulation,[],[f73,f81]) ).
tff(f115,plain,
div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__(sK4)),
inference(global_subsumption,[],[f52,f54]) ).
tff(f124,definition,
( spl20_3
<=> div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__(sK4)) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
tff(f126,plain,
( div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__(sK4))
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f124]) ).
tff(f127,plain,
spl20_3,
inference(avatar_split_clause,[],[f115,f124]) ).
tff(f151,plain,
! [X0: general,X1: general] :
( ~ p__less__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(resolution,[],[f59,f57]) ).
tff(f152,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( f__integer__(X1) = f__integer__(X0) )
| ~ p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
inference(resolution,[],[f59,f46]) ).
tff(f191,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( p__less__(X0,sK15(X1,X2,X3,X0))
| ~ div(X2,X1,X3,X0)
| ~ div(X2,X1,X3,X0) ),
inference(superposition,[],[f72,f107]) ).
tff(f192,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X2,X1,X3,X0)
| p__less__(X0,sK15(X1,X2,X3,X0)) ),
inference(duplicate_literal_removal,[],[f191]) ).
tff(f193,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X2,X1,X3,X0)
| p__less__(X0,sK9(X1,X2,X3,X0)) ),
inference(forward_subsumption_demodulation,[],[f192,f74]) ).
tff(f194,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X2,X1,X3,X0)
| p__less__(X0,X1) ),
inference(forward_subsumption_demodulation,[],[f193,f83]) ).
tff(f244,plain,
( ~ $less(sK4,$sum(sK2,-1))
| div(f__integer__($sum(sK1,1)),f__integer__(sK2),f__integer__(sK3),f__integer__($sum(sK4,1)))
| ~ spl20_3 ),
inference(resolution,[],[f106,f126]) ).
tff(f245,plain,
( ~ $less(sK4,$sum(sK2,-1))
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f244,f53]) ).
tff(f247,definition,
( spl20_13
<=> $less(sK4,$sum(sK2,-1)) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
tff(f249,plain,
( ~ $less(sK4,$sum(sK2,-1))
| spl20_13 ),
inference(avatar_component_clause,[],[f247]) ).
tff(f250,plain,
( ~ spl20_13
| ~ spl20_3 ),
inference(avatar_split_clause,[],[f245,f124,f247]) ).
tff(f322,plain,
( p__less__(f__integer__(sK4),f__integer__(sK2))
| ~ spl20_3 ),
inference(resolution,[],[f194,f126]) ).
tff(f324,definition,
( spl20_21
<=> p__less__(f__integer__(sK4),f__integer__(sK2)) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
tff(f326,plain,
( p__less__(f__integer__(sK4),f__integer__(sK2))
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f324]) ).
tff(f327,plain,
( spl20_21
| ~ spl20_3 ),
inference(avatar_split_clause,[],[f322,f124,f324]) ).
tff(f374,plain,
( ~ p__less_equal__(f__integer__(sK2),f__integer__(sK4))
| ( f__integer__(sK2) = f__integer__(sK4) )
| ~ spl20_21 ),
inference(resolution,[],[f326,f151]) ).
tff(f377,definition,
( spl20_27
<=> ( f__integer__(sK2) = f__integer__(sK4) ) ),
introduced(definition,[new_symbols(definition,[spl20_27])],[avatar_definition]) ).
tff(f379,plain,
( ( f__integer__(sK2) = f__integer__(sK4) )
| ~ spl20_27 ),
inference(avatar_component_clause,[],[f377]) ).
tff(f381,definition,
( spl20_28
<=> p__less_equal__(f__integer__(sK2),f__integer__(sK4)) ),
introduced(definition,[new_symbols(definition,[spl20_28])],[avatar_definition]) ).
tff(f383,plain,
( ~ p__less_equal__(f__integer__(sK2),f__integer__(sK4))
| spl20_28 ),
inference(avatar_component_clause,[],[f381]) ).
tff(f384,plain,
( spl20_27
| ~ spl20_28
| ~ spl20_21 ),
inference(avatar_split_clause,[],[f374,f324,f381,f377]) ).
tff(f474,plain,
( ~ p__less_equal__(f__integer__(sK4),f__integer__($sum(sK2,-1)))
| ( f__integer__($sum(sK2,-1)) = f__integer__(sK4) )
| spl20_13 ),
inference(resolution,[],[f152,f249]) ).
tff(f580,definition,
( spl20_48
<=> p__less_equal__(f__integer__(sK4),f__integer__($sum(sK2,-1))) ),
introduced(definition,[new_symbols(definition,[spl20_48])],[avatar_definition]) ).
tff(f582,plain,
( ~ p__less_equal__(f__integer__(sK4),f__integer__($sum(sK2,-1)))
| spl20_48 ),
inference(avatar_component_clause,[],[f580]) ).
tff(f584,definition,
( spl20_49
<=> ( f__integer__($sum(sK2,-1)) = f__integer__(sK4) ) ),
introduced(definition,[new_symbols(definition,[spl20_49])],[avatar_definition]) ).
tff(f586,plain,
( ( f__integer__($sum(sK2,-1)) = f__integer__(sK4) )
| ~ spl20_49 ),
inference(avatar_component_clause,[],[f584]) ).
tff(f587,plain,
( ~ spl20_48
| spl20_49
| spl20_13 ),
inference(avatar_split_clause,[],[f474,f247,f584,f580]) ).
tff(f650,plain,
( $less(sK4,sK2)
| spl20_28 ),
inference(resolution,[],[f383,f46]) ).
tff(f665,definition,
( spl20_59
<=> $less(sK4,sK2) ),
introduced(definition,[new_symbols(definition,[spl20_59])],[avatar_definition]) ).
tff(f668,plain,
( spl20_59
| spl20_28 ),
inference(avatar_split_clause,[],[f650,f381,f665]) ).
tff(f669,plain,
( $less($sum(sK2,-1),sK4)
| spl20_48 ),
inference(resolution,[],[f582,f46]) ).
tff(f674,definition,
( spl20_60
<=> $less($sum(sK2,-1),sK4) ),
introduced(definition,[new_symbols(definition,[spl20_60])],[avatar_definition]) ).
tff(f677,plain,
( spl20_60
| spl20_48 ),
inference(avatar_split_clause,[],[f669,f580,f674]) ).
tff(f690,plain,
( div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__($sum(sK2,-1)))
| ~ spl20_3
| ~ spl20_49 ),
inference(superposition,[],[f126,f586]) ).
tff(f736,definition,
( spl20_66
<=> div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__($sum(sK2,-1))) ),
introduced(definition,[new_symbols(definition,[spl20_66])],[avatar_definition]) ).
tff(f738,plain,
( div(f__integer__(sK1),f__integer__(sK2),f__integer__(sK3),f__integer__($sum(sK2,-1)))
| ~ spl20_66 ),
inference(avatar_component_clause,[],[f736]) ).
tff(f739,plain,
( spl20_66
| ~ spl20_3
| ~ spl20_49 ),
inference(avatar_split_clause,[],[f690,f584,f124,f736]) ).
tff(f790,plain,
( p__less__(f__integer__(sK2),f__integer__(sK2))
| ~ spl20_21
| ~ spl20_27 ),
inference(superposition,[],[f326,f379]) ).
tff(f816,plain,
( $false
| ~ spl20_21
| ~ spl20_27 ),
inference(forward_subsumption_resolution,[],[f790,f88]) ).
tff(f817,plain,
( ~ spl20_21
| ~ spl20_27 ),
inference(avatar_contradiction_clause,[],[f816]) ).
tff(f5541,plain,
( div(f__integer__($sum(sK1,1)),f__integer__(sK2),f__integer__($sum(sK3,1)),f__integer__(0))
| ~ spl20_66 ),
inference(resolution,[],[f738,f105]) ).
tff(f5555,plain,
( $false
| ~ spl20_66 ),
inference(forward_subsumption_resolution,[],[f5541,f53]) ).
tff(f5556,plain,
~ spl20_66,
inference(avatar_contradiction_clause,[],[f5555]) ).
tff(f5557,plain,
$false,
inference(avatar_smt_refutation,[],[f5556,f817,f739,f677,f668,f587,f384,f327,f250,f127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX083_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n015.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:03:02 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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.49/1.23 % (2693950)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.49/1.23 % (2693959)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2704318348:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.49/1.23 % (2693959)Instruction limit reached!
% 3.49/1.23 % (2693959)------------------------------
% 3.49/1.23 % (2693959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/1.23 % (2693959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/1.23 % (2693959)CaDiCaL version: 2.1.3
% 3.49/1.23 % (2693959)Termination reason: Instruction limit
% 3.49/1.23 % (2693959)Termination phase: Saturation
% 3.49/1.23 % (2693959)Time elapsed: 0.003 s
% 3.49/1.23 % (2693959)Peak memory usage: 89 MB
% 3.49/1.23 % (2693959)Instructions burned: 6 (million)
% 3.49/1.23 % (2693956)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=410947930:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.49/1.23 % (2693955)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1962080808:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.49/1.23 % (2693958)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=615760613:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.49/1.23 % (2693957)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3839673802:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.49/1.23 % (2693958)Instruction limit reached!
% 3.49/1.23 % (2693958)------------------------------
% 3.49/1.23 % (2693958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/1.23 % (2693958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/1.23 % (2693958)CaDiCaL version: 2.1.3
% 3.49/1.23 % (2693958)Termination reason: Instruction limit
% 3.49/1.23 % (2693958)Termination phase: Saturation
% 3.49/1.23 % (2693958)Time elapsed: 0.006 s
% 3.49/1.23 % (2693958)Peak memory usage: 88 MB
% 3.49/1.23 % (2693958)Instructions burned: 8 (million)
% 3.49/1.23 % (2693960)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2315262606:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.49/1.23 % (2693961)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3963874693:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.49/1.23 % (2693955)Instruction limit reached!
% 3.49/1.23 % (2693955)------------------------------
% 3.49/1.23 % (2693955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/1.23 % (2693955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/1.23 % (2693955)CaDiCaL version: 2.1.3
% 3.49/1.23 % (2693955)Termination reason: Instruction limit
% 3.49/1.23 % (2693955)Termination phase: Saturation
% 3.49/1.23 % (2693955)Time elapsed: 0.031 s
% 3.49/1.23 % (2693955)Peak memory usage: 115 MB
% 3.49/1.23 % (2693955)Instructions burned: 13 (million)
% 3.49/1.23 % (2693961)Instruction limit reached!
% 3.49/1.23 % (2693961)------------------------------
% 3.49/1.23 % (2693961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/1.23 % (2693961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/1.23 % (2693961)CaDiCaL version: 2.1.3
% 3.49/1.23 % (2693961)Termination reason: Instruction limit
% 3.49/1.23 % (2693961)Termination phase: Saturation
% 3.49/1.23 % (2693961)Time elapsed: 0.045 s
% 3.49/1.23 % (2693961)Peak memory usage: 116 MB
% 3.49/1.23 % (2693961)Instructions burned: 33 (million)
% 3.49/1.23 % (2693960)Instruction limit reached!
% 3.49/1.23 % (2693960)------------------------------
% 3.49/1.23 % (2693960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.49/1.23 % (2693960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/1.23 % (2693960)CaDiCaL version: 2.1.3
% 3.49/1.23 % (2693960)Termination reason: Instruction limit
% 3.49/1.23 % (2693960)Termination phase: Saturation
% 3.49/1.23 % (2693960)Time elapsed: 0.056 s
% 3.49/1.23 % (2693960)Peak memory usage: 117 MB
% 3.49/1.23 % (2693960)Instructions burned: 46 (million)
% 3.49/1.23 % (2693963)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3546153671:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.49/1.23 % (2693963)Instruction limit reached!
% 3.49/1.23 % (2693963)------------------------------
% 4.73/1.40 % (2693963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693963)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693963)Termination reason: Instruction limit
% 4.73/1.40 % (2693963)Termination phase: Saturation
% 4.73/1.40 % (2693963)Time elapsed: 0.006 s
% 4.73/1.40 % (2693963)Peak memory usage: 88 MB
% 4.73/1.40 % (2693963)Instructions burned: 15 (million)
% 4.73/1.40 % (2693957)Instruction limit reached!
% 4.73/1.40 % (2693957)------------------------------
% 4.73/1.40 % (2693957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693957)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693957)Termination reason: Instruction limit
% 4.73/1.40 % (2693957)Termination phase: Saturation
% 4.73/1.40 % (2693957)Time elapsed: 0.152 s
% 4.73/1.40 % (2693957)Peak memory usage: 117 MB
% 4.73/1.40 % (2693957)Instructions burned: 202 (million)
% 4.73/1.40 % (2693970)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=3969153574:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.73/1.40 % (2693970)Instruction limit reached!
% 4.73/1.40 % (2693970)------------------------------
% 4.73/1.40 % (2693970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693970)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693970)Termination reason: Instruction limit
% 4.73/1.40 % (2693970)Termination phase: Saturation
% 4.73/1.40 % (2693970)Time elapsed: 0.020 s
% 4.73/1.40 % (2693970)Peak memory usage: 89 MB
% 4.73/1.40 % (2693970)Instructions burned: 29 (million)
% 4.73/1.40 % (2693971)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3763189315:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.73/1.40 % (2693975)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1303740681:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.73/1.40 % (2693971)Instruction limit reached!
% 4.73/1.40 % (2693971)------------------------------
% 4.73/1.40 % (2693971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693971)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693971)Termination reason: Instruction limit
% 4.73/1.40 % (2693971)Termination phase: Saturation
% 4.73/1.40 % (2693971)Time elapsed: 0.012 s
% 4.73/1.40 % (2693971)Peak memory usage: 90 MB
% 4.73/1.40 % (2693971)Instructions burned: 17 (million)
% 4.73/1.40 % (2693972)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=612671994:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.73/1.40 % (2693975)Instruction limit reached!
% 4.73/1.40 % (2693975)------------------------------
% 4.73/1.40 % (2693975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693975)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693975)Termination reason: Instruction limit
% 4.73/1.40 % (2693975)Termination phase: Saturation
% 4.73/1.40 % (2693975)Time elapsed: 0.028 s
% 4.73/1.40 % (2693975)Peak memory usage: 89 MB
% 4.73/1.40 % (2693975)Instructions burned: 87 (million)
% 4.73/1.40 % (2693974)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=229848363:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.73/1.40 % (2693956)Instruction limit reached!
% 4.73/1.40 % (2693956)------------------------------
% 4.73/1.40 % (2693956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.40 % (2693956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.40 % (2693956)CaDiCaL version: 2.1.3
% 4.73/1.40 % (2693956)Termination reason: Instruction limit
% 4.73/1.40 % (2693956)Termination phase: Saturation
% 4.73/1.40 % (2693956)Time elapsed: 0.226 s
% 4.73/1.40 % (2693956)Peak memory usage: 117 MB
% 4.73/1.40 % (2693956)Instructions burned: 309 (million)
% 4.73/1.40 % (2693972)Instruction limit reached!
% 4.73/1.40 % (2693972)------------------------------
% 4.73/1.40 % (2693972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693972)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693972)Termination reason: Instruction limit
% 5.64/1.58 % (2693972)Termination phase: Saturation
% 5.64/1.58 % (2693972)Time elapsed: 0.019 s
% 5.64/1.58 % (2693972)Peak memory usage: 89 MB
% 5.64/1.58 % (2693972)Instructions burned: 24 (million)
% 5.64/1.58 % (2693974)Instruction limit reached!
% 5.64/1.58 % (2693974)------------------------------
% 5.64/1.58 % (2693974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693974)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693974)Termination reason: Instruction limit
% 5.64/1.58 % (2693974)Termination phase: Saturation
% 5.64/1.58 % (2693974)Time elapsed: 0.020 s
% 5.64/1.58 % (2693974)Peak memory usage: 89 MB
% 5.64/1.58 % (2693974)Instructions burned: 28 (million)
% 5.64/1.58 % (2693977)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=77401287:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.64/1.58 % (2693977)Instruction limit reached!
% 5.64/1.58 % (2693977)------------------------------
% 5.64/1.58 % (2693977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693977)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693977)Termination reason: Instruction limit
% 5.64/1.58 % (2693977)Termination phase: Saturation
% 5.64/1.58 % (2693977)Time elapsed: 0.002 s
% 5.64/1.58 % (2693977)Peak memory usage: 87 MB
% 5.64/1.58 % (2693977)Instructions burned: 2 (million)
% 5.64/1.58 % (2693978)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3094952025:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.64/1.58 % (2693984)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1501422289:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.64/1.58 % (2693981)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4069782490:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.64/1.58 % (2693981)Instruction limit reached!
% 5.64/1.58 % (2693981)------------------------------
% 5.64/1.58 % (2693981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693981)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693981)Termination reason: Instruction limit
% 5.64/1.58 % (2693981)Termination phase: Saturation
% 5.64/1.58 % (2693981)Time elapsed: 0.003 s
% 5.64/1.58 % (2693981)Peak memory usage: 88 MB
% 5.64/1.58 % (2693981)Instructions burned: 4 (million)
% 5.64/1.58 % (2693984)Instruction limit reached!
% 5.64/1.58 % (2693984)------------------------------
% 5.64/1.58 % (2693984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693984)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693984)Termination reason: Instruction limit
% 5.64/1.58 % (2693984)Termination phase: Saturation
% 5.64/1.58 % (2693984)Time elapsed: 0.057 s
% 5.64/1.58 % (2693984)Peak memory usage: 134 MB
% 5.64/1.58 % (2693984)Instructions burned: 66 (million)
% 5.64/1.58 % (2693986)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=662353514:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.64/1.58 % (2693987)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3215302764:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.64/1.58 % (2693985)lrs+10_1_thi=all:si=on:fd=off:random_seed=2684897783:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.64/1.58 % (2693987)Instruction limit reached!
% 5.64/1.58 % (2693987)------------------------------
% 5.64/1.58 % (2693987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.64/1.58 % (2693987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.58 % (2693987)CaDiCaL version: 2.1.3
% 5.64/1.58 % (2693987)Termination reason: Instruction limit
% 5.64/1.58 % (2693987)Termination phase: Saturation
% 7.20/1.78 % (2693987)Time elapsed: 0.005 s
% 7.20/1.78 % (2693987)Peak memory usage: 89 MB
% 7.20/1.78 % (2693987)Instructions burned: 6 (million)
% 7.20/1.78 % (2693986)Instruction limit reached!
% 7.20/1.78 % (2693986)------------------------------
% 7.20/1.78 % (2693986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693986)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693986)Termination reason: Instruction limit
% 7.20/1.78 % (2693986)Termination phase: Saturation
% 7.20/1.78 % (2693986)Time elapsed: 0.007 s
% 7.20/1.78 % (2693986)Peak memory usage: 88 MB
% 7.20/1.78 % (2693986)Instructions burned: 9 (million)
% 7.20/1.78 % (2693978)Instruction limit reached!
% 7.20/1.78 % (2693978)------------------------------
% 7.20/1.78 % (2693978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693978)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693978)Termination reason: Instruction limit
% 7.20/1.78 % (2693978)Termination phase: Saturation
% 7.20/1.78 % (2693978)Time elapsed: 0.114 s
% 7.20/1.78 % (2693978)Peak memory usage: 91 MB
% 7.20/1.78 % (2693978)Instructions burned: 182 (million)
% 7.20/1.78 % (2693985)Instruction limit reached!
% 7.20/1.78 % (2693985)------------------------------
% 7.20/1.78 % (2693985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693985)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693985)Termination reason: Instruction limit
% 7.20/1.78 % (2693985)Termination phase: Saturation
% 7.20/1.78 % (2693985)Time elapsed: 0.062 s
% 7.20/1.78 % (2693985)Peak memory usage: 116 MB
% 7.20/1.78 % (2693985)Instructions burned: 54 (million)
% 7.20/1.78 % (2693990)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2584561627:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.20/1.78 % (2693990)Instruction limit reached!
% 7.20/1.78 % (2693990)------------------------------
% 7.20/1.78 % (2693990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693990)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693990)Termination reason: Instruction limit
% 7.20/1.78 % (2693990)Termination phase: Saturation
% 7.20/1.78 % (2693990)Time elapsed: 0.002 s
% 7.20/1.78 % (2693990)Peak memory usage: 87 MB
% 7.20/1.78 % (2693990)Instructions burned: 2 (million)
% 7.20/1.78 % (2693993)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1672741527:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.20/1.78 % (2693997)dis+10_1_si=on:random_seed=495664278:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.20/1.78 % (2693997)Instruction limit reached!
% 7.20/1.78 % (2693997)------------------------------
% 7.20/1.78 % (2693997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693997)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693997)Termination reason: Instruction limit
% 7.20/1.78 % (2693997)Termination phase: Saturation
% 7.20/1.78 % (2693997)Time elapsed: 0.005 s
% 7.20/1.78 % (2693997)Peak memory usage: 88 MB
% 7.20/1.78 % (2693997)Instructions burned: 13 (million)
% 7.20/1.78 % (2693999)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=452138651:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.20/1.78 % (2693998)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1946697399:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.20/1.78 % (2693998)Refutation not found, incomplete strategy
% 7.20/1.78 % (2693998)------------------------------
% 7.20/1.78 % (2693998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.78 % (2693998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.78 % (2693998)CaDiCaL version: 2.1.3
% 7.20/1.78 % (2693998)Termination reason: Refutation not found, incomplete strategy
% 7.20/1.78 % (2693998)Time elapsed: 0.004 s
% 7.20/1.78 % (2693998)Peak memory usage: 89 MB
% 7.20/1.78 % (2693998)Instructions burned: 5 (million)
% 7.20/1.78 % (2693999)Instruction limit reached!
% 10.05/2.05 % (2693999)------------------------------
% 10.05/2.05 % (2693999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2693999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2693999)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2693999)Termination reason: Instruction limit
% 10.05/2.05 % (2693999)Termination phase: Saturation
% 10.05/2.05 % (2693999)Time elapsed: 0.029 s
% 10.05/2.05 % (2693999)Peak memory usage: 89 MB
% 10.05/2.05 % (2693999)Instructions burned: 35 (million)
% 10.05/2.05 % (2694000)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3946559128:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.05/2.05 % (2694000)Instruction limit reached!
% 10.05/2.05 % (2694000)------------------------------
% 10.05/2.05 % (2694000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2694000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2694000)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2694000)Termination reason: Instruction limit
% 10.05/2.05 % (2694000)Termination phase: Saturation
% 10.05/2.05 % (2694000)Time elapsed: 0.002 s
% 10.05/2.05 % (2694000)Peak memory usage: 86 MB
% 10.05/2.05 % (2694000)Instructions burned: 2 (million)
% 10.05/2.05 % (2693993)Instruction limit reached!
% 10.05/2.05 % (2693993)------------------------------
% 10.05/2.05 % (2693993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2693993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2693993)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2693993)Termination reason: Instruction limit
% 10.05/2.05 % (2693993)Termination phase: Saturation
% 10.05/2.05 % (2693993)Time elapsed: 0.112 s
% 10.05/2.05 % (2693993)Peak memory usage: 117 MB
% 10.05/2.05 % (2693993)Instructions burned: 128 (million)
% 10.05/2.05 % (2694001)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1396993037:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.05/2.05 % (2694006)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1029354278:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.05/2.05 % (2694003)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1678693493:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.05/2.05 % (2694001)Instruction limit reached!
% 10.05/2.05 % (2694001)------------------------------
% 10.05/2.05 % (2694001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2694001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2694001)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2694001)Termination reason: Instruction limit
% 10.05/2.05 % (2694001)Termination phase: Saturation
% 10.05/2.05 % (2694001)Time elapsed: 0.007 s
% 10.05/2.05 % (2694001)Peak memory usage: 88 MB
% 10.05/2.05 % (2694001)Instructions burned: 8 (million)
% 10.05/2.05 % (2694006)Instruction limit reached!
% 10.05/2.05 % (2694006)------------------------------
% 10.05/2.05 % (2694006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2694006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2694006)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2694006)Termination reason: Instruction limit
% 10.05/2.05 % (2694006)Termination phase: Saturation
% 10.05/2.05 % (2694006)Time elapsed: 0.019 s
% 10.05/2.05 % (2694006)Peak memory usage: 113 MB
% 10.05/2.05 % (2694006)Instructions burned: 16 (million)
% 10.05/2.05 % (2694009)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3605163522:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.05/2.05 % (2694013)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=104028986:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.05/2.05 % (2694011)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2137747064:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.05/2.05 % (2694017)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=2978885436:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 10.05/2.05 % (2694016)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=3390160439:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 11.21/2.31 % (2694011)Instruction limit reached!
% 11.21/2.31 % (2694011)------------------------------
% 11.21/2.31 % (2694011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694011)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694011)Termination reason: Instruction limit
% 11.21/2.31 % (2694011)Termination phase: Saturation
% 11.21/2.31 % (2694011)Time elapsed: 0.009 s
% 11.21/2.31 % (2694011)Peak memory usage: 88 MB
% 11.21/2.31 % (2694011)Instructions burned: 10 (million)
% 11.21/2.31 % (2693998)------------------------------
% 11.21/2.31 % (2693998)------------------------------
% 11.21/2.31 % (2694016)Instruction limit reached!
% 11.21/2.31 % (2694016)------------------------------
% 11.21/2.31 % (2694016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694016)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694016)Termination reason: Instruction limit
% 11.21/2.31 % (2694016)Termination phase: Saturation
% 11.21/2.31 % (2694016)Time elapsed: 0.057 s
% 11.21/2.31 % (2694016)Peak memory usage: 90 MB
% 11.21/2.31 % (2694016)Instructions burned: 75 (million)
% 11.21/2.31 % (2694003)Instruction limit reached!
% 11.21/2.31 % (2694003)------------------------------
% 11.21/2.31 % (2694003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694003)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694003)Termination reason: Instruction limit
% 11.21/2.31 % (2694003)Termination phase: Saturation
% 11.21/2.31 % (2694003)Time elapsed: 0.210 s
% 11.21/2.31 % (2694003)Peak memory usage: 95 MB
% 11.21/2.31 % (2694003)Instructions burned: 370 (million)
% 11.21/2.31 % (2694013)Instruction limit reached!
% 11.21/2.31 % (2694013)------------------------------
% 11.21/2.31 % (2694013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694013)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694013)Termination reason: Instruction limit
% 11.21/2.31 % (2694013)Termination phase: Saturation
% 11.21/2.31 % (2694013)Time elapsed: 0.092 s
% 11.21/2.31 % (2694013)Peak memory usage: 133 MB
% 11.21/2.31 % (2694013)Instructions burned: 72 (million)
% 11.21/2.31 % (2694017)Instruction limit reached!
% 11.21/2.31 % (2694017)------------------------------
% 11.21/2.31 % (2694017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694017)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694017)Termination reason: Instruction limit
% 11.21/2.31 % (2694017)Termination phase: Saturation
% 11.21/2.31 % (2694017)Time elapsed: 0.093 s
% 11.21/2.31 % (2694017)Peak memory usage: 91 MB
% 11.21/2.31 % (2694017)Instructions burned: 297 (million)
% 11.21/2.31 % (2694009)Instruction limit reached!
% 11.21/2.31 % (2694009)------------------------------
% 11.21/2.31 % (2694009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.31 % (2694009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.31 % (2694009)CaDiCaL version: 2.1.3
% 11.21/2.31 % (2694009)Termination reason: Instruction limit
% 11.21/2.31 % (2694009)Termination phase: Saturation
% 11.21/2.31 % (2694009)Time elapsed: 0.150 s
% 11.21/2.31 % (2694009)Peak memory usage: 116 MB
% 11.21/2.31 % (2694009)Instructions burned: 226 (million)
% 11.21/2.31 % (2694023)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4010931377:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 11.21/2.31 % (2694025)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=15476752:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 11.21/2.31 % (2694024)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2009315656:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.21/2.31 % (2694028)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3476034275:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.21/2.31 % (2694026)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2158586477:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 12.56/2.65 % (2694027)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=987703833:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 12.56/2.65 % (2694028)Instruction limit reached!
% 12.56/2.65 % (2694028)------------------------------
% 12.56/2.65 % (2694028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694028)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694028)Termination reason: Instruction limit
% 12.56/2.65 % (2694028)Termination phase: Saturation
% 12.56/2.65 % (2694028)Time elapsed: 0.060 s
% 12.56/2.65 % (2694028)Peak memory usage: 118 MB
% 12.56/2.65 % (2694028)Instructions burned: 133 (million)
% 12.56/2.65 % (2694023)Instruction limit reached!
% 12.56/2.65 % (2694023)------------------------------
% 12.56/2.65 % (2694023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694023)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694023)Termination reason: Instruction limit
% 12.56/2.65 % (2694023)Termination phase: Saturation
% 12.56/2.65 % (2694023)Time elapsed: 0.107 s
% 12.56/2.65 % (2694023)Peak memory usage: 117 MB
% 12.56/2.65 % (2694023)Instructions burned: 130 (million)
% 12.56/2.65 % (2694025)Instruction limit reached!
% 12.56/2.65 % (2694025)------------------------------
% 12.56/2.65 % (2694025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694025)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694025)Termination reason: Instruction limit
% 12.56/2.65 % (2694025)Termination phase: Saturation
% 12.56/2.65 % (2694025)Time elapsed: 0.069 s
% 12.56/2.65 % (2694025)Peak memory usage: 133 MB
% 12.56/2.65 % (2694025)Instructions burned: 40 (million)
% 12.56/2.65 % (2694029)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=370268380:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 12.56/2.65 % (2694024)Instruction limit reached!
% 12.56/2.65 % (2694024)------------------------------
% 12.56/2.65 % (2694024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694024)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694024)Termination reason: Instruction limit
% 12.56/2.65 % (2694024)Termination phase: Saturation
% 12.56/2.65 % (2694024)Time elapsed: 0.135 s
% 12.56/2.65 % (2694024)Peak memory usage: 135 MB
% 12.56/2.65 % (2694024)Instructions burned: 132 (million)
% 12.56/2.65 % (2694036)dis+10_1_si=on:random_seed=2002958598:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 12.56/2.65 % (2694026)Instruction limit reached!
% 12.56/2.65 % (2694026)------------------------------
% 12.56/2.65 % (2694026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694026)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694026)Termination reason: Instruction limit
% 12.56/2.65 % (2694026)Termination phase: Saturation
% 12.56/2.65 % (2694026)Time elapsed: 0.183 s
% 12.56/2.65 % (2694026)Peak memory usage: 92 MB
% 12.56/2.65 % (2694026)Instructions burned: 308 (million)
% 12.56/2.65 % (2694037)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2094435635:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.56/2.65 % (2694038)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=503234743:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 12.56/2.65 % (2694029)Instruction limit reached!
% 12.56/2.65 % (2694029)------------------------------
% 12.56/2.65 % (2694029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.65 % (2694029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.65 % (2694029)CaDiCaL version: 2.1.3
% 12.56/2.65 % (2694029)Termination reason: Instruction limit
% 12.56/2.65 % (2694029)Termination phase: Saturation
% 12.56/2.65 % (2694029)Time elapsed: 0.184 s
% 12.56/2.65 % (2694029)Peak memory usage: 116 MB
% 12.56/2.65 % (2694029)Instructions burned: 260 (million)
% 14.88/2.88 % (2694040)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1613186182:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 14.88/2.88 % (2694038)Instruction limit reached!
% 14.88/2.88 % (2694038)------------------------------
% 14.88/2.88 % (2694038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694038)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694038)Termination reason: Instruction limit
% 14.88/2.88 % (2694038)Termination phase: Saturation
% 14.88/2.88 % (2694038)Time elapsed: 0.094 s
% 14.88/2.88 % (2694038)Peak memory usage: 90 MB
% 14.88/2.88 % (2694038)Instructions burned: 142 (million)
% 14.88/2.88 % (2694042)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3944578291:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 14.88/2.88 % (2694040)Instruction limit reached!
% 14.88/2.88 % (2694040)------------------------------
% 14.88/2.88 % (2694040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694040)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694040)Termination reason: Instruction limit
% 14.88/2.88 % (2694040)Termination phase: Saturation
% 14.88/2.88 % (2694040)Time elapsed: 0.066 s
% 14.88/2.88 % (2694040)Peak memory usage: 117 MB
% 14.88/2.88 % (2694040)Instructions burned: 67 (million)
% 14.88/2.88 % (2694042)Instruction limit reached!
% 14.88/2.88 % (2694042)------------------------------
% 14.88/2.88 % (2694042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694042)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694042)Termination reason: Instruction limit
% 14.88/2.88 % (2694042)Termination phase: Saturation
% 14.88/2.88 % (2694042)Time elapsed: 0.071 s
% 14.88/2.88 % (2694042)Peak memory usage: 89 MB
% 14.88/2.88 % (2694042)Instructions burned: 122 (million)
% 14.88/2.88 % (2694045)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=2963136937:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.88/2.88 % (2694037)Instruction limit reached!
% 14.88/2.88 % (2694037)------------------------------
% 14.88/2.88 % (2694037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694037)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694037)Termination reason: Instruction limit
% 14.88/2.88 % (2694037)Termination phase: Saturation
% 14.88/2.88 % (2694037)Time elapsed: 0.231 s
% 14.88/2.88 % (2694037)Peak memory usage: 93 MB
% 14.88/2.88 % (2694037)Instructions burned: 383 (million)
% 14.88/2.88 % (2694036)Instruction limit reached!
% 14.88/2.88 % (2694036)------------------------------
% 14.88/2.88 % (2694036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694036)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694036)Termination reason: Instruction limit
% 14.88/2.88 % (2694036)Termination phase: Saturation
% 14.88/2.88 % (2694036)Time elapsed: 0.291 s
% 14.88/2.88 % (2694036)Peak memory usage: 96 MB
% 14.88/2.88 % (2694036)Instructions burned: 1002 (million)
% 14.88/2.88 % (2694027)Instruction limit reached!
% 14.88/2.88 % (2694027)------------------------------
% 14.88/2.88 % (2694027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/2.88 % (2694027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/2.88 % (2694027)CaDiCaL version: 2.1.3
% 14.88/2.88 % (2694027)Termination reason: Instruction limit
% 14.88/2.88 % (2694027)Termination phase: Saturation
% 14.88/2.88 % (2694027)Time elapsed: 0.441 s
% 14.88/2.88 % (2694027)Peak memory usage: 139 MB
% 14.88/2.88 % (2694027)Instructions burned: 600 (million)
% 14.88/2.88 % (2694047)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=2249244868:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 14.88/2.88 % (2694049)dis+1010_1_to=kbo:si=on:random_seed=3363473364:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 14.88/2.88 % (2694047)Instruction limit reached!
% 14.88/2.88 % (2694047)------------------------------
% 14.88/2.88 % (2694047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.23 % (2694047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.23 % (2694047)CaDiCaL version: 2.1.3
% 17.88/3.23 % (2694047)Termination reason: Instruction limit
% 17.88/3.23 % (2694047)Termination phase: Saturation
% 17.88/3.23 % (2694047)Time elapsed: 0.051 s
% 17.88/3.23 % (2694047)Peak memory usage: 117 MB
% 17.88/3.23 % (2694047)Instructions burned: 40 (million)
% 17.88/3.23 % (2694045)Instruction limit reached!
% 17.88/3.23 % (2694045)------------------------------
% 17.88/3.23 % (2694045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.23 % (2694045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.23 % (2694045)CaDiCaL version: 2.1.3
% 17.88/3.23 % (2694045)Termination reason: Instruction limit
% 17.88/3.23 % (2694045)Termination phase: Saturation
% 17.88/3.23 % (2694045)Time elapsed: 0.113 s
% 17.88/3.23 % (2694045)Peak memory usage: 119 MB
% 17.88/3.23 % (2694045)Instructions burned: 130 (million)
% 17.88/3.23 % (2694050)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=990623541:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 17.88/3.23 % (2694053)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=257165313:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 17.88/3.23 % (2694052)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1545914626:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 17.88/3.23 % (2694049)Instruction limit reached!
% 17.88/3.23 % (2694049)------------------------------
% 17.88/3.23 % (2694049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.23 % (2694049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.23 % (2694049)CaDiCaL version: 2.1.3
% 17.88/3.23 % (2694049)Termination reason: Instruction limit
% 17.88/3.23 % (2694049)Termination phase: Saturation
% 17.88/3.23 % (2694049)Time elapsed: 0.125 s
% 17.88/3.23 % (2694049)Peak memory usage: 91 MB
% 17.88/3.23 % (2694049)Instructions burned: 175 (million)
% 17.88/3.23 % (2694055)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2787554892:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 17.88/3.23 % (2694053)Instruction limit reached!
% 17.88/3.23 % (2694053)------------------------------
% 17.88/3.23 % (2694053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.23 % (2694053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.23 % (2694053)CaDiCaL version: 2.1.3
% 17.88/3.23 % (2694053)Termination reason: Instruction limit
% 17.88/3.23 % (2694053)Termination phase: Saturation
% 17.88/3.23 % (2694053)Time elapsed: 0.093 s
% 17.88/3.23 % (2694053)Peak memory usage: 135 MB
% 17.88/3.23 % (2694053)Instructions burned: 218 (million)
% 17.88/3.23 % (2694057)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2665051799:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 17.88/3.23 % (2694058)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3216404306:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi)
% 17.88/3.23 % (2694050)Instruction limit reached!
% 17.88/3.23 % (2694050)------------------------------
% 17.88/3.23 % (2694050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.23 % (2694050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.23 % (2694050)CaDiCaL version: 2.1.3
% 17.88/3.23 % (2694050)Termination reason: Instruction limit
% 17.88/3.23 % (2694050)Termination phase: Saturation
% 17.88/3.23 % (2694050)Time elapsed: 0.226 s
% 17.88/3.23 % (2694050)Peak memory usage: 118 MB
% 17.88/3.23 % (2694050)Instructions burned: 330 (million)
% 17.88/3.23 % (2694062)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=778943687:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 17.88/3.23 % (2694064)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1457385053:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi)
% 17.88/3.23 % (2694057)Instruction limit reached!
% 17.88/3.23 % (2694057)------------------------------
% 17.88/3.23 % (2694057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.45 % (2694057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.45 % (2694057)CaDiCaL version: 2.1.3
% 18.31/3.45 % (2694057)Termination reason: Instruction limit
% 18.31/3.45 % (2694057)Termination phase: Saturation
% 18.31/3.45 % (2694057)Time elapsed: 0.165 s
% 18.31/3.45 % (2694057)Peak memory usage: 90 MB
% 18.31/3.45 % (2694057)Instructions burned: 295 (million)
% 18.31/3.45 % (2694055)Instruction limit reached!
% 18.31/3.45 % (2694055)------------------------------
% 18.31/3.45 % (2694055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.45 % (2694055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.45 % (2694055)CaDiCaL version: 2.1.3
% 18.31/3.45 % (2694055)Termination reason: Instruction limit
% 18.31/3.45 % (2694055)Termination phase: Saturation
% 18.31/3.45 % (2694055)Time elapsed: 0.230 s
% 18.31/3.45 % (2694055)Peak memory usage: 117 MB
% 18.31/3.45 % (2694055)Instructions burned: 349 (million)
% 18.31/3.45 % (2694058)Instruction limit reached!
% 18.31/3.45 % (2694058)------------------------------
% 18.31/3.45 % (2694058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.46 % (2694058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.46 % (2694058)CaDiCaL version: 2.1.3
% 18.31/3.46 % (2694058)Termination reason: Instruction limit
% 18.31/3.46 % (2694058)Termination phase: Saturation
% 18.31/3.46 % (2694058)Time elapsed: 0.228 s
% 18.31/3.46 % (2694058)Peak memory usage: 118 MB
% 18.31/3.46 % (2694058)Instructions burned: 328 (million)
% 18.31/3.46 % (2694068)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2499425244:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 18.31/3.46 % (2694064)Instruction limit reached!
% 18.31/3.46 % (2694064)------------------------------
% 18.31/3.46 % (2694064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.46 % (2694064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.46 % (2694064)CaDiCaL version: 2.1.3
% 18.31/3.46 % (2694064)Termination reason: Instruction limit
% 18.31/3.46 % (2694064)Termination phase: Saturation
% 18.31/3.46 % (2694064)Time elapsed: 0.164 s
% 18.31/3.46 % (2694064)Peak memory usage: 93 MB
% 18.31/3.46 % (2694064)Instructions burned: 486 (million)
% 18.31/3.46 % (2694052)Instruction limit reached!
% 18.31/3.46 % (2694052)------------------------------
% 18.31/3.46 % (2694052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.46 % (2694052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.46 % (2694052)CaDiCaL version: 2.1.3
% 18.31/3.46 % (2694052)Termination reason: Instruction limit
% 18.31/3.46 % (2694052)Termination phase: Saturation
% 18.31/3.46 % (2694052)Time elapsed: 0.372 s
% 18.31/3.46 % (2694052)Peak memory usage: 135 MB
% 18.31/3.46 % (2694052)Instructions burned: 484 (million)
% 18.31/3.46 % (2694062)Instruction limit reached!
% 18.31/3.46 % (2694062)------------------------------
% 18.31/3.46 % (2694062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.31/3.46 % (2694062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.31/3.46 % (2694062)CaDiCaL version: 2.1.3
% 18.31/3.46 % (2694062)Termination reason: Instruction limit
% 18.31/3.46 % (2694062)Termination phase: Saturation
% 18.31/3.46 % (2694062)Time elapsed: 0.209 s
% 18.31/3.46 % (2694062)Peak memory usage: 118 MB
% 18.31/3.46 % (2694062)Instructions burned: 282 (million)
% 18.31/3.46 % (2694070)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1013453602:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 18.31/3.46 % (2694071)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3717768612:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 18.31/3.46 % (2694074)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2296914740:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 18.31/3.46 % (2694073)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=478378596:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 18.31/3.46 % (2694068)Instruction limit reached!
% 18.31/3.46 % (2694068)------------------------------
% 18.31/3.46 % (2694068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694068)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694068)Termination reason: Instruction limit
% 20.88/3.97 % (2694068)Termination phase: Saturation
% 20.88/3.97 % (2694068)Time elapsed: 0.156 s
% 20.88/3.97 % (2694068)Peak memory usage: 113 MB
% 20.88/3.97 % (2694068)Instructions burned: 323 (million)
% 20.88/3.97 % (2694075)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1602119730:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi)
% 20.88/3.97 % (2694076)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1795219264:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi)
% 20.88/3.97 % (2694074)Instruction limit reached!
% 20.88/3.97 % (2694074)------------------------------
% 20.88/3.97 % (2694074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694074)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694074)Termination reason: Instruction limit
% 20.88/3.97 % (2694074)Termination phase: Saturation
% 20.88/3.97 % (2694074)Time elapsed: 0.140 s
% 20.88/3.97 % (2694074)Peak memory usage: 118 MB
% 20.88/3.97 % (2694074)Instructions burned: 375 (million)
% 20.88/3.97 % (2694081)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3935052515:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 20.88/3.97 % (2694070)Instruction limit reached!
% 20.88/3.97 % (2694070)------------------------------
% 20.88/3.97 % (2694070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694070)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694070)Termination reason: Instruction limit
% 20.88/3.97 % (2694070)Termination phase: Saturation
% 20.88/3.97 % (2694070)Time elapsed: 0.250 s
% 20.88/3.97 % (2694070)Peak memory usage: 117 MB
% 20.88/3.97 % (2694070)Instructions burned: 416 (million)
% 20.88/3.97 % (2694073)Instruction limit reached!
% 20.88/3.97 % (2694073)------------------------------
% 20.88/3.97 % (2694073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694073)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694073)Termination reason: Instruction limit
% 20.88/3.97 % (2694073)Termination phase: Saturation
% 20.88/3.97 % (2694073)Time elapsed: 0.221 s
% 20.88/3.97 % (2694073)Peak memory usage: 136 MB
% 20.88/3.97 % (2694073)Instructions burned: 277 (million)
% 20.88/3.97 % (2694084)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=226325816:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi)
% 20.88/3.97 % (2694071)Instruction limit reached!
% 20.88/3.97 % (2694071)------------------------------
% 20.88/3.97 % (2694071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694071)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694071)Termination reason: Instruction limit
% 20.88/3.97 % (2694071)Termination phase: Saturation
% 20.88/3.97 % (2694071)Time elapsed: 0.320 s
% 20.88/3.97 % (2694071)Peak memory usage: 120 MB
% 20.88/3.97 % (2694071)Instructions burned: 472 (million)
% 20.88/3.97 % (2694075)Instruction limit reached!
% 20.88/3.97 % (2694075)------------------------------
% 20.88/3.97 % (2694075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.88/3.97 % (2694075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.88/3.97 % (2694075)CaDiCaL version: 2.1.3
% 20.88/3.97 % (2694075)Termination reason: Instruction limit
% 20.88/3.97 % (2694075)Termination phase: Saturation
% 20.88/3.97 % (2694075)Time elapsed: 0.268 s
% 20.88/3.97 % (2694075)Peak memory usage: 120 MB
% 20.88/3.97 % (2694075)Instructions burned: 387 (million)
% 20.88/3.97 % (2694086)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2390078677:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi)
% 20.88/3.97 % (2694087)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1154745443:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 25.35/4.39 % (2694084)Instruction limit reached!
% 25.35/4.39 % (2694084)------------------------------
% 25.35/4.39 % (2694084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694084)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694084)Termination reason: Instruction limit
% 25.35/4.39 % (2694084)Termination phase: Saturation
% 25.35/4.39 % (2694084)Time elapsed: 0.119 s
% 25.35/4.39 % (2694084)Peak memory usage: 91 MB
% 25.35/4.39 % (2694084)Instructions burned: 360 (million)
% 25.35/4.39 % (2694076)Instruction limit reached!
% 25.35/4.39 % (2694076)------------------------------
% 25.35/4.39 % (2694076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694076)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694076)Termination reason: Instruction limit
% 25.35/4.39 % (2694076)Termination phase: Saturation
% 25.35/4.39 % (2694076)Time elapsed: 0.320 s
% 25.35/4.39 % (2694076)Peak memory usage: 93 MB
% 25.35/4.39 % (2694076)Instructions burned: 514 (million)
% 25.35/4.39 % (2694087)Refutation not found, incomplete strategy
% 25.35/4.39 % (2694087)------------------------------
% 25.35/4.39 % (2694087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694087)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694087)Termination reason: Refutation not found, incomplete strategy
% 25.35/4.39 % (2694087)Time elapsed: 0.053 s
% 25.35/4.39 % (2694087)Peak memory usage: 116 MB
% 25.35/4.39 % (2694087)Instructions burned: 40 (million)
% 25.35/4.39 % (2694081)Instruction limit reached!
% 25.35/4.39 % (2694081)------------------------------
% 25.35/4.39 % (2694081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694081)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694081)Termination reason: Instruction limit
% 25.35/4.39 % (2694081)Termination phase: Saturation
% 25.35/4.39 % (2694081)Time elapsed: 0.247 s
% 25.35/4.39 % (2694081)Peak memory usage: 137 MB
% 25.35/4.39 % (2694081)Instructions burned: 335 (million)
% 25.35/4.39 % (2694089)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=1221572557:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 25.35/4.39 % (2694090)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3885017072:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 25.35/4.39 % (2694093)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=348364848:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 25.35/4.39 % (2694093)Instruction limit reached!
% 25.35/4.39 % (2694093)------------------------------
% 25.35/4.39 % (2694093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694093)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694093)Termination reason: Instruction limit
% 25.35/4.39 % (2694093)Termination phase: Saturation
% 25.35/4.39 % (2694093)Time elapsed: 0.053 s
% 25.35/4.39 % (2694093)Peak memory usage: 90 MB
% 25.35/4.39 % (2694093)Instructions burned: 147 (million)
% 25.35/4.39 % (2694094)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3320158881:i=4428:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/4428Mi)
% 25.35/4.39 % (2694086)Instruction limit reached!
% 25.35/4.39 % (2694086)------------------------------
% 25.35/4.39 % (2694086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.35/4.39 % (2694086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.35/4.39 % (2694086)CaDiCaL version: 2.1.3
% 25.35/4.39 % (2694086)Termination reason: Instruction limit
% 25.35/4.39 % (2694086)Termination phase: Saturation
% 25.35/4.39 % (2694086)Time elapsed: 0.225 s
% 25.35/4.39 % (2694086)Peak memory usage: 118 MB
% 25.35/4.39 % (2694086)Instructions burned: 342 (million)
% 25.35/4.39 % (2694096)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=2951407511:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 28.66/4.92 % (2694089)Instruction limit reached!
% 28.66/4.92 % (2694089)------------------------------
% 28.66/4.92 % (2694089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.66/4.92 % (2694089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.66/4.92 % (2694089)CaDiCaL version: 2.1.3
% 28.66/4.92 % (2694089)Termination reason: Instruction limit
% 28.66/4.92 % (2694089)Termination phase: Saturation
% 28.66/4.92 % (2694089)Time elapsed: 0.170 s
% 28.66/4.92 % (2694089)Peak memory usage: 116 MB
% 28.66/4.92 % (2694089)Instructions burned: 235 (million)
% 28.66/4.92 % (2694087)------------------------------
% 28.66/4.92 % (2694087)------------------------------
% 28.66/4.92 % (2694099)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3646890820:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 28.66/4.92 % (2694090)Instruction limit reached!
% 28.66/4.92 % (2694090)------------------------------
% 28.66/4.92 % (2694090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.66/4.92 % (2694090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.66/4.92 % (2694090)CaDiCaL version: 2.1.3
% 28.66/4.92 % (2694090)Termination reason: Instruction limit
% 28.66/4.92 % (2694090)Termination phase: Saturation
% 28.66/4.92 % (2694090)Time elapsed: 0.185 s
% 28.66/4.92 % (2694090)Peak memory usage: 92 MB
% 28.66/4.92 % (2694090)Instructions burned: 273 (million)
% 28.66/4.92 % (2694102)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=126942633:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi)
% 28.66/4.92 % (2694103)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1135614194:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi)
% 28.66/4.92 % (2694096)Instruction limit reached!
% 28.66/4.92 % (2694096)------------------------------
% 28.66/4.92 % (2694096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.66/4.92 % (2694096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.66/4.92 % (2694096)CaDiCaL version: 2.1.3
% 28.66/4.92 % (2694096)Termination reason: Instruction limit
% 28.66/4.92 % (2694096)Termination phase: Saturation
% 28.66/4.92 % (2694096)Time elapsed: 0.227 s
% 28.66/4.92 % (2694096)Peak memory usage: 134 MB
% 28.66/4.92 % (2694096)Instructions burned: 277 (million)
% 28.66/4.92 % (2694106)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3608796680:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 28.66/4.92 % (2694105)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=412745937:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 28.66/4.92 % (2694105)Refutation not found, incomplete strategy
% 28.66/4.92 % (2694105)------------------------------
% 28.66/4.92 % (2694105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.66/4.92 % (2694105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.66/4.92 % (2694105)CaDiCaL version: 2.1.3
% 28.66/4.92 % (2694105)Termination reason: Refutation not found, incomplete strategy
% 28.66/4.92 % (2694105)Time elapsed: 0.041 s
% 28.66/4.92 % (2694105)Peak memory usage: 116 MB
% 28.66/4.92 % (2694105)Instructions burned: 27 (million)
% 28.66/4.92 % (2694111)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
% 28.66/4.92 % (2694111)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=560601397:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi)
% 28.66/4.92 % (2694099)Instruction limit reached!
% 28.66/4.92 % (2694099)------------------------------
% 28.66/4.92 % (2694099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.66/4.92 % (2694099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.66/4.92 % (2694099)CaDiCaL version: 2.1.3
% 28.66/4.92 % (2694099)Termination reason: Instruction limit
% 28.66/4.92 % (2694099)Termination phase: Saturation
% 28.66/4.92 % (2694099)Time elapsed: 0.345 s
% 28.66/4.92 % (2694099)Peak memory usage: 95 MB
% 28.66/4.92 % (2694099)Instructions burned: 1054 (million)
% 28.66/4.92 % (2694105)------------------------------
% 28.66/4.92 % (2694105)------------------------------
% 32.26/5.34 % (2694113)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3002739006:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2967 on theBenchmark for (2967ds/130Mi)
% 32.26/5.34 % (2694106)Instruction limit reached!
% 32.26/5.34 % (2694106)------------------------------
% 32.26/5.34 % (2694106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694106)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694106)Termination reason: Instruction limit
% 32.26/5.34 % (2694106)Termination phase: Saturation
% 32.26/5.34 % (2694106)Time elapsed: 0.349 s
% 32.26/5.34 % (2694106)Peak memory usage: 135 MB
% 32.26/5.34 % (2694106)Instructions burned: 451 (million)
% 32.26/5.34 % (2694113)Instruction limit reached!
% 32.26/5.34 % (2694113)------------------------------
% 32.26/5.34 % (2694113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694102)Instruction limit reached!
% 32.26/5.34 % (2694102)------------------------------
% 32.26/5.34 % (2694102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694113)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694102)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694102)Termination reason: Instruction limit
% 32.26/5.34 % (2694102)Termination phase: Saturation
% 32.26/5.34 % (2694113)Termination reason: Instruction limit
% 32.26/5.34 % (2694113)Termination phase: Saturation
% 32.26/5.34 % (2694102)Time elapsed: 0.448 s
% 32.26/5.34 % (2694113)Time elapsed: 0.058 s
% 32.26/5.34 % (2694102)Peak memory usage: 97 MB
% 32.26/5.34 % (2694113)Peak memory usage: 116 MB
% 32.26/5.34 % (2694102)Instructions burned: 655 (million)
% 32.26/5.34 % (2694113)Instructions burned: 131 (million)
% 32.26/5.34 % (2694114)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2723849564:i=312:kws=inv_frequency:nm=20:rtra=on_2966 on theBenchmark for (2966ds/312Mi)
% 32.26/5.34 % (2694116)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1631934520:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi)
% 32.26/5.34 % (2694118)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3033036577:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi)
% 32.26/5.34 % (2694103)Instruction limit reached!
% 32.26/5.34 % (2694103)------------------------------
% 32.26/5.34 % (2694103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694103)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694103)Termination reason: Instruction limit
% 32.26/5.34 % (2694103)Termination phase: Saturation
% 32.26/5.34 % (2694103)Time elapsed: 0.574 s
% 32.26/5.34 % (2694103)Peak memory usage: 91 MB
% 32.26/5.34 % (2694103)Instructions burned: 1054 (million)
% 32.26/5.34 % (2694117)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3243402413:s2a=on:i=835:s2at=2:rtra=on_2965 on theBenchmark for (2965ds/835Mi)
% 32.26/5.34 % (2694118)Instruction limit reached!
% 32.26/5.34 % (2694118)------------------------------
% 32.26/5.34 % (2694118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694118)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694118)Termination reason: Instruction limit
% 32.26/5.34 % (2694118)Termination phase: Saturation
% 32.26/5.34 % (2694118)Time elapsed: 0.122 s
% 32.26/5.34 % (2694118)Peak memory usage: 92 MB
% 32.26/5.34 % (2694118)Instructions burned: 308 (million)
% 32.26/5.34 % (2694114)Instruction limit reached!
% 32.26/5.34 % (2694114)------------------------------
% 32.26/5.34 % (2694114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.26/5.34 % (2694114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.26/5.34 % (2694114)CaDiCaL version: 2.1.3
% 32.26/5.34 % (2694114)Termination reason: Instruction limit
% 32.26/5.34 % (2694114)Termination phase: Saturation
% 32.26/5.34 % (2694114)Time elapsed: 0.218 s
% 32.26/5.34 % (2694114)Peak memory usage: 118 MB
% 32.26/5.34 % (2694114)Instructions burned: 314 (million)
% 32.26/5.34 % (2694122)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3135016759:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi)
% 40.17/6.31 % (2694124)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2581505168:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi)
% 40.17/6.31 % (2694116)Instruction limit reached!
% 40.17/6.31 % (2694116)------------------------------
% 40.17/6.31 % (2694116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/6.31 % (2694116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/6.31 % (2694116)CaDiCaL version: 2.1.3
% 40.17/6.31 % (2694116)Termination reason: Instruction limit
% 40.17/6.31 % (2694116)Termination phase: Saturation
% 40.17/6.31 % (2694116)Time elapsed: 0.303 s
% 40.17/6.31 % (2694116)Peak memory usage: 94 MB
% 40.17/6.31 % (2694116)Instructions burned: 492 (million)
% 40.17/6.31 % (2694125)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=3199483610:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi)
% 40.17/6.31 % (2694111)Instruction limit reached!
% 40.17/6.31 % (2694111)------------------------------
% 40.17/6.31 % (2694111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/6.31 % (2694111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/6.31 % (2694111)CaDiCaL version: 2.1.3
% 40.17/6.31 % (2694111)Termination reason: Instruction limit
% 40.17/6.31 % (2694111)Termination phase: Saturation
% 40.17/6.31 % (2694111)Time elapsed: 0.724 s
% 40.17/6.31 % (2694111)Peak memory usage: 124 MB
% 40.17/6.31 % (2694111)Instructions burned: 1090 (million)
% 40.17/6.31 % (2694128)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=2051992645:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2961 on theBenchmark for (2961ds/1131Mi)
% 40.17/6.31 % (2694124)Instruction limit reached!
% 40.17/6.31 % (2694124)------------------------------
% 40.17/6.31 % (2694124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/6.31 % (2694124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/6.31 % (2694124)CaDiCaL version: 2.1.3
% 40.17/6.31 % (2694124)Termination reason: Instruction limit
% 40.17/6.31 % (2694124)Termination phase: Saturation
% 40.17/6.31 % (2694124)Time elapsed: 0.251 s
% 40.17/6.31 % (2694124)Peak memory usage: 139 MB
% 40.17/6.31 % (2694124)Instructions burned: 648 (million)
% 40.17/6.31 % (2694117)Instruction limit reached!
% 40.17/6.31 % (2694117)------------------------------
% 40.17/6.31 % (2694117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/6.31 % (2694117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/6.31 % (2694117)CaDiCaL version: 2.1.3
% 40.17/6.31 % (2694117)Termination reason: Instruction limit
% 40.17/6.31 % (2694117)Termination phase: Saturation
% 40.17/6.31 % (2694117)Time elapsed: 0.480 s
% 40.17/6.31 % (2694117)Peak memory usage: 94 MB
% 40.17/6.31 % (2694117)Instructions burned: 836 (million)
% 40.17/6.31 % (2694130)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=1059208512:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi)
% 40.17/6.31 % (2694132)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1775129916:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi)
% 40.17/6.31 % (2694122)Instruction limit reached!
% 40.17/6.31 % (2694122)------------------------------
% 40.17/6.31 % (2694122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/6.31 % (2694122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/6.31 % (2694122)CaDiCaL version: 2.1.3
% 40.17/6.31 % (2694122)Termination reason: Instruction limit
% 40.17/6.31 % (2694122)Termination phase: Saturation
% 40.17/6.31 % (2694122)Time elapsed: 0.430 s
% 40.17/6.31 % (2694122)Peak memory usage: 120 MB
% 40.17/6.31 % (2694122)Instructions burned: 778 (million)
% 40.17/6.31 % (2694133)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2296652365:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 40.17/6.31 % (2694130)Instruction limit reached!
% 40.17/6.31 % (2694130)------------------------------
% 40.17/6.31 % (2694130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694130)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694130)Termination reason: Instruction limit
% 54.64/8.65 % (2694130)Termination phase: Saturation
% 54.64/8.65 % (2694130)Time elapsed: 0.177 s
% 54.64/8.65 % (2694130)Peak memory usage: 116 MB
% 54.64/8.65 % (2694130)Instructions burned: 247 (million)
% 54.64/8.65 % (2694136)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2571850946:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi)
% 54.64/8.65 % (2694136)Instruction limit reached!
% 54.64/8.65 % (2694136)------------------------------
% 54.64/8.65 % (2694136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694136)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694136)Termination reason: Instruction limit
% 54.64/8.65 % (2694136)Termination phase: Saturation
% 54.64/8.65 % (2694136)Time elapsed: 0.060 s
% 54.64/8.65 % (2694136)Peak memory usage: 89 MB
% 54.64/8.65 % (2694136)Instructions burned: 104 (million)
% 54.64/8.65 % (2694133)Instruction limit reached!
% 54.64/8.65 % (2694133)------------------------------
% 54.64/8.65 % (2694133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694133)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694133)Termination reason: Instruction limit
% 54.64/8.65 % (2694133)Termination phase: Saturation
% 54.64/8.65 % (2694133)Time elapsed: 0.168 s
% 54.64/8.65 % (2694133)Peak memory usage: 91 MB
% 54.64/8.65 % (2694133)Instructions burned: 274 (million)
% 54.64/8.65 % (2694125)Instruction limit reached!
% 54.64/8.65 % (2694125)------------------------------
% 54.64/8.65 % (2694125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694125)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694125)Termination reason: Instruction limit
% 54.64/8.65 % (2694125)Termination phase: Saturation
% 54.64/8.65 % (2694125)Time elapsed: 0.512 s
% 54.64/8.65 % (2694125)Peak memory usage: 122 MB
% 54.64/8.65 % (2694125)Instructions burned: 785 (million)
% 54.64/8.65 % (2694138)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3949689071:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi)
% 54.64/8.65 % (2694132)Instruction limit reached!
% 54.64/8.65 % (2694132)------------------------------
% 54.64/8.65 % (2694132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694132)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694132)Termination reason: Instruction limit
% 54.64/8.65 % (2694132)Termination phase: Saturation
% 54.64/8.65 % (2694132)Time elapsed: 0.286 s
% 54.64/8.65 % (2694132)Peak memory usage: 96 MB
% 54.64/8.65 % (2694132)Instructions burned: 777 (million)
% 54.64/8.65 % (2694142)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=3277312115:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi)
% 54.64/8.65 % (2694140)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2836160583:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi)
% 54.64/8.65 % (2694141)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=2569962820:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi)
% 54.64/8.65 % (2694144)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2956159730:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi)
% 54.64/8.65 % (2694128)Instruction limit reached!
% 54.64/8.65 % (2694128)------------------------------
% 54.64/8.65 % (2694128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.64/8.65 % (2694128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.64/8.65 % (2694128)CaDiCaL version: 2.1.3
% 54.64/8.65 % (2694128)Termination reason: Instruction limit
% 54.64/8.65 % (2694128)Termination phase: Saturation
% 54.64/8.65 % (2694128)Time elapsed: 0.694 s
% 54.64/8.65 % (2694128)Peak memory usage: 123 MB
% 64.53/10.03 % (2694128)Instructions burned: 1132 (million)
% 64.53/10.03 % (2694149)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=15175430:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2953 on theBenchmark for (2953ds/273Mi)
% 64.53/10.03 % (2694138)Instruction limit reached!
% 64.53/10.03 % (2694138)------------------------------
% 64.53/10.03 % (2694138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.03 % (2694138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.03 % (2694138)CaDiCaL version: 2.1.3
% 64.53/10.03 % (2694138)Termination reason: Instruction limit
% 64.53/10.03 % (2694138)Termination phase: Saturation
% 64.53/10.03 % (2694138)Time elapsed: 0.587 s
% 64.53/10.03 % (2694138)Peak memory usage: 97 MB
% 64.53/10.03 % (2694138)Instructions burned: 1094 (million)
% 64.53/10.03 % (2694149)Instruction limit reached!
% 64.53/10.03 % (2694149)------------------------------
% 64.53/10.03 % (2694149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.03 % (2694149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.03 % (2694149)CaDiCaL version: 2.1.3
% 64.53/10.03 % (2694149)Termination reason: Instruction limit
% 64.53/10.03 % (2694149)Termination phase: Saturation
% 64.53/10.03 % (2694149)Time elapsed: 0.167 s
% 64.53/10.03 % (2694149)Peak memory usage: 92 MB
% 64.53/10.03 % (2694149)Instructions burned: 274 (million)
% 64.53/10.03 % (2694141)Instruction limit reached!
% 64.53/10.03 % (2694141)------------------------------
% 64.53/10.03 % (2694141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.03 % (2694141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.03 % (2694141)CaDiCaL version: 2.1.3
% 64.53/10.03 % (2694141)Termination reason: Instruction limit
% 64.53/10.03 % (2694141)Termination phase: Saturation
% 64.53/10.03 % (2694141)Time elapsed: 0.499 s
% 64.53/10.03 % (2694141)Peak memory usage: 119 MB
% 64.53/10.03 % (2694141)Instructions burned: 868 (million)
% 64.53/10.03 % (2694151)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1092689994:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2949 on theBenchmark for (2949ds/863Mi)
% 64.53/10.04 % (2694152)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1401275942:i=5811:kws=precedence:nm=0:rtra=on_2949 on theBenchmark for (2949ds/5811Mi)
% 64.53/10.04 % (2694153)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=291588659:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2949 on theBenchmark for (2949ds/2216Mi)
% 64.53/10.04 % (2694094)Instruction limit reached!
% 64.53/10.04 % (2694094)------------------------------
% 64.53/10.04 % (2694094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.04 % (2694094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.04 % (2694094)CaDiCaL version: 2.1.3
% 64.53/10.04 % (2694094)Termination reason: Instruction limit
% 64.53/10.04 % (2694094)Termination phase: Saturation
% 64.53/10.04 % (2694094)Time elapsed: 2.435 s
% 64.53/10.04 % (2694094)Peak memory usage: 112 MB
% 64.53/10.04 % (2694094)Instructions burned: 4430 (million)
% 64.53/10.04 % (2694157)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4042953726:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi)
% 64.53/10.04 % (2694142)Instruction limit reached!
% 64.53/10.04 % (2694142)------------------------------
% 64.53/10.04 % (2694142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.04 % (2694142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.04 % (2694142)CaDiCaL version: 2.1.3
% 64.53/10.04 % (2694142)Termination reason: Instruction limit
% 64.53/10.04 % (2694142)Termination phase: Saturation
% 64.53/10.04 % (2694142)Time elapsed: 1.005 s
% 64.53/10.04 % (2694142)Peak memory usage: 100 MB
% 64.53/10.04 % (2694142)Instructions burned: 1846 (million)
% 64.53/10.04 % (2694151)Instruction limit reached!
% 64.53/10.04 % (2694151)------------------------------
% 64.53/10.04 % (2694151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.53/10.04 % (2694151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.53/10.04 % (2694151)CaDiCaL version: 2.1.3
% 64.53/10.04 % (2694151)Termination reason: Instruction limit
% 64.53/10.04 % (2694151)Termination phase: Saturation
% 101.15/15.06 % (2694151)Time elapsed: 0.497 s
% 101.15/15.06 % (2694151)Peak memory usage: 119 MB
% 101.15/15.06 % (2694151)Instructions burned: 864 (million)
% 101.15/15.06 % (2694157)Instruction limit reached!
% 101.15/15.06 % (2694157)------------------------------
% 101.15/15.06 % (2694157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.15/15.06 % (2694157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/15.06 % (2694157)CaDiCaL version: 2.1.3
% 101.15/15.06 % (2694157)Termination reason: Instruction limit
% 101.15/15.06 % (2694157)Termination phase: Saturation
% 101.15/15.06 % (2694157)Time elapsed: 0.554 s
% 101.15/15.06 % (2694157)Peak memory usage: 98 MB
% 101.15/15.06 % (2694157)Instructions burned: 803 (million)
% 101.15/15.06 % (2694161)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3219194819:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2940 on theBenchmark for (2940ds/2127Mi)
% 101.15/15.06 % (2694159)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4265368361:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2944 on theBenchmark for (2944ds/1026Mi)
% 101.15/15.06 % (2694160)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1691251113:i=3509:rtra=on_2943 on theBenchmark for (2943ds/3509Mi)
% 101.15/15.06 % (2694153)Instruction limit reached!
% 101.15/15.06 % (2694153)------------------------------
% 101.15/15.06 % (2694153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.15/15.06 % (2694153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/15.06 % (2694153)CaDiCaL version: 2.1.3
% 101.15/15.06 % (2694153)Termination reason: Instruction limit
% 101.15/15.06 % (2694153)Termination phase: Saturation
% 101.15/15.06 % (2694153)Time elapsed: 1.193 s
% 101.15/15.06 % (2694153)Peak memory usage: 127 MB
% 101.15/15.06 % (2694153)Instructions burned: 2216 (million)
% 101.15/15.06 % (2694165)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1409149801:i=1959:rtra=on:fsd=on:proc=on_2936 on theBenchmark for (2936ds/1959Mi)
% 101.15/15.06 % (2694159)Instruction limit reached!
% 101.15/15.06 % (2694159)------------------------------
% 101.15/15.06 % (2694159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.15/15.06 % (2694159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/15.06 % (2694159)CaDiCaL version: 2.1.3
% 101.15/15.06 % (2694159)Termination reason: Instruction limit
% 101.15/15.06 % (2694159)Termination phase: Saturation
% 101.15/15.06 % (2694159)Time elapsed: 0.444 s
% 101.15/15.06 % (2694159)Peak memory usage: 90 MB
% 101.15/15.06 % (2694159)Instructions burned: 1026 (million)
% 101.15/15.06 % (2694167)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2442092716:s2a=on:i=3553:nm=0:rtra=on_2932 on theBenchmark for (2932ds/3553Mi)
% 101.15/15.06 % (2694161)Instruction limit reached!
% 101.15/15.06 % (2694161)------------------------------
% 101.15/15.06 % (2694161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.15/15.06 % (2694161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/15.06 % (2694161)CaDiCaL version: 2.1.3
% 101.15/15.06 % (2694161)Termination reason: Instruction limit
% 101.15/15.06 % (2694161)Termination phase: Saturation
% 101.15/15.06 % (2694161)Time elapsed: 1.105 s
% 101.15/15.06 % (2694161)Peak memory usage: 91 MB
% 101.15/15.06 % (2694161)Instructions burned: 2127 (million)
% 101.15/15.06 % (2694170)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3273586034:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2926 on theBenchmark for (2926ds/3201Mi)
% 101.15/15.06 % (2694165)Instruction limit reached!
% 101.15/15.06 % (2694165)------------------------------
% 101.15/15.06 % (2694165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.15/15.06 % (2694165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.15/15.06 % (2694165)CaDiCaL version: 2.1.3
% 101.15/15.06 % (2694165)Termination reason: Instruction limit
% 101.15/15.06 % (2694165)Termination phase: Saturation
% 101.15/15.06 % (2694165)Time elapsed: 1.152 s
% 101.15/15.06 % (2694165)Peak memory usage: 127 MB
% 101.15/15.06 % (2694165)Instructions burned: 1960 (million)
% 101.15/15.06 % (2694172)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=856837506:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2923 on theBenchmark for (2923ds/4093Mi)
% 101.15/15.06 % (2694140)Instruction limit reached!
% 118.46/17.63 % (2694140)------------------------------
% 118.46/17.63 % (2694140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694140)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694140)Termination reason: Instruction limit
% 118.46/17.63 % (2694140)Termination phase: Saturation
% 118.46/17.63 % (2694140)Time elapsed: 3.461 s
% 118.46/17.63 % (2694140)Peak memory usage: 117 MB
% 118.46/17.63 % (2694140)Instructions burned: 6401 (million)
% 118.46/17.63 % (2694174)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=3684377848:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2920 on theBenchmark for (2920ds/21173Mi)
% 118.46/17.63 % (2694160)Instruction limit reached!
% 118.46/17.63 % (2694160)------------------------------
% 118.46/17.63 % (2694160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694160)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694160)Termination reason: Instruction limit
% 118.46/17.63 % (2694160)Termination phase: Saturation
% 118.46/17.63 % (2694160)Time elapsed: 1.932 s
% 118.46/17.63 % (2694160)Peak memory usage: 110 MB
% 118.46/17.63 % (2694160)Instructions burned: 3510 (million)
% 118.46/17.63 % (2694152)Instruction limit reached!
% 118.46/17.63 % (2694152)------------------------------
% 118.46/17.63 % (2694152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694152)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694152)Termination reason: Instruction limit
% 118.46/17.63 % (2694152)Termination phase: Saturation
% 118.46/17.63 % (2694152)Time elapsed: 3.128 s
% 118.46/17.63 % (2694152)Peak memory usage: 133 MB
% 118.46/17.63 % (2694152)Instructions burned: 5811 (million)
% 118.46/17.63 % (2694176)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1405709723:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2918 on theBenchmark for (2918ds/10544Mi)
% 118.46/17.63 % (2694177)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3638276910:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2916 on theBenchmark for (2916ds/1262Mi)
% 118.46/17.63 % (2694170)Instruction limit reached!
% 118.46/17.63 % (2694170)------------------------------
% 118.46/17.63 % (2694170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694170)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694170)Termination reason: Instruction limit
% 118.46/17.63 % (2694170)Termination phase: Saturation
% 118.46/17.63 % (2694170)Time elapsed: 1.544 s
% 118.46/17.63 % (2694170)Peak memory usage: 92 MB
% 118.46/17.63 % (2694170)Instructions burned: 3202 (million)
% 118.46/17.63 % (2694167)Instruction limit reached!
% 118.46/17.63 % (2694167)------------------------------
% 118.46/17.63 % (2694167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694167)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694167)Termination reason: Instruction limit
% 118.46/17.63 % (2694167)Termination phase: Saturation
% 118.46/17.63 % (2694167)Time elapsed: 2.340 s
% 118.46/17.63 % (2694167)Peak memory usage: 107 MB
% 118.46/17.63 % (2694167)Instructions burned: 3554 (million)
% 118.46/17.63 % (2694177)Instruction limit reached!
% 118.46/17.63 % (2694177)------------------------------
% 118.46/17.63 % (2694177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.46/17.63 % (2694177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.46/17.63 % (2694177)CaDiCaL version: 2.1.3
% 118.46/17.63 % (2694177)Termination reason: Instruction limit
% 118.46/17.63 % (2694177)Termination phase: Saturation
% 118.46/17.63 % (2694177)Time elapsed: 0.757 s
% 118.46/17.63 % (2694177)Peak memory usage: 124 MB
% 118.46/17.63 % (2694177)Instructions burned: 1262 (million)
% 118.46/17.63 % (2694180)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=4147888944:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2909 on theBenchmark for (2909ds/775Mi)
% 118.46/17.63 % (2694181)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4202996192:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2907 on theBenchmark for (2907ds/270Mi)
% 124.31/18.36 % (2694182)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3155068695:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2907 on theBenchmark for (2907ds/17165Mi)
% 124.31/18.36 % (2694181)Instruction limit reached!
% 124.31/18.36 % (2694181)------------------------------
% 124.31/18.36 % (2694181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694181)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694181)Termination reason: Instruction limit
% 124.31/18.36 % (2694181)Termination phase: Saturation
% 124.31/18.36 % (2694181)Time elapsed: 0.160 s
% 124.31/18.36 % (2694181)Peak memory usage: 91 MB
% 124.31/18.36 % (2694181)Instructions burned: 271 (million)
% 124.31/18.36 % (2694186)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=386734694:s2a=on:i=13094:s2at=-1:rtra=on_2904 on theBenchmark for (2904ds/13094Mi)
% 124.31/18.36 % (2694180)Instruction limit reached!
% 124.31/18.36 % (2694180)------------------------------
% 124.31/18.36 % (2694180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694180)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694180)Termination reason: Instruction limit
% 124.31/18.36 % (2694180)Termination phase: Saturation
% 124.31/18.36 % (2694180)Time elapsed: 0.529 s
% 124.31/18.36 % (2694180)Peak memory usage: 97 MB
% 124.31/18.36 % (2694180)Instructions burned: 776 (million)
% 124.31/18.36 % (2694188)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=1037289870:st=2:i=12633:rtra=on:ss=axioms_2902 on theBenchmark for (2902ds/12633Mi)
% 124.31/18.36 % (2694172)Instruction limit reached!
% 124.31/18.36 % (2694172)------------------------------
% 124.31/18.36 % (2694172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694172)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694172)Termination reason: Instruction limit
% 124.31/18.36 % (2694172)Termination phase: Saturation
% 124.31/18.36 % (2694172)Time elapsed: 2.279 s
% 124.31/18.36 % (2694172)Peak memory usage: 148 MB
% 124.31/18.36 % (2694172)Instructions burned: 4093 (million)
% 124.31/18.36 % (2694190)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=1626985490:i=1783:rtra=on:gtg=position_2898 on theBenchmark for (2898ds/1783Mi)
% 124.31/18.36 % (2694190)Instruction limit reached!
% 124.31/18.36 % (2694190)------------------------------
% 124.31/18.36 % (2694190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694190)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694190)Termination reason: Instruction limit
% 124.31/18.36 % (2694190)Termination phase: Saturation
% 124.31/18.36 % (2694190)Time elapsed: 1.001 s
% 124.31/18.36 % (2694190)Peak memory usage: 123 MB
% 124.31/18.36 % (2694190)Instructions burned: 1783 (million)
% 124.31/18.36 % (2694192)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=3729794963:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2886 on theBenchmark for (2886ds/5451Mi)
% 124.31/18.36 % (2694192)Instruction limit reached!
% 124.31/18.36 % (2694192)------------------------------
% 124.31/18.36 % (2694192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694192)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694192)Termination reason: Instruction limit
% 124.31/18.36 % (2694192)Termination phase: Saturation
% 124.31/18.36 % (2694192)Time elapsed: 2.857 s
% 124.31/18.36 % (2694192)Peak memory usage: 130 MB
% 124.31/18.36 % (2694192)Instructions burned: 5451 (million)
% 124.31/18.36 % (2694144)Instruction limit reached!
% 124.31/18.36 % (2694144)------------------------------
% 124.31/18.36 % (2694144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694144)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694144)Termination reason: Instruction limit
% 124.31/18.36 % (2694144)Termination phase: Saturation
% 124.31/18.36 % (2694144)Time elapsed: 9.860 s
% 124.31/18.36 % (2694144)Peak memory usage: 113 MB
% 124.31/18.36 % (2694144)Instructions burned: 36820 (million)
% 124.31/18.36 % (2694194)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=556667305:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2856 on theBenchmark for (2856ds/4975Mi)
% 124.31/18.36 % (2694195)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3812381262:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2856 on theBenchmark for (2856ds/2076Mi)
% 124.31/18.36 % (2694176)Instruction limit reached!
% 124.31/18.36 % (2694176)------------------------------
% 124.31/18.36 % (2694176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694176)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694176)Termination reason: Instruction limit
% 124.31/18.36 % (2694176)Termination phase: Saturation
% 124.31/18.36 % (2694176)Time elapsed: 6.640 s
% 124.31/18.36 % (2694176)Peak memory usage: 200 MB
% 124.31/18.36 % (2694176)Instructions burned: 10544 (million)
% 124.31/18.36 % (2694198)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3616338818:i=5145:rtra=on_2849 on theBenchmark for (2849ds/5145Mi)
% 124.31/18.36 % (2694195)Instruction limit reached!
% 124.31/18.36 % (2694195)------------------------------
% 124.31/18.36 % (2694195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694195)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694195)Termination reason: Instruction limit
% 124.31/18.36 % (2694195)Termination phase: Saturation
% 124.31/18.36 % (2694195)Time elapsed: 0.664 s
% 124.31/18.36 % (2694195)Peak memory usage: 125 MB
% 124.31/18.36 % (2694195)Instructions burned: 2079 (million)
% 124.31/18.36 % (2694200)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=4277926397:i=3509:rtra=on_2848 on theBenchmark for (2848ds/3509Mi)
% 124.31/18.36 % (2694200)Instruction limit reached!
% 124.31/18.36 % (2694200)------------------------------
% 124.31/18.36 % (2694200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694200)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694200)Termination reason: Instruction limit
% 124.31/18.36 % (2694200)Termination phase: Saturation
% 124.31/18.36 % (2694200)Time elapsed: 1.037 s
% 124.31/18.36 % (2694200)Peak memory usage: 112 MB
% 124.31/18.36 % (2694200)Instructions burned: 3513 (million)
% 124.31/18.36 % (2694202)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2812419409:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2836 on theBenchmark for (2836ds/13800Mi)
% 124.31/18.36 % (2694188)Instruction limit reached!
% 124.31/18.36 % (2694188)------------------------------
% 124.31/18.36 % (2694188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694188)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694188)Termination reason: Instruction limit
% 124.31/18.36 % (2694188)Termination phase: Saturation
% 124.31/18.36 % (2694188)Time elapsed: 6.770 s
% 124.31/18.36 % (2694188)Peak memory usage: 150 MB
% 124.31/18.36 % (2694188)Instructions burned: 12633 (million)
% 124.31/18.36 % (2694186)Instruction limit reached!
% 124.31/18.36 % (2694186)------------------------------
% 124.31/18.36 % (2694186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694186)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694186)Termination reason: Instruction limit
% 124.31/18.36 % (2694186)Termination phase: Saturation
% 124.31/18.36 % (2694186)Time elapsed: 7.092 s
% 124.31/18.36 % (2694186)Peak memory usage: 139 MB
% 124.31/18.36 % (2694186)Instructions burned: 13094 (million)
% 124.31/18.36 % (2694204)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1036922540:i=1412:rtra=on:fsd=on:proc=on_2832 on theBenchmark for (2832ds/1412Mi)
% 124.31/18.36 % (2694205)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
% 124.31/18.36 % (2694205)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3530716410:i=11747:aac=none:nm=0:rtra=on:rawr=on_2831 on theBenchmark for (2831ds/11747Mi)
% 124.31/18.36 % (2694194)Instruction limit reached!
% 124.31/18.36 % (2694194)------------------------------
% 124.31/18.36 % (2694194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.31/18.36 % (2694194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.31/18.36 % (2694194)CaDiCaL version: 2.1.3
% 124.31/18.36 % (2694194)Termination reason: Instruction limit
% 124.31/18.36 % (2694194)Termination phase: Saturation
% 124.31/18.36 % (2694194)Time elapsed: 2.600 s
% 124.31/18.36 % (2694194)Peak memory usage: 127 MB
% 124.31/18.36 % (2694194)Instructions burned: 4976 (million)
% 124.31/18.36 % (2694208)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1153636836:s2a=on:i=3553:nm=0:rtra=on_2829 on theBenchmark for (2829ds/3553Mi)
% 124.31/18.36 % (2694204)First to succeed.
% 124.31/18.36 % (2694204)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2693950"
% 124.31/18.36 % (2694204)Refutation found. Thanks to Tanya!
% 124.31/18.36 % SZS status Theorem for theBenchmark
% 124.31/18.36 % SZS output start Proof for theBenchmark
% See solution above
% 124.67/18.45 % (2694204)------------------------------
% 124.67/18.45 % (2694204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.67/18.45 % (2694204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.67/18.45 % (2694204)CaDiCaL version: 2.1.3
% 124.67/18.45 % (2694204)Termination reason: Refutation
% 124.67/18.45 % (2694204)Time elapsed: 0.513 s
% 124.67/18.45 % (2694204)Peak memory usage: 122 MB
% 124.67/18.45 % (2694204)Instructions burned: 854 (million)
% 124.67/18.45 % (2694204)------------------------------
% 124.67/18.45 % (2694204)------------------------------
% 124.67/18.45 % (2693950)Success in time 17.69 s
% 124.67/18.45 % Vampire exiting
%------------------------------------------------------------------------------