c This Formular is generated by mcnf c c horn? no c forced? no c mixed sat? no c clause length = 3 c p cnf 20 91 -15 -9 -19 0 -8 -4 -5 0 2 5 -20 0 19 5 -16 0 -13 16 7 0 -13 -20 12 0 -7 -18 -10 0 -5 15 -4 0 -13 -14 11 0 10 -15 -13 0 14 20 -6 0 11 -7 -20 0 -7 15 -4 0 -6 2 17 0 8 -18 14 0 2 17 14 0 -16 -13 5 0 -4 -7 -14 0 -17 4 -16 0 -3 6 -11 0 -12 19 -13 0 12 -18 1 0 13 -17 11 0 6 8 -13 0 -19 5 10 0 6 -7 -20 0 14 -9 17 0 15 12 2 0 -15 -14 9 0 -2 18 17 0 2 11 -4 0 -18 10 -17 0 -15 3 10 0 3 -4 -11 0 -2 -13 -15 0 19 8 3 0 -20 -19 6 0 -7 -9 18 0 -20 2 15 0 -15 -20 -5 0 -16 -20 -1 0 -16 -18 -5 0 19 -11 -16 0 -11 -14 -10 0 -5 -16 -2 0 -13 -15 10 0 -9 -19 -20 0 -3 13 -7 0 9 -16 -7 0 -1 15 9 0 -7 -4 -11 0 7 16 -14 0 4 10 3 0 -7 -14 -5 0 -5 -18 -11 0 14 -18 -3 0 -19 3 15 0 3 -12 -5 0 -8 10 -18 0 -4 -5 6 0 -10 14 7 0 11 13 20 0 6 -12 13 0 4 -20 19 0 16 -4 10 0 -6 10 20 0 -18 -13 2 0 -19 -1 14 0 -1 -14 7 0 -4 -11 10 0 20 17 9 0 -15 -11 4 0 11 -7 -14 0 15 20 -14 0 -20 16 -11 0 -7 6 -10 0 -1 10 5 0 2 9 -1 0 19 1 9 0 -8 3 16 0 -5 14 -16 0 1 -2 4 0 -12 -15 -14 0 7 16 -15 0 11 -5 15 0 -14 7 -17 0 -14 9 -15 0 10 -16 13 0 8 -9 3 0 -1 -2 9 0 -17 -4 -9 0 % 0