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