Number of relations: 2184
Number of variables: 2160
Number of target variables: 96
Number of known variables: 0
Number of guessed variables: 60
Number of state copies (max_steps): 35
An upper bound for the number of guessed variables given by user (max_guess): 60
1391 out of 2160 state variables are known after 35 state copies
############################################################
The following 60 variable(s) are guessed:
k_0_22, k_2_46, k_4_17, k_4_20, k_4_34, k_6_71, k_7_58, k_8_2, k_9_3, k_9_47, k_11_4, k_12_8, k_12_22, k_13_50, k_13_52, k_13_54, k_14_28, k_14_33, k_16_9, k_16_67, k_16_72, k_17_47, k_18_12, k_18_18, k_18_20, k_18_22, k_18_45, k_18_54, k_18_68, k_19_54, k_19_74, k_20_41, k_20_61, k_20_64, k_20_77, k_21_11, k_21_13, k_22_45, k_23_63, k_23_67, k_24_24, k_24_29, k_24_62, k_25_34, k_25_35, k_25_36, k_25_37, k_25_50, k_26_0, k_26_2, k_26_8, k_26_29, k_26_30, k_26_32, k_26_33, k_26_42, k_26_43, k_26_45, k_26_63, k_26_77
############################################################
The following 0 variable(s) are initially known:

############################################################
Target variables:
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_0_28, k_0_29, k_0_30, k_0_31, k_0_32, k_0_33, k_0_34, k_0_35, k_0_36, k_0_37, k_0_38, k_0_39, k_0_40, k_0_41, k_0_42, k_0_43, k_0_44, k_0_45, k_0_46, k_0_47, k_1_20, k_1_21, k_1_22, k_1_23, k_1_24, k_1_25, k_1_26, k_1_27, k_1_36, k_1_37, k_1_38, k_1_39, k_1_40, k_1_41, k_1_42, k_1_43, k_25_0, k_25_2, k_25_8, k_25_10, k_25_16, k_25_18, k_25_24, k_25_26, k_25_32, k_25_34, k_25_40, k_25_42, k_25_48, k_25_50, k_25_56, k_25_58, k_26_0, k_26_2, k_26_4, k_26_6, k_26_8, k_26_10, k_26_12, k_26_14, k_26_16, k_26_18, k_26_20, k_26_22, k_26_24, k_26_26, k_26_28, k_26_30, k_26_32, k_26_34, k_26_36, k_26_38, k_26_40, k_26_42, k_26_44, k_26_46, k_26_48, k_26_50, k_26_52, k_26_54, k_26_56, k_26_58, k_26_60, k_26_62
############################################################
Determination flow:

State 0:
k_0_22 in symmetric relation [k_0_22, k_1_41] are known: k_0_22 ===> k_1_41
k_2_46 in symmetric relation [k_1_27, k_2_46] are known: k_2_46 ===> k_1_27
k_2_46 in symmetric relation [k_2_46, k_3_65] are known: k_2_46 ===> k_3_65
k_4_17 in symmetric relation [k_3_78, k_4_17] are known: k_4_17 ===> k_3_78
k_4_20 in symmetric relation [k_3_1, k_4_20] are known: k_4_20 ===> k_3_1
k_4_34 in symmetric relation [k_3_15, k_4_34] are known: k_4_34 ===> k_3_15
k_4_17 in symmetric relation [k_4_17, k_5_36] are known: k_4_17 ===> k_5_36
k_4_20 in symmetric relation [k_4_20, k_5_39] are known: k_4_20 ===> k_5_39
k_4_34 in symmetric relation [k_4_34, k_5_53] are known: k_4_34 ===> k_5_53
k_6_71 in symmetric relation [k_5_52, k_6_71] are known: k_6_71 ===> k_5_52
k_6_71 in symmetric relation [k_6_71, k_7_10] are known: k_6_71 ===> k_7_10
k_7_58 in symmetric relation [k_6_39, k_7_58] are known: k_7_58 ===> k_6_39
k_7_58 in symmetric relation [k_7_58, k_8_77] are known: k_7_58 ===> k_8_77
k_8_2 in symmetric relation [k_8_2, k_9_21] are known: k_8_2 ===> k_9_21
k_9_47 in symmetric relation [k_8_28, k_9_47] are known: k_9_47 ===> k_8_28
k_9_3 in symmetric relation [k_9_3, k_10_22] are known: k_9_3 ===> k_10_22
k_9_47 in symmetric relation [k_9_47, k_10_66] are known: k_9_47 ===> k_10_66
k_11_4 in symmetric relation [k_10_65, k_11_4] are known: k_11_4 ===> k_10_65
k_12_8 in symmetric relation [k_11_69, k_12_8] are known: k_12_8 ===> k_11_69
k_12_22 in symmetric relation [k_11_3, k_12_22] are known: k_12_22 ===> k_11_3
k_11_4 in symmetric relation [k_11_4, k_12_23] are known: k_11_4 ===> k_12_23
k_12_8 in symmetric relation [k_12_8, k_13_27] are known: k_12_8 ===> k_13_27
k_12_22 in symmetric relation [k_12_22, k_13_41] are known: k_12_22 ===> k_13_41
k_13_50 in symmetric relation [k_12_31, k_13_50] are known: k_13_50 ===> k_12_31
k_13_52 in symmetric relation [k_12_33, k_13_52] are known: k_13_52 ===> k_12_33
k_13_54 in symmetric relation [k_12_35, k_13_54] are known: k_13_54 ===> k_12_35
k_14_28 in symmetric relation [k_13_9, k_14_28] are known: k_14_28 ===> k_13_9
k_14_33 in symmetric relation [k_13_14, k_14_33] are known: k_14_33 ===> k_13_14
k_13_50 in symmetric relation [k_13_50, k_14_69] are known: k_13_50 ===> k_14_69
k_13_52 in symmetric relation [k_13_52, k_14_71] are known: k_13_52 ===> k_14_71
k_13_54 in symmetric relation [k_13_54, k_14_73] are known: k_13_54 ===> k_14_73
k_14_28 in symmetric relation [k_14_28, k_15_47] are known: k_14_28 ===> k_15_47
k_14_33 in symmetric relation [k_14_33, k_15_52] are known: k_14_33 ===> k_15_52
k_16_9 in symmetric relation [k_15_70, k_16_9] are known: k_16_9 ===> k_15_70
k_16_67 in symmetric relation [k_15_48, k_16_67] are known: k_16_67 ===> k_15_48
k_16_72 in symmetric relation [k_15_53, k_16_72] are known: k_16_72 ===> k_15_53
k_16_67 in symmetric relation [k_16_67, k_17_6] are known: k_16_67 ===> k_17_6
k_16_72 in symmetric relation [k_16_72, k_17_11] are known: k_16_72 ===> k_17_11
k_16_9 in symmetric relation [k_16_9, k_17_28] are known: k_16_9 ===> k_17_28
k_17_47 in symmetric relation [k_16_28, k_17_47] are known: k_17_47 ===> k_16_28
k_18_12 in symmetric relation [k_17_73, k_18_12] are known: k_18_12 ===> k_17_73
k_18_18 in symmetric relation [k_17_79, k_18_18] are known: k_18_18 ===> k_17_79
k_18_20 in symmetric relation [k_17_1, k_18_20] are known: k_18_20 ===> k_17_1
k_18_22 in symmetric relation [k_17_3, k_18_22] are known: k_18_22 ===> k_17_3
k_18_45 in symmetric relation [k_17_26, k_18_45] are known: k_18_45 ===> k_17_26
k_18_54 in symmetric relation [k_17_35, k_18_54] are known: k_18_54 ===> k_17_35
k_17_47 in symmetric relation [k_17_47, k_18_66] are known: k_17_47 ===> k_18_66
k_18_68 in symmetric relation [k_17_49, k_18_68] are known: k_18_68 ===> k_17_49
k_18_68 in symmetric relation [k_18_68, k_19_7] are known: k_18_68 ===> k_19_7
k_18_12 in symmetric relation [k_18_12, k_19_31] are known: k_18_12 ===> k_19_31
k_18_18 in symmetric relation [k_18_18, k_19_37] are known: k_18_18 ===> k_19_37
k_18_20 in symmetric relation [k_18_20, k_19_39] are known: k_18_20 ===> k_19_39
k_18_22 in symmetric relation [k_18_22, k_19_41] are known: k_18_22 ===> k_19_41
k_19_54 in symmetric relation [k_18_35, k_19_54] are known: k_19_54 ===> k_18_35
k_18_45 in symmetric relation [k_18_45, k_19_64] are known: k_18_45 ===> k_19_64
k_18_54 in symmetric relation [k_18_54, k_19_73] are known: k_18_54 ===> k_19_73
k_19_74 in symmetric relation [k_18_55, k_19_74] are known: k_19_74 ===> k_18_55
k_19_74 in symmetric relation [k_19_74, k_20_13] are known: k_19_74 ===> k_20_13
k_20_41 in symmetric relation [k_19_22, k_20_41] are known: k_20_41 ===> k_19_22
k_20_61 in symmetric relation [k_19_42, k_20_61] are known: k_20_61 ===> k_19_42
k_20_64 in symmetric relation [k_19_45, k_20_64] are known: k_20_64 ===> k_19_45
k_19_54 in symmetric relation [k_19_54, k_20_73] are known: k_19_54 ===> k_20_73
k_20_77 in symmetric relation [k_19_58, k_20_77] are known: k_20_77 ===> k_19_58
k_21_11 in symmetric relation [k_20_72, k_21_11] are known: k_21_11 ===> k_20_72
k_21_13 in symmetric relation [k_20_74, k_21_13] are known: k_21_13 ===> k_20_74
k_20_77 in symmetric relation [k_20_77, k_21_16] are known: k_20_77 ===> k_21_16
k_20_41 in symmetric relation [k_20_41, k_21_60] are known: k_20_41 ===> k_21_60
k_21_11 in symmetric relation [k_21_11, k_22_30] are known: k_21_11 ===> k_22_30
k_21_13 in symmetric relation [k_21_13, k_22_32] are known: k_21_13 ===> k_22_32
k_22_45 in symmetric relation [k_21_26, k_22_45] are known: k_22_45 ===> k_21_26
k_23_63 in symmetric relation [k_22_44, k_23_63] are known: k_23_63 ===> k_22_44
k_22_45 in symmetric relation [k_22_45, k_23_64] are known: k_22_45 ===> k_23_64
k_23_67 in symmetric relation [k_22_48, k_23_67] are known: k_23_67 ===> k_22_48
k_23_67 in symmetric relation [k_23_67, k_24_6] are known: k_23_67 ===> k_24_6
k_24_24 in symmetric relation [k_23_5, k_24_24] are known: k_24_24 ===> k_23_5
k_24_29 in symmetric relation [k_23_10, k_24_29] are known: k_24_29 ===> k_23_10
k_24_62 in symmetric relation [k_23_43, k_24_62] are known: k_24_62 ===> k_23_43
k_25_34 in symmetric relation [k_24_15, k_25_34] are known: k_25_34 ===> k_24_15
k_25_35 in symmetric relation [k_24_16, k_25_35] are known: k_25_35 ===> k_24_16
k_25_36 in symmetric relation [k_24_17, k_25_36] are known: k_25_36 ===> k_24_17
k_25_37 in symmetric relation [k_24_18, k_25_37] are known: k_25_37 ===> k_24_18
k_24_24 in symmetric relation [k_24_24, k_25_43] are known: k_24_24 ===> k_25_43
k_24_29 in symmetric relation [k_24_29, k_25_48] are known: k_24_29 ===> k_25_48
k_25_50 in symmetric relation [k_24_31, k_25_50] are known: k_25_50 ===> k_24_31
k_26_8 in symmetric relation [k_25_69, k_26_8] are known: k_26_8 ===> k_25_69
k_26_29 in symmetric relation [k_25_10, k_26_29] are known: k_26_29 ===> k_25_10
k_26_30 in symmetric relation [k_25_11, k_26_30] are known: k_26_30 ===> k_25_11
k_26_32 in symmetric relation [k_25_13, k_26_32] are known: k_26_32 ===> k_25_13
k_26_33 in symmetric relation [k_25_14, k_26_33] are known: k_26_33 ===> k_25_14
k_26_42 in symmetric relation [k_25_23, k_26_42] are known: k_26_42 ===> k_25_23
k_26_43 in symmetric relation [k_25_24, k_26_43] are known: k_26_43 ===> k_25_24
k_26_45 in symmetric relation [k_25_26, k_26_45] are known: k_26_45 ===> k_25_26
k_25_34 in symmetric relation [k_25_34, k_26_53] are known: k_25_34 ===> k_26_53
k_25_35 in symmetric relation [k_25_35, k_26_54] are known: k_25_35 ===> k_26_54
k_25_36 in symmetric relation [k_25_36, k_26_55] are known: k_25_36 ===> k_26_55
k_25_37 in symmetric relation [k_25_37, k_26_56] are known: k_25_37 ===> k_26_56
k_26_63 in symmetric relation [k_25_44, k_26_63] are known: k_26_63 ===> k_25_44
k_25_50 in symmetric relation [k_25_50, k_26_69] are known: k_25_50 ===> k_26_69
k_26_77 in symmetric relation [k_25_58, k_26_77] are known: k_26_77 ===> k_25_58
############################################################
State 1:
k_1_27 in symmetric relation [k_0_8, k_1_27] are known: k_1_27 ===> k_0_8
k_1_41 in symmetric relation [k_1_41, k_2_60] are known: k_1_41 ===> k_2_60
k_3_15 in symmetric relation [k_2_76, k_3_15] are known: k_3_15 ===> k_2_76
k_3_78 in symmetric relation [k_2_59, k_3_78] are known: k_3_78 ===> k_2_59
k_3_65 in symmetric relation [k_3_65, k_4_4] are known: k_3_65 ===> k_4_4
k_5_52 in symmetric relation [k_4_33, k_5_52] are known: k_5_52 ===> k_4_33
k_6_39 in symmetric relation [k_5_20, k_6_39] are known: k_6_39 ===> k_5_20
k_5_36 in symmetric relation [k_5_36, k_6_55] are known: k_5_36 ===> k_6_55
k_5_39 in symmetric relation [k_5_39, k_6_58] are known: k_5_39 ===> k_6_58
k_5_53 in symmetric relation [k_5_53, k_6_72] are known: k_5_53 ===> k_6_72
k_8_28 in symmetric relation [k_7_9, k_8_28] are known: k_8_28 ===> k_7_9
k_7_10 in symmetric relation [k_7_10, k_8_29] are known: k_7_10 ===> k_8_29
k_8_77 in symmetric relation [k_8_77, k_9_16] are known: k_8_77 ===> k_9_16
k_9_21 in symmetric relation [k_9_21, k_10_40] are known: k_9_21 ===> k_10_40
k_10_65 in symmetric relation [k_9_46, k_10_65] are known: k_10_65 ===> k_9_46
k_10_66 in symmetric relation [k_10_66, k_11_5] are known: k_10_66 ===> k_11_5
k_10_22 in symmetric relation [k_10_22, k_11_41] are known: k_10_22 ===> k_11_41
k_11_69 in symmetric relation [k_10_50, k_11_69] are known: k_11_69 ===> k_10_50
k_12_31 in symmetric relation [k_11_12, k_12_31] are known: k_12_31 ===> k_11_12
k_12_33 in symmetric relation [k_11_14, k_12_33] are known: k_12_33 ===> k_11_14
k_12_35 in symmetric relation [k_11_16, k_12_35] are known: k_12_35 ===> k_11_16
k_13_9 in symmetric relation [k_12_70, k_13_9] are known: k_13_9 ===> k_12_70
k_13_14 in symmetric relation [k_12_75, k_13_14] are known: k_13_14 ===> k_12_75
k_12_23 in symmetric relation [k_12_23, k_13_42] are known: k_12_23 ===> k_13_42
k_13_27 in symmetric relation [k_13_27, k_14_46] are known: k_13_27 ===> k_14_46
k_13_41 in symmetric relation [k_13_41, k_14_60] are known: k_13_41 ===> k_14_60
k_14_69 in symmetric relation [k_14_69, k_15_8] are known: k_14_69 ===> k_15_8
k_14_71 in symmetric relation [k_14_71, k_15_10] are known: k_14_71 ===> k_15_10
k_14_73 in symmetric relation [k_14_73, k_15_12] are known: k_14_73 ===> k_15_12
k_15_48 in symmetric relation [k_14_29, k_15_48] are known: k_15_48 ===> k_14_29
k_15_53 in symmetric relation [k_14_34, k_15_53] are known: k_15_53 ===> k_14_34
k_15_70 in symmetric relation [k_14_51, k_15_70] are known: k_15_70 ===> k_14_51
k_16_28 in symmetric relation [k_15_9, k_16_28] are known: k_16_28 ===> k_15_9
k_15_47 in symmetric relation [k_15_47, k_16_66] are known: k_15_47 ===> k_16_66
k_15_52 in symmetric relation [k_15_52, k_16_71] are known: k_15_52 ===> k_16_71
k_17_26 in symmetric relation [k_16_7, k_17_26] are known: k_17_26 ===> k_16_7
k_17_35 in symmetric relation [k_16_16, k_17_35] are known: k_17_35 ===> k_16_16
k_17_49 in symmetric relation [k_16_30, k_17_49] are known: k_17_49 ===> k_16_30
k_17_73 in symmetric relation [k_16_54, k_17_73] are known: k_17_73 ===> k_16_54
k_17_79 in symmetric relation [k_16_60, k_17_79] are known: k_17_79 ===> k_16_60
k_17_6 in symmetric relation [k_17_6, k_18_25] are known: k_17_6 ===> k_18_25
k_17_11 in symmetric relation [k_17_11, k_18_30] are known: k_17_11 ===> k_18_30
k_18_35 in symmetric relation [k_17_16, k_18_35] are known: k_18_35 ===> k_17_16
k_17_28 in symmetric relation [k_17_28, k_18_47] are known: k_17_28 ===> k_18_47
k_18_55 in symmetric relation [k_17_36, k_18_55] are known: k_18_55 ===> k_17_36
k_18_66 in symmetric relation [k_18_66, k_19_5] are known: k_18_66 ===> k_19_5
k_19_22 in symmetric relation [k_18_3, k_19_22] are known: k_19_22 ===> k_18_3
k_19_42 in symmetric relation [k_18_23, k_19_42] are known: k_19_42 ===> k_18_23
k_19_45 in symmetric relation [k_18_26, k_19_45] are known: k_19_45 ===> k_18_26
k_19_58 in symmetric relation [k_18_39, k_19_58] are known: k_19_58 ===> k_18_39
k_19_73 in symmetric relation [k_19_73, k_20_12] are known: k_19_73 ===> k_20_12
k_19_7 in symmetric relation [k_19_7, k_20_26] are known: k_19_7 ===> k_20_26
k_19_31 in symmetric relation [k_19_31, k_20_50] are known: k_19_31 ===> k_20_50
k_19_37 in symmetric relation [k_19_37, k_20_56] are known: k_19_37 ===> k_20_56
k_19_39 in symmetric relation [k_19_39, k_20_58] are known: k_19_39 ===> k_20_58
k_19_41 in symmetric relation [k_19_41, k_20_60] are known: k_19_41 ===> k_20_60
k_20_72 in symmetric relation [k_19_53, k_20_72] are known: k_20_72 ===> k_19_53
k_20_74 in symmetric relation [k_19_55, k_20_74] are known: k_20_74 ===> k_19_55
k_20_73 in symmetric relation [k_20_73, k_21_12] are known: k_20_73 ===> k_21_12
k_21_26 in symmetric relation [k_20_7, k_21_26] are known: k_21_26 ===> k_20_7
k_20_13 in symmetric relation [k_20_13, k_21_32] are known: k_20_13 ===> k_21_32
k_21_16 in symmetric relation [k_21_16, k_22_35] are known: k_21_16 ===> k_22_35
k_22_44 in symmetric relation [k_21_25, k_22_44] are known: k_22_44 ===> k_21_25
k_22_48 in symmetric relation [k_21_29, k_22_48] are known: k_22_48 ===> k_21_29
k_21_60 in symmetric relation [k_21_60, k_22_79] are known: k_21_60 ===> k_22_79
k_23_5 in symmetric relation [k_22_66, k_23_5] are known: k_23_5 ===> k_22_66
k_23_10 in symmetric relation [k_22_71, k_23_10] are known: k_23_10 ===> k_22_71
k_23_43 in symmetric relation [k_22_24, k_23_43] are known: k_23_43 ===> k_22_24
k_22_30 in symmetric relation [k_22_30, k_23_49] are known: k_22_30 ===> k_23_49
k_22_32 in symmetric relation [k_22_32, k_23_51] are known: k_22_32 ===> k_23_51
k_24_15 in symmetric relation [k_23_76, k_24_15] are known: k_24_15 ===> k_23_76
k_24_16 in symmetric relation [k_23_77, k_24_16] are known: k_24_16 ===> k_23_77
k_24_17 in symmetric relation [k_23_78, k_24_17] are known: k_24_17 ===> k_23_78
k_24_18 in symmetric relation [k_23_79, k_24_18] are known: k_24_18 ===> k_23_79
k_24_31 in symmetric relation [k_23_12, k_24_31] are known: k_24_31 ===> k_23_12
k_25_10 in symmetric relation [k_24_71, k_25_10] are known: k_25_10 ===> k_24_71
k_25_11 in symmetric relation [k_24_72, k_25_11] are known: k_25_11 ===> k_24_72
k_25_13 in symmetric relation [k_24_74, k_25_13] are known: k_25_13 ===> k_24_74
k_25_14 in symmetric relation [k_24_75, k_25_14] are known: k_25_14 ===> k_24_75
k_25_23 in symmetric relation [k_24_4, k_25_23] are known: k_25_23 ===> k_24_4
k_25_24 in symmetric relation [k_24_5, k_25_24] are known: k_25_24 ===> k_24_5
k_24_6 in symmetric relation [k_24_6, k_25_25] are known: k_24_6 ===> k_25_25
k_25_26 in symmetric relation [k_24_7, k_25_26] are known: k_25_26 ===> k_24_7
k_25_44 in symmetric relation [k_24_25, k_25_44] are known: k_25_44 ===> k_24_25
k_25_58 in symmetric relation [k_24_39, k_25_58] are known: k_25_58 ===> k_24_39
k_25_69 in symmetric relation [k_24_50, k_25_69] are known: k_25_69 ===> k_24_50
k_25_43 in symmetric relation [k_25_43, k_26_62] are known: k_25_43 ===> k_26_62
k_25_48 in symmetric relation [k_25_48, k_26_67] are known: k_25_48 ===> k_26_67
############################################################
State 2:
k_2_59 in symmetric relation [k_1_40, k_2_59] are known: k_2_59 ===> k_1_40
k_2_76 in symmetric relation [k_1_57, k_2_76] are known: k_2_76 ===> k_1_57
k_2_60 in symmetric relation [k_2_60, k_3_79] are known: k_2_60 ===> k_3_79
k_4_33 in symmetric relation [k_3_14, k_4_33] are known: k_4_33 ===> k_3_14
k_5_20 in symmetric relation [k_4_1, k_5_20] are known: k_5_20 ===> k_4_1
k_4_4 in symmetric relation [k_4_4, k_5_23] are known: k_4_4 ===> k_5_23
k_7_9 in symmetric relation [k_6_70, k_7_9] are known: k_7_9 ===> k_6_70
k_6_72 in symmetric relation [k_6_72, k_7_11] are known: k_6_72 ===> k_7_11
k_6_55 in symmetric relation [k_6_55, k_7_74] are known: k_6_55 ===> k_7_74
k_6_58 in symmetric relation [k_6_58, k_7_77] are known: k_6_58 ===> k_7_77
k_9_46 in symmetric relation [k_8_27, k_9_46] are known: k_9_46 ===> k_8_27
k_8_29 in symmetric relation [k_8_29, k_9_48] are known: k_8_29 ===> k_9_48
k_9_16 in symmetric relation [k_9_16, k_10_35] are known: k_9_16 ===> k_10_35
k_10_50 in symmetric relation [k_9_31, k_10_50] are known: k_10_50 ===> k_9_31
k_11_12 in symmetric relation [k_10_73, k_11_12] are known: k_11_12 ===> k_10_73
k_11_14 in symmetric relation [k_10_75, k_11_14] are known: k_11_14 ===> k_10_75
k_11_16 in symmetric relation [k_10_77, k_11_16] are known: k_11_16 ===> k_10_77
k_10_40 in symmetric relation [k_10_40, k_11_59] are known: k_10_40 ===> k_11_59
k_11_5 in symmetric relation [k_11_5, k_12_24] are known: k_11_5 ===> k_12_24
k_11_41 in symmetric relation [k_11_41, k_12_60] are known: k_11_41 ===> k_12_60
k_12_70 in symmetric relation [k_11_51, k_12_70] are known: k_12_70 ===> k_11_51
k_12_75 in symmetric relation [k_11_56, k_12_75] are known: k_12_75 ===> k_11_56
k_14_29 in symmetric relation [k_13_10, k_14_29] are known: k_14_29 ===> k_13_10
k_14_34 in symmetric relation [k_13_15, k_14_34] are known: k_14_34 ===> k_13_15
k_14_51 in symmetric relation [k_13_32, k_14_51] are known: k_14_51 ===> k_13_32
k_13_42 in symmetric relation [k_13_42, k_14_61] are known: k_13_42 ===> k_14_61
k_15_9 in symmetric relation [k_14_70, k_15_9] are known: k_15_9 ===> k_14_70
k_14_46 in symmetric relation [k_14_46, k_15_65] are known: k_14_46 ===> k_15_65
k_14_60 in symmetric relation [k_14_60, k_15_79] are known: k_14_60 ===> k_15_79
k_16_7 in symmetric relation [k_15_68, k_16_7] are known: k_16_7 ===> k_15_68
k_16_16 in symmetric relation [k_15_77, k_16_16] are known: k_16_16 ===> k_15_77
k_15_8 in symmetric relation [k_15_8, k_16_27] are known: k_15_8 ===> k_16_27
k_15_10 in symmetric relation [k_15_10, k_16_29] are known: k_15_10 ===> k_16_29
k_16_30 in symmetric relation [k_15_11, k_16_30] are known: k_16_30 ===> k_15_11
k_15_12 in symmetric relation [k_15_12, k_16_31] are known: k_15_12 ===> k_16_31
k_16_54 in symmetric relation [k_15_35, k_16_54] are known: k_16_54 ===> k_15_35
k_16_60 in symmetric relation [k_15_41, k_16_60] are known: k_16_60 ===> k_15_41
k_16_66 in symmetric relation [k_16_66, k_17_5] are known: k_16_66 ===> k_17_5
k_16_71 in symmetric relation [k_16_71, k_17_10] are known: k_16_71 ===> k_17_10
k_17_16 in symmetric relation [k_16_77, k_17_16] are known: k_17_16 ===> k_16_77
k_17_36 in symmetric relation [k_16_17, k_17_36] are known: k_17_36 ===> k_16_17
k_18_23 in symmetric relation [k_17_4, k_18_23] are known: k_18_23 ===> k_17_4
k_18_26 in symmetric relation [k_17_7, k_18_26] are known: k_18_26 ===> k_17_7
k_18_39 in symmetric relation [k_17_20, k_18_39] are known: k_18_39 ===> k_17_20
k_18_25 in symmetric relation [k_18_25, k_19_44] are known: k_18_25 ===> k_19_44
k_18_30 in symmetric relation [k_18_30, k_19_49] are known: k_18_30 ===> k_19_49
k_19_53 in symmetric relation [k_18_34, k_19_53] are known: k_19_53 ===> k_18_34
k_19_55 in symmetric relation [k_18_36, k_19_55] are known: k_19_55 ===> k_18_36
k_18_47 in symmetric relation [k_18_47, k_19_66] are known: k_18_47 ===> k_19_66
k_20_7 in symmetric relation [k_19_68, k_20_7] are known: k_20_7 ===> k_19_68
k_19_5 in symmetric relation [k_19_5, k_20_24] are known: k_19_5 ===> k_20_24
k_21_25 in symmetric relation [k_20_6, k_21_25] are known: k_21_25 ===> k_20_6
k_21_29 in symmetric relation [k_20_10, k_21_29] are known: k_21_29 ===> k_20_10
k_20_12 in symmetric relation [k_20_12, k_21_31] are known: k_20_12 ===> k_21_31
k_20_26 in symmetric relation [k_20_26, k_21_45] are known: k_20_26 ===> k_21_45
k_20_50 in symmetric relation [k_20_50, k_21_69] are known: k_20_50 ===> k_21_69
k_20_56 in symmetric relation [k_20_56, k_21_75] are known: k_20_56 ===> k_21_75
k_20_58 in symmetric relation [k_20_58, k_21_77] are known: k_20_58 ===> k_21_77
k_20_60 in symmetric relation [k_20_60, k_21_79] are known: k_20_60 ===> k_21_79
k_22_24 in symmetric relation [k_21_5, k_22_24] are known: k_22_24 ===> k_21_5
k_21_12 in symmetric relation [k_21_12, k_22_31] are known: k_21_12 ===> k_22_31
k_21_32 in symmetric relation [k_21_32, k_22_51] are known: k_21_32 ===> k_22_51
k_22_66 in symmetric relation [k_21_47, k_22_66] are known: k_22_66 ===> k_21_47
k_22_71 in symmetric relation [k_21_52, k_22_71] are known: k_22_71 ===> k_21_52
k_23_12 in symmetric relation [k_22_73, k_23_12] are known: k_23_12 ===> k_22_73
k_22_79 in symmetric relation [k_22_79, k_23_18] are known: k_22_79 ===> k_23_18
k_22_35 in symmetric relation [k_22_35, k_23_54] are known: k_22_35 ===> k_23_54
k_23_76 in symmetric relation [k_22_57, k_23_76] are known: k_23_76 ===> k_22_57
k_23_77 in symmetric relation [k_22_58, k_23_77] are known: k_23_77 ===> k_22_58
k_23_78 in symmetric relation [k_22_59, k_23_78] are known: k_23_78 ===> k_22_59
k_23_79 in symmetric relation [k_22_60, k_23_79] are known: k_23_79 ===> k_22_60
k_24_4 in symmetric relation [k_23_65, k_24_4] are known: k_24_4 ===> k_23_65
k_24_5 in symmetric relation [k_23_66, k_24_5] are known: k_24_5 ===> k_23_66
k_24_7 in symmetric relation [k_23_68, k_24_7] are known: k_24_7 ===> k_23_68
k_24_25 in symmetric relation [k_23_6, k_24_25] are known: k_24_25 ===> k_23_6
k_24_39 in symmetric relation [k_23_20, k_24_39] are known: k_24_39 ===> k_23_20
k_24_50 in symmetric relation [k_23_31, k_24_50] are known: k_24_50 ===> k_23_31
k_23_49 in symmetric relation [k_23_49, k_24_68] are known: k_23_49 ===> k_24_68
k_23_51 in symmetric relation [k_23_51, k_24_70] are known: k_23_51 ===> k_24_70
k_24_71 in symmetric relation [k_23_52, k_24_71] are known: k_24_71 ===> k_23_52
k_24_72 in symmetric relation [k_23_53, k_24_72] are known: k_24_72 ===> k_23_53
k_24_74 in symmetric relation [k_23_55, k_24_74] are known: k_24_74 ===> k_23_55
k_24_75 in symmetric relation [k_23_56, k_24_75] are known: k_24_75 ===> k_23_56
k_25_25 in symmetric relation [k_25_25, k_26_44] are known: k_25_25 ===> k_26_44
############################################################
State 3:
k_1_40 in symmetric relation [k_0_21, k_1_40] are known: k_1_40 ===> k_0_21
k_1_57 in symmetric relation [k_0_38, k_1_57] are known: k_1_57 ===> k_0_38
k_3_14 in symmetric relation [k_2_75, k_3_14] are known: k_3_14 ===> k_2_75
k_3_79 in symmetric relation [k_3_79, k_4_18] are known: k_3_79 ===> k_4_18
k_5_23 in symmetric relation [k_5_23, k_6_42] are known: k_5_23 ===> k_6_42
k_6_70 in symmetric relation [k_5_51, k_6_70] are known: k_6_70 ===> k_5_51
k_7_74 in symmetric relation [k_7_74, k_8_13] are known: k_7_74 ===> k_8_13
k_7_77 in symmetric relation [k_7_77, k_8_16] are known: k_7_77 ===> k_8_16
k_8_27 in symmetric relation [k_7_8, k_8_27] are known: k_8_27 ===> k_7_8
k_7_11 in symmetric relation [k_7_11, k_8_30] are known: k_7_11 ===> k_8_30
k_9_31 in symmetric relation [k_8_12, k_9_31] are known: k_9_31 ===> k_8_12
k_9_48 in symmetric relation [k_9_48, k_10_67] are known: k_9_48 ===> k_10_67
k_10_73 in symmetric relation [k_9_54, k_10_73] are known: k_10_73 ===> k_9_54
k_10_75 in symmetric relation [k_9_56, k_10_75] are known: k_10_75 ===> k_9_56
k_10_77 in symmetric relation [k_9_58, k_10_77] are known: k_10_77 ===> k_9_58
k_11_51 in symmetric relation [k_10_32, k_11_51] are known: k_11_51 ===> k_10_32
k_10_35 in symmetric relation [k_10_35, k_11_54] are known: k_10_35 ===> k_11_54
k_11_56 in symmetric relation [k_10_37, k_11_56] are known: k_11_56 ===> k_10_37
k_11_59 in symmetric relation [k_11_59, k_12_78] are known: k_11_59 ===> k_12_78
k_13_10 in symmetric relation [k_12_71, k_13_10] are known: k_13_10 ===> k_12_71
k_13_15 in symmetric relation [k_12_76, k_13_15] are known: k_13_15 ===> k_12_76
k_13_32 in symmetric relation [k_12_13, k_13_32] are known: k_13_32 ===> k_12_13
k_12_24 in symmetric relation [k_12_24, k_13_43] are known: k_12_24 ===> k_13_43
k_12_60 in symmetric relation [k_12_60, k_13_79] are known: k_12_60 ===> k_13_79
k_14_70 in symmetric relation [k_13_51, k_14_70] are known: k_14_70 ===> k_13_51
k_15_11 in symmetric relation [k_14_72, k_15_11] are known: k_15_11 ===> k_14_72
k_15_35 in symmetric relation [k_14_16, k_15_35] are known: k_15_35 ===> k_14_16
k_15_41 in symmetric relation [k_14_22, k_15_41] are known: k_15_41 ===> k_14_22
k_15_68 in symmetric relation [k_14_49, k_15_68] are known: k_15_68 ===> k_14_49
k_15_77 in symmetric relation [k_14_58, k_15_77] are known: k_15_77 ===> k_14_58
k_15_65 in symmetric relation [k_15_65, k_16_4] are known: k_15_65 ===> k_16_4
k_16_17 in symmetric relation [k_15_78, k_16_17] are known: k_16_17 ===> k_15_78
k_15_79 in symmetric relation [k_15_79, k_16_18] are known: k_15_79 ===> k_16_18
k_16_77 in symmetric relation [k_15_58, k_16_77] are known: k_16_77 ===> k_15_58
k_17_4 in symmetric relation [k_16_65, k_17_4] are known: k_17_4 ===> k_16_65
k_17_7 in symmetric relation [k_16_68, k_17_7] are known: k_17_7 ===> k_16_68
k_17_20 in symmetric relation [k_16_1, k_17_20] are known: k_17_20 ===> k_16_1
k_16_27 in symmetric relation [k_16_27, k_17_46] are known: k_16_27 ===> k_17_46
k_16_29 in symmetric relation [k_16_29, k_17_48] are known: k_16_29 ===> k_17_48
k_16_31 in symmetric relation [k_16_31, k_17_50] are known: k_16_31 ===> k_17_50
k_17_5 in symmetric relation [k_17_5, k_18_24] are known: k_17_5 ===> k_18_24
k_17_10 in symmetric relation [k_17_10, k_18_29] are known: k_17_10 ===> k_18_29
k_18_34 in symmetric relation [k_17_15, k_18_34] are known: k_18_34 ===> k_17_15
k_18_36 in symmetric relation [k_17_17, k_18_36] are known: k_18_36 ===> k_17_17
k_19_68 in symmetric relation [k_18_49, k_19_68] are known: k_19_68 ===> k_18_49
k_19_66 in symmetric relation [k_19_66, k_20_5] are known: k_19_66 ===> k_20_5
k_20_6 in symmetric relation [k_19_67, k_20_6] are known: k_20_6 ===> k_19_67
k_20_10 in symmetric relation [k_19_71, k_20_10] are known: k_20_10 ===> k_19_71
k_19_44 in symmetric relation [k_19_44, k_20_63] are known: k_19_44 ===> k_20_63
k_19_49 in symmetric relation [k_19_49, k_20_68] are known: k_19_49 ===> k_20_68
k_21_5 in symmetric relation [k_20_66, k_21_5] are known: k_21_5 ===> k_20_66
k_20_24 in symmetric relation [k_20_24, k_21_43] are known: k_20_24 ===> k_21_43
k_21_47 in symmetric relation [k_20_28, k_21_47] are known: k_21_47 ===> k_20_28
k_21_52 in symmetric relation [k_20_33, k_21_52] are known: k_21_52 ===> k_20_33
k_21_69 in symmetric relation [k_21_69, k_22_8] are known: k_21_69 ===> k_22_8
k_21_75 in symmetric relation [k_21_75, k_22_14] are known: k_21_75 ===> k_22_14
k_21_77 in symmetric relation [k_21_77, k_22_16] are known: k_21_77 ===> k_22_16
k_21_79 in symmetric relation [k_21_79, k_22_18] are known: k_21_79 ===> k_22_18
k_21_31 in symmetric relation [k_21_31, k_22_50] are known: k_21_31 ===> k_22_50
k_22_57 in symmetric relation [k_21_38, k_22_57] are known: k_22_57 ===> k_21_38
k_22_58 in symmetric relation [k_21_39, k_22_58] are known: k_22_58 ===> k_21_39
k_22_59 in symmetric relation [k_21_40, k_22_59] are known: k_22_59 ===> k_21_40
k_22_60 in symmetric relation [k_21_41, k_22_60] are known: k_22_60 ===> k_21_41
k_21_45 in symmetric relation [k_21_45, k_22_64] are known: k_21_45 ===> k_22_64
k_22_73 in symmetric relation [k_21_54, k_22_73] are known: k_22_73 ===> k_21_54
k_23_6 in symmetric relation [k_22_67, k_23_6] are known: k_23_6 ===> k_22_67
k_23_20 in symmetric relation [k_22_1, k_23_20] are known: k_23_20 ===> k_22_1
k_23_31 in symmetric relation [k_22_12, k_23_31] are known: k_23_31 ===> k_22_12
k_22_31 in symmetric relation [k_22_31, k_23_50] are known: k_22_31 ===> k_23_50
k_23_52 in symmetric relation [k_22_33, k_23_52] are known: k_23_52 ===> k_22_33
k_23_53 in symmetric relation [k_22_34, k_23_53] are known: k_23_53 ===> k_22_34
k_23_55 in symmetric relation [k_22_36, k_23_55] are known: k_23_55 ===> k_22_36
k_23_56 in symmetric relation [k_22_37, k_23_56] are known: k_23_56 ===> k_22_37
k_23_65 in symmetric relation [k_22_46, k_23_65] are known: k_23_65 ===> k_22_46
k_23_66 in symmetric relation [k_22_47, k_23_66] are known: k_23_66 ===> k_22_47
k_23_68 in symmetric relation [k_22_49, k_23_68] are known: k_23_68 ===> k_22_49
k_22_51 in symmetric relation [k_22_51, k_23_70] are known: k_22_51 ===> k_23_70
k_23_18 in symmetric relation [k_23_18, k_24_37] are known: k_23_18 ===> k_24_37
k_23_54 in symmetric relation [k_23_54, k_24_73] are known: k_23_54 ===> k_24_73
k_24_68 in symmetric relation [k_24_68, k_25_7] are known: k_24_68 ===> k_25_7
k_24_70 in symmetric relation [k_24_70, k_25_9] are known: k_24_70 ===> k_25_9
############################################################
State 4:
k_2_75 in symmetric relation [k_1_56, k_2_75] are known: k_2_75 ===> k_1_56
k_4_18 in symmetric relation [k_4_18, k_5_37] are known: k_4_18 ===> k_5_37
k_5_51 in symmetric relation [k_4_32, k_5_51] are known: k_5_51 ===> k_4_32
k_7_8 in symmetric relation [k_6_69, k_7_8] are known: k_7_8 ===> k_6_69
k_6_42 in symmetric relation [k_6_42, k_7_61] are known: k_6_42 ===> k_7_61
k_8_12 in symmetric relation [k_7_73, k_8_12] are known: k_8_12 ===> k_7_73
k_8_13 in symmetric relation [k_8_13, k_9_32] are known: k_8_13 ===> k_9_32
k_8_16 in symmetric relation [k_8_16, k_9_35] are known: k_8_16 ===> k_9_35
k_8_30 in symmetric relation [k_8_30, k_9_49] are known: k_8_30 ===> k_9_49
k_9_54 in symmetric relation [k_8_35, k_9_54] are known: k_9_54 ===> k_8_35
k_9_56 in symmetric relation [k_8_37, k_9_56] are known: k_9_56 ===> k_8_37
k_9_58 in symmetric relation [k_8_39, k_9_58] are known: k_9_58 ===> k_8_39
k_10_32 in symmetric relation [k_9_13, k_10_32] are known: k_10_32 ===> k_9_13
k_10_37 in symmetric relation [k_9_18, k_10_37] are known: k_10_37 ===> k_9_18
k_10_67 in symmetric relation [k_10_67, k_11_6] are known: k_10_67 ===> k_11_6
k_12_13 in symmetric relation [k_11_74, k_12_13] are known: k_12_13 ===> k_11_74
k_12_71 in symmetric relation [k_11_52, k_12_71] are known: k_12_71 ===> k_11_52
k_11_54 in symmetric relation [k_11_54, k_12_73] are known: k_11_54 ===> k_12_73
k_12_76 in symmetric relation [k_11_57, k_12_76] are known: k_12_76 ===> k_11_57
k_12_78 in symmetric relation [k_12_78, k_13_17] are known: k_12_78 ===> k_13_17
k_13_51 in symmetric relation [k_12_32, k_13_51] are known: k_13_51 ===> k_12_32
k_14_16 in symmetric relation [k_13_77, k_14_16] are known: k_14_16 ===> k_13_77
k_13_79 in symmetric relation [k_13_79, k_14_18] are known: k_13_79 ===> k_14_18
k_14_22 in symmetric relation [k_13_3, k_14_22] are known: k_14_22 ===> k_13_3
k_14_49 in symmetric relation [k_13_30, k_14_49] are known: k_14_49 ===> k_13_30
k_14_58 in symmetric relation [k_13_39, k_14_58] are known: k_14_58 ===> k_13_39
k_13_43 in symmetric relation [k_13_43, k_14_62] are known: k_13_43 ===> k_14_62
k_14_72 in symmetric relation [k_13_53, k_14_72] are known: k_14_72 ===> k_13_53
k_15_58 in symmetric relation [k_14_39, k_15_58] are known: k_15_58 ===> k_14_39
k_15_78 in symmetric relation [k_14_59, k_15_78] are known: k_15_78 ===> k_14_59
k_16_65 in symmetric relation [k_15_46, k_16_65] are known: k_16_65 ===> k_15_46
k_16_68 in symmetric relation [k_15_49, k_16_68] are known: k_16_68 ===> k_15_49
k_17_15 in symmetric relation [k_16_76, k_17_15] are known: k_17_15 ===> k_16_76
k_17_17 in symmetric relation [k_16_78, k_17_17] are known: k_17_17 ===> k_16_78
k_16_4 in symmetric relation [k_16_4, k_17_23] are known: k_16_4 ===> k_17_23
k_16_18 in symmetric relation [k_16_18, k_17_37] are known: k_16_18 ===> k_17_37
k_18_49 in symmetric relation [k_17_30, k_18_49] are known: k_18_49 ===> k_17_30
k_17_46 in symmetric relation [k_17_46, k_18_65] are known: k_17_46 ===> k_18_65
k_17_48 in symmetric relation [k_17_48, k_18_67] are known: k_17_48 ===> k_18_67
k_17_50 in symmetric relation [k_17_50, k_18_69] are known: k_17_50 ===> k_18_69
k_18_24 in symmetric relation [k_18_24, k_19_43] are known: k_18_24 ===> k_19_43
k_18_29 in symmetric relation [k_18_29, k_19_48] are known: k_18_29 ===> k_19_48
k_19_67 in symmetric relation [k_18_48, k_19_67] are known: k_19_67 ===> k_18_48
k_19_71 in symmetric relation [k_18_52, k_19_71] are known: k_19_71 ===> k_18_52
k_20_28 in symmetric relation [k_19_9, k_20_28] are known: k_20_28 ===> k_19_9
k_20_33 in symmetric relation [k_19_14, k_20_33] are known: k_20_33 ===> k_19_14
k_20_66 in symmetric relation [k_19_47, k_20_66] are known: k_20_66 ===> k_19_47
k_20_68 in symmetric relation [k_20_68, k_21_7] are known: k_20_68 ===> k_21_7
k_20_5 in symmetric relation [k_20_5, k_21_24] are known: k_20_5 ===> k_21_24
k_21_38 in symmetric relation [k_20_19, k_21_38] are known: k_21_38 ===> k_20_19
k_21_39 in symmetric relation [k_20_20, k_21_39] are known: k_21_39 ===> k_20_20
k_21_40 in symmetric relation [k_20_21, k_21_40] are known: k_21_40 ===> k_20_21
k_21_41 in symmetric relation [k_20_22, k_21_41] are known: k_21_41 ===> k_20_22
k_21_54 in symmetric relation [k_20_35, k_21_54] are known: k_21_54 ===> k_20_35
k_22_12 in symmetric relation [k_21_73, k_22_12] are known: k_22_12 ===> k_21_73
k_22_33 in symmetric relation [k_21_14, k_22_33] are known: k_22_33 ===> k_21_14
k_22_34 in symmetric relation [k_21_15, k_22_34] are known: k_22_34 ===> k_21_15
k_22_36 in symmetric relation [k_21_17, k_22_36] are known: k_22_36 ===> k_21_17
k_22_37 in symmetric relation [k_21_18, k_22_37] are known: k_22_37 ===> k_21_18
k_22_46 in symmetric relation [k_21_27, k_22_46] are known: k_22_46 ===> k_21_27
k_22_47 in symmetric relation [k_21_28, k_22_47] are known: k_22_47 ===> k_21_28
k_22_49 in symmetric relation [k_21_30, k_22_49] are known: k_22_49 ===> k_21_30
k_21_43 in symmetric relation [k_21_43, k_22_62] are known: k_21_43 ===> k_22_62
k_22_67 in symmetric relation [k_21_48, k_22_67] are known: k_22_67 ===> k_21_48
k_22_8 in symmetric relation [k_22_8, k_23_27] are known: k_22_8 ===> k_23_27
k_22_14 in symmetric relation [k_22_14, k_23_33] are known: k_22_14 ===> k_23_33
k_22_16 in symmetric relation [k_22_16, k_23_35] are known: k_22_16 ===> k_23_35
k_22_18 in symmetric relation [k_22_18, k_23_37] are known: k_22_18 ===> k_23_37
k_22_50 in symmetric relation [k_22_50, k_23_69] are known: k_22_50 ===> k_23_69
k_23_70 in symmetric relation [k_23_70, k_24_9] are known: k_23_70 ===> k_24_9
k_23_50 in symmetric relation [k_23_50, k_24_69] are known: k_23_50 ===> k_24_69
k_24_73 in symmetric relation [k_24_73, k_25_12] are known: k_24_73 ===> k_25_12
k_24_37 in symmetric relation [k_24_37, k_25_56] are known: k_24_37 ===> k_25_56
k_25_7 in symmetric relation [k_25_7, k_26_26] are known: k_25_7 ===> k_26_26
k_25_9 in symmetric relation [k_25_9, k_26_28] are known: k_25_9 ===> k_26_28
############################################################
State 5:
k_1_56 in symmetric relation [k_0_37, k_1_56] are known: k_1_56 ===> k_0_37
k_4_32 in symmetric relation [k_3_13, k_4_32] are known: k_4_32 ===> k_3_13
k_5_37 in symmetric relation [k_5_37, k_6_56] are known: k_5_37 ===> k_6_56
k_6_69 in symmetric relation [k_5_50, k_6_69] are known: k_6_69 ===> k_5_50
k_7_73 in symmetric relation [k_6_54, k_7_73] are known: k_7_73 ===> k_6_54
k_8_35 in symmetric relation [k_7_16, k_8_35] are known: k_8_35 ===> k_7_16
k_8_37 in symmetric relation [k_7_18, k_8_37] are known: k_8_37 ===> k_7_18
k_8_39 in symmetric relation [k_7_20, k_8_39] are known: k_8_39 ===> k_7_20
k_9_13 in symmetric relation [k_8_74, k_9_13] are known: k_9_13 ===> k_8_74
k_9_18 in symmetric relation [k_8_79, k_9_18] are known: k_9_18 ===> k_8_79
k_9_32 in symmetric relation [k_9_32, k_10_51] are known: k_9_32 ===> k_10_51
k_9_35 in symmetric relation [k_9_35, k_10_54] are known: k_9_35 ===> k_10_54
k_9_49 in symmetric relation [k_9_49, k_10_68] are known: k_9_49 ===> k_10_68
k_11_52 in symmetric relation [k_10_33, k_11_52] are known: k_11_52 ===> k_10_33
k_11_57 in symmetric relation [k_10_38, k_11_57] are known: k_11_57 ===> k_10_38
k_11_74 in symmetric relation [k_10_55, k_11_74] are known: k_11_74 ===> k_10_55
k_11_6 in symmetric relation [k_11_6, k_12_25] are known: k_11_6 ===> k_12_25
k_12_32 in symmetric relation [k_11_13, k_12_32] are known: k_12_32 ===> k_11_13
k_12_73 in symmetric relation [k_12_73, k_13_12] are known: k_12_73 ===> k_13_12
k_13_30 in symmetric relation [k_12_11, k_13_30] are known: k_13_30 ===> k_12_11
k_13_39 in symmetric relation [k_12_20, k_13_39] are known: k_13_39 ===> k_12_20
k_13_53 in symmetric relation [k_12_34, k_13_53] are known: k_13_53 ===> k_12_34
k_13_77 in symmetric relation [k_12_58, k_13_77] are known: k_13_77 ===> k_12_58
k_13_17 in symmetric relation [k_13_17, k_14_36] are known: k_13_17 ===> k_14_36
k_14_39 in symmetric relation [k_13_20, k_14_39] are known: k_14_39 ===> k_13_20
k_14_59 in symmetric relation [k_13_40, k_14_59] are known: k_14_59 ===> k_13_40
k_14_18 in symmetric relation [k_14_18, k_15_37] are known: k_14_18 ===> k_15_37
k_15_46 in symmetric relation [k_14_27, k_15_46] are known: k_15_46 ===> k_14_27
k_15_49 in symmetric relation [k_14_30, k_15_49] are known: k_15_49 ===> k_14_30
k_16_76 in symmetric relation [k_15_57, k_16_76] are known: k_16_76 ===> k_15_57
k_16_78 in symmetric relation [k_15_59, k_16_78] are known: k_16_78 ===> k_15_59
k_17_30 in symmetric relation [k_16_11, k_17_30] are known: k_17_30 ===> k_16_11
k_17_23 in symmetric relation [k_17_23, k_18_42] are known: k_17_23 ===> k_18_42
k_18_48 in symmetric relation [k_17_29, k_18_48] are known: k_18_48 ===> k_17_29
k_18_52 in symmetric relation [k_17_33, k_18_52] are known: k_18_52 ===> k_17_33
k_17_37 in symmetric relation [k_17_37, k_18_56] are known: k_17_37 ===> k_18_56
k_18_65 in symmetric relation [k_18_65, k_19_4] are known: k_18_65 ===> k_19_4
k_18_67 in symmetric relation [k_18_67, k_19_6] are known: k_18_67 ===> k_19_6
k_18_69 in symmetric relation [k_18_69, k_19_8] are known: k_18_69 ===> k_19_8
k_19_9 in symmetric relation [k_18_70, k_19_9] are known: k_19_9 ===> k_18_70
k_19_14 in symmetric relation [k_18_75, k_19_14] are known: k_19_14 ===> k_18_75
k_19_47 in symmetric relation [k_18_28, k_19_47] are known: k_19_47 ===> k_18_28
k_20_19 in symmetric relation [k_19_0, k_20_19] are known: k_20_19 ===> k_19_0
k_20_20 in symmetric relation [k_19_1, k_20_20] are known: k_20_20 ===> k_19_1
k_20_21 in symmetric relation [k_19_2, k_20_21] are known: k_20_21 ===> k_19_2
k_20_22 in symmetric relation [k_19_3, k_20_22] are known: k_20_22 ===> k_19_3
k_20_35 in symmetric relation [k_19_16, k_20_35] are known: k_20_35 ===> k_19_16
k_19_43 in symmetric relation [k_19_43, k_20_62] are known: k_19_43 ===> k_20_62
k_19_48 in symmetric relation [k_19_48, k_20_67] are known: k_19_48 ===> k_20_67
k_21_14 in symmetric relation [k_20_75, k_21_14] are known: k_21_14 ===> k_20_75
k_21_15 in symmetric relation [k_20_76, k_21_15] are known: k_21_15 ===> k_20_76
k_21_17 in symmetric relation [k_20_78, k_21_17] are known: k_21_17 ===> k_20_78
k_21_18 in symmetric relation [k_20_79, k_21_18] are known: k_21_18 ===> k_20_79
k_21_27 in symmetric relation [k_20_8, k_21_27] are known: k_21_27 ===> k_20_8
k_21_28 in symmetric relation [k_20_9, k_21_28] are known: k_21_28 ===> k_20_9
k_21_30 in symmetric relation [k_20_11, k_21_30] are known: k_21_30 ===> k_20_11
k_21_48 in symmetric relation [k_20_29, k_21_48] are known: k_21_48 ===> k_20_29
k_21_73 in symmetric relation [k_20_54, k_21_73] are known: k_21_73 ===> k_20_54
k_21_7 in symmetric relation [k_21_7, k_22_26] are known: k_21_7 ===> k_22_26
k_21_24 in symmetric relation [k_21_24, k_22_43] are known: k_21_24 ===> k_22_43
k_23_69 in symmetric relation [k_23_69, k_24_8] are known: k_23_69 ===> k_24_8
k_23_27 in symmetric relation [k_23_27, k_24_46] are known: k_23_27 ===> k_24_46
k_23_33 in symmetric relation [k_23_33, k_24_52] are known: k_23_33 ===> k_24_52
k_23_35 in symmetric relation [k_23_35, k_24_54] are known: k_23_35 ===> k_24_54
k_23_37 in symmetric relation [k_23_37, k_24_56] are known: k_23_37 ===> k_24_56
k_24_69 in symmetric relation [k_24_69, k_25_8] are known: k_24_69 ===> k_25_8
k_24_9 in symmetric relation [k_24_9, k_25_28] are known: k_24_9 ===> k_25_28
k_25_12 in symmetric relation [k_25_12, k_26_31] are known: k_25_12 ===> k_26_31
k_25_56 in symmetric relation [k_25_56, k_26_75] are known: k_25_56 ===> k_26_75
############################################################
State 6:
k_3_13 in symmetric relation [k_2_74, k_3_13] are known: k_3_13 ===> k_2_74
k_5_50 in symmetric relation [k_4_31, k_5_50] are known: k_5_50 ===> k_4_31
k_6_54 in symmetric relation [k_5_35, k_6_54] are known: k_6_54 ===> k_5_35
k_7_16 in symmetric relation [k_6_77, k_7_16] are known: k_7_16 ===> k_6_77
k_7_18 in symmetric relation [k_6_79, k_7_18] are known: k_7_18 ===> k_6_79
k_7_20 in symmetric relation [k_6_1, k_7_20] are known: k_7_20 ===> k_6_1
k_6_56 in symmetric relation [k_6_56, k_7_75] are known: k_6_56 ===> k_7_75
k_8_74 in symmetric relation [k_7_55, k_8_74] are known: k_8_74 ===> k_7_55
k_8_79 in symmetric relation [k_7_60, k_8_79] are known: k_8_79 ===> k_7_60
k_10_33 in symmetric relation [k_9_14, k_10_33] are known: k_10_33 ===> k_9_14
k_10_38 in symmetric relation [k_9_19, k_10_38] are known: k_10_38 ===> k_9_19
k_10_55 in symmetric relation [k_9_36, k_10_55] are known: k_10_55 ===> k_9_36
k_10_68 in symmetric relation [k_10_68, k_11_7] are known: k_10_68 ===> k_11_7
k_11_13 in symmetric relation [k_10_74, k_11_13] are known: k_11_13 ===> k_10_74
k_10_51 in symmetric relation [k_10_51, k_11_70] are known: k_10_51 ===> k_11_70
k_10_54 in symmetric relation [k_10_54, k_11_73] are known: k_10_54 ===> k_11_73
k_12_11 in symmetric relation [k_11_72, k_12_11] are known: k_12_11 ===> k_11_72
k_12_20 in symmetric relation [k_11_1, k_12_20] are known: k_12_20 ===> k_11_1
k_12_34 in symmetric relation [k_11_15, k_12_34] are known: k_12_34 ===> k_11_15
k_12_58 in symmetric relation [k_11_39, k_12_58] are known: k_12_58 ===> k_11_39
k_13_20 in symmetric relation [k_12_1, k_13_20] are known: k_13_20 ===> k_12_1
k_13_40 in symmetric relation [k_12_21, k_13_40] are known: k_13_40 ===> k_12_21
k_12_25 in symmetric relation [k_12_25, k_13_44] are known: k_12_25 ===> k_13_44
k_14_27 in symmetric relation [k_13_8, k_14_27] are known: k_14_27 ===> k_13_8
k_14_30 in symmetric relation [k_13_11, k_14_30] are known: k_14_30 ===> k_13_11
k_13_12 in symmetric relation [k_13_12, k_14_31] are known: k_13_12 ===> k_14_31
k_14_36 in symmetric relation [k_14_36, k_15_55] are known: k_14_36 ===> k_15_55
k_15_57 in symmetric relation [k_14_38, k_15_57] are known: k_15_57 ===> k_14_38
k_15_59 in symmetric relation [k_14_40, k_15_59] are known: k_15_59 ===> k_14_40
k_16_11 in symmetric relation [k_15_72, k_16_11] are known: k_16_11 ===> k_15_72
k_15_37 in symmetric relation [k_15_37, k_16_56] are known: k_15_37 ===> k_16_56
k_17_29 in symmetric relation [k_16_10, k_17_29] are known: k_17_29 ===> k_16_10
k_17_33 in symmetric relation [k_16_14, k_17_33] are known: k_17_33 ===> k_16_14
k_18_28 in symmetric relation [k_17_9, k_18_28] are known: k_18_28 ===> k_17_9
k_18_70 in symmetric relation [k_17_51, k_18_70] are known: k_18_70 ===> k_17_51
k_18_75 in symmetric relation [k_17_56, k_18_75] are known: k_18_75 ===> k_17_56
k_19_16 in symmetric relation [k_18_77, k_19_16] are known: k_19_16 ===> k_18_77
k_18_42 in symmetric relation [k_18_42, k_19_61] are known: k_18_42 ===> k_19_61
k_18_56 in symmetric relation [k_18_56, k_19_75] are known: k_18_56 ===> k_19_75
k_20_8 in symmetric relation [k_19_69, k_20_8] are known: k_20_8 ===> k_19_69
k_20_9 in symmetric relation [k_19_70, k_20_9] are known: k_20_9 ===> k_19_70
k_20_11 in symmetric relation [k_19_72, k_20_11] are known: k_20_11 ===> k_19_72
k_19_4 in symmetric relation [k_19_4, k_20_23] are known: k_19_4 ===> k_20_23
k_19_6 in symmetric relation [k_19_6, k_20_25] are known: k_19_6 ===> k_20_25
k_19_8 in symmetric relation [k_19_8, k_20_27] are known: k_19_8 ===> k_20_27
k_20_29 in symmetric relation [k_19_10, k_20_29] are known: k_20_29 ===> k_19_10
k_20_54 in symmetric relation [k_19_35, k_20_54] are known: k_20_54 ===> k_19_35
k_20_75 in symmetric relation [k_19_56, k_20_75] are known: k_20_75 ===> k_19_56
k_20_76 in symmetric relation [k_19_57, k_20_76] are known: k_20_76 ===> k_19_57
k_20_78 in symmetric relation [k_19_59, k_20_78] are known: k_20_78 ===> k_19_59
k_20_79 in symmetric relation [k_19_60, k_20_79] are known: k_20_79 ===> k_19_60
k_20_67 in symmetric relation [k_20_67, k_21_6] are known: k_20_67 ===> k_21_6
k_22_26 in symmetric relation [k_22_26, k_23_45] are known: k_22_26 ===> k_23_45
k_22_43 in symmetric relation [k_22_43, k_23_62] are known: k_22_43 ===> k_23_62
k_24_8 in symmetric relation [k_24_8, k_25_27] are known: k_24_8 ===> k_25_27
k_24_46 in symmetric relation [k_24_46, k_25_65] are known: k_24_46 ===> k_25_65
k_24_52 in symmetric relation [k_24_52, k_25_71] are known: k_24_52 ===> k_25_71
k_24_54 in symmetric relation [k_24_54, k_25_73] are known: k_24_54 ===> k_25_73
k_24_56 in symmetric relation [k_24_56, k_25_75] are known: k_24_56 ===> k_25_75
k_25_8 in symmetric relation [k_25_8, k_26_27] are known: k_25_8 ===> k_26_27
k_25_28 in symmetric relation [k_25_28, k_26_47] are known: k_25_28 ===> k_26_47
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_61] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_61
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_62] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_62
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_63] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_63
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_64] are known: k_19_0, k_19_1, k_19_2, k_19_3 ===> k_18_64
k_20_61, k_20_62, k_20_63, k_20_64 in implication relation [k_20_61, k_20_62, k_20_63, k_20_64, k_21_0] are known: k_20_61, k_20_62, k_20_63, k_20_64 ===> k_21_0
k_20_61, k_20_62, k_20_63, k_20_64 in implication relation [k_20_61, k_20_62, k_20_63, k_20_64, k_21_1] are known: k_20_61, k_20_62, k_20_63, k_20_64 ===> k_21_1
k_20_61, k_20_62, k_20_63, k_20_64 in implication relation [k_20_61, k_20_62, k_20_63, k_20_64, k_21_2] are known: k_20_61, k_20_62, k_20_63, k_20_64 ===> k_21_2
k_20_61, k_20_62, k_20_63, k_20_64 in implication relation [k_20_61, k_20_62, k_20_63, k_20_64, k_21_3] are known: k_20_61, k_20_62, k_20_63, k_20_64 ===> k_21_3
############################################################
State 7:
k_2_74 in symmetric relation [k_1_55, k_2_74] are known: k_2_74 ===> k_1_55
k_4_31 in symmetric relation [k_3_12, k_4_31] are known: k_4_31 ===> k_3_12
k_5_35 in symmetric relation [k_4_16, k_5_35] are known: k_5_35 ===> k_4_16
k_6_77 in symmetric relation [k_5_58, k_6_77] are known: k_6_77 ===> k_5_58
k_6_79 in symmetric relation [k_5_60, k_6_79] are known: k_6_79 ===> k_5_60
k_7_55 in symmetric relation [k_6_36, k_7_55] are known: k_7_55 ===> k_6_36
k_7_60 in symmetric relation [k_6_41, k_7_60] are known: k_7_60 ===> k_6_41
k_7_75 in symmetric relation [k_7_75, k_8_14] are known: k_7_75 ===> k_8_14
k_9_14 in symmetric relation [k_8_75, k_9_14] are known: k_9_14 ===> k_8_75
k_9_19 in symmetric relation [k_8_0, k_9_19] are known: k_9_19 ===> k_8_0
k_9_36 in symmetric relation [k_8_17, k_9_36] are known: k_9_36 ===> k_8_17
k_10_74 in symmetric relation [k_9_55, k_10_74] are known: k_10_74 ===> k_9_55
k_11_15 in symmetric relation [k_10_76, k_11_15] are known: k_11_15 ===> k_10_76
k_11_39 in symmetric relation [k_10_20, k_11_39] are known: k_11_39 ===> k_10_20
k_11_72 in symmetric relation [k_10_53, k_11_72] are known: k_11_72 ===> k_10_53
k_11_70 in symmetric relation [k_11_70, k_12_9] are known: k_11_70 ===> k_12_9
k_11_73 in symmetric relation [k_11_73, k_12_12] are known: k_11_73 ===> k_12_12
k_12_21 in symmetric relation [k_11_2, k_12_21] are known: k_12_21 ===> k_11_2
k_11_7 in symmetric relation [k_11_7, k_12_26] are known: k_11_7 ===> k_12_26
k_13_8 in symmetric relation [k_12_69, k_13_8] are known: k_13_8 ===> k_12_69
k_13_11 in symmetric relation [k_12_72, k_13_11] are known: k_13_11 ===> k_12_72
k_14_38 in symmetric relation [k_13_19, k_14_38] are known: k_14_38 ===> k_13_19
k_14_40 in symmetric relation [k_13_21, k_14_40] are known: k_14_40 ===> k_13_21
k_13_44 in symmetric relation [k_13_44, k_14_63] are known: k_13_44 ===> k_14_63
k_14_31 in symmetric relation [k_14_31, k_15_50] are known: k_14_31 ===> k_15_50
k_15_72 in symmetric relation [k_14_53, k_15_72] are known: k_15_72 ===> k_14_53
k_16_10 in symmetric relation [k_15_71, k_16_10] are known: k_16_10 ===> k_15_71
k_16_14 in symmetric relation [k_15_75, k_16_14] are known: k_16_14 ===> k_15_75
k_15_55 in symmetric relation [k_15_55, k_16_74] are known: k_15_55 ===> k_16_74
k_17_9 in symmetric relation [k_16_70, k_17_9] are known: k_17_9 ===> k_16_70
k_17_51 in symmetric relation [k_16_32, k_17_51] are known: k_17_51 ===> k_16_32
k_17_56 in symmetric relation [k_16_37, k_17_56] are known: k_17_56 ===> k_16_37
k_16_56 in symmetric relation [k_16_56, k_17_75] are known: k_16_56 ===> k_17_75
k_18_61 in symmetric relation [k_17_42, k_18_61] are known: k_18_61 ===> k_17_42
k_18_62 in symmetric relation [k_17_43, k_18_62] are known: k_18_62 ===> k_17_43
k_18_63 in symmetric relation [k_17_44, k_18_63] are known: k_18_63 ===> k_17_44
k_18_64 in symmetric relation [k_17_45, k_18_64] are known: k_18_64 ===> k_17_45
k_18_77 in symmetric relation [k_17_58, k_18_77] are known: k_18_77 ===> k_17_58
k_19_10 in symmetric relation [k_18_71, k_19_10] are known: k_19_10 ===> k_18_71
k_19_35 in symmetric relation [k_18_16, k_19_35] are known: k_19_35 ===> k_18_16
k_19_56 in symmetric relation [k_18_37, k_19_56] are known: k_19_56 ===> k_18_37
k_19_57 in symmetric relation [k_18_38, k_19_57] are known: k_19_57 ===> k_18_38
k_19_59 in symmetric relation [k_18_40, k_19_59] are known: k_19_59 ===> k_18_40
k_19_60 in symmetric relation [k_18_41, k_19_60] are known: k_19_60 ===> k_18_41
k_19_69 in symmetric relation [k_18_50, k_19_69] are known: k_19_69 ===> k_18_50
k_19_70 in symmetric relation [k_18_51, k_19_70] are known: k_19_70 ===> k_18_51
k_19_72 in symmetric relation [k_18_53, k_19_72] are known: k_19_72 ===> k_18_53
k_19_75 in symmetric relation [k_19_75, k_20_14] are known: k_19_75 ===> k_20_14
k_20_23 in symmetric relation [k_20_23, k_21_42] are known: k_20_23 ===> k_21_42
k_20_25 in symmetric relation [k_20_25, k_21_44] are known: k_20_25 ===> k_21_44
k_20_27 in symmetric relation [k_20_27, k_21_46] are known: k_20_27 ===> k_21_46
k_21_0 in symmetric relation [k_21_0, k_22_19] are known: k_21_0 ===> k_22_19
k_21_1 in symmetric relation [k_21_1, k_22_20] are known: k_21_1 ===> k_22_20
k_21_2 in symmetric relation [k_21_2, k_22_21] are known: k_21_2 ===> k_22_21
k_21_3 in symmetric relation [k_21_3, k_22_22] are known: k_21_3 ===> k_22_22
k_21_6 in symmetric relation [k_21_6, k_22_25] are known: k_21_6 ===> k_22_25
k_23_45 in symmetric relation [k_23_45, k_24_64] are known: k_23_45 ===> k_24_64
k_25_65 in symmetric relation [k_25_65, k_26_4] are known: k_25_65 ===> k_26_4
k_25_71 in symmetric relation [k_25_71, k_26_10] are known: k_25_71 ===> k_26_10
k_25_73 in symmetric relation [k_25_73, k_26_12] are known: k_25_73 ===> k_26_12
k_25_75 in symmetric relation [k_25_75, k_26_14] are known: k_25_75 ===> k_26_14
k_25_27 in symmetric relation [k_25_27, k_26_46] are known: k_25_27 ===> k_26_46
############################################################
State 8:
k_1_55 in symmetric relation [k_0_36, k_1_55] are known: k_1_55 ===> k_0_36
k_3_12 in symmetric relation [k_2_73, k_3_12] are known: k_3_12 ===> k_2_73
k_4_16 in symmetric relation [k_3_77, k_4_16] are known: k_4_16 ===> k_3_77
k_5_58 in symmetric relation [k_4_39, k_5_58] are known: k_5_58 ===> k_4_39
k_5_60 in symmetric relation [k_4_41, k_5_60] are known: k_5_60 ===> k_4_41
k_6_36 in symmetric relation [k_5_17, k_6_36] are known: k_6_36 ===> k_5_17
k_6_41 in symmetric relation [k_5_22, k_6_41] are known: k_6_41 ===> k_5_22
k_8_17 in symmetric relation [k_7_78, k_8_17] are known: k_8_17 ===> k_7_78
k_8_75 in symmetric relation [k_7_56, k_8_75] are known: k_8_75 ===> k_7_56
k_8_14 in symmetric relation [k_8_14, k_9_33] are known: k_8_14 ===> k_9_33
k_9_55 in symmetric relation [k_8_36, k_9_55] are known: k_9_55 ===> k_8_36
k_10_20 in symmetric relation [k_9_1, k_10_20] are known: k_10_20 ===> k_9_1
k_10_53 in symmetric relation [k_9_34, k_10_53] are known: k_10_53 ===> k_9_34
k_10_76 in symmetric relation [k_9_57, k_10_76] are known: k_10_76 ===> k_9_57
k_12_69 in symmetric relation [k_11_50, k_12_69] are known: k_12_69 ===> k_11_50
k_12_72 in symmetric relation [k_11_53, k_12_72] are known: k_12_72 ===> k_11_53
k_13_19 in symmetric relation [k_12_0, k_13_19] are known: k_13_19 ===> k_12_0
k_13_21 in symmetric relation [k_12_2, k_13_21] are known: k_13_21 ===> k_12_2
k_12_9 in symmetric relation [k_12_9, k_13_28] are known: k_12_9 ===> k_13_28
k_12_12 in symmetric relation [k_12_12, k_13_31] are known: k_12_12 ===> k_13_31
k_12_26 in symmetric relation [k_12_26, k_13_45] are known: k_12_26 ===> k_13_45
k_14_53 in symmetric relation [k_13_34, k_14_53] are known: k_14_53 ===> k_13_34
k_15_71 in symmetric relation [k_14_52, k_15_71] are known: k_15_71 ===> k_14_52
k_15_75 in symmetric relation [k_14_56, k_15_75] are known: k_15_75 ===> k_14_56
k_16_32 in symmetric relation [k_15_13, k_16_32] are known: k_16_32 ===> k_15_13
k_16_37 in symmetric relation [k_15_18, k_16_37] are known: k_16_37 ===> k_15_18
k_15_50 in symmetric relation [k_15_50, k_16_69] are known: k_15_50 ===> k_16_69
k_16_70 in symmetric relation [k_15_51, k_16_70] are known: k_16_70 ===> k_15_51
k_16_74 in symmetric relation [k_16_74, k_17_13] are known: k_16_74 ===> k_17_13
k_17_42 in symmetric relation [k_16_23, k_17_42] are known: k_17_42 ===> k_16_23
k_17_43 in symmetric relation [k_16_24, k_17_43] are known: k_17_43 ===> k_16_24
k_17_44 in symmetric relation [k_16_25, k_17_44] are known: k_17_44 ===> k_16_25
k_17_45 in symmetric relation [k_16_26, k_17_45] are known: k_17_45 ===> k_16_26
k_17_58 in symmetric relation [k_16_39, k_17_58] are known: k_17_58 ===> k_16_39
k_17_75 in symmetric relation [k_17_75, k_18_14] are known: k_17_75 ===> k_18_14
k_18_16 in symmetric relation [k_17_77, k_18_16] are known: k_18_16 ===> k_17_77
k_18_37 in symmetric relation [k_17_18, k_18_37] are known: k_18_37 ===> k_17_18
k_18_38 in symmetric relation [k_17_19, k_18_38] are known: k_18_38 ===> k_17_19
k_18_40 in symmetric relation [k_17_21, k_18_40] are known: k_18_40 ===> k_17_21
k_18_41 in symmetric relation [k_17_22, k_18_41] are known: k_18_41 ===> k_17_22
k_18_50 in symmetric relation [k_17_31, k_18_50] are known: k_18_50 ===> k_17_31
k_18_51 in symmetric relation [k_17_32, k_18_51] are known: k_18_51 ===> k_17_32
k_18_53 in symmetric relation [k_17_34, k_18_53] are known: k_18_53 ===> k_17_34
k_18_71 in symmetric relation [k_17_52, k_18_71] are known: k_18_71 ===> k_17_52
k_20_14 in symmetric relation [k_20_14, k_21_33] are known: k_20_14 ===> k_21_33
k_21_42 in symmetric relation [k_21_42, k_22_61] are known: k_21_42 ===> k_22_61
k_21_44 in symmetric relation [k_21_44, k_22_63] are known: k_21_44 ===> k_22_63
k_21_46 in symmetric relation [k_21_46, k_22_65] are known: k_21_46 ===> k_22_65
k_22_19 in symmetric relation [k_22_19, k_23_38] are known: k_22_19 ===> k_23_38
k_22_20 in symmetric relation [k_22_20, k_23_39] are known: k_22_20 ===> k_23_39
k_22_21 in symmetric relation [k_22_21, k_23_40] are known: k_22_21 ===> k_23_40
k_22_22 in symmetric relation [k_22_22, k_23_41] are known: k_22_22 ===> k_23_41
k_22_25 in symmetric relation [k_22_25, k_23_44] are known: k_22_25 ===> k_23_44
############################################################
State 9:
k_2_73 in symmetric relation [k_1_54, k_2_73] are known: k_2_73 ===> k_1_54
k_3_77 in symmetric relation [k_2_58, k_3_77] are known: k_3_77 ===> k_2_58
k_4_39 in symmetric relation [k_3_20, k_4_39] are known: k_4_39 ===> k_3_20
k_4_41 in symmetric relation [k_3_22, k_4_41] are known: k_4_41 ===> k_3_22
k_5_17 in symmetric relation [k_4_78, k_5_17] are known: k_5_17 ===> k_4_78
k_5_22 in symmetric relation [k_4_3, k_5_22] are known: k_5_22 ===> k_4_3
k_7_56 in symmetric relation [k_6_37, k_7_56] are known: k_7_56 ===> k_6_37
k_7_78 in symmetric relation [k_6_59, k_7_78] are known: k_7_78 ===> k_6_59
k_8_36 in symmetric relation [k_7_17, k_8_36] are known: k_8_36 ===> k_7_17
k_9_34 in symmetric relation [k_8_15, k_9_34] are known: k_9_34 ===> k_8_15
k_9_57 in symmetric relation [k_8_38, k_9_57] are known: k_9_57 ===> k_8_38
k_9_33 in symmetric relation [k_9_33, k_10_52] are known: k_9_33 ===> k_10_52
k_11_50 in symmetric relation [k_10_31, k_11_50] are known: k_11_50 ===> k_10_31
k_11_53 in symmetric relation [k_10_34, k_11_53] are known: k_11_53 ===> k_10_34
k_13_34 in symmetric relation [k_12_15, k_13_34] are known: k_13_34 ===> k_12_15
k_13_28 in symmetric relation [k_13_28, k_14_47] are known: k_13_28 ===> k_14_47
k_13_31 in symmetric relation [k_13_31, k_14_50] are known: k_13_31 ===> k_14_50
k_14_52 in symmetric relation [k_13_33, k_14_52] are known: k_14_52 ===> k_13_33
k_14_56 in symmetric relation [k_13_37, k_14_56] are known: k_14_56 ===> k_13_37
k_13_45 in symmetric relation [k_13_45, k_14_64] are known: k_13_45 ===> k_14_64
k_15_13 in symmetric relation [k_14_74, k_15_13] are known: k_15_13 ===> k_14_74
k_15_18 in symmetric relation [k_14_79, k_15_18] are known: k_15_18 ===> k_14_79
k_15_51 in symmetric relation [k_14_32, k_15_51] are known: k_15_51 ===> k_14_32
k_16_23 in symmetric relation [k_15_4, k_16_23] are known: k_16_23 ===> k_15_4
k_16_24 in symmetric relation [k_15_5, k_16_24] are known: k_16_24 ===> k_15_5
k_16_25 in symmetric relation [k_15_6, k_16_25] are known: k_16_25 ===> k_15_6
k_16_26 in symmetric relation [k_15_7, k_16_26] are known: k_16_26 ===> k_15_7
k_16_39 in symmetric relation [k_15_20, k_16_39] are known: k_16_39 ===> k_15_20
k_16_69 in symmetric relation [k_16_69, k_17_8] are known: k_16_69 ===> k_17_8
k_17_18 in symmetric relation [k_16_79, k_17_18] are known: k_17_18 ===> k_16_79
k_17_19 in symmetric relation [k_16_0, k_17_19] are known: k_17_19 ===> k_16_0
k_17_21 in symmetric relation [k_16_2, k_17_21] are known: k_17_21 ===> k_16_2
k_17_22 in symmetric relation [k_16_3, k_17_22] are known: k_17_22 ===> k_16_3
k_17_31 in symmetric relation [k_16_12, k_17_31] are known: k_17_31 ===> k_16_12
k_17_32 in symmetric relation [k_16_13, k_17_32] are known: k_17_32 ===> k_16_13
k_17_34 in symmetric relation [k_16_15, k_17_34] are known: k_17_34 ===> k_16_15
k_17_52 in symmetric relation [k_16_33, k_17_52] are known: k_17_52 ===> k_16_33
k_17_77 in symmetric relation [k_16_58, k_17_77] are known: k_17_77 ===> k_16_58
k_17_13 in symmetric relation [k_17_13, k_18_32] are known: k_17_13 ===> k_18_32
k_18_14 in symmetric relation [k_18_14, k_19_33] are known: k_18_14 ===> k_19_33
k_21_33 in symmetric relation [k_21_33, k_22_52] are known: k_21_33 ===> k_22_52
k_22_65 in symmetric relation [k_22_65, k_23_4] are known: k_22_65 ===> k_23_4
k_23_38 in symmetric relation [k_23_38, k_24_57] are known: k_23_38 ===> k_24_57
k_23_39 in symmetric relation [k_23_39, k_24_58] are known: k_23_39 ===> k_24_58
k_23_40 in symmetric relation [k_23_40, k_24_59] are known: k_23_40 ===> k_24_59
k_23_41 in symmetric relation [k_23_41, k_24_60] are known: k_23_41 ===> k_24_60
k_23_44 in symmetric relation [k_23_44, k_24_63] are known: k_23_44 ===> k_24_63
k_22_61, k_22_62, k_22_63, k_22_64 in implication relation [k_22_61, k_22_62, k_22_63, k_22_64, k_23_0] are known: k_22_61, k_22_62, k_22_63, k_22_64 ===> k_23_0
k_22_61, k_22_62, k_22_63, k_22_64 in implication relation [k_22_61, k_22_62, k_22_63, k_22_64, k_23_1] are known: k_22_61, k_22_62, k_22_63, k_22_64 ===> k_23_1
k_22_61, k_22_62, k_22_63, k_22_64 in implication relation [k_22_61, k_22_62, k_22_63, k_22_64, k_23_2] are known: k_22_61, k_22_62, k_22_63, k_22_64 ===> k_23_2
k_22_61, k_22_62, k_22_63, k_22_64 in implication relation [k_22_61, k_22_62, k_22_63, k_22_64, k_23_3] are known: k_22_61, k_22_62, k_22_63, k_22_64 ===> k_23_3
############################################################
State 10:
k_1_54 in symmetric relation [k_0_35, k_1_54] are known: k_1_54 ===> k_0_35
k_2_58 in symmetric relation [k_1_39, k_2_58] are known: k_2_58 ===> k_1_39
k_3_20 in symmetric relation [k_2_1, k_3_20] are known: k_3_20 ===> k_2_1
k_3_22 in symmetric relation [k_2_3, k_3_22] are known: k_3_22 ===> k_2_3
k_4_78 in symmetric relation [k_3_59, k_4_78] are known: k_4_78 ===> k_3_59
k_6_37 in symmetric relation [k_5_18, k_6_37] are known: k_6_37 ===> k_5_18
k_6_59 in symmetric relation [k_5_40, k_6_59] are known: k_6_59 ===> k_5_40
k_7_17 in symmetric relation [k_6_78, k_7_17] are known: k_7_17 ===> k_6_78
k_8_15 in symmetric relation [k_7_76, k_8_15] are known: k_8_15 ===> k_7_76
k_8_38 in symmetric relation [k_7_19, k_8_38] are known: k_8_38 ===> k_7_19
k_10_31 in symmetric relation [k_9_12, k_10_31] are known: k_10_31 ===> k_9_12
k_10_34 in symmetric relation [k_9_15, k_10_34] are known: k_10_34 ===> k_9_15
k_10_52 in symmetric relation [k_10_52, k_11_71] are known: k_10_52 ===> k_11_71
k_12_15 in symmetric relation [k_11_76, k_12_15] are known: k_12_15 ===> k_11_76
k_13_33 in symmetric relation [k_12_14, k_13_33] are known: k_13_33 ===> k_12_14
k_13_37 in symmetric relation [k_12_18, k_13_37] are known: k_13_37 ===> k_12_18
k_14_32 in symmetric relation [k_13_13, k_14_32] are known: k_14_32 ===> k_13_13
k_14_74 in symmetric relation [k_13_55, k_14_74] are known: k_14_74 ===> k_13_55
k_14_79 in symmetric relation [k_13_60, k_14_79] are known: k_14_79 ===> k_13_60
k_15_4 in symmetric relation [k_14_65, k_15_4] are known: k_15_4 ===> k_14_65
k_15_5 in symmetric relation [k_14_66, k_15_5] are known: k_15_5 ===> k_14_66
k_15_6 in symmetric relation [k_14_67, k_15_6] are known: k_15_6 ===> k_14_67
k_15_7 in symmetric relation [k_14_68, k_15_7] are known: k_15_7 ===> k_14_68
k_15_20 in symmetric relation [k_14_1, k_15_20] are known: k_15_20 ===> k_14_1
k_14_47 in symmetric relation [k_14_47, k_15_66] are known: k_14_47 ===> k_15_66
k_14_50 in symmetric relation [k_14_50, k_15_69] are known: k_14_50 ===> k_15_69
k_16_12 in symmetric relation [k_15_73, k_16_12] are known: k_16_12 ===> k_15_73
k_16_13 in symmetric relation [k_15_74, k_16_13] are known: k_16_13 ===> k_15_74
k_16_15 in symmetric relation [k_15_76, k_16_15] are known: k_16_15 ===> k_15_76
k_16_33 in symmetric relation [k_15_14, k_16_33] are known: k_16_33 ===> k_15_14
k_16_58 in symmetric relation [k_15_39, k_16_58] are known: k_16_58 ===> k_15_39
k_16_79 in symmetric relation [k_15_60, k_16_79] are known: k_16_79 ===> k_15_60
k_17_8 in symmetric relation [k_17_8, k_18_27] are known: k_17_8 ===> k_18_27
k_18_32 in symmetric relation [k_18_32, k_19_51] are known: k_18_32 ===> k_19_51
k_19_33 in symmetric relation [k_19_33, k_20_52] are known: k_19_33 ===> k_20_52
k_22_52 in symmetric relation [k_22_52, k_23_71] are known: k_22_52 ===> k_23_71
k_23_0 in symmetric relation [k_23_0, k_24_19] are known: k_23_0 ===> k_24_19
k_23_1 in symmetric relation [k_23_1, k_24_20] are known: k_23_1 ===> k_24_20
k_23_2 in symmetric relation [k_23_2, k_24_21] are known: k_23_2 ===> k_24_21
k_23_3 in symmetric relation [k_23_3, k_24_22] are known: k_23_3 ===> k_24_22
k_23_4 in symmetric relation [k_23_4, k_24_23] are known: k_23_4 ===> k_24_23
k_24_57 in symmetric relation [k_24_57, k_25_76] are known: k_24_57 ===> k_25_76
k_24_58 in symmetric relation [k_24_58, k_25_77] are known: k_24_58 ===> k_25_77
k_24_59 in symmetric relation [k_24_59, k_25_78] are known: k_24_59 ===> k_25_78
k_24_60 in symmetric relation [k_24_60, k_25_79] are known: k_24_60 ===> k_25_79
k_14_61, k_14_62, k_14_63, k_14_64 in implication relation [k_14_61, k_14_62, k_14_63, k_14_64, k_15_0] are known: k_14_61, k_14_62, k_14_63, k_14_64 ===> k_15_0
k_14_61, k_14_62, k_14_63, k_14_64 in implication relation [k_14_61, k_14_62, k_14_63, k_14_64, k_15_1] are known: k_14_61, k_14_62, k_14_63, k_14_64 ===> k_15_1
k_14_61, k_14_62, k_14_63, k_14_64 in implication relation [k_14_61, k_14_62, k_14_63, k_14_64, k_15_2] are known: k_14_61, k_14_62, k_14_63, k_14_64 ===> k_15_2
k_14_61, k_14_62, k_14_63, k_14_64 in implication relation [k_14_61, k_14_62, k_14_63, k_14_64, k_15_3] are known: k_14_61, k_14_62, k_14_63, k_14_64 ===> k_15_3
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_61] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_61
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_62] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_62
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_63] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_63
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_64] are known: k_16_0, k_16_1, k_16_2, k_16_3 ===> k_15_64
############################################################
State 11:
k_1_39 in symmetric relation [k_0_20, k_1_39] are known: k_1_39 ===> k_0_20
k_3_59 in symmetric relation [k_2_40, k_3_59] are known: k_3_59 ===> k_2_40
k_5_18 in symmetric relation [k_4_79, k_5_18] are known: k_5_18 ===> k_4_79
k_5_40 in symmetric relation [k_4_21, k_5_40] are known: k_5_40 ===> k_4_21
k_6_78 in symmetric relation [k_5_59, k_6_78] are known: k_6_78 ===> k_5_59
k_7_19 in symmetric relation [k_6_0, k_7_19] are known: k_7_19 ===> k_6_0
k_7_76 in symmetric relation [k_6_57, k_7_76] are known: k_7_76 ===> k_6_57
k_9_12 in symmetric relation [k_8_73, k_9_12] are known: k_9_12 ===> k_8_73
k_9_15 in symmetric relation [k_8_76, k_9_15] are known: k_9_15 ===> k_8_76
k_11_76 in symmetric relation [k_10_57, k_11_76] are known: k_11_76 ===> k_10_57
k_11_71 in symmetric relation [k_11_71, k_12_10] are known: k_11_71 ===> k_12_10
k_12_14 in symmetric relation [k_11_75, k_12_14] are known: k_12_14 ===> k_11_75
k_12_18 in symmetric relation [k_11_79, k_12_18] are known: k_12_18 ===> k_11_79
k_13_13 in symmetric relation [k_12_74, k_13_13] are known: k_13_13 ===> k_12_74
k_13_55 in symmetric relation [k_12_36, k_13_55] are known: k_13_55 ===> k_12_36
k_13_60 in symmetric relation [k_12_41, k_13_60] are known: k_13_60 ===> k_12_41
k_14_65 in symmetric relation [k_13_46, k_14_65] are known: k_14_65 ===> k_13_46
k_14_66 in symmetric relation [k_13_47, k_14_66] are known: k_14_66 ===> k_13_47
k_14_67 in symmetric relation [k_13_48, k_14_67] are known: k_14_67 ===> k_13_48
k_14_68 in symmetric relation [k_13_49, k_14_68] are known: k_14_68 ===> k_13_49
k_15_14 in symmetric relation [k_14_75, k_15_14] are known: k_15_14 ===> k_14_75
k_15_39 in symmetric relation [k_14_20, k_15_39] are known: k_15_39 ===> k_14_20
k_15_60 in symmetric relation [k_14_41, k_15_60] are known: k_15_60 ===> k_14_41
k_15_61 in symmetric relation [k_14_42, k_15_61] are known: k_15_61 ===> k_14_42
k_15_62 in symmetric relation [k_14_43, k_15_62] are known: k_15_62 ===> k_14_43
k_15_63 in symmetric relation [k_14_44, k_15_63] are known: k_15_63 ===> k_14_44
k_15_64 in symmetric relation [k_14_45, k_15_64] are known: k_15_64 ===> k_14_45
k_15_73 in symmetric relation [k_14_54, k_15_73] are known: k_15_73 ===> k_14_54
k_15_74 in symmetric relation [k_14_55, k_15_74] are known: k_15_74 ===> k_14_55
k_15_76 in symmetric relation [k_14_57, k_15_76] are known: k_15_76 ===> k_14_57
k_15_66 in symmetric relation [k_15_66, k_16_5] are known: k_15_66 ===> k_16_5
k_15_69 in symmetric relation [k_15_69, k_16_8] are known: k_15_69 ===> k_16_8
k_15_0 in symmetric relation [k_15_0, k_16_19] are known: k_15_0 ===> k_16_19
k_15_1 in symmetric relation [k_15_1, k_16_20] are known: k_15_1 ===> k_16_20
k_15_2 in symmetric relation [k_15_2, k_16_21] are known: k_15_2 ===> k_16_21
k_15_3 in symmetric relation [k_15_3, k_16_22] are known: k_15_3 ===> k_16_22
k_18_27 in symmetric relation [k_18_27, k_19_46] are known: k_18_27 ===> k_19_46
k_19_51 in symmetric relation [k_19_51, k_20_70] are known: k_19_51 ===> k_20_70
k_20_52 in symmetric relation [k_20_52, k_21_71] are known: k_20_52 ===> k_21_71
k_23_71 in symmetric relation [k_23_71, k_24_10] are known: k_23_71 ===> k_24_10
k_24_19 in symmetric relation [k_24_19, k_25_38] are known: k_24_19 ===> k_25_38
k_24_20 in symmetric relation [k_24_20, k_25_39] are known: k_24_20 ===> k_25_39
k_24_21 in symmetric relation [k_24_21, k_25_40] are known: k_24_21 ===> k_25_40
k_24_22 in symmetric relation [k_24_22, k_25_41] are known: k_24_22 ===> k_25_41
k_24_23 in symmetric relation [k_24_23, k_25_42] are known: k_24_23 ===> k_25_42
k_25_76 in symmetric relation [k_25_76, k_26_15] are known: k_25_76 ===> k_26_15
k_25_77 in symmetric relation [k_25_77, k_26_16] are known: k_25_77 ===> k_26_16
k_25_78 in symmetric relation [k_25_78, k_26_17] are known: k_25_78 ===> k_26_17
k_25_79 in symmetric relation [k_25_79, k_26_18] are known: k_25_79 ===> k_26_18
############################################################
State 12:
k_2_40 in symmetric relation [k_1_21, k_2_40] are known: k_2_40 ===> k_1_21
k_4_21 in symmetric relation [k_3_2, k_4_21] are known: k_4_21 ===> k_3_2
k_4_79 in symmetric relation [k_3_60, k_4_79] are known: k_4_79 ===> k_3_60
k_5_59 in symmetric relation [k_4_40, k_5_59] are known: k_5_59 ===> k_4_40
k_6_57 in symmetric relation [k_5_38, k_6_57] are known: k_6_57 ===> k_5_38
k_8_73 in symmetric relation [k_7_54, k_8_73] are known: k_8_73 ===> k_7_54
k_8_76 in symmetric relation [k_7_57, k_8_76] are known: k_8_76 ===> k_7_57
k_10_57 in symmetric relation [k_9_38, k_10_57] are known: k_10_57 ===> k_9_38
k_11_75 in symmetric relation [k_10_56, k_11_75] are known: k_11_75 ===> k_10_56
k_11_79 in symmetric relation [k_10_60, k_11_79] are known: k_11_79 ===> k_10_60
k_12_36 in symmetric relation [k_11_17, k_12_36] are known: k_12_36 ===> k_11_17
k_12_41 in symmetric relation [k_11_22, k_12_41] are known: k_12_41 ===> k_11_22
k_12_74 in symmetric relation [k_11_55, k_12_74] are known: k_12_74 ===> k_11_55
k_12_10 in symmetric relation [k_12_10, k_13_29] are known: k_12_10 ===> k_13_29
k_13_46 in symmetric relation [k_12_27, k_13_46] are known: k_13_46 ===> k_12_27
k_13_47 in symmetric relation [k_12_28, k_13_47] are known: k_13_47 ===> k_12_28
k_13_48 in symmetric relation [k_12_29, k_13_48] are known: k_13_48 ===> k_12_29
k_13_49 in symmetric relation [k_12_30, k_13_49] are known: k_13_49 ===> k_12_30
k_14_20 in symmetric relation [k_13_1, k_14_20] are known: k_14_20 ===> k_13_1
k_14_41 in symmetric relation [k_13_22, k_14_41] are known: k_14_41 ===> k_13_22
k_14_42 in symmetric relation [k_13_23, k_14_42] are known: k_14_42 ===> k_13_23
k_14_43 in symmetric relation [k_13_24, k_14_43] are known: k_14_43 ===> k_13_24
k_14_44 in symmetric relation [k_13_25, k_14_44] are known: k_14_44 ===> k_13_25
k_14_45 in symmetric relation [k_13_26, k_14_45] are known: k_14_45 ===> k_13_26
k_14_54 in symmetric relation [k_13_35, k_14_54] are known: k_14_54 ===> k_13_35
k_14_55 in symmetric relation [k_13_36, k_14_55] are known: k_14_55 ===> k_13_36
k_14_57 in symmetric relation [k_13_38, k_14_57] are known: k_14_57 ===> k_13_38
k_14_75 in symmetric relation [k_13_56, k_14_75] are known: k_14_75 ===> k_13_56
k_16_5 in symmetric relation [k_16_5, k_17_24] are known: k_16_5 ===> k_17_24
k_16_8 in symmetric relation [k_16_8, k_17_27] are known: k_16_8 ===> k_17_27
k_16_19 in symmetric relation [k_16_19, k_17_38] are known: k_16_19 ===> k_17_38
k_16_20 in symmetric relation [k_16_20, k_17_39] are known: k_16_20 ===> k_17_39
k_16_21 in symmetric relation [k_16_21, k_17_40] are known: k_16_21 ===> k_17_40
k_16_22 in symmetric relation [k_16_22, k_17_41] are known: k_16_22 ===> k_17_41
k_19_46 in symmetric relation [k_19_46, k_20_65] are known: k_19_46 ===> k_20_65
k_20_70 in symmetric relation [k_20_70, k_21_9] are known: k_20_70 ===> k_21_9
k_21_71 in symmetric relation [k_21_71, k_22_10] are known: k_21_71 ===> k_22_10
k_24_10 in symmetric relation [k_24_10, k_25_29] are known: k_24_10 ===> k_25_29
k_25_38 in symmetric relation [k_25_38, k_26_57] are known: k_25_38 ===> k_26_57
k_25_39 in symmetric relation [k_25_39, k_26_58] are known: k_25_39 ===> k_26_58
k_25_40 in symmetric relation [k_25_40, k_26_59] are known: k_25_40 ===> k_26_59
k_25_41 in symmetric relation [k_25_41, k_26_60] are known: k_25_41 ===> k_26_60
k_25_42 in symmetric relation [k_25_42, k_26_61] are known: k_25_42 ===> k_26_61
############################################################
State 13:
k_1_21 in symmetric relation [k_0_2, k_1_21] are known: k_1_21 ===> k_0_2
k_3_60 in symmetric relation [k_2_41, k_3_60] are known: k_3_60 ===> k_2_41
k_4_40 in symmetric relation [k_3_21, k_4_40] are known: k_4_40 ===> k_3_21
k_5_38 in symmetric relation [k_4_19, k_5_38] are known: k_5_38 ===> k_4_19
k_7_54 in symmetric relation [k_6_35, k_7_54] are known: k_7_54 ===> k_6_35
k_7_57 in symmetric relation [k_6_38, k_7_57] are known: k_7_57 ===> k_6_38
k_9_38 in symmetric relation [k_8_19, k_9_38] are known: k_9_38 ===> k_8_19
k_10_56 in symmetric relation [k_9_37, k_10_56] are known: k_10_56 ===> k_9_37
k_10_60 in symmetric relation [k_9_41, k_10_60] are known: k_10_60 ===> k_9_41
k_11_17 in symmetric relation [k_10_78, k_11_17] are known: k_11_17 ===> k_10_78
k_11_22 in symmetric relation [k_10_3, k_11_22] are known: k_11_22 ===> k_10_3
k_11_55 in symmetric relation [k_10_36, k_11_55] are known: k_11_55 ===> k_10_36
k_12_27 in symmetric relation [k_11_8, k_12_27] are known: k_12_27 ===> k_11_8
k_12_28 in symmetric relation [k_11_9, k_12_28] are known: k_12_28 ===> k_11_9
k_12_29 in symmetric relation [k_11_10, k_12_29] are known: k_12_29 ===> k_11_10
k_12_30 in symmetric relation [k_11_11, k_12_30] are known: k_12_30 ===> k_11_11
k_13_22 in symmetric relation [k_12_3, k_13_22] are known: k_13_22 ===> k_12_3
k_13_23 in symmetric relation [k_12_4, k_13_23] are known: k_13_23 ===> k_12_4
k_13_24 in symmetric relation [k_12_5, k_13_24] are known: k_13_24 ===> k_12_5
k_13_25 in symmetric relation [k_12_6, k_13_25] are known: k_13_25 ===> k_12_6
k_13_26 in symmetric relation [k_12_7, k_13_26] are known: k_13_26 ===> k_12_7
k_13_35 in symmetric relation [k_12_16, k_13_35] are known: k_13_35 ===> k_12_16
k_13_36 in symmetric relation [k_12_17, k_13_36] are known: k_13_36 ===> k_12_17
k_13_38 in symmetric relation [k_12_19, k_13_38] are known: k_13_38 ===> k_12_19
k_13_56 in symmetric relation [k_12_37, k_13_56] are known: k_13_56 ===> k_12_37
k_13_29 in symmetric relation [k_13_29, k_14_48] are known: k_13_29 ===> k_14_48
k_17_24 in symmetric relation [k_17_24, k_18_43] are known: k_17_24 ===> k_18_43
k_17_27 in symmetric relation [k_17_27, k_18_46] are known: k_17_27 ===> k_18_46
k_17_38 in symmetric relation [k_17_38, k_18_57] are known: k_17_38 ===> k_18_57
k_17_39 in symmetric relation [k_17_39, k_18_58] are known: k_17_39 ===> k_18_58
k_17_40 in symmetric relation [k_17_40, k_18_59] are known: k_17_40 ===> k_18_59
k_17_41 in symmetric relation [k_17_41, k_18_60] are known: k_17_41 ===> k_18_60
k_20_65 in symmetric relation [k_20_65, k_21_4] are known: k_20_65 ===> k_21_4
k_21_9 in symmetric relation [k_21_9, k_22_28] are known: k_21_9 ===> k_22_28
k_22_10 in symmetric relation [k_22_10, k_23_29] are known: k_22_10 ===> k_23_29
k_25_29 in symmetric relation [k_25_29, k_26_48] are known: k_25_29 ===> k_26_48
############################################################
State 14:
k_2_41 in symmetric relation [k_1_22, k_2_41] are known: k_2_41 ===> k_1_22
k_3_21 in symmetric relation [k_2_2, k_3_21] are known: k_3_21 ===> k_2_2
k_4_19 in symmetric relation [k_3_0, k_4_19] are known: k_4_19 ===> k_3_0
k_6_35 in symmetric relation [k_5_16, k_6_35] are known: k_6_35 ===> k_5_16
k_6_38 in symmetric relation [k_5_19, k_6_38] are known: k_6_38 ===> k_5_19
k_8_19 in symmetric relation [k_7_0, k_8_19] are known: k_8_19 ===> k_7_0
k_9_37 in symmetric relation [k_8_18, k_9_37] are known: k_9_37 ===> k_8_18
k_9_41 in symmetric relation [k_8_22, k_9_41] are known: k_9_41 ===> k_8_22
k_10_36 in symmetric relation [k_9_17, k_10_36] are known: k_10_36 ===> k_9_17
k_10_78 in symmetric relation [k_9_59, k_10_78] are known: k_10_78 ===> k_9_59
k_11_8 in symmetric relation [k_10_69, k_11_8] are known: k_11_8 ===> k_10_69
k_11_9 in symmetric relation [k_10_70, k_11_9] are known: k_11_9 ===> k_10_70
k_11_10 in symmetric relation [k_10_71, k_11_10] are known: k_11_10 ===> k_10_71
k_11_11 in symmetric relation [k_10_72, k_11_11] are known: k_11_11 ===> k_10_72
k_12_4 in symmetric relation [k_11_65, k_12_4] are known: k_12_4 ===> k_11_65
k_12_5 in symmetric relation [k_11_66, k_12_5] are known: k_12_5 ===> k_11_66
k_12_6 in symmetric relation [k_11_67, k_12_6] are known: k_12_6 ===> k_11_67
k_12_7 in symmetric relation [k_11_68, k_12_7] are known: k_12_7 ===> k_11_68
k_12_16 in symmetric relation [k_11_77, k_12_16] are known: k_12_16 ===> k_11_77
k_12_17 in symmetric relation [k_11_78, k_12_17] are known: k_12_17 ===> k_11_78
k_12_19 in symmetric relation [k_11_0, k_12_19] are known: k_12_19 ===> k_11_0
k_12_37 in symmetric relation [k_11_18, k_12_37] are known: k_12_37 ===> k_11_18
k_14_48 in symmetric relation [k_14_48, k_15_67] are known: k_14_48 ===> k_15_67
k_18_43 in symmetric relation [k_18_43, k_19_62] are known: k_18_43 ===> k_19_62
k_18_46 in symmetric relation [k_18_46, k_19_65] are known: k_18_46 ===> k_19_65
k_18_57 in symmetric relation [k_18_57, k_19_76] are known: k_18_57 ===> k_19_76
k_18_58 in symmetric relation [k_18_58, k_19_77] are known: k_18_58 ===> k_19_77
k_18_59 in symmetric relation [k_18_59, k_19_78] are known: k_18_59 ===> k_19_78
k_18_60 in symmetric relation [k_18_60, k_19_79] are known: k_18_60 ===> k_19_79
k_21_4 in symmetric relation [k_21_4, k_22_23] are known: k_21_4 ===> k_22_23
k_22_28 in symmetric relation [k_22_28, k_23_47] are known: k_22_28 ===> k_23_47
k_23_29 in symmetric relation [k_23_29, k_24_48] are known: k_23_29 ===> k_24_48
k_12_0, k_12_1, k_12_2, k_12_3 in implication relation [k_12_0, k_12_1, k_12_2, k_12_3, k_11_61] are known: k_12_0, k_12_1, k_12_2, k_12_3 ===> k_11_61
k_12_0, k_12_1, k_12_2, k_12_3 in implication relation [k_12_0, k_12_1, k_12_2, k_12_3, k_11_62] are known: k_12_0, k_12_1, k_12_2, k_12_3 ===> k_11_62
k_12_0, k_12_1, k_12_2, k_12_3 in implication relation [k_12_0, k_12_1, k_12_2, k_12_3, k_11_63] are known: k_12_0, k_12_1, k_12_2, k_12_3 ===> k_11_63
k_12_0, k_12_1, k_12_2, k_12_3 in implication relation [k_12_0, k_12_1, k_12_2, k_12_3, k_11_64] are known: k_12_0, k_12_1, k_12_2, k_12_3 ===> k_11_64
############################################################
State 15:
k_1_22 in symmetric relation [k_0_3, k_1_22] are known: k_1_22 ===> k_0_3
k_5_16 in symmetric relation [k_4_77, k_5_16] are known: k_5_16 ===> k_4_77
k_5_19 in symmetric relation [k_4_0, k_5_19] are known: k_5_19 ===> k_4_0
k_8_18 in symmetric relation [k_7_79, k_8_18] are known: k_8_18 ===> k_7_79
k_8_22 in symmetric relation [k_7_3, k_8_22] are known: k_8_22 ===> k_7_3
k_9_17 in symmetric relation [k_8_78, k_9_17] are known: k_9_17 ===> k_8_78
k_9_59 in symmetric relation [k_8_40, k_9_59] are known: k_9_59 ===> k_8_40
k_10_69 in symmetric relation [k_9_50, k_10_69] are known: k_10_69 ===> k_9_50
k_10_70 in symmetric relation [k_9_51, k_10_70] are known: k_10_70 ===> k_9_51
k_10_71 in symmetric relation [k_9_52, k_10_71] are known: k_10_71 ===> k_9_52
k_10_72 in symmetric relation [k_9_53, k_10_72] are known: k_10_72 ===> k_9_53
k_11_18 in symmetric relation [k_10_79, k_11_18] are known: k_11_18 ===> k_10_79
k_11_61 in symmetric relation [k_10_42, k_11_61] are known: k_11_61 ===> k_10_42
k_11_62 in symmetric relation [k_10_43, k_11_62] are known: k_11_62 ===> k_10_43
k_11_63 in symmetric relation [k_10_44, k_11_63] are known: k_11_63 ===> k_10_44
k_11_64 in symmetric relation [k_10_45, k_11_64] are known: k_11_64 ===> k_10_45
k_11_65 in symmetric relation [k_10_46, k_11_65] are known: k_11_65 ===> k_10_46
k_11_66 in symmetric relation [k_10_47, k_11_66] are known: k_11_66 ===> k_10_47
k_11_67 in symmetric relation [k_10_48, k_11_67] are known: k_11_67 ===> k_10_48
k_11_68 in symmetric relation [k_10_49, k_11_68] are known: k_11_68 ===> k_10_49
k_11_77 in symmetric relation [k_10_58, k_11_77] are known: k_11_77 ===> k_10_58
k_11_78 in symmetric relation [k_10_59, k_11_78] are known: k_11_78 ===> k_10_59
k_15_67 in symmetric relation [k_15_67, k_16_6] are known: k_15_67 ===> k_16_6
k_19_65 in symmetric relation [k_19_65, k_20_4] are known: k_19_65 ===> k_20_4
k_19_76 in symmetric relation [k_19_76, k_20_15] are known: k_19_76 ===> k_20_15
k_19_77 in symmetric relation [k_19_77, k_20_16] are known: k_19_77 ===> k_20_16
k_19_78 in symmetric relation [k_19_78, k_20_17] are known: k_19_78 ===> k_20_17
k_19_79 in symmetric relation [k_19_79, k_20_18] are known: k_19_79 ===> k_20_18
k_22_23 in symmetric relation [k_22_23, k_23_42] are known: k_22_23 ===> k_23_42
k_23_47 in symmetric relation [k_23_47, k_24_66] are known: k_23_47 ===> k_24_66
k_24_48 in symmetric relation [k_24_48, k_25_67] are known: k_24_48 ===> k_25_67
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_61] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_61
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_62] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_62
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_63] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_63
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_64] are known: k_11_0, k_11_1, k_11_2, k_11_3 ===> k_10_64
############################################################
State 16:
k_4_77 in symmetric relation [k_3_58, k_4_77] are known: k_4_77 ===> k_3_58
k_7_79 in symmetric relation [k_6_60, k_7_79] are known: k_7_79 ===> k_6_60
k_8_40 in symmetric relation [k_7_21, k_8_40] are known: k_8_40 ===> k_7_21
k_8_78 in symmetric relation [k_7_59, k_8_78] are known: k_8_78 ===> k_7_59
k_9_50 in symmetric relation [k_8_31, k_9_50] are known: k_9_50 ===> k_8_31
k_9_51 in symmetric relation [k_8_32, k_9_51] are known: k_9_51 ===> k_8_32
k_9_52 in symmetric relation [k_8_33, k_9_52] are known: k_9_52 ===> k_8_33
k_9_53 in symmetric relation [k_8_34, k_9_53] are known: k_9_53 ===> k_8_34
k_10_42 in symmetric relation [k_9_23, k_10_42] are known: k_10_42 ===> k_9_23
k_10_43 in symmetric relation [k_9_24, k_10_43] are known: k_10_43 ===> k_9_24
k_10_44 in symmetric relation [k_9_25, k_10_44] are known: k_10_44 ===> k_9_25
k_10_45 in symmetric relation [k_9_26, k_10_45] are known: k_10_45 ===> k_9_26
k_10_46 in symmetric relation [k_9_27, k_10_46] are known: k_10_46 ===> k_9_27
k_10_47 in symmetric relation [k_9_28, k_10_47] are known: k_10_47 ===> k_9_28
k_10_48 in symmetric relation [k_9_29, k_10_48] are known: k_10_48 ===> k_9_29
k_10_49 in symmetric relation [k_9_30, k_10_49] are known: k_10_49 ===> k_9_30
k_10_58 in symmetric relation [k_9_39, k_10_58] are known: k_10_58 ===> k_9_39
k_10_59 in symmetric relation [k_9_40, k_10_59] are known: k_10_59 ===> k_9_40
k_10_61 in symmetric relation [k_9_42, k_10_61] are known: k_10_61 ===> k_9_42
k_10_62 in symmetric relation [k_9_43, k_10_62] are known: k_10_62 ===> k_9_43
k_10_63 in symmetric relation [k_9_44, k_10_63] are known: k_10_63 ===> k_9_44
k_10_64 in symmetric relation [k_9_45, k_10_64] are known: k_10_64 ===> k_9_45
k_10_79 in symmetric relation [k_9_60, k_10_79] are known: k_10_79 ===> k_9_60
k_16_6 in symmetric relation [k_16_6, k_17_25] are known: k_16_6 ===> k_17_25
k_20_4 in symmetric relation [k_20_4, k_21_23] are known: k_20_4 ===> k_21_23
k_20_15 in symmetric relation [k_20_15, k_21_34] are known: k_20_15 ===> k_21_34
k_20_16 in symmetric relation [k_20_16, k_21_35] are known: k_20_16 ===> k_21_35
k_20_17 in symmetric relation [k_20_17, k_21_36] are known: k_20_17 ===> k_21_36
k_20_18 in symmetric relation [k_20_18, k_21_37] are known: k_20_18 ===> k_21_37
k_23_42 in symmetric relation [k_23_42, k_24_61] are known: k_23_42 ===> k_24_61
k_24_66 in symmetric relation [k_24_66, k_25_5] are known: k_24_66 ===> k_25_5
k_25_67 in symmetric relation [k_25_67, k_26_6] are known: k_25_67 ===> k_26_6
############################################################
State 17:
k_3_58 in symmetric relation [k_2_39, k_3_58] are known: k_3_58 ===> k_2_39
k_6_60 in symmetric relation [k_5_41, k_6_60] are known: k_6_60 ===> k_5_41
k_7_21 in symmetric relation [k_6_2, k_7_21] are known: k_7_21 ===> k_6_2
k_7_59 in symmetric relation [k_6_40, k_7_59] are known: k_7_59 ===> k_6_40
k_8_31 in symmetric relation [k_7_12, k_8_31] are known: k_8_31 ===> k_7_12
k_8_32 in symmetric relation [k_7_13, k_8_32] are known: k_8_32 ===> k_7_13
k_8_33 in symmetric relation [k_7_14, k_8_33] are known: k_8_33 ===> k_7_14
k_8_34 in symmetric relation [k_7_15, k_8_34] are known: k_8_34 ===> k_7_15
k_9_23 in symmetric relation [k_8_4, k_9_23] are known: k_9_23 ===> k_8_4
k_9_24 in symmetric relation [k_8_5, k_9_24] are known: k_9_24 ===> k_8_5
k_9_25 in symmetric relation [k_8_6, k_9_25] are known: k_9_25 ===> k_8_6
k_9_26 in symmetric relation [k_8_7, k_9_26] are known: k_9_26 ===> k_8_7
k_9_27 in symmetric relation [k_8_8, k_9_27] are known: k_9_27 ===> k_8_8
k_9_28 in symmetric relation [k_8_9, k_9_28] are known: k_9_28 ===> k_8_9
k_9_29 in symmetric relation [k_8_10, k_9_29] are known: k_9_29 ===> k_8_10
k_9_30 in symmetric relation [k_8_11, k_9_30] are known: k_9_30 ===> k_8_11
k_9_39 in symmetric relation [k_8_20, k_9_39] are known: k_9_39 ===> k_8_20
k_9_40 in symmetric relation [k_8_21, k_9_40] are known: k_9_40 ===> k_8_21
k_9_42 in symmetric relation [k_8_23, k_9_42] are known: k_9_42 ===> k_8_23
k_9_43 in symmetric relation [k_8_24, k_9_43] are known: k_9_43 ===> k_8_24
k_9_44 in symmetric relation [k_8_25, k_9_44] are known: k_9_44 ===> k_8_25
k_9_45 in symmetric relation [k_8_26, k_9_45] are known: k_9_45 ===> k_8_26
k_9_60 in symmetric relation [k_8_41, k_9_60] are known: k_9_60 ===> k_8_41
k_17_25 in symmetric relation [k_17_25, k_18_44] are known: k_17_25 ===> k_18_44
k_21_23 in symmetric relation [k_21_23, k_22_42] are known: k_21_23 ===> k_22_42
k_21_34 in symmetric relation [k_21_34, k_22_53] are known: k_21_34 ===> k_22_53
k_21_35 in symmetric relation [k_21_35, k_22_54] are known: k_21_35 ===> k_22_54
k_21_36 in symmetric relation [k_21_36, k_22_55] are known: k_21_36 ===> k_22_55
k_21_37 in symmetric relation [k_21_37, k_22_56] are known: k_21_37 ===> k_22_56
k_25_5 in symmetric relation [k_25_5, k_26_24] are known: k_25_5 ===> k_26_24
k_24_61, k_24_62, k_24_63, k_24_64 in implication relation [k_24_61, k_24_62, k_24_63, k_24_64, k_25_0] are known: k_24_61, k_24_62, k_24_63, k_24_64 ===> k_25_0
k_24_61, k_24_62, k_24_63, k_24_64 in implication relation [k_24_61, k_24_62, k_24_63, k_24_64, k_25_1] are known: k_24_61, k_24_62, k_24_63, k_24_64 ===> k_25_1
k_24_61, k_24_62, k_24_63, k_24_64 in implication relation [k_24_61, k_24_62, k_24_63, k_24_64, k_25_2] are known: k_24_61, k_24_62, k_24_63, k_24_64 ===> k_25_2
k_24_61, k_24_62, k_24_63, k_24_64 in implication relation [k_24_61, k_24_62, k_24_63, k_24_64, k_25_3] are known: k_24_61, k_24_62, k_24_63, k_24_64 ===> k_25_3
############################################################
State 18:
k_2_39 in symmetric relation [k_1_20, k_2_39] are known: k_2_39 ===> k_1_20
k_5_41 in symmetric relation [k_4_22, k_5_41] are known: k_5_41 ===> k_4_22
k_6_40 in symmetric relation [k_5_21, k_6_40] are known: k_6_40 ===> k_5_21
k_7_12 in symmetric relation [k_6_73, k_7_12] are known: k_7_12 ===> k_6_73
k_7_13 in symmetric relation [k_6_74, k_7_13] are known: k_7_13 ===> k_6_74
k_7_14 in symmetric relation [k_6_75, k_7_14] are known: k_7_14 ===> k_6_75
k_7_15 in symmetric relation [k_6_76, k_7_15] are known: k_7_15 ===> k_6_76
k_8_4 in symmetric relation [k_7_65, k_8_4] are known: k_8_4 ===> k_7_65
k_8_5 in symmetric relation [k_7_66, k_8_5] are known: k_8_5 ===> k_7_66
k_8_6 in symmetric relation [k_7_67, k_8_6] are known: k_8_6 ===> k_7_67
k_8_7 in symmetric relation [k_7_68, k_8_7] are known: k_8_7 ===> k_7_68
k_8_8 in symmetric relation [k_7_69, k_8_8] are known: k_8_8 ===> k_7_69
k_8_9 in symmetric relation [k_7_70, k_8_9] are known: k_8_9 ===> k_7_70
k_8_10 in symmetric relation [k_7_71, k_8_10] are known: k_8_10 ===> k_7_71
k_8_11 in symmetric relation [k_7_72, k_8_11] are known: k_8_11 ===> k_7_72
k_8_20 in symmetric relation [k_7_1, k_8_20] are known: k_8_20 ===> k_7_1
k_8_21 in symmetric relation [k_7_2, k_8_21] are known: k_8_21 ===> k_7_2
k_8_23 in symmetric relation [k_7_4, k_8_23] are known: k_8_23 ===> k_7_4
k_8_24 in symmetric relation [k_7_5, k_8_24] are known: k_8_24 ===> k_7_5
k_8_25 in symmetric relation [k_7_6, k_8_25] are known: k_8_25 ===> k_7_6
k_8_26 in symmetric relation [k_7_7, k_8_26] are known: k_8_26 ===> k_7_7
k_8_41 in symmetric relation [k_7_22, k_8_41] are known: k_8_41 ===> k_7_22
k_18_44 in symmetric relation [k_18_44, k_19_63] are known: k_18_44 ===> k_19_63
k_22_42 in symmetric relation [k_22_42, k_23_61] are known: k_22_42 ===> k_23_61
k_22_53 in symmetric relation [k_22_53, k_23_72] are known: k_22_53 ===> k_23_72
k_22_54 in symmetric relation [k_22_54, k_23_73] are known: k_22_54 ===> k_23_73
k_22_55 in symmetric relation [k_22_55, k_23_74] are known: k_22_55 ===> k_23_74
k_22_56 in symmetric relation [k_22_56, k_23_75] are known: k_22_56 ===> k_23_75
k_25_0 in symmetric relation [k_25_0, k_26_19] are known: k_25_0 ===> k_26_19
k_25_1 in symmetric relation [k_25_1, k_26_20] are known: k_25_1 ===> k_26_20
k_25_2 in symmetric relation [k_25_2, k_26_21] are known: k_25_2 ===> k_26_21
k_25_3 in symmetric relation [k_25_3, k_26_22] are known: k_25_3 ===> k_26_22
############################################################
State 19:
k_1_20 in symmetric relation [k_0_1, k_1_20] are known: k_1_20 ===> k_0_1
k_4_22 in symmetric relation [k_3_3, k_4_22] are known: k_4_22 ===> k_3_3
k_5_21 in symmetric relation [k_4_2, k_5_21] are known: k_5_21 ===> k_4_2
k_6_73 in symmetric relation [k_5_54, k_6_73] are known: k_6_73 ===> k_5_54
k_6_74 in symmetric relation [k_5_55, k_6_74] are known: k_6_74 ===> k_5_55
k_6_75 in symmetric relation [k_5_56, k_6_75] are known: k_6_75 ===> k_5_56
k_6_76 in symmetric relation [k_5_57, k_6_76] are known: k_6_76 ===> k_5_57
k_7_4 in symmetric relation [k_6_65, k_7_4] are known: k_7_4 ===> k_6_65
k_7_5 in symmetric relation [k_6_66, k_7_5] are known: k_7_5 ===> k_6_66
k_7_6 in symmetric relation [k_6_67, k_7_6] are known: k_7_6 ===> k_6_67
k_7_7 in symmetric relation [k_6_68, k_7_7] are known: k_7_7 ===> k_6_68
k_7_22 in symmetric relation [k_6_3, k_7_22] are known: k_7_22 ===> k_6_3
k_7_65 in symmetric relation [k_6_46, k_7_65] are known: k_7_65 ===> k_6_46
k_7_66 in symmetric relation [k_6_47, k_7_66] are known: k_7_66 ===> k_6_47
k_7_67 in symmetric relation [k_6_48, k_7_67] are known: k_7_67 ===> k_6_48
k_7_68 in symmetric relation [k_6_49, k_7_68] are known: k_7_68 ===> k_6_49
k_7_69 in symmetric relation [k_6_50, k_7_69] are known: k_7_69 ===> k_6_50
k_7_70 in symmetric relation [k_6_51, k_7_70] are known: k_7_70 ===> k_6_51
k_7_71 in symmetric relation [k_6_52, k_7_71] are known: k_7_71 ===> k_6_52
k_7_72 in symmetric relation [k_6_53, k_7_72] are known: k_7_72 ===> k_6_53
k_23_72 in symmetric relation [k_23_72, k_24_11] are known: k_23_72 ===> k_24_11
k_23_73 in symmetric relation [k_23_73, k_24_12] are known: k_23_73 ===> k_24_12
k_23_74 in symmetric relation [k_23_74, k_24_13] are known: k_23_74 ===> k_24_13
k_23_75 in symmetric relation [k_23_75, k_24_14] are known: k_23_75 ===> k_24_14
k_7_0, k_7_1, k_7_2, k_7_3 in implication relation [k_7_0, k_7_1, k_7_2, k_7_3, k_6_61] are known: k_7_0, k_7_1, k_7_2, k_7_3 ===> k_6_61
k_7_0, k_7_1, k_7_2, k_7_3 in implication relation [k_7_0, k_7_1, k_7_2, k_7_3, k_6_62] are known: k_7_0, k_7_1, k_7_2, k_7_3 ===> k_6_62
k_7_0, k_7_1, k_7_2, k_7_3 in implication relation [k_7_0, k_7_1, k_7_2, k_7_3, k_6_63] are known: k_7_0, k_7_1, k_7_2, k_7_3 ===> k_6_63
k_7_0, k_7_1, k_7_2, k_7_3 in implication relation [k_7_0, k_7_1, k_7_2, k_7_3, k_6_64] are known: k_7_0, k_7_1, k_7_2, k_7_3 ===> k_6_64
k_19_61, k_19_62, k_19_63, k_19_64 in implication relation [k_19_61, k_19_62, k_19_63, k_19_64, k_20_0] are known: k_19_61, k_19_62, k_19_63, k_19_64 ===> k_20_0
k_19_61, k_19_62, k_19_63, k_19_64 in implication relation [k_19_61, k_19_62, k_19_63, k_19_64, k_20_1] are known: k_19_61, k_19_62, k_19_63, k_19_64 ===> k_20_1
k_19_61, k_19_62, k_19_63, k_19_64 in implication relation [k_19_61, k_19_62, k_19_63, k_19_64, k_20_2] are known: k_19_61, k_19_62, k_19_63, k_19_64 ===> k_20_2
k_19_61, k_19_62, k_19_63, k_19_64 in implication relation [k_19_61, k_19_62, k_19_63, k_19_64, k_20_3] are known: k_19_61, k_19_62, k_19_63, k_19_64 ===> k_20_3
k_23_61, k_23_62, k_23_63, k_23_64 in implication relation [k_23_61, k_23_62, k_23_63, k_23_64, k_24_0] are known: k_23_61, k_23_62, k_23_63, k_23_64 ===> k_24_0
k_23_61, k_23_62, k_23_63, k_23_64 in implication relation [k_23_61, k_23_62, k_23_63, k_23_64, k_24_1] are known: k_23_61, k_23_62, k_23_63, k_23_64 ===> k_24_1
k_23_61, k_23_62, k_23_63, k_23_64 in implication relation [k_23_61, k_23_62, k_23_63, k_23_64, k_24_2] are known: k_23_61, k_23_62, k_23_63, k_23_64 ===> k_24_2
k_23_61, k_23_62, k_23_63, k_23_64 in implication relation [k_23_61, k_23_62, k_23_63, k_23_64, k_24_3] are known: k_23_61, k_23_62, k_23_63, k_23_64 ===> k_24_3
############################################################
State 20:
k_5_54 in symmetric relation [k_4_35, k_5_54] are known: k_5_54 ===> k_4_35
k_5_55 in symmetric relation [k_4_36, k_5_55] are known: k_5_55 ===> k_4_36
k_5_56 in symmetric relation [k_4_37, k_5_56] are known: k_5_56 ===> k_4_37
k_5_57 in symmetric relation [k_4_38, k_5_57] are known: k_5_57 ===> k_4_38
k_6_46 in symmetric relation [k_5_27, k_6_46] are known: k_6_46 ===> k_5_27
k_6_47 in symmetric relation [k_5_28, k_6_47] are known: k_6_47 ===> k_5_28
k_6_48 in symmetric relation [k_5_29, k_6_48] are known: k_6_48 ===> k_5_29
k_6_49 in symmetric relation [k_5_30, k_6_49] are known: k_6_49 ===> k_5_30
k_6_50 in symmetric relation [k_5_31, k_6_50] are known: k_6_50 ===> k_5_31
k_6_51 in symmetric relation [k_5_32, k_6_51] are known: k_6_51 ===> k_5_32
k_6_52 in symmetric relation [k_5_33, k_6_52] are known: k_6_52 ===> k_5_33
k_6_53 in symmetric relation [k_5_34, k_6_53] are known: k_6_53 ===> k_5_34
k_6_61 in symmetric relation [k_5_42, k_6_61] are known: k_6_61 ===> k_5_42
k_6_62 in symmetric relation [k_5_43, k_6_62] are known: k_6_62 ===> k_5_43
k_6_63 in symmetric relation [k_5_44, k_6_63] are known: k_6_63 ===> k_5_44
k_6_64 in symmetric relation [k_5_45, k_6_64] are known: k_6_64 ===> k_5_45
k_6_65 in symmetric relation [k_5_46, k_6_65] are known: k_6_65 ===> k_5_46
k_6_66 in symmetric relation [k_5_47, k_6_66] are known: k_6_66 ===> k_5_47
k_6_67 in symmetric relation [k_5_48, k_6_67] are known: k_6_67 ===> k_5_48
k_6_68 in symmetric relation [k_5_49, k_6_68] are known: k_6_68 ===> k_5_49
k_20_0 in symmetric relation [k_20_0, k_21_19] are known: k_20_0 ===> k_21_19
k_20_1 in symmetric relation [k_20_1, k_21_20] are known: k_20_1 ===> k_21_20
k_20_2 in symmetric relation [k_20_2, k_21_21] are known: k_20_2 ===> k_21_21
k_20_3 in symmetric relation [k_20_3, k_21_22] are known: k_20_3 ===> k_21_22
k_24_0 in symmetric relation [k_24_0, k_25_19] are known: k_24_0 ===> k_25_19
k_24_1 in symmetric relation [k_24_1, k_25_20] are known: k_24_1 ===> k_25_20
k_24_2 in symmetric relation [k_24_2, k_25_21] are known: k_24_2 ===> k_25_21
k_24_3 in symmetric relation [k_24_3, k_25_22] are known: k_24_3 ===> k_25_22
k_24_11 in symmetric relation [k_24_11, k_25_30] are known: k_24_11 ===> k_25_30
k_24_12 in symmetric relation [k_24_12, k_25_31] are known: k_24_12 ===> k_25_31
k_24_13 in symmetric relation [k_24_13, k_25_32] are known: k_24_13 ===> k_25_32
k_24_14 in symmetric relation [k_24_14, k_25_33] are known: k_24_14 ===> k_25_33
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_61] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_61
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_62] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_62
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_63] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_63
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_64] are known: k_3_0, k_3_1, k_3_2, k_3_3 ===> k_2_64
k_4_0, k_4_1, k_4_2, k_4_3 in implication relation [k_4_0, k_4_1, k_4_2, k_4_3, k_3_61] are known: k_4_0, k_4_1, k_4_2, k_4_3 ===> k_3_61
k_4_0, k_4_1, k_4_2, k_4_3 in implication relation [k_4_0, k_4_1, k_4_2, k_4_3, k_3_62] are known: k_4_0, k_4_1, k_4_2, k_4_3 ===> k_3_62
k_4_0, k_4_1, k_4_2, k_4_3 in implication relation [k_4_0, k_4_1, k_4_2, k_4_3, k_3_63] are known: k_4_0, k_4_1, k_4_2, k_4_3 ===> k_3_63
k_4_0, k_4_1, k_4_2, k_4_3 in implication relation [k_4_0, k_4_1, k_4_2, k_4_3, k_3_64] are known: k_4_0, k_4_1, k_4_2, k_4_3 ===> k_3_64
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_61] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_61
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_62] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_62
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_63] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_63
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_64] are known: k_6_0, k_6_1, k_6_2, k_6_3 ===> k_5_64
############################################################
State 21:
k_2_61 in symmetric relation [k_1_42, k_2_61] are known: k_2_61 ===> k_1_42
k_2_62 in symmetric relation [k_1_43, k_2_62] are known: k_2_62 ===> k_1_43
k_2_63 in symmetric relation [k_1_44, k_2_63] are known: k_2_63 ===> k_1_44
k_2_64 in symmetric relation [k_1_45, k_2_64] are known: k_2_64 ===> k_1_45
k_3_61 in symmetric relation [k_2_42, k_3_61] are known: k_3_61 ===> k_2_42
k_3_62 in symmetric relation [k_2_43, k_3_62] are known: k_3_62 ===> k_2_43
k_3_63 in symmetric relation [k_2_44, k_3_63] are known: k_3_63 ===> k_2_44
k_3_64 in symmetric relation [k_2_45, k_3_64] are known: k_3_64 ===> k_2_45
k_4_35 in symmetric relation [k_3_16, k_4_35] are known: k_4_35 ===> k_3_16
k_4_36 in symmetric relation [k_3_17, k_4_36] are known: k_4_36 ===> k_3_17
k_4_37 in symmetric relation [k_3_18, k_4_37] are known: k_4_37 ===> k_3_18
k_4_38 in symmetric relation [k_3_19, k_4_38] are known: k_4_38 ===> k_3_19
k_5_27 in symmetric relation [k_4_8, k_5_27] are known: k_5_27 ===> k_4_8
k_5_28 in symmetric relation [k_4_9, k_5_28] are known: k_5_28 ===> k_4_9
k_5_29 in symmetric relation [k_4_10, k_5_29] are known: k_5_29 ===> k_4_10
k_5_30 in symmetric relation [k_4_11, k_5_30] are known: k_5_30 ===> k_4_11
k_5_31 in symmetric relation [k_4_12, k_5_31] are known: k_5_31 ===> k_4_12
k_5_32 in symmetric relation [k_4_13, k_5_32] are known: k_5_32 ===> k_4_13
k_5_33 in symmetric relation [k_4_14, k_5_33] are known: k_5_33 ===> k_4_14
k_5_34 in symmetric relation [k_4_15, k_5_34] are known: k_5_34 ===> k_4_15
k_5_42 in symmetric relation [k_4_23, k_5_42] are known: k_5_42 ===> k_4_23
k_5_43 in symmetric relation [k_4_24, k_5_43] are known: k_5_43 ===> k_4_24
k_5_44 in symmetric relation [k_4_25, k_5_44] are known: k_5_44 ===> k_4_25
k_5_45 in symmetric relation [k_4_26, k_5_45] are known: k_5_45 ===> k_4_26
k_5_46 in symmetric relation [k_4_27, k_5_46] are known: k_5_46 ===> k_4_27
k_5_47 in symmetric relation [k_4_28, k_5_47] are known: k_5_47 ===> k_4_28
k_5_48 in symmetric relation [k_4_29, k_5_48] are known: k_5_48 ===> k_4_29
k_5_49 in symmetric relation [k_4_30, k_5_49] are known: k_5_49 ===> k_4_30
k_5_61 in symmetric relation [k_4_42, k_5_61] are known: k_5_61 ===> k_4_42
k_5_62 in symmetric relation [k_4_43, k_5_62] are known: k_5_62 ===> k_4_43
k_5_63 in symmetric relation [k_4_44, k_5_63] are known: k_5_63 ===> k_4_44
k_5_64 in symmetric relation [k_4_45, k_5_64] are known: k_5_64 ===> k_4_45
k_21_19 in symmetric relation [k_21_19, k_22_38] are known: k_21_19 ===> k_22_38
k_21_20 in symmetric relation [k_21_20, k_22_39] are known: k_21_20 ===> k_22_39
k_21_21 in symmetric relation [k_21_21, k_22_40] are known: k_21_21 ===> k_22_40
k_21_22 in symmetric relation [k_21_22, k_22_41] are known: k_21_22 ===> k_22_41
k_25_19 in symmetric relation [k_25_19, k_26_38] are known: k_25_19 ===> k_26_38
k_25_20 in symmetric relation [k_25_20, k_26_39] are known: k_25_20 ===> k_26_39
k_25_21 in symmetric relation [k_25_21, k_26_40] are known: k_25_21 ===> k_26_40
k_25_22 in symmetric relation [k_25_22, k_26_41] are known: k_25_22 ===> k_26_41
k_25_30 in symmetric relation [k_25_30, k_26_49] are known: k_25_30 ===> k_26_49
k_25_31 in symmetric relation [k_25_31, k_26_50] are known: k_25_31 ===> k_26_50
k_25_32 in symmetric relation [k_25_32, k_26_51] are known: k_25_32 ===> k_26_51
k_25_33 in symmetric relation [k_25_33, k_26_52] are known: k_25_33 ===> k_26_52
############################################################
State 22:
k_1_42 in symmetric relation [k_0_23, k_1_42] are known: k_1_42 ===> k_0_23
k_1_43 in symmetric relation [k_0_24, k_1_43] are known: k_1_43 ===> k_0_24
k_1_44 in symmetric relation [k_0_25, k_1_44] are known: k_1_44 ===> k_0_25
k_1_45 in symmetric relation [k_0_26, k_1_45] are known: k_1_45 ===> k_0_26
k_2_42 in symmetric relation [k_1_23, k_2_42] are known: k_2_42 ===> k_1_23
k_2_43 in symmetric relation [k_1_24, k_2_43] are known: k_2_43 ===> k_1_24
k_2_44 in symmetric relation [k_1_25, k_2_44] are known: k_2_44 ===> k_1_25
k_2_45 in symmetric relation [k_1_26, k_2_45] are known: k_2_45 ===> k_1_26
k_3_16 in symmetric relation [k_2_77, k_3_16] are known: k_3_16 ===> k_2_77
k_3_17 in symmetric relation [k_2_78, k_3_17] are known: k_3_17 ===> k_2_78
k_3_18 in symmetric relation [k_2_79, k_3_18] are known: k_3_18 ===> k_2_79
k_3_19 in symmetric relation [k_2_0, k_3_19] are known: k_3_19 ===> k_2_0
k_4_8 in symmetric relation [k_3_69, k_4_8] are known: k_4_8 ===> k_3_69
k_4_9 in symmetric relation [k_3_70, k_4_9] are known: k_4_9 ===> k_3_70
k_4_10 in symmetric relation [k_3_71, k_4_10] are known: k_4_10 ===> k_3_71
k_4_11 in symmetric relation [k_3_72, k_4_11] are known: k_4_11 ===> k_3_72
k_4_12 in symmetric relation [k_3_73, k_4_12] are known: k_4_12 ===> k_3_73
k_4_13 in symmetric relation [k_3_74, k_4_13] are known: k_4_13 ===> k_3_74
k_4_14 in symmetric relation [k_3_75, k_4_14] are known: k_4_14 ===> k_3_75
k_4_15 in symmetric relation [k_3_76, k_4_15] are known: k_4_15 ===> k_3_76
k_4_23 in symmetric relation [k_3_4, k_4_23] are known: k_4_23 ===> k_3_4
k_4_24 in symmetric relation [k_3_5, k_4_24] are known: k_4_24 ===> k_3_5
k_4_25 in symmetric relation [k_3_6, k_4_25] are known: k_4_25 ===> k_3_6
k_4_26 in symmetric relation [k_3_7, k_4_26] are known: k_4_26 ===> k_3_7
k_4_27 in symmetric relation [k_3_8, k_4_27] are known: k_4_27 ===> k_3_8
k_4_28 in symmetric relation [k_3_9, k_4_28] are known: k_4_28 ===> k_3_9
k_4_29 in symmetric relation [k_3_10, k_4_29] are known: k_4_29 ===> k_3_10
k_4_30 in symmetric relation [k_3_11, k_4_30] are known: k_4_30 ===> k_3_11
k_4_42 in symmetric relation [k_3_23, k_4_42] are known: k_4_42 ===> k_3_23
k_4_43 in symmetric relation [k_3_24, k_4_43] are known: k_4_43 ===> k_3_24
k_4_44 in symmetric relation [k_3_25, k_4_44] are known: k_4_44 ===> k_3_25
k_4_45 in symmetric relation [k_3_26, k_4_45] are known: k_4_45 ===> k_3_26
k_22_38 in symmetric relation [k_22_38, k_23_57] are known: k_22_38 ===> k_23_57
k_22_39 in symmetric relation [k_22_39, k_23_58] are known: k_22_39 ===> k_23_58
k_22_40 in symmetric relation [k_22_40, k_23_59] are known: k_22_40 ===> k_23_59
k_22_41 in symmetric relation [k_22_41, k_23_60] are known: k_22_41 ===> k_23_60
############################################################
State 23:
k_1_23 in symmetric relation [k_0_4, k_1_23] are known: k_1_23 ===> k_0_4
k_1_24 in symmetric relation [k_0_5, k_1_24] are known: k_1_24 ===> k_0_5
k_1_25 in symmetric relation [k_0_6, k_1_25] are known: k_1_25 ===> k_0_6
k_1_26 in symmetric relation [k_0_7, k_1_26] are known: k_1_26 ===> k_0_7
k_2_77 in symmetric relation [k_1_58, k_2_77] are known: k_2_77 ===> k_1_58
k_2_78 in symmetric relation [k_1_59, k_2_78] are known: k_2_78 ===> k_1_59
k_2_79 in symmetric relation [k_1_60, k_2_79] are known: k_2_79 ===> k_1_60
k_3_4 in symmetric relation [k_2_65, k_3_4] are known: k_3_4 ===> k_2_65
k_3_5 in symmetric relation [k_2_66, k_3_5] are known: k_3_5 ===> k_2_66
k_3_6 in symmetric relation [k_2_67, k_3_6] are known: k_3_6 ===> k_2_67
k_3_7 in symmetric relation [k_2_68, k_3_7] are known: k_3_7 ===> k_2_68
k_3_8 in symmetric relation [k_2_69, k_3_8] are known: k_3_8 ===> k_2_69
k_3_9 in symmetric relation [k_2_70, k_3_9] are known: k_3_9 ===> k_2_70
k_3_10 in symmetric relation [k_2_71, k_3_10] are known: k_3_10 ===> k_2_71
k_3_11 in symmetric relation [k_2_72, k_3_11] are known: k_3_11 ===> k_2_72
k_3_23 in symmetric relation [k_2_4, k_3_23] are known: k_3_23 ===> k_2_4
k_3_24 in symmetric relation [k_2_5, k_3_24] are known: k_3_24 ===> k_2_5
k_3_25 in symmetric relation [k_2_6, k_3_25] are known: k_3_25 ===> k_2_6
k_3_26 in symmetric relation [k_2_7, k_3_26] are known: k_3_26 ===> k_2_7
k_3_69 in symmetric relation [k_2_50, k_3_69] are known: k_3_69 ===> k_2_50
k_3_70 in symmetric relation [k_2_51, k_3_70] are known: k_3_70 ===> k_2_51
k_3_71 in symmetric relation [k_2_52, k_3_71] are known: k_3_71 ===> k_2_52
k_3_72 in symmetric relation [k_2_53, k_3_72] are known: k_3_72 ===> k_2_53
k_3_73 in symmetric relation [k_2_54, k_3_73] are known: k_3_73 ===> k_2_54
k_3_74 in symmetric relation [k_2_55, k_3_74] are known: k_3_74 ===> k_2_55
k_3_75 in symmetric relation [k_2_56, k_3_75] are known: k_3_75 ===> k_2_56
k_3_76 in symmetric relation [k_2_57, k_3_76] are known: k_3_76 ===> k_2_57
k_23_57 in symmetric relation [k_23_57, k_24_76] are known: k_23_57 ===> k_24_76
k_23_58 in symmetric relation [k_23_58, k_24_77] are known: k_23_58 ===> k_24_77
k_23_59 in symmetric relation [k_23_59, k_24_78] are known: k_23_59 ===> k_24_78
k_23_60 in symmetric relation [k_23_60, k_24_79] are known: k_23_60 ===> k_24_79
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_61] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_61
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_62] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_62
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_63] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_63
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_64] are known: k_2_0, k_2_1, k_2_2, k_2_3 ===> k_1_64
############################################################
State 24:
k_1_58 in symmetric relation [k_0_39, k_1_58] are known: k_1_58 ===> k_0_39
k_1_59 in symmetric relation [k_0_40, k_1_59] are known: k_1_59 ===> k_0_40
k_1_60 in symmetric relation [k_0_41, k_1_60] are known: k_1_60 ===> k_0_41
k_1_61 in symmetric relation [k_0_42, k_1_61] are known: k_1_61 ===> k_0_42
k_1_62 in symmetric relation [k_0_43, k_1_62] are known: k_1_62 ===> k_0_43
k_1_63 in symmetric relation [k_0_44, k_1_63] are known: k_1_63 ===> k_0_44
k_1_64 in symmetric relation [k_0_45, k_1_64] are known: k_1_64 ===> k_0_45
k_2_4 in symmetric relation [k_1_65, k_2_4] are known: k_2_4 ===> k_1_65
k_2_5 in symmetric relation [k_1_66, k_2_5] are known: k_2_5 ===> k_1_66
k_2_6 in symmetric relation [k_1_67, k_2_6] are known: k_2_6 ===> k_1_67
k_2_7 in symmetric relation [k_1_68, k_2_7] are known: k_2_7 ===> k_1_68
k_2_50 in symmetric relation [k_1_31, k_2_50] are known: k_2_50 ===> k_1_31
k_2_51 in symmetric relation [k_1_32, k_2_51] are known: k_2_51 ===> k_1_32
k_2_52 in symmetric relation [k_1_33, k_2_52] are known: k_2_52 ===> k_1_33
k_2_53 in symmetric relation [k_1_34, k_2_53] are known: k_2_53 ===> k_1_34
k_2_54 in symmetric relation [k_1_35, k_2_54] are known: k_2_54 ===> k_1_35
k_2_55 in symmetric relation [k_1_36, k_2_55] are known: k_2_55 ===> k_1_36
k_2_56 in symmetric relation [k_1_37, k_2_56] are known: k_2_56 ===> k_1_37
k_2_57 in symmetric relation [k_1_38, k_2_57] are known: k_2_57 ===> k_1_38
k_2_65 in symmetric relation [k_1_46, k_2_65] are known: k_2_65 ===> k_1_46
k_2_66 in symmetric relation [k_1_47, k_2_66] are known: k_2_66 ===> k_1_47
k_2_67 in symmetric relation [k_1_48, k_2_67] are known: k_2_67 ===> k_1_48
k_2_68 in symmetric relation [k_1_49, k_2_68] are known: k_2_68 ===> k_1_49
k_2_69 in symmetric relation [k_1_50, k_2_69] are known: k_2_69 ===> k_1_50
k_2_70 in symmetric relation [k_1_51, k_2_70] are known: k_2_70 ===> k_1_51
k_2_71 in symmetric relation [k_1_52, k_2_71] are known: k_2_71 ===> k_1_52
k_2_72 in symmetric relation [k_1_53, k_2_72] are known: k_2_72 ===> k_1_53
k_24_76 in symmetric relation [k_24_76, k_25_15] are known: k_24_76 ===> k_25_15
k_24_77 in symmetric relation [k_24_77, k_25_16] are known: k_24_77 ===> k_25_16
k_24_78 in symmetric relation [k_24_78, k_25_17] are known: k_24_78 ===> k_25_17
k_24_79 in symmetric relation [k_24_79, k_25_18] are known: k_24_79 ===> k_25_18
############################################################
State 25:
k_1_31 in symmetric relation [k_0_12, k_1_31] are known: k_1_31 ===> k_0_12
k_1_32 in symmetric relation [k_0_13, k_1_32] are known: k_1_32 ===> k_0_13
k_1_33 in symmetric relation [k_0_14, k_1_33] are known: k_1_33 ===> k_0_14
k_1_34 in symmetric relation [k_0_15, k_1_34] are known: k_1_34 ===> k_0_15
k_1_35 in symmetric relation [k_0_16, k_1_35] are known: k_1_35 ===> k_0_16
k_1_36 in symmetric relation [k_0_17, k_1_36] are known: k_1_36 ===> k_0_17
k_1_37 in symmetric relation [k_0_18, k_1_37] are known: k_1_37 ===> k_0_18
k_1_38 in symmetric relation [k_0_19, k_1_38] are known: k_1_38 ===> k_0_19
k_1_46 in symmetric relation [k_0_27, k_1_46] are known: k_1_46 ===> k_0_27
k_1_47 in symmetric relation [k_0_28, k_1_47] are known: k_1_47 ===> k_0_28
k_1_48 in symmetric relation [k_0_29, k_1_48] are known: k_1_48 ===> k_0_29
k_1_49 in symmetric relation [k_0_30, k_1_49] are known: k_1_49 ===> k_0_30
k_1_50 in symmetric relation [k_0_31, k_1_50] are known: k_1_50 ===> k_0_31
k_1_51 in symmetric relation [k_0_32, k_1_51] are known: k_1_51 ===> k_0_32
k_1_52 in symmetric relation [k_0_33, k_1_52] are known: k_1_52 ===> k_0_33
k_1_53 in symmetric relation [k_0_34, k_1_53] are known: k_1_53 ===> k_0_34
k_1_65 in symmetric relation [k_0_46, k_1_65] are known: k_1_65 ===> k_0_46
k_1_66 in symmetric relation [k_0_47, k_1_66] are known: k_1_66 ===> k_0_47
k_1_67 in symmetric relation [k_0_48, k_1_67] are known: k_1_67 ===> k_0_48
k_1_68 in symmetric relation [k_0_49, k_1_68] are known: k_1_68 ===> k_0_49
k_25_15 in symmetric relation [k_25_15, k_26_34] are known: k_25_15 ===> k_26_34
k_25_16 in symmetric relation [k_25_16, k_26_35] are known: k_25_16 ===> k_26_35
k_25_17 in symmetric relation [k_25_17, k_26_36] are known: k_25_17 ===> k_26_36
k_25_18 in symmetric relation [k_25_18, k_26_37] are known: k_25_18 ===> k_26_37
############################################################
The following variables are known in final state:
k_0_1, k_1_20, k_0_2, k_1_21, k_0_3, k_1_22, k_0_4, k_1_23, k_0_5, k_1_24, k_0_6, k_1_25, k_0_7, k_1_26, k_0_8, k_1_27, k_0_12, k_1_31, k_0_13, k_1_32, k_0_14, k_1_33, k_0_15, k_1_34, k_0_16, k_1_35, k_0_17, k_1_36, k_0_18, k_1_37, k_0_19, k_1_38, k_0_20, k_1_39, k_0_21, k_1_40, k_0_22, k_1_41, k_0_23, k_1_42, k_0_24, k_1_43, k_0_25, k_1_44, k_0_26, k_1_45, k_0_27, k_1_46, k_0_28, k_1_47, k_0_29, k_1_48, k_0_30, k_1_49, k_0_31, k_1_50, k_0_32, k_1_51, k_0_33, k_1_52, k_0_34, k_1_53, k_0_35, k_1_54, k_0_36, k_1_55, k_0_37, k_1_56, k_0_38, k_1_57, k_0_39, k_1_58, k_0_40, k_1_59, k_0_41, k_1_60, k_0_42, k_1_61, k_0_43, k_1_62, k_0_44, k_1_63, k_0_45, k_1_64, k_0_46, k_1_65, k_0_47, k_1_66, k_0_48, k_1_67, k_0_49, k_1_68, 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_39, k_2_40, k_2_41, k_2_42, k_2_43, k_2_44, k_2_45, k_2_46, k_2_50, k_2_51, k_2_52, k_2_53, k_2_54, k_2_55, k_2_56, k_2_57, k_2_58, k_2_59, k_2_60, k_2_61, k_2_62, k_2_63, k_2_64, k_2_65, k_2_66, k_2_67, k_2_68, k_2_69, k_2_70, k_2_71, k_2_72, k_2_73, k_2_74, 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_22, k_3_23, k_3_24, k_3_25, k_3_26, 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_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_0, k_4_1, k_4_2, k_4_3, k_4_4, k_4_8, k_4_9, k_4_10, k_4_11, k_4_12, k_4_13, k_4_14, k_4_15, k_4_16, 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_77, k_4_78, k_4_79, 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_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_44, k_5_45, k_5_46, k_5_47, k_5_48, k_5_49, k_5_50, k_5_51, k_5_52, k_5_53, k_5_54, k_5_55, k_5_56, k_5_57, k_5_58, k_5_59, k_5_60, k_5_61, k_5_62, k_5_63, k_5_64, k_6_0, k_6_1, k_6_2, k_6_3, k_6_35, k_6_36, k_6_37, k_6_38, k_6_39, k_6_40, k_6_41, k_6_42, 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_0, k_7_1, k_7_2, k_7_3, k_7_4, k_7_5, k_7_6, k_7_7, k_7_8, k_7_9, 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_54, k_7_55, k_7_56, k_7_57, k_7_58, k_7_59, k_7_60, k_7_61, k_7_65, k_7_66, k_7_67, k_7_68, k_7_69, k_7_70, k_7_71, k_7_72, k_7_73, k_7_74, k_7_75, k_7_76, k_7_77, k_7_78, k_7_79, k_8_0, k_8_2, 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_37, k_8_38, k_8_39, k_8_40, k_8_41, k_8_73, k_8_74, k_8_75, k_8_76, k_8_77, k_8_78, k_8_79, k_9_1, k_9_3, k_9_12, k_9_13, k_9_14, k_9_15, k_9_16, k_9_17, k_9_18, k_9_19, k_9_21, k_9_23, k_9_24, k_9_25, k_9_26, k_9_27, k_9_28, k_9_29, k_9_30, k_9_31, 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_10_3, k_10_20, k_10_22, 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_40, 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_59, k_10_60, k_10_61, k_10_62, k_10_63, k_10_64, k_10_65, k_10_66, k_10_67, k_10_68, k_10_69, k_10_70, k_10_71, k_10_72, k_10_73, k_10_74, k_10_75, k_10_76, k_10_77, k_10_78, k_10_79, 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_22, k_11_39, k_11_41, k_11_50, k_11_51, k_11_52, k_11_53, k_11_54, k_11_55, k_11_56, k_11_57, k_11_59, 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_2, k_12_3, k_12_4, k_12_5, k_12_6, k_12_7, k_12_8, k_12_9, k_12_10, k_12_11, k_12_12, k_12_13, k_12_14, k_12_15, k_12_16, k_12_17, k_12_18, k_12_19, k_12_20, k_12_21, k_12_22, k_12_23, k_12_24, 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_41, k_12_58, k_12_60, 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_78, k_13_1, k_13_3, 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_17, 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_53, k_13_54, k_13_55, k_13_56, k_13_60, k_13_77, k_13_79, k_14_1, k_14_16, k_14_18, k_14_20, k_14_22, k_14_27, k_14_28, k_14_29, k_14_30, k_14_31, k_14_32, k_14_33, k_14_34, k_14_36, k_14_38, k_14_39, k_14_40, k_14_41, k_14_42, k_14_43, k_14_44, k_14_45, k_14_46, 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_79, k_15_0, k_15_1, k_15_2, k_15_3, k_15_4, k_15_5, k_15_6, k_15_7, k_15_8, k_15_9, k_15_10, k_15_11, k_15_12, k_15_13, k_15_14, k_15_18, k_15_20, k_15_35, k_15_37, k_15_39, k_15_41, 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_55, 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_75, k_15_76, 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_37, k_16_39, k_16_54, k_16_56, k_16_58, k_16_60, k_16_65, k_16_66, k_16_67, k_16_68, k_16_69, k_16_70, k_16_71, k_16_72, k_16_74, k_16_76, k_16_77, k_16_78, k_16_79, k_17_1, 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_13, k_17_15, k_17_16, k_17_17, k_17_18, k_17_19, k_17_20, k_17_21, k_17_22, k_17_23, k_17_24, k_17_25, k_17_26, k_17_27, k_17_28, k_17_29, k_17_30, k_17_31, k_17_32, k_17_33, k_17_34, k_17_35, k_17_36, k_17_37, k_17_38, k_17_39, 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_56, k_17_58, k_17_73, k_17_75, k_17_77, k_17_79, k_18_3, k_18_12, k_18_14, k_18_16, k_18_18, k_18_20, 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_32, 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_68, k_18_69, k_18_70, k_18_71, k_18_75, k_18_77, 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_14, k_19_16, k_19_22, k_19_31, k_19_33, k_19_35, k_19_37, k_19_39, k_19_41, k_19_42, k_19_43, k_19_44, k_19_45, k_19_46, k_19_47, k_19_48, k_19_49, k_19_51, k_19_53, k_19_54, k_19_55, k_19_56, k_19_57, k_19_58, k_19_59, k_19_60, k_19_61, 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_10, k_20_11, k_20_12, k_20_13, k_20_14, k_20_15, k_20_16, k_20_17, k_20_18, k_20_19, k_20_20, k_20_21, k_20_22, k_20_23, k_20_24, k_20_25, k_20_26, k_20_27, k_20_28, k_20_29, k_20_33, k_20_35, k_20_41, k_20_50, k_20_52, k_20_54, k_20_56, k_20_58, 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_70, 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_0, k_21_1, k_21_2, k_21_3, k_21_4, k_21_5, k_21_6, k_21_7, k_21_9, 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_52, k_21_54, k_21_60, k_21_69, k_21_71, k_21_73, k_21_75, k_21_77, k_21_79, k_22_1, k_22_8, k_22_10, k_22_12, k_22_14, k_22_16, 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_28, k_22_30, k_22_31, k_22_32, k_22_33, k_22_34, k_22_35, k_22_36, k_22_37, k_22_38, k_22_39, k_22_40, k_22_41, k_22_42, k_22_43, k_22_44, k_22_45, k_22_46, k_22_47, k_22_48, k_22_49, k_22_50, k_22_51, k_22_52, k_22_53, k_22_54, 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_71, k_22_73, k_22_79, k_23_0, k_23_1, k_23_2, k_23_3, k_23_4, k_23_5, k_23_6, k_23_10, k_23_12, k_23_18, k_23_20, k_23_27, k_23_29, k_23_31, k_23_33, k_23_35, k_23_37, k_23_38, k_23_39, k_23_40, k_23_41, k_23_42, k_23_43, k_23_44, k_23_45, k_23_47, k_23_49, k_23_50, k_23_51, k_23_52, k_23_53, k_23_54, k_23_55, k_23_56, k_23_57, k_23_58, k_23_59, k_23_60, k_23_61, k_23_62, k_23_63, k_23_64, k_23_65, k_23_66, k_23_67, k_23_68, k_23_69, k_23_70, k_23_71, k_23_72, k_23_73, k_23_74, k_23_75, k_23_76, k_23_77, k_23_78, k_23_79, k_24_0, k_24_1, k_24_2, k_24_3, k_24_4, k_24_5, k_24_6, k_24_7, k_24_8, k_24_9, k_24_10, k_24_11, k_24_12, k_24_13, k_24_14, k_24_15, k_24_16, k_24_17, k_24_18, k_24_19, k_24_20, k_24_21, k_24_22, k_24_23, k_24_24, k_24_25, k_24_29, k_24_31, k_24_37, k_24_39, k_24_46, k_24_48, k_24_50, k_24_52, k_24_54, k_24_56, k_24_57, k_24_58, k_24_59, k_24_60, k_24_61, k_24_62, k_24_63, k_24_64, k_24_66, k_24_68, k_24_69, k_24_70, k_24_71, k_24_72, k_24_73, k_24_74, k_24_75, k_24_76, k_24_77, k_24_78, k_24_79, k_25_0, k_25_1, k_25_2, k_25_3, k_25_5, k_25_7, k_25_8, k_25_9, k_25_10, k_25_11, k_25_12, k_25_13, k_25_14, k_25_15, k_25_16, k_25_17, k_25_18, k_25_19, k_25_20, k_25_21, k_25_22, k_25_23, k_25_24, k_25_25, k_25_26, k_25_27, k_25_28, k_25_29, k_25_30, k_25_31, k_25_32, k_25_33, k_25_34, k_25_35, k_25_36, k_25_37, k_25_38, k_25_39, k_25_40, k_25_41, k_25_42, k_25_43, k_25_44, k_25_48, k_25_50, k_25_56, k_25_58, k_25_65, k_25_67, k_25_69, k_25_71, k_25_73, k_25_75, k_25_76, k_25_77, k_25_78, k_25_79, k_26_0, k_26_2, k_26_4, k_26_6, k_26_8, k_26_10, k_26_12, k_26_14, k_26_15, k_26_16, k_26_17, k_26_18, k_26_19, k_26_20, k_26_21, k_26_22, k_26_24, k_26_26, k_26_27, k_26_28, k_26_29, k_26_30, k_26_31, k_26_32, k_26_33, k_26_34, k_26_35, k_26_36, k_26_37, k_26_38, k_26_39, k_26_40, k_26_41, k_26_42, k_26_43, k_26_44, k_26_45, k_26_46, k_26_47, k_26_48, k_26_49, k_26_50, k_26_51, k_26_52, k_26_53, k_26_54, k_26_55, k_26_56, k_26_57, k_26_58, k_26_59, k_26_60, k_26_61, k_26_62, k_26_63, k_26_67, k_26_69, k_26_75, k_26_77