Input
Tab inserts two spaces. To move focus out of the editor, press Escape and then Tab. Press Control plus Enter to run the solver.
Output
Write SMT-LIB in the editor or load an example, then press Run. The solver's answers appear here, with sat and unsat marked.