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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0

Gamma_1: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0

Gamma_2: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0

Gamma_3: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0

Gamma_4: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0

Gamma_5: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0

Gamma_6: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0

Gamma_7: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0

Gamma_8: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0

Gamma_9: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0

Gamma_10: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0

Gamma_11: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)

Gamma_12: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)

Gamma_13: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)

Gamma_14: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)

Gamma_15: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)

Gamma_16: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)

Gamma_17: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)

Gamma_18: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)

Gamma_19: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)

Gamma_20: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)

Gamma_21: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0

Gamma_22: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]

Gamma_23: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)

Gamma_24: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)

Gamma_25: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)

Gamma_26: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)

Gamma_27: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)

Gamma_28: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)

Gamma_29: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_30: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)

Gamma_31: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)

Gamma_32: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)

Gamma_33: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  33: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_34: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  33: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  34: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)

Gamma_35: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  33: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  34: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  35: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)

Gamma_36: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  33: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  34: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  35: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  36: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_37: (extend-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  24: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  25: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  26: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  27: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  28: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  29: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  30: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  31: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  32: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  33: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  34: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  35: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  36: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  37: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)

Gamma_38: (move)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,a762), c5_2(a769,X0), c5_1(
a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  25: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  26: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  27: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  28: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  29: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  30: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  31: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  32: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  33: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  34: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  35: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  36: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  37: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_39: (right-split)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c2_2(a769,a770)], c3_2(a772,a762), c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_40: (right-split)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c2_2(a769,a770)], c3_2(a772,a762), c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_41: (resolve)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: [~(c1_2(a769,a770))], c3_2(a772,a762), c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_42: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)

Gamma_43: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)

Gamma_44: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]

Gamma_45: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)

Gamma_46: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)

Gamma_47: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)

Gamma_48: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)
  44: [c4_1(a731)]

Gamma_49: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)
  44: [c4_1(a731)]
  45: [c1_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)

Gamma_50: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)
  44: [c4_1(a731)]
  45: [c1_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  46: [c4_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)

Gamma_51: (extend-no-conflict)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)
  44: [c4_1(a731)]
  45: [c1_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  46: [c4_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  47: [c5_1(a731)], ndr1_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  0: [c5_2(a772,a773)], c3_1(a774), c1_0
  1: [c3_1(a774)], c2_1(a772), c1_0
  2: [c4_1(a771)], c1_0, c4_0
  3: [c2_1(a772)], c1_0, ndr1_0
  4: [c5_1(a772)], c1_0, ndr1_0
  5: [ndr1_1(a772)], c1_0, ndr1_0
  6: [c1_0], c4_0, ndr1_0
  7: [c5_2(a736,a737)], ~(c1_0), c2_0
  8: [ndr1_1(a736)], ~(c1_0), c2_0
  9: [c4_1(a736)], ~(c1_0), c2_0
  10: ~(c1_0), [c2_0], ndr1_0
  11: [c4_1(a757)], ~(c2_0)
  12: [c3_0], ~(c2_0)
  13: [c2_2(a726,a727)], c4_1(a729), ~(c3_0)
  14: [c4_2(a726,a727)], c4_1(a729), ~(c3_0)
  15: [c2_2(a726,a728)], c4_1(a729), ~(c3_0)
  16: [c4_2(a769,a770)], ~(c1_0), ~(c3_0)
  17: [c3_2(a769,a770)], ~(c1_0), ~(c3_0)
  18: [ndr1_1(a726)], c4_1(a729), ~(c3_0)
  19: [ndr1_1(a769)], ~(c1_0), ~(c3_0)
  20: [c1_2(a769,X0)], c4_2(a769,X0), c3_2(a769,X0), ~(ndr1_1(a769)), ~(
c1_0), ~(c3_0)
  21: [c4_1(a729)], ~(c3_0), ndr1_0
  22: ~(c1_0), ~(c3_0), [ndr1_0]
  23: [~(c2_2(a769,a770))], ~(c1_0), ~(c3_0)
  24: ~(c1_2(a769,a770)), [c3_2(a772,a762)], c5_2(a769,a770), c5_1(a769), ~(
ndr1_1(a769)), ~(c2_1(a772)), ~(c1_0), ~(c3_0), ~(ndr1_0)
  25: top(X0) != a770 | ~(c1_2(a769,X0)), [c2_2(a769,X0)], c3_2(a772,
a762), c5_2(a769,X0), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  26: [c1_2(a726,a727)], c4_2(a759,a760), ~(c4_2(a726,a727)), c5_2(a726,
a758), c1_1(a726), ~(ndr1_1(a726)), ~(ndr1_0)
  27: [c1_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  28: [c1_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  29: ~(c1_2(a736,a735)), [c2_2(a736,a735)], c3_2(a772,a762), c5_2(a736,
a735), c5_1(a736), ~(ndr1_1(a736)), ~(c2_1(a772)), ~(ndr1_0)
  30: [c1_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  31: [c1_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  32: [c4_2(a729,a735)], c5_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  33: [c4_2(a736,a735)], c5_1(a736), c4_1(a734), ~(c4_1(a736)), ~(ndr1_0)
  34: [c4_2(a771,a735)], c5_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  35: [c4_2(a757,a735)], c5_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  36: [c5_1(a729)], ndr1_1(a729), c4_1(a734), ~(c4_1(a729)), ~(ndr1_0)
  37: [c5_1(a771)], ndr1_1(a771), c4_1(a734), ~(c4_1(a771)), ~(ndr1_0)
  38: [c5_1(a757)], ndr1_1(a757), c4_1(a734), ~(c4_1(a757)), ~(ndr1_0)
  39: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a772,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a772)), ~(ndr1_0)
  40: [c2_1(a731)]
  41: ~(c1_2(a769,a770)), c2_2(a769,a770), [c3_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  42: ~(c1_2(a769,a770)), c2_2(a769,a770), [c2_2(a731,a762)], c5_2(a769,
a770), c5_1(a769), ~(ndr1_1(a769)), ~(c2_1(a731)), ~(ndr1_0)
  43: ~(c1_2(a769,a770)), c2_2(a769,a770), [c5_2(a769,a770)], c5_1(a769), ~(
ndr1_1(a769)), ndr1_1(a731), ~(c2_1(a731)), ~(ndr1_0)
  44: [c4_1(a731)]
  45: [c1_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  46: [c4_2(a731,a735)], c5_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)
  47: [c5_1(a731)], ndr1_1(a731), c4_1(a734), ~(c4_1(a731)), ~(ndr1_0)

SZS status Satisfiable