c 1 _r c 2 _r_1 c 3 _r_2 c 4 _r_3 c 5 _r_4 c 6 _r_51 c 7 _r_93 c 8 _r_1_5 c 9 _r_1_20 c 10 _r_1_72 c 11 _r_1_96 c 12 _r_2_34 c 13 _r_2_58 c 14 _r_2_62 c 15 _r_2_76 c 16 _r_2_78 c 17 _r_2_86 c 18 _r_4_69 c 19 _r_4_89 c 20 _r_51_52 c 21 _r_51_53 c 22 _r_51_54 c 23 _r_51_61 c 24 _r_51_62 c 25 _r_51_63 c 26 _r_51_70 c 27 _r_51_71 c 28 _r_51_72 c 29 _r_51_97 c 30 _r_51_98 c 31 _r_93_94 c 32 _r_93_95 c 33 _r_1_5_6_7 c 34 _r_1_5_6_8 c 35 _r_1_20_21 c 36 _r_1_20_26 c 37 _r_1_72_73_74 c 38 _r_1_72_73_75 c 39 _r_2_34_37_38 c 40 _r_2_34_37_43 c 41 _r_2_58_59_60 c 42 _r_2_58_59_61 c 43 _r_2_62_63_64 c 44 _r_2_62_63_65 c 45 _r_2_78_80 c 46 _r_2_78_81 c 47 _r_2_78_82 c 48 _r_2_86_87 c 49 _r_2_86_88 c 50 _r_4_69_70_71 c 51 _r_4_69_70_72 c 52 _r_4_89_90 c 53 _r_4_89_91 c 54 _r_4_89_92 c 55 _r_51_54_55 c 56 _r_51_54_56 c 57 _r_51_54_57 c 58 _r_51_54_58 c 59 _r_51_63_64 c 60 _r_51_63_66 c 61 _r_1_5_6_7_9_10 c 62 _r_1_5_6_7_9_11 c 63 _r_1_5_6_7_9_12 c 64 _r_1_5_6_7_9_13 c 65 _r_1_5_6_8_14_15 c 66 _r_1_5_6_8_14_16 c 67 _r_1_5_6_8_14_17 c 68 _r_1_5_6_8_14_18 c 69 _r_1_5_6_8_14_19 c 70 _r_1_20_21_25 c 71 _r_1_20_26_27_28 c 72 _r_1_20_26_27_29 c 73 _r_2_34_37_38_39_40 c 74 _r_2_34_37_38_39_41 c 75 _r_2_34_37_38_39_42 c 76 _r_2_34_37_43_46_47 c 77 _r_2_34_37_43_46_48 c 78 _r_2_78_82_83_84 c 79 _r_2_78_82_83_85 c 80 _r_51_54_57_59 c 81 _r_51_54_57_60 c 82 _r_51_54_57_75 c 83 _r_51_63_66_67_68 c 84 _r_51_63_66_67_69 c 85 _r_1_20_26_27_29_30_31 c 86 _r_1_20_26_27_29_30_32 c 87 _r_1_20_26_27_29_30_33 c 88 _r_2_34_37_43_46_47_49_50 c 89 _r_2_34_37_43_46_47_49_51 c 90 _r_2_34_37_43_46_47_49_52 c 91 _r_2_34_37_43_46_47_49_53 c 92 _r_2_34_37_43_46_48_54_55 c 93 _r_2_34_37_43_46_48_54_56 c 94 _r_2_34_37_43_46_48_54_57 p cnf 94 191 1 0 -2 1 0 -1 2 0 -3 1 0 -1 3 0 -4 1 0 -1 4 0 -5 1 0 -1 5 0 -6 1 0 -1 6 0 -7 1 0 -1 7 0 -8 2 0 -2 8 0 -9 2 0 -2 9 0 -10 2 0 -2 10 0 -11 2 0 -12 3 0 -3 12 0 -13 3 0 -3 13 0 -14 3 0 -3 14 0 -15 3 0 -3 15 0 -16 3 0 -3 16 0 -17 3 0 -3 17 0 -18 5 0 -5 18 0 -19 5 0 -5 19 0 -20 6 0 -6 20 0 -21 6 0 -22 6 0 -6 22 0 -23 6 0 -24 6 0 -25 6 0 -26 6 0 -6 26 0 -27 6 0 -28 6 0 -29 6 0 -6 29 0 -30 6 0 -6 30 0 -31 7 0 -7 31 0 -32 7 0 -7 32 0 -33 8 0 -34 8 0 -8 33 34 0 -33 -34 0 -35 9 0 -9 35 0 -36 9 0 -9 36 0 -37 10 0 -38 10 0 -10 37 38 0 -37 -38 0 -39 12 0 -40 12 0 -12 39 40 0 -39 -40 0 -41 13 0 -42 13 0 -13 41 42 0 -41 -42 0 -43 14 0 -44 14 0 -14 43 44 0 -43 -44 0 -45 16 0 -16 45 0 -46 16 0 -47 16 0 -48 17 0 -17 48 0 -49 17 0 -17 49 0 -50 18 0 -51 18 0 -18 50 51 0 -50 -51 0 -52 19 0 -19 52 0 -53 19 0 -19 53 0 -54 19 0 -19 54 0 -55 22 0 -22 55 0 -56 22 0 -22 56 0 -57 22 0 -58 22 0 -22 58 0 -59 25 0 -60 25 0 -61 33 0 -62 33 0 -63 33 0 -64 33 0 -33 61 62 63 64 0 -61 -62 0 -61 -63 0 -61 -64 0 -62 -63 0 -62 -64 0 -63 -64 0 -65 34 0 -66 34 0 -67 34 0 -68 34 0 -69 34 0 -34 65 66 67 68 69 0 -65 -66 0 -65 -67 0 -65 -68 0 -65 -69 0 -66 -67 0 -66 -68 0 -66 -69 0 -67 -68 0 -67 -69 0 -68 -69 0 -70 35 0 -35 70 0 -71 36 0 -72 36 0 -36 71 72 0 -71 -72 0 -73 39 0 -74 39 0 -75 39 0 -39 73 74 75 0 -73 -74 0 -73 -75 0 -74 -75 0 -76 40 0 -77 40 0 -40 76 77 0 -76 -77 0 -78 47 0 -79 47 0 -47 78 79 0 -80 57 0 -57 80 0 -81 57 0 -57 81 0 -82 57 0 -57 82 0 -83 60 0 -84 60 0 -60 83 84 0 -83 -84 0 -85 72 0 -86 72 0 -87 72 0 -72 85 86 87 0 -85 -86 0 -85 -87 0 -86 -87 0 -88 76 0 -89 76 0 -90 76 0 -91 76 0 -76 88 89 90 91 0 -88 -89 0 -88 -90 0 -88 -91 0 -89 -90 0 -89 -91 0 -90 -91 0 -92 77 0 -93 77 0 -94 77 0 -77 92 93 94 0 -92 -93 0 -92 -94 0 -93 -94 0 -41 43 0 21 -23 0