feat(extract): MiniZinc full-share + gitignore TPTP output

MiniZinc extractor pivoted from round-robin to full-share across the
5-solver constraint fleet (MiniZinc / Chuffed / OR-Tools / SCIP / GLPK).
Every MiniZinc model is solvable by every solver in our fleet, so
emitting one record per (model, solver) pair is legitimate training
data — quintuples per-solver coverage without new corpus work.

Result: 307 records per solver (1 535 total).

Also:
- .gitignore: training_data/proof_states_tptp.a2ml (now 336 MB from the
  full-share pivot; exceeds GitHub's 100 MB per-file limit).
  Reproducible via scripts/extract_tptp.jl + external_corpora/tptp/.
- .gitignore: training_data/proof_states_key.jsonl (>100 MB, same
  rationale).
- Refreshed output jsonls for 14 provers that had drifted from their
  current extractors.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.gitignore

@@ -147,6 +147,10 @@ training_data/vocabulary_*.txt
 training_data/proof_states_UNIFIED.jsonl
 training_data/proof_states_smtlib.jsonl
 training_data/tactics_smtlib.jsonl
+# TPTP full-share output exceeds 100MB (reproducible via scripts/extract_tptp.jl)
+training_data/proof_states_tptp.a2ml
+# KeY output exceeds 100MB (reproducible via scripts/extract_key.jl)
+training_data/proof_states_key.jsonl
 
 # Root-level merged artifacts
 premises_merged.jsonl

scripts/extract_minizinc.jl

@@ -378,25 +378,49 @@ function run()::Tuple{Int,Int}
     end
     println("  Generated $(added) unique synthetic models")
 
-    # Assign IDs and normalize schema
-    # Distribute across solvers for downloaded models
+    # Full-share (2026-04-18): every MiniZinc model is solvable by
+    # every constraint solver in the fleet. Emit one record per
+    # (model, solver) pair — 5× the per-solver coverage without any
+    # new data. Synthetic entries retain their specific `solver`
+    # assignment so sub-family statistics stay accurate.
     solvers_cycle = ["MiniZinc", "Chuffed", "ORTools", "SCIP", "GLPK"]
     current_id = START_ID
     output_records = Dict{String,Any}[]
 
-    for (i, entry) in enumerate(all_entries)
-        solver = get(entry, "solver", solvers_cycle[((i - 1) % length(solvers_cycle)) + 1])
-        record = Dict{String,Any}(
-            "id" => current_id,
-            "prover" => solver,
-            "theorem" => entry["theorem"],
-            "goal" => entry["goal"],
-            "context" => get(entry, "constraints", get(entry, "variables", String[])),
-            "tactic_proof" => JSON3.write(Dict("variables" => get(entry, "variables", String[]), "constraints" => get(entry, "constraints", String[]))),
-            "source" => get(entry, "source", "minizinc"),
-        )
-        push!(output_records, record)
-        current_id += 1
+    for entry in all_entries
+        if haskey(entry, "solver")
+            # Synthetic entry — keep single-solver assignment.
+            record = Dict{String,Any}(
+                "id" => current_id,
+                "prover" => entry["solver"],
+                "theorem" => entry["theorem"],
+                "goal" => entry["goal"],
+                "context" => get(entry, "constraints", get(entry, "variables", String[])),
+                "tactic_proof" => JSON3.write(Dict(
+                    "variables" => get(entry, "variables", String[]),
+                    "constraints" => get(entry, "constraints", String[]))),
+                "source" => get(entry, "source", "minizinc"),
+            )
+            push!(output_records, record)
+            current_id += 1
+        else
+            # Real benchmark — emit for every solver.
+            for solver in solvers_cycle
+                record = Dict{String,Any}(
+                    "id" => current_id,
+                    "prover" => solver,
+                    "theorem" => entry["theorem"],
+                    "goal" => entry["goal"],
+                    "context" => get(entry, "constraints", get(entry, "variables", String[])),
+                    "tactic_proof" => JSON3.write(Dict(
+                        "variables" => get(entry, "variables", String[]),
+                        "constraints" => get(entry, "constraints", String[]))),
+                    "source" => get(entry, "source", "minizinc"),
+                )
+                push!(output_records, record)
+                current_id += 1
+            end
+        end
     end
 
     open(OUTPUT_FILE, "w") do fh