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

------ Parsing...successful


------ Proving...
use I-
not ground preserving

Gamma_0: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]

Gamma_1: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]

Gamma_2: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]

Gamma_3: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]

Gamma_4: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]

Gamma_5: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]

Gamma_6: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]

Gamma_7: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]

Gamma_8: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]

Gamma_9: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]

Gamma_10: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]

Gamma_11: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]

Gamma_12: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]

Gamma_13: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p12(esk7_0)]

Gamma_14: (extend-no-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p12(esk7_0)]
  14: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]

Gamma_15: (extend-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p12(esk7_0)]
  14: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]
  15: [~(p12(esk7_0))]

Gamma_16: (move)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: [~(p12(esk7_0))]
  14: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p12(esk7_0)]
  15: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]

Gamma_17: (resolve)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: [~(p12(esk7_0))]
  14: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  15: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]

Gamma_18: (extend-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [r1(esk6_0,esk7_0)]
  12: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  13: [~(p12(esk7_0))]
  14: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  15: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]

Gamma_19: (move)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  12: [r1(esk6_0,esk7_0)]
  13: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p16(esk7_0)]
  14: [~(p12(esk7_0))]
  15: ~(r1(esk6_0,esk7_0)), ~(r1(esk1_0,esk6_0)), [p14(esk7_0)]

Gamma_20: (resolve)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  12: [~(r1(esk1_0,esk6_0))]
  13: [~(p12(esk7_0))]

Gamma_21: (extend-conflict)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [r1(esk1_0,esk6_0)]
  11: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  12: [~(r1(esk1_0,esk6_0))]
  13: [~(p12(esk7_0))]

Gamma_22: (move)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [~(r1(esk1_0,esk6_0))]
  11: [r1(esk1_0,esk6_0)]
  12: [~(r1(esk6_0,esk7_0))], ~(r1(esk1_0,esk6_0))
  13: [~(p12(esk7_0))]

Gamma_23: (resolve)
  0: [r1(esk1_0,esk2_0)]
  1: [r1(esk2_0,esk3_0)]
  2: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p16(esk3_0)]
  3: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p12(esk3_0)]
  4: ~(r1(esk2_0,esk3_0)), ~(r1(esk1_0,esk2_0)), [p14(esk3_0)]
  5: [r1(esk1_0,esk4_0)]
  6: [r1(esk4_0,esk5_0)]
  7: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p16(esk5_0)]
  8: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p12(esk5_0)]
  9: ~(r1(esk4_0,esk5_0)), ~(r1(esk1_0,esk4_0)), [p14(esk5_0)]
  10: [~(r1(esk1_0,esk6_0))]
  11: []
  12: [~(p12(esk7_0))]

SZS status Unsatisfiable