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

------ Parsing...successful


------ Proving...
use I-
not ground preserving

Gamma_0: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0

Gamma_1: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0

Gamma_2: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0

Gamma_3: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0

Gamma_4: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0
  4: ~(c3_0), [ndr1_0]

Gamma_5: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0
  4: ~(c3_0), [ndr1_0]
  5: [c3_2(X0,a147)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)

Gamma_6: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0
  4: ~(c3_0), [ndr1_0]
  5: [c3_2(X0,a147)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)
  6: [ndr1_1(X0)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)

Gamma_7: (extend-no-conflict)
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0
  4: ~(c3_0), [ndr1_0]
  5: [c3_2(X0,a147)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)
  6: [ndr1_1(X0)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)
  7: [c4_1(X0)], c5_1(X0), c3_1(a152), ~(ndr1_0), c2_0
  0: [c1_1(a154)], c3_0, ndr1_0
  1: [c3_1(a145)], c2_0
  2: [c5_0], c1_0, c2_0
  3: [c3_0], ndr1_0
  4: ~(c3_0), [ndr1_0]
  5: [c3_2(X0,a147)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)
  6: [ndr1_1(X0)], c4_1(a146), c5_1(X0), c4_0, ~(ndr1_0)
  7: [c4_1(X0)], c5_1(X0), c3_1(a152), ~(ndr1_0), c2_0

SZS status Satisfiable