4
(x1 v -x2 v x4) ^ (x2 v x3 v -x1) ^ (x3 v -x1 V -x4)