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