Lemma 4.2 and Remark 5.1 symbolic check, n <= 12: 0 failures -> ALL OK
