MAYBE 'Pop* (timeout of 60.0 seconds)' -------------------------------- Answer: MAYBE Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { top(north(old(n), e, s, w)) -> top(east(n, e, s, w)) , top(north(new(n), old(e), s, w)) -> top(east(n, old(e), s, w)) , top(north(new(n), e, old(s), w)) -> top(east(n, e, old(s), w)) , top(north(new(n), e, s, old(w))) -> top(east(n, e, s, old(w))) , top(east(n, old(e), s, w)) -> top(south(n, e, s, w)) , top(east(old(n), new(e), s, w)) -> top(south(old(n), e, s, w)) , top(east(n, new(e), old(s), w)) -> top(south(n, e, old(s), w)) , top(east(n, new(e), s, old(w))) -> top(south(n, e, s, old(w))) , top(south(n, e, old(s), w)) -> top(west(n, e, s, w)) , top(south(old(n), e, new(s), w)) -> top(west(old(n), e, s, w)) , top(south(n, old(e), new(s), w)) -> top(west(n, old(e), s, w)) , top(south(n, e, new(s), old(w))) -> top(west(n, e, s, old(w))) , top(west(n, e, s, old(w))) -> top(north(n, e, s, w)) , top(west(old(n), e, s, new(w))) -> top(north(old(n), e, s, w)) , top(west(n, old(e), s, new(w))) -> top(north(n, old(e), s, w)) , top(west(n, e, old(s), new(w))) -> top(north(n, e, old(s), w)) , top(north(bot(), old(e), s, w)) -> top(east(bot(), old(e), s, w)) , top(north(bot(), e, old(s), w)) -> top(east(bot(), e, old(s), w)) , top(north(bot(), e, s, old(w))) -> top(east(bot(), e, s, old(w))) , top(east(old(n), bot(), s, w)) -> top(south(old(n), bot(), s, w)) , top(east(n, bot(), old(s), w)) -> top(south(n, bot(), old(s), w)) , top(east(n, bot(), s, old(w))) -> top(south(n, bot(), s, old(w))) , top(south(old(n), e, bot(), w)) -> top(west(old(n), e, bot(), w)) , top(south(n, old(e), bot(), w)) -> top(west(n, old(e), bot(), w)) , top(south(n, e, bot(), old(w))) -> top(west(n, e, bot(), old(w))) , top(west(old(n), e, s, bot())) -> top(north(old(n), e, s, bot())) , top(west(n, old(e), s, bot())) -> top(north(n, old(e), s, bot())) , top(west(n, e, old(s), bot())) -> top(north(n, e, old(s), bot()))} Weak Rules: { top(north(old(n), e, s, w)) -> top(north(n, e, s, w)) , top(north(new(n), e, s, w)) -> top(north(n, e, s, w)) , top(east(n, old(e), s, w)) -> top(east(n, e, s, w)) , top(east(n, new(e), s, w)) -> top(east(n, e, s, w)) , top(south(n, e, old(s), w)) -> top(south(n, e, s, w)) , top(south(n, e, new(s), w)) -> top(south(n, e, s, w)) , top(west(n, e, s, old(w))) -> top(west(n, e, s, w)) , top(west(n, e, s, new(w))) -> top(west(n, e, s, w)) , bot() -> new(bot())} Proof Output: The input cannot be shown compatible