%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [m0(X0,d,X1)] Gamma_1: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) Gamma_2: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) Gamma_3: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) split p2(X0,X0,X0) by p2(e,e,e) partition: top(X0) != e & top(X0) != e & top(X0) != e | p2(X0,X0,X0) top(X0) != e & top(X0) != e | p2(e,e,e) top(X0) != e & top(X0) != e | p2(e,e,e) top(X0) != e | p2(e,e,e) top(X0) != e & top(X0) != e | p2(e,e,e) top(X0) != e | p2(e,e,e) top(X0) != e | p2(e,e,e) | p2(e,e,e) | p2(e,e,e) Gamma_4: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: [p2(X0,X0,X0)], ~(p2(e,e,e)), ~(q1(e,e,e)) Gamma_5: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) Gamma_6: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) Gamma_7: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) Gamma_8: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) Gamma_9: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) Gamma_10: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] split q1(X0,X0,X0) by q1(e,X0,X0) partition: top(X0) != e | q1(X0,X0,X0) | q1(e,e,e) top(X0) != e | q1(e,e,e) Gamma_11: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: [q1(X0,X0,X0)], ~(m0(X0,d,X0)) Gamma_12: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) Gamma_13: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) split m1(X0,d,X0) by m1(X0,X0,X0) partition: | m1(d,d,d) top(X0) != d | m1(X0,d,X0) Gamma_14: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: [m1(X0,d,X0)], ~(m0(d,d,X0)) Gamma_15: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) Gamma_16: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) Gamma_17: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] Gamma_18: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) Gamma_19: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_20: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] Gamma_21: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] Gamma_22: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] Gamma_23: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] split q5(X0,X0) by q5(c,c) partition: top(X0) != c & top(X0) != c | q5(X0,X0) top(X0) != c | q5(c,c) top(X0) != c | q5(c,c) | q5(c,c) | q5(c,c) Gamma_24: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: [q5(X0,X0)], ~(l4(X0)) Gamma_25: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) split m0(a,X0,a) by m0(X0,d,X1) partition: top(X0) != d | m0(a,X0,a) | m0(a,d,a) | m0(a,d,a) Gamma_26: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: [m0(a,X0,a)] Gamma_27: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] Gamma_28: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] Gamma_29: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] Gamma_30: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) Gamma_31: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] Gamma_32: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) Gamma_33: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) Gamma_34: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] Gamma_35: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) Gamma_36: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] Gamma_37: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] Gamma_38: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] Gamma_39: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) Gamma_40: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] split p3(d,X0,X0) by p3(X0,X0,X0) partition: | p3(d,d,d) top(X0) != d | p3(d,X0,X0) Gamma_41: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) Gamma_42: (right-split) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) Gamma_43: (extend-no-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 37: [p1(d,d,d)], ~(q0(X0,d)) Gamma_44: (extend-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 37: [p1(d,d,d)], ~(q0(X0,d)) 38: [~(p1(d,d,d))] Gamma_45: (move) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 37: [~(p1(d,d,d))] 38: [p1(d,d,d)], ~(q0(X0,d)) Gamma_46: (resolve) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 37: [~(p1(d,d,d))] 38: [~(q0(X0,d))] Gamma_47: (extend-conflict) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [q0(X0,d)] 34: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 35: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 36: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 37: [~(p1(d,d,d))] 38: [~(q0(X0,d))] Gamma_48: (move) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [~(q0(X0,d))] 34: [q0(X0,d)] 35: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 36: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 37: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 38: [~(p1(d,d,d))] Gamma_49: (resolve) 0: [m0(X0,d,X1)] 1: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 2: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 3: [p2(e,e,e)], ~(q1(e,e,e)) 4: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 5: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 6: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 8: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 9: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 10: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 11: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 12: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 13: [q2(c,c,c)], ~(q1(c,c,c)) 14: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 15: [n1(d,c,d)], ~(m0(X0,d,c)) 16: ~(q1(X0,X0,X0)), [k2(X0,X0)] 17: ~(p3(X0,X0,X0)), [l4(X0)] 18: ~(p2(X0,X0,X0)), [n3(X0)] 19: ~(q4(c,c)), [q5(c,c)] 20: ~(q4(c,c)), [n5(c,c)] 21: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0)) 22: top(X0) != d | [m0(a,X0,a)] 23: [m0(b,a,a)] 24: [m0(d,e,c)] 25: [n1(e,c,e)], ~(m0(d,e,c)) 26: [m0(b,b,e)] 27: [m1(e,b,e)], ~(m0(b,b,e)) 28: [p2(b,e,b)], ~(m1(e,b,e)) 29: [m0(e,b,c)] 30: [n1(b,c,b)], ~(m0(e,b,c)) 31: [m0(a,e,e)] 32: [m0(c,b,a)] 33: [~(q0(X0,d))] 34: [] 35: [q2(d,d,d)], ~(n1(d,d,X0)), ~(q0(d,d)) 36: ~(q2(d,d,d)), ~(m3(d,d,d)), ~(k3(d,d,d)), [q4(d,d)] 37: top(X0) != d | ~(q2(d,d,d)), [p3(d,X0,X0)], ~(k2(X0,X0)) 38: [~(p1(d,d,d))] SZS status Unsatisfiable