( let a in let !b in cnf ( (a !b) (!a b)) let !b in cnf ( (b) sat) cnf ( () sat) )