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