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