Computing Termination of core/src/test/resources/dbp_graph/termination/mapReduceFailure.dbp
Computing Termination of core/src/test/resources/dbp_graph/termination/mapReduceFailure.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
// self.trapExit = true
// var assignedMappers = Map[Actor, (K, V)]()
// def spawnMapper(key: K, value: V) = {
// val mapper = link {
// master ! Intermediate(mapping(key, value))
// }
// assignedMappers += (mapper -> (key, value))
// mapper
// }
// for ((key, value) <- input)
// spawnMapper(key, value)
// var intermediates = List[(K2, V2)]()
// var nleft = input.length
// while (nleft > 0)
// receive {
// case Intermediate(list) => intermediates :::= list
// case Exit(from, 'normal) => nleft -= 1
// case Exit(from, reason) =>
// // retrieve assigned work
// val (key, value) = assignedMappers(from)
// // spawn new worker to re-execute the work
// spawnMapper(key, value)
// }
// 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]]()
//TODO also consider failures of the reducers
// for (_ <- 1 to dict.size)
// receive {
// case Reduced(key, values) =>
// result += (key -> values)
// }
// result
// }
//To make this things work we need to bound the number of failure.
//the clean things is to have a fairness constraints to force some progress but it is not yet implemented
//for the moment we adda failure counter that prevents failure to occur infinitely often
init
(m, master) -> (i, input)*
node (f, failure)*
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: mapper died"
pre
(m, master1) -> (c, crash)
(c, crash) -> (i, input)
post
(m, master1) -> (w, mapper)
(w, mapper) -> (i, input)
==>
m -> m
i -> i
<==
transition "master: mapping done"
pre
node (m, master1)
post
node (m, master2)
==>
m -> m
<==
no
(m, master1) -> (w, _)
(w, _) -> (i, input)
==>
m -> m
transition "master: reducer"
pre
(m, master2) -> (k1, key) [inter]
post
(m, master2) -> (w, reducer)
(w, reducer) -> (k1, key)
==>
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: reducer died"
pre
(m, master3) -> (c, crash)
(c, crash) -> (k1, key)
post
(m, master3) -> (w, reducer)
(w, reducer) -> (k1, key)
==>
m -> m
k1 -> k1
<==
transition "master: done"
pre
node (m, master3)
post
node (m, master4)
==>
m -> m
<==
no
(m, master3) -> (w, _)
(w, _) -> (k1, key)
==>
m -> m
transition "mapper: ok"
pre
(m, _) -> (w, mapper)
(w, mapper) -> (i, input)
post
(m, _) -> (k, key)* [inter]
(k, key)* -> (v, value)**
node (f, failure)*
==>
<==
m -> m
transition "mapper: crash"
pre
(m, _) -> (w, mapper)
(w, mapper) -> (i, input)
node (f, failure)
post
(m, _) -> (c, crash)
(c, crash) -> (i, input)
==>
i -> i
<==
m -> m
transition "reducer: ok"
pre
(m, _) -> (w, reducer)
(w, reducer) -> (k1, key)
post
(m, _) -> (k2, key) [result]
(k2, key) -> (v1, value)
node (f, failure)*
==>
<==
m -> m
no
(k1, key) -> (v2, value)
==>
k1 -> k1
transition "reducer: crash"
pre
(m, _) -> (w, reducer)
(w, reducer) -> (k1, key)
node (f, failure)
post
(m, _) -> (c, crash)
(c, crash) -> (k1, key)
==>
k1 -> k1
<==
m -> m
Graph rewriting system
-
Initial Configuration
-
Transitions
-
master: make mappers
-
master: mappers created
-
master: mapper died
-
master: mapping done
-
master: reducer
-
master: reducers created
-
master: reducer died
-
master: done
-
mapper: ok
-
mapper: crash
-
reducer: ok
-
reducer: crash
Cover
-
cover element 0
-
cover element 1
-
cover element 2
-
cover element 3
-
cover element 4
Numerical Abstraction
% BEGIN FIXED PREAMBLE
:- multifile r/5,implicit_updates/0,var2names/2,preds/2,trans_preds/3,
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(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)), [(Failure_34, 'failure$34'), (Value_2, 'value$2'), (Value_4, 'value$4'), (Value_5, 'value$5'), (Input_27, 'input$27'), (Key_105, 'key$105'), (Key_6, 'key$6'), (Input_28, 'input$28'), (Crash_41, 'crash$41'), (Reducer_2, 'reducer$2'), (Key_5, 'key$5'), (Input_26, 'input$26'), (Value_3, 'value$3'), (Mapper_1, 'mapper$1'), (Key_4, 'key$4')]).
preds( p(_, data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)), []).
trans_preds(
p(_, data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(_, data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Crash_41_prime + Reducer_2_prime < Crash_41 + Reducer_2,
Crash_41_prime + Reducer_2_prime = Crash_41 + Reducer_2,
Crash_41_prime + Mapper_1_prime < Crash_41 + Mapper_1,
Crash_41_prime + Mapper_1_prime = Crash_41 + Mapper_1,
0 = Failure_34_prime,
0 =< Failure_34_prime,
Failure_34_prime < Failure_34,
Failure_34_prime = Failure_34,
0 = Value_2_prime,
0 =< Value_2_prime,
Value_2_prime < Value_2,
Value_2_prime = Value_2,
0 = Value_4_prime,
0 =< Value_4_prime,
Value_4_prime < Value_4,
Value_4_prime = Value_4,
0 = Value_5_prime,
0 =< Value_5_prime,
Value_5_prime < Value_5,
Value_5_prime = Value_5,
0 = Input_27_prime,
0 =< Input_27_prime,
Input_27_prime < Input_27,
Input_27_prime = Input_27,
0 = Key_105_prime,
0 =< Key_105_prime,
Key_105_prime < Key_105,
Key_105_prime = Key_105,
0 = Key_6_prime,
0 =< Key_6_prime,
Key_6_prime < Key_6,
Key_6_prime = Key_6,
0 = Input_28_prime,
0 =< Input_28_prime,
Input_28_prime < Input_28,
Input_28_prime = Input_28,
0 = Crash_41_prime,
0 =< Crash_41_prime,
Crash_41_prime < Crash_41,
Crash_41_prime = Crash_41,
0 = Reducer_2_prime,
0 =< Reducer_2_prime,
Reducer_2_prime < Reducer_2,
Reducer_2_prime = Reducer_2,
0 = Key_5_prime,
0 =< Key_5_prime,
Key_5_prime < Key_5,
Key_5_prime = Key_5,
0 = Input_26_prime,
0 =< Input_26_prime,
Input_26_prime < Input_26,
Input_26_prime = Input_26,
0 = Value_3_prime,
0 =< Value_3_prime,
Value_3_prime < Value_3,
Value_3_prime = Value_3,
0 = Mapper_1_prime,
0 =< Mapper_1_prime,
Mapper_1_prime < Mapper_1,
Mapper_1_prime = Mapper_1,
0 = Key_4_prime,
0 =< Key_4_prime,
Key_4_prime < Key_4,
Key_4_prime = Key_4
]).
start( pc(s__55)).
cutpoint(pc(s__30)).
cutpoint(pc(s__2)).
cutpoint(pc(s__42)).
cutpoint(pc(s__1)).
% unfolding; morphing, mapper: ok; folding; covering
r( p(pc(s__30), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__30), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Input_27 = Input_27_prime, Input_28 - Input_28_prime = 1, Mapper_1_prime - Mapper_1 = -1, Crash_41 = Crash_41_prime, Value_2 =< Value_2_prime, 0 =< Value_2, Failure_34 =< Failure_34_prime, 0 =< Failure_34, 0 =< Input_28_prime, 0 =< Crash_41_prime, 1 =< Mapper_1, Key_105 =< Key_105_prime, 0 =< Key_105, 0 =< Input_27_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 0).
% unfolding; morphing, master: mapper died; folding; covering
r( p(pc(s__30), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__30), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Failure_34_prime = Failure_34, Input_27 - Input_27_prime = 1, Value_2 = Value_2_prime, Input_28 - Input_28_prime = -1, Crash_41 - Crash_41_prime = 1, Key_105_prime = Key_105, Mapper_1 - Mapper_1_prime = -1, 1 =< Input_28_prime, 0 =< Failure_34, 0 =< Input_27_prime, 0 =< Value_2_prime, 0 =< Key_105, 0 =< Crash_41_prime, 1 =< Mapper_1_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 1).
% unfolding; morphing, mapper: crash; folding; covering
r( p(pc(s__30), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__30), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Value_2_prime = Value_2, Input_27 - Input_27_prime = -1, Input_28 - Input_28_prime = 1, Failure_34 - Failure_34_prime = 1, Key_105_prime = Key_105, Crash_41 - Crash_41_prime = -1, Mapper_1_prime - Mapper_1 = -1, 0 =< Value_2, 0 =< Input_28_prime, 1 =< Crash_41_prime, 1 =< Mapper_1, 0 =< Failure_34_prime, 0 =< Key_105, 1 =< Input_27_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 2).
% inhibiting; morphing, master: mapping done; covering
r( p(pc(s__30), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__2), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Failure_34 = Failure_34_prime, Key_6_prime = 0, Value_2 = Value_3_prime, Reducer_2_prime = 0, Key_105 = Key_5_prime, Value_5_prime = 0, Value_4_prime = 0, Crash_41_prime = 0, Value_2_prime = 0, Key_105_prime = 0, Key_4_prime = 0, Input_27_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Mapper_1_prime = 0 ],
[], 3).
% unfolding; morphing, master: reducer; folding; covering
r( p(pc(s__2), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__2), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Reducer_2 - Reducer_2_prime = -1, Failure_34_prime = Failure_34, Value_4 = Value_4_prime, Crash_41 = Crash_41_prime, Value_2 = Value_2_prime, Key_5_prime - Key_5 = -1, (Value_5_prime + Value_3_prime) - Value_3 - Value_5 = 0, Key_6 - Key_6_prime = -1, Key_4 = Key_4_prime, Key_105_prime = Key_105, 0 =< Value_4_prime, 0 =< Value_2_prime, 1 =< Key_5, 0 =< Key_105, 1 =< Reducer_2_prime, 0 =< Value_5, 0 =< Key_4_prime, Value_3_prime =< Value_3, 0 =< Value_3_prime, 0 =< Crash_41_prime, 1 =< Key_6_prime, 0 =< Failure_34, Input_27_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Mapper_1_prime = 0 ],
[], 4).
% unfolding; inhibiting; morphing, reducer: ok; folding; covering
r( p(pc(s__2), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__2), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Reducer_2 - Reducer_2_prime = 1, Value_4 = Value_4_prime, Crash_41_prime = Crash_41, Value_2 - Value_2_prime = -1, Key_6 - Key_6_prime = 1, Key_4 = Key_4_prime, Key_5 = Key_5_prime, Key_105 - Key_105_prime = -1, Value_3 = Value_3_prime, 0 =< Crash_41, 0 =< Reducer_2_prime, Value_5_prime =< Value_5, 0 =< Value_5_prime, 1 =< Value_2_prime, 0 =< Key_5_prime, 0 =< Key_6_prime, 0 =< Key_4_prime, Failure_34 =< Failure_34_prime, 0 =< Value_4_prime, 1 =< Key_105_prime, 0 =< Failure_34, 0 =< Value_3_prime, Input_27_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Mapper_1_prime = 0 ],
[], 5).
% unfolding; morphing, reducer: crash; folding; covering
r( p(pc(s__2), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__2), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Reducer_2 - Reducer_2_prime = 1, Key_4_prime - Key_4 = 1, (Value_4 + Value_5) - Value_4_prime - Value_5_prime = 0, Crash_41 - Crash_41_prime = -1, Value_2 = Value_2_prime, Key_6_prime - Key_6 = -1, Key_5 = Key_5_prime, Failure_34_prime - Failure_34 = -1, Key_105 = Key_105_prime, Value_3_prime = Value_3, Value_5_prime =< Value_5, 0 =< (Value_5_prime + Value_4_prime) - Value_5, 0 =< Value_5_prime, 0 =< Reducer_2_prime, 1 =< Key_6, 0 =< Key_4, 1 =< Crash_41_prime, 0 =< Value_2_prime, 0 =< Key_105_prime, 0 =< Key_5_prime, 1 =< Failure_34, 0 =< Value_3, Input_27_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Mapper_1_prime = 0 ],
[], 6).
% inhibiting; morphing, master: reducers created; folding; covering
r( p(pc(s__2), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__1), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Value_5 = Value_5_prime, Key_105 = Key_6_prime, (Value_2 + Value_3) - Value_2_prime = 0, Key_5_prime = Key_6, Key_4_prime = Key_4, Reducer_2_prime = Reducer_2, Crash_41_prime = Crash_41, Failure_34 = Failure_34_prime, Value_4_prime = Value_4, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0 ],
[], 7).
% inhibiting; morphing, master: mappers created; covering
r( p(pc(s__42), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__30), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Input_27 = Input_27_prime, Value_2 = Value_2_prime, Input_28 = Input_28_prime, Failure_34 = Failure_34_prime, Mapper_1_prime = Mapper_1, Key_105_prime = Key_105, Crash_41 = Crash_41_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 8).
% unfolding; morphing, mapper: crash; folding; covering
r( p(pc(s__42), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__42), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Input_27 - Input_27_prime = -1, Value_2 = Value_2_prime, Input_28 - Input_28_prime = 1, Failure_34 - Failure_34_prime = 1, Input_26_prime = Input_26, Mapper_1 - Mapper_1_prime = 1, Crash_41_prime - Crash_41 = 1, Key_105_prime = Key_105, 0 =< Failure_34_prime, 1 =< Input_27_prime, 0 =< Mapper_1_prime, 0 =< Input_28_prime, 0 =< Crash_41, 0 =< Key_105, 0 =< Value_2_prime, 0 =< Input_26, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 9).
% unfolding; morphing, mapper: ok; folding; covering
r( p(pc(s__42), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__42), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Input_27 = Input_27_prime, Input_28 - Input_28_prime = 1, Input_26_prime = Input_26, Mapper_1 - Mapper_1_prime = 1, Crash_41_prime = Crash_41, Value_2 =< Value_2_prime, 0 =< Value_2, 0 =< Input_27_prime, Key_105 =< Key_105_prime, Failure_34 =< Failure_34_prime, 0 =< Failure_34, 0 =< Mapper_1_prime, 0 =< Input_28_prime, 0 =< Crash_41, 0 =< Key_105, 0 =< Input_26, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 10).
% unfolding; morphing, master: make mappers; folding; covering
r( p(pc(s__42), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__42), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Input_27 = Input_27_prime, Value_2 = Value_2_prime, Input_28 - Input_28_prime = -1, Failure_34 = Failure_34_prime, Mapper_1 - Mapper_1_prime = -1, Key_105_prime = Key_105, Input_26_prime - Input_26 = -1, Crash_41 = Crash_41_prime, 0 =< Input_27_prime, 0 =< Failure_34_prime, 1 =< Input_28_prime, 0 =< Value_2_prime, 0 =< Crash_41_prime, 0 =< Key_105, 1 =< Mapper_1_prime, 1 =< Input_26, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 11).
% inhibiting; morphing, master: done; folding; covering
r( p(pc(s__1), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__27), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Key_6 = Key_6_prime, Failure_34 = Failure_34_prime, (Value_5 + Value_4 + Value_2) - Value_2_prime = 0, Value_4_prime = 0, Value_5_prime = 0, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Crash_41_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
[], 12).
% unfolding; morphing, master: reducer died; folding; covering
r( p(pc(s__1), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__1), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ (Value_5 + Value_4 + 0 - Value_4_prime) - Value_5_prime = 0, Key_5_prime - Key_5 = 1, Reducer_2 - Reducer_2_prime = -1, Crash_41 - Crash_41_prime = 1, Failure_34_prime = Failure_34, Key_4 - Key_4_prime = 1, Value_2_prime = Value_2, Key_6 = Key_6_prime, Value_4 =< Value_4_prime + Value_5_prime, Value_4_prime =< Value_4, 0 =< Failure_34, 0 =< Value_4_prime, 1 =< Reducer_2_prime, 0 =< Crash_41_prime, 0 =< Key_5, 0 =< Key_4_prime, 0 =< Key_6_prime, 0 =< Value_2, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0 ],
[], 13).
% unfolding; morphing, reducer: crash; folding; covering
r( p(pc(s__1), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__1), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ (Value_5 + Value_4 + 0 - Value_4_prime) - Value_5_prime = 0, Reducer_2 - Reducer_2_prime = 1, Key_4_prime - Key_4 = 1, Crash_41 - Crash_41_prime = -1, Key_5_prime - Key_5 = -1, Failure_34 - Failure_34_prime = 1, Key_6_prime = Key_6, Value_2_prime = Value_2, Value_4 =< Value_4_prime, 0 =< Value_4, 0 =< Key_4, 0 =< Value_5_prime, 1 =< Crash_41_prime, 0 =< Failure_34_prime, 1 =< Key_5, 0 =< Key_6, 0 =< Reducer_2_prime, 0 =< Value_2, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0 ],
[], 14).
% unfolding; inhibiting; morphing, reducer: ok; folding; covering
r( p(pc(s__1), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__1), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ Reducer_2 - Reducer_2_prime = 1, Value_4 = Value_4_prime, Crash_41 = Crash_41_prime, Key_4 = Key_4_prime, Key_5 - Key_5_prime = 1, Value_2_prime - Value_2 = 1, Key_6_prime - Key_6 = 1, Value_5_prime =< Value_5, 0 =< Value_4_prime, Failure_34 =< Failure_34_prime, 0 =< Failure_34, 0 =< Reducer_2_prime, 0 =< Key_4_prime, 0 =< Key_6, 0 =< Value_5_prime, 0 =< Value_2, 0 =< Crash_41_prime, 0 =< Key_5_prime, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0 ],
[], 15).
% initialize
r( p(pc(s__55), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__30), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ 0 =< Mapper_1_prime, 0 =< Value_2_prime, 0 =< Failure_34_prime, 0 =< Key_105_prime, 0 =< Crash_41_prime, 0 =< Input_28_prime, 0 =< Input_27_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 16).
% initialize
r( p(pc(s__55), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__27), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ 0 =< Value_2_prime, 0 =< Failure_34_prime, 0 =< Key_6_prime, Value_4_prime = 0, Value_5_prime = 0, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Crash_41_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0, Key_4_prime = 0 ],
[], 17).
% initialize
r( p(pc(s__55), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__2), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ 0 =< Value_5_prime, 0 =< Key_5_prime, 0 =< Key_105_prime, 0 =< Key_6_prime, 0 =< Reducer_2_prime, 0 =< Failure_34_prime, 0 =< Value_2_prime, 0 =< Value_3_prime, 0 =< Key_4_prime, 0 =< Value_4_prime, 0 =< Crash_41_prime, Input_27_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Mapper_1_prime = 0 ],
[], 18).
% initialize
r( p(pc(s__55), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__42), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ 0 =< Value_2_prime, 0 =< Mapper_1_prime, 0 =< Input_28_prime, 0 =< Crash_41_prime, 0 =< Input_26_prime, 0 =< Failure_34_prime, 0 =< Key_105_prime, 0 =< Input_27_prime, Value_4_prime = 0, Value_5_prime = 0, Key_6_prime = 0, Reducer_2_prime = 0, Key_5_prime = 0, Value_3_prime = 0, Key_4_prime = 0 ],
[], 19).
% initialize
r( p(pc(s__55), data(Failure_34, Value_2, Value_4, Value_5, Input_27, Key_105, Key_6, Input_28, Crash_41, Reducer_2, Key_5, Input_26, Value_3, Mapper_1, Key_4)),
p(pc(s__1), data(Failure_34_prime, Value_2_prime, Value_4_prime, Value_5_prime, Input_27_prime, Key_105_prime, Key_6_prime, Input_28_prime, Crash_41_prime, Reducer_2_prime, Key_5_prime, Input_26_prime, Value_3_prime, Mapper_1_prime, Key_4_prime)),
[ 0 =< Value_4_prime, 0 =< Failure_34_prime, 0 =< Key_4_prime, 0 =< Key_6_prime, 0 =< Value_5_prime, 0 =< Reducer_2_prime, 0 =< Value_2_prime, 0 =< Crash_41_prime, 0 =< Key_5_prime, Input_27_prime = 0, Key_105_prime = 0, Input_28_prime = 0, Input_26_prime = 0, Value_3_prime = 0, Mapper_1_prime = 0 ],
[], 20).
ARMC output
ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008)
rybal@mpi-sws.mpg.de
cmd line: [live,/tmp/tmp.uY9goJqy5d
]
reading input from /tmp/tmp.uY9goJqy5d
...done.
--------------------------------------------------
abstraction refinement iteration 0:
lfp iteration 0 1 2 3 4 5 6 7 8
==================================================
ARMC-LIVE: program is correct
abstract trans fixpoint
abstract_trans_state(0, pc(s__55), pc(s__55), [], stem, 1, (0,0)).
abstract_trans_state(1, pc(s__55), pc(s__30), [6,10,13,14,17,18,22,26,29,30,34,38,41,42,45,46,49,50,53,54,58,61,62], stem, 2, (1,16)).
abstract_trans_state(1, pc(s__55), pc(s__27), [6,10,13,14,17,18,21,22,25,26,30,33,34,37,38,41,42,45,46,49,50,53,54,57,58,61,62], stem, 3, (1,17)).
abstract_trans_state(1, pc(s__55), pc(s__2), [6,10,14,18,21,22,26,30,33,34,38,42,46,49,50,54,57,58,62], stem, 4, (1,18)).
abstract_trans_state(1, pc(s__55), pc(s__42), [6,10,13,14,17,18,22,26,29,30,34,38,41,42,45,46,50,53,54,58,61,62], stem, 5, (1,19)).
abstract_trans_state(1, pc(s__55), pc(s__1), [6,10,14,18,21,22,25,26,30,33,34,38,42,46,49,50,53,54,57,58,62], stem, 6, (1,20)).
abstract_trans_state(2, pc(s__30), pc(s__30), [2,3,6,10,13,14,16,17,18,20,22,24,26,29,30,32,34,35,38,40,41,42,44,45,46,48,49,50,52,53,54,56,58,59,61,62,64], loop, 7, (2,0)).
abstract_trans_state(2, pc(s__30), pc(s__30), [1,4,6,8,10,12,13,14,16,17,18,20,22,23,26,28,29,30,32,34,38,39,41,42,44,45,46,48,49,50,52,53,54,56,58,61,62,64], loop, 8, (2,1)).
abstract_trans_state(2, pc(s__30), pc(s__30), [4,6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,35,38,41,42,44,45,46,48,49,50,52,53,54,56,58,59,61,62,64], loop, 9, (2,2)).
abstract_trans_state(2, pc(s__30), pc(s__2), [6,8,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,46,49,50,52,54,57,58,61,62,64], loop, 10, (2,3)).
abstract_trans_state(2, pc(s__2), pc(s__2), [4,6,8,10,12,14,16,18,21,22,24,26,28,30,33,34,36,38,40,42,46,47,49,50,52,54,57,58,60,62,64], loop, 11, (4,4)).
abstract_trans_state(2, pc(s__2), pc(s__2), [1,4,6,10,14,16,18,21,22,24,26,30,31,33,34,36,38,40,42,43,46,48,49,50,52,54,56,57,58,60,62,64], loop, 12, (4,5)).
abstract_trans_state(2, pc(s__2), pc(s__2), [2,6,7,10,12,14,18,21,22,24,26,28,30,31,33,34,36,38,42,43,46,48,49,50,52,54,56,57,58,60,62], loop, 13, (4,6)).
abstract_trans_state(2, pc(s__2), pc(s__1), [2,4,6,8,10,14,16,18,20,21,22,24,25,26,30,33,34,36,38,40,42,44,46,49,50,52,53,54,57,58,60,62,64], loop, 14, (4,7)).
abstract_trans_state(2, pc(s__42), pc(s__30), [2,4,6,8,10,12,13,14,16,17,18,20,22,24,26,28,29,30,32,34,36,38,40,41,42,44,45,46,48,49,50,53,54,56,58,60,61,62,64], loop, 15, (5,8)).
abstract_trans_state(2, pc(s__42), pc(s__42), [4,6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,35,38,41,42,44,45,46,48,50,52,53,54,56,58,59,61,62,64], loop, 16, (5,9)).
abstract_trans_state(2, pc(s__42), pc(s__42), [2,3,6,10,13,14,16,17,18,20,22,24,26,29,30,32,34,35,38,40,41,42,44,45,46,48,50,52,53,54,56,58,59,61,62,64], loop, 17, (5,10)).
abstract_trans_state(2, pc(s__42), pc(s__42), [2,6,8,10,12,13,14,16,17,18,20,22,24,26,28,29,30,32,34,38,40,41,42,44,45,46,48,50,51,53,54,56,58,61,62,64], loop, 18, (5,11)).
abstract_trans_state(2, pc(s__1), pc(s__27), [6,8,10,13,14,17,18,21,22,24,25,26,28,30,32,33,34,36,37,38,41,42,45,46,49,50,52,53,54,56,57,58,60,61,62], loop, 19, (6,12)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,3,6,8,10,12,14,18,21,22,24,25,26,28,30,32,33,34,36,38,39,42,46,49,50,52,53,54,56,57,58,60,62,63], loop, 20, (6,13)).
abstract_trans_state(2, pc(s__1), pc(s__1), [2,6,7,10,12,14,18,21,22,24,25,26,28,30,32,33,34,36,38,42,43,46,47,49,50,52,53,54,56,57,58,60,62], loop, 21, (6,14)).
abstract_trans_state(2, pc(s__1), pc(s__1), [1,4,6,10,14,16,18,21,22,24,25,26,28,30,33,34,36,38,40,42,43,46,47,49,50,52,53,54,56,57,58,60,62,64], loop, 22, (6,15)).
abstract_trans_state(3, pc(s__30), pc(s__30), [1,3,6,10,13,14,16,17,18,20,22,23,26,29,30,32,34,38,39,41,42,44,45,46,48,49,50,52,53,54,56,58,61,62,64], loop, 23, (7,1)).
abstract_trans_state(3, pc(s__30), pc(s__30), [3,6,10,13,14,16,17,18,20,22,26,29,30,32,34,35,38,41,42,44,45,46,48,49,50,52,53,54,56,58,59,61,62,64], loop, 24, (7,2)).
abstract_trans_state(3, pc(s__30), pc(s__2), [3,6,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,46,49,50,52,54,57,58,59,61,62,64], loop, 25, (7,3)).
abstract_trans_state(3, pc(s__30), pc(s__30), [4,6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,38,41,42,44,45,46,48,49,50,52,53,54,56,58,61,62,64], loop, 26, (8,2)).
abstract_trans_state(3, pc(s__30), pc(s__2), [6,7,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,46,49,50,52,54,57,58,59,61,62,64], loop, 27, (9,3)).
abstract_trans_state(3, pc(s__30), pc(s__2), [6,8,9,10,13,14,16,18,21,22,25,26,30,33,34,37,38,42,46,49,50,52,54,57,58,61,62,64], loop, 28, (10,4)).
abstract_trans_state(3, pc(s__30), pc(s__1), [6,8,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 29, (10,7)).
abstract_trans_state(3, pc(s__2), pc(s__2), [4,6,10,14,16,18,21,22,24,26,30,33,34,36,38,40,42,46,47,49,50,52,54,57,58,60,62,64], loop, 30, (11,5)).
abstract_trans_state(3, pc(s__2), pc(s__2), [6,7,10,12,14,18,21,22,24,26,28,30,33,34,36,38,42,46,47,49,50,52,54,57,58,60,62], loop, 31, (11,6)).
abstract_trans_state(3, pc(s__2), pc(s__1), [4,6,8,10,14,16,18,21,22,24,25,26,30,33,34,36,38,40,42,46,49,50,52,53,54,57,58,60,62,64], loop, 32, (11,7)).
abstract_trans_state(3, pc(s__2), pc(s__2), [1,6,10,14,18,21,22,24,26,30,31,33,34,36,38,42,43,46,48,49,50,52,54,56,57,58,60,62], loop, 33, (12,6)).
abstract_trans_state(3, pc(s__2), pc(s__1), [1,4,6,10,14,16,18,21,22,24,25,26,30,33,34,36,38,40,42,43,46,49,50,52,53,54,57,58,60,62,64], loop, 34, (12,7)).
abstract_trans_state(3, pc(s__2), pc(s__1), [2,6,7,10,14,18,21,22,24,25,26,30,33,34,36,38,42,43,46,49,50,52,53,54,57,58,60,62], loop, 35, (13,7)).
abstract_trans_state(3, pc(s__2), pc(s__27), [6,8,10,13,14,17,18,21,22,24,25,26,30,33,34,36,37,38,41,42,45,46,49,50,52,53,54,57,58,60,61,62], loop, 36, (14,12)).
abstract_trans_state(3, pc(s__2), pc(s__1), [2,3,6,8,10,14,18,21,22,24,25,26,30,33,34,36,38,39,42,46,49,50,52,53,54,57,58,60,62,63], loop, 37, (14,13)).
abstract_trans_state(3, pc(s__42), pc(s__30), [2,3,6,10,13,14,16,17,18,20,22,24,26,29,30,32,34,35,38,40,41,42,44,45,46,48,49,50,53,54,56,58,59,61,62,64], loop, 38, (15,0)).
abstract_trans_state(3, pc(s__42), pc(s__30), [1,4,6,8,10,12,13,14,16,17,18,20,22,23,26,28,29,30,32,34,38,39,41,42,44,45,46,48,49,50,53,54,56,58,61,62,64], loop, 39, (15,1)).
abstract_trans_state(3, pc(s__42), pc(s__30), [4,6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,35,38,41,42,44,45,46,48,49,50,53,54,56,58,59,61,62,64], loop, 40, (15,2)).
abstract_trans_state(3, pc(s__42), pc(s__2), [6,8,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,46,49,50,54,57,58,61,62,64], loop, 41, (15,3)).
abstract_trans_state(3, pc(s__42), pc(s__42), [3,6,10,13,14,16,17,18,20,22,26,29,30,32,34,35,38,41,42,44,45,46,48,50,52,53,54,56,58,59,61,62,64], loop, 42, (16,10)).
abstract_trans_state(3, pc(s__42), pc(s__42), [6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,38,41,42,44,45,46,48,50,51,53,54,56,58,61,62,64], loop, 43, (16,11)).
abstract_trans_state(3, pc(s__42), pc(s__42), [2,6,10,13,14,16,17,18,20,22,24,26,29,30,32,34,38,40,41,42,44,45,46,48,50,51,53,54,56,58,61,62,64], loop, 44, (17,11)).
abstract_trans_state(3, pc(s__42), pc(s__30), [2,6,8,10,12,13,14,16,17,18,20,22,24,26,28,29,30,32,34,38,40,41,42,44,45,46,48,49,50,51,53,54,56,58,61,62,64], loop, 45, (18,8)).
abstract_trans_state(3, pc(s__1), pc(s__1), [2,6,7,10,12,14,18,21,22,24,25,26,28,30,32,33,34,36,38,42,46,49,50,52,53,54,56,57,58,60,62], loop, 46, (20,14)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,3,6,10,14,18,21,22,24,25,26,28,30,33,34,36,38,39,42,46,49,50,52,53,54,56,57,58,60,62,63], loop, 47, (20,15)).
abstract_trans_state(3, pc(s__1), pc(s__27), [6,7,10,13,14,17,18,21,22,24,25,26,28,30,32,33,34,36,37,38,41,42,43,45,46,47,49,50,52,53,54,56,57,58,60,61,62], loop, 48, (21,12)).
abstract_trans_state(3, pc(s__1), pc(s__1), [1,6,10,14,18,21,22,24,25,26,28,30,33,34,36,38,42,43,46,47,49,50,52,53,54,56,57,58,60,62], loop, 49, (21,15)).
abstract_trans_state(3, pc(s__1), pc(s__27), [1,6,10,13,14,17,18,21,22,24,25,26,28,30,33,34,36,37,38,41,42,43,45,46,47,49,50,52,53,54,56,57,58,60,61,62], loop, 50, (22,12)).
abstract_trans_state(4, pc(s__30), pc(s__30), [3,6,10,13,14,16,17,18,20,22,26,29,30,32,34,38,41,42,44,45,46,48,49,50,52,53,54,56,58,61,62,64], loop, 51, (23,2)).
abstract_trans_state(4, pc(s__30), pc(s__2), [1,3,6,9,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,46,49,50,52,54,57,58,61,62,64], loop, 52, (23,3)).
abstract_trans_state(4, pc(s__30), pc(s__2), [3,6,9,10,13,14,16,18,21,22,25,26,30,33,34,35,37,38,42,46,49,50,52,54,57,58,59,61,62,64], loop, 53, (25,4)).
abstract_trans_state(4, pc(s__30), pc(s__1), [3,6,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 54, (25,7)).
abstract_trans_state(4, pc(s__30), pc(s__2), [6,7,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,46,49,50,52,54,57,58,61,62,64], loop, 55, (26,3)).
abstract_trans_state(4, pc(s__30), pc(s__2), [6,7,9,10,13,14,16,18,21,22,25,26,30,33,34,35,37,38,42,46,49,50,52,54,57,58,59,61,62,64], loop, 56, (27,4)).
abstract_trans_state(4, pc(s__30), pc(s__1), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 57, (27,7)).
abstract_trans_state(4, pc(s__30), pc(s__2), [6,10,13,14,16,18,21,22,26,30,33,34,37,38,42,46,49,50,52,54,57,58,61,62,64], loop, 58, (28,5)).
abstract_trans_state(4, pc(s__30), pc(s__2), [6,7,9,10,14,18,21,22,25,26,30,33,34,38,42,46,49,50,52,54,57,58,62], loop, 59, (28,6)).
abstract_trans_state(4, pc(s__30), pc(s__1), [6,8,10,13,14,16,18,21,22,25,26,29,30,33,34,37,38,42,46,49,50,52,53,54,57,58,61,62,64], loop, 60, (28,7)).
abstract_trans_state(4, pc(s__30), pc(s__27), [6,8,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 61, (29,12)).
abstract_trans_state(4, pc(s__2), pc(s__2), [6,10,14,18,21,22,24,26,30,33,34,36,38,42,46,47,49,50,52,54,57,58,60,62], loop, 62, (30,6)).
abstract_trans_state(4, pc(s__2), pc(s__1), [4,6,10,14,16,18,21,22,24,25,26,30,33,34,36,38,40,42,46,49,50,52,53,54,57,58,60,62,64], loop, 63, (30,7)).
abstract_trans_state(4, pc(s__2), pc(s__1), [6,7,10,14,18,21,22,24,25,26,30,33,34,36,38,42,46,49,50,52,53,54,57,58,60,62], loop, 64, (31,7)).
abstract_trans_state(4, pc(s__2), pc(s__1), [3,6,8,10,14,18,21,22,24,25,26,30,33,34,36,38,39,42,46,49,50,52,53,54,57,58,60,62,63], loop, 65, (32,13)).
abstract_trans_state(4, pc(s__2), pc(s__1), [1,6,10,14,18,21,22,24,25,26,30,33,34,36,38,42,43,46,49,50,52,53,54,57,58,60,62], loop, 66, (33,7)).
abstract_trans_state(4, pc(s__2), pc(s__27), [1,6,10,13,14,17,18,21,22,24,25,26,30,33,34,36,37,38,41,42,43,45,46,49,50,52,53,54,57,58,60,61,62], loop, 67, (34,12)).
abstract_trans_state(4, pc(s__2), pc(s__1), [1,3,6,10,14,18,21,22,24,25,26,30,33,34,36,38,39,42,46,49,50,52,53,54,57,58,60,62,63], loop, 68, (34,13)).
abstract_trans_state(4, pc(s__2), pc(s__27), [6,7,10,13,14,17,18,21,22,24,25,26,30,33,34,36,37,38,41,42,43,45,46,49,50,52,53,54,57,58,60,61,62], loop, 69, (35,12)).
abstract_trans_state(4, pc(s__42), pc(s__30), [1,3,6,10,13,14,16,17,18,20,22,23,26,29,30,32,34,38,39,41,42,44,45,46,48,49,50,53,54,56,58,61,62,64], loop, 70, (38,1)).
abstract_trans_state(4, pc(s__42), pc(s__30), [3,6,10,13,14,16,17,18,20,22,26,29,30,32,34,35,38,41,42,44,45,46,48,49,50,53,54,56,58,59,61,62,64], loop, 71, (38,2)).
abstract_trans_state(4, pc(s__42), pc(s__2), [3,6,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,46,49,50,54,57,58,59,61,62,64], loop, 72, (38,3)).
abstract_trans_state(4, pc(s__42), pc(s__30), [4,6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,38,41,42,44,45,46,48,49,50,53,54,56,58,61,62,64], loop, 73, (39,2)).
abstract_trans_state(4, pc(s__42), pc(s__2), [6,7,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,46,49,50,54,57,58,59,61,62,64], loop, 74, (40,3)).
abstract_trans_state(4, pc(s__42), pc(s__2), [6,8,9,10,13,14,16,18,21,22,25,26,30,33,34,37,38,42,46,49,50,54,57,58,61,62,64], loop, 75, (41,4)).
abstract_trans_state(4, pc(s__42), pc(s__1), [6,8,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 76, (41,7)).
abstract_trans_state(4, pc(s__42), pc(s__42), [6,10,13,14,16,17,18,20,22,26,29,30,32,34,38,41,42,44,45,46,48,50,51,53,54,56,58,61,62,64], loop, 77, (42,11)).
abstract_trans_state(4, pc(s__42), pc(s__30), [6,7,10,12,13,14,16,17,18,20,22,26,28,29,30,32,34,38,41,42,44,45,46,48,49,50,51,53,54,56,58,61,62,64], loop, 78, (43,8)).
abstract_trans_state(4, pc(s__42), pc(s__30), [2,6,10,13,14,16,17,18,20,22,24,26,29,30,32,34,38,40,41,42,44,45,46,48,49,50,51,53,54,56,58,61,62,64], loop, 79, (44,8)).
abstract_trans_state(4, pc(s__42), pc(s__30), [1,6,8,10,12,13,14,16,17,18,20,22,23,26,28,29,30,32,34,38,39,41,42,44,45,46,48,49,50,51,53,54,56,58,61,62,64], loop, 80, (45,1)).
abstract_trans_state(4, pc(s__1), pc(s__27), [6,7,10,13,14,17,18,21,22,24,25,26,28,30,32,33,34,36,37,38,41,42,45,46,49,50,52,53,54,56,57,58,60,61,62], loop, 81, (46,12)).
abstract_trans_state(4, pc(s__1), pc(s__1), [1,6,10,14,18,21,22,24,25,26,28,30,33,34,36,38,42,46,49,50,52,53,54,56,57,58,60,62], loop, 82, (46,15)).
abstract_trans_state(4, pc(s__1), pc(s__27), [1,3,6,10,13,14,17,18,21,22,24,25,26,28,30,33,34,36,37,38,39,41,42,45,46,49,50,52,53,54,56,57,58,60,61,62,63], loop, 83, (47,12)).
abstract_trans_state(5, pc(s__30), pc(s__1), [1,3,6,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 84, (52,7)).
abstract_trans_state(5, pc(s__30), pc(s__2), [6,9,10,14,18,21,22,25,26,30,33,34,35,38,42,46,49,50,52,54,57,58,59,62], loop, 85, (53,6)).
abstract_trans_state(5, pc(s__30), pc(s__1), [3,6,10,13,14,16,18,21,22,25,26,29,30,33,34,35,37,38,42,46,49,50,52,53,54,57,58,59,61,62,64], loop, 86, (53,7)).
abstract_trans_state(5, pc(s__30), pc(s__27), [3,6,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 87, (54,12)).
abstract_trans_state(5, pc(s__30), pc(s__1), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 88, (55,7)).
abstract_trans_state(5, pc(s__30), pc(s__1), [6,7,10,13,14,16,18,21,22,25,26,29,30,33,34,35,37,38,42,46,49,50,52,53,54,57,58,59,61,62,64], loop, 89, (56,7)).
abstract_trans_state(5, pc(s__30), pc(s__27), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 90, (57,12)).
abstract_trans_state(5, pc(s__30), pc(s__2), [6,10,14,18,21,22,26,30,33,34,38,42,46,49,50,52,54,57,58,62], loop, 91, (58,6)).
abstract_trans_state(5, pc(s__30), pc(s__1), [6,10,13,14,16,18,21,22,25,26,30,33,34,37,38,42,46,49,50,52,53,54,57,58,61,62,64], loop, 92, (58,7)).
abstract_trans_state(5, pc(s__30), pc(s__1), [6,7,10,14,18,21,22,25,26,29,30,33,34,38,42,46,49,50,52,53,54,57,58,62], loop, 93, (59,7)).
abstract_trans_state(5, pc(s__30), pc(s__27), [6,8,10,13,14,16,17,18,21,22,25,26,29,30,33,34,37,38,41,42,45,46,49,50,52,53,54,57,58,61,62,64], loop, 94, (60,12)).
abstract_trans_state(5, pc(s__2), pc(s__1), [6,10,14,18,21,22,24,25,26,30,33,34,36,38,42,46,49,50,52,53,54,57,58,60,62], loop, 95, (62,7)).
abstract_trans_state(5, pc(s__2), pc(s__27), [6,10,13,14,17,18,21,22,24,25,26,30,33,34,36,37,38,41,42,45,46,49,50,52,53,54,57,58,60,61,62], loop, 96, (63,12)).
abstract_trans_state(5, pc(s__42), pc(s__30), [3,6,10,13,14,16,17,18,20,22,26,29,30,32,34,38,41,42,44,45,46,48,49,50,53,54,56,58,61,62,64], loop, 97, (70,2)).
abstract_trans_state(5, pc(s__42), pc(s__2), [1,3,6,9,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,46,49,50,54,57,58,61,62,64], loop, 98, (70,3)).
abstract_trans_state(5, pc(s__42), pc(s__2), [3,6,9,10,13,14,16,18,21,22,25,26,30,33,34,35,37,38,42,46,49,50,54,57,58,59,61,62,64], loop, 99, (72,4)).
abstract_trans_state(5, pc(s__42), pc(s__1), [3,6,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,53,54,57,58,59,61,62,64], loop, 100, (72,7)).
abstract_trans_state(5, pc(s__42), pc(s__2), [6,7,9,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,46,49,50,54,57,58,61,62,64], loop, 101, (73,3)).
abstract_trans_state(5, pc(s__42), pc(s__2), [6,7,9,10,13,14,16,18,21,22,25,26,30,33,34,35,37,38,42,46,49,50,54,57,58,59,61,62,64], loop, 102, (74,4)).
abstract_trans_state(5, pc(s__42), pc(s__1), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,53,54,57,58,59,61,62,64], loop, 103, (74,7)).
abstract_trans_state(5, pc(s__42), pc(s__2), [6,10,13,14,16,18,21,22,26,30,33,34,37,38,42,46,49,50,54,57,58,61,62,64], loop, 104, (75,5)).
abstract_trans_state(5, pc(s__42), pc(s__2), [6,7,9,10,14,18,21,22,25,26,30,33,34,38,42,46,49,50,54,57,58,62], loop, 105, (75,6)).
abstract_trans_state(5, pc(s__42), pc(s__1), [6,8,10,13,14,16,18,21,22,25,26,29,30,33,34,37,38,42,46,49,50,53,54,57,58,61,62,64], loop, 106, (75,7)).
abstract_trans_state(5, pc(s__42), pc(s__27), [6,8,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 107, (76,12)).
abstract_trans_state(5, pc(s__42), pc(s__30), [6,10,13,14,16,17,18,20,22,26,29,30,32,34,38,41,42,44,45,46,48,49,50,51,53,54,56,58,61,62,64], loop, 108, (77,8)).
abstract_trans_state(5, pc(s__1), pc(s__27), [1,6,10,13,14,17,18,21,22,24,25,26,28,30,33,34,36,37,38,41,42,45,46,49,50,52,53,54,56,57,58,60,61,62], loop, 109, (82,12)).
abstract_trans_state(6, pc(s__30), pc(s__27), [1,3,6,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 110, (84,12)).
abstract_trans_state(6, pc(s__30), pc(s__1), [6,10,14,18,21,22,25,26,29,30,33,34,35,38,42,46,49,50,52,53,54,57,58,59,62], loop, 111, (85,7)).
abstract_trans_state(6, pc(s__30), pc(s__27), [3,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 112, (86,12)).
abstract_trans_state(6, pc(s__30), pc(s__27), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,52,53,54,57,58,61,62,64], loop, 113, (88,12)).
abstract_trans_state(6, pc(s__30), pc(s__27), [6,7,10,13,14,16,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,52,53,54,57,58,59,61,62,64], loop, 114, (89,12)).
abstract_trans_state(6, pc(s__30), pc(s__1), [6,10,14,18,21,22,25,26,30,33,34,38,42,46,49,50,52,53,54,57,58,62], loop, 115, (91,7)).
abstract_trans_state(6, pc(s__30), pc(s__27), [6,10,13,14,16,17,18,21,22,25,26,30,33,34,37,38,41,42,45,46,49,50,52,53,54,57,58,61,62,64], loop, 116, (92,12)).
abstract_trans_state(6, pc(s__30), pc(s__27), [6,7,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42,45,46,49,50,52,53,54,57,58,61,62], loop, 117, (93,12)).
abstract_trans_state(6, pc(s__42), pc(s__1), [1,3,6,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 118, (98,7)).
abstract_trans_state(6, pc(s__42), pc(s__2), [6,9,10,14,18,21,22,25,26,30,33,34,35,38,42,46,49,50,54,57,58,59,62], loop, 119, (99,6)).
abstract_trans_state(6, pc(s__42), pc(s__1), [3,6,10,13,14,16,18,21,22,25,26,29,30,33,34,35,37,38,42,46,49,50,53,54,57,58,59,61,62,64], loop, 120, (99,7)).
abstract_trans_state(6, pc(s__42), pc(s__27), [3,6,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,53,54,57,58,59,61,62,64], loop, 121, (100,12)).
abstract_trans_state(6, pc(s__42), pc(s__1), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 122, (101,7)).
abstract_trans_state(6, pc(s__42), pc(s__1), [6,7,10,13,14,16,18,21,22,25,26,29,30,33,34,35,37,38,42,46,49,50,53,54,57,58,59,61,62,64], loop, 123, (102,7)).
abstract_trans_state(6, pc(s__42), pc(s__27), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,35,37,38,41,42,44,45,46,49,50,53,54,57,58,59,61,62,64], loop, 124, (103,12)).
abstract_trans_state(6, pc(s__42), pc(s__2), [6,10,14,18,21,22,26,30,33,34,38,42,46,49,50,54,57,58,62], loop, 125, (104,6)).
abstract_trans_state(6, pc(s__42), pc(s__1), [6,10,13,14,16,18,21,22,25,26,30,33,34,37,38,42,46,49,50,53,54,57,58,61,62,64], loop, 126, (104,7)).
abstract_trans_state(6, pc(s__42), pc(s__1), [6,7,10,14,18,21,22,25,26,29,30,33,34,38,42,46,49,50,53,54,57,58,62], loop, 127, (105,7)).
abstract_trans_state(6, pc(s__42), pc(s__27), [6,8,10,13,14,16,17,18,21,22,25,26,29,30,33,34,37,38,41,42,45,46,49,50,53,54,57,58,61,62,64], loop, 128, (106,12)).
abstract_trans_state(7, pc(s__30), pc(s__27), [6,10,13,14,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,52,53,54,57,58,59,61,62], loop, 129, (111,12)).
abstract_trans_state(7, pc(s__30), pc(s__27), [6,10,13,14,17,18,21,22,25,26,30,33,34,37,38,41,42,45,46,49,50,52,53,54,57,58,61,62], loop, 130, (115,12)).
abstract_trans_state(7, pc(s__42), pc(s__27), [1,3,6,10,13,14,16,17,18,20,21,22,23,25,26,29,30,32,33,34,37,38,39,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 131, (118,12)).
abstract_trans_state(7, pc(s__42), pc(s__1), [6,10,14,18,21,22,25,26,29,30,33,34,35,38,42,46,49,50,53,54,57,58,59,62], loop, 132, (119,7)).
abstract_trans_state(7, pc(s__42), pc(s__27), [3,6,10,13,14,16,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,53,54,57,58,59,61,62,64], loop, 133, (120,12)).
abstract_trans_state(7, pc(s__42), pc(s__27), [6,7,10,13,14,16,17,18,20,21,22,25,26,29,30,32,33,34,37,38,41,42,44,45,46,49,50,53,54,57,58,61,62,64], loop, 134, (122,12)).
abstract_trans_state(7, pc(s__42), pc(s__27), [6,7,10,13,14,16,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,53,54,57,58,59,61,62,64], loop, 135, (123,12)).
abstract_trans_state(7, pc(s__42), pc(s__1), [6,10,14,18,21,22,25,26,30,33,34,38,42,46,49,50,53,54,57,58,62], loop, 136, (125,7)).
abstract_trans_state(7, pc(s__42), pc(s__27), [6,10,13,14,16,17,18,21,22,25,26,30,33,34,37,38,41,42,45,46,49,50,53,54,57,58,61,62,64], loop, 137, (126,12)).
abstract_trans_state(7, pc(s__42), pc(s__27), [6,7,10,13,14,17,18,21,22,25,26,29,30,33,34,37,38,41,42,45,46,49,50,53,54,57,58,61,62], loop, 138, (127,12)).
abstract_trans_state(8, pc(s__42), pc(s__27), [6,10,13,14,17,18,21,22,25,26,29,30,33,34,35,37,38,41,42,45,46,49,50,53,54,57,58,59,61,62], loop, 139, (132,12)).
abstract_trans_state(8, pc(s__42), pc(s__27), [6,10,13,14,17,18,21,22,25,26,30,33,34,37,38,41,42,45,46,49,50,53,54,57,58,61,62], loop, 140, (136,12)).
frontier 0: stem 1 (pc(s__55)->pc(s__55)) from 0 by applying 0: T
frontier 1: stem 2 (pc(s__55)->pc(s__30)) from 1 by applying 16: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 1: stem 3 (pc(s__55)->pc(s__27)) from 1 by applying 17: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 1: stem 4 (pc(s__55)->pc(s__2)) from 1 by applying 18: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 1: stem 5 (pc(s__55)->pc(s__42)) from 1 by applying 19: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=<input$26', 0=value$3', 0=<value$3', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 1: stem 6 (pc(s__55)->pc(s__1)) from 1 by applying 20: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 2: loop 7 (pc(s__30)->pc(s__30)) from 2 by applying 0: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 8 (pc(s__30)->pc(s__30)) from 2 by applying 1: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'<input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 9 (pc(s__30)->pc(s__30)) from 2 by applying 2: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 10 (pc(s__30)->pc(s__2)) from 2 by applying 3: 0=<failure$34', failure$34'=failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 11 (pc(s__2)->pc(s__2)) from 4 by applying 4: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 2: loop 12 (pc(s__2)->pc(s__2)) from 4 by applying 5: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', 0=<key$6', key$6'<key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 2: loop 13 (pc(s__2)->pc(s__2)) from 4 by applying 6: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=<key$6', key$6'<key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 2: loop 14 (pc(s__2)->pc(s__1)) from 4 by applying 7: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 2: loop 15 (pc(s__42)->pc(s__30)) from 5 by applying 8: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 16 (pc(s__42)->pc(s__42)) from 5 by applying 9: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 17 (pc(s__42)->pc(s__42)) from 5 by applying 10: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 18 (pc(s__42)->pc(s__42)) from 5 by applying 11: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 2: loop 19 (pc(s__1)->pc(s__27)) from 6 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 2: loop 20 (pc(s__1)->pc(s__1)) from 6 by applying 13: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'<crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4
frontier 2: loop 21 (pc(s__1)->pc(s__1)) from 6 by applying 14: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 2: loop 22 (pc(s__1)->pc(s__1)) from 6 by applying 15: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 3: loop 23 (pc(s__30)->pc(s__30)) from 7 by applying 1: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'<input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 24 (pc(s__30)->pc(s__30)) from 7 by applying 2: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 25 (pc(s__30)->pc(s__2)) from 7 by applying 3: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 26 (pc(s__30)->pc(s__30)) from 8 by applying 2: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 27 (pc(s__30)->pc(s__2)) from 9 by applying 3: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 28 (pc(s__30)->pc(s__2)) from 10 by applying 4: 0=<failure$34', failure$34'=failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 29 (pc(s__30)->pc(s__1)) from 10 by applying 7: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 30 (pc(s__2)->pc(s__2)) from 11 by applying 5: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 3: loop 31 (pc(s__2)->pc(s__2)) from 11 by applying 6: 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 3: loop 32 (pc(s__2)->pc(s__1)) from 11 by applying 7: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 3: loop 33 (pc(s__2)->pc(s__2)) from 12 by applying 6: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', 0=<key$6', key$6'<key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 3: loop 34 (pc(s__2)->pc(s__1)) from 12 by applying 7: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 3: loop 35 (pc(s__2)->pc(s__1)) from 13 by applying 7: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 3: loop 36 (pc(s__2)->pc(s__27)) from 14 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 3: loop 37 (pc(s__2)->pc(s__1)) from 14 by applying 13: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'<crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4
frontier 3: loop 38 (pc(s__42)->pc(s__30)) from 15 by applying 0: crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 39 (pc(s__42)->pc(s__30)) from 15 by applying 1: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'<input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 40 (pc(s__42)->pc(s__30)) from 15 by applying 2: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 41 (pc(s__42)->pc(s__2)) from 15 by applying 3: 0=<failure$34', failure$34'=failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 42 (pc(s__42)->pc(s__42)) from 16 by applying 10: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 43 (pc(s__42)->pc(s__42)) from 16 by applying 11: 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 44 (pc(s__42)->pc(s__42)) from 17 by applying 11: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 45 (pc(s__42)->pc(s__30)) from 18 by applying 8: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 3: loop 46 (pc(s__1)->pc(s__1)) from 20 by applying 14: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 3: loop 47 (pc(s__1)->pc(s__1)) from 20 by applying 15: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'<crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4
frontier 3: loop 48 (pc(s__1)->pc(s__27)) from 21 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'<reducer$2, 0=key$5', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 3: loop 49 (pc(s__1)->pc(s__1)) from 21 by applying 15: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 3: loop 50 (pc(s__1)->pc(s__27)) from 22 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'<reducer$2, 0=key$5', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 4: loop 51 (pc(s__30)->pc(s__30)) from 23 by applying 2: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 52 (pc(s__30)->pc(s__2)) from 23 by applying 3: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 53 (pc(s__30)->pc(s__2)) from 25 by applying 4: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 54 (pc(s__30)->pc(s__1)) from 25 by applying 7: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 55 (pc(s__30)->pc(s__2)) from 26 by applying 3: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 56 (pc(s__30)->pc(s__2)) from 27 by applying 4: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 57 (pc(s__30)->pc(s__1)) from 27 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 58 (pc(s__30)->pc(s__2)) from 28 by applying 5: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 59 (pc(s__30)->pc(s__2)) from 28 by applying 6: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 4: loop 60 (pc(s__30)->pc(s__1)) from 28 by applying 7: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 61 (pc(s__30)->pc(s__27)) from 29 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 62 (pc(s__2)->pc(s__2)) from 30 by applying 6: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', key$5'<key$5, 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 4: loop 63 (pc(s__2)->pc(s__1)) from 30 by applying 7: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'=crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'=key$4
frontier 4: loop 64 (pc(s__2)->pc(s__1)) from 31 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 4: loop 65 (pc(s__2)->pc(s__1)) from 32 by applying 13: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'<crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4
frontier 4: loop 66 (pc(s__2)->pc(s__1)) from 33 by applying 7: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', reducer$2'<reducer$2, 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 4: loop 67 (pc(s__2)->pc(s__27)) from 34 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'<reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 4: loop 68 (pc(s__2)->pc(s__1)) from 34 by applying 13: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', crash$41'<crash$41, 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4', key$4'<key$4
frontier 4: loop 69 (pc(s__2)->pc(s__27)) from 35 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'<reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 4: loop 70 (pc(s__42)->pc(s__30)) from 38 by applying 1: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'<input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 71 (pc(s__42)->pc(s__30)) from 38 by applying 2: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', input$28'<input$28, 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 72 (pc(s__42)->pc(s__2)) from 38 by applying 3: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 73 (pc(s__42)->pc(s__30)) from 39 by applying 2: crash$41'+mapper$1'=crash$41+mapper$1, 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 74 (pc(s__42)->pc(s__2)) from 40 by applying 3: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 75 (pc(s__42)->pc(s__2)) from 41 by applying 4: 0=<failure$34', failure$34'=failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 76 (pc(s__42)->pc(s__1)) from 41 by applying 7: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 77 (pc(s__42)->pc(s__42)) from 42 by applying 11: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 78 (pc(s__42)->pc(s__30)) from 43 by applying 8: 0=<failure$34', failure$34'<failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 79 (pc(s__42)->pc(s__30)) from 44 by applying 8: crash$41'+reducer$2'=crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'=input$27, 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 80 (pc(s__42)->pc(s__30)) from 45 by applying 1: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', failure$34'=failure$34, 0=<value$2', value$2'=value$2, 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', input$27'<input$27, 0=<key$105', key$105'=key$105, 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 4: loop 81 (pc(s__1)->pc(s__27)) from 46 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 4: loop 82 (pc(s__1)->pc(s__1)) from 46 by applying 15: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 4: loop 83 (pc(s__1)->pc(s__27)) from 47 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4
frontier 5: loop 84 (pc(s__30)->pc(s__1)) from 52 by applying 7: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 85 (pc(s__30)->pc(s__2)) from 53 by applying 6: 0=<failure$34', 0=value$2', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4'
frontier 5: loop 86 (pc(s__30)->pc(s__1)) from 53 by applying 7: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 87 (pc(s__30)->pc(s__27)) from 54 by applying 12: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 88 (pc(s__30)->pc(s__1)) from 55 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 89 (pc(s__30)->pc(s__1)) from 56 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 90 (pc(s__30)->pc(s__27)) from 57 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 91 (pc(s__30)->pc(s__2)) from 58 by applying 6: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 5: loop 92 (pc(s__30)->pc(s__1)) from 58 by applying 7: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 93 (pc(s__30)->pc(s__1)) from 59 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 5: loop 94 (pc(s__30)->pc(s__27)) from 60 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 95 (pc(s__2)->pc(s__1)) from 62 by applying 7: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=<key$4'
frontier 5: loop 96 (pc(s__2)->pc(s__27)) from 63 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 5: loop 97 (pc(s__42)->pc(s__30)) from 70 by applying 2: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 98 (pc(s__42)->pc(s__2)) from 70 by applying 3: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 99 (pc(s__42)->pc(s__2)) from 72 by applying 4: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 100 (pc(s__42)->pc(s__1)) from 72 by applying 7: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 101 (pc(s__42)->pc(s__2)) from 73 by applying 3: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 102 (pc(s__42)->pc(s__2)) from 74 by applying 4: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 103 (pc(s__42)->pc(s__1)) from 74 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 104 (pc(s__42)->pc(s__2)) from 75 by applying 5: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 105 (pc(s__42)->pc(s__2)) from 75 by applying 6: 0=<failure$34', failure$34'<failure$34, 0=value$2', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 5: loop 106 (pc(s__42)->pc(s__1)) from 75 by applying 7: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 107 (pc(s__42)->pc(s__27)) from 76 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 108 (pc(s__42)->pc(s__30)) from 77 by applying 8: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=<input$27', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=<input$28', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 5: loop 109 (pc(s__1)->pc(s__27)) from 82 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', input$27'=input$27, 0=key$105', 0=<key$105', key$105'=key$105, 0=<key$6', 0=input$28', 0=<input$28', input$28'=input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'=mapper$1, 0=key$4', 0=<key$4'
frontier 6: loop 110 (pc(s__30)->pc(s__27)) from 84 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 111 (pc(s__30)->pc(s__1)) from 85 by applying 7: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4'
frontier 6: loop 112 (pc(s__30)->pc(s__27)) from 86 by applying 12: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 113 (pc(s__30)->pc(s__27)) from 88 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 114 (pc(s__30)->pc(s__27)) from 89 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 115 (pc(s__30)->pc(s__1)) from 91 by applying 7: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 6: loop 116 (pc(s__30)->pc(s__27)) from 92 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 117 (pc(s__30)->pc(s__27)) from 93 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 6: loop 118 (pc(s__42)->pc(s__1)) from 98 by applying 7: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 119 (pc(s__42)->pc(s__2)) from 99 by applying 6: 0=<failure$34', 0=value$2', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4'
frontier 6: loop 120 (pc(s__42)->pc(s__1)) from 99 by applying 7: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 121 (pc(s__42)->pc(s__27)) from 100 by applying 12: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 122 (pc(s__42)->pc(s__1)) from 101 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 123 (pc(s__42)->pc(s__1)) from 102 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 124 (pc(s__42)->pc(s__27)) from 103 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 125 (pc(s__42)->pc(s__2)) from 104 by applying 6: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 6: loop 126 (pc(s__42)->pc(s__1)) from 104 by applying 7: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 6: loop 127 (pc(s__42)->pc(s__1)) from 105 by applying 7: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 6: loop 128 (pc(s__42)->pc(s__27)) from 106 by applying 12: 0=<failure$34', failure$34'=failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 129 (pc(s__30)->pc(s__27)) from 111 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4'
frontier 7: loop 130 (pc(s__30)->pc(s__27)) from 115 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', input$26'=input$26, 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 7: loop 131 (pc(s__42)->pc(s__27)) from 118 by applying 12: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', crash$41'<crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 132 (pc(s__42)->pc(s__1)) from 119 by applying 7: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=<key$4'
frontier 7: loop 133 (pc(s__42)->pc(s__27)) from 120 by applying 12: crash$41'+mapper$1'<crash$41+mapper$1, 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 134 (pc(s__42)->pc(s__27)) from 122 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', value$5'=value$5, 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', key$6'=key$6, 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', reducer$2'=reducer$2, 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 135 (pc(s__42)->pc(s__27)) from 123 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 136 (pc(s__42)->pc(s__1)) from 125 by applying 7: 0=<failure$34', 0=<value$2', 0=<value$4', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=<crash$41', 0=<reducer$2', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=<key$4'
frontier 7: loop 137 (pc(s__42)->pc(s__27)) from 126 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', value$4'=value$4, 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4', key$4'=key$4
frontier 7: loop 138 (pc(s__42)->pc(s__27)) from 127 by applying 12: 0=<failure$34', failure$34'<failure$34, 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4'
frontier 8: loop 139 (pc(s__42)->pc(s__27)) from 132 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=key$6', 0=<key$6', 0=input$28', 0=<input$28', input$28'<input$28, 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, 0=key$4', 0=<key$4'
frontier 8: loop 140 (pc(s__42)->pc(s__27)) from 136 by applying 12: 0=<failure$34', 0=<value$2', 0=value$4', 0=<value$4', 0=value$5', 0=<value$5', 0=input$27', 0=<input$27', 0=key$105', 0=<key$105', 0=<key$6', 0=input$28', 0=<input$28', 0=crash$41', 0=<crash$41', 0=reducer$2', 0=<reducer$2', 0=key$5', 0=<key$5', 0=input$26', 0=<input$26', 0=value$3', 0=<value$3', 0=mapper$1', 0=<mapper$1', 0=key$4', 0=<key$4'
_8064->_8067: #64: crash$41'+reducer$2'<crash$41+reducer$2, crash$41'+reducer$2'=crash$41+reducer$2, crash$41'+mapper$1'<crash$41+mapper$1, crash$41'+mapper$1'=crash$41+mapper$1, 0=failure$34', 0=<failure$34', failure$34'<failure$34, failure$34'=failure$34, 0=value$2', 0=<value$2', value$2'<value$2, value$2'=value$2, 0=value$4', 0=<value$4', value$4'<value$4, value$4'=value$4, 0=value$5', 0=<value$5', value$5'<value$5, value$5'=value$5, 0=input$27', 0=<input$27', input$27'<input$27, input$27'=input$27, 0=key$105', 0=<key$105', key$105'<key$105, key$105'=key$105, 0=key$6', 0=<key$6', key$6'<key$6, key$6'=key$6, 0=input$28', 0=<input$28', input$28'<input$28, input$28'=input$28, 0=crash$41', 0=<crash$41', crash$41'<crash$41, crash$41'=crash$41, 0=reducer$2', 0=<reducer$2', reducer$2'<reducer$2, reducer$2'=reducer$2, 0=key$5', 0=<key$5', key$5'<key$5, key$5'=key$5, 0=input$26', 0=<input$26', input$26'<input$26, input$26'=input$26, 0=value$3', 0=<value$3', value$3'<value$3, value$3'=value$3, 0=mapper$1', 0=<mapper$1', mapper$1'<mapper$1, mapper$1'=mapper$1, 0=key$4', 0=<key$4', key$4'<key$4, key$4'=key$4
---------------------------------------------+----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.13 | 0.17 |
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