ltl  phi3 {
  !(eventually (((always (state[0] == 2)) ||
                 (always (state[0] == 3)) ||
                 (always (state[0] == 4)) ||
                 (always (state[0] == 5)) ||
                 (always (state[0] == 6)) ||
                 (always (state[0] == 7)) ||
                 (always (state[0] == 8)) ||
                 (always (state[0] == 9)) ||
                 (always (state[0] == 10)))
                &&
                ((always (state[1] == 2)) ||
                 (always (state[1] == 3)) ||
                 (always (state[1] == 4)) ||
                 (always (state[1] == 5)) ||
                 (always (state[1] == 6)) ||
                 (always (state[1] == 7)) ||
                 (always (state[1] == 8)) ||
                 (always (state[1] == 9)) ||
                 (always (state[1] == 10)))))
}