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 100 430 -68 -62 -10 0 10 95 24 0 -93 29 8 0 -24 79 80 0 22 -16 -42 0 5 35 -54 0 -66 -32 -48 0 -90 53 -17 0 22 48 30 0 -22 -40 63 0 56 -80 -64 0 63 60 -17 0 98 39 -29 0 -66 -57 1 0 42 80 59 0 -34 100 14 0 -83 -71 68 0 75 -78 -54 0 -57 46 -58 0 -93 84 -35 0 30 26 -82 0 9 -6 -57 0 -83 -64 27 0 43 -13 -62 0 77 -56 -49 0 -79 81 2 0 50 16 41 0 80 -5 90 0 -23 33 57 0 -49 10 75 0 -73 -100 6 0 10 -29 -50 0 95 56 66 0 24 79 -67 0 -56 21 -61 0 -25 41 93 0 -8 10 -33 0 -34 20 -39 0 -9 -45 -63 0 61 -7 96 0 -8 -83 -78 0 5 89 87 0 -21 -79 -32 0 44 -86 98 0 -81 22 55 0 -12 51 -96 0 -67 -55 65 0 -66 -13 -89 0 51 16 -48 0 -2 -33 -51 0 -90 -26 59 0 -45 31 100 0 -64 35 -97 0 13 23 -60 0 46 57 -7 0 -13 58 -28 0 36 -65 -62 0 -98 21 67 0 72 -50 -42 0 -87 -39 -22 0 -63 -74 12 0 52 100 -10 0 -84 -31 17 0 79 -62 -93 0 86 -80 -25 0 61 35 72 0 -76 -25 27 0 72 -89 -38 0 1 40 -75 0 7 -12 -85 0 75 19 -32 0 -63 18 81 0 11 79 27 0 31 2 -46 0 65 30 -90 0 -21 -17 92 0 -8 26 -52 0 -27 -26 37 0 59 5 -38 0 -82 74 90 0 45 -43 49 0 70 -2 -38 0 80 -17 -79 0 -54 29 -58 0 52 -15 -41 0 73 -30 -6 0 -34 -36 -2 0 23 -37 -8 0 54 -7 6 0 78 -49 53 0 -81 -62 68 0 -87 -17 69 0 -79 10 63 0 -64 22 70 0 -53 -67 -61 0 52 18 67 0 25 17 -70 0 -91 13 -57 0 41 -88 94 0 -19 -16 79 0 79 -39 -52 0 47 1 -70 0 -10 -4 86 0 39 21 -97 0 44 50 -74 0 56 -9 -98 0 60 1 -75 0 -2 -26 -91 0 -97 -32 92 0 51 7 73 0 -83 -11 -81 0 -49 -66 29 0 -79 8 -7 0 -63 -32 -69 0 5 1 -64 0 -12 -11 77 0 -46 49 -8 0 -91 -5 -97 0 75 -34 28 0 -34 93 23 0 62 33 -61 0 -79 71 9 0 -75 35 40 0 -67 6 44 0 17 -82 25 0 89 -39 78 0 9 56 73 0 -51 -16 -53 0 1 54 90 0 -76 64 -20 0 45 91 36 0 -25 -47 67 0 -15 14 24 0 51 4 63 0 -79 23 -75 0 94 -66 67 0 41 13 52 0 16 -25 29 0 49 -43 -36 0 -23 -62 5 0 73 -53 -92 0 -44 22 93 0 11 -46 27 0 72 34 62 0 -90 -67 -6 0 21 -35 -16 0 -93 18 19 0 87 -25 -94 0 -32 36 -11 0 37 33 -23 0 6 -49 -21 0 19 54 12 0 -86 24 50 0 -57 -69 -49 0 23 99 -25 0 -31 -46 -100 0 -45 85 -15 0 81 -7 76 0 -44 42 81 0 84 -31 -41 0 -59 -7 -27 0 20 -2 -78 0 -86 -38 -6 0 -74 11 33 0 97 -86 72 0 19 53 54 0 39 -31 -12 0 17 51 -7 0 14 86 -85 0 -87 -37 -73 0 -6 93 19 0 -71 -77 60 0 -51 10 -76 0 31 -45 73 0 -3 77 48 0 -42 -40 -15 0 89 -69 29 0 74 -2 -31 0 37 90 -7 0 -21 -8 74 0 91 -25 47 0 -56 73 -14 0 6 94 66 0 100 -79 14 0 -4 -9 27 0 84 -67 35 0 -75 27 91 0 53 -17 5 0 -43 -53 26 0 75 63 -22 0 11 -22 65 0 -64 25 -62 0 -66 -65 90 0 18 -25 -97 0 -57 -56 -18 0 77 68 78 0 76 77 -54 0 -11 -96 31 0 43 84 38 0 95 -84 74 0 69 -38 98 0 75 -54 87 0 93 2 -13 0 -36 -44 -62 0 -91 -78 72 0 -94 59 71 0 2 -78 88 0 98 -95 -16 0 57 40 55 0 -21 -100 14 0 -79 -48 -17 0 -71 30 -67 0 -62 -32 55 0 71 9 89 0 -68 58 11 0 29 -21 -48 0 -10 61 -29 0 -37 -80 95 0 41 -28 -56 0 -41 20 -51 0 -52 -30 14 0 98 -85 -65 0 -89 -98 64 0 -29 -30 -47 0 77 -1 19 0 21 4 51 0 39 1 -10 0 87 -15 -69 0 70 26 87 0 16 86 -46 0 55 -34 1 0 31 7 3 0 -11 97 43 0 37 16 -65 0 69 -47 -59 0 12 36 -6 0 14 71 -81 0 -46 22 87 0 -27 -38 -48 0 65 29 26 0 96 -54 -42 0 -76 -79 -53 0 47 41 -86 0 66 56 -25 0 93 11 -14 0 -25 30 -9 0 49 -7 53 0 -65 9 89 0 -37 8 73 0 -46 13 -31 0 15 55 94 0 98 -70 -32 0 -98 -36 3 0 -4 -23 -52 0 97 -30 85 0 -91 4 -70 0 10 -24 60 0 34 -71 -66 0 82 61 -75 0 -5 -34 -88 0 -3 51 80 0 63 -44 30 0 54 -18 74 0 71 -36 92 0 -3 -73 63 0 67 64 73 0 -52 98 51 0 -84 -74 52 0 -88 64 42 0 -7 11 82 0 -91 68 6 0 70 66 -39 0 54 -31 33 0 -13 -75 -89 0 64 60 8 0 -88 -19 -77 0 -34 -51 57 0 -32 25 34 0 -91 -42 96 0 -76 60 8 0 -92 55 -68 0 -19 -87 15 0 -23 81 -53 0 -78 53 69 0 32 8 -24 0 -6 -4 14 0 32 -7 -36 0 65 21 -73 0 -90 86 -36 0 -75 -73 92 0 -58 -93 -6 0 -20 97 -1 0 47 8 20 0 4 -13 -14 0 23 46 28 0 17 -2 -7 0 17 92 69 0 16 94 19 0 -64 -17 56 0 -32 -79 72 0 -73 9 -17 0 52 -47 81 0 -32 80 21 0 93 -79 50 0 75 86 -83 0 -62 -17 83 0 68 -48 61 0 -75 100 4 0 -29 -43 -97 0 -83 66 -38 0 40 -74 -99 0 -36 -20 42 0 20 44 -9 0 41 67 -1 0 89 -27 -57 0 8 -32 -41 0 100 -90 -13 0 -51 5 -24 0 16 68 -29 0 -8 94 -100 0 -32 27 -23 0 -66 -33 65 0 -59 -24 -55 0 -45 99 -50 0 47 -23 -49 0 -37 -18 95 0 -35 56 60 0 50 -93 57 0 86 -21 -37 0 90 -40 -74 0 -6 -23 -78 0 -28 17 -25 0 -20 -67 51 0 -16 -58 47 0 -4 82 -80 0 37 25 -89 0 84 52 88 0 66 58 71 0 -42 49 -99 0 29 -5 -73 0 -74 19 16 0 33 17 92 0 -24 89 87 0 36 46 -69 0 -26 -63 -74 0 90 45 73 0 46 -39 22 0 -67 -81 34 0 74 11 84 0 -12 -71 80 0 40 -58 -94 0 19 10 -39 0 86 -13 -77 0 57 -40 61 0 57 -93 76 0 -86 18 -2 0 80 -49 75 0 -14 -75 -34 0 41 -50 39 0 -6 -46 -13 0 26 68 9 0 -93 28 -87 0 88 60 51 0 -21 -89 -93 0 -80 -96 28 0 -84 3 77 0 31 -22 -52 0 94 -77 57 0 -87 -19 -94 0 -61 -59 -80 0 -98 36 -59 0 -99 -58 -10 0 48 68 -76 0 9 -98 -93 0 -87 38 -30 0 -22 -23 16 0 -68 96 -100 0 -76 -93 -43 0 24 5 51 0 87 -94 -64 0 97 -81 12 0 -55 28 4 0 -30 80 42 0 -25 -54 -44 0 -2 -56 45 0 -55 -68 84 0 -75 -35 -72 0 -29 -19 -56 0 -9 -14 40 0 2 -90 66 0 50 -9 -4 0 78 50 18 0 25 57 -81 0 -35 28 7 0 89 -6 81 0 84 69 21 0 95 92 22 0 68 77 -54 0 14 38 95 0 36 12 -17 0 -33 30 -46 0 -57 -42 -80 0 -8 -52 -76 0 28 14 16 0 -34 -69 -51 0 -28 -17 -27 0 60 26 -16 0 39 -12 -52 0 93 100 -65 0 -48 56 66 0 96 34 67 0 97 66 -61 0 -13 -44 78 0 -15 -51 -50 0 77 7 27 0 -93 1 -66 0 -94 20 36 0 -21 44 84 0 -48 23 92 0 -68 79 -57 0 -26 -14 -61 0 -61 66 3 0 37 41 -78 0 -61 -86 7 0 -2 49 87 0 -19 -67 -22 0 -63 18 -59 0 -100 -51 -20 0 -62 -31 43 0 -78 84 73 0 % 0