1 2 3 4 5 6 7 8 9 10 11
{ a ; b }. % Answer: 1 % % Answer: 2 % b % Answer: 3 % a % Answer: 4 % a b % SATISFIABLE