%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) Gamma_1: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] Gamma_2: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] Gamma_3: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_4: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_5: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [ce( esk1_1(i2003_11_14_17_20_32704))], ~(cd(esk1_1(i2003_11_14_17_20_32704))), ~( cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_6: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [ce( esk1_1(i2003_11_14_17_20_32704))], ~(cd(esk1_1(i2003_11_14_17_20_32704))), ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_7: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 6: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [ce( esk1_1(i2003_11_14_17_20_32704))], ~(cd(esk1_1(i2003_11_14_17_20_32704))), ~( cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_8: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cd(esk1_1(i2003_11_14_17_20_32704))), ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_9: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 6: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [~( cd(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_10: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [~( cd(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [cd( esk1_1(i2003_11_14_17_20_32704))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_11: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [~( cd(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_12: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [~( cd(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_13: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: [rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 5: ~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704))), [~( cd(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) 6: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_14: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: [~(cUnsatisfiable(i2003_11_14_17_20_32704))] 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_15: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cUnsatisfiable(i2003_11_14_17_20_32704)] 3: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 4: [~(cUnsatisfiable(i2003_11_14_17_20_32704))] 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_16: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cUnsatisfiable(i2003_11_14_17_20_32704))] 3: [cUnsatisfiable(i2003_11_14_17_20_32704)] 4: [~(rr(i2003_11_14_17_20_32704,esk1_1(i2003_11_14_17_20_32704)))], ~( cUnsatisfiable(i2003_11_14_17_20_32704)) 5: [~(ce(esk1_1(i2003_11_14_17_20_32704)))], ~(cUnsatisfiable(i2003_11_14_17_20_32704)) Gamma_17: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cUnsatisfiable(i2003_11_14_17_20_32704))] 3: [] SZS status Unsatisfiable