From dd246064a2d52f7f2bb69feb27f4f8ac6e4eea82 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 3 Nov 2026 10:48:26 +0000 Subject: [PATCH] =?UTF-8?q?systems:=20+AddTypes---1.4.4=20+Shot---0.1.5=20?= =?UTF-8?q?+Taelja---0.2.0.1=20+Vampire---5.1.1=20+Vampire-FMo---5.1.1=20+?= =?UTF-8?q?Vampire-LIT---5.1.1=20+Vampire-SAT---5.1.1=20+Vampire-SATLIT---?= =?UTF-8?q?5.1.1=20+cvc5---1.4.2=20+cvc5-SAT---1.4.2=20+cvc5-STC---1.4.2?= =?UTF-8?q?=20=E2=88=92Taelja---0.2.0.0=20=E2=88=92Vampire---5.0.1=20?= =?UTF-8?q?=E2=88=92Vampire-FMo---5.0.1=20=E2=88=92Vampire-LIT---5.0.1=20?= =?UTF-8?q?=E2=88=92Vampire-SAT---5.0.1=20=E2=88=92Vampire-SATLIT---5.0.1?= =?UTF-8?q?=20=E2=88=92cvc5---1.3.4=20=E2=88=92cvc5-SAT---1.3.4=20?= =?UTF-8?q?=E2=88=92cvc5-STC---1.3.4,=201=20field=20changed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- priv/system_on_tptp/SYSTEMS.md | 24 +++--- priv/system_on_tptp/systems.json | 135 ++++++++++++++++++++++++++----- 2 files changed, 126 insertions(+), 33 deletions(-) diff --git a/priv/system_on_tptp/SYSTEMS.md b/priv/system_on_tptp/SYSTEMS.md index 1310d7d..ca859fc 100644 --- a/priv/system_on_tptp/SYSTEMS.md +++ b/priv/system_on_tptp/SYSTEMS.md @@ -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-03T10:48:25Z; 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 | | @@ -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 | @@ -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/ | @@ -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/ | @@ -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/ | @@ -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/ | diff --git a/priv/system_on_tptp/systems.json b/priv/system_on_tptp/systems.json index 921a883..3c4a7ef 100644 --- a/priv/system_on_tptp/systems.json +++ b/priv/system_on_tptp/systems.json @@ -1,6 +1,6 @@ { - "count": 174, - "generated_at": "2026-10-16T09:09:16Z", + "count": 176, + "generated_at": "2026-11-03T10:48:25Z", "source": "https://tptp.org/cgi-bin/SystemOnTPTPFormReply", "systems": [ { @@ -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": { @@ -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" ], @@ -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", @@ -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" ], @@ -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", @@ -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", @@ -1333,8 +1375,11 @@ }, "spcs": [ "TH0_NAR", + "TH0_PRP", "TX0_NAR", + "TX0_PRP", "TF0_NAR", + "TF0_PRP", "FOF", "CNF" ], @@ -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": { @@ -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" ], @@ -5822,7 +5911,9 @@ ], "raw": { "dataforms": {}, - "end_soln": {}, + "end_soln": { + "Proof": "SZS output end Proof" + }, "gave_up": {}, "solved": {}, "status": [] @@ -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", @@ -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" ], @@ -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", @@ -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" ], @@ -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", @@ -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" ], @@ -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", @@ -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" ], @@ -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", @@ -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" ], @@ -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",