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