diff --git a/tptp-test-report.md b/tptp-test-report.md new file mode 100644 index 000000000..5dc404f4c --- /dev/null +++ b/tptp-test-report.md @@ -0,0 +1,139 @@ +# TPTP Integration Test Report — `copilot/integrate-tptp-into-src-shell` + +**Date:** 2026-05-12 +**Branch:** `copilot/integrate-tptp-into-src-shell` +**Z3 version:** 4.17.0 (64-bit) +**Test corpus:** 500 randomly-selected TPTP v8.1.2 problems +**Domains sampled:** ARI (Arithmetic, n=247), SET (Set Theory, n=168), SYN (Syntactic, n=85) +**Invocation:** `z3 -T:5 ` + +> **Note:** `tptp.org` was not accessible from the test sandbox (DNS blocked). Problems were drawn from the GoelandProver/GoelandBenchmarks repository, which mirrors TPTP v8.1.2 problem files in the same format. + +--- + +## Executive Summary + +| Category | Count | Pct | +|---|---|---| +| Correct answer | 178 | 35.6% | +| Wrong answer | 25 | 5.0% | +| Parse error - negative literal | 52 | 10.4% | +| Parse error - rational literal | 40 | 8.0% | +| Parse error - TFF type declaration | 96 | 19.2% | +| Sort mismatch (TFF arithmetic) | 46 | 9.2% | +| Crash (unhandled z3_error) | 40 | 8.0% | +| Timeout (process killed at 5s) | 23 | 4.6% | + +**Overall correct rate: 178/500 = 35.6%** + +--- + +## Timing + +| Metric | Value | +|---|---| +| Minimum | 0.010 s | +| Maximum | 10.141 s | +| Mean | 1.099 s | +| Median | 0.029 s | +| Under 1 s | 435 (87.0%) | +| 1-5 s | 2 (0.4%) | +| Over 5 s | 63 (12.6%) | + +--- + +## Per-Domain Results + +| Domain | Correct | Total | Rate | +|---|---|---|---| +| ARI (Arithmetic) | 0 | 247 | 0.0% | +| SET (Set Theory) | 113 | 168 | 67.3% | +| SYN (Syntactic) | 65 | 85 | 76.5% | + +--- + +## Bug Findings + +### Bug 1 - Negative integer literals not parsed (52 files) + +The TFF parser rejects negative integer literals such as `-2` or `-4`. + +Example (ARI007_1.p): +``` +tff(n2_less_2,conjecture, $less(-2,2) ). +``` +Error: `TPTP parse error: unexpected character '-' at 32:11` + +Every TFF problem using negative constants fails immediately. + +--- + +### Bug 2 - Rational/real literals not parsed (40 files) + +The parser rejects rational literals written as `p/q` (TPTP syntax for rationals, e.g. `1/2`). + +Error pattern: `TPTP parse error: unexpected character '/' at 32:11` + +--- + +### Bug 3 - TFF user-type declarations parse error (96 files) + +TFF problems that introduce predicate or function type signatures fail to parse. + +Example (ARI094_1.p): +``` +tff(p_type,type, p: $int > $o ). +``` +Error: `TPTP parse error: expected ')' at 32:19` + +The `: $int > $o` type product syntax is not supported. + +--- + +### Bug 4 - Sort mismatch for TFF typed variables (46 files) + +When a TFF formula uses typed quantifier variables such as `[X: $int]`, the TPTP frontend binds them to the uninterpreted sort `U` rather than Z3's `Int` sort, causing a sort mismatch when they are passed to arithmetic built-ins. + +Example (ARI005_1.p): +``` +tff(prove_12_less_something,conjecture, ? [X: $int] : $less(12,X) ). +``` +Error: `TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) supplied sort: Int` + +--- + +### Bug 5 - Arithmetic built-ins treated as uninterpreted (25 wrong answers) + +Even when parsing succeeds, simple TFF arithmetic conjectures return CounterSatisfiable instead of Theorem. The arithmetic predicates `$less`, `$lesseq`, `$greater`, `$greatereq` are being declared as uninterpreted predicates over sort `U`, not mapped to Z3 built-in arithmetic relations. + +Examples of wrong answers: +- ARI002_1.p: `~ $less(3,2)` → expected Theorem, got CounterSatisfiable +- ARI014_1.p: `$lesseq(2,2)` → expected Theorem, got CounterSatisfiable +- ARI015_1.p: `$less(2,3)` → expected Theorem, got CounterSatisfiable + +--- + +### Bug 6 - Unhandled z3_error exception on timeout (40 crashes) + +When a problem hits the timeout, Z3 crashes with: +``` +terminate called after throwing an instance of 'z3_error' + what(): timeout +``` +instead of printing `% SZS status Timeout` and exiting cleanly. The TPTP frontend does not catch `z3_error` around the solver call. + +--- + +## SET and SYN Domain (67-77% Success) + +The SET and SYN domains use purely first-order FOF (untyped) formulas with no arithmetic and work reasonably well. Main failure modes are timeouts on harder combinatorial problems. + +--- + +## Recommendations + +1. Fix negative/rational literal parsing in the TPTP5 lexer +2. Map TFF arithmetic sorts ($int, $rat, $real) to Z3 Int/Real sorts +3. Map arithmetic predicates ($less, $lesseq, etc.) to Z3 built-in arithmetic relations +4. Support TFF type declaration syntax (name: sort > sort) +5. Catch z3_error in the TPTP frontend and output SZS Timeout status instead of crashing diff --git a/tptp-test-results.json b/tptp-test-results.json new file mode 100644 index 000000000..5999078da --- /dev/null +++ b/tptp-test-results.json @@ -0,0 +1,4502 @@ +[ + { + "file": "ARI_ARI007_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:11", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:11" + }, + { + "file": "ARI_ARI014_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.022, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI002_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI008_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:11", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:11" + }, + { + "file": "ARI_ARI015_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.027, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI005_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.029, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI017_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supp", + "elapsed": 0.024, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI020_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI040_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:28", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:28" + }, + { + "file": "ARI_ARI046_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.014, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI029_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.027, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI031_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greater (U U) Bool) sup", + "elapsed": 0.025, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greater (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI024_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:15", + "elapsed": 0.031, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:15" + }, + { + "file": "ARI_ARI055_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI025_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supp", + "elapsed": 0.035, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI051_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:18", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:18" + }, + { + "file": "ARI_ARI044_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.036, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI062_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.02, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI072_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:28", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:28" + }, + { + "file": "ARI_ARI052_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.032, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI066_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:10", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:10" + }, + { + "file": "ARI_ARI065_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.025, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI074_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:28", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:28" + }, + { + "file": "ARI_ARI082_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sorts U and Int are incompatible", + "elapsed": 0.031, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sorts U and Int are incompatible" + }, + { + "file": "ARI_ARI089_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.023, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI097_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI086_1.p", + "expected": "CounterSatisfiable", + "z3_status": "CounterSatisfiable", + "elapsed": 0.033, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI103_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.021, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI094_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI091_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $difference (U U) U) sup", + "elapsed": 0.03, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $difference (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI105_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.013, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI104_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sorts U and Int are incompatible", + "elapsed": 0.027, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sorts U and Int are incompatible" + }, + { + "file": "ARI_ARI111_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:30", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:30" + }, + { + "file": "ARI_ARI119_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.012, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI118_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.021, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI115_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:32", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:32" + }, + { + "file": "ARI_ARI112_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:32", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:32" + }, + { + "file": "ARI_ARI117_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.027, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI120_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI131_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:10", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:10" + }, + { + "file": "ARI_ARI167_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:20", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:20" + }, + { + "file": "ARI_ARI121_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sorts U and Int are incompatible", + "elapsed": 0.028, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sorts U and Int are incompatible" + }, + { + "file": "ARI_ARI128_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:5", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:5" + }, + { + "file": "ARI_ARI164_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI125_1.p", + "expected": "CounterSatisfiable", + "z3_status": "CounterSatisfiable", + "elapsed": 0.034, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI171_1.p", + "expected": "CounterSatisfiable", + "z3_status": "Error: TPTP frontend error: Sorts U and Int are incompatible", + "elapsed": 0.013, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sorts U and Int are incompatible" + }, + { + "file": "ARI_ARI169_1.p", + "expected": "CounterSatisfiable", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.021, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI132_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.035, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI170_1.p", + "expected": "CounterSatisfiable", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.021, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI168_1.p", + "expected": "CounterSatisfiable", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.03, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI177_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.016, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI175_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI174_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.028, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI179_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.02, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI193_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:28", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:28" + }, + { + "file": "ARI_ARI183_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:21", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:21" + }, + { + "file": "ARI_ARI192_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:12", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:12" + }, + { + "file": "ARI_ARI190_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:12", + "elapsed": 0.031, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:12" + }, + { + "file": "ARI_ARI218_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:17", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:17" + }, + { + "file": "ARI_ARI211_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI196_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:11", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:11" + }, + { + "file": "ARI_ARI207_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:28", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:28" + }, + { + "file": "ARI_ARI204_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:14", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:14" + }, + { + "file": "ARI_ARI215_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:29", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:29" + }, + { + "file": "ARI_ARI220_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:30", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:30" + }, + { + "file": "ARI_ARI226_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:16", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:16" + }, + { + "file": "ARI_ARI222_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greater (U U) Bool) sup", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greater (U U) Bool) supplied sort is $rat" + }, + { + "file": "ARI_ARI223_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:16", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:16" + }, + { + "file": "ARI_ARI227_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:29", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:29" + }, + { + "file": "ARI_ARI229_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:28", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:28" + }, + { + "file": "ARI_ARI238_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:16", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:16" + }, + { + "file": "ARI_ARI225_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:16", + "elapsed": 0.035, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:16" + }, + { + "file": "ARI_ARI233_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:32", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:32" + }, + { + "file": "ARI_ARI239_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:18", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:18" + }, + { + "file": "ARI_ARI230_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:17", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:17" + }, + { + "file": "ARI_ARI241_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:33", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:33" + }, + { + "file": "ARI_ARI235_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.029, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is $rat" + }, + { + "file": "ARI_ARI246_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI258_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:20", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:20" + }, + { + "file": "ARI_ARI248_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI253_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:28", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:28" + }, + { + "file": "ARI_ARI252_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI256_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI262_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI263_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:11", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:11" + }, + { + "file": "ARI_ARI257_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:18", + "elapsed": 0.033, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:18" + }, + { + "file": "ARI_ARI276_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:17", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:17" + }, + { + "file": "ARI_ARI274_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:18", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:18" + }, + { + "file": "ARI_ARI284_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:15", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:15" + }, + { + "file": "ARI_ARI265_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:27", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:27" + }, + { + "file": "ARI_ARI291_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:16", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:16" + }, + { + "file": "ARI_ARI299_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI290_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI289_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI296_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:21", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:21" + }, + { + "file": "ARI_ARI286_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:15", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:15" + }, + { + "file": "ARI_ARI312_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:22", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:22" + }, + { + "file": "ARI_ARI297_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:23", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:23" + }, + { + "file": "ARI_ARI344_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:45", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:45" + }, + { + "file": "ARI_ARI304_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:32", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:32" + }, + { + "file": "ARI_ARI300_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:15", + "elapsed": 0.037, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:15" + }, + { + "file": "ARI_ARI337_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.021, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is $rat" + }, + { + "file": "ARI_ARI355_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:29", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:29" + }, + { + "file": "ARI_ARI354_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI359_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:14", + "elapsed": 0.016, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:14" + }, + { + "file": "ARI_ARI365_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI339_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:18", + "elapsed": 0.033, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:18" + }, + { + "file": "ARI_ARI357_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:26", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:26" + }, + { + "file": "ARI_ARI364_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI374_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:15", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:15" + }, + { + "file": "ARI_ARI368_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:15", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:15" + }, + { + "file": "ARI_ARI369_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:31", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:31" + }, + { + "file": "ARI_ARI370_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:30", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:30" + }, + { + "file": "ARI_ARI379_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI373_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:17", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:17" + }, + { + "file": "ARI_ARI375_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:31", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:31" + }, + { + "file": "ARI_ARI382_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:30", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:30" + }, + { + "file": "ARI_ARI378_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:15", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:15" + }, + { + "file": "ARI_ARI385_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:17", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:17" + }, + { + "file": "ARI_ARI392_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:17", + "elapsed": 0.011, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:17" + }, + { + "file": "ARI_ARI388_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:33", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:33" + }, + { + "file": "ARI_ARI384_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:31", + "elapsed": 0.032, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:31" + }, + { + "file": "ARI_ARI390_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.02, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is Real" + }, + { + "file": "ARI_ARI402_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:11", + "elapsed": 0.01, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:11" + }, + { + "file": "ARI_ARI386_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:17", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:17" + }, + { + "file": "ARI_ARI389_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:35", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:35" + }, + { + "file": "ARI_ARI391_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:16", + "elapsed": 0.032, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:16" + }, + { + "file": "ARI_ARI417_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:28", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:28" + }, + { + "file": "ARI_ARI405_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:28", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:28" + }, + { + "file": "ARI_ARI411_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:17", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:17" + }, + { + "file": "ARI_ARI424_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:30", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:30" + }, + { + "file": "ARI_ARI419_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:28", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:28" + }, + { + "file": "ARI_ARI414_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:11", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:11" + }, + { + "file": "ARI_ARI410_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:19", + "elapsed": 0.032, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:19" + }, + { + "file": "ARI_ARI440_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI427_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:18", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:18" + }, + { + "file": "ARI_ARI443_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:32", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:32" + }, + { + "file": "ARI_ARI432_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:25", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:25" + }, + { + "file": "ARI_ARI441_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:14", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:14" + }, + { + "file": "ARI_ARI444_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:34", + "elapsed": 0.024, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:34" + }, + { + "file": "ARI_ARI459_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:5", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:5" + }, + { + "file": "ARI_ARI446_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:18", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:18" + }, + { + "file": "ARI_ARI445_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:32", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:32" + }, + { + "file": "ARI_ARI463_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI464_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:21", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:21" + }, + { + "file": "ARI_ARI460_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:6", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:6" + }, + { + "file": "ARI_ARI491_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:17", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:17" + }, + { + "file": "ARI_ARI461_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:12", + "elapsed": 0.031, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:12" + }, + { + "file": "ARI_ARI504_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI505_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:15", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:15" + }, + { + "file": "ARI_ARI493_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.03, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Real" + }, + { + "file": "ARI_ARI510_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:17", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:17" + }, + { + "file": "ARI_ARI506_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:7", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:7" + }, + { + "file": "ARI_ARI508_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI512_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:13", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:13" + }, + { + "file": "ARI_ARI511_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:34", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:34" + }, + { + "file": "ARI_ARI507_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:16", + "elapsed": 0.031, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:16" + }, + { + "file": "ARI_ARI513_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:14", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:14" + }, + { + "file": "ARI_ARI519_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) s", + "elapsed": 0.02, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $greatereq (U U) Bool) supplied sort is Real" + }, + { + "file": "ARI_ARI523_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:25", + "elapsed": 0.012, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:25" + }, + { + "file": "ARI_ARI516_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:27", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:27" + }, + { + "file": "ARI_ARI528_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:20", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:20" + }, + { + "file": "ARI_ARI515_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supp", + "elapsed": 0.034, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $lesseq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI522_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:11", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:11" + }, + { + "file": "ARI_ARI525_1.p", + "expected": "CounterSatisfiable", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:38", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:38" + }, + { + "file": "ARI_ARI543_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:20", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:20" + }, + { + "file": "ARI_ARI520_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.035, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI536_2.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $product (U U) U) supplied sort is Real" + }, + { + "file": "ARI_ARI537_1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.021, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "ARI_ARI545_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI553_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 32:20", + "elapsed": 0.016, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 32:20" + }, + { + "file": "ARI_ARI546_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:33", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:33" + }, + { + "file": "ARI_ARI565_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:19", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:19" + }, + { + "file": "ARI_ARI558_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:39", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:39" + }, + { + "file": "ARI_ARI564_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:33", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:33" + }, + { + "file": "ARI_ARI548_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:39", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:39" + }, + { + "file": "ARI_ARI561_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:11", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:11" + }, + { + "file": "ARI_ARI576_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) suppli", + "elapsed": 0.014, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $product (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI571_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI567_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 32:40", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 32:40" + }, + { + "file": "ARI_ARI575_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.019, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI577_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $lesseq (U U) Bool) supp", + "elapsed": 0.027, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $lesseq (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI579_3.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 33:16", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 33:16" + }, + { + "file": "ARI_ARI581_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.023, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI579_2.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '/' at 33:16", + "elapsed": 0.033, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '/' at 33:16" + }, + { + "file": "ARI_ARI585_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied s", + "elapsed": 0.021, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $sum (U U) U) supplied sort is Int" + }, + { + "file": "ARI_ARI583_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.023, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #2 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI593_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI588_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: unexpected character '-' at 34:26", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: unexpected character '-' at 34:26" + }, + { + "file": "ARI_ARI582_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) suppli", + "elapsed": 0.034, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $less (U U) Bool) supplied sort is Int" + }, + { + "file": "ARI_ARI606_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:21", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:21" + }, + { + "file": "ARI_ARI597_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI610_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:21", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:21" + }, + { + "file": "ARI_ARI614_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI595_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.034, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI613_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI612_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:19", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:19" + }, + { + "file": "ARI_ARI608_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:21", + "elapsed": 0.038, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:21" + }, + { + "file": "ARI_ARI615_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: type product must be followed by '>'", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: type product must be followed by '>'" + }, + { + "file": "ARI_ARI616_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: type product must be followed by '>'", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: type product must be followed by '>'" + }, + { + "file": "ARI_ARI617_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:21", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:21" + }, + { + "file": "ARI_ARI619_2.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI620_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI626_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sorts Int and U are incompatible", + "elapsed": 0.012, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sorts Int and U are incompatible" + }, + { + "file": "ARI_ARI632_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:15", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:15" + }, + { + "file": "ARI_ARI621_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.032, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI622_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:22", + "elapsed": 0.029, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:22" + }, + { + "file": "ARI_ARI638_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:15", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:15" + }, + { + "file": "ARI_ARI646_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI636_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:15", + "elapsed": 0.025, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:15" + }, + { + "file": "ARI_ARI621_3.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:23", + "elapsed": 0.038, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:23" + }, + { + "file": "ARI_ARI635_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:15", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:15" + }, + { + "file": "ARI_ARI639_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:17", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:17" + }, + { + "file": "ARI_ARI659_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI653_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI661_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI670_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.016, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI676_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI652_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI663_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI669_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI679_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.021, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI682_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.019, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI700_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.016, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI698_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.016, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI683_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.027, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI689_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI688_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.026, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI680_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.036, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI712_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.013, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI707_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.022, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI716_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:46", + "elapsed": 0.017, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:46" + }, + { + "file": "ARI_ARI711_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 34:14", + "elapsed": 0.028, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 34:14" + }, + { + "file": "ARI_ARI713_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $ceiling (U) U) supplied", + "elapsed": 0.022, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $ceiling (U) U) supplied sort is Real" + }, + { + "file": "ARI_ARI725_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:46", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:46" + }, + { + "file": "ARI_ARI744_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:25", + "elapsed": 0.018, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:25" + }, + { + "file": "ARI_ARI733_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $is_int (U) Bool) suppli", + "elapsed": 0.02, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $is_int (U) Bool) supplied sort is Real" + }, + { + "file": "ARI_ARI732_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $is_int (U) Bool) suppli", + "elapsed": 0.023, + "timeout": false, + "exit_code": 110, + "stderr": "TPTP frontend error: Sort mismatch at argument #1 for function (declare-fun $is_int (U) Bool) supplied sort is Real" + }, + { + "file": "ARI_ARI715_1.p", + "expected": "Theorem", + "z3_status": "Error: TPTP parse error: expected ')' at 32:37", + "elapsed": 0.035, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 32:37" + }, + { + "file": "ARI_ARI749_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.02, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI755_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.015, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI758_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.014, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI748_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.03, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI745_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.031, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI752_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI751_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.033, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "ARI_ARI761_1.p", + "expected": "Unsatisfiable", + "z3_status": "Error: TPTP parse error: expected ')' at 35:23", + "elapsed": 0.023, + "timeout": false, + "exit_code": 103, + "stderr": "TPTP parse error: expected ')' at 35:23" + }, + { + "file": "SET_SET012+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.024, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET002+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.037, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET020+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.035, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET055+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET027+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.043, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET062+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.024, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET063+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.035, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET008+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.12, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET011+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.128, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET084+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.079, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET095+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.029, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET101+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.039, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET016+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.26, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET016+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.048, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET117+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.031, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET045+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.057, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET143+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.021, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET064+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.074, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET066+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.054, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET065+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.078, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET071+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.037, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET143+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.143, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET104+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.02, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET200+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.059, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET159+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.066, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET183+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.069, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET155+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.061, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET148+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.073, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET589+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET201+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.055, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET576+3.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.057, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET586+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.06, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET592+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.084, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET598+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.05, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET595+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.083, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET593+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.057, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET594+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.096, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET602+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.065, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET597+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.108, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET602+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.099, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET603+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.171, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET606+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.172, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET613+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.118, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET610+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.235, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET618+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.041, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET619+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.067, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET622+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.166, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET624+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.074, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET628+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.053, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET630+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.049, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET633+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.051, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET636+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.152, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET637+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 2.901, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET641+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 1.196, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET643+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.049, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET144+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.423, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET607+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.544, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET658+3.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.064, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET609+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.699, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET612+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.027, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET159+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.656, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET614+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.479, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET108+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.082, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET648+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.031, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET652+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.035, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET668+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.281, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET669+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.117, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET688+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET689+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.032, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET693+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.031, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET660+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.085, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET664+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.079, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET698+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.049, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET670+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.406, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET700+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.339, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET703+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.056, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET704+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.07, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET708+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.116, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET709+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.093, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET712+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.043, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET713+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.043, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET717+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.027, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET672+3.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.797, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET697+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 5.696, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET728+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.06, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET729+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.051, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET731+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.038, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET733+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET695+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.052, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET723+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.386, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET707+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.163, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET745+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.046, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET750+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET754+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.044, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET755+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.04, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET756+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.041, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET759+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.04, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET761+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET762+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.056, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET766+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.042, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET767+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.018, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET769+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.121, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET770+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.034, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET776+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.02, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET789+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.033, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET791+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET792+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET796+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.021, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET797+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.027, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET798+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.039, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET800+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.018, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET802+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET683+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.044, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET804+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.038, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET807+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.07, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET813+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.05, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET814+4.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.113, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET684+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.055, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET875+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.043, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET876+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.05, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET877+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.047, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET878+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.063, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET881+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET685+3.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.087, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET885+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.31, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET889+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.339, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET894+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.109, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET899+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.021, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET900+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.036, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET906+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.038, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET911+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.035, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET926+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET724+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.011, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET735+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.022, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET738+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.847, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET739+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.211, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET816+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 5.917, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET817+4.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.357, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET954+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.017, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET955+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET914+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 5.907, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET959+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.105, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET961+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET934+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.188, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET941+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.092, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET944+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.397, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET974+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET975+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET945+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.704, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET978+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.028, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET979+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.028, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET948+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.255, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET952+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.737, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET985+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET986+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.016, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET960+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 8.315, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET963+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 8.593, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET991+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.022, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET992+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.108, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET970+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 8.314, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SET_SET967+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.089, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET977+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.325, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN040+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.051, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN041+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.023, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN049+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.043, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN050+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN051+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN061+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.041, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN062+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.042, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET981+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 8.83, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN081+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.07, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN082+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN315+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET984+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.112, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SET_SET988+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.075, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN328+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.032, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN331+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.019, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN336+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.017, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN338+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN340+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.06, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN345+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.04, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET990+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.076, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN346+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.026, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN354+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.028, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN356+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.028, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN358+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.028, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN359+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.024, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN323+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.11, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN375+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.017, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN365+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.042, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN377+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN364+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.082, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN378+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.014, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN388+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.011, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN391+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.012, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN399+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.013, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN405+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN406+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN410+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.015, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN416+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.011, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN440+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.147, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN445+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.045, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN450+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.061, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET994+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.141, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN452+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.176, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN451+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.295, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN461+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.068, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN460+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.291, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN466+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.215, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN471+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.17, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN470+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.228, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN474+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.083, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN473+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.226, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN488+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.172, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN501+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.106, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN036+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 9.602, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN502+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.092, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SET_SET997+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.054, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN489+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.33, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN503+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.249, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN505+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.14, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN506+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.166, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN722+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.055, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN504+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.545, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN726+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.051, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN729+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.046, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN915+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN918+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.078, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN919+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.057, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN923+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.055, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN924+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.061, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN066+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.127, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN933+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.059, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN930+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.07, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN944+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.048, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN945+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.049, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN947+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.04, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN950+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.061, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN954+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.041, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN957+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.05, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN955+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.069, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN962+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.025, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN964+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.06, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN965+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.088, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN972+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.041, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN966+1.p", + "expected": "Theorem", + "z3_status": "CounterSatisfiable", + "elapsed": 0.194, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN973+1.p", + "expected": "Theorem", + "z3_status": "Theorem", + "elapsed": 0.175, + "timeout": false, + "exit_code": 0, + "stderr": "" + }, + { + "file": "SYN_SYN327+1.p", + "expected": "Theorem", + "z3_status": "Timeout", + "elapsed": 10.084, + "timeout": true, + "exit_code": -1, + "stderr": "" + }, + { + "file": "SYN_SYN381+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.189, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN548+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 5.807, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN376+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 7.959, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN723+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.186, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + }, + { + "file": "SYN_SYN550+1.p", + "expected": "Theorem", + "z3_status": "Error: terminate called after throwing an instance of 'z3_error'\n what(): timeout", + "elapsed": 6.709, + "timeout": true, + "exit_code": -6, + "stderr": "terminate called after throwing an instance of 'z3_error'\n what(): timeout" + } +] \ No newline at end of file