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