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.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.demorganor "(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) /\\ (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (p || q || ~p) /\\ (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (p || ~p || q) /\\ (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.complor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (T || q) /\\ (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.truezeroor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => T /\\ (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.truezeroand "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (r || s || ~p) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || r || s) /\\ (r || s || ~r) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || r || s) /\\ (r || ~r || s) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.complor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || r || s) /\\ (T || s) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.truezeroor "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || r || s) /\\ T /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => logic.propositional.truezeroand "(~p || r) /\\ (p || ~r) /\\ (s || ~q) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (r || s || ~q) /\\ (p || q || ~s)" => commor.sort "(~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => introfalseleft "(F || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => introcompl "((s /\\ ~s) || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => logic.propositional.oroverand "(s || ~p || r) /\\ (~s || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => commor.sort "(~p || r || s) /\\ (~s || ~p || r) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => commor.sort "(~p || r || s) /\\ (~p || r || ~s) /\\ (p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)" => introfalseleft "(~p || r || s) /\\ (~p || r || ~s) /\\ (F || p || ~r) /\\ (~q || s) /\\ (q || ~s) => (~p || r || s) /\\ (p || q || ~r) /\\ (~q || r || s) /\\ (p || q || ~s)"