%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-
not ground preserving

Gamma_0: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]

Gamma_1: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]

Gamma_2: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]

Gamma_3: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]

Gamma_4: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]

Gamma_5: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]

Gamma_6: (extend-no-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]
  6: [isa(f_citynamedfn(s_agen,c_france),c_individual)], ~(individual(f_citynamedfn(s_agen,c_france)))

Gamma_7: (extend-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]
  6: [isa(f_citynamedfn(s_agen,c_france),c_individual)], ~(individual(f_citynamedfn(s_agen,c_france)))
  7: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]

Gamma_8: (move)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]
  6: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]
  7: [isa(f_citynamedfn(s_agen,c_france),c_individual)], ~(individual(f_citynamedfn(s_agen,c_france)))

Gamma_9: (resolve)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]
  6: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]
  7: [~(individual(f_citynamedfn(s_agen,c_france)))]

Gamma_10: (extend-conflict)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [individual(f_citynamedfn(s_agen,c_france))]
  6: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]
  7: [~(individual(f_citynamedfn(s_agen,c_france)))]

Gamma_11: (move)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [~(individual(f_citynamedfn(s_agen,c_france)))]
  6: [individual(f_citynamedfn(s_agen,c_france))]
  7: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]

Gamma_12: (resolve)
  0: [mtvisible(c_reasoningaboutpossibleantecedentsmt)]
  1: [natargument(f_citynamedfn(X0,X1),n_2,X1)]
  2: [natargument(f_citynamedfn(X0,X1),n_1,X0)]
  3: [natfunction(f_citynamedfn(X0,X1),c_citynamedfn)]
  4: [city(f_citynamedfn(X0,X1))]
  5: [~(individual(f_citynamedfn(s_agen,c_france)))]
  6: []
  7: [~(isa(f_citynamedfn(s_agen,c_france),c_individual))]

SZS status Unsatisfiable