%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM861_1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 12:17:19 PM UTC 2026
% Result : Theorem 10.80s 2.67s
% Output : Refutation 11.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 37
% Syntax : Number of formulae : 174 ( 1 unt; 0 typ; 29 def)
% Number of atoms : 484 ( 13 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 506 ( 196 ~; 199 |; 55 &)
% ( 49 <=>; 6 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 378 ( 119 atm; 32 fun; 0 num; 227 var)
% Number of types : 2 ( 0 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 38 ( 34 usr; 30 prp; 0-3 aty)
% Number of functors : 13 ( 12 usr; 7 con; 0-3 aty)
% Number of variables : 227 ( 207 !; 20 ?; 227 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
c: $int ).
tff(func_def_1,type,
summation: $int > $int ).
tff(func_def_2,type,
max: ( $int * $int ) > $int ).
tff(func_def_4,type,
sK0: ( $int * $int * $int ) > $int ).
tff(func_def_5,type,
sK1: ( $int * $int * $int ) > $int ).
tff(func_def_6,type,
sK2: $int ).
tff(func_def_7,type,
sK3: $int ).
tff(func_def_8,type,
sK4: $int ).
tff(func_def_9,type,
sK5: ( $int * $int * $int ) > $int ).
tff(func_def_11,type,
'$inst7': $int ).
tff(func_def_12,type,
'$inst8': $int ).
tff(func_def_15,type,
'$inst9': $int ).
tff(pred_def_1,type,
ub: ( $int * $int * $int ) > $o ).
tff(pred_def_2,type,
model_max: ( $int * $int * $int ) > $o ).
tff(pred_def_3,type,
model_ub: ( $int * $int * $int ) > $o ).
tff(pred_def_4,type,
minsol_model_max: ( $int * $int * $int ) > $o ).
tff(pred_def_5,type,
minsol_model_ub: ( $int * $int * $int ) > $o ).
tff(f2,axiom,
! [X1: $int,X0: $int] :
( ~ $lesseq(X1,X0)
| ( max(X0,X1) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_1) ).
tff(f3,axiom,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X1 )
| ~ $lesseq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_2) ).
tff(f4,axiom,
! [X2: $int,X0: $int,X1: $int] :
( ub(X0,X1,X2)
<=> ( $lesseq(X1,X2)
& $lesseq(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ub) ).
tff(f5,axiom,
! [X2: $int,X0: $int,X1: $int] :
( $lesseq($sum(c,max(X0,X1)),X2)
<=> model_max(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_max_4) ).
tff(f6,axiom,
! [X1: $int,X0: $int,X2: $int] :
( model_ub(X0,X1,X2)
<=> ? [X3: $int] :
( ub(X0,X1,X3)
& $lesseq($sum(c,X3),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_ub_4) ).
tff(f7,axiom,
! [X1: $int,X0: $int,X2: $int] :
( ( model_max(X0,X1,X2)
& ! [X3: $int] :
( model_max(X0,X1,X3)
=> $lesseq(X2,X3) ) )
<=> minsol_model_max(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_max) ).
tff(f8,axiom,
! [X2: $int,X1: $int,X0: $int] :
( minsol_model_ub(X0,X1,X2)
<=> ( model_ub(X0,X1,X2)
& ! [X3: $int] :
( model_ub(X0,X1,X3)
=> $lesseq(X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_ub) ).
tff(f9,conjecture,
! [X0: $int,X2: $int,X1: $int] :
( minsol_model_max(X0,X1,X2)
<=> minsol_model_ub(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_is_ub_1) ).
tff(f10,negated_conjecture,
~ ! [X0: $int,X2: $int,X1: $int] :
( minsol_model_max(X0,X1,X2)
<=> minsol_model_ub(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f9]) ).
tff(f11,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X2,$sum(c,max(X0,X1)))
<=> model_max(X0,X1,X2) ),
inference(theory_normalization,[],[f5]) ).
tff(f12,plain,
! [X1: $int,X0: $int] :
( $less(X0,X1)
| ( max(X0,X1) = X0 ) ),
inference(theory_normalization,[],[f2]) ).
tff(f13,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X0,X1,X2)
<=> ( ~ $less(X2,X1)
& ~ $less(X2,X0) ) ),
inference(theory_normalization,[],[f4]) ).
tff(f15,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( model_max(X0,X1,X2)
& ! [X3: $int] :
( model_max(X0,X1,X3)
=> ~ $less(X3,X2) ) )
<=> minsol_model_max(X0,X1,X2) ),
inference(theory_normalization,[],[f7]) ).
tff(f16,plain,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X1 )
| $less(X1,X0) ),
inference(theory_normalization,[],[f3]) ).
tff(f17,plain,
! [X2: $int,X1: $int,X0: $int] :
( minsol_model_ub(X0,X1,X2)
<=> ( model_ub(X0,X1,X2)
& ! [X3: $int] :
( model_ub(X0,X1,X3)
=> ~ $less(X3,X2) ) ) ),
inference(theory_normalization,[],[f8]) ).
tff(f18,plain,
! [X1: $int,X0: $int,X2: $int] :
( model_ub(X0,X1,X2)
<=> ? [X3: $int] :
( ub(X0,X1,X3)
& ~ $less(X2,$sum(c,X3)) ) ),
inference(theory_normalization,[],[f6]) ).
tff(f19,plain,
! [X0: $int,X2: $int,X1: $int] :
( ~ $less(X0,$sum(c,max(X1,X2)))
<=> model_max(X1,X2,X0) ),
inference(rectify,[],[f11]) ).
tff(f20,plain,
~ ! [X2: $int,X1: $int,X0: $int] :
( minsol_model_max(X0,X2,X1)
<=> minsol_model_ub(X0,X2,X1) ),
inference(rectify,[],[f10]) ).
tff(f21,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| $less(X1,X0) ),
inference(rectify,[],[f12]) ).
tff(f22,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ~ $less(X0,X2)
& ~ $less(X0,X1) )
<=> ub(X1,X2,X0) ),
inference(rectify,[],[f13]) ).
tff(f23,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ! [X3: $int] :
( model_max(X1,X0,X3)
=> ~ $less(X3,X2) )
& model_max(X1,X0,X2) )
<=> minsol_model_max(X1,X0,X2) ),
inference(rectify,[],[f15]) ).
tff(f24,plain,
! [X1: $int,X0: $int] :
( ( max(X1,X0) = X0 )
| $less(X0,X1) ),
inference(rectify,[],[f16]) ).
tff(f25,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( model_ub(X2,X1,X0)
& ! [X3: $int] :
( model_ub(X2,X1,X3)
=> ~ $less(X3,X0) ) )
<=> minsol_model_ub(X2,X1,X0) ),
inference(rectify,[],[f17]) ).
tff(f26,plain,
! [X1: $int,X2: $int,X0: $int] :
( ? [X3: $int] :
( ub(X1,X0,X3)
& ~ $less(X2,$sum(c,X3)) )
<=> model_ub(X1,X0,X2) ),
inference(rectify,[],[f18]) ).
tff(f27,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( model_max(X1,X0,X2)
& ! [X3: $int] :
( ~ model_max(X1,X0,X3)
| ~ $less(X3,X2) ) )
<=> minsol_model_max(X1,X0,X2) ),
inference(ennf_transformation,[],[f23]) ).
tff(f28,plain,
! [X1: $int,X0: $int,X2: $int] :
( minsol_model_ub(X2,X1,X0)
<=> ( model_ub(X2,X1,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X2,X1,X3) ) ) ),
inference(ennf_transformation,[],[f25]) ).
tff(f29,plain,
? [X0: $int,X2: $int,X1: $int] :
( minsol_model_max(X0,X2,X1)
<~> minsol_model_ub(X0,X2,X1) ),
inference(ennf_transformation,[],[f20]) ).
tff(f31,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( ( model_max(X1,X0,X2)
& ! [X3: $int] :
( ~ model_max(X1,X0,X3)
| ~ $less(X3,X2) ) )
| ~ minsol_model_max(X1,X0,X2) )
& ( minsol_model_max(X1,X0,X2)
| ~ model_max(X1,X0,X2)
| ? [X3: $int] :
( model_max(X1,X0,X3)
& $less(X3,X2) ) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f32,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( ( model_max(X1,X0,X2)
& ! [X3: $int] :
( ~ model_max(X1,X0,X3)
| ~ $less(X3,X2) ) )
| ~ minsol_model_max(X1,X0,X2) )
& ( minsol_model_max(X1,X0,X2)
| ~ model_max(X1,X0,X2)
| ? [X3: $int] :
( model_max(X1,X0,X3)
& $less(X3,X2) ) ) ),
inference(flattening,[],[f31]) ).
tff(f33,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X2,X1,X0)
& ! [X3: $int] :
( ~ model_max(X2,X1,X3)
| ~ $less(X3,X0) ) )
| ~ minsol_model_max(X2,X1,X0) )
& ( minsol_model_max(X2,X1,X0)
| ~ model_max(X2,X1,X0)
| ? [X4: $int] :
( model_max(X2,X1,X4)
& $less(X4,X0) ) ) ),
inference(rectify,[],[f32]) ).
tff(f34,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X2,X1,X0)
& ! [X3: $int] :
( ~ model_max(X2,X1,X3)
| ~ $less(X3,X0) ) )
| ~ minsol_model_max(X2,X1,X0) )
& ( minsol_model_max(X2,X1,X0)
| ~ model_max(X2,X1,X0)
| ( model_max(X2,X1,sK0(X0,X1,X2))
& $less(sK0(X0,X1,X2),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X4,sK0(X0,X1,X2))],[f33]) ).
tff(f35,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( minsol_model_ub(X2,X1,X0)
| ~ model_ub(X2,X1,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_ub(X2,X1,X3) ) )
& ( ( model_ub(X2,X1,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X2,X1,X3) ) )
| ~ minsol_model_ub(X2,X1,X0) ) ),
inference(nnf_transformation,[],[f28]) ).
tff(f36,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( minsol_model_ub(X2,X1,X0)
| ~ model_ub(X2,X1,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_ub(X2,X1,X3) ) )
& ( ( model_ub(X2,X1,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X2,X1,X3) ) )
| ~ minsol_model_ub(X2,X1,X0) ) ),
inference(flattening,[],[f35]) ).
tff(f37,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X2,X0,X1)
| ~ model_ub(X2,X0,X1)
| ? [X3: $int] :
( $less(X3,X1)
& model_ub(X2,X0,X3) ) )
& ( ( model_ub(X2,X0,X1)
& ! [X4: $int] :
( ~ $less(X4,X1)
| ~ model_ub(X2,X0,X4) ) )
| ~ minsol_model_ub(X2,X0,X1) ) ),
inference(rectify,[],[f36]) ).
tff(f38,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X2,X0,X1)
| ~ model_ub(X2,X0,X1)
| ( $less(sK1(X0,X1,X2),X1)
& model_ub(X2,X0,sK1(X0,X1,X2)) ) )
& ( ( model_ub(X2,X0,X1)
& ! [X4: $int] :
( ~ $less(X4,X1)
| ~ model_ub(X2,X0,X4) ) )
| ~ minsol_model_ub(X2,X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f37]) ).
tff(f39,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ( ~ $less(X0,X2)
& ~ $less(X0,X1) )
| ~ ub(X1,X2,X0) )
& ( ub(X1,X2,X0)
| $less(X0,X2)
| $less(X0,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f40,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ( ~ $less(X0,X2)
& ~ $less(X0,X1) )
| ~ ub(X1,X2,X0) )
& ( ub(X1,X2,X0)
| $less(X0,X2)
| $less(X0,X1) ) ),
inference(flattening,[],[f39]) ).
tff(f41,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( ~ $less(X0,X1)
& ~ $less(X0,X2) )
| ~ ub(X2,X1,X0) )
& ( ub(X2,X1,X0)
| $less(X0,X1)
| $less(X0,X2) ) ),
inference(rectify,[],[f40]) ).
tff(f42,plain,
! [X0: $int,X1: $int] :
( ( max(X0,X1) = X1 )
| $less(X1,X0) ),
inference(rectify,[],[f24]) ).
tff(f43,plain,
? [X0: $int,X2: $int,X1: $int] :
( ( ~ minsol_model_ub(X0,X2,X1)
| ~ minsol_model_max(X0,X2,X1) )
& ( minsol_model_ub(X0,X2,X1)
| minsol_model_max(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f29]) ).
tff(f44,plain,
? [X0: $int,X1: $int,X2: $int] :
( ( ~ minsol_model_ub(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) )
& ( minsol_model_ub(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ) ),
inference(rectify,[],[f43]) ).
tff(f45,plain,
( ( ~ minsol_model_ub(sK2,sK3,sK4)
| ~ minsol_model_max(sK2,sK3,sK4) )
& ( minsol_model_ub(sK2,sK3,sK4)
| minsol_model_max(sK2,sK3,sK4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f44]) ).
tff(f46,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ~ $less(X0,$sum(c,max(X1,X2)))
| ~ model_max(X1,X2,X0) )
& ( model_max(X1,X2,X0)
| $less(X0,$sum(c,max(X1,X2))) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f47,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ~ $less(X0,$sum(c,max(X2,X1)))
| ~ model_max(X2,X1,X0) )
& ( model_max(X2,X1,X0)
| $less(X0,$sum(c,max(X2,X1))) ) ),
inference(rectify,[],[f46]) ).
tff(f48,plain,
! [X1: $int,X2: $int,X0: $int] :
( ( ? [X3: $int] :
( ub(X1,X0,X3)
& ~ $less(X2,$sum(c,X3)) )
| ~ model_ub(X1,X0,X2) )
& ( model_ub(X1,X0,X2)
| ! [X3: $int] :
( ~ ub(X1,X0,X3)
| $less(X2,$sum(c,X3)) ) ) ),
inference(nnf_transformation,[],[f26]) ).
tff(f49,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ? [X3: $int] :
( ub(X0,X2,X3)
& ~ $less(X1,$sum(c,X3)) )
| ~ model_ub(X0,X2,X1) )
& ( model_ub(X0,X2,X1)
| ! [X4: $int] :
( ~ ub(X0,X2,X4)
| $less(X1,$sum(c,X4)) ) ) ),
inference(rectify,[],[f48]) ).
tff(f50,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( ub(X0,X2,sK5(X0,X1,X2))
& ~ $less(X1,$sum(c,sK5(X0,X1,X2))) )
| ~ model_ub(X0,X2,X1) )
& ( model_ub(X0,X2,X1)
| ! [X4: $int] :
( ~ ub(X0,X2,X4)
| $less(X1,$sum(c,X4)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f49]) ).
tff(f53,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK0(X0,X1,X2),X0)
| minsol_model_max(X2,X1,X0)
| ~ model_max(X2,X1,X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f54,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_max(X2,X1,sK0(X0,X1,X2))
| ~ model_max(X2,X1,X0)
| minsol_model_max(X2,X1,X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f55,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ minsol_model_max(X2,X1,X0)
| ~ $less(X3,X0)
| ~ model_max(X2,X1,X3) ),
inference(cnf_transformation,[],[f34]) ).
tff(f56,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_max(X2,X1,X0)
| model_max(X2,X1,X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f57,plain,
! [X2: $int,X0: $int,X1: $int,X4: $int] :
( ~ minsol_model_ub(X2,X0,X1)
| ~ model_ub(X2,X0,X4)
| ~ $less(X4,X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f58,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_ub(X2,X0,X1)
| model_ub(X2,X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f59,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_ub(X2,X0,sK1(X0,X1,X2))
| ~ model_ub(X2,X0,X1)
| minsol_model_ub(X2,X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f60,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK1(X0,X1,X2),X1)
| ~ model_ub(X2,X0,X1)
| minsol_model_ub(X2,X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f61,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X2,X1,X0)
| $less(X0,X2)
| $less(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
tff(f62,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X2,X1,X0)
| ~ $less(X0,X2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f63,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X2,X1,X0)
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
tff(f64,plain,
! [X0: $int,X1: $int] :
( ( max(X0,X1) = X1 )
| $less(X1,X0) ),
inference(cnf_transformation,[],[f42]) ).
tff(f65,plain,
( minsol_model_ub(sK2,sK3,sK4)
| minsol_model_max(sK2,sK3,sK4) ),
inference(cnf_transformation,[],[f45]) ).
tff(f66,plain,
( ~ minsol_model_max(sK2,sK3,sK4)
| ~ minsol_model_ub(sK2,sK3,sK4) ),
inference(cnf_transformation,[],[f45]) ).
tff(f67,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X0,$sum(c,max(X2,X1)))
| model_max(X2,X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f68,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X0,$sum(c,max(X2,X1)))
| ~ model_max(X2,X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f69,plain,
! [X2: $int,X0: $int,X1: $int,X4: $int] :
( $less(X1,$sum(c,X4))
| ~ ub(X0,X2,X4)
| model_ub(X0,X2,X1) ),
inference(cnf_transformation,[],[f50]) ).
tff(f70,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,$sum(c,sK5(X0,X1,X2)))
| ~ model_ub(X0,X2,X1) ),
inference(cnf_transformation,[],[f50]) ).
tff(f71,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X0,X2,sK5(X0,X1,X2))
| ~ model_ub(X0,X2,X1) ),
inference(cnf_transformation,[],[f50]) ).
tff(f72,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| $less(X1,X0) ),
inference(cnf_transformation,[],[f21]) ).
tff(f74,definition,
( spl6_1
<=> minsol_model_ub(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
tff(f75,plain,
( ~ minsol_model_ub(sK2,sK3,sK4)
| spl6_1 ),
inference(avatar_component_clause,[],[f74]) ).
tff(f76,plain,
( minsol_model_ub(sK2,sK3,sK4)
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f74]) ).
tff(f78,definition,
( spl6_2
<=> minsol_model_max(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
tff(f79,plain,
( ~ minsol_model_max(sK2,sK3,sK4)
| spl6_2 ),
inference(avatar_component_clause,[],[f78]) ).
tff(f80,plain,
( minsol_model_max(sK2,sK3,sK4)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f78]) ).
tff(f81,plain,
( spl6_1
| spl6_2 ),
inference(avatar_split_clause,[],[f65,f78,f74]) ).
tff(f82,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f66,f78,f74]) ).
tff(f84,plain,
( model_ub(sK2,sK3,sK4)
| ~ spl6_1 ),
inference(resolution,[],[f58,f76]) ).
tff(f86,definition,
( spl6_3
<=> model_ub(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
tff(f87,plain,
( ~ model_ub(sK2,sK3,sK4)
| spl6_3 ),
inference(avatar_component_clause,[],[f86]) ).
tff(f88,plain,
( model_ub(sK2,sK3,sK4)
| ~ spl6_3 ),
inference(avatar_component_clause,[],[f86]) ).
tff(f89,plain,
( spl6_3
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f84,f74,f86]) ).
tff(f156,plain,
( ub(sK2,sK3,sK5(sK2,sK4,sK3))
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f71,f88]) ).
tff(f157,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK5(X0,X2,X1),X1)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f71,f63]) ).
tff(f158,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK5(X0,X2,X1),X0)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f71,f62]) ).
tff(f160,definition,
( spl6_9
<=> ub(sK2,sK3,sK5(sK2,sK4,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
tff(f162,plain,
( ub(sK2,sK3,sK5(sK2,sK4,sK3))
| ~ spl6_9 ),
inference(avatar_component_clause,[],[f160]) ).
tff(f163,plain,
( spl6_9
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f156,f86,f160]) ).
tff(f164,plain,
( ~ $less(sK5(sK2,sK4,sK3),sK3)
| ~ spl6_9 ),
inference(unit_resulting_resolution,[],[f63,f162]) ).
tff(f165,plain,
( ~ $less(sK5(sK2,sK4,sK3),sK2)
| ~ spl6_9 ),
inference(unit_resulting_resolution,[],[f62,f162]) ).
tff(f169,definition,
( spl6_10
<=> $less(sK5(sK2,sK4,sK3),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
tff(f172,plain,
( ~ spl6_10
| ~ spl6_9 ),
inference(avatar_split_clause,[],[f165,f160,f169]) ).
tff(f174,definition,
( spl6_11
<=> $less(sK5(sK2,sK4,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition]) ).
tff(f177,plain,
( ~ spl6_11
| ~ spl6_9 ),
inference(avatar_split_clause,[],[f164,f160,f174]) ).
tff(f178,plain,
( ~ $less(sK4,$sum(c,sK5(sK2,sK4,sK3)))
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f70,f88]) ).
tff(f180,definition,
( spl6_12
<=> $less(sK4,$sum(c,sK5(sK2,sK4,sK3))) ),
introduced(definition,[new_symbols(definition,[spl6_12])],[avatar_definition]) ).
tff(f183,plain,
( ~ spl6_12
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f178,f86,f180]) ).
tff(f184,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int,X4: $int] :
( ~ ub(X0,X1,max(X2,X3))
| ~ model_max(X2,X3,X4)
| model_ub(X0,X1,X4) ),
inference(resolution,[],[f69,f68]) ).
tff(f213,plain,
( model_max(sK2,sK3,sK4)
| ~ spl6_2 ),
inference(unit_resulting_resolution,[],[f56,f80]) ).
tff(f217,definition,
( spl6_17
<=> model_max(sK2,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_17])],[avatar_definition]) ).
tff(f219,plain,
( model_max(sK2,sK3,sK4)
| ~ spl6_17 ),
inference(avatar_component_clause,[],[f217]) ).
tff(f220,plain,
( spl6_17
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f213,f78,f217]) ).
tff(f367,plain,
( ~ $less(sK4,$sum(c,max(sK2,sK3)))
| ~ spl6_17 ),
inference(unit_resulting_resolution,[],[f68,f219]) ).
tff(f371,definition,
( spl6_35
<=> $less(sK4,$sum(c,max(sK2,sK3))) ),
introduced(definition,[new_symbols(definition,[spl6_35])],[avatar_definition]) ).
tff(f373,plain,
( ~ $less(sK4,$sum(c,max(sK2,sK3)))
| spl6_35 ),
inference(avatar_component_clause,[],[f371]) ).
tff(f374,plain,
( ~ spl6_35
| ~ spl6_17 ),
inference(avatar_split_clause,[],[f367,f217,f371]) ).
tff(f395,plain,
( ~ ub(sK2,sK3,max(sK2,sK3))
| spl6_3
| spl6_35 ),
inference(unit_resulting_resolution,[],[f69,f87,f373]) ).
tff(f401,plain,
( model_max(sK2,sK3,sK4)
| spl6_35 ),
inference(resolution,[],[f373,f67]) ).
tff(f404,plain,
( $less(sK2,sK3)
| ~ $less(sK4,$sum(c,sK2))
| spl6_35 ),
inference(superposition,[],[f373,f72]) ).
tff(f416,definition,
( spl6_40
<=> $less(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_40])],[avatar_definition]) ).
tff(f417,plain,
( ~ $less(sK3,sK2)
| spl6_40 ),
inference(avatar_component_clause,[],[f416]) ).
tff(f421,definition,
( spl6_41
<=> ub(sK2,sK3,max(sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_41])],[avatar_definition]) ).
tff(f422,plain,
( ub(sK2,sK3,max(sK2,sK3))
| ~ spl6_41 ),
inference(avatar_component_clause,[],[f421]) ).
tff(f423,plain,
( ~ ub(sK2,sK3,max(sK2,sK3))
| spl6_41 ),
inference(avatar_component_clause,[],[f421]) ).
tff(f424,plain,
( ~ spl6_41
| spl6_3
| spl6_35 ),
inference(avatar_split_clause,[],[f395,f371,f86,f421]) ).
tff(f426,definition,
( spl6_42
<=> $less(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_42])],[avatar_definition]) ).
tff(f427,plain,
( ~ $less(sK2,sK3)
| spl6_42 ),
inference(avatar_component_clause,[],[f426]) ).
tff(f430,definition,
( spl6_43
<=> $less(sK4,$sum(c,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_43])],[avatar_definition]) ).
tff(f432,plain,
( ~ $less(sK4,$sum(c,sK2))
| spl6_43 ),
inference(avatar_component_clause,[],[f430]) ).
tff(f433,plain,
( spl6_42
| ~ spl6_43
| spl6_35 ),
inference(avatar_split_clause,[],[f404,f371,f430,f426]) ).
tff(f487,plain,
( ( max(sK2,sK3) = sK3 )
| spl6_40 ),
inference(unit_resulting_resolution,[],[f64,f417]) ).
tff(f507,definition,
( spl6_53
<=> ( max(sK2,sK3) = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl6_53])],[avatar_definition]) ).
tff(f510,plain,
( spl6_53
| spl6_40 ),
inference(avatar_split_clause,[],[f487,f416,f507]) ).
tff(f613,plain,
( ~ ub(sK2,sK3,sK2)
| spl6_3
| spl6_43 ),
inference(unit_resulting_resolution,[],[f69,f87,f432]) ).
tff(f628,definition,
( spl6_62
<=> ub(sK2,sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_62])],[avatar_definition]) ).
tff(f630,plain,
( ~ ub(sK2,sK3,sK2)
| spl6_62 ),
inference(avatar_component_clause,[],[f628]) ).
tff(f631,plain,
( ~ spl6_62
| spl6_3
| spl6_43 ),
inference(avatar_split_clause,[],[f613,f430,f86,f628]) ).
tff(f694,plain,
( $less(max(sK2,sK3),sK2)
| $less(max(sK2,sK3),sK3)
| spl6_41 ),
inference(resolution,[],[f423,f61]) ).
tff(f698,definition,
( spl6_73
<=> $less(max(sK2,sK3),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_73])],[avatar_definition]) ).
tff(f702,definition,
( spl6_74
<=> $less(max(sK2,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_74])],[avatar_definition]) ).
tff(f705,plain,
( spl6_73
| spl6_74
| spl6_41 ),
inference(avatar_split_clause,[],[f694,f421,f702,f698]) ).
tff(f706,plain,
( $less(sK2,sK3)
| $less(sK2,sK2)
| spl6_62 ),
inference(resolution,[],[f630,f61]) ).
tff(f708,definition,
( spl6_75
<=> $less(sK2,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_75])],[avatar_definition]) ).
tff(f711,plain,
( spl6_42
| spl6_75
| spl6_62 ),
inference(avatar_split_clause,[],[f706,f628,f708,f426]) ).
tff(f713,plain,
( model_ub(sK2,sK3,sK1(sK3,sK4,sK2))
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f59,f75,f88]) ).
tff(f714,plain,
( $less(sK1(sK3,sK4,sK2),sK4)
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f60,f75,f88]) ).
tff(f720,definition,
( spl6_76
<=> $less(sK1(sK3,sK4,sK2),sK4) ),
introduced(definition,[new_symbols(definition,[spl6_76])],[avatar_definition]) ).
tff(f722,plain,
( $less(sK1(sK3,sK4,sK2),sK4)
| ~ spl6_76 ),
inference(avatar_component_clause,[],[f720]) ).
tff(f723,plain,
( spl6_76
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f714,f86,f74,f720]) ).
tff(f725,definition,
( spl6_77
<=> model_ub(sK2,sK3,sK1(sK3,sK4,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_77])],[avatar_definition]) ).
tff(f727,plain,
( model_ub(sK2,sK3,sK1(sK3,sK4,sK2))
| ~ spl6_77 ),
inference(avatar_component_clause,[],[f725]) ).
tff(f728,plain,
( spl6_77
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f713,f86,f74,f725]) ).
tff(f733,plain,
( ~ model_max(sK2,sK3,sK1(sK3,sK4,sK2))
| ~ spl6_2
| ~ spl6_76 ),
inference(unit_resulting_resolution,[],[f55,f80,f722]) ).
tff(f735,definition,
( spl6_78
<=> model_max(sK2,sK3,sK1(sK3,sK4,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_78])],[avatar_definition]) ).
tff(f737,plain,
( ~ model_max(sK2,sK3,sK1(sK3,sK4,sK2))
| spl6_78 ),
inference(avatar_component_clause,[],[f735]) ).
tff(f738,plain,
( ~ spl6_78
| ~ spl6_2
| ~ spl6_76 ),
inference(avatar_split_clause,[],[f733,f720,f78,f735]) ).
tff(f758,plain,
( ~ $less(sK1(sK3,sK4,sK2),$sum(c,sK5(sK2,sK1(sK3,sK4,sK2),sK3)))
| ~ spl6_77 ),
inference(unit_resulting_resolution,[],[f70,f727]) ).
tff(f760,plain,
( ~ $less(sK5(sK2,sK1(sK3,sK4,sK2),sK3),sK3)
| ~ spl6_77 ),
inference(unit_resulting_resolution,[],[f157,f727]) ).
tff(f761,plain,
( ~ $less(sK5(sK2,sK1(sK3,sK4,sK2),sK3),sK2)
| ~ spl6_77 ),
inference(unit_resulting_resolution,[],[f158,f727]) ).
tff(f763,definition,
( spl6_80
<=> $less(sK1(sK3,sK4,sK2),$sum(c,sK5(sK2,sK1(sK3,sK4,sK2),sK3))) ),
introduced(definition,[new_symbols(definition,[spl6_80])],[avatar_definition]) ).
tff(f766,plain,
( ~ spl6_80
| ~ spl6_77 ),
inference(avatar_split_clause,[],[f758,f725,f763]) ).
tff(f768,definition,
( spl6_81
<=> $less(sK5(sK2,sK1(sK3,sK4,sK2),sK3),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_81])],[avatar_definition]) ).
tff(f771,plain,
( ~ spl6_81
| ~ spl6_77 ),
inference(avatar_split_clause,[],[f761,f725,f768]) ).
tff(f778,definition,
( spl6_83
<=> $less(sK5(sK2,sK1(sK3,sK4,sK2),sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_83])],[avatar_definition]) ).
tff(f781,plain,
( ~ spl6_83
| ~ spl6_77 ),
inference(avatar_split_clause,[],[f760,f725,f778]) ).
tff(f787,plain,
( model_max(sK2,sK3,sK0(sK4,sK3,sK2))
| spl6_2
| ~ spl6_17 ),
inference(unit_resulting_resolution,[],[f54,f219,f79]) ).
tff(f788,plain,
( $less(sK0(sK4,sK3,sK2),sK4)
| spl6_2
| ~ spl6_17 ),
inference(unit_resulting_resolution,[],[f53,f219,f79]) ).
tff(f790,definition,
( spl6_84
<=> $less(sK0(sK4,sK3,sK2),sK4) ),
introduced(definition,[new_symbols(definition,[spl6_84])],[avatar_definition]) ).
tff(f792,plain,
( $less(sK0(sK4,sK3,sK2),sK4)
| ~ spl6_84 ),
inference(avatar_component_clause,[],[f790]) ).
tff(f793,plain,
( spl6_84
| spl6_2
| ~ spl6_17 ),
inference(avatar_split_clause,[],[f788,f217,f78,f790]) ).
tff(f795,definition,
( spl6_85
<=> model_max(sK2,sK3,sK0(sK4,sK3,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_85])],[avatar_definition]) ).
tff(f797,plain,
( model_max(sK2,sK3,sK0(sK4,sK3,sK2))
| ~ spl6_85 ),
inference(avatar_component_clause,[],[f795]) ).
tff(f798,plain,
( spl6_85
| spl6_2
| ~ spl6_17 ),
inference(avatar_split_clause,[],[f787,f217,f78,f795]) ).
tff(f809,plain,
( ~ model_ub(sK2,sK3,sK0(sK4,sK3,sK2))
| ~ spl6_1
| ~ spl6_84 ),
inference(unit_resulting_resolution,[],[f57,f76,f792]) ).
tff(f811,definition,
( spl6_86
<=> model_ub(sK2,sK3,sK0(sK4,sK3,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_86])],[avatar_definition]) ).
tff(f814,plain,
( ~ spl6_86
| ~ spl6_1
| ~ spl6_84 ),
inference(avatar_split_clause,[],[f809,f790,f74,f811]) ).
tff(f824,plain,
( ( max(sK2,sK3) = sK2 )
| spl6_42 ),
inference(unit_resulting_resolution,[],[f72,f427]) ).
tff(f840,definition,
( spl6_90
<=> ( max(sK2,sK3) = sK2 ) ),
introduced(definition,[new_symbols(definition,[spl6_90])],[avatar_definition]) ).
tff(f843,plain,
( spl6_90
| spl6_42 ),
inference(avatar_split_clause,[],[f824,f426,f840]) ).
tff(f887,plain,
( spl6_17
| spl6_35 ),
inference(avatar_split_clause,[],[f401,f371,f217]) ).
tff(f1062,plain,
( $less(sK1(sK3,sK4,sK2),$sum(c,max(sK2,sK3)))
| spl6_78 ),
inference(unit_resulting_resolution,[],[f67,f737]) ).
tff(f1071,definition,
( spl6_114
<=> $less(sK1(sK3,sK4,sK2),$sum(c,max(sK2,sK3))) ),
introduced(definition,[new_symbols(definition,[spl6_114])],[avatar_definition]) ).
tff(f1074,plain,
( spl6_114
| spl6_78 ),
inference(avatar_split_clause,[],[f1062,f735,f1071]) ).
tff(f1117,plain,
( model_ub(sK2,sK3,sK0(sK4,sK3,sK2))
| ~ spl6_41
| ~ spl6_85 ),
inference(unit_resulting_resolution,[],[f184,f422,f797]) ).
tff(f1118,plain,
( spl6_86
| ~ spl6_41
| ~ spl6_85 ),
inference(avatar_split_clause,[],[f1117,f795,f421,f811]) ).
tff(f1119,plain,
$false,
inference(avatar_smt_refutation,[],[f1118,f1074,f887,f843,f814,f798,f793,f781,f771,f766,f738,f728,f723,f711,f705,f631,f510,f433,f424,f374,f220,f183,f177,f172,f163,f89,f82,f81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM861_1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n017.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 21:32:24 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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.10/1.41 % (2955584)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.10/1.41 % (2955594)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1033539468:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.10/1.41 % (2955591)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2796516717:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.10/1.41 % (2955593)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3928798274:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.10/1.41 % (2955594)Instruction limit reached!
% 3.10/1.41 % (2955594)------------------------------
% 3.10/1.41 % (2955594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.41 % (2955594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.41 % (2955594)CaDiCaL version: 2.1.3
% 3.10/1.41 % (2955594)Termination reason: Instruction limit
% 3.10/1.41 % (2955594)Termination phase: Saturation
% 3.10/1.41 % (2955594)Time elapsed: 0.036 s
% 3.10/1.41 % (2955594)Peak memory usage: 115 MB
% 3.10/1.41 % (2955594)Instructions burned: 49 (million)
% 3.10/1.41 % (2955590)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=571137408:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.10/1.41 % (2955589)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2106720129:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.10/1.41 % (2955593)Instruction limit reached!
% 3.10/1.41 % (2955593)------------------------------
% 3.10/1.41 % (2955593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.41 % (2955593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.41 % (2955593)CaDiCaL version: 2.1.3
% 3.10/1.41 % (2955593)Termination reason: Instruction limit
% 3.10/1.41 % (2955593)Termination phase: Saturation
% 3.10/1.41 % (2955593)Time elapsed: 0.004 s
% 3.10/1.41 % (2955593)Peak memory usage: 89 MB
% 3.10/1.41 % (2955593)Instructions burned: 5 (million)
% 3.10/1.41 % (2955592)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1555857052:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.10/1.41 % (2955592)Instruction limit reached!
% 3.10/1.41 % (2955592)------------------------------
% 3.10/1.41 % (2955592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.41 % (2955592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.41 % (2955592)CaDiCaL version: 2.1.3
% 3.10/1.41 % (2955592)Termination reason: Instruction limit
% 3.10/1.41 % (2955592)Termination phase: Saturation
% 3.10/1.41 % (2955592)Time elapsed: 0.005 s
% 3.10/1.41 % (2955592)Peak memory usage: 88 MB
% 3.10/1.41 % (2955592)Instructions burned: 7 (million)
% 3.10/1.41 % (2955595)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3718992382:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.10/1.41 % (2955589)Instruction limit reached!
% 3.10/1.41 % (2955589)------------------------------
% 3.10/1.41 % (2955589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.41 % (2955589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.41 % (2955589)CaDiCaL version: 2.1.3
% 3.10/1.41 % (2955589)Termination reason: Instruction limit
% 3.10/1.41 % (2955589)Termination phase: Saturation
% 3.10/1.41 % (2955589)Time elapsed: 0.030 s
% 3.10/1.41 % (2955589)Peak memory usage: 115 MB
% 3.10/1.41 % (2955589)Instructions burned: 12 (million)
% 3.10/1.41 % (2955595)Instruction limit reached!
% 3.10/1.41 % (2955595)------------------------------
% 3.10/1.41 % (2955595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.41 % (2955595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.41 % (2955595)CaDiCaL version: 2.1.3
% 3.10/1.41 % (2955595)Termination reason: Instruction limit
% 3.10/1.41 % (2955595)Termination phase: Saturation
% 3.10/1.41 % (2955595)Time elapsed: 0.045 s
% 3.10/1.41 % (2955595)Peak memory usage: 115 MB
% 3.10/1.41 % (2955595)Instructions burned: 33 (million)
% 3.10/1.41 % (2955602)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=758982546:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.10/1.41 % (2955603)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=3847682450:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.16/1.55 % (2955604)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=201064409:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.16/1.55 % (2955604)Instruction limit reached!
% 4.16/1.55 % (2955604)------------------------------
% 4.16/1.55 % (2955604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955604)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955604)Termination reason: Instruction limit
% 4.16/1.55 % (2955604)Termination phase: Saturation
% 4.16/1.55 % (2955604)Time elapsed: 0.005 s
% 4.16/1.55 % (2955604)Peak memory usage: 90 MB
% 4.16/1.55 % (2955604)Instructions burned: 16 (million)
% 4.16/1.55 % (2955591)Instruction limit reached!
% 4.16/1.55 % (2955591)------------------------------
% 4.16/1.55 % (2955591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955591)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955591)Termination reason: Instruction limit
% 4.16/1.55 % (2955591)Termination phase: Saturation
% 4.16/1.55 % (2955591)Time elapsed: 0.155 s
% 4.16/1.55 % (2955591)Peak memory usage: 118 MB
% 4.16/1.55 % (2955591)Instructions burned: 201 (million)
% 4.16/1.55 % (2955602)Instruction limit reached!
% 4.16/1.55 % (2955602)------------------------------
% 4.16/1.55 % (2955602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955602)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955602)Termination reason: Instruction limit
% 4.16/1.55 % (2955602)Termination phase: Saturation
% 4.16/1.55 % (2955602)Time elapsed: 0.011 s
% 4.16/1.55 % (2955602)Peak memory usage: 88 MB
% 4.16/1.55 % (2955602)Instructions burned: 14 (million)
% 4.16/1.55 % (2955603)Instruction limit reached!
% 4.16/1.55 % (2955603)------------------------------
% 4.16/1.55 % (2955603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955603)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955603)Termination reason: Instruction limit
% 4.16/1.55 % (2955603)Termination phase: Saturation
% 4.16/1.55 % (2955603)Time elapsed: 0.023 s
% 4.16/1.55 % (2955603)Peak memory usage: 88 MB
% 4.16/1.55 % (2955603)Instructions burned: 29 (million)
% 4.16/1.55 % (2955606)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2280305897:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 4.16/1.55 % (2955607)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=2960874309:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.16/1.55 % (2955606)Instruction limit reached!
% 4.16/1.55 % (2955606)------------------------------
% 4.16/1.55 % (2955606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955606)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955606)Termination reason: Instruction limit
% 4.16/1.55 % (2955606)Termination phase: Saturation
% 4.16/1.55 % (2955606)Time elapsed: 0.018 s
% 4.16/1.55 % (2955606)Peak memory usage: 89 MB
% 4.16/1.55 % (2955606)Instructions burned: 24 (million)
% 4.16/1.55 % (2955607)Refutation not found, incomplete strategy
% 4.16/1.55 % (2955607)------------------------------
% 4.16/1.55 % (2955607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.55 % (2955607)CaDiCaL version: 2.1.3
% 4.16/1.55 % (2955607)Termination reason: Refutation not found, incomplete strategy
% 4.16/1.55 % (2955607)Time elapsed: 0.002 s
% 4.16/1.55 % (2955607)Peak memory usage: 89 MB
% 4.16/1.55 % (2955607)Instructions burned: 2 (million)
% 4.16/1.55 % (2955590)Instruction limit reached!
% 4.16/1.55 % (2955590)------------------------------
% 4.16/1.55 % (2955590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.55 % (2955590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955590)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955590)Termination reason: Instruction limit
% 5.35/1.72 % (2955590)Termination phase: Saturation
% 5.35/1.72 % (2955590)Time elapsed: 0.218 s
% 5.35/1.72 % (2955590)Peak memory usage: 117 MB
% 5.35/1.72 % (2955590)Instructions burned: 308 (million)
% 5.35/1.72 % (2955611)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=618865083:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.35/1.72 % (2955611)Instruction limit reached!
% 5.35/1.72 % (2955611)------------------------------
% 5.35/1.72 % (2955611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.35/1.72 % (2955611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955611)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955611)Termination reason: Instruction limit
% 5.35/1.72 % (2955611)Termination phase: Saturation
% 5.35/1.72 % (2955611)Time elapsed: 0.033 s
% 5.35/1.72 % (2955611)Peak memory usage: 89 MB
% 5.35/1.72 % (2955611)Instructions burned: 86 (million)
% 5.35/1.72 % (2955612)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2069093042:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.35/1.72 % (2955613)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2881726274:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 5.35/1.72 % (2955612)Instruction limit reached!
% 5.35/1.72 % (2955612)------------------------------
% 5.35/1.72 % (2955612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.35/1.72 % (2955612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955612)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955612)Termination reason: Instruction limit
% 5.35/1.72 % (2955612)Termination phase: Saturation
% 5.35/1.72 % (2955612)Time elapsed: 0.003 s
% 5.35/1.72 % (2955612)Peak memory usage: 88 MB
% 5.35/1.72 % (2955612)Instructions burned: 3 (million)
% 5.35/1.72 % (2955615)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=316095990:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.35/1.72 % (2955615)Instruction limit reached!
% 5.35/1.72 % (2955615)------------------------------
% 5.35/1.72 % (2955615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.35/1.72 % (2955615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955615)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955615)Termination reason: Instruction limit
% 5.35/1.72 % (2955615)Termination phase: Saturation
% 5.35/1.72 % (2955615)Time elapsed: 0.004 s
% 5.35/1.72 % (2955615)Peak memory usage: 88 MB
% 5.35/1.72 % (2955615)Instructions burned: 4 (million)
% 5.35/1.72 % (2955617)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1879530007:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.35/1.72 % (2955618)lrs+10_1_thi=all:si=on:fd=off:random_seed=2519340696:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.35/1.72 % (2955613)Refutation not found, incomplete strategy
% 5.35/1.72 % (2955613)------------------------------
% 5.35/1.72 % (2955613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.35/1.72 % (2955613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955613)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955613)Termination reason: Refutation not found, incomplete strategy
% 5.35/1.72 % (2955613)Time elapsed: 0.071 s
% 5.35/1.72 % (2955613)Peak memory usage: 89 MB
% 5.35/1.72 % (2955613)Instructions burned: 114 (million)
% 5.35/1.72 % (2955620)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=3470621516:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.35/1.72 % (2955620)Instruction limit reached!
% 5.35/1.72 % (2955620)------------------------------
% 5.35/1.72 % (2955620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.35/1.72 % (2955620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.35/1.72 % (2955620)CaDiCaL version: 2.1.3
% 5.35/1.72 % (2955620)Termination reason: Instruction limit
% 5.35/1.72 % (2955620)Termination phase: Saturation
% 5.35/1.72 % (2955620)Time elapsed: 0.004 s
% 5.35/1.72 % (2955620)Peak memory usage: 88 MB
% 5.35/1.72 % (2955620)Instructions burned: 10 (million)
% 5.35/1.72 % (2955623)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1364664929:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 6.67/1.94 % (2955623)Instruction limit reached!
% 6.67/1.94 % (2955623)------------------------------
% 6.67/1.94 % (2955623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955623)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955623)Termination reason: Instruction limit
% 6.67/1.94 % (2955623)Termination phase: Saturation
% 6.67/1.94 % (2955623)Time elapsed: 0.002 s
% 6.67/1.94 % (2955623)Peak memory usage: 88 MB
% 6.67/1.94 % (2955623)Instructions burned: 2 (million)
% 6.67/1.94 % (2955617)Instruction limit reached!
% 6.67/1.94 % (2955617)------------------------------
% 6.67/1.94 % (2955617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955617)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955617)Termination reason: Instruction limit
% 6.67/1.94 % (2955617)Termination phase: Saturation
% 6.67/1.94 % (2955617)Time elapsed: 0.093 s
% 6.67/1.94 % (2955617)Peak memory usage: 133 MB
% 6.67/1.94 % (2955617)Instructions burned: 66 (million)
% 6.67/1.94 % (2955618)Instruction limit reached!
% 6.67/1.94 % (2955618)------------------------------
% 6.67/1.94 % (2955618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955618)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955618)Termination reason: Instruction limit
% 6.67/1.94 % (2955618)Termination phase: Saturation
% 6.67/1.94 % (2955618)Time elapsed: 0.065 s
% 6.67/1.94 % (2955618)Peak memory usage: 116 MB
% 6.67/1.94 % (2955618)Instructions burned: 54 (million)
% 6.67/1.94 % (2955607)------------------------------
% 6.67/1.94 % (2955607)------------------------------
% 6.67/1.94 % (2955625)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2608315254:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.67/1.94 % (2955629)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1288997526:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 6.67/1.94 % (2955625)Instruction limit reached!
% 6.67/1.94 % (2955625)------------------------------
% 6.67/1.94 % (2955625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955625)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955625)Termination reason: Instruction limit
% 6.67/1.94 % (2955625)Termination phase: Saturation
% 6.67/1.94 % (2955625)Time elapsed: 0.003 s
% 6.67/1.94 % (2955625)Peak memory usage: 89 MB
% 6.67/1.94 % (2955625)Instructions burned: 3 (million)
% 6.67/1.94 % (2955629)Instruction limit reached!
% 6.67/1.94 % (2955629)------------------------------
% 6.67/1.94 % (2955629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955629)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955629)Termination reason: Instruction limit
% 6.67/1.94 % (2955629)Termination phase: Saturation
% 6.67/1.94 % (2955629)Time elapsed: 0.064 s
% 6.67/1.94 % (2955629)Peak memory usage: 117 MB
% 6.67/1.94 % (2955629)Instructions burned: 129 (million)
% 6.67/1.94 % (2955632)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2956033627:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.67/1.94 % (2955631)dis+10_1_si=on:random_seed=2979379038:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.67/1.94 % (2955633)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1181800645: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)
% 6.67/1.94 % (2955632)Refutation not found, incomplete strategy
% 6.67/1.94 % (2955632)------------------------------
% 6.67/1.94 % (2955632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.67/1.94 % (2955632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.94 % (2955632)CaDiCaL version: 2.1.3
% 6.67/1.94 % (2955632)Termination reason: Refutation not found, incomplete strategy
% 6.67/1.94 % (2955632)Time elapsed: 0.002 s
% 6.67/1.94 % (2955632)Peak memory usage: 88 MB
% 8.95/2.17 % (2955632)Instructions burned: 1 (million)
% 8.95/2.17 % (2955631)Instruction limit reached!
% 8.95/2.17 % (2955631)------------------------------
% 8.95/2.17 % (2955631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955631)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955631)Termination reason: Instruction limit
% 8.95/2.17 % (2955631)Termination phase: Saturation
% 8.95/2.17 % (2955631)Time elapsed: 0.008 s
% 8.95/2.17 % (2955631)Peak memory usage: 88 MB
% 8.95/2.17 % (2955631)Instructions burned: 10 (million)
% 8.95/2.17 % (2955633)Instruction limit reached!
% 8.95/2.17 % (2955633)------------------------------
% 8.95/2.17 % (2955633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955633)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955633)Termination reason: Instruction limit
% 8.95/2.17 % (2955633)Termination phase: Saturation
% 8.95/2.17 % (2955633)Time elapsed: 0.030 s
% 8.95/2.17 % (2955633)Peak memory usage: 89 MB
% 8.95/2.17 % (2955633)Instructions burned: 35 (million)
% 8.95/2.17 % (2955635)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2845731185:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.95/2.17 % (2955635)Instruction limit reached!
% 8.95/2.17 % (2955635)------------------------------
% 8.95/2.17 % (2955635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955635)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955635)Termination reason: Instruction limit
% 8.95/2.17 % (2955635)Termination phase: Saturation
% 8.95/2.17 % (2955635)Time elapsed: 0.003 s
% 8.95/2.17 % (2955635)Peak memory usage: 89 MB
% 8.95/2.17 % (2955635)Instructions burned: 3 (million)
% 8.95/2.17 % (2955637)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3845467162:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 8.95/2.17 % (2955613)------------------------------
% 8.95/2.17 % (2955613)------------------------------
% 8.95/2.17 % (2955637)Instruction limit reached!
% 8.95/2.17 % (2955637)------------------------------
% 8.95/2.17 % (2955637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955637)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955637)Termination reason: Instruction limit
% 8.95/2.17 % (2955637)Termination phase: Saturation
% 8.95/2.17 % (2955637)Time elapsed: 0.008 s
% 8.95/2.17 % (2955637)Peak memory usage: 88 MB
% 8.95/2.17 % (2955637)Instructions burned: 8 (million)
% 8.95/2.17 % (2955638)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=535969586:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.95/2.17 % (2955642)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2861909118:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 8.95/2.17 % (2955643)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=566511156:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 8.95/2.17 % (2955642)Instruction limit reached!
% 8.95/2.17 % (2955642)------------------------------
% 8.95/2.17 % (2955642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955642)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955642)Termination reason: Instruction limit
% 8.95/2.17 % (2955642)Termination phase: Saturation
% 8.95/2.17 % (2955642)Time elapsed: 0.033 s
% 8.95/2.17 % (2955642)Peak memory usage: 116 MB
% 8.95/2.17 % (2955642)Instructions burned: 14 (million)
% 8.95/2.17 % (2955638)Instruction limit reached!
% 8.95/2.17 % (2955638)------------------------------
% 8.95/2.17 % (2955638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.95/2.17 % (2955638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.95/2.17 % (2955638)CaDiCaL version: 2.1.3
% 8.95/2.17 % (2955638)Termination reason: Instruction limit
% 8.95/2.17 % (2955638)Termination phase: Saturation
% 8.95/2.17 % (2955638)Time elapsed: 0.112 s
% 8.95/2.17 % (2955638)Peak memory usage: 91 MB
% 10.30/2.42 % (2955638)Instructions burned: 374 (million)
% 10.30/2.42 % (2955646)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2128226594:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.30/2.42 % (2955647)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3779772016:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.30/2.42 % (2955646)Instruction limit reached!
% 10.30/2.42 % (2955646)------------------------------
% 10.30/2.42 % (2955646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.42 % (2955646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.42 % (2955646)CaDiCaL version: 2.1.3
% 10.30/2.42 % (2955646)Termination reason: Instruction limit
% 10.30/2.42 % (2955646)Termination phase: Saturation
% 10.30/2.42 % (2955646)Time elapsed: 0.008 s
% 10.30/2.42 % (2955646)Peak memory usage: 88 MB
% 10.30/2.42 % (2955646)Instructions burned: 11 (million)
% 10.30/2.42 % (2955649)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=1435726325:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.30/2.42 % (2955643)Refutation not found, incomplete strategy
% 10.30/2.42 % (2955643)------------------------------
% 10.30/2.42 % (2955643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.42 % (2955643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.42 % (2955643)CaDiCaL version: 2.1.3
% 10.30/2.42 % (2955643)Termination reason: Refutation not found, incomplete strategy
% 10.30/2.42 % (2955643)Time elapsed: 0.072 s
% 10.30/2.42 % (2955643)Peak memory usage: 116 MB
% 10.30/2.42 % (2955643)Instructions burned: 64 (million)
% 10.30/2.42 % (2955649)Instruction limit reached!
% 10.30/2.42 % (2955649)------------------------------
% 10.30/2.42 % (2955649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.42 % (2955649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.42 % (2955649)CaDiCaL version: 2.1.3
% 10.30/2.42 % (2955649)Termination reason: Instruction limit
% 10.30/2.42 % (2955649)Termination phase: Saturation
% 10.30/2.42 % (2955649)Time elapsed: 0.054 s
% 10.30/2.42 % (2955649)Peak memory usage: 90 MB
% 10.30/2.42 % (2955649)Instructions burned: 76 (million)
% 10.30/2.42 % (2955632)------------------------------
% 10.30/2.42 % (2955632)------------------------------
% 10.30/2.42 % (2955654)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=2091274582:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 10.30/2.42 % (2955647)Instruction limit reached!
% 10.30/2.42 % (2955647)------------------------------
% 10.30/2.42 % (2955647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.42 % (2955647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.42 % (2955647)CaDiCaL version: 2.1.3
% 10.30/2.42 % (2955647)Termination reason: Instruction limit
% 10.30/2.42 % (2955647)Termination phase: Saturation
% 10.30/2.42 % (2955647)Time elapsed: 0.098 s
% 10.30/2.42 % (2955647)Peak memory usage: 133 MB
% 10.30/2.42 % (2955647)Instructions burned: 71 (million)
% 10.30/2.42 % (2955655)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=906341240:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.30/2.42 % (2955657)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1315918034:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.30/2.42 % (2955658)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1344092528:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 10.30/2.42 % (2955654)Instruction limit reached!
% 10.30/2.42 % (2955654)------------------------------
% 10.30/2.42 % (2955654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.30/2.42 % (2955654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.30/2.42 % (2955654)CaDiCaL version: 2.1.3
% 10.30/2.42 % (2955654)Termination reason: Instruction limit
% 10.30/2.42 % (2955654)Termination phase: Saturation
% 10.30/2.42 % (2955654)Time elapsed: 0.114 s
% 10.30/2.42 % (2955654)Peak memory usage: 90 MB
% 10.30/2.42 % (2955654)Instructions burned: 296 (million)
% 10.30/2.42 % (2955659)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3945640804:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.80/2.67 % (2955655)Instruction limit reached!
% 10.80/2.67 % (2955655)------------------------------
% 10.80/2.67 % (2955655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955655)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955655)Termination reason: Instruction limit
% 10.80/2.67 % (2955655)Termination phase: Saturation
% 10.80/2.67 % (2955655)Time elapsed: 0.107 s
% 10.80/2.67 % (2955655)Peak memory usage: 117 MB
% 10.80/2.67 % (2955655)Instructions burned: 130 (million)
% 10.80/2.67 % (2955661)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2133772413:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 10.80/2.67 % (2955658)Instruction limit reached!
% 10.80/2.67 % (2955658)------------------------------
% 10.80/2.67 % (2955658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955658)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955658)Termination reason: Instruction limit
% 10.80/2.67 % (2955658)Termination phase: Saturation
% 10.80/2.67 % (2955658)Time elapsed: 0.069 s
% 10.80/2.67 % (2955658)Peak memory usage: 133 MB
% 10.80/2.67 % (2955658)Instructions burned: 42 (million)
% 10.80/2.67 % (2955657)Instruction limit reached!
% 10.80/2.67 % (2955657)------------------------------
% 10.80/2.67 % (2955657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955657)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955657)Termination reason: Instruction limit
% 10.80/2.67 % (2955657)Termination phase: Saturation
% 10.80/2.67 % (2955657)Time elapsed: 0.138 s
% 10.80/2.67 % (2955657)Peak memory usage: 133 MB
% 10.80/2.67 % (2955657)Instructions burned: 134 (million)
% 10.80/2.67 % (2955643)------------------------------
% 10.80/2.67 % (2955643)------------------------------
% 10.80/2.67 % (2955665)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2185282672:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 10.80/2.67 % (2955665)Instruction limit reached!
% 10.80/2.67 % (2955665)------------------------------
% 10.80/2.67 % (2955665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955665)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955665)Termination reason: Instruction limit
% 10.80/2.67 % (2955665)Termination phase: Saturation
% 10.80/2.67 % (2955665)Time elapsed: 0.055 s
% 10.80/2.67 % (2955665)Peak memory usage: 116 MB
% 10.80/2.67 % (2955665)Instructions burned: 133 (million)
% 10.80/2.67 % (2955667)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=3282211848:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 10.80/2.67 % (2955669)dis+10_1_si=on:random_seed=3756580037:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 10.80/2.67 % (2955670)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2195694485:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 10.80/2.67 % (2955672)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4238259889:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 10.80/2.67 % (2955659)Instruction limit reached!
% 10.80/2.67 % (2955659)------------------------------
% 10.80/2.67 % (2955659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955659)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955659)Termination reason: Instruction limit
% 10.80/2.67 % (2955659)Termination phase: Saturation
% 10.80/2.67 % (2955659)Time elapsed: 0.205 s
% 10.80/2.67 % (2955659)Peak memory usage: 92 MB
% 10.80/2.67 % (2955659)Instructions burned: 307 (million)
% 10.80/2.67 % (2955673)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1685754985:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 10.80/2.67 % (2955661)First to succeed.
% 10.80/2.67 % (2955661)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2955584"
% 10.80/2.67 % (2955673)Instruction limit reached!
% 10.80/2.67 % (2955673)------------------------------
% 10.80/2.67 % (2955673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955673)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955673)Termination reason: Instruction limit
% 10.80/2.67 % (2955673)Termination phase: Saturation
% 10.80/2.67 % (2955673)Time elapsed: 0.033 s
% 10.80/2.67 % (2955673)Peak memory usage: 115 MB
% 10.80/2.67 % (2955673)Instructions burned: 67 (million)
% 10.80/2.67 % (2955672)Instruction limit reached!
% 10.80/2.67 % (2955672)------------------------------
% 10.80/2.67 % (2955672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955672)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955672)Termination reason: Instruction limit
% 10.80/2.67 % (2955672)Termination phase: Saturation
% 10.80/2.67 % (2955672)Time elapsed: 0.093 s
% 10.80/2.67 % (2955672)Peak memory usage: 90 MB
% 10.80/2.67 % (2955672)Instructions burned: 142 (million)
% 10.80/2.67 % (2955678)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1410222176:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 10.80/2.67 % (2955667)Instruction limit reached!
% 10.80/2.67 % (2955667)------------------------------
% 10.80/2.67 % (2955667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955667)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955667)Termination reason: Instruction limit
% 10.80/2.67 % (2955667)Termination phase: Saturation
% 10.80/2.67 % (2955667)Time elapsed: 0.195 s
% 10.80/2.67 % (2955667)Peak memory usage: 117 MB
% 10.80/2.67 % (2955667)Instructions burned: 259 (million)
% 10.80/2.67 % (2955670)Instruction limit reached!
% 10.80/2.67 % (2955670)------------------------------
% 10.80/2.67 % (2955670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955670)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955670)Termination reason: Instruction limit
% 10.80/2.67 % (2955670)Termination phase: Saturation
% 10.80/2.67 % (2955670)Time elapsed: 0.191 s
% 10.80/2.67 % (2955670)Peak memory usage: 90 MB
% 10.80/2.67 % (2955670)Instructions burned: 384 (million)
% 10.80/2.67 % (2955680)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=3511310186:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 10.80/2.67 % (2955678)Instruction limit reached!
% 10.80/2.67 % (2955678)------------------------------
% 10.80/2.67 % (2955678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955678)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955678)Termination reason: Instruction limit
% 10.80/2.67 % (2955678)Termination phase: Saturation
% 10.80/2.67 % (2955678)Time elapsed: 0.069 s
% 10.80/2.67 % (2955678)Peak memory usage: 89 MB
% 10.80/2.67 % (2955678)Instructions burned: 121 (million)
% 10.80/2.67 % (2955681)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=4192081203:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 10.80/2.67 % (2955681)Instruction limit reached!
% 10.80/2.67 % (2955681)------------------------------
% 10.80/2.67 % (2955681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955681)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955681)Termination reason: Instruction limit
% 10.80/2.67 % (2955681)Termination phase: Saturation
% 10.80/2.67 % (2955681)Time elapsed: 0.052 s
% 10.80/2.67 % (2955681)Peak memory usage: 116 MB
% 10.80/2.67 % (2955681)Instructions burned: 39 (million)
% 10.80/2.67 % (2955680)Refutation not found, SMT solver inside AVATAR returned Unknown
% 10.80/2.67 % (2955680)------------------------------
% 10.80/2.67 % (2955680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.67 % (2955680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.67 % (2955680)CaDiCaL version: 2.1.3
% 10.80/2.67 % (2955680)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 10.80/2.67 % (2955680)Time elapsed: 0.080 s
% 10.80/2.67 % (2955680)Peak memory usage: 117 MB
% 10.80/2.67 % (2955680)Instructions burned: 78 (million)
% 10.80/2.67 % (2955680)------------------------------
% 10.80/2.67 % (2955680)------------------------------
% 10.80/2.67 % (2955661)Refutation found. Thanks to Tanya!
% 10.80/2.67 % SZS status Theorem for theBenchmark
% 10.80/2.67 % SZS output start Proof for theBenchmark
% See solution above
% 11.71/2.77 % (2955661)------------------------------
% 11.71/2.77 % (2955661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.71/2.77 % (2955661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.71/2.77 % (2955661)CaDiCaL version: 2.1.3
% 11.71/2.77 % (2955661)Termination reason: Refutation
% 11.71/2.77 % (2955661)Time elapsed: 0.193 s
% 11.71/2.77 % (2955661)Peak memory usage: 135 MB
% 11.71/2.77 % (2955661)Instructions burned: 209 (million)
% 11.71/2.77 % (2955661)------------------------------
% 11.71/2.77 % (2955661)------------------------------
% 11.71/2.77 % (2955584)Success in time 1.804 s
% 11.71/2.77 % Vampire exiting
%------------------------------------------------------------------------------