MAYBE
Time: 0.001525
TRS:
 {                             test(x_0, y) -> True(),
                               test(x_0, y) -> False(),
                 match_0(l1_2, l2_1, Nil()) -> l2_1,
            match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                         append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                   match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()),
             match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')),
                             part(a_4, l_3) -> match_1(a_4, l_3, l_3),
     match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)),
   match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)),
  match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                        match_4(l_5, Nil()) -> Nil(),
                  match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')),
                                  quick l_5 -> match_4(l_5, l_5),
          match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))}
 DP:
  DP:
   {       match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1),
                        append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2),
            match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'),
            match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')),
                            part#(a_4, l_3) -> match_1#(a_4, l_3, l_3),
    match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> test#(a_4, x),
    match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> match_3#(l1, l2, x, l', a_4, l_3, test(a_4, x)),
                 match_4#(l_5, Cons(a, l')) -> part#(a, l'),
                 match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')),
                                 quick# l_5 -> match_4#(l_5, l_5),
         match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2)),
         match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1,
         match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2}
  TRS:
  {                             test(x_0, y) -> True(),
                                test(x_0, y) -> False(),
                  match_0(l1_2, l2_1, Nil()) -> l2_1,
             match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                          append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                    match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()),
              match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')),
                              part(a_4, l_3) -> match_1(a_4, l_3, l_3),
      match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)),
    match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)),
   match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                         match_4(l_5, Nil()) -> Nil(),
                   match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')),
                                   quick l_5 -> match_4(l_5, l_5),
           match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))}
  EDG:
   {(match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2)), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2))
    (match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2, quick# l_5 -> match_4#(l_5, l_5))
    (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2)
    (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1)
    (match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')), match_5#(a, l', l_5, Pair(l1, l2)) -> append#(quick l1, Cons(a, quick l2)))
    (match_4#(l_5, Cons(a, l')) -> part#(a, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3))
    (part#(a_4, l_3) -> match_1#(a_4, l_3, l_3), match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'))
    (part#(a_4, l_3) -> match_1#(a_4, l_3, l_3), match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')))
    (match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3))
    (match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> test#(a_4, x))
    (match_1#(a_4, l_3, Cons(x, l')) -> match_2#(x, l', a_4, l_3, part(a_4, l')), match_2#(x, l', a_4, l_3, Pair(l1, l2)) -> match_3#(l1, l2, x, l', a_4, l_3, test(a_4, x)))
    (append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2), match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1))
    (match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, quick# l_5 -> match_4#(l_5, l_5))
    (match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1), append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2))
    (quick# l_5 -> match_4#(l_5, l_5), match_4#(l_5, Cons(a, l')) -> part#(a, l'))
    (quick# l_5 -> match_4#(l_5, l_5), match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')))}
   STATUS:
    arrows: 0.905325
    SCCS (3):
     Scc:
      {        match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')),
                               quick# l_5 -> match_4#(l_5, l_5),
       match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1,
       match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2}
     Scc:
      {match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1),
                    append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)}
     Scc:
      {match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'),
                       part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)}
     
     SCC (4):
      Strict:
       {        match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l')),
                                quick# l_5 -> match_4#(l_5, l_5),
        match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1,
        match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2}
      Weak:
      {                             test(x_0, y) -> True(),
                                    test(x_0, y) -> False(),
                      match_0(l1_2, l2_1, Nil()) -> l2_1,
                 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                              append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                        match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()),
                  match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')),
                                  part(a_4, l_3) -> match_1(a_4, l_3, l_3),
          match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)),
        match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)),
       match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                             match_4(l_5, Nil()) -> Nil(),
                       match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')),
                                       quick l_5 -> match_4(l_5, l_5),
               match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))}
      Open
     
     SCC (2):
      Strict:
       {match_0#(l1_2, l2_1, Cons(x, l)) -> append#(l, l2_1),
                     append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)}
      Weak:
      {                             test(x_0, y) -> True(),
                                    test(x_0, y) -> False(),
                      match_0(l1_2, l2_1, Nil()) -> l2_1,
                 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                              append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                        match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()),
                  match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')),
                                  part(a_4, l_3) -> match_1(a_4, l_3, l_3),
          match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)),
        match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)),
       match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                             match_4(l_5, Nil()) -> Nil(),
                       match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')),
                                       quick l_5 -> match_4(l_5, l_5),
               match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))}
      Open
     
     SCC (2):
      Strict:
       {match_1#(a_4, l_3, Cons(x, l')) -> part#(a_4, l'),
                        part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)}
      Weak:
      {                             test(x_0, y) -> True(),
                                    test(x_0, y) -> False(),
                      match_0(l1_2, l2_1, Nil()) -> l2_1,
                 match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                              append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                        match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil()),
                  match_1(a_4, l_3, Cons(x, l')) -> match_2(x, l', a_4, l_3, part(a_4, l')),
                                  part(a_4, l_3) -> match_1(a_4, l_3, l_3),
          match_2(x, l', a_4, l_3, Pair(l1, l2)) -> match_3(l1, l2, x, l', a_4, l_3, test(a_4, x)),
        match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2)),
       match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                             match_4(l_5, Nil()) -> Nil(),
                       match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l')),
                                       quick l_5 -> match_4(l_5, l_5),
               match_5(a, l', l_5, Pair(l1, l2)) -> append(quick l1, Cons(a, quick l2))}
      Open