
| 39                                                                                             |                                                                                                                                                                                                                                            |                     |                   |    |
|------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------------|-------------------|----|
| Configuration                                                                                  | Formula                                                                                                                                                                                                                                    |                     |                   |    |
| 2                                                                                              | (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → stubi) ∧ ¬(flex i ∧ flex j ) ∧ ¬(flex i ∧ stubj ) ∧ ¬(flex j ∧ stubi)                                                                                                                     |                     |                   |    |
| 3                                                                                              | (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → stubi) ∧ ¬(flex i ∧ flex j ) ∧ (flex i ∨ stubj ) ∧ ¬(flex i → stubj ) ∧ ¬(stubj → flex i ) ∧ ¬(flex j ∧ stubi)                                                                            |                     |                   |    |
| 4                                                                                              | (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → stubi) ∧ ¬(flex i ∧ flex j ) ∧ ¬(flex i ∧ stubj ) ∧ (flex j ∨ stubi) ∧ ¬(flex j → stubi) ∧ ¬(stubi ∨ flex j )                                                                             |                     |                   |    |
| 5                                                                                              | (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → stubi) ∧ ¬(flex i ∧ flex j ) ∧ ¬(flex i ∧ stubj ) ∧ (flex j → stubi)                                                                                                                      |                     |                   |    |
| 6                                                                                              | (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → stubi) ∧ ¬(flex i ∧ flex j ) ∧ (flex i → stubj ) ∧ ¬(flex j ∧ stubi) (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj →                                                                     |                     |                   |    |
| 9                                                                                              | stubi) ∧ ¬(flex i ∧ flex j ) ∧ (flex i ∨ stubj ) ∧ ¬(flex i                                                                                                                                                                                | →                   |                   |    |
| stubj ) ∧ ¬(stubj → flex i ) ∧ (flex j ∨ stubi) ∧ ¬(flex j → stubi) ∧ ¬(stubi → flex j )       |                                                                                                                                                                                                                                            |                     |                   |    |
| 10                                                                                             | (stubi ∨ stubj ) ∧ ¬(stubi                                                                                                                                                                                                                 | →                   | stubj ) ∧ ¬(stubj | →  |
| stubi) ∧ ¬(flex i ∧ flex j ) ∧ (flex i                                                         | →                                                                                                                                                                                                                                          | stubj ) ∧ (flex j ∨ |                   |    |
| stubi) ∧ ¬(flex j → stubi) ∧ ¬(stubi → flex j )                                                |                                                                                                                                                                                                                                            |                     |                   |    |
| 11                                                                                             | (stubi ∨ stubj ) ∧ ¬(stubi                                                                                                                                                                                                                 | →                   | stubj ) ∧ ¬(stubj | →  |
| stubi) ∧ ¬(flex i ∧ flex j ) ∧ (flex i ∨ stubj ) ∧ ¬(flex i                                    | →                                                                                                                                                                                                                                          |                     |                   |    |
| stubj ) ∧ ¬(stubj → flex i ) ∧ (flex j → stubi) (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj | →                                                                                                                                                                                                                                          |                     |                   |    |
| 14                                                                                             | stubi) ∧ (flex i ∨ flex j ) ∧ ¬(flex i → flex j ) ∧ ¬(flex j → flex i ) ∧ (flex i ∨ stubj ) ∧ ¬(flex i → stubj ) ∧ ¬(stubj → flex i )∧(flex j∨stubi)∧¬(flex j → stubi)∧¬(stubi → flex j ) (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj → |                     |                   |    |
| 15                                                                                             | stubi) ∧ (flex i ∨ flex j ) ∧ ¬(flex i → flex j ) ∧ ¬(flex j → flex i ) ∧ (flex i → stubj ) ∧ (flex j ∨ stubi) ∧ ¬(flex j → stubi) ∧ ¬(stubi → flex j ) (stubi ∨ stubj ) ∧ ¬(stubi → stubj ) ∧ ¬(stubj →                                   |                     |                   |    |
| 16                                                                                             | stubi) ∧ (flex i ∨ flex j ) ∧ ¬(flex i → flex j ) ∧ ¬(flex j → flex i ) ∧ (flex i ∨ stubj ) ∧ ¬(flex i → stubj ) ∧ ¬(stubj → flex i ) ∧ (flex j → stubi) Continued on next page                                                            |                     |                   |    |
