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