%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX081_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:50 PM UTC 2026
% Result : Theorem 42.54s 6.44s
% Output : Refutation 43.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 68
% Syntax : Number of formulae : 290 ( 40 unt; 0 typ; 57 def)
% Number of atoms : 983 ( 398 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 1219 ( 526 ~; 525 |; 106 &)
% ( 56 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 434 ( 33 atm; 155 fun; 80 num; 166 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 : 58 ( 54 usr; 48 prp; 0-4 aty)
% Number of functors : 43 ( 36 usr; 21 con; 0-4 aty)
% Number of variables : 450 ( 382 !; 68 ?; 450 :)
% 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_10,type,
sK0: general > $int ).
tff(func_def_11,type,
sK1: ( general * general * general * general ) > general ).
tff(func_def_12,type,
sK2: ( general * general * general * general ) > general ).
tff(func_def_13,type,
sK3: ( general * general * general * general ) > general ).
tff(func_def_14,type,
sK4: ( general * general * general * general ) > general ).
tff(func_def_15,type,
sK5: ( general * general * general * general ) > general ).
tff(func_def_16,type,
sK6: ( general * general * general * general ) > general ).
tff(func_def_17,type,
sK7: ( general * general * general * general ) > general ).
tff(func_def_18,type,
sK8: ( general * general * general * general ) > general ).
tff(func_def_19,type,
sK9: ( general * general * general * general ) > general ).
tff(func_def_20,type,
sK10: ( general * general * general * general ) > general ).
tff(func_def_21,type,
sK11: ( general * general * general * general ) > $int ).
tff(func_def_22,type,
sK12: ( general * general * general * general ) > $int ).
tff(func_def_23,type,
sK13: ( general * general * general * general ) > $int ).
tff(func_def_24,type,
sK14: ( general * general * general * general ) > $int ).
tff(func_def_25,type,
sK15: $int ).
tff(func_def_26,type,
sK16: $int ).
tff(func_def_27,type,
sK17: $int ).
tff(func_def_28,type,
sK18: $int ).
tff(func_def_29,type,
sK19: general > symbol ).
tff(func_def_30,type,
sF20: $int ).
tff(func_def_31,type,
sF21: $int ).
tff(func_def_32,type,
sF22: general ).
tff(func_def_33,type,
sF23: general ).
tff(func_def_34,type,
sF24: general ).
tff(func_def_35,type,
sF25: general ).
tff(func_def_36,type,
sF26: $int ).
tff(func_def_37,type,
sF27: general ).
tff(func_def_38,type,
sF28: $int ).
tff(func_def_39,type,
sF29: general ).
tff(func_def_42,type,
'$inst31': $int ).
tff(func_def_43,type,
'$inst32': $int ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
div: ( general * general * general * general ) > $o ).
tff(f4,axiom,
! [X1: $int,X0: $int] :
( ( X0 = X1 )
<=> ( f__integer__(X0) = f__integer__(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f__integer__def_ax) ).
tff(f6,axiom,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
<=> $lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f8,axiom,
! [X1: general,X2: general,X0: general] :
( ( p__less_equal__(X0,X1)
& p__less_equal__(X1,X2) )
=> p__less_equal__(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitive_ordering_ax) ).
tff(f10,axiom,
! [X1: general,X0: general] :
( ( p__less_equal__(X0,X1)
& ( X0 != X1 ) )
<=> p__less__(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__less__def_ax) ).
tff(f16,axiom,
! [X1: general,X0: general,X2: general,X3: general] :
( div(X0,X1,X2,X3)
<=> ? [X5: general,X7: general,X6: general,X4: general] :
( ? [X9: general,X8: general] :
( ( X9 = X5 )
& ( X8 = X7 )
& p__less__(X8,X9) )
& ( X3 = X7 )
& ( X2 = X6 )
& ( X1 = X5 )
& ? [X8: general,X9: general] :
( ? [X11: $int,X10: $int] :
( ( X9 = f__integer__($sum(X10,X11)) )
& ? [X12: $int,X11: $int] :
( ( X10 = $product(X12,X11) )
& ( f__integer__(X12) = X5 )
& ( f__integer__(X11) = X6 ) )
& ( f__integer__(X11) = X7 ) )
& ( X8 = X9 )
& ( X8 = X4 ) )
& ? [X8: general,X9: general] :
( p__less_equal__(X8,X9)
& ( X9 = X7 )
& ( X8 = f__integer__(0) ) )
& ( X0 = X4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_0_completed_definition_of_div_4) ).
tff(f17,conjecture,
! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ( $less(X3,$difference(X1,1))
& div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_unnamed_formula) ).
tff(f18,negated_conjecture,
~ ! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ( $less(X3,$difference(X1,1))
& div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
tff(f19,plain,
~ ! [X2: $int,X1: $int,X3: $int,X0: $int] :
( ( $less(X3,$sum(X1,$uminus(1)))
& div(f__integer__(X0),f__integer__(X1),f__integer__(X2),f__integer__(X3)) )
=> div(f__integer__($sum(X0,1)),f__integer__(X1),f__integer__(X2),f__integer__($sum(X3,1))) ),
inference(theory_normalization,[],[f18]) ).
tff(f20,plain,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
<=> ~ $less(X1,X0) ),
inference(theory_normalization,[],[f6]) ).
tff(f21,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f22,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) ),
introduced(definition,[],[tha_associativity]) ).
tff(f26,plain,
! [X0: $int] : ~ $less(X0,X0),
introduced(definition,[],[tha_non-reflexivity]) ).
tff(f30,plain,
! [X0: $int,X1: $int] :
( $less(X1,$sum(X0,1))
| $less(X0,X1) ),
introduced(definition,[],[tha_order_plus_one_dichotomy]) ).
tff(f32,plain,
! [X0: $int,X1: $int] : ( $product(X0,X1) = $product(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f39,plain,
! [X0: $int,X1: $int] :
( ( X0 = X1 )
<=> ( f__integer__(X0) = f__integer__(X1) ) ),
inference(rectify,[],[f4]) ).
tff(f43,plain,
! [X1: general,X2: general,X0: general] :
( ( p__less_equal__(X0,X1)
& p__less_equal__(X2,X0) )
=> p__less_equal__(X2,X1) ),
inference(rectify,[],[f8]) ).
tff(f44,plain,
! [X1: general,X2: general,X0: general,X3: general] :
( ? [X5: general,X7: general,X6: general,X4: general] :
( ? [X16: general,X17: general] :
( ( f__integer__(0) = X16 )
& ( X5 = X17 )
& p__less_equal__(X16,X17) )
& ( X1 = X7 )
& ( X3 = X5 )
& ( X2 = X6 )
& ? [X9: general,X8: general] :
( ( X4 = X8 )
& p__less__(X9,X8)
& ( X5 = X9 ) )
& ( X0 = X4 )
& ? [X10: general,X11: general] :
( ? [X13: $int,X12: $int] :
( ( f__integer__(X12) = X5 )
& ? [X15: $int,X14: $int] :
( ( f__integer__(X14) = X4 )
& ( $product(X14,X15) = X13 )
& ( f__integer__(X15) = X6 ) )
& ( f__integer__($sum(X13,X12)) = X11 ) )
& ( X10 = X11 )
& ( X7 = X10 ) ) )
<=> div(X1,X0,X2,X3) ),
inference(rectify,[],[f16]) ).
tff(f45,plain,
~ ! [X2: $int,X1: $int,X0: $int,X3: $int] :
( ( $less(X2,$sum(X1,$uminus(1)))
& div(f__integer__(X3),f__integer__(X1),f__integer__(X0),f__integer__(X2)) )
=> div(f__integer__($sum(X3,1)),f__integer__(X1),f__integer__(X0),f__integer__($sum(X2,1))) ),
inference(rectify,[],[f19]) ).
tff(f46,plain,
! [X1: $int,X0: $int] :
( p__less_equal__(f__integer__(X1),f__integer__(X0))
<=> ~ $less(X0,X1) ),
inference(rectify,[],[f20]) ).
tff(f48,plain,
! [X0: general,X1: general] :
( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
<=> p__less__(X1,X0) ),
inference(rectify,[],[f10]) ).
tff(f54,plain,
! [X1: general,X2: general,X0: general] :
( p__less_equal__(X2,X1)
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X2,X0) ),
inference(ennf_transformation,[],[f43]) ).
tff(f55,plain,
! [X1: general,X0: general,X2: general] :
( p__less_equal__(X2,X1)
| ~ p__less_equal__(X2,X0)
| ~ p__less_equal__(X0,X1) ),
inference(flattening,[],[f54]) ).
tff(f57,plain,
? [X2: $int,X1: $int,X0: $int,X3: $int] :
( ~ div(f__integer__($sum(X3,1)),f__integer__(X1),f__integer__(X0),f__integer__($sum(X2,1)))
& $less(X2,$sum(X1,$uminus(1)))
& div(f__integer__(X3),f__integer__(X1),f__integer__(X0),f__integer__(X2)) ),
inference(ennf_transformation,[],[f45]) ).
tff(f58,plain,
? [X2: $int,X0: $int,X1: $int,X3: $int] :
( $less(X2,$sum(X1,$uminus(1)))
& div(f__integer__(X3),f__integer__(X1),f__integer__(X0),f__integer__(X2))
& ~ div(f__integer__($sum(X3,1)),f__integer__(X1),f__integer__(X0),f__integer__($sum(X2,1))) ),
inference(flattening,[],[f57]) ).
tff(f59,plain,
! [X0: $int,X1: $int] :
( ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) )
& ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) ) ),
inference(nnf_transformation,[],[f39]) ).
tff(f60,plain,
! [X1: $int,X0: $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(nnf_transformation,[],[f46]) ).
tff(f61,plain,
! [X0: $int,X1: $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(rectify,[],[f60]) ).
tff(f62,plain,
! [X0: general,X1: general,X2: general] :
( p__less_equal__(X2,X0)
| ~ p__less_equal__(X2,X1)
| ~ p__less_equal__(X1,X0) ),
inference(rectify,[],[f55]) ).
tff(f64,plain,
! [X1: general,X2: general,X0: general,X3: general] :
( ( ? [X5: general,X7: general,X6: general,X4: general] :
( ? [X16: general,X17: general] :
( ( f__integer__(0) = X16 )
& ( X5 = X17 )
& p__less_equal__(X16,X17) )
& ( X1 = X7 )
& ( X3 = X5 )
& ( X2 = X6 )
& ? [X9: general,X8: general] :
( ( X4 = X8 )
& p__less__(X9,X8)
& ( X5 = X9 ) )
& ( X0 = X4 )
& ? [X10: general,X11: general] :
( ? [X13: $int,X12: $int] :
( ( f__integer__(X12) = X5 )
& ? [X15: $int,X14: $int] :
( ( f__integer__(X14) = X4 )
& ( $product(X14,X15) = X13 )
& ( f__integer__(X15) = X6 ) )
& ( f__integer__($sum(X13,X12)) = X11 ) )
& ( X10 = X11 )
& ( X7 = X10 ) ) )
| ~ div(X1,X0,X2,X3) )
& ( div(X1,X0,X2,X3)
| ! [X5: general,X7: general,X6: general,X4: general] :
( ! [X16: general,X17: general] :
( ( f__integer__(0) != X16 )
| ( X5 != X17 )
| ~ p__less_equal__(X16,X17) )
| ( X1 != X7 )
| ( X3 != X5 )
| ( X2 != X6 )
| ! [X9: general,X8: general] :
( ( X4 != X8 )
| ~ p__less__(X9,X8)
| ( X5 != X9 ) )
| ( X0 != X4 )
| ! [X10: general,X11: general] :
( ! [X13: $int,X12: $int] :
( ( f__integer__(X12) != X5 )
| ! [X15: $int,X14: $int] :
( ( f__integer__(X14) != X4 )
| ( $product(X14,X15) != X13 )
| ( f__integer__(X15) != X6 ) )
| ( f__integer__($sum(X13,X12)) != X11 ) )
| ( X10 != X11 )
| ( X7 != X10 ) ) ) ) ),
inference(nnf_transformation,[],[f44]) ).
tff(f65,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ? [X4: general,X5: general,X6: general,X7: general] :
( ? [X8: general,X9: general] :
( ( f__integer__(0) = X8 )
& ( X4 = X9 )
& p__less_equal__(X8,X9) )
& ( X0 = X5 )
& ( X3 = X4 )
& ( X1 = X6 )
& ? [X10: general,X11: general] :
( ( X7 = X11 )
& p__less__(X10,X11)
& ( X4 = X10 ) )
& ( X2 = X7 )
& ? [X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__(X15) = X4 )
& ? [X16: $int,X17: $int] :
( ( f__integer__(X17) = X7 )
& ( $product(X17,X16) = X14 )
& ( f__integer__(X16) = X6 ) )
& ( f__integer__($sum(X14,X15)) = X13 ) )
& ( X12 = X13 )
& ( X5 = X12 ) ) )
| ~ div(X0,X2,X1,X3) )
& ( div(X0,X2,X1,X3)
| ! [X18: general,X19: general,X20: general,X21: general] :
( ! [X22: general,X23: general] :
( ( f__integer__(0) != X22 )
| ( X18 != X23 )
| ~ p__less_equal__(X22,X23) )
| ( X0 != X19 )
| ( X3 != X18 )
| ( X1 != X20 )
| ! [X24: general,X25: general] :
( ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X18 != X24 ) )
| ( X2 != X21 )
| ! [X26: general,X27: general] :
( ! [X28: $int,X29: $int] :
( ( f__integer__(X29) != X18 )
| ! [X30: $int,X31: $int] :
( ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 ) )
| ( f__integer__($sum(X28,X29)) != X27 ) )
| ( X26 != X27 )
| ( X19 != X26 ) ) ) ) ),
inference(rectify,[],[f64]) ).
tff(f66,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ( ( f__integer__(0) = sK5(X0,X1,X2,X3) )
& ( sK6(X0,X1,X2,X3) = sK1(X0,X1,X2,X3) )
& p__less_equal__(sK5(X0,X1,X2,X3),sK6(X0,X1,X2,X3))
& ( sK2(X0,X1,X2,X3) = X0 )
& ( sK1(X0,X1,X2,X3) = X3 )
& ( sK3(X0,X1,X2,X3) = X1 )
& ( sK4(X0,X1,X2,X3) = sK8(X0,X1,X2,X3) )
& p__less__(sK7(X0,X1,X2,X3),sK8(X0,X1,X2,X3))
& ( sK7(X0,X1,X2,X3) = sK1(X0,X1,X2,X3) )
& ( sK4(X0,X1,X2,X3) = X2 )
& ( f__integer__(sK12(X0,X1,X2,X3)) = sK1(X0,X1,X2,X3) )
& ( f__integer__(sK14(X0,X1,X2,X3)) = sK4(X0,X1,X2,X3) )
& ( $product(sK14(X0,X1,X2,X3),sK13(X0,X1,X2,X3)) = sK11(X0,X1,X2,X3) )
& ( f__integer__(sK13(X0,X1,X2,X3)) = sK3(X0,X1,X2,X3) )
& ( f__integer__($sum(sK11(X0,X1,X2,X3),sK12(X0,X1,X2,X3))) = sK10(X0,X1,X2,X3) )
& ( sK10(X0,X1,X2,X3) = sK9(X0,X1,X2,X3) )
& ( sK2(X0,X1,X2,X3) = sK9(X0,X1,X2,X3) ) )
| ~ div(X0,X2,X1,X3) )
& ( div(X0,X2,X1,X3)
| ! [X18: general,X19: general,X20: general,X21: general] :
( ! [X22: general,X23: general] :
( ( f__integer__(0) != X22 )
| ( X18 != X23 )
| ~ p__less_equal__(X22,X23) )
| ( X0 != X19 )
| ( X3 != X18 )
| ( X1 != X20 )
| ! [X24: general,X25: general] :
( ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X18 != X24 ) )
| ( X2 != X21 )
| ! [X26: general,X27: general] :
( ! [X28: $int,X29: $int] :
( ( f__integer__(X29) != X18 )
| ! [X30: $int,X31: $int] :
( ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 ) )
| ( f__integer__($sum(X28,X29)) != X27 ) )
| ( X26 != X27 )
| ( X19 != X26 ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X4,sK1(X0,X1,X2,X3)),skolemize(X5,sK2(X0,X1,X2,X3)),skolemize(X6,sK3(X0,X1,X2,X3)),skolemize(X7,sK4(X0,X1,X2,X3)),skolemize(X8,sK5(X0,X1,X2,X3)),skolemize(X9,sK6(X0,X1,X2,X3)),skolemize(X10,sK7(X0,X1,X2,X3)),skolemize(X11,sK8(X0,X1,X2,X3)),skolemize(X12,sK9(X0,X1,X2,X3)),skolemize(X13,sK10(X0,X1,X2,X3)),skolemize(X14,sK11(X0,X1,X2,X3)),skolemize(X15,sK12(X0,X1,X2,X3)),skolemize(X16,sK13(X0,X1,X2,X3)),skolemize(X17,sK14(X0,X1,X2,X3))],[f65]) ).
tff(f68,plain,
! [X0: general,X1: general] :
( ( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
| ~ p__less__(X1,X0) )
& ( p__less__(X1,X0)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) ) ),
inference(nnf_transformation,[],[f48]) ).
tff(f69,plain,
! [X0: general,X1: general] :
( ( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
| ~ p__less__(X1,X0) )
& ( p__less__(X1,X0)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) ) ),
inference(flattening,[],[f68]) ).
tff(f70,plain,
? [X0: $int,X1: $int,X2: $int,X3: $int] :
( $less(X0,$sum(X2,$uminus(1)))
& div(f__integer__(X3),f__integer__(X2),f__integer__(X1),f__integer__(X0))
& ~ div(f__integer__($sum(X3,1)),f__integer__(X2),f__integer__(X1),f__integer__($sum(X0,1))) ),
inference(rectify,[],[f58]) ).
tff(f71,plain,
( $less(sK15,$sum(sK17,$uminus(1)))
& div(f__integer__(sK18),f__integer__(sK17),f__integer__(sK16),f__integer__(sK15))
& ~ div(f__integer__($sum(sK18,1)),f__integer__(sK17),f__integer__(sK16),f__integer__($sum(sK15,1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17,sK18]),skolemize(X0,sK15),skolemize(X1,sK16),skolemize(X2,sK17),skolemize(X3,sK18)],[f70]) ).
tff(f78,plain,
! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f59]) ).
tff(f79,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X0),f__integer__(X1))
| ~ $less(X1,X0) ),
inference(cnf_transformation,[],[f61]) ).
tff(f80,plain,
! [X0: $int,X1: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f61]) ).
tff(f81,plain,
! [X2: general,X0: general,X1: general] :
( p__less_equal__(X2,X0)
| ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X2,X1) ),
inference(cnf_transformation,[],[f62]) ).
tff(f83,plain,
! [X2: general,X21: general,X3: general,X31: $int,X0: general,X29: $int,X28: $int,X1: general,X18: general,X19: general,X26: general,X27: general,X24: general,X22: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X0,X2,X1,X3)
| ( f__integer__(0) != X22 )
| ( X18 != X23 )
| ~ p__less_equal__(X22,X23)
| ( X0 != X19 )
| ( X3 != X18 )
| ( X1 != X20 )
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X18 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X18 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f84,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK2(X0,X1,X2,X3) = sK9(X0,X1,X2,X3) )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f85,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( sK10(X0,X1,X2,X3) = sK9(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f86,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( f__integer__($sum(sK11(X0,X1,X2,X3),sK12(X0,X1,X2,X3))) = sK10(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f87,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( f__integer__(sK13(X0,X1,X2,X3)) = sK3(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f88,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( $product(sK14(X0,X1,X2,X3),sK13(X0,X1,X2,X3)) = sK11(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f89,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( f__integer__(sK14(X0,X1,X2,X3)) = sK4(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f90,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( f__integer__(sK12(X0,X1,X2,X3)) = sK1(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f91,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK4(X0,X1,X2,X3) = X2 )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f95,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK3(X0,X1,X2,X3) = X1 )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f96,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK1(X0,X1,X2,X3) = X3 )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f97,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK2(X0,X1,X2,X3) = X0 )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f98,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| p__less_equal__(sK5(X0,X1,X2,X3),sK6(X0,X1,X2,X3)) ),
inference(cnf_transformation,[],[f66]) ).
tff(f99,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ div(X0,X2,X1,X3)
| ( sK6(X0,X1,X2,X3) = sK1(X0,X1,X2,X3) ) ),
inference(cnf_transformation,[],[f66]) ).
tff(f100,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( f__integer__(0) = sK5(X0,X1,X2,X3) )
| ~ div(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f66]) ).
tff(f103,plain,
! [X0: general,X1: general] :
( p__less__(X1,X0)
| ( X0 = X1 )
| ~ p__less_equal__(X1,X0) ),
inference(cnf_transformation,[],[f69]) ).
tff(f106,plain,
~ div(f__integer__($sum(sK18,1)),f__integer__(sK17),f__integer__(sK16),f__integer__($sum(sK15,1))),
inference(cnf_transformation,[],[f71]) ).
tff(f107,plain,
div(f__integer__(sK18),f__integer__(sK17),f__integer__(sK16),f__integer__(sK15)),
inference(cnf_transformation,[],[f71]) ).
tff(f108,plain,
$less(sK15,$sum(sK17,$uminus(1))),
inference(cnf_transformation,[],[f71]) ).
tff(f119,plain,
! [X2: general,X21: general,X3: general,X31: $int,X0: general,X29: $int,X28: $int,X1: general,X18: general,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X0,X2,X1,X3)
| ( X18 != X23 )
| ~ p__less_equal__(f__integer__(0),X23)
| ( X0 != X19 )
| ( X3 != X18 )
| ( X1 != X20 )
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X18 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X18 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f83]) ).
tff(f120,plain,
! [X2: general,X21: general,X3: general,X31: $int,X0: general,X29: $int,X28: $int,X1: general,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X0,X2,X1,X3)
| ~ p__less_equal__(f__integer__(0),X23)
| ( X0 != X19 )
| ( X3 != X23 )
| ( X1 != X20 )
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X23 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X23 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f119]) ).
tff(f121,plain,
! [X2: general,X21: general,X3: general,X31: $int,X29: $int,X28: $int,X1: general,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X19,X2,X1,X3)
| ~ p__less_equal__(f__integer__(0),X23)
| ( X3 != X23 )
| ( X1 != X20 )
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X23 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X23 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f120]) ).
tff(f122,plain,
! [X2: general,X21: general,X31: $int,X28: $int,X29: $int,X1: general,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X19,X2,X1,X23)
| ~ p__less_equal__(f__integer__(0),X23)
| ( X1 != X20 )
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X23 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X23 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f121]) ).
tff(f123,plain,
! [X2: general,X21: general,X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X19,X2,X20,X23)
| ~ p__less_equal__(f__integer__(0),X23)
| ( X21 != X25 )
| ~ p__less__(X24,X25)
| ( X23 != X24 )
| ( X2 != X21 )
| ( f__integer__(X29) != X23 )
| ( f__integer__(X31) != X21 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f122]) ).
tff(f124,plain,
! [X2: general,X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X24: general,X25: general,X23: general,X30: $int,X20: general] :
( div(X19,X2,X20,X23)
| ~ p__less_equal__(f__integer__(0),X23)
| ~ p__less__(X24,X25)
| ( X23 != X24 )
| ( X2 != X25 )
| ( f__integer__(X29) != X23 )
| ( f__integer__(X31) != X25 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f123]) ).
tff(f125,plain,
! [X2: general,X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X24: general,X25: general,X30: $int,X20: general] :
( div(X19,X2,X20,X24)
| ~ p__less_equal__(f__integer__(0),X24)
| ~ p__less__(X24,X25)
| ( X2 != X25 )
| ( f__integer__(X29) != X24 )
| ( f__integer__(X31) != X25 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f124]) ).
tff(f126,plain,
! [X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X24: general,X25: general,X30: $int,X20: general] :
( div(X19,X25,X20,X24)
| ~ p__less_equal__(f__integer__(0),X24)
| ~ p__less__(X24,X25)
| ( f__integer__(X29) != X24 )
| ( f__integer__(X31) != X25 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f125]) ).
tff(f127,plain,
! [X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X25: general,X30: $int,X20: general] :
( div(X19,X25,X20,f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),X25)
| ( f__integer__(X31) != X25 )
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f126]) ).
tff(f128,plain,
! [X31: $int,X28: $int,X29: $int,X19: general,X26: general,X27: general,X30: $int,X20: general] :
( div(X19,f__integer__(X31),X20,f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31))
| ( $product(X31,X30) != X28 )
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum(X28,X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f127]) ).
tff(f129,plain,
! [X31: $int,X29: $int,X19: general,X26: general,X27: general,X30: $int,X20: general] :
( div(X19,f__integer__(X31),X20,f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31))
| ( f__integer__(X30) != X20 )
| ( f__integer__($sum($product(X31,X30),X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f128]) ).
tff(f130,plain,
! [X31: $int,X29: $int,X19: general,X26: general,X27: general,X30: $int] :
( div(X19,f__integer__(X31),f__integer__(X30),f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31))
| ( f__integer__($sum($product(X31,X30),X29)) != X27 )
| ( X26 != X27 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f129]) ).
tff(f131,plain,
! [X31: $int,X29: $int,X19: general,X26: general,X30: $int] :
( div(X19,f__integer__(X31),f__integer__(X30),f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31))
| ( f__integer__($sum($product(X31,X30),X29)) != X26 )
| ( X19 != X26 ) ),
inference(equality_resolution,[],[f130]) ).
tff(f132,plain,
! [X31: $int,X29: $int,X19: general,X30: $int] :
( div(X19,f__integer__(X31),f__integer__(X30),f__integer__(X29))
| ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31))
| ( f__integer__($sum($product(X31,X30),X29)) != X19 ) ),
inference(equality_resolution,[],[f131]) ).
tff(f133,plain,
! [X31: $int,X29: $int,X30: $int] :
( ~ p__less_equal__(f__integer__(0),f__integer__(X29))
| div(f__integer__($sum($product(X31,X30),X29)),f__integer__(X31),f__integer__(X30),f__integer__(X29))
| ~ p__less__(f__integer__(X29),f__integer__(X31)) ),
inference(equality_resolution,[],[f132]) ).
tff(f137,definition,
sF20 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f138,definition,
sF21 = $sum(sK17,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f139,plain,
$sum(sK17,sF20) = sF21,
inference(reorient_equations,[],[f138]) ).
tff(f140,plain,
$less(sK15,sF21),
inference(definition_folding,[],[f108,f139,f137]) ).
tff(f141,definition,
sF22 = f__integer__(sK18),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f142,definition,
sF23 = f__integer__(sK17),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f143,plain,
f__integer__(sK17) = sF23,
inference(reorient_equations,[],[f142]) ).
tff(f144,definition,
sF24 = f__integer__(sK16),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f145,plain,
f__integer__(sK16) = sF24,
inference(reorient_equations,[],[f144]) ).
tff(f146,definition,
sF25 = f__integer__(sK15),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f147,plain,
div(sF22,sF23,sF24,sF25),
inference(definition_folding,[],[f107,f146,f145,f143,f141]) ).
tff(f148,definition,
sF26 = $sum(sK18,1),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f149,definition,
sF27 = f__integer__(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f150,plain,
f__integer__(sF26) = sF27,
inference(reorient_equations,[],[f149]) ).
tff(f151,definition,
sF28 = $sum(sK15,1),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f152,definition,
sF29 = f__integer__(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f153,plain,
~ div(sF27,sF23,sF24,sF29),
inference(definition_folding,[],[f106,f152,f151,f145,f143,f150,f148]) ).
tff(f154,plain,
sF20 = -1,
inference(evaluation,[],[f137]) ).
tff(f156,definition,
( spl30_1
<=> ( sF20 = -1 ) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
tff(f159,plain,
spl30_1,
inference(avatar_split_clause,[],[f154,f156]) ).
tff(f161,definition,
( spl30_2
<=> ( sF26 = $sum(sK18,1) ) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
tff(f164,plain,
spl30_2,
inference(avatar_split_clause,[],[f148,f161]) ).
tff(f166,definition,
( spl30_3
<=> div(sF22,sF23,sF24,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
tff(f168,plain,
( div(sF22,sF23,sF24,sF25)
| ~ spl30_3 ),
inference(avatar_component_clause,[],[f166]) ).
tff(f169,plain,
spl30_3,
inference(avatar_split_clause,[],[f147,f166]) ).
tff(f171,definition,
( spl30_4
<=> ( f__integer__(sF26) = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
tff(f173,plain,
( ( f__integer__(sF26) = sF27 )
| ~ spl30_4 ),
inference(avatar_component_clause,[],[f171]) ).
tff(f174,plain,
spl30_4,
inference(avatar_split_clause,[],[f150,f171]) ).
tff(f176,definition,
( spl30_5
<=> div(sF27,sF23,sF24,sF29) ),
introduced(definition,[new_symbols(definition,[spl30_5])],[avatar_definition]) ).
tff(f178,plain,
( ~ div(sF27,sF23,sF24,sF29)
| spl30_5 ),
inference(avatar_component_clause,[],[f176]) ).
tff(f179,plain,
~ spl30_5,
inference(avatar_split_clause,[],[f153,f176]) ).
tff(f181,definition,
( spl30_6
<=> ( sF29 = f__integer__(sF28) ) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
tff(f183,plain,
( ( sF29 = f__integer__(sF28) )
| ~ spl30_6 ),
inference(avatar_component_clause,[],[f181]) ).
tff(f184,plain,
spl30_6,
inference(avatar_split_clause,[],[f152,f181]) ).
tff(f186,definition,
( spl30_7
<=> ( sF22 = f__integer__(sK18) ) ),
introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition]) ).
tff(f188,plain,
( ( sF22 = f__integer__(sK18) )
| ~ spl30_7 ),
inference(avatar_component_clause,[],[f186]) ).
tff(f189,plain,
spl30_7,
inference(avatar_split_clause,[],[f141,f186]) ).
tff(f191,definition,
( spl30_8
<=> ( sF25 = f__integer__(sK15) ) ),
introduced(definition,[new_symbols(definition,[spl30_8])],[avatar_definition]) ).
tff(f193,plain,
( ( sF25 = f__integer__(sK15) )
| ~ spl30_8 ),
inference(avatar_component_clause,[],[f191]) ).
tff(f194,plain,
spl30_8,
inference(avatar_split_clause,[],[f146,f191]) ).
tff(f196,definition,
( spl30_9
<=> $less(sK15,sF21) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
tff(f199,plain,
spl30_9,
inference(avatar_split_clause,[],[f140,f196]) ).
tff(f201,definition,
( spl30_10
<=> ( sF28 = $sum(sK15,1) ) ),
introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition]) ).
tff(f204,plain,
spl30_10,
inference(avatar_split_clause,[],[f151,f201]) ).
tff(f206,definition,
( spl30_11
<=> ( f__integer__(sK17) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl30_11])],[avatar_definition]) ).
tff(f208,plain,
( ( f__integer__(sK17) = sF23 )
| ~ spl30_11 ),
inference(avatar_component_clause,[],[f206]) ).
tff(f209,plain,
spl30_11,
inference(avatar_split_clause,[],[f143,f206]) ).
tff(f211,definition,
( spl30_12
<=> ( $sum(sK17,sF20) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl30_12])],[avatar_definition]) ).
tff(f214,plain,
spl30_12,
inference(avatar_split_clause,[],[f139,f211]) ).
tff(f216,definition,
( spl30_13
<=> ( f__integer__(sK16) = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition]) ).
tff(f218,plain,
( ( f__integer__(sK16) = sF24 )
| ~ spl30_13 ),
inference(avatar_component_clause,[],[f216]) ).
tff(f219,plain,
spl30_13,
inference(avatar_split_clause,[],[f145,f216]) ).
tff(f223,definition,
( spl30_14
<=> ( sF28 = $sum(1,sK15) ) ),
introduced(definition,[new_symbols(definition,[spl30_14])],[avatar_definition]) ).
tff(f225,plain,
( ( sF28 = $sum(1,sK15) )
| ~ spl30_14 ),
inference(avatar_component_clause,[],[f223]) ).
tff(f228,definition,
( spl30_15
<=> ( sF26 = $sum(1,sK18) ) ),
introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition]) ).
tff(f230,plain,
( ( sF26 = $sum(1,sK18) )
| ~ spl30_15 ),
inference(avatar_component_clause,[],[f228]) ).
tff(f264,plain,
( ! [X0: $int] :
( ~ $less(sK15,X0)
| ~ p__less_equal__(f__integer__(X0),sF25) )
| ~ spl30_8 ),
inference(superposition,[],[f79,f193]) ).
tff(f366,plain,
! [X0: $int] : $less(X0,$sum(X0,1)),
inference(resolution,[],[f30,f26]) ).
tff(f379,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sF23 )
| ( sK17 = X0 ) )
| ~ spl30_11 ),
inference(superposition,[],[f78,f208]) ).
tff(f383,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sF25 )
| ( sK15 = X0 ) )
| ~ spl30_8 ),
inference(superposition,[],[f78,f193]) ).
tff(f384,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sF24 )
| ( sK16 = X0 ) )
| ~ spl30_13 ),
inference(superposition,[],[f78,f218]) ).
tff(f386,plain,
( ! [X0: $int] :
( ( f__integer__(X0) != sF22 )
| ( sK18 = X0 ) )
| ~ spl30_7 ),
inference(superposition,[],[f78,f188]) ).
tff(f394,plain,
( ! [X0: $int] :
( p__less_equal__(sF25,f__integer__(X0))
| $less(X0,sK15) )
| ~ spl30_8 ),
inference(superposition,[],[f80,f193]) ).
tff(f399,plain,
( ! [X0: $int] :
( p__less_equal__(sF29,f__integer__(X0))
| $less(X0,sF28) )
| ~ spl30_6 ),
inference(superposition,[],[f80,f183]) ).
tff(f410,plain,
( ( sF28 = sK17 )
| ( sF23 != sF29 )
| ~ spl30_6
| ~ spl30_11 ),
inference(superposition,[],[f379,f183]) ).
tff(f421,definition,
( spl30_32
<=> ( sF28 = sK17 ) ),
introduced(definition,[new_symbols(definition,[spl30_32])],[avatar_definition]) ).
tff(f425,definition,
( spl30_33
<=> ( sF23 = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl30_33])],[avatar_definition]) ).
tff(f427,plain,
( ( sF23 != sF29 )
| spl30_33 ),
inference(avatar_component_clause,[],[f425]) ).
tff(f428,plain,
( spl30_32
| ~ spl30_33
| ~ spl30_6
| ~ spl30_11 ),
inference(avatar_split_clause,[],[f410,f206,f181,f425,f421]) ).
tff(f773,plain,
( ! [X0: $int] : ( $sum(sF28,X0) = $sum(1,$sum(sK15,X0)) )
| ~ spl30_14 ),
inference(superposition,[],[f22,f225]) ).
tff(f1075,plain,
( ( sK9(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f85,f168]) ).
tff(f1077,definition,
( spl30_99
<=> ( sK9(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_99])],[avatar_definition]) ).
tff(f1079,plain,
( ( sK9(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_99 ),
inference(avatar_component_clause,[],[f1077]) ).
tff(f1080,plain,
( spl30_99
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1075,f166,f1077]) ).
tff(f1172,plain,
( p__less_equal__(sK5(sF22,sF24,sF23,sF25),sK6(sF22,sF24,sF23,sF25))
| ~ spl30_3 ),
inference(resolution,[],[f98,f168]) ).
tff(f1174,definition,
( spl30_112
<=> p__less_equal__(sK5(sF22,sF24,sF23,sF25),sK6(sF22,sF24,sF23,sF25)) ),
introduced(definition,[new_symbols(definition,[spl30_112])],[avatar_definition]) ).
tff(f1176,plain,
( p__less_equal__(sK5(sF22,sF24,sF23,sF25),sK6(sF22,sF24,sF23,sF25))
| ~ spl30_112 ),
inference(avatar_component_clause,[],[f1174]) ).
tff(f1177,plain,
( spl30_112
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1172,f166,f1174]) ).
tff(f1192,plain,
( ( sK6(sF22,sF24,sF23,sF25) = sK1(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f99,f168]) ).
tff(f1194,definition,
( spl30_113
<=> ( sK6(sF22,sF24,sF23,sF25) = sK1(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_113])],[avatar_definition]) ).
tff(f1196,plain,
( ( sK6(sF22,sF24,sF23,sF25) = sK1(sF22,sF24,sF23,sF25) )
| ~ spl30_113 ),
inference(avatar_component_clause,[],[f1194]) ).
tff(f1197,plain,
( spl30_113
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1192,f166,f1194]) ).
tff(f1208,plain,
( ( sK3(sF22,sF24,sF23,sF25) = f__integer__(sK13(sF22,sF24,sF23,sF25)) )
| ~ spl30_3 ),
inference(resolution,[],[f87,f168]) ).
tff(f1210,definition,
( spl30_114
<=> ( sK3(sF22,sF24,sF23,sF25) = f__integer__(sK13(sF22,sF24,sF23,sF25)) ) ),
introduced(definition,[new_symbols(definition,[spl30_114])],[avatar_definition]) ).
tff(f1212,plain,
( ( sK3(sF22,sF24,sF23,sF25) = f__integer__(sK13(sF22,sF24,sF23,sF25)) )
| ~ spl30_114 ),
inference(avatar_component_clause,[],[f1210]) ).
tff(f1213,plain,
( spl30_114
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1208,f166,f1210]) ).
tff(f1226,plain,
( ( f__integer__(sK14(sF22,sF24,sF23,sF25)) = sK4(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f89,f168]) ).
tff(f1228,definition,
( spl30_115
<=> ( f__integer__(sK14(sF22,sF24,sF23,sF25)) = sK4(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_115])],[avatar_definition]) ).
tff(f1230,plain,
( ( f__integer__(sK14(sF22,sF24,sF23,sF25)) = sK4(sF22,sF24,sF23,sF25) )
| ~ spl30_115 ),
inference(avatar_component_clause,[],[f1228]) ).
tff(f1231,plain,
( spl30_115
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1226,f166,f1228]) ).
tff(f1248,plain,
( ( f__integer__(sK12(sF22,sF24,sF23,sF25)) = sK1(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f90,f168]) ).
tff(f1249,plain,
( ( f__integer__(sK12(sF22,sF24,sF23,sF25)) = sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_3
| ~ spl30_113 ),
inference(forward_demodulation,[],[f1248,f1196]) ).
tff(f1251,definition,
( spl30_116
<=> ( f__integer__(sK12(sF22,sF24,sF23,sF25)) = sK6(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_116])],[avatar_definition]) ).
tff(f1253,plain,
( ( f__integer__(sK12(sF22,sF24,sF23,sF25)) = sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_116 ),
inference(avatar_component_clause,[],[f1251]) ).
tff(f1254,plain,
( spl30_116
| ~ spl30_3
| ~ spl30_113 ),
inference(avatar_split_clause,[],[f1249,f1194,f166,f1251]) ).
tff(f1280,plain,
( ( $product(sK14(sF22,sF24,sF23,sF25),sK13(sF22,sF24,sF23,sF25)) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f88,f168]) ).
tff(f1281,plain,
( ( $product(sK13(sF22,sF24,sF23,sF25),sK14(sF22,sF24,sF23,sF25)) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(forward_demodulation,[],[f1280,f32]) ).
tff(f1283,definition,
( spl30_119
<=> ( $product(sK13(sF22,sF24,sF23,sF25),sK14(sF22,sF24,sF23,sF25)) = sK11(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_119])],[avatar_definition]) ).
tff(f1285,plain,
( ( $product(sK13(sF22,sF24,sF23,sF25),sK14(sF22,sF24,sF23,sF25)) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_119 ),
inference(avatar_component_clause,[],[f1283]) ).
tff(f1286,plain,
( spl30_119
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1281,f166,f1283]) ).
tff(f1299,plain,
( ( f__integer__($sum(sK11(sF22,sF24,sF23,sF25),sK12(sF22,sF24,sF23,sF25))) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_3 ),
inference(resolution,[],[f86,f168]) ).
tff(f1301,definition,
( spl30_120
<=> ( f__integer__($sum(sK11(sF22,sF24,sF23,sF25),sK12(sF22,sF24,sF23,sF25))) = sK10(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_120])],[avatar_definition]) ).
tff(f1303,plain,
( ( f__integer__($sum(sK11(sF22,sF24,sF23,sF25),sK12(sF22,sF24,sF23,sF25))) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_120 ),
inference(avatar_component_clause,[],[f1301]) ).
tff(f1304,plain,
( spl30_120
| ~ spl30_3 ),
inference(avatar_split_clause,[],[f1299,f166,f1301]) ).
tff(f1326,plain,
( ! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(0),sF29)
| ~ p__less__(sF29,f__integer__(X0))
| div(f__integer__($sum($product(X0,X1),sF28)),f__integer__(X0),f__integer__(X1),sF29) )
| ~ spl30_6 ),
inference(superposition,[],[f133,f183]) ).
tff(f1335,plain,
( ! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(0),sF29)
| ~ p__less__(sF29,f__integer__(X0))
| div(f__integer__($sum(sF28,$product(X0,X1))),f__integer__(X0),f__integer__(X1),sF29) )
| ~ spl30_6 ),
inference(forward_demodulation,[],[f1326,f21]) ).
tff(f1361,definition,
( spl30_127
<=> p__less_equal__(f__integer__(0),sF25) ),
introduced(definition,[new_symbols(definition,[spl30_127])],[avatar_definition]) ).
tff(f1362,plain,
( p__less_equal__(f__integer__(0),sF25)
| ~ spl30_127 ),
inference(avatar_component_clause,[],[f1361]) ).
tff(f1378,definition,
( spl30_131
<=> ! [X0: $int,X1: $int] :
( ~ p__less__(sF29,f__integer__(X0))
| div(f__integer__($sum(sF28,$product(X0,X1))),f__integer__(X0),f__integer__(X1),sF29) ) ),
introduced(definition,[new_symbols(definition,[spl30_131])],[avatar_definition]) ).
tff(f1379,plain,
( ! [X0: $int,X1: $int] :
( ~ p__less__(sF29,f__integer__(X0))
| div(f__integer__($sum(sF28,$product(X0,X1))),f__integer__(X0),f__integer__(X1),sF29) )
| ~ spl30_131 ),
inference(avatar_component_clause,[],[f1378]) ).
tff(f1381,definition,
( spl30_132
<=> p__less_equal__(f__integer__(0),sF29) ),
introduced(definition,[new_symbols(definition,[spl30_132])],[avatar_definition]) ).
tff(f1383,plain,
( ~ p__less_equal__(f__integer__(0),sF29)
| spl30_132 ),
inference(avatar_component_clause,[],[f1381]) ).
tff(f1384,plain,
( spl30_131
| ~ spl30_132
| ~ spl30_6 ),
inference(avatar_split_clause,[],[f1335,f181,f1381,f1378]) ).
tff(f1422,plain,
( ~ div(sF22,sF23,sF24,sF25)
| ( sK2(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_99 ),
inference(superposition,[],[f84,f1079]) ).
tff(f1423,plain,
( ( sK2(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_3
| ~ spl30_99 ),
inference(forward_subsumption_resolution,[],[f1422,f168]) ).
tff(f1426,definition,
( spl30_137
<=> ( sK2(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_137])],[avatar_definition]) ).
tff(f1428,plain,
( ( sK2(sF22,sF24,sF23,sF25) = sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_137 ),
inference(avatar_component_clause,[],[f1426]) ).
tff(f1429,plain,
( spl30_137
| ~ spl30_3
| ~ spl30_99 ),
inference(avatar_split_clause,[],[f1423,f1077,f166,f1426]) ).
tff(f1491,plain,
( p__less_equal__(f__integer__(0),sK6(sF22,sF24,sF23,sF25))
| ~ div(sF22,sF23,sF24,sF25)
| ~ spl30_112 ),
inference(superposition,[],[f1176,f100]) ).
tff(f1492,plain,
( p__less_equal__(f__integer__(0),sK6(sF22,sF24,sF23,sF25))
| ~ spl30_3
| ~ spl30_112 ),
inference(forward_subsumption_resolution,[],[f1491,f168]) ).
tff(f1503,definition,
( spl30_148
<=> p__less_equal__(f__integer__(0),sK6(sF22,sF24,sF23,sF25)) ),
introduced(definition,[new_symbols(definition,[spl30_148])],[avatar_definition]) ).
tff(f1506,plain,
( spl30_148
| ~ spl30_3
| ~ spl30_112 ),
inference(avatar_split_clause,[],[f1492,f1174,f166,f1503]) ).
tff(f1529,plain,
( ~ div(sF22,sF23,sF24,sF25)
| ( sF25 = sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_113 ),
inference(superposition,[],[f96,f1196]) ).
tff(f1530,plain,
( ( sF25 = sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_3
| ~ spl30_113 ),
inference(forward_subsumption_resolution,[],[f1529,f168]) ).
tff(f1533,definition,
( spl30_151
<=> ( sF25 = sK6(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_151])],[avatar_definition]) ).
tff(f1535,plain,
( ( sF25 = sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_151 ),
inference(avatar_component_clause,[],[f1533]) ).
tff(f1536,plain,
( spl30_151
| ~ spl30_3
| ~ spl30_113 ),
inference(avatar_split_clause,[],[f1530,f1194,f166,f1533]) ).
tff(f1537,plain,
( ! [X0: general] :
( ~ p__less_equal__(X0,sF29)
| ~ p__less_equal__(f__integer__(0),X0) )
| spl30_132 ),
inference(resolution,[],[f1383,f81]) ).
tff(f1677,plain,
( ( sK17 = sK14(sF22,sF24,sF23,sF25) )
| ( sK4(sF22,sF24,sF23,sF25) != sF23 )
| ~ spl30_11
| ~ spl30_115 ),
inference(superposition,[],[f379,f1230]) ).
tff(f1733,definition,
( spl30_183
<=> ( sK17 = sK14(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_183])],[avatar_definition]) ).
tff(f1735,plain,
( ( sK17 = sK14(sF22,sF24,sF23,sF25) )
| ~ spl30_183 ),
inference(avatar_component_clause,[],[f1733]) ).
tff(f1737,definition,
( spl30_184
<=> ( sK4(sF22,sF24,sF23,sF25) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl30_184])],[avatar_definition]) ).
tff(f1739,plain,
( ( sK4(sF22,sF24,sF23,sF25) != sF23 )
| spl30_184 ),
inference(avatar_component_clause,[],[f1737]) ).
tff(f1740,plain,
( spl30_183
| ~ spl30_184
| ~ spl30_11
| ~ spl30_115 ),
inference(avatar_split_clause,[],[f1677,f1228,f206,f1737,f1733]) ).
tff(f1768,plain,
( ( sK12(sF22,sF24,sF23,sF25) = sK15 )
| ( sF25 != sK6(sF22,sF24,sF23,sF25) )
| ~ spl30_8
| ~ spl30_116 ),
inference(superposition,[],[f383,f1253]) ).
tff(f1793,plain,
( ( sK12(sF22,sF24,sF23,sF25) = sK15 )
| ~ spl30_8
| ~ spl30_116
| ~ spl30_151 ),
inference(forward_subsumption_resolution,[],[f1768,f1535]) ).
tff(f1815,definition,
( spl30_192
<=> ( sK12(sF22,sF24,sF23,sF25) = sK15 ) ),
introduced(definition,[new_symbols(definition,[spl30_192])],[avatar_definition]) ).
tff(f1817,plain,
( ( sK12(sF22,sF24,sF23,sF25) = sK15 )
| ~ spl30_192 ),
inference(avatar_component_clause,[],[f1815]) ).
tff(f1818,plain,
( spl30_192
| ~ spl30_8
| ~ spl30_116
| ~ spl30_151 ),
inference(avatar_split_clause,[],[f1793,f1533,f1251,f191,f1815]) ).
tff(f2075,plain,
( ( sK3(sF22,sF24,sF23,sF25) != sF24 )
| ( sK13(sF22,sF24,sF23,sF25) = sK16 )
| ~ spl30_13
| ~ spl30_114 ),
inference(superposition,[],[f384,f1212]) ).
tff(f2094,definition,
( spl30_221
<=> ( sK13(sF22,sF24,sF23,sF25) = sK16 ) ),
introduced(definition,[new_symbols(definition,[spl30_221])],[avatar_definition]) ).
tff(f2096,plain,
( ( sK13(sF22,sF24,sF23,sF25) = sK16 )
| ~ spl30_221 ),
inference(avatar_component_clause,[],[f2094]) ).
tff(f2098,definition,
( spl30_222
<=> ( sK3(sF22,sF24,sF23,sF25) = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl30_222])],[avatar_definition]) ).
tff(f2100,plain,
( ( sK3(sF22,sF24,sF23,sF25) != sF24 )
| spl30_222 ),
inference(avatar_component_clause,[],[f2098]) ).
tff(f2101,plain,
( spl30_221
| ~ spl30_222
| ~ spl30_13
| ~ spl30_114 ),
inference(avatar_split_clause,[],[f2075,f1210,f216,f2098,f2094]) ).
tff(f2132,plain,
( ( $sum(sK11(sF22,sF24,sF23,sF25),sK12(sF22,sF24,sF23,sF25)) = sK18 )
| ( sF22 != sK10(sF22,sF24,sF23,sF25) )
| ~ spl30_7
| ~ spl30_120 ),
inference(superposition,[],[f386,f1303]) ).
tff(f2159,definition,
( spl30_229
<=> ( sK2(sF22,sF24,sF23,sF25) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl30_229])],[avatar_definition]) ).
tff(f2160,plain,
( ( sK2(sF22,sF24,sF23,sF25) = sF22 )
| ~ spl30_229 ),
inference(avatar_component_clause,[],[f2159]) ).
tff(f2161,plain,
( ( sK2(sF22,sF24,sF23,sF25) != sF22 )
| spl30_229 ),
inference(avatar_component_clause,[],[f2159]) ).
tff(f2183,plain,
( ( sF23 != sF23 )
| ~ div(sF22,sF23,sF24,sF25)
| spl30_184 ),
inference(superposition,[],[f1739,f91]) ).
tff(f2184,plain,
( ~ div(sF22,sF23,sF24,sF25)
| spl30_184 ),
inference(trivial_inequality_removal,[],[f2183]) ).
tff(f2185,plain,
( $false
| ~ spl30_3
| spl30_184 ),
inference(forward_subsumption_resolution,[],[f2184,f168]) ).
tff(f2186,plain,
( ~ spl30_3
| spl30_184 ),
inference(avatar_contradiction_clause,[],[f2185]) ).
tff(f2201,plain,
( p__less_equal__(sF25,sF29)
| $less(sF28,sK15)
| ~ spl30_6
| ~ spl30_8 ),
inference(superposition,[],[f394,f183]) ).
tff(f2214,definition,
( spl30_234
<=> $less(sF28,sK15) ),
introduced(definition,[new_symbols(definition,[spl30_234])],[avatar_definition]) ).
tff(f2218,definition,
( spl30_235
<=> p__less_equal__(sF25,sF29) ),
introduced(definition,[new_symbols(definition,[spl30_235])],[avatar_definition]) ).
tff(f2220,plain,
( p__less_equal__(sF25,sF29)
| ~ spl30_235 ),
inference(avatar_component_clause,[],[f2218]) ).
tff(f2221,plain,
( spl30_234
| spl30_235
| ~ spl30_6
| ~ spl30_8 ),
inference(avatar_split_clause,[],[f2201,f191,f181,f2218,f2214]) ).
tff(f2492,plain,
( ( sF22 != sK10(sF22,sF24,sF23,sF25) )
| ( $sum(sK11(sF22,sF24,sF23,sF25),sK15) = sK18 )
| ~ spl30_7
| ~ spl30_120
| ~ spl30_192 ),
inference(forward_demodulation,[],[f2132,f1817]) ).
tff(f2503,plain,
( ( $sum(sK11(sF22,sF24,sF23,sF25),sK15) = sK18 )
| ( sK2(sF22,sF24,sF23,sF25) != sF22 )
| ~ spl30_7
| ~ spl30_120
| ~ spl30_137
| ~ spl30_192 ),
inference(forward_demodulation,[],[f2492,f1428]) ).
tff(f2695,plain,
( p__less_equal__(sF29,sF25)
| $less(sK15,sF28)
| ~ spl30_6
| ~ spl30_8 ),
inference(superposition,[],[f399,f193]) ).
tff(f2697,plain,
( $less(sK17,sF28)
| p__less_equal__(sF29,sF23)
| ~ spl30_6
| ~ spl30_11 ),
inference(superposition,[],[f399,f208]) ).
tff(f2712,definition,
( spl30_310
<=> $less(sK15,sF28) ),
introduced(definition,[new_symbols(definition,[spl30_310])],[avatar_definition]) ).
tff(f2716,definition,
( spl30_311
<=> p__less_equal__(sF29,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_311])],[avatar_definition]) ).
tff(f2719,plain,
( spl30_310
| spl30_311
| ~ spl30_6
| ~ spl30_8 ),
inference(avatar_split_clause,[],[f2695,f191,f181,f2716,f2712]) ).
tff(f2741,definition,
( spl30_316
<=> $less(sK17,sF28) ),
introduced(definition,[new_symbols(definition,[spl30_316])],[avatar_definition]) ).
tff(f2745,definition,
( spl30_317
<=> p__less_equal__(sF29,sF23) ),
introduced(definition,[new_symbols(definition,[spl30_317])],[avatar_definition]) ).
tff(f2747,plain,
( p__less_equal__(sF29,sF23)
| ~ spl30_317 ),
inference(avatar_component_clause,[],[f2745]) ).
tff(f2748,plain,
( spl30_316
| spl30_317
| ~ spl30_6
| ~ spl30_11 ),
inference(avatar_split_clause,[],[f2697,f206,f181,f2745,f2741]) ).
tff(f2773,plain,
( ~ div(sF22,sF23,sF24,sF25)
| ( sF24 != sF24 )
| spl30_222 ),
inference(superposition,[],[f2100,f95]) ).
tff(f2774,plain,
( ~ div(sF22,sF23,sF24,sF25)
| spl30_222 ),
inference(trivial_inequality_removal,[],[f2773]) ).
tff(f2775,plain,
( $false
| ~ spl30_3
| spl30_222 ),
inference(forward_subsumption_resolution,[],[f2774,f168]) ).
tff(f2776,plain,
( ~ spl30_3
| spl30_222 ),
inference(avatar_contradiction_clause,[],[f2775]) ).
tff(f2778,plain,
( ( $product(sK16,sK14(sF22,sF24,sF23,sF25)) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_119
| ~ spl30_221 ),
inference(superposition,[],[f1285,f2096]) ).
tff(f2780,plain,
( ( $product(sK16,sK17) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_119
| ~ spl30_183
| ~ spl30_221 ),
inference(forward_demodulation,[],[f2778,f1735]) ).
tff(f2782,plain,
( ( $product(sK17,sK16) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_119
| ~ spl30_183
| ~ spl30_221 ),
inference(forward_demodulation,[],[f2780,f32]) ).
tff(f2784,definition,
( spl30_322
<=> ( $product(sK17,sK16) = sK11(sF22,sF24,sF23,sF25) ) ),
introduced(definition,[new_symbols(definition,[spl30_322])],[avatar_definition]) ).
tff(f2786,plain,
( ( $product(sK17,sK16) = sK11(sF22,sF24,sF23,sF25) )
| ~ spl30_322 ),
inference(avatar_component_clause,[],[f2784]) ).
tff(f2787,plain,
( spl30_322
| ~ spl30_119
| ~ spl30_183
| ~ spl30_221 ),
inference(avatar_split_clause,[],[f2782,f2094,f1733,f1283,f2784]) ).
tff(f2963,plain,
( ~ p__less_equal__(f__integer__($sum(sK15,1)),sF25)
| ~ spl30_8 ),
inference(resolution,[],[f366,f264]) ).
tff(f2978,plain,
( ~ p__less_equal__(f__integer__($sum(1,sK15)),sF25)
| ~ spl30_8 ),
inference(forward_demodulation,[],[f2963,f21]) ).
tff(f3000,plain,
( ~ p__less_equal__(f__integer__(sF28),sF25)
| ~ spl30_8
| ~ spl30_14 ),
inference(forward_demodulation,[],[f2978,f225]) ).
tff(f3002,plain,
( ~ p__less_equal__(sF29,sF25)
| ~ spl30_6
| ~ spl30_8
| ~ spl30_14 ),
inference(forward_demodulation,[],[f3000,f183]) ).
tff(f3004,plain,
( ~ spl30_311
| ~ spl30_6
| ~ spl30_8
| ~ spl30_14 ),
inference(avatar_split_clause,[],[f3002,f223,f191,f181,f2716]) ).
tff(f3005,plain,
( ~ div(sF22,sF23,sF24,sF25)
| ( sF22 != sF22 )
| spl30_229 ),
inference(superposition,[],[f2161,f97]) ).
tff(f3006,plain,
( ~ div(sF22,sF23,sF24,sF25)
| spl30_229 ),
inference(trivial_inequality_removal,[],[f3005]) ).
tff(f3007,plain,
( $false
| ~ spl30_3
| spl30_229 ),
inference(forward_subsumption_resolution,[],[f3006,f168]) ).
tff(f3008,plain,
( ~ spl30_3
| spl30_229 ),
inference(avatar_contradiction_clause,[],[f3007]) ).
tff(f3009,plain,
( ( $sum(sK11(sF22,sF24,sF23,sF25),sK15) = sK18 )
| ~ spl30_7
| ~ spl30_120
| ~ spl30_137
| ~ spl30_192
| ~ spl30_229 ),
inference(forward_subsumption_resolution,[],[f2503,f2160]) ).
tff(f3010,plain,
( ( $sum(sK15,sK11(sF22,sF24,sF23,sF25)) = sK18 )
| ~ spl30_7
| ~ spl30_120
| ~ spl30_137
| ~ spl30_192
| ~ spl30_229 ),
inference(forward_demodulation,[],[f3009,f21]) ).
tff(f3011,plain,
( ( sK18 = $sum(sK15,$product(sK17,sK16)) )
| ~ spl30_7
| ~ spl30_120
| ~ spl30_137
| ~ spl30_192
| ~ spl30_229
| ~ spl30_322 ),
inference(forward_demodulation,[],[f3010,f2786]) ).
tff(f3013,definition,
( spl30_335
<=> ( sK18 = $sum(sK15,$product(sK17,sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl30_335])],[avatar_definition]) ).
tff(f3015,plain,
( ( sK18 = $sum(sK15,$product(sK17,sK16)) )
| ~ spl30_335 ),
inference(avatar_component_clause,[],[f3013]) ).
tff(f3016,plain,
( spl30_335
| ~ spl30_7
| ~ spl30_120
| ~ spl30_137
| ~ spl30_192
| ~ spl30_229
| ~ spl30_322 ),
inference(avatar_split_clause,[],[f3011,f2784,f2159,f1815,f1426,f1301,f186,f3013]) ).
tff(f4333,plain,
( ( $sum(sF28,$product(sK17,sK16)) = $sum(1,sK18) )
| ~ spl30_14
| ~ spl30_335 ),
inference(superposition,[],[f773,f3015]) ).
tff(f4345,plain,
( ( sF26 = $sum(sF28,$product(sK17,sK16)) )
| ~ spl30_14
| ~ spl30_15
| ~ spl30_335 ),
inference(forward_demodulation,[],[f4333,f230]) ).
tff(f4353,definition,
( spl30_391
<=> ( sF26 = $sum(sF28,$product(sK17,sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl30_391])],[avatar_definition]) ).
tff(f4355,plain,
( ( sF26 = $sum(sF28,$product(sK17,sK16)) )
| ~ spl30_391 ),
inference(avatar_component_clause,[],[f4353]) ).
tff(f4356,plain,
( spl30_391
| ~ spl30_14
| ~ spl30_15
| ~ spl30_335 ),
inference(avatar_split_clause,[],[f4345,f3013,f228,f223,f4353]) ).
tff(f7319,plain,
( ~ p__less_equal__(f__integer__(0),sF25)
| spl30_132
| ~ spl30_235 ),
inference(resolution,[],[f1537,f2220]) ).
tff(f7322,plain,
( $false
| ~ spl30_127
| spl30_132
| ~ spl30_235 ),
inference(forward_subsumption_resolution,[],[f7319,f1362]) ).
tff(f7323,plain,
( ~ spl30_127
| spl30_132
| ~ spl30_235 ),
inference(avatar_contradiction_clause,[],[f7322]) ).
tff(f7381,definition,
( spl30_541
<=> p__less__(sF29,sF23) ),
introduced(definition,[new_symbols(definition,[spl30_541])],[avatar_definition]) ).
tff(f7382,plain,
( p__less__(sF29,sF23)
| ~ spl30_541 ),
inference(avatar_component_clause,[],[f7381]) ).
tff(f7383,plain,
( ~ p__less__(sF29,sF23)
| spl30_541 ),
inference(avatar_component_clause,[],[f7381]) ).
tff(f7424,plain,
( ~ p__less_equal__(sF29,sF23)
| ( sF23 = sF29 )
| spl30_541 ),
inference(resolution,[],[f7383,f103]) ).
tff(f7425,plain,
( ( sF23 = sF29 )
| ~ spl30_317
| spl30_541 ),
inference(forward_subsumption_resolution,[],[f7424,f2747]) ).
tff(f7426,plain,
( $false
| spl30_33
| ~ spl30_317
| spl30_541 ),
inference(forward_subsumption_resolution,[],[f7425,f427]) ).
tff(f7427,plain,
( spl30_33
| ~ spl30_317
| spl30_541 ),
inference(avatar_contradiction_clause,[],[f7426]) ).
tff(f8230,plain,
( ! [X0: $int] :
( ~ p__less__(sF29,sF23)
| div(f__integer__($sum(sF28,$product(sK17,X0))),sF23,f__integer__(X0),sF29) )
| ~ spl30_11
| ~ spl30_131 ),
inference(superposition,[],[f1379,f208]) ).
tff(f8244,plain,
( ! [X0: $int] : div(f__integer__($sum(sF28,$product(sK17,X0))),sF23,f__integer__(X0),sF29)
| ~ spl30_11
| ~ spl30_131
| ~ spl30_541 ),
inference(forward_subsumption_resolution,[],[f8230,f7382]) ).
tff(f8294,plain,
( div(f__integer__(sF26),sF23,f__integer__(sK16),sF29)
| ~ spl30_11
| ~ spl30_131
| ~ spl30_391
| ~ spl30_541 ),
inference(superposition,[],[f8244,f4355]) ).
tff(f8333,plain,
( div(f__integer__(sF26),sF23,sF24,sF29)
| ~ spl30_11
| ~ spl30_13
| ~ spl30_131
| ~ spl30_391
| ~ spl30_541 ),
inference(forward_demodulation,[],[f8294,f218]) ).
tff(f8350,plain,
( div(sF27,sF23,sF24,sF29)
| ~ spl30_4
| ~ spl30_11
| ~ spl30_13
| ~ spl30_131
| ~ spl30_391
| ~ spl30_541 ),
inference(forward_demodulation,[],[f8333,f173]) ).
tff(f8357,plain,
( $false
| ~ spl30_4
| spl30_5
| ~ spl30_11
| ~ spl30_13
| ~ spl30_131
| ~ spl30_391
| ~ spl30_541 ),
inference(forward_subsumption_resolution,[],[f8350,f178]) ).
tff(f8358,plain,
( ~ spl30_4
| spl30_5
| ~ spl30_11
| ~ spl30_13
| ~ spl30_131
| ~ spl30_391
| ~ spl30_541 ),
inference(avatar_contradiction_clause,[],[f8357]) ).
tff(f8368,plain,
$false,
inference(avatar_smt_refutation,[],[f8358,f7427,f7323,f4356,f3016,f3008,f3004,f2787,f2776,f2748,f2719,f2221,f2186,f2101,f1818,f1740,f1536,f1506,f1429,f1384,f1304,f1286,f1254,f1231,f1213,f1197,f1177,f1080,f428,f219,f214,f209,f204,f199,f194,f189,f184,f179,f174,f169,f164,f159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWX081_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 14:59:34 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.12 Running first-order theorem proving
% 0.09/0.12 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.41/0.76 % (3435526)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.41/0.76 % (3435532)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2747262405:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.41/0.76 % (3435537)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2601538702:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.41/0.76 % (3435534)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3797184305:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.41/0.76 % (3435536)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4024283525:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.41/0.76 % (3435535)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2956183756:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.41/0.76 % (3435533)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4222638498:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.41/0.76 % (3435531)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1947675381:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.41/0.76 % (3435535)Instruction limit reached!
% 2.41/0.76 % (3435535)------------------------------
% 2.41/0.76 % (3435535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.76 % (3435535)CaDiCaL version: 2.1.3
% 2.41/0.76 % (3435535)Termination reason: Instruction limit
% 2.41/0.76 % (3435535)Termination phase: Saturation
% 2.41/0.76 % (3435535)Time elapsed: 0.002 s
% 2.41/0.76 % (3435535)Peak memory usage: 88 MB
% 2.41/0.76 % (3435535)Instructions burned: 4 (million)
% 2.41/0.76 % (3435534)Instruction limit reached!
% 2.41/0.76 % (3435534)------------------------------
% 2.41/0.76 % (3435534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.76 % (3435534)CaDiCaL version: 2.1.3
% 2.41/0.76 % (3435534)Termination reason: Instruction limit
% 2.41/0.76 % (3435534)Termination phase: Saturation
% 2.41/0.76 % (3435534)Time elapsed: 0.003 s
% 2.41/0.76 % (3435534)Peak memory usage: 88 MB
% 2.41/0.76 % (3435534)Instructions burned: 8 (million)
% 2.41/0.76 % (3435531)Instruction limit reached!
% 2.41/0.76 % (3435531)------------------------------
% 2.41/0.76 % (3435531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.76 % (3435531)CaDiCaL version: 2.1.3
% 2.41/0.76 % (3435531)Termination reason: Instruction limit
% 2.41/0.76 % (3435531)Termination phase: Saturation
% 2.41/0.76 % (3435531)Time elapsed: 0.019 s
% 2.41/0.76 % (3435531)Peak memory usage: 115 MB
% 2.41/0.76 % (3435531)Instructions burned: 13 (million)
% 2.41/0.76 % (3435537)Instruction limit reached!
% 2.41/0.76 % (3435537)------------------------------
% 2.41/0.76 % (3435537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.76 % (3435537)CaDiCaL version: 2.1.3
% 2.41/0.76 % (3435537)Termination reason: Instruction limit
% 2.41/0.76 % (3435537)Termination phase: Saturation
% 2.41/0.76 % (3435537)Time elapsed: 0.027 s
% 2.41/0.76 % (3435537)Peak memory usage: 115 MB
% 2.41/0.76 % (3435537)Instructions burned: 34 (million)
% 2.41/0.76 % (3435536)Instruction limit reached!
% 2.41/0.76 % (3435536)------------------------------
% 2.41/0.76 % (3435536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.76 % (3435536)CaDiCaL version: 2.1.3
% 2.41/0.76 % (3435536)Termination reason: Instruction limit
% 2.41/0.76 % (3435536)Termination phase: Saturation
% 2.41/0.76 % (3435536)Time elapsed: 0.033 s
% 2.41/0.76 % (3435536)Peak memory usage: 116 MB
% 2.41/0.76 % (3435536)Instructions burned: 47 (million)
% 2.41/0.76 % (3435533)Instruction limit reached!
% 2.41/0.76 % (3435533)------------------------------
% 2.41/0.76 % (3435533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.41/0.76 % (3435533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435533)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435533)Termination reason: Instruction limit
% 3.27/0.85 % (3435533)Termination phase: Saturation
% 3.27/0.85 % (3435533)Time elapsed: 0.092 s
% 3.27/0.85 % (3435533)Peak memory usage: 118 MB
% 3.27/0.85 % (3435533)Instructions burned: 201 (million)
% 3.27/0.85 % (3435546)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=138268761:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.27/0.85 % (3435545)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1800417382:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.27/0.85 % (3435532)Instruction limit reached!
% 3.27/0.85 % (3435532)------------------------------
% 3.27/0.85 % (3435532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435532)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435532)Termination reason: Instruction limit
% 3.27/0.85 % (3435532)Termination phase: Saturation
% 3.27/0.85 % (3435532)Time elapsed: 0.118 s
% 3.27/0.85 % (3435532)Peak memory usage: 116 MB
% 3.27/0.85 % (3435532)Instructions burned: 309 (million)
% 3.27/0.85 % (3435545)Instruction limit reached!
% 3.27/0.85 % (3435545)------------------------------
% 3.27/0.85 % (3435545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435545)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435545)Termination reason: Instruction limit
% 3.27/0.85 % (3435545)Termination phase: Saturation
% 3.27/0.85 % (3435545)Time elapsed: 0.006 s
% 3.27/0.85 % (3435545)Peak memory usage: 88 MB
% 3.27/0.85 % (3435545)Instructions burned: 15 (million)
% 3.27/0.85 % (3435546)Instruction limit reached!
% 3.27/0.85 % (3435546)------------------------------
% 3.27/0.85 % (3435546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435546)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435546)Termination reason: Instruction limit
% 3.27/0.85 % (3435546)Termination phase: Saturation
% 3.27/0.85 % (3435546)Time elapsed: 0.012 s
% 3.27/0.85 % (3435546)Peak memory usage: 88 MB
% 3.27/0.85 % (3435546)Instructions burned: 29 (million)
% 3.27/0.85 % (3435547)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3615715713:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.27/0.85 % (3435547)Instruction limit reached!
% 3.27/0.85 % (3435547)------------------------------
% 3.27/0.85 % (3435547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435547)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435547)Termination reason: Instruction limit
% 3.27/0.85 % (3435547)Termination phase: Saturation
% 3.27/0.85 % (3435547)Time elapsed: 0.007 s
% 3.27/0.85 % (3435547)Peak memory usage: 90 MB
% 3.27/0.85 % (3435547)Instructions burned: 19 (million)
% 3.27/0.85 % (3435548)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1671206593:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 3.27/0.85 % (3435549)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=1932607760:i=27:canc=cautious:fsr=off:rtra=on_2998 on theBenchmark for (2998ds/27Mi)
% 3.27/0.85 % (3435548)Instruction limit reached!
% 3.27/0.85 % (3435548)------------------------------
% 3.27/0.85 % (3435548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/0.85 % (3435548)CaDiCaL version: 2.1.3
% 3.27/0.85 % (3435548)Termination reason: Instruction limit
% 3.27/0.85 % (3435548)Termination phase: Saturation
% 3.27/0.85 % (3435548)Time elapsed: 0.011 s
% 3.27/0.85 % (3435548)Peak memory usage: 89 MB
% 3.27/0.85 % (3435548)Instructions burned: 24 (million)
% 3.27/0.85 % (3435549)Instruction limit reached!
% 3.27/0.85 % (3435549)------------------------------
% 3.27/0.85 % (3435549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/0.85 % (3435549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435549)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435549)Termination reason: Instruction limit
% 3.67/1.01 % (3435549)Termination phase: Saturation
% 3.67/1.01 % (3435549)Time elapsed: 0.011 s
% 3.67/1.01 % (3435549)Peak memory usage: 89 MB
% 3.67/1.01 % (3435549)Instructions burned: 30 (million)
% 3.67/1.01 % (3435550)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1364826293:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.67/1.01 % (3435550)Instruction limit reached!
% 3.67/1.01 % (3435550)------------------------------
% 3.67/1.01 % (3435550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.01 % (3435550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435550)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435550)Termination reason: Instruction limit
% 3.67/1.01 % (3435550)Termination phase: Saturation
% 3.67/1.01 % (3435550)Time elapsed: 0.026 s
% 3.67/1.01 % (3435550)Peak memory usage: 89 MB
% 3.67/1.01 % (3435550)Instructions burned: 86 (million)
% 3.67/1.01 % (3435553)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1258386175:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 3.67/1.01 % (3435555)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4242308049:i=4:ep=RST:ins=2:rtra=on_2997 on theBenchmark for (2997ds/4Mi)
% 3.67/1.01 % (3435554)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1049127570:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 3.67/1.01 % (3435553)Instruction limit reached!
% 3.67/1.01 % (3435553)------------------------------
% 3.67/1.01 % (3435553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.01 % (3435553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435553)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435553)Termination reason: Instruction limit
% 3.67/1.01 % (3435553)Termination phase: Saturation
% 3.67/1.01 % (3435553)Time elapsed: 0.001 s
% 3.67/1.01 % (3435553)Peak memory usage: 87 MB
% 3.67/1.01 % (3435553)Instructions burned: 2 (million)
% 3.67/1.01 % (3435555)Instruction limit reached!
% 3.67/1.01 % (3435555)------------------------------
% 3.67/1.01 % (3435555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.01 % (3435555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435555)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435555)Termination reason: Instruction limit
% 3.67/1.01 % (3435555)Termination phase: Saturation
% 3.67/1.01 % (3435555)Time elapsed: 0.002 s
% 3.67/1.01 % (3435555)Peak memory usage: 88 MB
% 3.67/1.01 % (3435555)Instructions burned: 5 (million)
% 3.67/1.01 % (3435557)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1879887595:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2997 on theBenchmark for (2997ds/66Mi)
% 3.67/1.01 % (3435560)lrs+10_1_thi=all:si=on:fd=off:random_seed=1557072553:i=53:rtra=on:gtg=all_2997 on theBenchmark for (2997ds/53Mi)
% 3.67/1.01 % (3435561)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=250608134:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 3.67/1.01 % (3435561)Instruction limit reached!
% 3.67/1.01 % (3435561)------------------------------
% 3.67/1.01 % (3435561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.01 % (3435561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435561)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435561)Termination reason: Instruction limit
% 3.67/1.01 % (3435561)Termination phase: Saturation
% 3.67/1.01 % (3435561)Time elapsed: 0.004 s
% 3.67/1.01 % (3435561)Peak memory usage: 88 MB
% 3.67/1.01 % (3435561)Instructions burned: 10 (million)
% 3.67/1.01 % (3435554)Instruction limit reached!
% 3.67/1.01 % (3435554)------------------------------
% 3.67/1.01 % (3435554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.67/1.01 % (3435554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.01 % (3435554)CaDiCaL version: 2.1.3
% 3.67/1.01 % (3435554)Termination reason: Instruction limit
% 3.67/1.01 % (3435554)Termination phase: Saturation
% 3.67/1.01 % (3435554)Time elapsed: 0.068 s
% 3.67/1.01 % (3435554)Peak memory usage: 90 MB
% 3.67/1.01 % (3435554)Instructions burned: 183 (million)
% 3.67/1.01 % (3435560)Instruction limit reached!
% 5.28/1.17 % (3435560)------------------------------
% 5.28/1.17 % (3435560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435560)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435560)Termination reason: Instruction limit
% 5.28/1.17 % (3435560)Termination phase: Saturation
% 5.28/1.17 % (3435560)Time elapsed: 0.034 s
% 5.28/1.17 % (3435560)Peak memory usage: 116 MB
% 5.28/1.17 % (3435560)Instructions burned: 56 (million)
% 5.28/1.17 % (3435557)Instruction limit reached!
% 5.28/1.17 % (3435557)------------------------------
% 5.28/1.17 % (3435557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435557)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435557)Termination reason: Instruction limit
% 5.28/1.17 % (3435557)Termination phase: Saturation
% 5.28/1.17 % (3435557)Time elapsed: 0.056 s
% 5.28/1.17 % (3435557)Peak memory usage: 134 MB
% 5.28/1.17 % (3435557)Instructions burned: 66 (million)
% 5.28/1.17 % (3435566)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2098588615:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.28/1.17 % (3435566)Instruction limit reached!
% 5.28/1.17 % (3435566)------------------------------
% 5.28/1.17 % (3435566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435566)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435566)Termination reason: Instruction limit
% 5.28/1.17 % (3435566)Termination phase: Saturation
% 5.28/1.17 % (3435566)Time elapsed: 0.002 s
% 5.28/1.17 % (3435566)Peak memory usage: 88 MB
% 5.28/1.17 % (3435566)Instructions burned: 4 (million)
% 5.28/1.17 % (3435567)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3315524616:i=2:doe=on:canc=force:asg=cautious:rtra=on_2996 on theBenchmark for (2996ds/2Mi)
% 5.28/1.17 % (3435568)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3386470506:i=127:doe=on:rtra=on_2996 on theBenchmark for (2996ds/127Mi)
% 5.28/1.17 % (3435567)Instruction limit reached!
% 5.28/1.17 % (3435567)------------------------------
% 5.28/1.17 % (3435567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435567)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435567)Termination reason: Instruction limit
% 5.28/1.17 % (3435567)Termination phase: Property scanning
% 5.28/1.17 % (3435567)Time elapsed: 0.001 s
% 5.28/1.17 % (3435567)Peak memory usage: 86 MB
% 5.28/1.17 % (3435567)Instructions burned: 2 (million)
% 5.28/1.17 % (3435572)dis+10_1_si=on:random_seed=3436866791:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 5.28/1.17 % (3435573)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2374744709:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 5.28/1.17 % (3435573)Refutation not found, incomplete strategy
% 5.28/1.17 % (3435573)------------------------------
% 5.28/1.17 % (3435573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435573)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435573)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.17 % (3435573)Time elapsed: 0.002 s
% 5.28/1.17 % (3435573)Peak memory usage: 89 MB
% 5.28/1.17 % (3435573)Instructions burned: 4 (million)
% 5.28/1.17 % (3435568)Instruction limit reached!
% 5.28/1.17 % (3435568)------------------------------
% 5.28/1.17 % (3435568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.17 % (3435568)CaDiCaL version: 2.1.3
% 5.28/1.17 % (3435568)Termination reason: Instruction limit
% 5.28/1.17 % (3435568)Termination phase: Saturation
% 5.28/1.17 % (3435568)Time elapsed: 0.062 s
% 5.28/1.17 % (3435568)Peak memory usage: 117 MB
% 5.28/1.17 % (3435568)Instructions burned: 129 (million)
% 5.28/1.17 % (3435572)Instruction limit reached!
% 5.28/1.17 % (3435572)------------------------------
% 5.28/1.17 % (3435572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.17 % (3435572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435572)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435572)Termination reason: Instruction limit
% 6.29/1.36 % (3435572)Termination phase: Saturation
% 6.29/1.36 % (3435572)Time elapsed: 0.004 s
% 6.29/1.36 % (3435572)Peak memory usage: 88 MB
% 6.29/1.36 % (3435572)Instructions burned: 10 (million)
% 6.29/1.36 % (3435574)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2255629630: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_2995 on theBenchmark for (2995ds/35Mi)
% 6.29/1.36 % (3435575)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2358371601:i=2:fsr=off:rtra=on:inst=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.29/1.36 % (3435575)Instruction limit reached!
% 6.29/1.36 % (3435575)------------------------------
% 6.29/1.36 % (3435575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.36 % (3435575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435575)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435575)Termination reason: Instruction limit
% 6.29/1.36 % (3435575)Termination phase: Saturation
% 6.29/1.36 % (3435575)Time elapsed: 0.002 s
% 6.29/1.36 % (3435575)Peak memory usage: 89 MB
% 6.29/1.36 % (3435575)Instructions burned: 4 (million)
% 6.29/1.36 % (3435574)Instruction limit reached!
% 6.29/1.36 % (3435574)------------------------------
% 6.29/1.36 % (3435574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.36 % (3435574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435574)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435574)Termination reason: Instruction limit
% 6.29/1.36 % (3435574)Termination phase: Saturation
% 6.29/1.36 % (3435574)Time elapsed: 0.028 s
% 6.29/1.36 % (3435574)Peak memory usage: 89 MB
% 6.29/1.36 % (3435574)Instructions burned: 35 (million)
% 6.29/1.36 % (3435580)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=756180077:i=370:ep=RS:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/370Mi)
% 6.29/1.36 % (3435579)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2204864900:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2995 on theBenchmark for (2995ds/8Mi)
% 6.29/1.36 % (3435579)Instruction limit reached!
% 6.29/1.36 % (3435579)------------------------------
% 6.29/1.36 % (3435579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.36 % (3435579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435579)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435579)Termination reason: Instruction limit
% 6.29/1.36 % (3435579)Termination phase: Saturation
% 6.29/1.36 % (3435579)Time elapsed: 0.004 s
% 6.29/1.36 % (3435579)Peak memory usage: 88 MB
% 6.29/1.36 % (3435579)Instructions burned: 10 (million)
% 6.29/1.36 % (3435584)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3643526271:i=226:rtra=on:gtg=position:ss=axioms_2994 on theBenchmark for (2994ds/226Mi)
% 6.29/1.36 % (3435583)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2013110140:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 6.29/1.36 % (3435583)Instruction limit reached!
% 6.29/1.36 % (3435583)------------------------------
% 6.29/1.36 % (3435583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.36 % (3435583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435583)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435583)Termination reason: Instruction limit
% 6.29/1.36 % (3435583)Termination phase: Saturation
% 6.29/1.36 % (3435583)Time elapsed: 0.018 s
% 6.29/1.36 % (3435583)Peak memory usage: 112 MB
% 6.29/1.36 % (3435583)Instructions burned: 15 (million)
% 6.29/1.36 % (3435587)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3177100587:i=10:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.29/1.36 % (3435587)Instruction limit reached!
% 6.29/1.36 % (3435587)------------------------------
% 6.29/1.36 % (3435587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.36 % (3435587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.36 % (3435587)CaDiCaL version: 2.1.3
% 6.29/1.36 % (3435587)Termination reason: Instruction limit
% 6.29/1.36 % (3435587)Termination phase: Saturation
% 6.29/1.36 % (3435587)Time elapsed: 0.005 s
% 6.29/1.36 % (3435587)Peak memory usage: 88 MB
% 7.58/1.52 % (3435587)Instructions burned: 10 (million)
% 7.58/1.52 % (3435580)Instruction limit reached!
% 7.58/1.52 % (3435580)------------------------------
% 7.58/1.52 % (3435580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.58/1.52 % (3435580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.52 % (3435580)CaDiCaL version: 2.1.3
% 7.58/1.52 % (3435580)Termination reason: Instruction limit
% 7.58/1.52 % (3435580)Termination phase: Saturation
% 7.58/1.52 % (3435580)Time elapsed: 0.109 s
% 7.58/1.52 % (3435580)Peak memory usage: 94 MB
% 7.58/1.52 % (3435580)Instructions burned: 371 (million)
% 7.58/1.52 % (3435573)------------------------------
% 7.58/1.52 % (3435573)------------------------------
% 7.58/1.52 % (3435590)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2304695625:i=71:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/71Mi)
% 7.58/1.52 % (3435584)Instruction limit reached!
% 7.58/1.52 % (3435584)------------------------------
% 7.58/1.52 % (3435584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.58/1.52 % (3435584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.52 % (3435584)CaDiCaL version: 2.1.3
% 7.58/1.52 % (3435584)Termination reason: Instruction limit
% 7.58/1.52 % (3435584)Termination phase: Saturation
% 7.58/1.52 % (3435584)Time elapsed: 0.061 s
% 7.58/1.52 % (3435584)Peak memory usage: 115 MB
% 7.58/1.52 % (3435584)Instructions burned: 229 (million)
% 7.58/1.52 % (3435591)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=3897428895:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2994 on theBenchmark for (2994ds/75Mi)
% 7.58/1.52 % (3435591)Instruction limit reached!
% 7.58/1.52 % (3435591)------------------------------
% 7.58/1.52 % (3435591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.58/1.52 % (3435591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.52 % (3435591)CaDiCaL version: 2.1.3
% 7.58/1.52 % (3435591)Termination reason: Instruction limit
% 7.58/1.52 % (3435591)Termination phase: Saturation
% 7.58/1.52 % (3435591)Time elapsed: 0.032 s
% 7.58/1.52 % (3435591)Peak memory usage: 90 MB
% 7.58/1.52 % (3435591)Instructions burned: 76 (million)
% 7.58/1.52 % (3435590)Instruction limit reached!
% 7.58/1.52 % (3435590)------------------------------
% 7.58/1.52 % (3435590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.58/1.52 % (3435590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.52 % (3435590)CaDiCaL version: 2.1.3
% 7.58/1.52 % (3435590)Termination reason: Instruction limit
% 7.58/1.52 % (3435590)Termination phase: Saturation
% 7.58/1.52 % (3435590)Time elapsed: 0.057 s
% 7.58/1.52 % (3435590)Peak memory usage: 133 MB
% 7.58/1.52 % (3435590)Instructions burned: 73 (million)
% 7.58/1.52 % (3435594)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=2024315027:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2993 on theBenchmark for (2993ds/294Mi)
% 7.58/1.52 % (3435596)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2465281905:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2993 on theBenchmark for (2993ds/130Mi)
% 7.58/1.52 % (3435597)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=42028619:i=131:rtra=on_2993 on theBenchmark for (2993ds/131Mi)
% 7.58/1.52 % (3435598)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3007722072:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/40Mi)
% 7.58/1.52 % (3435601)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3376023154:i=307:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/307Mi)
% 7.58/1.52 % (3435598)Instruction limit reached!
% 7.58/1.52 % (3435598)------------------------------
% 7.58/1.52 % (3435598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.58/1.52 % (3435598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.58/1.52 % (3435598)CaDiCaL version: 2.1.3
% 7.58/1.52 % (3435598)Termination reason: Instruction limit
% 7.58/1.52 % (3435598)Termination phase: Saturation
% 7.58/1.52 % (3435598)Time elapsed: 0.042 s
% 7.58/1.52 % (3435598)Peak memory usage: 133 MB
% 7.58/1.52 % (3435598)Instructions burned: 41 (million)
% 7.58/1.52 % (3435602)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2419310985:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/598Mi)
% 8.98/1.75 % (3435596)Instruction limit reached!
% 8.98/1.75 % (3435596)------------------------------
% 8.98/1.75 % (3435596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435596)CaDiCaL version: 2.1.3
% 8.98/1.75 % (3435596)Termination reason: Instruction limit
% 8.98/1.75 % (3435596)Termination phase: Saturation
% 8.98/1.75 % (3435596)Time elapsed: 0.059 s
% 8.98/1.75 % (3435596)Peak memory usage: 116 MB
% 8.98/1.75 % (3435596)Instructions burned: 132 (million)
% 8.98/1.75 % (3435597)Instruction limit reached!
% 8.98/1.75 % (3435597)------------------------------
% 8.98/1.75 % (3435597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435597)CaDiCaL version: 2.1.3
% 8.98/1.75 % (3435597)Termination reason: Instruction limit
% 8.98/1.75 % (3435597)Termination phase: Saturation
% 8.98/1.75 % (3435597)Time elapsed: 0.078 s
% 8.98/1.75 % (3435597)Peak memory usage: 134 MB
% 8.98/1.75 % (3435597)Instructions burned: 132 (million)
% 8.98/1.75 % (3435594)Instruction limit reached!
% 8.98/1.75 % (3435594)------------------------------
% 8.98/1.75 % (3435594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435594)CaDiCaL version: 2.1.3
% 8.98/1.75 % (3435594)Termination reason: Instruction limit
% 8.98/1.75 % (3435594)Termination phase: Saturation
% 8.98/1.75 % (3435594)Time elapsed: 0.109 s
% 8.98/1.75 % (3435594)Peak memory usage: 92 MB
% 8.98/1.75 % (3435594)Instructions burned: 294 (million)
% 8.98/1.75 % (3435603)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2177840400:i=131:canc=cautious:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/131Mi)
% 8.98/1.75 % (3435601)Instruction limit reached!
% 8.98/1.75 % (3435601)------------------------------
% 8.98/1.75 % (3435601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435601)CaDiCaL version: 2.1.3
% 8.98/1.75 % (3435601)Termination reason: Instruction limit
% 8.98/1.75 % (3435601)Termination phase: Saturation
% 8.98/1.75 % (3435601)Time elapsed: 0.106 s
% 8.98/1.75 % (3435601)Peak memory usage: 92 MB
% 8.98/1.75 % (3435601)Instructions burned: 310 (million)
% 8.98/1.75 % (3435609)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=2147455811:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2991 on theBenchmark for (2991ds/259Mi)
% 8.98/1.75 % (3435603)Instruction limit reached!
% 8.98/1.75 % (3435603)------------------------------
% 8.98/1.75 % (3435603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435603)CaDiCaL version: 2.1.3
% 8.98/1.75 % (3435603)Termination reason: Instruction limit
% 8.98/1.75 % (3435603)Termination phase: Saturation
% 8.98/1.75 % (3435603)Time elapsed: 0.060 s
% 8.98/1.75 % (3435603)Peak memory usage: 118 MB
% 8.98/1.75 % (3435603)Instructions burned: 131 (million)
% 8.98/1.75 % (3435611)dis+10_1_si=on:random_seed=888534535:s2a=on:i=1000:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/1000Mi)
% 8.98/1.75 % (3435612)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3834117062:i=383:fsr=off:rtra=on:ev=force_2991 on theBenchmark for (2991ds/383Mi)
% 8.98/1.75 % (3435614)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2160570450:i=141:doe=on:rtra=on_2991 on theBenchmark for (2991ds/141Mi)
% 8.98/1.75 % (3435615)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=199177149:i=65:nm=16:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 8.98/1.75 % (3435609)Instruction limit reached!
% 8.98/1.75 % (3435609)------------------------------
% 8.98/1.75 % (3435609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.98/1.75 % (3435609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.98/1.75 % (3435609)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435609)Termination reason: Instruction limit
% 10.47/1.94 % (3435609)Termination phase: Saturation
% 10.47/1.94 % (3435609)Time elapsed: 0.095 s
% 10.47/1.94 % (3435609)Peak memory usage: 116 MB
% 10.47/1.94 % (3435609)Instructions burned: 261 (million)
% 10.47/1.94 % (3435614)Instruction limit reached!
% 10.47/1.94 % (3435614)------------------------------
% 10.47/1.94 % (3435614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435614)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435614)Termination reason: Instruction limit
% 10.47/1.94 % (3435614)Termination phase: Saturation
% 10.47/1.94 % (3435614)Time elapsed: 0.050 s
% 10.47/1.94 % (3435614)Peak memory usage: 90 MB
% 10.47/1.94 % (3435614)Instructions burned: 143 (million)
% 10.47/1.94 % (3435617)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3523188975:i=121:nm=16:rtra=on_2990 on theBenchmark for (2990ds/121Mi)
% 10.47/1.94 % (3435615)Instruction limit reached!
% 10.47/1.94 % (3435615)------------------------------
% 10.47/1.94 % (3435615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435615)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435615)Termination reason: Instruction limit
% 10.47/1.94 % (3435615)Termination phase: Saturation
% 10.47/1.94 % (3435615)Time elapsed: 0.039 s
% 10.47/1.94 % (3435615)Peak memory usage: 117 MB
% 10.47/1.94 % (3435615)Instructions burned: 66 (million)
% 10.47/1.94 % (3435602)Instruction limit reached!
% 10.47/1.94 % (3435602)------------------------------
% 10.47/1.94 % (3435602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435602)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435602)Termination reason: Instruction limit
% 10.47/1.94 % (3435602)Termination phase: Saturation
% 10.47/1.94 % (3435602)Time elapsed: 0.242 s
% 10.47/1.94 % (3435602)Peak memory usage: 138 MB
% 10.47/1.94 % (3435602)Instructions burned: 599 (million)
% 10.47/1.94 % (3435617)Instruction limit reached!
% 10.47/1.94 % (3435617)------------------------------
% 10.47/1.94 % (3435617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435617)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435617)Termination reason: Instruction limit
% 10.47/1.94 % (3435617)Termination phase: Saturation
% 10.47/1.94 % (3435617)Time elapsed: 0.040 s
% 10.47/1.94 % (3435617)Peak memory usage: 90 MB
% 10.47/1.94 % (3435617)Instructions burned: 122 (million)
% 10.47/1.94 % (3435612)Instruction limit reached!
% 10.47/1.94 % (3435612)------------------------------
% 10.47/1.94 % (3435612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435612)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435612)Termination reason: Instruction limit
% 10.47/1.94 % (3435612)Termination phase: Saturation
% 10.47/1.94 % (3435612)Time elapsed: 0.128 s
% 10.47/1.94 % (3435612)Peak memory usage: 93 MB
% 10.47/1.94 % (3435612)Instructions burned: 384 (million)
% 10.47/1.94 % (3435623)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=2372508614:i=39:ins=3:rtra=on_2989 on theBenchmark for (2989ds/39Mi)
% 10.47/1.94 % (3435622)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=3408587974:s2a=on:i=128:s2at=5:ins=3:rtra=on_2989 on theBenchmark for (2989ds/128Mi)
% 10.47/1.94 % (3435625)dis+1010_1_to=kbo:si=on:random_seed=339811872:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2989 on theBenchmark for (2989ds/175Mi)
% 10.47/1.94 % (3435623)Instruction limit reached!
% 10.47/1.94 % (3435623)------------------------------
% 10.47/1.94 % (3435623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/1.94 % (3435623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/1.94 % (3435623)CaDiCaL version: 2.1.3
% 10.47/1.94 % (3435623)Termination reason: Instruction limit
% 10.47/1.94 % (3435623)Termination phase: Saturation
% 10.47/1.94 % (3435623)Time elapsed: 0.030 s
% 10.47/1.94 % (3435623)Peak memory usage: 117 MB
% 10.47/1.94 % (3435623)Instructions burned: 41 (million)
% 10.47/1.94 % (3435626)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1678914778:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/329Mi)
% 12.55/2.14 % (3435627)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2056201822:s2a=on:i=483:doe=on:nm=32:rtra=on_2988 on theBenchmark for (2988ds/483Mi)
% 12.55/2.14 % (3435622)Instruction limit reached!
% 12.55/2.14 % (3435622)------------------------------
% 12.55/2.14 % (3435622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435622)CaDiCaL version: 2.1.3
% 12.55/2.14 % (3435622)Termination reason: Instruction limit
% 12.55/2.14 % (3435622)Termination phase: Saturation
% 12.55/2.14 % (3435622)Time elapsed: 0.061 s
% 12.55/2.14 % (3435622)Peak memory usage: 119 MB
% 12.55/2.14 % (3435622)Instructions burned: 128 (million)
% 12.55/2.14 % (3435628)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=1697765012:thitd=on:i=215:nm=0:rtra=on:ev=force_2988 on theBenchmark for (2988ds/215Mi)
% 12.55/2.14 % (3435625)Instruction limit reached!
% 12.55/2.14 % (3435625)------------------------------
% 12.55/2.14 % (3435625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435625)CaDiCaL version: 2.1.3
% 12.55/2.14 % (3435625)Termination reason: Instruction limit
% 12.55/2.14 % (3435625)Termination phase: Saturation
% 12.55/2.14 % (3435625)Time elapsed: 0.068 s
% 12.55/2.14 % (3435625)Peak memory usage: 91 MB
% 12.55/2.14 % (3435625)Instructions burned: 176 (million)
% 12.55/2.14 % (3435611)Instruction limit reached!
% 12.55/2.14 % (3435611)------------------------------
% 12.55/2.14 % (3435611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435611)CaDiCaL version: 2.1.3
% 12.55/2.14 % (3435611)Termination reason: Instruction limit
% 12.55/2.14 % (3435611)Termination phase: Saturation
% 12.55/2.14 % (3435611)Time elapsed: 0.300 s
% 12.55/2.14 % (3435611)Peak memory usage: 97 MB
% 12.55/2.14 % (3435611)Instructions burned: 1000 (million)
% 12.55/2.14 % (3435632)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=2513778931:i=349:rtra=on_2988 on theBenchmark for (2988ds/349Mi)
% 12.55/2.14 % (3435635)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=819969456:st=2:i=295:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/295Mi)
% 12.55/2.14 % (3435628)Instruction limit reached!
% 12.55/2.14 % (3435628)------------------------------
% 12.55/2.14 % (3435628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435628)CaDiCaL version: 2.1.3
% 12.55/2.14 % (3435628)Termination reason: Instruction limit
% 12.55/2.14 % (3435628)Termination phase: Saturation
% 12.55/2.14 % (3435628)Time elapsed: 0.097 s
% 12.55/2.14 % (3435628)Peak memory usage: 135 MB
% 12.55/2.14 % (3435628)Instructions burned: 216 (million)
% 12.55/2.14 % (3435626)Instruction limit reached!
% 12.55/2.14 % (3435626)------------------------------
% 12.55/2.14 % (3435626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435626)CaDiCaL version: 2.1.3
% 12.55/2.14 % (3435626)Termination reason: Instruction limit
% 12.55/2.14 % (3435626)Termination phase: Saturation
% 12.55/2.14 % (3435626)Time elapsed: 0.140 s
% 12.55/2.14 % (3435626)Peak memory usage: 119 MB
% 12.55/2.14 % (3435626)Instructions burned: 331 (million)
% 12.55/2.14 % (3435637)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=948352507:i=328:kws=inv_frequency:nm=20:rtra=on_2987 on theBenchmark for (2987ds/328Mi)
% 12.55/2.14 % (3435638)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1240672599:i=281:gtgl=2:rtra=on:gtg=all_2987 on theBenchmark for (2987ds/281Mi)
% 12.55/2.14 % (3435635)Instruction limit reached!
% 12.55/2.14 % (3435635)------------------------------
% 12.55/2.14 % (3435635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.55/2.14 % (3435635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.55/2.14 % (3435635)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435635)Termination reason: Instruction limit
% 13.27/2.32 % (3435635)Termination phase: Saturation
% 13.27/2.32 % (3435635)Time elapsed: 0.089 s
% 13.27/2.32 % (3435635)Peak memory usage: 90 MB
% 13.27/2.32 % (3435635)Instructions burned: 297 (million)
% 13.27/2.32 % (3435627)Instruction limit reached!
% 13.27/2.32 % (3435627)------------------------------
% 13.27/2.32 % (3435627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.32 % (3435627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.32 % (3435627)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435627)Termination reason: Instruction limit
% 13.27/2.32 % (3435627)Termination phase: Saturation
% 13.27/2.32 % (3435627)Time elapsed: 0.207 s
% 13.27/2.32 % (3435627)Peak memory usage: 135 MB
% 13.27/2.32 % (3435627)Instructions burned: 484 (million)
% 13.27/2.32 % (3435632)Instruction limit reached!
% 13.27/2.32 % (3435632)------------------------------
% 13.27/2.32 % (3435632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.32 % (3435632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.32 % (3435632)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435632)Termination reason: Instruction limit
% 13.27/2.32 % (3435632)Termination phase: Saturation
% 13.27/2.32 % (3435632)Time elapsed: 0.129 s
% 13.27/2.32 % (3435632)Peak memory usage: 118 MB
% 13.27/2.32 % (3435632)Instructions burned: 351 (million)
% 13.27/2.32 % (3435641)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2739593973:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/484Mi)
% 13.27/2.32 % (3435642)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=892130670:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2986 on theBenchmark for (2986ds/321Mi)
% 13.27/2.32 % (3435637)Instruction limit reached!
% 13.27/2.32 % (3435637)------------------------------
% 13.27/2.32 % (3435637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.32 % (3435637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.32 % (3435637)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435637)Termination reason: Instruction limit
% 13.27/2.32 % (3435637)Termination phase: Saturation
% 13.27/2.32 % (3435637)Time elapsed: 0.130 s
% 13.27/2.32 % (3435637)Peak memory usage: 118 MB
% 13.27/2.32 % (3435637)Instructions burned: 331 (million)
% 13.27/2.32 % (3435638)Instruction limit reached!
% 13.27/2.32 % (3435638)------------------------------
% 13.27/2.32 % (3435638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.32 % (3435638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.32 % (3435638)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435638)Termination reason: Instruction limit
% 13.27/2.32 % (3435638)Termination phase: Saturation
% 13.27/2.32 % (3435638)Time elapsed: 0.119 s
% 13.27/2.32 % (3435638)Peak memory usage: 118 MB
% 13.27/2.32 % (3435638)Instructions burned: 283 (million)
% 13.27/2.32 % (3435645)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=709269821:i=416:rtra=on:gtg=position:ss=axioms_2985 on theBenchmark for (2985ds/416Mi)
% 13.27/2.32 % (3435646)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3374352836:i=471:thf=on:kws=precedence:rtra=on_2985 on theBenchmark for (2985ds/471Mi)
% 13.27/2.32 % (3435642)Instruction limit reached!
% 13.27/2.32 % (3435642)------------------------------
% 13.27/2.32 % (3435642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.32 % (3435642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.32 % (3435642)CaDiCaL version: 2.1.3
% 13.27/2.32 % (3435642)Termination reason: Instruction limit
% 13.27/2.32 % (3435642)Termination phase: Saturation
% 13.27/2.32 % (3435642)Time elapsed: 0.084 s
% 13.27/2.32 % (3435642)Peak memory usage: 113 MB
% 13.27/2.32 % (3435642)Instructions burned: 325 (million)
% 13.27/2.32 % (3435647)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=589379377:avsq=on:i=276:avsqr=1,2:rtra=on_2985 on theBenchmark for (2985ds/276Mi)
% 13.27/2.32 % (3435650)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=293176097:i=375:kws=inv_arity_squared:rtra=on_2985 on theBenchmark for (2985ds/375Mi)
% 13.27/2.32 % (3435641)Instruction limit reached!
% 13.27/2.32 % (3435641)------------------------------
% 13.27/2.32 % (3435641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435641)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435641)Termination reason: Instruction limit
% 14.24/2.63 % (3435641)Termination phase: Saturation
% 14.24/2.63 % (3435641)Time elapsed: 0.159 s
% 14.24/2.63 % (3435641)Peak memory usage: 92 MB
% 14.24/2.63 % (3435641)Instructions burned: 488 (million)
% 14.24/2.63 % (3435651)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=761417778:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/387Mi)
% 14.24/2.63 % (3435645)Instruction limit reached!
% 14.24/2.63 % (3435645)------------------------------
% 14.24/2.63 % (3435645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435645)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435645)Termination reason: Instruction limit
% 14.24/2.63 % (3435645)Termination phase: Saturation
% 14.24/2.63 % (3435645)Time elapsed: 0.097 s
% 14.24/2.63 % (3435645)Peak memory usage: 115 MB
% 14.24/2.63 % (3435645)Instructions burned: 422 (million)
% 14.24/2.63 % (3435654)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=274398498:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2984 on theBenchmark for (2984ds/513Mi)
% 14.24/2.63 % (3435647)Instruction limit reached!
% 14.24/2.63 % (3435647)------------------------------
% 14.24/2.63 % (3435647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435647)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435647)Termination reason: Instruction limit
% 14.24/2.63 % (3435647)Termination phase: Saturation
% 14.24/2.63 % (3435647)Time elapsed: 0.132 s
% 14.24/2.63 % (3435647)Peak memory usage: 136 MB
% 14.24/2.63 % (3435647)Instructions burned: 276 (million)
% 14.24/2.63 % (3435646)Instruction limit reached!
% 14.24/2.63 % (3435646)------------------------------
% 14.24/2.63 % (3435646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435646)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435646)Termination reason: Instruction limit
% 14.24/2.63 % (3435646)Termination phase: Saturation
% 14.24/2.63 % (3435646)Time elapsed: 0.169 s
% 14.24/2.63 % (3435646)Peak memory usage: 119 MB
% 14.24/2.63 % (3435646)Instructions burned: 471 (million)
% 14.24/2.63 % (3435658)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1245539561:i=334:rtra=on_2983 on theBenchmark for (2983ds/334Mi)
% 14.24/2.63 % (3435650)Instruction limit reached!
% 14.24/2.63 % (3435650)------------------------------
% 14.24/2.63 % (3435650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435650)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435650)Termination reason: Instruction limit
% 14.24/2.63 % (3435650)Termination phase: Saturation
% 14.24/2.63 % (3435650)Time elapsed: 0.142 s
% 14.24/2.63 % (3435650)Peak memory usage: 118 MB
% 14.24/2.63 % (3435650)Instructions burned: 376 (million)
% 14.24/2.63 % (3435659)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3467460039:i=359:rtra=on:gtg=exists_top:ss=axioms_2983 on theBenchmark for (2983ds/359Mi)
% 14.24/2.63 % (3435651)Instruction limit reached!
% 14.24/2.63 % (3435651)------------------------------
% 14.24/2.63 % (3435651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.24/2.63 % (3435651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.24/2.63 % (3435651)CaDiCaL version: 2.1.3
% 14.24/2.63 % (3435651)Termination reason: Instruction limit
% 14.24/2.63 % (3435651)Termination phase: Saturation
% 14.24/2.63 % (3435651)Time elapsed: 0.155 s
% 14.24/2.63 % (3435651)Peak memory usage: 120 MB
% 14.24/2.63 % (3435651)Instructions burned: 388 (million)
% 14.24/2.63 % (3435662)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3539609812:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/261Mi)
% 14.24/2.63 % (3435661)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2410401572:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2982 on theBenchmark for (2982ds/341Mi)
% 16.58/2.97 % (3435654)Instruction limit reached!
% 16.58/2.97 % (3435654)------------------------------
% 16.58/2.97 % (3435654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435654)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435654)Termination reason: Instruction limit
% 16.58/2.97 % (3435654)Termination phase: Saturation
% 16.58/2.97 % (3435654)Time elapsed: 0.178 s
% 16.58/2.97 % (3435654)Peak memory usage: 93 MB
% 16.58/2.97 % (3435654)Instructions burned: 513 (million)
% 16.58/2.97 % (3435665)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=4003380261:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/235Mi)
% 16.58/2.97 % (3435662)Refutation not found, incomplete strategy
% 16.58/2.97 % (3435662)------------------------------
% 16.58/2.97 % (3435662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435662)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435662)Termination reason: Refutation not found, incomplete strategy
% 16.58/2.97 % (3435662)Time elapsed: 0.046 s
% 16.58/2.97 % (3435662)Peak memory usage: 116 MB
% 16.58/2.97 % (3435662)Instructions burned: 85 (million)
% 16.58/2.97 % (3435659)Instruction limit reached!
% 16.58/2.97 % (3435659)------------------------------
% 16.58/2.97 % (3435659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435659)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435659)Termination reason: Instruction limit
% 16.58/2.97 % (3435659)Termination phase: Saturation
% 16.58/2.97 % (3435659)Time elapsed: 0.123 s
% 16.58/2.97 % (3435659)Peak memory usage: 91 MB
% 16.58/2.97 % (3435659)Instructions burned: 359 (million)
% 16.58/2.97 % (3435658)Instruction limit reached!
% 16.58/2.97 % (3435658)------------------------------
% 16.58/2.97 % (3435658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435658)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435658)Termination reason: Instruction limit
% 16.58/2.97 % (3435658)Termination phase: Saturation
% 16.58/2.97 % (3435658)Time elapsed: 0.146 s
% 16.58/2.97 % (3435658)Peak memory usage: 137 MB
% 16.58/2.97 % (3435658)Instructions burned: 335 (million)
% 16.58/2.97 % (3435666)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3129261474:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2982 on theBenchmark for (2982ds/273Mi)
% 16.58/2.97 % (3435661)Instruction limit reached!
% 16.58/2.97 % (3435661)------------------------------
% 16.58/2.97 % (3435661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435661)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435661)Termination reason: Instruction limit
% 16.58/2.97 % (3435661)Termination phase: Saturation
% 16.58/2.97 % (3435661)Time elapsed: 0.126 s
% 16.58/2.97 % (3435661)Peak memory usage: 118 MB
% 16.58/2.97 % (3435661)Instructions burned: 345 (million)
% 16.58/2.97 % (3435665)Instruction limit reached!
% 16.58/2.97 % (3435665)------------------------------
% 16.58/2.97 % (3435665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.58/2.97 % (3435665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.58/2.97 % (3435665)CaDiCaL version: 2.1.3
% 16.58/2.97 % (3435665)Termination reason: Instruction limit
% 16.58/2.97 % (3435665)Termination phase: Saturation
% 16.58/2.97 % (3435665)Time elapsed: 0.088 s
% 16.58/2.97 % (3435665)Peak memory usage: 116 MB
% 16.58/2.97 % (3435665)Instructions burned: 238 (million)
% 16.58/2.97 % (3435669)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1903790560:i=146:doe=on:rtra=on_2981 on theBenchmark for (2981ds/146Mi)
% 16.58/2.97 % (3435671)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=3722333856:i=4428:doe=on:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/4428Mi)
% 16.58/2.97 % (3435672)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=186131321:avsq=on:i=276:avsqr=1,2:rtra=on_2981 on theBenchmark for (2981ds/276Mi)
% 20.07/3.28 % (3435666)Instruction limit reached!
% 20.07/3.28 % (3435666)------------------------------
% 20.07/3.28 % (3435666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.07/3.28 % (3435666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.07/3.28 % (3435666)CaDiCaL version: 2.1.3
% 20.07/3.28 % (3435666)Termination reason: Instruction limit
% 20.07/3.28 % (3435666)Termination phase: Saturation
% 20.07/3.28 % (3435666)Time elapsed: 0.103 s
% 20.07/3.28 % (3435666)Peak memory usage: 92 MB
% 20.07/3.28 % (3435666)Instructions burned: 274 (million)
% 20.07/3.28 % (3435662)------------------------------
% 20.07/3.28 % (3435662)------------------------------
% 20.07/3.28 % (3435669)Instruction limit reached!
% 20.07/3.28 % (3435669)------------------------------
% 20.07/3.28 % (3435669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.07/3.28 % (3435669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.07/3.28 % (3435669)CaDiCaL version: 2.1.3
% 20.07/3.28 % (3435669)Termination reason: Instruction limit
% 20.07/3.28 % (3435669)Termination phase: Saturation
% 20.07/3.28 % (3435669)Time elapsed: 0.053 s
% 20.07/3.28 % (3435669)Peak memory usage: 91 MB
% 20.07/3.28 % (3435669)Instructions burned: 147 (million)
% 20.07/3.28 % (3435674)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2703149100:i=1052:rtra=on_2980 on theBenchmark for (2980ds/1052Mi)
% 20.07/3.28 % (3435675)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=877054987:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2980 on theBenchmark for (2980ds/655Mi)
% 20.07/3.28 % (3435679)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4070456562:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2979 on theBenchmark for (2979ds/1054Mi)
% 20.07/3.28 % (3435672)Instruction limit reached!
% 20.07/3.28 % (3435672)------------------------------
% 20.07/3.28 % (3435672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.07/3.28 % (3435672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.07/3.28 % (3435672)CaDiCaL version: 2.1.3
% 20.07/3.28 % (3435672)Termination reason: Instruction limit
% 20.07/3.28 % (3435672)Termination phase: Saturation
% 20.07/3.28 % (3435672)Time elapsed: 0.127 s
% 20.07/3.28 % (3435672)Peak memory usage: 134 MB
% 20.07/3.28 % (3435672)Instructions burned: 276 (million)
% 20.07/3.28 % (3435681)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1643986022:s2a=on:i=450:doe=on:nm=32:rtra=on_2979 on theBenchmark for (2979ds/450Mi)
% 20.07/3.28 % (3435680)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3903640036:i=107:rtra=on_2979 on theBenchmark for (2979ds/107Mi)
% 20.07/3.28 % (3435680)Refutation not found, incomplete strategy
% 20.07/3.28 % (3435680)------------------------------
% 20.07/3.28 % (3435680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.07/3.28 % (3435680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.07/3.28 % (3435680)CaDiCaL version: 2.1.3
% 20.07/3.28 % (3435680)Termination reason: Refutation not found, incomplete strategy
% 20.07/3.28 % (3435680)Time elapsed: 0.020 s
% 20.07/3.28 % (3435680)Peak memory usage: 115 MB
% 20.07/3.28 % (3435680)Instructions burned: 10 (million)
% 20.07/3.28 % (3435685)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
% 20.07/3.28 % (3435685)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4141438590:i=1090:aac=none:nm=0:rtra=on:rawr=on_2978 on theBenchmark for (2978ds/1090Mi)
% 20.07/3.28 % (3435675)Instruction limit reached!
% 20.07/3.28 % (3435675)------------------------------
% 20.07/3.28 % (3435675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.07/3.28 % (3435675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.07/3.28 % (3435675)CaDiCaL version: 2.1.3
% 20.07/3.28 % (3435675)Termination reason: Instruction limit
% 20.07/3.28 % (3435675)Termination phase: Saturation
% 20.07/3.28 % (3435675)Time elapsed: 0.245 s
% 20.07/3.28 % (3435675)Peak memory usage: 95 MB
% 20.07/3.28 % (3435675)Instructions burned: 657 (million)
% 20.07/3.28 % (3435680)------------------------------
% 22.11/3.61 % (3435680)------------------------------
% 22.11/3.61 % (3435681)Instruction limit reached!
% 22.11/3.61 % (3435681)------------------------------
% 22.11/3.61 % (3435681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435681)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435681)Termination reason: Instruction limit
% 22.11/3.61 % (3435681)Termination phase: Saturation
% 22.11/3.61 % (3435681)Time elapsed: 0.195 s
% 22.11/3.61 % (3435681)Peak memory usage: 134 MB
% 22.11/3.61 % (3435681)Instructions burned: 451 (million)
% 22.11/3.61 % (3435689)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2163731453:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2976 on theBenchmark for (2976ds/130Mi)
% 22.11/3.61 % (3435674)Instruction limit reached!
% 22.11/3.61 % (3435674)------------------------------
% 22.11/3.61 % (3435674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435674)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435674)Termination reason: Instruction limit
% 22.11/3.61 % (3435674)Termination phase: Saturation
% 22.11/3.61 % (3435674)Time elapsed: 0.356 s
% 22.11/3.61 % (3435674)Peak memory usage: 95 MB
% 22.11/3.61 % (3435674)Instructions burned: 1052 (million)
% 22.11/3.61 % (3435690)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2875681506:i=312:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/312Mi)
% 22.11/3.61 % (3435679)Instruction limit reached!
% 22.11/3.61 % (3435679)------------------------------
% 22.11/3.61 % (3435679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435679)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435679)Termination reason: Instruction limit
% 22.11/3.61 % (3435679)Termination phase: Saturation
% 22.11/3.61 % (3435679)Time elapsed: 0.337 s
% 22.11/3.61 % (3435679)Peak memory usage: 91 MB
% 22.11/3.61 % (3435679)Instructions burned: 1057 (million)
% 22.11/3.61 % (3435691)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=883091719:i=491:doe=on:rtra=on:gtg=position_2976 on theBenchmark for (2976ds/491Mi)
% 22.11/3.61 % (3435689)Instruction limit reached!
% 22.11/3.61 % (3435689)------------------------------
% 22.11/3.61 % (3435689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435689)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435689)Termination reason: Instruction limit
% 22.11/3.61 % (3435689)Termination phase: Saturation
% 22.11/3.61 % (3435689)Time elapsed: 0.059 s
% 22.11/3.61 % (3435689)Peak memory usage: 117 MB
% 22.11/3.61 % (3435689)Instructions burned: 130 (million)
% 22.11/3.61 % (3435693)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2946377079:s2a=on:i=835:s2at=2:rtra=on_2975 on theBenchmark for (2975ds/835Mi)
% 22.11/3.61 % (3435690)Instruction limit reached!
% 22.11/3.61 % (3435690)------------------------------
% 22.11/3.61 % (3435690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435690)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435690)Termination reason: Instruction limit
% 22.11/3.61 % (3435690)Termination phase: Saturation
% 22.11/3.61 % (3435690)Time elapsed: 0.123 s
% 22.11/3.61 % (3435690)Peak memory usage: 118 MB
% 22.11/3.61 % (3435690)Instructions burned: 315 (million)
% 22.11/3.61 % (3435695)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2722321459:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2975 on theBenchmark for (2975ds/307Mi)
% 22.11/3.61 % (3435697)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3424547433:i=776:doe=on:rtra=on_2975 on theBenchmark for (2975ds/776Mi)
% 22.11/3.61 % (3435691)Instruction limit reached!
% 22.11/3.61 % (3435691)------------------------------
% 22.11/3.61 % (3435691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.11/3.61 % (3435691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.11/3.61 % (3435691)CaDiCaL version: 2.1.3
% 22.11/3.61 % (3435691)Termination reason: Instruction limit
% 22.11/3.61 % (3435691)Termination phase: Saturation
% 22.11/3.61 % (3435691)Time elapsed: 0.177 s
% 26.78/4.13 % (3435691)Peak memory usage: 93 MB
% 26.78/4.13 % (3435691)Instructions burned: 493 (million)
% 26.78/4.13 % (3435685)Instruction limit reached!
% 26.78/4.13 % (3435685)------------------------------
% 26.78/4.13 % (3435685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.78/4.13 % (3435685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.13 % (3435685)CaDiCaL version: 2.1.3
% 26.78/4.13 % (3435685)Termination reason: Instruction limit
% 26.78/4.13 % (3435685)Termination phase: Saturation
% 26.78/4.13 % (3435685)Time elapsed: 0.395 s
% 26.78/4.13 % (3435685)Peak memory usage: 123 MB
% 26.78/4.13 % (3435685)Instructions burned: 1093 (million)
% 26.78/4.13 % (3435695)Instruction limit reached!
% 26.78/4.13 % (3435695)------------------------------
% 26.78/4.13 % (3435695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.78/4.13 % (3435695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.13 % (3435695)CaDiCaL version: 2.1.3
% 26.78/4.13 % (3435695)Termination reason: Instruction limit
% 26.78/4.13 % (3435695)Termination phase: Saturation
% 26.78/4.13 % (3435695)Time elapsed: 0.113 s
% 26.78/4.13 % (3435695)Peak memory usage: 93 MB
% 26.78/4.13 % (3435695)Instructions burned: 308 (million)
% 26.78/4.13 % (3435699)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4156419632:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/646Mi)
% 26.78/4.13 % (3435703)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=485960007:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2973 on theBenchmark for (2973ds/1131Mi)
% 26.78/4.13 % (3435702)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=549583524:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2973 on theBenchmark for (2973ds/784Mi)
% 26.78/4.13 % (3435693)Instruction limit reached!
% 26.78/4.13 % (3435693)------------------------------
% 26.78/4.13 % (3435693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.78/4.13 % (3435693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.13 % (3435693)CaDiCaL version: 2.1.3
% 26.78/4.13 % (3435693)Termination reason: Instruction limit
% 26.78/4.13 % (3435693)Termination phase: Saturation
% 26.78/4.13 % (3435693)Time elapsed: 0.262 s
% 26.78/4.13 % (3435693)Peak memory usage: 93 MB
% 26.78/4.13 % (3435693)Instructions burned: 838 (million)
% 26.78/4.13 % (3435704)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=2148763569:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2973 on theBenchmark for (2973ds/246Mi)
% 26.78/4.13 % (3435697)Instruction limit reached!
% 26.78/4.13 % (3435697)------------------------------
% 26.78/4.13 % (3435697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.78/4.13 % (3435697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.13 % (3435697)CaDiCaL version: 2.1.3
% 26.78/4.13 % (3435697)Termination reason: Instruction limit
% 26.78/4.13 % (3435697)Termination phase: Saturation
% 26.78/4.13 % (3435697)Time elapsed: 0.227 s
% 26.78/4.13 % (3435697)Peak memory usage: 119 MB
% 26.78/4.13 % (3435697)Instructions burned: 778 (million)
% 26.78/4.13 % (3435704)Instruction limit reached!
% 26.78/4.13 % (3435704)------------------------------
% 26.78/4.13 % (3435704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.78/4.13 % (3435704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.78/4.13 % (3435704)CaDiCaL version: 2.1.3
% 26.78/4.13 % (3435704)Termination reason: Instruction limit
% 26.78/4.13 % (3435704)Termination phase: Saturation
% 26.78/4.13 % (3435704)Time elapsed: 0.092 s
% 26.78/4.13 % (3435704)Peak memory usage: 117 MB
% 26.78/4.13 % (3435704)Instructions burned: 247 (million)
% 26.78/4.13 % (3435708)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=3107028657:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/775Mi)
% 26.78/4.13 % (3435710)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1941269275:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2971 on theBenchmark for (2971ds/273Mi)
% 26.78/4.13 % (3435699)Instruction limit reached!
% 26.78/4.13 % (3435699)------------------------------
% 35.12/5.32 % (3435699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435699)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435699)Termination reason: Instruction limit
% 35.12/5.32 % (3435699)Termination phase: Saturation
% 35.12/5.32 % (3435699)Time elapsed: 0.255 s
% 35.12/5.32 % (3435699)Peak memory usage: 139 MB
% 35.12/5.32 % (3435699)Instructions burned: 648 (million)
% 35.12/5.32 % (3435711)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2606319343:i=102:nm=16:rtra=on_2970 on theBenchmark for (2970ds/102Mi)
% 35.12/5.32 % (3435710)Instruction limit reached!
% 35.12/5.32 % (3435710)------------------------------
% 35.12/5.32 % (3435710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435710)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435710)Termination reason: Instruction limit
% 35.12/5.32 % (3435710)Termination phase: Saturation
% 35.12/5.32 % (3435710)Time elapsed: 0.099 s
% 35.12/5.32 % (3435710)Peak memory usage: 92 MB
% 35.12/5.32 % (3435710)Instructions burned: 275 (million)
% 35.12/5.32 % (3435702)Instruction limit reached!
% 35.12/5.32 % (3435702)------------------------------
% 35.12/5.32 % (3435702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435702)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435702)Termination reason: Instruction limit
% 35.12/5.32 % (3435702)Termination phase: Saturation
% 35.12/5.32 % (3435702)Time elapsed: 0.301 s
% 35.12/5.32 % (3435702)Peak memory usage: 121 MB
% 35.12/5.32 % (3435702)Instructions burned: 784 (million)
% 35.12/5.32 % (3435711)Instruction limit reached!
% 35.12/5.32 % (3435711)------------------------------
% 35.12/5.32 % (3435711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435711)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435711)Termination reason: Instruction limit
% 35.12/5.32 % (3435711)Termination phase: Saturation
% 35.12/5.32 % (3435711)Time elapsed: 0.033 s
% 35.12/5.32 % (3435711)Peak memory usage: 89 MB
% 35.12/5.32 % (3435711)Instructions burned: 105 (million)
% 35.12/5.32 % (3435714)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=3589505499:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2970 on theBenchmark for (2970ds/1094Mi)
% 35.12/5.32 % (3435716)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1947291865:i=6400:doe=on:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/6400Mi)
% 35.12/5.32 % (3435703)Instruction limit reached!
% 35.12/5.32 % (3435703)------------------------------
% 35.12/5.32 % (3435703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435703)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435703)Termination reason: Instruction limit
% 35.12/5.32 % (3435703)Termination phase: Saturation
% 35.12/5.32 % (3435703)Time elapsed: 0.402 s
% 35.12/5.32 % (3435703)Peak memory usage: 123 MB
% 35.12/5.32 % (3435703)Instructions burned: 1134 (million)
% 35.12/5.32 % (3435717)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=2421513192:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2969 on theBenchmark for (2969ds/868Mi)
% 35.12/5.32 % (3435718)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=2219831672:i=1846:canc=cautious:fsr=off:rtra=on_2969 on theBenchmark for (2969ds/1846Mi)
% 35.12/5.32 % (3435708)Instruction limit reached!
% 35.12/5.32 % (3435708)------------------------------
% 35.12/5.32 % (3435708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.12/5.32 % (3435708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.12/5.32 % (3435708)CaDiCaL version: 2.1.3
% 35.12/5.32 % (3435708)Termination reason: Instruction limit
% 35.12/5.32 % (3435708)Termination phase: Saturation
% 35.12/5.32 % (3435708)Time elapsed: 0.290 s
% 35.12/5.32 % (3435708)Peak memory usage: 97 MB
% 35.12/5.32 % (3435708)Instructions burned: 776 (million)
% 35.12/5.32 % (3435721)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1096322026:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2968 on theBenchmark for (2968ds/36816Mi)
% 40.90/6.18 % (3435724)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=4136740149:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2967 on theBenchmark for (2967ds/273Mi)
% 40.90/6.18 % (3435671)Instruction limit reached!
% 40.90/6.18 % (3435671)------------------------------
% 40.90/6.18 % (3435671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435671)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435671)Termination reason: Instruction limit
% 40.90/6.18 % (3435671)Termination phase: Saturation
% 40.90/6.18 % (3435671)Time elapsed: 1.340 s
% 40.90/6.18 % (3435671)Peak memory usage: 112 MB
% 40.90/6.18 % (3435671)Instructions burned: 4428 (million)
% 40.90/6.18 % (3435714)Instruction limit reached!
% 40.90/6.18 % (3435714)------------------------------
% 40.90/6.18 % (3435714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435714)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435714)Termination reason: Instruction limit
% 40.90/6.18 % (3435714)Termination phase: Saturation
% 40.90/6.18 % (3435714)Time elapsed: 0.339 s
% 40.90/6.18 % (3435714)Peak memory usage: 96 MB
% 40.90/6.18 % (3435714)Instructions burned: 1095 (million)
% 40.90/6.18 % (3435724)Instruction limit reached!
% 40.90/6.18 % (3435724)------------------------------
% 40.90/6.18 % (3435724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435724)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435724)Termination reason: Instruction limit
% 40.90/6.18 % (3435724)Termination phase: Saturation
% 40.90/6.18 % (3435724)Time elapsed: 0.102 s
% 40.90/6.18 % (3435724)Peak memory usage: 92 MB
% 40.90/6.18 % (3435724)Instructions burned: 275 (million)
% 40.90/6.18 % (3435727)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=1941494058:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2966 on theBenchmark for (2966ds/863Mi)
% 40.90/6.18 % (3435717)Instruction limit reached!
% 40.90/6.18 % (3435717)------------------------------
% 40.90/6.18 % (3435717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435717)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435717)Termination reason: Instruction limit
% 40.90/6.18 % (3435717)Termination phase: Saturation
% 40.90/6.18 % (3435717)Time elapsed: 0.287 s
% 40.90/6.18 % (3435717)Peak memory usage: 119 MB
% 40.90/6.18 % (3435717)Instructions burned: 870 (million)
% 40.90/6.18 % (3435728)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=822497318:i=5811:kws=precedence:nm=0:rtra=on_2965 on theBenchmark for (2965ds/5811Mi)
% 40.90/6.18 % (3435729)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=161294690:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/2216Mi)
% 40.90/6.18 % (3435731)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1709724752:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2965 on theBenchmark for (2965ds/801Mi)
% 40.90/6.18 % (3435727)Instruction limit reached!
% 40.90/6.18 % (3435727)------------------------------
% 40.90/6.18 % (3435727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435727)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435727)Termination reason: Instruction limit
% 40.90/6.18 % (3435727)Termination phase: Saturation
% 40.90/6.18 % (3435727)Time elapsed: 0.273 s
% 40.90/6.18 % (3435727)Peak memory usage: 118 MB
% 40.90/6.18 % (3435727)Instructions burned: 865 (million)
% 40.90/6.18 % (3435718)Instruction limit reached!
% 40.90/6.18 % (3435718)------------------------------
% 40.90/6.18 % (3435718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.18 % (3435718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.18 % (3435718)CaDiCaL version: 2.1.3
% 40.90/6.18 % (3435718)Termination reason: Instruction limit
% 42.54/6.44 % (3435718)Termination phase: Saturation
% 42.54/6.44 % (3435718)Time elapsed: 0.619 s
% 42.54/6.44 % (3435718)Peak memory usage: 101 MB
% 42.54/6.44 % (3435718)Instructions burned: 1848 (million)
% 42.54/6.44 % (3435735)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=848928062:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2962 on theBenchmark for (2962ds/1026Mi)
% 42.54/6.44 % (3435736)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1860679968:i=3509:rtra=on_2961 on theBenchmark for (2961ds/3509Mi)
% 42.54/6.44 % (3435731)Instruction limit reached!
% 42.54/6.44 % (3435731)------------------------------
% 42.54/6.44 % (3435731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435731)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435731)Termination reason: Instruction limit
% 42.54/6.44 % (3435731)Termination phase: Saturation
% 42.54/6.44 % (3435731)Time elapsed: 0.324 s
% 42.54/6.44 % (3435731)Peak memory usage: 98 MB
% 42.54/6.44 % (3435731)Instructions burned: 801 (million)
% 42.54/6.44 % (3435739)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3928387491:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/2127Mi)
% 42.54/6.44 % (3435735)Instruction limit reached!
% 42.54/6.44 % (3435735)------------------------------
% 42.54/6.44 % (3435735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435735)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435735)Termination reason: Instruction limit
% 42.54/6.44 % (3435735)Termination phase: Saturation
% 42.54/6.44 % (3435735)Time elapsed: 0.316 s
% 42.54/6.44 % (3435735)Peak memory usage: 90 MB
% 42.54/6.44 % (3435735)Instructions burned: 1028 (million)
% 42.54/6.44 % (3435729)Instruction limit reached!
% 42.54/6.44 % (3435729)------------------------------
% 42.54/6.44 % (3435729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435729)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435729)Termination reason: Instruction limit
% 42.54/6.44 % (3435729)Termination phase: Saturation
% 42.54/6.44 % (3435729)Time elapsed: 0.728 s
% 42.54/6.44 % (3435729)Peak memory usage: 126 MB
% 42.54/6.44 % (3435729)Instructions burned: 2217 (million)
% 42.54/6.44 % (3435741)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1127596392:i=1959:rtra=on:fsd=on:proc=on_2958 on theBenchmark for (2958ds/1959Mi)
% 42.54/6.44 % (3435742)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4156975695:s2a=on:i=3553:nm=0:rtra=on_2957 on theBenchmark for (2957ds/3553Mi)
% 42.54/6.44 % (3435739)Instruction limit reached!
% 42.54/6.44 % (3435739)------------------------------
% 42.54/6.44 % (3435739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435739)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435739)Termination reason: Instruction limit
% 42.54/6.44 % (3435739)Termination phase: Saturation
% 42.54/6.44 % (3435739)Time elapsed: 0.594 s
% 42.54/6.44 % (3435739)Peak memory usage: 91 MB
% 42.54/6.44 % (3435739)Instructions burned: 2130 (million)
% 42.54/6.44 % (3435745)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1141611972:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2953 on theBenchmark for (2953ds/3201Mi)
% 42.54/6.44 % (3435741)Instruction limit reached!
% 42.54/6.44 % (3435741)------------------------------
% 42.54/6.44 % (3435741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435741)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435741)Termination reason: Instruction limit
% 42.54/6.44 % (3435741)Termination phase: Saturation
% 42.54/6.44 % (3435741)Time elapsed: 0.612 s
% 42.54/6.44 % (3435741)Peak memory usage: 123 MB
% 42.54/6.44 % (3435741)Instructions burned: 1960 (million)
% 42.54/6.44 % (3435736)Instruction limit reached!
% 42.54/6.44 % (3435736)------------------------------
% 42.54/6.44 % (3435736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435736)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435736)Termination reason: Instruction limit
% 42.54/6.44 % (3435736)Termination phase: Saturation
% 42.54/6.44 % (3435736)Time elapsed: 1.073 s
% 42.54/6.44 % (3435736)Peak memory usage: 108 MB
% 42.54/6.44 % (3435736)Instructions burned: 3511 (million)
% 42.54/6.44 % (3435747)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=2471348403:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2950 on theBenchmark for (2950ds/4093Mi)
% 42.54/6.44 % (3435716)Instruction limit reached!
% 42.54/6.44 % (3435716)------------------------------
% 42.54/6.44 % (3435716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435716)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435716)Termination reason: Instruction limit
% 42.54/6.44 % (3435716)Termination phase: Saturation
% 42.54/6.44 % (3435716)Time elapsed: 1.894 s
% 42.54/6.44 % (3435716)Peak memory usage: 119 MB
% 42.54/6.44 % (3435716)Instructions burned: 6402 (million)
% 42.54/6.44 % (3435748)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=54444007:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2949 on theBenchmark for (2949ds/21173Mi)
% 42.54/6.44 % (3435750)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3349773049:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2949 on theBenchmark for (2949ds/10544Mi)
% 42.54/6.44 % (3435728)Instruction limit reached!
% 42.54/6.44 % (3435728)------------------------------
% 42.54/6.44 % (3435728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435728)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435728)Termination reason: Instruction limit
% 42.54/6.44 % (3435728)Termination phase: Saturation
% 42.54/6.44 % (3435728)Time elapsed: 1.783 s
% 42.54/6.44 % (3435728)Peak memory usage: 133 MB
% 42.54/6.44 % (3435728)Instructions burned: 5814 (million)
% 42.54/6.44 % (3435753)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=820198165:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2946 on theBenchmark for (2946ds/1262Mi)
% 42.54/6.44 % (3435745)Instruction limit reached!
% 42.54/6.44 % (3435745)------------------------------
% 42.54/6.44 % (3435745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435745)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435745)Termination reason: Instruction limit
% 42.54/6.44 % (3435745)Termination phase: Saturation
% 42.54/6.44 % (3435745)Time elapsed: 0.808 s
% 42.54/6.44 % (3435745)Peak memory usage: 92 MB
% 42.54/6.44 % (3435745)Instructions burned: 3204 (million)
% 42.54/6.44 % (3435755)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1301015594:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2944 on theBenchmark for (2944ds/775Mi)
% 42.54/6.44 % (3435742)Instruction limit reached!
% 42.54/6.44 % (3435742)------------------------------
% 42.54/6.44 % (3435742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435742)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435742)Termination reason: Instruction limit
% 42.54/6.44 % (3435742)Termination phase: Saturation
% 42.54/6.44 % (3435742)Time elapsed: 1.320 s
% 42.54/6.44 % (3435742)Peak memory usage: 105 MB
% 42.54/6.44 % (3435742)Instructions burned: 3556 (million)
% 42.54/6.44 % (3435753)Instruction limit reached!
% 42.54/6.44 % (3435753)------------------------------
% 42.54/6.44 % (3435753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435753)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435753)Termination reason: Instruction limit
% 42.54/6.44 % (3435753)Termination phase: Saturation
% 42.54/6.44 % (3435753)Time elapsed: 0.395 s
% 42.54/6.44 % (3435753)Peak memory usage: 124 MB
% 42.54/6.44 % (3435753)Instructions burned: 1263 (million)
% 42.54/6.44 % (3435757)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2131195798:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2942 on theBenchmark for (2942ds/270Mi)
% 42.54/6.44 % (3435747)First to succeed.
% 42.54/6.44 % (3435747)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3435526"
% 42.54/6.44 % (3435757)Instruction limit reached!
% 42.54/6.44 % (3435757)------------------------------
% 42.54/6.44 % (3435757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435757)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435757)Termination reason: Instruction limit
% 42.54/6.44 % (3435757)Termination phase: Saturation
% 42.54/6.44 % (3435757)Time elapsed: 0.099 s
% 42.54/6.44 % (3435757)Peak memory usage: 92 MB
% 42.54/6.44 % (3435757)Instructions burned: 272 (million)
% 42.54/6.44 % (3435759)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2416642435:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2941 on theBenchmark for (2941ds/17165Mi)
% 42.54/6.44 % (3435755)Instruction limit reached!
% 42.54/6.44 % (3435755)------------------------------
% 42.54/6.44 % (3435755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.54/6.44 % (3435755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.54/6.44 % (3435755)CaDiCaL version: 2.1.3
% 42.54/6.44 % (3435755)Termination reason: Instruction limit
% 42.54/6.44 % (3435755)Termination phase: Saturation
% 42.54/6.44 % (3435755)Time elapsed: 0.287 s
% 42.54/6.44 % (3435755)Peak memory usage: 96 MB
% 42.54/6.44 % (3435755)Instructions burned: 775 (million)
% 42.54/6.44 % (3435760)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=225647240:s2a=on:i=13094:s2at=-1:rtra=on_2940 on theBenchmark for (2940ds/13094Mi)
% 42.54/6.44 % (3435747)Refutation found. Thanks to Tanya!
% 42.54/6.44 % SZS status Theorem for theBenchmark
% 42.54/6.44 % SZS output start Proof for theBenchmark
% See solution above
% 43.31/6.54 % (3435747)------------------------------
% 43.31/6.54 % (3435747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.31/6.54 % (3435747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.31/6.54 % (3435747)CaDiCaL version: 2.1.3
% 43.31/6.54 % (3435747)Termination reason: Refutation
% 43.31/6.54 % (3435747)Time elapsed: 0.919 s
% 43.31/6.54 % (3435747)Peak memory usage: 145 MB
% 43.31/6.54 % (3435747)Instructions burned: 2941 (million)
% 43.31/6.54 % (3435747)------------------------------
% 43.31/6.54 % (3435747)------------------------------
% 43.31/6.54 % (3435526)Success in time 6.118 s
% 43.31/6.54 % Vampire exiting
%------------------------------------------------------------------------------