[traths@jk-005 strip]$ strip-i686-linux-static
STRIP> define(p | (#q & r) -> (p | #q) & (p | r))
STRIP> solve
provable:  => ((p|(~q&r))->((p|~q)&(p|r)))
STRIP> define((p -> q) <-> (q |  #p) & (# q | p))
STRIP> solve
unprovable:  => (((p->q)->((q|~p)&(~q|p)))&(((q|~p)&(~q|p))->(p->q)))
STRIP> quit

[traths@jk-005 strip]$