TRS: { rev(nil()) -> nil(), rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)), rev1(0(), nil()) -> 0(), rev1(s(x), nil()) -> s(x), rev1(x, cons(y, l)) -> rev1(y, l), rev2(x, nil()) -> nil(), rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))} Fail