# MC: formula passed --- (start=1 -> AX(AX(AF(busy=0))))
# MC: formula passed --- AX(AX(AF(busy=0)))