Number of relations: 1936
Number of variables: 1840
Number of target variables: 144
Number of known variables: 73
Number of guessed variables: 0
Number of state copies (max_steps): 25
An upper bound for the number of guessed variables given by user (max_guess): 0
1442 out of 1840 state variables are known after 25 state copies
############################################################
The following 0 variable(s) are guessed:

############################################################
The following 73 variable(s) are initially known:
k_22_79, k_22_78, k_22_77, k_22_76, k_22_75, k_22_74, k_22_73, k_22_72, k_22_71, k_22_70, k_22_69, k_22_68, k_22_67, k_22_66, k_22_65, k_22_64, k_22_63, k_22_62, k_22_61, k_22_60, k_22_59, k_22_58, k_22_57, k_22_56, k_22_55, k_22_49, k_22_48, k_22_47, k_22_46, k_22_37, k_22_36, k_22_35, k_22_34, k_22_31, k_22_30, k_22_29, k_22_28, k_22_27, k_22_26, k_22_25, k_22_24, k_22_23, k_22_22, k_22_21, k_22_20, k_22_19, k_22_18, k_22_17, k_22_16, k_22_15, k_22_14, k_22_13, k_22_12, k_22_11, k_22_10, k_22_9, k_22_8, k_22_7, k_22_6, k_22_5, k_22_4, k_22_3, k_22_2, k_22_1, k_22_0, k_14_29, k_11_29, k_9_32, k_6_34, k_6_33, k_6_32, k_6_31, k_3_29
############################################################
Target variables:
k_0_0, k_0_1, k_0_2, k_0_3, k_0_4, k_0_5, k_0_6, k_0_7, k_0_8, k_0_9, k_0_10, k_0_11, k_0_12, k_0_13, k_0_14, k_0_15, k_0_16, k_0_17, k_0_18, k_0_19, k_0_20, k_0_21, k_0_22, k_0_23, k_0_24, k_0_25, k_0_26, k_0_27, k_1_4, k_1_5, k_1_6, k_1_7, k_1_16, k_1_17, k_1_18, k_1_19, k_1_24, k_1_25, k_1_26, k_1_27, k_1_28, k_1_29, k_1_30, k_1_31, k_2_0, k_2_1, k_2_2, k_2_3, k_2_20, k_2_21, k_2_22, k_2_23, k_3_16, k_3_17, k_3_18, k_3_19, k_18_20, k_18_21, k_18_22, k_18_23, k_19_8, k_19_9, k_19_10, k_19_11, k_19_16, k_19_17, k_19_18, k_19_19, k_20_0, k_20_1, k_20_2, k_20_3, k_20_4, k_20_5, k_20_6, k_20_7, k_20_12, k_20_13, k_20_14, k_20_15, k_20_24, k_20_25, k_20_26, k_20_27, k_21_4, k_21_5, k_21_6, k_21_7, k_21_8, k_21_9, k_21_10, k_21_11, k_21_12, k_21_13, k_21_14, k_21_15, k_21_16, k_21_17, k_21_18, k_21_19, k_21_20, k_21_21, k_21_22, k_21_23, k_21_24, k_21_25, k_21_26, k_21_27, k_21_28, k_21_29, k_21_30, k_21_31, k_22_0, k_22_1, k_22_2, k_22_3, k_22_4, k_22_5, k_22_6, k_22_7, k_22_8, k_22_9, k_22_10, k_22_11, k_22_12, k_22_13, k_22_14, k_22_15, k_22_16, k_22_17, k_22_18, k_22_19, k_22_20, k_22_21, k_22_22, k_22_23, k_22_24, k_22_25, k_22_26, k_22_27, k_22_28, k_22_29, k_22_30, k_22_31
############################################################
Determination flow:

State 0:
k_3_29 in symmetric relation [k_2_58, k_3_29] are known: k_3_29 ===> k_2_58
k_6_31 in symmetric relation [k_5_60, k_6_31] are known: k_6_31 ===> k_5_60
k_6_32 in symmetric relation [k_5_61, k_6_32] are known: k_6_32 ===> k_5_61
k_6_33 in symmetric relation [k_5_62, k_6_33] are known: k_6_33 ===> k_5_62
k_6_34 in symmetric relation [k_5_63, k_6_34] are known: k_6_34 ===> k_5_63
k_9_32 in symmetric relation [k_8_61, k_9_32] are known: k_9_32 ===> k_8_61
k_11_29 in symmetric relation [k_10_58, k_11_29] are known: k_11_29 ===> k_10_58
k_14_29 in symmetric relation [k_13_58, k_14_29] are known: k_14_29 ===> k_13_58
k_22_8 in symmetric relation [k_21_37, k_22_8] are known: k_22_8 ===> k_21_37
k_22_9 in symmetric relation [k_21_38, k_22_9] are known: k_22_9 ===> k_21_38
k_22_10 in symmetric relation [k_21_39, k_22_10] are known: k_22_10 ===> k_21_39
k_22_11 in symmetric relation [k_21_40, k_22_11] are known: k_22_11 ===> k_21_40
k_22_12 in symmetric relation [k_21_41, k_22_12] are known: k_22_12 ===> k_21_41
k_22_13 in symmetric relation [k_21_42, k_22_13] are known: k_22_13 ===> k_21_42
k_22_14 in symmetric relation [k_21_43, k_22_14] are known: k_22_14 ===> k_21_43
k_22_15 in symmetric relation [k_21_44, k_22_15] are known: k_22_15 ===> k_21_44
k_22_16 in symmetric relation [k_21_45, k_22_16] are known: k_22_16 ===> k_21_45
k_22_17 in symmetric relation [k_21_46, k_22_17] are known: k_22_17 ===> k_21_46
k_22_18 in symmetric relation [k_21_47, k_22_18] are known: k_22_18 ===> k_21_47
k_22_19 in symmetric relation [k_21_48, k_22_19] are known: k_22_19 ===> k_21_48
k_22_20 in symmetric relation [k_21_49, k_22_20] are known: k_22_20 ===> k_21_49
k_22_21 in symmetric relation [k_21_50, k_22_21] are known: k_22_21 ===> k_21_50
k_22_22 in symmetric relation [k_21_51, k_22_22] are known: k_22_22 ===> k_21_51
k_22_23 in symmetric relation [k_21_52, k_22_23] are known: k_22_23 ===> k_21_52
k_22_24 in symmetric relation [k_21_53, k_22_24] are known: k_22_24 ===> k_21_53
k_22_25 in symmetric relation [k_21_54, k_22_25] are known: k_22_25 ===> k_21_54
k_22_26 in symmetric relation [k_21_55, k_22_26] are known: k_22_26 ===> k_21_55
k_22_27 in symmetric relation [k_21_56, k_22_27] are known: k_22_27 ===> k_21_56
k_22_28 in symmetric relation [k_21_57, k_22_28] are known: k_22_28 ===> k_21_57
k_22_29 in symmetric relation [k_21_58, k_22_29] are known: k_22_29 ===> k_21_58
k_22_30 in symmetric relation [k_21_59, k_22_30] are known: k_22_30 ===> k_21_59
k_22_31 in symmetric relation [k_21_60, k_22_31] are known: k_22_31 ===> k_21_60
k_22_34 in symmetric relation [k_21_63, k_22_34] are known: k_22_34 ===> k_21_63
k_22_35 in symmetric relation [k_21_64, k_22_35] are known: k_22_35 ===> k_21_64
k_22_36 in symmetric relation [k_21_65, k_22_36] are known: k_22_36 ===> k_21_65
k_22_37 in symmetric relation [k_21_66, k_22_37] are known: k_22_37 ===> k_21_66
k_22_46 in symmetric relation [k_21_75, k_22_46] are known: k_22_46 ===> k_21_75
k_22_47 in symmetric relation [k_21_76, k_22_47] are known: k_22_47 ===> k_21_76
k_22_48 in symmetric relation [k_21_77, k_22_48] are known: k_22_48 ===> k_21_77
k_22_49 in symmetric relation [k_21_78, k_22_49] are known: k_22_49 ===> k_21_78
k_22_55 in symmetric relation [k_21_4, k_22_55] are known: k_22_55 ===> k_21_4
k_22_56 in symmetric relation [k_21_5, k_22_56] are known: k_22_56 ===> k_21_5
k_22_57 in symmetric relation [k_21_6, k_22_57] are known: k_22_57 ===> k_21_6
k_22_58 in symmetric relation [k_21_7, k_22_58] are known: k_22_58 ===> k_21_7
k_22_59 in symmetric relation [k_21_8, k_22_59] are known: k_22_59 ===> k_21_8
k_22_60 in symmetric relation [k_21_9, k_22_60] are known: k_22_60 ===> k_21_9
k_22_61 in symmetric relation [k_21_10, k_22_61] are known: k_22_61 ===> k_21_10
k_22_62 in symmetric relation [k_21_11, k_22_62] are known: k_22_62 ===> k_21_11
k_22_63 in symmetric relation [k_21_12, k_22_63] are known: k_22_63 ===> k_21_12
k_22_64 in symmetric relation [k_21_13, k_22_64] are known: k_22_64 ===> k_21_13
k_22_65 in symmetric relation [k_21_14, k_22_65] are known: k_22_65 ===> k_21_14
k_22_66 in symmetric relation [k_21_15, k_22_66] are known: k_22_66 ===> k_21_15
k_22_67 in symmetric relation [k_21_16, k_22_67] are known: k_22_67 ===> k_21_16
k_22_68 in symmetric relation [k_21_17, k_22_68] are known: k_22_68 ===> k_21_17
k_22_69 in symmetric relation [k_21_18, k_22_69] are known: k_22_69 ===> k_21_18
k_22_70 in symmetric relation [k_21_19, k_22_70] are known: k_22_70 ===> k_21_19
k_22_71 in symmetric relation [k_21_20, k_22_71] are known: k_22_71 ===> k_21_20
k_22_72 in symmetric relation [k_21_21, k_22_72] are known: k_22_72 ===> k_21_21
k_22_73 in symmetric relation [k_21_22, k_22_73] are known: k_22_73 ===> k_21_22
k_22_74 in symmetric relation [k_21_23, k_22_74] are known: k_22_74 ===> k_21_23
k_22_75 in symmetric relation [k_21_24, k_22_75] are known: k_22_75 ===> k_21_24
k_22_76 in symmetric relation [k_21_25, k_22_76] are known: k_22_76 ===> k_21_25
k_22_77 in symmetric relation [k_21_26, k_22_77] are known: k_22_77 ===> k_21_26
k_22_78 in symmetric relation [k_21_27, k_22_78] are known: k_22_78 ===> k_21_27
k_22_79 in symmetric relation [k_21_28, k_22_79] are known: k_22_79 ===> k_21_28
k_22_0, k_22_1, k_22_2, k_22_3 in implication relation [k_22_0, k_22_1, k_22_2, k_22_3, k_21_29] are known: k_22_0, k_22_1, k_22_2, k_22_3 ===> k_21_29
k_22_0, k_22_1, k_22_2, k_22_3 in implication relation [k_22_0, k_22_1, k_22_2, k_22_3, k_21_30] are known: k_22_0, k_22_1, k_22_2, k_22_3 ===> k_21_30
k_22_0, k_22_1, k_22_2, k_22_3 in implication relation [k_22_0, k_22_1, k_22_2, k_22_3, k_21_31] are known: k_22_0, k_22_1, k_22_2, k_22_3 ===> k_21_31
k_22_0, k_22_1, k_22_2, k_22_3 in implication relation [k_22_0, k_22_1, k_22_2, k_22_3, k_21_32] are known: k_22_0, k_22_1, k_22_2, k_22_3 ===> k_21_32
k_22_4, k_22_5, k_22_6, k_22_7 in implication relation [k_22_4, k_22_5, k_22_6, k_22_7, k_21_33] are known: k_22_4, k_22_5, k_22_6, k_22_7 ===> k_21_33
k_22_4, k_22_5, k_22_6, k_22_7 in implication relation [k_22_4, k_22_5, k_22_6, k_22_7, k_21_34] are known: k_22_4, k_22_5, k_22_6, k_22_7 ===> k_21_34
k_22_4, k_22_5, k_22_6, k_22_7 in implication relation [k_22_4, k_22_5, k_22_6, k_22_7, k_21_35] are known: k_22_4, k_22_5, k_22_6, k_22_7 ===> k_21_35
k_22_4, k_22_5, k_22_6, k_22_7 in implication relation [k_22_4, k_22_5, k_22_6, k_22_7, k_21_36] are known: k_22_4, k_22_5, k_22_6, k_22_7 ===> k_21_36
############################################################
State 1:
k_2_58 in symmetric relation [k_1_7, k_2_58] are known: k_2_58 ===> k_1_7
k_5_60 in symmetric relation [k_4_9, k_5_60] are known: k_5_60 ===> k_4_9
k_5_61 in symmetric relation [k_4_10, k_5_61] are known: k_5_61 ===> k_4_10
k_5_62 in symmetric relation [k_4_11, k_5_62] are known: k_5_62 ===> k_4_11
k_5_63 in symmetric relation [k_4_12, k_5_63] are known: k_5_63 ===> k_4_12
k_8_61 in symmetric relation [k_7_10, k_8_61] are known: k_8_61 ===> k_7_10
k_10_58 in symmetric relation [k_9_7, k_10_58] are known: k_10_58 ===> k_9_7
k_13_58 in symmetric relation [k_12_7, k_13_58] are known: k_13_58 ===> k_12_7
k_21_8 in symmetric relation [k_20_37, k_21_8] are known: k_21_8 ===> k_20_37
k_21_9 in symmetric relation [k_20_38, k_21_9] are known: k_21_9 ===> k_20_38
k_21_10 in symmetric relation [k_20_39, k_21_10] are known: k_21_10 ===> k_20_39
k_21_11 in symmetric relation [k_20_40, k_21_11] are known: k_21_11 ===> k_20_40
k_21_12 in symmetric relation [k_20_41, k_21_12] are known: k_21_12 ===> k_20_41
k_21_13 in symmetric relation [k_20_42, k_21_13] are known: k_21_13 ===> k_20_42
k_21_14 in symmetric relation [k_20_43, k_21_14] are known: k_21_14 ===> k_20_43
k_21_15 in symmetric relation [k_20_44, k_21_15] are known: k_21_15 ===> k_20_44
k_21_16 in symmetric relation [k_20_45, k_21_16] are known: k_21_16 ===> k_20_45
k_21_17 in symmetric relation [k_20_46, k_21_17] are known: k_21_17 ===> k_20_46
k_21_18 in symmetric relation [k_20_47, k_21_18] are known: k_21_18 ===> k_20_47
k_21_19 in symmetric relation [k_20_48, k_21_19] are known: k_21_19 ===> k_20_48
k_21_20 in symmetric relation [k_20_49, k_21_20] are known: k_21_20 ===> k_20_49
k_21_21 in symmetric relation [k_20_50, k_21_21] are known: k_21_21 ===> k_20_50
k_21_22 in symmetric relation [k_20_51, k_21_22] are known: k_21_22 ===> k_20_51
k_21_23 in symmetric relation [k_20_52, k_21_23] are known: k_21_23 ===> k_20_52
k_21_24 in symmetric relation [k_20_53, k_21_24] are known: k_21_24 ===> k_20_53
k_21_25 in symmetric relation [k_20_54, k_21_25] are known: k_21_25 ===> k_20_54
k_21_26 in symmetric relation [k_20_55, k_21_26] are known: k_21_26 ===> k_20_55
k_21_27 in symmetric relation [k_20_56, k_21_27] are known: k_21_27 ===> k_20_56
k_21_28 in symmetric relation [k_20_57, k_21_28] are known: k_21_28 ===> k_20_57
k_21_29 in symmetric relation [k_20_58, k_21_29] are known: k_21_29 ===> k_20_58
k_21_30 in symmetric relation [k_20_59, k_21_30] are known: k_21_30 ===> k_20_59
k_21_31 in symmetric relation [k_20_60, k_21_31] are known: k_21_31 ===> k_20_60
k_21_32 in symmetric relation [k_20_61, k_21_32] are known: k_21_32 ===> k_20_61
k_21_33 in symmetric relation [k_20_62, k_21_33] are known: k_21_33 ===> k_20_62
k_21_34 in symmetric relation [k_20_63, k_21_34] are known: k_21_34 ===> k_20_63
k_21_35 in symmetric relation [k_20_64, k_21_35] are known: k_21_35 ===> k_20_64
k_21_36 in symmetric relation [k_20_65, k_21_36] are known: k_21_36 ===> k_20_65
k_21_37 in symmetric relation [k_20_66, k_21_37] are known: k_21_37 ===> k_20_66
k_21_38 in symmetric relation [k_20_67, k_21_38] are known: k_21_38 ===> k_20_67
k_21_39 in symmetric relation [k_20_68, k_21_39] are known: k_21_39 ===> k_20_68
k_21_40 in symmetric relation [k_20_69, k_21_40] are known: k_21_40 ===> k_20_69
k_21_41 in symmetric relation [k_20_70, k_21_41] are known: k_21_41 ===> k_20_70
k_21_42 in symmetric relation [k_20_71, k_21_42] are known: k_21_42 ===> k_20_71
k_21_43 in symmetric relation [k_20_72, k_21_43] are known: k_21_43 ===> k_20_72
k_21_44 in symmetric relation [k_20_73, k_21_44] are known: k_21_44 ===> k_20_73
k_21_45 in symmetric relation [k_20_74, k_21_45] are known: k_21_45 ===> k_20_74
k_21_46 in symmetric relation [k_20_75, k_21_46] are known: k_21_46 ===> k_20_75
k_21_47 in symmetric relation [k_20_76, k_21_47] are known: k_21_47 ===> k_20_76
k_21_48 in symmetric relation [k_20_77, k_21_48] are known: k_21_48 ===> k_20_77
k_21_49 in symmetric relation [k_20_78, k_21_49] are known: k_21_49 ===> k_20_78
k_21_50 in symmetric relation [k_20_79, k_21_50] are known: k_21_50 ===> k_20_79
k_21_51 in symmetric relation [k_20_0, k_21_51] are known: k_21_51 ===> k_20_0
k_21_52 in symmetric relation [k_20_1, k_21_52] are known: k_21_52 ===> k_20_1
k_21_53 in symmetric relation [k_20_2, k_21_53] are known: k_21_53 ===> k_20_2
k_21_54 in symmetric relation [k_20_3, k_21_54] are known: k_21_54 ===> k_20_3
k_21_55 in symmetric relation [k_20_4, k_21_55] are known: k_21_55 ===> k_20_4
k_21_56 in symmetric relation [k_20_5, k_21_56] are known: k_21_56 ===> k_20_5
k_21_57 in symmetric relation [k_20_6, k_21_57] are known: k_21_57 ===> k_20_6
k_21_58 in symmetric relation [k_20_7, k_21_58] are known: k_21_58 ===> k_20_7
k_21_59 in symmetric relation [k_20_8, k_21_59] are known: k_21_59 ===> k_20_8
k_21_60 in symmetric relation [k_20_9, k_21_60] are known: k_21_60 ===> k_20_9
k_21_63 in symmetric relation [k_20_12, k_21_63] are known: k_21_63 ===> k_20_12
k_21_64 in symmetric relation [k_20_13, k_21_64] are known: k_21_64 ===> k_20_13
k_21_65 in symmetric relation [k_20_14, k_21_65] are known: k_21_65 ===> k_20_14
k_21_66 in symmetric relation [k_20_15, k_21_66] are known: k_21_66 ===> k_20_15
k_21_75 in symmetric relation [k_20_24, k_21_75] are known: k_21_75 ===> k_20_24
k_21_76 in symmetric relation [k_20_25, k_21_76] are known: k_21_76 ===> k_20_25
k_21_77 in symmetric relation [k_20_26, k_21_77] are known: k_21_77 ===> k_20_26
k_21_78 in symmetric relation [k_20_27, k_21_78] are known: k_21_78 ===> k_20_27
k_21_4, k_21_5, k_21_6, k_21_7 in implication relation [k_21_4, k_21_5, k_21_6, k_21_7, k_20_33] are known: k_21_4, k_21_5, k_21_6, k_21_7 ===> k_20_33
k_21_4, k_21_5, k_21_6, k_21_7 in implication relation [k_21_4, k_21_5, k_21_6, k_21_7, k_20_34] are known: k_21_4, k_21_5, k_21_6, k_21_7 ===> k_20_34
k_21_4, k_21_5, k_21_6, k_21_7 in implication relation [k_21_4, k_21_5, k_21_6, k_21_7, k_20_35] are known: k_21_4, k_21_5, k_21_6, k_21_7 ===> k_20_35
k_21_4, k_21_5, k_21_6, k_21_7 in implication relation [k_21_4, k_21_5, k_21_6, k_21_7, k_20_36] are known: k_21_4, k_21_5, k_21_6, k_21_7 ===> k_20_36
############################################################
State 2:
k_4_9 in symmetric relation [k_3_38, k_4_9] are known: k_4_9 ===> k_3_38
k_4_10 in symmetric relation [k_3_39, k_4_10] are known: k_4_10 ===> k_3_39
k_4_11 in symmetric relation [k_3_40, k_4_11] are known: k_4_11 ===> k_3_40
k_4_12 in symmetric relation [k_3_41, k_4_12] are known: k_4_12 ===> k_3_41
k_7_10 in symmetric relation [k_6_39, k_7_10] are known: k_7_10 ===> k_6_39
k_20_8 in symmetric relation [k_19_37, k_20_8] are known: k_20_8 ===> k_19_37
k_20_9 in symmetric relation [k_19_38, k_20_9] are known: k_20_9 ===> k_19_38
k_20_12 in symmetric relation [k_19_41, k_20_12] are known: k_20_12 ===> k_19_41
k_20_13 in symmetric relation [k_19_42, k_20_13] are known: k_20_13 ===> k_19_42
k_20_14 in symmetric relation [k_19_43, k_20_14] are known: k_20_14 ===> k_19_43
k_20_15 in symmetric relation [k_19_44, k_20_15] are known: k_20_15 ===> k_19_44
k_20_24 in symmetric relation [k_19_53, k_20_24] are known: k_20_24 ===> k_19_53
k_20_25 in symmetric relation [k_19_54, k_20_25] are known: k_20_25 ===> k_19_54
k_20_26 in symmetric relation [k_19_55, k_20_26] are known: k_20_26 ===> k_19_55
k_20_27 in symmetric relation [k_19_56, k_20_27] are known: k_20_27 ===> k_19_56
k_20_33 in symmetric relation [k_19_62, k_20_33] are known: k_20_33 ===> k_19_62
k_20_34 in symmetric relation [k_19_63, k_20_34] are known: k_20_34 ===> k_19_63
k_20_35 in symmetric relation [k_19_64, k_20_35] are known: k_20_35 ===> k_19_64
k_20_36 in symmetric relation [k_19_65, k_20_36] are known: k_20_36 ===> k_19_65
k_20_37 in symmetric relation [k_19_66, k_20_37] are known: k_20_37 ===> k_19_66
k_20_38 in symmetric relation [k_19_67, k_20_38] are known: k_20_38 ===> k_19_67
k_20_39 in symmetric relation [k_19_68, k_20_39] are known: k_20_39 ===> k_19_68
k_20_40 in symmetric relation [k_19_69, k_20_40] are known: k_20_40 ===> k_19_69
k_20_41 in symmetric relation [k_19_70, k_20_41] are known: k_20_41 ===> k_19_70
k_20_42 in symmetric relation [k_19_71, k_20_42] are known: k_20_42 ===> k_19_71
k_20_43 in symmetric relation [k_19_72, k_20_43] are known: k_20_43 ===> k_19_72
k_20_44 in symmetric relation [k_19_73, k_20_44] are known: k_20_44 ===> k_19_73
k_20_45 in symmetric relation [k_19_74, k_20_45] are known: k_20_45 ===> k_19_74
k_20_46 in symmetric relation [k_19_75, k_20_46] are known: k_20_46 ===> k_19_75
k_20_47 in symmetric relation [k_19_76, k_20_47] are known: k_20_47 ===> k_19_76
k_20_48 in symmetric relation [k_19_77, k_20_48] are known: k_20_48 ===> k_19_77
k_20_49 in symmetric relation [k_19_78, k_20_49] are known: k_20_49 ===> k_19_78
k_20_50 in symmetric relation [k_19_79, k_20_50] are known: k_20_50 ===> k_19_79
k_20_51 in symmetric relation [k_19_0, k_20_51] are known: k_20_51 ===> k_19_0
k_20_52 in symmetric relation [k_19_1, k_20_52] are known: k_20_52 ===> k_19_1
k_20_53 in symmetric relation [k_19_2, k_20_53] are known: k_20_53 ===> k_19_2
k_20_54 in symmetric relation [k_19_3, k_20_54] are known: k_20_54 ===> k_19_3
k_20_55 in symmetric relation [k_19_4, k_20_55] are known: k_20_55 ===> k_19_4
k_20_56 in symmetric relation [k_19_5, k_20_56] are known: k_20_56 ===> k_19_5
k_20_57 in symmetric relation [k_19_6, k_20_57] are known: k_20_57 ===> k_19_6
k_20_58 in symmetric relation [k_19_7, k_20_58] are known: k_20_58 ===> k_19_7
k_20_59 in symmetric relation [k_19_8, k_20_59] are known: k_20_59 ===> k_19_8
k_20_60 in symmetric relation [k_19_9, k_20_60] are known: k_20_60 ===> k_19_9
k_20_61 in symmetric relation [k_19_10, k_20_61] are known: k_20_61 ===> k_19_10
k_20_62 in symmetric relation [k_19_11, k_20_62] are known: k_20_62 ===> k_19_11
k_20_63 in symmetric relation [k_19_12, k_20_63] are known: k_20_63 ===> k_19_12
k_20_64 in symmetric relation [k_19_13, k_20_64] are known: k_20_64 ===> k_19_13
k_20_65 in symmetric relation [k_19_14, k_20_65] are known: k_20_65 ===> k_19_14
k_20_66 in symmetric relation [k_19_15, k_20_66] are known: k_20_66 ===> k_19_15
k_20_67 in symmetric relation [k_19_16, k_20_67] are known: k_20_67 ===> k_19_16
k_20_68 in symmetric relation [k_19_17, k_20_68] are known: k_20_68 ===> k_19_17
k_20_69 in symmetric relation [k_19_18, k_20_69] are known: k_20_69 ===> k_19_18
k_20_70 in symmetric relation [k_19_19, k_20_70] are known: k_20_70 ===> k_19_19
k_20_71 in symmetric relation [k_19_20, k_20_71] are known: k_20_71 ===> k_19_20
k_20_72 in symmetric relation [k_19_21, k_20_72] are known: k_20_72 ===> k_19_21
k_20_73 in symmetric relation [k_19_22, k_20_73] are known: k_20_73 ===> k_19_22
k_20_74 in symmetric relation [k_19_23, k_20_74] are known: k_20_74 ===> k_19_23
k_20_75 in symmetric relation [k_19_24, k_20_75] are known: k_20_75 ===> k_19_24
k_20_76 in symmetric relation [k_19_25, k_20_76] are known: k_20_76 ===> k_19_25
k_20_77 in symmetric relation [k_19_26, k_20_77] are known: k_20_77 ===> k_19_26
k_20_78 in symmetric relation [k_19_27, k_20_78] are known: k_20_78 ===> k_19_27
k_20_79 in symmetric relation [k_19_28, k_20_79] are known: k_20_79 ===> k_19_28
k_20_0, k_20_1, k_20_2, k_20_3 in implication relation [k_20_0, k_20_1, k_20_2, k_20_3, k_19_29] are known: k_20_0, k_20_1, k_20_2, k_20_3 ===> k_19_29
k_20_0, k_20_1, k_20_2, k_20_3 in implication relation [k_20_0, k_20_1, k_20_2, k_20_3, k_19_30] are known: k_20_0, k_20_1, k_20_2, k_20_3 ===> k_19_30
k_20_0, k_20_1, k_20_2, k_20_3 in implication relation [k_20_0, k_20_1, k_20_2, k_20_3, k_19_31] are known: k_20_0, k_20_1, k_20_2, k_20_3 ===> k_19_31
k_20_0, k_20_1, k_20_2, k_20_3 in implication relation [k_20_0, k_20_1, k_20_2, k_20_3, k_19_32] are known: k_20_0, k_20_1, k_20_2, k_20_3 ===> k_19_32
k_20_4, k_20_5, k_20_6, k_20_7 in implication relation [k_20_4, k_20_5, k_20_6, k_20_7, k_19_33] are known: k_20_4, k_20_5, k_20_6, k_20_7 ===> k_19_33
k_20_4, k_20_5, k_20_6, k_20_7 in implication relation [k_20_4, k_20_5, k_20_6, k_20_7, k_19_34] are known: k_20_4, k_20_5, k_20_6, k_20_7 ===> k_19_34
k_20_4, k_20_5, k_20_6, k_20_7 in implication relation [k_20_4, k_20_5, k_20_6, k_20_7, k_19_35] are known: k_20_4, k_20_5, k_20_6, k_20_7 ===> k_19_35
k_20_4, k_20_5, k_20_6, k_20_7 in implication relation [k_20_4, k_20_5, k_20_6, k_20_7, k_19_36] are known: k_20_4, k_20_5, k_20_6, k_20_7 ===> k_19_36
############################################################
State 3:
k_3_38 in symmetric relation [k_2_67, k_3_38] are known: k_3_38 ===> k_2_67
k_3_39 in symmetric relation [k_2_68, k_3_39] are known: k_3_39 ===> k_2_68
k_3_40 in symmetric relation [k_2_69, k_3_40] are known: k_3_40 ===> k_2_69
k_3_41 in symmetric relation [k_2_70, k_3_41] are known: k_3_41 ===> k_2_70
k_6_39 in symmetric relation [k_5_68, k_6_39] are known: k_6_39 ===> k_5_68
k_19_8 in symmetric relation [k_18_37, k_19_8] are known: k_19_8 ===> k_18_37
k_19_9 in symmetric relation [k_18_38, k_19_9] are known: k_19_9 ===> k_18_38
k_19_10 in symmetric relation [k_18_39, k_19_10] are known: k_19_10 ===> k_18_39
k_19_11 in symmetric relation [k_18_40, k_19_11] are known: k_19_11 ===> k_18_40
k_19_12 in symmetric relation [k_18_41, k_19_12] are known: k_19_12 ===> k_18_41
k_19_13 in symmetric relation [k_18_42, k_19_13] are known: k_19_13 ===> k_18_42
k_19_14 in symmetric relation [k_18_43, k_19_14] are known: k_19_14 ===> k_18_43
k_19_15 in symmetric relation [k_18_44, k_19_15] are known: k_19_15 ===> k_18_44
k_19_16 in symmetric relation [k_18_45, k_19_16] are known: k_19_16 ===> k_18_45
k_19_17 in symmetric relation [k_18_46, k_19_17] are known: k_19_17 ===> k_18_46
k_19_18 in symmetric relation [k_18_47, k_19_18] are known: k_19_18 ===> k_18_47
k_19_19 in symmetric relation [k_18_48, k_19_19] are known: k_19_19 ===> k_18_48
k_19_20 in symmetric relation [k_18_49, k_19_20] are known: k_19_20 ===> k_18_49
k_19_21 in symmetric relation [k_18_50, k_19_21] are known: k_19_21 ===> k_18_50
k_19_22 in symmetric relation [k_18_51, k_19_22] are known: k_19_22 ===> k_18_51
k_19_23 in symmetric relation [k_18_52, k_19_23] are known: k_19_23 ===> k_18_52
k_19_24 in symmetric relation [k_18_53, k_19_24] are known: k_19_24 ===> k_18_53
k_19_25 in symmetric relation [k_18_54, k_19_25] are known: k_19_25 ===> k_18_54
k_19_26 in symmetric relation [k_18_55, k_19_26] are known: k_19_26 ===> k_18_55
k_19_27 in symmetric relation [k_18_56, k_19_27] are known: k_19_27 ===> k_18_56
k_19_28 in symmetric relation [k_18_57, k_19_28] are known: k_19_28 ===> k_18_57
k_19_29 in symmetric relation [k_18_58, k_19_29] are known: k_19_29 ===> k_18_58
k_19_30 in symmetric relation [k_18_59, k_19_30] are known: k_19_30 ===> k_18_59
k_19_31 in symmetric relation [k_18_60, k_19_31] are known: k_19_31 ===> k_18_60
k_19_32 in symmetric relation [k_18_61, k_19_32] are known: k_19_32 ===> k_18_61
k_19_33 in symmetric relation [k_18_62, k_19_33] are known: k_19_33 ===> k_18_62
k_19_34 in symmetric relation [k_18_63, k_19_34] are known: k_19_34 ===> k_18_63
k_19_35 in symmetric relation [k_18_64, k_19_35] are known: k_19_35 ===> k_18_64
k_19_36 in symmetric relation [k_18_65, k_19_36] are known: k_19_36 ===> k_18_65
k_19_37 in symmetric relation [k_18_66, k_19_37] are known: k_19_37 ===> k_18_66
k_19_38 in symmetric relation [k_18_67, k_19_38] are known: k_19_38 ===> k_18_67
k_19_41 in symmetric relation [k_18_70, k_19_41] are known: k_19_41 ===> k_18_70
k_19_42 in symmetric relation [k_18_71, k_19_42] are known: k_19_42 ===> k_18_71
k_19_43 in symmetric relation [k_18_72, k_19_43] are known: k_19_43 ===> k_18_72
k_19_44 in symmetric relation [k_18_73, k_19_44] are known: k_19_44 ===> k_18_73
k_19_53 in symmetric relation [k_18_2, k_19_53] are known: k_19_53 ===> k_18_2
k_19_54 in symmetric relation [k_18_3, k_19_54] are known: k_19_54 ===> k_18_3
k_19_55 in symmetric relation [k_18_4, k_19_55] are known: k_19_55 ===> k_18_4
k_19_56 in symmetric relation [k_18_5, k_19_56] are known: k_19_56 ===> k_18_5
k_19_62 in symmetric relation [k_18_11, k_19_62] are known: k_19_62 ===> k_18_11
k_19_63 in symmetric relation [k_18_12, k_19_63] are known: k_19_63 ===> k_18_12
k_19_64 in symmetric relation [k_18_13, k_19_64] are known: k_19_64 ===> k_18_13
k_19_65 in symmetric relation [k_18_14, k_19_65] are known: k_19_65 ===> k_18_14
k_19_66 in symmetric relation [k_18_15, k_19_66] are known: k_19_66 ===> k_18_15
k_19_67 in symmetric relation [k_18_16, k_19_67] are known: k_19_67 ===> k_18_16
k_19_68 in symmetric relation [k_18_17, k_19_68] are known: k_19_68 ===> k_18_17
k_19_69 in symmetric relation [k_18_18, k_19_69] are known: k_19_69 ===> k_18_18
k_19_70 in symmetric relation [k_18_19, k_19_70] are known: k_19_70 ===> k_18_19
k_19_71 in symmetric relation [k_18_20, k_19_71] are known: k_19_71 ===> k_18_20
k_19_72 in symmetric relation [k_18_21, k_19_72] are known: k_19_72 ===> k_18_21
k_19_73 in symmetric relation [k_18_22, k_19_73] are known: k_19_73 ===> k_18_22
k_19_74 in symmetric relation [k_18_23, k_19_74] are known: k_19_74 ===> k_18_23
k_19_75 in symmetric relation [k_18_24, k_19_75] are known: k_19_75 ===> k_18_24
k_19_76 in symmetric relation [k_18_25, k_19_76] are known: k_19_76 ===> k_18_25
k_19_77 in symmetric relation [k_18_26, k_19_77] are known: k_19_77 ===> k_18_26
k_19_78 in symmetric relation [k_18_27, k_19_78] are known: k_19_78 ===> k_18_27
k_19_79 in symmetric relation [k_18_28, k_19_79] are known: k_19_79 ===> k_18_28
k_19_0, k_19_1, k_19_2, k_19_3 in implication relation [k_19_0, k_19_1, k_19_2, k_19_3, k_18_29] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_29
k_19_0, k_19_1, k_19_2, k_19_3 in implication relation [k_19_0, k_19_1, k_19_2, k_19_3, k_18_30] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_30
k_19_0, k_19_1, k_19_2, k_19_3 in implication relation [k_19_0, k_19_1, k_19_2, k_19_3, k_18_31] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_31
k_19_0, k_19_1, k_19_2, k_19_3 in implication relation [k_19_0, k_19_1, k_19_2, k_19_3, k_18_32] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_32
k_19_4, k_19_5, k_19_6, k_19_7 in implication relation [k_19_4, k_19_5, k_19_6, k_19_7, k_18_33] are known: k_19_4, k_19_5, k_19_6, k_19_7 ===> k_18_33
k_19_4, k_19_5, k_19_6, k_19_7 in implication relation [k_19_4, k_19_5, k_19_6, k_19_7, k_18_34] are known: k_19_4, k_19_5, k_19_6, k_19_7 ===> k_18_34
k_19_4, k_19_5, k_19_6, k_19_7 in implication relation [k_19_4, k_19_5, k_19_6, k_19_7, k_18_35] are known: k_19_4, k_19_5, k_19_6, k_19_7 ===> k_18_35
k_19_4, k_19_5, k_19_6, k_19_7 in implication relation [k_19_4, k_19_5, k_19_6, k_19_7, k_18_36] are known: k_19_4, k_19_5, k_19_6, k_19_7 ===> k_18_36
############################################################
State 4:
k_2_67 in symmetric relation [k_1_16, k_2_67] are known: k_2_67 ===> k_1_16
k_2_68 in symmetric relation [k_1_17, k_2_68] are known: k_2_68 ===> k_1_17
k_2_69 in symmetric relation [k_1_18, k_2_69] are known: k_2_69 ===> k_1_18
k_2_70 in symmetric relation [k_1_19, k_2_70] are known: k_2_70 ===> k_1_19
k_5_68 in symmetric relation [k_4_17, k_5_68] are known: k_5_68 ===> k_4_17
k_18_11 in symmetric relation [k_17_40, k_18_11] are known: k_18_11 ===> k_17_40
k_18_12 in symmetric relation [k_17_41, k_18_12] are known: k_18_12 ===> k_17_41
k_18_13 in symmetric relation [k_17_42, k_18_13] are known: k_18_13 ===> k_17_42
k_18_14 in symmetric relation [k_17_43, k_18_14] are known: k_18_14 ===> k_17_43
k_18_15 in symmetric relation [k_17_44, k_18_15] are known: k_18_15 ===> k_17_44
k_18_16 in symmetric relation [k_17_45, k_18_16] are known: k_18_16 ===> k_17_45
k_18_17 in symmetric relation [k_17_46, k_18_17] are known: k_18_17 ===> k_17_46
k_18_18 in symmetric relation [k_17_47, k_18_18] are known: k_18_18 ===> k_17_47
k_18_19 in symmetric relation [k_17_48, k_18_19] are known: k_18_19 ===> k_17_48
k_18_20 in symmetric relation [k_17_49, k_18_20] are known: k_18_20 ===> k_17_49
k_18_21 in symmetric relation [k_17_50, k_18_21] are known: k_18_21 ===> k_17_50
k_18_22 in symmetric relation [k_17_51, k_18_22] are known: k_18_22 ===> k_17_51
k_18_23 in symmetric relation [k_17_52, k_18_23] are known: k_18_23 ===> k_17_52
k_18_24 in symmetric relation [k_17_53, k_18_24] are known: k_18_24 ===> k_17_53
k_18_25 in symmetric relation [k_17_54, k_18_25] are known: k_18_25 ===> k_17_54
k_18_26 in symmetric relation [k_17_55, k_18_26] are known: k_18_26 ===> k_17_55
k_18_27 in symmetric relation [k_17_56, k_18_27] are known: k_18_27 ===> k_17_56
k_18_28 in symmetric relation [k_17_57, k_18_28] are known: k_18_28 ===> k_17_57
k_18_29 in symmetric relation [k_17_58, k_18_29] are known: k_18_29 ===> k_17_58
k_18_30 in symmetric relation [k_17_59, k_18_30] are known: k_18_30 ===> k_17_59
k_18_31 in symmetric relation [k_17_60, k_18_31] are known: k_18_31 ===> k_17_60
k_18_32 in symmetric relation [k_17_61, k_18_32] are known: k_18_32 ===> k_17_61
k_18_33 in symmetric relation [k_17_62, k_18_33] are known: k_18_33 ===> k_17_62
k_18_34 in symmetric relation [k_17_63, k_18_34] are known: k_18_34 ===> k_17_63
k_18_35 in symmetric relation [k_17_64, k_18_35] are known: k_18_35 ===> k_17_64
k_18_36 in symmetric relation [k_17_65, k_18_36] are known: k_18_36 ===> k_17_65
k_18_37 in symmetric relation [k_17_66, k_18_37] are known: k_18_37 ===> k_17_66
k_18_38 in symmetric relation [k_17_67, k_18_38] are known: k_18_38 ===> k_17_67
k_18_39 in symmetric relation [k_17_68, k_18_39] are known: k_18_39 ===> k_17_68
k_18_40 in symmetric relation [k_17_69, k_18_40] are known: k_18_40 ===> k_17_69
k_18_41 in symmetric relation [k_17_70, k_18_41] are known: k_18_41 ===> k_17_70
k_18_42 in symmetric relation [k_17_71, k_18_42] are known: k_18_42 ===> k_17_71
k_18_43 in symmetric relation [k_17_72, k_18_43] are known: k_18_43 ===> k_17_72
k_18_44 in symmetric relation [k_17_73, k_18_44] are known: k_18_44 ===> k_17_73
k_18_45 in symmetric relation [k_17_74, k_18_45] are known: k_18_45 ===> k_17_74
k_18_46 in symmetric relation [k_17_75, k_18_46] are known: k_18_46 ===> k_17_75
k_18_47 in symmetric relation [k_17_76, k_18_47] are known: k_18_47 ===> k_17_76
k_18_48 in symmetric relation [k_17_77, k_18_48] are known: k_18_48 ===> k_17_77
k_18_49 in symmetric relation [k_17_78, k_18_49] are known: k_18_49 ===> k_17_78
k_18_50 in symmetric relation [k_17_79, k_18_50] are known: k_18_50 ===> k_17_79
k_18_51 in symmetric relation [k_17_0, k_18_51] are known: k_18_51 ===> k_17_0
k_18_52 in symmetric relation [k_17_1, k_18_52] are known: k_18_52 ===> k_17_1
k_18_53 in symmetric relation [k_17_2, k_18_53] are known: k_18_53 ===> k_17_2
k_18_54 in symmetric relation [k_17_3, k_18_54] are known: k_18_54 ===> k_17_3
k_18_55 in symmetric relation [k_17_4, k_18_55] are known: k_18_55 ===> k_17_4
k_18_56 in symmetric relation [k_17_5, k_18_56] are known: k_18_56 ===> k_17_5
k_18_57 in symmetric relation [k_17_6, k_18_57] are known: k_18_57 ===> k_17_6
k_18_58 in symmetric relation [k_17_7, k_18_58] are known: k_18_58 ===> k_17_7
k_18_59 in symmetric relation [k_17_8, k_18_59] are known: k_18_59 ===> k_17_8
k_18_60 in symmetric relation [k_17_9, k_18_60] are known: k_18_60 ===> k_17_9
k_18_61 in symmetric relation [k_17_10, k_18_61] are known: k_18_61 ===> k_17_10
k_18_62 in symmetric relation [k_17_11, k_18_62] are known: k_18_62 ===> k_17_11
k_18_63 in symmetric relation [k_17_12, k_18_63] are known: k_18_63 ===> k_17_12
k_18_64 in symmetric relation [k_17_13, k_18_64] are known: k_18_64 ===> k_17_13
k_18_65 in symmetric relation [k_17_14, k_18_65] are known: k_18_65 ===> k_17_14
k_18_66 in symmetric relation [k_17_15, k_18_66] are known: k_18_66 ===> k_17_15
k_18_67 in symmetric relation [k_17_16, k_18_67] are known: k_18_67 ===> k_17_16
k_18_70 in symmetric relation [k_17_19, k_18_70] are known: k_18_70 ===> k_17_19
k_18_71 in symmetric relation [k_17_20, k_18_71] are known: k_18_71 ===> k_17_20
k_18_72 in symmetric relation [k_17_21, k_18_72] are known: k_18_72 ===> k_17_21
k_18_73 in symmetric relation [k_17_22, k_18_73] are known: k_18_73 ===> k_17_22
############################################################
State 5:
k_1_16 in symmetric relation [k_0_45, k_1_16] are known: k_1_16 ===> k_0_45
k_1_17 in symmetric relation [k_0_46, k_1_17] are known: k_1_17 ===> k_0_46
k_1_18 in symmetric relation [k_0_47, k_1_18] are known: k_1_18 ===> k_0_47
k_1_19 in symmetric relation [k_0_48, k_1_19] are known: k_1_19 ===> k_0_48
k_4_17 in symmetric relation [k_3_46, k_4_17] are known: k_4_17 ===> k_3_46
k_17_8 in symmetric relation [k_16_37, k_17_8] are known: k_17_8 ===> k_16_37
k_17_9 in symmetric relation [k_16_38, k_17_9] are known: k_17_9 ===> k_16_38
k_17_10 in symmetric relation [k_16_39, k_17_10] are known: k_17_10 ===> k_16_39
k_17_11 in symmetric relation [k_16_40, k_17_11] are known: k_17_11 ===> k_16_40
k_17_12 in symmetric relation [k_16_41, k_17_12] are known: k_17_12 ===> k_16_41
k_17_13 in symmetric relation [k_16_42, k_17_13] are known: k_17_13 ===> k_16_42
k_17_14 in symmetric relation [k_16_43, k_17_14] are known: k_17_14 ===> k_16_43
k_17_15 in symmetric relation [k_16_44, k_17_15] are known: k_17_15 ===> k_16_44
k_17_16 in symmetric relation [k_16_45, k_17_16] are known: k_17_16 ===> k_16_45
k_17_19 in symmetric relation [k_16_48, k_17_19] are known: k_17_19 ===> k_16_48
k_17_20 in symmetric relation [k_16_49, k_17_20] are known: k_17_20 ===> k_16_49
k_17_21 in symmetric relation [k_16_50, k_17_21] are known: k_17_21 ===> k_16_50
k_17_22 in symmetric relation [k_16_51, k_17_22] are known: k_17_22 ===> k_16_51
k_17_40 in symmetric relation [k_16_69, k_17_40] are known: k_17_40 ===> k_16_69
k_17_41 in symmetric relation [k_16_70, k_17_41] are known: k_17_41 ===> k_16_70
k_17_42 in symmetric relation [k_16_71, k_17_42] are known: k_17_42 ===> k_16_71
k_17_43 in symmetric relation [k_16_72, k_17_43] are known: k_17_43 ===> k_16_72
k_17_44 in symmetric relation [k_16_73, k_17_44] are known: k_17_44 ===> k_16_73
k_17_45 in symmetric relation [k_16_74, k_17_45] are known: k_17_45 ===> k_16_74
k_17_46 in symmetric relation [k_16_75, k_17_46] are known: k_17_46 ===> k_16_75
k_17_47 in symmetric relation [k_16_76, k_17_47] are known: k_17_47 ===> k_16_76
k_17_48 in symmetric relation [k_16_77, k_17_48] are known: k_17_48 ===> k_16_77
k_17_49 in symmetric relation [k_16_78, k_17_49] are known: k_17_49 ===> k_16_78
k_17_50 in symmetric relation [k_16_79, k_17_50] are known: k_17_50 ===> k_16_79
k_17_51 in symmetric relation [k_16_0, k_17_51] are known: k_17_51 ===> k_16_0
k_17_52 in symmetric relation [k_16_1, k_17_52] are known: k_17_52 ===> k_16_1
k_17_53 in symmetric relation [k_16_2, k_17_53] are known: k_17_53 ===> k_16_2
k_17_54 in symmetric relation [k_16_3, k_17_54] are known: k_17_54 ===> k_16_3
k_17_55 in symmetric relation [k_16_4, k_17_55] are known: k_17_55 ===> k_16_4
k_17_56 in symmetric relation [k_16_5, k_17_56] are known: k_17_56 ===> k_16_5
k_17_57 in symmetric relation [k_16_6, k_17_57] are known: k_17_57 ===> k_16_6
k_17_58 in symmetric relation [k_16_7, k_17_58] are known: k_17_58 ===> k_16_7
k_17_59 in symmetric relation [k_16_8, k_17_59] are known: k_17_59 ===> k_16_8
k_17_60 in symmetric relation [k_16_9, k_17_60] are known: k_17_60 ===> k_16_9
k_17_61 in symmetric relation [k_16_10, k_17_61] are known: k_17_61 ===> k_16_10
k_17_62 in symmetric relation [k_16_11, k_17_62] are known: k_17_62 ===> k_16_11
k_17_63 in symmetric relation [k_16_12, k_17_63] are known: k_17_63 ===> k_16_12
k_17_64 in symmetric relation [k_16_13, k_17_64] are known: k_17_64 ===> k_16_13
k_17_65 in symmetric relation [k_16_14, k_17_65] are known: k_17_65 ===> k_16_14
k_17_66 in symmetric relation [k_16_15, k_17_66] are known: k_17_66 ===> k_16_15
k_17_67 in symmetric relation [k_16_16, k_17_67] are known: k_17_67 ===> k_16_16
k_17_68 in symmetric relation [k_16_17, k_17_68] are known: k_17_68 ===> k_16_17
k_17_69 in symmetric relation [k_16_18, k_17_69] are known: k_17_69 ===> k_16_18
k_17_70 in symmetric relation [k_16_19, k_17_70] are known: k_17_70 ===> k_16_19
k_17_71 in symmetric relation [k_16_20, k_17_71] are known: k_17_71 ===> k_16_20
k_17_72 in symmetric relation [k_16_21, k_17_72] are known: k_17_72 ===> k_16_21
k_17_73 in symmetric relation [k_16_22, k_17_73] are known: k_17_73 ===> k_16_22
k_17_74 in symmetric relation [k_16_23, k_17_74] are known: k_17_74 ===> k_16_23
k_17_75 in symmetric relation [k_16_24, k_17_75] are known: k_17_75 ===> k_16_24
k_17_76 in symmetric relation [k_16_25, k_17_76] are known: k_17_76 ===> k_16_25
k_17_77 in symmetric relation [k_16_26, k_17_77] are known: k_17_77 ===> k_16_26
k_17_78 in symmetric relation [k_16_27, k_17_78] are known: k_17_78 ===> k_16_27
k_17_79 in symmetric relation [k_16_28, k_17_79] are known: k_17_79 ===> k_16_28
k_17_0, k_17_1, k_17_2, k_17_3 in implication relation [k_17_0, k_17_1, k_17_2, k_17_3, k_16_29] are known: k_17_0, k_17_1, k_17_2, k_17_3 ===> k_16_29
k_17_0, k_17_1, k_17_2, k_17_3 in implication relation [k_17_0, k_17_1, k_17_2, k_17_3, k_16_30] are known: k_17_0, k_17_1, k_17_2, k_17_3 ===> k_16_30
k_17_0, k_17_1, k_17_2, k_17_3 in implication relation [k_17_0, k_17_1, k_17_2, k_17_3, k_16_31] are known: k_17_0, k_17_1, k_17_2, k_17_3 ===> k_16_31
k_17_0, k_17_1, k_17_2, k_17_3 in implication relation [k_17_0, k_17_1, k_17_2, k_17_3, k_16_32] are known: k_17_0, k_17_1, k_17_2, k_17_3 ===> k_16_32
k_17_4, k_17_5, k_17_6, k_17_7 in implication relation [k_17_4, k_17_5, k_17_6, k_17_7, k_16_33] are known: k_17_4, k_17_5, k_17_6, k_17_7 ===> k_16_33
k_17_4, k_17_5, k_17_6, k_17_7 in implication relation [k_17_4, k_17_5, k_17_6, k_17_7, k_16_34] are known: k_17_4, k_17_5, k_17_6, k_17_7 ===> k_16_34
k_17_4, k_17_5, k_17_6, k_17_7 in implication relation [k_17_4, k_17_5, k_17_6, k_17_7, k_16_35] are known: k_17_4, k_17_5, k_17_6, k_17_7 ===> k_16_35
k_17_4, k_17_5, k_17_6, k_17_7 in implication relation [k_17_4, k_17_5, k_17_6, k_17_7, k_16_36] are known: k_17_4, k_17_5, k_17_6, k_17_7 ===> k_16_36
############################################################
State 6:
k_3_46 in symmetric relation [k_2_75, k_3_46] are known: k_3_46 ===> k_2_75
k_16_8 in symmetric relation [k_15_37, k_16_8] are known: k_16_8 ===> k_15_37
k_16_9 in symmetric relation [k_15_38, k_16_9] are known: k_16_9 ===> k_15_38
k_16_10 in symmetric relation [k_15_39, k_16_10] are known: k_16_10 ===> k_15_39
k_16_11 in symmetric relation [k_15_40, k_16_11] are known: k_16_11 ===> k_15_40
k_16_12 in symmetric relation [k_15_41, k_16_12] are known: k_16_12 ===> k_15_41
k_16_13 in symmetric relation [k_15_42, k_16_13] are known: k_16_13 ===> k_15_42
k_16_14 in symmetric relation [k_15_43, k_16_14] are known: k_16_14 ===> k_15_43
k_16_15 in symmetric relation [k_15_44, k_16_15] are known: k_16_15 ===> k_15_44
k_16_16 in symmetric relation [k_15_45, k_16_16] are known: k_16_16 ===> k_15_45
k_16_17 in symmetric relation [k_15_46, k_16_17] are known: k_16_17 ===> k_15_46
k_16_18 in symmetric relation [k_15_47, k_16_18] are known: k_16_18 ===> k_15_47
k_16_19 in symmetric relation [k_15_48, k_16_19] are known: k_16_19 ===> k_15_48
k_16_20 in symmetric relation [k_15_49, k_16_20] are known: k_16_20 ===> k_15_49
k_16_21 in symmetric relation [k_15_50, k_16_21] are known: k_16_21 ===> k_15_50
k_16_22 in symmetric relation [k_15_51, k_16_22] are known: k_16_22 ===> k_15_51
k_16_23 in symmetric relation [k_15_52, k_16_23] are known: k_16_23 ===> k_15_52
k_16_24 in symmetric relation [k_15_53, k_16_24] are known: k_16_24 ===> k_15_53
k_16_25 in symmetric relation [k_15_54, k_16_25] are known: k_16_25 ===> k_15_54
k_16_26 in symmetric relation [k_15_55, k_16_26] are known: k_16_26 ===> k_15_55
k_16_27 in symmetric relation [k_15_56, k_16_27] are known: k_16_27 ===> k_15_56
k_16_28 in symmetric relation [k_15_57, k_16_28] are known: k_16_28 ===> k_15_57
k_16_29 in symmetric relation [k_15_58, k_16_29] are known: k_16_29 ===> k_15_58
k_16_30 in symmetric relation [k_15_59, k_16_30] are known: k_16_30 ===> k_15_59
k_16_31 in symmetric relation [k_15_60, k_16_31] are known: k_16_31 ===> k_15_60
k_16_32 in symmetric relation [k_15_61, k_16_32] are known: k_16_32 ===> k_15_61
k_16_33 in symmetric relation [k_15_62, k_16_33] are known: k_16_33 ===> k_15_62
k_16_34 in symmetric relation [k_15_63, k_16_34] are known: k_16_34 ===> k_15_63
k_16_35 in symmetric relation [k_15_64, k_16_35] are known: k_16_35 ===> k_15_64
k_16_36 in symmetric relation [k_15_65, k_16_36] are known: k_16_36 ===> k_15_65
k_16_37 in symmetric relation [k_15_66, k_16_37] are known: k_16_37 ===> k_15_66
k_16_38 in symmetric relation [k_15_67, k_16_38] are known: k_16_38 ===> k_15_67
k_16_39 in symmetric relation [k_15_68, k_16_39] are known: k_16_39 ===> k_15_68
k_16_40 in symmetric relation [k_15_69, k_16_40] are known: k_16_40 ===> k_15_69
k_16_41 in symmetric relation [k_15_70, k_16_41] are known: k_16_41 ===> k_15_70
k_16_42 in symmetric relation [k_15_71, k_16_42] are known: k_16_42 ===> k_15_71
k_16_43 in symmetric relation [k_15_72, k_16_43] are known: k_16_43 ===> k_15_72
k_16_44 in symmetric relation [k_15_73, k_16_44] are known: k_16_44 ===> k_15_73
k_16_45 in symmetric relation [k_15_74, k_16_45] are known: k_16_45 ===> k_15_74
k_16_48 in symmetric relation [k_15_77, k_16_48] are known: k_16_48 ===> k_15_77
k_16_49 in symmetric relation [k_15_78, k_16_49] are known: k_16_49 ===> k_15_78
k_16_50 in symmetric relation [k_15_79, k_16_50] are known: k_16_50 ===> k_15_79
k_16_51 in symmetric relation [k_15_0, k_16_51] are known: k_16_51 ===> k_15_0
k_16_69 in symmetric relation [k_15_18, k_16_69] are known: k_16_69 ===> k_15_18
k_16_70 in symmetric relation [k_15_19, k_16_70] are known: k_16_70 ===> k_15_19
k_16_71 in symmetric relation [k_15_20, k_16_71] are known: k_16_71 ===> k_15_20
k_16_72 in symmetric relation [k_15_21, k_16_72] are known: k_16_72 ===> k_15_21
k_16_73 in symmetric relation [k_15_22, k_16_73] are known: k_16_73 ===> k_15_22
k_16_74 in symmetric relation [k_15_23, k_16_74] are known: k_16_74 ===> k_15_23
k_16_75 in symmetric relation [k_15_24, k_16_75] are known: k_16_75 ===> k_15_24
k_16_76 in symmetric relation [k_15_25, k_16_76] are known: k_16_76 ===> k_15_25
k_16_77 in symmetric relation [k_15_26, k_16_77] are known: k_16_77 ===> k_15_26
k_16_78 in symmetric relation [k_15_27, k_16_78] are known: k_16_78 ===> k_15_27
k_16_79 in symmetric relation [k_15_28, k_16_79] are known: k_16_79 ===> k_15_28
k_16_0, k_16_1, k_16_2, k_16_3 in implication relation [k_16_0, k_16_1, k_16_2, k_16_3, k_15_29] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_29
k_16_0, k_16_1, k_16_2, k_16_3 in implication relation [k_16_0, k_16_1, k_16_2, k_16_3, k_15_30] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_30
k_16_0, k_16_1, k_16_2, k_16_3 in implication relation [k_16_0, k_16_1, k_16_2, k_16_3, k_15_31] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_31
k_16_0, k_16_1, k_16_2, k_16_3 in implication relation [k_16_0, k_16_1, k_16_2, k_16_3, k_15_32] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_32
k_16_4, k_16_5, k_16_6, k_16_7 in implication relation [k_16_4, k_16_5, k_16_6, k_16_7, k_15_33] are known: k_16_4, k_16_5, k_16_6, k_16_7 ===> k_15_33
k_16_4, k_16_5, k_16_6, k_16_7 in implication relation [k_16_4, k_16_5, k_16_6, k_16_7, k_15_34] are known: k_16_4, k_16_5, k_16_6, k_16_7 ===> k_15_34
k_16_4, k_16_5, k_16_6, k_16_7 in implication relation [k_16_4, k_16_5, k_16_6, k_16_7, k_15_35] are known: k_16_4, k_16_5, k_16_6, k_16_7 ===> k_15_35
k_16_4, k_16_5, k_16_6, k_16_7 in implication relation [k_16_4, k_16_5, k_16_6, k_16_7, k_15_36] are known: k_16_4, k_16_5, k_16_6, k_16_7 ===> k_15_36
############################################################
State 7:
k_2_75 in symmetric relation [k_1_24, k_2_75] are known: k_2_75 ===> k_1_24
k_15_18 in symmetric relation [k_14_47, k_15_18] are known: k_15_18 ===> k_14_47
k_15_19 in symmetric relation [k_14_48, k_15_19] are known: k_15_19 ===> k_14_48
k_15_20 in symmetric relation [k_14_49, k_15_20] are known: k_15_20 ===> k_14_49
k_15_21 in symmetric relation [k_14_50, k_15_21] are known: k_15_21 ===> k_14_50
k_15_22 in symmetric relation [k_14_51, k_15_22] are known: k_15_22 ===> k_14_51
k_15_23 in symmetric relation [k_14_52, k_15_23] are known: k_15_23 ===> k_14_52
k_15_24 in symmetric relation [k_14_53, k_15_24] are known: k_15_24 ===> k_14_53
k_15_25 in symmetric relation [k_14_54, k_15_25] are known: k_15_25 ===> k_14_54
k_15_26 in symmetric relation [k_14_55, k_15_26] are known: k_15_26 ===> k_14_55
k_15_27 in symmetric relation [k_14_56, k_15_27] are known: k_15_27 ===> k_14_56
k_15_28 in symmetric relation [k_14_57, k_15_28] are known: k_15_28 ===> k_14_57
k_15_29 in symmetric relation [k_14_58, k_15_29] are known: k_15_29 ===> k_14_58
k_15_30 in symmetric relation [k_14_59, k_15_30] are known: k_15_30 ===> k_14_59
k_15_31 in symmetric relation [k_14_60, k_15_31] are known: k_15_31 ===> k_14_60
k_15_32 in symmetric relation [k_14_61, k_15_32] are known: k_15_32 ===> k_14_61
k_15_33 in symmetric relation [k_14_62, k_15_33] are known: k_15_33 ===> k_14_62
k_15_34 in symmetric relation [k_14_63, k_15_34] are known: k_15_34 ===> k_14_63
k_15_35 in symmetric relation [k_14_64, k_15_35] are known: k_15_35 ===> k_14_64
k_15_36 in symmetric relation [k_14_65, k_15_36] are known: k_15_36 ===> k_14_65
k_15_37 in symmetric relation [k_14_66, k_15_37] are known: k_15_37 ===> k_14_66
k_15_38 in symmetric relation [k_14_67, k_15_38] are known: k_15_38 ===> k_14_67
k_15_39 in symmetric relation [k_14_68, k_15_39] are known: k_15_39 ===> k_14_68
k_15_40 in symmetric relation [k_14_69, k_15_40] are known: k_15_40 ===> k_14_69
k_15_41 in symmetric relation [k_14_70, k_15_41] are known: k_15_41 ===> k_14_70
k_15_42 in symmetric relation [k_14_71, k_15_42] are known: k_15_42 ===> k_14_71
k_15_43 in symmetric relation [k_14_72, k_15_43] are known: k_15_43 ===> k_14_72
k_15_44 in symmetric relation [k_14_73, k_15_44] are known: k_15_44 ===> k_14_73
k_15_45 in symmetric relation [k_14_74, k_15_45] are known: k_15_45 ===> k_14_74
k_15_46 in symmetric relation [k_14_75, k_15_46] are known: k_15_46 ===> k_14_75
k_15_47 in symmetric relation [k_14_76, k_15_47] are known: k_15_47 ===> k_14_76
k_15_48 in symmetric relation [k_14_77, k_15_48] are known: k_15_48 ===> k_14_77
k_15_49 in symmetric relation [k_14_78, k_15_49] are known: k_15_49 ===> k_14_78
k_15_50 in symmetric relation [k_14_79, k_15_50] are known: k_15_50 ===> k_14_79
k_15_51 in symmetric relation [k_14_0, k_15_51] are known: k_15_51 ===> k_14_0
k_15_52 in symmetric relation [k_14_1, k_15_52] are known: k_15_52 ===> k_14_1
k_15_53 in symmetric relation [k_14_2, k_15_53] are known: k_15_53 ===> k_14_2
k_15_54 in symmetric relation [k_14_3, k_15_54] are known: k_15_54 ===> k_14_3
k_15_55 in symmetric relation [k_14_4, k_15_55] are known: k_15_55 ===> k_14_4
k_15_56 in symmetric relation [k_14_5, k_15_56] are known: k_15_56 ===> k_14_5
k_15_57 in symmetric relation [k_14_6, k_15_57] are known: k_15_57 ===> k_14_6
k_15_58 in symmetric relation [k_14_7, k_15_58] are known: k_15_58 ===> k_14_7
k_15_59 in symmetric relation [k_14_8, k_15_59] are known: k_15_59 ===> k_14_8
k_15_60 in symmetric relation [k_14_9, k_15_60] are known: k_15_60 ===> k_14_9
k_15_61 in symmetric relation [k_14_10, k_15_61] are known: k_15_61 ===> k_14_10
k_15_62 in symmetric relation [k_14_11, k_15_62] are known: k_15_62 ===> k_14_11
k_15_63 in symmetric relation [k_14_12, k_15_63] are known: k_15_63 ===> k_14_12
k_15_64 in symmetric relation [k_14_13, k_15_64] are known: k_15_64 ===> k_14_13
k_15_65 in symmetric relation [k_14_14, k_15_65] are known: k_15_65 ===> k_14_14
k_15_66 in symmetric relation [k_14_15, k_15_66] are known: k_15_66 ===> k_14_15
k_15_67 in symmetric relation [k_14_16, k_15_67] are known: k_15_67 ===> k_14_16
k_15_68 in symmetric relation [k_14_17, k_15_68] are known: k_15_68 ===> k_14_17
k_15_69 in symmetric relation [k_14_18, k_15_69] are known: k_15_69 ===> k_14_18
k_15_70 in symmetric relation [k_14_19, k_15_70] are known: k_15_70 ===> k_14_19
k_15_71 in symmetric relation [k_14_20, k_15_71] are known: k_15_71 ===> k_14_20
k_15_72 in symmetric relation [k_14_21, k_15_72] are known: k_15_72 ===> k_14_21
k_15_73 in symmetric relation [k_14_22, k_15_73] are known: k_15_73 ===> k_14_22
k_15_74 in symmetric relation [k_14_23, k_15_74] are known: k_15_74 ===> k_14_23
k_15_77 in symmetric relation [k_14_26, k_15_77] are known: k_15_77 ===> k_14_26
k_15_78 in symmetric relation [k_14_27, k_15_78] are known: k_15_78 ===> k_14_27
k_15_79 in symmetric relation [k_14_28, k_15_79] are known: k_15_79 ===> k_14_28
############################################################
State 8:
k_1_24 in symmetric relation [k_0_53, k_1_24] are known: k_1_24 ===> k_0_53
k_14_8 in symmetric relation [k_13_37, k_14_8] are known: k_14_8 ===> k_13_37
k_14_9 in symmetric relation [k_13_38, k_14_9] are known: k_14_9 ===> k_13_38
k_14_10 in symmetric relation [k_13_39, k_14_10] are known: k_14_10 ===> k_13_39
k_14_11 in symmetric relation [k_13_40, k_14_11] are known: k_14_11 ===> k_13_40
k_14_12 in symmetric relation [k_13_41, k_14_12] are known: k_14_12 ===> k_13_41
k_14_13 in symmetric relation [k_13_42, k_14_13] are known: k_14_13 ===> k_13_42
k_14_14 in symmetric relation [k_13_43, k_14_14] are known: k_14_14 ===> k_13_43
k_14_15 in symmetric relation [k_13_44, k_14_15] are known: k_14_15 ===> k_13_44
k_14_16 in symmetric relation [k_13_45, k_14_16] are known: k_14_16 ===> k_13_45
k_14_17 in symmetric relation [k_13_46, k_14_17] are known: k_14_17 ===> k_13_46
k_14_18 in symmetric relation [k_13_47, k_14_18] are known: k_14_18 ===> k_13_47
k_14_19 in symmetric relation [k_13_48, k_14_19] are known: k_14_19 ===> k_13_48
k_14_20 in symmetric relation [k_13_49, k_14_20] are known: k_14_20 ===> k_13_49
k_14_21 in symmetric relation [k_13_50, k_14_21] are known: k_14_21 ===> k_13_50
k_14_22 in symmetric relation [k_13_51, k_14_22] are known: k_14_22 ===> k_13_51
k_14_23 in symmetric relation [k_13_52, k_14_23] are known: k_14_23 ===> k_13_52
k_14_26 in symmetric relation [k_13_55, k_14_26] are known: k_14_26 ===> k_13_55
k_14_27 in symmetric relation [k_13_56, k_14_27] are known: k_14_27 ===> k_13_56
k_14_28 in symmetric relation [k_13_57, k_14_28] are known: k_14_28 ===> k_13_57
k_14_47 in symmetric relation [k_13_76, k_14_47] are known: k_14_47 ===> k_13_76
k_14_48 in symmetric relation [k_13_77, k_14_48] are known: k_14_48 ===> k_13_77
k_14_49 in symmetric relation [k_13_78, k_14_49] are known: k_14_49 ===> k_13_78
k_14_50 in symmetric relation [k_13_79, k_14_50] are known: k_14_50 ===> k_13_79
k_14_51 in symmetric relation [k_13_0, k_14_51] are known: k_14_51 ===> k_13_0
k_14_52 in symmetric relation [k_13_1, k_14_52] are known: k_14_52 ===> k_13_1
k_14_53 in symmetric relation [k_13_2, k_14_53] are known: k_14_53 ===> k_13_2
k_14_54 in symmetric relation [k_13_3, k_14_54] are known: k_14_54 ===> k_13_3
k_14_55 in symmetric relation [k_13_4, k_14_55] are known: k_14_55 ===> k_13_4
k_14_56 in symmetric relation [k_13_5, k_14_56] are known: k_14_56 ===> k_13_5
k_14_57 in symmetric relation [k_13_6, k_14_57] are known: k_14_57 ===> k_13_6
k_14_58 in symmetric relation [k_13_7, k_14_58] are known: k_14_58 ===> k_13_7
k_14_59 in symmetric relation [k_13_8, k_14_59] are known: k_14_59 ===> k_13_8
k_14_60 in symmetric relation [k_13_9, k_14_60] are known: k_14_60 ===> k_13_9
k_14_61 in symmetric relation [k_13_10, k_14_61] are known: k_14_61 ===> k_13_10
k_14_62 in symmetric relation [k_13_11, k_14_62] are known: k_14_62 ===> k_13_11
k_14_63 in symmetric relation [k_13_12, k_14_63] are known: k_14_63 ===> k_13_12
k_14_64 in symmetric relation [k_13_13, k_14_64] are known: k_14_64 ===> k_13_13
k_14_65 in symmetric relation [k_13_14, k_14_65] are known: k_14_65 ===> k_13_14
k_14_66 in symmetric relation [k_13_15, k_14_66] are known: k_14_66 ===> k_13_15
k_14_67 in symmetric relation [k_13_16, k_14_67] are known: k_14_67 ===> k_13_16
k_14_68 in symmetric relation [k_13_17, k_14_68] are known: k_14_68 ===> k_13_17
k_14_69 in symmetric relation [k_13_18, k_14_69] are known: k_14_69 ===> k_13_18
k_14_70 in symmetric relation [k_13_19, k_14_70] are known: k_14_70 ===> k_13_19
k_14_71 in symmetric relation [k_13_20, k_14_71] are known: k_14_71 ===> k_13_20
k_14_72 in symmetric relation [k_13_21, k_14_72] are known: k_14_72 ===> k_13_21
k_14_73 in symmetric relation [k_13_22, k_14_73] are known: k_14_73 ===> k_13_22
k_14_74 in symmetric relation [k_13_23, k_14_74] are known: k_14_74 ===> k_13_23
k_14_75 in symmetric relation [k_13_24, k_14_75] are known: k_14_75 ===> k_13_24
k_14_76 in symmetric relation [k_13_25, k_14_76] are known: k_14_76 ===> k_13_25
k_14_77 in symmetric relation [k_13_26, k_14_77] are known: k_14_77 ===> k_13_26
k_14_78 in symmetric relation [k_13_27, k_14_78] are known: k_14_78 ===> k_13_27
k_14_79 in symmetric relation [k_13_28, k_14_79] are known: k_14_79 ===> k_13_28
k_14_0, k_14_1, k_14_2, k_14_3 in implication relation [k_14_0, k_14_1, k_14_2, k_14_3, k_13_29] are known: k_14_0, k_14_1, k_14_2, k_14_3 ===> k_13_29
k_14_0, k_14_1, k_14_2, k_14_3 in implication relation [k_14_0, k_14_1, k_14_2, k_14_3, k_13_30] are known: k_14_0, k_14_1, k_14_2, k_14_3 ===> k_13_30
k_14_0, k_14_1, k_14_2, k_14_3 in implication relation [k_14_0, k_14_1, k_14_2, k_14_3, k_13_31] are known: k_14_0, k_14_1, k_14_2, k_14_3 ===> k_13_31
k_14_0, k_14_1, k_14_2, k_14_3 in implication relation [k_14_0, k_14_1, k_14_2, k_14_3, k_13_32] are known: k_14_0, k_14_1, k_14_2, k_14_3 ===> k_13_32
k_14_4, k_14_5, k_14_6, k_14_7 in implication relation [k_14_4, k_14_5, k_14_6, k_14_7, k_13_33] are known: k_14_4, k_14_5, k_14_6, k_14_7 ===> k_13_33
k_14_4, k_14_5, k_14_6, k_14_7 in implication relation [k_14_4, k_14_5, k_14_6, k_14_7, k_13_34] are known: k_14_4, k_14_5, k_14_6, k_14_7 ===> k_13_34
k_14_4, k_14_5, k_14_6, k_14_7 in implication relation [k_14_4, k_14_5, k_14_6, k_14_7, k_13_35] are known: k_14_4, k_14_5, k_14_6, k_14_7 ===> k_13_35
k_14_4, k_14_5, k_14_6, k_14_7 in implication relation [k_14_4, k_14_5, k_14_6, k_14_7, k_13_36] are known: k_14_4, k_14_5, k_14_6, k_14_7 ===> k_13_36
############################################################
State 9:
k_13_8 in symmetric relation [k_12_37, k_13_8] are known: k_13_8 ===> k_12_37
k_13_9 in symmetric relation [k_12_38, k_13_9] are known: k_13_9 ===> k_12_38
k_13_10 in symmetric relation [k_12_39, k_13_10] are known: k_13_10 ===> k_12_39
k_13_11 in symmetric relation [k_12_40, k_13_11] are known: k_13_11 ===> k_12_40
k_13_12 in symmetric relation [k_12_41, k_13_12] are known: k_13_12 ===> k_12_41
k_13_13 in symmetric relation [k_12_42, k_13_13] are known: k_13_13 ===> k_12_42
k_13_14 in symmetric relation [k_12_43, k_13_14] are known: k_13_14 ===> k_12_43
k_13_15 in symmetric relation [k_12_44, k_13_15] are known: k_13_15 ===> k_12_44
k_13_16 in symmetric relation [k_12_45, k_13_16] are known: k_13_16 ===> k_12_45
k_13_17 in symmetric relation [k_12_46, k_13_17] are known: k_13_17 ===> k_12_46
k_13_18 in symmetric relation [k_12_47, k_13_18] are known: k_13_18 ===> k_12_47
k_13_19 in symmetric relation [k_12_48, k_13_19] are known: k_13_19 ===> k_12_48
k_13_20 in symmetric relation [k_12_49, k_13_20] are known: k_13_20 ===> k_12_49
k_13_21 in symmetric relation [k_12_50, k_13_21] are known: k_13_21 ===> k_12_50
k_13_22 in symmetric relation [k_12_51, k_13_22] are known: k_13_22 ===> k_12_51
k_13_23 in symmetric relation [k_12_52, k_13_23] are known: k_13_23 ===> k_12_52
k_13_24 in symmetric relation [k_12_53, k_13_24] are known: k_13_24 ===> k_12_53
k_13_25 in symmetric relation [k_12_54, k_13_25] are known: k_13_25 ===> k_12_54
k_13_26 in symmetric relation [k_12_55, k_13_26] are known: k_13_26 ===> k_12_55
k_13_27 in symmetric relation [k_12_56, k_13_27] are known: k_13_27 ===> k_12_56
k_13_28 in symmetric relation [k_12_57, k_13_28] are known: k_13_28 ===> k_12_57
k_13_29 in symmetric relation [k_12_58, k_13_29] are known: k_13_29 ===> k_12_58
k_13_30 in symmetric relation [k_12_59, k_13_30] are known: k_13_30 ===> k_12_59
k_13_31 in symmetric relation [k_12_60, k_13_31] are known: k_13_31 ===> k_12_60
k_13_32 in symmetric relation [k_12_61, k_13_32] are known: k_13_32 ===> k_12_61
k_13_33 in symmetric relation [k_12_62, k_13_33] are known: k_13_33 ===> k_12_62
k_13_34 in symmetric relation [k_12_63, k_13_34] are known: k_13_34 ===> k_12_63
k_13_35 in symmetric relation [k_12_64, k_13_35] are known: k_13_35 ===> k_12_64
k_13_36 in symmetric relation [k_12_65, k_13_36] are known: k_13_36 ===> k_12_65
k_13_37 in symmetric relation [k_12_66, k_13_37] are known: k_13_37 ===> k_12_66
k_13_38 in symmetric relation [k_12_67, k_13_38] are known: k_13_38 ===> k_12_67
k_13_39 in symmetric relation [k_12_68, k_13_39] are known: k_13_39 ===> k_12_68
k_13_40 in symmetric relation [k_12_69, k_13_40] are known: k_13_40 ===> k_12_69
k_13_41 in symmetric relation [k_12_70, k_13_41] are known: k_13_41 ===> k_12_70
k_13_42 in symmetric relation [k_12_71, k_13_42] are known: k_13_42 ===> k_12_71
k_13_43 in symmetric relation [k_12_72, k_13_43] are known: k_13_43 ===> k_12_72
k_13_44 in symmetric relation [k_12_73, k_13_44] are known: k_13_44 ===> k_12_73
k_13_45 in symmetric relation [k_12_74, k_13_45] are known: k_13_45 ===> k_12_74
k_13_46 in symmetric relation [k_12_75, k_13_46] are known: k_13_46 ===> k_12_75
k_13_47 in symmetric relation [k_12_76, k_13_47] are known: k_13_47 ===> k_12_76
k_13_48 in symmetric relation [k_12_77, k_13_48] are known: k_13_48 ===> k_12_77
k_13_49 in symmetric relation [k_12_78, k_13_49] are known: k_13_49 ===> k_12_78
k_13_50 in symmetric relation [k_12_79, k_13_50] are known: k_13_50 ===> k_12_79
k_13_51 in symmetric relation [k_12_0, k_13_51] are known: k_13_51 ===> k_12_0
k_13_52 in symmetric relation [k_12_1, k_13_52] are known: k_13_52 ===> k_12_1
k_13_55 in symmetric relation [k_12_4, k_13_55] are known: k_13_55 ===> k_12_4
k_13_56 in symmetric relation [k_12_5, k_13_56] are known: k_13_56 ===> k_12_5
k_13_57 in symmetric relation [k_12_6, k_13_57] are known: k_13_57 ===> k_12_6
k_13_76 in symmetric relation [k_12_25, k_13_76] are known: k_13_76 ===> k_12_25
k_13_77 in symmetric relation [k_12_26, k_13_77] are known: k_13_77 ===> k_12_26
k_13_78 in symmetric relation [k_12_27, k_13_78] are known: k_13_78 ===> k_12_27
k_13_79 in symmetric relation [k_12_28, k_13_79] are known: k_13_79 ===> k_12_28
k_13_0, k_13_1, k_13_2, k_13_3 in implication relation [k_13_0, k_13_1, k_13_2, k_13_3, k_12_29] are known: k_13_0, k_13_1, k_13_2, k_13_3 ===> k_12_29
k_13_0, k_13_1, k_13_2, k_13_3 in implication relation [k_13_0, k_13_1, k_13_2, k_13_3, k_12_30] are known: k_13_0, k_13_1, k_13_2, k_13_3 ===> k_12_30
k_13_0, k_13_1, k_13_2, k_13_3 in implication relation [k_13_0, k_13_1, k_13_2, k_13_3, k_12_31] are known: k_13_0, k_13_1, k_13_2, k_13_3 ===> k_12_31
k_13_0, k_13_1, k_13_2, k_13_3 in implication relation [k_13_0, k_13_1, k_13_2, k_13_3, k_12_32] are known: k_13_0, k_13_1, k_13_2, k_13_3 ===> k_12_32
k_13_4, k_13_5, k_13_6, k_13_7 in implication relation [k_13_4, k_13_5, k_13_6, k_13_7, k_12_33] are known: k_13_4, k_13_5, k_13_6, k_13_7 ===> k_12_33
k_13_4, k_13_5, k_13_6, k_13_7 in implication relation [k_13_4, k_13_5, k_13_6, k_13_7, k_12_34] are known: k_13_4, k_13_5, k_13_6, k_13_7 ===> k_12_34
k_13_4, k_13_5, k_13_6, k_13_7 in implication relation [k_13_4, k_13_5, k_13_6, k_13_7, k_12_35] are known: k_13_4, k_13_5, k_13_6, k_13_7 ===> k_12_35
k_13_4, k_13_5, k_13_6, k_13_7 in implication relation [k_13_4, k_13_5, k_13_6, k_13_7, k_12_36] are known: k_13_4, k_13_5, k_13_6, k_13_7 ===> k_12_36
############################################################
State 10:
k_12_25 in symmetric relation [k_11_54, k_12_25] are known: k_12_25 ===> k_11_54
k_12_26 in symmetric relation [k_11_55, k_12_26] are known: k_12_26 ===> k_11_55
k_12_27 in symmetric relation [k_11_56, k_12_27] are known: k_12_27 ===> k_11_56
k_12_28 in symmetric relation [k_11_57, k_12_28] are known: k_12_28 ===> k_11_57
k_12_29 in symmetric relation [k_11_58, k_12_29] are known: k_12_29 ===> k_11_58
k_12_30 in symmetric relation [k_11_59, k_12_30] are known: k_12_30 ===> k_11_59
k_12_31 in symmetric relation [k_11_60, k_12_31] are known: k_12_31 ===> k_11_60
k_12_32 in symmetric relation [k_11_61, k_12_32] are known: k_12_32 ===> k_11_61
k_12_33 in symmetric relation [k_11_62, k_12_33] are known: k_12_33 ===> k_11_62
k_12_34 in symmetric relation [k_11_63, k_12_34] are known: k_12_34 ===> k_11_63
k_12_35 in symmetric relation [k_11_64, k_12_35] are known: k_12_35 ===> k_11_64
k_12_36 in symmetric relation [k_11_65, k_12_36] are known: k_12_36 ===> k_11_65
k_12_37 in symmetric relation [k_11_66, k_12_37] are known: k_12_37 ===> k_11_66
k_12_38 in symmetric relation [k_11_67, k_12_38] are known: k_12_38 ===> k_11_67
k_12_39 in symmetric relation [k_11_68, k_12_39] are known: k_12_39 ===> k_11_68
k_12_40 in symmetric relation [k_11_69, k_12_40] are known: k_12_40 ===> k_11_69
k_12_41 in symmetric relation [k_11_70, k_12_41] are known: k_12_41 ===> k_11_70
k_12_42 in symmetric relation [k_11_71, k_12_42] are known: k_12_42 ===> k_11_71
k_12_43 in symmetric relation [k_11_72, k_12_43] are known: k_12_43 ===> k_11_72
k_12_44 in symmetric relation [k_11_73, k_12_44] are known: k_12_44 ===> k_11_73
k_12_45 in symmetric relation [k_11_74, k_12_45] are known: k_12_45 ===> k_11_74
k_12_46 in symmetric relation [k_11_75, k_12_46] are known: k_12_46 ===> k_11_75
k_12_47 in symmetric relation [k_11_76, k_12_47] are known: k_12_47 ===> k_11_76
k_12_48 in symmetric relation [k_11_77, k_12_48] are known: k_12_48 ===> k_11_77
k_12_49 in symmetric relation [k_11_78, k_12_49] are known: k_12_49 ===> k_11_78
k_12_50 in symmetric relation [k_11_79, k_12_50] are known: k_12_50 ===> k_11_79
k_12_51 in symmetric relation [k_11_0, k_12_51] are known: k_12_51 ===> k_11_0
k_12_52 in symmetric relation [k_11_1, k_12_52] are known: k_12_52 ===> k_11_1
k_12_53 in symmetric relation [k_11_2, k_12_53] are known: k_12_53 ===> k_11_2
k_12_54 in symmetric relation [k_11_3, k_12_54] are known: k_12_54 ===> k_11_3
k_12_55 in symmetric relation [k_11_4, k_12_55] are known: k_12_55 ===> k_11_4
k_12_56 in symmetric relation [k_11_5, k_12_56] are known: k_12_56 ===> k_11_5
k_12_57 in symmetric relation [k_11_6, k_12_57] are known: k_12_57 ===> k_11_6
k_12_58 in symmetric relation [k_11_7, k_12_58] are known: k_12_58 ===> k_11_7
k_12_59 in symmetric relation [k_11_8, k_12_59] are known: k_12_59 ===> k_11_8
k_12_60 in symmetric relation [k_11_9, k_12_60] are known: k_12_60 ===> k_11_9
k_12_61 in symmetric relation [k_11_10, k_12_61] are known: k_12_61 ===> k_11_10
k_12_62 in symmetric relation [k_11_11, k_12_62] are known: k_12_62 ===> k_11_11
k_12_63 in symmetric relation [k_11_12, k_12_63] are known: k_12_63 ===> k_11_12
k_12_64 in symmetric relation [k_11_13, k_12_64] are known: k_12_64 ===> k_11_13
k_12_65 in symmetric relation [k_11_14, k_12_65] are known: k_12_65 ===> k_11_14
k_12_66 in symmetric relation [k_11_15, k_12_66] are known: k_12_66 ===> k_11_15
k_12_67 in symmetric relation [k_11_16, k_12_67] are known: k_12_67 ===> k_11_16
k_12_68 in symmetric relation [k_11_17, k_12_68] are known: k_12_68 ===> k_11_17
k_12_69 in symmetric relation [k_11_18, k_12_69] are known: k_12_69 ===> k_11_18
k_12_70 in symmetric relation [k_11_19, k_12_70] are known: k_12_70 ===> k_11_19
k_12_71 in symmetric relation [k_11_20, k_12_71] are known: k_12_71 ===> k_11_20
k_12_72 in symmetric relation [k_11_21, k_12_72] are known: k_12_72 ===> k_11_21
k_12_73 in symmetric relation [k_11_22, k_12_73] are known: k_12_73 ===> k_11_22
k_12_74 in symmetric relation [k_11_23, k_12_74] are known: k_12_74 ===> k_11_23
k_12_75 in symmetric relation [k_11_24, k_12_75] are known: k_12_75 ===> k_11_24
k_12_76 in symmetric relation [k_11_25, k_12_76] are known: k_12_76 ===> k_11_25
k_12_77 in symmetric relation [k_11_26, k_12_77] are known: k_12_77 ===> k_11_26
k_12_78 in symmetric relation [k_11_27, k_12_78] are known: k_12_78 ===> k_11_27
k_12_79 in symmetric relation [k_11_28, k_12_79] are known: k_12_79 ===> k_11_28
k_12_4, k_12_5, k_12_6, k_12_7 in implication relation [k_12_4, k_12_5, k_12_6, k_12_7, k_11_33] are known: k_12_4, k_12_5, k_12_6, k_12_7 ===> k_11_33
k_12_4, k_12_5, k_12_6, k_12_7 in implication relation [k_12_4, k_12_5, k_12_6, k_12_7, k_11_34] are known: k_12_4, k_12_5, k_12_6, k_12_7 ===> k_11_34
k_12_4, k_12_5, k_12_6, k_12_7 in implication relation [k_12_4, k_12_5, k_12_6, k_12_7, k_11_35] are known: k_12_4, k_12_5, k_12_6, k_12_7 ===> k_11_35
k_12_4, k_12_5, k_12_6, k_12_7 in implication relation [k_12_4, k_12_5, k_12_6, k_12_7, k_11_36] are known: k_12_4, k_12_5, k_12_6, k_12_7 ===> k_11_36
############################################################
State 11:
k_11_8 in symmetric relation [k_10_37, k_11_8] are known: k_11_8 ===> k_10_37
k_11_9 in symmetric relation [k_10_38, k_11_9] are known: k_11_9 ===> k_10_38
k_11_10 in symmetric relation [k_10_39, k_11_10] are known: k_11_10 ===> k_10_39
k_11_11 in symmetric relation [k_10_40, k_11_11] are known: k_11_11 ===> k_10_40
k_11_12 in symmetric relation [k_10_41, k_11_12] are known: k_11_12 ===> k_10_41
k_11_13 in symmetric relation [k_10_42, k_11_13] are known: k_11_13 ===> k_10_42
k_11_14 in symmetric relation [k_10_43, k_11_14] are known: k_11_14 ===> k_10_43
k_11_15 in symmetric relation [k_10_44, k_11_15] are known: k_11_15 ===> k_10_44
k_11_16 in symmetric relation [k_10_45, k_11_16] are known: k_11_16 ===> k_10_45
k_11_17 in symmetric relation [k_10_46, k_11_17] are known: k_11_17 ===> k_10_46
k_11_18 in symmetric relation [k_10_47, k_11_18] are known: k_11_18 ===> k_10_47
k_11_19 in symmetric relation [k_10_48, k_11_19] are known: k_11_19 ===> k_10_48
k_11_20 in symmetric relation [k_10_49, k_11_20] are known: k_11_20 ===> k_10_49
k_11_21 in symmetric relation [k_10_50, k_11_21] are known: k_11_21 ===> k_10_50
k_11_22 in symmetric relation [k_10_51, k_11_22] are known: k_11_22 ===> k_10_51
k_11_23 in symmetric relation [k_10_52, k_11_23] are known: k_11_23 ===> k_10_52
k_11_24 in symmetric relation [k_10_53, k_11_24] are known: k_11_24 ===> k_10_53
k_11_25 in symmetric relation [k_10_54, k_11_25] are known: k_11_25 ===> k_10_54
k_11_26 in symmetric relation [k_10_55, k_11_26] are known: k_11_26 ===> k_10_55
k_11_27 in symmetric relation [k_10_56, k_11_27] are known: k_11_27 ===> k_10_56
k_11_28 in symmetric relation [k_10_57, k_11_28] are known: k_11_28 ===> k_10_57
k_11_33 in symmetric relation [k_10_62, k_11_33] are known: k_11_33 ===> k_10_62
k_11_34 in symmetric relation [k_10_63, k_11_34] are known: k_11_34 ===> k_10_63
k_11_35 in symmetric relation [k_10_64, k_11_35] are known: k_11_35 ===> k_10_64
k_11_36 in symmetric relation [k_10_65, k_11_36] are known: k_11_36 ===> k_10_65
k_11_54 in symmetric relation [k_10_3, k_11_54] are known: k_11_54 ===> k_10_3
k_11_55 in symmetric relation [k_10_4, k_11_55] are known: k_11_55 ===> k_10_4
k_11_56 in symmetric relation [k_10_5, k_11_56] are known: k_11_56 ===> k_10_5
k_11_57 in symmetric relation [k_10_6, k_11_57] are known: k_11_57 ===> k_10_6
k_11_58 in symmetric relation [k_10_7, k_11_58] are known: k_11_58 ===> k_10_7
k_11_59 in symmetric relation [k_10_8, k_11_59] are known: k_11_59 ===> k_10_8
k_11_60 in symmetric relation [k_10_9, k_11_60] are known: k_11_60 ===> k_10_9
k_11_61 in symmetric relation [k_10_10, k_11_61] are known: k_11_61 ===> k_10_10
k_11_62 in symmetric relation [k_10_11, k_11_62] are known: k_11_62 ===> k_10_11
k_11_63 in symmetric relation [k_10_12, k_11_63] are known: k_11_63 ===> k_10_12
k_11_64 in symmetric relation [k_10_13, k_11_64] are known: k_11_64 ===> k_10_13
k_11_65 in symmetric relation [k_10_14, k_11_65] are known: k_11_65 ===> k_10_14
k_11_66 in symmetric relation [k_10_15, k_11_66] are known: k_11_66 ===> k_10_15
k_11_67 in symmetric relation [k_10_16, k_11_67] are known: k_11_67 ===> k_10_16
k_11_68 in symmetric relation [k_10_17, k_11_68] are known: k_11_68 ===> k_10_17
k_11_69 in symmetric relation [k_10_18, k_11_69] are known: k_11_69 ===> k_10_18
k_11_70 in symmetric relation [k_10_19, k_11_70] are known: k_11_70 ===> k_10_19
k_11_71 in symmetric relation [k_10_20, k_11_71] are known: k_11_71 ===> k_10_20
k_11_72 in symmetric relation [k_10_21, k_11_72] are known: k_11_72 ===> k_10_21
k_11_73 in symmetric relation [k_10_22, k_11_73] are known: k_11_73 ===> k_10_22
k_11_74 in symmetric relation [k_10_23, k_11_74] are known: k_11_74 ===> k_10_23
k_11_75 in symmetric relation [k_10_24, k_11_75] are known: k_11_75 ===> k_10_24
k_11_76 in symmetric relation [k_10_25, k_11_76] are known: k_11_76 ===> k_10_25
k_11_77 in symmetric relation [k_10_26, k_11_77] are known: k_11_77 ===> k_10_26
k_11_78 in symmetric relation [k_10_27, k_11_78] are known: k_11_78 ===> k_10_27
k_11_79 in symmetric relation [k_10_28, k_11_79] are known: k_11_79 ===> k_10_28
k_11_0, k_11_1, k_11_2, k_11_3 in implication relation [k_11_0, k_11_1, k_11_2, k_11_3, k_10_29] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_29
k_11_0, k_11_1, k_11_2, k_11_3 in implication relation [k_11_0, k_11_1, k_11_2, k_11_3, k_10_30] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_30
k_11_0, k_11_1, k_11_2, k_11_3 in implication relation [k_11_0, k_11_1, k_11_2, k_11_3, k_10_31] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_31
k_11_0, k_11_1, k_11_2, k_11_3 in implication relation [k_11_0, k_11_1, k_11_2, k_11_3, k_10_32] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_32
k_11_4, k_11_5, k_11_6, k_11_7 in implication relation [k_11_4, k_11_5, k_11_6, k_11_7, k_10_33] are known: k_11_4, k_11_5, k_11_6, k_11_7 ===> k_10_33
k_11_4, k_11_5, k_11_6, k_11_7 in implication relation [k_11_4, k_11_5, k_11_6, k_11_7, k_10_34] are known: k_11_4, k_11_5, k_11_6, k_11_7 ===> k_10_34
k_11_4, k_11_5, k_11_6, k_11_7 in implication relation [k_11_4, k_11_5, k_11_6, k_11_7, k_10_35] are known: k_11_4, k_11_5, k_11_6, k_11_7 ===> k_10_35
k_11_4, k_11_5, k_11_6, k_11_7 in implication relation [k_11_4, k_11_5, k_11_6, k_11_7, k_10_36] are known: k_11_4, k_11_5, k_11_6, k_11_7 ===> k_10_36
############################################################
State 12:
k_10_8 in symmetric relation [k_9_37, k_10_8] are known: k_10_8 ===> k_9_37
k_10_9 in symmetric relation [k_9_38, k_10_9] are known: k_10_9 ===> k_9_38
k_10_10 in symmetric relation [k_9_39, k_10_10] are known: k_10_10 ===> k_9_39
k_10_11 in symmetric relation [k_9_40, k_10_11] are known: k_10_11 ===> k_9_40
k_10_12 in symmetric relation [k_9_41, k_10_12] are known: k_10_12 ===> k_9_41
k_10_13 in symmetric relation [k_9_42, k_10_13] are known: k_10_13 ===> k_9_42
k_10_14 in symmetric relation [k_9_43, k_10_14] are known: k_10_14 ===> k_9_43
k_10_15 in symmetric relation [k_9_44, k_10_15] are known: k_10_15 ===> k_9_44
k_10_16 in symmetric relation [k_9_45, k_10_16] are known: k_10_16 ===> k_9_45
k_10_17 in symmetric relation [k_9_46, k_10_17] are known: k_10_17 ===> k_9_46
k_10_18 in symmetric relation [k_9_47, k_10_18] are known: k_10_18 ===> k_9_47
k_10_19 in symmetric relation [k_9_48, k_10_19] are known: k_10_19 ===> k_9_48
k_10_20 in symmetric relation [k_9_49, k_10_20] are known: k_10_20 ===> k_9_49
k_10_21 in symmetric relation [k_9_50, k_10_21] are known: k_10_21 ===> k_9_50
k_10_22 in symmetric relation [k_9_51, k_10_22] are known: k_10_22 ===> k_9_51
k_10_23 in symmetric relation [k_9_52, k_10_23] are known: k_10_23 ===> k_9_52
k_10_24 in symmetric relation [k_9_53, k_10_24] are known: k_10_24 ===> k_9_53
k_10_25 in symmetric relation [k_9_54, k_10_25] are known: k_10_25 ===> k_9_54
k_10_26 in symmetric relation [k_9_55, k_10_26] are known: k_10_26 ===> k_9_55
k_10_27 in symmetric relation [k_9_56, k_10_27] are known: k_10_27 ===> k_9_56
k_10_28 in symmetric relation [k_9_57, k_10_28] are known: k_10_28 ===> k_9_57
k_10_29 in symmetric relation [k_9_58, k_10_29] are known: k_10_29 ===> k_9_58
k_10_30 in symmetric relation [k_9_59, k_10_30] are known: k_10_30 ===> k_9_59
k_10_31 in symmetric relation [k_9_60, k_10_31] are known: k_10_31 ===> k_9_60
k_10_32 in symmetric relation [k_9_61, k_10_32] are known: k_10_32 ===> k_9_61
k_10_33 in symmetric relation [k_9_62, k_10_33] are known: k_10_33 ===> k_9_62
k_10_34 in symmetric relation [k_9_63, k_10_34] are known: k_10_34 ===> k_9_63
k_10_35 in symmetric relation [k_9_64, k_10_35] are known: k_10_35 ===> k_9_64
k_10_36 in symmetric relation [k_9_65, k_10_36] are known: k_10_36 ===> k_9_65
k_10_37 in symmetric relation [k_9_66, k_10_37] are known: k_10_37 ===> k_9_66
k_10_38 in symmetric relation [k_9_67, k_10_38] are known: k_10_38 ===> k_9_67
k_10_39 in symmetric relation [k_9_68, k_10_39] are known: k_10_39 ===> k_9_68
k_10_40 in symmetric relation [k_9_69, k_10_40] are known: k_10_40 ===> k_9_69
k_10_41 in symmetric relation [k_9_70, k_10_41] are known: k_10_41 ===> k_9_70
k_10_42 in symmetric relation [k_9_71, k_10_42] are known: k_10_42 ===> k_9_71
k_10_43 in symmetric relation [k_9_72, k_10_43] are known: k_10_43 ===> k_9_72
k_10_44 in symmetric relation [k_9_73, k_10_44] are known: k_10_44 ===> k_9_73
k_10_45 in symmetric relation [k_9_74, k_10_45] are known: k_10_45 ===> k_9_74
k_10_46 in symmetric relation [k_9_75, k_10_46] are known: k_10_46 ===> k_9_75
k_10_47 in symmetric relation [k_9_76, k_10_47] are known: k_10_47 ===> k_9_76
k_10_48 in symmetric relation [k_9_77, k_10_48] are known: k_10_48 ===> k_9_77
k_10_49 in symmetric relation [k_9_78, k_10_49] are known: k_10_49 ===> k_9_78
k_10_50 in symmetric relation [k_9_79, k_10_50] are known: k_10_50 ===> k_9_79
k_10_51 in symmetric relation [k_9_0, k_10_51] are known: k_10_51 ===> k_9_0
k_10_52 in symmetric relation [k_9_1, k_10_52] are known: k_10_52 ===> k_9_1
k_10_53 in symmetric relation [k_9_2, k_10_53] are known: k_10_53 ===> k_9_2
k_10_54 in symmetric relation [k_9_3, k_10_54] are known: k_10_54 ===> k_9_3
k_10_55 in symmetric relation [k_9_4, k_10_55] are known: k_10_55 ===> k_9_4
k_10_56 in symmetric relation [k_9_5, k_10_56] are known: k_10_56 ===> k_9_5
k_10_57 in symmetric relation [k_9_6, k_10_57] are known: k_10_57 ===> k_9_6
k_10_62 in symmetric relation [k_9_11, k_10_62] are known: k_10_62 ===> k_9_11
k_10_63 in symmetric relation [k_9_12, k_10_63] are known: k_10_63 ===> k_9_12
k_10_64 in symmetric relation [k_9_13, k_10_64] are known: k_10_64 ===> k_9_13
k_10_65 in symmetric relation [k_9_14, k_10_65] are known: k_10_65 ===> k_9_14
k_10_4, k_10_5, k_10_6, k_10_7 in implication relation [k_10_4, k_10_5, k_10_6, k_10_7, k_9_33] are known: k_10_4, k_10_5, k_10_6, k_10_7 ===> k_9_33
k_10_4, k_10_5, k_10_6, k_10_7 in implication relation [k_10_4, k_10_5, k_10_6, k_10_7, k_9_34] are known: k_10_4, k_10_5, k_10_6, k_10_7 ===> k_9_34
k_10_4, k_10_5, k_10_6, k_10_7 in implication relation [k_10_4, k_10_5, k_10_6, k_10_7, k_9_35] are known: k_10_4, k_10_5, k_10_6, k_10_7 ===> k_9_35
k_10_4, k_10_5, k_10_6, k_10_7 in implication relation [k_10_4, k_10_5, k_10_6, k_10_7, k_9_36] are known: k_10_4, k_10_5, k_10_6, k_10_7 ===> k_9_36
############################################################
State 13:
k_9_11 in symmetric relation [k_8_40, k_9_11] are known: k_9_11 ===> k_8_40
k_9_12 in symmetric relation [k_8_41, k_9_12] are known: k_9_12 ===> k_8_41
k_9_13 in symmetric relation [k_8_42, k_9_13] are known: k_9_13 ===> k_8_42
k_9_14 in symmetric relation [k_8_43, k_9_14] are known: k_9_14 ===> k_8_43
k_9_33 in symmetric relation [k_8_62, k_9_33] are known: k_9_33 ===> k_8_62
k_9_34 in symmetric relation [k_8_63, k_9_34] are known: k_9_34 ===> k_8_63
k_9_35 in symmetric relation [k_8_64, k_9_35] are known: k_9_35 ===> k_8_64
k_9_36 in symmetric relation [k_8_65, k_9_36] are known: k_9_36 ===> k_8_65
k_9_37 in symmetric relation [k_8_66, k_9_37] are known: k_9_37 ===> k_8_66
k_9_38 in symmetric relation [k_8_67, k_9_38] are known: k_9_38 ===> k_8_67
k_9_39 in symmetric relation [k_8_68, k_9_39] are known: k_9_39 ===> k_8_68
k_9_40 in symmetric relation [k_8_69, k_9_40] are known: k_9_40 ===> k_8_69
k_9_41 in symmetric relation [k_8_70, k_9_41] are known: k_9_41 ===> k_8_70
k_9_42 in symmetric relation [k_8_71, k_9_42] are known: k_9_42 ===> k_8_71
k_9_43 in symmetric relation [k_8_72, k_9_43] are known: k_9_43 ===> k_8_72
k_9_44 in symmetric relation [k_8_73, k_9_44] are known: k_9_44 ===> k_8_73
k_9_45 in symmetric relation [k_8_74, k_9_45] are known: k_9_45 ===> k_8_74
k_9_46 in symmetric relation [k_8_75, k_9_46] are known: k_9_46 ===> k_8_75
k_9_47 in symmetric relation [k_8_76, k_9_47] are known: k_9_47 ===> k_8_76
k_9_48 in symmetric relation [k_8_77, k_9_48] are known: k_9_48 ===> k_8_77
k_9_49 in symmetric relation [k_8_78, k_9_49] are known: k_9_49 ===> k_8_78
k_9_50 in symmetric relation [k_8_79, k_9_50] are known: k_9_50 ===> k_8_79
k_9_51 in symmetric relation [k_8_0, k_9_51] are known: k_9_51 ===> k_8_0
k_9_52 in symmetric relation [k_8_1, k_9_52] are known: k_9_52 ===> k_8_1
k_9_53 in symmetric relation [k_8_2, k_9_53] are known: k_9_53 ===> k_8_2
k_9_54 in symmetric relation [k_8_3, k_9_54] are known: k_9_54 ===> k_8_3
k_9_55 in symmetric relation [k_8_4, k_9_55] are known: k_9_55 ===> k_8_4
k_9_56 in symmetric relation [k_8_5, k_9_56] are known: k_9_56 ===> k_8_5
k_9_57 in symmetric relation [k_8_6, k_9_57] are known: k_9_57 ===> k_8_6
k_9_58 in symmetric relation [k_8_7, k_9_58] are known: k_9_58 ===> k_8_7
k_9_59 in symmetric relation [k_8_8, k_9_59] are known: k_9_59 ===> k_8_8
k_9_60 in symmetric relation [k_8_9, k_9_60] are known: k_9_60 ===> k_8_9
k_9_61 in symmetric relation [k_8_10, k_9_61] are known: k_9_61 ===> k_8_10
k_9_62 in symmetric relation [k_8_11, k_9_62] are known: k_9_62 ===> k_8_11
k_9_63 in symmetric relation [k_8_12, k_9_63] are known: k_9_63 ===> k_8_12
k_9_64 in symmetric relation [k_8_13, k_9_64] are known: k_9_64 ===> k_8_13
k_9_65 in symmetric relation [k_8_14, k_9_65] are known: k_9_65 ===> k_8_14
k_9_66 in symmetric relation [k_8_15, k_9_66] are known: k_9_66 ===> k_8_15
k_9_67 in symmetric relation [k_8_16, k_9_67] are known: k_9_67 ===> k_8_16
k_9_68 in symmetric relation [k_8_17, k_9_68] are known: k_9_68 ===> k_8_17
k_9_69 in symmetric relation [k_8_18, k_9_69] are known: k_9_69 ===> k_8_18
k_9_70 in symmetric relation [k_8_19, k_9_70] are known: k_9_70 ===> k_8_19
k_9_71 in symmetric relation [k_8_20, k_9_71] are known: k_9_71 ===> k_8_20
k_9_72 in symmetric relation [k_8_21, k_9_72] are known: k_9_72 ===> k_8_21
k_9_73 in symmetric relation [k_8_22, k_9_73] are known: k_9_73 ===> k_8_22
k_9_74 in symmetric relation [k_8_23, k_9_74] are known: k_9_74 ===> k_8_23
k_9_75 in symmetric relation [k_8_24, k_9_75] are known: k_9_75 ===> k_8_24
k_9_76 in symmetric relation [k_8_25, k_9_76] are known: k_9_76 ===> k_8_25
k_9_77 in symmetric relation [k_8_26, k_9_77] are known: k_9_77 ===> k_8_26
k_9_78 in symmetric relation [k_8_27, k_9_78] are known: k_9_78 ===> k_8_27
k_9_79 in symmetric relation [k_8_28, k_9_79] are known: k_9_79 ===> k_8_28
k_9_0, k_9_1, k_9_2, k_9_3 in implication relation [k_9_0, k_9_1, k_9_2, k_9_3, k_8_29] are known: k_9_0, k_9_1, k_9_2, k_9_3 ===> k_8_29
k_9_0, k_9_1, k_9_2, k_9_3 in implication relation [k_9_0, k_9_1, k_9_2, k_9_3, k_8_30] are known: k_9_0, k_9_1, k_9_2, k_9_3 ===> k_8_30
k_9_0, k_9_1, k_9_2, k_9_3 in implication relation [k_9_0, k_9_1, k_9_2, k_9_3, k_8_31] are known: k_9_0, k_9_1, k_9_2, k_9_3 ===> k_8_31
k_9_0, k_9_1, k_9_2, k_9_3 in implication relation [k_9_0, k_9_1, k_9_2, k_9_3, k_8_32] are known: k_9_0, k_9_1, k_9_2, k_9_3 ===> k_8_32
k_9_4, k_9_5, k_9_6, k_9_7 in implication relation [k_9_4, k_9_5, k_9_6, k_9_7, k_8_33] are known: k_9_4, k_9_5, k_9_6, k_9_7 ===> k_8_33
k_9_4, k_9_5, k_9_6, k_9_7 in implication relation [k_9_4, k_9_5, k_9_6, k_9_7, k_8_34] are known: k_9_4, k_9_5, k_9_6, k_9_7 ===> k_8_34
k_9_4, k_9_5, k_9_6, k_9_7 in implication relation [k_9_4, k_9_5, k_9_6, k_9_7, k_8_35] are known: k_9_4, k_9_5, k_9_6, k_9_7 ===> k_8_35
k_9_4, k_9_5, k_9_6, k_9_7 in implication relation [k_9_4, k_9_5, k_9_6, k_9_7, k_8_36] are known: k_9_4, k_9_5, k_9_6, k_9_7 ===> k_8_36
############################################################
State 14:
k_8_8 in symmetric relation [k_7_37, k_8_8] are known: k_8_8 ===> k_7_37
k_8_9 in symmetric relation [k_7_38, k_8_9] are known: k_8_9 ===> k_7_38
k_8_10 in symmetric relation [k_7_39, k_8_10] are known: k_8_10 ===> k_7_39
k_8_11 in symmetric relation [k_7_40, k_8_11] are known: k_8_11 ===> k_7_40
k_8_12 in symmetric relation [k_7_41, k_8_12] are known: k_8_12 ===> k_7_41
k_8_13 in symmetric relation [k_7_42, k_8_13] are known: k_8_13 ===> k_7_42
k_8_14 in symmetric relation [k_7_43, k_8_14] are known: k_8_14 ===> k_7_43
k_8_15 in symmetric relation [k_7_44, k_8_15] are known: k_8_15 ===> k_7_44
k_8_16 in symmetric relation [k_7_45, k_8_16] are known: k_8_16 ===> k_7_45
k_8_17 in symmetric relation [k_7_46, k_8_17] are known: k_8_17 ===> k_7_46
k_8_18 in symmetric relation [k_7_47, k_8_18] are known: k_8_18 ===> k_7_47
k_8_19 in symmetric relation [k_7_48, k_8_19] are known: k_8_19 ===> k_7_48
k_8_20 in symmetric relation [k_7_49, k_8_20] are known: k_8_20 ===> k_7_49
k_8_21 in symmetric relation [k_7_50, k_8_21] are known: k_8_21 ===> k_7_50
k_8_22 in symmetric relation [k_7_51, k_8_22] are known: k_8_22 ===> k_7_51
k_8_23 in symmetric relation [k_7_52, k_8_23] are known: k_8_23 ===> k_7_52
k_8_24 in symmetric relation [k_7_53, k_8_24] are known: k_8_24 ===> k_7_53
k_8_25 in symmetric relation [k_7_54, k_8_25] are known: k_8_25 ===> k_7_54
k_8_26 in symmetric relation [k_7_55, k_8_26] are known: k_8_26 ===> k_7_55
k_8_27 in symmetric relation [k_7_56, k_8_27] are known: k_8_27 ===> k_7_56
k_8_28 in symmetric relation [k_7_57, k_8_28] are known: k_8_28 ===> k_7_57
k_8_29 in symmetric relation [k_7_58, k_8_29] are known: k_8_29 ===> k_7_58
k_8_30 in symmetric relation [k_7_59, k_8_30] are known: k_8_30 ===> k_7_59
k_8_31 in symmetric relation [k_7_60, k_8_31] are known: k_8_31 ===> k_7_60
k_8_32 in symmetric relation [k_7_61, k_8_32] are known: k_8_32 ===> k_7_61
k_8_33 in symmetric relation [k_7_62, k_8_33] are known: k_8_33 ===> k_7_62
k_8_34 in symmetric relation [k_7_63, k_8_34] are known: k_8_34 ===> k_7_63
k_8_35 in symmetric relation [k_7_64, k_8_35] are known: k_8_35 ===> k_7_64
k_8_36 in symmetric relation [k_7_65, k_8_36] are known: k_8_36 ===> k_7_65
k_8_40 in symmetric relation [k_7_69, k_8_40] are known: k_8_40 ===> k_7_69
k_8_41 in symmetric relation [k_7_70, k_8_41] are known: k_8_41 ===> k_7_70
k_8_42 in symmetric relation [k_7_71, k_8_42] are known: k_8_42 ===> k_7_71
k_8_43 in symmetric relation [k_7_72, k_8_43] are known: k_8_43 ===> k_7_72
k_8_62 in symmetric relation [k_7_11, k_8_62] are known: k_8_62 ===> k_7_11
k_8_63 in symmetric relation [k_7_12, k_8_63] are known: k_8_63 ===> k_7_12
k_8_64 in symmetric relation [k_7_13, k_8_64] are known: k_8_64 ===> k_7_13
k_8_65 in symmetric relation [k_7_14, k_8_65] are known: k_8_65 ===> k_7_14
k_8_66 in symmetric relation [k_7_15, k_8_66] are known: k_8_66 ===> k_7_15
k_8_67 in symmetric relation [k_7_16, k_8_67] are known: k_8_67 ===> k_7_16
k_8_68 in symmetric relation [k_7_17, k_8_68] are known: k_8_68 ===> k_7_17
k_8_69 in symmetric relation [k_7_18, k_8_69] are known: k_8_69 ===> k_7_18
k_8_70 in symmetric relation [k_7_19, k_8_70] are known: k_8_70 ===> k_7_19
k_8_71 in symmetric relation [k_7_20, k_8_71] are known: k_8_71 ===> k_7_20
k_8_72 in symmetric relation [k_7_21, k_8_72] are known: k_8_72 ===> k_7_21
k_8_73 in symmetric relation [k_7_22, k_8_73] are known: k_8_73 ===> k_7_22
k_8_74 in symmetric relation [k_7_23, k_8_74] are known: k_8_74 ===> k_7_23
k_8_75 in symmetric relation [k_7_24, k_8_75] are known: k_8_75 ===> k_7_24
k_8_76 in symmetric relation [k_7_25, k_8_76] are known: k_8_76 ===> k_7_25
k_8_77 in symmetric relation [k_7_26, k_8_77] are known: k_8_77 ===> k_7_26
k_8_78 in symmetric relation [k_7_27, k_8_78] are known: k_8_78 ===> k_7_27
k_8_79 in symmetric relation [k_7_28, k_8_79] are known: k_8_79 ===> k_7_28
k_8_0, k_8_1, k_8_2, k_8_3 in implication relation [k_8_0, k_8_1, k_8_2, k_8_3, k_7_29] are known: k_8_0, k_8_1, k_8_2, k_8_3 ===> k_7_29
k_8_0, k_8_1, k_8_2, k_8_3 in implication relation [k_8_0, k_8_1, k_8_2, k_8_3, k_7_30] are known: k_8_0, k_8_1, k_8_2, k_8_3 ===> k_7_30
k_8_0, k_8_1, k_8_2, k_8_3 in implication relation [k_8_0, k_8_1, k_8_2, k_8_3, k_7_31] are known: k_8_0, k_8_1, k_8_2, k_8_3 ===> k_7_31
k_8_0, k_8_1, k_8_2, k_8_3 in implication relation [k_8_0, k_8_1, k_8_2, k_8_3, k_7_32] are known: k_8_0, k_8_1, k_8_2, k_8_3 ===> k_7_32
k_8_4, k_8_5, k_8_6, k_8_7 in implication relation [k_8_4, k_8_5, k_8_6, k_8_7, k_7_33] are known: k_8_4, k_8_5, k_8_6, k_8_7 ===> k_7_33
k_8_4, k_8_5, k_8_6, k_8_7 in implication relation [k_8_4, k_8_5, k_8_6, k_8_7, k_7_34] are known: k_8_4, k_8_5, k_8_6, k_8_7 ===> k_7_34
k_8_4, k_8_5, k_8_6, k_8_7 in implication relation [k_8_4, k_8_5, k_8_6, k_8_7, k_7_35] are known: k_8_4, k_8_5, k_8_6, k_8_7 ===> k_7_35
k_8_4, k_8_5, k_8_6, k_8_7 in implication relation [k_8_4, k_8_5, k_8_6, k_8_7, k_7_36] are known: k_8_4, k_8_5, k_8_6, k_8_7 ===> k_7_36
############################################################
State 15:
k_7_11 in symmetric relation [k_6_40, k_7_11] are known: k_7_11 ===> k_6_40
k_7_12 in symmetric relation [k_6_41, k_7_12] are known: k_7_12 ===> k_6_41
k_7_13 in symmetric relation [k_6_42, k_7_13] are known: k_7_13 ===> k_6_42
k_7_14 in symmetric relation [k_6_43, k_7_14] are known: k_7_14 ===> k_6_43
k_7_15 in symmetric relation [k_6_44, k_7_15] are known: k_7_15 ===> k_6_44
k_7_16 in symmetric relation [k_6_45, k_7_16] are known: k_7_16 ===> k_6_45
k_7_17 in symmetric relation [k_6_46, k_7_17] are known: k_7_17 ===> k_6_46
k_7_18 in symmetric relation [k_6_47, k_7_18] are known: k_7_18 ===> k_6_47
k_7_19 in symmetric relation [k_6_48, k_7_19] are known: k_7_19 ===> k_6_48
k_7_20 in symmetric relation [k_6_49, k_7_20] are known: k_7_20 ===> k_6_49
k_7_21 in symmetric relation [k_6_50, k_7_21] are known: k_7_21 ===> k_6_50
k_7_22 in symmetric relation [k_6_51, k_7_22] are known: k_7_22 ===> k_6_51
k_7_23 in symmetric relation [k_6_52, k_7_23] are known: k_7_23 ===> k_6_52
k_7_24 in symmetric relation [k_6_53, k_7_24] are known: k_7_24 ===> k_6_53
k_7_25 in symmetric relation [k_6_54, k_7_25] are known: k_7_25 ===> k_6_54
k_7_26 in symmetric relation [k_6_55, k_7_26] are known: k_7_26 ===> k_6_55
k_7_27 in symmetric relation [k_6_56, k_7_27] are known: k_7_27 ===> k_6_56
k_7_28 in symmetric relation [k_6_57, k_7_28] are known: k_7_28 ===> k_6_57
k_7_29 in symmetric relation [k_6_58, k_7_29] are known: k_7_29 ===> k_6_58
k_7_30 in symmetric relation [k_6_59, k_7_30] are known: k_7_30 ===> k_6_59
k_7_31 in symmetric relation [k_6_60, k_7_31] are known: k_7_31 ===> k_6_60
k_7_32 in symmetric relation [k_6_61, k_7_32] are known: k_7_32 ===> k_6_61
k_7_33 in symmetric relation [k_6_62, k_7_33] are known: k_7_33 ===> k_6_62
k_7_34 in symmetric relation [k_6_63, k_7_34] are known: k_7_34 ===> k_6_63
k_7_35 in symmetric relation [k_6_64, k_7_35] are known: k_7_35 ===> k_6_64
k_7_36 in symmetric relation [k_6_65, k_7_36] are known: k_7_36 ===> k_6_65
k_7_37 in symmetric relation [k_6_66, k_7_37] are known: k_7_37 ===> k_6_66
k_7_38 in symmetric relation [k_6_67, k_7_38] are known: k_7_38 ===> k_6_67
k_7_39 in symmetric relation [k_6_68, k_7_39] are known: k_7_39 ===> k_6_68
k_7_40 in symmetric relation [k_6_69, k_7_40] are known: k_7_40 ===> k_6_69
k_7_41 in symmetric relation [k_6_70, k_7_41] are known: k_7_41 ===> k_6_70
k_7_42 in symmetric relation [k_6_71, k_7_42] are known: k_7_42 ===> k_6_71
k_7_43 in symmetric relation [k_6_72, k_7_43] are known: k_7_43 ===> k_6_72
k_7_44 in symmetric relation [k_6_73, k_7_44] are known: k_7_44 ===> k_6_73
k_7_45 in symmetric relation [k_6_74, k_7_45] are known: k_7_45 ===> k_6_74
k_7_46 in symmetric relation [k_6_75, k_7_46] are known: k_7_46 ===> k_6_75
k_7_47 in symmetric relation [k_6_76, k_7_47] are known: k_7_47 ===> k_6_76
k_7_48 in symmetric relation [k_6_77, k_7_48] are known: k_7_48 ===> k_6_77
k_7_49 in symmetric relation [k_6_78, k_7_49] are known: k_7_49 ===> k_6_78
k_7_50 in symmetric relation [k_6_79, k_7_50] are known: k_7_50 ===> k_6_79
k_7_51 in symmetric relation [k_6_0, k_7_51] are known: k_7_51 ===> k_6_0
k_7_52 in symmetric relation [k_6_1, k_7_52] are known: k_7_52 ===> k_6_1
k_7_53 in symmetric relation [k_6_2, k_7_53] are known: k_7_53 ===> k_6_2
k_7_54 in symmetric relation [k_6_3, k_7_54] are known: k_7_54 ===> k_6_3
k_7_55 in symmetric relation [k_6_4, k_7_55] are known: k_7_55 ===> k_6_4
k_7_56 in symmetric relation [k_6_5, k_7_56] are known: k_7_56 ===> k_6_5
k_7_57 in symmetric relation [k_6_6, k_7_57] are known: k_7_57 ===> k_6_6
k_7_58 in symmetric relation [k_6_7, k_7_58] are known: k_7_58 ===> k_6_7
k_7_59 in symmetric relation [k_6_8, k_7_59] are known: k_7_59 ===> k_6_8
k_7_60 in symmetric relation [k_6_9, k_7_60] are known: k_7_60 ===> k_6_9
k_7_61 in symmetric relation [k_6_10, k_7_61] are known: k_7_61 ===> k_6_10
k_7_62 in symmetric relation [k_6_11, k_7_62] are known: k_7_62 ===> k_6_11
k_7_63 in symmetric relation [k_6_12, k_7_63] are known: k_7_63 ===> k_6_12
k_7_64 in symmetric relation [k_6_13, k_7_64] are known: k_7_64 ===> k_6_13
k_7_65 in symmetric relation [k_6_14, k_7_65] are known: k_7_65 ===> k_6_14
k_7_69 in symmetric relation [k_6_18, k_7_69] are known: k_7_69 ===> k_6_18
k_7_70 in symmetric relation [k_6_19, k_7_70] are known: k_7_70 ===> k_6_19
k_7_71 in symmetric relation [k_6_20, k_7_71] are known: k_7_71 ===> k_6_20
k_7_72 in symmetric relation [k_6_21, k_7_72] are known: k_7_72 ===> k_6_21
############################################################
State 16:
k_6_8 in symmetric relation [k_5_37, k_6_8] are known: k_6_8 ===> k_5_37
k_6_9 in symmetric relation [k_5_38, k_6_9] are known: k_6_9 ===> k_5_38
k_6_10 in symmetric relation [k_5_39, k_6_10] are known: k_6_10 ===> k_5_39
k_6_11 in symmetric relation [k_5_40, k_6_11] are known: k_6_11 ===> k_5_40
k_6_12 in symmetric relation [k_5_41, k_6_12] are known: k_6_12 ===> k_5_41
k_6_13 in symmetric relation [k_5_42, k_6_13] are known: k_6_13 ===> k_5_42
k_6_14 in symmetric relation [k_5_43, k_6_14] are known: k_6_14 ===> k_5_43
k_6_18 in symmetric relation [k_5_47, k_6_18] are known: k_6_18 ===> k_5_47
k_6_19 in symmetric relation [k_5_48, k_6_19] are known: k_6_19 ===> k_5_48
k_6_20 in symmetric relation [k_5_49, k_6_20] are known: k_6_20 ===> k_5_49
k_6_21 in symmetric relation [k_5_50, k_6_21] are known: k_6_21 ===> k_5_50
k_6_40 in symmetric relation [k_5_69, k_6_40] are known: k_6_40 ===> k_5_69
k_6_41 in symmetric relation [k_5_70, k_6_41] are known: k_6_41 ===> k_5_70
k_6_42 in symmetric relation [k_5_71, k_6_42] are known: k_6_42 ===> k_5_71
k_6_43 in symmetric relation [k_5_72, k_6_43] are known: k_6_43 ===> k_5_72
k_6_44 in symmetric relation [k_5_73, k_6_44] are known: k_6_44 ===> k_5_73
k_6_45 in symmetric relation [k_5_74, k_6_45] are known: k_6_45 ===> k_5_74
k_6_46 in symmetric relation [k_5_75, k_6_46] are known: k_6_46 ===> k_5_75
k_6_47 in symmetric relation [k_5_76, k_6_47] are known: k_6_47 ===> k_5_76
k_6_48 in symmetric relation [k_5_77, k_6_48] are known: k_6_48 ===> k_5_77
k_6_49 in symmetric relation [k_5_78, k_6_49] are known: k_6_49 ===> k_5_78
k_6_50 in symmetric relation [k_5_79, k_6_50] are known: k_6_50 ===> k_5_79
k_6_51 in symmetric relation [k_5_0, k_6_51] are known: k_6_51 ===> k_5_0
k_6_52 in symmetric relation [k_5_1, k_6_52] are known: k_6_52 ===> k_5_1
k_6_53 in symmetric relation [k_5_2, k_6_53] are known: k_6_53 ===> k_5_2
k_6_54 in symmetric relation [k_5_3, k_6_54] are known: k_6_54 ===> k_5_3
k_6_55 in symmetric relation [k_5_4, k_6_55] are known: k_6_55 ===> k_5_4
k_6_56 in symmetric relation [k_5_5, k_6_56] are known: k_6_56 ===> k_5_5
k_6_57 in symmetric relation [k_5_6, k_6_57] are known: k_6_57 ===> k_5_6
k_6_58 in symmetric relation [k_5_7, k_6_58] are known: k_6_58 ===> k_5_7
k_6_59 in symmetric relation [k_5_8, k_6_59] are known: k_6_59 ===> k_5_8
k_6_60 in symmetric relation [k_5_9, k_6_60] are known: k_6_60 ===> k_5_9
k_6_61 in symmetric relation [k_5_10, k_6_61] are known: k_6_61 ===> k_5_10
k_6_62 in symmetric relation [k_5_11, k_6_62] are known: k_6_62 ===> k_5_11
k_6_63 in symmetric relation [k_5_12, k_6_63] are known: k_6_63 ===> k_5_12
k_6_64 in symmetric relation [k_5_13, k_6_64] are known: k_6_64 ===> k_5_13
k_6_65 in symmetric relation [k_5_14, k_6_65] are known: k_6_65 ===> k_5_14
k_6_66 in symmetric relation [k_5_15, k_6_66] are known: k_6_66 ===> k_5_15
k_6_67 in symmetric relation [k_5_16, k_6_67] are known: k_6_67 ===> k_5_16
k_6_68 in symmetric relation [k_5_17, k_6_68] are known: k_6_68 ===> k_5_17
k_6_69 in symmetric relation [k_5_18, k_6_69] are known: k_6_69 ===> k_5_18
k_6_70 in symmetric relation [k_5_19, k_6_70] are known: k_6_70 ===> k_5_19
k_6_71 in symmetric relation [k_5_20, k_6_71] are known: k_6_71 ===> k_5_20
k_6_72 in symmetric relation [k_5_21, k_6_72] are known: k_6_72 ===> k_5_21
k_6_73 in symmetric relation [k_5_22, k_6_73] are known: k_6_73 ===> k_5_22
k_6_74 in symmetric relation [k_5_23, k_6_74] are known: k_6_74 ===> k_5_23
k_6_75 in symmetric relation [k_5_24, k_6_75] are known: k_6_75 ===> k_5_24
k_6_76 in symmetric relation [k_5_25, k_6_76] are known: k_6_76 ===> k_5_25
k_6_77 in symmetric relation [k_5_26, k_6_77] are known: k_6_77 ===> k_5_26
k_6_78 in symmetric relation [k_5_27, k_6_78] are known: k_6_78 ===> k_5_27
k_6_79 in symmetric relation [k_5_28, k_6_79] are known: k_6_79 ===> k_5_28
k_6_0, k_6_1, k_6_2, k_6_3 in implication relation [k_6_0, k_6_1, k_6_2, k_6_3, k_5_29] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_29
k_6_0, k_6_1, k_6_2, k_6_3 in implication relation [k_6_0, k_6_1, k_6_2, k_6_3, k_5_30] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_30
k_6_0, k_6_1, k_6_2, k_6_3 in implication relation [k_6_0, k_6_1, k_6_2, k_6_3, k_5_31] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_31
k_6_0, k_6_1, k_6_2, k_6_3 in implication relation [k_6_0, k_6_1, k_6_2, k_6_3, k_5_32] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_32
k_6_4, k_6_5, k_6_6, k_6_7 in implication relation [k_6_4, k_6_5, k_6_6, k_6_7, k_5_33] are known: k_6_4, k_6_5, k_6_6, k_6_7 ===> k_5_33
k_6_4, k_6_5, k_6_6, k_6_7 in implication relation [k_6_4, k_6_5, k_6_6, k_6_7, k_5_34] are known: k_6_4, k_6_5, k_6_6, k_6_7 ===> k_5_34
k_6_4, k_6_5, k_6_6, k_6_7 in implication relation [k_6_4, k_6_5, k_6_6, k_6_7, k_5_35] are known: k_6_4, k_6_5, k_6_6, k_6_7 ===> k_5_35
k_6_4, k_6_5, k_6_6, k_6_7 in implication relation [k_6_4, k_6_5, k_6_6, k_6_7, k_5_36] are known: k_6_4, k_6_5, k_6_6, k_6_7 ===> k_5_36
############################################################
State 17:
k_5_8 in symmetric relation [k_4_37, k_5_8] are known: k_5_8 ===> k_4_37
k_5_9 in symmetric relation [k_4_38, k_5_9] are known: k_5_9 ===> k_4_38
k_5_10 in symmetric relation [k_4_39, k_5_10] are known: k_5_10 ===> k_4_39
k_5_11 in symmetric relation [k_4_40, k_5_11] are known: k_5_11 ===> k_4_40
k_5_12 in symmetric relation [k_4_41, k_5_12] are known: k_5_12 ===> k_4_41
k_5_13 in symmetric relation [k_4_42, k_5_13] are known: k_5_13 ===> k_4_42
k_5_14 in symmetric relation [k_4_43, k_5_14] are known: k_5_14 ===> k_4_43
k_5_15 in symmetric relation [k_4_44, k_5_15] are known: k_5_15 ===> k_4_44
k_5_16 in symmetric relation [k_4_45, k_5_16] are known: k_5_16 ===> k_4_45
k_5_17 in symmetric relation [k_4_46, k_5_17] are known: k_5_17 ===> k_4_46
k_5_18 in symmetric relation [k_4_47, k_5_18] are known: k_5_18 ===> k_4_47
k_5_19 in symmetric relation [k_4_48, k_5_19] are known: k_5_19 ===> k_4_48
k_5_20 in symmetric relation [k_4_49, k_5_20] are known: k_5_20 ===> k_4_49
k_5_21 in symmetric relation [k_4_50, k_5_21] are known: k_5_21 ===> k_4_50
k_5_22 in symmetric relation [k_4_51, k_5_22] are known: k_5_22 ===> k_4_51
k_5_23 in symmetric relation [k_4_52, k_5_23] are known: k_5_23 ===> k_4_52
k_5_24 in symmetric relation [k_4_53, k_5_24] are known: k_5_24 ===> k_4_53
k_5_25 in symmetric relation [k_4_54, k_5_25] are known: k_5_25 ===> k_4_54
k_5_26 in symmetric relation [k_4_55, k_5_26] are known: k_5_26 ===> k_4_55
k_5_27 in symmetric relation [k_4_56, k_5_27] are known: k_5_27 ===> k_4_56
k_5_28 in symmetric relation [k_4_57, k_5_28] are known: k_5_28 ===> k_4_57
k_5_29 in symmetric relation [k_4_58, k_5_29] are known: k_5_29 ===> k_4_58
k_5_30 in symmetric relation [k_4_59, k_5_30] are known: k_5_30 ===> k_4_59
k_5_31 in symmetric relation [k_4_60, k_5_31] are known: k_5_31 ===> k_4_60
k_5_32 in symmetric relation [k_4_61, k_5_32] are known: k_5_32 ===> k_4_61
k_5_33 in symmetric relation [k_4_62, k_5_33] are known: k_5_33 ===> k_4_62
k_5_34 in symmetric relation [k_4_63, k_5_34] are known: k_5_34 ===> k_4_63
k_5_35 in symmetric relation [k_4_64, k_5_35] are known: k_5_35 ===> k_4_64
k_5_36 in symmetric relation [k_4_65, k_5_36] are known: k_5_36 ===> k_4_65
k_5_37 in symmetric relation [k_4_66, k_5_37] are known: k_5_37 ===> k_4_66
k_5_38 in symmetric relation [k_4_67, k_5_38] are known: k_5_38 ===> k_4_67
k_5_39 in symmetric relation [k_4_68, k_5_39] are known: k_5_39 ===> k_4_68
k_5_40 in symmetric relation [k_4_69, k_5_40] are known: k_5_40 ===> k_4_69
k_5_41 in symmetric relation [k_4_70, k_5_41] are known: k_5_41 ===> k_4_70
k_5_42 in symmetric relation [k_4_71, k_5_42] are known: k_5_42 ===> k_4_71
k_5_43 in symmetric relation [k_4_72, k_5_43] are known: k_5_43 ===> k_4_72
k_5_47 in symmetric relation [k_4_76, k_5_47] are known: k_5_47 ===> k_4_76
k_5_48 in symmetric relation [k_4_77, k_5_48] are known: k_5_48 ===> k_4_77
k_5_49 in symmetric relation [k_4_78, k_5_49] are known: k_5_49 ===> k_4_78
k_5_50 in symmetric relation [k_4_79, k_5_50] are known: k_5_50 ===> k_4_79
k_5_69 in symmetric relation [k_4_18, k_5_69] are known: k_5_69 ===> k_4_18
k_5_70 in symmetric relation [k_4_19, k_5_70] are known: k_5_70 ===> k_4_19
k_5_71 in symmetric relation [k_4_20, k_5_71] are known: k_5_71 ===> k_4_20
k_5_72 in symmetric relation [k_4_21, k_5_72] are known: k_5_72 ===> k_4_21
k_5_73 in symmetric relation [k_4_22, k_5_73] are known: k_5_73 ===> k_4_22
k_5_74 in symmetric relation [k_4_23, k_5_74] are known: k_5_74 ===> k_4_23
k_5_75 in symmetric relation [k_4_24, k_5_75] are known: k_5_75 ===> k_4_24
k_5_76 in symmetric relation [k_4_25, k_5_76] are known: k_5_76 ===> k_4_25
k_5_77 in symmetric relation [k_4_26, k_5_77] are known: k_5_77 ===> k_4_26
k_5_78 in symmetric relation [k_4_27, k_5_78] are known: k_5_78 ===> k_4_27
k_5_79 in symmetric relation [k_4_28, k_5_79] are known: k_5_79 ===> k_4_28
k_5_0, k_5_1, k_5_2, k_5_3 in implication relation [k_5_0, k_5_1, k_5_2, k_5_3, k_4_29] are known: k_5_0, k_5_1, k_5_2, k_5_3 ===> k_4_29
k_5_0, k_5_1, k_5_2, k_5_3 in implication relation [k_5_0, k_5_1, k_5_2, k_5_3, k_4_30] are known: k_5_0, k_5_1, k_5_2, k_5_3 ===> k_4_30
k_5_0, k_5_1, k_5_2, k_5_3 in implication relation [k_5_0, k_5_1, k_5_2, k_5_3, k_4_31] are known: k_5_0, k_5_1, k_5_2, k_5_3 ===> k_4_31
k_5_0, k_5_1, k_5_2, k_5_3 in implication relation [k_5_0, k_5_1, k_5_2, k_5_3, k_4_32] are known: k_5_0, k_5_1, k_5_2, k_5_3 ===> k_4_32
k_5_4, k_5_5, k_5_6, k_5_7 in implication relation [k_5_4, k_5_5, k_5_6, k_5_7, k_4_33] are known: k_5_4, k_5_5, k_5_6, k_5_7 ===> k_4_33
k_5_4, k_5_5, k_5_6, k_5_7 in implication relation [k_5_4, k_5_5, k_5_6, k_5_7, k_4_34] are known: k_5_4, k_5_5, k_5_6, k_5_7 ===> k_4_34
k_5_4, k_5_5, k_5_6, k_5_7 in implication relation [k_5_4, k_5_5, k_5_6, k_5_7, k_4_35] are known: k_5_4, k_5_5, k_5_6, k_5_7 ===> k_4_35
k_5_4, k_5_5, k_5_6, k_5_7 in implication relation [k_5_4, k_5_5, k_5_6, k_5_7, k_4_36] are known: k_5_4, k_5_5, k_5_6, k_5_7 ===> k_4_36
############################################################
State 18:
k_4_18 in symmetric relation [k_3_47, k_4_18] are known: k_4_18 ===> k_3_47
k_4_19 in symmetric relation [k_3_48, k_4_19] are known: k_4_19 ===> k_3_48
k_4_20 in symmetric relation [k_3_49, k_4_20] are known: k_4_20 ===> k_3_49
k_4_21 in symmetric relation [k_3_50, k_4_21] are known: k_4_21 ===> k_3_50
k_4_22 in symmetric relation [k_3_51, k_4_22] are known: k_4_22 ===> k_3_51
k_4_23 in symmetric relation [k_3_52, k_4_23] are known: k_4_23 ===> k_3_52
k_4_24 in symmetric relation [k_3_53, k_4_24] are known: k_4_24 ===> k_3_53
k_4_25 in symmetric relation [k_3_54, k_4_25] are known: k_4_25 ===> k_3_54
k_4_26 in symmetric relation [k_3_55, k_4_26] are known: k_4_26 ===> k_3_55
k_4_27 in symmetric relation [k_3_56, k_4_27] are known: k_4_27 ===> k_3_56
k_4_28 in symmetric relation [k_3_57, k_4_28] are known: k_4_28 ===> k_3_57
k_4_29 in symmetric relation [k_3_58, k_4_29] are known: k_4_29 ===> k_3_58
k_4_30 in symmetric relation [k_3_59, k_4_30] are known: k_4_30 ===> k_3_59
k_4_31 in symmetric relation [k_3_60, k_4_31] are known: k_4_31 ===> k_3_60
k_4_32 in symmetric relation [k_3_61, k_4_32] are known: k_4_32 ===> k_3_61
k_4_33 in symmetric relation [k_3_62, k_4_33] are known: k_4_33 ===> k_3_62
k_4_34 in symmetric relation [k_3_63, k_4_34] are known: k_4_34 ===> k_3_63
k_4_35 in symmetric relation [k_3_64, k_4_35] are known: k_4_35 ===> k_3_64
k_4_36 in symmetric relation [k_3_65, k_4_36] are known: k_4_36 ===> k_3_65
k_4_37 in symmetric relation [k_3_66, k_4_37] are known: k_4_37 ===> k_3_66
k_4_38 in symmetric relation [k_3_67, k_4_38] are known: k_4_38 ===> k_3_67
k_4_39 in symmetric relation [k_3_68, k_4_39] are known: k_4_39 ===> k_3_68
k_4_40 in symmetric relation [k_3_69, k_4_40] are known: k_4_40 ===> k_3_69
k_4_41 in symmetric relation [k_3_70, k_4_41] are known: k_4_41 ===> k_3_70
k_4_42 in symmetric relation [k_3_71, k_4_42] are known: k_4_42 ===> k_3_71
k_4_43 in symmetric relation [k_3_72, k_4_43] are known: k_4_43 ===> k_3_72
k_4_44 in symmetric relation [k_3_73, k_4_44] are known: k_4_44 ===> k_3_73
k_4_45 in symmetric relation [k_3_74, k_4_45] are known: k_4_45 ===> k_3_74
k_4_46 in symmetric relation [k_3_75, k_4_46] are known: k_4_46 ===> k_3_75
k_4_47 in symmetric relation [k_3_76, k_4_47] are known: k_4_47 ===> k_3_76
k_4_48 in symmetric relation [k_3_77, k_4_48] are known: k_4_48 ===> k_3_77
k_4_49 in symmetric relation [k_3_78, k_4_49] are known: k_4_49 ===> k_3_78
k_4_50 in symmetric relation [k_3_79, k_4_50] are known: k_4_50 ===> k_3_79
k_4_51 in symmetric relation [k_3_0, k_4_51] are known: k_4_51 ===> k_3_0
k_4_52 in symmetric relation [k_3_1, k_4_52] are known: k_4_52 ===> k_3_1
k_4_53 in symmetric relation [k_3_2, k_4_53] are known: k_4_53 ===> k_3_2
k_4_54 in symmetric relation [k_3_3, k_4_54] are known: k_4_54 ===> k_3_3
k_4_55 in symmetric relation [k_3_4, k_4_55] are known: k_4_55 ===> k_3_4
k_4_56 in symmetric relation [k_3_5, k_4_56] are known: k_4_56 ===> k_3_5
k_4_57 in symmetric relation [k_3_6, k_4_57] are known: k_4_57 ===> k_3_6
k_4_58 in symmetric relation [k_3_7, k_4_58] are known: k_4_58 ===> k_3_7
k_4_59 in symmetric relation [k_3_8, k_4_59] are known: k_4_59 ===> k_3_8
k_4_60 in symmetric relation [k_3_9, k_4_60] are known: k_4_60 ===> k_3_9
k_4_61 in symmetric relation [k_3_10, k_4_61] are known: k_4_61 ===> k_3_10
k_4_62 in symmetric relation [k_3_11, k_4_62] are known: k_4_62 ===> k_3_11
k_4_63 in symmetric relation [k_3_12, k_4_63] are known: k_4_63 ===> k_3_12
k_4_64 in symmetric relation [k_3_13, k_4_64] are known: k_4_64 ===> k_3_13
k_4_65 in symmetric relation [k_3_14, k_4_65] are known: k_4_65 ===> k_3_14
k_4_66 in symmetric relation [k_3_15, k_4_66] are known: k_4_66 ===> k_3_15
k_4_67 in symmetric relation [k_3_16, k_4_67] are known: k_4_67 ===> k_3_16
k_4_68 in symmetric relation [k_3_17, k_4_68] are known: k_4_68 ===> k_3_17
k_4_69 in symmetric relation [k_3_18, k_4_69] are known: k_4_69 ===> k_3_18
k_4_70 in symmetric relation [k_3_19, k_4_70] are known: k_4_70 ===> k_3_19
k_4_71 in symmetric relation [k_3_20, k_4_71] are known: k_4_71 ===> k_3_20
k_4_72 in symmetric relation [k_3_21, k_4_72] are known: k_4_72 ===> k_3_21
k_4_76 in symmetric relation [k_3_25, k_4_76] are known: k_4_76 ===> k_3_25
k_4_77 in symmetric relation [k_3_26, k_4_77] are known: k_4_77 ===> k_3_26
k_4_78 in symmetric relation [k_3_27, k_4_78] are known: k_4_78 ===> k_3_27
k_4_79 in symmetric relation [k_3_28, k_4_79] are known: k_4_79 ===> k_3_28
############################################################
State 19:
k_3_8 in symmetric relation [k_2_37, k_3_8] are known: k_3_8 ===> k_2_37
k_3_9 in symmetric relation [k_2_38, k_3_9] are known: k_3_9 ===> k_2_38
k_3_10 in symmetric relation [k_2_39, k_3_10] are known: k_3_10 ===> k_2_39
k_3_11 in symmetric relation [k_2_40, k_3_11] are known: k_3_11 ===> k_2_40
k_3_12 in symmetric relation [k_2_41, k_3_12] are known: k_3_12 ===> k_2_41
k_3_13 in symmetric relation [k_2_42, k_3_13] are known: k_3_13 ===> k_2_42
k_3_14 in symmetric relation [k_2_43, k_3_14] are known: k_3_14 ===> k_2_43
k_3_15 in symmetric relation [k_2_44, k_3_15] are known: k_3_15 ===> k_2_44
k_3_16 in symmetric relation [k_2_45, k_3_16] are known: k_3_16 ===> k_2_45
k_3_17 in symmetric relation [k_2_46, k_3_17] are known: k_3_17 ===> k_2_46
k_3_18 in symmetric relation [k_2_47, k_3_18] are known: k_3_18 ===> k_2_47
k_3_19 in symmetric relation [k_2_48, k_3_19] are known: k_3_19 ===> k_2_48
k_3_20 in symmetric relation [k_2_49, k_3_20] are known: k_3_20 ===> k_2_49
k_3_21 in symmetric relation [k_2_50, k_3_21] are known: k_3_21 ===> k_2_50
k_3_25 in symmetric relation [k_2_54, k_3_25] are known: k_3_25 ===> k_2_54
k_3_26 in symmetric relation [k_2_55, k_3_26] are known: k_3_26 ===> k_2_55
k_3_27 in symmetric relation [k_2_56, k_3_27] are known: k_3_27 ===> k_2_56
k_3_28 in symmetric relation [k_2_57, k_3_28] are known: k_3_28 ===> k_2_57
k_3_47 in symmetric relation [k_2_76, k_3_47] are known: k_3_47 ===> k_2_76
k_3_48 in symmetric relation [k_2_77, k_3_48] are known: k_3_48 ===> k_2_77
k_3_49 in symmetric relation [k_2_78, k_3_49] are known: k_3_49 ===> k_2_78
k_3_50 in symmetric relation [k_2_79, k_3_50] are known: k_3_50 ===> k_2_79
k_3_51 in symmetric relation [k_2_0, k_3_51] are known: k_3_51 ===> k_2_0
k_3_52 in symmetric relation [k_2_1, k_3_52] are known: k_3_52 ===> k_2_1
k_3_53 in symmetric relation [k_2_2, k_3_53] are known: k_3_53 ===> k_2_2
k_3_54 in symmetric relation [k_2_3, k_3_54] are known: k_3_54 ===> k_2_3
k_3_55 in symmetric relation [k_2_4, k_3_55] are known: k_3_55 ===> k_2_4
k_3_56 in symmetric relation [k_2_5, k_3_56] are known: k_3_56 ===> k_2_5
k_3_57 in symmetric relation [k_2_6, k_3_57] are known: k_3_57 ===> k_2_6
k_3_58 in symmetric relation [k_2_7, k_3_58] are known: k_3_58 ===> k_2_7
k_3_59 in symmetric relation [k_2_8, k_3_59] are known: k_3_59 ===> k_2_8
k_3_60 in symmetric relation [k_2_9, k_3_60] are known: k_3_60 ===> k_2_9
k_3_61 in symmetric relation [k_2_10, k_3_61] are known: k_3_61 ===> k_2_10
k_3_62 in symmetric relation [k_2_11, k_3_62] are known: k_3_62 ===> k_2_11
k_3_63 in symmetric relation [k_2_12, k_3_63] are known: k_3_63 ===> k_2_12
k_3_64 in symmetric relation [k_2_13, k_3_64] are known: k_3_64 ===> k_2_13
k_3_65 in symmetric relation [k_2_14, k_3_65] are known: k_3_65 ===> k_2_14
k_3_66 in symmetric relation [k_2_15, k_3_66] are known: k_3_66 ===> k_2_15
k_3_67 in symmetric relation [k_2_16, k_3_67] are known: k_3_67 ===> k_2_16
k_3_68 in symmetric relation [k_2_17, k_3_68] are known: k_3_68 ===> k_2_17
k_3_69 in symmetric relation [k_2_18, k_3_69] are known: k_3_69 ===> k_2_18
k_3_70 in symmetric relation [k_2_19, k_3_70] are known: k_3_70 ===> k_2_19
k_3_71 in symmetric relation [k_2_20, k_3_71] are known: k_3_71 ===> k_2_20
k_3_72 in symmetric relation [k_2_21, k_3_72] are known: k_3_72 ===> k_2_21
k_3_73 in symmetric relation [k_2_22, k_3_73] are known: k_3_73 ===> k_2_22
k_3_74 in symmetric relation [k_2_23, k_3_74] are known: k_3_74 ===> k_2_23
k_3_75 in symmetric relation [k_2_24, k_3_75] are known: k_3_75 ===> k_2_24
k_3_76 in symmetric relation [k_2_25, k_3_76] are known: k_3_76 ===> k_2_25
k_3_77 in symmetric relation [k_2_26, k_3_77] are known: k_3_77 ===> k_2_26
k_3_78 in symmetric relation [k_2_27, k_3_78] are known: k_3_78 ===> k_2_27
k_3_79 in symmetric relation [k_2_28, k_3_79] are known: k_3_79 ===> k_2_28
k_3_0, k_3_1, k_3_2, k_3_3 in implication relation [k_3_0, k_3_1, k_3_2, k_3_3, k_2_29] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_29
k_3_0, k_3_1, k_3_2, k_3_3 in implication relation [k_3_0, k_3_1, k_3_2, k_3_3, k_2_30] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_30
k_3_0, k_3_1, k_3_2, k_3_3 in implication relation [k_3_0, k_3_1, k_3_2, k_3_3, k_2_31] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_31
k_3_0, k_3_1, k_3_2, k_3_3 in implication relation [k_3_0, k_3_1, k_3_2, k_3_3, k_2_32] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_32
k_3_4, k_3_5, k_3_6, k_3_7 in implication relation [k_3_4, k_3_5, k_3_6, k_3_7, k_2_33] are known: k_3_4, k_3_5, k_3_6, k_3_7 ===> k_2_33
k_3_4, k_3_5, k_3_6, k_3_7 in implication relation [k_3_4, k_3_5, k_3_6, k_3_7, k_2_34] are known: k_3_4, k_3_5, k_3_6, k_3_7 ===> k_2_34
k_3_4, k_3_5, k_3_6, k_3_7 in implication relation [k_3_4, k_3_5, k_3_6, k_3_7, k_2_35] are known: k_3_4, k_3_5, k_3_6, k_3_7 ===> k_2_35
k_3_4, k_3_5, k_3_6, k_3_7 in implication relation [k_3_4, k_3_5, k_3_6, k_3_7, k_2_36] are known: k_3_4, k_3_5, k_3_6, k_3_7 ===> k_2_36
############################################################
State 20:
k_2_8 in symmetric relation [k_1_37, k_2_8] are known: k_2_8 ===> k_1_37
k_2_9 in symmetric relation [k_1_38, k_2_9] are known: k_2_9 ===> k_1_38
k_2_10 in symmetric relation [k_1_39, k_2_10] are known: k_2_10 ===> k_1_39
k_2_11 in symmetric relation [k_1_40, k_2_11] are known: k_2_11 ===> k_1_40
k_2_12 in symmetric relation [k_1_41, k_2_12] are known: k_2_12 ===> k_1_41
k_2_13 in symmetric relation [k_1_42, k_2_13] are known: k_2_13 ===> k_1_42
k_2_14 in symmetric relation [k_1_43, k_2_14] are known: k_2_14 ===> k_1_43
k_2_15 in symmetric relation [k_1_44, k_2_15] are known: k_2_15 ===> k_1_44
k_2_16 in symmetric relation [k_1_45, k_2_16] are known: k_2_16 ===> k_1_45
k_2_17 in symmetric relation [k_1_46, k_2_17] are known: k_2_17 ===> k_1_46
k_2_18 in symmetric relation [k_1_47, k_2_18] are known: k_2_18 ===> k_1_47
k_2_19 in symmetric relation [k_1_48, k_2_19] are known: k_2_19 ===> k_1_48
k_2_20 in symmetric relation [k_1_49, k_2_20] are known: k_2_20 ===> k_1_49
k_2_21 in symmetric relation [k_1_50, k_2_21] are known: k_2_21 ===> k_1_50
k_2_22 in symmetric relation [k_1_51, k_2_22] are known: k_2_22 ===> k_1_51
k_2_23 in symmetric relation [k_1_52, k_2_23] are known: k_2_23 ===> k_1_52
k_2_24 in symmetric relation [k_1_53, k_2_24] are known: k_2_24 ===> k_1_53
k_2_25 in symmetric relation [k_1_54, k_2_25] are known: k_2_25 ===> k_1_54
k_2_26 in symmetric relation [k_1_55, k_2_26] are known: k_2_26 ===> k_1_55
k_2_27 in symmetric relation [k_1_56, k_2_27] are known: k_2_27 ===> k_1_56
k_2_28 in symmetric relation [k_1_57, k_2_28] are known: k_2_28 ===> k_1_57
k_2_29 in symmetric relation [k_1_58, k_2_29] are known: k_2_29 ===> k_1_58
k_2_30 in symmetric relation [k_1_59, k_2_30] are known: k_2_30 ===> k_1_59
k_2_31 in symmetric relation [k_1_60, k_2_31] are known: k_2_31 ===> k_1_60
k_2_32 in symmetric relation [k_1_61, k_2_32] are known: k_2_32 ===> k_1_61
k_2_33 in symmetric relation [k_1_62, k_2_33] are known: k_2_33 ===> k_1_62
k_2_34 in symmetric relation [k_1_63, k_2_34] are known: k_2_34 ===> k_1_63
k_2_35 in symmetric relation [k_1_64, k_2_35] are known: k_2_35 ===> k_1_64
k_2_36 in symmetric relation [k_1_65, k_2_36] are known: k_2_36 ===> k_1_65
k_2_37 in symmetric relation [k_1_66, k_2_37] are known: k_2_37 ===> k_1_66
k_2_38 in symmetric relation [k_1_67, k_2_38] are known: k_2_38 ===> k_1_67
k_2_39 in symmetric relation [k_1_68, k_2_39] are known: k_2_39 ===> k_1_68
k_2_40 in symmetric relation [k_1_69, k_2_40] are known: k_2_40 ===> k_1_69
k_2_41 in symmetric relation [k_1_70, k_2_41] are known: k_2_41 ===> k_1_70
k_2_42 in symmetric relation [k_1_71, k_2_42] are known: k_2_42 ===> k_1_71
k_2_43 in symmetric relation [k_1_72, k_2_43] are known: k_2_43 ===> k_1_72
k_2_44 in symmetric relation [k_1_73, k_2_44] are known: k_2_44 ===> k_1_73
k_2_45 in symmetric relation [k_1_74, k_2_45] are known: k_2_45 ===> k_1_74
k_2_46 in symmetric relation [k_1_75, k_2_46] are known: k_2_46 ===> k_1_75
k_2_47 in symmetric relation [k_1_76, k_2_47] are known: k_2_47 ===> k_1_76
k_2_48 in symmetric relation [k_1_77, k_2_48] are known: k_2_48 ===> k_1_77
k_2_49 in symmetric relation [k_1_78, k_2_49] are known: k_2_49 ===> k_1_78
k_2_50 in symmetric relation [k_1_79, k_2_50] are known: k_2_50 ===> k_1_79
k_2_54 in symmetric relation [k_1_3, k_2_54] are known: k_2_54 ===> k_1_3
k_2_55 in symmetric relation [k_1_4, k_2_55] are known: k_2_55 ===> k_1_4
k_2_56 in symmetric relation [k_1_5, k_2_56] are known: k_2_56 ===> k_1_5
k_2_57 in symmetric relation [k_1_6, k_2_57] are known: k_2_57 ===> k_1_6
k_2_76 in symmetric relation [k_1_25, k_2_76] are known: k_2_76 ===> k_1_25
k_2_77 in symmetric relation [k_1_26, k_2_77] are known: k_2_77 ===> k_1_26
k_2_78 in symmetric relation [k_1_27, k_2_78] are known: k_2_78 ===> k_1_27
k_2_79 in symmetric relation [k_1_28, k_2_79] are known: k_2_79 ===> k_1_28
k_2_0, k_2_1, k_2_2, k_2_3 in implication relation [k_2_0, k_2_1, k_2_2, k_2_3, k_1_29] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_29
k_2_0, k_2_1, k_2_2, k_2_3 in implication relation [k_2_0, k_2_1, k_2_2, k_2_3, k_1_30] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_30
k_2_0, k_2_1, k_2_2, k_2_3 in implication relation [k_2_0, k_2_1, k_2_2, k_2_3, k_1_31] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_31
k_2_0, k_2_1, k_2_2, k_2_3 in implication relation [k_2_0, k_2_1, k_2_2, k_2_3, k_1_32] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_32
k_2_4, k_2_5, k_2_6, k_2_7 in implication relation [k_2_4, k_2_5, k_2_6, k_2_7, k_1_33] are known: k_2_4, k_2_5, k_2_6, k_2_7 ===> k_1_33
k_2_4, k_2_5, k_2_6, k_2_7 in implication relation [k_2_4, k_2_5, k_2_6, k_2_7, k_1_34] are known: k_2_4, k_2_5, k_2_6, k_2_7 ===> k_1_34
k_2_4, k_2_5, k_2_6, k_2_7 in implication relation [k_2_4, k_2_5, k_2_6, k_2_7, k_1_35] are known: k_2_4, k_2_5, k_2_6, k_2_7 ===> k_1_35
k_2_4, k_2_5, k_2_6, k_2_7 in implication relation [k_2_4, k_2_5, k_2_6, k_2_7, k_1_36] are known: k_2_4, k_2_5, k_2_6, k_2_7 ===> k_1_36
############################################################
State 21:
k_1_25 in symmetric relation [k_0_54, k_1_25] are known: k_1_25 ===> k_0_54
k_1_26 in symmetric relation [k_0_55, k_1_26] are known: k_1_26 ===> k_0_55
k_1_27 in symmetric relation [k_0_56, k_1_27] are known: k_1_27 ===> k_0_56
k_1_28 in symmetric relation [k_0_57, k_1_28] are known: k_1_28 ===> k_0_57
k_1_29 in symmetric relation [k_0_58, k_1_29] are known: k_1_29 ===> k_0_58
k_1_30 in symmetric relation [k_0_59, k_1_30] are known: k_1_30 ===> k_0_59
k_1_31 in symmetric relation [k_0_60, k_1_31] are known: k_1_31 ===> k_0_60
k_1_32 in symmetric relation [k_0_61, k_1_32] are known: k_1_32 ===> k_0_61
k_1_33 in symmetric relation [k_0_62, k_1_33] are known: k_1_33 ===> k_0_62
k_1_34 in symmetric relation [k_0_63, k_1_34] are known: k_1_34 ===> k_0_63
k_1_35 in symmetric relation [k_0_64, k_1_35] are known: k_1_35 ===> k_0_64
k_1_36 in symmetric relation [k_0_65, k_1_36] are known: k_1_36 ===> k_0_65
k_1_37 in symmetric relation [k_0_66, k_1_37] are known: k_1_37 ===> k_0_66
k_1_38 in symmetric relation [k_0_67, k_1_38] are known: k_1_38 ===> k_0_67
k_1_39 in symmetric relation [k_0_68, k_1_39] are known: k_1_39 ===> k_0_68
k_1_40 in symmetric relation [k_0_69, k_1_40] are known: k_1_40 ===> k_0_69
k_1_41 in symmetric relation [k_0_70, k_1_41] are known: k_1_41 ===> k_0_70
k_1_42 in symmetric relation [k_0_71, k_1_42] are known: k_1_42 ===> k_0_71
k_1_43 in symmetric relation [k_0_72, k_1_43] are known: k_1_43 ===> k_0_72
k_1_44 in symmetric relation [k_0_73, k_1_44] are known: k_1_44 ===> k_0_73
k_1_45 in symmetric relation [k_0_74, k_1_45] are known: k_1_45 ===> k_0_74
k_1_46 in symmetric relation [k_0_75, k_1_46] are known: k_1_46 ===> k_0_75
k_1_47 in symmetric relation [k_0_76, k_1_47] are known: k_1_47 ===> k_0_76
k_1_48 in symmetric relation [k_0_77, k_1_48] are known: k_1_48 ===> k_0_77
k_1_49 in symmetric relation [k_0_78, k_1_49] are known: k_1_49 ===> k_0_78
k_1_50 in symmetric relation [k_0_79, k_1_50] are known: k_1_50 ===> k_0_79
k_1_51 in symmetric relation [k_0_0, k_1_51] are known: k_1_51 ===> k_0_0
k_1_52 in symmetric relation [k_0_1, k_1_52] are known: k_1_52 ===> k_0_1
k_1_53 in symmetric relation [k_0_2, k_1_53] are known: k_1_53 ===> k_0_2
k_1_54 in symmetric relation [k_0_3, k_1_54] are known: k_1_54 ===> k_0_3
k_1_55 in symmetric relation [k_0_4, k_1_55] are known: k_1_55 ===> k_0_4
k_1_56 in symmetric relation [k_0_5, k_1_56] are known: k_1_56 ===> k_0_5
k_1_57 in symmetric relation [k_0_6, k_1_57] are known: k_1_57 ===> k_0_6
k_1_58 in symmetric relation [k_0_7, k_1_58] are known: k_1_58 ===> k_0_7
k_1_59 in symmetric relation [k_0_8, k_1_59] are known: k_1_59 ===> k_0_8
k_1_60 in symmetric relation [k_0_9, k_1_60] are known: k_1_60 ===> k_0_9
k_1_61 in symmetric relation [k_0_10, k_1_61] are known: k_1_61 ===> k_0_10
k_1_62 in symmetric relation [k_0_11, k_1_62] are known: k_1_62 ===> k_0_11
k_1_63 in symmetric relation [k_0_12, k_1_63] are known: k_1_63 ===> k_0_12
k_1_64 in symmetric relation [k_0_13, k_1_64] are known: k_1_64 ===> k_0_13
k_1_65 in symmetric relation [k_0_14, k_1_65] are known: k_1_65 ===> k_0_14
k_1_66 in symmetric relation [k_0_15, k_1_66] are known: k_1_66 ===> k_0_15
k_1_67 in symmetric relation [k_0_16, k_1_67] are known: k_1_67 ===> k_0_16
k_1_68 in symmetric relation [k_0_17, k_1_68] are known: k_1_68 ===> k_0_17
k_1_69 in symmetric relation [k_0_18, k_1_69] are known: k_1_69 ===> k_0_18
k_1_70 in symmetric relation [k_0_19, k_1_70] are known: k_1_70 ===> k_0_19
k_1_71 in symmetric relation [k_0_20, k_1_71] are known: k_1_71 ===> k_0_20
k_1_72 in symmetric relation [k_0_21, k_1_72] are known: k_1_72 ===> k_0_21
k_1_73 in symmetric relation [k_0_22, k_1_73] are known: k_1_73 ===> k_0_22
k_1_74 in symmetric relation [k_0_23, k_1_74] are known: k_1_74 ===> k_0_23
k_1_75 in symmetric relation [k_0_24, k_1_75] are known: k_1_75 ===> k_0_24
k_1_76 in symmetric relation [k_0_25, k_1_76] are known: k_1_76 ===> k_0_25
k_1_77 in symmetric relation [k_0_26, k_1_77] are known: k_1_77 ===> k_0_26
k_1_78 in symmetric relation [k_0_27, k_1_78] are known: k_1_78 ===> k_0_27
k_1_79 in symmetric relation [k_0_28, k_1_79] are known: k_1_79 ===> k_0_28
k_1_4, k_1_5, k_1_6, k_1_7 in implication relation [k_1_4, k_1_5, k_1_6, k_1_7, k_0_33] are known: k_1_4, k_1_5, k_1_6, k_1_7 ===> k_0_33
k_1_4, k_1_5, k_1_6, k_1_7 in implication relation [k_1_4, k_1_5, k_1_6, k_1_7, k_0_34] are known: k_1_4, k_1_5, k_1_6, k_1_7 ===> k_0_34
k_1_4, k_1_5, k_1_6, k_1_7 in implication relation [k_1_4, k_1_5, k_1_6, k_1_7, k_0_35] are known: k_1_4, k_1_5, k_1_6, k_1_7 ===> k_0_35
k_1_4, k_1_5, k_1_6, k_1_7 in implication relation [k_1_4, k_1_5, k_1_6, k_1_7, k_0_36] are known: k_1_4, k_1_5, k_1_6, k_1_7 ===> k_0_36
############################################################
The following variables are known in final state:
k_1_3, k_0_33, k_0_34, k_0_35, k_0_36, k_1_4, k_1_5, k_1_6, k_1_7, k_0_45, k_1_16, k_0_46, k_1_17, k_0_47, k_1_18, k_0_48, k_1_19, k_0_53, k_1_24, k_0_54, k_1_25, k_0_55, k_1_26, k_0_56, k_1_27, k_0_57, k_1_28, k_0_58, k_1_29, k_0_59, k_1_30, k_0_60, k_1_31, k_0_61, k_1_32, k_0_62, k_1_33, k_0_63, k_1_34, k_0_64, k_1_35, k_0_65, k_1_36, k_0_66, k_1_37, k_0_67, k_1_38, k_0_68, k_1_39, k_0_69, k_1_40, k_0_70, k_1_41, k_0_71, k_1_42, k_0_72, k_1_43, k_0_73, k_1_44, k_0_74, k_1_45, k_0_75, k_1_46, k_0_76, k_1_47, k_0_77, k_1_48, k_0_78, k_1_49, k_0_79, k_1_50, k_0_0, k_1_51, k_0_1, k_1_52, k_0_2, k_1_53, k_0_3, k_1_54, k_0_4, k_1_55, k_0_5, k_1_56, k_0_6, k_1_57, k_0_7, k_1_58, k_0_8, k_1_59, k_0_9, k_1_60, k_0_10, k_1_61, k_0_11, k_1_62, k_0_12, k_1_63, k_0_13, k_1_64, k_0_14, k_1_65, k_0_15, k_1_66, k_0_16, k_1_67, k_0_17, k_1_68, k_0_18, k_1_69, k_0_19, k_1_70, k_0_20, k_1_71, k_0_21, k_1_72, k_0_22, k_1_73, k_0_23, k_1_74, k_0_24, k_1_75, k_0_25, k_1_76, k_0_26, k_1_77, k_0_27, k_1_78, k_0_28, k_1_79, k_2_0, k_2_1, k_2_2, k_2_3, k_2_4, k_2_5, k_2_6, k_2_7, k_2_8, k_2_9, k_2_10, k_2_11, k_2_12, k_2_13, k_2_14, k_2_15, k_2_16, k_2_17, k_2_18, k_2_19, k_2_20, k_2_21, k_2_22, k_2_23, k_2_24, k_2_25, k_2_26, k_2_27, k_2_28, k_2_29, k_2_30, k_2_31, k_2_32, k_2_33, k_2_34, k_2_35, k_2_36, k_2_37, k_2_38, k_2_39, k_2_40, k_2_41, k_2_42, k_2_43, k_2_44, k_2_45, k_2_46, k_2_47, k_2_48, k_2_49, k_2_50, k_2_54, k_2_55, k_2_56, k_2_57, k_2_58, k_2_67, k_2_68, k_2_69, k_2_70, k_2_75, k_2_76, k_2_77, k_2_78, k_2_79, k_3_0, k_3_1, k_3_2, k_3_3, k_3_4, k_3_5, k_3_6, k_3_7, k_3_8, k_3_9, k_3_10, k_3_11, k_3_12, k_3_13, k_3_14, k_3_15, k_3_16, k_3_17, k_3_18, k_3_19, k_3_20, k_3_21, k_3_25, k_3_26, k_3_27, k_3_28, k_3_29, k_3_38, k_3_39, k_3_40, k_3_41, k_3_46, k_3_47, k_3_48, k_3_49, k_3_50, k_3_51, k_3_52, k_3_53, k_3_54, k_3_55, k_3_56, k_3_57, k_3_58, k_3_59, k_3_60, k_3_61, k_3_62, k_3_63, k_3_64, k_3_65, k_3_66, k_3_67, k_3_68, k_3_69, k_3_70, k_3_71, k_3_72, k_3_73, k_3_74, k_3_75, k_3_76, k_3_77, k_3_78, k_3_79, k_4_9, k_4_10, k_4_11, k_4_12, k_4_17, k_4_18, k_4_19, k_4_20, k_4_21, k_4_22, k_4_23, k_4_24, k_4_25, k_4_26, k_4_27, k_4_28, k_4_29, k_4_30, k_4_31, k_4_32, k_4_33, k_4_34, k_4_35, k_4_36, k_4_37, k_4_38, k_4_39, k_4_40, k_4_41, k_4_42, k_4_43, k_4_44, k_4_45, k_4_46, k_4_47, k_4_48, k_4_49, k_4_50, k_4_51, k_4_52, k_4_53, k_4_54, k_4_55, k_4_56, k_4_57, k_4_58, k_4_59, k_4_60, k_4_61, k_4_62, k_4_63, k_4_64, k_4_65, k_4_66, k_4_67, k_4_68, k_4_69, k_4_70, k_4_71, k_4_72, k_4_76, k_4_77, k_4_78, k_4_79, k_5_0, k_5_1, k_5_2, k_5_3, k_5_4, k_5_5, k_5_6, k_5_7, k_5_8, k_5_9, k_5_10, k_5_11, k_5_12, k_5_13, k_5_14, k_5_15, k_5_16, k_5_17, k_5_18, k_5_19, k_5_20, k_5_21, k_5_22, k_5_23, k_5_24, k_5_25, k_5_26, k_5_27, k_5_28, k_5_29, k_5_30, k_5_31, k_5_32, k_5_33, k_5_34, k_5_35, k_5_36, k_5_37, k_5_38, k_5_39, k_5_40, k_5_41, k_5_42, k_5_43, k_5_47, k_5_48, k_5_49, k_5_50, k_5_60, k_5_61, k_5_62, k_5_63, k_5_68, k_5_69, k_5_70, k_5_71, k_5_72, k_5_73, k_5_74, k_5_75, k_5_76, k_5_77, k_5_78, k_5_79, k_6_0, k_6_1, k_6_2, k_6_3, k_6_4, k_6_5, k_6_6, k_6_7, k_6_8, k_6_9, k_6_10, k_6_11, k_6_12, k_6_13, k_6_14, k_6_18, k_6_19, k_6_20, k_6_21, k_6_31, k_6_32, k_6_33, k_6_34, k_6_39, k_6_40, k_6_41, k_6_42, k_6_43, k_6_44, k_6_45, k_6_46, k_6_47, k_6_48, k_6_49, k_6_50, k_6_51, k_6_52, k_6_53, k_6_54, k_6_55, k_6_56, k_6_57, k_6_58, k_6_59, k_6_60, k_6_61, k_6_62, k_6_63, k_6_64, k_6_65, k_6_66, k_6_67, k_6_68, k_6_69, k_6_70, k_6_71, k_6_72, k_6_73, k_6_74, k_6_75, k_6_76, k_6_77, k_6_78, k_6_79, k_7_10, k_7_11, k_7_12, k_7_13, k_7_14, k_7_15, k_7_16, k_7_17, k_7_18, k_7_19, k_7_20, k_7_21, k_7_22, k_7_23, k_7_24, k_7_25, k_7_26, k_7_27, k_7_28, k_7_29, k_7_30, k_7_31, k_7_32, k_7_33, k_7_34, k_7_35, k_7_36, k_7_37, k_7_38, k_7_39, k_7_40, k_7_41, k_7_42, k_7_43, k_7_44, k_7_45, k_7_46, k_7_47, k_7_48, k_7_49, k_7_50, k_7_51, k_7_52, k_7_53, k_7_54, k_7_55, k_7_56, k_7_57, k_7_58, k_7_59, k_7_60, k_7_61, k_7_62, k_7_63, k_7_64, k_7_65, k_7_69, k_7_70, k_7_71, k_7_72, k_8_0, k_8_1, k_8_2, k_8_3, k_8_4, k_8_5, k_8_6, k_8_7, k_8_8, k_8_9, k_8_10, k_8_11, k_8_12, k_8_13, k_8_14, k_8_15, k_8_16, k_8_17, k_8_18, k_8_19, k_8_20, k_8_21, k_8_22, k_8_23, k_8_24, k_8_25, k_8_26, k_8_27, k_8_28, k_8_29, k_8_30, k_8_31, k_8_32, k_8_33, k_8_34, k_8_35, k_8_36, k_8_40, k_8_41, k_8_42, k_8_43, k_8_61, k_8_62, k_8_63, k_8_64, k_8_65, k_8_66, k_8_67, k_8_68, k_8_69, k_8_70, k_8_71, k_8_72, k_8_73, k_8_74, k_8_75, k_8_76, k_8_77, k_8_78, k_8_79, k_9_0, k_9_1, k_9_2, k_9_3, k_9_4, k_9_5, k_9_6, k_9_7, k_9_11, k_9_12, k_9_13, k_9_14, k_9_32, k_9_33, k_9_34, k_9_35, k_9_36, k_9_37, k_9_38, k_9_39, k_9_40, k_9_41, k_9_42, k_9_43, k_9_44, k_9_45, k_9_46, k_9_47, k_9_48, k_9_49, k_9_50, k_9_51, k_9_52, k_9_53, k_9_54, k_9_55, k_9_56, k_9_57, k_9_58, k_9_59, k_9_60, k_9_61, k_9_62, k_9_63, k_9_64, k_9_65, k_9_66, k_9_67, k_9_68, k_9_69, k_9_70, k_9_71, k_9_72, k_9_73, k_9_74, k_9_75, k_9_76, k_9_77, k_9_78, k_9_79, k_10_3, k_10_4, k_10_5, k_10_6, k_10_7, k_10_8, k_10_9, k_10_10, k_10_11, k_10_12, k_10_13, k_10_14, k_10_15, k_10_16, k_10_17, k_10_18, k_10_19, k_10_20, k_10_21, k_10_22, k_10_23, k_10_24, k_10_25, k_10_26, k_10_27, k_10_28, k_10_29, k_10_30, k_10_31, k_10_32, k_10_33, k_10_34, k_10_35, k_10_36, k_10_37, k_10_38, k_10_39, k_10_40, k_10_41, k_10_42, k_10_43, k_10_44, k_10_45, k_10_46, k_10_47, k_10_48, k_10_49, k_10_50, k_10_51, k_10_52, k_10_53, k_10_54, k_10_55, k_10_56, k_10_57, k_10_58, k_10_62, k_10_63, k_10_64, k_10_65, k_11_0, k_11_1, k_11_2, k_11_3, k_11_4, k_11_5, k_11_6, k_11_7, k_11_8, k_11_9, k_11_10, k_11_11, k_11_12, k_11_13, k_11_14, k_11_15, k_11_16, k_11_17, k_11_18, k_11_19, k_11_20, k_11_21, k_11_22, k_11_23, k_11_24, k_11_25, k_11_26, k_11_27, k_11_28, k_11_29, k_11_33, k_11_34, k_11_35, k_11_36, k_11_54, k_11_55, k_11_56, k_11_57, k_11_58, k_11_59, k_11_60, k_11_61, k_11_62, k_11_63, k_11_64, k_11_65, k_11_66, k_11_67, k_11_68, k_11_69, k_11_70, k_11_71, k_11_72, k_11_73, k_11_74, k_11_75, k_11_76, k_11_77, k_11_78, k_11_79, k_12_0, k_12_1, k_12_4, k_12_5, k_12_6, k_12_7, k_12_25, k_12_26, k_12_27, k_12_28, k_12_29, k_12_30, k_12_31, k_12_32, k_12_33, k_12_34, k_12_35, k_12_36, k_12_37, k_12_38, k_12_39, k_12_40, k_12_41, k_12_42, k_12_43, k_12_44, k_12_45, k_12_46, k_12_47, k_12_48, k_12_49, k_12_50, k_12_51, k_12_52, k_12_53, k_12_54, k_12_55, k_12_56, k_12_57, k_12_58, k_12_59, k_12_60, k_12_61, k_12_62, k_12_63, k_12_64, k_12_65, k_12_66, k_12_67, k_12_68, k_12_69, k_12_70, k_12_71, k_12_72, k_12_73, k_12_74, k_12_75, k_12_76, k_12_77, k_12_78, k_12_79, k_13_0, k_13_1, k_13_2, k_13_3, k_13_4, k_13_5, k_13_6, k_13_7, k_13_8, k_13_9, k_13_10, k_13_11, k_13_12, k_13_13, k_13_14, k_13_15, k_13_16, k_13_17, k_13_18, k_13_19, k_13_20, k_13_21, k_13_22, k_13_23, k_13_24, k_13_25, k_13_26, k_13_27, k_13_28, k_13_29, k_13_30, k_13_31, k_13_32, k_13_33, k_13_34, k_13_35, k_13_36, k_13_37, k_13_38, k_13_39, k_13_40, k_13_41, k_13_42, k_13_43, k_13_44, k_13_45, k_13_46, k_13_47, k_13_48, k_13_49, k_13_50, k_13_51, k_13_52, k_13_55, k_13_56, k_13_57, k_13_58, k_13_76, k_13_77, k_13_78, k_13_79, k_14_0, k_14_1, k_14_2, k_14_3, k_14_4, k_14_5, k_14_6, k_14_7, k_14_8, k_14_9, k_14_10, k_14_11, k_14_12, k_14_13, k_14_14, k_14_15, k_14_16, k_14_17, k_14_18, k_14_19, k_14_20, k_14_21, k_14_22, k_14_23, k_14_26, k_14_27, k_14_28, k_14_29, k_14_47, k_14_48, k_14_49, k_14_50, k_14_51, k_14_52, k_14_53, k_14_54, k_14_55, k_14_56, k_14_57, k_14_58, k_14_59, k_14_60, k_14_61, k_14_62, k_14_63, k_14_64, k_14_65, k_14_66, k_14_67, k_14_68, k_14_69, k_14_70, k_14_71, k_14_72, k_14_73, k_14_74, k_14_75, k_14_76, k_14_77, k_14_78, k_14_79, k_15_0, k_15_18, k_15_19, k_15_20, k_15_21, k_15_22, k_15_23, k_15_24, k_15_25, k_15_26, k_15_27, k_15_28, k_15_29, k_15_30, k_15_31, k_15_32, k_15_33, k_15_34, k_15_35, k_15_36, k_15_37, k_15_38, k_15_39, k_15_40, k_15_41, k_15_42, k_15_43, k_15_44, k_15_45, k_15_46, k_15_47, k_15_48, k_15_49, k_15_50, k_15_51, k_15_52, k_15_53, k_15_54, k_15_55, k_15_56, k_15_57, k_15_58, k_15_59, k_15_60, k_15_61, k_15_62, k_15_63, k_15_64, k_15_65, k_15_66, k_15_67, k_15_68, k_15_69, k_15_70, k_15_71, k_15_72, k_15_73, k_15_74, k_15_77, k_15_78, k_15_79, k_16_0, k_16_1, k_16_2, k_16_3, k_16_4, k_16_5, k_16_6, k_16_7, k_16_8, k_16_9, k_16_10, k_16_11, k_16_12, k_16_13, k_16_14, k_16_15, k_16_16, k_16_17, k_16_18, k_16_19, k_16_20, k_16_21, k_16_22, k_16_23, k_16_24, k_16_25, k_16_26, k_16_27, k_16_28, k_16_29, k_16_30, k_16_31, k_16_32, k_16_33, k_16_34, k_16_35, k_16_36, k_16_37, k_16_38, k_16_39, k_16_40, k_16_41, k_16_42, k_16_43, k_16_44, k_16_45, k_16_48, k_16_49, k_16_50, k_16_51, k_16_69, k_16_70, k_16_71, k_16_72, k_16_73, k_16_74, k_16_75, k_16_76, k_16_77, k_16_78, k_16_79, k_17_0, k_17_1, k_17_2, k_17_3, k_17_4, k_17_5, k_17_6, k_17_7, k_17_8, k_17_9, k_17_10, k_17_11, k_17_12, k_17_13, k_17_14, k_17_15, k_17_16, k_17_19, k_17_20, k_17_21, k_17_22, k_17_40, k_17_41, k_17_42, k_17_43, k_17_44, k_17_45, k_17_46, k_17_47, k_17_48, k_17_49, k_17_50, k_17_51, k_17_52, k_17_53, k_17_54, k_17_55, k_17_56, k_17_57, k_17_58, k_17_59, k_17_60, k_17_61, k_17_62, k_17_63, k_17_64, k_17_65, k_17_66, k_17_67, k_17_68, k_17_69, k_17_70, k_17_71, k_17_72, k_17_73, k_17_74, k_17_75, k_17_76, k_17_77, k_17_78, k_17_79, k_18_2, k_18_3, k_18_4, k_18_5, k_18_11, k_18_12, k_18_13, k_18_14, k_18_15, k_18_16, k_18_17, k_18_18, k_18_19, k_18_20, k_18_21, k_18_22, k_18_23, k_18_24, k_18_25, k_18_26, k_18_27, k_18_28, k_18_29, k_18_30, k_18_31, k_18_32, k_18_33, k_18_34, k_18_35, k_18_36, k_18_37, k_18_38, k_18_39, k_18_40, k_18_41, k_18_42, k_18_43, k_18_44, k_18_45, k_18_46, k_18_47, k_18_48, k_18_49, k_18_50, k_18_51, k_18_52, k_18_53, k_18_54, k_18_55, k_18_56, k_18_57, k_18_58, k_18_59, k_18_60, k_18_61, k_18_62, k_18_63, k_18_64, k_18_65, k_18_66, k_18_67, k_18_70, k_18_71, k_18_72, k_18_73, k_19_0, k_19_1, k_19_2, k_19_3, k_19_4, k_19_5, k_19_6, k_19_7, k_19_8, k_19_9, k_19_10, k_19_11, k_19_12, k_19_13, k_19_14, k_19_15, k_19_16, k_19_17, k_19_18, k_19_19, k_19_20, k_19_21, k_19_22, k_19_23, k_19_24, k_19_25, k_19_26, k_19_27, k_19_28, k_19_29, k_19_30, k_19_31, k_19_32, k_19_33, k_19_34, k_19_35, k_19_36, k_19_37, k_19_38, k_19_41, k_19_42, k_19_43, k_19_44, k_19_53, k_19_54, k_19_55, k_19_56, k_19_62, k_19_63, k_19_64, k_19_65, k_19_66, k_19_67, k_19_68, k_19_69, k_19_70, k_19_71, k_19_72, k_19_73, k_19_74, k_19_75, k_19_76, k_19_77, k_19_78, k_19_79, k_20_0, k_20_1, k_20_2, k_20_3, k_20_4, k_20_5, k_20_6, k_20_7, k_20_8, k_20_9, k_20_12, k_20_13, k_20_14, k_20_15, k_20_24, k_20_25, k_20_26, k_20_27, k_20_33, k_20_34, k_20_35, k_20_36, k_20_37, k_20_38, k_20_39, k_20_40, k_20_41, k_20_42, k_20_43, k_20_44, k_20_45, k_20_46, k_20_47, k_20_48, k_20_49, k_20_50, k_20_51, k_20_52, k_20_53, k_20_54, k_20_55, k_20_56, k_20_57, k_20_58, k_20_59, k_20_60, k_20_61, k_20_62, k_20_63, k_20_64, k_20_65, k_20_66, k_20_67, k_20_68, k_20_69, k_20_70, k_20_71, k_20_72, k_20_73, k_20_74, k_20_75, k_20_76, k_20_77, k_20_78, k_20_79, k_21_4, k_21_5, k_21_6, k_21_7, k_21_8, k_21_9, k_21_10, k_21_11, k_21_12, k_21_13, k_21_14, k_21_15, k_21_16, k_21_17, k_21_18, k_21_19, k_21_20, k_21_21, k_21_22, k_21_23, k_21_24, k_21_25, k_21_26, k_21_27, k_21_28, k_21_29, k_21_30, k_21_31, k_21_32, k_21_33, k_21_34, k_21_35, k_21_36, k_21_37, k_21_38, k_21_39, k_21_40, k_21_41, k_21_42, k_21_43, k_21_44, k_21_45, k_21_46, k_21_47, k_21_48, k_21_49, k_21_50, k_21_51, k_21_52, k_21_53, k_21_54, k_21_55, k_21_56, k_21_57, k_21_58, k_21_59, k_21_60, k_21_63, k_21_64, k_21_65, k_21_66, k_21_75, k_21_76, k_21_77, k_21_78, k_22_0, k_22_1, k_22_2, k_22_3, k_22_4, k_22_5, k_22_6, k_22_7, k_22_8, k_22_9, k_22_10, k_22_11, k_22_12, k_22_13, k_22_14, k_22_15, k_22_16, k_22_17, k_22_18, k_22_19, k_22_20, k_22_21, k_22_22, k_22_23, k_22_24, k_22_25, k_22_26, k_22_27, k_22_28, k_22_29, k_22_30, k_22_31, k_22_34, k_22_35, k_22_36, k_22_37, k_22_46, k_22_47, k_22_48, k_22_49, k_22_55, k_22_56, k_22_57, k_22_58, k_22_59, k_22_60, k_22_61, k_22_62, k_22_63, k_22_64, k_22_65, k_22_66, k_22_67, k_22_68, k_22_69, k_22_70, k_22_71, k_22_72, k_22_73, k_22_74, k_22_75, k_22_76, k_22_77, k_22_78, k_22_79