population protocol "Old Threshold Protocol with l = 3 and c = 1" {
    states { _l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3 _nl_true_m3 _nl_true_m2 _nl_true_m1 _nl_true_0 _nl_true_p1 _nl_true_p2 _nl_true_p3 _nl_false_m3 _nl_false_m2 _nl_false_m1 _nl_false_0 _nl_false_p1 _nl_false_p2 _nl_false_p3}
    transitions { x__l_true_m3__l_true_m3 x__l_true_m3__l_true_m2 x__l_true_m3__l_true_m1 x__l_true_m3__l_true_0 x__l_true_m3__l_true_p1 x__l_true_m3__l_true_p2 x__l_true_m3__l_true_p3 x__l_true_m2__l_true_m2 x__l_true_m2__l_true_m1 x__l_true_m2__l_true_0 x__l_true_m2__l_true_p1 x__l_true_m2__l_true_p2 x__l_true_m2__l_true_p3 x__l_true_m1__l_true_m1 x__l_true_m1__l_true_0 x__l_true_m1__l_true_p1 x__l_true_m1__l_true_p2 x__l_true_m1__l_true_p3 x__l_true_0__l_true_0 x__l_true_0__l_true_p1 x__l_true_0__l_true_p2 x__l_true_0__l_true_p3 x__l_true_p1__l_true_p1 x__l_true_p1__l_true_p2 x__l_true_p1__l_true_p3 x__l_true_p2__l_true_p2 x__l_true_p2__l_true_p3 x__l_true_p3__l_true_p3 x__l_false_m3__l_true_m3 x__l_false_m3__l_true_m2 x__l_false_m3__l_true_m1 x__l_false_m3__l_true_0 x__l_false_m3__l_true_p1 x__l_false_m3__l_true_p2 x__l_false_m3__l_true_p3 x__l_false_m3__l_false_m3 x__l_false_m3__l_false_m2 x__l_false_m3__l_false_m1 x__l_false_m3__l_false_0 x__l_false_m3__l_false_p1 x__l_false_m3__l_false_p2 x__l_false_m3__l_false_p3 x__l_false_m2__l_true_m3 x__l_false_m2__l_true_m2 x__l_false_m2__l_true_m1 x__l_false_m2__l_true_0 x__l_false_m2__l_true_p1 x__l_false_m2__l_true_p2 x__l_false_m2__l_true_p3 x__l_false_m2__l_false_m2 x__l_false_m2__l_false_m1 x__l_false_m2__l_false_0 x__l_false_m2__l_false_p1 x__l_false_m2__l_false_p2 x__l_false_m2__l_false_p3 x__l_false_m1__l_true_m3 x__l_false_m1__l_true_m2 x__l_false_m1__l_true_m1 x__l_false_m1__l_true_0 x__l_false_m1__l_true_p1 x__l_false_m1__l_true_p2 x__l_false_m1__l_true_p3 x__l_false_m1__l_false_m1 x__l_false_m1__l_false_0 x__l_false_m1__l_false_p1 x__l_false_m1__l_false_p2 x__l_false_m1__l_false_p3 x__l_false_0__l_true_m3 x__l_false_0__l_true_m2 x__l_false_0__l_true_m1 x__l_false_0__l_true_0 x__l_false_0__l_true_p1 x__l_false_0__l_true_p2 x__l_false_0__l_true_p3 x__l_false_0__l_false_0 x__l_false_0__l_false_p1 x__l_false_0__l_false_p2 x__l_false_0__l_false_p3 x__l_false_p1__l_true_m3 x__l_false_p1__l_true_m2 x__l_false_p1__l_true_m1 x__l_false_p1__l_true_0 x__l_false_p1__l_true_p1 x__l_false_p1__l_true_p2 x__l_false_p1__l_true_p3 x__l_false_p1__l_false_p1 x__l_false_p1__l_false_p2 x__l_false_p1__l_false_p3 x__l_false_p2__l_true_m3 x__l_false_p2__l_true_m2 x__l_false_p2__l_true_m1 x__l_false_p2__l_true_0 x__l_false_p2__l_true_p1 x__l_false_p2__l_true_p2 x__l_false_p2__l_true_p3 x__l_false_p2__l_false_p2 x__l_false_p2__l_false_p3 x__l_false_p3__l_true_m3 x__l_false_p3__l_true_m2 x__l_false_p3__l_true_m1 x__l_false_p3__l_true_0 x__l_false_p3__l_true_p1 x__l_false_p3__l_true_p2 x__l_false_p3__l_true_p3 x__l_false_p3__l_false_p3 x__nl_true_m3__l_true_m2 x__nl_true_m3__l_true_m1 x__nl_true_m3__l_true_0 x__nl_true_m3__l_true_p1 x__nl_true_m3__l_true_p2 x__nl_true_m3__l_true_p3 x__nl_true_m3__l_false_m3 x__nl_true_m3__l_false_m2 x__nl_true_m3__l_false_m1 x__nl_true_m3__l_false_0 x__nl_true_m3__l_false_p1 x__nl_true_m3__l_false_p2 x__nl_true_m3__l_false_p3 x__nl_true_m2__l_true_m2 x__nl_true_m2__l_true_m1 x__nl_true_m2__l_true_0 x__nl_true_m2__l_true_p1 x__nl_true_m2__l_true_p2 x__nl_true_m2__l_true_p3 x__nl_true_m2__l_false_m3 x__nl_true_m2__l_false_m2 x__nl_true_m2__l_false_m1 x__nl_true_m2__l_false_0 x__nl_true_m2__l_false_p1 x__nl_true_m2__l_false_p2 x__nl_true_m2__l_false_p3 x__nl_true_m1__l_true_m2 x__nl_true_m1__l_true_m1 x__nl_true_m1__l_true_0 x__nl_true_m1__l_true_p1 x__nl_true_m1__l_true_p2 x__nl_true_m1__l_true_p3 x__nl_true_m1__l_false_m3 x__nl_true_m1__l_false_m2 x__nl_true_m1__l_false_m1 x__nl_true_m1__l_false_0 x__nl_true_m1__l_false_p1 x__nl_true_m1__l_false_p2 x__nl_true_m1__l_false_p3 x__nl_true_0__l_true_p1 x__nl_true_0__l_true_p2 x__nl_true_0__l_true_p3 x__nl_true_0__l_false_m3 x__nl_true_0__l_false_m2 x__nl_true_0__l_false_m1 x__nl_true_0__l_false_0 x__nl_true_0__l_false_p1 x__nl_true_0__l_false_p2 x__nl_true_0__l_false_p3 x__nl_true_p1__l_true_m3 x__nl_true_p1__l_true_m2 x__nl_true_p1__l_true_m1 x__nl_true_p1__l_true_0 x__nl_true_p1__l_true_p1 x__nl_true_p1__l_true_p2 x__nl_true_p1__l_true_p3 x__nl_true_p1__l_false_m3 x__nl_true_p1__l_false_m2 x__nl_true_p1__l_false_m1 x__nl_true_p1__l_false_0 x__nl_true_p1__l_false_p1 x__nl_true_p1__l_false_p2 x__nl_true_p1__l_false_p3 x__nl_true_p2__l_true_m3 x__nl_true_p2__l_true_m2 x__nl_true_p2__l_true_m1 x__nl_true_p2__l_true_0 x__nl_true_p2__l_true_p1 x__nl_true_p2__l_true_p2 x__nl_true_p2__l_true_p3 x__nl_true_p2__l_false_m3 x__nl_true_p2__l_false_m2 x__nl_true_p2__l_false_m1 x__nl_true_p2__l_false_0 x__nl_true_p2__l_false_p1 x__nl_true_p2__l_false_p2 x__nl_true_p2__l_false_p3 x__nl_true_p3__l_true_m3 x__nl_true_p3__l_true_m2 x__nl_true_p3__l_true_m1 x__nl_true_p3__l_true_0 x__nl_true_p3__l_true_p1 x__nl_true_p3__l_true_p2 x__nl_true_p3__l_true_p3 x__nl_true_p3__l_false_m3 x__nl_true_p3__l_false_m2 x__nl_true_p3__l_false_m1 x__nl_true_p3__l_false_0 x__nl_true_p3__l_false_p1 x__nl_true_p3__l_false_p2 x__nl_true_p3__l_false_p3 x__nl_false_m3__l_true_m3 x__nl_false_m3__l_true_m2 x__nl_false_m3__l_true_m1 x__nl_false_m3__l_true_0 x__nl_false_m3__l_true_p1 x__nl_false_m3__l_true_p2 x__nl_false_m3__l_true_p3 x__nl_false_m3__l_false_m3 x__nl_false_m3__l_false_m2 x__nl_false_m3__l_false_m1 x__nl_false_m3__l_false_0 x__nl_false_m3__l_false_p1 x__nl_false_m3__l_false_p2 x__nl_false_m3__l_false_p3 x__nl_false_m2__l_true_m3 x__nl_false_m2__l_true_m2 x__nl_false_m2__l_true_m1 x__nl_false_m2__l_true_0 x__nl_false_m2__l_true_p1 x__nl_false_m2__l_true_p2 x__nl_false_m2__l_true_p3 x__nl_false_m2__l_false_m3 x__nl_false_m2__l_false_m2 x__nl_false_m2__l_false_m1 x__nl_false_m2__l_false_0 x__nl_false_m2__l_false_p1 x__nl_false_m2__l_false_p2 x__nl_false_m2__l_false_p3 x__nl_false_m1__l_true_m3 x__nl_false_m1__l_true_m2 x__nl_false_m1__l_true_m1 x__nl_false_m1__l_true_0 x__nl_false_m1__l_true_p1 x__nl_false_m1__l_true_p2 x__nl_false_m1__l_true_p3 x__nl_false_m1__l_false_m3 x__nl_false_m1__l_false_m2 x__nl_false_m1__l_false_m1 x__nl_false_m1__l_false_0 x__nl_false_m1__l_false_p1 x__nl_false_m1__l_false_p2 x__nl_false_m1__l_false_p3 x__nl_false_0__l_true_m3 x__nl_false_0__l_true_m2 x__nl_false_0__l_true_m1 x__nl_false_0__l_true_0 x__nl_false_0__l_true_p1 x__nl_false_0__l_true_p2 x__nl_false_0__l_true_p3 x__nl_false_0__l_false_m3 x__nl_false_0__l_false_m2 x__nl_false_0__l_false_m1 x__nl_false_0__l_false_0 x__nl_false_p1__l_true_m3 x__nl_false_p1__l_true_m2 x__nl_false_p1__l_true_m1 x__nl_false_p1__l_true_0 x__nl_false_p1__l_true_p1 x__nl_false_p1__l_true_p2 x__nl_false_p1__l_true_p3 x__nl_false_p1__l_false_m3 x__nl_false_p1__l_false_m2 x__nl_false_p1__l_false_m1 x__nl_false_p1__l_false_0 x__nl_false_p1__l_false_p1 x__nl_false_p1__l_false_p2 x__nl_false_p2__l_true_m3 x__nl_false_p2__l_true_m2 x__nl_false_p2__l_true_m1 x__nl_false_p2__l_true_0 x__nl_false_p2__l_true_p1 x__nl_false_p2__l_true_p2 x__nl_false_p2__l_true_p3 x__nl_false_p2__l_false_m3 x__nl_false_p2__l_false_m2 x__nl_false_p2__l_false_m1 x__nl_false_p2__l_false_0 x__nl_false_p2__l_false_p1 x__nl_false_p2__l_false_p2 x__nl_false_p3__l_true_m3 x__nl_false_p3__l_true_m2 x__nl_false_p3__l_true_m1 x__nl_false_p3__l_true_0 x__nl_false_p3__l_true_p1 x__nl_false_p3__l_true_p2 x__nl_false_p3__l_true_p3 x__nl_false_p3__l_false_m3 x__nl_false_p3__l_false_m2 x__nl_false_p3__l_false_m1 x__nl_false_p3__l_false_0 x__nl_false_p3__l_false_p1 x__nl_false_p3__l_false_p2 }
    arcs {
       { _l_true_m3, _l_true_m3 } -> x__l_true_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
       { _l_true_m3, _l_true_m2 } -> x__l_true_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
       { _l_true_m3, _l_true_m1 } -> x__l_true_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
       { _l_true_m3, _l_true_0 } -> x__l_true_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
       { _l_true_m3, _l_true_p1 } -> x__l_true_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
       { _l_true_m3, _l_true_p2 } -> x__l_true_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
       { _l_true_m3, _l_true_p3 } -> x__l_true_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
       { _l_true_m2, _l_true_m2 } -> x__l_true_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
       { _l_true_m2, _l_true_m1 } -> x__l_true_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
       { _l_true_m2, _l_true_0 } -> x__l_true_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
       { _l_true_m2, _l_true_p1 } -> x__l_true_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
       { _l_true_m2, _l_true_p2 } -> x__l_true_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
       { _l_true_m2, _l_true_p3 } -> x__l_true_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
       { _l_true_m1, _l_true_m1 } -> x__l_true_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
       { _l_true_m1, _l_true_0 } -> x__l_true_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
       { _l_true_m1, _l_true_p1 } -> x__l_true_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
       { _l_true_m1, _l_true_p2 } -> x__l_true_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
       { _l_true_m1, _l_true_p3 } -> x__l_true_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
       { _l_true_0, _l_true_0 } -> x__l_true_0__l_true_0 -> { _l_true_0, _nl_true_0 }
       { _l_true_0, _l_true_p1 } -> x__l_true_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
       { _l_true_0, _l_true_p2 } -> x__l_true_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
       { _l_true_0, _l_true_p3 } -> x__l_true_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
       { _l_true_p1, _l_true_p1 } -> x__l_true_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
       { _l_true_p1, _l_true_p2 } -> x__l_true_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
       { _l_true_p1, _l_true_p3 } -> x__l_true_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
       { _l_true_p2, _l_true_p2 } -> x__l_true_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
       { _l_true_p2, _l_true_p3 } -> x__l_true_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
       { _l_true_p3, _l_true_p3 } -> x__l_true_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
       { _l_false_m3, _l_true_m3 } -> x__l_false_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
       { _l_false_m3, _l_true_m2 } -> x__l_false_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
       { _l_false_m3, _l_true_m1 } -> x__l_false_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
       { _l_false_m3, _l_true_0 } -> x__l_false_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
       { _l_false_m3, _l_true_p1 } -> x__l_false_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m3, _l_true_p2 } -> x__l_false_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m3, _l_true_p3 } -> x__l_false_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
       { _l_false_m3, _l_false_m3 } -> x__l_false_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
       { _l_false_m3, _l_false_m2 } -> x__l_false_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
       { _l_false_m3, _l_false_m1 } -> x__l_false_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
       { _l_false_m3, _l_false_0 } -> x__l_false_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
       { _l_false_m3, _l_false_p1 } -> x__l_false_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m3, _l_false_p2 } -> x__l_false_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m3, _l_false_p3 } -> x__l_false_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
       { _l_false_m2, _l_true_m3 } -> x__l_false_m2__l_true_m3 -> { _l_true_m3, _nl_true_m2 }
       { _l_false_m2, _l_true_m2 } -> x__l_false_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
       { _l_false_m2, _l_true_m1 } -> x__l_false_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
       { _l_false_m2, _l_true_0 } -> x__l_false_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m2, _l_true_p1 } -> x__l_false_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m2, _l_true_p2 } -> x__l_false_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
       { _l_false_m2, _l_true_p3 } -> x__l_false_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
       { _l_false_m2, _l_false_m2 } -> x__l_false_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
       { _l_false_m2, _l_false_m1 } -> x__l_false_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
       { _l_false_m2, _l_false_0 } -> x__l_false_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m2, _l_false_p1 } -> x__l_false_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m2, _l_false_p2 } -> x__l_false_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
       { _l_false_m2, _l_false_p3 } -> x__l_false_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
       { _l_false_m1, _l_true_m3 } -> x__l_false_m1__l_true_m3 -> { _l_true_m3, _nl_true_m1 }
       { _l_false_m1, _l_true_m2 } -> x__l_false_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
       { _l_false_m1, _l_true_m1 } -> x__l_false_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m1, _l_true_0 } -> x__l_false_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m1, _l_true_p1 } -> x__l_false_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
       { _l_false_m1, _l_true_p2 } -> x__l_false_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
       { _l_false_m1, _l_true_p3 } -> x__l_false_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
       { _l_false_m1, _l_false_m1 } -> x__l_false_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
       { _l_false_m1, _l_false_0 } -> x__l_false_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
       { _l_false_m1, _l_false_p1 } -> x__l_false_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
       { _l_false_m1, _l_false_p2 } -> x__l_false_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
       { _l_false_m1, _l_false_p3 } -> x__l_false_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
       { _l_false_0, _l_true_m3 } -> x__l_false_0__l_true_m3 -> { _l_true_m3, _nl_true_0 }
       { _l_false_0, _l_true_m2 } -> x__l_false_0__l_true_m2 -> { _l_true_m2, _nl_true_0 }
       { _l_false_0, _l_true_m1 } -> x__l_false_0__l_true_m1 -> { _l_true_m1, _nl_true_0 }
       { _l_false_0, _l_true_0 } -> x__l_false_0__l_true_0 -> { _l_true_0, _nl_true_0 }
       { _l_false_0, _l_true_p1 } -> x__l_false_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
       { _l_false_0, _l_true_p2 } -> x__l_false_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
       { _l_false_0, _l_true_p3 } -> x__l_false_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
       { _l_false_0, _l_false_0 } -> x__l_false_0__l_false_0 -> { _l_true_0, _nl_true_0 }
       { _l_false_0, _l_false_p1 } -> x__l_false_0__l_false_p1 -> { _l_false_p1, _nl_false_0 }
       { _l_false_0, _l_false_p2 } -> x__l_false_0__l_false_p2 -> { _l_false_p2, _nl_false_0 }
       { _l_false_0, _l_false_p3 } -> x__l_false_0__l_false_p3 -> { _l_false_p3, _nl_false_0 }
       { _l_false_p1, _l_true_m3 } -> x__l_false_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
       { _l_false_p1, _l_true_m2 } -> x__l_false_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
       { _l_false_p1, _l_true_m1 } -> x__l_false_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
       { _l_false_p1, _l_true_0 } -> x__l_false_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
       { _l_false_p1, _l_true_p1 } -> x__l_false_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
       { _l_false_p1, _l_true_p2 } -> x__l_false_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
       { _l_false_p1, _l_true_p3 } -> x__l_false_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
       { _l_false_p1, _l_false_p1 } -> x__l_false_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
       { _l_false_p1, _l_false_p2 } -> x__l_false_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
       { _l_false_p1, _l_false_p3 } -> x__l_false_p1__l_false_p3 -> { _l_false_p3, _nl_false_p1 }
       { _l_false_p2, _l_true_m3 } -> x__l_false_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
       { _l_false_p2, _l_true_m2 } -> x__l_false_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
       { _l_false_p2, _l_true_m1 } -> x__l_false_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
       { _l_false_p2, _l_true_0 } -> x__l_false_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
       { _l_false_p2, _l_true_p1 } -> x__l_false_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
       { _l_false_p2, _l_true_p2 } -> x__l_false_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
       { _l_false_p2, _l_true_p3 } -> x__l_false_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
       { _l_false_p2, _l_false_p2 } -> x__l_false_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
       { _l_false_p2, _l_false_p3 } -> x__l_false_p2__l_false_p3 -> { _l_false_p3, _nl_false_p2 }
       { _l_false_p3, _l_true_m3 } -> x__l_false_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
       { _l_false_p3, _l_true_m2 } -> x__l_false_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
       { _l_false_p3, _l_true_m1 } -> x__l_false_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
       { _l_false_p3, _l_true_0 } -> x__l_false_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
       { _l_false_p3, _l_true_p1 } -> x__l_false_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
       { _l_false_p3, _l_true_p2 } -> x__l_false_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
       { _l_false_p3, _l_true_p3 } -> x__l_false_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
       { _l_false_p3, _l_false_p3 } -> x__l_false_p3__l_false_p3 -> { _l_false_p3, _nl_false_p3 }
       { _nl_true_m3, _l_true_m2 } -> x__nl_true_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
       { _nl_true_m3, _l_true_m1 } -> x__nl_true_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
       { _nl_true_m3, _l_true_0 } -> x__nl_true_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m3, _l_true_p1 } -> x__nl_true_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m3, _l_true_p2 } -> x__nl_true_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m3, _l_true_p3 } -> x__nl_true_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m3, _l_false_m3 } -> x__nl_true_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
       { _nl_true_m3, _l_false_m2 } -> x__nl_true_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
       { _nl_true_m3, _l_false_m1 } -> x__nl_true_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
       { _nl_true_m3, _l_false_0 } -> x__nl_true_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m3, _l_false_p1 } -> x__nl_true_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m3, _l_false_p2 } -> x__nl_true_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m3, _l_false_p3 } -> x__nl_true_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m2, _l_true_m2 } -> x__nl_true_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
       { _nl_true_m2, _l_true_m1 } -> x__nl_true_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m2, _l_true_0 } -> x__nl_true_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m2, _l_true_p1 } -> x__nl_true_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m2, _l_true_p2 } -> x__nl_true_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m2, _l_true_p3 } -> x__nl_true_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_m2, _l_false_m3 } -> x__nl_true_m2__l_false_m3 -> { _l_true_m3, _nl_true_m2 }
       { _nl_true_m2, _l_false_m2 } -> x__nl_true_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
       { _nl_true_m2, _l_false_m1 } -> x__nl_true_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m2, _l_false_0 } -> x__nl_true_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m2, _l_false_p1 } -> x__nl_true_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m2, _l_false_p2 } -> x__nl_true_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m2, _l_false_p3 } -> x__nl_true_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_m1, _l_true_m2 } -> x__nl_true_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m1, _l_true_m1 } -> x__nl_true_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m1, _l_true_0 } -> x__nl_true_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m1, _l_true_p1 } -> x__nl_true_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m1, _l_true_p2 } -> x__nl_true_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_m1, _l_true_p3 } -> x__nl_true_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_m1, _l_false_m3 } -> x__nl_true_m1__l_false_m3 -> { _l_true_m3, _nl_true_m1 }
       { _nl_true_m1, _l_false_m2 } -> x__nl_true_m1__l_false_m2 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_m1, _l_false_m1 } -> x__nl_true_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_m1, _l_false_0 } -> x__nl_true_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_m1, _l_false_p1 } -> x__nl_true_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
       { _nl_true_m1, _l_false_p2 } -> x__nl_true_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_m1, _l_false_p3 } -> x__nl_true_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_0, _l_true_p1 } -> x__nl_true_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_0, _l_true_p2 } -> x__nl_true_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_0, _l_true_p3 } -> x__nl_true_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_0, _l_false_m3 } -> x__nl_true_0__l_false_m3 -> { _l_true_m3, _nl_true_0 }
       { _nl_true_0, _l_false_m2 } -> x__nl_true_0__l_false_m2 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_0, _l_false_m1 } -> x__nl_true_0__l_false_m1 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_0, _l_false_0 } -> x__nl_true_0__l_false_0 -> { _l_true_0, _nl_true_0 }
       { _nl_true_0, _l_false_p1 } -> x__nl_true_0__l_false_p1 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_0, _l_false_p2 } -> x__nl_true_0__l_false_p2 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_0, _l_false_p3 } -> x__nl_true_0__l_false_p3 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p1, _l_true_m3 } -> x__nl_true_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_p1, _l_true_m2 } -> x__nl_true_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_p1, _l_true_m1 } -> x__nl_true_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p1, _l_true_0 } -> x__nl_true_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p1, _l_true_p1 } -> x__nl_true_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p1, _l_true_p2 } -> x__nl_true_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p1, _l_true_p3 } -> x__nl_true_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p1, _l_false_m3 } -> x__nl_true_p1__l_false_m3 -> { _l_true_m2, _nl_true_0 }
       { _nl_true_p1, _l_false_m2 } -> x__nl_true_p1__l_false_m2 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_p1, _l_false_m1 } -> x__nl_true_p1__l_false_m1 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p1, _l_false_0 } -> x__nl_true_p1__l_false_0 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p1, _l_false_p1 } -> x__nl_true_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p1, _l_false_p2 } -> x__nl_true_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p1, _l_false_p3 } -> x__nl_true_p1__l_false_p3 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p2, _l_true_m3 } -> x__nl_true_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_p2, _l_true_m2 } -> x__nl_true_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p2, _l_true_m1 } -> x__nl_true_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p2, _l_true_0 } -> x__nl_true_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p2, _l_true_p1 } -> x__nl_true_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p2, _l_true_p2 } -> x__nl_true_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p2, _l_true_p3 } -> x__nl_true_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
       { _nl_true_p2, _l_false_m3 } -> x__nl_true_p2__l_false_m3 -> { _l_true_m1, _nl_true_0 }
       { _nl_true_p2, _l_false_m2 } -> x__nl_true_p2__l_false_m2 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p2, _l_false_m1 } -> x__nl_true_p2__l_false_m1 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p2, _l_false_0 } -> x__nl_true_p2__l_false_0 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p2, _l_false_p1 } -> x__nl_true_p2__l_false_p1 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p2, _l_false_p2 } -> x__nl_true_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p2, _l_false_p3 } -> x__nl_true_p2__l_false_p3 -> { _l_false_p3, _nl_false_p2 }
       { _nl_true_p3, _l_true_m3 } -> x__nl_true_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p3, _l_true_m2 } -> x__nl_true_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p3, _l_true_m1 } -> x__nl_true_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p3, _l_true_0 } -> x__nl_true_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p3, _l_true_p1 } -> x__nl_true_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p3, _l_true_p2 } -> x__nl_true_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
       { _nl_true_p3, _l_true_p3 } -> x__nl_true_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
       { _nl_true_p3, _l_false_m3 } -> x__nl_true_p3__l_false_m3 -> { _l_true_0, _nl_true_0 }
       { _nl_true_p3, _l_false_m2 } -> x__nl_true_p3__l_false_m2 -> { _l_false_p1, _nl_false_0 }
       { _nl_true_p3, _l_false_m1 } -> x__nl_true_p3__l_false_m1 -> { _l_false_p2, _nl_false_0 }
       { _nl_true_p3, _l_false_0 } -> x__nl_true_p3__l_false_0 -> { _l_false_p3, _nl_false_0 }
       { _nl_true_p3, _l_false_p1 } -> x__nl_true_p3__l_false_p1 -> { _l_false_p3, _nl_false_p1 }
       { _nl_true_p3, _l_false_p2 } -> x__nl_true_p3__l_false_p2 -> { _l_false_p3, _nl_false_p2 }
       { _nl_true_p3, _l_false_p3 } -> x__nl_true_p3__l_false_p3 -> { _l_false_p3, _nl_false_p3 }
       { _nl_false_m3, _l_true_m3 } -> x__nl_false_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
       { _nl_false_m3, _l_true_m2 } -> x__nl_false_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
       { _nl_false_m3, _l_true_m1 } -> x__nl_false_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m3, _l_true_0 } -> x__nl_false_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m3, _l_true_p1 } -> x__nl_false_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m3, _l_true_p2 } -> x__nl_false_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m3, _l_true_p3 } -> x__nl_false_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m3, _l_false_m3 } -> x__nl_false_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
       { _nl_false_m3, _l_false_m2 } -> x__nl_false_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
       { _nl_false_m3, _l_false_m1 } -> x__nl_false_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m3, _l_false_0 } -> x__nl_false_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m3, _l_false_p1 } -> x__nl_false_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m3, _l_false_p2 } -> x__nl_false_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m3, _l_false_p3 } -> x__nl_false_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m2, _l_true_m3 } -> x__nl_false_m2__l_true_m3 -> { _l_true_m3, _nl_true_m2 }
       { _nl_false_m2, _l_true_m2 } -> x__nl_false_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m2, _l_true_m1 } -> x__nl_false_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m2, _l_true_0 } -> x__nl_false_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m2, _l_true_p1 } -> x__nl_false_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m2, _l_true_p2 } -> x__nl_false_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m2, _l_true_p3 } -> x__nl_false_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_m2, _l_false_m3 } -> x__nl_false_m2__l_false_m3 -> { _l_true_m3, _nl_true_m2 }
       { _nl_false_m2, _l_false_m2 } -> x__nl_false_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m2, _l_false_m1 } -> x__nl_false_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m2, _l_false_0 } -> x__nl_false_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m2, _l_false_p1 } -> x__nl_false_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m2, _l_false_p2 } -> x__nl_false_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m2, _l_false_p3 } -> x__nl_false_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_m1, _l_true_m3 } -> x__nl_false_m1__l_true_m3 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m1, _l_true_m2 } -> x__nl_false_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m1, _l_true_m1 } -> x__nl_false_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m1, _l_true_0 } -> x__nl_false_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m1, _l_true_p1 } -> x__nl_false_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m1, _l_true_p2 } -> x__nl_false_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_m1, _l_true_p3 } -> x__nl_false_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_m1, _l_false_m3 } -> x__nl_false_m1__l_false_m3 -> { _l_true_m3, _nl_true_m1 }
       { _nl_false_m1, _l_false_m2 } -> x__nl_false_m1__l_false_m2 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_m1, _l_false_m1 } -> x__nl_false_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_m1, _l_false_0 } -> x__nl_false_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_m1, _l_false_p1 } -> x__nl_false_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
       { _nl_false_m1, _l_false_p2 } -> x__nl_false_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_m1, _l_false_p3 } -> x__nl_false_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_0, _l_true_m3 } -> x__nl_false_0__l_true_m3 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_0, _l_true_m2 } -> x__nl_false_0__l_true_m2 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_0, _l_true_m1 } -> x__nl_false_0__l_true_m1 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_0, _l_true_0 } -> x__nl_false_0__l_true_0 -> { _l_true_0, _nl_true_0 }
       { _nl_false_0, _l_true_p1 } -> x__nl_false_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_0, _l_true_p2 } -> x__nl_false_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_0, _l_true_p3 } -> x__nl_false_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_0, _l_false_m3 } -> x__nl_false_0__l_false_m3 -> { _l_true_m3, _nl_true_0 }
       { _nl_false_0, _l_false_m2 } -> x__nl_false_0__l_false_m2 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_0, _l_false_m1 } -> x__nl_false_0__l_false_m1 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_0, _l_false_0 } -> x__nl_false_0__l_false_0 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p1, _l_true_m3 } -> x__nl_false_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_p1, _l_true_m2 } -> x__nl_false_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_p1, _l_true_m1 } -> x__nl_false_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p1, _l_true_0 } -> x__nl_false_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p1, _l_true_p1 } -> x__nl_false_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p1, _l_true_p2 } -> x__nl_false_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p1, _l_true_p3 } -> x__nl_false_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
       { _nl_false_p1, _l_false_m3 } -> x__nl_false_p1__l_false_m3 -> { _l_true_m2, _nl_true_0 }
       { _nl_false_p1, _l_false_m2 } -> x__nl_false_p1__l_false_m2 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_p1, _l_false_m1 } -> x__nl_false_p1__l_false_m1 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p1, _l_false_0 } -> x__nl_false_p1__l_false_0 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p1, _l_false_p1 } -> x__nl_false_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p1, _l_false_p2 } -> x__nl_false_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p2, _l_true_m3 } -> x__nl_false_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_p2, _l_true_m2 } -> x__nl_false_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p2, _l_true_m1 } -> x__nl_false_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p2, _l_true_0 } -> x__nl_false_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p2, _l_true_p1 } -> x__nl_false_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p2, _l_true_p2 } -> x__nl_false_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
       { _nl_false_p2, _l_true_p3 } -> x__nl_false_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
       { _nl_false_p2, _l_false_m3 } -> x__nl_false_p2__l_false_m3 -> { _l_true_m1, _nl_true_0 }
       { _nl_false_p2, _l_false_m2 } -> x__nl_false_p2__l_false_m2 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p2, _l_false_m1 } -> x__nl_false_p2__l_false_m1 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p2, _l_false_0 } -> x__nl_false_p2__l_false_0 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p2, _l_false_p1 } -> x__nl_false_p2__l_false_p1 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p2, _l_false_p2 } -> x__nl_false_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
       { _nl_false_p3, _l_true_m3 } -> x__nl_false_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p3, _l_true_m2 } -> x__nl_false_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p3, _l_true_m1 } -> x__nl_false_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p3, _l_true_0 } -> x__nl_false_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p3, _l_true_p1 } -> x__nl_false_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
       { _nl_false_p3, _l_true_p2 } -> x__nl_false_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
       { _nl_false_p3, _l_true_p3 } -> x__nl_false_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
       { _nl_false_p3, _l_false_m3 } -> x__nl_false_p3__l_false_m3 -> { _l_true_0, _nl_true_0 }
       { _nl_false_p3, _l_false_m2 } -> x__nl_false_p3__l_false_m2 -> { _l_false_p1, _nl_false_0 }
       { _nl_false_p3, _l_false_m1 } -> x__nl_false_p3__l_false_m1 -> { _l_false_p2, _nl_false_0 }
       { _nl_false_p3, _l_false_0 } -> x__nl_false_p3__l_false_0 -> { _l_false_p3, _nl_false_0 }
       { _nl_false_p3, _l_false_p1 } -> x__nl_false_p3__l_false_p1 -> { _l_false_p3, _nl_false_p1 }
       { _nl_false_p3, _l_false_p2 } -> x__nl_false_p3__l_false_p2 -> { _l_false_p3, _nl_false_p2 }
    }
    initial {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3}
    true {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _nl_true_m3 _nl_true_m2 _nl_true_m1 _nl_true_0 _nl_true_p1 _nl_true_p2 _nl_true_p3}
    false {_l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3 _nl_false_m3 _nl_false_m2 _nl_false_m1 _nl_false_0 _nl_false_p1 _nl_false_p2 _nl_false_p3}
}