%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) Gamma_1: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 Gamma_2: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 Gamma_3: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 Gamma_4: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 Gamma_5: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 Gamma_6: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 Gamma_7: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 Gamma_8: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) Gamma_9: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) Gamma_10: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 Gamma_11: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 Gamma_12: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 Gamma_13: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 Gamma_14: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 Gamma_15: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 Gamma_16: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 Gamma_17: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 Gamma_18: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 Gamma_19: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 Gamma_20: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 Gamma_21: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 Gamma_22: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 Gamma_23: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 Gamma_24: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 Gamma_25: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 Gamma_26: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 Gamma_27: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) Gamma_28: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) Gamma_29: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] Gamma_30: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_31: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_32: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) Gamma_33: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) Gamma_34: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) Gamma_35: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~(ndr1_0) Gamma_36: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) Gamma_37: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_38: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_39: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 38: [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_40: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 38: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_41: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 38: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 39: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) Gamma_42: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 38: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_43: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ndr1_1(a413)), ~(ssSkC0), ~( ndr1_0) 38: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_44: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 38: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_45: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 37: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 38: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_46: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(ssSkP0(a413)), ~(ssSkP1(a413)), [ndr1_1(a413)], ssSkC4, ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 40: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_47: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(ssSkP0(a413)), ~(ssSkP1(a413)), [ndr1_1(a413)], ssSkC4, ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a438)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 40: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_48: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(c1_2(a413,a414)), [~(ssSkP0(a413))], ~(ssSkP1(a413)), ~(c2_1(a438)), ssSkC4, ~( ssSkC0), ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_49: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a438)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_50: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a438)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 40: ~(c2_1(a438)), [ndr1_1(a413)], ~(ssSkC0), ~(ndr1_0) Gamma_51: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a438)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 40: ~(c1_2(a413,a414)), [~(c2_1(a438))], ~(ssSkC0), ~(ndr1_0) Gamma_52: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a438)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 37: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 38: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 39: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 40: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) Gamma_53: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: [c1_2(a413,a414)], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 36: ~(c1_2(a413,a414)), ~(c2_1(a438)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 37: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a438)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 38: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 39: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 40: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_54: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: [~(c2_1(a438))], ~(ssSkC0), ~(ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_55: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 33: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 34: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 35: ~(c2_1(a438)), ~(ssSkC0), [~(ndr1_0)] 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_56: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(c2_1(a438)), ~(ssSkC0), [~(ndr1_0)] 30: ~(ssSkC5), ~(ssSkC6), [ndr1_0] 31: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 33: [c2_2(a438,a417)], ~(c2_1(a438)), ssSkC2, ~(ndr1_0) 34: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 35: [~(c1_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a438)), ~(ssSkC0), ~(ndr1_0) 37: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_57: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(c2_1(a438)), ~(ssSkC0), [~(ndr1_0)] 30: ~(c2_1(a438)), ~(ssSkC0), [~(ssSkC5)], ~(ssSkC6) 31: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_58: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 28: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: ~(c2_1(a438)), ~(ssSkC0), [~(ndr1_0)] 30: [~(c2_1(a438))], ~(ssSkC0), ~(ssSkC5), ~(ssSkC6) 31: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_59: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [~(c2_1(a438))], ~(ssSkC0), ~(ssSkC5), ~(ssSkC6) 28: [c2_1(a438)], ~(ssSkC5), ~(ssSkC6) 29: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 30: ~(c2_1(a438)), ~(ssSkC0), [~(ndr1_0)] 31: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_60: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [~(c2_1(a438))], ~(ssSkC0), ~(ssSkC5), ~(ssSkC6) 28: ~(ssSkC0), [~(ssSkC5)], ~(ssSkC6) 29: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 30: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_61: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: [ssSkC6], ndr1_0 27: [~(c2_1(a438))], ~(ssSkC0), ~(ssSkC5), ~(ssSkC6) 28: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 29: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 30: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_62: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: [ssSkC6], ndr1_0 28: [~(c2_1(a438))], ~(ssSkC0), ~(ssSkC5), ~(ssSkC6) 29: [c1_1(a438)], ~(ssSkC5), ~(ssSkC6) 30: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_63: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_64: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_65: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_66: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_67: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) Gamma_68: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_69: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~(ndr1_0) Gamma_70: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) Gamma_71: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_72: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 35: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_73: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 35: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_74: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 35: [c5_2(a413,a414)], ~(c1_2(a413,a414)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) 36: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_75: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 35: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ndr1_1(a413)), ~(ssSkC0), ~( ndr1_0) 36: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_76: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 35: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 36: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_77: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 35: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 36: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_78: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(ssSkP0(a413)), ~(ssSkP1(a413)), [ndr1_1(a413)], ssSkC4, ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_79: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(ssSkP0(a413)), ~(ssSkP1(a413)), [ndr1_1(a413)], ssSkC4, ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 37: [c5_2(a413,a429)], ~(c1_2(a413,a429)), ~(c2_1(a416)), ~(ndr1_1(a413)), ~( ssSkC0), ~(ndr1_0) Gamma_80: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(c1_2(a413,a414)), [~(ssSkP0(a413))], ~(ssSkP1(a413)), ~(c2_1(a416)), ssSkC4, ~( ssSkC0), ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_81: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a416)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_82: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a416)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 37: ~(c2_1(a416)), [ndr1_1(a413)], ~(ssSkC0), ~(ndr1_0) Gamma_83: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a416)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 37: ~(c1_2(a413,a414)), [~(c2_1(a416))], ~(ssSkC0), ~(ndr1_0) Gamma_84: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 34: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a416)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 35: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 36: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 37: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_85: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: [c1_2(a413,a414)], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 34: ~(c1_2(a413,a414)), ~(c2_1(a416)), [~(ndr1_1(a413))], ~(ssSkC0), ~( ndr1_0) 35: ~(c1_2(a413,a414)), ~(ssSkP0(a413)), ~(ssSkP1(a413)), ~(c2_1(a416)), [ssSkC4], ~( ssSkC0), ~(ndr1_0) 36: top(X0) != a413 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 37: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_86: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: [~(c2_1(a416))], ~(ssSkC0), ~(ndr1_0) 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_87: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 29: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 30: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 32: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 33: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_88: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: ~(ssSkC0), ~(ssSkC5), [ndr1_0] 29: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 30: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 31: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 32: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 33: [~(c1_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) 34: [~(c5_2(a413,a414))], ~(c2_1(a416)), ~(ssSkC0), ~(ndr1_0) Gamma_89: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: ~(c2_1(a416)), [~(ssSkC0)], ~(ssSkC5) 29: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_90: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: [ssSkC5], ndr1_0 26: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 29: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_91: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: [ssSkC5], ndr1_0 27: ~(ssSkC0), ~(ssSkC5), [~(ssSkC6)] 28: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 29: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_92: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: ~(c2_1(a416)), ~(ssSkC0), [ndr1_0] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_93: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: ~(c2_1(a416)), ~(ssSkC0), [ndr1_0] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_94: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 27: ~(c2_1(a416)), ~(ssSkC0), [ndr1_0] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_95: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 27: [~(c2_1(a416))], ~(ssSkC0) 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_96: (extend-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: [ssSkC0], ndr1_0 23: [ssSkC1], ndr1_0 24: [ssSkC3], ndr1_0 25: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 26: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 27: ~(c2_1(a416)), [~(ssSkC0)] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_97: (move) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: [ssSkC0], ndr1_0 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: ~(c2_1(a416)), ~(ssSkC0), [~(ssSkC5)] 27: ~(c2_1(a416)), ~(ssSkC0), [~(ndr1_0)] 28: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_98: (resolve) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_99: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_100: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_101: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 28: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) Gamma_102: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 28: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 29: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) Gamma_103: (extend-no-conflict) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 28: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 29: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 30: ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~(ndr1_0) Gamma_104: (right-split) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 28: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 29: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 30: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) 0: [c1_2(X0,a429)], ssSkP1(X0) 1: [c4_2(a425,a426)], ssSkC3 2: [c2_2(a425,a427)], ssSkC3 3: [c3_2(a434,a435)], ssSkC5 4: [c4_2(a434,a435)], ssSkC5 5: [c5_2(a434,a435)], ssSkC5 6: [c3_2(a434,a436)], ssSkC5 7: [c1_2(a420,a421)], c4_0 8: [ssSkP0(X0)], ndr1_1(X0) 9: [ssSkP1(X0)], ndr1_1(X0) 10: [ndr1_1(a432)], c5_0, c1_0 11: [c4_1(a440)], c5_0, c1_0 12: [c2_1(a416)], ssSkC1 13: [ndr1_1(a425)], ssSkC3 14: [ndr1_1(a434)], ssSkC5 15: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), ssSkC5 16: [c4_1(a437)], ssSkC6 17: [c5_1(a420)], c4_0 18: [c4_1(a420)], c4_0 19: [ndr1_1(a420)], c4_0 20: [c5_1(a439)], c3_0 21: [c5_0], c1_0, ndr1_0 22: ~(c2_1(a416)), [~(ssSkC0)] 23: ~(c2_1(a416)), [ndr1_0] 24: [ssSkC1], ndr1_0 25: [ssSkC3], ndr1_0 26: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 27: [c5_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 28: [c1_2(X0,a430)], ~(ssSkP0(X0)), ~(ssSkP1(X0)), ssSkC4, ~(ndr1_0) 29: [c2_2(a416,a417)], ~(c2_1(a416)), ssSkC2, ~(ndr1_0) 30: top(X0) != a432 | ~(ssSkP0(X0)), ~(ssSkP1(X0)), [ndr1_1(X0)], ssSkC4, ~( ndr1_0) SZS status Satisfiable