Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
jonaprieto committed Feb 8, 2017
1 parent bc5d4ee commit bd141c2
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ fof(a4, conjecture, z).
````


We can now run the ATPS, in this example, we send the paramenter `--atp=vampire` specifying that we are going to use [Vampire](http://www.vprover.org) ATP to solve the problem described above. Then, we should run in our shell something like:
Using the option `--atp` we are able to use a ATP by his name. For instance, using `--atp=vampire` we specify that we are going to use [Vampire](http://www.vprover.org) ATP against the problem. Then, we should run in our shell something like:

```
$ online-atps basic.tptp --atp=vampire
Expand Down Expand Up @@ -104,7 +104,7 @@ OUTPUT: SOT_Xry401 - Vampire---4.1 says Refutation - CPU = 0.00 WC = 0.04
$ online-atps basic.tptp --atp=online-metis
````

* Only check if a problem states a theorem or not using `--only-check`
* Check if a problem states a theorem or not using `--only-check`

````bash
$ online-atps basic.tptp --atp=online-metis --only-check
Expand Down

0 comments on commit bd141c2

Please sign in to comment.