# Computing Termination of mapReduce.dbp

• Computing Termination of mapReduce.dbp
• ## Input

```//example from "Actors in Scala" chapter 9

//  def mapReduce[K, V, K2, V2](
//    input: List[(K, V)],
//    mapping: (K, V) => List[(K2, V2)],
//    reducing: (K2, List[V2]) => List[V2]
//  ): Map[K2, List[V2]] = {
//    case class Intermediate(list: List[(K2, V2)])
//    case class Reduced(key: K2, values: List[V2])
//    val master = self
//    val workers = for ((key, value) <- input) yield
//      actor {
//        master ! Intermediate(mapping(key, value))
//      }
//    var intermediates = List[(K2, V2)]()
//    for (_ <- 1 to input.length)
//        case Intermediate(list) => intermediates :::= list
//      }
//    var dict = Map[K2, List[V2]]() withDefault (k => List())
//    for ((key, value) <- intermediates)
//      dict += (key -> (value :: dict(key)))
//    val reducers = for ((key, values) <- dict) yield
//      actor {
//        master ! Reduced(key, reducing(key, values))
//      }
//    var result = Map[K2, List[V2]]()
//    for (_ <- 1 to dict.size)
//        case Reduced(key, values) =>
//          result += (key -> values)
//      }
//    result
//  }

init
(m, master) -> (i, input)*

transition "master: make mappers"
pre
(m, master) -> (i, input)
post
(m, master) -> (w, mapper)
(w, mapper) -> (i, input)
==>
m -> m
i -> i
<==

transition "master: mappers created"
pre
node (m, master)
post
node (m, master1)
==>
m -> m
<==
no
(m, master) -> (i, input)
==>
m -> m

transition "master: mapping done"
pre
node (m, master1)
post
node (m, master2)
==>
m -> m
<==
no
(m, master1) -> (w, mapper)
(w, mapper) -> (i, input)
==>
m -> m

transition "master: reducer"
pre
(m, master2) -> (k1, key) [inter]
post
(m, master2) -> (w, reducer)
(w, reducer) -> (k1, key)
(w, reducer) -> (v1, value)
==>
m -> m
k1 -> k1
<==

transition "master: reducers created"
pre
node (m, master2)
post
node (m, master3)
==>
m -> m
<==
no
(m, master2) -> (k, key) [inter]
==>
m -> m

transition "master: done"
pre
node (m, master3)
post
node (m, master4)
==>
m -> m
<==
no
(m, master3) -> (w, reducer)
(w, reducer) -> (k1, key)
==>
m -> m

transition "mapper"
pre
(m, _) -> (w, mapper)
(w, mapper) -> (i, input)
post
(m, _) -> (k, key)* [inter]
(k, key)* -> (v, value)**
==>
<==
m -> m

transition "reducer"
pre
(m, _) -> (w, reducer)
(w, reducer) -> (k1, key)
(w, reducer) -> (v1, value)
post
(m, _) -> (k2, key) [result]
(k2, key) -> (v1, value)
==>
k1 -> k2
v1 -> v1
<==
m -> m
no
(k1, key) -> (v2, value)
==>
k1 -> k1
```

## Numerical Abstraction

```% BEGIN FIXED PREAMBLE
cube_size/1,start/1,error/1,refinement/1,cutpoint/1,invgen_template/2,
invgen_template/1,cfg_exit_relation/1,stmtsrc/2,strengthening/2,globals/3,
bound_var/2,bounding_vars/2,transition_access/2,atomic/3.
refinement(inter).
cube_size(1).
% END FIXED PREAMBLE

var2names( p(_, data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)), [(Key_25, 'key\$25'), (Key_2, 'key\$2'), (Value_16, 'value\$16'), (Input_7, 'input\$7'), (Reducer_1, 'reducer\$1'), (Value_35, 'value\$35'), (Value_3, 'value\$3'), (Value_1, 'value\$1'), (Input_6, 'input\$6'), (Mapper_1, 'mapper\$1'), (Key_26, 'key\$26')]).

preds( p(_, data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)), []).

trans_preds(
p(_, data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(_, data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 = Key_25_prime,
0 =< Key_25_prime,
Key_25_prime < Key_25,
Key_25_prime = Key_25,
0 = Key_2_prime,
0 =< Key_2_prime,
Key_2_prime < Key_2,
Key_2_prime = Key_2,
0 = Value_16_prime,
0 =< Value_16_prime,
Value_16_prime < Value_16,
Value_16_prime = Value_16,
0 = Input_7_prime,
0 =< Input_7_prime,
Input_7_prime < Input_7,
Input_7_prime = Input_7,
0 = Reducer_1_prime,
0 =< Reducer_1_prime,
Reducer_1_prime < Reducer_1,
Reducer_1_prime = Reducer_1,
0 = Value_35_prime,
0 =< Value_35_prime,
Value_35_prime < Value_35,
Value_35_prime = Value_35,
0 = Value_3_prime,
0 =< Value_3_prime,
Value_3_prime < Value_3,
Value_3_prime = Value_3,
0 = Value_1_prime,
0 =< Value_1_prime,
Value_1_prime < Value_1,
Value_1_prime = Value_1,
0 = Input_6_prime,
0 =< Input_6_prime,
Input_6_prime < Input_6,
Input_6_prime = Input_6,
0 = Mapper_1_prime,
0 =< Mapper_1_prime,
Mapper_1_prime < Mapper_1,
Mapper_1_prime = Mapper_1,
0 = Key_26_prime,
0 =< Key_26_prime,
Key_26_prime < Key_26,
Key_26_prime = Key_26
]).

start( pc(s__36)).
cutpoint(pc(s__16)).
cutpoint(pc(s__3)).
cutpoint(pc(s__1)).
cutpoint(pc(s__17)).

% unfolding; morphing, master: reducer; folding; covering
r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_2 - Key_2_prime = -1, (Value_3 + Value_1 + 0 - Value_1_prime) - Value_3_prime = 0, Key_26_prime - Key_26 = -1, Key_25 = Key_25_prime, Value_16_prime = Value_16, Value_35 - Value_35_prime = -1, Reducer_1_prime - Reducer_1 = 1, Value_1 =< Value_1_prime + Value_3_prime, Value_1_prime =< Value_1, 1 =< Key_2_prime, 1 =< Key_26, 0 =< Value_16, 1 =< Value_35_prime, 0 =< Value_1_prime, 0 =< Reducer_1, 0 =< Key_25_prime, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
[], 0).
% unfolding; inhibiting; morphing, reducer; folding; covering
r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_2 - Key_2_prime = 1, Value_1 = Value_1_prime, Key_25 - Key_25_prime = -1, Key_26_prime = Key_26, Value_35 - Value_35_prime = 1, Reducer_1_prime - Reducer_1 = -1, Value_16_prime - Value_16 = 1, Value_3_prime =< Value_3, 1 =< Key_25_prime, 0 =< Key_26, 0 =< Key_2_prime, 0 =< Value_16, 0 =< Value_1_prime, 0 =< Value_35_prime, 0 =< Value_3_prime, 1 =< Reducer_1, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
[], 1).
% inhibiting; morphing, master: reducers created; folding; covering
r(  p(pc(s__16), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_2 = Key_2_prime, (Value_1_prime + 0 - Value_1) - Value_35 = 0, Value_3 = Value_3_prime, Value_16_prime = Value_16, Key_25 = Key_25_prime, Reducer_1_prime = Reducer_1, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
[], 2).
% inhibiting; morphing, master: mapping done; covering
r(  p(pc(s__3), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_25 = Key_26_prime, Value_1 = Value_1_prime, Key_25_prime = 0, Value_35_prime = 0, Key_2_prime = 0, Value_3_prime = 0, Reducer_1_prime = 0, Value_16_prime = 0, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
[], 3).
% unfolding; morphing, mapper; folding; covering
r(  p(pc(s__3), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Input_7_prime - Input_7 = -1, Mapper_1_prime - Mapper_1 = -1, Key_25 =< Key_25_prime, 0 =< Key_25, Value_1 =< Value_1_prime, 0 =< Value_1, 1 =< Input_7, 1 =< Mapper_1, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
[], 4).
% unfolding; inhibiting; morphing, reducer; folding; covering
r(  p(pc(s__1), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_25 - Key_25_prime = -1, Reducer_1 - Reducer_1_prime = 1, Value_1 - Value_1_prime = 1, Key_2 - Key_2_prime = 1, Value_16 - Value_16_prime = -1, Value_3_prime =< Value_3, 0 =< Value_3_prime, 0 =< Value_1_prime, 0 =< Reducer_1_prime, 0 =< Key_2_prime, 1 =< Value_16_prime, 1 =< Key_25_prime, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
[], 5).
% inhibiting; morphing, master: done; folding; covering
r(  p(pc(s__1), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__9), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Key_25 = Key_25_prime, (Value_1 + Value_16 + Value_3) - Value_16_prime = 0, Key_2_prime = 0, Input_7_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Value_1_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
[], 6).
% initialize
r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__16), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 =< Key_26_prime, 0 =< Value_3_prime, 0 =< Reducer_1_prime, 0 =< Key_25_prime, 0 =< Value_1_prime, 0 =< Value_16_prime, 0 =< Key_2_prime, 0 =< Value_35_prime, Input_7_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0 ],
[], 7).
% initialize
r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 =< Input_7_prime, 0 =< Value_1_prime, 0 =< Key_25_prime, 0 =< Mapper_1_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
[], 8).
% initialize
r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__1), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 =< Key_25_prime, 0 =< Key_2_prime, 0 =< Reducer_1_prime, 0 =< Value_1_prime, 0 =< Value_16_prime, 0 =< Value_3_prime, Input_7_prime = 0, Value_35_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
[], 9).
% initialize
r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__9), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 =< Key_25_prime, 0 =< Value_16_prime, Key_2_prime = 0, Input_7_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Value_1_prime = 0, Input_6_prime = 0, Mapper_1_prime = 0, Key_26_prime = 0 ],
[], 10).
% initialize
r(  p(pc(s__36), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ 0 =< Input_6_prime, 0 =< Value_1_prime, 0 =< Input_7_prime, 0 =< Key_25_prime, 0 =< Mapper_1_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_prime = 0 ],
[], 11).
% inhibiting; morphing, master: mappers created; covering
r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__3), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Mapper_1 = Mapper_1_prime, Key_25 = Key_25_prime, Value_1 = Value_1_prime, Input_6 = Input_7_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Input_6_prime = 0, Key_26_prime = 0 ],
[], 12).
% unfolding; morphing, master: make mappers; folding; covering
r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Mapper_1 - Mapper_1_prime = -1, Input_7 - Input_7_prime = 1, Value_1_prime = Value_1, Key_25 = Key_25_prime, Input_6_prime - Input_6 = 1, 1 =< Mapper_1_prime, 0 =< Input_7_prime, 0 =< Value_1, 0 =< Input_6, 0 =< Key_25_prime, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_prime = 0 ],
[], 13).
% unfolding; morphing, mapper; folding; covering
r(  p(pc(s__17), data(Key_25, Key_2, Value_16, Input_7, Reducer_1, Value_35, Value_3, Value_1, Input_6, Mapper_1, Key_26)),
p(pc(s__17), data(Key_25_prime, Key_2_prime, Value_16_prime, Input_7_prime, Reducer_1_prime, Value_35_prime, Value_3_prime, Value_1_prime, Input_6_prime, Mapper_1_prime, Key_26_prime)),
[ Mapper_1 - Mapper_1_prime = 1, Input_7 = Input_7_prime, Input_6_prime - Input_6 = -1, Key_25 =< Key_25_prime, 0 =< Key_25, 0 =< Mapper_1_prime, Value_1 =< Value_1_prime, 0 =< Value_1, 0 =< Input_7_prime, 1 =< Input_6, Key_2_prime = 0, Value_16_prime = 0, Reducer_1_prime = 0, Value_35_prime = 0, Value_3_prime = 0, Key_26_prime = 0 ],
[], 14).
```

## ARMC output

```ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.O2fHhllD1y
]
...done.

--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4 5 6 7

==================================================
ARMC-LIVE: program is correct

abstract trans fixpoint
abstract_trans_state(0, pc(s__36), pc(s__36), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__36), pc(s__16), [2,6,10,13,14,18,22,26,30,33,34,37,38,42], stem, 2, (1,7)).
abstract_trans_state(1, pc(s__36), pc(s__3), [2,5,6,9,10,14,17,18,21,22,25,26,30,33,34,38,41,42], stem, 3, (1,8)).
abstract_trans_state(1, pc(s__36), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,37,38,41,42], stem, 4, (1,9)).
abstract_trans_state(1, pc(s__36), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], stem, 5, (1,10)).
abstract_trans_state(1, pc(s__36), pc(s__17), [2,5,6,9,10,14,17,18,21,22,25,26,30,34,38,41,42], stem, 6, (1,11)).
abstract_trans_state(2, pc(s__16), pc(s__16), [2,4,6,10,12,13,14,16,18,22,26,30,33,34,36,37,38,40,42,43], loop, 7, (2,0)).
abstract_trans_state(2, pc(s__16), pc(s__16), [2,6,7,10,13,14,16,18,19,22,23,26,30,32,33,34,36,37,38,40,42,44], loop, 8, (2,1)).
abstract_trans_state(2, pc(s__16), pc(s__1), [2,4,6,8,10,12,13,14,16,18,20,21,22,26,28,30,33,34,36,37,38,40,41,42], loop, 9, (2,2)).
abstract_trans_state(2, pc(s__3), pc(s__16), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,36,37,38,42], loop, 10, (3,3)).
abstract_trans_state(2, pc(s__3), pc(s__3), [2,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,33,34,36,38,39,41,42,44], loop, 11, (3,4)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,24,26,30,31,33,34,36,37,38,40,41,42,44], loop, 12, (4,5)).
abstract_trans_state(2, pc(s__1), pc(s__9), [2,4,5,6,10,13,14,16,17,18,21,22,24,25,26,29,30,33,34,36,37,38,40,41,42,44], loop, 13, (4,6)).
abstract_trans_state(2, pc(s__17), pc(s__3), [2,4,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,32,33,34,38,40,41,42,44], loop, 14, (6,12)).
abstract_trans_state(2, pc(s__17), pc(s__17), [2,4,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,32,34,38,41,42,44], loop, 15, (6,13)).
abstract_trans_state(2, pc(s__17), pc(s__17), [2,5,6,8,9,10,12,14,16,17,18,20,21,22,24,25,26,28,30,34,35,38,39,41,42,44], loop, 16, (6,14)).
abstract_trans_state(3, pc(s__16), pc(s__16), [2,6,10,13,14,16,18,22,26,30,33,34,36,37,38,40,42,43], loop, 17, (7,1)).
abstract_trans_state(3, pc(s__16), pc(s__1), [2,4,6,10,12,13,14,16,18,21,22,26,30,33,34,36,37,38,40,41,42,43], loop, 18, (7,2)).
abstract_trans_state(3, pc(s__16), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,23,26,30,33,34,36,37,38,40,41,42], loop, 19, (8,2)).
abstract_trans_state(3, pc(s__16), pc(s__1), [2,6,7,10,13,14,16,18,19,21,22,26,30,33,34,36,37,38,40,41,42], loop, 20, (9,5)).
abstract_trans_state(3, pc(s__16), pc(s__9), [2,4,5,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,36,37,38,40,41,42], loop, 21, (9,6)).
abstract_trans_state(3, pc(s__3), pc(s__16), [1,2,6,9,10,12,13,14,18,22,26,30,33,34,36,37,38,42], loop, 22, (10,0)).
abstract_trans_state(3, pc(s__3), pc(s__1), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,36,37,38,41,42], loop, 23, (10,2)).
abstract_trans_state(3, pc(s__1), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,24,25,26,29,30,31,33,34,36,37,38,40,41,42,44], loop, 24, (12,6)).
abstract_trans_state(3, pc(s__17), pc(s__16), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,37,38,42], loop, 25, (14,3)).
abstract_trans_state(3, pc(s__17), pc(s__3), [2,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,33,34,38,39,41,42,44], loop, 26, (14,4)).
abstract_trans_state(3, pc(s__17), pc(s__3), [2,4,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,32,33,34,38,41,42,44], loop, 27, (15,12)).
abstract_trans_state(3, pc(s__17), pc(s__17), [2,5,6,8,9,10,12,14,15,17,18,20,21,22,24,25,26,28,30,34,38,41,42,44], loop, 28, (15,14)).
abstract_trans_state(4, pc(s__16), pc(s__1), [2,6,10,13,14,16,18,21,22,26,30,33,34,36,37,38,40,41,42,43], loop, 29, (17,2)).
abstract_trans_state(4, pc(s__16), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,23,25,26,29,30,33,34,36,37,38,40,41,42], loop, 30, (19,6)).
abstract_trans_state(4, pc(s__16), pc(s__9), [2,5,6,7,10,13,14,16,17,18,19,21,22,25,26,29,30,33,34,36,37,38,40,41,42], loop, 31, (20,6)).
abstract_trans_state(4, pc(s__3), pc(s__16), [2,6,10,13,14,18,22,26,30,33,34,36,37,38,42], loop, 32, (22,1)).
abstract_trans_state(4, pc(s__3), pc(s__1), [1,2,6,9,10,12,13,14,18,21,22,26,30,33,34,36,37,38,41,42], loop, 33, (22,2)).
abstract_trans_state(4, pc(s__3), pc(s__9), [1,2,5,6,8,10,13,14,17,18,20,21,22,24,25,26,28,29,30,33,34,36,37,38,41,42], loop, 34, (23,6)).
abstract_trans_state(4, pc(s__17), pc(s__16), [1,2,6,9,10,12,13,14,18,22,26,30,33,34,37,38,42], loop, 35, (25,0)).
abstract_trans_state(4, pc(s__17), pc(s__1), [1,2,5,6,8,9,10,12,13,14,17,18,20,21,22,24,25,26,28,30,32,33,34,37,38,41,42], loop, 36, (25,2)).
abstract_trans_state(4, pc(s__17), pc(s__3), [2,5,6,8,9,10,12,14,17,18,20,21,22,24,25,26,28,30,33,34,38,41,42,44], loop, 37, (27,4)).
abstract_trans_state(5, pc(s__16), pc(s__9), [2,5,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,36,37,38,40,41,42,43], loop, 38, (29,6)).
abstract_trans_state(5, pc(s__3), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,36,37,38,41,42], loop, 39, (32,2)).
abstract_trans_state(5, pc(s__3), pc(s__9), [1,2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,36,37,38,41,42], loop, 40, (33,6)).
abstract_trans_state(5, pc(s__17), pc(s__16), [2,6,10,13,14,18,22,26,30,33,34,37,38,42], loop, 41, (35,1)).
abstract_trans_state(5, pc(s__17), pc(s__1), [1,2,6,9,10,12,13,14,18,21,22,26,30,33,34,37,38,41,42], loop, 42, (35,2)).
abstract_trans_state(5, pc(s__17), pc(s__9), [1,2,5,6,8,10,13,14,17,18,20,21,22,24,25,26,28,29,30,33,34,37,38,41,42], loop, 43, (36,6)).
abstract_trans_state(6, pc(s__3), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,36,37,38,41,42], loop, 44, (39,6)).
abstract_trans_state(6, pc(s__17), pc(s__1), [2,6,10,13,14,18,21,22,26,30,33,34,37,38,41,42], loop, 45, (41,2)).
abstract_trans_state(6, pc(s__17), pc(s__9), [1,2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], loop, 46, (42,6)).
abstract_trans_state(7, pc(s__17), pc(s__9), [2,5,6,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42], loop, 47, (45,6)).

frontier 0: stem 1 (pc(s__36)->pc(s__36)) from 0 by applying 0: 	T
frontier 1: stem 2 (pc(s__36)->pc(s__16)) from 1 by applying 7: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 1: stem 3 (pc(s__36)->pc(s__3)) from 1 by applying 8: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=value\$16', 0=<value\$16', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 1: stem 4 (pc(s__36)->pc(s__1)) from 1 by applying 9: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 1: stem 5 (pc(s__36)->pc(s__9)) from 1 by applying 10: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 1: stem 6 (pc(s__36)->pc(s__17)) from 1 by applying 11: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=value\$16', 0=<value\$16', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=<value\$1', 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 2: loop 7 (pc(s__16)->pc(s__16)) from 2 by applying 0: 	0=<key\$25', key\$25'=key\$25, 0=<key\$2', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=<key\$26', key\$26'<key\$26
frontier 2: loop 8 (pc(s__16)->pc(s__16)) from 2 by applying 1: 	0=<key\$25', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', reducer\$1'<reducer\$1, 0=<value\$35', value\$35'<value\$35, 0=<value\$3', 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=<key\$26', key\$26'=key\$26
frontier 2: loop 9 (pc(s__16)->pc(s__1)) from 2 by applying 2: 	0=<key\$25', key\$25'=key\$25, 0=<key\$2', key\$2'=key\$2, 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 2: loop 10 (pc(s__3)->pc(s__16)) from 3 by applying 3: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 2: loop 11 (pc(s__3)->pc(s__3)) from 3 by applying 4: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', input\$7'<input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=<mapper\$1', mapper\$1'<mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 2: loop 12 (pc(s__1)->pc(s__1)) from 4 by applying 5: 	0=<key\$25', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=<value\$3', 0=<value\$1', value\$1'<value\$1, 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 2: loop 13 (pc(s__1)->pc(s__9)) from 4 by applying 6: 	0=<key\$25', key\$25'=key\$25, 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 2: loop 14 (pc(s__17)->pc(s__3)) from 6 by applying 12: 	0=<key\$25', key\$25'=key\$25, 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 2: loop 15 (pc(s__17)->pc(s__17)) from 6 by applying 13: 	0=<key\$25', key\$25'=key\$25, 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', input\$7'<input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 2: loop 16 (pc(s__17)->pc(s__17)) from 6 by applying 14: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=<input\$6', input\$6'<input\$6, 0=<mapper\$1', mapper\$1'<mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 3: loop 17 (pc(s__16)->pc(s__16)) from 7 by applying 1: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=<key\$26', key\$26'<key\$26
frontier 3: loop 18 (pc(s__16)->pc(s__1)) from 7 by applying 2: 	0=<key\$25', key\$25'=key\$25, 0=<key\$2', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'<key\$26
frontier 3: loop 19 (pc(s__16)->pc(s__1)) from 8 by applying 2: 	0=<key\$25', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', value\$35'<value\$35, 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 3: loop 20 (pc(s__16)->pc(s__1)) from 9 by applying 5: 	0=<key\$25', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 3: loop 21 (pc(s__16)->pc(s__9)) from 9 by applying 6: 	0=<key\$25', key\$25'=key\$25, 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 3: loop 22 (pc(s__3)->pc(s__16)) from 10 by applying 0: 	0=key\$25', 0=<key\$25', 0=<key\$2', 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 3: loop 23 (pc(s__3)->pc(s__1)) from 10 by applying 2: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 3: loop 24 (pc(s__1)->pc(s__9)) from 12 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', value\$1'<value\$1, 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 3: loop 25 (pc(s__17)->pc(s__16)) from 14 by applying 3: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 3: loop 26 (pc(s__17)->pc(s__3)) from 14 by applying 4: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=input\$6', 0=<input\$6', 0=<mapper\$1', mapper\$1'<mapper\$1, 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 3: loop 27 (pc(s__17)->pc(s__3)) from 15 by applying 12: 	0=<key\$25', key\$25'=key\$25, 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 3: loop 28 (pc(s__17)->pc(s__17)) from 15 by applying 14: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', input\$7'<input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 4: loop 29 (pc(s__16)->pc(s__1)) from 17 by applying 2: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'<key\$26
frontier 4: loop 30 (pc(s__16)->pc(s__9)) from 19 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', value\$35'<value\$35, 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 4: loop 31 (pc(s__16)->pc(s__9)) from 20 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'<key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'<reducer\$1, 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26'
frontier 4: loop 32 (pc(s__3)->pc(s__16)) from 22 by applying 1: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 4: loop 33 (pc(s__3)->pc(s__1)) from 22 by applying 2: 	0=key\$25', 0=<key\$25', 0=<key\$2', 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 4: loop 34 (pc(s__3)->pc(s__9)) from 23 by applying 6: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 4: loop 35 (pc(s__17)->pc(s__16)) from 25 by applying 0: 	0=key\$25', 0=<key\$25', 0=<key\$2', 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 4: loop 36 (pc(s__17)->pc(s__1)) from 25 by applying 2: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', value\$1'=value\$1, 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 4: loop 37 (pc(s__17)->pc(s__3)) from 27 by applying 4: 	0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=<value\$1', 0=input\$6', 0=<input\$6', 0=<mapper\$1', 0=key\$26', 0=<key\$26', key\$26'=key\$26
frontier 5: loop 38 (pc(s__16)->pc(s__9)) from 29 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'<key\$26
frontier 5: loop 39 (pc(s__3)->pc(s__1)) from 32 by applying 2: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 5: loop 40 (pc(s__3)->pc(s__9)) from 33 by applying 6: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 5: loop 41 (pc(s__17)->pc(s__16)) from 35 by applying 1: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=<key\$26'
frontier 5: loop 42 (pc(s__17)->pc(s__1)) from 35 by applying 2: 	0=key\$25', 0=<key\$25', 0=<key\$2', 0=value\$16', 0=<value\$16', value\$16'=value\$16, 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 5: loop 43 (pc(s__17)->pc(s__9)) from 36 by applying 6: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', key\$2'=key\$2, 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'=value\$3, 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 6: loop 44 (pc(s__3)->pc(s__9)) from 39 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 6: loop 45 (pc(s__17)->pc(s__1)) from 41 by applying 2: 	0=<key\$25', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=<value\$3', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 6: loop 46 (pc(s__17)->pc(s__9)) from 42 by applying 6: 	0=key\$25', 0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'
frontier 7: loop 47 (pc(s__17)->pc(s__9)) from 45 by applying 6: 	0=<key\$25', 0=key\$2', 0=<key\$2', 0=<value\$16', 0=input\$7', 0=<input\$7', 0=reducer\$1', 0=<reducer\$1', 0=value\$35', 0=<value\$35', 0=value\$3', 0=<value\$3', 0=value\$1', 0=<value\$1', 0=input\$6', 0=<input\$6', 0=mapper\$1', 0=<mapper\$1', 0=key\$26', 0=<key\$26'

_6498->_6501:	#44:	0=key\$25', 0=<key\$25', key\$25'<key\$25, key\$25'=key\$25, 0=key\$2', 0=<key\$2', key\$2'<key\$2, key\$2'=key\$2, 0=value\$16', 0=<value\$16', value\$16'<value\$16, value\$16'=value\$16, 0=input\$7', 0=<input\$7', input\$7'<input\$7, input\$7'=input\$7, 0=reducer\$1', 0=<reducer\$1', reducer\$1'<reducer\$1, reducer\$1'=reducer\$1, 0=value\$35', 0=<value\$35', value\$35'<value\$35, value\$35'=value\$35, 0=value\$3', 0=<value\$3', value\$3'<value\$3, value\$3'=value\$3, 0=value\$1', 0=<value\$1', value\$1'<value\$1, value\$1'=value\$1, 0=input\$6', 0=<input\$6', input\$6'<input\$6, input\$6'=input\$6, 0=mapper\$1', 0=<mapper\$1', mapper\$1'<mapper\$1, mapper\$1'=mapper\$1, 0=key\$26', 0=<key\$26', key\$26'<key\$26, key\$26'=key\$26
---------------------------------------------+----run(s)----+---wall(s)----+
Time on instantiating uf axioms              |     0.00     |     0.00     |
Time on cli constraint solving               |     0.00     |     0.00     |
Time on cli constraint preparation           |     0.00     |     0.00     |
Time on cli matrix parsing                   |     0.00     |     0.00     |
Time on cli preprocessing                    |     0.00     |     0.00     |
Time on concretizing trans rel               |     0.00     |     0.00     |
Time on concretizing from state              |     0.00     |     0.00     |
Time on computing the subsumer subtree       |     0.00     |     0.00     |
Time on finding the location of subsumer in queue|     0.00     |     0.00     |
Time on path invariant generation            |     0.00     |     0.00     |
Time on new predicate selection              |     0.00     |     0.00     |
Time on refinement preprocessing cut         |     0.00     |     0.00     |
Time on refinement cutting trace             |     0.00     |     0.00     |
Time on refinement finding unsat subtrace    |     0.00     |     0.00     |
Time on refinement                           |     0.00     |     0.00     |
Time on fixpoint abstraction                 |     0.00     |     0.00     |
Time on fixpoint test                        |     0.02     |     0.02     |
Time on abstract check                       |     0.00     |     0.00     |
Time on total including result checking      |     0.00     |     0.00     |
Time on check result                         |     0.00     |     0.00     |
Time on total                                |     0.00     |     0.00     |
---------------------------------------------+--------------+--------------+

==================================================
ARMC-LIVE: program is correct

```