%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX107_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:54 PM UTC 2026
% Result : Theorem 109.89s 16.17s
% Output : Refutation 110.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 38
% Syntax : Number of formulae : 328 ( 14 unt; 0 typ; 25 def)
% Number of atoms : 1519 ( 568 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 1993 ( 802 ~; 820 |; 331 &)
% ( 25 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 815 ( 188 atm; 158 fun; 200 num; 269 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 : 37 ( 33 usr; 23 prp; 0-3 aty)
% Number of functors : 33 ( 27 usr; 12 con; 0-2 aty)
% Number of variables : 533 ( 0 sgn 309 !; 224 ?; 533 :)
% 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_9,type,
sK3: ( general * general ) > general ).
tff(func_def_10,type,
sK4: ( general * general ) > general ).
tff(func_def_11,type,
sK5: ( general * general ) > $int ).
tff(func_def_12,type,
sK6: ( general * general ) > $int ).
tff(func_def_13,type,
sK7: general > general ).
tff(func_def_14,type,
sK8: general > general ).
tff(func_def_15,type,
sK9: general > $int ).
tff(func_def_16,type,
sK10: general > $int ).
tff(func_def_17,type,
sK11: general > $int ).
tff(func_def_18,type,
sK12: general > general ).
tff(func_def_19,type,
sK13: general > general ).
tff(func_def_20,type,
sK14: general > $int ).
tff(func_def_21,type,
sK15: general > $int ).
tff(func_def_22,type,
sK16: general > $int ).
tff(func_def_23,type,
sK17: general ).
tff(func_def_24,type,
sK18: general ).
tff(func_def_25,type,
sK19: general ).
tff(func_def_26,type,
sK20: general ).
tff(func_def_27,type,
sK21: general ).
tff(func_def_28,type,
sK22: $int ).
tff(func_def_29,type,
sK23: $int ).
tff(func_def_30,type,
sK24: general > $int ).
tff(func_def_31,type,
sK25: general > symbol ).
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 > $o ).
tff(pred_def_12,type,
sP1: general > $o ).
tff(pred_def_13,type,
sP2: ( general * general * general ) > $o ).
tff(f4,axiom,
! [X1: $int,X0: $int] :
( ( X0 = X1 )
<=> ( f__integer__(X0) = f__integer__(X1) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f9,axiom,
! [X0: general,X1: general] :
( p__less_equal__(X0,X1)
| p__less_equal__(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',strongly_connected_ordering_ax) ).
tff(f16,axiom,
! [X0: general] :
( hp(X0)
=> tp(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_0_transition_axiom_0) ).
tff(f17,axiom,
! [X1: general,X0: general,X2: general] :
( ( ( ( X0 = X2 )
& ? [X4: general,X3: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X1 )
& ( f__integer__(X5) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) )
& ( X3 = X2 ) )
& ? [X3: general,X4: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int,X7: $int] :
( $lesseq(X5,X7)
& ( X4 = f__integer__(X7) )
& ( X5 = 0 )
& ( X6 = 1 )
& $lesseq(X7,X6) )
& ( X3 = X1 ) ) )
=> tp(X0) )
& ( ( ( X0 = X2 )
& ? [X3: general,X4: general] :
( ( X3 = X4 )
& ( X3 = X2 )
& ? [X5: $int,X6: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) ) )
& ? [X3: general,X4: general] :
( ( X3 = X1 )
& ( X3 = X4 )
& ? [X7: $int,X5: $int,X6: $int] :
( ( X5 = 0 )
& ( X4 = f__integer__(X7) )
& ( X6 = 1 )
& $lesseq(X5,X7)
& $lesseq(X7,X6) ) ) )
=> hp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1_left_0) ).
tff(f18,conjecture,
! [X2: general,X0: general,X1: general] :
( ( ( ? [X3: general,X4: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int] :
( ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X6) = X1 )
& ( f__integer__(X5) = X1 ) )
& ( X3 = X2 ) )
& ( X0 = X2 )
& ? [X4: general,X3: general] :
( ? [X6: $int,X5: $int,X7: $int] :
( $lesseq(X7,X6)
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& ( X4 = f__integer__(X7) )
& $lesseq(X5,X7) )
& ( X3 = X1 )
& ( X3 = X4 ) ) )
=> hp(X0) )
& ( ( ? [X3: general,X4: general] :
( ( X3 = X2 )
& ? [X6: $int,X5: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) )
& ( X3 = X4 ) )
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int,X7: $int] :
( $lesseq(X7,X6)
& ( X4 = f__integer__(X7) )
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& $lesseq(X5,X7) )
& ( X3 = X1 )
& ( X3 = X4 ) )
& ( X0 = X2 ) )
=> tp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_right_0) ).
tff(f19,negated_conjecture,
~ ! [X2: general,X0: general,X1: general] :
( ( ( ? [X3: general,X4: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int] :
( ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X6) = X1 )
& ( f__integer__(X5) = X1 ) )
& ( X3 = X2 ) )
& ( X0 = X2 )
& ? [X4: general,X3: general] :
( ? [X6: $int,X5: $int,X7: $int] :
( $lesseq(X7,X6)
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& ( X4 = f__integer__(X7) )
& $lesseq(X5,X7) )
& ( X3 = X1 )
& ( X3 = X4 ) ) )
=> hp(X0) )
& ( ( ? [X3: general,X4: general] :
( ( X3 = X2 )
& ? [X6: $int,X5: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) )
& ( X3 = X4 ) )
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int,X7: $int] :
( $lesseq(X7,X6)
& ( X4 = f__integer__(X7) )
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& $lesseq(X5,X7) )
& ( X3 = X1 )
& ( X3 = X4 ) )
& ( X0 = X2 ) )
=> tp(X0) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
tff(f20,plain,
~ ! [X2: general,X0: general,X1: general] :
( ( ( ? [X3: general,X4: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int] :
( ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X6) = X1 )
& ( f__integer__(X5) = X1 ) )
& ( X3 = X2 ) )
& ( X0 = X2 )
& ? [X4: general,X3: general] :
( ? [X6: $int,X5: $int,X7: $int] :
( ~ $less(X6,X7)
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& ( X4 = f__integer__(X7) )
& ~ $less(X7,X5) )
& ( X3 = X1 )
& ( X3 = X4 ) ) )
=> hp(X0) )
& ( ( ? [X3: general,X4: general] :
( ( X3 = X2 )
& ? [X6: $int,X5: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) )
& ( X3 = X4 ) )
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int,X7: $int] :
( ~ $less(X6,X7)
& ( X4 = f__integer__(X7) )
& ( X5 = $uminus(1) )
& ( X6 = 1 )
& ~ $less(X7,X5) )
& ( X3 = X1 )
& ( X3 = X4 ) )
& ( X0 = X2 ) )
=> tp(X0) ) ),
inference(theory_normalization,[],[f19]) ).
tff(f21,plain,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
<=> ~ $less(X1,X0) ),
inference(theory_normalization,[],[f6]) ).
tff(f22,plain,
! [X1: general,X0: general,X2: general] :
( ( ( ( X0 = X2 )
& ? [X4: general,X3: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X1 )
& ( f__integer__(X5) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) )
& ( X3 = X2 ) )
& ? [X3: general,X4: general] :
( ( X3 = X4 )
& ? [X5: $int,X6: $int,X7: $int] :
( ~ $less(X7,X5)
& ( X4 = f__integer__(X7) )
& ( X5 = 0 )
& ( X6 = 1 )
& ~ $less(X6,X7) )
& ( X3 = X1 ) ) )
=> tp(X0) )
& ( ( ( X0 = X2 )
& ? [X3: general,X4: general] :
( ( X3 = X4 )
& ( X3 = X2 )
& ? [X5: $int,X6: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) ) ) )
& ? [X3: general,X4: general] :
( ( X3 = X1 )
& ( X3 = X4 )
& ? [X7: $int,X5: $int,X6: $int] :
( ( X5 = 0 )
& ( X4 = f__integer__(X7) )
& ( X6 = 1 )
& ~ $less(X7,X5)
& ~ $less(X6,X7) ) ) )
=> hp(X0) ) ),
inference(theory_normalization,[],[f17]) ).
tff(f23,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f27,plain,
! [X0: $int] : ( 0 = $sum(X0,$uminus(X0)) ),
introduced(definition,[],[tha_inverse_op_unit]) ).
tff(f30,plain,
! [X0: $int,X1: $int] :
( $less(X1,X0)
| $less(X0,X1)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f31,plain,
! [X2: $int,X0: $int,X1: $int] :
( $less($sum(X0,X2),$sum(X1,X2))
| ~ $less(X0,X1) ),
introduced(definition,[],[tha_order_monotonicity]) ).
tff(f34,plain,
! [X0: $int,X1: $int] : ( $product(X1,X0) = $product(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f35,plain,
! [X2: $int,X0: $int,X1: $int] : ( $product(X0,$product(X1,X2)) = $product($product(X0,X1),X2) ),
introduced(definition,[],[tha_associativity]) ).
tff(f40,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$sum(X0,1))
| ~ $less(X0,X1) ),
introduced(definition,[],[tha_extra_integer_ordering]) ).
tff(f41,plain,
~ ! [X2: general,X1: general,X0: general] :
( ( ( ? [X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__(X14) = X2 )
& ( f__integer__($product(X15,X14)) = X13 )
& ( f__integer__(X15) = X2 ) )
& ( X12 = X13 )
& ( X0 = X12 ) )
& ( X0 = X1 )
& ? [X16: general,X17: general] :
( ( X2 = X16 )
& ? [X20: $int,X18: $int,X19: $int] :
( ( $uminus(1) = X18 )
& ( f__integer__(X20) = X17 )
& ~ $less(X20,X18)
& ( 1 = X19 )
& ~ $less(X19,X20) )
& ( X16 = X17 ) ) )
=> tp(X1) )
& ( ( ( X0 = X1 )
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X2 ) )
& ( X0 = X3 )
& ( X3 = X4 ) )
& ? [X8: general,X7: general] :
( ? [X10: $int,X9: $int,X11: $int] :
( ( $uminus(1) = X10 )
& ~ $less(X11,X10)
& ~ $less(X9,X11)
& ( 1 = X9 )
& ( f__integer__(X11) = X7 ) )
& ( X7 = X8 )
& ( X2 = X8 ) ) )
=> hp(X1) ) ),
inference(rectify,[],[f20]) ).
tff(f44,plain,
! [X1: general,X2: general,X0: general] :
( ( ( ? [X8: general,X7: general] :
( ? [X9: $int,X10: $int,X11: $int] :
( ( f__integer__(X11) = X8 )
& ~ $less(X10,X11)
& ( 1 = X10 )
& ( 0 = X9 )
& ~ $less(X11,X9) )
& ( X7 = X8 )
& ( X0 = X7 ) )
& ( X1 = X2 )
& ? [X3: general,X4: general] :
( ( X3 = X4 )
& ( X2 = X4 )
& ? [X5: $int,X6: $int] :
( ( f__integer__(X5) = X0 )
& ( f__integer__($product(X5,X6)) = X3 )
& ( f__integer__(X6) = X0 ) ) ) )
=> tp(X1) )
& ( ( ? [X12: general,X13: general] :
( ( X2 = X12 )
& ( X12 = X13 )
& ? [X15: $int,X14: $int] :
( ( f__integer__(X14) = X0 )
& ( f__integer__(X15) = X0 )
& ( f__integer__($product(X14,X15)) = X13 ) ) )
& ? [X17: general,X16: general] :
( ( X16 = X17 )
& ? [X19: $int,X18: $int,X20: $int] :
( ~ $less(X20,X18)
& ( f__integer__(X18) = X17 )
& ~ $less(X18,X19)
& ( 1 = X20 )
& ( 0 = X19 ) )
& ( X0 = X16 ) )
& ( X1 = X2 ) )
=> hp(X1) ) ),
inference(rectify,[],[f22]) ).
tff(f51,plain,
! [X0: general] :
( ~ hp(X0)
| tp(X0) ),
inference(ennf_transformation,[],[f16]) ).
tff(f58,plain,
? [X2: general,X1: general,X0: general] :
( ( ~ tp(X1)
& ? [X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__(X14) = X2 )
& ( f__integer__($product(X15,X14)) = X13 )
& ( f__integer__(X15) = X2 ) )
& ( X12 = X13 )
& ( X0 = X12 ) )
& ( X0 = X1 )
& ? [X16: general,X17: general] :
( ( X2 = X16 )
& ? [X20: $int,X18: $int,X19: $int] :
( ( $uminus(1) = X18 )
& ( f__integer__(X20) = X17 )
& ~ $less(X20,X18)
& ( 1 = X19 )
& ~ $less(X19,X20) )
& ( X16 = X17 ) ) )
| ( ~ hp(X1)
& ( X0 = X1 )
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X2 ) )
& ( X0 = X3 )
& ( X3 = X4 ) )
& ? [X8: general,X7: general] :
( ? [X10: $int,X9: $int,X11: $int] :
( ( $uminus(1) = X10 )
& ~ $less(X11,X10)
& ~ $less(X9,X11)
& ( 1 = X9 )
& ( f__integer__(X11) = X7 ) )
& ( X7 = X8 )
& ( X2 = X8 ) ) ) ),
inference(ennf_transformation,[],[f41]) ).
tff(f59,plain,
? [X0: general,X2: general,X1: general] :
( ( ( X0 = X1 )
& ~ tp(X1)
& ? [X16: general,X17: general] :
( ( X2 = X16 )
& ? [X20: $int,X18: $int,X19: $int] :
( ( $uminus(1) = X18 )
& ( f__integer__(X20) = X17 )
& ~ $less(X20,X18)
& ( 1 = X19 )
& ~ $less(X19,X20) )
& ( X16 = X17 ) )
& ? [X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__(X14) = X2 )
& ( f__integer__($product(X15,X14)) = X13 )
& ( f__integer__(X15) = X2 ) )
& ( X12 = X13 )
& ( X0 = X12 ) ) )
| ( ~ hp(X1)
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X2 ) )
& ( X0 = X3 )
& ( X3 = X4 ) )
& ( X0 = X1 )
& ? [X8: general,X7: general] :
( ? [X10: $int,X9: $int,X11: $int] :
( ( $uminus(1) = X10 )
& ~ $less(X11,X10)
& ~ $less(X9,X11)
& ( 1 = X9 )
& ( f__integer__(X11) = X7 ) )
& ( X7 = X8 )
& ( X2 = X8 ) ) ) ),
inference(flattening,[],[f58]) ).
tff(f60,plain,
! [X1: general,X2: general,X0: general] :
( ( tp(X1)
| ! [X7: general,X8: general] :
( ( X0 != X7 )
| ! [X9: $int,X10: $int,X11: $int] :
( $less(X11,X9)
| ( 0 != X9 )
| ( f__integer__(X11) != X8 )
| $less(X10,X11)
| ( 1 != X10 ) )
| ( X7 != X8 ) )
| ( X1 != X2 )
| ! [X3: general,X4: general] :
( ( X2 != X4 )
| ! [X5: $int,X6: $int] :
( ( f__integer__(X6) != X0 )
| ( f__integer__($product(X5,X6)) != X3 )
| ( f__integer__(X5) != X0 ) )
| ( X3 != X4 ) ) )
& ( hp(X1)
| ! [X13: general,X12: general] :
( ( X2 != X12 )
| ! [X15: $int,X14: $int] :
( ( f__integer__(X14) != X0 )
| ( f__integer__(X15) != X0 )
| ( f__integer__($product(X14,X15)) != X13 ) )
| ( X12 != X13 ) )
| ! [X16: general,X17: general] :
( ! [X18: $int,X20: $int,X19: $int] :
( $less(X20,X18)
| ( 0 != X19 )
| ( f__integer__(X18) != X17 )
| ( 1 != X20 )
| $less(X18,X19) )
| ( X16 != X17 )
| ( X0 != X16 ) )
| ( X1 != X2 ) ) ),
inference(ennf_transformation,[],[f44]) ).
tff(f61,plain,
! [X2: general,X1: general,X0: general] :
( ( ! [X13: general,X12: general] :
( ( X2 != X12 )
| ! [X15: $int,X14: $int] :
( ( f__integer__(X14) != X0 )
| ( f__integer__(X15) != X0 )
| ( f__integer__($product(X14,X15)) != X13 ) )
| ( X12 != X13 ) )
| hp(X1)
| ! [X16: general,X17: general] :
( ! [X18: $int,X20: $int,X19: $int] :
( $less(X20,X18)
| ( 0 != X19 )
| ( f__integer__(X18) != X17 )
| ( 1 != X20 )
| $less(X18,X19) )
| ( X16 != X17 )
| ( X0 != X16 ) )
| ( X1 != X2 ) )
& ( ! [X3: general,X4: general] :
( ( X2 != X4 )
| ! [X5: $int,X6: $int] :
( ( f__integer__(X6) != X0 )
| ( f__integer__($product(X5,X6)) != X3 )
| ( f__integer__(X5) != X0 ) )
| ( X3 != X4 ) )
| ! [X7: general,X8: general] :
( ( X0 != X7 )
| ! [X9: $int,X10: $int,X11: $int] :
( $less(X11,X9)
| ( 0 != X9 )
| ( f__integer__(X11) != X8 )
| $less(X10,X11)
| ( 1 != X10 ) )
| ( X7 != X8 ) )
| ( X1 != X2 )
| tp(X1) ) ),
inference(flattening,[],[f60]) ).
tff(f62,definition,
! [X2: general] :
( ? [X8: general,X7: general] :
( ? [X10: $int,X9: $int,X11: $int] :
( ( $uminus(1) = X10 )
& ~ $less(X11,X10)
& ~ $less(X9,X11)
& ( 1 = X9 )
& ( f__integer__(X11) = X7 ) )
& ( X7 = X8 )
& ( X2 = X8 ) )
| ~ sP0(X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f63,definition,
! [X2: general] :
( ? [X16: general,X17: general] :
( ( X2 = X16 )
& ? [X20: $int,X18: $int,X19: $int] :
( ( $uminus(1) = X18 )
& ( f__integer__(X20) = X17 )
& ~ $less(X20,X18)
& ( 1 = X19 )
& ~ $less(X19,X20) )
& ( X16 = X17 ) )
| ~ sP1(X2) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f64,definition,
! [X1: general,X2: general,X0: general] :
( ( ~ hp(X1)
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X2 ) )
& ( X0 = X3 )
& ( X3 = X4 ) )
& ( X0 = X1 )
& sP0(X2) )
| ~ sP2(X1,X2,X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f65,plain,
? [X0: general,X2: general,X1: general] :
( ( ( X0 = X1 )
& ~ tp(X1)
& sP1(X2)
& ? [X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__(X14) = X2 )
& ( f__integer__($product(X15,X14)) = X13 )
& ( f__integer__(X15) = X2 ) )
& ( X12 = X13 )
& ( X0 = X12 ) ) )
| sP2(X1,X2,X0) ),
inference(definition_folding,[],[f59,f64,f63,f62]) ).
tff(f66,plain,
! [X1: general,X2: general,X0: general] :
( ( ~ hp(X1)
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X2 ) )
& ( X0 = X3 )
& ( X3 = X4 ) )
& ( X0 = X1 )
& sP0(X2) )
| ~ sP2(X1,X2,X0) ),
inference(nnf_transformation,[],[f64]) ).
tff(f67,plain,
! [X0: general,X1: general,X2: general] :
( ( ~ hp(X0)
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X6) = X1 )
& ( X4 = f__integer__($product(X5,X6)) )
& ( f__integer__(X5) = X1 ) )
& ( X2 = X3 )
& ( X3 = X4 ) )
& ( X0 = X2 )
& sP0(X1) )
| ~ sP2(X0,X1,X2) ),
inference(rectify,[],[f66]) ).
tff(f68,plain,
! [X0: general,X1: general,X2: general] :
( ( ~ hp(X0)
& ( f__integer__(sK6(X1,X2)) = X1 )
& ( sK4(X1,X2) = f__integer__($product(sK5(X1,X2),sK6(X1,X2))) )
& ( f__integer__(sK5(X1,X2)) = X1 )
& ( sK3(X1,X2) = X2 )
& ( sK4(X1,X2) = sK3(X1,X2) )
& ( X0 = X2 )
& sP0(X1) )
| ~ sP2(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X3,sK3(X1,X2)),skolemize(X4,sK4(X1,X2)),skolemize(X5,sK5(X1,X2)),skolemize(X6,sK6(X1,X2))],[f67]) ).
tff(f69,plain,
! [X2: general] :
( ? [X16: general,X17: general] :
( ( X2 = X16 )
& ? [X20: $int,X18: $int,X19: $int] :
( ( $uminus(1) = X18 )
& ( f__integer__(X20) = X17 )
& ~ $less(X20,X18)
& ( 1 = X19 )
& ~ $less(X19,X20) )
& ( X16 = X17 ) )
| ~ sP1(X2) ),
inference(nnf_transformation,[],[f63]) ).
tff(f70,plain,
! [X0: general] :
( ? [X1: general,X2: general] :
( ( X0 = X1 )
& ? [X3: $int,X4: $int,X5: $int] :
( ( $uminus(1) = X4 )
& ( f__integer__(X3) = X2 )
& ~ $less(X3,X4)
& ( 1 = X5 )
& ~ $less(X5,X3) )
& ( X1 = X2 ) )
| ~ sP1(X0) ),
inference(rectify,[],[f69]) ).
tff(f71,plain,
! [X0: general] :
( ( ( sK7(X0) = X0 )
& ( $uminus(1) = sK10(X0) )
& ( f__integer__(sK9(X0)) = sK8(X0) )
& ~ $less(sK9(X0),sK10(X0))
& ( 1 = sK11(X0) )
& ~ $less(sK11(X0),sK9(X0))
& ( sK8(X0) = sK7(X0) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11]),skolemize(X1,sK7(X0)),skolemize(X2,sK8(X0)),skolemize(X3,sK9(X0)),skolemize(X4,sK10(X0)),skolemize(X5,sK11(X0))],[f70]) ).
tff(f72,plain,
! [X2: general] :
( ? [X8: general,X7: general] :
( ? [X10: $int,X9: $int,X11: $int] :
( ( $uminus(1) = X10 )
& ~ $less(X11,X10)
& ~ $less(X9,X11)
& ( 1 = X9 )
& ( f__integer__(X11) = X7 ) )
& ( X7 = X8 )
& ( X2 = X8 ) )
| ~ sP0(X2) ),
inference(nnf_transformation,[],[f62]) ).
tff(f73,plain,
! [X0: general] :
( ? [X1: general,X2: general] :
( ? [X3: $int,X4: $int,X5: $int] :
( ( $uminus(1) = X3 )
& ~ $less(X5,X3)
& ~ $less(X4,X5)
& ( 1 = X4 )
& ( f__integer__(X5) = X2 ) )
& ( X1 = X2 )
& ( X0 = X1 ) )
| ~ sP0(X0) ),
inference(rectify,[],[f72]) ).
tff(f74,plain,
! [X0: general] :
( ( ( $uminus(1) = sK14(X0) )
& ~ $less(sK16(X0),sK14(X0))
& ~ $less(sK15(X0),sK16(X0))
& ( 1 = sK15(X0) )
& ( f__integer__(sK16(X0)) = sK13(X0) )
& ( sK13(X0) = sK12(X0) )
& ( sK12(X0) = X0 ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15,sK16]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0)),skolemize(X3,sK14(X0)),skolemize(X4,sK15(X0)),skolemize(X5,sK16(X0))],[f73]) ).
tff(f75,plain,
? [X0: general,X1: general,X2: general] :
( ( ( X0 = X2 )
& ~ tp(X2)
& sP1(X1)
& ? [X3: general,X4: general] :
( ? [X5: $int,X6: $int] :
( ( f__integer__(X5) = X1 )
& ( f__integer__($product(X6,X5)) = X4 )
& ( f__integer__(X6) = X1 ) )
& ( X3 = X4 )
& ( X0 = X3 ) ) )
| sP2(X2,X1,X0) ),
inference(rectify,[],[f65]) ).
tff(f76,plain,
( ( ( sK19 = sK17 )
& ~ tp(sK19)
& sP1(sK18)
& ( sK18 = f__integer__(sK22) )
& ( sK21 = f__integer__($product(sK23,sK22)) )
& ( sK18 = f__integer__(sK23) )
& ( sK21 = sK20 )
& ( sK20 = sK17 ) )
| sP2(sK19,sK18,sK17) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20,sK21,sK22,sK23]),skolemize(X0,sK17),skolemize(X1,sK18),skolemize(X2,sK19),skolemize(X3,sK20),skolemize(X4,sK21),skolemize(X5,sK22),skolemize(X6,sK23)],[f75]) ).
tff(f83,plain,
! [X0: general,X1: general,X2: general] :
( ( ! [X3: general,X4: general] :
( ( X0 != X4 )
| ! [X5: $int,X6: $int] :
( ( f__integer__(X6) != X2 )
| ( f__integer__(X5) != X2 )
| ( f__integer__($product(X6,X5)) != X3 ) )
| ( X3 != X4 ) )
| hp(X1)
| ! [X7: general,X8: general] :
( ! [X9: $int,X10: $int,X11: $int] :
( $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11) )
| ( X7 != X8 )
| ( X2 != X7 ) )
| ( X0 != X1 ) )
& ( ! [X12: general,X13: general] :
( ( X0 != X13 )
| ! [X14: $int,X15: $int] :
( ( f__integer__(X15) != X2 )
| ( f__integer__($product(X14,X15)) != X12 )
| ( f__integer__(X14) != X2 ) )
| ( X12 != X13 ) )
| ! [X16: general,X17: general] :
( ( X2 != X16 )
| ! [X18: $int,X19: $int,X20: $int] :
( $less(X20,X18)
| ( 0 != X18 )
| ( f__integer__(X20) != X17 )
| $less(X19,X20)
| ( 1 != X19 ) )
| ( X16 != X17 ) )
| ( X0 != X1 )
| tp(X1) ) ),
inference(rectify,[],[f61]) ).
tff(f85,plain,
! [X1: $int,X0: $int] :
( ( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) )
& ( ~ $less(X1,X0)
| ~ p__less_equal__(f__integer__(X0),f__integer__(X1)) ) ),
inference(nnf_transformation,[],[f21]) ).
tff(f86,plain,
! [X0: $int,X1: $int] :
( ( p__less_equal__(f__integer__(X1),f__integer__(X0))
| $less(X0,X1) )
& ( ~ $less(X0,X1)
| ~ p__less_equal__(f__integer__(X1),f__integer__(X0)) ) ),
inference(rectify,[],[f85]) ).
tff(f87,plain,
! [X1: $int,X0: $int] :
( ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) )
& ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f88,plain,
! [X0: $int,X1: $int] :
( ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) )
& ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) ) ),
inference(rectify,[],[f87]) ).
tff(f89,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| sP0(X1) ),
inference(cnf_transformation,[],[f68]) ).
tff(f90,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( X0 = X2 ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f91,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK4(X1,X2) = sK3(X1,X2) ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f92,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK3(X1,X2) = X2 ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f93,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( f__integer__(sK5(X1,X2)) = X1 ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f94,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK4(X1,X2) = f__integer__($product(sK5(X1,X2),sK6(X1,X2))) ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f95,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( f__integer__(sK6(X1,X2)) = X1 ) ),
inference(cnf_transformation,[],[f68]) ).
tff(f96,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ~ hp(X0) ),
inference(cnf_transformation,[],[f68]) ).
tff(f97,plain,
! [X0: general] :
( ~ sP1(X0)
| ( sK8(X0) = sK7(X0) ) ),
inference(cnf_transformation,[],[f71]) ).
tff(f98,plain,
! [X0: general] :
( ~ $less(sK11(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f71]) ).
tff(f99,plain,
! [X0: general] :
( ~ sP1(X0)
| ( 1 = sK11(X0) ) ),
inference(cnf_transformation,[],[f71]) ).
tff(f100,plain,
! [X0: general] :
( ~ $less(sK9(X0),sK10(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f71]) ).
tff(f101,plain,
! [X0: general] :
( ~ sP1(X0)
| ( f__integer__(sK9(X0)) = sK8(X0) ) ),
inference(cnf_transformation,[],[f71]) ).
tff(f102,plain,
! [X0: general] :
( ( $uminus(1) = sK10(X0) )
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f71]) ).
tff(f103,plain,
! [X0: general] :
( ~ sP1(X0)
| ( sK7(X0) = X0 ) ),
inference(cnf_transformation,[],[f71]) ).
tff(f104,plain,
! [X0: general] :
( ~ sP0(X0)
| ( sK12(X0) = X0 ) ),
inference(cnf_transformation,[],[f74]) ).
tff(f105,plain,
! [X0: general] :
( ~ sP0(X0)
| ( sK13(X0) = sK12(X0) ) ),
inference(cnf_transformation,[],[f74]) ).
tff(f106,plain,
! [X0: general] :
( ~ sP0(X0)
| ( f__integer__(sK16(X0)) = sK13(X0) ) ),
inference(cnf_transformation,[],[f74]) ).
tff(f107,plain,
! [X0: general] :
( ~ sP0(X0)
| ( 1 = sK15(X0) ) ),
inference(cnf_transformation,[],[f74]) ).
tff(f108,plain,
! [X0: general] :
( ~ $less(sK15(X0),sK16(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f109,plain,
! [X0: general] :
( ~ $less(sK16(X0),sK14(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f110,plain,
! [X0: general] :
( ( $uminus(1) = sK14(X0) )
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f111,plain,
( ( sK20 = sK17 )
| sP2(sK19,sK18,sK17) ),
inference(cnf_transformation,[],[f76]) ).
tff(f112,plain,
( ( sK21 = sK20 )
| sP2(sK19,sK18,sK17) ),
inference(cnf_transformation,[],[f76]) ).
tff(f113,plain,
( sP2(sK19,sK18,sK17)
| ( sK18 = f__integer__(sK23) ) ),
inference(cnf_transformation,[],[f76]) ).
tff(f114,plain,
( ( sK21 = f__integer__($product(sK23,sK22)) )
| sP2(sK19,sK18,sK17) ),
inference(cnf_transformation,[],[f76]) ).
tff(f115,plain,
( ( sK18 = f__integer__(sK22) )
| sP2(sK19,sK18,sK17) ),
inference(cnf_transformation,[],[f76]) ).
tff(f116,plain,
( sP2(sK19,sK18,sK17)
| sP1(sK18) ),
inference(cnf_transformation,[],[f76]) ).
tff(f117,plain,
( sP2(sK19,sK18,sK17)
| ~ tp(sK19) ),
inference(cnf_transformation,[],[f76]) ).
tff(f118,plain,
( sP2(sK19,sK18,sK17)
| ( sK19 = sK17 ) ),
inference(cnf_transformation,[],[f76]) ).
tff(f119,plain,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tff(f125,plain,
! [X0: general] :
( ~ hp(X0)
| tp(X0) ),
inference(cnf_transformation,[],[f51]) ).
tff(f133,plain,
! [X2: general,X3: general,X10: $int,X0: general,X11: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X4: general,X5: $int] :
( ( X0 != X4 )
| ( f__integer__(X6) != X2 )
| ( f__integer__(X5) != X2 )
| ( f__integer__($product(X6,X5)) != X3 )
| ( X3 != X4 )
| hp(X1)
| $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11)
| ( X7 != X8 )
| ( X2 != X7 )
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f83]) ).
tff(f135,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X1),f__integer__(X0))
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tff(f138,plain,
! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f88]) ).
tff(f141,plain,
! [X2: general,X3: general,X10: $int,X11: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X4: general,X5: $int] :
( ( f__integer__(X6) != X2 )
| ( f__integer__(X5) != X2 )
| ( f__integer__($product(X6,X5)) != X3 )
| ( X3 != X4 )
| hp(X1)
| $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11)
| ( X7 != X8 )
| ( X2 != X7 )
| ( X1 != X4 ) ),
inference(equality_resolution,[],[f133]) ).
tff(f142,plain,
! [X3: general,X10: $int,X11: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X4: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| ( f__integer__($product(X6,X5)) != X3 )
| ( X3 != X4 )
| hp(X1)
| $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11)
| ( X7 != X8 )
| ( f__integer__(X6) != X7 )
| ( X1 != X4 ) ),
inference(equality_resolution,[],[f141]) ).
tff(f143,plain,
! [X10: $int,X11: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X4: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| ( f__integer__($product(X6,X5)) != X4 )
| hp(X1)
| $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11)
| ( X7 != X8 )
| ( f__integer__(X6) != X7 )
| ( X1 != X4 ) ),
inference(equality_resolution,[],[f142]) ).
tff(f144,plain,
! [X10: $int,X11: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| hp(X1)
| $less(X10,X9)
| ( 0 != X11 )
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,X11)
| ( X7 != X8 )
| ( f__integer__(X6) != X7 )
| ( f__integer__($product(X6,X5)) != X1 ) ),
inference(equality_resolution,[],[f143]) ).
tff(f145,plain,
! [X10: $int,X1: general,X8: general,X6: $int,X9: $int,X7: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| hp(X1)
| $less(X10,X9)
| ( f__integer__(X9) != X8 )
| ( 1 != X10 )
| $less(X9,0)
| ( X7 != X8 )
| ( f__integer__(X6) != X7 )
| ( f__integer__($product(X6,X5)) != X1 ) ),
inference(equality_resolution,[],[f144]) ).
tff(f146,plain,
! [X10: $int,X1: general,X6: $int,X9: $int,X7: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| hp(X1)
| $less(X10,X9)
| ( 1 != X10 )
| $less(X9,0)
| ( f__integer__(X9) != X7 )
| ( f__integer__(X6) != X7 )
| ( f__integer__($product(X6,X5)) != X1 ) ),
inference(equality_resolution,[],[f145]) ).
tff(f147,plain,
! [X1: general,X6: $int,X9: $int,X7: general,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| hp(X1)
| $less(1,X9)
| $less(X9,0)
| ( f__integer__(X9) != X7 )
| ( f__integer__(X6) != X7 )
| ( f__integer__($product(X6,X5)) != X1 ) ),
inference(equality_resolution,[],[f146]) ).
tff(f148,plain,
! [X1: general,X6: $int,X9: $int,X5: $int] :
( ( f__integer__(X5) != f__integer__(X6) )
| hp(X1)
| $less(1,X9)
| $less(X9,0)
| ( f__integer__(X6) != f__integer__(X9) )
| ( f__integer__($product(X6,X5)) != X1 ) ),
inference(equality_resolution,[],[f147]) ).
tff(f149,plain,
! [X6: $int,X9: $int,X5: $int] :
( ( f__integer__(X6) != f__integer__(X9) )
| hp(f__integer__($product(X6,X5)))
| $less(1,X9)
| ( f__integer__(X5) != f__integer__(X6) )
| $less(X9,0) ),
inference(equality_resolution,[],[f148]) ).
tff(f161,plain,
! [X0: general] :
( ~ sP0(X0)
| ( -1 = sK14(X0) ) ),
inference(evaluation,[],[f110]) ).
tff(f162,plain,
! [X0: general] :
( ~ sP1(X0)
| ( -1 = sK10(X0) ) ),
inference(evaluation,[],[f102]) ).
tff(f164,definition,
( spl26_1
<=> ( sK19 = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
tff(f166,plain,
( ( sK19 = sK17 )
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f164]) ).
tff(f168,definition,
( spl26_2
<=> sP2(sK19,sK18,sK17) ),
introduced(definition,[new_symbols(definition,[spl26_2])],[avatar_definition]) ).
tff(f170,plain,
( sP2(sK19,sK18,sK17)
| ~ spl26_2 ),
inference(avatar_component_clause,[],[f168]) ).
tff(f171,plain,
( spl26_1
| spl26_2 ),
inference(avatar_split_clause,[],[f118,f168,f164]) ).
tff(f173,definition,
( spl26_3
<=> tp(sK19) ),
introduced(definition,[new_symbols(definition,[spl26_3])],[avatar_definition]) ).
tff(f175,plain,
( ~ tp(sK19)
| spl26_3 ),
inference(avatar_component_clause,[],[f173]) ).
tff(f176,plain,
( spl26_2
| ~ spl26_3 ),
inference(avatar_split_clause,[],[f117,f173,f168]) ).
tff(f178,definition,
( spl26_4
<=> ( sK18 = f__integer__(sK22) ) ),
introduced(definition,[new_symbols(definition,[spl26_4])],[avatar_definition]) ).
tff(f180,plain,
( ( sK18 = f__integer__(sK22) )
| ~ spl26_4 ),
inference(avatar_component_clause,[],[f178]) ).
tff(f181,plain,
( spl26_4
| spl26_2 ),
inference(avatar_split_clause,[],[f115,f168,f178]) ).
tff(f182,plain,
( sP2(sK19,sK18,sK17)
| ( f__integer__($product(sK22,sK23)) = sK21 ) ),
inference(forward_demodulation,[],[f114,f34]) ).
tff(f184,definition,
( spl26_5
<=> ( sK20 = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl26_5])],[avatar_definition]) ).
tff(f186,plain,
( ( sK20 = sK17 )
| ~ spl26_5 ),
inference(avatar_component_clause,[],[f184]) ).
tff(f187,plain,
( spl26_2
| spl26_5 ),
inference(avatar_split_clause,[],[f111,f184,f168]) ).
tff(f188,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK4(X1,X2) = f__integer__($product(sK6(X1,X2),sK5(X1,X2))) ) ),
inference(forward_demodulation,[],[f94,f34]) ).
tff(f190,definition,
( spl26_6
<=> sP1(sK18) ),
introduced(definition,[new_symbols(definition,[spl26_6])],[avatar_definition]) ).
tff(f192,plain,
( sP1(sK18)
| ~ spl26_6 ),
inference(avatar_component_clause,[],[f190]) ).
tff(f193,plain,
( spl26_2
| spl26_6 ),
inference(avatar_split_clause,[],[f116,f190,f168]) ).
tff(f195,definition,
( spl26_7
<=> ( sK21 = sK20 ) ),
introduced(definition,[new_symbols(definition,[spl26_7])],[avatar_definition]) ).
tff(f197,plain,
( ( sK21 = sK20 )
| ~ spl26_7 ),
inference(avatar_component_clause,[],[f195]) ).
tff(f198,plain,
( spl26_2
| spl26_7 ),
inference(avatar_split_clause,[],[f112,f195,f168]) ).
tff(f200,definition,
( spl26_8
<=> ( sK18 = f__integer__(sK23) ) ),
introduced(definition,[new_symbols(definition,[spl26_8])],[avatar_definition]) ).
tff(f202,plain,
( ( sK18 = f__integer__(sK23) )
| ~ spl26_8 ),
inference(avatar_component_clause,[],[f200]) ).
tff(f203,plain,
( spl26_2
| spl26_8 ),
inference(avatar_split_clause,[],[f113,f200,f168]) ).
tff(f205,definition,
( spl26_9
<=> ( f__integer__($product(sK22,sK23)) = sK21 ) ),
introduced(definition,[new_symbols(definition,[spl26_9])],[avatar_definition]) ).
tff(f207,plain,
( ( f__integer__($product(sK22,sK23)) = sK21 )
| ~ spl26_9 ),
inference(avatar_component_clause,[],[f205]) ).
tff(f208,plain,
( spl26_9
| spl26_2 ),
inference(avatar_split_clause,[],[f182,f168,f205]) ).
tff(f211,plain,
( sP0(sK18)
| ~ spl26_2 ),
inference(resolution,[],[f89,f170]) ).
tff(f212,plain,
( ~ hp(sK19)
| ~ spl26_2 ),
inference(resolution,[],[f96,f170]) ).
tff(f213,plain,
( ( sK18 = sK12(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f104,f211]) ).
tff(f214,plain,
( ( 1 = sK15(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f107,f211]) ).
tff(f215,plain,
! [X0: general] : p__less_equal__(X0,X0),
inference(factoring,[],[f119]) ).
tff(f219,plain,
( ( -1 = sK14(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f161,f211]) ).
tff(f232,plain,
( ( sK19 = sK17 )
| ~ spl26_2 ),
inference(resolution,[],[f90,f170]) ).
tff(f233,plain,
( spl26_1
| ~ spl26_2 ),
inference(avatar_split_clause,[],[f232,f168,f164]) ).
tff(f234,plain,
( ( sK21 = sK17 )
| ~ spl26_5
| ~ spl26_7 ),
inference(forward_demodulation,[],[f197,f186]) ).
tff(f235,plain,
( ( -1 = sK10(sK18) )
| ~ spl26_6 ),
inference(resolution,[],[f192,f162]) ).
tff(f236,plain,
( ( sK18 = sK7(sK18) )
| ~ spl26_6 ),
inference(resolution,[],[f192,f103]) ).
tff(f237,plain,
( ( 1 = sK11(sK18) )
| ~ spl26_6 ),
inference(resolution,[],[f192,f99]) ).
tff(f238,plain,
( ~ tp(sK17)
| ~ spl26_1
| spl26_3 ),
inference(superposition,[],[f175,f166]) ).
tff(f257,plain,
( ( sK8(sK18) = sK7(sK18) )
| ~ spl26_6 ),
inference(resolution,[],[f97,f192]) ).
tff(f258,plain,
( ( sK18 = sK8(sK18) )
| ~ spl26_6 ),
inference(forward_demodulation,[],[f257,f236]) ).
tff(f259,plain,
( ~ $less(sK9(sK18),-1)
| ~ sP1(sK18)
| ~ spl26_6 ),
inference(superposition,[],[f100,f235]) ).
tff(f260,plain,
( ~ $less(sK9(sK18),-1)
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f259,f192]) ).
tff(f261,plain,
( ~ sP1(sK18)
| ~ $less(1,sK9(sK18))
| ~ spl26_6 ),
inference(superposition,[],[f98,f237]) ).
tff(f262,plain,
( ~ $less(1,sK9(sK18))
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f261,f192]) ).
tff(f275,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$sum(1,X0))
| ~ $less(X0,X1) ),
inference(superposition,[],[f40,f23]) ).
tff(f276,plain,
( ( sK8(sK18) = f__integer__(sK9(sK18)) )
| ~ spl26_6 ),
inference(resolution,[],[f101,f192]) ).
tff(f277,plain,
( ( sK18 = f__integer__(sK9(sK18)) )
| ~ spl26_6 ),
inference(forward_demodulation,[],[f276,f258]) ).
tff(f290,plain,
( ! [X0: $int] :
( ~ p__less_equal__(sK18,f__integer__(X0))
| ~ $less(X0,sK22) )
| ~ spl26_4 ),
inference(superposition,[],[f135,f180]) ).
tff(f291,plain,
( ! [X0: $int] :
( ~ p__less_equal__(sK18,f__integer__(X0))
| ~ $less(X0,sK23) )
| ~ spl26_8 ),
inference(superposition,[],[f135,f202]) ).
tff(f294,plain,
( ! [X0: $int] :
( ~ p__less_equal__(f__integer__(X0),sK18)
| ~ $less(sK22,X0) )
| ~ spl26_4 ),
inference(superposition,[],[f135,f180]) ).
tff(f310,plain,
( ~ p__less_equal__(sK18,sK18)
| ~ $less(sK9(sK18),sK22)
| ~ spl26_4
| ~ spl26_6 ),
inference(superposition,[],[f290,f277]) ).
tff(f312,plain,
( ~ $less(sK23,sK22)
| ~ p__less_equal__(sK18,sK18)
| ~ spl26_4
| ~ spl26_8 ),
inference(superposition,[],[f290,f202]) ).
tff(f314,plain,
( ~ $less(sK9(sK18),sK22)
| ~ spl26_4
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f310,f215]) ).
tff(f315,plain,
( ~ $less(sK23,sK22)
| ~ spl26_4
| ~ spl26_8 ),
inference(forward_subsumption_resolution,[],[f312,f215]) ).
tff(f346,plain,
( $less(sK22,sK23)
| ( sK23 = sK22 )
| ~ spl26_4
| ~ spl26_8 ),
inference(resolution,[],[f30,f315]) ).
tff(f349,plain,
( $less(-1,sK9(sK18))
| ( sK9(sK18) = -1 )
| ~ spl26_6 ),
inference(resolution,[],[f30,f260]) ).
tff(f355,definition,
( spl26_12
<=> $less(-1,sK9(sK18)) ),
introduced(definition,[new_symbols(definition,[spl26_12])],[avatar_definition]) ).
tff(f357,plain,
( $less(-1,sK9(sK18))
| ~ spl26_12 ),
inference(avatar_component_clause,[],[f355]) ).
tff(f359,definition,
( spl26_13
<=> ( sK9(sK18) = -1 ) ),
introduced(definition,[new_symbols(definition,[spl26_13])],[avatar_definition]) ).
tff(f361,plain,
( ( sK9(sK18) = -1 )
| ~ spl26_13 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f364,definition,
( spl26_14
<=> $less(sK22,sK23) ),
introduced(definition,[new_symbols(definition,[spl26_14])],[avatar_definition]) ).
tff(f366,plain,
( $less(sK22,sK23)
| ~ spl26_14 ),
inference(avatar_component_clause,[],[f364]) ).
tff(f368,definition,
( spl26_15
<=> ( sK23 = sK22 ) ),
introduced(definition,[new_symbols(definition,[spl26_15])],[avatar_definition]) ).
tff(f370,plain,
( ( sK23 = sK22 )
| ~ spl26_15 ),
inference(avatar_component_clause,[],[f368]) ).
tff(f372,plain,
( spl26_13
| spl26_12
| ~ spl26_6 ),
inference(avatar_split_clause,[],[f349,f190,f355,f359]) ).
tff(f373,plain,
( spl26_14
| spl26_15
| ~ spl26_4
| ~ spl26_8 ),
inference(avatar_split_clause,[],[f346,f200,f178,f368,f364]) ).
tff(f433,plain,
! [X0: $int,X1: $int] :
( ~ $less(X0,X1)
| $less(0,$sum(X1,$uminus(X0))) ),
inference(superposition,[],[f31,f27]) ).
tff(f505,plain,
( ~ $less(sK22,sK23)
| ~ p__less_equal__(sK18,sK18)
| ~ spl26_4
| ~ spl26_8 ),
inference(superposition,[],[f291,f180]) ).
tff(f509,plain,
( ~ p__less_equal__(sK18,sK18)
| ~ spl26_4
| ~ spl26_8
| ~ spl26_14 ),
inference(forward_subsumption_resolution,[],[f505,f366]) ).
tff(f510,plain,
( $false
| ~ spl26_4
| ~ spl26_8
| ~ spl26_14 ),
inference(forward_subsumption_resolution,[],[f509,f215]) ).
tff(f511,plain,
( ~ spl26_4
| ~ spl26_8
| ~ spl26_14 ),
inference(avatar_contradiction_clause,[],[f510]) ).
tff(f542,plain,
( ( sK21 = f__integer__($product(sK22,sK22)) )
| ~ spl26_9
| ~ spl26_15 ),
inference(superposition,[],[f207,f370]) ).
tff(f544,plain,
( ( f__integer__($product(sK22,sK22)) = sK17 )
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15 ),
inference(forward_demodulation,[],[f542,f234]) ).
tff(f565,plain,
( ! [X0: $int,X1: $int] :
( $less(1,sK9(sK18))
| ( f__integer__(X0) != sK18 )
| ( f__integer__(X1) != f__integer__(X0) )
| $less(sK9(sK18),0)
| hp(f__integer__($product(X0,X1))) )
| ~ spl26_6 ),
inference(superposition,[],[f149,f277]) ).
tff(f568,plain,
! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| $less(X0,0)
| hp(f__integer__($product(X0,X1)))
| $less(1,X0) ),
inference(equality_resolution,[],[f149]) ).
tff(f570,definition,
( spl26_20
<=> ! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( f__integer__(X0) != sK18 )
| hp(f__integer__($product(X0,X1))) ) ),
introduced(definition,[new_symbols(definition,[spl26_20])],[avatar_definition]) ).
tff(f571,plain,
( ! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| hp(f__integer__($product(X0,X1)))
| ( f__integer__(X0) != sK18 ) )
| ~ spl26_20 ),
inference(avatar_component_clause,[],[f570]) ).
tff(f591,plain,
( ! [X0: $int,X1: $int] :
( hp(f__integer__($product(X0,X1)))
| ( f__integer__(X0) != sK18 )
| $less(sK9(sK18),0)
| ( f__integer__(X1) != f__integer__(X0) ) )
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f565,f262]) ).
tff(f601,definition,
( spl26_26
<=> $less(sK9(sK18),0) ),
introduced(definition,[new_symbols(definition,[spl26_26])],[avatar_definition]) ).
tff(f603,plain,
( $less(sK9(sK18),0)
| ~ spl26_26 ),
inference(avatar_component_clause,[],[f601]) ).
tff(f604,plain,
( spl26_20
| spl26_26
| ~ spl26_6 ),
inference(avatar_split_clause,[],[f591,f190,f601,f570]) ).
tff(f615,definition,
( spl26_28
<=> ! [X0: $int,X1: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(X0,X1)))
| ( f__integer__(X1) != f__integer__(X0) ) ) ),
introduced(definition,[new_symbols(definition,[spl26_28])],[avatar_definition]) ).
tff(f616,plain,
( ! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(X0,X1))) )
| ~ spl26_28 ),
inference(avatar_component_clause,[],[f615]) ).
tff(f623,definition,
( spl26_30
<=> ! [X0: $int] :
( $less(1,X0)
| ( f__integer__(X0) != sK17 )
| $less(X0,0) ) ),
introduced(definition,[new_symbols(definition,[spl26_30])],[avatar_definition]) ).
tff(f624,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK17 )
| $less(1,X0)
| $less(X0,0) )
| ~ spl26_30 ),
inference(avatar_component_clause,[],[f623]) ).
tff(f626,definition,
( spl26_31
<=> ! [X1: $int] :
( hp(f__integer__($product(sK22,$product(sK22,X1))))
| ( f__integer__(X1) != sK17 ) ) ),
introduced(definition,[new_symbols(definition,[spl26_31])],[avatar_definition]) ).
tff(f627,plain,
( ! [X1: $int] :
( ( f__integer__(X1) != sK17 )
| hp(f__integer__($product(sK22,$product(sK22,X1)))) )
| ~ spl26_31 ),
inference(avatar_component_clause,[],[f626]) ).
tff(f656,plain,
( ~ $less(sK22,sK9(sK18))
| ~ p__less_equal__(sK18,sK18)
| ~ spl26_4
| ~ spl26_6 ),
inference(superposition,[],[f294,f277]) ).
tff(f660,plain,
( ~ $less(sK22,sK9(sK18))
| ~ spl26_4
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f656,f215]) ).
tff(f687,plain,
( $less(sK9(sK18),sK22)
| ( sK9(sK18) = sK22 )
| ~ spl26_4
| ~ spl26_6 ),
inference(resolution,[],[f660,f30]) ).
tff(f690,plain,
( ( sK9(sK18) = sK22 )
| ~ spl26_4
| ~ spl26_6 ),
inference(forward_subsumption_resolution,[],[f687,f314]) ).
tff(f917,plain,
( ! [X0: $int,X1: $int] :
( $less(1,X0)
| ( f__integer__(X0) != sK17 )
| hp(f__integer__($product($product(sK22,sK22),X1)))
| ( f__integer__(X1) != sK17 )
| $less(X0,0) )
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15 ),
inference(superposition,[],[f149,f544]) ).
tff(f1023,plain,
( $less(1,$product(sK22,sK23))
| ( sK21 != sK17 )
| $less($product(sK22,sK23),0)
| ~ spl26_9
| ~ spl26_30 ),
inference(superposition,[],[f624,f207]) ).
tff(f1029,plain,
( $less(1,$product(sK22,sK23))
| $less($product(sK22,sK23),0)
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_30 ),
inference(forward_subsumption_resolution,[],[f1023,f234]) ).
tff(f1030,plain,
( $less(1,$product(sK22,sK23))
| $less($product(sK22,sK22),0)
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1029,f370]) ).
tff(f1043,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK18 )
| hp(f__integer__($product(X0,X0))) )
| ~ spl26_20 ),
inference(equality_resolution,[],[f571]) ).
tff(f1287,plain,
( $less(0,$sum(sK9(sK18),$uminus(-1)))
| ~ spl26_12 ),
inference(resolution,[],[f433,f357]) ).
tff(f1291,plain,
( $less(0,$sum(sK9(sK18),1))
| ~ spl26_12 ),
inference(evaluation,[],[f1287]) ).
tff(f1299,plain,
( $less(0,$sum(1,sK9(sK18)))
| ~ spl26_12 ),
inference(forward_demodulation,[],[f1291,f23]) ).
tff(f1329,plain,
( ~ $less(sK9(sK18),0)
| ~ spl26_12 ),
inference(resolution,[],[f1299,f275]) ).
tff(f1333,plain,
( $false
| ~ spl26_12
| ~ spl26_26 ),
inference(forward_subsumption_resolution,[],[f1329,f603]) ).
tff(f1334,plain,
( ~ spl26_12
| ~ spl26_26 ),
inference(avatar_contradiction_clause,[],[f1333]) ).
tff(f1396,plain,
( $less(1,$product(sK22,sK23))
| $less($product(sK9(sK18),sK9(sK18)),0)
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1030,f690]) ).
tff(f1401,plain,
( $less($product(sK9(sK18),sK9(sK18)),0)
| $less(1,$product(sK22,sK22))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1396,f370]) ).
tff(f1407,plain,
( $less($product(-1,-1),0)
| $less(1,$product(sK22,sK22))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1401,f361]) ).
tff(f1408,plain,
( $less(1,$product(sK22,sK22))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(evaluation,[],[f1407]) ).
tff(f1416,plain,
( $less(1,$product(sK9(sK18),sK9(sK18)))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1408,f690]) ).
tff(f1421,plain,
( $less(1,$product(-1,-1))
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(forward_demodulation,[],[f1416,f361]) ).
tff(f1422,plain,
( $false
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(evaluation,[],[f1421]) ).
tff(f1423,plain,
( ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(avatar_contradiction_clause,[],[f1422]) ).
tff(f1427,plain,
( ! [X1: $int] :
( ( f__integer__(X1) != sK17 )
| hp(f__integer__($product(sK9(sK18),$product(sK9(sK18),X1)))) )
| ~ spl26_4
| ~ spl26_6
| ~ spl26_31 ),
inference(forward_demodulation,[],[f627,f690]) ).
tff(f1428,plain,
( ! [X0: $int,X1: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(sK22,$product(sK22,X1))))
| $less(X0,0)
| ( f__integer__(X1) != sK17 )
| $less(1,X0) )
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15 ),
inference(forward_demodulation,[],[f917,f35]) ).
tff(f1433,plain,
( ! [X1: $int] :
( ( f__integer__(X1) != sK17 )
| hp(f__integer__($product(-1,$product(-1,X1)))) )
| ~ spl26_4
| ~ spl26_6
| ~ spl26_13
| ~ spl26_31 ),
inference(forward_demodulation,[],[f1427,f361]) ).
tff(f1434,plain,
( ! [X1: $int] :
( hp(f__integer__($uminus($uminus(X1))))
| ( f__integer__(X1) != sK17 ) )
| ~ spl26_4
| ~ spl26_6
| ~ spl26_13
| ~ spl26_31 ),
inference(evaluation,[],[f1433]) ).
tff(f4569,definition,
( spl26_53
<=> ( f__integer__(1) = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl26_53])],[avatar_definition]) ).
tff(f4570,plain,
( ( f__integer__(1) != sK17 )
| spl26_53 ),
inference(avatar_component_clause,[],[f4569]) ).
tff(f4571,plain,
( ( f__integer__(1) = sK17 )
| ~ spl26_53 ),
inference(avatar_component_clause,[],[f4569]) ).
tff(f4658,plain,
( ( sK18 != sK18 )
| hp(f__integer__($product(sK22,sK22)))
| ~ spl26_4
| ~ spl26_20 ),
inference(superposition,[],[f1043,f180]) ).
tff(f4660,plain,
( hp(f__integer__($product(sK22,sK22)))
| ~ spl26_4
| ~ spl26_20 ),
inference(trivial_inequality_removal,[],[f4658]) ).
tff(f4663,plain,
( hp(sK17)
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_20 ),
inference(forward_demodulation,[],[f4660,f544]) ).
tff(f4668,plain,
( tp(sK17)
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_20 ),
inference(resolution,[],[f4663,f125]) ).
tff(f4669,plain,
( $false
| ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_20 ),
inference(forward_subsumption_resolution,[],[f4668,f238]) ).
tff(f4670,plain,
( ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_20 ),
inference(avatar_contradiction_clause,[],[f4669]) ).
tff(f4672,plain,
( sP2(sK17,sK18,sK17)
| ~ spl26_1
| ~ spl26_2 ),
inference(forward_demodulation,[],[f170,f166]) ).
tff(f4676,plain,
( ! [X1: $int] :
( ( f__integer__(X1) != sK17 )
| hp(f__integer__(X1)) )
| ~ spl26_4
| ~ spl26_6
| ~ spl26_13
| ~ spl26_31 ),
inference(evaluation,[],[f1434]) ).
tff(f4744,plain,
( hp(sK17)
| ( sK17 != sK17 )
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(superposition,[],[f4676,f544]) ).
tff(f4748,plain,
( hp(sK17)
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(trivial_inequality_removal,[],[f4744]) ).
tff(f4751,plain,
( tp(sK17)
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(resolution,[],[f4748,f125]) ).
tff(f4752,plain,
( $false
| ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(forward_subsumption_resolution,[],[f4751,f238]) ).
tff(f4753,plain,
( ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(avatar_contradiction_clause,[],[f4752]) ).
tff(f4758,plain,
( ~ hp(sK17)
| ~ spl26_1
| ~ spl26_2 ),
inference(forward_demodulation,[],[f212,f166]) ).
tff(f4793,plain,
( spl26_30
| spl26_31
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15 ),
inference(avatar_split_clause,[],[f1428,f368,f205,f195,f184,f626,f623]) ).
tff(f4816,plain,
( ( sK3(sK18,sK17) = sK4(sK18,sK17) )
| ~ spl26_1
| ~ spl26_2 ),
inference(resolution,[],[f4672,f91]) ).
tff(f4817,plain,
( ( sK3(sK18,sK17) = sK17 )
| ~ spl26_1
| ~ spl26_2 ),
inference(resolution,[],[f4672,f92]) ).
tff(f4818,plain,
( ( sK18 = f__integer__(sK5(sK18,sK17)) )
| ~ spl26_1
| ~ spl26_2 ),
inference(resolution,[],[f4672,f93]) ).
tff(f4819,plain,
( ( sK18 = f__integer__(sK6(sK18,sK17)) )
| ~ spl26_1
| ~ spl26_2 ),
inference(resolution,[],[f4672,f95]) ).
tff(f4821,plain,
( ( sK4(sK18,sK17) = f__integer__($product(sK6(sK18,sK17),sK5(sK18,sK17))) )
| ~ spl26_1
| ~ spl26_2 ),
inference(resolution,[],[f4672,f188]) ).
tff(f4823,plain,
( ( sK12(sK18) = sK13(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f211,f105]) ).
tff(f4824,plain,
( ( f__integer__(sK16(sK18)) = sK13(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f211,f106]) ).
tff(f4829,plain,
( ( sK18 = sK13(sK18) )
| ~ spl26_2 ),
inference(forward_demodulation,[],[f4823,f213]) ).
tff(f4866,plain,
( ~ sP0(sK18)
| ~ $less(1,sK16(sK18))
| ~ spl26_2 ),
inference(superposition,[],[f108,f214]) ).
tff(f4867,plain,
( ~ $less(1,sK16(sK18))
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f4866,f211]) ).
tff(f4875,plain,
( ~ sP0(sK18)
| ~ $less(sK16(sK18),-1)
| ~ spl26_2 ),
inference(superposition,[],[f109,f219]) ).
tff(f4876,plain,
( ~ $less(sK16(sK18),-1)
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f4875,f211]) ).
tff(f4909,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK18 )
| hp(f__integer__($product(X0,sK5(sK18,sK17))))
| $less(1,X0)
| $less(X0,0) )
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f568,f4818]) ).
tff(f4979,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK18 )
| ( sK6(sK18,sK17) = X0 ) )
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f138,f4819]) ).
tff(f5050,plain,
( ( sK4(sK18,sK17) = sK17 )
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f4816,f4817]) ).
tff(f5133,plain,
( $less(-1,sK16(sK18))
| ( -1 = sK16(sK18) )
| ~ spl26_2 ),
inference(resolution,[],[f4876,f30]) ).
tff(f5137,definition,
( spl26_68
<=> ( -1 = sK16(sK18) ) ),
introduced(definition,[new_symbols(definition,[spl26_68])],[avatar_definition]) ).
tff(f5139,plain,
( ( -1 = sK16(sK18) )
| ~ spl26_68 ),
inference(avatar_component_clause,[],[f5137]) ).
tff(f5141,definition,
( spl26_69
<=> $less(-1,sK16(sK18)) ),
introduced(definition,[new_symbols(definition,[spl26_69])],[avatar_definition]) ).
tff(f5143,plain,
( $less(-1,sK16(sK18))
| ~ spl26_69 ),
inference(avatar_component_clause,[],[f5141]) ).
tff(f5145,plain,
( spl26_69
| spl26_68
| ~ spl26_2 ),
inference(avatar_split_clause,[],[f5133,f168,f5137,f5141]) ).
tff(f5449,plain,
( ( f__integer__(-1) = sK13(sK18) )
| ~ spl26_2
| ~ spl26_68 ),
inference(superposition,[],[f4824,f5139]) ).
tff(f5531,plain,
( ( sK18 = f__integer__(-1) )
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f5449,f4829]) ).
tff(f5881,plain,
( $less(0,$sum(sK16(sK18),$uminus(-1)))
| ~ spl26_69 ),
inference(resolution,[],[f5143,f433]) ).
tff(f5883,plain,
( $less(0,$sum(sK16(sK18),1))
| ~ spl26_69 ),
inference(evaluation,[],[f5881]) ).
tff(f5885,plain,
( $less(0,$sum(1,sK16(sK18)))
| ~ spl26_69 ),
inference(forward_demodulation,[],[f5883,f23]) ).
tff(f6844,plain,
( ( sK5(sK18,sK17) = sK6(sK18,sK17) )
| ( sK18 != sK18 )
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f4979,f4818]) ).
tff(f6846,plain,
( ( sK6(sK18,sK17) = sK16(sK18) )
| ( sK18 != sK13(sK18) )
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f4979,f4824]) ).
tff(f6848,plain,
( ( sK5(sK18,sK17) = sK6(sK18,sK17) )
| ~ spl26_1
| ~ spl26_2 ),
inference(trivial_inequality_removal,[],[f6844]) ).
tff(f6916,plain,
( ~ $less(sK16(sK18),0)
| ~ spl26_69 ),
inference(resolution,[],[f5885,f275]) ).
tff(f7955,plain,
( ! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| $less(1,1)
| hp(f__integer__($product(X0,X1)))
| ( f__integer__(X0) != sK17 )
| $less(1,0) )
| ~ spl26_53 ),
inference(superposition,[],[f149,f4571]) ).
tff(f8005,plain,
( ! [X0: $int,X1: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(X0,X1)))
| ( f__integer__(X1) != f__integer__(X0) ) )
| ~ spl26_53 ),
inference(evaluation,[],[f7955]) ).
tff(f8044,plain,
( spl26_28
| ~ spl26_53 ),
inference(avatar_split_clause,[],[f8005,f4569,f615]) ).
tff(f8607,plain,
( ( sK6(sK18,sK17) = sK16(sK18) )
| ~ spl26_1
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f6846,f4829]) ).
tff(f8669,plain,
( ( -1 = sK6(sK18,sK17) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f8607,f5139]) ).
tff(f8765,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK17 )
| ( f__integer__(X0) != sK4(sK18,sK17) )
| hp(f__integer__($product(X0,$product(sK6(sK18,sK17),sK5(sK18,sK17))))) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28 ),
inference(superposition,[],[f616,f4821]) ).
tff(f8777,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(X0,$product(sK6(sK18,sK17),sK5(sK18,sK17)))))
| ( f__integer__(X0) != sK17 ) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28 ),
inference(forward_demodulation,[],[f8765,f5050]) ).
tff(f8778,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__($product(X0,$product(sK6(sK18,sK17),sK5(sK18,sK17))))) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28 ),
inference(duplicate_literal_removal,[],[f8777]) ).
tff(f8788,plain,
( ! [X0: $int] :
( hp(f__integer__($product(X0,$product(sK6(sK18,sK17),sK6(sK18,sK17)))))
| ( f__integer__(X0) != sK17 ) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28 ),
inference(forward_demodulation,[],[f8778,f6848]) ).
tff(f8796,plain,
( ! [X0: $int] :
( hp(f__integer__($product(X0,$product(-1,-1))))
| ( f__integer__(X0) != sK17 ) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(forward_demodulation,[],[f8788,f8669]) ).
tff(f8797,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sK17 )
| hp(f__integer__(X0)) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(evaluation,[],[f8796]) ).
tff(f9033,plain,
( hp(sK4(sK18,sK17))
| ( sK4(sK18,sK17) != sK17 )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(superposition,[],[f8797,f4821]) ).
tff(f9038,plain,
( hp(sK4(sK18,sK17))
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(forward_subsumption_resolution,[],[f9033,f5050]) ).
tff(f9041,plain,
( hp(sK17)
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(forward_demodulation,[],[f9038,f5050]) ).
tff(f9043,plain,
( $false
| ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(forward_subsumption_resolution,[],[f9041,f4758]) ).
tff(f9044,plain,
( ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(avatar_contradiction_clause,[],[f9043]) ).
tff(f9055,definition,
( spl26_83
<=> $less(sK16(sK18),0) ),
introduced(definition,[new_symbols(definition,[spl26_83])],[avatar_definition]) ).
tff(f9056,plain,
( ~ $less(sK16(sK18),0)
| spl26_83 ),
inference(avatar_component_clause,[],[f9055]) ).
tff(f9073,plain,
( ~ spl26_83
| ~ spl26_69 ),
inference(avatar_split_clause,[],[f6916,f5141,f9055]) ).
tff(f11373,plain,
( ( sK18 != sK18 )
| hp(f__integer__($product(sK6(sK18,sK17),sK5(sK18,sK17))))
| $less(1,sK6(sK18,sK17))
| $less(sK6(sK18,sK17),0)
| ~ spl26_1
| ~ spl26_2 ),
inference(superposition,[],[f4909,f4819]) ).
tff(f11376,plain,
( $less(sK6(sK18,sK17),0)
| $less(1,sK6(sK18,sK17))
| hp(f__integer__($product(sK6(sK18,sK17),sK5(sK18,sK17))))
| ~ spl26_1
| ~ spl26_2 ),
inference(trivial_inequality_removal,[],[f11373]) ).
tff(f11401,plain,
( $less(1,sK6(sK18,sK17))
| hp(f__integer__($product(sK6(sK18,sK17),sK5(sK18,sK17))))
| $less(sK16(sK18),0)
| ~ spl26_1
| ~ spl26_2 ),
inference(forward_demodulation,[],[f11376,f8607]) ).
tff(f11404,plain,
( hp(f__integer__($product(sK6(sK18,sK17),sK5(sK18,sK17))))
| $less(1,sK6(sK18,sK17))
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_subsumption_resolution,[],[f11401,f9056]) ).
tff(f11405,plain,
( hp(sK4(sK18,sK17))
| $less(1,sK6(sK18,sK17))
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_demodulation,[],[f11404,f4821]) ).
tff(f11406,plain,
( $less(1,sK6(sK18,sK17))
| hp(sK17)
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_demodulation,[],[f11405,f5050]) ).
tff(f11407,plain,
( $less(1,sK6(sK18,sK17))
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_subsumption_resolution,[],[f11406,f4758]) ).
tff(f11408,plain,
( $less(1,sK16(sK18))
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_demodulation,[],[f11407,f8607]) ).
tff(f11409,plain,
( $false
| ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(forward_subsumption_resolution,[],[f11408,f4867]) ).
tff(f11410,plain,
( ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(avatar_contradiction_clause,[],[f11409]) ).
tff(f11840,plain,
( ( -1 = sK6(sK18,sK17) )
| ( sK18 != sK18 )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(superposition,[],[f4979,f5531]) ).
tff(f11879,plain,
( ( -1 = sK6(sK18,sK17) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(trivial_inequality_removal,[],[f11840]) ).
tff(f12013,plain,
( ( sK4(sK18,sK17) = f__integer__($product(-1,sK5(sK18,sK17))) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(superposition,[],[f4821,f11879]) ).
tff(f12027,plain,
( ( sK4(sK18,sK17) = f__integer__($uminus(sK5(sK18,sK17))) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(evaluation,[],[f12013]) ).
tff(f12033,plain,
( ( sK4(sK18,sK17) = f__integer__($uminus(sK6(sK18,sK17))) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f12027,f6848]) ).
tff(f12038,plain,
( ( f__integer__($uminus(sK16(sK18))) = sK4(sK18,sK17) )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f12033,f8607]) ).
tff(f12044,plain,
( ( f__integer__($uminus(sK16(sK18))) = sK17 )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f12038,f5050]) ).
tff(f12051,plain,
( ( f__integer__($uminus(-1)) = sK17 )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(forward_demodulation,[],[f12044,f5139]) ).
tff(f12052,plain,
( ( f__integer__(1) = sK17 )
| ~ spl26_1
| ~ spl26_2
| ~ spl26_68 ),
inference(evaluation,[],[f12051]) ).
tff(f12053,plain,
( $false
| ~ spl26_1
| ~ spl26_2
| spl26_53
| ~ spl26_68 ),
inference(forward_subsumption_resolution,[],[f12052,f4570]) ).
tff(f12054,plain,
( ~ spl26_1
| ~ spl26_2
| spl26_53
| ~ spl26_68 ),
inference(avatar_contradiction_clause,[],[f12053]) ).
cnf(s1,plain,
( spl26_1
| spl26_2 ),
inference(sat_conversion,[],[f171]) ).
cnf(s2,plain,
( spl26_2
| ~ spl26_3 ),
inference(sat_conversion,[],[f176]) ).
cnf(s3,plain,
( spl26_2
| spl26_4 ),
inference(sat_conversion,[],[f181]) ).
cnf(s4,plain,
( spl26_2
| spl26_5 ),
inference(sat_conversion,[],[f187]) ).
cnf(s5,plain,
( spl26_2
| spl26_6 ),
inference(sat_conversion,[],[f193]) ).
cnf(s6,plain,
( spl26_2
| spl26_7 ),
inference(sat_conversion,[],[f198]) ).
cnf(s7,plain,
( spl26_2
| spl26_8 ),
inference(sat_conversion,[],[f203]) ).
cnf(s8,plain,
( spl26_2
| spl26_9 ),
inference(sat_conversion,[],[f208]) ).
cnf(s9,plain,
( spl26_1
| ~ spl26_2 ),
inference(sat_conversion,[],[f233]) ).
cnf(s13,plain,
( ~ spl26_6
| spl26_12
| spl26_13 ),
inference(sat_conversion,[],[f372]) ).
cnf(s14,plain,
( ~ spl26_4
| ~ spl26_8
| spl26_14
| spl26_15 ),
inference(sat_conversion,[],[f373]) ).
cnf(s17,plain,
( ~ spl26_4
| ~ spl26_8
| ~ spl26_14 ),
inference(sat_conversion,[],[f511]) ).
cnf(s22,plain,
( ~ spl26_6
| spl26_20
| spl26_26 ),
inference(sat_conversion,[],[f604]) ).
cnf(s38,plain,
( ~ spl26_12
| ~ spl26_26 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s41,plain,
( ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_30 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s127,plain,
( ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| ~ spl26_20 ),
inference(sat_conversion,[],[f4670]) ).
cnf(s139,plain,
( ~ spl26_1
| spl26_3
| ~ spl26_4
| ~ spl26_5
| ~ spl26_6
| ~ spl26_7
| ~ spl26_9
| ~ spl26_13
| ~ spl26_15
| ~ spl26_31 ),
inference(sat_conversion,[],[f4753]) ).
cnf(s148,plain,
( ~ spl26_5
| ~ spl26_7
| ~ spl26_9
| ~ spl26_15
| spl26_30
| spl26_31 ),
inference(sat_conversion,[],[f4793]) ).
cnf(s171,plain,
( ~ spl26_2
| spl26_68
| spl26_69 ),
inference(sat_conversion,[],[f5145]) ).
cnf(s224,plain,
( spl26_28
| ~ spl26_53 ),
inference(sat_conversion,[],[f8044]) ).
cnf(s240,plain,
( ~ spl26_1
| ~ spl26_2
| ~ spl26_28
| ~ spl26_68 ),
inference(sat_conversion,[],[f9044]) ).
cnf(s246,plain,
( ~ spl26_69
| ~ spl26_83 ),
inference(sat_conversion,[],[f9073]) ).
cnf(s277,plain,
( ~ spl26_1
| ~ spl26_2
| spl26_83 ),
inference(sat_conversion,[],[f11410]) ).
cnf(s290,plain,
( ~ spl26_1
| ~ spl26_2
| spl26_53
| ~ spl26_68 ),
inference(sat_conversion,[],[f12054]) ).
cnf(s291,plain,
spl26_1,
inference(rat,[],[s1,s9]) ).
cnf(s292,plain,
spl26_2,
inference(rat,[],[s148,s139,s41,s13,s38,s22,s127,s14,s17,s2,s3,s4,s5,s6,s7,s8,s291]) ).
cnf(s294,plain,
spl26_83,
inference(rat,[],[s277,s291,s292]) ).
cnf(s297,plain,
~ spl26_69,
inference(rat,[],[s246,s294]) ).
cnf(s298,plain,
spl26_68,
inference(rat,[],[s171,s292,s297]) ).
cnf(s300,plain,
spl26_53,
inference(rat,[],[s290,s292,s291,s298]) ).
cnf(s302,plain,
~ spl26_28,
inference(rat,[],[s240,s292,s291,s298]) ).
cnf(s304,plain,
$false,
inference(rat,[],[s224,s300,s302]) ).
tff(f12055,plain,
$false,
inference(avatar_sat_refutation,[],[s304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX107_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n010.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:02 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.70/1.27 % (1986311)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.70/1.27 % (1986359)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4288845890:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.70/1.27 % (1986359)Instruction limit reached!
% 3.70/1.27 % (1986359)------------------------------
% 3.70/1.27 % (1986359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.27 % (1986359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.27 % (1986359)CaDiCaL version: 2.1.3
% 3.70/1.27 % (1986359)Termination reason: Instruction limit
% 3.70/1.27 % (1986359)Termination phase: Saturation
% 3.70/1.27 % (1986359)Time elapsed: 0.003 s
% 3.70/1.27 % (1986359)Peak memory usage: 89 MB
% 3.70/1.27 % (1986359)Instructions burned: 6 (million)
% 3.70/1.27 % (1986356)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=834746628:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.70/1.27 % (1986355)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3017349064:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.70/1.27 % (1986357)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4115399390:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.70/1.27 % (1986358)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3000085445:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.70/1.27 % (1986361)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1819774939:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.70/1.27 % (1986360)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1295901163:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.70/1.27 % (1986358)Instruction limit reached!
% 3.70/1.27 % (1986358)------------------------------
% 3.70/1.27 % (1986358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.27 % (1986358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.27 % (1986358)CaDiCaL version: 2.1.3
% 3.70/1.27 % (1986358)Termination reason: Instruction limit
% 3.70/1.27 % (1986358)Termination phase: Saturation
% 3.70/1.27 % (1986358)Time elapsed: 0.006 s
% 3.70/1.27 % (1986358)Peak memory usage: 88 MB
% 3.70/1.27 % (1986358)Instructions burned: 8 (million)
% 3.70/1.27 % (1986355)Instruction limit reached!
% 3.70/1.27 % (1986355)------------------------------
% 3.70/1.27 % (1986355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.27 % (1986355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.27 % (1986355)CaDiCaL version: 2.1.3
% 3.70/1.27 % (1986355)Termination reason: Instruction limit
% 3.70/1.27 % (1986355)Termination phase: Saturation
% 3.70/1.27 % (1986355)Time elapsed: 0.031 s
% 3.70/1.27 % (1986355)Peak memory usage: 116 MB
% 3.70/1.27 % (1986355)Instructions burned: 12 (million)
% 3.70/1.27 % (1986361)Instruction limit reached!
% 3.70/1.27 % (1986361)------------------------------
% 3.70/1.27 % (1986361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.27 % (1986361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.27 % (1986361)CaDiCaL version: 2.1.3
% 3.70/1.27 % (1986361)Termination reason: Instruction limit
% 3.70/1.27 % (1986361)Termination phase: Saturation
% 3.70/1.27 % (1986361)Time elapsed: 0.046 s
% 3.70/1.27 % (1986361)Peak memory usage: 116 MB
% 3.70/1.27 % (1986361)Instructions burned: 33 (million)
% 3.70/1.27 % (1986360)Instruction limit reached!
% 3.70/1.27 % (1986360)------------------------------
% 3.70/1.27 % (1986360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.27 % (1986360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.27 % (1986360)CaDiCaL version: 2.1.3
% 3.70/1.27 % (1986360)Termination reason: Instruction limit
% 3.70/1.27 % (1986360)Termination phase: Saturation
% 3.70/1.27 % (1986360)Time elapsed: 0.057 s
% 3.70/1.27 % (1986360)Peak memory usage: 117 MB
% 3.70/1.27 % (1986360)Instructions burned: 46 (million)
% 3.70/1.27 % (1986363)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3408461182:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.70/1.27 % (1986363)Instruction limit reached!
% 3.70/1.27 % (1986363)------------------------------
% 4.95/1.41 % (1986363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986363)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986363)Termination reason: Instruction limit
% 4.95/1.41 % (1986363)Termination phase: Saturation
% 4.95/1.41 % (1986363)Time elapsed: 0.006 s
% 4.95/1.41 % (1986363)Peak memory usage: 88 MB
% 4.95/1.41 % (1986363)Instructions burned: 14 (million)
% 4.95/1.41 % (1986357)Instruction limit reached!
% 4.95/1.41 % (1986357)------------------------------
% 4.95/1.41 % (1986357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986357)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986357)Termination reason: Instruction limit
% 4.95/1.41 % (1986357)Termination phase: Saturation
% 4.95/1.41 % (1986357)Time elapsed: 0.122 s
% 4.95/1.41 % (1986357)Peak memory usage: 116 MB
% 4.95/1.41 % (1986357)Instructions burned: 201 (million)
% 4.95/1.41 % (1986370)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=1676015689:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.95/1.41 % (1986370)Instruction limit reached!
% 4.95/1.41 % (1986370)------------------------------
% 4.95/1.41 % (1986370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986370)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986370)Termination reason: Instruction limit
% 4.95/1.41 % (1986370)Termination phase: Saturation
% 4.95/1.41 % (1986370)Time elapsed: 0.020 s
% 4.95/1.41 % (1986370)Peak memory usage: 89 MB
% 4.95/1.41 % (1986370)Instructions burned: 30 (million)
% 4.95/1.41 % (1986371)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2978759757:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.95/1.41 % (1986372)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=181797409:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.95/1.41 % (1986375)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2918293505:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.95/1.41 % (1986373)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=1655792731:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.95/1.41 % (1986371)Instruction limit reached!
% 4.95/1.41 % (1986371)------------------------------
% 4.95/1.41 % (1986371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986371)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986371)Termination reason: Instruction limit
% 4.95/1.41 % (1986371)Termination phase: Saturation
% 4.95/1.41 % (1986371)Time elapsed: 0.012 s
% 4.95/1.41 % (1986371)Peak memory usage: 90 MB
% 4.95/1.41 % (1986371)Instructions burned: 16 (million)
% 4.95/1.41 % (1986373)Refutation not found, incomplete strategy
% 4.95/1.41 % (1986373)------------------------------
% 4.95/1.41 % (1986373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986373)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986373)Termination reason: Refutation not found, incomplete strategy
% 4.95/1.41 % (1986373)Time elapsed: 0.006 s
% 4.95/1.41 % (1986373)Peak memory usage: 89 MB
% 4.95/1.41 % (1986373)Instructions burned: 6 (million)
% 4.95/1.41 % (1986372)Instruction limit reached!
% 4.95/1.41 % (1986372)------------------------------
% 4.95/1.41 % (1986372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.95/1.41 % (1986372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.95/1.41 % (1986372)CaDiCaL version: 2.1.3
% 4.95/1.41 % (1986372)Termination reason: Instruction limit
% 4.95/1.41 % (1986372)Termination phase: Saturation
% 4.95/1.41 % (1986372)Time elapsed: 0.019 s
% 4.95/1.41 % (1986372)Peak memory usage: 89 MB
% 4.95/1.41 % (1986372)Instructions burned: 24 (million)
% 4.95/1.41 % (1986375)Instruction limit reached!
% 4.95/1.41 % (1986375)------------------------------
% 4.95/1.41 % (1986375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986375)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986375)Termination reason: Instruction limit
% 5.68/1.58 % (1986375)Termination phase: Saturation
% 5.68/1.58 % (1986375)Time elapsed: 0.023 s
% 5.68/1.58 % (1986375)Peak memory usage: 89 MB
% 5.68/1.58 % (1986375)Instructions burned: 90 (million)
% 5.68/1.58 % (1986356)Instruction limit reached!
% 5.68/1.58 % (1986356)------------------------------
% 5.68/1.58 % (1986356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986356)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986356)Termination reason: Instruction limit
% 5.68/1.58 % (1986356)Termination phase: Saturation
% 5.68/1.58 % (1986356)Time elapsed: 0.223 s
% 5.68/1.58 % (1986356)Peak memory usage: 119 MB
% 5.68/1.58 % (1986356)Instructions burned: 308 (million)
% 5.68/1.58 % (1986376)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2682564787:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.68/1.58 % (1986376)Instruction limit reached!
% 5.68/1.58 % (1986376)------------------------------
% 5.68/1.58 % (1986376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986376)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986376)Termination reason: Instruction limit
% 5.68/1.58 % (1986376)Termination phase: Saturation
% 5.68/1.58 % (1986376)Time elapsed: 0.002 s
% 5.68/1.58 % (1986376)Peak memory usage: 86 MB
% 5.68/1.58 % (1986376)Instructions burned: 2 (million)
% 5.68/1.58 % (1986385)lrs+10_1_thi=all:si=on:fd=off:random_seed=3828010722:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.68/1.58 % (1986380)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2216020486:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.68/1.58 % (1986383)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2974742201:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.68/1.58 % (1986383)Instruction limit reached!
% 5.68/1.58 % (1986383)------------------------------
% 5.68/1.58 % (1986383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986383)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986383)Termination reason: Instruction limit
% 5.68/1.58 % (1986383)Termination phase: Saturation
% 5.68/1.58 % (1986383)Time elapsed: 0.003 s
% 5.68/1.58 % (1986383)Peak memory usage: 88 MB
% 5.68/1.58 % (1986383)Instructions burned: 4 (million)
% 5.68/1.58 % (1986385)Instruction limit reached!
% 5.68/1.58 % (1986385)------------------------------
% 5.68/1.58 % (1986385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986385)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986385)Termination reason: Instruction limit
% 5.68/1.58 % (1986385)Termination phase: Saturation
% 5.68/1.58 % (1986385)Time elapsed: 0.038 s
% 5.68/1.58 % (1986385)Peak memory usage: 116 MB
% 5.68/1.58 % (1986385)Instructions burned: 55 (million)
% 5.68/1.58 % (1986384)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=173621182:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.68/1.58 % (1986386)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=351964771:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.68/1.58 % (1986386)Instruction limit reached!
% 5.68/1.58 % (1986386)------------------------------
% 5.68/1.58 % (1986386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.58 % (1986386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.58 % (1986386)CaDiCaL version: 2.1.3
% 5.68/1.58 % (1986386)Termination reason: Instruction limit
% 5.68/1.58 % (1986386)Termination phase: Saturation
% 5.68/1.58 % (1986386)Time elapsed: 0.006 s
% 5.68/1.58 % (1986386)Peak memory usage: 88 MB
% 5.68/1.58 % (1986386)Instructions burned: 8 (million)
% 5.68/1.58 % (1986373)------------------------------
% 7.72/1.83 % (1986373)------------------------------
% 7.72/1.83 % (1986388)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2087842341:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 7.72/1.83 % (1986388)Instruction limit reached!
% 7.72/1.83 % (1986388)------------------------------
% 7.72/1.83 % (1986388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986388)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986388)Termination reason: Instruction limit
% 7.72/1.83 % (1986388)Termination phase: Saturation
% 7.72/1.83 % (1986388)Time elapsed: 0.002 s
% 7.72/1.83 % (1986388)Peak memory usage: 88 MB
% 7.72/1.83 % (1986388)Instructions burned: 2 (million)
% 7.72/1.83 % (1986380)Instruction limit reached!
% 7.72/1.83 % (1986380)------------------------------
% 7.72/1.83 % (1986380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986380)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986380)Termination reason: Instruction limit
% 7.72/1.83 % (1986380)Termination phase: Saturation
% 7.72/1.83 % (1986380)Time elapsed: 0.129 s
% 7.72/1.83 % (1986380)Peak memory usage: 91 MB
% 7.72/1.83 % (1986380)Instructions burned: 182 (million)
% 7.72/1.83 % (1986384)Instruction limit reached!
% 7.72/1.83 % (1986384)------------------------------
% 7.72/1.83 % (1986384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986384)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986384)Termination reason: Instruction limit
% 7.72/1.83 % (1986384)Termination phase: Saturation
% 7.72/1.83 % (1986384)Time elapsed: 0.096 s
% 7.72/1.83 % (1986384)Peak memory usage: 135 MB
% 7.72/1.83 % (1986384)Instructions burned: 67 (million)
% 7.72/1.83 % (1986392)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=348012831:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.72/1.83 % (1986392)Instruction limit reached!
% 7.72/1.83 % (1986392)------------------------------
% 7.72/1.83 % (1986392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986392)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986392)Termination reason: Instruction limit
% 7.72/1.83 % (1986392)Termination phase: Saturation
% 7.72/1.83 % (1986392)Time elapsed: 0.002 s
% 7.72/1.83 % (1986392)Peak memory usage: 89 MB
% 7.72/1.83 % (1986392)Instructions burned: 3 (million)
% 7.72/1.83 % (1986393)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2748773899:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.72/1.83 % (1986396)dis+10_1_si=on:random_seed=3236035846:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.72/1.83 % (1986396)Instruction limit reached!
% 7.72/1.83 % (1986396)------------------------------
% 7.72/1.83 % (1986396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986396)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986396)Termination reason: Instruction limit
% 7.72/1.83 % (1986396)Termination phase: Saturation
% 7.72/1.83 % (1986396)Time elapsed: 0.009 s
% 7.72/1.83 % (1986396)Peak memory usage: 88 MB
% 7.72/1.83 % (1986396)Instructions burned: 11 (million)
% 7.72/1.83 % (1986403)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2870043608:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.72/1.83 % (1986403)Refutation not found, incomplete strategy
% 7.72/1.83 % (1986403)------------------------------
% 7.72/1.83 % (1986403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.83 % (1986403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.83 % (1986403)CaDiCaL version: 2.1.3
% 7.72/1.83 % (1986403)Termination reason: Refutation not found, incomplete strategy
% 7.72/1.83 % (1986403)Time elapsed: 0.002 s
% 7.72/1.83 % (1986403)Peak memory usage: 89 MB
% 7.72/1.83 % (1986403)Instructions burned: 3 (million)
% 7.72/1.83 % (1986398)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=4112920000:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 7.72/1.83 % (1986400)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=666007080:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.08/2.05 % (1986399)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1373951497:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi)
% 10.08/2.05 % (1986400)Instruction limit reached!
% 10.08/2.05 % (1986400)------------------------------
% 10.08/2.05 % (1986400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986400)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986400)Termination reason: Instruction limit
% 10.08/2.05 % (1986400)Termination phase: Saturation
% 10.08/2.05 % (1986400)Time elapsed: 0.002 s
% 10.08/2.05 % (1986400)Peak memory usage: 88 MB
% 10.08/2.05 % (1986400)Instructions burned: 3 (million)
% 10.08/2.05 % (1986398)Refutation not found, incomplete strategy
% 10.08/2.05 % (1986398)------------------------------
% 10.08/2.05 % (1986398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986398)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986398)Termination reason: Refutation not found, incomplete strategy
% 10.08/2.05 % (1986398)Time elapsed: 0.004 s
% 10.08/2.05 % (1986398)Peak memory usage: 88 MB
% 10.08/2.05 % (1986398)Instructions burned: 4 (million)
% 10.08/2.05 % (1986399)Instruction limit reached!
% 10.08/2.05 % (1986399)------------------------------
% 10.08/2.05 % (1986399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986399)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986399)Termination reason: Instruction limit
% 10.08/2.05 % (1986399)Termination phase: Saturation
% 10.08/2.05 % (1986399)Time elapsed: 0.029 s
% 10.08/2.05 % (1986399)Peak memory usage: 89 MB
% 10.08/2.05 % (1986399)Instructions burned: 36 (million)
% 10.08/2.05 % (1986402)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1081096544:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.08/2.05 % (1986393)Instruction limit reached!
% 10.08/2.05 % (1986393)------------------------------
% 10.08/2.05 % (1986393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986393)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986393)Termination reason: Instruction limit
% 10.08/2.05 % (1986393)Termination phase: Saturation
% 10.08/2.05 % (1986393)Time elapsed: 0.102 s
% 10.08/2.05 % (1986393)Peak memory usage: 118 MB
% 10.08/2.05 % (1986393)Instructions burned: 127 (million)
% 10.08/2.05 % (1986402)Instruction limit reached!
% 10.08/2.05 % (1986402)------------------------------
% 10.08/2.05 % (1986402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986402)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986402)Termination reason: Instruction limit
% 10.08/2.05 % (1986402)Termination phase: Saturation
% 10.08/2.05 % (1986402)Time elapsed: 0.007 s
% 10.08/2.05 % (1986402)Peak memory usage: 88 MB
% 10.08/2.05 % (1986402)Instructions burned: 8 (million)
% 10.08/2.05 % (1986406)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=173031211:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 10.08/2.05 % (1986403)------------------------------
% 10.08/2.05 % (1986403)------------------------------
% 10.08/2.05 % (1986411)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1261769580:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.08/2.05 % (1986406)Instruction limit reached!
% 10.08/2.05 % (1986406)------------------------------
% 10.08/2.05 % (1986406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.08/2.05 % (1986406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.08/2.05 % (1986406)CaDiCaL version: 2.1.3
% 10.08/2.05 % (1986406)Termination reason: Instruction limit
% 10.08/2.05 % (1986406)Termination phase: Saturation
% 10.08/2.05 % (1986406)Time elapsed: 0.033 s
% 10.08/2.05 % (1986406)Peak memory usage: 116 MB
% 11.44/2.33 % (1986406)Instructions burned: 13 (million)
% 11.44/2.33 % (1986413)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1205030213:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.44/2.33 % (1986413)Instruction limit reached!
% 11.44/2.33 % (1986413)------------------------------
% 11.44/2.33 % (1986413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.44/2.33 % (1986413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.33 % (1986413)CaDiCaL version: 2.1.3
% 11.44/2.33 % (1986413)Termination reason: Instruction limit
% 11.44/2.33 % (1986413)Termination phase: Saturation
% 11.44/2.33 % (1986413)Time elapsed: 0.008 s
% 11.44/2.33 % (1986413)Peak memory usage: 88 MB
% 11.44/2.33 % (1986413)Instructions burned: 10 (million)
% 11.44/2.33 % (1986415)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=1778391973:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 11.44/2.33 % (1986414)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=383328940:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 11.44/2.33 % (1986398)------------------------------
% 11.44/2.33 % (1986398)------------------------------
% 11.44/2.33 % (1986415)Instruction limit reached!
% 11.44/2.33 % (1986415)------------------------------
% 11.44/2.33 % (1986415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.44/2.33 % (1986415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.33 % (1986415)CaDiCaL version: 2.1.3
% 11.44/2.33 % (1986415)Termination reason: Instruction limit
% 11.44/2.33 % (1986415)Termination phase: Saturation
% 11.44/2.33 % (1986415)Time elapsed: 0.058 s
% 11.44/2.33 % (1986415)Peak memory usage: 90 MB
% 11.44/2.33 % (1986415)Instructions burned: 75 (million)
% 11.44/2.33 % (1986418)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=307616032:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi)
% 11.44/2.33 % (1986414)Instruction limit reached!
% 11.44/2.33 % (1986414)------------------------------
% 11.44/2.33 % (1986414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.44/2.33 % (1986414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.33 % (1986414)CaDiCaL version: 2.1.3
% 11.44/2.33 % (1986414)Termination reason: Instruction limit
% 11.44/2.33 % (1986414)Termination phase: Saturation
% 11.44/2.33 % (1986414)Time elapsed: 0.096 s
% 11.44/2.33 % (1986414)Peak memory usage: 134 MB
% 11.44/2.33 % (1986414)Instructions burned: 72 (million)
% 11.44/2.33 % (1986420)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2555643191:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 11.44/2.33 % (1986411)Instruction limit reached!
% 11.44/2.33 % (1986411)------------------------------
% 11.44/2.33 % (1986411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.44/2.33 % (1986411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.33 % (1986411)CaDiCaL version: 2.1.3
% 11.44/2.33 % (1986411)Termination reason: Instruction limit
% 11.44/2.33 % (1986411)Termination phase: Saturation
% 11.44/2.33 % (1986411)Time elapsed: 0.187 s
% 11.44/2.33 % (1986411)Peak memory usage: 119 MB
% 11.44/2.33 % (1986411)Instructions burned: 227 (million)
% 11.44/2.33 % (1986421)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3373572511:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.44/2.33 % (1986418)Instruction limit reached!
% 11.44/2.33 % (1986418)------------------------------
% 11.44/2.33 % (1986418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.44/2.33 % (1986418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.44/2.33 % (1986418)CaDiCaL version: 2.1.3
% 11.44/2.33 % (1986418)Termination reason: Instruction limit
% 11.44/2.33 % (1986418)Termination phase: Saturation
% 11.44/2.33 % (1986418)Time elapsed: 0.104 s
% 11.44/2.33 % (1986418)Peak memory usage: 90 MB
% 11.44/2.33 % (1986418)Instructions burned: 297 (million)
% 11.44/2.33 % (1986424)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2034121225:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 11.44/2.33 % (1986425)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3111996453:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 12.97/2.64 % (1986420)Instruction limit reached!
% 12.97/2.64 % (1986420)------------------------------
% 12.97/2.64 % (1986420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986420)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986420)Termination reason: Instruction limit
% 12.97/2.64 % (1986420)Termination phase: Saturation
% 12.97/2.64 % (1986420)Time elapsed: 0.112 s
% 12.97/2.64 % (1986420)Peak memory usage: 119 MB
% 12.97/2.64 % (1986420)Instructions burned: 132 (million)
% 12.97/2.64 % (1986427)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1783019083:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 12.97/2.64 % (1986424)Instruction limit reached!
% 12.97/2.64 % (1986424)------------------------------
% 12.97/2.64 % (1986424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986424)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986424)Termination reason: Instruction limit
% 12.97/2.64 % (1986424)Termination phase: Saturation
% 12.97/2.64 % (1986424)Time elapsed: 0.073 s
% 12.97/2.64 % (1986424)Peak memory usage: 135 MB
% 12.97/2.64 % (1986424)Instructions burned: 41 (million)
% 12.97/2.64 % (1986430)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3137715300:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.97/2.64 % (1986421)Instruction limit reached!
% 12.97/2.64 % (1986421)------------------------------
% 12.97/2.64 % (1986421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986421)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986421)Termination reason: Instruction limit
% 12.97/2.64 % (1986421)Termination phase: Saturation
% 12.97/2.64 % (1986421)Time elapsed: 0.142 s
% 12.97/2.64 % (1986421)Peak memory usage: 136 MB
% 12.97/2.64 % (1986421)Instructions burned: 131 (million)
% 12.97/2.64 % (1986431)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=705047894:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi)
% 12.97/2.64 % (1986430)Instruction limit reached!
% 12.97/2.64 % (1986430)------------------------------
% 12.97/2.64 % (1986430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986430)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986430)Termination reason: Instruction limit
% 12.97/2.64 % (1986430)Termination phase: Saturation
% 12.97/2.64 % (1986430)Time elapsed: 0.099 s
% 12.97/2.64 % (1986430)Peak memory usage: 117 MB
% 12.97/2.64 % (1986430)Instructions burned: 132 (million)
% 12.97/2.64 % (1986431)Instruction limit reached!
% 12.97/2.64 % (1986431)------------------------------
% 12.97/2.64 % (1986431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986431)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986431)Termination reason: Instruction limit
% 12.97/2.64 % (1986431)Termination phase: Saturation
% 12.97/2.64 % (1986431)Time elapsed: 0.113 s
% 12.97/2.64 % (1986431)Peak memory usage: 119 MB
% 12.97/2.64 % (1986431)Instructions burned: 261 (million)
% 12.97/2.64 % (1986435)dis+10_1_si=on:random_seed=3772268817:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 12.97/2.64 % (1986436)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1571644708:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 12.97/2.64 % (1986425)Instruction limit reached!
% 12.97/2.64 % (1986425)------------------------------
% 12.97/2.64 % (1986425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.97/2.64 % (1986425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.97/2.64 % (1986425)CaDiCaL version: 2.1.3
% 12.97/2.64 % (1986425)Termination reason: Instruction limit
% 12.97/2.64 % (1986425)Termination phase: Saturation
% 12.97/2.64 % (1986425)Time elapsed: 0.215 s
% 12.97/2.64 % (1986425)Peak memory usage: 92 MB
% 12.97/2.64 % (1986425)Instructions burned: 307 (million)
% 15.25/2.91 % (1986439)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3757122492:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 15.25/2.91 % (1986442)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2100576556:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 15.25/2.91 % (1986440)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4007357406:i=65:nm=16:rtra=on_2986 on theBenchmark for (2986ds/65Mi)
% 15.25/2.91 % (1986439)Instruction limit reached!
% 15.25/2.91 % (1986439)------------------------------
% 15.25/2.91 % (1986439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986439)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986439)Termination reason: Instruction limit
% 15.25/2.91 % (1986439)Termination phase: Saturation
% 15.25/2.91 % (1986439)Time elapsed: 0.092 s
% 15.25/2.91 % (1986439)Peak memory usage: 90 MB
% 15.25/2.91 % (1986439)Instructions burned: 141 (million)
% 15.25/2.91 % (1986442)Instruction limit reached!
% 15.25/2.91 % (1986442)------------------------------
% 15.25/2.91 % (1986442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986442)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986442)Termination reason: Instruction limit
% 15.25/2.91 % (1986442)Termination phase: Saturation
% 15.25/2.91 % (1986442)Time elapsed: 0.041 s
% 15.25/2.91 % (1986442)Peak memory usage: 90 MB
% 15.25/2.91 % (1986442)Instructions burned: 122 (million)
% 15.25/2.91 % (1986440)Instruction limit reached!
% 15.25/2.91 % (1986440)------------------------------
% 15.25/2.91 % (1986440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986440)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986440)Termination reason: Instruction limit
% 15.25/2.91 % (1986440)Termination phase: Saturation
% 15.25/2.91 % (1986440)Time elapsed: 0.069 s
% 15.25/2.91 % (1986440)Peak memory usage: 118 MB
% 15.25/2.91 % (1986440)Instructions burned: 65 (million)
% 15.25/2.91 % (1986444)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=1449102999:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 15.25/2.91 % (1986436)Instruction limit reached!
% 15.25/2.91 % (1986436)------------------------------
% 15.25/2.91 % (1986436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986436)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986436)Termination reason: Instruction limit
% 15.25/2.91 % (1986436)Termination phase: Saturation
% 15.25/2.91 % (1986436)Time elapsed: 0.237 s
% 15.25/2.91 % (1986436)Peak memory usage: 91 MB
% 15.25/2.91 % (1986436)Instructions burned: 384 (million)
% 15.25/2.91 % (1986449)dis+1010_1_to=kbo:si=on:random_seed=3097142794:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 15.25/2.91 % (1986448)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=2081783515:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi)
% 15.25/2.91 % (1986427)Instruction limit reached!
% 15.25/2.91 % (1986427)------------------------------
% 15.25/2.91 % (1986427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986427)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986427)Termination reason: Instruction limit
% 15.25/2.91 % (1986427)Termination phase: Saturation
% 15.25/2.91 % (1986427)Time elapsed: 0.461 s
% 15.25/2.91 % (1986427)Peak memory usage: 138 MB
% 15.25/2.91 % (1986427)Instructions burned: 598 (million)
% 15.25/2.91 % (1986444)Instruction limit reached!
% 15.25/2.91 % (1986444)------------------------------
% 15.25/2.91 % (1986444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/2.91 % (1986444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/2.91 % (1986444)CaDiCaL version: 2.1.3
% 15.25/2.91 % (1986444)Termination reason: Instruction limit
% 15.25/2.91 % (1986444)Termination phase: Saturation
% 15.25/2.91 % (1986444)Time elapsed: 0.114 s
% 15.25/2.91 % (1986444)Peak memory usage: 119 MB
% 18.04/3.26 % (1986444)Instructions burned: 128 (million)
% 18.04/3.26 % (1986449)Instruction limit reached!
% 18.04/3.26 % (1986449)------------------------------
% 18.04/3.26 % (1986449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986449)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986449)Termination reason: Instruction limit
% 18.04/3.26 % (1986449)Termination phase: Saturation
% 18.04/3.26 % (1986449)Time elapsed: 0.071 s
% 18.04/3.26 % (1986449)Peak memory usage: 92 MB
% 18.04/3.26 % (1986449)Instructions burned: 177 (million)
% 18.04/3.26 % (1986451)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=293227213:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 18.04/3.26 % (1986448)Instruction limit reached!
% 18.04/3.26 % (1986448)------------------------------
% 18.04/3.26 % (1986448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986448)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986448)Termination reason: Instruction limit
% 18.04/3.26 % (1986448)Termination phase: Saturation
% 18.04/3.26 % (1986448)Time elapsed: 0.054 s
% 18.04/3.26 % (1986448)Peak memory usage: 118 MB
% 18.04/3.26 % (1986448)Instructions burned: 40 (million)
% 18.04/3.26 % (1986452)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3040058833:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi)
% 18.04/3.26 % (1986458)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3769274242:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 18.04/3.26 % (1986456)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2313135397:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 18.04/3.26 % (1986455)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1061997337:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi)
% 18.04/3.26 % (1986459)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1553283138:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.04/3.26 % (1986451)Instruction limit reached!
% 18.04/3.26 % (1986451)------------------------------
% 18.04/3.26 % (1986451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986451)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986451)Termination reason: Instruction limit
% 18.04/3.26 % (1986451)Termination phase: Saturation
% 18.04/3.26 % (1986451)Time elapsed: 0.181 s
% 18.04/3.26 % (1986451)Peak memory usage: 116 MB
% 18.04/3.26 % (1986451)Instructions burned: 331 (million)
% 18.04/3.26 % (1986458)Instruction limit reached!
% 18.04/3.26 % (1986458)------------------------------
% 18.04/3.26 % (1986458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986458)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986458)Termination reason: Instruction limit
% 18.04/3.26 % (1986458)Termination phase: Saturation
% 18.04/3.26 % (1986458)Time elapsed: 0.087 s
% 18.04/3.26 % (1986458)Peak memory usage: 91 MB
% 18.04/3.26 % (1986458)Instructions burned: 296 (million)
% 18.04/3.26 % (1986435)Instruction limit reached!
% 18.04/3.26 % (1986435)------------------------------
% 18.04/3.26 % (1986435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986435)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986435)Termination reason: Instruction limit
% 18.04/3.26 % (1986435)Termination phase: Saturation
% 18.04/3.26 % (1986435)Time elapsed: 0.531 s
% 18.04/3.26 % (1986435)Peak memory usage: 93 MB
% 18.04/3.26 % (1986435)Instructions burned: 1000 (million)
% 18.04/3.26 % (1986455)Instruction limit reached!
% 18.04/3.26 % (1986455)------------------------------
% 18.04/3.26 % (1986455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/3.26 % (1986455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/3.26 % (1986455)CaDiCaL version: 2.1.3
% 18.04/3.26 % (1986455)Termination reason: Instruction limit
% 19.13/3.52 % (1986455)Termination phase: Saturation
% 19.13/3.52 % (1986455)Time elapsed: 0.176 s
% 19.13/3.52 % (1986455)Peak memory usage: 137 MB
% 19.13/3.52 % (1986455)Instructions burned: 217 (million)
% 19.13/3.52 % (1986466)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1037804496:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 19.13/3.52 % (1986465)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2568758094:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi)
% 19.13/3.52 % (1986467)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2281807727:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 19.13/3.52 % (1986456)Instruction limit reached!
% 19.13/3.52 % (1986456)------------------------------
% 19.13/3.52 % (1986456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986456)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986456)Termination reason: Instruction limit
% 19.13/3.52 % (1986456)Termination phase: Saturation
% 19.13/3.52 % (1986456)Time elapsed: 0.243 s
% 19.13/3.52 % (1986456)Peak memory usage: 118 MB
% 19.13/3.52 % (1986456)Instructions burned: 351 (million)
% 19.13/3.52 % (1986459)Instruction limit reached!
% 19.13/3.52 % (1986459)------------------------------
% 19.13/3.52 % (1986459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986459)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986459)Termination reason: Instruction limit
% 19.13/3.52 % (1986459)Termination phase: Saturation
% 19.13/3.52 % (1986459)Time elapsed: 0.234 s
% 19.13/3.52 % (1986459)Peak memory usage: 120 MB
% 19.13/3.52 % (1986459)Instructions burned: 328 (million)
% 19.13/3.52 % (1986466)Instruction limit reached!
% 19.13/3.52 % (1986466)------------------------------
% 19.13/3.52 % (1986466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986466)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986466)Termination reason: Instruction limit
% 19.13/3.52 % (1986466)Termination phase: Saturation
% 19.13/3.52 % (1986466)Time elapsed: 0.134 s
% 19.13/3.52 % (1986466)Peak memory usage: 90 MB
% 19.13/3.52 % (1986466)Instructions burned: 485 (million)
% 19.13/3.52 % (1986468)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=163481010:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 19.13/3.52 % (1986452)Instruction limit reached!
% 19.13/3.52 % (1986452)------------------------------
% 19.13/3.52 % (1986452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986452)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986452)Termination reason: Instruction limit
% 19.13/3.52 % (1986452)Termination phase: Saturation
% 19.13/3.52 % (1986452)Time elapsed: 0.397 s
% 19.13/3.52 % (1986452)Peak memory usage: 136 MB
% 19.13/3.52 % (1986452)Instructions burned: 484 (million)
% 19.13/3.52 % (1986472)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1325057488:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi)
% 19.13/3.52 % (1986467)Instruction limit reached!
% 19.13/3.52 % (1986467)------------------------------
% 19.13/3.52 % (1986467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986467)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986467)Termination reason: Instruction limit
% 19.13/3.52 % (1986467)Termination phase: Saturation
% 19.13/3.52 % (1986467)Time elapsed: 0.184 s
% 19.13/3.52 % (1986467)Peak memory usage: 114 MB
% 19.13/3.52 % (1986467)Instructions burned: 322 (million)
% 19.13/3.52 % (1986465)Instruction limit reached!
% 19.13/3.52 % (1986465)------------------------------
% 19.13/3.52 % (1986465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.13/3.52 % (1986465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.13/3.52 % (1986465)CaDiCaL version: 2.1.3
% 19.13/3.52 % (1986465)Termination reason: Instruction limit
% 19.13/3.52 % (1986465)Termination phase: Saturation
% 19.13/3.52 % (1986465)Time elapsed: 0.215 s
% 21.17/3.92 % (1986465)Peak memory usage: 119 MB
% 21.17/3.92 % (1986465)Instructions burned: 282 (million)
% 21.17/3.92 % (1986474)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2441083668:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi)
% 21.17/3.92 % (1986473)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=3288549318:avsq=on:i=276:avsqr=1,2:rtra=on_2978 on theBenchmark for (2978ds/276Mi)
% 21.17/3.92 % (1986476)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2099181562:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 21.17/3.92 % (1986478)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=116088811:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 21.17/3.92 % (1986474)Instruction limit reached!
% 21.17/3.92 % (1986474)------------------------------
% 21.17/3.92 % (1986474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.17/3.92 % (1986474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.92 % (1986474)CaDiCaL version: 2.1.3
% 21.17/3.92 % (1986474)Termination reason: Instruction limit
% 21.17/3.92 % (1986474)Termination phase: Saturation
% 21.17/3.92 % (1986474)Time elapsed: 0.148 s
% 21.17/3.92 % (1986474)Peak memory usage: 120 MB
% 21.17/3.92 % (1986474)Instructions burned: 378 (million)
% 21.17/3.92 % (1986480)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3162751095:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 21.17/3.92 % (1986468)Instruction limit reached!
% 21.17/3.92 % (1986468)------------------------------
% 21.17/3.92 % (1986468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.17/3.92 % (1986468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.92 % (1986468)CaDiCaL version: 2.1.3
% 21.17/3.92 % (1986468)Termination reason: Instruction limit
% 21.17/3.92 % (1986468)Termination phase: Saturation
% 21.17/3.92 % (1986468)Time elapsed: 0.296 s
% 21.17/3.92 % (1986468)Peak memory usage: 120 MB
% 21.17/3.92 % (1986468)Instructions burned: 417 (million)
% 21.17/3.92 % (1986473)Instruction limit reached!
% 21.17/3.92 % (1986473)------------------------------
% 21.17/3.92 % (1986473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.17/3.92 % (1986473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.92 % (1986473)CaDiCaL version: 2.1.3
% 21.17/3.92 % (1986473)Termination reason: Instruction limit
% 21.17/3.92 % (1986473)Termination phase: Saturation
% 21.17/3.92 % (1986473)Time elapsed: 0.187 s
% 21.17/3.92 % (1986473)Peak memory usage: 136 MB
% 21.17/3.92 % (1986473)Instructions burned: 277 (million)
% 21.17/3.92 % (1986472)Instruction limit reached!
% 21.17/3.92 % (1986472)------------------------------
% 21.17/3.92 % (1986472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.17/3.92 % (1986472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.92 % (1986472)CaDiCaL version: 2.1.3
% 21.17/3.92 % (1986472)Termination reason: Instruction limit
% 21.17/3.92 % (1986472)Termination phase: Saturation
% 21.17/3.92 % (1986472)Time elapsed: 0.292 s
% 21.17/3.92 % (1986472)Peak memory usage: 120 MB
% 21.17/3.92 % (1986472)Instructions burned: 471 (million)
% 21.17/3.92 % (1986484)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1073728424:i=359:rtra=on:gtg=exists_top:ss=axioms_2975 on theBenchmark for (2975ds/359Mi)
% 21.17/3.92 % (1986484)Refutation not found, incomplete strategy
% 21.17/3.92 % (1986484)------------------------------
% 21.17/3.92 % (1986484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.17/3.92 % (1986484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.92 % (1986484)CaDiCaL version: 2.1.3
% 21.17/3.92 % (1986484)Termination reason: Refutation not found, incomplete strategy
% 21.17/3.92 % (1986484)Time elapsed: 0.002 s
% 21.17/3.92 % (1986484)Peak memory usage: 89 MB
% 21.17/3.92 % (1986484)Instructions burned: 4 (million)
% 21.17/3.92 % (1986486)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=3551515028:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi)
% 21.17/3.92 % (1986487)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1853576803:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 26.39/4.44 % (1986476)Instruction limit reached!
% 26.39/4.44 % (1986476)------------------------------
% 26.39/4.44 % (1986476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986476)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986476)Termination reason: Instruction limit
% 26.39/4.44 % (1986476)Termination phase: Saturation
% 26.39/4.44 % (1986476)Time elapsed: 0.296 s
% 26.39/4.44 % (1986476)Peak memory usage: 120 MB
% 26.39/4.44 % (1986476)Instructions burned: 387 (million)
% 26.39/4.44 % (1986484)------------------------------
% 26.39/4.44 % (1986484)------------------------------
% 26.39/4.44 % (1986488)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=134395064:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi)
% 26.39/4.44 % (1986480)Instruction limit reached!
% 26.39/4.44 % (1986480)------------------------------
% 26.39/4.44 % (1986480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986480)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986480)Termination reason: Instruction limit
% 26.39/4.44 % (1986480)Termination phase: Saturation
% 26.39/4.44 % (1986480)Time elapsed: 0.282 s
% 26.39/4.44 % (1986480)Peak memory usage: 136 MB
% 26.39/4.44 % (1986480)Instructions burned: 335 (million)
% 26.39/4.44 % (1986478)Instruction limit reached!
% 26.39/4.44 % (1986478)------------------------------
% 26.39/4.44 % (1986478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986478)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986478)Termination reason: Instruction limit
% 26.39/4.44 % (1986478)Termination phase: Saturation
% 26.39/4.44 % (1986478)Time elapsed: 0.327 s
% 26.39/4.44 % (1986478)Peak memory usage: 92 MB
% 26.39/4.44 % (1986478)Instructions burned: 514 (million)
% 26.39/4.44 % (1986487)Instruction limit reached!
% 26.39/4.44 % (1986487)------------------------------
% 26.39/4.44 % (1986487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986487)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986487)Termination reason: Instruction limit
% 26.39/4.44 % (1986487)Termination phase: Saturation
% 26.39/4.44 % (1986487)Time elapsed: 0.155 s
% 26.39/4.44 % (1986487)Peak memory usage: 118 MB
% 26.39/4.44 % (1986487)Instructions burned: 264 (million)
% 26.39/4.44 % (1986492)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3298861883:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2973 on theBenchmark for (2973ds/273Mi)
% 26.39/4.44 % (1986494)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1128538181:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi)
% 26.39/4.44 % (1986494)Instruction limit reached!
% 26.39/4.44 % (1986494)------------------------------
% 26.39/4.44 % (1986494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986494)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986494)Termination reason: Instruction limit
% 26.39/4.44 % (1986494)Termination phase: Saturation
% 26.39/4.44 % (1986494)Time elapsed: 0.052 s
% 26.39/4.44 % (1986494)Peak memory usage: 90 MB
% 26.39/4.44 % (1986494)Instructions burned: 148 (million)
% 26.39/4.44 % (1986486)Instruction limit reached!
% 26.39/4.44 % (1986486)------------------------------
% 26.39/4.44 % (1986486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.39/4.44 % (1986486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/4.44 % (1986486)CaDiCaL version: 2.1.3
% 26.39/4.44 % (1986486)Termination reason: Instruction limit
% 26.39/4.44 % (1986486)Termination phase: Saturation
% 26.39/4.44 % (1986486)Time elapsed: 0.249 s
% 26.39/4.44 % (1986486)Peak memory usage: 119 MB
% 26.39/4.44 % (1986486)Instructions burned: 341 (million)
% 26.39/4.44 % (1986495)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1651727964:i=4428:doe=on:fsr=off:rtra=on_2972 on theBenchmark for (2972ds/4428Mi)
% 29.07/4.96 % (1986496)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=2131404553:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi)
% 29.07/4.96 % (1986488)Instruction limit reached!
% 29.07/4.96 % (1986488)------------------------------
% 29.07/4.96 % (1986488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1986488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1986488)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1986488)Termination reason: Instruction limit
% 29.07/4.96 % (1986488)Termination phase: Saturation
% 29.07/4.96 % (1986488)Time elapsed: 0.189 s
% 29.07/4.96 % (1986488)Peak memory usage: 119 MB
% 29.07/4.96 % (1986488)Instructions burned: 236 (million)
% 29.07/4.96 % (1986497)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2145973280:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 29.07/4.96 % (1986500)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1981810803:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2971 on theBenchmark for (2971ds/655Mi)
% 29.07/4.96 % (1986492)Instruction limit reached!
% 29.07/4.96 % (1986492)------------------------------
% 29.07/4.96 % (1986492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1986492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1986492)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1986492)Termination reason: Instruction limit
% 29.07/4.96 % (1986492)Termination phase: Saturation
% 29.07/4.96 % (1986492)Time elapsed: 0.201 s
% 29.07/4.96 % (1986492)Peak memory usage: 92 MB
% 29.07/4.96 % (1986492)Instructions burned: 273 (million)
% 29.07/4.96 % (1986503)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=41715868:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi)
% 29.07/4.96 % (1986504)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=622469406:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 29.07/4.96 % (1986504)Refutation not found, incomplete strategy
% 29.07/4.96 % (1986504)------------------------------
% 29.07/4.96 % (1986504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1986504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1986504)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1986504)Termination reason: Refutation not found, incomplete strategy
% 29.07/4.96 % (1986504)Time elapsed: 0.034 s
% 29.07/4.96 % (1986504)Peak memory usage: 117 MB
% 29.07/4.96 % (1986504)Instructions burned: 14 (million)
% 29.07/4.96 % (1986496)Instruction limit reached!
% 29.07/4.96 % (1986496)------------------------------
% 29.07/4.96 % (1986496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1986496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1986496)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1986496)Termination reason: Instruction limit
% 29.07/4.96 % (1986496)Termination phase: Saturation
% 29.07/4.96 % (1986496)Time elapsed: 0.239 s
% 29.07/4.96 % (1986496)Peak memory usage: 136 MB
% 29.07/4.96 % (1986496)Instructions burned: 276 (million)
% 29.07/4.96 % (1986507)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3001962868:s2a=on:i=450:doe=on:nm=32:rtra=on_2970 on theBenchmark for (2970ds/450Mi)
% 29.07/4.96 % (1986500)Instruction limit reached!
% 29.07/4.96 % (1986500)------------------------------
% 29.07/4.96 % (1986500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.07/4.96 % (1986500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.07/4.96 % (1986500)CaDiCaL version: 2.1.3
% 29.07/4.96 % (1986500)Termination reason: Instruction limit
% 29.07/4.96 % (1986500)Termination phase: Saturation
% 29.07/4.96 % (1986500)Time elapsed: 0.224 s
% 29.07/4.96 % (1986500)Peak memory usage: 93 MB
% 29.07/4.96 % (1986500)Instructions burned: 658 (million)
% 29.07/4.96 % (1986510)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
% 29.07/4.96 % (1986510)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3745256182:i=1090:aac=none:nm=0:rtra=on:rawr=on_2968 on theBenchmark for (2968ds/1090Mi)
% 32.52/5.31 % (1986504)------------------------------
% 32.52/5.31 % (1986504)------------------------------
% 32.52/5.31 % (1986512)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3460212140:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi)
% 32.52/5.31 % (1986512)Instruction limit reached!
% 32.52/5.31 % (1986512)------------------------------
% 32.52/5.31 % (1986512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986512)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986512)Termination reason: Instruction limit
% 32.52/5.31 % (1986512)Termination phase: Saturation
% 32.52/5.31 % (1986512)Time elapsed: 0.054 s
% 32.52/5.31 % (1986512)Peak memory usage: 118 MB
% 32.52/5.31 % (1986512)Instructions burned: 131 (million)
% 32.52/5.31 % (1986515)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=220794224:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi)
% 32.52/5.31 % (1986507)Instruction limit reached!
% 32.52/5.31 % (1986507)------------------------------
% 32.52/5.31 % (1986507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986507)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986507)Termination reason: Instruction limit
% 32.52/5.31 % (1986507)Termination phase: Saturation
% 32.52/5.31 % (1986507)Time elapsed: 0.366 s
% 32.52/5.31 % (1986507)Peak memory usage: 136 MB
% 32.52/5.31 % (1986507)Instructions burned: 450 (million)
% 32.52/5.31 % (1986516)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3790681734:i=491:doe=on:rtra=on:gtg=position_2966 on theBenchmark for (2966ds/491Mi)
% 32.52/5.31 % (1986497)Instruction limit reached!
% 32.52/5.31 % (1986497)------------------------------
% 32.52/5.31 % (1986497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986497)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986497)Termination reason: Instruction limit
% 32.52/5.31 % (1986497)Termination phase: Saturation
% 32.52/5.31 % (1986497)Time elapsed: 0.695 s
% 32.52/5.31 % (1986497)Peak memory usage: 94 MB
% 32.52/5.31 % (1986497)Instructions burned: 1052 (million)
% 32.52/5.31 % (1986503)Instruction limit reached!
% 32.52/5.31 % (1986503)------------------------------
% 32.52/5.31 % (1986503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986503)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986503)Termination reason: Instruction limit
% 32.52/5.31 % (1986503)Termination phase: Saturation
% 32.52/5.31 % (1986503)Time elapsed: 0.627 s
% 32.52/5.31 % (1986503)Peak memory usage: 91 MB
% 32.52/5.31 % (1986503)Instructions burned: 1054 (million)
% 32.52/5.31 % (1986519)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=4259652637:s2a=on:i=835:s2at=2:rtra=on_2964 on theBenchmark for (2964ds/835Mi)
% 32.52/5.31 % (1986515)Instruction limit reached!
% 32.52/5.31 % (1986515)------------------------------
% 32.52/5.31 % (1986515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986515)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986515)Termination reason: Instruction limit
% 32.52/5.31 % (1986515)Termination phase: Saturation
% 32.52/5.31 % (1986515)Time elapsed: 0.216 s
% 32.52/5.31 % (1986515)Peak memory usage: 120 MB
% 32.52/5.31 % (1986515)Instructions burned: 312 (million)
% 32.52/5.31 % (1986516)Instruction limit reached!
% 32.52/5.31 % (1986516)------------------------------
% 32.52/5.31 % (1986516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.31 % (1986516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.31 % (1986516)CaDiCaL version: 2.1.3
% 32.52/5.31 % (1986516)Termination reason: Instruction limit
% 32.52/5.31 % (1986516)Termination phase: Saturation
% 32.52/5.31 % (1986516)Time elapsed: 0.178 s
% 32.52/5.31 % (1986516)Peak memory usage: 93 MB
% 32.52/5.31 % (1986516)Instructions burned: 492 (million)
% 32.52/5.31 % (1986520)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=679248659:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2963 on theBenchmark for (2963ds/307Mi)
% 38.39/6.13 % (1986521)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2405464962:i=776:doe=on:rtra=on_2963 on theBenchmark for (2963ds/776Mi)
% 38.39/6.13 % (1986524)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=1093946352:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2962 on theBenchmark for (2962ds/784Mi)
% 38.39/6.13 % (1986523)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1561153347:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2963 on theBenchmark for (2963ds/646Mi)
% 38.39/6.13 % (1986510)Instruction limit reached!
% 38.39/6.13 % (1986510)------------------------------
% 38.39/6.13 % (1986510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.39/6.13 % (1986510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.39/6.13 % (1986510)CaDiCaL version: 2.1.3
% 38.39/6.13 % (1986510)Termination reason: Instruction limit
% 38.39/6.13 % (1986510)Termination phase: Saturation
% 38.39/6.13 % (1986510)Time elapsed: 0.644 s
% 38.39/6.13 % (1986510)Peak memory usage: 120 MB
% 38.39/6.13 % (1986510)Instructions burned: 1091 (million)
% 38.39/6.13 % (1986520)Instruction limit reached!
% 38.39/6.13 % (1986520)------------------------------
% 38.39/6.13 % (1986520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.39/6.13 % (1986520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.39/6.13 % (1986520)CaDiCaL version: 2.1.3
% 38.39/6.13 % (1986520)Termination reason: Instruction limit
% 38.39/6.13 % (1986520)Termination phase: Saturation
% 38.39/6.13 % (1986520)Time elapsed: 0.192 s
% 38.39/6.13 % (1986520)Peak memory usage: 91 MB
% 38.39/6.13 % (1986520)Instructions burned: 308 (million)
% 38.39/6.13 % (1986529)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=2956885240:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2960 on theBenchmark for (2960ds/1131Mi)
% 38.39/6.13 % (1986530)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=3225161822:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2960 on theBenchmark for (2960ds/246Mi)
% 38.39/6.13 % (1986524)Instruction limit reached!
% 38.39/6.13 % (1986524)------------------------------
% 38.39/6.13 % (1986524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.39/6.13 % (1986524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.39/6.13 % (1986524)CaDiCaL version: 2.1.3
% 38.39/6.13 % (1986524)Termination reason: Instruction limit
% 38.39/6.13 % (1986524)Termination phase: Saturation
% 38.39/6.13 % (1986524)Time elapsed: 0.319 s
% 38.39/6.13 % (1986524)Peak memory usage: 123 MB
% 38.39/6.13 % (1986524)Instructions burned: 786 (million)
% 38.39/6.13 % (1986519)Instruction limit reached!
% 38.39/6.13 % (1986519)------------------------------
% 38.39/6.13 % (1986519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.39/6.13 % (1986519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.39/6.13 % (1986519)CaDiCaL version: 2.1.3
% 38.39/6.13 % (1986519)Termination reason: Instruction limit
% 38.39/6.13 % (1986519)Termination phase: Saturation
% 38.39/6.13 % (1986519)Time elapsed: 0.473 s
% 38.39/6.13 % (1986519)Peak memory usage: 94 MB
% 38.39/6.13 % (1986519)Instructions burned: 835 (million)
% 38.39/6.13 % (1986521)Instruction limit reached!
% 38.39/6.13 % (1986521)------------------------------
% 38.39/6.13 % (1986521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.39/6.13 % (1986521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.39/6.13 % (1986521)CaDiCaL version: 2.1.3
% 38.39/6.13 % (1986521)Termination reason: Instruction limit
% 38.39/6.13 % (1986521)Termination phase: Saturation
% 38.39/6.13 % (1986521)Time elapsed: 0.389 s
% 38.39/6.13 % (1986521)Peak memory usage: 119 MB
% 38.39/6.13 % (1986521)Instructions burned: 777 (million)
% 38.39/6.13 % (1986533)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1698220464:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2958 on theBenchmark for (2958ds/775Mi)
% 38.39/6.13 % (1986534)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=24187440:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi)
% 52.56/8.10 % (1986530)Instruction limit reached!
% 52.56/8.10 % (1986530)------------------------------
% 52.56/8.10 % (1986530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986530)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986530)Termination reason: Instruction limit
% 52.56/8.10 % (1986530)Termination phase: Saturation
% 52.56/8.10 % (1986530)Time elapsed: 0.194 s
% 52.56/8.10 % (1986530)Peak memory usage: 119 MB
% 52.56/8.10 % (1986530)Instructions burned: 247 (million)
% 52.56/8.10 % (1986523)Instruction limit reached!
% 52.56/8.10 % (1986523)------------------------------
% 52.56/8.10 % (1986523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986523)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986523)Termination reason: Instruction limit
% 52.56/8.10 % (1986523)Termination phase: Saturation
% 52.56/8.10 % (1986523)Time elapsed: 0.493 s
% 52.56/8.10 % (1986523)Peak memory usage: 138 MB
% 52.56/8.10 % (1986523)Instructions burned: 646 (million)
% 52.56/8.10 % (1986535)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3476180291:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi)
% 52.56/8.10 % (1986535)Instruction limit reached!
% 52.56/8.10 % (1986535)------------------------------
% 52.56/8.10 % (1986535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986535)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986535)Termination reason: Instruction limit
% 52.56/8.10 % (1986535)Termination phase: Saturation
% 52.56/8.10 % (1986535)Time elapsed: 0.068 s
% 52.56/8.10 % (1986535)Peak memory usage: 89 MB
% 52.56/8.10 % (1986535)Instructions burned: 103 (million)
% 52.56/8.10 % (1986538)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3793635976:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2956 on theBenchmark for (2956ds/1094Mi)
% 52.56/8.10 % (1986534)Instruction limit reached!
% 52.56/8.10 % (1986534)------------------------------
% 52.56/8.10 % (1986534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986534)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986534)Termination reason: Instruction limit
% 52.56/8.10 % (1986534)Termination phase: Saturation
% 52.56/8.10 % (1986534)Time elapsed: 0.197 s
% 52.56/8.10 % (1986534)Peak memory usage: 93 MB
% 52.56/8.10 % (1986534)Instructions burned: 274 (million)
% 52.56/8.10 % (1986540)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=121209718:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi)
% 52.56/8.10 % (1986533)Instruction limit reached!
% 52.56/8.10 % (1986533)------------------------------
% 52.56/8.10 % (1986533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986533)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986533)Termination reason: Instruction limit
% 52.56/8.10 % (1986533)Termination phase: Saturation
% 52.56/8.10 % (1986533)Time elapsed: 0.279 s
% 52.56/8.10 % (1986533)Peak memory usage: 95 MB
% 52.56/8.10 % (1986533)Instructions burned: 776 (million)
% 52.56/8.10 % (1986541)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=183300515:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/868Mi)
% 52.56/8.10 % (1986544)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=3365152905:i=1846:canc=cautious:fsr=off:rtra=on_2954 on theBenchmark for (2954ds/1846Mi)
% 52.56/8.10 % (1986544)Refutation not found, incomplete strategy
% 52.56/8.10 % (1986544)------------------------------
% 52.56/8.10 % (1986544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.56/8.10 % (1986544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.56/8.10 % (1986544)CaDiCaL version: 2.1.3
% 52.56/8.10 % (1986544)Termination reason: Refutation not found, incomplete strategy
% 52.56/8.10 % (1986544)Time elapsed: 0.004 s
% 52.56/8.10 % (1986544)Peak memory usage: 89 MB
% 64.28/9.99 % (1986544)Instructions burned: 4 (million)
% 64.28/9.99 % (1986545)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3041612416:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2954 on theBenchmark for (2954ds/36816Mi)
% 64.28/9.99 % (1986529)Instruction limit reached!
% 64.28/9.99 % (1986529)------------------------------
% 64.28/9.99 % (1986529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.28/9.99 % (1986529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.28/9.99 % (1986529)CaDiCaL version: 2.1.3
% 64.28/9.99 % (1986529)Termination reason: Instruction limit
% 64.28/9.99 % (1986529)Termination phase: Saturation
% 64.28/9.99 % (1986529)Time elapsed: 0.720 s
% 64.28/9.99 % (1986529)Peak memory usage: 122 MB
% 64.28/9.99 % (1986529)Instructions burned: 1132 (million)
% 64.28/9.99 % (1986544)------------------------------
% 64.28/9.99 % (1986544)------------------------------
% 64.28/9.99 % (1986538)Instruction limit reached!
% 64.28/9.99 % (1986538)------------------------------
% 64.28/9.99 % (1986538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.28/9.99 % (1986538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.28/9.99 % (1986538)CaDiCaL version: 2.1.3
% 64.28/9.99 % (1986538)Termination reason: Instruction limit
% 64.28/9.99 % (1986538)Termination phase: Saturation
% 64.28/9.99 % (1986538)Time elapsed: 0.480 s
% 64.28/9.99 % (1986538)Peak memory usage: 90 MB
% 64.28/9.99 % (1986538)Instructions burned: 1096 (million)
% 64.28/9.99 % (1986549)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3890092188:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2952 on theBenchmark for (2952ds/273Mi)
% 64.28/9.99 % (1986550)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=2696753868:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/863Mi)
% 64.28/9.99 % (1986551)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3306568342:i=5811:kws=precedence:nm=0:rtra=on_2950 on theBenchmark for (2950ds/5811Mi)
% 64.28/9.99 % (1986541)Instruction limit reached!
% 64.28/9.99 % (1986541)------------------------------
% 64.28/9.99 % (1986541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.28/9.99 % (1986541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.28/9.99 % (1986541)CaDiCaL version: 2.1.3
% 64.28/9.99 % (1986541)Termination reason: Instruction limit
% 64.28/9.99 % (1986541)Termination phase: Saturation
% 64.28/9.99 % (1986541)Time elapsed: 0.519 s
% 64.28/9.99 % (1986541)Peak memory usage: 120 MB
% 64.28/9.99 % (1986541)Instructions burned: 869 (million)
% 64.28/9.99 % (1986549)Instruction limit reached!
% 64.28/9.99 % (1986549)------------------------------
% 64.28/9.99 % (1986549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.28/9.99 % (1986549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.28/9.99 % (1986549)CaDiCaL version: 2.1.3
% 64.28/9.99 % (1986549)Termination reason: Instruction limit
% 64.28/9.99 % (1986549)Termination phase: Saturation
% 64.28/9.99 % (1986549)Time elapsed: 0.195 s
% 64.28/9.99 % (1986549)Peak memory usage: 92 MB
% 64.28/9.99 % (1986549)Instructions burned: 273 (million)
% 64.28/9.99 % (1986555)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=4080822416:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2948 on theBenchmark for (2948ds/2216Mi)
% 64.28/9.99 % (1986495)Instruction limit reached!
% 64.28/9.99 % (1986495)------------------------------
% 64.28/9.99 % (1986495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.28/9.99 % (1986495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.28/9.99 % (1986495)CaDiCaL version: 2.1.3
% 64.28/9.99 % (1986495)Termination reason: Instruction limit
% 64.28/9.99 % (1986495)Termination phase: Saturation
% 64.28/9.99 % (1986495)Time elapsed: 2.432 s
% 64.28/9.99 % (1986495)Peak memory usage: 111 MB
% 64.28/9.99 % (1986495)Instructions burned: 4428 (million)
% 64.28/9.99 % (1986556)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3779982035:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2948 on theBenchmark for (2948ds/801Mi)
% 64.28/9.99 % (1986558)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3275753528:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2947 on theBenchmark for (2947ds/1026Mi)
% 99.29/14.75 % (1986550)Instruction limit reached!
% 99.29/14.75 % (1986550)------------------------------
% 99.29/14.75 % (1986550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986550)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986550)Termination reason: Instruction limit
% 99.29/14.75 % (1986550)Termination phase: Saturation
% 99.29/14.75 % (1986550)Time elapsed: 0.522 s
% 99.29/14.75 % (1986550)Peak memory usage: 120 MB
% 99.29/14.75 % (1986550)Instructions burned: 863 (million)
% 99.29/14.75 % (1986561)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=442547876:i=3509:rtra=on_2944 on theBenchmark for (2944ds/3509Mi)
% 99.29/14.75 % (1986556)Instruction limit reached!
% 99.29/14.75 % (1986556)------------------------------
% 99.29/14.75 % (1986556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986556)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986556)Termination reason: Instruction limit
% 99.29/14.75 % (1986556)Termination phase: Saturation
% 99.29/14.75 % (1986556)Time elapsed: 0.569 s
% 99.29/14.75 % (1986556)Peak memory usage: 95 MB
% 99.29/14.75 % (1986556)Instructions burned: 801 (million)
% 99.29/14.75 % (1986563)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1570250090:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/2127Mi)
% 99.29/14.75 % (1986558)Instruction limit reached!
% 99.29/14.75 % (1986558)------------------------------
% 99.29/14.75 % (1986558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986558)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986558)Termination reason: Instruction limit
% 99.29/14.75 % (1986558)Termination phase: Saturation
% 99.29/14.75 % (1986558)Time elapsed: 0.577 s
% 99.29/14.75 % (1986558)Peak memory usage: 91 MB
% 99.29/14.75 % (1986558)Instructions burned: 1027 (million)
% 99.29/14.75 % (1986565)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3404256540:i=1959:rtra=on:fsd=on:proc=on_2939 on theBenchmark for (2939ds/1959Mi)
% 99.29/14.75 % (1986555)Instruction limit reached!
% 99.29/14.75 % (1986555)------------------------------
% 99.29/14.75 % (1986555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986555)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986555)Termination reason: Instruction limit
% 99.29/14.75 % (1986555)Termination phase: Saturation
% 99.29/14.75 % (1986555)Time elapsed: 1.360 s
% 99.29/14.75 % (1986555)Peak memory usage: 123 MB
% 99.29/14.75 % (1986555)Instructions burned: 2217 (million)
% 99.29/14.75 % (1986567)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3859484467:s2a=on:i=3553:nm=0:rtra=on_2933 on theBenchmark for (2933ds/3553Mi)
% 99.29/14.75 % (1986563)Instruction limit reached!
% 99.29/14.75 % (1986563)------------------------------
% 99.29/14.75 % (1986563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986563)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986563)Termination reason: Instruction limit
% 99.29/14.75 % (1986563)Termination phase: Saturation
% 99.29/14.75 % (1986563)Time elapsed: 1.026 s
% 99.29/14.75 % (1986563)Peak memory usage: 90 MB
% 99.29/14.75 % (1986563)Instructions burned: 2128 (million)
% 99.29/14.75 % (1986569)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2761956381:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2929 on theBenchmark for (2929ds/3201Mi)
% 99.29/14.75 % (1986561)Instruction limit reached!
% 99.29/14.75 % (1986561)------------------------------
% 99.29/14.75 % (1986561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.29/14.75 % (1986561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.29/14.75 % (1986561)CaDiCaL version: 2.1.3
% 99.29/14.75 % (1986561)Termination reason: Instruction limit
% 99.29/14.75 % (1986561)Termination phase: Saturation
% 99.29/14.75 % (1986561)Time elapsed: 1.535 s
% 99.29/14.75 % (1986561)Peak memory usage: 106 MB
% 99.29/14.75 % (1986561)Instructions burned: 3510 (million)
% 99.29/14.75 % (1986571)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=575872360:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2927 on theBenchmark for (2927ds/4093Mi)
% 109.89/16.17 % (1986565)Instruction limit reached!
% 109.89/16.17 % (1986565)------------------------------
% 109.89/16.17 % (1986565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986565)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986565)Termination reason: Instruction limit
% 109.89/16.17 % (1986565)Termination phase: Saturation
% 109.89/16.17 % (1986565)Time elapsed: 1.257 s
% 109.89/16.17 % (1986565)Peak memory usage: 125 MB
% 109.89/16.17 % (1986565)Instructions burned: 1959 (million)
% 109.89/16.17 % (1986573)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=1499883829:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2925 on theBenchmark for (2925ds/21173Mi)
% 109.89/16.17 % (1986540)Instruction limit reached!
% 109.89/16.17 % (1986540)------------------------------
% 109.89/16.17 % (1986540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986540)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986540)Termination reason: Instruction limit
% 109.89/16.17 % (1986540)Termination phase: Saturation
% 109.89/16.17 % (1986540)Time elapsed: 3.518 s
% 109.89/16.17 % (1986540)Peak memory usage: 119 MB
% 109.89/16.17 % (1986540)Instructions burned: 6401 (million)
% 109.89/16.17 % (1986575)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=770927825:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2919 on theBenchmark for (2919ds/10544Mi)
% 109.89/16.17 % (1986551)Instruction limit reached!
% 109.89/16.17 % (1986551)------------------------------
% 109.89/16.17 % (1986551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986551)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986551)Termination reason: Instruction limit
% 109.89/16.17 % (1986551)Termination phase: Saturation
% 109.89/16.17 % (1986551)Time elapsed: 3.279 s
% 109.89/16.17 % (1986551)Peak memory usage: 134 MB
% 109.89/16.17 % (1986551)Instructions burned: 5812 (million)
% 109.89/16.17 % (1986577)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2151817824:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2916 on theBenchmark for (2916ds/1262Mi)
% 109.89/16.17 % (1986569)Instruction limit reached!
% 109.89/16.17 % (1986569)------------------------------
% 109.89/16.17 % (1986569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986569)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986569)Termination reason: Instruction limit
% 109.89/16.17 % (1986569)Termination phase: Saturation
% 109.89/16.17 % (1986569)Time elapsed: 1.514 s
% 109.89/16.17 % (1986569)Peak memory usage: 92 MB
% 109.89/16.17 % (1986569)Instructions burned: 3203 (million)
% 109.89/16.17 % (1986579)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=432776530:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2912 on theBenchmark for (2912ds/775Mi)
% 109.89/16.17 % (1986567)Instruction limit reached!
% 109.89/16.17 % (1986567)------------------------------
% 109.89/16.17 % (1986567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986567)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986567)Termination reason: Instruction limit
% 109.89/16.17 % (1986567)Termination phase: Saturation
% 109.89/16.17 % (1986567)Time elapsed: 2.229 s
% 109.89/16.17 % (1986567)Peak memory usage: 110 MB
% 109.89/16.17 % (1986567)Instructions burned: 3554 (million)
% 109.89/16.17 % (1986581)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=709281673:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2909 on theBenchmark for (2909ds/270Mi)
% 109.89/16.17 % (1986577)Instruction limit reached!
% 109.89/16.17 % (1986577)------------------------------
% 109.89/16.17 % (1986577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986577)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986577)Termination reason: Instruction limit
% 109.89/16.17 % (1986577)Termination phase: Saturation
% 109.89/16.17 % (1986577)Time elapsed: 0.778 s
% 109.89/16.17 % (1986577)Peak memory usage: 122 MB
% 109.89/16.17 % (1986577)Instructions burned: 1263 (million)
% 109.89/16.17 % (1986581)Instruction limit reached!
% 109.89/16.17 % (1986581)------------------------------
% 109.89/16.17 % (1986581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986581)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986581)Termination reason: Instruction limit
% 109.89/16.17 % (1986581)Termination phase: Saturation
% 109.89/16.17 % (1986581)Time elapsed: 0.190 s
% 109.89/16.17 % (1986581)Peak memory usage: 92 MB
% 109.89/16.17 % (1986581)Instructions burned: 270 (million)
% 109.89/16.17 % (1986579)Instruction limit reached!
% 109.89/16.17 % (1986579)------------------------------
% 109.89/16.17 % (1986579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986579)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986579)Termination reason: Instruction limit
% 109.89/16.17 % (1986579)Termination phase: Saturation
% 109.89/16.17 % (1986579)Time elapsed: 0.505 s
% 109.89/16.17 % (1986579)Peak memory usage: 95 MB
% 109.89/16.17 % (1986579)Instructions burned: 775 (million)
% 109.89/16.17 % (1986583)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1427826323:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2906 on theBenchmark for (2906ds/17165Mi)
% 109.89/16.17 % (1986584)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2362511440:s2a=on:i=13094:s2at=-1:rtra=on_2906 on theBenchmark for (2906ds/13094Mi)
% 109.89/16.17 % (1986571)Instruction limit reached!
% 109.89/16.17 % (1986571)------------------------------
% 109.89/16.17 % (1986571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986571)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986571)Termination reason: Instruction limit
% 109.89/16.17 % (1986571)Termination phase: Saturation
% 109.89/16.17 % (1986571)Time elapsed: 2.125 s
% 109.89/16.17 % (1986571)Peak memory usage: 141 MB
% 109.89/16.17 % (1986571)Instructions burned: 4095 (million)
% 109.89/16.17 % (1986585)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=527511498:st=2:i=12633:rtra=on:ss=axioms_2905 on theBenchmark for (2905ds/12633Mi)
% 109.89/16.17 % (1986588)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=2745637860:i=1783:rtra=on:gtg=position_2904 on theBenchmark for (2904ds/1783Mi)
% 109.89/16.17 % (1986588)Instruction limit reached!
% 109.89/16.17 % (1986588)------------------------------
% 109.89/16.17 % (1986588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986588)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986588)Termination reason: Instruction limit
% 109.89/16.17 % (1986588)Termination phase: Saturation
% 109.89/16.17 % (1986588)Time elapsed: 1.038 s
% 109.89/16.17 % (1986588)Peak memory usage: 124 MB
% 109.89/16.17 % (1986588)Instructions burned: 1784 (million)
% 109.89/16.17 % (1986591)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=2742479980:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2892 on theBenchmark for (2892ds/5451Mi)
% 109.89/16.17 % (1986591)Instruction limit reached!
% 109.89/16.17 % (1986591)------------------------------
% 109.89/16.17 % (1986591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986591)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986591)Termination reason: Instruction limit
% 109.89/16.17 % (1986591)Termination phase: Saturation
% 109.89/16.17 % (1986591)Time elapsed: 2.471 s
% 109.89/16.17 % (1986591)Peak memory usage: 120 MB
% 109.89/16.17 % (1986591)Instructions burned: 5452 (million)
% 109.89/16.17 % (1986624)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=2804163806:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2865 on theBenchmark for (2865ds/4975Mi)
% 109.89/16.17 % (1986545)Instruction limit reached!
% 109.89/16.17 % (1986545)------------------------------
% 109.89/16.17 % (1986545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986545)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986545)Termination reason: Instruction limit
% 109.89/16.17 % (1986545)Termination phase: Saturation
% 109.89/16.17 % (1986545)Time elapsed: 9.412 s
% 109.89/16.17 % (1986545)Peak memory usage: 101 MB
% 109.89/16.17 % (1986545)Instructions burned: 36819 (million)
% 109.89/16.17 % (1986745)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=2631907675:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2859 on theBenchmark for (2859ds/2076Mi)
% 109.89/16.17 % (1986575)Instruction limit reached!
% 109.89/16.17 % (1986575)------------------------------
% 109.89/16.17 % (1986575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986575)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986575)Termination reason: Instruction limit
% 109.89/16.17 % (1986575)Termination phase: Saturation
% 109.89/16.17 % (1986575)Time elapsed: 6.343 s
% 109.89/16.17 % (1986575)Peak memory usage: 202 MB
% 109.89/16.17 % (1986575)Instructions burned: 10545 (million)
% 109.89/16.17 % (1986867)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=8888608:i=5145:rtra=on_2854 on theBenchmark for (2854ds/5145Mi)
% 109.89/16.17 % (1986745)Instruction limit reached!
% 109.89/16.17 % (1986745)------------------------------
% 109.89/16.17 % (1986745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986745)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986745)Termination reason: Instruction limit
% 109.89/16.17 % (1986745)Termination phase: Saturation
% 109.89/16.17 % (1986745)Time elapsed: 0.707 s
% 109.89/16.17 % (1986745)Peak memory usage: 122 MB
% 109.89/16.17 % (1986745)Instructions burned: 2077 (million)
% 109.89/16.17 % (1986974)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3905436252:i=3509:rtra=on_2850 on theBenchmark for (2850ds/3509Mi)
% 109.89/16.17 % (1986585)Instruction limit reached!
% 109.89/16.17 % (1986585)------------------------------
% 109.89/16.17 % (1986585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.89/16.17 % (1986585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.89/16.17 % (1986585)CaDiCaL version: 2.1.3
% 109.89/16.17 % (1986585)Termination reason: Instruction limit
% 109.89/16.17 % (1986585)Termination phase: Saturation
% 109.89/16.17 % (1986585)Time elapsed: 5.471 s
% 109.89/16.17 % (1986585)Peak memory usage: 133 MB
% 109.89/16.17 % (1986585)Instructions burned: 12633 (million)
% 109.89/16.17 % (1986974)First to succeed.
% 109.89/16.17 % (1986974)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1986311"
% 109.89/16.17 % (1987019)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2116841093:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2849 on theBenchmark for (2849ds/13800Mi)
% 109.89/16.17 % (1986974)Refutation found. Thanks to Tanya!
% 109.89/16.17 % SZS status Theorem for theBenchmark
% 109.89/16.17 % SZS output start Proof for theBenchmark
% See solution above
% 110.37/16.38 % (1986974)------------------------------
% 110.37/16.38 % (1986974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.37/16.38 % (1986974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.37/16.38 % (1986974)CaDiCaL version: 2.1.3
% 110.37/16.38 % (1986974)Termination reason: Refutation
% 110.37/16.38 % (1986974)Time elapsed: 0.154 s
% 110.37/16.38 % (1986974)Peak memory usage: 94 MB
% 110.37/16.38 % (1986974)Instructions burned: 433 (million)
% 110.37/16.38 % (1986974)------------------------------
% 110.37/16.38 % (1986974)------------------------------
% 110.37/16.38 % (1986311)Success in time 15.51 s
% 110.37/16.38 % Vampire exiting
%------------------------------------------------------------------------------