prop automatically applies all propositional logic rules for propositional operators ¬,∧,∨,→,↔ unfolding them as usual. If this yields too many branches, Undo and exercise more search control to reduce branching.