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