\[u2200] A ^ \[u2203] P ^ \[u2200] B ^ [ B \[u2208] P \[u21d4] \[u2200] C ^ ( C \[u2208] B \[u21d2] C \[u2208] A ) ]