%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] Gamma_1: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) Gamma_2: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] Gamma_3: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] Gamma_4: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) Gamma_5: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) Gamma_6: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) Gamma_7: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 7: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), ~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)), [geographicalsubregions( c_georegion_l2_x5_y8,c_georegion_l4_x45_y72)] Gamma_8: (extend-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 7: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), ~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)), [geographicalsubregions( c_georegion_l2_x5_y8,c_georegion_l4_x45_y72)] 8: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_9: (move) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 7: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] 8: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), ~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)), [geographicalsubregions( c_georegion_l2_x5_y8,c_georegion_l4_x45_y72)] Gamma_10: (resolve) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 7: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] 8: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)) Gamma_11: (extend-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 7: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] 8: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24))] Gamma_12: (move) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24))] 7: [geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24)], ~( mtvisible(c_tptpgeo_member7_mt)) 8: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_13: (resolve) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24))] 7: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( mtvisible(c_tptpgeo_member7_mt))] 8: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_14: (extend-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 2: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 4: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 5: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 6: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24))] 7: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( mtvisible(c_tptpgeo_member7_mt)) 8: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_15: (move) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( mtvisible(c_tptpgeo_member7_mt)) 2: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)], ~( mtvisible(c_tptpgeo_member7_mt)) 3: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l3_x15_y24)] 4: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [geographicalregion( c_georegion_l4_x45_y72)] 5: [geographicalsubregions(c_georegion_l4_x45_y72,c_georegion_l4_x45_y72)], ~( geographicalregion(c_georegion_l4_x45_y72)) 6: [geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l3_x15_y24)], ~( geographicalregion(c_georegion_l3_x15_y24)) 7: ~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72)), [~( geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24))] 8: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_16: (resolve) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( mtvisible(c_tptpgeo_member7_mt)) 2: [~(mtvisible(c_tptpgeo_member7_mt))] 3: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_17: (extend-conflict) 0: [mtvisible(c_tptpgeo_member7_mt)] 1: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( mtvisible(c_tptpgeo_member7_mt)) 2: [~(mtvisible(c_tptpgeo_member7_mt))] 3: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_18: (move) 0: [~(mtvisible(c_tptpgeo_member7_mt))] 1: [mtvisible(c_tptpgeo_member7_mt)] 2: [~(geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72))], ~( mtvisible(c_tptpgeo_member7_mt)) 3: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] Gamma_19: (resolve) 0: [~(mtvisible(c_tptpgeo_member7_mt))] 1: [] 2: [~(geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l4_x45_y72))] SZS status Unsatisfiable