:: YELLOW_5 semantic presentation

K88() is set
K19(K88()) is set
1 is set

the U1 of L is set
a is M2( the U1 of L)
a "\/" a is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
a "/\" a is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
c is M2( the U1 of L)

the U1 of L is set
c is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
c is M2( the U1 of L)
a "\/" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a "\/" c is M2( the U1 of L)
b "\/" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
c is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
c "\/" b is M2( the U1 of L)

the U1 of L is set
b is M2( the U1 of L)
a is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
b "/\" b is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
'not' a is M2( the U1 of L)
c is M2( the U1 of L)
'not' c is M2( the U1 of L)
'not' () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "\/" () is M2( the U1 of L)
Top L is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(a "\/" ()) "/\" b is M2( the U1 of L)
(a "/\" b) "\/" (b "/\" ()) is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
L is non empty RelStr
the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
L is non empty RelStr
the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(L,a,b) "\/" (L,b,a) is M2( the U1 of L)

the U1 of L is set
c is M2( the U1 of L)
d is M2( the U1 of L)
(L,c,d) is M2( the U1 of L)
(L,c,d) is M2( the U1 of L)
'not' d is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
(L,d,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
d "/\" () is M2( the U1 of L)
(L,c,d) "\/" (L,d,c) is M2( the U1 of L)
(L,d,c) is M2( the U1 of L)
(L,d,c) "\/" (L,c,d) is M2( the U1 of L)
(L,c,d) "\/" (L,d,c) is M2( the U1 of L)
L is non empty RelStr
the U1 of L is set
L is non empty RelStr
the U1 of L is set
L is non empty antisymmetric with_infima RelStr
the U1 of L is set
L is non empty antisymmetric with_infima RelStr
the U1 of L is set
c is M2( the U1 of L)
d is M2( the U1 of L)
c "/\" d is M2( the U1 of L)
Bottom L is M2( the U1 of L)
d "/\" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
c is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
(L,a,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
b "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
(L,a,b) "\/" (L,b,a) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
a "/\" a is M2( the U1 of L)
a "/\" a is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
(a "/\" b) "\/" (a "/\" c) is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
(b "\/" c) "/\" a is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "\/" (b "/\" c) is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
a "\/" c is M2( the U1 of L)
(a "\/" b) "/\" (a "\/" c) is M2( the U1 of L)
(a "\/" b) "/\" a is M2( the U1 of L)
(a "\/" b) "/\" c is M2( the U1 of L)
((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c) is M2( the U1 of L)
a "\/" ((a "\/" b) "/\" c) is M2( the U1 of L)
c "/\" a is M2( the U1 of L)
c "/\" b is M2( the U1 of L)
(c "/\" a) "\/" (c "/\" b) is M2( the U1 of L)
a "\/" ((c "/\" a) "\/" (c "/\" b)) is M2( the U1 of L)
a "\/" (c "/\" a) is M2( the U1 of L)
(a "\/" (c "/\" a)) "\/" (c "/\" b) is M2( the U1 of L)
a "\/" (c "/\" b) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
c is M2( the U1 of L)
(L,(a "\/" b),c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
(L,a,c) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(L,a,c) "\/" (L,b,c) is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
() "/\" a is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
(() "/\" a) "\/" (() "/\" b) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
(L,(),a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
() "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
a "/\" c is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "/\" (b "/\" c) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(a "/\" b) "/\" c is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
a "/\" (L,b,c) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(a "/\" b) "/\" () is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" () is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
c is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "/\" b is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "/\" (b "/\" c) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(a "/\" b) "/\" c is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" c is M2( the U1 of L)
a "/\" (b "/\" c) is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
(a "/\" c) "/\" b is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" b is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
(a "/\" c) "/\" (b "/\" c) is M2( the U1 of L)
a "/\" (b "/\" c) is M2( the U1 of L)
c "/\" (a "/\" (b "/\" c)) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
c "/\" (a "/\" b) is M2( the U1 of L)
(c "/\" (a "/\" b)) "/\" c is M2( the U1 of L)
Bottom L is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
(c "/\" ()) "/\" c is M2( the U1 of L)
() "/\" c is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
(a "/\" b) "\/" (b "/\" c) is M2( the U1 of L)
c "/\" a is M2( the U1 of L)
((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
(a "\/" b) "/\" (b "\/" c) is M2( the U1 of L)
c "\/" a is M2( the U1 of L)
((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) is M2( the U1 of L)
a "\/" (b "/\" c) is M2( the U1 of L)
b "\/" (b "/\" c) is M2( the U1 of L)
(a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c)) is M2( the U1 of L)
((a "\/" (b "/\" c)) "/\" (b "\/" (b "/\" c))) "\/" (c "/\" a) is M2( the U1 of L)
(a "\/" (b "/\" c)) "/\" b is M2( the U1 of L)
((a "\/" (b "/\" c)) "/\" b) "\/" (c "/\" a) is M2( the U1 of L)
(a "\/" (b "/\" c)) "\/" (c "/\" a) is M2( the U1 of L)
b "\/" (c "/\" a) is M2( the U1 of L)
((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" (b "\/" (c "/\" a)) is M2( the U1 of L)
b "\/" a is M2( the U1 of L)
(b "\/" c) "/\" (b "\/" a) is M2( the U1 of L)
((a "\/" (b "/\" c)) "\/" (c "/\" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)
a "\/" (c "/\" a) is M2( the U1 of L)
(b "/\" c) "\/" (a "\/" (c "/\" a)) is M2( the U1 of L)
((b "/\" c) "\/" (a "\/" (c "/\" a))) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)
(b "/\" c) "\/" a is M2( the U1 of L)
((b "/\" c) "\/" a) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)
(b "\/" a) "/\" (c "\/" a) is M2( the U1 of L)
((b "\/" a) "/\" (c "\/" a)) "/\" ((b "\/" c) "/\" (b "\/" a)) is M2( the U1 of L)
(c "\/" a) "/\" (b "\/" a) is M2( the U1 of L)
((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c) is M2( the U1 of L)
(b "\/" a) "/\" (((c "\/" a) "/\" (b "\/" a)) "/\" (b "\/" c)) is M2( the U1 of L)
(c "\/" a) "/\" (b "\/" c) is M2( the U1 of L)
(b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c)) is M2( the U1 of L)
(b "\/" a) "/\" ((b "\/" a) "/\" ((c "\/" a) "/\" (b "\/" c))) is M2( the U1 of L)
(b "\/" a) "/\" (b "\/" a) is M2( the U1 of L)
((b "\/" a) "/\" (b "\/" a)) "/\" ((c "\/" a) "/\" (b "\/" c)) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
Top L is M2( the U1 of L)
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "\/" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" b is M2( the U1 of L)
c "\/" b is M2( the U1 of L)
b "\/" a is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
(b "\/" a) "/\" (b "\/" ()) is M2( the U1 of L)
Top L is M2( the U1 of L)
(b "\/" a) "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
'not' (a "\/" b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
'not' (a "/\" b) is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
(a "\/" b) "/\" (() "/\" ()) is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
((a "\/" b) "/\" ()) "/\" () is M2( the U1 of L)
() "/\" a is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
(() "/\" a) "\/" (() "/\" b) is M2( the U1 of L)
((() "/\" a) "\/" (() "/\" b)) "/\" () is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (() "/\" b) is M2( the U1 of L)
(() "\/" (() "/\" b)) "/\" () is M2( the U1 of L)
(() "/\" b) "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
() "/\" (b "/\" ()) is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
(a "\/" b) "\/" (() "/\" ()) is M2( the U1 of L)
b "\/" (() "/\" ()) is M2( the U1 of L)
a "\/" (b "\/" (() "/\" ())) is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
(b "\/" ()) "/\" (b "\/" ()) is M2( the U1 of L)
a "\/" ((b "\/" ()) "/\" (b "\/" ())) is M2( the U1 of L)
Top L is M2( the U1 of L)
(b "\/" ()) "/\" (Top L) is M2( the U1 of L)
a "\/" ((b "\/" ()) "/\" (Top L)) is M2( the U1 of L)
a "\/" (b "\/" ()) is M2( the U1 of L)
a "\/" () is M2( the U1 of L)
(a "\/" ()) "\/" b is M2( the U1 of L)
(Top L) "\/" b is M2( the U1 of L)
(a "/\" b) "/\" (() "\/" ()) is M2( the U1 of L)
b "/\" (() "\/" ()) is M2( the U1 of L)
a "/\" (b "/\" (() "\/" ())) is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(b "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
a "/\" ((b "/\" ()) "\/" (b "/\" ())) is M2( the U1 of L)
(b "/\" ()) "\/" () is M2( the U1 of L)
a "/\" ((b "/\" ()) "\/" ()) is M2( the U1 of L)
a "/\" (b "/\" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "/\" b is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
(a "/\" b) "\/" (() "\/" ()) is M2( the U1 of L)
(a "/\" b) "\/" () is M2( the U1 of L)
((a "/\" b) "\/" ()) "\/" () is M2( the U1 of L)
() "\/" a is M2( the U1 of L)
() "\/" b is M2( the U1 of L)
(() "\/" a) "/\" (() "\/" b) is M2( the U1 of L)
((() "\/" a) "/\" (() "\/" b)) "\/" () is M2( the U1 of L)
(Top L) "/\" (() "\/" b) is M2( the U1 of L)
((Top L) "/\" (() "\/" b)) "\/" () is M2( the U1 of L)
(() "\/" b) "\/" () is M2( the U1 of L)
() "\/" (b "\/" ()) is M2( the U1 of L)
() "\/" (Top L) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
b is M2( the U1 of L)
'not' b is M2( the U1 of L)
b "/\" a is M2( the U1 of L)
'not' (b "/\" a) is M2( the U1 of L)
() "\/" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
(L,c,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
(L,c,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
c "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
d is M2( the U1 of L)
(L,a,d) is M2( the U1 of L)
'not' d is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
(L,a,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(b "\/" c) "/\" () is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
() "/\" c is M2( the U1 of L)
(() "/\" b) "\/" (() "/\" c) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (() "/\" c) is M2( the U1 of L)
c "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(b "\/" c) "/\" () is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
() "/\" c is M2( the U1 of L)
(() "/\" b) "\/" (() "/\" c) is M2( the U1 of L)
(() "/\" b) "\/" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
'not' (a "/\" b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
() "\/" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
'not' (a "\/" b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
() "/\" () is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(b "/\" ()) "/\" a is M2( the U1 of L)
() "/\" a is M2( the U1 of L)
b "/\" (() "/\" a) is M2( the U1 of L)
b "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
a "\/" (L,b,a) is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
a "\/" () is M2( the U1 of L)
(a "\/" b) "/\" (a "\/" ()) is M2( the U1 of L)
() "\/" a is M2( the U1 of L)
b "/\" (() "\/" a) is M2( the U1 of L)
Top L is M2( the U1 of L)
b "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "\/" a is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
(b "\/" a) "/\" (b "\/" ()) is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
Top L is M2( the U1 of L)
(a "\/" b) "/\" (Top L) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
c is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
a "/\" (b "\/" c) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(a "/\" b) "\/" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,b) "\/" b is M2( the U1 of L)
b "\/" a is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
(b "\/" a) "/\" (b "\/" ()) is M2( the U1 of L)
Top L is M2( the U1 of L)
(b "\/" a) "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
(L,a,(a "\/" b)) is M2( the U1 of L)
'not' (a "\/" b) is M2( the U1 of L)
a "/\" ('not' (a "\/" b)) is M2( the U1 of L)
'not' a is M2( the U1 of L)
'not' b is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
a "/\" (() "/\" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "/\" () is M2( the U1 of L)
() "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(L,a,(a "/\" b)) is M2( the U1 of L)
'not' (a "/\" b) is M2( the U1 of L)
a "/\" ('not' (a "/\" b)) is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
'not' a is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
a "/\" (() "\/" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (a "/\" ()) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (a "/\" ()) is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,b) "/\" b is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
a "/\" (() "/\" b) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
a "\/" (L,b,a) is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
a "\/" () is M2( the U1 of L)
(a "\/" b) "/\" (a "\/" ()) is M2( the U1 of L)
Top L is M2( the U1 of L)
(a "\/" b) "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" b) "\/" (L,a,b) is M2( the U1 of L)
(a "/\" b) "\/" a is M2( the U1 of L)
(a "/\" b) "\/" () is M2( the U1 of L)
((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" ()) is M2( the U1 of L)
a "/\" ((a "/\" b) "\/" ()) is M2( the U1 of L)
() "\/" a is M2( the U1 of L)
() "\/" b is M2( the U1 of L)
(() "\/" a) "/\" (() "\/" b) is M2( the U1 of L)
a "/\" ((() "\/" a) "/\" (() "\/" b)) is M2( the U1 of L)
Top L is M2( the U1 of L)
(() "\/" a) "/\" (Top L) is M2( the U1 of L)
a "/\" ((() "\/" a) "/\" (Top L)) is M2( the U1 of L)
a "/\" (() "\/" a) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(L,a,(L,b,c)) is M2( the U1 of L)
'not' (L,b,c) is M2( the U1 of L)
a "/\" ('not' (L,b,c)) is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
(L,a,b) "\/" (a "/\" c) is M2( the U1 of L)
'not' () is M2( the U1 of L)
() "\/" ('not' ()) is M2( the U1 of L)
a "/\" (() "\/" ('not' ())) is M2( the U1 of L)
() "\/" c is M2( the U1 of L)
a "/\" (() "\/" c) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,(L,a,b)) is M2( the U1 of L)
'not' (L,a,b) is M2( the U1 of L)
a "/\" ('not' (L,a,b)) is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
'not' a is M2( the U1 of L)
'not' () is M2( the U1 of L)
() "\/" ('not' ()) is M2( the U1 of L)
a "/\" (() "\/" ('not' ())) is M2( the U1 of L)
() "\/" b is M2( the U1 of L)
a "/\" (() "\/" b) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (a "/\" b) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (a "/\" b) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
(L,(a "\/" b),b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
(a "/\" ()) "\/" () is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" a is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
'not' a is M2( the U1 of L)
'not' () is M2( the U1 of L)
() "\/" ('not' ()) is M2( the U1 of L)
() "\/" b is M2( the U1 of L)
a "/\" (() "\/" b) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (a "/\" b) is M2( the U1 of L)
() "\/" (a "/\" b) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
(L,a,(b "\/" c)) is M2( the U1 of L)
'not' (b "\/" c) is M2( the U1 of L)
a "/\" ('not' (b "\/" c)) is M2( the U1 of L)
(L,a,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,b) "/\" (L,a,c) is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
a "/\" (() "/\" ()) is M2( the U1 of L)
a "/\" a is M2( the U1 of L)
(a "/\" a) "/\" (() "/\" ()) is M2( the U1 of L)
(a "/\" a) "/\" () is M2( the U1 of L)
((a "/\" a) "/\" ()) "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
a "/\" (a "/\" ()) is M2( the U1 of L)
(a "/\" (a "/\" ())) "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
b "/\" c is M2( the U1 of L)
(L,a,(b "/\" c)) is M2( the U1 of L)
'not' (b "/\" c) is M2( the U1 of L)
a "/\" ('not' (b "/\" c)) is M2( the U1 of L)
(L,a,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,b) "\/" (L,a,c) is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
a "/\" (() "\/" ()) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
c is M2( the U1 of L)
(L,b,c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
a "/\" (L,b,c) is M2( the U1 of L)
a "/\" c is M2( the U1 of L)
(L,(a "/\" b),(a "/\" c)) is M2( the U1 of L)
'not' (a "/\" c) is M2( the U1 of L)
(a "/\" b) "/\" ('not' (a "/\" c)) is M2( the U1 of L)
'not' a is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
(a "/\" b) "/\" (() "\/" ()) is M2( the U1 of L)
(a "/\" b) "/\" () is M2( the U1 of L)
(a "/\" b) "/\" () is M2( the U1 of L)
((a "/\" b) "/\" ()) "\/" ((a "/\" b) "/\" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "/\" b is M2( the U1 of L)
((a "/\" ()) "/\" b) "\/" ((a "/\" b) "/\" ()) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
(() "/\" b) "\/" ((a "/\" b) "/\" ()) is M2( the U1 of L)
() "\/" ((a "/\" b) "/\" ()) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(L,(a "\/" b),(a "/\" b)) is M2( the U1 of L)
'not' (a "/\" b) is M2( the U1 of L)
(a "\/" b) "/\" ('not' (a "/\" b)) is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,b,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(L,a,b) "\/" (L,b,a) is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
(a "\/" b) "/\" (() "\/" ()) is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
((a "\/" b) "/\" ()) "\/" ((a "\/" b) "/\" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
((a "/\" ()) "\/" (b "/\" ())) "\/" ((a "\/" b) "/\" ()) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "\/" (b "/\" ()) is M2( the U1 of L)
(() "\/" (b "/\" ())) "\/" ((a "\/" b) "/\" ()) is M2( the U1 of L)
(L,b,a) "\/" ((a "\/" b) "/\" ()) is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
(L,b,a) "\/" ((a "/\" ()) "\/" (b "/\" ())) is M2( the U1 of L)
(a "/\" ()) "\/" () is M2( the U1 of L)
(L,b,a) "\/" ((a "/\" ()) "\/" ()) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
c is M2( the U1 of L)
(L,(L,a,b),c) is M2( the U1 of L)
'not' c is M2( the U1 of L)
(L,a,b) "/\" () is M2( the U1 of L)
b "\/" c is M2( the U1 of L)
(L,a,(b "\/" c)) is M2( the U1 of L)
'not' (b "\/" c) is M2( the U1 of L)
a "/\" ('not' (b "\/" c)) is M2( the U1 of L)
() "/\" () is M2( the U1 of L)
a "/\" (() "/\" ()) is M2( the U1 of L)

Bottom L is M2( the U1 of L)
the U1 of L is set
'not' () is M2( the U1 of L)
Top L is M2( the U1 of L)
() "/\" (Top L) is M2( the U1 of L)
() "\/" (Top L) is M2( the U1 of L)

Top L is M2( the U1 of L)
the U1 of L is set
'not' (Top L) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
() "/\" (Top L) is M2( the U1 of L)
() "\/" (Top L) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
(L,a,a) is M2( the U1 of L)
'not' a is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
Bottom L is M2( the U1 of L)

the U1 of L is set
Bottom L is M2( the U1 of L)
a is M2( the U1 of L)
(L,a,()) is M2( the U1 of L)
'not' () is M2( the U1 of L)
a "/\" ('not' ()) is M2( the U1 of L)
Top L is M2( the U1 of L)
a "/\" (Top L) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
'not' a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
'not' (L,a,b) is M2( the U1 of L)
() "\/" b is M2( the U1 of L)
'not' () is M2( the U1 of L)
() "\/" ('not' ()) is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" b) "/\" (L,a,b) is M2( the U1 of L)
(a "/\" b) "/\" () is M2( the U1 of L)
((a "/\" b) "/\" ()) "/\" a is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
a "/\" (b "/\" ()) is M2( the U1 of L)
(a "/\" (b "/\" ())) "/\" a is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(a "/\" ()) "/\" a is M2( the U1 of L)
() "/\" a is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
(L,a,b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
(L,a,b) "/\" b is M2( the U1 of L)
() "/\" b is M2( the U1 of L)
a "/\" (() "/\" b) is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "/\" () is M2( the U1 of L)

the U1 of L is set
a is M2( the U1 of L)
b is M2( the U1 of L)
a "\/" b is M2( the U1 of L)
(L,(a "\/" b),b) is M2( the U1 of L)
'not' b is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
a "/\" b is M2( the U1 of L)
Bottom L is M2( the U1 of L)
a "\/" () is M2( the U1 of L)
b "\/" () is M2( the U1 of L)
(a "\/" ()) "/\" (b "\/" ()) is M2( the U1 of L)
() "\/" () is M2( the U1 of L)
Top L is M2( the U1 of L)
(a "\/" ()) "/\" (Top L) is M2( the U1 of L)
(a "\/" b) "/\" () is M2( the U1 of L)
a "/\" () is M2( the U1 of L)
b "/\" () is M2( the U1 of L)
(a "/\" ()) "\/" (b "/\" ()) is M2( the U1 of L)
(a "/\" ()) "\/" () is M2( the U1 of L)