%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW628_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:59 PM UTC 2026
% Result : Theorem 40.63s 6.81s
% Output : Refutation 43.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of formulae : 94 ( 66 unt; 0 typ; 0 def)
% Number of atoms : 326 ( 165 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 327 ( 95 ~; 32 |; 139 &)
% ( 0 <=>; 61 =>; 0 <=; 0 <~>)
% Maximal formula depth : 34 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number arithmetic : 69 ( 7 atm; 36 fun; 21 num; 5 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 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 58 ( 56 usr; 27 con; 0-5 aty)
% Number of variables : 281 ( 210 !; 71 ?; 281 :)
% 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,
elt1: $tType ).
tff(type_def_10,type,
list_elt: $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,
length2: ( ty * uni ) > $int ).
tff(func_def_21,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
num_occ1: ( ty * uni * uni ) > $int ).
tff(func_def_23,type,
reverse: ( ty * uni ) > uni ).
tff(func_def_24,type,
t: ty > ty ).
tff(func_def_25,type,
mk_t: ( ty * uni ) > uni ).
tff(func_def_26,type,
elts: ( ty * uni ) > uni ).
tff(func_def_27,type,
length3: ( ty * uni ) > $int ).
tff(func_def_28,type,
elt: ty ).
tff(func_def_29,type,
t2tb: list_elt > uni ).
tff(func_def_30,type,
tb2t: uni > list_elt ).
tff(func_def_31,type,
t2tb1: elt1 > uni ).
tff(func_def_32,type,
tb2t1: uni > elt1 ).
tff(func_def_34,type,
sK0: list_elt > elt1 ).
tff(func_def_35,type,
sK1: list_elt > elt1 ).
tff(func_def_36,type,
sK2: list_elt > elt1 ).
tff(func_def_37,type,
sK3: list_elt > list_elt ).
tff(func_def_38,type,
sK4: ( list_elt * elt1 ) > elt1 ).
tff(func_def_39,type,
sK5: ( uni * ty * uni ) > uni ).
tff(func_def_40,type,
sK6: ( uni * ty * uni ) > uni ).
tff(func_def_41,type,
sK7: list_elt ).
tff(func_def_42,type,
sK8: list_elt ).
tff(func_def_43,type,
sK9: list_elt ).
tff(func_def_44,type,
sK10: list_elt ).
tff(func_def_45,type,
sK11: list_elt ).
tff(func_def_46,type,
sK12: list_elt ).
tff(func_def_47,type,
sK13: elt1 ).
tff(func_def_48,type,
sK14: elt1 ).
tff(func_def_49,type,
sK15: list_elt ).
tff(func_def_50,type,
sK16: elt1 ).
tff(func_def_51,type,
sK17: list_elt ).
tff(func_def_52,type,
sK18: elt1 ).
tff(func_def_53,type,
sK19: list_elt ).
tff(func_def_54,type,
sK20: elt1 ).
tff(func_def_55,type,
sK21: list_elt ).
tff(func_def_56,type,
sK22: list_elt ).
tff(func_def_57,type,
sK23: elt1 ).
tff(func_def_58,type,
sK24: ( list_elt * list_elt ) > elt1 ).
tff(func_def_59,type,
sK25: ( list_elt * list_elt ) > elt1 ).
tff(func_def_60,type,
sK26: ( ty * uni * uni ) > uni ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
permut: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
le1: ( elt1 * elt1 ) > $o ).
tff(pred_def_7,type,
sorted1: list_elt > $o ).
tff(f16,axiom,
! [X1: uni,X2: uni,X0: ty] :
( sort1(X0,X1)
=> ( cons_proj_11(X0,cons(X0,X1,X2)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cons_proj_1_def1) ).
tff(f18,axiom,
! [X2: uni,X1: uni,X0: ty] : ( cons_proj_21(X0,cons(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cons_proj_2_def1) ).
tff(f25,axiom,
! [X1: uni,X0: ty] :
( ( infix_plpl(X0,nil(X0),X1) = X1 )
& ! [X3: uni,X2: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f26,axiom,
! [X2: uni,X1: uni,X3: uni,X0: ty] : ( infix_plpl(X0,X1,infix_plpl(X0,X2,X3)) = infix_plpl(X0,infix_plpl(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',append_assoc) ).
tff(f33,axiom,
! [X2: uni,X0: ty,X1: uni,X3: uni] : ( num_occ1(X0,X1,infix_plpl(X0,X2,X3)) = $sum(num_occ1(X0,X1,X2),num_occ1(X0,X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',append_Num_Occ) ).
tff(f42,axiom,
! [X0: ty,X2: uni,X1: uni] :
( ( permut(X0,X1,X2)
=> ! [X3: uni] : ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) ) )
& ( ! [X3: uni] :
( sort1(X0,X3)
=> ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) ) )
=> permut(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_def) ).
tff(f44,axiom,
! [X2: uni,X0: ty,X1: uni] :
( permut(X0,X1,X2)
=> permut(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_sym) ).
tff(f48,axiom,
! [X2: uni,X0: ty,X1: uni,X3: uni] : permut(X0,infix_plpl(X0,cons(X0,X1,X2),X3),infix_plpl(X0,X2,cons(X0,X1,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_cons_append) ).
tff(f64,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f66,axiom,
! [X0: elt1] : sort1(elt,t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f74,conjecture,
! [X1: list_elt,X0: list_elt,X2: list_elt] :
( ( sorted1(X1)
& sorted1(X0)
& ( X2 = tb2t(nil(elt)) ) )
=> ! [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1)))
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X5))
=> le1(X6,X7) ) )
& sorted1(X5)
& sorted1(X3)
& ! [X7: elt1,X6: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X4))
=> le1(X6,X7) ) )
& sorted1(X4) )
=> ( $less(0,length2(elt,t2tb(X5)))
=> ( ( length2(elt,t2tb(X5)) != 0 )
=> ( ( length2(elt,t2tb(X4)) != 0 )
=> ( ( X5 != tb2t(nil(elt)) )
=> ! [X8: elt1] :
( ? [X9: list_elt,X6: elt1] :
( ( X8 = X6 )
& ( X5 = tb2t(cons(elt,t2tb1(X6),t2tb(X9))) ) )
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X9: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X9 = X6 )
& ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) ) )
=> ( ~ le1(X8,X9)
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X11: list_elt,X12: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) )
& ( X11 = X10 )
& ( X12 = X6 ) )
=> ! [X13: list_elt] :
( ( X13 = tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X12),nil(elt)))) )
=> permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X13),t2tb(X5)),t2tb(X11)),infix_plpl(elt,t2tb(X0),t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_merge) ).
tff(f75,negated_conjecture,
~ ! [X1: list_elt,X0: list_elt,X2: list_elt] :
( ( sorted1(X1)
& sorted1(X0)
& ( X2 = tb2t(nil(elt)) ) )
=> ! [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1)))
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X5))
=> le1(X6,X7) ) )
& sorted1(X5)
& sorted1(X3)
& ! [X7: elt1,X6: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X4))
=> le1(X6,X7) ) )
& sorted1(X4) )
=> ( $less(0,length2(elt,t2tb(X5)))
=> ( ( length2(elt,t2tb(X5)) != 0 )
=> ( ( length2(elt,t2tb(X4)) != 0 )
=> ( ( X5 != tb2t(nil(elt)) )
=> ! [X8: elt1] :
( ? [X9: list_elt,X6: elt1] :
( ( X8 = X6 )
& ( X5 = tb2t(cons(elt,t2tb1(X6),t2tb(X9))) ) )
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X9: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X9 = X6 )
& ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) ) )
=> ( ~ le1(X8,X9)
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X11: list_elt,X12: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) )
& ( X11 = X10 )
& ( X12 = X6 ) )
=> ! [X13: list_elt] :
( ( X13 = tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X12),nil(elt)))) )
=> permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X13),t2tb(X5)),t2tb(X11)),infix_plpl(elt,t2tb(X0),t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f74]) ).
tff(f78,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f79,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum($sum(X0,X1),X2) = $sum(X0,$sum(X1,X2)) ),
introduced(definition,[],[tha_associativity]) ).
tff(f100,plain,
! [X1: uni,X0: ty,X2: uni] :
( ( permut(X0,X2,X1)
=> ! [X3: uni] : ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) ) )
& ( ! [X4: uni] :
( sort1(X0,X4)
=> ( num_occ1(X0,X4,X1) = num_occ1(X0,X4,X2) ) )
=> permut(X0,X2,X1) ) ),
inference(rectify,[],[f42]) ).
tff(f112,plain,
! [X3: uni,X2: uni,X1: ty,X0: uni] : ( num_occ1(X1,X2,infix_plpl(X1,X0,X3)) = $sum(num_occ1(X1,X2,X0),num_occ1(X1,X2,X3)) ),
inference(rectify,[],[f33]) ).
tff(f118,plain,
! [X0: uni,X1: ty,X2: uni] :
( permut(X1,X2,X0)
=> permut(X1,X0,X2) ),
inference(rectify,[],[f44]) ).
tff(f120,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty] : ( infix_plpl(X3,infix_plpl(X3,X1,X0),X2) = infix_plpl(X3,X1,infix_plpl(X3,X0,X2)) ),
inference(rectify,[],[f26]) ).
tff(f124,plain,
! [X3: uni,X1: ty,X2: uni,X0: uni] : permut(X1,infix_plpl(X1,cons(X1,X2,X0),X3),infix_plpl(X1,X0,cons(X1,X2,X3))),
inference(rectify,[],[f48]) ).
tff(f126,plain,
! [X1: uni,X2: ty,X0: uni] :
( sort1(X2,X0)
=> ( cons_proj_11(X2,cons(X2,X0,X1)) = X0 ) ),
inference(rectify,[],[f16]) ).
tff(f134,plain,
~ ! [X0: list_elt,X1: list_elt,X2: list_elt] :
( ( ( X2 = tb2t(nil(elt)) )
& sorted1(X1)
& sorted1(X0) )
=> ! [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X5))
=> ( mem(elt,t2tb1(X7),t2tb(X4))
=> le1(X6,X7) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X5),t2tb(X4)),t2tb(X3)),infix_plpl(elt,t2tb(X1),t2tb(X0)))
& sorted1(X3)
& ! [X9: elt1,X8: elt1] :
( mem(elt,t2tb1(X9),t2tb(X5))
=> ( mem(elt,t2tb1(X8),t2tb(X3))
=> le1(X9,X8) ) )
& sorted1(X5)
& sorted1(X4) )
=> ( $less(0,length2(elt,t2tb(X4)))
=> ( ( 0 != length2(elt,t2tb(X4)) )
=> ( ( 0 != length2(elt,t2tb(X3)) )
=> ( ( tb2t(nil(elt)) != X4 )
=> ! [X10: elt1] :
( ? [X11: list_elt,X12: elt1] :
( ( X10 = X12 )
& ( tb2t(cons(elt,t2tb1(X12),t2tb(X11))) = X4 ) )
=> ( ( tb2t(nil(elt)) != X3 )
=> ! [X13: elt1] :
( ? [X14: elt1,X15: list_elt] :
( ( X13 = X14 )
& ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X3 ) )
=> ( ~ le1(X10,X13)
=> ( ( tb2t(nil(elt)) != X3 )
=> ! [X17: elt1,X16: list_elt] :
( ? [X19: list_elt,X18: elt1] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X3 )
& ( X17 = X18 )
& ( X16 = X19 ) )
=> ! [X20: list_elt] :
( ( tb2t(infix_plpl(elt,t2tb(X5),cons(elt,t2tb1(X17),nil(elt)))) = X20 )
=> permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X4)),t2tb(X16)),infix_plpl(elt,t2tb(X1),t2tb(X0))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f75]) ).
tff(f136,plain,
! [X0: uni,X1: uni,X2: ty] : ( cons_proj_21(X2,cons(X2,X1,X0)) = X0 ),
inference(rectify,[],[f18]) ).
tff(f138,plain,
! [X0: uni,X1: ty] :
( ( infix_plpl(X1,nil(X1),X0) = X0 )
& ! [X2: uni,X3: uni] : ( infix_plpl(X1,cons(X1,X3,X2),X0) = cons(X1,X3,infix_plpl(X1,X2,X0)) ) ),
inference(rectify,[],[f25]) ).
tff(f149,plain,
! [X0: uni,X2: ty,X1: uni] :
( ( cons_proj_11(X2,cons(X2,X0,X1)) = X0 )
| ~ sort1(X2,X0) ),
inference(ennf_transformation,[],[f126]) ).
tff(f156,plain,
! [X2: uni,X1: ty,X0: uni] :
( permut(X1,X0,X2)
| ~ permut(X1,X2,X0) ),
inference(ennf_transformation,[],[f118]) ).
tff(f160,plain,
? [X0: list_elt,X1: list_elt,X2: list_elt] :
( ? [X4: list_elt,X5: list_elt,X3: list_elt] :
( ? [X10: elt1] :
( ? [X13: elt1] :
( ? [X16: list_elt,X17: elt1] :
( ? [X19: list_elt,X18: elt1] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X3 )
& ( X17 = X18 )
& ( X16 = X19 ) )
& ? [X20: list_elt] :
( ( tb2t(infix_plpl(elt,t2tb(X5),cons(elt,t2tb1(X17),nil(elt)))) = X20 )
& ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X4)),t2tb(X16)),infix_plpl(elt,t2tb(X1),t2tb(X0))) ) )
& ( tb2t(nil(elt)) != X3 )
& ~ le1(X10,X13)
& ? [X14: elt1,X15: list_elt] :
( ( X13 = X14 )
& ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X3 ) ) )
& ( tb2t(nil(elt)) != X3 )
& ? [X11: list_elt,X12: elt1] :
( ( X10 = X12 )
& ( tb2t(cons(elt,t2tb1(X12),t2tb(X11))) = X4 ) ) )
& ( tb2t(nil(elt)) != X4 )
& ( 0 != length2(elt,t2tb(X3)) )
& ( 0 != length2(elt,t2tb(X4)) )
& $less(0,length2(elt,t2tb(X4)))
& ! [X6: elt1,X7: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X7),t2tb(X4))
| ~ mem(elt,t2tb1(X6),t2tb(X5)) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X5),t2tb(X4)),t2tb(X3)),infix_plpl(elt,t2tb(X1),t2tb(X0)))
& sorted1(X3)
& ! [X9: elt1,X8: elt1] :
( le1(X9,X8)
| ~ mem(elt,t2tb1(X8),t2tb(X3))
| ~ mem(elt,t2tb1(X9),t2tb(X5)) )
& sorted1(X5)
& sorted1(X4) )
& ( X2 = tb2t(nil(elt)) )
& sorted1(X1)
& sorted1(X0) ),
inference(ennf_transformation,[],[f134]) ).
tff(f161,plain,
? [X1: list_elt,X2: list_elt,X0: list_elt] :
( sorted1(X1)
& sorted1(X0)
& ? [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( 0 != length2(elt,t2tb(X3)) )
& ! [X9: elt1,X8: elt1] :
( le1(X9,X8)
| ~ mem(elt,t2tb1(X9),t2tb(X5))
| ~ mem(elt,t2tb1(X8),t2tb(X3)) )
& ! [X7: elt1,X6: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X6),t2tb(X5))
| ~ mem(elt,t2tb1(X7),t2tb(X4)) )
& sorted1(X4)
& ( 0 != length2(elt,t2tb(X4)) )
& $less(0,length2(elt,t2tb(X4)))
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X5),t2tb(X4)),t2tb(X3)),infix_plpl(elt,t2tb(X1),t2tb(X0)))
& sorted1(X5)
& ( tb2t(nil(elt)) != X4 )
& sorted1(X3)
& ? [X10: elt1] :
( ( tb2t(nil(elt)) != X3 )
& ? [X13: elt1] :
( ? [X16: list_elt,X17: elt1] :
( ? [X19: list_elt,X18: elt1] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X3 )
& ( X17 = X18 )
& ( X16 = X19 ) )
& ? [X20: list_elt] :
( ( tb2t(infix_plpl(elt,t2tb(X5),cons(elt,t2tb1(X17),nil(elt)))) = X20 )
& ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X4)),t2tb(X16)),infix_plpl(elt,t2tb(X1),t2tb(X0))) ) )
& ? [X14: elt1,X15: list_elt] :
( ( X13 = X14 )
& ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X3 ) )
& ( tb2t(nil(elt)) != X3 )
& ~ le1(X10,X13) )
& ? [X11: list_elt,X12: elt1] :
( ( X10 = X12 )
& ( tb2t(cons(elt,t2tb1(X12),t2tb(X11))) = X4 ) ) ) )
& ( X2 = tb2t(nil(elt)) ) ),
inference(flattening,[],[f160]) ).
tff(f171,plain,
! [X0: ty,X1: uni,X2: uni] :
( ( permut(X0,X2,X1)
| ? [X4: uni] :
( ( num_occ1(X0,X4,X1) != num_occ1(X0,X4,X2) )
& sort1(X0,X4) ) )
& ( ~ permut(X0,X2,X1)
| ! [X3: uni] : ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) ) ) ),
inference(ennf_transformation,[],[f100]) ).
tff(f186,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni] : ( $sum(num_occ1(X2,X1,X3),num_occ1(X2,X1,X0)) = num_occ1(X2,X1,infix_plpl(X2,X3,X0)) ),
inference(rectify,[],[f112]) ).
tff(f206,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni] : permut(X1,infix_plpl(X1,cons(X1,X2,X3),X0),infix_plpl(X1,X3,cons(X1,X2,X0))),
inference(rectify,[],[f124]) ).
tff(f215,plain,
? [X0: list_elt,X1: list_elt,X2: list_elt] :
( sorted1(X0)
& sorted1(X2)
& ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( 0 != length2(elt,t2tb(X5)) )
& ! [X6: elt1,X7: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X6),t2tb(X4))
| ~ mem(elt,t2tb1(X7),t2tb(X5)) )
& ! [X8: elt1,X9: elt1] :
( le1(X9,X8)
| ~ mem(elt,t2tb1(X9),t2tb(X4))
| ~ mem(elt,t2tb1(X8),t2tb(X3)) )
& sorted1(X3)
& ( 0 != length2(elt,t2tb(X3)) )
& $less(0,length2(elt,t2tb(X3)))
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),infix_plpl(elt,t2tb(X0),t2tb(X2)))
& sorted1(X4)
& ( tb2t(nil(elt)) != X3 )
& sorted1(X5)
& ? [X10: elt1] :
( ( tb2t(nil(elt)) != X5 )
& ? [X11: elt1] :
( ? [X12: list_elt,X13: elt1] :
( ? [X14: list_elt,X15: elt1] :
( ( tb2t(cons(elt,t2tb1(X15),t2tb(X14))) = X5 )
& ( X13 = X15 )
& ( X12 = X14 ) )
& ? [X16: list_elt] :
( ( tb2t(infix_plpl(elt,t2tb(X4),cons(elt,t2tb1(X13),nil(elt)))) = X16 )
& ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X16),t2tb(X3)),t2tb(X12)),infix_plpl(elt,t2tb(X0),t2tb(X2))) ) )
& ? [X17: elt1,X18: list_elt] :
( ( X11 = X17 )
& ( tb2t(cons(elt,t2tb1(X17),t2tb(X18))) = X5 ) )
& ( tb2t(nil(elt)) != X5 )
& ~ le1(X10,X11) )
& ? [X19: list_elt,X20: elt1] :
( ( X10 = X20 )
& ( tb2t(cons(elt,t2tb1(X20),t2tb(X19))) = X3 ) ) ) )
& ( tb2t(nil(elt)) = X1 ) ),
inference(rectify,[],[f161]) ).
tff(f216,plain,
( sorted1(sK7)
& sorted1(sK9)
& ( 0 != length2(elt,t2tb(sK12)) )
& ! [X6: elt1,X7: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X6),t2tb(sK11))
| ~ mem(elt,t2tb1(X7),t2tb(sK12)) )
& ! [X8: elt1,X9: elt1] :
( le1(X9,X8)
| ~ mem(elt,t2tb1(X9),t2tb(sK11))
| ~ mem(elt,t2tb1(X8),t2tb(sK10)) )
& sorted1(sK10)
& ( 0 != length2(elt,t2tb(sK10)) )
& $less(0,length2(elt,t2tb(sK10)))
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK11),t2tb(sK10)),t2tb(sK12)),infix_plpl(elt,t2tb(sK7),t2tb(sK9)))
& sorted1(sK11)
& ( tb2t(nil(elt)) != sK10 )
& sorted1(sK12)
& ( tb2t(nil(elt)) != sK12 )
& ( tb2t(cons(elt,t2tb1(sK18),t2tb(sK17))) = sK12 )
& ( sK16 = sK18 )
& ( sK15 = sK17 )
& ( sK19 = tb2t(infix_plpl(elt,t2tb(sK11),cons(elt,t2tb1(sK16),nil(elt)))) )
& ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK19),t2tb(sK10)),t2tb(sK15)),infix_plpl(elt,t2tb(sK7),t2tb(sK9)))
& ( sK14 = sK20 )
& ( tb2t(cons(elt,t2tb1(sK20),t2tb(sK21))) = sK12 )
& ( tb2t(nil(elt)) != sK12 )
& ~ le1(sK13,sK14)
& ( sK13 = sK23 )
& ( sK10 = tb2t(cons(elt,t2tb1(sK23),t2tb(sK22))) )
& ( tb2t(nil(elt)) = sK8 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK11),skolemize(X5,sK12),skolemize(X10,sK13),skolemize(X11,sK14),skolemize(X12,sK15),skolemize(X13,sK16),skolemize(X14,sK17),skolemize(X15,sK18),skolemize(X16,sK19),skolemize(X17,sK20),skolemize(X18,sK21),skolemize(X19,sK22),skolemize(X20,sK23)],[f215]) ).
tff(f225,plain,
! [X0: uni,X1: ty,X2: uni] :
( permut(X1,X2,X0)
| ~ permut(X1,X0,X2) ),
inference(rectify,[],[f156]) ).
tff(f227,plain,
! [X0: ty,X1: uni,X2: uni] :
( ( permut(X0,X2,X1)
| ? [X3: uni] :
( ( num_occ1(X0,X3,X1) != num_occ1(X0,X3,X2) )
& sort1(X0,X3) ) )
& ( ~ permut(X0,X2,X1)
| ! [X4: uni] : ( num_occ1(X0,X4,X1) = num_occ1(X0,X4,X2) ) ) ),
inference(rectify,[],[f171]) ).
tff(f228,plain,
! [X0: ty,X1: uni,X2: uni] :
( ( permut(X0,X2,X1)
| ( ( num_occ1(X0,sK26(X0,X1,X2),X1) != num_occ1(X0,sK26(X0,X1,X2),X2) )
& sort1(X0,sK26(X0,X1,X2)) ) )
& ( ~ permut(X0,X2,X1)
| ! [X4: uni] : ( num_occ1(X0,X4,X1) = num_occ1(X0,X4,X2) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X3,sK26(X0,X1,X2))],[f227]) ).
tff(f235,plain,
! [X0: uni,X1: ty,X2: uni] :
( ( cons_proj_11(X1,cons(X1,X0,X2)) = X0 )
| ~ sort1(X1,X0) ),
inference(rectify,[],[f149]) ).
tff(f245,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] : ( $sum(num_occ1(X2,X1,X3),num_occ1(X2,X1,X0)) = num_occ1(X2,X1,infix_plpl(X2,X3,X0)) ),
inference(cnf_transformation,[],[f186]) ).
tff(f263,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] : ( infix_plpl(X1,cons(X1,X3,X2),X0) = cons(X1,X3,infix_plpl(X1,X2,X0)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f264,plain,
! [X0: uni,X1: ty] : ( infix_plpl(X1,nil(X1),X0) = X0 ),
inference(cnf_transformation,[],[f138]) ).
tff(f266,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f64]) ).
tff(f286,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] : permut(X1,infix_plpl(X1,cons(X1,X2,X3),X0),infix_plpl(X1,X3,cons(X1,X2,X0))),
inference(cnf_transformation,[],[f206]) ).
tff(f308,plain,
tb2t(cons(elt,t2tb1(sK20),t2tb(sK21))) = sK12,
inference(cnf_transformation,[],[f216]) ).
tff(f310,plain,
~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK19),t2tb(sK10)),t2tb(sK15)),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),
inference(cnf_transformation,[],[f216]) ).
tff(f311,plain,
sK19 = tb2t(infix_plpl(elt,t2tb(sK11),cons(elt,t2tb1(sK16),nil(elt)))),
inference(cnf_transformation,[],[f216]) ).
tff(f312,plain,
sK15 = sK17,
inference(cnf_transformation,[],[f216]) ).
tff(f313,plain,
sK16 = sK18,
inference(cnf_transformation,[],[f216]) ).
tff(f314,plain,
tb2t(cons(elt,t2tb1(sK18),t2tb(sK17))) = sK12,
inference(cnf_transformation,[],[f216]) ).
tff(f319,plain,
permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK11),t2tb(sK10)),t2tb(sK12)),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),
inference(cnf_transformation,[],[f216]) ).
tff(f329,plain,
! [X2: ty,X0: uni,X1: uni] : ( cons_proj_21(X2,cons(X2,X1,X0)) = X0 ),
inference(cnf_transformation,[],[f136]) ).
tff(f333,plain,
! [X0: elt1] : sort1(elt,t2tb1(X0)),
inference(cnf_transformation,[],[f66]) ).
tff(f342,plain,
! [X2: uni,X0: uni,X1: ty] :
( permut(X1,X2,X0)
| ~ permut(X1,X0,X2) ),
inference(cnf_transformation,[],[f225]) ).
tff(f346,plain,
! [X2: uni,X0: ty,X1: uni,X4: uni] :
( ~ permut(X0,X2,X1)
| ( num_occ1(X0,X4,X1) = num_occ1(X0,X4,X2) ) ),
inference(cnf_transformation,[],[f228]) ).
tff(f348,plain,
! [X2: uni,X0: ty,X1: uni] :
( permut(X0,X2,X1)
| ( num_occ1(X0,sK26(X0,X1,X2),X1) != num_occ1(X0,sK26(X0,X1,X2),X2) ) ),
inference(cnf_transformation,[],[f228]) ).
tff(f349,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni] : ( infix_plpl(X3,infix_plpl(X3,X1,X0),X2) = infix_plpl(X3,X1,infix_plpl(X3,X0,X2)) ),
inference(cnf_transformation,[],[f120]) ).
tff(f360,plain,
! [X2: uni,X0: uni,X1: ty] :
( ( cons_proj_11(X1,cons(X1,X0,X2)) = X0 )
| ~ sort1(X1,X0) ),
inference(cnf_transformation,[],[f235]) ).
tff(f363,plain,
sK19 = tb2t(infix_plpl(elt,t2tb(sK11),cons(elt,t2tb1(sK18),nil(elt)))),
inference(definition_unfolding,[],[f311,f313]) ).
tff(f364,plain,
~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK19),t2tb(sK10)),t2tb(sK17)),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),
inference(definition_unfolding,[],[f310,f312]) ).
tff(f372,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK19),infix_plpl(elt,t2tb(sK10),t2tb(sK17))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),
inference(forward_demodulation,[],[f364,f349]) ).
tff(f373,plain,
permut(elt,infix_plpl(elt,t2tb(sK11),infix_plpl(elt,t2tb(sK10),t2tb(sK12))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),
inference(forward_demodulation,[],[f319,f349]) ).
tff(f391,plain,
cons(elt,t2tb1(sK20),t2tb(sK21)) = t2tb(sK12),
inference(superposition,[],[f266,f308]) ).
tff(f395,plain,
cons(elt,t2tb1(sK18),t2tb(sK17)) = t2tb(sK12),
inference(superposition,[],[f266,f314]) ).
tff(f465,plain,
infix_plpl(elt,t2tb(sK11),cons(elt,t2tb1(sK18),nil(elt))) = t2tb(sK19),
inference(superposition,[],[f266,f363]) ).
tff(f527,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,t2tb(sK19),infix_plpl(elt,t2tb(sK10),t2tb(sK17)))),
inference(resolution,[],[f372,f342]) ).
tff(f532,plain,
! [X0: uni] : ( num_occ1(elt,X0,infix_plpl(elt,t2tb(sK11),infix_plpl(elt,t2tb(sK10),t2tb(sK12)))) = num_occ1(elt,X0,infix_plpl(elt,t2tb(sK7),t2tb(sK9))) ),
inference(resolution,[],[f373,f346]) ).
tff(f535,plain,
! [X0: uni] : ( $sum(num_occ1(elt,X0,t2tb(sK7)),num_occ1(elt,X0,t2tb(sK9))) = num_occ1(elt,X0,infix_plpl(elt,t2tb(sK11),infix_plpl(elt,t2tb(sK10),t2tb(sK12)))) ),
inference(forward_demodulation,[],[f532,f245]) ).
tff(f537,plain,
! [X0: uni] : ( $sum(num_occ1(elt,X0,t2tb(sK7)),num_occ1(elt,X0,t2tb(sK9))) = $sum(num_occ1(elt,X0,t2tb(sK11)),num_occ1(elt,X0,infix_plpl(elt,t2tb(sK10),t2tb(sK12)))) ),
inference(forward_demodulation,[],[f535,f245]) ).
tff(f539,plain,
! [X0: uni] : ( $sum(num_occ1(elt,X0,infix_plpl(elt,t2tb(sK10),t2tb(sK12))),num_occ1(elt,X0,t2tb(sK11))) = $sum(num_occ1(elt,X0,t2tb(sK7)),num_occ1(elt,X0,t2tb(sK9))) ),
inference(forward_demodulation,[],[f537,f78]) ).
tff(f541,plain,
! [X0: uni] : ( $sum($sum(num_occ1(elt,X0,t2tb(sK10)),num_occ1(elt,X0,t2tb(sK12))),num_occ1(elt,X0,t2tb(sK11))) = $sum(num_occ1(elt,X0,t2tb(sK7)),num_occ1(elt,X0,t2tb(sK9))) ),
inference(forward_demodulation,[],[f539,f245]) ).
tff(f543,plain,
! [X0: uni] : ( $sum(num_occ1(elt,X0,t2tb(sK10)),$sum(num_occ1(elt,X0,t2tb(sK12)),num_occ1(elt,X0,t2tb(sK11)))) = $sum(num_occ1(elt,X0,t2tb(sK7)),num_occ1(elt,X0,t2tb(sK9))) ),
inference(forward_demodulation,[],[f541,f79]) ).
tff(f557,plain,
! [X0: uni] : permut(elt,infix_plpl(elt,cons(elt,t2tb1(sK20),X0),t2tb(sK21)),infix_plpl(elt,X0,t2tb(sK12))),
inference(superposition,[],[f286,f391]) ).
tff(f560,plain,
t2tb(sK21) = cons_proj_21(elt,t2tb(sK12)),
inference(superposition,[],[f329,f391]) ).
tff(f564,plain,
( ~ sort1(elt,t2tb1(sK20))
| ( t2tb1(sK20) = cons_proj_11(elt,t2tb(sK12)) ) ),
inference(superposition,[],[f360,f391]) ).
tff(f571,plain,
! [X0: uni] : permut(elt,cons(elt,t2tb1(sK20),infix_plpl(elt,X0,t2tb(sK21))),infix_plpl(elt,X0,t2tb(sK12))),
inference(forward_demodulation,[],[f557,f263]) ).
tff(f574,plain,
t2tb1(sK20) = cons_proj_11(elt,t2tb(sK12)),
inference(forward_subsumption_resolution,[],[f564,f333]) ).
tff(f589,plain,
! [X0: uni] : permut(elt,cons(elt,t2tb1(sK20),infix_plpl(elt,X0,cons_proj_21(elt,t2tb(sK12)))),infix_plpl(elt,X0,t2tb(sK12))),
inference(forward_demodulation,[],[f571,f560]) ).
tff(f607,plain,
! [X0: uni] : permut(elt,cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,X0,cons_proj_21(elt,t2tb(sK12)))),infix_plpl(elt,X0,t2tb(sK12))),
inference(forward_demodulation,[],[f589,f574]) ).
tff(f624,plain,
cons_proj_21(elt,t2tb(sK12)) = t2tb(sK17),
inference(superposition,[],[f329,f395]) ).
tff(f628,plain,
( ~ sort1(elt,t2tb1(sK18))
| ( t2tb1(sK18) = cons_proj_11(elt,t2tb(sK12)) ) ),
inference(superposition,[],[f360,f395]) ).
tff(f638,plain,
t2tb1(sK18) = cons_proj_11(elt,t2tb(sK12)),
inference(forward_subsumption_resolution,[],[f628,f333]) ).
tff(f647,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,t2tb(sK19),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),
inference(backward_demodulation,[],[f527,f624]) ).
tff(f661,plain,
infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),nil(elt))) = t2tb(sK19),
inference(backward_demodulation,[],[f465,f638]) ).
tff(f678,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),nil(elt))),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),
inference(backward_demodulation,[],[f647,f661]) ).
tff(f683,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,t2tb(sK11),infix_plpl(elt,cons(elt,cons_proj_11(elt,t2tb(sK12)),nil(elt)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(forward_demodulation,[],[f678,f349]) ).
tff(f687,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,nil(elt),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))))),
inference(forward_demodulation,[],[f683,f263]) ).
tff(f691,plain,
~ permut(elt,infix_plpl(elt,t2tb(sK7),t2tb(sK9)),infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(forward_demodulation,[],[f687,f264]) ).
tff(f1004,plain,
num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))) != num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(resolution,[],[f691,f348]) ).
tff(f1006,plain,
num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))) != $sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(forward_demodulation,[],[f1004,f245]) ).
tff(f1007,plain,
$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK7)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK9))) != $sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(forward_demodulation,[],[f1006,f245]) ).
tff(f1008,plain,
$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK10)),$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK12)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)))) != $sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12)))))),
inference(forward_demodulation,[],[f1007,f543]) ).
tff(f1501,plain,
! [X0: uni,X1: uni] : ( num_occ1(elt,X0,cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,X1,cons_proj_21(elt,t2tb(sK12))))) = num_occ1(elt,X0,infix_plpl(elt,X1,t2tb(sK12))) ),
inference(resolution,[],[f607,f346]) ).
tff(f1520,plain,
! [X0: uni,X1: uni] : ( num_occ1(elt,X0,cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,X1,cons_proj_21(elt,t2tb(sK12))))) = $sum(num_occ1(elt,X0,X1),num_occ1(elt,X0,t2tb(sK12))) ),
inference(forward_demodulation,[],[f1501,f245]) ).
tff(f1527,plain,
$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)),$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK10)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK12)))) != $sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK10)),$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK12)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)))),
inference(backward_demodulation,[],[f1008,f1520]) ).
tff(f1529,plain,
$sum($sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK10)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK12))),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11))) != $sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK10)),$sum(num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK12)),num_occ1(elt,sK26(elt,infix_plpl(elt,t2tb(sK11),cons(elt,cons_proj_11(elt,t2tb(sK12)),infix_plpl(elt,t2tb(sK10),cons_proj_21(elt,t2tb(sK12))))),infix_plpl(elt,t2tb(sK7),t2tb(sK9))),t2tb(sK11)))),
inference(forward_demodulation,[],[f1527,f78]) ).
tff(f1532,plain,
$false,
inference(forward_subsumption_resolution,[],[f1529,f79]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW628_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.26 % Computer : n003.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 14:24:57 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.32 Running first-order theorem proving
% 0.26/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.07/1.54 % (1622481)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.07/1.54 % (1622492)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2138228102:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.07/1.54 % (1622492)Instruction limit reached!
% 5.07/1.54 % (1622492)------------------------------
% 5.07/1.54 % (1622492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.07/1.54 % (1622492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.07/1.54 % (1622492)CaDiCaL version: 2.1.3
% 5.07/1.54 % (1622492)Termination reason: Instruction limit
% 5.07/1.54 % (1622492)Termination phase: Property scanning
% 5.07/1.54 % (1622492)Time elapsed: 0.002 s
% 5.07/1.54 % (1622492)Peak memory usage: 87 MB
% 5.07/1.54 % (1622492)Instructions burned: 7 (million)
% 5.07/1.54 % (1622488)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2621948267:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.07/1.54 % (1622491)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3657996081:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.07/1.54 % (1622494)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3302521696:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.07/1.54 % (1622489)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2867695778:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.07/1.54 % (1622490)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1383293002:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.07/1.54 % (1622493)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3111320656:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.07/1.54 % (1622491)Instruction limit reached!
% 5.07/1.54 % (1622491)------------------------------
% 5.07/1.54 % (1622491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.07/1.54 % (1622491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.07/1.54 % (1622491)CaDiCaL version: 2.1.3
% 5.07/1.54 % (1622491)Termination reason: Instruction limit
% 5.07/1.54 % (1622491)Termination phase: Property scanning
% 5.07/1.54 % (1622491)Time elapsed: 0.007 s
% 5.07/1.54 % (1622491)Peak memory usage: 86 MB
% 5.07/1.54 % (1622491)Instructions burned: 7 (million)
% 5.07/1.54 % (1622488)Instruction limit reached!
% 5.07/1.54 % (1622488)------------------------------
% 5.07/1.54 % (1622488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.07/1.54 % (1622488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.07/1.54 % (1622488)CaDiCaL version: 2.1.3
% 5.07/1.54 % (1622488)Termination reason: Instruction limit
% 5.07/1.54 % (1622488)Termination phase: Saturation
% 5.07/1.54 % (1622488)Time elapsed: 0.040 s
% 5.07/1.54 % (1622488)Peak memory usage: 111 MB
% 5.07/1.54 % (1622488)Instructions burned: 12 (million)
% 5.07/1.54 % (1622496)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2306364301:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.07/1.54 % (1622494)Instruction limit reached!
% 5.07/1.54 % (1622494)------------------------------
% 5.07/1.54 % (1622494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.07/1.54 % (1622494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.07/1.54 % (1622494)CaDiCaL version: 2.1.3
% 5.07/1.54 % (1622494)Termination reason: Instruction limit
% 5.07/1.54 % (1622494)Termination phase: Saturation
% 5.07/1.54 % (1622494)Time elapsed: 0.049 s
% 5.07/1.54 % (1622494)Peak memory usage: 116 MB
% 5.07/1.54 % (1622494)Instructions burned: 34 (million)
% 5.07/1.54 % (1622496)Instruction limit reached!
% 5.07/1.54 % (1622496)------------------------------
% 5.07/1.54 % (1622496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.07/1.54 % (1622496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.07/1.54 % (1622496)CaDiCaL version: 2.1.3
% 5.07/1.54 % (1622496)Termination reason: Instruction limit
% 5.07/1.54 % (1622496)Termination phase: Saturation
% 5.07/1.54 % (1622496)Time elapsed: 0.009 s
% 5.07/1.54 % (1622496)Peak memory usage: 88 MB
% 5.07/1.54 % (1622496)Instructions burned: 14 (million)
% 5.07/1.54 % (1622493)Instruction limit reached!
% 5.07/1.54 % (1622493)------------------------------
% 6.59/1.80 % (1622493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622493)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622493)Termination reason: Instruction limit
% 6.59/1.80 % (1622493)Termination phase: Saturation
% 6.59/1.80 % (1622493)Time elapsed: 0.078 s
% 6.59/1.80 % (1622493)Peak memory usage: 116 MB
% 6.59/1.80 % (1622493)Instructions burned: 46 (million)
% 6.59/1.80 % (1622490)Instruction limit reached!
% 6.59/1.80 % (1622490)------------------------------
% 6.59/1.80 % (1622490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622490)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622490)Termination reason: Instruction limit
% 6.59/1.80 % (1622490)Termination phase: Saturation
% 6.59/1.80 % (1622490)Time elapsed: 0.214 s
% 6.59/1.80 % (1622490)Peak memory usage: 116 MB
% 6.59/1.80 % (1622490)Instructions burned: 201 (million)
% 6.59/1.80 % (1622506)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1890948646:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.59/1.80 % (1622506)Instruction limit reached!
% 6.59/1.80 % (1622506)------------------------------
% 6.59/1.80 % (1622506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622506)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622506)Termination reason: Instruction limit
% 6.59/1.80 % (1622506)Termination phase: Saturation
% 6.59/1.80 % (1622506)Time elapsed: 0.017 s
% 6.59/1.80 % (1622506)Peak memory usage: 89 MB
% 6.59/1.80 % (1622506)Instructions burned: 25 (million)
% 6.59/1.80 % (1622507)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=1338809531:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.59/1.80 % (1622505)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1078526858:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 6.59/1.80 % (1622503)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=3060496069:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.59/1.80 % (1622505)Instruction limit reached!
% 6.59/1.80 % (1622505)------------------------------
% 6.59/1.80 % (1622505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622505)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622505)Termination reason: Instruction limit
% 6.59/1.80 % (1622505)Termination phase: Saturation
% 6.59/1.80 % (1622505)Time elapsed: 0.017 s
% 6.59/1.80 % (1622505)Peak memory usage: 88 MB
% 6.59/1.80 % (1622505)Instructions burned: 16 (million)
% 6.59/1.80 % (1622507)Instruction limit reached!
% 6.59/1.80 % (1622507)------------------------------
% 6.59/1.80 % (1622507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622507)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622507)Termination reason: Instruction limit
% 6.59/1.80 % (1622507)Termination phase: Saturation
% 6.59/1.80 % (1622507)Time elapsed: 0.030 s
% 6.59/1.80 % (1622507)Peak memory usage: 89 MB
% 6.59/1.80 % (1622507)Instructions burned: 27 (million)
% 6.59/1.80 % (1622503)Instruction limit reached!
% 6.59/1.80 % (1622503)------------------------------
% 6.59/1.80 % (1622503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.59/1.80 % (1622503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.59/1.80 % (1622503)CaDiCaL version: 2.1.3
% 6.59/1.80 % (1622503)Termination reason: Instruction limit
% 6.59/1.80 % (1622503)Termination phase: Saturation
% 6.59/1.80 % (1622503)Time elapsed: 0.034 s
% 6.59/1.80 % (1622503)Peak memory usage: 88 MB
% 6.59/1.80 % (1622503)Instructions burned: 29 (million)
% 6.59/1.80 % (1622508)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=389868399:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.59/1.80 % (1622489)Instruction limit reached!
% 6.59/1.80 % (1622489)------------------------------
% 6.59/1.80 % (1622489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622489)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622489)Termination reason: Instruction limit
% 8.06/2.01 % (1622489)Termination phase: Saturation
% 8.06/2.01 % (1622489)Time elapsed: 0.336 s
% 8.06/2.01 % (1622489)Peak memory usage: 117 MB
% 8.06/2.01 % (1622489)Instructions burned: 307 (million)
% 8.06/2.01 % (1622508)Instruction limit reached!
% 8.06/2.01 % (1622508)------------------------------
% 8.06/2.01 % (1622508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622508)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622508)Termination reason: Instruction limit
% 8.06/2.01 % (1622508)Termination phase: Saturation
% 8.06/2.01 % (1622508)Time elapsed: 0.077 s
% 8.06/2.01 % (1622508)Peak memory usage: 89 MB
% 8.06/2.01 % (1622508)Instructions burned: 85 (million)
% 8.06/2.01 % (1622518)lrs+10_1_thi=all:si=on:fd=off:random_seed=2186235108:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 8.06/2.01 % (1622509)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=593443618:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 8.06/2.01 % (1622511)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=634751451:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 8.06/2.01 % (1622509)Instruction limit reached!
% 8.06/2.01 % (1622509)------------------------------
% 8.06/2.01 % (1622509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622509)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622509)Termination reason: Instruction limit
% 8.06/2.01 % (1622509)Termination phase: Preprocessing 1
% 8.06/2.01 % (1622509)Time elapsed: 0.003 s
% 8.06/2.01 % (1622509)Peak memory usage: 85 MB
% 8.06/2.01 % (1622509)Instructions burned: 2 (million)
% 8.06/2.01 % (1622518)Instruction limit reached!
% 8.06/2.01 % (1622518)------------------------------
% 8.06/2.01 % (1622518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622518)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622518)Termination reason: Instruction limit
% 8.06/2.01 % (1622518)Termination phase: Saturation
% 8.06/2.01 % (1622518)Time elapsed: 0.037 s
% 8.06/2.01 % (1622518)Peak memory usage: 116 MB
% 8.06/2.01 % (1622518)Instructions burned: 54 (million)
% 8.06/2.01 % (1622515)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=887937855:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 8.06/2.01 % (1622515)Instruction limit reached!
% 8.06/2.01 % (1622515)------------------------------
% 8.06/2.01 % (1622515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622515)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622515)Termination reason: Instruction limit
% 8.06/2.01 % (1622515)Termination phase: Property scanning
% 8.06/2.01 % (1622515)Time elapsed: 0.005 s
% 8.06/2.01 % (1622515)Peak memory usage: 86 MB
% 8.06/2.01 % (1622515)Instructions burned: 5 (million)
% 8.06/2.01 % (1622520)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=1190206660:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 8.06/2.01 % (1622520)Instruction limit reached!
% 8.06/2.01 % (1622520)------------------------------
% 8.06/2.01 % (1622520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.01 % (1622520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.01 % (1622520)CaDiCaL version: 2.1.3
% 8.06/2.01 % (1622520)Termination reason: Instruction limit
% 8.06/2.01 % (1622520)Termination phase: Property scanning
% 8.06/2.01 % (1622520)Time elapsed: 0.005 s
% 8.06/2.01 % (1622520)Peak memory usage: 87 MB
% 8.06/2.01 % (1622520)Instructions burned: 8 (million)
% 8.06/2.01 % (1622516)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3361747746:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 11.46/2.42 % (1622521)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3924481696:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 11.46/2.42 % (1622521)Instruction limit reached!
% 11.46/2.42 % (1622521)------------------------------
% 11.46/2.42 % (1622521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622521)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622521)Termination reason: Instruction limit
% 11.46/2.42 % (1622521)Termination phase: Preprocessing 3
% 11.46/2.42 % (1622521)Time elapsed: 0.003 s
% 11.46/2.42 % (1622521)Peak memory usage: 86 MB
% 11.46/2.42 % (1622521)Instructions burned: 2 (million)
% 11.46/2.42 % (1622526)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4112467161:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.46/2.42 % (1622511)Instruction limit reached!
% 11.46/2.42 % (1622511)------------------------------
% 11.46/2.42 % (1622511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622511)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622511)Termination reason: Instruction limit
% 11.46/2.42 % (1622511)Termination phase: Saturation
% 11.46/2.42 % (1622511)Time elapsed: 0.200 s
% 11.46/2.42 % (1622511)Peak memory usage: 92 MB
% 11.46/2.42 % (1622511)Instructions burned: 181 (million)
% 11.46/2.42 % (1622516)Instruction limit reached!
% 11.46/2.42 % (1622516)------------------------------
% 11.46/2.42 % (1622516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622516)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622516)Termination reason: Instruction limit
% 11.46/2.42 % (1622516)Termination phase: Saturation
% 11.46/2.42 % (1622516)Time elapsed: 0.123 s
% 11.46/2.42 % (1622516)Peak memory usage: 133 MB
% 11.46/2.42 % (1622516)Instructions burned: 67 (million)
% 11.46/2.42 % (1622525)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4132239290:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 11.46/2.42 % (1622525)Instruction limit reached!
% 11.46/2.42 % (1622525)------------------------------
% 11.46/2.42 % (1622525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622525)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622525)Termination reason: Instruction limit
% 11.46/2.42 % (1622525)Termination phase: shuffling
% 11.46/2.42 % (1622525)Time elapsed: 0.003 s
% 11.46/2.42 % (1622525)Peak memory usage: 86 MB
% 11.46/2.42 % (1622525)Instructions burned: 2 (million)
% 11.46/2.42 % (1622526)Instruction limit reached!
% 11.46/2.42 % (1622526)------------------------------
% 11.46/2.42 % (1622526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622526)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622526)Termination reason: Instruction limit
% 11.46/2.42 % (1622526)Termination phase: Saturation
% 11.46/2.42 % (1622526)Time elapsed: 0.089 s
% 11.46/2.42 % (1622526)Peak memory usage: 117 MB
% 11.46/2.42 % (1622526)Instructions burned: 128 (million)
% 11.46/2.42 % (1622531)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=647656664:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.46/2.42 % (1622531)Instruction limit reached!
% 11.46/2.42 % (1622531)------------------------------
% 11.46/2.42 % (1622531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.42 % (1622531)CaDiCaL version: 2.1.3
% 11.46/2.42 % (1622531)Termination reason: Instruction limit
% 11.46/2.42 % (1622531)Termination phase: Saturation
% 11.46/2.42 % (1622531)Time elapsed: 0.029 s
% 11.46/2.42 % (1622531)Peak memory usage: 89 MB
% 11.46/2.42 % (1622531)Instructions burned: 26 (million)
% 11.46/2.42 % (1622530)dis+10_1_si=on:random_seed=1904521333:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.46/2.42 % (1622530)Instruction limit reached!
% 11.46/2.42 % (1622530)------------------------------
% 11.46/2.42 % (1622530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/2.42 % (1622530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622530)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622530)Termination reason: Instruction limit
% 13.15/2.89 % (1622530)Termination phase: Saturation
% 13.15/2.89 % (1622530)Time elapsed: 0.012 s
% 13.15/2.89 % (1622530)Peak memory usage: 88 MB
% 13.15/2.89 % (1622530)Instructions burned: 10 (million)
% 13.15/2.89 % (1622534)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1142981263: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_2990 on theBenchmark for (2990ds/35Mi)
% 13.15/2.89 % (1622537)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=97425648:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 13.15/2.89 % (1622536)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3947576725:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 13.15/2.89 % (1622537)Instruction limit reached!
% 13.15/2.89 % (1622537)------------------------------
% 13.15/2.89 % (1622537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.89 % (1622537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622537)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622537)Termination reason: Instruction limit
% 13.15/2.89 % (1622537)Termination phase: Saturation
% 13.15/2.89 % (1622537)Time elapsed: 0.006 s
% 13.15/2.89 % (1622537)Peak memory usage: 88 MB
% 13.15/2.89 % (1622537)Instructions burned: 9 (million)
% 13.15/2.89 % (1622536)Instruction limit reached!
% 13.15/2.89 % (1622536)------------------------------
% 13.15/2.89 % (1622536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.89 % (1622536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622536)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622536)Termination reason: Instruction limit
% 13.15/2.89 % (1622536)Termination phase: Unused predicate definition removal
% 13.15/2.89 % (1622536)Time elapsed: 0.003 s
% 13.15/2.89 % (1622536)Peak memory usage: 85 MB
% 13.15/2.89 % (1622536)Instructions burned: 2 (million)
% 13.15/2.89 % (1622534)Instruction limit reached!
% 13.15/2.89 % (1622534)------------------------------
% 13.15/2.89 % (1622534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.89 % (1622534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622534)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622534)Termination reason: Instruction limit
% 13.15/2.89 % (1622534)Termination phase: Saturation
% 13.15/2.89 % (1622534)Time elapsed: 0.041 s
% 13.15/2.89 % (1622534)Peak memory usage: 89 MB
% 13.15/2.89 % (1622534)Instructions burned: 35 (million)
% 13.15/2.89 % (1622541)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3973810339:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 13.15/2.89 % (1622541)Instruction limit reached!
% 13.15/2.89 % (1622541)------------------------------
% 13.15/2.89 % (1622541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.89 % (1622541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622541)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622541)Termination reason: Instruction limit
% 13.15/2.89 % (1622541)Termination phase: Saturation
% 13.15/2.89 % (1622541)Time elapsed: 0.024 s
% 13.15/2.89 % (1622541)Peak memory usage: 111 MB
% 13.15/2.89 % (1622541)Instructions burned: 13 (million)
% 13.15/2.89 % (1622539)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3489113157:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 13.15/2.89 % (1622544)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3756416869:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 13.15/2.89 % (1622544)Instruction limit reached!
% 13.15/2.89 % (1622544)------------------------------
% 13.15/2.89 % (1622544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.89 % (1622544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.89 % (1622544)CaDiCaL version: 2.1.3
% 13.15/2.89 % (1622544)Termination reason: Instruction limit
% 13.15/2.89 % (1622544)Termination phase: Saturation
% 13.15/2.89 % (1622544)Time elapsed: 0.008 s
% 13.15/2.89 % (1622544)Peak memory usage: 88 MB
% 13.15/2.89 % (1622544)Instructions burned: 11 (million)
% 13.15/2.89 % (1622542)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2200036077:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 18.27/3.32 % (1622549)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=529267504:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 18.27/3.32 % (1622548)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1337735146:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 18.27/3.32 % (1622549)Instruction limit reached!
% 18.27/3.32 % (1622549)------------------------------
% 18.27/3.32 % (1622549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.27/3.32 % (1622549)CaDiCaL version: 2.1.3
% 18.27/3.32 % (1622549)Termination reason: Instruction limit
% 18.27/3.32 % (1622549)Termination phase: Saturation
% 18.27/3.32 % (1622549)Time elapsed: 0.051 s
% 18.27/3.32 % (1622549)Peak memory usage: 90 MB
% 18.27/3.32 % (1622549)Instructions burned: 77 (million)
% 18.27/3.32 % (1622551)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=2867658892:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 18.27/3.32 % (1622552)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1606543453:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 18.27/3.32 % (1622548)Instruction limit reached!
% 18.27/3.32 % (1622548)------------------------------
% 18.27/3.32 % (1622548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.27/3.32 % (1622548)CaDiCaL version: 2.1.3
% 18.27/3.32 % (1622548)Termination reason: Instruction limit
% 18.27/3.32 % (1622548)Termination phase: Saturation
% 18.27/3.32 % (1622548)Time elapsed: 0.128 s
% 18.27/3.32 % (1622548)Peak memory usage: 133 MB
% 18.27/3.32 % (1622548)Instructions burned: 72 (million)
% 18.27/3.32 % (1622542)Instruction limit reached!
% 18.27/3.32 % (1622542)------------------------------
% 18.27/3.32 % (1622542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.27/3.32 % (1622542)CaDiCaL version: 2.1.3
% 18.27/3.32 % (1622542)Termination reason: Instruction limit
% 18.27/3.32 % (1622542)Termination phase: Saturation
% 18.27/3.32 % (1622542)Time elapsed: 0.250 s
% 18.27/3.32 % (1622542)Peak memory usage: 117 MB
% 18.27/3.32 % (1622542)Instructions burned: 227 (million)
% 18.27/3.32 % (1622556)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1009505826:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 18.27/3.32 % (1622559)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2121486284:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 18.27/3.32 % (1622539)Instruction limit reached!
% 18.27/3.32 % (1622539)------------------------------
% 18.27/3.32 % (1622539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.27/3.32 % (1622539)CaDiCaL version: 2.1.3
% 18.27/3.32 % (1622539)Termination reason: Instruction limit
% 18.27/3.32 % (1622539)Termination phase: Saturation
% 18.27/3.32 % (1622539)Time elapsed: 0.388 s
% 18.27/3.32 % (1622539)Peak memory usage: 94 MB
% 18.27/3.32 % (1622539)Instructions burned: 370 (million)
% 18.27/3.32 % (1622552)Instruction limit reached!
% 18.27/3.32 % (1622552)------------------------------
% 18.27/3.32 % (1622552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.27/3.32 % (1622552)CaDiCaL version: 2.1.3
% 18.27/3.32 % (1622552)Termination reason: Instruction limit
% 18.27/3.32 % (1622552)Termination phase: Saturation
% 18.27/3.32 % (1622552)Time elapsed: 0.159 s
% 18.27/3.32 % (1622552)Peak memory usage: 116 MB
% 18.27/3.32 % (1622552)Instructions burned: 130 (million)
% 18.27/3.32 % (1622559)Instruction limit reached!
% 18.27/3.32 % (1622559)------------------------------
% 18.27/3.32 % (1622559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.27/3.32 % (1622559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622559)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622559)Termination reason: Instruction limit
% 19.23/3.75 % (1622559)Termination phase: Saturation
% 19.23/3.75 % (1622559)Time elapsed: 0.087 s
% 19.23/3.75 % (1622559)Peak memory usage: 134 MB
% 19.23/3.75 % (1622559)Instructions burned: 40 (million)
% 19.23/3.75 % (1622562)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2336698705:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 19.23/3.75 % (1622556)Instruction limit reached!
% 19.23/3.75 % (1622556)------------------------------
% 19.23/3.75 % (1622556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.23/3.75 % (1622556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622556)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622556)Termination reason: Instruction limit
% 19.23/3.75 % (1622556)Termination phase: Saturation
% 19.23/3.75 % (1622556)Time elapsed: 0.197 s
% 19.23/3.75 % (1622556)Peak memory usage: 134 MB
% 19.23/3.75 % (1622556)Instructions burned: 131 (million)
% 19.23/3.75 % (1622551)Instruction limit reached!
% 19.23/3.75 % (1622551)------------------------------
% 19.23/3.75 % (1622551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.23/3.75 % (1622551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622551)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622551)Termination reason: Instruction limit
% 19.23/3.75 % (1622551)Termination phase: Saturation
% 19.23/3.75 % (1622551)Time elapsed: 0.311 s
% 19.23/3.75 % (1622551)Peak memory usage: 92 MB
% 19.23/3.75 % (1622551)Instructions burned: 294 (million)
% 19.23/3.75 % (1622563)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4252559568:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 19.23/3.75 % (1622562)Instruction limit reached!
% 19.23/3.75 % (1622562)------------------------------
% 19.23/3.75 % (1622562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.23/3.75 % (1622562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622562)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622562)Termination reason: Instruction limit
% 19.23/3.75 % (1622562)Termination phase: Saturation
% 19.23/3.75 % (1622562)Time elapsed: 0.151 s
% 19.23/3.75 % (1622562)Peak memory usage: 92 MB
% 19.23/3.75 % (1622562)Instructions burned: 308 (million)
% 19.23/3.75 % (1622566)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4149499759:i=131:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/131Mi)
% 19.23/3.75 % (1622567)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=1929975024:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 19.23/3.75 % (1622568)dis+10_1_si=on:random_seed=1433345077:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 19.23/3.75 % (1622570)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3962984136:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 19.23/3.75 % (1622571)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1058514939:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 19.23/3.75 % (1622566)Instruction limit reached!
% 19.23/3.75 % (1622566)------------------------------
% 19.23/3.75 % (1622566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.23/3.75 % (1622566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622566)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622566)Termination reason: Instruction limit
% 19.23/3.75 % (1622566)Termination phase: Saturation
% 19.23/3.75 % (1622566)Time elapsed: 0.163 s
% 19.23/3.75 % (1622566)Peak memory usage: 117 MB
% 19.23/3.75 % (1622566)Instructions burned: 132 (million)
% 19.23/3.75 % (1622574)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3570283669:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 19.23/3.75 % (1622571)Instruction limit reached!
% 19.23/3.75 % (1622571)------------------------------
% 19.23/3.75 % (1622571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.23/3.75 % (1622571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.23/3.75 % (1622571)CaDiCaL version: 2.1.3
% 19.23/3.75 % (1622571)Termination reason: Instruction limit
% 25.16/4.35 % (1622571)Termination phase: Saturation
% 25.16/4.35 % (1622571)Time elapsed: 0.144 s
% 25.16/4.35 % (1622571)Peak memory usage: 91 MB
% 25.16/4.35 % (1622571)Instructions burned: 141 (million)
% 25.16/4.35 % (1622567)Instruction limit reached!
% 25.16/4.35 % (1622567)------------------------------
% 25.16/4.35 % (1622567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622567)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622567)Termination reason: Instruction limit
% 25.16/4.35 % (1622567)Termination phase: Saturation
% 25.16/4.35 % (1622567)Time elapsed: 0.281 s
% 25.16/4.35 % (1622567)Peak memory usage: 117 MB
% 25.16/4.35 % (1622567)Instructions burned: 260 (million)
% 25.16/4.35 % (1622574)Instruction limit reached!
% 25.16/4.35 % (1622574)------------------------------
% 25.16/4.35 % (1622574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622574)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622574)Termination reason: Instruction limit
% 25.16/4.35 % (1622574)Termination phase: Saturation
% 25.16/4.35 % (1622574)Time elapsed: 0.088 s
% 25.16/4.35 % (1622574)Peak memory usage: 116 MB
% 25.16/4.35 % (1622574)Instructions burned: 65 (million)
% 25.16/4.35 % (1622579)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4109049007:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 25.16/4.35 % (1622570)Instruction limit reached!
% 25.16/4.35 % (1622570)------------------------------
% 25.16/4.35 % (1622570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622570)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622570)Termination reason: Instruction limit
% 25.16/4.35 % (1622570)Termination phase: Saturation
% 25.16/4.35 % (1622570)Time elapsed: 0.396 s
% 25.16/4.35 % (1622570)Peak memory usage: 94 MB
% 25.16/4.35 % (1622570)Instructions burned: 383 (million)
% 25.16/4.35 % (1622582)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=4115350403:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 25.16/4.35 % (1622581)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=1276489315:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 25.16/4.35 % (1622583)dis+1010_1_to=kbo:si=on:random_seed=3747122572:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 25.16/4.35 % (1622563)Instruction limit reached!
% 25.16/4.35 % (1622563)------------------------------
% 25.16/4.35 % (1622563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622563)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622563)Termination reason: Instruction limit
% 25.16/4.35 % (1622563)Termination phase: Saturation
% 25.16/4.35 % (1622563)Time elapsed: 0.648 s
% 25.16/4.35 % (1622563)Peak memory usage: 137 MB
% 25.16/4.35 % (1622563)Instructions burned: 599 (million)
% 25.16/4.35 % (1622582)Instruction limit reached!
% 25.16/4.35 % (1622582)------------------------------
% 25.16/4.35 % (1622582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622582)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622582)Termination reason: Instruction limit
% 25.16/4.35 % (1622582)Termination phase: Saturation
% 25.16/4.35 % (1622582)Time elapsed: 0.038 s
% 25.16/4.35 % (1622582)Peak memory usage: 116 MB
% 25.16/4.35 % (1622582)Instructions burned: 40 (million)
% 25.16/4.35 % (1622579)Instruction limit reached!
% 25.16/4.35 % (1622579)------------------------------
% 25.16/4.35 % (1622579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.16/4.35 % (1622579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.16/4.35 % (1622579)CaDiCaL version: 2.1.3
% 25.16/4.35 % (1622579)Termination reason: Instruction limit
% 25.16/4.35 % (1622579)Termination phase: Saturation
% 25.16/4.35 % (1622579)Time elapsed: 0.128 s
% 25.16/4.35 % (1622579)Peak memory usage: 90 MB
% 25.16/4.35 % (1622579)Instructions burned: 121 (million)
% 25.16/4.35 % (1622581)Instruction limit reached!
% 25.16/4.35 % (1622581)------------------------------
% 25.16/4.35 % (1622581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622581)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622581)Termination reason: Instruction limit
% 26.35/4.71 % (1622581)Termination phase: Saturation
% 26.35/4.71 % (1622581)Time elapsed: 0.164 s
% 26.35/4.71 % (1622581)Peak memory usage: 119 MB
% 26.35/4.71 % (1622581)Instructions burned: 128 (million)
% 26.35/4.71 % (1622583)Instruction limit reached!
% 26.35/4.71 % (1622583)------------------------------
% 26.35/4.71 % (1622583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622583)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622583)Termination reason: Instruction limit
% 26.35/4.71 % (1622583)Termination phase: Saturation
% 26.35/4.71 % (1622583)Time elapsed: 0.190 s
% 26.35/4.71 % (1622583)Peak memory usage: 91 MB
% 26.35/4.71 % (1622583)Instructions burned: 175 (million)
% 26.35/4.71 % (1622591)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3298931033:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 26.35/4.71 % (1622589)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2849851132:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/329Mi)
% 26.35/4.71 % (1622594)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4016806505:i=349:rtra=on_2974 on theBenchmark for (2974ds/349Mi)
% 26.35/4.71 % (1622593)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2889760958:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 26.35/4.71 % (1622597)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=726550113:st=2:i=295:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/295Mi)
% 26.35/4.71 % (1622591)Instruction limit reached!
% 26.35/4.71 % (1622591)------------------------------
% 26.35/4.71 % (1622591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622591)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622591)Termination reason: Instruction limit
% 26.35/4.71 % (1622591)Termination phase: Saturation
% 26.35/4.71 % (1622591)Time elapsed: 0.205 s
% 26.35/4.71 % (1622591)Peak memory usage: 133 MB
% 26.35/4.71 % (1622591)Instructions burned: 484 (million)
% 26.35/4.71 % (1622598)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=895781975:i=328:kws=inv_frequency:nm=20:rtra=on_2973 on theBenchmark for (2973ds/328Mi)
% 26.35/4.71 % (1622568)Instruction limit reached!
% 26.35/4.71 % (1622568)------------------------------
% 26.35/4.71 % (1622568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622568)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622568)Termination reason: Instruction limit
% 26.35/4.71 % (1622568)Termination phase: Saturation
% 26.35/4.71 % (1622568)Time elapsed: 0.989 s
% 26.35/4.71 % (1622568)Peak memory usage: 95 MB
% 26.35/4.71 % (1622568)Instructions burned: 1000 (million)
% 26.35/4.71 % (1622593)Instruction limit reached!
% 26.35/4.71 % (1622593)------------------------------
% 26.35/4.71 % (1622593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622593)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622593)Termination reason: Instruction limit
% 26.35/4.71 % (1622593)Termination phase: Saturation
% 26.35/4.71 % (1622593)Time elapsed: 0.254 s
% 26.35/4.71 % (1622593)Peak memory usage: 135 MB
% 26.35/4.71 % (1622593)Instructions burned: 216 (million)
% 26.35/4.71 % (1622589)Instruction limit reached!
% 26.35/4.71 % (1622589)------------------------------
% 26.35/4.71 % (1622589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.71 % (1622589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.71 % (1622589)CaDiCaL version: 2.1.3
% 26.35/4.71 % (1622589)Termination reason: Instruction limit
% 26.35/4.71 % (1622589)Termination phase: Saturation
% 26.35/4.71 % (1622589)Time elapsed: 0.343 s
% 26.35/4.71 % (1622589)Peak memory usage: 117 MB
% 26.35/4.71 % (1622589)Instructions burned: 330 (million)
% 31.08/5.14 % (1622605)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1379827199:i=281:gtgl=2:rtra=on:gtg=all_2970 on theBenchmark for (2970ds/281Mi)
% 31.08/5.14 % (1622594)Instruction limit reached!
% 31.08/5.14 % (1622594)------------------------------
% 31.08/5.14 % (1622594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.14 % (1622594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.14 % (1622594)CaDiCaL version: 2.1.3
% 31.08/5.14 % (1622594)Termination reason: Instruction limit
% 31.08/5.14 % (1622594)Termination phase: Saturation
% 31.08/5.14 % (1622594)Time elapsed: 0.401 s
% 31.08/5.14 % (1622594)Peak memory usage: 119 MB
% 31.08/5.14 % (1622594)Instructions burned: 350 (million)
% 31.08/5.14 % (1622597)Instruction limit reached!
% 31.08/5.14 % (1622597)------------------------------
% 31.08/5.14 % (1622597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.14 % (1622597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.14 % (1622597)CaDiCaL version: 2.1.3
% 31.08/5.14 % (1622597)Termination reason: Instruction limit
% 31.08/5.14 % (1622597)Termination phase: Saturation
% 31.08/5.14 % (1622597)Time elapsed: 0.281 s
% 31.08/5.14 % (1622597)Peak memory usage: 91 MB
% 31.08/5.14 % (1622597)Instructions burned: 296 (million)
% 31.08/5.14 % (1622607)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2079125404:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi)
% 31.08/5.14 % (1622608)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2852911366:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi)
% 31.08/5.14 % (1622598)Instruction limit reached!
% 31.08/5.14 % (1622598)------------------------------
% 31.08/5.14 % (1622598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.14 % (1622598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.14 % (1622598)CaDiCaL version: 2.1.3
% 31.08/5.14 % (1622598)Termination reason: Instruction limit
% 31.08/5.14 % (1622598)Termination phase: Saturation
% 31.08/5.14 % (1622598)Time elapsed: 0.348 s
% 31.08/5.14 % (1622598)Peak memory usage: 118 MB
% 31.08/5.14 % (1622598)Instructions burned: 328 (million)
% 31.08/5.14 % (1622605)Instruction limit reached!
% 31.08/5.14 % (1622605)------------------------------
% 31.08/5.14 % (1622605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.14 % (1622605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.14 % (1622605)CaDiCaL version: 2.1.3
% 31.08/5.14 % (1622605)Termination reason: Instruction limit
% 31.08/5.14 % (1622605)Termination phase: Saturation
% 31.08/5.14 % (1622605)Time elapsed: 0.172 s
% 31.08/5.14 % (1622605)Peak memory usage: 118 MB
% 31.08/5.14 % (1622605)Instructions burned: 281 (million)
% 31.08/5.14 % (1622609)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1745935087:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 31.08/5.14 % (1622611)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=4028605683:i=471:thf=on:kws=precedence:rtra=on_2968 on theBenchmark for (2968ds/471Mi)
% 31.08/5.14 % (1622612)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=3264320760:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 31.08/5.14 % (1622615)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=1277876118:i=375:kws=inv_arity_squared:rtra=on_2966 on theBenchmark for (2966ds/375Mi)
% 31.08/5.14 % (1622616)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1934192503:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/387Mi)
% 31.08/5.14 % (1622608)Instruction limit reached!
% 31.08/5.14 % (1622608)------------------------------
% 31.08/5.14 % (1622608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.14 % (1622608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.14 % (1622608)CaDiCaL version: 2.1.3
% 31.08/5.14 % (1622608)Termination reason: Instruction limit
% 31.08/5.14 % (1622608)Termination phase: Saturation
% 31.08/5.14 % (1622608)Time elapsed: 0.367 s
% 31.08/5.14 % (1622608)Peak memory usage: 118 MB
% 31.08/5.14 % (1622608)Instructions burned: 322 (million)
% 33.34/5.71 % (1622612)Instruction limit reached!
% 33.34/5.71 % (1622612)------------------------------
% 33.34/5.71 % (1622612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.71 % (1622612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.71 % (1622612)CaDiCaL version: 2.1.3
% 33.34/5.71 % (1622612)Termination reason: Instruction limit
% 33.34/5.71 % (1622612)Termination phase: Saturation
% 33.34/5.71 % (1622612)Time elapsed: 0.253 s
% 33.34/5.71 % (1622612)Peak memory usage: 133 MB
% 33.34/5.71 % (1622612)Instructions burned: 276 (million)
% 33.34/5.71 % (1622607)Instruction limit reached!
% 33.34/5.71 % (1622607)------------------------------
% 33.34/5.71 % (1622607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.71 % (1622607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.71 % (1622607)CaDiCaL version: 2.1.3
% 33.34/5.71 % (1622607)Termination reason: Instruction limit
% 33.34/5.71 % (1622607)Termination phase: Saturation
% 33.34/5.71 % (1622607)Time elapsed: 0.470 s
% 33.34/5.71 % (1622607)Peak memory usage: 95 MB
% 33.34/5.72 % (1622607)Instructions burned: 484 (million)
% 33.34/5.72 % (1622615)Instruction limit reached!
% 33.34/5.72 % (1622615)------------------------------
% 33.34/5.72 % (1622615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.72 % (1622615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.72 % (1622615)CaDiCaL version: 2.1.3
% 33.34/5.72 % (1622615)Termination reason: Instruction limit
% 33.34/5.72 % (1622615)Termination phase: Saturation
% 33.34/5.72 % (1622615)Time elapsed: 0.211 s
% 33.34/5.72 % (1622615)Peak memory usage: 118 MB
% 33.34/5.72 % (1622615)Instructions burned: 377 (million)
% 33.34/5.72 % (1622609)Instruction limit reached!
% 33.34/5.72 % (1622609)------------------------------
% 33.34/5.72 % (1622609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.72 % (1622609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.72 % (1622609)CaDiCaL version: 2.1.3
% 33.34/5.72 % (1622609)Termination reason: Instruction limit
% 33.34/5.72 % (1622609)Termination phase: Saturation
% 33.34/5.72 % (1622609)Time elapsed: 0.413 s
% 33.34/5.72 % (1622609)Peak memory usage: 118 MB
% 33.34/5.72 % (1622609)Instructions burned: 417 (million)
% 33.34/5.72 % (1622611)Instruction limit reached!
% 33.34/5.72 % (1622611)------------------------------
% 33.34/5.72 % (1622611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.72 % (1622611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.72 % (1622611)CaDiCaL version: 2.1.3
% 33.34/5.72 % (1622611)Termination reason: Instruction limit
% 33.34/5.72 % (1622611)Termination phase: Saturation
% 33.34/5.72 % (1622611)Time elapsed: 0.482 s
% 33.34/5.72 % (1622611)Peak memory usage: 119 MB
% 33.34/5.72 % (1622611)Instructions burned: 471 (million)
% 33.34/5.72 % (1622625)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=26549228:i=334:rtra=on_2962 on theBenchmark for (2962ds/334Mi)
% 33.34/5.72 % (1622624)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1439661065:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2963 on theBenchmark for (2963ds/513Mi)
% 33.34/5.72 % (1622627)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2884981393:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2962 on theBenchmark for (2962ds/341Mi)
% 33.34/5.72 % (1622626)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3548385299:i=359:rtra=on:gtg=exists_top:ss=axioms_2962 on theBenchmark for (2962ds/359Mi)
% 33.34/5.72 % (1622628)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=3358548139:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2962 on theBenchmark for (2962ds/261Mi)
% 33.34/5.72 % (1622616)Instruction limit reached!
% 33.34/5.72 % (1622616)------------------------------
% 33.34/5.72 % (1622616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/5.72 % (1622616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/5.72 % (1622616)CaDiCaL version: 2.1.3
% 33.34/5.72 % (1622616)Termination reason: Instruction limit
% 33.34/5.72 % (1622616)Termination phase: Saturation
% 33.34/5.72 % (1622616)Time elapsed: 0.431 s
% 33.34/5.72 % (1622616)Peak memory usage: 118 MB
% 33.34/5.72 % (1622616)Instructions burned: 387 (million)
% 39.68/6.45 % (1622629)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=804189195:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2961 on theBenchmark for (2961ds/235Mi)
% 39.68/6.45 % (1622627)Instruction limit reached!
% 39.68/6.45 % (1622627)------------------------------
% 39.68/6.45 % (1622627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622627)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622627)Termination reason: Instruction limit
% 39.68/6.45 % (1622627)Termination phase: Saturation
% 39.68/6.45 % (1622627)Time elapsed: 0.206 s
% 39.68/6.45 % (1622627)Peak memory usage: 119 MB
% 39.68/6.45 % (1622627)Instructions burned: 342 (million)
% 39.68/6.45 % (1622625)Instruction limit reached!
% 39.68/6.45 % (1622625)------------------------------
% 39.68/6.45 % (1622625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622625)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622625)Termination reason: Instruction limit
% 39.68/6.45 % (1622625)Termination phase: Saturation
% 39.68/6.45 % (1622635)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=965824726:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi)
% 39.68/6.45 % (1622625)Time elapsed: 0.327 s
% 39.68/6.45 % (1622625)Peak memory usage: 135 MB
% 39.68/6.45 % (1622625)Instructions burned: 335 (million)
% 39.68/6.45 % (1622628)Instruction limit reached!
% 39.68/6.45 % (1622628)------------------------------
% 39.68/6.45 % (1622628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622628)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622628)Termination reason: Instruction limit
% 39.68/6.45 % (1622628)Termination phase: Saturation
% 39.68/6.45 % (1622628)Time elapsed: 0.266 s
% 39.68/6.45 % (1622628)Peak memory usage: 117 MB
% 39.68/6.45 % (1622628)Instructions burned: 262 (million)
% 39.68/6.45 % (1622626)Instruction limit reached!
% 39.68/6.45 % (1622626)------------------------------
% 39.68/6.45 % (1622626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622626)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622626)Termination reason: Instruction limit
% 39.68/6.45 % (1622626)Termination phase: Saturation
% 39.68/6.45 % (1622626)Time elapsed: 0.366 s
% 39.68/6.45 % (1622626)Peak memory usage: 92 MB
% 39.68/6.45 % (1622626)Instructions burned: 359 (million)
% 39.68/6.45 % (1622637)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2092060675:i=146:doe=on:rtra=on_2958 on theBenchmark for (2958ds/146Mi)
% 39.68/6.45 % (1622629)Instruction limit reached!
% 39.68/6.45 % (1622629)------------------------------
% 39.68/6.45 % (1622629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622629)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622629)Termination reason: Instruction limit
% 39.68/6.45 % (1622629)Termination phase: Saturation
% 39.68/6.45 % (1622629)Time elapsed: 0.262 s
% 39.68/6.45 % (1622629)Peak memory usage: 117 MB
% 39.68/6.45 % (1622629)Instructions burned: 236 (million)
% 39.68/6.45 % (1622624)Instruction limit reached!
% 39.68/6.45 % (1622624)------------------------------
% 39.68/6.45 % (1622624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622624)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622624)Termination reason: Instruction limit
% 39.68/6.45 % (1622624)Termination phase: Saturation
% 39.68/6.45 % (1622624)Time elapsed: 0.505 s
% 39.68/6.45 % (1622624)Peak memory usage: 93 MB
% 39.68/6.45 % (1622624)Instructions burned: 513 (million)
% 39.68/6.45 % (1622637)Instruction limit reached!
% 39.68/6.45 % (1622637)------------------------------
% 39.68/6.45 % (1622637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.68/6.45 % (1622637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.68/6.45 % (1622637)CaDiCaL version: 2.1.3
% 39.68/6.45 % (1622637)Termination reason: Instruction limit
% 40.63/6.80 % (1622637)Termination phase: Saturation
% 40.63/6.80 % (1622637)Time elapsed: 0.077 s
% 40.63/6.80 % (1622637)Peak memory usage: 90 MB
% 40.63/6.80 % (1622637)Instructions burned: 152 (million)
% 40.63/6.80 % (1622640)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1931877397:i=4428:doe=on:fsr=off:rtra=on_2957 on theBenchmark for (2957ds/4428Mi)
% 40.63/6.80 % (1622635)Instruction limit reached!
% 40.63/6.80 % (1622635)------------------------------
% 40.63/6.80 % (1622635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622635)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622635)Termination reason: Instruction limit
% 40.63/6.80 % (1622635)Termination phase: Saturation
% 40.63/6.80 % (1622635)Time elapsed: 0.304 s
% 40.63/6.80 % (1622635)Peak memory usage: 92 MB
% 40.63/6.80 % (1622635)Instructions burned: 273 (million)
% 40.63/6.80 % (1622641)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=3748385880:avsq=on:i=276:avsqr=1,2:rtra=on_2957 on theBenchmark for (2957ds/276Mi)
% 40.63/6.80 % (1622642)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=378012478:i=1052:rtra=on_2956 on theBenchmark for (2956ds/1052Mi)
% 40.63/6.80 % (1622647)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=850252388:i=107:rtra=on_2955 on theBenchmark for (2955ds/107Mi)
% 40.63/6.80 % (1622645)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1880745616:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/655Mi)
% 40.63/6.80 % (1622646)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3402333634:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1054Mi)
% 40.63/6.80 % (1622647)Instruction limit reached!
% 40.63/6.80 % (1622647)------------------------------
% 40.63/6.80 % (1622647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622647)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622647)Termination reason: Instruction limit
% 40.63/6.80 % (1622647)Termination phase: Saturation
% 40.63/6.80 % (1622647)Time elapsed: 0.077 s
% 40.63/6.80 % (1622647)Peak memory usage: 116 MB
% 40.63/6.80 % (1622647)Instructions burned: 107 (million)
% 40.63/6.80 % (1622650)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3502583836:s2a=on:i=450:doe=on:nm=32:rtra=on_2954 on theBenchmark for (2954ds/450Mi)
% 40.63/6.80 % (1622641)Instruction limit reached!
% 40.63/6.80 % (1622641)------------------------------
% 40.63/6.80 % (1622641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622641)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622641)Termination reason: Instruction limit
% 40.63/6.80 % (1622641)Termination phase: Saturation
% 40.63/6.80 % (1622641)Time elapsed: 0.346 s
% 40.63/6.80 % (1622641)Peak memory usage: 135 MB
% 40.63/6.80 % (1622641)Instructions burned: 276 (million)
% 40.63/6.80 % (1622650)Instruction limit reached!
% 40.63/6.80 % (1622650)------------------------------
% 40.63/6.80 % (1622650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622650)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622650)Termination reason: Instruction limit
% 40.63/6.80 % (1622650)Termination phase: Saturation
% 40.63/6.80 % (1622650)Time elapsed: 0.249 s
% 40.63/6.80 % (1622650)Peak memory usage: 133 MB
% 40.63/6.80 % (1622650)Instructions burned: 450 (million)
% 40.63/6.80 % (1622656)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
% 40.63/6.80 % (1622656)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=4251246287:i=1090:aac=none:nm=0:rtra=on:rawr=on_2953 on theBenchmark for (2953ds/1090Mi)
% 40.63/6.80 % (1622645)Instruction limit reached!
% 40.63/6.80 % (1622645)------------------------------
% 40.63/6.80 % (1622645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622645)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622645)Termination reason: Instruction limit
% 40.63/6.80 % (1622645)Termination phase: Saturation
% 40.63/6.80 % (1622645)Time elapsed: 0.397 s
% 40.63/6.80 % (1622645)Peak memory usage: 89 MB
% 40.63/6.80 % (1622645)Instructions burned: 655 (million)
% 40.63/6.80 % (1622659)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4286814561:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2951 on theBenchmark for (2951ds/130Mi)
% 40.63/6.80 % (1622660)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1873876280:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi)
% 40.63/6.80 % (1622662)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=1420569643:i=491:doe=on:rtra=on:gtg=position_2949 on theBenchmark for (2949ds/491Mi)
% 40.63/6.80 % (1622646)Instruction limit reached!
% 40.63/6.80 % (1622646)------------------------------
% 40.63/6.80 % (1622646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622646)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622646)Termination reason: Instruction limit
% 40.63/6.80 % (1622646)Termination phase: Saturation
% 40.63/6.80 % (1622646)Time elapsed: 0.616 s
% 40.63/6.80 % (1622646)Peak memory usage: 89 MB
% 40.63/6.80 % (1622646)Instructions burned: 1055 (million)
% 40.63/6.80 % (1622659)Instruction limit reached!
% 40.63/6.80 % (1622659)------------------------------
% 40.63/6.80 % (1622659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.80 % (1622659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.80 % (1622659)CaDiCaL version: 2.1.3
% 40.63/6.80 % (1622659)Termination reason: Instruction limit
% 40.63/6.80 % (1622659)Termination phase: Saturation
% 40.63/6.80 % (1622659)Time elapsed: 0.156 s
% 40.63/6.80 % (1622659)Peak memory usage: 116 MB
% 40.63/6.80 % (1622659)Instructions burned: 131 (million)
% 40.63/6.80 % (1622660)Instruction limit reached!
% 40.63/6.80 % (1622660)------------------------------
% 40.63/6.80 % (1622660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.81 % (1622660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.81 % (1622660)CaDiCaL version: 2.1.3
% 40.63/6.81 % (1622660)Termination reason: Instruction limit
% 40.63/6.81 % (1622660)Termination phase: Saturation
% 40.63/6.81 % (1622660)Time elapsed: 0.159 s
% 40.63/6.81 % (1622660)Peak memory usage: 118 MB
% 40.63/6.81 % (1622660)Instructions burned: 313 (million)
% 40.63/6.81 % (1622667)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=241753190:s2a=on:i=835:s2at=2:rtra=on_2947 on theBenchmark for (2947ds/835Mi)
% 40.63/6.81 % (1622670)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4266799951:i=776:doe=on:rtra=on_2946 on theBenchmark for (2946ds/776Mi)
% 40.63/6.81 % (1622669)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=2045764777:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2946 on theBenchmark for (2946ds/307Mi)
% 40.63/6.81 % (1622642)Instruction limit reached!
% 40.63/6.81 % (1622642)------------------------------
% 40.63/6.81 % (1622642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.81 % (1622642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.81 % (1622642)CaDiCaL version: 2.1.3
% 40.63/6.81 % (1622642)Termination reason: Instruction limit
% 40.63/6.81 % (1622642)Termination phase: Saturation
% 40.63/6.81 % (1622642)Time elapsed: 1.012 s
% 40.63/6.81 % (1622642)Peak memory usage: 97 MB
% 40.63/6.81 % (1622642)Instructions burned: 1052 (million)
% 40.63/6.81 % (1622669)First to succeed.
% 40.63/6.81 % (1622669)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1622481"
% 40.63/6.81 % (1622662)Instruction limit reached!
% 40.63/6.81 % (1622662)------------------------------
% 40.63/6.81 % (1622662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.81 % (1622662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.81 % (1622662)CaDiCaL version: 2.1.3
% 40.63/6.81 % (1622662)Termination reason: Instruction limit
% 40.63/6.81 % (1622662)Termination phase: Saturation
% 40.63/6.81 % (1622662)Time elapsed: 0.520 s
% 40.63/6.81 % (1622662)Peak memory usage: 94 MB
% 40.63/6.81 % (1622662)Instructions burned: 491 (million)
% 40.63/6.81 % (1622674)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=493234793:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2944 on theBenchmark for (2944ds/646Mi)
% 40.63/6.81 % (1622670)Instruction limit reached!
% 40.63/6.81 % (1622670)------------------------------
% 40.63/6.81 % (1622670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.81 % (1622670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.81 % (1622670)CaDiCaL version: 2.1.3
% 40.63/6.81 % (1622670)Termination reason: Instruction limit
% 40.63/6.81 % (1622670)Termination phase: Saturation
% 40.63/6.81 % (1622670)Time elapsed: 0.398 s
% 40.63/6.81 % (1622670)Peak memory usage: 122 MB
% 40.63/6.81 % (1622670)Instructions burned: 777 (million)
% 40.63/6.81 % (1622675)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=960433428:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2942 on theBenchmark for (2942ds/784Mi)
% 40.63/6.81 % (1622656)Instruction limit reached!
% 40.63/6.81 % (1622656)------------------------------
% 40.63/6.81 % (1622656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.63/6.81 % (1622656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.63/6.81 % (1622656)CaDiCaL version: 2.1.3
% 40.63/6.81 % (1622656)Termination reason: Instruction limit
% 40.63/6.81 % (1622656)Termination phase: Saturation
% 40.63/6.81 % (1622656)Time elapsed: 1.075 s
% 40.63/6.81 % (1622656)Peak memory usage: 122 MB
% 40.63/6.81 % (1622656)Instructions burned: 1090 (million)
% 40.63/6.81 % (1622669)Refutation found. Thanks to Tanya!
% 40.63/6.81 % SZS status Theorem for theBenchmark
% 40.63/6.81 % SZS output start Proof for theBenchmark
% See solution above
% 43.42/6.98 % (1622669)------------------------------
% 43.42/6.98 % (1622669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.42/6.98 % (1622669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.42/6.98 % (1622669)CaDiCaL version: 2.1.3
% 43.42/6.98 % (1622669)Termination reason: Refutation
% 43.42/6.98 % (1622669)Time elapsed: 0.122 s
% 43.42/6.98 % (1622669)Peak memory usage: 91 MB
% 43.42/6.98 % (1622669)Instructions burned: 111 (million)
% 43.42/6.98 % (1622669)------------------------------
% 43.42/6.98 % (1622669)------------------------------
% 43.42/6.98 % (1622481)Success in time 6.104 s
% 43.42/6.98 % Vampire exiting
%------------------------------------------------------------------------------