// test case for CNF reduction
// shows three programs P1,P2,P3
// where P2 is a reduction of P1 and 
// P3 is a reduction of P2.
<program>
<let> 
  <assignment>
    <pos> a </pos>  
  </assignment>
  <let>
    <assignment>
      <pos> b </pos> 
    </assignment>
    <cnf> 
      <clause>
        <weight> 2 </weight> 
	  <literals>
	  <pos> a </pos>
	  <neg> b </neg>
	  </literals>
      </clause>
      <clause>
        <weight> 3 </weight> 
	  <literals>
	  <neg> a </neg>
	  <neg> b </neg>
	  </literals>
      </clause>
      <sat> 
        <clausecount> 5 </clausecount>
      </sat>
      <unsat> 
        <clausecount> 10 </clausecount>
      </unsat>
    </cnf>
  </let>
</let>
<let>
  <assignment>
    <pos> b </pos>
  </assignment>
  <cnf>
    <clause>
      <weight> 3 </weight>
        <literals>
	  <neg> b </neg>
        </literals>
    </clause>
      <sat> 
        <clausecount> 7 </clausecount>
      </sat>
      <unsat> 
        <clausecount> 10 </clausecount>
      </unsat>
  </cnf>
</let>
  <cnf>
      <sat> 
        <clausecount> 7 </clausecount>
      </sat>
      <unsat> 
        <clausecount> 13 </clausecount>
      </unsat>
  </cnf>
</program>

//  let !b in 
//    cnf (
//      3 (b))
//    sat 2

//    cnf ()
//    sat 2
//    unsat 3