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