Visit the Confluence checker for Conditional term rewrite systems (ConCon).
Visit the Knuth-Bendix Completion Visualizer (KBCV).