%---------------- 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-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: [~(k2(d,d))] Gamma_21: (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: [~(k2(d,d))] 17: ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_22: (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: [~(k2(d,d))] 17: top(X0) != d | ~(q1(d,d,d)), [k2(d,d)] 18: top(X0) != d & top(X0) != d | ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_23: (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: [~(k2(d,d))] 17: top(X0) != d | [~(q1(d,d,d))] 18: top(X0) != d & top(X0) != d | ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_24: (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: [~(k2(d,d))] 17: [~(q1(d,d,d))] 18: top(X0) != d & top(X0) != d | ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_25: (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: [~(q1(d,d,d))] 11: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0)) 12: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 13: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 14: [q2(c,c,c)], ~(q1(c,c,c)) 15: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 16: [n1(d,c,d)], ~(m0(X0,d,c)) 17: [~(k2(d,d))] 18: top(X0) != d & top(X0) != d | ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_26: (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: [~(q1(d,d,d))] 11: top(X0) != d & top(X0) != d | [q1(d,d,d)], ~(m0(d,d,d)) 12: top(X0) != d & top(X0) != d & top(X0) != d | [q1(X0,X0,X0)], ~( m0(X0,d,X0)) 13: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 14: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 15: [q2(c,c,c)], ~(q1(c,c,c)) 16: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 17: [n1(d,c,d)], ~(m0(X0,d,c)) 18: [~(k2(d,d))] 19: top(X0) != d & top(X0) != d | ~(q1(X0,X0,X0)), [k2(X0,X0)] Gamma_27: (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: [~(q1(d,d,d))] 11: top(X0) != d & top(X0) != d | [~(m0(d,d,d))] 12: top(X0) != d & top(X0) != d & top(X0) != d | [q1(X0,X0,X0)], ~( m0(X0,d,X0)) 13: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 14: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 15: [q2(c,c,c)], ~(q1(c,c,c)) 16: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 17: [n1(d,c,d)], ~(m0(X0,d,c)) 18: [~(k2(d,d))] Gamma_28: (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: [~(q1(d,d,d))] 11: [~(m0(d,d,d))] 12: top(X0) != d & top(X0) != d & top(X0) != d | [q1(X0,X0,X0)], ~( m0(X0,d,X0)) 13: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 14: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 15: [q2(c,c,c)], ~(q1(c,c,c)) 16: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 17: [n1(d,c,d)], ~(m0(X0,d,c)) 18: [~(k2(d,d))] Gamma_29: (move) 0: [~(m0(d,d,d))] 1: [m0(X0,d,X1)] 2: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 3: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 4: [p2(e,e,e)], ~(q1(e,e,e)) 5: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 6: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 8: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 9: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 10: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 11: [~(q1(d,d,d))] 12: top(X0) != d & top(X0) != d & top(X0) != d | [q1(X0,X0,X0)], ~( m0(X0,d,X0)) 13: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 14: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 15: [q2(c,c,c)], ~(q1(c,c,c)) 16: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 17: [n1(d,c,d)], ~(m0(X0,d,c)) 18: [~(k2(d,d))] Gamma_30: (right-split) 0: [~(m0(d,d,d))] 1: [m0(d,d,d)] 2: top(X0) != d | [m0(X0,d,d)] 3: top(X1) != d | [m0(d,d,X0)] 4: top(X1) != d & top(X0) != d | [m0(X0,d,X1)] 5: [n1(X0,X0,X1)], ~(m0(X1,d,X0)), ~(m0(d,d,d)) 6: [q1(e,X0,X0)], ~(m0(X0,d,X0)), ~(m0(e,d,X0)) 7: [p2(e,e,e)], ~(q1(e,e,e)) 8: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 9: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 10: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 11: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 12: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 13: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 14: [~(q1(d,d,d))] 15: top(X0) != d & top(X0) != d & top(X0) != d | [q1(X0,X0,X0)], ~( m0(X0,d,X0)) 16: [m1(X0,X0,X0)], ~(m0(X1,d,X0)) 17: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0)) 18: [q2(c,c,c)], ~(q1(c,c,c)) 19: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)] 20: [n1(d,c,d)], ~(m0(X0,d,c)) 21: [~(k2(d,d))] Gamma_31: (resolve) 0: [~(m0(d,d,d))] 1: [] 2: top(X0) != d | [m0(X0,d,d)] 3: top(X1) != d | [m0(d,d,X0)] 4: top(X1) != d & top(X0) != d | [m0(X0,d,X1)] 5: [p2(e,e,e)], ~(q1(e,e,e)) 6: top(X0) != e & top(X0) != e & top(X0) != e | [p2(X0,X0,X0)], ~(p2(e,e,e)), ~( q1(e,e,e)) 7: [r3(X0,X0,X0)], ~(p2(X0,X0,X0)) 8: [m3(X0,X0,X0)], ~(p2(X0,X0,X0)) 9: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,X0)) 10: [p4(X0,X0,X0)], ~(p3(X0,X0,X0)) 11: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)] 12: [~(q1(d,d,d))] 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: [~(k2(d,d))] SZS status Unsatisfiable