A Theorem with Contradictory Axioms

The USA is a country. The capital of every country is a beautiful big city Washington is the capital of the USA, and it's not a big city. Every big city has crime. A big city is a city. Prove there is some city that is beautiful and has no crime. Then prove there is some city that is beautiful and has crime.

%------------------------------------------------------------------------------
%----The USA is a country.
fof(usa,axiom,
    country(usa) ).

%----The capital of every country is a beautiful big city
fof(country_big_city,axiom,
    ! [C] :
      ( country(C)
     => ( big_city(capital_of(C))
        & beautiful(capital_of(C)) ) ) ).

%----Washington is the capital of the USA, and it's not a big city.
fof(usa_capital_axiom,axiom,
    ( capital_of(usa) = washington
    & ~ big_city(washington) ) ).

%----Every big city has crime.
fof(crime_axiom,axiom,
    ! [C] :
      ( big_city(C)
     => has_crime(C) ) ).

%----A big city is a city.
fof(big_city_city,axiom,
    ! [C] :
      ( big_city(C)
     => city(C) ) ).

%----There is some city that is beautiful and has (no) crime.
fof(some_beautiful_crime,conjecture,
    ? [C] :
      ( city(C)
      & beautiful(C)
      & ~ has_crime(C) ) ).
%------------------------------------------------------------------------------