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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [r]

Gamma_1: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)

Gamma_2: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)

Gamma_3: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)

Gamma_4: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)

Gamma_5: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)

Gamma_6: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]

Gamma_7: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)

Gamma_8: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)

Gamma_9: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)

Gamma_10: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)

Gamma_11: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)

Gamma_12: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]

Gamma_13: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)

Gamma_14: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)

Gamma_15: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)

Gamma_16: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)

Gamma_17: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: ~(p_5), ~(r_5), [p_6]

Gamma_18: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: ~(p_5), ~(r_5), [p_6]
  18: [~(p_6)]

Gamma_19: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: ~(p_5), ~(r_5), [p_6]

Gamma_20: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: [~(p_5)], ~(r_5)

Gamma_21: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: [~(p_5)], ~(r_5)

Gamma_22: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [p_5], ~(p_4), ~(r_4)
  18: [~(p_6)]

Gamma_23: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [~(p_4)], ~(r_5), ~(r_4)
  18: [~(p_6)]

Gamma_24: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [~(p_4)], ~(r_5), ~(r_4)
  18: [~(p_6)]

Gamma_25: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [p_4], ~(p_3), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_26: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_27: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_28: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [p_3], ~(p_2), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_29: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_30: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_31: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [p_2], ~(r_1), ~(p_1)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_32: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)], ~(p_1)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_33: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_34: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: [p_1]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_35: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: [~(r_5)], ~(r_4), ~(r_3), ~(r_2), ~(r_1)
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_36: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_37: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: [r_1], ~(r)
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_38: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r)]
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_39: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_40: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: [r_2], ~(r)
  6: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_41: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), [~(r)]
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_42: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_43: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: [r_3], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_44: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: ~(r_5), ~(r_4), [~(r)]
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_45: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: ~(r_5), [~(r_4)], ~(r)
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_46: (move)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: [r_4], ~(r)
  4: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_47: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: ~(r_5), [~(r)]
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_48: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: [~(r_5)], ~(r)
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_49: (move)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [r_5], ~(r)
  3: ~(r_5), [~(r_4)], ~(r)
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_50: (resolve)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [~(r)]
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_51: (extend-conflict)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [~(r)]
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_52: (move)
  0: [~(r)]
  1: [r]
  2: [~(r_5)], ~(r)
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_53: (resolve)
  0: [~(r)]
  1: []
  2: [q]
  3: [q_5], ~(q)
  4: [q_4], ~(q)
  5: [q_3], ~(q)
  6: [q_2], ~(q)
  7: [q_1], ~(q)
  8: [~(p_6)]

SZS status Unsatisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [r]

Gamma_1: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)

Gamma_2: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)

Gamma_3: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)

Gamma_4: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)

Gamma_5: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)

Gamma_6: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]

Gamma_7: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)

Gamma_8: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)

Gamma_9: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)

Gamma_10: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)

Gamma_11: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)

Gamma_12: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]

Gamma_13: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)

Gamma_14: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)

Gamma_15: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)

Gamma_16: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)

Gamma_17: (extend-no-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: ~(p_5), ~(r_5), [p_6]

Gamma_18: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: ~(p_5), ~(r_5), [p_6]
  18: [~(p_6)]

Gamma_19: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: ~(p_5), ~(r_5), [p_6]

Gamma_20: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: [~(p_5)], ~(r_5)

Gamma_21: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [p_5], ~(p_4), ~(r_4)
  17: [~(p_6)]
  18: [~(p_5)], ~(r_5)

Gamma_22: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [p_5], ~(p_4), ~(r_4)
  18: [~(p_6)]

Gamma_23: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [~(p_4)], ~(r_5), ~(r_4)
  18: [~(p_6)]

Gamma_24: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [p_4], ~(p_3), ~(r_3)
  16: [~(p_5)], ~(r_5)
  17: [~(p_4)], ~(r_5), ~(r_4)
  18: [~(p_6)]

Gamma_25: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [p_4], ~(p_3), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_26: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_27: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [p_3], ~(p_2), ~(r_2)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_28: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [p_3], ~(p_2), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_29: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_30: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [p_2], ~(r_1), ~(p_1)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_31: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [p_2], ~(r_1), ~(p_1)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_32: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)], ~(p_1)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_33: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [p_1]
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_34: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: [p_1]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_35: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: [~(r_5)], ~(r_4), ~(r_3), ~(r_2), ~(r_1)
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_36: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: [r_1], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  13: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_37: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: [r_1], ~(r)
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: ~(r_5), ~(r_4), ~(r_3), ~(r_2), ~(r_1), [~(p_1)]
  14: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  15: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  16: [~(p_4)], ~(r_5), ~(r_4)
  17: [~(p_5)], ~(r_5)
  18: [~(p_6)]

Gamma_38: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r)]
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_39: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: [r_2], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  6: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_40: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: [r_2], ~(r)
  6: ~(r_5), ~(r_4), ~(r_3), ~(r_2), [~(r_1)]
  7: [q]
  8: [q_5], ~(q)
  9: [q_4], ~(q)
  10: [q_3], ~(q)
  11: [q_2], ~(q)
  12: [q_1], ~(q)
  13: [~(p_2)], ~(r_5), ~(r_4), ~(r_3), ~(r_2)
  14: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  15: [~(p_4)], ~(r_5), ~(r_4)
  16: [~(p_5)], ~(r_5)
  17: [~(p_6)]

Gamma_41: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), [~(r)]
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_42: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: [r_3], ~(r)
  4: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  5: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_43: (move)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: [r_3], ~(r)
  5: ~(r_5), ~(r_4), ~(r_3), [~(r_2)], ~(r)
  6: [q]
  7: [q_5], ~(q)
  8: [q_4], ~(q)
  9: [q_3], ~(q)
  10: [q_2], ~(q)
  11: [q_1], ~(q)
  12: [~(p_3)], ~(r_5), ~(r_4), ~(r_3)
  13: [~(p_4)], ~(r_5), ~(r_4)
  14: [~(p_5)], ~(r_5)
  15: [~(p_6)]

Gamma_44: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: ~(r_5), ~(r_4), [~(r)]
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_45: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: [r_4], ~(r)
  3: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  4: ~(r_5), [~(r_4)], ~(r)
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_46: (move)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: [r_4], ~(r)
  4: ~(r_5), ~(r_4), [~(r_3)], ~(r)
  5: [q]
  6: [q_5], ~(q)
  7: [q_4], ~(q)
  8: [q_3], ~(q)
  9: [q_2], ~(q)
  10: [q_1], ~(q)
  11: [~(p_4)], ~(r_5), ~(r_4)
  12: [~(p_5)], ~(r_5)
  13: [~(p_6)]

Gamma_47: (resolve)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: ~(r_5), [~(r)]
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_48: (extend-conflict)
  0: [r]
  1: [r_5], ~(r)
  2: ~(r_5), [~(r_4)], ~(r)
  3: [~(r_5)], ~(r)
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_49: (move)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [r_5], ~(r)
  3: ~(r_5), [~(r_4)], ~(r)
  4: [q]
  5: [q_5], ~(q)
  6: [q_4], ~(q)
  7: [q_3], ~(q)
  8: [q_2], ~(q)
  9: [q_1], ~(q)
  10: [~(p_5)], ~(r_5)
  11: [~(p_6)]

Gamma_50: (resolve)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [~(r)]
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_51: (extend-conflict)
  0: [r]
  1: [~(r_5)], ~(r)
  2: [~(r)]
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_52: (move)
  0: [~(r)]
  1: [r]
  2: [~(r_5)], ~(r)
  3: [q]
  4: [q_5], ~(q)
  5: [q_4], ~(q)
  6: [q_3], ~(q)
  7: [q_2], ~(q)
  8: [q_1], ~(q)
  9: [~(p_6)]

Gamma_53: (resolve)
  0: [~(r)]
  1: []
  2: [q]
  3: [q_5], ~(q)
  4: [q_4], ~(q)
  5: [q_3], ~(q)
  6: [q_2], ~(q)
  7: [q_1], ~(q)
  8: [~(p_6)]

SZS status Unsatisfiable