Time out after 50 steps. "(\172(q \8594 p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s))) \8743 (\172(q \8594 p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.idempand "(\172(q \8594 p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.defimpl "(\172(\172q \8744 p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.demorganor "((\172\172q \8743 \172p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.notnot "((q \8743 \172p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(q \8594 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.defimpl "((q \8743 \172p) \8596 ((r \8596 s) \8744 \172s)) \8743 (\172(\172q \8744 p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.demorganor "((q \8743 \172p) \8596 ((r \8596 s) \8744 \172s)) \8743 ((\172\172q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.notnot "((q \8743 \172p) \8596 ((r \8596 s) \8744 \172s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.defequiv "((q \8743 \172p) \8596 ((r \8743 s) \8744 (\172r \8743 \172s) \8744 \172s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.absorpor "((q \8743 \172p) \8596 ((r \8743 s) \8744 \172s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.oroverand "((q \8743 \172p) \8596 ((r \8744 \172s) \8743 (s \8744 \172s))) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.complor "((q \8743 \172p) \8596 ((r \8744 \172s) \8743 T)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.truezeroand "((q \8743 \172p) \8596 (r \8744 \172s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.defequiv "((q \8743 \172p \8743 (r \8744 \172s)) \8744 (\172(q \8743 \172p) \8743 \172(r \8744 \172s))) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.demorganand "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 \172\172p) \8743 \172(r \8744 \172s))) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172(r \8744 \172s))) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.demorganor "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 \172\172s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8596 s)))" => logic.propositional.defequiv "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p) \8596 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s)))" => logic.propositional.defequiv "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 (\172(q \8743 \172p) \8743 \172(\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))))" => logic.propositional.demorganand "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 \172\172p) \8743 \172(\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 \172(\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))))" => logic.propositional.gendemorganor "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 \172\172s \8743 \172(r \8743 s) \8743 \172(\172r \8743 \172s)))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 \172(r \8743 s) \8743 \172(\172r \8743 \172s)))" => logic.propositional.demorganand "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 \172(r \8743 s) \8743 (\172\172r \8744 \172\172s)))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 \172(r \8743 s) \8743 (r \8744 \172\172s)))" => logic.propositional.notnot "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 \172(r \8743 s) \8743 (r \8744 s)))" => logic.propositional.demorganand "((q \8743 \172p \8743 (r \8744 \172s)) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 (\172r \8744 \172s) \8743 (r \8744 s)))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 ((\172q \8744 p) \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 (\172r \8744 \172s) \8743 (r \8744 s)))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 (\172r \8744 \172s) \8743 (r \8744 s)))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 (((\172r \8744 \172s) \8743 r) \8744 ((\172r \8744 \172s) \8743 s))))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 ((\172r \8743 r) \8744 (\172s \8743 r) \8744 ((\172r \8744 \172s) \8743 s))))" => logic.propositional.compland "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 (F \8744 (\172s \8743 r) \8744 ((\172r \8744 \172s) \8743 s))))" => logic.propositional.falsezeroor "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 ((\172s \8743 r) \8744 ((\172r \8744 \172s) \8743 s))))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 ((\172s \8743 r) \8744 (\172r \8743 s) \8744 (\172s \8743 s))))" => logic.propositional.compland "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 ((\172s \8743 r) \8744 (\172r \8743 s) \8744 F)))" => logic.propositional.falsezeroor "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 ((\172s \8743 r) \8744 (\172r \8743 s))))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 ((s \8743 \172s \8743 r) \8744 (s \8743 \172r \8743 s))))" => logic.propositional.compland "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 ((F \8743 r) \8744 (s \8743 \172r \8743 s))))" => logic.propositional.falsezeroand "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 (F \8744 (s \8743 \172r \8743 s))))" => logic.propositional.falsezeroor "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 ((\172q \8744 p) \8743 s \8743 \172r \8743 s))" => logic.propositional.andoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 (\172s \8744 (r \8743 s) \8744 (\172r \8743 \172s))) \8744 (\172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 s \8743 \172r \8743 s))" => logic.propositional.genandoveror "((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 ((q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 s \8743 \172r \8743 s))" => logic.propositional.genandoveror "(((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.genandoveror "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.genandoveror "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.genandoveror "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.genandoveror "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (((q \8743 \172p \8743 r) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s)) \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.genandoveror "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 r \8743 p \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 p \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.idempand "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 r \8743 p \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 p \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s)" => logic.propositional.absorpor "(q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 r \8743 s) \8744 (q \8743 \172p \8743 r \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 \172s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (\172q \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (p \8743 \172r \8743 s \8743 q \8743 \172p \8743 \172r \8743 \172s) \8744 (q \8743 \172p \8743 r \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 \172q \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 r \8743 p \8743 s \8743 \172r \8743 s) \8744 (q \8743 \172p \8743 \172s \8743 p \8743 s \8743 \172r \8743 s) \8744 (\172q \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s) \8744 (p \8743 \172r \8743 s \8743 p \8743 s \8743 \172r \8743 s)"