MAYBE 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { car(cons(x, l)) -> x , cddr(nil()) -> nil() , cddr(cons(x, nil())) -> nil() , cddr(cons(x, cons(y, l))) -> l , cadr(cons(x, cons(y, l))) -> y , isZero(0()) -> true() , isZero(s(x)) -> false() , plus(x, y) -> ifplus(isZero(x), x, y) , ifplus(true(), x, y) -> y , ifplus(false(), x, y) -> s(plus(p(x), y)) , times(x, y) -> iftimes(isZero(x), x, y) , iftimes(true(), x, y) -> 0() , iftimes(false(), x, y) -> plus(y, times(p(x), y)) , p(s(x)) -> x , p(0()) -> 0() , shorter(nil(), y) -> true() , shorter(cons(x, l), 0()) -> false() , shorter(cons(x, l), s(y)) -> shorter(l, y) , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l) , if(true(), b, l) -> s(0()) , if(false(), b, l) -> if2(b, l) , if2(true(), l) -> car(l) , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))} Proof Output: The input cannot be shown compatible