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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0

Gamma_1: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0

Gamma_2: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0

Gamma_3: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0

Gamma_4: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0

Gamma_5: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0

Gamma_6: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0

Gamma_7: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0

Gamma_8: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0

Gamma_9: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0

Gamma_10: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0

Gamma_11: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0

Gamma_12: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0

Gamma_13: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0
  13: [c1_0], ndr1_0, c2_0

Gamma_14: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0
  13: [c1_0], ndr1_0, c2_0
  14: [c3_0], ndr1_0

Gamma_15: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0
  13: [c1_0], ndr1_0, c2_0
  14: [c3_0], ndr1_0
  15: [c4_0], c5_0

Gamma_16: (extend-no-conflict)
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0
  13: [c1_0], ndr1_0, c2_0
  14: [c3_0], ndr1_0
  15: [c4_0], c5_0
  16: [ndr1_0], c2_0
  0: [c4_2(a57,a58)], c2_1(a59), c3_0
  1: [c2_2(a57,a58)], c2_1(a59), c3_0
  2: [c3_2(a53,a54)], c1_0, c2_0
  3: [c2_2(a53,a54)], c1_0, c2_0
  4: [c5_2(a65,a66)], c2_0
  5: [c4_2(a65,a66)], c2_0
  6: [c2_1(a59)], ndr1_1(a57), c3_0
  7: [c5_1(a59)], ndr1_1(a57), c3_0
  8: [c5_1(a53)], c1_0, c2_0
  9: [ndr1_1(a53)], c1_0, c2_0
  10: [c1_1(a53)], c1_0, c2_0
  11: [ndr1_1(a57)], c3_0, ndr1_0
  12: [ndr1_1(a65)], c2_0
  13: [c1_0], ndr1_0, c2_0
  14: [c3_0], ndr1_0
  15: [c4_0], c5_0
  16: [ndr1_0], c2_0

SZS status Satisfiable