%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
flip all literals with predicate c3_1
use I+

Gamma_0: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)

Gamma_1: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)

Gamma_2: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)

Gamma_3: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)

Gamma_4: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)

Gamma_5: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)

Gamma_6: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)

Gamma_7: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)

Gamma_8: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)

Gamma_9: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)

Gamma_10: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)

Gamma_11: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)

Gamma_12: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)

Gamma_13: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)

Gamma_14: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)

Gamma_15: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)

Gamma_16: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)

Gamma_17: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)

Gamma_18: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)
  18: [~(c3_1(a7))], ~(hskp10)

Gamma_19: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)
  18: [~(c3_1(a7))], ~(hskp10)
  19: [~(c3_1(a9))], ~(hskp11)

Gamma_20: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)
  18: [~(c3_1(a7))], ~(hskp10)
  19: [~(c3_1(a9))], ~(hskp11)
  20: [~(c3_1(a10))], ~(hskp12)

Gamma_21: (extend-no-conflict)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)
  18: [~(c3_1(a7))], ~(hskp10)
  19: [~(c3_1(a9))], ~(hskp11)
  20: [~(c3_1(a10))], ~(hskp12)
  21: [~(c3_1(a15))], ~(hskp13)
  0: [~(c1_1(a2))], ~(hskp0)
  1: [~(c2_1(a4))], ~(hskp1)
  2: [~(c2_1(a5))], ~(hskp2)
  3: [~(c0_1(a8))], ~(hskp3)
  4: [~(c0_1(a11))], ~(hskp4)
  5: [~(c1_1(a12))], ~(hskp5)
  6: [~(c0_1(a12))], ~(hskp5)
  7: [~(c2_1(a12))], ~(hskp5)
  8: [~(c0_1(a14))], ~(hskp6)
  9: [~(c2_1(a14))], ~(hskp6)
  10: [~(c1_1(a3))], ~(hskp8)
  11: [~(c2_1(a7))], ~(hskp10)
  12: [~(c1_1(a7))], ~(hskp10)
  13: [~(c1_1(a10))], ~(hskp12)
  14: [~(c2_1(a10))], ~(hskp12)
  15: [~(c3_1(a8))], ~(hskp3)
  16: [~(c3_1(a1))], ~(hskp7)
  17: [~(c3_1(a6))], ~(hskp9)
  18: [~(c3_1(a7))], ~(hskp10)
  19: [~(c3_1(a9))], ~(hskp11)
  20: [~(c3_1(a10))], ~(hskp12)
  21: [~(c3_1(a15))], ~(hskp13)

SZS status Satisfiable