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