c mkcnf random cnf with seed 522186, max clause length 3 c FORCED SATISFIABLE c p cnf 50 215 49 44 28 0 -18 38 7 0 -13 26 40 0 -23 -16 -6 0 1 6 22 0 -26 -6 -20 0 -43 -2 14 0 -40 21 30 0 36 -21 -27 0 22 -16 6 0 -37 29 -26 0 -14 -16 18 0 -29 -10 -18 0 50 -41 7 0 1 -9 -39 0 -4 -43 -50 0 1 42 30 0 19 47 -9 0 -41 -17 -34 0 -8 -44 36 0 26 -28 41 0 -26 35 19 0 -35 11 -28 0 10 -42 27 0 37 -50 42 0 23 5 46 0 36 35 8 0 -19 45 21 0 -39 -30 14 0 -29 43 -42 0 -43 -28 6 0 6 -31 16 0 4 22 -45 0 -4 -39 29 0 46 -18 -23 0 7 -36 -28 0 15 -33 -44 0 23 16 -43 0 -30 -41 -1 0 -20 -14 26 0 25 44 -50 0 3 -40 2 0 -39 -10 -16 0 16 5 42 0 -22 -2 32 0 -42 44 -25 0 -19 -50 -32 0 4 -10 19 0 -41 -38 33 0 -7 29 -38 0 8 -17 -47 0 30 5 -17 0 43 30 -41 0 -17 11 -23 0 13 -32 26 0 -39 7 17 0 -35 -17 11 0 -50 -35 49 0 27 -2 35 0 9 44 -40 0 45 17 -29 0 -26 -30 -47 0 3 23 -44 0 -38 -48 21 0 12 49 -26 0 47 -38 22 0 -45 -22 38 0 23 37 1 0 3 12 16 0 -47 35 39 0 16 -44 15 0 42 -14 8 0 -45 40 28 0 -40 -3 27 0 -44 -9 12 0 35 33 19 0 -2 -14 12 0 -10 26 -14 0 -22 12 36 0 -19 31 16 0 -43 35 -12 0 39 -7 24 0 -14 31 10 0 -7 -21 10 0 14 41 4 0 -7 13 -49 0 5 31 18 0 23 25 30 0 -25 -34 -14 0 44 45 1 0 -47 -38 -17 0 28 -4 -13 0 -36 -4 50 0 8 -15 1 0 -45 -8 7 0 -9 7 -34 0 -2 36 -1 0 -15 19 -33 0 11 43 50 0 30 22 34 0 25 -5 -21 0 14 32 17 0 32 -35 39 0 9 -37 42 0 1 -19 -18 0 27 -36 5 0 45 16 32 0 19 30 -46 0 49 19 -32 0 -42 45 -32 0 2 -45 -30 0 -44 21 12 0 8 5 34 0 41 48 -45 0 -27 43 -1 0 -23 -30 7 0 -18 -47 -15 0 31 -20 -19 0 38 -46 16 0 48 23 -17 0 -41 34 -16 0 5 19 -2 0 23 -17 29 0 -7 17 -40 0 -49 -11 -26 0 48 -49 39 0 17 -33 4 0 -12 35 -5 0 18 9 27 0 -19 -38 -40 0 35 -42 44 0 17 2 -31 0 35 -5 14 0 14 -35 1 0 43 -9 2 0 50 34 -22 0 43 -1 -15 0 -11 -12 -32 0 -9 -2 -10 0 14 30 49 0 -18 39 -28 0 38 34 -46 0 2 35 -44 0 -5 49 42 0 27 -14 -42 0 20 -6 30 0 5 -44 26 0 -28 -16 -22 0 -43 45 36 0 -18 -28 44 0 -42 13 -15 0 -15 -43 24 0 8 10 7 0 15 -36 -32 0 41 4 -46 0 -15 -17 11 0 24 34 -35 0 39 -46 -50 0 -12 43 -24 0 9 5 28 0 -48 -41 -15 0 -7 32 34 0 -22 50 -38 0 -17 23 -37 0 -26 -31 40 0 48 8 -21 0 -46 32 37 0 26 39 -38 0 -21 -10 -27 0 -7 -13 -26 0 -17 48 -47 0 -12 -17 -32 0 -17 43 42 0 -43 12 -18 0 -39 1 36 0 38 -34 44 0 -24 1 -33 0 -48 19 18 0 18 23 -30 0 7 11 -49 0 41 -37 26 0 20 47 -15 0 16 -21 26 0 5 -40 43 0 42 -25 16 0 -6 -15 -25 0 13 4 22 0 13 43 -45 0 -22 -10 -16 0 43 38 -8 0 41 -20 -39 0 14 -9 50 0 50 12 17 0 -5 -45 -3 0 -23 26 43 0 3 -14 30 0 13 26 19 0 -25 35 23 0 44 14 -33 0 33 -37 -1 0 -22 -21 -33 0 20 49 18 0 -45 -5 39 0 8 21 37 0 -37 16 46 0 16 -26 47 0 -49 -6 28 0 11 30 48 0 -33 -10 -8 0 -19 -32 30 0 -22 12 -18 0 9 10 46 0 -50 -44 -8 0 -6 -20 43 0 11 8 26 0