%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW575_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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:30:50 PM UTC 2026
% Result : Theorem 3.54s 1.16s
% Output : Refutation 4.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 25
% Syntax : Number of formulae : 89 ( 22 unt; 0 typ; 24 def)
% Number of atoms : 639 ( 61 equ)
% Maximal formula atoms : 54 ( 7 avg)
% Number of connectives : 804 ( 254 ~; 174 |; 276 &)
% ( 20 <=>; 80 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 810 ( 464 atm; 63 fun; 145 num; 138 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 : 35 ( 31 usr; 21 prp; 0-7 aty)
% Number of functors : 75 ( 68 usr; 33 con; 0-7 aty)
% Number of variables : 159 ( 118 !; 41 ?; 159 :)
% 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,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $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,
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,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
get3: ( map_int_int * $int ) > $int ).
tff(func_def_18,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_19,type,
t2tb: map_int_int > uni ).
tff(func_def_20,type,
tb2t: uni > map_int_int ).
tff(func_def_21,type,
t2tb1: $int > uni ).
tff(func_def_22,type,
tb2t1: uni > $int ).
tff(func_def_23,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_24,type,
array: ty > ty ).
tff(func_def_25,type,
mk_array2: ( ty * $int * uni ) > uni ).
tff(func_def_26,type,
mk_array3: ( $int * map_int_int ) > array_int ).
tff(func_def_27,type,
length1: ( ty * uni ) > $int ).
tff(func_def_28,type,
t2tb2: array_int > uni ).
tff(func_def_29,type,
tb2t2: uni > array_int ).
tff(func_def_30,type,
elts: ( ty * uni ) > uni ).
tff(func_def_31,type,
get4: ( ty * uni * $int ) > uni ).
tff(func_def_32,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_33,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_34,type,
occ1: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_40,type,
sK0: ( $int * map_int_int * map_int_int * $int ) > $int ).
tff(func_def_41,type,
sK1: ( map_int_int * map_int_int * $int * $int ) > $int ).
tff(func_def_42,type,
sK2: ( map_int_int * $int * $int * $int * $int * map_int_int ) > $int ).
tff(func_def_43,type,
sK3: ( $int * $int * $int * map_int_int * map_int_int ) > $int ).
tff(func_def_44,type,
sK4: ( $int * uni * uni * ty * $int ) > $int ).
tff(func_def_45,type,
sK5: ( map_int_int * $int * $int * $int ) > $int ).
tff(func_def_46,type,
sK6: ( uni * ty * $int * uni * $int ) > uni ).
tff(func_def_47,type,
sK7: ( $int * map_int_int * $int * $int ) > $int ).
tff(func_def_48,type,
sK8: ( uni * $int * $int * ty * uni ) > $int ).
tff(func_def_49,type,
sK9: ( $int * $int * ty * uni * uni * $int ) > $int ).
tff(func_def_50,type,
sK10: ( uni * ty * $int * uni * $int * $int * $int ) > $int ).
tff(func_def_51,type,
sK11: ( $int * $int * uni * ty * uni ) > $int ).
tff(func_def_52,type,
sK12: $int ).
tff(func_def_53,type,
sK13: $int ).
tff(func_def_54,type,
sK14: map_int_int ).
tff(func_def_55,type,
sK15: $int ).
tff(func_def_56,type,
sK16: $int ).
tff(func_def_57,type,
sK17: $int ).
tff(func_def_58,type,
sK18: map_int_int ).
tff(func_def_59,type,
sK19: $int ).
tff(func_def_60,type,
sK20: map_int_int ).
tff(func_def_61,type,
sK21: $int > $int ).
tff(func_def_62,type,
sK22: $int ).
tff(func_def_63,type,
sK23: ( ty * uni * $int * $int * uni ) > $int ).
tff(func_def_64,type,
sF24: array_int ).
tff(func_def_65,type,
sF25: array_int ).
tff(func_def_66,type,
sF26: $int ).
tff(func_def_67,type,
sF27: $int ).
tff(func_def_68,type,
sF28: $int ).
tff(func_def_69,type,
sF29: $int ).
tff(func_def_70,type,
sF30: array_int ).
tff(func_def_71,type,
sF31: $int ).
tff(func_def_72,type,
sF32: $int ).
tff(func_def_73,type,
sF33: $int ).
tff(func_def_74,type,
sF34: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_4,type,
permut2: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_5,type,
map_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_6,type,
array_eq_sub1: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_7,type,
array_eq: ( ty * uni * uni ) > $o ).
tff(pred_def_8,type,
exchange2: ( ty * uni * uni * $int * $int * $int * $int ) > $o ).
tff(pred_def_9,type,
exchange3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_10,type,
permut3: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_11,type,
permut_sub2: ( ty * uni * uni * $int * $int ) > $o ).
tff(pred_def_12,type,
permut_sub3: ( array_int * array_int * $int * $int ) > $o ).
tff(pred_def_13,type,
permut_all: ( ty * uni * uni ) > $o ).
tff(f85,conjecture,
! [X2: $int,X1: map_int_int,X4: $int,X3: $int,X0: $int] :
( ( $lesseq(0,X2)
& $less(X3,X0)
& $lesseq(0,X0)
& $lesseq(X2,X4)
& $lesseq(X4,X3) )
=> ( $less(X2,X3)
=> ( ( $lesseq(0,X2)
& $less(X3,X0)
& $less(X2,X3) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( $lesseq(X6,X3)
& ! [X8: $int] :
( ( $lesseq(X8,X5)
& $lesseq(X2,X8) )
=> $lesseq(get3(X7,X8),42) )
& $less(X5,X6)
& $lesseq(0,X0)
& $lesseq(X2,X5)
& ! [X8: $int] :
( ( $less(X5,X8)
& $less(X8,X6) )
=> ( get3(X7,X8) = 42 ) )
& permut_sub3(mk_array3(X0,X1),mk_array3(X0,X7),X2,$sum(X3,1))
& ! [X8: $int] :
( ( $lesseq(X6,X8)
& $lesseq(X8,X3) )
=> $lesseq(42,get3(X7,X8)) ) )
=> ( $lesseq(X4,X5)
=> ( ( $lesseq(X2,X4)
& $lesseq(X4,X5)
& $less(X5,X0)
& $lesseq(0,X2) )
=> ! [X9: map_int_int] :
( ( ! [X8: $int] :
( ( $lesseq(X2,X8)
& $lesseq(X8,X4) )
=> $lesseq(get3(X9,X8),get3(X9,X4)) )
& ! [X8: $int] :
( ( $lesseq(X4,X8)
& $lesseq(X8,X5) )
=> $lesseq(get3(X9,X4),get3(X9,X8)) )
& $lesseq(0,X0)
& permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X5,1)) )
=> ( permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X3,1))
=> ( ! [X8: $int] :
( ( $less(X5,X8)
& $lesseq(X8,X3) )
=> ( get3(X9,X8) = get3(X7,X8) ) )
=> ( ! [X8: $int] :
( ( $lesseq(X2,X8)
& $lesseq(X8,X5) )
=> ( $lesseq(get3(X9,X8),get3(X9,$sum(X5,1)))
& ? [X10: $int] :
( $lesseq(X10,X5)
& $lesseq(X2,X10)
& ( get3(X9,X8) = get3(X7,X10) ) ) ) )
=> ( ~ $lesseq(X6,X4)
=> ( permut_sub3(mk_array3(X0,X9),mk_array3(X0,X9),X2,$sum(X3,1))
=> ! [X8: $int] :
( ( $lesseq(X6,X8)
& $lesseq(X8,X3) )
=> ( ? [X10: $int] :
( ( get3(X9,X8) = get3(X9,X10) )
& $lesseq(X6,X10)
& $lesseq(X10,X3) )
& $lesseq(get3(X9,$difference(X6,1)),get3(X9,X8)) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_find) ).
tff(f86,negated_conjecture,
~ ! [X2: $int,X1: map_int_int,X4: $int,X3: $int,X0: $int] :
( ( $lesseq(0,X2)
& $less(X3,X0)
& $lesseq(0,X0)
& $lesseq(X2,X4)
& $lesseq(X4,X3) )
=> ( $less(X2,X3)
=> ( ( $lesseq(0,X2)
& $less(X3,X0)
& $less(X2,X3) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( $lesseq(X6,X3)
& ! [X8: $int] :
( ( $lesseq(X8,X5)
& $lesseq(X2,X8) )
=> $lesseq(get3(X7,X8),42) )
& $less(X5,X6)
& $lesseq(0,X0)
& $lesseq(X2,X5)
& ! [X8: $int] :
( ( $less(X5,X8)
& $less(X8,X6) )
=> ( get3(X7,X8) = 42 ) )
& permut_sub3(mk_array3(X0,X1),mk_array3(X0,X7),X2,$sum(X3,1))
& ! [X8: $int] :
( ( $lesseq(X6,X8)
& $lesseq(X8,X3) )
=> $lesseq(42,get3(X7,X8)) ) )
=> ( $lesseq(X4,X5)
=> ( ( $lesseq(X2,X4)
& $lesseq(X4,X5)
& $less(X5,X0)
& $lesseq(0,X2) )
=> ! [X9: map_int_int] :
( ( ! [X8: $int] :
( ( $lesseq(X2,X8)
& $lesseq(X8,X4) )
=> $lesseq(get3(X9,X8),get3(X9,X4)) )
& ! [X8: $int] :
( ( $lesseq(X4,X8)
& $lesseq(X8,X5) )
=> $lesseq(get3(X9,X4),get3(X9,X8)) )
& $lesseq(0,X0)
& permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X5,1)) )
=> ( permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X3,1))
=> ( ! [X8: $int] :
( ( $less(X5,X8)
& $lesseq(X8,X3) )
=> ( get3(X9,X8) = get3(X7,X8) ) )
=> ( ! [X8: $int] :
( ( $lesseq(X2,X8)
& $lesseq(X8,X5) )
=> ( $lesseq(get3(X9,X8),get3(X9,$sum(X5,1)))
& ? [X10: $int] :
( $lesseq(X10,X5)
& $lesseq(X2,X10)
& ( get3(X9,X8) = get3(X7,X10) ) ) ) )
=> ( ~ $lesseq(X6,X4)
=> ( permut_sub3(mk_array3(X0,X9),mk_array3(X0,X9),X2,$sum(X3,1))
=> ! [X8: $int] :
( ( $lesseq(X6,X8)
& $lesseq(X8,X3) )
=> ( ? [X10: $int] :
( ( get3(X9,X8) = get3(X9,X10) )
& $lesseq(X6,X10)
& $lesseq(X10,X3) )
& $lesseq(get3(X9,$difference(X6,1)),get3(X9,X8)) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f85]) ).
tff(f106,plain,
~ ! [X2: $int,X1: map_int_int,X4: $int,X3: $int,X0: $int] :
( ( ~ $less(X2,0)
& $less(X3,X0)
& ~ $less(X0,0)
& ~ $less(X4,X2)
& ~ $less(X3,X4) )
=> ( $less(X2,X3)
=> ( ( ~ $less(X2,0)
& $less(X3,X0)
& $less(X2,X3) )
=> ! [X7: map_int_int,X6: $int,X5: $int] :
( ( ~ $less(X3,X6)
& ! [X8: $int] :
( ( ~ $less(X5,X8)
& ~ $less(X8,X2) )
=> ~ $less(42,get3(X7,X8)) )
& $less(X5,X6)
& ~ $less(X0,0)
& ~ $less(X5,X2)
& ! [X8: $int] :
( ( $less(X5,X8)
& $less(X8,X6) )
=> ( get3(X7,X8) = 42 ) )
& permut_sub3(mk_array3(X0,X1),mk_array3(X0,X7),X2,$sum(X3,1))
& ! [X8: $int] :
( ( ~ $less(X8,X6)
& ~ $less(X3,X8) )
=> ~ $less(get3(X7,X8),42) ) )
=> ( ~ $less(X5,X4)
=> ( ( ~ $less(X4,X2)
& ~ $less(X5,X4)
& $less(X5,X0)
& ~ $less(X2,0) )
=> ! [X9: map_int_int] :
( ( ! [X8: $int] :
( ( ~ $less(X8,X2)
& ~ $less(X4,X8) )
=> ~ $less(get3(X9,X4),get3(X9,X8)) )
& ! [X8: $int] :
( ( ~ $less(X8,X4)
& ~ $less(X5,X8) )
=> ~ $less(get3(X9,X8),get3(X9,X4)) )
& ~ $less(X0,0)
& permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X5,1)) )
=> ( permut_sub3(mk_array3(X0,X7),mk_array3(X0,X9),X2,$sum(X3,1))
=> ( ! [X8: $int] :
( ( $less(X5,X8)
& ~ $less(X3,X8) )
=> ( get3(X9,X8) = get3(X7,X8) ) )
=> ( ! [X8: $int] :
( ( ~ $less(X8,X2)
& ~ $less(X5,X8) )
=> ( ~ $less(get3(X9,$sum(X5,1)),get3(X9,X8))
& ? [X10: $int] :
( ~ $less(X5,X10)
& ~ $less(X10,X2)
& ( get3(X9,X8) = get3(X7,X10) ) ) ) )
=> ( $less(X4,X6)
=> ( permut_sub3(mk_array3(X0,X9),mk_array3(X0,X9),X2,$sum(X3,1))
=> ! [X8: $int] :
( ( ~ $less(X8,X6)
& ~ $less(X3,X8) )
=> ( ? [X10: $int] :
( ( get3(X9,X8) = get3(X9,X10) )
& ~ $less(X10,X6)
& ~ $less(X3,X10) )
& ~ $less(get3(X9,X8),get3(X9,$sum(X6,$uminus(1)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f86]) ).
tff(f160,plain,
~ ! [X2: $int,X4: $int,X0: $int,X1: map_int_int,X3: $int] :
( ( $less(X3,X4)
& ~ $less(X3,X2)
& ~ $less(X0,0)
& ~ $less(X2,X0)
& ~ $less(X4,0) )
=> ( $less(X0,X3)
=> ( ( $less(X0,X3)
& ~ $less(X0,0)
& $less(X3,X4) )
=> ! [X7: $int,X6: $int,X5: map_int_int] :
( ( ~ $less(X7,X0)
& ~ $less(X4,0)
& ! [X10: $int] :
( ( ~ $less(X3,X10)
& ~ $less(X10,X6) )
=> ~ $less(get3(X5,X10),42) )
& permut_sub3(mk_array3(X4,X1),mk_array3(X4,X5),X0,$sum(X3,1))
& $less(X7,X6)
& ! [X8: $int] :
( ( ~ $less(X7,X8)
& ~ $less(X8,X0) )
=> ~ $less(42,get3(X5,X8)) )
& ! [X9: $int] :
( ( $less(X7,X9)
& $less(X9,X6) )
=> ( 42 = get3(X5,X9) ) )
& ~ $less(X3,X6) )
=> ( ~ $less(X7,X2)
=> ( ( ~ $less(X7,X2)
& ~ $less(X2,X0)
& $less(X7,X4)
& ~ $less(X0,0) )
=> ! [X11: map_int_int] :
( ( ! [X12: $int] :
( ( ~ $less(X12,X0)
& ~ $less(X2,X12) )
=> ~ $less(get3(X11,X2),get3(X11,X12)) )
& permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X7,1))
& ! [X13: $int] :
( ( ~ $less(X13,X2)
& ~ $less(X7,X13) )
=> ~ $less(get3(X11,X13),get3(X11,X2)) )
& ~ $less(X4,0) )
=> ( permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X3,1))
=> ( ! [X14: $int] :
( ( $less(X7,X14)
& ~ $less(X3,X14) )
=> ( get3(X11,X14) = get3(X5,X14) ) )
=> ( ! [X15: $int] :
( ( ~ $less(X15,X0)
& ~ $less(X7,X15) )
=> ( ? [X16: $int] :
( ~ $less(X16,X0)
& ( get3(X11,X15) = get3(X5,X16) )
& ~ $less(X7,X16) )
& ~ $less(get3(X11,$sum(X7,1)),get3(X11,X15)) ) )
=> ( $less(X2,X6)
=> ( permut_sub3(mk_array3(X4,X11),mk_array3(X4,X11),X0,$sum(X3,1))
=> ! [X17: $int] :
( ( ~ $less(X17,X6)
& ~ $less(X3,X17) )
=> ( ~ $less(get3(X11,X17),get3(X11,$sum(X6,$uminus(1))))
& ? [X18: $int] :
( ~ $less(X3,X18)
& ~ $less(X18,X6)
& ( get3(X11,X18) = get3(X11,X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f106]) ).
tff(f187,plain,
? [X2: $int,X4: $int,X0: $int,X1: map_int_int,X3: $int] :
( ? [X7: $int,X6: $int,X5: map_int_int] :
( ? [X11: map_int_int] :
( ? [X17: $int] :
( ( ! [X18: $int] :
( ( get3(X11,X18) != get3(X11,X17) )
| $less(X3,X18)
| $less(X18,X6) )
| $less(get3(X11,X17),get3(X11,$sum(X6,$uminus(1)))) )
& ~ $less(X17,X6)
& ~ $less(X3,X17) )
& permut_sub3(mk_array3(X4,X11),mk_array3(X4,X11),X0,$sum(X3,1))
& $less(X2,X6)
& ! [X15: $int] :
( ( ? [X16: $int] :
( ~ $less(X16,X0)
& ( get3(X11,X15) = get3(X5,X16) )
& ~ $less(X7,X16) )
& ~ $less(get3(X11,$sum(X7,1)),get3(X11,X15)) )
| $less(X15,X0)
| $less(X7,X15) )
& ! [X14: $int] :
( ( get3(X11,X14) = get3(X5,X14) )
| ~ $less(X7,X14)
| $less(X3,X14) )
& permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X3,1))
& ! [X12: $int] :
( ~ $less(get3(X11,X2),get3(X11,X12))
| $less(X12,X0)
| $less(X2,X12) )
& permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X7,1))
& ! [X13: $int] :
( ~ $less(get3(X11,X13),get3(X11,X2))
| $less(X13,X2)
| $less(X7,X13) )
& ~ $less(X4,0) )
& ~ $less(X7,X2)
& ~ $less(X2,X0)
& $less(X7,X4)
& ~ $less(X0,0)
& ~ $less(X7,X2)
& ~ $less(X7,X0)
& ~ $less(X4,0)
& ! [X10: $int] :
( ~ $less(get3(X5,X10),42)
| $less(X3,X10)
| $less(X10,X6) )
& permut_sub3(mk_array3(X4,X1),mk_array3(X4,X5),X0,$sum(X3,1))
& $less(X7,X6)
& ! [X8: $int] :
( ~ $less(42,get3(X5,X8))
| $less(X7,X8)
| $less(X8,X0) )
& ! [X9: $int] :
( ( 42 = get3(X5,X9) )
| ~ $less(X7,X9)
| ~ $less(X9,X6) )
& ~ $less(X3,X6) )
& $less(X0,X3)
& ~ $less(X0,0)
& $less(X3,X4)
& $less(X0,X3)
& $less(X3,X4)
& ~ $less(X3,X2)
& ~ $less(X0,0)
& ~ $less(X2,X0)
& ~ $less(X4,0) ),
inference(ennf_transformation,[],[f160]) ).
tff(f188,plain,
? [X0: $int,X3: $int,X1: map_int_int,X2: $int,X4: $int] :
( ~ $less(X3,X2)
& ~ $less(X0,0)
& $less(X3,X4)
& ~ $less(X4,0)
& ~ $less(X0,0)
& $less(X3,X4)
& $less(X0,X3)
& $less(X0,X3)
& ~ $less(X2,X0)
& ? [X7: $int,X5: map_int_int,X6: $int] :
( ~ $less(X7,X0)
& ~ $less(X2,X0)
& $less(X7,X4)
& ! [X9: $int] :
( ( 42 = get3(X5,X9) )
| ~ $less(X7,X9)
| ~ $less(X9,X6) )
& ~ $less(X4,0)
& permut_sub3(mk_array3(X4,X1),mk_array3(X4,X5),X0,$sum(X3,1))
& ? [X11: map_int_int] :
( ! [X15: $int] :
( $less(X15,X0)
| ( ? [X16: $int] :
( ~ $less(X16,X0)
& ( get3(X11,X15) = get3(X5,X16) )
& ~ $less(X7,X16) )
& ~ $less(get3(X11,$sum(X7,1)),get3(X11,X15)) )
| $less(X7,X15) )
& ! [X13: $int] :
( ~ $less(get3(X11,X13),get3(X11,X2))
| $less(X7,X13)
| $less(X13,X2) )
& permut_sub3(mk_array3(X4,X11),mk_array3(X4,X11),X0,$sum(X3,1))
& permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X3,1))
& ! [X14: $int] :
( ~ $less(X7,X14)
| ( get3(X11,X14) = get3(X5,X14) )
| $less(X3,X14) )
& ? [X17: $int] :
( ~ $less(X3,X17)
& ~ $less(X17,X6)
& ( ! [X18: $int] :
( ( get3(X11,X18) != get3(X11,X17) )
| $less(X3,X18)
| $less(X18,X6) )
| $less(get3(X11,X17),get3(X11,$sum(X6,$uminus(1)))) ) )
& ! [X12: $int] :
( $less(X2,X12)
| ~ $less(get3(X11,X2),get3(X11,X12))
| $less(X12,X0) )
& permut_sub3(mk_array3(X4,X5),mk_array3(X4,X11),X0,$sum(X7,1))
& ~ $less(X4,0)
& $less(X2,X6) )
& ~ $less(X0,0)
& ! [X8: $int] :
( $less(X8,X0)
| $less(X7,X8)
| ~ $less(42,get3(X5,X8)) )
& ~ $less(X3,X6)
& ~ $less(X7,X2)
& ! [X10: $int] :
( $less(X3,X10)
| $less(X10,X6)
| ~ $less(get3(X5,X10),42) )
& $less(X7,X6)
& ~ $less(X7,X2) ) ),
inference(flattening,[],[f187]) ).
tff(f329,plain,
? [X0: $int,X1: $int,X2: map_int_int,X3: $int,X4: $int] :
( ~ $less(X1,X3)
& ~ $less(X0,0)
& $less(X1,X4)
& ~ $less(X4,0)
& ~ $less(X0,0)
& $less(X1,X4)
& $less(X0,X1)
& $less(X0,X1)
& ~ $less(X3,X0)
& ? [X5: $int,X6: map_int_int,X7: $int] :
( ~ $less(X5,X0)
& ~ $less(X3,X0)
& $less(X5,X4)
& ! [X8: $int] :
( ( 42 = get3(X6,X8) )
| ~ $less(X5,X8)
| ~ $less(X8,X7) )
& ~ $less(X4,0)
& permut_sub3(mk_array3(X4,X2),mk_array3(X4,X6),X0,$sum(X1,1))
& ? [X9: map_int_int] :
( ! [X10: $int] :
( $less(X10,X0)
| ( ? [X11: $int] :
( ~ $less(X11,X0)
& ( get3(X9,X10) = get3(X6,X11) )
& ~ $less(X5,X11) )
& ~ $less(get3(X9,$sum(X5,1)),get3(X9,X10)) )
| $less(X5,X10) )
& ! [X12: $int] :
( ~ $less(get3(X9,X12),get3(X9,X3))
| $less(X5,X12)
| $less(X12,X3) )
& permut_sub3(mk_array3(X4,X9),mk_array3(X4,X9),X0,$sum(X1,1))
& permut_sub3(mk_array3(X4,X6),mk_array3(X4,X9),X0,$sum(X1,1))
& ! [X13: $int] :
( ~ $less(X5,X13)
| ( get3(X6,X13) = get3(X9,X13) )
| $less(X1,X13) )
& ? [X14: $int] :
( ~ $less(X1,X14)
& ~ $less(X14,X7)
& ( ! [X15: $int] :
( ( get3(X9,X14) != get3(X9,X15) )
| $less(X1,X15)
| $less(X15,X7) )
| $less(get3(X9,X14),get3(X9,$sum(X7,$uminus(1)))) ) )
& ! [X16: $int] :
( $less(X3,X16)
| ~ $less(get3(X9,X3),get3(X9,X16))
| $less(X16,X0) )
& permut_sub3(mk_array3(X4,X6),mk_array3(X4,X9),X0,$sum(X5,1))
& ~ $less(X4,0)
& $less(X3,X7) )
& ~ $less(X0,0)
& ! [X17: $int] :
( $less(X17,X0)
| $less(X5,X17)
| ~ $less(42,get3(X6,X17)) )
& ~ $less(X1,X7)
& ~ $less(X5,X3)
& ! [X18: $int] :
( $less(X1,X18)
| $less(X18,X7)
| ~ $less(get3(X6,X18),42) )
& $less(X5,X7)
& ~ $less(X5,X3) ) ),
inference(rectify,[],[f188]) ).
tff(f330,plain,
( ~ $less(sK13,sK15)
& ~ $less(sK12,0)
& $less(sK13,sK16)
& ~ $less(sK16,0)
& ~ $less(sK12,0)
& $less(sK13,sK16)
& $less(sK12,sK13)
& $less(sK12,sK13)
& ~ $less(sK15,sK12)
& ~ $less(sK17,sK12)
& ~ $less(sK15,sK12)
& $less(sK17,sK16)
& ! [X8: $int] :
( ( 42 = get3(sK18,X8) )
| ~ $less(sK17,X8)
| ~ $less(X8,sK19) )
& ~ $less(sK16,0)
& permut_sub3(mk_array3(sK16,sK14),mk_array3(sK16,sK18),sK12,$sum(sK13,1))
& ! [X10: $int] :
( $less(X10,sK12)
| ( ~ $less(sK21(X10),sK12)
& ( get3(sK18,sK21(X10)) = get3(sK20,X10) )
& ~ $less(sK17,sK21(X10))
& ~ $less(get3(sK20,$sum(sK17,1)),get3(sK20,X10)) )
| $less(sK17,X10) )
& ! [X12: $int] :
( ~ $less(get3(sK20,X12),get3(sK20,sK15))
| $less(sK17,X12)
| $less(X12,sK15) )
& permut_sub3(mk_array3(sK16,sK20),mk_array3(sK16,sK20),sK12,$sum(sK13,1))
& permut_sub3(mk_array3(sK16,sK18),mk_array3(sK16,sK20),sK12,$sum(sK13,1))
& ! [X13: $int] :
( ~ $less(sK17,X13)
| ( get3(sK20,X13) = get3(sK18,X13) )
| $less(sK13,X13) )
& ~ $less(sK13,sK22)
& ~ $less(sK22,sK19)
& ( ! [X15: $int] :
( ( get3(sK20,sK22) != get3(sK20,X15) )
| $less(sK13,X15)
| $less(X15,sK19) )
| $less(get3(sK20,sK22),get3(sK20,$sum(sK19,$uminus(1)))) )
& ! [X16: $int] :
( $less(sK15,X16)
| ~ $less(get3(sK20,sK15),get3(sK20,X16))
| $less(X16,sK12) )
& permut_sub3(mk_array3(sK16,sK18),mk_array3(sK16,sK20),sK12,$sum(sK17,1))
& ~ $less(sK16,0)
& $less(sK15,sK19)
& ~ $less(sK12,0)
& ! [X17: $int] :
( $less(X17,sK12)
| $less(sK17,X17)
| ~ $less(42,get3(sK18,X17)) )
& ~ $less(sK13,sK19)
& ~ $less(sK17,sK15)
& ! [X18: $int] :
( $less(sK13,X18)
| $less(X18,sK19)
| ~ $less(get3(sK18,X18),42) )
& $less(sK17,sK19)
& ~ $less(sK17,sK15) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK12),skolemize(X1,sK13),skolemize(X2,sK14),skolemize(X3,sK15),skolemize(X4,sK16),skolemize(X5,sK17),skolemize(X6,sK18),skolemize(X7,sK19),skolemize(X9,sK20),skolemize(X11,sK21(X10)),skolemize(X14,sK22)],[f329]) ).
tff(f467,plain,
$less(sK17,sK19),
inference(cnf_transformation,[],[f330]) ).
tff(f468,plain,
! [X18: $int] :
( ~ $less(get3(sK18,X18),42)
| $less(X18,sK19)
| $less(sK13,X18) ),
inference(cnf_transformation,[],[f330]) ).
tff(f471,plain,
! [X17: $int] :
( ~ $less(42,get3(sK18,X17))
| $less(X17,sK12)
| $less(sK17,X17) ),
inference(cnf_transformation,[],[f330]) ).
tff(f473,plain,
$less(sK15,sK19),
inference(cnf_transformation,[],[f330]) ).
tff(f477,plain,
! [X15: $int] :
( ( get3(sK20,sK22) != get3(sK20,X15) )
| $less(sK13,X15)
| $less(X15,sK19)
| $less(get3(sK20,sK22),get3(sK20,$sum(sK19,$uminus(1)))) ),
inference(cnf_transformation,[],[f330]) ).
tff(f478,plain,
~ $less(sK22,sK19),
inference(cnf_transformation,[],[f330]) ).
tff(f479,plain,
~ $less(sK13,sK22),
inference(cnf_transformation,[],[f330]) ).
tff(f480,plain,
! [X13: $int] :
( ( get3(sK20,X13) = get3(sK18,X13) )
| $less(sK13,X13)
| ~ $less(sK17,X13) ),
inference(cnf_transformation,[],[f330]) ).
tff(f485,plain,
! [X10: $int] :
( ~ $less(sK17,sK21(X10))
| $less(sK17,X10)
| $less(X10,sK12) ),
inference(cnf_transformation,[],[f330]) ).
tff(f486,plain,
! [X10: $int] :
( ( get3(sK18,sK21(X10)) = get3(sK20,X10) )
| $less(X10,sK12)
| $less(sK17,X10) ),
inference(cnf_transformation,[],[f330]) ).
tff(f487,plain,
! [X10: $int] :
( ~ $less(sK21(X10),sK12)
| $less(X10,sK12)
| $less(sK17,X10) ),
inference(cnf_transformation,[],[f330]) ).
tff(f490,plain,
! [X8: $int] :
( ( 42 = get3(sK18,X8) )
| ~ $less(X8,sK19)
| ~ $less(sK17,X8) ),
inference(cnf_transformation,[],[f330]) ).
tff(f492,plain,
~ $less(sK15,sK12),
inference(cnf_transformation,[],[f330]) ).
tff(f548,definition,
sF31 = get3(sK20,sK22),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f549,plain,
get3(sK20,sK22) = sF31,
inference(reorient_equations,[],[f548]) ).
tff(f550,definition,
sF32 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f551,definition,
sF33 = $sum(sK19,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f552,plain,
$sum(sK19,sF32) = sF33,
inference(reorient_equations,[],[f551]) ).
tff(f553,definition,
sF34 = get3(sK20,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f554,plain,
! [X15: $int] :
( $less(sF31,sF34)
| $less(sK13,X15)
| $less(X15,sK19)
| ( sF31 != get3(sK20,X15) ) ),
inference(definition_folding,[],[f477,f553,f552,f550,f549,f549]) ).
tff(f557,plain,
sF32 = -1,
inference(evaluation,[],[f550]) ).
tff(f563,definition,
( spl35_1
<=> ( sF32 = -1 ) ),
introduced(definition,[new_symbols(definition,[spl35_1])],[avatar_definition]) ).
tff(f565,plain,
( ( sF32 = -1 )
| ~ spl35_1 ),
inference(avatar_component_clause,[],[f563]) ).
tff(f566,plain,
spl35_1,
inference(avatar_split_clause,[],[f557,f563]) ).
tff(f593,definition,
( spl35_7
<=> $less(sK17,sK19) ),
introduced(definition,[new_symbols(definition,[spl35_7])],[avatar_definition]) ).
tff(f596,plain,
spl35_7,
inference(avatar_split_clause,[],[f467,f593]) ).
tff(f598,definition,
( spl35_8
<=> $less(sK22,sK19) ),
introduced(definition,[new_symbols(definition,[spl35_8])],[avatar_definition]) ).
tff(f600,plain,
( ~ $less(sK22,sK19)
| spl35_8 ),
inference(avatar_component_clause,[],[f598]) ).
tff(f601,plain,
~ spl35_8,
inference(avatar_split_clause,[],[f478,f598]) ).
tff(f613,definition,
( spl35_11
<=> $less(sK15,sK12) ),
introduced(definition,[new_symbols(definition,[spl35_11])],[avatar_definition]) ).
tff(f616,plain,
~ spl35_11,
inference(avatar_split_clause,[],[f492,f613]) ).
tff(f643,definition,
( spl35_17
<=> ( $sum(sK19,sF32) = sF33 ) ),
introduced(definition,[new_symbols(definition,[spl35_17])],[avatar_definition]) ).
tff(f645,plain,
( ( $sum(sK19,sF32) = sF33 )
| ~ spl35_17 ),
inference(avatar_component_clause,[],[f643]) ).
tff(f646,plain,
spl35_17,
inference(avatar_split_clause,[],[f552,f643]) ).
tff(f658,definition,
( spl35_20
<=> ! [X15: $int] :
( $less(sK13,X15)
| ( sF31 != get3(sK20,X15) )
| $less(X15,sK19) ) ),
introduced(definition,[new_symbols(definition,[spl35_20])],[avatar_definition]) ).
tff(f659,plain,
( ! [X15: $int] :
( ( sF31 != get3(sK20,X15) )
| $less(sK13,X15)
| $less(X15,sK19) )
| ~ spl35_20 ),
inference(avatar_component_clause,[],[f658]) ).
tff(f661,definition,
( spl35_21
<=> $less(sF31,sF34) ),
introduced(definition,[new_symbols(definition,[spl35_21])],[avatar_definition]) ).
tff(f664,plain,
( spl35_20
| spl35_21 ),
inference(avatar_split_clause,[],[f554,f661,f658]) ).
tff(f671,definition,
( spl35_23
<=> ( get3(sK20,sK22) = sF31 ) ),
introduced(definition,[new_symbols(definition,[spl35_23])],[avatar_definition]) ).
tff(f673,plain,
( ( get3(sK20,sK22) = sF31 )
| ~ spl35_23 ),
inference(avatar_component_clause,[],[f671]) ).
tff(f674,plain,
spl35_23,
inference(avatar_split_clause,[],[f549,f671]) ).
tff(f696,definition,
( spl35_28
<=> $less(sK13,sK22) ),
introduced(definition,[new_symbols(definition,[spl35_28])],[avatar_definition]) ).
tff(f698,plain,
( ~ $less(sK13,sK22)
| spl35_28 ),
inference(avatar_component_clause,[],[f696]) ).
tff(f699,plain,
~ spl35_28,
inference(avatar_split_clause,[],[f479,f696]) ).
tff(f701,definition,
( spl35_29
<=> ( sF34 = get3(sK20,sF33) ) ),
introduced(definition,[new_symbols(definition,[spl35_29])],[avatar_definition]) ).
tff(f703,plain,
( ( sF34 = get3(sK20,sF33) )
| ~ spl35_29 ),
inference(avatar_component_clause,[],[f701]) ).
tff(f704,plain,
spl35_29,
inference(avatar_split_clause,[],[f553,f701]) ).
tff(f716,definition,
( spl35_32
<=> $less(sK15,sK19) ),
introduced(definition,[new_symbols(definition,[spl35_32])],[avatar_definition]) ).
tff(f719,plain,
spl35_32,
inference(avatar_split_clause,[],[f473,f716]) ).
tff(f722,plain,
! [X0: $int] :
( ( 42 = get3(sK20,X0) )
| ~ $less(sK17,X0)
| ~ $less(X0,sK19)
| $less(sK13,X0)
| ~ $less(sK17,X0) ),
inference(superposition,[],[f480,f490]) ).
tff(f725,plain,
! [X0: $int] :
( ~ $less(get3(sK20,X0),42)
| ~ $less(sK17,X0)
| $less(sK13,X0)
| $less(sK13,X0)
| $less(X0,sK19) ),
inference(superposition,[],[f468,f480]) ).
tff(f726,plain,
! [X0: $int] :
( ( 42 = get3(sK20,X0) )
| $less(sK13,X0)
| ~ $less(X0,sK19)
| ~ $less(sK17,X0) ),
inference(duplicate_literal_removal,[],[f722]) ).
tff(f727,plain,
! [X0: $int] :
( ~ $less(get3(sK20,X0),42)
| $less(X0,sK19)
| $less(sK13,X0)
| ~ $less(sK17,X0) ),
inference(duplicate_literal_removal,[],[f725]) ).
tff(f733,plain,
! [X0: $int] :
( $less(sK17,X0)
| ~ $less(42,get3(sK20,X0))
| $less(sK17,sK21(X0))
| $less(X0,sK12)
| $less(sK21(X0),sK12) ),
inference(superposition,[],[f471,f486]) ).
tff(f735,plain,
! [X0: $int] :
( $less(sK17,sK21(X0))
| $less(sK17,X0)
| ~ $less(42,get3(sK20,X0))
| $less(X0,sK12) ),
inference(forward_subsumption_resolution,[],[f733,f487]) ).
tff(f736,plain,
! [X0: $int] :
( ~ $less(42,get3(sK20,X0))
| $less(sK17,X0)
| $less(X0,sK12) ),
inference(forward_subsumption_resolution,[],[f735,f485]) ).
tff(f791,plain,
( ( $sum(sK19,-1) = sF33 )
| ~ spl35_1
| ~ spl35_17 ),
inference(forward_demodulation,[],[f645,f565]) ).
tff(f793,definition,
( spl35_39
<=> ( $sum(sK19,-1) = sF33 ) ),
introduced(definition,[new_symbols(definition,[spl35_39])],[avatar_definition]) ).
tff(f796,plain,
( spl35_39
| ~ spl35_1
| ~ spl35_17 ),
inference(avatar_split_clause,[],[f791,f643,f563,f793]) ).
tff(f802,plain,
( ~ $less(sK17,sK22)
| ~ $less(sF31,42)
| $less(sK13,sK22)
| $less(sK22,sK19)
| ~ spl35_23 ),
inference(superposition,[],[f727,f673]) ).
tff(f806,definition,
( spl35_40
<=> $less(sK17,sK22) ),
introduced(definition,[new_symbols(definition,[spl35_40])],[avatar_definition]) ).
tff(f841,plain,
( ~ $less(sF31,42)
| $less(sK22,sK19)
| ~ $less(sK17,sK22)
| ~ spl35_23
| spl35_28 ),
inference(forward_subsumption_resolution,[],[f802,f698]) ).
tff(f843,definition,
( spl35_48
<=> $less(sF31,42) ),
introduced(definition,[new_symbols(definition,[spl35_48])],[avatar_definition]) ).
tff(f855,plain,
( ~ $less(sF31,42)
| ~ $less(sK17,sK22)
| spl35_8
| ~ spl35_23
| spl35_28 ),
inference(forward_subsumption_resolution,[],[f841,f600]) ).
tff(f856,plain,
( ~ spl35_48
| ~ spl35_40
| spl35_8
| ~ spl35_23
| spl35_28 ),
inference(avatar_split_clause,[],[f855,f696,f671,f598,f806,f843]) ).
tff(f935,plain,
( ( 42 = sF34 )
| ~ $less(sF33,sK19)
| $less(sK13,sF33)
| ~ $less(sK17,sF33)
| ~ spl35_29 ),
inference(superposition,[],[f726,f703]) ).
tff(f938,plain,
( ~ $less(42,sF34)
| $less(sK17,sF33)
| $less(sF33,sK12)
| ~ spl35_29 ),
inference(superposition,[],[f736,f703]) ).
tff(f940,definition,
( spl35_65
<=> $less(sK17,sF33) ),
introduced(definition,[new_symbols(definition,[spl35_65])],[avatar_definition]) ).
tff(f957,definition,
( spl35_69
<=> $less(sK13,sF33) ),
introduced(definition,[new_symbols(definition,[spl35_69])],[avatar_definition]) ).
tff(f961,definition,
( spl35_70
<=> $less(sF33,sK19) ),
introduced(definition,[new_symbols(definition,[spl35_70])],[avatar_definition]) ).
tff(f974,definition,
( spl35_73
<=> $less(sF33,sK12) ),
introduced(definition,[new_symbols(definition,[spl35_73])],[avatar_definition]) ).
tff(f988,definition,
( spl35_76
<=> ( 42 = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl35_76])],[avatar_definition]) ).
tff(f993,definition,
( spl35_77
<=> $less(42,sF34) ),
introduced(definition,[new_symbols(definition,[spl35_77])],[avatar_definition]) ).
tff(f996,plain,
( ~ spl35_77
| spl35_73
| spl35_65
| ~ spl35_29 ),
inference(avatar_split_clause,[],[f938,f701,f940,f974,f993]) ).
tff(f1002,plain,
( ~ spl35_65
| spl35_69
| ~ spl35_70
| spl35_76
| ~ spl35_29 ),
inference(avatar_split_clause,[],[f935,f701,f988,f961,f957,f940]) ).
tff(f1005,plain,
( $less(sK13,sK22)
| ( sF31 != sF31 )
| $less(sK22,sK19)
| ~ spl35_20
| ~ spl35_23 ),
inference(superposition,[],[f659,f673]) ).
tff(f1008,plain,
( $less(sK22,sK19)
| $less(sK13,sK22)
| ~ spl35_20
| ~ spl35_23 ),
inference(trivial_inequality_removal,[],[f1005]) ).
tff(f1010,plain,
( $less(sK13,sK22)
| spl35_8
| ~ spl35_20
| ~ spl35_23 ),
inference(forward_subsumption_resolution,[],[f1008,f600]) ).
tff(f1021,plain,
( $false
| spl35_8
| ~ spl35_20
| ~ spl35_23
| spl35_28 ),
inference(forward_subsumption_resolution,[],[f1010,f698]) ).
tff(f1022,plain,
( spl35_8
| ~ spl35_20
| ~ spl35_23
| spl35_28 ),
inference(avatar_contradiction_clause,[],[f1021]) ).
tff(f1023,plain,
$false,
inference(avatar_smt_refutation,[],[f1022,f1002,f996,f856,f796,f719,f704,f699,f674,f664,f646,f616,f601,f596,f566]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW575_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n009.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 14:19:45 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.54/1.16 % (3056612)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.54/1.16 % (3056617)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=823018898:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.54/1.16 % (3056617)Instruction limit reached!
% 3.54/1.16 % (3056617)------------------------------
% 3.54/1.16 % (3056617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056617)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056617)Termination reason: Instruction limit
% 3.54/1.16 % (3056617)Termination phase: Saturation
% 3.54/1.16 % (3056617)Time elapsed: 0.004 s
% 3.54/1.16 % (3056617)Peak memory usage: 89 MB
% 3.54/1.16 % (3056617)Instructions burned: 12 (million)
% 3.54/1.16 % (3056621)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2023993593:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.54/1.16 % (3056622)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2311451057:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.54/1.16 % (3056620)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=714930959:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.54/1.16 % (3056623)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2963656913:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.54/1.16 % (3056618)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2741025653:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.54/1.16 % (3056619)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1631112183:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.54/1.16 % (3056621)Instruction limit reached!
% 3.54/1.16 % (3056621)------------------------------
% 3.54/1.16 % (3056621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056621)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056621)Termination reason: Instruction limit
% 3.54/1.16 % (3056621)Termination phase: Naming
% 3.54/1.16 % (3056621)Time elapsed: 0.003 s
% 3.54/1.16 % (3056621)Peak memory usage: 86 MB
% 3.54/1.16 % (3056621)Instructions burned: 5 (million)
% 3.54/1.16 % (3056620)Instruction limit reached!
% 3.54/1.16 % (3056620)------------------------------
% 3.54/1.16 % (3056620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056620)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056620)Termination reason: Instruction limit
% 3.54/1.16 % (3056620)Termination phase: Property scanning
% 3.54/1.16 % (3056620)Time elapsed: 0.005 s
% 3.54/1.16 % (3056620)Peak memory usage: 86 MB
% 3.54/1.16 % (3056620)Instructions burned: 8 (million)
% 3.54/1.16 % (3056625)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=824170918:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.54/1.16 % (3056623)Instruction limit reached!
% 3.54/1.16 % (3056623)------------------------------
% 3.54/1.16 % (3056623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056623)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056623)Termination reason: Instruction limit
% 3.54/1.16 % (3056623)Termination phase: Saturation
% 3.54/1.16 % (3056623)Time elapsed: 0.043 s
% 3.54/1.16 % (3056623)Peak memory usage: 116 MB
% 3.54/1.16 % (3056623)Instructions burned: 33 (million)
% 3.54/1.16 % (3056625)Instruction limit reached!
% 3.54/1.16 % (3056625)------------------------------
% 3.54/1.16 % (3056625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056625)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056625)Termination reason: Instruction limit
% 3.54/1.16 % (3056625)Termination phase: shuffling
% 3.54/1.16 % (3056625)Time elapsed: 0.004 s
% 3.54/1.16 % (3056625)Peak memory usage: 87 MB
% 3.54/1.16 % (3056625)Instructions burned: 14 (million)
% 3.54/1.16 % (3056622)Instruction limit reached!
% 3.54/1.16 % (3056622)------------------------------
% 3.54/1.16 % (3056622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056622)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056622)Termination reason: Instruction limit
% 3.54/1.16 % (3056622)Termination phase: Saturation
% 3.54/1.16 % (3056622)Time elapsed: 0.054 s
% 3.54/1.16 % (3056622)Peak memory usage: 116 MB
% 3.54/1.16 % (3056622)Instructions burned: 46 (million)
% 3.54/1.16 % (3056618)First to succeed.
% 3.54/1.16 % (3056618)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3056612"
% 3.54/1.16 % (3056635)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3865786231:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.54/1.16 % (3056635)Instruction limit reached!
% 3.54/1.16 % (3056635)------------------------------
% 3.54/1.16 % (3056635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056635)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056635)Termination reason: Instruction limit
% 3.54/1.16 % (3056635)Termination phase: Saturation
% 3.54/1.16 % (3056635)Time elapsed: 0.008 s
% 3.54/1.16 % (3056635)Peak memory usage: 90 MB
% 3.54/1.16 % (3056635)Instructions burned: 24 (million)
% 3.54/1.16 % (3056633)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2263725904:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.54/1.16 % (3056632)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=3769262327:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.54/1.16 % (3056633)Instruction limit reached!
% 3.54/1.16 % (3056633)------------------------------
% 3.54/1.16 % (3056633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056633)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056633)Termination reason: Instruction limit
% 3.54/1.16 % (3056633)Termination phase: Saturation
% 3.54/1.16 % (3056633)Time elapsed: 0.010 s
% 3.54/1.16 % (3056633)Peak memory usage: 89 MB
% 3.54/1.16 % (3056633)Instructions burned: 16 (million)
% 3.54/1.16 % (3056632)Instruction limit reached!
% 3.54/1.16 % (3056632)------------------------------
% 3.54/1.16 % (3056632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056632)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056632)Termination reason: Instruction limit
% 3.54/1.16 % (3056632)Termination phase: Saturation
% 3.54/1.16 % (3056632)Time elapsed: 0.021 s
% 3.54/1.16 % (3056632)Peak memory usage: 89 MB
% 3.54/1.16 % (3056632)Instructions burned: 29 (million)
% 3.54/1.16 % (3056619)Instruction limit reached!
% 3.54/1.16 % (3056619)------------------------------
% 3.54/1.16 % (3056619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056619)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056619)Termination reason: Instruction limit
% 3.54/1.16 % (3056619)Termination phase: Saturation
% 3.54/1.16 % (3056619)Time elapsed: 0.164 s
% 3.54/1.16 % (3056619)Peak memory usage: 118 MB
% 3.54/1.16 % (3056619)Instructions burned: 201 (million)
% 3.54/1.16 % (3056636)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=214156743:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.54/1.16 % (3056637)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4203255828:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.54/1.16 % (3056636)Instruction limit reached!
% 3.54/1.16 % (3056636)------------------------------
% 3.54/1.16 % (3056636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056636)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056636)Termination reason: Instruction limit
% 3.54/1.16 % (3056636)Termination phase: Saturation
% 3.54/1.16 % (3056636)Time elapsed: 0.017 s
% 3.54/1.16 % (3056636)Peak memory usage: 90 MB
% 3.54/1.16 % (3056636)Instructions burned: 28 (million)
% 3.54/1.16 % (3056639)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3253656918:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 3.54/1.16 % (3056639)Instruction limit reached!
% 3.54/1.16 % (3056639)------------------------------
% 3.54/1.16 % (3056639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056639)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056639)Termination reason: Instruction limit
% 3.54/1.16 % (3056639)Termination phase: Preprocessing 1
% 3.54/1.16 % (3056639)Time elapsed: 0.001 s
% 3.54/1.16 % (3056639)Peak memory usage: 85 MB
% 3.54/1.16 % (3056639)Instructions burned: 3 (million)
% 3.54/1.16 % (3056637)Instruction limit reached!
% 3.54/1.16 % (3056637)------------------------------
% 3.54/1.16 % (3056637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056637)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056637)Termination reason: Instruction limit
% 3.54/1.16 % (3056637)Termination phase: Saturation
% 3.54/1.16 % (3056637)Time elapsed: 0.047 s
% 3.54/1.16 % (3056637)Peak memory usage: 89 MB
% 3.54/1.16 % (3056637)Instructions burned: 86 (million)
% 3.54/1.16 % (3056642)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=584887283:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 3.54/1.16 % (3056643)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=155658407:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 3.54/1.16 % (3056645)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=824969135:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 3.54/1.16 % (3056643)Instruction limit reached!
% 3.54/1.16 % (3056643)------------------------------
% 3.54/1.16 % (3056643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056643)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056643)Termination reason: Instruction limit
% 3.54/1.16 % (3056643)Termination phase: Preprocessing 2
% 3.54/1.16 % (3056643)Time elapsed: 0.003 s
% 3.54/1.16 % (3056643)Peak memory usage: 86 MB
% 3.54/1.16 % (3056643)Instructions burned: 5 (million)
% 3.54/1.16 % (3056649)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=2395350499:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 3.54/1.16 % (3056647)lrs+10_1_thi=all:si=on:fd=off:random_seed=3961847637:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 3.54/1.16 % (3056649)Instruction limit reached!
% 3.54/1.16 % (3056649)------------------------------
% 3.54/1.16 % (3056649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.54/1.16 % (3056649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.54/1.16 % (3056649)CaDiCaL version: 2.1.3
% 3.54/1.16 % (3056649)Termination reason: Instruction limit
% 3.54/1.16 % (3056649)Termination phase: Preprocessing 3
% 3.54/1.16 % (3056649)Time elapsed: 0.002 s
% 3.54/1.16 % (3056649)Peak memory usage: 86 MB
% 3.54/1.16 % (3056649)Instructions burned: 8 (million)
% 3.54/1.16 % (3056618)Refutation found. Thanks to Tanya!
% 3.54/1.16 % SZS status Theorem for theBenchmark
% 3.54/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 4.03/1.26 % (3056618)------------------------------
% 4.03/1.26 % (3056618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.03/1.26 % (3056618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/1.26 % (3056618)CaDiCaL version: 2.1.3
% 4.03/1.26 % (3056618)Termination reason: Refutation
% 4.03/1.26 % (3056618)Time elapsed: 0.077 s
% 4.03/1.26 % (3056618)Peak memory usage: 118 MB
% 4.03/1.26 % (3056618)Instructions burned: 78 (million)
% 4.03/1.26 % (3056618)------------------------------
% 4.03/1.26 % (3056618)------------------------------
% 4.03/1.26 % (3056612)Success in time 0.506 s
% 4.03/1.26 % Vampire exiting
%------------------------------------------------------------------------------