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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [p], r, n

Gamma_1: (extend-no-conflict)
  0: [p], r, n
  1: [n], q, m

Gamma_2: (extend-no-conflict)
  0: [p], r, n
  1: [n], q, m
  2: [t]

Gamma_3: (extend-conflict)
  0: [p], r, n
  1: [n], q, m
  2: [t]
  3: ~(n), [~(t)]

Gamma_4: (move)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [t]

Gamma_5: (resolve)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [~(n)]

Gamma_6: (extend-conflict)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [~(n)]

Gamma_7: (move)
  0: [p], r, n
  1: [~(n)]
  2: [n], q, m
  3: ~(n), [~(t)]

Gamma_8: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: [q], m

Gamma_9: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m

Gamma_10: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(q), [l]

Gamma_11: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(q), [l]
  4: ~(p), [~(l)]

Gamma_12: (move)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(q), [l]

Gamma_13: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(p), [~(q)]

Gamma_14: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(p), [~(q)]

Gamma_15: (move)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: [q], m
  4: ~(p), [~(l)]

Gamma_16: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]

Gamma_17: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]

Gamma_18: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(m), [l]

Gamma_19: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(p), [~(m)]

Gamma_20: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(p), [~(m)]

Gamma_21: (move)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: ~(p), [m]
  5: ~(p), [~(l)]

Gamma_22: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: [~(p)]
  5: ~(p), [~(l)]

Gamma_23: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: [~(p)]
  5: ~(p), [~(l)]

Gamma_24: (move)
  0: [~(p)]
  1: [p], r, n
  2: [~(n)]
  3: ~(p), [~(q)]
  4: ~(p), [~(m)]
  5: ~(p), [~(l)]

Gamma_25: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]

Gamma_26: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]

Gamma_27: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m

Gamma_28: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(q), [l]

Gamma_29: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(q), [l]
  5: ~(r), [~(l)]

Gamma_30: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(q), [l]

Gamma_31: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(r), [~(q)]

Gamma_32: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(r), [~(q)]

Gamma_33: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: n, [q], m
  5: ~(r), [~(l)]

Gamma_34: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [n], m
  5: ~(r), [~(l)]

Gamma_35: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]

Gamma_36: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(m), [l]

Gamma_37: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(r), [~(m)]

Gamma_38: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(r), [~(m)]

Gamma_39: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: ~(r), n, [m]
  6: ~(r), [~(l)]

Gamma_40: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)], n
  6: ~(r), [~(l)]

Gamma_41: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: ~(r), [n]
  6: ~(r), [~(l)]

Gamma_42: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)]
  6: ~(r), [~(l)]

Gamma_43: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)]
  6: ~(r), [~(l)]

Gamma_44: (move)
  0: [~(p)]
  1: [~(r)]
  2: [r], n
  3: [~(n)]
  4: ~(r), [~(q)]
  5: ~(r), [~(m)]
  6: ~(r), [~(l)]

Gamma_45: (resolve)
  0: [~(p)]
  1: [~(r)]
  2: [n]
  3: [~(n)]

Gamma_46: (extend-conflict)
  0: [~(p)]
  1: [~(r)]
  2: [n]
  3: [~(n)]

Gamma_47: (move)
  0: [~(p)]
  1: [~(r)]
  2: [~(n)]
  3: [n]

Gamma_48: (resolve)
  0: [~(p)]
  1: [~(r)]
  2: [~(n)]
  3: []

SZS status Unsatisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [p], r, n

Gamma_1: (extend-no-conflict)
  0: [p], r, n
  1: [n], q, m

Gamma_2: (extend-no-conflict)
  0: [p], r, n
  1: [n], q, m
  2: [t]

Gamma_3: (extend-conflict)
  0: [p], r, n
  1: [n], q, m
  2: [t]
  3: ~(n), [~(t)]

Gamma_4: (move)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [t]

Gamma_5: (resolve)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [~(n)]

Gamma_6: (extend-conflict)
  0: [p], r, n
  1: [n], q, m
  2: ~(n), [~(t)]
  3: [~(n)]

Gamma_7: (move)
  0: [p], r, n
  1: [~(n)]
  2: [n], q, m
  3: ~(n), [~(t)]

Gamma_8: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: [q], m

Gamma_9: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m

Gamma_10: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(q), [l]

Gamma_11: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(q), [l]
  4: ~(p), [~(l)]

Gamma_12: (move)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(q), [l]

Gamma_13: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(p), [~(q)]

Gamma_14: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: [q], m
  3: ~(p), [~(l)]
  4: ~(p), [~(q)]

Gamma_15: (move)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: [q], m
  4: ~(p), [~(l)]

Gamma_16: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]

Gamma_17: (extend-no-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]

Gamma_18: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(m), [l]

Gamma_19: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(p), [~(m)]

Gamma_20: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [m]
  4: ~(p), [~(l)]
  5: ~(p), [~(m)]

Gamma_21: (move)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: ~(p), [m]
  5: ~(p), [~(l)]

Gamma_22: (resolve)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: [~(p)]
  5: ~(p), [~(l)]

Gamma_23: (extend-conflict)
  0: [p], r, n
  1: [~(n)]
  2: ~(p), [~(q)]
  3: ~(p), [~(m)]
  4: [~(p)]
  5: ~(p), [~(l)]

Gamma_24: (move)
  0: [~(p)]
  1: [p], r, n
  2: [~(n)]
  3: ~(p), [~(q)]
  4: ~(p), [~(m)]
  5: ~(p), [~(l)]

Gamma_25: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]

Gamma_26: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]

Gamma_27: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m

Gamma_28: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(q), [l]

Gamma_29: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(q), [l]
  5: ~(r), [~(l)]

Gamma_30: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(q), [l]

Gamma_31: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(r), [~(q)]

Gamma_32: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: n, [q], m
  4: ~(r), [~(l)]
  5: ~(r), [~(q)]

Gamma_33: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: n, [q], m
  5: ~(r), [~(l)]

Gamma_34: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [n], m
  5: ~(r), [~(l)]

Gamma_35: (extend-no-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]

Gamma_36: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(m), [l]

Gamma_37: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(r), [~(m)]

Gamma_38: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), n, [m]
  5: ~(r), [~(l)]
  6: ~(r), [~(m)]

Gamma_39: (move)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: ~(r), n, [m]
  6: ~(r), [~(l)]

Gamma_40: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)], n
  6: ~(r), [~(l)]

Gamma_41: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: ~(r), [n]
  6: ~(r), [~(l)]

Gamma_42: (resolve)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)]
  6: ~(r), [~(l)]

Gamma_43: (extend-conflict)
  0: [~(p)]
  1: [r], n
  2: [~(n)]
  3: ~(r), [~(q)]
  4: ~(r), [~(m)]
  5: [~(r)]
  6: ~(r), [~(l)]

Gamma_44: (move)
  0: [~(p)]
  1: [~(r)]
  2: [r], n
  3: [~(n)]
  4: ~(r), [~(q)]
  5: ~(r), [~(m)]
  6: ~(r), [~(l)]

Gamma_45: (resolve)
  0: [~(p)]
  1: [~(r)]
  2: [n]
  3: [~(n)]

Gamma_46: (extend-conflict)
  0: [~(p)]
  1: [~(r)]
  2: [n]
  3: [~(n)]

Gamma_47: (move)
  0: [~(p)]
  1: [~(r)]
  2: [~(n)]
  3: [n]

Gamma_48: (resolve)
  0: [~(p)]
  1: [~(r)]
  2: [~(n)]
  3: []

SZS status Unsatisfiable