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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0

Gamma_1: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0

Gamma_2: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0

Gamma_3: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]

Gamma_4: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0

Gamma_5: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)

Gamma_6: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)

Gamma_7: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)

Gamma_8: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)

Gamma_9: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)
  9: [c5_1(a10)], c1_1(a8), ~(epred1_0)

Gamma_10: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)
  9: [c5_1(a10)], c1_1(a8), ~(epred1_0)
  10: [c1_1(a8)], ndr1_1(a10), ~(epred1_0)

Gamma_11: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)
  9: [c5_1(a10)], c1_1(a8), ~(epred1_0)
  10: [c1_1(a8)], ndr1_1(a10), ~(epred1_0)
  11: [ndr1_1(a10)], ndr1_1(a8), ~(epred1_0)

Gamma_12: (extend-no-conflict)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)
  9: [c5_1(a10)], c1_1(a8), ~(epred1_0)
  10: [c1_1(a8)], ndr1_1(a10), ~(epred1_0)
  11: [ndr1_1(a10)], ndr1_1(a8), ~(epred1_0)
  12: [c1_1(a10)], ndr1_1(a8), ~(epred1_0)
  0: [c4_1(a12)], c4_0, ndr1_0
  1: [c3_1(a12)], c4_0, ndr1_0
  2: [c4_0], ndr1_0
  3: ~(c4_0), [epred1_0]
  4: [ndr1_0], epred2_0
  5: [c5_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  6: [c2_2(a10,a11)], c3_2(a8,a9), ~(epred1_0)
  7: [c3_2(a8,a9)], c5_1(a10), ~(epred1_0)
  8: [c1_2(a8,a9)], c5_1(a10), ~(epred1_0)
  9: [c5_1(a10)], c1_1(a8), ~(epred1_0)
  10: [c1_1(a8)], ndr1_1(a10), ~(epred1_0)
  11: [ndr1_1(a10)], ndr1_1(a8), ~(epred1_0)
  12: [c1_1(a10)], ndr1_1(a8), ~(epred1_0)

SZS status Satisfiable