diff --git a/priv/system_on_tptp/SYSTEMS.md b/priv/system_on_tptp/SYSTEMS.md index 1310d7d..e2c9b33 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-04T10:51:39Z; 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..894932a 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-04T10:51:39Z", "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",