%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW664_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:31:05 PM UTC 2026
% Result : Theorem 17.17s 3.50s
% Output : Refutation 18.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 20
% Syntax : Number of formulae : 163 ( 39 unt; 0 typ; 5 def)
% Number of atoms : 529 ( 229 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 538 ( 172 ~; 161 |; 179 &)
% ( 4 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 11 ( 2 avg)
% Number arithmetic : 946 ( 88 atm; 458 fun; 230 num; 170 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 : 13 ( 9 usr; 5 prp; 0-4 aty)
% Number of functors : 57 ( 52 usr; 16 con; 0-5 aty)
% Number of variables : 316 ( 0 sgn 245 !; 71 ?; 316 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
map_int_int: $tType ).
tff(type_def_10,type,
array_int: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
abs1: $int > $int ).
tff(func_def_14,type,
div1: ( $int * $int ) > $int ).
tff(func_def_15,type,
mod1: ( $int * $int ) > $int ).
tff(func_def_18,type,
power1: ( $int * $int ) > $int ).
tff(func_def_20,type,
map: ( ty * ty ) > ty ).
tff(func_def_21,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_22,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_23,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_24,type,
array: ty > ty ).
tff(func_def_25,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_26,type,
length1: ( ty * uni ) > $int ).
tff(func_def_27,type,
elts: ( ty * uni ) > uni ).
tff(func_def_28,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_29,type,
t2tb: $int > uni ).
tff(func_def_30,type,
tb2t: uni > $int ).
tff(func_def_31,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_32,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_33,type,
sum2: ( map_int_int * $int * $int ) > $int ).
tff(func_def_34,type,
t2tb1: map_int_int > uni ).
tff(func_def_35,type,
tb2t1: uni > map_int_int ).
tff(func_def_36,type,
sum3: ( array_int * $int * $int ) > $int ).
tff(func_def_37,type,
t2tb2: array_int > uni ).
tff(func_def_38,type,
tb2t2: uni > array_int ).
tff(func_def_40,type,
go_left1: ( $int * $int ) > $int ).
tff(func_def_41,type,
go_right1: ( $int * $int ) > $int ).
tff(func_def_42,type,
sK1: map_int_int ).
tff(func_def_43,type,
sK2: $int ).
tff(func_def_44,type,
sK3: map_int_int ).
tff(func_def_45,type,
sK4: $int ).
tff(func_def_46,type,
sK5: $int ).
tff(func_def_47,type,
sK6: $int ).
tff(func_def_48,type,
sK7: $int > $int ).
tff(func_def_49,type,
sK8: ( $int * array_int * array_int * $int ) > $int ).
tff(func_def_50,type,
sK9: ( map_int_int * $int * $int * map_int_int ) > $int ).
tff(func_def_51,type,
sK10: ( array_int * array_int * $int * $int ) > array_int ).
tff(func_def_52,type,
sK11: ( array_int * array_int * $int * $int ) > $int ).
tff(func_def_53,type,
sK12: ( array_int * array_int * $int * $int ) > $int ).
tff(func_def_54,type,
sK13: ( array_int * array_int * $int * $int ) > array_int ).
tff(func_def_55,type,
sK14: ( $int * $int * array_int * array_int ) > $int ).
tff(func_def_56,type,
sK15: ( $int * $int * array_int * array_int ) > array_int ).
tff(func_def_57,type,
sK16: ( $int * $int * array_int * array_int ) > array_int ).
tff(func_def_58,type,
sK17: ( array_int * $int * $int * array_int ) > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_4,type,
is_power_of_21: $int > $o ).
tff(pred_def_5,type,
phase11: ( $int * $int * array_int * array_int ) > $o ).
tff(pred_def_6,type,
partial_sum1: ( $int * $int * array_int * array_int ) > $o ).
tff(pred_def_7,type,
sP0: ( array_int * array_int * $int * $int ) > $o ).
tff(f42,axiom,
! [X0: ty,X2: uni,X1: $int] :
( sort1(map(int,X0),X2)
=> ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def1) ).
tff(f48,axiom,
! [X1: uni,X2: $int,X0: ty] : ( get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def) ).
tff(f53,axiom,
! [X1: $int,X2: $int,X0: map_int_int] :
( $lesseq(X2,X1)
=> ( sum2(X0,X1,X2) = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def_empty) ).
tff(f54,axiom,
! [X0: map_int_int] : sort1(map(int,int),t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f55,axiom,
! [X0: map_int_int] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL1) ).
tff(f57,axiom,
! [X1: $int,X0: map_int_int,X2: $int] :
( $less(X1,X2)
=> ( sum2(X0,X1,X2) = $sum(tb2t(get(int,int,t2tb1(X0),t2tb(X1))),sum2(X0,$sum(X1,1),X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def_non_empty) ).
tff(f63,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(f64,axiom,
! [X1: $int,X0: array_int,X2: $int] : ( sum3(X0,X1,X2) = sum2(tb2t1(elts(int,t2tb2(X0))),X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def) ).
tff(f72,axiom,
! [X2: array_int,X0: $int,X1: $int,X3: array_int] :
( phase11(X0,X1,X2,X3)
=> ( ? [X6: array_int,X5: array_int,X7: $int,X4: $int] :
( phase11(go_left1(X4,X7),X4,X5,X6)
& phase11(go_right1(X4,X7),X7,X5,X6)
& ( tb2t(get2(int,t2tb2(X6),X4)) = sum3(X5,$sum($difference(X4,$difference(X7,X4)),1),$sum(X4,1)) )
& ( X3 = X6 )
& $less($sum(X4,1),X7)
& ( X2 = X5 )
& ( X0 = X4 )
& ( X1 = X7 ) )
| ? [X6: array_int,X5: array_int,X4: $int] :
( ( X1 = $sum(X4,1) )
& ( X0 = X4 )
& ( X3 = X6 )
& ( tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) )
& ( X2 = X5 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',phase1_inversion) ).
tff(f76,conjecture,
! [X3: map_int_int,X5: map_int_int,X4: $int,X2: $int,X0: $int,X1: $int] :
( ( $lesseq(0,X2)
& $less(X0,X1)
& $less(X1,X4)
& is_power_of_21($difference(X1,X0))
& phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))
& $lesseq(0,X0)
& $lesseq($uminus(1),$difference(X0,$difference(X1,X0)))
& ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) )
& $lesseq(0,X4) )
=> ( ( $lesseq(0,X1)
& $less(X1,X4) )
=> ( ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) )
=> ( tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($difference(X0,$difference(X1,X0)),1),$sum(X0,1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_downsweep) ).
tff(f77,negated_conjecture,
~ ! [X3: map_int_int,X5: map_int_int,X4: $int,X2: $int,X0: $int,X1: $int] :
( ( $lesseq(0,X2)
& $less(X0,X1)
& $less(X1,X4)
& is_power_of_21($difference(X1,X0))
& phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))
& $lesseq(0,X0)
& $lesseq($uminus(1),$difference(X0,$difference(X1,X0)))
& ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) )
& $lesseq(0,X4) )
=> ( ( $lesseq(0,X1)
& $less(X1,X4) )
=> ( ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($difference(X0,$difference(X1,X0)),1)) )
=> ( tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($difference(X0,$difference(X1,X0)),1),$sum(X0,1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f76]) ).
tff(f85,plain,
! [X2: array_int,X0: $int,X1: $int,X3: array_int] :
( phase11(X0,X1,X2,X3)
=> ( ? [X6: array_int,X5: array_int,X7: $int,X4: $int] :
( phase11(go_left1(X4,X7),X4,X5,X6)
& phase11(go_right1(X4,X7),X7,X5,X6)
& ( tb2t(get2(int,t2tb2(X6),X4)) = sum3(X5,$sum($sum(X4,$uminus($sum(X7,$uminus(X4)))),1),$sum(X4,1)) )
& ( X3 = X6 )
& $less($sum(X4,1),X7)
& ( X2 = X5 )
& ( X0 = X4 )
& ( X1 = X7 ) )
| ? [X6: array_int,X5: array_int,X4: $int] :
( ( X1 = $sum(X4,1) )
& ( X0 = X4 )
& ( X3 = X6 )
& ( tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) )
& ( X2 = X5 ) ) ) ),
inference(theory_normalization,[],[f72]) ).
tff(f104,plain,
~ ! [X3: map_int_int,X5: map_int_int,X4: $int,X2: $int,X0: $int,X1: $int] :
( ( ~ $less(X2,0)
& $less(X0,X1)
& $less(X1,X4)
& is_power_of_21($sum(X1,$uminus(X0)))
& phase11(X0,X1,tb2t2(mk_array1(int,X2,t2tb1(X3))),tb2t2(mk_array1(int,X4,t2tb1(X5))))
& ~ $less(X0,0)
& ~ $less($sum(X0,$uminus($sum(X1,$uminus(X0)))),$uminus(1))
& ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) )
& ~ $less(X4,0) )
=> ( ( ~ $less(X1,0)
& $less(X1,X4) )
=> ( ( tb2t(get(int,int,t2tb1(X5),t2tb(X1))) = sum2(X3,0,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1)) )
=> ( tb2t(get(int,int,t2tb1(X5),t2tb(X0))) = sum2(X3,$sum($sum(X0,$uminus($sum(X1,$uminus(X0)))),1),$sum(X0,1)) ) ) ) ),
inference(theory_normalization,[],[f77]) ).
tff(f108,plain,
! [X1: $int,X2: $int,X0: map_int_int] :
( ~ $less(X1,X2)
=> ( sum2(X0,X1,X2) = 0 ) ),
inference(theory_normalization,[],[f53]) ).
tff(f111,plain,
! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f112,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) ),
introduced(definition,[],[tha_associativity]) ).
tff(f114,plain,
! [X0: $int,X1: $int] : ( $uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0)) ),
introduced(definition,[],[tha_inverse_op_op_inverses]) ).
tff(f115,plain,
! [X0: $int] : ( 0 = $sum(X0,$uminus(X0)) ),
introduced(definition,[],[tha_inverse_op_unit]) ).
tff(f121,plain,
! [X0: $int] : ( $uminus($uminus(X0)) = X0 ),
introduced(definition,[],[tha_minus_minus_x]) ).
tff(f142,plain,
! [X2: $int,X0: array_int,X1: $int,X3: array_int] :
( phase11(X1,X2,X0,X3)
=> ( ? [X5: array_int,X6: $int,X7: $int,X4: array_int] :
( ( X3 = X4 )
& phase11(go_left1(X7,X6),X7,X5,X4)
& phase11(go_right1(X7,X6),X6,X5,X4)
& ( X0 = X5 )
& ( sum3(X5,$sum($sum(X7,$uminus($sum(X6,$uminus(X7)))),1),$sum(X7,1)) = tb2t(get2(int,t2tb2(X4),X7)) )
& ( X1 = X7 )
& $less($sum(X7,1),X6)
& ( X2 = X6 ) )
| ? [X10: $int,X9: array_int,X8: array_int] :
( ( $sum(X10,1) = X2 )
& ( X3 = X8 )
& ( tb2t(get2(int,t2tb2(X8),X10)) = tb2t(get2(int,t2tb2(X9),X10)) )
& ( X1 = X10 )
& ( X0 = X9 ) ) ) ),
inference(rectify,[],[f85]) ).
tff(f145,plain,
! [X0: ty,X1: uni,X2: $int] :
( sort1(map(int,X0),X1)
=> ( elts(X0,mk_array1(X0,X2,X1)) = X1 ) ),
inference(rectify,[],[f42]) ).
tff(f153,plain,
! [X2: ty,X1: $int,X0: uni] : ( get(X2,int,elts(X2,X0),t2tb(X1)) = get2(X2,X0,X1) ),
inference(rectify,[],[f48]) ).
tff(f157,plain,
! [X1: array_int,X0: $int,X2: $int] : ( sum2(tb2t1(elts(int,t2tb2(X1))),X0,X2) = sum3(X1,X0,X2) ),
inference(rectify,[],[f64]) ).
tff(f164,plain,
~ ! [X2: $int,X0: map_int_int,X5: $int,X4: $int,X1: map_int_int,X3: $int] :
( ( ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
& ~ $less(X2,0)
& ~ $less(X4,0)
& $less(X5,X2)
& phase11(X4,X5,tb2t2(mk_array1(int,X3,t2tb1(X0))),tb2t2(mk_array1(int,X2,t2tb1(X1))))
& is_power_of_21($sum(X5,$uminus(X4)))
& ~ $less(X3,0)
& ~ $less($sum(X4,$uminus($sum(X5,$uminus(X4)))),$uminus(1))
& $less(X4,X5) )
=> ( ( $less(X5,X2)
& ~ $less(X5,0) )
=> ( ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
=> ( tb2t(get(int,int,t2tb1(X1),t2tb(X4))) = sum2(X0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1),$sum(X4,1)) ) ) ) ),
inference(rectify,[],[f104]) ).
tff(f165,plain,
! [X2: $int,X0: $int,X1: map_int_int] :
( $less(X0,X2)
=> ( $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X0))),sum2(X1,$sum(X0,1),X2)) = sum2(X1,X0,X2) ) ),
inference(rectify,[],[f57]) ).
tff(f171,plain,
! [X0: $int,X1: $int,X2: map_int_int] :
( ~ $less(X0,X1)
=> ( 0 = sum2(X2,X0,X1) ) ),
inference(rectify,[],[f108]) ).
tff(f180,plain,
! [X0: ty,X2: $int,X1: uni] :
( ~ sort1(map(int,X0),X1)
| ( elts(X0,mk_array1(X0,X2,X1)) = X1 ) ),
inference(ennf_transformation,[],[f145]) ).
tff(f181,plain,
? [X2: $int,X0: map_int_int,X5: $int,X4: $int,X1: map_int_int,X3: $int] :
( ( tb2t(get(int,int,t2tb1(X1),t2tb(X4))) != sum2(X0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1),$sum(X4,1)) )
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
& $less(X5,X2)
& ~ $less(X5,0)
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
& ~ $less(X2,0)
& ~ $less(X4,0)
& $less(X5,X2)
& phase11(X4,X5,tb2t2(mk_array1(int,X3,t2tb1(X0))),tb2t2(mk_array1(int,X2,t2tb1(X1))))
& is_power_of_21($sum(X5,$uminus(X4)))
& ~ $less(X3,0)
& ~ $less($sum(X4,$uminus($sum(X5,$uminus(X4)))),$uminus(1))
& $less(X4,X5) ),
inference(ennf_transformation,[],[f164]) ).
tff(f182,plain,
? [X1: map_int_int,X3: $int,X0: map_int_int,X2: $int,X5: $int,X4: $int] :
( ~ $less(X2,0)
& $less(X5,X2)
& $less(X4,X5)
& ~ $less(X5,0)
& ~ $less(X4,0)
& $less(X5,X2)
& ~ $less($sum(X4,$uminus($sum(X5,$uminus(X4)))),$uminus(1))
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = sum2(X0,0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1)) )
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X4))) != sum2(X0,$sum($sum(X4,$uminus($sum(X5,$uminus(X4)))),1),$sum(X4,1)) )
& is_power_of_21($sum(X5,$uminus(X4)))
& ~ $less(X3,0)
& phase11(X4,X5,tb2t2(mk_array1(int,X3,t2tb1(X0))),tb2t2(mk_array1(int,X2,t2tb1(X1)))) ),
inference(flattening,[],[f181]) ).
tff(f199,plain,
! [X2: map_int_int,X1: $int,X0: $int] :
( ( 0 = sum2(X2,X0,X1) )
| $less(X0,X1) ),
inference(ennf_transformation,[],[f171]) ).
tff(f202,plain,
! [X2: $int,X0: array_int,X1: $int,X3: array_int] :
( ? [X5: array_int,X6: $int,X7: $int,X4: array_int] :
( ( X3 = X4 )
& phase11(go_left1(X7,X6),X7,X5,X4)
& phase11(go_right1(X7,X6),X6,X5,X4)
& ( X0 = X5 )
& ( sum3(X5,$sum($sum(X7,$uminus($sum(X6,$uminus(X7)))),1),$sum(X7,1)) = tb2t(get2(int,t2tb2(X4),X7)) )
& ( X1 = X7 )
& $less($sum(X7,1),X6)
& ( X2 = X6 ) )
| ? [X10: $int,X9: array_int,X8: array_int] :
( ( $sum(X10,1) = X2 )
& ( X3 = X8 )
& ( tb2t(get2(int,t2tb2(X8),X10)) = tb2t(get2(int,t2tb2(X9),X10)) )
& ( X1 = X10 )
& ( X0 = X9 ) )
| ~ phase11(X1,X2,X0,X3) ),
inference(ennf_transformation,[],[f142]) ).
tff(f203,plain,
! [X2: $int,X1: $int,X3: array_int,X0: array_int] :
( ~ phase11(X1,X2,X0,X3)
| ? [X5: array_int,X6: $int,X7: $int,X4: array_int] :
( ( X3 = X4 )
& phase11(go_left1(X7,X6),X7,X5,X4)
& phase11(go_right1(X7,X6),X6,X5,X4)
& ( X0 = X5 )
& ( sum3(X5,$sum($sum(X7,$uminus($sum(X6,$uminus(X7)))),1),$sum(X7,1)) = tb2t(get2(int,t2tb2(X4),X7)) )
& ( X1 = X7 )
& $less($sum(X7,1),X6)
& ( X2 = X6 ) )
| ? [X10: $int,X9: array_int,X8: array_int] :
( ( $sum(X10,1) = X2 )
& ( X3 = X8 )
& ( tb2t(get2(int,t2tb2(X8),X10)) = tb2t(get2(int,t2tb2(X9),X10)) )
& ( X1 = X10 )
& ( X0 = X9 ) ) ),
inference(flattening,[],[f202]) ).
tff(f221,plain,
! [X2: $int,X1: map_int_int,X0: $int] :
( ~ $less(X0,X2)
| ( $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X0))),sum2(X1,$sum(X0,1),X2)) = sum2(X1,X0,X2) ) ),
inference(ennf_transformation,[],[f165]) ).
tff(f235,definition,
! [X3: array_int,X0: array_int,X1: $int,X2: $int] :
( ? [X5: array_int,X6: $int,X7: $int,X4: array_int] :
( ( X3 = X4 )
& phase11(go_left1(X7,X6),X7,X5,X4)
& phase11(go_right1(X7,X6),X6,X5,X4)
& ( X0 = X5 )
& ( sum3(X5,$sum($sum(X7,$uminus($sum(X6,$uminus(X7)))),1),$sum(X7,1)) = tb2t(get2(int,t2tb2(X4),X7)) )
& ( X1 = X7 )
& $less($sum(X7,1),X6)
& ( X2 = X6 ) )
| ~ sP0(X3,X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f236,plain,
! [X2: $int,X1: $int,X3: array_int,X0: array_int] :
( ~ phase11(X1,X2,X0,X3)
| sP0(X3,X0,X1,X2)
| ? [X10: $int,X9: array_int,X8: array_int] :
( ( $sum(X10,1) = X2 )
& ( X3 = X8 )
& ( tb2t(get2(int,t2tb2(X8),X10)) = tb2t(get2(int,t2tb2(X9),X10)) )
& ( X1 = X10 )
& ( X0 = X9 ) ) ),
inference(definition_folding,[],[f203,f235]) ).
tff(f243,plain,
? [X0: map_int_int,X1: $int,X2: map_int_int,X3: $int,X4: $int,X5: $int] :
( ~ $less(X3,0)
& $less(X4,X3)
& $less(X5,X4)
& ~ $less(X4,0)
& ~ $less(X5,0)
& $less(X4,X3)
& ~ $less($sum(X5,$uminus($sum(X4,$uminus(X5)))),$uminus(1))
& ( tb2t(get(int,int,t2tb1(X0),t2tb(X4))) = sum2(X2,0,$sum($sum(X5,$uminus($sum(X4,$uminus(X5)))),1)) )
& ( tb2t(get(int,int,t2tb1(X0),t2tb(X4))) = sum2(X2,0,$sum($sum(X5,$uminus($sum(X4,$uminus(X5)))),1)) )
& ( tb2t(get(int,int,t2tb1(X0),t2tb(X5))) != sum2(X2,$sum($sum(X5,$uminus($sum(X4,$uminus(X5)))),1),$sum(X5,1)) )
& is_power_of_21($sum(X4,$uminus(X5)))
& ~ $less(X1,0)
& phase11(X5,X4,tb2t2(mk_array1(int,X1,t2tb1(X2))),tb2t2(mk_array1(int,X3,t2tb1(X0)))) ),
inference(rectify,[],[f182]) ).
tff(f244,plain,
( ~ $less(sK4,0)
& $less(sK5,sK4)
& $less(sK6,sK5)
& ~ $less(sK5,0)
& ~ $less(sK6,0)
& $less(sK5,sK4)
& ~ $less($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),$uminus(1))
& ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK5))) = sum2(sK3,0,$sum($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),1)) )
& ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK5))) = sum2(sK3,0,$sum($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),1)) )
& ( sum2(sK3,$sum($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),1),$sum(sK6,1)) != tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) )
& is_power_of_21($sum(sK5,$uminus(sK6)))
& ~ $less(sK2,0)
& phase11(sK6,sK5,tb2t2(mk_array1(int,sK2,t2tb1(sK3))),tb2t2(mk_array1(int,sK4,t2tb1(sK1)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X5,sK6)],[f243]) ).
tff(f247,plain,
! [X0: map_int_int,X1: $int,X2: $int] :
( ( 0 = sum2(X0,X2,X1) )
| $less(X2,X1) ),
inference(rectify,[],[f199]) ).
tff(f252,plain,
! [X0: array_int,X1: $int,X2: $int] : ( sum3(X0,X1,X2) = sum2(tb2t1(elts(int,t2tb2(X0))),X1,X2) ),
inference(rectify,[],[f157]) ).
tff(f264,plain,
! [X0: ty,X1: $int,X2: uni] : ( get(X0,int,elts(X0,X2),t2tb(X1)) = get2(X0,X2,X1) ),
inference(rectify,[],[f153]) ).
tff(f269,plain,
! [X0: ty,X1: $int,X2: uni] :
( ~ sort1(map(int,X0),X2)
| ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
inference(rectify,[],[f180]) ).
tff(f272,plain,
! [X3: array_int,X0: array_int,X1: $int,X2: $int] :
( ? [X5: array_int,X6: $int,X7: $int,X4: array_int] :
( ( X3 = X4 )
& phase11(go_left1(X7,X6),X7,X5,X4)
& phase11(go_right1(X7,X6),X6,X5,X4)
& ( X0 = X5 )
& ( sum3(X5,$sum($sum(X7,$uminus($sum(X6,$uminus(X7)))),1),$sum(X7,1)) = tb2t(get2(int,t2tb2(X4),X7)) )
& ( X1 = X7 )
& $less($sum(X7,1),X6)
& ( X2 = X6 ) )
| ~ sP0(X3,X0,X1,X2) ),
inference(nnf_transformation,[],[f235]) ).
tff(f273,plain,
! [X0: array_int,X1: array_int,X2: $int,X3: $int] :
( ? [X4: array_int,X5: $int,X6: $int,X7: array_int] :
( ( X0 = X7 )
& phase11(go_left1(X6,X5),X6,X4,X7)
& phase11(go_right1(X6,X5),X5,X4,X7)
& ( X1 = X4 )
& ( tb2t(get2(int,t2tb2(X7),X6)) = sum3(X4,$sum($sum(X6,$uminus($sum(X5,$uminus(X6)))),1),$sum(X6,1)) )
& ( X2 = X6 )
& $less($sum(X6,1),X5)
& ( X3 = X5 ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(rectify,[],[f272]) ).
tff(f274,plain,
! [X0: array_int,X1: array_int,X2: $int,X3: $int] :
( ( ( sK13(X0,X1,X2,X3) = X0 )
& phase11(go_left1(sK12(X0,X1,X2,X3),sK11(X0,X1,X2,X3)),sK12(X0,X1,X2,X3),sK10(X0,X1,X2,X3),sK13(X0,X1,X2,X3))
& phase11(go_right1(sK12(X0,X1,X2,X3),sK11(X0,X1,X2,X3)),sK11(X0,X1,X2,X3),sK10(X0,X1,X2,X3),sK13(X0,X1,X2,X3))
& ( sK10(X0,X1,X2,X3) = X1 )
& ( sum3(sK10(X0,X1,X2,X3),$sum($sum(sK12(X0,X1,X2,X3),$uminus($sum(sK11(X0,X1,X2,X3),$uminus(sK12(X0,X1,X2,X3))))),1),$sum(sK12(X0,X1,X2,X3),1)) = tb2t(get2(int,t2tb2(sK13(X0,X1,X2,X3)),sK12(X0,X1,X2,X3))) )
& ( sK12(X0,X1,X2,X3) = X2 )
& $less($sum(sK12(X0,X1,X2,X3),1),sK11(X0,X1,X2,X3))
& ( sK11(X0,X1,X2,X3) = X3 ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13]),skolemize(X4,sK10(X0,X1,X2,X3)),skolemize(X5,sK11(X0,X1,X2,X3)),skolemize(X6,sK12(X0,X1,X2,X3)),skolemize(X7,sK13(X0,X1,X2,X3))],[f273]) ).
tff(f275,plain,
! [X0: $int,X1: $int,X2: array_int,X3: array_int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ? [X4: $int,X5: array_int,X6: array_int] :
( ( $sum(X4,1) = X0 )
& ( X2 = X6 )
& ( tb2t(get2(int,t2tb2(X6),X4)) = tb2t(get2(int,t2tb2(X5),X4)) )
& ( X1 = X4 )
& ( X3 = X5 ) ) ),
inference(rectify,[],[f236]) ).
tff(f276,plain,
! [X0: $int,X1: $int,X2: array_int,X3: array_int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ( ( $sum(sK14(X0,X1,X2,X3),1) = X0 )
& ( sK16(X0,X1,X2,X3) = X2 )
& ( tb2t(get2(int,t2tb2(sK15(X0,X1,X2,X3)),sK14(X0,X1,X2,X3))) = tb2t(get2(int,t2tb2(sK16(X0,X1,X2,X3)),sK14(X0,X1,X2,X3))) )
& ( sK14(X0,X1,X2,X3) = X1 )
& ( sK15(X0,X1,X2,X3) = X3 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X4,sK14(X0,X1,X2,X3)),skolemize(X5,sK15(X0,X1,X2,X3)),skolemize(X6,sK16(X0,X1,X2,X3))],[f275]) ).
tff(f281,plain,
! [X0: $int,X1: map_int_int,X2: $int] :
( ~ $less(X2,X0)
| ( sum2(X1,X2,X0) = $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),sum2(X1,$sum(X2,1),X0)) ) ),
inference(rectify,[],[f221]) ).
tff(f299,plain,
phase11(sK6,sK5,tb2t2(mk_array1(int,sK2,t2tb1(sK3))),tb2t2(mk_array1(int,sK4,t2tb1(sK1)))),
inference(cnf_transformation,[],[f244]) ).
tff(f302,plain,
sum2(sK3,$sum($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),1),$sum(sK6,1)) != tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))),
inference(cnf_transformation,[],[f244]) ).
tff(f315,plain,
! [X2: $int,X0: map_int_int,X1: $int] :
( ( 0 = sum2(X0,X2,X1) )
| $less(X2,X1) ),
inference(cnf_transformation,[],[f247]) ).
tff(f323,plain,
! [X2: $int,X0: array_int,X1: $int] : ( sum3(X0,X1,X2) = sum2(tb2t1(elts(int,t2tb2(X0))),X1,X2) ),
inference(cnf_transformation,[],[f252]) ).
tff(f344,plain,
! [X2: uni,X0: ty,X1: $int] : ( get(X0,int,elts(X0,X2),t2tb(X1)) = get2(X0,X2,X1) ),
inference(cnf_transformation,[],[f264]) ).
tff(f346,plain,
! [X0: map_int_int] : sort1(map(int,int),t2tb1(X0)),
inference(cnf_transformation,[],[f54]) ).
tff(f352,plain,
! [X2: uni,X0: ty,X1: $int] :
( ~ sort1(map(int,X0),X2)
| ( elts(X0,mk_array1(X0,X1,X2)) = X2 ) ),
inference(cnf_transformation,[],[f269]) ).
tff(f362,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sK11(X0,X1,X2,X3) = X3 ) ),
inference(cnf_transformation,[],[f274]) ).
tff(f364,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sK12(X0,X1,X2,X3) = X2 ) ),
inference(cnf_transformation,[],[f274]) ).
tff(f365,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ( sum3(sK10(X0,X1,X2,X3),$sum($sum(sK12(X0,X1,X2,X3),$uminus($sum(sK11(X0,X1,X2,X3),$uminus(sK12(X0,X1,X2,X3))))),1),$sum(sK12(X0,X1,X2,X3),1)) = tb2t(get2(int,t2tb2(sK13(X0,X1,X2,X3)),sK12(X0,X1,X2,X3))) )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f274]) ).
tff(f366,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sK10(X0,X1,X2,X3) = X1 ) ),
inference(cnf_transformation,[],[f274]) ).
tff(f369,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sK13(X0,X1,X2,X3) = X0 ) ),
inference(cnf_transformation,[],[f274]) ).
tff(f370,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ( sK15(X0,X1,X2,X3) = X3 ) ),
inference(cnf_transformation,[],[f276]) ).
tff(f371,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| ( sK14(X0,X1,X2,X3) = X1 )
| sP0(X2,X3,X1,X0) ),
inference(cnf_transformation,[],[f276]) ).
tff(f372,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ( tb2t(get2(int,t2tb2(sK15(X0,X1,X2,X3)),sK14(X0,X1,X2,X3))) = tb2t(get2(int,t2tb2(sK16(X0,X1,X2,X3)),sK14(X0,X1,X2,X3))) ) ),
inference(cnf_transformation,[],[f276]) ).
tff(f373,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| ( sK16(X0,X1,X2,X3) = X2 )
| sP0(X2,X3,X1,X0) ),
inference(cnf_transformation,[],[f276]) ).
tff(f374,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ( $sum(sK14(X0,X1,X2,X3),1) = X0 ) ),
inference(cnf_transformation,[],[f276]) ).
tff(f378,plain,
! [X0: map_int_int] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f55]) ).
tff(f386,plain,
! [X2: $int,X0: $int,X1: map_int_int] :
( ~ $less(X2,X0)
| ( sum2(X1,X2,X0) = $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),sum2(X1,$sum(X2,1),X0)) ) ),
inference(cnf_transformation,[],[f281]) ).
tff(f398,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f63]) ).
tff(f410,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sum2(tb2t1(elts(int,t2tb2(sK10(X0,X1,X2,X3)))),$sum($sum(sK12(X0,X1,X2,X3),$uminus($sum(sK11(X0,X1,X2,X3),$uminus(sK12(X0,X1,X2,X3))))),1),$sum(sK12(X0,X1,X2,X3),1)) = tb2t(get(int,int,elts(int,t2tb2(sK13(X0,X1,X2,X3))),t2tb(sK12(X0,X1,X2,X3)))) ) ),
inference(definition_unfolding,[],[f365,f323,f344]) ).
tff(f411,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| ( tb2t(get(int,int,elts(int,t2tb2(sK15(X0,X1,X2,X3))),t2tb(sK14(X0,X1,X2,X3)))) = tb2t(get(int,int,elts(int,t2tb2(sK16(X0,X1,X2,X3))),t2tb(sK14(X0,X1,X2,X3)))) )
| sP0(X2,X3,X1,X0) ),
inference(definition_unfolding,[],[f372,f344,f344]) ).
tff(f428,plain,
! [X2: $int,X0: map_int_int,X1: $int] :
( $less(0,$sum(X1,$uminus(X2)))
| ( 0 = sum2(X0,X2,X1) ) ),
inference(evaluation,[],[f315]) ).
tff(f431,plain,
! [X2: $int,X0: $int,X1: map_int_int] :
( $less(0,$sum($sum(X2,1),$uminus(X0)))
| ( sum2(X1,X2,X0) = $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X2))),sum2(X1,$sum(X2,1),X0)) ) ),
inference(evaluation,[],[f386]) ).
tff(f471,plain,
! [X2: array_int,X3: array_int,X0: $int,X1: $int] :
( ~ phase11(X1,X0,X3,X2)
| sP0(X2,X3,X1,X0)
| ( $sum(1,sK14(X0,X1,X2,X3)) = X0 ) ),
inference(forward_demodulation,[],[f374,f111]) ).
tff(f474,plain,
sum2(sK3,$sum($sum(sK6,$uminus($sum(sK5,$uminus(sK6)))),1),$sum(1,sK6)) != tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))),
inference(forward_demodulation,[],[f302,f111]) ).
tff(f475,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ( sum2(tb2t1(elts(int,t2tb2(sK10(X0,X1,X2,X3)))),$sum($sum(sK12(X0,X1,X2,X3),$uminus($sum(sK11(X0,X1,X2,X3),$uminus(sK12(X0,X1,X2,X3))))),1),$sum(1,sK12(X0,X1,X2,X3))) = tb2t(get(int,int,elts(int,t2tb2(sK13(X0,X1,X2,X3))),t2tb(sK12(X0,X1,X2,X3)))) )
| ~ sP0(X0,X1,X2,X3) ),
inference(forward_demodulation,[],[f410,f111]) ).
tff(f476,plain,
tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) != sum2(sK3,$sum(1,$sum(sK6,$uminus($sum(sK5,$uminus(sK6))))),$sum(1,sK6)),
inference(forward_demodulation,[],[f474,f111]) ).
tff(f477,plain,
! [X2: $int,X3: $int,X0: array_int,X1: array_int] :
( ~ sP0(X0,X1,X2,X3)
| ( sum2(tb2t1(elts(int,t2tb2(sK10(X0,X1,X2,X3)))),$sum(1,$sum(sK12(X0,X1,X2,X3),$uminus($sum(sK11(X0,X1,X2,X3),$uminus(sK12(X0,X1,X2,X3)))))),$sum(1,sK12(X0,X1,X2,X3))) = tb2t(get(int,int,elts(int,t2tb2(sK13(X0,X1,X2,X3))),t2tb(sK12(X0,X1,X2,X3)))) ) ),
inference(forward_demodulation,[],[f475,f111]) ).
tff(f626,plain,
! [X0: $int,X1: $int] : ( $uminus($sum(X1,$uminus(X0))) = $sum(X0,$uminus(X1)) ),
inference(superposition,[],[f114,f121]) ).
tff(f746,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0)) ),
inference(superposition,[],[f112,f111]) ).
tff(f822,plain,
! [X0: $int,X1: map_int_int] :
( ( 0 = sum2(X1,X0,X0) )
| $less(0,0) ),
inference(superposition,[],[f428,f115]) ).
tff(f828,plain,
! [X0: $int,X1: map_int_int] : ( 0 = sum2(X1,X0,X0) ),
inference(evaluation,[],[f822]) ).
tff(f873,plain,
! [X0: $int,X1: map_int_int] : ( t2tb1(X1) = elts(int,mk_array1(int,X0,t2tb1(X1))) ),
inference(resolution,[],[f352,f346]) ).
tff(f1055,plain,
( sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)
| ( tb2t2(mk_array1(int,sK2,t2tb1(sK3))) = sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) ) ),
inference(resolution,[],[f370,f299]) ).
tff(f1057,definition,
( spl18_3
<=> ( tb2t2(mk_array1(int,sK2,t2tb1(sK3))) = sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) ) ),
introduced(definition,[new_symbols(definition,[spl18_3])],[avatar_definition]) ).
tff(f1059,plain,
( ( tb2t2(mk_array1(int,sK2,t2tb1(sK3))) = sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) )
| ~ spl18_3 ),
inference(avatar_component_clause,[],[f1057]) ).
tff(f1061,definition,
( spl18_4
<=> sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl18_4])],[avatar_definition]) ).
tff(f1062,plain,
( ~ sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)
| spl18_4 ),
inference(avatar_component_clause,[],[f1061]) ).
tff(f1063,plain,
( sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)
| ~ spl18_4 ),
inference(avatar_component_clause,[],[f1061]) ).
tff(f1064,plain,
( spl18_3
| spl18_4 ),
inference(avatar_split_clause,[],[f1055,f1061,f1057]) ).
tff(f1067,plain,
( ( sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) = sK6 )
| sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) ),
inference(resolution,[],[f371,f299]) ).
tff(f1069,definition,
( spl18_5
<=> ( sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl18_5])],[avatar_definition]) ).
tff(f1071,plain,
( ( sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) = sK6 )
| ~ spl18_5 ),
inference(avatar_component_clause,[],[f1069]) ).
tff(f1072,plain,
( spl18_5
| spl18_4 ),
inference(avatar_split_clause,[],[f1067,f1061,f1069]) ).
tff(f1082,plain,
( sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)
| ( tb2t2(mk_array1(int,sK4,t2tb1(sK1))) = sK16(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) ) ),
inference(resolution,[],[f373,f299]) ).
tff(f1256,plain,
( ( sK5 = $sum(1,sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))) )
| sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) ),
inference(resolution,[],[f471,f299]) ).
tff(f1471,plain,
! [X0: $int,X1: map_int_int] :
( ( $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X0))),sum2(X1,$sum(X0,1),$sum(X0,1))) = sum2(X1,X0,$sum(X0,1)) )
| $less(0,0) ),
inference(superposition,[],[f431,f115]) ).
tff(f1474,plain,
! [X0: $int,X1: map_int_int] : ( $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X0))),sum2(X1,$sum(X0,1),$sum(X0,1))) = sum2(X1,X0,$sum(X0,1)) ),
inference(evaluation,[],[f1471]) ).
tff(f1476,plain,
! [X0: $int,X1: map_int_int] : ( sum2(X1,X0,$sum(X0,1)) = $sum(tb2t(get(int,int,t2tb1(X1),t2tb(X0))),0) ),
inference(forward_demodulation,[],[f1474,f828]) ).
tff(f1477,plain,
! [X0: $int,X1: map_int_int] : ( tb2t(get(int,int,t2tb1(X1),t2tb(X0))) = sum2(X1,X0,$sum(X0,1)) ),
inference(evaluation,[],[f1476]) ).
tff(f1556,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))))) = tb2t(get(int,int,elts(int,t2tb2(sK16(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))))) )
| sP0(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) ),
inference(resolution,[],[f411,f299]) ).
tff(f1709,plain,
( ( sum2(tb2t1(elts(int,t2tb2(sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))),$sum(1,$sum(sK12(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5),$uminus($sum(sK11(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5),$uminus(sK12(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))))),$sum(1,sK12(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))) = tb2t(get(int,int,elts(int,t2tb2(sK13(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))),t2tb(sK12(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))) )
| ~ spl18_4 ),
inference(resolution,[],[f1063,f477]) ).
tff(f1711,plain,
( ( sK13(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) = tb2t2(mk_array1(int,sK4,t2tb1(sK1))) )
| ~ spl18_4 ),
inference(resolution,[],[f1063,f369]) ).
tff(f1712,plain,
( ( sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) = tb2t2(mk_array1(int,sK2,t2tb1(sK3))) )
| ~ spl18_4 ),
inference(resolution,[],[f1063,f366]) ).
tff(f1713,plain,
( ( sK12(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) = sK6 )
| ~ spl18_4 ),
inference(resolution,[],[f1063,f364]) ).
tff(f1714,plain,
( ( sK5 = sK11(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5) )
| ~ spl18_4 ),
inference(resolution,[],[f1063,f362]) ).
tff(f1715,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sK13(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))),t2tb(sK6))) = sum2(tb2t1(elts(int,t2tb2(sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))),$sum(1,$sum(sK6,$uminus($sum(sK11(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5),$uminus(sK6))))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1709,f1713]) ).
tff(f1716,plain,
( ( sum2(tb2t1(elts(int,t2tb2(sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK11(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))))),$sum(1,sK6)) = tb2t(get(int,int,elts(int,t2tb2(sK13(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))),t2tb(sK6))) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1715,f626]) ).
tff(f1717,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(tb2t1(elts(int,t2tb2(sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK11(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5))))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1716,f1711]) ).
tff(f1718,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(tb2t1(elts(int,t2tb2(sK10(tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))),sK6,sK5)))),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1717,f1714]) ).
tff(f1719,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(tb2t1(elts(int,t2tb2(tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1718,f1712]) ).
tff(f1720,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(tb2t1(elts(int,mk_array1(int,sK2,t2tb1(sK3)))),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1719,f398]) ).
tff(f1721,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(tb2t1(t2tb1(sK3)),$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1720,f873]) ).
tff(f1722,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1721,f378]) ).
tff(f1723,plain,
( ( sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) = tb2t(get(int,int,elts(int,mk_array1(int,sK4,t2tb1(sK1))),t2tb(sK6))) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1722,f398]) ).
tff(f1724,plain,
( ( sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) = tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1723,f873]) ).
tff(f1725,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) = sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1724,f1477]) ).
tff(f1726,plain,
( ( sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) = sum2(sK1,sK6,$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f1725,f111]) ).
tff(f2047,plain,
sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)) != tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))),
inference(superposition,[],[f476,f626]) ).
tff(f2134,plain,
sum2(sK1,sK6,$sum(sK6,1)) != sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),$sum(1,sK6)),
inference(forward_demodulation,[],[f2047,f1477]) ).
tff(f2143,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) != sum2(sK1,sK6,$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f2134,f1726]) ).
tff(f2148,plain,
( ( sum2(sK1,sK6,$sum(1,sK6)) != sum2(sK1,sK6,$sum(1,sK6)) )
| ~ spl18_4 ),
inference(forward_demodulation,[],[f2143,f111]) ).
tff(f2149,plain,
( $false
| ~ spl18_4 ),
inference(trivial_inequality_removal,[],[f2148]) ).
tff(f2150,plain,
~ spl18_4,
inference(avatar_contradiction_clause,[],[f2149]) ).
tff(f2155,definition,
( spl18_12
<=> ( sK5 = $sum(1,sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))) ) ),
introduced(definition,[new_symbols(definition,[spl18_12])],[avatar_definition]) ).
tff(f2157,plain,
( ( sK5 = $sum(1,sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))) )
| ~ spl18_12 ),
inference(avatar_component_clause,[],[f2155]) ).
tff(f2158,plain,
( spl18_12
| spl18_4 ),
inference(avatar_split_clause,[],[f1256,f1061,f2155]) ).
tff(f2160,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))))) = tb2t(get(int,int,elts(int,t2tb2(sK16(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK14(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3))))))) )
| spl18_4 ),
inference(forward_subsumption_resolution,[],[f1556,f1062]) ).
tff(f2161,plain,
( ( tb2t2(mk_array1(int,sK4,t2tb1(sK1))) = sK16(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))) )
| spl18_4 ),
inference(forward_subsumption_resolution,[],[f1082,f1062]) ).
tff(f2162,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK6))) = tb2t(get(int,int,elts(int,t2tb2(sK16(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK6))) )
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2160,f1071]) ).
tff(f2163,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = tb2t(get(int,int,elts(int,t2tb2(sK15(sK5,sK6,tb2t2(mk_array1(int,sK4,t2tb1(sK1))),tb2t2(mk_array1(int,sK2,t2tb1(sK3)))))),t2tb(sK6))) )
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2162,f2161]) ).
tff(f2164,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK2,t2tb1(sK3))))),t2tb(sK6))) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2163,f1059]) ).
tff(f2165,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = tb2t(get(int,int,elts(int,mk_array1(int,sK2,t2tb1(sK3))),t2tb(sK6))) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2164,f398]) ).
tff(f2166,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = tb2t(get(int,int,t2tb1(sK3),t2tb(sK6))) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2165,f873]) ).
tff(f2167,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(sK3,sK6,$sum(sK6,1)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2166,f1477]) ).
tff(f2168,plain,
( ( tb2t(get(int,int,elts(int,t2tb2(tb2t2(mk_array1(int,sK4,t2tb1(sK1))))),t2tb(sK6))) = sum2(sK3,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2167,f111]) ).
tff(f2169,plain,
( ( tb2t(get(int,int,elts(int,mk_array1(int,sK4,t2tb1(sK1))),t2tb(sK6))) = sum2(sK3,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2168,f398]) ).
tff(f2170,plain,
( ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) = sum2(sK3,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2169,f873]) ).
tff(f2171,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) = sum2(sK3,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2170,f1477]) ).
tff(f2172,plain,
( ( sum2(sK3,sK6,$sum(1,sK6)) = sum2(sK1,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5 ),
inference(forward_demodulation,[],[f2171,f111]) ).
tff(f2173,plain,
( ( sK5 = $sum(1,sK6) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2157,f1071]) ).
tff(f2178,plain,
( ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) != sum2(sK3,$sum(1,$sum(sK6,$uminus($sum(sK5,$uminus(sK6))))),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(superposition,[],[f476,f2173]) ).
tff(f2179,plain,
( ! [X0: $int] : ( $sum(1,$sum(sK6,X0)) = $sum(sK5,X0) )
| ~ spl18_5
| ~ spl18_12 ),
inference(superposition,[],[f112,f2173]) ).
tff(f2184,plain,
( ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) != sum2(sK3,$sum(1,$sum(sK6,$sum(sK6,$uminus(sK5)))),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2178,f626]) ).
tff(f2185,plain,
( ( tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) != sum2(sK3,$sum(sK5,$sum(sK6,$uminus(sK5))),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2184,f2179]) ).
tff(f2186,plain,
( ( sum2(sK3,$sum(sK6,$sum($uminus(sK5),sK5)),sK5) != tb2t(get(int,int,t2tb1(sK1),t2tb(sK6))) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2185,f746]) ).
tff(f2187,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) != sum2(sK3,$sum(sK6,$sum($uminus(sK5),sK5)),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2186,f1477]) ).
tff(f2188,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) != sum2(sK3,$sum(sK6,$sum(sK5,$uminus(sK5))),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2187,f111]) ).
tff(f2189,plain,
( ( sum2(sK1,sK6,$sum(sK6,1)) != sum2(sK3,$sum(sK6,0),sK5) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2188,f115]) ).
tff(f2190,plain,
( ( sum2(sK3,sK6,sK5) != sum2(sK1,sK6,$sum(sK6,1)) )
| ~ spl18_5
| ~ spl18_12 ),
inference(evaluation,[],[f2189]) ).
tff(f2191,plain,
( ( sum2(sK3,sK6,sK5) != sum2(sK1,sK6,$sum(1,sK6)) )
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2190,f111]) ).
tff(f2192,plain,
( ( sum2(sK3,sK6,sK5) != sum2(sK3,sK6,$sum(1,sK6)) )
| ~ spl18_3
| spl18_4
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2191,f2172]) ).
tff(f2193,plain,
( ( sum2(sK3,sK6,sK5) != sum2(sK3,sK6,sK5) )
| ~ spl18_3
| spl18_4
| ~ spl18_5
| ~ spl18_12 ),
inference(forward_demodulation,[],[f2192,f2173]) ).
tff(f2194,plain,
( $false
| ~ spl18_3
| spl18_4
| ~ spl18_5
| ~ spl18_12 ),
inference(trivial_inequality_removal,[],[f2193]) ).
tff(f2195,plain,
( ~ spl18_3
| spl18_4
| ~ spl18_5
| ~ spl18_12 ),
inference(avatar_contradiction_clause,[],[f2194]) ).
cnf(s2,plain,
( spl18_3
| spl18_4 ),
inference(sat_conversion,[],[f1064]) ).
cnf(s3,plain,
( spl18_4
| spl18_5 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s7,plain,
~ spl18_4,
inference(sat_conversion,[],[f2150]) ).
cnf(s8,plain,
( spl18_4
| spl18_12 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s9,plain,
( ~ spl18_3
| spl18_4
| ~ spl18_5
| ~ spl18_12 ),
inference(sat_conversion,[],[f2195]) ).
cnf(s10,plain,
spl18_12,
inference(rat,[],[s8,s7]) ).
cnf(s11,plain,
spl18_5,
inference(rat,[],[s3,s7]) ).
cnf(s12,plain,
~ spl18_3,
inference(rat,[],[s9,s10,s7,s11]) ).
cnf(s13,plain,
$false,
inference(rat,[],[s2,s7,s12]) ).
tff(f2196,plain,
$false,
inference(avatar_sat_refutation,[],[s13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW664_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 % Computer : n014.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 14:24:30 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.32 Running first-order theorem proving
% 0.24/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.29/1.81 % (1809696)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.29/1.81 % (1809708)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1213729116:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.29/1.81 % (1809712)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=498876802:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.29/1.81 % (1809706)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2143412770:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.29/1.81 % (1809710)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2799492489:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.29/1.81 % (1809709)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=691551326:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.29/1.81 % (1809712)Instruction limit reached!
% 5.29/1.81 % (1809712)------------------------------
% 5.29/1.81 % (1809712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.81 % (1809712)CaDiCaL version: 2.1.3
% 5.29/1.81 % (1809712)Termination reason: Instruction limit
% 5.29/1.81 % (1809712)Termination phase: Saturation
% 5.29/1.81 % (1809712)Time elapsed: 0.068 s
% 5.29/1.81 % (1809712)Peak memory usage: 116 MB
% 5.29/1.81 % (1809712)Instructions burned: 33 (million)
% 5.29/1.81 % (1809710)Instruction limit reached!
% 5.29/1.81 % (1809710)------------------------------
% 5.29/1.81 % (1809710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.81 % (1809710)CaDiCaL version: 2.1.3
% 5.29/1.81 % (1809710)Termination reason: Instruction limit
% 5.29/1.81 % (1809710)Termination phase: Preprocessing 3
% 5.29/1.81 % (1809710)Time elapsed: 0.006 s
% 5.29/1.81 % (1809710)Peak memory usage: 86 MB
% 5.29/1.81 % (1809710)Instructions burned: 5 (million)
% 5.29/1.81 % (1809709)Instruction limit reached!
% 5.29/1.81 % (1809709)------------------------------
% 5.29/1.81 % (1809709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.81 % (1809709)CaDiCaL version: 2.1.3
% 5.29/1.81 % (1809709)Termination reason: Instruction limit
% 5.29/1.81 % (1809709)Termination phase: Saturation
% 5.29/1.81 % (1809709)Time elapsed: 0.008 s
% 5.29/1.81 % (1809709)Peak memory usage: 87 MB
% 5.29/1.81 % (1809709)Instructions burned: 7 (million)
% 5.29/1.81 % (1809711)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1521958248:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.29/1.81 % (1809706)Instruction limit reached!
% 5.29/1.81 % (1809706)------------------------------
% 5.29/1.81 % (1809706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.81 % (1809706)CaDiCaL version: 2.1.3
% 5.29/1.81 % (1809706)Termination reason: Instruction limit
% 5.29/1.81 % (1809706)Termination phase: Saturation
% 5.29/1.81 % (1809706)Time elapsed: 0.040 s
% 5.29/1.81 % (1809706)Peak memory usage: 111 MB
% 5.29/1.81 % (1809706)Instructions burned: 12 (million)
% 5.29/1.81 % (1809708)Instruction limit reached!
% 5.29/1.81 % (1809708)------------------------------
% 5.29/1.81 % (1809708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.81 % (1809708)CaDiCaL version: 2.1.3
% 5.29/1.81 % (1809708)Termination reason: Instruction limit
% 5.29/1.81 % (1809708)Termination phase: Saturation
% 5.29/1.81 % (1809708)Time elapsed: 0.119 s
% 5.29/1.81 % (1809708)Peak memory usage: 119 MB
% 5.29/1.81 % (1809708)Instructions burned: 201 (million)
% 5.29/1.81 % (1809707)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=722882655:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.29/1.81 % (1809711)Instruction limit reached!
% 5.29/1.81 % (1809711)------------------------------
% 5.29/1.81 % (1809711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.81 % (1809711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809711)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809711)Termination reason: Instruction limit
% 6.83/1.98 % (1809711)Termination phase: Saturation
% 6.83/1.98 % (1809711)Time elapsed: 0.084 s
% 6.83/1.98 % (1809711)Peak memory usage: 116 MB
% 6.83/1.98 % (1809711)Instructions burned: 46 (million)
% 6.83/1.98 % (1809725)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=1456382456:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.83/1.98 % (1809721)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=95029444:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.83/1.98 % (1809720)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=2822664465:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.83/1.98 % (1809719)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3474734933:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.83/1.98 % (1809725)Instruction limit reached!
% 6.83/1.98 % (1809725)------------------------------
% 6.83/1.98 % (1809725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.83/1.98 % (1809725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809725)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809725)Termination reason: Instruction limit
% 6.83/1.98 % (1809725)Termination phase: Saturation
% 6.83/1.98 % (1809725)Time elapsed: 0.018 s
% 6.83/1.98 % (1809725)Peak memory usage: 89 MB
% 6.83/1.98 % (1809725)Instructions burned: 27 (million)
% 6.83/1.98 % (1809719)Instruction limit reached!
% 6.83/1.98 % (1809719)------------------------------
% 6.83/1.98 % (1809719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.83/1.98 % (1809719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809719)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809719)Termination reason: Instruction limit
% 6.83/1.98 % (1809719)Termination phase: Saturation
% 6.83/1.98 % (1809719)Time elapsed: 0.016 s
% 6.83/1.98 % (1809719)Peak memory usage: 88 MB
% 6.83/1.98 % (1809719)Instructions burned: 14 (million)
% 6.83/1.98 % (1809721)Instruction limit reached!
% 6.83/1.98 % (1809721)------------------------------
% 6.83/1.98 % (1809721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.83/1.98 % (1809721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809721)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809721)Termination reason: Instruction limit
% 6.83/1.98 % (1809721)Termination phase: Saturation
% 6.83/1.98 % (1809721)Time elapsed: 0.016 s
% 6.83/1.98 % (1809721)Peak memory usage: 89 MB
% 6.83/1.98 % (1809721)Instructions burned: 16 (million)
% 6.83/1.98 % (1809720)Instruction limit reached!
% 6.83/1.98 % (1809720)------------------------------
% 6.83/1.98 % (1809720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.83/1.98 % (1809720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809720)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809720)Termination reason: Instruction limit
% 6.83/1.98 % (1809720)Termination phase: Saturation
% 6.83/1.98 % (1809720)Time elapsed: 0.034 s
% 6.83/1.98 % (1809720)Peak memory usage: 89 MB
% 6.83/1.98 % (1809720)Instructions burned: 29 (million)
% 6.83/1.98 % (1809724)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1741141367:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.83/1.98 % (1809727)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2622046135:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.83/1.98 % (1809724)Instruction limit reached!
% 6.83/1.98 % (1809724)------------------------------
% 6.83/1.98 % (1809724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.83/1.98 % (1809724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.83/1.98 % (1809724)CaDiCaL version: 2.1.3
% 6.83/1.98 % (1809724)Termination reason: Instruction limit
% 6.83/1.98 % (1809724)Termination phase: Saturation
% 6.83/1.98 % (1809724)Time elapsed: 0.028 s
% 6.83/1.98 % (1809724)Peak memory usage: 89 MB
% 6.83/1.98 % (1809724)Instructions burned: 24 (million)
% 6.83/1.98 % (1809727)Instruction limit reached!
% 6.83/1.98 % (1809727)------------------------------
% 6.83/1.98 % (1809727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.20 % (1809727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.20 % (1809727)CaDiCaL version: 2.1.3
% 9.36/2.20 % (1809727)Termination reason: Instruction limit
% 9.36/2.20 % (1809727)Termination phase: Saturation
% 9.36/2.20 % (1809727)Time elapsed: 0.039 s
% 9.36/2.20 % (1809727)Peak memory usage: 89 MB
% 9.36/2.20 % (1809727)Instructions burned: 87 (million)
% 9.36/2.20 % (1809707)Instruction limit reached!
% 9.36/2.20 % (1809707)------------------------------
% 9.36/2.20 % (1809707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.20 % (1809707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.20 % (1809707)CaDiCaL version: 2.1.3
% 9.36/2.20 % (1809707)Termination reason: Instruction limit
% 9.36/2.20 % (1809707)Termination phase: Saturation
% 9.36/2.20 % (1809707)Time elapsed: 0.366 s
% 9.36/2.20 % (1809707)Peak memory usage: 118 MB
% 9.36/2.20 % (1809707)Instructions burned: 307 (million)
% 9.36/2.20 % (1809732)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1067279870:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.36/2.21 % (1809732)Instruction limit reached!
% 9.36/2.21 % (1809732)------------------------------
% 9.36/2.21 % (1809732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.21 % (1809732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.21 % (1809732)CaDiCaL version: 2.1.3
% 9.36/2.21 % (1809732)Termination reason: Instruction limit
% 9.36/2.21 % (1809732)Termination phase: Preprocessing 1
% 9.36/2.21 % (1809732)Time elapsed: 0.003 s
% 9.36/2.21 % (1809732)Peak memory usage: 85 MB
% 9.36/2.21 % (1809732)Instructions burned: 2 (million)
% 9.36/2.21 % (1809734)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2869266571:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.36/2.21 % (1809733)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2219633737:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.36/2.21 % (1809734)Instruction limit reached!
% 9.36/2.21 % (1809734)------------------------------
% 9.36/2.21 % (1809734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.21 % (1809734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.21 % (1809734)CaDiCaL version: 2.1.3
% 9.36/2.21 % (1809734)Termination reason: Instruction limit
% 9.36/2.21 % (1809734)Termination phase: Preprocessing 3
% 9.36/2.21 % (1809734)Time elapsed: 0.005 s
% 9.36/2.21 % (1809734)Peak memory usage: 86 MB
% 9.36/2.21 % (1809734)Instructions burned: 5 (million)
% 9.36/2.21 % (1809739)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=2579133645:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 9.36/2.21 % (1809735)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2244043118:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.36/2.21 % (1809739)Instruction limit reached!
% 9.36/2.21 % (1809739)------------------------------
% 9.36/2.21 % (1809739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.21 % (1809739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.21 % (1809739)CaDiCaL version: 2.1.3
% 9.36/2.21 % (1809739)Termination reason: Instruction limit
% 9.36/2.21 % (1809739)Termination phase: Property scanning
% 9.36/2.21 % (1809739)Time elapsed: 0.005 s
% 9.36/2.21 % (1809739)Peak memory usage: 86 MB
% 9.36/2.21 % (1809739)Instructions burned: 10 (million)
% 9.36/2.21 % (1809738)lrs+10_1_thi=all:si=on:fd=off:random_seed=2869526068:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.36/2.21 % (1809743)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1344271015:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 9.36/2.21 % (1809743)Instruction limit reached!
% 9.36/2.21 % (1809743)------------------------------
% 9.36/2.21 % (1809743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.36/2.21 % (1809743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.36/2.21 % (1809743)CaDiCaL version: 2.1.3
% 9.36/2.21 % (1809743)Termination reason: Instruction limit
% 9.36/2.21 % (1809743)Termination phase: Naming
% 10.75/2.61 % (1809743)Time elapsed: 0.002 s
% 10.75/2.61 % (1809743)Peak memory usage: 86 MB
% 10.75/2.61 % (1809743)Instructions burned: 3 (million)
% 10.75/2.61 % (1809741)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3453024790:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 10.75/2.61 % (1809741)Instruction limit reached!
% 10.75/2.61 % (1809741)------------------------------
% 10.75/2.61 % (1809741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809741)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809741)Termination reason: Instruction limit
% 10.75/2.61 % (1809741)Termination phase: SInE selection
% 10.75/2.61 % (1809741)Time elapsed: 0.002 s
% 10.75/2.61 % (1809741)Peak memory usage: 85 MB
% 10.75/2.61 % (1809741)Instructions burned: 2 (million)
% 10.75/2.61 % (1809735)Instruction limit reached!
% 10.75/2.61 % (1809735)------------------------------
% 10.75/2.61 % (1809735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809735)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809735)Termination reason: Instruction limit
% 10.75/2.61 % (1809735)Termination phase: Saturation
% 10.75/2.61 % (1809735)Time elapsed: 0.134 s
% 10.75/2.61 % (1809735)Peak memory usage: 134 MB
% 10.75/2.61 % (1809735)Instructions burned: 66 (million)
% 10.75/2.61 % (1809733)Instruction limit reached!
% 10.75/2.61 % (1809733)------------------------------
% 10.75/2.61 % (1809733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809733)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809733)Termination reason: Instruction limit
% 10.75/2.61 % (1809733)Termination phase: Saturation
% 10.75/2.61 % (1809733)Time elapsed: 0.187 s
% 10.75/2.61 % (1809733)Peak memory usage: 91 MB
% 10.75/2.61 % (1809733)Instructions burned: 181 (million)
% 10.75/2.61 % (1809738)Instruction limit reached!
% 10.75/2.61 % (1809738)------------------------------
% 10.75/2.61 % (1809738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809738)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809738)Termination reason: Instruction limit
% 10.75/2.61 % (1809738)Termination phase: Saturation
% 10.75/2.61 % (1809738)Time elapsed: 0.091 s
% 10.75/2.61 % (1809738)Peak memory usage: 116 MB
% 10.75/2.61 % (1809738)Instructions burned: 53 (million)
% 10.75/2.61 % (1809746)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2909011153:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 10.75/2.61 % (1809749)dis+10_1_si=on:random_seed=3927491526:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.75/2.61 % (1809749)Instruction limit reached!
% 10.75/2.61 % (1809749)------------------------------
% 10.75/2.61 % (1809749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809749)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809749)Termination reason: Instruction limit
% 10.75/2.61 % (1809749)Termination phase: Saturation
% 10.75/2.61 % (1809749)Time elapsed: 0.010 s
% 10.75/2.61 % (1809749)Peak memory usage: 88 MB
% 10.75/2.61 % (1809749)Instructions burned: 10 (million)
% 10.75/2.61 % (1809754)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2878353867: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_2990 on theBenchmark for (2990ds/35Mi)
% 10.75/2.61 % (1809753)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3680811101:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 10.75/2.61 % (1809754)Instruction limit reached!
% 10.75/2.61 % (1809754)------------------------------
% 10.75/2.61 % (1809754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.61 % (1809754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.61 % (1809754)CaDiCaL version: 2.1.3
% 10.75/2.61 % (1809754)Termination reason: Instruction limit
% 10.75/2.61 % (1809754)Termination phase: Saturation
% 10.75/2.61 % (1809754)Time elapsed: 0.021 s
% 10.75/2.61 % (1809754)Peak memory usage: 89 MB
% 10.75/2.61 % (1809754)Instructions burned: 36 (million)
% 12.67/3.08 % (1809753)Instruction limit reached!
% 12.67/3.08 % (1809753)------------------------------
% 12.67/3.08 % (1809753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809753)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809753)Termination reason: Instruction limit
% 12.67/3.08 % (1809753)Termination phase: Saturation
% 12.67/3.08 % (1809753)Time elapsed: 0.029 s
% 12.67/3.08 % (1809753)Peak memory usage: 89 MB
% 12.67/3.08 % (1809753)Instructions burned: 26 (million)
% 12.67/3.08 % (1809756)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3539583655:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 12.67/3.08 % (1809756)Instruction limit reached!
% 12.67/3.08 % (1809756)------------------------------
% 12.67/3.08 % (1809756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809756)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809756)Termination reason: Instruction limit
% 12.67/3.08 % (1809756)Termination phase: Preprocessing 1
% 12.67/3.08 % (1809756)Time elapsed: 0.003 s
% 12.67/3.08 % (1809756)Peak memory usage: 85 MB
% 12.67/3.08 % (1809756)Instructions burned: 3 (million)
% 12.67/3.08 % (1809746)Instruction limit reached!
% 12.67/3.08 % (1809746)------------------------------
% 12.67/3.08 % (1809746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809746)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809746)Termination reason: Instruction limit
% 12.67/3.08 % (1809746)Termination phase: Saturation
% 12.67/3.08 % (1809746)Time elapsed: 0.174 s
% 12.67/3.08 % (1809746)Peak memory usage: 117 MB
% 12.67/3.08 % (1809746)Instructions burned: 127 (million)
% 12.67/3.08 % (1809757)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3931134221:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 12.67/3.08 % (1809758)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3213103815:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 12.67/3.08 % (1809757)Instruction limit reached!
% 12.67/3.08 % (1809757)------------------------------
% 12.67/3.08 % (1809757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809757)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809757)Termination reason: Instruction limit
% 12.67/3.08 % (1809757)Termination phase: Saturation
% 12.67/3.08 % (1809757)Time elapsed: 0.009 s
% 12.67/3.08 % (1809757)Peak memory usage: 87 MB
% 12.67/3.08 % (1809757)Instructions burned: 9 (million)
% 12.67/3.08 % (1809765)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1173448377:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi)
% 12.67/3.08 % (1809761)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3810858435:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 12.67/3.08 % (1809765)Instruction limit reached!
% 12.67/3.08 % (1809765)------------------------------
% 12.67/3.08 % (1809765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809765)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809765)Termination reason: Instruction limit
% 12.67/3.08 % (1809765)Termination phase: Saturation
% 12.67/3.08 % (1809765)Time elapsed: 0.007 s
% 12.67/3.08 % (1809765)Peak memory usage: 88 MB
% 12.67/3.08 % (1809765)Instructions burned: 11 (million)
% 12.67/3.08 % (1809761)Instruction limit reached!
% 12.67/3.08 % (1809761)------------------------------
% 12.67/3.08 % (1809761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/3.08 % (1809761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/3.08 % (1809764)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3296912252:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 12.67/3.08 % (1809761)CaDiCaL version: 2.1.3
% 12.67/3.08 % (1809761)Termination reason: Instruction limit
% 12.67/3.08 % (1809761)Termination phase: Saturation
% 12.67/3.08 % (1809761)Time elapsed: 0.038 s
% 12.67/3.08 % (1809761)Peak memory usage: 105 MB
% 17.17/3.50 % (1809761)Instructions burned: 13 (million)
% 17.17/3.50 % (1809767)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1761081290:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 17.17/3.50 % (1809767)Instruction limit reached!
% 17.17/3.50 % (1809767)------------------------------
% 17.17/3.50 % (1809767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809767)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809767)Termination reason: Instruction limit
% 17.17/3.50 % (1809767)Termination phase: Saturation
% 17.17/3.50 % (1809767)Time elapsed: 0.077 s
% 17.17/3.50 % (1809767)Peak memory usage: 133 MB
% 17.17/3.50 % (1809767)Instructions burned: 71 (million)
% 17.17/3.50 % (1809769)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=2721750371:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2988 on theBenchmark for (2988ds/75Mi)
% 17.17/3.50 % (1809771)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=1312734242:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 17.17/3.50 % (1809758)Instruction limit reached!
% 17.17/3.50 % (1809758)------------------------------
% 17.17/3.50 % (1809758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809758)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809758)Termination reason: Instruction limit
% 17.17/3.50 % (1809758)Termination phase: Saturation
% 17.17/3.50 % (1809758)Time elapsed: 0.317 s
% 17.17/3.50 % (1809758)Peak memory usage: 90 MB
% 17.17/3.50 % (1809758)Instructions burned: 371 (million)
% 17.17/3.50 % (1809769)Instruction limit reached!
% 17.17/3.50 % (1809769)------------------------------
% 17.17/3.50 % (1809769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809769)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809769)Termination reason: Instruction limit
% 17.17/3.50 % (1809769)Termination phase: Saturation
% 17.17/3.50 % (1809769)Time elapsed: 0.084 s
% 17.17/3.50 % (1809769)Peak memory usage: 90 MB
% 17.17/3.50 % (1809769)Instructions burned: 75 (million)
% 17.17/3.50 % (1809774)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1409404181:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/130Mi)
% 17.17/3.50 % (1809764)Instruction limit reached!
% 17.17/3.50 % (1809764)------------------------------
% 17.17/3.50 % (1809764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809764)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809764)Termination reason: Instruction limit
% 17.17/3.50 % (1809764)Termination phase: Saturation
% 17.17/3.50 % (1809764)Time elapsed: 0.261 s
% 17.17/3.50 % (1809764)Peak memory usage: 120 MB
% 17.17/3.50 % (1809764)Instructions burned: 226 (million)
% 17.17/3.50 % (1809776)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3648680566:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi)
% 17.17/3.50 % (1809778)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=93061242:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 17.17/3.50 % (1809778)Instruction limit reached!
% 17.17/3.50 % (1809778)------------------------------
% 17.17/3.50 % (1809778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809778)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809778)Termination reason: Instruction limit
% 17.17/3.50 % (1809778)Termination phase: Saturation
% 17.17/3.50 % (1809778)Time elapsed: 0.056 s
% 17.17/3.50 % (1809778)Peak memory usage: 134 MB
% 17.17/3.50 % (1809778)Instructions burned: 41 (million)
% 17.17/3.50 % (1809782)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2202524904:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 17.17/3.50 % (1809774)Instruction limit reached!
% 17.17/3.50 % (1809774)------------------------------
% 17.17/3.50 % (1809774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809774)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809774)Termination reason: Instruction limit
% 17.17/3.50 % (1809774)Termination phase: Saturation
% 17.17/3.50 % (1809774)Time elapsed: 0.171 s
% 17.17/3.50 % (1809774)Peak memory usage: 117 MB
% 17.17/3.50 % (1809774)Instructions burned: 130 (million)
% 17.17/3.50 % (1809776)Instruction limit reached!
% 17.17/3.50 % (1809776)------------------------------
% 17.17/3.50 % (1809776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809776)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809776)Termination reason: Instruction limit
% 17.17/3.50 % (1809776)Termination phase: Saturation
% 17.17/3.50 % (1809776)Time elapsed: 0.202 s
% 17.17/3.50 % (1809776)Peak memory usage: 134 MB
% 17.17/3.50 % (1809776)Instructions burned: 131 (million)
% 17.17/3.50 % (1809771)Instruction limit reached!
% 17.17/3.50 % (1809771)------------------------------
% 17.17/3.50 % (1809771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809771)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809771)Termination reason: Instruction limit
% 17.17/3.50 % (1809771)Termination phase: Saturation
% 17.17/3.50 % (1809771)Time elapsed: 0.317 s
% 17.17/3.50 % (1809771)Peak memory usage: 92 MB
% 17.17/3.50 % (1809771)Instructions burned: 295 (million)
% 17.17/3.50 % (1809781)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1330101397:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 17.17/3.50 % (1809785)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4156239610:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi)
% 17.17/3.50 % (1809789)dis+10_1_si=on:random_seed=1496651991:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 17.17/3.50 % (1809787)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=349289790:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2983 on theBenchmark for (2983ds/259Mi)
% 17.17/3.50 % (1809785)Instruction limit reached!
% 17.17/3.50 % (1809785)------------------------------
% 17.17/3.50 % (1809785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809785)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809785)Termination reason: Instruction limit
% 17.17/3.50 % (1809785)Termination phase: Saturation
% 17.17/3.50 % (1809785)Time elapsed: 0.163 s
% 17.17/3.50 % (1809785)Peak memory usage: 117 MB
% 17.17/3.50 % (1809785)Instructions burned: 131 (million)
% 17.17/3.50 % (1809782)Instruction limit reached!
% 17.17/3.50 % (1809782)------------------------------
% 17.17/3.50 % (1809782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809782)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809782)Termination reason: Instruction limit
% 17.17/3.50 % (1809782)Termination phase: Saturation
% 17.17/3.50 % (1809782)Time elapsed: 0.357 s
% 17.17/3.50 % (1809782)Peak memory usage: 139 MB
% 17.17/3.50 % (1809782)Instructions burned: 598 (million)
% 17.17/3.50 % (1809792)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1877326598:i=141:doe=on:rtra=on_2982 on theBenchmark for (2982ds/141Mi)
% 17.17/3.50 % (1809791)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3864192649:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 17.17/3.50 % (1809781)Instruction limit reached!
% 17.17/3.50 % (1809781)------------------------------
% 17.17/3.50 % (1809781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809781)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809781)Termination reason: Instruction limit
% 17.17/3.50 % (1809781)Termination phase: Saturation
% 17.17/3.50 % (1809781)Time elapsed: 0.289 s
% 17.17/3.50 % (1809781)Peak memory usage: 93 MB
% 17.17/3.50 % (1809781)Instructions burned: 307 (million)
% 17.17/3.50 % (1809792)First to succeed.
% 17.17/3.50 % (1809792)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1809696"
% 17.17/3.50 % (1809796)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2305618298:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 17.17/3.50 % (1809799)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2430407276:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 17.17/3.50 % (1809787)Instruction limit reached!
% 17.17/3.50 % (1809787)------------------------------
% 17.17/3.50 % (1809787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809787)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809787)Termination reason: Instruction limit
% 17.17/3.50 % (1809787)Termination phase: Saturation
% 17.17/3.50 % (1809787)Time elapsed: 0.309 s
% 17.17/3.50 % (1809787)Peak memory usage: 117 MB
% 17.17/3.50 % (1809787)Instructions burned: 260 (million)
% 17.17/3.50 % (1809799)Instruction limit reached!
% 17.17/3.50 % (1809799)------------------------------
% 17.17/3.50 % (1809799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809799)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809799)Termination reason: Instruction limit
% 17.17/3.50 % (1809799)Termination phase: Saturation
% 17.17/3.50 % (1809799)Time elapsed: 0.065 s
% 17.17/3.50 % (1809799)Peak memory usage: 90 MB
% 17.17/3.50 % (1809799)Instructions burned: 121 (million)
% 17.17/3.50 % (1809796)Instruction limit reached!
% 17.17/3.50 % (1809796)------------------------------
% 17.17/3.50 % (1809796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809796)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809796)Termination reason: Instruction limit
% 17.17/3.50 % (1809796)Termination phase: Saturation
% 17.17/3.50 % (1809796)Time elapsed: 0.102 s
% 17.17/3.50 % (1809796)Peak memory usage: 116 MB
% 17.17/3.50 % (1809796)Instructions burned: 65 (million)
% 17.17/3.50 % (1809800)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=1394898961:s2a=on:i=128:s2at=5:ins=3:rtra=on_2979 on theBenchmark for (2979ds/128Mi)
% 17.17/3.50 % (1809791)Instruction limit reached!
% 17.17/3.50 % (1809791)------------------------------
% 17.17/3.50 % (1809791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809791)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809791)Termination reason: Instruction limit
% 17.17/3.50 % (1809791)Termination phase: Saturation
% 17.17/3.50 % (1809791)Time elapsed: 0.369 s
% 17.17/3.50 % (1809791)Peak memory usage: 93 MB
% 17.17/3.50 % (1809791)Instructions burned: 383 (million)
% 17.17/3.50 % (1809804)dis+1010_1_to=kbo:si=on:random_seed=1688800430:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi)
% 17.17/3.50 % (1809803)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=754545184:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi)
% 17.17/3.50 % (1809800)Instruction limit reached!
% 17.17/3.50 % (1809800)------------------------------
% 17.17/3.50 % (1809800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809800)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809800)Termination reason: Instruction limit
% 17.17/3.50 % (1809800)Termination phase: Saturation
% 17.17/3.50 % (1809800)Time elapsed: 0.165 s
% 17.17/3.50 % (1809800)Peak memory usage: 119 MB
% 17.17/3.50 % (1809800)Instructions burned: 128 (million)
% 17.17/3.50 % (1809803)Instruction limit reached!
% 17.17/3.50 % (1809803)------------------------------
% 17.17/3.50 % (1809803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.17/3.50 % (1809803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.17/3.50 % (1809803)CaDiCaL version: 2.1.3
% 17.17/3.50 % (1809803)Termination reason: Instruction limit
% 17.17/3.50 % (1809803)Termination phase: Saturation
% 17.17/3.50 % (1809803)Time elapsed: 0.074 s
% 17.17/3.50 % (1809803)Peak memory usage: 116 MB
% 17.17/3.50 % (1809803)Instructions burned: 39 (million)
% 17.17/3.50 % (1809792)Refutation found. Thanks to Tanya!
% 17.17/3.50 % SZS status Theorem for theBenchmark
% 17.17/3.50 % SZS output start Proof for theBenchmark
% See solution above
% 18.88/3.64 % (1809792)------------------------------
% 18.88/3.64 % (1809792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.64 % (1809792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.64 % (1809792)CaDiCaL version: 2.1.3
% 18.88/3.64 % (1809792)Termination reason: Refutation
% 18.88/3.64 % (1809792)Time elapsed: 0.132 s
% 18.88/3.64 % (1809792)Peak memory usage: 91 MB
% 18.88/3.64 % (1809792)Instructions burned: 125 (million)
% 18.88/3.64 % (1809792)------------------------------
% 18.88/3.64 % (1809792)------------------------------
% 18.88/3.64 % (1809696)Success in time 2.594 s
% 18.88/3.64 % Vampire exiting
%------------------------------------------------------------------------------