assume [P,R,A,B] : (line(P) & plane(R) & point(A) & point(B) & ninc_l_pl(P,R) & inc_po_l(A,P) & inc_po_pl(A,R) & inc_po_l(B,P) & inc_po_pl(B,R))
%goal (A = B)
infer (A = B)
%lookup goal

