Enter an NJ proof and I'll tell you some things about it!

Input proof:

Output proof:

• You can input connectives by using the symbols below or their ASCII approximations as shown:

  Connective	Write (click to copy symbol to your clipboard):
  Negation	¬ or ~
  Conjunction	∧ or /\
  Disjunction	∨ or \/
  Implication	→ or ->
  Falsum	⊥ or _|_

• For rule labels, use the connective plus I for introductions or E for eliminations. For disjunction introductions and conjunction eliminations, you should add in addition an L or R as appropriate. For example, you might write ∧I or ∧EL.
• For discharging rules (that's →I, ¬I, and ∨E), add a numeral to the end of the rule name as a discharge marker. For example, you might use →I5 or ∨E23.
• To discharge an assumption, surround it with [ and ], and put the appropriate discharge numeral immediately after that. For example, you might write [p -> q]3 to discharge the assumption p -> q with the label 3.
• Press Enter to create a new sibling node.
• Press Ctrl-Enter to create a new parent node.
• Press Ctrl-Shift-Enter to create a new child node.
• Cycle nodes with Tab and Shift-Tab.
• Undo and Redo changes with Ctrl-Z and Ctrl-Shift-Z.
• Delete subtrees with Ctrl-Backspace.
• Cut, Copy, and Paste subtrees with Shift-Ctrl-X, Shift-Ctrl-C, and Shift-Ctrl-V
• Finally, if you run into bugs or difficulties, please let me know! Screenshots are very much appreciated.