# HG changeset patch
# User webertj
# Date 1127509130 -7200
# Node ID 1330157e156a0bc975e0dc322e78b450efe71508
# Parent  73397145d58a732723ed55e2b781f3ea9965994d
new sat tactic imports resolution proofs from zChaff

diff -r 73397145d58a -r 1330157e156a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Sep 23 22:49:25 2005 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 23 22:58:50 2005 +0200
@@ -91,12 +91,13 @@
   Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
   Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
-  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
+  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
   Tools/ATP/recon_transfer_proof.ML			\
   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
   Tools/ATP/watcher.ML 					\
+  Tools/cnf_funcs.ML					\
   Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
   Tools/datatype_codegen.ML Tools/datatype_package.ML				\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
@@ -108,6 +109,7 @@
   Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
   Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML		\
   Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML				\
+  Tools/sat_funcs.ML					\
   Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
   Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
   Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
@@ -598,7 +600,7 @@
   ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
   ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML	\
   ex/Recdefs.thy ex/Records.thy ex/Reflected_Presburger.thy		\
-  ex/Refute_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy		\
+  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy		\
   ex/StringEx.thy ex/Tarski.thy ex/Tuple.thy ex/document/root.bib	\
   ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/set.thy	\
   ex/svc_funcs.ML ex/svc_test.ML ex/svc_test.thy
diff -r 73397145d58a -r 1330157e156a src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Sep 23 22:49:25 2005 +0200
+++ b/src/HOL/Main.thy	Fri Sep 23 22:58:50 2005 +0200
@@ -5,7 +5,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Refute Reconstruction
+imports Refute Reconstruction SAT
 begin
 
 text {*
diff -r 73397145d58a -r 1330157e156a src/HOL/SAT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SAT.thy	Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,41 @@
+(*  Title:      HOL/SAT.thy
+    ID:         $Id$
+    Author:     Alwen Tiu, Tjark Weber
+    Copyright   2005
+
+Basic setup for the 'sat' tactic.
+*)
+
+header {* Reconstructing external resolution proofs for propositional logic *}
+
+theory SAT imports HOL
+
+uses "Tools/sat_solver.ML"
+     "Tools/cnf_funcs.ML"
+     "Tools/sat_funcs.ML"
+
+begin
+
+ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
+
+method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
+  "SAT solver"
+
+method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
+  "SAT solver (with definitional CNF)"
+
+(*
+method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
+  "Transforming hypotheses in a goal into CNF"
+
+method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
+  "Transforming the conclusion of a goal to CNF"
+
+method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
+  "Same as cnf, but remove the original hypotheses"
+
+method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
+  "Same as cnf_thin, but may introduce extra variables"
+*)
+
+end
diff -r 73397145d58a -r 1330157e156a src/HOL/Tools/cnf_funcs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,660 @@
+(*  Title:      HOL/Tools/cnf_funcs.ML
+    ID:         $Id$
+    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+    Copyright   2005
+
+  Description:
+  This file contains functions and tactics to transform a formula into 
+  Conjunctive Normal Forms (CNF). 
+  A formula in CNF is of the following form:
+
+      (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
+
+  where each xij is a literal (i.e., positive or negative propositional
+  variables).
+  This kind of formula will simply be referred to as CNF.
+  A disjunction of literals is referred to as "clause".
+
+  For the purpose of SAT proof reconstruction, we also make use of another
+  representation of clauses, which we call the "raw clauses".
+  Raw clauses are of the form
+
+      (x1 ==> x2 ==> .. ==> xn ==> False)
+
+  where each xi is a literal. Note that the above raw clause corresponds
+  to the clause (x1' | ... | xn'), where each xi' is the negation normal
+  form of ~xi.
+
+  Notes for current revision:
+  - the "definitional CNF transformation" (anything with prefix cnfx_ )
+    introduces new literals of the form (lit_i) where i is an integer.
+    For these functions to work, it is necessary that no free variables
+    which names are of the form lit_i appears in the formula being
+    transformed.
+*)
+
+
+(***************************************************************************)
+
+signature CNF =
+sig
+  val cnf_tac : Tactical.tactic
+  val cnf_thin_tac : Tactical.tactic
+  val cnfx_thin_tac : Tactical.tactic
+  val cnf_concl_tac : Tactical.tactic
+  val weakening_tac : int -> Tactical.tactic
+  val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
+  val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
+  val is_atm : Term.term -> bool
+  val is_lit : Term.term -> bool
+  val is_clause : Term.term -> bool
+  val is_raw_clause : Term.term -> bool
+  val cnf2raw_thm : Thm.thm -> Thm.thm
+  val cnf2raw_thms : Thm.thm list -> Thm.thm list
+  val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
+end
+
+
+(***************************************************************************)
+
+structure cnf : CNF =
+struct
+
+val cur_thy = the_context();
+val mk_disj = HOLogic.mk_disj;
+val mk_conj = HOLogic.mk_conj;
+val mk_imp  = HOLogic.mk_imp;
+val Not = HOLogic.Not;
+val false_const = HOLogic.false_const;
+val true_const = HOLogic.true_const;
+
+
+(* Index for new literals *)
+val lit_id = ref 0;
+
+fun thm_by_auto G =
+    prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
+
+(***************************************************************************)
+
+
+val cnf_eq_id = thm_by_auto "(P :: bool) = P";
+
+val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
+
+val cnf_not_true_false = thm_by_auto "~True = False";
+
+val cnf_not_false_true = thm_by_auto "~False = True";
+
+val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
+
+val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
+
+val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
+
+val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
+
+val cnf_double_neg = thm_by_auto "(~~P) = P";
+ 
+val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
+
+val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
+
+val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
+
+val cnf_disj_false = thm_by_auto "(False | P) = P";
+
+val cnf_disj_true = thm_by_auto "(True | P) = True";
+
+val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
+
+val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
+
+val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
+
+val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
+
+val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
+
+val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
+
+val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
+
+val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
+
+val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
+
+val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
+
+val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
+
+val cnf_newlit = thm_by_auto 
+    "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
+
+val cnf_all_ex = thm_by_auto 
+    "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
+
+(* [| P ; ~P |] ==> False *)
+val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
+
+val cnf_dneg = thm_by_auto "P ==> ~~P";
+
+val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
+
+val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
+
+(***************************************************************************)
+
+fun is_atm (Const("Trueprop",_) $ x) = is_atm x
+  | is_atm (Const("==>",_) $ x $ y) = false
+  | is_atm (Const("False",_)) = false
+  | is_atm (Const("True", _)) = false
+  | is_atm (Const("op &",_) $ x $ y) = false
+  | is_atm (Const("op |",_) $ x $ y) = false
+  | is_atm (Const("op -->",_) $ x $ y) = false
+  | is_atm (Const("Not",_) $ x) = false
+  | is_atm t = true
+
+
+fun is_lit (Const("Trueprop",_) $ x) = is_lit x
+  | is_lit (Const("Not", _) $ x) = is_atm x
+  | is_lit t = is_atm t
+
+fun is_clause (Const("Trueprop",_) $ x) = is_clause x
+  | is_clause (Const("op |", _) $ x $ y) = 
+          (is_clause x) andalso (is_clause y)
+  | is_clause t = is_lit t
+
+fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
+  | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
+  | is_cnf t = is_clause t
+
+
+(* Checking for raw clauses *)
+fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
+  | is_raw_clause (Const("==>",_) $ x $ 
+                   (Const("Trueprop",_) $ Const("False",_))) = is_lit x
+  | is_raw_clause (Const("==>",_) $ x $ y) = 
+        (is_lit x) andalso (is_raw_clause y)
+  | is_raw_clause t = false
+
+
+
+(* Translate a CNF clause into a raw clause *)
+fun cnf2raw_thm c =
+let val nc = c RS cnf_notE
+in
+rule_by_tactic (REPEAT_SOME (fn i => 
+               rtac cnf_dneg i 
+               ORELSE rtac cnf_neg_disjI i)) nc
+handle THM _ => nc
+end
+
+fun cnf2raw_thms nil = nil
+  | cnf2raw_thms (c::l) =
+    let val t = term_of (cprop_of c)
+    in
+       if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
+       else cnf2raw_thms l
+    end
+
+
+(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
+   association list, relating literals to their indices *)
+
+local
+  (* maps atomic formulas to variable numbers *)
+  val dictionary : ((Term.term * int) list) ref = ref nil;
+  val var_count = ref 0;
+  val pAnd = PropLogic.And;
+  val pOr = PropLogic.Or;
+  val pNot = PropLogic.Not;
+  val pFalse = PropLogic.False;
+  val pTrue = PropLogic.True;
+  val pVar = PropLogic.BoolVar;
+
+  fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
+    | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
+    | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
+    | mk_clause (Const("True",_)) = pTrue
+    | mk_clause (Const("False",_)) = pFalse
+    | mk_clause t =
+      let
+         val idx = AList.lookup op= (!dictionary) t
+      in
+         case idx of
+            (SOME x) => pVar x
+           | NONE =>
+             let
+                val new_var = inc var_count
+             in
+                dictionary := (t, new_var) :: (!dictionary);
+                pVar new_var
+             end
+      end
+
+   fun mk_clauses nil = pTrue
+     | mk_clauses (x::nil) = mk_clause x
+     | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
+
+in
+   fun cnf2prop thms =
+   (
+     var_count := 0;
+     dictionary := nil;
+     (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
+   )
+end
+
+
+
+(* Instantiate a theorem with a list of terms *)
+fun inst_thm sign l thm = 
+  instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
+
+(* Tactic to remove the first hypothesis of the first subgoal. *) 
+fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
+
+(* Tactic for removing the n first hypotheses of the first subgoal. *)
+fun weakenings_tac 0 state = all_tac state
+  | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
+
+
+(* 
+  Transform a formula into a "head" negation normal form, that is, 
+  the top level connective is not a negation, with the exception
+  of negative literals. Returns the pair of the head normal term with
+  the theorem corresponding to the transformation.
+*)
+fun head_nnf sign (Const("Not",_)  $ (Const("op &",_) $ x $ y)) =
+    let val t = mk_disj(Not $ x, Not $ y)
+        val neg_thm = inst_thm sign [x, y] cnf_neg_conj 
+    in
+        (t, neg_thm)
+    end
+
+  | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
+    let val t = mk_conj(Not $ x, Not $ y)
+        val neg_thm =  inst_thm sign [x, y] cnf_neg_disj; 
+    in
+        (t, neg_thm)
+    end
+
+  | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) = 
+    let val t = mk_conj(x, Not $ y)
+        val neg_thm = inst_thm sign [x, y] cnf_neg_imp
+    in
+        (t, neg_thm)
+    end
+
+  | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
+    (x, inst_thm sign [x] cnf_double_neg)
+
+  | head_nnf sign (Const("Not",_) $ Const("True",_)) = 
+      (false_const, cnf_not_true_false)
+
+  | head_nnf sign (Const("Not",_) $ Const("False",_)) = 
+      (true_const, cnf_not_false_true)  
+
+  | head_nnf sign t = 
+    (t, inst_thm sign [t] cnf_eq_id)
+
+
+(***************************************************************************)
+(*                  Tactics for simple CNF transformation                  *)
+
+(* A naive procedure for CNF transformation:
+   Given any t, produce a theorem t = t', where t' is in
+   conjunction normal form 
+*)
+fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
+  | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
+  | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
+ 
+  | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
+       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
+           val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op &", _) $ x $ y) = 
+       let val cnf1 = mk_cnf_thm sign x;
+           val cnf2 = mk_cnf_thm sign y;
+       in
+           cnf_comb2eq OF [cnf1, cnf2]
+       end
+
+  | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) = 
+        cnf_not_true_false
+
+  | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) = 
+        cnf_not_false_true
+
+  | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
+      ( 
+       if (is_atm x) then inst_thm sign [t] cnf_eq_id
+       else
+         let val (t1, hn_thm) = head_nnf sign t
+             val cnf_thm = mk_cnf_thm sign t1
+         in
+             cnf_eq_trans OF [hn_thm, cnf_thm]
+         end
+       ) 
+
+  | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
+       let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
+           val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
+       in
+          cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
+       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
+           val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
+       in
+          cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
+       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
+           val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
+       let val thm1 = inst_thm sign [p] cnf_disj_false;
+           val thm2 = mk_cnf_thm sign p
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
+       inst_thm sign [p] cnf_disj_true
+
+  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
+       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
+           val thm2 = mk_cnf_thm sign p
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
+       inst_thm sign [p] cnf_disj_not_false
+
+  | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) = 
+       if (is_lit p) then
+          (
+            if (is_clause t) then inst_thm sign [t] cnf_eq_id
+            else 
+             let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
+                 val thm2 = mk_cnf_thm sign (mk_disj(q, p))
+             in
+                cnf_eq_trans OF [thm1, thm2]
+             end
+          )
+       else 
+            let val (u, thm1) = head_nnf sign p;
+                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
+                val thm3 = mk_cnf_thm sign (mk_disj(u, q))
+            in
+                cnf_eq_trans OF [(thm1 RS thm2), thm3]
+            end
+
+ | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
+    (* error ("I don't know how to handle the formula " ^ 
+                          (Sign.string_of_term sign t))
+    *)
+
+fun term_of_thm c = term_of (cprop_of c)
+
+
+(* Transform a given list of theorems (thms) into CNF *)
+
+fun mk_cnf_thms sg nil = nil
+  | mk_cnf_thms sg (x::l) = 
+    let val t = term_of_thm x
+    in
+      if (is_clause t) then x :: mk_cnf_thms sg l
+      else 
+       let val thm1 = mk_cnf_thm sg t
+           val thm2 = cnf_eq_imp OF [thm1, x]
+       in 
+           thm2 :: mk_cnf_thms sg l
+       end
+    end
+
+
+(* Count the number of hypotheses in a formula *)
+fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
+  | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
+  | num_of_hyps t = 0
+
+(* Tactic for converting to CNF (in primitive form): 
+   it takes the first subgoal of the proof state, transform all its
+   hypotheses into CNF (in primivite form) and remove the original 
+   hypotheses.
+*)
+fun cnf_thin_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of 
+  [] => Seq.empty
+| (subgoal::_) => 
+  let 
+    val n = num_of_hyps (strip_all_body subgoal);
+    val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
+  in
+    (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
+  end
+end
+
+(* Tactic for converting to CNF (in primitive form), keeping 
+   the original hypotheses. *)
+
+fun cnf_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of 
+  [] => Seq.empty
+| (subgoal::_) => 
+   METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1 
+                    THEN (REPEAT (etac conjE 1)) ) 1 state
+end
+
+
+(***************************************************************************)
+(*            CNF transformation by introducing new literals               *)
+
+(*** IMPORTANT: 
+  This transformation uses variables of the form "lit_i", where i is a natural
+  number. For the transformation to work, these variables must not already
+  occur freely in the formula being transformed.
+***)
+
+fun ext_conj x p q r =
+   mk_conj(
+    mk_disj(Not $ x, p),
+    mk_conj(
+      mk_disj(Not $ x, q),
+      mk_conj(
+        mk_disj(x, mk_disj(Not $ p, Not $ q)),
+        mk_disj(x, r)
+      )
+    )
+   )
+
+
+(* Transform to CNF in primitive forms, possibly introduce extra variables *)
+fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x 
+  | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
+  | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
+  | mk_cnfx_thm sign (Const("op -->", _) $ x $ y)  =
+       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
+           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y)) 
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnfx_thm sign (Const("op &", _) $ x $ y)  = 
+       let val cnf1 = mk_cnfx_thm sign x
+           val cnf2 = mk_cnfx_thm sign y
+       in
+           cnf_comb2eq OF [cnf1, cnf2]
+       end
+
+  | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) = 
+        cnf_not_true_false
+
+  | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_))  = 
+        cnf_not_false_true
+
+  | mk_cnfx_thm sign (t as (Const("Not", _) $ x))  =
+      ( 
+       if (is_atm x) then inst_thm sign [t] cnf_eq_id
+       else
+         let val (t1, hn_thm) = head_nnf sign t
+             val cnf_thm = mk_cnfx_thm sign t1 
+         in
+             cnf_eq_trans OF [hn_thm, cnf_thm]
+         end
+       ) 
+
+  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r)  =
+      if (is_lit r) then
+        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
+            val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
+        in
+           cnf_eq_trans OF [thm1, thm2]
+        end
+      else cnfx_newlit sign p q r 
+
+  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r)  =
+       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
+           val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r))) 
+       in
+          cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
+       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
+           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r))) 
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p)  =
+       let val thm1 = inst_thm sign [p] cnf_disj_false;
+           val thm2 = mk_cnfx_thm sign p 
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p)  =
+       inst_thm sign [p] cnf_disj_true
+
+  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p)  =
+       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
+           val thm2 = mk_cnfx_thm sign p 
+       in
+           cnf_eq_trans OF [thm1, thm2]
+       end
+
+  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p)  =
+       inst_thm sign [p] cnf_disj_not_false
+
+  | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q))  = 
+       if (is_lit p) then
+          (
+            if (is_clause t) then inst_thm sign [t] cnf_eq_id
+            else 
+             let val thm1 = inst_thm sign [p, q] cnf_disj_sym
+                 val thm2 = mk_cnfx_thm sign (mk_disj(q, p)) 
+             in
+                cnf_eq_trans OF [thm1, thm2]
+             end
+          )
+       else 
+            let val (u, thm1) = head_nnf sign p
+                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
+                val thm3 = mk_cnfx_thm sign (mk_disj(u, q)) 
+            in
+                cnf_eq_trans OF [(thm1 RS thm2), thm3]
+            end
+
+ | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^ 
+                          (Sign.string_of_term sign t))
+
+and cnfx_newlit sign p q r  = 
+   let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
+       val _ = (lit_id := !lit_id + 1)
+       val ct_lit = cterm_of sign lit
+       val x_conj = ext_conj lit p q r
+       val thm1 = inst_thm sign [p,q,r] cnf_newlit
+       val thm2 = mk_cnfx_thm sign x_conj 
+       val thm3 = forall_intr ct_lit thm2
+       val thm4 = strip_shyps (thm3 COMP allI)
+       val thm5 = strip_shyps (thm4 RS cnf_all_ex)
+   in
+       cnf_eq_trans OF [thm1, thm5]
+   end
+
+
+(* Theorems for converting formula into CNF (in primitive form), with 
+   new extra variables *)
+
+
+fun mk_cnfx_thms sg nil = nil
+  | mk_cnfx_thms sg (x::l) = 
+    let val t = term_of_thm x
+    in
+      if (is_clause t) then x :: mk_cnfx_thms sg l
+      else 
+       let val thm1 = mk_cnfx_thm sg t
+           val thm2 = cnf_eq_imp OF [thm1,x]
+       in 
+           thm2 :: mk_cnfx_thms sg l
+       end
+    end
+
+
+(* Tactic for converting hypotheses into CNF, possibly
+   introducing new variables *)
+
+fun cnfx_thin_tac state =
+let val sg = Thm.sign_of_thm state
+in
+case (prems_of state) of 
+  [] => Seq.empty
+| (subgoal::_) => 
+   let val n = num_of_hyps (strip_all_body subgoal);
+       val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
+   in
+      EVERY [tac1, weakenings_tac n, 
+             REPEAT (etac conjE 1 ORELSE etac exE 1)] state
+   end
+end
+
+(* Tactic for converting the conclusion of a goal into CNF *)
+
+fun get_concl (Const("Trueprop", _) $ x) = get_concl x
+  | get_concl (Const("==>",_) $ x $ y) = get_concl y
+  | get_concl t = t
+
+fun cnf_concl_tac' state =
+case (prems_of state) of 
+  [] => Seq.empty
+| (subgoal::_) =>
+  let val sg = Thm.sign_of_thm state
+      val c = get_concl subgoal
+      val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
+      val thm2 = thm1 RS subst
+  in
+    rtac thm2 1 state
+  end
+
+val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1 
+
+
+end (*of structure*)
diff -r 73397145d58a -r 1330157e156a src/HOL/Tools/sat_funcs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/sat_funcs.ML	Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,328 @@
+(*  Title:      HOL/Tools/sat_funcs.ML
+    ID:         $Id$
+    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+    Copyright   2005
+
+
+Proof reconstruction from SAT solvers.
+
+  Description:
+    This file defines several tactics to invoke a proof-producing
+    SAT solver on a propositional goal in clausal form.
+
+    We use a sequent presentation of clauses to speed up resolution
+    proof reconstruction. 
+    We call such clauses as "raw clauses", which are of the form
+          [| c1; c2; ...; ck |] ==> False
+    where each clause ci is of the form
+          [|l1,  l2,  ..., lm |] ==> False,
+    where li is a literal  (see also comments in cnf_funcs.ML).
+
+    -- observe that this is the "dualized" version of the standard
+       clausal form
+           l1' \/ l2' \/ ... \/ lm', where li is the negation normal
+       form of ~li'.
+       The tactic produces a clause representation of the given goal
+       in DIMACS format and invokes a SAT solver, which should return
+       a proof consisting of a sequence of resolution steps, indicating
+       the two input clauses and the variable resolved upon, and resulting
+       in new clauses, leading to the empty clause (i.e., False).
+       The tactic replays this proof in Isabelle and thus solves the
+       overall goal.
+
+   There are two SAT tactics available. They differ in the CNF transformation
+   used. The "sat_tac" uses naive CNF transformation to transform the theorem
+   to be proved before giving it to SAT solver. The naive transformation in 
+   some worst case can lead to explonential blow up in formula size.
+   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
+   which produces formula of linear size increase compared to the input formula.
+   This transformation introduces new variables. See also cnf_funcs.ML for
+   more comments.
+
+
+ Notes for the current revision:
+   - The current version supports only zChaff prover.
+   - The environment variable ZCHAFF_HOME must be set to point to
+     the directory where zChaff executable resides
+   - The environment variable ZCHAFF_VERSION must be set according to
+     the version of zChaff used. Current supported version of zChaff:
+     zChaff version 2004.11.15
+
+*)
+
+(***************************************************************************)
+(** Array of clauses **)
+
+signature CLAUSEARR =
+sig
+   val init : int -> unit 
+   val register_at : int -> Thm.thm -> unit
+   val register_list : Thm.thm list -> unit
+   val getClause : int -> Thm.thm option
+end
+
+structure ClauseArr : CLAUSEARR =
+struct
+
+val clauses : ((Thm.thm option) array) ref = ref (Array.array(1, NONE));
+
+fun init size = (clauses := Array.array(size, NONE))
+
+fun register_at i c =  Array.update (!clauses, i, (SOME c))
+
+fun reg_list n nil = ()
+  | reg_list n (x::l) = 
+     (register_at n x; reg_list (n+1) l)
+
+fun register_list l = reg_list 0 l
+
+fun getClause i = Array.sub (!clauses, i)
+
+end
+
+
+(***************************************************************************)
+
+signature SAT =
+sig
+  val trace_sat : bool ref      (* trace tactic *)
+  val sat_tac : Tactical.tactic
+  val satx_tac : Tactical.tactic
+end
+
+functor SATFunc (structure cnf_struct : CNF) : SAT =
+struct
+
+structure cnf = cnf_struct
+
+val trace_sat = ref false;	(* debugging flag *)
+
+
+(* Look up the Isabelle atom corresponding to a DIMACS index in the
+   reverse dictionary. This entry should exist, otherwise an error
+   is raised.
+*)
+fun rev_lookup idx dictionary = 
+let
+   fun rev_assoc [] = NONE
+     | rev_assoc ((key, entry)::list) =
+       if entry = idx then SOME key else rev_assoc list
+in
+   the (rev_assoc dictionary)
+end;
+
+
+(* Convert rules of the form
+   l1 ==> l2 ==> .. ==> li ==> .. ==> False
+    to
+   l1 ==> l2 ==> .... ==> ~li
+*)
+fun swap_prem rslv c = 
+let 
+    val thm1 = rule_by_tactic (metacut_tac c 1  THEN 
+                  (atac 1) THEN (REPEAT_SOME atac)) rslv
+in
+    rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
+end
+
+(*** Proof reconstruction: given two clauses
+   [| x1 ; .. ; a ; .. ; xn |] ==> False
+   and 
+   [| y1 ; .. ; ~a ; .. ; ym |] ==> False , 
+
+   we firt convert the first clause into
+
+   [| x1 ; ... ; xn |] ==> ~a     (using swap_prem)
+
+   and do a resolution with the second clause to produce
+   [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False
+
+***)
+
+fun dual (Const("Trueprop",_) $ x) (Const("Trueprop",_) $ y) = dual x y
+  | dual (Const("Not",_) $ x) y = (x = y)
+  | dual x (Const("Not",_) $ y) = (x = y)
+  | dual x y = false
+
+(* Check if an atom has a dual in a list of atoms *)
+
+fun dual_mem x nil = false
+  | dual_mem x (y::l) = if (dual x y) then true else dual_mem x l
+
+
+fun replay_chain sg idx (c::cs) =
+let
+   val (SOME fc) = ClauseArr.getClause c;
+
+   fun strip_neg (Const("Trueprop", _) $ x) = strip_neg x
+     | strip_neg (Const("Not",_) $ x) = x
+     | strip_neg x = x
+
+   (* Find out which atom (literal) is used in the resolution *)
+   fun res_atom nil l = raise THM ("Proof reconstruction failed!", 0, [])
+     | res_atom (x::l1) l2 = 
+        if (dual_mem x l2) then strip_neg x
+        else res_atom l1 l2
+
+   fun replay old [] = old
+     | replay old (cls :: clss) =
+       let
+          val (SOME icls) = ClauseArr.getClause cls;
+          val var = res_atom (prems_of old) (prems_of icls);
+          val atom = cterm_of sg var;
+          val rslv = instantiate' [] [SOME atom] notI;
+
+          val _ = if (!trace_sat) then
+            (
+              writeln "-- resolving clause:";
+              print_thm old;
+              writeln "-- with clause: ";
+              print_thm icls;
+              writeln "-- using ";
+              writeln (string_of_cterm atom)
+            ) else ();
+
+          val thm1 = (
+              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icls
+              handle THM _ =>
+              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icls))) old );
+
+          val new = rule_by_tactic distinct_subgoals_tac thm1;
+          val _ = if (!trace_sat) then (writeln "-- resulting clause:"; print_thm new)
+                  else ()
+       in
+          replay new clss 
+       end
+in
+   ClauseArr.register_at idx (replay fc cs);
+   if (!trace_sat) then (
+      writeln ("-- Replay chain successful. " ^ 
+               "The resulting clause stored at #" ^ (Int.toString idx))
+   ) else ()
+end
+
+
+(* Replay the resolution proof from file prf_file with hypotheses hyps.
+   Returns the theorem established by the proof (which is just False).
+*)
+fun replay_prf sg tab size =
+  let
+     val prf = Inttab.dest tab;
+
+     fun complete nil = true
+       | complete (x::l) = (
+           case ClauseArr.getClause x of 
+             NONE => false
+           | (SOME _) => complete l)
+
+     fun do_chains [] = ()
+       | do_chains (pr :: rs) = 
+         let val (idx, cls) = pr
+         in
+            if (complete cls) then  
+               (replay_chain sg idx cls; do_chains rs)
+            else do_chains (rs @ [pr])
+         end
+  in
+    if (!trace_sat) then (
+        writeln "Proof trace from SAT solver: ";
+        print prf ; ()
+     ) else () ;
+     do_chains prf;
+     ClauseArr.getClause size
+  end;
+
+
+(***************************************************************************)
+(***                  Functions to build the sat tactic                  ***)
+
+(* A trivial tactic, used in preprocessing before calling the main 
+   tactic *)
+
+val pre_sat_tac  = (REPEAT (etac conjE 1)) THEN 
+                   (REPEAT ((atac 1) ORELSE (etac FalseE 1)))
+
+fun collect_atoms (Const("Trueprop",_) $ x) l = collect_atoms x l
+  | collect_atoms (Const("op |", _) $ x $ y) l = 
+        collect_atoms x (collect_atoms y l) 
+  | collect_atoms x l = if (x mem l) then l else (x::l) 
+
+fun has_duals nil = false
+  | has_duals (x::l) = if (dual_mem x l) then true else has_duals l
+
+fun trivial_clause (Const("True",_)) = true
+  | trivial_clause c = has_duals (collect_atoms c nil)
+
+(* Remove trivial clauses *)
+fun filter_clauses nil = nil
+  | filter_clauses (x::l) =
+    if (trivial_clause (term_of (cprop_of x))) then filter_clauses l
+    else (x:: filter_clauses l)
+
+fun is_true assignment x =
+    case (assignment x) of 
+      NONE => false
+    | SOME b => b
+
+fun get_model dict assignment = 
+    map (fn (x,y) => x) (List.filter (fn (x,y) => is_true assignment y) dict)
+
+fun string_of_model sg nil = ""
+  | string_of_model sg [x] = Sign.string_of_term sg x
+  | string_of_model sg (x::l) = (Sign.string_of_term sg x) ^ ", " ^ (string_of_model sg l)
+
+(* Run external SAT solver with the given clauses. Reconstruct a proof from
+   the resulting proof trace of the SAT solver. 
+*)
+
+fun rawsat_thm sg prems =
+let val thms = filter_clauses prems 
+    val (fm, dict) = cnf.cnf2prop thms
+    val raw_thms = cnf.cnf2raw_thms thms
+in
+   let
+       val result = SatSolver.invoke_solver "zchaff_with_proofs" fm;
+   in
+     case result of
+       (SatSolver.UNSATISFIABLE (SOME (table, size))) => 
+          let val _ = ClauseArr.init (size + 1);
+              val _ = ClauseArr.register_list 
+                      (map (fn x => (rule_by_tactic distinct_subgoals_tac x)) raw_thms);
+              val (SOME thm1) = replay_prf sg table size
+          in 
+              thm1
+          end
+      | (SatSolver.SATISFIABLE model) => 
+          let val msg = "\nSAT solver found a countermodel:\n{ " ^ 
+                        (string_of_model sg (get_model dict model)) ^ " }\n"
+          in
+                raise THM (msg, 0, [])
+          end    
+      | _ => raise THM ("SAT solver failed!\n", 0, [])
+
+  end
+end
+
+fun cnfsat_basic_tac state = 
+let val sg = Thm.sign_of_thm state
+in 
+  METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
+end
+
+(* Tactic for calling external SAT solver, taking as input CNF clauses *)
+val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac)
+
+
+(* 
+   Tactic for calling external SAT solver, taking as input arbitrary formula. 
+*)
+val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;
+
+(* 
+  Tactic for calling external SAT solver, taking as input arbitratry formula.
+  The input is translated to CNF (in primitive form), possibly introducing
+  new literals. 
+*)
+val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;
+
+end (*of structure*)
diff -r 73397145d58a -r 1330157e156a src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Sep 23 22:49:25 2005 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Sep 23 22:58:50 2005 +0200
@@ -45,6 +45,9 @@
 time_use_thy "SVC_Oracle";
 if_svc_enabled time_use_thy "svc_test";
 
+(* requires zChaff with proof generation to be installed: *)
+time_use_thy "SAT_Examples" handle ERROR => ();
+
 time_use_thy "Refute_Examples";
 time_use_thy "Quickcheck_Examples";
 
diff -r 73397145d58a -r 1330157e156a src/HOL/ex/SAT_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Sep 23 22:58:50 2005 +0200
@@ -0,0 +1,212 @@
+(*  Title:      HOL/ex/SAT_Examples.thy
+    ID:         $Id$
+    Author:     Alwen Tiu, Tjark Weber
+    Copyright   2005
+*)
+
+header {* Examples for the 'sat' command *}
+
+theory SAT_Examples imports Main
+
+begin
+
+(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
+
+lemma assumes 1: "~x0"
+and 2: "~x30"
+and 3: "~x29"
+and 4: "~x59"
+and 5: "x1 | x31 | x0"
+and 6: "x2 | x32 | x1"
+and 7: "x3 | x33 | x2"
+and 8: "x4 | x34 | x3"
+and 9: "x35 | x4"
+and 10: "x5 | x36 | x30"
+and 11: "x6 | x37 | x5 | x31"
+and 12: "x7 | x38 | x6 | x32"
+and 13: "x8 | x39 | x7 | x33"
+and 14: "x9 | x40 | x8 | x34"
+and 15: "x41 | x9 | x35"
+and 16: "x10 | x42 | x36"
+and 17: "x11 | x43 | x10 | x37"
+and 18: "x12 | x44 | x11 | x38"
+and 19: "x13 | x45 | x12 | x39"
+and 20: "x14 | x46 | x13 | x40"
+and 21: "x47 | x14 | x41"
+and 22: "x15 | x48 | x42"
+and 23: "x16 | x49 | x15 | x43"
+and 24: "x17 | x50 | x16 | x44"
+and 25: "x18 | x51 | x17 | x45"
+and 26: "x19 | x52 | x18 | x46"
+and 27: "x53 | x19 | x47"
+and 28: "x20 | x54 | x48"
+and 29: "x21 | x55 | x20 | x49"
+and 30: "x22 | x56 | x21 | x50"
+and 31: "x23 | x57 | x22 | x51"
+and 32: "x24 | x58 | x23 | x52"
+and 33: "x59 | x24 | x53"
+and 34: "x25 | x54"
+and 35: "x26 | x25 | x55"
+and 36: "x27 | x26 | x56"
+and 37: "x28 | x27 | x57"
+and 38: "x29 | x28 | x58"
+and 39: "~x1 | ~x31"
+and 40: "~x1 | ~x0"
+and 41: "~x31 | ~x0"
+and 42: "~x2 | ~x32"
+and 43: "~x2 | ~x1"
+and 44: "~x32 | ~x1"
+and 45: "~x3 | ~x33"
+and 46: "~x3 | ~x2"
+and 47: "~x33 | ~x2"
+and 48: "~x4 | ~x34"
+and 49: "~x4 | ~x3"
+and 50: "~x34 | ~x3"
+and 51: "~x35 | ~x4"
+and 52: "~x5 | ~x36"
+and 53: "~x5 | ~x30"
+and 54: "~x36 | ~x30"
+and 55: "~x6 | ~x37"
+and 56: "~x6 | ~x5"
+and 57: "~x6 | ~x31"
+and 58: "~x37 | ~x5"
+and 59: "~x37 | ~x31"
+and 60: "~x5 | ~x31"
+and 61: "~x7 | ~x38"
+and 62: "~x7 | ~x6"
+and 63: "~x7 | ~x32"
+and 64: "~x38 | ~x6"
+and 65: "~x38 | ~x32"
+and 66: "~x6 | ~x32"
+and 67: "~x8 | ~x39"
+and 68: "~x8 | ~x7"
+and 69: "~x8 | ~x33"
+and 70: "~x39 | ~x7"
+and 71: "~x39 | ~x33"
+and 72: "~x7 | ~x33"
+and 73: "~x9 | ~x40"
+and 74: "~x9 | ~x8"
+and 75: "~x9 | ~x34"
+and 76: "~x40 | ~x8"
+and 77: "~x40 | ~x34"
+and 78: "~x8 | ~x34"
+and 79: "~x41 | ~x9"
+and 80: "~x41 | ~x35"
+and 81: "~x9 | ~x35"
+and 82: "~x10 | ~x42"
+and 83: "~x10 | ~x36"
+and 84: "~x42 | ~x36"
+and 85: "~x11 | ~x43"
+and 86: "~x11 | ~x10"
+and 87: "~x11 | ~x37"
+and 88: "~x43 | ~x10"
+and 89: "~x43 | ~x37"
+and 90: "~x10 | ~x37"
+and 91: "~x12 | ~x44"
+and 92: "~x12 | ~x11"
+and 93: "~x12 | ~x38"
+and 94: "~x44 | ~x11"
+and 95: "~x44 | ~x38"
+and 96: "~x11 | ~x38"
+and 97: "~x13 | ~x45"
+and 98: "~x13 | ~x12"
+and 99: "~x13 | ~x39"
+and 100: "~x45 | ~x12"
+and 101: "~x45 | ~x39"
+and 102: "~x12 | ~x39"
+and 103: "~x14 | ~x46"
+and 104: "~x14 | ~x13"
+and 105: "~x14 | ~x40"
+and 106: "~x46 | ~x13"
+and 107: "~x46 | ~x40"
+and 108: "~x13 | ~x40"
+and 109: "~x47 | ~x14"
+and 110: "~x47 | ~x41"
+and 111: "~x14 | ~x41"
+and 112: "~x15 | ~x48"
+and 113: "~x15 | ~x42"
+and 114: "~x48 | ~x42"
+and 115: "~x16 | ~x49"
+and 116: "~x16 | ~x15"
+and 117: "~x16 | ~x43"
+and 118: "~x49 | ~x15"
+and 119: "~x49 | ~x43"
+and 120: "~x15 | ~x43"
+and 121: "~x17 | ~x50"
+and 122: "~x17 | ~x16"
+and 123: "~x17 | ~x44"
+and 124: "~x50 | ~x16"
+and 125: "~x50 | ~x44"
+and 126: "~x16 | ~x44"
+and 127: "~x18 | ~x51"
+and 128: "~x18 | ~x17"
+and 129: "~x18 | ~x45"
+and 130: "~x51 | ~x17"
+and 131: "~x51 | ~x45"
+and 132: "~x17 | ~x45"
+and 133: "~x19 | ~x52"
+and 134: "~x19 | ~x18"
+and 135: "~x19 | ~x46"
+and 136: "~x52 | ~x18"
+and 137: "~x52 | ~x46"
+and 138: "~x18 | ~x46"
+and 139: "~x53 | ~x19"
+and 140: "~x53 | ~x47"
+and 141: "~x19 | ~x47"
+and 142: "~x20 | ~x54"
+and 143: "~x20 | ~x48"
+and 144: "~x54 | ~x48"
+and 145: "~x21 | ~x55"
+and 146: "~x21 | ~x20"
+and 147: "~x21 | ~x49"
+and 148: "~x55 | ~x20"
+and 149: "~x55 | ~x49"
+and 150: "~x20 | ~x49"
+and 151: "~x22 | ~x56"
+and 152: "~x22 | ~x21"
+and 153: "~x22 | ~x50"
+and 154: "~x56 | ~x21"
+and 155: "~x56 | ~x50"
+and 156: "~x21 | ~x50"
+and 157: "~x23 | ~x57"
+and 158: "~x23 | ~x22"
+and 159: "~x23 | ~x51"
+and 160: "~x57 | ~x22"
+and 161: "~x57 | ~x51"
+and 162: "~x22 | ~x51"
+and 163: "~x24 | ~x58"
+and 164: "~x24 | ~x23"
+and 165: "~x24 | ~x52"
+and 166: "~x58 | ~x23"
+and 167: "~x58 | ~x52"
+and 168: "~x23 | ~x52"
+and 169: "~x59 | ~x24"
+and 170: "~x59 | ~x53"
+and 171: "~x24 | ~x53"
+and 172: "~x25 | ~x54"
+and 173: "~x26 | ~x25"
+and 174: "~x26 | ~x55"
+and 175: "~x25 | ~x55"
+and 176: "~x27 | ~x26"
+and 177: "~x27 | ~x56"
+and 178: "~x26 | ~x56"
+and 179: "~x28 | ~x27"
+and 180: "~x28 | ~x57"
+and 181: "~x27 | ~x57"
+and 182: "~x29 | ~x28"
+and 183: "~x29 | ~x58"
+and 184: "~x28 | ~x58"
+shows "False"
+using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 
+20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 
+40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 
+60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 
+80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 
+100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 
+120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 
+140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 
+160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 
+180 181 182 183 184 
+by sat
+
+end