3
(x1 v -x2 v x3) ^ (x1 v x2 v x3) ^ (x2 v -x1 v -x3)