MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { gcd(x, y) -> gcd2(x, y, 0()) , gcd2(x, y, i) -> if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i)) , if1(true(), b1, b2, b3, x, y, i) -> pair(result(y), neededIterations(i)) , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i) , if2(true(), b2, b3, x, y, i) -> pair(result(x), neededIterations(i)) , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i) , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i) , if3(true(), b3, x, y, i) -> if4(b3, x, y, i) , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i) , if4(true(), x, y, i) -> pair(result(x), neededIterations(i)) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , le(s(x), 0()) -> false() , le(0(), y) -> true() , le(s(x), s(y)) -> le(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , a() -> b() , a() -> c()} Proof Output: The input cannot be shown compatible