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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [after(five,six)]

Gamma_1: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]

Gamma_2: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))

Gamma_3: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]

Gamma_4: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))

Gamma_5: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))

Gamma_6: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]

Gamma_7: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))

Gamma_8: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))

Gamma_9: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))

Gamma_10: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]

Gamma_11: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))

Gamma_12: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))

Gamma_13: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))

Gamma_14: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))

Gamma_15: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]

Gamma_16: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]

Gamma_17: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))

Gamma_18: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]

Gamma_19: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))

Gamma_20: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))

Gamma_21: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]

Gamma_22: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))

Gamma_23: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))

Gamma_24: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))

Gamma_25: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]

Gamma_26: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))

Gamma_27: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))

Gamma_28: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))

Gamma_29: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))

Gamma_30: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]

Gamma_31: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))

Gamma_32: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))
  32: [not_familiar(one,five)], familiar(one,five), ~(after(one,five)), ~(
person(five)), ~(person(one))

Gamma_33: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))
  32: [not_familiar(one,five)], familiar(one,five), ~(after(one,five)), ~(
person(five)), ~(person(one))
  33: [not_familiar(one,four)], familiar(one,four), ~(after(one,four)), ~(
person(four)), ~(person(one))

Gamma_34: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))
  32: [not_familiar(one,five)], familiar(one,five), ~(after(one,five)), ~(
person(five)), ~(person(one))
  33: [not_familiar(one,four)], familiar(one,four), ~(after(one,four)), ~(
person(four)), ~(person(one))
  34: [not_familiar(one,three)], familiar(one,three), ~(after(one,three)), ~(
person(three)), ~(person(one))

Gamma_35: (extend-no-conflict)
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))
  32: [not_familiar(one,five)], familiar(one,five), ~(after(one,five)), ~(
person(five)), ~(person(one))
  33: [not_familiar(one,four)], familiar(one,four), ~(after(one,four)), ~(
person(four)), ~(person(one))
  34: [not_familiar(one,three)], familiar(one,three), ~(after(one,three)), ~(
person(three)), ~(person(one))
  35: [not_familiar(one,two)], familiar(one,two), ~(after(one,two)), ~(
person(two)), ~(person(one))
  0: [after(five,six)]
  1: [after(four,five)]
  2: ~(after(five,six)), [after(four,six)], ~(after(four,five))
  3: [after(three,four)]
  4: ~(after(four,six)), [after(three,six)], ~(after(three,four))
  5: ~(after(four,five)), [after(three,five)], ~(after(three,four))
  6: [after(two,three)]
  7: ~(after(three,five)), [after(two,five)], ~(after(two,three))
  8: ~(after(five,six)), [after(two,six)], ~(after(two,five))
  9: ~(after(three,four)), [after(two,four)], ~(after(two,three))
  10: [after(one,two)]
  11: ~(after(two,four)), [after(one,four)], ~(after(one,two))
  12: ~(after(four,six)), [after(one,six)], ~(after(one,four))
  13: ~(after(four,five)), [after(one,five)], ~(after(one,four))
  14: ~(after(two,three)), [after(one,three)], ~(after(one,two))
  15: [person(six)]
  16: [person(five)]
  17: [not_familiar(five,six)], familiar(five,six), ~(after(five,six)), ~(
person(six)), ~(person(five))
  18: [person(four)]
  19: [not_familiar(four,six)], familiar(four,six), ~(after(four,six)), ~(
person(six)), ~(person(four))
  20: [not_familiar(four,five)], familiar(four,five), ~(after(four,five)), ~(
person(five)), ~(person(four))
  21: [person(three)]
  22: [not_familiar(three,six)], familiar(three,six), ~(after(three,six)), ~(
person(six)), ~(person(three))
  23: [not_familiar(three,five)], familiar(three,five), ~(after(three,five)), ~(
person(five)), ~(person(three))
  24: [not_familiar(three,four)], familiar(three,four), ~(after(three,four)), ~(
person(four)), ~(person(three))
  25: [person(two)]
  26: [not_familiar(two,six)], familiar(two,six), ~(after(two,six)), ~(
person(six)), ~(person(two))
  27: [not_familiar(two,five)], familiar(two,five), ~(after(two,five)), ~(
person(five)), ~(person(two))
  28: [not_familiar(two,four)], familiar(two,four), ~(after(two,four)), ~(
person(four)), ~(person(two))
  29: [not_familiar(two,three)], familiar(two,three), ~(after(two,three)), ~(
person(three)), ~(person(two))
  30: [person(one)]
  31: [not_familiar(one,six)], familiar(one,six), ~(after(one,six)), ~(
person(six)), ~(person(one))
  32: [not_familiar(one,five)], familiar(one,five), ~(after(one,five)), ~(
person(five)), ~(person(one))
  33: [not_familiar(one,four)], familiar(one,four), ~(after(one,four)), ~(
person(four)), ~(person(one))
  34: [not_familiar(one,three)], familiar(one,three), ~(after(one,three)), ~(
person(three)), ~(person(one))
  35: [not_familiar(one,two)], familiar(one,two), ~(after(one,two)), ~(
person(two)), ~(person(one))

SZS status Satisfiable