%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [product(X0,X0,X0)] Gamma_1: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] Gamma_2: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] Gamma_3: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] Gamma_4: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] Gamma_5: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] Gamma_6: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] Gamma_7: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] Gamma_8: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] Gamma_9: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] Gamma_10: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] Gamma_11: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] Gamma_12: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] Gamma_13: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] Gamma_14: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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_15: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] Gamma_16: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 16: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] Gamma_17: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 16: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 17: [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_18: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 16: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 17: [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)) 18: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_19: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 16: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 17: [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)) 18: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 19: [~(equalish(e_3,e_2))] Gamma_20: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 17: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 18: [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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_21: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: [~(equalish(e_3,e_2))] 16: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_2,e_3)) 17: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 18: [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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_22: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: [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)) 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 17: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 18: [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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_23: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 18: [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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_24: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: [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)) 18: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_25: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: [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)) 18: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_26: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: [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)) 18: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 19: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) Gamma_27: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_28: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: ~(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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_29: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: ~(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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_30: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: ~(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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 20: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] Gamma_31: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: ~(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)) 19: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 20: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] 21: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) Gamma_32: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(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)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 21: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] Gamma_33: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: [~(product(e_3,e_3,e_3))], product(e_2,e_3,e_1), ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_34: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_35: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 21: ~(product(e_3,e_2,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_3, e_2)] Gamma_36: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 21: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) Gamma_37: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: ~(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)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 20: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 21: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) Gamma_38: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(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)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_39: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: [~(product(e_3,e_3,e_3))], product(e_3,e_2,e_1), ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_40: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) Gamma_41: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] Gamma_42: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) Gamma_43: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] Gamma_44: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] Gamma_45: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: [product(e_2,e_1,e_3)], product(e_2,e_1,e_2), product(e_2,e_1,e_1), ~( group_element(e_2)), ~(group_element(e_1)) Gamma_46: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: [product(e_2,e_1,e_3)], product(e_2,e_1,e_2), product(e_2,e_1,e_1), ~( group_element(e_2)), ~(group_element(e_1)) 27: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) Gamma_47: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: [product(e_2,e_1,e_3)], product(e_2,e_1,e_2), product(e_2,e_1,e_1), ~( group_element(e_2)), ~(group_element(e_1)) Gamma_48: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) Gamma_49: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) Gamma_50: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] Gamma_51: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] Gamma_52: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) Gamma_53: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: [product(e_1,e_2,e_3)], product(e_1,e_2,e_2), product(e_1,e_2,e_1), ~( group_element(e_2)), ~(group_element(e_1)) Gamma_54: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: [product(e_1,e_2,e_3)], product(e_1,e_2,e_2), product(e_1,e_2,e_1), ~( group_element(e_2)), ~(group_element(e_1)) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_55: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 32: [product(e_1,e_2,e_3)], product(e_1,e_2,e_2), product(e_1,e_2,e_1), ~( group_element(e_2)), ~(group_element(e_1)) Gamma_56: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) Gamma_57: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) Gamma_58: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 33: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_59: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 26: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 27: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 28: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 30: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 33: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 34: [~(equalish(e_3,e_1))] Gamma_60: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 26: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 27: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 28: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 30: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 31: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 33: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 34: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_61: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: [~(equalish(e_3,e_1))] 25: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_1,e_3)) 26: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 27: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 28: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 30: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 31: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 33: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 34: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_62: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 26: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 27: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 28: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 30: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 31: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 33: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 34: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_63: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [product(e_3,e_1,e_3)], product(e_3,e_1,e_2), product(e_3,e_1,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 27: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 28: ~(product(e_3,e_1,e_3)), [product(e_2,e_1,e_2)], product(e_2,e_1, e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~(group_element(e_1)) 29: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 30: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 31: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 32: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 33: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 34: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_64: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 29: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_65: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 29: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_66: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 29: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 30: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_67: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: [product(e_1,e_3,e_3)], product(e_1,e_3,e_2), product(e_1,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_68: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_69: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_70: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 31: ~(product(e_2,e_3,e_1)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_3,e_2)), [equalish( e_2,e_3)] Gamma_71: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 31: ~(product(e_2,e_3,e_1)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_3,e_2)), [equalish( e_2,e_3)] 32: ~(product(e_2,e_3,e_1)), ~(product(e_1,e_3,e_2)), ~(product(e_1,e_1,e_1)), [equalish( e_1,e_3)] Gamma_72: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 28: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 30: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 31: ~(product(e_2,e_3,e_1)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_3,e_2)), [equalish( e_2,e_3)] 32: ~(product(e_2,e_3,e_1)), ~(product(e_1,e_3,e_2)), ~(product(e_1,e_1,e_1)), [equalish( e_1,e_3)] 33: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) Gamma_73: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: ~(product(e_3,e_3,e_3)), [product(e_1,e_3,e_2)], product(e_1,e_3, e_1), equalish(e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 31: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 32: ~(product(e_2,e_3,e_1)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_3,e_2)), [equalish( e_2,e_3)] 33: ~(product(e_2,e_3,e_1)), ~(product(e_1,e_3,e_2)), ~(product(e_1,e_1,e_1)), [equalish( e_1,e_3)] Gamma_74: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_3,e_1)), product(e_1, e_3,e_1), ~(product(e_1,e_1,e_1)), equalish(e_3,e_1), ~(group_element(e_3)), ~( group_element(e_1)) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 31: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_75: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), [product(e_1, e_3,e_1)], ~(product(e_1,e_1,e_1)), equalish(e_3,e_1), ~(group_element(e_3)), ~( group_element(e_1)) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 31: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_76: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), [product(e_1, e_3,e_1)], ~(product(e_1,e_1,e_1)), equalish(e_3,e_1), ~(group_element(e_3)), ~( group_element(e_1)) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 31: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 32: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] Gamma_77: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), [product(e_1, e_3,e_1)], ~(product(e_1,e_1,e_1)), equalish(e_3,e_1), ~(group_element(e_3)), ~( group_element(e_1)) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 31: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 32: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] 33: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_78: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), [product(e_1, e_3,e_1)], ~(product(e_1,e_1,e_1)), equalish(e_3,e_1), ~(group_element(e_3)), ~( group_element(e_1)) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) 33: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] Gamma_79: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), equalish( e_3,e_1), ~(group_element(e_3)), ~(group_element(e_1)) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_80: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish( e_3,e_1)], ~(group_element(e_3)), ~(group_element(e_1)) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_81: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), ~(group_element(e_1)) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_82: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: [group_element(e_1)] 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_1))] 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_83: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_1))] 23: [group_element(e_1)] 24: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 25: ~(product(e_3,e_3,e_3)), [product(e_3,e_1,e_2)], product(e_3,e_1, e_1), ~(group_element(e_3)), ~(group_element(e_1)) 26: [~(equalish(e_3,e_1))] 27: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 28: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 29: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 30: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) 31: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [product(e_1, e_2,e_2)], product(e_1,e_2,e_1), equalish(e_3,e_2), ~(group_element(e_2)), ~( group_element(e_1)) 32: [cycle(e_1,e_0)], cycle(e_1,e_2), cycle(e_1,e_1), ~(group_element(e_1)) Gamma_84: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_1))] 23: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 24: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_85: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 21: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_1))] 23: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 24: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_86: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_1)], ~(product(e_2,e_2,e_2)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_3,e_1)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_1))] 24: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 25: [~(equalish(e_3,e_1))] 26: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 27: ~(product(e_2,e_3,e_1)), [~(product(e_1,e_3,e_2))], ~(product(e_1,e_1,e_1)), equalish( e_3,e_1) 28: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 29: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_87: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), equalish( e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 26: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_88: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [equalish( e_3,e_2)], ~(group_element(e_3)), ~(group_element(e_2)) 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 26: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_89: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), ~(group_element(e_2)) 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 26: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_90: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: [group_element(e_2)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_2))] 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 26: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_91: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_2))] 14: [group_element(e_2)] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_1)], ~(product(e_2,e_2,e_2)), ~( group_element(e_3)), ~(group_element(e_2)) 18: [~(equalish(e_3,e_2))] 19: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 20: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 21: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 22: [cycle(e_2,e_0)], cycle(e_2,e_2), cycle(e_2,e_1), ~(group_element(e_2)) 23: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 24: [~(equalish(e_3,e_1))] 25: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 26: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 27: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_1)), [~(product(e_1,e_2,e_3))], equalish( e_3,e_2) Gamma_92: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_2))] 14: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 22: [~(equalish(e_3,e_1))] 23: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 24: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_93: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: [group_element(e_3)] 13: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_2))] 14: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 22: [~(equalish(e_3,e_1))] 23: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 24: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_94: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 13: [group_element(e_3)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), ~( group_element(e_3)), [~(group_element(e_2))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_1))], ~(product(e_1,e_1,e_1)), ~( group_element(e_3)) 21: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 22: [~(equalish(e_3,e_1))] 23: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 24: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_95: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 13: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)) 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 20: [~(equalish(e_3,e_1))] 21: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 22: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_96: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [cycle(e_3,e_0)] 3: [greater(e_3,e_2)] 4: [greater(e_3,e_1)] 5: [greater(e_2,e_1)] 6: [greater(e_3,e_0)] 7: [greater(e_2,e_0)] 8: [greater(e_1,e_0)] 9: [next(e_2,e_3)] 10: [next(e_1,e_2)] 11: [next(e_0,e_1)] 12: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 13: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~(product(e_1,e_1,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 20: [~(equalish(e_3,e_1))] 21: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 22: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_97: (move) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: [product(X0,X0,X0)] 2: ~(product(X0,X0,X0)), [equalish(X0,X0)] 3: [cycle(e_3,e_0)] 4: [greater(e_3,e_2)] 5: [greater(e_3,e_1)] 6: [greater(e_2,e_1)] 7: [greater(e_3,e_0)] 8: [greater(e_2,e_0)] 9: [greater(e_1,e_0)] 10: [next(e_2,e_3)] 11: [next(e_1,e_2)] 12: [next(e_0,e_1)] 13: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 20: [~(equalish(e_3,e_1))] 21: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 22: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_98: (right-split) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: top(X0) != e_1 & top(X0) != e_1 | [product(e_1,e_1,e_1)] 2: top(X0) != e_1 & top(X0) != e_1 & top(X0) != e_1 | [product(X0,X0, X0)] 3: ~(product(X0,X0,X0)), [equalish(X0,X0)] 4: [cycle(e_3,e_0)] 5: [greater(e_3,e_2)] 6: [greater(e_3,e_1)] 7: [greater(e_2,e_1)] 8: [greater(e_3,e_0)] 9: [greater(e_2,e_0)] 10: [greater(e_1,e_0)] 11: [next(e_2,e_3)] 12: [next(e_1,e_2)] 13: [next(e_0,e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 21: [~(equalish(e_3,e_1))] 22: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 23: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_99: (right-split) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: [product(e_1,e_1,e_1)] 2: top(X0) != e_1 & top(X0) != e_1 & top(X0) != e_1 | [product(X0,X0, X0)] 3: ~(product(X0,X0,X0)), [equalish(X0,X0)] 4: [cycle(e_3,e_0)] 5: [greater(e_3,e_2)] 6: [greater(e_3,e_1)] 7: [greater(e_2,e_1)] 8: [greater(e_3,e_0)] 9: [greater(e_2,e_0)] 10: [greater(e_1,e_0)] 11: [next(e_2,e_3)] 12: [next(e_1,e_2)] 13: [next(e_0,e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)), [~( group_element(e_3))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 17: [~(equalish(e_3,e_2))] 18: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 19: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 20: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 21: [~(equalish(e_3,e_1))] 22: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 23: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_100: (resolve) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)) 2: top(X0) != e_1 & top(X0) != e_1 & top(X0) != e_1 | [product(X0,X0, X0)] 3: [cycle(e_3,e_0)] 4: [greater(e_3,e_2)] 5: [greater(e_3,e_1)] 6: [greater(e_2,e_1)] 7: [greater(e_3,e_0)] 8: [greater(e_2,e_0)] 9: [greater(e_1,e_0)] 10: [next(e_2,e_3)] 11: [next(e_1,e_2)] 12: [next(e_0,e_1)] 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 14: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 17: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 18: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 19: [~(equalish(e_3,e_1))] 20: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_101: (extend-conflict) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: top(X0) != e_1 & top(X0) != e_1 & top(X0) != e_1 | [product(X0,X0, X0)] 3: [cycle(e_3,e_0)] 4: [greater(e_3,e_2)] 5: [greater(e_3,e_1)] 6: [greater(e_2,e_1)] 7: [greater(e_3,e_0)] 8: [greater(e_2,e_0)] 9: [greater(e_1,e_0)] 10: [next(e_2,e_3)] 11: [next(e_1,e_2)] 12: [next(e_0,e_1)] 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 14: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 17: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 18: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 19: [~(equalish(e_3,e_1))] 20: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_102: (right-split) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: top(X0) != e_2 & top(X0) != e_2 | [product(e_2,e_2,e_2)] 3: top(X0) != e_2 & top(X0) != e_2 & top(X0) != e_2 | [product(X0,X0, X0)] 4: [cycle(e_3,e_0)] 5: [greater(e_3,e_2)] 6: [greater(e_3,e_1)] 7: [greater(e_2,e_1)] 8: [greater(e_3,e_0)] 9: [greater(e_2,e_0)] 10: [greater(e_1,e_0)] 11: [next(e_2,e_3)] 12: [next(e_1,e_2)] 13: [next(e_0,e_1)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 19: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 20: [~(equalish(e_3,e_1))] 21: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_103: (resolve) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: top(X0) != e_2 & top(X0) != e_2 | [~(product(e_3,e_3,e_3))] 3: top(X0) != e_2 & top(X0) != e_2 & top(X0) != e_2 | [product(X0,X0, X0)] 4: [cycle(e_3,e_0)] 5: [greater(e_3,e_2)] 6: [greater(e_3,e_1)] 7: [greater(e_2,e_1)] 8: [greater(e_3,e_0)] 9: [greater(e_2,e_0)] 10: [greater(e_1,e_0)] 11: [next(e_2,e_3)] 12: [next(e_1,e_2)] 13: [next(e_0,e_1)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 17: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 18: [~(equalish(e_3,e_1))] 19: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_104: (extend-conflict) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: [~(product(e_3,e_3,e_3))] 3: top(X0) != e_2 & top(X0) != e_2 & top(X0) != e_2 | [product(X0,X0, X0)] 4: [cycle(e_3,e_0)] 5: [greater(e_3,e_2)] 6: [greater(e_3,e_1)] 7: [greater(e_2,e_1)] 8: [greater(e_3,e_0)] 9: [greater(e_2,e_0)] 10: [greater(e_1,e_0)] 11: [next(e_2,e_3)] 12: [next(e_1,e_2)] 13: [next(e_0,e_1)] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 15: [~(equalish(e_3,e_2))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 17: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 18: [~(equalish(e_3,e_1))] 19: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_105: (right-split) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: [~(product(e_3,e_3,e_3))] 3: top(X0) != e_3 & top(X0) != e_3 | [product(e_3,e_3,e_3)] 4: top(X0) != e_3 & top(X0) != e_3 & top(X0) != e_3 | [product(X0,X0, X0)] 5: [cycle(e_3,e_0)] 6: [greater(e_3,e_2)] 7: [greater(e_3,e_1)] 8: [greater(e_2,e_1)] 9: [greater(e_3,e_0)] 10: [greater(e_2,e_0)] 11: [greater(e_1,e_0)] 12: [next(e_2,e_3)] 13: [next(e_1,e_2)] 14: [next(e_0,e_1)] 15: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 16: [~(equalish(e_3,e_2))] 17: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 18: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 19: [~(equalish(e_3,e_1))] 20: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_106: (resolve) 0: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~( product(e_1,e_1,e_1))] 1: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_2,e_2))] 2: [~(product(e_3,e_3,e_3))] 3: [] 4: top(X0) != e_3 & top(X0) != e_3 & top(X0) != e_3 | [product(X0,X0, X0)] 5: [cycle(e_3,e_0)] 6: [greater(e_3,e_2)] 7: [greater(e_3,e_1)] 8: [greater(e_2,e_1)] 9: [greater(e_3,e_0)] 10: [greater(e_2,e_0)] 11: [greater(e_1,e_0)] 12: [next(e_2,e_3)] 13: [next(e_1,e_2)] 14: [next(e_0,e_1)] 15: [~(equalish(e_3,e_2))] 16: [~(equalish(e_3,e_1))] SZS status Unsatisfiable