%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... flip all literals with predicate c1_1 use I+ Gamma_0: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) Gamma_1: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) Gamma_2: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) Gamma_3: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) Gamma_4: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) Gamma_5: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) Gamma_6: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) Gamma_7: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) Gamma_8: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) Gamma_9: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) Gamma_10: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) Gamma_11: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) Gamma_12: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) Gamma_13: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) Gamma_14: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) Gamma_15: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) Gamma_16: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) Gamma_17: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) Gamma_18: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) Gamma_19: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) Gamma_20: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) Gamma_21: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) Gamma_22: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) Gamma_23: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) Gamma_24: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) Gamma_25: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) Gamma_26: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) Gamma_27: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) Gamma_28: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) Gamma_29: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) Gamma_30: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) Gamma_31: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) Gamma_32: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) Gamma_33: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) Gamma_34: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) Gamma_35: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) Gamma_36: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) Gamma_37: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) Gamma_38: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) Gamma_39: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) Gamma_40: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) Gamma_41: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) 41: c2_1(a106), c1_1(a121), [~(c3_1(a106))], ~(c3_1(a121)), c0_1(a106), ~( c0_1(a121)), ~(ndr1_0) Gamma_42: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) 41: c2_1(a106), c1_1(a121), [~(c3_1(a106))], ~(c3_1(a121)), c0_1(a106), ~( c0_1(a121)), ~(ndr1_0) 42: c3_1(a128), [~(hskp14)] Gamma_43: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) 41: c2_1(a106), c1_1(a121), [~(c3_1(a106))], ~(c3_1(a121)), c0_1(a106), ~( c0_1(a121)), ~(ndr1_0) 42: c3_1(a128), [~(hskp14)] 43: c3_1(a106), [~(hskp15)] Gamma_44: (extend-no-conflict) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) 41: c2_1(a106), c1_1(a121), [~(c3_1(a106))], ~(c3_1(a121)), c0_1(a106), ~( c0_1(a121)), ~(ndr1_0) 42: c3_1(a128), [~(hskp14)] 43: c3_1(a106), [~(hskp15)] 44: [~(c1_1(a129))], ~(hskp22) 0: [~(c2_1(a105))], ~(hskp0) 1: [~(c0_1(a107))], ~(hskp1) 2: [~(c3_1(a107))], ~(hskp1) 3: [~(c2_1(a108))], ~(hskp2) 4: [~(c2_1(a109))], ~(hskp3) 5: [~(c2_1(a110))], ~(hskp4) 6: [~(c3_1(a110))], ~(hskp4) 7: [~(c2_1(a112))], ~(hskp6) 8: [~(c0_1(a112))], ~(hskp6) 9: [~(c0_1(a114))], ~(hskp7) 10: [~(c0_1(a118))], ~(hskp8) 11: [~(c2_1(a118))], ~(hskp8) 12: [~(c0_1(a120))], ~(hskp9) 13: [~(c2_1(a120))], ~(hskp9) 14: [~(c3_1(a122))], ~(hskp10) 15: [~(c0_1(a123))], ~(hskp11) 16: [~(c3_1(a126))], ~(hskp12) 17: [~(c3_1(a127))], ~(hskp13) 18: [~(c2_1(a127))], ~(hskp13) 19: [~(c0_1(a128))], ~(hskp14) 20: [~(c2_1(a128))], ~(hskp14) 21: [~(c2_1(a106))], ~(hskp15) 22: [~(c0_1(a106))], ~(hskp15) 23: [~(c3_1(a113))], ~(hskp16) 24: [~(c0_1(a115))], ~(hskp17) 25: [~(c3_1(a116))], ~(hskp18) 26: [~(c2_1(a117))], ~(hskp19) 27: [~(c0_1(a119))], ~(hskp20) 28: [~(c3_1(a129))], ~(hskp22) 29: [~(c0_1(a129))], ~(hskp22) 30: [~(c2_1(a130))], ~(hskp23) 31: [~(c1_1(a114))], ~(hskp7) 32: [~(c1_1(a126))], ~(hskp12) 33: [~(c1_1(a115))], ~(hskp17) 34: [~(c1_1(a116))], ~(hskp18) 35: [~(c1_1(a119))], ~(hskp20) 36: [~(c1_1(a121))], ~(hskp21) 37: c2_1(a112), c1_1(a121), [~(c3_1(a112))], ~(c3_1(a121)), c0_1(a112), ~( c0_1(a121)), ~(ndr1_0) 38: c2_1(a118), c1_1(a121), [~(c3_1(a118))], ~(c3_1(a121)), c0_1(a118), ~( c0_1(a121)), ~(ndr1_0) 39: c2_1(a120), c1_1(a121), [~(c3_1(a120))], ~(c3_1(a121)), c0_1(a120), ~( c0_1(a121)), ~(ndr1_0) 40: c2_1(a128), c1_1(a121), [~(c3_1(a128))], ~(c3_1(a121)), c0_1(a128), ~( c0_1(a121)), ~(ndr1_0) 41: c2_1(a106), c1_1(a121), [~(c3_1(a106))], ~(c3_1(a121)), c0_1(a106), ~( c0_1(a121)), ~(ndr1_0) 42: c3_1(a128), [~(hskp14)] 43: c3_1(a106), [~(hskp15)] 44: [~(c1_1(a129))], ~(hskp22) SZS status Satisfiable