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