(#@p -> @#p)
(@#p -> #@p)
((#@p -> @#p) & (#p -> ##p))
((#@p -> @#p) | (#p -> @p))
(#(#p -> p) -> #p)
(c -> ~ @c)
(#@(p & q) | #@~ p | #@~ q)
(##p -> @p)
(##p -> #p)
(#p -> ##p)
(@p -> #@p)
(@(q & ~ p) | #~ q | p)
(~ @p2 | @@~ (p1 | ~ p2) | @@p1)
(p -> [U]p)
((<U>p1 & <U>p2 & <U>p3) -> (<U>(p1 & p2) | <U>(p1 & p3) | <U>(p2 & p3)))
(T -> C(1, 1))
((0 != p) -> C(p, 1))
((0 != p) -> C(p, p))
(C(p, q) -> C(q, p))
(C(p, q) -> (C(p, r) | C(-r, q)))
(((0 != p) & (0 != -p)) -> C(p, -p))
(((0 == (p * q)) & (1 == (p + q))) -> (C(p, p) | C(q, q)))
((0 != (p * -q)) -> (C(p, -q) | C(q, -q)))
KD45: ((#((##0 & #(p | q | r)) -> (@(p -> q) | (q -> p) | r)) -> (@p & #(@(p -> r) & #(q -> r) & (p -> q)))) -> #p)
(#p -> [U]p)
<U>#0
<U>@1
[3](~ [1]p, ~ [2](~ p, q), <1>[1]q)
[2](~ [1](~ [1]p | p), ([1]0 & p))
(@((p -> q), r) -> (@(p, r) -> @(q, r)))
(@(p, (q -> r)) -> (@(p, q) -> @(p, r)))
(@(p, (q -> r)) -> (@(p, q) -> @(q, r)))
(#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)
((@(ci & p) -> <U>(ci & p)) & (@(ci & p) -> @ci))
(#([U]p -> p) -> [U]p)
([1][2]-1p -> [3]p)
((@#(~ p | ~ q) & @#(p <-> q)) -> #@(~ p & ~ q))
(#((##0 & #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)) -> 0 )
~ (#((p & ~ r) | q) | ~ p)
(#p & #q)
((#(@p -> #q) & p) -> @##q)
(#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))