%---------------- 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: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_3: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_4: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_5: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_6: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), cowlNothing(esk2_0), ~( cowlThing(esk1_0)) Gamma_7: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [cowlNothing(esk2_0)], ~( cowlThing(esk1_0)) Gamma_8: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [cowlNothing(esk2_0)], ~( cowlThing(esk1_0)) 5: [~(cowlNothing(esk2_0))] Gamma_9: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: [~(cowlNothing(esk2_0))] 5: ~(cB(esk4_0)), ~(xsd_integer(esk3_0)), [cowlNothing(esk2_0)], ~( cowlThing(esk1_0)) Gamma_10: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: [~(cowlNothing(esk2_0))] 5: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) Gamma_11: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 3: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 4: [~(cowlNothing(esk2_0))] 5: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) Gamma_12: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cB(esk4_0)], cA(esk4_0), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] Gamma_13: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] Gamma_14: (extend-no-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] Gamma_15: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] 6: ~(cA(esk4_0)), ~(xsd_integer(esk3_0)), xsd_string(esk3_0), [cowlNothing( esk2_0)], ~(cowlThing(esk1_0)) Gamma_16: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] 6: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), ~(cowlThing(esk1_0)) Gamma_17: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] 6: ~(cA(esk4_0)), ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], ~(cowlThing(esk1_0)) Gamma_18: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] 6: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) Gamma_19: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 5: [~(cowlNothing(esk2_0))] 6: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) Gamma_20: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [cA(esk4_0)], ~(xsd_integer(esk3_0)), xsd_string(esk3_0), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: [~(cowlNothing(esk2_0))] Gamma_21: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(xsd_integer(esk3_0))], xsd_string(esk3_0), cowlNothing(esk2_0), ~( cowlThing(esk1_0)) 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: [~(cowlNothing(esk2_0))] Gamma_22: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: ~(xsd_integer(esk3_0)), xsd_string(esk3_0), [cowlNothing(esk2_0)], ~( cowlThing(esk1_0)) 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: [~(cowlNothing(esk2_0))] Gamma_23: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), xsd_string(esk3_0), [cowlNothing(esk2_0)], ~( cowlThing(esk1_0)) 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_24: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: [~(xsd_integer(esk3_0))], xsd_string(esk3_0), ~(cowlThing(esk1_0)) 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_25: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], ~(cowlThing(esk1_0)) 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_26: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: ~(xsd_integer(esk3_0)), [xsd_string(esk3_0)], ~(cowlThing(esk1_0)) Gamma_27: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: [~(xsd_integer(esk3_0))], ~(cowlThing(esk1_0)) Gamma_28: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: [cowlThing(X0)] 2: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 3: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] 6: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] Gamma_29: (move) 0: [xsd_integer(X0)], xsd_string(X0) 1: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 2: [cowlThing(X0)] 3: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 4: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 5: [~(cowlNothing(esk2_0))] 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_30: (right-split) 0: [xsd_integer(X0)], xsd_string(X0) 1: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 2: [cowlThing(esk1_0)] 3: top(X0) != esk1_0 | [cowlThing(X0)] 4: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 5: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 6: [~(cowlNothing(esk2_0))] 7: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_31: (right-split) 0: [xsd_integer(X0)], xsd_string(X0) 1: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 2: [cowlThing(esk1_0)] 3: top(X0) != esk1_0 | [cowlThing(X0)] 4: [~(cB(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 5: [~(cA(esk4_0))], ~(xsd_integer(esk3_0)), ~(cowlThing(esk1_0)) 6: [~(cowlNothing(esk2_0))] 7: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_32: (resolve) 0: [xsd_integer(X0)], xsd_string(X0) 1: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 2: [~(xsd_integer(esk3_0))] 3: top(X0) != esk1_0 | [cowlThing(X0)] 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_33: (extend-conflict) 0: [xsd_integer(X0)], xsd_string(X0) 1: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 2: [~(xsd_integer(esk3_0))] 3: top(X0) != esk1_0 | [cowlThing(X0)] 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_34: (move) 0: [~(xsd_integer(esk3_0))] 1: [xsd_integer(X0)], xsd_string(X0) 2: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 3: top(X0) != esk1_0 | [cowlThing(X0)] 4: [~(cowlNothing(esk2_0))] 5: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_35: (right-split) 0: [~(xsd_integer(esk3_0))] 1: [xsd_integer(esk3_0)], xsd_string(esk3_0) 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 4: top(X0) != esk1_0 | [cowlThing(X0)] 5: [~(cowlNothing(esk2_0))] 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_36: (right-split) 0: [~(xsd_integer(esk3_0))] 1: [xsd_integer(esk3_0)], xsd_string(esk3_0) 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: ~(xsd_integer(esk3_0)), [~(cowlThing(esk1_0))] 4: top(X0) != esk1_0 | [cowlThing(X0)] 5: [~(cowlNothing(esk2_0))] 6: ~(xsd_integer(esk3_0)), [~(xsd_string(esk3_0))] Gamma_37: (resolve) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] Gamma_38: (extend-no-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] Gamma_39: (extend-no-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] Gamma_40: (extend-no-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [cB(esk4_0)], cA(esk4_0), xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_41: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [cB(esk4_0)], cA(esk4_0), xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_42: (move) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [cB(esk4_0)], cA(esk4_0), xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_43: (resolve) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [cA(esk4_0)], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_44: (extend-no-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [cA(esk4_0)], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_45: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [cA(esk4_0)], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 7: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_46: (move) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 7: [cA(esk4_0)], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_47: (resolve) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 7: [xsd_integer(esk3_0)], ~(xsd_string(esk3_0)), cowlNothing(esk2_0), ~( cowlThing(esk1_0)) Gamma_48: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: [cowlThing(X0)] 5: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 6: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 7: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] Gamma_49: (move) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: [cowlThing(X0)] 6: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 7: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_50: (right-split) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: [cowlThing(esk1_0)] 6: top(X0) != esk1_0 | [cowlThing(X0)] 7: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 8: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_51: (right-split) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: [cowlThing(esk1_0)] 6: top(X0) != esk1_0 | [cowlThing(X0)] 7: [~(cB(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) 8: [~(cA(esk4_0))], xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing( esk2_0), ~(cowlThing(esk1_0)) Gamma_52: (resolve) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: [xsd_integer(esk3_0)], ~(xsd_string(esk3_0)), cowlNothing(esk2_0) 6: top(X0) != esk1_0 | [cowlThing(X0)] Gamma_53: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), [cowlNothing(esk2_0)] 6: top(X0) != esk1_0 | [cowlThing(X0)] Gamma_54: (resolve) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: [xsd_integer(esk3_0)], ~(xsd_string(esk3_0)) 6: top(X0) != esk1_0 | [cowlThing(X0)] Gamma_55: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: [xsd_string(esk3_0)] 2: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 3: [~(cowlNothing(esk2_0))] 4: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 5: xsd_integer(esk3_0), [~(xsd_string(esk3_0))] 6: top(X0) != esk1_0 | [cowlThing(X0)] Gamma_56: (move) 0: [~(xsd_integer(esk3_0))] 1: xsd_integer(esk3_0), [~(xsd_string(esk3_0))] 2: [xsd_string(esk3_0)] 3: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 4: [~(cowlNothing(esk2_0))] 5: xsd_integer(esk3_0), ~(xsd_string(esk3_0)), cowlNothing(esk2_0), [~( cowlThing(esk1_0))] 6: top(X0) != esk1_0 | [cowlThing(X0)] Gamma_57: (resolve) 0: [~(xsd_integer(esk3_0))] 1: xsd_integer(esk3_0), [~(xsd_string(esk3_0))] 2: [xsd_integer(esk3_0)] 3: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 4: [~(cowlNothing(esk2_0))] Gamma_58: (extend-conflict) 0: [~(xsd_integer(esk3_0))] 1: xsd_integer(esk3_0), [~(xsd_string(esk3_0))] 2: [xsd_integer(esk3_0)] 3: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 4: [~(cowlNothing(esk2_0))] Gamma_59: (resolve) 0: [~(xsd_integer(esk3_0))] 1: xsd_integer(esk3_0), [~(xsd_string(esk3_0))] 2: [] 3: top(X0) != esk3_0 | [xsd_integer(X0)], xsd_string(X0) 4: [~(cowlNothing(esk2_0))] SZS status Unsatisfiable