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