(* Pruebas del proyecto final *)
prueba(InRuUno(lr([],[impl(impl(lp("p"),lp("q")),impl(nega(lp("q")),nega(lp("p"))))])));
prueba(InRuUno(lr([],[impl(impl(impl(lp("p"),lp("q")),lp("r")),impl(lp("p"),impl(lp("q"),lp("r"))))])));
prueba(InRuUno(lr([],[impl(impl(lp("p"),impl(lp("q"),lp("r"))),impl(impl(lp("p"),lp("q")),lp("r")))])));
prueba(InRuUno(lr([conj(lp("p"),nega(lp("q"))),impl(lp("p"),lp("q")),impl(lp("t"),lp("r")),conj(lp("p"),lp("s"))],[lp("t")])));
prueba(InRuUno(lr([conj(lp("p"),nega(lp("q"))),impl(lp("p"),lp("q"))],[lp("t")])));
prueba(InRuUno(lr([],[impl(impl(nega(lp("p")),lp("q")),impl(nega(lp("r")),lp("s")))])));
prueba(InRuUno(lr([],[impl(lp("p"),lp("p"))])));
prueba(InRuUno(lr([],[conj(nega(lp("p")),lp("p"))])));
prueba(InRuUno(lr([],[disy(nega(lp("p")),lp("p"))])));
prueba(InRuUno(lr([impl(lp("a"),disy(lp("a"),lp("b")))],[impl(lp("b"),disy(lp("a"),lp("b")))])));
prueba(InRuUno(lr([impl(conj(lp("a"),lp("b")),lp("a"))],[impl(conj(lp("a"),lp("b")),lp("b"))])));