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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [~(f(exists))]

Gamma_1: (extend-no-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)

Gamma_2: (extend-no-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)

Gamma_3: (extend-no-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))

Gamma_4: (extend-no-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  4: r(exists,u1r1(exists)), d(u1r1(exists)), [~(c(exists))]

Gamma_5: (extend-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  4: r(exists,u1r1(exists)), d(u1r1(exists)), [~(c(exists))]
  5: [c(exists)]

Gamma_6: (move)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  4: [c(exists)]
  5: r(exists,u1r1(exists)), d(u1r1(exists)), [~(c(exists))]

Gamma_7: (resolve)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  4: [c(exists)]
  5: [r(exists,u1r1(exists))], d(u1r1(exists))

Gamma_8: (extend-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  4: [c(exists)]
  5: r(exists,u1r1(exists)), [d(u1r1(exists))]

Gamma_9: (move)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: r(exists,u1r1(exists)), [~(d(u1r1(exists)))], e(u1r1(exists)), ~(
c(exists))
  5: [c(exists)]

Gamma_10: (resolve)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: [r(exists,u1r1(exists))], e(u1r1(exists)), ~(c(exists))
  5: [c(exists)]

Gamma_11: (extend-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: r(exists,u1r1(exists)), e(u1r1(exists)), [~(c(exists))]
  5: [c(exists)]

Gamma_12: (move)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: [c(exists)]
  5: r(exists,u1r1(exists)), e(u1r1(exists)), [~(c(exists))]

Gamma_13: (resolve)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: [c(exists)]
  5: [r(exists,u1r1(exists))], e(u1r1(exists))

Gamma_14: (extend-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: [~(e(u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [d(u1r1(exists))]
  4: [c(exists)]
  5: r(exists,u1r1(exists)), [e(u1r1(exists))]

Gamma_15: (move)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: r(exists,u1r1(exists)), [e(u1r1(exists))]
  3: [~(e(u1r1(exists)))], f(exists)
  4: r(exists,u1r1(exists)), [d(u1r1(exists))]
  5: [c(exists)]

Gamma_16: (resolve)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: r(exists,u1r1(exists)), [e(u1r1(exists))]
  3: r(exists,u1r1(exists)), [f(exists)]
  4: r(exists,u1r1(exists)), [d(u1r1(exists))]
  5: [c(exists)]

Gamma_17: (extend-conflict)
  0: [~(f(exists))]
  1: [~(r(exists,u1r1(exists)))], f(exists)
  2: r(exists,u1r1(exists)), [e(u1r1(exists))]
  3: [r(exists,u1r1(exists))], f(exists)
  4: r(exists,u1r1(exists)), [d(u1r1(exists))]
  5: [c(exists)]

Gamma_18: (move)
  0: [~(f(exists))]
  1: [r(exists,u1r1(exists))], f(exists)
  2: [~(r(exists,u1r1(exists)))], f(exists)
  3: r(exists,u1r1(exists)), [e(u1r1(exists))]
  4: r(exists,u1r1(exists)), [d(u1r1(exists))]
  5: [c(exists)]

Gamma_19: (resolve)
  0: [~(f(exists))]
  1: [r(exists,u1r1(exists))], f(exists)
  2: [f(exists)]
  3: [c(exists)]

Gamma_20: (extend-conflict)
  0: [~(f(exists))]
  1: [r(exists,u1r1(exists))], f(exists)
  2: [f(exists)]
  3: [c(exists)]

Gamma_21: (move)
  0: [f(exists)]
  1: [~(f(exists))]
  2: [r(exists,u1r1(exists))], f(exists)
  3: [c(exists)]

Gamma_22: (resolve)
  0: [f(exists)]
  1: []
  2: [c(exists)]

SZS status Unsatisfiable