%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW616_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 : n018.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:57 PM UTC 2026
% Result : Theorem 4.69s 1.74s
% Output : Refutation 0.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 10
% Syntax : Number of formulae : 47 ( 32 unt; 0 typ; 8 def)
% Number of atoms : 259 ( 79 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 331 ( 119 ~; 28 |; 136 &)
% ( 0 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 881 ( 179 atm; 418 fun; 184 num; 100 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 : 7 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 68 ( 62 usr; 36 con; 0-5 aty)
% Number of variables : 107 ( 71 !; 36 ?; 107 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
abs: $int > $int ).
tff(func_def_17,type,
div: ( $int * $int ) > $int ).
tff(func_def_18,type,
mod: ( $int * $int ) > $int ).
tff(func_def_21,type,
map: ( ty * ty ) > ty ).
tff(func_def_22,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_23,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_24,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_25,type,
array: ty > ty ).
tff(func_def_26,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_27,type,
length: ( ty * uni ) > $int ).
tff(func_def_28,type,
elts: ( ty * uni ) > uni ).
tff(func_def_29,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_30,type,
t2tb: $int > uni ).
tff(func_def_31,type,
tb2t: uni > $int ).
tff(func_def_32,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_33,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_34,type,
sum: ( map_int_int * $int * $int ) > $int ).
tff(func_def_35,type,
t2tb1: map_int_int > uni ).
tff(func_def_36,type,
tb2t1: uni > map_int_int ).
tff(func_def_38,type,
sum1: ( array_int * $int * $int ) > $int ).
tff(func_def_39,type,
t2tb2: array_int > uni ).
tff(func_def_40,type,
tb2t2: uni > array_int ).
tff(func_def_42,type,
sK0: $int ).
tff(func_def_43,type,
sK1: map_int_int ).
tff(func_def_44,type,
sK2: $int ).
tff(func_def_45,type,
sK3: $int ).
tff(func_def_46,type,
sK4: $int ).
tff(func_def_47,type,
sK5: $int ).
tff(func_def_48,type,
sK6: $int ).
tff(func_def_49,type,
sK7: $int ).
tff(func_def_50,type,
sK8: $int ).
tff(func_def_51,type,
sK9: $int ).
tff(func_def_52,type,
sK10: $int ).
tff(func_def_53,type,
sK11: $int ).
tff(func_def_54,type,
sK12: ( map_int_int * map_int_int * $int * $int ) > $int ).
tff(func_def_55,type,
sF13: $int ).
tff(func_def_56,type,
sF14: $int ).
tff(func_def_57,type,
sF15: $int ).
tff(func_def_58,type,
sF16: $int ).
tff(func_def_59,type,
sF17: $int ).
tff(func_def_60,type,
sF18: $int > $int ).
tff(func_def_61,type,
sF19: $int ).
tff(func_def_62,type,
sF20: $int ).
tff(func_def_63,type,
sF21: $int ).
tff(func_def_64,type,
sF22: $int ).
tff(func_def_65,type,
sF23: $int ).
tff(func_def_66,type,
sF24: $int ).
tff(func_def_67,type,
sF25: $int ).
tff(func_def_68,type,
sF26: $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_4,type,
maxsublo: ( array_int * $int * $int ) > $o ).
tff(pred_def_5,type,
maxsub: ( array_int * $int ) > $o ).
tff(f64,conjecture,
! [X1: map_int_int,X2: $int,X3: $int,X0: $int] :
( ( $lesseq(X2,X3)
& $lesseq(0,X0)
& $lesseq(0,X2)
& $lesseq(X3,X0) )
=> ( ( X3 != X2 )
=> ! [X4: $int] :
( ( X4 = $sum(X2,div($difference(X3,X2),2)) )
=> ! [X5: $int] :
( ( X5 = $sum(X2,div($difference(X3,X2),2)) )
=> ( $lesseq(X2,$difference($sum(X2,div($difference(X3,X2),2)),1))
=> ! [X7: $int,X8: $int,X6: $int] :
( ( ! [X9: $int] :
( ( $less($difference(X2,1),X9)
& $lesseq(X9,$sum(X2,div($difference(X3,X2),2))) )
=> $lesseq(sum(X1,X9,$sum(X2,div($difference(X3,X2),2))),X7) )
& ( X6 = sum(X1,$sum($difference(X2,1),1),$sum(X2,div($difference(X3,X2),2))) )
& ( X7 = sum(X1,X8,X5) )
& $lesseq(X8,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X8)
& ( $sum(X2,div($difference(X3,X2),2)) = X5 ) )
=> ( ! [X9: $int] :
( ( $lesseq(X9,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X9) )
=> $lesseq(sum(X1,X9,$sum(X2,div($difference(X3,X2),2))),sum(X1,X8,$sum(X2,div($difference(X3,X2),2)))) )
=> ! [X10: $int] :
( ( X10 = X7 )
=> ( $lesseq($sum(X2,div($difference(X3,X2),2)),$difference(X3,1))
=> ! [X11: $int,X9: $int] :
( ( $lesseq(X9,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X9)
& $lesseq($sum(X2,div($difference(X3,X2),2)),X11)
& $lesseq(X11,$sum(X2,div($difference(X3,X2),2))) )
=> $lesseq(sum(X1,X9,X11),X7) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_maximum_subarray_rec) ).
tff(f65,negated_conjecture,
~ ! [X1: map_int_int,X2: $int,X3: $int,X0: $int] :
( ( $lesseq(X2,X3)
& $lesseq(0,X0)
& $lesseq(0,X2)
& $lesseq(X3,X0) )
=> ( ( X3 != X2 )
=> ! [X4: $int] :
( ( X4 = $sum(X2,div($difference(X3,X2),2)) )
=> ! [X5: $int] :
( ( X5 = $sum(X2,div($difference(X3,X2),2)) )
=> ( $lesseq(X2,$difference($sum(X2,div($difference(X3,X2),2)),1))
=> ! [X7: $int,X8: $int,X6: $int] :
( ( ! [X9: $int] :
( ( $less($difference(X2,1),X9)
& $lesseq(X9,$sum(X2,div($difference(X3,X2),2))) )
=> $lesseq(sum(X1,X9,$sum(X2,div($difference(X3,X2),2))),X7) )
& ( X6 = sum(X1,$sum($difference(X2,1),1),$sum(X2,div($difference(X3,X2),2))) )
& ( X7 = sum(X1,X8,X5) )
& $lesseq(X8,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X8)
& ( $sum(X2,div($difference(X3,X2),2)) = X5 ) )
=> ( ! [X9: $int] :
( ( $lesseq(X9,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X9) )
=> $lesseq(sum(X1,X9,$sum(X2,div($difference(X3,X2),2))),sum(X1,X8,$sum(X2,div($difference(X3,X2),2)))) )
=> ! [X10: $int] :
( ( X10 = X7 )
=> ( $lesseq($sum(X2,div($difference(X3,X2),2)),$difference(X3,1))
=> ! [X11: $int,X9: $int] :
( ( $lesseq(X9,$sum(X2,div($difference(X3,X2),2)))
& $lesseq(X2,X9)
& $lesseq($sum(X2,div($difference(X3,X2),2)),X11)
& $lesseq(X11,$sum(X2,div($difference(X3,X2),2))) )
=> $lesseq(sum(X1,X9,X11),X7) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f64]) ).
tff(f79,plain,
~ ! [X1: map_int_int,X2: $int,X3: $int,X0: $int] :
( ( ~ $less(X3,X2)
& ~ $less(X0,0)
& ~ $less(X2,0)
& ~ $less(X0,X3) )
=> ( ( X3 != X2 )
=> ! [X4: $int] :
( ( $sum(X2,div($sum(X3,$uminus(X2)),2)) = X4 )
=> ! [X5: $int] :
( ( $sum(X2,div($sum(X3,$uminus(X2)),2)) = X5 )
=> ( ~ $less($sum($sum(X2,div($sum(X3,$uminus(X2)),2)),$uminus(1)),X2)
=> ! [X7: $int,X8: $int,X6: $int] :
( ( ! [X9: $int] :
( ( $less($sum(X2,$uminus(1)),X9)
& ~ $less($sum(X2,div($sum(X3,$uminus(X2)),2)),X9) )
=> ~ $less(X7,sum(X1,X9,$sum(X2,div($sum(X3,$uminus(X2)),2)))) )
& ( sum(X1,$sum($sum(X2,$uminus(1)),1),$sum(X2,div($sum(X3,$uminus(X2)),2))) = X6 )
& ( X7 = sum(X1,X8,X5) )
& ~ $less($sum(X2,div($sum(X3,$uminus(X2)),2)),X8)
& ~ $less(X8,X2)
& ( $sum(X2,div($sum(X3,$uminus(X2)),2)) = X5 ) )
=> ( ! [X9: $int] :
( ( ~ $less($sum(X2,div($sum(X3,$uminus(X2)),2)),X9)
& ~ $less(X9,X2) )
=> ~ $less(sum(X1,X8,$sum(X2,div($sum(X3,$uminus(X2)),2))),sum(X1,X9,$sum(X2,div($sum(X3,$uminus(X2)),2)))) )
=> ! [X10: $int] :
( ( X10 = X7 )
=> ( ~ $less($sum(X3,$uminus(1)),$sum(X2,div($sum(X3,$uminus(X2)),2)))
=> ! [X11: $int,X9: $int] :
( ( ~ $less($sum(X2,div($sum(X3,$uminus(X2)),2)),X9)
& ~ $less(X9,X2)
& ~ $less(X11,$sum(X2,div($sum(X3,$uminus(X2)),2)))
& ~ $less($sum(X2,div($sum(X3,$uminus(X2)),2)),X11) )
=> ~ $less(X7,sum(X1,X9,X11)) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f65]) ).
tff(f94,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,X0)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f132,plain,
~ ! [X3: $int,X2: $int,X1: $int,X0: map_int_int] :
( ( ~ $less(X3,0)
& ~ $less(X2,X1)
& ~ $less(X3,X2)
& ~ $less(X1,0) )
=> ( ( X1 != X2 )
=> ! [X4: $int] :
( ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X4 )
=> ! [X5: $int] :
( ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 )
=> ( ~ $less($sum($sum(X1,div($sum(X2,$uminus(X1)),2)),$uminus(1)),X1)
=> ! [X6: $int,X8: $int,X7: $int] :
( ( ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 )
& ( sum(X0,$sum($sum(X1,$uminus(1)),1),$sum(X1,div($sum(X2,$uminus(X1)),2))) = X8 )
& ! [X9: $int] :
( ( $less($sum(X1,$uminus(1)),X9)
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X9) )
=> ~ $less(X6,sum(X0,X9,$sum(X1,div($sum(X2,$uminus(X1)),2)))) )
& ~ $less(X7,X1)
& ( sum(X0,X7,X5) = X6 )
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X7) )
=> ( ! [X10: $int] :
( ( ~ $less(X10,X1)
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X10) )
=> ~ $less(sum(X0,X7,$sum(X1,div($sum(X2,$uminus(X1)),2))),sum(X0,X10,$sum(X1,div($sum(X2,$uminus(X1)),2)))) )
=> ! [X11: $int] :
( ( X6 = X11 )
=> ( ~ $less($sum(X2,$uminus(1)),$sum(X1,div($sum(X2,$uminus(X1)),2)))
=> ! [X13: $int,X12: $int] :
( ( ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X13)
& ~ $less(X13,X1)
& ~ $less(X12,$sum(X1,div($sum(X2,$uminus(X1)),2)))
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X12) )
=> ~ $less(X6,sum(X0,X13,X12)) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f79]) ).
tff(f152,plain,
? [X3: $int,X2: $int,X1: $int,X0: map_int_int] :
( ? [X4: $int] :
( ? [X5: $int] :
( ? [X6: $int,X8: $int,X7: $int] :
( ? [X11: $int] :
( ? [X13: $int,X12: $int] :
( $less(X6,sum(X0,X13,X12))
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X13)
& ~ $less(X13,X1)
& ~ $less(X12,$sum(X1,div($sum(X2,$uminus(X1)),2)))
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X12) )
& ~ $less($sum(X2,$uminus(1)),$sum(X1,div($sum(X2,$uminus(X1)),2)))
& ( X6 = X11 ) )
& ! [X10: $int] :
( ~ $less(sum(X0,X7,$sum(X1,div($sum(X2,$uminus(X1)),2))),sum(X0,X10,$sum(X1,div($sum(X2,$uminus(X1)),2))))
| $less(X10,X1)
| $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X10) )
& ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 )
& ( sum(X0,$sum($sum(X1,$uminus(1)),1),$sum(X1,div($sum(X2,$uminus(X1)),2))) = X8 )
& ! [X9: $int] :
( ~ $less(X6,sum(X0,X9,$sum(X1,div($sum(X2,$uminus(X1)),2))))
| ~ $less($sum(X1,$uminus(1)),X9)
| $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X9) )
& ~ $less(X7,X1)
& ( sum(X0,X7,X5) = X6 )
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X7) )
& ~ $less($sum($sum(X1,div($sum(X2,$uminus(X1)),2)),$uminus(1)),X1)
& ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 ) )
& ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X4 ) )
& ( X1 != X2 )
& ~ $less(X3,0)
& ~ $less(X2,X1)
& ~ $less(X3,X2)
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f132]) ).
tff(f153,plain,
? [X2: $int,X0: map_int_int,X3: $int,X1: $int] :
( ~ $less(X3,0)
& ( X1 != X2 )
& ? [X4: $int] :
( ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X4 )
& ? [X5: $int] :
( ? [X6: $int,X7: $int,X8: $int] :
( ( sum(X0,X7,X5) = X6 )
& ! [X9: $int] :
( ~ $less(X6,sum(X0,X9,$sum(X1,div($sum(X2,$uminus(X1)),2))))
| ~ $less($sum(X1,$uminus(1)),X9)
| $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X9) )
& ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 )
& ! [X10: $int] :
( $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X10)
| ~ $less(sum(X0,X7,$sum(X1,div($sum(X2,$uminus(X1)),2))),sum(X0,X10,$sum(X1,div($sum(X2,$uminus(X1)),2))))
| $less(X10,X1) )
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X7)
& ( sum(X0,$sum($sum(X1,$uminus(1)),1),$sum(X1,div($sum(X2,$uminus(X1)),2))) = X8 )
& ~ $less(X7,X1)
& ? [X11: $int] :
( ( X6 = X11 )
& ~ $less($sum(X2,$uminus(1)),$sum(X1,div($sum(X2,$uminus(X1)),2)))
& ? [X12: $int,X13: $int] :
( $less(X6,sum(X0,X13,X12))
& ~ $less(X13,X1)
& ~ $less(X12,$sum(X1,div($sum(X2,$uminus(X1)),2)))
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X13)
& ~ $less($sum(X1,div($sum(X2,$uminus(X1)),2)),X12) ) ) )
& ( $sum(X1,div($sum(X2,$uminus(X1)),2)) = X5 )
& ~ $less($sum($sum(X1,div($sum(X2,$uminus(X1)),2)),$uminus(1)),X1) ) )
& ~ $less(X1,0)
& ~ $less(X2,X1)
& ~ $less(X3,X2) ),
inference(flattening,[],[f152]) ).
tff(f189,plain,
? [X0: $int,X1: map_int_int,X2: $int,X3: $int] :
( ~ $less(X2,0)
& ( X0 != X3 )
& ? [X4: $int] :
( ( $sum(X3,div($sum(X0,$uminus(X3)),2)) = X4 )
& ? [X5: $int] :
( ? [X6: $int,X7: $int,X8: $int] :
( ( sum(X1,X7,X5) = X6 )
& ! [X9: $int] :
( ~ $less(X6,sum(X1,X9,$sum(X3,div($sum(X0,$uminus(X3)),2))))
| ~ $less($sum(X3,$uminus(1)),X9)
| $less($sum(X3,div($sum(X0,$uminus(X3)),2)),X9) )
& ( $sum(X3,div($sum(X0,$uminus(X3)),2)) = X5 )
& ! [X10: $int] :
( $less($sum(X3,div($sum(X0,$uminus(X3)),2)),X10)
| ~ $less(sum(X1,X7,$sum(X3,div($sum(X0,$uminus(X3)),2))),sum(X1,X10,$sum(X3,div($sum(X0,$uminus(X3)),2))))
| $less(X10,X3) )
& ~ $less($sum(X3,div($sum(X0,$uminus(X3)),2)),X7)
& ( sum(X1,$sum($sum(X3,$uminus(1)),1),$sum(X3,div($sum(X0,$uminus(X3)),2))) = X8 )
& ~ $less(X7,X3)
& ? [X11: $int] :
( ( X6 = X11 )
& ~ $less($sum(X0,$uminus(1)),$sum(X3,div($sum(X0,$uminus(X3)),2)))
& ? [X12: $int,X13: $int] :
( $less(X6,sum(X1,X13,X12))
& ~ $less(X13,X3)
& ~ $less(X12,$sum(X3,div($sum(X0,$uminus(X3)),2)))
& ~ $less($sum(X3,div($sum(X0,$uminus(X3)),2)),X13)
& ~ $less($sum(X3,div($sum(X0,$uminus(X3)),2)),X12) ) ) )
& ( $sum(X3,div($sum(X0,$uminus(X3)),2)) = X5 )
& ~ $less($sum($sum(X3,div($sum(X0,$uminus(X3)),2)),$uminus(1)),X3) ) )
& ~ $less(X3,0)
& ~ $less(X0,X3)
& ~ $less(X2,X0) ),
inference(rectify,[],[f153]) ).
tff(f190,plain,
( ~ $less(sK2,0)
& ( sK0 != sK3 )
& ( sK4 = $sum(sK3,div($sum(sK0,$uminus(sK3)),2)) )
& ( sum(sK1,sK7,sK5) = sK6 )
& ! [X9: $int] :
( ~ $less(sK6,sum(sK1,X9,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))))
| ~ $less($sum(sK3,$uminus(1)),X9)
| $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),X9) )
& ( sK5 = $sum(sK3,div($sum(sK0,$uminus(sK3)),2)) )
& ! [X10: $int] :
( $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),X10)
| ~ $less(sum(sK1,sK7,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))),sum(sK1,X10,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))))
| $less(X10,sK3) )
& ~ $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),sK7)
& ( sum(sK1,$sum($sum(sK3,$uminus(1)),1),$sum(sK3,div($sum(sK0,$uminus(sK3)),2))) = sK8 )
& ~ $less(sK7,sK3)
& ( sK6 = sK9 )
& ~ $less($sum(sK0,$uminus(1)),$sum(sK3,div($sum(sK0,$uminus(sK3)),2)))
& $less(sK6,sum(sK1,sK11,sK10))
& ~ $less(sK11,sK3)
& ~ $less(sK10,$sum(sK3,div($sum(sK0,$uminus(sK3)),2)))
& ~ $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),sK11)
& ~ $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),sK10)
& ( sK5 = $sum(sK3,div($sum(sK0,$uminus(sK3)),2)) )
& ~ $less($sum($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),$uminus(1)),sK3)
& ~ $less(sK3,0)
& ~ $less(sK0,sK3)
& ~ $less(sK2,sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X11,sK9),skolemize(X12,sK10),skolemize(X13,sK11)],[f189]) ).
tff(f231,plain,
~ $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),sK10),
inference(cnf_transformation,[],[f190]) ).
tff(f232,plain,
~ $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),sK11),
inference(cnf_transformation,[],[f190]) ).
tff(f233,plain,
~ $less(sK10,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))),
inference(cnf_transformation,[],[f190]) ).
tff(f234,plain,
~ $less(sK11,sK3),
inference(cnf_transformation,[],[f190]) ).
tff(f235,plain,
$less(sK6,sum(sK1,sK11,sK10)),
inference(cnf_transformation,[],[f190]) ).
tff(f241,plain,
! [X10: $int] :
( $less($sum(sK3,div($sum(sK0,$uminus(sK3)),2)),X10)
| ~ $less(sum(sK1,sK7,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))),sum(sK1,X10,$sum(sK3,div($sum(sK0,$uminus(sK3)),2))))
| $less(X10,sK3) ),
inference(cnf_transformation,[],[f190]) ).
tff(f242,plain,
sK5 = $sum(sK3,div($sum(sK0,$uminus(sK3)),2)),
inference(cnf_transformation,[],[f190]) ).
tff(f244,plain,
sum(sK1,sK7,sK5) = sK6,
inference(cnf_transformation,[],[f190]) ).
tff(f311,definition,
sF13 = $uminus(sK3),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f312,definition,
sF14 = $sum(sK0,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f313,definition,
sF15 = div(sF14,2),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f314,definition,
sF16 = $sum(sK3,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f316,definition,
sF17 = sum(sK1,sK7,sK5),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f317,plain,
sum(sK1,sK7,sK5) = sF17,
inference(reorient_equations,[],[f316]) ).
tff(f318,plain,
sF17 = sK6,
inference(definition_folding,[],[f244,f317]) ).
tff(f319,definition,
! [X9: $int] : ( sF18(X9) = sum(sK1,X9,sF16) ),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f320,plain,
! [X9: $int] : ( sum(sK1,X9,sF16) = sF18(X9) ),
inference(reorient_equations,[],[f319]) ).
tff(f326,plain,
sF16 = sK5,
inference(definition_folding,[],[f242,f314,f313,f312,f311]) ).
tff(f327,definition,
sF21 = sum(sK1,sK7,sF16),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f328,plain,
! [X10: $int] :
( ~ $less(sF21,sF18(X10))
| $less(X10,sK3)
| $less(sF16,X10) ),
inference(definition_folding,[],[f241,f320,f314,f313,f312,f311,f327,f314,f313,f312,f311,f314,f313,f312,f311]) ).
tff(f337,definition,
sF25 = sum(sK1,sK11,sK10),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f338,plain,
sum(sK1,sK11,sK10) = sF25,
inference(reorient_equations,[],[f337]) ).
tff(f339,plain,
$less(sK6,sF25),
inference(definition_folding,[],[f235,f338]) ).
tff(f340,plain,
~ $less(sK10,sF16),
inference(definition_folding,[],[f233,f314,f313,f312,f311]) ).
tff(f341,plain,
~ $less(sF16,sK11),
inference(definition_folding,[],[f232,f314,f313,f312,f311]) ).
tff(f342,plain,
~ $less(sF16,sK10),
inference(definition_folding,[],[f231,f314,f313,f312,f311]) ).
tff(f354,plain,
sum(sK1,sK7,sK5) = sK6,
inference(forward_demodulation,[],[f317,f318]) ).
tff(f355,plain,
sK6 = sum(sK1,sK7,sF16),
inference(forward_demodulation,[],[f354,f326]) ).
tff(f356,plain,
sF21 = sK6,
inference(forward_demodulation,[],[f327,f355]) ).
tff(f357,plain,
! [X0: $int] :
( ~ $less(sK6,sF18(X0))
| $less(X0,sK3)
| $less(sF16,X0) ),
inference(superposition,[],[f328,f356]) ).
tff(f418,plain,
( $less(sK10,sF16)
| ( sK10 = sF16 ) ),
inference(resolution,[],[f94,f342]) ).
tff(f423,plain,
sK10 = sF16,
inference(forward_subsumption_resolution,[],[f418,f340]) ).
tff(f432,plain,
sum(sK1,sK11,sF16) = sF25,
inference(superposition,[],[f338,f423]) ).
tff(f435,plain,
sF18(sK11) = sF25,
inference(forward_demodulation,[],[f432,f320]) ).
tff(f472,plain,
( $less(sK11,sK3)
| $less(sF16,sK11)
| ~ $less(sK6,sF25) ),
inference(superposition,[],[f357,f435]) ).
tff(f477,plain,
( ~ $less(sK6,sF25)
| $less(sF16,sK11) ),
inference(forward_subsumption_resolution,[],[f472,f234]) ).
tff(f480,plain,
$less(sF16,sK11),
inference(forward_subsumption_resolution,[],[f477,f339]) ).
tff(f482,plain,
$false,
inference(forward_subsumption_resolution,[],[f480,f341]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW616_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 % Computer : n018.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 14:24:58 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.28 Running first-order theorem proving
% 0.11/0.28 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
% 4.69/1.71 % (3420038)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.69/1.71 % (3420056)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3337206920:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.69/1.71 % (3420061)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2806199654:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.69/1.71 % (3420059)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1043699467:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.69/1.71 % (3420055)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2449171333:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.69/1.71 % (3420058)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=189872456:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.69/1.71 % (3420057)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2318642388:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.69/1.71 % (3420059)Instruction limit reached!
% 4.69/1.71 % (3420059)------------------------------
% 4.69/1.71 % (3420059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.71 % (3420059)CaDiCaL version: 2.1.3
% 4.69/1.71 % (3420059)Termination reason: Instruction limit
% 4.69/1.71 % (3420059)Termination phase: Property scanning
% 4.69/1.71 % (3420059)Time elapsed: 0.005 s
% 4.69/1.71 % (3420059)Peak memory usage: 87 MB
% 4.69/1.71 % (3420059)Instructions burned: 5 (million)
% 4.69/1.71 % (3420058)Instruction limit reached!
% 4.69/1.71 % (3420058)------------------------------
% 4.69/1.71 % (3420058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.71 % (3420058)CaDiCaL version: 2.1.3
% 4.69/1.71 % (3420058)Termination reason: Instruction limit
% 4.69/1.71 % (3420058)Termination phase: Saturation
% 4.69/1.71 % (3420058)Time elapsed: 0.009 s
% 4.69/1.71 % (3420058)Peak memory usage: 88 MB
% 4.69/1.71 % (3420058)Instructions burned: 7 (million)
% 4.69/1.71 % (3420060)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3183364745:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.69/1.71 % (3420061)Instruction limit reached!
% 4.69/1.71 % (3420061)------------------------------
% 4.69/1.71 % (3420061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.71 % (3420061)CaDiCaL version: 2.1.3
% 4.69/1.71 % (3420061)Termination reason: Instruction limit
% 4.69/1.71 % (3420061)Termination phase: Saturation
% 4.69/1.71 % (3420061)Time elapsed: 0.069 s
% 4.69/1.71 % (3420061)Peak memory usage: 116 MB
% 4.69/1.71 % (3420061)Instructions burned: 35 (million)
% 4.69/1.71 % (3420055)Instruction limit reached!
% 4.69/1.71 % (3420055)------------------------------
% 4.69/1.71 % (3420055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.71 % (3420055)CaDiCaL version: 2.1.3
% 4.69/1.71 % (3420055)Termination reason: Instruction limit
% 4.69/1.71 % (3420055)Termination phase: Saturation
% 4.69/1.71 % (3420055)Time elapsed: 0.041 s
% 4.69/1.71 % (3420055)Peak memory usage: 112 MB
% 4.69/1.71 % (3420055)Instructions burned: 13 (million)
% 4.69/1.71 % (3420060)Instruction limit reached!
% 4.69/1.71 % (3420060)------------------------------
% 4.69/1.71 % (3420060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.71 % (3420060)CaDiCaL version: 2.1.3
% 4.69/1.71 % (3420060)Termination reason: Instruction limit
% 4.69/1.71 % (3420060)Termination phase: Saturation
% 4.69/1.71 % (3420060)Time elapsed: 0.082 s
% 4.69/1.71 % (3420060)Peak memory usage: 116 MB
% 4.69/1.71 % (3420060)Instructions burned: 46 (million)
% 4.69/1.71 % (3420056)Instruction limit reached!
% 4.69/1.71 % (3420056)------------------------------
% 4.69/1.71 % (3420056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.71 % (3420056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420056)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420056)Termination reason: Instruction limit
% 4.69/1.74 % (3420056)Termination phase: Saturation
% 4.69/1.74 % (3420056)Time elapsed: 0.195 s
% 4.69/1.74 % (3420056)Peak memory usage: 117 MB
% 4.69/1.74 % (3420056)Instructions burned: 308 (million)
% 4.69/1.74 % (3420071)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2256175320:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.69/1.74 % (3420071)Instruction limit reached!
% 4.69/1.74 % (3420071)------------------------------
% 4.69/1.74 % (3420071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420071)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420071)Termination reason: Instruction limit
% 4.69/1.74 % (3420071)Termination phase: Saturation
% 4.69/1.74 % (3420071)Time elapsed: 0.017 s
% 4.69/1.74 % (3420071)Peak memory usage: 89 MB
% 4.69/1.74 % (3420071)Instructions burned: 16 (million)
% 4.69/1.74 % (3420068)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=708618179:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 4.69/1.74 % (3420070)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=2474351328:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 4.69/1.74 % (3420068)Instruction limit reached!
% 4.69/1.74 % (3420068)------------------------------
% 4.69/1.74 % (3420068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420068)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420068)Termination reason: Instruction limit
% 4.69/1.74 % (3420068)Termination phase: Saturation
% 4.69/1.74 % (3420068)Time elapsed: 0.018 s
% 4.69/1.74 % (3420068)Peak memory usage: 88 MB
% 4.69/1.74 % (3420068)Instructions burned: 14 (million)
% 4.69/1.74 % (3420070)First to succeed.
% 4.69/1.74 % (3420070)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3420038"
% 4.69/1.74 % (3420072)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3763933297:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.69/1.74 % (3420057)Instruction limit reached!
% 4.69/1.74 % (3420057)------------------------------
% 4.69/1.74 % (3420057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420057)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420057)Termination reason: Instruction limit
% 4.69/1.74 % (3420057)Termination phase: Saturation
% 4.69/1.74 % (3420057)Time elapsed: 0.260 s
% 4.69/1.74 % (3420057)Peak memory usage: 118 MB
% 4.69/1.74 % (3420057)Instructions burned: 201 (million)
% 4.69/1.74 % (3420074)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2478030541:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 4.69/1.74 % (3420072)Instruction limit reached!
% 4.69/1.74 % (3420072)------------------------------
% 4.69/1.74 % (3420072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420072)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420072)Termination reason: Instruction limit
% 4.69/1.74 % (3420072)Termination phase: Saturation
% 4.69/1.74 % (3420072)Time elapsed: 0.028 s
% 4.69/1.74 % (3420072)Peak memory usage: 89 MB
% 4.69/1.74 % (3420072)Instructions burned: 24 (million)
% 4.69/1.74 % (3420074)Instruction limit reached!
% 4.69/1.74 % (3420074)------------------------------
% 4.69/1.74 % (3420074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420074)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420074)Termination reason: Instruction limit
% 4.69/1.74 % (3420074)Termination phase: Saturation
% 4.69/1.74 % (3420074)Time elapsed: 0.042 s
% 4.69/1.74 % (3420074)Peak memory usage: 89 MB
% 4.69/1.74 % (3420074)Instructions burned: 86 (million)
% 4.69/1.74 % (3420073)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=947136444:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 4.69/1.74 % (3420073)Instruction limit reached!
% 4.69/1.74 % (3420073)------------------------------
% 4.69/1.74 % (3420073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420073)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420073)Termination reason: Instruction limit
% 4.69/1.74 % (3420073)Termination phase: Saturation
% 4.69/1.74 % (3420073)Time elapsed: 0.029 s
% 4.69/1.74 % (3420073)Peak memory usage: 89 MB
% 4.69/1.74 % (3420073)Instructions burned: 27 (million)
% 4.69/1.74 % (3420077)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2848569803:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 4.69/1.74 % (3420077)Instruction limit reached!
% 4.69/1.74 % (3420077)------------------------------
% 4.69/1.74 % (3420077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420077)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420077)Termination reason: Instruction limit
% 4.69/1.74 % (3420077)Termination phase: Unused predicate definition removal
% 4.69/1.74 % (3420077)Time elapsed: 0.003 s
% 4.69/1.74 % (3420077)Peak memory usage: 85 MB
% 4.69/1.74 % (3420077)Instructions burned: 2 (million)
% 4.69/1.74 % (3420079)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=912275203:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 4.69/1.74 % (3420085)lrs+10_1_thi=all:si=on:fd=off:random_seed=184512129:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 4.69/1.74 % (3420082)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2677938988:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 4.69/1.74 % (3420082)Instruction limit reached!
% 4.69/1.74 % (3420082)------------------------------
% 4.69/1.74 % (3420082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420082)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420082)Termination reason: Instruction limit
% 4.69/1.74 % (3420082)Termination phase: Property scanning
% 4.69/1.74 % (3420082)Time elapsed: 0.006 s
% 4.69/1.74 % (3420082)Peak memory usage: 86 MB
% 4.69/1.74 % (3420082)Instructions burned: 5 (million)
% 4.69/1.74 % (3420086)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=2790716047:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 4.69/1.74 % (3420083)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2392844616:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 4.69/1.74 % (3420086)Instruction limit reached!
% 4.69/1.74 % (3420086)------------------------------
% 4.69/1.74 % (3420086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420086)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420086)Termination reason: Instruction limit
% 4.69/1.74 % (3420086)Termination phase: Property scanning
% 4.69/1.74 % (3420086)Time elapsed: 0.009 s
% 4.69/1.74 % (3420086)Peak memory usage: 87 MB
% 4.69/1.74 % (3420086)Instructions burned: 8 (million)
% 4.69/1.74 % (3420085)Instruction limit reached!
% 4.69/1.74 % (3420085)------------------------------
% 4.69/1.74 % (3420085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420085)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420085)Termination reason: Instruction limit
% 4.69/1.74 % (3420085)Termination phase: Saturation
% 4.69/1.74 % (3420085)Time elapsed: 0.052 s
% 4.69/1.74 % (3420085)Peak memory usage: 116 MB
% 4.69/1.74 % (3420085)Instructions burned: 56 (million)
% 4.69/1.74 % (3420079)Instruction limit reached!
% 4.69/1.74 % (3420079)------------------------------
% 4.69/1.74 % (3420079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420079)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420079)Termination reason: Instruction limit
% 4.69/1.74 % (3420079)Termination phase: Saturation
% 4.69/1.74 % (3420079)Time elapsed: 0.185 s
% 4.69/1.74 % (3420079)Peak memory usage: 90 MB
% 4.69/1.74 % (3420079)Instructions burned: 182 (million)
% 4.69/1.74 % (3420083)Instruction limit reached!
% 4.69/1.74 % (3420083)------------------------------
% 4.69/1.74 % (3420083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420083)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420083)Termination reason: Instruction limit
% 4.69/1.74 % (3420083)Termination phase: Saturation
% 4.69/1.74 % (3420083)Time elapsed: 0.135 s
% 4.69/1.74 % (3420083)Peak memory usage: 134 MB
% 4.69/1.74 % (3420083)Instructions burned: 66 (million)
% 4.69/1.74 % (3420088)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=836674765:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 4.69/1.74 % (3420088)Instruction limit reached!
% 4.69/1.74 % (3420088)------------------------------
% 4.69/1.74 % (3420088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.69/1.74 % (3420088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.69/1.74 % (3420088)CaDiCaL version: 2.1.3
% 4.69/1.74 % (3420088)Termination reason: Instruction limit
% 4.69/1.74 % (3420088)Termination phase: Property scanning
% 4.69/1.74 % (3420088)Time elapsed: 0.004 s
% 4.69/1.74 % (3420088)Peak memory usage: 86 MB
% 4.69/1.74 % (3420088)Instructions burned: 3 (million)
% 4.69/1.74 % (3420095)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2150190709:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 4.69/1.74 % (3420070)Refutation found. Thanks to Tanya!
% 4.69/1.74 % SZS status Theorem for theBenchmark
% 4.69/1.74 % SZS output start Proof for theBenchmark
% See solution above
% 0.25/2.03 % (3420070)------------------------------
% 0.25/2.03 % (3420070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.25/2.03 % (3420070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.25/2.03 % (3420070)CaDiCaL version: 2.1.3
% 0.25/2.03 % (3420070)Termination reason: Refutation
% 0.25/2.03 % (3420070)Time elapsed: 0.024 s
% 0.25/2.03 % (3420070)Peak memory usage: 89 MB
% 0.25/2.03 % (3420070)Instructions burned: 19 (million)
% 0.25/2.03 % (3420070)------------------------------
% 0.25/2.03 % (3420070)------------------------------
% 0.25/2.03 % (3420038)Success in time 0.872 s
% 0.25/2.03 % Vampire exiting
%------------------------------------------------------------------------------