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