%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW603_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 : n005.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:55 PM UTC 2026
% Result : Theorem 26.53s 4.47s
% Output : Refutation 27.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 19
% Syntax : Number of formulae : 131 ( 60 unt; 0 typ; 8 def)
% Number of atoms : 502 ( 155 equ)
% Maximal formula atoms : 25 ( 3 avg)
% Number of connectives : 516 ( 145 ~; 147 |; 163 &)
% ( 15 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 52 ( 18 atm; 0 fun; 18 num; 16 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 88 ( 71 usr; 29 con; 0-5 aty)
% Number of variables : 279 ( 201 !; 78 ?; 279 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
tree1: $tType ).
tff(type_def_10,type,
list_tree: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_18,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
length2: ( ty * uni ) > $int ).
tff(func_def_22,type,
map: ( ty * ty ) > ty ).
tff(func_def_23,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_24,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_25,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_26,type,
array: ty > ty ).
tff(func_def_27,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
length3: ( ty * uni ) > $int ).
tff(func_def_29,type,
elts: ( ty * uni ) > uni ).
tff(func_def_30,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_31,type,
t2tb: $int > uni ).
tff(func_def_32,type,
tb2t: uni > $int ).
tff(func_def_33,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_34,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_35,type,
tree: ty ).
tff(func_def_36,type,
empty1: tree1 ).
tff(func_def_37,type,
node1: ( tree1 * tree1 ) > tree1 ).
tff(func_def_38,type,
match_tree1: ( ty * tree1 * uni * uni ) > uni ).
tff(func_def_39,type,
node_proj_11: tree1 > tree1 ).
tff(func_def_40,type,
node_proj_21: tree1 > tree1 ).
tff(func_def_41,type,
size1: tree1 > $int ).
tff(func_def_42,type,
t2tb1: list_tree > uni ).
tff(func_def_43,type,
tb2t1: uni > list_tree ).
tff(func_def_44,type,
t2tb2: tree1 > uni ).
tff(func_def_45,type,
tb2t2: uni > tree1 ).
tff(func_def_46,type,
sK0: ( uni * ty ) > uni ).
tff(func_def_47,type,
sK1: ( uni * ty ) > uni ).
tff(func_def_48,type,
sK2: ( uni * ty ) > uni ).
tff(func_def_49,type,
sK3: $int ).
tff(func_def_50,type,
sK4: $int ).
tff(func_def_51,type,
sK5: list_tree ).
tff(func_def_52,type,
sK6: list_tree ).
tff(func_def_53,type,
sK7: list_tree ).
tff(func_def_54,type,
sK8: list_tree ).
tff(func_def_55,type,
sK9: tree1 ).
tff(func_def_56,type,
sK10: list_tree ).
tff(func_def_57,type,
sK11: tree1 > tree1 ).
tff(func_def_58,type,
sK12: tree1 > tree1 ).
tff(func_def_59,type,
sK13: list_tree ).
tff(func_def_60,type,
sK14: tree1 > tree1 ).
tff(func_def_61,type,
sK15: ( uni * ty * uni ) > uni ).
tff(func_def_62,type,
sK16: ( uni * ty * uni ) > uni ).
tff(func_def_63,type,
sK17: tree1 > tree1 ).
tff(func_def_64,type,
sK18: tree1 > tree1 ).
tff(func_def_65,type,
sK19: ( uni * uni * ty ) > uni ).
tff(func_def_66,type,
sF20: uni ).
tff(func_def_67,type,
sF21: uni ).
tff(func_def_68,type,
sF22: uni ).
tff(func_def_69,type,
sF23: uni ).
tff(func_def_70,type,
sF24: list_tree ).
tff(func_def_71,type,
sF25: uni ).
tff(func_def_72,type,
sF26: uni ).
tff(func_def_73,type,
sF27: uni ).
tff(func_def_74,type,
sF28: uni ).
tff(func_def_85,type,
2: $int > $int ).
tff(func_def_86,type,
3: $int > $int ).
tff(func_def_87,type,
4: $int > $int ).
tff(func_def_88,type,
5: $int > $int ).
tff(func_def_89,type,
6: $int > $int ).
tff(func_def_90,type,
7: $int > $int ).
tff(func_def_91,type,
8: $int > $int ).
tff(func_def_92,type,
9: $int > $int ).
tff(func_def_93,type,
10: $int > $int ).
tff(func_def_94,type,
11: $int > $int ).
tff(func_def_95,type,
12: $int > $int ).
tff(func_def_97,type,
13: $int > $int ).
tff(func_def_99,type,
14: $int > $int ).
tff(func_def_101,type,
15: $int > $int ).
tff(func_def_103,type,
16: $int > $int ).
tff(func_def_105,type,
17: $int > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
distinct: ( ty * uni ) > $o ).
tff(pred_def_6,type,
all_trees1: ( $int * list_tree ) > $o ).
tff(f14,axiom,
! [X2: uni,X1: uni,X0: ty] : ( nil(X0) != cons(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nil_Cons1) ).
tff(f16,axiom,
! [X1: uni,X0: ty,X2: uni] :
( sort1(X0,X1)
=> ( cons_proj_11(X0,cons(X0,X1,X2)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_1_def1) ).
tff(f18,axiom,
! [X2: uni,X0: ty,X1: uni] : ( cons_proj_21(X0,cons(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_2_def1) ).
tff(f20,axiom,
! [X1: uni,X0: ty] :
( sort1(X0,X1)
=> ( ~ mem(X0,X1,nil(X0))
& ! [X3: uni,X2: uni] :
( sort1(X0,X2)
=> ( ( ( X1 = X2 )
| mem(X0,X1,X3) )
<=> mem(X0,X1,cons(X0,X2,X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def) ).
tff(f34,axiom,
! [X1: uni,X0: ty] :
( distinct(X0,X1)
=> ( ( X1 = nil(X0) )
| ? [X2: uni,X3: uni] :
( distinct(X0,X3)
& sort1(X0,X2)
& sort1(list(X0),X3)
& ~ mem(X0,X2,X3)
& ( X1 = cons(X0,X2,X3) ) )
| ? [X2: uni] :
( sort1(X0,X2)
& ( X1 = cons(X0,X2,nil(X0)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distinct_inversion) ).
tff(f35,axiom,
! [X2: uni,X1: uni,X0: ty] :
( distinct(X0,X1)
=> ( distinct(X0,X2)
=> ( ! [X3: uni] :
( sort1(X0,X3)
=> ( mem(X0,X3,X1)
=> ~ mem(X0,X3,X2) ) )
=> distinct(X0,infix_plpl(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distinct_append) ).
tff(f60,axiom,
! [X1: tree1,X0: tree1] : ( node_proj_11(node1(X0,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',node_proj_1_def1) ).
tff(f68,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f69,axiom,
! [X0: tree1] : sort1(tree,t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f71,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f75,conjecture,
! [X2: $int,X3: list_tree,X1: list_tree,X0: $int] :
( ( $lesseq(0,X0)
& all_trees1(X0,X1)
& all_trees1(X2,X3)
& $lesseq(0,X2) )
=> ! [X4: list_tree] :
( distinct(tree,t2tb1(X4))
=> ! [X6: list_tree,X5: tree1] :
( ( X4 = tb2t1(cons(tree,t2tb2(X5),t2tb1(X6))) )
=> ( distinct(tree,t2tb1(X6))
=> ! [X7: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X7))
<=> ? [X10: tree1,X9: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X9,X10) )
& mem(tree,t2tb2(X9),t2tb1(X6)) ) )
& distinct(tree,t2tb1(X7)) )
=> ( distinct(tree,t2tb1(X3))
=> ! [X11: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X11))
<=> ? [X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X5,X10) ) ) )
& distinct(tree,t2tb1(X11)) )
=> distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_combine) ).
tff(f76,negated_conjecture,
~ ! [X2: $int,X3: list_tree,X1: list_tree,X0: $int] :
( ( $lesseq(0,X0)
& all_trees1(X0,X1)
& all_trees1(X2,X3)
& $lesseq(0,X2) )
=> ! [X4: list_tree] :
( distinct(tree,t2tb1(X4))
=> ! [X6: list_tree,X5: tree1] :
( ( X4 = tb2t1(cons(tree,t2tb2(X5),t2tb1(X6))) )
=> ( distinct(tree,t2tb1(X6))
=> ! [X7: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X7))
<=> ? [X10: tree1,X9: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X9,X10) )
& mem(tree,t2tb2(X9),t2tb1(X6)) ) )
& distinct(tree,t2tb1(X7)) )
=> ( distinct(tree,t2tb1(X3))
=> ! [X11: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X11))
<=> ? [X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X5,X10) ) ) )
& distinct(tree,t2tb1(X11)) )
=> distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7))) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f75]) ).
tff(f77,plain,
~ ! [X2: $int,X3: list_tree,X1: list_tree,X0: $int] :
( ( ~ $less(X0,0)
& all_trees1(X0,X1)
& all_trees1(X2,X3)
& ~ $less(X2,0) )
=> ! [X4: list_tree] :
( distinct(tree,t2tb1(X4))
=> ! [X6: list_tree,X5: tree1] :
( ( X4 = tb2t1(cons(tree,t2tb2(X5),t2tb1(X6))) )
=> ( distinct(tree,t2tb1(X6))
=> ! [X7: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X7))
<=> ? [X10: tree1,X9: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X9,X10) )
& mem(tree,t2tb2(X9),t2tb1(X6)) ) )
& distinct(tree,t2tb1(X7)) )
=> ( distinct(tree,t2tb1(X3))
=> ! [X11: list_tree] :
( ( ! [X8: tree1] :
( mem(tree,t2tb2(X8),t2tb1(X11))
<=> ? [X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X3))
& ( X8 = node1(X5,X10) ) ) )
& distinct(tree,t2tb1(X11)) )
=> distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7))) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f76]) ).
tff(f81,plain,
~ ! [X0: $int,X2: list_tree,X3: $int,X1: list_tree] :
( ( ~ $less(X0,0)
& ~ $less(X3,0)
& all_trees1(X0,X1)
& all_trees1(X3,X2) )
=> ! [X4: list_tree] :
( distinct(tree,t2tb1(X4))
=> ! [X5: list_tree,X6: tree1] :
( ( tb2t1(cons(tree,t2tb2(X6),t2tb1(X5))) = X4 )
=> ( distinct(tree,t2tb1(X5))
=> ! [X7: list_tree] :
( ( ! [X8: tree1] :
( ? [X9: tree1,X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X5))
& mem(tree,t2tb2(X9),t2tb1(X1))
& ( node1(X10,X9) = X8 ) )
<=> mem(tree,t2tb2(X8),t2tb1(X7)) )
& distinct(tree,t2tb1(X7)) )
=> ( distinct(tree,t2tb1(X1))
=> ! [X11: list_tree] :
( ( ! [X12: tree1] :
( ? [X13: tree1] :
( mem(tree,t2tb2(X13),t2tb1(X1))
& ( node1(X6,X13) = X12 ) )
<=> mem(tree,t2tb2(X12),t2tb1(X11)) )
& distinct(tree,t2tb1(X11)) )
=> distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7))) ) ) ) ) ) ) ),
inference(rectify,[],[f77]) ).
tff(f82,plain,
! [X1: uni,X0: uni,X2: ty] : ( cons(X2,X1,X0) != nil(X2) ),
inference(rectify,[],[f14]) ).
tff(f83,plain,
! [X1: ty,X0: uni] :
( distinct(X1,X0)
=> ( ? [X2: uni,X3: uni] :
( ~ mem(X1,X2,X3)
& sort1(list(X1),X3)
& sort1(X1,X2)
& ( cons(X1,X2,X3) = X0 )
& distinct(X1,X3) )
| ( nil(X1) = X0 )
| ? [X4: uni] :
( sort1(X1,X4)
& ( cons(X1,X4,nil(X1)) = X0 ) ) ) ),
inference(rectify,[],[f34]) ).
tff(f84,plain,
! [X1: ty,X0: uni] :
( sort1(X1,X0)
=> ( ! [X3: uni,X2: uni] :
( sort1(X1,X3)
=> ( mem(X1,X0,cons(X1,X3,X2))
<=> ( mem(X1,X0,X2)
| ( X0 = X3 ) ) ) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(rectify,[],[f20]) ).
tff(f87,plain,
! [X2: ty,X0: uni,X1: uni] :
( distinct(X2,X1)
=> ( distinct(X2,X0)
=> ( ! [X3: uni] :
( sort1(X2,X3)
=> ( mem(X2,X3,X1)
=> ~ mem(X2,X3,X0) ) )
=> distinct(X2,infix_plpl(X2,X1,X0)) ) ) ),
inference(rectify,[],[f35]) ).
tff(f93,plain,
! [X2: uni,X0: uni,X1: ty] :
( sort1(X1,X0)
=> ( cons_proj_11(X1,cons(X1,X0,X2)) = X0 ) ),
inference(rectify,[],[f16]) ).
tff(f95,plain,
! [X1: ty,X0: uni,X2: uni] : ( cons_proj_21(X1,cons(X1,X2,X0)) = X0 ),
inference(rectify,[],[f18]) ).
tff(f103,plain,
! [X0: tree1,X1: tree1] : ( node_proj_11(node1(X1,X0)) = X1 ),
inference(rectify,[],[f60]) ).
tff(f113,plain,
! [X2: uni,X1: ty,X0: uni] :
( ( cons_proj_11(X1,cons(X1,X0,X2)) = X0 )
| ~ sort1(X1,X0) ),
inference(ennf_transformation,[],[f93]) ).
tff(f114,plain,
? [X0: $int,X2: list_tree,X3: $int,X1: list_tree] :
( ? [X4: list_tree] :
( ? [X5: list_tree,X6: tree1] :
( ? [X7: list_tree] :
( ? [X11: list_tree] :
( ~ distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7)))
& ! [X12: tree1] :
( ? [X13: tree1] :
( mem(tree,t2tb2(X13),t2tb1(X1))
& ( node1(X6,X13) = X12 ) )
<=> mem(tree,t2tb2(X12),t2tb1(X11)) )
& distinct(tree,t2tb1(X11)) )
& distinct(tree,t2tb1(X1))
& ! [X8: tree1] :
( ? [X9: tree1,X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X5))
& mem(tree,t2tb2(X9),t2tb1(X1))
& ( node1(X10,X9) = X8 ) )
<=> mem(tree,t2tb2(X8),t2tb1(X7)) )
& distinct(tree,t2tb1(X7)) )
& distinct(tree,t2tb1(X5))
& ( tb2t1(cons(tree,t2tb2(X6),t2tb1(X5))) = X4 ) )
& distinct(tree,t2tb1(X4)) )
& ~ $less(X0,0)
& ~ $less(X3,0)
& all_trees1(X0,X1)
& all_trees1(X3,X2) ),
inference(ennf_transformation,[],[f81]) ).
tff(f115,plain,
? [X0: $int,X3: $int,X1: list_tree,X2: list_tree] :
( ~ $less(X3,0)
& all_trees1(X0,X1)
& ~ $less(X0,0)
& ? [X4: list_tree] :
( distinct(tree,t2tb1(X4))
& ? [X5: list_tree,X6: tree1] :
( distinct(tree,t2tb1(X5))
& ( tb2t1(cons(tree,t2tb2(X6),t2tb1(X5))) = X4 )
& ? [X7: list_tree] :
( ! [X8: tree1] :
( ? [X9: tree1,X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X5))
& mem(tree,t2tb2(X9),t2tb1(X1))
& ( node1(X10,X9) = X8 ) )
<=> mem(tree,t2tb2(X8),t2tb1(X7)) )
& distinct(tree,t2tb1(X1))
& ? [X11: list_tree] :
( ! [X12: tree1] :
( ? [X13: tree1] :
( mem(tree,t2tb2(X13),t2tb1(X1))
& ( node1(X6,X13) = X12 ) )
<=> mem(tree,t2tb2(X12),t2tb1(X11)) )
& ~ distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7)))
& distinct(tree,t2tb1(X11)) )
& distinct(tree,t2tb1(X7)) ) ) )
& all_trees1(X3,X2) ),
inference(flattening,[],[f114]) ).
tff(f116,plain,
! [X2: ty,X0: uni,X1: uni] :
( distinct(X2,infix_plpl(X2,X1,X0))
| ? [X3: uni] :
( mem(X2,X3,X0)
& mem(X2,X3,X1)
& sort1(X2,X3) )
| ~ distinct(X2,X0)
| ~ distinct(X2,X1) ),
inference(ennf_transformation,[],[f87]) ).
tff(f117,plain,
! [X1: uni,X0: uni,X2: ty] :
( distinct(X2,infix_plpl(X2,X1,X0))
| ~ distinct(X2,X1)
| ~ distinct(X2,X0)
| ? [X3: uni] :
( mem(X2,X3,X1)
& sort1(X2,X3)
& mem(X2,X3,X0) ) ),
inference(flattening,[],[f116]) ).
tff(f124,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( mem(X1,X0,cons(X1,X3,X2))
<=> ( mem(X1,X0,X2)
| ( X0 = X3 ) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(ennf_transformation,[],[f84]) ).
tff(f129,plain,
! [X1: ty,X0: uni] :
( ? [X2: uni,X3: uni] :
( ~ mem(X1,X2,X3)
& sort1(list(X1),X3)
& sort1(X1,X2)
& ( cons(X1,X2,X3) = X0 )
& distinct(X1,X3) )
| ( nil(X1) = X0 )
| ? [X4: uni] :
( sort1(X1,X4)
& ( cons(X1,X4,nil(X1)) = X0 ) )
| ~ distinct(X1,X0) ),
inference(ennf_transformation,[],[f83]) ).
tff(f130,plain,
! [X0: uni,X1: ty] :
( ? [X4: uni] :
( sort1(X1,X4)
& ( cons(X1,X4,nil(X1)) = X0 ) )
| ( nil(X1) = X0 )
| ~ distinct(X1,X0)
| ? [X2: uni,X3: uni] :
( ~ mem(X1,X2,X3)
& sort1(list(X1),X3)
& sort1(X1,X2)
& ( cons(X1,X2,X3) = X0 )
& distinct(X1,X3) ) ),
inference(flattening,[],[f129]) ).
tff(f133,plain,
! [X0: uni,X1: ty] :
( ? [X2: uni] :
( sort1(X1,X2)
& ( cons(X1,X2,nil(X1)) = X0 ) )
| ( nil(X1) = X0 )
| ~ distinct(X1,X0)
| ? [X3: uni,X4: uni] :
( ~ mem(X1,X3,X4)
& sort1(list(X1),X4)
& sort1(X1,X3)
& ( cons(X1,X3,X4) = X0 )
& distinct(X1,X4) ) ),
inference(rectify,[],[f130]) ).
tff(f134,plain,
! [X0: uni,X1: ty] :
( ( sort1(X1,sK0(X0,X1))
& ( cons(X1,sK0(X0,X1),nil(X1)) = X0 ) )
| ( nil(X1) = X0 )
| ~ distinct(X1,X0)
| ( ~ mem(X1,sK1(X0,X1),sK2(X0,X1))
& sort1(list(X1),sK2(X0,X1))
& sort1(X1,sK1(X0,X1))
& ( cons(X1,sK1(X0,X1),sK2(X0,X1)) = X0 )
& distinct(X1,sK2(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X2,sK0(X0,X1)),skolemize(X3,sK1(X0,X1)),skolemize(X4,sK2(X0,X1))],[f133]) ).
tff(f138,plain,
! [X0: ty,X1: uni,X2: uni] : ( cons_proj_21(X0,cons(X0,X2,X1)) = X1 ),
inference(rectify,[],[f95]) ).
tff(f141,plain,
! [X0: uni,X1: ty,X2: uni] :
( ( cons_proj_11(X1,cons(X1,X2,X0)) = X2 )
| ~ sort1(X1,X2) ),
inference(rectify,[],[f113]) ).
tff(f142,plain,
! [X0: uni,X1: uni,X2: ty] : ( cons(X2,X0,X1) != nil(X2) ),
inference(rectify,[],[f82]) ).
tff(f146,plain,
? [X0: $int,X3: $int,X1: list_tree,X2: list_tree] :
( ~ $less(X3,0)
& all_trees1(X0,X1)
& ~ $less(X0,0)
& ? [X4: list_tree] :
( distinct(tree,t2tb1(X4))
& ? [X5: list_tree,X6: tree1] :
( distinct(tree,t2tb1(X5))
& ( tb2t1(cons(tree,t2tb2(X6),t2tb1(X5))) = X4 )
& ? [X7: list_tree] :
( ! [X8: tree1] :
( ( ? [X9: tree1,X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X5))
& mem(tree,t2tb2(X9),t2tb1(X1))
& ( node1(X10,X9) = X8 ) )
| ~ mem(tree,t2tb2(X8),t2tb1(X7)) )
& ( mem(tree,t2tb2(X8),t2tb1(X7))
| ! [X9: tree1,X10: tree1] :
( ~ mem(tree,t2tb2(X10),t2tb1(X5))
| ~ mem(tree,t2tb2(X9),t2tb1(X1))
| ( node1(X10,X9) != X8 ) ) ) )
& distinct(tree,t2tb1(X1))
& ? [X11: list_tree] :
( ! [X12: tree1] :
( ( ? [X13: tree1] :
( mem(tree,t2tb2(X13),t2tb1(X1))
& ( node1(X6,X13) = X12 ) )
| ~ mem(tree,t2tb2(X12),t2tb1(X11)) )
& ( mem(tree,t2tb2(X12),t2tb1(X11))
| ! [X13: tree1] :
( ~ mem(tree,t2tb2(X13),t2tb1(X1))
| ( node1(X6,X13) != X12 ) ) ) )
& ~ distinct(tree,infix_plpl(tree,t2tb1(X11),t2tb1(X7)))
& distinct(tree,t2tb1(X11)) )
& distinct(tree,t2tb1(X7)) ) ) )
& all_trees1(X3,X2) ),
inference(nnf_transformation,[],[f115]) ).
tff(f147,plain,
? [X0: $int,X1: $int,X2: list_tree,X3: list_tree] :
( ~ $less(X1,0)
& all_trees1(X0,X2)
& ~ $less(X0,0)
& ? [X4: list_tree] :
( distinct(tree,t2tb1(X4))
& ? [X5: list_tree,X6: tree1] :
( distinct(tree,t2tb1(X5))
& ( tb2t1(cons(tree,t2tb2(X6),t2tb1(X5))) = X4 )
& ? [X7: list_tree] :
( ! [X8: tree1] :
( ( ? [X9: tree1,X10: tree1] :
( mem(tree,t2tb2(X10),t2tb1(X5))
& mem(tree,t2tb2(X9),t2tb1(X2))
& ( node1(X10,X9) = X8 ) )
| ~ mem(tree,t2tb2(X8),t2tb1(X7)) )
& ( mem(tree,t2tb2(X8),t2tb1(X7))
| ! [X11: tree1,X12: tree1] :
( ~ mem(tree,t2tb2(X12),t2tb1(X5))
| ~ mem(tree,t2tb2(X11),t2tb1(X2))
| ( node1(X12,X11) != X8 ) ) ) )
& distinct(tree,t2tb1(X2))
& ? [X13: list_tree] :
( ! [X14: tree1] :
( ( ? [X15: tree1] :
( mem(tree,t2tb2(X15),t2tb1(X2))
& ( node1(X6,X15) = X14 ) )
| ~ mem(tree,t2tb2(X14),t2tb1(X13)) )
& ( mem(tree,t2tb2(X14),t2tb1(X13))
| ! [X16: tree1] :
( ~ mem(tree,t2tb2(X16),t2tb1(X2))
| ( node1(X6,X16) != X14 ) ) ) )
& ~ distinct(tree,infix_plpl(tree,t2tb1(X13),t2tb1(X7)))
& distinct(tree,t2tb1(X13)) )
& distinct(tree,t2tb1(X7)) ) ) )
& all_trees1(X1,X3) ),
inference(rectify,[],[f146]) ).
tff(f148,plain,
( ~ $less(sK4,0)
& all_trees1(sK3,sK5)
& ~ $less(sK3,0)
& distinct(tree,t2tb1(sK7))
& distinct(tree,t2tb1(sK8))
& ( sK7 = tb2t1(cons(tree,t2tb2(sK9),t2tb1(sK8))) )
& ! [X8: tree1] :
( ( ( mem(tree,t2tb2(sK12(X8)),t2tb1(sK8))
& mem(tree,t2tb2(sK11(X8)),t2tb1(sK5))
& ( node1(sK12(X8),sK11(X8)) = X8 ) )
| ~ mem(tree,t2tb2(X8),t2tb1(sK10)) )
& ( mem(tree,t2tb2(X8),t2tb1(sK10))
| ! [X11: tree1,X12: tree1] :
( ~ mem(tree,t2tb2(X12),t2tb1(sK8))
| ~ mem(tree,t2tb2(X11),t2tb1(sK5))
| ( node1(X12,X11) != X8 ) ) ) )
& distinct(tree,t2tb1(sK5))
& ! [X14: tree1] :
( ( ( mem(tree,t2tb2(sK14(X14)),t2tb1(sK5))
& ( node1(sK9,sK14(X14)) = X14 ) )
| ~ mem(tree,t2tb2(X14),t2tb1(sK13)) )
& ( mem(tree,t2tb2(X14),t2tb1(sK13))
| ! [X16: tree1] :
( ~ mem(tree,t2tb2(X16),t2tb1(sK5))
| ( node1(sK9,X16) != X14 ) ) ) )
& ~ distinct(tree,infix_plpl(tree,t2tb1(sK13),t2tb1(sK10)))
& distinct(tree,t2tb1(sK13))
& distinct(tree,t2tb1(sK10))
& all_trees1(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X5,sK8),skolemize(X6,sK9),skolemize(X7,sK10),skolemize(X9,sK11(X8)),skolemize(X10,sK12(X8)),skolemize(X13,sK13),skolemize(X15,sK14(X14))],[f147]) ).
tff(f157,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X3,X2))
| ( ~ mem(X1,X0,X2)
& ( X0 != X3 ) ) )
& ( mem(X1,X0,X2)
| ( X0 = X3 )
| ~ mem(X1,X0,cons(X1,X3,X2)) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(nnf_transformation,[],[f124]) ).
tff(f158,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X3,X2))
| ( ~ mem(X1,X0,X2)
& ( X0 != X3 ) ) )
& ( mem(X1,X0,X2)
| ( X0 = X3 )
| ~ mem(X1,X0,cons(X1,X3,X2)) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(flattening,[],[f157]) ).
tff(f159,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X2: uni,X3: uni] :
( ( ( mem(X0,X1,cons(X0,X2,X3))
| ( ~ mem(X0,X1,X3)
& ( X1 != X2 ) ) )
& ( mem(X0,X1,X3)
| ( X1 = X2 )
| ~ mem(X0,X1,cons(X0,X2,X3)) ) )
| ~ sort1(X0,X2) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(rectify,[],[f158]) ).
tff(f166,plain,
! [X0: uni,X1: uni,X2: ty] :
( distinct(X2,infix_plpl(X2,X0,X1))
| ~ distinct(X2,X0)
| ~ distinct(X2,X1)
| ? [X3: uni] :
( mem(X2,X3,X0)
& sort1(X2,X3)
& mem(X2,X3,X1) ) ),
inference(rectify,[],[f117]) ).
tff(f167,plain,
! [X0: uni,X1: uni,X2: ty] :
( distinct(X2,infix_plpl(X2,X0,X1))
| ~ distinct(X2,X0)
| ~ distinct(X2,X1)
| ( mem(X2,sK19(X0,X1,X2),X0)
& sort1(X2,sK19(X0,X1,X2))
& mem(X2,sK19(X0,X1,X2),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X3,sK19(X0,X1,X2))],[f166]) ).
tff(f173,plain,
! [X0: uni,X1: ty] :
( ( cons(X1,sK1(X0,X1),sK2(X0,X1)) = X0 )
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 )
| ( nil(X1) = X0 )
| ~ distinct(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
tff(f174,plain,
! [X0: uni,X1: ty] :
( sort1(X1,sK1(X0,X1))
| ( nil(X1) = X0 )
| ~ distinct(X1,X0)
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 ) ),
inference(cnf_transformation,[],[f134]) ).
tff(f176,plain,
! [X0: uni,X1: ty] :
( ~ mem(X1,sK1(X0,X1),sK2(X0,X1))
| ( nil(X1) = X0 )
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 )
| ~ distinct(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
tff(f189,plain,
! [X2: uni,X0: ty,X1: uni] : ( cons_proj_21(X0,cons(X0,X2,X1)) = X1 ),
inference(cnf_transformation,[],[f138]) ).
tff(f193,plain,
! [X2: uni,X0: uni,X1: ty] :
( ( cons_proj_11(X1,cons(X1,X2,X0)) = X2 )
| ~ sort1(X1,X2) ),
inference(cnf_transformation,[],[f141]) ).
tff(f194,plain,
! [X2: ty,X0: uni,X1: uni] : ( cons(X2,X0,X1) != nil(X2) ),
inference(cnf_transformation,[],[f142]) ).
tff(f200,plain,
distinct(tree,t2tb1(sK10)),
inference(cnf_transformation,[],[f148]) ).
tff(f201,plain,
distinct(tree,t2tb1(sK13)),
inference(cnf_transformation,[],[f148]) ).
tff(f202,plain,
~ distinct(tree,infix_plpl(tree,t2tb1(sK13),t2tb1(sK10))),
inference(cnf_transformation,[],[f148]) ).
tff(f204,plain,
! [X14: tree1] :
( ( node1(sK9,sK14(X14)) = X14 )
| ~ mem(tree,t2tb2(X14),t2tb1(sK13)) ),
inference(cnf_transformation,[],[f148]) ).
tff(f208,plain,
! [X8: tree1] :
( ( node1(sK12(X8),sK11(X8)) = X8 )
| ~ mem(tree,t2tb2(X8),t2tb1(sK10)) ),
inference(cnf_transformation,[],[f148]) ).
tff(f210,plain,
! [X8: tree1] :
( mem(tree,t2tb2(sK12(X8)),t2tb1(sK8))
| ~ mem(tree,t2tb2(X8),t2tb1(sK10)) ),
inference(cnf_transformation,[],[f148]) ).
tff(f211,plain,
sK7 = tb2t1(cons(tree,t2tb2(sK9),t2tb1(sK8))),
inference(cnf_transformation,[],[f148]) ).
tff(f213,plain,
distinct(tree,t2tb1(sK7)),
inference(cnf_transformation,[],[f148]) ).
tff(f229,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f71]) ).
tff(f235,plain,
! [X0: ty,X1: uni] :
( ~ mem(X0,X1,nil(X0))
| ~ sort1(X0,X1) ),
inference(cnf_transformation,[],[f159]) ).
tff(f241,plain,
! [X0: tree1] : sort1(tree,t2tb2(X0)),
inference(cnf_transformation,[],[f69]) ).
tff(f244,plain,
! [X0: tree1,X1: tree1] : ( node_proj_11(node1(X1,X0)) = X1 ),
inference(cnf_transformation,[],[f103]) ).
tff(f249,plain,
! [X2: ty,X0: uni,X1: uni] :
( distinct(X2,infix_plpl(X2,X0,X1))
| ~ distinct(X2,X0)
| mem(X2,sK19(X0,X1,X2),X1)
| ~ distinct(X2,X1) ),
inference(cnf_transformation,[],[f167]) ).
tff(f251,plain,
! [X2: ty,X0: uni,X1: uni] :
( distinct(X2,infix_plpl(X2,X0,X1))
| mem(X2,sK19(X0,X1,X2),X0)
| ~ distinct(X2,X1)
| ~ distinct(X2,X0) ),
inference(cnf_transformation,[],[f167]) ).
tff(f255,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f68]) ).
tff(f267,definition,
sF20 = t2tb1(sK7),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f268,plain,
distinct(tree,sF20),
inference(definition_folding,[],[f213,f267]) ).
tff(f269,definition,
sF21 = t2tb1(sK8),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f270,plain,
t2tb1(sK8) = sF21,
inference(reorient_equations,[],[f269]) ).
tff(f272,definition,
sF22 = t2tb2(sK9),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f273,definition,
sF23 = cons(tree,sF22,sF21),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f274,definition,
sF24 = tb2t1(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f275,plain,
sF24 = sK7,
inference(definition_folding,[],[f211,f274,f273,f270,f272]) ).
tff(f276,definition,
sF25 = t2tb1(sK10),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f277,plain,
! [X8: tree1] :
( mem(tree,t2tb2(sK12(X8)),sF21)
| ~ mem(tree,t2tb2(X8),sF25) ),
inference(definition_folding,[],[f210,f276,f270]) ).
tff(f281,plain,
! [X8: tree1] :
( ~ mem(tree,t2tb2(X8),sF25)
| ( node1(sK12(X8),sK11(X8)) = X8 ) ),
inference(definition_folding,[],[f208,f276]) ).
tff(f284,definition,
sF27 = t2tb1(sK13),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f285,plain,
t2tb1(sK13) = sF27,
inference(reorient_equations,[],[f284]) ).
tff(f287,plain,
! [X14: tree1] :
( ~ mem(tree,t2tb2(X14),sF27)
| ( node1(sK9,sK14(X14)) = X14 ) ),
inference(definition_folding,[],[f204,f285]) ).
tff(f289,definition,
sF28 = infix_plpl(tree,sF27,sF25),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f290,plain,
~ distinct(tree,sF28),
inference(definition_folding,[],[f202,f289,f276,f285]) ).
tff(f291,plain,
distinct(tree,sF27),
inference(definition_folding,[],[f201,f285]) ).
tff(f292,plain,
distinct(tree,sF25),
inference(definition_folding,[],[f200,f276]) ).
tff(f299,plain,
t2tb1(sF24) = sF20,
inference(forward_demodulation,[],[f267,f275]) ).
tff(f300,plain,
sort1(tree,sF22),
inference(constrained_superposition,[],[f241,f272]) ).
tff(f305,plain,
! [X0: uni] : sort1(tree,X0),
inference(constrained_superposition,[],[f241,f229]) ).
tff(f308,plain,
! [X0: uni] :
( ~ mem(tree,X0,sF25)
| ( tb2t2(X0) = node1(sK12(tb2t2(X0)),sK11(tb2t2(X0))) ) ),
inference(constrained_superposition,[],[f281,f229]) ).
tff(f309,plain,
! [X0: uni] :
( ~ mem(tree,X0,sF27)
| ( tb2t2(X0) = node1(sK9,sK14(tb2t2(X0))) ) ),
inference(constrained_superposition,[],[f287,f229]) ).
tff(f337,plain,
t2tb1(sF24) = sF23,
inference(constrained_superposition,[],[f255,f274]) ).
tff(f342,plain,
sF20 = sF23,
inference(forward_demodulation,[],[f337,f299]) ).
tff(f415,plain,
sF20 = cons(tree,sF22,sF21),
inference(forward_demodulation,[],[f273,f342]) ).
tff(f467,plain,
nil(tree) != sF20,
inference(constrained_superposition,[],[f194,f415]) ).
tff(f516,plain,
cons_proj_21(tree,sF20) = sF21,
inference(constrained_superposition,[],[f189,f415]) ).
tff(f609,plain,
( ~ sort1(tree,sF22)
| ( sF22 = cons_proj_11(tree,sF20) ) ),
inference(constrained_superposition,[],[f193,f415]) ).
tff(f611,plain,
sF22 = cons_proj_11(tree,sF20),
inference(forward_subsumption_resolution,[],[f609,f300]) ).
tff(f1095,plain,
( distinct(tree,sF28)
| ~ distinct(tree,sF25)
| ~ distinct(tree,sF27)
| mem(tree,sK19(sF27,sF25,tree),sF25) ),
inference(constrained_superposition,[],[f249,f289]) ).
tff(f1101,plain,
( ~ distinct(tree,sF27)
| mem(tree,sK19(sF27,sF25,tree),sF25)
| ~ distinct(tree,sF25) ),
inference(forward_subsumption_resolution,[],[f1095,f290]) ).
tff(f1102,plain,
( ~ distinct(tree,sF25)
| mem(tree,sK19(sF27,sF25,tree),sF25) ),
inference(forward_subsumption_resolution,[],[f1101,f291]) ).
tff(f1103,plain,
mem(tree,sK19(sF27,sF25,tree),sF25),
inference(forward_subsumption_resolution,[],[f1102,f292]) ).
tff(f1105,plain,
node1(sK12(tb2t2(sK19(sF27,sF25,tree))),sK11(tb2t2(sK19(sF27,sF25,tree)))) = tb2t2(sK19(sF27,sF25,tree)),
inference(resolution,[],[f1103,f308]) ).
tff(f1279,plain,
( ~ distinct(tree,sF27)
| distinct(tree,sF28)
| ~ distinct(tree,sF25)
| mem(tree,sK19(sF27,sF25,tree),sF27) ),
inference(constrained_superposition,[],[f251,f289]) ).
tff(f1285,plain,
( distinct(tree,sF28)
| ~ distinct(tree,sF25)
| mem(tree,sK19(sF27,sF25,tree),sF27) ),
inference(forward_subsumption_resolution,[],[f1279,f291]) ).
tff(f1286,plain,
( ~ distinct(tree,sF25)
| mem(tree,sK19(sF27,sF25,tree),sF27) ),
inference(forward_subsumption_resolution,[],[f1285,f290]) ).
tff(f1287,plain,
mem(tree,sK19(sF27,sF25,tree),sF27),
inference(forward_subsumption_resolution,[],[f1286,f292]) ).
tff(f1288,plain,
node1(sK9,sK14(tb2t2(sK19(sF27,sF25,tree)))) = tb2t2(sK19(sF27,sF25,tree)),
inference(resolution,[],[f1287,f309]) ).
tff(f1498,plain,
! [X0: uni,X1: ty] :
( ( sK2(X0,X1) = cons_proj_21(X1,X0) )
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 )
| ( nil(X1) = X0 )
| ~ distinct(X1,X0) ),
inference(constrained_superposition,[],[f189,f173]) ).
tff(f1500,plain,
! [X0: uni,X1: ty] :
( ( sK1(X0,X1) = cons_proj_11(X1,X0) )
| ~ sort1(X1,sK1(X0,X1))
| ( nil(X1) = X0 )
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 )
| ~ distinct(X1,X0) ),
inference(constrained_superposition,[],[f193,f173]) ).
tff(f1509,plain,
! [X0: uni,X1: ty] :
( ( sK1(X0,X1) = cons_proj_11(X1,X0) )
| ~ distinct(X1,X0)
| ( cons(X1,sK0(X0,X1),nil(X1)) = X0 )
| ( nil(X1) = X0 ) ),
inference(forward_subsumption_resolution,[],[f1500,f174]) ).
tff(f2809,plain,
( ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ( sK2(sF20,tree) = sF21 )
| ( nil(tree) = sF20 )
| ~ distinct(tree,sF20) ),
inference(constrained_superposition,[],[f1498,f516]) ).
tff(f2825,plain,
( ~ distinct(tree,sF20)
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ( sK2(sF20,tree) = sF21 ) ),
inference(forward_subsumption_resolution,[],[f2809,f467]) ).
tff(f2831,plain,
( ( sK2(sF20,tree) = sF21 )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(forward_subsumption_resolution,[],[f2825,f268]) ).
tff(f2856,plain,
( ( nil(tree) = sF20 )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ( sF22 = sK1(sF20,tree) )
| ~ distinct(tree,sF20) ),
inference(constrained_superposition,[],[f1509,f611]) ).
tff(f2875,plain,
( ( sF22 = sK1(sF20,tree) )
| ~ distinct(tree,sF20)
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(forward_subsumption_resolution,[],[f2856,f467]) ).
tff(f2881,plain,
( ( sF22 = sK1(sF20,tree) )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(forward_subsumption_resolution,[],[f2875,f268]) ).
tff(f3347,plain,
sK9 = node_proj_11(tb2t2(sK19(sF27,sF25,tree))),
inference(constrained_superposition,[],[f244,f1288]) ).
tff(f3377,plain,
( ~ mem(tree,sK1(sF20,tree),sF21)
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ~ distinct(tree,sF20)
| ( nil(tree) = sF20 )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(constrained_superposition,[],[f176,f2831]) ).
tff(f3385,plain,
( ~ distinct(tree,sF20)
| ( nil(tree) = sF20 )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ~ mem(tree,sK1(sF20,tree),sF21) ),
inference(duplicate_literal_removal,[],[f3377]) ).
tff(f3389,plain,
( ( nil(tree) = sF20 )
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ~ mem(tree,sK1(sF20,tree),sF21) ),
inference(forward_subsumption_resolution,[],[f3385,f268]) ).
tff(f3392,plain,
( ~ mem(tree,sK1(sF20,tree),sF21)
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(forward_subsumption_resolution,[],[f3389,f467]) ).
tff(f3712,plain,
node_proj_11(tb2t2(sK19(sF27,sF25,tree))) = sK12(tb2t2(sK19(sF27,sF25,tree))),
inference(constrained_superposition,[],[f244,f1105]) ).
tff(f3715,plain,
sK9 = sK12(tb2t2(sK19(sF27,sF25,tree))),
inference(forward_demodulation,[],[f3712,f3347]) ).
tff(f3723,plain,
( ~ mem(tree,t2tb2(tb2t2(sK19(sF27,sF25,tree))),sF25)
| mem(tree,t2tb2(sK9),sF21) ),
inference(constrained_superposition,[],[f277,f3715]) ).
tff(f3724,plain,
( ~ mem(tree,sK19(sF27,sF25,tree),sF25)
| mem(tree,t2tb2(sK9),sF21) ),
inference(forward_demodulation,[],[f3723,f229]) ).
tff(f3725,plain,
mem(tree,t2tb2(sK9),sF21),
inference(forward_subsumption_resolution,[],[f3724,f1103]) ).
tff(f3726,plain,
mem(tree,sF22,sF21),
inference(forward_demodulation,[],[f3725,f272]) ).
tff(f13327,plain,
( ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ~ mem(tree,sF22,sF21)
| ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 ) ),
inference(constrained_superposition,[],[f3392,f2881]) ).
tff(f13328,plain,
( ( cons(tree,sK0(sF20,tree),nil(tree)) = sF20 )
| ~ mem(tree,sF22,sF21) ),
inference(duplicate_literal_removal,[],[f13327]) ).
tff(f13329,plain,
cons(tree,sK0(sF20,tree),nil(tree)) = sF20,
inference(forward_subsumption_resolution,[],[f13328,f3726]) ).
tff(f13598,plain,
nil(tree) = cons_proj_21(tree,sF20),
inference(constrained_superposition,[],[f189,f13329]) ).
tff(f13633,plain,
nil(tree) = sF21,
inference(forward_demodulation,[],[f13598,f516]) ).
tff(f13673,plain,
! [X0: uni] :
( ~ mem(tree,X0,sF21)
| ~ sort1(tree,X0) ),
inference(constrained_superposition,[],[f235,f13633]) ).
tff(f13680,plain,
! [X0: uni] : ~ mem(tree,X0,sF21),
inference(forward_subsumption_resolution,[],[f13673,f305]) ).
tff(f13688,plain,
$false,
inference(resolution,[],[f13680,f3726]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW603_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n005.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 14:21:01 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/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.59/1.25 % (813730)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.59/1.25 % (813736)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1028582880:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.59/1.25 % (813735)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1128195555:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.59/1.25 % (813738)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3197710536:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.59/1.25 % (813737)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3497694146:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.59/1.25 % (813739)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3938063490:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.59/1.25 % (813739)Instruction limit reached!
% 3.59/1.25 % (813739)------------------------------
% 3.59/1.25 % (813739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813739)CaDiCaL version: 2.1.3
% 3.59/1.25 % (813739)Termination reason: Instruction limit
% 3.59/1.25 % (813739)Termination phase: Function definition elimination
% 3.59/1.25 % (813739)Time elapsed: 0.003 s
% 3.59/1.25 % (813739)Peak memory usage: 86 MB
% 3.59/1.25 % (813739)Instructions burned: 5 (million)
% 3.59/1.25 % (813738)Instruction limit reached!
% 3.59/1.25 % (813738)------------------------------
% 3.59/1.25 % (813738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813738)CaDiCaL version: 2.1.3
% 3.59/1.25 % (813738)Termination reason: Instruction limit
% 3.59/1.25 % (813738)Termination phase: Saturation
% 3.59/1.25 % (813738)Time elapsed: 0.005 s
% 3.59/1.25 % (813738)Peak memory usage: 88 MB
% 3.59/1.25 % (813738)Instructions burned: 8 (million)
% 3.59/1.25 % (813740)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3594091681:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.59/1.25 % (813741)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2712060185:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.59/1.25 % (813735)Instruction limit reached!
% 3.59/1.25 % (813735)------------------------------
% 3.59/1.25 % (813735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813735)CaDiCaL version: 2.1.3
% 3.59/1.25 % (813735)Termination reason: Instruction limit
% 3.59/1.25 % (813735)Termination phase: Saturation
% 3.59/1.25 % (813735)Time elapsed: 0.030 s
% 3.59/1.25 % (813735)Peak memory usage: 114 MB
% 3.59/1.25 % (813735)Instructions burned: 12 (million)
% 3.59/1.25 % (813741)Instruction limit reached!
% 3.59/1.25 % (813741)------------------------------
% 3.59/1.25 % (813741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813741)CaDiCaL version: 2.1.3
% 3.59/1.25 % (813741)Termination reason: Instruction limit
% 3.59/1.25 % (813741)Termination phase: Saturation
% 3.59/1.25 % (813741)Time elapsed: 0.044 s
% 3.59/1.25 % (813741)Peak memory usage: 116 MB
% 3.59/1.25 % (813741)Instructions burned: 33 (million)
% 3.59/1.25 % (813740)Instruction limit reached!
% 3.59/1.25 % (813740)------------------------------
% 3.59/1.25 % (813740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813740)CaDiCaL version: 2.1.3
% 3.59/1.25 % (813740)Termination reason: Instruction limit
% 3.59/1.25 % (813740)Termination phase: Saturation
% 3.59/1.25 % (813740)Time elapsed: 0.055 s
% 3.59/1.25 % (813740)Peak memory usage: 115 MB
% 3.59/1.25 % (813740)Instructions burned: 47 (million)
% 3.59/1.25 % (813736)Instruction limit reached!
% 3.59/1.25 % (813736)------------------------------
% 3.59/1.25 % (813736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.25 % (813736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.25 % (813736)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813736)Termination reason: Instruction limit
% 4.94/1.40 % (813736)Termination phase: Saturation
% 4.94/1.40 % (813736)Time elapsed: 0.122 s
% 4.94/1.40 % (813736)Peak memory usage: 117 MB
% 4.94/1.40 % (813736)Instructions burned: 308 (million)
% 4.94/1.40 % (813749)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3803725703:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.94/1.40 % (813750)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=3137705245:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.94/1.40 % (813749)Instruction limit reached!
% 4.94/1.40 % (813749)------------------------------
% 4.94/1.40 % (813749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.40 % (813749)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813749)Termination reason: Instruction limit
% 4.94/1.40 % (813749)Termination phase: Saturation
% 4.94/1.40 % (813749)Time elapsed: 0.010 s
% 4.94/1.40 % (813749)Peak memory usage: 88 MB
% 4.94/1.40 % (813749)Instructions burned: 14 (million)
% 4.94/1.40 % (813737)Instruction limit reached!
% 4.94/1.40 % (813737)------------------------------
% 4.94/1.40 % (813737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.40 % (813737)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813737)Termination reason: Instruction limit
% 4.94/1.40 % (813737)Termination phase: Saturation
% 4.94/1.40 % (813737)Time elapsed: 0.180 s
% 4.94/1.40 % (813737)Peak memory usage: 119 MB
% 4.94/1.40 % (813737)Instructions burned: 201 (million)
% 4.94/1.40 % (813750)Instruction limit reached!
% 4.94/1.40 % (813750)------------------------------
% 4.94/1.40 % (813750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.40 % (813750)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813751)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3886976439:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.94/1.40 % (813750)Termination reason: Instruction limit
% 4.94/1.40 % (813750)Termination phase: Saturation
% 4.94/1.40 % (813750)Time elapsed: 0.025 s
% 4.94/1.40 % (813750)Peak memory usage: 88 MB
% 4.94/1.40 % (813750)Instructions burned: 31 (million)
% 4.94/1.40 % (813754)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1957405145:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.94/1.40 % (813752)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4273395386:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.94/1.40 % (813751)Instruction limit reached!
% 4.94/1.40 % (813751)------------------------------
% 4.94/1.40 % (813751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.40 % (813751)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813751)Termination reason: Instruction limit
% 4.94/1.40 % (813751)Termination phase: Saturation
% 4.94/1.40 % (813751)Time elapsed: 0.011 s
% 4.94/1.40 % (813751)Peak memory usage: 89 MB
% 4.94/1.40 % (813751)Instructions burned: 17 (million)
% 4.94/1.40 % (813753)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=1262392388:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.94/1.40 % (813752)Instruction limit reached!
% 4.94/1.40 % (813752)------------------------------
% 4.94/1.40 % (813752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.94/1.40 % (813752)CaDiCaL version: 2.1.3
% 4.94/1.40 % (813752)Termination reason: Instruction limit
% 4.94/1.40 % (813752)Termination phase: Saturation
% 4.94/1.40 % (813752)Time elapsed: 0.018 s
% 4.94/1.40 % (813752)Peak memory usage: 89 MB
% 4.94/1.40 % (813752)Instructions burned: 24 (million)
% 4.94/1.40 % (813754)Instruction limit reached!
% 4.94/1.40 % (813754)------------------------------
% 4.94/1.40 % (813754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.94/1.40 % (813754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813754)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813754)Termination reason: Instruction limit
% 5.74/1.57 % (813754)Termination phase: Saturation
% 5.74/1.57 % (813754)Time elapsed: 0.027 s
% 5.74/1.57 % (813754)Peak memory usage: 89 MB
% 5.74/1.57 % (813754)Instructions burned: 87 (million)
% 5.74/1.57 % (813753)Instruction limit reached!
% 5.74/1.57 % (813753)------------------------------
% 5.74/1.57 % (813753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.74/1.57 % (813753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813753)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813753)Termination reason: Instruction limit
% 5.74/1.57 % (813753)Termination phase: Saturation
% 5.74/1.57 % (813753)Time elapsed: 0.020 s
% 5.74/1.57 % (813753)Peak memory usage: 90 MB
% 5.74/1.57 % (813753)Instructions burned: 28 (million)
% 5.74/1.57 % (813757)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3991260031:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.74/1.57 % (813757)Instruction limit reached!
% 5.74/1.57 % (813757)------------------------------
% 5.74/1.57 % (813757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.74/1.57 % (813757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813757)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813757)Termination reason: Instruction limit
% 5.74/1.57 % (813757)Termination phase: Naming
% 5.74/1.57 % (813757)Time elapsed: 0.002 s
% 5.74/1.57 % (813757)Peak memory usage: 86 MB
% 5.74/1.57 % (813757)Instructions burned: 2 (million)
% 5.74/1.57 % (813766)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=3579716375:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.74/1.57 % (813759)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3937416836:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.74/1.57 % (813760)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3505466157:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.74/1.57 % (813763)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1097187511:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.74/1.57 % (813766)Instruction limit reached!
% 5.74/1.57 % (813766)------------------------------
% 5.74/1.57 % (813766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.74/1.57 % (813766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813766)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813766)Termination reason: Instruction limit
% 5.74/1.57 % (813766)Termination phase: Saturation
% 5.74/1.57 % (813766)Time elapsed: 0.003 s
% 5.74/1.57 % (813766)Peak memory usage: 88 MB
% 5.74/1.57 % (813766)Instructions burned: 9 (million)
% 5.74/1.57 % (813760)Instruction limit reached!
% 5.74/1.57 % (813760)------------------------------
% 5.74/1.57 % (813760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.74/1.57 % (813760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813760)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813760)Termination reason: Instruction limit
% 5.74/1.57 % (813760)Termination phase: Property scanning
% 5.74/1.57 % (813760)Time elapsed: 0.003 s
% 5.74/1.57 % (813760)Peak memory usage: 86 MB
% 5.74/1.57 % (813760)Instructions burned: 5 (million)
% 5.74/1.57 % (813765)lrs+10_1_thi=all:si=on:fd=off:random_seed=2028860748:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.74/1.57 % (813767)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2402625674:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.74/1.57 % (813767)Instruction limit reached!
% 5.74/1.57 % (813767)------------------------------
% 5.74/1.57 % (813767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.74/1.57 % (813767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.57 % (813767)CaDiCaL version: 2.1.3
% 5.74/1.57 % (813767)Termination reason: Instruction limit
% 5.74/1.57 % (813767)Termination phase: Preprocessing 3
% 5.74/1.57 % (813767)Time elapsed: 0.002 s
% 5.74/1.57 % (813767)Peak memory usage: 86 MB
% 5.74/1.57 % (813767)Instructions burned: 2 (million)
% 5.74/1.57 % (813763)Instruction limit reached!
% 6.95/1.79 % (813763)------------------------------
% 6.95/1.79 % (813763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.79 % (813763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.79 % (813763)CaDiCaL version: 2.1.3
% 6.95/1.79 % (813763)Termination reason: Instruction limit
% 6.95/1.79 % (813763)Termination phase: Saturation
% 6.95/1.79 % (813763)Time elapsed: 0.087 s
% 6.95/1.79 % (813763)Peak memory usage: 133 MB
% 6.95/1.79 % (813763)Instructions burned: 67 (million)
% 6.95/1.79 % (813765)Instruction limit reached!
% 6.95/1.79 % (813765)------------------------------
% 6.95/1.79 % (813765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.79 % (813765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.79 % (813765)CaDiCaL version: 2.1.3
% 6.95/1.79 % (813765)Termination reason: Instruction limit
% 6.95/1.79 % (813765)Termination phase: Saturation
% 6.95/1.79 % (813765)Time elapsed: 0.063 s
% 6.95/1.79 % (813765)Peak memory usage: 117 MB
% 6.95/1.79 % (813765)Instructions burned: 53 (million)
% 6.95/1.79 % (813774)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3090195771:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 6.95/1.80 % (813769)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3592446430:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.95/1.80 % (813769)Instruction limit reached!
% 6.95/1.80 % (813769)------------------------------
% 6.95/1.80 % (813769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.80 % (813769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.80 % (813769)CaDiCaL version: 2.1.3
% 6.95/1.80 % (813769)Termination reason: Instruction limit
% 6.95/1.80 % (813769)Termination phase: Preprocessing 3
% 6.95/1.80 % (813769)Time elapsed: 0.002 s
% 6.95/1.80 % (813769)Peak memory usage: 86 MB
% 6.95/1.80 % (813769)Instructions burned: 2 (million)
% 6.95/1.80 % (813759)Instruction limit reached!
% 6.95/1.80 % (813759)------------------------------
% 6.95/1.80 % (813759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.80 % (813759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.80 % (813759)CaDiCaL version: 2.1.3
% 6.95/1.80 % (813759)Termination reason: Instruction limit
% 6.95/1.80 % (813759)Termination phase: Saturation
% 6.95/1.80 % (813759)Time elapsed: 0.132 s
% 6.95/1.80 % (813759)Peak memory usage: 91 MB
% 6.95/1.80 % (813759)Instructions burned: 181 (million)
% 6.95/1.80 % (813775)dis+10_1_si=on:random_seed=2882196836:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.95/1.80 % (813775)Instruction limit reached!
% 6.95/1.80 % (813775)------------------------------
% 6.95/1.80 % (813775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.80 % (813775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.80 % (813775)CaDiCaL version: 2.1.3
% 6.95/1.80 % (813775)Termination reason: Instruction limit
% 6.95/1.80 % (813775)Termination phase: Saturation
% 6.95/1.80 % (813775)Time elapsed: 0.007 s
% 6.95/1.80 % (813775)Peak memory usage: 88 MB
% 6.95/1.80 % (813775)Instructions burned: 11 (million)
% 6.95/1.80 % (813774)Instruction limit reached!
% 6.95/1.80 % (813774)------------------------------
% 6.95/1.80 % (813774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.95/1.80 % (813774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.95/1.80 % (813774)CaDiCaL version: 2.1.3
% 6.95/1.80 % (813774)Termination reason: Instruction limit
% 6.95/1.80 % (813774)Termination phase: Saturation
% 6.95/1.80 % (813774)Time elapsed: 0.062 s
% 6.95/1.80 % (813774)Peak memory usage: 118 MB
% 6.95/1.80 % (813774)Instructions burned: 129 (million)
% 6.95/1.80 % (813778)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3314136889:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.95/1.80 % (813779)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1604960807: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.95/1.80 % (813780)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=460284505:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 6.95/1.80 % (813778)Instruction limit reached!
% 6.95/1.80 % (813778)------------------------------
% 10.04/2.06 % (813778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813778)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813778)Termination reason: Instruction limit
% 10.04/2.06 % (813778)Termination phase: Saturation
% 10.04/2.06 % (813778)Time elapsed: 0.017 s
% 10.04/2.06 % (813778)Peak memory usage: 89 MB
% 10.04/2.06 % (813778)Instructions burned: 27 (million)
% 10.04/2.06 % (813780)Instruction limit reached!
% 10.04/2.06 % (813780)------------------------------
% 10.04/2.06 % (813780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813780)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813780)Termination reason: Instruction limit
% 10.04/2.06 % (813780)Termination phase: Preprocessing 3
% 10.04/2.06 % (813780)Time elapsed: 0.002 s
% 10.04/2.06 % (813780)Peak memory usage: 86 MB
% 10.04/2.06 % (813780)Instructions burned: 3 (million)
% 10.04/2.06 % (813779)Instruction limit reached!
% 10.04/2.06 % (813779)------------------------------
% 10.04/2.06 % (813779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813779)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813779)Termination reason: Instruction limit
% 10.04/2.06 % (813779)Termination phase: Saturation
% 10.04/2.06 % (813779)Time elapsed: 0.027 s
% 10.04/2.06 % (813779)Peak memory usage: 89 MB
% 10.04/2.06 % (813779)Instructions burned: 35 (million)
% 10.04/2.06 % (813783)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=207948503:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.04/2.06 % (813784)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3271930994:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.04/2.06 % (813783)Instruction limit reached!
% 10.04/2.06 % (813783)------------------------------
% 10.04/2.06 % (813783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813783)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813783)Termination reason: Instruction limit
% 10.04/2.06 % (813783)Termination phase: Saturation
% 10.04/2.06 % (813783)Time elapsed: 0.006 s
% 10.04/2.06 % (813783)Peak memory usage: 88 MB
% 10.04/2.06 % (813783)Instructions burned: 9 (million)
% 10.04/2.06 % (813786)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3613274277:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.04/2.06 % (813787)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3964552503:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 10.04/2.06 % (813786)Instruction limit reached!
% 10.04/2.06 % (813786)------------------------------
% 10.04/2.06 % (813786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813786)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813786)Termination reason: Instruction limit
% 10.04/2.06 % (813786)Termination phase: Saturation
% 10.04/2.06 % (813786)Time elapsed: 0.030 s
% 10.04/2.06 % (813786)Peak memory usage: 113 MB
% 10.04/2.06 % (813786)Instructions burned: 14 (million)
% 10.04/2.06 % (813787)Instruction limit reached!
% 10.04/2.06 % (813787)------------------------------
% 10.04/2.06 % (813787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.04/2.06 % (813787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.04/2.06 % (813787)CaDiCaL version: 2.1.3
% 10.04/2.06 % (813787)Termination reason: Instruction limit
% 10.04/2.06 % (813787)Termination phase: Saturation
% 10.04/2.06 % (813787)Time elapsed: 0.087 s
% 10.04/2.06 % (813787)Peak memory usage: 117 MB
% 10.04/2.06 % (813787)Instructions burned: 230 (million)
% 10.04/2.06 % (813791)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1837263195:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.04/2.06 % (813792)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1825701783:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.04/2.06 % (813791)Instruction limit reached!
% 10.04/2.06 % (813791)------------------------------
% 11.46/2.30 % (813791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.30 % (813791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.30 % (813791)CaDiCaL version: 2.1.3
% 11.46/2.30 % (813791)Termination reason: Instruction limit
% 11.46/2.30 % (813791)Termination phase: Saturation
% 11.46/2.30 % (813791)Time elapsed: 0.008 s
% 11.46/2.30 % (813791)Peak memory usage: 88 MB
% 11.46/2.30 % (813791)Instructions burned: 11 (million)
% 11.46/2.30 % (813794)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=72939680:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 11.46/2.30 % (813796)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=3734189426:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 11.46/2.30 % (813794)Instruction limit reached!
% 11.46/2.30 % (813794)------------------------------
% 11.46/2.30 % (813794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.31 % (813794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.31 % (813794)CaDiCaL version: 2.1.3
% 11.46/2.31 % (813794)Termination reason: Instruction limit
% 11.46/2.31 % (813794)Termination phase: Saturation
% 11.46/2.31 % (813794)Time elapsed: 0.059 s
% 11.46/2.31 % (813794)Peak memory usage: 90 MB
% 11.46/2.31 % (813794)Instructions burned: 75 (million)
% 11.46/2.31 % (813799)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1186654767:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 11.46/2.31 % (813784)Instruction limit reached!
% 11.46/2.31 % (813784)------------------------------
% 11.46/2.31 % (813784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.31 % (813784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.31 % (813784)CaDiCaL version: 2.1.3
% 11.46/2.31 % (813784)Termination reason: Instruction limit
% 11.46/2.31 % (813784)Termination phase: Saturation
% 11.46/2.31 % (813784)Time elapsed: 0.209 s
% 11.46/2.31 % (813784)Peak memory usage: 92 MB
% 11.46/2.31 % (813784)Instructions burned: 370 (million)
% 11.46/2.31 % (813792)Instruction limit reached!
% 11.46/2.31 % (813792)------------------------------
% 11.46/2.31 % (813792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.31 % (813792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.31 % (813792)CaDiCaL version: 2.1.3
% 11.46/2.31 % (813792)Termination reason: Instruction limit
% 11.46/2.31 % (813792)Termination phase: Saturation
% 11.46/2.31 % (813792)Time elapsed: 0.094 s
% 11.46/2.31 % (813792)Peak memory usage: 133 MB
% 11.46/2.31 % (813792)Instructions burned: 72 (million)
% 11.46/2.31 % (813800)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2116684942:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 11.46/2.31 % (813803)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=444946364:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 11.46/2.31 % (813800)Instruction limit reached!
% 11.46/2.31 % (813800)------------------------------
% 11.46/2.31 % (813800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.31 % (813800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.31 % (813800)CaDiCaL version: 2.1.3
% 11.46/2.31 % (813800)Termination reason: Instruction limit
% 11.46/2.31 % (813800)Termination phase: Saturation
% 11.46/2.31 % (813800)Time elapsed: 0.074 s
% 11.46/2.31 % (813800)Peak memory usage: 134 MB
% 11.46/2.31 % (813800)Instructions burned: 131 (million)
% 11.46/2.31 % (813799)Instruction limit reached!
% 11.46/2.31 % (813799)------------------------------
% 11.46/2.31 % (813799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.31 % (813799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.31 % (813799)CaDiCaL version: 2.1.3
% 11.46/2.31 % (813799)Termination reason: Instruction limit
% 11.46/2.31 % (813799)Termination phase: Saturation
% 11.46/2.31 % (813799)Time elapsed: 0.110 s
% 11.46/2.31 % (813799)Peak memory usage: 117 MB
% 11.46/2.31 % (813799)Instructions burned: 131 (million)
% 11.46/2.31 % (813807)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3434839754:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 12.79/2.60 % (813808)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2790467558:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 12.79/2.60 % (813796)Instruction limit reached!
% 12.79/2.60 % (813796)------------------------------
% 12.79/2.60 % (813796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813796)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813796)Termination reason: Instruction limit
% 12.79/2.60 % (813796)Termination phase: Saturation
% 12.79/2.60 % (813796)Time elapsed: 0.213 s
% 12.79/2.60 % (813796)Peak memory usage: 91 MB
% 12.79/2.60 % (813796)Instructions burned: 294 (million)
% 12.79/2.60 % (813803)Instruction limit reached!
% 12.79/2.60 % (813803)------------------------------
% 12.79/2.60 % (813803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813803)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813803)Termination reason: Instruction limit
% 12.79/2.60 % (813803)Termination phase: Saturation
% 12.79/2.60 % (813803)Time elapsed: 0.070 s
% 12.79/2.60 % (813803)Peak memory usage: 133 MB
% 12.79/2.60 % (813803)Instructions burned: 41 (million)
% 12.79/2.60 % (813809)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3496492560:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.79/2.60 % (813812)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=2855189418:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 12.79/2.60 % (813813)dis+10_1_si=on:random_seed=2350827558:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 12.79/2.60 % (813809)Instruction limit reached!
% 12.79/2.60 % (813809)------------------------------
% 12.79/2.60 % (813809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813809)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813809)Termination reason: Instruction limit
% 12.79/2.60 % (813809)Termination phase: Saturation
% 12.79/2.60 % (813809)Time elapsed: 0.107 s
% 12.79/2.60 % (813809)Peak memory usage: 117 MB
% 12.79/2.60 % (813809)Instructions burned: 132 (million)
% 12.79/2.60 % (813816)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3940433098:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.79/2.60 % (813817)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3104309360:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 12.79/2.60 % (813807)Instruction limit reached!
% 12.79/2.60 % (813807)------------------------------
% 12.79/2.60 % (813807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813807)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813807)Termination reason: Instruction limit
% 12.79/2.60 % (813807)Termination phase: Saturation
% 12.79/2.60 % (813807)Time elapsed: 0.177 s
% 12.79/2.60 % (813807)Peak memory usage: 93 MB
% 12.79/2.60 % (813807)Instructions burned: 308 (million)
% 12.79/2.60 % (813812)Instruction limit reached!
% 12.79/2.60 % (813812)------------------------------
% 12.79/2.60 % (813812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813812)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813812)Termination reason: Instruction limit
% 12.79/2.60 % (813812)Termination phase: Saturation
% 12.79/2.60 % (813812)Time elapsed: 0.099 s
% 12.79/2.60 % (813812)Peak memory usage: 117 MB
% 12.79/2.60 % (813812)Instructions burned: 260 (million)
% 12.79/2.60 % (813817)Instruction limit reached!
% 12.79/2.60 % (813817)------------------------------
% 12.79/2.60 % (813817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.79/2.60 % (813817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.79/2.60 % (813817)CaDiCaL version: 2.1.3
% 12.79/2.60 % (813817)Termination reason: Instruction limit
% 12.79/2.60 % (813817)Termination phase: Saturation
% 12.79/2.60 % (813817)Time elapsed: 0.098 s
% 12.79/2.60 % (813817)Peak memory usage: 91 MB
% 14.60/2.92 % (813817)Instructions burned: 142 (million)
% 14.60/2.92 % (813821)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3637526998:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 14.60/2.92 % (813825)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=2947088105:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.60/2.92 % (813824)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=509302723:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 14.60/2.92 % (813821)Instruction limit reached!
% 14.60/2.92 % (813821)------------------------------
% 14.60/2.92 % (813821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813821)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813821)Termination reason: Instruction limit
% 14.60/2.92 % (813821)Termination phase: Saturation
% 14.60/2.92 % (813821)Time elapsed: 0.064 s
% 14.60/2.92 % (813821)Peak memory usage: 116 MB
% 14.60/2.92 % (813821)Instructions burned: 65 (million)
% 14.60/2.92 % (813825)Instruction limit reached!
% 14.60/2.92 % (813825)------------------------------
% 14.60/2.92 % (813825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813825)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813825)Termination reason: Instruction limit
% 14.60/2.92 % (813825)Termination phase: Saturation
% 14.60/2.92 % (813825)Time elapsed: 0.060 s
% 14.60/2.92 % (813825)Peak memory usage: 117 MB
% 14.60/2.92 % (813825)Instructions burned: 129 (million)
% 14.60/2.92 % (813824)Instruction limit reached!
% 14.60/2.92 % (813824)------------------------------
% 14.60/2.92 % (813824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813824)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813824)Termination reason: Instruction limit
% 14.60/2.92 % (813824)Termination phase: Saturation
% 14.60/2.92 % (813824)Time elapsed: 0.083 s
% 14.60/2.92 % (813824)Peak memory usage: 90 MB
% 14.60/2.92 % (813824)Instructions burned: 121 (million)
% 14.60/2.92 % (813808)Instruction limit reached!
% 14.60/2.92 % (813808)------------------------------
% 14.60/2.92 % (813808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813808)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813808)Termination reason: Instruction limit
% 14.60/2.92 % (813808)Termination phase: Saturation
% 14.60/2.92 % (813808)Time elapsed: 0.400 s
% 14.60/2.92 % (813808)Peak memory usage: 139 MB
% 14.60/2.92 % (813808)Instructions burned: 599 (million)
% 14.60/2.92 % (813826)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=3914327604:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 14.60/2.92 % (813816)Instruction limit reached!
% 14.60/2.92 % (813816)------------------------------
% 14.60/2.92 % (813816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813816)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813816)Termination reason: Instruction limit
% 14.60/2.92 % (813816)Termination phase: Saturation
% 14.60/2.92 % (813816)Time elapsed: 0.264 s
% 14.60/2.92 % (813816)Peak memory usage: 95 MB
% 14.60/2.92 % (813816)Instructions burned: 384 (million)
% 14.60/2.92 % (813826)Instruction limit reached!
% 14.60/2.92 % (813826)------------------------------
% 14.60/2.92 % (813826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.92 % (813826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.92 % (813826)CaDiCaL version: 2.1.3
% 14.60/2.92 % (813826)Termination reason: Instruction limit
% 14.60/2.92 % (813826)Termination phase: Saturation
% 14.60/2.92 % (813826)Time elapsed: 0.052 s
% 14.60/2.92 % (813826)Peak memory usage: 116 MB
% 14.60/2.92 % (813826)Instructions burned: 39 (million)
% 14.60/2.92 % (813831)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2767602375:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 14.60/2.92 % (813830)dis+1010_1_to=kbo:si=on:random_seed=3984265584:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 18.16/3.29 % (813832)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3662093831:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 18.16/3.29 % (813835)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=939504155:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi)
% 18.16/3.29 % (813833)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2370077211:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 18.16/3.29 % (813831)Instruction limit reached!
% 18.16/3.29 % (813831)------------------------------
% 18.16/3.29 % (813831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813831)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813831)Termination reason: Instruction limit
% 18.16/3.29 % (813831)Termination phase: Saturation
% 18.16/3.29 % (813831)Time elapsed: 0.113 s
% 18.16/3.29 % (813831)Peak memory usage: 118 MB
% 18.16/3.29 % (813831)Instructions burned: 329 (million)
% 18.16/3.29 % (813837)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2564304331:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 18.16/3.29 % (813830)Instruction limit reached!
% 18.16/3.29 % (813830)------------------------------
% 18.16/3.29 % (813830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813830)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813830)Termination reason: Instruction limit
% 18.16/3.29 % (813830)Termination phase: Saturation
% 18.16/3.29 % (813830)Time elapsed: 0.129 s
% 18.16/3.29 % (813830)Peak memory usage: 91 MB
% 18.16/3.29 % (813830)Instructions burned: 175 (million)
% 18.16/3.29 % (813813)Instruction limit reached!
% 18.16/3.29 % (813813)------------------------------
% 18.16/3.29 % (813813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813813)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813813)Termination reason: Instruction limit
% 18.16/3.29 % (813813)Termination phase: Saturation
% 18.16/3.29 % (813813)Time elapsed: 0.566 s
% 18.16/3.29 % (813813)Peak memory usage: 93 MB
% 18.16/3.29 % (813813)Instructions burned: 1001 (million)
% 18.16/3.29 % (813842)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=863376892:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 18.16/3.29 % (813833)Instruction limit reached!
% 18.16/3.29 % (813833)------------------------------
% 18.16/3.29 % (813833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813833)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813833)Termination reason: Instruction limit
% 18.16/3.29 % (813833)Termination phase: Saturation
% 18.16/3.29 % (813833)Time elapsed: 0.155 s
% 18.16/3.29 % (813833)Peak memory usage: 134 MB
% 18.16/3.29 % (813833)Instructions burned: 216 (million)
% 18.16/3.29 % (813837)Instruction limit reached!
% 18.16/3.29 % (813837)------------------------------
% 18.16/3.29 % (813837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813837)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813837)Termination reason: Instruction limit
% 18.16/3.29 % (813837)Termination phase: Saturation
% 18.16/3.29 % (813837)Time elapsed: 0.160 s
% 18.16/3.29 % (813837)Peak memory usage: 90 MB
% 18.16/3.29 % (813837)Instructions burned: 296 (million)
% 18.16/3.29 % (813844)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=264152477:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 18.16/3.29 % (813835)Instruction limit reached!
% 18.16/3.29 % (813835)------------------------------
% 18.16/3.29 % (813835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.16/3.29 % (813835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.16/3.29 % (813835)CaDiCaL version: 2.1.3
% 18.16/3.29 % (813835)Termination reason: Instruction limit
% 18.16/3.29 % (813835)Termination phase: Saturation
% 18.16/3.29 % (813835)Time elapsed: 0.241 s
% 18.69/3.48 % (813835)Peak memory usage: 118 MB
% 18.69/3.48 % (813835)Instructions burned: 349 (million)
% 18.69/3.48 % (813842)Instruction limit reached!
% 18.69/3.48 % (813842)------------------------------
% 18.69/3.48 % (813842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813842)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813842)Termination reason: Instruction limit
% 18.69/3.48 % (813842)Termination phase: Saturation
% 18.69/3.48 % (813842)Time elapsed: 0.125 s
% 18.69/3.48 % (813842)Peak memory usage: 118 MB
% 18.69/3.48 % (813842)Instructions burned: 331 (million)
% 18.69/3.48 % (813845)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1854369160:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 18.69/3.48 % (813847)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3228604208:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 18.69/3.48 % (813832)Instruction limit reached!
% 18.69/3.48 % (813832)------------------------------
% 18.69/3.48 % (813832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813832)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813832)Termination reason: Instruction limit
% 18.69/3.48 % (813832)Termination phase: Saturation
% 18.69/3.48 % (813832)Time elapsed: 0.359 s
% 18.69/3.48 % (813832)Peak memory usage: 135 MB
% 18.69/3.48 % (813832)Instructions burned: 483 (million)
% 18.69/3.48 % (813849)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3573482789:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 18.69/3.48 % (813850)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1132949978:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 18.69/3.48 % (813851)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=3584378003:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi)
% 18.69/3.48 % (813844)Instruction limit reached!
% 18.69/3.48 % (813844)------------------------------
% 18.69/3.48 % (813844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813844)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813844)Termination reason: Instruction limit
% 18.69/3.48 % (813844)Termination phase: Saturation
% 18.69/3.48 % (813844)Time elapsed: 0.212 s
% 18.69/3.48 % (813844)Peak memory usage: 118 MB
% 18.69/3.48 % (813844)Instructions burned: 282 (million)
% 18.69/3.48 % (813854)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=90583970:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 18.69/3.48 % (813851)Instruction limit reached!
% 18.69/3.48 % (813851)------------------------------
% 18.69/3.48 % (813851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813851)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813851)Termination reason: Instruction limit
% 18.69/3.48 % (813851)Termination phase: Saturation
% 18.69/3.48 % (813851)Time elapsed: 0.131 s
% 18.69/3.48 % (813851)Peak memory usage: 135 MB
% 18.69/3.48 % (813851)Instructions burned: 277 (million)
% 18.69/3.48 % (813847)Instruction limit reached!
% 18.69/3.48 % (813847)------------------------------
% 18.69/3.48 % (813847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813847)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813847)Termination reason: Instruction limit
% 18.69/3.48 % (813847)Termination phase: Saturation
% 18.69/3.48 % (813847)Time elapsed: 0.225 s
% 18.69/3.48 % (813847)Peak memory usage: 117 MB
% 18.69/3.48 % (813847)Instructions burned: 322 (million)
% 18.69/3.48 % (813845)Instruction limit reached!
% 18.69/3.48 % (813845)------------------------------
% 18.69/3.48 % (813845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.69/3.48 % (813845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.69/3.48 % (813845)CaDiCaL version: 2.1.3
% 18.69/3.48 % (813845)Termination reason: Instruction limit
% 20.98/3.97 % (813845)Termination phase: Saturation
% 20.98/3.97 % (813845)Time elapsed: 0.271 s
% 20.98/3.97 % (813845)Peak memory usage: 97 MB
% 20.98/3.97 % (813845)Instructions burned: 486 (million)
% 20.98/3.97 % (813858)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1794237102:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 20.98/3.97 % (813849)Instruction limit reached!
% 20.98/3.97 % (813849)------------------------------
% 20.98/3.97 % (813849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.97 % (813849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.97 % (813849)CaDiCaL version: 2.1.3
% 20.98/3.97 % (813849)Termination reason: Instruction limit
% 20.98/3.97 % (813849)Termination phase: Saturation
% 20.98/3.97 % (813849)Time elapsed: 0.249 s
% 20.98/3.97 % (813849)Peak memory usage: 118 MB
% 20.98/3.97 % (813849)Instructions burned: 418 (million)
% 20.98/3.97 % (813861)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=2829909662:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 20.98/3.97 % (813862)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1070118561:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 20.98/3.97 % (813850)Instruction limit reached!
% 20.98/3.97 % (813850)------------------------------
% 20.98/3.97 % (813850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.97 % (813850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.97 % (813850)CaDiCaL version: 2.1.3
% 20.98/3.97 % (813850)Termination reason: Instruction limit
% 20.98/3.97 % (813850)Termination phase: Saturation
% 20.98/3.97 % (813850)Time elapsed: 0.330 s
% 20.98/3.97 % (813850)Peak memory usage: 119 MB
% 20.98/3.97 % (813850)Instructions burned: 471 (million)
% 20.98/3.97 % (813863)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=446608526:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 20.98/3.97 % (813865)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1353725019:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 20.98/3.97 % (813854)Instruction limit reached!
% 20.98/3.97 % (813854)------------------------------
% 20.98/3.97 % (813854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.97 % (813854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.97 % (813854)CaDiCaL version: 2.1.3
% 20.98/3.97 % (813854)Termination reason: Instruction limit
% 20.98/3.97 % (813854)Termination phase: Saturation
% 20.98/3.97 % (813854)Time elapsed: 0.268 s
% 20.98/3.97 % (813854)Peak memory usage: 118 MB
% 20.98/3.97 % (813854)Instructions burned: 377 (million)
% 20.98/3.97 % (813861)Instruction limit reached!
% 20.98/3.97 % (813861)------------------------------
% 20.98/3.97 % (813861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.97 % (813861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.97 % (813861)CaDiCaL version: 2.1.3
% 20.98/3.97 % (813861)Termination reason: Instruction limit
% 20.98/3.97 % (813861)Termination phase: Saturation
% 20.98/3.97 % (813861)Time elapsed: 0.176 s
% 20.98/3.97 % (813861)Peak memory usage: 94 MB
% 20.98/3.97 % (813861)Instructions burned: 513 (million)
% 20.98/3.97 % (813858)Instruction limit reached!
% 20.98/3.97 % (813858)------------------------------
% 20.98/3.97 % (813858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.97 % (813858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.97 % (813858)CaDiCaL version: 2.1.3
% 20.98/3.97 % (813858)Termination reason: Instruction limit
% 20.98/3.97 % (813858)Termination phase: Saturation
% 20.98/3.97 % (813858)Time elapsed: 0.267 s
% 20.98/3.97 % (813858)Peak memory usage: 118 MB
% 20.98/3.97 % (813858)Instructions burned: 389 (million)
% 20.98/3.97 % (813868)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=983206249:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 20.98/3.97 % (813872)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2576289868:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 26.53/4.47 % (813871)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=1549791527:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi)
% 26.53/4.47 % (813863)Instruction limit reached!
% 26.53/4.47 % (813863)------------------------------
% 26.53/4.47 % (813863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813863)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813863)Termination reason: Instruction limit
% 26.53/4.47 % (813863)Termination phase: Saturation
% 26.53/4.47 % (813863)Time elapsed: 0.215 s
% 26.53/4.47 % (813863)Peak memory usage: 91 MB
% 26.53/4.47 % (813863)Instructions burned: 360 (million)
% 26.53/4.47 % (813862)Instruction limit reached!
% 26.53/4.47 % (813862)------------------------------
% 26.53/4.47 % (813862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813862)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813862)Termination reason: Instruction limit
% 26.53/4.47 % (813862)Termination phase: Saturation
% 26.53/4.47 % (813862)Time elapsed: 0.258 s
% 26.53/4.47 % (813862)Peak memory usage: 135 MB
% 26.53/4.47 % (813862)Instructions burned: 335 (million)
% 26.53/4.47 % (813874)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2537654302:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 26.53/4.47 % (813865)Instruction limit reached!
% 26.53/4.47 % (813865)------------------------------
% 26.53/4.47 % (813865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813865)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813865)Termination reason: Instruction limit
% 26.53/4.47 % (813865)Termination phase: Saturation
% 26.53/4.47 % (813865)Time elapsed: 0.258 s
% 26.53/4.47 % (813865)Peak memory usage: 120 MB
% 26.53/4.47 % (813865)Instructions burned: 344 (million)
% 26.53/4.47 % (813872)Instruction limit reached!
% 26.53/4.47 % (813872)------------------------------
% 26.53/4.47 % (813872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813872)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813872)Termination reason: Instruction limit
% 26.53/4.47 % (813872)Termination phase: Saturation
% 26.53/4.47 % (813872)Time elapsed: 0.106 s
% 26.53/4.47 % (813872)Peak memory usage: 92 MB
% 26.53/4.47 % (813872)Instructions burned: 276 (million)
% 26.53/4.47 % (813868)Instruction limit reached!
% 26.53/4.47 % (813868)------------------------------
% 26.53/4.47 % (813868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813868)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813868)Termination reason: Instruction limit
% 26.53/4.47 % (813868)Termination phase: Saturation
% 26.53/4.47 % (813868)Time elapsed: 0.184 s
% 26.53/4.47 % (813868)Peak memory usage: 117 MB
% 26.53/4.47 % (813868)Instructions burned: 262 (million)
% 26.53/4.47 % (813877)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2758790978:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 26.53/4.47 % (813871)Instruction limit reached!
% 26.53/4.47 % (813871)------------------------------
% 26.53/4.47 % (813871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813871)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813871)Termination reason: Instruction limit
% 26.53/4.47 % (813871)Termination phase: Saturation
% 26.53/4.47 % (813871)Time elapsed: 0.172 s
% 26.53/4.47 % (813871)Peak memory usage: 117 MB
% 26.53/4.47 % (813871)Instructions burned: 235 (million)
% 26.53/4.47 % (813874)Instruction limit reached!
% 26.53/4.47 % (813874)------------------------------
% 26.53/4.47 % (813874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813874)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813874)Termination reason: Instruction limit
% 26.53/4.47 % (813874)Termination phase: Saturation
% 26.53/4.47 % (813874)Time elapsed: 0.102 s
% 26.53/4.47 % (813874)Peak memory usage: 90 MB
% 26.53/4.47 % (813874)Instructions burned: 147 (million)
% 26.53/4.47 % (813878)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=3107350223:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 26.53/4.47 % (813880)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4233642653:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 26.53/4.47 % (813881)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1516143108:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi)
% 26.53/4.47 % (813882)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=285127538:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi)
% 26.53/4.47 % (813884)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=965706164:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 26.53/4.47 % (813886)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1286263932:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 26.53/4.47 % (813884)Instruction limit reached!
% 26.53/4.47 % (813884)------------------------------
% 26.53/4.47 % (813884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813884)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813884)Termination reason: Instruction limit
% 26.53/4.47 % (813884)Termination phase: Saturation
% 26.53/4.47 % (813884)Time elapsed: 0.093 s
% 26.53/4.47 % (813884)Peak memory usage: 116 MB
% 26.53/4.47 % (813884)Instructions burned: 107 (million)
% 26.53/4.47 % (813878)Instruction limit reached!
% 26.53/4.47 % (813878)------------------------------
% 26.53/4.47 % (813878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813878)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813878)Termination reason: Instruction limit
% 26.53/4.47 % (813878)Termination phase: Saturation
% 26.53/4.47 % (813878)Time elapsed: 0.240 s
% 26.53/4.47 % (813878)Peak memory usage: 135 MB
% 26.53/4.47 % (813878)Instructions burned: 276 (million)
% 26.53/4.47 % (813892)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
% 26.53/4.47 % (813892)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2013171487:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi)
% 26.53/4.47 % (813880)Instruction limit reached!
% 26.53/4.47 % (813880)------------------------------
% 26.53/4.47 % (813880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813880)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813880)Termination reason: Instruction limit
% 26.53/4.47 % (813880)Termination phase: Saturation
% 26.53/4.47 % (813880)Time elapsed: 0.363 s
% 26.53/4.47 % (813880)Peak memory usage: 96 MB
% 26.53/4.47 % (813880)Instructions burned: 1052 (million)
% 26.53/4.47 % (813893)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2522584935:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi)
% 26.53/4.47 % (813881)Instruction limit reached!
% 26.53/4.47 % (813881)------------------------------
% 26.53/4.47 % (813881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813881)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813881)Termination reason: Instruction limit
% 26.53/4.47 % (813881)Termination phase: Saturation
% 26.53/4.47 % (813881)Time elapsed: 0.361 s
% 26.53/4.47 % (813881)Peak memory usage: 94 MB
% 26.53/4.47 % (813881)Instructions burned: 655 (million)
% 26.53/4.47 % (813886)Instruction limit reached!
% 26.53/4.47 % (813886)------------------------------
% 26.53/4.47 % (813886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813886)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813886)Termination reason: Instruction limit
% 26.53/4.47 % (813886)Termination phase: Saturation
% 26.53/4.47 % (813886)Time elapsed: 0.337 s
% 26.53/4.47 % (813886)Peak memory usage: 135 MB
% 26.53/4.47 % (813886)Instructions burned: 451 (million)
% 26.53/4.47 % (813895)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=66047226:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi)
% 26.53/4.47 % (813893)Instruction limit reached!
% 26.53/4.47 % (813893)------------------------------
% 26.53/4.47 % (813893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813893)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813893)Termination reason: Instruction limit
% 26.53/4.47 % (813893)Termination phase: Saturation
% 26.53/4.47 % (813893)Time elapsed: 0.108 s
% 26.53/4.47 % (813893)Peak memory usage: 117 MB
% 26.53/4.47 % (813893)Instructions burned: 131 (million)
% 26.53/4.47 % (813897)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=731692158:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi)
% 26.53/4.47 % (813895)Instruction limit reached!
% 26.53/4.47 % (813895)------------------------------
% 26.53/4.47 % (813895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813895)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813895)Termination reason: Instruction limit
% 26.53/4.47 % (813895)Termination phase: Saturation
% 26.53/4.47 % (813895)Time elapsed: 0.122 s
% 26.53/4.47 % (813895)Peak memory usage: 118 MB
% 26.53/4.47 % (813895)Instructions burned: 314 (million)
% 26.53/4.47 % (813898)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=585017274:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 26.53/4.47 % (813900)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2744446683:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi)
% 26.53/4.47 % (813882)First to succeed.
% 26.53/4.47 % (813882)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-813730"
% 26.53/4.47 % (813902)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3923010018:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi)
% 26.53/4.47 % (813897)Also succeeded, but the first one will report.
% 26.53/4.47 % (813900)Instruction limit reached!
% 26.53/4.47 % (813900)------------------------------
% 26.53/4.47 % (813900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/4.47 % (813900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/4.47 % (813900)CaDiCaL version: 2.1.3
% 26.53/4.47 % (813900)Termination reason: Instruction limit
% 26.53/4.47 % (813900)Termination phase: Saturation
% 26.53/4.47 % (813900)Time elapsed: 0.205 s
% 26.53/4.47 % (813900)Peak memory usage: 93 MB
% 26.53/4.47 % (813900)Instructions burned: 307 (million)
% 26.53/4.47 % (813882)Refutation found. Thanks to Tanya!
% 26.53/4.47 % SZS status Theorem for theBenchmark
% 26.53/4.47 % SZS output start Proof for theBenchmark
% See solution above
% 27.36/4.57 % (813882)------------------------------
% 27.36/4.57 % (813882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.36/4.57 % (813882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.36/4.57 % (813882)CaDiCaL version: 2.1.3
% 27.36/4.57 % (813882)Termination reason: Refutation
% 27.36/4.57 % (813882)Time elapsed: 0.644 s
% 27.36/4.57 % (813882)Peak memory usage: 98 MB
% 27.36/4.57 % (813882)Instructions burned: 1021 (million)
% 27.36/4.57 % (813882)------------------------------
% 27.36/4.57 % (813882)------------------------------
% 27.36/4.57 % (813730)Success in time 3.804 s
% 27.36/4.57 % Vampire exiting
%------------------------------------------------------------------------------