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