%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX073_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:45:49 PM UTC 2026
% Result : Theorem 90.88s 13.92s
% Output : Refutation 94.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 91
% Syntax : Number of formulae : 449 ( 25 unt; 0 typ; 71 def)
% Number of atoms : 1262 ( 269 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1325 ( 512 ~; 587 |; 133 &)
% ( 76 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 306 ( 50 atm; 17 fun; 182 num; 57 var)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 82 ( 77 usr; 70 prp; 0-2 aty)
% Number of functors : 29 ( 21 usr; 19 con; 0-2 aty)
% Number of variables : 300 ( 226 !; 74 ?; 300 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
general: $tType ).
tff(type_def_6,type,
symbol: $tType ).
tff(func_def_0,type,
f__integer__: $int > general ).
tff(func_def_1,type,
f__symbolic__: symbol > general ).
tff(func_def_2,type,
c__infimum__: general ).
tff(func_def_3,type,
c__supremum__: general ).
tff(func_def_11,type,
sK1: general > general ).
tff(func_def_12,type,
sK2: general > general ).
tff(func_def_13,type,
sK3: general > general ).
tff(func_def_14,type,
sK4: general > general ).
tff(func_def_15,type,
sK5: general ).
tff(func_def_16,type,
sK6: general ).
tff(func_def_17,type,
sK7: general ).
tff(func_def_18,type,
sK8: general ).
tff(func_def_19,type,
sK9: general ).
tff(func_def_20,type,
sK10: general ).
tff(func_def_21,type,
sK11: general > symbol ).
tff(func_def_22,type,
sK12: general > $int ).
tff(func_def_23,type,
sF13: general ).
tff(func_def_24,type,
sF14: general ).
tff(func_def_26,type,
'$inst16': $int ).
tff(func_def_27,type,
'$inst17': $int ).
tff(func_def_33,type,
'$inst18': $int ).
tff(func_def_34,type,
-1: $int > $int ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
hp: general > $o ).
tff(pred_def_9,type,
tp: general > $o ).
tff(pred_def_11,type,
sP0: ( general * general ) > $o ).
tff(f1,axiom,
! [X0: general] :
( ? [X1: $int] : ( X0 = f__integer__(X1) )
<=> p__is_integer__(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__is_integer__def_ax) ).
tff(f2,axiom,
! [X0: general] :
( p__is_symbolic__(X0)
<=> ? [X1: symbol] : ( X0 = f__symbolic__(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__is_symbolic__def_ax) ).
tff(f3,axiom,
! [X0: general] :
( p__is_symbolic__(X0)
| ( X0 = c__supremum__ )
| p__is_integer__(X0)
| ( X0 = c__infimum__ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',general_universe_ax) ).
tff(f4,axiom,
! [X1: $int,X0: $int] :
( ( f__integer__(X0) = f__integer__(X1) )
<=> ( X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f__integer__def_ax) ).
tff(f6,axiom,
! [X0: $int,X1: $int] :
( $lesseq(X0,X1)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f7,axiom,
! [X1: general,X0: general] :
( ( p__less_equal__(X0,X1)
& p__less_equal__(X1,X0) )
=> ( X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetric_ordering_ax) ).
tff(f8,axiom,
! [X1: general,X2: general,X0: general] :
( ( p__less_equal__(X1,X2)
& p__less_equal__(X0,X1) )
=> p__less_equal__(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitive_ordering_ax) ).
tff(f9,axiom,
! [X1: general,X0: general] :
( p__less_equal__(X0,X1)
| p__less_equal__(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',strongly_connected_ordering_ax) ).
tff(f10,axiom,
! [X1: general,X0: general] :
( p__less__(X0,X1)
<=> ( p__less_equal__(X0,X1)
& ( X0 != X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__less__def_ax) ).
tff(f12,axiom,
! [X0: general,X1: general] :
( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
<=> p__greater__(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__greater__def_ax) ).
tff(f13,axiom,
! [X0: $int] : p__less__(c__infimum__,f__integer__(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimal_element_ax) ).
tff(f14,axiom,
! [X1: symbol,X0: $int] : p__less__(f__integer__(X0),f__symbolic__(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',numerals_less_than_symbols_ax) ).
tff(f15,axiom,
! [X0: symbol] : p__less__(f__symbolic__(X0),c__supremum__),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maximal_element_ax) ).
tff(f17,axiom,
! [X0: general] :
( ( ( ( X0 = f__integer__(4) )
& $true )
=> hp(X0) )
& ( ( ( X0 = f__integer__(4) )
& $true )
=> tp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_right_0) ).
tff(f18,conjecture,
! [X1: general,X0: general] :
( ( ( ? [X3: general,X2: general] :
( p__greater__(X2,X3)
& ( X3 = f__integer__(3) )
& ( X2 = X1 ) )
& ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X3 = f__integer__(5) )
& p__less__(X2,X3) )
& ( X0 = X1 ) )
=> hp(X0) )
& ( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X3 = f__integer__(3) )
& p__greater__(X2,X3) )
& ( X0 = X1 )
& ? [X3: general,X2: general] :
( ( X3 = f__integer__(5) )
& ( X2 = X1 )
& p__less__(X2,X3) ) )
=> tp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_left_0) ).
tff(f19,negated_conjecture,
~ ! [X1: general,X0: general] :
( ( ( ? [X3: general,X2: general] :
( p__greater__(X2,X3)
& ( X3 = f__integer__(3) )
& ( X2 = X1 ) )
& ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X3 = f__integer__(5) )
& p__less__(X2,X3) )
& ( X0 = X1 ) )
=> hp(X0) )
& ( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X3 = f__integer__(3) )
& p__greater__(X2,X3) )
& ( X0 = X1 )
& ? [X3: general,X2: general] :
( ( X3 = f__integer__(5) )
& ( X2 = X1 )
& p__less__(X2,X3) ) )
=> tp(X0) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
tff(f20,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,X0)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
inference(theory_normalization,[],[f6]) ).
tff(f21,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f26,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f28,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| ( X0 = X1 )
| $less(X1,X0) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f29,plain,
! [X2: $int,X0: $int,X1: $int] :
( ~ $less(X0,X1)
| $less($sum(X0,X2),$sum(X1,X2)) ),
introduced(definition,[],[tha_order_monotonicity]) ).
tff(f32,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$sum(X0,1))
| ~ $less(X0,X1) ),
introduced(definition,[],[tha_extra_integer_ordering]) ).
tff(f33,plain,
! [X0: general,X2: general,X1: general] :
( ( p__less_equal__(X2,X0)
& p__less_equal__(X0,X1) )
=> p__less_equal__(X2,X1) ),
inference(rectify,[],[f8]) ).
tff(f34,plain,
! [X0: symbol,X1: $int] : p__less__(f__integer__(X1),f__symbolic__(X0)),
inference(rectify,[],[f14]) ).
tff(f35,plain,
! [X1: $int,X0: $int] :
( ( f__integer__(X0) = f__integer__(X1) )
<=> ( X0 = X1 ) ),
inference(rectify,[],[f4]) ).
tff(f36,plain,
! [X0: general] :
( ( ( X0 = f__integer__(4) )
=> tp(X0) )
& ( ( X0 = f__integer__(4) )
=> hp(X0) ) ),
inference(true_and_false_elimination,[],[f17]) ).
tff(f37,plain,
~ ! [X0: general,X1: general] :
( ( ( ( X0 = X1 )
& ? [X9: general,X8: general] :
( ( X0 = X9 )
& ( f__integer__(5) = X8 )
& p__less__(X9,X8) )
& ? [X7: general,X6: general] :
( p__greater__(X6,X7)
& ( f__integer__(3) = X7 )
& ( X0 = X6 ) ) )
=> tp(X1) )
& ( ( ? [X3: general,X2: general] :
( ( X0 = X3 )
& p__greater__(X3,X2)
& ( f__integer__(3) = X2 ) )
& ? [X4: general,X5: general] :
( p__less__(X4,X5)
& ( X0 = X4 )
& ( f__integer__(5) = X5 ) )
& ( X0 = X1 ) )
=> hp(X1) ) ),
inference(rectify,[],[f19]) ).
tff(f38,plain,
! [X0: general,X1: general] :
( p__greater__(X0,X1)
=> ( p__less_equal__(X1,X0)
& ( X0 != X1 ) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
tff(f39,plain,
! [X1: general,X0: general] :
( p__less__(X0,X1)
=> ( p__less_equal__(X0,X1)
& ( X0 != X1 ) ) ),
inference(unused_predicate_definition_removal,[],[f10]) ).
tff(f40,plain,
! [X0: general] :
( p__is_symbolic__(X0)
=> ? [X1: symbol] : ( X0 = f__symbolic__(X1) ) ),
inference(unused_predicate_definition_removal,[],[f2]) ).
tff(f41,plain,
! [X0: general] :
( p__is_integer__(X0)
=> ? [X1: $int] : ( X0 = f__integer__(X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
tff(f42,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| ( p__less_equal__(X1,X0)
& ( X0 != X1 ) ) ),
inference(ennf_transformation,[],[f38]) ).
tff(f43,plain,
! [X0: general] :
( ( hp(X0)
| ( f__integer__(4) != X0 ) )
& ( tp(X0)
| ( f__integer__(4) != X0 ) ) ),
inference(ennf_transformation,[],[f36]) ).
tff(f44,plain,
! [X1: general,X0: general] :
( ( X0 = X1 )
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X0) ),
inference(ennf_transformation,[],[f7]) ).
tff(f45,plain,
! [X1: general,X0: general] :
( ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(flattening,[],[f44]) ).
tff(f47,plain,
! [X0: general] :
( ? [X1: $int] : ( X0 = f__integer__(X1) )
| ~ p__is_integer__(X0) ),
inference(ennf_transformation,[],[f41]) ).
tff(f48,plain,
! [X0: general] :
( ~ p__is_symbolic__(X0)
| ? [X1: symbol] : ( X0 = f__symbolic__(X1) ) ),
inference(ennf_transformation,[],[f40]) ).
tff(f49,plain,
! [X0: general,X2: general,X1: general] :
( p__less_equal__(X2,X1)
| ~ p__less_equal__(X2,X0)
| ~ p__less_equal__(X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
tff(f50,plain,
! [X0: general,X2: general,X1: general] :
( ~ p__less_equal__(X0,X1)
| p__less_equal__(X2,X1)
| ~ p__less_equal__(X2,X0) ),
inference(flattening,[],[f49]) ).
tff(f51,plain,
? [X0: general,X1: general] :
( ( ~ tp(X1)
& ( X0 = X1 )
& ? [X9: general,X8: general] :
( ( X0 = X9 )
& ( f__integer__(5) = X8 )
& p__less__(X9,X8) )
& ? [X7: general,X6: general] :
( p__greater__(X6,X7)
& ( f__integer__(3) = X7 )
& ( X0 = X6 ) ) )
| ( ~ hp(X1)
& ? [X3: general,X2: general] :
( ( X0 = X3 )
& p__greater__(X3,X2)
& ( f__integer__(3) = X2 ) )
& ? [X4: general,X5: general] :
( p__less__(X4,X5)
& ( X0 = X4 )
& ( f__integer__(5) = X5 ) )
& ( X0 = X1 ) ) ),
inference(ennf_transformation,[],[f37]) ).
tff(f52,plain,
? [X0: general,X1: general] :
( ( ~ hp(X1)
& ( X0 = X1 )
& ? [X3: general,X2: general] :
( ( X0 = X3 )
& p__greater__(X3,X2)
& ( f__integer__(3) = X2 ) )
& ? [X4: general,X5: general] :
( p__less__(X4,X5)
& ( X0 = X4 )
& ( f__integer__(5) = X5 ) ) )
| ( ? [X7: general,X6: general] :
( p__greater__(X6,X7)
& ( f__integer__(3) = X7 )
& ( X0 = X6 ) )
& ? [X9: general,X8: general] :
( ( X0 = X9 )
& ( f__integer__(5) = X8 )
& p__less__(X9,X8) )
& ~ tp(X1)
& ( X0 = X1 ) ) ),
inference(flattening,[],[f51]) ).
tff(f53,plain,
! [X0: general,X1: general] :
( ( p__less_equal__(X0,X1)
& ( X0 != X1 ) )
| ~ p__less__(X0,X1) ),
inference(ennf_transformation,[],[f39]) ).
tff(f54,definition,
! [X0: general,X1: general] :
( ( ? [X7: general,X6: general] :
( p__greater__(X6,X7)
& ( f__integer__(3) = X7 )
& ( X0 = X6 ) )
& ? [X9: general,X8: general] :
( ( X0 = X9 )
& ( f__integer__(5) = X8 )
& p__less__(X9,X8) )
& ~ tp(X1)
& ( X0 = X1 ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f55,plain,
? [X0: general,X1: general] :
( ( ~ hp(X1)
& ( X0 = X1 )
& ? [X3: general,X2: general] :
( ( X0 = X3 )
& p__greater__(X3,X2)
& ( f__integer__(3) = X2 ) )
& ? [X4: general,X5: general] :
( p__less__(X4,X5)
& ( X0 = X4 )
& ( f__integer__(5) = X5 ) ) )
| sP0(X0,X1) ),
inference(definition_folding,[],[f52,f54]) ).
tff(f60,plain,
! [X1: $int,X0: $int] :
( ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) )
& ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) ) ),
inference(nnf_transformation,[],[f35]) ).
tff(f61,plain,
! [X0: $int,X1: $int] :
( ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) )
& ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) ) ),
inference(rectify,[],[f60]) ).
tff(f62,plain,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(rectify,[],[f9]) ).
tff(f63,plain,
! [X0: general,X1: general] :
( ( ? [X7: general,X6: general] :
( p__greater__(X6,X7)
& ( f__integer__(3) = X7 )
& ( X0 = X6 ) )
& ? [X9: general,X8: general] :
( ( X0 = X9 )
& ( f__integer__(5) = X8 )
& p__less__(X9,X8) )
& ~ tp(X1)
& ( X0 = X1 ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f54]) ).
tff(f64,plain,
! [X0: general,X1: general] :
( ( ? [X2: general,X3: general] :
( p__greater__(X3,X2)
& ( f__integer__(3) = X2 )
& ( X0 = X3 ) )
& ? [X4: general,X5: general] :
( ( X0 = X4 )
& ( f__integer__(5) = X5 )
& p__less__(X4,X5) )
& ~ tp(X1)
& ( X0 = X1 ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f63]) ).
tff(f65,plain,
! [X0: general,X1: general] :
( ( p__greater__(sK2(X0),sK1(X0))
& ( f__integer__(3) = sK1(X0) )
& ( sK2(X0) = X0 )
& ( sK3(X0) = X0 )
& ( f__integer__(5) = sK4(X0) )
& p__less__(sK3(X0),sK4(X0))
& ~ tp(X1)
& ( X0 = X1 ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X2,sK1(X0)),skolemize(X3,sK2(X0)),skolemize(X4,sK3(X0)),skolemize(X5,sK4(X0))],[f64]) ).
tff(f66,plain,
? [X0: general,X1: general] :
( ( ~ hp(X1)
& ( X0 = X1 )
& ? [X2: general,X3: general] :
( ( X0 = X2 )
& p__greater__(X2,X3)
& ( f__integer__(3) = X3 ) )
& ? [X4: general,X5: general] :
( p__less__(X4,X5)
& ( X0 = X4 )
& ( f__integer__(5) = X5 ) ) )
| sP0(X0,X1) ),
inference(rectify,[],[f55]) ).
tff(f67,plain,
( ( ~ hp(sK6)
& ( sK6 = sK5 )
& ( sK7 = sK5 )
& p__greater__(sK7,sK8)
& ( f__integer__(3) = sK8 )
& p__less__(sK9,sK10)
& ( sK9 = sK5 )
& ( f__integer__(5) = sK10 ) )
| sP0(sK5,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK5),skolemize(X1,sK6),skolemize(X2,sK7),skolemize(X3,sK8),skolemize(X4,sK9),skolemize(X5,sK10)],[f66]) ).
tff(f68,plain,
! [X0: general,X1: general,X2: general] :
( ~ p__less_equal__(X0,X2)
| p__less_equal__(X1,X2)
| ~ p__less_equal__(X1,X0) ),
inference(rectify,[],[f50]) ).
tff(f69,plain,
! [X0: general] :
( ~ p__is_symbolic__(X0)
| ( f__symbolic__(sK11(X0)) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X1,sK11(X0))],[f48]) ).
tff(f70,plain,
! [X0: general,X1: general] :
( ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) ),
inference(rectify,[],[f45]) ).
tff(f71,plain,
! [X0: general] :
( ( f__integer__(sK12(X0)) = X0 )
| ~ p__is_integer__(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X1,sK12(X0))],[f47]) ).
tff(f72,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(X1,X0)
| ~ p__less_equal__(f__integer__(X0),f__integer__(X1)) )
& ( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f73,plain,
! [X0: general,X1: general] :
( ( X0 != X1 )
| ~ p__less__(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tff(f74,plain,
! [X0: general,X1: general] :
( p__less_equal__(X0,X1)
| ~ p__less__(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tff(f75,plain,
! [X0: symbol] : p__less__(f__symbolic__(X0),c__supremum__),
inference(cnf_transformation,[],[f15]) ).
tff(f78,plain,
! [X0: symbol,X1: $int] : p__less__(f__integer__(X1),f__symbolic__(X0)),
inference(cnf_transformation,[],[f34]) ).
tff(f81,plain,
! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f83,plain,
! [X0: general] :
( p__is_symbolic__(X0)
| p__is_integer__(X0)
| ( c__supremum__ = X0 )
| ( c__infimum__ = X0 ) ),
inference(cnf_transformation,[],[f3]) ).
tff(f84,plain,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(cnf_transformation,[],[f62]) ).
tff(f86,plain,
! [X0: general,X1: general] :
( ~ sP0(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f65]) ).
tff(f87,plain,
! [X0: general,X1: general] :
( ~ tp(X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tff(f88,plain,
! [X0: general,X1: general] :
( p__less__(sK3(X0),sK4(X0))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tff(f89,plain,
! [X0: general,X1: general] :
( ~ sP0(X0,X1)
| ( f__integer__(5) = sK4(X0) ) ),
inference(cnf_transformation,[],[f65]) ).
tff(f90,plain,
! [X0: general,X1: general] :
( ( sK3(X0) = X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tff(f91,plain,
! [X0: general,X1: general] :
( ( sK2(X0) = X0 )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tff(f92,plain,
! [X0: general,X1: general] :
( ( f__integer__(3) = sK1(X0) )
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tff(f93,plain,
! [X0: general,X1: general] :
( ~ sP0(X0,X1)
| p__greater__(sK2(X0),sK1(X0)) ),
inference(cnf_transformation,[],[f65]) ).
tff(f94,plain,
( ( f__integer__(5) = sK10 )
| sP0(sK5,sK6) ),
inference(cnf_transformation,[],[f67]) ).
tff(f95,plain,
( sP0(sK5,sK6)
| ( sK9 = sK5 ) ),
inference(cnf_transformation,[],[f67]) ).
tff(f96,plain,
( p__less__(sK9,sK10)
| sP0(sK5,sK6) ),
inference(cnf_transformation,[],[f67]) ).
tff(f97,plain,
( ( f__integer__(3) = sK8 )
| sP0(sK5,sK6) ),
inference(cnf_transformation,[],[f67]) ).
tff(f98,plain,
( sP0(sK5,sK6)
| p__greater__(sK7,sK8) ),
inference(cnf_transformation,[],[f67]) ).
tff(f99,plain,
( sP0(sK5,sK6)
| ( sK7 = sK5 ) ),
inference(cnf_transformation,[],[f67]) ).
tff(f100,plain,
( ( sK6 = sK5 )
| sP0(sK5,sK6) ),
inference(cnf_transformation,[],[f67]) ).
tff(f101,plain,
( ~ hp(sK6)
| sP0(sK5,sK6) ),
inference(cnf_transformation,[],[f67]) ).
tff(f102,plain,
! [X2: general,X0: general,X1: general] :
( p__less_equal__(X1,X2)
| ~ p__less_equal__(X0,X2)
| ~ p__less_equal__(X1,X0) ),
inference(cnf_transformation,[],[f68]) ).
tff(f103,plain,
! [X0: general] :
( tp(X0)
| ( f__integer__(4) != X0 ) ),
inference(cnf_transformation,[],[f43]) ).
tff(f104,plain,
! [X0: general] :
( hp(X0)
| ( f__integer__(4) != X0 ) ),
inference(cnf_transformation,[],[f43]) ).
tff(f105,plain,
! [X0: general] :
( ~ p__is_symbolic__(X0)
| ( f__symbolic__(sK11(X0)) = X0 ) ),
inference(cnf_transformation,[],[f69]) ).
tff(f106,plain,
! [X0: general,X1: general] :
( ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f70]) ).
tff(f107,plain,
! [X0: $int] : p__less__(c__infimum__,f__integer__(X0)),
inference(cnf_transformation,[],[f13]) ).
tff(f108,plain,
! [X0: general] :
( ~ p__is_integer__(X0)
| ( f__integer__(sK12(X0)) = X0 ) ),
inference(cnf_transformation,[],[f71]) ).
tff(f109,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f42]) ).
tff(f110,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| p__less_equal__(X1,X0) ),
inference(cnf_transformation,[],[f42]) ).
tff(f111,plain,
! [X0: $int,X1: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f72]) ).
tff(f112,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X0),f__integer__(X1))
| ~ $less(X1,X0) ),
inference(cnf_transformation,[],[f72]) ).
tff(f113,plain,
! [X1: general] : ~ p__less__(X1,X1),
inference(equality_resolution,[],[f73]) ).
tff(f116,plain,
hp(f__integer__(4)),
inference(equality_resolution,[],[f104]) ).
tff(f117,plain,
tp(f__integer__(4)),
inference(equality_resolution,[],[f103]) ).
tff(f118,plain,
! [X1: general] : ~ p__greater__(X1,X1),
inference(equality_resolution,[],[f109]) ).
tff(f119,definition,
sF13 = f__integer__(3),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f120,plain,
f__integer__(3) = sF13,
inference(reorient_equations,[],[f119]) ).
tff(f121,plain,
( sP0(sK5,sK6)
| ( sK8 = sF13 ) ),
inference(definition_folding,[],[f97,f120]) ).
tff(f122,definition,
sF14 = f__integer__(5),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f123,plain,
f__integer__(5) = sF14,
inference(reorient_equations,[],[f122]) ).
tff(f124,plain,
( ( sF14 = sK10 )
| sP0(sK5,sK6) ),
inference(definition_folding,[],[f94,f123]) ).
tff(f126,definition,
( spl15_1
<=> hp(f__integer__(4)) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
tff(f128,plain,
( hp(f__integer__(4))
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f126]) ).
tff(f129,plain,
spl15_1,
inference(avatar_split_clause,[],[f116,f126]) ).
tff(f131,definition,
( spl15_2
<=> ( f__integer__(5) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
tff(f133,plain,
( ( f__integer__(5) = sF14 )
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f131]) ).
tff(f134,plain,
spl15_2,
inference(avatar_split_clause,[],[f123,f131]) ).
tff(f136,definition,
( spl15_3
<=> tp(f__integer__(4)) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
tff(f138,plain,
( tp(f__integer__(4))
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f136]) ).
tff(f139,plain,
spl15_3,
inference(avatar_split_clause,[],[f117,f136]) ).
tff(f141,definition,
( spl15_4
<=> sP0(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
tff(f143,plain,
( sP0(sK5,sK6)
| ~ spl15_4 ),
inference(avatar_component_clause,[],[f141]) ).
tff(f145,definition,
( spl15_5
<=> p__less__(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
tff(f147,plain,
( p__less__(sK9,sK10)
| ~ spl15_5 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f148,plain,
( spl15_4
| spl15_5 ),
inference(avatar_split_clause,[],[f96,f145,f141]) ).
tff(f150,definition,
( spl15_6
<=> ( sF14 = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
tff(f152,plain,
( ( sF14 = sK10 )
| ~ spl15_6 ),
inference(avatar_component_clause,[],[f150]) ).
tff(f153,plain,
( spl15_4
| spl15_6 ),
inference(avatar_split_clause,[],[f124,f150,f141]) ).
tff(f155,definition,
( spl15_7
<=> ( f__integer__(3) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
tff(f157,plain,
( ( f__integer__(3) = sF13 )
| ~ spl15_7 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f158,plain,
spl15_7,
inference(avatar_split_clause,[],[f120,f155]) ).
tff(f160,definition,
( spl15_8
<=> p__greater__(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
tff(f162,plain,
( p__greater__(sK7,sK8)
| ~ spl15_8 ),
inference(avatar_component_clause,[],[f160]) ).
tff(f163,plain,
( spl15_8
| spl15_4 ),
inference(avatar_split_clause,[],[f98,f141,f160]) ).
tff(f165,definition,
( spl15_9
<=> hp(sK6) ),
introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition]) ).
tff(f168,plain,
( spl15_4
| ~ spl15_9 ),
inference(avatar_split_clause,[],[f101,f165,f141]) ).
tff(f170,definition,
( spl15_10
<=> ( sK7 = sK5 ) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
tff(f172,plain,
( ( sK7 = sK5 )
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f170]) ).
tff(f173,plain,
( spl15_4
| spl15_10 ),
inference(avatar_split_clause,[],[f99,f170,f141]) ).
tff(f175,definition,
( spl15_11
<=> ( sK9 = sK5 ) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
tff(f177,plain,
( ( sK9 = sK5 )
| ~ spl15_11 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f178,plain,
( spl15_11
| spl15_4 ),
inference(avatar_split_clause,[],[f95,f141,f175]) ).
tff(f180,definition,
( spl15_12
<=> ( sK8 = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
tff(f182,plain,
( ( sK8 = sF13 )
| ~ spl15_12 ),
inference(avatar_component_clause,[],[f180]) ).
tff(f183,plain,
( spl15_4
| spl15_12 ),
inference(avatar_split_clause,[],[f121,f180,f141]) ).
tff(f185,definition,
( spl15_13
<=> ( sK6 = sK5 ) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
tff(f187,plain,
( ( sK6 = sK5 )
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f188,plain,
( spl15_4
| spl15_13 ),
inference(avatar_split_clause,[],[f100,f185,f141]) ).
tff(f189,plain,
( ! [X0: general] : ~ sP0(X0,f__integer__(4))
| ~ spl15_3 ),
inference(resolution,[],[f87,f138]) ).
tff(f191,plain,
( ~ p__less_equal__(f__integer__(1),f__integer__(0))
| ~ $less(0,1) ),
inference(instantiation,[],[f112]) ).
tff(f192,plain,
~ p__less_equal__(f__integer__(1),f__integer__(0)),
inference(interpreted_simplification,[],[f191]) ).
tff(f194,definition,
( spl15_14
<=> p__less_equal__(f__integer__(1),f__integer__(0)) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
tff(f196,plain,
( ~ p__less_equal__(f__integer__(1),f__integer__(0))
| spl15_14 ),
inference(avatar_component_clause,[],[f194]) ).
tff(f197,plain,
~ spl15_14,
inference(avatar_split_clause,[],[f192,f194]) ).
tff(f198,plain,
( ! [X0: $int] :
( ~ $less(5,X0)
| ~ p__less_equal__(f__integer__(X0),sF14) )
| ~ spl15_2 ),
inference(superposition,[],[f112,f133]) ).
tff(f215,plain,
( ~ $less(5,6)
| ~ p__less_equal__(f__integer__(6),sF14)
| ~ spl15_2 ),
inference(instantiation,[],[f198]) ).
tff(f216,plain,
( ~ p__less_equal__(f__integer__(6),sF14)
| ~ spl15_2 ),
inference(interpreted_simplification,[],[f215]) ).
tff(f218,definition,
( spl15_17
<=> p__less_equal__(f__integer__(6),sF14) ),
introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition]) ).
tff(f220,plain,
( ~ p__less_equal__(f__integer__(6),sF14)
| spl15_17 ),
inference(avatar_component_clause,[],[f218]) ).
tff(f221,plain,
( ~ spl15_17
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f216,f131,f218]) ).
tff(f236,plain,
( ! [X0: symbol] : p__less__(sF14,f__symbolic__(X0))
| ~ spl15_2 ),
inference(superposition,[],[f78,f133]) ).
tff(f249,plain,
( ~ p__less__(f__integer__(6),sF14)
| spl15_17 ),
inference(resolution,[],[f74,f220]) ).
tff(f274,definition,
( spl15_25
<=> p__less__(f__integer__(6),sF14) ),
introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition]) ).
tff(f277,plain,
( ~ spl15_25
| spl15_17 ),
inference(avatar_split_clause,[],[f249,f218,f274]) ).
tff(f283,plain,
( p__less_equal__(sF14,f__integer__(6))
| spl15_17 ),
inference(resolution,[],[f84,f220]) ).
tff(f287,plain,
! [X0: general] : p__less_equal__(X0,X0),
inference(factoring,[],[f84]) ).
tff(f289,definition,
( spl15_26
<=> p__less_equal__(sF14,f__integer__(6)) ),
introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition]) ).
tff(f291,plain,
( p__less_equal__(sF14,f__integer__(6))
| ~ spl15_26 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f292,plain,
( spl15_26
| spl15_17 ),
inference(avatar_split_clause,[],[f283,f218,f289]) ).
tff(f314,plain,
( ( sK6 = sK5 )
| ~ spl15_4 ),
inference(resolution,[],[f86,f143]) ).
tff(f315,plain,
( spl15_13
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f314,f141,f185]) ).
tff(f316,plain,
( sP0(sK6,sK6)
| ~ spl15_4
| ~ spl15_13 ),
inference(superposition,[],[f143,f187]) ).
tff(f318,definition,
( spl15_31
<=> sP0(sK6,sK6) ),
introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition]) ).
tff(f320,plain,
( sP0(sK6,sK6)
| ~ spl15_31 ),
inference(avatar_component_clause,[],[f318]) ).
tff(f321,plain,
( spl15_31
| ~ spl15_4
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f316,f185,f141,f318]) ).
tff(f327,plain,
! [X0: $int,X1: $int] :
( ~ $less(X0,X1)
| ~ $less(X1,$sum(1,X0)) ),
inference(superposition,[],[f32,f21]) ).
tff(f340,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sF13 )
| ( 3 = X0 ) )
| ~ spl15_7 ),
inference(superposition,[],[f81,f157]) ).
tff(f344,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1)
| ~ sP0(X0,X2)
| p__less__(X0,sK4(X0)) ),
inference(superposition,[],[f88,f90]) ).
tff(f345,plain,
! [X0: general,X1: general] :
( ~ sP0(X0,X1)
| p__less__(X0,sK4(X0)) ),
inference(condensation,[],[f344]) ).
tff(f353,plain,
( ( f__integer__(5) = sK4(sK5) )
| ~ spl15_4 ),
inference(resolution,[],[f89,f143]) ).
tff(f355,plain,
( ( f__integer__(5) = sK4(sK6) )
| ~ spl15_4
| ~ spl15_13 ),
inference(forward_demodulation,[],[f353,f187]) ).
tff(f357,plain,
( ( sF14 = sK4(sK6) )
| ~ spl15_2
| ~ spl15_4
| ~ spl15_13 ),
inference(forward_demodulation,[],[f355,f133]) ).
tff(f359,definition,
( spl15_33
<=> ( sF14 = sK4(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl15_33])],[avatar_definition]) ).
tff(f361,plain,
( ( sF14 = sK4(sK6) )
| ~ spl15_33 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f363,plain,
( spl15_33
| ~ spl15_2
| ~ spl15_4
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f357,f185,f141,f131,f359]) ).
tff(f364,plain,
( ! [X0: general] :
( p__less__(sK3(sK6),sF14)
| ~ sP0(sK6,X0) )
| ~ spl15_33 ),
inference(superposition,[],[f88,f361]) ).
tff(f366,definition,
( spl15_34
<=> ! [X0: general] : ~ sP0(sK6,X0) ),
introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition]) ).
tff(f367,plain,
( ! [X0: general] : ~ sP0(sK6,X0)
| ~ spl15_34 ),
inference(avatar_component_clause,[],[f366]) ).
tff(f369,definition,
( spl15_35
<=> p__less__(sK3(sK6),sF14) ),
introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition]) ).
tff(f371,plain,
( p__less__(sK3(sK6),sF14)
| ~ spl15_35 ),
inference(avatar_component_clause,[],[f369]) ).
tff(f372,plain,
( spl15_34
| spl15_35
| ~ spl15_33 ),
inference(avatar_split_clause,[],[f364,f359,f369,f366]) ).
tff(f373,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| p__less__(sK6,sF14) )
| ~ spl15_35 ),
inference(superposition,[],[f371,f90]) ).
tff(f375,definition,
( spl15_36
<=> p__less__(sK6,sF14) ),
introduced(definition,[new_symbols(definition,[spl15_36])],[avatar_definition]) ).
tff(f377,plain,
( p__less__(sK6,sF14)
| ~ spl15_36 ),
inference(avatar_component_clause,[],[f375]) ).
tff(f378,plain,
( spl15_34
| spl15_36
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f373,f369,f375,f366]) ).
tff(f379,plain,
( p__greater__(sK2(sK5),sK1(sK5))
| ~ spl15_4 ),
inference(resolution,[],[f93,f143]) ).
tff(f381,plain,
( p__greater__(sK2(sK6),sK1(sK6))
| ~ spl15_4
| ~ spl15_13 ),
inference(forward_demodulation,[],[f379,f187]) ).
tff(f383,definition,
( spl15_37
<=> p__greater__(sK2(sK6),sK1(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_37])],[avatar_definition]) ).
tff(f385,plain,
( p__greater__(sK2(sK6),sK1(sK6))
| ~ spl15_37 ),
inference(avatar_component_clause,[],[f383]) ).
tff(f387,plain,
( spl15_37
| ~ spl15_4
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f381,f185,f141,f383]) ).
tff(f388,plain,
( $false
| ~ spl15_31
| ~ spl15_34 ),
inference(resolution,[],[f367,f320]) ).
tff(f389,plain,
( ~ spl15_31
| ~ spl15_34 ),
inference(avatar_contradiction_clause,[],[f388]) ).
tff(f391,plain,
( ( sK9 = sK6 )
| ~ spl15_11
| ~ spl15_13 ),
inference(forward_demodulation,[],[f177,f187]) ).
tff(f392,plain,
( ( sK6 = sK7 )
| ~ spl15_10
| ~ spl15_13 ),
inference(forward_demodulation,[],[f172,f187]) ).
tff(f393,plain,
( p__greater__(sK7,sF13)
| ~ spl15_8
| ~ spl15_12 ),
inference(forward_demodulation,[],[f162,f182]) ).
tff(f395,definition,
( spl15_38
<=> ( sK9 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_38])],[avatar_definition]) ).
tff(f397,plain,
( ( sK9 = sK6 )
| ~ spl15_38 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f398,plain,
( spl15_38
| ~ spl15_11
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f391,f185,f175,f395]) ).
tff(f400,definition,
( spl15_39
<=> ( sK6 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl15_39])],[avatar_definition]) ).
tff(f402,plain,
( ( sK6 = sK7 )
| ~ spl15_39 ),
inference(avatar_component_clause,[],[f400]) ).
tff(f403,plain,
( spl15_39
| ~ spl15_10
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f392,f185,f170,f400]) ).
tff(f405,definition,
( spl15_40
<=> p__greater__(sK7,sF13) ),
introduced(definition,[new_symbols(definition,[spl15_40])],[avatar_definition]) ).
tff(f407,plain,
( p__greater__(sK7,sF13)
| ~ spl15_40 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f408,plain,
( spl15_40
| ~ spl15_8
| ~ spl15_12 ),
inference(avatar_split_clause,[],[f393,f180,f160,f405]) ).
tff(f409,plain,
( p__greater__(sK6,sF13)
| ~ spl15_39
| ~ spl15_40 ),
inference(forward_demodulation,[],[f407,f402]) ).
tff(f411,definition,
( spl15_41
<=> p__greater__(sK6,sF13) ),
introduced(definition,[new_symbols(definition,[spl15_41])],[avatar_definition]) ).
tff(f413,plain,
( p__greater__(sK6,sF13)
| ~ spl15_41 ),
inference(avatar_component_clause,[],[f411]) ).
tff(f414,plain,
( spl15_41
| ~ spl15_39
| ~ spl15_40 ),
inference(avatar_split_clause,[],[f409,f405,f400,f411]) ).
tff(f416,plain,
( ~ p__less_equal__(f__integer__(6),sK10)
| ~ spl15_6
| spl15_17 ),
inference(superposition,[],[f220,f152]) ).
tff(f455,definition,
( spl15_48
<=> p__less_equal__(f__integer__(6),sK10) ),
introduced(definition,[new_symbols(definition,[spl15_48])],[avatar_definition]) ).
tff(f457,plain,
( ~ p__less_equal__(f__integer__(6),sK10)
| spl15_48 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f458,plain,
( ~ spl15_48
| ~ spl15_6
| spl15_17 ),
inference(avatar_split_clause,[],[f416,f218,f150,f455]) ).
tff(f466,plain,
( p__less__(sK6,sK10)
| ~ spl15_5
| ~ spl15_38 ),
inference(superposition,[],[f147,f397]) ).
tff(f468,definition,
( spl15_50
<=> p__less__(sK6,sK10) ),
introduced(definition,[new_symbols(definition,[spl15_50])],[avatar_definition]) ).
tff(f471,plain,
( spl15_50
| ~ spl15_5
| ~ spl15_38 ),
inference(avatar_split_clause,[],[f466,f395,f145,f468]) ).
tff(f474,plain,
( p__less_equal__(sF13,sK6)
| ~ spl15_41 ),
inference(resolution,[],[f413,f110]) ).
tff(f476,definition,
( spl15_51
<=> p__less_equal__(sF13,sK6) ),
introduced(definition,[new_symbols(definition,[spl15_51])],[avatar_definition]) ).
tff(f478,plain,
( p__less_equal__(sF13,sK6)
| ~ spl15_51 ),
inference(avatar_component_clause,[],[f476]) ).
tff(f479,plain,
( spl15_51
| ~ spl15_41 ),
inference(avatar_split_clause,[],[f474,f411,f476]) ).
tff(f487,plain,
( ! [X0: $int] :
( p__less_equal__(f__integer__(X0),sF13)
| $less(3,X0) )
| ~ spl15_7 ),
inference(superposition,[],[f111,f157]) ).
tff(f504,plain,
( ! [X0: general] :
( ~ p__less_equal__(f__integer__(1),X0)
| ~ p__less_equal__(X0,f__integer__(0)) )
| spl15_14 ),
inference(resolution,[],[f102,f196]) ).
tff(f505,plain,
( ! [X0: general] :
( ~ p__less_equal__(X0,sK10)
| ~ p__less_equal__(f__integer__(6),X0) )
| spl15_48 ),
inference(resolution,[],[f102,f457]) ).
tff(f507,plain,
( ! [X0: general] :
( ~ p__less_equal__(f__integer__(6),X0)
| ~ p__less_equal__(X0,sF14) )
| spl15_17 ),
inference(resolution,[],[f102,f220]) ).
tff(f518,plain,
( ! [X0: general] :
( p__less_equal__(sK10,X0)
| ~ p__less_equal__(f__integer__(6),X0) )
| spl15_48 ),
inference(resolution,[],[f505,f84]) ).
tff(f521,plain,
! [X2: general,X0: general,X1: general] :
( ~ p__less_equal__(X1,X2)
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X2,X0)
| ( X0 = X1 ) ),
inference(resolution,[],[f106,f102]) ).
tff(f523,plain,
! [X0: general,X1: general] :
( ~ p__less__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(resolution,[],[f106,f74]) ).
tff(f528,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X0,X1)
| ( f__integer__(X1) = f__integer__(X0) ) ),
inference(resolution,[],[f106,f111]) ).
tff(f530,plain,
( ( sK6 = sF13 )
| ~ p__less_equal__(sK6,sF13)
| ~ spl15_51 ),
inference(resolution,[],[f106,f478]) ).
tff(f533,definition,
( spl15_52
<=> ( sK6 = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl15_52])],[avatar_definition]) ).
tff(f535,plain,
( ( sK6 = sF13 )
| ~ spl15_52 ),
inference(avatar_component_clause,[],[f533]) ).
tff(f537,definition,
( spl15_53
<=> p__less_equal__(sK6,sF13) ),
introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition]) ).
tff(f540,plain,
( spl15_52
| ~ spl15_53
| ~ spl15_51 ),
inference(avatar_split_clause,[],[f530,f476,f537,f533]) ).
tff(f557,plain,
( ! [X0: general,X1: general] :
( ~ p__less_equal__(X0,f__integer__(0))
| ~ p__less_equal__(f__integer__(1),X1)
| ~ p__less_equal__(X1,X0) )
| spl15_14 ),
inference(resolution,[],[f504,f102]) ).
tff(f595,plain,
( p__less_equal__(sK1(sK6),sK2(sK6))
| ~ spl15_37 ),
inference(resolution,[],[f385,f110]) ).
tff(f596,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| p__greater__(sK6,sK1(sK6)) )
| ~ spl15_37 ),
inference(superposition,[],[f385,f91]) ).
tff(f597,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| p__greater__(sK2(sK6),f__integer__(3)) )
| ~ spl15_37 ),
inference(superposition,[],[f385,f92]) ).
tff(f599,definition,
( spl15_58
<=> p__less_equal__(sK1(sK6),sK2(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition]) ).
tff(f601,plain,
( p__less_equal__(sK1(sK6),sK2(sK6))
| ~ spl15_58 ),
inference(avatar_component_clause,[],[f599]) ).
tff(f602,plain,
( spl15_58
| ~ spl15_37 ),
inference(avatar_split_clause,[],[f595,f383,f599]) ).
tff(f608,plain,
! [X0: general] :
( p__is_integer__(X0)
| ( f__symbolic__(sK11(X0)) = X0 )
| ( c__infimum__ = X0 )
| ( c__supremum__ = X0 ) ),
inference(resolution,[],[f83,f105]) ).
tff(f609,plain,
( ~ p__less_equal__(sK2(sK6),sK1(sK6))
| ( sK2(sK6) = sK1(sK6) )
| ~ spl15_58 ),
inference(resolution,[],[f601,f106]) ).
tff(f613,definition,
( spl15_59
<=> p__less_equal__(sK2(sK6),sK1(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_59])],[avatar_definition]) ).
tff(f615,plain,
( ~ p__less_equal__(sK2(sK6),sK1(sK6))
| spl15_59 ),
inference(avatar_component_clause,[],[f613]) ).
tff(f617,definition,
( spl15_60
<=> ( sK2(sK6) = sK1(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition]) ).
tff(f619,plain,
( ( sK2(sK6) = sK1(sK6) )
| ~ spl15_60 ),
inference(avatar_component_clause,[],[f617]) ).
tff(f620,plain,
( ~ spl15_59
| spl15_60
| ~ spl15_58 ),
inference(avatar_split_clause,[],[f609,f599,f617,f613]) ).
tff(f649,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| ~ p__less_equal__(sK6,sK1(sK6)) )
| spl15_59 ),
inference(superposition,[],[f615,f91]) ).
tff(f665,definition,
( spl15_62
<=> p__less_equal__(f__integer__(1),sF13) ),
introduced(definition,[new_symbols(definition,[spl15_62])],[avatar_definition]) ).
tff(f666,plain,
( p__less_equal__(f__integer__(1),sF13)
| ~ spl15_62 ),
inference(avatar_component_clause,[],[f665]) ).
tff(f667,plain,
( ~ p__less_equal__(f__integer__(1),sF13)
| spl15_62 ),
inference(avatar_component_clause,[],[f665]) ).
tff(f677,definition,
( spl15_64
<=> p__less_equal__(sF13,f__integer__(1)) ),
introduced(definition,[new_symbols(definition,[spl15_64])],[avatar_definition]) ).
tff(f678,plain,
( ~ p__less_equal__(sF13,f__integer__(1))
| spl15_64 ),
inference(avatar_component_clause,[],[f677]) ).
tff(f679,plain,
( p__less_equal__(sF13,f__integer__(1))
| ~ spl15_64 ),
inference(avatar_component_clause,[],[f677]) ).
tff(f712,plain,
( ! [X0: general,X1: general] :
( ~ p__less__(X1,f__integer__(0))
| ~ p__less_equal__(f__integer__(1),X0)
| ~ p__less_equal__(X0,X1) )
| spl15_14 ),
inference(resolution,[],[f557,f74]) ).
tff(f743,plain,
( ( f__integer__(1) = sF13 )
| ~ p__less_equal__(f__integer__(1),sF13)
| ~ spl15_64 ),
inference(resolution,[],[f679,f106]) ).
tff(f805,plain,
( $less(3,1)
| ~ spl15_7
| spl15_62 ),
inference(resolution,[],[f487,f667]) ).
tff(f812,plain,
( $false
| ~ spl15_7
| spl15_62 ),
inference(evaluation,[],[f805]) ).
tff(f813,plain,
( ~ spl15_7
| spl15_62 ),
inference(avatar_contradiction_clause,[],[f812]) ).
tff(f816,plain,
( ( f__integer__(1) = sF13 )
| ~ spl15_62
| ~ spl15_64 ),
inference(forward_subsumption_resolution,[],[f743,f666]) ).
tff(f818,definition,
( spl15_72
<=> ( f__integer__(1) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl15_72])],[avatar_definition]) ).
tff(f820,plain,
( ( f__integer__(1) = sF13 )
| ~ spl15_72 ),
inference(avatar_component_clause,[],[f818]) ).
tff(f821,plain,
( spl15_72
| ~ spl15_62
| ~ spl15_64 ),
inference(avatar_split_clause,[],[f816,f677,f665,f818]) ).
tff(f850,plain,
! [X0: symbol] :
( ~ p__less_equal__(c__supremum__,f__symbolic__(X0))
| ( c__supremum__ = f__symbolic__(X0) ) ),
inference(resolution,[],[f523,f75]) ).
tff(f855,plain,
! [X0: general,X1: general] :
( ~ sP0(X0,X1)
| ( sK3(X0) = sK4(X0) )
| ~ p__less_equal__(sK4(X0),sK3(X0)) ),
inference(resolution,[],[f523,f88]) ).
tff(f857,plain,
( ~ p__less_equal__(sK10,sK9)
| ( sK9 = sK10 )
| ~ spl15_5 ),
inference(resolution,[],[f523,f147]) ).
tff(f863,definition,
( spl15_76
<=> p__less_equal__(sK10,sK6) ),
introduced(definition,[new_symbols(definition,[spl15_76])],[avatar_definition]) ).
tff(f865,plain,
( ~ p__less_equal__(sK10,sK6)
| spl15_76 ),
inference(avatar_component_clause,[],[f863]) ).
tff(f867,definition,
( spl15_77
<=> ( sK6 = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl15_77])],[avatar_definition]) ).
tff(f869,plain,
( ( sK6 = sK10 )
| ~ spl15_77 ),
inference(avatar_component_clause,[],[f867]) ).
tff(f881,plain,
( ~ p__less_equal__(sK10,sK6)
| ( sK9 = sK10 )
| ~ spl15_5
| ~ spl15_38 ),
inference(forward_demodulation,[],[f857,f397]) ).
tff(f884,plain,
( ( sK6 = sK10 )
| ~ p__less_equal__(sK10,sK6)
| ~ spl15_5
| ~ spl15_38 ),
inference(forward_demodulation,[],[f881,f397]) ).
tff(f886,plain,
( ~ spl15_76
| spl15_77
| ~ spl15_5
| ~ spl15_38 ),
inference(avatar_split_clause,[],[f884,f395,f145,f867,f863]) ).
tff(f887,plain,
( ~ p__less_equal__(f__integer__(6),sK6)
| spl15_48
| spl15_76 ),
inference(resolution,[],[f865,f518]) ).
tff(f890,plain,
( p__less_equal__(sK6,sK10)
| spl15_76 ),
inference(resolution,[],[f865,f84]) ).
tff(f893,definition,
( spl15_80
<=> p__less_equal__(sK6,sK10) ),
introduced(definition,[new_symbols(definition,[spl15_80])],[avatar_definition]) ).
tff(f896,plain,
( spl15_80
| spl15_76 ),
inference(avatar_split_clause,[],[f890,f863,f893]) ).
tff(f903,definition,
( spl15_82
<=> p__less_equal__(f__integer__(6),sK6) ),
introduced(definition,[new_symbols(definition,[spl15_82])],[avatar_definition]) ).
tff(f904,plain,
( p__less_equal__(f__integer__(6),sK6)
| ~ spl15_82 ),
inference(avatar_component_clause,[],[f903]) ).
tff(f905,plain,
( ~ p__less_equal__(f__integer__(6),sK6)
| spl15_82 ),
inference(avatar_component_clause,[],[f903]) ).
tff(f906,plain,
( ~ spl15_82
| spl15_48
| spl15_76 ),
inference(avatar_split_clause,[],[f887,f863,f455,f903]) ).
tff(f947,plain,
! [X2: general,X0: general,X1: general] :
( ~ p__less__(X1,X2)
| ~ p__less_equal__(X2,X0)
| ( X0 = X1 )
| ~ p__less_equal__(X0,X1) ),
inference(resolution,[],[f521,f74]) ).
tff(f995,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| ( f__integer__(X1) = f__integer__(X0) )
| $less(X0,X1) ),
inference(resolution,[],[f528,f111]) ).
tff(f1031,plain,
( ( 3 = 1 )
| ( sF13 != sF13 )
| ~ spl15_7
| ~ spl15_72 ),
inference(superposition,[],[f340,f820]) ).
tff(f1039,plain,
( ( 3 = 1 )
| ~ spl15_7
| ~ spl15_72 ),
inference(trivial_inequality_removal,[],[f1031]) ).
tff(f1040,plain,
( $false
| ~ spl15_7
| ~ spl15_72 ),
inference(evaluation,[],[f1039]) ).
tff(f1041,plain,
( ~ spl15_7
| ~ spl15_72 ),
inference(avatar_contradiction_clause,[],[f1040]) ).
tff(f1045,plain,
( ! [X0: general] :
( ~ p__less_equal__(X0,f__integer__(1))
| ~ p__less_equal__(sF13,X0) )
| spl15_64 ),
inference(resolution,[],[f678,f102]) ).
tff(f1053,plain,
! [X0: general] :
( ( f__symbolic__(sK11(X0)) = X0 )
| ( f__integer__(sK12(X0)) = X0 )
| ( c__supremum__ = X0 )
| ( c__infimum__ = X0 ) ),
inference(resolution,[],[f608,f108]) ).
tff(f1107,plain,
( ~ p__less__(f__integer__(6),sK6)
| spl15_82 ),
inference(resolution,[],[f905,f74]) ).
tff(f1109,definition,
( spl15_87
<=> p__less__(f__integer__(6),sK6) ),
introduced(definition,[new_symbols(definition,[spl15_87])],[avatar_definition]) ).
tff(f1110,plain,
( p__less__(f__integer__(6),sK6)
| ~ spl15_87 ),
inference(avatar_component_clause,[],[f1109]) ).
tff(f1111,plain,
( ~ p__less__(f__integer__(6),sK6)
| spl15_87 ),
inference(avatar_component_clause,[],[f1109]) ).
tff(f1112,plain,
( ~ spl15_87
| spl15_82 ),
inference(avatar_split_clause,[],[f1107,f903,f1109]) ).
tff(f1289,plain,
( ! [X0: general] :
( ~ p__less_equal__(X0,c__infimum__)
| ~ p__less_equal__(f__integer__(1),X0) )
| spl15_14 ),
inference(resolution,[],[f712,f107]) ).
tff(f1293,plain,
! [X0: symbol] :
( p__less_equal__(f__symbolic__(X0),c__supremum__)
| ( c__supremum__ = f__symbolic__(X0) ) ),
inference(resolution,[],[f850,f84]) ).
tff(f1452,definition,
( spl15_98
<=> p__less_equal__(sK6,sK1(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_98])],[avatar_definition]) ).
tff(f1454,plain,
( ~ p__less_equal__(sK6,sK1(sK6))
| spl15_98 ),
inference(avatar_component_clause,[],[f1452]) ).
tff(f1739,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less(X1,X0)
| ( f__integer__(X1) = f__integer__(X0) )
| $less($sum(X0,X2),$sum(X1,X2)) ),
inference(resolution,[],[f995,f29]) ).
tff(f1804,plain,
( ! [X0: symbol,X1: general] :
( ~ p__less_equal__(f__symbolic__(X0),X1)
| ~ p__less_equal__(X1,sF14)
| ( sF14 = X1 ) )
| ~ spl15_2 ),
inference(resolution,[],[f947,f236]) ).
tff(f1955,plain,
( ~ p__less_equal__(f__integer__(1),c__infimum__)
| spl15_14 ),
inference(resolution,[],[f1289,f287]) ).
tff(f1964,definition,
( spl15_115
<=> p__less_equal__(f__integer__(1),c__infimum__) ),
introduced(definition,[new_symbols(definition,[spl15_115])],[avatar_definition]) ).
tff(f1967,plain,
( ~ spl15_115
| spl15_14 ),
inference(avatar_split_clause,[],[f1955,f194,f1964]) ).
tff(f2315,plain,
( ! [X0: general] :
( ~ p__less_equal__(sF13,X0)
| p__less_equal__(f__integer__(1),X0) )
| spl15_64 ),
inference(resolution,[],[f1045,f84]) ).
tff(f2345,plain,
! [X0: general,X1: $int] :
( p__less__(f__integer__(X1),X0)
| ( f__integer__(sK12(X0)) = X0 )
| ( c__supremum__ = X0 )
| ( c__infimum__ = X0 ) ),
inference(superposition,[],[f78,f1053]) ).
tff(f2608,plain,
( p__less_equal__(f__integer__(1),sK6)
| ~ spl15_51
| spl15_64 ),
inference(resolution,[],[f2315,f478]) ).
tff(f2617,definition,
( spl15_120
<=> p__less_equal__(f__integer__(1),sK6) ),
introduced(definition,[new_symbols(definition,[spl15_120])],[avatar_definition]) ).
tff(f2620,plain,
( spl15_120
| ~ spl15_51
| spl15_64 ),
inference(avatar_split_clause,[],[f2608,f677,f476,f2617]) ).
tff(f3175,definition,
( spl15_150
<=> ( c__supremum__ = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_150])],[avatar_definition]) ).
tff(f3176,plain,
( ( c__supremum__ != sK6 )
| spl15_150 ),
inference(avatar_component_clause,[],[f3175]) ).
tff(f3177,plain,
( ( c__supremum__ = sK6 )
| ~ spl15_150 ),
inference(avatar_component_clause,[],[f3175]) ).
tff(f3179,definition,
( spl15_151
<=> ( f__integer__(sK12(sK6)) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_151])],[avatar_definition]) ).
tff(f3180,plain,
( ( f__integer__(sK12(sK6)) != sK6 )
| spl15_151 ),
inference(avatar_component_clause,[],[f3179]) ).
tff(f3181,plain,
( ( f__integer__(sK12(sK6)) = sK6 )
| ~ spl15_151 ),
inference(avatar_component_clause,[],[f3179]) ).
tff(f3183,definition,
( spl15_152
<=> ( c__infimum__ = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_152])],[avatar_definition]) ).
tff(f3184,plain,
( ( c__infimum__ != sK6 )
| spl15_152 ),
inference(avatar_component_clause,[],[f3183]) ).
tff(f3580,plain,
( ! [X0: $int] :
( ~ p__less_equal__(sK6,f__integer__(X0))
| ~ $less(X0,sK12(sK6)) )
| ~ spl15_151 ),
inference(superposition,[],[f112,f3181]) ).
tff(f3585,plain,
( $less(3,sK12(sK6))
| p__less_equal__(sK6,sF13)
| ~ spl15_7
| ~ spl15_151 ),
inference(superposition,[],[f487,f3181]) ).
tff(f3646,definition,
( spl15_189
<=> ( 5 = sK12(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl15_189])],[avatar_definition]) ).
tff(f3648,plain,
( ( 5 = sK12(sK6) )
| ~ spl15_189 ),
inference(avatar_component_clause,[],[f3646]) ).
tff(f3655,definition,
( spl15_190
<=> $less(3,sK12(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_190])],[avatar_definition]) ).
tff(f3657,plain,
( $less(3,sK12(sK6))
| ~ spl15_190 ),
inference(avatar_component_clause,[],[f3655]) ).
tff(f3661,definition,
( spl15_191
<=> $less(sK12(sK6),5) ),
introduced(definition,[new_symbols(definition,[spl15_191])],[avatar_definition]) ).
tff(f3662,plain,
( ~ $less(sK12(sK6),5)
| spl15_191 ),
inference(avatar_component_clause,[],[f3661]) ).
tff(f3696,plain,
( ~ spl15_98
| spl15_34
| spl15_59 ),
inference(avatar_split_clause,[],[f649,f613,f366,f1452]) ).
tff(f3714,definition,
( spl15_200
<=> p__greater__(sK6,sK1(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_200])],[avatar_definition]) ).
tff(f3716,plain,
( p__greater__(sK6,sK1(sK6))
| ~ spl15_200 ),
inference(avatar_component_clause,[],[f3714]) ).
tff(f3717,plain,
( spl15_34
| spl15_200
| ~ spl15_37 ),
inference(avatar_split_clause,[],[f596,f383,f3714,f366]) ).
tff(f3725,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| p__greater__(sK2(sK6),sF13) )
| ~ spl15_7
| ~ spl15_37 ),
inference(forward_demodulation,[],[f597,f157]) ).
tff(f3736,definition,
( spl15_203
<=> p__greater__(sK2(sK6),sF13) ),
introduced(definition,[new_symbols(definition,[spl15_203])],[avatar_definition]) ).
tff(f3738,plain,
( p__greater__(sK2(sK6),sF13)
| ~ spl15_203 ),
inference(avatar_component_clause,[],[f3736]) ).
tff(f3739,plain,
( spl15_34
| spl15_203
| ~ spl15_7
| ~ spl15_37 ),
inference(avatar_split_clause,[],[f3725,f383,f155,f3736,f366]) ).
tff(f3750,plain,
( p__greater__(sK6,sK2(sK6))
| ~ spl15_60
| ~ spl15_200 ),
inference(forward_demodulation,[],[f3716,f619]) ).
tff(f3759,definition,
( spl15_206
<=> p__greater__(sK6,sK2(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_206])],[avatar_definition]) ).
tff(f3761,plain,
( p__greater__(sK6,sK2(sK6))
| ~ spl15_206 ),
inference(avatar_component_clause,[],[f3759]) ).
tff(f3762,plain,
( spl15_206
| ~ spl15_60
| ~ spl15_200 ),
inference(avatar_split_clause,[],[f3750,f3714,f617,f3759]) ).
tff(f3764,plain,
( p__less__(sK6,sK4(sK6))
| ~ spl15_31 ),
inference(resolution,[],[f320,f345]) ).
tff(f3770,plain,
( p__less__(sK6,sF14)
| ~ spl15_31
| ~ spl15_33 ),
inference(forward_demodulation,[],[f3764,f361]) ).
tff(f3791,definition,
( spl15_209
<=> p__less_equal__(f__integer__(6),sK3(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_209])],[avatar_definition]) ).
tff(f3792,plain,
( p__less_equal__(f__integer__(6),sK3(sK6))
| ~ spl15_209 ),
inference(avatar_component_clause,[],[f3791]) ).
tff(f3793,plain,
( ~ p__less_equal__(f__integer__(6),sK3(sK6))
| spl15_209 ),
inference(avatar_component_clause,[],[f3791]) ).
tff(f3796,plain,
( ! [X0: general] :
( p__greater__(sK6,sF13)
| ~ sP0(sK6,X0) )
| ~ spl15_203 ),
inference(superposition,[],[f3738,f91]) ).
tff(f3797,plain,
( spl15_41
| spl15_34
| ~ spl15_203 ),
inference(avatar_split_clause,[],[f3796,f3736,f366,f411]) ).
tff(f3800,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| p__greater__(sK6,sK6) )
| ~ spl15_206 ),
inference(superposition,[],[f3761,f91]) ).
tff(f3801,plain,
( ! [X0: general] : ~ sP0(sK6,X0)
| ~ spl15_206 ),
inference(forward_subsumption_resolution,[],[f3800,f118]) ).
tff(f3802,plain,
( spl15_34
| ~ spl15_206 ),
inference(avatar_split_clause,[],[f3801,f3759,f366]) ).
tff(f3912,definition,
( spl15_220
<=> ( c__infimum__ = sK3(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl15_220])],[avatar_definition]) ).
tff(f3913,plain,
( ( c__infimum__ != sK3(sK6) )
| spl15_220 ),
inference(avatar_component_clause,[],[f3912]) ).
tff(f3935,plain,
( ! [X0: general] :
( ~ p__less_equal__(sK6,f__integer__(3))
| ~ sP0(sK6,X0) )
| spl15_98 ),
inference(superposition,[],[f1454,f92]) ).
tff(f3936,plain,
( ! [X0: general] :
( ~ p__less_equal__(sK6,sF13)
| ~ sP0(sK6,X0) )
| ~ spl15_7
| spl15_98 ),
inference(forward_demodulation,[],[f3935,f157]) ).
tff(f4071,plain,
( ~ $less(sK12(sK6),$sum(1,3))
| ~ spl15_190 ),
inference(resolution,[],[f3657,f327]) ).
tff(f4073,plain,
( ~ $less(sK12(sK6),4)
| ~ spl15_190 ),
inference(evaluation,[],[f4071]) ).
tff(f4079,definition,
( spl15_227
<=> $less(sK12(sK6),4) ),
introduced(definition,[new_symbols(definition,[spl15_227])],[avatar_definition]) ).
tff(f4081,plain,
( ~ $less(sK12(sK6),4)
| spl15_227 ),
inference(avatar_component_clause,[],[f4079]) ).
tff(f4082,plain,
( ~ spl15_227
| ~ spl15_190 ),
inference(avatar_split_clause,[],[f4073,f3655,f4079]) ).
tff(f4173,plain,
( ! [X0: $int] :
( ~ p__less__(sK6,f__integer__(X0))
| ~ $less(X0,sK12(sK6)) )
| ~ spl15_151 ),
inference(resolution,[],[f3580,f74]) ).
tff(f4191,definition,
( spl15_236
<=> $less(5,sK12(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_236])],[avatar_definition]) ).
tff(f4192,plain,
( $less(5,sK12(sK6))
| ~ spl15_236 ),
inference(avatar_component_clause,[],[f4191]) ).
tff(f4193,plain,
( ~ $less(5,sK12(sK6))
| spl15_236 ),
inference(avatar_component_clause,[],[f4191]) ).
tff(f4367,plain,
( ! [X0: general] :
( ( c__infimum__ != sK6 )
| ~ sP0(sK6,X0) )
| spl15_220 ),
inference(superposition,[],[f3913,f90]) ).
tff(f4368,plain,
( spl15_34
| ~ spl15_152
| spl15_220 ),
inference(avatar_split_clause,[],[f4367,f3912,f3183,f366]) ).
tff(f4566,plain,
( ( f__integer__(5) = f__integer__(sK12(sK6)) )
| $less(sK12(sK6),5)
| spl15_236 ),
inference(resolution,[],[f4193,f995]) ).
tff(f4692,plain,
( ! [X0: general] :
( ~ p__less_equal__(f__integer__(6),sK6)
| ~ sP0(sK6,X0) )
| spl15_209 ),
inference(superposition,[],[f3793,f90]) ).
tff(f4699,definition,
( spl15_259
<=> p__less__(f__integer__(6),sK3(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_259])],[avatar_definition]) ).
tff(f4701,plain,
( ~ p__less__(f__integer__(6),sK3(sK6))
| spl15_259 ),
inference(avatar_component_clause,[],[f4699]) ).
tff(f4842,plain,
( ( f__integer__(4) = f__integer__(sK12(sK6)) )
| $less(4,sK12(sK6))
| spl15_227 ),
inference(resolution,[],[f4081,f995]) ).
tff(f4854,definition,
( spl15_267
<=> $less(4,sK12(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_267])],[avatar_definition]) ).
tff(f4858,plain,
( $less(4,sK12(sK6))
| ( f__integer__(4) = sK6 )
| ~ spl15_151
| spl15_227 ),
inference(forward_demodulation,[],[f4842,f3181]) ).
tff(f4863,definition,
( spl15_268
<=> ( f__integer__(4) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_268])],[avatar_definition]) ).
tff(f4865,plain,
( ( f__integer__(4) = sK6 )
| ~ spl15_268 ),
inference(avatar_component_clause,[],[f4863]) ).
tff(f4866,plain,
( spl15_268
| spl15_267
| ~ spl15_151
| spl15_227 ),
inference(avatar_split_clause,[],[f4858,f4079,f3179,f4854,f4863]) ).
tff(f5162,plain,
( ! [X0: general] :
( ~ sP0(sK6,X0)
| ~ p__less__(f__integer__(6),sK6) )
| spl15_259 ),
inference(superposition,[],[f4701,f90]) ).
tff(f5561,plain,
( ~ p__less__(sK6,sF14)
| ~ $less(5,sK12(sK6))
| ~ spl15_2
| ~ spl15_151 ),
inference(superposition,[],[f4173,f133]) ).
tff(f6367,plain,
( ! [X0: $int] :
( $less($sum(sK12(sK6),X0),$sum(5,X0))
| ( f__integer__(5) = f__integer__(sK12(sK6)) ) )
| spl15_236 ),
inference(resolution,[],[f1739,f4193]) ).
tff(f6563,plain,
( hp(sK6)
| ~ spl15_1
| ~ spl15_268 ),
inference(superposition,[],[f128,f4865]) ).
tff(f6565,plain,
( ! [X0: general] : ~ sP0(X0,sK6)
| ~ spl15_3
| ~ spl15_268 ),
inference(superposition,[],[f189,f4865]) ).
tff(f6677,plain,
( spl15_9
| ~ spl15_1
| ~ spl15_268 ),
inference(avatar_split_clause,[],[f6563,f4863,f126,f165]) ).
tff(f6973,plain,
( ( c__infimum__ = sK6 )
| ( f__integer__(sK12(sK6)) = sK6 )
| ( c__supremum__ = sK6 )
| spl15_87 ),
inference(resolution,[],[f2345,f1111]) ).
tff(f7031,plain,
( $false
| ~ spl15_3
| ~ spl15_31
| ~ spl15_268 ),
inference(resolution,[],[f6565,f320]) ).
tff(f7032,plain,
( ~ spl15_3
| ~ spl15_31
| ~ spl15_268 ),
inference(avatar_contradiction_clause,[],[f7031]) ).
tff(f7039,plain,
( ~ spl15_53
| spl15_34
| ~ spl15_7
| spl15_98 ),
inference(avatar_split_clause,[],[f3936,f1452,f155,f366,f537]) ).
tff(f7107,plain,
( p__greater__(sK7,sK6)
| ~ spl15_40
| ~ spl15_52 ),
inference(forward_demodulation,[],[f407,f535]) ).
tff(f7147,plain,
( p__greater__(sK6,sK6)
| ~ spl15_39
| ~ spl15_40
| ~ spl15_52 ),
inference(forward_demodulation,[],[f7107,f402]) ).
tff(f7160,plain,
( $false
| ~ spl15_39
| ~ spl15_40
| ~ spl15_52 ),
inference(forward_subsumption_resolution,[],[f7147,f118]) ).
tff(f7161,plain,
( ~ spl15_39
| ~ spl15_40
| ~ spl15_52 ),
inference(avatar_contradiction_clause,[],[f7160]) ).
tff(f7195,plain,
( ( f__integer__(5) = sK6 )
| $less(sK12(sK6),5)
| ~ spl15_151
| spl15_236 ),
inference(forward_demodulation,[],[f4566,f3181]) ).
tff(f7212,plain,
( spl15_53
| spl15_190
| ~ spl15_7
| ~ spl15_151 ),
inference(avatar_split_clause,[],[f3585,f3179,f155,f3655,f537]) ).
tff(f7217,plain,
( ! [X0: $int] :
( ( f__integer__(5) = sK6 )
| $less($sum(sK12(sK6),X0),$sum(5,X0)) )
| ~ spl15_151
| spl15_236 ),
inference(forward_demodulation,[],[f6367,f3181]) ).
tff(f7257,plain,
( ( f__integer__(5) = sK6 )
| ~ spl15_151
| spl15_191
| spl15_236 ),
inference(forward_subsumption_resolution,[],[f7195,f3662]) ).
tff(f7263,plain,
( ! [X0: $int] :
( $less($sum(sK12(sK6),X0),$sum(5,X0))
| ( sK6 = sF14 ) )
| ~ spl15_2
| ~ spl15_151
| spl15_236 ),
inference(forward_demodulation,[],[f7217,f133]) ).
tff(f7283,definition,
( spl15_332
<=> ( f__integer__(5) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl15_332])],[avatar_definition]) ).
tff(f7286,plain,
( spl15_332
| ~ spl15_151
| spl15_191
| spl15_236 ),
inference(avatar_split_clause,[],[f7257,f4191,f3661,f3179,f7283]) ).
tff(f7289,plain,
( ! [X0: $int] :
( ( sK6 = sF14 )
| $less($sum(5,X0),$sum(5,X0)) )
| ~ spl15_2
| ~ spl15_151
| ~ spl15_189
| spl15_236 ),
inference(forward_demodulation,[],[f7263,f3648]) ).
tff(f7297,plain,
( ( sK6 = sF14 )
| ~ spl15_2
| ~ spl15_151
| ~ spl15_189
| spl15_236 ),
inference(forward_subsumption_resolution,[],[f7289,f26]) ).
tff(f7301,definition,
( spl15_333
<=> ( sK6 = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl15_333])],[avatar_definition]) ).
tff(f7302,plain,
( ( sK6 != sF14 )
| spl15_333 ),
inference(avatar_component_clause,[],[f7301]) ).
tff(f7303,plain,
( ( sK6 = sF14 )
| ~ spl15_333 ),
inference(avatar_component_clause,[],[f7301]) ).
tff(f7304,plain,
( spl15_333
| ~ spl15_2
| ~ spl15_151
| ~ spl15_189
| spl15_236 ),
inference(avatar_split_clause,[],[f7297,f4191,f3646,f3179,f131,f7301]) ).
tff(f7343,plain,
( p__less__(sK9,sK6)
| ~ spl15_5
| ~ spl15_77 ),
inference(superposition,[],[f147,f869]) ).
tff(f7443,plain,
( p__less__(sK6,sK6)
| ~ spl15_5
| ~ spl15_38
| ~ spl15_77 ),
inference(forward_demodulation,[],[f7343,f397]) ).
tff(f7474,plain,
( $false
| ~ spl15_5
| ~ spl15_38
| ~ spl15_77 ),
inference(forward_subsumption_resolution,[],[f7443,f113]) ).
tff(f7475,plain,
( ~ spl15_5
| ~ spl15_38
| ~ spl15_77 ),
inference(avatar_contradiction_clause,[],[f7474]) ).
tff(f7628,plain,
( p__less__(sK6,sK6)
| ~ spl15_31
| ~ spl15_33
| ~ spl15_333 ),
inference(forward_demodulation,[],[f3770,f7303]) ).
tff(f7719,plain,
( $false
| ~ spl15_31
| ~ spl15_33
| ~ spl15_333 ),
inference(forward_subsumption_resolution,[],[f7628,f113]) ).
tff(f7720,plain,
( ~ spl15_31
| ~ spl15_33
| ~ spl15_333 ),
inference(avatar_contradiction_clause,[],[f7719]) ).
tff(f7788,plain,
( ~ p__less__(sK6,sF14)
| ~ spl15_2
| ~ spl15_151
| ~ spl15_236 ),
inference(forward_subsumption_resolution,[],[f5561,f4192]) ).
tff(f7806,plain,
( ! [X0: general] : ~ sP0(sK6,X0)
| ~ spl15_82
| spl15_209 ),
inference(forward_subsumption_resolution,[],[f4692,f904]) ).
tff(f7833,plain,
( $false
| ~ spl15_2
| ~ spl15_36
| ~ spl15_151
| ~ spl15_236 ),
inference(forward_subsumption_resolution,[],[f7788,f377]) ).
tff(f7834,plain,
( ~ spl15_2
| ~ spl15_36
| ~ spl15_151
| ~ spl15_236 ),
inference(avatar_contradiction_clause,[],[f7833]) ).
tff(f7836,definition,
( spl15_364
<=> p__less_equal__(sK6,sF14) ),
introduced(definition,[new_symbols(definition,[spl15_364])],[avatar_definition]) ).
tff(f7837,plain,
( p__less_equal__(sK6,sF14)
| ~ spl15_364 ),
inference(avatar_component_clause,[],[f7836]) ).
tff(f7842,plain,
( spl15_34
| ~ spl15_82
| spl15_209 ),
inference(avatar_split_clause,[],[f7806,f3791,f903,f366]) ).
tff(f7878,plain,
( ( c__supremum__ = sK6 )
| ( f__integer__(sK12(sK6)) = sK6 )
| spl15_87
| spl15_152 ),
inference(forward_subsumption_resolution,[],[f6973,f3184]) ).
tff(f7899,plain,
( ( f__integer__(sK12(sK6)) = sK6 )
| spl15_87
| spl15_150
| spl15_152 ),
inference(forward_subsumption_resolution,[],[f7878,f3176]) ).
tff(f7903,plain,
( $false
| spl15_87
| spl15_150
| spl15_151
| spl15_152 ),
inference(forward_subsumption_resolution,[],[f7899,f3180]) ).
tff(f7904,plain,
( spl15_87
| spl15_150
| spl15_151
| spl15_152 ),
inference(avatar_contradiction_clause,[],[f7903]) ).
tff(f7905,plain,
( ! [X0: general] : ~ sP0(sK6,X0)
| ~ spl15_87
| spl15_259 ),
inference(forward_subsumption_resolution,[],[f5162,f1110]) ).
tff(f7906,plain,
( spl15_34
| ~ spl15_87
| spl15_259 ),
inference(avatar_split_clause,[],[f7905,f4699,f1109,f366]) ).
tff(f7908,plain,
( ~ p__less_equal__(sK4(sK6),sK3(sK6))
| ( sK3(sK6) = sK4(sK6) )
| ~ spl15_31 ),
inference(resolution,[],[f320,f855]) ).
tff(f7913,plain,
( ( sK3(sK6) = sK4(sK6) )
| ~ p__less_equal__(sF14,sK3(sK6))
| ~ spl15_31
| ~ spl15_33 ),
inference(forward_demodulation,[],[f7908,f361]) ).
tff(f7917,plain,
( ( sF14 = sK3(sK6) )
| ~ p__less_equal__(sF14,sK3(sK6))
| ~ spl15_31
| ~ spl15_33 ),
inference(forward_demodulation,[],[f7913,f361]) ).
tff(f7919,definition,
( spl15_375
<=> p__less_equal__(sF14,sK3(sK6)) ),
introduced(definition,[new_symbols(definition,[spl15_375])],[avatar_definition]) ).
tff(f7921,plain,
( ~ p__less_equal__(sF14,sK3(sK6))
| spl15_375 ),
inference(avatar_component_clause,[],[f7919]) ).
tff(f7923,definition,
( spl15_376
<=> ( sF14 = sK3(sK6) ) ),
introduced(definition,[new_symbols(definition,[spl15_376])],[avatar_definition]) ).
tff(f7926,plain,
( ~ spl15_375
| spl15_376
| ~ spl15_31
| ~ spl15_33 ),
inference(avatar_split_clause,[],[f7917,f359,f318,f7923,f7919]) ).
tff(f8008,plain,
( ( sK6 = sF14 )
| ~ p__less_equal__(sF14,sK6)
| ~ spl15_36 ),
inference(resolution,[],[f377,f523]) ).
tff(f8009,plain,
( ~ p__less_equal__(sF14,sK6)
| ~ spl15_36
| spl15_333 ),
inference(forward_subsumption_resolution,[],[f8008,f7302]) ).
tff(f8011,definition,
( spl15_378
<=> p__less_equal__(sF14,sK6) ),
introduced(definition,[new_symbols(definition,[spl15_378])],[avatar_definition]) ).
tff(f8013,plain,
( ~ p__less_equal__(sF14,sK6)
| spl15_378 ),
inference(avatar_component_clause,[],[f8011]) ).
tff(f8014,plain,
( ~ spl15_378
| ~ spl15_36
| spl15_333 ),
inference(avatar_split_clause,[],[f8009,f7301,f375,f8011]) ).
tff(f8016,plain,
( p__less_equal__(sK6,sF14)
| spl15_378 ),
inference(resolution,[],[f8013,f84]) ).
tff(f8023,plain,
( spl15_364
| spl15_378 ),
inference(avatar_split_clause,[],[f8016,f8011,f7836]) ).
tff(f8050,plain,
( ! [X0: general] :
( ~ p__less_equal__(sF14,X0)
| ~ p__less_equal__(X0,sK3(sK6)) )
| spl15_375 ),
inference(resolution,[],[f7921,f102]) ).
tff(f8152,plain,
( ! [X0: general] :
( ~ p__less__(f__integer__(6),X0)
| ~ p__less_equal__(X0,sF14) )
| spl15_17 ),
inference(resolution,[],[f507,f74]) ).
tff(f8482,plain,
( ( 5 = sK12(sK6) )
| $less(5,sK12(sK6))
| spl15_191 ),
inference(resolution,[],[f3662,f28]) ).
tff(f8495,plain,
( spl15_236
| spl15_189
| spl15_191 ),
inference(avatar_split_clause,[],[f8482,f3661,f3646,f4191]) ).
tff(f8564,plain,
( ~ p__less_equal__(f__integer__(6),sK3(sK6))
| ~ spl15_26
| spl15_375 ),
inference(resolution,[],[f8050,f291]) ).
tff(f8572,plain,
( $false
| ~ spl15_26
| ~ spl15_209
| spl15_375 ),
inference(forward_subsumption_resolution,[],[f8564,f3792]) ).
tff(f8573,plain,
( ~ spl15_26
| ~ spl15_209
| spl15_375 ),
inference(avatar_contradiction_clause,[],[f8572]) ).
tff(f9055,plain,
( ! [X0: symbol] :
( ~ p__less_equal__(c__supremum__,sF14)
| ( c__supremum__ = sF14 )
| ( c__supremum__ = f__symbolic__(X0) ) )
| ~ spl15_2 ),
inference(resolution,[],[f1804,f1293]) ).
tff(f9062,plain,
( ! [X0: symbol] :
( ( c__supremum__ = sF14 )
| ( c__supremum__ = f__symbolic__(X0) )
| ~ p__less_equal__(sK6,sF14) )
| ~ spl15_2
| ~ spl15_150 ),
inference(forward_demodulation,[],[f9055,f3177]) ).
tff(f9063,plain,
( ! [X0: symbol] :
( ( c__supremum__ = sF14 )
| ( c__supremum__ = f__symbolic__(X0) ) )
| ~ spl15_2
| ~ spl15_150
| ~ spl15_364 ),
inference(forward_subsumption_resolution,[],[f9062,f7837]) ).
tff(f9064,plain,
( ! [X0: symbol] :
( ( c__supremum__ = f__symbolic__(X0) )
| ( sK6 = sF14 ) )
| ~ spl15_2
| ~ spl15_150
| ~ spl15_364 ),
inference(forward_demodulation,[],[f9063,f3177]) ).
tff(f9065,plain,
( ! [X0: symbol] : ( c__supremum__ = f__symbolic__(X0) )
| ~ spl15_2
| ~ spl15_150
| spl15_333
| ~ spl15_364 ),
inference(forward_subsumption_resolution,[],[f9064,f7302]) ).
tff(f9066,plain,
( ! [X0: symbol] : ( f__symbolic__(X0) = sK6 )
| ~ spl15_2
| ~ spl15_150
| spl15_333
| ~ spl15_364 ),
inference(forward_demodulation,[],[f9065,f3177]) ).
tff(f9067,plain,
( ! [X0: symbol] : ~ p__less_equal__(f__symbolic__(X0),sF14)
| spl15_17 ),
inference(resolution,[],[f8152,f78]) ).
tff(f9070,plain,
( ~ p__less_equal__(sK6,sF14)
| ~ spl15_2
| spl15_17
| ~ spl15_150
| spl15_333
| ~ spl15_364 ),
inference(forward_demodulation,[],[f9067,f9066]) ).
tff(f9072,plain,
( $false
| ~ spl15_2
| spl15_17
| ~ spl15_150
| spl15_333
| ~ spl15_364 ),
inference(forward_subsumption_resolution,[],[f9070,f7837]) ).
tff(f9073,plain,
( ~ spl15_2
| spl15_17
| ~ spl15_150
| spl15_333
| ~ spl15_364 ),
inference(avatar_contradiction_clause,[],[f9072]) ).
tff(f9074,plain,
$false,
inference(avatar_smt_refutation,[],[f9073,f8573,f8495,f8023,f8014,f7926,f7906,f7904,f7842,f7834,f7720,f7475,f7304,f7286,f7212,f7161,f7039,f7032,f6677,f4866,f4368,f4082,f3802,f3797,f3762,f3739,f3717,f3696,f2620,f1967,f1112,f1041,f906,f896,f886,f821,f813,f620,f602,f540,f479,f471,f458,f414,f408,f403,f398,f389,f387,f378,f372,f363,f321,f315,f292,f277,f221,f197,f188,f183,f178,f173,f168,f163,f158,f153,f148,f139,f134,f129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX073_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n002.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:02:52 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.35/1.42 % (419020)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.35/1.42 % (419096)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1987432224:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.35/1.42 % (419096)Instruction limit reached!
% 4.35/1.42 % (419096)------------------------------
% 4.35/1.42 % (419096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.42 % (419096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.42 % (419096)CaDiCaL version: 2.1.3
% 4.35/1.42 % (419096)Termination reason: Instruction limit
% 4.35/1.42 % (419096)Termination phase: Saturation
% 4.35/1.42 % (419096)Time elapsed: 0.003 s
% 4.35/1.42 % (419096)Peak memory usage: 88 MB
% 4.35/1.42 % (419096)Instructions burned: 7 (million)
% 4.35/1.42 % (419095)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2769292715:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.35/1.42 % (419092)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1600951597:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.35/1.42 % (419094)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4080153476:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.35/1.42 % (419098)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3886101987:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.35/1.42 % (419100)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=269729842:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.35/1.42 % (419098)Instruction limit reached!
% 4.35/1.42 % (419098)------------------------------
% 4.35/1.42 % (419098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.42 % (419098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.42 % (419098)CaDiCaL version: 2.1.3
% 4.35/1.42 % (419098)Termination reason: Instruction limit
% 4.35/1.42 % (419098)Termination phase: Saturation
% 4.35/1.42 % (419098)Time elapsed: 0.005 s
% 4.35/1.42 % (419098)Peak memory usage: 88 MB
% 4.35/1.42 % (419098)Instructions burned: 5 (million)
% 4.35/1.42 % (419099)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=494852983:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.35/1.42 % (419092)Instruction limit reached!
% 4.35/1.42 % (419092)------------------------------
% 4.35/1.42 % (419092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.42 % (419092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.42 % (419092)CaDiCaL version: 2.1.3
% 4.35/1.42 % (419092)Termination reason: Instruction limit
% 4.35/1.42 % (419092)Termination phase: Saturation
% 4.35/1.42 % (419092)Time elapsed: 0.032 s
% 4.35/1.42 % (419092)Peak memory usage: 115 MB
% 4.35/1.42 % (419092)Instructions burned: 12 (million)
% 4.35/1.42 % (419100)Instruction limit reached!
% 4.35/1.42 % (419100)------------------------------
% 4.35/1.42 % (419100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.42 % (419100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.42 % (419100)CaDiCaL version: 2.1.3
% 4.35/1.42 % (419100)Termination reason: Instruction limit
% 4.35/1.42 % (419100)Termination phase: Saturation
% 4.35/1.42 % (419100)Time elapsed: 0.046 s
% 4.35/1.42 % (419100)Peak memory usage: 115 MB
% 4.35/1.42 % (419100)Instructions burned: 34 (million)
% 4.35/1.42 % (419099)Instruction limit reached!
% 4.35/1.42 % (419099)------------------------------
% 4.35/1.42 % (419099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.35/1.42 % (419099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.35/1.42 % (419099)CaDiCaL version: 2.1.3
% 4.35/1.42 % (419099)Termination reason: Instruction limit
% 4.35/1.42 % (419099)Termination phase: Saturation
% 4.35/1.42 % (419099)Time elapsed: 0.056 s
% 4.35/1.42 % (419099)Peak memory usage: 115 MB
% 4.35/1.42 % (419099)Instructions burned: 47 (million)
% 4.35/1.42 % (419120)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=96159996:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.35/1.42 % (419120)Instruction limit reached!
% 4.35/1.42 % (419120)------------------------------
% 4.35/1.42 % (419120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419120)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419120)Termination reason: Instruction limit
% 6.05/1.64 % (419120)Termination phase: Saturation
% 6.05/1.64 % (419120)Time elapsed: 0.006 s
% 6.05/1.64 % (419120)Peak memory usage: 89 MB
% 6.05/1.64 % (419120)Instructions burned: 14 (million)
% 6.05/1.64 % (419095)Instruction limit reached!
% 6.05/1.64 % (419095)------------------------------
% 6.05/1.64 % (419095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419095)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419095)Termination reason: Instruction limit
% 6.05/1.64 % (419095)Termination phase: Saturation
% 6.05/1.64 % (419095)Time elapsed: 0.138 s
% 6.05/1.64 % (419095)Peak memory usage: 116 MB
% 6.05/1.64 % (419095)Instructions burned: 201 (million)
% 6.05/1.64 % (419143)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=2885474996:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 6.05/1.64 % (419094)Instruction limit reached!
% 6.05/1.64 % (419094)------------------------------
% 6.05/1.64 % (419094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419094)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419094)Termination reason: Instruction limit
% 6.05/1.64 % (419094)Termination phase: Saturation
% 6.05/1.64 % (419094)Time elapsed: 0.213 s
% 6.05/1.64 % (419094)Peak memory usage: 116 MB
% 6.05/1.64 % (419094)Instructions burned: 307 (million)
% 6.05/1.64 % (419146)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1432594415:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 6.05/1.64 % (419143)Instruction limit reached!
% 6.05/1.64 % (419143)------------------------------
% 6.05/1.64 % (419143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419143)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419143)Termination reason: Instruction limit
% 6.05/1.64 % (419143)Termination phase: Saturation
% 6.05/1.64 % (419143)Time elapsed: 0.039 s
% 6.05/1.64 % (419143)Peak memory usage: 88 MB
% 6.05/1.64 % (419143)Instructions burned: 30 (million)
% 6.05/1.64 % (419146)Instruction limit reached!
% 6.05/1.64 % (419146)------------------------------
% 6.05/1.64 % (419146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419146)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419146)Termination reason: Instruction limit
% 6.05/1.64 % (419146)Termination phase: Saturation
% 6.05/1.64 % (419146)Time elapsed: 0.020 s
% 6.05/1.64 % (419146)Peak memory usage: 90 MB
% 6.05/1.64 % (419146)Instructions burned: 16 (million)
% 6.05/1.64 % (419152)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=67720099:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.05/1.64 % (419152)Instruction limit reached!
% 6.05/1.64 % (419152)------------------------------
% 6.05/1.64 % (419152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (419152)CaDiCaL version: 2.1.3
% 6.05/1.64 % (419152)Termination reason: Instruction limit
% 6.05/1.64 % (419152)Termination phase: Saturation
% 6.05/1.64 % (419152)Time elapsed: 0.025 s
% 6.05/1.64 % (419152)Peak memory usage: 89 MB
% 6.05/1.64 % (419152)Instructions burned: 24 (million)
% 6.05/1.64 % (419162)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3821378443:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 6.05/1.64 % (419158)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=2512318181:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 6.05/1.64 % (419158)Instruction limit reached!
% 6.05/1.64 % (419158)------------------------------
% 6.05/1.64 % (419158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (419158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419158)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419158)Termination reason: Instruction limit
% 7.42/1.93 % (419158)Termination phase: Saturation
% 7.42/1.93 % (419158)Time elapsed: 0.036 s
% 7.42/1.93 % (419158)Peak memory usage: 89 MB
% 7.42/1.93 % (419158)Instructions burned: 28 (million)
% 7.42/1.93 % (419162)Instruction limit reached!
% 7.42/1.93 % (419162)------------------------------
% 7.42/1.93 % (419162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.93 % (419162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419162)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419162)Termination reason: Instruction limit
% 7.42/1.93 % (419162)Termination phase: Saturation
% 7.42/1.93 % (419162)Time elapsed: 0.070 s
% 7.42/1.93 % (419162)Peak memory usage: 88 MB
% 7.42/1.93 % (419162)Instructions burned: 86 (million)
% 7.42/1.93 % (419183)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1980792164:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 7.42/1.93 % (419183)Instruction limit reached!
% 7.42/1.93 % (419183)------------------------------
% 7.42/1.93 % (419183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.93 % (419183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419183)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419183)Termination reason: Instruction limit
% 7.42/1.93 % (419183)Termination phase: Saturation
% 7.42/1.93 % (419183)Time elapsed: 0.004 s
% 7.42/1.93 % (419183)Peak memory usage: 88 MB
% 7.42/1.93 % (419183)Instructions burned: 2 (million)
% 7.42/1.93 % (419195)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3283577085:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 7.42/1.93 % (419198)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3550929893:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.42/1.93 % (419199)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1249888603:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.42/1.93 % (419198)Instruction limit reached!
% 7.42/1.93 % (419198)------------------------------
% 7.42/1.93 % (419198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.93 % (419198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419198)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419198)Termination reason: Instruction limit
% 7.42/1.93 % (419198)Termination phase: Saturation
% 7.42/1.93 % (419198)Time elapsed: 0.006 s
% 7.42/1.93 % (419198)Peak memory usage: 88 MB
% 7.42/1.93 % (419198)Instructions burned: 4 (million)
% 7.42/1.93 % (419195)Instruction limit reached!
% 7.42/1.93 % (419195)------------------------------
% 7.42/1.93 % (419195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.93 % (419195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419195)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419195)Termination reason: Instruction limit
% 7.42/1.93 % (419195)Termination phase: Saturation
% 7.42/1.93 % (419195)Time elapsed: 0.110 s
% 7.42/1.93 % (419195)Peak memory usage: 90 MB
% 7.42/1.93 % (419195)Instructions burned: 182 (million)
% 7.42/1.93 % (419208)lrs+10_1_thi=all:si=on:fd=off:random_seed=1865853520:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 7.42/1.93 % (419213)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=2833198116:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 7.42/1.93 % (419213)Instruction limit reached!
% 7.42/1.93 % (419213)------------------------------
% 7.42/1.93 % (419213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.42/1.93 % (419213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.42/1.93 % (419213)CaDiCaL version: 2.1.3
% 7.42/1.93 % (419213)Termination reason: Instruction limit
% 7.42/1.93 % (419213)Termination phase: Saturation
% 7.42/1.93 % (419213)Time elapsed: 0.011 s
% 7.42/1.93 % (419213)Peak memory usage: 89 MB
% 7.42/1.93 % (419213)Instructions burned: 8 (million)
% 7.42/1.93 % (419216)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1218550139:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 7.42/1.93 % (419216)Instruction limit reached!
% 7.42/1.93 % (419216)------------------------------
% 11.04/2.33 % (419216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419216)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419216)Termination reason: Instruction limit
% 11.04/2.33 % (419216)Termination phase: Saturation
% 11.04/2.33 % (419216)Time elapsed: 0.003 s
% 11.04/2.33 % (419216)Peak memory usage: 88 MB
% 11.04/2.33 % (419216)Instructions burned: 2 (million)
% 11.04/2.33 % (419208)Instruction limit reached!
% 11.04/2.33 % (419208)------------------------------
% 11.04/2.33 % (419208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419208)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419208)Termination reason: Instruction limit
% 11.04/2.33 % (419208)Termination phase: Saturation
% 11.04/2.33 % (419208)Time elapsed: 0.096 s
% 11.04/2.33 % (419208)Peak memory usage: 116 MB
% 11.04/2.33 % (419208)Instructions burned: 53 (million)
% 11.04/2.33 % (419199)Instruction limit reached!
% 11.04/2.33 % (419199)------------------------------
% 11.04/2.33 % (419199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419199)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419199)Termination reason: Instruction limit
% 11.04/2.33 % (419199)Termination phase: Saturation
% 11.04/2.33 % (419199)Time elapsed: 0.138 s
% 11.04/2.33 % (419199)Peak memory usage: 133 MB
% 11.04/2.33 % (419199)Instructions burned: 66 (million)
% 11.04/2.33 % (419220)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1825215919:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 11.04/2.33 % (419220)Instruction limit reached!
% 11.04/2.33 % (419220)------------------------------
% 11.04/2.33 % (419220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419220)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419220)Termination reason: Instruction limit
% 11.04/2.33 % (419220)Termination phase: Saturation
% 11.04/2.33 % (419220)Time elapsed: 0.004 s
% 11.04/2.33 % (419220)Peak memory usage: 89 MB
% 11.04/2.33 % (419220)Instructions burned: 2 (million)
% 11.04/2.33 % (419228)dis+10_1_si=on:random_seed=3417769833:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 11.04/2.33 % (419228)Instruction limit reached!
% 11.04/2.33 % (419228)------------------------------
% 11.04/2.33 % (419228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419228)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419228)Termination reason: Instruction limit
% 11.04/2.33 % (419228)Termination phase: Saturation
% 11.04/2.33 % (419228)Time elapsed: 0.013 s
% 11.04/2.33 % (419228)Peak memory usage: 88 MB
% 11.04/2.33 % (419228)Instructions burned: 10 (million)
% 11.04/2.33 % (419227)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=865043623:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 11.04/2.33 % (419240)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4242494316:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2992 on theBenchmark for (2992ds/35Mi)
% 11.04/2.33 % (419240)Instruction limit reached!
% 11.04/2.33 % (419240)------------------------------
% 11.04/2.33 % (419240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/2.33 % (419240)CaDiCaL version: 2.1.3
% 11.04/2.33 % (419240)Termination reason: Instruction limit
% 11.04/2.33 % (419240)Termination phase: Saturation
% 11.04/2.33 % (419240)Time elapsed: 0.032 s
% 11.04/2.33 % (419240)Peak memory usage: 89 MB
% 11.04/2.33 % (419240)Instructions burned: 36 (million)
% 11.04/2.33 % (419242)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3352587905:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.04/2.33 % (419242)Instruction limit reached!
% 11.04/2.33 % (419242)------------------------------
% 11.04/2.33 % (419242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/2.33 % (419242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419242)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419242)Termination reason: Instruction limit
% 12.52/2.84 % (419242)Termination phase: Saturation
% 12.52/2.84 % (419242)Time elapsed: 0.002 s
% 12.52/2.84 % (419242)Peak memory usage: 88 MB
% 12.52/2.84 % (419242)Instructions burned: 2 (million)
% 12.52/2.84 % (419239)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1725752147:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 12.52/2.84 % (419239)Refutation not found, incomplete strategy
% 12.52/2.84 % (419239)------------------------------
% 12.52/2.84 % (419239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419239)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419239)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.84 % (419239)Time elapsed: 0.005 s
% 12.52/2.84 % (419239)Peak memory usage: 88 MB
% 12.52/2.84 % (419239)Instructions burned: 3 (million)
% 12.52/2.84 % (419245)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1263063378:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 12.52/2.84 % (419244)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1028091542:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 12.52/2.84 % (419245)Refutation not found, incomplete strategy
% 12.52/2.84 % (419245)------------------------------
% 12.52/2.84 % (419245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419245)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419245)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.84 % (419245)Time elapsed: 0.004 s
% 12.52/2.84 % (419245)Peak memory usage: 88 MB
% 12.52/2.84 % (419245)Instructions burned: 2 (million)
% 12.52/2.84 % (419244)Instruction limit reached!
% 12.52/2.84 % (419244)------------------------------
% 12.52/2.84 % (419244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419244)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419244)Termination reason: Instruction limit
% 12.52/2.84 % (419244)Termination phase: Saturation
% 12.52/2.84 % (419244)Time elapsed: 0.011 s
% 12.52/2.84 % (419244)Peak memory usage: 88 MB
% 12.52/2.84 % (419244)Instructions burned: 8 (million)
% 12.52/2.84 % (419227)Instruction limit reached!
% 12.52/2.84 % (419227)------------------------------
% 12.52/2.84 % (419227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419227)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419227)Termination reason: Instruction limit
% 12.52/2.84 % (419227)Termination phase: Saturation
% 12.52/2.84 % (419227)Time elapsed: 0.167 s
% 12.52/2.84 % (419227)Peak memory usage: 116 MB
% 12.52/2.84 % (419227)Instructions burned: 127 (million)
% 12.52/2.84 % (419247)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3011334588:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/13Mi)
% 12.52/2.84 % (419250)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2073553059:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 12.52/2.84 % (419247)Instruction limit reached!
% 12.52/2.84 % (419247)------------------------------
% 12.52/2.84 % (419247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419247)CaDiCaL version: 2.1.3
% 12.52/2.84 % (419247)Termination reason: Instruction limit
% 12.52/2.84 % (419247)Termination phase: Saturation
% 12.52/2.84 % (419247)Time elapsed: 0.046 s
% 12.52/2.84 % (419247)Peak memory usage: 116 MB
% 12.52/2.84 % (419247)Instructions burned: 13 (million)
% 12.52/2.84 % (419253)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1664827012:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 12.52/2.84 % (419253)Instruction limit reached!
% 12.52/2.84 % (419253)------------------------------
% 12.52/2.84 % (419253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.84 % (419253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.84 % (419253)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419253)Termination reason: Instruction limit
% 17.37/3.15 % (419253)Termination phase: Saturation
% 17.37/3.15 % (419253)Time elapsed: 0.014 s
% 17.37/3.15 % (419253)Peak memory usage: 89 MB
% 17.37/3.15 % (419253)Instructions burned: 10 (million)
% 17.37/3.15 % (419257)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=561470183:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi)
% 17.37/3.15 % (419250)Instruction limit reached!
% 17.37/3.15 % (419250)------------------------------
% 17.37/3.15 % (419250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.37/3.15 % (419250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.37/3.15 % (419250)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419250)Termination reason: Instruction limit
% 17.37/3.15 % (419250)Termination phase: Saturation
% 17.37/3.15 % (419250)Time elapsed: 0.199 s
% 17.37/3.15 % (419250)Peak memory usage: 115 MB
% 17.37/3.15 % (419250)Instructions burned: 227 (million)
% 17.37/3.15 % (419258)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=3197560932:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 17.37/3.15 % (419257)Instruction limit reached!
% 17.37/3.15 % (419257)------------------------------
% 17.37/3.15 % (419257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.37/3.15 % (419257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.37/3.15 % (419257)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419257)Termination reason: Instruction limit
% 17.37/3.15 % (419257)Termination phase: Saturation
% 17.37/3.15 % (419257)Time elapsed: 0.078 s
% 17.37/3.15 % (419257)Peak memory usage: 133 MB
% 17.37/3.15 % (419257)Instructions burned: 71 (million)
% 17.37/3.15 % (419239)------------------------------
% 17.37/3.15 % (419239)------------------------------
% 17.37/3.15 % (419245)------------------------------
% 17.37/3.15 % (419245)------------------------------
% 17.37/3.15 % (419263)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=1284587769:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi)
% 17.37/3.15 % (419258)Instruction limit reached!
% 17.37/3.15 % (419258)------------------------------
% 17.37/3.15 % (419258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.37/3.15 % (419258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.37/3.15 % (419258)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419258)Termination reason: Instruction limit
% 17.37/3.15 % (419258)Termination phase: Saturation
% 17.37/3.15 % (419258)Time elapsed: 0.098 s
% 17.37/3.15 % (419258)Peak memory usage: 90 MB
% 17.37/3.15 % (419258)Instructions burned: 75 (million)
% 17.37/3.15 % (419270)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4206348235:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 17.37/3.15 % (419275)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3636822623:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2986 on theBenchmark for (2986ds/40Mi)
% 17.37/3.15 % (419277)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2466482921:i=307:rtra=on:gtg=exists_top_2985 on theBenchmark for (2985ds/307Mi)
% 17.37/3.15 % (419273)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1617252371:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 17.37/3.15 % (419275)Instruction limit reached!
% 17.37/3.15 % (419275)------------------------------
% 17.37/3.15 % (419275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.37/3.15 % (419275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.37/3.15 % (419275)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419275)Termination reason: Instruction limit
% 17.37/3.15 % (419275)Termination phase: Saturation
% 17.37/3.15 % (419275)Time elapsed: 0.057 s
% 17.37/3.15 % (419275)Peak memory usage: 133 MB
% 17.37/3.15 % (419275)Instructions burned: 40 (million)
% 17.37/3.15 % (419270)Instruction limit reached!
% 17.37/3.15 % (419270)------------------------------
% 17.37/3.15 % (419270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.37/3.15 % (419270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.37/3.15 % (419270)CaDiCaL version: 2.1.3
% 17.37/3.15 % (419270)Termination reason: Instruction limit
% 17.37/3.15 % (419270)Termination phase: Saturation
% 20.17/3.66 % (419270)Time elapsed: 0.143 s
% 20.17/3.66 % (419270)Peak memory usage: 116 MB
% 20.17/3.66 % (419270)Instructions burned: 131 (million)
% 20.17/3.66 % (419278)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=608111648:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/598Mi)
% 20.17/3.66 % (419280)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=128076614:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 20.17/3.66 % (419263)Instruction limit reached!
% 20.17/3.66 % (419263)------------------------------
% 20.17/3.66 % (419263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.17/3.66 % (419263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.17/3.66 % (419263)CaDiCaL version: 2.1.3
% 20.17/3.66 % (419263)Termination reason: Instruction limit
% 20.17/3.66 % (419263)Termination phase: Saturation
% 20.17/3.66 % (419263)Time elapsed: 0.290 s
% 20.17/3.66 % (419263)Peak memory usage: 90 MB
% 20.17/3.66 % (419263)Instructions burned: 294 (million)
% 20.17/3.66 % (419273)Instruction limit reached!
% 20.17/3.66 % (419273)------------------------------
% 20.17/3.66 % (419273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.17/3.66 % (419273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.17/3.66 % (419273)CaDiCaL version: 2.1.3
% 20.17/3.66 % (419273)Termination reason: Instruction limit
% 20.17/3.66 % (419273)Termination phase: Saturation
% 20.17/3.66 % (419273)Time elapsed: 0.207 s
% 20.17/3.66 % (419273)Peak memory usage: 133 MB
% 20.17/3.66 % (419273)Instructions burned: 131 (million)
% 20.17/3.66 % (419277)Instruction limit reached!
% 20.17/3.66 % (419277)------------------------------
% 20.17/3.66 % (419277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.17/3.66 % (419277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.17/3.66 % (419277)CaDiCaL version: 2.1.3
% 20.17/3.66 % (419277)Termination reason: Instruction limit
% 20.17/3.66 % (419277)Termination phase: Saturation
% 20.17/3.66 % (419277)Time elapsed: 0.275 s
% 20.17/3.66 % (419277)Peak memory usage: 90 MB
% 20.17/3.66 % (419277)Instructions burned: 307 (million)
% 20.17/3.66 % (419285)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=4039417347:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 20.17/3.66 % (419280)Instruction limit reached!
% 20.17/3.66 % (419280)------------------------------
% 20.17/3.66 % (419280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.17/3.66 % (419280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.17/3.66 % (419280)CaDiCaL version: 2.1.3
% 20.17/3.66 % (419280)Termination reason: Instruction limit
% 20.17/3.66 % (419280)Termination phase: Saturation
% 20.17/3.66 % (419280)Time elapsed: 0.148 s
% 20.17/3.66 % (419280)Peak memory usage: 116 MB
% 20.17/3.66 % (419280)Instructions burned: 132 (million)
% 20.17/3.66 % (419291)dis+10_1_si=on:random_seed=1034623568:s2a=on:i=1000:rtra=on:gtg=exists_all_2983 on theBenchmark for (2983ds/1000Mi)
% 20.17/3.66 % (419293)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1334673455:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 20.17/3.66 % (419294)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1056748798:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 20.17/3.66 % (419295)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=419939506:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 20.17/3.66 % (419285)Instruction limit reached!
% 20.17/3.66 % (419285)------------------------------
% 20.17/3.66 % (419285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.17/3.66 % (419285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.17/3.66 % (419285)CaDiCaL version: 2.1.3
% 20.17/3.66 % (419285)Termination reason: Instruction limit
% 20.17/3.66 % (419285)Termination phase: Saturation
% 20.17/3.66 % (419285)Time elapsed: 0.248 s
% 20.17/3.66 % (419285)Peak memory usage: 115 MB
% 20.17/3.66 % (419285)Instructions burned: 260 (million)
% 20.17/3.66 % (419298)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2495315153:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi)
% 20.17/3.66 % (419294)Instruction limit reached!
% 24.74/4.19 % (419294)------------------------------
% 24.74/4.19 % (419294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419294)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419294)Termination reason: Instruction limit
% 24.74/4.19 % (419294)Termination phase: Saturation
% 24.74/4.19 % (419294)Time elapsed: 0.157 s
% 24.74/4.19 % (419294)Peak memory usage: 90 MB
% 24.74/4.19 % (419294)Instructions burned: 142 (million)
% 24.74/4.19 % (419295)Instruction limit reached!
% 24.74/4.19 % (419295)------------------------------
% 24.74/4.19 % (419295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419295)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419295)Termination reason: Instruction limit
% 24.74/4.19 % (419295)Termination phase: Saturation
% 24.74/4.19 % (419295)Time elapsed: 0.102 s
% 24.74/4.19 % (419295)Peak memory usage: 115 MB
% 24.74/4.19 % (419295)Instructions burned: 66 (million)
% 24.74/4.19 % (419278)Instruction limit reached!
% 24.74/4.19 % (419278)------------------------------
% 24.74/4.19 % (419278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419278)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419278)Termination reason: Instruction limit
% 24.74/4.19 % (419278)Termination phase: Saturation
% 24.74/4.19 % (419278)Time elapsed: 0.590 s
% 24.74/4.19 % (419278)Peak memory usage: 136 MB
% 24.74/4.19 % (419278)Instructions burned: 598 (million)
% 24.74/4.19 % (419298)Instruction limit reached!
% 24.74/4.19 % (419298)------------------------------
% 24.74/4.19 % (419298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419298)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419298)Termination reason: Instruction limit
% 24.74/4.19 % (419298)Termination phase: Saturation
% 24.74/4.19 % (419298)Time elapsed: 0.123 s
% 24.74/4.19 % (419298)Peak memory usage: 89 MB
% 24.74/4.19 % (419298)Instructions burned: 122 (million)
% 24.74/4.19 % (419293)Instruction limit reached!
% 24.74/4.19 % (419293)------------------------------
% 24.74/4.19 % (419293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419293)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419293)Termination reason: Instruction limit
% 24.74/4.19 % (419293)Termination phase: Saturation
% 24.74/4.19 % (419293)Time elapsed: 0.383 s
% 24.74/4.19 % (419293)Peak memory usage: 91 MB
% 24.74/4.19 % (419293)Instructions burned: 383 (million)
% 24.74/4.19 % (419304)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=2712705053:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 24.74/4.19 % (419291)Instruction limit reached!
% 24.74/4.19 % (419291)------------------------------
% 24.74/4.19 % (419291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419291)CaDiCaL version: 2.1.3
% 24.74/4.19 % (419291)Termination reason: Instruction limit
% 24.74/4.19 % (419291)Termination phase: Saturation
% 24.74/4.19 % (419291)Time elapsed: 0.514 s
% 24.74/4.19 % (419291)Peak memory usage: 93 MB
% 24.74/4.19 % (419291)Instructions burned: 1000 (million)
% 24.74/4.19 % (419307)dis+1010_1_to=kbo:si=on:random_seed=3196543726:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 24.74/4.19 % (419306)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=3181025678:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 24.74/4.19 % (419308)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2380899748:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2977 on theBenchmark for (2977ds/329Mi)
% 24.74/4.19 % (419306)Refutation not found, incomplete strategy
% 24.74/4.19 % (419306)------------------------------
% 24.74/4.19 % (419306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.74/4.19 % (419306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.74/4.19 % (419306)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419306)Termination reason: Refutation not found, incomplete strategy
% 26.52/4.68 % (419306)Time elapsed: 0.052 s
% 26.52/4.68 % (419306)Peak memory usage: 115 MB
% 26.52/4.68 % (419306)Instructions burned: 16 (million)
% 26.52/4.68 % (419309)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1727828459:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi)
% 26.52/4.68 % (419304)Instruction limit reached!
% 26.52/4.68 % (419304)------------------------------
% 26.52/4.68 % (419304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419304)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419304)Termination reason: Instruction limit
% 26.52/4.68 % (419304)Termination phase: Saturation
% 26.52/4.68 % (419304)Time elapsed: 0.172 s
% 26.52/4.68 % (419304)Peak memory usage: 116 MB
% 26.52/4.68 % (419304)Instructions burned: 128 (million)
% 26.52/4.68 % (419312)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3615206726:thitd=on:i=215:nm=0:rtra=on:ev=force_2976 on theBenchmark for (2976ds/215Mi)
% 26.52/4.68 % (419314)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2037973252:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi)
% 26.52/4.68 % (419307)Instruction limit reached!
% 26.52/4.68 % (419307)------------------------------
% 26.52/4.68 % (419307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419307)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419307)Termination reason: Instruction limit
% 26.52/4.68 % (419307)Termination phase: Saturation
% 26.52/4.68 % (419307)Time elapsed: 0.205 s
% 26.52/4.68 % (419307)Peak memory usage: 90 MB
% 26.52/4.68 % (419307)Instructions burned: 175 (million)
% 26.52/4.68 % (419319)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3595877067:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi)
% 26.52/4.68 % (419308)Instruction limit reached!
% 26.52/4.68 % (419308)------------------------------
% 26.52/4.68 % (419308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419308)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419308)Termination reason: Instruction limit
% 26.52/4.68 % (419308)Termination phase: Saturation
% 26.52/4.68 % (419308)Time elapsed: 0.349 s
% 26.52/4.68 % (419308)Peak memory usage: 117 MB
% 26.52/4.68 % (419308)Instructions burned: 337 (million)
% 26.52/4.68 % (419314)Instruction limit reached!
% 26.52/4.68 % (419314)------------------------------
% 26.52/4.68 % (419314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419314)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419314)Termination reason: Instruction limit
% 26.52/4.68 % (419314)Termination phase: Saturation
% 26.52/4.68 % (419314)Time elapsed: 0.214 s
% 26.52/4.68 % (419314)Peak memory usage: 117 MB
% 26.52/4.68 % (419314)Instructions burned: 356 (million)
% 26.52/4.68 % (419312)Instruction limit reached!
% 26.52/4.68 % (419312)------------------------------
% 26.52/4.68 % (419312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419312)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419312)Termination reason: Instruction limit
% 26.52/4.68 % (419312)Termination phase: Saturation
% 26.52/4.68 % (419312)Time elapsed: 0.278 s
% 26.52/4.68 % (419312)Peak memory usage: 135 MB
% 26.52/4.68 % (419312)Instructions burned: 215 (million)
% 26.52/4.68 % (419306)------------------------------
% 26.52/4.68 % (419306)------------------------------
% 26.52/4.68 % (419322)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3313018351:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi)
% 26.52/4.68 % (419309)Instruction limit reached!
% 26.52/4.68 % (419309)------------------------------
% 26.52/4.68 % (419309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.52/4.68 % (419309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.52/4.68 % (419309)CaDiCaL version: 2.1.3
% 26.52/4.68 % (419309)Termination reason: Instruction limit
% 26.52/4.68 % (419309)Termination phase: Saturation
% 31.06/5.13 % (419309)Time elapsed: 0.429 s
% 31.06/5.13 % (419309)Peak memory usage: 133 MB
% 31.06/5.13 % (419309)Instructions burned: 483 (million)
% 31.06/5.13 % (419319)Instruction limit reached!
% 31.06/5.13 % (419319)------------------------------
% 31.06/5.13 % (419319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.13 % (419319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.13 % (419319)CaDiCaL version: 2.1.3
% 31.06/5.13 % (419319)Termination reason: Instruction limit
% 31.06/5.13 % (419319)Termination phase: Saturation
% 31.06/5.13 % (419319)Time elapsed: 0.238 s
% 31.06/5.13 % (419319)Peak memory usage: 90 MB
% 31.06/5.13 % (419319)Instructions burned: 295 (million)
% 31.06/5.13 % (419324)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3018990349:i=281:gtgl=2:rtra=on:gtg=all_2971 on theBenchmark for (2971ds/281Mi)
% 31.06/5.13 % (419326)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1717320793:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2971 on theBenchmark for (2971ds/321Mi)
% 31.06/5.13 % (419325)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=4186599441:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 31.06/5.13 % (419327)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1625661044:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi)
% 31.06/5.13 % (419324)Instruction limit reached!
% 31.06/5.13 % (419324)------------------------------
% 31.06/5.13 % (419324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.13 % (419324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.13 % (419324)CaDiCaL version: 2.1.3
% 31.06/5.13 % (419324)Termination reason: Instruction limit
% 31.06/5.13 % (419324)Termination phase: Saturation
% 31.06/5.13 % (419324)Time elapsed: 0.182 s
% 31.06/5.13 % (419324)Peak memory usage: 117 MB
% 31.06/5.13 % (419324)Instructions burned: 283 (million)
% 31.06/5.13 % (419332)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2046181806:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi)
% 31.06/5.13 % (419326)Instruction limit reached!
% 31.06/5.13 % (419326)------------------------------
% 31.06/5.13 % (419326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.13 % (419326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.13 % (419326)CaDiCaL version: 2.1.3
% 31.06/5.13 % (419326)Termination reason: Instruction limit
% 31.06/5.13 % (419326)Termination phase: Saturation
% 31.06/5.13 % (419326)Time elapsed: 0.219 s
% 31.06/5.13 % (419326)Peak memory usage: 114 MB
% 31.06/5.13 % (419326)Instructions burned: 321 (million)
% 31.06/5.13 % (419334)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=2145133776:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi)
% 31.06/5.13 % (419322)Instruction limit reached!
% 31.06/5.13 % (419322)------------------------------
% 31.06/5.13 % (419322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.13 % (419322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.13 % (419322)CaDiCaL version: 2.1.3
% 31.06/5.13 % (419322)Termination reason: Instruction limit
% 31.06/5.13 % (419322)Termination phase: Saturation
% 31.06/5.13 % (419322)Time elapsed: 0.359 s
% 31.06/5.13 % (419322)Peak memory usage: 117 MB
% 31.06/5.13 % (419322)Instructions burned: 328 (million)
% 31.06/5.13 % (419339)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=860663824:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 31.06/5.13 % (419327)Instruction limit reached!
% 31.06/5.13 % (419327)------------------------------
% 31.06/5.13 % (419327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.13 % (419327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.13 % (419327)CaDiCaL version: 2.1.3
% 31.06/5.13 % (419327)Termination reason: Instruction limit
% 31.06/5.13 % (419327)Termination phase: Saturation
% 31.06/5.13 % (419327)Time elapsed: 0.317 s
% 31.06/5.13 % (419327)Peak memory usage: 116 MB
% 31.06/5.13 % (419327)Instructions burned: 417 (million)
% 31.06/5.13 % (419325)Instruction limit reached!
% 31.06/5.13 % (419325)------------------------------
% 31.06/5.13 % (419325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419325)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419325)Termination reason: Instruction limit
% 35.76/6.01 % (419325)Termination phase: Saturation
% 35.76/6.01 % (419325)Time elapsed: 0.434 s
% 35.76/6.01 % (419325)Peak memory usage: 89 MB
% 35.76/6.01 % (419325)Instructions burned: 484 (million)
% 35.76/6.01 % (419342)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3089070475:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi)
% 35.76/6.01 % (419343)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=873258734:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2966 on theBenchmark for (2966ds/513Mi)
% 35.76/6.01 % (419339)Instruction limit reached!
% 35.76/6.01 % (419339)------------------------------
% 35.76/6.01 % (419339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419339)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419339)Termination reason: Instruction limit
% 35.76/6.01 % (419339)Termination phase: Saturation
% 35.76/6.01 % (419339)Time elapsed: 0.216 s
% 35.76/6.01 % (419339)Peak memory usage: 117 MB
% 35.76/6.01 % (419339)Instructions burned: 376 (million)
% 35.76/6.01 % (419334)Instruction limit reached!
% 35.76/6.01 % (419334)------------------------------
% 35.76/6.01 % (419334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419334)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419334)Termination reason: Instruction limit
% 35.76/6.01 % (419334)Termination phase: Saturation
% 35.76/6.01 % (419334)Time elapsed: 0.354 s
% 35.76/6.01 % (419334)Peak memory usage: 134 MB
% 35.76/6.01 % (419334)Instructions burned: 276 (million)
% 35.76/6.01 % (419345)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1619964583:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi)
% 35.76/6.01 % (419346)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3093288399:i=359:rtra=on:gtg=exists_top:ss=axioms_2964 on theBenchmark for (2964ds/359Mi)
% 35.76/6.01 % (419346)Refutation not found, incomplete strategy
% 35.76/6.01 % (419346)------------------------------
% 35.76/6.01 % (419346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419346)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419346)Termination reason: Refutation not found, incomplete strategy
% 35.76/6.01 % (419346)Time elapsed: 0.005 s
% 35.76/6.01 % (419346)Peak memory usage: 89 MB
% 35.76/6.01 % (419346)Instructions burned: 2 (million)
% 35.76/6.01 % (419332)Instruction limit reached!
% 35.76/6.01 % (419332)------------------------------
% 35.76/6.01 % (419332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419332)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419332)Termination reason: Instruction limit
% 35.76/6.01 % (419332)Termination phase: Saturation
% 35.76/6.01 % (419332)Time elapsed: 0.512 s
% 35.76/6.01 % (419332)Peak memory usage: 118 MB
% 35.76/6.01 % (419332)Instructions burned: 471 (million)
% 35.76/6.01 % (419349)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3974215901:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi)
% 35.76/6.01 % (419350)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=837451445:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/261Mi)
% 35.76/6.01 % (419350)Refutation not found, incomplete strategy
% 35.76/6.01 % (419350)------------------------------
% 35.76/6.01 % (419350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.76/6.01 % (419350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/6.01 % (419350)CaDiCaL version: 2.1.3
% 35.76/6.01 % (419350)Termination reason: Refutation not found, incomplete strategy
% 35.76/6.01 % (419350)Time elapsed: 0.061 s
% 35.76/6.01 % (419350)Peak memory usage: 115 MB
% 35.76/6.01 % (419350)Instructions burned: 24 (million)
% 35.76/6.01 % (419342)Instruction limit reached!
% 41.42/6.75 % (419342)------------------------------
% 41.42/6.75 % (419342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.42/6.75 % (419342)CaDiCaL version: 2.1.3
% 41.42/6.75 % (419342)Termination reason: Instruction limit
% 41.42/6.75 % (419342)Termination phase: Saturation
% 41.42/6.75 % (419342)Time elapsed: 0.472 s
% 41.42/6.75 % (419342)Peak memory usage: 118 MB
% 41.42/6.75 % (419342)Instructions burned: 388 (million)
% 41.42/6.75 % (419343)Instruction limit reached!
% 41.42/6.75 % (419343)------------------------------
% 41.42/6.75 % (419343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.42/6.75 % (419343)CaDiCaL version: 2.1.3
% 41.42/6.75 % (419343)Termination reason: Instruction limit
% 41.42/6.75 % (419343)Termination phase: Saturation
% 41.42/6.75 % (419343)Time elapsed: 0.466 s
% 41.42/6.75 % (419343)Peak memory usage: 90 MB
% 41.42/6.75 % (419343)Instructions burned: 513 (million)
% 41.42/6.75 % (419349)Instruction limit reached!
% 41.42/6.75 % (419349)------------------------------
% 41.42/6.75 % (419349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.42/6.75 % (419349)CaDiCaL version: 2.1.3
% 41.42/6.75 % (419349)Termination reason: Instruction limit
% 41.42/6.75 % (419349)Termination phase: Saturation
% 41.42/6.75 % (419349)Time elapsed: 0.216 s
% 41.42/6.75 % (419349)Peak memory usage: 118 MB
% 41.42/6.75 % (419349)Instructions burned: 341 (million)
% 41.42/6.75 % (419353)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=2173997166:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi)
% 41.42/6.75 % (419345)Instruction limit reached!
% 41.42/6.75 % (419345)------------------------------
% 41.42/6.75 % (419345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.42/6.75 % (419345)CaDiCaL version: 2.1.3
% 41.42/6.75 % (419345)Termination reason: Instruction limit
% 41.42/6.75 % (419345)Termination phase: Saturation
% 41.42/6.75 % (419345)Time elapsed: 0.396 s
% 41.42/6.75 % (419345)Peak memory usage: 134 MB
% 41.42/6.75 % (419345)Instructions burned: 334 (million)
% 41.42/6.75 % (419346)------------------------------
% 41.42/6.75 % (419346)------------------------------
% 41.42/6.75 % (419359)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1916302866:i=4428:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/4428Mi)
% 41.42/6.75 % (419356)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=537589110:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 41.42/6.75 % (419353)Instruction limit reached!
% 41.42/6.75 % (419353)------------------------------
% 41.42/6.75 % (419353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.42/6.75 % (419353)CaDiCaL version: 2.1.3
% 41.42/6.75 % (419353)Termination reason: Instruction limit
% 41.42/6.75 % (419353)Termination phase: Saturation
% 41.42/6.75 % (419353)Time elapsed: 0.225 s
% 41.42/6.75 % (419353)Peak memory usage: 116 MB
% 41.42/6.75 % (419353)Instructions burned: 236 (million)
% 41.42/6.75 % (419357)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=889121903:i=146:doe=on:rtra=on_2959 on theBenchmark for (2959ds/146Mi)
% 41.42/6.75 % (419363)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=1397150067:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi)
% 41.42/6.75 % (419350)------------------------------
% 41.42/6.75 % (419350)------------------------------
% 41.42/6.75 % (419362)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=4231123070:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi)
% 41.42/6.75 % (419357)Instruction limit reached!
% 41.42/6.75 % (419357)------------------------------
% 41.42/6.75 % (419357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.42/6.75 % (419357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419357)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419357)Termination reason: Instruction limit
% 46.97/7.48 % (419357)Termination phase: Saturation
% 46.97/7.48 % (419357)Time elapsed: 0.161 s
% 46.97/7.48 % (419357)Peak memory usage: 90 MB
% 46.97/7.48 % (419357)Instructions burned: 146 (million)
% 46.97/7.48 % (419356)Instruction limit reached!
% 46.97/7.48 % (419356)------------------------------
% 46.97/7.48 % (419356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.97/7.48 % (419356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419356)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419356)Termination reason: Instruction limit
% 46.97/7.48 % (419356)Termination phase: Saturation
% 46.97/7.48 % (419356)Time elapsed: 0.307 s
% 46.97/7.48 % (419356)Peak memory usage: 92 MB
% 46.97/7.48 % (419356)Instructions burned: 273 (million)
% 46.97/7.48 % (419367)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2359092918:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi)
% 46.97/7.48 % (419370)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2938811727:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi)
% 46.97/7.48 % (419371)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2542067279:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi)
% 46.97/7.48 % (419371)Refutation not found, incomplete strategy
% 46.97/7.48 % (419371)------------------------------
% 46.97/7.48 % (419371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.97/7.48 % (419371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419371)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419371)Termination reason: Refutation not found, incomplete strategy
% 46.97/7.48 % (419371)Time elapsed: 0.033 s
% 46.97/7.48 % (419371)Peak memory usage: 115 MB
% 46.97/7.48 % (419371)Instructions burned: 10 (million)
% 46.97/7.48 % (419362)Instruction limit reached!
% 46.97/7.48 % (419362)------------------------------
% 46.97/7.48 % (419362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.97/7.48 % (419362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419362)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419362)Termination reason: Instruction limit
% 46.97/7.48 % (419362)Termination phase: Saturation
% 46.97/7.48 % (419362)Time elapsed: 0.358 s
% 46.97/7.48 % (419362)Peak memory usage: 135 MB
% 46.97/7.48 % (419362)Instructions burned: 276 (million)
% 46.97/7.48 % (419372)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4140606717:s2a=on:i=450:doe=on:nm=32:rtra=on_2954 on theBenchmark for (2954ds/450Mi)
% 46.97/7.48 % (419378)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
% 46.97/7.48 % (419371)------------------------------
% 46.97/7.48 % (419371)------------------------------
% 46.97/7.48 % (419378)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1172265083:i=1090:aac=none:nm=0:rtra=on:rawr=on_2952 on theBenchmark for (2952ds/1090Mi)
% 46.97/7.48 % (419372)Instruction limit reached!
% 46.97/7.48 % (419372)------------------------------
% 46.97/7.48 % (419372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.97/7.48 % (419372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419372)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419372)Termination reason: Instruction limit
% 46.97/7.48 % (419372)Termination phase: Saturation
% 46.97/7.48 % (419372)Time elapsed: 0.361 s
% 46.97/7.48 % (419372)Peak memory usage: 134 MB
% 46.97/7.48 % (419372)Instructions burned: 450 (million)
% 46.97/7.48 % (419367)Instruction limit reached!
% 46.97/7.48 % (419367)------------------------------
% 46.97/7.48 % (419367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.97/7.48 % (419367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.97/7.48 % (419367)CaDiCaL version: 2.1.3
% 46.97/7.48 % (419367)Termination reason: Instruction limit
% 46.97/7.48 % (419367)Termination phase: Saturation
% 46.97/7.48 % (419367)Time elapsed: 0.632 s
% 46.97/7.48 % (419367)Peak memory usage: 93 MB
% 46.97/7.48 % (419367)Instructions burned: 656 (million)
% 46.97/7.48 % (419389)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2490056202:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2949 on theBenchmark for (2949ds/130Mi)
% 52.27/8.09 % (419363)Instruction limit reached!
% 52.27/8.09 % (419363)------------------------------
% 52.27/8.09 % (419363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419363)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419363)Termination reason: Instruction limit
% 52.27/8.09 % (419363)Termination phase: Saturation
% 52.27/8.09 % (419363)Time elapsed: 1.055 s
% 52.27/8.09 % (419363)Peak memory usage: 92 MB
% 52.27/8.09 % (419363)Instructions burned: 1053 (million)
% 52.27/8.09 % (419390)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2375747326:i=312:kws=inv_frequency:nm=20:rtra=on_2947 on theBenchmark for (2947ds/312Mi)
% 52.27/8.09 % (419391)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2356194949:i=491:doe=on:rtra=on:gtg=position_2947 on theBenchmark for (2947ds/491Mi)
% 52.27/8.09 % (419370)Instruction limit reached!
% 52.27/8.09 % (419370)------------------------------
% 52.27/8.09 % (419370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419370)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419370)Termination reason: Instruction limit
% 52.27/8.09 % (419370)Termination phase: Saturation
% 52.27/8.09 % (419370)Time elapsed: 0.809 s
% 52.27/8.09 % (419370)Peak memory usage: 91 MB
% 52.27/8.09 % (419370)Instructions burned: 1056 (million)
% 52.27/8.09 % (419389)Instruction limit reached!
% 52.27/8.09 % (419389)------------------------------
% 52.27/8.09 % (419389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419389)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419389)Termination reason: Instruction limit
% 52.27/8.09 % (419389)Termination phase: Saturation
% 52.27/8.09 % (419389)Time elapsed: 0.170 s
% 52.27/8.09 % (419389)Peak memory usage: 116 MB
% 52.27/8.09 % (419389)Instructions burned: 130 (million)
% 52.27/8.09 % (419398)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=1767947088:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2945 on theBenchmark for (2945ds/307Mi)
% 52.27/8.09 % (419395)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=499724855:s2a=on:i=835:s2at=2:rtra=on_2945 on theBenchmark for (2945ds/835Mi)
% 52.27/8.09 % (419390)Instruction limit reached!
% 52.27/8.09 % (419390)------------------------------
% 52.27/8.09 % (419390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419390)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419390)Termination reason: Instruction limit
% 52.27/8.09 % (419390)Termination phase: Saturation
% 52.27/8.09 % (419390)Time elapsed: 0.336 s
% 52.27/8.09 % (419390)Peak memory usage: 117 MB
% 52.27/8.09 % (419390)Instructions burned: 312 (million)
% 52.27/8.09 % (419399)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=823044219:i=776:doe=on:rtra=on_2944 on theBenchmark for (2944ds/776Mi)
% 52.27/8.09 % (419398)Instruction limit reached!
% 52.27/8.09 % (419398)------------------------------
% 52.27/8.09 % (419398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419398)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419398)Termination reason: Instruction limit
% 52.27/8.09 % (419398)Termination phase: Saturation
% 52.27/8.09 % (419398)Time elapsed: 0.294 s
% 52.27/8.09 % (419398)Peak memory usage: 91 MB
% 52.27/8.09 % (419398)Instructions burned: 307 (million)
% 52.27/8.09 % (419391)Instruction limit reached!
% 52.27/8.09 % (419391)------------------------------
% 52.27/8.09 % (419391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.27/8.09 % (419391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.27/8.09 % (419391)CaDiCaL version: 2.1.3
% 52.27/8.09 % (419391)Termination reason: Instruction limit
% 52.27/8.09 % (419391)Termination phase: Saturation
% 52.27/8.09 % (419391)Time elapsed: 0.515 s
% 52.27/8.09 % (419391)Peak memory usage: 92 MB
% 52.27/8.09 % (419391)Instructions burned: 492 (million)
% 52.27/8.09 % (419403)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=373960608:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2941 on theBenchmark for (2941ds/646Mi)
% 62.40/9.53 % (419404)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=2680358699:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2940 on theBenchmark for (2940ds/784Mi)
% 62.40/9.53 % (419378)Instruction limit reached!
% 62.40/9.53 % (419378)------------------------------
% 62.40/9.53 % (419378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.40/9.53 % (419378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.40/9.53 % (419378)CaDiCaL version: 2.1.3
% 62.40/9.53 % (419378)Termination reason: Instruction limit
% 62.40/9.53 % (419378)Termination phase: Saturation
% 62.40/9.53 % (419378)Time elapsed: 1.141 s
% 62.40/9.53 % (419378)Peak memory usage: 121 MB
% 62.40/9.53 % (419378)Instructions burned: 1090 (million)
% 62.40/9.53 % (419405)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=2569110095:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2939 on theBenchmark for (2939ds/1131Mi)
% 62.40/9.53 % (419395)Instruction limit reached!
% 62.40/9.53 % (419395)------------------------------
% 62.40/9.53 % (419395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.40/9.53 % (419395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.40/9.53 % (419395)CaDiCaL version: 2.1.3
% 62.40/9.53 % (419395)Termination reason: Instruction limit
% 62.40/9.53 % (419395)Termination phase: Saturation
% 62.40/9.53 % (419395)Time elapsed: 0.706 s
% 62.40/9.53 % (419395)Peak memory usage: 90 MB
% 62.40/9.53 % (419395)Instructions burned: 836 (million)
% 62.40/9.53 % (419359)Instruction limit reached!
% 62.40/9.53 % (419359)------------------------------
% 62.40/9.53 % (419359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.40/9.53 % (419359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.40/9.53 % (419359)CaDiCaL version: 2.1.3
% 62.40/9.53 % (419359)Termination reason: Instruction limit
% 62.40/9.53 % (419359)Termination phase: Saturation
% 62.40/9.53 % (419359)Time elapsed: 2.169 s
% 62.40/9.53 % (419359)Peak memory usage: 112 MB
% 62.40/9.53 % (419359)Instructions burned: 4431 (million)
% 62.40/9.53 % (419408)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=3628518249:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2937 on theBenchmark for (2937ds/246Mi)
% 62.40/9.53 % (419399)Instruction limit reached!
% 62.40/9.53 % (419399)------------------------------
% 62.40/9.53 % (419399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.40/9.53 % (419399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.40/9.53 % (419399)CaDiCaL version: 2.1.3
% 62.40/9.53 % (419399)Termination reason: Instruction limit
% 62.40/9.53 % (419399)Termination phase: Saturation
% 62.40/9.53 % (419399)Time elapsed: 0.746 s
% 62.40/9.53 % (419399)Peak memory usage: 120 MB
% 62.40/9.53 % (419399)Instructions burned: 777 (million)
% 62.40/9.53 % (419412)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2527177397:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2936 on theBenchmark for (2936ds/775Mi)
% 62.40/9.53 % (419413)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3164121663:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/273Mi)
% 62.40/9.53 % (419408)Instruction limit reached!
% 62.40/9.53 % (419408)------------------------------
% 62.40/9.53 % (419408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.40/9.53 % (419408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.40/9.53 % (419408)CaDiCaL version: 2.1.3
% 62.40/9.53 % (419408)Termination reason: Instruction limit
% 62.40/9.53 % (419408)Termination phase: Saturation
% 62.40/9.53 % (419408)Time elapsed: 0.243 s
% 62.40/9.53 % (419408)Peak memory usage: 116 MB
% 62.40/9.53 % (419408)Instructions burned: 247 (million)
% 62.40/9.53 % (419415)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=144682843:i=102:nm=16:rtra=on_2934 on theBenchmark for (2934ds/102Mi)
% 62.40/9.53 % (419415)Instruction limit reached!
% 62.40/9.53 % (419415)------------------------------
% 62.40/9.53 % (419415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419415)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419415)Termination reason: Instruction limit
% 85.49/12.84 % (419415)Termination phase: Saturation
% 85.49/12.84 % (419415)Time elapsed: 0.058 s
% 85.49/12.84 % (419415)Peak memory usage: 89 MB
% 85.49/12.84 % (419415)Instructions burned: 102 (million)
% 85.49/12.84 % (419403)Instruction limit reached!
% 85.49/12.84 % (419403)------------------------------
% 85.49/12.84 % (419403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419403)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419403)Termination reason: Instruction limit
% 85.49/12.84 % (419403)Termination phase: Saturation
% 85.49/12.84 % (419403)Time elapsed: 0.733 s
% 85.49/12.84 % (419403)Peak memory usage: 136 MB
% 85.49/12.84 % (419403)Instructions burned: 646 (million)
% 85.49/12.84 % (419404)Instruction limit reached!
% 85.49/12.84 % (419404)------------------------------
% 85.49/12.84 % (419404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419404)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419404)Termination reason: Instruction limit
% 85.49/12.84 % (419404)Termination phase: Saturation
% 85.49/12.84 % (419404)Time elapsed: 0.785 s
% 85.49/12.84 % (419404)Peak memory usage: 120 MB
% 85.49/12.84 % (419404)Instructions burned: 785 (million)
% 85.49/12.84 % (419413)Instruction limit reached!
% 85.49/12.84 % (419413)------------------------------
% 85.49/12.84 % (419413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419413)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419413)Termination reason: Instruction limit
% 85.49/12.84 % (419413)Termination phase: Saturation
% 85.49/12.84 % (419413)Time elapsed: 0.310 s
% 85.49/12.84 % (419413)Peak memory usage: 92 MB
% 85.49/12.84 % (419413)Instructions burned: 273 (million)
% 85.49/12.84 % (419419)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2344852560:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2932 on theBenchmark for (2932ds/1094Mi)
% 85.49/12.84 % (419420)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=651774724:i=6400:doe=on:fsr=off:rtra=on_2931 on theBenchmark for (2931ds/6400Mi)
% 85.49/12.84 % (419421)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=3585999847:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2931 on theBenchmark for (2931ds/868Mi)
% 85.49/12.84 % (419422)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=3561053998:i=1846:canc=cautious:fsr=off:rtra=on_2930 on theBenchmark for (2930ds/1846Mi)
% 85.49/12.84 % (419422)Refutation not found, incomplete strategy
% 85.49/12.84 % (419422)------------------------------
% 85.49/12.84 % (419422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419422)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419422)Termination reason: Refutation not found, incomplete strategy
% 85.49/12.84 % (419422)Time elapsed: 0.004 s
% 85.49/12.84 % (419422)Peak memory usage: 89 MB
% 85.49/12.84 % (419422)Instructions burned: 2 (million)
% 85.49/12.84 % (419423)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=103807963:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2929 on theBenchmark for (2929ds/36816Mi)
% 85.49/12.84 % (419412)Instruction limit reached!
% 85.49/12.84 % (419412)------------------------------
% 85.49/12.84 % (419412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.49/12.84 % (419412)CaDiCaL version: 2.1.3
% 85.49/12.84 % (419412)Termination reason: Instruction limit
% 85.49/12.84 % (419412)Termination phase: Saturation
% 85.49/12.84 % (419412)Time elapsed: 0.705 s
% 85.49/12.84 % (419412)Peak memory usage: 93 MB
% 85.49/12.84 % (419412)Instructions burned: 775 (million)
% 85.49/12.84 % (419405)Instruction limit reached!
% 85.49/12.84 % (419405)------------------------------
% 85.49/12.84 % (419405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.49/12.84 % (419405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419405)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419405)Termination reason: Instruction limit
% 90.88/13.92 % (419405)Termination phase: Saturation
% 90.88/13.92 % (419405)Time elapsed: 1.169 s
% 90.88/13.92 % (419405)Peak memory usage: 119 MB
% 90.88/13.92 % (419405)Instructions burned: 1132 (million)
% 90.88/13.92 % (419429)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1840215464:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2926 on theBenchmark for (2926ds/273Mi)
% 90.88/13.92 % (419422)------------------------------
% 90.88/13.92 % (419422)------------------------------
% 90.88/13.92 % (419430)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=3718406495:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2925 on theBenchmark for (2925ds/863Mi)
% 90.88/13.92 % (419421)Instruction limit reached!
% 90.88/13.92 % (419421)------------------------------
% 90.88/13.92 % (419421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419421)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419421)Termination reason: Instruction limit
% 90.88/13.92 % (419421)Termination phase: Saturation
% 90.88/13.92 % (419421)Time elapsed: 0.846 s
% 90.88/13.92 % (419421)Peak memory usage: 118 MB
% 90.88/13.92 % (419421)Instructions burned: 868 (million)
% 90.88/13.92 % (419429)Instruction limit reached!
% 90.88/13.92 % (419429)------------------------------
% 90.88/13.92 % (419429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419429)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419429)Termination reason: Instruction limit
% 90.88/13.92 % (419429)Termination phase: Saturation
% 90.88/13.92 % (419429)Time elapsed: 0.306 s
% 90.88/13.92 % (419429)Peak memory usage: 92 MB
% 90.88/13.92 % (419429)Instructions burned: 273 (million)
% 90.88/13.92 % (419432)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1232681149:i=5811:kws=precedence:nm=0:rtra=on_2923 on theBenchmark for (2923ds/5811Mi)
% 90.88/13.92 % (419419)Instruction limit reached!
% 90.88/13.92 % (419419)------------------------------
% 90.88/13.92 % (419419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419419)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419419)Termination reason: Instruction limit
% 90.88/13.92 % (419419)Termination phase: Saturation
% 90.88/13.92 % (419419)Time elapsed: 0.933 s
% 90.88/13.92 % (419419)Peak memory usage: 91 MB
% 90.88/13.92 % (419419)Instructions burned: 1095 (million)
% 90.88/13.92 % (419435)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2051620955:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2920 on theBenchmark for (2920ds/801Mi)
% 90.88/13.92 % (419434)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=2047240430:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2216Mi)
% 90.88/13.92 % (419437)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1902295830:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2920 on theBenchmark for (2920ds/1026Mi)
% 90.88/13.92 % (419430)Instruction limit reached!
% 90.88/13.92 % (419430)------------------------------
% 90.88/13.92 % (419430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419430)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419430)Termination reason: Instruction limit
% 90.88/13.92 % (419430)Termination phase: Saturation
% 90.88/13.92 % (419430)Time elapsed: 0.835 s
% 90.88/13.92 % (419430)Peak memory usage: 118 MB
% 90.88/13.92 % (419430)Instructions burned: 864 (million)
% 90.88/13.92 % (419441)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3910604220:i=3509:rtra=on_2914 on theBenchmark for (2914ds/3509Mi)
% 90.88/13.92 % (419435)Instruction limit reached!
% 90.88/13.92 % (419435)------------------------------
% 90.88/13.92 % (419435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419435)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419435)Termination reason: Instruction limit
% 90.88/13.92 % (419435)Termination phase: Saturation
% 90.88/13.92 % (419435)Time elapsed: 0.691 s
% 90.88/13.92 % (419435)Peak memory usage: 91 MB
% 90.88/13.92 % (419435)Instructions burned: 802 (million)
% 90.88/13.92 % (419443)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=950400378:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/2127Mi)
% 90.88/13.92 % (419437)Instruction limit reached!
% 90.88/13.92 % (419437)------------------------------
% 90.88/13.92 % (419437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419437)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419437)Termination reason: Instruction limit
% 90.88/13.92 % (419437)Termination phase: Saturation
% 90.88/13.92 % (419437)Time elapsed: 0.942 s
% 90.88/13.92 % (419437)Peak memory usage: 90 MB
% 90.88/13.92 % (419437)Instructions burned: 1027 (million)
% 90.88/13.92 % (419445)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=305226682:i=1959:rtra=on:fsd=on:proc=on_2908 on theBenchmark for (2908ds/1959Mi)
% 90.88/13.92 % (419420)Instruction limit reached!
% 90.88/13.92 % (419420)------------------------------
% 90.88/13.92 % (419420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419420)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419420)Termination reason: Instruction limit
% 90.88/13.92 % (419420)Termination phase: Saturation
% 90.88/13.92 % (419420)Time elapsed: 3.151 s
% 90.88/13.92 % (419420)Peak memory usage: 122 MB
% 90.88/13.92 % (419420)Instructions burned: 6400 (million)
% 90.88/13.92 % (419434)Instruction limit reached!
% 90.88/13.92 % (419434)------------------------------
% 90.88/13.92 % (419434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419434)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419434)Termination reason: Instruction limit
% 90.88/13.92 % (419434)Termination phase: Saturation
% 90.88/13.92 % (419434)Time elapsed: 2.067 s
% 90.88/13.92 % (419434)Peak memory usage: 121 MB
% 90.88/13.92 % (419434)Instructions burned: 2217 (million)
% 90.88/13.92 % (419449)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1470016032:s2a=on:i=3553:nm=0:rtra=on_2898 on theBenchmark for (2898ds/3553Mi)
% 90.88/13.92 % (419450)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2009968948:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2897 on theBenchmark for (2897ds/3201Mi)
% 90.88/13.92 % (419443)Instruction limit reached!
% 90.88/13.92 % (419443)------------------------------
% 90.88/13.92 % (419443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419443)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419443)Termination reason: Instruction limit
% 90.88/13.92 % (419443)Termination phase: Saturation
% 90.88/13.92 % (419443)Time elapsed: 1.742 s
% 90.88/13.92 % (419443)Peak memory usage: 91 MB
% 90.88/13.92 % (419443)Instructions burned: 2128 (million)
% 90.88/13.92 % (419453)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=4099525037:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2890 on theBenchmark for (2890ds/4093Mi)
% 90.88/13.92 % (419445)Instruction limit reached!
% 90.88/13.92 % (419445)------------------------------
% 90.88/13.92 % (419445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419445)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419445)Termination reason: Instruction limit
% 90.88/13.92 % (419445)Termination phase: Saturation
% 90.88/13.92 % (419445)Time elapsed: 1.984 s
% 90.88/13.92 % (419445)Peak memory usage: 122 MB
% 90.88/13.92 % (419445)Instructions burned: 1959 (million)
% 90.88/13.92 % (419455)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=1125365432:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2885 on theBenchmark for (2885ds/21173Mi)
% 90.88/13.92 % (419449)Instruction limit reached!
% 90.88/13.92 % (419449)------------------------------
% 90.88/13.92 % (419449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419449)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419449)Termination reason: Instruction limit
% 90.88/13.92 % (419449)Termination phase: Saturation
% 90.88/13.92 % (419449)Time elapsed: 1.772 s
% 90.88/13.92 % (419449)Peak memory usage: 98 MB
% 90.88/13.92 % (419449)Instructions burned: 3554 (million)
% 90.88/13.92 % (419457)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2807562171:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2878 on theBenchmark for (2878ds/10544Mi)
% 90.88/13.92 % (419441)Instruction limit reached!
% 90.88/13.92 % (419441)------------------------------
% 90.88/13.92 % (419441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.88/13.92 % (419441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.88/13.92 % (419441)CaDiCaL version: 2.1.3
% 90.88/13.92 % (419441)Termination reason: Instruction limit
% 90.88/13.92 % (419441)Termination phase: Saturation
% 90.88/13.92 % (419441)Time elapsed: 3.648 s
% 90.88/13.92 % (419441)Peak memory usage: 103 MB
% 90.88/13.92 % (419441)Instructions burned: 3509 (million)
% 90.88/13.92 % (419453)First to succeed.
% 90.88/13.92 % (419453)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-419020"
% 90.88/13.92 % (419459)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1241645420:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2874 on theBenchmark for (2874ds/1262Mi)
% 90.88/13.92 % (419453)Refutation found. Thanks to Tanya!
% 90.88/13.92 % SZS status Theorem for theBenchmark
% 90.88/13.92 % SZS output start Proof for theBenchmark
% See solution above
% 94.18/14.13 % (419453)------------------------------
% 94.18/14.13 % (419453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.18/14.13 % (419453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.18/14.13 % (419453)CaDiCaL version: 2.1.3
% 94.18/14.13 % (419453)Termination reason: Refutation
% 94.18/14.13 % (419453)Time elapsed: 1.602 s
% 94.18/14.13 % (419453)Peak memory usage: 140 MB
% 94.18/14.13 % (419453)Instructions burned: 1530 (million)
% 94.18/14.13 % (419453)------------------------------
% 94.18/14.13 % (419453)------------------------------
% 94.18/14.13 % (419020)Success in time 13.262 s
% 94.18/14.13 % Vampire exiting
%------------------------------------------------------------------------------