%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-
not ground preserving

Gamma_0: (extend-no-conflict)
  0: [d(exist)]

Gamma_1: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]

Gamma_2: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)

Gamma_3: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)
  3: ~(s(exist,u3r2(exist))), [r(exist,u3r2(exist))], ~(c(exist))

Gamma_4: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)
  3: ~(s(exist,u3r2(exist))), [r(exist,u3r2(exist))], ~(c(exist))
  4: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))

Gamma_5: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)
  3: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))
  4: ~(s(exist,u3r2(exist))), [r(exist,u3r2(exist))], ~(c(exist))

Gamma_6: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)
  3: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))
  4: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))

Gamma_7: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [s(X0,u3r2(X0))], s1most(X0)
  3: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))
  4: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))

Gamma_8: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s(X0,u3r2(X0))], s1most(X0)
  4: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))

Gamma_9: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: top(X0) != exist | [s(exist,u3r2(exist))], s1most(exist)
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))

Gamma_10: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s(exist,u3r2(exist))], s1most(exist)
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: ~(s(exist,u3r2(exist))), [~(r(exist,u3r2(exist)))], ~(d(exist))

Gamma_11: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)

Gamma_12: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)

Gamma_13: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)

Gamma_14: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))

Gamma_15: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  7: ~(s(exist,u3r1(exist))), [r(exist,u3r1(exist))], ~(c(exist))

Gamma_16: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  7: ~(s(exist,u3r1(exist))), [r(exist,u3r1(exist))], ~(c(exist))
  8: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))

Gamma_17: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  7: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))
  8: ~(s(exist,u3r1(exist))), [r(exist,u3r1(exist))], ~(c(exist))

Gamma_18: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  7: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))
  8: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))

Gamma_19: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [s(X0,u3r1(X0))], s1most(X0)
  6: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  7: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))
  8: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))

Gamma_20: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: [s(X0,u3r1(X0))], s1most(X0)
  7: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  8: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))

Gamma_21: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist | [s(exist,u3r1(exist))], s1most(exist)
  7: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  8: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  9: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))

Gamma_22: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: [s(exist,u3r1(exist))], s1most(exist)
  7: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  8: [equalish(u3r1(exist),u3r1(exist))], ~(s(exist,u3r1(exist))), ~(
s1most(exist))
  9: ~(s(exist,u3r1(exist))), [~(r(exist,u3r1(exist)))], ~(d(exist))

Gamma_23: (resolve+delete)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)

Gamma_24: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)

Gamma_25: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [s(exist,u1r2(exist))], ~(r(exist,u1r2(exist))), ~(c(exist))

Gamma_26: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [s(exist,u1r2(exist))], ~(r(exist,u1r2(exist))), ~(c(exist))
  9: [equalish(u1r2(exist),u1r2(exist))], ~(s(exist,u1r2(exist))), ~(
s1most(exist))

Gamma_27: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [s(exist,u1r2(exist))], ~(r(exist,u1r2(exist))), ~(c(exist))
  9: [equalish(u1r2(exist),u1r2(exist))], ~(s(exist,u1r2(exist))), ~(
s1most(exist))
  10: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))

Gamma_28: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))
  9: [s(exist,u1r2(exist))], ~(r(exist,u1r2(exist))), ~(c(exist))
  10: [equalish(u1r2(exist),u1r2(exist))], ~(s(exist,u1r2(exist))), ~(
s1most(exist))

Gamma_29: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))
  9: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))

Gamma_30: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [r(X0,u1r2(X0))], r1most(X0)
  8: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))
  9: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))

Gamma_31: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r(X0,u1r2(X0))], r1most(X0)
  9: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))

Gamma_32: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: top(X0) != exist | [r(exist,u1r2(exist))], r1most(exist)
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))

Gamma_33: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r(exist,u1r2(exist))], r1most(exist)
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(s(exist,u1r2(exist)))], ~(r(exist,u1r2(exist))), ~(d(exist))

Gamma_34: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)

Gamma_35: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)

Gamma_36: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)

Gamma_37: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))

Gamma_38: (extend-no-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  12: [s(exist,u1r1(exist))], ~(r(exist,u1r1(exist))), ~(c(exist))

Gamma_39: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  12: [s(exist,u1r1(exist))], ~(r(exist,u1r1(exist))), ~(c(exist))
  13: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))

Gamma_40: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  12: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))
  13: [s(exist,u1r1(exist))], ~(r(exist,u1r1(exist))), ~(c(exist))

Gamma_41: (resolve)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  12: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))
  13: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))

Gamma_42: (extend-conflict)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [r(X0,u1r1(X0))], r1most(X0)
  11: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  12: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))
  13: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))

Gamma_43: (move)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))
  11: [r(X0,u1r1(X0))], r1most(X0)
  12: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  13: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))

Gamma_44: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))
  11: top(X0) != exist | [r(exist,u1r1(exist))], r1most(exist)
  12: top(X0) != exist & top(X0) != exist | [r(X0,u1r1(X0))], r1most(
X0)
  13: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  14: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))

Gamma_45: (right-split)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))
  11: [r(exist,u1r1(exist))], r1most(exist)
  12: top(X0) != exist & top(X0) != exist | [r(X0,u1r1(X0))], r1most(
X0)
  13: [equalish(u1r1(exist),u1r1(exist))], ~(r(exist,u1r1(exist))), ~(
r1most(exist))
  14: [~(s(exist,u1r1(exist)))], ~(r(exist,u1r1(exist))), ~(d(exist))

Gamma_46: (resolve+delete)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))
  11: top(X0) != exist & top(X0) != exist | [r(X0,u1r1(X0))], r1most(
X0)
  0: [d(exist)]
  1: [c(exist)]
  2: [~(s(exist,u3r2(exist)))], ~(d(exist)), ~(c(exist))
  3: [s1most(exist)], ~(d(exist)), ~(c(exist))
  4: top(X0) != exist & top(X0) != exist | [s(X0,u3r2(X0))], s1most(X0)
  5: [~(s(exist,u3r1(exist)))], ~(d(exist)), ~(c(exist))
  6: top(X0) != exist & top(X0) != exist | [s(X0,u3r1(X0))], s1most(X0)
  7: [~(r(exist,u1r2(exist)))], ~(d(exist)), ~(c(exist))
  8: [r1most(exist)], ~(d(exist)), ~(c(exist))
  9: top(X0) != exist & top(X0) != exist | [r(X0,u1r2(X0))], r1most(X0)
  10: [~(r(exist,u1r1(exist)))], ~(d(exist)), ~(c(exist))
  11: top(X0) != exist & top(X0) != exist | [r(X0,u1r1(X0))], r1most(
X0)

SZS status Satisfiable