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