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

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]

Gamma_1: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]

Gamma_2: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))

Gamma_3: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]

Gamma_4: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]

Gamma_5: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))

Gamma_6: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))

Gamma_7: (extend-no-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  7: [borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)], ~(mtvisible(c_tptpgeo_member1_mt))

Gamma_8: (extend-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  7: [borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)], ~(mtvisible(c_tptpgeo_member1_mt))
  8: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_9: (move)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  7: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]
  8: [borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)], ~(mtvisible(c_tptpgeo_member1_mt))

Gamma_10: (resolve)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  7: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]
  8: [~(mtvisible(c_tptpgeo_member1_mt))]

Gamma_11: (extend-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  5: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  7: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]
  8: [~(mtvisible(c_tptpgeo_member1_mt))]

Gamma_12: (move)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: [~(mtvisible(c_tptpgeo_member1_mt))]
  3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [mtvisible(
c_tptpgeo_member1_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt))
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  6: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  8: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_13: (resolve)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: [~(mtvisible(c_tptpgeo_member1_mt))]
  3: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  6: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  8: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_14: (extend-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  2: [~(mtvisible(c_tptpgeo_member1_mt))]
  3: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  6: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  8: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_15: (move)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  2: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)]
  3: [~(mtvisible(c_tptpgeo_member1_mt))]
  4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_spindlecollectormt)]
  5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt)), [microtheory(
c_tptpgeo_member1_mt)]
  6: [genlmt(c_tptpgeo_member1_mt,c_tptpgeo_member1_mt)], ~(microtheory(c_tptpgeo_member1_mt))
  7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~(
microtheory(c_tptpgeo_spindlecollectormt))
  8: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_16: (resolve)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  2: [~(mtvisible(c_tptpgeo_spindlecollectormt))]
  3: [~(mtvisible(c_tptpgeo_member1_mt))]
  4: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_17: (extend-conflict)
  0: [mtvisible(c_tptpgeo_spindlecollectormt)]
  1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  2: [~(mtvisible(c_tptpgeo_spindlecollectormt))]
  3: [~(mtvisible(c_tptpgeo_member1_mt))]
  4: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_18: (move)
  0: [~(mtvisible(c_tptpgeo_spindlecollectormt))]
  1: [mtvisible(c_tptpgeo_spindlecollectormt)]
  2: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt))], ~(
mtvisible(c_tptpgeo_spindlecollectormt))
  3: [~(mtvisible(c_tptpgeo_member1_mt))]
  4: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

Gamma_19: (resolve)
  0: [~(mtvisible(c_tptpgeo_spindlecollectormt))]
  1: []
  2: [~(mtvisible(c_tptpgeo_member1_mt))]
  3: [~(borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10))]

SZS status Unsatisfiable