Hugging Face's logo

Spaces:
Laborator
/
qverify
Running

App Files Community
Laborator commited on
Commit
cde4ea2
·
verified ·
1 Parent(s): 3039fea

v1.0.0 — qverify-mini-50 dataset + report

Browse files
Files changed (6) hide show
  1. benchmarks/qverify_mini/README.md +75 -0
  2. benchmarks/qverify_mini/dataset.json +2433 -0
  3. benchmarks/results/qverify_mini_simulator/accuracy.png +0 -0
  4. benchmarks/results/qverify_mini_simulator/latency.png +0 -0
  5. benchmarks/results/qverify_mini_simulator/qubits.png +0 -0
  6. benchmarks/results/qverify_mini_simulator/report.json +515 -0
benchmarks/qverify_mini/README.md ADDED
@@ -0,0 +1,75 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # qverify-mini-50
2
+
3
+ A 50-example hand-crafted benchmark for the QVerify verifier. Every CNF is
4
+ small enough (1-9 distinct atoms) to fit comfortably under the 16-qubit
5
+ PennyLane statevector ceiling, every label is validated against the PySAT
6
+ Glucose3 oracle before commit, and every record carries a pre-rendered CNF
7
+ so the verifier runs without a translator.
8
+
9
+ The dataset exists because the public NL benchmarks (ProofWriter, RuleTaker)
10
+ produce CNFs whose atom counts dwarf the simulator ceiling once grounded;
11
+ those datasets exercise the *translation* path but starve the *verifier*.
12
+ qverify-mini-50 covers the inverse: it stresses the verifier on hand-picked
13
+ SAT/UNSAT patterns where the ground truth is unambiguous.
14
+
15
+ ## Composition
16
+
17
+ | Category | Examples | Pattern |
18
+ | --- | --- | --- |
19
+ | A — propositional trivia | 8 (4 SAT / 4 UNSAT) | single atoms, conjunctions, direct contradictions |
20
+ | B — modus ponens | 6 (3 / 3) | `(¬P ∨ Q) ∧ P` chains, with and without contradicting `¬Q` |
21
+ | C — transitivity | 6 (3 / 3) | three-step implication chains, with and without UNSAT terminator |
22
+ | D — resolution | 6 (3 / 3) | clause pairs that resolve to a single literal, plus full XOR |
23
+ | E — pigeonhole-tiny | 4 (2 / 2) | 2p1h, 2p2h, 3p2h (classic), 3p3h |
24
+ | F — grounded first-order | 10 (5 / 5) | `Cat(Tom)`, `Bird(Robin)`, two-constant universals |
25
+ | G — AND/OR mixes | 10 (5 / 5) | three-way disjunctions, exactly-one cardinality, six-atom mixes |
26
+ | **Total** | **50 (25 / 25)** | |
27
+
28
+ ## Atom-count distribution
29
+
30
+ All examples fall in the range `1 <= atoms <= 9`. The
31
+ 3-pigeon-3-hole formula (e04) is the largest at 9 distinct atoms.
32
+
33
+ ## Schema
34
+
35
+ ```json
36
+ {
37
+ "id": "a01",
38
+ "description": "Single positive atom P",
39
+ "rendered_cnf": {
40
+ "clauses": [[{"predicate": "P", "args": [], "negated": false}]]
41
+ },
42
+ "label": "consistent",
43
+ "mode": "consistency",
44
+ "atom_count": 1
45
+ }
46
+ ```
47
+
48
+ `label` is the consistency-mode verdict: `"consistent"` when the formula is
49
+ SAT, `"inconsistent"` when UNSAT. `mode` is always `"consistency"` in v1.0.
50
+
51
+ ## Reproduce
52
+
53
+ ```bash
54
+ python scripts/run_benchmarks.py --dataset qverify-mini --backend simulator \
55
+ --output benchmarks/results/qverify_mini_simulator
56
+ ```
57
+
58
+ The runner emits `report.json` plus three PNG charts under the output
59
+ directory. The simulator finishes the full 50-example sweep in well under
60
+ a minute on a CPU-only machine.
61
+
62
+ ## Why hand-crafted?
63
+
64
+ The verifier's correctness is a property of the SAT-checking pipeline
65
+ (grounding -> Grover oracle synthesis -> simulator backend -> classical
66
+ post-check). To measure it honestly we need:
67
+
68
+ 1. CNFs small enough to actually run on the simulator,
69
+ 2. ground-truth labels that are *not* derived from the verifier itself,
70
+ 3. coverage of the failure modes that matter (resolution chains,
71
+ pigeonhole, modus ponens contradictions).
72
+
73
+ A hand-designed mini benchmark satisfies all three. The labels were
74
+ generated by PySAT before the JSON was written, so every record's gold
75
+ verdict is independent of QVerify's own implementation.
benchmarks/qverify_mini/dataset.json ADDED
@@ -0,0 +1,2433 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ [
2
+ {
3
+ "id": "a01",
4
+ "description": "Single positive atom P",
5
+ "rendered_cnf": {
6
+ "clauses": [
7
+ [
8
+ {
9
+ "predicate": "P",
10
+ "args": [],
11
+ "negated": false
12
+ }
13
+ ]
14
+ ]
15
+ },
16
+ "label": "consistent",
17
+ "mode": "consistency",
18
+ "atom_count": 1
19
+ },
20
+ {
21
+ "id": "a02",
22
+ "description": "Single negative atom \u00acP",
23
+ "rendered_cnf": {
24
+ "clauses": [
25
+ [
26
+ {
27
+ "predicate": "P",
28
+ "args": [],
29
+ "negated": true
30
+ }
31
+ ]
32
+ ]
33
+ },
34
+ "label": "consistent",
35
+ "mode": "consistency",
36
+ "atom_count": 1
37
+ },
38
+ {
39
+ "id": "a03",
40
+ "description": "Direct contradiction P \u2227 \u00acP",
41
+ "rendered_cnf": {
42
+ "clauses": [
43
+ [
44
+ {
45
+ "predicate": "P",
46
+ "args": [],
47
+ "negated": false
48
+ }
49
+ ],
50
+ [
51
+ {
52
+ "predicate": "P",
53
+ "args": [],
54
+ "negated": true
55
+ }
56
+ ]
57
+ ]
58
+ },
59
+ "label": "inconsistent",
60
+ "mode": "consistency",
61
+ "atom_count": 1
62
+ },
63
+ {
64
+ "id": "a04",
65
+ "description": "Disjunction P \u2228 Q",
66
+ "rendered_cnf": {
67
+ "clauses": [
68
+ [
69
+ {
70
+ "predicate": "P",
71
+ "args": [],
72
+ "negated": false
73
+ },
74
+ {
75
+ "predicate": "Q",
76
+ "args": [],
77
+ "negated": false
78
+ }
79
+ ]
80
+ ]
81
+ },
82
+ "label": "consistent",
83
+ "mode": "consistency",
84
+ "atom_count": 2
85
+ },
86
+ {
87
+ "id": "a05",
88
+ "description": "Force false: \u00acP \u2227 \u00acQ \u2227 (P \u2228 Q)",
89
+ "rendered_cnf": {
90
+ "clauses": [
91
+ [
92
+ {
93
+ "predicate": "P",
94
+ "args": [],
95
+ "negated": true
96
+ }
97
+ ],
98
+ [
99
+ {
100
+ "predicate": "Q",
101
+ "args": [],
102
+ "negated": true
103
+ }
104
+ ],
105
+ [
106
+ {
107
+ "predicate": "P",
108
+ "args": [],
109
+ "negated": false
110
+ },
111
+ {
112
+ "predicate": "Q",
113
+ "args": [],
114
+ "negated": false
115
+ }
116
+ ]
117
+ ]
118
+ },
119
+ "label": "inconsistent",
120
+ "mode": "consistency",
121
+ "atom_count": 2
122
+ },
123
+ {
124
+ "id": "a06",
125
+ "description": "Conjunction P \u2227 Q",
126
+ "rendered_cnf": {
127
+ "clauses": [
128
+ [
129
+ {
130
+ "predicate": "P",
131
+ "args": [],
132
+ "negated": false
133
+ }
134
+ ],
135
+ [
136
+ {
137
+ "predicate": "Q",
138
+ "args": [],
139
+ "negated": false
140
+ }
141
+ ]
142
+ ]
143
+ },
144
+ "label": "consistent",
145
+ "mode": "consistency",
146
+ "atom_count": 2
147
+ },
148
+ {
149
+ "id": "a07",
150
+ "description": "Both true but at-most-one: P \u2227 Q \u2227 (\u00acP \u2228 \u00acQ)",
151
+ "rendered_cnf": {
152
+ "clauses": [
153
+ [
154
+ {
155
+ "predicate": "P",
156
+ "args": [],
157
+ "negated": false
158
+ }
159
+ ],
160
+ [
161
+ {
162
+ "predicate": "Q",
163
+ "args": [],
164
+ "negated": false
165
+ }
166
+ ],
167
+ [
168
+ {
169
+ "predicate": "P",
170
+ "args": [],
171
+ "negated": true
172
+ },
173
+ {
174
+ "predicate": "Q",
175
+ "args": [],
176
+ "negated": true
177
+ }
178
+ ]
179
+ ]
180
+ },
181
+ "label": "inconsistent",
182
+ "mode": "consistency",
183
+ "atom_count": 2
184
+ },
185
+ {
186
+ "id": "a08",
187
+ "description": "XOR plus equivalence: 4-clause UNSAT",
188
+ "rendered_cnf": {
189
+ "clauses": [
190
+ [
191
+ {
192
+ "predicate": "P",
193
+ "args": [],
194
+ "negated": false
195
+ },
196
+ {
197
+ "predicate": "Q",
198
+ "args": [],
199
+ "negated": false
200
+ }
201
+ ],
202
+ [
203
+ {
204
+ "predicate": "P",
205
+ "args": [],
206
+ "negated": true
207
+ },
208
+ {
209
+ "predicate": "Q",
210
+ "args": [],
211
+ "negated": true
212
+ }
213
+ ],
214
+ [
215
+ {
216
+ "predicate": "P",
217
+ "args": [],
218
+ "negated": false
219
+ },
220
+ {
221
+ "predicate": "Q",
222
+ "args": [],
223
+ "negated": true
224
+ }
225
+ ],
226
+ [
227
+ {
228
+ "predicate": "P",
229
+ "args": [],
230
+ "negated": true
231
+ },
232
+ {
233
+ "predicate": "Q",
234
+ "args": [],
235
+ "negated": false
236
+ }
237
+ ]
238
+ ]
239
+ },
240
+ "label": "inconsistent",
241
+ "mode": "consistency",
242
+ "atom_count": 2
243
+ },
244
+ {
245
+ "id": "b01",
246
+ "description": "Modus ponens premise: (\u00acP \u2228 Q) \u2227 P",
247
+ "rendered_cnf": {
248
+ "clauses": [
249
+ [
250
+ {
251
+ "predicate": "P",
252
+ "args": [],
253
+ "negated": true
254
+ },
255
+ {
256
+ "predicate": "Q",
257
+ "args": [],
258
+ "negated": false
259
+ }
260
+ ],
261
+ [
262
+ {
263
+ "predicate": "P",
264
+ "args": [],
265
+ "negated": false
266
+ }
267
+ ]
268
+ ]
269
+ },
270
+ "label": "consistent",
271
+ "mode": "consistency",
272
+ "atom_count": 2
273
+ },
274
+ {
275
+ "id": "b02",
276
+ "description": "Modus ponens contradiction: above \u2227 \u00acQ",
277
+ "rendered_cnf": {
278
+ "clauses": [
279
+ [
280
+ {
281
+ "predicate": "P",
282
+ "args": [],
283
+ "negated": true
284
+ },
285
+ {
286
+ "predicate": "Q",
287
+ "args": [],
288
+ "negated": false
289
+ }
290
+ ],
291
+ [
292
+ {
293
+ "predicate": "P",
294
+ "args": [],
295
+ "negated": false
296
+ }
297
+ ],
298
+ [
299
+ {
300
+ "predicate": "Q",
301
+ "args": [],
302
+ "negated": true
303
+ }
304
+ ]
305
+ ]
306
+ },
307
+ "label": "inconsistent",
308
+ "mode": "consistency",
309
+ "atom_count": 2
310
+ },
311
+ {
312
+ "id": "b03",
313
+ "description": "Two-step MP chain: (\u00acP \u2228 Q) \u2227 (\u00acQ \u2228 R) \u2227 P",
314
+ "rendered_cnf": {
315
+ "clauses": [
316
+ [
317
+ {
318
+ "predicate": "P",
319
+ "args": [],
320
+ "negated": true
321
+ },
322
+ {
323
+ "predicate": "Q",
324
+ "args": [],
325
+ "negated": false
326
+ }
327
+ ],
328
+ [
329
+ {
330
+ "predicate": "Q",
331
+ "args": [],
332
+ "negated": true
333
+ },
334
+ {
335
+ "predicate": "R",
336
+ "args": [],
337
+ "negated": false
338
+ }
339
+ ],
340
+ [
341
+ {
342
+ "predicate": "P",
343
+ "args": [],
344
+ "negated": false
345
+ }
346
+ ]
347
+ ]
348
+ },
349
+ "label": "consistent",
350
+ "mode": "consistency",
351
+ "atom_count": 3
352
+ },
353
+ {
354
+ "id": "b04",
355
+ "description": "Two-step MP contradiction: above \u2227 \u00acR",
356
+ "rendered_cnf": {
357
+ "clauses": [
358
+ [
359
+ {
360
+ "predicate": "P",
361
+ "args": [],
362
+ "negated": true
363
+ },
364
+ {
365
+ "predicate": "Q",
366
+ "args": [],
367
+ "negated": false
368
+ }
369
+ ],
370
+ [
371
+ {
372
+ "predicate": "Q",
373
+ "args": [],
374
+ "negated": true
375
+ },
376
+ {
377
+ "predicate": "R",
378
+ "args": [],
379
+ "negated": false
380
+ }
381
+ ],
382
+ [
383
+ {
384
+ "predicate": "P",
385
+ "args": [],
386
+ "negated": false
387
+ }
388
+ ],
389
+ [
390
+ {
391
+ "predicate": "R",
392
+ "args": [],
393
+ "negated": true
394
+ }
395
+ ]
396
+ ]
397
+ },
398
+ "label": "inconsistent",
399
+ "mode": "consistency",
400
+ "atom_count": 3
401
+ },
402
+ {
403
+ "id": "b05",
404
+ "description": "Modus tollens setup: (\u00acP \u2228 Q) \u2227 \u00acQ (forces \u00acP)",
405
+ "rendered_cnf": {
406
+ "clauses": [
407
+ [
408
+ {
409
+ "predicate": "P",
410
+ "args": [],
411
+ "negated": true
412
+ },
413
+ {
414
+ "predicate": "Q",
415
+ "args": [],
416
+ "negated": false
417
+ }
418
+ ],
419
+ [
420
+ {
421
+ "predicate": "Q",
422
+ "args": [],
423
+ "negated": true
424
+ }
425
+ ]
426
+ ]
427
+ },
428
+ "label": "consistent",
429
+ "mode": "consistency",
430
+ "atom_count": 2
431
+ },
432
+ {
433
+ "id": "b06",
434
+ "description": "Modus tollens contradiction: above \u2227 P",
435
+ "rendered_cnf": {
436
+ "clauses": [
437
+ [
438
+ {
439
+ "predicate": "P",
440
+ "args": [],
441
+ "negated": true
442
+ },
443
+ {
444
+ "predicate": "Q",
445
+ "args": [],
446
+ "negated": false
447
+ }
448
+ ],
449
+ [
450
+ {
451
+ "predicate": "Q",
452
+ "args": [],
453
+ "negated": true
454
+ }
455
+ ],
456
+ [
457
+ {
458
+ "predicate": "P",
459
+ "args": [],
460
+ "negated": false
461
+ }
462
+ ]
463
+ ]
464
+ },
465
+ "label": "inconsistent",
466
+ "mode": "consistency",
467
+ "atom_count": 2
468
+ },
469
+ {
470
+ "id": "c01",
471
+ "description": "Three-step chain SAT: (\u00acA\u2228B)\u2227(\u00acB\u2228C)\u2227(\u00acC\u2228D)",
472
+ "rendered_cnf": {
473
+ "clauses": [
474
+ [
475
+ {
476
+ "predicate": "A",
477
+ "args": [],
478
+ "negated": true
479
+ },
480
+ {
481
+ "predicate": "B",
482
+ "args": [],
483
+ "negated": false
484
+ }
485
+ ],
486
+ [
487
+ {
488
+ "predicate": "B",
489
+ "args": [],
490
+ "negated": true
491
+ },
492
+ {
493
+ "predicate": "C",
494
+ "args": [],
495
+ "negated": false
496
+ }
497
+ ],
498
+ [
499
+ {
500
+ "predicate": "C",
501
+ "args": [],
502
+ "negated": true
503
+ },
504
+ {
505
+ "predicate": "D",
506
+ "args": [],
507
+ "negated": false
508
+ }
509
+ ]
510
+ ]
511
+ },
512
+ "label": "consistent",
513
+ "mode": "consistency",
514
+ "atom_count": 4
515
+ },
516
+ {
517
+ "id": "c02",
518
+ "description": "Three-step chain UNSAT: above \u2227 A \u2227 \u00acD",
519
+ "rendered_cnf": {
520
+ "clauses": [
521
+ [
522
+ {
523
+ "predicate": "A",
524
+ "args": [],
525
+ "negated": true
526
+ },
527
+ {
528
+ "predicate": "B",
529
+ "args": [],
530
+ "negated": false
531
+ }
532
+ ],
533
+ [
534
+ {
535
+ "predicate": "B",
536
+ "args": [],
537
+ "negated": true
538
+ },
539
+ {
540
+ "predicate": "C",
541
+ "args": [],
542
+ "negated": false
543
+ }
544
+ ],
545
+ [
546
+ {
547
+ "predicate": "C",
548
+ "args": [],
549
+ "negated": true
550
+ },
551
+ {
552
+ "predicate": "D",
553
+ "args": [],
554
+ "negated": false
555
+ }
556
+ ],
557
+ [
558
+ {
559
+ "predicate": "A",
560
+ "args": [],
561
+ "negated": false
562
+ }
563
+ ],
564
+ [
565
+ {
566
+ "predicate": "D",
567
+ "args": [],
568
+ "negated": true
569
+ }
570
+ ]
571
+ ]
572
+ },
573
+ "label": "inconsistent",
574
+ "mode": "consistency",
575
+ "atom_count": 4
576
+ },
577
+ {
578
+ "id": "c03",
579
+ "description": "Redundant transitivity: (\u00acA\u2228B)\u2227(\u00acB\u2228C)\u2227(\u00acA\u2228C)",
580
+ "rendered_cnf": {
581
+ "clauses": [
582
+ [
583
+ {
584
+ "predicate": "A",
585
+ "args": [],
586
+ "negated": true
587
+ },
588
+ {
589
+ "predicate": "B",
590
+ "args": [],
591
+ "negated": false
592
+ }
593
+ ],
594
+ [
595
+ {
596
+ "predicate": "B",
597
+ "args": [],
598
+ "negated": true
599
+ },
600
+ {
601
+ "predicate": "C",
602
+ "args": [],
603
+ "negated": false
604
+ }
605
+ ],
606
+ [
607
+ {
608
+ "predicate": "A",
609
+ "args": [],
610
+ "negated": true
611
+ },
612
+ {
613
+ "predicate": "C",
614
+ "args": [],
615
+ "negated": false
616
+ }
617
+ ]
618
+ ]
619
+ },
620
+ "label": "consistent",
621
+ "mode": "consistency",
622
+ "atom_count": 3
623
+ },
624
+ {
625
+ "id": "c04",
626
+ "description": "Transitive trigger: (\u00acA\u2228B)\u2227(\u00acB\u2228C)\u2227A",
627
+ "rendered_cnf": {
628
+ "clauses": [
629
+ [
630
+ {
631
+ "predicate": "A",
632
+ "args": [],
633
+ "negated": true
634
+ },
635
+ {
636
+ "predicate": "B",
637
+ "args": [],
638
+ "negated": false
639
+ }
640
+ ],
641
+ [
642
+ {
643
+ "predicate": "B",
644
+ "args": [],
645
+ "negated": true
646
+ },
647
+ {
648
+ "predicate": "C",
649
+ "args": [],
650
+ "negated": false
651
+ }
652
+ ],
653
+ [
654
+ {
655
+ "predicate": "A",
656
+ "args": [],
657
+ "negated": false
658
+ }
659
+ ]
660
+ ]
661
+ },
662
+ "label": "consistent",
663
+ "mode": "consistency",
664
+ "atom_count": 3
665
+ },
666
+ {
667
+ "id": "c05",
668
+ "description": "Transitive contradiction: above \u2227 \u00acC",
669
+ "rendered_cnf": {
670
+ "clauses": [
671
+ [
672
+ {
673
+ "predicate": "A",
674
+ "args": [],
675
+ "negated": true
676
+ },
677
+ {
678
+ "predicate": "B",
679
+ "args": [],
680
+ "negated": false
681
+ }
682
+ ],
683
+ [
684
+ {
685
+ "predicate": "B",
686
+ "args": [],
687
+ "negated": true
688
+ },
689
+ {
690
+ "predicate": "C",
691
+ "args": [],
692
+ "negated": false
693
+ }
694
+ ],
695
+ [
696
+ {
697
+ "predicate": "A",
698
+ "args": [],
699
+ "negated": false
700
+ }
701
+ ],
702
+ [
703
+ {
704
+ "predicate": "C",
705
+ "args": [],
706
+ "negated": true
707
+ }
708
+ ]
709
+ ]
710
+ },
711
+ "label": "inconsistent",
712
+ "mode": "consistency",
713
+ "atom_count": 3
714
+ },
715
+ {
716
+ "id": "c06",
717
+ "description": "Cyclic implications: (\u00acA\u2228B)\u2227(\u00acB\u2228A)\u2227A",
718
+ "rendered_cnf": {
719
+ "clauses": [
720
+ [
721
+ {
722
+ "predicate": "A",
723
+ "args": [],
724
+ "negated": true
725
+ },
726
+ {
727
+ "predicate": "B",
728
+ "args": [],
729
+ "negated": false
730
+ }
731
+ ],
732
+ [
733
+ {
734
+ "predicate": "B",
735
+ "args": [],
736
+ "negated": true
737
+ },
738
+ {
739
+ "predicate": "A",
740
+ "args": [],
741
+ "negated": false
742
+ }
743
+ ],
744
+ [
745
+ {
746
+ "predicate": "A",
747
+ "args": [],
748
+ "negated": false
749
+ }
750
+ ]
751
+ ]
752
+ },
753
+ "label": "consistent",
754
+ "mode": "consistency",
755
+ "atom_count": 2
756
+ },
757
+ {
758
+ "id": "d01",
759
+ "description": "Resolves Q: (P\u2228Q) \u2227 (\u00acP\u2228Q)",
760
+ "rendered_cnf": {
761
+ "clauses": [
762
+ [
763
+ {
764
+ "predicate": "P",
765
+ "args": [],
766
+ "negated": false
767
+ },
768
+ {
769
+ "predicate": "Q",
770
+ "args": [],
771
+ "negated": false
772
+ }
773
+ ],
774
+ [
775
+ {
776
+ "predicate": "P",
777
+ "args": [],
778
+ "negated": true
779
+ },
780
+ {
781
+ "predicate": "Q",
782
+ "args": [],
783
+ "negated": false
784
+ }
785
+ ]
786
+ ]
787
+ },
788
+ "label": "consistent",
789
+ "mode": "consistency",
790
+ "atom_count": 2
791
+ },
792
+ {
793
+ "id": "d02",
794
+ "description": "Resolution UNSAT: above \u2227 \u00acQ",
795
+ "rendered_cnf": {
796
+ "clauses": [
797
+ [
798
+ {
799
+ "predicate": "P",
800
+ "args": [],
801
+ "negated": false
802
+ },
803
+ {
804
+ "predicate": "Q",
805
+ "args": [],
806
+ "negated": false
807
+ }
808
+ ],
809
+ [
810
+ {
811
+ "predicate": "P",
812
+ "args": [],
813
+ "negated": true
814
+ },
815
+ {
816
+ "predicate": "Q",
817
+ "args": [],
818
+ "negated": false
819
+ }
820
+ ],
821
+ [
822
+ {
823
+ "predicate": "Q",
824
+ "args": [],
825
+ "negated": true
826
+ }
827
+ ]
828
+ ]
829
+ },
830
+ "label": "inconsistent",
831
+ "mode": "consistency",
832
+ "atom_count": 2
833
+ },
834
+ {
835
+ "id": "d03",
836
+ "description": "Resolves P: (P\u2228Q) \u2227 (P\u2228\u00acQ)",
837
+ "rendered_cnf": {
838
+ "clauses": [
839
+ [
840
+ {
841
+ "predicate": "P",
842
+ "args": [],
843
+ "negated": false
844
+ },
845
+ {
846
+ "predicate": "Q",
847
+ "args": [],
848
+ "negated": false
849
+ }
850
+ ],
851
+ [
852
+ {
853
+ "predicate": "P",
854
+ "args": [],
855
+ "negated": false
856
+ },
857
+ {
858
+ "predicate": "Q",
859
+ "args": [],
860
+ "negated": true
861
+ }
862
+ ]
863
+ ]
864
+ },
865
+ "label": "consistent",
866
+ "mode": "consistency",
867
+ "atom_count": 2
868
+ },
869
+ {
870
+ "id": "d04",
871
+ "description": "Resolution UNSAT: above \u2227 \u00acP",
872
+ "rendered_cnf": {
873
+ "clauses": [
874
+ [
875
+ {
876
+ "predicate": "P",
877
+ "args": [],
878
+ "negated": false
879
+ },
880
+ {
881
+ "predicate": "Q",
882
+ "args": [],
883
+ "negated": false
884
+ }
885
+ ],
886
+ [
887
+ {
888
+ "predicate": "P",
889
+ "args": [],
890
+ "negated": false
891
+ },
892
+ {
893
+ "predicate": "Q",
894
+ "args": [],
895
+ "negated": true
896
+ }
897
+ ],
898
+ [
899
+ {
900
+ "predicate": "P",
901
+ "args": [],
902
+ "negated": true
903
+ }
904
+ ]
905
+ ]
906
+ },
907
+ "label": "inconsistent",
908
+ "mode": "consistency",
909
+ "atom_count": 2
910
+ },
911
+ {
912
+ "id": "d05",
913
+ "description": "Three-clause resolution SAT",
914
+ "rendered_cnf": {
915
+ "clauses": [
916
+ [
917
+ {
918
+ "predicate": "P",
919
+ "args": [],
920
+ "negated": false
921
+ },
922
+ {
923
+ "predicate": "Q",
924
+ "args": [],
925
+ "negated": false
926
+ }
927
+ ],
928
+ [
929
+ {
930
+ "predicate": "P",
931
+ "args": [],
932
+ "negated": true
933
+ },
934
+ {
935
+ "predicate": "Q",
936
+ "args": [],
937
+ "negated": false
938
+ }
939
+ ],
940
+ [
941
+ {
942
+ "predicate": "P",
943
+ "args": [],
944
+ "negated": false
945
+ },
946
+ {
947
+ "predicate": "Q",
948
+ "args": [],
949
+ "negated": true
950
+ }
951
+ ]
952
+ ]
953
+ },
954
+ "label": "consistent",
955
+ "mode": "consistency",
956
+ "atom_count": 2
957
+ },
958
+ {
959
+ "id": "d06",
960
+ "description": "Four-corner UNSAT (full XOR contradiction)",
961
+ "rendered_cnf": {
962
+ "clauses": [
963
+ [
964
+ {
965
+ "predicate": "P",
966
+ "args": [],
967
+ "negated": false
968
+ },
969
+ {
970
+ "predicate": "Q",
971
+ "args": [],
972
+ "negated": false
973
+ }
974
+ ],
975
+ [
976
+ {
977
+ "predicate": "P",
978
+ "args": [],
979
+ "negated": true
980
+ },
981
+ {
982
+ "predicate": "Q",
983
+ "args": [],
984
+ "negated": false
985
+ }
986
+ ],
987
+ [
988
+ {
989
+ "predicate": "P",
990
+ "args": [],
991
+ "negated": false
992
+ },
993
+ {
994
+ "predicate": "Q",
995
+ "args": [],
996
+ "negated": true
997
+ }
998
+ ],
999
+ [
1000
+ {
1001
+ "predicate": "P",
1002
+ "args": [],
1003
+ "negated": true
1004
+ },
1005
+ {
1006
+ "predicate": "Q",
1007
+ "args": [],
1008
+ "negated": true
1009
+ }
1010
+ ]
1011
+ ]
1012
+ },
1013
+ "label": "inconsistent",
1014
+ "mode": "consistency",
1015
+ "atom_count": 2
1016
+ },
1017
+ {
1018
+ "id": "e01",
1019
+ "description": "2-pigeon-1-hole UNSAT (each pigeon needs a hole, but only one hole)",
1020
+ "rendered_cnf": {
1021
+ "clauses": [
1022
+ [
1023
+ {
1024
+ "predicate": "P1H1",
1025
+ "args": [],
1026
+ "negated": false
1027
+ }
1028
+ ],
1029
+ [
1030
+ {
1031
+ "predicate": "P2H1",
1032
+ "args": [],
1033
+ "negated": false
1034
+ }
1035
+ ],
1036
+ [
1037
+ {
1038
+ "predicate": "P1H1",
1039
+ "args": [],
1040
+ "negated": true
1041
+ },
1042
+ {
1043
+ "predicate": "P2H1",
1044
+ "args": [],
1045
+ "negated": true
1046
+ }
1047
+ ]
1048
+ ]
1049
+ },
1050
+ "label": "inconsistent",
1051
+ "mode": "consistency",
1052
+ "atom_count": 2
1053
+ },
1054
+ {
1055
+ "id": "e02",
1056
+ "description": "2-pigeon-2-hole SAT (place pigeons in distinct holes)",
1057
+ "rendered_cnf": {
1058
+ "clauses": [
1059
+ [
1060
+ {
1061
+ "predicate": "P1H1",
1062
+ "args": [],
1063
+ "negated": false
1064
+ },
1065
+ {
1066
+ "predicate": "P1H2",
1067
+ "args": [],
1068
+ "negated": false
1069
+ }
1070
+ ],
1071
+ [
1072
+ {
1073
+ "predicate": "P2H1",
1074
+ "args": [],
1075
+ "negated": false
1076
+ },
1077
+ {
1078
+ "predicate": "P2H2",
1079
+ "args": [],
1080
+ "negated": false
1081
+ }
1082
+ ],
1083
+ [
1084
+ {
1085
+ "predicate": "P1H1",
1086
+ "args": [],
1087
+ "negated": true
1088
+ },
1089
+ {
1090
+ "predicate": "P2H1",
1091
+ "args": [],
1092
+ "negated": true
1093
+ }
1094
+ ],
1095
+ [
1096
+ {
1097
+ "predicate": "P1H2",
1098
+ "args": [],
1099
+ "negated": true
1100
+ },
1101
+ {
1102
+ "predicate": "P2H2",
1103
+ "args": [],
1104
+ "negated": true
1105
+ }
1106
+ ]
1107
+ ]
1108
+ },
1109
+ "label": "consistent",
1110
+ "mode": "consistency",
1111
+ "atom_count": 4
1112
+ },
1113
+ {
1114
+ "id": "e03",
1115
+ "description": "3-pigeon-2-hole UNSAT (classic pigeonhole)",
1116
+ "rendered_cnf": {
1117
+ "clauses": [
1118
+ [
1119
+ {
1120
+ "predicate": "P1H1",
1121
+ "args": [],
1122
+ "negated": false
1123
+ },
1124
+ {
1125
+ "predicate": "P1H2",
1126
+ "args": [],
1127
+ "negated": false
1128
+ }
1129
+ ],
1130
+ [
1131
+ {
1132
+ "predicate": "P2H1",
1133
+ "args": [],
1134
+ "negated": false
1135
+ },
1136
+ {
1137
+ "predicate": "P2H2",
1138
+ "args": [],
1139
+ "negated": false
1140
+ }
1141
+ ],
1142
+ [
1143
+ {
1144
+ "predicate": "P3H1",
1145
+ "args": [],
1146
+ "negated": false
1147
+ },
1148
+ {
1149
+ "predicate": "P3H2",
1150
+ "args": [],
1151
+ "negated": false
1152
+ }
1153
+ ],
1154
+ [
1155
+ {
1156
+ "predicate": "P1H1",
1157
+ "args": [],
1158
+ "negated": true
1159
+ },
1160
+ {
1161
+ "predicate": "P2H1",
1162
+ "args": [],
1163
+ "negated": true
1164
+ }
1165
+ ],
1166
+ [
1167
+ {
1168
+ "predicate": "P1H1",
1169
+ "args": [],
1170
+ "negated": true
1171
+ },
1172
+ {
1173
+ "predicate": "P3H1",
1174
+ "args": [],
1175
+ "negated": true
1176
+ }
1177
+ ],
1178
+ [
1179
+ {
1180
+ "predicate": "P2H1",
1181
+ "args": [],
1182
+ "negated": true
1183
+ },
1184
+ {
1185
+ "predicate": "P3H1",
1186
+ "args": [],
1187
+ "negated": true
1188
+ }
1189
+ ],
1190
+ [
1191
+ {
1192
+ "predicate": "P1H2",
1193
+ "args": [],
1194
+ "negated": true
1195
+ },
1196
+ {
1197
+ "predicate": "P2H2",
1198
+ "args": [],
1199
+ "negated": true
1200
+ }
1201
+ ],
1202
+ [
1203
+ {
1204
+ "predicate": "P1H2",
1205
+ "args": [],
1206
+ "negated": true
1207
+ },
1208
+ {
1209
+ "predicate": "P3H2",
1210
+ "args": [],
1211
+ "negated": true
1212
+ }
1213
+ ],
1214
+ [
1215
+ {
1216
+ "predicate": "P2H2",
1217
+ "args": [],
1218
+ "negated": true
1219
+ },
1220
+ {
1221
+ "predicate": "P3H2",
1222
+ "args": [],
1223
+ "negated": true
1224
+ }
1225
+ ]
1226
+ ]
1227
+ },
1228
+ "label": "inconsistent",
1229
+ "mode": "consistency",
1230
+ "atom_count": 6
1231
+ },
1232
+ {
1233
+ "id": "e04",
1234
+ "description": "3-pigeon-3-hole SAT (a perfect matching exists)",
1235
+ "rendered_cnf": {
1236
+ "clauses": [
1237
+ [
1238
+ {
1239
+ "predicate": "P1H1",
1240
+ "args": [],
1241
+ "negated": false
1242
+ },
1243
+ {
1244
+ "predicate": "P1H2",
1245
+ "args": [],
1246
+ "negated": false
1247
+ },
1248
+ {
1249
+ "predicate": "P1H3",
1250
+ "args": [],
1251
+ "negated": false
1252
+ }
1253
+ ],
1254
+ [
1255
+ {
1256
+ "predicate": "P2H1",
1257
+ "args": [],
1258
+ "negated": false
1259
+ },
1260
+ {
1261
+ "predicate": "P2H2",
1262
+ "args": [],
1263
+ "negated": false
1264
+ },
1265
+ {
1266
+ "predicate": "P2H3",
1267
+ "args": [],
1268
+ "negated": false
1269
+ }
1270
+ ],
1271
+ [
1272
+ {
1273
+ "predicate": "P3H1",
1274
+ "args": [],
1275
+ "negated": false
1276
+ },
1277
+ {
1278
+ "predicate": "P3H2",
1279
+ "args": [],
1280
+ "negated": false
1281
+ },
1282
+ {
1283
+ "predicate": "P3H3",
1284
+ "args": [],
1285
+ "negated": false
1286
+ }
1287
+ ],
1288
+ [
1289
+ {
1290
+ "predicate": "P1H1",
1291
+ "args": [],
1292
+ "negated": true
1293
+ },
1294
+ {
1295
+ "predicate": "P2H1",
1296
+ "args": [],
1297
+ "negated": true
1298
+ }
1299
+ ],
1300
+ [
1301
+ {
1302
+ "predicate": "P1H1",
1303
+ "args": [],
1304
+ "negated": true
1305
+ },
1306
+ {
1307
+ "predicate": "P3H1",
1308
+ "args": [],
1309
+ "negated": true
1310
+ }
1311
+ ],
1312
+ [
1313
+ {
1314
+ "predicate": "P2H1",
1315
+ "args": [],
1316
+ "negated": true
1317
+ },
1318
+ {
1319
+ "predicate": "P3H1",
1320
+ "args": [],
1321
+ "negated": true
1322
+ }
1323
+ ],
1324
+ [
1325
+ {
1326
+ "predicate": "P1H2",
1327
+ "args": [],
1328
+ "negated": true
1329
+ },
1330
+ {
1331
+ "predicate": "P2H2",
1332
+ "args": [],
1333
+ "negated": true
1334
+ }
1335
+ ],
1336
+ [
1337
+ {
1338
+ "predicate": "P1H2",
1339
+ "args": [],
1340
+ "negated": true
1341
+ },
1342
+ {
1343
+ "predicate": "P3H2",
1344
+ "args": [],
1345
+ "negated": true
1346
+ }
1347
+ ],
1348
+ [
1349
+ {
1350
+ "predicate": "P2H2",
1351
+ "args": [],
1352
+ "negated": true
1353
+ },
1354
+ {
1355
+ "predicate": "P3H2",
1356
+ "args": [],
1357
+ "negated": true
1358
+ }
1359
+ ],
1360
+ [
1361
+ {
1362
+ "predicate": "P1H3",
1363
+ "args": [],
1364
+ "negated": true
1365
+ },
1366
+ {
1367
+ "predicate": "P2H3",
1368
+ "args": [],
1369
+ "negated": true
1370
+ }
1371
+ ],
1372
+ [
1373
+ {
1374
+ "predicate": "P1H3",
1375
+ "args": [],
1376
+ "negated": true
1377
+ },
1378
+ {
1379
+ "predicate": "P3H3",
1380
+ "args": [],
1381
+ "negated": true
1382
+ }
1383
+ ],
1384
+ [
1385
+ {
1386
+ "predicate": "P2H3",
1387
+ "args": [],
1388
+ "negated": true
1389
+ },
1390
+ {
1391
+ "predicate": "P3H3",
1392
+ "args": [],
1393
+ "negated": true
1394
+ }
1395
+ ]
1396
+ ]
1397
+ },
1398
+ "label": "consistent",
1399
+ "mode": "consistency",
1400
+ "atom_count": 9
1401
+ },
1402
+ {
1403
+ "id": "f01",
1404
+ "description": "Cat(Tom)",
1405
+ "rendered_cnf": {
1406
+ "clauses": [
1407
+ [
1408
+ {
1409
+ "predicate": "Cat",
1410
+ "args": [
1411
+ "Tom"
1412
+ ],
1413
+ "negated": false
1414
+ }
1415
+ ]
1416
+ ]
1417
+ },
1418
+ "label": "consistent",
1419
+ "mode": "consistency",
1420
+ "atom_count": 1
1421
+ },
1422
+ {
1423
+ "id": "f02",
1424
+ "description": "Cat(Tom) \u2227 \u00acCat(Tom)",
1425
+ "rendered_cnf": {
1426
+ "clauses": [
1427
+ [
1428
+ {
1429
+ "predicate": "Cat",
1430
+ "args": [
1431
+ "Tom"
1432
+ ],
1433
+ "negated": false
1434
+ }
1435
+ ],
1436
+ [
1437
+ {
1438
+ "predicate": "Cat",
1439
+ "args": [
1440
+ "Tom"
1441
+ ],
1442
+ "negated": true
1443
+ }
1444
+ ]
1445
+ ]
1446
+ },
1447
+ "label": "inconsistent",
1448
+ "mode": "consistency",
1449
+ "atom_count": 1
1450
+ },
1451
+ {
1452
+ "id": "f03",
1453
+ "description": "Cat(Tom) \u2227 HasFur(Tom)",
1454
+ "rendered_cnf": {
1455
+ "clauses": [
1456
+ [
1457
+ {
1458
+ "predicate": "Cat",
1459
+ "args": [
1460
+ "Tom"
1461
+ ],
1462
+ "negated": false
1463
+ }
1464
+ ],
1465
+ [
1466
+ {
1467
+ "predicate": "HasFur",
1468
+ "args": [
1469
+ "Tom"
1470
+ ],
1471
+ "negated": false
1472
+ }
1473
+ ]
1474
+ ]
1475
+ },
1476
+ "label": "consistent",
1477
+ "mode": "consistency",
1478
+ "atom_count": 2
1479
+ },
1480
+ {
1481
+ "id": "f04",
1482
+ "description": "Modus ponens grounded: (\u00acCat(Tom) \u2228 HasFur(Tom)) \u2227 Cat(Tom)",
1483
+ "rendered_cnf": {
1484
+ "clauses": [
1485
+ [
1486
+ {
1487
+ "predicate": "Cat",
1488
+ "args": [
1489
+ "Tom"
1490
+ ],
1491
+ "negated": true
1492
+ },
1493
+ {
1494
+ "predicate": "HasFur",
1495
+ "args": [
1496
+ "Tom"
1497
+ ],
1498
+ "negated": false
1499
+ }
1500
+ ],
1501
+ [
1502
+ {
1503
+ "predicate": "Cat",
1504
+ "args": [
1505
+ "Tom"
1506
+ ],
1507
+ "negated": false
1508
+ }
1509
+ ]
1510
+ ]
1511
+ },
1512
+ "label": "consistent",
1513
+ "mode": "consistency",
1514
+ "atom_count": 2
1515
+ },
1516
+ {
1517
+ "id": "f05",
1518
+ "description": "Grounded MP UNSAT: above \u2227 \u00acHasFur(Tom)",
1519
+ "rendered_cnf": {
1520
+ "clauses": [
1521
+ [
1522
+ {
1523
+ "predicate": "Cat",
1524
+ "args": [
1525
+ "Tom"
1526
+ ],
1527
+ "negated": true
1528
+ },
1529
+ {
1530
+ "predicate": "HasFur",
1531
+ "args": [
1532
+ "Tom"
1533
+ ],
1534
+ "negated": false
1535
+ }
1536
+ ],
1537
+ [
1538
+ {
1539
+ "predicate": "Cat",
1540
+ "args": [
1541
+ "Tom"
1542
+ ],
1543
+ "negated": false
1544
+ }
1545
+ ],
1546
+ [
1547
+ {
1548
+ "predicate": "HasFur",
1549
+ "args": [
1550
+ "Tom"
1551
+ ],
1552
+ "negated": true
1553
+ }
1554
+ ]
1555
+ ]
1556
+ },
1557
+ "label": "inconsistent",
1558
+ "mode": "consistency",
1559
+ "atom_count": 2
1560
+ },
1561
+ {
1562
+ "id": "f06",
1563
+ "description": "Two birds, one negated: Bird(Robin) \u2227 Bird(Tweety) \u2227 \u00acBird(Tweety)",
1564
+ "rendered_cnf": {
1565
+ "clauses": [
1566
+ [
1567
+ {
1568
+ "predicate": "Bird",
1569
+ "args": [
1570
+ "Robin"
1571
+ ],
1572
+ "negated": false
1573
+ }
1574
+ ],
1575
+ [
1576
+ {
1577
+ "predicate": "Bird",
1578
+ "args": [
1579
+ "Tweety"
1580
+ ],
1581
+ "negated": false
1582
+ }
1583
+ ],
1584
+ [
1585
+ {
1586
+ "predicate": "Bird",
1587
+ "args": [
1588
+ "Tweety"
1589
+ ],
1590
+ "negated": true
1591
+ }
1592
+ ]
1593
+ ]
1594
+ },
1595
+ "label": "inconsistent",
1596
+ "mode": "consistency",
1597
+ "atom_count": 2
1598
+ },
1599
+ {
1600
+ "id": "f07",
1601
+ "description": "Universal grounded over 2 constants \u2014 SAT",
1602
+ "rendered_cnf": {
1603
+ "clauses": [
1604
+ [
1605
+ {
1606
+ "predicate": "Bird",
1607
+ "args": [
1608
+ "Robin"
1609
+ ],
1610
+ "negated": true
1611
+ },
1612
+ {
1613
+ "predicate": "Flies",
1614
+ "args": [
1615
+ "Robin"
1616
+ ],
1617
+ "negated": false
1618
+ }
1619
+ ],
1620
+ [
1621
+ {
1622
+ "predicate": "Bird",
1623
+ "args": [
1624
+ "Tweety"
1625
+ ],
1626
+ "negated": true
1627
+ },
1628
+ {
1629
+ "predicate": "Flies",
1630
+ "args": [
1631
+ "Tweety"
1632
+ ],
1633
+ "negated": false
1634
+ }
1635
+ ],
1636
+ [
1637
+ {
1638
+ "predicate": "Bird",
1639
+ "args": [
1640
+ "Robin"
1641
+ ],
1642
+ "negated": false
1643
+ }
1644
+ ],
1645
+ [
1646
+ {
1647
+ "predicate": "Bird",
1648
+ "args": [
1649
+ "Tweety"
1650
+ ],
1651
+ "negated": false
1652
+ }
1653
+ ]
1654
+ ]
1655
+ },
1656
+ "label": "consistent",
1657
+ "mode": "consistency",
1658
+ "atom_count": 4
1659
+ },
1660
+ {
1661
+ "id": "f08",
1662
+ "description": "Above + \u00acFlies(Tweety) \u2014 UNSAT",
1663
+ "rendered_cnf": {
1664
+ "clauses": [
1665
+ [
1666
+ {
1667
+ "predicate": "Bird",
1668
+ "args": [
1669
+ "Robin"
1670
+ ],
1671
+ "negated": true
1672
+ },
1673
+ {
1674
+ "predicate": "Flies",
1675
+ "args": [
1676
+ "Robin"
1677
+ ],
1678
+ "negated": false
1679
+ }
1680
+ ],
1681
+ [
1682
+ {
1683
+ "predicate": "Bird",
1684
+ "args": [
1685
+ "Tweety"
1686
+ ],
1687
+ "negated": true
1688
+ },
1689
+ {
1690
+ "predicate": "Flies",
1691
+ "args": [
1692
+ "Tweety"
1693
+ ],
1694
+ "negated": false
1695
+ }
1696
+ ],
1697
+ [
1698
+ {
1699
+ "predicate": "Bird",
1700
+ "args": [
1701
+ "Robin"
1702
+ ],
1703
+ "negated": false
1704
+ }
1705
+ ],
1706
+ [
1707
+ {
1708
+ "predicate": "Bird",
1709
+ "args": [
1710
+ "Tweety"
1711
+ ],
1712
+ "negated": false
1713
+ }
1714
+ ],
1715
+ [
1716
+ {
1717
+ "predicate": "Flies",
1718
+ "args": [
1719
+ "Tweety"
1720
+ ],
1721
+ "negated": true
1722
+ }
1723
+ ]
1724
+ ]
1725
+ },
1726
+ "label": "inconsistent",
1727
+ "mode": "consistency",
1728
+ "atom_count": 4
1729
+ },
1730
+ {
1731
+ "id": "f09",
1732
+ "description": "Three-step grounded chain SAT",
1733
+ "rendered_cnf": {
1734
+ "clauses": [
1735
+ [
1736
+ {
1737
+ "predicate": "Cat",
1738
+ "args": [
1739
+ "Tom"
1740
+ ],
1741
+ "negated": true
1742
+ },
1743
+ {
1744
+ "predicate": "Animal",
1745
+ "args": [
1746
+ "Tom"
1747
+ ],
1748
+ "negated": false
1749
+ }
1750
+ ],
1751
+ [
1752
+ {
1753
+ "predicate": "Animal",
1754
+ "args": [
1755
+ "Tom"
1756
+ ],
1757
+ "negated": true
1758
+ },
1759
+ {
1760
+ "predicate": "Mortal",
1761
+ "args": [
1762
+ "Tom"
1763
+ ],
1764
+ "negated": false
1765
+ }
1766
+ ],
1767
+ [
1768
+ {
1769
+ "predicate": "Cat",
1770
+ "args": [
1771
+ "Tom"
1772
+ ],
1773
+ "negated": false
1774
+ }
1775
+ ]
1776
+ ]
1777
+ },
1778
+ "label": "consistent",
1779
+ "mode": "consistency",
1780
+ "atom_count": 3
1781
+ },
1782
+ {
1783
+ "id": "f10",
1784
+ "description": "Three-step grounded chain UNSAT",
1785
+ "rendered_cnf": {
1786
+ "clauses": [
1787
+ [
1788
+ {
1789
+ "predicate": "Cat",
1790
+ "args": [
1791
+ "Tom"
1792
+ ],
1793
+ "negated": true
1794
+ },
1795
+ {
1796
+ "predicate": "Animal",
1797
+ "args": [
1798
+ "Tom"
1799
+ ],
1800
+ "negated": false
1801
+ }
1802
+ ],
1803
+ [
1804
+ {
1805
+ "predicate": "Animal",
1806
+ "args": [
1807
+ "Tom"
1808
+ ],
1809
+ "negated": true
1810
+ },
1811
+ {
1812
+ "predicate": "Mortal",
1813
+ "args": [
1814
+ "Tom"
1815
+ ],
1816
+ "negated": false
1817
+ }
1818
+ ],
1819
+ [
1820
+ {
1821
+ "predicate": "Cat",
1822
+ "args": [
1823
+ "Tom"
1824
+ ],
1825
+ "negated": false
1826
+ }
1827
+ ],
1828
+ [
1829
+ {
1830
+ "predicate": "Mortal",
1831
+ "args": [
1832
+ "Tom"
1833
+ ],
1834
+ "negated": true
1835
+ }
1836
+ ]
1837
+ ]
1838
+ },
1839
+ "label": "inconsistent",
1840
+ "mode": "consistency",
1841
+ "atom_count": 3
1842
+ },
1843
+ {
1844
+ "id": "g01",
1845
+ "description": "Three-way OR with two negated: (P\u2228Q\u2228R) \u2227 \u00acP \u2227 \u00acQ",
1846
+ "rendered_cnf": {
1847
+ "clauses": [
1848
+ [
1849
+ {
1850
+ "predicate": "P",
1851
+ "args": [],
1852
+ "negated": false
1853
+ },
1854
+ {
1855
+ "predicate": "Q",
1856
+ "args": [],
1857
+ "negated": false
1858
+ },
1859
+ {
1860
+ "predicate": "R",
1861
+ "args": [],
1862
+ "negated": false
1863
+ }
1864
+ ],
1865
+ [
1866
+ {
1867
+ "predicate": "P",
1868
+ "args": [],
1869
+ "negated": true
1870
+ }
1871
+ ],
1872
+ [
1873
+ {
1874
+ "predicate": "Q",
1875
+ "args": [],
1876
+ "negated": true
1877
+ }
1878
+ ]
1879
+ ]
1880
+ },
1881
+ "label": "consistent",
1882
+ "mode": "consistency",
1883
+ "atom_count": 3
1884
+ },
1885
+ {
1886
+ "id": "g02",
1887
+ "description": "Above with all negated: UNSAT",
1888
+ "rendered_cnf": {
1889
+ "clauses": [
1890
+ [
1891
+ {
1892
+ "predicate": "P",
1893
+ "args": [],
1894
+ "negated": false
1895
+ },
1896
+ {
1897
+ "predicate": "Q",
1898
+ "args": [],
1899
+ "negated": false
1900
+ },
1901
+ {
1902
+ "predicate": "R",
1903
+ "args": [],
1904
+ "negated": false
1905
+ }
1906
+ ],
1907
+ [
1908
+ {
1909
+ "predicate": "P",
1910
+ "args": [],
1911
+ "negated": true
1912
+ }
1913
+ ],
1914
+ [
1915
+ {
1916
+ "predicate": "Q",
1917
+ "args": [],
1918
+ "negated": true
1919
+ }
1920
+ ],
1921
+ [
1922
+ {
1923
+ "predicate": "R",
1924
+ "args": [],
1925
+ "negated": true
1926
+ }
1927
+ ]
1928
+ ]
1929
+ },
1930
+ "label": "inconsistent",
1931
+ "mode": "consistency",
1932
+ "atom_count": 3
1933
+ },
1934
+ {
1935
+ "id": "g03",
1936
+ "description": "Two-pair OR with at-most-one cross: (P\u2228Q)\u2227(R\u2228S)\u2227(\u00acP\u2228\u00acR)",
1937
+ "rendered_cnf": {
1938
+ "clauses": [
1939
+ [
1940
+ {
1941
+ "predicate": "P",
1942
+ "args": [],
1943
+ "negated": false
1944
+ },
1945
+ {
1946
+ "predicate": "Q",
1947
+ "args": [],
1948
+ "negated": false
1949
+ }
1950
+ ],
1951
+ [
1952
+ {
1953
+ "predicate": "R",
1954
+ "args": [],
1955
+ "negated": false
1956
+ },
1957
+ {
1958
+ "predicate": "S",
1959
+ "args": [],
1960
+ "negated": false
1961
+ }
1962
+ ],
1963
+ [
1964
+ {
1965
+ "predicate": "P",
1966
+ "args": [],
1967
+ "negated": true
1968
+ },
1969
+ {
1970
+ "predicate": "R",
1971
+ "args": [],
1972
+ "negated": true
1973
+ }
1974
+ ]
1975
+ ]
1976
+ },
1977
+ "label": "consistent",
1978
+ "mode": "consistency",
1979
+ "atom_count": 4
1980
+ },
1981
+ {
1982
+ "id": "g04",
1983
+ "description": "Three asserted, three-clause exclusion UNSAT",
1984
+ "rendered_cnf": {
1985
+ "clauses": [
1986
+ [
1987
+ {
1988
+ "predicate": "P",
1989
+ "args": [],
1990
+ "negated": false
1991
+ }
1992
+ ],
1993
+ [
1994
+ {
1995
+ "predicate": "Q",
1996
+ "args": [],
1997
+ "negated": false
1998
+ }
1999
+ ],
2000
+ [
2001
+ {
2002
+ "predicate": "R",
2003
+ "args": [],
2004
+ "negated": false
2005
+ }
2006
+ ],
2007
+ [
2008
+ {
2009
+ "predicate": "P",
2010
+ "args": [],
2011
+ "negated": true
2012
+ },
2013
+ {
2014
+ "predicate": "Q",
2015
+ "args": [],
2016
+ "negated": true
2017
+ },
2018
+ {
2019
+ "predicate": "R",
2020
+ "args": [],
2021
+ "negated": true
2022
+ }
2023
+ ]
2024
+ ]
2025
+ },
2026
+ "label": "inconsistent",
2027
+ "mode": "consistency",
2028
+ "atom_count": 3
2029
+ },
2030
+ {
2031
+ "id": "g05",
2032
+ "description": "At-most-one of {P,Q,R}",
2033
+ "rendered_cnf": {
2034
+ "clauses": [
2035
+ [
2036
+ {
2037
+ "predicate": "P",
2038
+ "args": [],
2039
+ "negated": true
2040
+ },
2041
+ {
2042
+ "predicate": "Q",
2043
+ "args": [],
2044
+ "negated": true
2045
+ }
2046
+ ],
2047
+ [
2048
+ {
2049
+ "predicate": "P",
2050
+ "args": [],
2051
+ "negated": true
2052
+ },
2053
+ {
2054
+ "predicate": "R",
2055
+ "args": [],
2056
+ "negated": true
2057
+ }
2058
+ ],
2059
+ [
2060
+ {
2061
+ "predicate": "Q",
2062
+ "args": [],
2063
+ "negated": true
2064
+ },
2065
+ {
2066
+ "predicate": "R",
2067
+ "args": [],
2068
+ "negated": true
2069
+ }
2070
+ ]
2071
+ ]
2072
+ },
2073
+ "label": "consistent",
2074
+ "mode": "consistency",
2075
+ "atom_count": 3
2076
+ },
2077
+ {
2078
+ "id": "g06",
2079
+ "description": "Exactly-one of {P,Q,R}: at-most-1 + at-least-1",
2080
+ "rendered_cnf": {
2081
+ "clauses": [
2082
+ [
2083
+ {
2084
+ "predicate": "P",
2085
+ "args": [],
2086
+ "negated": true
2087
+ },
2088
+ {
2089
+ "predicate": "Q",
2090
+ "args": [],
2091
+ "negated": true
2092
+ }
2093
+ ],
2094
+ [
2095
+ {
2096
+ "predicate": "P",
2097
+ "args": [],
2098
+ "negated": true
2099
+ },
2100
+ {
2101
+ "predicate": "R",
2102
+ "args": [],
2103
+ "negated": true
2104
+ }
2105
+ ],
2106
+ [
2107
+ {
2108
+ "predicate": "Q",
2109
+ "args": [],
2110
+ "negated": true
2111
+ },
2112
+ {
2113
+ "predicate": "R",
2114
+ "args": [],
2115
+ "negated": true
2116
+ }
2117
+ ],
2118
+ [
2119
+ {
2120
+ "predicate": "P",
2121
+ "args": [],
2122
+ "negated": false
2123
+ },
2124
+ {
2125
+ "predicate": "Q",
2126
+ "args": [],
2127
+ "negated": false
2128
+ },
2129
+ {
2130
+ "predicate": "R",
2131
+ "args": [],
2132
+ "negated": false
2133
+ }
2134
+ ]
2135
+ ]
2136
+ },
2137
+ "label": "consistent",
2138
+ "mode": "consistency",
2139
+ "atom_count": 3
2140
+ },
2141
+ {
2142
+ "id": "g07",
2143
+ "description": "Exactly-one of {P,Q,R} but force two true: UNSAT",
2144
+ "rendered_cnf": {
2145
+ "clauses": [
2146
+ [
2147
+ {
2148
+ "predicate": "P",
2149
+ "args": [],
2150
+ "negated": true
2151
+ },
2152
+ {
2153
+ "predicate": "Q",
2154
+ "args": [],
2155
+ "negated": true
2156
+ }
2157
+ ],
2158
+ [
2159
+ {
2160
+ "predicate": "P",
2161
+ "args": [],
2162
+ "negated": true
2163
+ },
2164
+ {
2165
+ "predicate": "R",
2166
+ "args": [],
2167
+ "negated": true
2168
+ }
2169
+ ],
2170
+ [
2171
+ {
2172
+ "predicate": "Q",
2173
+ "args": [],
2174
+ "negated": true
2175
+ },
2176
+ {
2177
+ "predicate": "R",
2178
+ "args": [],
2179
+ "negated": true
2180
+ }
2181
+ ],
2182
+ [
2183
+ {
2184
+ "predicate": "P",
2185
+ "args": [],
2186
+ "negated": false
2187
+ },
2188
+ {
2189
+ "predicate": "Q",
2190
+ "args": [],
2191
+ "negated": false
2192
+ },
2193
+ {
2194
+ "predicate": "R",
2195
+ "args": [],
2196
+ "negated": false
2197
+ }
2198
+ ],
2199
+ [
2200
+ {
2201
+ "predicate": "P",
2202
+ "args": [],
2203
+ "negated": false
2204
+ }
2205
+ ],
2206
+ [
2207
+ {
2208
+ "predicate": "Q",
2209
+ "args": [],
2210
+ "negated": false
2211
+ }
2212
+ ]
2213
+ ]
2214
+ },
2215
+ "label": "inconsistent",
2216
+ "mode": "consistency",
2217
+ "atom_count": 3
2218
+ },
2219
+ {
2220
+ "id": "g08",
2221
+ "description": "Six-atom forced inconsistency: cover all six and refute their conjunction",
2222
+ "rendered_cnf": {
2223
+ "clauses": [
2224
+ [
2225
+ {
2226
+ "predicate": "P",
2227
+ "args": [],
2228
+ "negated": false
2229
+ }
2230
+ ],
2231
+ [
2232
+ {
2233
+ "predicate": "Q",
2234
+ "args": [],
2235
+ "negated": false
2236
+ }
2237
+ ],
2238
+ [
2239
+ {
2240
+ "predicate": "R",
2241
+ "args": [],
2242
+ "negated": false
2243
+ }
2244
+ ],
2245
+ [
2246
+ {
2247
+ "predicate": "S",
2248
+ "args": [],
2249
+ "negated": false
2250
+ }
2251
+ ],
2252
+ [
2253
+ {
2254
+ "predicate": "T",
2255
+ "args": [],
2256
+ "negated": false
2257
+ }
2258
+ ],
2259
+ [
2260
+ {
2261
+ "predicate": "U",
2262
+ "args": [],
2263
+ "negated": false
2264
+ }
2265
+ ],
2266
+ [
2267
+ {
2268
+ "predicate": "P",
2269
+ "args": [],
2270
+ "negated": true
2271
+ },
2272
+ {
2273
+ "predicate": "R",
2274
+ "args": [],
2275
+ "negated": true
2276
+ },
2277
+ {
2278
+ "predicate": "U",
2279
+ "args": [],
2280
+ "negated": true
2281
+ }
2282
+ ]
2283
+ ]
2284
+ },
2285
+ "label": "inconsistent",
2286
+ "mode": "consistency",
2287
+ "atom_count": 6
2288
+ },
2289
+ {
2290
+ "id": "g09",
2291
+ "description": "Six-atom UNSAT",
2292
+ "rendered_cnf": {
2293
+ "clauses": [
2294
+ [
2295
+ {
2296
+ "predicate": "P",
2297
+ "args": [],
2298
+ "negated": false
2299
+ }
2300
+ ],
2301
+ [
2302
+ {
2303
+ "predicate": "Q",
2304
+ "args": [],
2305
+ "negated": false
2306
+ }
2307
+ ],
2308
+ [
2309
+ {
2310
+ "predicate": "R",
2311
+ "args": [],
2312
+ "negated": false
2313
+ }
2314
+ ],
2315
+ [
2316
+ {
2317
+ "predicate": "S",
2318
+ "args": [],
2319
+ "negated": false
2320
+ }
2321
+ ],
2322
+ [
2323
+ {
2324
+ "predicate": "T",
2325
+ "args": [],
2326
+ "negated": false
2327
+ }
2328
+ ],
2329
+ [
2330
+ {
2331
+ "predicate": "U",
2332
+ "args": [],
2333
+ "negated": false
2334
+ }
2335
+ ],
2336
+ [
2337
+ {
2338
+ "predicate": "P",
2339
+ "args": [],
2340
+ "negated": true
2341
+ },
2342
+ {
2343
+ "predicate": "Q",
2344
+ "args": [],
2345
+ "negated": true
2346
+ },
2347
+ {
2348
+ "predicate": "R",
2349
+ "args": [],
2350
+ "negated": true
2351
+ },
2352
+ {
2353
+ "predicate": "S",
2354
+ "args": [],
2355
+ "negated": true
2356
+ },
2357
+ {
2358
+ "predicate": "T",
2359
+ "args": [],
2360
+ "negated": true
2361
+ },
2362
+ {
2363
+ "predicate": "U",
2364
+ "args": [],
2365
+ "negated": true
2366
+ }
2367
+ ]
2368
+ ]
2369
+ },
2370
+ "label": "inconsistent",
2371
+ "mode": "consistency",
2372
+ "atom_count": 6
2373
+ },
2374
+ {
2375
+ "id": "g10",
2376
+ "description": "Five-atom resolution UNSAT",
2377
+ "rendered_cnf": {
2378
+ "clauses": [
2379
+ [
2380
+ {
2381
+ "predicate": "P",
2382
+ "args": [],
2383
+ "negated": false
2384
+ },
2385
+ {
2386
+ "predicate": "Q",
2387
+ "args": [],
2388
+ "negated": false
2389
+ }
2390
+ ],
2391
+ [
2392
+ {
2393
+ "predicate": "P",
2394
+ "args": [],
2395
+ "negated": false
2396
+ },
2397
+ {
2398
+ "predicate": "Q",
2399
+ "args": [],
2400
+ "negated": true
2401
+ }
2402
+ ],
2403
+ [
2404
+ {
2405
+ "predicate": "P",
2406
+ "args": [],
2407
+ "negated": true
2408
+ },
2409
+ {
2410
+ "predicate": "R",
2411
+ "args": [],
2412
+ "negated": false
2413
+ }
2414
+ ],
2415
+ [
2416
+ {
2417
+ "predicate": "P",
2418
+ "args": [],
2419
+ "negated": true
2420
+ },
2421
+ {
2422
+ "predicate": "R",
2423
+ "args": [],
2424
+ "negated": true
2425
+ }
2426
+ ]
2427
+ ]
2428
+ },
2429
+ "label": "inconsistent",
2430
+ "mode": "consistency",
2431
+ "atom_count": 3
2432
+ }
2433
+ ]
benchmarks/results/qverify_mini_simulator/accuracy.png ADDED
benchmarks/results/qverify_mini_simulator/latency.png ADDED
benchmarks/results/qverify_mini_simulator/qubits.png ADDED
benchmarks/results/qverify_mini_simulator/report.json ADDED
@@ -0,0 +1,515 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ {
2
+ "dataset": "qverify-mini",
3
+ "backend": "default.qubit",
4
+ "n_examples": 50,
5
+ "n_skipped": 0,
6
+ "accuracy": 1.0,
7
+ "avg_seconds": 3.3067833896195227,
8
+ "p95_seconds": 0.3194446280031116,
9
+ "n_translated": 0,
10
+ "n_translation_failed": 0,
11
+ "avg_translation_seconds": 0.0,
12
+ "n_skipped_too_large": 0,
13
+ "results": [
14
+ {
15
+ "example_id": "a01",
16
+ "dataset_label": "consistent",
17
+ "expected": "consistent",
18
+ "predicted": "consistent",
19
+ "agrees": true,
20
+ "verify_seconds": 0.06022830899746623,
21
+ "n_qubits": 1,
22
+ "n_iterations": 1
23
+ },
24
+ {
25
+ "example_id": "a02",
26
+ "dataset_label": "consistent",
27
+ "expected": "consistent",
28
+ "predicted": "consistent",
29
+ "agrees": true,
30
+ "verify_seconds": 0.029432226001517847,
31
+ "n_qubits": 1,
32
+ "n_iterations": 1
33
+ },
34
+ {
35
+ "example_id": "a03",
36
+ "dataset_label": "inconsistent",
37
+ "expected": "inconsistent",
38
+ "predicted": "inconsistent",
39
+ "agrees": true,
40
+ "verify_seconds": 0.04833027799759293,
41
+ "n_qubits": 1,
42
+ "n_iterations": 1
43
+ },
44
+ {
45
+ "example_id": "a04",
46
+ "dataset_label": "consistent",
47
+ "expected": "consistent",
48
+ "predicted": "consistent",
49
+ "agrees": true,
50
+ "verify_seconds": 0.0926051060014288,
51
+ "n_qubits": 2,
52
+ "n_iterations": 2
53
+ },
54
+ {
55
+ "example_id": "a05",
56
+ "dataset_label": "inconsistent",
57
+ "expected": "inconsistent",
58
+ "predicted": "inconsistent",
59
+ "agrees": true,
60
+ "verify_seconds": 0.20489475599606521,
61
+ "n_qubits": 2,
62
+ "n_iterations": 2
63
+ },
64
+ {
65
+ "example_id": "a06",
66
+ "dataset_label": "consistent",
67
+ "expected": "consistent",
68
+ "predicted": "consistent",
69
+ "agrees": true,
70
+ "verify_seconds": 0.023863778995291796,
71
+ "n_qubits": 2,
72
+ "n_iterations": 2
73
+ },
74
+ {
75
+ "example_id": "a07",
76
+ "dataset_label": "inconsistent",
77
+ "expected": "inconsistent",
78
+ "predicted": "inconsistent",
79
+ "agrees": true,
80
+ "verify_seconds": 0.020170801995845977,
81
+ "n_qubits": 2,
82
+ "n_iterations": 2
83
+ },
84
+ {
85
+ "example_id": "a08",
86
+ "dataset_label": "inconsistent",
87
+ "expected": "inconsistent",
88
+ "predicted": "inconsistent",
89
+ "agrees": true,
90
+ "verify_seconds": 0.025361142004840076,
91
+ "n_qubits": 2,
92
+ "n_iterations": 2
93
+ },
94
+ {
95
+ "example_id": "b01",
96
+ "dataset_label": "consistent",
97
+ "expected": "consistent",
98
+ "predicted": "consistent",
99
+ "agrees": true,
100
+ "verify_seconds": 0.0216899890001514,
101
+ "n_qubits": 2,
102
+ "n_iterations": 2
103
+ },
104
+ {
105
+ "example_id": "b02",
106
+ "dataset_label": "inconsistent",
107
+ "expected": "inconsistent",
108
+ "predicted": "inconsistent",
109
+ "agrees": true,
110
+ "verify_seconds": 0.029466830994351767,
111
+ "n_qubits": 2,
112
+ "n_iterations": 2
113
+ },
114
+ {
115
+ "example_id": "b03",
116
+ "dataset_label": "consistent",
117
+ "expected": "consistent",
118
+ "predicted": "consistent",
119
+ "agrees": true,
120
+ "verify_seconds": 0.028637160998187028,
121
+ "n_qubits": 3,
122
+ "n_iterations": 2
123
+ },
124
+ {
125
+ "example_id": "b04",
126
+ "dataset_label": "inconsistent",
127
+ "expected": "inconsistent",
128
+ "predicted": "inconsistent",
129
+ "agrees": true,
130
+ "verify_seconds": 0.02621250399533892,
131
+ "n_qubits": 3,
132
+ "n_iterations": 2
133
+ },
134
+ {
135
+ "example_id": "b05",
136
+ "dataset_label": "consistent",
137
+ "expected": "consistent",
138
+ "predicted": "consistent",
139
+ "agrees": true,
140
+ "verify_seconds": 0.016958011998212896,
141
+ "n_qubits": 2,
142
+ "n_iterations": 2
143
+ },
144
+ {
145
+ "example_id": "b06",
146
+ "dataset_label": "inconsistent",
147
+ "expected": "inconsistent",
148
+ "predicted": "inconsistent",
149
+ "agrees": true,
150
+ "verify_seconds": 0.024013021000428125,
151
+ "n_qubits": 2,
152
+ "n_iterations": 2
153
+ },
154
+ {
155
+ "example_id": "c01",
156
+ "dataset_label": "consistent",
157
+ "expected": "consistent",
158
+ "predicted": "consistent",
159
+ "agrees": true,
160
+ "verify_seconds": 0.03195743799733464,
161
+ "n_qubits": 4,
162
+ "n_iterations": 3
163
+ },
164
+ {
165
+ "example_id": "c02",
166
+ "dataset_label": "inconsistent",
167
+ "expected": "inconsistent",
168
+ "predicted": "inconsistent",
169
+ "agrees": true,
170
+ "verify_seconds": 0.04545175699604442,
171
+ "n_qubits": 4,
172
+ "n_iterations": 3
173
+ },
174
+ {
175
+ "example_id": "c03",
176
+ "dataset_label": "consistent",
177
+ "expected": "consistent",
178
+ "predicted": "consistent",
179
+ "agrees": true,
180
+ "verify_seconds": 0.0189066829989315,
181
+ "n_qubits": 3,
182
+ "n_iterations": 2
183
+ },
184
+ {
185
+ "example_id": "c04",
186
+ "dataset_label": "consistent",
187
+ "expected": "consistent",
188
+ "predicted": "consistent",
189
+ "agrees": true,
190
+ "verify_seconds": 0.018903102005424444,
191
+ "n_qubits": 3,
192
+ "n_iterations": 2
193
+ },
194
+ {
195
+ "example_id": "c05",
196
+ "dataset_label": "inconsistent",
197
+ "expected": "inconsistent",
198
+ "predicted": "inconsistent",
199
+ "agrees": true,
200
+ "verify_seconds": 0.021963377002975903,
201
+ "n_qubits": 3,
202
+ "n_iterations": 2
203
+ },
204
+ {
205
+ "example_id": "c06",
206
+ "dataset_label": "consistent",
207
+ "expected": "consistent",
208
+ "predicted": "consistent",
209
+ "agrees": true,
210
+ "verify_seconds": 0.0176239339998574,
211
+ "n_qubits": 2,
212
+ "n_iterations": 2
213
+ },
214
+ {
215
+ "example_id": "d01",
216
+ "dataset_label": "consistent",
217
+ "expected": "consistent",
218
+ "predicted": "consistent",
219
+ "agrees": true,
220
+ "verify_seconds": 0.02074646999972174,
221
+ "n_qubits": 2,
222
+ "n_iterations": 2
223
+ },
224
+ {
225
+ "example_id": "d02",
226
+ "dataset_label": "inconsistent",
227
+ "expected": "inconsistent",
228
+ "predicted": "inconsistent",
229
+ "agrees": true,
230
+ "verify_seconds": 0.029774761002045125,
231
+ "n_qubits": 2,
232
+ "n_iterations": 2
233
+ },
234
+ {
235
+ "example_id": "d03",
236
+ "dataset_label": "consistent",
237
+ "expected": "consistent",
238
+ "predicted": "consistent",
239
+ "agrees": true,
240
+ "verify_seconds": 0.019483926000248175,
241
+ "n_qubits": 2,
242
+ "n_iterations": 2
243
+ },
244
+ {
245
+ "example_id": "d04",
246
+ "dataset_label": "inconsistent",
247
+ "expected": "inconsistent",
248
+ "predicted": "inconsistent",
249
+ "agrees": true,
250
+ "verify_seconds": 0.024527371999283787,
251
+ "n_qubits": 2,
252
+ "n_iterations": 2
253
+ },
254
+ {
255
+ "example_id": "d05",
256
+ "dataset_label": "consistent",
257
+ "expected": "consistent",
258
+ "predicted": "consistent",
259
+ "agrees": true,
260
+ "verify_seconds": 0.02095619199826615,
261
+ "n_qubits": 2,
262
+ "n_iterations": 2
263
+ },
264
+ {
265
+ "example_id": "d06",
266
+ "dataset_label": "inconsistent",
267
+ "expected": "inconsistent",
268
+ "predicted": "inconsistent",
269
+ "agrees": true,
270
+ "verify_seconds": 0.027239916002145037,
271
+ "n_qubits": 2,
272
+ "n_iterations": 2
273
+ },
274
+ {
275
+ "example_id": "e01",
276
+ "dataset_label": "inconsistent",
277
+ "expected": "inconsistent",
278
+ "predicted": "inconsistent",
279
+ "agrees": true,
280
+ "verify_seconds": 0.017952793001313694,
281
+ "n_qubits": 2,
282
+ "n_iterations": 2
283
+ },
284
+ {
285
+ "example_id": "e02",
286
+ "dataset_label": "consistent",
287
+ "expected": "consistent",
288
+ "predicted": "consistent",
289
+ "agrees": true,
290
+ "verify_seconds": 0.03525932400225429,
291
+ "n_qubits": 4,
292
+ "n_iterations": 3
293
+ },
294
+ {
295
+ "example_id": "e03",
296
+ "dataset_label": "inconsistent",
297
+ "expected": "inconsistent",
298
+ "predicted": "inconsistent",
299
+ "agrees": true,
300
+ "verify_seconds": 0.8611685339928954,
301
+ "n_qubits": 6,
302
+ "n_iterations": 6
303
+ },
304
+ {
305
+ "example_id": "e04",
306
+ "dataset_label": "consistent",
307
+ "expected": "consistent",
308
+ "predicted": "consistent",
309
+ "agrees": true,
310
+ "verify_seconds": 162.7746966440027,
311
+ "n_qubits": 9,
312
+ "n_iterations": 18
313
+ },
314
+ {
315
+ "example_id": "f01",
316
+ "dataset_label": "consistent",
317
+ "expected": "consistent",
318
+ "predicted": "consistent",
319
+ "agrees": true,
320
+ "verify_seconds": 0.004586983995977789,
321
+ "n_qubits": 1,
322
+ "n_iterations": 1
323
+ },
324
+ {
325
+ "example_id": "f02",
326
+ "dataset_label": "inconsistent",
327
+ "expected": "inconsistent",
328
+ "predicted": "inconsistent",
329
+ "agrees": true,
330
+ "verify_seconds": 0.005704925999452826,
331
+ "n_qubits": 1,
332
+ "n_iterations": 1
333
+ },
334
+ {
335
+ "example_id": "f03",
336
+ "dataset_label": "consistent",
337
+ "expected": "consistent",
338
+ "predicted": "consistent",
339
+ "agrees": true,
340
+ "verify_seconds": 0.008855961998051498,
341
+ "n_qubits": 2,
342
+ "n_iterations": 2
343
+ },
344
+ {
345
+ "example_id": "f04",
346
+ "dataset_label": "consistent",
347
+ "expected": "consistent",
348
+ "predicted": "consistent",
349
+ "agrees": true,
350
+ "verify_seconds": 0.009374143999593798,
351
+ "n_qubits": 2,
352
+ "n_iterations": 2
353
+ },
354
+ {
355
+ "example_id": "f05",
356
+ "dataset_label": "inconsistent",
357
+ "expected": "inconsistent",
358
+ "predicted": "inconsistent",
359
+ "agrees": true,
360
+ "verify_seconds": 0.013478348999342415,
361
+ "n_qubits": 2,
362
+ "n_iterations": 2
363
+ },
364
+ {
365
+ "example_id": "f06",
366
+ "dataset_label": "inconsistent",
367
+ "expected": "inconsistent",
368
+ "predicted": "inconsistent",
369
+ "agrees": true,
370
+ "verify_seconds": 0.009732865000842139,
371
+ "n_qubits": 2,
372
+ "n_iterations": 2
373
+ },
374
+ {
375
+ "example_id": "f07",
376
+ "dataset_label": "consistent",
377
+ "expected": "consistent",
378
+ "predicted": "consistent",
379
+ "agrees": true,
380
+ "verify_seconds": 0.01844363800046267,
381
+ "n_qubits": 4,
382
+ "n_iterations": 3
383
+ },
384
+ {
385
+ "example_id": "f08",
386
+ "dataset_label": "inconsistent",
387
+ "expected": "inconsistent",
388
+ "predicted": "inconsistent",
389
+ "agrees": true,
390
+ "verify_seconds": 0.026018026997917332,
391
+ "n_qubits": 4,
392
+ "n_iterations": 3
393
+ },
394
+ {
395
+ "example_id": "f09",
396
+ "dataset_label": "consistent",
397
+ "expected": "consistent",
398
+ "predicted": "consistent",
399
+ "agrees": true,
400
+ "verify_seconds": 0.01415224900119938,
401
+ "n_qubits": 3,
402
+ "n_iterations": 2
403
+ },
404
+ {
405
+ "example_id": "f10",
406
+ "dataset_label": "inconsistent",
407
+ "expected": "inconsistent",
408
+ "predicted": "inconsistent",
409
+ "agrees": true,
410
+ "verify_seconds": 0.015700916999776382,
411
+ "n_qubits": 3,
412
+ "n_iterations": 2
413
+ },
414
+ {
415
+ "example_id": "g01",
416
+ "dataset_label": "consistent",
417
+ "expected": "consistent",
418
+ "predicted": "consistent",
419
+ "agrees": true,
420
+ "verify_seconds": 0.013543050998123363,
421
+ "n_qubits": 3,
422
+ "n_iterations": 2
423
+ },
424
+ {
425
+ "example_id": "g02",
426
+ "dataset_label": "inconsistent",
427
+ "expected": "inconsistent",
428
+ "predicted": "inconsistent",
429
+ "agrees": true,
430
+ "verify_seconds": 0.015096809001988731,
431
+ "n_qubits": 3,
432
+ "n_iterations": 2
433
+ },
434
+ {
435
+ "example_id": "g03",
436
+ "dataset_label": "consistent",
437
+ "expected": "consistent",
438
+ "predicted": "consistent",
439
+ "agrees": true,
440
+ "verify_seconds": 0.015624907995515969,
441
+ "n_qubits": 4,
442
+ "n_iterations": 3
443
+ },
444
+ {
445
+ "example_id": "g04",
446
+ "dataset_label": "inconsistent",
447
+ "expected": "inconsistent",
448
+ "predicted": "inconsistent",
449
+ "agrees": true,
450
+ "verify_seconds": 0.011863673993502744,
451
+ "n_qubits": 3,
452
+ "n_iterations": 2
453
+ },
454
+ {
455
+ "example_id": "g05",
456
+ "dataset_label": "consistent",
457
+ "expected": "consistent",
458
+ "predicted": "consistent",
459
+ "agrees": true,
460
+ "verify_seconds": 0.010823272001289297,
461
+ "n_qubits": 3,
462
+ "n_iterations": 2
463
+ },
464
+ {
465
+ "example_id": "g06",
466
+ "dataset_label": "consistent",
467
+ "expected": "consistent",
468
+ "predicted": "consistent",
469
+ "agrees": true,
470
+ "verify_seconds": 0.01448877400252968,
471
+ "n_qubits": 3,
472
+ "n_iterations": 2
473
+ },
474
+ {
475
+ "example_id": "g07",
476
+ "dataset_label": "inconsistent",
477
+ "expected": "inconsistent",
478
+ "predicted": "inconsistent",
479
+ "agrees": true,
480
+ "verify_seconds": 0.021978369004500564,
481
+ "n_qubits": 3,
482
+ "n_iterations": 2
483
+ },
484
+ {
485
+ "example_id": "g08",
486
+ "dataset_label": "inconsistent",
487
+ "expected": "inconsistent",
488
+ "predicted": "inconsistent",
489
+ "agrees": true,
490
+ "verify_seconds": 0.13563275200431235,
491
+ "n_qubits": 6,
492
+ "n_iterations": 6
493
+ },
494
+ {
495
+ "example_id": "g09",
496
+ "dataset_label": "inconsistent",
497
+ "expected": "inconsistent",
498
+ "predicted": "inconsistent",
499
+ "agrees": true,
500
+ "verify_seconds": 0.3194446280031116,
501
+ "n_qubits": 6,
502
+ "n_iterations": 6
503
+ },
504
+ {
505
+ "example_id": "g10",
506
+ "dataset_label": "inconsistent",
507
+ "expected": "inconsistent",
508
+ "predicted": "inconsistent",
509
+ "agrees": true,
510
+ "verify_seconds": 0.016149044000485446,
511
+ "n_qubits": 3,
512
+ "n_iterations": 2
513
+ }
514
+ ]
515
+ }