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

------ Parsing...successful


------ Proving...
flip all literals with predicate differ
use I+

Gamma_0: (extend-no-conflict)
  0: [~(differ(d,table))]

Gamma_1: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)

Gamma_2: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]

Gamma_3: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)

Gamma_4: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]

Gamma_5: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)

Gamma_6: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]

Gamma_7: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)

Gamma_8: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]

Gamma_9: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)

Gamma_10: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]

Gamma_11: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)

Gamma_12: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]

Gamma_13: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)

Gamma_14: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]

Gamma_15: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)

Gamma_16: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)
  16: [~(differ(a,c))]

Gamma_17: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)
  16: [~(differ(a,c))]
  17: [~(differ(c,a))], differ(a,c)

Gamma_18: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)
  16: [~(differ(a,c))]
  17: [~(differ(c,a))], differ(a,c)
  18: [~(differ(a,b))]

Gamma_19: (extend-no-conflict)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)
  16: [~(differ(a,c))]
  17: [~(differ(c,a))], differ(a,c)
  18: [~(differ(a,b))]
  19: [~(differ(b,a))], differ(a,b)
  0: [~(differ(d,table))]
  1: [~(differ(table,d))], differ(d,table)
  2: [~(differ(c,table))]
  3: [~(differ(table,c))], differ(c,table)
  4: [~(differ(c,d))]
  5: [~(differ(d,c))], differ(c,d)
  6: [~(differ(b,table))]
  7: [~(differ(table,b))], differ(b,table)
  8: [~(differ(b,d))]
  9: [~(differ(d,b))], differ(b,d)
  10: [~(differ(b,c))]
  11: [~(differ(c,b))], differ(b,c)
  12: [~(differ(a,table))]
  13: [~(differ(table,a))], differ(a,table)
  14: [~(differ(a,d))]
  15: [~(differ(d,a))], differ(a,d)
  16: [~(differ(a,c))]
  17: [~(differ(c,a))], differ(a,c)
  18: [~(differ(a,b))]
  19: [~(differ(b,a))], differ(a,b)

SZS status Satisfiable