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