%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW628_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:40:33 PM UTC 2026
% Result : Theorem 17.46s 5.21s
% Output : Refutation 17.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 27
% Syntax : Number of formulae : 104 ( 87 unt; 0 typ; 19 def)
% Number of atoms : 314 ( 165 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 287 ( 77 ~; 26 |; 130 &)
% ( 0 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 34 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 28 ( 7 atm; 0 fun; 21 num; 0 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 : 87 ( 86 usr; 57 con; 0-5 aty)
% Number of variables : 208 ( 139 !; 69 ?; 208 :)
% 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: ( ty * uni * uni ) > uni ).
tff(func_def_35,type,
sK1: ( ty * uni * uni ) > uni ).
tff(func_def_36,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_37,type,
sK3: list_elt > elt1 ).
tff(func_def_38,type,
sK4: list_elt > elt1 ).
tff(func_def_39,type,
sK5: list_elt > elt1 ).
tff(func_def_40,type,
sK6: list_elt > list_elt ).
tff(func_def_41,type,
sK7: ( elt1 * list_elt ) > elt1 ).
tff(func_def_42,type,
sK8: ( list_elt * list_elt ) > elt1 ).
tff(func_def_43,type,
sK9: ( list_elt * list_elt ) > elt1 ).
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: list_elt ).
tff(func_def_48,type,
sK14: list_elt ).
tff(func_def_49,type,
sK15: list_elt ).
tff(func_def_50,type,
sK16: elt1 ).
tff(func_def_51,type,
sK17: elt1 ).
tff(func_def_52,type,
sK18: list_elt ).
tff(func_def_53,type,
sK19: elt1 ).
tff(func_def_54,type,
sK20: list_elt ).
tff(func_def_55,type,
sK21: elt1 ).
tff(func_def_56,type,
sK22: list_elt ).
tff(func_def_57,type,
sK23: elt1 ).
tff(func_def_58,type,
sK24: list_elt ).
tff(func_def_59,type,
sK25: elt1 ).
tff(func_def_60,type,
sK26: list_elt ).
tff(func_def_61,type,
sF27: uni ).
tff(func_def_62,type,
sF28: uni ).
tff(func_def_63,type,
sF29: uni ).
tff(func_def_64,type,
sF30: uni ).
tff(func_def_65,type,
sF31: uni ).
tff(func_def_66,type,
sF32: uni ).
tff(func_def_67,type,
sF33: uni ).
tff(func_def_68,type,
sF34: uni ).
tff(func_def_69,type,
sF35: uni ).
tff(func_def_70,type,
sF36: uni ).
tff(func_def_71,type,
sF37: uni ).
tff(func_def_72,type,
sF38: uni ).
tff(func_def_73,type,
sF39: uni ).
tff(func_def_74,type,
sF40: list_elt ).
tff(func_def_75,type,
sF41: uni ).
tff(func_def_76,type,
sF42: list_elt ).
tff(func_def_77,type,
sF43: list_elt ).
tff(func_def_78,type,
sF44: uni ).
tff(func_def_79,type,
sF45: uni ).
tff(func_def_80,type,
sF46: uni ).
tff(func_def_81,type,
sF47: list_elt ).
tff(func_def_82,type,
sF48: uni ).
tff(func_def_83,type,
sF49: uni ).
tff(func_def_84,type,
sF50: uni ).
tff(func_def_85,type,
sF51: list_elt ).
tff(func_def_86,type,
sF52: uni ).
tff(func_def_87,type,
sF53: $int ).
tff(func_def_88,type,
sF54: $int ).
tff(func_def_89,type,
sF55: uni ).
tff(func_def_90,type,
sF56: 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(f25,axiom,
! [X0: ty,X1: uni] :
( ( infix_plpl(X0,nil(X0),X1) = X1 )
& ! [X2: uni,X3: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f26,axiom,
! [X0: ty,X1: uni,X2: uni,X3: uni] : ( infix_plpl(X0,X1,infix_plpl(X0,X2,X3)) = infix_plpl(X0,infix_plpl(X0,X1,X2),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',append_assoc) ).
tff(f44,axiom,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X1,X2)
=> permut(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_sym) ).
tff(f45,axiom,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X2)
=> ( permut(X0,X2,X3)
=> permut(X0,X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_trans) ).
tff(f48,axiom,
! [X0: ty,X1: uni,X2: uni,X3: uni] : permut(X0,infix_plpl(X0,cons(X0,X1,X2),X3),infix_plpl(X0,X2,cons(X0,X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_cons_append) ).
tff(f51,axiom,
! [X0: ty,X1: uni,X2: uni] : permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',permut_append_swap) ).
tff(f64,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f74,conjecture,
! [X0: list_elt,X1: list_elt,X2: list_elt] :
( ( ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) )
=> ! [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X5))
=> le1(X6,X7) ) )
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X4))
=> le1(X6,X7) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
=> ( $less(0,length2(elt,t2tb(X5)))
=> ( ( length2(elt,t2tb(X5)) != 0 )
=> ( ( length2(elt,t2tb(X4)) != 0 )
=> ( ( X5 != tb2t(nil(elt)) )
=> ! [X8: elt1] :
( ? [X6: elt1,X9: list_elt] :
( ( X5 = tb2t(cons(elt,t2tb1(X6),t2tb(X9))) )
& ( X8 = X6 ) )
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X9: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) )
& ( X9 = X6 ) )
=> ( ~ 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))) )
& ( X12 = X6 )
& ( X11 = X10 ) )
=> ! [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/sandbox/benchmark/theBenchmark.p',wP_parameter_merge) ).
tff(f75,negated_conjecture,
~ ! [X0: list_elt,X1: list_elt,X2: list_elt] :
( ( ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) )
=> ! [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X5))
=> le1(X6,X7) ) )
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X4))
=> le1(X6,X7) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
=> ( $less(0,length2(elt,t2tb(X5)))
=> ( ( length2(elt,t2tb(X5)) != 0 )
=> ( ( length2(elt,t2tb(X4)) != 0 )
=> ( ( X5 != tb2t(nil(elt)) )
=> ! [X8: elt1] :
( ? [X6: elt1,X9: list_elt] :
( ( X5 = tb2t(cons(elt,t2tb1(X6),t2tb(X9))) )
& ( X8 = X6 ) )
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X9: elt1] :
( ? [X6: elt1,X10: list_elt] :
( ( X4 = tb2t(cons(elt,t2tb1(X6),t2tb(X10))) )
& ( X9 = X6 ) )
=> ( ~ 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))) )
& ( X12 = X6 )
& ( X11 = X10 ) )
=> ! [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(f98,plain,
~ ! [X0: list_elt,X1: list_elt,X2: list_elt] :
( ( ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) )
=> ! [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X6: elt1,X7: elt1] :
( mem(elt,t2tb1(X6),t2tb(X3))
=> ( mem(elt,t2tb1(X7),t2tb(X5))
=> le1(X6,X7) ) )
& ! [X8: elt1,X9: elt1] :
( mem(elt,t2tb1(X8),t2tb(X3))
=> ( mem(elt,t2tb1(X9),t2tb(X4))
=> le1(X8,X9) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
=> ( $less(0,length2(elt,t2tb(X5)))
=> ( ( length2(elt,t2tb(X5)) != 0 )
=> ( ( length2(elt,t2tb(X4)) != 0 )
=> ( ( X5 != tb2t(nil(elt)) )
=> ! [X10: elt1] :
( ? [X11: elt1,X12: list_elt] :
( ( tb2t(cons(elt,t2tb1(X11),t2tb(X12))) = X5 )
& ( X10 = X11 ) )
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X13: elt1] :
( ? [X14: elt1,X15: list_elt] :
( ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X4 )
& ( X13 = X14 ) )
=> ( ~ le1(X10,X13)
=> ( ( X4 != tb2t(nil(elt)) )
=> ! [X16: list_elt,X17: elt1] :
( ? [X18: elt1,X19: list_elt] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X4 )
& ( X17 = X18 )
& ( X16 = X19 ) )
=> ! [X20: list_elt] :
( ( tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X17),nil(elt)))) = X20 )
=> permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X5)),t2tb(X16)),infix_plpl(elt,t2tb(X0),t2tb(X1))) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f75]) ).
tff(f110,plain,
! [X0: ty,X1: uni,X2: uni] :
( permut(X0,X2,X1)
| ~ permut(X0,X1,X2) ),
inference(ennf_transformation,[],[f44]) ).
tff(f111,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X3)
| ~ permut(X0,X2,X3)
| ~ permut(X0,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
tff(f112,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( permut(X0,X1,X3)
| ~ permut(X0,X2,X3)
| ~ permut(X0,X1,X2) ),
inference(flattening,[],[f111]) ).
tff(f129,plain,
? [X0: list_elt,X1: list_elt,X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X10: elt1] :
( ? [X13: elt1] :
( ? [X16: list_elt,X17: elt1] :
( ? [X20: list_elt] :
( ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X5)),t2tb(X16)),infix_plpl(elt,t2tb(X0),t2tb(X1)))
& ( tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X17),nil(elt)))) = X20 ) )
& ? [X18: elt1,X19: list_elt] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X4 )
& ( X17 = X18 )
& ( X16 = X19 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ~ le1(X10,X13)
& ? [X14: elt1,X15: list_elt] :
( ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X4 )
& ( X13 = X14 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ? [X11: elt1,X12: list_elt] :
( ( tb2t(cons(elt,t2tb1(X11),t2tb(X12))) = X5 )
& ( X10 = X11 ) ) )
& ( X5 != tb2t(nil(elt)) )
& ( length2(elt,t2tb(X4)) != 0 )
& ( length2(elt,t2tb(X5)) != 0 )
& $less(0,length2(elt,t2tb(X5)))
& sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X6: elt1,X7: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X7),t2tb(X5))
| ~ mem(elt,t2tb1(X6),t2tb(X3)) )
& ! [X8: elt1,X9: elt1] :
( le1(X8,X9)
| ~ mem(elt,t2tb1(X9),t2tb(X4))
| ~ mem(elt,t2tb1(X8),t2tb(X3)) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
& ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) ),
inference(ennf_transformation,[],[f98]) ).
tff(f130,plain,
? [X0: list_elt,X1: list_elt,X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X10: elt1] :
( ? [X13: elt1] :
( ? [X16: list_elt,X17: elt1] :
( ? [X20: list_elt] :
( ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X20),t2tb(X5)),t2tb(X16)),infix_plpl(elt,t2tb(X0),t2tb(X1)))
& ( tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X17),nil(elt)))) = X20 ) )
& ? [X18: elt1,X19: list_elt] :
( ( tb2t(cons(elt,t2tb1(X18),t2tb(X19))) = X4 )
& ( X17 = X18 )
& ( X16 = X19 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ~ le1(X10,X13)
& ? [X14: elt1,X15: list_elt] :
( ( tb2t(cons(elt,t2tb1(X14),t2tb(X15))) = X4 )
& ( X13 = X14 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ? [X11: elt1,X12: list_elt] :
( ( tb2t(cons(elt,t2tb1(X11),t2tb(X12))) = X5 )
& ( X10 = X11 ) ) )
& ( X5 != tb2t(nil(elt)) )
& ( length2(elt,t2tb(X4)) != 0 )
& ( length2(elt,t2tb(X5)) != 0 )
& $less(0,length2(elt,t2tb(X5)))
& sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X6: elt1,X7: elt1] :
( le1(X6,X7)
| ~ mem(elt,t2tb1(X7),t2tb(X5))
| ~ mem(elt,t2tb1(X6),t2tb(X3)) )
& ! [X8: elt1,X9: elt1] :
( le1(X8,X9)
| ~ mem(elt,t2tb1(X9),t2tb(X4))
| ~ mem(elt,t2tb1(X8),t2tb(X3)) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
& ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) ),
inference(flattening,[],[f129]) ).
tff(f149,plain,
? [X0: list_elt,X1: list_elt,X2: list_elt] :
( ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ? [X6: elt1] :
( ? [X7: elt1] :
( ? [X8: list_elt,X9: elt1] :
( ? [X10: list_elt] :
( ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X10),t2tb(X5)),t2tb(X8)),infix_plpl(elt,t2tb(X0),t2tb(X1)))
& ( tb2t(infix_plpl(elt,t2tb(X3),cons(elt,t2tb1(X9),nil(elt)))) = X10 ) )
& ? [X11: elt1,X12: list_elt] :
( ( tb2t(cons(elt,t2tb1(X11),t2tb(X12))) = X4 )
& ( X9 = X11 )
& ( X8 = X12 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ~ le1(X6,X7)
& ? [X13: elt1,X14: list_elt] :
( ( tb2t(cons(elt,t2tb1(X13),t2tb(X14))) = X4 )
& ( X7 = X13 ) ) )
& ( X4 != tb2t(nil(elt)) )
& ? [X15: elt1,X16: list_elt] :
( ( tb2t(cons(elt,t2tb1(X15),t2tb(X16))) = X5 )
& ( X6 = X15 ) ) )
& ( X5 != tb2t(nil(elt)) )
& ( length2(elt,t2tb(X4)) != 0 )
& ( length2(elt,t2tb(X5)) != 0 )
& $less(0,length2(elt,t2tb(X5)))
& sorted1(X5)
& sorted1(X4)
& sorted1(X3)
& ! [X17: elt1,X18: elt1] :
( le1(X17,X18)
| ~ mem(elt,t2tb1(X18),t2tb(X5))
| ~ mem(elt,t2tb1(X17),t2tb(X3)) )
& ! [X19: elt1,X20: elt1] :
( le1(X19,X20)
| ~ mem(elt,t2tb1(X20),t2tb(X4))
| ~ mem(elt,t2tb1(X19),t2tb(X3)) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X5)),t2tb(X4)),infix_plpl(elt,t2tb(X0),t2tb(X1))) )
& ( X2 = tb2t(nil(elt)) )
& sorted1(X0)
& sorted1(X1) ),
inference(rectify,[],[f130]) ).
tff(f150,plain,
( ~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK20),t2tb(sK15)),t2tb(sK18)),infix_plpl(elt,t2tb(sK10),t2tb(sK11)))
& ( sK20 = tb2t(infix_plpl(elt,t2tb(sK13),cons(elt,t2tb1(sK19),nil(elt)))) )
& ( sK14 = tb2t(cons(elt,t2tb1(sK21),t2tb(sK22))) )
& ( sK19 = sK21 )
& ( sK18 = sK22 )
& ( tb2t(nil(elt)) != sK14 )
& ~ le1(sK16,sK17)
& ( sK14 = tb2t(cons(elt,t2tb1(sK23),t2tb(sK24))) )
& ( sK17 = sK23 )
& ( tb2t(nil(elt)) != sK14 )
& ( sK15 = tb2t(cons(elt,t2tb1(sK25),t2tb(sK26))) )
& ( sK16 = sK25 )
& ( tb2t(nil(elt)) != sK15 )
& ( 0 != length2(elt,t2tb(sK14)) )
& ( 0 != length2(elt,t2tb(sK15)) )
& $less(0,length2(elt,t2tb(sK15)))
& sorted1(sK15)
& sorted1(sK14)
& sorted1(sK13)
& ! [X17: elt1,X18: elt1] :
( le1(X17,X18)
| ~ mem(elt,t2tb1(X18),t2tb(sK15))
| ~ mem(elt,t2tb1(X17),t2tb(sK13)) )
& ! [X19: elt1,X20: elt1] :
( le1(X19,X20)
| ~ mem(elt,t2tb1(X20),t2tb(sK14))
| ~ mem(elt,t2tb1(X19),t2tb(sK13)) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK13),t2tb(sK15)),t2tb(sK14)),infix_plpl(elt,t2tb(sK10),t2tb(sK11)))
& ( tb2t(nil(elt)) = sK12 )
& sorted1(sK10)
& sorted1(sK11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13),skolemize(X4,sK14),skolemize(X5,sK15),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X8,sK18),skolemize(X9,sK19),skolemize(X10,sK20),skolemize(X11,sK21),skolemize(X12,sK22),skolemize(X13,sK23),skolemize(X14,sK24),skolemize(X15,sK25),skolemize(X16,sK26)],[f149]) ).
tff(f180,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) ),
inference(cnf_transformation,[],[f25]) ).
tff(f181,plain,
! [X0: ty,X1: uni] : ( infix_plpl(X0,nil(X0),X1) = X1 ),
inference(cnf_transformation,[],[f25]) ).
tff(f182,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( infix_plpl(X0,X1,infix_plpl(X0,X2,X3)) = infix_plpl(X0,infix_plpl(X0,X1,X2),X3) ),
inference(cnf_transformation,[],[f26]) ).
tff(f211,plain,
! [X2: uni,X0: ty,X1: uni] :
( ~ permut(X0,X1,X2)
| permut(X0,X2,X1) ),
inference(cnf_transformation,[],[f110]) ).
tff(f212,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ permut(X0,X2,X3)
| permut(X0,X1,X3)
| ~ permut(X0,X1,X2) ),
inference(cnf_transformation,[],[f112]) ).
tff(f215,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : permut(X0,infix_plpl(X0,cons(X0,X1,X2),X3),infix_plpl(X0,X2,cons(X0,X1,X3))),
inference(cnf_transformation,[],[f48]) ).
tff(f218,plain,
! [X2: uni,X0: ty,X1: uni] : permut(X0,infix_plpl(X0,X1,X2),infix_plpl(X0,X2,X1)),
inference(cnf_transformation,[],[f51]) ).
tff(f231,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f64]) ).
tff(f254,plain,
permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK13),t2tb(sK15)),t2tb(sK14)),infix_plpl(elt,t2tb(sK10),t2tb(sK11))),
inference(cnf_transformation,[],[f150]) ).
tff(f271,plain,
sK18 = sK22,
inference(cnf_transformation,[],[f150]) ).
tff(f272,plain,
sK19 = sK21,
inference(cnf_transformation,[],[f150]) ).
tff(f273,plain,
sK14 = tb2t(cons(elt,t2tb1(sK21),t2tb(sK22))),
inference(cnf_transformation,[],[f150]) ).
tff(f274,plain,
sK20 = tb2t(infix_plpl(elt,t2tb(sK13),cons(elt,t2tb1(sK19),nil(elt)))),
inference(cnf_transformation,[],[f150]) ).
tff(f275,plain,
~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK20),t2tb(sK15)),t2tb(sK18)),infix_plpl(elt,t2tb(sK10),t2tb(sK11))),
inference(cnf_transformation,[],[f150]) ).
tff(f276,plain,
~ permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK20),t2tb(sK15)),t2tb(sK22)),infix_plpl(elt,t2tb(sK10),t2tb(sK11))),
inference(definition_unfolding,[],[f275,f271]) ).
tff(f277,plain,
sK20 = tb2t(infix_plpl(elt,t2tb(sK13),cons(elt,t2tb1(sK21),nil(elt)))),
inference(definition_unfolding,[],[f274,f272]) ).
tff(f283,definition,
sF27 = t2tb(sK20),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f284,plain,
t2tb(sK20) = sF27,
inference(reorient_equations,[],[f283]) ).
tff(f285,definition,
sF28 = t2tb(sK15),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f286,plain,
t2tb(sK15) = sF28,
inference(reorient_equations,[],[f285]) ).
tff(f287,definition,
sF29 = infix_plpl(elt,sF27,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f288,plain,
infix_plpl(elt,sF27,sF28) = sF29,
inference(reorient_equations,[],[f287]) ).
tff(f289,definition,
sF30 = t2tb(sK22),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f290,plain,
t2tb(sK22) = sF30,
inference(reorient_equations,[],[f289]) ).
tff(f291,definition,
sF31 = infix_plpl(elt,sF29,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f292,plain,
infix_plpl(elt,sF29,sF30) = sF31,
inference(reorient_equations,[],[f291]) ).
tff(f293,definition,
sF32 = t2tb(sK10),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f294,plain,
t2tb(sK10) = sF32,
inference(reorient_equations,[],[f293]) ).
tff(f295,definition,
sF33 = t2tb(sK11),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f296,plain,
t2tb(sK11) = sF33,
inference(reorient_equations,[],[f295]) ).
tff(f297,definition,
sF34 = infix_plpl(elt,sF32,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f298,plain,
infix_plpl(elt,sF32,sF33) = sF34,
inference(reorient_equations,[],[f297]) ).
tff(f299,plain,
~ permut(elt,sF31,sF34),
inference(definition_folding,[],[f276,f298,f296,f294,f292,f290,f288,f286,f284]) ).
tff(f300,definition,
sF35 = t2tb(sK13),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f301,plain,
t2tb(sK13) = sF35,
inference(reorient_equations,[],[f300]) ).
tff(f302,definition,
sF36 = t2tb1(sK21),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
tff(f303,plain,
t2tb1(sK21) = sF36,
inference(reorient_equations,[],[f302]) ).
tff(f304,definition,
sF37 = nil(elt),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
tff(f305,plain,
nil(elt) = sF37,
inference(reorient_equations,[],[f304]) ).
tff(f306,definition,
sF38 = cons(elt,sF36,sF37),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
tff(f307,plain,
cons(elt,sF36,sF37) = sF38,
inference(reorient_equations,[],[f306]) ).
tff(f308,definition,
sF39 = infix_plpl(elt,sF35,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
tff(f309,plain,
infix_plpl(elt,sF35,sF38) = sF39,
inference(reorient_equations,[],[f308]) ).
tff(f310,definition,
sF40 = tb2t(sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
tff(f311,plain,
tb2t(sF39) = sF40,
inference(reorient_equations,[],[f310]) ).
tff(f312,plain,
sK20 = sF40,
inference(definition_folding,[],[f277,f311,f309,f307,f305,f303,f301]) ).
tff(f313,definition,
sF41 = cons(elt,sF36,sF30),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
tff(f314,plain,
cons(elt,sF36,sF30) = sF41,
inference(reorient_equations,[],[f313]) ).
tff(f315,definition,
sF42 = tb2t(sF41),
introduced(definition,[new_symbols(definition,[sF42])],[function_definition]) ).
tff(f316,plain,
tb2t(sF41) = sF42,
inference(reorient_equations,[],[f315]) ).
tff(f317,plain,
sK14 = sF42,
inference(definition_folding,[],[f273,f316,f314,f290,f303]) ).
tff(f341,definition,
sF52 = t2tb(sK14),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
tff(f342,plain,
t2tb(sK14) = sF52,
inference(reorient_equations,[],[f341]) ).
tff(f352,definition,
sF55 = infix_plpl(elt,sF35,sF28),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
tff(f353,plain,
infix_plpl(elt,sF35,sF28) = sF55,
inference(reorient_equations,[],[f352]) ).
tff(f354,definition,
sF56 = infix_plpl(elt,sF55,sF52),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
tff(f355,plain,
infix_plpl(elt,sF55,sF52) = sF56,
inference(reorient_equations,[],[f354]) ).
tff(f356,plain,
permut(elt,sF56,sF34),
inference(definition_folding,[],[f254,f298,f296,f294,f355,f342,f353,f286,f301]) ).
tff(f361,plain,
sK20 = tb2t(sF39),
inference(forward_demodulation,[],[f311,f312]) ).
tff(f362,plain,
sK14 = tb2t(sF41),
inference(forward_demodulation,[],[f316,f317]) ).
tff(f419,plain,
t2tb(sK20) = sF39,
inference(superposition,[],[f231,f361]) ).
tff(f420,plain,
t2tb(sK14) = sF41,
inference(superposition,[],[f231,f362]) ).
tff(f426,plain,
sF41 = sF52,
inference(forward_demodulation,[],[f420,f342]) ).
tff(f427,plain,
sF27 = sF39,
inference(forward_demodulation,[],[f419,f284]) ).
tff(f484,plain,
! [X0: uni] : ( infix_plpl(elt,sF37,X0) = X0 ),
inference(superposition,[],[f181,f305]) ).
tff(f1077,plain,
! [X0: uni] :
( ~ permut(elt,X0,sF56)
| permut(elt,X0,sF34) ),
inference(resolution,[],[f212,f356]) ).
tff(f1079,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ permut(X0,X1,infix_plpl(X0,X3,X2))
| permut(X0,X1,infix_plpl(X0,X2,X3)) ),
inference(resolution,[],[f212,f218]) ).
tff(f1285,plain,
! [X0: uni] : ( cons(elt,sF36,infix_plpl(elt,sF37,X0)) = infix_plpl(elt,sF38,X0) ),
inference(superposition,[],[f180,f307]) ).
tff(f1286,plain,
! [X0: uni] : ( cons(elt,sF36,infix_plpl(elt,sF30,X0)) = infix_plpl(elt,sF41,X0) ),
inference(superposition,[],[f180,f314]) ).
tff(f1300,plain,
! [X0: uni] : ( infix_plpl(elt,sF52,X0) = cons(elt,sF36,infix_plpl(elt,sF30,X0)) ),
inference(forward_demodulation,[],[f1286,f426]) ).
tff(f1301,plain,
! [X0: uni] : ( cons(elt,sF36,X0) = infix_plpl(elt,sF38,X0) ),
inference(forward_demodulation,[],[f1285,f484]) ).
tff(f1307,plain,
! [X0: uni] : ( infix_plpl(elt,sF35,infix_plpl(elt,sF38,X0)) = infix_plpl(elt,sF39,X0) ),
inference(superposition,[],[f182,f309]) ).
tff(f1323,plain,
! [X0: uni] : ( infix_plpl(elt,sF35,infix_plpl(elt,sF38,X0)) = infix_plpl(elt,sF27,X0) ),
inference(forward_demodulation,[],[f1307,f427]) ).
tff(f1326,plain,
! [X0: uni] : ( infix_plpl(elt,sF27,X0) = infix_plpl(elt,sF35,cons(elt,sF36,X0)) ),
inference(forward_demodulation,[],[f1323,f1301]) ).
tff(f2296,plain,
! [X0: uni,X1: uni] : permut(elt,infix_plpl(elt,infix_plpl(elt,sF52,X0),X1),infix_plpl(elt,infix_plpl(elt,sF30,X0),cons(elt,sF36,X1))),
inference(superposition,[],[f215,f1300]) ).
tff(f2301,plain,
! [X0: uni,X1: uni] : permut(elt,infix_plpl(elt,infix_plpl(elt,sF52,X0),X1),infix_plpl(elt,sF30,infix_plpl(elt,X0,cons(elt,sF36,X1)))),
inference(forward_demodulation,[],[f2296,f182]) ).
tff(f2308,plain,
! [X0: uni,X1: uni] : permut(elt,infix_plpl(elt,sF52,infix_plpl(elt,X0,X1)),infix_plpl(elt,sF30,infix_plpl(elt,X0,cons(elt,sF36,X1)))),
inference(forward_demodulation,[],[f2301,f182]) ).
tff(f66756,plain,
permut(elt,infix_plpl(elt,sF52,sF55),infix_plpl(elt,sF30,infix_plpl(elt,sF35,cons(elt,sF36,sF28)))),
inference(superposition,[],[f2308,f353]) ).
tff(f66812,plain,
permut(elt,infix_plpl(elt,sF52,sF55),infix_plpl(elt,sF30,infix_plpl(elt,sF27,sF28))),
inference(forward_demodulation,[],[f66756,f1326]) ).
tff(f66835,plain,
permut(elt,infix_plpl(elt,sF52,sF55),infix_plpl(elt,sF30,sF29)),
inference(forward_demodulation,[],[f66812,f288]) ).
tff(f68602,plain,
permut(elt,infix_plpl(elt,sF52,sF55),infix_plpl(elt,sF29,sF30)),
inference(resolution,[],[f66835,f1079]) ).
tff(f68618,plain,
permut(elt,infix_plpl(elt,sF52,sF55),sF31),
inference(forward_demodulation,[],[f68602,f292]) ).
tff(f68662,plain,
permut(elt,sF31,infix_plpl(elt,sF52,sF55)),
inference(resolution,[],[f68618,f211]) ).
tff(f68739,plain,
permut(elt,sF31,infix_plpl(elt,sF55,sF52)),
inference(resolution,[],[f68662,f1079]) ).
tff(f68755,plain,
permut(elt,sF31,sF56),
inference(forward_demodulation,[],[f68739,f355]) ).
tff(f68814,plain,
permut(elt,sF31,sF34),
inference(resolution,[],[f68755,f1077]) ).
tff(f68830,plain,
$false,
inference(forward_subsumption_resolution,[],[f68814,f299]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW628_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 % Computer : n009.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Mon Sep 28 14:23:15 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.27 Running first-order model finding
% 0.10/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.29/1.19 % (3060835)Will run a generic schedule for satisfiability detection.
% 6.29/1.19 % (3060842)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3638121102:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.29/1.19 % (3060840)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3863756375_2999 on theBenchmark for (2999ds/0Mi)
% 6.29/1.19 % (3060840)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.29/1.19 % (3060840)Terminated due to inappropriate strategy.
% 6.29/1.19 % (3060840)------------------------------
% 6.29/1.19 % (3060840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.19 % (3060840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.19 % (3060840)CaDiCaL version: 2.1.3
% 6.29/1.19 % (3060840)Termination reason: Inappropriate
% 6.29/1.19 % (3060840)Time elapsed: 0.005 s
% 6.29/1.19 % (3060840)Peak memory usage: 11 MB
% 6.29/1.19 % (3060840)Instructions burned: 7 (million)
% 6.29/1.19 % (3060841)% WARNING: option uhcvi not known.
% 6.29/1.19 % (3060840)------------------------------
% 6.29/1.19 % (3060840)------------------------------
% 6.29/1.19 % (3060841)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3641625049:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.29/1.19 % (3060844)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2822356165:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.29/1.19 % (3060846)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=563254281:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.29/1.19 % (3060843)dis+10_1_sil=32000:sp=arity:random_seed=544683678:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.29/1.19 % (3060845)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2468028725:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.29/1.19 % (3060849)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2686648635:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.29/1.19 % (3060849)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.29/1.19 % (3060849)Terminated due to inappropriate strategy.
% 6.29/1.19 % (3060849)------------------------------
% 6.29/1.19 % (3060849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.19 % (3060849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.19 % (3060849)CaDiCaL version: 2.1.3
% 6.29/1.19 % (3060849)Termination reason: Inappropriate
% 6.29/1.19 % (3060849)Time elapsed: 0.009 s
% 6.29/1.19 % (3060849)Peak memory usage: 11 MB
% 6.29/1.19 % (3060849)Instructions burned: 7 (million)
% 6.29/1.19 % (3060849)------------------------------
% 6.29/1.19 % (3060849)------------------------------
% 6.29/1.19 % (3060856)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2502173663:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.29/1.19 % (3060843)Instruction limit reached!
% 6.29/1.19 % (3060843)------------------------------
% 6.29/1.19 % (3060843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.19 % (3060843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.19 % (3060843)CaDiCaL version: 2.1.3
% 6.29/1.19 % (3060843)Termination reason: Instruction limit
% 6.29/1.19 % (3060843)Termination phase: Saturation
% 6.29/1.19 % (3060843)Time elapsed: 0.111 s
% 6.29/1.19 % (3060843)Peak memory usage: 13 MB
% 6.29/1.19 % (3060843)Instructions burned: 103 (million)
% 6.29/1.19 % (3060844)Instruction limit reached!
% 6.29/1.19 % (3060844)------------------------------
% 6.29/1.19 % (3060844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.19 % (3060844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.19 % (3060844)CaDiCaL version: 2.1.3
% 6.29/1.19 % (3060844)Termination reason: Instruction limit
% 6.29/1.19 % (3060844)Termination phase: Saturation
% 6.29/1.19 % (3060844)Time elapsed: 0.117 s
% 6.29/1.19 % (3060844)Peak memory usage: 13 MB
% 6.29/1.19 % (3060844)Instructions burned: 117 (million)
% 6.29/1.19 % (3060846)Instruction limit reached!
% 6.29/1.19 % (3060846)------------------------------
% 6.29/1.19 % (3060846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.19 % (3060846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.19 % (3060846)CaDiCaL version: 2.1.3
% 6.29/1.19 % (3060846)Termination reason: Instruction limit
% 8.49/1.74 % (3060846)Termination phase: Saturation
% 8.49/1.74 % (3060846)Time elapsed: 0.127 s
% 8.49/1.74 % (3060846)Peak memory usage: 12 MB
% 8.49/1.74 % (3060846)Instructions burned: 160 (million)
% 8.49/1.74 % (3060845)Instruction limit reached!
% 8.49/1.74 % (3060845)------------------------------
% 8.49/1.74 % (3060845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.49/1.74 % (3060845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.74 % (3060845)CaDiCaL version: 2.1.3
% 8.49/1.74 % (3060845)Termination reason: Instruction limit
% 8.49/1.74 % (3060845)Termination phase: Saturation
% 8.49/1.74 % (3060845)Time elapsed: 0.138 s
% 8.49/1.74 % (3060845)Peak memory usage: 13 MB
% 8.49/1.74 % (3060845)Instructions burned: 132 (million)
% 8.49/1.74 % (3060858)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2765593366:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.49/1.74 % (3060859)ott-21_1_sil=16000:fs=off:random_seed=3316394259:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.49/1.74 % (3060860)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1072090904:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.49/1.74 % (3060861)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4211529655:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.49/1.74 % (3060861)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.49/1.74 % (3060861)Terminated due to inappropriate strategy.
% 8.49/1.74 % (3060861)------------------------------
% 8.49/1.74 % (3060861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.49/1.74 % (3060861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.74 % (3060861)CaDiCaL version: 2.1.3
% 8.49/1.74 % (3060861)Termination reason: Inappropriate
% 8.49/1.74 % (3060861)Time elapsed: 0.007 s
% 8.49/1.74 % (3060861)Peak memory usage: 10 MB
% 8.49/1.74 % (3060861)Instructions burned: 6 (million)
% 8.49/1.74 % (3060861)------------------------------
% 8.49/1.74 % (3060861)------------------------------
% 8.49/1.74 % (3060856)Instruction limit reached!
% 8.49/1.74 % (3060856)------------------------------
% 8.49/1.74 % (3060856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.49/1.74 % (3060856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.74 % (3060856)CaDiCaL version: 2.1.3
% 8.49/1.74 % (3060856)Termination reason: Instruction limit
% 8.49/1.74 % (3060856)Termination phase: Saturation
% 8.49/1.74 % (3060856)Time elapsed: 0.143 s
% 8.49/1.74 % (3060856)Peak memory usage: 14 MB
% 8.49/1.74 % (3060856)Instructions burned: 131 (million)
% 8.49/1.74 % (3060866)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2197411578:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.49/1.74 % (3060868)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=925197675:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.49/1.74 % (3060868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.49/1.74 % (3060868)Terminated due to inappropriate strategy.
% 8.49/1.74 % (3060868)------------------------------
% 8.49/1.74 % (3060868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.49/1.74 % (3060868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.74 % (3060868)CaDiCaL version: 2.1.3
% 8.49/1.74 % (3060868)Termination reason: Inappropriate
% 8.49/1.74 % (3060868)Time elapsed: 0.007 s
% 8.49/1.74 % (3060868)Peak memory usage: 10 MB
% 8.49/1.74 % (3060868)Instructions burned: 6 (million)
% 8.49/1.74 % (3060868)------------------------------
% 8.49/1.74 % (3060868)------------------------------
% 8.49/1.74 % (3060870)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2566899166:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 8.49/1.74 % (3060859)Instruction limit reached!
% 8.49/1.74 % (3060859)------------------------------
% 8.49/1.74 % (3060859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.49/1.74 % (3060859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/1.74 % (3060859)CaDiCaL version: 2.1.3
% 8.49/1.74 % (3060859)Termination reason: Instruction limit
% 8.49/1.74 % (3060859)Termination phase: Saturation
% 17.46/5.21 % (3060859)Time elapsed: 0.167 s
% 17.46/5.21 % (3060859)Peak memory usage: 13 MB
% 17.46/5.21 % (3060859)Instructions burned: 180 (million)
% 17.46/5.21 % (3060872)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2785674821:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 17.46/5.21 % (3060860)Instruction limit reached!
% 17.46/5.21 % (3060860)------------------------------
% 17.46/5.21 % (3060860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060860)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060860)Termination reason: Instruction limit
% 17.46/5.21 % (3060860)Termination phase: Saturation
% 17.46/5.21 % (3060860)Time elapsed: 0.516 s
% 17.46/5.21 % (3060860)Peak memory usage: 13 MB
% 17.46/5.21 % (3060860)Instructions burned: 477 (million)
% 17.46/5.21 % (3060874)fmb+10_1_sil=64000:random_seed=997811919:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 17.46/5.21 % (3060874)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060874)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060874)------------------------------
% 17.46/5.21 % (3060874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060874)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060874)Termination reason: Inappropriate
% 17.46/5.21 % (3060874)Time elapsed: 0.007 s
% 17.46/5.21 % (3060874)Peak memory usage: 11 MB
% 17.46/5.21 % (3060874)Instructions burned: 7 (million)
% 17.46/5.21 % (3060874)------------------------------
% 17.46/5.21 % (3060874)------------------------------
% 17.46/5.21 % (3060876)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1041878875:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 17.46/5.21 % (3060876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060876)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060876)------------------------------
% 17.46/5.21 % (3060876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060876)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060876)Termination reason: Inappropriate
% 17.46/5.21 % (3060876)Time elapsed: 0.004 s
% 17.46/5.21 % (3060876)Peak memory usage: 11 MB
% 17.46/5.21 % (3060876)Instructions burned: 6 (million)
% 17.46/5.21 % (3060876)------------------------------
% 17.46/5.21 % (3060876)------------------------------
% 17.46/5.21 % (3060878)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1848127739:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 17.46/5.21 % (3060878)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060878)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060878)------------------------------
% 17.46/5.21 % (3060878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060878)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060878)Termination reason: Inappropriate
% 17.46/5.21 % (3060878)Time elapsed: 0.004 s
% 17.46/5.21 % (3060878)Peak memory usage: 10 MB
% 17.46/5.21 % (3060878)Instructions burned: 6 (million)
% 17.46/5.21 % (3060878)------------------------------
% 17.46/5.21 % (3060878)------------------------------
% 17.46/5.21 % (3060880)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=847838416:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 17.46/5.21 % (3060870)Instruction limit reached!
% 17.46/5.21 % (3060870)------------------------------
% 17.46/5.21 % (3060870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060870)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060870)Termination reason: Instruction limit
% 17.46/5.21 % (3060870)Termination phase: Saturation
% 17.46/5.21 % (3060870)Time elapsed: 0.580 s
% 17.46/5.21 % (3060870)Peak memory usage: 15 MB
% 17.46/5.21 % (3060870)Instructions burned: 692 (million)
% 17.46/5.21 % (3060858)Instruction limit reached!
% 17.46/5.21 % (3060858)------------------------------
% 17.46/5.21 % (3060858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060858)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060858)Termination reason: Instruction limit
% 17.46/5.21 % (3060858)Termination phase: Saturation
% 17.46/5.21 % (3060858)Time elapsed: 0.723 s
% 17.46/5.21 % (3060858)Peak memory usage: 17 MB
% 17.46/5.21 % (3060858)Instructions burned: 684 (million)
% 17.46/5.21 % (3060882)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1726996068:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 17.46/5.21 % (3060883)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3265963503:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 17.46/5.21 % (3060883)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060883)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060883)------------------------------
% 17.46/5.21 % (3060883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060883)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060883)Termination reason: Inappropriate
% 17.46/5.21 % (3060883)Time elapsed: 0.008 s
% 17.46/5.21 % (3060883)Peak memory usage: 11 MB
% 17.46/5.21 % (3060883)Instructions burned: 7 (million)
% 17.46/5.21 % (3060883)------------------------------
% 17.46/5.21 % (3060883)------------------------------
% 17.46/5.21 % (3060886)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3539782723:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 17.46/5.21 % (3060886)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060886)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060886)------------------------------
% 17.46/5.21 % (3060886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060886)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060886)Termination reason: Inappropriate
% 17.46/5.21 % (3060886)Time elapsed: 0.004 s
% 17.46/5.21 % (3060886)Peak memory usage: 10 MB
% 17.46/5.21 % (3060886)Instructions burned: 6 (million)
% 17.46/5.21 % (3060886)------------------------------
% 17.46/5.21 % (3060886)------------------------------
% 17.46/5.21 % (3060888)ott-2_1_sil=16000:newcnf=on:random_seed=1066250766:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 17.46/5.21 % (3060872)Instruction limit reached!
% 17.46/5.21 % (3060872)------------------------------
% 17.46/5.21 % (3060872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060872)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060872)Termination reason: Instruction limit
% 17.46/5.21 % (3060872)Termination phase: Saturation
% 17.46/5.21 % (3060872)Time elapsed: 0.838 s
% 17.46/5.21 % (3060872)Peak memory usage: 19 MB
% 17.46/5.21 % (3060872)Instructions burned: 880 (million)
% 17.46/5.21 % (3060890)ott+10_1_sil=32000:tgt=ground:random_seed=2346069284:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 17.46/5.21 % (3060866)Instruction limit reached!
% 17.46/5.21 % (3060866)------------------------------
% 17.46/5.21 % (3060866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060866)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060866)Termination reason: Instruction limit
% 17.46/5.21 % (3060866)Termination phase: Saturation
% 17.46/5.21 % (3060866)Time elapsed: 1.175 s
% 17.46/5.21 % (3060866)Peak memory usage: 23 MB
% 17.46/5.21 % (3060866)Instructions burned: 1180 (million)
% 17.46/5.21 % (3060892)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=946700504:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 17.46/5.21 % (3060892)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060892)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060892)------------------------------
% 17.46/5.21 % (3060892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060892)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060892)Termination reason: Inappropriate
% 17.46/5.21 % (3060892)Time elapsed: 0.005 s
% 17.46/5.21 % (3060892)Peak memory usage: 11 MB
% 17.46/5.21 % (3060892)Instructions burned: 7 (million)
% 17.46/5.21 % (3060892)------------------------------
% 17.46/5.21 % (3060892)------------------------------
% 17.46/5.21 % (3060894)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3599623727:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi)
% 17.46/5.21 % (3060888)Instruction limit reached!
% 17.46/5.21 % (3060888)------------------------------
% 17.46/5.21 % (3060888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060888)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060888)Termination reason: Instruction limit
% 17.46/5.21 % (3060888)Termination phase: Saturation
% 17.46/5.21 % (3060888)Time elapsed: 0.828 s
% 17.46/5.21 % (3060888)Peak memory usage: 15 MB
% 17.46/5.21 % (3060888)Instructions burned: 869 (million)
% 17.46/5.21 % (3060896)dis+21_1_sil=32000:sas=cadical:random_seed=1463995099:i=3773:amm=off_2981 on theBenchmark for (2981ds/3773Mi)
% 17.46/5.21 % (3060882)Instruction limit reached!
% 17.46/5.21 % (3060882)------------------------------
% 17.46/5.21 % (3060882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060882)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060882)Termination reason: Instruction limit
% 17.46/5.21 % (3060882)Termination phase: Saturation
% 17.46/5.21 % (3060882)Time elapsed: 1.517 s
% 17.46/5.21 % (3060882)Peak memory usage: 30 MB
% 17.46/5.21 % (3060882)Instructions burned: 1472 (million)
% 17.46/5.21 % (3060898)ott+11_1_sil=16000:gs=on:random_seed=2231516494:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2975 on theBenchmark for (2975ds/2251Mi)
% 17.46/5.21 % (3060898)Instruction limit reached!
% 17.46/5.21 % (3060898)------------------------------
% 17.46/5.21 % (3060898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060898)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060898)Termination reason: Instruction limit
% 17.46/5.21 % (3060898)Termination phase: Saturation
% 17.46/5.21 % (3060898)Time elapsed: 2.063 s
% 17.46/5.21 % (3060898)Peak memory usage: 26 MB
% 17.46/5.21 % (3060898)Instructions burned: 2252 (million)
% 17.46/5.21 % (3060900)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=596059880:fmbsr=1.6:i=67534_2954 on theBenchmark for (2954ds/67534Mi)
% 17.46/5.21 % (3060900)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 17.46/5.21 % (3060900)Terminated due to inappropriate strategy.
% 17.46/5.21 % (3060900)------------------------------
% 17.46/5.21 % (3060900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060900)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060900)Termination reason: Inappropriate
% 17.46/5.21 % (3060900)Time elapsed: 0.004 s
% 17.46/5.21 % (3060900)Peak memory usage: 11 MB
% 17.46/5.21 % (3060900)Instructions burned: 7 (million)
% 17.46/5.21 % (3060900)------------------------------
% 17.46/5.21 % (3060900)------------------------------
% 17.46/5.21 % (3060902)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1270024525:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2954 on theBenchmark for (2954ds/4591Mi)
% 17.46/5.21 % (3060894)Instruction limit reached!
% 17.46/5.21 % (3060894)------------------------------
% 17.46/5.21 % (3060894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.21 % (3060894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.21 % (3060894)CaDiCaL version: 2.1.3
% 17.46/5.21 % (3060894)Termination reason: Instruction limit
% 17.46/5.21 % (3060894)Termination phase: Saturation
% 17.46/5.21 % (3060894)Time elapsed: 3.325 s
% 17.46/5.21 % (3060894)Peak memory usage: 44 MB
% 17.46/5.21 % (3060894)Instructions burned: 3513 (million)
% 17.46/5.21 % (3060906)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2488890439:i=29340_2951 on theBenchmark for (2951ds/29340Mi)
% 17.46/5.21 % (3060890) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3060835-3060890"...
% 17.46/5.21 % (3060890)...printing done.
% 17.46/5.21 % (3060890)Refutation found. Thanks to Tanya!
% 17.46/5.21 % SZS status Theorem for theBenchmark
% 17.46/5.21 % SZS output start Proof for theBenchmark
% See solution above
% 17.46/5.22 % (3060890)------------------------------
% 17.46/5.22 % (3060890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.46/5.22 % (3060890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.46/5.22 % (3060890)CaDiCaL version: 2.1.3
% 17.46/5.22 % (3060890)Termination reason: Refutation
% 17.46/5.22 % (3060890)Time elapsed: 3.662 s
% 17.46/5.22 % (3060890)Peak memory usage: 45 MB
% 17.46/5.22 % (3060890)Instructions burned: 3755 (million)
% 17.46/5.22 % (3060835)Success in time 4.931 s
% 17.46/5.22 % Vampire exiting
%------------------------------------------------------------------------------