Time out after 50 steps. "p /\\ ((~~T /\\ ~F /\\ ~q) || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ T /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ((~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T) || (p /\\ ~q /\\ T /\\ ~~T /\\ ~F /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.truezeroand "p /\\ ((~~T /\\ ~F /\\ ~q) || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ((~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T) || (p /\\ ~q /\\ T /\\ ~~T /\\ ~F /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.absorpor "p /\\ ~~T /\\ ~F /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ((~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T) || (p /\\ ~q /\\ T /\\ ~~T /\\ ~F /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.absorpor "p /\\ ~~T /\\ ~F /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ T /\\ ~~~~(p /\\ ~q)" => logic.propositional.truezeroand "p /\\ ~~T /\\ ~F /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.idempand "p /\\ ~~T /\\ ~F /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.notfalse "p /\\ ~~T /\\ T /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.truezeroand "p /\\ ~~T /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ ~F)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.notfalse "p /\\ ~~T /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.notnot "p /\\ T /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.truezeroand "p /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ ~~~~(p /\\ ~q)" => logic.propositional.notnot "p /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ ~~(p /\\ ~q)" => logic.propositional.notnot "p /\\ ~q /\\ ((T /\\ p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ ((p /\\ T) || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ (p || (~~T /\\ p /\\ T /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ (p || (~~T /\\ p /\\ ~F /\\ ~(q || q) /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ (p || (~~T /\\ p /\\ ~F /\\ ~(q || q) /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.idempor "p /\\ ~q /\\ (p || (~~T /\\ p /\\ ~F /\\ ~q /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.idempand "p /\\ ~q /\\ (p || (~~T /\\ p /\\ ~F /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notfalse "p /\\ ~q /\\ (p || (~~T /\\ p /\\ T /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ (p || (~~T /\\ p /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notnot "p /\\ ~q /\\ (p || (T /\\ p /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ (p || (p /\\ ~q)) /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.absorpor "p /\\ ~q /\\ p /\\ (q || (~~T /\\ ~F /\\ ~q /\\ T /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~~T /\\ ~F /\\ ~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notfalse "p /\\ ~q /\\ p /\\ (q || (~~T /\\ T /\\ ~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~~T /\\ ~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notnot "p /\\ ~q /\\ p /\\ (q || (T /\\ ~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ T /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~F /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notfalse "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q /\\ ~F) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notfalse "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q /\\ T) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~~T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notnot "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((T /\\ ~q /\\ ~~(p /\\ ~q) /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ ~~(p /\\ ~q) /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.notnot "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ ~q /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.idempand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q) /\\ T)) /\\ p /\\ ~q" => logic.propositional.truezeroand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ q) || (~r /\\ ~~(p /\\ ~q))) /\\ p /\\ ~q" => logic.propositional.notnot "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ q) || (~r /\\ p /\\ ~q)) /\\ p /\\ ~q" => logic.propositional.andoveror "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ q /\\ p /\\ ~q) || (~r /\\ p /\\ ~q /\\ p /\\ ~q))" => logic.propositional.idempand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ((~q /\\ p /\\ q /\\ p /\\ ~q) || (~r /\\ p /\\ ~q))" => logic.propositional.andoveror "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ((~q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || (~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.idempand "p /\\ ~q /\\ p /\\ (q || (~q /\\ p /\\ ~q)) /\\ ((~q /\\ p /\\ q /\\ p /\\ ~q) || (~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.andoveror "p /\\ ~q /\\ p /\\ (((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.andoveror "p /\\ ~q /\\ p /\\ ((q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || (~q /\\ p /\\ ~q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.compland "p /\\ ~q /\\ p /\\ ((F /\\ p /\\ q /\\ p /\\ ~q) || (~q /\\ p /\\ ~q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.falsezeroand "p /\\ ~q /\\ p /\\ (F || (~q /\\ p /\\ ~q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.falsezeroor "p /\\ ~q /\\ p /\\ ((~q /\\ p /\\ ~q /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))" => logic.propositional.idempand "p /\\ ~q /\\ p /\\ ((~q /\\ p /\\ ~q /\\ p /\\ q /\\ p /\\ ~q) || ((q || (~q /\\ p /\\ ~q)) /\\ ~q /\\ ~r /\\ p /\\ ~q))"