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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2

Gamma_1: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8

Gamma_2: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8

Gamma_3: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0

Gamma_4: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0

Gamma_5: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0

Gamma_6: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0

Gamma_7: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2

Gamma_8: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2

Gamma_9: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4

Gamma_10: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7

Gamma_11: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7

Gamma_12: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8

Gamma_13: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8

Gamma_14: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0

Gamma_15: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0

Gamma_16: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0

Gamma_17: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0

Gamma_18: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0

Gamma_19: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0

Gamma_20: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0

Gamma_21: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0

Gamma_22: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)

Gamma_23: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)

Gamma_24: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)

Gamma_25: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)

Gamma_26: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0

Gamma_27: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0

Gamma_28: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)

Gamma_29: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]

Gamma_30: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)

Gamma_31: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)

Gamma_32: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)

Gamma_33: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)

Gamma_34: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(a495), ~(
ndr1_1(a495)), ssSkC1, ~(ndr1_0)

Gamma_35: (right-split)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)

Gamma_36: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)

Gamma_37: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  36: [c4_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)

Gamma_38: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  36: [c4_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  37: [c4_0], c1_0

Gamma_39: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  36: [c4_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  37: [c4_0], c1_0
  38: [c1_1(a512)], ~(ssSkC6), ~(c4_0)

Gamma_40: (extend-no-conflict)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  36: [c4_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  37: [c4_0], c1_0
  38: [c1_1(a512)], ~(ssSkC6), ~(c4_0)
  39: [c4_1(a512)], ~(ssSkC6), ~(c4_0)
  0: [c1_2(a500,a501)], ssSkC2
  1: [c5_2(a517,a518)], ssSkC8
  2: [c3_2(a517,a518)], ssSkC8
  3: [c2_2(a495,a496)], c3_0
  4: [c4_2(a495,a496)], c3_0
  5: [c5_1(a492)], ssSkC0
  6: [ndr1_1(a492)], ssSkC0
  7: [c3_1(a500)], ssSkC2
  8: [ndr1_1(a500)], ssSkC2
  9: [c3_1(a507)], ssSkC4
  10: [c3_1(a513)], ssSkC7
  11: [c1_1(a513)], ssSkC7
  12: [c4_1(a517)], ssSkC8
  13: [ndr1_1(a517)], ssSkC8
  14: [c2_1(a495)], c3_0
  15: [ndr1_1(a495)], c3_0
  16: [ssSkC0], ndr1_0
  17: [ssSkC2], ndr1_0
  18: [ssSkC4], ndr1_0
  19: [ssSkC5], ndr1_0
  20: [ssSkC6], ndr1_0
  21: [ssSkC7], ndr1_0
  22: [c2_2(a514,a515)], c2_0, ~(ssSkC7)
  23: [c3_2(a514,a515)], c2_0, ~(ssSkC7)
  24: [c1_1(a514)], c2_0, ~(ssSkC7)
  25: [ndr1_1(a514)], c2_0, ~(ssSkC7)
  26: [c2_0], ~(ssSkC7), ndr1_0
  27: [ssSkC8], ndr1_0
  28: [c1_1(a519)], ~(c2_0), ~(ssSkC8)
  29: ~(c2_0), ~(ssSkC8), [ndr1_0]
  30: [c1_2(a495,a496)], c5_2(a495,a502), c3_2(a495,a496), ~(c4_2(a495,a496)), c5_1(
a495), ~(ndr1_1(a495)), ~(c2_0), ~(ssSkC2), ~(ndr1_0)
  31: [c1_2(a514,X0)], c3_2(a514,a497), c2_2(a514,X0), c3_1(a514), ~(
ndr1_1(a514)), ssSkC1, ~(ndr1_0)
  32: [c1_2(a492,X0)], c3_2(a492,a497), c2_2(a492,X0), c3_1(a492), ~(
ndr1_1(a492)), ssSkC1, ~(ndr1_0)
  33: [c1_2(a517,X0)], c3_2(a517,a497), c2_2(a517,X0), c3_1(a517), ~(
ndr1_1(a517)), ssSkC1, ~(ndr1_0)
  34: top(X0) != a496 | [c1_2(a495,X0)], c3_2(a495,a497), c2_2(a495,X0), c3_1(
a495), ~(ndr1_1(a495)), ssSkC1, ~(ndr1_0)
  35: [c5_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  36: [c4_2(a492,a506)], ~(c5_1(a492)), c4_1(a492), ssSkC3, ~(ndr1_0)
  37: [c4_0], c1_0
  38: [c1_1(a512)], ~(ssSkC6), ~(c4_0)
  39: [c4_1(a512)], ~(ssSkC6), ~(c4_0)

SZS status Satisfiable