%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ANA136_1 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 09:31:12 AM UTC 2026
% Result : Theorem 57.46s 10.76s
% Output : Refutation 72.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 4
% Syntax : Number of formulae : 122 ( 8 unt; 0 typ; 2 def)
% Number of atoms : 724 ( 17 equ)
% Maximal formula atoms : 11 ( 5 avg)
% Number of connectives : 697 ( 95 ~; 520 |; 50 &)
% ( 2 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 8 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 3109 ( 683 atm; 859 fun;1347 num; 220 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 : 7 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 21 ( 6 usr; 8 con; 0-2 aty)
% Number of variables : 220 ( 0 sgn 209 !; 11 ?; 220 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
f: $real > $real ).
tff(func_def_1,type,
a: $real ).
tff(func_def_2,type,
l: $real ).
tff(func_def_11,type,
sK0: $real ).
tff(func_def_12,type,
sK1: $real > $real ).
tff(func_def_13,type,
sK2: $real > $real ).
tff(func_def_14,type,
-1/1: $real > $real ).
tff(func_def_15,type,
-93/1: $real > $real ).
tff(func_def_16,type,
-47/1: $real > $real ).
tff(func_def_17,type,
93/1: $real > $real ).
tff(func_def_25,type,
47/1: $real > $real ).
tff(pred_def_4,type,
sQ3_eqProxy: ( $real * $real ) > $o ).
tff(f1,axiom,
! [X0: $real] :
( $less(0/1,X0)
=> ? [X1: $real] :
( $less(0/1,X1)
& ! [X2: $real] :
( ( ( $greatereq($difference(X2,a),0/1)
=> $less($difference(X2,a),X1) )
& ( ~ $greatereq($difference(X2,a),0/1)
=> $less($uminus($difference(X2,a)),X1) )
& ( X2 != a ) )
=> ( ( ~ $greatereq($difference(f(X2),l),0/1)
=> $less($uminus($difference(f(X2),l)),X0) )
& ( $greatereq($difference(f(X2),l),0/1)
=> $less($difference(f(X2),l),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1) ).
tff(f2,conjecture,
! [X0: $real] :
( $less(0/1,X0)
=> ? [X1: $real] :
( $less(0/1,X1)
& ! [X2: $real] :
( ( ( ~ $greatereq($difference(X2,a),0/1)
=> $less($uminus($difference(X2,a)),X1) )
& ( X2 != a )
& ( $greatereq($difference(X2,a),0/1)
=> $less($difference(X2,a),X1) ) )
=> ( ( $greatereq($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),0/1)
=> $less($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),X0) )
& ( ~ $greatereq($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),0/1)
=> $less($uminus($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l))),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2) ).
tff(f3,negated_conjecture,
~ ! [X0: $real] :
( $less(0/1,X0)
=> ? [X1: $real] :
( $less(0/1,X1)
& ! [X2: $real] :
( ( ( ~ $greatereq($difference(X2,a),0/1)
=> $less($uminus($difference(X2,a)),X1) )
& ( X2 != a )
& ( $greatereq($difference(X2,a),0/1)
=> $less($difference(X2,a),X1) ) )
=> ( ( $greatereq($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),0/1)
=> $less($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),X0) )
& ( ~ $greatereq($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l)),0/1)
=> $less($uminus($difference($product($uminus($quotient(93/1,47/1)),f(X2)),$product($uminus($quotient(93/1,47/1)),l))),X0) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
tff(f4,plain,
~ ! [X0: $real] :
( $less(0/1,X0)
=> ? [X1: $real] :
( ! [X2: $real] :
( ( ( X2 != a )
& ( ~ $less($sum(X2,$uminus(a)),0/1)
=> $less($sum(X2,$uminus(a)),X1) )
& ( $less($sum(X2,$uminus(a)),0/1)
=> $less($uminus($sum(X2,$uminus(a))),X1) ) )
=> ( ( $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1)
=> $less($uminus($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l)))),X0) )
& ( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1)
=> $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),X0) ) ) )
& $less(0/1,X1) ) ),
inference(theory_normalization,[],[f3]) ).
tff(f5,plain,
! [X0: $real] :
( $less(0/1,X0)
=> ? [X1: $real] :
( ! [X2: $real] :
( ( ( ~ $less($sum(X2,$uminus(a)),0/1)
=> $less($sum(X2,$uminus(a)),X1) )
& ( $less($sum(X2,$uminus(a)),0/1)
=> $less($uminus($sum(X2,$uminus(a))),X1) )
& ( X2 != a ) )
=> ( ( $less($sum(f(X2),$uminus(l)),0/1)
=> $less($uminus($sum(f(X2),$uminus(l))),X0) )
& ( ~ $less($sum(f(X2),$uminus(l)),0/1)
=> $less($sum(f(X2),$uminus(l)),X0) ) ) )
& $less(0/1,X1) ) ),
inference(theory_normalization,[],[f1]) ).
tff(f11,plain,
? [X0: $real] :
( ! [X1: $real] :
( ? [X2: $real] :
( ( ( $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1)
& ~ $less($uminus($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l)))),X0) )
| ( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),X0)
& ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1) ) )
& ( X2 != a )
& ( $less($sum(X2,$uminus(a)),X1)
| $less($sum(X2,$uminus(a)),0/1) )
& ( $less($uminus($sum(X2,$uminus(a))),X1)
| ~ $less($sum(X2,$uminus(a)),0/1) ) )
| ~ $less(0/1,X1) )
& $less(0/1,X0) ),
inference(ennf_transformation,[],[f4]) ).
tff(f12,plain,
? [X0: $real] :
( ! [X1: $real] :
( ~ $less(0/1,X1)
| ? [X2: $real] :
( ( $less($uminus($sum(X2,$uminus(a))),X1)
| ~ $less($sum(X2,$uminus(a)),0/1) )
& ( $less($sum(X2,$uminus(a)),X1)
| $less($sum(X2,$uminus(a)),0/1) )
& ( X2 != a )
& ( ( $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1)
& ~ $less($uminus($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l)))),X0) )
| ( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),X0)
& ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(X2)),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1) ) ) ) )
& $less(0/1,X0) ),
inference(flattening,[],[f11]) ).
tff(f13,plain,
! [X0: $real] :
( ? [X1: $real] :
( ! [X2: $real] :
( ( ( ~ $less($sum(f(X2),$uminus(l)),0/1)
| $less($uminus($sum(f(X2),$uminus(l))),X0) )
& ( $less($sum(f(X2),$uminus(l)),0/1)
| $less($sum(f(X2),$uminus(l)),X0) ) )
| ( ~ $less($sum(X2,$uminus(a)),X1)
& ~ $less($sum(X2,$uminus(a)),0/1) )
| ( ~ $less($uminus($sum(X2,$uminus(a))),X1)
& $less($sum(X2,$uminus(a)),0/1) )
| ( a = X2 ) )
& $less(0/1,X1) )
| ~ $less(0/1,X0) ),
inference(ennf_transformation,[],[f5]) ).
tff(f14,plain,
! [X0: $real] :
( ~ $less(0/1,X0)
| ? [X1: $real] :
( $less(0/1,X1)
& ! [X2: $real] :
( ( a = X2 )
| ( ~ $less($sum(X2,$uminus(a)),X1)
& ~ $less($sum(X2,$uminus(a)),0/1) )
| ( ~ $less($uminus($sum(X2,$uminus(a))),X1)
& $less($sum(X2,$uminus(a)),0/1) )
| ( ( ~ $less($sum(f(X2),$uminus(l)),0/1)
| $less($uminus($sum(f(X2),$uminus(l))),X0) )
& ( $less($sum(f(X2),$uminus(l)),0/1)
| $less($sum(f(X2),$uminus(l)),X0) ) ) ) ) ),
inference(flattening,[],[f13]) ).
tff(f15,plain,
( ! [X1: $real] :
( ~ $less(0/1,X1)
| ( ( $less($uminus($sum(sK1(X1),$uminus(a))),X1)
| ~ $less($sum(sK1(X1),$uminus(a)),0/1) )
& ( $less($sum(sK1(X1),$uminus(a)),X1)
| $less($sum(sK1(X1),$uminus(a)),0/1) )
& ( a != sK1(X1) )
& ( ( $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1)
& ~ $less($uminus($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l)))),sK0) )
| ( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),sK0)
& ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1) ) ) ) )
& $less(0/1,sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X2,sK1(X1))],[f12]) ).
tff(f16,plain,
! [X0: $real] :
( ~ $less(0/1,X0)
| ( $less(0/1,sK2(X0))
& ! [X2: $real] :
( ( a = X2 )
| ( ~ $less($sum(X2,$uminus(a)),sK2(X0))
& ~ $less($sum(X2,$uminus(a)),0/1) )
| ( ~ $less($uminus($sum(X2,$uminus(a))),sK2(X0))
& $less($sum(X2,$uminus(a)),0/1) )
| ( ( ~ $less($sum(f(X2),$uminus(l)),0/1)
| $less($uminus($sum(f(X2),$uminus(l))),X0) )
& ( $less($sum(f(X2),$uminus(l)),0/1)
| $less($sum(f(X2),$uminus(l)),X0) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X1,sK2(X0))],[f14]) ).
tff(f17,plain,
$less(0/1,sK0),
inference(cnf_transformation,[],[f15]) ).
tff(f19,plain,
! [X1: $real] :
( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),sK0)
| ~ $less($uminus($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l)))),sK0)
| ~ $less(0/1,X1) ),
inference(cnf_transformation,[],[f15]) ).
tff(f21,plain,
! [X1: $real] :
( ~ $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),sK0)
| ~ $less(0/1,X1)
| $less($sum($product($uminus($quotient(93/1,47/1)),f(sK1(X1))),$uminus($product($uminus($quotient(93/1,47/1)),l))),0/1) ),
inference(cnf_transformation,[],[f15]) ).
tff(f22,plain,
! [X1: $real] :
( ~ $less(0/1,X1)
| ( a != sK1(X1) ) ),
inference(cnf_transformation,[],[f15]) ).
tff(f23,plain,
! [X1: $real] :
( $less($sum(sK1(X1),$uminus(a)),X1)
| ~ $less(0/1,X1)
| $less($sum(sK1(X1),$uminus(a)),0/1) ),
inference(cnf_transformation,[],[f15]) ).
tff(f24,plain,
! [X1: $real] :
( ~ $less(0/1,X1)
| ~ $less($sum(sK1(X1),$uminus(a)),0/1)
| $less($uminus($sum(sK1(X1),$uminus(a))),X1) ),
inference(cnf_transformation,[],[f15]) ).
tff(f27,plain,
! [X2: $real,X0: $real] :
( ~ $less(0/1,X0)
| ( a = X2 )
| ~ $less($sum(X2,$uminus(a)),0/1)
| ~ $less($uminus($sum(X2,$uminus(a))),sK2(X0))
| $less($sum(f(X2),$uminus(l)),0/1)
| $less($sum(f(X2),$uminus(l)),X0) ),
inference(cnf_transformation,[],[f16]) ).
tff(f28,plain,
! [X2: $real,X0: $real] :
( ~ $less(0/1,X0)
| ( a = X2 )
| ~ $less($sum(X2,$uminus(a)),0/1)
| ~ $less($uminus($sum(X2,$uminus(a))),sK2(X0))
| ~ $less($sum(f(X2),$uminus(l)),0/1)
| $less($uminus($sum(f(X2),$uminus(l))),X0) ),
inference(cnf_transformation,[],[f16]) ).
tff(f29,plain,
! [X2: $real,X0: $real] :
( ~ $less(0/1,X0)
| ( a = X2 )
| ~ $less($sum(X2,$uminus(a)),sK2(X0))
| $less($sum(X2,$uminus(a)),0/1)
| $less($sum(f(X2),$uminus(l)),0/1)
| $less($sum(f(X2),$uminus(l)),X0) ),
inference(cnf_transformation,[],[f16]) ).
tff(f30,plain,
! [X2: $real,X0: $real] :
( ~ $less(0/1,X0)
| ( a = X2 )
| ~ $less($sum(X2,$uminus(a)),sK2(X0))
| $less($sum(X2,$uminus(a)),0/1)
| ~ $less($sum(f(X2),$uminus(l)),0/1)
| $less($uminus($sum(f(X2),$uminus(l))),X0) ),
inference(cnf_transformation,[],[f16]) ).
tff(f33,plain,
! [X0: $real] :
( $less(0/1,sK2(X0))
| ~ $less(0/1,X0) ),
inference(cnf_transformation,[],[f16]) ).
tff(f34,definition,
! [X0: $real,X1: $real] :
( sQ3_eqProxy(X0,X1)
<=> ( X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ3_eqProxy])],[equality_proxy_definition]) ).
tff(f38,plain,
! [X1: $real] :
( ~ $less(0/1,X1)
| ~ sQ3_eqProxy(a,sK1(X1)) ),
inference(equality_proxy_replacement,[],[f22,f34]) ).
tff(f41,plain,
! [X2: $real,X0: $real] :
( $less($sum(X2,$uminus(a)),0/1)
| sQ3_eqProxy(a,X2)
| ~ $less($sum(X2,$uminus(a)),sK2(X0))
| ~ $less($sum(f(X2),$uminus(l)),0/1)
| ~ $less(0/1,X0)
| $less($uminus($sum(f(X2),$uminus(l))),X0) ),
inference(equality_proxy_replacement,[],[f30,f34]) ).
tff(f42,plain,
! [X2: $real,X0: $real] :
( sQ3_eqProxy(a,X2)
| $less($sum(f(X2),$uminus(l)),0/1)
| ~ $less($sum(X2,$uminus(a)),sK2(X0))
| $less($sum(f(X2),$uminus(l)),X0)
| $less($sum(X2,$uminus(a)),0/1)
| ~ $less(0/1,X0) ),
inference(equality_proxy_replacement,[],[f29,f34]) ).
tff(f43,plain,
! [X2: $real,X0: $real] :
( ~ $less(0/1,X0)
| sQ3_eqProxy(a,X2)
| ~ $less($sum(X2,$uminus(a)),0/1)
| ~ $less($uminus($sum(X2,$uminus(a))),sK2(X0))
| $less($uminus($sum(f(X2),$uminus(l))),X0)
| ~ $less($sum(f(X2),$uminus(l)),0/1) ),
inference(equality_proxy_replacement,[],[f28,f34]) ).
tff(f44,plain,
! [X2: $real,X0: $real] :
( $less($sum(f(X2),$uminus(l)),0/1)
| ~ $less(0/1,X0)
| ~ $less($uminus($sum(X2,$uminus(a))),sK2(X0))
| $less($sum(f(X2),$uminus(l)),X0)
| ~ $less($sum(X2,$uminus(a)),0/1)
| sQ3_eqProxy(a,X2) ),
inference(equality_proxy_replacement,[],[f27,f34]) ).
tff(f51,plain,
$greater(sK0,0/1),
inference(alasca_normalization,[],[f17]) ).
tff(f52,plain,
! [X0: $real] :
( $greater(sK2(X0),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_normalization,[],[f33]) ).
tff(f53,plain,
! [X2: $real,X0: $real] :
( sQ3_eqProxy(a,X2)
| $greater($sum(l,-1/1(f(X2))),0/1)
| $greater($sum(l,$sum(X0,-1/1(f(X2)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(X2),$sum(a,-1/1(sK2(X0)))),0/1)
| $greatereq($sum(X2,-1/1(a)),0/1) ),
inference(alasca_normalization,[],[f44]) ).
tff(f54,plain,
! [X1: $real] :
( $greatereq($sum(93/1(l),$sum(-47/1(sK0),-93/1(f(sK1(X1))))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1) ),
inference(alasca_normalization,[],[f19]) ).
tff(f56,plain,
! [X2: $real,X0: $real] :
( sQ3_eqProxy(a,X2)
| $greatereq($sum(X2,$sum(-1/1(a),-1/1(sK2(X0)))),0/1)
| $greatereq($sum(-1/1(l),f(X2)),0/1)
| $greater($sum(-1/1(X2),a),0/1)
| $greater($sum(-1/1(l),$sum(X0,f(X2))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_normalization,[],[f41]) ).
tff(f57,plain,
! [X1: $real] :
( $greater($sum(a,$sum(X1,-1/1(sK1(X1)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1) ),
inference(alasca_normalization,[],[f23]) ).
tff(f59,plain,
! [X2: $real,X0: $real] :
( sQ3_eqProxy(a,X2)
| $greater($sum(l,$sum(X0,-1/1(f(X2)))),0/1)
| $greatereq($sum(X2,$sum(-1/1(a),-1/1(sK2(X0)))),0/1)
| $greater($sum(l,-1/1(f(X2))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(X2),a),0/1) ),
inference(alasca_normalization,[],[f42]) ).
tff(f61,plain,
! [X2: $real,X0: $real] :
( sQ3_eqProxy(a,X2)
| $greatereq($sum(-1/1(l),f(X2)),0/1)
| $greatereq($sum(-1/1(X2),$sum(a,-1/1(sK2(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(l),$sum(X0,f(X2))),0/1)
| $greatereq($sum(X2,-1/1(a)),0/1) ),
inference(alasca_normalization,[],[f43]) ).
tff(f62,plain,
! [X1: $real] :
( $greatereq($sum(93/1(l),$sum(-47/1(sK0),-93/1(f(sK1(X1))))),0/1)
| $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f21]) ).
tff(f63,plain,
! [X1: $real] :
( $greater($sum(-1/1(a),$sum(X1,sK1(X1))),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f24]) ).
tff(f67,plain,
! [X1: $real] :
( ~ sQ3_eqProxy(a,sK1(X1))
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f38]) ).
tff(f156,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq($sum(sK1(X0),-1/1(a)),0/1)
| $greater($sum(l,$sum(X1,-1/1(f(sK1(X0))))),0/1)
| $greatereq($sum(-1/1(sK1(X0)),$sum(a,-1/1(sK2(X1)))),0/1) ),
inference(resolution,[],[f53,f67]) ).
tff(f158,plain,
! [X0: $real,X1: $real] :
( $greater($sum(l,$sum(X1,-1/1(f(sK1(X0))))),0/1)
| $greatereq($sum(a,$sum(-1/1(sK1(X0)),-1/1(sK2(X1)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1) ),
inference(alasca_normalization,[],[f156]) ).
tff(f160,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(sK1(X0)),a),0/1)
| $greatereq($sum(-1/1(l),f(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(sK1(X0),$sum(-1/1(a),-1/1(sK2(X1)))),0/1) ),
inference(resolution,[],[f56,f67]) ).
tff(f162,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(a),$sum(sK1(X0),-1/1(sK2(X1)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(l),f(sK1(X0))),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f160]) ).
tff(f164,plain,
! [X0: $real,X1: $real] :
( $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(sK1(X1),$sum(-1/1(a),-1/1(sK2(X0)))),0/1)
| $greater($sum(l,$sum(X0,-1/1(f(sK1(X1))))),0/1)
| $greater($sum(-1/1(sK1(X1)),a),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(resolution,[],[f59,f67]) ).
tff(f166,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(-1/1(a),$sum(-1/1(sK2(X0)),sK1(X1))),0/1)
| $greater($sum(l,$sum(X0,-1/1(f(sK1(X1))))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f164]) ).
tff(f168,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(l),f(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(sK1(X0),-1/1(a)),0/1)
| $greatereq($sum(-1/1(sK1(X0)),$sum(a,-1/1(sK2(X1)))),0/1) ),
inference(resolution,[],[f61,f67]) ).
tff(f171,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(a,$sum(-1/1(sK1(X0)),-1/1(sK2(X1)))),0/1)
| $greatereq($sum(-1/1(l),f(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f168]) ).
tff(f192,plain,
! [X0: $real] :
( $greatereq($sum(-1/1(X0),$sum(a,-1/1(a))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(a),$sum(X0,sK1(X0))),0/1) ),
inference(alasca_inequality_literal_factoring,[],[f63]) ).
tff(f197,plain,
! [X0: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(a),$sum(X0,sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_normalization,[],[f192]) ).
tff(f198,plain,
! [X0: $real] :
( $greater($sum(-1/1(a),$sum(X0,sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f197]) ).
tff(f219,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum($sum(X0,$uminus(a)),$sum($uminus(sK2(X1)),a)),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greater($sum(l,$sum(X1,-1/1(f(sK1(X0))))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_fourier_motzkin,[],[f198,f158]) ).
tff(f222,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greater($sum(l,$sum(X1,-1/1(f(sK1(X0))))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f219]) ).
tff(f223,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(l,$sum(X1,-1/1(f(sK1(X0))))),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1) ),
inference(duplicate_literal_removal,[],[f222]) ).
tff(f236,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(X1),$sum(l,-1/1(l))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),$sum(sK1(X0),-1/1(sK2(X1)))),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1) ),
inference(alasca_inequality_literal_factoring,[],[f162]) ).
tff(f238,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(a),$sum(sK1(X0),-1/1(sK2(X1)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_normalization,[],[f236]) ).
tff(f239,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(a),$sum(sK1(X0),-1/1(sK2(X1)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f238]) ).
tff(f259,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum($sum($uminus(sK2(X1)),$uminus(a)),$sum(X0,a)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1) ),
inference(alasca_fourier_motzkin,[],[f239,f57]) ).
tff(f267,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1) ),
inference(alasca_normalization,[],[f259]) ).
tff(f268,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(duplicate_literal_removal,[],[f267]) ).
tff(f275,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greater($sum($product(93/1,$sum(X0,$uminus(l))),$sum($product(-47/1,sK0),$product(93/1,l))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_fourier_motzkin,[],[f268,f54]) ).
tff(f277,plain,
! [X0: $real,X1: $real] :
( $greater($sum($product(93/1,$sum(X0,$uminus(l))),$sum($product(-47/1,sK0),$product(93/1,l))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(-1/1(l),f(sK1(X1))),0/1) ),
inference(alasca_fourier_motzkin,[],[f268,f62]) ).
tff(f279,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ),
inference(alasca_normalization,[],[f275]) ).
tff(f280,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1) ),
inference(duplicate_literal_removal,[],[f279]) ).
tff(f281,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ),
inference(alasca_normalization,[],[f277]) ).
tff(f282,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ),
inference(duplicate_literal_removal,[],[f281]) ).
tff(f407,definition,
( spl4_6
<=> ! [X0: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
tff(f408,plain,
( ! [X0: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) )
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f407]) ).
tff(f413,plain,
( $greater(-1/1(0/1),0/1)
| $greatereq(-1/1(47/1(sK0)),0/1)
| ~ spl4_6 ),
inference(alasca_viras_quantifier_elimination,[],[f408]) ).
tff(f415,plain,
( $greatereq(-1/1(sK0),0/1)
| ~ spl4_6 ),
inference(alasca_normalization,[],[f413]) ).
tff(f416,plain,
( $greater(0/1,0/1)
| ~ spl4_6 ),
inference(alasca_fourier_motzkin,[],[f51,f415]) ).
tff(f417,plain,
( $false
| ~ spl4_6 ),
inference(alasca_normalization,[],[f416]) ).
tff(f418,plain,
~ spl4_6,
inference(avatar_contradiction_clause,[],[f417]) ).
tff(f499,plain,
! [X0: $real,X1: $real] :
( $greater($sum(l,$sum(X0,-1/1(f(sK1(X1))))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum($sum($uminus(sK2(X0)),$uminus(a)),$sum(X1,a)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_fourier_motzkin,[],[f166,f57]) ).
tff(f534,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greater($sum(l,$sum(X0,-1/1(f(sK1(X1))))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1) ),
inference(alasca_normalization,[],[f499]) ).
tff(f535,plain,
! [X0: $real,X1: $real] :
( $greater($sum(l,$sum(X0,-1/1(f(sK1(X1))))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f534]) ).
tff(f550,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greater($sum($sum($product(-47/1,sK0),$product(-93/1,l)),$product(93/1,$sum(X2,l))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1) ),
inference(alasca_fourier_motzkin,[],[f280,f535]) ).
tff(f555,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1) ),
inference(alasca_normalization,[],[f550]) ).
tff(f556,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1) ),
inference(duplicate_literal_removal,[],[f555]) ).
tff(f557,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1) ),
inference(condensation,[],[f556]) ).
tff(f558,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1) ),
inference(duplicate_literal_removal,[],[f557]) ).
tff(f579,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum($uminus(l),l),0/1) ),
inference(alasca_fourier_motzkin,[],[f282,f558]) ).
tff(f604,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1) ),
inference(alasca_normalization,[],[f579]) ).
tff(f605,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(a,-1/1(sK1(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1) ),
inference(duplicate_literal_removal,[],[f604]) ).
tff(f606,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(a,-1/1(sK1(X1))),0/1) ),
inference(condensation,[],[f605]) ).
tff(f607,plain,
! [X0: $real,X1: $real] :
( $greater($sum(a,-1/1(sK1(X1))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f606]) ).
tff(f778,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq($sum(a,$sum(-1/1(sK1(X0)),-1/1(sK2(X1)))),0/1)
| $greatereq($sum(-1/1(X1),$sum(l,-1/1(l))),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_inequality_literal_factoring,[],[f171]) ).
tff(f807,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(a,$sum(-1/1(sK1(X0)),-1/1(sK2(X1)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1) ),
inference(alasca_normalization,[],[f778]) ).
tff(f808,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(a,$sum(-1/1(sK1(X0)),-1/1(sK2(X1)))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(duplicate_literal_removal,[],[f807]) ).
tff(f836,plain,
! [X0: $real,X1: $real] :
( $greater($sum($sum(X0,$uminus(a)),$sum($uminus(sK2(X1)),a)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_fourier_motzkin,[],[f63,f808]) ).
tff(f844,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1) ),
inference(alasca_normalization,[],[f836]) ).
tff(f845,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(-1/1(l),$sum(X1,f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1) ),
inference(duplicate_literal_removal,[],[f844]) ).
tff(f869,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greater($sum($product(93/1,$sum(X0,$uminus(l))),$sum($product(-47/1,sK0),$product(93/1,l))),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_fourier_motzkin,[],[f845,f54]) ).
tff(f870,plain,
! [X0: $real,X1: $real] :
( $greater($sum($product(93/1,$sum(X0,$uminus(l))),$sum($product(-47/1,sK0),$product(93/1,l))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1) ),
inference(alasca_fourier_motzkin,[],[f845,f62]) ).
tff(f877,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1) ),
inference(alasca_normalization,[],[f869]) ).
tff(f878,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(-93/1(l),$sum(-47/1(sK0),93/1(f(sK1(X1))))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ),
inference(duplicate_literal_removal,[],[f877]) ).
tff(f883,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1) ),
inference(alasca_normalization,[],[f870]) ).
tff(f884,plain,
! [X0: $real,X1: $real] :
( $greater($sum(-1/1(l),f(sK1(X1))),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f883]) ).
tff(f1000,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum($sum($product(-47/1,sK0),$product(-93/1,l)),$product(93/1,$sum(X2,l))),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_fourier_motzkin,[],[f878,f223]) ).
tff(f1010,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f1000]) ).
tff(f1011,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(l,-1/1(f(sK1(X0)))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X2),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1) ),
inference(duplicate_literal_removal,[],[f1010]) ).
tff(f1012,plain,
! [X0: $real,X1: $real] :
( $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(condensation,[],[f1011]) ).
tff(f1013,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(l,-1/1(f(sK1(X1)))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(duplicate_literal_removal,[],[f1012]) ).
tff(f1028,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum($uminus(l),l),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1) ),
inference(alasca_fourier_motzkin,[],[f884,f1013]) ).
tff(f1044,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greatereq(-1/1(X2),0/1) ),
inference(alasca_normalization,[],[f1028]) ).
tff(f1045,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq($sum(-1/1(a),sK1(X0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f1044]) ).
tff(f1046,plain,
! [X0: $real,X1: $real] :
( $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(condensation,[],[f1045]) ).
tff(f1047,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X1,-1/1(sK2(X0))),0/1)
| $greatereq($sum(-1/1(a),sK1(X1)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1) ),
inference(duplicate_literal_removal,[],[f1046]) ).
tff(f1073,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum($uminus(a),a),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X2),0/1) ),
inference(alasca_fourier_motzkin,[],[f1047,f607]) ).
tff(f1094,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(alasca_normalization,[],[f1073]) ).
tff(f1095,plain,
! [X2: $real,X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greatereq(-1/1(X2),0/1)
| $greater($sum(93/1(X2),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(X0,-1/1(sK2(X2))),0/1) ),
inference(duplicate_literal_removal,[],[f1094]) ).
tff(f1096,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(condensation,[],[f1095]) ).
tff(f1097,plain,
! [X0: $real,X1: $real] :
( $greater($sum(X0,-1/1(sK2(X1))),0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1)
| $greatereq(-1/1(X1),0/1) ),
inference(duplicate_literal_removal,[],[f1096]) ).
tff(f1099,plain,
! [X1: $real] :
( $greater(-1/1($sum(-93/1(X1),47/1(sK0))),0/1)
| $greater(-1/1(0/1),0/1)
| $greatereq(-1/1(X1),0/1)
| $greatereq(-1/1(sK2(X1)),0/1) ),
inference(alasca_viras_quantifier_elimination,[],[f1097]) ).
tff(f1100,plain,
! [X1: $real] :
( $greatereq(-1/1(sK2(X1)),0/1)
| $greatereq(-1/1(X1),0/1)
| $greater($sum(93/1(X1),-47/1(sK0)),0/1) ),
inference(alasca_normalization,[],[f1099]) ).
tff(f1101,plain,
! [X0: $real] :
( $greater(0/1,0/1)
| $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_fourier_motzkin,[],[f52,f1100]) ).
tff(f1102,plain,
! [X0: $real] :
( $greatereq(-1/1(X0),0/1)
| $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(alasca_normalization,[],[f1101]) ).
tff(f1103,plain,
! [X0: $real] :
( $greater($sum(93/1(X0),-47/1(sK0)),0/1)
| $greatereq(-1/1(X0),0/1) ),
inference(duplicate_literal_removal,[],[f1102]) ).
tff(f1104,plain,
spl4_6,
inference(avatar_split_clause,[],[f1103,f407]) ).
cnf(s7,plain,
~ spl4_6,
inference(sat_conversion,[],[f418]) ).
cnf(s18,plain,
spl4_6,
inference(sat_conversion,[],[f1104]) ).
cnf(s25,plain,
$false,
inference(rat,[],[s7,s18]) ).
tff(f1105,plain,
$false,
inference(avatar_sat_refutation,[],[s25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA136_1 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.15 % Computer : n020.cluster.edu
% 0.11/0.15 % Model : x86_64 x86_64
% 0.11/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.15 % Memory : 8046.5625MB
% 0.11/0.15 % OS : Linux 6.8.0-71-generic
% 0.11/0.16 % CPULimit : 300
% 0.11/0.16 % WCLimit : 300
% 0.11/0.16 % DateTime : Mon Sep 28 20:40:50 UTC 2026
% 0.11/0.16 % CPUTime :
% 0.11/0.16 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.19 Running first-order theorem proving
% 0.11/0.19 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.99/0.95 % (510602)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.99/0.95 % (510612)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1815115350:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.99/0.95 % (510612)Refutation not found, incomplete strategy
% 2.99/0.95 % (510612)------------------------------
% 2.99/0.95 % (510612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510612)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510612)Termination reason: Refutation not found, incomplete strategy
% 2.99/0.95 % (510612)Time elapsed: 0.020 s
% 2.99/0.95 % (510612)Peak memory usage: 115 MB
% 2.99/0.95 % (510612)Instructions burned: 11 (million)
% 2.99/0.95 % (510611)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2314942576:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.99/0.95 % (510608)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3859876508:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.99/0.95 % (510613)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3569598271:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.99/0.95 % (510607)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4272657968:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.99/0.95 % (510610)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4264833651:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.99/0.95 % (510609)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1991948076:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.99/0.95 % (510611)Instruction limit reached!
% 2.99/0.95 % (510611)------------------------------
% 2.99/0.95 % (510611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510611)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510611)Termination reason: Instruction limit
% 2.99/0.95 % (510611)Termination phase: Saturation
% 2.99/0.95 % (510611)Time elapsed: 0.003 s
% 2.99/0.95 % (510611)Peak memory usage: 88 MB
% 2.99/0.95 % (510611)Instructions burned: 4 (million)
% 2.99/0.95 % (510610)Instruction limit reached!
% 2.99/0.95 % (510610)------------------------------
% 2.99/0.95 % (510610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510610)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510610)Termination reason: Instruction limit
% 2.99/0.95 % (510610)Termination phase: Saturation
% 2.99/0.95 % (510610)Time elapsed: 0.005 s
% 2.99/0.95 % (510610)Peak memory usage: 88 MB
% 2.99/0.95 % (510610)Instructions burned: 9 (million)
% 2.99/0.95 % (510607)Instruction limit reached!
% 2.99/0.95 % (510607)------------------------------
% 2.99/0.95 % (510607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510607)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510607)Termination reason: Instruction limit
% 2.99/0.95 % (510607)Termination phase: Saturation
% 2.99/0.95 % (510607)Time elapsed: 0.029 s
% 2.99/0.95 % (510607)Peak memory usage: 115 MB
% 2.99/0.95 % (510607)Instructions burned: 12 (million)
% 2.99/0.95 % (510608)Refutation not found, incomplete strategy
% 2.99/0.95 % (510608)------------------------------
% 2.99/0.95 % (510608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510608)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510608)Termination reason: Refutation not found, incomplete strategy
% 2.99/0.95 % (510608)Time elapsed: 0.033 s
% 2.99/0.95 % (510608)Peak memory usage: 116 MB
% 2.99/0.95 % (510608)Instructions burned: 14 (million)
% 2.99/0.95 % (510613)Instruction limit reached!
% 2.99/0.95 % (510613)------------------------------
% 2.99/0.95 % (510613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/0.95 % (510613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/0.95 % (510613)CaDiCaL version: 2.1.3
% 2.99/0.95 % (510613)Termination reason: Instruction limit
% 4.74/1.09 % (510613)Termination phase: Saturation
% 4.74/1.09 % (510613)Time elapsed: 0.044 s
% 4.74/1.09 % (510613)Peak memory usage: 116 MB
% 4.74/1.09 % (510613)Instructions burned: 33 (million)
% 4.74/1.09 % (510621)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=684794362:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.74/1.09 % (510622)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=2349726485:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.74/1.09 % (510621)Refutation not found, incomplete strategy
% 4.74/1.09 % (510621)------------------------------
% 4.74/1.09 % (510621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510621)CaDiCaL version: 2.1.3
% 4.74/1.09 % (510621)Termination reason: Refutation not found, incomplete strategy
% 4.74/1.09 % (510621)Time elapsed: 0.008 s
% 4.74/1.09 % (510621)Peak memory usage: 89 MB
% 4.74/1.09 % (510621)Instructions burned: 10 (million)
% 4.74/1.09 % (510612)------------------------------
% 4.74/1.09 % (510612)------------------------------
% 4.74/1.09 % (510622)Instruction limit reached!
% 4.74/1.09 % (510622)------------------------------
% 4.74/1.09 % (510622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510622)CaDiCaL version: 2.1.3
% 4.74/1.09 % (510622)Termination reason: Instruction limit
% 4.74/1.09 % (510622)Termination phase: Saturation
% 4.74/1.09 % (510622)Time elapsed: 0.020 s
% 4.74/1.09 % (510622)Peak memory usage: 88 MB
% 4.74/1.09 % (510622)Instructions burned: 30 (million)
% 4.74/1.09 % (510609)Instruction limit reached!
% 4.74/1.09 % (510609)------------------------------
% 4.74/1.09 % (510609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510609)CaDiCaL version: 2.1.3
% 4.74/1.09 % (510609)Termination reason: Instruction limit
% 4.74/1.09 % (510609)Termination phase: Saturation
% 4.74/1.09 % (510609)Time elapsed: 0.170 s
% 4.74/1.09 % (510609)Peak memory usage: 117 MB
% 4.74/1.09 % (510609)Instructions burned: 202 (million)
% 4.74/1.09 % (510623)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=95840247:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.74/1.09 % (510623)Instruction limit reached!
% 4.74/1.09 % (510623)------------------------------
% 4.74/1.09 % (510623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510623)CaDiCaL version: 2.1.3
% 4.74/1.09 % (510623)Termination reason: Instruction limit
% 4.74/1.09 % (510623)Termination phase: Saturation
% 4.74/1.09 % (510623)Time elapsed: 0.009 s
% 4.74/1.09 % (510623)Peak memory usage: 89 MB
% 4.74/1.09 % (510623)Instructions burned: 18 (million)
% 4.74/1.09 % (510624)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1936305851:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 4.74/1.09 % (510624)Instruction limit reached!
% 4.74/1.09 % (510624)------------------------------
% 4.74/1.09 % (510624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510624)CaDiCaL version: 2.1.3
% 4.74/1.09 % (510624)Termination reason: Instruction limit
% 4.74/1.09 % (510624)Termination phase: Saturation
% 4.74/1.09 % (510624)Time elapsed: 0.017 s
% 4.74/1.09 % (510624)Peak memory usage: 89 MB
% 4.74/1.09 % (510624)Instructions burned: 24 (million)
% 4.74/1.09 % (510627)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=374430673:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.74/1.09 % (510627)Instruction limit reached!
% 4.74/1.09 % (510627)------------------------------
% 4.74/1.09 % (510627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.74/1.09 % (510627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.74/1.09 % (510627)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510627)Termination reason: Instruction limit
% 5.56/1.26 % (510627)Termination phase: Saturation
% 5.56/1.26 % (510627)Time elapsed: 0.009 s
% 5.56/1.26 % (510627)Peak memory usage: 89 MB
% 5.56/1.26 % (510627)Instructions burned: 28 (million)
% 5.56/1.26 % (510608)------------------------------
% 5.56/1.26 % (510608)------------------------------
% 5.56/1.26 % (510628)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4101694040:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.56/1.26 % (510630)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1431985312:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.56/1.26 % (510630)Instruction limit reached!
% 5.56/1.26 % (510630)------------------------------
% 5.56/1.26 % (510630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.26 % (510630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.26 % (510630)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510630)Termination reason: Instruction limit
% 5.56/1.26 % (510630)Termination phase: Saturation
% 5.56/1.26 % (510630)Time elapsed: 0.002 s
% 5.56/1.26 % (510630)Peak memory usage: 88 MB
% 5.56/1.26 % (510630)Instructions burned: 2 (million)
% 5.56/1.26 % (510631)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4156358515:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.56/1.26 % (510635)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=182182488:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.56/1.26 % (510628)Instruction limit reached!
% 5.56/1.26 % (510628)------------------------------
% 5.56/1.26 % (510628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.26 % (510628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.26 % (510628)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510628)Termination reason: Instruction limit
% 5.56/1.26 % (510628)Termination phase: Saturation
% 5.56/1.26 % (510628)Time elapsed: 0.042 s
% 5.56/1.26 % (510628)Peak memory usage: 88 MB
% 5.56/1.26 % (510628)Instructions burned: 85 (million)
% 5.56/1.26 % (510633)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3071515841:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.56/1.26 % (510633)Instruction limit reached!
% 5.56/1.26 % (510633)------------------------------
% 5.56/1.26 % (510633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.26 % (510633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.26 % (510633)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510633)Termination reason: Instruction limit
% 5.56/1.26 % (510633)Termination phase: Saturation
% 5.56/1.26 % (510633)Time elapsed: 0.003 s
% 5.56/1.26 % (510633)Peak memory usage: 88 MB
% 5.56/1.26 % (510633)Instructions burned: 4 (million)
% 5.56/1.26 % (510631)Refutation not found, incomplete strategy
% 5.56/1.26 % (510631)------------------------------
% 5.56/1.26 % (510631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.26 % (510631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.26 % (510631)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510631)Termination reason: Refutation not found, incomplete strategy
% 5.56/1.26 % (510631)Time elapsed: 0.032 s
% 5.56/1.26 % (510631)Peak memory usage: 89 MB
% 5.56/1.26 % (510631)Instructions burned: 50 (million)
% 5.56/1.26 % (510635)Instruction limit reached!
% 5.56/1.26 % (510635)------------------------------
% 5.56/1.26 % (510635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.26 % (510635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.26 % (510635)CaDiCaL version: 2.1.3
% 5.56/1.26 % (510635)Termination reason: Instruction limit
% 5.56/1.26 % (510635)Termination phase: Saturation
% 5.56/1.26 % (510635)Time elapsed: 0.050 s
% 5.56/1.26 % (510635)Peak memory usage: 133 MB
% 5.56/1.26 % (510635)Instructions burned: 68 (million)
% 5.56/1.26 % (510621)------------------------------
% 5.56/1.26 % (510621)------------------------------
% 5.56/1.26 % (510637)lrs+10_1_thi=all:si=on:fd=off:random_seed=1193914950:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 5.56/1.26 % (510640)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=2260318462:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 6.69/1.47 % (510640)Instruction limit reached!
% 6.69/1.47 % (510640)------------------------------
% 6.69/1.47 % (510640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510640)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510640)Termination reason: Instruction limit
% 6.69/1.47 % (510640)Termination phase: Saturation
% 6.69/1.47 % (510640)Time elapsed: 0.006 s
% 6.69/1.47 % (510640)Peak memory usage: 88 MB
% 6.69/1.47 % (510640)Instructions burned: 9 (million)
% 6.69/1.47 % (510642)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3320325861:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 6.69/1.47 % (510642)Instruction limit reached!
% 6.69/1.47 % (510642)------------------------------
% 6.69/1.47 % (510642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510642)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510642)Termination reason: Instruction limit
% 6.69/1.47 % (510642)Termination phase: Saturation
% 6.69/1.47 % (510642)Time elapsed: 0.002 s
% 6.69/1.47 % (510642)Peak memory usage: 88 MB
% 6.69/1.47 % (510642)Instructions burned: 2 (million)
% 6.69/1.47 % (510644)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1037036263:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.69/1.47 % (510645)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2575380984:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 6.69/1.47 % (510644)Instruction limit reached!
% 6.69/1.47 % (510644)------------------------------
% 6.69/1.47 % (510644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510644)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510644)Termination reason: Instruction limit
% 6.69/1.47 % (510644)Termination phase: Saturation
% 6.69/1.47 % (510644)Time elapsed: 0.002 s
% 6.69/1.47 % (510644)Peak memory usage: 88 MB
% 6.69/1.47 % (510644)Instructions burned: 3 (million)
% 6.69/1.47 % (510637)Instruction limit reached!
% 6.69/1.47 % (510637)------------------------------
% 6.69/1.47 % (510637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510637)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510637)Termination reason: Instruction limit
% 6.69/1.47 % (510637)Termination phase: Saturation
% 6.69/1.47 % (510637)Time elapsed: 0.063 s
% 6.69/1.47 % (510637)Peak memory usage: 116 MB
% 6.69/1.47 % (510637)Instructions burned: 53 (million)
% 6.69/1.47 % (510646)dis+10_1_si=on:random_seed=353759154:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.69/1.47 % (510646)Instruction limit reached!
% 6.69/1.47 % (510646)------------------------------
% 6.69/1.47 % (510646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510646)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510646)Termination reason: Instruction limit
% 6.69/1.47 % (510646)Termination phase: Saturation
% 6.69/1.47 % (510646)Time elapsed: 0.007 s
% 6.69/1.47 % (510646)Peak memory usage: 88 MB
% 6.69/1.47 % (510646)Instructions burned: 10 (million)
% 6.69/1.47 % (510645)Instruction limit reached!
% 6.69/1.47 % (510645)------------------------------
% 6.69/1.47 % (510645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510645)CaDiCaL version: 2.1.3
% 6.69/1.47 % (510645)Termination reason: Instruction limit
% 6.69/1.47 % (510645)Termination phase: Saturation
% 6.69/1.47 % (510645)Time elapsed: 0.060 s
% 6.69/1.47 % (510645)Peak memory usage: 117 MB
% 6.69/1.47 % (510645)Instructions burned: 127 (million)
% 6.69/1.47 % (510649)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2475334973:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.69/1.47 % (510649)Refutation not found, incomplete strategy
% 6.69/1.47 % (510649)------------------------------
% 6.69/1.47 % (510649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.69/1.47 % (510649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.69/1.47 % (510649)CaDiCaL version: 2.1.3
% 8.65/1.72 % (510649)Termination reason: Refutation not found, incomplete strategy
% 8.65/1.72 % (510649)Time elapsed: 0.004 s
% 8.65/1.72 % (510649)Peak memory usage: 89 MB
% 8.65/1.72 % (510649)Instructions burned: 5 (million)
% 8.65/1.72 % (510651)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2041046708: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/1.72 % (510631)------------------------------
% 8.65/1.72 % (510631)------------------------------
% 8.65/1.72 % (510651)Instruction limit reached!
% 8.65/1.72 % (510651)------------------------------
% 8.65/1.72 % (510651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/1.72 % (510651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/1.72 % (510651)CaDiCaL version: 2.1.3
% 8.65/1.72 % (510651)Termination reason: Instruction limit
% 8.65/1.72 % (510651)Termination phase: Saturation
% 8.65/1.72 % (510651)Time elapsed: 0.028 s
% 8.65/1.72 % (510651)Peak memory usage: 89 MB
% 8.65/1.72 % (510651)Instructions burned: 36 (million)
% 8.65/1.72 % (510654)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1803366737:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 8.65/1.72 % (510654)Instruction limit reached!
% 8.65/1.72 % (510654)------------------------------
% 8.65/1.72 % (510654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/1.72 % (510654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/1.72 % (510654)CaDiCaL version: 2.1.3
% 8.65/1.72 % (510654)Termination reason: Instruction limit
% 8.65/1.72 % (510654)Termination phase: Saturation
% 8.65/1.72 % (510654)Time elapsed: 0.002 s
% 8.65/1.72 % (510654)Peak memory usage: 88 MB
% 8.65/1.72 % (510654)Instructions burned: 3 (million)
% 8.65/1.72 % (510658)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3268292843:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 8.65/1.72 % (510655)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3331207514:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 8.65/1.72 % (510658)Instruction limit reached!
% 8.65/1.72 % (510658)------------------------------
% 8.65/1.72 % (510658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/1.72 % (510658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/1.72 % (510658)CaDiCaL version: 2.1.3
% 8.65/1.72 % (510658)Termination reason: Instruction limit
% 8.65/1.72 % (510658)Termination phase: Saturation
% 8.65/1.72 % (510658)Time elapsed: 0.018 s
% 8.65/1.72 % (510658)Peak memory usage: 116 MB
% 8.65/1.72 % (510658)Instructions burned: 13 (million)
% 8.65/1.72 % (510655)Instruction limit reached!
% 8.65/1.72 % (510655)------------------------------
% 8.65/1.72 % (510655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/1.72 % (510655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/1.72 % (510655)CaDiCaL version: 2.1.3
% 8.65/1.72 % (510655)Termination reason: Instruction limit
% 8.65/1.72 % (510655)Termination phase: Saturation
% 8.65/1.72 % (510655)Time elapsed: 0.006 s
% 8.65/1.72 % (510655)Peak memory usage: 89 MB
% 8.65/1.72 % (510655)Instructions burned: 8 (million)
% 8.65/1.72 % (510657)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=4092651760:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.65/1.72 % (510661)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2201280640:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 8.65/1.72 % (510668)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=2850292089:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 8.65/1.72 % (510663)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3688764991:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 8.65/1.72 % (510664)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2946842555:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 8.65/1.72 % (510663)Refutation not found, incomplete strategy
% 8.65/1.72 % (510663)------------------------------
% 10.14/2.01 % (510663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510663)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510663)Termination reason: Refutation not found, incomplete strategy
% 10.14/2.01 % (510663)Time elapsed: 0.003 s
% 10.14/2.01 % (510663)Peak memory usage: 88 MB
% 10.14/2.01 % (510663)Instructions burned: 3 (million)
% 10.14/2.01 % (510667)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=1040228815:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.14/2.01 % (510649)------------------------------
% 10.14/2.01 % (510649)------------------------------
% 10.14/2.01 % (510664)Refutation not found, incomplete strategy
% 10.14/2.01 % (510664)------------------------------
% 10.14/2.01 % (510664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510664)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510664)Termination reason: Refutation not found, incomplete strategy
% 10.14/2.01 % (510664)Time elapsed: 0.065 s
% 10.14/2.01 % (510664)Peak memory usage: 133 MB
% 10.14/2.01 % (510664)Instructions burned: 28 (million)
% 10.14/2.01 % (510667)Instruction limit reached!
% 10.14/2.01 % (510667)------------------------------
% 10.14/2.01 % (510667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510667)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510667)Termination reason: Instruction limit
% 10.14/2.01 % (510667)Termination phase: Saturation
% 10.14/2.01 % (510667)Time elapsed: 0.046 s
% 10.14/2.01 % (510667)Peak memory usage: 89 MB
% 10.14/2.01 % (510667)Instructions burned: 77 (million)
% 10.14/2.01 % (510668)Instruction limit reached!
% 10.14/2.01 % (510668)------------------------------
% 10.14/2.01 % (510668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510668)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510668)Termination reason: Instruction limit
% 10.14/2.01 % (510668)Termination phase: Saturation
% 10.14/2.01 % (510668)Time elapsed: 0.100 s
% 10.14/2.01 % (510668)Peak memory usage: 89 MB
% 10.14/2.01 % (510668)Instructions burned: 295 (million)
% 10.14/2.01 % (510657)Instruction limit reached!
% 10.14/2.01 % (510657)------------------------------
% 10.14/2.01 % (510657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510657)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510657)Termination reason: Instruction limit
% 10.14/2.01 % (510657)Termination phase: Saturation
% 10.14/2.01 % (510657)Time elapsed: 0.189 s
% 10.14/2.01 % (510657)Peak memory usage: 91 MB
% 10.14/2.01 % (510657)Instructions burned: 371 (million)
% 10.14/2.01 % (510661)Instruction limit reached!
% 10.14/2.01 % (510661)------------------------------
% 10.14/2.01 % (510661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510661)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510661)Termination reason: Instruction limit
% 10.14/2.01 % (510661)Termination phase: Saturation
% 10.14/2.01 % (510661)Time elapsed: 0.140 s
% 10.14/2.01 % (510661)Peak memory usage: 116 MB
% 10.14/2.01 % (510661)Instructions burned: 228 (million)
% 10.14/2.01 % (510677)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=4054324045:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 10.14/2.01 % (510677)Instruction limit reached!
% 10.14/2.01 % (510677)------------------------------
% 10.14/2.01 % (510677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.14/2.01 % (510677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.14/2.01 % (510677)CaDiCaL version: 2.1.3
% 10.14/2.01 % (510677)Termination reason: Instruction limit
% 10.14/2.01 % (510677)Termination phase: Saturation
% 10.14/2.01 % (510677)Time elapsed: 0.042 s
% 10.14/2.01 % (510677)Peak memory usage: 133 MB
% 10.14/2.01 % (510677)Instructions burned: 42 (million)
% 10.14/2.01 % (510675)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2594164865:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 12.64/2.25 % (510676)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2909372508:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 12.64/2.25 % (510678)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=83725448:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 12.64/2.25 % (510679)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4025804957:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 12.64/2.25 % (510663)------------------------------
% 12.64/2.25 % (510663)------------------------------
% 12.64/2.25 % (510682)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2523969120:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.64/2.25 % (510675)Instruction limit reached!
% 12.64/2.25 % (510675)------------------------------
% 12.64/2.25 % (510675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.64/2.25 % (510675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.64/2.25 % (510675)CaDiCaL version: 2.1.3
% 12.64/2.25 % (510675)Termination reason: Instruction limit
% 12.64/2.25 % (510675)Termination phase: Saturation
% 12.64/2.25 % (510675)Time elapsed: 0.100 s
% 12.64/2.25 % (510675)Peak memory usage: 117 MB
% 12.64/2.25 % (510675)Instructions burned: 132 (million)
% 12.64/2.25 % (510664)------------------------------
% 12.64/2.25 % (510664)------------------------------
% 12.64/2.25 % (510676)Instruction limit reached!
% 12.64/2.25 % (510676)------------------------------
% 12.64/2.25 % (510676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.64/2.25 % (510676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.64/2.25 % (510676)CaDiCaL version: 2.1.3
% 12.64/2.25 % (510676)Termination reason: Instruction limit
% 12.64/2.25 % (510676)Termination phase: Saturation
% 12.64/2.25 % (510676)Time elapsed: 0.128 s
% 12.64/2.25 % (510676)Peak memory usage: 133 MB
% 12.64/2.25 % (510676)Instructions burned: 131 (million)
% 12.64/2.25 % (510682)Instruction limit reached!
% 12.64/2.25 % (510682)------------------------------
% 12.64/2.25 % (510682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.64/2.25 % (510682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.64/2.25 % (510682)CaDiCaL version: 2.1.3
% 12.64/2.25 % (510682)Termination reason: Instruction limit
% 12.64/2.25 % (510682)Termination phase: Saturation
% 12.64/2.25 % (510682)Time elapsed: 0.062 s
% 12.64/2.25 % (510682)Peak memory usage: 117 MB
% 12.64/2.25 % (510682)Instructions burned: 131 (million)
% 12.64/2.25 % (510686)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=2933468119:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi)
% 12.64/2.25 % (510678)Instruction limit reached!
% 12.64/2.25 % (510678)------------------------------
% 12.64/2.25 % (510678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.64/2.25 % (510678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.64/2.25 % (510678)CaDiCaL version: 2.1.3
% 12.64/2.25 % (510678)Termination reason: Instruction limit
% 12.64/2.25 % (510678)Termination phase: Saturation
% 12.64/2.25 % (510678)Time elapsed: 0.181 s
% 12.64/2.25 % (510678)Peak memory usage: 91 MB
% 12.64/2.25 % (510678)Instructions burned: 309 (million)
% 12.64/2.25 % (510689)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1722610443:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.64/2.25 % (510688)dis+10_1_si=on:random_seed=820434755:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 12.64/2.25 % (510691)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2349373850:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 12.64/2.25 % (510689)Refutation not found, incomplete strategy
% 12.64/2.25 % (510689)------------------------------
% 12.64/2.25 % (510689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.64/2.25 % (510689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.64/2.25 % (510689)CaDiCaL version: 2.1.3
% 12.64/2.25 % (510689)Termination reason: Refutation not found, incomplete strategy
% 12.64/2.25 % (510689)Time elapsed: 0.009 s
% 12.64/2.25 % (510689)Peak memory usage: 89 MB
% 14.07/2.58 % (510689)Instructions burned: 15 (million)
% 14.07/2.58 % (510691)Refutation not found, incomplete strategy
% 14.07/2.58 % (510691)------------------------------
% 14.07/2.58 % (510691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.07/2.58 % (510691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.07/2.58 % (510691)CaDiCaL version: 2.1.3
% 14.07/2.58 % (510691)Termination reason: Refutation not found, incomplete strategy
% 14.07/2.58 % (510691)Time elapsed: 0.018 s
% 14.07/2.58 % (510691)Peak memory usage: 115 MB
% 14.07/2.58 % (510691)Instructions burned: 10 (million)
% 14.07/2.58 % (510690)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=737520173:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 14.07/2.58 % (510693)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3371308880:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 14.07/2.58 % (510690)Instruction limit reached!
% 14.07/2.58 % (510690)------------------------------
% 14.07/2.58 % (510690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.07/2.58 % (510690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.07/2.58 % (510690)CaDiCaL version: 2.1.3
% 14.07/2.58 % (510690)Termination reason: Instruction limit
% 14.07/2.58 % (510690)Termination phase: Saturation
% 14.07/2.58 % (510690)Time elapsed: 0.095 s
% 14.07/2.58 % (510690)Peak memory usage: 90 MB
% 14.07/2.58 % (510690)Instructions burned: 141 (million)
% 14.07/2.58 % (510686)Instruction limit reached!
% 14.07/2.58 % (510686)------------------------------
% 14.07/2.58 % (510686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.07/2.58 % (510686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.07/2.58 % (510686)CaDiCaL version: 2.1.3
% 14.07/2.58 % (510686)Termination reason: Instruction limit
% 14.07/2.58 % (510686)Termination phase: Saturation
% 14.07/2.58 % (510686)Time elapsed: 0.190 s
% 14.07/2.58 % (510686)Peak memory usage: 117 MB
% 14.07/2.58 % (510686)Instructions burned: 259 (million)
% 14.07/2.58 % (510679)Instruction limit reached!
% 14.07/2.58 % (510679)------------------------------
% 14.07/2.58 % (510679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.07/2.58 % (510679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.07/2.58 % (510679)CaDiCaL version: 2.1.3
% 14.07/2.58 % (510679)Termination reason: Instruction limit
% 14.07/2.58 % (510679)Termination phase: Saturation
% 14.07/2.58 % (510679)Time elapsed: 0.355 s
% 14.07/2.58 % (510679)Peak memory usage: 135 MB
% 14.07/2.58 % (510679)Instructions burned: 598 (million)
% 14.07/2.58 % (510693)Instruction limit reached!
% 14.07/2.58 % (510693)------------------------------
% 14.07/2.58 % (510693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.07/2.58 % (510693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.07/2.58 % (510693)CaDiCaL version: 2.1.3
% 14.07/2.58 % (510693)Termination reason: Instruction limit
% 14.07/2.58 % (510693)Termination phase: Saturation
% 14.07/2.58 % (510693)Time elapsed: 0.070 s
% 14.07/2.58 % (510693)Peak memory usage: 89 MB
% 14.07/2.58 % (510693)Instructions burned: 121 (million)
% 14.07/2.58 % (510691)------------------------------
% 14.07/2.58 % (510691)------------------------------
% 14.07/2.58 % (510699)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=327654342:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi)
% 14.07/2.58 % (510689)------------------------------
% 14.07/2.58 % (510689)------------------------------
% 14.07/2.58 % (510703)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=871924924:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 14.07/2.58 % (510700)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=911221232:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 14.07/2.58 % (510701)dis+1010_1_to=kbo:si=on:random_seed=602225749:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 14.07/2.58 % (510702)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3156677262:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi)
% 14.07/2.58 % (510703)Refutation not found, incomplete strategy
% 14.07/2.58 % (510703)------------------------------
% 15.77/2.84 % (510703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.84 % (510703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.84 % (510703)CaDiCaL version: 2.1.3
% 15.77/2.84 % (510703)Termination reason: Refutation not found, incomplete strategy
% 15.77/2.84 % (510703)Time elapsed: 0.042 s
% 15.77/2.84 % (510703)Peak memory usage: 133 MB
% 15.77/2.84 % (510703)Instructions burned: 36 (million)
% 15.77/2.84 % (510700)Instruction limit reached!
% 15.77/2.84 % (510700)------------------------------
% 15.77/2.84 % (510700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.84 % (510700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.84 % (510700)CaDiCaL version: 2.1.3
% 15.77/2.84 % (510700)Termination reason: Instruction limit
% 15.77/2.84 % (510700)Termination phase: Saturation
% 15.77/2.84 % (510700)Time elapsed: 0.044 s
% 15.77/2.84 % (510700)Peak memory usage: 115 MB
% 15.77/2.84 % (510700)Instructions burned: 39 (million)
% 15.77/2.84 % (510699)Instruction limit reached!
% 15.77/2.84 % (510699)------------------------------
% 15.77/2.85 % (510699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.85 % (510699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.85 % (510699)CaDiCaL version: 2.1.3
% 15.77/2.85 % (510699)Termination reason: Instruction limit
% 15.77/2.85 % (510699)Termination phase: Saturation
% 15.77/2.85 % (510699)Time elapsed: 0.098 s
% 15.77/2.85 % (510699)Peak memory usage: 118 MB
% 15.77/2.85 % (510699)Instructions burned: 129 (million)
% 15.77/2.85 % (510707)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2409173655:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 15.77/2.85 % (510701)Instruction limit reached!
% 15.77/2.85 % (510701)------------------------------
% 15.77/2.85 % (510701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.85 % (510701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.85 % (510701)CaDiCaL version: 2.1.3
% 15.77/2.85 % (510701)Termination reason: Instruction limit
% 15.77/2.85 % (510701)Termination phase: Saturation
% 15.77/2.85 % (510701)Time elapsed: 0.128 s
% 15.77/2.85 % (510701)Peak memory usage: 91 MB
% 15.77/2.85 % (510701)Instructions burned: 175 (million)
% 15.77/2.85 % (510710)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3154013439:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 15.77/2.85 % (510703)------------------------------
% 15.77/2.85 % (510703)------------------------------
% 15.77/2.85 % (510711)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=921787843:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 15.77/2.85 % (510710)Refutation not found, incomplete strategy
% 15.77/2.85 % (510710)------------------------------
% 15.77/2.85 % (510710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.85 % (510710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.85 % (510710)CaDiCaL version: 2.1.3
% 15.77/2.85 % (510710)Termination reason: Refutation not found, incomplete strategy
% 15.77/2.85 % (510710)Time elapsed: 0.030 s
% 15.77/2.85 % (510710)Peak memory usage: 116 MB
% 15.77/2.85 % (510710)Instructions burned: 9 (million)
% 15.77/2.85 % (510707)Refutation not found, incomplete strategy
% 15.77/2.85 % (510707)------------------------------
% 15.77/2.85 % (510707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.85 % (510707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.85 % (510707)CaDiCaL version: 2.1.3
% 15.77/2.85 % (510707)Termination reason: Refutation not found, incomplete strategy
% 15.77/2.85 % (510707)Time elapsed: 0.106 s
% 15.77/2.85 % (510707)Peak memory usage: 135 MB
% 15.77/2.85 % (510707)Instructions burned: 85 (million)
% 15.77/2.85 % (510702)Instruction limit reached!
% 15.77/2.85 % (510702)------------------------------
% 15.77/2.85 % (510702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.77/2.85 % (510702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.77/2.85 % (510702)CaDiCaL version: 2.1.3
% 15.77/2.85 % (510702)Termination reason: Instruction limit
% 15.77/2.85 % (510702)Termination phase: Saturation
% 15.77/2.85 % (510702)Time elapsed: 0.252 s
% 15.77/2.85 % (510702)Peak memory usage: 118 MB
% 15.77/2.85 % (510702)Instructions burned: 330 (million)
% 15.77/2.85 % (510715)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2183702683:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 18.89/3.12 % (510713)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3610653484:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.89/3.12 % (510688)Instruction limit reached!
% 18.89/3.12 % (510688)------------------------------
% 18.89/3.12 % (510688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.89/3.12 % (510688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.89/3.12 % (510688)CaDiCaL version: 2.1.3
% 18.89/3.12 % (510688)Termination reason: Instruction limit
% 18.89/3.12 % (510688)Termination phase: Saturation
% 18.89/3.12 % (510688)Time elapsed: 0.619 s
% 18.89/3.12 % (510688)Peak memory usage: 94 MB
% 18.89/3.12 % (510688)Instructions burned: 1001 (million)
% 18.89/3.12 % (510711)Instruction limit reached!
% 18.89/3.12 % (510711)------------------------------
% 18.89/3.12 % (510711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.89/3.12 % (510711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.89/3.12 % (510711)CaDiCaL version: 2.1.3
% 18.89/3.12 % (510711)Termination reason: Instruction limit
% 18.89/3.12 % (510711)Termination phase: Saturation
% 18.89/3.12 % (510711)Time elapsed: 0.162 s
% 18.89/3.12 % (510711)Peak memory usage: 90 MB
% 18.89/3.12 % (510711)Instructions burned: 297 (million)
% 18.89/3.12 % (510715)Instruction limit reached!
% 18.89/3.12 % (510715)------------------------------
% 18.89/3.12 % (510715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.89/3.12 % (510715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.89/3.12 % (510715)CaDiCaL version: 2.1.3
% 18.89/3.12 % (510715)Termination reason: Instruction limit
% 18.89/3.12 % (510715)Termination phase: Saturation
% 18.89/3.12 % (510715)Time elapsed: 0.112 s
% 18.89/3.12 % (510715)Peak memory usage: 117 MB
% 18.89/3.12 % (510715)Instructions burned: 281 (million)
% 18.89/3.12 % (510718)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3608312405:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 18.89/3.12 % (510710)------------------------------
% 18.89/3.12 % (510710)------------------------------
% 18.89/3.12 % (510707)------------------------------
% 18.89/3.12 % (510707)------------------------------
% 18.89/3.12 % (510722)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3816351404:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 18.89/3.12 % (510720)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1234923092:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 18.89/3.12 % (510722)Refutation not found, incomplete strategy
% 18.89/3.12 % (510722)------------------------------
% 18.89/3.12 % (510722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.89/3.12 % (510722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.89/3.12 % (510722)CaDiCaL version: 2.1.3
% 18.89/3.12 % (510722)Termination reason: Refutation not found, incomplete strategy
% 18.89/3.12 % (510722)Time elapsed: 0.021 s
% 18.89/3.12 % (510722)Peak memory usage: 116 MB
% 18.89/3.12 % (510722)Instructions burned: 15 (million)
% 18.89/3.12 % (510721)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3968025253:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 18.89/3.12 % (510713)Instruction limit reached!
% 18.89/3.12 % (510713)------------------------------
% 18.89/3.12 % (510713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.89/3.12 % (510713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.89/3.12 % (510713)CaDiCaL version: 2.1.3
% 18.89/3.12 % (510713)Termination reason: Instruction limit
% 18.89/3.12 % (510713)Termination phase: Saturation
% 18.89/3.12 % (510713)Time elapsed: 0.231 s
% 18.89/3.12 % (510713)Peak memory usage: 119 MB
% 18.89/3.12 % (510713)Instructions burned: 328 (million)
% 18.89/3.12 % (510724)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=739747696:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 18.89/3.12 % (510726)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=175818890:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 20.14/3.39 % (510720)Instruction limit reached!
% 20.14/3.39 % (510720)------------------------------
% 20.14/3.39 % (510720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510720)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510720)Termination reason: Instruction limit
% 20.14/3.39 % (510720)Termination phase: Saturation
% 20.14/3.39 % (510720)Time elapsed: 0.148 s
% 20.14/3.39 % (510720)Peak memory usage: 114 MB
% 20.14/3.39 % (510720)Instructions burned: 323 (million)
% 20.14/3.39 % (510726)Refutation not found, incomplete strategy
% 20.14/3.39 % (510726)------------------------------
% 20.14/3.39 % (510726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510726)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510726)Termination reason: Refutation not found, incomplete strategy
% 20.14/3.39 % (510726)Time elapsed: 0.034 s
% 20.14/3.39 % (510726)Peak memory usage: 116 MB
% 20.14/3.39 % (510726)Instructions burned: 14 (million)
% 20.14/3.39 % (510722)------------------------------
% 20.14/3.39 % (510722)------------------------------
% 20.14/3.39 % (510729)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=4164368336:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 20.14/3.39 % (510718)Instruction limit reached!
% 20.14/3.39 % (510718)------------------------------
% 20.14/3.39 % (510718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510718)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510718)Termination reason: Instruction limit
% 20.14/3.39 % (510718)Termination phase: Saturation
% 20.14/3.39 % (510718)Time elapsed: 0.265 s
% 20.14/3.39 % (510718)Peak memory usage: 90 MB
% 20.14/3.39 % (510718)Instructions burned: 485 (million)
% 20.14/3.39 % (510721)Instruction limit reached!
% 20.14/3.39 % (510721)------------------------------
% 20.14/3.39 % (510721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510721)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510721)Termination reason: Instruction limit
% 20.14/3.39 % (510721)Termination phase: Saturation
% 20.14/3.39 % (510721)Time elapsed: 0.228 s
% 20.14/3.39 % (510721)Peak memory usage: 117 MB
% 20.14/3.39 % (510721)Instructions burned: 418 (million)
% 20.14/3.39 % (510773)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2763080368:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 20.14/3.39 % (510763)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2214736134:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 20.14/3.39 % (510783)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=608379812:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 20.14/3.39 % (510724)Instruction limit reached!
% 20.14/3.39 % (510724)------------------------------
% 20.14/3.39 % (510724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510724)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510724)Termination reason: Instruction limit
% 20.14/3.39 % (510724)Termination phase: Saturation
% 20.14/3.39 % (510724)Time elapsed: 0.238 s
% 20.14/3.39 % (510724)Peak memory usage: 134 MB
% 20.14/3.39 % (510724)Instructions burned: 276 (million)
% 20.14/3.39 % (510808)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2118091112:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 20.14/3.39 % (510773)Instruction limit reached!
% 20.14/3.39 % (510773)------------------------------
% 20.14/3.39 % (510773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/3.39 % (510773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.39 % (510773)CaDiCaL version: 2.1.3
% 20.14/3.39 % (510773)Termination reason: Instruction limit
% 20.14/3.39 % (510773)Termination phase: Saturation
% 20.14/3.39 % (510773)Time elapsed: 0.129 s
% 20.14/3.39 % (510773)Peak memory usage: 134 MB
% 23.26/4.03 % (510773)Instructions burned: 337 (million)
% 23.26/4.03 % (510726)------------------------------
% 23.26/4.03 % (510726)------------------------------
% 23.26/4.03 % (510808)Refutation not found, incomplete strategy
% 23.26/4.03 % (510808)------------------------------
% 23.26/4.03 % (510808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510808)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510808)Termination reason: Refutation not found, incomplete strategy
% 23.26/4.03 % (510808)Time elapsed: 0.041 s
% 23.26/4.03 % (510808)Peak memory usage: 116 MB
% 23.26/4.03 % (510808)Instructions burned: 26 (million)
% 23.26/4.03 % (510729)Instruction limit reached!
% 23.26/4.03 % (510729)------------------------------
% 23.26/4.03 % (510729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510729)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510729)Termination reason: Instruction limit
% 23.26/4.03 % (510729)Termination phase: Saturation
% 23.26/4.03 % (510729)Time elapsed: 0.292 s
% 23.26/4.03 % (510729)Peak memory usage: 121 MB
% 23.26/4.03 % (510729)Instructions burned: 388 (million)
% 23.26/4.03 % (510813)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=3325334185:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 23.26/4.03 % (510811)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=641846242:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 23.26/4.03 % (510811)Refutation not found, incomplete strategy
% 23.26/4.03 % (510811)------------------------------
% 23.26/4.03 % (510811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510811)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510811)Termination reason: Refutation not found, incomplete strategy
% 23.26/4.03 % (510811)Time elapsed: 0.032 s
% 23.26/4.03 % (510811)Peak memory usage: 116 MB
% 23.26/4.03 % (510811)Instructions burned: 13 (million)
% 23.26/4.03 % (510783)Instruction limit reached!
% 23.26/4.03 % (510783)------------------------------
% 23.26/4.03 % (510783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510783)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510783)Termination reason: Instruction limit
% 23.26/4.03 % (510783)Termination phase: Saturation
% 23.26/4.03 % (510783)Time elapsed: 0.215 s
% 23.26/4.03 % (510783)Peak memory usage: 91 MB
% 23.26/4.03 % (510783)Instructions burned: 360 (million)
% 23.26/4.03 % (510814)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=158112225:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi)
% 23.26/4.03 % (510813)Instruction limit reached!
% 23.26/4.03 % (510813)------------------------------
% 23.26/4.03 % (510813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510813)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510813)Termination reason: Instruction limit
% 23.26/4.03 % (510813)Termination phase: Saturation
% 23.26/4.03 % (510813)Time elapsed: 0.094 s
% 23.26/4.03 % (510813)Peak memory usage: 117 MB
% 23.26/4.03 % (510813)Instructions burned: 238 (million)
% 23.26/4.03 % (510763)Instruction limit reached!
% 23.26/4.03 % (510763)------------------------------
% 23.26/4.03 % (510763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.26/4.03 % (510763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.26/4.03 % (510763)CaDiCaL version: 2.1.3
% 23.26/4.03 % (510763)Termination reason: Instruction limit
% 23.26/4.03 % (510763)Termination phase: Saturation
% 23.26/4.03 % (510763)Time elapsed: 0.311 s
% 23.26/4.03 % (510763)Peak memory usage: 93 MB
% 23.26/4.03 % (510763)Instructions burned: 514 (million)
% 23.26/4.03 % (510815)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2858553548:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 23.26/4.03 % (510818)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1801977418:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 28.56/4.83 % (510820)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=4271624844:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 28.56/4.83 % (510808)------------------------------
% 28.56/4.83 % (510808)------------------------------
% 28.56/4.83 % (510815)Instruction limit reached!
% 28.56/4.83 % (510815)------------------------------
% 28.56/4.83 % (510815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.56/4.83 % (510815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.56/4.83 % (510815)CaDiCaL version: 2.1.3
% 28.56/4.83 % (510815)Termination reason: Instruction limit
% 28.56/4.83 % (510815)Termination phase: Saturation
% 28.56/4.83 % (510815)Time elapsed: 0.099 s
% 28.56/4.83 % (510815)Peak memory usage: 90 MB
% 28.56/4.83 % (510815)Instructions burned: 146 (million)
% 28.56/4.83 % (510821)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2787489890:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi)
% 28.56/4.83 % (510814)Instruction limit reached!
% 28.56/4.83 % (510814)------------------------------
% 28.56/4.83 % (510814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.56/4.83 % (510814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.56/4.83 % (510814)CaDiCaL version: 2.1.3
% 28.56/4.83 % (510814)Termination reason: Instruction limit
% 28.56/4.83 % (510814)Termination phase: Saturation
% 28.56/4.83 % (510814)Time elapsed: 0.197 s
% 28.56/4.83 % (510814)Peak memory usage: 91 MB
% 28.56/4.83 % (510814)Instructions burned: 274 (million)
% 28.56/4.83 % (510811)------------------------------
% 28.56/4.83 % (510811)------------------------------
% 28.56/4.83 % (510842)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3865266242:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi)
% 28.56/4.83 % (510820)Instruction limit reached!
% 28.56/4.83 % (510820)------------------------------
% 28.56/4.83 % (510820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.56/4.83 % (510820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.56/4.83 % (510820)CaDiCaL version: 2.1.3
% 28.56/4.83 % (510820)Termination reason: Instruction limit
% 28.56/4.83 % (510820)Termination phase: Saturation
% 28.56/4.83 % (510820)Time elapsed: 0.141 s
% 28.56/4.83 % (510820)Peak memory usage: 134 MB
% 28.56/4.83 % (510820)Instructions burned: 277 (million)
% 28.56/4.83 % (510842)Refutation not found, incomplete strategy
% 28.56/4.83 % (510842)------------------------------
% 28.56/4.83 % (510842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.56/4.83 % (510842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.56/4.83 % (510842)CaDiCaL version: 2.1.3
% 28.56/4.83 % (510842)Termination reason: Refutation not found, incomplete strategy
% 28.56/4.83 % (510842)Time elapsed: 0.005 s
% 28.56/4.83 % (510842)Peak memory usage: 89 MB
% 28.56/4.83 % (510842)Instructions burned: 6 (million)
% 28.56/4.83 % (510857)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1147192692:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi)
% 28.56/4.83 % (510857)Refutation not found, incomplete strategy
% 28.56/4.83 % (510857)------------------------------
% 28.56/4.83 % (510857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.56/4.83 % (510857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.56/4.83 % (510857)CaDiCaL version: 2.1.3
% 28.56/4.83 % (510857)Termination reason: Refutation not found, incomplete strategy
% 28.56/4.83 % (510857)Time elapsed: 0.009 s
% 28.56/4.83 % (510857)Peak memory usage: 89 MB
% 28.56/4.83 % (510857)Instructions burned: 13 (million)
% 28.56/4.83 % (510877)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=159946631:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 28.56/4.83 % (510893)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2938071373:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 28.56/4.83 % (510902)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 34.71/5.35 % (510902)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=8395515:i=1090:aac=none:nm=0:rtra=on:rawr=on_2971 on theBenchmark for (2971ds/1090Mi)
% 34.71/5.35 % (510902)Refutation not found, incomplete strategy
% 34.71/5.35 % (510902)------------------------------
% 34.71/5.35 % (510902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.35 % (510902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.35 % (510902)CaDiCaL version: 2.1.3
% 34.71/5.35 % (510902)Termination reason: Refutation not found, incomplete strategy
% 34.71/5.35 % (510902)Time elapsed: 0.029 s
% 34.71/5.35 % (510902)Peak memory usage: 116 MB
% 34.71/5.35 % (510902)Instructions burned: 9 (million)
% 34.71/5.35 % (510893)Refutation not found, incomplete strategy
% 34.71/5.35 % (510893)------------------------------
% 34.71/5.35 % (510893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.35 % (510893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.35 % (510893)CaDiCaL version: 2.1.3
% 34.71/5.35 % (510893)Termination reason: Refutation not found, incomplete strategy
% 34.71/5.35 % (510893)Time elapsed: 0.073 s
% 34.71/5.35 % (510893)Peak memory usage: 133 MB
% 34.71/5.35 % (510893)Instructions burned: 36 (million)
% 34.71/5.35 % (510877)Instruction limit reached!
% 34.71/5.35 % (510877)------------------------------
% 34.71/5.35 % (510877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.35 % (510877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.35 % (510877)CaDiCaL version: 2.1.3
% 34.71/5.35 % (510877)Termination reason: Instruction limit
% 34.71/5.35 % (510877)Termination phase: Saturation
% 34.71/5.35 % (510877)Time elapsed: 0.104 s
% 34.71/5.35 % (510877)Peak memory usage: 115 MB
% 34.71/5.35 % (510877)Instructions burned: 107 (million)
% 34.71/5.35 % (510842)------------------------------
% 34.71/5.35 % (510842)------------------------------
% 34.71/5.35 % (510857)------------------------------
% 34.71/5.35 % (510857)------------------------------
% 34.71/5.35 % (510954)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2003072913:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi)
% 34.71/5.35 % (510979)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2141869578:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi)
% 34.71/5.35 % (510902)------------------------------
% 34.71/5.35 % (510902)------------------------------
% 34.71/5.35 % (510954)Instruction limit reached!
% 34.71/5.35 % (510954)------------------------------
% 34.71/5.35 % (510954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.35 % (510954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.35 % (510954)CaDiCaL version: 2.1.3
% 34.71/5.35 % (510954)Termination reason: Instruction limit
% 34.71/5.35 % (510954)Termination phase: Saturation
% 34.71/5.35 % (510954)Time elapsed: 0.139 s
% 34.71/5.35 % (510954)Peak memory usage: 117 MB
% 34.71/5.35 % (510954)Instructions burned: 132 (million)
% 34.71/5.35 % (510893)------------------------------
% 34.71/5.35 % (510893)------------------------------
% 34.71/5.35 % (510985)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=955864025:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi)
% 34.71/5.35 % (511000)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1914671101:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 34.71/5.35 % (511002)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=556640577:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2965 on theBenchmark for (2965ds/307Mi)
% 34.71/5.35 % (510821)Instruction limit reached!
% 34.71/5.35 % (510821)------------------------------
% 34.71/5.35 % (510821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.71/5.35 % (510821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.71/5.35 % (510821)CaDiCaL version: 2.1.3
% 34.71/5.35 % (510821)Termination reason: Instruction limit
% 34.71/5.35 % (510821)Termination phase: Saturation
% 34.71/5.35 % (510821)Time elapsed: 0.810 s
% 34.71/5.35 % (510821)Peak memory usage: 91 MB
% 34.71/5.35 % (510821)Instructions burned: 1052 (million)
% 34.71/5.35 % (511004)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3875887944:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi)
% 42.27/6.42 % (510979)Instruction limit reached!
% 42.27/6.42 % (510979)------------------------------
% 42.27/6.42 % (510979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (510979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (510979)CaDiCaL version: 2.1.3
% 42.27/6.42 % (510979)Termination reason: Instruction limit
% 42.27/6.42 % (510979)Termination phase: Saturation
% 42.27/6.42 % (510979)Time elapsed: 0.353 s
% 42.27/6.42 % (510979)Peak memory usage: 119 MB
% 42.27/6.42 % (510979)Instructions burned: 312 (million)
% 42.27/6.42 % (511011)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2556361637:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi)
% 42.27/6.42 % (511013)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=3674715860:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi)
% 42.27/6.42 % (510985)Instruction limit reached!
% 42.27/6.42 % (510985)------------------------------
% 42.27/6.42 % (510985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (510985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (510985)CaDiCaL version: 2.1.3
% 42.27/6.42 % (510985)Termination reason: Instruction limit
% 42.27/6.42 % (510985)Termination phase: Saturation
% 42.27/6.42 % (510985)Time elapsed: 0.473 s
% 42.27/6.42 % (510985)Peak memory usage: 91 MB
% 42.27/6.42 % (510985)Instructions burned: 491 (million)
% 42.27/6.42 % (511002)Instruction limit reached!
% 42.27/6.42 % (511002)------------------------------
% 42.27/6.42 % (511002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (511002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (511002)CaDiCaL version: 2.1.3
% 42.27/6.42 % (511002)Termination reason: Instruction limit
% 42.27/6.42 % (511002)Termination phase: Saturation
% 42.27/6.42 % (511002)Time elapsed: 0.339 s
% 42.27/6.42 % (511002)Peak memory usage: 92 MB
% 42.27/6.42 % (511002)Instructions burned: 307 (million)
% 42.27/6.42 % (511000)Instruction limit reached!
% 42.27/6.42 % (511000)------------------------------
% 42.27/6.42 % (511000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (511000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (511000)CaDiCaL version: 2.1.3
% 42.27/6.42 % (511000)Termination reason: Instruction limit
% 42.27/6.42 % (511000)Termination phase: Saturation
% 42.27/6.42 % (511000)Time elapsed: 0.452 s
% 42.27/6.42 % (511000)Peak memory usage: 94 MB
% 42.27/6.42 % (511000)Instructions burned: 836 (million)
% 42.27/6.42 % (511024)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=1427107935:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2961 on theBenchmark for (2961ds/1131Mi)
% 42.27/6.42 % (511031)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=674800749:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2959 on theBenchmark for (2959ds/775Mi)
% 42.27/6.42 % (511028)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=1560875973:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi)
% 42.27/6.42 % (511011)Instruction limit reached!
% 42.27/6.42 % (511011)------------------------------
% 42.27/6.42 % (511011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (511011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (511011)CaDiCaL version: 2.1.3
% 42.27/6.42 % (511011)Termination reason: Instruction limit
% 42.27/6.42 % (511011)Termination phase: Saturation
% 42.27/6.42 % (511011)Time elapsed: 0.632 s
% 42.27/6.42 % (511011)Peak memory usage: 135 MB
% 42.27/6.42 % (511011)Instructions burned: 646 (million)
% 42.27/6.42 % (511028)Instruction limit reached!
% 42.27/6.42 % (511028)------------------------------
% 42.27/6.42 % (511028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.27/6.42 % (511028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (511028)CaDiCaL version: 2.1.3
% 42.27/6.42 % (511028)Termination reason: Instruction limit
% 42.27/6.42 % (511028)Termination phase: Saturation
% 42.27/6.42 % (511028)Time elapsed: 0.282 s
% 42.27/6.42 % (511028)Peak memory usage: 117 MB
% 55.09/8.19 % (511028)Instructions burned: 247 (million)
% 55.09/8.19 % (511004)Instruction limit reached!
% 55.09/8.19 % (511004)------------------------------
% 55.09/8.19 % (511004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511004)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511004)Termination reason: Instruction limit
% 55.09/8.19 % (511004)Termination phase: Saturation
% 55.09/8.19 % (511004)Time elapsed: 0.815 s
% 55.09/8.19 % (511004)Peak memory usage: 121 MB
% 55.09/8.19 % (511004)Instructions burned: 776 (million)
% 55.09/8.19 % (511031)Instruction limit reached!
% 55.09/8.19 % (511031)------------------------------
% 55.09/8.19 % (511031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511031)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511031)Termination reason: Instruction limit
% 55.09/8.19 % (511031)Termination phase: Saturation
% 55.09/8.19 % (511031)Time elapsed: 0.435 s
% 55.09/8.19 % (511031)Peak memory usage: 95 MB
% 55.09/8.19 % (511031)Instructions burned: 776 (million)
% 55.09/8.19 % (511044)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=935142241:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2955 on theBenchmark for (2955ds/273Mi)
% 55.09/8.19 % (511045)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=851068096:i=102:nm=16:rtra=on_2955 on theBenchmark for (2955ds/102Mi)
% 55.09/8.19 % (511046)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3342557638:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2955 on theBenchmark for (2955ds/1094Mi)
% 55.09/8.19 % (511046)Refutation not found, incomplete strategy
% 55.09/8.19 % (511046)------------------------------
% 55.09/8.19 % (511046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511046)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511046)Termination reason: Refutation not found, incomplete strategy
% 55.09/8.19 % (511046)Time elapsed: 0.008 s
% 55.09/8.19 % (511046)Peak memory usage: 88 MB
% 55.09/8.19 % (511046)Instructions burned: 6 (million)
% 55.09/8.19 % (511047)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1690413641:i=6400:doe=on:fsr=off:rtra=on_2953 on theBenchmark for (2953ds/6400Mi)
% 55.09/8.19 % (511045)Instruction limit reached!
% 55.09/8.19 % (511045)------------------------------
% 55.09/8.19 % (511045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511045)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511045)Termination reason: Instruction limit
% 55.09/8.19 % (511045)Termination phase: Saturation
% 55.09/8.19 % (511045)Time elapsed: 0.097 s
% 55.09/8.19 % (511045)Peak memory usage: 89 MB
% 55.09/8.19 % (511045)Instructions burned: 104 (million)
% 55.09/8.19 % (511013)Instruction limit reached!
% 55.09/8.19 % (511013)------------------------------
% 55.09/8.19 % (511013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511013)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511013)Termination reason: Instruction limit
% 55.09/8.19 % (511013)Termination phase: Saturation
% 55.09/8.19 % (511013)Time elapsed: 0.897 s
% 55.09/8.19 % (511013)Peak memory usage: 121 MB
% 55.09/8.19 % (511013)Instructions burned: 784 (million)
% 55.09/8.19 % (511044)Instruction limit reached!
% 55.09/8.19 % (511044)------------------------------
% 55.09/8.19 % (511044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.09/8.19 % (511044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.09/8.19 % (511044)CaDiCaL version: 2.1.3
% 55.09/8.19 % (511044)Termination reason: Instruction limit
% 55.09/8.19 % (511044)Termination phase: Saturation
% 55.09/8.19 % (511044)Time elapsed: 0.290 s
% 55.09/8.19 % (511044)Peak memory usage: 91 MB
% 55.09/8.19 % (511044)Instructions burned: 273 (million)
% 55.09/8.19 % (511055)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=2150317735:i=1846:canc=cautious:fsr=off:rtra=on_2952 on theBenchmark for (2952ds/1846Mi)
% 71.14/10.46 % (511054)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=17124497:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2952 on theBenchmark for (2952ds/868Mi)
% 71.14/10.46 % (511054)Refutation not found, incomplete strategy
% 71.14/10.46 % (511054)------------------------------
% 71.14/10.46 % (511054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.14/10.46 % (511054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.14/10.46 % (511054)CaDiCaL version: 2.1.3
% 71.14/10.46 % (511054)Termination reason: Refutation not found, incomplete strategy
% 71.14/10.46 % (511054)Time elapsed: 0.050 s
% 71.14/10.46 % (511054)Peak memory usage: 116 MB
% 71.14/10.46 % (511054)Instructions burned: 15 (million)
% 71.14/10.46 % (511046)------------------------------
% 71.14/10.46 % (511046)------------------------------
% 71.14/10.46 % (511057)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3005181990:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2950 on theBenchmark for (2950ds/36816Mi)
% 71.14/10.46 % (511024)Instruction limit reached!
% 71.14/10.46 % (511024)------------------------------
% 71.14/10.46 % (511024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.14/10.46 % (511024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.14/10.46 % (511024)CaDiCaL version: 2.1.3
% 71.14/10.46 % (511024)Termination reason: Instruction limit
% 71.14/10.46 % (511024)Termination phase: Saturation
% 71.14/10.46 % (511024)Time elapsed: 1.109 s
% 71.14/10.46 % (511024)Peak memory usage: 121 MB
% 71.14/10.46 % (511024)Instructions burned: 1132 (million)
% 71.14/10.46 % (511061)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4014348179:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2949 on theBenchmark for (2949ds/273Mi)
% 71.14/10.46 % (511054)------------------------------
% 71.14/10.46 % (511054)------------------------------
% 71.14/10.46 % (511063)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1567193853:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2947 on theBenchmark for (2947ds/863Mi)
% 71.14/10.46 % (511063)Refutation not found, incomplete strategy
% 71.14/10.46 % (511063)------------------------------
% 71.14/10.46 % (511063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.14/10.46 % (511063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.14/10.46 % (511063)CaDiCaL version: 2.1.3
% 71.14/10.46 % (511063)Termination reason: Refutation not found, incomplete strategy
% 71.14/10.46 % (511063)Time elapsed: 0.050 s
% 71.14/10.46 % (511063)Peak memory usage: 116 MB
% 71.14/10.46 % (511063)Instructions burned: 15 (million)
% 71.14/10.46 % (511066)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1233309366:i=5811:kws=precedence:nm=0:rtra=on_2945 on theBenchmark for (2945ds/5811Mi)
% 71.14/10.46 % (511061)Instruction limit reached!
% 71.14/10.46 % (511061)------------------------------
% 71.14/10.46 % (511061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.14/10.46 % (511061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.14/10.46 % (511061)CaDiCaL version: 2.1.3
% 71.14/10.46 % (511061)Termination reason: Instruction limit
% 71.14/10.46 % (511061)Termination phase: Saturation
% 71.14/10.46 % (511061)Time elapsed: 0.305 s
% 71.14/10.46 % (511061)Peak memory usage: 91 MB
% 71.14/10.46 % (511061)Instructions burned: 273 (million)
% 71.14/10.46 % (511066)Refutation not found, incomplete strategy
% 71.14/10.46 % (511066)------------------------------
% 71.14/10.46 % (511066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.14/10.46 % (511066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.14/10.46 % (511066)CaDiCaL version: 2.1.3
% 71.14/10.46 % (511066)Termination reason: Refutation not found, incomplete strategy
% 71.14/10.46 % (511066)Time elapsed: 0.052 s
% 71.14/10.46 % (511066)Peak memory usage: 116 MB
% 71.14/10.46 % (511066)Instructions burned: 14 (million)
% 71.14/10.46 % (511068)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3700221799:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2943 on theBenchmark for (2943ds/2216Mi)
% 71.14/10.46 % (511063)------------------------------
% 71.14/10.46 % (511063)------------------------------
% 71.14/10.46 % (511066)------------------------------
% 71.14/10.46 % (511066)------------------------------
% 57.46/10.76 % (511070)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3976026702:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2940 on theBenchmark for (2940ds/801Mi)
% 57.46/10.76 % (511070)Refutation not found, incomplete strategy
% 57.46/10.76 % (511070)------------------------------
% 57.46/10.76 % (511070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511070)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511070)Termination reason: Refutation not found, incomplete strategy
% 57.46/10.76 % (511070)Time elapsed: 0.008 s
% 57.46/10.76 % (511070)Peak memory usage: 89 MB
% 57.46/10.76 % (511070)Instructions burned: 6 (million)
% 57.46/10.76 % (511071)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2987231240:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2939 on theBenchmark for (2939ds/1026Mi)
% 57.46/10.76 % (511071)Refutation not found, incomplete strategy
% 57.46/10.76 % (511071)------------------------------
% 57.46/10.76 % (511071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511071)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511071)Termination reason: Refutation not found, incomplete strategy
% 57.46/10.76 % (511071)Time elapsed: 0.016 s
% 57.46/10.76 % (511071)Peak memory usage: 89 MB
% 57.46/10.76 % (511071)Instructions burned: 13 (million)
% 57.46/10.76 % (511055)Instruction limit reached!
% 57.46/10.76 % (511055)------------------------------
% 57.46/10.76 % (511055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511055)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511055)Termination reason: Instruction limit
% 57.46/10.76 % (511055)Termination phase: Saturation
% 57.46/10.76 % (511055)Time elapsed: 1.556 s
% 57.46/10.76 % (511055)Peak memory usage: 97 MB
% 57.46/10.76 % (511055)Instructions burned: 1846 (million)
% 57.46/10.76 % (511070)------------------------------
% 57.46/10.76 % (511070)------------------------------
% 57.46/10.76 % (511071)------------------------------
% 57.46/10.76 % (511071)------------------------------
% 57.46/10.76 % (511078)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2676163771:i=3509:rtra=on_2934 on theBenchmark for (2934ds/3509Mi)
% 57.46/10.76 % (511079)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3299648377:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2934 on theBenchmark for (2934ds/2127Mi)
% 57.46/10.76 % (510818)Instruction limit reached!
% 57.46/10.76 % (510818)------------------------------
% 57.46/10.76 % (510818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (510818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (510818)CaDiCaL version: 2.1.3
% 57.46/10.76 % (510818)Termination reason: Instruction limit
% 57.46/10.76 % (510818)Termination phase: Saturation
% 57.46/10.76 % (510818)Time elapsed: 4.071 s
% 57.46/10.76 % (510818)Peak memory usage: 121 MB
% 57.46/10.76 % (510818)Instructions burned: 4428 (million)
% 57.46/10.76 % (511080)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2166008227:i=1959:rtra=on:fsd=on:proc=on_2933 on theBenchmark for (2933ds/1959Mi)
% 57.46/10.76 % (511080)Refutation not found, incomplete strategy
% 57.46/10.76 % (511080)------------------------------
% 57.46/10.76 % (511080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511080)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511080)Termination reason: Refutation not found, incomplete strategy
% 57.46/10.76 % (511080)Time elapsed: 0.044 s
% 57.46/10.76 % (511080)Peak memory usage: 116 MB
% 57.46/10.76 % (511080)Instructions burned: 9 (million)
% 57.46/10.76 % (511083)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2222239849:s2a=on:i=3553:nm=0:rtra=on_2931 on theBenchmark for (2931ds/3553Mi)
% 57.46/10.76 % (511080)------------------------------
% 57.46/10.76 % (511080)------------------------------
% 57.46/10.76 % (511088)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1380885074:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2926 on theBenchmark for (2926ds/3201Mi)
% 57.46/10.76 % (511047)Instruction limit reached!
% 57.46/10.76 % (511047)------------------------------
% 57.46/10.76 % (511047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511047)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511047)Termination reason: Instruction limit
% 57.46/10.76 % (511047)Termination phase: Saturation
% 57.46/10.76 % (511047)Time elapsed: 3.111 s
% 57.46/10.76 % (511047)Peak memory usage: 132 MB
% 57.46/10.76 % (511047)Instructions burned: 6401 (million)
% 57.46/10.76 % (511092)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=1408616331:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2921 on theBenchmark for (2921ds/4093Mi)
% 57.46/10.76 % (511068)Instruction limit reached!
% 57.46/10.76 % (511068)------------------------------
% 57.46/10.76 % (511068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511068)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511068)Termination reason: Instruction limit
% 57.46/10.76 % (511068)Termination phase: Saturation
% 57.46/10.76 % (511068)Time elapsed: 2.200 s
% 57.46/10.76 % (511068)Peak memory usage: 126 MB
% 57.46/10.76 % (511068)Instructions burned: 2216 (million)
% 57.46/10.76 % (511094)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=2068258857:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2919 on theBenchmark for (2919ds/21173Mi)
% 57.46/10.76 % (511094)Refutation not found, incomplete strategy
% 57.46/10.76 % (511094)------------------------------
% 57.46/10.76 % (511094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511094)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511094)Termination reason: Refutation not found, incomplete strategy
% 57.46/10.76 % (511094)Time elapsed: 0.189 s
% 57.46/10.76 % (511094)Peak memory usage: 115 MB
% 57.46/10.76 % (511094)Instructions burned: 275 (million)
% 57.46/10.76 % (511079)Instruction limit reached!
% 57.46/10.76 % (511079)------------------------------
% 57.46/10.76 % (511079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511079)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511079)Termination reason: Instruction limit
% 57.46/10.76 % (511079)Termination phase: Saturation
% 57.46/10.76 % (511079)Time elapsed: 2.001 s
% 57.46/10.76 % (511079)Peak memory usage: 100 MB
% 57.46/10.76 % (511079)Instructions burned: 2128 (million)
% 57.46/10.76 % (511094)------------------------------
% 57.46/10.76 % (511094)------------------------------
% 57.46/10.76 % (511108)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2295324164:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2912 on theBenchmark for (2912ds/10544Mi)
% 57.46/10.76 % (511109)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=3201828491:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2911 on theBenchmark for (2911ds/1262Mi)
% 57.46/10.76 % (511088)First to succeed.
% 57.46/10.76 % (511088)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-510602"
% 57.46/10.76 % (511092)Instruction limit reached!
% 57.46/10.76 % (511092)------------------------------
% 57.46/10.76 % (511092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511092)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511092)Termination reason: Instruction limit
% 57.46/10.76 % (511092)Termination phase: Saturation
% 57.46/10.76 % (511092)Time elapsed: 2.065 s
% 57.46/10.76 % (511092)Peak memory usage: 148 MB
% 57.46/10.76 % (511092)Instructions burned: 4094 (million)
% 57.46/10.76 % (511109)Refutation not found, SMT solver inside AVATAR returned Unknown
% 57.46/10.76 % (511109)------------------------------
% 57.46/10.76 % (511109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.46/10.76 % (511109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.46/10.76 % (511109)CaDiCaL version: 2.1.3
% 57.46/10.76 % (511109)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 57.46/10.76 % (511109)Time elapsed: 0.996 s
% 57.46/10.76 % (511109)Peak memory usage: 119 MB
% 57.46/10.76 % (511109)Instructions burned: 989 (million)
% 57.46/10.76 % (511109)------------------------------
% 57.46/10.76 % (511109)------------------------------
% 57.46/10.76 % (511088)Refutation found. Thanks to Tanya!
% 57.46/10.76 % SZS status Theorem for theBenchmark
% 57.46/10.76 % SZS output start Proof for theBenchmark
% See solution above
% 72.07/11.00 % (511088)------------------------------
% 72.07/11.00 % (511088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.07/11.00 % (511088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/11.00 % (511088)CaDiCaL version: 2.1.3
% 72.07/11.00 % (511088)Termination reason: Refutation
% 72.07/11.00 % (511088)Time elapsed: 2.065 s
% 72.07/11.00 % (511088)Peak memory usage: 93 MB
% 72.07/11.00 % (511088)Instructions burned: 2753 (million)
% 72.07/11.00 % (511088)------------------------------
% 72.07/11.00 % (511088)------------------------------
% 72.07/11.00 % (510602)Success in time 10.374 s
% 72.07/11.00 % Vampire exiting
%------------------------------------------------------------------------------