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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)

Gamma_1: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)

Gamma_2: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0

Gamma_3: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0

Gamma_4: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5

Gamma_5: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)

Gamma_6: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0

Gamma_7: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0

Gamma_8: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1

Gamma_9: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1

Gamma_10: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3

Gamma_11: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5

Gamma_12: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5

Gamma_13: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5

Gamma_14: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0

Gamma_15: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0

Gamma_16: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)

Gamma_17: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)

Gamma_18: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)

Gamma_19: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)

Gamma_20: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0

Gamma_21: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0

Gamma_22: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)

Gamma_23: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]

Gamma_24: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]
  24: c2_2(a192,a193), [c1_2(a192,X0)], c1_2(a192,a217), c1_2(a192,a193), c5_2(
a192,X0), ~(c5_2(a192,a193)), c4_2(a192,X0), c4_1(a192), c1_1(a192), ~(
ndr1_1(a192)), ~(ndr1_0)

Gamma_25: (right-split)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]
  24: top(X0) != a197 | c2_2(a192,a193), [c1_2(a192,X0)], c1_2(a192,a217), c1_2(
a192,a193), c5_2(a192,X0), ~(c5_2(a192,a193)), c4_2(a192,X0), c4_1(a192), c1_1(
a192), ~(ndr1_1(a192)), ~(ndr1_0)

Gamma_26: (extend-no-conflict)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]
  24: top(X0) != a197 | c2_2(a192,a193), [c1_2(a192,X0)], c1_2(a192,a217), c1_2(
a192,a193), c5_2(a192,X0), ~(c5_2(a192,a193)), c4_2(a192,X0), c4_1(a192), c1_1(
a192), ~(ndr1_1(a192)), ~(ndr1_0)
  25: c2_2(a188,a189), [c1_2(a188,X0)], c1_2(a188,a217), c1_2(a188,a189), c5_2(
a188,X0), ~(c5_2(a188,a189)), c4_2(a188,X0), c4_1(a188), c1_1(a188), ~(
ndr1_1(a188)), ~(ndr1_0)

Gamma_27: (right-split)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]
  24: top(X0) != a197 | c2_2(a192,a193), [c1_2(a192,X0)], c1_2(a192,a217), c1_2(
a192,a193), c5_2(a192,X0), ~(c5_2(a192,a193)), c4_2(a192,X0), c4_1(a192), c1_1(
a192), ~(ndr1_1(a192)), ~(ndr1_0)
  25: top(X0) != a197 | c2_2(a188,a189), [c1_2(a188,X0)], c1_2(a188,a217), c1_2(
a188,a189), c5_2(a188,X0), ~(c5_2(a188,a189)), c4_2(a188,X0), c4_1(a188), c1_1(
a188), ~(ndr1_1(a188)), ~(ndr1_0)
  0: [c4_2(X0,a197)], ssSkP0(X0)
  1: [c1_2(X0,a197)], ssSkP0(X0)
  2: [c5_2(a188,a189)], ssSkC0
  3: [c3_2(a188,a189)], ssSkC0
  4: [c4_2(a210,a211)], ssSkC5
  5: [ssSkP0(X0)], ndr1_1(X0)
  6: [c3_1(a188)], ssSkC0
  7: [ndr1_1(a188)], ssSkC0
  8: [c2_1(a191)], ssSkC1
  9: [c5_1(a191)], ssSkC1
  10: [c3_1(a200)], ssSkC3
  11: [c1_1(a210)], ssSkC5
  12: [ndr1_1(a210)], ssSkC5
  13: [c2_2(a210,X0)], c3_2(a210,X0), c4_2(a210,X0), ~(ndr1_1(a210)), ssSkC5
  14: [ssSkC0], ndr1_0
  15: [ssSkC1], ndr1_0
  16: [c5_2(a192,a193)], c1_0, ~(ssSkC1)
  17: [c5_2(a192,a194)], c1_0, ~(ssSkC1)
  18: [c3_2(a192,a194)], c1_0, ~(ssSkC1)
  19: [ndr1_1(a192)], c1_0, ~(ssSkC1)
  20: [c1_0], ~(ssSkC1), ndr1_0
  21: [ssSkC2], ndr1_0
  22: [c4_1(a196)], ~(ssSkC2)
  23: ~(ssSkC2), [ndr1_0]
  24: top(X0) != a197 | c2_2(a192,a193), [c1_2(a192,X0)], c1_2(a192,a217), c1_2(
a192,a193), c5_2(a192,X0), ~(c5_2(a192,a193)), c4_2(a192,X0), c4_1(a192), c1_1(
a192), ~(ndr1_1(a192)), ~(ndr1_0)
  25: top(X0) != a197 | c2_2(a188,a189), [c1_2(a188,X0)], c1_2(a188,a217), c1_2(
a188,a189), c5_2(a188,X0), ~(c5_2(a188,a189)), c4_2(a188,X0), c4_1(a188), c1_1(
a188), ~(ndr1_1(a188)), ~(ndr1_0)

SZS status Satisfiable