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