# `AtpClient.SystemOnTptp`
[🔗](https://github.com/jcschuster/AtpClient/blob/v0.2.0/lib/atp_client/system_on_tptp.ex#L1)

Public tptp.org HTTP form API; see `query_system/3` and `query_all_systems/2`.

## Configuration

    config :atp_client, :sotptp,
      url: "tptp.example.org/SystemOnTPTPFormReply",
      auto_refresh: true,
      refresh_timeout_ms: 100_000,
      default_time_limit_sec: 10

## Example

    thf_problem = """
    thf(conj,conjecture,
      ![X: $o]: (X | ~X)
    ).
    """

    {:ok, result} = AtpClient.SystemOnTptp.query_system(thf_problem, "Vampire-FMo---5.0")
    # => {:ok, :thm}

# `list_provers`

```elixir
@spec list_provers() :: [String.t()]
```

Returns a list with all available system identifiers from SystemOnTPTP that
correspond to known provers. This excludes type checking systems etc. which
also get returned by the API.

# `query_all_systems`

```elixir
@spec query_all_systems(String.t(), Keyword.t()) ::
  {:ok, [{String.t(), AtpClient.ResultNormalization.atp_result()}]}
  | {:ok, [{String.t(), String.t()}]}
  | {:error, term()}
```

Queries all available provers on SystemOnTPTP and returns results from systems
that did not error out. Returns a list of tuples `{system_id, result}`.

All options accepted by `query_selected_systems/3` are forwarded.

# `query_selected_systems`

```elixir
@spec query_selected_systems(String.t(), [String.t()], Keyword.t()) ::
  {:ok, [{String.t(), AtpClient.ResultNormalization.atp_result()}]}
  | {:ok, [{String.t(), String.t()}]}
  | {:error, term()}
```

Makes a single request to SystemOnTPTP to run all given systems with default
arguments. Accepted options are the same as for `query_system/3`.

# `query_system`

```elixir
@spec query_system(String.t(), String.t(), Keyword.t()) ::
  {:ok, String.t()}
  | AtpClient.ResultNormalization.atp_result()
  | {:error, term()}
```

Queries a specific system via SystemOnTPTP. Available systems can be looked
up with `list_provers/0`. The problem is expected to be in valid TPTP format
and compatible with the selected prover.

## Options

  * `:time_limit_sec` — time limit in seconds (default `5`);
  * `:raw` — return the raw prover output instead of interpreting it
    (default `false`);
  * `:url` — override the SystemOnTPTP endpoint URL.

---

*Consult [api-reference.md](api-reference.md) for complete listing*