%---------------- 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: [group_element(e_3)] Gamma_3: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] Gamma_4: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_5: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] Gamma_6: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] Gamma_7: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: [product(e_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_8: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: [~(equalish(e_3,e_2))] Gamma_9: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_3, e_2)] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_10: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: [~(equalish(e_3,e_2))] 6: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_2,e_3)) 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_11: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_12: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [product(e_3,e_2,e_3)], product(e_3,e_2,e_2), product(e_3,e_2,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_2,e_3)), [equalish(e_2, e_3)] 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_13: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_14: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_15: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) Gamma_16: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [product(e_2,e_3,e_3)], product(e_2,e_3,e_2), product(e_2,e_3,e_1), ~( group_element(e_3)), ~(group_element(e_2)) Gamma_17: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) Gamma_18: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) Gamma_19: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: ~(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)) 9: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] Gamma_20: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: ~(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)) 9: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] 10: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) Gamma_21: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [product(e_2,e_3,e_2)], product(e_2,e_3, e_1), equalish(e_3,e_2), ~(group_element(e_3)), ~(group_element(e_2)) 10: ~(product(e_2,e_3,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_2, e_3)] Gamma_22: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: [~(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)) Gamma_23: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(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)) Gamma_24: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(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)) 10: ~(product(e_3,e_2,e_2)), ~(product(e_2,e_2,e_2)), [equalish(e_3, e_2)] Gamma_25: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(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)) 10: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) Gamma_26: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(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)) 10: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) Gamma_27: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(product(e_3,e_3,e_3)), [product(e_3,e_2,e_2)], product(e_3,e_2, e_1), ~(group_element(e_3)), ~(group_element(e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) Gamma_28: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: [~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) Gamma_29: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) Gamma_30: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] Gamma_31: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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_32: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] Gamma_33: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] Gamma_34: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: [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_35: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: [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)) 16: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) Gamma_36: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: [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_37: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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_38: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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_39: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] Gamma_40: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] Gamma_41: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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_42: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: [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_43: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: [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)) 21: ~(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_44: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: ~(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) 21: [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_45: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: ~(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) 21: ~(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_46: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: ~(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) 21: ~(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_47: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 15: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 16: ~(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)) 17: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 19: [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)) 20: ~(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) 21: ~(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)) 22: [~(equalish(e_3,e_1))] Gamma_48: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_3, e_1)] 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 16: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 17: ~(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)) 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 19: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 20: [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)) 21: ~(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) 22: ~(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_49: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: [~(equalish(e_3,e_1))] 14: [~(product(e_3,e_3,e_3))], ~(product(e_3,e_1,e_3)) 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 16: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 17: ~(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)) 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 19: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 20: [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)) 21: ~(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) 22: ~(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_50: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: [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)) 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 16: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 17: ~(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)) 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 19: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 20: [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)) 21: ~(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) 22: ~(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_51: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_1,e_3)), [equalish(e_1, e_3)] 16: ~(product(e_3,e_1,e_3)), [~(product(e_2,e_1,e_3))], equalish(e_3, e_2) 17: ~(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)) 18: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_2, e_1)] 19: ~(product(e_2,e_2,e_2)), ~(product(e_2,e_1,e_2)), [equalish(e_1, e_2)] 20: [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)) 21: ~(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) 22: ~(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_52: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: [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)) 16: ~(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) 17: ~(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_53: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: [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)) 16: ~(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) 17: ~(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_54: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: [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)) 16: ~(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) 17: ~(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)) 18: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_55: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: [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)) 17: ~(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) 18: ~(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_56: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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)) 17: ~(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) 18: ~(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: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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)) 17: ~(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) 18: ~(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: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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)) 17: ~(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) 18: ~(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)) 19: ~(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_59: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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)) 17: ~(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) 18: ~(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)) 19: ~(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)] 20: ~(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_60: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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)) 17: ~(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) 18: ~(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)) 19: ~(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)] 20: ~(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)] 21: ~(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_61: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: ~(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)) 18: ~(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) 19: ~(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)) 20: ~(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)] 21: ~(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_62: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(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)) 18: ~(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) 19: ~(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_63: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: ~(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)) 18: ~(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) 19: ~(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_64: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: ~(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)) 18: ~(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) 19: ~(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)) 20: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] Gamma_65: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: ~(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)) 18: ~(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) 19: ~(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)) 20: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] 21: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_66: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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)) 19: ~(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) 20: ~(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)) 21: ~(product(e_1,e_3,e_1)), ~(product(e_1,e_1,e_1)), [equalish(e_1, e_3)] Gamma_67: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: [~(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)) 19: ~(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) 20: ~(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_68: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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)) 19: ~(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) 20: ~(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_69: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: [~(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)) 19: ~(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) 20: ~(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_70: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [group_element(e_1)] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: ~(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)) 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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))] 19: ~(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) 20: ~(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_71: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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))] 12: [group_element(e_1)] 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 14: ~(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)) 15: [~(equalish(e_3,e_1))] 16: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 17: ~(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) 18: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 19: ~(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) 20: ~(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_72: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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))] 12: [~(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)) 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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_73: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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))] 12: ~(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)) 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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_74: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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)) 12: ~(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))] 13: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 14: [~(equalish(e_3,e_1))] 15: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 16: ~(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) 17: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 18: ~(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_75: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [~(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)) 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 15: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 16: ~(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_76: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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)) 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 15: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 16: ~(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_77: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: [~(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)) 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 15: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 16: ~(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_78: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: [group_element(e_2)] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: ~(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)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(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))] 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 15: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 16: ~(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_79: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: ~(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))] 4: [group_element(e_2)] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: ~(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)) 8: [~(equalish(e_3,e_2))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 10: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 11: ~(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)) 12: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 13: [~(equalish(e_3,e_1))] 14: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 15: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) 16: ~(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_80: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: ~(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))] 4: [~(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)) 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 12: [~(equalish(e_3,e_1))] 13: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 14: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_81: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_3)] 3: ~(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))] 4: ~(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))] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 12: [~(equalish(e_3,e_1))] 13: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 14: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_82: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: ~(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))] 3: [group_element(e_3)] 4: ~(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))] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(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)) 11: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 12: [~(equalish(e_3,e_1))] 13: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 14: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_83: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: ~(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))] 3: [~(product(e_3,e_3,e_3))], ~(product(e_2,e_2,e_2)), ~(product(e_1,e_1,e_1)) 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 10: [~(equalish(e_3,e_1))] 11: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 12: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_84: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: ~(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))] 3: ~(product(e_3,e_3,e_3)), ~(product(e_2,e_2,e_2)), [~(product(e_1,e_1,e_1))] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 10: [~(equalish(e_3,e_1))] 11: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 12: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_85: (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: ~(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))] 4: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 10: [~(equalish(e_3,e_1))] 11: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 12: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_86: (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: ~(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))] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 11: [~(equalish(e_3,e_1))] 12: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 13: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_87: (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: ~(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))] 5: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 7: [~(equalish(e_3,e_2))] 8: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 9: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 10: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 11: [~(equalish(e_3,e_1))] 12: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) 13: [~(product(e_1,e_3,e_1))], ~(product(e_1,e_1,e_1)), equalish(e_3, e_1) Gamma_88: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 4: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 7: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 8: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 9: [~(equalish(e_3,e_1))] 10: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_89: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 4: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 7: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 8: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 9: [~(equalish(e_3,e_1))] 10: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_90: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(product(e_3,e_2,e_2))], ~(product(e_2,e_2,e_2)) 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: [~(product(e_2,e_3,e_2))], ~(product(e_2,e_2,e_2)), equalish(e_3, e_2) 9: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 10: [~(equalish(e_3,e_1))] 11: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_91: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 7: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 8: [~(equalish(e_3,e_1))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_92: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 5: [~(equalish(e_3,e_2))] 6: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 7: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 8: [~(equalish(e_3,e_1))] 9: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_93: (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: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_2,e_3))] 6: [~(equalish(e_3,e_2))] 7: ~(product(e_3,e_3,e_3)), [~(product(e_2,e_3,e_3))], equalish(e_3, e_2) 8: ~(product(e_3,e_3,e_3)), [~(product(e_3,e_1,e_3))] 9: [~(equalish(e_3,e_1))] 10: ~(product(e_3,e_3,e_3)), [~(product(e_1,e_3,e_3))], equalish(e_3, e_1) Gamma_94: (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: [~(equalish(e_3,e_2))] 6: [~(equalish(e_3,e_1))] SZS status Unsatisfiable