%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW629_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 : n011.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 5.71s 1.63s
% Output : Refutation 7.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 65 ( 15 unt; 0 typ; 7 def)
% Number of atoms : 347 ( 123 equ)
% Maximal formula atoms : 25 ( 5 avg)
% Number of connectives : 356 ( 74 ~; 74 |; 150 &)
% ( 12 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 57 ( 9 atm; 21 fun; 27 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 : 15 ( 12 usr; 8 prp; 0-3 aty)
% Number of functors : 52 ( 49 usr; 21 con; 0-5 aty)
% Number of variables : 155 ( 103 !; 52 ?; 155 :)
% 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_33,type,
sK0: ( uni * uni * ty ) > uni ).
tff(func_def_34,type,
sK1: ( ty * uni * uni ) > uni ).
tff(func_def_35,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_36,type,
sK3: list_elt ).
tff(func_def_37,type,
sK4: list_elt ).
tff(func_def_38,type,
sK5: list_elt ).
tff(func_def_39,type,
sK6: list_elt ).
tff(func_def_40,type,
sK7: list_elt ).
tff(func_def_41,type,
sK8: list_elt ).
tff(func_def_42,type,
sK9: bool1 ).
tff(func_def_43,type,
sK10: list_elt ).
tff(func_def_44,type,
sK11: list_elt ).
tff(func_def_45,type,
sK12: list_elt ).
tff(func_def_46,type,
sK13: ( list_elt * list_elt ) > elt1 ).
tff(func_def_47,type,
sK14: ( list_elt * list_elt ) > elt1 ).
tff(func_def_48,type,
sK15: ( list_elt * elt1 ) > elt1 ).
tff(func_def_49,type,
sK16: list_elt > elt1 ).
tff(func_def_50,type,
sK17: list_elt > elt1 ).
tff(func_def_51,type,
sK18: list_elt > list_elt ).
tff(func_def_52,type,
sK19: list_elt > elt1 ).
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(f33,axiom,
! [X0: ty,X2: uni,X3: uni,X1: 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(f45,axiom,
! [X1: uni,X3: uni,X0: ty,X2: uni] :
( permut(X0,X1,X2)
=> ( permut(X0,X2,X3)
=> permut(X0,X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',permut_trans) ).
tff(f74,conjecture,
! [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
=> ! [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
=> ! [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
=> ! [X5: list_elt,X4: list_elt,X3: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
=> ! [X6: bool1] :
( ( ( X5 = tb2t(nil(elt)) )
<=> ( X6 = true1 ) )
=> ( ( X6 = true1 )
=> ( ( X5 = tb2t(nil(elt)) )
=> ( permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
=> ! [X7: list_elt] :
( ( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
=> ! [X8: list_elt] :
( ( permut(elt,t2tb(X8),t2tb(X3))
& sorted1(X8) )
=> ( ( ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8) )
=> ! [X9: list_elt] :
( ( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
=> ( permut(elt,t2tb(X9),t2tb(X0))
& sorted1(X9) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_mergesort) ).
tff(f75,negated_conjecture,
~ ! [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
=> ! [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
=> ! [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
=> ! [X5: list_elt,X4: list_elt,X3: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X5)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( length2(elt,t2tb(X5)) = 0 )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X3)),1) ) ) ) )
=> ! [X6: bool1] :
( ( ( X5 = tb2t(nil(elt)) )
<=> ( X6 = true1 ) )
=> ( ( X6 = true1 )
=> ( ( X5 = tb2t(nil(elt)) )
=> ( permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X3)),t2tb(X0))
=> ! [X7: list_elt] :
( ( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
=> ! [X8: list_elt] :
( ( permut(elt,t2tb(X8),t2tb(X3))
& sorted1(X8) )
=> ( ( ( X5 = tb2t(nil(elt)) )
& sorted1(X7)
& sorted1(X8) )
=> ! [X9: list_elt] :
( ( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
=> ( permut(elt,t2tb(X9),t2tb(X0))
& sorted1(X9) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f74]) ).
tff(f78,plain,
~ ! [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
=> ! [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
=> ! [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
=> ! [X5: list_elt,X4: list_elt,X3: list_elt] :
( ( permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X3)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X5)) )
| ( ( 0 = length2(elt,t2tb(X3)) )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X5)),1) ) ) ) )
=> ! [X6: bool1] :
( ( ( X6 = true1 )
<=> ( tb2t(nil(elt)) = X3 ) )
=> ( ( X6 = true1 )
=> ( ( tb2t(nil(elt)) = X3 )
=> ( permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X0))
=> ! [X7: list_elt] :
( ( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
=> ! [X8: list_elt] :
( ( sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X5)) )
=> ( ( ( tb2t(nil(elt)) = X3 )
& sorted1(X7)
& sorted1(X8) )
=> ! [X9: list_elt] :
( ( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
=> ( permut(elt,t2tb(X9),t2tb(X0))
& sorted1(X9) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f75]) ).
tff(f83,plain,
! [X3: uni,X2: ty,X0: uni,X1: uni] :
( permut(X2,X0,X3)
=> ( permut(X2,X3,X1)
=> permut(X2,X0,X1) ) ),
inference(rectify,[],[f45]) ).
tff(f99,plain,
! [X3: uni,X1: uni,X2: uni,X0: ty] : ( num_occ1(X0,X3,infix_plpl(X0,X1,X2)) = $sum(num_occ1(X0,X3,X1),num_occ1(X0,X3,X2)) ),
inference(rectify,[],[f33]) ).
tff(f105,plain,
! [X2: uni,X0: ty,X1: uni] :
( ( ! [X4: uni] :
( sort1(X0,X4)
=> ( num_occ1(X0,X4,X1) = num_occ1(X0,X4,X2) ) )
=> permut(X0,X2,X1) )
& ( permut(X0,X2,X1)
=> ! [X3: uni] : ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) ) ) ),
inference(rectify,[],[f42]) ).
tff(f123,plain,
! [X3: uni,X2: ty,X0: uni,X1: uni] :
( permut(X2,X0,X1)
| ~ permut(X2,X3,X1)
| ~ permut(X2,X0,X3) ),
inference(ennf_transformation,[],[f83]) ).
tff(f124,plain,
! [X3: uni,X1: uni,X0: uni,X2: ty] :
( ~ permut(X2,X3,X1)
| ~ permut(X2,X0,X3)
| permut(X2,X0,X1) ),
inference(flattening,[],[f123]) ).
tff(f131,plain,
? [X0: list_elt] :
( ? [X1: list_elt] :
( ? [X2: list_elt] :
( ? [X5: list_elt,X4: list_elt,X3: list_elt] :
( ? [X6: bool1] :
( ? [X7: list_elt] :
( ? [X8: list_elt] :
( ? [X9: list_elt] :
( ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) )
& sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8))) )
& ( tb2t(nil(elt)) = X3 )
& sorted1(X7)
& sorted1(X8)
& sorted1(X8)
& permut(elt,t2tb(X8),t2tb(X5)) )
& sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4)) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X0))
& ( tb2t(nil(elt)) = X3 )
& ( X6 = true1 )
& ( ( X6 = true1 )
<=> ( tb2t(nil(elt)) = X3 ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X3)),t2tb(X0))
& ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X5)) )
| ( ( 0 = length2(elt,t2tb(X3)) )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X5)),1) ) ) ) )
& ( X2 = tb2t(nil(elt)) ) )
& ( X1 = tb2t(nil(elt)) ) )
& $less(1,length2(elt,t2tb(X0))) ),
inference(ennf_transformation,[],[f78]) ).
tff(f132,plain,
? [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
& ? [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
& ? [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
& ? [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X5)) )
| ( ( 0 = length2(elt,t2tb(X3)) )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X5)),1) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X3)),t2tb(X0))
& ? [X6: bool1] :
( ? [X7: list_elt] :
( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4))
& ? [X8: list_elt] :
( sorted1(X8)
& ( tb2t(nil(elt)) = X3 )
& ? [X9: list_elt] :
( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8)))
& ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) ) )
& permut(elt,t2tb(X8),t2tb(X5))
& sorted1(X8)
& sorted1(X7) ) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X0))
& ( X6 = true1 )
& ( tb2t(nil(elt)) = X3 )
& ( ( X6 = true1 )
<=> ( tb2t(nil(elt)) = X3 ) ) ) ) ) ) ),
inference(flattening,[],[f131]) ).
tff(f134,plain,
! [X2: uni,X1: uni,X0: ty] :
( ( ! [X3: uni] : ( num_occ1(X0,X3,X1) = num_occ1(X0,X3,X2) )
| ~ permut(X0,X2,X1) )
& ( permut(X0,X2,X1)
| ? [X4: uni] :
( ( num_occ1(X0,X4,X1) != num_occ1(X0,X4,X2) )
& sort1(X0,X4) ) ) ),
inference(ennf_transformation,[],[f105]) ).
tff(f140,plain,
! [X0: uni,X1: uni,X2: ty] :
( ( ! [X3: uni] : ( num_occ1(X2,X3,X0) = num_occ1(X2,X3,X1) )
| ~ permut(X2,X0,X1) )
& ( permut(X2,X0,X1)
| ? [X4: uni] :
( ( num_occ1(X2,X4,X0) != num_occ1(X2,X4,X1) )
& sort1(X2,X4) ) ) ),
inference(rectify,[],[f134]) ).
tff(f141,plain,
! [X0: uni,X1: uni,X2: ty] :
( ( ! [X3: uni] : ( num_occ1(X2,X3,X0) = num_occ1(X2,X3,X1) )
| ~ permut(X2,X0,X1) )
& ( permut(X2,X0,X1)
| ( ( num_occ1(X2,sK0(X0,X1,X2),X1) != num_occ1(X2,sK0(X0,X1,X2),X0) )
& sort1(X2,sK0(X0,X1,X2)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X4,sK0(X0,X1,X2))],[f140]) ).
tff(f151,plain,
? [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
& ? [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
& ? [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
& ? [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X5)) )
| ( ( 0 = length2(elt,t2tb(X3)) )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X5)),1) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X3)),t2tb(X0))
& ? [X6: bool1] :
( ? [X7: list_elt] :
( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4))
& ? [X8: list_elt] :
( sorted1(X8)
& ( tb2t(nil(elt)) = X3 )
& ? [X9: list_elt] :
( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8)))
& ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) ) )
& permut(elt,t2tb(X8),t2tb(X5))
& sorted1(X8)
& sorted1(X7) ) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X0))
& ( X6 = true1 )
& ( tb2t(nil(elt)) = X3 )
& ( ( X6 = true1 )
| ( tb2t(nil(elt)) != X3 ) )
& ( ( tb2t(nil(elt)) = X3 )
| ( true1 != X6 ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f132]) ).
tff(f152,plain,
? [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
& ? [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
& ? [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
& ? [X4: list_elt,X5: list_elt,X3: list_elt] :
( ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X5)) )
| ( ( 0 = length2(elt,t2tb(X3)) )
& ( length2(elt,t2tb(X4)) = $sum(length2(elt,t2tb(X5)),1) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X3)),t2tb(X0))
& ? [X6: bool1] :
( ? [X7: list_elt] :
( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X4))
& ? [X8: list_elt] :
( sorted1(X8)
& ( tb2t(nil(elt)) = X3 )
& ? [X9: list_elt] :
( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8)))
& ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) ) )
& permut(elt,t2tb(X8),t2tb(X5))
& sorted1(X8)
& sorted1(X7) ) )
& permut(elt,infix_plpl(elt,t2tb(X4),t2tb(X5)),t2tb(X0))
& ( X6 = true1 )
& ( tb2t(nil(elt)) = X3 )
& ( ( X6 = true1 )
| ( tb2t(nil(elt)) != X3 ) )
& ( ( tb2t(nil(elt)) = X3 )
| ( true1 != X6 ) ) ) ) ) ) ),
inference(flattening,[],[f151]) ).
tff(f153,plain,
? [X0: list_elt] :
( $less(1,length2(elt,t2tb(X0)))
& ? [X1: list_elt] :
( ( X1 = tb2t(nil(elt)) )
& ? [X2: list_elt] :
( ( X2 = tb2t(nil(elt)) )
& ? [X3: list_elt,X4: list_elt,X5: list_elt] :
( ( ( length2(elt,t2tb(X4)) = length2(elt,t2tb(X3)) )
| ( ( 0 = length2(elt,t2tb(X5)) )
& ( length2(elt,t2tb(X3)) = $sum(length2(elt,t2tb(X4)),1) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(X3),t2tb(X4)),t2tb(X5)),t2tb(X0))
& ? [X6: bool1] :
( ? [X7: list_elt] :
( sorted1(X7)
& permut(elt,t2tb(X7),t2tb(X3))
& ? [X8: list_elt] :
( sorted1(X8)
& ( tb2t(nil(elt)) = X5 )
& ? [X9: list_elt] :
( sorted1(X9)
& permut(elt,t2tb(X9),infix_plpl(elt,t2tb(X7),t2tb(X8)))
& ( ~ sorted1(X9)
| ~ permut(elt,t2tb(X9),t2tb(X0)) ) )
& permut(elt,t2tb(X8),t2tb(X4))
& sorted1(X8)
& sorted1(X7) ) )
& permut(elt,infix_plpl(elt,t2tb(X3),t2tb(X4)),t2tb(X0))
& ( X6 = true1 )
& ( tb2t(nil(elt)) = X5 )
& ( ( X6 = true1 )
| ( tb2t(nil(elt)) != X5 ) )
& ( ( tb2t(nil(elt)) = X5 )
| ( true1 != X6 ) ) ) ) ) ) ),
inference(rectify,[],[f152]) ).
tff(f154,plain,
( $less(1,length2(elt,t2tb(sK3)))
& ( tb2t(nil(elt)) = sK4 )
& ( tb2t(nil(elt)) = sK5 )
& ( ( length2(elt,t2tb(sK7)) = length2(elt,t2tb(sK6)) )
| ( ( 0 = length2(elt,t2tb(sK8)) )
& ( length2(elt,t2tb(sK6)) = $sum(length2(elt,t2tb(sK7)),1) ) ) )
& permut(elt,infix_plpl(elt,infix_plpl(elt,t2tb(sK6),t2tb(sK7)),t2tb(sK8)),t2tb(sK3))
& sorted1(sK10)
& permut(elt,t2tb(sK10),t2tb(sK6))
& sorted1(sK11)
& ( tb2t(nil(elt)) = sK8 )
& sorted1(sK12)
& permut(elt,t2tb(sK12),infix_plpl(elt,t2tb(sK10),t2tb(sK11)))
& ( ~ sorted1(sK12)
| ~ permut(elt,t2tb(sK12),t2tb(sK3)) )
& permut(elt,t2tb(sK11),t2tb(sK7))
& sorted1(sK11)
& sorted1(sK10)
& permut(elt,infix_plpl(elt,t2tb(sK6),t2tb(sK7)),t2tb(sK3))
& ( true1 = sK9 )
& ( tb2t(nil(elt)) = sK8 )
& ( ( true1 = sK9 )
| ( tb2t(nil(elt)) != sK8 ) )
& ( ( tb2t(nil(elt)) = sK8 )
| ( true1 != sK9 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X5,sK8),skolemize(X6,sK9),skolemize(X7,sK10),skolemize(X8,sK11),skolemize(X9,sK12)],[f153]) ).
tff(f177,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty] :
( ~ permut(X3,X0,X1)
| ~ permut(X3,X2,X0)
| permut(X3,X2,X1) ),
inference(rectify,[],[f124]) ).
tff(f189,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty] : ( $sum(num_occ1(X3,X0,X1),num_occ1(X3,X0,X2)) = num_occ1(X3,X0,infix_plpl(X3,X1,X2)) ),
inference(rectify,[],[f99]) ).
tff(f196,plain,
! [X2: ty,X0: uni,X1: uni] :
( ( num_occ1(X2,sK0(X0,X1,X2),X1) != num_occ1(X2,sK0(X0,X1,X2),X0) )
| permut(X2,X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
tff(f197,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] :
( ( num_occ1(X2,X3,X0) = num_occ1(X2,X3,X1) )
| ~ permut(X2,X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
tff(f219,plain,
permut(elt,infix_plpl(elt,t2tb(sK6),t2tb(sK7)),t2tb(sK3)),
inference(cnf_transformation,[],[f154]) ).
tff(f222,plain,
permut(elt,t2tb(sK11),t2tb(sK7)),
inference(cnf_transformation,[],[f154]) ).
tff(f223,plain,
( ~ permut(elt,t2tb(sK12),t2tb(sK3))
| ~ sorted1(sK12) ),
inference(cnf_transformation,[],[f154]) ).
tff(f224,plain,
permut(elt,t2tb(sK12),infix_plpl(elt,t2tb(sK10),t2tb(sK11))),
inference(cnf_transformation,[],[f154]) ).
tff(f225,plain,
sorted1(sK12),
inference(cnf_transformation,[],[f154]) ).
tff(f228,plain,
permut(elt,t2tb(sK10),t2tb(sK6)),
inference(cnf_transformation,[],[f154]) ).
tff(f269,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni] :
( permut(X3,X2,X1)
| ~ permut(X3,X2,X0)
| ~ permut(X3,X0,X1) ),
inference(cnf_transformation,[],[f177]) ).
tff(f287,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni] : ( $sum(num_occ1(X3,X0,X1),num_occ1(X3,X0,X2)) = num_occ1(X3,X0,infix_plpl(X3,X1,X2)) ),
inference(cnf_transformation,[],[f189]) ).
tff(f318,definition,
( spl20_5
<=> sorted1(sK12) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
tff(f321,plain,
spl20_5,
inference(avatar_split_clause,[],[f225,f318]) ).
tff(f333,definition,
( spl20_8
<=> permut(elt,t2tb(sK12),t2tb(sK3)) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
tff(f335,plain,
( ~ permut(elt,t2tb(sK12),t2tb(sK3))
| spl20_8 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f336,plain,
( ~ spl20_8
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f223,f318,f333]) ).
tff(f338,definition,
( spl20_9
<=> permut(elt,t2tb(sK11),t2tb(sK7)) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
tff(f340,plain,
( permut(elt,t2tb(sK11),t2tb(sK7))
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f338]) ).
tff(f341,plain,
spl20_9,
inference(avatar_split_clause,[],[f222,f338]) ).
tff(f358,definition,
( spl20_13
<=> permut(elt,t2tb(sK12),infix_plpl(elt,t2tb(sK10),t2tb(sK11))) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
tff(f360,plain,
( permut(elt,t2tb(sK12),infix_plpl(elt,t2tb(sK10),t2tb(sK11)))
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f358]) ).
tff(f361,plain,
spl20_13,
inference(avatar_split_clause,[],[f224,f358]) ).
tff(f363,definition,
( spl20_14
<=> permut(elt,t2tb(sK10),t2tb(sK6)) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
tff(f365,plain,
( permut(elt,t2tb(sK10),t2tb(sK6))
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f363]) ).
tff(f366,plain,
spl20_14,
inference(avatar_split_clause,[],[f228,f363]) ).
tff(f368,definition,
( spl20_15
<=> permut(elt,infix_plpl(elt,t2tb(sK6),t2tb(sK7)),t2tb(sK3)) ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
tff(f370,plain,
( permut(elt,infix_plpl(elt,t2tb(sK6),t2tb(sK7)),t2tb(sK3))
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f368]) ).
tff(f371,plain,
spl20_15,
inference(avatar_split_clause,[],[f219,f368]) ).
tff(f399,plain,
( ! [X0: uni] : ( num_occ1(elt,X0,t2tb(sK11)) = num_occ1(elt,X0,t2tb(sK7)) )
| ~ spl20_9 ),
inference(unit_resulting_resolution,[],[f197,f340]) ).
tff(f452,plain,
( ! [X0: uni] : ( num_occ1(elt,X0,t2tb(sK10)) = num_occ1(elt,X0,t2tb(sK6)) )
| ~ spl20_14 ),
inference(unit_resulting_resolution,[],[f197,f365]) ).
tff(f626,plain,
( ~ permut(elt,infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3))
| spl20_8
| ~ spl20_13 ),
inference(unit_resulting_resolution,[],[f269,f335,f360]) ).
tff(f645,definition,
( spl20_36
<=> permut(elt,infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3)) ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
tff(f647,plain,
( ~ permut(elt,infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3))
| spl20_36 ),
inference(avatar_component_clause,[],[f645]) ).
tff(f648,plain,
( ~ spl20_36
| spl20_8
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f626,f358,f333,f645]) ).
tff(f823,plain,
( ! [X0: uni] : ( num_occ1(elt,X0,t2tb(sK3)) = num_occ1(elt,X0,infix_plpl(elt,t2tb(sK6),t2tb(sK7))) )
| ~ spl20_15 ),
inference(unit_resulting_resolution,[],[f197,f370]) ).
tff(f897,plain,
( ! [X0: uni] : ( num_occ1(elt,X0,t2tb(sK3)) = $sum(num_occ1(elt,X0,t2tb(sK6)),num_occ1(elt,X0,t2tb(sK7))) )
| ~ spl20_15 ),
inference(forward_demodulation,[],[f823,f287]) ).
tff(f1233,plain,
( ( num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),infix_plpl(elt,t2tb(sK10),t2tb(sK11))) != num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK3)) )
| spl20_36 ),
inference(unit_resulting_resolution,[],[f196,f647]) ).
tff(f1259,plain,
( ( num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),infix_plpl(elt,t2tb(sK10),t2tb(sK11))) != $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK6)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) )
| ~ spl20_15
| spl20_36 ),
inference(forward_demodulation,[],[f1233,f897]) ).
tff(f1263,plain,
( ( $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK6)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) != $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK10)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK11))) )
| ~ spl20_15
| spl20_36 ),
inference(forward_demodulation,[],[f1259,f287]) ).
tff(f1265,plain,
( ( $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK10)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) != $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK6)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) )
| ~ spl20_9
| ~ spl20_15
| spl20_36 ),
inference(forward_demodulation,[],[f1263,f399]) ).
tff(f1268,plain,
( ( $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK6)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) != $sum(num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK6)),num_occ1(elt,sK0(infix_plpl(elt,t2tb(sK10),t2tb(sK11)),t2tb(sK3),elt),t2tb(sK7))) )
| ~ spl20_9
| ~ spl20_14
| ~ spl20_15
| spl20_36 ),
inference(forward_demodulation,[],[f1265,f452]) ).
tff(f1269,plain,
( $false
| ~ spl20_9
| ~ spl20_14
| ~ spl20_15
| spl20_36 ),
inference(trivial_inequality_removal,[],[f1268]) ).
tff(f1270,plain,
( ~ spl20_9
| ~ spl20_14
| ~ spl20_15
| spl20_36 ),
inference(avatar_contradiction_clause,[],[f1269]) ).
tff(f1271,plain,
$false,
inference(avatar_smt_refutation,[],[f1270,f648,f371,f366,f361,f341,f336,f321]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW629_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 14:23:15 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 3.14/1.19 % (3416704)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.14/1.19 % (3416712)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=814857674:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.14/1.19 % (3416712)Instruction limit reached!
% 3.14/1.19 % (3416712)------------------------------
% 3.14/1.19 % (3416712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.19 % (3416712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.19 % (3416712)CaDiCaL version: 2.1.3
% 3.14/1.19 % (3416712)Termination reason: Instruction limit
% 3.14/1.19 % (3416712)Termination phase: Saturation
% 3.14/1.19 % (3416712)Time elapsed: 0.003 s
% 3.14/1.19 % (3416712)Peak memory usage: 88 MB
% 3.14/1.19 % (3416712)Instructions burned: 8 (million)
% 3.14/1.19 % (3416709)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3653730714:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.14/1.19 % (3416710)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2721637118:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.14/1.19 % (3416711)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4251759045:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.14/1.19 % (3416714)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2098145057:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.14/1.19 % (3416713)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2324533002:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.14/1.19 % (3416715)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3386172428:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.14/1.19 % (3416713)Instruction limit reached!
% 3.14/1.19 % (3416713)------------------------------
% 3.14/1.19 % (3416713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.19 % (3416713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.19 % (3416713)CaDiCaL version: 2.1.3
% 3.14/1.19 % (3416713)Termination reason: Instruction limit
% 3.14/1.19 % (3416713)Termination phase: Property scanning
% 3.14/1.19 % (3416713)Time elapsed: 0.003 s
% 3.14/1.19 % (3416713)Peak memory usage: 86 MB
% 3.14/1.19 % (3416713)Instructions burned: 5 (million)
% 3.14/1.19 % (3416709)Instruction limit reached!
% 3.14/1.19 % (3416709)------------------------------
% 3.14/1.19 % (3416709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.19 % (3416709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.19 % (3416709)CaDiCaL version: 2.1.3
% 3.14/1.19 % (3416709)Termination reason: Instruction limit
% 3.14/1.19 % (3416709)Termination phase: Saturation
% 3.14/1.19 % (3416709)Time elapsed: 0.029 s
% 3.14/1.19 % (3416709)Peak memory usage: 111 MB
% 3.14/1.19 % (3416709)Instructions burned: 12 (million)
% 3.14/1.19 % (3416715)Instruction limit reached!
% 3.14/1.19 % (3416715)------------------------------
% 3.14/1.19 % (3416715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.19 % (3416715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.19 % (3416715)CaDiCaL version: 2.1.3
% 3.14/1.19 % (3416715)Termination reason: Instruction limit
% 3.14/1.19 % (3416715)Termination phase: Saturation
% 3.14/1.19 % (3416715)Time elapsed: 0.041 s
% 3.14/1.19 % (3416715)Peak memory usage: 116 MB
% 3.14/1.19 % (3416715)Instructions burned: 33 (million)
% 3.14/1.19 % (3416714)Instruction limit reached!
% 3.14/1.19 % (3416714)------------------------------
% 3.14/1.19 % (3416714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.14/1.19 % (3416714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.14/1.19 % (3416714)CaDiCaL version: 2.1.3
% 3.14/1.19 % (3416714)Termination reason: Instruction limit
% 3.14/1.19 % (3416714)Termination phase: Saturation
% 3.14/1.19 % (3416714)Time elapsed: 0.048 s
% 3.14/1.19 % (3416714)Peak memory usage: 116 MB
% 3.14/1.19 % (3416714)Instructions burned: 47 (million)
% 3.14/1.19 % (3416717)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1954170854:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.14/1.19 % (3416717)Instruction limit reached!
% 3.14/1.19 % (3416717)------------------------------
% 4.37/1.37 % (3416717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416717)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416717)Termination reason: Instruction limit
% 4.37/1.37 % (3416717)Termination phase: Saturation
% 4.37/1.37 % (3416717)Time elapsed: 0.005 s
% 4.37/1.37 % (3416717)Peak memory usage: 88 MB
% 4.37/1.37 % (3416717)Instructions burned: 16 (million)
% 4.37/1.37 % (3416711)Instruction limit reached!
% 4.37/1.37 % (3416711)------------------------------
% 4.37/1.37 % (3416711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416711)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416711)Termination reason: Instruction limit
% 4.37/1.37 % (3416711)Termination phase: Saturation
% 4.37/1.37 % (3416711)Time elapsed: 0.112 s
% 4.37/1.37 % (3416711)Peak memory usage: 116 MB
% 4.37/1.37 % (3416711)Instructions burned: 203 (million)
% 4.37/1.37 % (3416724)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=1194767921:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.37/1.37 % (3416725)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4177832723:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.37/1.37 % (3416725)Instruction limit reached!
% 4.37/1.37 % (3416725)------------------------------
% 4.37/1.37 % (3416725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416725)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416725)Termination reason: Instruction limit
% 4.37/1.37 % (3416725)Termination phase: Saturation
% 4.37/1.37 % (3416725)Time elapsed: 0.011 s
% 4.37/1.37 % (3416725)Peak memory usage: 89 MB
% 4.37/1.37 % (3416725)Instructions burned: 17 (million)
% 4.37/1.37 % (3416724)Instruction limit reached!
% 4.37/1.37 % (3416724)------------------------------
% 4.37/1.37 % (3416724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416724)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416724)Termination reason: Instruction limit
% 4.37/1.37 % (3416724)Termination phase: Saturation
% 4.37/1.37 % (3416724)Time elapsed: 0.022 s
% 4.37/1.37 % (3416724)Peak memory usage: 89 MB
% 4.37/1.37 % (3416724)Instructions burned: 30 (million)
% 4.37/1.37 % (3416729)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2354816701:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.37/1.37 % (3416726)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1444705922:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.37/1.37 % (3416727)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=1356234596:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.37/1.37 % (3416710)Instruction limit reached!
% 4.37/1.37 % (3416710)------------------------------
% 4.37/1.37 % (3416710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416710)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416710)Termination reason: Instruction limit
% 4.37/1.37 % (3416710)Termination phase: Saturation
% 4.37/1.37 % (3416710)Time elapsed: 0.214 s
% 4.37/1.37 % (3416710)Peak memory usage: 117 MB
% 4.37/1.37 % (3416710)Instructions burned: 308 (million)
% 4.37/1.37 % (3416726)Instruction limit reached!
% 4.37/1.37 % (3416726)------------------------------
% 4.37/1.37 % (3416726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.37/1.37 % (3416726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.37/1.37 % (3416726)CaDiCaL version: 2.1.3
% 4.37/1.37 % (3416726)Termination reason: Instruction limit
% 4.37/1.37 % (3416726)Termination phase: Saturation
% 4.37/1.37 % (3416726)Time elapsed: 0.016 s
% 4.37/1.37 % (3416726)Peak memory usage: 89 MB
% 4.37/1.37 % (3416726)Instructions burned: 25 (million)
% 4.37/1.37 % (3416727)Instruction limit reached!
% 4.37/1.37 % (3416727)------------------------------
% 4.37/1.37 % (3416727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.53 % (3416727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.53 % (3416727)CaDiCaL version: 2.1.3
% 5.55/1.53 % (3416727)Termination reason: Instruction limit
% 5.55/1.53 % (3416727)Termination phase: Saturation
% 5.55/1.53 % (3416727)Time elapsed: 0.019 s
% 5.55/1.53 % (3416727)Peak memory usage: 89 MB
% 5.55/1.53 % (3416727)Instructions burned: 28 (million)
% 5.55/1.53 % (3416729)Instruction limit reached!
% 5.55/1.53 % (3416729)------------------------------
% 5.55/1.53 % (3416729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.53 % (3416729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.53 % (3416729)CaDiCaL version: 2.1.3
% 5.55/1.53 % (3416729)Termination reason: Instruction limit
% 5.55/1.53 % (3416729)Termination phase: Saturation
% 5.55/1.53 % (3416729)Time elapsed: 0.024 s
% 5.55/1.53 % (3416729)Peak memory usage: 89 MB
% 5.55/1.53 % (3416729)Instructions burned: 86 (million)
% 5.55/1.53 % (3416730)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2517424402:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.55/1.53 % (3416730)Instruction limit reached!
% 5.55/1.53 % (3416730)------------------------------
% 5.55/1.53 % (3416730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.53 % (3416730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.53 % (3416730)CaDiCaL version: 2.1.3
% 5.55/1.53 % (3416730)Termination reason: Instruction limit
% 5.55/1.53 % (3416730)Termination phase: Naming
% 5.55/1.53 % (3416730)Time elapsed: 0.002 s
% 5.55/1.53 % (3416730)Peak memory usage: 86 MB
% 5.55/1.53 % (3416730)Instructions burned: 3 (million)
% 5.55/1.53 % (3416733)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3889377757:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.55/1.53 % (3416740)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=1424350870:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.55/1.53 % (3416737)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2600149470:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.55/1.54 % (3416740)Instruction limit reached!
% 5.55/1.54 % (3416740)------------------------------
% 5.55/1.54 % (3416740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.54 % (3416740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.54 % (3416740)CaDiCaL version: 2.1.3
% 5.55/1.54 % (3416740)Termination reason: Instruction limit
% 5.55/1.54 % (3416740)Termination phase: Saturation
% 5.55/1.54 % (3416740)Time elapsed: 0.003 s
% 5.55/1.54 % (3416740)Peak memory usage: 88 MB
% 5.55/1.54 % (3416740)Instructions burned: 10 (million)
% 5.55/1.54 % (3416737)Instruction limit reached!
% 5.55/1.54 % (3416737)------------------------------
% 5.55/1.54 % (3416737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.54 % (3416737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.54 % (3416737)CaDiCaL version: 2.1.3
% 5.55/1.54 % (3416737)Termination reason: Instruction limit
% 5.55/1.54 % (3416737)Termination phase: Function definition elimination
% 5.55/1.54 % (3416737)Time elapsed: 0.003 s
% 5.55/1.54 % (3416737)Peak memory usage: 86 MB
% 5.55/1.54 % (3416737)Instructions burned: 5 (million)
% 5.55/1.54 % (3416738)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=950101801:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.55/1.54 % (3416741)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3908421910:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.55/1.54 % (3416739)lrs+10_1_thi=all:si=on:fd=off:random_seed=1715904667:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.55/1.54 % (3416741)Instruction limit reached!
% 5.55/1.54 % (3416741)------------------------------
% 5.55/1.54 % (3416741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.55/1.54 % (3416741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.54 % (3416741)CaDiCaL version: 2.1.3
% 5.55/1.54 % (3416741)Termination reason: Instruction limit
% 5.55/1.54 % (3416741)Termination phase: Preprocessing 3
% 5.71/1.63 % (3416741)Time elapsed: 0.002 s
% 5.71/1.63 % (3416741)Peak memory usage: 86 MB
% 5.71/1.63 % (3416741)Instructions burned: 2 (million)
% 5.71/1.63 % (3416743)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1977510278:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 5.71/1.63 % (3416739)Instruction limit reached!
% 5.71/1.63 % (3416739)------------------------------
% 5.71/1.63 % (3416739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416739)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416739)Termination reason: Instruction limit
% 5.71/1.63 % (3416739)Termination phase: Saturation
% 5.71/1.63 % (3416739)Time elapsed: 0.050 s
% 5.71/1.63 % (3416739)Peak memory usage: 115 MB
% 5.71/1.63 % (3416739)Instructions burned: 54 (million)
% 5.71/1.63 % (3416743)Instruction limit reached!
% 5.71/1.63 % (3416743)------------------------------
% 5.71/1.63 % (3416743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416743)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416743)Termination reason: Instruction limit
% 5.71/1.63 % (3416743)Termination phase: Preprocessing 3
% 5.71/1.63 % (3416743)Time elapsed: 0.002 s
% 5.71/1.63 % (3416743)Peak memory usage: 86 MB
% 5.71/1.63 % (3416743)Instructions burned: 3 (million)
% 5.71/1.63 % (3416738)Instruction limit reached!
% 5.71/1.63 % (3416738)------------------------------
% 5.71/1.63 % (3416738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416738)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416738)Termination reason: Instruction limit
% 5.71/1.63 % (3416738)Termination phase: Saturation
% 5.71/1.63 % (3416738)Time elapsed: 0.078 s
% 5.71/1.63 % (3416738)Peak memory usage: 133 MB
% 5.71/1.63 % (3416738)Instructions burned: 67 (million)
% 5.71/1.63 % (3416747)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2424886720:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 5.71/1.63 % (3416733)Instruction limit reached!
% 5.71/1.63 % (3416733)------------------------------
% 5.71/1.63 % (3416733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416733)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416733)Termination reason: Instruction limit
% 5.71/1.63 % (3416733)Termination phase: Saturation
% 5.71/1.63 % (3416733)Time elapsed: 0.122 s
% 5.71/1.63 % (3416733)Peak memory usage: 91 MB
% 5.71/1.63 % (3416733)Instructions burned: 182 (million)
% 5.71/1.63 % (3416748)dis+10_1_si=on:random_seed=3309009666:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 5.71/1.63 % (3416748)Instruction limit reached!
% 5.71/1.63 % (3416748)------------------------------
% 5.71/1.63 % (3416748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416748)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416748)Termination reason: Instruction limit
% 5.71/1.63 % (3416748)Termination phase: Saturation
% 5.71/1.63 % (3416748)Time elapsed: 0.007 s
% 5.71/1.63 % (3416748)Peak memory usage: 88 MB
% 5.71/1.63 % (3416748)Instructions burned: 11 (million)
% 5.71/1.63 % (3416747)Instruction limit reached!
% 5.71/1.63 % (3416747)------------------------------
% 5.71/1.63 % (3416747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416747)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416747)Termination reason: Instruction limit
% 5.71/1.63 % (3416747)Termination phase: Saturation
% 5.71/1.63 % (3416747)Time elapsed: 0.063 s
% 5.71/1.63 % (3416747)Peak memory usage: 117 MB
% 5.71/1.63 % (3416747)Instructions burned: 129 (million)
% 5.71/1.63 % (3416752)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1263059812:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 5.71/1.63 % (3416752)Instruction limit reached!
% 5.71/1.63 % (3416752)------------------------------
% 5.71/1.63 % (3416752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416752)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416752)Termination reason: Instruction limit
% 5.71/1.63 % (3416752)Termination phase: Saturation
% 5.71/1.63 % (3416752)Time elapsed: 0.018 s
% 5.71/1.63 % (3416752)Peak memory usage: 89 MB
% 5.71/1.63 % (3416752)Instructions burned: 26 (million)
% 5.71/1.63 % (3416754)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2428408764:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 5.71/1.63 % (3416755)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1595855717:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 5.71/1.63 % (3416755)Instruction limit reached!
% 5.71/1.63 % (3416755)------------------------------
% 5.71/1.63 % (3416755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416755)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416755)Termination reason: Instruction limit
% 5.71/1.63 % (3416755)Termination phase: Preprocessing 3
% 5.71/1.63 % (3416755)Time elapsed: 0.002 s
% 5.71/1.63 % (3416755)Peak memory usage: 86 MB
% 5.71/1.63 % (3416755)Instructions burned: 3 (million)
% 5.71/1.63 % (3416757)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3536009019:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 5.71/1.63 % (3416757)Instruction limit reached!
% 5.71/1.63 % (3416757)------------------------------
% 5.71/1.63 % (3416757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416757)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416757)Termination reason: Instruction limit
% 5.71/1.63 % (3416757)Termination phase: Saturation
% 5.71/1.63 % (3416757)Time elapsed: 0.006 s
% 5.71/1.63 % (3416757)Peak memory usage: 88 MB
% 5.71/1.63 % (3416757)Instructions burned: 9 (million)
% 5.71/1.63 % (3416754)Instruction limit reached!
% 5.71/1.63 % (3416754)------------------------------
% 5.71/1.63 % (3416754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416754)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416754)Termination reason: Instruction limit
% 5.71/1.63 % (3416754)Termination phase: Saturation
% 5.71/1.63 % (3416754)Time elapsed: 0.026 s
% 5.71/1.63 % (3416754)Peak memory usage: 89 MB
% 5.71/1.63 % (3416754)Instructions burned: 35 (million)
% 5.71/1.63 % (3416758)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2263990786:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 5.71/1.63 % (3416761)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2118930224:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 5.71/1.63 % (3416760)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3327533147:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 5.71/1.63 % (3416761)First to succeed.
% 5.71/1.63 % (3416761)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3416704"
% 5.71/1.63 % (3416760)Instruction limit reached!
% 5.71/1.63 % (3416760)------------------------------
% 5.71/1.63 % (3416760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416760)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416760)Termination reason: Instruction limit
% 5.71/1.63 % (3416760)Termination phase: Saturation
% 5.71/1.63 % (3416760)Time elapsed: 0.029 s
% 5.71/1.63 % (3416760)Peak memory usage: 112 MB
% 5.71/1.63 % (3416760)Instructions burned: 14 (million)
% 5.71/1.63 % (3416767)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2589009983:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 5.71/1.63 % (3416763)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3466978238:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 5.71/1.63 % (3416763)Instruction limit reached!
% 5.71/1.63 % (3416763)------------------------------
% 5.71/1.63 % (3416763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416763)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416763)Termination reason: Instruction limit
% 5.71/1.63 % (3416763)Termination phase: Saturation
% 5.71/1.63 % (3416763)Time elapsed: 0.007 s
% 5.71/1.63 % (3416763)Peak memory usage: 88 MB
% 5.71/1.63 % (3416763)Instructions burned: 10 (million)
% 5.71/1.63 % (3416768)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=2393152782:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 5.71/1.63 % (3416771)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=3782375231:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 5.71/1.63 % (3416768)Instruction limit reached!
% 5.71/1.63 % (3416768)------------------------------
% 5.71/1.63 % (3416768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416768)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416768)Termination reason: Instruction limit
% 5.71/1.63 % (3416768)Termination phase: Saturation
% 5.71/1.63 % (3416768)Time elapsed: 0.037 s
% 5.71/1.63 % (3416768)Peak memory usage: 89 MB
% 5.71/1.63 % (3416768)Instructions burned: 75 (million)
% 5.71/1.63 % (3416767)Instruction limit reached!
% 5.71/1.63 % (3416767)------------------------------
% 5.71/1.63 % (3416767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416767)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416767)Termination reason: Instruction limit
% 5.71/1.63 % (3416767)Termination phase: Saturation
% 5.71/1.63 % (3416767)Time elapsed: 0.082 s
% 5.71/1.63 % (3416767)Peak memory usage: 133 MB
% 5.71/1.63 % (3416767)Instructions burned: 71 (million)
% 5.71/1.63 % (3416758)Instruction limit reached!
% 5.71/1.63 % (3416758)------------------------------
% 5.71/1.63 % (3416758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.71/1.63 % (3416758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.63 % (3416758)CaDiCaL version: 2.1.3
% 5.71/1.63 % (3416758)Termination reason: Instruction limit
% 5.71/1.63 % (3416758)Termination phase: Saturation
% 5.71/1.63 % (3416758)Time elapsed: 0.212 s
% 5.71/1.63 % (3416758)Peak memory usage: 92 MB
% 5.71/1.63 % (3416758)Instructions burned: 371 (million)
% 5.71/1.63 % (3416761)Refutation found. Thanks to Tanya!
% 5.71/1.63 % SZS status Theorem for theBenchmark
% 5.71/1.63 % SZS output start Proof for theBenchmark
% See solution above
% 7.46/1.82 % (3416761)------------------------------
% 7.46/1.82 % (3416761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.82 % (3416761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.82 % (3416761)CaDiCaL version: 2.1.3
% 7.46/1.82 % (3416761)Termination reason: Refutation
% 7.46/1.82 % (3416761)Time elapsed: 0.051 s
% 7.46/1.82 % (3416761)Peak memory usage: 118 MB
% 7.46/1.82 % (3416761)Instructions burned: 101 (million)
% 7.46/1.82 % (3416761)------------------------------
% 7.46/1.82 % (3416761)------------------------------
% 7.46/1.82 % (3416704)Success in time 0.967 s
% 7.46/1.82 % Vampire exiting
%------------------------------------------------------------------------------