%---------------- 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-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: [~(q1(b,b,b))]

Gamma_22: (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: [~(q1(b,b,b))]
  15: top(X0) != e | [q1(X0,X0,X0)], ~(m0(X0,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: [~(q1(b,b,b))]
  15: top(X0) != b & top(X0) != b | [q1(b,b,b)], ~(m0(b,d,b))
  16: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

Gamma_24: (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: [~(q1(b,b,b))]
  15: [q1(b,b,b)], ~(m0(b,d,b))
  16: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

Gamma_25: (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: [~(q1(b,b,b))]
  15: [~(m0(b,d,b))]
  16: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

Gamma_26: (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: [~(q1(b,b,b))]
  15: [~(m0(b,d,b))]
  16: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

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

Gamma_28: (right-split)
  0: [~(m0(b,d,b))]
  1: [m0(b,d,b)]
  2: top(X0) != b | [m0(X0,d,b)]
  3: top(X1) != b | [m0(b,d,X0)]
  4: top(X1) != b & top(X0) != b | [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(e,e,e)], ~(p2(e,e,e))
  10: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(
p2(X0,X0,X0))
  11: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  12: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  13: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(
m3(X0,X0,X0)), ~(p2(X0,X0,X0))
  14: [p4(e,e,e)], ~(p3(e,e,e))
  15: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  16: ~(p2(e,e,e)), [k3(e,e,e)]
  17: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  18: [~(q1(b,b,b))]
  19: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

Gamma_29: (right-split)
  0: [~(m0(b,d,b))]
  1: [m0(b,d,b)]
  2: top(X0) != b | [m0(X0,d,b)]
  3: top(X1) != b | [m0(b,d,X0)]
  4: top(X1) != b & top(X0) != b | [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(e,e,e)], ~(p2(e,e,e))
  10: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(
p2(X0,X0,X0))
  11: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  12: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  13: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(
m3(X0,X0,X0)), ~(p2(X0,X0,X0))
  14: [p4(e,e,e)], ~(p3(e,e,e))
  15: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  16: ~(p2(e,e,e)), [k3(e,e,e)]
  17: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  18: [~(q1(b,b,b))]
  19: top(X0) != b & top(X0) != b & top(X0) != b | [q1(X0,X0,X0)], ~(
m0(X0,d,X0))

Gamma_30: (resolve)
  0: [~(m0(b,d,b))]
  1: []
  2: top(X0) != b | [m0(X0,d,b)]
  3: top(X1) != b | [m0(b,d,X0)]
  4: top(X1) != b & top(X0) != b | [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(e,e,e)], ~(p2(e,e,e))
  8: top(X0) != e & top(X0) != e & top(X0) != e | [r3(X0,X0,X0)], ~(p2(X0,X0,X0))
  9: [m3(X0,X0,X0)], ~(p2(X0,X0,X0))
  10: [p3(e,e,e)], ~(m3(e,e,e)), ~(p2(e,e,e))
  11: top(X0) != e & top(X0) != e & top(X0) != e | [p3(X0,X0,X0)], ~(
m3(X0,X0,X0)), ~(p2(X0,X0,X0))
  12: [p4(e,e,e)], ~(p3(e,e,e))
  13: top(X0) != e & top(X0) != e & top(X0) != e | [p4(X0,X0,X0)], ~(
p4(e,e,e)), ~(r3(X0,X0,X0))
  14: ~(p2(e,e,e)), [k3(e,e,e)]
  15: top(X0) != e & top(X0) != e & top(X0) != e | ~(p2(X0,X0,X0)), [k3(
X0,X0,X0)]
  16: [~(q1(b,b,b))]

SZS status Unsatisfiable