c generated from cruc5-105.in and triv5-105.in c Command: atmost2or3of5.awksh {-v sign=-1 cruc5-105.in | triv5-105.in} p cnf 105 320 -78 54 -23 0 -78 54 47 0 -78 54 -22 0 -78 -23 47 0 -78 -23 -22 0 -78 47 -22 0 54 -23 47 0 54 -23 -22 0 54 47 -22 0 -23 47 -22 0 -43 100 -10 89 0 81 100 -10 89 0 81 -43 -10 89 0 81 -43 100 89 0 81 -43 100 -10 0 -70 62 -73 0 -70 62 80 0 -70 62 -3 0 -70 -73 80 0 -70 -73 -3 0 -70 80 -3 0 62 -73 80 0 62 -73 -3 0 62 80 -3 0 -73 80 -3 0 -18 7 -34 99 0 94 7 -34 99 0 94 -18 -34 99 0 94 -18 7 99 0 94 -18 7 -34 0 -26 11 -75 0 -26 11 77 0 -26 11 -95 0 -26 -75 77 0 -26 -75 -95 0 -26 77 -95 0 11 -75 77 0 11 -75 -95 0 11 77 -95 0 -75 77 -95 0 -91 69 -82 46 0 30 69 -82 46 0 30 -91 -82 46 0 30 -91 69 46 0 30 -91 69 -82 0 -71 83 -102 0 -71 83 66 0 -71 83 -41 0 -71 -102 66 0 -71 -102 -41 0 -71 66 -41 0 83 -102 66 0 83 -102 -41 0 83 66 -41 0 -102 66 -41 0 -14 92 -85 12 0 40 92 -85 12 0 40 -14 -85 12 0 40 -14 92 12 0 40 -14 92 -85 0 -33 15 -103 0 -33 15 48 0 -33 15 -57 0 -33 -103 48 0 -33 -103 -57 0 -33 48 -57 0 15 -103 48 0 15 -103 -57 0 15 48 -57 0 -103 48 -57 0 -8 93 -65 58 0 38 93 -65 58 0 38 -8 -65 58 0 38 -8 93 58 0 38 -8 93 -65 0 -97 16 -67 0 -97 16 49 0 -97 16 -31 0 -97 -67 49 0 -97 -67 -31 0 -97 49 -31 0 16 -67 49 0 16 -67 -31 0 16 49 -31 0 -67 49 -31 0 -56 39 -50 13 0 51 39 -50 13 0 51 -56 -50 13 0 51 -56 39 13 0 51 -56 39 -50 0 -21 45 -6 0 -21 45 29 0 -21 45 -84 0 -21 -6 29 0 -21 -6 -84 0 -21 29 -84 0 45 -6 29 0 45 -6 -84 0 45 29 -84 0 -6 29 -84 0 -44 35 -68 96 0 24 35 -68 96 0 24 -44 -68 96 0 24 -44 35 96 0 24 -44 35 -68 0 -37 25 -19 0 -37 25 60 0 -37 25 -55 0 -37 -19 60 0 -37 -19 -55 0 -37 60 -55 0 25 -19 60 0 25 -19 -55 0 25 60 -55 0 -19 60 -55 0 -53 76 -101 98 0 42 76 -101 98 0 42 -53 -101 98 0 42 -53 76 98 0 42 -53 76 -101 0 -104 74 -1 0 -104 74 17 0 -104 74 -5 0 -104 -1 17 0 -104 -1 -5 0 -104 17 -5 0 74 -1 17 0 74 -1 -5 0 74 17 -5 0 -1 17 -5 0 -105 88 -52 87 0 27 88 -52 87 0 27 -105 -52 87 0 27 -105 88 87 0 27 -105 88 -52 0 -59 86 -9 0 -59 86 63 0 -59 86 -61 0 -59 -9 63 0 -59 -9 -61 0 -59 63 -61 0 86 -9 63 0 86 -9 -61 0 86 63 -61 0 -9 63 -61 0 -90 79 -2 72 0 20 79 -2 72 0 20 -90 -2 72 0 20 -90 79 72 0 20 -90 79 -2 0 -64 28 -32 0 -64 28 4 0 -64 28 -36 0 -64 -32 4 0 -64 -32 -36 0 -64 4 -36 0 28 -32 4 0 28 -32 -36 0 28 4 -36 0 -32 4 -36 0 78 -81 70 0 78 -81 -94 0 78 -81 26 0 78 70 -94 0 78 70 26 0 78 -94 26 0 -81 70 -94 0 -81 70 26 0 -81 -94 26 0 70 -94 26 0 -30 71 -40 33 0 -54 71 -40 33 0 -54 -30 -40 33 0 -54 -30 71 33 0 -54 -30 71 -40 0 23 -38 97 0 23 -38 -51 0 23 -38 21 0 23 97 -51 0 23 97 21 0 23 -51 21 0 -38 97 -51 0 -38 97 21 0 -38 -51 21 0 97 -51 21 0 -24 37 -42 104 0 -47 37 -42 104 0 -47 -24 -42 104 0 -47 -24 37 104 0 -47 -24 37 -42 0 22 -27 59 0 22 -27 -20 0 22 -27 64 0 22 59 -20 0 22 59 64 0 22 -20 64 0 -27 59 -20 0 -27 59 64 0 -27 -20 64 0 59 -20 64 0 91 8 53 -28 0 43 8 53 -28 0 43 91 53 -28 0 43 91 8 -28 0 43 91 8 53 0 -100 -83 -16 0 -100 -83 44 0 -100 -83 90 0 -100 -16 44 0 -100 -16 90 0 -100 44 90 0 -83 -16 44 0 -83 -16 90 0 -83 44 90 0 -16 44 90 0 14 56 -25 -86 0 10 56 -25 -86 0 10 14 -25 -86 0 10 14 56 -86 0 10 14 56 -25 0 -89 -15 -45 0 -89 -15 -74 0 -89 -15 105 0 -89 -45 -74 0 -89 -45 105 0 -89 -74 105 0 -15 -45 -74 0 -15 -45 105 0 -15 -74 105 0 -45 -74 105 0 -92 -93 -35 -88 0 -62 -93 -35 -88 0 -62 -92 -35 -88 0 -62 -92 -93 -88 0 -62 -92 -93 -35 0 73 103 67 0 73 103 -76 0 73 103 9 0 73 67 -76 0 73 67 9 0 73 -76 9 0 103 67 -76 0 103 67 9 0 103 -76 9 0 67 -76 9 0 -69 -39 1 -79 0 -80 -39 1 -79 0 -80 -69 1 -79 0 -80 -69 -39 -79 0 -80 -69 -39 1 0 3 102 6 0 3 102 19 0 3 102 32 0 3 6 19 0 3 6 32 0 3 19 32 0 102 6 19 0 102 6 32 0 102 19 32 0 6 19 32 0 82 -29 68 -63 0 18 -29 68 -63 0 18 82 68 -63 0 18 82 -29 -63 0 18 82 -29 68 0 -7 -48 65 0 -7 -48 -60 0 -7 -48 2 0 -7 65 -60 0 -7 65 2 0 -7 -60 2 0 -48 65 -60 0 -48 65 2 0 -48 -60 2 0 65 -60 2 0 -66 50 101 52 0 34 50 101 52 0 34 -66 101 52 0 34 -66 50 52 0 34 -66 50 101 0 -99 85 -49 0 -99 85 -17 0 -99 85 -4 0 -99 -49 -17 0 -99 -49 -4 0 -99 -17 -4 0 85 -49 -17 0 85 -49 -4 0 85 -17 -4 0 -49 -17 -4 0 -46 31 55 -87 0 -11 31 55 -87 0 -11 -46 55 -87 0 -11 -46 31 -87 0 -11 -46 31 55 0 75 41 -58 0 75 41 5 0 75 41 61 0 75 -58 5 0 75 -58 61 0 75 5 61 0 41 -58 5 0 41 -58 61 0 41 5 61 0 -58 5 61 0 -12 84 -98 -72 0 -77 84 -98 -72 0 -77 -12 -98 -72 0 -77 -12 84 -72 0 -77 -12 84 -98 0 95 57 -13 0 95 57 -96 0 95 57 36 0 95 -13 -96 0 95 -13 36 0 95 -96 36 0 57 -13 -96 0 57 -13 36 0 57 -96 36 0 -13 -96 36 0