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