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