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