%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW596_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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:53 PM UTC 2026
% Result : Theorem 24.98s 4.24s
% Output : Refutation 25.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 25
% Syntax : Number of formulae : 264 ( 77 unt; 0 typ; 12 def)
% Number of atoms : 692 ( 508 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 565 ( 137 ~; 326 |; 48 &)
% ( 0 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 429 ( 122 atm; 83 fun; 76 num; 148 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 : 6 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 56 ( 50 usr; 34 con; 0-5 aty)
% Number of variables : 473 ( 449 !; 24 ?; 473 :)
% 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,
color: $tType ).
tff(type_def_10,type,
map_int_color: $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,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_16,type,
ref: ty > ty ).
tff(func_def_17,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_18,type,
contents: ( ty * uni ) > uni ).
tff(func_def_19,type,
color1: ty ).
tff(func_def_20,type,
blue: color ).
tff(func_def_21,type,
white: color ).
tff(func_def_22,type,
red: color ).
tff(func_def_23,type,
match_color: ( ty * color * uni * uni * uni ) > uni ).
tff(func_def_24,type,
t2tb: map_int_color > uni ).
tff(func_def_25,type,
tb2t: uni > map_int_color ).
tff(func_def_26,type,
t2tb1: color > uni ).
tff(func_def_27,type,
tb2t1: uni > color ).
tff(func_def_28,type,
t2tb2: $int > uni ).
tff(func_def_29,type,
tb2t2: uni > $int ).
tff(func_def_30,type,
nb_occ: ( map_int_color * $int * $int * color ) > $int ).
tff(func_def_35,type,
sK0: $int ).
tff(func_def_36,type,
sK1: $int ).
tff(func_def_37,type,
sK2: map_int_color ).
tff(func_def_38,type,
sK3: map_int_color ).
tff(func_def_39,type,
sK4: map_int_color ).
tff(func_def_40,type,
sK5: $int ).
tff(func_def_41,type,
sK6: color ).
tff(func_def_42,type,
sK7: $int ).
tff(func_def_43,type,
sK8: ( map_int_color * $int * map_int_color * $int ) > $int ).
tff(func_def_44,type,
sF9: uni ).
tff(func_def_45,type,
sF10: uni ).
tff(func_def_46,type,
sF11: uni ).
tff(func_def_47,type,
sF12: uni ).
tff(func_def_48,type,
sF13: uni ).
tff(func_def_49,type,
sF14: map_int_color ).
tff(func_def_50,type,
sF15: uni ).
tff(func_def_51,type,
sF16: uni ).
tff(func_def_52,type,
sF17: uni ).
tff(func_def_53,type,
sF18: map_int_color ).
tff(func_def_54,type,
sF19: $int ).
tff(func_def_55,type,
sF20: $int ).
tff(func_def_56,type,
2: $int > $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
monochrome: ( map_int_color * $int * $int * color ) > $o ).
tff(f9,axiom,
! [X0: ty,X3: uni,X1: ty,X2: uni] : sort(X1,get(X1,X0,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_sort) ).
tff(f10,axiom,
! [X4: uni,X0: ty,X2: uni,X1: ty,X3: uni] : sort(map(X0,X1),set(X1,X0,X2,X3,X4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',set_sort) ).
tff(f11,axiom,
! [X1: ty,X0: ty,X4: uni,X5: uni,X3: uni,X2: uni] :
( sort(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq) ).
tff(f12,axiom,
! [X2: uni,X3: uni,X4: uni,X0: ty,X1: ty] :
( sort(X0,X3)
=> ( sort(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f29,axiom,
! [X0: uni] :
( sort(map(int,color1),X0)
=> ( t2tb(tb2t(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f31,axiom,
! [X0: color] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL1) ).
tff(f32,axiom,
! [X0: uni] :
( sort(color1,X0)
=> ( t2tb1(tb2t1(X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f33,axiom,
! [X0: $int] : sort(int,t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f44,axiom,
! [X3: $int,X1: $int,X4: color,X0: map_int_color,X2: $int] :
( ( $less(X3,X2)
& $lesseq(X1,X3) )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) = X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X4))),X1,X2,X4) = nb_occ(X0,X1,X2,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nb_occ_store_eq_eq) ).
tff(f45,axiom,
! [X2: $int,X4: color,X0: map_int_color,X1: $int,X3: $int] :
( ( $lesseq(X1,X3)
& $less(X3,X2) )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) != X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X4))),X1,X2,X4) = $sum(nb_occ(X0,X1,X2,X4),1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nb_occ_store_eq_neq) ).
tff(f46,axiom,
! [X2: $int,X1: $int,X0: map_int_color,X5: color,X4: color,X3: $int] :
( ( $less(X3,X2)
& $lesseq(X1,X3) )
=> ( ( X4 != X5 )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) = X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X5))),X1,X2,X4) = $difference(nb_occ(X0,X1,X2,X4),1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nb_occ_store_neq_eq) ).
tff(f47,axiom,
! [X2: $int,X4: color,X3: $int,X1: $int,X0: map_int_color,X5: color] :
( ( $lesseq(X1,X3)
& $less(X3,X2) )
=> ( ( X4 != X5 )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) != X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X5))),X1,X2,X4) = nb_occ(X0,X1,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nb_occ_store_neq_neq) ).
tff(f48,conjecture,
! [X2: $int,X1: $int,X3: map_int_color,X0: map_int_color] :
( ( X3 = tb2t(set(color1,int,t2tb(X0),t2tb2(X1),get(color1,int,t2tb(X0),t2tb2(X2)))) )
=> ! [X4: map_int_color] :
( ( X4 = tb2t(set(color1,int,t2tb(X3),t2tb2(X2),get(color1,int,t2tb(X0),t2tb2(X1)))) )
=> ! [X5: $int,X6: $int,X7: color] :
( ( $lesseq(X5,X2)
& $less(X1,X6)
& $lesseq(X5,X1)
& $less(X2,X6) )
=> ( nb_occ(X4,X5,X6,X7) = nb_occ(X0,X5,X6,X7) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_swap) ).
tff(f49,negated_conjecture,
~ ! [X2: $int,X1: $int,X3: map_int_color,X0: map_int_color] :
( ( X3 = tb2t(set(color1,int,t2tb(X0),t2tb2(X1),get(color1,int,t2tb(X0),t2tb2(X2)))) )
=> ! [X4: map_int_color] :
( ( X4 = tb2t(set(color1,int,t2tb(X3),t2tb2(X2),get(color1,int,t2tb(X0),t2tb2(X1)))) )
=> ! [X5: $int,X6: $int,X7: color] :
( ( $lesseq(X5,X2)
& $less(X1,X6)
& $lesseq(X5,X1)
& $less(X2,X6) )
=> ( nb_occ(X4,X5,X6,X7) = nb_occ(X0,X5,X6,X7) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
tff(f51,plain,
! [X2: $int,X1: $int,X0: map_int_color,X5: color,X4: color,X3: $int] :
( ( $less(X3,X2)
& ~ $less(X3,X1) )
=> ( ( X4 != X5 )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) = X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X5))),X1,X2,X4) = $sum(nb_occ(X0,X1,X2,X4),$uminus(1)) ) ) ) ),
inference(theory_normalization,[],[f46]) ).
tff(f54,plain,
~ ! [X2: $int,X1: $int,X3: map_int_color,X0: map_int_color] :
( ( X3 = tb2t(set(color1,int,t2tb(X0),t2tb2(X1),get(color1,int,t2tb(X0),t2tb2(X2)))) )
=> ! [X4: map_int_color] :
( ( X4 = tb2t(set(color1,int,t2tb(X3),t2tb2(X2),get(color1,int,t2tb(X0),t2tb2(X1)))) )
=> ! [X5: $int,X6: $int,X7: color] :
( ( ~ $less(X2,X5)
& $less(X1,X6)
& ~ $less(X1,X5)
& $less(X2,X6) )
=> ( nb_occ(X4,X5,X6,X7) = nb_occ(X0,X5,X6,X7) ) ) ) ),
inference(theory_normalization,[],[f49]) ).
tff(f56,plain,
! [X2: $int,X4: color,X3: $int,X1: $int,X0: map_int_color,X5: color] :
( ( ~ $less(X3,X1)
& $less(X3,X2) )
=> ( ( X4 != X5 )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) != X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X5))),X1,X2,X4) = nb_occ(X0,X1,X2,X4) ) ) ) ),
inference(theory_normalization,[],[f47]) ).
tff(f61,plain,
! [X2: $int,X4: color,X0: map_int_color,X1: $int,X3: $int] :
( ( ~ $less(X3,X1)
& $less(X3,X2) )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) != X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X4))),X1,X2,X4) = $sum(nb_occ(X0,X1,X2,X4),1) ) ) ),
inference(theory_normalization,[],[f45]) ).
tff(f63,plain,
! [X3: $int,X1: $int,X4: color,X0: map_int_color,X2: $int] :
( ( $less(X3,X2)
& ~ $less(X3,X1) )
=> ( ( tb2t1(get(color1,int,t2tb(X0),t2tb2(X3))) = X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(X3),t2tb1(X4))),X1,X2,X4) = nb_occ(X0,X1,X2,X4) ) ) ),
inference(theory_normalization,[],[f44]) ).
tff(f64,plain,
~ ! [X0: $int,X3: map_int_color,X1: $int,X2: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X3),t2tb2(X1),get(color1,int,t2tb(X3),t2tb2(X0)))) = X2 )
=> ! [X4: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X2),t2tb2(X0),get(color1,int,t2tb(X3),t2tb2(X1)))) = X4 )
=> ! [X6: $int,X5: $int,X7: color] :
( ( ~ $less(X0,X5)
& ~ $less(X1,X5)
& $less(X0,X6)
& $less(X1,X6) )
=> ( nb_occ(X4,X5,X6,X7) = nb_occ(X3,X5,X6,X7) ) ) ) ),
inference(rectify,[],[f54]) ).
tff(f65,plain,
! [X0: $int,X3: map_int_color,X1: $int,X4: $int,X2: color] :
( ( ~ $less(X0,X1)
& $less(X0,X4) )
=> ( ( tb2t1(get(color1,int,t2tb(X3),t2tb2(X0))) = X2 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X3),t2tb2(X0),t2tb1(X2))),X1,X4,X2) = nb_occ(X3,X1,X4,X2) ) ) ),
inference(rectify,[],[f63]) ).
tff(f67,plain,
! [X5: uni,X0: ty,X2: uni,X1: ty,X3: uni,X4: uni] :
( sort(X0,X3)
=> ( ( X2 = X4 )
=> ( get(X0,X1,set(X0,X1,X5,X4,X3),X2) = X3 ) ) ),
inference(rectify,[],[f11]) ).
tff(f68,plain,
! [X5: color,X1: color,X3: $int,X0: $int,X2: $int,X4: map_int_color] :
( ( $less(X2,X0)
& ~ $less(X2,X3) )
=> ( ( X1 != X5 )
=> ( ( tb2t1(get(color1,int,t2tb(X4),t2tb2(X2))) != X1 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X4),t2tb2(X2),t2tb1(X5))),X3,X0,X1) = nb_occ(X4,X3,X0,X1) ) ) ) ),
inference(rectify,[],[f56]) ).
tff(f70,plain,
! [X4: ty,X1: uni,X0: uni,X2: uni,X3: ty] :
( sort(X3,X1)
=> ( sort(X3,X2)
=> ! [X5: uni] :
( ( X1 != X2 )
=> ( get(X4,X3,set(X4,X3,X0,X1,X5),X2) = get(X4,X3,X0,X2) ) ) ) ),
inference(rectify,[],[f12]) ).
tff(f73,plain,
! [X1: color,X2: map_int_color,X4: $int,X0: $int,X3: $int] :
( ( ~ $less(X4,X3)
& $less(X4,X0) )
=> ( ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X4))) != X1 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X4),t2tb1(X1))),X3,X0,X1) = $sum(nb_occ(X2,X3,X0,X1),1) ) ) ),
inference(rectify,[],[f61]) ).
tff(f75,plain,
! [X4: color,X3: color,X0: $int,X1: $int,X5: $int,X2: map_int_color] :
( ( ~ $less(X5,X1)
& $less(X5,X0) )
=> ( ( X3 != X4 )
=> ( ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X5))) = X4 )
=> ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X5),t2tb1(X3))),X1,X0,X4) = $sum(nb_occ(X2,X1,X0,X4),$uminus(1)) ) ) ) ),
inference(rectify,[],[f51]) ).
tff(f77,plain,
! [X0: ty,X3: uni,X2: ty,X1: uni] : sort(X2,get(X2,X0,X3,X1)),
inference(rectify,[],[f9]) ).
tff(f78,plain,
! [X0: uni,X3: ty,X2: uni,X4: uni,X1: ty] : sort(map(X1,X3),set(X3,X1,X2,X4,X0)),
inference(rectify,[],[f10]) ).
tff(f83,plain,
! [X5: color,X1: color,X3: $int,X0: $int,X2: $int,X4: map_int_color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X4),t2tb2(X2),t2tb1(X5))),X3,X0,X1) = nb_occ(X4,X3,X0,X1) )
| ( tb2t1(get(color1,int,t2tb(X4),t2tb2(X2))) = X1 )
| ( X1 = X5 )
| ~ $less(X2,X0)
| $less(X2,X3) ),
inference(ennf_transformation,[],[f68]) ).
tff(f84,plain,
! [X0: $int,X3: $int,X1: color,X4: map_int_color,X5: color,X2: $int] :
( ~ $less(X2,X0)
| ( X1 = X5 )
| ( tb2t1(get(color1,int,t2tb(X4),t2tb2(X2))) = X1 )
| $less(X2,X3)
| ( nb_occ(tb2t(set(color1,int,t2tb(X4),t2tb2(X2),t2tb1(X5))),X3,X0,X1) = nb_occ(X4,X3,X0,X1) ) ),
inference(flattening,[],[f83]) ).
tff(f89,plain,
! [X5: uni,X0: ty,X2: uni,X1: ty,X3: uni,X4: uni] :
( ( get(X0,X1,set(X0,X1,X5,X4,X3),X2) = X3 )
| ( X2 != X4 )
| ~ sort(X0,X3) ),
inference(ennf_transformation,[],[f67]) ).
tff(f90,plain,
! [X3: uni,X4: uni,X1: ty,X2: uni,X5: uni,X0: ty] :
( ( X2 != X4 )
| ~ sort(X0,X3)
| ( get(X0,X1,set(X0,X1,X5,X4,X3),X2) = X3 ) ),
inference(flattening,[],[f89]) ).
tff(f91,plain,
! [X0: $int,X3: map_int_color,X1: $int,X4: $int,X2: color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X3),t2tb2(X0),t2tb1(X2))),X1,X4,X2) = nb_occ(X3,X1,X4,X2) )
| ( tb2t1(get(color1,int,t2tb(X3),t2tb2(X0))) != X2 )
| $less(X0,X1)
| ~ $less(X0,X4) ),
inference(ennf_transformation,[],[f65]) ).
tff(f92,plain,
! [X4: $int,X3: map_int_color,X0: $int,X2: color,X1: $int] :
( $less(X0,X1)
| ( nb_occ(tb2t(set(color1,int,t2tb(X3),t2tb2(X0),t2tb1(X2))),X1,X4,X2) = nb_occ(X3,X1,X4,X2) )
| ~ $less(X0,X4)
| ( tb2t1(get(color1,int,t2tb(X3),t2tb2(X0))) != X2 ) ),
inference(flattening,[],[f91]) ).
tff(f95,plain,
? [X0: $int,X3: map_int_color,X1: $int,X2: map_int_color] :
( ? [X4: map_int_color] :
( ? [X6: $int,X5: $int,X7: color] :
( ( nb_occ(X4,X5,X6,X7) != nb_occ(X3,X5,X6,X7) )
& ~ $less(X0,X5)
& ~ $less(X1,X5)
& $less(X0,X6)
& $less(X1,X6) )
& ( tb2t(set(color1,int,t2tb(X2),t2tb2(X0),get(color1,int,t2tb(X3),t2tb2(X1)))) = X4 ) )
& ( tb2t(set(color1,int,t2tb(X3),t2tb2(X1),get(color1,int,t2tb(X3),t2tb2(X0)))) = X2 ) ),
inference(ennf_transformation,[],[f64]) ).
tff(f96,plain,
? [X1: $int,X0: $int,X2: map_int_color,X3: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X3),t2tb2(X1),get(color1,int,t2tb(X3),t2tb2(X0)))) = X2 )
& ? [X4: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X2),t2tb2(X0),get(color1,int,t2tb(X3),t2tb2(X1)))) = X4 )
& ? [X6: $int,X7: color,X5: $int] :
( $less(X1,X6)
& ~ $less(X0,X5)
& ( nb_occ(X4,X5,X6,X7) != nb_occ(X3,X5,X6,X7) )
& $less(X0,X6)
& ~ $less(X1,X5) ) ) ),
inference(flattening,[],[f95]) ).
tff(f102,plain,
! [X0: uni] :
( ~ sort(color1,X0)
| ( t2tb1(tb2t1(X0)) = X0 ) ),
inference(ennf_transformation,[],[f32]) ).
tff(f103,plain,
! [X1: color,X2: map_int_color,X4: $int,X0: $int,X3: $int] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X4),t2tb1(X1))),X3,X0,X1) = $sum(nb_occ(X2,X3,X0,X1),1) )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X4))) = X1 )
| $less(X4,X3)
| ~ $less(X4,X0) ),
inference(ennf_transformation,[],[f73]) ).
tff(f104,plain,
! [X4: $int,X0: $int,X2: map_int_color,X1: color,X3: $int] :
( ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X4))) = X1 )
| ~ $less(X4,X0)
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X4),t2tb1(X1))),X3,X0,X1) = $sum(nb_occ(X2,X3,X0,X1),1) )
| $less(X4,X3) ),
inference(flattening,[],[f103]) ).
tff(f105,plain,
! [X4: color,X3: color,X0: $int,X1: $int,X5: $int,X2: map_int_color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X5),t2tb1(X3))),X1,X0,X4) = $sum(nb_occ(X2,X1,X0,X4),$uminus(1)) )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X5))) != X4 )
| ( X3 = X4 )
| $less(X5,X1)
| ~ $less(X5,X0) ),
inference(ennf_transformation,[],[f75]) ).
tff(f106,plain,
! [X1: $int,X3: color,X5: $int,X0: $int,X4: color,X2: map_int_color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X5),t2tb1(X3))),X1,X0,X4) = $sum(nb_occ(X2,X1,X0,X4),$uminus(1)) )
| ( X3 = X4 )
| ~ $less(X5,X0)
| $less(X5,X1)
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X5))) != X4 ) ),
inference(flattening,[],[f105]) ).
tff(f107,plain,
! [X0: uni] :
( ( t2tb(tb2t(X0)) = X0 )
| ~ sort(map(int,color1),X0) ),
inference(ennf_transformation,[],[f29]) ).
tff(f108,plain,
! [X4: ty,X1: uni,X0: uni,X2: uni,X3: ty] :
( ! [X5: uni] :
( ( get(X4,X3,set(X4,X3,X0,X1,X5),X2) = get(X4,X3,X0,X2) )
| ( X1 = X2 ) )
| ~ sort(X3,X2)
| ~ sort(X3,X1) ),
inference(ennf_transformation,[],[f70]) ).
tff(f109,plain,
! [X4: ty,X0: uni,X2: uni,X1: uni,X3: ty] :
( ~ sort(X3,X1)
| ! [X5: uni] :
( ( get(X4,X3,set(X4,X3,X0,X1,X5),X2) = get(X4,X3,X0,X2) )
| ( X1 = X2 ) )
| ~ sort(X3,X2) ),
inference(flattening,[],[f108]) ).
tff(f110,plain,
! [X0: ty,X1: uni,X2: ty,X3: uni] : sort(X2,get(X2,X0,X1,X3)),
inference(rectify,[],[f77]) ).
tff(f112,plain,
! [X0: $int,X1: map_int_color,X2: $int,X3: color,X4: $int] :
( $less(X2,X4)
| ( nb_occ(X1,X4,X0,X3) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(X2),t2tb1(X3))),X4,X0,X3) )
| ~ $less(X2,X0)
| ( tb2t1(get(color1,int,t2tb(X1),t2tb2(X2))) != X3 ) ),
inference(rectify,[],[f92]) ).
tff(f114,plain,
? [X0: $int,X1: $int,X2: map_int_color,X3: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X3),t2tb2(X0),get(color1,int,t2tb(X3),t2tb2(X1)))) = X2 )
& ? [X4: map_int_color] :
( ( tb2t(set(color1,int,t2tb(X2),t2tb2(X1),get(color1,int,t2tb(X3),t2tb2(X0)))) = X4 )
& ? [X5: $int,X6: color,X7: $int] :
( $less(X0,X5)
& ~ $less(X1,X7)
& ( nb_occ(X4,X7,X5,X6) != nb_occ(X3,X7,X5,X6) )
& $less(X1,X5)
& ~ $less(X0,X7) ) ) ),
inference(rectify,[],[f96]) ).
tff(f115,plain,
( ( sK2 = tb2t(set(color1,int,t2tb(sK3),t2tb2(sK0),get(color1,int,t2tb(sK3),t2tb2(sK1)))) )
& ( sK4 = tb2t(set(color1,int,t2tb(sK2),t2tb2(sK1),get(color1,int,t2tb(sK3),t2tb2(sK0)))) )
& $less(sK0,sK5)
& ~ $less(sK1,sK7)
& ( nb_occ(sK3,sK7,sK5,sK6) != nb_occ(sK4,sK7,sK5,sK6) )
& $less(sK1,sK5)
& ~ $less(sK0,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7)],[f114]) ).
tff(f118,plain,
! [X0: $int,X1: $int,X2: color,X3: map_int_color,X4: color,X5: $int] :
( ~ $less(X5,X0)
| ( X2 = X4 )
| ( tb2t1(get(color1,int,t2tb(X3),t2tb2(X5))) = X2 )
| $less(X5,X1)
| ( nb_occ(tb2t(set(color1,int,t2tb(X3),t2tb2(X5),t2tb1(X4))),X1,X0,X2) = nb_occ(X3,X1,X0,X2) ) ),
inference(rectify,[],[f84]) ).
tff(f120,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni,X4: ty] :
( ~ sort(X4,X3)
| ! [X5: uni] :
( ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) )
| ( X2 = X3 ) )
| ~ sort(X4,X2) ),
inference(rectify,[],[f109]) ).
tff(f122,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni,X4: ty] : sort(map(X4,X1),set(X1,X4,X2,X3,X0)),
inference(rectify,[],[f78]) ).
tff(f123,plain,
! [X0: $int,X1: $int,X2: map_int_color,X3: color,X4: $int] :
( ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X0))) = X3 )
| ~ $less(X0,X1)
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X0),t2tb1(X3))),X4,X1,X3) = $sum(nb_occ(X2,X4,X1,X3),1) )
| $less(X0,X4) ),
inference(rectify,[],[f104]) ).
tff(f126,plain,
! [X0: $int,X1: color,X2: $int,X3: $int,X4: color,X5: map_int_color] :
( ( $sum(nb_occ(X5,X0,X3,X4),$uminus(1)) = nb_occ(tb2t(set(color1,int,t2tb(X5),t2tb2(X2),t2tb1(X1))),X0,X3,X4) )
| ( X1 = X4 )
| ~ $less(X2,X3)
| $less(X2,X0)
| ( tb2t1(get(color1,int,t2tb(X5),t2tb2(X2))) != X4 ) ),
inference(rectify,[],[f106]) ).
tff(f127,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni,X4: uni,X5: ty] :
( ( X1 != X3 )
| ~ sort(X5,X0)
| ( get(X5,X2,set(X5,X2,X4,X1,X0),X3) = X0 ) ),
inference(rectify,[],[f90]) ).
tff(f129,plain,
! [X2: ty,X3: uni,X0: ty,X1: uni] : sort(X2,get(X2,X0,X1,X3)),
inference(cnf_transformation,[],[f110]) ).
tff(f131,plain,
! [X2: $int,X3: color,X0: $int,X1: map_int_color,X4: $int] :
( $less(X2,X4)
| ( nb_occ(X1,X4,X0,X3) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(X2),t2tb1(X3))),X4,X0,X3) )
| ~ $less(X2,X0)
| ( tb2t1(get(color1,int,t2tb(X1),t2tb2(X2))) != X3 ) ),
inference(cnf_transformation,[],[f112]) ).
tff(f135,plain,
~ $less(sK0,sK7),
inference(cnf_transformation,[],[f115]) ).
tff(f136,plain,
$less(sK1,sK5),
inference(cnf_transformation,[],[f115]) ).
tff(f137,plain,
nb_occ(sK3,sK7,sK5,sK6) != nb_occ(sK4,sK7,sK5,sK6),
inference(cnf_transformation,[],[f115]) ).
tff(f138,plain,
~ $less(sK1,sK7),
inference(cnf_transformation,[],[f115]) ).
tff(f139,plain,
$less(sK0,sK5),
inference(cnf_transformation,[],[f115]) ).
tff(f140,plain,
sK4 = tb2t(set(color1,int,t2tb(sK2),t2tb2(sK1),get(color1,int,t2tb(sK3),t2tb2(sK0)))),
inference(cnf_transformation,[],[f115]) ).
tff(f141,plain,
sK2 = tb2t(set(color1,int,t2tb(sK3),t2tb2(sK0),get(color1,int,t2tb(sK3),t2tb2(sK1)))),
inference(cnf_transformation,[],[f115]) ).
tff(f145,plain,
! [X0: $int] : sort(int,t2tb2(X0)),
inference(cnf_transformation,[],[f33]) ).
tff(f146,plain,
! [X2: color,X3: map_int_color,X0: $int,X1: $int,X4: color,X5: $int] :
( $less(X5,X1)
| ( X2 = X4 )
| ( nb_occ(tb2t(set(color1,int,t2tb(X3),t2tb2(X5),t2tb1(X4))),X1,X0,X2) = nb_occ(X3,X1,X0,X2) )
| ~ $less(X5,X0)
| ( tb2t1(get(color1,int,t2tb(X3),t2tb2(X5))) = X2 ) ),
inference(cnf_transformation,[],[f118]) ).
tff(f148,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni,X4: ty,X5: uni] :
( ( get(X0,X4,set(X0,X4,X1,X3,X5),X2) = get(X0,X4,X1,X2) )
| ( X2 = X3 )
| ~ sort(X4,X3)
| ~ sort(X4,X2) ),
inference(cnf_transformation,[],[f120]) ).
tff(f151,plain,
! [X0: uni] :
( ~ sort(map(int,color1),X0)
| ( t2tb(tb2t(X0)) = X0 ) ),
inference(cnf_transformation,[],[f107]) ).
tff(f152,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: ty] : sort(map(X4,X1),set(X1,X4,X2,X3,X0)),
inference(cnf_transformation,[],[f122]) ).
tff(f153,plain,
! [X2: map_int_color,X3: color,X0: $int,X1: $int,X4: $int] :
( $less(X0,X4)
| ~ $less(X0,X1)
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X0))) = X3 )
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X0),t2tb1(X3))),X4,X1,X3) = $sum(nb_occ(X2,X4,X1,X3),1) ) ),
inference(cnf_transformation,[],[f123]) ).
tff(f155,plain,
! [X0: color] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f31]) ).
tff(f157,plain,
! [X2: $int,X3: $int,X0: $int,X1: color,X4: color,X5: map_int_color] :
( ( $sum(nb_occ(X5,X0,X3,X4),$uminus(1)) = nb_occ(tb2t(set(color1,int,t2tb(X5),t2tb2(X2),t2tb1(X1))),X0,X3,X4) )
| ( X1 = X4 )
| ~ $less(X2,X3)
| $less(X2,X0)
| ( tb2t1(get(color1,int,t2tb(X5),t2tb2(X2))) != X4 ) ),
inference(cnf_transformation,[],[f126]) ).
tff(f158,plain,
! [X0: uni] :
( ( t2tb1(tb2t1(X0)) = X0 )
| ~ sort(color1,X0) ),
inference(cnf_transformation,[],[f102]) ).
tff(f159,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni,X4: uni,X5: ty] :
( ( X1 != X3 )
| ~ sort(X5,X0)
| ( get(X5,X2,set(X5,X2,X4,X1,X0),X3) = X0 ) ),
inference(cnf_transformation,[],[f127]) ).
tff(f161,plain,
! [X2: $int,X0: $int,X1: map_int_color,X4: $int] :
( $less(X2,X4)
| ~ $less(X2,X0)
| ( nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(X2),t2tb1(tb2t1(get(color1,int,t2tb(X1),t2tb2(X2)))))),X4,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(X2)))) = nb_occ(X1,X4,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(X2)))) ) ),
inference(equality_resolution,[],[f131]) ).
tff(f163,plain,
! [X2: $int,X3: $int,X0: $int,X1: color,X5: map_int_color] :
( $less(X2,X0)
| ( $sum(nb_occ(X5,X0,X3,tb2t1(get(color1,int,t2tb(X5),t2tb2(X2)))),$uminus(1)) = nb_occ(tb2t(set(color1,int,t2tb(X5),t2tb2(X2),t2tb1(X1))),X0,X3,tb2t1(get(color1,int,t2tb(X5),t2tb2(X2)))) )
| ( tb2t1(get(color1,int,t2tb(X5),t2tb2(X2))) = X1 )
| ~ $less(X2,X3) ),
inference(equality_resolution,[],[f157]) ).
tff(f164,plain,
! [X2: ty,X3: uni,X0: uni,X4: uni,X5: ty] :
( ( get(X5,X2,set(X5,X2,X4,X3,X0),X3) = X0 )
| ~ sort(X5,X0) ),
inference(equality_resolution,[],[f159]) ).
tff(f165,definition,
sF9 = t2tb(sK3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f166,definition,
sF10 = t2tb2(sK0),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f167,definition,
sF11 = t2tb2(sK1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f168,plain,
t2tb2(sK1) = sF11,
inference(reorient_equations,[],[f167]) ).
tff(f169,definition,
sF12 = get(color1,int,sF9,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f170,definition,
sF13 = set(color1,int,sF9,sF10,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f171,plain,
set(color1,int,sF9,sF10,sF12) = sF13,
inference(reorient_equations,[],[f170]) ).
tff(f172,definition,
sF14 = tb2t(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f173,plain,
sF14 = sK2,
inference(definition_folding,[],[f141,f172,f171,f169,f168,f165,f166,f165]) ).
tff(f174,definition,
sF15 = t2tb(sK2),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f175,definition,
sF16 = get(color1,int,sF9,sF10),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f176,plain,
get(color1,int,sF9,sF10) = sF16,
inference(reorient_equations,[],[f175]) ).
tff(f177,definition,
sF17 = set(color1,int,sF15,sF11,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f178,definition,
sF18 = tb2t(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f179,plain,
tb2t(sF17) = sF18,
inference(reorient_equations,[],[f178]) ).
tff(f180,plain,
sK4 = sF18,
inference(definition_folding,[],[f140,f179,f177,f176,f166,f165,f168,f174]) ).
tff(f181,definition,
sF19 = nb_occ(sK3,sK7,sK5,sK6),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f182,plain,
nb_occ(sK3,sK7,sK5,sK6) = sF19,
inference(reorient_equations,[],[f181]) ).
tff(f183,definition,
sF20 = nb_occ(sK4,sK7,sK5,sK6),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f184,plain,
sF20 != sF19,
inference(definition_folding,[],[f137,f183,f182]) ).
tff(f185,plain,
sort(int,sF10),
inference(constrained_superposition,[],[f145,f166]) ).
tff(f186,plain,
sort(int,sF11),
inference(constrained_superposition,[],[f145,f168]) ).
tff(f187,plain,
t2tb(sF14) = sF15,
inference(forward_demodulation,[],[f174,f173]) ).
tff(f188,plain,
sK4 = tb2t(sF17),
inference(forward_demodulation,[],[f179,f180]) ).
tff(f193,plain,
sort(color1,sF12),
inference(constrained_superposition,[],[f129,f169]) ).
tff(f194,plain,
sort(color1,sF16),
inference(constrained_superposition,[],[f129,f176]) ).
tff(f204,plain,
sort(map(int,color1),sF13),
inference(constrained_superposition,[],[f152,f171]) ).
tff(f206,plain,
t2tb(tb2t(sF13)) = sF13,
inference(resolution,[],[f204,f151]) ).
tff(f207,plain,
t2tb(sF14) = sF13,
inference(forward_demodulation,[],[f206,f172]) ).
tff(f208,plain,
sF13 = sF15,
inference(forward_demodulation,[],[f207,f187]) ).
tff(f217,plain,
( ~ sort(color1,sF12)
| ( sF12 = get(color1,int,sF13,sF10) ) ),
inference(constrained_superposition,[],[f164,f171]) ).
tff(f220,plain,
sF12 = get(color1,int,sF13,sF10),
inference(forward_subsumption_resolution,[],[f217,f193]) ).
tff(f222,plain,
sF12 = get(color1,int,sF15,sF10),
inference(forward_demodulation,[],[f220,f208]) ).
tff(f262,plain,
! [X0: uni] :
( ~ sort(int,sF10)
| ( sF10 = X0 )
| ( get(color1,int,sF9,X0) = get(color1,int,sF13,X0) )
| ~ sort(int,X0) ),
inference(constrained_superposition,[],[f148,f171]) ).
tff(f266,plain,
! [X0: uni] :
( ( get(color1,int,sF9,X0) = get(color1,int,sF13,X0) )
| ~ sort(int,X0)
| ( sF10 = X0 ) ),
inference(forward_subsumption_resolution,[],[f262,f185]) ).
tff(f268,plain,
! [X0: uni] :
( ( get(color1,int,sF15,X0) = get(color1,int,sF9,X0) )
| ~ sort(int,X0)
| ( sF10 = X0 ) ),
inference(forward_demodulation,[],[f266,f208]) ).
tff(f515,plain,
! [X2: map_int_color,X3: color,X0: $int,X1: $int,X4: $int] :
( $less(X0,X4)
| ~ $less(X0,X1)
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(X0))) = X3 )
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(X0),t2tb1(X3))),X4,X1,X3) = $sum(1,nb_occ(X2,X4,X1,X3)) ) ),
inference(evaluation,[],[f153]) ).
tff(f592,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ( tb2t1(get(color1,int,t2tb(X1),t2tb2(sK0))) = X2 )
| ~ $less(sK0,X0)
| ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK0),t2tb1(X2))),sK7,X0,X2) ) ),
inference(resolution,[],[f515,f135]) ).
tff(f593,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ~ $less(sK1,X0)
| ( tb2t1(get(color1,int,t2tb(X1),t2tb2(sK1))) = X2 )
| ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK1),t2tb1(X2))),sK7,X0,X2) ) ),
inference(resolution,[],[f515,f138]) ).
tff(f597,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ( tb2t1(get(color1,int,t2tb(X1),sF11)) = X2 )
| ~ $less(sK1,X0)
| ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK1),t2tb1(X2))),sK7,X0,X2) ) ),
inference(forward_demodulation,[],[f593,f168]) ).
tff(f598,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK0),t2tb1(X2))),sK7,X0,X2) )
| ( tb2t1(get(color1,int,t2tb(X1),sF10)) = X2 )
| ~ $less(sK0,X0) ),
inference(forward_demodulation,[],[f592,f166]) ).
tff(f599,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ~ $less(sK1,X0)
| ( tb2t1(get(color1,int,t2tb(X1),sF11)) = X2 )
| ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),sF11,t2tb1(X2))),sK7,X0,X2) ) ),
inference(forward_demodulation,[],[f597,f168]) ).
tff(f600,plain,
! [X2: color,X0: $int,X1: map_int_color] :
( ~ $less(sK0,X0)
| ( tb2t1(get(color1,int,t2tb(X1),sF10)) = X2 )
| ( $sum(1,nb_occ(X1,sK7,X0,X2)) = nb_occ(tb2t(set(color1,int,t2tb(X1),sF10,t2tb1(X2))),sK7,X0,X2) ) ),
inference(forward_demodulation,[],[f598,f166]) ).
tff(f610,plain,
! [X0: map_int_color,X1: color] :
( ( $sum(1,nb_occ(X0,sK7,sK5,X1)) = nb_occ(tb2t(set(color1,int,t2tb(X0),sF11,t2tb1(X1))),sK7,sK5,X1) )
| ( tb2t1(get(color1,int,t2tb(X0),sF11)) = X1 ) ),
inference(resolution,[],[f599,f136]) ).
tff(f620,plain,
! [X0: color] :
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,X0) = $sum(1,nb_occ(sF14,sK7,sK5,X0)) )
| ( tb2t1(get(color1,int,sF15,sF11)) = X0 ) ),
inference(constrained_superposition,[],[f610,f187]) ).
tff(f626,plain,
! [X0: uni] :
( ( $sum(1,nb_occ(sF14,sK7,sK5,tb2t1(X0))) = nb_occ(tb2t(set(color1,int,sF15,sF11,X0)),sK7,sK5,tb2t1(X0)) )
| ~ sort(color1,X0)
| ( tb2t1(X0) = tb2t1(get(color1,int,sF15,sF11)) ) ),
inference(constrained_superposition,[],[f620,f158]) ).
tff(f638,plain,
! [X0: map_int_color,X1: color] :
( ( $sum(1,nb_occ(X0,sK7,sK5,X1)) = nb_occ(tb2t(set(color1,int,t2tb(X0),sF10,t2tb1(X1))),sK7,sK5,X1) )
| ( tb2t1(get(color1,int,t2tb(X0),sF10)) = X1 ) ),
inference(resolution,[],[f600,f139]) ).
tff(f646,plain,
! [X0: color] :
( ( $sum(1,nb_occ(sK3,sK7,sK5,X0)) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,X0) )
| ( tb2t1(get(color1,int,sF9,sF10)) = X0 ) ),
inference(constrained_superposition,[],[f638,f165]) ).
tff(f650,plain,
! [X0: color] :
( ( $sum(1,nb_occ(sK3,sK7,sK5,X0)) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,X0) )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f646,f176]) ).
tff(f659,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ( nb_occ(X2,sK7,X3,X0) = nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(sK0),t2tb1(X1))),sK7,X3,X0) )
| ( X0 = X1 )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(sK0))) = X0 )
| ~ $less(sK0,X3) ),
inference(resolution,[],[f146,f135]) ).
tff(f660,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ( X0 = X1 )
| ~ $less(sK1,X3)
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),t2tb2(sK1),t2tb1(X1))),sK7,X3,X0) = nb_occ(X2,sK7,X3,X0) )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(sK1))) = X0 ) ),
inference(resolution,[],[f146,f138]) ).
tff(f666,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ( X0 = X1 )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(sK0))) = X0 )
| ~ $less(sK0,X3)
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),sF10,t2tb1(X1))),sK7,X3,X0) = nb_occ(X2,sK7,X3,X0) ) ),
inference(forward_demodulation,[],[f659,f166]) ).
tff(f667,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ~ $less(sK1,X3)
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),sF11,t2tb1(X1))),sK7,X3,X0) = nb_occ(X2,sK7,X3,X0) )
| ( tb2t1(get(color1,int,t2tb(X2),t2tb2(sK1))) = X0 )
| ( X0 = X1 ) ),
inference(forward_demodulation,[],[f660,f168]) ).
tff(f670,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ~ $less(sK0,X3)
| ( tb2t1(get(color1,int,t2tb(X2),sF10)) = X0 )
| ( X0 = X1 )
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),sF10,t2tb1(X1))),sK7,X3,X0) = nb_occ(X2,sK7,X3,X0) ) ),
inference(forward_demodulation,[],[f666,f166]) ).
tff(f671,plain,
! [X2: map_int_color,X3: $int,X0: color,X1: color] :
( ~ $less(sK1,X3)
| ( X0 = X1 )
| ( nb_occ(tb2t(set(color1,int,t2tb(X2),sF11,t2tb1(X1))),sK7,X3,X0) = nb_occ(X2,sK7,X3,X0) )
| ( tb2t1(get(color1,int,t2tb(X2),sF11)) = X0 ) ),
inference(forward_demodulation,[],[f667,f168]) ).
tff(f711,plain,
( ( tb2t1(get(color1,int,sF15,sF11)) = tb2t1(sF16) )
| ( nb_occ(tb2t(sF17),sK7,sK5,tb2t1(sF16)) = $sum(1,nb_occ(sF14,sK7,sK5,tb2t1(sF16))) )
| ~ sort(color1,sF16) ),
inference(constrained_superposition,[],[f626,f177]) ).
tff(f713,plain,
( ( nb_occ(tb2t(sF17),sK7,sK5,tb2t1(sF16)) = $sum(1,nb_occ(sF14,sK7,sK5,tb2t1(sF16))) )
| ( tb2t1(get(color1,int,sF15,sF11)) = tb2t1(sF16) ) ),
inference(forward_subsumption_resolution,[],[f711,f194]) ).
tff(f714,plain,
( ( nb_occ(sK4,sK7,sK5,tb2t1(sF16)) = $sum(1,nb_occ(sF14,sK7,sK5,tb2t1(sF16))) )
| ( tb2t1(get(color1,int,sF15,sF11)) = tb2t1(sF16) ) ),
inference(forward_demodulation,[],[f713,f188]) ).
tff(f725,plain,
! [X2: color,X0: map_int_color,X1: color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X0),sF10,t2tb1(X2))),sK7,sK5,X1) = nb_occ(X0,sK7,sK5,X1) )
| ( tb2t1(get(color1,int,t2tb(X0),sF10)) = X1 )
| ( X1 = X2 ) ),
inference(resolution,[],[f670,f139]) ).
tff(f735,plain,
! [X0: color,X1: color] :
( ( nb_occ(sK3,sK7,sK5,X1) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,X1) )
| ( tb2t1(get(color1,int,sF9,sF10)) = X1 )
| ( X0 = X1 ) ),
inference(constrained_superposition,[],[f725,f165]) ).
tff(f740,plain,
! [X0: color,X1: color] :
( ( nb_occ(sK3,sK7,sK5,X1) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,X1) )
| ( X0 = X1 )
| ( tb2t1(sF16) = X1 ) ),
inference(forward_demodulation,[],[f735,f176]) ).
tff(f747,plain,
! [X0: uni,X1: color] :
( ~ sort(color1,X0)
| ( tb2t1(X0) = X1 )
| ( nb_occ(sK3,sK7,sK5,X1) = nb_occ(tb2t(set(color1,int,sF9,sF10,X0)),sK7,sK5,X1) )
| ( tb2t1(sF16) = X1 ) ),
inference(constrained_superposition,[],[f740,f158]) ).
tff(f759,plain,
! [X0: color] :
( ( tb2t1(sF12) = X0 )
| ( nb_occ(sK3,sK7,sK5,X0) = nb_occ(tb2t(set(color1,int,sF9,sF10,sF12)),sK7,sK5,X0) )
| ( tb2t1(sF16) = X0 ) ),
inference(resolution,[],[f747,f193]) ).
tff(f763,plain,
! [X0: color] :
( ( tb2t1(sF12) = X0 )
| ( nb_occ(sK3,sK7,sK5,X0) = nb_occ(tb2t(sF13),sK7,sK5,X0) )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f759,f171]) ).
tff(f765,plain,
! [X0: color] :
( ( nb_occ(sK3,sK7,sK5,X0) = nb_occ(sF14,sK7,sK5,X0) )
| ( tb2t1(sF12) = X0 )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f763,f172]) ).
tff(f766,plain,
( ( nb_occ(sF14,sK7,sK5,sK6) = sF19 )
| ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(sF12) ) ),
inference(constrained_superposition,[],[f765,f182]) ).
tff(f861,plain,
! [X0: $int,X1: map_int_color] :
( ~ $less(sK0,X0)
| ( nb_occ(X1,sK7,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(sK0)))) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK0),t2tb1(tb2t1(get(color1,int,t2tb(X1),t2tb2(sK0)))))),sK7,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(sK0)))) ) ),
inference(resolution,[],[f161,f135]) ).
tff(f862,plain,
! [X0: $int,X1: map_int_color] :
( ~ $less(sK1,X0)
| ( nb_occ(X1,sK7,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(sK1)))) = nb_occ(tb2t(set(color1,int,t2tb(X1),t2tb2(sK1),t2tb1(tb2t1(get(color1,int,t2tb(X1),t2tb2(sK1)))))),sK7,X0,tb2t1(get(color1,int,t2tb(X1),t2tb2(sK1)))) ) ),
inference(resolution,[],[f161,f138]) ).
tff(f866,plain,
! [X0: $int,X1: map_int_color] :
( ~ $less(sK1,X0)
| ( nb_occ(X1,sK7,X0,tb2t1(get(color1,int,t2tb(X1),sF11))) = nb_occ(tb2t(set(color1,int,t2tb(X1),sF11,t2tb1(tb2t1(get(color1,int,t2tb(X1),sF11))))),sK7,X0,tb2t1(get(color1,int,t2tb(X1),sF11))) ) ),
inference(forward_demodulation,[],[f862,f168]) ).
tff(f870,plain,
! [X0: $int,X1: map_int_color] :
( ~ $less(sK0,X0)
| ( nb_occ(X1,sK7,X0,tb2t1(get(color1,int,t2tb(X1),sF10))) = nb_occ(tb2t(set(color1,int,t2tb(X1),sF10,t2tb1(tb2t1(get(color1,int,t2tb(X1),sF10))))),sK7,X0,tb2t1(get(color1,int,t2tb(X1),sF10))) ) ),
inference(forward_demodulation,[],[f861,f166]) ).
tff(f941,plain,
! [X2: map_int_color,X0: color,X1: color] :
( ( nb_occ(X2,sK7,sK5,X0) = nb_occ(tb2t(set(color1,int,t2tb(X2),sF11,t2tb1(X1))),sK7,sK5,X0) )
| ( X0 = X1 )
| ( tb2t1(get(color1,int,t2tb(X2),sF11)) = X0 ) ),
inference(resolution,[],[f671,f136]) ).
tff(f954,plain,
! [X0: color,X1: color] :
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X1))),sK7,sK5,X0) = nb_occ(sF14,sK7,sK5,X0) )
| ( tb2t1(get(color1,int,sF15,sF11)) = X0 )
| ( X0 = X1 ) ),
inference(constrained_superposition,[],[f941,f187]) ).
tff(f980,plain,
! [X2: $int,X3: $int,X0: $int,X1: color,X5: map_int_color] :
( $less(X2,X0)
| ( $sum(-1,nb_occ(X5,X0,X3,tb2t1(get(color1,int,t2tb(X5),t2tb2(X2))))) = nb_occ(tb2t(set(color1,int,t2tb(X5),t2tb2(X2),t2tb1(X1))),X0,X3,tb2t1(get(color1,int,t2tb(X5),t2tb2(X2)))) )
| ( tb2t1(get(color1,int,t2tb(X5),t2tb2(X2))) = X1 )
| ~ $less(X2,X3) ),
inference(evaluation,[],[f163]) ).
tff(f981,plain,
! [X0: uni,X1: color] :
( ~ sort(color1,X0)
| ( tb2t1(get(color1,int,sF15,sF11)) = X1 )
| ( tb2t1(X0) = X1 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,X0)),sK7,sK5,X1) = nb_occ(sF14,sK7,sK5,X1) ) ),
inference(constrained_superposition,[],[f954,f158]) ).
tff(f988,plain,
! [X0: color] :
( ( tb2t1(get(color1,int,sF15,sF11)) = X0 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,sF16)),sK7,sK5,X0) = nb_occ(sF14,sK7,sK5,X0) )
| ( tb2t1(sF16) = X0 ) ),
inference(resolution,[],[f981,f194]) ).
tff(f990,plain,
! [X0: color] :
( ( tb2t1(get(color1,int,sF15,sF11)) = X0 )
| ( nb_occ(tb2t(sF17),sK7,sK5,X0) = nb_occ(sF14,sK7,sK5,X0) )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f988,f177]) ).
tff(f992,plain,
! [X0: color] :
( ( nb_occ(sF14,sK7,sK5,X0) = nb_occ(sK4,sK7,sK5,X0) )
| ( tb2t1(get(color1,int,sF15,sF11)) = X0 )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f990,f188]) ).
tff(f993,plain,
( ( sF20 = nb_occ(sF14,sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF16) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 ) ),
inference(constrained_superposition,[],[f992,f183]) ).
tff(f997,plain,
( ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sF20 = sF19 )
| ( sK6 = tb2t1(sF16) ) ),
inference(constrained_superposition,[],[f766,f993]) ).
tff(f999,plain,
( ( sK6 = tb2t1(sF16) )
| ( sF20 = sF19 )
| ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 ) ),
inference(duplicate_literal_removal,[],[f997]) ).
tff(f1002,plain,
( ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) ) ),
inference(forward_subsumption_resolution,[],[f999,f184]) ).
tff(f1005,plain,
( ( sK6 = tb2t1(sF16) )
| ( tb2t1(get(color1,int,sF9,sF11)) = sK6 )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF12) )
| ~ sort(int,sF11) ),
inference(constrained_superposition,[],[f1002,f268]) ).
tff(f1030,plain,
( ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) )
| ( tb2t1(get(color1,int,sF9,sF11)) = sK6 )
| ( sF11 = sF10 ) ),
inference(forward_subsumption_resolution,[],[f1005,f186]) ).
tff(f1041,plain,
( ( sK6 = tb2t1(sF12) )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) ) ),
inference(forward_demodulation,[],[f1030,f169]) ).
tff(f1042,plain,
( ( sF11 = sF10 )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) ) ),
inference(duplicate_literal_removal,[],[f1041]) ).
tff(f1065,plain,
( ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(get(color1,int,sF15,sF10)) )
| ( sK6 = tb2t1(sF12) ) ),
inference(constrained_superposition,[],[f1002,f1042]) ).
tff(f1067,plain,
( ( sK6 = tb2t1(get(color1,int,sF15,sF10)) )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) ) ),
inference(duplicate_literal_removal,[],[f1065]) ).
tff(f1073,plain,
( ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f1067,f222]) ).
tff(f1074,plain,
( ( sK6 = tb2t1(sF16) )
| ( sK6 = tb2t1(sF12) ) ),
inference(duplicate_literal_removal,[],[f1073]) ).
tff(f1087,plain,
( ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( nb_occ(sK4,sK7,sK5,sK6) = $sum(1,nb_occ(sF14,sK7,sK5,sK6)) ) ),
inference(constrained_superposition,[],[f714,f1074]) ).
tff(f1103,plain,
( ( sF20 = $sum(1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f1087,f183]) ).
tff(f1211,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ~ $less(sK0,X1)
| ( tb2t1(get(color1,int,t2tb(X0),t2tb2(sK0))) = X2 )
| ( $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK0))))) = nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(sK0),t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK0)))) ) ),
inference(resolution,[],[f980,f135]) ).
tff(f1212,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ( $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK1))))) = nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(sK1),t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK1)))) )
| ( tb2t1(get(color1,int,t2tb(X0),t2tb2(sK1))) = X2 )
| ~ $less(sK1,X1) ),
inference(resolution,[],[f980,f138]) ).
tff(f1220,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ( tb2t1(get(color1,int,t2tb(X0),sF10)) = X2 )
| ~ $less(sK0,X1)
| ( $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK0))))) = nb_occ(tb2t(set(color1,int,t2tb(X0),t2tb2(sK0),t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),t2tb2(sK0)))) ) ),
inference(forward_demodulation,[],[f1211,f166]) ).
tff(f1222,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ~ $less(sK1,X1)
| ( $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF11)))) = nb_occ(tb2t(set(color1,int,t2tb(X0),sF11,t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF11))) )
| ( tb2t1(get(color1,int,t2tb(X0),t2tb2(sK1))) = X2 ) ),
inference(forward_demodulation,[],[f1212,f168]) ).
tff(f1228,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ~ $less(sK0,X1)
| ( nb_occ(tb2t(set(color1,int,t2tb(X0),sF10,t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF10))) = $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF10)))) )
| ( tb2t1(get(color1,int,t2tb(X0),sF10)) = X2 ) ),
inference(forward_demodulation,[],[f1220,f166]) ).
tff(f1230,plain,
! [X2: color,X0: map_int_color,X1: $int] :
( ~ $less(sK1,X1)
| ( tb2t1(get(color1,int,t2tb(X0),sF11)) = X2 )
| ( $sum(-1,nb_occ(X0,sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF11)))) = nb_occ(tb2t(set(color1,int,t2tb(X0),sF11,t2tb1(X2))),sK7,X1,tb2t1(get(color1,int,t2tb(X0),sF11))) ) ),
inference(forward_demodulation,[],[f1222,f168]) ).
tff(f1292,plain,
! [X0: map_int_color] : ( nb_occ(tb2t(set(color1,int,t2tb(X0),sF11,t2tb1(tb2t1(get(color1,int,t2tb(X0),sF11))))),sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF11))) = nb_occ(X0,sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF11))) ),
inference(resolution,[],[f866,f136]) ).
tff(f1355,plain,
! [X0: map_int_color] : ( nb_occ(X0,sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF10))) = nb_occ(tb2t(set(color1,int,t2tb(X0),sF10,t2tb1(tb2t1(get(color1,int,t2tb(X0),sF10))))),sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF10))) ),
inference(resolution,[],[f870,f139]) ).
tff(f1397,plain,
! [X0: map_int_color,X1: color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X0),sF10,t2tb1(X1))),sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF10))) = $sum(-1,nb_occ(X0,sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF10)))) )
| ( tb2t1(get(color1,int,t2tb(X0),sF10)) = X1 ) ),
inference(resolution,[],[f1228,f139]) ).
tff(f1450,plain,
! [X0: map_int_color,X1: color] :
( ( nb_occ(tb2t(set(color1,int,t2tb(X0),sF11,t2tb1(X1))),sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF11))) = $sum(-1,nb_occ(X0,sK7,sK5,tb2t1(get(color1,int,t2tb(X0),sF11)))) )
| ( tb2t1(get(color1,int,t2tb(X0),sF11)) = X1 ) ),
inference(resolution,[],[f1230,f136]) ).
tff(f1858,plain,
nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(tb2t1(get(color1,int,sF15,sF11))))),sK7,sK5,tb2t1(get(color1,int,sF15,sF11))) = nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF15,sF11))),
inference(constrained_superposition,[],[f1292,f187]) ).
tff(f1921,plain,
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(tb2t1(get(color1,int,sF9,sF11))))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) = nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) )
| ~ sort(int,sF11)
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f1858,f268]) ).
tff(f1924,plain,
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(tb2t1(get(color1,int,sF9,sF11))))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) = nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) )
| ( sF11 = sF10 ) ),
inference(forward_subsumption_resolution,[],[f1921,f186]) ).
tff(f1925,plain,
( ( nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(tb2t1(sF12)))),sK7,sK5,tb2t1(sF12)) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f1924,f169]) ).
tff(f1926,plain,
( ( nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF11,sF12)),sK7,sK5,tb2t1(sF12)) )
| ~ sort(color1,sF12)
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f1925,f158]) ).
tff(f1930,plain,
( ( nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF11,sF12)),sK7,sK5,tb2t1(sF12)) )
| ( sF11 = sF10 ) ),
inference(forward_subsumption_resolution,[],[f1926,f193]) ).
tff(f2045,plain,
nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(tb2t1(get(color1,int,sF9,sF10))))),sK7,sK5,tb2t1(get(color1,int,sF9,sF10))) = nb_occ(sK3,sK7,sK5,tb2t1(get(color1,int,sF9,sF10))),
inference(constrained_superposition,[],[f1355,f165]) ).
tff(f2047,plain,
nb_occ(tb2t(set(color1,int,sF15,sF10,t2tb1(tb2t1(get(color1,int,sF15,sF10))))),sK7,sK5,tb2t1(get(color1,int,sF15,sF10))) = nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF15,sF10))),
inference(constrained_superposition,[],[f1355,f187]) ).
tff(f2048,plain,
nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF10,t2tb1(tb2t1(sF12)))),sK7,sK5,tb2t1(sF12)),
inference(forward_demodulation,[],[f2047,f222]) ).
tff(f2049,plain,
nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(tb2t1(sF16)))),sK7,sK5,tb2t1(sF16)) = nb_occ(sK3,sK7,sK5,tb2t1(sF16)),
inference(forward_demodulation,[],[f2045,f176]) ).
tff(f2051,plain,
( ~ sort(color1,sF12)
| ( nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF10,sF12)),sK7,sK5,tb2t1(sF12)) ) ),
inference(constrained_superposition,[],[f2048,f158]) ).
tff(f2053,plain,
nb_occ(sF14,sK7,sK5,tb2t1(sF12)) = nb_occ(tb2t(set(color1,int,sF15,sF10,sF12)),sK7,sK5,tb2t1(sF12)),
inference(forward_subsumption_resolution,[],[f2051,f193]) ).
tff(f3140,plain,
! [X0: color] :
( ( nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF9,sF10))) = $sum(-1,nb_occ(sK3,sK7,sK5,tb2t1(get(color1,int,sF9,sF10)))) )
| ( tb2t1(get(color1,int,sF9,sF10)) = X0 ) ),
inference(constrained_superposition,[],[f1397,f165]) ).
tff(f3144,plain,
! [X0: color] :
( ( tb2t1(get(color1,int,sF9,sF10)) = X0 )
| ( $sum(-1,nb_occ(sK3,sK7,sK5,tb2t1(sF16))) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,tb2t1(sF16)) ) ),
inference(forward_demodulation,[],[f3140,f176]) ).
tff(f3146,plain,
! [X0: color] :
( ( $sum(-1,nb_occ(sK3,sK7,sK5,tb2t1(sF16))) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,tb2t1(sF16)) )
| ( tb2t1(sF16) = X0 ) ),
inference(forward_demodulation,[],[f3144,f176]) ).
tff(f3152,plain,
! [X0: color] :
( ( sK6 = X0 )
| ( sK6 = tb2t1(sF12) )
| ( nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,sK6) = $sum(-1,nb_occ(sK3,sK7,sK5,sK6)) ) ),
inference(constrained_superposition,[],[f3146,f1074]) ).
tff(f3154,plain,
! [X0: color] :
( ( $sum(-1,sF19) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(X0))),sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = X0 ) ),
inference(forward_demodulation,[],[f3152,f182]) ).
tff(f3157,plain,
! [X0: uni] :
( ~ sort(color1,X0)
| ( tb2t1(X0) = sK6 )
| ( $sum(-1,sF19) = nb_occ(tb2t(set(color1,int,sF9,sF10,X0)),sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF12) ) ),
inference(constrained_superposition,[],[f3154,f158]) ).
tff(f3175,plain,
( ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF12) )
| ( $sum(-1,sF19) = nb_occ(tb2t(set(color1,int,sF9,sF10,sF12)),sK7,sK5,sK6) ) ),
inference(resolution,[],[f3157,f193]) ).
tff(f3178,plain,
( ( sK6 = tb2t1(sF12) )
| ( $sum(-1,sF19) = nb_occ(tb2t(set(color1,int,sF9,sF10,sF12)),sK7,sK5,sK6) ) ),
inference(duplicate_literal_removal,[],[f3175]) ).
tff(f3180,plain,
( ( $sum(-1,sF19) = nb_occ(tb2t(sF13),sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f3178,f171]) ).
tff(f3181,plain,
( ( $sum(-1,sF19) = nb_occ(sF14,sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f3180,f172]) ).
tff(f3195,plain,
( ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sF20 = $sum(1,$sum(-1,sF19)) ) ),
inference(constrained_superposition,[],[f1103,f3181]) ).
tff(f3200,plain,
( ( sF20 = $sum(1,$sum(-1,sF19)) )
| ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF15,sF11)) = sK6 ) ),
inference(duplicate_literal_removal,[],[f3195]) ).
tff(f3238,plain,
! [X0: color] :
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF15,sF11))) = $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF15,sF11)))) )
| ( tb2t1(get(color1,int,sF15,sF11)) = X0 ) ),
inference(constrained_superposition,[],[f1450,f187]) ).
tff(f3262,plain,
( ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sF20 = sF19 )
| ( sK6 = tb2t1(sF12) ) ),
inference(evaluation,[],[f3200]) ).
tff(f3263,plain,
( ( tb2t1(get(color1,int,sF15,sF11)) = sK6 )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_subsumption_resolution,[],[f3262,f184]) ).
tff(f3275,plain,
( ~ sort(int,sF11)
| ( tb2t1(get(color1,int,sF9,sF11)) = sK6 )
| ( sK6 = tb2t1(sF12) )
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f3263,f268]) ).
tff(f3299,plain,
( ( sF11 = sF10 )
| ( sK6 = tb2t1(sF12) )
| ( tb2t1(get(color1,int,sF9,sF11)) = sK6 ) ),
inference(forward_subsumption_resolution,[],[f3275,f186]) ).
tff(f3308,plain,
( ( sF11 = sF10 )
| ( sK6 = tb2t1(sF12) )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f3299,f169]) ).
tff(f3309,plain,
( ( sK6 = tb2t1(sF12) )
| ( sF11 = sF10 ) ),
inference(duplicate_literal_removal,[],[f3308]) ).
tff(f3338,plain,
( ( sF11 = sF10 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,sF12)),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6) )
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f1930,f3309]) ).
tff(f3352,plain,
( ( sF12 = t2tb1(sK6) )
| ( sF11 = sF10 )
| ~ sort(color1,sF12) ),
inference(constrained_superposition,[],[f158,f3309]) ).
tff(f3368,plain,
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,sF12)),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6) )
| ( sF11 = sF10 ) ),
inference(duplicate_literal_removal,[],[f3338]) ).
tff(f3388,plain,
( ( sF11 = sF10 )
| ( sF12 = t2tb1(sK6) ) ),
inference(forward_subsumption_resolution,[],[f3352,f193]) ).
tff(f3465,plain,
( ( sK6 = tb2t1(get(color1,int,sF15,sF10)) )
| ( sK6 = tb2t1(sF12) )
| ( sF12 = t2tb1(sK6) ) ),
inference(constrained_superposition,[],[f3263,f3388]) ).
tff(f3468,plain,
( ( sK6 = tb2t1(sF12) )
| ( sF12 = t2tb1(sK6) )
| ( sK6 = tb2t1(sF12) ) ),
inference(forward_demodulation,[],[f3465,f222]) ).
tff(f3469,plain,
( ( sK6 = tb2t1(sF12) )
| ( sF12 = t2tb1(sK6) ) ),
inference(duplicate_literal_removal,[],[f3468]) ).
tff(f3701,plain,
( ( sF12 = t2tb1(sK6) )
| ( sF12 = t2tb1(sK6) )
| ~ sort(color1,sF12) ),
inference(constrained_superposition,[],[f158,f3469]) ).
tff(f3712,plain,
( ( sF12 = t2tb1(sK6) )
| ~ sort(color1,sF12) ),
inference(duplicate_literal_removal,[],[f3701]) ).
tff(f3719,plain,
sF12 = t2tb1(sK6),
inference(forward_subsumption_resolution,[],[f3712,f193]) ).
tff(f3741,plain,
sK6 = tb2t1(sF12),
inference(constrained_superposition,[],[f155,f3719]) ).
tff(f3768,plain,
( ( $sum(1,nb_occ(sK3,sK7,sK5,sK6)) = nb_occ(tb2t(set(color1,int,sF9,sF10,sF12)),sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF16) ) ),
inference(constrained_superposition,[],[f650,f3719]) ).
tff(f3821,plain,
( ( sK6 = tb2t1(sF16) )
| ( $sum(1,nb_occ(sK3,sK7,sK5,sK6)) = nb_occ(tb2t(sF13),sK7,sK5,sK6) ) ),
inference(forward_demodulation,[],[f3768,f171]) ).
tff(f3830,plain,
( ( sK6 = tb2t1(sF16) )
| ( $sum(1,nb_occ(sK3,sK7,sK5,sK6)) = nb_occ(sF14,sK7,sK5,sK6) ) ),
inference(forward_demodulation,[],[f3821,f172]) ).
tff(f3834,plain,
( ( $sum(1,sF19) = nb_occ(sF14,sK7,sK5,sK6) )
| ( sK6 = tb2t1(sF16) ) ),
inference(forward_demodulation,[],[f3830,f182]) ).
tff(f3863,plain,
nb_occ(tb2t(set(color1,int,sF15,sF10,sF12)),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6),
inference(constrained_superposition,[],[f2053,f3741]) ).
tff(f5363,plain,
! [X0: color] :
( ( tb2t1(get(color1,int,sF9,sF11)) = X0 )
| ~ sort(int,sF11)
| ( $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11)))) = nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) )
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f3238,f268]) ).
tff(f5366,plain,
! [X0: color] :
( ( tb2t1(get(color1,int,sF9,sF11)) = X0 )
| ( sF11 = sF10 )
| ( $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11)))) = nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) ) ),
inference(forward_subsumption_resolution,[],[f5363,f186]) ).
tff(f5368,plain,
! [X0: color] :
( ( tb2t1(sF12) = X0 )
| ( $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11)))) = nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f5366,f169]) ).
tff(f5369,plain,
! [X0: color] :
( ( sK6 = X0 )
| ( $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(get(color1,int,sF9,sF11)))) = nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(get(color1,int,sF9,sF11))) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f5368,f3741]) ).
tff(f5370,plain,
! [X0: color] :
( ( sF11 = sF10 )
| ( sK6 = X0 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,tb2t1(sF12)) = $sum(-1,nb_occ(sF14,sK7,sK5,tb2t1(sF12))) ) ),
inference(forward_demodulation,[],[f5369,f169]) ).
tff(f5371,plain,
! [X0: color] :
( ( nb_occ(tb2t(set(color1,int,sF15,sF11,t2tb1(X0))),sK7,sK5,sK6) = $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( sF11 = sF10 )
| ( sK6 = X0 ) ),
inference(forward_demodulation,[],[f5370,f3741]) ).
tff(f5372,plain,
! [X0: uni] :
( ~ sort(color1,X0)
| ( sF11 = sF10 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,X0)),sK7,sK5,sK6) = $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( tb2t1(X0) = sK6 ) ),
inference(constrained_superposition,[],[f5371,f158]) ).
tff(f5652,plain,
( ( $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) = nb_occ(tb2t(set(color1,int,sF15,sF11,sF16)),sK7,sK5,sK6) )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF16) ) ),
inference(resolution,[],[f5372,f194]) ).
tff(f5654,plain,
( ( nb_occ(tb2t(sF17),sK7,sK5,sK6) = $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( sK6 = tb2t1(sF16) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f5652,f177]) ).
tff(f5656,plain,
( ( nb_occ(sK4,sK7,sK5,sK6) = $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( sK6 = tb2t1(sF16) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f5654,f188]) ).
tff(f5657,plain,
( ( sF20 = $sum(-1,nb_occ(sF14,sK7,sK5,sK6)) )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF16) ) ),
inference(forward_demodulation,[],[f5656,f183]) ).
tff(f5667,plain,
( ( sK6 = tb2t1(sF16) )
| ( sF11 = sF10 )
| ( sF20 = $sum(-1,$sum(1,sF19)) )
| ( sK6 = tb2t1(sF16) ) ),
inference(constrained_superposition,[],[f5657,f3834]) ).
tff(f5676,plain,
( ( sF20 = $sum(-1,$sum(1,sF19)) )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF16) ) ),
inference(duplicate_literal_removal,[],[f5667]) ).
tff(f5681,plain,
( ( sF20 = sF19 )
| ( sF11 = sF10 )
| ( sK6 = tb2t1(sF16) ) ),
inference(evaluation,[],[f5676]) ).
tff(f5682,plain,
( ( sK6 = tb2t1(sF16) )
| ( sF11 = sF10 ) ),
inference(forward_subsumption_resolution,[],[f5681,f184]) ).
tff(f5719,plain,
( ( t2tb1(sK6) = sF16 )
| ( sF11 = sF10 )
| ~ sort(color1,sF16) ),
inference(constrained_superposition,[],[f158,f5682]) ).
tff(f5737,plain,
( ( t2tb1(sK6) = sF16 )
| ( sF11 = sF10 ) ),
inference(forward_subsumption_resolution,[],[f5719,f194]) ).
tff(f5792,plain,
( ( sF11 = sF10 )
| ( sF12 = sF16 ) ),
inference(constrained_superposition,[],[f5737,f3719]) ).
tff(f5918,plain,
( ( sF12 = get(color1,int,sF9,sF10) )
| ( sF12 = sF16 ) ),
inference(constrained_superposition,[],[f169,f5792]) ).
tff(f6027,plain,
( ( sF12 = sF16 )
| ( sF12 = sF16 ) ),
inference(forward_demodulation,[],[f5918,f176]) ).
tff(f6028,plain,
sF12 = sF16,
inference(duplicate_literal_removal,[],[f6027]) ).
tff(f6171,plain,
( ( sF11 = sF10 )
| ( nb_occ(tb2t(set(color1,int,sF15,sF11,sF16)),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6) ) ),
inference(constrained_superposition,[],[f3368,f6028]) ).
tff(f6174,plain,
sK6 = tb2t1(sF16),
inference(constrained_superposition,[],[f3741,f6028]) ).
tff(f6210,plain,
nb_occ(tb2t(set(color1,int,sF15,sF10,sF16)),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6),
inference(constrained_superposition,[],[f3863,f6028]) ).
tff(f6235,plain,
( ( nb_occ(tb2t(sF17),sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f6171,f177]) ).
tff(f6270,plain,
( ( sF11 = sF10 )
| ( nb_occ(sK4,sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6) ) ),
inference(forward_demodulation,[],[f6235,f188]) ).
tff(f6278,plain,
( ( sF20 = nb_occ(sF14,sK7,sK5,sK6) )
| ( sF11 = sF10 ) ),
inference(forward_demodulation,[],[f6270,f183]) ).
tff(f6300,plain,
nb_occ(sK3,sK7,sK5,sK6) = nb_occ(tb2t(set(color1,int,sF9,sF10,t2tb1(sK6))),sK7,sK5,sK6),
inference(constrained_superposition,[],[f2049,f6174]) ).
tff(f6340,plain,
nb_occ(sK3,sK7,sK5,sK6) = nb_occ(tb2t(set(color1,int,sF9,sF10,sF12)),sK7,sK5,sK6),
inference(forward_demodulation,[],[f6300,f3719]) ).
tff(f6353,plain,
nb_occ(sK3,sK7,sK5,sK6) = nb_occ(tb2t(sF13),sK7,sK5,sK6),
inference(forward_demodulation,[],[f6340,f171]) ).
tff(f6356,plain,
nb_occ(sK3,sK7,sK5,sK6) = nb_occ(sF14,sK7,sK5,sK6),
inference(forward_demodulation,[],[f6353,f172]) ).
tff(f6358,plain,
nb_occ(sF14,sK7,sK5,sK6) = sF19,
inference(forward_demodulation,[],[f6356,f182]) ).
tff(f6648,plain,
( ( sF20 = sF19 )
| ( sF11 = sF10 ) ),
inference(constrained_superposition,[],[f6278,f6358]) ).
tff(f6669,plain,
sF11 = sF10,
inference(forward_subsumption_resolution,[],[f6648,f184]) ).
tff(f6674,plain,
sF17 = set(color1,int,sF15,sF10,sF16),
inference(constrained_superposition,[],[f177,f6669]) ).
tff(f6999,plain,
nb_occ(tb2t(set(color1,int,sF15,sF10,sF16)),sK7,sK5,sK6) = sF19,
inference(forward_demodulation,[],[f6210,f6358]) ).
tff(f7000,plain,
nb_occ(tb2t(sF17),sK7,sK5,sK6) = sF19,
inference(forward_demodulation,[],[f6999,f6674]) ).
tff(f7001,plain,
nb_occ(sK4,sK7,sK5,sK6) = sF19,
inference(forward_demodulation,[],[f7000,f188]) ).
tff(f7002,plain,
sF20 = sF19,
inference(forward_demodulation,[],[f7001,f183]) ).
tff(f7003,plain,
$false,
inference(forward_subsumption_resolution,[],[f7002,f184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW596_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:22:57 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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.32/1.23 % (1620114)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.32/1.23 % (1620120)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3876393170:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.32/1.23 % (1620119)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4161292392:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.32/1.23 % (1620121)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2852652510:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.32/1.23 % (1620122)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2753489356:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.32/1.23 % (1620122)Instruction limit reached!
% 3.32/1.23 % (1620122)------------------------------
% 3.32/1.23 % (1620122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/1.23 % (1620122)CaDiCaL version: 2.1.3
% 3.32/1.23 % (1620122)Termination reason: Instruction limit
% 3.32/1.23 % (1620122)Termination phase: Saturation
% 3.32/1.23 % (1620122)Time elapsed: 0.005 s
% 3.32/1.23 % (1620122)Peak memory usage: 88 MB
% 3.32/1.23 % (1620122)Instructions burned: 8 (million)
% 3.32/1.23 % (1620124)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3604299394:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.32/1.23 % (1620125)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2449816160:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.32/1.23 % (1620123)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=804003330:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.32/1.23 % (1620123)Instruction limit reached!
% 3.32/1.23 % (1620123)------------------------------
% 3.32/1.23 % (1620123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/1.23 % (1620123)CaDiCaL version: 2.1.3
% 3.32/1.23 % (1620123)Termination reason: Instruction limit
% 3.32/1.23 % (1620123)Termination phase: Saturation
% 3.32/1.23 % (1620123)Time elapsed: 0.003 s
% 3.32/1.23 % (1620123)Peak memory usage: 87 MB
% 3.32/1.23 % (1620123)Instructions burned: 4 (million)
% 3.32/1.23 % (1620119)Instruction limit reached!
% 3.32/1.23 % (1620119)------------------------------
% 3.32/1.23 % (1620119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/1.23 % (1620119)CaDiCaL version: 2.1.3
% 3.32/1.23 % (1620119)Termination reason: Instruction limit
% 3.32/1.23 % (1620119)Termination phase: Saturation
% 3.32/1.23 % (1620119)Time elapsed: 0.030 s
% 3.32/1.23 % (1620119)Peak memory usage: 115 MB
% 3.32/1.23 % (1620119)Instructions burned: 12 (million)
% 3.32/1.23 % (1620125)Instruction limit reached!
% 3.32/1.23 % (1620125)------------------------------
% 3.32/1.23 % (1620125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/1.23 % (1620125)CaDiCaL version: 2.1.3
% 3.32/1.23 % (1620125)Termination reason: Instruction limit
% 3.32/1.23 % (1620125)Termination phase: Saturation
% 3.32/1.23 % (1620125)Time elapsed: 0.044 s
% 3.32/1.23 % (1620125)Peak memory usage: 116 MB
% 3.32/1.23 % (1620125)Instructions burned: 33 (million)
% 3.32/1.23 % (1620124)Instruction limit reached!
% 3.32/1.23 % (1620124)------------------------------
% 3.32/1.23 % (1620124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.32/1.23 % (1620124)CaDiCaL version: 2.1.3
% 3.32/1.23 % (1620124)Termination reason: Instruction limit
% 3.32/1.23 % (1620124)Termination phase: Saturation
% 3.32/1.23 % (1620124)Time elapsed: 0.055 s
% 3.32/1.23 % (1620124)Peak memory usage: 116 MB
% 3.32/1.23 % (1620124)Instructions burned: 47 (million)
% 3.32/1.23 % (1620120)Instruction limit reached!
% 3.32/1.23 % (1620120)------------------------------
% 3.32/1.23 % (1620120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.32/1.23 % (1620120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620120)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620120)Termination reason: Instruction limit
% 4.42/1.37 % (1620120)Termination phase: Saturation
% 4.42/1.37 % (1620120)Time elapsed: 0.116 s
% 4.42/1.37 % (1620120)Peak memory usage: 117 MB
% 4.42/1.37 % (1620120)Instructions burned: 309 (million)
% 4.42/1.37 % (1620121)Instruction limit reached!
% 4.42/1.37 % (1620121)------------------------------
% 4.42/1.37 % (1620121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.37 % (1620121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620121)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620121)Termination reason: Instruction limit
% 4.42/1.37 % (1620121)Termination phase: Saturation
% 4.42/1.37 % (1620121)Time elapsed: 0.133 s
% 4.42/1.37 % (1620121)Peak memory usage: 116 MB
% 4.42/1.37 % (1620121)Instructions burned: 202 (million)
% 4.42/1.37 % (1620130)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1789544753:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.42/1.37 % (1620134)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=3831134218:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.42/1.37 % (1620130)Instruction limit reached!
% 4.42/1.37 % (1620130)------------------------------
% 4.42/1.37 % (1620130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.37 % (1620130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620130)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620130)Termination reason: Instruction limit
% 4.42/1.37 % (1620130)Termination phase: Saturation
% 4.42/1.37 % (1620130)Time elapsed: 0.010 s
% 4.42/1.37 % (1620130)Peak memory usage: 88 MB
% 4.42/1.37 % (1620130)Instructions burned: 14 (million)
% 4.42/1.37 % (1620135)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2144670091:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.42/1.37 % (1620134)Instruction limit reached!
% 4.42/1.37 % (1620134)------------------------------
% 4.42/1.37 % (1620134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.37 % (1620134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620134)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620134)Termination reason: Instruction limit
% 4.42/1.37 % (1620134)Termination phase: Saturation
% 4.42/1.37 % (1620134)Time elapsed: 0.023 s
% 4.42/1.37 % (1620134)Peak memory usage: 89 MB
% 4.42/1.37 % (1620134)Instructions burned: 30 (million)
% 4.42/1.37 % (1620135)Instruction limit reached!
% 4.42/1.37 % (1620135)------------------------------
% 4.42/1.37 % (1620135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.37 % (1620135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620135)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620135)Termination reason: Instruction limit
% 4.42/1.37 % (1620135)Termination phase: Saturation
% 4.42/1.37 % (1620135)Time elapsed: 0.011 s
% 4.42/1.37 % (1620135)Peak memory usage: 90 MB
% 4.42/1.37 % (1620135)Instructions burned: 17 (million)
% 4.42/1.37 % (1620138)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1442676006:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.42/1.37 % (1620136)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1497036408:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.42/1.37 % (1620137)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=2822909104:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.42/1.37 % (1620136)Instruction limit reached!
% 4.42/1.37 % (1620136)------------------------------
% 4.42/1.37 % (1620136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.37 % (1620136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.37 % (1620136)CaDiCaL version: 2.1.3
% 4.42/1.37 % (1620136)Termination reason: Instruction limit
% 4.42/1.37 % (1620136)Termination phase: Saturation
% 4.42/1.37 % (1620136)Time elapsed: 0.018 s
% 4.42/1.37 % (1620136)Peak memory usage: 89 MB
% 4.42/1.37 % (1620136)Instructions burned: 24 (million)
% 4.42/1.37 % (1620138)Instruction limit reached!
% 4.42/1.37 % (1620138)------------------------------
% 4.42/1.37 % (1620138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620138)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620138)Termination reason: Instruction limit
% 5.56/1.54 % (1620138)Termination phase: Saturation
% 5.56/1.54 % (1620138)Time elapsed: 0.025 s
% 5.56/1.54 % (1620138)Peak memory usage: 89 MB
% 5.56/1.54 % (1620138)Instructions burned: 86 (million)
% 5.56/1.54 % (1620137)Instruction limit reached!
% 5.56/1.54 % (1620137)------------------------------
% 5.56/1.54 % (1620137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620137)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620137)Termination reason: Instruction limit
% 5.56/1.54 % (1620137)Termination phase: Saturation
% 5.56/1.54 % (1620137)Time elapsed: 0.019 s
% 5.56/1.54 % (1620137)Peak memory usage: 89 MB
% 5.56/1.54 % (1620137)Instructions burned: 28 (million)
% 5.56/1.54 % (1620139)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3850975974:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.56/1.54 % (1620139)Instruction limit reached!
% 5.56/1.54 % (1620139)------------------------------
% 5.56/1.54 % (1620139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620139)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620139)Termination reason: Instruction limit
% 5.56/1.54 % (1620139)Termination phase: Preprocessing 3
% 5.56/1.54 % (1620139)Time elapsed: 0.002 s
% 5.56/1.54 % (1620139)Peak memory usage: 86 MB
% 5.56/1.54 % (1620139)Instructions burned: 2 (million)
% 5.56/1.54 % (1620144)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3945717773:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.56/1.54 % (1620142)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1178021817:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.56/1.54 % (1620144)Instruction limit reached!
% 5.56/1.54 % (1620144)------------------------------
% 5.56/1.54 % (1620144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620144)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620144)Termination reason: Instruction limit
% 5.56/1.54 % (1620144)Termination phase: Property scanning
% 5.56/1.54 % (1620144)Time elapsed: 0.003 s
% 5.56/1.54 % (1620144)Peak memory usage: 87 MB
% 5.56/1.54 % (1620144)Instructions burned: 5 (million)
% 5.56/1.54 % (1620147)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2009011653:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.56/1.54 % (1620149)lrs+10_1_thi=all:si=on:fd=off:random_seed=3580851269:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.56/1.54 % (1620150)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=2344151754:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.56/1.54 % (1620149)Instruction limit reached!
% 5.56/1.54 % (1620149)------------------------------
% 5.56/1.54 % (1620149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620149)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620149)Termination reason: Instruction limit
% 5.56/1.54 % (1620149)Termination phase: Saturation
% 5.56/1.54 % (1620149)Time elapsed: 0.036 s
% 5.56/1.54 % (1620149)Peak memory usage: 116 MB
% 5.56/1.54 % (1620149)Instructions burned: 54 (million)
% 5.56/1.54 % (1620150)Instruction limit reached!
% 5.56/1.54 % (1620150)------------------------------
% 5.56/1.54 % (1620150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.56/1.54 % (1620150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.56/1.54 % (1620150)CaDiCaL version: 2.1.3
% 5.56/1.54 % (1620150)Termination reason: Instruction limit
% 5.56/1.54 % (1620150)Termination phase: Saturation
% 5.56/1.54 % (1620150)Time elapsed: 0.005 s
% 5.56/1.54 % (1620150)Peak memory usage: 88 MB
% 5.56/1.54 % (1620150)Instructions burned: 8 (million)
% 5.56/1.54 % (1620151)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3401785603:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 6.96/1.74 % (1620151)Instruction limit reached!
% 6.96/1.74 % (1620151)------------------------------
% 6.96/1.74 % (1620151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620151)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620151)Termination reason: Instruction limit
% 6.96/1.74 % (1620151)Termination phase: Saturation
% 6.96/1.74 % (1620151)Time elapsed: 0.002 s
% 6.96/1.74 % (1620151)Peak memory usage: 87 MB
% 6.96/1.74 % (1620151)Instructions burned: 3 (million)
% 6.96/1.74 % (1620147)Instruction limit reached!
% 6.96/1.74 % (1620147)------------------------------
% 6.96/1.74 % (1620147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620147)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620147)Termination reason: Instruction limit
% 6.96/1.74 % (1620147)Termination phase: Saturation
% 6.96/1.74 % (1620147)Time elapsed: 0.090 s
% 6.96/1.74 % (1620147)Peak memory usage: 134 MB
% 6.96/1.74 % (1620147)Instructions burned: 66 (million)
% 6.96/1.74 % (1620142)Instruction limit reached!
% 6.96/1.74 % (1620142)------------------------------
% 6.96/1.74 % (1620142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620142)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620142)Termination reason: Instruction limit
% 6.96/1.74 % (1620142)Termination phase: Saturation
% 6.96/1.74 % (1620142)Time elapsed: 0.105 s
% 6.96/1.74 % (1620142)Peak memory usage: 90 MB
% 6.96/1.74 % (1620142)Instructions burned: 182 (million)
% 6.96/1.74 % (1620153)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2163087739:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.96/1.74 % (1620153)Instruction limit reached!
% 6.96/1.74 % (1620153)------------------------------
% 6.96/1.74 % (1620153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620153)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620153)Termination reason: Instruction limit
% 6.96/1.74 % (1620153)Termination phase: Preprocessing 3
% 6.96/1.74 % (1620153)Time elapsed: 0.002 s
% 6.96/1.74 % (1620153)Peak memory usage: 86 MB
% 6.96/1.74 % (1620153)Instructions burned: 2 (million)
% 6.96/1.74 % (1620157)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2006310256:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.96/1.74 % (1620161)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2451868912:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.96/1.74 % (1620161)Instruction limit reached!
% 6.96/1.74 % (1620161)------------------------------
% 6.96/1.74 % (1620161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620161)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620161)Termination reason: Instruction limit
% 6.96/1.74 % (1620161)Termination phase: Saturation
% 6.96/1.74 % (1620161)Time elapsed: 0.010 s
% 6.96/1.74 % (1620161)Peak memory usage: 89 MB
% 6.96/1.74 % (1620161)Instructions burned: 30 (million)
% 6.96/1.74 % (1620160)dis+10_1_si=on:random_seed=2482748937:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.96/1.74 % (1620160)Instruction limit reached!
% 6.96/1.74 % (1620160)------------------------------
% 6.96/1.74 % (1620160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.74 % (1620160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.74 % (1620160)CaDiCaL version: 2.1.3
% 6.96/1.74 % (1620160)Termination reason: Instruction limit
% 6.96/1.74 % (1620160)Termination phase: Saturation
% 6.96/1.74 % (1620160)Time elapsed: 0.007 s
% 6.96/1.74 % (1620160)Peak memory usage: 88 MB
% 6.96/1.74 % (1620160)Instructions burned: 10 (million)
% 6.96/1.74 % (1620163)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2372045652: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)
% 7.82/1.99 % (1620163)Instruction limit reached!
% 7.82/1.99 % (1620163)------------------------------
% 7.82/1.99 % (1620163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620163)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620163)Termination reason: Instruction limit
% 7.82/1.99 % (1620163)Termination phase: Saturation
% 7.82/1.99 % (1620163)Time elapsed: 0.028 s
% 7.82/1.99 % (1620163)Peak memory usage: 89 MB
% 7.82/1.99 % (1620163)Instructions burned: 36 (million)
% 7.82/1.99 % (1620164)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2309904601:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.82/1.99 % (1620165)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2340817546:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 7.82/1.99 % (1620164)Instruction limit reached!
% 7.82/1.99 % (1620164)------------------------------
% 7.82/1.99 % (1620164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620164)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620164)Termination reason: Instruction limit
% 7.82/1.99 % (1620164)Termination phase: Preprocessing 3
% 7.82/1.99 % (1620164)Time elapsed: 0.002 s
% 7.82/1.99 % (1620164)Peak memory usage: 86 MB
% 7.82/1.99 % (1620164)Instructions burned: 2 (million)
% 7.82/1.99 % (1620165)Instruction limit reached!
% 7.82/1.99 % (1620165)------------------------------
% 7.82/1.99 % (1620165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620165)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620165)Termination reason: Instruction limit
% 7.82/1.99 % (1620165)Termination phase: Saturation
% 7.82/1.99 % (1620165)Time elapsed: 0.006 s
% 7.82/1.99 % (1620165)Peak memory usage: 88 MB
% 7.82/1.99 % (1620165)Instructions burned: 8 (million)
% 7.82/1.99 % (1620157)Instruction limit reached!
% 7.82/1.99 % (1620157)------------------------------
% 7.82/1.99 % (1620157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620157)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620157)Termination reason: Instruction limit
% 7.82/1.99 % (1620157)Termination phase: Saturation
% 7.82/1.99 % (1620157)Time elapsed: 0.118 s
% 7.82/1.99 % (1620157)Peak memory usage: 117 MB
% 7.82/1.99 % (1620157)Instructions burned: 128 (million)
% 7.82/1.99 % (1620167)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=134681259:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.82/1.99 % (1620170)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1101075361:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 7.82/1.99 % (1620170)Instruction limit reached!
% 7.82/1.99 % (1620170)------------------------------
% 7.82/1.99 % (1620170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620170)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620170)Termination reason: Instruction limit
% 7.82/1.99 % (1620170)Termination phase: Saturation
% 7.82/1.99 % (1620170)Time elapsed: 0.018 s
% 7.82/1.99 % (1620170)Peak memory usage: 112 MB
% 7.82/1.99 % (1620170)Instructions burned: 15 (million)
% 7.82/1.99 % (1620172)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=356527448:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 7.82/1.99 % (1620174)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3953535291:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 7.82/1.99 % (1620174)Instruction limit reached!
% 7.82/1.99 % (1620174)------------------------------
% 7.82/1.99 % (1620174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.82/1.99 % (1620174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.82/1.99 % (1620174)CaDiCaL version: 2.1.3
% 7.82/1.99 % (1620174)Termination reason: Instruction limit
% 7.82/1.99 % (1620174)Termination phase: Saturation
% 7.82/1.99 % (1620174)Time elapsed: 0.008 s
% 7.82/1.99 % (1620174)Peak memory usage: 88 MB
% 10.80/2.21 % (1620174)Instructions burned: 11 (million)
% 10.80/2.21 % (1620177)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1284747257:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.80/2.21 % (1620178)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=2271015611:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.80/2.21 % (1620180)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=2809843238:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.80/2.21 % (1620182)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1838353729:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi)
% 10.80/2.21 % (1620178)Instruction limit reached!
% 10.80/2.21 % (1620178)------------------------------
% 10.80/2.21 % (1620178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.21 % (1620178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.21 % (1620178)CaDiCaL version: 2.1.3
% 10.80/2.21 % (1620178)Termination reason: Instruction limit
% 10.80/2.21 % (1620178)Termination phase: Saturation
% 10.80/2.21 % (1620178)Time elapsed: 0.049 s
% 10.80/2.21 % (1620178)Peak memory usage: 90 MB
% 10.80/2.21 % (1620178)Instructions burned: 76 (million)
% 10.80/2.21 % (1620167)Instruction limit reached!
% 10.80/2.21 % (1620167)------------------------------
% 10.80/2.21 % (1620167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.21 % (1620167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.21 % (1620167)CaDiCaL version: 2.1.3
% 10.80/2.21 % (1620167)Termination reason: Instruction limit
% 10.80/2.21 % (1620167)Termination phase: Saturation
% 10.80/2.21 % (1620167)Time elapsed: 0.195 s
% 10.80/2.21 % (1620167)Peak memory usage: 91 MB
% 10.80/2.21 % (1620167)Instructions burned: 370 (million)
% 10.80/2.21 % (1620182)Instruction limit reached!
% 10.80/2.21 % (1620182)------------------------------
% 10.80/2.21 % (1620182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.21 % (1620182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.21 % (1620182)CaDiCaL version: 2.1.3
% 10.80/2.21 % (1620182)Termination reason: Instruction limit
% 10.80/2.21 % (1620182)Termination phase: Saturation
% 10.80/2.21 % (1620182)Time elapsed: 0.058 s
% 10.80/2.21 % (1620182)Peak memory usage: 117 MB
% 10.80/2.21 % (1620182)Instructions burned: 130 (million)
% 10.80/2.21 % (1620177)Instruction limit reached!
% 10.80/2.21 % (1620177)------------------------------
% 10.80/2.21 % (1620177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.21 % (1620177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.21 % (1620177)CaDiCaL version: 2.1.3
% 10.80/2.21 % (1620177)Termination reason: Instruction limit
% 10.80/2.21 % (1620177)Termination phase: Saturation
% 10.80/2.21 % (1620177)Time elapsed: 0.091 s
% 10.80/2.21 % (1620177)Peak memory usage: 133 MB
% 10.80/2.21 % (1620177)Instructions burned: 71 (million)
% 10.80/2.21 % (1620172)Instruction limit reached!
% 10.80/2.21 % (1620172)------------------------------
% 10.80/2.21 % (1620172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.80/2.21 % (1620172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.80/2.21 % (1620172)CaDiCaL version: 2.1.3
% 10.80/2.21 % (1620172)Termination reason: Instruction limit
% 10.80/2.21 % (1620172)Termination phase: Saturation
% 10.80/2.21 % (1620172)Time elapsed: 0.157 s
% 10.80/2.21 % (1620172)Peak memory usage: 117 MB
% 10.80/2.21 % (1620172)Instructions burned: 228 (million)
% 10.80/2.21 % (1620187)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=757328275:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 10.80/2.21 % (1620192)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1224611182:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 10.80/2.21 % (1620191)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2905237482:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.80/2.21 % (1620190)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3852461249:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 12.41/2.52 % (1620180)Instruction limit reached!
% 12.41/2.52 % (1620180)------------------------------
% 12.41/2.52 % (1620180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620180)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620180)Termination reason: Instruction limit
% 12.41/2.52 % (1620180)Termination phase: Saturation
% 12.41/2.52 % (1620180)Time elapsed: 0.187 s
% 12.41/2.52 % (1620180)Peak memory usage: 90 MB
% 12.41/2.52 % (1620180)Instructions burned: 294 (million)
% 12.41/2.52 % (1620193)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3510701282:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 12.41/2.52 % (1620194)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2229338762:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi)
% 12.41/2.52 % (1620190)Instruction limit reached!
% 12.41/2.52 % (1620190)------------------------------
% 12.41/2.52 % (1620190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620190)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620190)Termination reason: Instruction limit
% 12.41/2.52 % (1620190)Termination phase: Saturation
% 12.41/2.52 % (1620190)Time elapsed: 0.070 s
% 12.41/2.52 % (1620190)Peak memory usage: 134 MB
% 12.41/2.52 % (1620190)Instructions burned: 40 (million)
% 12.41/2.52 % (1620187)Instruction limit reached!
% 12.41/2.52 % (1620187)------------------------------
% 12.41/2.52 % (1620187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620187)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620187)Termination reason: Instruction limit
% 12.41/2.52 % (1620187)Termination phase: Saturation
% 12.41/2.52 % (1620187)Time elapsed: 0.129 s
% 12.41/2.52 % (1620187)Peak memory usage: 134 MB
% 12.41/2.52 % (1620187)Instructions burned: 132 (million)
% 12.41/2.52 % (1620199)dis+10_1_si=on:random_seed=2494909214:s2a=on:i=1000:rtra=on:gtg=exists_all_2989 on theBenchmark for (2989ds/1000Mi)
% 12.41/2.52 % (1620193)Instruction limit reached!
% 12.41/2.52 % (1620193)------------------------------
% 12.41/2.52 % (1620193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620193)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620193)Termination reason: Instruction limit
% 12.41/2.52 % (1620193)Termination phase: Saturation
% 12.41/2.52 % (1620193)Time elapsed: 0.105 s
% 12.41/2.52 % (1620193)Peak memory usage: 118 MB
% 12.41/2.52 % (1620193)Instructions burned: 131 (million)
% 12.41/2.52 % (1620191)Instruction limit reached!
% 12.41/2.52 % (1620191)------------------------------
% 12.41/2.52 % (1620191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620191)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620191)Termination reason: Instruction limit
% 12.41/2.52 % (1620191)Termination phase: Saturation
% 12.41/2.52 % (1620191)Time elapsed: 0.181 s
% 12.41/2.52 % (1620191)Peak memory usage: 91 MB
% 12.41/2.52 % (1620191)Instructions burned: 307 (million)
% 12.41/2.52 % (1620192)Instruction limit reached!
% 12.41/2.52 % (1620192)------------------------------
% 12.41/2.52 % (1620192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.41/2.52 % (1620192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.41/2.52 % (1620192)CaDiCaL version: 2.1.3
% 12.41/2.52 % (1620192)Termination reason: Instruction limit
% 12.41/2.52 % (1620192)Termination phase: Saturation
% 12.41/2.52 % (1620192)Time elapsed: 0.237 s
% 12.41/2.52 % (1620192)Peak memory usage: 136 MB
% 12.41/2.52 % (1620192)Instructions burned: 601 (million)
% 12.41/2.52 % (1620203)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4237610179:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 12.41/2.52 % (1620202)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3142118821:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.41/2.52 % (1620194)Instruction limit reached!
% 14.40/2.90 % (1620194)------------------------------
% 14.40/2.90 % (1620194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620194)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620194)Termination reason: Instruction limit
% 14.40/2.90 % (1620194)Termination phase: Saturation
% 14.40/2.90 % (1620194)Time elapsed: 0.182 s
% 14.40/2.90 % (1620194)Peak memory usage: 117 MB
% 14.40/2.90 % (1620194)Instructions burned: 259 (million)
% 14.40/2.90 % (1620206)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1708482543:i=121:nm=16:rtra=on_2987 on theBenchmark for (2987ds/121Mi)
% 14.40/2.90 % (1620205)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=607589596:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 14.40/2.90 % (1620203)Instruction limit reached!
% 14.40/2.90 % (1620203)------------------------------
% 14.40/2.90 % (1620203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620203)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620203)Termination reason: Instruction limit
% 14.40/2.90 % (1620203)Termination phase: Saturation
% 14.40/2.90 % (1620203)Time elapsed: 0.095 s
% 14.40/2.90 % (1620203)Peak memory usage: 90 MB
% 14.40/2.90 % (1620203)Instructions burned: 142 (million)
% 14.40/2.90 % (1620209)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=3397679978:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 14.40/2.90 % (1620205)Refutation not found, incomplete strategy
% 14.40/2.90 % (1620205)------------------------------
% 14.40/2.90 % (1620205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620205)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620205)Termination reason: Refutation not found, incomplete strategy
% 14.40/2.90 % (1620205)Time elapsed: 0.035 s
% 14.40/2.90 % (1620205)Peak memory usage: 116 MB
% 14.40/2.90 % (1620205)Instructions burned: 15 (million)
% 14.40/2.90 % (1620206)Instruction limit reached!
% 14.40/2.90 % (1620206)------------------------------
% 14.40/2.90 % (1620206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620206)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620206)Termination reason: Instruction limit
% 14.40/2.90 % (1620206)Termination phase: Saturation
% 14.40/2.90 % (1620206)Time elapsed: 0.069 s
% 14.40/2.90 % (1620206)Peak memory usage: 89 MB
% 14.40/2.90 % (1620206)Instructions burned: 122 (million)
% 14.40/2.90 % (1620209)Instruction limit reached!
% 14.40/2.90 % (1620209)------------------------------
% 14.40/2.90 % (1620209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620209)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620209)Termination reason: Instruction limit
% 14.40/2.90 % (1620209)Termination phase: Saturation
% 14.40/2.90 % (1620209)Time elapsed: 0.060 s
% 14.40/2.90 % (1620209)Peak memory usage: 117 MB
% 14.40/2.90 % (1620209)Instructions burned: 130 (million)
% 14.40/2.90 % (1620210)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=32385966:i=39:ins=3:rtra=on_2986 on theBenchmark for (2986ds/39Mi)
% 14.40/2.90 % (1620202)Instruction limit reached!
% 14.40/2.90 % (1620202)------------------------------
% 14.40/2.90 % (1620202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620202)CaDiCaL version: 2.1.3
% 14.40/2.90 % (1620202)Termination reason: Instruction limit
% 14.40/2.90 % (1620202)Termination phase: Saturation
% 14.40/2.90 % (1620202)Time elapsed: 0.198 s
% 14.40/2.90 % (1620202)Peak memory usage: 92 MB
% 14.40/2.90 % (1620202)Instructions burned: 384 (million)
% 14.40/2.90 % (1620210)Instruction limit reached!
% 14.40/2.90 % (1620210)------------------------------
% 14.40/2.90 % (1620210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.90 % (1620210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.90 % (1620210)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620210)Termination reason: Instruction limit
% 17.60/3.18 % (1620210)Termination phase: Saturation
% 17.60/3.18 % (1620210)Time elapsed: 0.051 s
% 17.60/3.18 % (1620210)Peak memory usage: 116 MB
% 17.60/3.18 % (1620210)Instructions burned: 40 (million)
% 17.60/3.18 % (1620213)dis+1010_1_to=kbo:si=on:random_seed=2016515376:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 17.60/3.18 % (1620216)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3984206709:s2a=on:i=483:doe=on:nm=32:rtra=on_2985 on theBenchmark for (2985ds/483Mi)
% 17.60/3.18 % (1620215)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1661003134:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/329Mi)
% 17.60/3.18 % (1620218)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4187099504:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 17.60/3.18 % (1620205)------------------------------
% 17.60/3.18 % (1620205)------------------------------
% 17.60/3.18 % (1620213)Instruction limit reached!
% 17.60/3.18 % (1620213)------------------------------
% 17.60/3.18 % (1620213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.18 % (1620213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.18 % (1620213)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620213)Termination reason: Instruction limit
% 17.60/3.18 % (1620213)Termination phase: Saturation
% 17.60/3.18 % (1620213)Time elapsed: 0.118 s
% 17.60/3.18 % (1620213)Peak memory usage: 91 MB
% 17.60/3.18 % (1620213)Instructions burned: 176 (million)
% 17.60/3.18 % (1620219)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1236792001:i=349:rtra=on_2984 on theBenchmark for (2984ds/349Mi)
% 17.60/3.18 % (1620216)Instruction limit reached!
% 17.60/3.18 % (1620216)------------------------------
% 17.60/3.18 % (1620216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.18 % (1620216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.18 % (1620216)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620216)Termination reason: Instruction limit
% 17.60/3.18 % (1620216)Termination phase: Saturation
% 17.60/3.18 % (1620216)Time elapsed: 0.178 s
% 17.60/3.18 % (1620216)Peak memory usage: 134 MB
% 17.60/3.18 % (1620216)Instructions burned: 484 (million)
% 17.60/3.18 % (1620199)Instruction limit reached!
% 17.60/3.18 % (1620199)------------------------------
% 17.60/3.18 % (1620199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.18 % (1620199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.18 % (1620199)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620199)Termination reason: Instruction limit
% 17.60/3.18 % (1620199)Termination phase: Saturation
% 17.60/3.18 % (1620199)Time elapsed: 0.572 s
% 17.60/3.18 % (1620199)Peak memory usage: 93 MB
% 17.60/3.18 % (1620199)Instructions burned: 1001 (million)
% 17.60/3.18 % (1620215)Instruction limit reached!
% 17.60/3.18 % (1620215)------------------------------
% 17.60/3.18 % (1620215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.18 % (1620215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.18 % (1620215)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620215)Termination reason: Instruction limit
% 17.60/3.18 % (1620215)Termination phase: Saturation
% 17.60/3.18 % (1620215)Time elapsed: 0.207 s
% 17.60/3.18 % (1620215)Peak memory usage: 117 MB
% 17.60/3.18 % (1620215)Instructions burned: 331 (million)
% 17.60/3.18 % (1620224)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2096476076:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 17.60/3.18 % (1620218)Instruction limit reached!
% 17.60/3.18 % (1620218)------------------------------
% 17.60/3.18 % (1620218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.60/3.18 % (1620218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.60/3.18 % (1620218)CaDiCaL version: 2.1.3
% 17.60/3.18 % (1620218)Termination reason: Instruction limit
% 17.60/3.18 % (1620218)Termination phase: Saturation
% 17.60/3.18 % (1620218)Time elapsed: 0.168 s
% 17.60/3.18 % (1620218)Peak memory usage: 135 MB
% 17.60/3.18 % (1620218)Instructions burned: 215 (million)
% 17.60/3.18 % (1620225)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2305974825:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi)
% 17.84/3.38 % (1620227)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3064012983:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 17.84/3.38 % (1620219)Instruction limit reached!
% 17.84/3.38 % (1620219)------------------------------
% 17.84/3.38 % (1620219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.38 % (1620219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.38 % (1620219)CaDiCaL version: 2.1.3
% 17.84/3.38 % (1620219)Termination reason: Instruction limit
% 17.84/3.38 % (1620219)Termination phase: Saturation
% 17.84/3.38 % (1620219)Time elapsed: 0.221 s
% 17.84/3.38 % (1620219)Peak memory usage: 117 MB
% 17.84/3.38 % (1620219)Instructions burned: 350 (million)
% 17.84/3.38 % (1620228)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1714704342:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 17.84/3.38 % (1620230)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3685329562:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi)
% 17.84/3.38 % (1620231)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3217454385:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi)
% 17.84/3.38 % (1620224)Instruction limit reached!
% 17.84/3.38 % (1620224)------------------------------
% 17.84/3.38 % (1620224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.38 % (1620224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.38 % (1620224)CaDiCaL version: 2.1.3
% 17.84/3.38 % (1620224)Termination reason: Instruction limit
% 17.84/3.38 % (1620224)Termination phase: Saturation
% 17.84/3.38 % (1620224)Time elapsed: 0.163 s
% 17.84/3.38 % (1620224)Peak memory usage: 90 MB
% 17.84/3.38 % (1620224)Instructions burned: 296 (million)
% 17.84/3.38 % (1620227)Instruction limit reached!
% 17.84/3.38 % (1620227)------------------------------
% 17.84/3.38 % (1620227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.38 % (1620227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.38 % (1620227)CaDiCaL version: 2.1.3
% 17.84/3.38 % (1620227)Termination reason: Instruction limit
% 17.84/3.38 % (1620227)Termination phase: Saturation
% 17.84/3.38 % (1620227)Time elapsed: 0.110 s
% 17.84/3.38 % (1620227)Peak memory usage: 117 MB
% 17.84/3.38 % (1620227)Instructions burned: 284 (million)
% 17.84/3.38 % (1620225)Instruction limit reached!
% 17.84/3.38 % (1620225)------------------------------
% 17.84/3.38 % (1620225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.38 % (1620225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.38 % (1620225)CaDiCaL version: 2.1.3
% 17.84/3.38 % (1620225)Termination reason: Instruction limit
% 17.84/3.38 % (1620225)Termination phase: Saturation
% 17.84/3.38 % (1620225)Time elapsed: 0.232 s
% 17.84/3.38 % (1620225)Peak memory usage: 118 MB
% 17.84/3.38 % (1620225)Instructions burned: 328 (million)
% 17.84/3.38 % (1620234)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=256396390:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi)
% 17.84/3.38 % (1620239)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3484573379:i=375:kws=inv_arity_squared:rtra=on_2980 on theBenchmark for (2980ds/375Mi)
% 17.84/3.38 % (1620238)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1599707641:avsq=on:i=276:avsqr=1,2:rtra=on_2980 on theBenchmark for (2980ds/276Mi)
% 17.84/3.38 % (1620230)Instruction limit reached!
% 17.84/3.38 % (1620230)------------------------------
% 17.84/3.38 % (1620230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.84/3.38 % (1620230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.84/3.38 % (1620230)CaDiCaL version: 2.1.3
% 17.84/3.38 % (1620230)Termination reason: Instruction limit
% 17.84/3.38 % (1620230)Termination phase: Saturation
% 17.84/3.38 % (1620230)Time elapsed: 0.158 s
% 17.84/3.38 % (1620230)Peak memory usage: 114 MB
% 17.84/3.38 % (1620230)Instructions burned: 321 (million)
% 17.84/3.38 % (1620231)Instruction limit reached!
% 17.84/3.38 % (1620231)------------------------------
% 17.84/3.38 % (1620231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620231)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620231)Termination reason: Instruction limit
% 20.33/3.79 % (1620231)Termination phase: Saturation
% 20.33/3.79 % (1620231)Time elapsed: 0.250 s
% 20.33/3.79 % (1620231)Peak memory usage: 117 MB
% 20.33/3.79 % (1620231)Instructions burned: 416 (million)
% 20.33/3.79 % (1620239)Instruction limit reached!
% 20.33/3.79 % (1620239)------------------------------
% 20.33/3.79 % (1620239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620239)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620239)Termination reason: Instruction limit
% 20.33/3.79 % (1620239)Termination phase: Saturation
% 20.33/3.79 % (1620239)Time elapsed: 0.121 s
% 20.33/3.79 % (1620239)Peak memory usage: 117 MB
% 20.33/3.79 % (1620239)Instructions burned: 376 (million)
% 20.33/3.79 % (1620228)Instruction limit reached!
% 20.33/3.79 % (1620228)------------------------------
% 20.33/3.79 % (1620228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620228)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620228)Termination reason: Instruction limit
% 20.33/3.79 % (1620228)Termination phase: Saturation
% 20.33/3.79 % (1620228)Time elapsed: 0.283 s
% 20.33/3.79 % (1620228)Peak memory usage: 94 MB
% 20.33/3.79 % (1620228)Instructions burned: 484 (million)
% 20.33/3.79 % (1620241)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3713267741:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/387Mi)
% 20.33/3.79 % (1620244)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3589533716:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2978 on theBenchmark for (2978ds/513Mi)
% 20.33/3.79 % (1620247)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3464024800:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi)
% 20.33/3.79 % (1620238)Instruction limit reached!
% 20.33/3.79 % (1620238)------------------------------
% 20.33/3.79 % (1620238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620238)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620238)Termination reason: Instruction limit
% 20.33/3.79 % (1620238)Termination phase: Saturation
% 20.33/3.79 % (1620238)Time elapsed: 0.236 s
% 20.33/3.79 % (1620238)Peak memory usage: 135 MB
% 20.33/3.79 % (1620238)Instructions burned: 277 (million)
% 20.33/3.79 % (1620245)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2653773463:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi)
% 20.33/3.79 % (1620234)Instruction limit reached!
% 20.33/3.79 % (1620234)------------------------------
% 20.33/3.79 % (1620234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620234)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620234)Termination reason: Instruction limit
% 20.33/3.79 % (1620234)Termination phase: Saturation
% 20.33/3.79 % (1620234)Time elapsed: 0.306 s
% 20.33/3.79 % (1620234)Peak memory usage: 119 MB
% 20.33/3.79 % (1620234)Instructions burned: 471 (million)
% 20.33/3.79 % (1620248)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=842272780:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2977 on theBenchmark for (2977ds/341Mi)
% 20.33/3.79 % (1620247)Instruction limit reached!
% 20.33/3.79 % (1620247)------------------------------
% 20.33/3.79 % (1620247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.33/3.79 % (1620247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.33/3.79 % (1620247)CaDiCaL version: 2.1.3
% 20.33/3.79 % (1620247)Termination reason: Instruction limit
% 20.33/3.79 % (1620247)Termination phase: Saturation
% 20.33/3.79 % (1620247)Time elapsed: 0.114 s
% 20.33/3.79 % (1620247)Peak memory usage: 91 MB
% 20.33/3.79 % (1620247)Instructions burned: 359 (million)
% 20.33/3.79 % (1620251)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1943334190:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi)
% 24.98/4.24 % (1620241)Instruction limit reached!
% 24.98/4.24 % (1620241)------------------------------
% 24.98/4.24 % (1620241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620241)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620241)Termination reason: Instruction limit
% 24.98/4.24 % (1620241)Termination phase: Saturation
% 24.98/4.24 % (1620241)Time elapsed: 0.274 s
% 24.98/4.24 % (1620241)Peak memory usage: 118 MB
% 24.98/4.24 % (1620241)Instructions burned: 388 (million)
% 24.98/4.24 % (1620253)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=485453611:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi)
% 24.98/4.24 % (1620255)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3164665547:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi)
% 24.98/4.24 % (1620244)Instruction limit reached!
% 24.98/4.24 % (1620244)------------------------------
% 24.98/4.24 % (1620244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620244)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620244)Termination reason: Instruction limit
% 24.98/4.24 % (1620244)Termination phase: Saturation
% 24.98/4.24 % (1620244)Time elapsed: 0.319 s
% 24.98/4.24 % (1620244)Peak memory usage: 92 MB
% 24.98/4.24 % (1620244)Instructions burned: 513 (million)
% 24.98/4.24 % (1620245)Instruction limit reached!
% 24.98/4.24 % (1620245)------------------------------
% 24.98/4.24 % (1620245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620245)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620245)Termination reason: Instruction limit
% 24.98/4.24 % (1620245)Termination phase: Saturation
% 24.98/4.24 % (1620245)Time elapsed: 0.245 s
% 24.98/4.24 % (1620245)Peak memory usage: 135 MB
% 24.98/4.24 % (1620245)Instructions burned: 335 (million)
% 24.98/4.24 % (1620248)Instruction limit reached!
% 24.98/4.24 % (1620248)------------------------------
% 24.98/4.24 % (1620248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620248)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620248)Termination reason: Instruction limit
% 24.98/4.24 % (1620248)Termination phase: Saturation
% 24.98/4.24 % (1620248)Time elapsed: 0.230 s
% 24.98/4.24 % (1620248)Peak memory usage: 119 MB
% 24.98/4.24 % (1620248)Instructions burned: 343 (million)
% 24.98/4.24 % (1620255)Instruction limit reached!
% 24.98/4.24 % (1620255)------------------------------
% 24.98/4.24 % (1620255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620255)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620255)Termination reason: Instruction limit
% 24.98/4.24 % (1620255)Termination phase: Saturation
% 24.98/4.24 % (1620255)Time elapsed: 0.099 s
% 24.98/4.24 % (1620255)Peak memory usage: 91 MB
% 24.98/4.24 % (1620255)Instructions burned: 274 (million)
% 24.98/4.24 % (1620257)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1075502530:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi)
% 24.98/4.24 % (1620251)Instruction limit reached!
% 24.98/4.24 % (1620251)------------------------------
% 24.98/4.24 % (1620251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620251)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620251)Termination reason: Instruction limit
% 24.98/4.24 % (1620251)Termination phase: Saturation
% 24.98/4.24 % (1620251)Time elapsed: 0.171 s
% 24.98/4.24 % (1620251)Peak memory usage: 117 MB
% 24.98/4.24 % (1620251)Instructions burned: 262 (million)
% 24.98/4.24 % (1620253)Instruction limit reached!
% 24.98/4.24 % (1620253)------------------------------
% 24.98/4.24 % (1620253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620253)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620253)Termination reason: Instruction limit
% 24.98/4.24 % (1620253)Termination phase: Saturation
% 24.98/4.24 % (1620253)Time elapsed: 0.168 s
% 24.98/4.24 % (1620253)Peak memory usage: 117 MB
% 24.98/4.24 % (1620253)Instructions burned: 236 (million)
% 24.98/4.24 % (1620260)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2865863869:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 24.98/4.24 % (1620261)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3287557378:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi)
% 24.98/4.24 % (1620263)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2940129308:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2973 on theBenchmark for (2973ds/655Mi)
% 24.98/4.24 % (1620257)Instruction limit reached!
% 24.98/4.24 % (1620257)------------------------------
% 24.98/4.24 % (1620257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620257)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620257)Termination reason: Instruction limit
% 24.98/4.24 % (1620257)Termination phase: Saturation
% 24.98/4.24 % (1620257)Time elapsed: 0.100 s
% 24.98/4.24 % (1620257)Peak memory usage: 90 MB
% 24.98/4.24 % (1620257)Instructions burned: 146 (million)
% 24.98/4.24 % (1620262)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=324661459:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi)
% 24.98/4.24 % (1620265)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3170206690:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2973 on theBenchmark for (2973ds/1054Mi)
% 24.98/4.24 % (1620266)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1343335727:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi)
% 24.98/4.24 % (1620270)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=737147122:s2a=on:i=450:doe=on:nm=32:rtra=on_2972 on theBenchmark for (2972ds/450Mi)
% 24.98/4.24 % (1620266)Instruction limit reached!
% 24.98/4.24 % (1620266)------------------------------
% 24.98/4.24 % (1620266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620266)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620266)Termination reason: Instruction limit
% 24.98/4.24 % (1620266)Termination phase: Saturation
% 24.98/4.24 % (1620266)Time elapsed: 0.089 s
% 24.98/4.24 % (1620266)Peak memory usage: 116 MB
% 24.98/4.24 % (1620266)Instructions burned: 108 (million)
% 24.98/4.24 % (1620263)Instruction limit reached!
% 24.98/4.24 % (1620263)------------------------------
% 24.98/4.24 % (1620263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620263)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620263)Termination reason: Instruction limit
% 24.98/4.24 % (1620263)Termination phase: Saturation
% 24.98/4.24 % (1620263)Time elapsed: 0.220 s
% 24.98/4.24 % (1620263)Peak memory usage: 94 MB
% 24.98/4.24 % (1620263)Instructions burned: 657 (million)
% 24.98/4.24 % (1620261)Instruction limit reached!
% 24.98/4.24 % (1620261)------------------------------
% 24.98/4.24 % (1620261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620261)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620261)Termination reason: Instruction limit
% 24.98/4.24 % (1620261)Termination phase: Saturation
% 24.98/4.24 % (1620261)Time elapsed: 0.232 s
% 24.98/4.24 % (1620261)Peak memory usage: 135 MB
% 24.98/4.24 % (1620261)Instructions burned: 277 (million)
% 24.98/4.24 % (1620275)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 24.98/4.24 % (1620275)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2438765773:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi)
% 24.98/4.24 % (1620276)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2049188763:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi)
% 24.98/4.24 % (1620277)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3666102125:i=312:kws=inv_frequency:nm=20:rtra=on_2970 on theBenchmark for (2970ds/312Mi)
% 24.98/4.24 % (1620276)Instruction limit reached!
% 24.98/4.24 % (1620276)------------------------------
% 24.98/4.24 % (1620276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620276)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620276)Termination reason: Instruction limit
% 24.98/4.24 % (1620276)Termination phase: Saturation
% 24.98/4.24 % (1620276)Time elapsed: 0.058 s
% 24.98/4.24 % (1620276)Peak memory usage: 117 MB
% 24.98/4.24 % (1620276)Instructions burned: 132 (million)
% 24.98/4.24 % (1620270)Instruction limit reached!
% 24.98/4.24 % (1620270)------------------------------
% 24.98/4.24 % (1620270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620270)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620270)Termination reason: Instruction limit
% 24.98/4.24 % (1620270)Termination phase: Saturation
% 24.98/4.24 % (1620270)Time elapsed: 0.317 s
% 24.98/4.24 % (1620270)Peak memory usage: 135 MB
% 24.98/4.24 % (1620270)Instructions burned: 451 (million)
% 24.98/4.24 % (1620281)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3147386013:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi)
% 24.98/4.24 % (1620265)First to succeed.
% 24.98/4.24 % (1620265)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1620114"
% 24.98/4.24 % (1620277)Instruction limit reached!
% 24.98/4.24 % (1620277)------------------------------
% 24.98/4.24 % (1620277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620277)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620277)Termination reason: Instruction limit
% 24.98/4.24 % (1620277)Termination phase: Saturation
% 24.98/4.24 % (1620277)Time elapsed: 0.214 s
% 24.98/4.24 % (1620277)Peak memory usage: 118 MB
% 24.98/4.24 % (1620277)Instructions burned: 312 (million)
% 24.98/4.24 % (1620262)Instruction limit reached!
% 24.98/4.24 % (1620262)------------------------------
% 24.98/4.24 % (1620262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620262)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620262)Termination reason: Instruction limit
% 24.98/4.24 % (1620262)Termination phase: Saturation
% 24.98/4.24 % (1620262)Time elapsed: 0.629 s
% 24.98/4.24 % (1620262)Peak memory usage: 94 MB
% 24.98/4.24 % (1620262)Instructions burned: 1052 (million)
% 24.98/4.24 % (1620282)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=3316877722:s2a=on:i=835:s2at=2:rtra=on_2967 on theBenchmark for (2967ds/835Mi)
% 24.98/4.24 % (1620281)Instruction limit reached!
% 24.98/4.24 % (1620281)------------------------------
% 24.98/4.24 % (1620281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.98/4.24 % (1620281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.98/4.24 % (1620281)CaDiCaL version: 2.1.3
% 24.98/4.24 % (1620281)Termination reason: Instruction limit
% 24.98/4.24 % (1620281)Termination phase: Saturation
% 24.98/4.24 % (1620281)Time elapsed: 0.157 s
% 24.98/4.24 % (1620281)Peak memory usage: 91 MB
% 24.98/4.24 % (1620281)Instructions burned: 494 (million)
% 24.98/4.24 % (1620284)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3205189009:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi)
% 24.98/4.24 % (1620265)Refutation found. Thanks to Tanya!
% 24.98/4.24 % SZS status Theorem for theBenchmark
% 24.98/4.24 % SZS output start Proof for theBenchmark
% See solution above
% 25.71/4.34 % (1620265)------------------------------
% 25.71/4.34 % (1620265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.71/4.34 % (1620265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.71/4.34 % (1620265)CaDiCaL version: 2.1.3
% 25.71/4.34 % (1620265)Termination reason: Refutation
% 25.71/4.34 % (1620265)Time elapsed: 0.484 s
% 25.71/4.34 % (1620265)Peak memory usage: 95 MB
% 25.71/4.34 % (1620265)Instructions burned: 815 (million)
% 25.71/4.34 % (1620265)------------------------------
% 25.71/4.34 % (1620265)------------------------------
% 25.71/4.34 % (1620114)Success in time 3.562 s
% 25.71/4.34 % Vampire exiting
%------------------------------------------------------------------------------