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