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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [b0], a0

Gamma_1: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)

Gamma_2: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2

Gamma_3: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3

Gamma_4: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]

Gamma_5: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4

Gamma_6: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]

Gamma_7: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5

Gamma_8: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]

Gamma_9: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5

Gamma_10: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4

Gamma_11: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]

Gamma_12: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3

Gamma_13: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]

Gamma_14: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2

Gamma_15: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0

Gamma_16: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: [b1], ~(a1)

Gamma_17: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: [b1], ~(a1)
  17: ~(q1), [~(b1)], ~(b0)

Gamma_18: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: [b1], ~(a1)

Gamma_19: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)

Gamma_20: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)

Gamma_21: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(p1), [a1], a0
  17: ~(q1), [~(b1)], ~(b0)

Gamma_22: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), [~(p1)], ~(b0), a0
  17: ~(q1), [~(b1)], ~(b0)

Gamma_23: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), ~(p1), ~(b0), [a0]
  17: ~(q1), [~(b1)], ~(b0)

Gamma_24: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), ~(p1), ~(b0), [a0]
  17: ~(q1), [~(b1)], ~(b0)
  18: ~(b0), [~(a0)]

Gamma_25: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: ~(q1), ~(p1), ~(b0), [a0]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_26: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: [~(q1)], ~(p1), ~(b0)
  18: ~(q1), [~(b1)], ~(b0)

Gamma_27: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: ~(q1), [~(p1)], ~(b0)
  18: ~(q1), [~(b1)], ~(b0)

Gamma_28: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(p2), [p1], a2
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_29: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), [~(p2)], a2, ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_30: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_31: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: [b2], ~(a2)

Gamma_32: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: [b2], ~(a2)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_33: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [b2], ~(a2)

Gamma_34: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: ~(q2), ~(q1), [~(a2)]

Gamma_35: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: ~(q2), ~(q1), [~(a2)]

Gamma_36: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), ~(p2), [a2], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_37: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q2), [~(q1)], ~(p2), ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_38: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q2), ~(q1), [~(p2)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_39: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(p3), [p2], a3
  14: ~(p3), ~(p2), [a3]
  15: ~(q1), [~(p1)], ~(b0)
  16: ~(q2), ~(q1), [~(a2)]
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_40: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), [~(p3)], a3, ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]

Gamma_41: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]

Gamma_42: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]

Gamma_43: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]
  21: [q5]
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]
  21: [q5]

SZS status Satisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [b0], a0

Gamma_1: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)

Gamma_2: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2

Gamma_3: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3

Gamma_4: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]

Gamma_5: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4

Gamma_6: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]

Gamma_7: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5

Gamma_8: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]

Gamma_9: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5

Gamma_10: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4

Gamma_11: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]

Gamma_12: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3

Gamma_13: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]

Gamma_14: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2

Gamma_15: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0

Gamma_16: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: [b1], ~(a1)

Gamma_17: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: [b1], ~(a1)
  17: ~(q1), [~(b1)], ~(b0)

Gamma_18: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: [b1], ~(a1)

Gamma_19: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)

Gamma_20: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(p1), [a1], a0
  16: ~(q1), [~(b1)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)

Gamma_21: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(p1), [a1], a0
  17: ~(q1), [~(b1)], ~(b0)

Gamma_22: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), [~(p1)], ~(b0), a0
  17: ~(q1), [~(b1)], ~(b0)

Gamma_23: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), ~(p1), ~(b0), [a0]
  17: ~(q1), [~(b1)], ~(b0)

Gamma_24: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(q1), ~(p1), ~(b0), [a0]
  17: ~(q1), [~(b1)], ~(b0)
  18: ~(b0), [~(a0)]

Gamma_25: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: ~(q1), ~(p1), ~(b0), [a0]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_26: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: [~(q1)], ~(p1), ~(b0)
  18: ~(q1), [~(b1)], ~(b0)

Gamma_27: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(p2), [p1], a2
  15: ~(q1), [~(a1)], ~(b0)
  16: ~(b0), [~(a0)]
  17: ~(q1), [~(p1)], ~(b0)
  18: ~(q1), [~(b1)], ~(b0)

Gamma_28: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(p2), [p1], a2
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_29: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), [~(p2)], a2, ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_30: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)

Gamma_31: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: [b2], ~(a2)

Gamma_32: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: [b2], ~(a2)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_33: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [b2], ~(a2)

Gamma_34: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: ~(q2), ~(q1), [~(a2)]

Gamma_35: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q1), ~(p2), [a2], ~(b0)
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: ~(q2), ~(q1), [~(a2)]

Gamma_36: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), ~(p2), [a2], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_37: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q2), [~(q1)], ~(p2), ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_38: (extend-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(p3), [p2], a3
  13: ~(p3), ~(p2), [a3]
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q2), ~(q1), [~(p2)], ~(b0)
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_39: (move)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(p3), [p2], a3
  14: ~(p3), ~(p2), [a3]
  15: ~(q1), [~(p1)], ~(b0)
  16: ~(q2), ~(q1), [~(a2)]
  17: ~(q1), [~(a1)], ~(b0)
  18: ~(b0), [~(a0)]
  19: ~(q1), [~(b1)], ~(b0)
  20: ~(q2), ~(q1), [~(b2)]

Gamma_40: (resolve)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), [~(p3)], a3, ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]

Gamma_41: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]

Gamma_42: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]

Gamma_43: (extend-no-conflict)
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]
  21: [q5]
  0: [b0], a0
  1: [q1], b1, ~(b0)
  2: [q2], ~(q1), b2
  3: [q3], ~(q2), b3
  4: ~(q3), ~(q2), [b3]
  5: [q4], ~(q3), b4
  6: ~(q4), ~(q3), [b4]
  7: ~(q4), [b5], q5
  8: ~(b5), [a5]
  9: [p4], ~(a5), p5
  10: ~(p4), [p3], a4
  11: ~(p4), ~(p3), [a4]
  12: ~(q2), ~(q1), [~(p2)], ~(b0)
  13: ~(q2), ~(q1), ~(p3), [a3], ~(b0)
  14: ~(q1), [~(p1)], ~(b0)
  15: ~(q2), ~(q1), [~(a2)]
  16: ~(q1), [~(a1)], ~(b0)
  17: ~(b0), [~(a0)]
  18: ~(q1), [~(b1)], ~(b0)
  19: ~(q2), ~(q1), [~(b2)]
  20: [p5]
  21: [q5]

SZS status Satisfiable