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