(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 )