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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0

Gamma_1: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0

Gamma_2: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0

Gamma_3: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0

Gamma_4: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0
  4: [ndr1_1(a248)], c3_0

Gamma_5: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0
  4: [ndr1_1(a248)], c3_0
  5: [c3_1(a248)], c3_0

Gamma_6: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0
  4: [ndr1_1(a248)], c3_0
  5: [c3_1(a248)], c3_0
  6: [c4_0], c5_0, ndr1_0

Gamma_7: (extend-no-conflict)
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0
  4: [ndr1_1(a248)], c3_0
  5: [c3_1(a248)], c3_0
  6: [c4_0], c5_0, ndr1_0
  7: [ndr1_0], c3_0
  0: [c1_2(a221,a222)], c4_0, c5_0
  1: [c4_2(a248,a249)], c3_0
  2: [c2_2(a248,a249)], c3_0
  3: [ndr1_1(a221)], c4_0, c5_0
  4: [ndr1_1(a248)], c3_0
  5: [c3_1(a248)], c3_0
  6: [c4_0], c5_0, ndr1_0
  7: [ndr1_0], c3_0

SZS status Satisfiable