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