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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)

Gamma_1: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)

Gamma_2: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]

Gamma_3: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))

Gamma_4: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)

Gamma_5: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_6: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]
  6: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_7: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  6: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_8: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: [~(f(esk1_0))], ~(g(esk2_0)), g(esk1_0)

Gamma_9: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]

Gamma_10: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]
  6: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_11: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]

Gamma_12: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: h(esk1_0), [~(f(esk1_0))], ~(g(esk2_0))

Gamma_13: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [h(esk1_0)], ~(f(esk1_0)), ~(g(esk2_0))

Gamma_14: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [~(f(esk1_0))], ~(g(esk2_0))

Gamma_15: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [~(f(esk1_0))], ~(g(esk2_0))

Gamma_16: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [f(esk1_0)], ~(g(esk2_0))
  5: [~(h(esk1_0))], ~(g(esk2_0))
  6: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_17: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [~(g(esk2_0))]
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_18: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [~(g(esk2_0))]
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_19: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  4: [~(f(esk1_0))], ~(g(esk2_0))
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_20: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: [~(h(esk2_0))], ~(f(esk2_0))

Gamma_21: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: [~(h(esk2_0))], ~(f(esk2_0))

Gamma_22: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  3: [~(g(esk2_0))]

Gamma_23: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(f(esk2_0))], g(esk2_0)
  3: [~(g(esk2_0))]

Gamma_24: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: ~(f(esk2_0)), [g(esk2_0)]
  3: [~(g(esk2_0))]

Gamma_25: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: ~(f(esk2_0)), [g(esk2_0)]

Gamma_26: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: [~(f(esk2_0))]

Gamma_27: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: [~(f(esk2_0))]

Gamma_28: (move)
  0: [~(f(esk2_0))]
  1: [f(esk2_0)], f(esk1_0)
  2: [~(h(esk2_0))], ~(f(esk2_0))
  3: [~(g(esk2_0))]

Gamma_29: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]

Gamma_30: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]

Gamma_31: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)

Gamma_32: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  4: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_33: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  4: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]
  5: [~(h(esk1_0))], f(esk2_0)

Gamma_34: (move)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_35: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), [~(f(esk1_0))], g(esk1_0)

Gamma_36: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]

Gamma_37: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_38: (move)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]

Gamma_39: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: h(esk1_0), [f(esk2_0)], ~(f(esk1_0))

Gamma_40: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: [h(esk1_0)], f(esk2_0), ~(f(esk1_0))

Gamma_41: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: [f(esk2_0)], ~(f(esk1_0))

Gamma_42: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: f(esk2_0), [~(f(esk1_0))]

Gamma_43: (move)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk1_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_44: (resolve)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk2_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

Gamma_45: (extend-conflict)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk2_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

Gamma_46: (resolve)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: []
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

SZS status Unsatisfiable

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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)

Gamma_1: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)

Gamma_2: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]

Gamma_3: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))

Gamma_4: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)

Gamma_5: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_6: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]
  6: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_7: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  6: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_8: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: [~(f(esk1_0))], ~(g(esk2_0)), g(esk1_0)

Gamma_9: (extend-no-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]

Gamma_10: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]
  6: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_11: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: ~(f(esk1_0)), ~(g(esk2_0)), [g(esk1_0)]

Gamma_12: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: h(esk1_0), [~(f(esk1_0))], ~(g(esk2_0))

Gamma_13: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [h(esk1_0)], ~(f(esk1_0)), ~(g(esk2_0))

Gamma_14: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [~(f(esk1_0))], ~(g(esk2_0))

Gamma_15: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [f(esk1_0)], ~(g(esk2_0))
  4: [~(h(esk1_0))], ~(g(esk2_0))
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  6: [~(f(esk1_0))], ~(g(esk2_0))

Gamma_16: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [f(esk1_0)], ~(g(esk2_0))
  5: [~(h(esk1_0))], ~(g(esk2_0))
  6: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_17: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [~(g(esk2_0))]
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_18: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  3: [~(f(esk1_0))], ~(g(esk2_0))
  4: [~(g(esk2_0))]
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_19: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: ~(h(esk2_0)), ~(f(esk2_0)), [g(esk2_0)]
  4: [~(f(esk1_0))], ~(g(esk2_0))
  5: [~(h(esk1_0))], ~(g(esk2_0))

Gamma_20: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: [~(h(esk2_0))], ~(f(esk2_0))

Gamma_21: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  2: [~(g(esk2_0))]
  3: [~(h(esk2_0))], ~(f(esk2_0))

Gamma_22: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [h(esk2_0)], ~(f(esk2_0)), g(esk2_0)
  3: [~(g(esk2_0))]

Gamma_23: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(f(esk2_0))], g(esk2_0)
  3: [~(g(esk2_0))]

Gamma_24: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: ~(f(esk2_0)), [g(esk2_0)]
  3: [~(g(esk2_0))]

Gamma_25: (move)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: ~(f(esk2_0)), [g(esk2_0)]

Gamma_26: (resolve)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: [~(f(esk2_0))]

Gamma_27: (extend-conflict)
  0: [f(esk2_0)], f(esk1_0)
  1: [~(h(esk2_0))], ~(f(esk2_0))
  2: [~(g(esk2_0))]
  3: [~(f(esk2_0))]

Gamma_28: (move)
  0: [~(f(esk2_0))]
  1: [f(esk2_0)], f(esk1_0)
  2: [~(h(esk2_0))], ~(f(esk2_0))
  3: [~(g(esk2_0))]

Gamma_29: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]

Gamma_30: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]

Gamma_31: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)

Gamma_32: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  4: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_33: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  4: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]
  5: [~(h(esk1_0))], f(esk2_0)

Gamma_34: (move)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: [h(esk1_0)], ~(f(esk1_0)), g(esk1_0)
  5: ~(h(esk1_0)), ~(f(esk1_0)), [g(esk1_0)]

Gamma_35: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), [~(f(esk1_0))], g(esk1_0)

Gamma_36: (extend-no-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]

Gamma_37: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_38: (move)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: f(esk2_0), ~(f(esk1_0)), [g(esk1_0)]

Gamma_39: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: h(esk1_0), [f(esk2_0)], ~(f(esk1_0))

Gamma_40: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: [h(esk1_0)], f(esk2_0), ~(f(esk1_0))

Gamma_41: (resolve)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: [f(esk2_0)], ~(f(esk1_0))

Gamma_42: (extend-conflict)
  0: [~(f(esk2_0))]
  1: [f(esk1_0)]
  2: [~(g(esk2_0))]
  3: [~(h(esk1_0))], f(esk2_0)
  4: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]
  5: f(esk2_0), [~(f(esk1_0))]

Gamma_43: (move)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk1_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)
  5: h(esk1_0), ~(f(esk1_0)), [~(g(esk1_0))]

Gamma_44: (resolve)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk2_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

Gamma_45: (extend-conflict)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: [f(esk2_0)]
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

Gamma_46: (resolve)
  0: [~(f(esk2_0))]
  1: f(esk2_0), [~(f(esk1_0))]
  2: []
  3: [~(g(esk2_0))]
  4: [~(h(esk1_0))], f(esk2_0)

SZS status Unsatisfiable