% These problems seem to contain some errors.
% In particular, 4.13, 4.2, 4.24, and 4.25 are missing.

r([4,1,0],((p => q) <==> ( ~q =>  ~p))).
r([4,1,1],((p <==> q) <==> ( ~p <==>  ~q))).
r([4,1,2],((p <==>  ~q) <==> (q <==>  ~p))).
r([4,1,4],(((p and q) => r) <==> ((p and  ~r) =>  ~q))).
r([4,1,5],(((p and q) =>  ~r) <==> ((q and r) =>  ~p))).
r([4,2,1],((p <==> q) <==> (q <==> p))).
r([4,2,2],(((p <==> q) and (q <==> r)) => (p <==> r))).
r([4,3,0],((p and q) <==> (q and p))).
r([4,3,1],((p or q) <==> (q or p))).
r([4,3,2],(((p and q) and r) <==> (p and (q and r)))).
r([4,3,3],(((p or q) or r) <==> (p or (q or r)))).
r([4,3,6],((p <==> q) => ((p and r) <==> (q and r)))).
r([4,3,7],((p <==> q) => ((p or r) <==> (q or r)))).
r([4,3,8],(((p <==> r) and (q <==> s)) => ((p and q) <==> (r and s)))).
r([4,3,9],(((p <==> r) and (q <==> s)) => ((p or q) <==> (r or s)))).
r([4,4,0],((p and (q or r)) <==> ((p and q) or (p and r)))).
r([4,4,1],((p or (q and r)) <==> ((p or q) and (p or r)))).
r([4,4,2],(p <==> ((p and q) or (p and  ~q)))).
r([4,4,3],(p <==> ((p or q) and (p or  ~q)))).
r([4,4,4],(p <==> (p or (p and q)))).
r([4,4,5],(p <==> (p and (p or q)))).
r([4,5,0],((p and q) <==>  ~( ~p or  ~q))).
r([4,5,1],( ~(p and q) <==> ( ~p or  ~q))).
r([4,5,2],((p and  ~q) <==>  ~( ~p or q))).
r([4,5,3],( ~(p and  ~q) <==>  (~p or q))).
r([4,5,4],(( ~p and q) <==>  ~(p or  ~q))).
r([4,5,5],( ~( ~p and q) <==> (p or  ~q))).
r([4,5,6],(( ~p and  ~q) <==>  ~(p or q))).
r([4,5,7],( ~( ~p and  ~q) <==> (p or q))).
r([4,6,0],((p => q) <==> ( ~p or q))).
r([4,6,1],( ~(p => q) <==> (p and  ~q))).
r([4,6,2],((p =>  ~q) <==> ( ~p or  ~q))).
r([4,6,3],( ~(p =>  ~q) <==> (p and q))).
r([4,6,4],(( ~p => q) <==> (p or q))).
r([4,6,5],( ~( ~p => q) <==> ( ~p and  ~q))).
r([4,6,6],( ~p => ~q) <==> (p or  ~q)).
r([4,6,7],( ~( ~p =>  ~q) <==> ( ~p and q))).
r([4,7,0],((p => q) <==> (p => (p and q)))).
r([4,7,1],((p => q) <==> (p <==> (p and q)))).
r([4,7,2],((p => q) <==> (q <==> (p or q)))).
r([4,7,3],(q => (p <==> (p and q)))).
r([4,7,4],( ~p => (q <==> (p or q)))).
r([4,7,6],(((p => q) and (p => r)) <==> (p => (q and r)))).
r([4,7,7],(((q => p) and (r => p)) <==> ((q or r) => p))).
r([4,7,8],(((p => q) or (p => r)) <==> (p => (q or r)))).
r([4,7,9],(((q => p) or (r => p)) <==> ((q and r) => p))).
r([4,8,0],((p =>  ~p) <==>  ~p)).
r([4,8,1],(( ~p => p) <==> p)).
r([4,8,2],(((p => q) and (p =>  ~q)) <==>  ~p)).
r([4,8,3],(((p => q) and ( ~p => q)) <==> q)).
r([4,8,4],((p <==> q) => ((p => r) <==> (q => r)))).
r([4,8,5],((p <==> q) => ((r => p) <==> (r => q)))).
r([4,8,6],((p <==> q) => ((p <==> r) <==> (q <==> r)))).
r([5,3,0],(((p and q) => r) <==> ((p and q) => (p and r)))).
r([5,3,1],(((r and (p => q)) => (p => (q and r))))). /* corrected by Pfahring 11-25-88 */
r([5,3,2],((p => (q <==> r)) <==> ((p and q) <==> (p and r)))).
r([5,3,3],((p and (q => r)) <==> (p and ((p and q) => r)))).
r([5,3,5],(((p => q) and (p => r)) => (p => (q <==> r)))).
r([5,3,6],((p and (p <==> q)) <==> (q and (p <==> q)))).
r([5,4,0],((p => (p => q)) <==> (p => q))).
r([5,4,1],(((p => q) => (p => r)) <==> (p => (q => r)))).
r([5,4,2],((p => (q => r)) <==> (p => (q => (p and r))))).
r([5,4,4],((p => q) => ((p => r) <==> (p => (q and r))))).
r([5,5,0],(p => ((p => q) <==> q))).
r([5,5,0,1],(p => (q <==> (p <==> q)))).
r([5,5,3],((((p or q) or r) => s) <==> (((p => s) and (q => s)) and (r => s)))).
r([5,5,4],(((p and q) <==> p) or ((p and q) <==> q))).
r([5,5,5],(((p or q) <==> p) or ((p or q) <==> q))).
r([5,6,0],(((p and  ~q) => r) <==> (p => (q or r)))).
r([5,6,1],(((p or q) and  ~q) <==> (p and  ~q))).
r([5,6,2],(((p and q) or  ~q) <==> (p or  ~q))).
r([5,6,3],((p or q) <==> (p or ( ~p and q)))).
r([5,7,0],(((p or r) <==> (q or r)) <==> (r or (p <==> q)))).
r([5,7,1],((q =>  ~r) => (((p or q) and r) <==> (p and r)))).
r([5,7,4],((p => (q <==> r)) <==> ((p => q) <==> (p => r)))).
r([5,7,5],(((r =>  ~q) and (p <==> (q or r))) => ((p and  ~q) <==> r))).

4-14-89		Bernard Pfahring reported an error in 2.86.

4.13 p = ~~p is missing!
4.2  p = p is also missing!
4.24 
4.25 are also missing!