12
(-x3 v -x7 v x1) ^ (-x3 v -x2 v x5) ^ (-x12 v -x1 v x4) ^ (x9 v x12 v x6) ^ (-x3 v -x12 v -x11) ^ (-x12 v -x2 v -x3) ^ (-x5 v -x8 v x6) ^ (x3 v x7 v x5) ^ (-x11 v x7 v x8) ^ (-x12 v -x6 v -x5) ^ (x3 v x5 v x8) ^ (x6 v x3 v x12) ^ (x3 v x10 v x8) ^ (x8 v -x10 v -x5) ^ (-x4 v -x5 v -x3) ^ (-x11 v x12 v -x9) ^ (-x10 v -x9 v -x8) ^ (x9 v x2 v x10) ^ (x4 v -x2 v x1) ^ (x7 v -x5 v -x2)