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