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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)

Gamma_1: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)

Gamma_2: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)

Gamma_3: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)

Gamma_4: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)

Gamma_5: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5

Gamma_6: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5

Gamma_7: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5

Gamma_8: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)

Gamma_9: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)

Gamma_10: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)

Gamma_11: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)

Gamma_12: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2

Gamma_13: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5

Gamma_14: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6

Gamma_15: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0

Gamma_16: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0

Gamma_17: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0

Gamma_18: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)

Gamma_19: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0

Gamma_20: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0

Gamma_21: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0

Gamma_22: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0

Gamma_23: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0

Gamma_24: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0

Gamma_25: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0

Gamma_26: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0

Gamma_27: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)

Gamma_28: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)

Gamma_29: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]

Gamma_30: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)

Gamma_31: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)

Gamma_32: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)

Gamma_33: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)

Gamma_34: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)

Gamma_35: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  35: ~(ssSkP3(a312)), [ndr1_1(a312)], ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)

Gamma_36: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  35: ~(ssSkP3(a312)), [ndr1_1(a312)], ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  36: ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC1, ~(ndr1_0)

Gamma_37: (right-split)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  35: ~(ssSkP3(a312)), [ndr1_1(a312)], ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  36: top(X0) != a307 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC1, ~(
ndr1_0)

Gamma_38: (extend-no-conflict)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  35: ~(ssSkP3(a312)), [ndr1_1(a312)], ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  36: top(X0) != a307 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC1, ~(
ndr1_0)
  37: [c2_2(a292,a305)], ~(c3_2(a292,a305)), ~(c5_2(a292,a305)), c1_1(
a312), c3_1(a312), ~(ndr1_1(a292)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  0: [c4_2(X0,a284)], ssSkP1(X0)
  1: [c4_2(X0,a289)], ssSkP2(X0)
  2: [c4_2(X0,a305)], ssSkP3(X0)
  3: [c3_2(X0,a305)], ssSkP3(X0)
  4: [c5_2(X0,a305)], ssSkP3(X0)
  5: [c4_2(a307,a308)], ssSkC5
  6: [c3_2(a307,a308)], ssSkC5
  7: [c5_2(a307,a308)], ssSkC5
  8: [ssSkP0(X0)], ndr1_1(X0)
  9: [ssSkP1(X0)], ndr1_1(X0)
  10: [ssSkP2(X0)], ndr1_1(X0)
  11: [ssSkP3(X0)], ndr1_1(X0)
  12: [c3_1(a294)], ssSkC2
  13: [ndr1_1(a307)], ssSkC5
  14: [c4_1(a312)], ssSkC6
  15: [c1_0], c4_0, c3_0
  16: [c3_2(a297,a298)], ~(c1_0), c3_0
  17: [c2_2(a297,a298)], ~(c1_0), c3_0
  18: [c2_1(a277)], c5_0, ~(c1_0)
  19: [c2_1(a297)], ~(c1_0), c3_0
  20: [ndr1_1(a297)], ~(c1_0), c3_0
  21: [c5_0], ~(c1_0), ndr1_0
  22: [c2_1(a311)], ~(c5_0), c4_0
  23: ~(c5_0), [c3_0], ndr1_0
  24: ~(c5_0), [c4_0], ndr1_0
  25: [ssSkC2], ndr1_0
  26: [ssSkC3], ndr1_0
  27: [c3_1(a296)], ~(ssSkC2), ~(ssSkC3)
  28: [c4_1(a296)], ~(ssSkC2), ~(ssSkC3)
  29: ~(ssSkC2), ~(ssSkC3), [ndr1_0]
  30: [c4_2(a296,a306)], ~(ssSkP3(a296)), ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  31: [c4_2(a312,a306)], ~(ssSkP3(a312)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  32: [c3_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  33: [c1_2(X0,a285)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC1, ~(ndr1_0)
  34: ~(ssSkP3(a296)), [ndr1_1(a296)], ~(c4_1(a296)), ~(c3_0), ~(ndr1_0)
  35: ~(ssSkP3(a312)), [ndr1_1(a312)], ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)
  36: top(X0) != a307 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC1, ~(
ndr1_0)
  37: [c2_2(a292,a305)], ~(c3_2(a292,a305)), ~(c5_2(a292,a305)), c1_1(
a312), c3_1(a312), ~(ndr1_1(a292)), ~(c4_1(a312)), ~(c3_0), ~(ndr1_0)

SZS status Satisfiable