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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)

Gamma_1: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]

Gamma_2: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))

Gamma_3: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)

Gamma_4: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]

Gamma_5: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))

Gamma_6: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)

Gamma_7: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]

Gamma_8: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))

Gamma_9: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  9: ~(cd(X0)), [ca_Cx4xcomp(X0)], ~(cexcomp(X0))

Gamma_10: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  9: ~(cd(X0)), [ca_Cx4xcomp(X0)], ~(cexcomp(X0))
  10: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_11: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: ~(cd(X0)), [ca_Cx4xcomp(X0)], ~(cexcomp(X0))

Gamma_12: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))

Gamma_13: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  8: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))

Gamma_14: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  8: ~(ra_Px2(X0,esk5_1(X0))), [cd(X0)]
  9: [ra_Px2(X0,esk4_1(X0))], ~(cd(X0))
  10: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_15: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_16: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  7: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_17: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: [ra_Px2(X0,esk5_1(X0))], cdxcomp(X0)
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_18: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_19: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]

Gamma_20: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)

Gamma_21: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]

Gamma_22: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]

Gamma_23: (extend-no-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  13: [rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584))], ~(
cUnsatisfiable(i2003_11_14_17_22_31584))

Gamma_24: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  13: [rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584))], ~(
cUnsatisfiable(i2003_11_14_17_22_31584))
  14: [~(rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584)))], cd(
esk1_1(i2003_11_14_17_22_31584)), ~(cUnsatisfiable(i2003_11_14_17_22_31584))

Gamma_25: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  13: [~(rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584)))], cd(
esk1_1(i2003_11_14_17_22_31584)), ~(cUnsatisfiable(i2003_11_14_17_22_31584))
  14: [rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584))], ~(
cUnsatisfiable(i2003_11_14_17_22_31584))

Gamma_26: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  13: [~(rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584)))], cd(
esk1_1(i2003_11_14_17_22_31584)), ~(cUnsatisfiable(i2003_11_14_17_22_31584))
  14: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_27: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  13: [~(rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584)))], cd(
esk1_1(i2003_11_14_17_22_31584)), ~(cUnsatisfiable(i2003_11_14_17_22_31584))
  14: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_28: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]
  13: [cUnsatisfiable(i2003_11_14_17_22_31584)]
  14: [~(rr(i2003_11_14_17_22_31584,esk1_1(i2003_11_14_17_22_31584)))], cd(
esk1_1(i2003_11_14_17_22_31584)), ~(cUnsatisfiable(i2003_11_14_17_22_31584))

Gamma_29: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]
  13: [cd(esk1_1(i2003_11_14_17_22_31584))]

Gamma_30: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]
  13: [cd(esk1_1(i2003_11_14_17_22_31584))]

Gamma_31: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]
  13: [~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584))))], ~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))

Gamma_32: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  5: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  6: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  10: [xsd_integer(X0)], xsd_string(X0)
  11: [cowlThing(X0)]
  12: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]
  13: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]

Gamma_33: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  5: ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  6: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  7: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  8: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  10: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  11: [xsd_integer(X0)], xsd_string(X0)
  12: [cowlThing(X0)]
  13: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_34: (right-split)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  5: ~(ra_Px1(esk1_1(i2003_11_14_17_22_31584),esk6_1(esk1_1(i2003_11_14_17_22_31584)))), [cexcomp(
esk1_1(i2003_11_14_17_22_31584))]
  6: top(X1) != i2003_11_14_17_22_31584 | ~(ra_Px1(esk1_1(X0),esk6_1(esk1_1(X0)))), [cexcomp(
esk1_1(X0))]
  7: top(X0) != esk1_1 | ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  8: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  10: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  11: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  12: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  13: [xsd_integer(X0)], xsd_string(X0)
  14: [cowlThing(X0)]
  15: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_35: (right-split)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  5: ~(ra_Px1(esk1_1(i2003_11_14_17_22_31584),esk6_1(esk1_1(i2003_11_14_17_22_31584)))), [cexcomp(
esk1_1(i2003_11_14_17_22_31584))]
  6: top(X1) != i2003_11_14_17_22_31584 | ~(ra_Px1(esk1_1(X0),esk6_1(esk1_1(X0)))), [cexcomp(
esk1_1(X0))]
  7: top(X0) != esk1_1 | ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  8: [ra_Px1(X0,esk7_1(X0))], ~(cexcomp(X0))
  9: ~(ra_Px4(X0,esk8_1(X0))), [~(ra_Px2(X0,esk5_1(X0)))], ~(cexcomp(X0))
  10: ~(ra_Px4(X0,esk8_1(X0))), ~(cexcomp(X0)), [cdxcomp(X0)]
  11: ~(ra_Px4(X0,esk8_1(X0))), [~(cd(X0))], ~(cexcomp(X0))
  12: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  13: [xsd_integer(X0)], xsd_string(X0)
  14: [cowlThing(X0)]
  15: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_36: (resolve)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  5: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
ra_Px1(esk1_1(i2003_11_14_17_22_31584),esk6_1(esk1_1(i2003_11_14_17_22_31584))))]
  6: top(X1) != i2003_11_14_17_22_31584 | ~(ra_Px1(esk1_1(X0),esk6_1(esk1_1(X0)))), [cexcomp(
esk1_1(X0))]
  7: top(X0) != esk1_1 | ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  9: [xsd_integer(X0)], xsd_string(X0)
  10: [cowlThing(X0)]
  11: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_37: (extend-conflict)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(
X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  4: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  5: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
ra_Px1(esk1_1(i2003_11_14_17_22_31584),esk6_1(esk1_1(i2003_11_14_17_22_31584))))]
  6: top(X1) != i2003_11_14_17_22_31584 | ~(ra_Px1(esk1_1(X0),esk6_1(esk1_1(X0)))), [cexcomp(
esk1_1(X0))]
  7: top(X0) != esk1_1 | ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  9: [xsd_integer(X0)], xsd_string(X0)
  10: [cowlThing(X0)]
  11: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]

Gamma_38: (move)
  0: [ra_Px4(X0,esk9_1(X0))], ca_Cx4xcomp(X0)
  1: ~(ra_Px4(X0,esk9_1(X0))), [ca_Cx4(X0)]
  2: [ra_Px4(X0,esk8_1(X0))], ~(ca_Cx4(X0))
  3: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
ra_Px1(esk1_1(i2003_11_14_17_22_31584),esk6_1(esk1_1(i2003_11_14_17_22_31584))))]
  4: [ra_Px1(X0,esk6_1(X0))], ce(X0)
  5: ~(ra_Px4(esk1_1(i2003_11_14_17_22_31584),esk8_1(esk1_1(i2003_11_14_17_22_31584)))), [~(
cexcomp(esk1_1(i2003_11_14_17_22_31584)))]
  6: top(X1) != i2003_11_14_17_22_31584 | ~(ra_Px1(esk1_1(X0),esk6_1(esk1_1(X0)))), [cexcomp(
esk1_1(X0))]
  7: top(X0) != esk1_1 | ~(ra_Px1(X0,esk6_1(X0))), [cexcomp(X0)]
  8: ~(ra_Px4(X0,esk8_1(X0))), [~(ca_Cx4xcomp(X0))]
  9: [xsd_integer(X0)], xsd_string(X0)
  10: [cowlThing(X0)]
  11: cd(esk1_1(i2003_11_14_17_22_31584)), [~(cUnsatisfiable(i2003_11_14_17_22_31584))]