(VAR a a_4 l l' l1 l1_2 l2 l2_1 l_3 l_5 x x_0 y )
(RULES 
        test(x_0, y) -> True
        test(x_0, y) -> False
        append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
        match_0(l1_2, l2_1, Nil) -> l2_1
        match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
        part(a_4, l_3) -> match_1(a_4, l_3, l_3)
        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'))
        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, False) -> Pair(Cons(x, l1), l2)
        match_3(l1, l2, x, l', a_4, l_3, True) -> Pair(l1, Cons(x, l2))
        quick(l_5) -> match_4(l_5, l_5)
        match_4(l_5, Nil) -> Nil
        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)))
        
)