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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [b_is_a_knight]

Gamma_1: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)

Gamma_2: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: ~(c_is_a_knight), [a_is_a_knight]

Gamma_3: (extend-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: ~(c_is_a_knight), [a_is_a_knight]
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_4: (move)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: ~(c_is_a_knight), [a_is_a_knight]

Gamma_5: (resolve)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: [~(c_is_a_knight)], ~(b_is_a_knight)

Gamma_6: (extend-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: [~(c_is_a_knight)], ~(b_is_a_knight)

Gamma_7: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_8: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_9: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_10: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: [e_is_a_knight], a_is_a_knight

Gamma_11: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: [e_is_a_knight], a_is_a_knight
  5: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]

Gamma_12: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: [e_is_a_knight], a_is_a_knight

Gamma_13: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, ~(d_is_a_knight), [a_is_a_knight]

Gamma_14: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, ~(d_is_a_knight), [a_is_a_knight]

Gamma_15: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: [c_is_a_knight], ~(d_is_a_knight), ~(b_is_a_knight)

Gamma_16: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)

Gamma_17: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [d_is_a_knight], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)
  5: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]

Gamma_18: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: c_is_a_knight, [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_19: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [c_is_a_knight], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_20: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_21: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_22: (move)
  0: [~(b_is_a_knight)]
  1: [b_is_a_knight]
  2: [~(c_is_a_knight)], ~(b_is_a_knight)
  3: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_23: (resolve)
  0: [~(b_is_a_knight)]
  1: []

SZS status Unsatisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [b_is_a_knight]

Gamma_1: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)

Gamma_2: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: ~(c_is_a_knight), [a_is_a_knight]

Gamma_3: (extend-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: ~(c_is_a_knight), [a_is_a_knight]
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_4: (move)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: ~(c_is_a_knight), [a_is_a_knight]

Gamma_5: (resolve)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: [~(c_is_a_knight)], ~(b_is_a_knight)

Gamma_6: (extend-conflict)
  0: [b_is_a_knight]
  1: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  2: [~(a_is_a_knight)], ~(b_is_a_knight)
  3: [~(c_is_a_knight)], ~(b_is_a_knight)

Gamma_7: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [c_is_a_knight], d_is_a_knight, ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_8: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_9: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_10: (extend-no-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: [e_is_a_knight], a_is_a_knight

Gamma_11: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: [e_is_a_knight], a_is_a_knight
  5: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]

Gamma_12: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: [e_is_a_knight], a_is_a_knight

Gamma_13: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, ~(d_is_a_knight), [a_is_a_knight]

Gamma_14: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, ~(d_is_a_knight), [a_is_a_knight]

Gamma_15: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: [c_is_a_knight], ~(d_is_a_knight), ~(b_is_a_knight)

Gamma_16: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: [d_is_a_knight], ~(b_is_a_knight)
  3: [~(a_is_a_knight)], ~(b_is_a_knight)
  4: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]
  5: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)

Gamma_17: (move)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [d_is_a_knight], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)
  5: c_is_a_knight, ~(d_is_a_knight), [~(e_is_a_knight)]

Gamma_18: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: c_is_a_knight, [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_19: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [c_is_a_knight], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_20: (resolve)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_21: (extend-conflict)
  0: [b_is_a_knight]
  1: [~(c_is_a_knight)], ~(b_is_a_knight)
  2: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  3: [~(b_is_a_knight)]
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_22: (move)
  0: [~(b_is_a_knight)]
  1: [b_is_a_knight]
  2: [~(c_is_a_knight)], ~(b_is_a_knight)
  3: c_is_a_knight, [~(d_is_a_knight)], ~(b_is_a_knight)
  4: [~(a_is_a_knight)], ~(b_is_a_knight)

Gamma_23: (resolve)
  0: [~(b_is_a_knight)]
  1: []

SZS status Unsatisfiable