%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [group_element(e_3)] Gamma_1: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) Gamma_2: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] Gamma_3: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] Gamma_4: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_5: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] Gamma_6: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] Gamma_7: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] Gamma_8: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_9: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] Gamma_10: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] 10: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] Gamma_11: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] 10: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) Gamma_12: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] 10: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 12: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) Gamma_13: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] 10: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 12: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) Gamma_14: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2,e_2, e_3)] 10: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 12: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) 14: [~(equalish(e_3,e_2))] Gamma_15: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 9: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2, e_2,e_3)] 11: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 12: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) Gamma_16: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: [~(equalish(e_3,e_2))] 8: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_2,e_3)) 9: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2, e_2,e_3)] 11: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 12: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) Gamma_17: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 9: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2, e_2,e_3)] 11: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 12: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) Gamma_18: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 6: ~(product(e_3,e_2,e_3)), [equalish(e_2,e_2)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 8: [~(equalish(e_3,e_2))] 9: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_3,e_2,e_3)), ~(product(e_2,e_3,e_3)), [product(e_2, e_2,e_3)] 11: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 12: ~(product(e_2,e_3,e_3)), [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_3)) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_3)), ~(product(e_3,e_2,e_2)) Gamma_19: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_20: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_21: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [product(e_2,e_2,e_2)] Gamma_22: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [product(e_2,e_2,e_2)] 9: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) Gamma_23: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 9: ~(product(e_3,e_2,e_2)), [product(e_2,e_2,e_2)] Gamma_24: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 9: [~(product(e_3,e_2,e_2))], equalish(e_3,e_2) Gamma_25: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 9: ~(product(e_3,e_2,e_2)), [equalish(e_3,e_2)] Gamma_26: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 9: [~(product(e_3,e_2,e_2))] Gamma_27: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 9: [~(product(e_3,e_2,e_2))] Gamma_28: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_2,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) Gamma_29: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: [~(product(e_3,e_3,e_3))], product(e_3,e_2,e_1), ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_30: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_31: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) Gamma_32: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_33: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) Gamma_34: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) Gamma_35: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [product(e_2,e_2,e_2)] Gamma_36: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_2,e_2)), [equalish(e_2,e_2)] Gamma_37: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [product(e_2,e_2,e_2)] 11: ~(product(e_2,e_2,e_2)), [equalish(e_2,e_2)] 12: ~(product(e_2,e_3,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) Gamma_38: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 11: ~(product(e_2,e_3,e_2)), [product(e_2,e_2,e_2)] 12: ~(product(e_2,e_2,e_2)), [equalish(e_2,e_2)] Gamma_39: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 11: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) Gamma_40: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 11: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) Gamma_41: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_2,e_3,e_2)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) Gamma_42: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: [~(product(e_3,e_3,e_3))], product(e_2,e_3,e_1), equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_43: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_44: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] Gamma_45: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] Gamma_46: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) Gamma_47: (extend-no-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 14: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] Gamma_48: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 14: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] 15: ~(product(e_2,e_2,e_3)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) Gamma_49: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 13: ~(product(e_2,e_2,e_3)), [product(e_2,e_2,e_2)] 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 15: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] Gamma_50: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 13: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 15: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] Gamma_51: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 12: ~(product(e_2,e_2,e_3)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 13: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 15: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] Gamma_52: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 12: ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)), [product(e_2, e_2,e_3)] 13: ~(product(e_2,e_2,e_3)), [~(product(e_2,e_2,e_2))], equalish(e_3, e_2) 14: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) 15: ~(product(e_2,e_2,e_3)), [equalish(e_2,e_2)] Gamma_53: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 12: [~(product(e_3,e_2,e_1))], ~(product(e_2,e_3,e_1)), equalish(e_3, e_2) 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) Gamma_54: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 12: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) Gamma_55: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 11: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], equalish(e_3,e_2), ~( group_element(e_3)), ~(group_element(e_2)) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 13: [product(e_3,e_3,e_2)], ~(product(e_3,e_2,e_1)), ~(product(e_2,e_3,e_1)) Gamma_56: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 11: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_2,e_1)), equalish(e_3, e_2), ~(group_element(e_3)), ~(group_element(e_2)) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_57: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 11: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [equalish(e_3, e_2)], ~(group_element(e_3)), ~(group_element(e_2)) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_58: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 11: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_2,e_1)), ~(group_element(e_3)), ~( group_element(e_2)) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_59: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 11: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_1))], ~(group_element(e_3)), ~( group_element(e_2)) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_60: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_1))], ~(group_element(e_3)), ~( group_element(e_2)) 7: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(group_element(e_3)), ~( group_element(e_2)) 8: [~(equalish(e_3,e_2))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 10: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 11: ~(product(e_3,e_2,e_1)), [~(product(e_2,e_3,e_1))], equalish(e_3, e_2) 12: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_61: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_1))], ~(group_element(e_3)), ~( group_element(e_2)) 7: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)), ~(group_element(e_2)) 8: [~(equalish(e_3,e_2))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 10: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_62: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_1))], ~(group_element(e_3)), ~( group_element(e_2)) 7: ~(product(e_3,e_3,e_3)), ~(group_element(e_3)), [~(group_element(e_2))] 8: [~(equalish(e_3,e_2))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 10: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_63: (move) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: ~(product(e_3,e_3,e_3)), ~(group_element(e_3)), [~(group_element(e_2))] 4: [group_element(e_2)] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_1))], ~(group_element(e_3)), ~( group_element(e_2)) 8: [~(equalish(e_3,e_2))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 10: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 11: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_64: (resolve) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: ~(product(e_3,e_3,e_3)), ~(group_element(e_3)), [~(group_element(e_2))] 4: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))] 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_65: (extend-conflict) 0: [group_element(e_3)] 1: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 2: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 3: ~(product(e_3,e_3,e_3)), ~(group_element(e_3)), [~(group_element(e_2))] 4: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))] 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_66: (move) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: [product(e_3,e_3,e_3)], product(e_3,e_3,e_2), product(e_3,e_3,e_1), ~( group_element(e_3)) 3: ~(product(e_3,e_3,e_3)), [equalish(e_3,e_3)] 4: ~(product(e_3,e_3,e_3)), ~(group_element(e_3)), [~(group_element(e_2))] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))] 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 10: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_67: (resolve) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: [product(e_3,e_3,e_2)], product(e_3,e_3,e_1), ~(group_element(e_3)) 3: [~(product(e_3,e_2,e_2))] 4: [~(equalish(e_3,e_2))] 5: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 6: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_68: (extend-no-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: [product(e_3,e_3,e_2)], product(e_3,e_3,e_1), ~(group_element(e_3)) 3: [~(product(e_3,e_2,e_2))] 4: [~(equalish(e_3,e_2))] 5: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 6: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_69: (extend-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: [product(e_3,e_3,e_2)], product(e_3,e_3,e_1), ~(group_element(e_3)) 3: [~(product(e_3,e_2,e_2))] 4: [~(equalish(e_3,e_2))] 5: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 6: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 7: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] Gamma_70: (move) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: [product(e_3,e_3,e_2)], product(e_3,e_3,e_1), ~(group_element(e_3)) 4: [~(product(e_3,e_2,e_2))] 5: [~(equalish(e_3,e_2))] 6: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 7: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_71: (resolve) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [product(e_3,e_3,e_1)], ~(group_element(e_3)) 4: [~(product(e_3,e_2,e_2))] 5: [~(equalish(e_3,e_2))] 6: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 7: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_72: (extend-no-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [product(e_3,e_3,e_1)], ~(group_element(e_3)) 4: [~(product(e_3,e_2,e_2))] 5: [~(equalish(e_3,e_2))] 6: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 7: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_73: (extend-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [product(e_3,e_3,e_1)], ~(group_element(e_3)) 4: [~(product(e_3,e_2,e_2))] 5: [~(equalish(e_3,e_2))] 6: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 7: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) 8: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] Gamma_74: (move) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 4: product(e_3,e_3,e_3), [product(e_3,e_3,e_1)], ~(group_element(e_3)) 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_75: (resolve) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 4: [product(e_3,e_3,e_3)], ~(group_element(e_3)) 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_76: (extend-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 4: [product(e_3,e_3,e_3)], ~(group_element(e_3)) 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_77: (resolve) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 4: [~(group_element(e_3))] 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_78: (extend-conflict) 0: [group_element(e_3)] 1: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 2: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 4: [~(group_element(e_3))] 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_79: (move) 0: [~(group_element(e_3))] 1: [group_element(e_3)] 2: [~(product(e_3,e_3,e_3))], ~(group_element(e_3)) 3: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_2))] 4: product(e_3,e_3,e_3), [~(product(e_3,e_3,e_1))] 5: [~(product(e_3,e_2,e_2))] 6: [~(equalish(e_3,e_2))] 7: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 8: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) Gamma_80: (resolve) 0: [~(group_element(e_3))] 1: [] 2: [~(product(e_3,e_2,e_2))] 3: [~(equalish(e_3,e_2))] 4: [~(product(e_2,e_3,e_2))], equalish(e_3,e_2) 5: [~(product(e_2,e_2,e_3))], equalish(e_3,e_2) SZS status Unsatisfiable