c This table represents how propositions correspond to numbers c p[1] = 1, p[2] = 2, p[3] = 3, p[4] = 4, p[5] = 5, p[6] = 6, p[7] = 7, p[8] = 8, p[9] = 9, p[10] = 10, c break = 11 c b[1][1][2] = 12 b[1][1][1] = 13 b[1][1][0] = 14 c b[1][2][2] = 15 b[1][2][1] = 16 b[1][2][0] = 17 c b[1][3][2] = 18 b[1][3][1] = 19 b[1][3][0] = 20 c b[1][4][2] = 21 b[1][4][1] = 22 b[1][4][0] = 23 c b[1][5][2] = 24 b[1][5][1] = 25 b[1][5][0] = 26 c b[1][6][2] = 27 b[1][6][1] = 28 b[1][6][0] = 29 c b[1][7][2] = 30 b[1][7][1] = 31 b[1][7][0] = 32 c b[1][8][2] = 33 b[1][8][1] = 34 b[1][8][0] = 35 c b[1][9][2] = 36 b[1][9][1] = 37 b[1][9][0] = 38 c b[1][10][2] = 39 b[1][10][1] = 40 b[1][10][0] = 41 c b[1][11][2] = 42 b[1][11][1] = 43 b[1][11][0] = 44 c b[2][1][2] = 45 b[2][1][1] = 46 b[2][1][0] = 47 c b[2][2][2] = 48 b[2][2][1] = 49 b[2][2][0] = 50 c b[2][3][2] = 51 b[2][3][1] = 52 b[2][3][0] = 53 c b[2][4][2] = 54 b[2][4][1] = 55 b[2][4][0] = 56 c b[2][5][2] = 57 b[2][5][1] = 58 b[2][5][0] = 59 c b[2][6][2] = 60 b[2][6][1] = 61 b[2][6][0] = 62 c b[3][1][2] = 63 b[3][1][1] = 64 b[3][1][0] = 65 c b[3][2][2] = 66 b[3][2][1] = 67 b[3][2][0] = 68 c b[3][3][2] = 69 b[3][3][1] = 70 b[3][3][0] = 71 c b[3][4][2] = 72 b[3][4][1] = 73 b[3][4][0] = 74 p cnf 74 532 c Automaton should not be broken c -break -11 0 c INIT for k = 1 c -b^{1, 1}_2 c -b^{1, 1}_1 c -b^{1, 1}_0 c in DIMACS: -12 0 -13 0 -14 0 c Transitions for k = 1 c i = 1 c -2+1 --> -1 c ( b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ p_1) -> ( b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0) c in CNF: c -b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ b^{1, 2}_2 c -b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_1 c -b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ b^{1, 2}_0 c in DIMACS: -12 -13 14 -1 15 0 -12 -13 14 -1 -16 0 -12 -13 14 -1 17 0 c -1+1 --> 0 c ( b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ p_1) -> (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ -b^{1, 2}_0) c in CNF: c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_2 c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_1 c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_0 c in DIMACS: -12 13 -14 -1 -15 0 -12 13 -14 -1 -16 0 -12 13 -14 -1 -17 0 c 0+1 --> 1 c (-b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ p_1) -> (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0) c in CNF: c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_2 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_1 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ b^{1, 2}_0 c in DIMACS: 12 13 14 -1 -15 0 12 13 14 -1 -16 0 12 13 14 -1 17 0 c 1+1 --> 2 c (-b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ p_1) -> (-b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0) c in CNF: c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_2 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ b^{1, 2}_1 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ -p_1 ∨ -b^{1, 2}_0 c in DIMACS: 12 13 -14 -1 -15 0 12 13 -14 -1 16 0 12 13 -14 -1 -17 0 c 2+1 --> break c (-b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ p_1) -> break c in CNF: c b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ -p_1 ∨ break c in DIMACS: 12 -13 14 -1 11 0 c 2-1 --> 1 c (-b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ -p_1) -> (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0) c in CNF: c b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_2 c b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_1 c b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ b^{1, 2}_0 c in DIMACS: 12 -13 14 1 -15 0 12 -13 14 1 -16 0 12 -13 14 1 17 0 c 1-1 --> 0 c (-b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ -p_1) -> (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ -b^{1, 2}_0) c in CNF: c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_2 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_1 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_0 c in DIMACS: 12 13 -14 1 -15 0 12 13 -14 1 -16 0 12 13 -14 1 -17 0 c 0-1 --> -1 c (-b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ -p_1) -> ( b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0) c in CNF: c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ b^{1, 2}_2 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_1 c b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ b^{1, 2}_0 c in DIMACS: 12 13 14 1 15 0 12 13 14 1 -16 0 12 13 14 1 17 0 c -1-1 --> -2 c ( b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ -p_1) -> ( b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0) c in CNF: c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ b^{1, 2}_2 c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ b^{1, 2}_1 c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ p_1 ∨ -b^{1, 2}_0 c in DIMACS: -12 13 -14 1 15 0 -12 13 -14 1 16 0 -12 13 -14 1 -17 0 c -2-1 --> break c ( b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ -p_1) -> break c in CNF: c -b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ p_1 ∨ break c in DIMACS: -12 -13 14 1 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 1}_2 ∧ -b^{1, 1}_1 ∧ -b^{1, 1}_0 ∧ true) c in CNF: c -b^{1, 1}_2 ∨ b^{1, 1}_1 ∨ b^{1, 1}_0 ∨ false c in DIMACS: -12 13 14 0 c 3 does not represent an automaton state. c -(-b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ true) c in CNF: c b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ false c in DIMACS: 12 -13 -14 0 c -3 does not represent an automaton state. c -( b^{1, 1}_2 ∧ b^{1, 1}_1 ∧ b^{1, 1}_0 ∧ true) c in CNF: c -b^{1, 1}_2 ∨ -b^{1, 1}_1 ∨ -b^{1, 1}_0 ∨ false c in DIMACS: -12 -13 -14 0 c i = 2 c -2+1 --> -1 c ( b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ p_2) -> ( b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0) c in CNF: c -b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ b^{1, 3}_2 c -b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_1 c -b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ b^{1, 3}_0 c in DIMACS: -15 -16 17 -2 18 0 -15 -16 17 -2 -19 0 -15 -16 17 -2 20 0 c -1+1 --> 0 c ( b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ p_2) -> (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ -b^{1, 3}_0) c in CNF: c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_2 c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_1 c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_0 c in DIMACS: -15 16 -17 -2 -18 0 -15 16 -17 -2 -19 0 -15 16 -17 -2 -20 0 c 0+1 --> 1 c (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ p_2) -> (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0) c in CNF: c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_2 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_1 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ b^{1, 3}_0 c in DIMACS: 15 16 17 -2 -18 0 15 16 17 -2 -19 0 15 16 17 -2 20 0 c 1+1 --> 2 c (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ p_2) -> (-b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0) c in CNF: c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_2 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ b^{1, 3}_1 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ -p_2 ∨ -b^{1, 3}_0 c in DIMACS: 15 16 -17 -2 -18 0 15 16 -17 -2 19 0 15 16 -17 -2 -20 0 c 2+1 --> break c (-b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ p_2) -> break c in CNF: c b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ -p_2 ∨ break c in DIMACS: 15 -16 17 -2 11 0 c 2-1 --> 1 c (-b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ -p_2) -> (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0) c in CNF: c b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_2 c b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_1 c b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ b^{1, 3}_0 c in DIMACS: 15 -16 17 2 -18 0 15 -16 17 2 -19 0 15 -16 17 2 20 0 c 1-1 --> 0 c (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ -p_2) -> (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ -b^{1, 3}_0) c in CNF: c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_2 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_1 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_0 c in DIMACS: 15 16 -17 2 -18 0 15 16 -17 2 -19 0 15 16 -17 2 -20 0 c 0-1 --> -1 c (-b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ -p_2) -> ( b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0) c in CNF: c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ b^{1, 3}_2 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_1 c b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ b^{1, 3}_0 c in DIMACS: 15 16 17 2 18 0 15 16 17 2 -19 0 15 16 17 2 20 0 c -1-1 --> -2 c ( b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ -p_2) -> ( b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0) c in CNF: c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ b^{1, 3}_2 c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ b^{1, 3}_1 c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ p_2 ∨ -b^{1, 3}_0 c in DIMACS: -15 16 -17 2 18 0 -15 16 -17 2 19 0 -15 16 -17 2 -20 0 c -2-1 --> break c ( b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ -p_2) -> break c in CNF: c -b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ p_2 ∨ break c in DIMACS: -15 -16 17 2 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 2}_2 ∧ -b^{1, 2}_1 ∧ -b^{1, 2}_0 ∧ true) c in CNF: c -b^{1, 2}_2 ∨ b^{1, 2}_1 ∨ b^{1, 2}_0 ∨ false c in DIMACS: -15 16 17 0 c 3 does not represent an automaton state. c -(-b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ true) c in CNF: c b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ false c in DIMACS: 15 -16 -17 0 c -3 does not represent an automaton state. c -( b^{1, 2}_2 ∧ b^{1, 2}_1 ∧ b^{1, 2}_0 ∧ true) c in CNF: c -b^{1, 2}_2 ∨ -b^{1, 2}_1 ∨ -b^{1, 2}_0 ∨ false c in DIMACS: -15 -16 -17 0 c i = 3 c -2+1 --> -1 c ( b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ p_3) -> ( b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0) c in CNF: c -b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ b^{1, 4}_2 c -b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_1 c -b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ b^{1, 4}_0 c in DIMACS: -18 -19 20 -3 21 0 -18 -19 20 -3 -22 0 -18 -19 20 -3 23 0 c -1+1 --> 0 c ( b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ p_3) -> (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ -b^{1, 4}_0) c in CNF: c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_2 c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_1 c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_0 c in DIMACS: -18 19 -20 -3 -21 0 -18 19 -20 -3 -22 0 -18 19 -20 -3 -23 0 c 0+1 --> 1 c (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ p_3) -> (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0) c in CNF: c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_2 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_1 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ b^{1, 4}_0 c in DIMACS: 18 19 20 -3 -21 0 18 19 20 -3 -22 0 18 19 20 -3 23 0 c 1+1 --> 2 c (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ p_3) -> (-b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0) c in CNF: c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_2 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ b^{1, 4}_1 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ -p_3 ∨ -b^{1, 4}_0 c in DIMACS: 18 19 -20 -3 -21 0 18 19 -20 -3 22 0 18 19 -20 -3 -23 0 c 2+1 --> break c (-b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ p_3) -> break c in CNF: c b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ -p_3 ∨ break c in DIMACS: 18 -19 20 -3 11 0 c 2-1 --> 1 c (-b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ -p_3) -> (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0) c in CNF: c b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_2 c b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_1 c b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ b^{1, 4}_0 c in DIMACS: 18 -19 20 3 -21 0 18 -19 20 3 -22 0 18 -19 20 3 23 0 c 1-1 --> 0 c (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ -p_3) -> (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ -b^{1, 4}_0) c in CNF: c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_2 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_1 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_0 c in DIMACS: 18 19 -20 3 -21 0 18 19 -20 3 -22 0 18 19 -20 3 -23 0 c 0-1 --> -1 c (-b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ -p_3) -> ( b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0) c in CNF: c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ b^{1, 4}_2 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_1 c b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ b^{1, 4}_0 c in DIMACS: 18 19 20 3 21 0 18 19 20 3 -22 0 18 19 20 3 23 0 c -1-1 --> -2 c ( b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ -p_3) -> ( b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0) c in CNF: c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ b^{1, 4}_2 c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ b^{1, 4}_1 c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ p_3 ∨ -b^{1, 4}_0 c in DIMACS: -18 19 -20 3 21 0 -18 19 -20 3 22 0 -18 19 -20 3 -23 0 c -2-1 --> break c ( b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ -p_3) -> break c in CNF: c -b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ p_3 ∨ break c in DIMACS: -18 -19 20 3 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 3}_2 ∧ -b^{1, 3}_1 ∧ -b^{1, 3}_0 ∧ true) c in CNF: c -b^{1, 3}_2 ∨ b^{1, 3}_1 ∨ b^{1, 3}_0 ∨ false c in DIMACS: -18 19 20 0 c 3 does not represent an automaton state. c -(-b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ true) c in CNF: c b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ false c in DIMACS: 18 -19 -20 0 c -3 does not represent an automaton state. c -( b^{1, 3}_2 ∧ b^{1, 3}_1 ∧ b^{1, 3}_0 ∧ true) c in CNF: c -b^{1, 3}_2 ∨ -b^{1, 3}_1 ∨ -b^{1, 3}_0 ∨ false c in DIMACS: -18 -19 -20 0 c i = 4 c -2+1 --> -1 c ( b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ p_4) -> ( b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0) c in CNF: c -b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ b^{1, 5}_2 c -b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_1 c -b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ b^{1, 5}_0 c in DIMACS: -21 -22 23 -4 24 0 -21 -22 23 -4 -25 0 -21 -22 23 -4 26 0 c -1+1 --> 0 c ( b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ p_4) -> (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ -b^{1, 5}_0) c in CNF: c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_2 c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_1 c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_0 c in DIMACS: -21 22 -23 -4 -24 0 -21 22 -23 -4 -25 0 -21 22 -23 -4 -26 0 c 0+1 --> 1 c (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ p_4) -> (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0) c in CNF: c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_2 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_1 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ b^{1, 5}_0 c in DIMACS: 21 22 23 -4 -24 0 21 22 23 -4 -25 0 21 22 23 -4 26 0 c 1+1 --> 2 c (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ p_4) -> (-b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0) c in CNF: c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_2 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ b^{1, 5}_1 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ -p_4 ∨ -b^{1, 5}_0 c in DIMACS: 21 22 -23 -4 -24 0 21 22 -23 -4 25 0 21 22 -23 -4 -26 0 c 2+1 --> break c (-b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ p_4) -> break c in CNF: c b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ -p_4 ∨ break c in DIMACS: 21 -22 23 -4 11 0 c 2-1 --> 1 c (-b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ -p_4) -> (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0) c in CNF: c b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_2 c b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_1 c b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ b^{1, 5}_0 c in DIMACS: 21 -22 23 4 -24 0 21 -22 23 4 -25 0 21 -22 23 4 26 0 c 1-1 --> 0 c (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ -p_4) -> (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ -b^{1, 5}_0) c in CNF: c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_2 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_1 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_0 c in DIMACS: 21 22 -23 4 -24 0 21 22 -23 4 -25 0 21 22 -23 4 -26 0 c 0-1 --> -1 c (-b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ -p_4) -> ( b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0) c in CNF: c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ b^{1, 5}_2 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_1 c b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ b^{1, 5}_0 c in DIMACS: 21 22 23 4 24 0 21 22 23 4 -25 0 21 22 23 4 26 0 c -1-1 --> -2 c ( b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ -p_4) -> ( b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0) c in CNF: c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ b^{1, 5}_2 c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ b^{1, 5}_1 c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ p_4 ∨ -b^{1, 5}_0 c in DIMACS: -21 22 -23 4 24 0 -21 22 -23 4 25 0 -21 22 -23 4 -26 0 c -2-1 --> break c ( b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ -p_4) -> break c in CNF: c -b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ p_4 ∨ break c in DIMACS: -21 -22 23 4 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 4}_2 ∧ -b^{1, 4}_1 ∧ -b^{1, 4}_0 ∧ true) c in CNF: c -b^{1, 4}_2 ∨ b^{1, 4}_1 ∨ b^{1, 4}_0 ∨ false c in DIMACS: -21 22 23 0 c 3 does not represent an automaton state. c -(-b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ true) c in CNF: c b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ false c in DIMACS: 21 -22 -23 0 c -3 does not represent an automaton state. c -( b^{1, 4}_2 ∧ b^{1, 4}_1 ∧ b^{1, 4}_0 ∧ true) c in CNF: c -b^{1, 4}_2 ∨ -b^{1, 4}_1 ∨ -b^{1, 4}_0 ∨ false c in DIMACS: -21 -22 -23 0 c i = 5 c -2+1 --> -1 c ( b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ p_5) -> ( b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0) c in CNF: c -b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ b^{1, 6}_2 c -b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_1 c -b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ b^{1, 6}_0 c in DIMACS: -24 -25 26 -5 27 0 -24 -25 26 -5 -28 0 -24 -25 26 -5 29 0 c -1+1 --> 0 c ( b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ p_5) -> (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ -b^{1, 6}_0) c in CNF: c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_2 c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_1 c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_0 c in DIMACS: -24 25 -26 -5 -27 0 -24 25 -26 -5 -28 0 -24 25 -26 -5 -29 0 c 0+1 --> 1 c (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ p_5) -> (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0) c in CNF: c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_2 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_1 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ b^{1, 6}_0 c in DIMACS: 24 25 26 -5 -27 0 24 25 26 -5 -28 0 24 25 26 -5 29 0 c 1+1 --> 2 c (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ p_5) -> (-b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0) c in CNF: c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_2 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ b^{1, 6}_1 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ -p_5 ∨ -b^{1, 6}_0 c in DIMACS: 24 25 -26 -5 -27 0 24 25 -26 -5 28 0 24 25 -26 -5 -29 0 c 2+1 --> break c (-b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ p_5) -> break c in CNF: c b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ -p_5 ∨ break c in DIMACS: 24 -25 26 -5 11 0 c 2-1 --> 1 c (-b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ -p_5) -> (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0) c in CNF: c b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_2 c b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_1 c b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ b^{1, 6}_0 c in DIMACS: 24 -25 26 5 -27 0 24 -25 26 5 -28 0 24 -25 26 5 29 0 c 1-1 --> 0 c (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ -p_5) -> (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ -b^{1, 6}_0) c in CNF: c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_2 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_1 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_0 c in DIMACS: 24 25 -26 5 -27 0 24 25 -26 5 -28 0 24 25 -26 5 -29 0 c 0-1 --> -1 c (-b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ -p_5) -> ( b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0) c in CNF: c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ b^{1, 6}_2 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_1 c b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ b^{1, 6}_0 c in DIMACS: 24 25 26 5 27 0 24 25 26 5 -28 0 24 25 26 5 29 0 c -1-1 --> -2 c ( b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ -p_5) -> ( b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0) c in CNF: c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ b^{1, 6}_2 c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ b^{1, 6}_1 c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ p_5 ∨ -b^{1, 6}_0 c in DIMACS: -24 25 -26 5 27 0 -24 25 -26 5 28 0 -24 25 -26 5 -29 0 c -2-1 --> break c ( b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ -p_5) -> break c in CNF: c -b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ p_5 ∨ break c in DIMACS: -24 -25 26 5 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 5}_2 ∧ -b^{1, 5}_1 ∧ -b^{1, 5}_0 ∧ true) c in CNF: c -b^{1, 5}_2 ∨ b^{1, 5}_1 ∨ b^{1, 5}_0 ∨ false c in DIMACS: -24 25 26 0 c 3 does not represent an automaton state. c -(-b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ true) c in CNF: c b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ false c in DIMACS: 24 -25 -26 0 c -3 does not represent an automaton state. c -( b^{1, 5}_2 ∧ b^{1, 5}_1 ∧ b^{1, 5}_0 ∧ true) c in CNF: c -b^{1, 5}_2 ∨ -b^{1, 5}_1 ∨ -b^{1, 5}_0 ∨ false c in DIMACS: -24 -25 -26 0 c i = 6 c -2+1 --> -1 c ( b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ p_6) -> ( b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0) c in CNF: c -b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ b^{1, 7}_2 c -b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_1 c -b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ b^{1, 7}_0 c in DIMACS: -27 -28 29 -6 30 0 -27 -28 29 -6 -31 0 -27 -28 29 -6 32 0 c -1+1 --> 0 c ( b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ p_6) -> (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ -b^{1, 7}_0) c in CNF: c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_2 c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_1 c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_0 c in DIMACS: -27 28 -29 -6 -30 0 -27 28 -29 -6 -31 0 -27 28 -29 -6 -32 0 c 0+1 --> 1 c (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ p_6) -> (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0) c in CNF: c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_2 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_1 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ b^{1, 7}_0 c in DIMACS: 27 28 29 -6 -30 0 27 28 29 -6 -31 0 27 28 29 -6 32 0 c 1+1 --> 2 c (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ p_6) -> (-b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0) c in CNF: c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_2 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ b^{1, 7}_1 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ -p_6 ∨ -b^{1, 7}_0 c in DIMACS: 27 28 -29 -6 -30 0 27 28 -29 -6 31 0 27 28 -29 -6 -32 0 c 2+1 --> break c (-b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ p_6) -> break c in CNF: c b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ -p_6 ∨ break c in DIMACS: 27 -28 29 -6 11 0 c 2-1 --> 1 c (-b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ -p_6) -> (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0) c in CNF: c b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_2 c b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_1 c b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ b^{1, 7}_0 c in DIMACS: 27 -28 29 6 -30 0 27 -28 29 6 -31 0 27 -28 29 6 32 0 c 1-1 --> 0 c (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ -p_6) -> (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ -b^{1, 7}_0) c in CNF: c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_2 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_1 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_0 c in DIMACS: 27 28 -29 6 -30 0 27 28 -29 6 -31 0 27 28 -29 6 -32 0 c 0-1 --> -1 c (-b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ -p_6) -> ( b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0) c in CNF: c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ b^{1, 7}_2 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_1 c b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ b^{1, 7}_0 c in DIMACS: 27 28 29 6 30 0 27 28 29 6 -31 0 27 28 29 6 32 0 c -1-1 --> -2 c ( b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ -p_6) -> ( b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0) c in CNF: c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ b^{1, 7}_2 c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ b^{1, 7}_1 c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ p_6 ∨ -b^{1, 7}_0 c in DIMACS: -27 28 -29 6 30 0 -27 28 -29 6 31 0 -27 28 -29 6 -32 0 c -2-1 --> break c ( b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ -p_6) -> break c in CNF: c -b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ p_6 ∨ break c in DIMACS: -27 -28 29 6 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 6}_2 ∧ -b^{1, 6}_1 ∧ -b^{1, 6}_0 ∧ true) c in CNF: c -b^{1, 6}_2 ∨ b^{1, 6}_1 ∨ b^{1, 6}_0 ∨ false c in DIMACS: -27 28 29 0 c 3 does not represent an automaton state. c -(-b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ true) c in CNF: c b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ false c in DIMACS: 27 -28 -29 0 c -3 does not represent an automaton state. c -( b^{1, 6}_2 ∧ b^{1, 6}_1 ∧ b^{1, 6}_0 ∧ true) c in CNF: c -b^{1, 6}_2 ∨ -b^{1, 6}_1 ∨ -b^{1, 6}_0 ∨ false c in DIMACS: -27 -28 -29 0 c i = 7 c -2+1 --> -1 c ( b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ p_7) -> ( b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0) c in CNF: c -b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ b^{1, 8}_2 c -b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_1 c -b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ b^{1, 8}_0 c in DIMACS: -30 -31 32 -7 33 0 -30 -31 32 -7 -34 0 -30 -31 32 -7 35 0 c -1+1 --> 0 c ( b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ p_7) -> (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ -b^{1, 8}_0) c in CNF: c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_2 c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_1 c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_0 c in DIMACS: -30 31 -32 -7 -33 0 -30 31 -32 -7 -34 0 -30 31 -32 -7 -35 0 c 0+1 --> 1 c (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ p_7) -> (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0) c in CNF: c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_2 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_1 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ b^{1, 8}_0 c in DIMACS: 30 31 32 -7 -33 0 30 31 32 -7 -34 0 30 31 32 -7 35 0 c 1+1 --> 2 c (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ p_7) -> (-b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0) c in CNF: c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_2 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ b^{1, 8}_1 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ -p_7 ∨ -b^{1, 8}_0 c in DIMACS: 30 31 -32 -7 -33 0 30 31 -32 -7 34 0 30 31 -32 -7 -35 0 c 2+1 --> break c (-b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ p_7) -> break c in CNF: c b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ -p_7 ∨ break c in DIMACS: 30 -31 32 -7 11 0 c 2-1 --> 1 c (-b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ -p_7) -> (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0) c in CNF: c b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_2 c b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_1 c b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ b^{1, 8}_0 c in DIMACS: 30 -31 32 7 -33 0 30 -31 32 7 -34 0 30 -31 32 7 35 0 c 1-1 --> 0 c (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ -p_7) -> (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ -b^{1, 8}_0) c in CNF: c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_2 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_1 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_0 c in DIMACS: 30 31 -32 7 -33 0 30 31 -32 7 -34 0 30 31 -32 7 -35 0 c 0-1 --> -1 c (-b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ -p_7) -> ( b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0) c in CNF: c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ b^{1, 8}_2 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_1 c b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ b^{1, 8}_0 c in DIMACS: 30 31 32 7 33 0 30 31 32 7 -34 0 30 31 32 7 35 0 c -1-1 --> -2 c ( b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ -p_7) -> ( b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0) c in CNF: c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ b^{1, 8}_2 c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ b^{1, 8}_1 c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ p_7 ∨ -b^{1, 8}_0 c in DIMACS: -30 31 -32 7 33 0 -30 31 -32 7 34 0 -30 31 -32 7 -35 0 c -2-1 --> break c ( b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ -p_7) -> break c in CNF: c -b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ p_7 ∨ break c in DIMACS: -30 -31 32 7 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 7}_2 ∧ -b^{1, 7}_1 ∧ -b^{1, 7}_0 ∧ true) c in CNF: c -b^{1, 7}_2 ∨ b^{1, 7}_1 ∨ b^{1, 7}_0 ∨ false c in DIMACS: -30 31 32 0 c 3 does not represent an automaton state. c -(-b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ true) c in CNF: c b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ false c in DIMACS: 30 -31 -32 0 c -3 does not represent an automaton state. c -( b^{1, 7}_2 ∧ b^{1, 7}_1 ∧ b^{1, 7}_0 ∧ true) c in CNF: c -b^{1, 7}_2 ∨ -b^{1, 7}_1 ∨ -b^{1, 7}_0 ∨ false c in DIMACS: -30 -31 -32 0 c i = 8 c -2+1 --> -1 c ( b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ p_8) -> ( b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0) c in CNF: c -b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ b^{1, 9}_2 c -b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_1 c -b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ b^{1, 9}_0 c in DIMACS: -33 -34 35 -8 36 0 -33 -34 35 -8 -37 0 -33 -34 35 -8 38 0 c -1+1 --> 0 c ( b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ p_8) -> (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ -b^{1, 9}_0) c in CNF: c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_2 c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_1 c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_0 c in DIMACS: -33 34 -35 -8 -36 0 -33 34 -35 -8 -37 0 -33 34 -35 -8 -38 0 c 0+1 --> 1 c (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ p_8) -> (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0) c in CNF: c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_2 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_1 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ b^{1, 9}_0 c in DIMACS: 33 34 35 -8 -36 0 33 34 35 -8 -37 0 33 34 35 -8 38 0 c 1+1 --> 2 c (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ p_8) -> (-b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0) c in CNF: c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_2 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ b^{1, 9}_1 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ -p_8 ∨ -b^{1, 9}_0 c in DIMACS: 33 34 -35 -8 -36 0 33 34 -35 -8 37 0 33 34 -35 -8 -38 0 c 2+1 --> break c (-b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ p_8) -> break c in CNF: c b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ -p_8 ∨ break c in DIMACS: 33 -34 35 -8 11 0 c 2-1 --> 1 c (-b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ -p_8) -> (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0) c in CNF: c b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_2 c b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_1 c b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ b^{1, 9}_0 c in DIMACS: 33 -34 35 8 -36 0 33 -34 35 8 -37 0 33 -34 35 8 38 0 c 1-1 --> 0 c (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ -p_8) -> (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ -b^{1, 9}_0) c in CNF: c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_2 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_1 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_0 c in DIMACS: 33 34 -35 8 -36 0 33 34 -35 8 -37 0 33 34 -35 8 -38 0 c 0-1 --> -1 c (-b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ -p_8) -> ( b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0) c in CNF: c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ b^{1, 9}_2 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_1 c b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ b^{1, 9}_0 c in DIMACS: 33 34 35 8 36 0 33 34 35 8 -37 0 33 34 35 8 38 0 c -1-1 --> -2 c ( b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ -p_8) -> ( b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0) c in CNF: c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ b^{1, 9}_2 c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ b^{1, 9}_1 c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ p_8 ∨ -b^{1, 9}_0 c in DIMACS: -33 34 -35 8 36 0 -33 34 -35 8 37 0 -33 34 -35 8 -38 0 c -2-1 --> break c ( b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ -p_8) -> break c in CNF: c -b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ p_8 ∨ break c in DIMACS: -33 -34 35 8 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 8}_2 ∧ -b^{1, 8}_1 ∧ -b^{1, 8}_0 ∧ true) c in CNF: c -b^{1, 8}_2 ∨ b^{1, 8}_1 ∨ b^{1, 8}_0 ∨ false c in DIMACS: -33 34 35 0 c 3 does not represent an automaton state. c -(-b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ true) c in CNF: c b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ false c in DIMACS: 33 -34 -35 0 c -3 does not represent an automaton state. c -( b^{1, 8}_2 ∧ b^{1, 8}_1 ∧ b^{1, 8}_0 ∧ true) c in CNF: c -b^{1, 8}_2 ∨ -b^{1, 8}_1 ∨ -b^{1, 8}_0 ∨ false c in DIMACS: -33 -34 -35 0 c i = 9 c -2+1 --> -1 c ( b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ p_9) -> ( b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0) c in CNF: c -b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ b^{1, 10}_2 c -b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_1 c -b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ b^{1, 10}_0 c in DIMACS: -36 -37 38 -9 39 0 -36 -37 38 -9 -40 0 -36 -37 38 -9 41 0 c -1+1 --> 0 c ( b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ p_9) -> (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ -b^{1, 10}_0) c in CNF: c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_2 c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_1 c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_0 c in DIMACS: -36 37 -38 -9 -39 0 -36 37 -38 -9 -40 0 -36 37 -38 -9 -41 0 c 0+1 --> 1 c (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ p_9) -> (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0) c in CNF: c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_2 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_1 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ b^{1, 10}_0 c in DIMACS: 36 37 38 -9 -39 0 36 37 38 -9 -40 0 36 37 38 -9 41 0 c 1+1 --> 2 c (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ p_9) -> (-b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0) c in CNF: c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_2 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ b^{1, 10}_1 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ -p_9 ∨ -b^{1, 10}_0 c in DIMACS: 36 37 -38 -9 -39 0 36 37 -38 -9 40 0 36 37 -38 -9 -41 0 c 2+1 --> break c (-b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ p_9) -> break c in CNF: c b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ -p_9 ∨ break c in DIMACS: 36 -37 38 -9 11 0 c 2-1 --> 1 c (-b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ -p_9) -> (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0) c in CNF: c b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_2 c b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_1 c b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ b^{1, 10}_0 c in DIMACS: 36 -37 38 9 -39 0 36 -37 38 9 -40 0 36 -37 38 9 41 0 c 1-1 --> 0 c (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ -p_9) -> (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ -b^{1, 10}_0) c in CNF: c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_2 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_1 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_0 c in DIMACS: 36 37 -38 9 -39 0 36 37 -38 9 -40 0 36 37 -38 9 -41 0 c 0-1 --> -1 c (-b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ -p_9) -> ( b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0) c in CNF: c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ b^{1, 10}_2 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_1 c b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ b^{1, 10}_0 c in DIMACS: 36 37 38 9 39 0 36 37 38 9 -40 0 36 37 38 9 41 0 c -1-1 --> -2 c ( b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ -p_9) -> ( b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0) c in CNF: c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ b^{1, 10}_2 c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ b^{1, 10}_1 c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ p_9 ∨ -b^{1, 10}_0 c in DIMACS: -36 37 -38 9 39 0 -36 37 -38 9 40 0 -36 37 -38 9 -41 0 c -2-1 --> break c ( b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ -p_9) -> break c in CNF: c -b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ p_9 ∨ break c in DIMACS: -36 -37 38 9 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 9}_2 ∧ -b^{1, 9}_1 ∧ -b^{1, 9}_0 ∧ true) c in CNF: c -b^{1, 9}_2 ∨ b^{1, 9}_1 ∨ b^{1, 9}_0 ∨ false c in DIMACS: -36 37 38 0 c 3 does not represent an automaton state. c -(-b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ true) c in CNF: c b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ false c in DIMACS: 36 -37 -38 0 c -3 does not represent an automaton state. c -( b^{1, 9}_2 ∧ b^{1, 9}_1 ∧ b^{1, 9}_0 ∧ true) c in CNF: c -b^{1, 9}_2 ∨ -b^{1, 9}_1 ∨ -b^{1, 9}_0 ∨ false c in DIMACS: -36 -37 -38 0 c i = 10 c -2+1 --> -1 c ( b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ p_10) -> ( b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ b^{1, 11}_0) c in CNF: c -b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ b^{1, 11}_2 c -b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_1 c -b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ b^{1, 11}_0 c in DIMACS: -39 -40 41 -10 42 0 -39 -40 41 -10 -43 0 -39 -40 41 -10 44 0 c -1+1 --> 0 c ( b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ p_10) -> (-b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ -b^{1, 11}_0) c in CNF: c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_2 c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_1 c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_0 c in DIMACS: -39 40 -41 -10 -42 0 -39 40 -41 -10 -43 0 -39 40 -41 -10 -44 0 c 0+1 --> 1 c (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ p_10) -> (-b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ b^{1, 11}_0) c in CNF: c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_2 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_1 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ b^{1, 11}_0 c in DIMACS: 39 40 41 -10 -42 0 39 40 41 -10 -43 0 39 40 41 -10 44 0 c 1+1 --> 2 c (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ p_10) -> (-b^{1, 11}_2 ∧ b^{1, 11}_1 ∧ -b^{1, 11}_0) c in CNF: c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_2 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ b^{1, 11}_1 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ -p_10 ∨ -b^{1, 11}_0 c in DIMACS: 39 40 -41 -10 -42 0 39 40 -41 -10 43 0 39 40 -41 -10 -44 0 c 2+1 --> break c (-b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ p_10) -> break c in CNF: c b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ -p_10 ∨ break c in DIMACS: 39 -40 41 -10 11 0 c 2-1 --> 1 c (-b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ -p_10) -> (-b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ b^{1, 11}_0) c in CNF: c b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_2 c b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_1 c b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ b^{1, 11}_0 c in DIMACS: 39 -40 41 10 -42 0 39 -40 41 10 -43 0 39 -40 41 10 44 0 c 1-1 --> 0 c (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ -p_10) -> (-b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ -b^{1, 11}_0) c in CNF: c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_2 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_1 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_0 c in DIMACS: 39 40 -41 10 -42 0 39 40 -41 10 -43 0 39 40 -41 10 -44 0 c 0-1 --> -1 c (-b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ -p_10) -> ( b^{1, 11}_2 ∧ -b^{1, 11}_1 ∧ b^{1, 11}_0) c in CNF: c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ b^{1, 11}_2 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_1 c b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ b^{1, 11}_0 c in DIMACS: 39 40 41 10 42 0 39 40 41 10 -43 0 39 40 41 10 44 0 c -1-1 --> -2 c ( b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ -p_10) -> ( b^{1, 11}_2 ∧ b^{1, 11}_1 ∧ -b^{1, 11}_0) c in CNF: c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ b^{1, 11}_2 c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ b^{1, 11}_1 c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ p_10 ∨ -b^{1, 11}_0 c in DIMACS: -39 40 -41 10 42 0 -39 40 -41 10 43 0 -39 40 -41 10 -44 0 c -2-1 --> break c ( b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ -p_10) -> break c in CNF: c -b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ p_10 ∨ break c in DIMACS: -39 -40 41 10 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{1, 10}_2 ∧ -b^{1, 10}_1 ∧ -b^{1, 10}_0 ∧ true) c in CNF: c -b^{1, 10}_2 ∨ b^{1, 10}_1 ∨ b^{1, 10}_0 ∨ false c in DIMACS: -39 40 41 0 c 3 does not represent an automaton state. c -(-b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ true) c in CNF: c b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ false c in DIMACS: 39 -40 -41 0 c -3 does not represent an automaton state. c -( b^{1, 10}_2 ∧ b^{1, 10}_1 ∧ b^{1, 10}_0 ∧ true) c in CNF: c -b^{1, 10}_2 ∨ -b^{1, 10}_1 ∨ -b^{1, 10}_0 ∨ false c in DIMACS: -39 -40 -41 0 c INIT for k = 2 c -b^{2, 1}_2 c -b^{2, 1}_1 c -b^{2, 1}_0 c in DIMACS: -45 0 -46 0 -47 0 c Transitions for k = 2 c i = 1 c -2+1 --> -1 c ( b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ p_2) -> ( b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0) c in CNF: c -b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ b^{2, 2}_2 c -b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_1 c -b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ b^{2, 2}_0 c in DIMACS: -45 -46 47 -2 48 0 -45 -46 47 -2 -49 0 -45 -46 47 -2 50 0 c -1+1 --> 0 c ( b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ p_2) -> (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ -b^{2, 2}_0) c in CNF: c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_2 c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_1 c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_0 c in DIMACS: -45 46 -47 -2 -48 0 -45 46 -47 -2 -49 0 -45 46 -47 -2 -50 0 c 0+1 --> 1 c (-b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ p_2) -> (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0) c in CNF: c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_2 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_1 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ b^{2, 2}_0 c in DIMACS: 45 46 47 -2 -48 0 45 46 47 -2 -49 0 45 46 47 -2 50 0 c 1+1 --> 2 c (-b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ p_2) -> (-b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0) c in CNF: c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_2 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ b^{2, 2}_1 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ -p_2 ∨ -b^{2, 2}_0 c in DIMACS: 45 46 -47 -2 -48 0 45 46 -47 -2 49 0 45 46 -47 -2 -50 0 c 2+1 --> break c (-b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ p_2) -> break c in CNF: c b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ -p_2 ∨ break c in DIMACS: 45 -46 47 -2 11 0 c 2-1 --> 1 c (-b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ -p_2) -> (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0) c in CNF: c b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_2 c b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_1 c b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ b^{2, 2}_0 c in DIMACS: 45 -46 47 2 -48 0 45 -46 47 2 -49 0 45 -46 47 2 50 0 c 1-1 --> 0 c (-b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ -p_2) -> (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ -b^{2, 2}_0) c in CNF: c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_2 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_1 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_0 c in DIMACS: 45 46 -47 2 -48 0 45 46 -47 2 -49 0 45 46 -47 2 -50 0 c 0-1 --> -1 c (-b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ -p_2) -> ( b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0) c in CNF: c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ b^{2, 2}_2 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_1 c b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ b^{2, 2}_0 c in DIMACS: 45 46 47 2 48 0 45 46 47 2 -49 0 45 46 47 2 50 0 c -1-1 --> -2 c ( b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ -p_2) -> ( b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0) c in CNF: c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ b^{2, 2}_2 c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ b^{2, 2}_1 c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ p_2 ∨ -b^{2, 2}_0 c in DIMACS: -45 46 -47 2 48 0 -45 46 -47 2 49 0 -45 46 -47 2 -50 0 c -2-1 --> break c ( b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ -p_2) -> break c in CNF: c -b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ p_2 ∨ break c in DIMACS: -45 -46 47 2 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{2, 1}_2 ∧ -b^{2, 1}_1 ∧ -b^{2, 1}_0 ∧ true) c in CNF: c -b^{2, 1}_2 ∨ b^{2, 1}_1 ∨ b^{2, 1}_0 ∨ false c in DIMACS: -45 46 47 0 c 3 does not represent an automaton state. c -(-b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ true) c in CNF: c b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ false c in DIMACS: 45 -46 -47 0 c -3 does not represent an automaton state. c -( b^{2, 1}_2 ∧ b^{2, 1}_1 ∧ b^{2, 1}_0 ∧ true) c in CNF: c -b^{2, 1}_2 ∨ -b^{2, 1}_1 ∨ -b^{2, 1}_0 ∨ false c in DIMACS: -45 -46 -47 0 c i = 2 c -2+1 --> -1 c ( b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ p_4) -> ( b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0) c in CNF: c -b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ b^{2, 3}_2 c -b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_1 c -b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ b^{2, 3}_0 c in DIMACS: -48 -49 50 -4 51 0 -48 -49 50 -4 -52 0 -48 -49 50 -4 53 0 c -1+1 --> 0 c ( b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ p_4) -> (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ -b^{2, 3}_0) c in CNF: c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_2 c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_1 c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_0 c in DIMACS: -48 49 -50 -4 -51 0 -48 49 -50 -4 -52 0 -48 49 -50 -4 -53 0 c 0+1 --> 1 c (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ p_4) -> (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0) c in CNF: c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_2 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_1 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ b^{2, 3}_0 c in DIMACS: 48 49 50 -4 -51 0 48 49 50 -4 -52 0 48 49 50 -4 53 0 c 1+1 --> 2 c (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ p_4) -> (-b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0) c in CNF: c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_2 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ b^{2, 3}_1 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ -p_4 ∨ -b^{2, 3}_0 c in DIMACS: 48 49 -50 -4 -51 0 48 49 -50 -4 52 0 48 49 -50 -4 -53 0 c 2+1 --> break c (-b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ p_4) -> break c in CNF: c b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ -p_4 ∨ break c in DIMACS: 48 -49 50 -4 11 0 c 2-1 --> 1 c (-b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ -p_4) -> (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0) c in CNF: c b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_2 c b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_1 c b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ b^{2, 3}_0 c in DIMACS: 48 -49 50 4 -51 0 48 -49 50 4 -52 0 48 -49 50 4 53 0 c 1-1 --> 0 c (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ -p_4) -> (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ -b^{2, 3}_0) c in CNF: c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_2 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_1 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_0 c in DIMACS: 48 49 -50 4 -51 0 48 49 -50 4 -52 0 48 49 -50 4 -53 0 c 0-1 --> -1 c (-b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ -p_4) -> ( b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0) c in CNF: c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ b^{2, 3}_2 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_1 c b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ b^{2, 3}_0 c in DIMACS: 48 49 50 4 51 0 48 49 50 4 -52 0 48 49 50 4 53 0 c -1-1 --> -2 c ( b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ -p_4) -> ( b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0) c in CNF: c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ b^{2, 3}_2 c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ b^{2, 3}_1 c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ p_4 ∨ -b^{2, 3}_0 c in DIMACS: -48 49 -50 4 51 0 -48 49 -50 4 52 0 -48 49 -50 4 -53 0 c -2-1 --> break c ( b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ -p_4) -> break c in CNF: c -b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ p_4 ∨ break c in DIMACS: -48 -49 50 4 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{2, 2}_2 ∧ -b^{2, 2}_1 ∧ -b^{2, 2}_0 ∧ true) c in CNF: c -b^{2, 2}_2 ∨ b^{2, 2}_1 ∨ b^{2, 2}_0 ∨ false c in DIMACS: -48 49 50 0 c 3 does not represent an automaton state. c -(-b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ true) c in CNF: c b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ false c in DIMACS: 48 -49 -50 0 c -3 does not represent an automaton state. c -( b^{2, 2}_2 ∧ b^{2, 2}_1 ∧ b^{2, 2}_0 ∧ true) c in CNF: c -b^{2, 2}_2 ∨ -b^{2, 2}_1 ∨ -b^{2, 2}_0 ∨ false c in DIMACS: -48 -49 -50 0 c i = 3 c -2+1 --> -1 c ( b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ p_6) -> ( b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0) c in CNF: c -b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ b^{2, 4}_2 c -b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_1 c -b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ b^{2, 4}_0 c in DIMACS: -51 -52 53 -6 54 0 -51 -52 53 -6 -55 0 -51 -52 53 -6 56 0 c -1+1 --> 0 c ( b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ p_6) -> (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ -b^{2, 4}_0) c in CNF: c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_2 c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_1 c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_0 c in DIMACS: -51 52 -53 -6 -54 0 -51 52 -53 -6 -55 0 -51 52 -53 -6 -56 0 c 0+1 --> 1 c (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ p_6) -> (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0) c in CNF: c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_2 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_1 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ b^{2, 4}_0 c in DIMACS: 51 52 53 -6 -54 0 51 52 53 -6 -55 0 51 52 53 -6 56 0 c 1+1 --> 2 c (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ p_6) -> (-b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0) c in CNF: c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_2 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ b^{2, 4}_1 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ -p_6 ∨ -b^{2, 4}_0 c in DIMACS: 51 52 -53 -6 -54 0 51 52 -53 -6 55 0 51 52 -53 -6 -56 0 c 2+1 --> break c (-b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ p_6) -> break c in CNF: c b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ -p_6 ∨ break c in DIMACS: 51 -52 53 -6 11 0 c 2-1 --> 1 c (-b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ -p_6) -> (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0) c in CNF: c b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_2 c b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_1 c b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ b^{2, 4}_0 c in DIMACS: 51 -52 53 6 -54 0 51 -52 53 6 -55 0 51 -52 53 6 56 0 c 1-1 --> 0 c (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ -p_6) -> (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ -b^{2, 4}_0) c in CNF: c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_2 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_1 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_0 c in DIMACS: 51 52 -53 6 -54 0 51 52 -53 6 -55 0 51 52 -53 6 -56 0 c 0-1 --> -1 c (-b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ -p_6) -> ( b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0) c in CNF: c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ b^{2, 4}_2 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_1 c b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ b^{2, 4}_0 c in DIMACS: 51 52 53 6 54 0 51 52 53 6 -55 0 51 52 53 6 56 0 c -1-1 --> -2 c ( b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ -p_6) -> ( b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0) c in CNF: c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ b^{2, 4}_2 c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ b^{2, 4}_1 c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ p_6 ∨ -b^{2, 4}_0 c in DIMACS: -51 52 -53 6 54 0 -51 52 -53 6 55 0 -51 52 -53 6 -56 0 c -2-1 --> break c ( b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ -p_6) -> break c in CNF: c -b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ p_6 ∨ break c in DIMACS: -51 -52 53 6 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{2, 3}_2 ∧ -b^{2, 3}_1 ∧ -b^{2, 3}_0 ∧ true) c in CNF: c -b^{2, 3}_2 ∨ b^{2, 3}_1 ∨ b^{2, 3}_0 ∨ false c in DIMACS: -51 52 53 0 c 3 does not represent an automaton state. c -(-b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ true) c in CNF: c b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ false c in DIMACS: 51 -52 -53 0 c -3 does not represent an automaton state. c -( b^{2, 3}_2 ∧ b^{2, 3}_1 ∧ b^{2, 3}_0 ∧ true) c in CNF: c -b^{2, 3}_2 ∨ -b^{2, 3}_1 ∨ -b^{2, 3}_0 ∨ false c in DIMACS: -51 -52 -53 0 c i = 4 c -2+1 --> -1 c ( b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ p_8) -> ( b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0) c in CNF: c -b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ b^{2, 5}_2 c -b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_1 c -b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ b^{2, 5}_0 c in DIMACS: -54 -55 56 -8 57 0 -54 -55 56 -8 -58 0 -54 -55 56 -8 59 0 c -1+1 --> 0 c ( b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ p_8) -> (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ -b^{2, 5}_0) c in CNF: c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_2 c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_1 c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_0 c in DIMACS: -54 55 -56 -8 -57 0 -54 55 -56 -8 -58 0 -54 55 -56 -8 -59 0 c 0+1 --> 1 c (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ p_8) -> (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0) c in CNF: c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_2 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_1 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ b^{2, 5}_0 c in DIMACS: 54 55 56 -8 -57 0 54 55 56 -8 -58 0 54 55 56 -8 59 0 c 1+1 --> 2 c (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ p_8) -> (-b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0) c in CNF: c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_2 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ b^{2, 5}_1 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ -p_8 ∨ -b^{2, 5}_0 c in DIMACS: 54 55 -56 -8 -57 0 54 55 -56 -8 58 0 54 55 -56 -8 -59 0 c 2+1 --> break c (-b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ p_8) -> break c in CNF: c b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ -p_8 ∨ break c in DIMACS: 54 -55 56 -8 11 0 c 2-1 --> 1 c (-b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ -p_8) -> (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0) c in CNF: c b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_2 c b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_1 c b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ b^{2, 5}_0 c in DIMACS: 54 -55 56 8 -57 0 54 -55 56 8 -58 0 54 -55 56 8 59 0 c 1-1 --> 0 c (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ -p_8) -> (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ -b^{2, 5}_0) c in CNF: c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_2 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_1 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_0 c in DIMACS: 54 55 -56 8 -57 0 54 55 -56 8 -58 0 54 55 -56 8 -59 0 c 0-1 --> -1 c (-b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ -p_8) -> ( b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0) c in CNF: c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ b^{2, 5}_2 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_1 c b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ b^{2, 5}_0 c in DIMACS: 54 55 56 8 57 0 54 55 56 8 -58 0 54 55 56 8 59 0 c -1-1 --> -2 c ( b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ -p_8) -> ( b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0) c in CNF: c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ b^{2, 5}_2 c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ b^{2, 5}_1 c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ p_8 ∨ -b^{2, 5}_0 c in DIMACS: -54 55 -56 8 57 0 -54 55 -56 8 58 0 -54 55 -56 8 -59 0 c -2-1 --> break c ( b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ -p_8) -> break c in CNF: c -b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ p_8 ∨ break c in DIMACS: -54 -55 56 8 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{2, 4}_2 ∧ -b^{2, 4}_1 ∧ -b^{2, 4}_0 ∧ true) c in CNF: c -b^{2, 4}_2 ∨ b^{2, 4}_1 ∨ b^{2, 4}_0 ∨ false c in DIMACS: -54 55 56 0 c 3 does not represent an automaton state. c -(-b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ true) c in CNF: c b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ false c in DIMACS: 54 -55 -56 0 c -3 does not represent an automaton state. c -( b^{2, 4}_2 ∧ b^{2, 4}_1 ∧ b^{2, 4}_0 ∧ true) c in CNF: c -b^{2, 4}_2 ∨ -b^{2, 4}_1 ∨ -b^{2, 4}_0 ∨ false c in DIMACS: -54 -55 -56 0 c i = 5 c -2+1 --> -1 c ( b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ p_10) -> ( b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ b^{2, 6}_0) c in CNF: c -b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ b^{2, 6}_2 c -b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_1 c -b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ b^{2, 6}_0 c in DIMACS: -57 -58 59 -10 60 0 -57 -58 59 -10 -61 0 -57 -58 59 -10 62 0 c -1+1 --> 0 c ( b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ p_10) -> (-b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ -b^{2, 6}_0) c in CNF: c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_2 c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_1 c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_0 c in DIMACS: -57 58 -59 -10 -60 0 -57 58 -59 -10 -61 0 -57 58 -59 -10 -62 0 c 0+1 --> 1 c (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ p_10) -> (-b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ b^{2, 6}_0) c in CNF: c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_2 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_1 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ b^{2, 6}_0 c in DIMACS: 57 58 59 -10 -60 0 57 58 59 -10 -61 0 57 58 59 -10 62 0 c 1+1 --> 2 c (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ p_10) -> (-b^{2, 6}_2 ∧ b^{2, 6}_1 ∧ -b^{2, 6}_0) c in CNF: c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_2 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ b^{2, 6}_1 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ -p_10 ∨ -b^{2, 6}_0 c in DIMACS: 57 58 -59 -10 -60 0 57 58 -59 -10 61 0 57 58 -59 -10 -62 0 c 2+1 --> break c (-b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ p_10) -> break c in CNF: c b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ -p_10 ∨ break c in DIMACS: 57 -58 59 -10 11 0 c 2-1 --> 1 c (-b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ -p_10) -> (-b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ b^{2, 6}_0) c in CNF: c b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_2 c b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_1 c b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ b^{2, 6}_0 c in DIMACS: 57 -58 59 10 -60 0 57 -58 59 10 -61 0 57 -58 59 10 62 0 c 1-1 --> 0 c (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ -p_10) -> (-b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ -b^{2, 6}_0) c in CNF: c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_2 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_1 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_0 c in DIMACS: 57 58 -59 10 -60 0 57 58 -59 10 -61 0 57 58 -59 10 -62 0 c 0-1 --> -1 c (-b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ -p_10) -> ( b^{2, 6}_2 ∧ -b^{2, 6}_1 ∧ b^{2, 6}_0) c in CNF: c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ b^{2, 6}_2 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_1 c b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ b^{2, 6}_0 c in DIMACS: 57 58 59 10 60 0 57 58 59 10 -61 0 57 58 59 10 62 0 c -1-1 --> -2 c ( b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ -p_10) -> ( b^{2, 6}_2 ∧ b^{2, 6}_1 ∧ -b^{2, 6}_0) c in CNF: c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ b^{2, 6}_2 c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ b^{2, 6}_1 c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ p_10 ∨ -b^{2, 6}_0 c in DIMACS: -57 58 -59 10 60 0 -57 58 -59 10 61 0 -57 58 -59 10 -62 0 c -2-1 --> break c ( b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ -p_10) -> break c in CNF: c -b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ p_10 ∨ break c in DIMACS: -57 -58 59 10 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{2, 5}_2 ∧ -b^{2, 5}_1 ∧ -b^{2, 5}_0 ∧ true) c in CNF: c -b^{2, 5}_2 ∨ b^{2, 5}_1 ∨ b^{2, 5}_0 ∨ false c in DIMACS: -57 58 59 0 c 3 does not represent an automaton state. c -(-b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ true) c in CNF: c b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ false c in DIMACS: 57 -58 -59 0 c -3 does not represent an automaton state. c -( b^{2, 5}_2 ∧ b^{2, 5}_1 ∧ b^{2, 5}_0 ∧ true) c in CNF: c -b^{2, 5}_2 ∨ -b^{2, 5}_1 ∨ -b^{2, 5}_0 ∨ false c in DIMACS: -57 -58 -59 0 c INIT for k = 3 c -b^{3, 1}_2 c -b^{3, 1}_1 c -b^{3, 1}_0 c in DIMACS: -63 0 -64 0 -65 0 c Transitions for k = 3 c i = 1 c -2+1 --> -1 c ( b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ p_3) -> ( b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0) c in CNF: c -b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ b^{3, 2}_2 c -b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_1 c -b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ b^{3, 2}_0 c in DIMACS: -63 -64 65 -3 66 0 -63 -64 65 -3 -67 0 -63 -64 65 -3 68 0 c -1+1 --> 0 c ( b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ p_3) -> (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ -b^{3, 2}_0) c in CNF: c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_2 c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_1 c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_0 c in DIMACS: -63 64 -65 -3 -66 0 -63 64 -65 -3 -67 0 -63 64 -65 -3 -68 0 c 0+1 --> 1 c (-b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ p_3) -> (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0) c in CNF: c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_2 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_1 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ b^{3, 2}_0 c in DIMACS: 63 64 65 -3 -66 0 63 64 65 -3 -67 0 63 64 65 -3 68 0 c 1+1 --> 2 c (-b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ p_3) -> (-b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0) c in CNF: c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_2 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ b^{3, 2}_1 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ -p_3 ∨ -b^{3, 2}_0 c in DIMACS: 63 64 -65 -3 -66 0 63 64 -65 -3 67 0 63 64 -65 -3 -68 0 c 2+1 --> break c (-b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ p_3) -> break c in CNF: c b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ -p_3 ∨ break c in DIMACS: 63 -64 65 -3 11 0 c 2-1 --> 1 c (-b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ -p_3) -> (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0) c in CNF: c b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_2 c b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_1 c b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ b^{3, 2}_0 c in DIMACS: 63 -64 65 3 -66 0 63 -64 65 3 -67 0 63 -64 65 3 68 0 c 1-1 --> 0 c (-b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ -p_3) -> (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ -b^{3, 2}_0) c in CNF: c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_2 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_1 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_0 c in DIMACS: 63 64 -65 3 -66 0 63 64 -65 3 -67 0 63 64 -65 3 -68 0 c 0-1 --> -1 c (-b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ -p_3) -> ( b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0) c in CNF: c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ b^{3, 2}_2 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_1 c b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ b^{3, 2}_0 c in DIMACS: 63 64 65 3 66 0 63 64 65 3 -67 0 63 64 65 3 68 0 c -1-1 --> -2 c ( b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ -p_3) -> ( b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0) c in CNF: c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ b^{3, 2}_2 c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ b^{3, 2}_1 c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ p_3 ∨ -b^{3, 2}_0 c in DIMACS: -63 64 -65 3 66 0 -63 64 -65 3 67 0 -63 64 -65 3 -68 0 c -2-1 --> break c ( b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ -p_3) -> break c in CNF: c -b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ p_3 ∨ break c in DIMACS: -63 -64 65 3 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{3, 1}_2 ∧ -b^{3, 1}_1 ∧ -b^{3, 1}_0 ∧ true) c in CNF: c -b^{3, 1}_2 ∨ b^{3, 1}_1 ∨ b^{3, 1}_0 ∨ false c in DIMACS: -63 64 65 0 c 3 does not represent an automaton state. c -(-b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ true) c in CNF: c b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ false c in DIMACS: 63 -64 -65 0 c -3 does not represent an automaton state. c -( b^{3, 1}_2 ∧ b^{3, 1}_1 ∧ b^{3, 1}_0 ∧ true) c in CNF: c -b^{3, 1}_2 ∨ -b^{3, 1}_1 ∨ -b^{3, 1}_0 ∨ false c in DIMACS: -63 -64 -65 0 c i = 2 c -2+1 --> -1 c ( b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ p_6) -> ( b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0) c in CNF: c -b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ b^{3, 3}_2 c -b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_1 c -b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ b^{3, 3}_0 c in DIMACS: -66 -67 68 -6 69 0 -66 -67 68 -6 -70 0 -66 -67 68 -6 71 0 c -1+1 --> 0 c ( b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ p_6) -> (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ -b^{3, 3}_0) c in CNF: c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_2 c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_1 c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_0 c in DIMACS: -66 67 -68 -6 -69 0 -66 67 -68 -6 -70 0 -66 67 -68 -6 -71 0 c 0+1 --> 1 c (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ p_6) -> (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0) c in CNF: c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_2 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_1 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ b^{3, 3}_0 c in DIMACS: 66 67 68 -6 -69 0 66 67 68 -6 -70 0 66 67 68 -6 71 0 c 1+1 --> 2 c (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ p_6) -> (-b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0) c in CNF: c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_2 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ b^{3, 3}_1 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ -p_6 ∨ -b^{3, 3}_0 c in DIMACS: 66 67 -68 -6 -69 0 66 67 -68 -6 70 0 66 67 -68 -6 -71 0 c 2+1 --> break c (-b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ p_6) -> break c in CNF: c b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ -p_6 ∨ break c in DIMACS: 66 -67 68 -6 11 0 c 2-1 --> 1 c (-b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ -p_6) -> (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0) c in CNF: c b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_2 c b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_1 c b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ b^{3, 3}_0 c in DIMACS: 66 -67 68 6 -69 0 66 -67 68 6 -70 0 66 -67 68 6 71 0 c 1-1 --> 0 c (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ -p_6) -> (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ -b^{3, 3}_0) c in CNF: c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_2 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_1 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_0 c in DIMACS: 66 67 -68 6 -69 0 66 67 -68 6 -70 0 66 67 -68 6 -71 0 c 0-1 --> -1 c (-b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ -p_6) -> ( b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0) c in CNF: c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ b^{3, 3}_2 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_1 c b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ b^{3, 3}_0 c in DIMACS: 66 67 68 6 69 0 66 67 68 6 -70 0 66 67 68 6 71 0 c -1-1 --> -2 c ( b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ -p_6) -> ( b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0) c in CNF: c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ b^{3, 3}_2 c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ b^{3, 3}_1 c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ p_6 ∨ -b^{3, 3}_0 c in DIMACS: -66 67 -68 6 69 0 -66 67 -68 6 70 0 -66 67 -68 6 -71 0 c -2-1 --> break c ( b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ -p_6) -> break c in CNF: c -b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ p_6 ∨ break c in DIMACS: -66 -67 68 6 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{3, 2}_2 ∧ -b^{3, 2}_1 ∧ -b^{3, 2}_0 ∧ true) c in CNF: c -b^{3, 2}_2 ∨ b^{3, 2}_1 ∨ b^{3, 2}_0 ∨ false c in DIMACS: -66 67 68 0 c 3 does not represent an automaton state. c -(-b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ true) c in CNF: c b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ false c in DIMACS: 66 -67 -68 0 c -3 does not represent an automaton state. c -( b^{3, 2}_2 ∧ b^{3, 2}_1 ∧ b^{3, 2}_0 ∧ true) c in CNF: c -b^{3, 2}_2 ∨ -b^{3, 2}_1 ∨ -b^{3, 2}_0 ∨ false c in DIMACS: -66 -67 -68 0 c i = 3 c -2+1 --> -1 c ( b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ p_9) -> ( b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ b^{3, 4}_0) c in CNF: c -b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ b^{3, 4}_2 c -b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_1 c -b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ b^{3, 4}_0 c in DIMACS: -69 -70 71 -9 72 0 -69 -70 71 -9 -73 0 -69 -70 71 -9 74 0 c -1+1 --> 0 c ( b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ p_9) -> (-b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ -b^{3, 4}_0) c in CNF: c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_2 c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_1 c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_0 c in DIMACS: -69 70 -71 -9 -72 0 -69 70 -71 -9 -73 0 -69 70 -71 -9 -74 0 c 0+1 --> 1 c (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ p_9) -> (-b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ b^{3, 4}_0) c in CNF: c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_2 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_1 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ b^{3, 4}_0 c in DIMACS: 69 70 71 -9 -72 0 69 70 71 -9 -73 0 69 70 71 -9 74 0 c 1+1 --> 2 c (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ p_9) -> (-b^{3, 4}_2 ∧ b^{3, 4}_1 ∧ -b^{3, 4}_0) c in CNF: c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_2 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ b^{3, 4}_1 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ -p_9 ∨ -b^{3, 4}_0 c in DIMACS: 69 70 -71 -9 -72 0 69 70 -71 -9 73 0 69 70 -71 -9 -74 0 c 2+1 --> break c (-b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ p_9) -> break c in CNF: c b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ -p_9 ∨ break c in DIMACS: 69 -70 71 -9 11 0 c 2-1 --> 1 c (-b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ -p_9) -> (-b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ b^{3, 4}_0) c in CNF: c b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_2 c b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_1 c b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ b^{3, 4}_0 c in DIMACS: 69 -70 71 9 -72 0 69 -70 71 9 -73 0 69 -70 71 9 74 0 c 1-1 --> 0 c (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ -p_9) -> (-b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ -b^{3, 4}_0) c in CNF: c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_2 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_1 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_0 c in DIMACS: 69 70 -71 9 -72 0 69 70 -71 9 -73 0 69 70 -71 9 -74 0 c 0-1 --> -1 c (-b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ -p_9) -> ( b^{3, 4}_2 ∧ -b^{3, 4}_1 ∧ b^{3, 4}_0) c in CNF: c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ b^{3, 4}_2 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_1 c b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ b^{3, 4}_0 c in DIMACS: 69 70 71 9 72 0 69 70 71 9 -73 0 69 70 71 9 74 0 c -1-1 --> -2 c ( b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ -p_9) -> ( b^{3, 4}_2 ∧ b^{3, 4}_1 ∧ -b^{3, 4}_0) c in CNF: c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ b^{3, 4}_2 c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ b^{3, 4}_1 c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ p_9 ∨ -b^{3, 4}_0 c in DIMACS: -69 70 -71 9 72 0 -69 70 -71 9 73 0 -69 70 -71 9 -74 0 c -2-1 --> break c ( b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ -p_9) -> break c in CNF: c -b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ p_9 ∨ break c in DIMACS: -69 -70 71 9 11 0 c Disallowed combinations c 0b100 represents a "negated" zero. Not a state. c -( b^{3, 3}_2 ∧ -b^{3, 3}_1 ∧ -b^{3, 3}_0 ∧ true) c in CNF: c -b^{3, 3}_2 ∨ b^{3, 3}_1 ∨ b^{3, 3}_0 ∨ false c in DIMACS: -69 70 71 0 c 3 does not represent an automaton state. c -(-b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ true) c in CNF: c b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ false c in DIMACS: 69 -70 -71 0 c -3 does not represent an automaton state. c -( b^{3, 3}_2 ∧ b^{3, 3}_1 ∧ b^{3, 3}_0 ∧ true) c in CNF: c -b^{3, 3}_2 ∨ -b^{3, 3}_1 ∨ -b^{3, 3}_0 ∨ false c in DIMACS: -69 -70 -71 0