%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM862_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 : n014.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.45s
% Output : Refutation 11.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 45
% Syntax : Number of formulae : 210 ( 1 unt; 0 typ; 36 def)
% Number of atoms : 569 ( 12 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 586 ( 227 ~; 238 |; 56 &)
% ( 58 <=>; 6 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 440 ( 158 atm; 40 fun; 0 num; 242 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 : 45 ( 41 usr; 37 prp; 0-3 aty)
% Number of functors : 13 ( 12 usr; 7 con; 0-3 aty)
% Number of variables : 242 ( 222 !; 20 ?; 242 :)
% 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 ).
tff(func_def_6,type,
sK2: $int ).
tff(func_def_7,type,
sK3: $int ).
tff(func_def_8,type,
sK4: ( $int * $int * $int ) > $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(f1,axiom,
! [X0: $int,X1: $int] :
( $lesseq(summation(X0),summation(X1))
<=> $lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',summation_monotone) ).
tff(f2,axiom,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X0 )
| ~ $lesseq(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_1) ).
tff(f3,axiom,
! [X0: $int,X1: $int] :
( ( max(X0,X1) = X1 )
| ~ $lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_2) ).
tff(f4,axiom,
! [X1: $int,X0: $int,X2: $int] :
( ub(X0,X1,X2)
<=> ( $lesseq(X1,X2)
& $lesseq(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ub) ).
tff(f5,axiom,
! [X0: $int,X2: $int,X1: $int] :
( $lesseq($sum(c,summation(max(X0,X1))),X2)
<=> model_max(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_max_5) ).
tff(f6,axiom,
! [X1: $int,X2: $int,X0: $int] :
( ? [X3: $int] :
( ub(X0,X1,X3)
& $lesseq($sum(c,summation(X3)),X2) )
<=> model_ub(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_ub_5) ).
tff(f7,axiom,
! [X2: $int,X0: $int,X1: $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,
! [X1: $int,X2: $int,X0: $int] :
( ( ! [X3: $int] :
( model_ub(X0,X1,X3)
=> $lesseq(X2,X3) )
& model_ub(X0,X1,X2) )
<=> minsol_model_ub(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minsol_model_ub) ).
tff(f9,conjecture,
! [X2: $int,X1: $int,X0: $int] :
( minsol_model_max(X0,X1,X2)
<=> minsol_model_ub(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_ub_1) ).
tff(f10,negated_conjecture,
~ ! [X2: $int,X1: $int,X0: $int] :
( minsol_model_max(X0,X1,X2)
<=> minsol_model_ub(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f9]) ).
tff(f11,plain,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X0 )
| $less(X0,X1) ),
inference(theory_normalization,[],[f2]) ).
tff(f12,plain,
! [X1: $int,X2: $int,X0: $int] :
( ? [X3: $int] :
( ub(X0,X1,X3)
& ~ $less(X2,$sum(c,summation(X3))) )
<=> model_ub(X0,X1,X2) ),
inference(theory_normalization,[],[f6]) ).
tff(f13,plain,
! [X1: $int,X0: $int,X2: $int] :
( ub(X0,X1,X2)
<=> ( ~ $less(X2,X1)
& ~ $less(X2,X0) ) ),
inference(theory_normalization,[],[f4]) ).
tff(f14,plain,
! [X0: $int,X2: $int,X1: $int] :
( ~ $less(X2,$sum(c,summation(max(X0,X1))))
<=> model_max(X0,X1,X2) ),
inference(theory_normalization,[],[f5]) ).
tff(f15,plain,
! [X1: $int,X2: $int,X0: $int] :
( ( ! [X3: $int] :
( model_ub(X0,X1,X3)
=> ~ $less(X3,X2) )
& model_ub(X0,X1,X2) )
<=> minsol_model_ub(X0,X1,X2) ),
inference(theory_normalization,[],[f8]) ).
tff(f16,plain,
! [X0: $int,X1: $int] :
( ~ $less(summation(X1),summation(X0))
<=> ~ $less(X1,X0) ),
inference(theory_normalization,[],[f1]) ).
tff(f17,plain,
! [X1: $int,X0: $int] :
( $less(X1,X0)
| ( max(X0,X1) = X1 ) ),
inference(theory_normalization,[],[f3]) ).
tff(f18,plain,
! [X2: $int,X0: $int,X1: $int] :
( minsol_model_max(X0,X1,X2)
<=> ( model_max(X0,X1,X2)
& ! [X3: $int] :
( model_max(X0,X1,X3)
=> ~ $less(X3,X2) ) ) ),
inference(theory_normalization,[],[f7]) ).
tff(f19,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| $less(X1,X0) ),
inference(rectify,[],[f11]) ).
tff(f20,plain,
! [X0: $int,X2: $int,X1: $int] :
( model_ub(X2,X0,X1)
<=> ? [X3: $int] :
( ub(X2,X0,X3)
& ~ $less(X1,$sum(c,summation(X3))) ) ),
inference(rectify,[],[f12]) ).
tff(f21,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( ~ $less(X2,X0)
& ~ $less(X2,X1) )
<=> ub(X1,X0,X2) ),
inference(rectify,[],[f13]) ).
tff(f22,plain,
! [X2: $int,X1: $int,X0: $int] :
( model_max(X0,X2,X1)
<=> ~ $less(X1,$sum(c,summation(max(X0,X2)))) ),
inference(rectify,[],[f14]) ).
tff(f23,plain,
! [X1: $int,X2: $int,X0: $int] :
( minsol_model_ub(X2,X0,X1)
<=> ( ! [X3: $int] :
( model_ub(X2,X0,X3)
=> ~ $less(X3,X1) )
& model_ub(X2,X0,X1) ) ),
inference(rectify,[],[f15]) ).
tff(f24,plain,
~ ! [X1: $int,X0: $int,X2: $int] :
( minsol_model_ub(X2,X1,X0)
<=> minsol_model_max(X2,X1,X0) ),
inference(rectify,[],[f10]) ).
tff(f25,plain,
! [X0: $int,X2: $int,X1: $int] :
( minsol_model_max(X1,X2,X0)
<=> ( ! [X3: $int] :
( model_max(X1,X2,X3)
=> ~ $less(X3,X0) )
& model_max(X1,X2,X0) ) ),
inference(rectify,[],[f18]) ).
tff(f26,plain,
! [X2: $int,X0: $int,X1: $int] :
( minsol_model_ub(X2,X0,X1)
<=> ( model_ub(X2,X0,X1)
& ! [X3: $int] :
( ~ model_ub(X2,X0,X3)
| ~ $less(X3,X1) ) ) ),
inference(ennf_transformation,[],[f23]) ).
tff(f27,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_max(X1,X2,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_max(X1,X2,X3) ) )
<=> minsol_model_max(X1,X2,X0) ),
inference(ennf_transformation,[],[f25]) ).
tff(f28,plain,
? [X2: $int,X1: $int,X0: $int] :
( minsol_model_ub(X2,X1,X0)
<~> minsol_model_max(X2,X1,X0) ),
inference(ennf_transformation,[],[f24]) ).
tff(f29,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( minsol_model_ub(X2,X0,X1)
| ~ model_ub(X2,X0,X1)
| ? [X3: $int] :
( model_ub(X2,X0,X3)
& $less(X3,X1) ) )
& ( ( model_ub(X2,X0,X1)
& ! [X3: $int] :
( ~ model_ub(X2,X0,X3)
| ~ $less(X3,X1) ) )
| ~ minsol_model_ub(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f26]) ).
tff(f30,plain,
! [X2: $int,X0: $int,X1: $int] :
( ( minsol_model_ub(X2,X0,X1)
| ~ model_ub(X2,X0,X1)
| ? [X3: $int] :
( model_ub(X2,X0,X3)
& $less(X3,X1) ) )
& ( ( model_ub(X2,X0,X1)
& ! [X3: $int] :
( ~ model_ub(X2,X0,X3)
| ~ $less(X3,X1) ) )
| ~ minsol_model_ub(X2,X0,X1) ) ),
inference(flattening,[],[f29]) ).
tff(f31,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ? [X3: $int] :
( model_ub(X0,X1,X3)
& $less(X3,X2) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X4: $int] :
( ~ model_ub(X0,X1,X4)
| ~ $less(X4,X2) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(rectify,[],[f30]) ).
tff(f32,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ( model_ub(X0,X1,sK0(X0,X1,X2))
& $less(sK0(X0,X1,X2),X2) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X4: $int] :
( ~ model_ub(X0,X1,X4)
| ~ $less(X4,X2) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f31]) ).
tff(f33,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( ( ~ $less(X2,X0)
& ~ $less(X2,X1) )
| ~ ub(X1,X0,X2) )
& ( ub(X1,X0,X2)
| $less(X2,X0)
| $less(X2,X1) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f34,plain,
! [X1: $int,X0: $int,X2: $int] :
( ( ( ~ $less(X2,X0)
& ~ $less(X2,X1) )
| ~ ub(X1,X0,X2) )
& ( ub(X1,X0,X2)
| $less(X2,X0)
| $less(X2,X1) ) ),
inference(flattening,[],[f33]) ).
tff(f35,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( ~ $less(X2,X1)
& ~ $less(X2,X0) )
| ~ ub(X0,X1,X2) )
& ( ub(X0,X1,X2)
| $less(X2,X1)
| $less(X2,X0) ) ),
inference(rectify,[],[f34]) ).
tff(f36,plain,
? [X2: $int,X1: $int,X0: $int] :
( ( ~ minsol_model_max(X2,X1,X0)
| ~ minsol_model_ub(X2,X1,X0) )
& ( minsol_model_max(X2,X1,X0)
| minsol_model_ub(X2,X1,X0) ) ),
inference(nnf_transformation,[],[f28]) ).
tff(f37,plain,
? [X0: $int,X1: $int,X2: $int] :
( ( ~ minsol_model_max(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) )
& ( minsol_model_max(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(rectify,[],[f36]) ).
tff(f38,plain,
( ( ~ minsol_model_max(sK1,sK2,sK3)
| ~ minsol_model_ub(sK1,sK2,sK3) )
& ( minsol_model_max(sK1,sK2,sK3)
| minsol_model_ub(sK1,sK2,sK3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f37]) ).
tff(f39,plain,
! [X0: $int,X2: $int,X1: $int] :
( ( model_ub(X2,X0,X1)
| ! [X3: $int] :
( ~ ub(X2,X0,X3)
| $less(X1,$sum(c,summation(X3))) ) )
& ( ? [X3: $int] :
( ub(X2,X0,X3)
& ~ $less(X1,$sum(c,summation(X3))) )
| ~ model_ub(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f40,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_ub(X1,X0,X2)
| ! [X3: $int] :
( ~ ub(X1,X0,X3)
| $less(X2,$sum(c,summation(X3))) ) )
& ( ? [X4: $int] :
( ub(X1,X0,X4)
& ~ $less(X2,$sum(c,summation(X4))) )
| ~ model_ub(X1,X0,X2) ) ),
inference(rectify,[],[f39]) ).
tff(f41,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_ub(X1,X0,X2)
| ! [X3: $int] :
( ~ ub(X1,X0,X3)
| $less(X2,$sum(c,summation(X3))) ) )
& ( ( ub(X1,X0,sK4(X0,X1,X2))
& ~ $less(X2,$sum(c,summation(sK4(X0,X1,X2)))) )
| ~ model_ub(X1,X0,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X4,sK4(X0,X1,X2))],[f40]) ).
tff(f42,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( max(X1,X0) = X0 ) ),
inference(rectify,[],[f17]) ).
tff(f43,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(summation(X1),summation(X0))
| $less(X1,X0) )
& ( ~ $less(X1,X0)
| $less(summation(X1),summation(X0)) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f44,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X1,X2,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_max(X1,X2,X3) ) )
| ~ minsol_model_max(X1,X2,X0) )
& ( minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_max(X1,X2,X3) ) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f45,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X1,X2,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_max(X1,X2,X3) ) )
| ~ minsol_model_max(X1,X2,X0) )
& ( minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0)
| ? [X3: $int] :
( $less(X3,X0)
& model_max(X1,X2,X3) ) ) ),
inference(flattening,[],[f44]) ).
tff(f46,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X1,X2,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_max(X1,X2,X3) ) )
| ~ minsol_model_max(X1,X2,X0) )
& ( minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0)
| ? [X4: $int] :
( $less(X4,X0)
& model_max(X1,X2,X4) ) ) ),
inference(rectify,[],[f45]) ).
tff(f47,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( ( model_max(X1,X2,X0)
& ! [X3: $int] :
( ~ $less(X3,X0)
| ~ model_max(X1,X2,X3) ) )
| ~ minsol_model_max(X1,X2,X0) )
& ( minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0)
| ( $less(sK5(X0,X1,X2),X0)
& model_max(X1,X2,sK5(X0,X1,X2)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X4,sK5(X0,X1,X2))],[f46]) ).
tff(f48,plain,
! [X2: $int,X1: $int,X0: $int] :
( ( model_max(X0,X2,X1)
| $less(X1,$sum(c,summation(max(X0,X2)))) )
& ( ~ $less(X1,$sum(c,summation(max(X0,X2))))
| ~ model_max(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f49,plain,
! [X0: $int,X1: $int,X2: $int] :
( ( model_max(X2,X0,X1)
| $less(X1,$sum(c,summation(max(X2,X0)))) )
& ( ~ $less(X1,$sum(c,summation(max(X2,X0))))
| ~ model_max(X2,X0,X1) ) ),
inference(rectify,[],[f48]) ).
tff(f50,plain,
! [X2: $int,X0: $int,X1: $int,X4: $int] :
( ~ minsol_model_ub(X0,X1,X2)
| ~ $less(X4,X2)
| ~ model_ub(X0,X1,X4) ),
inference(cnf_transformation,[],[f32]) ).
tff(f51,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_ub(X0,X1,X2)
| model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
tff(f52,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK0(X0,X1,X2),X2)
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
tff(f53,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_ub(X0,X1,sK0(X0,X1,X2))
| minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
tff(f54,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X0,X1,X2)
| $less(X2,X0)
| $less(X2,X1) ),
inference(cnf_transformation,[],[f35]) ).
tff(f55,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X0,X1,X2)
| ~ $less(X2,X0) ),
inference(cnf_transformation,[],[f35]) ).
tff(f56,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ ub(X0,X1,X2)
| ~ $less(X2,X1) ),
inference(cnf_transformation,[],[f35]) ).
tff(f57,plain,
( minsol_model_max(sK1,sK2,sK3)
| minsol_model_ub(sK1,sK2,sK3) ),
inference(cnf_transformation,[],[f38]) ).
tff(f58,plain,
( ~ minsol_model_ub(sK1,sK2,sK3)
| ~ minsol_model_max(sK1,sK2,sK3) ),
inference(cnf_transformation,[],[f38]) ).
tff(f59,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X2,$sum(c,summation(sK4(X0,X1,X2))))
| ~ model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f60,plain,
! [X2: $int,X0: $int,X1: $int] :
( ub(X1,X0,sK4(X0,X1,X2))
| ~ model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f61,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( $less(X2,$sum(c,summation(X3)))
| ~ ub(X1,X0,X3)
| model_ub(X1,X0,X2) ),
inference(cnf_transformation,[],[f41]) ).
tff(f62,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X0 )
| $less(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tff(f63,plain,
! [X0: $int,X1: $int] :
( $less(summation(X1),summation(X0))
| ~ $less(X1,X0) ),
inference(cnf_transformation,[],[f43]) ).
tff(f64,plain,
! [X0: $int,X1: $int] :
( ~ $less(summation(X1),summation(X0))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f43]) ).
tff(f65,plain,
! [X2: $int,X0: $int,X1: $int] :
( model_max(X1,X2,sK5(X0,X1,X2))
| minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f66,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(sK5(X0,X1,X2),X0)
| ~ model_max(X1,X2,X0)
| minsol_model_max(X1,X2,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f67,plain,
! [X2: $int,X3: $int,X0: $int,X1: $int] :
( ~ minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X3)
| ~ $less(X3,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f68,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ minsol_model_max(X1,X2,X0)
| model_max(X1,X2,X0) ),
inference(cnf_transformation,[],[f47]) ).
tff(f69,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| $less(X1,X0) ),
inference(cnf_transformation,[],[f19]) ).
tff(f70,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X1,$sum(c,summation(max(X2,X0))))
| ~ model_max(X2,X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tff(f71,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X1,$sum(c,summation(max(X2,X0))))
| model_max(X2,X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tff(f73,definition,
( spl6_1
<=> minsol_model_max(sK1,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
tff(f74,plain,
( ~ minsol_model_max(sK1,sK2,sK3)
| spl6_1 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f75,plain,
( minsol_model_max(sK1,sK2,sK3)
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f77,definition,
( spl6_2
<=> minsol_model_ub(sK1,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
tff(f78,plain,
( ~ minsol_model_ub(sK1,sK2,sK3)
| spl6_2 ),
inference(avatar_component_clause,[],[f77]) ).
tff(f79,plain,
( minsol_model_ub(sK1,sK2,sK3)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f77]) ).
tff(f80,plain,
( spl6_1
| spl6_2 ),
inference(avatar_split_clause,[],[f57,f77,f73]) ).
tff(f81,plain,
( ~ spl6_2
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f58,f73,f77]) ).
tff(f83,plain,
( model_max(sK1,sK2,sK3)
| ~ spl6_1 ),
inference(resolution,[],[f68,f75]) ).
tff(f85,definition,
( spl6_3
<=> model_max(sK1,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
tff(f87,plain,
( model_max(sK1,sK2,sK3)
| ~ spl6_3 ),
inference(avatar_component_clause,[],[f85]) ).
tff(f88,plain,
( spl6_3
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f83,f73,f85]) ).
tff(f148,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK4(X1,X0,X2),X1)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f60,f56]) ).
tff(f149,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK4(X1,X0,X2),X0)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[],[f60,f55]) ).
tff(f150,plain,
( ~ $less(sK3,$sum(c,summation(max(sK1,sK2))))
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f70,f87]) ).
tff(f156,definition,
( spl6_9
<=> $less(sK3,$sum(c,summation(max(sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
tff(f157,plain,
( $less(sK3,$sum(c,summation(max(sK1,sK2))))
| ~ spl6_9 ),
inference(avatar_component_clause,[],[f156]) ).
tff(f158,plain,
( ~ $less(sK3,$sum(c,summation(max(sK1,sK2))))
| spl6_9 ),
inference(avatar_component_clause,[],[f156]) ).
tff(f159,plain,
( ~ spl6_9
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f150,f85,f156]) ).
tff(f161,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X1,$sum(c,summation(X0)))
| model_max(X0,X2,X1)
| $less(X0,X2) ),
inference(superposition,[],[f71,f69]) ).
tff(f162,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X1,$sum(c,summation(X0)))
| model_max(X2,X0,X1)
| $less(X0,X2) ),
inference(superposition,[],[f71,f62]) ).
tff(f169,plain,
( model_max(sK1,sK2,sK3)
| spl6_9 ),
inference(resolution,[],[f158,f71]) ).
tff(f170,plain,
( $less(sK1,sK2)
| ~ $less(sK3,$sum(c,summation(sK1)))
| spl6_9 ),
inference(superposition,[],[f158,f69]) ).
tff(f171,plain,
( ~ $less(sK3,$sum(c,summation(sK2)))
| $less(sK2,sK1)
| spl6_9 ),
inference(superposition,[],[f158,f62]) ).
tff(f173,definition,
( spl6_10
<=> $less(sK3,$sum(c,summation(sK2))) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
tff(f177,definition,
( spl6_11
<=> $less(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition]) ).
tff(f178,plain,
( ~ $less(sK2,sK1)
| spl6_11 ),
inference(avatar_component_clause,[],[f177]) ).
tff(f180,plain,
( ~ spl6_10
| spl6_11
| spl6_9 ),
inference(avatar_split_clause,[],[f171,f156,f177,f173]) ).
tff(f197,definition,
( spl6_15
<=> $less(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition]) ).
tff(f198,plain,
( ~ $less(sK1,sK2)
| spl6_15 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f199,plain,
( $less(sK1,sK2)
| ~ spl6_15 ),
inference(avatar_component_clause,[],[f197]) ).
tff(f201,definition,
( spl6_16
<=> $less(sK3,$sum(c,summation(sK1))) ),
introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition]) ).
tff(f203,plain,
( ~ $less(sK3,$sum(c,summation(sK1)))
| spl6_16 ),
inference(avatar_component_clause,[],[f201]) ).
tff(f204,plain,
( spl6_15
| ~ spl6_16
| spl6_9 ),
inference(avatar_split_clause,[],[f170,f156,f201,f197]) ).
tff(f210,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,[],[f61,f70]) ).
tff(f278,plain,
( model_ub(sK1,sK2,sK3)
| ~ spl6_2 ),
inference(resolution,[],[f79,f51]) ).
tff(f280,definition,
( spl6_26
<=> model_ub(sK1,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_26])],[avatar_definition]) ).
tff(f281,plain,
( ~ model_ub(sK1,sK2,sK3)
| spl6_26 ),
inference(avatar_component_clause,[],[f280]) ).
tff(f282,plain,
( model_ub(sK1,sK2,sK3)
| ~ spl6_26 ),
inference(avatar_component_clause,[],[f280]) ).
tff(f283,plain,
( spl6_26
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f278,f77,f280]) ).
tff(f290,plain,
( ( max(sK1,sK2) = sK2 )
| spl6_11 ),
inference(unit_resulting_resolution,[],[f62,f178]) ).
tff(f292,definition,
( spl6_27
<=> ( max(sK1,sK2) = sK2 ) ),
introduced(definition,[new_symbols(definition,[spl6_27])],[avatar_definition]) ).
tff(f295,plain,
( spl6_27
| spl6_11 ),
inference(avatar_split_clause,[],[f290,f177,f292]) ).
tff(f307,plain,
( ~ $less(sK3,$sum(c,summation(sK4(sK2,sK1,sK3))))
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f59,f282]) ).
tff(f308,plain,
( ub(sK1,sK2,sK4(sK2,sK1,sK3))
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f60,f282]) ).
tff(f311,definition,
( spl6_30
<=> ub(sK1,sK2,sK4(sK2,sK1,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_30])],[avatar_definition]) ).
tff(f313,plain,
( ub(sK1,sK2,sK4(sK2,sK1,sK3))
| ~ spl6_30 ),
inference(avatar_component_clause,[],[f311]) ).
tff(f314,plain,
( spl6_30
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f308,f280,f311]) ).
tff(f317,definition,
( spl6_31
<=> $less(sK3,$sum(c,summation(sK4(sK2,sK1,sK3)))) ),
introduced(definition,[new_symbols(definition,[spl6_31])],[avatar_definition]) ).
tff(f320,plain,
( ~ spl6_31
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f307,f280,f317]) ).
tff(f328,plain,
( ~ $less(sK4(sK2,sK1,sK3),sK2)
| ~ spl6_30 ),
inference(unit_resulting_resolution,[],[f56,f313]) ).
tff(f329,plain,
( ~ $less(sK4(sK2,sK1,sK3),sK1)
| ~ spl6_30 ),
inference(unit_resulting_resolution,[],[f55,f313]) ).
tff(f333,definition,
( spl6_32
<=> $less(sK4(sK2,sK1,sK3),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_32])],[avatar_definition]) ).
tff(f335,plain,
( ~ $less(sK4(sK2,sK1,sK3),sK2)
| spl6_32 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f336,plain,
( ~ spl6_32
| ~ spl6_30 ),
inference(avatar_split_clause,[],[f328,f311,f333]) ).
tff(f338,definition,
( spl6_33
<=> $less(sK4(sK2,sK1,sK3),sK1) ),
introduced(definition,[new_symbols(definition,[spl6_33])],[avatar_definition]) ).
tff(f340,plain,
( ~ $less(sK4(sK2,sK1,sK3),sK1)
| spl6_33 ),
inference(avatar_component_clause,[],[f338]) ).
tff(f341,plain,
( ~ spl6_33
| ~ spl6_30 ),
inference(avatar_split_clause,[],[f329,f311,f338]) ).
tff(f348,plain,
( $less(sK1,sK2)
| $less(sK3,$sum(c,summation(sK1)))
| ~ spl6_9 ),
inference(superposition,[],[f157,f69]) ).
tff(f356,plain,
( spl6_15
| spl6_16
| ~ spl6_9 ),
inference(avatar_split_clause,[],[f348,f156,f201,f197]) ).
tff(f505,plain,
( ~ $less(summation(sK4(sK2,sK1,sK3)),summation(sK2))
| spl6_32 ),
inference(unit_resulting_resolution,[],[f64,f335]) ).
tff(f531,definition,
( spl6_49
<=> $less(summation(sK4(sK2,sK1,sK3)),summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_49])],[avatar_definition]) ).
tff(f534,plain,
( ~ spl6_49
| spl6_32 ),
inference(avatar_split_clause,[],[f505,f333,f531]) ).
tff(f549,plain,
( spl6_3
| spl6_9 ),
inference(avatar_split_clause,[],[f169,f156,f85]) ).
tff(f556,plain,
( ~ ub(sK1,sK2,max(sK1,sK2))
| ~ spl6_3
| spl6_26 ),
inference(unit_resulting_resolution,[],[f210,f87,f281]) ).
tff(f559,definition,
( spl6_53
<=> ub(sK1,sK2,max(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_53])],[avatar_definition]) ).
tff(f560,plain,
( ub(sK1,sK2,max(sK1,sK2))
| ~ spl6_53 ),
inference(avatar_component_clause,[],[f559]) ).
tff(f561,plain,
( ~ ub(sK1,sK2,max(sK1,sK2))
| spl6_53 ),
inference(avatar_component_clause,[],[f559]) ).
tff(f562,plain,
( ~ spl6_53
| ~ spl6_3
| spl6_26 ),
inference(avatar_split_clause,[],[f556,f280,f85,f559]) ).
tff(f632,plain,
( ~ ub(sK1,sK2,sK1)
| spl6_16
| spl6_26 ),
inference(unit_resulting_resolution,[],[f61,f281,f203]) ).
tff(f686,definition,
( spl6_67
<=> ub(sK1,sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_67])],[avatar_definition]) ).
tff(f688,plain,
( ~ ub(sK1,sK2,sK1)
| spl6_67 ),
inference(avatar_component_clause,[],[f686]) ).
tff(f689,plain,
( ~ spl6_67
| spl6_16
| spl6_26 ),
inference(avatar_split_clause,[],[f632,f280,f201,f686]) ).
tff(f701,plain,
( ~ $less(summation(sK4(sK2,sK1,sK3)),summation(sK1))
| spl6_33 ),
inference(unit_resulting_resolution,[],[f64,f340]) ).
tff(f727,definition,
( spl6_73
<=> $less(summation(sK4(sK2,sK1,sK3)),summation(sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_73])],[avatar_definition]) ).
tff(f730,plain,
( ~ spl6_73
| spl6_33 ),
inference(avatar_split_clause,[],[f701,f338,f727]) ).
tff(f755,plain,
( $less(sK1,sK1)
| $less(sK1,sK2)
| spl6_67 ),
inference(resolution,[],[f688,f54]) ).
tff(f757,definition,
( spl6_78
<=> $less(sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl6_78])],[avatar_definition]) ).
tff(f760,plain,
( spl6_15
| spl6_78
| spl6_67 ),
inference(avatar_split_clause,[],[f755,f686,f757,f197]) ).
tff(f787,plain,
( $less(summation(sK1),summation(sK2))
| ~ spl6_15 ),
inference(unit_resulting_resolution,[],[f63,f199]) ).
tff(f791,definition,
( spl6_81
<=> $less(summation(sK1),summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_81])],[avatar_definition]) ).
tff(f794,plain,
( spl6_81
| ~ spl6_15 ),
inference(avatar_split_clause,[],[f787,f197,f791]) ).
tff(f815,plain,
( $less(max(sK1,sK2),sK1)
| $less(max(sK1,sK2),sK2)
| spl6_53 ),
inference(resolution,[],[f561,f54]) ).
tff(f819,definition,
( spl6_83
<=> $less(max(sK1,sK2),sK1) ),
introduced(definition,[new_symbols(definition,[spl6_83])],[avatar_definition]) ).
tff(f823,definition,
( spl6_84
<=> $less(max(sK1,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_84])],[avatar_definition]) ).
tff(f826,plain,
( spl6_83
| spl6_84
| spl6_53 ),
inference(avatar_split_clause,[],[f815,f559,f823,f819]) ).
tff(f852,plain,
( model_max(sK1,sK2,sK5(sK3,sK1,sK2))
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f65,f87,f74]) ).
tff(f853,plain,
( $less(sK5(sK3,sK1,sK2),sK3)
| spl6_1
| ~ spl6_3 ),
inference(unit_resulting_resolution,[],[f66,f87,f74]) ).
tff(f855,definition,
( spl6_89
<=> model_max(sK1,sK2,sK5(sK3,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_89])],[avatar_definition]) ).
tff(f857,plain,
( model_max(sK1,sK2,sK5(sK3,sK1,sK2))
| ~ spl6_89 ),
inference(avatar_component_clause,[],[f855]) ).
tff(f858,plain,
( spl6_89
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f852,f85,f73,f855]) ).
tff(f860,definition,
( spl6_90
<=> $less(sK5(sK3,sK1,sK2),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_90])],[avatar_definition]) ).
tff(f862,plain,
( $less(sK5(sK3,sK1,sK2),sK3)
| ~ spl6_90 ),
inference(avatar_component_clause,[],[f860]) ).
tff(f863,plain,
( spl6_90
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f853,f85,f73,f860]) ).
tff(f866,plain,
( ! [X0: $int] :
( ~ model_ub(sK1,sK2,X0)
| ~ $less(X0,sK3) )
| ~ spl6_2 ),
inference(resolution,[],[f79,f50]) ).
tff(f878,plain,
( ~ model_ub(sK1,sK2,sK5(sK3,sK1,sK2))
| ~ spl6_2
| ~ spl6_90 ),
inference(unit_resulting_resolution,[],[f866,f862]) ).
tff(f884,definition,
( spl6_91
<=> model_ub(sK1,sK2,sK5(sK3,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_91])],[avatar_definition]) ).
tff(f887,plain,
( ~ spl6_91
| ~ spl6_2
| ~ spl6_90 ),
inference(avatar_split_clause,[],[f878,f860,f77,f884]) ).
tff(f964,plain,
( ( sK1 = max(sK1,sK2) )
| spl6_15 ),
inference(unit_resulting_resolution,[],[f69,f198]) ).
tff(f990,plain,
( model_ub(sK1,sK2,sK5(sK3,sK1,sK2))
| ~ spl6_53
| ~ spl6_89 ),
inference(unit_resulting_resolution,[],[f210,f857,f560]) ).
tff(f1001,plain,
( spl6_91
| ~ spl6_53
| ~ spl6_89 ),
inference(avatar_split_clause,[],[f990,f855,f559,f884]) ).
tff(f1008,plain,
( model_ub(sK1,sK2,sK0(sK1,sK2,sK3))
| spl6_2
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f53,f282,f78]) ).
tff(f1009,plain,
( $less(sK0(sK1,sK2,sK3),sK3)
| spl6_2
| ~ spl6_26 ),
inference(unit_resulting_resolution,[],[f52,f282,f78]) ).
tff(f1011,definition,
( spl6_103
<=> $less(sK0(sK1,sK2,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_103])],[avatar_definition]) ).
tff(f1013,plain,
( $less(sK0(sK1,sK2,sK3),sK3)
| ~ spl6_103 ),
inference(avatar_component_clause,[],[f1011]) ).
tff(f1014,plain,
( spl6_103
| spl6_2
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f1009,f280,f77,f1011]) ).
tff(f1016,definition,
( spl6_104
<=> model_ub(sK1,sK2,sK0(sK1,sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_104])],[avatar_definition]) ).
tff(f1018,plain,
( model_ub(sK1,sK2,sK0(sK1,sK2,sK3))
| ~ spl6_104 ),
inference(avatar_component_clause,[],[f1016]) ).
tff(f1019,plain,
( spl6_104
| spl6_2
| ~ spl6_26 ),
inference(avatar_split_clause,[],[f1008,f280,f77,f1016]) ).
tff(f1100,plain,
( ~ model_max(sK1,sK2,sK0(sK1,sK2,sK3))
| ~ spl6_1
| ~ spl6_103 ),
inference(unit_resulting_resolution,[],[f67,f75,f1013]) ).
tff(f1108,definition,
( spl6_117
<=> model_max(sK1,sK2,sK0(sK1,sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_117])],[avatar_definition]) ).
tff(f1110,plain,
( ~ model_max(sK1,sK2,sK0(sK1,sK2,sK3))
| spl6_117 ),
inference(avatar_component_clause,[],[f1108]) ).
tff(f1111,plain,
( ~ spl6_117
| ~ spl6_1
| ~ spl6_103 ),
inference(avatar_split_clause,[],[f1100,f1011,f73,f1108]) ).
tff(f1138,plain,
( ~ $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3)))))
| ~ spl6_104 ),
inference(unit_resulting_resolution,[],[f59,f1018]) ).
tff(f1140,plain,
( ~ $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK2)
| ~ spl6_104 ),
inference(unit_resulting_resolution,[],[f148,f1018]) ).
tff(f1141,plain,
( ~ $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK1)
| ~ spl6_104 ),
inference(unit_resulting_resolution,[],[f149,f1018]) ).
tff(f1149,definition,
( spl6_122
<=> $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK2) ),
introduced(definition,[new_symbols(definition,[spl6_122])],[avatar_definition]) ).
tff(f1151,plain,
( ~ $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK2)
| spl6_122 ),
inference(avatar_component_clause,[],[f1149]) ).
tff(f1152,plain,
( ~ spl6_122
| ~ spl6_104 ),
inference(avatar_split_clause,[],[f1140,f1016,f1149]) ).
tff(f1159,definition,
( spl6_124
<=> $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK1) ),
introduced(definition,[new_symbols(definition,[spl6_124])],[avatar_definition]) ).
tff(f1161,plain,
( ~ $less(sK4(sK2,sK1,sK0(sK1,sK2,sK3)),sK1)
| spl6_124 ),
inference(avatar_component_clause,[],[f1159]) ).
tff(f1162,plain,
( ~ spl6_124
| ~ spl6_104 ),
inference(avatar_split_clause,[],[f1141,f1016,f1159]) ).
tff(f1164,definition,
( spl6_125
<=> $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3))))) ),
introduced(definition,[new_symbols(definition,[spl6_125])],[avatar_definition]) ).
tff(f1167,plain,
( ~ spl6_125
| ~ spl6_104 ),
inference(avatar_split_clause,[],[f1138,f1016,f1164]) ).
tff(f1206,plain,
( $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK2)))
| spl6_11
| spl6_117 ),
inference(unit_resulting_resolution,[],[f162,f178,f1110]) ).
tff(f1207,plain,
( $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK1)))
| spl6_15
| spl6_117 ),
inference(unit_resulting_resolution,[],[f161,f198,f1110]) ).
tff(f1222,definition,
( spl6_131
<=> $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK1))) ),
introduced(definition,[new_symbols(definition,[spl6_131])],[avatar_definition]) ).
tff(f1225,plain,
( spl6_131
| spl6_15
| spl6_117 ),
inference(avatar_split_clause,[],[f1207,f1108,f197,f1222]) ).
tff(f1227,definition,
( spl6_132
<=> $less(sK0(sK1,sK2,sK3),$sum(c,summation(sK2))) ),
introduced(definition,[new_symbols(definition,[spl6_132])],[avatar_definition]) ).
tff(f1230,plain,
( spl6_132
| spl6_11
| spl6_117 ),
inference(avatar_split_clause,[],[f1206,f1108,f177,f1227]) ).
tff(f1374,plain,
( ~ $less(summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3))),summation(sK2))
| spl6_122 ),
inference(unit_resulting_resolution,[],[f64,f1151]) ).
tff(f1391,definition,
( spl6_151
<=> $less(summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3))),summation(sK2)) ),
introduced(definition,[new_symbols(definition,[spl6_151])],[avatar_definition]) ).
tff(f1394,plain,
( ~ spl6_151
| spl6_122 ),
inference(avatar_split_clause,[],[f1374,f1149,f1391]) ).
tff(f1442,definition,
( spl6_160
<=> ( sK1 = max(sK1,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl6_160])],[avatar_definition]) ).
tff(f1445,plain,
( spl6_160
| spl6_15 ),
inference(avatar_split_clause,[],[f964,f197,f1442]) ).
tff(f1502,plain,
( ~ $less(summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3))),summation(sK1))
| spl6_124 ),
inference(unit_resulting_resolution,[],[f64,f1161]) ).
tff(f1506,definition,
( spl6_161
<=> $less(summation(sK4(sK2,sK1,sK0(sK1,sK2,sK3))),summation(sK1)) ),
introduced(definition,[new_symbols(definition,[spl6_161])],[avatar_definition]) ).
tff(f1509,plain,
( ~ spl6_161
| spl6_124 ),
inference(avatar_split_clause,[],[f1502,f1159,f1506]) ).
tff(f1539,plain,
$false,
inference(avatar_smt_refutation,[],[f1509,f1445,f1394,f1230,f1225,f1167,f1162,f1152,f1111,f1019,f1014,f1001,f887,f863,f858,f826,f794,f760,f730,f689,f562,f549,f534,f356,f341,f336,f320,f314,f295,f283,f204,f180,f159,f88,f81,f80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM862_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.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 21:36:50 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 2.83/1.37 % (1188544)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.83/1.37 % (1188551)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2163572741:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.83/1.37 % (1188549)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1463736305:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.83/1.37 % (1188550)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2084937593:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.83/1.37 % (1188555)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2064469065:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.83/1.37 % (1188553)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3162795899:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.83/1.37 % (1188552)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3125103057:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.83/1.37 % (1188554)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3548554868:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.83/1.37 % (1188553)Instruction limit reached!
% 2.83/1.37 % (1188553)------------------------------
% 2.83/1.37 % (1188553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.37 % (1188553)CaDiCaL version: 2.1.3
% 2.83/1.37 % (1188553)Termination reason: Instruction limit
% 2.83/1.37 % (1188553)Termination phase: Saturation
% 2.83/1.37 % (1188553)Time elapsed: 0.004 s
% 2.83/1.37 % (1188553)Peak memory usage: 89 MB
% 2.83/1.37 % (1188553)Instructions burned: 5 (million)
% 2.83/1.37 % (1188552)Instruction limit reached!
% 2.83/1.37 % (1188552)------------------------------
% 2.83/1.37 % (1188552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.37 % (1188552)CaDiCaL version: 2.1.3
% 2.83/1.37 % (1188552)Termination reason: Instruction limit
% 2.83/1.37 % (1188552)Termination phase: Saturation
% 2.83/1.37 % (1188552)Time elapsed: 0.006 s
% 2.83/1.37 % (1188552)Peak memory usage: 88 MB
% 2.83/1.37 % (1188552)Instructions burned: 8 (million)
% 2.83/1.37 % (1188549)Instruction limit reached!
% 2.83/1.37 % (1188549)------------------------------
% 2.83/1.37 % (1188549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.37 % (1188549)CaDiCaL version: 2.1.3
% 2.83/1.37 % (1188549)Termination reason: Instruction limit
% 2.83/1.37 % (1188549)Termination phase: Saturation
% 2.83/1.37 % (1188549)Time elapsed: 0.031 s
% 2.83/1.37 % (1188549)Peak memory usage: 115 MB
% 2.83/1.37 % (1188549)Instructions burned: 12 (million)
% 2.83/1.37 % (1188555)Instruction limit reached!
% 2.83/1.37 % (1188555)------------------------------
% 2.83/1.37 % (1188555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.37 % (1188555)CaDiCaL version: 2.1.3
% 2.83/1.37 % (1188555)Termination reason: Instruction limit
% 2.83/1.37 % (1188555)Termination phase: Saturation
% 2.83/1.37 % (1188555)Time elapsed: 0.047 s
% 2.83/1.37 % (1188555)Peak memory usage: 115 MB
% 2.83/1.37 % (1188555)Instructions burned: 34 (million)
% 2.83/1.37 % (1188551)Instruction limit reached!
% 2.83/1.37 % (1188551)------------------------------
% 2.83/1.37 % (1188551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.37 % (1188551)CaDiCaL version: 2.1.3
% 2.83/1.37 % (1188551)Termination reason: Instruction limit
% 2.83/1.37 % (1188551)Termination phase: Saturation
% 2.83/1.37 % (1188551)Time elapsed: 0.088 s
% 2.83/1.37 % (1188551)Peak memory usage: 117 MB
% 2.83/1.37 % (1188551)Instructions burned: 202 (million)
% 2.83/1.37 % (1188554)Instruction limit reached!
% 2.83/1.37 % (1188554)------------------------------
% 2.83/1.37 % (1188554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.37 % (1188554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188554)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188554)Termination reason: Instruction limit
% 4.20/1.52 % (1188554)Termination phase: Saturation
% 4.20/1.52 % (1188554)Time elapsed: 0.057 s
% 4.20/1.52 % (1188554)Peak memory usage: 116 MB
% 4.20/1.52 % (1188554)Instructions burned: 46 (million)
% 4.20/1.52 % (1188563)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1593117878:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.20/1.52 % (1188563)Instruction limit reached!
% 4.20/1.52 % (1188563)------------------------------
% 4.20/1.52 % (1188563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.52 % (1188563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188563)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188563)Termination reason: Instruction limit
% 4.20/1.52 % (1188563)Termination phase: Saturation
% 4.20/1.52 % (1188563)Time elapsed: 0.011 s
% 4.20/1.52 % (1188563)Peak memory usage: 88 MB
% 4.20/1.52 % (1188563)Instructions burned: 14 (million)
% 4.20/1.52 % (1188564)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=2826764098:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.20/1.52 % (1188565)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1013928387:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.20/1.52 % (1188567)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=2554353812:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.20/1.52 % (1188567)Refutation not found, incomplete strategy
% 4.20/1.52 % (1188567)------------------------------
% 4.20/1.52 % (1188567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.52 % (1188567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188567)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188567)Termination reason: Refutation not found, incomplete strategy
% 4.20/1.52 % (1188567)Time elapsed: 0.001 s
% 4.20/1.52 % (1188567)Peak memory usage: 89 MB
% 4.20/1.52 % (1188567)Instructions burned: 2 (million)
% 4.20/1.52 % (1188565)Instruction limit reached!
% 4.20/1.52 % (1188565)------------------------------
% 4.20/1.52 % (1188565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.52 % (1188565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188565)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188565)Termination reason: Instruction limit
% 4.20/1.52 % (1188565)Termination phase: Saturation
% 4.20/1.52 % (1188565)Time elapsed: 0.010 s
% 4.20/1.52 % (1188565)Peak memory usage: 90 MB
% 4.20/1.52 % (1188565)Instructions burned: 17 (million)
% 4.20/1.52 % (1188564)Instruction limit reached!
% 4.20/1.52 % (1188564)------------------------------
% 4.20/1.52 % (1188564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.52 % (1188564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188564)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188564)Termination reason: Instruction limit
% 4.20/1.52 % (1188564)Termination phase: Saturation
% 4.20/1.52 % (1188564)Time elapsed: 0.023 s
% 4.20/1.52 % (1188564)Peak memory usage: 89 MB
% 4.20/1.52 % (1188564)Instructions burned: 29 (million)
% 4.20/1.52 % (1188566)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2493710168:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 4.20/1.52 % (1188568)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4115250390:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.20/1.52 % (1188566)Instruction limit reached!
% 4.20/1.52 % (1188566)------------------------------
% 4.20/1.52 % (1188566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.52 % (1188566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.52 % (1188566)CaDiCaL version: 2.1.3
% 4.20/1.52 % (1188566)Termination reason: Instruction limit
% 4.20/1.52 % (1188566)Termination phase: Saturation
% 4.20/1.52 % (1188566)Time elapsed: 0.018 s
% 4.20/1.52 % (1188566)Peak memory usage: 89 MB
% 4.20/1.52 % (1188566)Instructions burned: 25 (million)
% 4.20/1.52 % (1188550)Instruction limit reached!
% 4.20/1.52 % (1188550)------------------------------
% 4.20/1.52 % (1188550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188550)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188550)Termination reason: Instruction limit
% 5.19/1.68 % (1188550)Termination phase: Saturation
% 5.19/1.68 % (1188550)Time elapsed: 0.214 s
% 5.19/1.68 % (1188550)Peak memory usage: 117 MB
% 5.19/1.68 % (1188550)Instructions burned: 307 (million)
% 5.19/1.68 % (1188568)Instruction limit reached!
% 5.19/1.68 % (1188568)------------------------------
% 5.19/1.68 % (1188568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188568)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188568)Termination reason: Instruction limit
% 5.19/1.68 % (1188568)Termination phase: Saturation
% 5.19/1.68 % (1188568)Time elapsed: 0.051 s
% 5.19/1.68 % (1188568)Peak memory usage: 89 MB
% 5.19/1.68 % (1188568)Instructions burned: 86 (million)
% 5.19/1.68 % (1188571)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1770924212:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.19/1.68 % (1188571)Instruction limit reached!
% 5.19/1.68 % (1188571)------------------------------
% 5.19/1.68 % (1188571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188571)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188571)Termination reason: Instruction limit
% 5.19/1.68 % (1188571)Termination phase: Saturation
% 5.19/1.68 % (1188571)Time elapsed: 0.003 s
% 5.19/1.68 % (1188571)Peak memory usage: 89 MB
% 5.19/1.68 % (1188571)Instructions burned: 3 (million)
% 5.19/1.68 % (1188574)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3529473543:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.19/1.68 % (1188575)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=31245785:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.19/1.68 % (1188575)Instruction limit reached!
% 5.19/1.68 % (1188575)------------------------------
% 5.19/1.68 % (1188575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188575)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188575)Termination reason: Instruction limit
% 5.19/1.68 % (1188575)Termination phase: Saturation
% 5.19/1.68 % (1188575)Time elapsed: 0.004 s
% 5.19/1.68 % (1188575)Peak memory usage: 88 MB
% 5.19/1.68 % (1188575)Instructions burned: 4 (million)
% 5.19/1.68 % (1188567)------------------------------
% 5.19/1.68 % (1188567)------------------------------
% 5.19/1.68 % (1188578)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=312588387:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.19/1.68 % (1188574)Refutation not found, incomplete strategy
% 5.19/1.68 % (1188574)------------------------------
% 5.19/1.68 % (1188574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188574)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188574)Termination reason: Refutation not found, incomplete strategy
% 5.19/1.68 % (1188574)Time elapsed: 0.037 s
% 5.19/1.68 % (1188574)Peak memory usage: 90 MB
% 5.19/1.68 % (1188574)Instructions burned: 59 (million)
% 5.19/1.68 % (1188579)lrs+10_1_thi=all:si=on:fd=off:random_seed=168467382:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.19/1.68 % (1188580)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=1959274795:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.19/1.68 % (1188580)Instruction limit reached!
% 5.19/1.68 % (1188580)------------------------------
% 5.19/1.68 % (1188580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.19/1.68 % (1188580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.19/1.68 % (1188580)CaDiCaL version: 2.1.3
% 5.19/1.68 % (1188580)Termination reason: Instruction limit
% 5.19/1.68 % (1188580)Termination phase: Saturation
% 5.19/1.68 % (1188580)Time elapsed: 0.006 s
% 5.19/1.68 % (1188580)Peak memory usage: 88 MB
% 6.97/1.91 % (1188580)Instructions burned: 8 (million)
% 6.97/1.91 % (1188583)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1376481036:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 6.97/1.91 % (1188583)Instruction limit reached!
% 6.97/1.91 % (1188583)------------------------------
% 6.97/1.91 % (1188583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188583)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188583)Termination reason: Instruction limit
% 6.97/1.91 % (1188583)Termination phase: Saturation
% 6.97/1.91 % (1188583)Time elapsed: 0.002 s
% 6.97/1.91 % (1188583)Peak memory usage: 88 MB
% 6.97/1.91 % (1188583)Instructions burned: 2 (million)
% 6.97/1.91 % (1188588)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1806090207:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.97/1.91 % (1188579)Instruction limit reached!
% 6.97/1.91 % (1188579)------------------------------
% 6.97/1.91 % (1188579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188579)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188579)Termination reason: Instruction limit
% 6.97/1.91 % (1188579)Termination phase: Saturation
% 6.97/1.91 % (1188579)Time elapsed: 0.063 s
% 6.97/1.91 % (1188579)Peak memory usage: 116 MB
% 6.97/1.91 % (1188579)Instructions burned: 54 (million)
% 6.97/1.91 % (1188578)Instruction limit reached!
% 6.97/1.91 % (1188578)------------------------------
% 6.97/1.91 % (1188578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188578)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188578)Termination reason: Instruction limit
% 6.97/1.91 % (1188578)Termination phase: Saturation
% 6.97/1.91 % (1188578)Time elapsed: 0.093 s
% 6.97/1.91 % (1188578)Peak memory usage: 134 MB
% 6.97/1.91 % (1188578)Instructions burned: 67 (million)
% 6.97/1.91 % (1188586)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=701001613:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.97/1.91 % (1188586)Instruction limit reached!
% 6.97/1.91 % (1188586)------------------------------
% 6.97/1.91 % (1188586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188586)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188586)Termination reason: Instruction limit
% 6.97/1.91 % (1188586)Termination phase: Saturation
% 6.97/1.91 % (1188586)Time elapsed: 0.003 s
% 6.97/1.91 % (1188586)Peak memory usage: 89 MB
% 6.97/1.91 % (1188586)Instructions burned: 3 (million)
% 6.97/1.91 % (1188588)Instruction limit reached!
% 6.97/1.91 % (1188588)------------------------------
% 6.97/1.91 % (1188588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188588)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188588)Termination reason: Instruction limit
% 6.97/1.91 % (1188588)Termination phase: Saturation
% 6.97/1.91 % (1188588)Time elapsed: 0.065 s
% 6.97/1.91 % (1188588)Peak memory usage: 117 MB
% 6.97/1.91 % (1188588)Instructions burned: 129 (million)
% 6.97/1.91 % (1188591)dis+10_1_si=on:random_seed=2201293103:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.97/1.91 % (1188591)Instruction limit reached!
% 6.97/1.91 % (1188591)------------------------------
% 6.97/1.91 % (1188591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.97/1.91 % (1188591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.97/1.91 % (1188591)CaDiCaL version: 2.1.3
% 6.97/1.91 % (1188591)Termination reason: Instruction limit
% 6.97/1.91 % (1188591)Termination phase: Saturation
% 6.97/1.91 % (1188591)Time elapsed: 0.008 s
% 6.97/1.91 % (1188591)Peak memory usage: 88 MB
% 6.97/1.91 % (1188591)Instructions burned: 10 (million)
% 6.97/1.91 % (1188594)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1248098686:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.97/1.91 % (1188595)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=661918097: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)
% 8.65/2.11 % (1188594)Refutation not found, incomplete strategy
% 8.65/2.11 % (1188594)------------------------------
% 8.65/2.11 % (1188594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188594)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188594)Termination reason: Refutation not found, incomplete strategy
% 8.65/2.11 % (1188594)Time elapsed: 0.002 s
% 8.65/2.11 % (1188594)Peak memory usage: 88 MB
% 8.65/2.11 % (1188594)Instructions burned: 2 (million)
% 8.65/2.11 % (1188596)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1461433611:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.65/2.11 % (1188596)Instruction limit reached!
% 8.65/2.11 % (1188596)------------------------------
% 8.65/2.11 % (1188596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188596)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188596)Termination reason: Instruction limit
% 8.65/2.11 % (1188596)Termination phase: Saturation
% 8.65/2.11 % (1188596)Time elapsed: 0.003 s
% 8.65/2.11 % (1188596)Peak memory usage: 89 MB
% 8.65/2.11 % (1188596)Instructions burned: 3 (million)
% 8.65/2.11 % (1188595)Instruction limit reached!
% 8.65/2.11 % (1188595)------------------------------
% 8.65/2.11 % (1188595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188595)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188595)Termination reason: Instruction limit
% 8.65/2.11 % (1188595)Termination phase: Saturation
% 8.65/2.11 % (1188595)Time elapsed: 0.030 s
% 8.65/2.11 % (1188595)Peak memory usage: 89 MB
% 8.65/2.11 % (1188595)Instructions burned: 36 (million)
% 8.65/2.11 % (1188599)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1222688643:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.65/2.11 % (1188574)------------------------------
% 8.65/2.11 % (1188574)------------------------------
% 8.65/2.11 % (1188598)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3086161009:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 8.65/2.11 % (1188598)Instruction limit reached!
% 8.65/2.11 % (1188598)------------------------------
% 8.65/2.11 % (1188598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188598)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188598)Termination reason: Instruction limit
% 8.65/2.11 % (1188598)Termination phase: Saturation
% 8.65/2.11 % (1188598)Time elapsed: 0.007 s
% 8.65/2.11 % (1188598)Peak memory usage: 88 MB
% 8.65/2.11 % (1188598)Instructions burned: 8 (million)
% 8.65/2.11 % (1188601)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2332559844:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 8.65/2.11 % (1188601)Instruction limit reached!
% 8.65/2.11 % (1188601)------------------------------
% 8.65/2.11 % (1188601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188601)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188601)Termination reason: Instruction limit
% 8.65/2.11 % (1188601)Termination phase: Saturation
% 8.65/2.11 % (1188601)Time elapsed: 0.032 s
% 8.65/2.11 % (1188601)Peak memory usage: 116 MB
% 8.65/2.11 % (1188601)Instructions burned: 13 (million)
% 8.65/2.11 % (1188605)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=900795178:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 8.65/2.11 % (1188599)Instruction limit reached!
% 8.65/2.11 % (1188599)------------------------------
% 8.65/2.11 % (1188599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.11 % (1188599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.11 % (1188599)CaDiCaL version: 2.1.3
% 8.65/2.11 % (1188599)Termination reason: Instruction limit
% 8.65/2.11 % (1188599)Termination phase: Saturation
% 8.65/2.11 % (1188599)Time elapsed: 0.115 s
% 8.65/2.11 % (1188599)Peak memory usage: 91 MB
% 9.86/2.36 % (1188599)Instructions burned: 373 (million)
% 9.86/2.36 % (1188606)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=244607610:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.86/2.36 % (1188606)Instruction limit reached!
% 9.86/2.36 % (1188606)------------------------------
% 9.86/2.36 % (1188606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.36 % (1188606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.36 % (1188606)CaDiCaL version: 2.1.3
% 9.86/2.36 % (1188606)Termination reason: Instruction limit
% 9.86/2.36 % (1188606)Termination phase: Saturation
% 9.86/2.36 % (1188606)Time elapsed: 0.009 s
% 9.86/2.36 % (1188606)Peak memory usage: 88 MB
% 9.86/2.36 % (1188606)Instructions burned: 12 (million)
% 9.86/2.36 % (1188609)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2420169583:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 9.86/2.36 % (1188610)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=1743291855:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 9.86/2.36 % (1188610)Instruction limit reached!
% 9.86/2.36 % (1188610)------------------------------
% 9.86/2.36 % (1188610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.36 % (1188610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.36 % (1188610)CaDiCaL version: 2.1.3
% 9.86/2.36 % (1188610)Termination reason: Instruction limit
% 9.86/2.36 % (1188610)Termination phase: Saturation
% 9.86/2.36 % (1188610)Time elapsed: 0.053 s
% 9.86/2.36 % (1188610)Peak memory usage: 90 MB
% 9.86/2.36 % (1188610)Instructions burned: 75 (million)
% 9.86/2.36 % (1188615)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1144350843:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 9.86/2.36 % (1188594)------------------------------
% 9.86/2.36 % (1188594)------------------------------
% 9.86/2.36 % (1188612)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=1893355357:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 9.86/2.36 % (1188609)Instruction limit reached!
% 9.86/2.36 % (1188609)------------------------------
% 9.86/2.36 % (1188609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.36 % (1188609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.36 % (1188609)CaDiCaL version: 2.1.3
% 9.86/2.36 % (1188609)Termination reason: Instruction limit
% 9.86/2.36 % (1188609)Termination phase: Saturation
% 9.86/2.36 % (1188609)Time elapsed: 0.097 s
% 9.86/2.36 % (1188609)Peak memory usage: 133 MB
% 9.86/2.36 % (1188609)Instructions burned: 72 (million)
% 9.86/2.36 % (1188616)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=528773611:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 9.86/2.36 % (1188615)Instruction limit reached!
% 9.86/2.36 % (1188615)------------------------------
% 9.86/2.36 % (1188615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.36 % (1188615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.36 % (1188615)CaDiCaL version: 2.1.3
% 9.86/2.36 % (1188615)Termination reason: Instruction limit
% 9.86/2.36 % (1188615)Termination phase: Saturation
% 9.86/2.36 % (1188615)Time elapsed: 0.060 s
% 9.86/2.36 % (1188615)Peak memory usage: 116 MB
% 9.86/2.36 % (1188615)Instructions burned: 131 (million)
% 9.86/2.36 % (1188605)Instruction limit reached!
% 9.86/2.36 % (1188605)------------------------------
% 9.86/2.36 % (1188605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.36 % (1188605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.36 % (1188605)CaDiCaL version: 2.1.3
% 9.86/2.36 % (1188605)Termination reason: Instruction limit
% 9.86/2.36 % (1188605)Termination phase: Saturation
% 9.86/2.36 % (1188605)Time elapsed: 0.173 s
% 9.86/2.36 % (1188605)Peak memory usage: 116 MB
% 9.86/2.36 % (1188605)Instructions burned: 226 (million)
% 9.86/2.36 % (1188619)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1542005947:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 9.86/2.36 % (1188621)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4238917035:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.80/2.45 % (1188625)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1559177765:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.80/2.45 % (1188623)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=475427449:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 10.80/2.45 % (1188619)Instruction limit reached!
% 10.80/2.45 % (1188619)------------------------------
% 10.80/2.45 % (1188619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188619)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188619)Termination reason: Instruction limit
% 10.80/2.45 % (1188619)Termination phase: Saturation
% 10.80/2.45 % (1188619)Time elapsed: 0.066 s
% 10.80/2.45 % (1188619)Peak memory usage: 133 MB
% 10.80/2.45 % (1188619)Instructions burned: 42 (million)
% 10.80/2.45 % (1188616)Instruction limit reached!
% 10.80/2.45 % (1188616)------------------------------
% 10.80/2.45 % (1188616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188616)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188616)Termination reason: Instruction limit
% 10.80/2.45 % (1188616)Termination phase: Saturation
% 10.80/2.45 % (1188616)Time elapsed: 0.137 s
% 10.80/2.45 % (1188616)Peak memory usage: 133 MB
% 10.80/2.45 % (1188616)Instructions burned: 132 (million)
% 10.80/2.45 % (1188625)Instruction limit reached!
% 10.80/2.45 % (1188625)------------------------------
% 10.80/2.45 % (1188625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188625)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188625)Termination reason: Instruction limit
% 10.80/2.45 % (1188625)Termination phase: Saturation
% 10.80/2.45 % (1188625)Time elapsed: 0.057 s
% 10.80/2.45 % (1188625)Peak memory usage: 117 MB
% 10.80/2.45 % (1188625)Instructions burned: 131 (million)
% 10.80/2.45 % (1188626)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=59670081: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.45 % (1188612)Instruction limit reached!
% 10.80/2.45 % (1188612)------------------------------
% 10.80/2.45 % (1188612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188612)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188612)Termination reason: Instruction limit
% 10.80/2.45 % (1188612)Termination phase: Saturation
% 10.80/2.45 % (1188612)Time elapsed: 0.199 s
% 10.80/2.45 % (1188612)Peak memory usage: 90 MB
% 10.80/2.45 % (1188612)Instructions burned: 295 (million)
% 10.80/2.45 % (1188633)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3064737801:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 10.80/2.45 % (1188631)dis+10_1_si=on:random_seed=1758909757:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 10.80/2.45 % (1188632)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=946532852:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 10.80/2.45 % (1188633)Instruction limit reached!
% 10.80/2.45 % (1188633)------------------------------
% 10.80/2.45 % (1188633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188633)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188633)Termination reason: Instruction limit
% 10.80/2.45 % (1188633)Termination phase: Saturation
% 10.80/2.45 % (1188633)Time elapsed: 0.049 s
% 10.80/2.45 % (1188633)Peak memory usage: 90 MB
% 10.80/2.45 % (1188633)Instructions burned: 141 (million)
% 10.80/2.45 % (1188621)Instruction limit reached!
% 10.80/2.45 % (1188621)------------------------------
% 10.80/2.45 % (1188621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188621)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188621)Termination reason: Instruction limit
% 10.80/2.45 % (1188621)Termination phase: Saturation
% 10.80/2.45 % (1188621)Time elapsed: 0.202 s
% 10.80/2.45 % (1188621)Peak memory usage: 91 MB
% 10.80/2.45 % (1188621)Instructions burned: 307 (million)
% 10.80/2.45 % (1188635)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=1264192295:i=65:nm=16:rtra=on_2988 on theBenchmark for (2988ds/65Mi)
% 10.80/2.45 % (1188626)Instruction limit reached!
% 10.80/2.45 % (1188626)------------------------------
% 10.80/2.45 % (1188626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188626)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188626)Termination reason: Instruction limit
% 10.80/2.45 % (1188626)Termination phase: Saturation
% 10.80/2.45 % (1188626)Time elapsed: 0.194 s
% 10.80/2.45 % (1188626)Peak memory usage: 117 MB
% 10.80/2.45 % (1188626)Instructions burned: 259 (million)
% 10.80/2.45 % (1188623)First to succeed.
% 10.80/2.45 % (1188623)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1188544"
% 10.80/2.45 % (1188635)Instruction limit reached!
% 10.80/2.45 % (1188635)------------------------------
% 10.80/2.45 % (1188635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188635)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188635)Termination reason: Instruction limit
% 10.80/2.45 % (1188635)Termination phase: Saturation
% 10.80/2.45 % (1188635)Time elapsed: 0.058 s
% 10.80/2.45 % (1188635)Peak memory usage: 116 MB
% 10.80/2.45 % (1188635)Instructions burned: 65 (million)
% 10.80/2.45 % (1188639)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2686258318:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 10.80/2.45 % (1188639)Instruction limit reached!
% 10.80/2.45 % (1188639)------------------------------
% 10.80/2.45 % (1188639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188639)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188639)Termination reason: Instruction limit
% 10.80/2.45 % (1188639)Termination phase: Saturation
% 10.80/2.45 % (1188639)Time elapsed: 0.038 s
% 10.80/2.45 % (1188639)Peak memory usage: 89 MB
% 10.80/2.45 % (1188639)Instructions burned: 122 (million)
% 10.80/2.45 % (1188640)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=621466961:s2a=on:i=128:s2at=5:ins=3:rtra=on_2987 on theBenchmark for (2987ds/128Mi)
% 10.80/2.45 % (1188632)Instruction limit reached!
% 10.80/2.45 % (1188632)------------------------------
% 10.80/2.45 % (1188632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188632)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188632)Termination reason: Instruction limit
% 10.80/2.45 % (1188632)Termination phase: Saturation
% 10.80/2.45 % (1188632)Time elapsed: 0.187 s
% 10.80/2.45 % (1188632)Peak memory usage: 90 MB
% 10.80/2.45 % (1188632)Instructions burned: 383 (million)
% 10.80/2.45 % (1188642)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=1286109580:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 10.80/2.45 % (1188643)dis+1010_1_to=kbo:si=on:random_seed=1989898713:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2986 on theBenchmark for (2986ds/175Mi)
% 10.80/2.45 % (1188645)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=789703396:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/329Mi)
% 10.80/2.45 % (1188642)Instruction limit reached!
% 10.80/2.45 % (1188642)------------------------------
% 10.80/2.45 % (1188642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188642)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188642)Termination reason: Instruction limit
% 10.80/2.45 % (1188642)Termination phase: Saturation
% 10.80/2.45 % (1188642)Time elapsed: 0.050 s
% 10.80/2.45 % (1188642)Peak memory usage: 116 MB
% 10.80/2.45 % (1188642)Instructions burned: 39 (million)
% 10.80/2.45 % (1188640)Instruction limit reached!
% 10.80/2.45 % (1188640)------------------------------
% 10.80/2.45 % (1188640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.45 % (1188640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.45 % (1188640)CaDiCaL version: 2.1.3
% 10.80/2.45 % (1188640)Termination reason: Instruction limit
% 10.80/2.45 % (1188640)Termination phase: Saturation
% 10.80/2.45 % (1188640)Time elapsed: 0.110 s
% 10.80/2.45 % (1188640)Peak memory usage: 117 MB
% 10.80/2.45 % (1188640)Instructions burned: 129 (million)
% 10.80/2.45 % (1188647)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1780691836:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi)
% 10.80/2.45 % (1188623)Refutation found. Thanks to Tanya!
% 10.80/2.45 % SZS status Theorem for theBenchmark
% 10.80/2.45 % SZS output start Proof for theBenchmark
% See solution above
% 11.85/2.64 % (1188623)------------------------------
% 11.85/2.64 % (1188623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.85/2.64 % (1188623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.85/2.64 % (1188623)CaDiCaL version: 2.1.3
% 11.85/2.64 % (1188623)Termination reason: Refutation
% 11.85/2.64 % (1188623)Time elapsed: 0.252 s
% 11.85/2.64 % (1188623)Peak memory usage: 136 MB
% 11.85/2.64 % (1188623)Instructions burned: 306 (million)
% 11.85/2.64 % (1188623)------------------------------
% 11.85/2.64 % (1188623)------------------------------
% 11.85/2.64 % (1188544)Success in time 1.592 s
% 11.85/2.64 % Vampire exiting
%------------------------------------------------------------------------------