REFUTATION
==========

  policy        policy.co
  sha256        470bfaea5ca9297edde3c6f9dd1287ac090b0db94091edd9bf067c4d63c22ec5
  parse         clean: the circuit carries every edge the file describes
  unroll        none
  question      can respond with permitted high risk answer fire with risk_warning_given false?
  pin           respond with permitted high risk answer = 1   (action)
  pin           risk_warning_given = 0   (obligation)
  pin           product_is_nmmi = 1   (conditioning)
  origin        external_oracle
  replayable    no

  A row below was asserted by an external decision procedure. Checking
  it means running that procedure again; nothing here can stand in for
  it.

DERIVATION
----------


  final  0 = 1 was asserted directly by this row (cryptominisat-phase0) rather than derived, so there is no step to replay.

WHAT THIS ESTABLISHES
---------------------

  The derivation is valid: the listed steps really do combine the listed
  rows into 0 = 1. It does not establish that those rows are the policy.
  The citations above say where each row was compiled from, and they are
  the compiler's own record rather than an independent check of it --
  closing that second hop means re-deriving the circuit and comparing.