%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) Gamma_1: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) Gamma_2: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) Gamma_3: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) Gamma_4: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 Gamma_5: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 Gamma_6: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 Gamma_7: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) Gamma_8: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) Gamma_9: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 Gamma_10: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 Gamma_11: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 Gamma_12: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 Gamma_13: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 Gamma_14: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 Gamma_15: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 Gamma_16: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 Gamma_17: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 Gamma_18: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 Gamma_19: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 Gamma_20: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 Gamma_21: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 Gamma_22: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] Gamma_23: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) Gamma_24: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) Gamma_25: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) Gamma_26: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) Gamma_27: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) Gamma_28: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) Gamma_29: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) Gamma_30: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) Gamma_31: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 31: [ndr1_1(X0)], ~(epred1_0), ~(ndr1_0) Gamma_32: (right-split) 0: [c5_2(a434,a435)], c1_1(a438), c4_1(a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 31: top(X0) != a434 | [ndr1_1(X0)], ~(epred1_0), ~(ndr1_0) Gamma_33: (extend-no-conflict) 0: [c5_2(a434,a435)], c1_1(a438), c4_1( a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 31: top(X0) != a434 | [ndr1_1(X0)], ~(epred1_0), ~(ndr1_0) 32: [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 Gamma_34: (right-split) 0: [c5_2(a434,a435)], c1_1(a438), c4_1(a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 31: top(X0) != a434 | [ndr1_1(X0)], ~(epred1_0), ~(ndr1_0) 32: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 0: [c5_2(a434,a435)], c1_1(a438), c4_1(a437) 1: [c4_2(a434,a435)], c1_1(a438), c4_1(a437) 2: [c3_2(a434,a435)], c1_1(a438), c4_1(a437) 3: [c3_2(a434,a436)], c1_1(a438), c4_1(a437) 4: [c4_2(a425,a426)], c3_1(a431), epred1_0 5: [c2_2(a425,a427)], c3_1(a431), epred1_0 6: [c1_2(a420,a421)], c4_0 7: [c1_1(a438)], ndr1_1(a434), c4_1(a437) 8: [c2_1(a438)], ndr1_1(a434), c4_1(a437) 9: [c3_1(a431)], ndr1_1(a425), epred1_0 10: [ndr1_1(a434)], c4_1(a437), ndr1_0 11: [c2_2(a434,a435)], ~(c4_2(a434,a435)), ~(c3_2(a434,a435)), ~(ndr1_1(a434)), c4_1( a437), ndr1_0 12: [ndr1_1(a425)], epred1_0, ndr1_0 13: [ndr1_1(a432)], c5_0, c1_0 14: [c4_1(a437)], ndr1_0 15: [c4_1(a440)], c5_0, c1_0 16: [ndr1_1(a420)], c4_0 17: [c4_1(a420)], c4_0 18: [c5_1(a420)], c4_0 19: [c5_1(a439)], c3_0 20: [epred1_0], ndr1_0 21: [c5_0], c1_0, ndr1_0 22: [ndr1_0] 23: [c2_2(a438,a417)], c4_2(a418,a419), c2_1(a416), ~(c2_1(a438)), ~( ndr1_0) 24: [c4_2(a418,a419)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 25: [c2_1(a418)], c2_1(a416), ~(c2_1(a438)), ndr1_1(a438), ~(ndr1_0) 26: [c2_2(a418,a417)], ~(c2_1(a418)), c2_1(a416), ndr1_1(a418), ~(ndr1_0) 27: ~(c2_1(a418)), [c2_1(a416)], ndr1_1(a418), ~(ndr1_0) 28: [c1_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 29: [c5_2(X0,a430)], c1_2(X0,a429), ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 30: [c1_2(X0,a429)], ndr1_1(X0), ~(epred1_0), ~(ndr1_0) 31: top(X0) != a434 | [ndr1_1(X0)], ~(epred1_0), ~(ndr1_0) 32: top(X0) != a430 | [c5_2(a439,X0)], c3_2(a439,X0), ~(ndr1_1(a439)), c3_0 SZS status Satisfiable