YES
Time: 0.017949
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')))}
   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_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:
     {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 (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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [match_3](x0, x1, x2, x3, x4, x5, x6) = x0 + x1 + 1,
       
       [match_2](x0, x1, x2, x3, x4) = x0 + 1,
       
       [match_5](x0, x1, x2, x3) = 0,
       
       [match_0](x0, x1, x2) = 0,
       
       [match_1](x0, x1, x2) = x0,
       
       [test](x0, x1) = 0,
       
       [append](x0, x1) = x0,
       
       [Cons](x0, x1) = x0 + 1,
       
       [part](x0, x1) = x0,
       
       [Pair](x0, x1) = x0 + x1,
       
       [match_4](x0, x1) = 0,
       
       [quick](x0) = 1,
       
       [True] = 0,
       
       [False] = 0,
       
       [Nil] = 0,
       
       [match_5#](x0, x1, x2, x3) = x0,
       
       [match_4#](x0, x1) = x0,
       
       [quick#](x0) = x0
      Strict:
       match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2
       0 + 0l' + 1l1 + 1l2 + 0l_5 + 0a >= 0 + 1l2
       match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1
       0 + 0l' + 1l1 + 1l2 + 0l_5 + 0a >= 0 + 1l1
       quick# l_5 -> match_4#(l_5, l_5)
       0 + 1l_5 >= 0 + 1l_5
       match_4#(l_5, Cons(a, l')) -> match_5#(a, l', l_5, part(a, l'))
       1 + 1l' + 0l_5 + 0a >= 0 + 1l' + 0l_5 + 0a
      Weak:
       
     EDG:
      {(match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l1, quick# l_5 -> match_4#(l_5, l_5))
       (match_5#(a, l', l_5, Pair(l1, l2)) -> quick# l2, quick# l_5 -> match_4#(l_5, l_5))}
      SCCS (0):
       
       Qed
   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))}
    SPSC:
     Simple Projection:
      pi(part#) = 1, pi(match_1#) = 2
     Strict:
      {part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)}
     EDG:
      {}
      SCCS (0):
       
       Qed
   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))}
    SPSC:
     Simple Projection:
      pi(append#) = 0, pi(match_0#) = 2
     Strict:
      {append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)}
     EDG:
      {}
      SCCS (0):
       
       Qed