MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { T(ok(sys(x, p(d, 0()), r(0()), y))) -> T(check(sys(x, bot(), r(1()), y))) , T(ok(sys(x, p(d, 1()), r(1()), y))) -> T(check(sys(x, bot(), r(0()), y)))} Weak Rules: { T(ok(sys(S(0(), c(d, ds)), bot(), y, z))) -> T(check(sys(S(0(), c(d, ds)), p(d, 0()), y, z))) , T(ok(sys(S(1(), c(d, ds)), bot(), y, z))) -> T(check(sys(S(0(), c(d, ds)), p(d, 1()), y, z))) , T(ok(sys(S(0(), c(d, ds)), x, y, f(0())))) -> T(check(sys(S(1(), ds), x, y, bot()))) , T(ok(sys(S(1(), c(d, ds)), x, y, f(1())))) -> T(check(sys(S(0(), ds), x, y, bot()))) , T(ok(sys(x, y, r(0()), bot()))) -> T(check(sys(x, y, r(0()), f(1())))) , T(ok(sys(x, y, r(1()), bot()))) -> T(check(sys(x, y, r(1()), f(0())))) , nils() -> c(new(), nils()) , p(d, b) -> bot() , f(b) -> bot() , check(old()) -> ok(old()) , check(r(v1)) -> r(check(v1)) , r(ok(v1)) -> ok(r(v1)) , check(f(v1)) -> f(check(v1)) , f(ok(v1)) -> ok(f(v1)) , check(p(v1, v2)) -> p(v1, check(v2)) , check(p(v1, v2)) -> p(check(v1), v2) , p(v1, ok(v2)) -> ok(p(v1, v2)) , p(ok(v1), v2) -> ok(p(v1, v2)) , check(c(v1, v2)) -> c(v1, check(v2)) , check(c(v1, v2)) -> c(check(v1), v2) , c(v1, ok(v2)) -> ok(c(v1, v2)) , c(ok(v1), v2) -> ok(c(v1, v2)) , check(S(v1, v2)) -> S(v1, check(v2)) , check(S(v1, v2)) -> S(check(v1), v2) , S(v1, ok(v2)) -> ok(S(v1, v2)) , S(ok(v1), v2) -> ok(S(v1, v2)) , check(sys(v1, v2, v3, v4)) -> sys(v1, v2, v3, check(v4)) , check(sys(v1, v2, v3, v4)) -> sys(v1, v2, check(v3), v4) , check(sys(v1, v2, v3, v4)) -> sys(v1, check(v2), v3, v4) , check(sys(v1, v2, v3, v4)) -> sys(check(v1), v2, v3, v4) , sys(v1, v2, v3, ok(v4)) -> ok(sys(v1, v2, v3, v4)) , sys(v1, v2, ok(v3), v4) -> ok(sys(v1, v2, v3, v4)) , sys(v1, ok(v2), v3, v4) -> ok(sys(v1, v2, v3, v4)) , sys(ok(v1), v2, v3, v4) -> ok(sys(v1, v2, v3, v4))} Proof Output: The input cannot be shown compatible