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 7 -2 15 0 -16 -6 -3 0 -15 -2 10 0 -7 -15 -6 0 6 4 -2 0 -19 12 -18 0 2 -16 -18 0 16 6 -13 0 16 7 5 0 -18 13 4 0 -16 -20 1 0 6 -13 17 0 -14 -13 -6 0 13 1 -14 0 20 -5 11 0 -20 -15 19 0 -4 -12 -7 0 -13 12 -5 0 -4 -5 1 0 -8 -11 -6 0 3 11 15 0 5 -1 11 0 17 -11 -14 0 10 -1 -14 0 -14 -3 1 0 -13 4 15 0 19 -10 5 0 -19 -10 14 0 -6 -7 10 0 -15 -7 -4 0 15 10 2 0 -13 -2 16 0 -20 10 -19 0 3 -8 -12 0 -1 -2 -17 0 -11 -7 16 0 12 18 9 0 -12 5 2 0 1 -3 17 0 8 -19 6 0 -14 -4 -16 0 -4 6 15 0 -20 6 2 0 -13 9 -2 0 7 5 -17 0 -4 -13 -16 0 2 5 -11 0 9 -12 -13 0 -13 -6 -1 0 19 -16 8 0 12 -19 18 0 -6 17 -13 0 8 -15 10 0 -19 -7 12 0 10 -17 18 0 16 11 20 0 9 4 -20 0 -13 -4 -8 0 11 5 -10 0 19 -4 -16 0 19 -7 17 0 -10 17 4 0 -7 9 10 0 -10 -11 -8 0 -18 -12 -14 0 -14 -20 -8 0 -5 -9 -15 0 6 2 -5 0 -19 16 -14 0 -3 -7 -4 0 11 -19 -2 0 9 -19 8 0 -13 14 -11 0 12 -1 15 0 -16 10 -19 0 3 -7 16 0 17 16 -4 0 2 12 14 0 -4 5 10 0 12 18 -4 0 -7 13 -12 0 -10 -6 -16 0 10 -14 -8 0 -8 -1 3 0 2 -9 -8 0 -2 -18 -6 0 13 -2 -20 0 6 5 -14 0 -16 4 14 0 -14 9 10 0 -20 18 9 0 % 0