c 1 _r c 2 _r_1 c 3 _r_28 c 4 _r_38 c 5 _r_63 c 6 _r_77 c 7 _r_80 c 8 _r_1_7 c 9 _r_1_21 c 10 _r_1_24 c 11 _r_28_29_30 c 12 _r_28_29_31 c 13 _r_28_29_32 c 14 _r_28_29_33 c 15 _r_28_29_34 c 16 _r_28_29_35 c 17 _r_28_29_36 c 18 _r_28_29_37 c 19 _r_38_39 c 20 _r_38_53 c 21 _r_63_64 c 22 _r_63_69 c 23 _r_63_74 c 24 _r_63_75 c 25 _r_77_78 c 26 _r_77_79 c 27 _r_80_81 c 28 _r_80_82 c 29 _r_1_7_8 c 30 _r_1_7_13 c 31 _r_1_21_22 c 32 _r_1_21_23 c 33 _r_1_24_26 c 34 _r_1_24_27 c 35 _r_38_39_40_41 c 36 _r_38_39_40_42 c 37 _r_38_39_40_43 c 38 _r_38_39_40_44 c 39 _r_38_39_40_45 c 40 _r_38_39_40_46 c 41 _r_38_39_40_47 c 42 _r_38_39_40_48 c 43 _r_38_39_40_49 c 44 _r_38_39_40_50 c 45 _r_38_39_40_52 c 46 _r_38_53_54_55 c 47 _r_38_53_54_56 c 48 _r_38_53_54_57 c 49 _r_38_53_54_58 c 50 _r_38_53_54_59 c 51 _r_38_53_54_60 c 52 _r_38_53_54_61 c 53 _r_63_64_65 c 54 _r_63_64_66 c 55 _r_63_64_67 c 56 _r_63_64_68 c 57 _r_63_69_70 c 58 _r_63_69_71 c 59 _r_63_69_73 c 60 _r_63_75_76 c 61 _r_80_82_83 c 62 _r_80_82_84 c 63 _r_1_7_8_9_10 c 64 _r_1_7_8_9_11 c 65 _r_1_7_8_9_12 c 66 _r_1_7_13_14_15 c 67 _r_1_7_13_14_16 c 68 _r_1_7_13_14_17 c 69 _r_1_7_13_14_18 c 70 _r_1_7_13_14_19 c 71 _r_1_7_13_14_20 p cnf 71 99 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 -9 2 0 -2 9 0 -10 2 0 -11 3 0 -12 3 0 -13 3 0 -14 3 0 -15 3 0 -16 3 0 -17 3 0 -18 3 0 -3 11 12 13 14 15 16 17 18 0 -19 4 0 -4 19 0 -20 4 0 -4 20 0 -21 5 0 -5 21 0 -22 5 0 -5 22 0 -23 5 0 -24 5 0 -25 6 0 -26 6 0 -27 7 0 -28 7 0 -29 8 0 -8 29 0 -30 8 0 -8 30 0 -31 9 0 -9 31 0 -32 9 0 -33 10 0 -34 10 0 -10 34 0 -35 19 0 -36 19 0 -37 19 0 -38 19 0 -39 19 0 -40 19 0 -41 19 0 -42 19 0 -43 19 0 -44 19 0 -45 19 0 -19 35 36 37 38 39 40 41 42 43 44 45 0 -46 20 0 -47 20 0 -48 20 0 -49 20 0 -50 20 0 -51 20 0 -52 20 0 -20 46 47 48 49 50 51 52 0 -53 21 0 -21 53 0 -54 21 0 -21 54 0 -55 21 0 -56 21 0 -57 22 0 -22 57 0 -58 22 0 -22 58 0 -59 22 0 -22 59 0 -60 24 0 -24 60 0 -61 28 0 -28 61 0 -62 28 0 -28 62 0 -63 29 0 -64 29 0 -65 29 0 -29 63 64 65 0 -66 30 0 -67 30 0 -68 30 0 -69 30 0 -70 30 0 -71 30 0 -30 66 67 68 69 70 71 0