%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] Gamma_1: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] Gamma_2: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] Gamma_3: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) Gamma_4: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] Gamma_5: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) Gamma_6: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] Gamma_7: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) Gamma_8: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] Gamma_9: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) Gamma_10: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] Gamma_11: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] Gamma_12: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) Gamma_13: (extend-no-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 13: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))] Gamma_14: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 13: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))] 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_15: (move) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 13: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 14: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0))] Gamma_16: (resolve) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 13: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 14: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_17: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 9: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 10: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 11: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 12: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 13: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 14: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_18: (move) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 9: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk5_0))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_19: (resolve) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 9: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_20: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 8: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 9: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_21: (move) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 8: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 9: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_22: (resolve) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 8: [~(a_member_of(esk4_0,esk3_0))], ~(a_member_of(esk5_0,esk3_0)), ~( path_connected(esk3_0)) 9: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_23: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: [path_connected(esk3_0)] 3: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 4: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 5: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 6: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 7: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 8: ~(a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), [~( path_connected(esk3_0))] 9: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_24: (move) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: ~(a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), [~( path_connected(esk3_0))] 3: [path_connected(esk3_0)] 4: [a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(path_connected(esk3_0)) 5: ~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk4_0),esk4_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk4_0,esk4_0)),first_homotop_grp(esk3_0,esk4_0), first_homotop_grp(esk3_0,esk4_0))] 6: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)], ~( a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 7: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk4_0),esk5_0,esk4_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk4_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk4_0))] 8: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 9: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 10: [a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)], ~( a_member_of(esk5_0,esk3_0)), ~(path_connected(esk3_0)) 11: ~(a_path_from_to_in(esk2_3(esk3_0,esk5_0,esk5_0),esk5_0,esk5_0,esk3_0)), [a_group_isomorphism_from_to( alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0), first_homotop_grp(esk3_0,esk5_0))] 12: ~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk5_0,esk5_0)),first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))), [isomorphic_groups( first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))] 13: [a_group_isomorphism_from_to(esk1_2(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0)), first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))], ~( isomorphic_groups(first_homotop_grp(esk3_0,esk5_0),first_homotop_grp(esk3_0,esk5_0))) 14: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_25: (resolve) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: ~(a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), [~( path_connected(esk3_0))] 3: [~(a_member_of(esk4_0,esk3_0))], ~(a_member_of(esk5_0,esk3_0)) 4: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 5: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 6: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_26: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: [a_member_of(esk5_0,esk3_0)] 2: ~(a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), [~( path_connected(esk3_0))] 3: ~(a_member_of(esk4_0,esk3_0)), [~(a_member_of(esk5_0,esk3_0))] 4: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 5: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 6: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_27: (move) 0: [a_member_of(esk4_0,esk3_0)] 1: ~(a_member_of(esk4_0,esk3_0)), [~(a_member_of(esk5_0,esk3_0))] 2: [a_member_of(esk5_0,esk3_0)] 3: ~(a_member_of(esk4_0,esk3_0)), ~(a_member_of(esk5_0,esk3_0)), [~( path_connected(esk3_0))] 4: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 5: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 6: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_28: (resolve) 0: [a_member_of(esk4_0,esk3_0)] 1: ~(a_member_of(esk4_0,esk3_0)), [~(a_member_of(esk5_0,esk3_0))] 2: [~(a_member_of(esk4_0,esk3_0))] 3: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 4: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 5: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_29: (extend-conflict) 0: [a_member_of(esk4_0,esk3_0)] 1: ~(a_member_of(esk4_0,esk3_0)), [~(a_member_of(esk5_0,esk3_0))] 2: [~(a_member_of(esk4_0,esk3_0))] 3: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 4: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 5: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_30: (move) 0: [~(a_member_of(esk4_0,esk3_0))] 1: [a_member_of(esk4_0,esk3_0)] 2: ~(a_member_of(esk4_0,esk3_0)), [~(a_member_of(esk5_0,esk3_0))] 3: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 4: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 5: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] Gamma_31: (resolve) 0: [~(a_member_of(esk4_0,esk3_0))] 1: [] 2: [~(a_path_from_to_in(esk2_3(esk3_0,esk4_0,esk5_0),esk4_0,esk5_0,esk3_0))] 3: [~(a_group_isomorphism_from_to(alpha_hat(esk2_3(esk3_0,esk4_0,esk5_0)),first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] 4: [~(isomorphic_groups(first_homotop_grp(esk3_0,esk4_0),first_homotop_grp(esk3_0,esk5_0)))] SZS status Unsatisfiable