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 50 218 41 -47 3 0 48 50 -44 0 -27 -29 -10 0 46 8 -49 0 -23 24 42 0 36 21 5 0 1 -2 24 0 34 -3 28 0 -19 -48 33 0 13 -4 -47 0 -42 -49 3 0 45 1 13 0 -20 -39 8 0 21 19 -5 0 9 -21 39 0 3 19 15 0 -17 -8 15 0 -35 -46 9 0 50 12 -28 0 -40 -23 -6 0 45 -30 1 0 -24 -1 -21 0 9 15 -42 0 27 7 46 0 -40 -1 34 0 -27 -24 40 0 41 -8 26 0 9 5 -21 0 35 -48 -30 0 -41 -47 -24 0 -13 -50 -24 0 -31 -40 -24 0 2 39 -50 0 36 9 12 0 -6 -1 -4 0 -13 -50 28 0 35 20 -50 0 -38 14 -24 0 -16 2 42 0 -35 23 -3 0 -17 -14 -39 0 4 -34 48 0 38 30 -24 0 -44 33 40 0 -38 -45 -29 0 30 -49 -44 0 -46 -47 28 0 -3 -37 50 0 15 -41 50 0 -12 15 -4 0 21 35 -34 0 -8 -49 23 0 4 45 9 0 20 -36 47 0 -30 -2 -37 0 19 -12 -26 0 28 33 50 0 21 -14 -30 0 44 21 32 0 -43 13 -42 0 -44 -17 -9 0 24 -25 -15 0 45 -12 -48 0 -10 -29 4 0 -46 35 -28 0 -20 -4 -49 0 -17 -23 15 0 15 42 18 0 -45 26 32 0 -13 14 8 0 -22 21 20 0 -15 -43 -24 0 11 -30 -48 0 17 -22 31 0 27 2 -12 0 37 23 49 0 -16 -36 12 0 20 42 -31 0 -16 -30 -48 0 1 -20 -39 0 -41 -22 -13 0 8 -44 20 0 20 3 43 0 27 -35 -37 0 -11 -32 -1 0 40 34 -8 0 37 31 30 0 -8 20 -15 0 -7 47 -17 0 23 -31 30 0 9 21 -7 0 -2 9 10 0 43 22 -30 0 40 28 46 0 -5 43 -47 0 6 -24 47 0 41 -29 50 0 14 -15 -39 0 10 -14 -34 0 20 -26 46 0 9 15 -20 0 11 46 18 0 20 -30 25 0 -46 9 23 0 29 -43 32 0 47 4 -38 0 6 -35 37 0 33 14 -32 0 -16 -18 39 0 -45 -25 5 0 -49 45 -4 0 28 -16 13 0 -17 -21 -49 0 -43 10 -18 0 26 -31 -35 0 -50 -24 40 0 -12 -1 -30 0 -43 -10 -6 0 -21 29 8 0 19 -35 45 0 -39 35 -47 0 45 32 24 0 -50 30 16 0 -10 44 -21 0 17 39 29 0 -8 -10 -49 0 30 10 -12 0 -13 16 -12 0 42 16 21 0 46 -30 -13 0 27 -7 47 0 4 -22 35 0 47 39 17 0 36 7 38 0 -31 -15 -30 0 -31 -16 -35 0 -2 44 49 0 38 6 -12 0 26 49 35 0 -14 -35 18 0 23 -9 22 0 -34 37 5 0 6 10 -19 0 -44 40 -31 0 -31 16 -20 0 -5 -32 -6 0 -38 23 -27 0 -5 10 24 0 -20 12 36 0 -29 -30 -41 0 32 21 -45 0 -45 -32 12 0 42 45 -21 0 20 -41 5 0 26 -17 -49 0 -5 -25 8 0 -34 28 -48 0 -8 5 -28 0 21 -39 -38 0 -44 -20 -42 0 -29 -40 -9 0 3 23 -19 0 33 26 37 0 -8 -23 -45 0 20 -41 -8 0 46 -12 33 0 46 1 45 0 -46 -34 -39 0 -39 -2 15 0 -21 -16 -3 0 22 -23 -47 0 26 -23 -45 0 33 32 30 0 -14 -2 25 0 -40 -5 37 0 28 5 37 0 18 34 36 0 -8 37 3 0 -11 -22 17 0 -6 -39 43 0 10 43 34 0 -34 41 13 0 -23 -15 7 0 -2 47 -1 0 -2 50 -21 0 -32 48 13 0 16 43 -27 0 25 -19 3 0 6 -45 -21 0 46 -43 -28 0 46 -15 -30 0 -23 12 -26 0 -45 -39 -49 0 -16 49 -42 0 -15 1 26 0 25 12 23 0 37 -43 -31 0 -42 -35 32 0 -38 -47 -24 0 -11 -48 -29 0 44 14 -7 0 35 5 20 0 -9 -8 -46 0 -16 35 24 0 -17 25 -5 0 -41 4 -8 0 -24 4 -30 0 4 27 -49 0 32 -36 49 0 -38 -23 10 0 23 37 -11 0 -44 -10 16 0 -41 5 15 0 16 3 -1 0 -19 -11 23 0 -32 -16 -42 0 -28 29 -8 0 4 -7 40 0 % 0