RRPPOGRG PGPOPRRO YYBBYRYB GBYYRGGP OGBRRORY BYRRPRBG YOYYROBB OROBPPRB ok: board_init no-match invariant holds