← all suites

simplipy

SimpliPy rewrite rules under principal branches

307 cases derived from the rewrite rules of SimpliPy (engine acj-4, Paul Saegert). SimpliPy's rules were accepted by numerical equivalence of real-valued float functions; read as claims over the reals or over the complex numbers with principal branches, many of them hold only under assumptions. Each rule appears in up to three flavours: over the reals, over the complex numbers, and under the weakest natural assumption that makes it true (or false everywhere). Labels come from the harness's numerics; almost every case is verified in Lean (universal statements for true and false cases, one true and one false witness for contingent ones). A public development set: systems may have seen these cases.

licence MIT

Categories
simplipy-real
Real flavour of rules found in both rule files: the rule over the reals, with only the assumptions that make it defined.
simplipy-f64-edge
Rules only in rules_real.json (rejected in float64, e.g. because of overflow), real flavour; and exact ground identities found only there.
simplipy-complex-branch
Complex flavour: the rule over the complex numbers with principal branches; tests branch cuts of log, pow and the inverse functions.
simplipy-conditional
The rule under the weakest natural assumption that makes it true, or under one that makes it false everywhere.
simplipy-ground
Exact variable-free identities found in both rule files (constant folding).

official cases as LaTeX (.tex)

Case set ba9dc4def822 — latest run per system

One column per CAS: the best of its routines (wrong if any is wrong, else solved if any solved it, else declined correctly if any did); +N shows the routines, older older versions. Click a category to see its cases.

show expected
category / casesympy best wolfram best
simplipy-complex-branch 8013/8015/80
simplipy-conditional 9212/9238/92
simplipy-f64-edge 4514/4517/45
simplipy-ground 2020/2020/20
simplipy-real 7024/7039/70
total83/307129/307
wrong00
declined correctly117117

Each cell shows what the system said, coloured by outcome: true ✓ solved, true ✗ wrong, no verdict: the system ran but did not commit to true or false (null); no verdict ✓ (grey ✓, on a contingent case) declined correctly: Correct: neither true nor false holds here. Not counted as solved, since a system that never answers would get this too.

Older case sets (2)

Case set 3ba0dfac4bca — latest run per system

One column per CAS: the best of its routines (wrong if any is wrong, else solved if any solved it, else declined correctly if any did); +N shows the routines, older older versions. Click a category to see its cases.

always-none, sympy-ask, sympy-refine, sympy-simplify, wolfram-fullsimplify, wolfram-refine, wolfram-simplify: old report format (graded with a combined score): its nulls are shown as no verdict, because an old report cannot tell a correct decline on a contingent case from no verdict

show expected
category / casesympy best wolfram best
simplipy-complex-branch 8013/8015/80
simplipy-conditional 9212/9238/92
simplipy-f64-edge 4514/4517/45
simplipy-ground 2020/2020/20
simplipy-real 7024/7039/70
total83/307129/307
wrong00
declined correctly00

Each cell shows what the system said, coloured by outcome: true ✓ solved, true ✗ wrong, no verdict: the system ran but did not commit to true or false (null); no verdict ✓ (grey ✓, on a contingent case) declined correctly: Correct: neither true nor false holds here. Not counted as solved, since a system that never answers would get this too.

Case set ee702ae2fe06 — latest run per system

One column per CAS: the best of its routines (wrong if any is wrong, else solved if any solved it, else declined correctly if any did); +N shows the routines, older older versions. Click a category to see its cases.

always-none, sympy-ask, sympy-refine, sympy-simplify, wolfram-fullsimplify, wolfram-refine, wolfram-simplify: old report format (graded with a combined score): its nulls are shown as no verdict, because an old report cannot tell a correct decline on a contingent case from no verdict

show expected
category / casesympy best wolfram best
simplipy-complex-branch 8013/8015/80
simplipy-conditional 9213/9238/92
simplipy-f64-edge 4516/4517/45
simplipy-ground 2020/2020/20
simplipy-real 7024/7039/70
total86/307129/307
wrong00
declined correctly00

Each cell shows what the system said, coloured by outcome: true ✓ solved, true ✗ wrong, no verdict: the system ran but did not commit to true or false (null); no verdict ✓ (grey ✓, on a contingent case) declined correctly: Correct: neither true nor false holds here. Not counted as solved, since a system that never answers would get this too.

All runs of this suite (21, official cases)
whensystemversion · mode · machinedialectcase setsolvedwrongdeclined correctlyno verdicttimeoutunsupported
2026-10-13 17:24:42wolfram-fullsimplify 14.3.0 · fork · pi5wolframba9dc4def82212901176100
2026-10-13 17:24:31wolfram-refine 14.3.0 · fork · pi5wolframba9dc4def82210301178700
2026-10-13 17:24:17wolfram-simplify 14.3.0 · fork · pi5wolframba9dc4def82210901178100
2026-10-13 17:24:01sympy-simplify1.14.0 · fork · pi5sympyba9dc4def82283011710700
2026-10-13 17:22:30sympy-refine1.14.0 · fork · pi5sympyba9dc4def82263011512630
2026-10-13 17:21:19sympy-ask1.14.0 · fork · pi5sympyba9dc4def82263011712700
2026-10-13 17:21:18always-nonepi5sexpba9dc4def8220011719000
2026-10-13 16:43:00wolfram-fullsimplify 14.3.0 · fork · pi5wolfram3ba0dfac4bca1290017800 old report
2026-10-13 16:42:50wolfram-refine 14.3.0 · fork · pi5wolfram3ba0dfac4bca1030020400 old report
2026-10-13 16:42:35wolfram-simplify 14.3.0 · fork · pi5wolfram3ba0dfac4bca1090019800 old report
2026-10-13 16:42:18sympy-simplify1.14.0 · fork · pi5sympy3ba0dfac4bca830022400 old report
2026-10-13 16:40:40sympy-refine1.14.0 · fork · pi5sympy3ba0dfac4bca630024040 old report
2026-10-13 16:39:28always-nonepi5sexp3ba0dfac4bca00030700 old report
2026-10-13 16:39:28sympy-ask1.14.0 · fork · pi5sympy3ba0dfac4bca630024400 old report
2026-10-12 21:55:24wolfram-fullsimplify 14.3.0 · fork · pi5wolframee702ae2fe061290017800 old report
2026-10-12 21:55:14wolfram-refine 14.3.0 · fork · pi5wolframee702ae2fe061030020400 old report
2026-10-12 21:55:00always-nonepi5sexpee702ae2fe0600030700 old report
2026-10-12 21:55:00wolfram-simplify 14.3.0 · fork · pi5wolframee702ae2fe061090019800 old report
2026-10-12 21:54:43sympy-simplify1.15.0.dev · fork · pi5sympyee702ae2fe06850022200 old report
2026-10-12 21:54:16sympy-refine1.15.0.dev · fork · pi5sympyee702ae2fe06650024200 old report
2026-10-12 21:54:02sympy-ask1.15.0.dev · fork · pi5sympyee702ae2fe06640024300 old report