MAYBE 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { isEmpty(empty()) -> true() , isEmpty(node(l, x, r)) -> false() , left(empty()) -> empty() , left(node(l, x, r)) -> l , right(empty()) -> empty() , right(node(l, x, r)) -> r , elem(node(l, x, r)) -> x , append(nil(), x) -> cons(x, nil()) , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) , listify(n, xs) -> if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n)) , if(true(), b, n, m, xs, ys) -> xs , if(false(), false(), n, m, xs, ys) -> listify(m, xs) , if(false(), true(), n, m, xs, ys) -> listify(n, ys) , toList(n) -> listify(n, nil())} Proof Output: The input cannot be shown compatible