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 numberCarroll's numberSymbolic form of premiss
11~s ~r
22~m h d
33*E ~a
44l n ~v
55z m c
66t ~A
77~s ~n c r
88z v ~m
99E ~w
1010v k m ~t
1111*E ~s
1212A B
1313k ~h ~n
1414r ~c
1515~v ~a ~h ~l
1616w ~t s ~n
1717*d ~e
1818s n ~b ~B
1919w e ~z
2020~t ~A ~r ~c n
213**E k
2211**E ~c
2311***E n
2417**d ~k
The registry is now:
EntityAppears inComplement appears in
a3 15
b18
c5 7 14 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 18 20 23 7 13 16
r7 14 1 20
s16 18 1 7 11
t6 10 16 20
v8 10 4 15
w16 19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12 18
and the barred premises are as follows:
12 barred by6 20
6 barred by10 16 20
19 barred by5 8
9 barred by16 19
2 barred by13 15
24 barred by10 13 21
Using proposition 1 add ~s ~r to the solution string
so the solution string becomes:
~s ~r
The registry is now:
EntityAppears inComplement appears in
a3 15
b18
c5 7 14 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 18 20 23 7 13 16
r7 14 20
s16 18 7 11
t6 10 16 20
v8 10 4 15
w16 19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12 18
and the barred premises are as follows:
12 barred by6 20
6 barred by10 16 20
20 barred by7 14
19 barred by5 8
9 barred by16 19
2 barred by13 15
24 barred by10 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
The registry is now:
EntityAppears inComplement appears in
a3 15
b18
c5 14 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 18 20 23 13 16
r14 20
s16 18 11
t6 10 16 20
v8 10 4 15
w16 19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12 18
and the barred premises are as follows:
12 barred by6 20
5 barred by14 20 22
20 barred by14
2 barred by13 15
11 barred by16 18
24 barred by10 13 21
6 barred by10 16 20
19 barred by5 8
9 barred by16 19
From the solution string ~s ~r ~s ~n c r
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
The registry is now:
EntityAppears inComplement appears in
a3 15
b18
c5 14 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 18 20 23 13
r14 20
s18 11
t6 10 20
v8 10 4 15
w19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12 18
and the barred premises are as follows:
12 barred by6 20
5 barred by14 20 22
20 barred by14
2 barred by13 15
11 barred by18
24 barred by10 13 21
13 barred by4 18 20 23
6 barred by10 20
19 barred by5 8
9 barred by19
From the solution string ~s ~s ~n c w ~t s ~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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 14 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 20 23 13
r14 20
s11
t6 10 20
v8 10 4 15
w19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12
and the barred premises are as follows:
12 barred by6 20
5 barred by14 20 22
20 barred by14
2 barred by13 15
24 barred by10 13 21
13 barred by4 20 23
6 barred by10 20
19 barred by5 8
9 barred by19
From the solution string ~n c w ~t ~n s n ~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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 20 23 13
r20
s11
t6 10 20
v8 10 4 15
w19 9
z5 8 19
A12 6 20
E3 9 11 21 22 23
B12
and the barred premises are as follows:
12 barred by6 20
5 barred by20 22
2 barred by13 15
24 barred by10 13 21
13 barred by4 20 23
6 barred by10 20
19 barred by5 8
9 barred by19
From the solution string c w ~t s ~b ~B r ~c
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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 20 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 20 23 13
r20
s
t6 10 20
v8 10 4 15
w19 9
z5 8 19
A12 6 20
E3 9 21 22 23
B12
and the barred premises are as follows:
12 barred by6 20
5 barred by20 22
2 barred by13 15
24 barred by10 13 21
13 barred by4 20 23
6 barred by10 20
19 barred by5 8
9 barred by19
From the solution string w ~t s ~b ~B r E ~s
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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 22
d2 17 24
e19 17
h2 13 15
k10 13 21 24
l4 15
m5 10 2 8
n4 23 13
r
s
t6 10
v8 10 4 15
w19 9
z5 8 19
A12 6
E3 9 21 22 23
B12
and the barred premises are as follows:
12 barred by6
5 barred by22
2 barred by13 15
24 barred by10 13 21
13 barred by4 23
6 barred by10
19 barred by5 8
9 barred by19
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

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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 22
d2 17 24
e19 17
h2 13 15
k13 21 24
l4 15
m5 2 8
n4 23 13
r
s
t6
v8 4 15
w19 9
z5 8 19
A12 6
E3 9 21 22 23
B12
and the barred premises are as follows:
12 barred by6
5 barred by22
2 barred by13 15
24 barred by13 21
13 barred by4 23
19 barred by5 8
9 barred by19
8 barred by4 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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 22
d2 17 24
e19 17
h2 13 15
k13 21 24
l4 15
m5 2 8
n4 23 13
r
s
t
v8 4 15
w19 9
z5 8 19
A12
E3 9 21 22 23
B12
and the barred premises are as follows:
5 barred by22
2 barred by13 15
24 barred by13 21
13 barred by4 23
19 barred by5 8
9 barred by19
8 barred by4 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

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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 22
d2 17 24
e19 17
h2 13 15
k13 21 24
l15
m5 2 8
n23 13
r
s
t
v8 15
w19 9
z5 8 19
A12
E3 9 21 22 23
B12
and the barred premises are as follows:
5 barred by22
2 barred by13 15
24 barred by13 21
13 barred by23
19 barred by5 8
9 barred by19
8 barred by15
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

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
The registry is now:
EntityAppears inComplement appears in
a3 15
b
c5 22
d2 17 24
e19 17
h2 13 15
k13 21 24
l15
m5 2 8
n23 13
r
s
t
v8 15
w19 9
z5 8 19
A
E3 9 21 22 23
B
and the barred premises are as follows:
5 barred by22
2 barred by13 15
24 barred by13 21
13 barred by23
19 barred by5 8
9 barred by19
8 barred by15
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
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c5 22
d2 17 24
e19 17
h2 13
k13 21 24
l
m5 2 8
n23 13
r
s
t
v8
w19 9
z5 8 19
A
E3 9 21 22 23
B
and the barred premises are as follows:
5 barred by22
2 barred by13
24 barred by13 21
13 barred by23
19 barred by5 8
9 barred by19
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c5 22
d2 17 24
e19 17
h2 13
k13 21 24
l
m5 2
n23 13
r
s
t
v
w19 9
z5 19
A
E3 9 21 22 23
B
and the barred premises are as follows:
5 barred by22
2 barred by13
24 barred by13 21
13 barred by23
19 barred by5
9 barred by19
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
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c5
d2 17 24
e19 17
h2 13
k13 21 24
l
m5 2
n23 13
r
s
t
v
w19 9
z5 19
A
E3 9 21 23
B
and the barred premises are as follows:
2 barred by13
24 barred by13 21
13 barred by23
19 barred by5
9 barred by19

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 17 24
e19 17
h2 13
k13 21 24
l
m2
n23 13
r
s
t
v
w19 9
z19
A
E3 9 21 23
B
and the barred premises are as follows:
2 barred by13
24 barred by13 21
13 barred by23
9 barred by19
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 17 24
e17
h2 13
k13 21 24
l
m2
n23 13
r
s
t
v
w9
z
A
E3 9 21 23
B
and the barred premises are as follows:
2 barred by13
24 barred by13 21
13 barred by23
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 17 24
e17
h2 13
k13 21 24
l
m2
n23 13
r
s
t
v
w
z
A
E3 21 23
B
and the barred premises are as follows:
2 barred by13
24 barred by13 21
13 barred by23
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 24
e
h2 13
k13 21 24
l
m2
n23 13
r
s
t
v
w
z
A
E3 21 23
B
and the barred premises are as follows:
2 barred by13
24 barred by13 21
13 barred by23
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 24
e
h2 13
k13 21 24
l
m2
n13
r
s
t
v
w
z
A
E3 21
B
and the barred premises are as follows:
2 barred by13
24 barred by13 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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d2 24
e
h2
k21 24
l
m2
n
r
s
t
v
w
z
A
E3 21
B
and the barred premises are as follows:
24 barred by21
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d24
e
h
k21 24
l
m
n
r
s
t
v
w
z
A
E3 21
B
and the barred premises are as follows:
24 barred by21
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
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

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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d24
e
h
k24
l
m
n
r
s
t
v
w
z
A
E3
B
and the barred premises are as follows:
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
The registry is now:
EntityAppears inComplement appears in
a3
b
c
d
e
h
k
l
m
n
r
s
t
v
w
z
A
E3
B
and the barred premises are as follows:
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
So we are left with only the retinends,
giving us the desired conclusion of Ea'b'd0 as required