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

------ Parsing...successful


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

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

Gamma_1: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]

Gamma_2: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]

Gamma_3: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))

Gamma_4: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))

Gamma_5: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))

Gamma_6: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))

Gamma_7: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))

Gamma_8: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))

Gamma_9: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]

Gamma_10: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))

Gamma_11: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))

Gamma_12: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))

Gamma_13: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]

Gamma_14: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))

Gamma_15: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]

Gamma_16: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))

Gamma_17: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))

Gamma_18: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))

Gamma_19: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))

Gamma_20: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))

Gamma_21: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))

Gamma_22: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]

Gamma_23: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))

Gamma_24: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))

Gamma_25: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))

Gamma_26: (extend-no-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  26: ~(q_2_2(a,a)), ~(q_1_1(a,a)), [p_1_2(a,a)]

Gamma_27: (extend-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  26: ~(q_2_2(a,a)), ~(q_1_1(a,a)), [p_1_2(a,a)]
  27: [~(p_1_2(a,a))]

Gamma_28: (move)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  26: [~(p_1_2(a,a))]
  27: ~(q_2_2(a,a)), ~(q_1_1(a,a)), [p_1_2(a,a)]

Gamma_29: (resolve)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  26: [~(p_1_2(a,a))]
  27: [~(q_2_2(a,a))], ~(q_1_1(a,a))

Gamma_30: (extend-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  25: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  26: [~(p_1_2(a,a))]
  27: ~(q_2_2(a,a)), [~(q_1_1(a,a))]

Gamma_31: (move)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: ~(q_2_2(a,a)), [~(q_1_1(a,a))]
  25: [q_1_1(a,a)], ~(nq_2(a)), ~(nq_1(a))
  26: [q_1_2(a,a)], ~(p_2_2(a,a)), ~(q_1_1(a,a))
  27: [~(p_1_2(a,a))]

Gamma_32: (resolve)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: ~(q_2_2(a,a)), [~(q_1_1(a,a))]
  25: ~(q_2_2(a,a)), [~(nq_2(a))], ~(nq_1(a))
  26: [~(p_1_2(a,a))]

Gamma_33: (extend-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  18: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  19: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  20: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  21: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  22: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  23: [p_1_1(a,b)], ~(p_1_2(a,b))
  24: ~(q_2_2(a,a)), [~(q_1_1(a,a))]
  25: [~(q_2_2(a,a))], ~(nq_2(a)), ~(nq_1(a))
  26: [~(p_1_2(a,a))]

Gamma_34: (move)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [~(q_2_2(a,a))], ~(nq_2(a)), ~(nq_1(a))
  18: [q_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  19: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  20: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  21: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  22: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  23: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  24: [p_1_1(a,b)], ~(p_1_2(a,b))
  25: ~(q_2_2(a,a)), [~(q_1_1(a,a))]
  26: [~(p_1_2(a,a))]

Gamma_35: (resolve)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [~(q_2_2(a,a))], ~(nq_2(a)), ~(nq_1(a))
  18: [~(nq_2(a))], ~(nq_1(a))
  19: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  20: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  21: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  22: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  23: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  24: [p_1_1(a,b)], ~(p_1_2(a,b))
  25: [~(p_1_2(a,a))]

Gamma_36: (extend-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: [nq_1(a)]
  16: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  17: [~(q_2_2(a,a))], ~(nq_2(a)), ~(nq_1(a))
  18: ~(nq_2(a)), [~(nq_1(a))]
  19: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  20: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  21: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  22: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  23: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  24: [p_1_1(a,b)], ~(p_1_2(a,b))
  25: [~(p_1_2(a,a))]

Gamma_37: (move)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: ~(nq_2(a)), [~(nq_1(a))]
  16: [nq_1(a)]
  17: [q_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  18: [~(q_2_2(a,a))], ~(nq_2(a)), ~(nq_1(a))
  19: [p_2_2(a,b)], ~(nq_2(b)), ~(nq_1(a))
  20: [p_2_2(a,a)], ~(nq_2(a)), ~(nq_1(a))
  21: [q_1_1(a,b)], ~(nq_2(b)), ~(nq_1(a))
  22: [q_1_2(a,b)], ~(p_2_2(a,b)), ~(q_1_1(a,b))
  23: ~(q_2_2(a,b)), ~(q_1_1(a,b)), [p_1_2(a,b)]
  24: [p_1_1(a,b)], ~(p_1_2(a,b))
  25: [~(p_1_2(a,a))]

Gamma_38: (resolve)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: ~(nq_2(a)), [~(nq_1(a))]
  16: [~(nq_2(a))]
  17: [~(p_1_2(a,a))]

Gamma_39: (extend-conflict)
  0: [nq_2(b)]
  1: [nq_2(a)]
  2: [nq_1(b)]
  3: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  4: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  7: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  8: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  9: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  10: [p_1_1(b,b)], ~(p_1_2(b,b))
  11: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  12: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  13: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  14: [p_1_1(b,a)], ~(p_1_2(b,a))
  15: ~(nq_2(a)), [~(nq_1(a))]
  16: [~(nq_2(a))]
  17: [~(p_1_2(a,a))]

Gamma_40: (move)
  0: [nq_2(b)]
  1: [~(nq_2(a))]
  2: [nq_2(a)]
  3: [nq_1(b)]
  4: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  5: [q_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  6: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  7: [p_2_2(b,a)], ~(nq_2(a)), ~(nq_1(b))
  8: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  9: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  10: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  11: [p_1_1(b,b)], ~(p_1_2(b,b))
  12: [q_1_1(b,a)], ~(nq_2(a)), ~(nq_1(b))
  13: [q_1_2(b,a)], ~(p_2_2(b,a)), ~(q_1_1(b,a))
  14: ~(q_2_2(b,a)), ~(q_1_1(b,a)), [p_1_2(b,a)]
  15: [p_1_1(b,a)], ~(p_1_2(b,a))
  16: ~(nq_2(a)), [~(nq_1(a))]
  17: [~(p_1_2(a,a))]

Gamma_41: (resolve)
  0: [nq_2(b)]
  1: [~(nq_2(a))]
  2: []
  3: [nq_1(b)]
  4: [q_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  5: [p_2_2(b,b)], ~(nq_2(b)), ~(nq_1(b))
  6: [q_1_1(b,b)], ~(nq_2(b)), ~(nq_1(b))
  7: [q_1_2(b,b)], ~(p_2_2(b,b)), ~(q_1_1(b,b))
  8: ~(q_2_2(b,b)), ~(q_1_1(b,b)), [p_1_2(b,b)]
  9: [p_1_1(b,b)], ~(p_1_2(b,b))
  10: [~(p_1_2(a,a))]

SZS status Unsatisfiable