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