%---------------- 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))

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(e,e,e)], ~(p2(e,e,e))

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(e,e,e)], ~(p2(e,e,e))
  6: [r3(X0,X0,X0)], ~(p2(X0,X0,X0))

Gamma_8: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(p2(X0,X0,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: [p4(X0,X0,X0)], ~(p4(e,e,e)), ~(r3(X0,X0,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: ~(p2(X0,X0,X0)), [k3(X0,X0,X0)]

Gamma_18: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: [q1(X0,X0,X0)], ~(m0(X0,d,X0))

Gamma_20: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: [m1(X0,d,X0)], ~(m0(d,d,X0))

Gamma_23: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))

Gamma_25: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))

Gamma_27: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: ~(p3(X0,X0,X0)), [l4(X0)]

Gamma_31: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: ~(p2(X0,X0,X0)), [n3(X0)]

Gamma_34: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: [q5(X0,X0)], ~(l4(X0))

Gamma_38: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))

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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: [m0(a,X0,a)]

Gamma_40: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: top(X0) != d | [m0(a,X0,a)]

Gamma_41: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: top(X0) != d | [m0(a,X0,a)]
  30: [~(m0(a,e,a))]

Gamma_42: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: [~(m0(a,e,a))]
  30: top(X0) != d | [m0(a,X0,a)]

Gamma_43: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: [~(m0(a,e,a))]
  30: [m0(a,e,a)]
  31: top(X0) != e | [m0(a,X0,a)]

Gamma_44: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: [~(m0(a,e,a))]
  30: [m0(a,e,a)]
  31: top(X0) != e | [m0(a,X0,a)]

Gamma_45: (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(e,e,e)], ~(p2(e,e,e))
  6: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  7: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  8: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  9: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(m3(X0,X0,X0)), ~(
p2(X0,X0,X0))
  10: [p4(e,e,e)], ~(p3(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  12: ~(p2(e,e,e)), [k3(e,e,e)]
  13: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  14: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,d,X0))
  15: [m1(X0,X0,X0)], ~(m0(X1,d,X0))
  16: top(X0) != d | [m1(X0,d,X0)], ~(m0(d,d,X0))
  17: [q2(c,c,c)], ~(q1(e,c,c))
  18: ~(q2(c,c,c)), ~(m3(c,c,c)), ~(k3(c,c,c)), [q4(c,c)]
  19: [n1(d,c,d)], ~(m0(X0,d,c))
  20: ~(q1(e,X0,X0)), [k2(X0,X0)]
  21: ~(p3(e,e,e)), [l4(e)]
  22: ~(m0(e,d,d)), ~(l4(e)), [l4(d)]
  23: top(X0) != e | ~(p3(X0,X0,X0)), [l4(X0)]
  24: ~(p2(e,e,e)), [n3(e)]
  25: top(X0) != e | ~(p2(X0,X0,X0)), [n3(X0)]
  26: ~(q4(c,c)), [q5(c,c)]
  27: ~(q4(c,c)), [n5(c,c)]
  28: top(X0) != c & top(X0) != c | [q5(X0,X0)], ~(l4(X0))
  29: [~(m0(a,e,a))]
  30: []
  31: top(X0) != e | [m0(a,X0,a)]

SZS status Unsatisfiable