p cnf 83 570 -1 -4 61 63 0 -1 -4 61 66 0 -1 -7 50 51 52 63 0 -1 -7 50 51 52 73 0 -1 -7 61 63 0 -1 -7 61 66 0 -1 -8 50 51 52 63 0 -1 -8 50 51 52 73 0 -1 -9 50 51 52 63 0 -1 -9 50 51 52 73 0 -1 -10 50 51 52 63 0 -1 -10 50 51 52 73 0 -1 -11 50 51 52 63 0 -1 -11 50 51 52 73 0 -1 -12 50 51 52 63 0 -1 -12 50 51 52 73 0 -1 -13 49 61 63 0 -1 -13 49 61 66 0 -1 -16 26 63 0 -1 -16 26 73 0 -1 -17 26 63 0 -1 -17 26 73 0 -1 -17 61 63 0 -1 -17 61 66 0 -1 -18 26 63 0 -1 -18 26 73 0 -1 -18 61 63 0 -1 -18 61 66 0 -1 -19 61 63 0 -1 -19 61 66 0 -1 -20 61 63 0 -1 -20 61 66 0 -1 -21 61 63 0 -1 -21 61 66 0 -1 -22 61 63 0 -1 -22 61 66 0 -1 -23 61 63 0 -1 -23 61 66 0 -1 -24 61 63 0 -1 -24 61 66 0 -1 37 -49 64 0 -1 37 -49 70 0 -1 -69 0 -1 -70 0 -1 -71 0 -2 -4 61 63 0 -2 -4 61 66 0 -2 -7 61 63 0 -2 -7 61 66 0 -2 -14 49 61 63 0 -2 -14 49 61 66 0 -2 -17 61 63 0 -2 -17 61 66 0 -2 -18 61 63 0 -2 -18 61 66 0 -2 -19 61 63 0 -2 -19 61 66 0 -2 -20 61 63 0 -2 -20 61 66 0 -2 -21 61 63 0 -2 -21 61 66 0 -2 -22 61 63 0 -2 -22 61 66 0 -2 -23 61 63 0 -2 -23 61 66 0 -2 -24 61 63 0 -2 -24 61 66 0 -2 38 -49 64 0 -2 38 -49 70 0 -2 -49 64 0 -2 -49 70 0 -3 -4 61 63 0 -3 -4 61 66 0 -3 -7 61 63 0 -3 -7 61 66 0 -3 -15 49 61 63 0 -3 -15 49 61 66 0 -3 -17 61 63 0 -3 -17 61 66 0 -3 -18 61 63 0 -3 -18 61 66 0 -3 -19 61 63 0 -3 -19 61 66 0 -3 -20 61 63 0 -3 -20 61 66 0 -3 -21 61 63 0 -3 -21 61 66 0 -3 -22 61 63 0 -3 -22 61 66 0 -3 -23 61 63 0 -3 -23 61 66 0 -3 -24 61 63 0 -3 -24 61 66 0 -3 39 -49 64 0 -3 39 -49 70 0 -4 -7 61 63 0 -4 -7 61 66 0 -4 -13 50 51 63 0 -4 -13 50 51 73 0 -4 -14 50 51 63 0 -4 -14 50 51 73 0 -4 -15 50 51 63 0 -4 -15 50 51 73 0 -4 -16 26 63 0 -4 -16 26 73 0 -4 -16 27 -28 50 51 -61 63 0 -4 -16 27 -28 50 51 -61 74 0 -4 -16 49 61 63 0 -4 -16 49 61 66 0 -4 -16 50 51 63 0 -4 -16 50 51 73 0 -4 -17 25 -28 -29 50 51 -61 63 0 -4 -17 25 -28 -29 50 51 -61 72 0 -4 -17 26 63 0 -4 -17 26 73 0 -4 -17 27 -28 -29 50 51 -61 63 0 -4 -17 27 -28 -29 50 51 -61 74 0 -4 -17 50 51 63 0 -4 -17 50 51 73 0 -4 -18 25 -28 -30 50 51 -61 63 0 -4 -18 25 -28 -30 50 51 -61 72 0 -4 -18 26 63 0 -4 -18 26 73 0 -4 -18 50 51 63 0 -4 -18 50 51 73 0 -4 -20 61 63 0 -4 -20 61 66 0 -4 -21 61 63 0 -4 -21 61 66 0 -4 -22 61 63 0 -4 -22 61 66 0 -4 -23 61 63 0 -4 -23 61 66 0 -4 -24 61 63 0 -4 -24 61 66 0 -4 -25 -49 64 0 -4 25 -49 65 0 -4 25 -49 70 0 -4 -25 -49 72 0 -4 -26 -49 64 0 -4 26 -49 65 0 -4 26 -49 70 0 -4 -26 -49 73 0 -4 -27 -49 64 0 -4 27 -49 65 0 -4 27 -49 70 0 -4 -27 -49 74 0 -5 -7 61 63 0 -5 -7 61 66 0 -5 -13 50 51 63 0 -5 -13 50 51 73 0 -5 -14 50 51 63 0 -5 -14 50 51 73 0 -5 -15 50 51 63 0 -5 -15 50 51 73 0 -5 -16 27 -28 -29 50 51 -61 63 0 -5 -16 27 -28 -29 50 51 -61 74 0 -5 -16 50 51 63 0 -5 -16 50 51 73 0 -5 -17 25 -29 50 51 -61 63 0 -5 -17 25 -29 50 51 -61 72 0 -5 -17 27 -29 50 51 -61 63 0 -5 -17 27 -29 50 51 -61 74 0 -5 -17 49 61 63 0 -5 -17 49 61 66 0 -5 -17 50 51 63 0 -5 -17 50 51 73 0 -5 -18 25 -29 -30 50 51 -61 63 0 -5 -18 25 -29 -30 50 51 -61 72 0 -5 -18 50 51 63 0 -5 -18 50 51 73 0 -5 -20 61 63 0 -5 -20 61 66 0 -5 -21 61 63 0 -5 -21 61 66 0 -5 -22 61 63 0 -5 -22 61 66 0 -5 -23 61 63 0 -5 -23 61 66 0 -5 -24 61 63 0 -5 -24 61 66 0 -5 -25 -49 64 0 -5 25 -49 65 0 -5 25 -49 70 0 -5 -25 -49 72 0 -5 -26 -49 64 0 -5 26 -49 65 0 -5 26 -49 70 0 -5 -26 -49 73 0 -5 -27 -49 64 0 -5 27 -49 65 0 -5 27 -49 70 0 -5 -27 -49 74 0 -6 -7 61 63 0 -6 -7 61 66 0 -6 -13 50 51 63 0 -6 -13 50 51 73 0 -6 -14 50 51 63 0 -6 -14 50 51 73 0 -6 -15 50 51 63 0 -6 -15 50 51 73 0 -6 -16 27 -28 -30 50 51 -61 63 0 -6 -16 27 -28 -30 50 51 -61 74 0 -6 -16 50 51 63 0 -6 -16 50 51 73 0 -6 -17 25 -29 -30 50 51 -61 63 0 -6 -17 25 -29 -30 50 51 -61 72 0 -6 -17 27 -29 -30 50 51 -61 63 0 -6 -17 27 -29 -30 50 51 -61 74 0 -6 -17 50 51 63 0 -6 -17 50 51 73 0 -6 -18 25 -30 50 51 -61 63 0 -6 -18 25 -30 50 51 -61 72 0 -6 -18 49 61 63 0 -6 -18 49 61 66 0 -6 -18 50 51 63 0 -6 -18 50 51 73 0 -6 -20 61 63 0 -6 -20 61 66 0 -6 -21 61 63 0 -6 -21 61 66 0 -6 -22 61 63 0 -6 -22 61 66 0 -6 -23 61 63 0 -6 -23 61 66 0 -6 -24 61 63 0 -6 -24 61 66 0 -6 -25 -49 64 0 -6 25 -49 65 0 -6 25 -49 70 0 -6 -25 -49 72 0 -6 -26 -49 64 0 -6 26 -49 65 0 -6 26 -49 70 0 -6 -26 -49 73 0 -6 -27 -49 64 0 -6 27 -49 65 0 -6 27 -49 70 0 -6 -27 -49 74 0 -7 -13 50 51 63 0 -7 -13 50 51 73 0 -7 -14 50 51 52 63 0 -7 -14 50 51 52 73 0 -7 -14 50 51 63 0 -7 -14 50 51 73 0 -7 -15 50 51 52 63 0 -7 -15 50 51 52 73 0 -7 -15 50 51 63 0 -7 -15 50 51 73 0 -7 -16 27 -28 -31 50 51 -61 63 0 -7 -16 27 -28 -31 50 51 -61 74 0 -7 -16 50 51 52 63 0 -7 -16 50 51 52 73 0 -7 -16 50 51 63 0 -7 -16 50 51 73 0 -7 -17 25 -29 -31 50 51 -61 63 0 -7 -17 25 -29 -31 50 51 -61 72 0 -7 -17 27 -29 -31 50 51 -61 63 0 -7 -17 27 -29 -31 50 51 -61 74 0 -7 -17 50 51 52 63 0 -7 -17 50 51 52 73 0 -7 -17 50 51 63 0 -7 -17 50 51 73 0 -7 -18 25 -30 -31 50 51 -61 63 0 -7 -18 25 -30 -31 50 51 -61 72 0 -7 -18 50 51 52 63 0 -7 -18 50 51 52 73 0 -7 -18 50 51 63 0 -7 -18 50 51 73 0 -7 -19 49 61 63 0 -7 -19 49 61 66 0 -7 -49 64 0 -7 -49 67 0 -8 -13 50 51 63 0 -8 -13 50 51 73 0 -8 -14 50 51 52 63 0 -8 -14 50 51 52 73 0 -8 -14 50 51 63 0 -8 -14 50 51 73 0 -8 -15 50 51 52 63 0 -8 -15 50 51 52 73 0 -8 -15 50 51 63 0 -8 -15 50 51 73 0 -8 -16 27 -28 -32 50 51 -61 63 0 -8 -16 27 -28 -32 50 51 -61 74 0 -8 -16 50 51 52 63 0 -8 -16 50 51 52 73 0 -8 -16 50 51 63 0 -8 -16 50 51 73 0 -8 -17 25 -29 -32 50 51 -61 63 0 -8 -17 25 -29 -32 50 51 -61 72 0 -8 -17 27 -29 -32 50 51 -61 63 0 -8 -17 27 -29 -32 50 51 -61 74 0 -8 -17 50 51 52 63 0 -8 -17 50 51 52 73 0 -8 -17 50 51 63 0 -8 -17 50 51 73 0 -8 -18 25 -30 -32 50 51 -61 63 0 -8 -18 25 -30 -32 50 51 -61 72 0 -8 -18 50 51 52 63 0 -8 -18 50 51 52 73 0 -8 -18 50 51 63 0 -8 -18 50 51 73 0 -8 -20 49 61 63 0 -8 -20 49 61 66 0 -8 -49 64 0 -8 -49 67 0 -9 -13 50 51 63 0 -9 -13 50 51 73 0 -9 -14 50 51 52 63 0 -9 -14 50 51 52 73 0 -9 -14 50 51 63 0 -9 -14 50 51 73 0 -9 -15 50 51 52 63 0 -9 -15 50 51 52 73 0 -9 -15 50 51 63 0 -9 -15 50 51 73 0 -9 -16 27 -28 -33 50 51 -61 63 0 -9 -16 27 -28 -33 50 51 -61 74 0 -9 -16 50 51 52 63 0 -9 -16 50 51 52 73 0 -9 -16 50 51 63 0 -9 -16 50 51 73 0 -9 -17 25 -29 -33 50 51 -61 63 0 -9 -17 25 -29 -33 50 51 -61 72 0 -9 -17 27 -29 -33 50 51 -61 63 0 -9 -17 27 -29 -33 50 51 -61 74 0 -9 -17 50 51 52 63 0 -9 -17 50 51 52 73 0 -9 -17 50 51 63 0 -9 -17 50 51 73 0 -9 -18 25 -30 -33 50 51 -61 63 0 -9 -18 25 -30 -33 50 51 -61 72 0 -9 -18 50 51 52 63 0 -9 -18 50 51 52 73 0 -9 -18 50 51 63 0 -9 -18 50 51 73 0 -9 -21 49 61 63 0 -9 -21 49 61 66 0 -9 -49 64 0 -9 -49 67 0 -10 -14 50 51 52 63 0 -10 -14 50 51 52 73 0 -10 -15 50 51 52 63 0 -10 -15 50 51 52 73 0 -10 -16 50 51 52 63 0 -10 -16 50 51 52 73 0 -10 -17 50 51 52 63 0 -10 -17 50 51 52 73 0 -10 -18 50 51 52 63 0 -10 -18 50 51 52 73 0 -10 -22 49 61 63 0 -10 -22 49 61 66 0 -11 -14 50 51 52 63 0 -11 -14 50 51 52 73 0 -11 -15 50 51 52 63 0 -11 -15 50 51 52 73 0 -11 -16 50 51 52 63 0 -11 -16 50 51 52 73 0 -11 -17 50 51 52 63 0 -11 -17 50 51 52 73 0 -11 -18 50 51 52 63 0 -11 -18 50 51 52 73 0 -11 -23 49 61 63 0 -11 -23 49 61 66 0 -12 -14 50 51 52 63 0 -12 -14 50 51 52 73 0 -12 -15 50 51 52 63 0 -12 -15 50 51 52 73 0 -12 -16 50 51 52 63 0 -12 -16 50 51 52 73 0 -12 -17 50 51 52 63 0 -12 -17 50 51 52 73 0 -12 -18 50 51 52 63 0 -12 -18 50 51 52 73 0 -12 -24 49 61 63 0 -12 -24 49 61 66 0 -49 -63 0 49 -64 0 49 -65 0 -50 61 63 0 -50 61 66 0 -51 61 63 0 -51 61 66 0 63 64 65 0 -63 -67 0 -64 -66 0 -65 -66 0 -65 -67 0 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 0 -66 -68 0 -67 -68 0 -68 -69 0 -68 -70 0 -68 -71 0 -68 -72 0 -68 -73 0 -68 -74 0 -68 -75 0 -68 -76 0 -68 -77 0 -68 -78 0 -68 -79 0 -68 -80 0 -68 -81 0 -68 -82 0 -68 -83 0 -69 -73 0 -69 -74 0 -69 -75 0 -69 -76 0 -69 -77 0 -69 -78 0 -69 -79 0 -69 -80 0 -69 -81 0 -69 -82 0 -69 -83 0 -70 -73 0 -70 -74 0 -70 -75 0 -70 -76 0 -70 -77 0 -70 -78 0 -70 -79 0 -70 -80 0 -70 -81 0 -70 -82 0 -70 -83 0 -71 -73 0 -71 -74 0 -71 -75 0 -71 -76 0 -71 -77 0 -71 -78 0 -71 -79 0 -71 -80 0 -71 -81 0 -71 -82 0 -71 -83 0 -72 -73 0 -72 -74 0 -72 -75 0 -72 -76 0 -72 -77 0 -72 -78 0 -72 -79 0 -72 -80 0 -72 -81 0 -72 -82 0 -72 -83 0 -73 -74 0 -73 -75 0 -73 -76 0 -73 -77 0 -73 -78 0 -73 -79 0 -73 -80 0 -73 -81 0 -73 -82 0 -73 -83 0 -74 -75 0 -74 -76 0 -74 -77 0 -74 -78 0 -74 -79 0 -74 -80 0 -74 -81 0 -74 -82 0 -74 -83 0 -75 -76 0 -75 -77 0 -75 -78 0 -75 -79 0 -75 -80 0 -75 -81 0 -75 -82 0 -75 -83 0 -76 -77 0 -76 -78 0 -76 -79 0 -76 -80 0 -76 -81 0 -76 -82 0 -76 -83 0 -77 -78 0 -77 -79 0 -77 -80 0 -77 -81 0 -77 -82 0 -77 -83 0 -78 -79 0 -78 -80 0 -78 -81 0 -78 -82 0 -78 -83 0 -79 -80 0 -79 -81 0 -79 -82 0 -79 -83 0 -80 -81 0 -80 -82 0 -80 -83 0 -81 -82 0 -81 -83 0 -82 -83 0 -1 0 -2 0 -3 0 -4 0 5 0 -6 0 -7 0 -8 0 -9 0 -10 0 -11 0 -12 0 -13 0 -14 0 -15 0 -16 0 17 0 -18 0 -19 0 -20 0 -21 0 -22 0 -23 0 -24 0 -25 0 -26 0 -27 0 28 0 29 0 -30 0 31 0 32 0 33 0 -34 0 35 0 -36 0 37 0 38 0 39 0 40 0 41 0 42 0 -43 0 44 0 -45 0 -46 0 -47 0 -48 0 -49 0 -50 0 -51 0 52 0 -53 0 -54 0 -55 0 -56 0 -57 0 -58 0 -59 0 -60 0 61 0 -62 0 -63 0 -66 0