claim !P:prop.!Q:prop.~(P <-> Q) -> !R:prop.(P -> ~ Q -> R) -> (~ P -> Q -> R) -> R