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