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