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

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [b], a

Gamma_1: (extend-no-conflict)
  0: [b], a
  1: [c], e, ~(b)

Gamma_2: (extend-no-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a

Gamma_3: (extend-no-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a
  3: [e], ~(d)

Gamma_4: (extend-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a
  3: [e], ~(d)
  4: ~(c), [~(e)], ~(b)

Gamma_5: (move)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a
  3: ~(c), [~(e)], ~(b)
  4: [e], ~(d)

Gamma_6: (resolve)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a
  3: ~(c), [~(e)], ~(b)
  4: ~(c), [~(d)], ~(b)

Gamma_7: (extend-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [d], a
  3: ~(c), [~(e)], ~(b)
  4: ~(c), [~(d)], ~(b)

Gamma_8: (move)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(c), [d], a
  4: ~(c), [~(e)], ~(b)

Gamma_9: (resolve)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: [~(c)], ~(b), a
  4: ~(c), [~(e)], ~(b)

Gamma_10: (extend-no-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(c), ~(b), [a]
  4: ~(c), [~(e)], ~(b)

Gamma_11: (extend-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(c), ~(b), [a]
  4: ~(c), [~(e)], ~(b)
  5: ~(b), [~(a)]

Gamma_12: (move)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(b), [~(a)]
  4: ~(c), ~(b), [a]
  5: ~(c), [~(e)], ~(b)

Gamma_13: (resolve)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(b), [~(a)]
  4: [~(c)], ~(b)
  5: ~(c), [~(e)], ~(b)

Gamma_14: (extend-conflict)
  0: [b], a
  1: [c], e, ~(b)
  2: ~(c), [~(d)], ~(b)
  3: ~(b), [~(a)]
  4: [~(c)], ~(b)
  5: ~(c), [~(e)], ~(b)

Gamma_15: (move)
  0: [b], a
  1: [~(c)], ~(b)
  2: [c], e, ~(b)
  3: ~(c), [~(d)], ~(b)
  4: ~(b), [~(a)]
  5: ~(c), [~(e)], ~(b)

Gamma_16: (resolve)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]

Gamma_17: (extend-no-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]

Gamma_18: (extend-no-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: ~(e), [d]

Gamma_19: (extend-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: ~(e), [d]
  5: c, [~(d)], a

Gamma_20: (move)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: c, [~(d)], a
  5: ~(e), [d]

Gamma_21: (resolve)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: c, [~(d)], a
  5: c, [~(e)], a

Gamma_22: (extend-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: c, [~(d)], a
  5: c, ~(e), [a]

Gamma_23: (resolve)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: c, [~(d)], a
  5: [c], ~(e), ~(b)

Gamma_24: (extend-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: [e], ~(b)
  3: ~(b), [~(a)]
  4: c, [~(d)], a
  5: c, [~(e)], ~(b)

Gamma_25: (move)
  0: [b], a
  1: [~(c)], ~(b)
  2: c, [~(e)], ~(b)
  3: [e], ~(b)
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_26: (resolve)
  0: [b], a
  1: [~(c)], ~(b)
  2: c, [~(e)], ~(b)
  3: c, [~(b)]
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_27: (extend-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: c, [~(e)], ~(b)
  3: [c], ~(b)
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_28: (resolve)
  0: [b], a
  1: [~(c)], ~(b)
  2: c, [~(e)], ~(b)
  3: [~(b)]
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_29: (extend-conflict)
  0: [b], a
  1: [~(c)], ~(b)
  2: c, [~(e)], ~(b)
  3: [~(b)]
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_30: (move)
  0: [~(b)]
  1: [b], a
  2: [~(c)], ~(b)
  3: c, [~(e)], ~(b)
  4: ~(b), [~(a)]
  5: c, [~(d)], a

Gamma_31: (resolve)
  0: [~(b)]
  1: [a]

Gamma_32: (extend-no-conflict)
  0: [~(b)]
  1: [a]

Gamma_33: (extend-no-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)

Gamma_34: (extend-no-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b

Gamma_35: (extend-no-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b
  4: ~(e), [d]

Gamma_36: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b
  4: ~(e), [d]
  5: ~(c), [~(d)], ~(a)

Gamma_37: (move)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b
  4: ~(c), [~(d)], ~(a)
  5: ~(e), [d]

Gamma_38: (resolve)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b
  4: ~(c), [~(d)], ~(a)
  5: ~(c), [~(e)], ~(a)

Gamma_39: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [e], b
  4: ~(c), [~(d)], ~(a)
  5: ~(c), [~(e)], ~(a)

Gamma_40: (move)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [~(e)], ~(a)
  4: ~(c), [e], b
  5: ~(c), [~(d)], ~(a)

Gamma_41: (resolve)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [~(e)], ~(a)
  4: [~(c)], b, ~(a)
  5: ~(c), [~(d)], ~(a)

Gamma_42: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [c], d, ~(a)
  3: ~(c), [~(e)], ~(a)
  4: [~(c)], b, ~(a)
  5: ~(c), [~(d)], ~(a)

Gamma_43: (move)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [c], d, ~(a)
  4: ~(c), [~(e)], ~(a)
  5: ~(c), [~(d)], ~(a)

Gamma_44: (resolve)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)

Gamma_45: (extend-no-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)

Gamma_46: (extend-no-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)
  4: [e], ~(d)

Gamma_47: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)
  4: [e], ~(d)
  5: c, [~(e)], b

Gamma_48: (move)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)
  4: c, [~(e)], b
  5: [e], ~(d)

Gamma_49: (resolve)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)
  4: c, [~(e)], b
  5: c, [~(d)], b

Gamma_50: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: [d], b, ~(a)
  4: c, [~(e)], b
  5: c, [~(d)], b

Gamma_51: (move)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: c, [~(d)], b
  4: [d], b, ~(a)
  5: c, [~(e)], b

Gamma_52: (resolve)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: c, [~(d)], b
  4: c, [b], ~(a)
  5: c, [~(e)], b

Gamma_53: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: c, [~(d)], b
  4: [c], b, ~(a)
  5: c, [~(e)], b

Gamma_54: (resolve)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: c, [~(d)], b
  4: [b], ~(a)
  5: c, [~(e)], b

Gamma_55: (extend-conflict)
  0: [~(b)]
  1: [a]
  2: [~(c)], b, ~(a)
  3: c, [~(d)], b
  4: b, [~(a)]
  5: c, [~(e)], b

Gamma_56: (move)
  0: [~(b)]
  1: b, [~(a)]
  2: [a]
  3: [~(c)], b, ~(a)
  4: c, [~(d)], b
  5: c, [~(e)], b

Gamma_57: (resolve)
  0: [~(b)]
  1: b, [~(a)]
  2: [b]

Gamma_58: (extend-conflict)
  0: [~(b)]
  1: b, [~(a)]
  2: [b]

Gamma_59: (resolve)
  0: [~(b)]
  1: b, [~(a)]
  2: []

SZS status Unsatisfiable