(
p -> [U]p)
<U>
<U>
(p -> [U]p)
((<U>p1 
<U>p2 <U>p3) -> (<U>(p1 p2) 
<U>(p1 p3) <U>(p2 p3)))
(p -> [U]p)
(p -> [U]p)
((<U>p p) -> p)
((p p) -> [U]p)
((<U>p p) -> [U]p)
([U]p -> p)
([U](p -> p) -> p)
((p <-> q) <-> p)
(p <-> ((( (p q r)) -> ((p -> q) (q -> p) r)) -> (p ((p -> r) (q -> r) (p -> q)))))
((p -> p) (p -> p))
(((ci p) -> <U>(ci p)) ((ci p) -> ci))
(([U]p -> p) -> [U]p)
([1][2]-1p -> [3]p)
(((
p q) (p <-> q)) -> (p q))
((( p) -> p) -> p)
(p -> p)
((p -> p) (p -> p))
((p q) -> (p q))
(((p q r) (p q r) (p r q) (p q r) (q r p) (q p r) (r p q) (p q r)) -> )
(((p r) q) p)
(p q)
(((p -> q) p) -> q)
(p -> p)
(p -> p)
(p -> p)
((p -> p) -> p)
((p -> q) (q -> p))
((p <-> q) -> p)
((p p q) (p p q) p)
(((p q) q) -> (p q))
((p -> q) (p -> p))
((p p) -> q)
(p -> p)
(p -> p)
((p q) -> (p -> q))
(((p q) (p q)) -> (p q))
(((p q) -> (p -> q)) (((p q) (p q)) -> (p q)))
((p p q) (p p q))