%---------------- 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: [~(c3_1(a107))], ~(hskp1)

Gamma_2: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)

Gamma_3: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)

Gamma_4: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)

Gamma_5: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)

Gamma_6: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)

Gamma_7: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)

Gamma_8: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)

Gamma_9: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)

Gamma_10: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)

Gamma_11: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)

Gamma_12: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)

Gamma_13: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)

Gamma_14: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)

Gamma_15: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)

Gamma_16: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)

Gamma_18: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)

Gamma_19: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)

Gamma_20: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)

Gamma_21: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)

Gamma_22: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_1(a106))], ~(hskp15)

Gamma_23: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_1(a106))], ~(hskp15)
  23: [~(c3_1(a113))], ~(hskp16)

Gamma_24: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_1(a106))], ~(hskp15)
  23: [~(c3_1(a113))], ~(hskp16)
  24: [~(c0_1(a115))], ~(hskp17)

Gamma_25: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)

Gamma_29: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_1(a129))], ~(hskp22)

Gamma_30: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_1(a129))], ~(hskp22)
  30: [~(c2_1(a130))], ~(hskp23)

Gamma_31: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_1(a129))], ~(hskp22)
  30: [~(c2_1(a130))], ~(hskp23)
  31: [~(c1_1(a114))], ~(hskp7)

Gamma_32: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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), c0_1(a112), [~(c0_1(a121))], ~(c3_1(a112)), ~(
c3_1(a121)), ~(ndr1_0)

Gamma_38: (extend-no-conflict)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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), c0_1(a112), [~(c0_1(a121))], ~(c3_1(a112)), ~(
c3_1(a121)), ~(ndr1_0)
  38: [~(c1_1(a129))], ~(hskp22)
  0: [~(c2_1(a105))], ~(hskp0)
  1: [~(c3_1(a107))], ~(hskp1)
  2: [~(c0_1(a107))], ~(hskp1)
  3: [~(c2_1(a108))], ~(hskp2)
  4: [~(c2_1(a109))], ~(hskp3)
  5: [~(c3_1(a110))], ~(hskp4)
  6: [~(c2_1(a110))], ~(hskp4)
  7: [~(c0_1(a112))], ~(hskp6)
  8: [~(c2_1(a112))], ~(hskp6)
  9: [~(c0_1(a114))], ~(hskp7)
  10: [~(c2_1(a118))], ~(hskp8)
  11: [~(c0_1(a118))], ~(hskp8)
  12: [~(c2_1(a120))], ~(hskp9)
  13: [~(c0_1(a120))], ~(hskp9)
  14: [~(c3_1(a122))], ~(hskp10)
  15: [~(c0_1(a123))], ~(hskp11)
  16: [~(c3_1(a126))], ~(hskp12)
  17: [~(c2_1(a127))], ~(hskp13)
  18: [~(c3_1(a127))], ~(hskp13)
  19: [~(c2_1(a128))], ~(hskp14)
  20: [~(c0_1(a128))], ~(hskp14)
  21: [~(c0_1(a106))], ~(hskp15)
  22: [~(c2_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: [~(c0_1(a129))], ~(hskp22)
  29: [~(c3_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), c0_1(a112), [~(c0_1(a121))], ~(c3_1(a112)), ~(
c3_1(a121)), ~(ndr1_0)
  38: [~(c1_1(a129))], ~(hskp22)

SZS status Satisfiable