[traths@jk-005 IPTP]$ less formula1
p | (~ q & r) -> (p | ~ q) & (p | r)
[traths@jk-005 IPTP]$ ./iptp -p 2 -f formula1
search result = provable
search time = 0e-3

[traths@jk-005 IPTP]$ less formula2
(p -> q) -> (q |  ~ p) & (~ q | p)
[traths@jk-005 iptp]$ ./iptp -p 2 -f formula2
search result = unprovable
search time = 0e-3

[traths@jk-005 IPTP]$