Skip to content

systems: +AddTypes---1.4.4 +Shot---0.1.5 +Taelja---0.2.0.1 +Vampire---5.1.1 +Vampire-FMo---5.1.1 +Vampire-LIT---5.1.1 +Vampire-SAT---5.1.1 +Vampire-SATLIT---5.1.1 +cvc5---1.4.2 +cvc5-SAT---1.4.2 +cvc5-STC---1.4.2 −Taelja---0.2.0.0 −Vampire---5.0.1 −Vampire-FMo---5.0.1 −Vampire-LIT---5.0.1 −Vampire-SAT---5.0.1 −Vampire-SATLIT---5.0.1 −cvc5---1.3.4 −cvc5-SAT---1.3.4 −cvc5-STC---1.3.4, 1 field changed #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
github-actions wants to merge 1 commit into
base: main
Choose a base branch
from
Open

systems: +AddTypes---1.4.4 +Shot---0.1.5 +Taelja---0.2.0.1 +Vampire---5.1.1 +Vampire-FMo---5.1.1 +Vampire-LIT---5.1.1 +Vampire-SAT---5.1.1 +Vampire-SATLIT---5.1.1 +cvc5---1.4.2 +cvc5-SAT---1.4.2 +cvc5-STC---1.4.2 −Taelja---0.2.0.0 −Vampire---5.0.1 −Vampire-FMo---5.0.1 −Vampire-LIT---5.0.1 −Vampire-SAT---5.0.1 −Vampire-SATLIT---5.0.1 −cvc5---1.3.4 −cvc5-SAT---1.3.4 −cvc5-STC---1.3.4, 1 field changed #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 13 additions & 11 deletions priv/system_on_tptp/SYSTEMS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,12 @@
# SystemOnTPTP systems

Generated by `mix atp_client.systems.refresh` from https://tptp.org/cgi-bin/SystemOnTPTPFormReply at 2026-10-16T09:09:16Z; 174 systems.
Generated by `mix atp_client.systems.refresh` from https://tptp.org/cgi-bin/SystemOnTPTPFormReply at 2026-11-01T10:24:46Z; 176 systems.
Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` from `overrides.json`.

| System | Capabilities | Interfaces | SPCs | URL |
|---|---|---|---|---|
| `ACE2TPTP---0.0` | import | pre_tptp | | |
| `AddTypes---1.4.4` | transform | system_b4_tptp | TH1 TH0 TX1 TX0 TF1 TF0 | |
| `AGInTRater---0.0` | inspect† | system_on_tstp | | https://tptp.org/Seminars/AGInT/RaterSummary.html |
| `AGMV---1.0` | verify†, verify_model† | system_on_tstp | NX0 TX0 TF0 FOF | |
| `Alt-Ergo---0.95.2` | prove | system_on_tptp | TF1 TF0 FOF CNF | |
Expand All @@ -24,10 +25,10 @@ Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` fro
| `CSE_E---1.7` | find_model, prove | system_on_tptp | FOF CNF | |
| `CSI_E---1.1` | prove | | FOF CNF | |
| `CSI_PP---1.0` | prove | system_on_tptp | FOF CNF | |
| `cvc5---1.3.4` | find_model, prove | system_on_tptp | TH0 TX0 TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5---1.4.2` | find_model, prove | system_on_tptp | TH0 TX0 TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5-SAT---1.3.3.LK` | find_model | | TH0_NAR TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5-SAT---1.3.4` | find_model | system_on_tptp | TH0_NAR TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5-STC---1.3.4` | check† | | TH0_NAR TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5-SAT---1.4.2` | find_model | system_on_tptp | TH0_NAR TF0 FOF CNF | https://cvc5.github.io/ |
| `cvc5-STC---1.4.2` | check† | | TH0_NAR TF0 FOF CNF | https://cvc5.github.io/ |
| `Darwin---1.4.5` | find_model, prove | system_on_tptp | FOF CNF | |
| `DarwinFM---1.4.5` | find_model, prove | system_on_tptp | FOF_CSA FOF_SAT CNF_SAT FOF_UNK CNF_UNK | |
| `Dedukti---2.7` | verify | | TH0 TF0 FOF CNF | https://github.com/Deducteam/lambdapi |
Expand All @@ -37,7 +38,7 @@ Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` fro
| `Drodi-SAT---4.1.1` | find_model, prove | system_on_tptp | FOF CNF | |
| `DT2H2X---1.9.5` | find_model, prove | system_on_tptp | DH1_NAR DH0_NAR NH1_NAR NH0_NAR TH1_NAR TH0_NAR | |
| `Duper---1.0` | prove | system_on_tptp | TH1_NAR TH0_NAR TF1_NAR TF0_NAR FOF | https://github.com/leanprover-community/duper |
| `E---3.5.1` | find_model, prove | system_on_tptp | TH0_NAR TX0_NAR TF0_NAR FOF CNF | http://www.eprover.org/ |
| `E---3.5.1` | find_model, prove | system_on_tptp | TH0_NAR TH0_PRP TX0_NAR TX0_PRP TF0_NAR TF0_PRP FOF CNF | http://www.eprover.org/ |
| `E-Darwin---1.5` | find_model, prove | system_on_tptp | FOF CNF | |
| `E-SAT---3.5.1` | find_model, prove | system_on_tptp | TF0_NAR FOF CNF | http://www.eprover.org/ |
| `ECNF---3.5.1` | transform | system_b4_tptp | FOF | http://www.eprover.org/ |
Expand Down Expand Up @@ -134,6 +135,7 @@ Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` fro
| `SC-TPTP---0.0` | verify | system_on_tstp | FOF CNF | https://github.com/SC-TPTP/sc-tptp |
| `Scavenger---EP-0.2` | find_model, prove | system_on_tptp | FOF CNF | https://gitlab.com/aossie/Scavenger |
| `SEM---1.7` | find_model | | CNF_SAT CNF_UNK | http://www.cs.uiowa.edu/~hzhang/sem.html |
| `Shot---0.1.5` | prove | system_on_tptp | TH0_NAR | https://github.com/jcschuster/ShotTx/ |
| `ShZZaM---0.2` | transform | system_b4_tptp | | |
| `SInE---0.4` | prove | | FOF | http://www.cs.man.ac.uk/~hoderk/sine/ |
| `SInE-LTB---0.4` | prove | | | http://www.cs.man.ac.uk/~hoderk/sine/ |
Expand All @@ -149,7 +151,7 @@ Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` fro
| `SRASS---0.1` | prove | system_on_tptp | FOF | https://tptp.org/ATPSystems/SRASS/ |
| `SSCPA---0.0` | prove | | | https://tptp.org/cgi-bin/SystemOnTPTP |
| `SUPr---1.0` | prove | system_on_tptp | TF0 FOF CNF | https://github.com/ontologyportal/sigma-rs |
| `Taelja---0.2.0.0` | transform† | system_on_tstp | | https://github.com/kondylidou/Taelja |
| `Taelja---0.2.0.1` | transform† | system_on_tstp | | https://github.com/kondylidou/Taelja |
| `ToFoF---0.1` | find_model, prove | system_on_tptp | TF0_NAR | http://tptp.org/ATPSystems/ToFoF/ |
| `ToFoF-SAT---0.1` | find_model, prove | system_on_tptp | TF0_NAR | http://tptp.org/ATPSystems/ToFoF/ |
| `Toma---0.7` | prove | system_on_tptp | CNF_UEQ | https://www.jaist.ac.jp/project/maxcomp/ |
Expand All @@ -161,12 +163,12 @@ Capabilities: unmarked from the rules, `*` from the UserNote fallback, `†` fro
| `TSTP2NL---0.2` | transform† | system_on_tstp | | |
| `Twee---2.7` | find_model, prove | system_on_tptp | TF0_NAR FOF CNF | http://nick8325.github.io/twee/ |
| `VaLeaDate---0.1` | verify | | FOF CNF | https://github.com/i-am-a-teapot/VaLeaDate |
| `Vampire---5.0.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-FMo---5.0.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TF1_NAR TX0 TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-LIT---5.0.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire---5.1.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-FMo---5.1.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TF1_NAR TX0 TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-LIT---5.1.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-LP---5.0.1` | prove† | system_on_tptp | TH1_NAR TH0_NAR TF1_NAR TX0 TF0 FOF CNF | |
| `Vampire-SAT---5.0.1` | find_model, prove | system_on_tptp | TX0 TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-SATLIT---5.0.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-SAT---5.1.1` | find_model, prove | system_on_tptp | TX0 TF0 FOF CNF | https://vprover.github.io/ |
| `Vampire-SATLIT---5.1.1` | find_model, prove | system_on_tptp | TH1_NAR TH0_NAR TX1_NAR TX0 TF1_NAR TF0 FOF CNF | https://vprover.github.io/ |
| `VCNF---4.8` | transform | system_b4_tptp | FOF | https://vprover.github.io/ |
| `VIP---1.718` | prove | system_on_tptp | FOF CNF | https://github.com/delahayd/ip.git |
| `VSelect---4.4` | transform | system_b4_tptp | | https://vprover.github.io/ |
Expand Down
135 changes: 113 additions & 22 deletions priv/system_on_tptp/systems.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"count": 174,
"generated_at": "2026-10-16T09:09:16Z",
"count": 176,
"generated_at": "2026-11-01T10:24:46Z",
"source": "https://tptp.org/cgi-bin/SystemOnTPTPFormReply",
"systems": [
{
Expand Down Expand Up @@ -29,6 +29,48 @@
"url": null,
"version": "0.0"
},
{
"command": "run_addtypes %s",
"dataforms": {
"ListOfFormulae": "SZS output start ListOfFormulae"
},
"format": "tptp:raw",
"id": "AddTypes---1.4.4",
"interfaces": [
"system_b4_tptp"
],
"listings": [],
"name": "AddTypes",
"note": "Add missing type declarations",
"people": [
"Alex Steen"
],
"raw": {
"dataforms": {},
"end_soln": {
"ListOfFormulae": "SZS output end ListOfFormulae"
},
"gave_up": {},
"solved": {},
"status": []
},
"solved": {
"NoSuccess": "SZS status UsageError",
"Success": "SZS status Success"
},
"spcs": [
"TH1",
"TH0",
"TX1",
"TX0",
"TF1",
"TF0"
],
"statistic": null,
"transform": "none",
"url": null,
"version": "1.4.4"
},
{
"command": "AGInTRater -c %s",
"dataforms": {
Expand Down Expand Up @@ -742,7 +784,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "cvc5---1.3.4",
"id": "cvc5---1.4.2",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -785,7 +827,7 @@
"statistic": null,
"transform": "none",
"url": "https://cvc5.github.io/",
"version": "1.3.4"
"version": "1.4.2"
},
{
"command": "do_cvc5 %s %d SAT",
Expand Down Expand Up @@ -839,7 +881,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "cvc5-SAT---1.3.4",
"id": "cvc5-SAT---1.4.2",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -878,13 +920,13 @@
"statistic": null,
"transform": "none",
"url": "https://cvc5.github.io/",
"version": "1.3.4"
"version": "1.4.2"
},
{
"command": "run_stc %s",
"dataforms": {},
"format": "tptp:raw",
"id": "cvc5-STC---1.3.4",
"id": "cvc5-STC---1.4.2",
"interfaces": [],
"listings": [],
"name": "cvc5-STC",
Expand Down Expand Up @@ -912,7 +954,7 @@
"statistic": null,
"transform": "none",
"url": "https://cvc5.github.io/",
"version": "1.3.4"
"version": "1.4.2"
},
{
"command": "darwin -pl 0 -pmc true -to %d %s",
Expand Down Expand Up @@ -1333,8 +1375,11 @@
},
"spcs": [
"TH0_NAR",
"TH0_PRP",
"TX0_NAR",
"TX0_PRP",
"TF0_NAR",
"TF0_PRP",
"FOF",
"CNF"
],
Expand Down Expand Up @@ -5236,6 +5281,48 @@
"url": "http://www.cs.uiowa.edu/~hzhang/sem.html",
"version": "1.7"
},
{
"command": "bin/shot --szs --proof --cpu-timeout %d000 %s",
"dataforms": {
"Proof": "SZS output start Proof"
},
"format": "tptp:raw",
"id": "Shot---0.1.5",
"interfaces": [
"system_on_tptp"
],
"listings": [
"tstp",
"starexec"
],
"name": "Shot",
"note": "Prover",
"people": [
"Johannes Schuster"
],
"raw": {
"dataforms": {},
"end_soln": {
"Proof": "SZS output end Proof"
},
"gave_up": {},
"solved": {},
"status": []
},
"solved": {
"CounterSatisfiable": "SZS status CounterSatisfiable",
"Satisfiable": "SZS status Satisfiable",
"Theorem": "SZS status Theorem",
"Unsatisfiable": "SZS status Unsatisfiable"
},
"spcs": [
"TH0_NAR"
],
"statistic": null,
"transform": "none",
"url": "https://github.com/jcschuster/ShotTx/",
"version": "0.1.5"
},
{
"command": "run_ShZZaM %s",
"dataforms": {
Expand Down Expand Up @@ -5808,9 +5895,11 @@
},
{
"command": "run_taelja %s",
"dataforms": {},
"dataforms": {
"Proof": "SZS output start Proof"
},
"format": "tptp:raw",
"id": "Taelja---0.2.0.0",
"id": "Taelja---0.2.0.1",
"interfaces": [
"system_on_tstp"
],
Expand All @@ -5822,7 +5911,9 @@
],
"raw": {
"dataforms": {},
"end_soln": {},
"end_soln": {
"Proof": "SZS output end Proof"
},
"gave_up": {},
"solved": {},
"status": []
Expand All @@ -5834,7 +5925,7 @@
"statistic": null,
"transform": "none",
"url": "https://github.com/kondylidou/Taelja",
"version": "0.2.0.0"
"version": "0.2.0.1"
},
{
"command": "tofof %d %s",
Expand Down Expand Up @@ -6245,7 +6336,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "Vampire---5.0.1",
"id": "Vampire---5.1.1",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -6293,7 +6384,7 @@
"statistic": null,
"transform": "none",
"url": "https://vprover.github.io/",
"version": "5.0.1"
"version": "5.1.1"
},
{
"command": "vampire -sa fmb --forced_options bce=off:updr=off:fde=none:rp=off -m 16384 -t %d %s",
Expand All @@ -6303,7 +6394,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "Vampire-FMo---5.0.1",
"id": "Vampire-FMo---5.1.1",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -6344,7 +6435,7 @@
"statistic": null,
"transform": "none",
"url": "https://vprover.github.io/",
"version": "5.0.1"
"version": "5.1.1"
},
{
"command": "vampire --mode vampire --forced_options av=off:nm=0:bce=off:updr=off:fde=none:rp=off --proof tptp -m 16384 -t %d %s",
Expand All @@ -6354,7 +6445,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "Vampire-LIT---5.0.1",
"id": "Vampire-LIT---5.1.1",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -6397,7 +6488,7 @@
"statistic": null,
"transform": "none",
"url": "https://vprover.github.io/",
"version": "5.0.1"
"version": "5.1.1"
},
{
"command": "run_vlp %s",
Expand Down Expand Up @@ -6449,7 +6540,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "Vampire-SAT---5.0.1",
"id": "Vampire-SAT---5.1.1",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -6493,7 +6584,7 @@
"statistic": null,
"transform": "none",
"url": "https://vprover.github.io/",
"version": "5.0.1"
"version": "5.1.1"
},
{
"command": "vampire --mode vampire --intent sat --forced_options av=off:nm=0:bce=off:updr=off:fde=none:rp=off --proof tptp -m 16384 -t %d %s",
Expand All @@ -6503,7 +6594,7 @@
"Saturation": "SZS output start Saturation"
},
"format": "tptp:raw",
"id": "Vampire-SATLIT---5.0.1",
"id": "Vampire-SATLIT---5.1.1",
"interfaces": [
"system_on_tptp"
],
Expand Down Expand Up @@ -6546,7 +6637,7 @@
"statistic": null,
"transform": "none",
"url": "https://vprover.github.io/",
"version": "5.0.1"
"version": "5.1.1"
},
{
"command": "run_vclausify_rel %s %d",
Expand Down