%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW598_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:54 PM UTC 2026
% Result : Theorem 90.30s 13.46s
% Output : Refutation 91.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 106
% Syntax : Number of formulae : 386 ( 57 unt; 0 typ; 96 def)
% Number of atoms : 1688 ( 507 equ)
% Maximal formula atoms : 46 ( 4 avg)
% Number of connectives : 1821 ( 519 ~; 847 |; 244 &)
% ( 87 <=>; 124 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number arithmetic : 1147 ( 389 atm; 245 fun; 265 num; 248 var)
% Number of types : 7 ( 5 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 91 ( 87 usr; 86 prp; 0-2 aty)
% Number of functors : 56 ( 52 usr; 44 con; 0-4 aty)
% Number of variables : 382 ( 319 !; 63 ?; 382 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
tree: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
min: ( $int * $int ) > $int ).
tff(func_def_13,type,
max: ( $int * $int ) > $int ).
tff(func_def_14,type,
tree1: ty ).
tff(func_def_15,type,
empty: tree ).
tff(func_def_16,type,
node: ( tree * $int * tree ) > tree ).
tff(func_def_17,type,
match_tree: ( ty * tree * uni * uni ) > uni ).
tff(func_def_18,type,
node_proj_1: tree > tree ).
tff(func_def_19,type,
node_proj_2: tree > $int ).
tff(func_def_20,type,
node_proj_3: tree > tree ).
tff(func_def_21,type,
size: tree > $int ).
tff(func_def_25,type,
sK0: tree ).
tff(func_def_26,type,
sK1: tree ).
tff(func_def_27,type,
sK2: tree ).
tff(func_def_28,type,
sK3: $int ).
tff(func_def_29,type,
sK4: tree ).
tff(func_def_30,type,
sK5: tree ).
tff(func_def_31,type,
sK6: $int ).
tff(func_def_32,type,
sK7: $int ).
tff(func_def_33,type,
sK8: $int ).
tff(func_def_34,type,
sK9: $int ).
tff(func_def_35,type,
sK10: tree ).
tff(func_def_36,type,
sK11: $int ).
tff(func_def_37,type,
sK12: tree ).
tff(func_def_38,type,
sK13: $int ).
tff(func_def_39,type,
sK14: tree ).
tff(func_def_40,type,
sK15: tree ).
tff(func_def_41,type,
sK16: $int ).
tff(func_def_42,type,
sK17: $int ).
tff(func_def_43,type,
sK18: $int ).
tff(func_def_44,type,
sK19: $int ).
tff(func_def_45,type,
sK20: $int ).
tff(func_def_46,type,
sF21: tree ).
tff(func_def_47,type,
sF22: tree ).
tff(func_def_48,type,
sF23: tree ).
tff(func_def_49,type,
sF24: $int ).
tff(func_def_50,type,
sF25: $int ).
tff(func_def_51,type,
sF26: $int ).
tff(func_def_52,type,
sF27: $int ).
tff(func_def_53,type,
sF28: $int ).
tff(func_def_54,type,
sF29: $int ).
tff(func_def_55,type,
sF30: $int ).
tff(func_def_56,type,
sF31: tree ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( $int * tree ) > $o ).
tff(f9,axiom,
! [X0: $int,X1: $int] :
( $lesseq(X0,max(X0,X1))
& $lesseq(X1,max(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_ge) ).
tff(f10,axiom,
! [X1: $int,X0: $int] :
( ( max(X0,X1) = X0 )
| ( max(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_some) ).
tff(f22,axiom,
! [X2: tree,X1: $int,X0: tree] : ( empty != node(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',empty_Node) ).
tff(f23,axiom,
! [X2: tree,X1: $int,X0: tree] : ( node_proj_1(node(X0,X1,X2)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',node_proj_1_def) ).
tff(f27,axiom,
( ( size(empty) = 0 )
& ! [X2: tree,X0: tree,X1: $int] : ( size(node(X0,X1,X2)) = $sum($sum(1,size(X0)),size(X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',size_def) ).
tff(f28,axiom,
! [X0: tree] : $lesseq(0,size(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',size_nonneg) ).
tff(f29,axiom,
! [X0: $int] :
( ! [X3: tree,X2: $int,X1: tree] :
( ( mem(X0,X1)
| ( X0 = X2 )
| mem(X0,X3) )
<=> mem(X0,node(X1,X2,X3)) )
& ~ mem(X0,empty) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def) ).
tff(f30,conjecture,
! [X0: tree] :
( ( X0 != empty )
=> ( ( ( X0 = empty )
=> $false )
& ! [X2: $int,X1: tree,X3: tree] :
( ( X0 = node(X1,X2,X3) )
=> ( ( ( X3 = empty )
=> ( ! [X6: $int,X7: tree,X5: tree] :
( ( X1 = node(X5,X6,X7) )
=> ( $lesseq(0,size(X0))
& ! [X8: $int] :
( ( ! [X4: $int] :
( mem(X4,X1)
=> $lesseq(X4,X8) )
& mem(X8,X1) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X8,X2)) ) ) )
& $less(size(X1),size(X0))
& ( X1 != empty ) ) )
& ( ( X1 = empty )
=> ( ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,X2) )
& mem(X2,X0) ) ) ) )
& ! [X6: $int,X5: tree,X7: tree] :
( ( X3 = node(X5,X6,X7) )
=> ( ! [X11: tree,X9: tree,X10: $int] :
( ( X1 = node(X9,X10,X11) )
=> ( ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> $lesseq(X4,X8) ) )
=> ( $less(size(X1),size(X0))
& $lesseq(0,size(X0))
& ( X1 != empty )
& ! [X12: $int] :
( ( mem(X12,X1)
& ! [X4: $int] :
( mem(X4,X1)
=> $lesseq(X4,X12) ) )
=> ( mem(max(X12,max(X2,X8)),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X12,max(X2,X8))) ) ) ) ) )
& ( X3 != empty )
& $less(size(X3),size(X0))
& $lesseq(0,size(X0)) ) )
& ( ( X1 = empty )
=> ( ( X3 != empty )
& ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> $lesseq(X4,X8) ) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X8,X2)) ) ) )
& $less(size(X3),size(X0))
& $lesseq(0,size(X0)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_maximum) ).
tff(f31,negated_conjecture,
~ ! [X0: tree] :
( ( X0 != empty )
=> ( ( ( X0 = empty )
=> $false )
& ! [X2: $int,X1: tree,X3: tree] :
( ( X0 = node(X1,X2,X3) )
=> ( ( ( X3 = empty )
=> ( ! [X6: $int,X7: tree,X5: tree] :
( ( X1 = node(X5,X6,X7) )
=> ( $lesseq(0,size(X0))
& ! [X8: $int] :
( ( ! [X4: $int] :
( mem(X4,X1)
=> $lesseq(X4,X8) )
& mem(X8,X1) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X8,X2)) ) ) )
& $less(size(X1),size(X0))
& ( X1 != empty ) ) )
& ( ( X1 = empty )
=> ( ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,X2) )
& mem(X2,X0) ) ) ) )
& ! [X6: $int,X5: tree,X7: tree] :
( ( X3 = node(X5,X6,X7) )
=> ( ! [X11: tree,X9: tree,X10: $int] :
( ( X1 = node(X9,X10,X11) )
=> ( ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> $lesseq(X4,X8) ) )
=> ( $less(size(X1),size(X0))
& $lesseq(0,size(X0))
& ( X1 != empty )
& ! [X12: $int] :
( ( mem(X12,X1)
& ! [X4: $int] :
( mem(X4,X1)
=> $lesseq(X4,X12) ) )
=> ( mem(max(X12,max(X2,X8)),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X12,max(X2,X8))) ) ) ) ) )
& ( X3 != empty )
& $less(size(X3),size(X0))
& $lesseq(0,size(X0)) ) )
& ( ( X1 = empty )
=> ( ( X3 != empty )
& ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> $lesseq(X4,X8) ) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> $lesseq(X4,max(X8,X2)) ) ) )
& $less(size(X3),size(X0))
& $lesseq(0,size(X0)) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
tff(f32,plain,
~ ! [X0: tree] :
( ( X0 != empty )
=> ( ( ( X0 = empty )
=> $false )
& ! [X2: $int,X1: tree,X3: tree] :
( ( X0 = node(X1,X2,X3) )
=> ( ( ( X3 = empty )
=> ( ! [X6: $int,X7: tree,X5: tree] :
( ( X1 = node(X5,X6,X7) )
=> ( ~ $less(size(X0),0)
& ! [X8: $int] :
( ( ! [X4: $int] :
( mem(X4,X1)
=> ~ $less(X8,X4) )
& mem(X8,X1) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> ~ $less(max(X8,X2),X4) ) ) )
& $less(size(X1),size(X0))
& ( X1 != empty ) ) )
& ( ( X1 = empty )
=> ( ! [X4: $int] :
( mem(X4,X0)
=> ~ $less(X2,X4) )
& mem(X2,X0) ) ) ) )
& ! [X6: $int,X5: tree,X7: tree] :
( ( X3 = node(X5,X6,X7) )
=> ( ! [X11: tree,X9: tree,X10: $int] :
( ( X1 = node(X9,X10,X11) )
=> ( ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> ~ $less(X8,X4) ) )
=> ( $less(size(X1),size(X0))
& ~ $less(size(X0),0)
& ( X1 != empty )
& ! [X12: $int] :
( ( mem(X12,X1)
& ! [X4: $int] :
( mem(X4,X1)
=> ~ $less(X12,X4) ) )
=> ( mem(max(X12,max(X2,X8)),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> ~ $less(max(X12,max(X2,X8)),X4) ) ) ) ) )
& ( X3 != empty )
& $less(size(X3),size(X0))
& ~ $less(size(X0),0) ) )
& ( ( X1 = empty )
=> ( ( X3 != empty )
& ! [X8: $int] :
( ( mem(X8,X3)
& ! [X4: $int] :
( mem(X4,X3)
=> ~ $less(X8,X4) ) )
=> ( mem(max(X8,X2),X0)
& ! [X4: $int] :
( mem(X4,X0)
=> ~ $less(max(X8,X2),X4) ) ) )
& $less(size(X3),size(X0))
& ~ $less(size(X0),0) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f31]) ).
tff(f34,plain,
! [X1: $int,X0: $int] :
( ~ $less(max(X0,X1),X0)
& ~ $less(max(X0,X1),X1) ),
inference(theory_normalization,[],[f9]) ).
tff(f39,plain,
! [X0: tree] : ~ $less(size(X0),0),
inference(theory_normalization,[],[f28]) ).
tff(f43,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f44,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum($sum(X0,X1),X2) = $sum(X0,$sum(X1,X2)) ),
introduced(definition,[],[tha_associativity]) ).
tff(f62,plain,
! [X1: $int,X2: tree,X0: tree] : ( node_proj_1(node(X2,X1,X0)) = X2 ),
inference(rectify,[],[f23]) ).
tff(f63,plain,
~ ! [X0: tree] :
( ( X0 != empty )
=> ( ( ( X0 = empty )
=> $false )
& ! [X1: $int,X3: tree,X2: tree] :
( ( node(X2,X1,X3) = X0 )
=> ( ! [X12: tree,X11: $int,X13: tree] :
( ( node(X12,X11,X13) = X3 )
=> ( ( ( empty = X2 )
=> ( ( X3 != empty )
& ~ $less(size(X0),0)
& ! [X22: $int] :
( ( mem(X22,X3)
& ! [X23: $int] :
( mem(X23,X3)
=> ~ $less(X22,X23) ) )
=> ( mem(max(X22,X1),X0)
& ! [X24: $int] :
( mem(X24,X0)
=> ~ $less(max(X22,X1),X24) ) ) )
& $less(size(X3),size(X0)) ) )
& ! [X15: tree,X16: $int,X14: tree] :
( ( node(X15,X16,X14) = X2 )
=> ( ~ $less(size(X0),0)
& ( X3 != empty )
& $less(size(X3),size(X0))
& ! [X17: $int] :
( ( ! [X18: $int] :
( mem(X18,X3)
=> ~ $less(X17,X18) )
& mem(X17,X3) )
=> ( $less(size(X2),size(X0))
& ! [X19: $int] :
( ( ! [X20: $int] :
( mem(X20,X2)
=> ~ $less(X19,X20) )
& mem(X19,X2) )
=> ( mem(max(X19,max(X1,X17)),X0)
& ! [X21: $int] :
( mem(X21,X0)
=> ~ $less(max(X19,max(X1,X17)),X21) ) ) )
& ( empty != X2 )
& ~ $less(size(X0),0) ) ) ) ) ) )
& ( ( X3 = empty )
=> ( ( ( empty = X2 )
=> ( mem(X1,X0)
& ! [X10: $int] :
( mem(X10,X0)
=> ~ $less(X1,X10) ) ) )
& ! [X6: tree,X4: $int,X5: tree] :
( ( node(X6,X4,X5) = X2 )
=> ( ( empty != X2 )
& $less(size(X2),size(X0))
& ! [X7: $int] :
( ( mem(X7,X2)
& ! [X8: $int] :
( mem(X8,X2)
=> ~ $less(X7,X8) ) )
=> ( ! [X9: $int] :
( mem(X9,X0)
=> ~ $less(max(X7,X1),X9) )
& mem(max(X7,X1),X0) ) )
& ~ $less(size(X0),0) ) ) ) ) ) ) ) ),
inference(rectify,[],[f32]) ).
tff(f64,plain,
~ ! [X0: tree] :
( ( X0 != empty )
=> ( ( ( ~ X0 ) = empty )
& ! [X1: $int,X3: tree,X2: tree] :
( ( node(X2,X1,X3) = X0 )
=> ( ! [X12: tree,X11: $int,X13: tree] :
( ( node(X12,X11,X13) = X3 )
=> ( ( ( empty = X2 )
=> ( ( X3 != empty )
& ~ $less(size(X0),0)
& ! [X22: $int] :
( ( mem(X22,X3)
& ! [X23: $int] :
( mem(X23,X3)
=> ~ $less(X22,X23) ) )
=> ( mem(max(X22,X1),X0)
& ! [X24: $int] :
( mem(X24,X0)
=> ~ $less(max(X22,X1),X24) ) ) )
& $less(size(X3),size(X0)) ) )
& ! [X15: tree,X16: $int,X14: tree] :
( ( node(X15,X16,X14) = X2 )
=> ( ~ $less(size(X0),0)
& ( X3 != empty )
& $less(size(X3),size(X0))
& ! [X17: $int] :
( ( ! [X18: $int] :
( mem(X18,X3)
=> ~ $less(X17,X18) )
& mem(X17,X3) )
=> ( $less(size(X2),size(X0))
& ! [X19: $int] :
( ( ! [X20: $int] :
( mem(X20,X2)
=> ~ $less(X19,X20) )
& mem(X19,X2) )
=> ( mem(max(X19,max(X1,X17)),X0)
& ! [X21: $int] :
( mem(X21,X0)
=> ~ $less(max(X19,max(X1,X17)),X21) ) ) )
& ( empty != X2 )
& ~ $less(size(X0),0) ) ) ) ) ) )
& ( ( X3 = empty )
=> ( ( ( empty = X2 )
=> ( mem(X1,X0)
& ! [X10: $int] :
( mem(X10,X0)
=> ~ $less(X1,X10) ) ) )
& ! [X6: tree,X4: $int,X5: tree] :
( ( node(X6,X4,X5) = X2 )
=> ( ( empty != X2 )
& $less(size(X2),size(X0))
& ! [X7: $int] :
( ( mem(X7,X2)
& ! [X8: $int] :
( mem(X8,X2)
=> ~ $less(X7,X8) ) )
=> ( ! [X9: $int] :
( mem(X9,X0)
=> ~ $less(max(X7,X1),X9) )
& mem(max(X7,X1),X0) ) )
& ~ $less(size(X0),0) ) ) ) ) ) ) ) ),
inference(true_and_false_elimination,[],[f63]) ).
tff(f65,plain,
~ ! [X0: tree] :
( ( X0 != empty )
=> ( ( empty != X0 )
& ! [X1: $int,X3: tree,X2: tree] :
( ( node(X2,X1,X3) = X0 )
=> ( ! [X12: tree,X11: $int,X13: tree] :
( ( node(X12,X11,X13) = X3 )
=> ( ( ( empty = X2 )
=> ( ( X3 != empty )
& ~ $less(size(X0),0)
& ! [X22: $int] :
( ( mem(X22,X3)
& ! [X23: $int] :
( mem(X23,X3)
=> ~ $less(X22,X23) ) )
=> ( mem(max(X22,X1),X0)
& ! [X24: $int] :
( mem(X24,X0)
=> ~ $less(max(X22,X1),X24) ) ) )
& $less(size(X3),size(X0)) ) )
& ! [X15: tree,X16: $int,X14: tree] :
( ( node(X15,X16,X14) = X2 )
=> ( ~ $less(size(X0),0)
& ( X3 != empty )
& $less(size(X3),size(X0))
& ! [X17: $int] :
( ( ! [X18: $int] :
( mem(X18,X3)
=> ~ $less(X17,X18) )
& mem(X17,X3) )
=> ( $less(size(X2),size(X0))
& ! [X19: $int] :
( ( ! [X20: $int] :
( mem(X20,X2)
=> ~ $less(X19,X20) )
& mem(X19,X2) )
=> ( mem(max(X19,max(X1,X17)),X0)
& ! [X21: $int] :
( mem(X21,X0)
=> ~ $less(max(X19,max(X1,X17)),X21) ) ) )
& ( empty != X2 )
& ~ $less(size(X0),0) ) ) ) ) ) )
& ( ( X3 = empty )
=> ( ( ( empty = X2 )
=> ( mem(X1,X0)
& ! [X10: $int] :
( mem(X10,X0)
=> ~ $less(X1,X10) ) ) )
& ! [X6: tree,X4: $int,X5: tree] :
( ( node(X6,X4,X5) = X2 )
=> ( ( empty != X2 )
& $less(size(X2),size(X0))
& ! [X7: $int] :
( ( mem(X7,X2)
& ! [X8: $int] :
( mem(X8,X2)
=> ~ $less(X7,X8) ) )
=> ( ! [X9: $int] :
( mem(X9,X0)
=> ~ $less(max(X7,X1),X9) )
& mem(max(X7,X1),X0) ) )
& ~ $less(size(X0),0) ) ) ) ) ) ) ) ),
inference(flattening,[],[f64]) ).
tff(f67,plain,
( ! [X2: $int,X0: tree,X1: tree] : ( size(node(X1,X2,X0)) = $sum($sum(1,size(X1)),size(X0)) )
& ( size(empty) = 0 ) ),
inference(rectify,[],[f27]) ).
tff(f69,plain,
! [X0: $int] :
( ! [X3: tree,X2: $int,X1: tree] :
( mem(X0,node(X3,X2,X1))
<=> ( mem(X0,X1)
| ( X0 = X2 )
| mem(X0,X3) ) )
& ~ mem(X0,empty) ),
inference(rectify,[],[f29]) ).
tff(f87,plain,
? [X0: tree] :
( ( ( empty = X0 )
| ? [X1: $int,X3: tree,X2: tree] :
( ( ? [X12: tree,X11: $int,X13: tree] :
( ( ( ( ( empty = X3 )
| $less(size(X0),0)
| ? [X22: $int] :
( ( ? [X24: $int] :
( mem(X24,X0)
& $less(max(X22,X1),X24) )
| ~ mem(max(X22,X1),X0) )
& mem(X22,X3)
& ! [X23: $int] :
( ~ mem(X23,X3)
| ~ $less(X22,X23) ) )
| ~ $less(size(X3),size(X0)) )
& ( empty = X2 ) )
| ? [X15: tree,X16: $int,X14: tree] :
( ( $less(size(X0),0)
| ( empty = X3 )
| ~ $less(size(X3),size(X0))
| ? [X17: $int] :
( ( ~ $less(size(X2),size(X0))
| ? [X19: $int] :
( ( ~ mem(max(X19,max(X1,X17)),X0)
| ? [X21: $int] :
( $less(max(X19,max(X1,X17)),X21)
& mem(X21,X0) ) )
& ! [X20: $int] :
( ~ mem(X20,X2)
| ~ $less(X19,X20) )
& mem(X19,X2) )
| ( empty = X2 )
| $less(size(X0),0) )
& ! [X18: $int] :
( ~ $less(X17,X18)
| ~ mem(X18,X3) )
& mem(X17,X3) ) )
& ( node(X15,X16,X14) = X2 ) ) )
& ( node(X12,X11,X13) = X3 ) )
| ( ( ( ( ? [X10: $int] :
( mem(X10,X0)
& $less(X1,X10) )
| ~ mem(X1,X0) )
& ( empty = X2 ) )
| ? [X6: tree,X4: $int,X5: tree] :
( ( ( empty = X2 )
| ~ $less(size(X2),size(X0))
| ? [X7: $int] :
( ( ~ mem(max(X7,X1),X0)
| ? [X9: $int] :
( $less(max(X7,X1),X9)
& mem(X9,X0) ) )
& mem(X7,X2)
& ! [X8: $int] :
( ~ mem(X8,X2)
| ~ $less(X7,X8) ) )
| $less(size(X0),0) )
& ( node(X6,X4,X5) = X2 ) ) )
& ( X3 = empty ) ) )
& ( node(X2,X1,X3) = X0 ) ) )
& ( X0 != empty ) ),
inference(ennf_transformation,[],[f65]) ).
tff(f88,plain,
? [X0: tree] :
( ( ( empty = X0 )
| ? [X2: tree,X3: tree,X1: $int] :
( ( node(X2,X1,X3) = X0 )
& ( ( ( X3 = empty )
& ( ? [X5: tree,X6: tree,X4: $int] :
( ( ( empty = X2 )
| $less(size(X0),0)
| ~ $less(size(X2),size(X0))
| ? [X7: $int] :
( ( ~ mem(max(X7,X1),X0)
| ? [X9: $int] :
( $less(max(X7,X1),X9)
& mem(X9,X0) ) )
& mem(X7,X2)
& ! [X8: $int] :
( ~ mem(X8,X2)
| ~ $less(X7,X8) ) ) )
& ( node(X6,X4,X5) = X2 ) )
| ( ( ? [X10: $int] :
( mem(X10,X0)
& $less(X1,X10) )
| ~ mem(X1,X0) )
& ( empty = X2 ) ) ) )
| ? [X13: tree,X11: $int,X12: tree] :
( ( node(X12,X11,X13) = X3 )
& ( ? [X16: $int,X14: tree,X15: tree] :
( ( node(X15,X16,X14) = X2 )
& ( ( empty = X3 )
| ~ $less(size(X3),size(X0))
| ? [X17: $int] :
( mem(X17,X3)
& ( ? [X19: $int] :
( mem(X19,X2)
& ! [X20: $int] :
( ~ mem(X20,X2)
| ~ $less(X19,X20) )
& ( ~ mem(max(X19,max(X1,X17)),X0)
| ? [X21: $int] :
( $less(max(X19,max(X1,X17)),X21)
& mem(X21,X0) ) ) )
| ( empty = X2 )
| ~ $less(size(X2),size(X0))
| $less(size(X0),0) )
& ! [X18: $int] :
( ~ $less(X17,X18)
| ~ mem(X18,X3) ) )
| $less(size(X0),0) ) )
| ( ( ( empty = X3 )
| ? [X22: $int] :
( ( ? [X24: $int] :
( mem(X24,X0)
& $less(max(X22,X1),X24) )
| ~ mem(max(X22,X1),X0) )
& mem(X22,X3)
& ! [X23: $int] :
( ~ mem(X23,X3)
| ~ $less(X22,X23) ) )
| $less(size(X0),0)
| ~ $less(size(X3),size(X0)) )
& ( empty = X2 ) ) ) ) ) ) )
& ( X0 != empty ) ),
inference(flattening,[],[f87]) ).
tff(f97,plain,
! [X0: $int] :
( ! [X3: tree,X2: $int,X1: tree] :
( ( mem(X0,node(X3,X2,X1))
| ( ~ mem(X0,X1)
& ( X0 != X2 )
& ~ mem(X0,X3) ) )
& ( mem(X0,X1)
| ( X0 = X2 )
| mem(X0,X3)
| ~ mem(X0,node(X3,X2,X1)) ) )
& ~ mem(X0,empty) ),
inference(nnf_transformation,[],[f69]) ).
tff(f98,plain,
! [X0: $int] :
( ! [X3: tree,X2: $int,X1: tree] :
( ( mem(X0,node(X3,X2,X1))
| ( ~ mem(X0,X1)
& ( X0 != X2 )
& ~ mem(X0,X3) ) )
& ( mem(X0,X1)
| ( X0 = X2 )
| mem(X0,X3)
| ~ mem(X0,node(X3,X2,X1)) ) )
& ~ mem(X0,empty) ),
inference(flattening,[],[f97]) ).
tff(f99,plain,
! [X0: $int] :
( ! [X1: tree,X2: $int,X3: tree] :
( ( mem(X0,node(X1,X2,X3))
| ( ~ mem(X0,X3)
& ( X0 != X2 )
& ~ mem(X0,X1) ) )
& ( mem(X0,X3)
| ( X0 = X2 )
| mem(X0,X1)
| ~ mem(X0,node(X1,X2,X3)) ) )
& ~ mem(X0,empty) ),
inference(rectify,[],[f98]) ).
tff(f101,plain,
! [X0: tree,X1: $int,X2: tree] : ( empty != node(X2,X1,X0) ),
inference(rectify,[],[f22]) ).
tff(f102,plain,
! [X0: $int,X1: $int] :
( ~ $less(max(X1,X0),X1)
& ~ $less(max(X1,X0),X0) ),
inference(rectify,[],[f34]) ).
tff(f103,plain,
( ! [X0: $int,X1: tree,X2: tree] : ( size(node(X2,X0,X1)) = $sum($sum(1,size(X2)),size(X1)) )
& ( size(empty) = 0 ) ),
inference(rectify,[],[f67]) ).
tff(f104,plain,
? [X0: tree] :
( ( ( empty = X0 )
| ? [X1: tree,X2: tree,X3: $int] :
( ( node(X1,X3,X2) = X0 )
& ( ( ( empty = X2 )
& ( ? [X4: tree,X5: tree,X6: $int] :
( ( ( empty = X1 )
| $less(size(X0),0)
| ~ $less(size(X1),size(X0))
| ? [X7: $int] :
( ( ~ mem(max(X7,X3),X0)
| ? [X8: $int] :
( $less(max(X7,X3),X8)
& mem(X8,X0) ) )
& mem(X7,X1)
& ! [X9: $int] :
( ~ mem(X9,X1)
| ~ $less(X7,X9) ) ) )
& ( node(X5,X6,X4) = X1 ) )
| ( ( ? [X10: $int] :
( mem(X10,X0)
& $less(X3,X10) )
| ~ mem(X3,X0) )
& ( empty = X1 ) ) ) )
| ? [X11: tree,X12: $int,X13: tree] :
( ( node(X13,X12,X11) = X2 )
& ( ? [X14: $int,X15: tree,X16: tree] :
( ( node(X16,X14,X15) = X1 )
& ( ( empty = X2 )
| ~ $less(size(X2),size(X0))
| ? [X17: $int] :
( mem(X17,X2)
& ( ? [X18: $int] :
( mem(X18,X1)
& ! [X19: $int] :
( ~ mem(X19,X1)
| ~ $less(X18,X19) )
& ( ~ mem(max(X18,max(X3,X17)),X0)
| ? [X20: $int] :
( $less(max(X18,max(X3,X17)),X20)
& mem(X20,X0) ) ) )
| ( empty = X1 )
| ~ $less(size(X1),size(X0))
| $less(size(X0),0) )
& ! [X21: $int] :
( ~ $less(X17,X21)
| ~ mem(X21,X2) ) )
| $less(size(X0),0) ) )
| ( ( ( empty = X2 )
| ? [X22: $int] :
( ( ? [X23: $int] :
( mem(X23,X0)
& $less(max(X22,X3),X23) )
| ~ mem(max(X22,X3),X0) )
& mem(X22,X2)
& ! [X24: $int] :
( ~ mem(X24,X2)
| ~ $less(X22,X24) ) )
| $less(size(X0),0)
| ~ $less(size(X2),size(X0)) )
& ( empty = X1 ) ) ) ) ) ) )
& ( X0 != empty ) ),
inference(rectify,[],[f88]) ).
tff(f105,plain,
( ( ( empty = sK0 )
| ( ( sK0 = node(sK1,sK3,sK2) )
& ( ( ( empty = sK2 )
& ( ( ( ( empty = sK1 )
| $less(size(sK0),0)
| ~ $less(size(sK1),size(sK0))
| ( ( ~ mem(max(sK7,sK3),sK0)
| ( $less(max(sK7,sK3),sK8)
& mem(sK8,sK0) ) )
& mem(sK7,sK1)
& ! [X9: $int] :
( ~ mem(X9,sK1)
| ~ $less(sK7,X9) ) ) )
& ( sK1 = node(sK5,sK6,sK4) ) )
| ( ( ( mem(sK9,sK0)
& $less(sK3,sK9) )
| ~ mem(sK3,sK0) )
& ( empty = sK1 ) ) ) )
| ( ( sK2 = node(sK12,sK11,sK10) )
& ( ( ( sK1 = node(sK15,sK13,sK14) )
& ( ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| ( mem(sK16,sK2)
& ( ( mem(sK17,sK1)
& ! [X19: $int] :
( ~ mem(X19,sK1)
| ~ $less(sK17,X19) )
& ( ~ mem(max(sK17,max(sK3,sK16)),sK0)
| ( $less(max(sK17,max(sK3,sK16)),sK18)
& mem(sK18,sK0) ) ) )
| ( empty = sK1 )
| ~ $less(size(sK1),size(sK0))
| $less(size(sK0),0) )
& ! [X21: $int] :
( ~ $less(sK16,X21)
| ~ mem(X21,sK2) ) )
| $less(size(sK0),0) ) )
| ( ( ( empty = sK2 )
| ( ( ( mem(sK20,sK0)
& $less(max(sK19,sK3),sK20) )
| ~ mem(max(sK19,sK3),sK0) )
& mem(sK19,sK2)
& ! [X24: $int] :
( ~ mem(X24,sK2)
| ~ $less(sK19,X24) ) )
| $less(size(sK0),0)
| ~ $less(size(sK2),size(sK0)) )
& ( empty = sK1 ) ) ) ) ) ) )
& ( empty != sK0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X10,sK9),skolemize(X11,sK10),skolemize(X12,sK11),skolemize(X13,sK12),skolemize(X14,sK13),skolemize(X15,sK14),skolemize(X16,sK15),skolemize(X17,sK16),skolemize(X18,sK17),skolemize(X20,sK18),skolemize(X22,sK19),skolemize(X23,sK20)],[f104]) ).
tff(f106,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| ( max(X1,X0) = X0 ) ),
inference(rectify,[],[f10]) ).
tff(f108,plain,
! [X0: $int,X1: tree,X2: tree] : ( node_proj_1(node(X1,X0,X2)) = X1 ),
inference(rectify,[],[f62]) ).
tff(f118,plain,
! [X0: tree] : ~ $less(size(X0),0),
inference(cnf_transformation,[],[f39]) ).
tff(f124,plain,
! [X0: $int] : ~ mem(X0,empty),
inference(cnf_transformation,[],[f99]) ).
tff(f125,plain,
! [X2: $int,X3: tree,X0: $int,X1: tree] :
( ~ mem(X0,node(X1,X2,X3))
| mem(X0,X1)
| ( X0 = X2 )
| mem(X0,X3) ),
inference(cnf_transformation,[],[f99]) ).
tff(f126,plain,
! [X2: $int,X3: tree,X0: $int,X1: tree] :
( mem(X0,node(X1,X2,X3))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f99]) ).
tff(f127,plain,
! [X2: $int,X3: tree,X0: $int,X1: tree] :
( mem(X0,node(X1,X2,X3))
| ( X0 != X2 ) ),
inference(cnf_transformation,[],[f99]) ).
tff(f128,plain,
! [X2: $int,X3: tree,X0: $int,X1: tree] :
( mem(X0,node(X1,X2,X3))
| ~ mem(X0,X3) ),
inference(cnf_transformation,[],[f99]) ).
tff(f130,plain,
! [X2: tree,X0: tree,X1: $int] : ( empty != node(X2,X1,X0) ),
inference(cnf_transformation,[],[f101]) ).
tff(f133,plain,
! [X0: $int,X1: $int] : ~ $less(max(X1,X0),X0),
inference(cnf_transformation,[],[f102]) ).
tff(f134,plain,
! [X0: $int,X1: $int] : ~ $less(max(X1,X0),X1),
inference(cnf_transformation,[],[f102]) ).
tff(f136,plain,
! [X2: tree,X0: $int,X1: tree] : ( size(node(X2,X0,X1)) = $sum($sum(1,size(X2)),size(X1)) ),
inference(cnf_transformation,[],[f103]) ).
tff(f137,plain,
empty != sK0,
inference(cnf_transformation,[],[f105]) ).
tff(f209,plain,
( ( empty = sK0 )
| ( sK1 = node(sK5,sK6,sK4) )
| $less(sK3,sK9)
| ~ mem(sK3,sK0)
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f245,plain,
( ( empty = sK0 )
| ( sK1 = node(sK5,sK6,sK4) )
| mem(sK9,sK0)
| ~ mem(sK3,sK0)
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f281,plain,
! [X9: $int] :
( ( empty = sK0 )
| ( empty = sK1 )
| $less(size(sK0),0)
| ~ $less(size(sK1),size(sK0))
| ~ mem(X9,sK1)
| ~ $less(sK7,X9)
| ( empty = sK1 )
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f389,plain,
( ( empty = sK0 )
| ( empty = sK1 )
| $less(size(sK0),0)
| ~ $less(size(sK1),size(sK0))
| mem(sK7,sK1)
| ( empty = sK1 )
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f497,plain,
( ( empty = sK0 )
| ( empty = sK1 )
| $less(size(sK0),0)
| ~ $less(size(sK1),size(sK0))
| ~ mem(max(sK7,sK3),sK0)
| mem(sK8,sK0)
| ( empty = sK1 )
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f605,plain,
( ( empty = sK0 )
| ( empty = sK1 )
| $less(size(sK0),0)
| ~ $less(size(sK1),size(sK0))
| ~ mem(max(sK7,sK3),sK0)
| $less(max(sK7,sK3),sK8)
| ( empty = sK1 )
| ( sK2 = node(sK12,sK11,sK10) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f678,plain,
! [X21: $int] :
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| ~ $less(sK16,X21)
| ~ mem(X21,sK2)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f683,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| ~ mem(max(sK17,max(sK3,sK16)),sK0)
| mem(sK18,sK0)
| ( empty = sK1 )
| ~ $less(size(sK1),size(sK0))
| $less(size(sK0),0)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f688,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| ~ mem(max(sK17,max(sK3,sK16)),sK0)
| $less(max(sK17,max(sK3,sK16)),sK18)
| ( empty = sK1 )
| ~ $less(size(sK1),size(sK0))
| $less(size(sK0),0)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f693,plain,
! [X19: $int] :
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| ~ mem(X19,sK1)
| ~ $less(sK17,X19)
| ( empty = sK1 )
| ~ $less(size(sK1),size(sK0))
| $less(size(sK0),0)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f698,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| mem(sK17,sK1)
| ( empty = sK1 )
| ~ $less(size(sK1),size(sK0))
| $less(size(sK0),0)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f703,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(size(sK2),size(sK0))
| mem(sK16,sK2)
| $less(size(sK0),0)
| ( empty = sK1 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f709,plain,
! [X24: $int] :
( ( empty = sK0 )
| ( empty = sK2 )
| ( sK1 = node(sK15,sK13,sK14) )
| ( empty = sK2 )
| ~ mem(X24,sK2)
| ~ $less(sK19,X24)
| $less(size(sK0),0)
| ~ $less(size(sK2),size(sK0)) ),
inference(cnf_transformation,[],[f105]) ).
tff(f710,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( sK1 = node(sK15,sK13,sK14) )
| ( empty = sK2 )
| mem(sK19,sK2)
| $less(size(sK0),0)
| ~ $less(size(sK2),size(sK0)) ),
inference(cnf_transformation,[],[f105]) ).
tff(f711,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( sK1 = node(sK15,sK13,sK14) )
| ( empty = sK2 )
| $less(max(sK19,sK3),sK20)
| ~ mem(max(sK19,sK3),sK0)
| $less(size(sK0),0)
| ~ $less(size(sK2),size(sK0)) ),
inference(cnf_transformation,[],[f105]) ).
tff(f712,plain,
( ( empty = sK0 )
| ( empty = sK2 )
| ( sK1 = node(sK15,sK13,sK14) )
| ( empty = sK2 )
| mem(sK20,sK0)
| ~ mem(max(sK19,sK3),sK0)
| $less(size(sK0),0)
| ~ $less(size(sK2),size(sK0)) ),
inference(cnf_transformation,[],[f105]) ).
tff(f714,plain,
( ( empty = sK0 )
| ( sK0 = node(sK1,sK3,sK2) ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f716,plain,
! [X0: $int,X1: $int] :
( ( max(X1,X0) = X1 )
| ( max(X1,X0) = X0 ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f720,plain,
! [X2: tree,X0: $int,X1: tree] : ( node_proj_1(node(X1,X0,X2)) = X1 ),
inference(cnf_transformation,[],[f108]) ).
tff(f727,plain,
! [X2: $int,X3: tree,X1: tree] : mem(X2,node(X1,X2,X3)),
inference(equality_resolution,[],[f127]) ).
tff(f729,definition,
sF21 = node(sK1,sK3,sK2),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f730,plain,
( ( empty = sK0 )
| ( sF21 = sK0 ) ),
inference(definition_folding,[],[f714,f729]) ).
tff(f731,definition,
sF22 = node(sK12,sK11,sK10),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f732,plain,
node(sK12,sK11,sK10) = sF22,
inference(reorient_equations,[],[f731]) ).
tff(f734,definition,
sF23 = node(sK15,sK13,sK14),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f735,definition,
sF24 = max(sK19,sK3),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f736,plain,
max(sK19,sK3) = sF24,
inference(reorient_equations,[],[f735]) ).
tff(f737,definition,
sF25 = size(sK0),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f738,definition,
sF26 = size(sK2),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f739,plain,
( ~ mem(sF24,sK0)
| ( sF23 = sK1 )
| ( empty = sK2 )
| $less(sF25,0)
| mem(sK20,sK0)
| ~ $less(sF26,sF25)
| ( empty = sK2 )
| ( empty = sK0 ) ),
inference(definition_folding,[],[f712,f737,f738,f737,f736,f734]) ).
tff(f740,plain,
( ( empty = sK2 )
| ( sF23 = sK1 )
| $less(sF25,0)
| ~ $less(sF26,sF25)
| ( empty = sK0 )
| ~ mem(sF24,sK0)
| $less(sF24,sK20)
| ( empty = sK2 ) ),
inference(definition_folding,[],[f711,f737,f738,f737,f736,f736,f734]) ).
tff(f741,plain,
( ( empty = sK0 )
| $less(sF25,0)
| ( empty = sK2 )
| ( sF23 = sK1 )
| ( empty = sK2 )
| ~ $less(sF26,sF25)
| mem(sK19,sK2) ),
inference(definition_folding,[],[f710,f737,f738,f737,f734]) ).
tff(f742,plain,
! [X24: $int] :
( ~ mem(X24,sK2)
| ( empty = sK2 )
| ( sF23 = sK1 )
| ( empty = sK2 )
| ~ $less(sK19,X24)
| ( empty = sK0 )
| ~ $less(sF26,sF25)
| $less(sF25,0) ),
inference(definition_folding,[],[f709,f737,f738,f737,f734]) ).
tff(f748,plain,
( ~ $less(sF26,sF25)
| mem(sK16,sK2)
| ( empty = sK1 )
| $less(sF25,0)
| ( empty = sK2 )
| ( empty = sK2 )
| ( empty = sK0 ) ),
inference(definition_folding,[],[f703,f737,f737,f738]) ).
tff(f749,definition,
sF27 = size(sK1),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f750,plain,
size(sK1) = sF27,
inference(reorient_equations,[],[f749]) ).
tff(f755,plain,
( ( empty = sK2 )
| ( empty = sK2 )
| $less(sF25,0)
| ~ $less(sF26,sF25)
| $less(sF25,0)
| ( empty = sK1 )
| mem(sK17,sK1)
| ( empty = sK1 )
| ( empty = sK0 )
| ~ $less(sF27,sF25) ),
inference(definition_folding,[],[f698,f737,f737,f737,f750,f737,f738]) ).
tff(f760,plain,
! [X19: $int] :
( $less(sF25,0)
| ( empty = sK2 )
| ~ $less(sF26,sF25)
| ~ mem(X19,sK1)
| ( empty = sK2 )
| ~ $less(sK17,X19)
| $less(sF25,0)
| ( empty = sK0 )
| ~ $less(sF27,sF25)
| ( empty = sK1 )
| ( empty = sK1 ) ),
inference(definition_folding,[],[f693,f737,f737,f737,f750,f737,f738]) ).
tff(f761,definition,
sF28 = max(sK3,sK16),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f762,plain,
max(sK3,sK16) = sF28,
inference(reorient_equations,[],[f761]) ).
tff(f763,definition,
sF29 = max(sK17,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f764,plain,
max(sK17,sF28) = sF29,
inference(reorient_equations,[],[f763]) ).
tff(f769,plain,
( ~ $less(sF27,sF25)
| $less(sF25,0)
| ( empty = sK1 )
| $less(sF25,0)
| ( empty = sK1 )
| $less(sF29,sK18)
| ~ mem(sF29,sK0)
| ( empty = sK2 )
| ~ $less(sF26,sF25)
| ( empty = sK2 )
| ( empty = sK0 ) ),
inference(definition_folding,[],[f688,f737,f737,f737,f750,f764,f762,f764,f762,f737,f738]) ).
tff(f774,plain,
( mem(sK18,sK0)
| $less(sF25,0)
| ( empty = sK0 )
| ~ $less(sF26,sF25)
| ( empty = sK2 )
| ( empty = sK2 )
| ~ $less(sF27,sF25)
| $less(sF25,0)
| ~ mem(sF29,sK0)
| ( empty = sK1 )
| ( empty = sK1 ) ),
inference(definition_folding,[],[f683,f737,f737,f737,f750,f764,f762,f737,f738]) ).
tff(f779,plain,
! [X21: $int] :
( ~ $less(sK16,X21)
| ~ $less(sF26,sF25)
| ( empty = sK1 )
| ~ mem(X21,sK2)
| ( empty = sK2 )
| ( empty = sK2 )
| ( empty = sK0 )
| $less(sF25,0) ),
inference(definition_folding,[],[f678,f737,f737,f738]) ).
tff(f780,definition,
sF30 = max(sK7,sK3),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f781,plain,
max(sK7,sK3) = sF30,
inference(reorient_equations,[],[f780]) ).
tff(f854,plain,
( $less(sF30,sK8)
| $less(sF25,0)
| ( empty = sK1 )
| ~ mem(sF30,sK0)
| ( empty = sK1 )
| ( sK2 = sF22 )
| ( empty = sK0 )
| ~ $less(sF27,sF25) ),
inference(definition_folding,[],[f605,f732,f781,f781,f737,f750,f737]) ).
tff(f962,plain,
( ( empty = sK0 )
| ( empty = sK1 )
| mem(sK8,sK0)
| $less(sF25,0)
| ( sK2 = sF22 )
| ( empty = sK1 )
| ~ $less(sF27,sF25)
| ~ mem(sF30,sK0) ),
inference(definition_folding,[],[f497,f732,f781,f737,f750,f737]) ).
tff(f1070,plain,
( ~ $less(sF27,sF25)
| ( empty = sK1 )
| ( sK2 = sF22 )
| ( empty = sK1 )
| ( empty = sK0 )
| $less(sF25,0)
| mem(sK7,sK1) ),
inference(definition_folding,[],[f389,f732,f737,f750,f737]) ).
tff(f1178,plain,
! [X9: $int] :
( $less(sF25,0)
| ( empty = sK0 )
| ( sK2 = sF22 )
| ~ $less(sF27,sF25)
| ( empty = sK1 )
| ~ mem(X9,sK1)
| ( empty = sK1 )
| ~ $less(sK7,X9) ),
inference(definition_folding,[],[f281,f732,f737,f750,f737]) ).
tff(f1214,definition,
sF31 = node(sK5,sK6,sK4),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f1215,plain,
node(sK5,sK6,sK4) = sF31,
inference(reorient_equations,[],[f1214]) ).
tff(f1216,plain,
( ( sK2 = sF22 )
| ~ mem(sK3,sK0)
| ( empty = sK0 )
| ( sK1 = sF31 )
| mem(sK9,sK0) ),
inference(definition_folding,[],[f245,f732,f1215]) ).
tff(f1252,plain,
( ( empty = sK0 )
| ~ mem(sK3,sK0)
| $less(sK3,sK9)
| ( sK1 = sF31 )
| ( sK2 = sF22 ) ),
inference(definition_folding,[],[f209,f732,f1215]) ).
tff(f1396,plain,
! [X24: $int] :
( ~ $less(sF26,sF25)
| ~ $less(sK19,X24)
| ( empty = sK0 )
| $less(sF25,0)
| ( empty = sK2 )
| ( sF23 = sK1 )
| ~ mem(X24,sK2) ),
inference(duplicate_literal_removal,[],[f742]) ).
tff(f1397,plain,
! [X24: $int] :
( $less(0,$uminus(sF25))
| ( empty = sK0 )
| ( empty = sK2 )
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| ~ mem(X24,sK2)
| $less(0,$sum($sum(sK19,1),$uminus(X24)))
| ( sF23 = sK1 ) ),
inference(evaluation,[],[f1396]) ).
tff(f1447,plain,
! [X19: $int] :
( ~ $less(sF27,sF25)
| ( empty = sK1 )
| ~ $less(sK17,X19)
| ~ $less(sF26,sF25)
| ~ mem(X19,sK1)
| ( empty = sK0 )
| ( empty = sK2 )
| $less(sF25,0) ),
inference(duplicate_literal_removal,[],[f760]) ).
tff(f1448,plain,
! [X19: $int] :
( $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| ~ mem(X19,sK1)
| $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| ( empty = sK0 )
| $less(0,$sum($sum(sK17,1),$uminus(X19)))
| ( empty = sK2 )
| ( empty = sK1 )
| $less(0,$uminus(sF25)) ),
inference(evaluation,[],[f1447]) ).
tff(f1476,plain,
( ( empty = sK2 )
| $less(sF25,0)
| $less(sF24,sK20)
| ~ mem(sF24,sK0)
| ( empty = sK0 )
| ( sF23 = sK1 )
| ~ $less(sF26,sF25) ),
inference(duplicate_literal_removal,[],[f740]) ).
tff(f1477,plain,
( $less(0,$sum(sK20,$uminus(sF24)))
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| ( empty = sK0 )
| $less(0,$uminus(sF25))
| ( empty = sK2 )
| ( sF23 = sK1 )
| ~ mem(sF24,sK0) ),
inference(evaluation,[],[f1476]) ).
tff(f1568,plain,
( $less(sF25,0)
| ( empty = sK0 )
| ~ mem(sF30,sK0)
| ( sK2 = sF22 )
| ( empty = sK1 )
| $less(sF30,sK8)
| ~ $less(sF27,sF25) ),
inference(duplicate_literal_removal,[],[f854]) ).
tff(f1569,plain,
( ( empty = sK0 )
| ( sK2 = sF22 )
| ~ mem(sF30,sK0)
| $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| $less(0,$uminus(sF25))
| ( empty = sK1 )
| $less(0,$sum(sK8,$uminus(sF30))) ),
inference(evaluation,[],[f1568]) ).
tff(f1604,plain,
! [X0: $int,X1: $int] : $less(0,$sum($sum(max(X1,X0),1),$uminus(X0))),
inference(evaluation,[],[f133]) ).
tff(f1695,plain,
! [X21: $int] :
( ~ $less(sF26,sF25)
| $less(sF25,0)
| ( empty = sK1 )
| ~ mem(X21,sK2)
| ~ $less(sK16,X21)
| ( empty = sK2 )
| ( empty = sK0 ) ),
inference(duplicate_literal_removal,[],[f779]) ).
tff(f1696,plain,
! [X21: $int] :
( ( empty = sK0 )
| ~ mem(X21,sK2)
| $less(0,$sum($sum(sK16,1),$uminus(X21)))
| $less(0,$uminus(sF25))
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| ( empty = sK1 )
| ( empty = sK2 ) ),
inference(evaluation,[],[f1695]) ).
tff(f1815,plain,
( ~ $less(sF27,sF25)
| ( sK2 = sF22 )
| mem(sK7,sK1)
| ( empty = sK1 )
| ( empty = sK0 )
| $less(sF25,0) ),
inference(duplicate_literal_removal,[],[f1070]) ).
tff(f1816,plain,
( $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| ( sK2 = sF22 )
| ( empty = sK1 )
| $less(0,$uminus(sF25))
| ( empty = sK0 )
| mem(sK7,sK1) ),
inference(evaluation,[],[f1815]) ).
tff(f1937,plain,
( $less(sF25,0)
| ( empty = sK1 )
| ~ mem(sF29,sK0)
| ~ $less(sF27,sF25)
| ( empty = sK0 )
| ~ $less(sF26,sF25)
| ( empty = sK2 )
| $less(sF29,sK18) ),
inference(duplicate_literal_removal,[],[f769]) ).
tff(f1938,plain,
( ( empty = sK1 )
| $less(0,$sum(sK18,$uminus(sF29)))
| ( empty = sK2 )
| ( empty = sK0 )
| ~ mem(sF29,sK0)
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| $less(0,$uminus(sF25)) ),
inference(evaluation,[],[f1937]) ).
tff(f1978,plain,
( ( empty = sK2 )
| ~ $less(sF26,sF25)
| ( empty = sK0 )
| ( sF23 = sK1 )
| $less(sF25,0)
| mem(sK19,sK2) ),
inference(duplicate_literal_removal,[],[f741]) ).
tff(f1979,plain,
( ( empty = sK2 )
| ( sF23 = sK1 )
| mem(sK19,sK2)
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| $less(0,$uminus(sF25))
| ( empty = sK0 ) ),
inference(evaluation,[],[f1978]) ).
tff(f2020,plain,
! [X0: $int,X1: $int] : $less(0,$sum($sum(max(X1,X0),1),$uminus(X1))),
inference(evaluation,[],[f134]) ).
tff(f2063,plain,
! [X9: $int] :
( $less(sF25,0)
| ~ mem(X9,sK1)
| ( empty = sK1 )
| ( sK2 = sF22 )
| ( empty = sK0 )
| ~ $less(sF27,sF25)
| ~ $less(sK7,X9) ),
inference(duplicate_literal_removal,[],[f1178]) ).
tff(f2064,plain,
! [X9: $int] :
( ( empty = sK1 )
| $less(0,$uminus(sF25))
| ( empty = sK0 )
| ( sK2 = sF22 )
| ~ mem(X9,sK1)
| $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| $less(0,$sum($sum(sK7,1),$uminus(X9))) ),
inference(evaluation,[],[f2063]) ).
tff(f2067,plain,
( $less(0,$sum(sK9,$uminus(sK3)))
| ( empty = sK0 )
| ( sK1 = sF31 )
| ( sK2 = sF22 )
| ~ mem(sK3,sK0) ),
inference(evaluation,[],[f1252]) ).
tff(f2109,plain,
( ( empty = sK2 )
| ~ $less(sF27,sF25)
| mem(sK17,sK1)
| ( empty = sK1 )
| $less(sF25,0)
| ~ $less(sF26,sF25)
| ( empty = sK0 ) ),
inference(duplicate_literal_removal,[],[f755]) ).
tff(f2110,plain,
( $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| ( empty = sK0 )
| ( empty = sK1 )
| ( empty = sK2 )
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| $less(0,$uminus(sF25))
| mem(sK17,sK1) ),
inference(evaluation,[],[f2109]) ).
tff(f2194,plain,
! [X0: tree] : $less(0,$sum(size(X0),1)),
inference(evaluation,[],[f118]) ).
tff(f2247,plain,
( $less(sF25,0)
| mem(sK16,sK2)
| ( empty = sK2 )
| ( empty = sK1 )
| ( empty = sK0 )
| ~ $less(sF26,sF25) ),
inference(duplicate_literal_removal,[],[f748]) ).
tff(f2248,plain,
( ( empty = sK0 )
| mem(sK16,sK2)
| $less(0,$uminus(sF25))
| ( empty = sK2 )
| ( empty = sK1 )
| $less(0,$sum($sum(sF26,1),$uminus(sF25))) ),
inference(evaluation,[],[f2247]) ).
tff(f2286,plain,
( ~ $less(sF26,sF25)
| ( empty = sK2 )
| ( empty = sK1 )
| ( empty = sK0 )
| mem(sK18,sK0)
| ~ $less(sF27,sF25)
| ~ mem(sF29,sK0)
| $less(sF25,0) ),
inference(duplicate_literal_removal,[],[f774]) ).
tff(f2287,plain,
( ~ mem(sF29,sK0)
| ( empty = sK0 )
| mem(sK18,sK0)
| ( empty = sK1 )
| $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| ( empty = sK2 )
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| $less(0,$uminus(sF25)) ),
inference(evaluation,[],[f2286]) ).
tff(f2306,plain,
( ~ $less(sF27,sF25)
| mem(sK8,sK0)
| $less(sF25,0)
| ( empty = sK0 )
| ( sK2 = sF22 )
| ~ mem(sF30,sK0)
| ( empty = sK1 ) ),
inference(duplicate_literal_removal,[],[f962]) ).
tff(f2307,plain,
( $less(0,$sum($sum(sF27,1),$uminus(sF25)))
| $less(0,$uminus(sF25))
| mem(sK8,sK0)
| ~ mem(sF30,sK0)
| ( empty = sK0 )
| ( sK2 = sF22 )
| ( empty = sK1 ) ),
inference(evaluation,[],[f2306]) ).
tff(f2381,plain,
( ( sF23 = sK1 )
| $less(sF25,0)
| ( empty = sK2 )
| ~ mem(sF24,sK0)
| ( empty = sK0 )
| ~ $less(sF26,sF25)
| mem(sK20,sK0) ),
inference(duplicate_literal_removal,[],[f739]) ).
tff(f2382,plain,
( mem(sK20,sK0)
| ( empty = sK0 )
| $less(0,$uminus(sF25))
| ( empty = sK2 )
| ~ mem(sF24,sK0)
| $less(0,$sum($sum(sF26,1),$uminus(sF25)))
| ( sF23 = sK1 ) ),
inference(evaluation,[],[f2381]) ).
tff(f2452,definition,
( spl32_1
<=> $less(0,$sum($sum(sF27,1),$uminus(sF25))) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
tff(f2455,definition,
( spl32_2
<=> ( empty = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
tff(f2458,definition,
( spl32_3
<=> mem(sK3,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
tff(f2461,definition,
( spl32_4
<=> $less(0,$sum($sum(sF26,1),$uminus(sF25))) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
tff(f2464,definition,
( spl32_5
<=> mem(sK7,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
tff(f2465,plain,
( mem(sK7,sK1)
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f2464]) ).
tff(f2467,definition,
( spl32_6
<=> ( empty = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
tff(f2468,plain,
( ( empty = sK1 )
| ~ spl32_6 ),
inference(avatar_component_clause,[],[f2467]) ).
tff(f2470,definition,
( spl32_7
<=> ! [X19: $int] :
( ~ mem(X19,sK1)
| $less(0,$sum($sum(sK17,1),$uminus(X19))) ) ),
introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition]) ).
tff(f2471,plain,
( ! [X19: $int] :
( ~ mem(X19,sK1)
| $less(0,$sum($sum(sK17,1),$uminus(X19))) )
| ~ spl32_7 ),
inference(avatar_component_clause,[],[f2470]) ).
tff(f2473,definition,
( spl32_8
<=> ( empty = sK2 ) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
tff(f2474,plain,
( ( empty = sK2 )
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f2473]) ).
tff(f2476,definition,
( spl32_9
<=> $less(0,$uminus(sF25)) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
tff(f2479,definition,
( spl32_10
<=> mem(sK9,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
tff(f2480,plain,
( mem(sK9,sK0)
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f2479]) ).
tff(f2483,definition,
( spl32_11
<=> ! [X24: $int] :
( $less(0,$sum($sum(sK19,1),$uminus(X24)))
| ~ mem(X24,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition]) ).
tff(f2484,plain,
( ! [X24: $int] :
( ~ mem(X24,sK2)
| $less(0,$sum($sum(sK19,1),$uminus(X24))) )
| ~ spl32_11 ),
inference(avatar_component_clause,[],[f2483]) ).
tff(f2486,definition,
( spl32_12
<=> mem(sF30,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
tff(f2489,definition,
( spl32_13
<=> $less(0,$sum(sK8,$uminus(sF30))) ),
introduced(definition,[new_symbols(definition,[spl32_13])],[avatar_definition]) ).
tff(f2493,definition,
( spl32_14
<=> $less(0,$sum(sK9,$uminus(sK3))) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
tff(f2496,definition,
( spl32_15
<=> ( sK1 = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl32_15])],[avatar_definition]) ).
tff(f2500,definition,
( spl32_16
<=> mem(sK20,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
tff(f2501,plain,
( mem(sK20,sK0)
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f2500]) ).
tff(f2503,definition,
( spl32_17
<=> mem(sK18,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_17])],[avatar_definition]) ).
tff(f2504,plain,
( mem(sK18,sK0)
| ~ spl32_17 ),
inference(avatar_component_clause,[],[f2503]) ).
tff(f2506,definition,
( spl32_18
<=> mem(sF24,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_18])],[avatar_definition]) ).
tff(f2509,definition,
( spl32_19
<=> mem(sF29,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_19])],[avatar_definition]) ).
tff(f2513,definition,
( spl32_20
<=> mem(sK19,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
tff(f2514,plain,
( mem(sK19,sK2)
| ~ spl32_20 ),
inference(avatar_component_clause,[],[f2513]) ).
tff(f2516,definition,
( spl32_21
<=> ! [X21: $int] :
( ~ mem(X21,sK2)
| $less(0,$sum($sum(sK16,1),$uminus(X21))) ) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
tff(f2517,plain,
( ! [X21: $int] :
( ~ mem(X21,sK2)
| $less(0,$sum($sum(sK16,1),$uminus(X21))) )
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f2516]) ).
tff(f2520,definition,
( spl32_22
<=> mem(sK16,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_22])],[avatar_definition]) ).
tff(f2521,plain,
( mem(sK16,sK2)
| ~ spl32_22 ),
inference(avatar_component_clause,[],[f2520]) ).
tff(f2523,definition,
( spl32_23
<=> $less(0,$sum(sK20,$uminus(sF24))) ),
introduced(definition,[new_symbols(definition,[spl32_23])],[avatar_definition]) ).
tff(f2526,definition,
( spl32_24
<=> ! [X9: $int] :
( ~ mem(X9,sK1)
| $less(0,$sum($sum(sK7,1),$uminus(X9))) ) ),
introduced(definition,[new_symbols(definition,[spl32_24])],[avatar_definition]) ).
tff(f2527,plain,
( ! [X9: $int] :
( ~ mem(X9,sK1)
| $less(0,$sum($sum(sK7,1),$uminus(X9))) )
| ~ spl32_24 ),
inference(avatar_component_clause,[],[f2526]) ).
tff(f2531,definition,
( spl32_25
<=> $less(0,$sum(sK18,$uminus(sF29))) ),
introduced(definition,[new_symbols(definition,[spl32_25])],[avatar_definition]) ).
tff(f2534,definition,
( spl32_26
<=> mem(sK8,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_26])],[avatar_definition]) ).
tff(f2535,plain,
( mem(sK8,sK0)
| ~ spl32_26 ),
inference(avatar_component_clause,[],[f2534]) ).
tff(f2538,definition,
( spl32_27
<=> mem(sK17,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_27])],[avatar_definition]) ).
tff(f2539,plain,
( mem(sK17,sK1)
| ~ spl32_27 ),
inference(avatar_component_clause,[],[f2538]) ).
tff(f2569,definition,
( spl32_28
<=> ( sF23 = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
tff(f2570,plain,
( ( sF23 = sK1 )
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f2569]) ).
tff(f2571,plain,
( spl32_4
| spl32_8
| spl32_28
| spl32_9
| spl32_11
| spl32_2 ),
inference(avatar_split_clause,[],[f1397,f2455,f2483,f2476,f2569,f2473,f2461]) ).
tff(f2577,definition,
( spl32_29
<=> ( sF25 = size(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
tff(f2578,plain,
( ( sF25 = size(sK0) )
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f2577]) ).
tff(f2579,plain,
spl32_29,
inference(avatar_split_clause,[],[f737,f2577]) ).
tff(f2601,plain,
( spl32_6
| spl32_1
| spl32_4
| spl32_2
| spl32_7
| spl32_9
| spl32_8 ),
inference(avatar_split_clause,[],[f1448,f2473,f2476,f2470,f2455,f2461,f2452,f2467]) ).
tff(f2616,plain,
( spl32_23
| spl32_4
| spl32_9
| spl32_2
| spl32_28
| ~ spl32_18
| spl32_8 ),
inference(avatar_split_clause,[],[f1477,f2473,f2506,f2569,f2455,f2476,f2461,f2523]) ).
tff(f2635,definition,
( spl32_30
<=> ( max(sK3,sK16) = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl32_30])],[avatar_definition]) ).
tff(f2636,plain,
( ( max(sK3,sK16) = sF28 )
| ~ spl32_30 ),
inference(avatar_component_clause,[],[f2635]) ).
tff(f2637,plain,
spl32_30,
inference(avatar_split_clause,[],[f762,f2635]) ).
tff(f2646,definition,
( spl32_31
<=> ( max(sK7,sK3) = sF30 ) ),
introduced(definition,[new_symbols(definition,[spl32_31])],[avatar_definition]) ).
tff(f2647,plain,
( ( max(sK7,sK3) = sF30 )
| ~ spl32_31 ),
inference(avatar_component_clause,[],[f2646]) ).
tff(f2648,plain,
spl32_31,
inference(avatar_split_clause,[],[f781,f2646]) ).
tff(f2656,definition,
( spl32_32
<=> ( sF23 = node(sK15,sK13,sK14) ) ),
introduced(definition,[new_symbols(definition,[spl32_32])],[avatar_definition]) ).
tff(f2657,plain,
( ( sF23 = node(sK15,sK13,sK14) )
| ~ spl32_32 ),
inference(avatar_component_clause,[],[f2656]) ).
tff(f2658,plain,
spl32_32,
inference(avatar_split_clause,[],[f734,f2656]) ).
tff(f2676,definition,
( spl32_33
<=> ( sK2 = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl32_33])],[avatar_definition]) ).
tff(f2677,plain,
( ( sK2 = sF22 )
| ~ spl32_33 ),
inference(avatar_component_clause,[],[f2676]) ).
tff(f2678,plain,
( spl32_13
| ~ spl32_12
| spl32_9
| spl32_33
| spl32_1
| spl32_2
| spl32_6 ),
inference(avatar_split_clause,[],[f1569,f2467,f2455,f2452,f2676,f2476,f2486,f2489]) ).
tff(f2745,plain,
( spl32_2
| spl32_9
| spl32_8
| spl32_6
| spl32_21
| spl32_4 ),
inference(avatar_split_clause,[],[f1696,f2461,f2516,f2467,f2473,f2476,f2455]) ).
tff(f2807,plain,
( spl32_5
| spl32_6
| spl32_9
| spl32_33
| spl32_1
| spl32_2 ),
inference(avatar_split_clause,[],[f1816,f2455,f2452,f2676,f2476,f2467,f2464]) ).
tff(f2870,plain,
( spl32_8
| spl32_25
| spl32_4
| spl32_1
| spl32_2
| spl32_9
| ~ spl32_19
| spl32_6 ),
inference(avatar_split_clause,[],[f1938,f2467,f2509,f2476,f2455,f2452,f2461,f2531,f2473]) ).
tff(f2887,definition,
( spl32_35
<=> ( max(sK17,sF28) = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition]) ).
tff(f2888,plain,
( ( max(sK17,sF28) = sF29 )
| ~ spl32_35 ),
inference(avatar_component_clause,[],[f2887]) ).
tff(f2889,plain,
spl32_35,
inference(avatar_split_clause,[],[f764,f2887]) ).
tff(f2895,plain,
( spl32_20
| spl32_28
| spl32_4
| spl32_9
| spl32_2
| spl32_8 ),
inference(avatar_split_clause,[],[f1979,f2473,f2455,f2476,f2461,f2569,f2513]) ).
tff(f2921,definition,
( spl32_36
<=> ( node(sK12,sK11,sK10) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition]) ).
tff(f2922,plain,
( ( node(sK12,sK11,sK10) = sF22 )
| ~ spl32_36 ),
inference(avatar_component_clause,[],[f2921]) ).
tff(f2923,plain,
spl32_36,
inference(avatar_split_clause,[],[f732,f2921]) ).
tff(f2929,definition,
( spl32_37
<=> ( sF26 = size(sK2) ) ),
introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition]) ).
tff(f2930,plain,
( ( sF26 = size(sK2) )
| ~ spl32_37 ),
inference(avatar_component_clause,[],[f2929]) ).
tff(f2931,plain,
spl32_37,
inference(avatar_split_clause,[],[f738,f2929]) ).
tff(f2946,plain,
( spl32_24
| spl32_2
| spl32_33
| spl32_6
| spl32_9
| spl32_1 ),
inference(avatar_split_clause,[],[f2064,f2452,f2476,f2467,f2676,f2455,f2526]) ).
tff(f2949,plain,
( spl32_14
| ~ spl32_3
| spl32_33
| spl32_2
| spl32_15 ),
inference(avatar_split_clause,[],[f2067,f2496,f2455,f2676,f2458,f2493]) ).
tff(f2967,definition,
( spl32_38
<=> ( size(sK1) = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl32_38])],[avatar_definition]) ).
tff(f2968,plain,
( ( size(sK1) = sF27 )
| ~ spl32_38 ),
inference(avatar_component_clause,[],[f2967]) ).
tff(f2969,plain,
spl32_38,
inference(avatar_split_clause,[],[f750,f2967]) ).
tff(f2974,plain,
( spl32_6
| spl32_9
| spl32_8
| spl32_27
| spl32_2
| spl32_1
| spl32_4 ),
inference(avatar_split_clause,[],[f2110,f2461,f2452,f2455,f2538,f2473,f2476,f2467]) ).
tff(f3043,plain,
( spl32_2
| spl32_15
| ~ spl32_3
| spl32_10
| spl32_33 ),
inference(avatar_split_clause,[],[f1216,f2676,f2479,f2458,f2496,f2455]) ).
tff(f3049,plain,
( spl32_9
| spl32_22
| spl32_6
| spl32_4
| spl32_2
| spl32_8 ),
inference(avatar_split_clause,[],[f2248,f2473,f2455,f2461,f2467,f2520,f2476]) ).
tff(f3067,definition,
( spl32_40
<=> ( node(sK5,sK6,sK4) = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl32_40])],[avatar_definition]) ).
tff(f3068,plain,
( ( node(sK5,sK6,sK4) = sF31 )
| ~ spl32_40 ),
inference(avatar_component_clause,[],[f3067]) ).
tff(f3069,plain,
spl32_40,
inference(avatar_split_clause,[],[f1215,f3067]) ).
tff(f3074,plain,
( spl32_6
| spl32_2
| spl32_9
| ~ spl32_19
| spl32_17
| spl32_8
| spl32_4
| spl32_1 ),
inference(avatar_split_clause,[],[f2287,f2452,f2461,f2473,f2503,f2509,f2476,f2455,f2467]) ).
tff(f3079,definition,
( spl32_41
<=> ( max(sK19,sK3) = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl32_41])],[avatar_definition]) ).
tff(f3080,plain,
( ( max(sK19,sK3) = sF24 )
| ~ spl32_41 ),
inference(avatar_component_clause,[],[f3079]) ).
tff(f3081,plain,
spl32_41,
inference(avatar_split_clause,[],[f736,f3079]) ).
tff(f3088,plain,
( spl32_6
| spl32_26
| spl32_9
| spl32_2
| spl32_33
| ~ spl32_12
| spl32_1 ),
inference(avatar_split_clause,[],[f2307,f2452,f2486,f2676,f2455,f2476,f2534,f2467]) ).
tff(f3116,definition,
( spl32_42
<=> ( sF21 = node(sK1,sK3,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl32_42])],[avatar_definition]) ).
tff(f3117,plain,
( ( sF21 = node(sK1,sK3,sK2) )
| ~ spl32_42 ),
inference(avatar_component_clause,[],[f3116]) ).
tff(f3118,plain,
spl32_42,
inference(avatar_split_clause,[],[f729,f3116]) ).
tff(f3130,plain,
( spl32_16
| spl32_28
| spl32_9
| ~ spl32_18
| spl32_4
| spl32_2
| spl32_8 ),
inference(avatar_split_clause,[],[f2382,f2473,f2455,f2461,f2506,f2476,f2569,f2500]) ).
tff(f3151,definition,
( spl32_43
<=> ( sF21 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl32_43])],[avatar_definition]) ).
tff(f3152,plain,
( ( sF21 = sK0 )
| ~ spl32_43 ),
inference(avatar_component_clause,[],[f3151]) ).
tff(f3153,plain,
( spl32_2
| spl32_43 ),
inference(avatar_split_clause,[],[f730,f3151,f2455]) ).
tff(f3162,plain,
~ spl32_2,
inference(avatar_split_clause,[],[f137,f2455]) ).
tff(f3466,plain,
( ( empty != sF23 )
| ~ spl32_32 ),
inference(superposition,[],[f130,f2657]) ).
tff(f3469,definition,
( spl32_61
<=> ( empty = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl32_61])],[avatar_definition]) ).
tff(f3470,plain,
( ( empty != sF23 )
| spl32_61 ),
inference(avatar_component_clause,[],[f3469]) ).
tff(f3471,plain,
( ~ spl32_61
| ~ spl32_32 ),
inference(avatar_split_clause,[],[f3466,f2656,f3469]) ).
tff(f3613,plain,
( ( empty != sF22 )
| ~ spl32_36 ),
inference(superposition,[],[f130,f2922]) ).
tff(f3620,definition,
( spl32_74
<=> ( empty = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl32_74])],[avatar_definition]) ).
tff(f3621,plain,
( ( empty != sF22 )
| spl32_74 ),
inference(avatar_component_clause,[],[f3620]) ).
tff(f3622,plain,
( ~ spl32_74
| ~ spl32_36 ),
inference(avatar_split_clause,[],[f3613,f2921,f3620]) ).
tff(f3625,plain,
( ( empty != sF31 )
| ~ spl32_40 ),
inference(superposition,[],[f130,f3068]) ).
tff(f3628,definition,
( spl32_75
<=> ( empty = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl32_75])],[avatar_definition]) ).
tff(f3630,plain,
( ~ spl32_75
| ~ spl32_40 ),
inference(avatar_split_clause,[],[f3625,f3067,f3628]) ).
tff(f3635,plain,
( ( node(sK1,sK3,empty) = sF21 )
| ~ spl32_8
| ~ spl32_42 ),
inference(forward_demodulation,[],[f3117,f2474]) ).
tff(f3636,plain,
( ( node(sK1,sK3,empty) = sK0 )
| ~ spl32_8
| ~ spl32_42
| ~ spl32_43 ),
inference(forward_demodulation,[],[f3635,f3152]) ).
tff(f3637,plain,
( ( node(empty,sK3,empty) = sK0 )
| ~ spl32_6
| ~ spl32_8
| ~ spl32_42
| ~ spl32_43 ),
inference(forward_demodulation,[],[f3636,f2468]) ).
tff(f3639,definition,
( spl32_77
<=> ( node(empty,sK3,empty) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl32_77])],[avatar_definition]) ).
tff(f3640,plain,
( ( node(empty,sK3,empty) = sK0 )
| ~ spl32_77 ),
inference(avatar_component_clause,[],[f3639]) ).
tff(f3641,plain,
( spl32_77
| ~ spl32_6
| ~ spl32_8
| ~ spl32_42
| ~ spl32_43 ),
inference(avatar_split_clause,[],[f3637,f3151,f3116,f2473,f2467,f3639]) ).
tff(f3644,plain,
( ! [X0: $int] :
( ( sK3 = X0 )
| mem(X0,empty)
| ~ mem(X0,sK0)
| mem(X0,empty) )
| ~ spl32_77 ),
inference(superposition,[],[f125,f3640]) ).
tff(f3645,plain,
( ! [X0: $int] :
( mem(X0,empty)
| ( sK3 = X0 )
| ~ mem(X0,sK0) )
| ~ spl32_77 ),
inference(duplicate_literal_removal,[],[f3644]) ).
tff(f3646,plain,
( ! [X0: $int] :
( ~ mem(X0,sK0)
| ( sK3 = X0 ) )
| ~ spl32_77 ),
inference(forward_subsumption_resolution,[],[f3645,f124]) ).
tff(f3652,plain,
( ( sK9 = sK3 )
| ~ spl32_10
| ~ spl32_77 ),
inference(resolution,[],[f3646,f2480]) ).
tff(f3654,definition,
( spl32_78
<=> ( sK9 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl32_78])],[avatar_definition]) ).
tff(f3656,plain,
( spl32_78
| ~ spl32_10
| ~ spl32_77 ),
inference(avatar_split_clause,[],[f3652,f3639,f2479,f3654]) ).
tff(f3658,definition,
( spl32_79
<=> ( node(sK1,sK3,empty) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl32_79])],[avatar_definition]) ).
tff(f3659,plain,
( ( node(sK1,sK3,empty) = sK0 )
| ~ spl32_79 ),
inference(avatar_component_clause,[],[f3658]) ).
tff(f3660,plain,
( spl32_79
| ~ spl32_8
| ~ spl32_42
| ~ spl32_43 ),
inference(avatar_split_clause,[],[f3636,f3151,f3116,f2473,f3658]) ).
tff(f3675,plain,
( ! [X0: $int] :
( ~ mem(X0,sK0)
| mem(X0,empty)
| mem(X0,sK1)
| ( sK3 = X0 ) )
| ~ spl32_79 ),
inference(superposition,[],[f125,f3659]) ).
tff(f3676,plain,
( ! [X0: $int] :
( ~ mem(X0,sK0)
| ( sK3 = X0 )
| mem(X0,sK1) )
| ~ spl32_79 ),
inference(forward_subsumption_resolution,[],[f3675,f124]) ).
tff(f3686,plain,
! [X0: tree] : $less(0,$sum(1,size(X0))),
inference(superposition,[],[f2194,f43]) ).
tff(f4000,definition,
( spl32_111
<=> ( sK1 = node_proj_1(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl32_111])],[avatar_definition]) ).
tff(f4084,plain,
( ! [X0: $int] :
( ~ mem(X0,sK1)
| mem(X0,sK0) )
| ~ spl32_79 ),
inference(superposition,[],[f126,f3659]) ).
tff(f4088,plain,
( mem(sK7,sK0)
| ~ spl32_5
| ~ spl32_79 ),
inference(resolution,[],[f4084,f2465]) ).
tff(f4090,definition,
( spl32_115
<=> mem(sK7,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_115])],[avatar_definition]) ).
tff(f4092,plain,
( spl32_115
| ~ spl32_5
| ~ spl32_79 ),
inference(avatar_split_clause,[],[f4088,f3658,f2464,f4090]) ).
tff(f4219,plain,
( ( sK3 = max(sK7,sK3) )
| ( sF30 = sK7 )
| ~ spl32_31 ),
inference(superposition,[],[f2647,f716]) ).
tff(f4220,plain,
( ( max(sK19,sK3) = sK3 )
| ( sK19 = sF24 )
| ~ spl32_41 ),
inference(superposition,[],[f3080,f716]) ).
tff(f4221,plain,
( ( max(sK3,sK16) = sK3 )
| ( sK16 = sF28 )
| ~ spl32_30 ),
inference(superposition,[],[f2636,f716]) ).
tff(f4222,plain,
( ( sK17 = max(sK17,sF28) )
| ( sF28 = sF29 )
| ~ spl32_35 ),
inference(superposition,[],[f2888,f716]) ).
tff(f4226,definition,
( spl32_118
<=> ( sK3 = sF30 ) ),
introduced(definition,[new_symbols(definition,[spl32_118])],[avatar_definition]) ).
tff(f4229,definition,
( spl32_119
<=> ( sF30 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl32_119])],[avatar_definition]) ).
tff(f4232,plain,
( ( sK17 = sF29 )
| ( sF28 = sF29 )
| ~ spl32_35 ),
inference(forward_demodulation,[],[f4222,f2888]) ).
tff(f4233,plain,
( ( sK3 = sF28 )
| ( sK16 = sF28 )
| ~ spl32_30 ),
inference(forward_demodulation,[],[f4221,f2636]) ).
tff(f4235,definition,
( spl32_120
<=> ( sK17 = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl32_120])],[avatar_definition]) ).
tff(f4238,definition,
( spl32_121
<=> ( sF28 = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl32_121])],[avatar_definition]) ).
tff(f4242,plain,
( ( sF30 = sK7 )
| ( sK3 = sF30 )
| ~ spl32_31 ),
inference(forward_demodulation,[],[f4219,f2647]) ).
tff(f4244,definition,
( spl32_122
<=> ( sK19 = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl32_122])],[avatar_definition]) ).
tff(f4247,definition,
( spl32_123
<=> ( sK3 = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl32_123])],[avatar_definition]) ).
tff(f4251,definition,
( spl32_124
<=> ( sK16 = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl32_124])],[avatar_definition]) ).
tff(f4254,definition,
( spl32_125
<=> ( sK3 = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl32_125])],[avatar_definition]) ).
tff(f4257,plain,
( ( sK3 = sF24 )
| ( sK19 = sF24 )
| ~ spl32_41 ),
inference(forward_demodulation,[],[f4220,f3080]) ).
tff(f4261,plain,
( spl32_121
| spl32_120
| ~ spl32_35 ),
inference(avatar_split_clause,[],[f4232,f2887,f4235,f4238]) ).
tff(f4262,plain,
( spl32_125
| spl32_124
| ~ spl32_30 ),
inference(avatar_split_clause,[],[f4233,f2635,f4251,f4254]) ).
tff(f4263,plain,
( spl32_119
| spl32_118
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f4242,f2646,f4226,f4229]) ).
tff(f4264,plain,
( spl32_122
| spl32_123
| ~ spl32_41 ),
inference(avatar_split_clause,[],[f4257,f3079,f4247,f4244]) ).
tff(f4435,plain,
! [X0: $int,X1: $int] : $less(0,$sum(max(X0,X1),$sum(1,$uminus(X1)))),
inference(superposition,[],[f1604,f44]) ).
tff(f4436,plain,
! [X0: $int,X1: $int] : $less(0,$sum(max(X0,X1),$sum(1,$uminus(X0)))),
inference(superposition,[],[f2020,f44]) ).
tff(f4767,plain,
! [X2: tree,X0: $int,X1: tree] : ( size(node(X2,X0,X1)) = $sum(1,$sum(size(X2),size(X1))) ),
inference(forward_demodulation,[],[f136,f44]) ).
tff(f4844,plain,
( mem(sK8,sK1)
| ( sK8 = sK3 )
| ~ spl32_26
| ~ spl32_79 ),
inference(resolution,[],[f3676,f2535]) ).
tff(f4847,definition,
( spl32_150
<=> ( sK8 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl32_150])],[avatar_definition]) ).
tff(f4850,definition,
( spl32_151
<=> mem(sK8,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_151])],[avatar_definition]) ).
tff(f4851,plain,
( mem(sK8,sK1)
| ~ spl32_151 ),
inference(avatar_component_clause,[],[f4850]) ).
tff(f4852,plain,
( spl32_150
| spl32_151
| ~ spl32_26
| ~ spl32_79 ),
inference(avatar_split_clause,[],[f4844,f3658,f2534,f4850,f4847]) ).
tff(f4904,plain,
( ! [X0: tree,X1: $int] : ( size(node(X0,X1,sK2)) = $sum(1,$sum(size(X0),sF26)) )
| ~ spl32_37 ),
inference(superposition,[],[f4767,f2930]) ).
tff(f4907,plain,
! [X2: tree,X3: $int,X0: tree,X1: $int] : ( size(node(X0,X1,X2)) = size(node(X0,X3,X2)) ),
inference(superposition,[],[f4767,f4767]) ).
tff(f4923,plain,
( ! [X0: tree,X1: $int] : ( $sum(1,$sum(sF26,size(X0))) = size(node(X0,X1,sK2)) )
| ~ spl32_37 ),
inference(forward_demodulation,[],[f4904,f43]) ).
tff(f4933,plain,
( $less(0,$sum($sum(sK7,1),$uminus(sK8)))
| ~ spl32_24
| ~ spl32_151 ),
inference(resolution,[],[f4851,f2527]) ).
tff(f4936,definition,
( spl32_153
<=> $less(0,$sum($sum(sK7,1),$uminus(sK8))) ),
introduced(definition,[new_symbols(definition,[spl32_153])],[avatar_definition]) ).
tff(f4938,plain,
( spl32_153
| ~ spl32_24
| ~ spl32_151 ),
inference(avatar_split_clause,[],[f4933,f4850,f2526,f4936]) ).
tff(f5065,plain,
( ( sK0 = node(sK1,sK3,sK2) )
| ~ spl32_42
| ~ spl32_43 ),
inference(forward_demodulation,[],[f3117,f3152]) ).
tff(f5067,definition,
( spl32_166
<=> ( sK0 = node(sK1,sK3,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl32_166])],[avatar_definition]) ).
tff(f5068,plain,
( ( sK0 = node(sK1,sK3,sK2) )
| ~ spl32_166 ),
inference(avatar_component_clause,[],[f5067]) ).
tff(f5069,plain,
( spl32_166
| ~ spl32_42
| ~ spl32_43 ),
inference(avatar_split_clause,[],[f5065,f3151,f3116,f5067]) ).
tff(f5124,plain,
( ( empty != sK1 )
| ~ spl32_28
| spl32_61 ),
inference(superposition,[],[f3470,f2570]) ).
tff(f5126,plain,
( ~ spl32_6
| ~ spl32_28
| spl32_61 ),
inference(avatar_split_clause,[],[f5124,f3469,f2569,f2467]) ).
tff(f5131,plain,
( ( empty != sK2 )
| ~ spl32_33
| spl32_74 ),
inference(superposition,[],[f3621,f2677]) ).
tff(f5134,plain,
( ~ spl32_8
| ~ spl32_33
| spl32_74 ),
inference(avatar_split_clause,[],[f5131,f3620,f2676,f2473]) ).
tff(f5206,plain,
( ! [X0: $int] :
( ~ mem(X0,sK0)
| mem(X0,sK1)
| ( sK3 = X0 )
| mem(X0,sK2) )
| ~ spl32_166 ),
inference(superposition,[],[f125,f5068]) ).
tff(f5207,plain,
( ! [X0: $int] :
( ~ mem(X0,sK1)
| mem(X0,sK0) )
| ~ spl32_166 ),
inference(superposition,[],[f126,f5068]) ).
tff(f5208,plain,
( ! [X0: $int] :
( ~ mem(X0,sK2)
| mem(X0,sK0) )
| ~ spl32_166 ),
inference(superposition,[],[f128,f5068]) ).
tff(f5211,plain,
( ( sK1 = node_proj_1(sK0) )
| ~ spl32_166 ),
inference(superposition,[],[f720,f5068]) ).
tff(f5212,plain,
( mem(sK3,sK0)
| ~ spl32_166 ),
inference(superposition,[],[f727,f5068]) ).
tff(f5214,plain,
( spl32_111
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f5211,f5067,f4000]) ).
tff(f5221,plain,
( spl32_3
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f5212,f5067,f2458]) ).
tff(f5973,definition,
( spl32_235
<=> $less(0,$sum(1,sF27)) ),
introduced(definition,[new_symbols(definition,[spl32_235])],[avatar_definition]) ).
tff(f6000,definition,
( spl32_236
<=> $less(0,$sum(1,sF25)) ),
introduced(definition,[new_symbols(definition,[spl32_236])],[avatar_definition]) ).
tff(f6018,definition,
( spl32_237
<=> $less(0,$sum(1,sF26)) ),
introduced(definition,[new_symbols(definition,[spl32_237])],[avatar_definition]) ).
tff(f6077,plain,
( $less(0,$sum(1,sF25))
| ~ spl32_29 ),
inference(superposition,[],[f3686,f2578]) ).
tff(f6078,plain,
( $less(0,$sum(1,sF27))
| ~ spl32_38 ),
inference(superposition,[],[f3686,f2968]) ).
tff(f6079,plain,
( $less(0,$sum(1,sF26))
| ~ spl32_37 ),
inference(superposition,[],[f3686,f2930]) ).
tff(f6081,plain,
( spl32_235
| ~ spl32_38 ),
inference(avatar_split_clause,[],[f6078,f2967,f5973]) ).
tff(f6082,plain,
( spl32_236
| ~ spl32_29 ),
inference(avatar_split_clause,[],[f6077,f2577,f6000]) ).
tff(f6083,plain,
( spl32_237
| ~ spl32_37 ),
inference(avatar_split_clause,[],[f6079,f2929,f6018]) ).
tff(f6479,definition,
( spl32_274
<=> $less(0,$sum(sF29,$sum(1,$uminus(sF28)))) ),
introduced(definition,[new_symbols(definition,[spl32_274])],[avatar_definition]) ).
tff(f6500,definition,
( spl32_277
<=> $less(0,$sum(sF24,$sum(1,$uminus(sK3)))) ),
introduced(definition,[new_symbols(definition,[spl32_277])],[avatar_definition]) ).
tff(f6554,definition,
( spl32_282
<=> $less(0,$sum(sF28,$sum(1,$uminus(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl32_282])],[avatar_definition]) ).
tff(f6596,definition,
( spl32_285
<=> $less(0,$sum(sF30,$sum(1,$uminus(sK3)))) ),
introduced(definition,[new_symbols(definition,[spl32_285])],[avatar_definition]) ).
tff(f6649,definition,
( spl32_290
<=> $less(0,$sum(sF28,$sum(1,$uminus(sK3)))) ),
introduced(definition,[new_symbols(definition,[spl32_290])],[avatar_definition]) ).
tff(f6663,definition,
( spl32_291
<=> $less(0,$sum(sF29,$sum(1,$uminus(sK17)))) ),
introduced(definition,[new_symbols(definition,[spl32_291])],[avatar_definition]) ).
tff(f6693,definition,
( spl32_296
<=> $less(0,$sum(sF24,$sum(1,$uminus(sK19)))) ),
introduced(definition,[new_symbols(definition,[spl32_296])],[avatar_definition]) ).
tff(f6715,definition,
( spl32_297
<=> $less(0,$sum(sF30,$sum(1,$uminus(sK7)))) ),
introduced(definition,[new_symbols(definition,[spl32_297])],[avatar_definition]) ).
tff(f8116,plain,
( $less(0,$sum(sF28,$sum(1,$uminus(sK16))))
| ~ spl32_30 ),
inference(superposition,[],[f4435,f2636]) ).
tff(f8117,plain,
( $less(0,$sum(sF30,$sum(1,$uminus(sK3))))
| ~ spl32_31 ),
inference(superposition,[],[f4435,f2647]) ).
tff(f8118,plain,
( $less(0,$sum(sF29,$sum(1,$uminus(sF28))))
| ~ spl32_35 ),
inference(superposition,[],[f4435,f2888]) ).
tff(f8119,plain,
( $less(0,$sum(sF24,$sum(1,$uminus(sK3))))
| ~ spl32_41 ),
inference(superposition,[],[f4435,f3080]) ).
tff(f8128,plain,
( spl32_285
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f8117,f2646,f6596]) ).
tff(f8129,plain,
( spl32_274
| ~ spl32_35 ),
inference(avatar_split_clause,[],[f8118,f2887,f6479]) ).
tff(f8130,plain,
( spl32_282
| ~ spl32_30 ),
inference(avatar_split_clause,[],[f8116,f2635,f6554]) ).
tff(f8131,plain,
( spl32_277
| ~ spl32_41 ),
inference(avatar_split_clause,[],[f8119,f3079,f6500]) ).
tff(f8181,plain,
( $less(0,$sum(sF28,$sum(1,$uminus(sK3))))
| ~ spl32_30 ),
inference(superposition,[],[f4436,f2636]) ).
tff(f8182,plain,
( $less(0,$sum(sF30,$sum(1,$uminus(sK7))))
| ~ spl32_31 ),
inference(superposition,[],[f4436,f2647]) ).
tff(f8183,plain,
( $less(0,$sum(sF29,$sum(1,$uminus(sK17))))
| ~ spl32_35 ),
inference(superposition,[],[f4436,f2888]) ).
tff(f8184,plain,
( $less(0,$sum(sF24,$sum(1,$uminus(sK19))))
| ~ spl32_41 ),
inference(superposition,[],[f4436,f3080]) ).
tff(f8193,plain,
( spl32_290
| ~ spl32_30 ),
inference(avatar_split_clause,[],[f8181,f2635,f6649]) ).
tff(f8194,plain,
( spl32_297
| ~ spl32_31 ),
inference(avatar_split_clause,[],[f8182,f2646,f6715]) ).
tff(f8195,plain,
( spl32_291
| ~ spl32_35 ),
inference(avatar_split_clause,[],[f8183,f2887,f6663]) ).
tff(f8196,plain,
( spl32_296
| ~ spl32_41 ),
inference(avatar_split_clause,[],[f8184,f3079,f6693]) ).
tff(f10861,plain,
( ! [X0: $int] : ( size(node(sK1,X0,sK2)) = size(sK0) )
| ~ spl32_166 ),
inference(superposition,[],[f4907,f5068]) ).
tff(f10900,plain,
( ! [X0: $int] : ( sF25 = size(node(sK1,X0,sK2)) )
| ~ spl32_29
| ~ spl32_166 ),
inference(forward_demodulation,[],[f10861,f2578]) ).
tff(f12581,plain,
( ( sF25 = $sum(1,$sum(sF26,size(sK1))) )
| ~ spl32_29
| ~ spl32_37
| ~ spl32_166 ),
inference(superposition,[],[f4923,f10900]) ).
tff(f12598,plain,
( ( $sum(1,$sum(sF26,sF27)) = sF25 )
| ~ spl32_29
| ~ spl32_37
| ~ spl32_38
| ~ spl32_166 ),
inference(forward_demodulation,[],[f12581,f2968]) ).
tff(f12610,definition,
( spl32_529
<=> ( $sum(1,$sum(sF26,sF27)) = sF25 ) ),
introduced(definition,[new_symbols(definition,[spl32_529])],[avatar_definition]) ).
tff(f12612,plain,
( spl32_529
| ~ spl32_29
| ~ spl32_37
| ~ spl32_38
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f12598,f5067,f2967,f2929,f2577,f12610]) ).
tff(f12646,plain,
( mem(sK16,sK0)
| ~ spl32_22
| ~ spl32_166 ),
inference(resolution,[],[f2521,f5208]) ).
tff(f12649,definition,
( spl32_530
<=> mem(sK16,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_530])],[avatar_definition]) ).
tff(f12651,plain,
( spl32_530
| ~ spl32_22
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f12646,f5067,f2520,f12649]) ).
tff(f12656,plain,
( mem(sK17,sK0)
| ~ spl32_27
| ~ spl32_166 ),
inference(resolution,[],[f2539,f5207]) ).
tff(f12669,definition,
( spl32_534
<=> mem(sK17,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_534])],[avatar_definition]) ).
tff(f12671,plain,
( spl32_534
| ~ spl32_27
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f12656,f5067,f2538,f12669]) ).
tff(f12672,plain,
( mem(sK18,sK1)
| mem(sK18,sK2)
| ( sK18 = sK3 )
| ~ spl32_17
| ~ spl32_166 ),
inference(resolution,[],[f2504,f5206]) ).
tff(f12674,definition,
( spl32_535
<=> mem(sK18,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_535])],[avatar_definition]) ).
tff(f12675,plain,
( mem(sK18,sK2)
| ~ spl32_535 ),
inference(avatar_component_clause,[],[f12674]) ).
tff(f12677,definition,
( spl32_536
<=> ( sK18 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl32_536])],[avatar_definition]) ).
tff(f12680,definition,
( spl32_537
<=> mem(sK18,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_537])],[avatar_definition]) ).
tff(f12681,plain,
( mem(sK18,sK1)
| ~ spl32_537 ),
inference(avatar_component_clause,[],[f12680]) ).
tff(f12682,plain,
( spl32_535
| spl32_536
| spl32_537
| ~ spl32_17
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f12672,f5067,f2503,f12680,f12677,f12674]) ).
tff(f12892,plain,
( $less(0,$sum($sum(sK16,1),$uminus(sK18)))
| ~ spl32_21
| ~ spl32_535 ),
inference(resolution,[],[f12675,f2517]) ).
tff(f12896,definition,
( spl32_563
<=> $less(0,$sum($sum(sK16,1),$uminus(sK18))) ),
introduced(definition,[new_symbols(definition,[spl32_563])],[avatar_definition]) ).
tff(f12898,plain,
( spl32_563
| ~ spl32_21
| ~ spl32_535 ),
inference(avatar_split_clause,[],[f12892,f12674,f2516,f12896]) ).
tff(f12930,plain,
( $less(0,$sum($sum(sK17,1),$uminus(sK18)))
| ~ spl32_7
| ~ spl32_537 ),
inference(resolution,[],[f12681,f2471]) ).
tff(f12934,definition,
( spl32_570
<=> $less(0,$sum($sum(sK17,1),$uminus(sK18))) ),
introduced(definition,[new_symbols(definition,[spl32_570])],[avatar_definition]) ).
tff(f12936,plain,
( spl32_570
| ~ spl32_7
| ~ spl32_537 ),
inference(avatar_split_clause,[],[f12930,f12680,f2470,f12934]) ).
tff(f13053,plain,
( mem(sK19,sK0)
| ~ spl32_20
| ~ spl32_166 ),
inference(resolution,[],[f2514,f5208]) ).
tff(f13057,definition,
( spl32_585
<=> mem(sK19,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_585])],[avatar_definition]) ).
tff(f13059,plain,
( spl32_585
| ~ spl32_20
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f13053,f5067,f2513,f13057]) ).
tff(f13080,plain,
( mem(sK20,sK1)
| ( sK3 = sK20 )
| mem(sK20,sK2)
| ~ spl32_16
| ~ spl32_166 ),
inference(resolution,[],[f2501,f5206]) ).
tff(f13082,definition,
( spl32_588
<=> mem(sK20,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_588])],[avatar_definition]) ).
tff(f13083,plain,
( mem(sK20,sK1)
| ~ spl32_588 ),
inference(avatar_component_clause,[],[f13082]) ).
tff(f13085,definition,
( spl32_589
<=> mem(sK20,sK2) ),
introduced(definition,[new_symbols(definition,[spl32_589])],[avatar_definition]) ).
tff(f13086,plain,
( mem(sK20,sK2)
| ~ spl32_589 ),
inference(avatar_component_clause,[],[f13085]) ).
tff(f13088,definition,
( spl32_590
<=> ( sK3 = sK20 ) ),
introduced(definition,[new_symbols(definition,[spl32_590])],[avatar_definition]) ).
tff(f13090,plain,
( spl32_588
| spl32_589
| spl32_590
| ~ spl32_16
| ~ spl32_166 ),
inference(avatar_split_clause,[],[f13080,f5067,f2500,f13088,f13085,f13082]) ).
tff(f13301,plain,
( mem(sK20,empty)
| ~ spl32_6
| ~ spl32_588 ),
inference(superposition,[],[f13083,f2468]) ).
tff(f13302,plain,
( $false
| ~ spl32_6
| ~ spl32_588 ),
inference(forward_subsumption_resolution,[],[f13301,f124]) ).
tff(f13303,plain,
( ~ spl32_6
| ~ spl32_588 ),
inference(avatar_contradiction_clause,[],[f13302]) ).
tff(f13336,plain,
( $less(0,$sum($sum(sK19,1),$uminus(sK20)))
| ~ spl32_11
| ~ spl32_589 ),
inference(resolution,[],[f13086,f2484]) ).
tff(f13340,definition,
( spl32_609
<=> $less(0,$sum($sum(sK19,1),$uminus(sK20))) ),
introduced(definition,[new_symbols(definition,[spl32_609])],[avatar_definition]) ).
tff(f13342,plain,
( spl32_609
| ~ spl32_11
| ~ spl32_589 ),
inference(avatar_split_clause,[],[f13336,f13085,f2483,f13340]) ).
tff(f13353,plain,
$false,
inference(avatar_smt_refutation,[],[f13342,f13303,f13090,f13059,f12936,f12898,f12682,f12671,f12651,f12612,f8196,f8195,f8194,f8193,f8131,f8130,f8129,f8128,f6083,f6082,f6081,f5221,f5214,f5134,f5126,f5069,f4938,f4852,f4264,f4263,f4262,f4261,f4092,f3660,f3656,f3641,f3630,f3622,f3471,f3162,f3153,f3130,f3118,f3088,f3081,f3074,f3069,f3049,f3043,f2974,f2969,f2949,f2946,f2931,f2923,f2895,f2889,f2870,f2807,f2745,f2678,f2658,f2648,f2637,f2616,f2601,f2579,f2571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW598_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n015.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 14:24:31 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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
% 3.42/1.22 % (2660768)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.42/1.22 % (2660779)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1648744136:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.42/1.22 % (2660779)Instruction limit reached!
% 3.42/1.22 % (2660779)------------------------------
% 3.42/1.22 % (2660779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.22 % (2660779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.22 % (2660779)CaDiCaL version: 2.1.3
% 3.42/1.22 % (2660779)Termination reason: Instruction limit
% 3.42/1.22 % (2660779)Termination phase: Saturation
% 3.42/1.22 % (2660779)Time elapsed: 0.028 s
% 3.42/1.22 % (2660779)Peak memory usage: 116 MB
% 3.42/1.22 % (2660779)Instructions burned: 35 (million)
% 3.42/1.22 % (2660774)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=583902346:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.42/1.22 % (2660778)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2735375776:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.42/1.22 % (2660777)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1864145272:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.42/1.22 % (2660776)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1093501647:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.42/1.22 % (2660775)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1322880967:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.42/1.22 % (2660773)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=281538394:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.42/1.22 % (2660777)Instruction limit reached!
% 3.42/1.22 % (2660777)------------------------------
% 3.42/1.22 % (2660777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.22 % (2660777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.22 % (2660777)CaDiCaL version: 2.1.3
% 3.42/1.22 % (2660777)Termination reason: Instruction limit
% 3.42/1.22 % (2660777)Termination phase: Saturation
% 3.42/1.22 % (2660777)Time elapsed: 0.003 s
% 3.42/1.22 % (2660777)Peak memory usage: 88 MB
% 3.42/1.22 % (2660777)Instructions burned: 4 (million)
% 3.42/1.22 % (2660776)Instruction limit reached!
% 3.42/1.22 % (2660776)------------------------------
% 3.42/1.22 % (2660776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.22 % (2660776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.22 % (2660776)CaDiCaL version: 2.1.3
% 3.42/1.22 % (2660776)Termination reason: Instruction limit
% 3.42/1.22 % (2660776)Termination phase: Saturation
% 3.42/1.22 % (2660776)Time elapsed: 0.005 s
% 3.42/1.22 % (2660776)Peak memory usage: 88 MB
% 3.42/1.22 % (2660776)Instructions burned: 8 (million)
% 3.42/1.22 % (2660773)Instruction limit reached!
% 3.42/1.22 % (2660773)------------------------------
% 3.42/1.22 % (2660773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.22 % (2660773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.22 % (2660773)CaDiCaL version: 2.1.3
% 3.42/1.22 % (2660773)Termination reason: Instruction limit
% 3.42/1.22 % (2660773)Termination phase: Saturation
% 3.42/1.22 % (2660773)Time elapsed: 0.030 s
% 3.42/1.22 % (2660773)Peak memory usage: 115 MB
% 3.42/1.22 % (2660773)Instructions burned: 12 (million)
% 3.42/1.22 % (2660778)Instruction limit reached!
% 3.42/1.22 % (2660778)------------------------------
% 3.42/1.22 % (2660778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.42/1.22 % (2660778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.42/1.22 % (2660778)CaDiCaL version: 2.1.3
% 3.42/1.22 % (2660778)Termination reason: Instruction limit
% 3.42/1.22 % (2660778)Termination phase: Saturation
% 3.42/1.22 % (2660778)Time elapsed: 0.057 s
% 3.42/1.22 % (2660778)Peak memory usage: 115 MB
% 3.42/1.22 % (2660778)Instructions burned: 46 (million)
% 3.42/1.22 % (2660781)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=891041556:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.42/1.22 % (2660781)Instruction limit reached!
% 3.42/1.22 % (2660781)------------------------------
% 3.42/1.22 % (2660781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660781)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660781)Termination reason: Instruction limit
% 4.58/1.39 % (2660781)Termination phase: Saturation
% 4.58/1.39 % (2660781)Time elapsed: 0.006 s
% 4.58/1.39 % (2660781)Peak memory usage: 88 MB
% 4.58/1.39 % (2660781)Instructions burned: 15 (million)
% 4.58/1.39 % (2660775)Instruction limit reached!
% 4.58/1.39 % (2660775)------------------------------
% 4.58/1.39 % (2660775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660775)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660775)Termination reason: Instruction limit
% 4.58/1.39 % (2660775)Termination phase: Saturation
% 4.58/1.39 % (2660775)Time elapsed: 0.117 s
% 4.58/1.39 % (2660775)Peak memory usage: 116 MB
% 4.58/1.39 % (2660775)Instructions burned: 203 (million)
% 4.58/1.39 % (2660789)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=838018557:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.58/1.39 % (2660788)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=4069339392:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.58/1.39 % (2660789)Instruction limit reached!
% 4.58/1.39 % (2660789)------------------------------
% 4.58/1.39 % (2660789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660789)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660789)Termination reason: Instruction limit
% 4.58/1.39 % (2660789)Termination phase: Saturation
% 4.58/1.39 % (2660789)Time elapsed: 0.011 s
% 4.58/1.39 % (2660789)Peak memory usage: 88 MB
% 4.58/1.39 % (2660789)Instructions burned: 19 (million)
% 4.58/1.39 % (2660788)Instruction limit reached!
% 4.58/1.39 % (2660788)------------------------------
% 4.58/1.39 % (2660788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660788)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660788)Termination reason: Instruction limit
% 4.58/1.39 % (2660788)Termination phase: Property scanning
% 4.58/1.39 % (2660788)Time elapsed: 0.012 s
% 4.58/1.39 % (2660788)Peak memory usage: 86 MB
% 4.58/1.39 % (2660788)Instructions burned: 31 (million)
% 4.58/1.39 % (2660774)Instruction limit reached!
% 4.58/1.39 % (2660774)------------------------------
% 4.58/1.39 % (2660774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660774)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660774)Termination reason: Instruction limit
% 4.58/1.39 % (2660774)Termination phase: Saturation
% 4.58/1.39 % (2660774)Time elapsed: 0.171 s
% 4.58/1.39 % (2660774)Peak memory usage: 118 MB
% 4.58/1.39 % (2660774)Instructions burned: 308 (million)
% 4.58/1.39 % (2660790)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=774848226:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.58/1.39 % (2660790)Instruction limit reached!
% 4.58/1.39 % (2660790)------------------------------
% 4.58/1.39 % (2660790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.39 % (2660790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.39 % (2660790)CaDiCaL version: 2.1.3
% 4.58/1.39 % (2660790)Termination reason: Instruction limit
% 4.58/1.39 % (2660790)Termination phase: Saturation
% 4.58/1.39 % (2660790)Time elapsed: 0.020 s
% 4.58/1.39 % (2660790)Peak memory usage: 89 MB
% 4.58/1.39 % (2660790)Instructions burned: 24 (million)
% 4.58/1.39 % (2660791)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=3102153362:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.58/1.39 % (2660793)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1281298015:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.58/1.39 % (2660791)Instruction limit reached!
% 4.58/1.39 % (2660791)------------------------------
% 4.58/1.39 % (2660791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660791)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660791)Termination reason: Instruction limit
% 5.73/1.56 % (2660791)Termination phase: Saturation
% 5.73/1.56 % (2660791)Time elapsed: 0.019 s
% 5.73/1.56 % (2660791)Peak memory usage: 90 MB
% 5.73/1.56 % (2660791)Instructions burned: 27 (million)
% 5.73/1.56 % (2660793)Instruction limit reached!
% 5.73/1.56 % (2660793)------------------------------
% 5.73/1.56 % (2660793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660793)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660793)Termination reason: Instruction limit
% 5.73/1.56 % (2660793)Termination phase: Saturation
% 5.73/1.56 % (2660793)Time elapsed: 0.025 s
% 5.73/1.56 % (2660793)Peak memory usage: 89 MB
% 5.73/1.56 % (2660793)Instructions burned: 86 (million)
% 5.73/1.56 % (2660794)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3747388304:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.73/1.56 % (2660794)Instruction limit reached!
% 5.73/1.56 % (2660794)------------------------------
% 5.73/1.56 % (2660794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660794)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660794)Termination reason: Instruction limit
% 5.73/1.56 % (2660794)Termination phase: Preprocessing 3
% 5.73/1.56 % (2660794)Time elapsed: 0.002 s
% 5.73/1.56 % (2660794)Peak memory usage: 86 MB
% 5.73/1.56 % (2660794)Instructions burned: 2 (million)
% 5.73/1.56 % (2660798)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4107505078:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.73/1.56 % (2660797)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1980598797:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.73/1.56 % (2660798)Instruction limit reached!
% 5.73/1.56 % (2660798)------------------------------
% 5.73/1.56 % (2660798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660798)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660798)Termination reason: Instruction limit
% 5.73/1.56 % (2660798)Termination phase: Saturation
% 5.73/1.56 % (2660798)Time elapsed: 0.003 s
% 5.73/1.56 % (2660798)Peak memory usage: 88 MB
% 5.73/1.56 % (2660798)Instructions burned: 5 (million)
% 5.73/1.56 % (2660799)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1654173446:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.73/1.56 % (2660801)lrs+10_1_thi=all:si=on:fd=off:random_seed=375661459:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.73/1.56 % (2660805)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3107806960:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.73/1.56 % (2660804)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=2566799261:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.73/1.56 % (2660805)Instruction limit reached!
% 5.73/1.56 % (2660805)------------------------------
% 5.73/1.56 % (2660805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660805)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660805)Termination reason: Instruction limit
% 5.73/1.56 % (2660805)Termination phase: Saturation
% 5.73/1.56 % (2660805)Time elapsed: 0.002 s
% 5.73/1.56 % (2660805)Peak memory usage: 88 MB
% 5.73/1.56 % (2660805)Instructions burned: 4 (million)
% 5.73/1.56 % (2660804)Instruction limit reached!
% 5.73/1.56 % (2660804)------------------------------
% 5.73/1.56 % (2660804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.56 % (2660804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.56 % (2660804)CaDiCaL version: 2.1.3
% 5.73/1.56 % (2660804)Termination reason: Instruction limit
% 5.73/1.56 % (2660804)Termination phase: Saturation
% 6.88/1.74 % (2660804)Time elapsed: 0.005 s
% 6.88/1.74 % (2660804)Peak memory usage: 88 MB
% 6.88/1.74 % (2660804)Instructions burned: 9 (million)
% 6.88/1.74 % (2660801)Instruction limit reached!
% 6.88/1.74 % (2660801)------------------------------
% 6.88/1.74 % (2660801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660801)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660801)Termination reason: Instruction limit
% 6.88/1.74 % (2660801)Termination phase: Saturation
% 6.88/1.74 % (2660801)Time elapsed: 0.059 s
% 6.88/1.74 % (2660801)Peak memory usage: 116 MB
% 6.88/1.74 % (2660801)Instructions burned: 53 (million)
% 6.88/1.74 % (2660799)Instruction limit reached!
% 6.88/1.74 % (2660799)------------------------------
% 6.88/1.74 % (2660799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660799)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660799)Termination reason: Instruction limit
% 6.88/1.74 % (2660799)Termination phase: Saturation
% 6.88/1.74 % (2660799)Time elapsed: 0.093 s
% 6.88/1.74 % (2660799)Peak memory usage: 134 MB
% 6.88/1.74 % (2660799)Instructions burned: 66 (million)
% 6.88/1.74 % (2660807)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4007704278:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.88/1.74 % (2660807)Instruction limit reached!
% 6.88/1.74 % (2660807)------------------------------
% 6.88/1.74 % (2660807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660807)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660807)Termination reason: Instruction limit
% 6.88/1.74 % (2660807)Termination phase: Property scanning
% 6.88/1.74 % (2660807)Time elapsed: 0.002 s
% 6.88/1.74 % (2660807)Peak memory usage: 86 MB
% 6.88/1.74 % (2660807)Instructions burned: 2 (million)
% 6.88/1.74 % (2660797)Instruction limit reached!
% 6.88/1.74 % (2660797)------------------------------
% 6.88/1.74 % (2660797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660797)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660797)Termination reason: Instruction limit
% 6.88/1.74 % (2660797)Termination phase: Saturation
% 6.88/1.74 % (2660797)Time elapsed: 0.130 s
% 6.88/1.74 % (2660797)Peak memory usage: 91 MB
% 6.88/1.74 % (2660797)Instructions burned: 182 (million)
% 6.88/1.74 % (2660810)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=241086197:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.88/1.74 % (2660815)dis+10_1_si=on:random_seed=3000317959:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.88/1.74 % (2660815)Instruction limit reached!
% 6.88/1.74 % (2660815)------------------------------
% 6.88/1.74 % (2660815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660815)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660815)Termination reason: Instruction limit
% 6.88/1.74 % (2660815)Termination phase: Saturation
% 6.88/1.74 % (2660815)Time elapsed: 0.004 s
% 6.88/1.74 % (2660815)Peak memory usage: 88 MB
% 6.88/1.74 % (2660815)Instructions burned: 11 (million)
% 6.88/1.74 % (2660816)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3443013790:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.88/1.74 % (2660817)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=797331205:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 6.88/1.74 % (2660816)Instruction limit reached!
% 6.88/1.74 % (2660816)------------------------------
% 6.88/1.74 % (2660816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.74 % (2660816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.74 % (2660816)CaDiCaL version: 2.1.3
% 6.88/1.74 % (2660816)Termination reason: Instruction limit
% 6.88/1.74 % (2660816)Termination phase: Saturation
% 6.88/1.74 % (2660816)Time elapsed: 0.018 s
% 6.88/1.74 % (2660816)Peak memory usage: 89 MB
% 6.88/1.74 % (2660816)Instructions burned: 26 (million)
% 10.05/2.05 % (2660819)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2459808651:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.05/2.05 % (2660820)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1850958154:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.05/2.05 % (2660819)Instruction limit reached!
% 10.05/2.05 % (2660819)------------------------------
% 10.05/2.05 % (2660819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660819)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660819)Termination reason: Instruction limit
% 10.05/2.05 % (2660819)Termination phase: Property scanning
% 10.05/2.05 % (2660819)Time elapsed: 0.002 s
% 10.05/2.05 % (2660819)Peak memory usage: 86 MB
% 10.05/2.05 % (2660819)Instructions burned: 3 (million)
% 10.05/2.05 % (2660810)Instruction limit reached!
% 10.05/2.05 % (2660810)------------------------------
% 10.05/2.05 % (2660810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660810)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660810)Termination reason: Instruction limit
% 10.05/2.05 % (2660810)Termination phase: Saturation
% 10.05/2.05 % (2660810)Time elapsed: 0.118 s
% 10.05/2.05 % (2660810)Peak memory usage: 117 MB
% 10.05/2.05 % (2660810)Instructions burned: 127 (million)
% 10.05/2.05 % (2660820)Instruction limit reached!
% 10.05/2.05 % (2660820)------------------------------
% 10.05/2.05 % (2660820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660820)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660820)Termination reason: Instruction limit
% 10.05/2.05 % (2660820)Termination phase: Saturation
% 10.05/2.05 % (2660820)Time elapsed: 0.006 s
% 10.05/2.05 % (2660820)Peak memory usage: 88 MB
% 10.05/2.05 % (2660820)Instructions burned: 8 (million)
% 10.05/2.05 % (2660817)Instruction limit reached!
% 10.05/2.05 % (2660817)------------------------------
% 10.05/2.05 % (2660817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660817)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660817)Termination reason: Instruction limit
% 10.05/2.05 % (2660817)Termination phase: Saturation
% 10.05/2.05 % (2660817)Time elapsed: 0.027 s
% 10.05/2.05 % (2660817)Peak memory usage: 89 MB
% 10.05/2.05 % (2660817)Instructions burned: 36 (million)
% 10.05/2.05 % (2660821)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2626942134:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.05/2.05 % (2660824)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2516787838:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.05/2.05 % (2660824)Instruction limit reached!
% 10.05/2.05 % (2660824)------------------------------
% 10.05/2.05 % (2660824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660824)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660824)Termination reason: Instruction limit
% 10.05/2.05 % (2660824)Termination phase: Saturation
% 10.05/2.05 % (2660824)Time elapsed: 0.018 s
% 10.05/2.05 % (2660824)Peak memory usage: 112 MB
% 10.05/2.05 % (2660824)Instructions burned: 14 (million)
% 10.05/2.05 % (2660827)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2709705936:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.05/2.05 % (2660830)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3677326720:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.05/2.05 % (2660830)Instruction limit reached!
% 10.05/2.05 % (2660830)------------------------------
% 10.05/2.05 % (2660830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.05/2.05 % (2660830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/2.05 % (2660830)CaDiCaL version: 2.1.3
% 10.05/2.05 % (2660830)Termination reason: Instruction limit
% 10.05/2.05 % (2660830)Termination phase: Saturation
% 10.05/2.05 % (2660830)Time elapsed: 0.009 s
% 10.05/2.05 % (2660830)Peak memory usage: 88 MB
% 10.85/2.26 % (2660830)Instructions burned: 11 (million)
% 10.85/2.26 % (2660833)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=2802158734:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.85/2.26 % (2660832)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=1922316600:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.85/2.26 % (2660831)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=4110786155:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.85/2.26 % (2660836)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2325377361:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.85/2.26 % (2660832)Instruction limit reached!
% 10.85/2.26 % (2660832)------------------------------
% 10.85/2.26 % (2660832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660832)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660832)Termination reason: Instruction limit
% 10.85/2.26 % (2660832)Termination phase: Saturation
% 10.85/2.26 % (2660832)Time elapsed: 0.050 s
% 10.85/2.26 % (2660832)Peak memory usage: 90 MB
% 10.85/2.26 % (2660832)Instructions burned: 75 (million)
% 10.85/2.26 % (2660821)Instruction limit reached!
% 10.85/2.26 % (2660821)------------------------------
% 10.85/2.26 % (2660821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660821)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660821)Termination reason: Instruction limit
% 10.85/2.26 % (2660821)Termination phase: Saturation
% 10.85/2.26 % (2660821)Time elapsed: 0.198 s
% 10.85/2.26 % (2660821)Peak memory usage: 92 MB
% 10.85/2.26 % (2660821)Instructions burned: 370 (million)
% 10.85/2.26 % (2660836)Instruction limit reached!
% 10.85/2.26 % (2660836)------------------------------
% 10.85/2.26 % (2660836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660836)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660836)Termination reason: Instruction limit
% 10.85/2.26 % (2660836)Termination phase: Saturation
% 10.85/2.26 % (2660836)Time elapsed: 0.044 s
% 10.85/2.26 % (2660836)Peak memory usage: 113 MB
% 10.85/2.26 % (2660836)Instructions burned: 134 (million)
% 10.85/2.26 % (2660831)Instruction limit reached!
% 10.85/2.26 % (2660831)------------------------------
% 10.85/2.26 % (2660831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660831)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660831)Termination reason: Instruction limit
% 10.85/2.26 % (2660831)Termination phase: Saturation
% 10.85/2.26 % (2660831)Time elapsed: 0.093 s
% 10.85/2.26 % (2660831)Peak memory usage: 133 MB
% 10.85/2.26 % (2660831)Instructions burned: 71 (million)
% 10.85/2.26 % (2660827)Instruction limit reached!
% 10.85/2.26 % (2660827)------------------------------
% 10.85/2.26 % (2660827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660827)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660827)Termination reason: Instruction limit
% 10.85/2.26 % (2660827)Termination phase: Saturation
% 10.85/2.26 % (2660827)Time elapsed: 0.172 s
% 10.85/2.26 % (2660827)Peak memory usage: 117 MB
% 10.85/2.26 % (2660827)Instructions burned: 226 (million)
% 10.85/2.26 % (2660839)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1982808042:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.85/2.26 % (2660833)Instruction limit reached!
% 10.85/2.26 % (2660833)------------------------------
% 10.85/2.26 % (2660833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.26 % (2660833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.26 % (2660833)CaDiCaL version: 2.1.3
% 10.85/2.26 % (2660833)Termination reason: Instruction limit
% 10.85/2.26 % (2660833)Termination phase: Saturation
% 10.85/2.26 % (2660833)Time elapsed: 0.163 s
% 10.85/2.26 % (2660833)Peak memory usage: 91 MB
% 12.36/2.58 % (2660833)Instructions burned: 294 (million)
% 12.36/2.58 % (2660846)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2342904887:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 12.36/2.58 % (2660844)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3785872996:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 12.36/2.58 % (2660845)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=754187214:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 12.36/2.58 % (2660844)Instruction limit reached!
% 12.36/2.58 % (2660844)------------------------------
% 12.36/2.58 % (2660844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.36/2.58 % (2660844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.36/2.58 % (2660844)CaDiCaL version: 2.1.3
% 12.36/2.58 % (2660844)Termination reason: Instruction limit
% 12.36/2.58 % (2660844)Termination phase: Saturation
% 12.36/2.58 % (2660844)Time elapsed: 0.069 s
% 12.36/2.58 % (2660844)Peak memory usage: 133 MB
% 12.36/2.58 % (2660844)Instructions burned: 41 (million)
% 12.36/2.58 % (2660847)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1360046348:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.36/2.58 % (2660848)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=3792231401:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 12.36/2.58 % (2660839)Instruction limit reached!
% 12.36/2.58 % (2660839)------------------------------
% 12.36/2.58 % (2660839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.36/2.58 % (2660839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.36/2.58 % (2660839)CaDiCaL version: 2.1.3
% 12.36/2.58 % (2660839)Termination reason: Instruction limit
% 12.36/2.58 % (2660839)Termination phase: Saturation
% 12.36/2.58 % (2660839)Time elapsed: 0.137 s
% 12.36/2.58 % (2660839)Peak memory usage: 133 MB
% 12.36/2.58 % (2660839)Instructions burned: 131 (million)
% 12.36/2.58 % (2660850)dis+10_1_si=on:random_seed=3325357633:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 12.36/2.58 % (2660847)Instruction limit reached!
% 12.36/2.58 % (2660847)------------------------------
% 12.36/2.58 % (2660847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.36/2.58 % (2660847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.36/2.58 % (2660847)CaDiCaL version: 2.1.3
% 12.36/2.58 % (2660847)Termination reason: Instruction limit
% 12.36/2.58 % (2660847)Termination phase: Saturation
% 12.36/2.58 % (2660847)Time elapsed: 0.111 s
% 12.36/2.58 % (2660847)Peak memory usage: 118 MB
% 12.36/2.58 % (2660847)Instructions burned: 131 (million)
% 12.36/2.58 % (2660846)Instruction limit reached!
% 12.36/2.58 % (2660846)------------------------------
% 12.36/2.58 % (2660846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.36/2.58 % (2660846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.36/2.58 % (2660846)CaDiCaL version: 2.1.3
% 12.36/2.58 % (2660846)Termination reason: Instruction limit
% 12.36/2.58 % (2660846)Termination phase: Saturation
% 12.36/2.58 % (2660846)Time elapsed: 0.239 s
% 12.36/2.58 % (2660846)Peak memory usage: 139 MB
% 12.36/2.58 % (2660846)Instructions burned: 599 (million)
% 12.36/2.58 % (2660854)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=4112849125:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.36/2.58 % (2660845)Instruction limit reached!
% 12.36/2.58 % (2660845)------------------------------
% 12.36/2.58 % (2660845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.36/2.58 % (2660845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.36/2.58 % (2660845)CaDiCaL version: 2.1.3
% 12.36/2.58 % (2660845)Termination reason: Instruction limit
% 12.36/2.58 % (2660845)Termination phase: Saturation
% 12.36/2.58 % (2660845)Time elapsed: 0.205 s
% 12.36/2.58 % (2660845)Peak memory usage: 93 MB
% 12.36/2.58 % (2660845)Instructions burned: 308 (million)
% 12.36/2.58 % (2660857)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3516905259:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 12.36/2.58 % (2660848)Instruction limit reached!
% 14.52/2.86 % (2660848)------------------------------
% 14.52/2.86 % (2660848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660848)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660848)Termination reason: Instruction limit
% 14.52/2.86 % (2660848)Termination phase: Saturation
% 14.52/2.86 % (2660848)Time elapsed: 0.190 s
% 14.52/2.86 % (2660848)Peak memory usage: 117 MB
% 14.52/2.86 % (2660848)Instructions burned: 259 (million)
% 14.52/2.86 % (2660859)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2515451606:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 14.52/2.86 % (2660861)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1933830651:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 14.52/2.86 % (2660857)Instruction limit reached!
% 14.52/2.86 % (2660857)------------------------------
% 14.52/2.86 % (2660857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660857)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660857)Termination reason: Instruction limit
% 14.52/2.86 % (2660857)Termination phase: Saturation
% 14.52/2.86 % (2660857)Time elapsed: 0.101 s
% 14.52/2.86 % (2660857)Peak memory usage: 90 MB
% 14.52/2.86 % (2660857)Instructions burned: 142 (million)
% 14.52/2.86 % (2660861)Instruction limit reached!
% 14.52/2.86 % (2660861)------------------------------
% 14.52/2.86 % (2660861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660861)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660861)Termination reason: Instruction limit
% 14.52/2.86 % (2660861)Termination phase: Saturation
% 14.52/2.86 % (2660861)Time elapsed: 0.041 s
% 14.52/2.86 % (2660861)Peak memory usage: 89 MB
% 14.52/2.86 % (2660861)Instructions burned: 123 (million)
% 14.52/2.86 % (2660862)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=3327785372:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.52/2.86 % (2660859)Refutation not found, incomplete strategy
% 14.52/2.86 % (2660859)------------------------------
% 14.52/2.86 % (2660859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660859)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660859)Termination reason: Refutation not found, incomplete strategy
% 14.52/2.86 % (2660859)Time elapsed: 0.061 s
% 14.52/2.86 % (2660859)Peak memory usage: 116 MB
% 14.52/2.86 % (2660859)Instructions burned: 54 (million)
% 14.52/2.86 % (2660864)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=3715092712:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 14.52/2.86 % (2660854)Instruction limit reached!
% 14.52/2.86 % (2660854)------------------------------
% 14.52/2.86 % (2660854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660854)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660854)Termination reason: Instruction limit
% 14.52/2.86 % (2660854)Termination phase: Saturation
% 14.52/2.86 % (2660854)Time elapsed: 0.243 s
% 14.52/2.86 % (2660854)Peak memory usage: 95 MB
% 14.52/2.86 % (2660854)Instructions burned: 384 (million)
% 14.52/2.86 % (2660864)Instruction limit reached!
% 14.52/2.86 % (2660864)------------------------------
% 14.52/2.86 % (2660864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660864)CaDiCaL version: 2.1.3
% 14.52/2.86 % (2660864)Termination reason: Instruction limit
% 14.52/2.86 % (2660864)Termination phase: Saturation
% 14.52/2.86 % (2660864)Time elapsed: 0.050 s
% 14.52/2.86 % (2660864)Peak memory usage: 116 MB
% 14.52/2.86 % (2660864)Instructions burned: 39 (million)
% 14.52/2.86 % (2660862)Instruction limit reached!
% 14.52/2.86 % (2660862)------------------------------
% 14.52/2.86 % (2660862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.52/2.86 % (2660862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.52/2.86 % (2660862)CaDiCaL version: 2.1.3
% 18.15/3.23 % (2660862)Termination reason: Instruction limit
% 18.15/3.23 % (2660862)Termination phase: Saturation
% 18.15/3.23 % (2660862)Time elapsed: 0.107 s
% 18.15/3.23 % (2660862)Peak memory usage: 118 MB
% 18.15/3.23 % (2660862)Instructions burned: 128 (million)
% 18.15/3.23 % (2660869)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1293229018:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi)
% 18.15/3.23 % (2660867)dis+1010_1_to=kbo:si=on:random_seed=3588065034:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 18.15/3.23 % (2660871)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1717573254:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 18.15/3.23 % (2660869)Instruction limit reached!
% 18.15/3.23 % (2660869)------------------------------
% 18.15/3.23 % (2660869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.23 % (2660869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.23 % (2660869)CaDiCaL version: 2.1.3
% 18.15/3.23 % (2660869)Termination reason: Instruction limit
% 18.15/3.23 % (2660869)Termination phase: Saturation
% 18.15/3.23 % (2660869)Time elapsed: 0.093 s
% 18.15/3.23 % (2660869)Peak memory usage: 116 MB
% 18.15/3.23 % (2660869)Instructions burned: 332 (million)
% 18.15/3.23 % (2660867)Instruction limit reached!
% 18.15/3.23 % (2660867)------------------------------
% 18.15/3.23 % (2660867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.23 % (2660867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.23 % (2660867)CaDiCaL version: 2.1.3
% 18.15/3.23 % (2660867)Termination reason: Instruction limit
% 18.15/3.23 % (2660867)Termination phase: Saturation
% 18.15/3.23 % (2660867)Time elapsed: 0.094 s
% 18.15/3.23 % (2660867)Peak memory usage: 91 MB
% 18.15/3.23 % (2660867)Instructions burned: 175 (million)
% 18.15/3.23 % (2660859)------------------------------
% 18.15/3.23 % (2660859)------------------------------
% 18.15/3.23 % (2660850)Instruction limit reached!
% 18.15/3.23 % (2660850)------------------------------
% 18.15/3.23 % (2660850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.23 % (2660850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.23 % (2660850)CaDiCaL version: 2.1.3
% 18.15/3.23 % (2660850)Termination reason: Instruction limit
% 18.15/3.23 % (2660850)Termination phase: Saturation
% 18.15/3.23 % (2660850)Time elapsed: 0.511 s
% 18.15/3.23 % (2660850)Peak memory usage: 96 MB
% 18.15/3.23 % (2660850)Instructions burned: 1001 (million)
% 18.15/3.23 % (2660873)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=854022075:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 18.15/3.23 % (2660872)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2382670710:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi)
% 18.15/3.23 % (2660877)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1814449073:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi)
% 18.15/3.23 % (2660878)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2084412349:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.15/3.23 % (2660872)Instruction limit reached!
% 18.15/3.23 % (2660872)------------------------------
% 18.15/3.23 % (2660872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.15/3.23 % (2660872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.15/3.23 % (2660872)CaDiCaL version: 2.1.3
% 18.15/3.23 % (2660872)Termination reason: Instruction limit
% 18.15/3.23 % (2660872)Termination phase: Saturation
% 18.15/3.23 % (2660872)Time elapsed: 0.134 s
% 18.15/3.23 % (2660872)Peak memory usage: 131 MB
% 18.15/3.23 % (2660872)Instructions burned: 215 (million)
% 18.15/3.23 % (2660882)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2195507497:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/484Mi)
% 18.15/3.23 % (2660881)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3486198421:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 18.15/3.23 % (2660877)Instruction limit reached!
% 18.15/3.23 % (2660877)------------------------------
% 18.15/3.23 % (2660877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660877)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660877)Termination reason: Instruction limit
% 18.68/3.48 % (2660877)Termination phase: Saturation
% 18.68/3.48 % (2660877)Time elapsed: 0.085 s
% 18.68/3.48 % (2660877)Peak memory usage: 91 MB
% 18.68/3.48 % (2660877)Instructions burned: 297 (million)
% 18.68/3.48 % (2660873)Instruction limit reached!
% 18.68/3.48 % (2660873)------------------------------
% 18.68/3.48 % (2660873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660873)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660873)Termination reason: Instruction limit
% 18.68/3.48 % (2660873)Termination phase: Saturation
% 18.68/3.48 % (2660873)Time elapsed: 0.237 s
% 18.68/3.48 % (2660873)Peak memory usage: 119 MB
% 18.68/3.48 % (2660873)Instructions burned: 350 (million)
% 18.68/3.48 % (2660888)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1052565588:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 18.68/3.48 % (2660885)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3397049582:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 18.68/3.48 % (2660871)Instruction limit reached!
% 18.68/3.48 % (2660871)------------------------------
% 18.68/3.48 % (2660871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660871)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660871)Termination reason: Instruction limit
% 18.68/3.48 % (2660871)Termination phase: Saturation
% 18.68/3.48 % (2660871)Time elapsed: 0.347 s
% 18.68/3.48 % (2660871)Peak memory usage: 135 MB
% 18.68/3.48 % (2660871)Instructions burned: 485 (million)
% 18.68/3.48 % (2660878)Instruction limit reached!
% 18.68/3.48 % (2660878)------------------------------
% 18.68/3.48 % (2660878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660878)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660878)Termination reason: Instruction limit
% 18.68/3.48 % (2660878)Termination phase: Saturation
% 18.68/3.48 % (2660878)Time elapsed: 0.233 s
% 18.68/3.48 % (2660878)Peak memory usage: 118 MB
% 18.68/3.48 % (2660878)Instructions burned: 329 (million)
% 18.68/3.48 % (2660881)Instruction limit reached!
% 18.68/3.48 % (2660881)------------------------------
% 18.68/3.48 % (2660881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660881)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660881)Termination reason: Instruction limit
% 18.68/3.48 % (2660881)Termination phase: Saturation
% 18.68/3.48 % (2660881)Time elapsed: 0.210 s
% 18.68/3.48 % (2660881)Peak memory usage: 118 MB
% 18.68/3.48 % (2660881)Instructions burned: 281 (million)
% 18.68/3.48 % (2660889)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4041836719:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi)
% 18.68/3.48 % (2660882)Instruction limit reached!
% 18.68/3.48 % (2660882)------------------------------
% 18.68/3.48 % (2660882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660882)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660882)Termination reason: Instruction limit
% 18.68/3.48 % (2660882)Termination phase: Saturation
% 18.68/3.48 % (2660882)Time elapsed: 0.263 s
% 18.68/3.48 % (2660882)Peak memory usage: 90 MB
% 18.68/3.48 % (2660882)Instructions burned: 486 (million)
% 18.68/3.48 % (2660888)Instruction limit reached!
% 18.68/3.48 % (2660888)------------------------------
% 18.68/3.48 % (2660888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.68/3.48 % (2660888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.68/3.48 % (2660888)CaDiCaL version: 2.1.3
% 18.68/3.48 % (2660888)Termination reason: Instruction limit
% 18.68/3.48 % (2660888)Termination phase: Saturation
% 18.68/3.48 % (2660888)Time elapsed: 0.155 s
% 18.68/3.48 % (2660888)Peak memory usage: 119 MB
% 18.68/3.48 % (2660888)Instructions burned: 416 (million)
% 18.68/3.48 % (2660885)Instruction limit reached!
% 20.77/3.89 % (2660885)------------------------------
% 20.77/3.89 % (2660885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.77/3.89 % (2660885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.89 % (2660885)CaDiCaL version: 2.1.3
% 20.77/3.89 % (2660885)Termination reason: Instruction limit
% 20.77/3.89 % (2660885)Termination phase: Saturation
% 20.77/3.89 % (2660885)Time elapsed: 0.162 s
% 20.77/3.89 % (2660885)Peak memory usage: 119 MB
% 20.77/3.89 % (2660885)Instructions burned: 322 (million)
% 20.77/3.89 % (2660892)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=2974211844:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 20.77/3.89 % (2660893)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=280035421:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi)
% 20.77/3.89 % (2660894)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2756639109:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 20.77/3.89 % (2660897)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4269152212:i=334:rtra=on_2978 on theBenchmark for (2978ds/334Mi)
% 20.77/3.89 % (2660896)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=615133705:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi)
% 20.77/3.89 % (2660898)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3036675138:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 20.77/3.89 % (2660897)Instruction limit reached!
% 20.77/3.89 % (2660897)------------------------------
% 20.77/3.89 % (2660897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.77/3.89 % (2660897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.89 % (2660897)CaDiCaL version: 2.1.3
% 20.77/3.89 % (2660897)Termination reason: Instruction limit
% 20.77/3.89 % (2660897)Termination phase: Saturation
% 20.77/3.89 % (2660897)Time elapsed: 0.141 s
% 20.77/3.89 % (2660897)Peak memory usage: 135 MB
% 20.77/3.89 % (2660897)Instructions burned: 337 (million)
% 20.77/3.89 % (2660892)Instruction limit reached!
% 20.77/3.89 % (2660892)------------------------------
% 20.77/3.89 % (2660892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.77/3.89 % (2660892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.89 % (2660892)CaDiCaL version: 2.1.3
% 20.77/3.89 % (2660892)Termination reason: Instruction limit
% 20.77/3.89 % (2660892)Termination phase: Saturation
% 20.77/3.89 % (2660892)Time elapsed: 0.225 s
% 20.77/3.89 % (2660892)Peak memory usage: 135 MB
% 20.77/3.89 % (2660892)Instructions burned: 276 (million)
% 20.77/3.89 % (2660889)Instruction limit reached!
% 20.77/3.89 % (2660889)------------------------------
% 20.77/3.89 % (2660889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.77/3.89 % (2660889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.89 % (2660889)CaDiCaL version: 2.1.3
% 20.77/3.89 % (2660889)Termination reason: Instruction limit
% 20.77/3.89 % (2660889)Termination phase: Saturation
% 20.77/3.89 % (2660889)Time elapsed: 0.326 s
% 20.77/3.89 % (2660889)Peak memory usage: 120 MB
% 20.77/3.89 % (2660889)Instructions burned: 472 (million)
% 20.77/3.89 % (2660893)Instruction limit reached!
% 20.77/3.89 % (2660893)------------------------------
% 20.77/3.89 % (2660893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.77/3.89 % (2660893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.77/3.89 % (2660893)CaDiCaL version: 2.1.3
% 20.77/3.89 % (2660893)Termination reason: Instruction limit
% 20.77/3.89 % (2660893)Termination phase: Saturation
% 20.77/3.89 % (2660893)Time elapsed: 0.272 s
% 20.77/3.89 % (2660893)Peak memory usage: 119 MB
% 20.77/3.89 % (2660893)Instructions burned: 376 (million)
% 20.77/3.89 % (2660905)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2576804205:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi)
% 20.77/3.89 % (2660894)Instruction limit reached!
% 20.77/3.89 % (2660894)------------------------------
% 20.77/3.89 % (2660894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.74/4.33 % (2660894)CaDiCaL version: 2.1.3
% 25.74/4.33 % (2660894)Termination reason: Instruction limit
% 25.74/4.33 % (2660894)Termination phase: Saturation
% 25.74/4.33 % (2660894)Time elapsed: 0.295 s
% 25.74/4.33 % (2660894)Peak memory usage: 119 MB
% 25.74/4.33 % (2660894)Instructions burned: 387 (million)
% 25.74/4.33 % (2660898)Instruction limit reached!
% 25.74/4.33 % (2660898)------------------------------
% 25.74/4.33 % (2660898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.74/4.33 % (2660898)CaDiCaL version: 2.1.3
% 25.74/4.33 % (2660898)Termination reason: Instruction limit
% 25.74/4.33 % (2660898)Termination phase: Saturation
% 25.74/4.33 % (2660898)Time elapsed: 0.231 s
% 25.74/4.33 % (2660898)Peak memory usage: 92 MB
% 25.74/4.33 % (2660898)Instructions burned: 360 (million)
% 25.74/4.33 % (2660906)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2503304392:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 25.74/4.33 % (2660907)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=2917626242:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 25.74/4.33 % (2660896)Instruction limit reached!
% 25.74/4.33 % (2660896)------------------------------
% 25.74/4.33 % (2660896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.74/4.33 % (2660896)CaDiCaL version: 2.1.3
% 25.74/4.33 % (2660896)Termination reason: Instruction limit
% 25.74/4.33 % (2660896)Termination phase: Saturation
% 25.74/4.33 % (2660896)Time elapsed: 0.322 s
% 25.74/4.33 % (2660896)Peak memory usage: 93 MB
% 25.74/4.33 % (2660896)Instructions burned: 514 (million)
% 25.74/4.33 % (2660908)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1185173007:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 25.74/4.33 % (2660905)Instruction limit reached!
% 25.74/4.33 % (2660905)------------------------------
% 25.74/4.33 % (2660905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.74/4.33 % (2660905)CaDiCaL version: 2.1.3
% 25.74/4.33 % (2660905)Termination reason: Instruction limit
% 25.74/4.33 % (2660905)Termination phase: Saturation
% 25.74/4.33 % (2660905)Time elapsed: 0.132 s
% 25.74/4.33 % (2660905)Peak memory usage: 120 MB
% 25.74/4.33 % (2660905)Instructions burned: 341 (million)
% 25.74/4.33 % (2660910)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4263708563:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 25.74/4.33 % (2660911)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=309028590:i=4428:doe=on:fsr=off:rtra=on_2974 on theBenchmark for (2974ds/4428Mi)
% 25.74/4.33 % (2660906)Instruction limit reached!
% 25.74/4.33 % (2660906)------------------------------
% 25.74/4.33 % (2660906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.74/4.33 % (2660906)CaDiCaL version: 2.1.3
% 25.74/4.33 % (2660906)Termination reason: Instruction limit
% 25.74/4.33 % (2660906)Termination phase: Saturation
% 25.74/4.33 % (2660906)Time elapsed: 0.185 s
% 25.74/4.33 % (2660906)Peak memory usage: 118 MB
% 25.74/4.33 % (2660906)Instructions burned: 262 (million)
% 25.74/4.33 % (2660914)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=2971923198:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 25.74/4.33 % (2660916)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3856489278:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi)
% 25.74/4.33 % (2660907)Instruction limit reached!
% 25.74/4.33 % (2660907)------------------------------
% 25.74/4.33 % (2660907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.74/4.33 % (2660907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660907)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660907)Termination reason: Instruction limit
% 27.66/4.88 % (2660907)Termination phase: Saturation
% 27.66/4.88 % (2660907)Time elapsed: 0.185 s
% 27.66/4.88 % (2660907)Peak memory usage: 117 MB
% 27.66/4.88 % (2660907)Instructions burned: 236 (million)
% 27.66/4.88 % (2660910)Instruction limit reached!
% 27.66/4.88 % (2660910)------------------------------
% 27.66/4.88 % (2660910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/4.88 % (2660910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660910)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660910)Termination reason: Instruction limit
% 27.66/4.88 % (2660910)Termination phase: Saturation
% 27.66/4.88 % (2660910)Time elapsed: 0.104 s
% 27.66/4.88 % (2660910)Peak memory usage: 90 MB
% 27.66/4.88 % (2660910)Instructions burned: 146 (million)
% 27.66/4.88 % (2660908)Instruction limit reached!
% 27.66/4.88 % (2660908)------------------------------
% 27.66/4.88 % (2660908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/4.88 % (2660908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660908)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660908)Termination reason: Instruction limit
% 27.66/4.88 % (2660908)Termination phase: Saturation
% 27.66/4.88 % (2660908)Time elapsed: 0.194 s
% 27.66/4.88 % (2660908)Peak memory usage: 92 MB
% 27.66/4.88 % (2660908)Instructions burned: 273 (million)
% 27.66/4.88 % (2660921)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1455090722:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2971 on theBenchmark for (2971ds/655Mi)
% 27.66/4.88 % (2660923)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=703959563:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 27.66/4.88 % (2660922)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2696354787:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi)
% 27.66/4.88 % (2660923)Refutation not found, incomplete strategy
% 27.66/4.88 % (2660923)------------------------------
% 27.66/4.88 % (2660923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/4.88 % (2660923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660923)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660923)Termination reason: Refutation not found, incomplete strategy
% 27.66/4.88 % (2660923)Time elapsed: 0.040 s
% 27.66/4.88 % (2660923)Peak memory usage: 116 MB
% 27.66/4.88 % (2660923)Instructions burned: 22 (million)
% 27.66/4.88 % (2660924)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1017398957:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 27.66/4.88 % (2660914)Instruction limit reached!
% 27.66/4.88 % (2660914)------------------------------
% 27.66/4.88 % (2660914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/4.88 % (2660914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660914)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660914)Termination reason: Instruction limit
% 27.66/4.88 % (2660914)Termination phase: Saturation
% 27.66/4.88 % (2660914)Time elapsed: 0.226 s
% 27.66/4.88 % (2660914)Peak memory usage: 134 MB
% 27.66/4.88 % (2660914)Instructions burned: 276 (million)
% 27.66/4.88 % (2660916)Instruction limit reached!
% 27.66/4.88 % (2660916)------------------------------
% 27.66/4.88 % (2660916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/4.88 % (2660916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/4.88 % (2660916)CaDiCaL version: 2.1.3
% 27.66/4.88 % (2660916)Termination reason: Instruction limit
% 27.66/4.88 % (2660916)Termination phase: Saturation
% 27.66/4.88 % (2660916)Time elapsed: 0.295 s
% 27.66/4.88 % (2660916)Peak memory usage: 96 MB
% 27.66/4.88 % (2660916)Instructions burned: 1056 (million)
% 27.66/4.88 % (2660929)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
% 27.66/4.88 % (2660929)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2677582680:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi)
% 27.66/4.88 % (2660930)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1535631082:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi)
% 31.39/5.22 % (2660923)------------------------------
% 31.39/5.22 % (2660923)------------------------------
% 31.39/5.22 % (2660930)Instruction limit reached!
% 31.39/5.22 % (2660930)------------------------------
% 31.39/5.22 % (2660930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660930)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660930)Termination reason: Instruction limit
% 31.39/5.22 % (2660930)Termination phase: Saturation
% 31.39/5.22 % (2660930)Time elapsed: 0.043 s
% 31.39/5.22 % (2660930)Peak memory usage: 113 MB
% 31.39/5.22 % (2660930)Instructions burned: 134 (million)
% 31.39/5.22 % (2660921)Instruction limit reached!
% 31.39/5.22 % (2660921)------------------------------
% 31.39/5.22 % (2660921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660921)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660921)Termination reason: Instruction limit
% 31.39/5.22 % (2660921)Termination phase: Saturation
% 31.39/5.22 % (2660921)Time elapsed: 0.358 s
% 31.39/5.22 % (2660921)Peak memory usage: 95 MB
% 31.39/5.22 % (2660921)Instructions burned: 656 (million)
% 31.39/5.22 % (2660924)Instruction limit reached!
% 31.39/5.22 % (2660924)------------------------------
% 31.39/5.22 % (2660924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660924)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660924)Termination reason: Instruction limit
% 31.39/5.22 % (2660924)Termination phase: Saturation
% 31.39/5.22 % (2660924)Time elapsed: 0.321 s
% 31.39/5.22 % (2660924)Peak memory usage: 136 MB
% 31.39/5.22 % (2660924)Instructions burned: 451 (million)
% 31.39/5.22 % (2660934)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=18454518:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi)
% 31.39/5.22 % (2660933)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2724161832:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi)
% 31.39/5.22 % (2660935)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=912014602:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 31.39/5.22 % (2660936)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3287520717:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi)
% 31.39/5.22 % (2660934)Instruction limit reached!
% 31.39/5.22 % (2660934)------------------------------
% 31.39/5.22 % (2660934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660934)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660934)Termination reason: Instruction limit
% 31.39/5.22 % (2660934)Termination phase: Saturation
% 31.39/5.22 % (2660934)Time elapsed: 0.162 s
% 31.39/5.22 % (2660934)Peak memory usage: 93 MB
% 31.39/5.22 % (2660934)Instructions burned: 494 (million)
% 31.39/5.22 % (2660922)Instruction limit reached!
% 31.39/5.22 % (2660922)------------------------------
% 31.39/5.22 % (2660922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660922)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660922)Termination reason: Instruction limit
% 31.39/5.22 % (2660922)Termination phase: Saturation
% 31.39/5.22 % (2660922)Time elapsed: 0.621 s
% 31.39/5.22 % (2660922)Peak memory usage: 97 MB
% 31.39/5.22 % (2660922)Instructions burned: 1054 (million)
% 31.39/5.22 % (2660933)Instruction limit reached!
% 31.39/5.22 % (2660933)------------------------------
% 31.39/5.22 % (2660933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.39/5.22 % (2660933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.39/5.22 % (2660933)CaDiCaL version: 2.1.3
% 31.39/5.22 % (2660933)Termination reason: Instruction limit
% 31.39/5.22 % (2660933)Termination phase: Saturation
% 31.39/5.22 % (2660933)Time elapsed: 0.222 s
% 31.39/5.22 % (2660933)Peak memory usage: 118 MB
% 31.39/5.22 % (2660933)Instructions burned: 312 (million)
% 31.39/5.22 % (2660941)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2598313729:i=776:doe=on:rtra=on_2964 on theBenchmark for (2964ds/776Mi)
% 39.46/6.25 % (2660936)Instruction limit reached!
% 39.46/6.25 % (2660936)------------------------------
% 39.46/6.25 % (2660936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.46/6.25 % (2660936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.46/6.25 % (2660936)CaDiCaL version: 2.1.3
% 39.46/6.25 % (2660936)Termination reason: Instruction limit
% 39.46/6.25 % (2660936)Termination phase: Saturation
% 39.46/6.25 % (2660936)Time elapsed: 0.215 s
% 39.46/6.25 % (2660936)Peak memory usage: 92 MB
% 39.46/6.25 % (2660936)Instructions burned: 307 (million)
% 39.46/6.25 % (2660942)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=453869865:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2964 on theBenchmark for (2964ds/646Mi)
% 39.46/6.25 % (2660943)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=3861693104:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2963 on theBenchmark for (2963ds/784Mi)
% 39.46/6.25 % (2660929)Instruction limit reached!
% 39.46/6.25 % (2660929)------------------------------
% 39.46/6.25 % (2660929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.46/6.25 % (2660929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.46/6.25 % (2660929)CaDiCaL version: 2.1.3
% 39.46/6.25 % (2660929)Termination reason: Instruction limit
% 39.46/6.25 % (2660929)Termination phase: Saturation
% 39.46/6.25 % (2660929)Time elapsed: 0.639 s
% 39.46/6.25 % (2660929)Peak memory usage: 120 MB
% 39.46/6.25 % (2660929)Instructions burned: 1090 (million)
% 39.46/6.25 % (2660945)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=3681863098:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2962 on theBenchmark for (2962ds/1131Mi)
% 39.46/6.25 % (2660941)Instruction limit reached!
% 39.46/6.25 % (2660941)------------------------------
% 39.46/6.25 % (2660941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.46/6.25 % (2660941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.46/6.25 % (2660941)CaDiCaL version: 2.1.3
% 39.46/6.25 % (2660941)Termination reason: Instruction limit
% 39.46/6.25 % (2660941)Termination phase: Saturation
% 39.46/6.25 % (2660941)Time elapsed: 0.268 s
% 39.46/6.25 % (2660941)Peak memory usage: 123 MB
% 39.46/6.25 % (2660941)Instructions burned: 776 (million)
% 39.46/6.25 % (2660935)Instruction limit reached!
% 39.46/6.25 % (2660935)------------------------------
% 39.46/6.25 % (2660935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.46/6.25 % (2660935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.46/6.25 % (2660935)CaDiCaL version: 2.1.3
% 39.46/6.25 % (2660935)Termination reason: Instruction limit
% 39.46/6.25 % (2660935)Termination phase: Saturation
% 39.46/6.25 % (2660935)Time elapsed: 0.534 s
% 39.46/6.25 % (2660935)Peak memory usage: 94 MB
% 39.46/6.25 % (2660935)Instructions burned: 835 (million)
% 39.46/6.25 % (2660948)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=3894335921:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/246Mi)
% 39.46/6.25 % (2660950)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2910191816:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2960 on theBenchmark for (2960ds/775Mi)
% 39.46/6.25 % (2660952)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=654844934:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2960 on theBenchmark for (2960ds/273Mi)
% 39.46/6.25 % (2660948)Instruction limit reached!
% 39.46/6.25 % (2660948)------------------------------
% 39.46/6.25 % (2660948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.46/6.25 % (2660948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.46/6.25 % (2660948)CaDiCaL version: 2.1.3
% 39.46/6.25 % (2660948)Termination reason: Instruction limit
% 39.46/6.25 % (2660948)Termination phase: Saturation
% 39.46/6.25 % (2660948)Time elapsed: 0.182 s
% 39.46/6.25 % (2660948)Peak memory usage: 117 MB
% 39.46/6.25 % (2660948)Instructions burned: 246 (million)
% 39.46/6.25 % (2660942)Instruction limit reached!
% 39.46/6.25 % (2660942)------------------------------
% 39.46/6.25 % (2660942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660942)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660942)Termination reason: Instruction limit
% 50.03/7.99 % (2660942)Termination phase: Saturation
% 50.03/7.99 % (2660942)Time elapsed: 0.465 s
% 50.03/7.99 % (2660942)Peak memory usage: 140 MB
% 50.03/7.99 % (2660942)Instructions burned: 647 (million)
% 50.03/7.99 % (2660943)Instruction limit reached!
% 50.03/7.99 % (2660943)------------------------------
% 50.03/7.99 % (2660943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660943)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660943)Termination reason: Instruction limit
% 50.03/7.99 % (2660943)Termination phase: Saturation
% 50.03/7.99 % (2660943)Time elapsed: 0.480 s
% 50.03/7.99 % (2660943)Peak memory usage: 122 MB
% 50.03/7.99 % (2660943)Instructions burned: 785 (million)
% 50.03/7.99 % (2660950)Instruction limit reached!
% 50.03/7.99 % (2660950)------------------------------
% 50.03/7.99 % (2660950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660950)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660950)Termination reason: Instruction limit
% 50.03/7.99 % (2660950)Termination phase: Saturation
% 50.03/7.99 % (2660950)Time elapsed: 0.246 s
% 50.03/7.99 % (2660950)Peak memory usage: 95 MB
% 50.03/7.99 % (2660950)Instructions burned: 776 (million)
% 50.03/7.99 % (2660955)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2480687876:i=102:nm=16:rtra=on_2958 on theBenchmark for (2958ds/102Mi)
% 50.03/7.99 % (2660952)Instruction limit reached!
% 50.03/7.99 % (2660952)------------------------------
% 50.03/7.99 % (2660952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660952)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660952)Termination reason: Instruction limit
% 50.03/7.99 % (2660952)Termination phase: Saturation
% 50.03/7.99 % (2660952)Time elapsed: 0.191 s
% 50.03/7.99 % (2660952)Peak memory usage: 92 MB
% 50.03/7.99 % (2660952)Instructions burned: 273 (million)
% 50.03/7.99 % (2660956)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=1192429388:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2957 on theBenchmark for (2957ds/1094Mi)
% 50.03/7.99 % (2660955)Instruction limit reached!
% 50.03/7.99 % (2660955)------------------------------
% 50.03/7.99 % (2660955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660955)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660955)Termination reason: Instruction limit
% 50.03/7.99 % (2660955)Termination phase: Saturation
% 50.03/7.99 % (2660955)Time elapsed: 0.067 s
% 50.03/7.99 % (2660955)Peak memory usage: 89 MB
% 50.03/7.99 % (2660955)Instructions burned: 103 (million)
% 50.03/7.99 % (2660957)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=477609162:i=6400:doe=on:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/6400Mi)
% 50.03/7.99 % (2660958)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=2448271745:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/868Mi)
% 50.03/7.99 % (2660960)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=3078280193:i=1846:canc=cautious:fsr=off:rtra=on_2956 on theBenchmark for (2956ds/1846Mi)
% 50.03/7.99 % (2660945)Instruction limit reached!
% 50.03/7.99 % (2660945)------------------------------
% 50.03/7.99 % (2660945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.03/7.99 % (2660945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.03/7.99 % (2660945)CaDiCaL version: 2.1.3
% 50.03/7.99 % (2660945)Termination reason: Instruction limit
% 50.03/7.99 % (2660945)Termination phase: Saturation
% 50.03/7.99 % (2660945)Time elapsed: 0.654 s
% 50.03/7.99 % (2660945)Peak memory usage: 126 MB
% 50.03/7.99 % (2660945)Instructions burned: 1132 (million)
% 50.03/7.99 % (2660962)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=4027708644:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2955 on theBenchmark for (2955ds/36816Mi)
% 61.98/9.42 % (2660966)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2681196461:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2954 on theBenchmark for (2954ds/273Mi)
% 61.98/9.42 % (2660966)Instruction limit reached!
% 61.98/9.42 % (2660966)------------------------------
% 61.98/9.42 % (2660966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660966)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660966)Termination reason: Instruction limit
% 61.98/9.42 % (2660966)Termination phase: Saturation
% 61.98/9.42 % (2660966)Time elapsed: 0.185 s
% 61.98/9.42 % (2660966)Peak memory usage: 92 MB
% 61.98/9.42 % (2660966)Instructions burned: 273 (million)
% 61.98/9.42 % (2660958)Instruction limit reached!
% 61.98/9.42 % (2660958)------------------------------
% 61.98/9.42 % (2660958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660958)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660958)Termination reason: Instruction limit
% 61.98/9.42 % (2660958)Termination phase: Saturation
% 61.98/9.42 % (2660958)Time elapsed: 0.493 s
% 61.98/9.42 % (2660958)Peak memory usage: 120 MB
% 61.98/9.42 % (2660958)Instructions burned: 868 (million)
% 61.98/9.42 % (2660956)Instruction limit reached!
% 61.98/9.42 % (2660956)------------------------------
% 61.98/9.42 % (2660956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660956)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660956)Termination reason: Instruction limit
% 61.98/9.42 % (2660956)Termination phase: Saturation
% 61.98/9.42 % (2660956)Time elapsed: 0.592 s
% 61.98/9.42 % (2660956)Peak memory usage: 99 MB
% 61.98/9.42 % (2660956)Instructions burned: 1096 (million)
% 61.98/9.42 % (2660969)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=3592144682:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2951 on theBenchmark for (2951ds/863Mi)
% 61.98/9.42 % (2660970)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3200614346:i=5811:kws=precedence:nm=0:rtra=on_2950 on theBenchmark for (2950ds/5811Mi)
% 61.98/9.42 % (2660971)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=2138541423:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2950 on theBenchmark for (2950ds/2216Mi)
% 61.98/9.42 % (2660960)Instruction limit reached!
% 61.98/9.42 % (2660960)------------------------------
% 61.98/9.42 % (2660960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660960)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660960)Termination reason: Instruction limit
% 61.98/9.42 % (2660960)Termination phase: Saturation
% 61.98/9.42 % (2660960)Time elapsed: 0.926 s
% 61.98/9.42 % (2660960)Peak memory usage: 96 MB
% 61.98/9.42 % (2660960)Instructions burned: 1847 (million)
% 61.98/9.42 % (2660911)Instruction limit reached!
% 61.98/9.42 % (2660911)------------------------------
% 61.98/9.42 % (2660911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660911)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660911)Termination reason: Instruction limit
% 61.98/9.42 % (2660911)Termination phase: Saturation
% 61.98/9.42 % (2660911)Time elapsed: 2.738 s
% 61.98/9.42 % (2660911)Peak memory usage: 122 MB
% 61.98/9.42 % (2660911)Instructions burned: 4429 (million)
% 61.98/9.42 % (2660969)Instruction limit reached!
% 61.98/9.42 % (2660969)------------------------------
% 61.98/9.42 % (2660969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.98/9.42 % (2660969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.98/9.42 % (2660969)CaDiCaL version: 2.1.3
% 61.98/9.42 % (2660969)Termination reason: Instruction limit
% 61.98/9.42 % (2660969)Termination phase: Saturation
% 61.98/9.42 % (2660969)Time elapsed: 0.495 s
% 61.98/9.42 % (2660969)Peak memory usage: 120 MB
% 61.98/9.42 % (2660969)Instructions burned: 863 (million)
% 61.98/9.42 % (2660975)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3664827472:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2945 on theBenchmark for (2945ds/801Mi)
% 90.30/13.46 % (2660976)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=2404922676:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2945 on theBenchmark for (2945ds/1026Mi)
% 90.30/13.46 % (2660977)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=696874998:i=3509:rtra=on_2944 on theBenchmark for (2944ds/3509Mi)
% 90.30/13.46 % (2660975)Instruction limit reached!
% 90.30/13.46 % (2660975)------------------------------
% 90.30/13.46 % (2660975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660975)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660975)Termination reason: Instruction limit
% 90.30/13.46 % (2660975)Termination phase: Saturation
% 90.30/13.46 % (2660975)Time elapsed: 0.423 s
% 90.30/13.46 % (2660975)Peak memory usage: 96 MB
% 90.30/13.46 % (2660975)Instructions burned: 801 (million)
% 90.30/13.46 % (2660981)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=1931372409:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2939 on theBenchmark for (2939ds/2127Mi)
% 90.30/13.46 % (2660976)Instruction limit reached!
% 90.30/13.46 % (2660976)------------------------------
% 90.30/13.46 % (2660976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660976)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660976)Termination reason: Instruction limit
% 90.30/13.46 % (2660976)Termination phase: Saturation
% 90.30/13.46 % (2660976)Time elapsed: 0.605 s
% 90.30/13.46 % (2660976)Peak memory usage: 97 MB
% 90.30/13.46 % (2660976)Instructions burned: 1026 (million)
% 90.30/13.46 % (2660971)Instruction limit reached!
% 90.30/13.46 % (2660971)------------------------------
% 90.30/13.46 % (2660971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660971)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660971)Termination reason: Instruction limit
% 90.30/13.46 % (2660971)Termination phase: Saturation
% 90.30/13.46 % (2660971)Time elapsed: 1.252 s
% 90.30/13.46 % (2660971)Peak memory usage: 135 MB
% 90.30/13.46 % (2660971)Instructions burned: 2217 (million)
% 90.30/13.46 % (2660983)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=444257760:i=1959:rtra=on:fsd=on:proc=on_2937 on theBenchmark for (2937ds/1959Mi)
% 90.30/13.46 % (2660957)Instruction limit reached!
% 90.30/13.46 % (2660957)------------------------------
% 90.30/13.46 % (2660957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660957)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660957)Termination reason: Instruction limit
% 90.30/13.46 % (2660957)Termination phase: Saturation
% 90.30/13.46 % (2660957)Time elapsed: 2.045 s
% 90.30/13.46 % (2660957)Peak memory usage: 132 MB
% 90.30/13.46 % (2660957)Instructions burned: 6401 (million)
% 90.30/13.46 % (2660984)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1555906608:s2a=on:i=3553:nm=0:rtra=on_2936 on theBenchmark for (2936ds/3553Mi)
% 90.30/13.46 % (2660986)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=308899705:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2935 on theBenchmark for (2935ds/3201Mi)
% 90.30/13.46 % (2660986)Instruction limit reached!
% 90.30/13.46 % (2660986)------------------------------
% 90.30/13.46 % (2660986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660986)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660986)Termination reason: Instruction limit
% 90.30/13.46 % (2660986)Termination phase: Saturation
% 90.30/13.46 % (2660986)Time elapsed: 0.720 s
% 90.30/13.46 % (2660986)Peak memory usage: 94 MB
% 90.30/13.46 % (2660986)Instructions burned: 3206 (million)
% 90.30/13.46 % (2660981)Instruction limit reached!
% 90.30/13.46 % (2660981)------------------------------
% 90.30/13.46 % (2660981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660981)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660981)Termination reason: Instruction limit
% 90.30/13.46 % (2660981)Termination phase: Saturation
% 90.30/13.46 % (2660981)Time elapsed: 1.133 s
% 90.30/13.46 % (2660981)Peak memory usage: 106 MB
% 90.30/13.46 % (2660981)Instructions burned: 2128 (million)
% 90.30/13.46 % (2660990)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=3078747869:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2926 on theBenchmark for (2926ds/21173Mi)
% 90.30/13.46 % (2660983)Instruction limit reached!
% 90.30/13.46 % (2660983)------------------------------
% 90.30/13.46 % (2660983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660983)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660983)Termination reason: Instruction limit
% 90.30/13.46 % (2660983)Termination phase: Saturation
% 90.30/13.46 % (2660983)Time elapsed: 1.059 s
% 90.30/13.46 % (2660983)Peak memory usage: 122 MB
% 90.30/13.46 % (2660983)Instructions burned: 1960 (million)
% 90.30/13.46 % (2660989)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=888054855:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2926 on theBenchmark for (2926ds/4093Mi)
% 90.30/13.46 % (2660992)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=2105487173:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2925 on theBenchmark for (2925ds/10544Mi)
% 90.30/13.46 % (2660977)Instruction limit reached!
% 90.30/13.46 % (2660977)------------------------------
% 90.30/13.46 % (2660977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660977)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660977)Termination reason: Instruction limit
% 90.30/13.46 % (2660977)Termination phase: Saturation
% 90.30/13.46 % (2660977)Time elapsed: 2.165 s
% 90.30/13.46 % (2660977)Peak memory usage: 108 MB
% 90.30/13.46 % (2660977)Instructions burned: 3510 (million)
% 90.30/13.46 % (2660995)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=4084447915:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2921 on theBenchmark for (2921ds/1262Mi)
% 90.30/13.46 % (2660970)Instruction limit reached!
% 90.30/13.46 % (2660970)------------------------------
% 90.30/13.46 % (2660970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660970)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660970)Termination reason: Instruction limit
% 90.30/13.46 % (2660970)Termination phase: Saturation
% 90.30/13.46 % (2660970)Time elapsed: 3.004 s
% 90.30/13.46 % (2660970)Peak memory usage: 143 MB
% 90.30/13.46 % (2660970)Instructions burned: 5812 (million)
% 90.30/13.46 % (2660997)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1906970529:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/775Mi)
% 90.30/13.46 % (2660984)Instruction limit reached!
% 90.30/13.46 % (2660984)------------------------------
% 90.30/13.46 % (2660984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660984)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660984)Termination reason: Instruction limit
% 90.30/13.46 % (2660984)Termination phase: Saturation
% 90.30/13.46 % (2660984)Time elapsed: 1.882 s
% 90.30/13.46 % (2660984)Peak memory usage: 109 MB
% 90.30/13.46 % (2660984)Instructions burned: 3554 (million)
% 90.30/13.46 % (2660999)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2434310936:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2915 on theBenchmark for (2915ds/270Mi)
% 90.30/13.46 % (2660997)Instruction limit reached!
% 90.30/13.46 % (2660997)------------------------------
% 90.30/13.46 % (2660997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660997)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660997)Termination reason: Instruction limit
% 90.30/13.46 % (2660997)Termination phase: Saturation
% 90.30/13.46 % (2660997)Time elapsed: 0.449 s
% 90.30/13.46 % (2660997)Peak memory usage: 95 MB
% 90.30/13.46 % (2660997)Instructions burned: 777 (million)
% 90.30/13.46 % (2660999)Instruction limit reached!
% 90.30/13.46 % (2660999)------------------------------
% 90.30/13.46 % (2660999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660999)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660999)Termination reason: Instruction limit
% 90.30/13.46 % (2660999)Termination phase: Saturation
% 90.30/13.46 % (2660999)Time elapsed: 0.183 s
% 90.30/13.46 % (2660999)Peak memory usage: 92 MB
% 90.30/13.46 % (2660999)Instructions burned: 270 (million)
% 90.30/13.46 % (2660995)Instruction limit reached!
% 90.30/13.46 % (2660995)------------------------------
% 90.30/13.46 % (2660995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660995)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660995)Termination reason: Instruction limit
% 90.30/13.46 % (2660995)Termination phase: Saturation
% 90.30/13.46 % (2660995)Time elapsed: 0.728 s
% 90.30/13.46 % (2660995)Peak memory usage: 126 MB
% 90.30/13.46 % (2660995)Instructions burned: 1263 (million)
% 90.30/13.46 % (2661001)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2795546592:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2912 on theBenchmark for (2912ds/17165Mi)
% 90.30/13.46 % (2661002)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2912944309:s2a=on:i=13094:s2at=-1:rtra=on_2912 on theBenchmark for (2912ds/13094Mi)
% 90.30/13.46 % (2661003)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=422539068:st=2:i=12633:rtra=on:ss=axioms_2911 on theBenchmark for (2911ds/12633Mi)
% 90.30/13.46 % (2660989)Instruction limit reached!
% 90.30/13.46 % (2660989)------------------------------
% 90.30/13.46 % (2660989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660989)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660989)Termination reason: Instruction limit
% 90.30/13.46 % (2660989)Termination phase: Saturation
% 90.30/13.46 % (2660989)Time elapsed: 2.078 s
% 90.30/13.46 % (2660989)Peak memory usage: 154 MB
% 90.30/13.46 % (2660989)Instructions burned: 4094 (million)
% 90.30/13.46 % (2661007)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=34430101:i=1783:rtra=on:gtg=position_2904 on theBenchmark for (2904ds/1783Mi)
% 90.30/13.46 % (2661007)Instruction limit reached!
% 90.30/13.46 % (2661007)------------------------------
% 90.30/13.46 % (2661007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2661007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2661007)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2661007)Termination reason: Instruction limit
% 90.30/13.46 % (2661007)Termination phase: Saturation
% 90.30/13.46 % (2661007)Time elapsed: 1.059 s
% 90.30/13.46 % (2661007)Peak memory usage: 121 MB
% 90.30/13.46 % (2661007)Instructions burned: 1784 (million)
% 90.30/13.46 % (2661009)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=3522425045:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2892 on theBenchmark for (2892ds/5451Mi)
% 90.30/13.46 % (2660990)Instruction limit reached!
% 90.30/13.46 % (2660990)------------------------------
% 90.30/13.46 % (2660990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.30/13.46 % (2660990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.30/13.46 % (2660990)CaDiCaL version: 2.1.3
% 90.30/13.46 % (2660990)Termination reason: Instruction limit
% 90.30/13.46 % (2660990)Termination phase: Saturation
% 90.30/13.46 % (2660990)Time elapsed: 4.893 s
% 90.30/13.46 % (2660990)Peak memory usage: 125 MB
% 90.30/13.46 % (2660990)Instructions burned: 21185 (million)
% 90.30/13.46 % (2661011)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=2427658611:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2876 on theBenchmark for (2876ds/4975Mi)
% 90.30/13.46 % (2661009)First to succeed.
% 90.30/13.46 % (2661009)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2660768"
% 90.30/13.46 % (2661009)Refutation found. Thanks to Tanya!
% 90.30/13.46 % SZS status Theorem for theBenchmark
% 90.30/13.46 % SZS output start Proof for theBenchmark
% See solution above
% 91.23/13.65 % (2661009)------------------------------
% 91.23/13.65 % (2661009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.23/13.65 % (2661009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.23/13.65 % (2661009)CaDiCaL version: 2.1.3
% 91.23/13.65 % (2661009)Termination reason: Refutation
% 91.23/13.65 % (2661009)Time elapsed: 1.546 s
% 91.23/13.65 % (2661009)Peak memory usage: 127 MB
% 91.23/13.65 % (2661009)Instructions burned: 2846 (million)
% 91.23/13.65 % (2661009)------------------------------
% 91.23/13.65 % (2661009)------------------------------
% 91.23/13.65 % (2660768)Success in time 12.792 s
% 91.23/13.65 % Vampire exiting
%------------------------------------------------------------------------------