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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)

Gamma_1: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)

Gamma_2: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)

Gamma_3: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)

Gamma_4: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]

Gamma_5: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))

Gamma_6: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))

Gamma_7: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))
  7: ~(rq(X0,esk5_1(X0))), [cA(X0)], ~(cowlThing(esk5_1(X0)))

Gamma_8: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))
  7: ~(rq(X0,esk5_1(X0))), [cA(X0)], ~(cowlThing(esk5_1(X0)))
  8: [rr(X0,esk3_1(X0))], ~(cB(X0))

Gamma_9: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))
  7: ~(rq(X0,esk5_1(X0))), [cA(X0)], ~(cowlThing(esk5_1(X0)))
  8: [rr(X0,esk3_1(X0))], ~(cB(X0))
  9: [rs(X0,esk2_1(X0))], ~(cAorB(X0))

Gamma_10: (extend-no-conflict)
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))
  7: ~(rq(X0,esk5_1(X0))), [cA(X0)], ~(cowlThing(esk5_1(X0)))
  8: [rr(X0,esk3_1(X0))], ~(cB(X0))
  9: [rs(X0,esk2_1(X0))], ~(cAorB(X0))
  10: [rq(X0,esk1_1(X0))], ~(cA(X0))
  0: [rr(X0,esk7_1(X0))], cnotB(X0)
  1: [rs(X0,esk6_1(X0))], cnotAorB(X0)
  2: [rq(X0,esk5_1(X0))], cnotA(X0)
  3: [xsd_integer(X0)], xsd_string(X0)
  4: [cowlThing(X0)]
  5: ~(rr(X0,esk7_1(X0))), [cB(X0)], ~(cowlThing(esk7_1(X0)))
  6: ~(rs(X0,esk6_1(X0))), [cAorB(X0)], ~(cowlThing(esk6_1(X0)))
  7: ~(rq(X0,esk5_1(X0))), [cA(X0)], ~(cowlThing(esk5_1(X0)))
  8: [rr(X0,esk3_1(X0))], ~(cB(X0))
  9: [rs(X0,esk2_1(X0))], ~(cAorB(X0))
  10: [rq(X0,esk1_1(X0))], ~(cA(X0))

SZS status Satisfiable