Froggy Problem Solved by underscores and barred premisses

Lewis Carroll's Froggy problem using the Dictionary given by Lewis Carroll. I have followed the method and roughly the presentation used by Carroll in "The Pigs and Balloons Problem" Book XIII Chapter XII as published by Bartley from a Carroll manuscript dated 7/2/93.

Bartley explains how to handle the case where a term appears in one premiss (say A) whereas its complement appears in two or more premisses (say B and C). In Carroll's terminology, premiss A is thus *barred* by premisses B and C. His rule is that a barred premiss may not be used until all the premisses barring it have been used. However, no mention is made of the case where both the term and its complement appear in two or more premisses. The solution I have devised, which seems to me logical and has the added merit that it seems to work, is as follows:
Apply Carroll's original rule to determine barred premisses. After using a premiss, recreate the register omitting the used premiss and re-apply Carroll's rule to determine the new bars, but of course honouring the bars that still remain from the previous list.

Here is the symbolic form of the problem. I have divided Carroll's premisses 3,11 and 17 into their consituent parts as in Carroll's method of trees but I have renumbered the resulting premisses instead of using Carroll's notation of 3*, 3** etc.

New number | Carroll's number | Symbolic form of premiss |

1 | 1 | ~s ~r |

2 | 2 | ~m h d |

3 | 3* | E ~a |

4 | 4 | l n ~v |

5 | 5 | z m c |

6 | 6 | t ~A |

7 | 7 | ~s ~n c r |

8 | 8 | z v ~m |

9 | 9 | E ~w |

10 | 10 | v k m ~t |

11 | 11* | E ~s |

12 | 12 | A B |

13 | 13 | k ~h ~n |

14 | 14 | r ~c |

15 | 15 | ~v ~a ~h ~l |

16 | 16 | w ~t s ~n |

17 | 17* | d ~e |

18 | 18 | s n ~b ~B |

19 | 19 | w e ~z |

20 | 20 | ~t ~A ~r ~c n |

21 | 3** | E k |

22 | 11** | E ~c |

23 | 11*** | E n |

24 | 17** | d ~k |

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | 18 | |

c | 5 7 | 14 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 18 20 23 | 7 13 16 |

r | 7 14 | 1 20 |

s | 16 18 | 1 7 11 |

t | 6 | 10 16 20 |

v | 8 10 | 4 15 |

w | 16 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 | 18 |

12 | barred by | 6 20 |

6 | barred by | 10 16 20 |

19 | barred by | 5 8 |

9 | barred by | 16 19 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

Using proposition 1 add ~s ~r to the solution string

so the solution string becomes:

~s ~r

so the solution string becomes:

~s ~r

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | 18 | |

c | 5 7 | 14 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 18 20 23 | 7 13 16 |

r | 7 14 | 20 |

s | 16 18 | 7 11 |

t | 6 | 10 16 20 |

v | 8 10 | 4 15 |

w | 16 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 | 18 |

12 | barred by | 6 20 |

6 | barred by | 10 16 20 |

20 | barred by | 7 14 |

19 | barred by | 5 8 |

9 | barred by | 16 19 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

Using proposition 7 add ~s ~n c r to the solution string

so the solution string becomes:

~s ~r ~s ~n c r

so the solution string becomes:

~s ~r ~s ~n c r

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | 18 | |

c | 5 | 14 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 18 20 23 | 13 16 |

r | 14 | 20 |

s | 16 18 | 11 |

t | 6 | 10 16 20 |

v | 8 10 | 4 15 |

w | 16 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 | 18 |

12 | barred by | 6 20 |

5 | barred by | 14 20 22 |

20 | barred by | 14 |

2 | barred by | 13 15 |

11 | barred by | 16 18 |

24 | barred by | 10 13 21 |

6 | barred by | 10 16 20 |

19 | barred by | 5 8 |

9 | barred by | 16 19 |

From the solution string ~s ~r ~s ~n c r

we can delete "r" giving:

~s ~s ~n c

we can delete "r" giving:

~s ~s ~n c

Using proposition 16 add w ~t s ~n to the solution string

so the solution string becomes:

~s ~s ~n c w ~t s ~n

so the solution string becomes:

~s ~s ~n c w ~t s ~n

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | 18 | |

c | 5 | 14 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 18 20 23 | 13 |

r | 14 | 20 |

s | 18 | 11 |

t | 6 | 10 20 |

v | 8 10 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 | 18 |

12 | barred by | 6 20 |

5 | barred by | 14 20 22 |

20 | barred by | 14 |

2 | barred by | 13 15 |

11 | barred by | 18 |

24 | barred by | 10 13 21 |

13 | barred by | 4 18 20 23 |

6 | barred by | 10 20 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string ~s ~s ~n c w ~t s ~n

we can delete "s" giving:

~n c w ~t ~n

we can delete "s" giving:

~n c w ~t ~n

Using proposition 18 add s n ~b ~B to the solution string

so the solution string becomes:

~n c w ~t ~n s n ~b ~B

so the solution string becomes:

~n c w ~t ~n s n ~b ~B

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 14 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 20 23 | 13 |

r | 14 | 20 |

s | 11 | |

t | 6 | 10 20 |

v | 8 10 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 |

12 | barred by | 6 20 |

5 | barred by | 14 20 22 |

20 | barred by | 14 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

13 | barred by | 4 20 23 |

6 | barred by | 10 20 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string ~n c w ~t ~n s n ~b ~B

we can delete "n" giving:

c w ~t s ~b ~B

we can delete "n" giving:

c w ~t s ~b ~B

Using proposition 14 add r ~c to the solution string

so the solution string becomes:

c w ~t s ~b ~B r ~c

so the solution string becomes:

c w ~t s ~b ~B r ~c

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 20 23 | 13 |

r | 20 | |

s | 11 | |

t | 6 | 10 20 |

v | 8 10 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 11 21 22 23 | |

B | 12 |

12 | barred by | 6 20 |

5 | barred by | 20 22 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

13 | barred by | 4 20 23 |

6 | barred by | 10 20 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string c w ~t s ~b ~B r ~c

we can delete "c" giving:

w ~t s ~b ~B r

we can delete "c" giving:

w ~t s ~b ~B r

Using proposition 11 add E ~s to the solution string

so the solution string becomes:

w ~t s ~b ~B r E ~s

so the solution string becomes:

w ~t s ~b ~B r E ~s

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 20 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 20 23 | 13 |

r | 20 | |

s | ||

t | 6 | 10 20 |

v | 8 10 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 20 |

E | 3 9 21 22 23 | |

B | 12 |

12 | barred by | 6 20 |

5 | barred by | 20 22 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

13 | barred by | 4 20 23 |

6 | barred by | 10 20 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string w ~t s ~b ~B r E ~s

we can delete "s" giving:

w ~t ~b ~B r E

we can delete "s" giving:

w ~t ~b ~B r E

Using proposition 20 add ~t ~A ~r ~c n to the solution string

so the solution string becomes:

w ~t ~b ~B r E ~t ~A ~r ~c n

so the solution string becomes:

w ~t ~b ~B r E ~t ~A ~r ~c n

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 10 13 21 | 24 |

l | 4 | 15 |

m | 5 10 | 2 8 |

n | 4 23 | 13 |

r | ||

s | ||

t | 6 | 10 |

v | 8 10 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 |

E | 3 9 21 22 23 | |

B | 12 |

12 | barred by | 6 |

5 | barred by | 22 |

2 | barred by | 13 15 |

24 | barred by | 10 13 21 |

13 | barred by | 4 23 |

6 | barred by | 10 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string w ~t ~b ~B r E ~t ~A ~r ~c n

we can delete "r" giving:

w ~t ~b ~B E ~t ~A ~c n

we can delete "r" giving:

w ~t ~b ~B E ~t ~A ~c n

Using proposition 10 add v k m ~t to the solution string

so the solution string becomes:

w ~t ~b ~B E ~t ~A ~c n v k m ~t

so the solution string becomes:

w ~t ~b ~B E ~t ~A ~c n v k m ~t

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 13 21 | 24 |

l | 4 | 15 |

m | 5 | 2 8 |

n | 4 23 | 13 |

r | ||

s | ||

t | 6 | |

v | 8 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | 6 |

E | 3 9 21 22 23 | |

B | 12 |

12 | barred by | 6 |

5 | barred by | 22 |

2 | barred by | 13 15 |

24 | barred by | 13 21 |

13 | barred by | 4 23 |

19 | barred by | 5 8 |

9 | barred by | 19 |

8 | barred by | 4 15 |

Using proposition 6 add t ~A to the solution string

so the solution string becomes:

w ~t ~b ~B E ~t ~A ~c n v k m ~t t ~A

so the solution string becomes:

w ~t ~b ~B E ~t ~A ~c n v k m ~t t ~A

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 13 21 | 24 |

l | 4 | 15 |

m | 5 | 2 8 |

n | 4 23 | 13 |

r | ||

s | ||

t | ||

v | 8 | 4 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | |

E | 3 9 21 22 23 | |

B | 12 |

5 | barred by | 22 |

2 | barred by | 13 15 |

24 | barred by | 13 21 |

13 | barred by | 4 23 |

19 | barred by | 5 8 |

9 | barred by | 19 |

8 | barred by | 4 15 |

From the solution string w ~t ~b ~B E ~t ~A ~c n v k m ~t t ~A

we can delete "t" giving:

w ~b ~B E ~A ~c n v k m ~A

we can delete "t" giving:

w ~b ~B E ~A ~c n v k m ~A

Using proposition 4 add l n ~v to the solution string

so the solution string becomes:

w ~b ~B E ~A ~c n v k m ~A l n ~v

so the solution string becomes:

w ~b ~B E ~A ~c n v k m ~A l n ~v

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 13 21 | 24 |

l | 15 | |

m | 5 | 2 8 |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | 8 | 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | 12 | |

E | 3 9 21 22 23 | |

B | 12 |

5 | barred by | 22 |

2 | barred by | 13 15 |

24 | barred by | 13 21 |

13 | barred by | 23 |

19 | barred by | 5 8 |

9 | barred by | 19 |

8 | barred by | 15 |

From the solution string w ~b ~B E ~A ~c n v k m ~A l n ~v

we can delete "v" giving:

w ~b ~B E ~A ~c n k m ~A l n

we can delete "v" giving:

w ~b ~B E ~A ~c n k m ~A l n

Using proposition 12 add A B to the solution string

so the solution string becomes:

w ~b ~B E ~A ~c n k m ~A l n A B

so the solution string becomes:

w ~b ~B E ~A ~c n k m ~A l n A B

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 15 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 15 |

k | 13 21 | 24 |

l | 15 | |

m | 5 | 2 8 |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | 8 | 15 |

w | 19 | 9 |

z | 5 8 | 19 |

A | ||

E | 3 9 21 22 23 | |

B |

5 | barred by | 22 |

2 | barred by | 13 15 |

24 | barred by | 13 21 |

13 | barred by | 23 |

19 | barred by | 5 8 |

9 | barred by | 19 |

8 | barred by | 15 |

From the solution string w ~b ~B E ~A ~c n k m ~A l n A B

we can delete "A" giving:

w ~b ~B E ~c n k m l n B

we can delete "A" giving:

w ~b ~B E ~c n k m l n B

From the solution string w ~b ~B E ~c n k m l n B

we can delete "B" giving:

w ~b E ~c n k m l n

we can delete "B" giving:

w ~b E ~c n k m l n

Using proposition 15 add ~v ~a ~h ~l to the solution string

so the solution string becomes:

w ~b E ~c n k m l n ~v ~a ~h ~l

so the solution string becomes:

w ~b E ~c n k m l n ~v ~a ~h ~l

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 5 | 2 8 |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | 8 | |

w | 19 | 9 |

z | 5 8 | 19 |

A | ||

E | 3 9 21 22 23 | |

B |

5 | barred by | 22 |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

19 | barred by | 5 8 |

9 | barred by | 19 |

From the solution string w ~b E ~c n k m l n ~v ~a ~h ~l

we can delete "l" giving:

w ~b E ~c n k m n ~v ~a ~h

we can delete "l" giving:

w ~b E ~c n k m n ~v ~a ~h

Using proposition 8 add z v ~m to the solution string

so the solution string becomes:

w ~b E ~c n k m n ~v ~a ~h z v ~m

so the solution string becomes:

w ~b E ~c n k m n ~v ~a ~h z v ~m

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | 5 | 22 |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 5 | 2 |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | 19 | 9 |

z | 5 | 19 |

A | ||

E | 3 9 21 22 23 | |

B |

5 | barred by | 22 |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

19 | barred by | 5 |

9 | barred by | 19 |

From the solution string w ~b E ~c n k m n ~v ~a ~h z v ~m

we can delete "m" giving:

w ~b E ~c n k n ~v ~a ~h z v

we can delete "m" giving:

w ~b E ~c n k n ~v ~a ~h z v

From the solution string w ~b E ~c n k n ~v ~a ~h z v

we can delete "v" giving:

w ~b E ~c n k n ~a ~h z

we can delete "v" giving:

w ~b E ~c n k n ~a ~h z

Using proposition 22 add E ~c to the solution string

so the solution string becomes:

w ~b E ~c n k n ~a ~h z E ~c

so the solution string becomes:

w ~b E ~c n k n ~a ~h z E ~c

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | 5 | |

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 5 | 2 |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | 19 | 9 |

z | 5 | 19 |

A | ||

E | 3 9 21 23 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

19 | barred by | 5 |

9 | barred by | 19 |

Using proposition 5 add z m c to the solution string

so the solution string becomes:

w ~b E ~c n k n ~a ~h z E ~c z m c

so the solution string becomes:

w ~b E ~c n k n ~a ~h z E ~c z m c

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 17 24 | |

e | 19 | 17 |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 2 | |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | 19 | 9 |

z | 19 | |

A | ||

E | 3 9 21 23 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

9 | barred by | 19 |

From the solution string w ~b E ~c n k n ~a ~h z E ~c z m c

we can delete "c" giving:

w ~b E n k n ~a ~h z E z m

we can delete "c" giving:

w ~b E n k n ~a ~h z E z m

Using proposition 19 add w e ~z to the solution string

so the solution string becomes:

w ~b E n k n ~a ~h z E z m w e ~z

so the solution string becomes:

w ~b E n k n ~a ~h z E z m w e ~z

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 17 24 | |

e | 17 | |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 2 | |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | 9 | |

z | ||

A | ||

E | 3 9 21 23 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

From the solution string w ~b E n k n ~a ~h z E z m w e ~z

we can delete "z" giving:

w ~b E n k n ~a ~h E m w e

we can delete "z" giving:

w ~b E n k n ~a ~h E m w e

Using proposition 9 add E ~w to the solution string

so the solution string becomes:

w ~b E n k n ~a ~h E m w e E ~w

so the solution string becomes:

w ~b E n k n ~a ~h E m w e E ~w

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 17 24 | |

e | 17 | |

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 2 | |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 21 23 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

From the solution string w ~b E n k n ~a ~h E m w e E ~w

we can delete "w" giving:

~b E n k n ~a ~h E m e E

we can delete "w" giving:

~b E n k n ~a ~h E m e E

Using proposition 17 add d ~e to the solution string

so the solution string becomes:

~b E n k n ~a ~h E m e E d ~e

so the solution string becomes:

~b E n k n ~a ~h E m e E d ~e

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 24 | |

e | ||

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 2 | |

n | 23 | 13 |

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 21 23 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

13 | barred by | 23 |

From the solution string ~b E n k n ~a ~h E m e E d ~e

we can delete "e" giving:

~b E n k n ~a ~h E m E d

we can delete "e" giving:

~b E n k n ~a ~h E m E d

Using proposition 23 add E n to the solution string

so the solution string becomes:

~b E n k n ~a ~h E m E d E n

so the solution string becomes:

~b E n k n ~a ~h E m E d E n

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 24 | |

e | ||

h | 2 | 13 |

k | 13 21 | 24 |

l | ||

m | 2 | |

n | 13 | |

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 21 | |

B |

2 | barred by | 13 |

24 | barred by | 13 21 |

Using proposition 13 add k ~h ~n to the solution string

so the solution string becomes:

~b E n k n ~a ~h E m E d E n k ~h ~n

so the solution string becomes:

~b E n k n ~a ~h E m E d E n k ~h ~n

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 2 24 | |

e | ||

h | 2 | |

k | 21 | 24 |

l | ||

m | 2 | |

n | ||

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 21 | |

B |

24 | barred by | 21 |

From the solution string ~b E n k n ~a ~h E m E d E n k ~h ~n

we can delete "n" giving:

~b E k ~a ~h E m E d E k ~h

we can delete "n" giving:

~b E k ~a ~h E m E d E k ~h

Using proposition 2 add ~m h d to the solution string

so the solution string becomes:

~b E k ~a ~h E m E d E k ~h ~m h d

so the solution string becomes:

~b E k ~a ~h E m E d E k ~h ~m h d

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 24 | |

e | ||

h | ||

k | 21 | 24 |

l | ||

m | ||

n | ||

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 21 | |

B |

24 | barred by | 21 |

From the solution string ~b E k ~a ~h E m E d E k ~h ~m h d

we can delete "m" giving:

~b E k ~a ~h E E d E k ~h h d

we can delete "m" giving:

~b E k ~a ~h E E d E k ~h h d

From the solution string ~b E k ~a ~h E E d E k ~h h d

we can delete "h" giving:

~b E k ~a E E d E k d

we can delete "h" giving:

~b E k ~a E E d E k d

Using proposition 21 add E k to the solution string

so the solution string becomes:

~b E k ~a E E d E k d E k

so the solution string becomes:

~b E k ~a E E d E k d E k

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | 24 | |

e | ||

h | ||

k | 24 | |

l | ||

m | ||

n | ||

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 | |

B |

There are no bars |

Using proposition 24 add d ~k to the solution string

so the solution string becomes:

~b E k ~a E E d E k d E k d ~k

so the solution string becomes:

~b E k ~a E E d E k d E k d ~k

The registry is now:

Entity | Appears in | Complement appears in |

a | 3 | |

b | ||

c | ||

d | ||

e | ||

h | ||

k | ||

l | ||

m | ||

n | ||

r | ||

s | ||

t | ||

v | ||

w | ||

z | ||

A | ||

E | 3 | |

B |

There are no bars |

From the solution string ~b E k ~a E E d E k d E k d ~k

we can delete "k" giving:

~b E ~a E E d E d E d

we can delete "k" giving:

~b E ~a E E d E d E d

So we are left with only the retinends,

giving us the desired conclusion of as required

giving us the desired conclusion of as required