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