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