%---------------- 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_4)] Gamma_3: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] Gamma_4: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_5: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] Gamma_6: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) Gamma_7: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] Gamma_8: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) Gamma_9: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] Gamma_10: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] Gamma_11: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 11: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_3,e_3)), [equalish(e_4, e_3)] Gamma_12: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 11: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_3,e_3)), [equalish(e_4, e_3)] 12: [~(equalish(e_4,e_3))] Gamma_13: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 11: [~(equalish(e_4,e_3))] 12: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_3,e_3)), [equalish(e_4, e_3)] Gamma_14: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 11: [~(equalish(e_4,e_3))] 12: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) Gamma_15: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 7: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 8: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 9: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3,e_4, e_4)] 10: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 11: [~(equalish(e_4,e_3))] 12: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) Gamma_16: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 7: [product(e_4,e_3,e_3)], ~(product(e_3,e_4,e_3)), ~(product(e_3,e_3,e_3)) 8: ~(product(e_4,e_3,e_3)), ~(product(e_3,e_4,e_3)), [product(e_3,e_3, e_4)] 9: [product(e_4,e_4,e_3)], ~(product(e_3,e_3,e_4)) 10: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_3)), [product(e_3, e_4,e_4)] 11: ~(product(e_4,e_3,e_4)), ~(product(e_3,e_3,e_4)), [equalish(e_3, e_4)] 12: [~(equalish(e_4,e_3))] Gamma_17: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_18: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 6: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_19: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 6: ~(product(e_4,e_3,e_4)), [product(e_3,e_4,e_3)] 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_20: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 6: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_21: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 5: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 6: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_22: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: [product(e_4,e_3,e_4)], product(e_4,e_3,e_3), product(e_4,e_3,e_2), product( e_4,e_3,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_23: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: [product(e_4,e_3,e_3)], product(e_4,e_3,e_2), product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_24: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] Gamma_25: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: [product(e_3,e_4,e_4)], product(e_3,e_4,e_3), product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_26: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: [product(e_3,e_4,e_4)], product(e_3,e_4,e_3), product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 10: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_4)), [product(e_2, e_4,e_4)] Gamma_27: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: [product(e_3,e_4,e_4)], product(e_3,e_4,e_3), product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 10: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_4)), [product(e_2, e_4,e_4)] 11: ~(product(e_4,e_3,e_2)), [product(e_4,e_2,e_3)], ~(product(e_3,e_4,e_4)) Gamma_28: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: [product(e_3,e_4,e_4)], product(e_3,e_4,e_3), product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 10: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_4)), [product(e_2, e_4,e_4)] 11: ~(product(e_4,e_3,e_2)), [product(e_4,e_2,e_3)], ~(product(e_3,e_4,e_4)) 12: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] Gamma_29: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: [product(e_3,e_4,e_4)], product(e_3,e_4,e_3), product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_4)), [product(e_2, e_4,e_4)] 12: ~(product(e_4,e_3,e_2)), [product(e_4,e_2,e_3)], ~(product(e_3,e_4,e_4)) Gamma_30: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), [product(e_3,e_4,e_3)], product(e_3,e_4,e_2), product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_31: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_32: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] Gamma_33: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) Gamma_34: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) Gamma_35: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] Gamma_36: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] Gamma_37: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) Gamma_38: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) Gamma_39: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] Gamma_40: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) Gamma_41: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) Gamma_42: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 21: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] Gamma_43: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 21: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 22: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_44: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 21: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 22: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] 23: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] Gamma_45: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_2, e_3,e_3)] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 23: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_46: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_3,e_3,e_3))], ~( product(e_3,e_3,e_2)) 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 23: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_47: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 13: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 23: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_48: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 13: [product(e_3,e_3,e_2)], ~(product(e_2,e_2,e_3)) 14: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_3,e_3,e_3)), ~(product(e_3,e_3,e_2)), [product(e_3, e_2,e_3)] 23: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_49: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 14: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_50: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 12: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 14: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_51: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_3)] 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 14: [product(e_3,e_2,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 15: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 16: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 17: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 18: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 19: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 20: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 21: [product(e_2,e_3,e_2)], ~(product(e_2,e_2,e_3)), ~(product(e_2,e_2,e_2)) 22: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_52: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 12: product(e_4,e_3,e_3), [~(product(e_4,e_3,e_2))], ~(product(e_3,e_4,e_2)), ~( product(e_3,e_3,e_3)) 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_53: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 11: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 12: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_54: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), product(e_3,e_4,e_3), [product(e_3,e_4,e_2)], product( e_3,e_4,e_1), ~(group_element(e_4)), ~(group_element(e_3)) 12: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_2,e_2,e_3))] 13: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), ~(product(e_3,e_3,e_3)), [~( product(e_3,e_3,e_2))] 14: product(e_4,e_3,e_3), ~(product(e_3,e_4,e_2)), [~(product(e_2,e_3,e_3))] 15: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_2)), [product(e_2, e_2,e_4)] 16: [product(e_4,e_4,e_2)], ~(product(e_2,e_2,e_4)) 17: [product(e_4,e_2,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 18: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_2, e_4,e_4)] 19: [product(e_2,e_4,e_2)], ~(product(e_2,e_2,e_4)), ~(product(e_2,e_2,e_2)) 20: ~(product(e_4,e_4,e_4)), ~(product(e_4,e_4,e_2)), [product(e_4, e_2,e_4)] Gamma_55: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: [product(e_4,e_3,e_3)], ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), product(e_3,e_4,e_1), ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_56: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_57: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] Gamma_58: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] Gamma_59: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: [product(e_4,e_4,e_3)], product(e_4,e_3,e_3), product(e_4,e_2,e_3), product( e_4,e_1,e_3), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_60: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: [product(e_4,e_4,e_3)], product(e_4,e_3,e_3), product(e_4,e_2,e_3), product( e_4,e_1,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 15: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) Gamma_61: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: [product(e_4,e_4,e_3)], product(e_4,e_3,e_3), product(e_4,e_2,e_3), product( e_4,e_1,e_3), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_62: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), [product(e_4,e_3, e_3)], product(e_4,e_2,e_3), product(e_4,e_1,e_3), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_63: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), [product(e_4,e_2,e_3)], product(e_4,e_1,e_3), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_64: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), [product(e_4,e_2,e_3)], product(e_4,e_1,e_3), ~(group_element(e_4)), ~( group_element(e_3)) 16: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) Gamma_65: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), [product(e_4,e_2,e_3)], product(e_4,e_1,e_3), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_66: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: [~(product(e_4,e_4,e_4))], product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), product(e_4,e_1,e_3), product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_67: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_68: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_3,e_4,e_4), [product(e_3,e_3,e_4)], product(e_3,e_2,e_4), product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_69: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_3,e_4,e_4), [product(e_3,e_3,e_4)], product(e_3,e_2,e_4), product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 18: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] Gamma_70: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_3,e_4,e_4), [product(e_3,e_3,e_4)], product(e_3,e_2,e_4), product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_71: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), [product(e_3,e_4,e_4)], product(e_3,e_2,e_4), product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_72: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_73: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] Gamma_74: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] Gamma_75: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_76: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_3,e_4), product(e_3,e_3,e_4), [product(e_2,e_3,e_4)], product( e_1,e_3,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_77: (extend-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_3,e_4), product(e_3,e_3,e_4), [product(e_2,e_3,e_4)], product( e_1,e_3,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 23: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] Gamma_78: (move) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_3,e_4), product(e_3,e_3,e_4), [product(e_2,e_3,e_4)], product( e_1,e_3,e_4), ~(group_element(e_4)), ~(group_element(e_3)) Gamma_79: (resolve) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), [product(e_4,e_3,e_4)], product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), product(e_1,e_3,e_4), ~(group_element(e_4)), ~( group_element(e_3)) Gamma_80: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) Gamma_81: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) 24: [product(e_4,e_2,e_1)], ~(product(e_2,e_4,e_3)), ~(product(e_1,e_3,e_4)) Gamma_82: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) 24: [product(e_4,e_2,e_1)], ~(product(e_2,e_4,e_3)), ~(product(e_1,e_3,e_4)) 25: ~(product(e_4,e_2,e_1)), [product(e_3,e_1,e_2)], ~(product(e_2,e_4,e_3)) Gamma_83: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) 24: [product(e_4,e_2,e_1)], ~(product(e_2,e_4,e_3)), ~(product(e_1,e_3,e_4)) 25: ~(product(e_4,e_2,e_1)), [product(e_3,e_1,e_2)], ~(product(e_2,e_4,e_3)) 26: [group_element(e_2)] Gamma_84: (extend-no-conflict) 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) 24: [product(e_4,e_2,e_1)], ~(product(e_2,e_4,e_3)), ~(product(e_1,e_3,e_4)) 25: ~(product(e_4,e_2,e_1)), [product(e_3,e_1,e_2)], ~(product(e_2,e_4,e_3)) 26: [group_element(e_2)] 27: [group_element(e_1)] 0: [product(X0,X0,X0)] 1: ~(product(X0,X0,X0)), [equalish(X0,X0)] 2: [group_element(e_4)] 3: [group_element(e_3)] 4: [~(product(e_4,e_3,e_4))], ~(product(e_3,e_3,e_3)) 5: product(e_4,e_3,e_3), [product(e_4,e_3,e_2)], product(e_4,e_3,e_1), ~( product(e_3,e_3,e_3)), ~(group_element(e_4)), ~(group_element(e_3)) 6: [~(product(e_3,e_4,e_3))], ~(product(e_3,e_3,e_3)) 7: [~(product(e_4,e_3,e_3))], ~(product(e_3,e_3,e_3)) 8: [~(equalish(e_4,e_3))] 9: product(e_4,e_3,e_3), [~(product(e_3,e_4,e_4))] 10: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), [~(product(e_3,e_4,e_2))], ~( product(e_3,e_3,e_3)) 11: product(e_4,e_3,e_3), ~(product(e_4,e_3,e_2)), product(e_3,e_4, e_3), [product(e_3,e_4,e_1)], ~(product(e_3,e_3,e_3)), ~(group_element(e_4)), ~( group_element(e_3)) 12: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_1, e_2,e_3)] 13: ~(product(e_4,e_3,e_2)), ~(product(e_3,e_4,e_1)), [product(e_2, e_1,e_4)] 14: ~(product(e_4,e_4,e_4)), [~(product(e_4,e_4,e_3))], product(e_4, e_3,e_4) 15: ~(product(e_4,e_3,e_2)), [~(product(e_4,e_2,e_3))], product(e_3, e_4,e_4) 16: ~(product(e_4,e_4,e_4)), product(e_4,e_3,e_4), product(e_4,e_3, e_3), ~(product(e_4,e_3,e_2)), [product(e_4,e_1,e_3)], product(e_3,e_4, e_4), ~(group_element(e_4)), ~(group_element(e_3)) 17: product(e_4,e_4,e_3), [~(product(e_3,e_3,e_4))] 18: product(e_4,e_4,e_3), product(e_3,e_4,e_4), [product(e_3,e_2,e_4)], product( e_3,e_1,e_4), ~(group_element(e_4)), ~(group_element(e_3)) 19: ~(product(e_4,e_1,e_3)), ~(product(e_3,e_2,e_4)), [product(e_2, e_3,e_1)] 20: ~(product(e_3,e_2,e_4)), ~(product(e_2,e_3,e_1)), [product(e_1, e_4,e_2)] 21: product(e_4,e_4,e_3), product(e_3,e_4,e_3), [product(e_2,e_4,e_3)], product( e_1,e_4,e_3), ~(group_element(e_4)), ~(group_element(e_3)) 22: product(e_4,e_4,e_3), ~(product(e_3,e_2,e_4)), [~(product(e_2,e_3,e_4))] 23: product(e_4,e_4,e_3), product(e_4,e_3,e_4), product(e_3,e_3,e_4), ~( product(e_3,e_2,e_4)), [product(e_1,e_3,e_4)], ~(group_element(e_4)), ~( group_element(e_3)) 24: [product(e_4,e_2,e_1)], ~(product(e_2,e_4,e_3)), ~(product(e_1,e_3,e_4)) 25: ~(product(e_4,e_2,e_1)), [product(e_3,e_1,e_2)], ~(product(e_2,e_4,e_3)) 26: [group_element(e_2)] 27: [group_element(e_1)] SZS status Satisfiable