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