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