Solving a contradiction in premises

Question

I've got a set of premises:

$m \rightarrow j, a \rightarrow j, \neg m \rightarrow a, a \rightarrow \neg j$

Clearly, $a \rightarrow \neg j$ Contradicts $a \rightarrow j$

I'm asked to proof that out of these premises follows the following consequence:

$\neg a, m,j$

How do I proceed solving this?

P.S. These are the premises in words:

(a) John comes if Mary or Ann comes. (b) Ann comes if Mary does not come. (c) If Ann comes, John does not.

I need to solve the question using Modus ponens and the corresponding axioms. Here is a link to the axioms: http://www.logicinaction.org/docs/ch2.pdf

They are in section 2.7 page 22.

Answer 1

We need, in addition to the axioms (1), (2) and (3) and using modus ponens as only rule of inference, the following "derived rules" :

(Taut-1) --- $(\varphi \rightarrow \psi), (\varphi \rightarrow \lnot \psi) \vdash \lnot \varphi$

corresponding to the tautology :

$\vDash_{TAUT} (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \lnot \psi) \rightarrow \lnot \varphi)$

and :

(Taut-2) --- $(\lnot \varphi \rightarrow \psi) \vdash (\lnot \psi \rightarrow \varphi)$

corresponding to the tautology :

$\vDash_{TAUT} (\lnot \varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$.

---

Now for the proof :

(1) $a \rightarrow j$ --- premise

(2) $a \rightarrow \lnot j$ --- premise

From the above premises (1) and (2), we apply the "derived rule" Taut-1 : $a \rightarrow j, a \rightarrow \lnot j \vdash \lnot a$ to derive :

(3) $\lnot a$

(4) $\lnot m \rightarrow a$ --- premise

From (4), we apply the "derived rule" Taut-2 : $\lnot m \rightarrow a \vdash \lnot a \rightarrow m$ to derive :

(5) $\lnot a \rightarrow m$

(6) $m$ --- from (3) and (5) by modus ponens

(7) $m \rightarrow j$ - premise

(8) $j$ --- from (6) and (7) by modus ponens.

Thus, the solution to the problem : "Can you invite people under these constraints ?" is :

$\lnot a, m, j$

i.e. do not invite Ann, but invite Mary and John.

---

---

Added

Now we have to prove the above "derived rules"; we proceed proving some preliminary Lemmas.

In your lecture notes, we have already the proof of [see Example 2.24, page 2-23 ]:

Lemma $0$ : $\vdash \varphi \rightarrow \varphi$.

Now we add :

Lemma 1 : $\varphi \rightarrow \psi, \psi \rightarrow \sigma \vdash \varphi \rightarrow \sigma$ (Syllogism)

Proof :

(1) $\varphi \rightarrow \psi$ --- assumed

(2) $\psi \rightarrow \sigma$ --- assumed

(3) $\vdash (\psi \rightarrow \sigma) \rightarrow (\varphi \rightarrow (\psi \rightarrow \sigma))$ --- Ax1

(4) $(\varphi \rightarrow (\psi \rightarrow \sigma))$ --- from (2) and (3) by modus ponens

(5) $\vdash (\varphi \rightarrow (\psi \rightarrow \sigma)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \sigma))$ --- Ax2

(6) $(\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \sigma)$ --- from (4) and (5) by modus ponens

(7) $\varphi \rightarrow \sigma$ --- from (1) and (6) by modus ponens.

Lemma 2 : $\vdash \lnot \varphi \rightarrow (\varphi \rightarrow \psi)$

Proof :

(1) $\vdash \lnot \varphi \rightarrow (\lnot \psi \rightarrow \lnot \varphi)$ --- Ax1

(2) $\vdash (\lnot \psi \rightarrow \lnot \varphi) \rightarrow (\varphi \rightarrow \psi)$ --- Ax3

(3) $\vdash \lnot \varphi \rightarrow (\varphi \rightarrow \psi)$ --- from (1) and (2) by Lemma 1 (Syll).

Lemma 3 : $\vdash \lnot \lnot \varphi \rightarrow \varphi$

Proof :

(1) $\vdash \lnot \lnot \varphi \rightarrow (\lnot \varphi \rightarrow \lnot \lnot \lnot \varphi)$ --- by Lemma 2

(2) $\vdash (\lnot \varphi \rightarrow \lnot \lnot \lnot \varphi) \rightarrow (\lnot \lnot \varphi \rightarrow \varphi)$ --- Ax3

(3) $\vdash \lnot \lnot \varphi \rightarrow (\lnot \lnot \varphi \rightarrow \varphi)$ --- by Syll

(4) $\vdash \lnot \lnot \varphi \rightarrow (\lnot \lnot \varphi \rightarrow \varphi) \rightarrow ((\lnot \lnot \varphi \rightarrow \lnot \lnot \varphi) \rightarrow (\lnot \lnot \varphi \rightarrow \varphi))$ --- Ax2

(5) $\vdash (\lnot \lnot \varphi \rightarrow \lnot \lnot \varphi) \rightarrow (\lnot \lnot \varphi \rightarrow \varphi)$ --- from (3) and (4) by modus ponens

(6) $\vdash (\lnot \lnot \varphi \rightarrow \lnot \lnot \varphi)$ --- Lemma $0$

(7) $\vdash \lnot \lnot \varphi \rightarrow \varphi$ --- from (5) and (6) by modus ponens.

Lemma 4 : $\vdash \varphi \rightarrow \lnot \lnot \varphi$

Proof :

(1) $\vdash (\lnot \lnot \lnot \varphi \rightarrow \lnot \varphi) \rightarrow (\varphi \rightarrow \lnot \lnot \varphi)$ --- Ax2

(2) $\vdash \lnot \lnot \lnot \varphi \rightarrow \lnot \varphi$ --- Lemma 3

(3) $\vdash \varphi \rightarrow \lnot \lnot \varphi$ --- from (1) and (2) by modus ponens.

---

Now we can prove the "derived rule" Taut-2 :

$(\lnot \varphi \rightarrow \psi) \vdash (\lnot \psi \rightarrow \varphi)$.

Proof :

(1) $\vdash (\lnot \varphi \rightarrow \lnot \lnot \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$ --- Ax3

(2) $\lnot \varphi \rightarrow \psi, \psi \rightarrow \lnot \lnot \psi \vdash \lnot \varphi \rightarrow \lnot \lnot \psi$ --- Syll

(3) $(\lnot \varphi \rightarrow \psi) \vdash (\lnot \psi \rightarrow \varphi)$ --- from (1) and (3) by modus ponens and Lemma 4

---

Lemma 5 : $(\varphi \rightarrow \psi) \vdash (\lnot \psi \rightarrow \lnot \varphi)$.

Proof :

(1) $\vdash (\lnot \lnot \varphi \rightarrow \lnot \lnot \psi) \rightarrow (\lnot \psi \rightarrow \lnot \varphi)$ --- Ax3

(2) $\vdash (\lnot \lnot \varphi \rightarrow \varphi)$ --- Lemma 3

(3) $\varphi \rightarrow \psi \vdash \lnot \lnot \varphi \rightarrow \psi$ --- from (2) and Syll

(4) $\vdash (\psi \rightarrow \lnot \lnot \psi)$ --- Lemma 4

(5) $\varphi \rightarrow \psi \vdash \lnot \lnot \varphi \rightarrow \lnot \lnot \psi$ --- from (3) and (4) by Syll

(6) $(\varphi \rightarrow \psi) \vdash (\lnot \psi \rightarrow \lnot \varphi)$ --- from (1) and (5) by modus ponens.

Lemma 6 : $(\lnot \varphi \rightarrow \varphi) \vdash (\psi \rightarrow \varphi)$

(1) $\vdash \lnot \varphi \rightarrow (\varphi \rightarrow \lnot \psi)$ --- Lemma 2

(2) $\vdash (\lnot \varphi \rightarrow (\varphi \rightarrow \lnot \psi)) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow (\lnot \varphi \rightarrow \lnot \psi))$ --- Ax2

(3) $\vdash (\lnot \varphi \rightarrow \varphi) \rightarrow (\lnot \varphi \rightarrow \lnot \psi)$ --- from (1) and (2) by modus ponens

(4) $\vdash (\lnot \varphi \rightarrow \lnot \psi) \rightarrow (\psi \rightarrow \varphi)$ --- Ax3

(5) $(\lnot \varphi \rightarrow \varphi) \vdash (\psi \rightarrow \varphi)$ --- from (3) and (4) by modus ponens and Syll.

Lemma 7 : $(\lnot \varphi \rightarrow \varphi) \vdash \varphi$

(1) $(\lnot \varphi \rightarrow \varphi) \vdash ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi)$ --- Lemma 6

(2) $\vdash ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi))$ --- Ax1

(3) $(\lnot \varphi \rightarrow \varphi) \vdash ((\lnot \varphi \rightarrow \varphi) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi))$ --- from (1) and (2) by modus ponens

(4) $\vdash ((\lnot \varphi \rightarrow \varphi) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi)) \rightarrow (((\lnot \varphi \rightarrow \varphi) \rightarrow (\lnot \varphi \rightarrow \varphi)) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi))$ --- Ax2

(5) $(\lnot \varphi \rightarrow \varphi) \vdash ((\lnot \varphi \rightarrow \varphi) \rightarrow (\lnot \varphi \rightarrow \varphi)) \rightarrow ((\lnot \varphi \rightarrow \varphi) \rightarrow \varphi)$ --- from (3) and (4) by modus ponens

(6) $\vdash (\lnot \varphi \rightarrow \varphi) \rightarrow (\lnot \varphi \rightarrow \varphi)$ --- Lemma $0$

(7) $(\lnot \varphi \rightarrow \varphi) \vdash (\lnot \varphi \rightarrow \varphi) \rightarrow \varphi$ --- from (5) and (6) by modus ponens

(8) $(\lnot \varphi \rightarrow \varphi) \vdash \varphi$ --- from (7) by modus ponens.

---

Now we can prove the "derived rule" Taut-1 :

$\varphi \rightarrow \psi, \varphi \rightarrow \lnot \psi \vdash \lnot \varphi$

Proof :

(1) $\varphi \rightarrow \psi$ --- assumed

(2) $\varphi \rightarrow \lnot \psi$ --- assumed

(3) $\lnot \lnot \psi \rightarrow \lnot \varphi$ --- from (2) by Lemma 5

(4) $\vdash \psi \rightarrow \lnot \lnot \psi$ --- Lemma 4

(5) $\psi \rightarrow \lnot \varphi$ --- from (3) and (4) by Syll

(6) $\varphi \rightarrow \lnot \varphi$ --- from (1) and (5) by Syll

(7) $\lnot \lnot \varphi \rightarrow \lnot \varphi$ --- from (6) by Lemma 5

(8) $(\lnot \lnot \varphi \rightarrow \lnot \varphi) \vdash \lnot \varphi$ --- Lemma 7

(9) $\varphi$ --- from (7) and (8) by modus ponens.

I'm sure you can simplify it ...

---

---

Note

With Ax1, Ax2, modus ponens and Lemma $0$, you can prove the Deduction Theorem : if $\Gamma, \alpha \vdash \beta$, then $\Gamma \vdash \alpha \rightarrow \beta$.

The proof is easy but tedious; you can find it in every mathematical logic textbook.

With the DT, some proof can be simplified; in addition, you can apply it to the "derived rules" $\alpha \vdash \beta$ in order to derive the corresponding theorems : $\vdash \alpha \rightarrow \beta$.

---

---

Final comment

Following amWhy's suggestion, if we rewrite the set of premises as follows :

$(¬m → a) → j, ¬m → a, a → ¬j$

we can simplify the proof :

(1) $(¬m → a) → j$ --- premise

(2) $¬m → a$ --- premise

(3) $j$ --- from (1) and (2) by mp

(4) $a \rightarrow \lnot j$ --- premise

here we need a new "derived rule" : $\varphi \rightarrow \lnot \psi \vdash \psi \rightarrow \lnot \varphi$ (call it : Taut-3) in order to derive from (4) :

(5) $j \rightarrow \lnot a$

(6) $\lnot a$ --- from (3) and (5) by mp

(7) $\lnot a \rightarrow m$ --- from (2) by Taut-2

(8) $m$ --- from (6) and (7) by mp.

Again we have the "solution" : $j, \lnot a, m$.

---

In order to complete this alternative proof, we have to prove the new "derived rule" Taut-3 :

$(\varphi \rightarrow \lnot \psi) \vdash (\psi \rightarrow \lnot \varphi)$.

Proof :

(1) $\varphi \rightarrow \lnot \psi$ --- assumed

(2) $\vdash \lnot \lnot \varphi \rightarrow \varphi$ --- Lemma 3

(3) $(\varphi \rightarrow \lnot \psi) \vdash (\lnot \lnot \varphi \rightarrow \lnot \psi)$ --- from (1) and (2) by Syll

(4) $\vdash (\lnot \lnot \varphi \rightarrow \lnot \psi) \rightarrow (\psi \rightarrow \lnot \varphi)$ --- Ax3

(5) $(\varphi \rightarrow \lnot \psi) \vdash (\psi \rightarrow \lnot \varphi)$ --- from (3) and (4) by mp.

With this approach, we can "save" Lemma 5, Lemma 6, Lemma 7 and Taut-1, which are replaced by Taut-3 only.

Answer 2

I use Polish notation.

Hint: You can derive CCpqCCrpCrq as a theorem scehma, and CCNppp as a theorem schema, and CNNpp also. Then since you have CNma and CaNj as premises you can deduce CNmNj. Then using the third axiom you'll get Cjm. Since you have Caj, using CCpqCCrpCrq again you can derive Cam. Since you have CNma, and Cam then, you can deduce CNmm by CCpqCCrpCrq. Then using CCNppp you can deduce m. Since you have Cmj, you can then get j. Since you have CNNaa and CaNj you can use CCpqCCrpCrq to get to CNNaNj. Using CCNpNqCqp you can then infer CjNa. Since you have j, you can then infer Na.

Update:

The relevant formation rules for your system (p.11 chapter 2) here go:

1. All lower case letters of the Latin alphabet are formulas.
2. If $\phi$ is a formula, then so is $\lnot$$\phi$.
3. If $\phi$ and $\psi$ are formulas, then so is ($\phi$$\rightarrow$$\psi$).

In Polish notation, the formation rules go:

1. All lower case letters of the Latin alphabet are formulas.
2. If $\phi$ is a formula, then so is N$\phi$.
3. If $\phi$ and $\psi$ are formulas, then so is C$\phi$$\psi$.

To convert from Polish notation to (fully parenthesized infix) notation the above will suffice. I use lower case Latin letters for the variables in axioms instead of Greek variables, and allow substitution for those variables. But, we can't validly make substitutions for "m", "j", and "a" for this problem, so really I should say that for this problem the first formation rule says

1. All lower case letters of the Latin alphabet, except "a", "j" and "m" are formulas.

I just didn't do that before, because I pointed out these formation rules to help you to translate between Polish notation and infix notation. The axioms you have go

  Polish notation   Infix notation

3 CpCqp             (p→(q→p)) recursive variable prefixing 

4 CCpCqrCCpqCpr     ((p→(q→r))→((p→q)→(p→r))) self-distribution 

5 CCNpNqCqp         ((¬p→¬q)→(q→p)) strong transposition 

We want to prove as theorems

  CCpqCCrpCrq       ((p→q)→((r→p)→(r→q))) double prefixing 

  CCNppp            ((¬p→p)→p) Clavius or "key"

  CNNpp             (¬¬p→p) double negation elimination

Now first let's make two copies of 3 and put them above and below each other.

 3 C p    Cqp
     |
    -----
 3  CpCqp

Now we could at this point assume that p/CpCqp and thus get C CpCqp CqCpCqp by substitution. Then we can infer CqCpCqp by detachment. This is not incorrect. However, it comes as more useful to notice that the "q" on the right side of "3" doesn't appear on the left hand side of 3. Thus, we can change it to something not in CpCqp and obtain a more general formula. Thus, p/CpCqp, q/r in 3 allows us to wrtie C CpCqp CrCpCqp, and thus since we have CpCqp we can detach

7 CrCpCqp.

If we had inferred to CqCpCqp, we would have a less general formula than 7, in the sense that 7 r/p yields CqCpCqp, but there is no way to move from CqCpCqp to CrCpCqp by uniform substitution (all instances of a variable that get substituted for in a formula need to get substituted by the very same formula... in CqCpCqp if we substitute a formula for q, we need to substitute that same formula for each q in CqCpCqp).

We can summarize this by writing D3.3=7.

Now let's make two copies of 4 also.

4 C C p     C q   r CCpqCpr
      |       |   |
      -----   --- ---
4   C CpCqr C Cpq Cpr

Thus the diagram here suggests that we substitute p/CpCqr, q/Cpq, r/Cpr. Doing these substitutions transforms 4 into C CCpCqrCCpqCpr CCCpCqrCpqCCpCqrCpr. Thus, since CCpCqrCCpqCpr is an axiom, by detachment we can infer (D4.4=8).

8 CCCpCqrCpqCCpCqrCpr.

Now let's put 3 and 4 next to each other, and assume that we want to make "3" into the longer formula of the form C$\alpha$$\beta$ and 4 into the formula $\alpha$.

3  C p Cqp
     |
     -------------
4    CCpCqrCCpqCpr

Again "q" doesn't appear anywhere on the left hand side of 3. So, we can infer (D3.4).

9 CsCCpCqrCCpqCpr.

You've seen D4.3 before in another answer, just in infix notation. So, D4.3=10

10 CCpqCpp. ((p→q)→(p→p))

Now we'll figure out D4.5

4 C C p     C q r CCpqCpr
      |       | |
      -----   | |
5   C CNpNq C q p

So 4 p/CNpNq, r/p allows us to detach

11 CCCNpNqqCCNpNqp.

D3.5 has a similar diagram to any time you have "3" first. So, D3.5 yields

12 CrCCNpNqCqp.

D3.7 yields

13 CsCrCpCqp.

D10.7 you've seen elsewhere and thus we have

14 Cpp.

Now we'll look at D4.14 which involves something which strikes me as more complicated.

4 C C p Cqr CCpqCpr
      | ---
      | |
14  C p p

Now you can only substitute variables with formula. You can't substitute any formula with a variable. Thus, the upper "p" can't get substituted by the lower "p". But, the lower "p" needs substituted with "Cqr". Things may become easier to see if we relabel the variables of 4 by other letters so that it doesn't have any lower case letters in common with 14 as follows:

4 C C p Cqr CCpqCpr
4 C C x Cbc CCxbCxc
      | ---
      | |
14  C p p

So here in 4 x/p, and in 14 p/Cbc. But substitution needs to come as uniform. Thus, if we apply p/Cbc in 14, we also need to apply x/Cbc in 4 instead of x/p in 14. Consequently, 4 becomes C CCbcCbc CCCbcbCCbcc and 14 becomes CCbcCbc. Then we can infer

15 CCCbcbCCbcc.

For D4.12 we can write the following

4 C C p C q     r CCpqCpr
      |   |     |
      |   ----- ---
12  C r C CNpNq Cqp

So 4 p/r, q/CNpNq, r/Cqp makes 4 and 12 into a common form, and thus we can infer

16 CCrCNpNqCrCqp.

Now D16.3

 16 C C r C Np Nq CrCqp
        |   -- --
        |   |  |
 3    C p C q  p

So it might look like 16 r/p, and 3 q/Np, p/Nq will work. But again, substitutions need to come as uniform. So if q/Np, p/Nq in 3, then 3 transforms into CNqCNpNq. And thus in 16 we need r/Nq. Then the left hand side (or antecedent) of 16 and 3 unite into a most general common form. And from that we can infer

17 CNqCqp.

D4.17 comes as straightforward. 4 along with detachment allows you to infer from C$\alpha$C$\beta$$\gamma$ to CC$\alpha$$\beta$C$\alpha$$\gamma$. So, D4.17 yields

18 CCNqqCNqp.

D3.17 follows the pattern of D3.3, D3.4, and D3.[any formula]. So D3.17 yields

19 CrCNqCqp.

For D15.19

15 C C Cbc b CCbcc
       --- | 
       |   ------
19   C r   CNqCqp

Now if b/CNqCqp in 15, then in 19 r/CCNqCqpc. From that we can infer

20 CCCNqCqpcc.

D8.13

8 C C CpCqr C p q CCpCqrCpr
      -----   | | 
      |       | -----
13  C s     C r CpCqp

Since "s" only appears at one spot in 13, we need not worry about any substitution for "s" changing any substitution made in 8. But we also have substitutions happening in both 8 and 13. So, as before, let's change the variables of 8 as follows:

8  C C CpCqr C p q CCpCqrCpr
   C C CxCbc C x b CCxCbcCxc
       -----   | | 
       |       | -----
13  C  s     C r CpCqp

Thus in 8 x/r, b/CpCqp (and the substitution in 13) allows us to detach

21 CCrCCpCqpcCrc.

D8.7

8 C C CpCqr C p q CCpCqrCpr
8 C C CxCbc C x b CCxCbcCxc
      -----   | |
      |       | |
7   C r     C p Cqp

Thus we can infer

22 CCpCCqpcCpc.

D22.9

22 C C p CC q p   c Cpc
       |    | |   |
       |    | --- -------
9    C s CC p Cqr CCpqCpr

Here we need not re-letter 22. Thus, we can infer

23 CCqrCCpqCpr. or equivalently CCpqCCrpCrq.

D21.23

 21 C C r   C C p Cqp c Crc
 21 C C x   C C y Czy b Cxb      
        |       | --- |
        ---     | |   ---
 23   C Cpq C C r p   Crq

So in 21 we have x/Cpq, y/r, b/Crq as suggested. In 23 we have p/Czy. We also have y/r. So, in 23 we have p/Czr. And in 21 we actually need x/CCzrq, y/r, b/Crq. Thus, we can detach

25 CCCzrqCrq.

D25.11

25 C C C z     r q Crq
         |     | |
         ----- | -------
11   C C CNpNq q CCNpNqp

Thus, we can infer

26 CqCCNpNqp.

D4.26 yields

27 CCqCNpNqCqp.

Now D20.27

20 C C C Nq C q  p  c  c
20 C C C Nx C x  y  z  z
         --   |  |  |
         |    -- -- ---
27   C C q  C Np Nq Cqp

So in 20 x/Np, y/Nq, z/Cqp, and in 27 q/Nx comes as suggested. In 20 we thus really can use x/Np, y/NNq, z/CNxp... but we still have an "x" on the right and left hand side of the "/". So, we actually want x/Np, y/NNq, z/CNNpp. Thus we can detach

28 CNNpp.

D27.18

27  C C q    C N p Nq Cqp
        |        | --
        ----     | |
18    C CNqq C N q p

And thus we can detach

29 CCNqqq or equivalently CCNppp.

From here on the left you'll see either "premise" or the theorem/axiom which justifies a step, or (x, y) to indicate that the previous two lines got inferred from "x" and "y" with "x" as the longer formula (or "major premise" in other terminology).

Premise      1 Cmj or (m→j)

Premise      2 Caj or (a→j)

Premise      3 CNma or (¬m→a)

Premise      4 CaNj or (a→¬j)

CCpqCCrpCrq  5 CCaNjCCNmaCNmNj

(5, 4)       6 CCNmaCNmNj

(6, 3)       7 CNmNj

CCNpNqCqp    8 CCNmNjCjm

(8, 7)       9 Cjm

CCpqCCrpCrq 10 CCjmCCajCam

(10, 9)     11 CCajCam

(11, 2)     12 Cam

CCpqCCrpCrq 13 CCamCCNmaCNmm

(13, 12)    14 CCNmaCNmm

(14, 3)     15 CNmm

CCNppp      16 CCNmmm

(16, 15)    17 m

(1, 17)     18 j

CNNpp       19 CNNaa

CCpqCCrpCrq 20 CCaNjCCNNaaCNNaNj

(20, 4)     21 CCNNaaCNNaNj

(21, 19)    22 CNNaNj

CCNpNqCqp   23 CCNNaNjCjNa

(23, 22)    24 CjNa

(24, 18)    25 Na.