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

    Cover

    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