Time out after 50 steps. "p <-> r, q <-> s => (p -> q) <-> (r -> s)" => conj-intro "(p <-> r) /\\ (q <-> s) => (p -> q) <-> (r -> s)" => logic.propositional.defequiv "((p /\\ r) || (~p /\\ ~r)) /\\ (q <-> s) => (p -> q) <-> (r -> s)" => logic.propositional.defequiv "((p /\\ r) || (~p /\\ ~r)) /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "((p /\\ r) || ~p) /\\ ((p /\\ r) || ~r) /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "(p || ~p) /\\ (r || ~p) /\\ ((p /\\ r) || ~r) /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.complor "T /\\ (r || ~p) /\\ ((p /\\ r) || ~r) /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "T /\\ (r || ~p) /\\ (p || ~r) /\\ (r || ~r) /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.complor "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ ((q /\\ s) || (~q /\\ ~s)) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ ((q /\\ s) || ~q) /\\ ((q /\\ s) || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ (q || ~q) /\\ (s || ~q) /\\ ((q /\\ s) || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.complor "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ T /\\ (s || ~q) /\\ ((q /\\ s) || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.idempand "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ (s || ~q) /\\ ((q /\\ s) || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.oroverand "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ (s || ~q) /\\ (q || ~s) /\\ (s || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.complor "T /\\ (r || ~p) /\\ (p || ~r) /\\ T /\\ (s || ~q) /\\ (q || ~s) /\\ T => (p -> q) <-> (r -> s)" => logic.propositional.truezeroand "(r || ~p) /\\ (p || ~r) /\\ T /\\ (s || ~q) /\\ (q || ~s) /\\ T => (p -> q) <-> (r -> s)" => logic.propositional.truezeroand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) /\\ T => (p -> q) <-> (r -> s)" => logic.propositional.truezeroand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (p -> q) <-> (r -> s)" => logic.propositional.defimpl "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q) <-> (r -> s)" => logic.propositional.defimpl "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q) <-> (~r || s)" => logic.propositional.defequiv "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => ((~p || q) /\\ (~r || s)) || (~(~p || q) /\\ ~(~r || s))" => logic.propositional.demorganor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => ((~p || q) /\\ (~r || s)) || (~~p /\\ ~q /\\ ~(~r || s))" => logic.propositional.notnot "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => ((~p || q) /\\ (~r || s)) || (p /\\ ~q /\\ ~(~r || s))" => logic.propositional.demorganor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => ((~p || q) /\\ (~r || s)) || (p /\\ ~q /\\ ~~r /\\ ~s)" => logic.propositional.notnot "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => ((~p || q) /\\ (~r || s)) || (p /\\ ~q /\\ r /\\ ~s)" => logic.propositional.genoroverand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (((~p || q) /\\ (~r || s)) || p) /\\ (((~p || q) /\\ (~r || s)) || ~q) /\\ (((~p || q) /\\ (~r || s)) || r) /\\ (((~p || q) /\\ (~r || s)) || ~s)" => logic.propositional.oroverand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (((~p || q) /\\ (~r || s)) || ~q) /\\ (((~p || q) /\\ (~r || s)) || r) /\\ (((~p || q) /\\ (~r || s)) || ~s)" => logic.propositional.oroverand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~p || q || ~q) /\\ (~r || s || ~q) /\\ (((~p || q) /\\ (~r || s)) || r) /\\ (((~p || q) /\\ (~r || s)) || ~s)" => logic.propositional.complor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~p || T) /\\ (~r || s || ~q) /\\ (((~p || q) /\\ (~r || s)) || r) /\\ (((~p || q) /\\ (~r || s)) || ~s)" => logic.propositional.oroverand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~p || T) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (((~p || q) /\\ (~r || s)) || ~s)" => logic.propositional.oroverand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~p || T) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s) /\\ (~r || s || ~s)" => logic.propositional.complor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~p || T) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s) /\\ (~r || T)" => logic.propositional.truezeroor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ T /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s) /\\ (~r || T)" => logic.propositional.truezeroand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s) /\\ (~r || T)" => logic.propositional.truezeroor "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s) /\\ T" => logic.propositional.truezeroand "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~p || q || ~s)" => top-is-and.com "(r || ~p) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || p) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (p || ~p || q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.complor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (T || q) /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.truezeroor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => T /\\ (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.truezeroand "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ (~r || s || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ (r || ~r || s) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.complor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ (T || s) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.truezeroor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ T /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => logic.propositional.truezeroand "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ (~r || s || p) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || q || r) /\\ (p || ~r || s) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || q || r) /\\ (p || ~r || s) /\\ (~r || s || ~q) /\\ (~p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || q || r) /\\ (p || ~r || s) /\\ (~q || ~r || s) /\\ (~p || q || ~s)" => introfalseleft "(F || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || q || r) /\\ (p || ~r || s) /\\ (~q || ~r || s) /\\ (~p || q || ~s)" => introcompl "((q /\\ ~q) || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || q || r) /\\ (p || ~r || s) /\\ (~q || ~r || s) /\\ (~p || q || ~s)"