%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM860_1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:18 PM UTC 2026
% Result : Theorem 12.85s 3.01s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 44
% Syntax : Number of formulae : 204 ( 1 unt; 0 typ; 35 def)
% Number of atoms : 554 ( 12 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 569 ( 219 ~; 233 |; 55 &)
% ( 56 <=>; 5 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 391 ( 159 atm; 0 fun; 0 num; 232 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 : 44 ( 40 usr; 36 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 232 ( 213 !; 19 ?; 232 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
summation: $int > $int ).
tff(func_def_1,type,
max: ( $int * $int ) > $int ).
tff(func_def_2,type,
sK0: $int ).
tff(func_def_3,type,
sK1: $int ).
tff(func_def_4,type,
sK2: $int ).
tff(func_def_5,type,
sK3: ( $int * $int * $int ) > $int ).
tff(func_def_6,type,
sK4: ( $int * $int * $int ) > $int ).
tff(func_def_7,type,
sK5: ( $int * $int * $int ) > $int ).
tff(func_def_9,type,
'$inst7': $int ).
tff(func_def_10,type,
'$inst8': $int ).
tff(func_def_14,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(f1,axiom,
! [X1: $int,X0: $int] :
( $lesseq(summation(X0),summation(X1))
<=> $lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',summation_monotone) ).
tff(f2,axiom,
! [X0: $int,X1: $int] :
( ~ $lesseq(X1,X0)
| ( max(X0,X1) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_1) ).
tff(f3,axiom,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X1 )
| ~ $lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_2) ).
tff(f4,axiom,
! [X2: $int,X1: $int,X0: $int] :
( ub(X0,X1,X2)
<=> ( $lesseq(X1,X2)
& $lesseq(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ub) ).
tff(f5,axiom,
! [X2: $int,X1: $int,X0: $int] :
( model_max(X0,X1,X2)
<=> $lesseq(summation(max(X0,X1)),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_max_3) ).
tff(f6,axiom,
! [X0: $int,X1: $int,X2: $int] :
( ? [X3: $int] :
( $lesseq(summation(X3),X2)
& ub(X0,X1,X3) )
<=> model_ub(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_ub_3) ).
tff(f7,axiom,
! [X0: $int,X1: $int,X2: $int] :
( minsol_model_max(X0,X1,X2)
<=> ( model_max(X0,X1,X2)
& ! [X3: $int] :
( model_max(X0,X1,X3)
=> $lesseq(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minsol_model_max) ).
tff(f8,axiom,
! [X2: $int,X0: $int,X1: $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/sandbox/benchmark/theBenchmark.p',minsol_model_ub) ).
tff(f9,conjecture,
! [X2: $int,X0: $int,X1: $int] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_ub_1) ).
tff(f10,negated_conjecture,
~ ! [X2: $int,X0: $int,X1: $int] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f9]) ).
tff(f11,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( max(X0,X1) = X0 ) ),
inference(theory_normalization,[],[f2]) ).
tff(f12,plain,
! [X2: $int,X1: $int,X0: $int] :
( ub(X0,X1,X2)
<=> ( ~ $less(X2,X1)
& ~ $less(X2,X0) ) ),
inference(theory_normalization,[],[f4]) ).
tff(f13,plain,
! [X2: $int,X0: $int,X1: $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(f14,plain,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X1 )
| $less(X1,X0) ),
inference(theory_normalization,[],[f3]) ).
tff(f15,plain,
! [X1: $int,X0: $int] :
( ~ $less(summation(X1),summation(X0))
<=> ~ $less(X1,X0) ),
inference(theory_normalization,[],[f1]) ).
tff(f16,plain,
! [X2: $int,X1: $int,X0: $int] :
( model_ub(X0,X1,X2)
<=> ? [X3: $int] :
( ub(X0,X1,X3)
& ~ $less(X2,summation(X3)) ) ),
inference(theory_normalization,[],[f6]) ).
tff(f17,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( ! [X3: $int] :
( model_max(X0,X1,X3)
=> ~ $less(X3,X2) )
& model_max(X0,X1,X2) )
<=> minsol_model_max(X0,X1,X2) ),
inference(theory_normalization,[],[f7]) ).
tff(f18,plain,
! [X2: $int,X1: $int,X0: $int] :
( model_max(X0,X1,X2)
<=> ~ $less(X2,summation(max(X0,X1))) ),
inference(theory_normalization,[],[f5]) ).
tff(f19,plain,
! [X0: $int,X2: $int,X1: $int] :
( ub(X2,X1,X0)
<=> ( ~ $less(X0,X2)
& ~ $less(X0,X1) ) ),
inference(rectify,[],[f12]) ).
tff(f20,plain,
! [X1: $int,X2: $int,X0: $int] :
( minsol_model_ub(X1,X2,X0)
<=> ( ! [X3: $int] :
( model_ub(X1,X2,X3)
=> ~ $less(X3,X0) )
& model_ub(X1,X2,X0) ) ),
inference(rectify,[],[f13]) ).
tff(f21,plain,
! [X1: $int,X0: $int] :
( $less(X0,X1)
| ( max(X1,X0) = X0 ) ),
inference(rectify,[],[f14]) ).
tff(f22,plain,
! [X1: $int,X0: $int] :
( ~ $less(X0,X1)
<=> ~ $less(summation(X0),summation(X1)) ),
inference(rectify,[],[f15]) ).
tff(f23,plain,
~ ! [X0: $int,X2: $int,X1: $int] :
( minsol_model_ub(X1,X2,X0)
<=> minsol_model_max(X1,X2,X0) ),
inference(rectify,[],[f10]) ).
tff(f24,plain,
! [X1: $int,X2: $int,X0: $int] :
( ~ $less(X0,summation(max(X2,X1)))
<=> model_max(X2,X1,X0) ),
inference(rectify,[],[f18]) ).
tff(f25,plain,
? [X2: $int,X0: $int,X1: $int] :
( minsol_model_ub(X1,X2,X0)
<~> minsol_model_max(X1,X2,X0) ),
inference(ennf_transformation,[],[f23]) ).
tff(f26,plain,
! [X1: $int,X0: $int,X2: $int] :
( minsol_model_max(X0,X1,X2)
<=> ( ! [X3: $int] :
( ~ model_max(X0,X1,X3)
| ~ $less(X3,X2) )
& model_max(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f17]) ).
tff(f27,plain,
! [X2: $int,X1: $int,X0: $int] :
( minsol_model_ub(X1,X2,X0)
<=> ( ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X1,X2,X3) )
& model_ub(X1,X2,X0) ) ),
inference(ennf_transformation,[],[f20]) ).
tff(f28,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( max(X0,X1) = X1 ) ),
inference(rectify,[],[f21]) ).
tff(f29,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ub(X2,X1,X0)
| $less(X0,X2)
| $less(X0,X1) )
& ( ( ~ $less(X0,X2)
& ~ $less(X0,X1) )
| ~ ub(X2,X1,X0) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f30,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( ub(X2,X1,X0)
| $less(X0,X2)
| $less(X0,X1) )
& ( ( ~ $less(X0,X2)
& ~ $less(X0,X1) )
| ~ ub(X2,X1,X0) ) ),
inference(flattening,[],[f29]) ).
tff(f31,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ub(X1,X2,X0)
| $less(X0,X1)
| $less(X0,X2) )
& ( ( ~ $less(X0,X1)
& ~ $less(X0,X2) )
| ~ ub(X1,X2,X0) ) ),
inference(rectify,[],[f30]) ).
tff(f32,plain,
? [X2: $int,X0: $int,X1: $int] :
( ( ~ minsol_model_max(X1,X2,X0)
| ~ minsol_model_ub(X1,X2,X0) )
& ( minsol_model_max(X1,X2,X0)
| minsol_model_ub(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f25]) ).
tff(f33,plain,
? [X0: $int,X1: $int,X2: $int] :
( ( ~ minsol_model_max(X2,X0,X1)
| ~ minsol_model_ub(X2,X0,X1) )
& ( minsol_model_max(X2,X0,X1)
| minsol_model_ub(X2,X0,X1) ) ),
inference(rectify,[],[f32]) ).
tff(f34,plain,
( ( ~ minsol_model_max(sK2,sK0,sK1)
| ~ minsol_model_ub(sK2,sK0,sK1) )
& ( minsol_model_max(sK2,sK0,sK1)
| minsol_model_ub(sK2,sK0,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f33]) ).
tff(f35,plain,
! [X1: $int,X2: $int,X0: $int] :
( ( ~ $less(X0,summation(max(X2,X1)))
| ~ model_max(X2,X1,X0) )
& ( model_max(X2,X1,X0)
| $less(X0,summation(max(X2,X1))) ) ),
inference(nnf_transformation,[],[f24]) ).
tff(f36,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ~ $less(X2,summation(max(X1,X0)))
| ~ model_max(X1,X0,X2) )
& ( model_max(X1,X0,X2)
| $less(X2,summation(max(X1,X0))) ) ),
inference(rectify,[],[f35]) ).
tff(f37,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( minsol_model_ub(X1,X2,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_ub(X1,X2,X3) )
| ~ model_ub(X1,X2,X0) )
& ( ( ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X1,X2,X3) )
& model_ub(X1,X2,X0) )
| ~ minsol_model_ub(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f38,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( minsol_model_ub(X1,X2,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_ub(X1,X2,X3) )
| ~ model_ub(X1,X2,X0) )
& ( ( ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_ub(X1,X2,X3) )
& model_ub(X1,X2,X0) )
| ~ minsol_model_ub(X1,X2,X0) ) ),
inference(flattening,[],[f37]) ).
tff(f39,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X1,X0,X2)
| ? [X3: $int] :
( $less(X3,X2)
& model_ub(X1,X0,X3) )
| ~ model_ub(X1,X0,X2) )
& ( ( ! [X4: $int] :
( ~ $less(X4,X2)
| ~ model_ub(X1,X0,X4) )
& model_ub(X1,X0,X2) )
| ~ minsol_model_ub(X1,X0,X2) ) ),
inference(rectify,[],[f38]) ).
tff(f40,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X1,X0,X2)
| ( $less(sK3(X0,X1,X2),X2)
& model_ub(X1,X0,sK3(X0,X1,X2)) )
| ~ model_ub(X1,X0,X2) )
& ( ( ! [X4: $int] :
( ~ $less(X4,X2)
| ~ model_ub(X1,X0,X4) )
& model_ub(X1,X0,X2) )
| ~ minsol_model_ub(X1,X0,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f39]) ).
tff(f41,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( minsol_model_max(X0,X1,X2)
| ? [X3: $int] :
( model_max(X0,X1,X3)
& $less(X3,X2) )
| ~ model_max(X0,X1,X2) )
& ( ( ! [X3: $int] :
( ~ model_max(X0,X1,X3)
| ~ $less(X3,X2) )
& model_max(X0,X1,X2) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f26]) ).
tff(f42,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( minsol_model_max(X0,X1,X2)
| ? [X3: $int] :
( model_max(X0,X1,X3)
& $less(X3,X2) )
| ~ model_max(X0,X1,X2) )
& ( ( ! [X3: $int] :
( ~ model_max(X0,X1,X3)
| ~ $less(X3,X2) )
& model_max(X0,X1,X2) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(flattening,[],[f41]) ).
tff(f43,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_max(X1,X0,X2)
| ? [X3: $int] :
( model_max(X1,X0,X3)
& $less(X3,X2) )
| ~ model_max(X1,X0,X2) )
& ( ( ! [X4: $int] :
( ~ model_max(X1,X0,X4)
| ~ $less(X4,X2) )
& model_max(X1,X0,X2) )
| ~ minsol_model_max(X1,X0,X2) ) ),
inference(rectify,[],[f42]) ).
tff(f44,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_max(X1,X0,X2)
| ( model_max(X1,X0,sK4(X0,X1,X2))
& $less(sK4(X0,X1,X2),X2) )
| ~ model_max(X1,X0,X2) )
& ( ( ! [X4: $int] :
( ~ model_max(X1,X0,X4)
| ~ $less(X4,X2) )
& model_max(X1,X0,X2) )
| ~ minsol_model_max(X1,X0,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f43]) ).
tff(f45,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( model_ub(X0,X1,X2)
| ! [X3: $int] :
( ~ ub(X0,X1,X3)
| $less(X2,summation(X3)) ) )
& ( ? [X3: $int] :
( ub(X0,X1,X3)
& ~ $less(X2,summation(X3)) )
| ~ model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f46,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_ub(X2,X1,X0)
| ! [X3: $int] :
( ~ ub(X2,X1,X3)
| $less(X0,summation(X3)) ) )
& ( ? [X4: $int] :
( ub(X2,X1,X4)
& ~ $less(X0,summation(X4)) )
| ~ model_ub(X2,X1,X0) ) ),
inference(rectify,[],[f45]) ).
tff(f47,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_ub(X2,X1,X0)
| ! [X3: $int] :
( ~ ub(X2,X1,X3)
| $less(X0,summation(X3)) ) )
& ( ( ub(X2,X1,sK5(X0,X1,X2))
& ~ $less(X0,summation(sK5(X0,X1,X2))) )
| ~ model_ub(X2,X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X4,sK5(X0,X1,X2))],[f46]) ).
tff(f48,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(X0,X1)
| $less(summation(X0),summation(X1)) )
& ( ~ $less(summation(X0),summation(X1))
| $less(X0,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f49,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(X1,X0)
| $less(summation(X1),summation(X0)) )
& ( ~ $less(summation(X1),summation(X0))
| $less(X1,X0) ) ),
inference(rectify,[],[f48]) ).
tff(f50,plain,
! [X0: $int,X1: $int] :
( ( max(X0,X1) = X1 )
| $less(X1,X0) ),
inference(cnf_transformation,[],[f28]) ).
tff(f51,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X1,X2,X0)
| ~ $less(X0,X2) ),
inference(cnf_transformation,[],[f31]) ).
tff(f52,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X1,X2,X0)
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tff(f53,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X1,X2,X0)
| $less(X0,X2)
| $less(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tff(f54,plain,
( minsol_model_max(sK2,sK0,sK1)
| minsol_model_ub(sK2,sK0,sK1) ),
inference(cnf_transformation,[],[f34]) ).
tff(f55,plain,
( ~ minsol_model_ub(sK2,sK0,sK1)
| ~ minsol_model_max(sK2,sK0,sK1) ),
inference(cnf_transformation,[],[f34]) ).
tff(f56,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X2,summation(max(X1,X0)))
| model_max(X1,X0,X2) ),
inference(cnf_transformation,[],[f36]) ).
tff(f57,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X2,summation(max(X1,X0)))
| ~ model_max(X1,X0,X2) ),
inference(cnf_transformation,[],[f36]) ).
tff(f58,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_ub(X1,X0,X2)
| model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f40]) ).
tff(f59,plain,
! [X2: $int,X0: $int,X1: $int,X4: $int] :
( ~ minsol_model_ub(X1,X0,X2)
| ~ $less(X4,X2)
| ~ model_ub(X1,X0,X4) ),
inference(cnf_transformation,[],[f40]) ).
tff(f60,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_ub(X1,X0,sK3(X0,X1,X2))
| minsol_model_ub(X1,X0,X2)
| ~ model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f40]) ).
tff(f61,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK3(X0,X1,X2),X2)
| minsol_model_ub(X1,X0,X2)
| ~ model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f40]) ).
tff(f62,plain,
! [X0: $int,X1: $int] :
( ( max(X0,X1) = X0 )
| $less(X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
tff(f63,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_max(X1,X0,X2)
| model_max(X1,X0,X2) ),
inference(cnf_transformation,[],[f44]) ).
tff(f64,plain,
! [X2: $int,X0: $int,X1: $int,X4: $int] :
( ~ minsol_model_max(X1,X0,X2)
| ~ model_max(X1,X0,X4)
| ~ $less(X4,X2) ),
inference(cnf_transformation,[],[f44]) ).
tff(f65,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK4(X0,X1,X2),X2)
| ~ model_max(X1,X0,X2)
| minsol_model_max(X1,X0,X2) ),
inference(cnf_transformation,[],[f44]) ).
tff(f66,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_max(X1,X0,sK4(X0,X1,X2))
| minsol_model_max(X1,X0,X2)
| ~ model_max(X1,X0,X2) ),
inference(cnf_transformation,[],[f44]) ).
tff(f67,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X0,summation(sK5(X0,X1,X2)))
| ~ model_ub(X2,X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f68,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X2,X1,sK5(X0,X1,X2))
| ~ model_ub(X2,X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f69,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ ub(X2,X1,X3)
| $less(X0,summation(X3))
| model_ub(X2,X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f70,plain,
! [X0: $int,X1: $int] :
( ~ $less(summation(X1),summation(X0))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f73,definition,
( spl6_1
<=> minsol_model_max(sK2,sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
tff(f74,plain,
( minsol_model_max(sK2,sK0,sK1)
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f75,plain,
( ~ minsol_model_max(sK2,sK0,sK1)
| spl6_1 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f77,definition,
( spl6_2
<=> minsol_model_ub(sK2,sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
tff(f78,plain,
( minsol_model_ub(sK2,sK0,sK1)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f77]) ).
tff(f79,plain,
( ~ minsol_model_ub(sK2,sK0,sK1)
| spl6_2 ),
inference(avatar_component_clause,[],[f77]) ).
tff(f80,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f55,f77,f73]) ).
tff(f81,plain,
( spl6_1
| spl6_2 ),
inference(avatar_split_clause,[],[f54,f77,f73]) ).
tff(f83,plain,
( model_max(sK2,sK0,sK1)
| ~ spl6_1 ),
inference(resolution,[],[f63,f74]) ).
tff(f85,definition,
( spl6_3
<=> model_max(sK2,sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
tff(f86,plain,
( ~ model_max(sK2,sK0,sK1)
| spl6_3 ),
inference(avatar_component_clause,[],[f85]) ).
tff(f87,plain,
( model_max(sK2,sK0,sK1)
| ~ spl6_3 ),
inference(avatar_component_clause,[],[f85]) ).
tff(f88,plain,
( spl6_3
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f83,f73,f85]) ).
tff(f150,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X1,summation(X0))
| model_max(X2,X0,X1)
| $less(X0,X2) ),
inference(superposition,[],[f56,f50]) ).
tff(f151,plain,
( ~ $less(sK1,summation(max(sK2,sK0)))
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f57,f87]) ).
tff(f159,definition,
( spl6_9
<=> $less(sK1,summation(max(sK2,sK0))) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
tff(f161,plain,
( ~ $less(sK1,summation(max(sK2,sK0)))
| spl6_9 ),
inference(avatar_component_clause,[],[f159]) ).
tff(f162,plain,
( ~ spl6_9
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f151,f85,f159]) ).
tff(f170,plain,
( model_max(sK2,sK0,sK1)
| spl6_9 ),
inference(resolution,[],[f161,f56]) ).
tff(f171,plain,
( ~ $less(sK1,summation(sK2))
| $less(sK2,sK0)
| spl6_9 ),
inference(superposition,[],[f161,f62]) ).
tff(f172,plain,
( ~ $less(sK1,summation(sK0))
| $less(sK0,sK2)
| spl6_9 ),
inference(superposition,[],[f161,f50]) ).
tff(f174,definition,
( spl6_10
<=> $less(sK1,summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
tff(f176,plain,
( ~ $less(sK1,summation(sK2))
| spl6_10 ),
inference(avatar_component_clause,[],[f174]) ).
tff(f178,definition,
( spl6_11
<=> $less(sK2,sK0) ),
introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition]) ).
tff(f179,plain,
( ~ $less(sK2,sK0)
| spl6_11 ),
inference(avatar_component_clause,[],[f178]) ).
tff(f181,plain,
( ~ spl6_10
| spl6_11
| spl6_9 ),
inference(avatar_split_clause,[],[f171,f159,f178,f174]) ).
tff(f193,definition,
( spl6_14
<=> $less(sK1,summation(sK0)) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
tff(f195,plain,
( ~ $less(sK1,summation(sK0))
| spl6_14 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f197,definition,
( spl6_15
<=> $less(sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition]) ).
tff(f198,plain,
( ~ $less(sK0,sK2)
| spl6_15 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f200,plain,
( ~ spl6_14
| spl6_15
| spl6_9 ),
inference(avatar_split_clause,[],[f172,f159,f197,f193]) ).
tff(f211,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK5(X2,X1,X0),X0)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f68,f52]) ).
tff(f212,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK5(X2,X1,X0),X1)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f68,f51]) ).
tff(f213,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( $less(X0,summation(X1))
| model_ub(X2,X3,X0)
| $less(X1,X2)
| $less(X1,X3) ),
inference(resolution,[],[f69,f53]) ).
tff(f279,plain,
( ! [X0: $int] :
( ~ model_ub(sK2,sK0,X0)
| ~ $less(X0,sK1) )
| ~ spl6_2 ),
inference(resolution,[],[f78,f59]) ).
tff(f280,plain,
( model_ub(sK2,sK0,sK1)
| ~ spl6_2 ),
inference(resolution,[],[f78,f58]) ).
tff(f282,definition,
( spl6_26
<=> model_ub(sK2,sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_26])],[avatar_definition]) ).
tff(f283,plain,
( ~ model_ub(sK2,sK0,sK1)
| spl6_26 ),
inference(avatar_component_clause,[],[f282]) ).
tff(f284,plain,
( model_ub(sK2,sK0,sK1)
| ~ spl6_26 ),
inference(avatar_component_clause,[],[f282]) ).
tff(f285,plain,
( spl6_26
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f280,f77,f282]) ).
tff(f291,plain,
( ( sK2 = max(sK2,sK0) )
| spl6_11 ),
inference(unit_resulting_resolution,[],[f62,f179]) ).
tff(f305,definition,
( spl6_29
<=> ( sK2 = max(sK2,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl6_29])],[avatar_definition]) ).
tff(f308,plain,
( spl6_29
| spl6_11 ),
inference(avatar_split_clause,[],[f291,f178,f305]) ).
tff(f309,plain,
( ub(sK2,sK0,sK5(sK1,sK0,sK2))
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f68,f284]) ).
tff(f310,plain,
( ~ $less(sK1,summation(sK5(sK1,sK0,sK2)))
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f67,f284]) ).
tff(f314,definition,
( spl6_30
<=> ub(sK2,sK0,sK5(sK1,sK0,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_30])],[avatar_definition]) ).
tff(f316,plain,
( ub(sK2,sK0,sK5(sK1,sK0,sK2))
| ~ spl6_30 ),
inference(avatar_component_clause,[],[f314]) ).
tff(f317,plain,
( spl6_30
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f309,f282,f314]) ).
tff(f319,definition,
( spl6_31
<=> $less(sK1,summation(sK5(sK1,sK0,sK2))) ),
introduced(definition,[new_symbols(definition,[spl6_31])],[avatar_definition]) ).
tff(f322,plain,
( ~ spl6_31
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f310,f282,f319]) ).
tff(f355,plain,
( ~ $less(sK5(sK1,sK0,sK2),sK2)
| ~ spl6_30 ),
inference(resolution,[],[f316,f52]) ).
tff(f356,plain,
( ~ $less(sK5(sK1,sK0,sK2),sK0)
| ~ spl6_30 ),
inference(resolution,[],[f316,f51]) ).
tff(f358,definition,
( spl6_34
<=> $less(sK5(sK1,sK0,sK2),sK0) ),
introduced(definition,[new_symbols(definition,[spl6_34])],[avatar_definition]) ).
tff(f360,plain,
( ~ $less(sK5(sK1,sK0,sK2),sK0)
| spl6_34 ),
inference(avatar_component_clause,[],[f358]) ).
tff(f361,plain,
( ~ spl6_34
| ~ spl6_30 ),
inference(avatar_split_clause,[],[f356,f314,f358]) ).
tff(f363,definition,
( spl6_35
<=> $less(sK5(sK1,sK0,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_35])],[avatar_definition]) ).
tff(f365,plain,
( ~ $less(sK5(sK1,sK0,sK2),sK2)
| spl6_35 ),
inference(avatar_component_clause,[],[f363]) ).
tff(f366,plain,
( ~ spl6_35
| ~ spl6_30 ),
inference(avatar_split_clause,[],[f355,f314,f363]) ).
tff(f465,definition,
( spl6_49
<=> $less(sK2,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_49])],[avatar_definition]) ).
tff(f614,plain,
( ~ $less(summation(sK5(sK1,sK0,sK2)),summation(sK0))
| spl6_34 ),
inference(unit_resulting_resolution,[],[f70,f360]) ).
tff(f645,definition,
( spl6_61
<=> $less(summation(sK5(sK1,sK0,sK2)),summation(sK0)) ),
introduced(definition,[new_symbols(definition,[spl6_61])],[avatar_definition]) ).
tff(f648,plain,
( ~ spl6_61
| spl6_34 ),
inference(avatar_split_clause,[],[f614,f358,f645]) ).
tff(f696,plain,
( $less(sK0,sK2)
| spl6_3
| spl6_14 ),
inference(unit_resulting_resolution,[],[f150,f86,f195]) ).
tff(f752,plain,
( ~ $less(summation(sK5(sK1,sK0,sK2)),summation(sK2))
| spl6_35 ),
inference(unit_resulting_resolution,[],[f70,f365]) ).
tff(f796,definition,
( spl6_85
<=> $less(summation(sK5(sK1,sK0,sK2)),summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_85])],[avatar_definition]) ).
tff(f799,plain,
( ~ spl6_85
| spl6_35 ),
inference(avatar_split_clause,[],[f752,f363,f796]) ).
tff(f809,plain,
( spl6_3
| spl6_9 ),
inference(avatar_split_clause,[],[f170,f159,f85]) ).
tff(f811,plain,
( spl6_15
| spl6_3
| spl6_14 ),
inference(avatar_split_clause,[],[f696,f193,f85,f197]) ).
tff(f813,plain,
( model_max(sK2,sK0,sK4(sK0,sK2,sK1))
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f66,f75,f87]) ).
tff(f814,plain,
( $less(sK4(sK0,sK2,sK1),sK1)
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f65,f75,f87]) ).
tff(f816,definition,
( spl6_88
<=> $less(sK4(sK0,sK2,sK1),sK1) ),
introduced(definition,[new_symbols(definition,[spl6_88])],[avatar_definition]) ).
tff(f818,plain,
( $less(sK4(sK0,sK2,sK1),sK1)
| ~ spl6_88 ),
inference(avatar_component_clause,[],[f816]) ).
tff(f819,plain,
( spl6_88
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f814,f85,f73,f816]) ).
tff(f821,definition,
( spl6_89
<=> model_max(sK2,sK0,sK4(sK0,sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_89])],[avatar_definition]) ).
tff(f823,plain,
( model_max(sK2,sK0,sK4(sK0,sK2,sK1))
| ~ spl6_89 ),
inference(avatar_component_clause,[],[f821]) ).
tff(f824,plain,
( spl6_89
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f813,f85,f73,f821]) ).
tff(f875,plain,
( ~ model_ub(sK2,sK0,sK4(sK0,sK2,sK1))
| ~ spl6_2
| ~ spl6_88 ),
inference(unit_resulting_resolution,[],[f279,f818]) ).
tff(f887,definition,
( spl6_97
<=> model_ub(sK2,sK0,sK4(sK0,sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_97])],[avatar_definition]) ).
tff(f889,plain,
( ~ model_ub(sK2,sK0,sK4(sK0,sK2,sK1))
| spl6_97 ),
inference(avatar_component_clause,[],[f887]) ).
tff(f890,plain,
( ~ spl6_97
| ~ spl6_2
| ~ spl6_88 ),
inference(avatar_split_clause,[],[f875,f816,f77,f887]) ).
tff(f896,plain,
( ~ $less(sK4(sK0,sK2,sK1),summation(max(sK2,sK0)))
| ~ spl6_89 ),
inference(unit_resulting_resolution,[],[f57,f823]) ).
tff(f899,definition,
( spl6_99
<=> $less(sK4(sK0,sK2,sK1),summation(max(sK2,sK0))) ),
introduced(definition,[new_symbols(definition,[spl6_99])],[avatar_definition]) ).
tff(f902,plain,
( ~ spl6_99
| ~ spl6_89 ),
inference(avatar_split_clause,[],[f896,f821,f899]) ).
tff(f903,plain,
( ( max(sK2,sK0) = sK0 )
| spl6_15 ),
inference(unit_resulting_resolution,[],[f50,f198]) ).
tff(f1140,plain,
( $less(sK3(sK0,sK2,sK1),sK1)
| spl6_2
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f61,f284,f79]) ).
tff(f1143,definition,
( spl6_126
<=> model_ub(sK2,sK0,sK3(sK0,sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_126])],[avatar_definition]) ).
tff(f1144,plain,
( ~ model_ub(sK2,sK0,sK3(sK0,sK2,sK1))
| spl6_126 ),
inference(avatar_component_clause,[],[f1143]) ).
tff(f1145,plain,
( model_ub(sK2,sK0,sK3(sK0,sK2,sK1))
| ~ spl6_126 ),
inference(avatar_component_clause,[],[f1143]) ).
tff(f1148,definition,
( spl6_127
<=> $less(sK3(sK0,sK2,sK1),sK1) ),
introduced(definition,[new_symbols(definition,[spl6_127])],[avatar_definition]) ).
tff(f1150,plain,
( $less(sK3(sK0,sK2,sK1),sK1)
| ~ spl6_127 ),
inference(avatar_component_clause,[],[f1148]) ).
tff(f1151,plain,
( spl6_127
| spl6_2
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f1140,f282,f77,f1148]) ).
tff(f1166,plain,
( ~ model_max(sK2,sK0,sK3(sK0,sK2,sK1))
| ~ spl6_1
| ~ spl6_127 ),
inference(unit_resulting_resolution,[],[f64,f74,f1150]) ).
tff(f1179,definition,
( spl6_130
<=> model_max(sK2,sK0,sK3(sK0,sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_130])],[avatar_definition]) ).
tff(f1181,plain,
( ~ model_max(sK2,sK0,sK3(sK0,sK2,sK1))
| spl6_130 ),
inference(avatar_component_clause,[],[f1179]) ).
tff(f1182,plain,
( ~ spl6_130
| ~ spl6_1
| ~ spl6_127 ),
inference(avatar_split_clause,[],[f1166,f1148,f73,f1179]) ).
tff(f1207,plain,
( ~ $less(sK3(sK0,sK2,sK1),summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2)))
| ~ spl6_126 ),
inference(unit_resulting_resolution,[],[f67,f1145]) ).
tff(f1209,plain,
( ~ $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK2)
| ~ spl6_126 ),
inference(unit_resulting_resolution,[],[f211,f1145]) ).
tff(f1210,plain,
( ~ $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK0)
| ~ spl6_126 ),
inference(unit_resulting_resolution,[],[f212,f1145]) ).
tff(f1214,definition,
( spl6_132
<=> $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK0) ),
introduced(definition,[new_symbols(definition,[spl6_132])],[avatar_definition]) ).
tff(f1216,plain,
( ~ $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK0)
| spl6_132 ),
inference(avatar_component_clause,[],[f1214]) ).
tff(f1217,plain,
( ~ spl6_132
| ~ spl6_126 ),
inference(avatar_split_clause,[],[f1210,f1143,f1214]) ).
tff(f1229,definition,
( spl6_135
<=> $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_135])],[avatar_definition]) ).
tff(f1231,plain,
( ~ $less(sK5(sK3(sK0,sK2,sK1),sK0,sK2),sK2)
| spl6_135 ),
inference(avatar_component_clause,[],[f1229]) ).
tff(f1232,plain,
( ~ spl6_135
| ~ spl6_126 ),
inference(avatar_split_clause,[],[f1209,f1143,f1229]) ).
tff(f1239,definition,
( spl6_137
<=> $less(sK3(sK0,sK2,sK1),summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2))) ),
introduced(definition,[new_symbols(definition,[spl6_137])],[avatar_definition]) ).
tff(f1242,plain,
( ~ spl6_137
| ~ spl6_126 ),
inference(avatar_split_clause,[],[f1207,f1143,f1239]) ).
tff(f1261,plain,
( $less(sK3(sK0,sK2,sK1),summation(max(sK2,sK0)))
| spl6_130 ),
inference(unit_resulting_resolution,[],[f56,f1181]) ).
tff(f1275,definition,
( spl6_140
<=> $less(sK3(sK0,sK2,sK1),summation(max(sK2,sK0))) ),
introduced(definition,[new_symbols(definition,[spl6_140])],[avatar_definition]) ).
tff(f1278,plain,
( spl6_140
| spl6_130 ),
inference(avatar_split_clause,[],[f1261,f1179,f1275]) ).
tff(f1663,plain,
( ~ $less(summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2)),summation(sK0))
| spl6_132 ),
inference(unit_resulting_resolution,[],[f70,f1216]) ).
tff(f1678,definition,
( spl6_191
<=> $less(summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2)),summation(sK0)) ),
introduced(definition,[new_symbols(definition,[spl6_191])],[avatar_definition]) ).
tff(f1681,plain,
( ~ spl6_191
| spl6_132 ),
inference(avatar_split_clause,[],[f1663,f1214,f1678]) ).
tff(f1719,definition,
( spl6_198
<=> ( max(sK2,sK0) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl6_198])],[avatar_definition]) ).
tff(f1722,plain,
( spl6_198
| spl6_15 ),
inference(avatar_split_clause,[],[f903,f197,f1719]) ).
tff(f1757,definition,
( spl6_204
<=> ub(sK2,sK0,max(sK2,sK0)) ),
introduced(definition,[new_symbols(definition,[spl6_204])],[avatar_definition]) ).
tff(f1758,plain,
( ub(sK2,sK0,max(sK2,sK0))
| ~ spl6_204 ),
inference(avatar_component_clause,[],[f1757]) ).
tff(f1759,plain,
( ~ ub(sK2,sK0,max(sK2,sK0))
| spl6_204 ),
inference(avatar_component_clause,[],[f1757]) ).
tff(f1779,plain,
( $less(sK2,sK2)
| spl6_10
| spl6_11
| spl6_26 ),
inference(unit_resulting_resolution,[],[f213,f283,f176,f179]) ).
tff(f1781,plain,
( spl6_49
| spl6_10
| spl6_11
| spl6_26 ),
inference(avatar_split_clause,[],[f1779,f282,f178,f174,f465]) ).
tff(f1794,plain,
( ~ model_ub(sK2,sK0,sK1)
| minsol_model_ub(sK2,sK0,sK1)
| spl6_126 ),
inference(resolution,[],[f1144,f60]) ).
tff(f1815,plain,
( $less(sK0,sK0)
| spl6_14
| spl6_15
| spl6_26 ),
inference(unit_resulting_resolution,[],[f213,f283,f195,f198]) ).
tff(f1819,definition,
( spl6_208
<=> $less(sK0,sK0) ),
introduced(definition,[new_symbols(definition,[spl6_208])],[avatar_definition]) ).
tff(f1822,plain,
( spl6_208
| spl6_14
| spl6_15
| spl6_26 ),
inference(avatar_split_clause,[],[f1815,f282,f197,f193,f1819]) ).
tff(f1823,plain,
( ~ spl6_26
| spl6_2
| spl6_126 ),
inference(avatar_split_clause,[],[f1794,f1143,f77,f282]) ).
tff(f1923,plain,
( $less(max(sK2,sK0),sK2)
| $less(max(sK2,sK0),sK0)
| spl6_204 ),
inference(resolution,[],[f1759,f53]) ).
tff(f1927,definition,
( spl6_213
<=> $less(max(sK2,sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl6_213])],[avatar_definition]) ).
tff(f1931,definition,
( spl6_214
<=> $less(max(sK2,sK0),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_214])],[avatar_definition]) ).
tff(f1934,plain,
( spl6_213
| spl6_214
| spl6_204 ),
inference(avatar_split_clause,[],[f1923,f1757,f1931,f1927]) ).
tff(f1935,plain,
( $less(sK4(sK0,sK2,sK1),summation(max(sK2,sK0)))
| spl6_97
| ~ spl6_204 ),
inference(unit_resulting_resolution,[],[f69,f889,f1758]) ).
tff(f1948,plain,
( spl6_99
| spl6_97
| ~ spl6_204 ),
inference(avatar_split_clause,[],[f1935,f1757,f887,f899]) ).
tff(f2070,plain,
( ~ $less(summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2)),summation(sK2))
| spl6_135 ),
inference(unit_resulting_resolution,[],[f70,f1231]) ).
tff(f2093,definition,
( spl6_224
<=> $less(summation(sK5(sK3(sK0,sK2,sK1),sK0,sK2)),summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_224])],[avatar_definition]) ).
tff(f2096,plain,
( ~ spl6_224
| spl6_135 ),
inference(avatar_split_clause,[],[f2070,f1229,f2093]) ).
tff(f2107,plain,
$false,
inference(avatar_smt_refutation,[],[f2096,f1948,f1934,f1823,f1822,f1781,f1722,f1681,f1278,f1242,f1232,f1217,f1182,f1151,f902,f890,f824,f819,f811,f809,f799,f648,f366,f361,f322,f317,f308,f285,f200,f181,f162,f88,f81,f80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM860_1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 21:40:53 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.51/1.49 % (3014818)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.51/1.49 % (3014823)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=960462669:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.51/1.49 % (3014823)Refutation not found, incomplete strategy
% 3.51/1.49 % (3014823)------------------------------
% 3.51/1.49 % (3014823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.49 % (3014823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.49 % (3014823)CaDiCaL version: 2.1.3
% 3.51/1.49 % (3014823)Termination reason: Refutation not found, incomplete strategy
% 3.51/1.49 % (3014823)Time elapsed: 0.022 s
% 3.51/1.49 % (3014823)Peak memory usage: 116 MB
% 3.51/1.49 % (3014823)Instructions burned: 14 (million)
% 3.51/1.49 % (3014827)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2097850535:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.51/1.49 % (3014824)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3286323293:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.51/1.49 % (3014826)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3741813681:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.51/1.49 % (3014829)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3251293429:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.51/1.49 % (3014825)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=370170921:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.51/1.49 % (3014828)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=606715161:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.51/1.49 % (3014827)Instruction limit reached!
% 3.51/1.49 % (3014827)------------------------------
% 3.51/1.49 % (3014827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.49 % (3014827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.49 % (3014827)CaDiCaL version: 2.1.3
% 3.51/1.49 % (3014827)Termination reason: Instruction limit
% 3.51/1.49 % (3014827)Termination phase: Saturation
% 3.51/1.49 % (3014827)Time elapsed: 0.005 s
% 3.51/1.49 % (3014827)Peak memory usage: 89 MB
% 3.51/1.49 % (3014827)Instructions burned: 5 (million)
% 3.51/1.49 % (3014826)Instruction limit reached!
% 3.51/1.49 % (3014826)------------------------------
% 3.51/1.49 % (3014826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.49 % (3014826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.49 % (3014826)CaDiCaL version: 2.1.3
% 3.51/1.49 % (3014826)Termination reason: Instruction limit
% 3.51/1.49 % (3014826)Termination phase: Saturation
% 3.51/1.49 % (3014826)Time elapsed: 0.006 s
% 3.51/1.49 % (3014826)Peak memory usage: 88 MB
% 3.51/1.49 % (3014826)Instructions burned: 8 (million)
% 3.51/1.49 % (3014829)Instruction limit reached!
% 3.51/1.49 % (3014829)------------------------------
% 3.51/1.49 % (3014829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.49 % (3014829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.49 % (3014829)CaDiCaL version: 2.1.3
% 3.51/1.49 % (3014829)Termination reason: Instruction limit
% 3.51/1.49 % (3014829)Termination phase: Saturation
% 3.51/1.49 % (3014829)Time elapsed: 0.046 s
% 3.51/1.49 % (3014829)Peak memory usage: 115 MB
% 3.51/1.49 % (3014829)Instructions burned: 33 (million)
% 3.51/1.49 % (3014828)Instruction limit reached!
% 3.51/1.49 % (3014828)------------------------------
% 3.51/1.49 % (3014828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.49 % (3014828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.49 % (3014828)CaDiCaL version: 2.1.3
% 3.51/1.49 % (3014828)Termination reason: Instruction limit
% 3.51/1.49 % (3014828)Termination phase: Saturation
% 3.51/1.49 % (3014828)Time elapsed: 0.057 s
% 3.51/1.49 % (3014828)Peak memory usage: 115 MB
% 3.51/1.49 % (3014828)Instructions burned: 46 (million)
% 3.51/1.49 % (3014823)------------------------------
% 3.51/1.49 % (3014823)------------------------------
% 3.51/1.49 % (3014838)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=604719183:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 5.00/1.67 % (3014837)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=823589139:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.00/1.67 % (3014825)Instruction limit reached!
% 5.00/1.67 % (3014825)------------------------------
% 5.00/1.67 % (3014825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014825)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014825)Termination reason: Instruction limit
% 5.00/1.67 % (3014825)Termination phase: Saturation
% 5.00/1.67 % (3014825)Time elapsed: 0.163 s
% 5.00/1.67 % (3014825)Peak memory usage: 117 MB
% 5.00/1.67 % (3014825)Instructions burned: 202 (million)
% 5.00/1.67 % (3014837)Instruction limit reached!
% 5.00/1.67 % (3014837)------------------------------
% 5.00/1.67 % (3014837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014837)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014837)Termination reason: Instruction limit
% 5.00/1.67 % (3014837)Termination phase: Saturation
% 5.00/1.67 % (3014837)Time elapsed: 0.012 s
% 5.00/1.67 % (3014837)Peak memory usage: 88 MB
% 5.00/1.67 % (3014837)Instructions burned: 15 (million)
% 5.00/1.67 % (3014838)Instruction limit reached!
% 5.00/1.67 % (3014838)------------------------------
% 5.00/1.67 % (3014838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014838)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014838)Termination reason: Instruction limit
% 5.00/1.67 % (3014838)Termination phase: Saturation
% 5.00/1.67 % (3014838)Time elapsed: 0.024 s
% 5.00/1.67 % (3014838)Peak memory usage: 88 MB
% 5.00/1.67 % (3014838)Instructions burned: 30 (million)
% 5.00/1.67 % (3014839)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1515995413:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.00/1.67 % (3014840)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=165074160:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 5.00/1.67 % (3014839)Instruction limit reached!
% 5.00/1.67 % (3014839)------------------------------
% 5.00/1.67 % (3014839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014839)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014839)Termination reason: Instruction limit
% 5.00/1.67 % (3014839)Termination phase: Saturation
% 5.00/1.67 % (3014839)Time elapsed: 0.011 s
% 5.00/1.67 % (3014839)Peak memory usage: 90 MB
% 5.00/1.67 % (3014839)Instructions burned: 17 (million)
% 5.00/1.67 % (3014840)Instruction limit reached!
% 5.00/1.67 % (3014840)------------------------------
% 5.00/1.67 % (3014840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014840)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014840)Termination reason: Instruction limit
% 5.00/1.67 % (3014840)Termination phase: Saturation
% 5.00/1.67 % (3014840)Time elapsed: 0.019 s
% 5.00/1.67 % (3014840)Peak memory usage: 89 MB
% 5.00/1.67 % (3014840)Instructions burned: 24 (million)
% 5.00/1.67 % (3014824)Instruction limit reached!
% 5.00/1.67 % (3014824)------------------------------
% 5.00/1.67 % (3014824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.67 % (3014824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.67 % (3014824)CaDiCaL version: 2.1.3
% 5.00/1.67 % (3014824)Termination reason: Instruction limit
% 5.00/1.67 % (3014824)Termination phase: Saturation
% 5.00/1.67 % (3014824)Time elapsed: 0.241 s
% 5.00/1.67 % (3014824)Peak memory usage: 117 MB
% 5.00/1.67 % (3014824)Instructions burned: 307 (million)
% 5.00/1.67 % (3014841)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=3267103206:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 5.00/1.67 % (3014841)Refutation not found, incomplete strategy
% 5.00/1.67 % (3014841)------------------------------
% 5.00/1.67 % (3014841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.86 % (3014841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.86 % (3014841)CaDiCaL version: 2.1.3
% 6.31/1.86 % (3014841)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.86 % (3014841)Time elapsed: 0.002 s
% 6.31/1.86 % (3014841)Peak memory usage: 89 MB
% 6.31/1.86 % (3014841)Instructions burned: 1 (million)
% 6.31/1.86 % (3014845)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=551595941:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 6.31/1.86 % (3014844)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2944955662:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.31/1.86 % (3014845)Instruction limit reached!
% 6.31/1.86 % (3014845)------------------------------
% 6.31/1.86 % (3014845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.86 % (3014845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.86 % (3014845)CaDiCaL version: 2.1.3
% 6.31/1.86 % (3014845)Termination reason: Instruction limit
% 6.31/1.87 % (3014845)Termination phase: Saturation
% 6.31/1.87 % (3014845)Time elapsed: 0.003 s
% 6.31/1.87 % (3014845)Peak memory usage: 88 MB
% 6.31/1.87 % (3014845)Instructions burned: 3 (million)
% 6.31/1.87 % (3014846)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4239809286:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 6.31/1.87 % (3014844)Instruction limit reached!
% 6.31/1.87 % (3014844)------------------------------
% 6.31/1.87 % (3014844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.87 % (3014844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.87 % (3014844)CaDiCaL version: 2.1.3
% 6.31/1.87 % (3014844)Termination reason: Instruction limit
% 6.31/1.87 % (3014844)Termination phase: Saturation
% 6.31/1.87 % (3014844)Time elapsed: 0.055 s
% 6.31/1.87 % (3014844)Peak memory usage: 89 MB
% 6.31/1.87 % (3014844)Instructions burned: 86 (million)
% 6.31/1.87 % (3014849)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2500402088:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 6.31/1.87 % (3014849)Refutation not found, incomplete strategy
% 6.31/1.87 % (3014849)------------------------------
% 6.31/1.87 % (3014849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.87 % (3014849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.87 % (3014849)CaDiCaL version: 2.1.3
% 6.31/1.87 % (3014849)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.87 % (3014849)Time elapsed: 0.003 s
% 6.31/1.87 % (3014849)Peak memory usage: 89 MB
% 6.31/1.87 % (3014849)Instructions burned: 2 (million)
% 6.31/1.87 % (3014851)lrs+10_1_thi=all:si=on:fd=off:random_seed=820281603:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 6.31/1.87 % (3014850)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=112122452:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 6.31/1.87 % (3014841)------------------------------
% 6.31/1.87 % (3014841)------------------------------
% 6.31/1.87 % (3014846)Instruction limit reached!
% 6.31/1.87 % (3014846)------------------------------
% 6.31/1.87 % (3014846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.87 % (3014846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.87 % (3014846)CaDiCaL version: 2.1.3
% 6.31/1.87 % (3014846)Termination reason: Instruction limit
% 6.31/1.87 % (3014846)Termination phase: Saturation
% 6.31/1.87 % (3014846)Time elapsed: 0.118 s
% 6.31/1.87 % (3014846)Peak memory usage: 90 MB
% 6.31/1.87 % (3014846)Instructions burned: 181 (million)
% 6.31/1.87 % (3014851)Instruction limit reached!
% 6.31/1.87 % (3014851)------------------------------
% 6.31/1.87 % (3014851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.87 % (3014851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.87 % (3014851)CaDiCaL version: 2.1.3
% 6.31/1.87 % (3014851)Termination reason: Instruction limit
% 6.31/1.87 % (3014851)Termination phase: Saturation
% 6.31/1.87 % (3014851)Time elapsed: 0.065 s
% 6.31/1.87 % (3014851)Peak memory usage: 116 MB
% 6.31/1.87 % (3014851)Instructions burned: 54 (million)
% 6.31/1.87 % (3014855)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=289097338:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 8.81/2.08 % (3014855)Instruction limit reached!
% 8.81/2.08 % (3014855)------------------------------
% 8.81/2.08 % (3014855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014855)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014855)Termination reason: Instruction limit
% 8.81/2.08 % (3014855)Termination phase: Saturation
% 8.81/2.08 % (3014855)Time elapsed: 0.007 s
% 8.81/2.08 % (3014855)Peak memory usage: 89 MB
% 8.81/2.08 % (3014855)Instructions burned: 9 (million)
% 8.81/2.08 % (3014850)Instruction limit reached!
% 8.81/2.08 % (3014850)------------------------------
% 8.81/2.08 % (3014850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014850)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014850)Termination reason: Instruction limit
% 8.81/2.08 % (3014850)Termination phase: Saturation
% 8.81/2.08 % (3014850)Time elapsed: 0.095 s
% 8.81/2.08 % (3014850)Peak memory usage: 133 MB
% 8.81/2.08 % (3014850)Instructions burned: 66 (million)
% 8.81/2.08 % (3014861)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1832683167:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.81/2.08 % (3014861)Instruction limit reached!
% 8.81/2.08 % (3014861)------------------------------
% 8.81/2.08 % (3014861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014861)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014861)Termination reason: Instruction limit
% 8.81/2.08 % (3014861)Termination phase: Saturation
% 8.81/2.08 % (3014861)Time elapsed: 0.002 s
% 8.81/2.08 % (3014861)Peak memory usage: 89 MB
% 8.81/2.08 % (3014861)Instructions burned: 3 (million)
% 8.81/2.08 % (3014857)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1011962688:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 8.81/2.08 % (3014857)Instruction limit reached!
% 8.81/2.08 % (3014857)------------------------------
% 8.81/2.08 % (3014857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014857)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014857)Termination reason: Instruction limit
% 8.81/2.08 % (3014857)Termination phase: Saturation
% 8.81/2.08 % (3014857)Time elapsed: 0.002 s
% 8.81/2.08 % (3014857)Peak memory usage: 88 MB
% 8.81/2.08 % (3014857)Instructions burned: 2 (million)
% 8.81/2.08 % (3014862)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=577462714:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 8.81/2.08 % (3014864)dis+10_1_si=on:random_seed=1678467915:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 8.81/2.08 % (3014864)Instruction limit reached!
% 8.81/2.08 % (3014864)------------------------------
% 8.81/2.08 % (3014864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014864)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014864)Termination reason: Instruction limit
% 8.81/2.08 % (3014864)Termination phase: Saturation
% 8.81/2.08 % (3014864)Time elapsed: 0.009 s
% 8.81/2.08 % (3014864)Peak memory usage: 88 MB
% 8.81/2.08 % (3014864)Instructions burned: 11 (million)
% 8.81/2.08 % (3014849)------------------------------
% 8.81/2.08 % (3014849)------------------------------
% 8.81/2.08 % (3014865)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=773232131:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 8.81/2.08 % (3014865)Refutation not found, incomplete strategy
% 8.81/2.08 % (3014865)------------------------------
% 8.81/2.08 % (3014865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/2.08 % (3014865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/2.08 % (3014865)CaDiCaL version: 2.1.3
% 8.81/2.08 % (3014865)Termination reason: Refutation not found, incomplete strategy
% 8.81/2.08 % (3014865)Time elapsed: 0.002 s
% 8.81/2.08 % (3014865)Peak memory usage: 88 MB
% 8.81/2.08 % (3014865)Instructions burned: 1 (million)
% 8.81/2.08 % (3014869)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2848228350:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.11/2.34 % (3014869)Instruction limit reached!
% 10.11/2.34 % (3014869)------------------------------
% 10.11/2.34 % (3014869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.34 % (3014869)CaDiCaL version: 2.1.3
% 10.11/2.34 % (3014869)Termination reason: Instruction limit
% 10.11/2.34 % (3014869)Termination phase: Saturation
% 10.11/2.34 % (3014869)Time elapsed: 0.002 s
% 10.11/2.34 % (3014869)Peak memory usage: 89 MB
% 10.11/2.34 % (3014869)Instructions burned: 4 (million)
% 10.11/2.34 % (3014866)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=721581357:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi)
% 10.11/2.34 % (3014866)Instruction limit reached!
% 10.11/2.34 % (3014866)------------------------------
% 10.11/2.34 % (3014866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.34 % (3014866)CaDiCaL version: 2.1.3
% 10.11/2.34 % (3014866)Termination reason: Instruction limit
% 10.11/2.34 % (3014866)Termination phase: Saturation
% 10.11/2.34 % (3014866)Time elapsed: 0.031 s
% 10.11/2.34 % (3014866)Peak memory usage: 89 MB
% 10.11/2.34 % (3014866)Instructions burned: 36 (million)
% 10.11/2.34 % (3014870)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3967892458:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi)
% 10.11/2.34 % (3014870)Instruction limit reached!
% 10.11/2.34 % (3014870)------------------------------
% 10.11/2.34 % (3014870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.34 % (3014870)CaDiCaL version: 2.1.3
% 10.11/2.34 % (3014870)Termination reason: Instruction limit
% 10.11/2.34 % (3014870)Termination phase: Saturation
% 10.11/2.34 % (3014870)Time elapsed: 0.007 s
% 10.11/2.34 % (3014870)Peak memory usage: 88 MB
% 10.11/2.34 % (3014870)Instructions burned: 8 (million)
% 10.11/2.34 % (3014862)Instruction limit reached!
% 10.11/2.34 % (3014862)------------------------------
% 10.11/2.34 % (3014862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.34 % (3014862)CaDiCaL version: 2.1.3
% 10.11/2.34 % (3014862)Termination reason: Instruction limit
% 10.11/2.34 % (3014862)Termination phase: Saturation
% 10.11/2.34 % (3014862)Time elapsed: 0.120 s
% 10.11/2.34 % (3014862)Peak memory usage: 117 MB
% 10.11/2.34 % (3014862)Instructions burned: 128 (million)
% 10.11/2.34 % (3014878)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2680136507:i=226:rtra=on:gtg=position:ss=axioms_2991 on theBenchmark for (2991ds/226Mi)
% 10.11/2.34 % (3014873)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3596417364:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 10.11/2.34 % (3014875)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1787059417:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 10.11/2.34 % (3014875)Instruction limit reached!
% 10.11/2.34 % (3014875)------------------------------
% 10.11/2.34 % (3014875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.34 % (3014875)CaDiCaL version: 2.1.3
% 10.11/2.34 % (3014875)Termination reason: Instruction limit
% 10.11/2.34 % (3014875)Termination phase: Saturation
% 10.11/2.34 % (3014875)Time elapsed: 0.032 s
% 10.11/2.34 % (3014875)Peak memory usage: 116 MB
% 10.11/2.34 % (3014875)Instructions burned: 13 (million)
% 10.11/2.34 % (3014879)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=562566210:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.11/2.34 % (3014879)Instruction limit reached!
% 10.11/2.34 % (3014879)------------------------------
% 10.11/2.34 % (3014879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.34 % (3014879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.64 % (3014879)CaDiCaL version: 2.1.3
% 11.70/2.64 % (3014879)Termination reason: Instruction limit
% 11.70/2.64 % (3014879)Termination phase: Saturation
% 11.70/2.64 % (3014879)Time elapsed: 0.008 s
% 11.70/2.64 % (3014879)Peak memory usage: 88 MB
% 11.70/2.64 % (3014879)Instructions burned: 10 (million)
% 11.70/2.64 % (3014878)Instruction limit reached!
% 11.70/2.64 % (3014878)------------------------------
% 11.70/2.64 % (3014878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.64 % (3014878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.64 % (3014878)CaDiCaL version: 2.1.3
% 11.70/2.64 % (3014878)Termination reason: Instruction limit
% 11.70/2.64 % (3014878)Termination phase: Saturation
% 11.70/2.64 % (3014878)Time elapsed: 0.093 s
% 11.70/2.64 % (3014878)Peak memory usage: 117 MB
% 11.70/2.64 % (3014878)Instructions burned: 228 (million)
% 11.70/2.64 % (3014881)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=421500205:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi)
% 11.70/2.64 % (3014865)------------------------------
% 11.70/2.64 % (3014865)------------------------------
% 11.70/2.64 % (3014882)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=4207002606:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2990 on theBenchmark for (2990ds/75Mi)
% 11.70/2.64 % (3014882)Instruction limit reached!
% 11.70/2.64 % (3014882)------------------------------
% 11.70/2.64 % (3014882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.64 % (3014882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.64 % (3014882)CaDiCaL version: 2.1.3
% 11.70/2.64 % (3014882)Termination reason: Instruction limit
% 11.70/2.64 % (3014882)Termination phase: Saturation
% 11.70/2.64 % (3014882)Time elapsed: 0.051 s
% 11.70/2.64 % (3014882)Peak memory usage: 90 MB
% 11.70/2.64 % (3014882)Instructions burned: 75 (million)
% 11.70/2.64 % (3014881)Instruction limit reached!
% 11.70/2.64 % (3014881)------------------------------
% 11.70/2.64 % (3014881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.64 % (3014881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.65 % (3014881)CaDiCaL version: 2.1.3
% 11.70/2.65 % (3014881)Termination reason: Instruction limit
% 11.70/2.65 % (3014881)Termination phase: Saturation
% 11.70/2.65 % (3014881)Time elapsed: 0.098 s
% 11.70/2.65 % (3014881)Peak memory usage: 133 MB
% 11.70/2.65 % (3014881)Instructions burned: 71 (million)
% 11.70/2.65 % (3014886)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=4120860708:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi)
% 11.70/2.65 % (3014890)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=813517327:i=131:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.70/2.65 % (3014888)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3917881469:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/130Mi)
% 11.70/2.65 % (3014873)Instruction limit reached!
% 11.70/2.65 % (3014873)------------------------------
% 11.70/2.65 % (3014873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.65 % (3014873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.65 % (3014873)CaDiCaL version: 2.1.3
% 11.70/2.65 % (3014873)Termination reason: Instruction limit
% 11.70/2.65 % (3014873)Termination phase: Saturation
% 11.70/2.65 % (3014873)Time elapsed: 0.227 s
% 11.70/2.65 % (3014873)Peak memory usage: 91 MB
% 11.70/2.65 % (3014873)Instructions burned: 371 (million)
% 11.70/2.65 % (3014892)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2311846758:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 11.70/2.65 % (3014890)Instruction limit reached!
% 11.70/2.65 % (3014890)------------------------------
% 11.70/2.65 % (3014890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.65 % (3014890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.65 % (3014890)CaDiCaL version: 2.1.3
% 11.70/2.65 % (3014890)Termination reason: Instruction limit
% 11.70/2.65 % (3014890)Termination phase: Saturation
% 11.70/2.65 % (3014890)Time elapsed: 0.077 s
% 11.70/2.65 % (3014890)Peak memory usage: 134 MB
% 11.70/2.65 % (3014890)Instructions burned: 132 (million)
% 12.85/3.01 % (3014888)Instruction limit reached!
% 12.85/3.01 % (3014888)------------------------------
% 12.85/3.01 % (3014888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014888)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014888)Termination reason: Instruction limit
% 12.85/3.01 % (3014888)Termination phase: Saturation
% 12.85/3.01 % (3014888)Time elapsed: 0.113 s
% 12.85/3.01 % (3014888)Peak memory usage: 117 MB
% 12.85/3.01 % (3014888)Instructions burned: 130 (million)
% 12.85/3.01 % (3014893)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2638464373:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi)
% 12.85/3.01 % (3014892)Instruction limit reached!
% 12.85/3.01 % (3014892)------------------------------
% 12.85/3.01 % (3014892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014892)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014892)Termination reason: Instruction limit
% 12.85/3.01 % (3014892)Termination phase: Saturation
% 12.85/3.01 % (3014892)Time elapsed: 0.070 s
% 12.85/3.01 % (3014892)Peak memory usage: 133 MB
% 12.85/3.01 % (3014892)Instructions burned: 41 (million)
% 12.85/3.01 % (3014895)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2023822665:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi)
% 12.85/3.01 % (3014898)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3528080556:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 12.85/3.01 % (3014886)Instruction limit reached!
% 12.85/3.01 % (3014886)------------------------------
% 12.85/3.01 % (3014886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014886)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014886)Termination reason: Instruction limit
% 12.85/3.01 % (3014886)Termination phase: Saturation
% 12.85/3.01 % (3014886)Time elapsed: 0.208 s
% 12.85/3.01 % (3014886)Peak memory usage: 90 MB
% 12.85/3.01 % (3014886)Instructions burned: 295 (million)
% 12.85/3.01 % (3014900)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=3430334603:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi)
% 12.85/3.01 % (3014902)dis+10_1_si=on:random_seed=3658927104:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 12.85/3.01 % (3014898)Instruction limit reached!
% 12.85/3.01 % (3014898)------------------------------
% 12.85/3.01 % (3014898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014898)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014898)Termination reason: Instruction limit
% 12.85/3.01 % (3014898)Termination phase: Saturation
% 12.85/3.01 % (3014898)Time elapsed: 0.100 s
% 12.85/3.01 % (3014898)Peak memory usage: 117 MB
% 12.85/3.01 % (3014898)Instructions burned: 132 (million)
% 12.85/3.01 % (3014903)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4048901298:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 12.85/3.01 % (3014900)Instruction limit reached!
% 12.85/3.01 % (3014900)------------------------------
% 12.85/3.01 % (3014900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014900)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014900)Termination reason: Instruction limit
% 12.85/3.01 % (3014900)Termination phase: Saturation
% 12.85/3.01 % (3014900)Time elapsed: 0.107 s
% 12.85/3.01 % (3014900)Peak memory usage: 117 MB
% 12.85/3.01 % (3014900)Instructions burned: 260 (million)
% 12.85/3.01 % (3014893)Instruction limit reached!
% 12.85/3.01 % (3014893)------------------------------
% 12.85/3.01 % (3014893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014893)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014893)Termination reason: Instruction limit
% 12.85/3.01 % (3014893)Termination phase: Saturation
% 12.85/3.01 % (3014893)Time elapsed: 0.214 s
% 12.85/3.01 % (3014893)Peak memory usage: 91 MB
% 12.85/3.01 % (3014893)Instructions burned: 307 (million)
% 12.85/3.01 % (3014906)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=843270259:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi)
% 12.85/3.01 % (3014909)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1428067202:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi)
% 12.85/3.01 % (3014911)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3967060007:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi)
% 12.85/3.01 % (3014906)Instruction limit reached!
% 12.85/3.01 % (3014906)------------------------------
% 12.85/3.01 % (3014906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014906)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014906)Termination reason: Instruction limit
% 12.85/3.01 % (3014906)Termination phase: Saturation
% 12.85/3.01 % (3014906)Time elapsed: 0.094 s
% 12.85/3.01 % (3014906)Peak memory usage: 90 MB
% 12.85/3.01 % (3014906)Instructions burned: 142 (million)
% 12.85/3.01 % (3014911)Instruction limit reached!
% 12.85/3.01 % (3014911)------------------------------
% 12.85/3.01 % (3014911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014911)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014911)Termination reason: Instruction limit
% 12.85/3.01 % (3014911)Termination phase: Saturation
% 12.85/3.01 % (3014911)Time elapsed: 0.039 s
% 12.85/3.01 % (3014911)Peak memory usage: 89 MB
% 12.85/3.01 % (3014911)Instructions burned: 124 (million)
% 12.85/3.01 % (3014909)Instruction limit reached!
% 12.85/3.01 % (3014909)------------------------------
% 12.85/3.01 % (3014909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014909)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014909)Termination reason: Instruction limit
% 12.85/3.01 % (3014909)Termination phase: Saturation
% 12.85/3.01 % (3014909)Time elapsed: 0.056 s
% 12.85/3.01 % (3014909)Peak memory usage: 116 MB
% 12.85/3.01 % (3014909)Instructions burned: 65 (million)
% 12.85/3.01 % (3014895)First to succeed.
% 12.85/3.01 % (3014912)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=3058655388:s2a=on:i=128:s2at=5:ins=3:rtra=on_2984 on theBenchmark for (2984ds/128Mi)
% 12.85/3.01 % (3014895)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3014818"
% 12.85/3.01 % (3014903)Instruction limit reached!
% 12.85/3.01 % (3014903)------------------------------
% 12.85/3.01 % (3014903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014903)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014903)Termination reason: Instruction limit
% 12.85/3.01 % (3014903)Termination phase: Saturation
% 12.85/3.01 % (3014903)Time elapsed: 0.214 s
% 12.85/3.01 % (3014903)Peak memory usage: 92 MB
% 12.85/3.01 % (3014903)Instructions burned: 384 (million)
% 12.85/3.01 % (3014917)dis+1010_1_to=kbo:si=on:random_seed=643415467:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi)
% 12.85/3.01 % (3014912)Instruction limit reached!
% 12.85/3.01 % (3014912)------------------------------
% 12.85/3.01 % (3014912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014912)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014912)Termination reason: Instruction limit
% 12.85/3.01 % (3014912)Termination phase: Saturation
% 12.85/3.01 % (3014912)Time elapsed: 0.114 s
% 12.85/3.01 % (3014912)Peak memory usage: 117 MB
% 12.85/3.01 % (3014912)Instructions burned: 129 (million)
% 12.85/3.01 % (3014916)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=3701848957:i=39:ins=3:rtra=on_2983 on theBenchmark for (2983ds/39Mi)
% 12.85/3.01 % (3014917)Instruction limit reached!
% 12.85/3.01 % (3014917)------------------------------
% 12.85/3.01 % (3014917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014917)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014917)Termination reason: Instruction limit
% 12.85/3.01 % (3014917)Termination phase: Saturation
% 12.85/3.01 % (3014917)Time elapsed: 0.065 s
% 12.85/3.01 % (3014917)Peak memory usage: 90 MB
% 12.85/3.01 % (3014917)Instructions burned: 177 (million)
% 12.85/3.01 % (3014918)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4287189149:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi)
% 12.85/3.01 % (3014920)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1557773035:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi)
% 12.85/3.01 % (3014916)Instruction limit reached!
% 12.85/3.01 % (3014916)------------------------------
% 12.85/3.01 % (3014916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014916)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014916)Termination reason: Instruction limit
% 12.85/3.01 % (3014916)Termination phase: Saturation
% 12.85/3.01 % (3014916)Time elapsed: 0.054 s
% 12.85/3.01 % (3014916)Peak memory usage: 116 MB
% 12.85/3.01 % (3014916)Instructions burned: 40 (million)
% 12.85/3.01 % (3014920)Refutation not found, SMT solver inside AVATAR returned Unknown
% 12.85/3.01 % (3014920)------------------------------
% 12.85/3.01 % (3014920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.85/3.01 % (3014920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.85/3.01 % (3014920)CaDiCaL version: 2.1.3
% 12.85/3.01 % (3014920)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 12.85/3.01 % (3014920)Time elapsed: 0.107 s
% 12.85/3.01 % (3014920)Peak memory usage: 133 MB
% 12.85/3.01 % (3014920)Instructions burned: 75 (million)
% 12.85/3.01 % (3014920)------------------------------
% 12.85/3.01 % (3014920)------------------------------
% 12.85/3.01 % (3014895)Refutation found. Thanks to Tanya!
% 12.85/3.01 % SZS status Theorem for theBenchmark
% 12.85/3.01 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/3.21 % (3014895)------------------------------
% 0.16/3.21 % (3014895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.21 % (3014895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.21 % (3014895)CaDiCaL version: 2.1.3
% 0.16/3.21 % (3014895)Termination reason: Refutation
% 0.16/3.21 % (3014895)Time elapsed: 0.353 s
% 0.16/3.21 % (3014895)Peak memory usage: 137 MB
% 0.16/3.21 % (3014895)Instructions burned: 463 (million)
% 0.16/3.21 % (3014895)------------------------------
% 0.16/3.21 % (3014895)------------------------------
% 0.16/3.21 % (3014818)Success in time 2.172 s
% 0.16/3.21 % Vampire exiting
%------------------------------------------------------------------------------