MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { Tl(O(x), y) -> Wr(check(x), y) , Tl(O(x), y) -> Wr(x, check(y)) , Tl(N(x), y) -> Wr(check(x), y) , Tl(N(x), y) -> Wr(x, check(y)) , Tr(x, O(y)) -> Wl(check(x), y) , Tr(x, O(y)) -> Wl(x, check(y)) , Tr(x, N(y)) -> Wl(check(x), y) , Tr(x, N(y)) -> Wl(x, check(y)) , Tl(B(), y) -> Wr(check(B()), y) , Tl(B(), y) -> Wr(B(), check(y)) , Tr(x, B()) -> Wl(check(x), B()) , Tr(x, B()) -> Wl(x, check(B()))} Weak Rules: { Tl(O(x), y) -> Wl(check(x), y) , Tl(O(x), y) -> Wl(x, check(y)) , Tl(N(x), y) -> Wl(check(x), y) , Tl(N(x), y) -> Wl(x, check(y)) , Tr(x, O(y)) -> Wr(check(x), y) , Tr(x, O(y)) -> Wr(x, check(y)) , Tr(x, N(y)) -> Wr(check(x), y) , Tr(x, N(y)) -> Wr(x, check(y)) , B() -> N(B()) , check(O(x)) -> ok(O(x)) , Wl(ok(x), y) -> Tl(x, y) , Wl(x, ok(y)) -> Tl(x, y) , Wr(ok(x), y) -> Tr(x, y) , Wr(x, ok(y)) -> Tr(x, y) , check(O(x)) -> O(check(x)) , check(N(x)) -> N(check(x)) , O(ok(x)) -> ok(O(x)) , N(ok(x)) -> ok(N(x))} Proof Output: The input cannot be shown compatible