core-labs/core
core-labs/core
1
0
Fork 0
Code Issues 11 Pull requests 2 Projects Releases Packages Wiki Activity Actions 1

Merge pull request #549 from AssetOverflow/feat/deductive-logic-entailment

Browse source 
feat: sound+complete propositional entailment operator + deductive-logic lane (the pivot)
This commit is contained in:
Shay 2026-06-04 08:11:36 -07:00 committed by GitHub
commit cc885157a5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 1629 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

175
docs/analysis/pivot-to-deductive-logic-2026-06-04.md Normal file
View file

@ -0,0 +1,175 @@
<!-- CANONICAL | docs/analysis/pivot-to-deductive-logic-2026-06-04.md | 2026-06-04 | strategy/post-mortem | why we left the GSM8K chase, what went wrong, and the deductive-logic path we are now on | verified: holdout 500/500 wrong=0, 8000-case engine-vs-oracle fuzz 0 disagreements -->
# The pivot to deductive logic — what went wrong, and the path now
This is the load-bearing record of a strategic correction. It documents (1) the
GSM8K capability chase and exactly how it misled us for weeks, (2) the measurement
that exposed the truth, (3) why the terrain was wrong for CORE, and (4) the
deductive-logic direction we are now on, with the plan and the disciplines that keep
us honest. Read this before resuming capability work.
---
## 1. What we were doing, and what went wrong
**The goal:** lift CORE's GSM8K (grade-school math word problem) accuracy off zero
while holding the prime directive `wrong = 0` (refuse rather than confabulate).
**The mistake — a ruler that could not measure.** Development was scored on
`train_sample` — the **50 cases the grammar was hand-built against**. Tuning against
those 50 produced "lift" with **no predictive validity**: it was overfit to the exact
problems being optimised. Worse, it hid a real defect.
**The breach.** The first real **sealed** measurement (the full 1,319-case GSM8K test
split, decrypted and run by the operator, never read by Claude) showed serving was
**`0 correct / 5 WRONG / 1314 refused`** — a live `wrong = 0` **breach**. The five
wrong answers were `product_bridge` promoting the derivation composer's confabulations
to serving. This had been invisible *for weeks* behind the 50-case ruler, which
reported a clean `wrong = 0` the whole time.
**The cost.** Time and tokens were spent making the system *worse* (wiring an unsound
reader into serving) while believing it was improving, and the work was shown to
outside professionals as progress. That is the failure this document exists to prevent
recurring.
**Immediate remediation (done):** the unsound committing bridges (`product_bridge`,
`goal_residual`) were disabled; sealed re-confirmed `0 / 0 / 1319` — back to the honest
refusal floor with zero confabulation. Rule recorded in `docs/claims_ledger.md`: never
re-enable a committing bridge without sealed-proven `wrong = 0`.
---
## 2. The measurement that exposed the truth
We built the instrument we never had: a **held-out dev lane** — 500 real GSM8K
problems CORE was **not** built against (`evals/gsm8k_math/holdout_dev/`). One scorer,
three sets, same day:
| Set | correct | wrong | what it is |
|---|---:|---:|---|
| `train_sample` (50) | 4 | 0 | the data CORE was **built on** — overfit, no predictive validity |
| `holdout_dev` (500) | **0** | 0 | real GSM8K **never built-against** — the honest baseline |
| sealed test (1,319) | 0 | 0 | the final exam |
**Real GSM8K capability was 0%.** The four train "correct" generalised to *zero* of
500 held-out cases. Serving held `wrong = 0` only because it refused everything real.
**The deeper finding — the composer is *unsound*, not just narrow.** The derivation
composer (`resolve_pooled`), the reader the whole composition program was built around
as "`wrong=0`-safe", measured on held-out: **2 correct / 87 WRONG / 411 refused —
17% confabulation.** And no gate fixes it: characterising all 89 commits, *step count,
pool size, and op-sequence do not separate the 2 right from the 87 wrong.* The composer
**cannot distinguish its correct readings from its wrong ones** — so no principled gate
admits the right while refusing the wrong. (Full analysis:
`docs/analysis/real-gsm8k-capability-measurement-2026-06-04.md`.)
Four committing-reader lift attempts were built and **empirically falsified** on
held-out (not just argued): the composer (17% wrong), a maximally-narrow forced reader
(100% wrong when it fired), a strict sum-reader (100% wrong), and the sound
candidate-graph filter (built 0 admissible candidates — sound but constructs nothing).
**Shallow committing cannot be sound on real GSM8K**, because GSM8K problems that look
like "two numbers and a cue word" are almost always multi-step problems where the
shallow reading is wrong every time.
---
## 3. Why the terrain was wrong for CORE
GSM8K is **deliberately engineered** to require 2–8 step natural-language reasoning —
built to defeat exactly the pattern-matching we kept attempting. CORE is a
**deterministic, verifiable** engine; its strength is exact, inspectable, replayable
reasoning where a conclusion can be *checked*. GSM8K is the benchmark built *for*
stochastic multi-step LLM reasoning. **We were arm-wrestling a machine on its home
court.**
This is not a new realisation buried in the loss — it is CORE's own stated doctrine:
*"Next primitives = checkable-conclusion domains (logic / constraint / proof)."* The
GSM8K chase had drifted away from it.
---
## 4. The path now: deductive logic (checkable-conclusion terrain)
We pivoted the "sizeable numbers" goal to **deductive logic**, where the answer is
*verifiable by construction* — so capability can show real correct numbers, not just a
refusal floor, and `wrong = 0` is structural rather than aspirational.
**What this reuses (already paid for, previously zero-consumer):** the ADR-0201 ROBDD
propositional canonicalizer, the binding-graph DAG (ADR-0132), the proof_chain model /
builder / single-step modus ponens (ADR-0204/0205).
### Phase 1 — DONE (this PR)
A **sound and complete propositional entailment operator**
(`generate/proof_chain/entail.py`, ADR-0206) — the multi-hop inference operator
`evals/symbolic_logic/gaps.md` said did not exist and ADR-0205 deferred:
> premises ⊨ query iff `(⋀ premises) → query` is a tautology — an exact ROBDD check.
Outcomes: `entailed` / `refuted` / `unknown` / `refused` (inconsistent or
out-of-decidable-regime). `wrong = 0` is structural; quantified/predicate input refuses
by design (propositional regime only).
**Measured, honestly:**
| set | n | correct | wrong | non-trivial (entailed+refuted) |
|---|---:|---:|---:|---:|
| dev | 200 | 200 | **0** | 74 |
| **holdout v1** | 500 | **500** | **0** | **227** |
| fuzz (fresh random, engine vs **independent** oracle) | 7,340 | 7,340 | **0** | 3,360 |
The gold is computed by an **independent truth-table oracle**
(`evals/deductive_logic/oracle.py`) sharing **no code** with the ROBDD engine.
**8,000 fresh random problems, two independent sound decision procedures, zero
disagreements** — the soundness evidence the GSM8K composer could never produce.
**Honest caveat (state it plainly):** propositional validity is *decidable*, so 100%
is the expected ceiling for a correct implementation. The value is not "solved
something unsolved" — it is (a) CORE's first real, non-zero, **independently-verified**
capability (not a refusal floor), (b) the honest foundation the harder layers build on,
(c) it is on CORE's terrain. External framing: *"CORE performs sound, complete,
deterministic deductive inference — multi-hop entailment and refutation — verified
`wrong = 0` against an independent oracle on held-out data."*
### Phases 2–4 — the plan
2. **Scale + recognizable benchmark.** Harder/deeper held-out sets; a grounded
**RuleTaker / ProofWriter** mirror (finite-entity rules ground to propositional) →
a number on a *published, recognizable* benchmark, same `wrong = 0` discipline.
3. **NL→logic grounding.** Read English logic problems into formulas. This is where it
becomes externally impressive — and where the GSM8K natural-language rake lives, so
it is measured the same disciplined way (held-out + independent gold) and refuses
what it cannot ground.
4. **Serving.** Wire the operator into `chat/runtime` so CORE answers deductive queries
to users, gated by the same `wrong = 0` discipline (and, for any serving promotion,
the sealed-confirmation rule from §1).
---
## 5. Disciplines carried forward (the anti-recurrence rules)
1. **Never score capability on data the system was built against.** Every capability
claim is measured on held-out data + confirmed on a sealed/independent arbiter.
No `train_sample`-class ruler is ever the score again.
2. **Gold must be independent of the system under test.** A held-out lane uses an
independent oracle (or sealed operator-run gold), never the engine's own output.
3. **`wrong = 0` is a floor, not a result.** "Refuses everything" is the *failing*
baseline. The capability claim is *coverage with* `wrong = 0`.
4. **No serving promotion without sealed/independent-proven `wrong = 0`.** The
product_bridge breach is the standing reason.
5. **Falsify lift attempts empirically, on held-out, before trusting them.** Build the
reader, measure it on data it was not tuned to, and report what it actually does —
including the failures.
6. **Prefer checkable-conclusion terrain.** Where the answer is verifiable, capability
is honest and `wrong = 0` is structural. That is where CORE competes.
---
## Reproduce
```bash
PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.runner # dev + holdout; exits 1 if wrong>0
PYTHONPATH=. .venv/bin/python -m pytest tests/test_deductive_logic_entail.py -q
# GSM8K honest baseline (context for the pivot):
PYTHONPATH=. .venv/bin/python -m evals.gsm8k_math.holdout_dev.v1.runner # the held-out instrument
```

1
evals/deductive_logic/__init__.py Normal file
View file

@ -0,0 +1 @@
"""Deductive-logic eval lane (ADR-0206): sound+complete propositional entailment."""

88
evals/deductive_logic/contract.md Normal file
View file

@ -0,0 +1,88 @@
<!-- CANONICAL | evals/deductive_logic/contract.md | 2026-06-04 | deductive-logic lane | what CORE's propositional entailment operator decides, and its honesty boundary | verified: holdout 500/500 correct wrong=0, 8000-case engine-vs-oracle fuzz 0 disagreements -->
# deductive-logic eval lane (ADR-0206)
## What it measures — and why it is honest
CORE's **deterministic propositional entailment operator**
(`generate.proof_chain.entail.evaluate_entailment`): given premise formulas and a
query formula, does the premise set **entail**, **refute**, or **leave undetermined**
the query — or is the input outside the decidable regime?
This is the inference operator `evals/symbolic_logic/gaps.md` asked for ("no operator
that takes A→B, B→C and returns A→C") and ADR-0205 deferred. It is built directly on
the ADR-0201 ROBDD canonicalizer, so it is **sound and complete** for propositional
logic, not single-step:
> premises ⊨ query iff `(⋀ premises) → query` is a tautology (an exact ROBDD check).
Unlike the GSM8K lanes, capability here can show **real correct numbers** because the
answer is *checkable*: this is the terrain CORE was built for (exact, verifiable,
deterministic), not the multi-step natural-language arithmetic GSM8K is engineered to
make stochastic.
## The numbers (2026-06-04)
| Set | n | correct | wrong | of which non-trivial (entailed + refuted) |
|---|---:|---:|---:|---:|
| dev | 200 | 200 | **0** | 74 |
| **holdout v1** | 500 | **500** | **0** | **227** (117 entailed + 110 refuted) |
| fuzz (fresh random, engine vs oracle) | 7,340 | 7,340 | **0** | 3,360 |
**100% correct with `wrong = 0`**, and the correct answers include hundreds of
non-trivial multi-hop entailments and refutations — not just `unknown` pass-throughs.
## Why the gold is trustworthy (the GSM8K lesson applied)
The gold is **not** computed by the engine under test. It comes from an *independent*
truth-table decision procedure (`oracle.py`): a separate parser + brute-force model
enumeration over all 2^k assignments, sharing **no code** with the ROBDD engine. Two
independently-coded sound procedures agreeing on **8,000** fresh random problems with
**zero disagreements** is real soundness evidence — exactly the property the GSM8K
composer could never establish (it could not tell its 2 right answers from its 87
wrong ones). A single engine/oracle disagreement fails the test suite.
## Honesty boundary (load-bearing — do not overclaim)
- **Propositional only.** Atoms are opaque Boolean variables. Quantified / predicate
input (`forall x. P(x)`, `rough(x)`) is **out of regime** and refuses (typed,
by design — ADR-0201.1), never guessed. A finite-entity problem *grounded* to
per-(entity,predicate) atoms is propositional and in scope; an ungrounded
first-order rule is not.
- **This is given formulas, not natural language.** The operator decides logic; it
does not yet *read* English word-problems into logic. NL→formula grounding is a
separate, later layer (and the place the GSM8K rake lives — kept out of scope here
deliberately).
- **`wrong = 0` is the floor, not a bragging point.** It is structural (an exact
tautology check refuses rather than approximates). The capability claim is the
*coverage with* `wrong=0`: hundreds of correct non-trivial deductions on held-out
data, independently verified.
## Outcomes (closed vocabulary)
| outcome | meaning |
|---|---|
| `entailed` | `(⋀P) → Q` is a tautology — Q holds in every model of the premises |
| `refuted` | `(⋀P) → ¬Q` is a tautology — Q fails in every model |
| `unknown` | neither — Q is true in some premise-models and false in others |
| `refused` | premises inconsistent (no model) **or** malformed / out-of-regime |
## Run
```bash
PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.runner # dev + holdout, exits 1 if wrong>0
PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.generate # regenerate committed cases (deterministic)
PYTHONPATH=. .venv/bin/python -m pytest tests/test_deductive_logic_entail.py -q
```
## Data layout
```
evals/deductive_logic/
contract.md
oracle.py # independent truth-table gold (no shared code with the engine)
generate.py # deterministic, seeded; gold from oracle
runner.py # engine vs gold; correct/wrong/refused + class breakdown
dev/cases.jsonl # seed 20260604, 200 cases
holdout/v1/cases.jsonl # seed 70260604, 500 cases (disjoint)
```

200
evals/deductive_logic/dev/cases.jsonl Normal file
View file

@ -0,0 +1,200 @@
{"gold": "unknown", "id": "dl-dev-v1-0000", "premises": ["e", "(~b & f) -> c", "(a & ~d) -> ~g", "(g & ~b) -> g", "(~g & ~b) -> ~a", "(c) -> e"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0001", "premises": ["~b", "(e) -> ~f", "(~g & a) -> g", "(e & a) -> b", "(b & e) -> ~e"], "query": "e"}
{"gold": "refuted", "id": "dl-dev-v1-0002", "premises": ["~d", "(~d & ~e) -> d", "(a) -> d", "(d) -> c", "(~a) -> ~d", "(c & ~e) -> c"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0003", "premises": ["~a", "(~g) -> d", "(~e & d) -> ~f", "(~b & ~g) -> ~f", "(a) -> c", "(~b & ~f) -> g"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0004", "premises": ["~c", "~g", "b", "(~d) -> ~g", "(b) -> f"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0005", "premises": ["e", "~f", "d", "(~a & ~f) -> ~a", "(~b) -> b", "(d & ~e) -> e", "(~e) -> d"], "query": "a"}
{"gold": "entailed", "id": "dl-dev-v1-0006", "premises": ["~e", "b", "(~c & ~f) -> e", "(~c) -> ~a"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0007", "premises": ["~a", "~g", "(e & d) -> ~c", "(e & d) -> ~f", "(~d) -> d", "(e & ~a) -> e", "(~a & c) -> ~g"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0008", "premises": ["~a", "(b) -> ~f", "(b) -> c"], "query": "~f"}
{"gold": "refuted", "id": "dl-dev-v1-0009", "premises": ["c", "~d", "(f) -> f", "(~c & ~d) -> c", "(~c & ~d) -> f", "(g) -> ~c", "(~d) -> f"], "query": "~f"}
{"gold": "entailed", "id": "dl-dev-v1-0010", "premises": ["c", "~g", "(g & c) -> g", "(b) -> ~c", "(~c & b) -> ~g", "(g) -> ~c"], "query": "c"}
{"gold": "refuted", "id": "dl-dev-v1-0011", "premises": ["d", "~c", "(c) -> d", "(~f & a) -> ~d", "(f & a) -> f", "(f & a) -> ~c"], "query": "~d"}
{"gold": "entailed", "id": "dl-dev-v1-0012", "premises": ["~g", "d", "~b", "(b) -> ~g", "(~e) -> ~c"], "query": "~b"}
{"gold": "refuted", "id": "dl-dev-v1-0013", "premises": ["b", "a", "(e) -> e", "(~b & f) -> b", "(~e) -> d"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0014", "premises": ["a", "~e", "(f) -> c", "(c & f) -> a"], "query": "~c"}
{"gold": "entailed", "id": "dl-dev-v1-0015", "premises": ["~e", "(~b) -> e", "(b) -> ~e"], "query": "~e"}
{"gold": "entailed", "id": "dl-dev-v1-0016", "premises": ["g", "~b", "(~d) -> ~g", "(a & e) -> b", "(e & f) -> c", "(~d) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0017", "premises": ["~f", "~b", "(~d & c) -> ~a", "(d & c) -> a", "(~c & f) -> ~c", "(~f & b) -> ~d"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0018", "premises": ["~a", "(b) -> g", "(g) -> b", "(g & a) -> ~a"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0019", "premises": ["~f", "(d & ~f) -> a", "(c) -> b"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0020", "premises": ["a", "d", "b", "(~f & c) -> ~d", "(~f & ~b) -> ~b", "(~b & f) -> ~e"], "query": "e"}
{"gold": "entailed", "id": "dl-dev-v1-0021", "premises": ["b", "e", "(~e & b) -> ~b", "(~b & ~f) -> ~f", "(a & ~f) -> ~f", "(a) -> ~b", "(~f) -> a"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0022", "premises": ["a", "~e", "(~c) -> ~f", "(a & f) -> ~g", "(c & ~f) -> e", "(a) -> a"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0023", "premises": ["~g", "f", "~c", "(~b & ~d) -> a", "(~c & ~a) -> g", "(e) -> c"], "query": "~b"}
{"gold": "refuted", "id": "dl-dev-v1-0024", "premises": ["d", "c", "(d) -> ~a", "(~b & a) -> ~g"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0025", "premises": ["~f", "(~f & b) -> c", "(a) -> a", "(c & f) -> ~b", "(~b & c) -> b"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0026", "premises": ["~e", "(~a) -> ~a", "(c) -> ~d", "(~d) -> ~c"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0027", "premises": ["~e", "~d", "(f) -> ~b", "(~d) -> ~e", "(e & ~c) -> ~d", "(b) -> f"], "query": "c"}
{"gold": "refuted", "id": "dl-dev-v1-0028", "premises": ["~g", "(~f & ~d) -> c", "(~c) -> f", "(~f & ~g) -> c"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0029", "premises": ["a", "(e & ~b) -> g", "(a) -> e", "(e & ~g) -> a"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0030", "premises": ["b", "g", "(~e & ~c) -> b", "(~a) -> ~e", "(~f) -> ~f", "(b & ~c) -> f"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0031", "premises": ["e", "(g) -> d", "(g) -> ~f", "(e & b) -> f", "(~e) -> ~d", "(b & g) -> ~c"], "query": "b"}
{"gold": "entailed", "id": "dl-dev-v1-0032", "premises": ["e", "~c", "~f", "(g & ~d) -> ~c", "(~g & c) -> f", "(~c) -> ~f", "(~g) -> ~d", "(~a & ~f) -> a"], "query": "a"}
{"gold": "entailed", "id": "dl-dev-v1-0033", "premises": ["~b", "~g", "(g) -> b", "(~d & g) -> ~e"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0034", "premises": ["~d", "b", "(~c) -> g", "(~g) -> ~c"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0035", "premises": ["d", "(~g & ~e) -> ~b", "(~e) -> d"], "query": "~g"}
{"gold": "entailed", "id": "dl-dev-v1-0036", "premises": ["d", "(~c) -> ~d", "(~d) -> ~d"], "query": "c"}
{"gold": "refuted", "id": "dl-dev-v1-0037", "premises": ["~g", "~e", "(c & ~g) -> e", "(~e & ~g) -> ~g", "(d & b) -> f"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0038", "premises": ["g", "(~b & e) -> f", "(~g) -> e", "(c & g) -> e", "(e & ~g) -> c", "(b) -> ~f"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0039", "premises": ["~b", "(b) -> ~e", "(~b) -> g", "(~b & f) -> ~g"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0040", "premises": ["~d", "(b & ~d) -> ~f", "(~d) -> b"], "query": "~a"}
{"gold": "refuted", "id": "dl-dev-v1-0041", "premises": ["~e", "a", "~g", "(~c & f) -> e", "(~e & ~f) -> c", "(~c & f) -> ~d"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0042", "premises": ["~d", "(~a & g) -> ~f", "(~g & c) -> ~a", "(~d & g) -> f"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0043", "premises": ["e", "~d", "(g) -> ~g", "(~b & a) -> ~g", "(a & ~b) -> ~e"], "query": "a"}
{"gold": "entailed", "id": "dl-dev-v1-0044", "premises": ["~b", "~c", "a", "(c & ~d) -> ~d", "(a & ~d) -> ~c"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0045", "premises": ["~b", "(e & d) -> ~g", "(b & d) -> ~b"], "query": "~e"}
{"gold": "refuted", "id": "dl-dev-v1-0046", "premises": ["c", "e", "(~c) -> ~d", "(d & e) -> e", "(c & ~d) -> ~c", "(d & ~f) -> d", "(e & b) -> ~e"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0047", "premises": ["~a", "(c & ~b) -> e", "(e) -> ~g"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0048", "premises": ["a", "~c", "(a & b) -> ~a", "(~b & e) -> ~b", "(d) -> d"], "query": "~d"}
{"gold": "refuted", "id": "dl-dev-v1-0049", "premises": ["~b", "(~d) -> ~c", "(b) -> ~c", "(d & ~f) -> ~c", "(~b & c) -> ~f", "(~f & ~c) -> b"], "query": "~f"}
{"gold": "unknown", "id": "dl-dev-v1-0050", "premises": ["~a", "g", "(~a) -> f", "(~f & ~a) -> a", "(g & ~f) -> ~a"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0051", "premises": ["g", "(b & d) -> ~f", "(a) -> ~c", "(~b & ~f) -> ~g"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0052", "premises": ["f", "~g", "(~e & ~d) -> ~e", "(~g & ~b) -> e", "(b & ~e) -> ~d", "(~f) -> g", "(c & ~d) -> ~f"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0053", "premises": ["~b", "c", "(g & b) -> a", "(a & e) -> g", "(c & ~f) -> ~b"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0054", "premises": ["~c", "(~g & ~a) -> ~c", "(e) -> e", "(b) -> ~f", "(g & a) -> ~c", "(g & c) -> ~b"], "query": "f"}
{"gold": "unknown", "id": "dl-dev-v1-0055", "premises": ["b", "d", "e", "(~a) -> a", "(e) -> a", "(a & d) -> d"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0056", "premises": ["~c", "(c) -> ~e", "(d & e) -> ~g", "(f & ~g) -> f"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0057", "premises": ["f", "b", "(g) -> d", "(c & e) -> ~c", "(~d) -> e"], "query": "~g"}
{"gold": "entailed", "id": "dl-dev-v1-0058", "premises": ["f", "~g", "~b", "(b & e) -> g", "(~a & e) -> ~c", "(~c) -> c", "(~b & ~f) -> ~g"], "query": "c"}
{"gold": "refuted", "id": "dl-dev-v1-0059", "premises": ["~d", "~g", "(g & c) -> e", "(~g) -> ~e", "(g & e) -> e", "(e) -> ~d", "(~b) -> ~g"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0060", "premises": ["f", "(g) -> a", "(~c & ~d) -> ~g", "(e) -> ~d", "(a & g) -> e"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0061", "premises": ["a", "~g", "(~f & ~b) -> g", "(~g) -> d", "(a & b) -> a", "(~d) -> ~a"], "query": "f"}
{"gold": "entailed", "id": "dl-dev-v1-0062", "premises": ["f", "~d", "(a & ~f) -> ~a", "(~d) -> ~e", "(a & f) -> ~e", "(d & c) -> ~a", "(e) -> ~f"], "query": "~e"}
{"gold": "refuted", "id": "dl-dev-v1-0063", "premises": ["d", "(~a & d) -> ~a", "(~a & e) -> ~e"], "query": "~d"}
{"gold": "entailed", "id": "dl-dev-v1-0064", "premises": ["f", "e", "(c & ~f) -> f", "(b) -> d", "(~c) -> ~e", "(e & c) -> ~d"], "query": "e"}
{"gold": "entailed", "id": "dl-dev-v1-0065", "premises": ["e", "c", "(d) -> ~c", "(d) -> a", "(e & ~c) -> ~c", "(~c) -> ~d", "(e) -> ~d"], "query": "e"}
{"gold": "refuted", "id": "dl-dev-v1-0066", "premises": ["~d", "b", "(b & d) -> ~d", "(c & g) -> d", "(d) -> d", "(~b) -> ~g", "(d & c) -> ~g"], "query": "d"}
{"gold": "entailed", "id": "dl-dev-v1-0067", "premises": ["b", "a", "~f", "(~b & ~e) -> a", "(c) -> ~a", "(~e) -> ~c", "(d & ~g) -> e"], "query": "~f"}
{"gold": "entailed", "id": "dl-dev-v1-0068", "premises": ["~b", "~d", "e", "(~e & ~a) -> e", "(~c) -> c"], "query": "~b"}
{"gold": "entailed", "id": "dl-dev-v1-0069", "premises": ["d", "f", "~g", "(e) -> ~a", "(d) -> ~e"], "query": "d"}
{"gold": "entailed", "id": "dl-dev-v1-0070", "premises": ["a", "~g", "(~c) -> ~d", "(g & e) -> ~g", "(~c & ~e) -> ~c"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0071", "premises": ["~c", "f", "(~c) -> ~b", "(c) -> ~e", "(e & ~b) -> ~c", "(~f) -> c", "(e) -> ~c"], "query": "~f"}
{"gold": "unknown", "id": "dl-dev-v1-0072", "premises": ["~d", "(~a) -> ~c", "(c) -> e", "(~c) -> ~d", "(~a & e) -> ~a", "(~e & a) -> e"], "query": "a"}
{"gold": "refuted", "id": "dl-dev-v1-0073", "premises": ["~g", "~d", "(~d & e) -> c", "(~d) -> ~b", "(~g) -> ~f", "(~d & c) -> b"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0074", "premises": ["e", "(e & ~g) -> g", "(~a) -> c"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0075", "premises": ["e", "c", "a", "(d & ~c) -> c", "(e) -> ~g"], "query": "b"}
{"gold": "entailed", "id": "dl-dev-v1-0076", "premises": ["a", "~c", "~e", "(g) -> ~a", "(~g & ~f) -> e", "(~d) -> ~g", "(~e & g) -> ~a"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0077", "premises": ["~f", "(g & ~f) -> ~d", "(f & e) -> ~d", "(e & a) -> ~c"], "query": "f"}
{"gold": "entailed", "id": "dl-dev-v1-0078", "premises": ["f", "~c", "(d & a) -> a", "(~g) -> ~c", "(~g & ~f) -> ~g"], "query": "f"}
{"gold": "refuted", "id": "dl-dev-v1-0079", "premises": ["~b", "(b & c) -> ~d", "(c) -> b", "(b) -> e"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0080", "premises": ["g", "(g & f) -> f", "(~e & c) -> ~f", "(~e) -> e"], "query": "f"}
{"gold": "unknown", "id": "dl-dev-v1-0081", "premises": ["~f", "(a) -> ~d", "(d) -> ~c", "(f) -> d", "(~b) -> ~c", "(b & ~a) -> d"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0082", "premises": ["~f", "~b", "~g", "(b & ~e) -> g", "(~d) -> d", "(~c & ~b) -> ~g", "(~a & b) -> ~g"], "query": "~e"}
{"gold": "refuted", "id": "dl-dev-v1-0083", "premises": ["f", "(~a) -> f", "(~g) -> g"], "query": "~f"}
{"gold": "entailed", "id": "dl-dev-v1-0084", "premises": ["g", "b", "f", "(e & ~a) -> ~c", "(d) -> a"], "query": "b"}
{"gold": "refuted", "id": "dl-dev-v1-0085", "premises": ["b", "~e", "(~a) -> ~d", "(~a) -> ~d", "(~a & ~b) -> d", "(~b) -> ~e"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0086", "premises": ["~g", "b", "(g) -> e", "(~b & ~d) -> ~b"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0087", "premises": ["~d", "(d & ~a) -> b", "(a & ~b) -> b", "(~c) -> c"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0088", "premises": ["b", "f", "g", "(~a & e) -> ~b", "(~b & a) -> g", "(~d) -> ~b", "(~g & ~d) -> a", "(b & e) -> ~e"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0089", "premises": ["~a", "(~b) -> ~f", "(c & b) -> f", "(~g) -> e", "(~b) -> a"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0090", "premises": ["c", "~d", "(c) -> ~d", "(a) -> ~b", "(~d & ~f) -> ~b", "(f & ~c) -> ~c"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0091", "premises": ["~g", "(~c) -> f", "(~d) -> ~f", "(~c) -> f", "(g & ~f) -> f"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0092", "premises": ["~b", "f", "(~a) -> ~b", "(a) -> e", "(e) -> e", "(b) -> ~c", "(c) -> ~e"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0093", "premises": ["~c", "(d) -> ~a", "(d & e) -> c", "(~a) -> ~b"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0094", "premises": ["g", "(f) -> ~e", "(d) -> ~b", "(b & ~f) -> ~g", "(g & ~f) -> c", "(d) -> ~d"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0095", "premises": ["~g", "f", "(d) -> g", "(~e) -> d", "(~f & ~g) -> ~g", "(f & g) -> a"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0096", "premises": ["~e", "(~e & ~c) -> d", "(~d & ~c) -> e", "(f & e) -> f", "(~f) -> ~d", "(d & c) -> ~d"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0097", "premises": ["~b", "a", "(~f) -> ~a", "(~f & ~e) -> a", "(~b & ~f) -> e", "(a & d) -> ~b"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0098", "premises": ["~c", "(~c & g) -> ~g", "(g) -> c", "(~g & f) -> f"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0099", "premises": ["~e", "~g", "(~f & ~e) -> ~f", "(~f & g) -> ~f"], "query": "~a"}
{"gold": "refuted", "id": "dl-dev-v1-0100", "premises": ["~f", "~c", "(d) -> f", "(d) -> e", "(d & f) -> ~f", "(e) -> e"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0101", "premises": ["a", "(a) -> g", "(~e & ~d) -> ~c", "(~g & c) -> ~g", "(~b & a) -> ~e"], "query": "b"}
{"gold": "entailed", "id": "dl-dev-v1-0102", "premises": ["~a", "(~a) -> ~b", "(~b & a) -> b"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0103", "premises": ["~d", "(a) -> ~b", "(g) -> g"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0104", "premises": ["~b", "~c", "(~b & ~c) -> ~e", "(b) -> ~c", "(~b & ~f) -> b", "(g) -> f"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0105", "premises": ["e", "~f", "~g", "(c) -> ~g", "(b & g) -> ~a", "(~a) -> g"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0106", "premises": ["~d", "a", "e", "(~a & d) -> b", "(f & a) -> ~b", "(~b) -> ~e", "(~e & ~f) -> ~e", "(c & ~a) -> d"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0107", "premises": ["~d", "g", "(g & d) -> f", "(d & b) -> f", "(~d & ~b) -> d"], "query": "f"}
{"gold": "unknown", "id": "dl-dev-v1-0108", "premises": ["~c", "~b", "(c) -> g", "(~f & ~a) -> ~c"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0109", "premises": ["~g", "(~b & ~e) -> a", "(~e & a) -> ~c", "(~b & c) -> b"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0110", "premises": ["d", "~g", "(~g & ~d) -> g", "(~g & ~d) -> ~e", "(g & ~b) -> d"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0111", "premises": ["~c", "~f", "(c) -> f", "(~d) -> d", "(~c & a) -> ~g", "(~d & ~c) -> b", "(~b) -> ~d"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0112", "premises": ["e", "g", "(g) -> d", "(~d & g) -> ~g", "(g & ~d) -> ~d", "(d & ~e) -> e"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0113", "premises": ["~g", "(~f) -> g", "(g) -> ~g", "(~f & ~c) -> ~b", "(g & ~b) -> e", "(b) -> b"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0114", "premises": ["~g", "(~b & c) -> c", "(~c & ~d) -> ~b", "(~b) -> ~c", "(~b & g) -> ~g", "(c & ~b) -> ~e"], "query": "e"}
{"gold": "entailed", "id": "dl-dev-v1-0115", "premises": ["~d", "(g) -> d", "(e & ~a) -> ~a"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0116", "premises": ["g", "~c", "~e", "(~g) -> ~e", "(b & f) -> ~b", "(e) -> e", "(~c) -> g"], "query": "c"}
{"gold": "entailed", "id": "dl-dev-v1-0117", "premises": ["~c", "e", "(~b & e) -> c", "(b) -> d", "(~e) -> ~e", "(~c) -> d"], "query": "d"}
{"gold": "refuted", "id": "dl-dev-v1-0118", "premises": ["~d", "c", "e", "(d) -> ~c", "(f) -> ~e", "(f) -> ~d", "(~g & e) -> ~e", "(~d) -> ~d"], "query": "f"}
{"gold": "refuted", "id": "dl-dev-v1-0119", "premises": ["c", "d", "b", "(~e & f) -> ~d", "(~c & ~g) -> ~d"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0120", "premises": ["f", "e", "(~b & ~f) -> ~d", "(d & e) -> b", "(~b & ~d) -> f", "(~b & e) -> e"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0121", "premises": ["~e", "(~e & f) -> ~e", "(f & a) -> ~g", "(a) -> g", "(~c) -> ~a", "(d & ~g) -> b"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0122", "premises": ["b", "(~b) -> ~g", "(e) -> d", "(b & ~f) -> ~g", "(b & c) -> f", "(~c & ~e) -> b"], "query": "~d"}
{"gold": "entailed", "id": "dl-dev-v1-0123", "premises": ["~a", "(a & f) -> ~e", "(e) -> ~d"], "query": "~a"}
{"gold": "entailed", "id": "dl-dev-v1-0124", "premises": ["e", "a", "(~e & ~g) -> ~g", "(~c & a) -> e", "(~e) -> ~b"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0125", "premises": ["b", "~e", "a", "(e & f) -> b", "(~c) -> f"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0126", "premises": ["d", "(~f & c) -> d", "(~c) -> a", "(~c) -> ~f"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0127", "premises": ["b", "e", "(~a) -> ~d", "(~b) -> ~b"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0128", "premises": ["c", "~g", "~f", "(~e & ~a) -> a", "(~d & ~f) -> ~c", "(g) -> b", "(d) -> ~e", "(e & ~d) -> g"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0129", "premises": ["g", "(f & ~c) -> ~g", "(~a & c) -> ~a"], "query": "~b"}
{"gold": "entailed", "id": "dl-dev-v1-0130", "premises": ["a", "~c", "(~d) -> a", "(b) -> ~f", "(a) -> ~d", "(d & ~f) -> a", "(~d & b) -> c"], "query": "~c"}
{"gold": "refuted", "id": "dl-dev-v1-0131", "premises": ["d", "~b", "(d & f) -> ~f", "(~b & f) -> ~b", "(~b & f) -> f"], "query": "~d"}
{"gold": "refuted", "id": "dl-dev-v1-0132", "premises": ["g", "c", "(~c) -> e", "(~c & ~e) -> d", "(c) -> ~d", "(g) -> e"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0133", "premises": ["~f", "b", "d", "(f) -> b", "(d & ~a) -> d"], "query": "~g"}
{"gold": "refuted", "id": "dl-dev-v1-0134", "premises": ["c", "(c & b) -> ~b", "(~b) -> c", "(~d) -> a"], "query": "b"}
{"gold": "entailed", "id": "dl-dev-v1-0135", "premises": ["~a", "(d) -> ~g", "(g & ~a) -> ~c", "(~c & e) -> ~d", "(g & ~d) -> d"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0136", "premises": ["d", "(~g) -> f", "(~a) -> ~a", "(~d & ~a) -> e", "(~d) -> d"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0137", "premises": ["~e", "b", "(~d & a) -> ~g", "(a) -> ~g", "(e & ~f) -> ~d", "(g & e) -> g", "(~f & ~a) -> ~e"], "query": "f"}
{"gold": "entailed", "id": "dl-dev-v1-0138", "premises": ["d", "(~c) -> a", "(~a) -> ~d", "(~c & ~a) -> c"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0139", "premises": ["d", "(~g) -> ~f", "(~b) -> ~c", "(~f) -> ~e", "(c) -> ~g"], "query": "g"}
{"gold": "unknown", "id": "dl-dev-v1-0140", "premises": ["f", "~b", "(c) -> f", "(~a) -> ~d", "(~g) -> ~e", "(~g & b) -> d"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0141", "premises": ["~c", "(~c) -> ~f", "(~c & b) -> g", "(e & b) -> c", "(b) -> c", "(~f & ~g) -> e"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0142", "premises": ["~c", "~g", "(~c) -> ~c", "(~c & f) -> ~d", "(f) -> ~c"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0143", "premises": ["d", "e", "(~b) -> a", "(c & ~a) -> ~b", "(d & ~c) -> ~c"], "query": "a"}
{"gold": "entailed", "id": "dl-dev-v1-0144", "premises": ["c", "(~g) -> d", "(c) -> ~d"], "query": "~d"}
{"gold": "refuted", "id": "dl-dev-v1-0145", "premises": ["~g", "e", "(g) -> ~e", "(~g & ~f) -> g", "(b & a) -> b", "(~f & e) -> e", "(~b & f) -> b"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0146", "premises": ["c", "e", "(~a) -> d", "(c & b) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0147", "premises": ["g", "d", "(~f & e) -> e", "(~a & e) -> ~a"], "query": "~e"}
{"gold": "refuted", "id": "dl-dev-v1-0148", "premises": ["~c", "~b", "d", "(~f) -> ~d", "(d) -> e", "(~g) -> ~e", "(~f) -> ~c"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0149", "premises": ["~g", "d", "f", "(d & f) -> ~e", "(~c & g) -> ~f", "(~f & e) -> ~b", "(~c) -> ~e"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0150", "premises": ["b", "(e & d) -> f", "(~d) -> ~c"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0151", "premises": ["c", "(~e) -> d", "(~e & g) -> ~d", "(a & e) -> b", "(~a) -> a"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0152", "premises": ["~a", "(e & ~d) -> ~e", "(~d) -> f", "(~a & ~b) -> b"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0153", "premises": ["~a", "(~c) -> ~f", "(~d & ~f) -> d", "(~a) -> c", "(~a & f) -> c"], "query": "~d"}
{"gold": "refuted", "id": "dl-dev-v1-0154", "premises": ["g", "~c", "(c) -> a", "(g) -> f", "(c) -> ~a", "(~g) -> g"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0155", "premises": ["~e", "(a & ~g) -> a", "(~e & ~b) -> ~d", "(~b & ~a) -> ~e"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0156", "premises": ["~c", "(~e & a) -> ~a", "(f & a) -> ~g", "(~b) -> ~c"], "query": "~a"}
{"gold": "unknown", "id": "dl-dev-v1-0157", "premises": ["b", "c", "(~c & ~d) -> ~e", "(b & d) -> b", "(~e) -> f", "(d & c) -> ~e", "(~e & ~b) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0158", "premises": ["~b", "(g) -> f", "(~g) -> a", "(~b) -> a", "(~g) -> ~b"], "query": "e"}
{"gold": "refuted", "id": "dl-dev-v1-0159", "premises": ["a", "e", "(~c & f) -> e", "(~b & ~f) -> f", "(~f & e) -> a"], "query": "~e"}
{"gold": "refuted", "id": "dl-dev-v1-0160", "premises": ["g", "b", "(a) -> a", "(~e & a) -> e", "(g) -> a", "(a) -> e", "(~e) -> e"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0161", "premises": ["e", "~b", "a", "(~d) -> ~d", "(f & ~e) -> c", "(d) -> ~a", "(~c & b) -> b", "(~a) -> ~a"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0162", "premises": ["e", "(~e & ~a) -> ~a", "(a & g) -> c", "(~g) -> ~g", "(~a & ~c) -> a", "(~g) -> c"], "query": "~g"}
{"gold": "unknown", "id": "dl-dev-v1-0163", "premises": ["c", "(d & a) -> ~f", "(~e) -> ~g"], "query": "~f"}
{"gold": "unknown", "id": "dl-dev-v1-0164", "premises": ["~a", "(~a) -> ~f", "(f) -> ~f", "(b) -> ~f", "(~f & c) -> ~b", "(b & ~f) -> ~a"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0165", "premises": ["b", "d", "(g) -> ~e", "(a & ~c) -> b"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0166", "premises": ["g", "(~e & ~a) -> e", "(e) -> ~a", "(g) -> g"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0167", "premises": ["b", "~d", "(~c & b) -> f", "(a) -> ~d", "(b) -> g"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0168", "premises": ["g", "e", "(c) -> f", "(~a) -> e"], "query": "~c"}
{"gold": "refuted", "id": "dl-dev-v1-0169", "premises": ["~f", "~d", "(~g) -> ~f", "(g) -> c", "(f & ~g) -> c"], "query": "d"}
{"gold": "entailed", "id": "dl-dev-v1-0170", "premises": ["~e", "(a) -> g", "(~a) -> a", "(e) -> c", "(~c) -> d", "(~g & f) -> ~g"], "query": "g"}
{"gold": "refuted", "id": "dl-dev-v1-0171", "premises": ["f", "~e", "~d", "(f & a) -> b", "(~e & ~g) -> a"], "query": "e"}
{"gold": "entailed", "id": "dl-dev-v1-0172", "premises": ["b", "~f", "(e) -> ~b", "(e) -> e"], "query": "b"}
{"gold": "entailed", "id": "dl-dev-v1-0173", "premises": ["b", "~f", "(~e & ~f) -> e", "(~f) -> ~a", "(e) -> e", "(~a) -> ~g", "(~b) -> a"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0174", "premises": ["~a", "(~c) -> ~d", "(~b) -> ~d", "(~f & ~g) -> a", "(~d) -> ~g", "(f & c) -> c"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0175", "premises": ["~g", "(~e & d) -> d", "(d) -> ~f", "(~g) -> ~g", "(~b & e) -> ~f", "(~g & ~c) -> ~a"], "query": "~c"}
{"gold": "unknown", "id": "dl-dev-v1-0176", "premises": ["~c", "~a", "(e & ~d) -> ~f", "(c) -> d", "(~e & d) -> g", "(e & ~c) -> d"], "query": "~f"}
{"gold": "entailed", "id": "dl-dev-v1-0177", "premises": ["~g", "(~f) -> f", "(g & ~b) -> a", "(~e & ~a) -> e", "(~e) -> e", "(a) -> f"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0178", "premises": ["a", "e", "d", "(e & f) -> f", "(~d) -> f", "(g & ~b) -> ~e", "(~f) -> ~e"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0179", "premises": ["f", "~a", "(a & ~e) -> ~f", "(~a & d) -> d"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0180", "premises": ["~d", "c", "(d) -> ~f", "(~g) -> ~f", "(~b & ~c) -> ~g"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0181", "premises": ["~d", "(~c & d) -> b", "(c) -> a", "(~b & ~f) -> c"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0182", "premises": ["g", "(g & f) -> ~f", "(a) -> f", "(f) -> ~e", "(a & g) -> a"], "query": "~b"}
{"gold": "unknown", "id": "dl-dev-v1-0183", "premises": ["a", "(~a) -> ~a", "(~d & ~a) -> ~d", "(~e) -> ~e", "(~b) -> b", "(f & c) -> b"], "query": "~d"}
{"gold": "unknown", "id": "dl-dev-v1-0184", "premises": ["~g", "(e) -> ~b", "(~e) -> ~e"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0185", "premises": ["~b", "(~a & ~b) -> ~g", "(~f & d) -> b", "(d) -> f"], "query": "~d"}
{"gold": "refuted", "id": "dl-dev-v1-0186", "premises": ["~d", "~f", "(~e) -> f", "(~a & e) -> ~d", "(f & d) -> ~d"], "query": "~e"}
{"gold": "unknown", "id": "dl-dev-v1-0187", "premises": ["d", "g", "~e", "(c) -> ~f", "(c & ~e) -> e"], "query": "b"}
{"gold": "unknown", "id": "dl-dev-v1-0188", "premises": ["d", "g", "~a", "(b & f) -> b", "(b) -> ~d"], "query": "~f"}
{"gold": "entailed", "id": "dl-dev-v1-0189", "premises": ["b", "c", "(~b) -> e", "(b & ~c) -> ~c", "(~f) -> e"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0190", "premises": ["b", "~d", "(f) -> f", "(d & ~g) -> g"], "query": "~e"}
{"gold": "entailed", "id": "dl-dev-v1-0191", "premises": ["e", "~b", "(g) -> ~g", "(~e) -> ~e"], "query": "e"}
{"gold": "unknown", "id": "dl-dev-v1-0192", "premises": ["~e", "(e & ~a) -> ~b", "(g) -> ~a", "(c & ~a) -> f", "(e & b) -> g"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0193", "premises": ["b", "(~a & ~g) -> ~a", "(f) -> ~a", "(~g & b) -> d", "(f & g) -> ~f"], "query": "d"}
{"gold": "unknown", "id": "dl-dev-v1-0194", "premises": ["a", "~d", "(~f) -> ~d", "(c & ~a) -> f", "(~a) -> ~c", "(a & f) -> ~c", "(~a) -> a"], "query": "~f"}
{"gold": "refuted", "id": "dl-dev-v1-0195", "premises": ["~c", "~a", "(c & a) -> f", "(~c & ~d) -> d"], "query": "c"}
{"gold": "unknown", "id": "dl-dev-v1-0196", "premises": ["d", "(c & ~b) -> ~f", "(~g & c) -> g", "(g) -> e", "(~e) -> ~a", "(a & ~e) -> ~b"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0197", "premises": ["~b", "(~a) -> ~a", "(e) -> e", "(~a & c) -> ~f", "(e) -> e"], "query": "a"}
{"gold": "unknown", "id": "dl-dev-v1-0198", "premises": ["~g", "(c & d) -> ~g", "(~c) -> ~f"], "query": "~d"}
{"gold": "entailed", "id": "dl-dev-v1-0199", "premises": ["~d", "e", "(~c) -> g", "(~d) -> ~g"], "query": "c"}

92
evals/deductive_logic/generate.py Normal file
View file

@ -0,0 +1,92 @@
"""Deterministic generator for the deductive-logic lane.
Produces RuleTaker-style propositional problems — base **facts** plus implication
**rules** (conjunctive antecedent → literal consequent) plus a literal **query** —
with the gold answer computed by the *independent* truth-table oracle
(:mod:`evals.deductive_logic.oracle`), never by the engine under test.
Determinism: a fixed-seed ``random.Random`` per split, so the committed
``cases.jsonl`` is exactly reproducible. Splits use disjoint seeds. Inconsistent
premise sets (oracle → ``refused``) are discarded, so every emitted case has a
definite ``entailed`` / ``refuted`` / ``unknown`` gold — the engine is scored on
producing the right *deduction*, with ``wrong=0`` as the floor.
Atom counts are kept small (≤ 7) so the oracle's 2^k enumeration is cheap and the
ROBDD never approaches its node budget.
"""
from __future__ import annotations
import json
import random
from pathlib import Path
from typing import Final
from evals.deductive_logic.oracle import REFUSED, oracle_entailment
_ATOMS: Final[tuple[str, ...]] = ("a", "b", "c", "d", "e", "f", "g")
def _literal(rng: random.Random, atom: str) -> str:
return atom if rng.random() < 0.5 else f"~{atom}"
def _make_case(rng: random.Random, case_id: str) -> dict | None:
k = rng.randint(4, len(_ATOMS))
atoms = rng.sample(_ATOMS, k)
premises: list[str] = []
# Base facts: assert a few literals (kept distinct atoms).
n_facts = rng.randint(1, max(1, k // 2))
fact_atoms = rng.sample(atoms, n_facts)
for at in fact_atoms:
premises.append(_literal(rng, at))
# Implication rules: (L1 & ... ) -> Lc. Bias antecedents toward earlier atoms
# and consequents toward later atoms so multi-hop chains form.
n_rules = rng.randint(2, 5)
for _ in range(n_rules):
body_size = rng.randint(1, 2)
body_atoms = rng.sample(atoms, min(body_size, k))
body = " & ".join(_literal(rng, at) for at in body_atoms)
head_atom = rng.choice(atoms)
head = _literal(rng, head_atom)
premises.append(f"({body}) -> {head}")
query = _literal(rng, rng.choice(atoms))
gold = oracle_entailment(tuple(premises), query)
if gold == REFUSED:
return None # inconsistent premises — discard; keep only definite golds
return {"id": case_id, "premises": premises, "query": query, "gold": gold}
def generate(seed: int, n: int, prefix: str) -> list[dict]:
"""Generate ``n`` consistent cases deterministically from ``seed``."""
rng = random.Random(seed)
cases: list[dict] = []
attempts = 0
while len(cases) < n:
attempts += 1
case = _make_case(rng, f"{prefix}-{len(cases):04d}")
if case is not None:
cases.append(case)
if attempts > n * 50: # pragma: no cover - safety valve
raise RuntimeError("generator could not reach target count")
return cases
def _write(path: Path, cases: list[dict]) -> None:
path.parent.mkdir(parents=True, exist_ok=True)
with path.open("w", encoding="utf-8") as fh:
for case in cases:
fh.write(json.dumps(case, ensure_ascii=False, sort_keys=True) + "\n")
if __name__ == "__main__":
root = Path(__file__).resolve().parent
_write(root / "dev" / "cases.jsonl", generate(20260604, 200, "dl-dev-v1"))
_write(root / "holdout" / "v1" / "cases.jsonl", generate(70260604, 500, "dl-holdout-v1"))
print("generated dev=200 holdout=500")

500
evals/deductive_logic/holdout/v1/cases.jsonl Normal file
View file

@ -0,0 +1,500 @@
{"gold": "unknown", "id": "dl-holdout-v1-0000", "premises": ["b", "a", "~g", "(e) -> a", "(b) -> ~d", "(g & d) -> ~g", "(e) -> ~b", "(g & a) -> b"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0001", "premises": ["d", "c", "(~b) -> d", "(b) -> ~c", "(~b & d) -> ~b"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0002", "premises": ["d", "(d) -> b", "(d) -> d", "(e) -> d"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0003", "premises": ["e", "~d", "b", "(c & ~f) -> d", "(c) -> c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0004", "premises": ["g", "(~g) -> d", "(~g & ~f) -> ~a", "(~e & a) -> ~b"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0005", "premises": ["f", "g", "c", "(~a & ~d) -> ~f", "(~d & g) -> ~c", "(~e & f) -> ~a", "(~f & a) -> a", "(b) -> ~a"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0006", "premises": ["a", "(~b & d) -> a", "(e & ~a) -> d", "(g) -> d", "(c) -> ~f", "(~d & ~c) -> ~b"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0007", "premises": ["~e", "(a & ~e) -> e", "(~g & ~e) -> a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0008", "premises": ["e", "(~e & ~d) -> d", "(~d) -> ~f", "(c) -> ~c"], "query": "~f"}
{"gold": "refuted", "id": "dl-holdout-v1-0009", "premises": ["g", "(a) -> ~e", "(a & ~e) -> g", "(g) -> a", "(~g & ~a) -> f"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0010", "premises": ["~e", "(d) -> e", "(~c & e) -> ~d", "(c & g) -> c"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0011", "premises": ["e", "~g", "(g) -> d", "(b) -> c", "(~f & ~g) -> ~e"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0012", "premises": ["c", "~a", "(b & g) -> ~c", "(f & d) -> f", "(a) -> a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0013", "premises": ["c", "(b) -> d", "(e & ~f) -> ~g"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0014", "premises": ["g", "(d) -> ~b", "(~c & f) -> c", "(c) -> ~c", "(c) -> g"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0015", "premises": ["f", "(~d & b) -> ~b", "(e) -> ~f"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0016", "premises": ["~g", "(~a) -> b", "(g & ~a) -> b", "(~g) -> a"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0017", "premises": ["~b", "(~c) -> ~f", "(f) -> ~g"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0018", "premises": ["c", "(d & ~b) -> d", "(f) -> ~c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0019", "premises": ["~d", "~a", "~g", "(~g) -> ~f", "(g & c) -> ~f"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0020", "premises": ["~b", "~g", "(e & b) -> a", "(~f) -> e", "(~c) -> a", "(c) -> e"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0021", "premises": ["f", "(~a & b) -> f", "(~e) -> b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0022", "premises": ["f", "a", "g", "(e & g) -> g", "(~a & f) -> d", "(~e) -> g", "(b) -> ~b"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0023", "premises": ["~e", "(d & ~f) -> ~c", "(~a) -> f"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0024", "premises": ["~b", "g", "(a) -> ~a", "(~f & ~b) -> ~f", "(~g) -> e"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0025", "premises": ["f", "(c) -> f", "(b & ~e) -> ~b", "(e) -> ~c", "(f & ~b) -> e"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0026", "premises": ["~c", "~f", "(b & ~c) -> c", "(~d & ~b) -> f", "(~f & ~d) -> c", "(f & ~d) -> ~c"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0027", "premises": ["e", "(e & ~d) -> a", "(d & a) -> d", "(~c) -> ~a", "(f & ~d) -> e"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0028", "premises": ["~b", "~c", "~f", "(f & e) -> f", "(~e) -> a", "(~g) -> ~c", "(d & ~b) -> ~c", "(e) -> ~g"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0029", "premises": ["e", "(~d & a) -> ~d", "(c) -> ~d", "(a & ~g) -> ~b", "(f & g) -> f"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0030", "premises": ["~c", "(~b & g) -> g", "(c & b) -> ~g", "(~a & ~f) -> d", "(d & ~e) -> e"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0031", "premises": ["g", "(c & ~b) -> g", "(~d) -> g", "(e) -> g"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0032", "premises": ["e", "a", "~g", "(~d) -> ~d", "(~c) -> ~b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0033", "premises": ["g", "f", "(d) -> d", "(~g & ~d) -> a", "(~g) -> ~a", "(~a & ~g) -> ~d"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0034", "premises": ["c", "e", "(~e & ~b) -> ~c", "(c & e) -> e", "(~e) -> c"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0035", "premises": ["~g", "(~e & c) -> c", "(~c & ~g) -> d", "(g) -> ~d", "(e) -> g", "(d) -> e"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0036", "premises": ["~b", "(~b) -> ~d", "(~e & f) -> ~e", "(d) -> ~f", "(~e & ~f) -> f"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0037", "premises": ["f", "~b", "(~d & g) -> b", "(f & g) -> f", "(d & a) -> ~b", "(g & ~a) -> b", "(~a) -> g"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0038", "premises": ["c", "(f & ~d) -> ~d", "(a) -> c", "(e & ~d) -> a", "(~a) -> ~f", "(d) -> ~c"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0039", "premises": ["g", "b", "(g & a) -> a", "(~e) -> a", "(g) -> g", "(a & ~g) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0040", "premises": ["~a", "(f & ~b) -> b", "(d) -> d", "(a) -> ~f", "(f & g) -> a", "(~a & ~g) -> f"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0041", "premises": ["d", "e", "(~c & ~d) -> c", "(~g) -> ~d", "(a & ~d) -> ~g", "(f & ~d) -> f", "(g & ~b) -> a"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0042", "premises": ["c", "(a) -> b", "(~c & a) -> a"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0043", "premises": ["~f", "~d", "(~e) -> ~c", "(b & ~g) -> g", "(d) -> ~d", "(b) -> ~a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0044", "premises": ["f", "(f & ~d) -> ~e", "(d & e) -> f"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0045", "premises": ["a", "c", "(f & c) -> ~c", "(b & ~a) -> a", "(a) -> a", "(~b) -> ~b"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0046", "premises": ["c", "b", "(~b & g) -> g", "(f) -> f", "(g & ~d) -> f"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0047", "premises": ["b", "d", "(~a & ~e) -> ~e", "(b & ~d) -> ~d", "(~d & ~b) -> d", "(~d & e) -> ~d"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0048", "premises": ["c", "~e", "d", "(~g) -> a", "(a & ~d) -> ~e", "(~g) -> g", "(~a) -> ~g", "(~c & ~g) -> e"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0049", "premises": ["~g", "a", "(c) -> a", "(~e & a) -> c"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0050", "premises": ["d", "(c) -> g", "(d) -> b", "(g & ~b) -> ~g", "(~g) -> ~g", "(~d & ~c) -> g"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0051", "premises": ["~b", "d", "(a & ~f) -> ~e", "(e & a) -> ~d", "(~f & e) -> e"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0052", "premises": ["~e", "(c) -> ~c", "(~d & ~c) -> ~c", "(e) -> a", "(~d & ~c) -> ~c"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0053", "premises": ["b", "e", "(~b) -> ~e", "(a) -> ~g"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0054", "premises": ["~e", "(~e & ~c) -> ~a", "(~a) -> ~a", "(a & g) -> e", "(~d & ~b) -> a", "(~a & ~g) -> g"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0055", "premises": ["f", "~a", "(~f) -> a", "(~d & ~a) -> ~d", "(d & ~f) -> e"], "query": "~f"}
{"gold": "refuted", "id": "dl-holdout-v1-0056", "premises": ["~g", "(~d) -> ~d", "(~e & ~g) -> g", "(g & b) -> ~g", "(~g) -> d", "(~b & d) -> e"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0057", "premises": ["d", "f", "(f & ~d) -> ~f", "(b & ~a) -> ~b", "(~a & ~b) -> f"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0058", "premises": ["~e", "(~b) -> b", "(~e & ~b) -> ~d", "(~c) -> d", "(c) -> b", "(~e & d) -> b"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0059", "premises": ["b", "~e", "(~b) -> ~b", "(~d & a) -> ~a"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0060", "premises": ["~c", "(~d) -> ~c", "(b) -> ~d", "(f) -> c", "(~g) -> ~b", "(b) -> ~g"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0061", "premises": ["~e", "~c", "(~a & ~b) -> ~g", "(e & a) -> a"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0062", "premises": ["~c", "~f", "(~f) -> d", "(~c & ~b) -> ~f"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0063", "premises": ["~e", "(b) -> ~e", "(~b) -> ~e"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0064", "premises": ["~d", "(a) -> b", "(d & c) -> ~g", "(d) -> ~g"], "query": "~a"}
{"gold": "entailed", "id": "dl-holdout-v1-0065", "premises": ["e", "~f", "(~f & ~b) -> b", "(~d & a) -> ~e"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0066", "premises": ["~d", "(~f & ~d) -> ~a", "(~e) -> f", "(g & ~f) -> c", "(~b & a) -> ~f", "(e & ~a) -> b"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0067", "premises": ["b", "(~c & f) -> b", "(~c & ~f) -> b", "(~e) -> ~c", "(~g & ~b) -> f", "(b) -> b"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0068", "premises": ["a", "(a & b) -> ~c", "(~c & ~f) -> ~c", "(f) -> a", "(~f) -> f"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0069", "premises": ["~a", "(b & f) -> ~d", "(~f) -> f", "(~g) -> a", "(~f) -> d", "(f) -> e"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0070", "premises": ["d", "(f & d) -> ~a", "(a & ~c) -> a"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0071", "premises": ["~c", "(e) -> b", "(g) -> c", "(b & ~g) -> ~e", "(g) -> c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0072", "premises": ["~f", "(g & ~a) -> d", "(~b & c) -> ~c", "(e) -> a", "(~d) -> ~b"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0073", "premises": ["d", "(~f & g) -> ~b", "(~b & f) -> e", "(~e & c) -> ~f", "(g) -> ~d", "(e & d) -> ~g"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0074", "premises": ["~c", "(b) -> a", "(~c) -> ~e", "(d & e) -> e"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0075", "premises": ["~g", "(d & ~g) -> c", "(g & b) -> b", "(~f & b) -> c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0076", "premises": ["d", "e", "(~c) -> e", "(~g) -> a", "(c) -> ~a", "(~e & ~c) -> c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0077", "premises": ["~d", "(~g) -> c", "(~d & ~g) -> ~d", "(~b) -> ~b", "(~g & b) -> e"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0078", "premises": ["a", "(~b & d) -> d", "(~a & b) -> ~b", "(g) -> ~a", "(d) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0079", "premises": ["~a", "~b", "(d & e) -> ~b", "(~c) -> f"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0080", "premises": ["f", "a", "(~a & ~b) -> c", "(f & a) -> b", "(c & g) -> c", "(c) -> ~a", "(~a & f) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0081", "premises": ["~a", "c", "(b) -> ~f", "(a & d) -> e", "(~d) -> b"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0082", "premises": ["~b", "(~a & ~b) -> c", "(b & ~d) -> ~c"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0083", "premises": ["d", "(~a & ~d) -> ~e", "(~e & g) -> e", "(g & e) -> g", "(~g) -> a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0084", "premises": ["f", "e", "(~a) -> f", "(~e) -> ~c", "(b & ~d) -> ~g"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0085", "premises": ["c", "(e) -> e", "(b) -> ~b", "(e) -> ~e", "(a & b) -> f", "(b & ~g) -> a"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0086", "premises": ["b", "(~f) -> d", "(f) -> ~g", "(d & ~b) -> ~f", "(~d & ~g) -> ~d"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0087", "premises": ["e", "~a", "(c & e) -> a", "(~d & ~a) -> a", "(c) -> e", "(e & b) -> ~b", "(~b) -> ~c"], "query": "a"}
{"gold": "entailed", "id": "dl-holdout-v1-0088", "premises": ["f", "~e", "(c) -> g", "(e) -> ~e", "(f & c) -> ~f"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0089", "premises": ["~d", "g", "(~c & ~f) -> ~d", "(~d & b) -> ~a"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0090", "premises": ["e", "(~d) -> ~e", "(~d & g) -> g", "(e & d) -> ~b"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0091", "premises": ["e", "c", "(~a) -> b", "(a & e) -> ~b"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0092", "premises": ["~g", "f", "(~e) -> g", "(~g) -> ~c", "(e & f) -> f"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0093", "premises": ["c", "g", "(c & a) -> ~b", "(a) -> g"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0094", "premises": ["c", "(~b & ~f) -> e", "(~d & ~e) -> e"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0095", "premises": ["~g", "f", "(e) -> ~f", "(e & f) -> g", "(e) -> c", "(~e) -> ~g"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0096", "premises": ["c", "~e", "d", "(a & ~d) -> ~a", "(~g & ~b) -> d"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0097", "premises": ["d", "(~c & ~b) -> a", "(a & ~e) -> ~f"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0098", "premises": ["f", "~d", "(~d) -> ~b", "(d) -> e"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0099", "premises": ["e", "(e) -> g", "(e & g) -> ~b"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0100", "premises": ["g", "~c", "(b) -> ~e", "(e) -> c"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0101", "premises": ["a", "(a) -> a", "(~c & a) -> a", "(d) -> c"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0102", "premises": ["d", "(~b & c) -> ~c", "(d) -> ~f", "(~b & f) -> b"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0103", "premises": ["d", "~a", "(f & ~d) -> ~f", "(a & ~c) -> d"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0104", "premises": ["~g", "e", "~d", "(~b & ~f) -> ~g", "(~d) -> a", "(e) -> a", "(~e & ~f) -> f", "(g & ~d) -> d"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0105", "premises": ["a", "(~d) -> b", "(~b) -> e", "(~a & ~g) -> ~a", "(~a) -> ~g"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0106", "premises": ["d", "g", "f", "(e & f) -> d", "(b & ~c) -> ~g"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0107", "premises": ["~b", "(b) -> ~g", "(a) -> ~e"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0108", "premises": ["c", "~b", "(c) -> f", "(b & f) -> d", "(c) -> d"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0109", "premises": ["~f", "c", "(~d & c) -> e", "(e) -> ~d"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0110", "premises": ["~e", "~b", "(f) -> g", "(~f & ~e) -> ~g", "(~e) -> ~f", "(g) -> ~e", "(g & ~e) -> ~b"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0111", "premises": ["a", "~f", "~d", "(a & ~c) -> ~e", "(~c) -> ~b", "(~f & a) -> ~d", "(c) -> ~c"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0112", "premises": ["~c", "~b", "(c) -> ~e", "(c) -> c", "(e) -> f", "(~c & ~a) -> b"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0113", "premises": ["g", "a", "(d) -> ~f", "(~a & f) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0114", "premises": ["~f", "d", "(~d) -> ~f", "(f & ~g) -> g"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0115", "premises": ["g", "(~d & e) -> d", "(d) -> ~c", "(~c & f) -> g", "(g & e) -> ~b"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0116", "premises": ["~b", "c", "(e & ~c) -> c", "(~d) -> ~g", "(d & ~e) -> ~d", "(c) -> ~b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0117", "premises": ["~b", "~f", "(b) -> ~d", "(~f & c) -> ~b", "(~f) -> a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0118", "premises": ["~a", "(~d & a) -> d", "(~a) -> b", "(~b & ~e) -> ~b"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0119", "premises": ["b", "~g", "(~g & ~d) -> e", "(d & g) -> ~b", "(d & g) -> ~e", "(b) -> ~e"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0120", "premises": ["e", "b", "(b & ~c) -> ~c", "(~f & e) -> ~b"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0121", "premises": ["c", "~g", "(b) -> e", "(g) -> ~f", "(e) -> g"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0122", "premises": ["~b", "d", "(~d & ~a) -> a", "(d & c) -> ~f", "(~d & c) -> ~a", "(b) -> ~f", "(c & ~e) -> ~a"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0123", "premises": ["f", "~e", "(~a) -> ~f", "(~f) -> a"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0124", "premises": ["~g", "(b) -> e", "(~b) -> ~c", "(~b) -> c", "(~b) -> ~b"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0125", "premises": ["~d", "g", "(~b & ~g) -> d", "(~b) -> ~g", "(~e & ~f) -> ~e", "(d & ~f) -> e"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0126", "premises": ["d", "(c & ~e) -> e", "(c & d) -> d", "(c & f) -> ~c", "(~d & ~e) -> ~f", "(f & c) -> c"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0127", "premises": ["~d", "(c & ~d) -> ~f", "(~d & a) -> a", "(b & ~d) -> d", "(f & c) -> b", "(b & ~d) -> ~f"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0128", "premises": ["b", "a", "(b) -> d", "(~c & ~a) -> ~d", "(~b & ~a) -> ~b"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0129", "premises": ["~b", "~f", "(~c & ~b) -> f", "(~a & ~f) -> a", "(b & a) -> ~f"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0130", "premises": ["~a", "b", "(f & e) -> e", "(~e) -> ~f", "(~g) -> f", "(a & e) -> ~f", "(b) -> b"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0131", "premises": ["f", "~g", "(~f & ~b) -> f", "(~f & g) -> ~g", "(~b & ~g) -> ~b", "(~f & b) -> ~b", "(b & ~g) -> b"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0132", "premises": ["c", "~b", "(g & b) -> g", "(~e) -> ~f", "(~a & ~b) -> a", "(d) -> ~a"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0133", "premises": ["~d", "e", "(~f & ~a) -> ~c", "(d) -> c"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0134", "premises": ["~a", "~d", "(f) -> a", "(f) -> ~c", "(e) -> c", "(~d & ~c) -> ~a", "(f) -> f"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0135", "premises": ["~d", "(a) -> ~d", "(a) -> e", "(c) -> ~d"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0136", "premises": ["~a", "(~c) -> g", "(~f) -> a"], "query": "~f"}
{"gold": "refuted", "id": "dl-holdout-v1-0137", "premises": ["~f", "~e", "(g & e) -> f", "(~g & ~e) -> ~f", "(~e & ~g) -> ~b", "(~f & g) -> c"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0138", "premises": ["a", "f", "~e", "(~f) -> e", "(~c & e) -> b"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0139", "premises": ["c", "(g & ~a) -> f", "(~g) -> ~g", "(a) -> ~e", "(c) -> e"], "query": "~a"}
{"gold": "entailed", "id": "dl-holdout-v1-0140", "premises": ["~d", "(~a) -> c", "(~a) -> ~c", "(~d & ~c) -> a", "(~c & g) -> ~e", "(~e & a) -> ~a"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0141", "premises": ["c", "~b", "e", "(a & f) -> e", "(~f & a) -> ~b", "(e & c) -> c", "(~a) -> f"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0142", "premises": ["e", "~b", "(c & ~g) -> e", "(~g) -> ~g"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0143", "premises": ["~a", "d", "c", "(a & ~c) -> ~f", "(f) -> ~e", "(a & c) -> a", "(~c & f) -> ~e", "(c) -> ~e"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0144", "premises": ["~b", "(~g & ~d) -> d", "(b & d) -> ~b", "(~d & g) -> ~g"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0145", "premises": ["~a", "~d", "e", "(d) -> g", "(e & f) -> ~d", "(~f & a) -> ~f", "(~f & ~e) -> ~e", "(~f & a) -> b"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0146", "premises": ["~g", "e", "~f", "(~e & g) -> ~b", "(b) -> ~b", "(g & ~b) -> b", "(~e) -> ~g", "(d) -> ~e"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0147", "premises": ["~g", "~f", "(~b) -> f", "(~c & g) -> ~g"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0148", "premises": ["b", "d", "f", "(~c & g) -> g", "(~f) -> ~e", "(~d & b) -> c", "(~e & ~b) -> b", "(g & b) -> ~b"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0149", "premises": ["~a", "f", "(a) -> a", "(b & e) -> ~e", "(a) -> a"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0150", "premises": ["~d", "~b", "f", "(~b & d) -> ~d", "(~f) -> ~e", "(g & ~c) -> ~g"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0151", "premises": ["~a", "(b & ~d) -> ~g", "(e & ~f) -> ~d", "(~d & g) -> ~b"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0152", "premises": ["d", "(~e & ~g) -> ~d", "(g & ~d) -> ~e"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0153", "premises": ["~f", "(~a) -> a", "(~f) -> c", "(f & g) -> ~c"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0154", "premises": ["e", "(~a) -> a", "(e) -> g"], "query": "a"}
{"gold": "entailed", "id": "dl-holdout-v1-0155", "premises": ["~f", "~d", "(~a & f) -> e", "(~g & c) -> a", "(~e) -> ~d"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0156", "premises": ["~f", "(e & ~f) -> c", "(~f & ~c) -> f"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0157", "premises": ["~c", "a", "(a & ~f) -> ~a", "(~c & ~f) -> ~g", "(~c) -> ~g", "(~c & ~g) -> f", "(f) -> a"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0158", "premises": ["~e", "(~d & ~b) -> b", "(f & a) -> ~b", "(f & g) -> ~a", "(f & ~g) -> ~b"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0159", "premises": ["g", "c", "~e", "(a & e) -> g", "(~c) -> f"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0160", "premises": ["b", "(~g) -> a", "(b & e) -> ~g", "(e) -> g"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0161", "premises": ["~e", "a", "g", "(f & ~g) -> ~g", "(~b) -> b", "(~b & ~g) -> e", "(c & a) -> b", "(g & ~b) -> c"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0162", "premises": ["~e", "(c) -> e", "(b & e) -> ~d"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0163", "premises": ["~a", "~e", "f", "(f & g) -> b", "(~b) -> ~e"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0164", "premises": ["f", "(e & ~b) -> f", "(~e & c) -> f", "(g & ~c) -> e", "(g & ~e) -> e"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0165", "premises": ["g", "~c", "b", "(e) -> ~e", "(~g & b) -> f", "(~b) -> ~b", "(~c & e) -> ~c", "(~f) -> a"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0166", "premises": ["~g", "(~c) -> g", "(c) -> ~d", "(g & ~c) -> a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0167", "premises": ["e", "(~d & ~b) -> c", "(g & ~b) -> e"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0168", "premises": ["b", "(g) -> ~b", "(b) -> ~e"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0169", "premises": ["a", "(~e & ~d) -> ~g", "(~a & d) -> ~e", "(g & ~b) -> d", "(a & g) -> b", "(a & ~b) -> d"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0170", "premises": ["~e", "c", "(g & a) -> c", "(g & ~b) -> a"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0171", "premises": ["g", "e", "~d", "(~b) -> ~c", "(e) -> a", "(~d & b) -> g"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0172", "premises": ["~b", "e", "(~e) -> a", "(b) -> d", "(b) -> d", "(a) -> a"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0173", "premises": ["b", "(a & e) -> b", "(e & a) -> a"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0174", "premises": ["f", "e", "(~g) -> c", "(~b) -> ~b"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0175", "premises": ["b", "~e", "~f", "(d & ~e) -> e", "(~g) -> f"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0176", "premises": ["d", "(b & e) -> ~b", "(~b) -> e"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0177", "premises": ["~b", "(e) -> e", "(d & ~a) -> ~a", "(~e) -> b", "(~a & ~g) -> ~e", "(~e) -> g"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0178", "premises": ["e", "(~f & ~d) -> e", "(e) -> a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0179", "premises": ["c", "(~d & ~c) -> ~d", "(~b) -> f", "(b & d) -> ~a"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0180", "premises": ["~c", "a", "(~c) -> g", "(e) -> e", "(a) -> a", "(~d & ~g) -> g", "(~c) -> g"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0181", "premises": ["e", "(c) -> ~e", "(c & ~g) -> ~d", "(d & e) -> ~g", "(e & g) -> ~a"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0182", "premises": ["~c", "~a", "~b", "(c & d) -> a", "(~e & ~b) -> b"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0183", "premises": ["~c", "(~g & ~a) -> e", "(~a) -> b", "(~e & c) -> ~d"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0184", "premises": ["b", "f", "(~b) -> d", "(~f & ~b) -> b", "(~f) -> ~a", "(a) -> ~f"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0185", "premises": ["~d", "~f", "(~e & ~c) -> d", "(b & ~c) -> b", "(c) -> ~d"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0186", "premises": ["~e", "(a) -> c", "(a & c) -> e", "(~a) -> c", "(c & ~d) -> ~e", "(~a & e) -> ~e"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0187", "premises": ["f", "c", "(b) -> b", "(e) -> ~c", "(e) -> ~b", "(f) -> f"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0188", "premises": ["f", "e", "(b & ~d) -> d", "(~e) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0189", "premises": ["~d", "(~g & e) -> ~d", "(b & a) -> ~b", "(~d) -> b", "(~g) -> c", "(~a & ~g) -> c"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0190", "premises": ["~b", "e", "c", "(b) -> g", "(e) -> e", "(d & ~e) -> g", "(~c & ~g) -> ~g"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0191", "premises": ["f", "d", "(~f & ~b) -> f", "(d) -> b", "(~c & ~d) -> ~b", "(g & ~f) -> ~d", "(b & ~g) -> ~d"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0192", "premises": ["~g", "~a", "(c) -> ~c", "(~g & c) -> g", "(~d & ~a) -> ~a"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0193", "premises": ["b", "~a", "f", "(~a) -> e", "(~c) -> ~g", "(~f) -> ~f", "(~e & g) -> a", "(e & ~d) -> ~d"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0194", "premises": ["~a", "d", "(c) -> ~b", "(~c) -> ~b"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0195", "premises": ["~d", "~e", "(c & ~g) -> b", "(f) -> f", "(g) -> e", "(e) -> c"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0196", "premises": ["a", "(a) -> ~b", "(~c) -> a", "(~g & ~b) -> b"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0197", "premises": ["~c", "(~d) -> ~a", "(b) -> f"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0198", "premises": ["~b", "a", "(b) -> a", "(~c) -> d", "(d & ~b) -> ~b", "(d) -> a"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0199", "premises": ["b", "(e & g) -> a", "(~e) -> g", "(g & ~b) -> b", "(b) -> c", "(b) -> a"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0200", "premises": ["~e", "a", "g", "(b) -> ~c", "(~a & b) -> ~f"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0201", "premises": ["c", "(c & ~f) -> c", "(~c) -> c"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0202", "premises": ["e", "c", "(e & f) -> ~f", "(~c) -> g", "(b & ~c) -> ~b", "(~g & c) -> ~b"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0203", "premises": ["a", "c", "~e", "(~a & ~e) -> ~c", "(f & ~e) -> c"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0204", "premises": ["g", "(~a) -> g", "(~g & ~f) -> c"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0205", "premises": ["b", "(b & ~f) -> f", "(g & a) -> a", "(~f & ~g) -> b"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0206", "premises": ["~g", "~e", "f", "(~e) -> ~e", "(b & ~c) -> e", "(~b) -> ~b", "(d) -> ~f"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0207", "premises": ["~d", "(~g) -> f", "(f & e) -> d", "(d) -> f", "(~e & ~g) -> g"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0208", "premises": ["g", "(~e) -> ~g", "(g) -> ~d", "(~c & e) -> a"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0209", "premises": ["~d", "(~e & ~f) -> d", "(c & e) -> ~e", "(~f & ~c) -> c", "(~e) -> e", "(~e) -> e"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0210", "premises": ["e", "(g) -> ~c", "(~g & ~c) -> ~c", "(c) -> g", "(~b & ~f) -> f", "(b & e) -> ~e"], "query": "~g"}
{"gold": "refuted", "id": "dl-holdout-v1-0211", "premises": ["~e", "~d", "b", "(~f & e) -> b", "(~d & ~a) -> d", "(~g) -> c", "(f & ~a) -> ~d", "(~a) -> e"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0212", "premises": ["f", "~a", "(c) -> e", "(~b & e) -> ~b", "(~f & e) -> ~e", "(~b) -> b", "(c & b) -> ~a"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0213", "premises": ["~b", "~a", "(~e & g) -> ~b", "(~b) -> ~g"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0214", "premises": ["b", "(b & d) -> d", "(d & b) -> b", "(~b & g) -> ~d", "(d & ~a) -> a", "(a) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0215", "premises": ["~e", "(~g & c) -> ~c", "(d) -> ~e"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0216", "premises": ["d", "a", "~e", "(e) -> ~b", "(g & ~d) -> ~a", "(~g) -> ~a", "(e & ~a) -> ~g"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0217", "premises": ["g", "e", "(~g) -> ~a", "(a) -> c", "(~a) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0218", "premises": ["~b", "(~c & f) -> c", "(f & a) -> e"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0219", "premises": ["f", "(d) -> ~f", "(~f) -> f"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0220", "premises": ["a", "~g", "~e", "(g & ~e) -> b", "(~d) -> d"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0221", "premises": ["g", "d", "(a) -> d", "(d & ~f) -> ~d"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0222", "premises": ["a", "(~f & ~b) -> ~d", "(c & ~f) -> b", "(~b) -> ~d", "(f & ~b) -> c"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0223", "premises": ["c", "~d", "(f) -> ~a", "(~b) -> ~a", "(~d & ~c) -> c"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0224", "premises": ["~a", "g", "(b) -> ~a", "(~a) -> e", "(~f) -> ~c", "(c) -> c"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0225", "premises": ["f", "~g", "(b) -> g", "(a & ~e) -> d", "(d & f) -> ~g", "(~a) -> ~a", "(~c & ~a) -> ~b"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0226", "premises": ["~f", "g", "e", "(b & d) -> ~a", "(e & d) -> a", "(g & ~a) -> f", "(~e) -> ~d", "(d & e) -> ~g"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0227", "premises": ["a", "~g", "c", "(~a) -> ~c", "(~a & g) -> b", "(~a) -> ~a", "(~e & ~a) -> b"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0228", "premises": ["~b", "f", "(~d & ~a) -> ~a", "(~c & ~e) -> ~c", "(~b & c) -> ~b"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0229", "premises": ["~e", "(a) -> b", "(d) -> ~d"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0230", "premises": ["~g", "(~e) -> ~e", "(~a & b) -> ~e", "(~b) -> e", "(c & e) -> ~d", "(a & ~d) -> c"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0231", "premises": ["~a", "~b", "(~c) -> ~g", "(~a & c) -> ~e"], "query": "~g"}
{"gold": "refuted", "id": "dl-holdout-v1-0232", "premises": ["a", "(~f & ~d) -> f", "(~a) -> ~g", "(~g & d) -> ~d", "(d) -> ~f"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0233", "premises": ["~g", "(g & ~d) -> g", "(c) -> ~e", "(~c & e) -> a", "(~a) -> c"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0234", "premises": ["~f", "~d", "g", "(~a) -> e", "(f) -> ~f", "(~a) -> g", "(c) -> ~g"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0235", "premises": ["~b", "g", "(~b) -> ~e", "(~f) -> b", "(~c) -> e"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0236", "premises": ["~c", "a", "(f & ~g) -> ~b", "(b & g) -> ~c", "(c) -> ~b", "(a & f) -> ~b", "(~g) -> e"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0237", "premises": ["d", "f", "(~f & ~g) -> ~b", "(g & ~c) -> f", "(~e) -> d", "(~d) -> d"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0238", "premises": ["~f", "(f & b) -> ~e", "(~c & f) -> ~c", "(b) -> d", "(e) -> ~e"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0239", "premises": ["~f", "(b & f) -> a", "(f) -> f", "(~g & f) -> ~b", "(f & ~b) -> ~b", "(~f) -> ~g"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0240", "premises": ["~f", "e", "(~d & e) -> c", "(~e) -> a", "(~d & f) -> ~a", "(~d) -> ~e", "(~a & ~e) -> a"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0241", "premises": ["f", "e", "(a) -> ~g", "(~e & g) -> ~a", "(a & ~g) -> g", "(a) -> f"], "query": "a"}
{"gold": "entailed", "id": "dl-holdout-v1-0242", "premises": ["b", "~e", "(~b) -> ~f", "(~b) -> ~b", "(e & b) -> ~e", "(e) -> g", "(c & f) -> ~b"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0243", "premises": ["~e", "~f", "d", "(g & d) -> ~c", "(~d & e) -> ~e", "(~b) -> g"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0244", "premises": ["e", "(~b & e) -> b", "(a & b) -> ~f", "(~f & ~e) -> ~d", "(b & ~g) -> ~f", "(e & a) -> ~g"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0245", "premises": ["~d", "~f", "(~g & f) -> d", "(~g & b) -> ~g", "(g & ~f) -> b", "(~d & ~g) -> ~f", "(d) -> ~b"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0246", "premises": ["~c", "g", "~a", "(~d & c) -> e", "(e) -> b", "(~f) -> d", "(~f & ~b) -> d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0247", "premises": ["e", "(~b) -> e", "(a) -> ~d", "(~c & e) -> ~a", "(c & ~b) -> d"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0248", "premises": ["~a", "(~a) -> ~f", "(~a) -> ~e", "(~a) -> g"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0249", "premises": ["c", "(~g & ~f) -> f", "(~g & f) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0250", "premises": ["c", "~e", "~d", "(d) -> g", "(~b) -> ~e"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0251", "premises": ["~e", "f", "~d", "(g & c) -> ~b", "(b & e) -> b", "(b) -> d", "(~b) -> c", "(~e) -> a"], "query": "~f"}
{"gold": "refuted", "id": "dl-holdout-v1-0252", "premises": ["g", "(f & d) -> ~a", "(a & g) -> ~a", "(f) -> ~f"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0253", "premises": ["~f", "(f & e) -> ~a", "(~f & a) -> ~c", "(~f) -> ~c", "(~c) -> ~e"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0254", "premises": ["~c", "(d & ~a) -> ~g", "(c & ~d) -> ~b", "(~a & ~f) -> c"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0255", "premises": ["~d", "a", "f", "(~g) -> ~d", "(b) -> g"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0256", "premises": ["a", "(~c & ~f) -> ~c", "(c & g) -> c", "(~g & c) -> ~g"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0257", "premises": ["~c", "a", "~f", "(~f) -> g", "(e) -> ~c", "(g & c) -> b"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0258", "premises": ["c", "(~g & ~d) -> e", "(~e) -> c", "(~c & g) -> ~c", "(~e) -> ~d", "(e) -> b"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0259", "premises": ["d", "(g & ~a) -> b", "(f) -> ~g", "(f & b) -> d"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0260", "premises": ["~d", "g", "(d & c) -> ~d", "(f & g) -> ~g", "(f & c) -> ~c", "(~b & g) -> ~g", "(~a & ~d) -> b"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0261", "premises": ["~b", "d", "~c", "(~f) -> f", "(b & c) -> a"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0262", "premises": ["a", "~d", "(e & ~b) -> e", "(c & ~e) -> ~b", "(e) -> a"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0263", "premises": ["~b", "a", "(~a) -> f", "(~e & ~a) -> ~a"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0264", "premises": ["g", "~a", "(~e) -> g", "(~c & ~e) -> f", "(~d & ~g) -> a", "(~e & g) -> d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0265", "premises": ["b", "(b & d) -> f", "(~f) -> c", "(c & d) -> ~e"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0266", "premises": ["~b", "~a", "~e", "(g & f) -> c", "(~f & ~g) -> e", "(~g & d) -> f", "(d) -> c"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0267", "premises": ["~a", "c", "(d & ~g) -> c", "(d & ~a) -> ~c", "(~f & ~c) -> ~g", "(f & g) -> ~g"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0268", "premises": ["~g", "~a", "(g) -> ~a", "(~b & a) -> ~a", "(~f) -> ~e", "(g & ~b) -> e", "(e) -> ~g"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0269", "premises": ["a", "(a & ~c) -> ~g", "(b & ~d) -> ~b", "(~c & ~g) -> d"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0270", "premises": ["b", "f", "(g & d) -> ~e", "(b & ~d) -> ~g", "(~e) -> ~f", "(~b & ~e) -> ~a"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0271", "premises": ["~e", "(a & ~b) -> ~b", "(b) -> ~e", "(a & b) -> ~b", "(~e) -> d", "(d & b) -> ~d"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0272", "premises": ["g", "(d) -> f", "(a) -> b"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0273", "premises": ["a", "(~g) -> e", "(a & e) -> d", "(a & ~g) -> ~d", "(d & c) -> e", "(e) -> c"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0274", "premises": ["b", "(~e & a) -> ~b", "(b & ~a) -> ~g"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0275", "premises": ["c", "f", "(d & ~e) -> f", "(e & ~c) -> c", "(~d & ~f) -> g", "(g) -> d"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0276", "premises": ["g", "(c & b) -> ~b", "(~b) -> c", "(g) -> ~f"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0277", "premises": ["b", "(a) -> ~d", "(d & ~c) -> c", "(~f) -> ~b", "(~a & d) -> b"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0278", "premises": ["a", "(g) -> ~f", "(~a) -> ~c", "(c) -> ~e", "(a & c) -> e"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0279", "premises": ["f", "b", "d", "(c) -> f", "(~b) -> b", "(b & ~a) -> a"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0280", "premises": ["g", "~d", "(e) -> ~g", "(~a) -> e"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0281", "premises": ["d", "~f", "e", "(a) -> d", "(~b & ~a) -> ~e", "(~b) -> ~a", "(a & ~e) -> a"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0282", "premises": ["~d", "f", "b", "(g & c) -> a", "(~d & e) -> ~f", "(a & ~g) -> b"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0283", "premises": ["~f", "~e", "(~g) -> a", "(~b) -> g", "(~g) -> ~b", "(~e) -> ~a", "(a & b) -> f"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0284", "premises": ["~g", "f", "~d", "(d & ~b) -> g", "(b) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0285", "premises": ["e", "(d & ~b) -> ~d", "(~b) -> f", "(f & ~e) -> ~d", "(f & d) -> ~c"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0286", "premises": ["d", "a", "~e", "(b) -> d", "(a & c) -> d", "(~d & f) -> ~e"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0287", "premises": ["c", "~f", "(~f & d) -> ~a", "(e & f) -> e"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0288", "premises": ["f", "~c", "(~d & ~a) -> e", "(~d) -> ~e", "(~a & d) -> ~d", "(a) -> f"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0289", "premises": ["a", "(g & ~d) -> d", "(~f) -> ~b", "(~f & d) -> f", "(a) -> f"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0290", "premises": ["c", "(f & e) -> ~c", "(a) -> ~a", "(a & e) -> c"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0291", "premises": ["~d", "(~a & ~b) -> ~c", "(d & e) -> ~c", "(~e & b) -> b", "(b) -> ~b"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0292", "premises": ["~e", "~d", "(g & a) -> c", "(~g) -> ~g", "(~e & ~f) -> ~g", "(~g & a) -> g", "(~f) -> ~f"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0293", "premises": ["~g", "e", "(a & g) -> ~e", "(~e) -> f", "(~g) -> a"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0294", "premises": ["b", "~f", "e", "(a & ~b) -> c", "(c & a) -> ~f", "(~f) -> ~c", "(~a) -> ~c"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0295", "premises": ["e", "~c", "f", "(a) -> ~d", "(g & b) -> a"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0296", "premises": ["f", "~d", "(f) -> e", "(e & ~b) -> ~c", "(g & d) -> c", "(~g & ~b) -> ~d"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0297", "premises": ["g", "(c) -> ~g", "(~c) -> ~a"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0298", "premises": ["~g", "(~c & e) -> e", "(d) -> e", "(e & g) -> c", "(~e) -> ~d", "(~d & ~e) -> e"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0299", "premises": ["~e", "~d", "g", "(~e & ~b) -> c", "(f) -> ~e", "(e & ~d) -> d", "(c) -> ~d", "(e & ~b) -> g"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0300", "premises": ["~a", "(a & d) -> ~b", "(d) -> a", "(d) -> a", "(a & c) -> ~d"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0301", "premises": ["~e", "(f & b) -> ~e", "(f & b) -> e", "(~e) -> ~b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0302", "premises": ["b", "(b) -> b", "(~g) -> ~g", "(d) -> g", "(f) -> f"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0303", "premises": ["~a", "(~g) -> g", "(~d) -> ~e", "(~a & e) -> ~g", "(a) -> g", "(g) -> ~d"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0304", "premises": ["~e", "d", "(~c) -> ~d", "(a & c) -> ~c", "(~c & ~d) -> d", "(f & e) -> ~a"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0305", "premises": ["~e", "~a", "~b", "(f & ~c) -> d", "(~b) -> ~a", "(a & ~d) -> b", "(~c) -> ~f", "(d) -> e"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0306", "premises": ["g", "(d & ~g) -> ~f", "(~a & ~f) -> a"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0307", "premises": ["~b", "~e", "f", "(~d & e) -> c", "(d) -> ~c", "(e) -> ~c"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0308", "premises": ["c", "~f", "(a) -> a", "(g) -> f", "(~e & c) -> e", "(~e) -> f"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0309", "premises": ["~f", "(~a & c) -> ~f", "(~c & d) -> d", "(~f & c) -> ~c"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0310", "premises": ["g", "f", "~d", "(a) -> f", "(b & ~g) -> d", "(~a) -> ~b", "(f) -> a", "(~c & ~a) -> e"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0311", "premises": ["~a", "e", "(e & a) -> b", "(b & ~d) -> b", "(d & b) -> d", "(b) -> ~e"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0312", "premises": ["f", "(e & f) -> ~b", "(~e & b) -> ~e"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0313", "premises": ["~g", "e", "(b & e) -> g", "(~e) -> ~d", "(b & ~g) -> ~g"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0314", "premises": ["~d", "~b", "(~f) -> b", "(~f) -> ~g"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0315", "premises": ["c", "a", "(c & ~g) -> ~e", "(~e & ~c) -> ~a", "(a & ~g) -> ~e", "(g & e) -> ~e", "(g & c) -> a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0316", "premises": ["~b", "~a", "(b) -> ~a", "(f) -> f", "(~e & a) -> ~a"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0317", "premises": ["a", "(f) -> g", "(~e & f) -> a", "(f) -> ~a", "(d) -> ~f", "(g) -> d"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0318", "premises": ["~e", "~a", "(f) -> c", "(c) -> ~f", "(a) -> ~a", "(b & e) -> a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0319", "premises": ["f", "(d) -> ~b", "(~b & ~g) -> ~d", "(~b & ~d) -> d"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0320", "premises": ["f", "b", "g", "(~e) -> a", "(d & ~a) -> ~g"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0321", "premises": ["~g", "~f", "e", "(c & ~g) -> b", "(~d) -> ~f"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0322", "premises": ["c", "(d) -> ~d", "(d & c) -> f", "(f & ~d) -> c", "(d) -> ~f", "(~f) -> f"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0323", "premises": ["c", "g", "(~a) -> g", "(c) -> d", "(~g) -> d", "(~c & g) -> ~g"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0324", "premises": ["~a", "(~c & e) -> ~a", "(f & c) -> ~f", "(b & ~f) -> a"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0325", "premises": ["~c", "(~f) -> b", "(f & d) -> f", "(b & g) -> b", "(~c & ~g) -> f"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0326", "premises": ["~f", "~c", "b", "(c) -> d", "(e & ~f) -> d", "(f) -> ~b", "(e) -> e"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0327", "premises": ["~g", "(~f & g) -> f", "(c & ~d) -> ~a", "(a) -> d", "(~f) -> d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0328", "premises": ["~c", "~b", "(e & a) -> ~c", "(e) -> ~e", "(~e & a) -> ~e", "(b) -> b", "(~g) -> ~g"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0329", "premises": ["~f", "~c", "(~c) -> ~g", "(f & c) -> a"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0330", "premises": ["b", "f", "~c", "(~g) -> ~b", "(~g) -> ~b", "(~g & ~c) -> b", "(b & ~f) -> a", "(~f & ~g) -> f"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0331", "premises": ["d", "~g", "f", "(f & b) -> f", "(~g) -> d", "(g) -> ~d", "(d) -> a"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0332", "premises": ["~g", "(~b) -> g", "(~g & d) -> b", "(~d) -> ~a", "(d & ~f) -> d", "(~e) -> d"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0333", "premises": ["d", "f", "~c", "(~b & g) -> ~g", "(~f) -> ~b", "(~d) -> g"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0334", "premises": ["~e", "f", "(a) -> f", "(~c) -> ~c", "(a & f) -> ~e", "(f) -> ~c"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0335", "premises": ["~a", "(~g & ~a) -> ~f", "(a) -> ~d", "(g & ~f) -> ~d"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0336", "premises": ["d", "b", "~e", "(~a) -> b", "(f & c) -> e", "(~g) -> ~b"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0337", "premises": ["d", "~g", "~f", "(a) -> f", "(c) -> ~f"], "query": "a"}
{"gold": "refuted", "id": "dl-holdout-v1-0338", "premises": ["d", "b", "(~b) -> ~d", "(~b & e) -> b", "(e & c) -> ~c", "(c) -> c", "(~c) -> c"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0339", "premises": ["g", "(g) -> g", "(~b & g) -> ~b", "(g) -> ~c", "(~e) -> ~g", "(~b) -> ~g"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0340", "premises": ["~c", "(g) -> ~c", "(f) -> ~a", "(~f & g) -> c"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0341", "premises": ["~c", "e", "(~a) -> d", "(~g) -> d"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0342", "premises": ["d", "f", "(~g & f) -> ~a", "(~a) -> c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0343", "premises": ["d", "(g) -> d", "(~d & c) -> d", "(~g & ~c) -> ~c", "(~c) -> ~b"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0344", "premises": ["~c", "~a", "~d", "(~e & ~c) -> ~d", "(d) -> e", "(g) -> e"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0345", "premises": ["~f", "(f & d) -> b", "(f & ~e) -> d"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0346", "premises": ["~f", "g", "c", "(~d) -> c", "(~c) -> f", "(~a) -> ~e"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0347", "premises": ["~b", "(~d) -> ~b", "(~g) -> ~g", "(~d & ~c) -> ~d", "(~c & ~b) -> ~d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0348", "premises": ["a", "~c", "~g", "(~f) -> b", "(d) -> a"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0349", "premises": ["b", "~c", "(~f & ~b) -> ~g", "(d) -> ~a", "(~c) -> f", "(~f & e) -> d", "(~c) -> f"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0350", "premises": ["~d", "c", "(~d & a) -> a", "(c & f) -> f", "(~a) -> d"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0351", "premises": ["e", "d", "(c & e) -> e", "(~b & ~a) -> e"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0352", "premises": ["~d", "(~d) -> b", "(~d) -> b", "(~a) -> ~d", "(~a) -> ~a"], "query": "~d"}
{"gold": "entailed", "id": "dl-holdout-v1-0353", "premises": ["b", "~c", "(~c) -> f", "(~f) -> f", "(~b) -> ~f", "(~f & b) -> ~f", "(c) -> f"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0354", "premises": ["~b", "(~a) -> b", "(e & ~b) -> g", "(~a) -> ~d", "(f) -> ~b"], "query": "~a"}
{"gold": "entailed", "id": "dl-holdout-v1-0355", "premises": ["~g", "e", "(c) -> a", "(f & c) -> ~c", "(f) -> a", "(e & g) -> ~f", "(c) -> ~f"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0356", "premises": ["g", "(a) -> ~c", "(~c) -> b", "(c & d) -> ~c"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0357", "premises": ["e", "(~b) -> ~f", "(e) -> b", "(~c) -> f"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0358", "premises": ["~d", "(~b) -> ~d", "(~b & c) -> ~a", "(b) -> d"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0359", "premises": ["~f", "b", "(~d) -> b", "(~d & ~g) -> c", "(~d & b) -> ~e", "(~a & ~d) -> ~c", "(a & g) -> ~b"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0360", "premises": ["~f", "(~d) -> g", "(d & b) -> g", "(~d) -> e", "(~f & e) -> ~b"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0361", "premises": ["~d", "b", "~e", "(a & ~g) -> e", "(~g) -> g", "(c) -> ~g", "(~f) -> b"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0362", "premises": ["b", "(a) -> ~b", "(~e & ~f) -> ~b", "(~e) -> ~a", "(e & a) -> ~b"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0363", "premises": ["b", "(~b & ~a) -> d", "(~a) -> ~b", "(~a) -> ~b", "(~f & b) -> g", "(g) -> ~a"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0364", "premises": ["~d", "~e", "~g", "(~d) -> b", "(c) -> a"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0365", "premises": ["e", "d", "(g) -> ~f", "(c & ~d) -> e"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0366", "premises": ["~c", "(~b) -> e", "(f & e) -> b", "(~e & ~g) -> ~c", "(~e) -> ~e", "(g & ~b) -> f"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0367", "premises": ["~e", "~c", "(f & ~b) -> e", "(~c & ~e) -> ~e", "(f & ~b) -> b"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0368", "premises": ["f", "(c & ~b) -> b", "(~f & e) -> e", "(f & ~e) -> ~e"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0369", "premises": ["~d", "(e) -> c", "(~g) -> c", "(~c) -> b", "(~f) -> g"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0370", "premises": ["f", "~b", "(e & ~b) -> b", "(~e) -> ~g", "(~e & ~a) -> f", "(~e) -> f"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0371", "premises": ["~a", "(f & ~b) -> a", "(d) -> d", "(~d & ~a) -> b"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0372", "premises": ["~g", "~c", "~a", "(~g) -> ~b", "(d) -> g", "(~e) -> ~f", "(b & a) -> ~e"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0373", "premises": ["~c", "(f & ~d) -> ~d", "(~g & e) -> d", "(~f) -> ~d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0374", "premises": ["e", "f", "(~e) -> c", "(~d) -> b", "(c & b) -> e", "(~b & g) -> ~c"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0375", "premises": ["~d", "(c & ~b) -> g", "(c) -> b", "(a) -> ~a", "(~e & d) -> b", "(~e & c) -> a"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0376", "premises": ["~e", "(e & c) -> a", "(a & c) -> ~f"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0377", "premises": ["~g", "(~g & c) -> ~f", "(a) -> ~c"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0378", "premises": ["b", "~a", "(~a & e) -> ~a", "(d) -> e", "(~a) -> e", "(a) -> ~b", "(~d) -> ~d"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0379", "premises": ["~a", "(~e & f) -> ~f", "(b) -> ~g", "(b & a) -> ~g"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0380", "premises": ["b", "(~g) -> ~e", "(~e & d) -> ~g", "(d & ~c) -> d", "(~d & ~e) -> c"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0381", "premises": ["c", "(e & ~c) -> ~e", "(~d & a) -> e", "(~d) -> d", "(a & c) -> c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0382", "premises": ["d", "c", "(a & c) -> ~e", "(c) -> ~e", "(e & f) -> e", "(~a & ~f) -> ~f", "(f) -> ~c"], "query": "~a"}
{"gold": "entailed", "id": "dl-holdout-v1-0383", "premises": ["e", "f", "(~a) -> ~f", "(~b & g) -> f"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0384", "premises": ["~c", "b", "(b & f) -> f", "(~a) -> ~f", "(b & ~c) -> ~c"], "query": "~f"}
{"gold": "entailed", "id": "dl-holdout-v1-0385", "premises": ["~f", "~g", "(c & ~b) -> b", "(~a) -> ~f", "(d) -> ~g", "(d) -> ~c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0386", "premises": ["g", "e", "(~f) -> ~a", "(a & e) -> ~a", "(g & a) -> ~a"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0387", "premises": ["~b", "f", "(a) -> d", "(~f & e) -> d"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0388", "premises": ["~b", "d", "(~d & ~a) -> ~g", "(~c & b) -> ~a", "(~d & c) -> a", "(b & ~a) -> ~b"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0389", "premises": ["~e", "a", "d", "(d & ~f) -> ~f", "(~g & ~d) -> c", "(~c) -> ~f", "(a) -> ~e", "(~f) -> e"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0390", "premises": ["~b", "~e", "(~b & g) -> e", "(~e & b) -> e", "(~f & g) -> e"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0391", "premises": ["~b", "(b) -> ~e", "(b) -> ~f", "(~d) -> ~f", "(~b & ~e) -> e", "(~b & e) -> ~b"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0392", "premises": ["e", "(~g & a) -> e", "(b) -> ~a", "(~b & ~d) -> c", "(g & d) -> b"], "query": "~b"}
{"gold": "refuted", "id": "dl-holdout-v1-0393", "premises": ["c", "(~g & ~f) -> d", "(c & b) -> ~b", "(~g & ~d) -> f", "(~f) -> c", "(~a) -> ~d"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0394", "premises": ["~b", "(b) -> ~a", "(~d & c) -> a", "(a) -> ~c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0395", "premises": ["b", "(a & f) -> ~a", "(~g) -> e", "(b) -> ~f", "(~e & ~g) -> g", "(~b) -> ~e"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0396", "premises": ["~b", "~f", "a", "(d & a) -> c", "(f) -> f", "(~d & b) -> ~c", "(~b) -> ~f"], "query": "~b"}
{"gold": "entailed", "id": "dl-holdout-v1-0397", "premises": ["f", "~b", "(f) -> ~a", "(a) -> ~e"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0398", "premises": ["d", "e", "(e & b) -> g", "(~g & b) -> ~e"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0399", "premises": ["~g", "~a", "d", "(e) -> c", "(e & g) -> ~g"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0400", "premises": ["b", "d", "e", "(a) -> f", "(~e) -> d", "(b) -> ~a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0401", "premises": ["e", "(g & ~e) -> b", "(b & e) -> ~b", "(g) -> ~b", "(f & d) -> e"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0402", "premises": ["a", "(a & ~g) -> g", "(g & e) -> ~a", "(~g) -> b", "(a) -> a"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0403", "premises": ["g", "~c", "(f & ~a) -> ~f", "(~e) -> ~c"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0404", "premises": ["~f", "~c", "(~b) -> ~d", "(~c & ~b) -> ~g", "(~c) -> ~d", "(~f) -> ~f", "(~g & b) -> c"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0405", "premises": ["a", "(e & ~a) -> c", "(~a) -> ~e", "(g) -> a", "(~g & ~a) -> ~a"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0406", "premises": ["~d", "~f", "~e", "(d & ~f) -> b", "(g & ~f) -> g", "(~g) -> c", "(c & a) -> ~g"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0407", "premises": ["a", "(d & a) -> ~e", "(d & ~e) -> a", "(d) -> d"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0408", "premises": ["~d", "g", "(c) -> ~c", "(g) -> ~e", "(d) -> a", "(d) -> d"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0409", "premises": ["f", "b", "e", "(~b & f) -> ~e", "(~f) -> ~c", "(d & f) -> e"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0410", "premises": ["~f", "(a & ~b) -> b", "(a) -> ~f", "(f & c) -> f", "(b) -> a", "(f & e) -> ~c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0411", "premises": ["~b", "~c", "(~f & ~b) -> b", "(~a & ~d) -> ~e", "(a & g) -> ~f"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0412", "premises": ["~g", "(c) -> ~d", "(a) -> b", "(~c & ~d) -> ~d", "(a) -> b", "(~a) -> c"], "query": "~g"}
{"gold": "refuted", "id": "dl-holdout-v1-0413", "premises": ["~d", "~e", "(~g) -> c", "(c) -> e", "(~c & ~g) -> ~d"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0414", "premises": ["a", "c", "(~e & c) -> ~b", "(~f & ~a) -> ~e"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0415", "premises": ["~c", "(~c) -> ~b", "(a & ~d) -> ~c", "(~c & ~d) -> ~a"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0416", "premises": ["b", "(d & b) -> d", "(f & ~b) -> ~f"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0417", "premises": ["~c", "(c) -> ~a", "(d) -> ~c", "(~d & ~c) -> c"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0418", "premises": ["b", "f", "(b) -> e", "(~b) -> ~e", "(~b) -> ~b", "(~f & c) -> ~b", "(c) -> ~e"], "query": "~f"}
{"gold": "refuted", "id": "dl-holdout-v1-0419", "premises": ["g", "b", "(~c) -> ~g", "(c) -> ~d"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0420", "premises": ["~g", "c", "(f & g) -> ~c", "(c & g) -> ~f", "(f & ~d) -> ~d", "(~a & ~d) -> ~c"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0421", "premises": ["b", "f", "g", "(d & a) -> a", "(f & ~c) -> ~f"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0422", "premises": ["c", "b", "~e", "(~d) -> a", "(~g & b) -> g", "(e & b) -> ~c"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0423", "premises": ["~d", "f", "(~d & ~c) -> e", "(~f) -> ~d", "(~c & d) -> ~a", "(~a & ~b) -> ~a"], "query": "~e"}
{"gold": "entailed", "id": "dl-holdout-v1-0424", "premises": ["e", "~c", "(b & ~a) -> ~b", "(d) -> b", "(b & f) -> b", "(~b) -> ~c"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0425", "premises": ["c", "~g", "(e & ~g) -> d", "(g) -> ~a", "(c & ~b) -> ~e"], "query": "~c"}
{"gold": "refuted", "id": "dl-holdout-v1-0426", "premises": ["d", "(c) -> ~c", "(~f & c) -> d", "(d) -> e"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0427", "premises": ["~a", "~b", "g", "(f & ~d) -> ~e", "(~f) -> ~e", "(g) -> ~e", "(a & e) -> ~f", "(~b) -> ~d"], "query": "a"}
{"gold": "entailed", "id": "dl-holdout-v1-0428", "premises": ["g", "d", "(~b) -> e", "(~b) -> ~e", "(~e) -> b", "(e) -> ~d"], "query": "g"}
{"gold": "refuted", "id": "dl-holdout-v1-0429", "premises": ["~c", "~a", "g", "(~e) -> a", "(~g) -> d", "(~e) -> ~a"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0430", "premises": ["d", "~e", "(~d) -> f", "(~g) -> ~d", "(d) -> f", "(~f) -> d"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0431", "premises": ["g", "a", "(d) -> ~c", "(~d & e) -> ~e", "(e) -> ~d", "(a) -> d"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0432", "premises": ["~a", "(e & b) -> ~a", "(g) -> ~d", "(~c) -> ~f"], "query": "~g"}
{"gold": "refuted", "id": "dl-holdout-v1-0433", "premises": ["a", "g", "(~g & d) -> b", "(~g & e) -> b", "(~g) -> ~g", "(e) -> ~b"], "query": "~a"}
{"gold": "refuted", "id": "dl-holdout-v1-0434", "premises": ["~b", "(d) -> e", "(d & e) -> ~b", "(~a & ~e) -> d", "(e) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0435", "premises": ["~a", "(~f & ~g) -> b", "(~g & ~d) -> ~b", "(e & f) -> f"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0436", "premises": ["~d", "(~e) -> f", "(~e & g) -> ~f", "(e & ~f) -> e", "(~d & ~e) -> e"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0437", "premises": ["d", "a", "~b", "(~d) -> a", "(b & a) -> ~a"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0438", "premises": ["d", "(f & ~d) -> e", "(~c & b) -> ~e", "(f) -> e", "(b) -> d"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0439", "premises": ["d", "f", "(~c & ~b) -> ~b", "(~f & a) -> a"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0440", "premises": ["b", "(~g & b) -> ~b", "(f) -> ~g", "(~d & b) -> ~a", "(~d) -> ~a", "(g) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0441", "premises": ["~c", "(e & ~d) -> g", "(g) -> ~e", "(~e & g) -> g"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0442", "premises": ["~d", "g", "(~f) -> d", "(~a) -> e", "(~d) -> ~e", "(~a) -> f", "(~d) -> ~e"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0443", "premises": ["e", "b", "~d", "(~b & d) -> ~b", "(~d & a) -> ~b", "(~a) -> b", "(f & ~d) -> c", "(f & g) -> ~c"], "query": "~c"}
{"gold": "entailed", "id": "dl-holdout-v1-0444", "premises": ["e", "(e & b) -> b", "(e) -> ~f", "(a & ~f) -> f", "(e) -> ~b", "(~f & b) -> ~b"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0445", "premises": ["b", "f", "e", "(a & ~b) -> ~b", "(c) -> a"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0446", "premises": ["~d", "(b & ~d) -> ~e", "(b) -> ~a", "(~b & d) -> a"], "query": "~d"}
{"gold": "refuted", "id": "dl-holdout-v1-0447", "premises": ["b", "~a", "(f & d) -> ~b", "(~f & ~a) -> ~d", "(~d) -> ~a", "(~d & ~a) -> ~f", "(a & ~b) -> ~f"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0448", "premises": ["~d", "b", "(~b) -> e", "(~e) -> b"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0449", "premises": ["b", "(d & ~b) -> ~b", "(d) -> g"], "query": "~c"}
{"gold": "unknown", "id": "dl-holdout-v1-0450", "premises": ["g", "b", "(c) -> ~b", "(f) -> d"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0451", "premises": ["e", "~a", "(~a) -> ~a", "(~g) -> ~c", "(b) -> ~c"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0452", "premises": ["f", "~d", "(~g) -> g", "(~d) -> b", "(f) -> ~e", "(b & ~d) -> a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0453", "premises": ["~d", "(f & e) -> ~d", "(~b) -> e"], "query": "e"}
{"gold": "refuted", "id": "dl-holdout-v1-0454", "premises": ["e", "d", "~b", "(~d) -> b", "(~e & g) -> g"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0455", "premises": ["~f", "~e", "(~e) -> b", "(d) -> ~e", "(~a) -> ~d", "(~a) -> b"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0456", "premises": ["~e", "(~e & ~b) -> ~a", "(~a) -> ~b", "(~b) -> ~b"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0457", "premises": ["~e", "~b", "(~g) -> ~g", "(~d & ~b) -> ~c", "(~d & c) -> g", "(g & ~d) -> ~b"], "query": "~g"}
{"gold": "entailed", "id": "dl-holdout-v1-0458", "premises": ["~g", "(a) -> a", "(b) -> ~a", "(~b) -> f"], "query": "~g"}
{"gold": "unknown", "id": "dl-holdout-v1-0459", "premises": ["~g", "b", "(a) -> e", "(~b) -> f", "(~c & ~d) -> ~d", "(~d) -> ~b", "(~e & ~g) -> ~e"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0460", "premises": ["~c", "(~d) -> c", "(e) -> ~e", "(~a & ~c) -> ~e"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0461", "premises": ["e", "(c) -> ~b", "(a) -> ~d"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0462", "premises": ["a", "(~f) -> ~g", "(~d & ~e) -> ~a", "(~e) -> ~f", "(g & d) -> a", "(~e) -> f"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0463", "premises": ["~a", "(~f & ~g) -> c", "(f & ~c) -> ~f", "(b & f) -> g", "(~g & c) -> ~a", "(f & b) -> c"], "query": "~f"}
{"gold": "unknown", "id": "dl-holdout-v1-0464", "premises": ["f", "(~f & ~e) -> e", "(f & c) -> f", "(a & ~e) -> ~e"], "query": "c"}
{"gold": "entailed", "id": "dl-holdout-v1-0465", "premises": ["f", "e", "(~g) -> ~e", "(g & ~f) -> ~b", "(~g & ~b) -> ~b", "(g & ~f) -> ~e", "(b) -> f"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0466", "premises": ["a", "f", "(~g & ~f) -> ~g", "(g & ~b) -> ~g", "(c & a) -> a"], "query": "a"}
{"gold": "unknown", "id": "dl-holdout-v1-0467", "premises": ["e", "f", "(b) -> f", "(c) -> ~g", "(b) -> b"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0468", "premises": ["~f", "~b", "(~f & ~b) -> ~c", "(~c & e) -> ~e", "(b) -> c", "(~g & c) -> ~c", "(~g & c) -> ~f"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0469", "premises": ["~g", "(f) -> ~d", "(~f) -> g", "(~g & d) -> ~d"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0470", "premises": ["~f", "d", "(a) -> c", "(a) -> ~f", "(~c) -> ~c"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0471", "premises": ["~b", "~f", "(d) -> ~e", "(e) -> ~b", "(a & c) -> ~e"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0472", "premises": ["~g", "(g & c) -> b", "(~d & ~b) -> ~d", "(d & ~b) -> d", "(~g) -> b", "(d) -> c"], "query": "c"}
{"gold": "unknown", "id": "dl-holdout-v1-0473", "premises": ["~e", "(e) -> g", "(a) -> a", "(~g) -> d", "(g) -> ~g"], "query": "a"}
{"gold": "entailed", "id": "dl-holdout-v1-0474", "premises": ["c", "(f) -> g", "(~f) -> b", "(b & ~c) -> ~g", "(b) -> ~f"], "query": "c"}
{"gold": "refuted", "id": "dl-holdout-v1-0475", "premises": ["~f", "~e", "(~b & ~f) -> f", "(~b & f) -> e", "(~b) -> ~b", "(~b & f) -> ~f", "(e) -> e"], "query": "f"}
{"gold": "refuted", "id": "dl-holdout-v1-0476", "premises": ["~g", "(~c & ~e) -> ~d", "(~e) -> c"], "query": "g"}
{"gold": "entailed", "id": "dl-holdout-v1-0477", "premises": ["~g", "(~d & c) -> f", "(f & e) -> ~e", "(f) -> c", "(g & ~f) -> ~e", "(e) -> g"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0478", "premises": ["~c", "~b", "(~g & c) -> c", "(d & f) -> f", "(c & ~d) -> g", "(g) -> ~d"], "query": "d"}
{"gold": "entailed", "id": "dl-holdout-v1-0479", "premises": ["g", "c", "~a", "(f) -> d", "(d & g) -> d", "(~a) -> ~b", "(g) -> e"], "query": "e"}
{"gold": "entailed", "id": "dl-holdout-v1-0480", "premises": ["~a", "(a) -> e", "(c) -> ~f", "(f & g) -> ~a"], "query": "~a"}
{"gold": "unknown", "id": "dl-holdout-v1-0481", "premises": ["~e", "(~a & ~c) -> ~e", "(e & b) -> c", "(~e) -> b", "(c) -> ~b"], "query": "~a"}
{"gold": "entailed", "id": "dl-holdout-v1-0482", "premises": ["b", "(g) -> ~b", "(e) -> a"], "query": "b"}
{"gold": "unknown", "id": "dl-holdout-v1-0483", "premises": ["d", "f", "(b) -> f", "(~f & d) -> g", "(b) -> f", "(~b & ~g) -> ~g", "(~g & ~f) -> ~b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0484", "premises": ["b", "~g", "(~b & ~d) -> f", "(f) -> d", "(b & a) -> ~f", "(~d & ~f) -> d"], "query": "f"}
{"gold": "unknown", "id": "dl-holdout-v1-0485", "premises": ["f", "~e", "(~e & ~d) -> b", "(c) -> ~a"], "query": "d"}
{"gold": "refuted", "id": "dl-holdout-v1-0486", "premises": ["~b", "(d & ~c) -> ~e", "(c) -> ~d", "(b & ~e) -> ~c", "(g) -> ~e"], "query": "b"}
{"gold": "refuted", "id": "dl-holdout-v1-0487", "premises": ["~g", "(~e & f) -> e", "(b & e) -> e", "(~a) -> ~d", "(~g) -> ~c", "(~c) -> a"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0488", "premises": ["~b", "f", "(b) -> e", "(f & e) -> ~c", "(~d & ~a) -> ~b"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0489", "premises": ["~f", "(~c) -> ~f", "(c & ~f) -> f", "(g) -> g", "(e) -> g", "(c & ~e) -> e"], "query": "~e"}
{"gold": "refuted", "id": "dl-holdout-v1-0490", "premises": ["~g", "~e", "(~f) -> ~d", "(g) -> ~b", "(~g) -> ~a"], "query": "e"}
{"gold": "unknown", "id": "dl-holdout-v1-0491", "premises": ["e", "a", "d", "(~a) -> e", "(b) -> g", "(~e & b) -> g"], "query": "g"}
{"gold": "unknown", "id": "dl-holdout-v1-0492", "premises": ["~b", "(~a) -> ~c", "(f) -> ~c", "(e) -> f", "(b) -> g"], "query": "f"}
{"gold": "entailed", "id": "dl-holdout-v1-0493", "premises": ["d", "~g", "(~c) -> b", "(~d & ~b) -> d", "(~c & b) -> ~c"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0494", "premises": ["~e", "b", "~f", "(d & ~a) -> d", "(~g & ~e) -> ~c", "(c & a) -> ~g", "(c) -> c", "(d & c) -> b"], "query": "~d"}
{"gold": "unknown", "id": "dl-holdout-v1-0495", "premises": ["~e", "~a", "(~b) -> d", "(~b) -> f", "(~e) -> ~e"], "query": "d"}
{"gold": "unknown", "id": "dl-holdout-v1-0496", "premises": ["~g", "~d", "(~e) -> ~a", "(~e) -> ~a", "(a & ~d) -> ~d"], "query": "~e"}
{"gold": "unknown", "id": "dl-holdout-v1-0497", "premises": ["~c", "(~e & ~d) -> b", "(e) -> c"], "query": "b"}
{"gold": "entailed", "id": "dl-holdout-v1-0498", "premises": ["~f", "(~g) -> b", "(~d) -> e", "(~e) -> ~d", "(f) -> c", "(~f) -> ~b"], "query": "~b"}
{"gold": "unknown", "id": "dl-holdout-v1-0499", "premises": ["c", "(~f) -> g", "(b) -> f", "(f) -> ~a", "(~a) -> ~d", "(~f & c) -> g"], "query": "~e"}

228
evals/deductive_logic/oracle.py Normal file
View file

@ -0,0 +1,228 @@
"""Independent entailment oracle — the gold for the deductive-logic lane.
This is **deliberately a second, independent decision procedure**: a self-contained
recursive-descent parser plus brute-force truth-table model enumeration. It shares
**no code** with :mod:`generate.logic_canonical` (the ROBDD) or
:mod:`generate.proof_chain.entail` (the engine under test). Two independent sound
procedures agreeing on held-out random problems is real evidence the engine is
correct; a shared-code "oracle" would only prove the engine agrees with itself.
It is intentionally simple and slow (O(2^atoms)) — correctness by obviousness, not
performance. The lane keeps atom counts small so enumeration stays cheap.
Grammar / precedence match the ROBDD's so the same formula string means the same
thing in both procedures (the comparison is about the *decision*, not parsing):
iff < implies < or < and < not (implies right-associative)
"""
from __future__ import annotations
from itertools import product
from typing import Final
# --- independent tokenizer -------------------------------------------------
_OPS: Final[tuple[tuple[str, str], ...]] = (
("<->", "IFF"), ("↔", "IFF"), ("≡", "IFF"),
("->", "IMP"), ("→", "IMP"), ("⊃", "IMP"),
("∧", "AND"), ("&&", "AND"), ("&", "AND"),
("∨", "OR"), ("||", "OR"), ("|", "OR"),
("¬", "NOT"), ("~", "NOT"), ("!", "NOT"),
("(", "LP"), (")", "RP"),
)
_KW: Final[dict[str, str]] = {
"and": "AND", "or": "OR", "not": "NOT", "implies": "IMP",
"iff": "IFF", "true": "TRUE", "false": "FALSE",
}
class OracleError(ValueError):
"""Malformed formula — the oracle refuses to guess, same posture as the engine."""
def _tokenize(text: str) -> list[tuple[str, str]]:
toks: list[tuple[str, str]] = []
i, n = 0, len(text)
while i < n:
c = text[i]
if c.isspace():
i += 1
continue
hit = False
for spell, kind in _OPS:
if text.startswith(spell, i):
toks.append((kind, spell))
i += len(spell)
hit = True
break
if hit:
continue
if c.isalpha() or c == "_":
j = i + 1
while j < n and (text[j].isalnum() or text[j] == "_"):
j += 1
word = text[i:j]
toks.append((_KW.get(word.lower(), "ATOM"), word))
i = j
continue
raise OracleError(f"unexpected character {c!r}")
return toks
# --- independent recursive-descent parser ----------------------------------
class _P:
def __init__(self, toks: list[tuple[str, str]]) -> None:
self.toks = toks
self.i = 0
def _peek(self) -> tuple[str, str] | None:
return self.toks[self.i] if self.i < len(self.toks) else None
def _eat(self) -> tuple[str, str]:
if self.i >= len(self.toks):
raise OracleError("unexpected end of formula")
t = self.toks[self.i]
self.i += 1
return t
def parse(self) -> tuple:
if not self.toks:
raise OracleError("empty formula")
ast = self._iff()
if self.i != len(self.toks):
raise OracleError("trailing tokens")
return ast
def _iff(self) -> tuple:
node = self._imp()
while (t := self._peek()) and t[0] == "IFF":
self._eat()
node = ("iff", node, self._imp())
return node
def _imp(self) -> tuple:
node = self._or()
if (t := self._peek()) and t[0] == "IMP":
self._eat()
node = ("imp", node, self._imp()) # right-assoc
return node
def _or(self) -> tuple:
node = self._and()
while (t := self._peek()) and t[0] == "OR":
self._eat()
node = ("or", node, self._and())
return node
def _and(self) -> tuple:
node = self._not()
while (t := self._peek()) and t[0] == "AND":
self._eat()
node = ("and", node, self._not())
return node
def _not(self) -> tuple:
if (t := self._peek()) and t[0] == "NOT":
self._eat()
return ("not", self._not())
return self._atom()
def _atom(self) -> tuple:
kind, lex = self._eat()
if kind == "ATOM":
return ("atom", lex)
if kind == "TRUE":
return ("const", True)
if kind == "FALSE":
return ("const", False)
if kind == "LP":
inner = self._iff()
if self._eat()[0] != "RP":
raise OracleError("expected ')'")
return inner
raise OracleError(f"unexpected token {lex!r}")
def _atoms(ast: tuple) -> set[str]:
k = ast[0]
if k == "atom":
return {ast[1]}
if k == "const":
return set()
if k == "not":
return _atoms(ast[1])
return _atoms(ast[1]) | _atoms(ast[2])
def _eval(ast: tuple, env: dict[str, bool]) -> bool:
k = ast[0]
if k == "atom":
return env[ast[1]]
if k == "const":
return ast[1]
if k == "not":
return not _eval(ast[1], env)
a = _eval(ast[1], env)
b = _eval(ast[2], env)
if k == "and":
return a and b
if k == "or":
return a or b
if k == "imp":
return (not a) or b
if k == "iff":
return a == b
raise OracleError(f"unknown node {k!r}") # pragma: no cover
def _parse(formula: str) -> tuple:
return _P(_tokenize(formula)).parse()
# --- the oracle verdict ----------------------------------------------------
# Verdict strings match generate.proof_chain.entail.Entailment values exactly so the
# runner can compare engine.outcome.value to the oracle verdict directly.
ENTAILED: Final[str] = "entailed"
REFUTED: Final[str] = "refuted"
UNKNOWN: Final[str] = "unknown"
REFUSED: Final[str] = "refused"
def oracle_entailment(premises: tuple[str, ...], query: str) -> str:
"""Brute-force entailment verdict over all truth assignments.
Enumerates every assignment of the atoms appearing anywhere in premises+query;
a *model* is an assignment satisfying every premise. Returns:
``entailed`` if query holds in all models, ``refuted`` if in none,
``unknown`` if in some-but-not-all, ``refused`` if there are no models
(inconsistent premises) or anything fails to parse."""
try:
prem_asts = [_parse(p) for p in premises]
q_ast = _parse(query)
except OracleError:
return REFUSED
atoms = set(_atoms(q_ast))
for a in prem_asts:
atoms |= _atoms(a)
ordered = sorted(atoms)
models = 0
q_true = 0
for combo in product((False, True), repeat=len(ordered)):
env = dict(zip(ordered, combo))
if all(_eval(a, env) for a in prem_asts):
models += 1
if _eval(q_ast, env):
q_true += 1
if models == 0:
return REFUSED # inconsistent premises
if q_true == models:
return ENTAILED
if q_true == 0:
return REFUTED
return UNKNOWN

97
evals/deductive_logic/runner.py Normal file
View file

@ -0,0 +1,97 @@
"""Deductive-logic lane runner — scores the entailment engine against the oracle gold.
The honest capability metric for CORE's deterministic deduction. For each committed
case it runs :func:`generate.proof_chain.entail.evaluate_entailment` and compares the
outcome to the gold (computed by the independent truth-table oracle at generation).
Counts:
* ``correct`` — engine outcome == gold (a right deduction, including a right
``unknown``).
* ``wrong`` — engine outcome != gold and engine did not refuse (a confabulated
deduction — this MUST stay 0).
* ``refused`` — engine returned ``refused`` (should not happen on these
well-formed, consistent, propositional cases; counted separately, never as wrong).
A breakdown by gold class (entailed / refuted / unknown) is reported so the
"sizeable numbers" are visible: how many non-trivial entailments/refutations the
engine decides correctly, not just how many ``unknown``s it passes through.
Exits non-zero if ``wrong > 0`` (the floor).
"""
from __future__ import annotations
import json
import sys
from collections import Counter
from pathlib import Path
from generate.proof_chain.entail import Entailment, evaluate_entailment
_ROOT = Path(__file__).resolve().parent
def _load(path: Path) -> list[dict]:
with path.open(encoding="utf-8") as fh:
return [json.loads(line) for line in fh if line.strip()]
def build_report(cases: list[dict]) -> dict:
counts = Counter({"correct": 0, "wrong": 0, "refused": 0})
by_gold: Counter[str] = Counter()
correct_by_gold: Counter[str] = Counter()
wrong_examples: list[dict] = []
for case in cases:
gold = case["gold"]
by_gold[gold] += 1
verdict = evaluate_entailment(tuple(case["premises"]), case["query"])
got = verdict.outcome.value
if got == gold:
counts["correct"] += 1
correct_by_gold[gold] += 1
elif verdict.outcome is Entailment.REFUSED:
counts["refused"] += 1
else:
counts["wrong"] += 1
if len(wrong_examples) < 10:
wrong_examples.append(
{"id": case["id"], "gold": gold, "got": got,
"premises": case["premises"], "query": case["query"]}
)
return {
"n": len(cases),
"counts": dict(counts),
"by_gold": dict(by_gold),
"correct_by_gold": dict(correct_by_gold),
"wrong_examples": wrong_examples,
}
def _run(name: str, path: Path) -> dict:
report = build_report(_load(path))
c = report["counts"]
bg = report["by_gold"]
cbg = report["correct_by_gold"]
print(f"[{name}] n={report['n']} "
f"correct={c['correct']} wrong={c['wrong']} refused={c['refused']}")
print(f" gold mix: entailed={bg.get('entailed', 0)} "
f"refuted={bg.get('refuted', 0)} unknown={bg.get('unknown', 0)}")
print(f" correct by class: entailed={cbg.get('entailed', 0)} "
f"refuted={cbg.get('refuted', 0)} unknown={cbg.get('unknown', 0)}")
if report["wrong_examples"]:
print(" WRONG examples:")
for w in report["wrong_examples"]:
print(f" {w['id']}: gold={w['gold']} got={w['got']} "
f"premises={w['premises']} query={w['query']}")
return report
if __name__ == "__main__":
reports = {
"dev": _run("dev", _ROOT / "dev" / "cases.jsonl"),
"holdout-v1": _run("holdout-v1", _ROOT / "holdout" / "v1" / "cases.jsonl"),
}
total_wrong = sum(r["counts"]["wrong"] for r in reports.values())
sys.exit(1 if total_wrong > 0 else 0)

108
generate/proof_chain/entail.py Normal file
View file

@ -0,0 +1,108 @@
"""ADR-0206 — Propositional entailment operator (proof_chain phase 2.4).
The multi-hop inference operator ``gaps.md`` asked for and ADR-0205 deferred. Where
:func:`generate.proof_chain.rules.evaluate_modus_ponens` is **single-step** ("unique
conclusion among single-step modus ponens"), this is the full, sound **and complete**
propositional entailment decision built directly on the ADR-0201 ROBDD keystone:
premises ⊨ query iff (⋀ premises) → query is a tautology.
Because the ROBDD is a *canonical, complete* decision procedure for propositional
logic, this answers arbitrary multi-hop deductive queries (chains of implications,
conjunctive rules, contrapositive, disjunctive syllogism — anything propositional),
not just one modus-ponens step. ``wrong == 0`` is structural: a tautology check is
exact, never approximate, and the canonicalizer **refuses** (``LogicError``) rather
than guess on malformed / out-of-decidable-regime (quantified/predicate) input.
Four outcomes, all sound:
* ``ENTAILED`` — ``(⋀P) → Q`` is a tautology (Q holds in every model of P).
* ``REFUTED`` — ``(⋀P) → ¬Q`` is a tautology (Q fails in every model of P).
* ``UNKNOWN`` — neither; Q is true in some models of P and false in others.
* ``REFUSED`` — premises are inconsistent (no model — everything would follow
vacuously, so we decline an answer) **or** input is malformed / out-of-regime.
Honesty boundary (load-bearing): **propositional only**. Atoms are opaque Boolean
variables; predicate/quantified structure is out of regime and refuses (ADR-0201.1).
A grounded finite-entity problem (each predicate-entity pair → one atom) IS
propositional and in scope; an ungrounded ``forall x. P(x)`` is not.
"""
from __future__ import annotations
from dataclasses import dataclass
from enum import Enum
from typing import Final
from generate.logic_canonical import LogicError, canonicalize
class Entailment(str, Enum):
ENTAILED = "entailed"
REFUTED = "refuted"
UNKNOWN = "unknown"
REFUSED = "refused"
# Closed reason vocabulary (the mechanism makes exactly these distinctions).
TAUTOLOGICAL_IMPLICATION: Final[str] = "tautological_implication" # entailed
TAUTOLOGICAL_REFUTATION: Final[str] = "tautological_refutation" # refuted
UNDETERMINED: Final[str] = "undetermined" # unknown
INCONSISTENT_PREMISES: Final[str] = "inconsistent_premises" # refused
OUT_OF_REGIME_OR_MALFORMED: Final[str] = "out_of_regime_or_malformed" # refused
ENTAILMENT_REASONS: Final[frozenset[str]] = frozenset({
TAUTOLOGICAL_IMPLICATION,
TAUTOLOGICAL_REFUTATION,
UNDETERMINED,
INCONSISTENT_PREMISES,
OUT_OF_REGIME_OR_MALFORMED,
})
@dataclass(frozen=True, slots=True)
class EntailmentVerdict:
outcome: Entailment
reason: str
def _conjoin(premises: tuple[str, ...]) -> str:
"""Fully-parenthesized conjunction of the premise formulas (``true`` if empty).
Each premise is wrapped so its internal precedence cannot bleed across the
``&`` joins; an empty premise set is the always-true antecedent."""
if not premises:
return "true"
return " & ".join(f"({p})" for p in premises)
def evaluate_entailment(premises: tuple[str, ...], query: str) -> EntailmentVerdict:
"""Decide whether ``premises`` propositionally entail / refute ``query``.
Sound and complete over the propositional regime; refusal-first on anything
outside it. Never raises on a logic-domain error — every ``LogicError`` (and
its regime/budget subclasses) maps to a typed ``REFUSED`` verdict."""
try:
conj = _conjoin(premises)
conj_canon = canonicalize(conj)
if conj_canon.is_contradiction:
# No model satisfies the premises: from a contradiction everything
# follows. We decline rather than assert a vacuous entailment.
return EntailmentVerdict(Entailment.REFUSED, INCONSISTENT_PREMISES)
# Force the query through the canonicalizer too, so a malformed / out-of-
# regime query refuses even when the implication check would shortcut.
canonicalize(query)
entailed = canonicalize(f"({conj}) -> ({query})").is_tautology
refuted = canonicalize(f"({conj}) -> (~({query}))").is_tautology
except LogicError:
return EntailmentVerdict(Entailment.REFUSED, OUT_OF_REGIME_OR_MALFORMED)
if entailed and refuted:
# Only possible if the premises are inconsistent, already handled above;
# defensive — never assert a contradiction-derived answer.
return EntailmentVerdict(Entailment.REFUSED, INCONSISTENT_PREMISES)
if entailed:
return EntailmentVerdict(Entailment.ENTAILED, TAUTOLOGICAL_IMPLICATION)
if refuted:
return EntailmentVerdict(Entailment.REFUTED, TAUTOLOGICAL_REFUTATION)
return EntailmentVerdict(Entailment.UNKNOWN, UNDETERMINED)

140
tests/test_deductive_logic_entail.py Normal file
View file

@ -0,0 +1,140 @@
"""ADR-0206 — propositional entailment operator + the deductive-logic lane.
Three obligations, each able to fail loudly under the violation it guards:
1. **Soundness on classic inference shapes** — hand-verified modus ponens, multi-hop
chains, modus tollens, disjunctive/hypothetical syllogism, and a genuine
``unknown`` all decide correctly.
2. **Refusal-first boundary** — inconsistent premises, out-of-regime (quantified)
and malformed input all return a typed ``REFUSED`` rather than a guess.
3. **wrong=0 vs an independent oracle** — a deterministic fuzz cross-checks the
ROBDD engine against the brute-force truth-table oracle on fresh random
problems; any disagreement is a real soundness bug and fails this test. Plus the
committed held-out lane holds ``wrong == 0``.
"""
from __future__ import annotations
import random
import pytest
from evals.deductive_logic.generate import _make_case
from evals.deductive_logic.oracle import oracle_entailment
from evals.deductive_logic.runner import _ROOT, _load, build_report
from generate.proof_chain.entail import (
INCONSISTENT_PREMISES,
OUT_OF_REGIME_OR_MALFORMED,
Entailment,
evaluate_entailment,
)
# --- 1. classic inference shapes (hand-verified) ---------------------------
@pytest.mark.parametrize(
"premises,query,expected",
[
# modus ponens
(("P", "P -> Q"), "Q", Entailment.ENTAILED),
# multi-hop chain: P, P->Q, Q->R ⊨ R
(("P", "P -> Q", "Q -> R"), "R", Entailment.ENTAILED),
# modus tollens: P->Q, ~Q ⊨ ~P
(("P -> Q", "~Q"), "~P", Entailment.ENTAILED),
# disjunctive syllogism: P|Q, ~P ⊨ Q
(("P | Q", "~P"), "Q", Entailment.ENTAILED),
# hypothetical syllogism (the conclusion is itself an implication)
(("P -> Q", "Q -> R"), "P -> R", Entailment.ENTAILED),
# refutation: P, P->~Q ⊨ ~Q (so Q is REFUTED)
(("P", "P -> ~Q"), "Q", Entailment.REFUTED),
# genuinely undetermined: nothing forces Q either way
(("P", "R -> Q"), "Q", Entailment.UNKNOWN),
# conjunctive antecedent rule: A, B, (A & B)->C ⊨ C
(("A", "B", "(A & B) -> C"), "C", Entailment.ENTAILED),
# conjunctive rule with a missing conjunct: A, (A & B)->C ⊭ C
(("A", "(A & B) -> C"), "C", Entailment.UNKNOWN),
],
)
def test_classic_inferences(premises, query, expected) -> None:
assert evaluate_entailment(premises, query).outcome is expected
# --- 2. refusal-first boundary --------------------------------------------
def test_inconsistent_premises_refuse() -> None:
v = evaluate_entailment(("P", "~P"), "Q")
assert v.outcome is Entailment.REFUSED
assert v.reason == INCONSISTENT_PREMISES
def test_quantified_input_refuses_out_of_regime() -> None:
v = evaluate_entailment(("forall x. P",), "P")
assert v.outcome is Entailment.REFUSED
assert v.reason == OUT_OF_REGIME_OR_MALFORMED
def test_predicate_application_refuses() -> None:
assert evaluate_entailment(("rough(x)",), "P").outcome is Entailment.REFUSED
def test_malformed_query_refuses() -> None:
assert evaluate_entailment(("P",), "P & & Q").outcome is Entailment.REFUSED
# --- 3a. wrong=0 vs the independent oracle (deterministic fuzz) -------------
def test_engine_matches_independent_oracle_fuzz() -> None:
"""ROBDD engine vs brute-force truth-table oracle on 3000 fresh random cases.
These are two independently-coded sound decision procedures. A single
disagreement means one of them is wrong — the property the GSM8K composer
could never establish. Deterministic seed for reproducibility."""
rng = random.Random(424242)
checked = disagreements = 0
for i in range(3000):
case = _make_case(rng, f"t-{i}")
if case is None:
# generator-discarded == oracle said inconsistent; engine must REFUSE too
continue
checked += 1
got = evaluate_entailment(tuple(case["premises"]), case["query"]).outcome.value
if got != case["gold"]:
disagreements += 1
assert checked > 1500, f"fuzz produced too few definite cases ({checked})"
assert disagreements == 0, f"{disagreements} engine/oracle disagreements"
def test_engine_refuses_every_inconsistent_case() -> None:
"""The complement: when the oracle reports inconsistency, the engine must also
refuse (never silently 'decide' from a contradiction)."""
rng = random.Random(515151)
seen_inconsistent = 0
for _ in range(4000):
k = rng.randint(2, 4)
atoms = [chr(ord("a") + j) for j in range(k)]
prem = [rng.choice([at, f"~{at}"]) for at in atoms] + [
rng.choice([at, f"~{at}"]) for at in atoms
]
query = rng.choice(atoms)
if oracle_entailment(tuple(prem), query) == "refused":
seen_inconsistent += 1
assert evaluate_entailment(tuple(prem), query).outcome is Entailment.REFUSED
assert seen_inconsistent > 0 # the test actually exercised the path
# --- 3b. committed held-out lane holds wrong=0 -----------------------------
def test_holdout_lane_wrong_is_zero() -> None:
report = build_report(_load(_ROOT / "holdout" / "v1" / "cases.jsonl"))
assert report["n"] == 500
assert report["counts"]["wrong"] == 0
# the sizeable, honest signal: non-trivial deductions decided correctly
cbg = report["correct_by_gold"]
assert cbg.get("entailed", 0) >= 50
assert cbg.get("refuted", 0) >= 50
def test_dev_lane_wrong_is_zero() -> None:
report = build_report(_load(_ROOT / "dev" / "cases.jsonl"))
assert report["n"] == 200
assert report["counts"]["wrong"] == 0