This rule is used to introduce an OR formula into a proof by using an existing formula in the proof as one side of the OR formula and a formula the user enters for the other side. (the user must enter a formula that uses only relation symbols, function symbols or constants that are in the signature), or when used backwards to extract a sub formula of an OR formula to use as a goal.
To use it forwards:

1. select an empty line and click on Or Introduction.
2. then select the line containing the formula you wish to use as one side of the OR formula (this line must be in scope of the empty line).
3. you will be asked which side of the OR statement you want the selected formula to appear on (enter "l" for left or "r" for right).
4. next enter the formula you wish to appear on the other side of the OR formula. This formula must only contain relation symbols, function symbols or constants in the signature of the empty line.
5. the OR formula will be added as a new line to your proof

1. select the goal line in your proof or box (this line must be an OR formula) and click on Or Introduction.
2. when prompted enter the side of the formula you wish to extract as your new goal by entering "l" for left or "r" for right.
3. the sub formula will appear as a new goal line