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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))

Gamma_1: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))

Gamma_2: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  2: p(a), [~(r(a))]

Gamma_3: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  2: p(a), [~(r(a))]
  3: [q(esk1_0)]

Gamma_4: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_5: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [p(a)], ~(q(c)), ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_6: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_7: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]
  4: [q(c)]

Gamma_8: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  4: p(a), [~(r(a))]

Gamma_9: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [p(a)], ~(q(d)), ~(q(a))
  4: p(a), [~(r(a))]

Gamma_10: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(d))], ~(q(a))
  4: p(a), [~(r(a))]

Gamma_11: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(d))], ~(q(a))
  4: p(a), [~(r(a))]
  5: [q(d)]

Gamma_12: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(d))], ~(q(a))
  5: p(a), [~(r(a))]

Gamma_13: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [p(a)], ~(q(a))
  5: p(a), [~(r(a))]

Gamma_14: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(a))]
  5: p(a), [~(r(a))]

Gamma_15: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(a))]
  5: p(a), [~(r(a))]
  6: [q(a)]

Gamma_16: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: p(a), [~(q(a))]
  6: p(a), [~(r(a))]

Gamma_17: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: [p(a)]
  6: p(a), [~(r(a))]

Gamma_18: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: [p(a)]
  6: p(a), [~(r(a))]

Gamma_19: (move)
  0: [p(a)]
  1: [~(p(a))], ~(p(b))
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(a), [~(r(a))]

Gamma_20: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]

Gamma_21: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]

Gamma_22: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]

Gamma_23: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  7: p(b), [~(r(b))]

Gamma_24: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  7: p(b), [~(r(b))]
  8: [q(b)]

Gamma_25: (move)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  8: p(b), [~(r(b))]

Gamma_26: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0)), ~(q(c)), ~(q(d))
  8: p(b), [~(r(b))]

Gamma_27: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), ~(q(c)), [~(q(d))]
  8: p(b), [~(r(b))]

Gamma_28: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0)), ~(q(c))
  8: p(b), [~(r(b))]

Gamma_29: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), [~(q(c))]
  8: p(b), [~(r(b))]

Gamma_30: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0))
  8: p(b), [~(r(b))]

Gamma_31: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), [~(q(esk1_0))]
  8: p(b), [~(r(b))]

Gamma_32: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)]
  8: p(b), [~(r(b))]

Gamma_33: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)]
  8: p(b), [~(r(b))]

Gamma_34: (move)
  0: [p(a)]
  1: [p(b)]
  2: [~(p(b))]
  3: [q(esk1_0)]
  4: [q(c)]
  5: [q(d)]
  6: [q(a)]
  7: [q(b)]
  8: p(b), [~(r(b))]

Gamma_35: (resolve)
  0: [p(a)]
  1: [p(b)]
  2: []
  3: [q(esk1_0)]
  4: [q(c)]
  5: [q(d)]
  6: [q(a)]
  7: [q(b)]

SZS status Unsatisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))

Gamma_1: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))

Gamma_2: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  2: p(a), [~(r(a))]

Gamma_3: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  2: p(a), [~(r(a))]
  3: [q(esk1_0)]

Gamma_4: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(esk1_0))], ~(q(c)), ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_5: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [p(a)], ~(q(c)), ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_6: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]

Gamma_7: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  3: p(a), [~(r(a))]
  4: [q(c)]

Gamma_8: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(c))], ~(q(d)), ~(q(a))
  4: p(a), [~(r(a))]

Gamma_9: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [p(a)], ~(q(d)), ~(q(a))
  4: p(a), [~(r(a))]

Gamma_10: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(d))], ~(q(a))
  4: p(a), [~(r(a))]

Gamma_11: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: p(a), [~(q(d))], ~(q(a))
  4: p(a), [~(r(a))]
  5: [q(d)]

Gamma_12: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(d))], ~(q(a))
  5: p(a), [~(r(a))]

Gamma_13: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [p(a)], ~(q(a))
  5: p(a), [~(r(a))]

Gamma_14: (extend-no-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(a))]
  5: p(a), [~(r(a))]

Gamma_15: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: p(a), [~(q(a))]
  5: p(a), [~(r(a))]
  6: [q(a)]

Gamma_16: (move)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: p(a), [~(q(a))]
  6: p(a), [~(r(a))]

Gamma_17: (resolve)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: [p(a)]
  6: p(a), [~(r(a))]

Gamma_18: (extend-conflict)
  0: [~(p(a))], ~(p(b))
  1: [q(esk1_0)]
  2: [q(c)]
  3: [q(d)]
  4: [q(a)]
  5: [p(a)]
  6: p(a), [~(r(a))]

Gamma_19: (move)
  0: [p(a)]
  1: [~(p(a))], ~(p(b))
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(a), [~(r(a))]

Gamma_20: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]

Gamma_21: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]

Gamma_22: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]

Gamma_23: (extend-no-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  7: p(b), [~(r(b))]

Gamma_24: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  7: p(b), [~(r(b))]
  8: [q(b)]

Gamma_25: (move)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), ~(q(c)), ~(q(d)), [~(q(b))]
  8: p(b), [~(r(b))]

Gamma_26: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0)), ~(q(c)), ~(q(d))
  8: p(b), [~(r(b))]

Gamma_27: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), ~(q(c)), [~(q(d))]
  8: p(b), [~(r(b))]

Gamma_28: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0)), ~(q(c))
  8: p(b), [~(r(b))]

Gamma_29: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), ~(q(esk1_0)), [~(q(c))]
  8: p(b), [~(r(b))]

Gamma_30: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)], ~(q(esk1_0))
  8: p(b), [~(r(b))]

Gamma_31: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: p(b), [~(q(esk1_0))]
  8: p(b), [~(r(b))]

Gamma_32: (resolve)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)]
  8: p(b), [~(r(b))]

Gamma_33: (extend-conflict)
  0: [p(a)]
  1: [~(p(b))]
  2: [q(esk1_0)]
  3: [q(c)]
  4: [q(d)]
  5: [q(a)]
  6: [q(b)]
  7: [p(b)]
  8: p(b), [~(r(b))]

Gamma_34: (move)
  0: [p(a)]
  1: [p(b)]
  2: [~(p(b))]
  3: [q(esk1_0)]
  4: [q(c)]
  5: [q(d)]
  6: [q(a)]
  7: [q(b)]
  8: p(b), [~(r(b))]

Gamma_35: (resolve)
  0: [p(a)]
  1: [p(b)]
  2: []
  3: [q(esk1_0)]
  4: [q(c)]
  5: [q(d)]
  6: [q(a)]
  7: [q(b)]

SZS status Unsatisfiable