TPTP editor Smart Cell with a backend mode switch.

The cell drives all four AtpClient backends — SystemOnTPTP, StarExec, Isabelle, LocalExec — from a single TPTP problem editor. Switching the backend dropdown swaps both the per-call controls in the header (solver picker for SoTPTP, proof method for Isabelle, …) and the output rendering (raw prover text for SoTPTP, normalized SZS badge for StarExec/LocalExec, per-lemma table for Isabelle).

Cross-cutting credentials (StarExec base URL, Isabelle password, …) live in KinoAtpClient.BackendConfig so this cell stays focused on a single problem run.