Fixed a bug where backward inference is sometimes not applied for an axiom that has multiple literals in the RHS. Added a sophisticated graph visualization module.