%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW631_2 : TPTP v9.3.1. Released v6.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 01:30:59 PM UTC 2026
% Result : Theorem 14.92s 3.03s
% Output : Refutation 15.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 26
% Syntax : Number of formulae : 106 ( 25 unt; 0 typ; 22 def)
% Number of atoms : 599 ( 74 equ)
% Maximal formula atoms : 44 ( 5 avg)
% Number of connectives : 756 ( 263 ~; 151 |; 238 &)
% ( 22 <=>; 82 =>; 0 <=; 0 <~>)
% Maximal formula depth : 42 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 904 ( 391 atm; 127 fun; 289 num; 97 var)
% Number of types : 7 ( 5 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 26 usr; 23 prp; 0-2 aty)
% Number of functors : 49 ( 43 usr; 22 con; 0-5 aty)
% Number of variables : 120 ( 90 !; 30 ?; 120 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
n: $int ).
tff(func_def_29,type,
f: $int > $int ).
tff(func_def_32,type,
t2tb1: map_int_int > uni ).
tff(func_def_33,type,
tb2t1: uni > map_int_int ).
tff(func_def_36,type,
sK1: map_int_int ).
tff(func_def_37,type,
sK2: map_int_int ).
tff(func_def_38,type,
sK3: $int ).
tff(func_def_39,type,
sK4: $int ).
tff(func_def_40,type,
sK5: map_int_int ).
tff(func_def_41,type,
sK6: $int ).
tff(func_def_42,type,
sK7: $int ).
tff(func_def_43,type,
sK8: $int ).
tff(func_def_44,type,
sK9: $int ).
tff(func_def_45,type,
sK10: $int ).
tff(func_def_46,type,
sK11: ( $int * $int ) > $int ).
tff(func_def_47,type,
sK12: ( $int * $int ) > $int ).
tff(func_def_48,type,
sK13: ( $int * $int ) > $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_4,type,
path: ( $int * $int ) > $o ).
tff(pred_def_5,type,
distance: ( $int * $int ) > $o ).
tff(pred_def_6,type,
sP0: ( $int * $int ) > $o ).
tff(f27,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f34,axiom,
! [X0: $int] :
( ( $less(0,X0)
& $less(X0,n) )
=> ( $lesseq(0,f(X0))
& $less(f(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_prop) ).
tff(f42,conjecture,
( $lesseq(0,n)
=> ( $lesseq(0,n)
=> ( ( $less(0,n)
& $lesseq(0,0) )
=> ! [X0: map_int_int] :
( ( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) )
& $lesseq(0,n) )
=> ( $lesseq(0,n)
=> ( $lesseq(0,n)
=> ( $lesseq(1,$difference(n,1))
=> ! [X4: $int,X3: map_int_int,X1: $int,X2: map_int_int] :
( ( $lesseq(X4,$difference(n,1))
& $lesseq(1,X4) )
=> ( ( ( tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 )
& ! [X5: $int] :
( ( $less(0,X5)
& $less(X5,X4) )
=> ( ! [X6: $int] :
( ( $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6)
& $less(X6,X5) )
=> $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6)))) )
& $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5))))
& ( tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) )
& $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5)
& $lesseq(f(X5),tb2t(get(int,int,t2tb1(X3),t2tb(X5))))
& $less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) ) )
& ! [X5: $int] :
( ( $less(X5,X4)
& $lesseq(0,X5) )
=> path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5) )
& ( tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) )
& $lesseq($sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($difference(X4,1))))),$difference(X4,1)) )
=> ! [X8: $int,X7: $int] :
( ( ! [X5: $int] :
( ( $less(X7,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) )
& $lesseq($sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7)))),$difference(X4,1))
& $lesseq(f(X4),X7)
& $less(X7,X4) )
=> ( ( $less(X7,n)
& $lesseq(0,X7)
& $lesseq(0,n) )
=> ( $lesseq(f(X4),tb2t(get(int,int,t2tb1(X3),t2tb(X7))))
=> ! [X9: $int] :
( ( X9 = $sum(X8,1) )
=> ( ( $less(X7,n)
& $lesseq(0,X7) )
=> ! [X10: $int] :
( ( X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) )
=> ! [X5: $int] :
( ( $less(X10,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_distance) ).
tff(f43,negated_conjecture,
~ ( $lesseq(0,n)
=> ( $lesseq(0,n)
=> ( ( $less(0,n)
& $lesseq(0,0) )
=> ! [X0: map_int_int] :
( ( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) )
& $lesseq(0,n) )
=> ( $lesseq(0,n)
=> ( $lesseq(0,n)
=> ( $lesseq(1,$difference(n,1))
=> ! [X4: $int,X3: map_int_int,X1: $int,X2: map_int_int] :
( ( $lesseq(X4,$difference(n,1))
& $lesseq(1,X4) )
=> ( ( ( tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 )
& ! [X5: $int] :
( ( $less(0,X5)
& $less(X5,X4) )
=> ( ! [X6: $int] :
( ( $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6)
& $less(X6,X5) )
=> $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6)))) )
& $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5))))
& ( tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) )
& $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5)
& $lesseq(f(X5),tb2t(get(int,int,t2tb1(X3),t2tb(X5))))
& $less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) ) )
& ! [X5: $int] :
( ( $less(X5,X4)
& $lesseq(0,X5) )
=> path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5) )
& ( tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) )
& $lesseq($sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($difference(X4,1))))),$difference(X4,1)) )
=> ! [X8: $int,X7: $int] :
( ( ! [X5: $int] :
( ( $less(X7,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) )
& $lesseq($sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7)))),$difference(X4,1))
& $lesseq(f(X4),X7)
& $less(X7,X4) )
=> ( ( $less(X7,n)
& $lesseq(0,X7)
& $lesseq(0,n) )
=> ( $lesseq(f(X4),tb2t(get(int,int,t2tb1(X3),t2tb(X7))))
=> ! [X9: $int] :
( ( X9 = $sum(X8,1) )
=> ( ( $less(X7,n)
& $lesseq(0,X7) )
=> ! [X10: $int] :
( ( X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) )
=> ! [X5: $int] :
( ( $less(X10,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
tff(f46,plain,
! [X0: $int] :
( ( $less(0,X0)
& $less(X0,n) )
=> ( $less(f(X0),X0)
& ~ $less(f(X0),0) ) ),
inference(theory_normalization,[],[f34]) ).
tff(f47,plain,
~ ( ~ $less(n,0)
=> ( ~ $less(n,0)
=> ( ( ~ $less(0,0)
& $less(0,n) )
=> ! [X0: map_int_int] :
( ( ~ $less(n,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) ) )
=> ( ~ $less(n,0)
=> ( ~ $less(n,0)
=> ( ~ $less($sum(n,$uminus(1)),1)
=> ! [X4: $int,X3: map_int_int,X1: $int,X2: map_int_int] :
( ( ~ $less($sum(n,$uminus(1)),X4)
& ~ $less(X4,1) )
=> ( ( ( tb2t(get(int,int,t2tb1(X2),t2tb(0))) = 0 )
& ! [X5: $int] :
( ( $less(0,X5)
& $less(X5,X4) )
=> ( ! [X6: $int] :
( ( $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X6)
& $less(X6,X5) )
=> $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),tb2t(get(int,int,t2tb1(X2),t2tb(X6)))) )
& $less(0,tb2t(get(int,int,t2tb1(X2),t2tb(X5))))
& ( tb2t(get(int,int,t2tb1(X2),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X3),t2tb(X5)))),1) )
& $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),X5)
& ~ $less(tb2t(get(int,int,t2tb1(X3),t2tb(X5))),f(X5))
& $less(tb2t(get(int,int,t2tb1(X3),get(int,int,t2tb1(X3),t2tb(X5)))),f(X5)) ) )
& ! [X5: $int] :
( ( $less(X5,X4)
& ~ $less(X5,0) )
=> path(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5) )
& ( tb2t(get(int,int,t2tb1(X3),t2tb(0))) = $uminus(1) )
& ~ $less($sum(X4,$uminus(1)),$sum(X1,tb2t(get(int,int,t2tb1(X2),t2tb($sum(X4,$uminus(1))))))) )
=> ! [X8: $int,X7: $int] :
( ( ! [X5: $int] :
( ( $less(X7,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X7))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) )
& ~ $less($sum(X4,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X2),t2tb(X7)))))
& ~ $less(X7,f(X4))
& $less(X7,X4) )
=> ( ( $less(X7,n)
& ~ $less(X7,0)
& ~ $less(n,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X3),t2tb(X7))),f(X4))
=> ! [X9: $int] :
( ( X9 = $sum(X8,1) )
=> ( ( $less(X7,n)
& ~ $less(X7,0) )
=> ! [X10: $int] :
( ( X10 = tb2t(get(int,int,t2tb1(X3),t2tb(X7))) )
=> ! [X5: $int] :
( ( $less(X10,X5)
& $less(X5,X4) )
=> $less(tb2t(get(int,int,t2tb1(X2),t2tb(X10))),tb2t(get(int,int,t2tb1(X2),t2tb(X5)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f43]) ).
tff(f57,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( X0 = X1 )
| $less(X0,X1) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f68,plain,
~ ( ~ $less(n,0)
=> ( ~ $less(n,0)
=> ( ( ~ $less(0,0)
& $less(0,n) )
=> ! [X0: map_int_int] :
( ( ~ $less(n,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) ) )
=> ( ~ $less(n,0)
=> ( ~ $less(n,0)
=> ( ~ $less($sum(n,$uminus(1)),1)
=> ! [X2: map_int_int,X4: map_int_int,X3: $int,X1: $int] :
( ( ~ $less($sum(n,$uminus(1)),X1)
& ~ $less(X1,1) )
=> ( ( ( 0 = tb2t(get(int,int,t2tb1(X4),t2tb(0))) )
& ! [X5: $int] :
( ( $less(X5,X1)
& $less(0,X5) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),f(X5))
& $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5)
& $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X2),t2tb(X5)))),f(X5))
& $less(0,tb2t(get(int,int,t2tb1(X4),t2tb(X5))))
& ! [X6: $int] :
( ( $less(X6,X5)
& $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X6) )
=> $less(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),tb2t(get(int,int,t2tb1(X4),t2tb(X6)))) )
& ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),1) ) ) )
& ~ $less($sum(X1,$uminus(1)),$sum(X3,tb2t(get(int,int,t2tb1(X4),t2tb($sum(X1,$uminus(1)))))))
& ( $uminus(1) = tb2t(get(int,int,t2tb1(X2),t2tb(0))) )
& ! [X7: $int] :
( ( ~ $less(X7,0)
& $less(X7,X1) )
=> path(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X7) ) )
=> ! [X9: $int,X8: $int] :
( ( $less(X9,X1)
& ! [X10: $int] :
( ( $less(X9,X10)
& $less(X10,X1) )
=> $less(tb2t(get(int,int,t2tb1(X4),t2tb(X9))),tb2t(get(int,int,t2tb1(X4),t2tb(X10)))) )
& ~ $less(X9,f(X1))
& ~ $less($sum(X1,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X4),t2tb(X9))))) )
=> ( ( ~ $less(X9,0)
& $less(X9,n)
& ~ $less(n,0) )
=> ( ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X9))),f(X1))
=> ! [X11: $int] :
( ( $sum(X8,1) = X11 )
=> ( ( ~ $less(X9,0)
& $less(X9,n) )
=> ! [X12: $int] :
( ( tb2t(get(int,int,t2tb1(X2),t2tb(X9))) = X12 )
=> ! [X13: $int] :
( ( $less(X12,X13)
& $less(X13,X1) )
=> $less(tb2t(get(int,int,t2tb1(X4),t2tb(X12))),tb2t(get(int,int,t2tb1(X4),t2tb(X13)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f47]) ).
tff(f83,plain,
! [X0: $int] :
( ( $less(f(X0),X0)
& ~ $less(f(X0),0) )
| ~ $less(0,X0)
| ~ $less(X0,n) ),
inference(ennf_transformation,[],[f46]) ).
tff(f84,plain,
! [X0: $int] :
( ~ $less(X0,n)
| ( $less(f(X0),X0)
& ~ $less(f(X0),0) )
| ~ $less(0,X0) ),
inference(flattening,[],[f83]) ).
tff(f91,plain,
( ? [X0: map_int_int] :
( ? [X2: map_int_int,X4: map_int_int,X3: $int,X1: $int] :
( ? [X9: $int,X8: $int] :
( ? [X11: $int] :
( ? [X12: $int] :
( ? [X13: $int] :
( ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X12))),tb2t(get(int,int,t2tb1(X4),t2tb(X13))))
& $less(X12,X13)
& $less(X13,X1) )
& ( tb2t(get(int,int,t2tb1(X2),t2tb(X9))) = X12 ) )
& ~ $less(X9,0)
& $less(X9,n)
& ( $sum(X8,1) = X11 ) )
& ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X9))),f(X1))
& ~ $less(X9,0)
& $less(X9,n)
& ~ $less(n,0)
& $less(X9,X1)
& ! [X10: $int] :
( $less(tb2t(get(int,int,t2tb1(X4),t2tb(X9))),tb2t(get(int,int,t2tb1(X4),t2tb(X10))))
| ~ $less(X9,X10)
| ~ $less(X10,X1) )
& ~ $less(X9,f(X1))
& ~ $less($sum(X1,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X4),t2tb(X9))))) )
& ( 0 = tb2t(get(int,int,t2tb1(X4),t2tb(0))) )
& ! [X5: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),f(X5))
& $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5)
& $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X2),t2tb(X5)))),f(X5))
& $less(0,tb2t(get(int,int,t2tb1(X4),t2tb(X5))))
& ! [X6: $int] :
( $less(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),tb2t(get(int,int,t2tb1(X4),t2tb(X6))))
| ~ $less(X6,X5)
| ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X6) )
& ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),1) ) )
| ~ $less(X5,X1)
| ~ $less(0,X5) )
& ~ $less($sum(X1,$uminus(1)),$sum(X3,tb2t(get(int,int,t2tb1(X4),t2tb($sum(X1,$uminus(1)))))))
& ( $uminus(1) = tb2t(get(int,int,t2tb1(X2),t2tb(0))) )
& ! [X7: $int] :
( path(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X7)
| $less(X7,0)
| ~ $less(X7,X1) )
& ~ $less($sum(n,$uminus(1)),X1)
& ~ $less(X1,1) )
& ~ $less($sum(n,$uminus(1)),1)
& ~ $less(n,0)
& ~ $less(n,0)
& ~ $less(n,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) ) )
& ~ $less(0,0)
& $less(0,n)
& ~ $less(n,0)
& ~ $less(n,0) ),
inference(ennf_transformation,[],[f68]) ).
tff(f92,plain,
( ~ $less(n,0)
& ~ $less(0,0)
& ~ $less(n,0)
& $less(0,n)
& ? [X0: map_int_int] :
( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) )
& ~ $less($sum(n,$uminus(1)),1)
& ~ $less(n,0)
& ~ $less(n,0)
& ? [X4: map_int_int,X1: $int,X3: $int,X2: map_int_int] :
( ~ $less($sum(n,$uminus(1)),X1)
& ( $uminus(1) = tb2t(get(int,int,t2tb1(X2),t2tb(0))) )
& ~ $less($sum(X1,$uminus(1)),$sum(X3,tb2t(get(int,int,t2tb1(X4),t2tb($sum(X1,$uminus(1)))))))
& ! [X5: $int] :
( ( ! [X6: $int] :
( ~ $less(X6,X5)
| $less(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),tb2t(get(int,int,t2tb1(X4),t2tb(X6))))
| ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X6) )
& $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),X5)
& $less(tb2t(get(int,int,t2tb1(X2),get(int,int,t2tb1(X2),t2tb(X5)))),f(X5))
& ( tb2t(get(int,int,t2tb1(X4),t2tb(X5))) = $sum(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X2),t2tb(X5)))),1) )
& ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X5))),f(X5))
& $less(0,tb2t(get(int,int,t2tb1(X4),t2tb(X5)))) )
| ~ $less(0,X5)
| ~ $less(X5,X1) )
& ? [X9: $int,X8: $int] :
( ~ $less(X9,0)
& ? [X11: $int] :
( ~ $less(X9,0)
& ( $sum(X8,1) = X11 )
& ? [X12: $int] :
( ( tb2t(get(int,int,t2tb1(X2),t2tb(X9))) = X12 )
& ? [X13: $int] :
( $less(X12,X13)
& $less(X13,X1)
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X12))),tb2t(get(int,int,t2tb1(X4),t2tb(X13)))) ) )
& $less(X9,n) )
& $less(X9,X1)
& ~ $less(X9,f(X1))
& $less(X9,n)
& ~ $less($sum(X1,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X4),t2tb(X9)))))
& ~ $less(n,0)
& ~ $less(tb2t(get(int,int,t2tb1(X2),t2tb(X9))),f(X1))
& ! [X10: $int] :
( $less(tb2t(get(int,int,t2tb1(X4),t2tb(X9))),tb2t(get(int,int,t2tb1(X4),t2tb(X10))))
| ~ $less(X9,X10)
| ~ $less(X10,X1) ) )
& ~ $less(X1,1)
& ( 0 = tb2t(get(int,int,t2tb1(X4),t2tb(0))) )
& ! [X7: $int] :
( ~ $less(X7,X1)
| path(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),X7)
| $less(X7,0) ) )
& ~ $less(n,0) ) ),
inference(flattening,[],[f91]) ).
tff(f100,plain,
( ~ $less(n,0)
& ~ $less(0,0)
& ~ $less(n,0)
& $less(0,n)
& ? [X0: map_int_int] :
( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) )
& ~ $less($sum(n,$uminus(1)),1)
& ~ $less(n,0)
& ~ $less(n,0)
& ? [X1: map_int_int,X2: $int,X3: $int,X4: map_int_int] :
( ~ $less($sum(n,$uminus(1)),X2)
& ( $uminus(1) = tb2t(get(int,int,t2tb1(X4),t2tb(0))) )
& ~ $less($sum(X2,$uminus(1)),$sum(X3,tb2t(get(int,int,t2tb1(X1),t2tb($sum(X2,$uminus(1)))))))
& ! [X5: $int] :
( ( ! [X6: $int] :
( ~ $less(X6,X5)
| $less(tb2t(get(int,int,t2tb1(X1),get(int,int,t2tb1(X4),t2tb(X5)))),tb2t(get(int,int,t2tb1(X1),t2tb(X6))))
| ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),X6) )
& $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),X5)
& $less(tb2t(get(int,int,t2tb1(X4),get(int,int,t2tb1(X4),t2tb(X5)))),f(X5))
& ( $sum(tb2t(get(int,int,t2tb1(X1),get(int,int,t2tb1(X4),t2tb(X5)))),1) = tb2t(get(int,int,t2tb1(X1),t2tb(X5))) )
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X5))),f(X5))
& $less(0,tb2t(get(int,int,t2tb1(X1),t2tb(X5)))) )
| ~ $less(0,X5)
| ~ $less(X5,X2) )
& ? [X7: $int,X8: $int] :
( ~ $less(X7,0)
& ? [X9: $int] :
( ~ $less(X7,0)
& ( $sum(X8,1) = X9 )
& ? [X10: $int] :
( ( tb2t(get(int,int,t2tb1(X4),t2tb(X7))) = X10 )
& ? [X11: $int] :
( $less(X10,X11)
& $less(X11,X2)
& ~ $less(tb2t(get(int,int,t2tb1(X1),t2tb(X10))),tb2t(get(int,int,t2tb1(X1),t2tb(X11)))) ) )
& $less(X7,n) )
& $less(X7,X2)
& ~ $less(X7,f(X2))
& $less(X7,n)
& ~ $less($sum(X2,$uminus(1)),$sum(X8,tb2t(get(int,int,t2tb1(X1),t2tb(X7)))))
& ~ $less(n,0)
& ~ $less(tb2t(get(int,int,t2tb1(X4),t2tb(X7))),f(X2))
& ! [X12: $int] :
( $less(tb2t(get(int,int,t2tb1(X1),t2tb(X7))),tb2t(get(int,int,t2tb1(X1),t2tb(X12))))
| ~ $less(X7,X12)
| ~ $less(X12,X2) ) )
& ~ $less(X2,1)
& ( 0 = tb2t(get(int,int,t2tb1(X1),t2tb(0))) )
& ! [X13: $int] :
( ~ $less(X13,X2)
| path(tb2t(get(int,int,t2tb1(X1),t2tb(X13))),X13)
| $less(X13,0) ) )
& ~ $less(n,0) ) ),
inference(rectify,[],[f92]) ).
tff(f101,plain,
( ~ $less(n,0)
& ~ $less(0,0)
& ~ $less(n,0)
& $less(0,n)
& ( tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb($uminus(1)))) = sK1 )
& ~ $less($sum(n,$uminus(1)),1)
& ~ $less(n,0)
& ~ $less(n,0)
& ~ $less($sum(n,$uminus(1)),sK3)
& ( $uminus(1) = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
& ~ $less($sum(sK3,$uminus(1)),$sum(sK4,tb2t(get(int,int,t2tb1(sK2),t2tb($sum(sK3,$uminus(1)))))))
& ! [X5: $int] :
( ( ! [X6: $int] :
( ~ $less(X6,X5)
| $less(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(X5)))),tb2t(get(int,int,t2tb1(sK2),t2tb(X6))))
| ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(X5))),X6) )
& $less(tb2t(get(int,int,t2tb1(sK5),t2tb(X5))),X5)
& $less(tb2t(get(int,int,t2tb1(sK5),get(int,int,t2tb1(sK5),t2tb(X5)))),f(X5))
& ( $sum(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(X5)))),1) = tb2t(get(int,int,t2tb1(sK2),t2tb(X5))) )
& ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(X5))),f(X5))
& $less(0,tb2t(get(int,int,t2tb1(sK2),t2tb(X5)))) )
| ~ $less(0,X5)
| ~ $less(X5,sK3) )
& ~ $less(sK6,0)
& ~ $less(sK6,0)
& ( $sum(sK7,1) = sK8 )
& ( sK9 = tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))) )
& $less(sK9,sK10)
& $less(sK10,sK3)
& ~ $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10))))
& $less(sK6,n)
& $less(sK6,sK3)
& ~ $less(sK6,f(sK3))
& $less(sK6,n)
& ~ $less($sum(sK3,$uminus(1)),$sum(sK7,tb2t(get(int,int,t2tb1(sK2),t2tb(sK6)))))
& ~ $less(n,0)
& ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),f(sK3))
& ! [X12: $int] :
( $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK2),t2tb(X12))))
| ~ $less(sK6,X12)
| ~ $less(X12,sK3) )
& ~ $less(sK3,1)
& ( 0 = tb2t(get(int,int,t2tb1(sK2),t2tb(0))) )
& ! [X13: $int] :
( ~ $less(X13,sK3)
| path(tb2t(get(int,int,t2tb1(sK2),t2tb(X13))),X13)
| $less(X13,0) )
& ~ $less(n,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X7,sK6),skolemize(X8,sK7),skolemize(X9,sK8),skolemize(X10,sK9),skolemize(X11,sK10)],[f100]) ).
tff(f120,plain,
~ $less(sK3,1),
inference(cnf_transformation,[],[f101]) ).
tff(f121,plain,
! [X12: $int] :
( ~ $less(sK6,X12)
| $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK2),t2tb(X12))))
| ~ $less(X12,sK3) ),
inference(cnf_transformation,[],[f101]) ).
tff(f122,plain,
~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),f(sK3)),
inference(cnf_transformation,[],[f101]) ).
tff(f127,plain,
$less(sK6,sK3),
inference(cnf_transformation,[],[f101]) ).
tff(f129,plain,
~ $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10)))),
inference(cnf_transformation,[],[f101]) ).
tff(f130,plain,
$less(sK10,sK3),
inference(cnf_transformation,[],[f101]) ).
tff(f131,plain,
$less(sK9,sK10),
inference(cnf_transformation,[],[f101]) ).
tff(f132,plain,
sK9 = tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),
inference(cnf_transformation,[],[f101]) ).
tff(f135,plain,
~ $less(sK6,0),
inference(cnf_transformation,[],[f101]) ).
tff(f138,plain,
! [X5: $int] :
( ~ $less(0,X5)
| ~ $less(X5,sK3)
| ( $sum(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(X5)))),1) = tb2t(get(int,int,t2tb1(sK2),t2tb(X5))) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f141,plain,
! [X6: $int,X5: $int] :
( ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(X5))),X6)
| $less(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(X5)))),tb2t(get(int,int,t2tb1(sK2),t2tb(X6))))
| ~ $less(0,X5)
| ~ $less(X5,sK3)
| ~ $less(X6,X5) ),
inference(cnf_transformation,[],[f101]) ).
tff(f143,plain,
$uminus(1) = tb2t(get(int,int,t2tb1(sK5),t2tb(0))),
inference(cnf_transformation,[],[f101]) ).
tff(f144,plain,
~ $less($sum(n,$uminus(1)),sK3),
inference(cnf_transformation,[],[f101]) ).
tff(f154,plain,
! [X0: $int] :
( ~ $less(f(X0),0)
| ~ $less(X0,n)
| ~ $less(0,X0) ),
inference(cnf_transformation,[],[f84]) ).
tff(f168,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f27]) ).
tff(f175,plain,
~ $less($sum(n,-1),sK3),
inference(evaluation,[],[f144]) ).
tff(f176,plain,
-1 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))),
inference(evaluation,[],[f143]) ).
tff(f210,definition,
( spl14_7
<=> $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10)))) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
tff(f212,plain,
( ~ $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10))))
| spl14_7 ),
inference(avatar_component_clause,[],[f210]) ).
tff(f213,plain,
~ spl14_7,
inference(avatar_split_clause,[],[f129,f210]) ).
tff(f215,definition,
( spl14_8
<=> $less(sK6,0) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
tff(f217,plain,
( ~ $less(sK6,0)
| spl14_8 ),
inference(avatar_component_clause,[],[f215]) ).
tff(f218,plain,
~ spl14_8,
inference(avatar_split_clause,[],[f135,f215]) ).
tff(f225,definition,
( spl14_10
<=> $less($sum(n,-1),sK3) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
tff(f228,plain,
~ spl14_10,
inference(avatar_split_clause,[],[f175,f225]) ).
tff(f230,definition,
( spl14_11
<=> $less(sK6,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
tff(f232,plain,
( $less(sK6,sK3)
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f230]) ).
tff(f233,plain,
spl14_11,
inference(avatar_split_clause,[],[f127,f230]) ).
tff(f240,definition,
( spl14_13
<=> $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),f(sK3)) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
tff(f242,plain,
( ~ $less(tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))),f(sK3))
| spl14_13 ),
inference(avatar_component_clause,[],[f240]) ).
tff(f243,plain,
~ spl14_13,
inference(avatar_split_clause,[],[f122,f240]) ).
tff(f245,definition,
( spl14_14
<=> ( sK9 = tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))) ) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
tff(f247,plain,
( ( sK9 = tb2t(get(int,int,t2tb1(sK5),t2tb(sK6))) )
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f245]) ).
tff(f248,plain,
spl14_14,
inference(avatar_split_clause,[],[f132,f245]) ).
tff(f250,definition,
( spl14_15
<=> $less(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
tff(f252,plain,
( $less(sK9,sK10)
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f250]) ).
tff(f253,plain,
spl14_15,
inference(avatar_split_clause,[],[f131,f250]) ).
tff(f255,definition,
( spl14_16
<=> $less(sK3,1) ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
tff(f258,plain,
~ spl14_16,
inference(avatar_split_clause,[],[f120,f255]) ).
tff(f260,definition,
( spl14_17
<=> ( -1 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) ) ),
introduced(definition,[new_symbols(definition,[spl14_17])],[avatar_definition]) ).
tff(f262,plain,
( ( -1 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ spl14_17 ),
inference(avatar_component_clause,[],[f260]) ).
tff(f263,plain,
spl14_17,
inference(avatar_split_clause,[],[f176,f260]) ).
tff(f275,definition,
( spl14_20
<=> $less(sK10,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_20])],[avatar_definition]) ).
tff(f277,plain,
( $less(sK10,sK3)
| ~ spl14_20 ),
inference(avatar_component_clause,[],[f275]) ).
tff(f278,plain,
spl14_20,
inference(avatar_split_clause,[],[f130,f275]) ).
tff(f293,plain,
( $less(0,sK6)
| ( 0 = sK6 )
| spl14_8 ),
inference(resolution,[],[f217,f57]) ).
tff(f297,definition,
( spl14_23
<=> ( 0 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl14_23])],[avatar_definition]) ).
tff(f299,plain,
( ( 0 = sK6 )
| ~ spl14_23 ),
inference(avatar_component_clause,[],[f297]) ).
tff(f301,definition,
( spl14_24
<=> $less(0,sK6) ),
introduced(definition,[new_symbols(definition,[spl14_24])],[avatar_definition]) ).
tff(f303,plain,
( $less(0,sK6)
| ~ spl14_24 ),
inference(avatar_component_clause,[],[f301]) ).
tff(f305,plain,
( spl14_24
| spl14_23
| spl14_8 ),
inference(avatar_split_clause,[],[f293,f215,f297,f301]) ).
tff(f374,plain,
( ~ $less(sK9,f(sK3))
| spl14_13
| ~ spl14_14 ),
inference(forward_demodulation,[],[f242,f247]) ).
tff(f376,definition,
( spl14_33
<=> $less(sK9,f(sK3)) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
tff(f379,plain,
( ~ spl14_33
| spl14_13
| ~ spl14_14 ),
inference(avatar_split_clause,[],[f374,f245,f240,f376]) ).
tff(f391,definition,
( spl14_34
<=> $less(0,sK3) ),
introduced(definition,[new_symbols(definition,[spl14_34])],[avatar_definition]) ).
tff(f392,plain,
( $less(0,sK3)
| ~ spl14_34 ),
inference(avatar_component_clause,[],[f391]) ).
tff(f422,plain,
( ( sK9 = tb2t(get(int,int,t2tb1(sK5),t2tb(0))) )
| ~ spl14_14
| ~ spl14_23 ),
inference(superposition,[],[f247,f299]) ).
tff(f430,definition,
( spl14_37
<=> $less(f(sK3),0) ),
introduced(definition,[new_symbols(definition,[spl14_37])],[avatar_definition]) ).
tff(f432,plain,
( $less(f(sK3),0)
| ~ spl14_37 ),
inference(avatar_component_clause,[],[f430]) ).
tff(f436,plain,
( ( -1 = sK9 )
| ~ spl14_14
| ~ spl14_17
| ~ spl14_23 ),
inference(forward_demodulation,[],[f422,f262]) ).
tff(f448,definition,
( spl14_40
<=> ( -1 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl14_40])],[avatar_definition]) ).
tff(f451,plain,
( spl14_40
| ~ spl14_14
| ~ spl14_17
| ~ spl14_23 ),
inference(avatar_split_clause,[],[f436,f297,f260,f245,f448]) ).
tff(f490,plain,
! [X0: $int] :
( ~ $less(X0,sK3)
| $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK2),t2tb(X0))))
| $less(X0,sK6)
| ( sK6 = X0 ) ),
inference(resolution,[],[f121,f57]) ).
tff(f502,plain,
( ( tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))) = $sum(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),1) )
| ~ $less(sK6,sK3)
| ~ spl14_24 ),
inference(resolution,[],[f138,f303]) ).
tff(f506,plain,
( ( tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))) = $sum(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),1) )
| ~ spl14_11
| ~ spl14_24 ),
inference(forward_subsumption_resolution,[],[f502,f232]) ).
tff(f508,definition,
( spl14_46
<=> ( tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))) = $sum(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),1) ) ),
introduced(definition,[new_symbols(definition,[spl14_46])],[avatar_definition]) ).
tff(f511,plain,
( spl14_46
| ~ spl14_11
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f506,f301,f230,f508]) ).
tff(f516,definition,
( spl14_47
<=> $less(sK3,n) ),
introduced(definition,[new_symbols(definition,[spl14_47])],[avatar_definition]) ).
tff(f518,plain,
( $less(sK3,n)
| ~ spl14_47 ),
inference(avatar_component_clause,[],[f516]) ).
tff(f560,plain,
( ! [X0: $int] :
( ~ $less(sK6,sK3)
| ~ $less(X0,sK6)
| $less(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),tb2t(get(int,int,t2tb1(sK2),t2tb(X0))))
| ~ $less(sK9,X0)
| ~ $less(0,sK6) )
| ~ spl14_14 ),
inference(superposition,[],[f141,f247]) ).
tff(f562,plain,
( ! [X0: $int] :
( ~ $less(X0,sK6)
| ~ $less(sK9,X0)
| $less(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),tb2t(get(int,int,t2tb1(sK2),t2tb(X0))))
| ~ $less(0,sK6) )
| ~ spl14_11
| ~ spl14_14 ),
inference(forward_subsumption_resolution,[],[f560,f232]) ).
tff(f563,plain,
( ! [X0: $int] :
( ~ $less(sK9,X0)
| ~ $less(X0,sK6)
| $less(tb2t(get(int,int,t2tb1(sK2),get(int,int,t2tb1(sK5),t2tb(sK6)))),tb2t(get(int,int,t2tb1(sK2),t2tb(X0)))) )
| ~ spl14_11
| ~ spl14_14
| ~ spl14_24 ),
inference(forward_subsumption_resolution,[],[f562,f303]) ).
tff(f581,plain,
( ( t2tb(sK9) = get(int,int,t2tb1(sK5),t2tb(sK6)) )
| ~ spl14_14 ),
inference(superposition,[],[f168,f247]) ).
tff(f593,definition,
( spl14_53
<=> ( t2tb(sK9) = get(int,int,t2tb1(sK5),t2tb(sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl14_53])],[avatar_definition]) ).
tff(f595,plain,
( ( t2tb(sK9) = get(int,int,t2tb1(sK5),t2tb(sK6)) )
| ~ spl14_53 ),
inference(avatar_component_clause,[],[f593]) ).
tff(f596,plain,
( spl14_53
| ~ spl14_14 ),
inference(avatar_split_clause,[],[f581,f245,f593]) ).
tff(f927,plain,
( ~ $less(sK3,n)
| ~ $less(0,sK3)
| ~ spl14_37 ),
inference(resolution,[],[f432,f154]) ).
tff(f933,plain,
( ~ $less(0,sK3)
| ~ spl14_37
| ~ spl14_47 ),
inference(forward_subsumption_resolution,[],[f927,f518]) ).
tff(f934,plain,
( $false
| ~ spl14_34
| ~ spl14_37
| ~ spl14_47 ),
inference(forward_subsumption_resolution,[],[f933,f392]) ).
tff(f935,plain,
( ~ spl14_34
| ~ spl14_37
| ~ spl14_47 ),
inference(avatar_contradiction_clause,[],[f934]) ).
tff(f1282,plain,
( ( sK10 = sK6 )
| $less(sK10,sK6)
| $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10))))
| ~ spl14_20 ),
inference(resolution,[],[f490,f277]) ).
tff(f1297,definition,
( spl14_122
<=> $less(sK10,sK6) ),
introduced(definition,[new_symbols(definition,[spl14_122])],[avatar_definition]) ).
tff(f1299,plain,
( $less(sK10,sK6)
| ~ spl14_122 ),
inference(avatar_component_clause,[],[f1297]) ).
tff(f1301,definition,
( spl14_123
<=> ( sK10 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl14_123])],[avatar_definition]) ).
tff(f1305,definition,
( spl14_124
<=> $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK6))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10)))) ),
introduced(definition,[new_symbols(definition,[spl14_124])],[avatar_definition]) ).
tff(f1308,plain,
( spl14_122
| spl14_123
| spl14_124
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f1282,f275,f1305,f1301,f1297]) ).
tff(f1377,plain,
( ! [X0: $int] :
( ~ $less(sK9,X0)
| ~ $less(X0,sK6)
| $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(X0)))) )
| ~ spl14_11
| ~ spl14_14
| ~ spl14_24
| ~ spl14_53 ),
inference(forward_demodulation,[],[f563,f595]) ).
tff(f1395,plain,
( ~ $less(sK10,sK6)
| $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10))))
| ~ spl14_11
| ~ spl14_14
| ~ spl14_15
| ~ spl14_24
| ~ spl14_53 ),
inference(resolution,[],[f1377,f252]) ).
tff(f1417,plain,
( $less(tb2t(get(int,int,t2tb1(sK2),t2tb(sK9))),tb2t(get(int,int,t2tb1(sK2),t2tb(sK10))))
| ~ spl14_11
| ~ spl14_14
| ~ spl14_15
| ~ spl14_24
| ~ spl14_53
| ~ spl14_122 ),
inference(forward_subsumption_resolution,[],[f1395,f1299]) ).
tff(f1418,plain,
( $false
| spl14_7
| ~ spl14_11
| ~ spl14_14
| ~ spl14_15
| ~ spl14_24
| ~ spl14_53
| ~ spl14_122 ),
inference(forward_subsumption_resolution,[],[f1417,f212]) ).
tff(f1419,plain,
( spl14_7
| ~ spl14_11
| ~ spl14_14
| ~ spl14_15
| ~ spl14_24
| ~ spl14_53
| ~ spl14_122 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
tff(f1420,plain,
$false,
inference(avatar_smt_refutation,[],[f1419,f1308,f935,f596,f511,f451,f379,f305,f278,f263,f258,f253,f248,f243,f233,f228,f218,f213]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW631_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.18 % Computer : n014.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.18 % WCLimit : 300
% 0.11/0.18 % DateTime : Mon Sep 28 14:23:00 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.20 Running first-order theorem proving
% 0.11/0.20 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
% 4.10/1.40 % (1806800)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.10/1.40 % (1806843)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3676084530:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.10/1.40 % (1806843)Instruction limit reached!
% 4.10/1.40 % (1806843)------------------------------
% 4.10/1.40 % (1806843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.10/1.40 % (1806843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.40 % (1806843)CaDiCaL version: 2.1.3
% 4.10/1.40 % (1806843)Termination reason: Instruction limit
% 4.10/1.40 % (1806843)Termination phase: Saturation
% 4.10/1.40 % (1806843)Time elapsed: 0.004 s
% 4.10/1.40 % (1806843)Peak memory usage: 88 MB
% 4.10/1.40 % (1806843)Instructions burned: 9 (million)
% 4.10/1.40 % (1806838)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=815027015:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.10/1.40 % (1806848)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=294012434:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.10/1.40 % (1806846)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2078748824:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.10/1.40 % (1806841)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1356401997:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.10/1.40 % (1806840)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3475275785:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.10/1.40 % (1806845)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1002784430:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.10/1.40 % (1806845)Instruction limit reached!
% 4.10/1.40 % (1806845)------------------------------
% 4.10/1.40 % (1806845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.10/1.40 % (1806845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.40 % (1806845)CaDiCaL version: 2.1.3
% 4.10/1.40 % (1806845)Termination reason: Instruction limit
% 4.10/1.40 % (1806845)Termination phase: Property scanning
% 4.10/1.40 % (1806845)Time elapsed: 0.005 s
% 4.10/1.40 % (1806845)Peak memory usage: 87 MB
% 4.10/1.40 % (1806845)Instructions burned: 4 (million)
% 4.10/1.40 % (1806838)Instruction limit reached!
% 4.10/1.40 % (1806838)------------------------------
% 4.10/1.40 % (1806838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.10/1.40 % (1806838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.40 % (1806838)CaDiCaL version: 2.1.3
% 4.10/1.40 % (1806838)Termination reason: Instruction limit
% 4.10/1.40 % (1806838)Termination phase: Saturation
% 4.10/1.40 % (1806838)Time elapsed: 0.028 s
% 4.10/1.40 % (1806838)Peak memory usage: 112 MB
% 4.10/1.40 % (1806838)Instructions burned: 12 (million)
% 4.10/1.40 % (1806848)Instruction limit reached!
% 4.10/1.40 % (1806848)------------------------------
% 4.10/1.40 % (1806848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.10/1.40 % (1806848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.40 % (1806848)CaDiCaL version: 2.1.3
% 4.10/1.40 % (1806848)Termination reason: Instruction limit
% 4.10/1.40 % (1806848)Termination phase: Saturation
% 4.10/1.40 % (1806848)Time elapsed: 0.044 s
% 4.10/1.40 % (1806848)Peak memory usage: 116 MB
% 4.10/1.40 % (1806848)Instructions burned: 34 (million)
% 4.10/1.40 % (1806846)Instruction limit reached!
% 4.10/1.40 % (1806846)------------------------------
% 4.10/1.40 % (1806846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.10/1.40 % (1806846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/1.40 % (1806846)CaDiCaL version: 2.1.3
% 4.10/1.40 % (1806846)Termination reason: Instruction limit
% 4.10/1.40 % (1806846)Termination phase: Saturation
% 4.10/1.40 % (1806846)Time elapsed: 0.077 s
% 4.10/1.40 % (1806846)Peak memory usage: 116 MB
% 4.10/1.40 % (1806846)Instructions burned: 46 (million)
% 4.10/1.40 % (1806885)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=146358300:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.10/1.40 % (1806885)Instruction limit reached!
% 4.10/1.40 % (1806885)------------------------------
% 5.65/1.64 % (1806885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806885)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806885)Termination reason: Instruction limit
% 5.65/1.64 % (1806885)Termination phase: Saturation
% 5.65/1.64 % (1806885)Time elapsed: 0.010 s
% 5.65/1.64 % (1806885)Peak memory usage: 89 MB
% 5.65/1.64 % (1806885)Instructions burned: 14 (million)
% 5.65/1.64 % (1806903)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=3243503364:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 5.65/1.64 % (1806903)Instruction limit reached!
% 5.65/1.64 % (1806903)------------------------------
% 5.65/1.64 % (1806903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806903)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806903)Termination reason: Instruction limit
% 5.65/1.64 % (1806903)Termination phase: Saturation
% 5.65/1.64 % (1806903)Time elapsed: 0.013 s
% 5.65/1.64 % (1806903)Peak memory usage: 89 MB
% 5.65/1.64 % (1806903)Instructions burned: 29 (million)
% 5.65/1.64 % (1806841)Instruction limit reached!
% 5.65/1.64 % (1806841)------------------------------
% 5.65/1.64 % (1806841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806841)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806841)Termination reason: Instruction limit
% 5.65/1.64 % (1806841)Termination phase: Saturation
% 5.65/1.64 % (1806841)Time elapsed: 0.176 s
% 5.65/1.64 % (1806841)Peak memory usage: 119 MB
% 5.65/1.64 % (1806841)Instructions burned: 201 (million)
% 5.65/1.64 % (1806912)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=965782590:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.65/1.64 % (1806912)Instruction limit reached!
% 5.65/1.64 % (1806912)------------------------------
% 5.65/1.64 % (1806912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806912)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806912)Termination reason: Instruction limit
% 5.65/1.64 % (1806912)Termination phase: Saturation
% 5.65/1.64 % (1806912)Time elapsed: 0.012 s
% 5.65/1.64 % (1806912)Peak memory usage: 88 MB
% 5.65/1.64 % (1806912)Instructions burned: 16 (million)
% 5.65/1.64 % (1806920)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1468002885:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 5.65/1.64 % (1806840)Instruction limit reached!
% 5.65/1.64 % (1806840)------------------------------
% 5.65/1.64 % (1806840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806840)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806840)Termination reason: Instruction limit
% 5.65/1.64 % (1806840)Termination phase: Saturation
% 5.65/1.64 % (1806840)Time elapsed: 0.231 s
% 5.65/1.64 % (1806840)Peak memory usage: 117 MB
% 5.65/1.64 % (1806840)Instructions burned: 307 (million)
% 5.65/1.64 % (1806920)Instruction limit reached!
% 5.65/1.64 % (1806920)------------------------------
% 5.65/1.64 % (1806920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.64 % (1806920)CaDiCaL version: 2.1.3
% 5.65/1.64 % (1806920)Termination reason: Instruction limit
% 5.65/1.64 % (1806920)Termination phase: Saturation
% 5.65/1.64 % (1806920)Time elapsed: 0.030 s
% 5.65/1.64 % (1806920)Peak memory usage: 90 MB
% 5.65/1.64 % (1806920)Instructions burned: 25 (million)
% 5.65/1.64 % (1806926)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=4092753137:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 5.65/1.64 % (1806926)Instruction limit reached!
% 5.65/1.64 % (1806926)------------------------------
% 5.65/1.64 % (1806926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.64 % (1806926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806926)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806926)Termination reason: Instruction limit
% 7.45/1.91 % (1806926)Termination phase: Saturation
% 7.45/1.91 % (1806926)Time elapsed: 0.016 s
% 7.45/1.91 % (1806926)Peak memory usage: 89 MB
% 7.45/1.91 % (1806926)Instructions burned: 28 (million)
% 7.45/1.91 % (1806936)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1610305673:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 7.45/1.91 % (1806945)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1809172594:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.45/1.91 % (1806945)Instruction limit reached!
% 7.45/1.91 % (1806945)------------------------------
% 7.45/1.91 % (1806945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.91 % (1806945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806945)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806945)Termination reason: Instruction limit
% 7.45/1.91 % (1806945)Termination phase: Naming
% 7.45/1.91 % (1806945)Time elapsed: 0.003 s
% 7.45/1.91 % (1806945)Peak memory usage: 86 MB
% 7.45/1.91 % (1806945)Instructions burned: 2 (million)
% 7.45/1.91 % (1806967)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=118157010:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 7.45/1.91 % (1806967)Instruction limit reached!
% 7.45/1.91 % (1806967)------------------------------
% 7.45/1.91 % (1806967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.91 % (1806967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806967)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806967)Termination reason: Instruction limit
% 7.45/1.91 % (1806967)Termination phase: Property scanning
% 7.45/1.91 % (1806967)Time elapsed: 0.005 s
% 7.45/1.91 % (1806967)Peak memory usage: 86 MB
% 7.45/1.91 % (1806967)Instructions burned: 4 (million)
% 7.45/1.91 % (1806936)Instruction limit reached!
% 7.45/1.91 % (1806936)------------------------------
% 7.45/1.91 % (1806936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.91 % (1806936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806936)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806936)Termination reason: Instruction limit
% 7.45/1.91 % (1806936)Termination phase: Saturation
% 7.45/1.91 % (1806936)Time elapsed: 0.077 s
% 7.45/1.91 % (1806936)Peak memory usage: 89 MB
% 7.45/1.91 % (1806936)Instructions burned: 85 (million)
% 7.45/1.91 % (1806953)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1976874571:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 7.45/1.91 % (1806977)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4111384946:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.45/1.91 % (1806979)lrs+10_1_thi=all:si=on:fd=off:random_seed=1727299572:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 7.45/1.91 % (1806981)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=3145775562:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 7.45/1.91 % (1806981)Instruction limit reached!
% 7.45/1.91 % (1806981)------------------------------
% 7.45/1.91 % (1806981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.91 % (1806981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806981)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806981)Termination reason: Instruction limit
% 7.45/1.91 % (1806981)Termination phase: Saturation
% 7.45/1.91 % (1806981)Time elapsed: 0.010 s
% 7.45/1.91 % (1806981)Peak memory usage: 88 MB
% 7.45/1.91 % (1806981)Instructions burned: 9 (million)
% 7.45/1.91 % (1806998)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1050889487:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.45/1.91 % (1806998)Instruction limit reached!
% 7.45/1.91 % (1806998)------------------------------
% 7.45/1.91 % (1806998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.91 % (1806998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.91 % (1806998)CaDiCaL version: 2.1.3
% 7.45/1.91 % (1806998)Termination reason: Instruction limit
% 7.45/1.91 % (1806998)Termination phase: Preprocessing 3
% 10.49/2.19 % (1806998)Time elapsed: 0.002 s
% 10.49/2.19 % (1806998)Peak memory usage: 86 MB
% 10.49/2.19 % (1806998)Instructions burned: 3 (million)
% 10.49/2.19 % (1806996)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2701254225:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 10.49/2.19 % (1806996)Instruction limit reached!
% 10.49/2.19 % (1806996)------------------------------
% 10.49/2.19 % (1806996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1806996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1806996)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1806996)Termination reason: Instruction limit
% 10.49/2.19 % (1806996)Termination phase: Preprocessing 3
% 10.49/2.19 % (1806996)Time elapsed: 0.003 s
% 10.49/2.19 % (1806996)Peak memory usage: 86 MB
% 10.49/2.19 % (1806996)Instructions burned: 2 (million)
% 10.49/2.19 % (1806979)Instruction limit reached!
% 10.49/2.19 % (1806979)------------------------------
% 10.49/2.19 % (1806979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1806979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1806979)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1806979)Termination reason: Instruction limit
% 10.49/2.19 % (1806979)Termination phase: Saturation
% 10.49/2.19 % (1806979)Time elapsed: 0.094 s
% 10.49/2.19 % (1806979)Peak memory usage: 116 MB
% 10.49/2.19 % (1806979)Instructions burned: 53 (million)
% 10.49/2.19 % (1806953)Instruction limit reached!
% 10.49/2.19 % (1806953)------------------------------
% 10.49/2.19 % (1806953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1806953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1806953)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1806953)Termination reason: Instruction limit
% 10.49/2.19 % (1806953)Termination phase: Saturation
% 10.49/2.19 % (1806953)Time elapsed: 0.200 s
% 10.49/2.19 % (1806953)Peak memory usage: 91 MB
% 10.49/2.19 % (1806953)Instructions burned: 181 (million)
% 10.49/2.19 % (1806977)Instruction limit reached!
% 10.49/2.19 % (1806977)------------------------------
% 10.49/2.19 % (1806977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1806977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1806977)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1806977)Termination reason: Instruction limit
% 10.49/2.19 % (1806977)Termination phase: Saturation
% 10.49/2.19 % (1806977)Time elapsed: 0.135 s
% 10.49/2.19 % (1806977)Peak memory usage: 134 MB
% 10.49/2.19 % (1806977)Instructions burned: 66 (million)
% 10.49/2.19 % (1807000)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=74285448:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 10.49/2.19 % (1807013)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=334588872:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.49/2.19 % (1807010)dis+10_1_si=on:random_seed=2259680174:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.49/2.19 % (1807013)Refutation not found, incomplete strategy
% 10.49/2.19 % (1807013)------------------------------
% 10.49/2.19 % (1807013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1807013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1807013)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1807013)Termination reason: Refutation not found, incomplete strategy
% 10.49/2.19 % (1807013)Time elapsed: 0.007 s
% 10.49/2.19 % (1807013)Peak memory usage: 89 MB
% 10.49/2.19 % (1807013)Instructions burned: 11 (million)
% 10.49/2.19 % (1807010)Instruction limit reached!
% 10.49/2.19 % (1807010)------------------------------
% 10.49/2.19 % (1807010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.19 % (1807010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.19 % (1807010)CaDiCaL version: 2.1.3
% 10.49/2.19 % (1807010)Termination reason: Instruction limit
% 10.49/2.19 % (1807010)Termination phase: Saturation
% 10.49/2.19 % (1807010)Time elapsed: 0.012 s
% 10.49/2.19 % (1807010)Peak memory usage: 88 MB
% 10.49/2.19 % (1807010)Instructions burned: 10 (million)
% 10.49/2.19 % (1807016)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2196980796:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.49/2.19 % (1807016)Instruction limit reached!
% 10.49/2.19 % (1807016)------------------------------
% 10.49/2.19 % (1807016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/2.46 % (1807016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/2.46 % (1807016)CaDiCaL version: 2.1.3
% 11.40/2.46 % (1807016)Termination reason: Instruction limit
% 11.40/2.46 % (1807016)Termination phase: Unused predicate definition removal
% 11.40/2.46 % (1807016)Time elapsed: 0.001 s
% 11.40/2.46 % (1807016)Peak memory usage: 85 MB
% 11.40/2.46 % (1807016)Instructions burned: 2 (million)
% 11.40/2.46 % (1807014)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2802235049: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_2992 on theBenchmark for (2992ds/35Mi)
% 11.40/2.46 % (1807017)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3711315389:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi)
% 11.40/2.46 % (1807017)Instruction limit reached!
% 11.40/2.46 % (1807017)------------------------------
% 11.40/2.46 % (1807017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/2.46 % (1807017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/2.46 % (1807017)CaDiCaL version: 2.1.3
% 11.40/2.46 % (1807017)Termination reason: Instruction limit
% 11.40/2.46 % (1807017)Termination phase: Saturation
% 11.40/2.46 % (1807017)Time elapsed: 0.010 s
% 11.40/2.46 % (1807017)Peak memory usage: 89 MB
% 11.40/2.46 % (1807017)Instructions burned: 8 (million)
% 11.40/2.46 % (1807014)Instruction limit reached!
% 11.40/2.46 % (1807014)------------------------------
% 11.40/2.46 % (1807014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/2.46 % (1807014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/2.46 % (1807014)CaDiCaL version: 2.1.3
% 11.40/2.46 % (1807014)Termination reason: Instruction limit
% 11.40/2.46 % (1807014)Termination phase: Saturation
% 11.40/2.46 % (1807014)Time elapsed: 0.043 s
% 11.40/2.46 % (1807014)Peak memory usage: 89 MB
% 11.40/2.46 % (1807014)Instructions burned: 35 (million)
% 11.40/2.46 % (1807000)Instruction limit reached!
% 11.40/2.46 % (1807000)------------------------------
% 11.40/2.46 % (1807000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/2.46 % (1807000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/2.46 % (1807000)CaDiCaL version: 2.1.3
% 11.40/2.46 % (1807000)Termination reason: Instruction limit
% 11.40/2.46 % (1807000)Termination phase: Saturation
% 11.40/2.46 % (1807000)Time elapsed: 0.185 s
% 11.40/2.46 % (1807000)Peak memory usage: 117 MB
% 11.40/2.46 % (1807000)Instructions burned: 127 (million)
% 11.40/2.46 % (1807019)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4002871179:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 11.40/2.46 % (1807013)------------------------------
% 11.40/2.46 % (1807013)------------------------------
% 11.40/2.46 % (1807029)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1931788147:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 11.40/2.46 % (1807033)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3100283161:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 11.40/2.46 % (1807034)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3344094432:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 11.40/2.46 % (1807034)Instruction limit reached!
% 11.40/2.46 % (1807034)------------------------------
% 11.40/2.46 % (1807034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.40/2.46 % (1807034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.40/2.46 % (1807034)CaDiCaL version: 2.1.3
% 11.40/2.46 % (1807034)Termination reason: Instruction limit
% 11.40/2.46 % (1807034)Termination phase: Saturation
% 11.40/2.46 % (1807034)Time elapsed: 0.013 s
% 11.40/2.46 % (1807034)Peak memory usage: 88 MB
% 11.40/2.46 % (1807034)Instructions burned: 10 (million)
% 11.40/2.46 % (1807035)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4158377675:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 11.40/2.46 % (1807029)Instruction limit reached!
% 11.40/2.46 % (1807029)------------------------------
% 11.40/2.46 % (1807029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807029)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807029)Termination reason: Instruction limit
% 13.13/2.72 % (1807029)Termination phase: Saturation
% 13.13/2.72 % (1807029)Time elapsed: 0.042 s
% 13.13/2.72 % (1807029)Peak memory usage: 112 MB
% 13.13/2.72 % (1807029)Instructions burned: 13 (million)
% 13.13/2.72 % (1807019)Instruction limit reached!
% 13.13/2.72 % (1807019)------------------------------
% 13.13/2.72 % (1807019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807019)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807019)Termination reason: Instruction limit
% 13.13/2.72 % (1807019)Termination phase: Saturation
% 13.13/2.72 % (1807019)Time elapsed: 0.248 s
% 13.13/2.72 % (1807019)Peak memory usage: 92 MB
% 13.13/2.72 % (1807019)Instructions burned: 370 (million)
% 13.13/2.72 % (1807037)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=1005639423:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 13.13/2.72 % (1807033)Refutation not found, incomplete strategy
% 13.13/2.72 % (1807033)------------------------------
% 13.13/2.72 % (1807033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807033)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807033)Termination reason: Refutation not found, incomplete strategy
% 13.13/2.72 % (1807033)Time elapsed: 0.083 s
% 13.13/2.72 % (1807033)Peak memory usage: 116 MB
% 13.13/2.72 % (1807033)Instructions burned: 41 (million)
% 13.13/2.72 % (1807040)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=374807012:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 13.13/2.72 % (1807035)Instruction limit reached!
% 13.13/2.72 % (1807035)------------------------------
% 13.13/2.72 % (1807035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807035)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807035)Termination reason: Instruction limit
% 13.13/2.72 % (1807035)Termination phase: Saturation
% 13.13/2.72 % (1807035)Time elapsed: 0.114 s
% 13.13/2.72 % (1807035)Peak memory usage: 133 MB
% 13.13/2.72 % (1807035)Instructions burned: 71 (million)
% 13.13/2.72 % (1807037)Instruction limit reached!
% 13.13/2.72 % (1807037)------------------------------
% 13.13/2.72 % (1807037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807037)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807037)Termination reason: Instruction limit
% 13.13/2.72 % (1807037)Termination phase: Saturation
% 13.13/2.72 % (1807037)Time elapsed: 0.059 s
% 13.13/2.72 % (1807037)Peak memory usage: 90 MB
% 13.13/2.72 % (1807037)Instructions burned: 75 (million)
% 13.13/2.72 % (1807045)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1370144358:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 13.13/2.72 % (1807046)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=179728326:i=131:rtra=on_2987 on theBenchmark for (2987ds/131Mi)
% 13.13/2.72 % (1807040)Instruction limit reached!
% 13.13/2.72 % (1807040)------------------------------
% 13.13/2.72 % (1807040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.13/2.72 % (1807040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.13/2.72 % (1807040)CaDiCaL version: 2.1.3
% 13.13/2.72 % (1807040)Termination reason: Instruction limit
% 13.13/2.72 % (1807040)Termination phase: Saturation
% 13.13/2.72 % (1807040)Time elapsed: 0.114 s
% 13.13/2.72 % (1807040)Peak memory usage: 91 MB
% 13.13/2.72 % (1807040)Instructions burned: 296 (million)
% 13.13/2.72 % (1807049)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2644883060:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi)
% 13.13/2.72 % (1807052)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2174567351:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi)
% 13.13/2.72 % (1807045)Instruction limit reached!
% 14.92/3.02 % (1807045)------------------------------
% 14.92/3.02 % (1807045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.02 % (1807045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.02 % (1807045)CaDiCaL version: 2.1.3
% 14.92/3.02 % (1807045)Termination reason: Instruction limit
% 14.92/3.02 % (1807045)Termination phase: Saturation
% 14.92/3.02 % (1807045)Time elapsed: 0.106 s
% 14.92/3.02 % (1807045)Peak memory usage: 117 MB
% 14.92/3.02 % (1807045)Instructions burned: 130 (million)
% 14.92/3.02 % (1807049)Instruction limit reached!
% 14.92/3.02 % (1807049)------------------------------
% 14.92/3.02 % (1807049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.02 % (1807049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.02 % (1807049)CaDiCaL version: 2.1.3
% 14.92/3.02 % (1807049)Termination reason: Instruction limit
% 14.92/3.02 % (1807049)Termination phase: Saturation
% 14.92/3.02 % (1807049)Time elapsed: 0.069 s
% 14.92/3.02 % (1807049)Peak memory usage: 134 MB
% 14.92/3.02 % (1807049)Instructions burned: 41 (million)
% 14.92/3.02 % (1807053)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3824047130:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi)
% 14.92/3.02 % (1807033)------------------------------
% 14.92/3.02 % (1807033)------------------------------
% 14.92/3.02 % (1807046)Instruction limit reached!
% 14.92/3.02 % (1807046)------------------------------
% 14.92/3.02 % (1807046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.02 % (1807046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.02 % (1807046)CaDiCaL version: 2.1.3
% 14.92/3.02 % (1807046)Termination reason: Instruction limit
% 14.92/3.02 % (1807046)Termination phase: Saturation
% 14.92/3.02 % (1807046)Time elapsed: 0.136 s
% 14.92/3.02 % (1807046)Peak memory usage: 134 MB
% 14.92/3.02 % (1807046)Instructions burned: 132 (million)
% 14.92/3.02 % (1807056)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2337614718:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 14.92/3.02 % (1807056)Instruction limit reached!
% 14.92/3.02 % (1807056)------------------------------
% 14.92/3.03 % (1807056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807056)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807056)Termination reason: Instruction limit
% 14.92/3.03 % (1807056)Termination phase: Saturation
% 14.92/3.03 % (1807056)Time elapsed: 0.059 s
% 14.92/3.03 % (1807056)Peak memory usage: 117 MB
% 14.92/3.03 % (1807056)Instructions burned: 133 (million)
% 14.92/3.03 % (1807081)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=3437001795:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2984 on theBenchmark for (2984ds/259Mi)
% 14.92/3.03 % (1807083)dis+10_1_si=on:random_seed=1678495644:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi)
% 14.92/3.03 % (1807052)Instruction limit reached!
% 14.92/3.03 % (1807052)------------------------------
% 14.92/3.03 % (1807052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807052)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807052)Termination reason: Instruction limit
% 14.92/3.03 % (1807052)Termination phase: Saturation
% 14.92/3.03 % (1807052)Time elapsed: 0.192 s
% 14.92/3.03 % (1807052)Peak memory usage: 92 MB
% 14.92/3.03 % (1807052)Instructions burned: 308 (million)
% 14.92/3.03 % (1807097)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=566256873:i=383:fsr=off:rtra=on:ev=force_2984 on theBenchmark for (2984ds/383Mi)
% 14.92/3.03 % (1807099)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3420107213:i=141:doe=on:rtra=on_2984 on theBenchmark for (2984ds/141Mi)
% 14.92/3.03 % (1807125)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3777345223:i=65:nm=16:rtra=on_2983 on theBenchmark for (2983ds/65Mi)
% 14.92/3.03 % (1807099)Instruction limit reached!
% 14.92/3.03 % (1807099)------------------------------
% 14.92/3.03 % (1807099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807099)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807099)Termination reason: Instruction limit
% 14.92/3.03 % (1807099)Termination phase: Saturation
% 14.92/3.03 % (1807099)Time elapsed: 0.091 s
% 14.92/3.03 % (1807099)Peak memory usage: 90 MB
% 14.92/3.03 % (1807099)Instructions burned: 142 (million)
% 14.92/3.03 % (1807125)Instruction limit reached!
% 14.92/3.03 % (1807125)------------------------------
% 14.92/3.03 % (1807125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807125)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807125)Termination reason: Instruction limit
% 14.92/3.03 % (1807125)Termination phase: Saturation
% 14.92/3.03 % (1807125)Time elapsed: 0.062 s
% 14.92/3.03 % (1807125)Peak memory usage: 116 MB
% 14.92/3.03 % (1807125)Instructions burned: 66 (million)
% 14.92/3.03 % (1807147)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3607291530:i=121:nm=16:rtra=on_2982 on theBenchmark for (2982ds/121Mi)
% 14.92/3.03 % (1807081)First to succeed.
% 14.92/3.03 % (1807081)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1806800"
% 14.92/3.03 % (1807097)Instruction limit reached!
% 14.92/3.03 % (1807097)------------------------------
% 14.92/3.03 % (1807097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807097)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807097)Termination reason: Instruction limit
% 14.92/3.03 % (1807097)Termination phase: Saturation
% 14.92/3.03 % (1807097)Time elapsed: 0.175 s
% 14.92/3.03 % (1807097)Peak memory usage: 90 MB
% 14.92/3.03 % (1807097)Instructions burned: 384 (million)
% 14.92/3.03 % (1807147)Instruction limit reached!
% 14.92/3.03 % (1807147)------------------------------
% 14.92/3.03 % (1807147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807147)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807147)Termination reason: Instruction limit
% 14.92/3.03 % (1807147)Termination phase: Saturation
% 14.92/3.03 % (1807147)Time elapsed: 0.076 s
% 14.92/3.03 % (1807147)Peak memory usage: 89 MB
% 14.92/3.03 % (1807147)Instructions burned: 121 (million)
% 14.92/3.03 % (1807053)Instruction limit reached!
% 14.92/3.03 % (1807053)------------------------------
% 14.92/3.03 % (1807053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807053)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807053)Termination reason: Instruction limit
% 14.92/3.03 % (1807053)Termination phase: Saturation
% 14.92/3.03 % (1807053)Time elapsed: 0.388 s
% 14.92/3.03 % (1807053)Peak memory usage: 138 MB
% 14.92/3.03 % (1807053)Instructions burned: 601 (million)
% 14.92/3.03 % (1807177)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=572626776:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi)
% 14.92/3.03 % (1807178)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=3591722140:i=39:ins=3:rtra=on_2981 on theBenchmark for (2981ds/39Mi)
% 14.92/3.03 % (1807178)Instruction limit reached!
% 14.92/3.03 % (1807178)------------------------------
% 14.92/3.03 % (1807178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807178)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807178)Termination reason: Instruction limit
% 14.92/3.03 % (1807178)Termination phase: Saturation
% 14.92/3.03 % (1807178)Time elapsed: 0.049 s
% 14.92/3.03 % (1807178)Peak memory usage: 116 MB
% 14.92/3.03 % (1807178)Instructions burned: 39 (million)
% 14.92/3.03 % (1807180)dis+1010_1_to=kbo:si=on:random_seed=1759312676:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2981 on theBenchmark for (2981ds/175Mi)
% 14.92/3.03 % (1807177)Instruction limit reached!
% 14.92/3.03 % (1807177)------------------------------
% 14.92/3.03 % (1807177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807177)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807177)Termination reason: Instruction limit
% 14.92/3.03 % (1807177)Termination phase: Saturation
% 14.92/3.03 % (1807177)Time elapsed: 0.110 s
% 14.92/3.03 % (1807177)Peak memory usage: 117 MB
% 14.92/3.03 % (1807177)Instructions burned: 128 (million)
% 14.92/3.03 % (1807186)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=948905152:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/329Mi)
% 14.92/3.03 % (1807187)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=179355538:s2a=on:i=483:doe=on:nm=32:rtra=on_2980 on theBenchmark for (2980ds/483Mi)
% 14.92/3.03 % (1807083)Instruction limit reached!
% 14.92/3.03 % (1807083)------------------------------
% 14.92/3.03 % (1807083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807083)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807083)Termination reason: Instruction limit
% 14.92/3.03 % (1807083)Termination phase: Saturation
% 14.92/3.03 % (1807083)Time elapsed: 0.418 s
% 14.92/3.03 % (1807083)Peak memory usage: 96 MB
% 14.92/3.03 % (1807083)Instructions burned: 1001 (million)
% 14.92/3.03 % (1807187)Refutation not found, SMT solver inside AVATAR returned Unknown
% 14.92/3.03 % (1807187)------------------------------
% 14.92/3.03 % (1807187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.92/3.03 % (1807187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.92/3.03 % (1807187)CaDiCaL version: 2.1.3
% 14.92/3.03 % (1807187)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 14.92/3.03 % (1807187)Time elapsed: 0.057 s
% 14.92/3.03 % (1807187)Peak memory usage: 132 MB
% 14.92/3.03 % (1807187)Instructions burned: 18 (million)
% 14.92/3.03 % (1807187)------------------------------
% 14.92/3.03 % (1807187)------------------------------
% 14.92/3.03 % (1807081)Refutation found. Thanks to Tanya!
% 14.92/3.03 % SZS status Theorem for theBenchmark
% 14.92/3.03 % SZS output start Proof for theBenchmark
% See solution above
% 15.60/3.13 % (1807081)------------------------------
% 15.60/3.13 % (1807081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.60/3.13 % (1807081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.60/3.13 % (1807081)CaDiCaL version: 2.1.3
% 15.60/3.13 % (1807081)Termination reason: Refutation
% 15.60/3.13 % (1807081)Time elapsed: 0.193 s
% 15.60/3.13 % (1807081)Peak memory usage: 119 MB
% 15.60/3.13 % (1807081)Instructions burned: 261 (million)
% 15.60/3.13 % (1807081)------------------------------
% 15.60/3.13 % (1807081)------------------------------
% 15.60/3.13 % (1806800)Success in time 2.369 s
% 15.60/3.13 % Vampire exiting
%------------------------------------------------------------------------------