Help with a Predicate Logic homework proof

Question

I have a Predicate Logic argument I need to translate into the symbolism of predicate logic first and then I need to construct a proof in CP.

The argument is "Some wars are just. No war of aggression is just. Therefore, there are wars that are not wars of aggression. (Wx = x is a war, Jx = x is just, Ax = x is a war of aggression)."

I think I have it translated right, however, I am lost on how to construct the proof into CP.

This is how I have translated it (∃x) (Wx • Jx), (x) (Ax → ~Jx) ∴ (∃x) (Wx • ~Ax)

I need help with the CP proof. Any help would be very much appreciated!

I am also only allowed to use implicational rules like, MP, MT, HS, DS, CD, Simp, Conj, and Add. Equivalence rules such as DN, Com, As, DeM, Cont, Dist, Ex, Re, ME, MI. As well as QN, UI, EG, EI, UG.

Answer 1

Your translations are okay, but as Philip Klöcking♦ suggests, it would be better to use Ax to only mean x is of aggression, so that "x is a war of aggression" is represented: Wx • Ax and so forth.

Thus the proof becomes easy, so I'll just start you off.

 1.|  (∃x) (Wx • Jx)        Premise
 2.|_ (Ɐx) (Wx • Ax → ~Jx)  Premise
 3.|[c]|_ Wc • Jc           Assumption (of Witness c ; aka Existential Instantiation)
 4.|   |  Wc                • Elimination (aka Simplification)
 5.|   |  Jc                • Elimination (aka Simplification)
 6.|   |  Wc • Ac → ~Jc     Ɐ Elimination (aka Universal Instantiation)
 7.|   |   |_ Ac            Assumption
   :   :   :  ...
   :   :
   |  (∃x) (Wx • ~Ax)