%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) Gamma_1: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) Gamma_2: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 Gamma_3: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 Gamma_4: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 Gamma_5: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 Gamma_6: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) Gamma_7: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 Gamma_8: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 Gamma_9: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 Gamma_10: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 Gamma_11: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 Gamma_12: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 Gamma_13: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 Gamma_14: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 Gamma_15: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~(ndr1_1(a698)), c5_0 Gamma_16: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 Gamma_17: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] Gamma_18: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) Gamma_19: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 Gamma_20: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 Gamma_21: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] Gamma_22: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) Gamma_23: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) Gamma_24: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) Gamma_25: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) 24: [c2_0], ~(c4_0) Gamma_26: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) 24: [c2_0], ~(c4_0) 25: [~(c2_0)], ~(c1_0) Gamma_27: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) 24: [~(c2_0)], ~(c1_0) 25: [c2_0], ~(c4_0) Gamma_28: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) 24: [~(c2_0)], ~(c1_0) 25: [~(c4_0)], ~(c1_0) Gamma_29: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [c4_0], ~(c5_0), ~(c1_0) 23: [c5_1(a697)], ~(c4_0) 24: [~(c2_0)], ~(c1_0) 25: [~(c4_0)], ~(c1_0) Gamma_30: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [~(c4_0)], ~(c1_0) 23: [c4_0], ~(c5_0), ~(c1_0) 24: [c5_1(a697)], ~(c4_0) 25: [~(c2_0)], ~(c1_0) Gamma_31: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [~(c4_0)], ~(c1_0) 23: [~(c5_0)], ~(c1_0) 24: [~(c2_0)], ~(c1_0) Gamma_32: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 21: [ndr1_1(a700)], c4_0, ~(c1_0) 22: [~(c4_0)], ~(c1_0) 23: ~(c5_0), [~(c1_0)] 24: [~(c2_0)], ~(c1_0) Gamma_33: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c5_0), [~(c1_0)] 21: ~(c2_2(a713,a714)), ~(c3_0), [c1_0] 22: [ndr1_1(a700)], c4_0, ~(c1_0) 23: [~(c4_0)], ~(c1_0) 24: [~(c2_0)], ~(c1_0) Gamma_34: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c5_0), [~(c1_0)] 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_35: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 20: ~(c5_0), [~(c1_0)] 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_36: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 21: ~(c5_0), [~(c1_0)] Gamma_37: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: [c2_2(a713,a714)], ~(ndr1_1(a713)), ~(c3_0), c1_0 21: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 22: ~(c5_0), [~(c1_0)] Gamma_38: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: [c2_2(a713,a714)], ~(ndr1_1(a713)), ~(c3_0), c1_0 21: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 22: ~(c5_0), [~(c1_0)] Gamma_39: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0), c1_0 21: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 22: ~(c5_0), [~(c1_0)] Gamma_40: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: ~(ndr1_1(a713)), ~(c3_0), ~(c5_0), [c1_0] 21: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 22: ~(c5_0), [~(c1_0)] Gamma_41: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: ~(c5_0), [~(c1_0)] 21: ~(ndr1_1(a713)), ~(c3_0), ~(c5_0), [c1_0] 22: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 Gamma_42: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: ~(c5_0), [~(c1_0)] 21: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 22: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 Gamma_43: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [ndr1_1(a713)], ~(c3_0), c1_0 19: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 20: ~(c5_0), [~(c1_0)] 21: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 22: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 Gamma_44: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: [ndr1_1(a713)], ~(c3_0), c1_0 20: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 21: ~(c5_0), [~(c1_0)] 22: top(X0) != a714 | [c2_2(a713,X0)], ~(ndr1_1(a713)), ~(c3_0), c1_0 Gamma_45: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: [~(c3_0)], ~(c5_0), c1_0 20: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 21: ~(c5_0), [~(c1_0)] Gamma_46: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: ~(c3_0), ~(c5_0), [c1_0] 20: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) 21: ~(c5_0), [~(c1_0)] Gamma_47: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: ~(c3_0), ~(c5_0), [c1_0] 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_48: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [~(c3_0)], ~(c5_0) 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_49: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [c3_0], c2_0, ~(c5_0) 18: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [~(c3_0)], ~(c5_0) 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_50: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c3_0], c2_0, ~(c5_0) 19: [~(ndr1_1(a713))], ~(c3_0), ~(c5_0) 20: ~(c5_0), [~(c1_0)] 21: [~(c2_2(a713,a714))], ~(c3_0), ~(c5_0) Gamma_51: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] Gamma_52: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] Gamma_53: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 Gamma_54: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 Gamma_55: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 Gamma_56: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 Gamma_57: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 Gamma_58: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 Gamma_59: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 Gamma_60: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) Gamma_61: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] Gamma_62: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) Gamma_63: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) Gamma_64: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) Gamma_65: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) Gamma_66: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) Gamma_67: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) Gamma_68: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) Gamma_69: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) Gamma_70: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) Gamma_71: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) Gamma_72: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) Gamma_73: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) Gamma_74: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) Gamma_75: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) Gamma_76: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] Gamma_77: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_78: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: top(X0) != a698 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_79: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: top(X0) != a698 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) Gamma_80: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: top(X0) != a698 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_81: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [c5_1(a693)], ndr1_1(a693), c3_0, ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_82: (right-split) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [c5_1(a693)], ndr1_1(a693), c3_0, ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_83: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_84: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) Gamma_85: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 46: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) Gamma_86: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 46: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 47: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_87: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 43: [~(c5_1(a693))], c3_0, ~(ssSkC2) 44: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 45: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 46: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 47: [ndr1_1(a685)], ~(ssSkC0), c3_0 48: ~(c2_0), [~(c4_0)], c1_0 Gamma_88: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c2_0), [~(c4_0)], c1_0 43: ~(c1_2(a689,a690)), ~(ssSkC1), [c4_0] 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_89: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c2_0), [~(c4_0)], c1_0 43: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_90: (extend-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 39: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 40: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 41: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 42: ~(c2_0), [~(c4_0)], c1_0 43: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_91: (move) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 39: ~(c2_2(a689,a690)), [c1_2(a689,a690)], c1_1(a689), ~(ndr1_1(a689)), c4_0, ~( ndr1_0) 40: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 41: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 42: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 43: ~(c2_0), [~(c4_0)], c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_92: (resolve) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 39: [~(c2_2(a689,a690))], c1_1(a689), ~(ndr1_1(a689)), ~(c2_0), ~(ssSkC1), c4_0, c1_0, ~( ndr1_0) 40: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 41: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 42: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 43: ~(c2_0), [~(c4_0)], c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 Gamma_93: (extend-no-conflict) 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 39: ~(c2_2(a689,a690)), [c1_1(a689)], ~(ndr1_1(a689)), ~(c2_0), ~(ssSkC1), c4_0, c1_0, ~( ndr1_0) 40: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 41: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 42: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 43: ~(c2_0), [~(c4_0)], c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 0: [c1_2(X0,a683)], ssSkP0(X0) 1: [c4_2(X0,a683)], ssSkP0(X0) 2: [c2_2(a687,a688)], ssSkC1 3: [c4_2(a687,a688)], ssSkC1 4: [c1_2(a717,a718)], ssSkC5 5: [c5_2(a717,a718)], ssSkC5 6: [ssSkP0(X0)], ndr1_1(X0) 7: [ndr1_1(a687)], ssSkC1 8: [ndr1_1(a706)], ssSkC3 9: [c1_1(a710)], ssSkC4 10: [c4_1(a717)], ssSkC5 11: [ndr1_1(a717)], ssSkC5 12: [c3_1(a722)], ssSkC6 13: [c3_1(a698)], c5_0 14: [ndr1_1(a698)], c5_0 15: top(X0) != a683 | [c4_2(a698,X0)], c1_2(a698,X0), c5_2(a698,X0), ~( ndr1_1(a698)), c5_0 16: ~(c4_2(a698,a699)), [c5_0] 17: [~(c3_0)], ~(c5_0) 18: [c2_0], ~(c5_0) 19: ~(c5_0), [~(c1_0)] 20: [ssSkC1], ndr1_0 21: [c3_2(a689,a690)], ~(ssSkC1), c4_0 22: [c2_2(a689,a690)], ~(ssSkC1), c4_0 23: [c1_2(a689,a691)], ~(ssSkC1), c4_0 24: [c5_2(a689,a691)], ~(ssSkC1), c4_0 25: [ndr1_1(a689)], ~(ssSkC1), c4_0 26: [ssSkC2], ndr1_0 27: [c2_1(a693)], c3_0, ~(ssSkC2) 28: c3_0, ~(ssSkC2), [ndr1_0] 29: [c3_2(a687,a688)], ~(c2_2(a687,a688)), ~(c4_2(a687,a688)), c1_2( a687,a682), c5_2(a687,a688), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 30: [c2_2(a698,X0)], ~(c4_2(a698,X0)), c1_2(a698,X0), c5_2(a698,a681), c2_1( a698), ~(ndr1_1(a698)), c4_0, c1_0, ~(ndr1_0) 31: [c3_2(a698,X0)], ~(c2_2(a698,X1)), ~(c2_2(a698,X0)), ~(c4_2(a698,X0)), ~( c4_2(a698,a682)), c5_2(a698,X1), c5_1(a717), ~(c4_1(a717)), ~(ndr1_1(a698)), c4_0, ~( ndr1_0) 32: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c1_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 33: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c4_2(a704,a705)], c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 34: [c3_2(a704,a705)], ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), c3_1( a689), ~(ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 35: ~(c3_2(a689,a690)), ~(c2_2(a689,a690)), [c3_1(a689)], ndr1_1(a704), ~( ndr1_1(a689)), ~(c2_0), ~(ndr1_0) 36: ~(c3_2(a687,a688)), ~(c2_2(a687,a688)), [c3_1(a687)], ndr1_1(a704), ~( ndr1_1(a687)), ~(c2_0), ~(ndr1_0) 37: top(X0) != a683 | ~(c2_2(a698,X0)), [c1_2(a698,X0)], c1_1(a698), ~( ndr1_1(a698)), c4_0, ~(ndr1_0) 38: [~(c1_2(a689,a690))], ~(c2_0), ~(ssSkC1), c1_0 39: ~(c2_2(a689,a690)), [c1_1(a689)], ~(ndr1_1(a689)), ~(c2_0), ~(ssSkC1), c4_0, c1_0, ~( ndr1_0) 40: ~(c2_2(a687,a688)), [c1_2(a687,a688)], c1_1(a687), ~(ndr1_1(a687)), c4_0, ~( ndr1_0) 41: ~(c2_2(a698,a684)), ~(ssSkP0(a698)), [ssSkC0], ~(ndr1_0) 42: ~(c3_2(a698,a703)), [c5_1(a698)], c3_0, ~(c5_0), ~(ndr1_0) 43: ~(c2_0), [~(c4_0)], c1_0 44: [~(c5_1(a693))], c3_0, ~(ssSkC2) 45: [ndr1_1(a693)], c3_0, ~(ssSkC2), ~(c5_0), ~(ndr1_0) 46: top(X0) != a693 | [c5_1(X0)], ndr1_1(X0), c3_0, ~(c5_0), ~(ndr1_0) 47: [c2_2(a693,a683)], ~(c1_2(a693,a683)), ~(ndr1_1(a693)), c3_0, ~( ssSkC2) 48: [ndr1_1(a685)], ~(ssSkC0), c3_0 SZS status Satisfiable