claim !P:(set set set set) prop.!Q:(set set set set) prop.(?R:set set set set.P R & Q R) -> !R:prop.(!P2:set set set set.P P2 -> Q P2 -> R) -> R