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