(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS maxlength))
(VAR ls m l h n)
(RULES
maxlength(ls, m, l) -> Com_2(max(ls, 0, m), len(ls, l))
len(xs, l) -> len(t, l - 1) :|: xs = h :: t
len([], 0) -> c(0)
max(xs, n, m) -> max(t, n, m) :|: h >= n && xs = h :: t
max([], m, m) -> c(0)
max(xs, n, m) -> max(t, h, m) :|: h > n && xs = h :: t
)