When exploring starting with A, B, the best proofs discovered are not the atomic ones, but composite ones such as a double constant, with type $A \to B \to B \to A$. This is correct, but ideally should be avoided.
This can be avoided by giving a greater weight to absolute entropy of the statement, for example using $p / q (log(q))^2$.