(* Resolution prover on h1 clauses.
   Copyright (C) 2003-2005 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "clause_h";
open "heap_h";
open "verbose_h";
open "rel_h";
open "sort_h";
open "scc_h";
open "topsort_h";
open "gensym_h";
open "intersym_h";

(*$P+*)

fun head_vars (HVAR _) = {1}
  | head_vars (HFUN (_, _, _, xs, _)) = xs
  | head_vars _ = {};

fun al_vars al = union {tvars t
		       | (_, t) in list al};

fun clause_vars (CL (h, ql, al, Bs, ...)) =
    head_vars h U
    al_vars al U
    dom Bs;

(* Clause printing functions: *)

fun print_q (f as |[put, ...]|) q =
    let val delimr = ref "#ne("
    in
	iterate
	  (put (!delimr); delimr := " & "; put P)
	| P in set q
	end;
	put ")"
    end;

exception PrintVarNotInEnv of int;

fun print_head (f as |[put, ...]|, xname, vars) =
    let val pdterm1 = print_term (f, vars)
	val pq = print_q f
	fun phead (HVAR P) = (put P; put "("; pdterm1 (V 1); put ")")
	  | phead (HFUN (P, f, k, xs, t)) =
	    (put P; if invisible_fun f
			then (put " "; pdterm1 t)
		    else (put "("; pdterm1 t; put ")"))
	  | phead (HQ q) = pq q
	  | phead (HBOT name) = (put "#false("; put name; put ")")
    in
	phead
    end;

fun clause_var_names xname =
    let val f as |[convert, put, seek, truncate, ...]| = outstring xname
	val n = size xname
	fun vname i =  (seek n; truncate ();
			print f (pack i);
			convert ())
    in
	fn c =>
	   {i => vname i
	   | i in set clause_vars c}
    end;

fun invisible_term (f $ nil) = invisible_fun f
  | invisible_term _ = false;

fun noshow_term (x, t) = invisible_term t orelse t=V x;

fun print_clause (f as |[put, ...]|, xname) =
    let val pq = print_q f
	val cvarnames = clause_var_names xname
    in
	fn (c as CL (h, ql, al, Bs, ...)) =>
	   let val vars = cvarnames c
	       val getvars = ?vars
	       val pt = print_term (f, getvars)
	       val delimr = ref " :- "
	   in
	       print_head (f, xname, getvars) h;
	       iterate
		 (put (!delimr); delimr := ", "; pq q)
	       | q in set ql
	       end;
	       iterate
		 (put (!delimr); delimr := ", ";
		  put P; if invisible_fun g
			     then (put " "; pt t)
			 else (put "("; pt t; put ")"))
	       | (P, t as g $ _) in list al
	       end;
	       iterate
		 iterate
		   (put (!delimr); delimr := ", ";
		    put P; put "(";
		    if i inset vars
			then put (?vars i)
		    else raise PrintVarNotInEnv i;
			put ")")
		 | P in set blk
		 end
	       | i => blk in map Bs
	       end;
	       put "."
	   end
    end;

val perrclause = print_clause (stderr, "X");

fun print_h_al (f as |[put, ...]|, xname) =
    let val pq = print_q f
    in
	fn ((h, al), Bss) =>
	   let val fvars = head_vars h U al_vars al U
		   union {dom Bs | Bs in set Bss}
	       val vars = let val f as |[convert, put, seek, ...]| = outstring xname
			      val n = size xname
			  in
			      {i => (seek n;
				     print f (pack i);
				     convert ())
			      | i in set fvars}
			  end
	       val getvars = ?vars
	       val pt = print_term (f, getvars)
	       val delimr = ref " :- "
	   in
	       print_head (f, xname, getvars) h;
	       iterate
		 (put (!delimr); delimr := ", ";
		  put P; put " "; pt t)
	       | (P, t) in list al
	       end;
	       put (!delimr);
	       delimr := "| ";
	       iterate
		 (put (!delimr);
		  delimr := "";
		  iterate
		    iterate
		      (put (!delimr); delimr := ", ";
		       put P; put " ";
		       if i inset vars
			   then put (?vars i)
		       else raise PrintVarNotInEnv i)
		    | P in set blk
		    end
		  | i => blk in map Bs
		  end;
		  put ".";
		  delimr := "\t... | ")
	       | Bs => (_, pi) in map Bss
	       end
	   end
    end;

val perr_h_al = print_h_al (stderr, "X");

exception InconsistentSig of string;

fun sig_add (f, k, sigmap) =
    if f inset sigmap
	then if ?sigmap f = k
		 then sigmap
	     else raise InconsistentSig f
    else sigmap ++ {f => k};

fun head_sig (HVAR _, acc) = acc
  | head_sig (HFUN (_, f, k, ...), acc) = sig_add (f, k, acc)
  | head_sig (_, acc) = acc;

fun t_sig (V _, acc) = acc
  | t_sig (f $ l, acc) =
    tl_sig (l, sig_add (f, len l, acc))
and tl_sig (nil, acc) = acc
  | tl_sig (t::l, acc) =
    tl_sig (l, t_sig (t, acc));

fun al_sig (nil, acc) = acc
  | al_sig ((_, t)::al, acc) =
    al_sig (al, t_sig (t, acc));

fun clause_sig (CL (h, ql, al, Bs, ...), acc) =
    head_sig (h, al_sig (al, acc));

fun clause_list_sig_1 (nil, acc) = acc
  | clause_list_sig_1 (c :: l, acc) =
    clause_list_sig_1 (l, clause_sig (c, acc));

fun clause_list_sig cl = clause_list_sig_1 (cl, {});

fun head_preds (HVAR P) = {P}
  | head_preds (HFUN (P, ...)) = {P}
  | head_preds _ = {};

fun al_preds nil = {}
  | al_preds ((P, _)::al) =
    {P} U al_preds al;

fun Bs_preds Bs = union {blk
			| _ => blk in map Bs};

fun clause_preds (CL (h, ql, al, Bs, ...)) =
    head_preds h U al_preds al U Bs_preds Bs;

fun clause_list_preds cl = union {clause_preds c
				 | c in list cl};

fun clause_bots (CL (HBOT botname, ...)) = {botname}
  | clause_bots _ = {};

fun clause_list_bots cl = union {clause_bots c
				| c in list cl};

(* The standard ordering on atoms: *)

(*** The old ordering, used when we selected just one atom
 from clauses.

(* Assume there are nf function symbols.
 Given a random ground term t, the probability P(u) that it is matched by
 some term u, under simplistic probabilistic assumptions, is:
 P(V x) = 1
 P(f(u1, ..., un)) = 1/nf . P(u1) ... P(un).
 So:
 log P (V x) = 0
 log P(f(u1,...,un)) = -log nf + sum_i log P (ui).
 In particular, log P(u) is the size of u, counting variables as 0,
 up to some (negative) multiplicative constant.

 We prefer to select negative literals u that have the least chance of
 being matched, that is, with log P(u) minimal, therefore of maximal size.
 We then organize bodies of clauses (the al field) so that atoms (of depth>=1)
 are listed in reverse order of size.
 For any two atoms with the same size, we then select the one with the
 lexicographically smallest predicate symbol.
*)

memofun t_size (V _) = 0
      | t_size (f $ l) =
	tl_size (l, 1)
with tl_size (t::l, n) = tl_size (l, t_size t+n)
   | tl_size (_, n) = n;

fun atom_less ((P, t), (P', t')) =
    let val n = t_size t
	val n' = t_size t'
    in
	n > n' orelse
	n=n' andalso P strless P'
    end;
 ***)

(* The new ordering, much simpler. *)

fun term_less (V x, V y) = x > y
  | term_less (V _, _ $ _) = true
  | term_less (f $ l, f' $ l') =
    f strless f' orelse
    f=f' andalso tl_less (l, l')
  | term_less _ = false
and tl_less (nil, nil) = false
  | tl_less (nil, _) = true
  | tl_less (t::l, t' :: l') =
    term_less (t, t') orelse
    t=t' andalso tl_less (l, l')
  | tl_less _ = false;

local val nfa = re_make_nfa [(re_parse "^__type_", fn _ => 1),
			     (re_parse "^__def_", fn _ => ~1)]
in
      memofun pred_cat P =
	      case nfa_run (nfa, P) of
		  SOME cat => cat
		| NONE => 0
end;

fun atom_less ((P, t), (P', t')) =
    let val c = pred_cat P
	val c' = pred_cat P'
    in
	c < c' orelse
	c=c' andalso (P strless P' orelse
		      P=P' andalso term_less (t, t'))
    end;

(***
(* Even simpler: *)

val atom_less = system_less; (* Problem: clause_from_seidl uses atom_sort,
			      but gc may be called between two calls to
			      clause_from_seidl on the same clause, and
			      this may foil this ordering. *)
***)

fun atom_merge (atl as at::atr, atl' as at' :: atr') =
    if atom_less (at, at')
	then at' :: atom_merge (atl, atr')
    else if at=at'
	then at :: atom_merge (atr, atr')
    else at :: atom_merge (atr, atl')
  | atom_merge (nil, atl') = atl'
  | atom_merge (atl, nil) = atl;

fun atom_insert (at, atl' as at' :: atr') =
    if atom_less (at, at')
	then at' :: atom_insert (at, atr')
    else if at=at'
	then atl'
    else at::atl'
  | atom_insert (at, nil) = [at];

fun atom_sort {} = []
  | atom_sort {at} = [at]
  | atom_sort ats = let val (ats1, ats2) = split ats
		    in
			atom_merge (atom_sort ats1, atom_sort ats2)
		    end;

(*
exception CheckAtomSort;

fun check_atom_sort (a :: (l as a' :: _)) =
    if a=a' orelse atom_less (a, a')
	then raise CheckAtomSort
    else check_atom_sort l
  | check_atom_sort _ = ();
*)

exception GenResolvent;

fun default_do_bot c = raise BotFoundEvt c;

fun al_less (nil, nil) = false
  | al_less (nil, _) = true
  | al_less ((maxd, atl)::al, (maxd', atl')::al') =
    maxd < maxd' orelse (maxd=maxd' andalso
			 let val l = len atl
			     val l' = len atl'
			 in
			     l < l' orelse
			     (l=l' andalso al_less (al, al'))
			 end)
  | al_less _ = false;

fun t_size (V _) = 0
      | t_size (f $ l) =
	tl_size (l, 1)
and tl_size (t::l, n) = tl_size (l, t_size t+n)
  | tl_size (_, n) = n;

fun al_len ((_, t)::al, acc) =
    al_len (al, t_size t+acc+1)
  | al_len (_, acc) = acc;

fun Bs_len {} = 0
  | Bs_len {_ => B} U rest = card B + Bs_len rest;

(*
fun clause_category (CL (_, {}, nil, {}, ...)) = 0
  | clause_category (CL (HBOT _, _, ...)) = 3
  | clause_category (CL (_, _, nil, {}, ...)) = 1
  | clause_category (CL (h, ql, al, Bs, ...)) =
    if empty ql
	then (*if null al
		 then 4 + Bs_len Bs
	     else*) al_len (al, 10000000 + Bs_len Bs)
    else 2;
*)

val pred_less = op strless;
val pred_sort = sort pred_less;

datatype blocks = BS_ONE (* {{}} *)
       | BS_ZERO (* {} *)
       | BS_B of atom * blocks * blocks;
	 (* BS_B (a, b1, b2) = (a::b1) U b2 *)

fun atoms_from_Bs Bs =
    union {{(P, x)
	   | P in set B}
	  | i => B in map Bs
	      val x = V i};

fun bs_from_al nil = BS_ONE
  | bs_from_al (a::rest) =
    BS_B (a, bs_from_al rest, BS_ZERO);

fun bs_add (Bs, blks) =
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	fun bs_add_1 (al, BS_ZERO) = bs_from_al al
	  | bs_add_1 (nil, blks) = BS_ONE (* subsumes blkls *)
	  | bs_add_1 (_, BS_ONE) = BS_ONE (* subsumed *)
	  | bs_add_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
	    if a=a'
		then BS_B (a, bs_add_1 (rest, b1), b2)
	    else if atom_less (a, a') (* a' is first *)
		then BS_B (a', b1, bs_add_1 (al, b2))
	    else (* a is first *)
		BS_B (a, bs_from_al rest, b)
    in
	bs_add_1 (al, blks)
    end;

fun bs_make (a, BS_ZERO, b2) = b2
  | bs_make (a, b1, b2) = BS_B (a, b1, b2);

fun bs_rem (Bs, blks) =
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	fun bs_rem_1 (_, BS_ZERO) = BS_ZERO
	  | bs_rem_1 (nil, BS_ONE) = BS_ZERO
	  | bs_rem_1 (nil, BS_B (_, _, b2)) =
	    bs_rem_1 (nil, b2)
	  | bs_rem_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
	    if a=a'
		then bs_make (a, bs_rem_1 (rest, b1), b2)
	    else if atom_less (a, a') (* a' is first *)
		then bs_make (a', b1, bs_rem_1 (al, b2))
	    else (* a is first *)
		b
    in
	bs_rem_1 (al, blks)
    end;

fun bs_subsumed (Bs, blks) = (* tests whether Bs is subsumed by (contains)
			      some Bs' in blks. *)
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	memofun bs_subsumed_1 (_, BS_ZERO) = false
	      | bs_subsumed_1 (_, BS_ONE) = true
	      | bs_subsumed_1 (nil, _) = false
	      | bs_subsumed_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
		if a=a'
		    then bs_subsumed_1 (rest, b1) orelse
			bs_subsumed_1 (rest, b2)
		else if atom_less (a, a') (* a' is first *)
		    then bs_subsumed_1 (al, b2)
		else (* a is first *)
		    bs_subsumed_1 (rest, b)
    in
	bs_subsumed_1 (al, blks)
    end;

fun B_add (Bs, i, P) =
    if i inset Bs
	then Bs ++ {i => ?Bs i U {P}}
    else Bs ++ {i => {P}};

fun blkls_from_blocks () =
    let memofun blkls_from_blocks_1 BS_ZERO = {}
	      | blkls_from_blocks_1 BS_ONE = {{}}
	      | blkls_from_blocks_1 (BS_B ((P, V i), b1, b2)) =
		{B_add (Bs', i, P)
		| Bs' in set blkls_from_blocks_1 b1}
		U blkls_from_blocks_1 b2
    in
	blkls_from_blocks_1
(*
	fn b => (
#put stdout "*** Extracting blocks from ";
pretty stdout (pack b);
		 let val Bss = blkls_from_blocks_1 b
		 in
#put stdout "*** Result: ";
pretty stdout (pack Bss);
		     Bss
		 end
		 )
*)
    end;

fun bs_subsumes (Bs : int -m> block, blks : blocks) =
    (* returns all Bs' in blkls that Bs subsumes (is contained in).
     *)
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	val blkls_from_blocks_1 = blkls_from_blocks ()
	memofun bs_subsumes_1 (nil, b) = blkls_from_blocks_1 b
	      | bs_subsumes_1 (_, BS_ZERO) = {}
	      | bs_subsumes_1 (_, BS_ONE) = {}
	      | bs_subsumes_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
		if a=a'
		    then let val (P, V i) = a
			 in
			     {B_add (Bs', i, P)
			     | Bs' in set bs_subsumes_1 (rest, b1)}
			 end
		else if atom_less (a, a')
		    then (* a' is first *)
			let val (P, V i) = a
			in
			    {B_add (Bs', i, P)
			    | Bs' in set bs_subsumes_1 (al, b1)}
			end U bs_subsumes_1 (al, b2)
		else (* a is first *)
		    {}
    in
	bs_subsumes_1 (al, blks)
    end;

fun bs_count_subsumes (Bs, blks) =
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	memofun count_blocks BS_ZERO = 0
	      | count_blocks BS_ONE = 1
	      | count_blocks (BS_B (_, b1, b2)) =
		count_blocks b1 + count_blocks b2
	memofun bs_count_subsumes_1 (nil, b) = count_blocks b
	      | bs_count_subsumes_1 (_, BS_ZERO) = 0
	      | bs_count_subsumes_1 (_, BS_ONE) = 0
	      | bs_count_subsumes_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
		if a=a'
		    then bs_count_subsumes_1 (rest, b1)
		else if atom_less (a, a')
		    then (* a' is first *)
			bs_count_subsumes_1 (al, b1) +
			bs_count_subsumes_1 (al, b2)
		else (* a is first *)
		    0
    in
	bs_count_subsumes_1 (al, blks)
    end;

fun bs_elim_subsumes (Bs, blks) =
    (* eliminates all Bs' in blks that Bs subsumes (is contained in).
     *)
    let val al = atom_sort (atoms_from_Bs Bs)
	    (* al puts the largest atoms first. *)
	memofun bs_elim_subsumes_1 (nil, _) = BS_ZERO
	      | bs_elim_subsumes_1 (_, BS_ZERO) = BS_ZERO
	      | bs_elim_subsumes_1 (_, BS_ONE) = BS_ONE
	      | bs_elim_subsumes_1 (al as (a::rest), b as BS_B (a', b1, b2)) =
		if a=a'
		    then bs_make (a, bs_elim_subsumes_1 (rest, b1), b2)
		else if atom_less (a, a')
		    then (* a' is first *)
			bs_make (a', bs_elim_subsumes_1 (al, b1),
				 bs_elim_subsumes_1 (al, b2))
		else (* a is first *)
		    b
    in
	bs_elim_subsumes_1 (al, blks)
    end;

(*extern val auto_simple_match_term : automaton -> string * 'a term -> bool;*)
(* auto_simple_match_term auto (P, t)
 quickly tests whether t has a chance of being recognized at P
 in auto.  Not an exact test, except when t is ground.
*)

fun auto_simple_match_term (AUTO (auto, univ)) =
    let memofun auto_simple_match (P, V _) = true
	      | auto_simple_match (P, f $ l) =
		P inset univ orelse
		(P inset auto andalso
		 let val fmap = ?auto P
		 in
		     f inset fmap andalso
		     exists
		       all
			 all
			   auto_simple_match (Q, t)
			 | Q in set blk
			 end
		       || t in list l and
			  blk in list blkl
		       end
		     | blkl in set #1 (?fmap f)
		     end
		 end)
    in
	auto_simple_match
    end;

(* The prover: *)

(*
memofun match_k 0 = {}
      | match_k 1 = {~1 => V 1}
      | match_k n = {~n => V n} ++ match_k (n-1);
*)

exception ResolvePF_BadHead;
exception ResolvePF_BadSelF;
exception ResolvePF_BadSelX;
exception ResolvePF_BadSelQ;
exception ResolvePF_BlackHole;
exception ResolvePFs_BlackHole;
exception ResolveInterFlat;

fun is_tautology (CL (HVAR P, _, _, Bs, ...)) =
    1 inset Bs andalso P inset ?Bs 1
  | is_tautology (CL (HFUN _, _, nil, ...)) = false
  | is_tautology (CL (HFUN (P, _, _, _, t), _, al, ...)) =
    let val a = (P, t)
    in
	exists a=a' | a' in list al end
    end
  | is_tautology (CL (HQ q, ql, ...)) = q inset ql
  | is_tautology _ = false;

fun is_h_al_tauto (HFUN (P, _, _, _, t), al) =
    let val a = (P, t)
    in
	exists a=a' | a' in list al end
    end
  | is_h_al_tauto _ = false;

fun Bs_sub (Bs, Bs') =
    all
      i inset Bs' andalso
      B subset ?Bs' i
    | i => B in map Bs
    end;

fun al_sub (nil, _) = true
  | al_sub (_, nil) = false
  | al_sub (al as (a::rest), al' as (a' :: rest')) =
    if a=a'
	then al_sub (rest, rest')
    else if atom_less (a, a')
	then al_sub (al, rest')
    else false;

fun subsumes (CL (h, ql, al, Bs), CL (h', ql', al', Bs')) =
    (h=h' andalso
     ql subset ql' andalso
     al_sub (al, al') andalso
     Bs_sub (Bs, Bs')) orelse
    (case h of
	 HVAR P =>
	 (case h' of
	      HFUN (P', f, k, vars, t) =>
	      let fun tsub (V 1) = t
		    | tsub (V n) = V (n+k-1)
		    | tsub (g $ l) = g $ [tsub u | u in list l]
	      in
		  P=P' andalso
		  ql subset ql' andalso
		  all
		    i' inset Bs' andalso
		    B subset  ?Bs' i'
		  | i => B in map {1} <-| Bs
		    val i' = i+k-1
		  end andalso
		  al_sub (atom_sort ({(Q, tsub u)
				     | (Q, u) in list al} U
				       {(Q, t)
				       | Q in set if 1 inset Bs
						      then ?Bs 1
						  else {}}
				       ), al')
		  
	      end
	    | _ => false)
       | _ => false);

datatype predicate = P_BOT of string
       | P_PRED of string
       | P_ROOT;

exception ResolveUseful;
exception InfosMax;

fun opt_inter (NONE, fso) = fso
  | opt_inter (fso, NONE) = fso
  | opt_inter (SOME fs, SOME fs') = SOME (fs & fs');


(*
exception RandChoose;

fun rand_choose {} = raise RandChoose
  | rand_choose {i} =  i
  | rand_choose s = let val (s1, s2) = split s
		    in
			if maybe ()
			    then rand_choose s1
			else rand_choose s2
		    end;

fun random_oracle_funs (fargs : string -m> int * int set * int term, dsize : int) =
    let val dsize2 = dsize*dsize
	val D = 0 to dsize-1
	fun rand_table (a, siz) =
	    let val ir = ref siz
	    in
		while (dec ir; !ir>=0) do
		    iupdate (a, !ir, irand dsize)
	    end
	fun rand_permut {} = nil
	  | rand_permut s =
	    let val i = rand_choose s
	    in
		i :: rand_permut (s \ {i})
	    end
	val cons_table = iarrayoflist [j mod dsize
				      | j in list rand_permut (0 to dsize2-1)]
	(* we draw a random surjective function to represent cons pairs;
	 n-ary functions f (t1, ..., tn) are encoded as
	 f (cons (t1, cons (..., cons (tn, nil)))),
	 where nil = 0, and f is a random function from 0..dsize-1 to 0..dsize-1.
	 *)
	val f_tables = {f => iarrayoflist (rand_permut D)
		       | f => (k, ...) in map fargs}
	(* t_table (vars, t) produces a relation mapping
	 cons (x1, ..., cons (xn, nil)) to t
	 where vars = {x1, ..., xn} contains all free variables of t.
	 *)
	fun cons (i, j) =
	    isub (cons_table, dsize*i+j)
	val nihil = 0
	memofun t_table (vars, V x) =
		let val x1 = choose vars
		    val vars' = vars \ {x1}
		in
		    if x1=x
			then if empty vars'
				 then union_rel {{cons (d, nihil) => {d}}
						| d in set D}
			     else union_rel
		end
    in
	rand_table (cons_table, dsize2);

    end;
*)

(*
datatype qenv_set = Q_ONE
       | Q_Z
       | Q_B of int * (string -m> qenv_set); (* variable, then a q_env_set
					      for each value of the variable
					      (which should be a state, i.e.,
					      a string). *)

exception QEnvInter;

fun qenv_funs () =
    let fun q_b (x, {}) = Q_Z
	  | q_b xmap = Q_B xmap
	memofun qenv_union {} = Q_Z
	      | qenv_union {qe} = qe
	      | qenv_union {qe1, qe2} =
		(case qe1 of
		     Q_Z => qe2
		   | Q_ONE => Q_ONE
		   | Q_B (x1, map1) =>
		     (case qe2 of
			  Q_Z => qe1
			| Q_ONE => Q_ONE
			| Q_B (x2, map2) =>
			  if x1 = x2
			      then Q_B (x1, (map1 delta map2) ++
					{P => qenv_union {qe'1, qe'2}
					| P => qe'1 in map map2 <| map1
					  val qe'2 = ?map2 P})
			  else if x1 < x2
			      then Q_B (x1, {P => qenv_union {qe'1, qe2}
					    | P => qe'1 in map map1})
			  else Q_B (x2, {P => qenv_union {qe1, qe'2}
					| P => qe'2 in map map2})
			      ))
	      | qenv_union qes =
		let val (qes1, qes2) = split qes
		in
		    qenv_union {qenv_union qes1, qenv_union qes2}
		end
	memofun qenv_inter {} = raise QEnvInter
	      | qenv_inter {qe} = qe
	      | qenv_inter {qe1, qe2} =
		(case qe1 of
		     Q_Z => Q_Z
		   | Q_ONE => Q_ONE
		   | Q_B (x1, map1) =>
		     (case qe2 of
			  Q_Z => Q_Z
			| Q_ONE => qe1
			| Q_B (x2, map2) =>
			  if x1 = x2
			      then q_b (x1, {P => qe'
					    | P => qe'1 in map map2 <| map1
						val qe'2 = ?map2 P
						val qe' = qenv_inter {qe'1, qe'2}
						    such that qe'<>Q_Z})
			  else if x1 < x2
			      then q_b (x1, {P => qe'
					    | P => qe'1 in map map1
						val qe' = qenv_inter {qe'1, qe2}
						    such that qe'<>Q_Z})
			  else q_b (x2, {P => qe'
					| P => qe'2 in map map2
					    val qe' = qenv_inter {qe1, qe'2}
					    such that qe'<>Q_Z})
			  ))
	      | qenv_inter qes =
		let val (qes1, qes2) = split qes
		in
		    qenv_inter {qenv_inter qes1, qenv_inter qes2}
		end
    in
	|[ union = qenv_union,
	   inter = qenv_inter
	   ]|
    end;

fun auto_match_funs (AUTO (auto, univ)) =
    let val |[union = qenv_union, inter = qenv_inter, ...]| = qenv_funs ()
	memofun auto_match_term (P, t) =
		if P inset univ
		    then Q_ONE
		else case t of
			 V x => Q_B (x, {P => Q_ONE})
		       | f $ l =>
			 if P inset auto
			     then let val fmap = ?auto P
				  in
				      if f inset fmap
					  then qenv_union {auto_match_terml (blkl, l)
							  | blkl in set #1 (?fmap f)}
				      else Q_Z
				  end
			 else Q_Z
	with auto_match_terml (blk::blkl, t::l) =
	     qenv_inter ({auto_match_terml (blkl, l)} U
			   {auto_match_term (P, t)
			   | P in set blk})
	   | auto_match_terml (nil, nil) = Q_ONE
	   | auto_match_terml _ = Q_Z
	fun auto_eval_var (x, Q_ONE) = 
    in
 !!!
    end;
*)

datatype pathset = PS_ALL
       | PS_ENUM of string * int -m> pathset; (* maps (f, i) to non-empty pathset;
					       maps (f, 0) to PS_ALL in case f is a constant. *)

fun print_pathset (|[put, ...]|) =
    let val delimr = ref ""
	val buf as |[put=puts, convert, tell, seek, truncate, ...]| = outstring ""
	fun printps PS_ALL = (put (!delimr); delimr := ", ";
			      truncate (); put (convert ()); put "*")
	  | printps (PS_ENUM fimap) =
	    let val pos = tell ()
	    in
		iterate
		  (seek pos;
		   if i=0
		       then (put (!delimr); delimr := ", ";
			     truncate (); put (convert ()); put f)
		   else (puts f; puts "[";
			 print buf (pack i);
			 puts "]";
			 printps ps)
		       )
		| (f, i) => ps in map fimap
		end
	    end
    in
	fn ps => (delimr := ""; seek 0; printps ps)
    end;

val perr_pathset = print_pathset stderr;

val ps_empty = PS_ENUM {};

fun ps_inter (PS_ALL, ps) = ps
  | ps_inter (ps, PS_ALL) = ps
  | ps_inter (PS_ENUM fimap, PS_ENUM fimap') =
    PS_ENUM {fi => ps''
	    | fi => ps in map (fimap' <| fimap)
		val ps' = ?fimap' fi
		val ps'' = ps_inter (ps, ps')
		such that ps''<>ps_empty};

fun ps_funs PS_ALL = NONE
  | ps_funs (PS_ENUM fimap) = SOME {f | (f, _) in set fimap}

exception NoPathSetEvt;
(*exception NoPathSetBug of string;*)

fun clause_index cl =
    inv_rel {c => {P
		  | (P, _) in list al}
	      U union (rng Bs)
	    | c as CL (_, _, al, Bs) in list cl};

fun compute_skeleta (cl, maxpathlen) =
    let val pathsets = ref ({} : string -m> pathset)
	val qs = ref ({} : block set)
	val bots = ref ({} : string set)

	val ci = clause_index cl

	val changed_P = ref ({} : string set)

	fun ps_union (PS_ALL, _) = PS_ALL
	  | ps_union (_, PS_ALL) = PS_ALL
	  | ps_union (PS_ENUM fimap, PS_ENUM fimap') =
	    PS_ENUM ((fimap delta fimap') ++ {fi => ps_union (ps, ps')
					     | fi => ps in map fimap' <| fimap
						 val ps' = ?fimap' fi})

	fun ps_add (P, ps) =
	    (if P inset !pathsets
		 then let val old = ?(!pathsets) P
			  val new = ps_union (ps, old)
		      in
			  if old=new
			      then ()
			  else (pathsets := !pathsets ++ {P => new};
				changed_P := !changed_P ++ {P})
		      end
	     else (pathsets := !pathsets ++ {P => ps};
		   changed_P := !changed_P ++ {P}))

	fun ps_chop (PS_ALL, _) = PS_ALL
	  | ps_chop (_, 0) = PS_ALL
	  | ps_chop (PS_ENUM fimap, n) =
	    let val n' = n-1
	    in
		PS_ENUM {fi => ps_chop (ps, n')
			| fi => ps in map fimap}
	    end

	memofun psinter x = ps_inter x

	fun ps_match_term (V x, ps, env) =
	    if x inset env
		then let val ps' = psinter (ps, ?env x)
		     in
			 if ps' = ps_empty
			     then raise NoPathSetEvt
			 else env ++ {x => ps'}
		     end
	    else env ++ {x => ps}
	  | ps_match_term (_, PS_ALL, env) = env
	  | ps_match_term (f $ nil, PS_ENUM fimap, env) =
	    if (f, 0) inset fimap
		then env
	    else raise NoPathSetEvt
	  | ps_match_term (f $ l, PS_ENUM fimap, env) =
	    ps_match_term_list (f, l, 1, fimap, env)
	and ps_match_term_list (_, nil, _, _, env) = env
	  | ps_match_term_list (f, ti::l, i, fimap, env) =
	    let val fi = (f, i)
	    in
		if fi inset fimap
		    then let val env' = ps_match_term (ti, ?fimap fi, env)
			 in
			     ps_match_term_list (f, l, i+1, fimap, env')
			 end
		else raise NoPathSetEvt
	    end

	fun ps_match_atom ((P, t), env) =
	    if P inset !pathsets
		then ps_match_term (t, ?(!pathsets) P, env)
	    else raise NoPathSetEvt

	fun ps_match_al (nil, env) = env
	  | ps_match_al (a::al, env) =
	    ps_match_al (al, ps_match_atom (a, env))

	fun blk_pathsets {} = PS_ALL
	  | blk_pathsets {P} = if P inset !pathsets
				   then ?(!pathsets) P
			       else raise NoPathSetEvt
	  | blk_pathsets blk = let val (blk1, blk2) = split blk
				   val ps = psinter (blk_pathsets blk1,
						      blk_pathsets blk2)
			       in
				   if ps=ps_empty
				       then raise NoPathSetEvt
				   else ps
			       end

	fun ps_match_blk (x, blk, env) =
	    let val ps = blk_pathsets blk
	    in
		if x inset env
		    then let val ps' = psinter (ps, ?env x)
			 in
			     if ps' = ps_empty
				 then raise NoPathSetEvt
			     else env ++ {x => ps'}
			 end
		else env ++ {x => ps}
	    end

	fun ps_match_blks ({}, env) = env
	  | ps_match_blks ({x => blk} U rest, env) =
	    ps_match_blks (rest, ps_match_blk (x, blk, env))

	fun ps_eval_clause (c as CL (h, ql, al, Bs, ...)) =
	    if ql subset !qs
		then (let val env = ps_match_blks (Bs, ps_match_al (al, {}))
		      in
			  case h of
			      HQ q => qs := !qs U {q}
			    | HBOT botname => bots := !bots U {botname}
			    | HVAR P => if 1 inset env
					    then ps_add (P, ?env 1)
					else ps_add (P, PS_ALL)
			    | HFUN (P, f, k, vars, ...) =>
			      let val ps = if k=0
					       then PS_ENUM {(f, 0) => PS_ALL}
					  else PS_ENUM {(f, i) => ps_chop (psi, maxpathlen)
						       | i in set vars
							   val psi = if i inset env
									 then ?env i
								     else PS_ALL}
			      in
				  ps_add (P, ps)
			      end
		      end handle NoPathSetEvt => ())
	    else ()

	fun ps_saturate clauses =
	    (changed_P := {};
	     iterate
	       ps_eval_clause c
	     | c in list cl
	     end;
	     while not (empty (!changed_P)) do
		 let val Ps = !changed_P
		 in
		     changed_P := {};
		     iterate
		       ps_eval_clause c
		     | c in set union {cs
				      | _ => cs in map Ps <| ci}
		     end
		 end)
    in
	ps_saturate cl;
	(!pathsets, !bots)
    end;

fun blkl_from_Bs (Bs, k) =
    let val ir = ref 0
    in
	[(inc ir;
	  if !ir inset Bs
	      then ?Bs (!ir)
	  else {})
	|while !ir<k]
    end;

fun revblkl_from_Bs (Bs, k) =
    let val ir = ref k
    in
	[((if !ir inset Bs
	       then ?Bs (!ir)
	   else {})
	      before dec ir)
	|while !ir>0]
    end;

fun Bs_from_blkl blkl =
    let val jr = ref 0
    in
	{!jr => blk
	| blk in list blkl
	    such that (inc jr; not (empty blk))}
    end;

exception BsSubBlkl;

fun Bs_sub_blkl_1 ({}, _) =
    (fn _ => true)
  | Bs_sub_blkl_1 (Bs, i) =
    let val i' = i+1
	val sub_blkl = Bs_sub_blkl_1 ({i'} <-| Bs, i')
    in
	if i' inset Bs
	    then let val B = ?Bs i'
		 in
		     case B of
			 {P} =>
			 (fn (B'::rest) =>
			     P inset B' andalso sub_blkl rest
			   | _ => raise BsSubBlkl)
		       | _ =>
			 (fn (B'::rest) =>
			     B subset B' andalso sub_blkl rest
			   | _ => raise BsSubBlkl)
		 end
	else (fn (_ :: rest) =>
		 sub_blkl rest
	       | _ => raise BsSubBlkl)
    end;

fun Bs_sub_blkl Bs =
    Bs_sub_blkl_1 (Bs, 0)

fun blkl_sub_Bs (blkl, Bs) =
    let val ir = ref 0
    in
	all
	  (inc ir;
	   empty B orelse
	   (!ir inset Bs andalso
	    B subset ?Bs (!ir)))
	| B in list blkl
	end
    end;

(*!!! to finish: might be interesting.
fun compute_char_states (cl, maxq) =
    let val fargs = clause_list_sig cl
	val q_all = "q_all"
	(* first create a state recognizing every term: *)
	val autop = ref {q_all => {f => let val ir = ref 0
					in
					    [(inc ir; q_all)
					    |while !ir<k]
					end
				  | f => k in map fargs}}
	val preds = ref ({} : string -m> string set)
	    (* map predicates to sets of (final) states. *)
	fun newstate_0 () = gensym "$q"
	val remaining_states = ref maxq
	val existing_states = ref {}
	fun random_state {} = newstate_0 ()
	  | random_state {q} = q
	  | random_state s =
	    let val (s1, s2) = split s
	    in
		random_state (if maybe ()
				  then s1
			      else s2)
	    end
	fun newstate () =
	    if !remaining_states=0
		then random_state (!existing_states)
	    else let val q = newstate_0 ()
		 in
		     dec remaining_states;
		     existing_states := !existing_states U {q};
		     q
		 end
	fun auto_match_term 
    in
    end;
*)

(* compute_witnesses tries to compute obvious facts
 derivable from a list cl of clauses. *)
datatype wshape = W_CST
       | W_APP of string -m> wshape list set;

fun w_from_term (V _) = W_CST
  | w_from_term (f $ l) =
    (case l of
	 nil => W_CST
       | _ => W_APP {f => {[w_from_term t | t in list l]}});

fun w_union (W_CST, w) = w
  | w_union (w, W_CST) = w
  | w_union (W_APP fmap, W_APP fmap') =
    W_APP (fmap Urel fmap');

fun w_dunion {} = W_CST
  | w_dunion {w} = w
  | w_dunion ws =
    let val (ws1, ws2) = split ws
    in
	w_union (w_dunion ws1, w_dunion ws2)
    end;

fun w_from_head (HVAR _) = W_CST
  | w_from_head (HFUN (_, _, _, _, t)) = w_from_term t
  | w_from_head _ = W_CST;

fun w_from_clause (CL (h, _, al, Bs, ...)) =
    w_dunion {w_from_term t
	     | (_, t) in list al};

fun w_match (V _, _) = true
  | w_match (_ $ nil, _) = true
  | w_match (_ $ _, W_CST) = false
  | w_match (f $ l, W_APP fmap) =
    f inset fmap andalso
    exists
      all
	w_match (t, w)
      || t in list l and
	 w in list wl
      end
    | wl in set ?fmap f
    end;

exception MatchTermEvt;

fun compute_witnesses (cl, wantproof) =
    let val ci = clause_index cl
	val wsh = w_dunion {w_from_clause c
			   | c in list cl}
	val facts = ref ({} : string -m> unit term set)
	    (* Facts are ground terms.  The special variable V () denotes
	     some fixed constant. *)
	val bots = ref ({} : string set)
	    (* maps botname to proof. *)
	fun match_term (sigma, V x, t) =
	    if x inset sigma
		then if ?sigma x=t
			 then sigma
		     else raise MatchTermEvt
	    else sigma ++ {x => t}
	  | match_term (sigma, f $ l, t) =
	    (case t of
		 f' $ l' =>
		 if f=f'
		     then match_tl (sigma, l, l')
		 else raise MatchTermEvt
	       | _ => raise MatchTermEvt)
	and match_tl (sigma, nil, nil) = sigma
	  | match_tl (sigma, t::l, t'::l') =
	    match_tl (match_term (sigma, t, t'), l, l')
	  | match_tl _ = raise MatchTermEvt

	val changed_P = ref ({} : string set)

	val (p_up, p_up_bot) =
	    case wantproof of
		SOME (f as |[put, ...]|) =>
		let val pclause = print_clause (f, "X")
		    val pt = print_term (f, fn () => "")
		    fun psigma sigma =
			let val sigma' = {x => v
					 | x => v in map sigma
					   such that not (invisible_term v)}
			    val delimr = ref "{"
			in
			    case sigma' of
				{} => ()
			      | _ => 
				(iterate
				   (put (!delimr); delimr := ",";
				    put "X"; print f (pack (x : int));
				    put "="; pt v)
				 | x => v in map sigma'
				 end;
				   put "}")
			end
		    fun p_upl upl =
			iterate
			  (put Q; put " "; pt t; put ". ")
			| (Q, t) in list upl
			end
		    fun p_u (c, sigma, upl) =
			(put "[unit-resolve:\n  ";
			 pclause c; put " "; psigma sigma;
			 put "\n  "; p_upl upl; put "\n  ]\n")
		in
		    (fn (P, v, u) =>
			(put P; put " "; pt v; put ". ";
			 p_u u),
			fn (botname, u) => (put botname; put ". "; p_u u)
			   )
		end
	      | _ => (fn _ => (), fn _ => ())

	fun add_fact (P, v, up) =
	    if P inset !facts
		then let val vs = ?(!facts) P
		     in
			 if v inset vs
			     then ()
			 else (p_up (P, v, up);
			       facts := !facts ++ {P => vs U {v}};
			       changed_P := !changed_P U {P})
		     end
	    else (p_up (P, v, up);
		  facts := !facts ++ {P => {v}};
		  changed_P := !changed_P U {P})

	fun w_eval_clause (c as CL (h, _, al, Bs, ...), newfacts) =
	    if (case h of
		    HBOT botname => botname inset !bots
		  | HQ _ => true (* ignore q heads. *)
		  | _ => false)
		then ()
	    else let fun w_eval_Bs ({}, sigma, upl) =
			 (case h of
			      HVAR P =>
			      let val v = if 1 inset sigma
					      then ?sigma 1
					  else V ()
			      in
				  add_fact (P, v, (c, sigma, rev upl))
			      end
			    | HFUN (P, f, k, vars, ...) =>
			      let val sigma' = sigma ++ {x => V ()
							| x in set sigma <-| vars}
				  val ir = ref 0
				  val v = f $ [(inc ir;
						?sigma' (!ir)
						)
					      |while !ir<k]
			      in
				  if w_match (v, wsh)
				      then add_fact (P, v, (c, sigma', rev upl))
				  else () (* term too large: ignore it. *)
			      end
			    | HBOT botname =>
			      (p_up_bot (botname, (c, sigma, rev upl));
			       bots := !bots U {botname})
			    | _ => ())
		       | w_eval_Bs ({i => B0 as ({P} U B)} U rest, sigma, upl) =
			 if i inset sigma
			     then let val v = ?sigma i
				  in
				      if P inset newfacts
					  then let val vs = ?newfacts P
					       in
						   if v inset vs
						       then w_eval_Bs (if empty B
									   then rest
								       else rest ++ {i => B},
									   sigma, (P, v) :: upl)
						   else ()
					       end
				      else ()
				 end
			 else if (case h of
				 HVAR _ => i<>1
			       | HFUN _ => false
			       | _ => true) (* if we don't need to browse through all values v
					     such that P(v) is derivable; we just need to check
					     whether there is one. *)
			     then (case inter {if Q inset newfacts
						   then ?newfacts Q
					       else {}
					      | Q in set B0} of
				       {v, ...} =>
					 w_eval_Bs (if empty B
							then rest
						    else rest ++ {i => B},
							sigma ++ {i => v},
							(P, v) :: upl)
				     | _ => ())
			 else let val Bs' = if empty B
						then rest
					    else rest ++ {i => B}
			      in
				  iterate
				    w_eval_Bs (Bs', sigma ++ {i => v}, (P, v)::upl)
				  | v in set
				    if P inset newfacts
					then if empty B
						 then ?newfacts P
					     else (inter {?newfacts Q
							 | Q in set B}
						   <| ?newfacts P
						   handle MapGet => {})
				    else {}
				  end
			      end
		     fun w_eval_al (nil, sigma, upl) =
			 w_eval_Bs (Bs, sigma, upl)
		       | w_eval_al ((P, t) :: al, sigma, upl) =
			 iterate
			   (let val sigma' = match_term (sigma, t, v)
			    in
				w_eval_al (al, sigma', (P, v)::upl)
			    end handle MatchTermEvt => ())
			 | v in set
			   if P inset newfacts
			       then ?newfacts P
			   else {}
			 end
	    in
		w_eval_al (al, {}, nil)
	    end

	fun w_saturate clauses =
	    (changed_P := {};
	     iterate
	       w_eval_clause (c, {})
	     | c in list cl
	     end;
	     while not (empty (!changed_P)) do
		 let val Ps = !changed_P
		     val newfacts = !facts
		 in
		     changed_P := {};
		     iterate
		       w_eval_clause (c, newfacts)
		     | c in set union {cs
				      | _ => cs in map Ps <| ci}
		     end
		 end
	     )
    in
	w_saturate cl;
	(!facts, !bots)
    end;

(*
fun opt_dinter {} = NONE
  | opt_dinter {fso} = fso
  | opt_dinter fsos = let val (fsos1, fsos2) = split fsos
		      in
			  opt_inter (opt_dinter fsos1, opt_dinter fsos2)
		      end;
*)

fun iter_sub_map (f, gmap, small_cards, large_cards) =
    let val gmap_list = [(x, y) | x => y in map gmap]
	val card_gmap = len gmap_list
	fun iter_small (0, _, gmap_acc) = f gmap_acc
	  | iter_small (n, gmap_rem, gmap_acc) =
	    let val n1 = n-1
		fun iter_small_pick_1 nil = ()
		  | iter_small_pick_1 ((x,y)::l) =
		    (iter_small (n1, l, gmap_acc ++ {x => y});
		     iter_small_pick_1 l)
	    in
		iter_small_pick_1 gmap_rem
	    end
	fun iter_large (0, _, gmap_acc) = f gmap_acc
	  | iter_large (n, gmap_rem, gmap_acc) =
	    let val n1 = n-1
		fun iter_large_pick_1 nil = ()
		  | iter_large_pick_1 ((x,_)::l) =
		    (iter_large (n1, l, {x} <-| gmap_acc);
		     iter_large_pick_1 l)
	    in
		iter_large_pick_1 gmap_rem
	    end
    in
	iterate
	  iter_small (crd, gmap_list, {})
	| crd in set small_cards
	  such that crd<=card_gmap
	end;
	iterate
	  iter_large (crd, gmap_list, gmap)
	| crd in set large_cards
	  such that not (card_gmap - crd inset small_cards)
	      andalso crd<=card_gmap
	end
    end;

fun iter_sub_Bs f =
    let fun iter ({i => B} U rest) =
	    let val iter' = iter rest
	    in
		fn Bs_acc =>
		   iterate
		     if empty B'
			 then iter' Bs_acc
		     else iter' (Bs_acc ++ {i => B'})
		   | B' sub map B
		   end
	    end
	  | iter _ = f
    in
	fn Bs => iter Bs {}
    end;

(*
fun iter_sub_grad (f, Bs, k, nBs) =
    let fun pick (0, _, acc, _) = f acc
	  | pick (_, {}, _, _) = ()
	  | pick (n, Bs as ({i => B} U rest), acc, nrem) =
	    if n>nrem
		then ()
	    else let val n1 = n-1
		     val nrem1 = nrem-1
		 in
		     case B of
			 {P} => (pick (n1, rest, B_add (acc, i, P), nrem1);
				 pick (n, rest, acc, nrem1))
		       | _ => 
			 iterate
			   (pick (n1, rest', B_add (acc, i, P), nrem1);
			    pick (n, rest', acc, nrem1))
			 | P in set B
			 val B' = B \ {P}
			 val rest' = rest ++ {i => B'}
			 end
		 end
    in
	fn n => pick (n, Bs, {}, nBs)
    end;
*)

(*
fun iter_sub_revblkl f =
    let fun iter ({} :: rest) = (* optimization *)
	    let val iter' = iter rest
	    in
		fn blkl_acc =>
		   iter' ({} :: blkl_acc)
	    end
	  | iter (B :: rest) =
	    let val iter' = iter rest
	    in
		fn blkl_acc =>
		   iterate
		     iter' (B' :: blkl_acc)
		   | B' sub map B
		   end
	    end
	  | iter _ = f
    in
	fn blkl => iter blkl nil
    end;
*)

fun t_get_table t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = table ()
	      in
		  t_put t (x, t');
		  t'
	      end);

fun t_get_mapr t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = ref {}
	      in
		  t_put t (x, t');
		  t'
	      end);

(*
fun t_get_mapr_n t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = ref ({}, 0)
	      in
		  t_put t (x, t');
		  t'
	      end);
*)

fun t_get_blocksr t x =
    (case t_get t x of
	 SOME t' => t'
       | _ => let val t' = ref BS_ZERO
	      in
		  t_put t (x, t');
		  t'
	      end);

exception ResolveSelxEvt;
exception ResolveAutoEvt;
exception ResolventSubsumesPremiseEvt;
exception CtSubsumedEvt;
exception ElimClauseFromSelq;
exception DecPdef;
exception BsPut;
exception ResolveAuto;

exception CheckPdef of |[ predicate : string,
			  refcount : int,
			  shouldbe : int
			  ]|;

exception AlFirst1Evt;

fun al_first_1 (nil, ...) = raise AlFirst1Evt
  | al_first_1 (_, 0, acc) = rev acc
  | al_first_1 (a::al, n, acc) =
    al_first_1 (al, n-1, a::acc);

fun al_first (al, n) =
    (al_first_1 (al, n, nil)
     handle AlFirst1Evt => al);

(*
exception NthBug;
*)

exception DeepPathSet;
exception SortSimplifyBBug;

(*
fun g_merge ({}, gaif) = ({}, {}, gaif)
  | g_merge (vars : int set, gaif : (int set * atom set) list) =
    let fun gmerge ((g as (xs, al))::rest, vars', als, gaif') =
	    if xs intersects vars
		then gmerge (rest, vars' U xs, al U als, gaif')
	    else gmerge (rest, vars', als, g::gaif')
	  | gmerge (_, vars', als, gaif') = (vars', als, gaif')
    in
	gmerge (gaif, {}, {}, nil)
    end;

fun g_sort (al : atom list, gaif : (int set * atom set) list) =
    case al of
	(a as (_, t)) :: rest =>
	let val vars = tvars t
	    val (vars', al', gaif') = g_merge (vars, gaif)
	in
	    g_sort (rest, (vars U vars', al' U {a})::gaif')
	end
      | _ => gaif;

exception DeepSplitEvt;

fun deep_split () =
    let memofun newP _ = gensym "#deep-split"
	memofun ds (CL (h, {}, al as [_, ...], Bs)) =
		let val hvars = head_vars h
		    val gaif = g_sort (al, nil)
		    val (vars', al', gaif') = g_merge (hvars, gaif)
		in
		    case gaif' of
			nil => raise DeepSplitEvt
		      | _ => let val splits = [let val sigma = case xs of
								   {x} => {x => V 1}
								 | _ => let val ir = ref 0
									in
									    {x => V (inc ir; !ir)
									    | x in set xs}
									end
						   val tsub = tsubst sigma
						   val newal = atom_sort {(P, tsub t)
									 | (P, t) in set al}
						   val newBs = {y => B
							       | x => B in map sigma <| Bs
								   val V y = ?sigma x}
						   val Q = newP (newal, newBs)
						   val h' = case xs of
								{x} => HVAR Q
							      | _ =>
								let val f = Q ^ "_fun"
								    val k = card xs
								    val vars = 1 to k
								    val ir = ref 0
								    val t = f $ [V (inc ir; !ir)
										|while !ir<k]
								in
								    HFUN (Q, f, k, vars, t)
								end
					       in
						   (Q, CL (h', {}, newal, newBs))
					       end
					      | (xs, al) in list gaif'
						   such that not (empty xs)]
			     in
				 (CL (h, {{Q} | (Q, _) in list splits},
				      atom_sort (al' U {al
						       | ({}, {al}) (* in (xs,al) in gaif',
								     if xs is empty then
								     al is always a one-element
								     set. *)
							 in list gaif'}),
				      (hvars U vars') <| Bs),
				  splits)
			     end
		end
	      | ds _ = raise DeepSplitEvt
    in
	ds
    end;
*)

local
    val nfa = re_make_nfa [(re_parse "^#q", fn _ => ())]
in
    fun da_matches P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

val default_term = "*" $ nil;

val hash_n = 0; (*100;*)

fun resolver (do_bot : clause -> unit, maxpathlen, maxneglit,
	      auto_guide, onlyuseful, mknondet, deepabbrvp, sortsimplp,
	      wantproof, wanttrace) =
    let val (p_reset,
	     p_ne, p_split_def, p_split_use, p_split_split,
	     p_nondet_split_def, p_nondet_split_use,
	     p_abbrv_def, p_abbrv_use,
	     p_q_resolve, p_auto_resolve, p_eps_resolve, p_unit_resolve,
	     p_rename_resolve,
	     p_sort_simplify,
	     p_definition, p_cond_q_resolve,
	     p_pick, p_forw_subsume, p_back_subsume,
	     p_vdash, p_fully_defined, p_msg,
	     p_useless,
	     p_flush) =
	    case wantproof of
		SOME (f as |[put, flush, ...]|) =>
		let memofun ivname i =
			    let val f as |[convert, ...]| = outstring "X"
			    in
				print f (pack (i:int));
				convert ()
			    end
		    val c_numbers : (clause, int) table = table ()
		    val cn_put = t_put c_numbers
		    val cn_get = t_get c_numbers
		    val cn_remove = t_remove c_numbers
		    val c_invnums : clause option array = array (hash_n, NONE)
		    val c_ir = ref 0
		    fun p_reset () =
			(t_iter c_numbers (fn (c, k) =>
					      (c_invnums.(k).:=NONE;
					       false));
			 t_reset c_numbers;
			 c_ir := 0)
		    fun p_define c =
			let val j = irand hash_n
		    (*val i = (inc c_ir; !c_ir)
		     val j = if i=hash_n then (c_ir:=0; 0) else i
		     *)
			in
			    (case c_invnums.(j) of
				 SOME c' => cn_remove c'
			       | _ => ());
			    cn_put (c, j);
			    c_invnums.(j).:=SOME c;
			    j
			end
		    val pclause = print_clause (f, "X")
		    fun p_new_clause c =
			(
			 if hash_n=0
			     then ()
			 else let val j = p_define c
			      in
				  print f (pack j);
				  put ":"
			      end;
			      pclause c
			      )
		    fun p_use_clause c =
			case cn_get c of
			    SOME j => (print f (pack j); put ";")
			  | _ => pclause c
		    val pq = print_q f
		    val pt = print_term (f, fn () => "")
		    val pit = print_term (f, ivname)
		    fun pa (P, t) = (put P; put " "; pit t; put ".")
		    fun p_ne (q, c, ut) =
			(pq q; put ". [unit-resolve:\n  ";
			 p_use_clause c;
			 if noshow_term (1, ut)
			     then ()
			 else (put " {X1="; pit ut; put "}");
			     put "\n";
			 iterate
			   (put "  "; put P; put " ";
			    pit ut; put ".\n")
			 | P in set q
			 end;
			 put "  ]\n")
		    fun p_nondet_split_def splitdef =
			(p_new_clause splitdef;
			 put " [inter-def]\n")
		    fun p_nondet_split_use (conc, c) =
			(p_new_clause conc;
			 put " [inter-use:\n  ";
			 p_use_clause c;
			 put "\n  ]\n")
		    fun p_split_def splitdef =
			(p_new_clause splitdef;
			 put " [split-def]\n")
		    fun p_split_use (conc, c, splitBs) =
			(p_new_clause conc;
			 put " [split-use:\n  ";
			 p_use_clause c;
			 put "\n  ]\n")
		    fun p_split_split (q, c) =
			(pq q; put ". [split-split:\n  ";
			 p_use_clause c;
			 put "\n  ]\n")
		    fun p_abbrv_def def = 
			(p_new_clause def;
			 put " [abbrv-def]\n")
		    fun p_abbrv_use (conc, c) =
			(p_new_clause conc;
			 put " [abbrv-use:\n  ";
			 p_use_clause c;
			 put "\n  ]\n")
		    fun p_q_resolve (conc, c, q) =
			(p_new_clause conc;
			 put " [q-resolve:\n  ";
			 p_use_clause c;
			 put "\n  "; pq q; put ".\n  ]\n")
		    fun p_auto (AC_UNIV P) =
			(put P; put " X1.")
		      | p_auto (AC_Q q) =
			(pq q; put ".")
		      | p_auto (AC_POP (P, f, blkl)) =
			let val k = len blkl
			    val vars = 1 to k
			    val ir = ref 0
			    val t = f $ [V (inc ir; !ir)
					|while !ir<k]
			in
			    p_use_clause (CL (HFUN (P, f, k, vars, t), {}, nil,
					      Bs_from_blkl blkl))
			end
		      | p_auto (AC_POP_RAW c) = p_use_clause c
		    fun p_mgu (MGU_AUTO_X1_IS t) =
			if noshow_term (1, t)
			    then ()
			else (put "{X1="; pit t; put "}")
		      | p_mgu (MGU_AUTO_Xs_ARE tl) =
			if let val ir = ref 0
			   in
			       all (inc ir; noshow_term (!ir, t))
			       | t in list tl
			       end
			   end
			    then ()
			else let val ir = ref 0
				 val delimr = ref "{X";
			     in
				 iterate
				   (inc ir;
				    if noshow_term (!ir, t)
					then ()
				    else (put (!delimr); delimr := ",X";
					  print f (pack (!ir));
					  put "=";
					  pit t)
					)
				 | t in list tl
				 end;
				 put "}"
			     end
		    fun p_auto_resolve (conc, c, pi_l) =
			if null pi_l andalso conc<>c
			    then raise ResolveAuto
			else
			    (p_new_clause conc;
			     put " [auto-resolve:\n  ";
			     p_use_clause c; put "\n";
			     iterate
			       (put "  "; p_auto ac; p_mgu mgu; put "\n")
			     | (ac, mgu) in list pi_l
			     end;
			     put "  ]\n")
		    fun p_eps_resolve (conc, c, ac, it) =
			(p_new_clause conc;
			 put " [eps-resolve:\n  ";
			 p_use_clause c;
			 if noshow_term (1, it)
			     then ()
			 else (put " {X1="; pit it; put "}");
			     put "\n  "; p_auto ac; put "\n  ]\n")
		    fun p_unit_resolve (conc, c, sigma, premises) =
			(pa conc;
			 put " [unit-resolve:\n  ";
			 p_auto c; put " "; p_mgu sigma;
			 iterate
			   (put "\n  ";
			    pa prem)
			 | prem in list premises
			 end;
			 put "\n  ]\n")
		    fun p_rename_resolve (conc, c, sigma) =
			(p_new_clause conc;
			 put " [rename-resolve:\n  ";
			 p_use_clause c; put " ";
			 let val delimr = ref " {X"
			 in
			     iterate
			       (put (!delimr); delimr := ",X";
				print f (pack i);
				put "=X";
				print f (pack j))
			     | i => j in map sigma
			     end
			 end;
			 put "}\n  ]\n")
		    fun p_sort_simplify (conc, c, wits) =
			(p_new_clause conc;
			 put " [sort-simplify:\n  ";
			 p_use_clause c; put "\n";
			 iterate
			   (put "  "; p_use_clause sc; put " ";
			    p_mgu sigma; put "\n")
			 | (sc, sigma) in set wits
			 end;
			 put "  ]\n")
		    fun p_pick c =
			do_verbose (1, fn () =>
				    (put "% Picking: "; pclause c; put "\n"))
		    fun p_forw_subsume c =
			do_verbose (1, fn () =>
				    (put "% Subsumed [forward]: "; pclause c; put "\n"))
		    fun p_back_subsume c =
			do_verbose (1, fn () =>
				    (put "% Subsumed [backward]: "; pclause c;
				     put "\n"))
		    fun p_vdash c =
			do_verbose (1, fn () =>
				    (put "% |- "; pclause c; put "\n"))
		    fun p_fully_defined P =
			do_verbose (1, fn () =>
				    (put "% "; put P; put " is now fully defined.\n"))
		    fun p_msg msg =
			(put "% "; put msg; put "\n"; flush ())
		    fun p_definition cdef =
			(p_new_clause cdef;
			 put " [definition]\n")
		    fun p_cond_q_resolve (conc, c, sides) =
			(p_new_clause conc;
			 put " [def-resolve:\n  ";
			 p_use_clause c; put "\n";
			 iterate
			   (put "  "; p_use_clause sc; put "\n")
			 | sc in list sides
			 end;
			 put "  ]\n")
		    fun p_useless c =
			do_verbose (1, fn () =>
				    (put "% Ignoring useless clause ";
				     pclause c;
				     put "\n"))
		in
		    (p_reset,
		     p_ne, p_split_def, p_split_use, p_split_split,
		     p_nondet_split_def, p_nondet_split_use,
		     p_abbrv_def, p_abbrv_use,
		     p_q_resolve, p_auto_resolve, p_eps_resolve, p_unit_resolve,
		     p_rename_resolve,
		     p_sort_simplify,
		     p_definition, p_cond_q_resolve,
		     p_pick, p_forw_subsume, p_back_subsume,
		     p_vdash, p_fully_defined, p_msg,
		     p_useless,
		     flush)
		end
	      | _ => (fn _ => (),
			 fn _ => (), fn _ => (), fn _ => (), fn _ => (),
			    fn _ => (), fn _ => (),
			       fn _ => (), fn _ => (),
				  fn _ => (), fn _ => (), fn _ => (), fn _ => (),
				     fn _ => (),
					fn _ => (),
					   fn _ => (), fn _ => (),
					      fn _ => (), fn _ => (), fn _ => (),
						 fn _ => (), fn _ => (), fn _ => (),
						    fn _ => (),
						       fn _ => ())

	val (prog_vdash, prog_pick, prog_new_fact,
	     prog_rec_bot, prog_rec_auto, prog_rec_univ, prog_rec_ne, prog_rec_split_def,
	     prog_rec_nondet_split_def,
	     prog_rec_cond, prog_fully_defined,
	     prog_abbrv,
	     prog_sort_simplify,
	     prog_rem_pruned, prog_rem_fully_defined_parent, prog_rem_fully_defined_backward,
	     prog_rem_subsumed_premise, prog_rem_subsumed_forward, prog_rem_subsumed_forward_auto,
	     prog_rem_subsumed_backward, prog_rem_subsumed_backward_auto, prog_rem_cond,
	     prog_flush) =
	    case wanttrace of
		SOME |[put, flush, ...]| =>
		(fn () => (put ">"),
		    fn () => (put "<"),
		       fn () => (put "f"),
			  fn () => (put "!"),
			     fn () => (put "+"),
				fn () => (put "*"),
				   fn () => (put "q"),
				      fn () => (put "s"),
					 fn () => (put "S"),
					    fn () => (put "c"),
					       fn () => (put "d"),
						  fn () => (put "a"),
						     fn () => (put "k"),
							fn () => (put "/"),
							   fn () => (put "^"),
							      fn () => (put "D"),
								 fn () => (put "\\"),
								    fn () => (put "-"),
								       fn () => (put "_"),
									  fn () => (put "b"),
									     fn () => (put "B"),
										fn () => (put "C"),
										   flush
										   )
	      | _ => (fn () => (), fn () => (), fn () => (),
			 fn () => (), fn () => (), fn () => (), fn () => (), fn () => (),
			    fn () => (),
			       fn () => (), fn () => (),
				  fn () => (),
				     fn () => (),
					fn () => (), fn () => (), fn () => (), fn () => (),
					   fn () => (), fn () => (), fn () => (), fn () => (),
					      fn () => (), fn () => ())

	val wantproofp = case wantproof of
			     SOME _ => true
			   | _ => false
	val wanttracep = case wanttrace of
			     SOME _ => true
			   | _ => false

	fun say_rem_fully_defined_parent () =
	    (prog_rem_fully_defined_parent ();
	     do_verbose (2, fn () =>
			 p_msg "Remove parent clause, which was resolved on fully defined predicates."))
	fun say_rem_subsumed_premise () =
	    (prog_rem_subsumed_premise ();
	     do_verbose (2, fn () =>
			 p_msg "Remove parent clause, which is subsumed by conclusion."))
	fun say_rem_fully_defined_parent_implicit () =
	    (prog_rem_fully_defined_parent ();
	     do_verbose (2, fn () =>
			 p_msg "Remove parent clause, which was resolved on predicates just realized to be fully defined."))

	fun flush_all () =
	    (do_verbose (1, #flush stderr);
	     p_flush ();
	     prog_flush ())

	val predicate_graph = ref ({} : predicate digraph)
	val clause_list = ref (nil : clause list)
	val skeleta = ref ({} : string -m> pathset)
	val skel_bots = ref ({} : string set)
	val sure_facts = ref ({} : string -m> int term -m> int)

	val ag_intersects_blk =
	    case auto_guide of
		SOME a => auto_intersects a
	      | _ => (fn _ => true)

	val ag_match_term =
	    case auto_guide of
		SOME a => auto_simple_match_term a
	      | _ => (fn _ => true)

	(*
	val ag_intersects =
	    case auto_guide of
		SOME a => (fn Bs =>
			      all
				ag_intersects_blk blk
			      | _ => blk in map Bs
			      end)
	      | _ => (fn _ => true)
	 *)

	memofun psinter x = ps_inter x

	val q_skel_rem = ref ({} : block -m> pathset)

	fun q_skeleta {} = PS_ALL
	  | q_skeleta {P} = if P inset !skeleta then ?(!skeleta) P else ps_empty
	  | q_skeleta blk =
	    if blk inset !q_skel_rem
		then ?(!q_skel_rem) blk
	    else let val (blk1, blk2) = split blk
		     val ps = psinter (q_skeleta blk1, q_skeleta blk2)
		 in
		     q_skel_rem := !q_skel_rem ++ {blk => ps};
		     ps
		 end

		 (* Old version [also memorized the {} and {P} cases]
	memofun q_skeleta {} = PS_ALL
	      | q_skeleta {P} = if P inset !skeleta then ?(!skeleta) P else ps_empty
	      | q_skeleta blk = let val (blk1, blk2) = split blk
				in
				    psinter (q_skeleta blk1, q_skeleta blk2)
				end
		  *)

	fun ps_check_empty (PS_ENUM {}) = raise NoPathSetEvt
	  | ps_check_empty env = env

	fun ps_env_inter (psenv, psenv') =
	    (psenv delta psenv') ++ {i => ps_check_empty (psinter (ps, ps'))
				    | i => ps in map psenv' <| psenv
					val ps' = ?psenv' i}

	fun ps_match_term (V x, ps, env) =
	    if x inset env
		then let val ps' = psinter (ps, ?env x)
		     in
			 env ++ {x => ps_check_empty ps'}
		     end
	    else env ++ {x => ps}
	  | ps_match_term (_, PS_ALL, env) = env
	  | ps_match_term (f $ nil, PS_ENUM fimap, env) =
	    if (f, 0) inset fimap
		then env
	    else raise NoPathSetEvt
	  | ps_match_term (f $ l, PS_ENUM fimap, env) =
	    ps_match_term_list (f, l, 1, fimap, env)
	and ps_match_term_list (_, nil, _, _, env) = env
	  | ps_match_term_list (f, ti::l, i, fimap, env) =
	    let val fi = (f, i)
	    in
		if fi inset fimap
		    then let val env' = ps_match_term (ti, ?fimap fi, env)
			 in
			     ps_match_term_list (f, l, i+1, fimap, env')
			 end
		else raise NoPathSetEvt
	    end

	fun ps_match_a (a as (P, t), env) =
	    if P inset !skeleta
		then let val psenv = ps_match_term (t,
						    ps_check_empty (?(!skeleta) P),
						    env)
		     in
			 if ag_match_term a
			     then psenv
			 else (prog_rem_pruned ();
			       raise NoPathSetEvt)
		     end
	    else raise NoPathSetEvt

	fun ps_match_al (a::al, env) =
	    ps_match_al (al, ps_match_a (a, env))
	  | ps_match_al (_, env) = env;

	fun ps_match_as ({a} U ats, env) =
	    ps_match_as (ats, ps_match_a (a, env))
	  | ps_match_as (_, env) = env;

	fun ps_match_Bs ({i => B} U rest, env) =
	    ps_match_Bs (rest,
			 let val env' =
				 if i inset env
				     then env ++ {i => ps_check_empty (psinter (?env i,
										q_skeleta B))}
				 else env ++ {i => ps_check_empty (q_skeleta B)}
			 in
			     if ag_intersects_blk B
				 then ()
			     else (prog_rem_pruned ();
				   raise NoPathSetEvt);
			     env'
			 end)
	  | ps_match_Bs (_, env) = env

	val partially_defined : (string, int ref) table = table ()
	    (* maps every predicate symbol P to the number of clauses
	     everywhere except in autoinfoq and univq (in waitq, in selxq,
	     selfq), with head P(...).
	     *)
	val pdef_get = t_get partially_defined
	val pdef_put = t_put partially_defined
	val pdef_rem = t_remove partially_defined

	val new_fully_defined = ref ({} : string set)
	val new_fully_defined_ok = ref ({} : string set)

	fun fully_defined P =
	    case pdef_get P of
		SOME (ref n) => n=0
	      | _ => true

	fun fully_defineds B =
	    {P
	    | P in set B
	      such that fully_defined P}

	fun inc_pdef P =
	    ( (*p_msg (P ^ "++");*)
	     case pdef_get P of
		 SOME ir => inc ir
	       | _ => pdef_put (P, ref 1))

	fun h_new_def (HFUN (P, ...)) =
	    inc_pdef P
	  | h_new_def (HVAR P) =
	    inc_pdef P
	  | h_new_def _ = ()

	fun new_def (CL (h, ...)) = h_new_def h

	fun dec_pdef P =
	    ( (*p_msg (P ^ "--");*)
	     case pdef_get P of
		 SOME ir => if !ir<=0
				then raise DecPdef
			    else (dec ir;
				  if !ir=0
				      then (pdef_rem P;
					    prog_fully_defined ();
					    p_fully_defined P;
					    new_fully_defined := !new_fully_defined U {P}
					    )
				  else ())
	       | _ => raise DecPdef)

	fun h_rem_def (HFUN (P, ...)) = dec_pdef P
	  | h_rem_def (HVAR P) = dec_pdef P
	  | h_rem_def _ = ()

	fun rem_def (c as CL (h, ...)) =
	    (h_rem_def h)

	fun add_graph (pred, CL (_, ql, al, Bs, ...)) =
	    predicate_graph := !predicate_graph Urel {pred => union {{P_PRED P
								     | P in set blk}
								    | blk in set ql}
						      U {P_PRED P
							| (P, _) in list al}
						      U union {{P_PRED P
							       | P in set blk}
							      | _ => blk in map Bs}}
	fun new_clause (c as CL (HBOT botname, ...)) =
	    (predicate_graph := !predicate_graph Urel {P_ROOT => {P_BOT botname}};
	     add_graph (P_BOT botname, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HVAR P, ...)) =
	    (add_graph (P_PRED P, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HFUN (P, f, ...), ...)) =
	    (add_graph (P_PRED P, c);
	     clause_list := c :: !clause_list)
	  | new_clause (c as CL (HQ blk, ...)) =
	    (iterate
	       add_graph (P_PRED P, c)
	     | P in set blk
	     end;
	       clause_list := c :: !clause_list)

	val fargsq = ref ({} : string -m> int * int set * int term);
	(* map f to (k, {1, ..., k}, f(x1,...,xk)),
	 where k is the arity of f.*)

	val dfs_info = ref ({} : predicate -m> int * int) (* dfsnum, revtopsort number of low *)
	val scc_info = ref ({} : int -m> predicate set) (* map (revtopsort of) low to corresponding scc *)
	val dfs_q_info = ref ({} : block -m> int * int) (* max {(revnum P, low P) | P in blk},
							 where the max is taken in the right-to-left
							 lexicographic ordering. *)
	val useful =
	    if onlyuseful
		then fn (CL (HBOT botname, ...)) => P_BOT botname inset !dfs_info
		      | (CL (HVAR P, ...)) => P_PRED P inset !dfs_info
		      | (CL (HFUN (P, ...), ...)) => P_PRED P inset !dfs_info
		      | (CL (HQ blk, ...)) =>
			all
			  P_PRED P inset !dfs_info
			| P in set blk
			end
	    else fn _ => true

	fun info_less ((revnum, low), (revnum', low')) =
	    low<low' orelse low=low' andalso revnum<revnum'
	fun info_max (dlow, dlow') =
	    if info_less (dlow, dlow')
		then dlow'
	    else dlow
	fun infos_max {} = raise InfosMax
	  | infos_max {dlow} = dlow
	  | infos_max dlows = let val (dlows1, dlows2) = split dlows
			      in
				  info_max (infos_max dlows1, infos_max dlows2)
			      end
	fun p_info P = ?(!dfs_info) P
	fun h_info (HBOT botname) = p_info (P_BOT botname)
	  | h_info (HVAR P) = p_info (P_PRED P)
	  | h_info (HFUN (P, ...)) = p_info (P_PRED P)
	  | h_info (HQ blk) =
	    let val dfs_q = !dfs_q_info
	    in
		if blk inset dfs_q
		    then ?dfs_q blk
		else let val info = !dfs_info
			 val m = infos_max {p_info (P_PRED P)
					   | P in set blk}
		     in
			 dfs_q_info := dfs_q ++ {blk => m};
			 m
		     end
	    end
	fun head_info (CL (h, ...)) = h_info h

	val selqq : (block, (head * atom list, (block set * (int -m> block)) set ref) table) table
	    = table ()
		     (* for each clause C \/ -q with -q selected,
		      maps q to the set of such C's. *)

	val selqq_get = t_get selqq
	val selqq_put = t_put selqq
	val selqq_rem = t_remove selqq

	val selfq : (string,
		     (string,
		      (head * atom list, (int -m> block) set ref) table)
		     table) table
	    = table ()
	val selfq_get = t_get selfq
	val selfq_get_table = t_get_table selfq
	(*val selfq_put = t_put selfq*)
	val selfq_rem = t_remove selfq
	(* maps P, f to clauses C \/ -P(f(...))
	 where -P(f(...)) is selected. *)

	(* The following check_selfq function is buggy: instead of iterating
	 on al in do_check_selfq, the iteration should also change fmapr and clsr
	 (be two levels higher).  This was precisely the same bug as in
	 bs_put, which check_selfq was meant to discover...
	 *)
	(*
	exception CheckSelfq0 of |[ clause : head * atom list,
				    Bss : (int -m> block) -m> int -m> pathset
				    ]|
	exception CheckSelfq1 of |[ clause : head * atom list,
				    Bss : (int -m> block) -m> int -m> pathset,
				    Bss' : (int -m> block) -m> int -m> pathset
				    ]|
	fun check_selfq () =
	    (t_iter selfq
	     (fn (P, fmapr) =>
		 t_iter fmapr
		 (fn (f, clsr) =>
		     t_iter clsr
		     (fn ((h, al, nil), ref Bss) =>
			 let fun do_check_selfq (nil, ...) = false
			       | do_check_selfq (al1 as (a::rest), acc) =
				 (case t_get clsr (h, al1, acc) of
				      SOME (ref Bss') =>
				      if Bss<>Bss'
					  then raise CheckSelfq1 |[ clause = (h, al),
								    Bss = Bss,
								    Bss' = Bss' ]|
				      else do_check_selfq (rest, a::acc)
				    | _ => raise CheckSelfq0 |[ clause = (h, al),
								Bss = Bss ]|)
			 in
			     do_check_selfq (al, nil)
			 end)));
		 ())
	 *)

	val selxq : (string, (head, block set ref) table) table
	    = table ()
	val selxq_get = t_get selxq
	(*val selxq_put = t_put selxq*)
	val selxq_rem = t_remove selxq
	(* maps P to clauses C \/ -P(x), with -P(x) selected.
	 These clauses must be of the form h :- B(x), with P in B,
	 and we map P and h to the set of B's. *)

	val iselxq : (string, string set ref) table = table ()
	    (* maps P to set of Qs, where we have
	     clauses P(x) :- Q(x).
	     Used in sort_simplify. *)
	val iselxq_get = t_get iselxq

	    (*
	val iiselxq : (string, block set ref) table = table ()
	    (* maps P to set of blocks B, of length at least 2
	     (those of length 1 are stored in iselxq), where we
	     have P(x) :- B(x).
	     Used in sort_simplify. *)
	    *)

	fun insert_selxq (h, B) = (* insert P(x) :- B (x) into selxq and iselxq. *)
	    (do_verbose (1, fn () => p_msg "Insert parent clause into selxq.");
	     iterate
	       let val csr = t_get_table selxq P1
		   val Br = t_get_mapr csr h
	       in
		   Br := !Br U {B}
	       end
	     | P1 in set B
	     end;
	       case h of
		   HVAR P =>
		   (case B of
			{Q} =>
			let val pr = t_get_mapr iselxq P
			in
(*
#put stderr "Adding ";
#put stderr P;
#put stderr " <= ";
#put stderr Q;
#put stderr ".\n";
#flush stderr ();
*)
			    pr := !pr U {Q}
			end
		      | _ => ()
			)
		 | _ => ()
		   )

	val autoinfoq : (string, (string, blocks ref) table) table
	    = table ()
	(* current set of automata clauses, maps P, f, to blocks blkls
	 where blkls is the set of possible bodies, each mapped to a proof of the
	 corresponding pop clause; invariant: n = card blkls;
	 each body is a list of blocks, one for each variable argument (1, ..., k) to f.
	 *)
	val a_get = t_get autoinfoq
	val a_rem = t_remove autoinfoq

	fun sort_check Bs =
	    (* as sort_check_with_witnesses (below), only
	     returns a boolean: true if and only if atom (P,t)
	     in argument is deducible from automaton clauses
	     (in autoinfoq) and simple clauses P(x)<=Q(x) (in iselxq)
	     starting from the atoms Pi(xi) in Bs.
	     *)
	    let memofun sort_check_1 (P, V x) =
			(* sort_check_1 (P, t) checks that t has sort P,
			 i.e., that P(t) is derivable from the P(Xi) in Bs. *)
			x inset Bs andalso P inset ?Bs x
		      | sort_check_1 (P, f $ l) =
			(case a_get P of
			     SOME fmapr =>
			     (case t_get fmapr f of
				  SOME (blksr as ref blks) =>
				  sort_check_l (blks, l)
				| _ => false)
			   | _ => false)
		and sort_check_l (BS_ZERO, _) = false
		  | sort_check_l (BS_ONE, _) = true
		  | sort_check_l (BS_B ((Pj, V j), b1, b2), l) =
		    (sort_check_1 (Pj, l nth (j-1)) andalso
		     sort_check_l (b1, l)) orelse
		    sort_check_l (b2, l)
		with sort_check_selxq (P, t) =
		     let val doner = ref {}
			 fun sort_check_selxq_1 P =
			     if P inset !doner
				 then ?(!doner) P
			     else
				 (doner := !doner ++ {P => false};
				  let val res = 
					  (sort_check_1 (P, t) orelse
					   (case iselxq_get P of
						SOME (ref Qs) =>
						exists
						  sort_check_selxq_1 Q
						| Q in set Qs
						end
					      | _ => false))
				  in
				      doner := !doner ++ {P => res};
				      res
				  end)
		    in
			sort_check_selxq_1 P
		    end
	    in
		sort_check_selxq
		(*
		fn (P, t) => (#put stderr "Sort_check ";
			      #put stderr P;
			      #put stderr " ";
			      print_term (stderr,
					  fn i => let val f as |[convert, ...]|
							  = outstring "X"
						  in
						      print f (pack (i:int));
						      convert ()
						  end) t;
			      #put stderr "... ";
			      #flush stderr ();
			      sort_check_selxq (P, t)
			      before (
				      #put stderr "Done.\n";
				      #flush stderr ()))
		 *)
	    end

	fun sort_check_with_witnesses Bs =
	    (* as sort_check (above), but return set of clauses used. *)
	    let memofun sort_check_with_witnesses_1 (P, V x) =
			if x inset Bs andalso P inset ?Bs x
			    then SOME {}
			else NONE
		      | sort_check_with_witnesses_1 (P, f $ l) =
			(case a_get P of
			     SOME fmapr =>
			     (case t_get fmapr f of
				  SOME (blksr as ref blks) =>
				  (case sort_check_with_witnesses_l (blks, l) of
				       SOME (Bs_auto, wits) =>
				       let val (k, vars, t) = ?(!fargsq) f
				       in
					   SOME (wits U {(CL (HFUN (P, f, k, vars, t),
							      {}, nil, Bs_auto),
							  MGU_AUTO_Xs_ARE l)})
				       end
				     | _ => NONE)
				| _ => NONE)
			   | _ => NONE)
		and sort_check_with_witnesses_l (BS_ZERO, _) = NONE
		  | sort_check_with_witnesses_l (BS_ONE, _) = SOME ({}, {})
		  | sort_check_with_witnesses_l (BS_B ((Pj, V j), b1, b2), l) =
		    let val b1OK =
			    (case sort_check_with_witnesses_1 (Pj, l nth (j-1)) of
				 SOME wits =>
				 (case sort_check_with_witnesses_l (b1, l) of
				      SOME (Bs_auto, wits') =>
				      SOME (B_add (Bs_auto, j, Pj), wits U wits')
				    | _ => NONE)
			       | _ => NONE
				 )
		    in
			case b1OK of
			    SOME _ => b1OK
			  | _ => sort_check_with_witnesses_l (b2, l)
		    end
		with sort_check_with_witnesses_selxq (P, t) =
		     let val doner = ref {}
			 fun sort_check_with_witnesses_selxq_1 P =
			     if P inset !doner
				 then ?(!doner) P
			     else (doner := !doner ++ {P => NONE};
				   (case sort_check_with_witnesses_1 (P, t) of
					SOME wits => SOME wits
				      | _ =>
					(case iselxq_get P of
					     SOME (ref Qs) =>
					     let val res =
						     some
						       wits U {(CL (HVAR P, {},
								    nil,
								    {1 => {Q}}),
								MGU_AUTO_X1_IS t)}
						     | Q in set Qs
						     val SOME wits =
							 sort_check_with_witnesses_selxq_1 Q
						     end
					     in
						 doner := !doner ++ {P => res};
						 res
					     end
					   | _ => NONE)
					))
		     in
			 sort_check_with_witnesses_selxq_1 P
		     end
	    in
		sort_check_with_witnesses_selxq
	    end

	fun sort_simplify (al, Bs) =
	    (* as sort_simplify_with_witnesses (below), only returns simplified al. *)
	    let val sort_check_1 = sort_check Bs
	    in
		[a
		| a in list al
		  such that not (sort_check_1 a)]
	    end

	fun sort_simplify_with_witnesses (al, Bs) =
	    (* as sort_simplify (above), only returns sets of clauses used
	     in simplifying out atoms that sort_simplify removes. *)
	    let val sort_check_with_witnesses_1 = sort_check_with_witnesses Bs
	    in
		union {wits
		      | a in list al
			  val SOME wits = sort_check_with_witnesses_1 a
			      }
	    end;

	fun sort_simplify_B (B : block) =
	    (* as sort_simplify_B_with_witnesses (below), only
	     returns simplified block.  Simplification is just
	     applying the rule:
	     B U {P, Q} --> B U {Q}
	     if there is a sequence of clauses
	     P(x)<=P1(x), P1(x)<=P2(x), ..., Pn(x)<=Q(x)
	     in iselxq.
	     *)
	    let val doner = ref {}
		val survived = ref {}
		val notseenyet = ref B
		fun ssB_1 P =
		    if P inset !doner
			then ?(!doner) P
		    else
			(doner := !doner ++ {P => false};
			 let val res =
				 P inset !survived orelse
				 P inset !notseenyet orelse
				 (case iselxq_get P of
				      SOME (ref Qs) =>
				      exists
					ssB_1 Q
				      | Q in set Qs
				      end
				    | _ => false)
			 in
			     doner := !doner ++ {P => res};
			     res
			 end)
	    in
		while not (empty (!notseenyet)) do
		    let val {P} U rest = !notseenyet
		    in
			notseenyet := rest;
			doner := {};
			if ssB_1 P
			    then ()
			else survived := !survived U {P}
		    end;
		    !survived
	    end

	fun sort_simplify_B_with_witnesses (B : block, B1) =
	    (* Given that sort_simplify_B B returned B1 (subset of B),
	     return set of clauses P(x)<=Q(x) used.
	     This is just a collection of reachability tests.
	     *)
	    let val doner = ref {}
		memofun ssB_path P =
			if P inset B1
			    then SOME {}
			else if P inset !doner
			    then ?(!doner) P (* cycle detected *)
			else (doner := !doner ++ {P => NONE};
			      (case iselxq_get P of
				   SOME (ref Qs) =>
				   let val res =
					   some
					     path U {CL (HVAR P, {},
							 nil, {1 => {Q}})}
					   | Q in set Qs
					   val SOME path = ssB_path Q
					   end
				   in
				       doner := !doner ++ {P => res};
				       res
				   end
				 | _ => NONE))
	    in
		union {(case ssB_path P of
			    SOME path => path
			  | _ => raise SortSimplifyBBug)
		      | P in set B \ B1}
	    end

	fun sort_simplify_Bs Bs =
	    {i => sort_simplify_B B
	    | i => B in map Bs}

	fun sort_simplify_Bs_with_witnesses (Bs, Bs1) =
	    union {sort_simplify_B_with_witnesses (B, B1)
		  | i => B in map Bs
		      val B1 = if i inset Bs1
				   then ?Bs1 i
			       else {}}

	     (* remove clause from tables selqq, selxq, selfq, autoinfoq. *)
	fun bs_put (c as CL (h, {q} U rest, al, Bs)) =
	    (case selqq_get q of
		 SOME clr =>
		 (case t_get clr (h, al) of
		      SOME Bsr =>
		      (Bsr := {(rest, Bs)} <-| !Bsr;
		       prog_rem_subsumed_backward ();
		       p_back_subsume c;
		       h_rem_def h)
		    | _ => ())
	       | _ => ())
	  | bs_put (c as CL (h, _, al as (P, f $ _) :: rest, Bs)) =
	    let val entry = (h, al)
	    in
		(case selfq_get P of
		     SOME fmapr =>
		     (case t_get fmapr f of
			  SOME clsr =>
			  (case t_get clsr entry of
			       SOME Bsr =>
			       if Bs inset !Bsr
				   then (Bsr := {Bs} <-| !Bsr;
					 iterate
					   (case selfq_get Q of
						SOME fmapr' =>
						(case t_get fmapr' g of
						     SOME clsr' =>
						     (case t_get clsr' entry of
							  SOME Bsr' => Bsr' := {Bs} <-| !Bsr'
							| _ => ())
						   | _ => ())
					      | _ => ())
					 | (Q, g $ _) in list rest
					 end;
					 prog_rem_subsumed_backward ();
					 p_back_subsume c;
					 rem_def c)
			       else ()
			     | _ => ())
			| _ => ())
		   | _ => ())
	    end
	  | bs_put (c as CL (HFUN (P, f, k, ...), _, _, Bs, ...)) =
	    (case a_get P of
		 SOME fmapr =>
		 (case t_get fmapr f of
		      SOME (blksr as ref blks) =>
		      let val blks' = bs_rem (Bs, blks)
		      in
			  if blks=blks'
			      then ()
			  else (blksr := blks';
				prog_rem_subsumed_backward_auto ();
				p_back_subsume c)
		      end
		    | _ => ())
	       | _ => ())
	  | bs_put (c as CL (HVAR _, ...)) = ()
	  | bs_put (c as CL (h, _, _, Bs, ...)) =
	    (case Bs of
		 {} => ()
	       | {1 => B} =>
		 (case selxq_get (choose B) of
		      SOME cls =>
		      (case t_get cls h of
			   SOME _ =>
			   (iterate
			      (case selxq_get P of
				   SOME cls =>
				   (case t_get cls h of
					SOME Br => Br := {B} <-| !Br
				      | _ => ())
				 | _ => ())
			    | P in set B
			    end;
			      prog_rem_subsumed_backward ();
			      p_back_subsume c;
			      rem_def c)
			 | _ => ())
		    | _ => ())
	       | _ => raise BsPut)

	fun b_set c = bs_put c

	fun auto_back_subsume (CL (h as HFUN (P, f, ...), {}, nil, Bs)) =
	    (case a_get P of
		 SOME fmap =>
		 (case t_get fmap f of
		      SOME (blksr as ref blks) =>
		      (if wantproofp
			   then let val subs_blkls = bs_subsumes (Bs, blks)
				in
				    (*
				    (case wantproof of
					 SOME (f as |[put, ...]|) =>
					 do_verbose (2, fn () =>
						     (put "% Auto clause = ";
						      print_clause (f, "X") (CL (h, {}, nil, Bs));
						      put "\n"))
				       | _ => ());
				     *)
				    iterate
				      (prog_rem_subsumed_backward_auto ();
				       p_back_subsume (CL (h, {}, nil, Bs')))
				    | Bs' in set subs_blkls
				    end
				end
		       else if wanttracep
			   then let val nr = ref (bs_count_subsumes (Bs, blks))
				in
				    while (!nr>0) do
					(prog_rem_subsumed_backward_auto ();
					 dec nr)
				end
		       else ();
			   blksr := bs_elim_subsumes (Bs, blks))
		    | _ => ())
	       | _ => ())
	  | auto_back_subsume _ = ()

        val b_set_auto = b_set
	fun compile_auto_back _ = ()

	(*
	val eps_back : (head, (int -m> block) ref
			* (int -m> block, clause list ref) table) table
	    = table ()
	val eps_back_get = t_get eps_back
	val eps_back_put = t_put eps_back

	fun eps_back_head (HFUN _) = true
	  | eps_back_head (HVAR _) = true
	  | eps_back_head _ = false
	    (* used to backward subsume clauses. *)
	fun eps_back_subsume (CL (h, {}, nil, Bs, ...) (*, do_check*)) =
	    if eps_back_head h
		then case eps_back_get h of
			 SOME (ref dBs, bbr) =>
			 let val bbget = t_get bbr
			     val bbrem = t_remove bbr
			     fun bb_set Bs' =
				 (case bbget Bs' of
				      SOME (ref cl) =>
				      (iterate
					 (b_set c (*;
					  p_msg "Check after b_set."; 
					  do_check () *))
				       | c in list cl
				       end;
					 bbrem Bs';
					 iterate
					   iterate
					     bb_set (if i inset Bs'
							 then Bs' ++ {i => ?Bs' i U {P}}
						     else Bs' ++ {i => {P}})
					   | P in set B
					   end
					 | i => B in map diff_rel (dBs, Bs')
					 end)
				    | _ => ())
			 in
			     bb_set Bs
			 end
		       | _ => ()
	    else ()
	  | eps_back_subsume _ = ()
	fun compile_eps_back (c as CL (h, ql, al, Bs, ...)) =
	    if eps_back_head h andalso empty ql
		then let val (dBsr, bbr) =
			     case eps_back_get h of
				 SOME x => x
			       | _ => let val newr = (ref {}, table ())
				      in
					  eps_back_put (h, newr);
					  newr
				      end
			 val cl = [c]
			 val bbget = t_get bbr
			 val bbput = t_put bbr
		     in
			 if empty ql andalso null al
			     then
				 iterate
				   iterate
				     (case bbget Bs' of
					  SOME clr => clr := c :: !clr
					| _ => bbput (Bs', ref cl))
				   | P in set B
				   val B' = B \ {P}
				   val Bs' = if empty B'
						 then {i} <-| Bs
					     else Bs ++ {i => B'}
				   end
				 | i => B in map Bs
				 end
			 else (case bbget Bs of
				   SOME clr => clr := c :: !clr
				 | _ => bbput (Bs, ref cl));
			     dBsr := !dBsr Urel Bs;
			     iter_sub_Bs (fn Bs' =>
					     (case bbget Bs' of
						  SOME _ => ()
						| _ => bbput (Bs', ref nil))
						  ) Bs
		     end
	    else ()
	  | compile_eps_back _ = ()
	    *)

	fun insert_selqq (q, h, restql, al, Bs) =
	    let val clr = t_get_table selqq q
		val Bsr = t_get_mapr clr (h, al)
		val entry = (restql, Bs)
	    in
		if entry inset !Bsr
		    then false
		else (prog_rec_cond ();
		      Bsr := !Bsr U {entry};
		      true)
	    end

	val waitq as |[ insert = wait_insert_basic,
			popmin = wait_pop_basic,
			dump_list = get_clauses,
			iter = wait_iter,
			... ]|
	    = mheap (fn (n, n') => n<n')

	(* list of unprocessed clauses; may even be automaton clauses,
	 we do not know yet. *)

	val fast_waitq = ref nil

	fun wait_insert_fast (_, c) = ( (* do not use this function directly;
					 always call through do_fast (fn () => wait_insert c). *)
				       fast_waitq := c :: !fast_waitq)

	val wr = ref wait_insert_basic

	fun do_fast f = let val w = !wr
			in
			    wr := wait_insert_fast;
			    f ();
			    wr := w
			end

	fun wait_pop () =
	    case !fast_waitq of
		c :: rest => (fast_waitq := rest; c)
	      | _ => #2 (wait_pop_basic ())

		(*
	fun check_pdef_1 (pd : (string, int ref) table) =
	    let val pd_get = t_get pd
		val pd_put = t_put pd
		fun inc_t P =
		    (case pd_get P of
			 SOME ir => inc ir
		       | _ => pd_put (P, ref 1))
		fun inc_c (CL (HVAR P, ...)) = inc_t P
		  | inc_c (CL (HFUN (P, ...), ...)) = inc_t P
		  | inc_c _ = ()
	    in
		wait_iter (fn (_, c) => inc_c c);
		iterate
		  inc_c c
		| c in list !fast_waitq
		end;
		let val selfq_clauses =
			t_collect selfq
			(fn (P, fmap) =>
			    t_collect fmap
			    (fn (f, cls) =>
				t_collect cls
				(fn ((h, al1), ref Bss) =>
				    {CL (h, {}, al1, Bs)
				    | Bs in set Bss}
				  | _ => {})))
		in
		    iterate
		      inc_c c
		    | c in set selfq_clauses
		    end
		end;
	        let val selxq_clauses =
			t_collect selxq
			(fn (P, cls) =>
			    t_collect cls
			    (fn (h, ref Bs) =>
				{CL (h, {}, nil, {1 => B})
				| B in set Bs}))
		in
		    iterate
		      inc_c c
		    | c in set selxq_clauses
		    end
		end;
		let val selqq_clauses =
			t_collect selqq
			(fn (q, clr) =>
			    t_collect clr
			    (fn ((h, al), ref qBss) =>
                                {CL (h, {q} U ql, al, Bs)
				| (ql, Bs) in set qBss}))
		in
		    iterate
		      inc_c c
		    | c in set selqq_clauses
		    end
		end;
		t_iter pd
		(fn (P, ref i) =>
		    (case pdef_get P of
			 SOME (ref n) =>
			 if i=n
			     then false
			 else raise CheckPdef |[predicate=P, refcount=n, shouldbe=i]|
		       | _ => raise CheckPdef |[predicate=P, refcount=0, shouldbe=i]|));
		t_iter partially_defined
		(fn (P, ref n) =>
		    (case pd_get P of
			 SOME _ => false
		       | _ => raise CheckPdef |[predicate=P, refcount=n, shouldbe=0]|))
	    end
	fun check_pdef () = check_pdef_1 (table ())
	fun check_pdef_except_P P =
	    let val pd = table ()
	    in
		t_put pd (P, ref 1);
		check_pdef_1 pd
	    end
	fun check_pdef_except_h (HVAR P) =
	    check_pdef_except_P P
	  | check_pdef_except_h (HFUN (P, ...)) =
	    check_pdef_except_P P
	  | check_pdef_except_h _ =
	    check_pdef ()
	fun check_pdef_except_c (CL (h, ...)) =
	    check_pdef_except_h h
          *)

	fun selqq_remove q =
	    (case selqq_get q of
		 SOME clr =>
		 (t_iter clr
		  (fn ((h, al), Bsr) =>
		      (iterate
			 (prog_rem_cond ();
			  rem_def (CL (h, restql, al, Bs)))
		       | (restql, Bs) in set !Bsr
		       end;
			 false));
		  selqq_rem q)
	       | _ => ())

	fun clause_category (CL (HFUN _, {}, nil, ...)) = 0
	  | clause_category (CL (HBOT _, ...)) = 1
	  | clause_category (CL (HQ _, ...)) = 2
	  | clause_category (CL (HVAR _, ...)) = 4
	  | clause_category (CL (HFUN (P, ...), ql, al, Bs, ...)) =
	    if empty ql
		then if da_matches P
			 then 3
		     else 4+al_len (al, Bs_len Bs)
	    else 2

	val univq = ref ({} : automaton_univ_trans)
	(* set of predicates P for which we have a clause +P(x). *)
	val qq = ref ({} : block set);
	(* current set of unit clauses +q. *)

	    (*
	fun P_f_score (P, f) =
	    case a_get P of
		SOME fmap =>
		(case t_get fmap f of
		     SOME blkls => num (let val nr = ref 0
					in
					    t_iter blkls
					    (fn _ => (inc nr; false));
						!nr
					end)
		   | _ => 0.0)
	      | _ => 0.0

	fun al_score (nil, acc) = acc
	  | al_score ((P, f $ _)::al, acc) =
	    if P inset !univq
		then 1000.0
	    else if fully_defined P
		then 2.0 #* P_f_score (P, f)
	    else P_f_score (P, f)

	fun clause_category (CL (HFUN (P, f, ...), {}, nil, ...)) = 0
	  | clause_category (CL (HBOT _, ...)) = 1
	  | clause_category (CL (HQ _, ...)) = 2
	  | clause_category (CL (HVAR _, ...)) = 3
	  | clause_category (CL (h, ql, al, Bs, ...)) =
	    if empty ql
		then al_len (al, Bs_len Bs) + (max_int - int (al_score (al, 0.0)))
	    else 2
	     *)

	fun wait_insert_0 c =
	    (prog_vdash (); p_vdash c;
	     compile_auto_back c;
	     new_def c;
	     !wr (clause_category c, c))

	fun p_split_def_1 splitdef =
	    (prog_rec_split_def ();
	     p_split_def splitdef)

	fun deep (V _) = false
	  | deep (_ $ l) =
	    exists
	      true
	    | _ $ _ in list l
	    end

	fun rename_deep_term (V x, rho, n) =
	    if x inset rho
		then (V (?rho x), rho, n)
	    else (V n, rho ++ {x => n}, n+1)
	  | rename_deep_term (f $ l, rho, n) =
	    let val (l', rho', n') = rename_deep_term_list (l, rho, n)
	    in
		(f $ l', rho', n')
	    end
	and rename_deep_term_list (a as (nil, ...)) = a
	  | rename_deep_term_list (t::l, rho, n) =
	    let val (t', rho', n') = rename_deep_term (t, rho, n)
		val (l', rho'', n'') = rename_deep_term_list (l, rho', n')
	    in
		(t'::l', rho'', n'')
	    end

	val deep_abbrevs : (atom, string) table = table ()
	val da_get = t_get deep_abbrevs
	val da_put = t_put deep_abbrevs

	fun wait_insert_1 (c as CL (h, ql, al, Bs)) =
	    if deepabbrvp andalso
		exists
		  exists
		    true
		  | _ $ _ in list l
		  end
		| (P, _ $ l) in list al
		end andalso
		(case h of
		     HFUN (P, ...) => not (da_matches P)
		   | _ => not (empty Bs) orelse
		     exists
		       not (da_matches Q)
		     | (Q, _) in list al
		     end
		     )
		then let val al' =
			     [if deep t
				  then let val (t', rho, n) = rename_deep_term (t, {}, 1)
					   val invrho = inv rho
					   val (newQ, newf) =
					       case da_get a of
						   SOME Q => (Q, Q ^ "_fun")
						 | _ =>
						   let val Q = gensym "#q"
						       val g = Q ^ "_fun"
						       val ir = ref 1
						       val t'' = g $ [V (!ir) before inc ir
								     |while !ir<n]
						       val vars' = rng rho
						       val h' = HFUN (Q, g, n-1,
								      vars', t'')
						       val psenv = if P inset !skeleta
								       then ps_match_term (t,
											   ?(!skeleta) P,
											   {})
								   else raise NoPathSetEvt
								       handle NoPathSetEvt => raise DeepPathSet
						       val ps = if empty vars'
								    then PS_ENUM {(g, 0) => PS_ALL}
								else PS_ENUM {(g, i) => psi
									     | i in set vars'
										 val psi =
										     if i inset psenv
											 then ?psenv i
										     else PS_ALL}
						       val def = CL (h', {}, [(P, t')], {})
						   in
						       prog_abbrv ();
						       p_abbrv_def def;
						       da_put (a, Q);
						       fargsq := !fargsq ++ {g => (n-1, vars', t'')};
						       skeleta := !skeleta ++ {Q => ps};
						       (*!!! in case auto_guide is not NONE,
							should also make something with
							ag_intersects_blk and ag_match_term.
							While this has not been done,
							the -auto option is deactivated in main.ml.*)
						       wait_insert_0 def;
						       (Q, g)
						   end
					   val ir = ref 1
				       in
					   (newQ, newf $ [V (?invrho (!ir)) before inc ir
							 |while !ir<n])
				       end
			      else a
			     | a as (P, t) in list al]
			 val conc = CL (h, ql, atom_sort (elems al'), Bs)
		     in
			 p_abbrv_use (conc, c);
			 wait_insert_0 conc
		     end
	    else (* no deep split *)
		     wait_insert_0 c

	(* gen_resolvent ([t1, ..., tn], [B1, ..., Bn], al, Bs)
	 adds B1(t1), ..., Bn(tn) to part of clause referenced as al, Bs.
	 This is only done provided pathsets are compatible with those
	 given in environment psenv. *)

	fun gen_resolvent (_, nil, al, Bs) = (* optimization *)
	    let val pse = ps_match_al (al, ps_match_Bs (Bs, {}))
	    in
		(al, Bs, pse)
	    end
	  | gen_resolvent (t1n, B1n, al, Bs) =
	    let val Bsr = ref Bs
		val atomsr = ref ({} : atom set)
		val psenvr = ref {}
	    in
		iterate
		  (case t of
		       V x => let val curBs = !Bsr
				  val B1ps = ps_check_empty (q_skeleta B1)
				  val pse = !psenvr
			      in
				  if x inset pse
				      then psenvr := pse ++
					  {x =>
					   ps_check_empty (ps_inter (?pse x,
								     B1ps))}
				  else psenvr := pse ++ {x => B1ps};
				  if x inset curBs
				      then Bsr := curBs ++ {x => ?curBs x U B1}
				  else if empty B1
				      then ()
				  else Bsr := curBs ++ {x => B1}
			      end
		     | _ => atomsr := !atomsr ++ {(psenvr := ps_match_a (a, !psenvr);
						   a)
						 | P in set B1
						     val a = (P, t)})
		|| t in list t1n
		and B1 in list B1n
		end;
		let val al' = atom_sort (!atomsr)
		    val al'' = atom_merge (al', al)
		    val pse = ps_match_al (al, ps_match_Bs (Bs, !psenvr))
		in
		    (al'', !Bsr, pse)
		end
	    end

	(* gen_resolvent_auto: variant of gen_resolvent where
	 al is not a list but a set of atoms.  Used by resolve_auto. *)

	fun gen_resolvent_auto (_, nil, ats, Bs, pse) = (* optimization *)
	    (* pse = ps_match_as (ats, ps_match_Bs (Bs, {})) *)
	    (ats, Bs, pse)
	  | gen_resolvent_auto ([t], [B1], ats, Bs, pse) = (* optimization again *)
	    (case t of
		 V x =>
		 let val B1ps = ps_check_empty (q_skeleta B1)
		     val pse' = if x inset pse
				    then pse ++ {x =>
						 ps_check_empty (ps_inter (?pse x,
									   B1ps))}
				else pse ++ {x => B1ps}
		     val Bs' = if x inset Bs
				   then Bs ++ {x => ?Bs x U B1}
			       else if empty B1
				   then Bs
			       else Bs ++ {x => B1}
		 in
		     (ats, Bs', pse')
		 end
	       | _ =>
		 let val ats' = {(P, t)
				| P in set B1}
		 in
		     (ats U ats', Bs, ps_match_as (ats', pse))
		 end)
	  | gen_resolvent_auto (t1n, B1n, ats, Bs, pse) =
	    let val Bsr = ref Bs
		val atomsr = ref ats
		val psenvr = ref pse
	    in
		iterate
		  (case t of
		       V x => let val curBs = !Bsr
				  val B1ps = ps_check_empty (q_skeleta B1)
				  val pse = !psenvr
			      in
				  if x inset pse
				      then psenvr := pse ++
					  {x =>
					   ps_check_empty (ps_inter (?pse x,
								     B1ps))}
				  else psenvr := pse ++ {x => B1ps};
				  if x inset curBs
				      then Bsr := curBs ++ {x => ?curBs x U B1}
				  else if empty B1
				      then ()
				  else Bsr := curBs ++ {x => B1}
			      end
		     | _ => atomsr := !atomsr U {(psenvr := ps_match_a (a, !psenvr);
						  a)
						| P in set B1
						    val a = (P, t)})
		|| t in list t1n
		and B1 in list B1n
		end;
		(!atomsr, !Bsr, !psenvr)
	    end


	val splitdefq : (block, unit) table = table ()
	    (* memoizes which splitting literals have been defined already. *)
	val sdq_get = t_get splitdefq
	val sdq_put = t_put splitdefq
	val sdq_rem = t_remove splitdefq

	fun new_q_1 q =
	    (sdq_rem q;
	     qq := !qq U {q})

	fun new_q (q, winsert) =
	    (new_q_1 q;
	     let val c = CL (HQ q, {}, nil, {})
		 val card_q = card q
		 val maxn = if card_q<=10
				then 2
			    else if card_q<=100
				then 1
			    else 0
		 val cards = 1 to maxn
	     in
		 iter_sub_map ((fn q' =>
				   if not (empty q') andalso not (q' inset !qq)
				       then
					   (p_split_split (q', c);
					    winsert (CL (HQ q', {}, nil, {}))
					    (* instead of new_q_1 q'; *)
					    )
				   else ()),
				   q, cards, cards)
	     end)

	fun prove_q_simple q =
	    if q inset !qq
		then true
	    else let val witnesses = inter {if P inset !sure_facts
						then ?(!sure_facts) P
					    else {}
					   | P in set q}
		 in
		     if empty witnesses
			 then false
		     else let val splitdef = CL (HQ q, {}, nil, {1 => q})
			      val ut = choose witnesses
			  in
			      p_split_def_1 splitdef;
			      p_ne (q, splitdef, ut);
			      (* now generate fact q. *)
			      wait_insert_0 (CL (HQ q, {}, nil, {})); (*new_q q;*)
			      true
			  end
		 end

	val wait_insert_1_aux =
	    if maxneglit=max_int
		then wait_insert_1
	    else if maxneglit=0
		then fn (CL (h, ql, _, Bs)) =>
		    wait_insert_1 (CL (h, ql, nil, Bs))
	    else fn (ce as (CL (h, ql, al, Bs))) =>
		(let val |[insert, popmin, ...]| = mheap (op <)
		     val ir = ref 0
		     val others = ref {}
		     val defineds = {a
				    | a as (P, t) in list al
				      such that if fully_defined P
						    then true
						else (inc ir;
						      insert (t_size t, a);
						      false)}
		 in
		     if !ir<=maxneglit
			 then raise AlFirst1Evt
		     else
			 (ir := maxneglit;
			  while !ir<>0 do
			      (dec ir;
			       let val (_, a) = popmin ()
			       in
				   others := !others U {a}
			       end);
			 wait_insert_1 (CL (h, ql, atom_sort (defineds U !others), Bs)))
		 end
		     handle AlFirst1Evt => wait_insert_1 ce)

	fun wait_insert_2 c =
	    if is_tautology c
		then ()
	    else let val CL (h, ql, al, Bs) = c
		     val splitBs1 = head_vars h <-| Bs
		     val splitBs = if empty splitBs1
				       then {}
				   else al_vars al <-| splitBs1
		 in
		     if empty splitBs (* nothing to split *)
			 then wait_insert_1_aux c
		     else if (case h of
				  HQ _ => true
				| HBOT _ => true
				(* | HFUN (_, _, 0, ...) => true
				 No: otherwise P(c) :- Q(X) would
				 be considered as an automaton clause;
				 but this is not one. *)
				| _ => false)
			 (* head is ground and *)
			 andalso null al (* body is just a block: don't split *)
			 andalso (case Bs of
				      {i => B} =>
				      (if i=1
					   then wait_insert_1_aux c
				       else let val c' = CL (h, ql, al,
							     {1 => B})
					    in
						p_rename_resolve (c', c,
								  {i => 1});
						wait_insert_1_aux c'
					    end;
					   true)
				    | _ => false)
			 then ()
		     else
			 (* split: first generate splitting clauses *)
			 (iterate
			    if prove_q_simple blk
				then ()
			    else (case sdq_get blk of
				      SOME _ => ()
				    | _ =>
				      let val splitdef = CL (HQ blk, {}, nil, {1 => blk})
				      in
					  p_split_def_1 splitdef;
					  wait_insert_1_aux splitdef;
					  sdq_put (blk, ())
				      end)
			  | x => blk in map splitBs
			  end; (* then process split clause *)
			    let fun process_split_clause (c as CL (h, ql, al, Bs)) =
				    case ql <| !qq of
					{} =>
					  (case ql of
					       {} => wait_insert_1_aux c
					     | {q} U ql' => 
					       (* do as if we had called resolve_P_f directly,
						and insert clause into selqq: *)
					       if insert_selqq (q, h, ql', al, Bs)
						   then (h_new_def h;
							 compile_auto_back c
							 )
					       else ()
						   )
				      | {q} U ql' =>
					(* resolve directly with known q's: *)
					let val c' = CL (h, ql \ {q}, al, Bs)
					in
					    p_q_resolve (c', c, q);
					    process_split_clause c'
					end
				val conc = CL (h, rng splitBs, al,
					       splitBs <-| Bs)
			    in
				p_split_use (conc, c, splitBs);
				process_split_clause conc
			    end)
		 end

	val wait_insert = wait_insert_2

	val botq = ref ({} : string set);
	(* current set of bot names that have been derived. *)

	fun record_bot (c as CL (HBOT botname, ...)) =
	    (flush_all ();
	     do_bot c;
	     prog_rec_bot ();
	     (* Now update botq: *)
	     botq := !botq U {botname})

	fun insert_selfq (h, al, Bs) =
	    let val entry = (h, al)
	    in
		iterate
		  let val fmapr = selfq_get_table P
		      val clsr = t_get_table fmapr f
		      val Bsr = t_get_mapr clsr entry
		  in
		      Bsr := !Bsr U {Bs}
		  end
		| (P, f $ _) in list al
		end
	    end

	fun clause_compile_auto (P, f, Bs) =
	    (let val fmapr = t_get_table autoinfoq P
		 val blksr as ref blks = t_get_blocksr fmapr f
	     in
(*
let val (k, vars, t) = ?(!fargsq) f
    val extraBs = vars <-| Bs
in
  if empty extraBs then () else raise NthBug
end;
*)
		 blksr := bs_add (Bs, blks)
		 (* t_put_behind blklsr (blkl, ()) *)
	     end
	     )

	fun ct_subsumed (CL (h, ql, al, Bs)) =
	    (case h of
		 HVAR P => P inset !univq
	       | HFUN (P, ...) => P inset !univq
	       | HQ q => q inset !qq
	       | HBOT botname => botname inset !botq)

	    (* ct_subsumed_by_auto c
	     checks whether c is subsumed by some clause from autoinfoq (an automaton clause).
	     Classically, this amounts to saying when c = c'.sigma \/ d
	     for some c' in autoinfoq, some substitution sigma, and some additional literals d.

	     A Trick we can use is:

	     We rather ask [only if number of matching automata clauses in autoinfoq is <=4]:
	     (+) Is c valid in all models defined by automata containing (at least) all clauses
	     in autoinfoq?
	     (In the sense used in model.ml.)
	     Abbreviate this condition as ||- c.
	     Then we have the rules:
	     - if c is a tautology then ||- c.
	     - if c = P(f(X1,...,Xn)) :- body, and the clauses with head P(f(X1,...,Xn))
	       in autoinfoq are ci = P(f(X1,...,Xn)) :- Bi1(X1), ..., Bin(Xn),  i=1..p,
	       then ||- c as soon as ||- \/_i (Bi1(X1), ..., Bin(Xn)) :- body,
	       in particular as soon as for some i, for every j=1..n,
	       for every P in Bij, ||- P(Xi) :- body.  [A variant of rule MC_DEDUCE_POS in model_h.ml]
	       We test the latter by requiring ||- P(Xi) :- ql, al, B(Xi),
	       where body = ql, al, Bs as {B(X1), ...}.

	     The problem is that this removes important automaton clauses from
	     final automaton model.  E.g, assume that state P is defined by:
	     P(f(X)) :- Q(X)
	     in the final model.
	     Now assume all terms recognized at P are recognized at P'. Say:
	     P'(f(X)) :- Q(X)
	     P'(g(X)) :- R(X)
	     Then this optimization will remove the clause P'(f(X)) :- Q(X),
	     on the grounds that it can be derived from P(f(X)) :- Q(X) and
	     the epsilon-clause P'(Z) :- P(Z).  But epsilon-clauses are
	     not produced in the final automaton.
	     The same phenomenon induces some fundamental incompleteness
	     of the prover if this Trick is used.  So it is deactivated.

	     At point (1) below, we had:
			   ((iter_sub_Bs (fn Bs' =>
					     if blkl_from_Bs (Bs', k) inset blkls
						 then raise CtSubsumedEvt
					     else ()
						 ) Bs;
			     false)
				handle CtSubsumedEvt => true)

             At point (2) below, we had:
			   exists
			     all
			       B subset B' (* shortcut, tested anyway below. *)
			       orelse
			       all
				 P inset B' orelse
				 let val Bs' = if !ir=1
						   then Bs
					       else (Bs O {1 => !ir, !ir => 1}) ++ ({1, !ir} <-| Bs)
				     val al' = if !ir=1
						   then al
					       else let val sigma = {1 => V (!ir), !ir => V 1}
							val tsub = tsubst sigma
						    in
							atom_sort {(Q, tsub t)
								  | (Q, t) in list al}
						    end
				 in
				     ct_subsumed_try (CL (HVAR P, ql, al', Bs'))
				 end
			       | P in set B
			       end
			     | B in list blkl
			     val B' = (inc ir;
				       if !ir inset Bs
					   then ?Bs (!ir)
				       else {})
			     end
			   | blkl in set blkls
			   val ir = ref 0
			   end
	     *)
	fun ct_subsumed_by_auto (CL (HFUN (P, f, k, ...), ql, al, Bs)) =
	    (case a_get P of
		 SOME fmap =>
		 (case t_get fmap f of
		      SOME (ref blks) =>
		      bs_subsumed (Bs, blks)
		    | _ => false)
	       | _ => false)
	  | ct_subsumed_by_auto _ = false
	and ct_subsumed_try (CL (h, ql, al, Bs)) =
	    ((iter_sub_map (fn als =>
			       let val al' = [a | a in list al such that a inset als]
			       in
(*
(case wantproof of
     SOME (f as |[put, flush, ...]|) =>
(put "* ct_subsumed_try ";
print_clause (f, "X") (CL (h, ql, al', Bs));
put "\n";
flush ())
   | _ => ());
*)
				   if ct_subsumed_simple (CL (h, ql, al', Bs))
				       then (
(*
(case wantproof of
     SOME (f as |[put, flush, ...]|) =>
     (put "SUBSUMED!\n";
      flush ())
   | _ => ());
*)
					     raise CtSubsumedEvt)
				   else ()
			       end,
			       elems al, {0, 1, 2}, {0, 1, 2});
	      false)
	     handle CtSubsumedEvt => true)
	    (*
	    exists
	      ct_subsumed_simple (CL (h, ql, al', Bs))
	    | als sub map elems al
	    val al' = [a | a in list al such that a inset als]
	    end
	     *)
	and ct_subsumed_simple (c as CL (h, _, al as (P, f $ _) :: _, Bs)) =
	    (case selfq_get P of
		 SOME fmap =>
		 (case t_get fmap f of
		      SOME clsr =>
		      (case t_get clsr (h, al) of
			   SOME Bsr => Bs inset !Bsr
			 | _ => false)
		    | _ => false)
	       | _ => false)
		 orelse ct_subsumed_by_auto c
		 orelse ct_subsumed_by_eps c
	  | ct_subsumed_simple (c as CL (HFUN _, _, nil, ...)) =
	    ct_subsumed_by_auto c orelse ct_subsumed_by_eps c
	  | ct_subsumed_simple (CL (h as HVAR P, _, nil, {1 => B, ...}, ...)) =
	    exists
	      (case selxq_get (choose B') of
		   SOME cls =>
		   (case t_get cls h of
			SOME Br => B' inset !Br
		      | _ => false)
		 | _ => false)
	    | B' sub map B
		such that not (empty B')
	    end
	  | ct_subsumed_simple (CL (HVAR _, _, nil, ...)) =
	    false (* case of clauses P(X1) <= B2 (X2), B3(X3), ...
		   with no X1 on the right. *)
	  | ct_subsumed_simple (CL (h, ql, nil, Bs)) =
	    exists
	      exists
		(case selxq_get (choose B') of
		     SOME cls =>
		     (case t_get cls h of
			  SOME Br => B' inset !Br
			| _ => false)
		   | _ => false)
	      | B' sub map B
		  such that not (empty B')
	      end
	    | _ => B in map Bs
	    end
	  | ct_subsumed_simple _ = false
	and ct_subsumed_by_eps (CL (h as HFUN (P, f, _, _, t), _, al, ...)) =
	    ct_subsumed_simple (CL (HVAR P, {}, nil,
				    {1 => {Q
					  | (Q, u) in list al
					      such that t=u}}))
	  | ct_subsumed_by_eps _ = false

	fun elim_subsumed_by_univ P =
	    a_rem P

	fun P_clauses P =
	    let val csf = case selfq_get P of
			      SOME fmap =>
			      t_collect fmap (fn (_, clsr) =>
						 t_collect clsr (fn ((h, al), Bsr) => 
								    {CL (h, {}, al, Bs)
								    | Bs in set !Bsr}))
			    | _ => {}
	    (* Don't include clauses from selxq:
	     only clauses from selfq are resolved with fully defined Ps.
		val csx = case selxq_get P of
			      SOME cls =>
			      t_collect cls
			      (fn (h, Br) =>
				  {CL (h, {}, nil, {1 => B})
				  | B in set !Br})
			    | _ => {}
	     *)
	    in
		csf (* U csx *)
	    end

	fun some_fully_defined_al al =
	    exists
	      fully_defined P
	    | (P, _) in list al
	    end

	    (*
	fun resolve_auto (h, nil, newal, Bs, pi_l, c, c0) =
	    let val conc = CL (h, {}, newal, Bs)
	    in
		p_auto_resolve (conc, c, pi_l);
		wait_insert conc;
		subsumes (conc, c0)
	    end
	  | resolve_auto (h, (P, t as f $ l) :: rest, newal, Bs, pi_l, c, c0) =
	    if P inset !univq
		then resolve_auto (h, rest, newal, Bs,
				   (AC_UNIV P, MGU_AUTO_X1_IS t)::pi_l,
				   c, c0)
	    else (case a_get P of
		      SOME fmap =>
		      (case t_get fmap f of
			   SOME blkls =>
			   let val (k, vars, t) = ?(!fargsq) f
			       val some_subs = ref false (* will be set to true as soon
							  as one of the produced resolvents
							  subsumes the non-automaton premise. *)
			   in
			       iterate
				 (*
			       t_iter blkls
			       (fn (blkl, _) =>
				  *)
				   (let val (newal', Bs', _) =
					    gen_resolvent (l, blkl, newal, Bs)
				    in
					(*ps_match_al (newal', ps_match_Bs (Bs', {}));*)
					(* Resolve with P (f(x1,...,xn)) <= B1(x1), ..., Bn(xn) *)
					if resolve_auto (h, rest, newal', Bs',
							 (AC_POP (P, f, blkl),
							  MGU_AUTO_Xs_ARE l)::pi_l,
							 c, c0)
					    then some_subs := true
					else ()
					    (*;
				       false*)
				   end handle NoPathSetEvt => () (*false*) )
				   (*
				    );
				    *)
			       | blkl in set !blkls
			       end;
			       !some_subs
			   end
			 | _ => false (* cannot resolve: no automaton clause with head P(f(...)) *)
			   )
		    | _ => false (* cannot resolve: no automaton clause with head P (...) *)
		      )
		*)

	val ra_sort = sort ((fn ((m, ...), (n, ...)) => m<n) : (int * atom * block list set) order);

	fun resolve_auto (h, al, newal, Bs, pi_l, c, c0) =
	    (* As the resolve_auto in comments above, except clauses are sorted so that
	     - we resolve on universal predicates first (univa);
	     - if any atom cannot be resolved upon, no resolvent is generated (raise ResolveAutoEvt);
	     - non-universal atoms with the least number of resolvents are resolved upon first (ra_sort).
	     *)
	    (let val univa = ref nil
		 val blkls_from_blocks_1 = blkls_from_blocks ()
		 val notuniva = [(case a_get P of
				      SOME fmap =>
				      (case t_get fmap f of
					   SOME (ref blks)
					   => let val blkls =
						      blkls_from_blocks_1 blks
					      in
						  (card blkls, a, blkls)
					      end
					 | _ => raise ResolveAutoEvt (* no resolvent *))
				    | _ => raise ResolveAutoEvt (* no resolvent *))
				| a as (P, t as f $ _) in list al
				  such that if P inset !univq
						then (univa := a :: !univa;
						      false)
					    else true]
		 val newas = elems newal
		 val new_clauses = ref {}
		 fun rauto_notuniv (nil, newas, Bs, pi_l, c, c0, _) =
		     let val conc = CL (h, {}, atom_sort newas, Bs)
		     in
			 if subsumes (conc, c0)
			     then if subsumes (c0, conc)
				      then () (* if conc=c0 (up to renaming),
					       don't generate anything *)
				  else (p_auto_resolve (conc, c, pi_l);
					(* Insert conc, and backward subsume c0;
					 don't do this if conc=c0, otherwise,
					 we shall keep generating the same clause
					 over and over again. *)
					wait_insert conc;
					raise ResolventSubsumesPremiseEvt)
			 else new_clauses := !new_clauses U {(conc, c, pi_l)}
		     end
		   | rauto_notuniv ((_, (P, f $ l), Bss) :: rest, newas, Bs, pi_l, c, c0, pse) =
		     let val (_, _, t) = ?(!fargsq) f
			 val k = len l
		     in
			 iterate
			   (let val blkl = blkl_from_Bs (Bsauto, k)
				val (newas', Bs', pse') =
				    gen_resolvent_auto (l, blkl, newas, Bs, pse)
			    in
				(*ps_match_al (newal', ps_match_Bs (Bs', {}));*)
				(* Resolve with P (f(x1,...,xn)) <= B1(x1), ..., Bn(xn) *)
				rauto_notuniv (rest, newas', Bs',
					       (AC_POP (P, f, blkl),
						MGU_AUTO_Xs_ARE l)::pi_l,
					       c, c0, pse')
			    end handle NoPathSetEvt => () (*false*) )
			 | Bsauto in set Bss
			 end
		     end
		 fun rauto_univ (nil, pi_l, c, c0) =
		     (rauto_notuniv (notuniva, newas, Bs, pi_l, c, c0,
				     ps_match_as (newas, ps_match_Bs (Bs, {}))
				     )
		      handle NoPathSetEvt => () (* false *)
		      )
		   | rauto_univ ((P, t) :: rest, pi_l, c, c0) =
		     rauto_univ (rest, (AC_UNIV P, MGU_AUTO_X1_IS t)::pi_l, c, c0)
	     in
		 (rauto_univ (!univa, pi_l, c, c0);
		  iterate
		    (p_auto_resolve cdata;
		     wait_insert conc)
		  | cdata as (conc, ...) in set !new_clauses
		  end;
		  false
		  ) handle ResolventSubsumesPremiseEvt => true
	     end handle ResolveAutoEvt => false)

	fun resolve_auto_def (h, nil, newal, Bs, pi_l, c, c0) =
	    let val conc = CL (h, {}, newal, Bs)
	    in
		p_auto_resolve (conc, c, pi_l);
		if subsumes (c0, conc)
		    then false (* conc always subsumes c0; if c0 also subsumes conc,
				then they are equal up to renaming: don't generate
				anything, and don't back-subsume c0. *)
		else (do_fast (fn () => wait_insert conc);
		      true)
	    end
	  | resolve_auto_def (h, (a as (P, t as f $ l)) :: rest, newal, Bs, pi_l, c, c0) =
	    if fully_defined P
		then if P inset !univq
			 then resolve_auto_def (h, rest, newal, Bs,
						(AC_UNIV P, MGU_AUTO_X1_IS t)::pi_l, c, c0)
		     else (
(*
(case wantproof of
     SOME (f as |[put, flush, ...]|) =>
(put "% fully defined symbol: ";
 put P; put "\n";
flush ())
   | _ => ());
*)
			   case a_get P of
			       SOME fmap =>
			       (case t_get fmap f of
				    SOME (ref blks) =>
				    let val (k, vars, t) = ?(!fargsq) f
				    in
					iterate
					    (let val blkl = blkl_from_Bs (Bsauto, k)
						 val (newal', Bs', _) =
						    gen_resolvent (l, blkl, newal, Bs)
					    in
						(*ps_match_al (newal',
							     ps_match_Bs (Bs', {}));*)
						resolve_auto_def (h, rest, newal', Bs',
								  (AC_POP (P, f, blkl),
								   MGU_AUTO_Xs_ARE l)::pi_l,
								  c, c0)
					    end handle NoPathSetEvt => false)
					| Bsauto in set blkls_from_blocks () blks
					end;
					true
				    end
				  | _ => true)
			     | _ => true)
	    else resolve_auto_def (h, rest, atom_insert (a, newal), Bs, pi_l, c, c0)

	fun resolve_selx (h, B, c, c0) =
	    case B <| !univq of
		{P} U rest =>
		  let val B' = B \ {P}
		      val c' = CL (h, {}, nil,
				   if empty B' then {} else {1 => B'})
		  in
		      p_eps_resolve (c', c, AC_UNIV P, V 1);
		      resolve_selx (h, B', c', c0)
		  end
	      | _ =>
		if empty B
		    then if subsumes (c, c0)
			     then if subsumes (c0, c)
				      then false (* don't generate c; don't backward
						  subsume c0 (this would loop) *)
				  else (wait_insert c; true
					(* generate c, backward subsume c0 *)
					)
			 else (wait_insert c; false
			       (* generate c; cannot backward subsume c0 *)
			       )
		else (let val funs0 = inter {(case a_get P of
						  SOME fmapr =>
						  t_collect fmapr (fn (f, _) => {f})
						| _ => raise ResolveSelxEvt)
					    | P in set B}
			  val psB = q_skeleta B
			  val funs = case ps_funs psB of
					 SOME fs => funs0 & fs
				       | _ => funs0
			  val {P} U rest = B
			  val SOME fmapP = a_get P
			  val fmap_get = t_get fmapP
			  val some_subs = ref false
		      in
			  iterate
			    let val SOME (ref blks) = fmap_get f
				val (k, vars, t) = ?(!fargsq) f
				val h' = case h of
					     HVAR P => HFUN (P, f, k, vars, t)
					   | _ => h (* does not work if h is HFUN _,
						     in which case resolve_selx should not be
						     called. *)
			    in
				iterate
				  (let val al' = if empty rest
						     then nil
						 else atom_sort {(Q, t) | Q in set rest}
				       val pse = ps_match_al (al',
							      ps_match_Bs (Bsauto,
									   {}))
				       val c' = CL (h', {}, al', Bsauto)
				   in
				       (case wantproof of
					    SOME _ =>
					    let val (k, ...) = ?(!fargsq) f
						val blkl = blkl_from_Bs (Bsauto, k)
					    in
						p_eps_resolve (c', c,
							       AC_POP (P, f, blkl),
							       t)
					    end
					  | _ => ());
				       if resolve_auto (h', al', nil, Bsauto,
							nil, c', c0)
					   then some_subs := true
				       else ()
				   end handle NoPathSetEvt => () )
				| Bsauto in set blkls_from_blocks () blks
				end
			    end
			  | f in set funs
			  end;
			  !some_subs
		      end handle ResolveSelxEvt => false)

		    (* Don't use resolve_selx_def.  This causes loops as in:
		     #false(clause3) :- p(X1). [eps-resolve:
		       #false(clause3) :- p(X1). {X1=f(X1)}
		       p(f(X1)) :- p(X1).
		       ]
		     % |- #false(clause3) :- p(X1).
		     *)
		    (*
	fun resolve_selx_def (h, B, defB, c) =
	    case defB <| !univq of
		{P => pi} U rest =>
		  let val defB' = defB \ {P}
		      val allB' = B U defB'
		      val c' = CL (h, {}, nil,
				   if empty allB' then {} else {1 => allB'})
		  in
		      p_eps_resolve (c', c, AC_UNIV P, V 1);
		      resolve_selx_def (h, B, defB', c')
		  end
	      | _ =>
		if empty defB
		    then do_fast (fn () => wait_insert c)
		else (let val funs0 = inter {(case a_get P of
						  SOME fmapr =>
						  t_collect fmapr (fn (f, _) => {f})
						| _ => raise ResolveSelxEvt)
					    | P in set defB}
			  val psB = q_skeleta (B U defB)
			  val funs = case ps_funs psB of
					 SOME fs => funs0 & fs
				       | _ => funs0
			  val {P} U rest0 = defB
			  val rest = B U rest0
			  val SOME fmapP = a_get P
			  val fmap_get = t_get fmapP
		      in
			  iterate
			    let val SOME (ref blks) = fmap_get f
				val (k, vars, t) = ?(!fargsq) f
				val h' = case h of
					     HVAR P => HFUN (P, f, k, vars, t)
					   | _ => h (* does not work if h is HFUN _,
						     in which case resolve_selx_def should not be
						     called. *)
			    in
				iterate
				  (let val al' = if empty rest
						     then nil
						 else atom_sort {(Q, t) | Q in set rest}
				       val pse = ps_match_al (al',
							      ps_match_Bs (Bsauto,
									   {}))
				       val c' = CL (h', {}, al', Bsauto)
				   in
				       (case wantproof of
					    SOME _ =>
					    let val (k, ...) = ?(!fargsq) f
						val blkl = blkl_from_Bs (Bsauto, k)
					    in
						p_eps_resolve (c', c,
							       AC_POP (P, f, blkl),
							       t)
					    end
					  | _ => ());
				       if empty rest0
					   then do_fast (fn () => wait_insert c')
				       else (resolve_auto_def (h', al', nil,
							       Bsauto, nil,
							       c', c);
					     ())
				   end handle NoPathSetEvt => () )
				| Bsauto in set blkls_from_blocks () blks
				end
			    end
			  | f in set funs
			  end
		      end handle ResolveSelxEvt => ()
			  )
		    *)

	val intermap = ref ({} : string -m> block) (* if mknondet=true,
						    keeps a map from __inter_P_Q_..._R symbols
						    to blocks {P, Q, ..., R} (where P, Q, ..., R
						    are possibly __inter_* symbols). *)

	memofun interflat B = (* in case mknondet=true, expand each P in B to the block
			       it represents, and return corresponding predicate name.
			       B should not be empty. *)
	    case B of
		{} => raise ResolveInterFlat
	      | {P} => P
	      | _ => let val Q = mk_inter B
		     in
			 if Q inset !intermap
			     then ()
			 else let val c = CL (HVAR Q, {}, nil, {1 => B})
			      in
				  intermap := !intermap ++ {Q => B};
				  skeleta := !skeleta ++ {Q => q_skeleta B};
				  prog_rec_nondet_split_def ();
				  p_nondet_split_def c;
				  wait_insert c
			      end;
			      Q
		     end

	fun do_resolve_auto (c as CL (h as HFUN (P, f, k, vars, t), {}, nil, Bs), res_auto) =
	    (* automaton clause *)
	    (auto_back_subsume c;
	     let
		val backs = ref {} (* clauses that will have to be backward subsumed. *)
	     in
		    (* first try to resolve with some C \/ -P(f(...)) with -P(f(...)) selected: *)
		    (case selfq_get P of
			 SOME fmapr =>
			 (case t_get fmapr f of
			      SOME clsr =>
			      let val c_raw = AC_POP_RAW c
				  val blkl = blkl_from_Bs (Bs, k)
			      in
				  t_iter clsr
				  (fn ((h', al'1), Bsr') =>
				      (iterate
					 let val c' = CL (h', {}, al'1, Bs')
					     fun res_1 (al' as (a' as (P', f' $ l')) :: rest', acc') =
						 (if P=P' andalso f=f'
						      then let val other_al = revappend (acc', rest')
							       val (al'', Bs'', _) =
								   gen_resolvent (l', blkl, nil, {})
							       val mgu' = MGU_AUTO_Xs_ARE l'
							       val Bs1 = (Bs' delta Bs'') ++
								   {i => B U B'
								   | i => B in map Bs'' <| Bs'
								       val B' = ?Bs'' i}
							   in
(*
(case wantproof of
     SOME (f as |[put, flush, ...]|) =>
(put "% clause may be removed later because of fully defined symbol ";
put P; put ": ";
 print_clause (f, "X") c'; put "\n";
flush ())
   | _ => ());
*)
						      if res_auto (h', other_al, al'', Bs1,
								   [(c_raw, mgu')], c', c')
							  then (prog_rem_subsumed_premise ();
(*
(case wantproof of
     SOME (f as |[put, flush, ...]|) =>
(put "% clause will be removed because of fully defined symbol ";
put P; put ": ";
 print_clause (f, "X") c'; put "\n";
flush ())
   | _ => ());
*)
								backs := !backs U {c'})
						      else ()
							   end handle NoPathSetEvt => ()
						  else ();
						      res_1 (rest', a'::acc'))
					       | res_1 _ = ()
					 in
					     res_1 (al'1, nil)
					 end
				       | Bs' in set !Bsr'
				       end;
					 false));
				  ()
			       (* [this is fishy:]
				if empty Bs (* unit clause *)
				   then t_remove fmapr f
			       else ()
				   *)
			   end
			 | _ => ())
		    | _ => ());
		      iterate
			b_set_auto c' (* was b_set c'; b_set_auto is auto_back_subsume
				       in case auto_back is used.  This is used here because
				       this will also remove c' from auto_back; in
				       theory also removes clauses subsumed by c', but
				       they should have been removed already. *)
		      | c' in set !backs
		      end;
		      backs := {};
		      (* then try to resolve with some C \/ -P(x) with -P(x) selected: *)
		      (case selxq_get P of
			   SOME cls =>
			   (t_iter cls
			    (fn (h', Br) =>
				(* with h' of the form P'(x1), q, or bot, and B
				 containing P. *)
				(iterate
				   (let val Bs' = {1 => B}
					val c' = CL (h', {}, nil, Bs')
					val h'' = case h' of
						      HVAR P' => HFUN (P', f, k, vars, t)
						    | _ => h'
					val B' = B \ {P}
					val al' = if empty B'
						      then nil
						  else atom_sort {(Q, t) | Q in set B'}
					val c'' = CL (h'', {}, al', Bs)
				    in
					ps_match_al (al', ps_match_Bs (Bs, {}));
					p_eps_resolve (c'', c', AC_POP_RAW c, t);
					if null al'
					    then wait_insert c''
					else if res_auto (h'', al', nil, Bs,
							  nil, c'', c')
					    then (prog_rem_subsumed_premise ();
						  backs := !backs U {c'})
					else ()
				    end handle NoPathSetEvt => ())
				 | B in set !Br
				 end;
				   false)
				);
				())
			 | _ => ())
	     end)
	| do_resolve_auto _ = () (* only deal with automaton clauses *)

	(* resolve_P_f (c, psenv)
	 Resolves clause c against all automata clauses in autoinfoq, qq
	 (if c is a non-automaton clause)
	 or against all non-automata clauses in selfq, selxq (if c is an automaton clause).
	 Adds all resolvents to waitq, as objects of type 'clause', even though
	 some are automata clauses.
	 psenv is a pathset environment that constrains variables.
	 *)
	fun resolve_P_f (c as CL (h, {q} U ql, al, Bs)) =
	    (if q inset !qq
		 then let val conc = CL (h, ql, al, Bs)
		      in
			  p_q_resolve (conc, c, q);
			  wait_insert conc;
			  say_rem_subsumed_premise ();
			  h_rem_def h
		      end
	     (* resolve C \/ -q with +q, and return C in front of acc.
	      Do not add c either to forward subsumption structures or to selqq,
	      because resolvent subsumes premise. *)
	     else ( (* otherwise cannot resolve. *)
		   (* Now update selqq: *)
		   if insert_selqq (q, h, ql, al, Bs)
		       then ()
		   else (say_rem_subsumed_premise ();
			 h_rem_def h)
		 ))
	  | resolve_P_f (c as CL (h, {}, al as [_, ...], Bs)) =
	    (if some_fully_defined_al al
		 then (resolve_auto_def (h, al, nil, Bs, nil, c, c);
		       say_rem_fully_defined_parent ();
		       h_rem_def h)
	     else if resolve_auto (h, al, nil, Bs, nil, c, c)
		 then (say_rem_subsumed_premise ();
		       h_rem_def h)
	     else
		 ( do_verbose (1, fn () => p_msg "Insert parent clause into selfq.");
		  (* Now update selfq: *)
		  insert_selfq (h, al, Bs))
	     )
	  | resolve_P_f (c as CL (h as HFUN (P, f, _, _, t), {}, nil, Bs)) =
	    (* automaton clause *)
	    if mknondet
		andalso let val Bs' = {i => {interflat B}
				      | i => B in map Bs}
			in
			    if Bs=Bs'
				then false
			    else let val conc = CL (h, {}, nil, Bs')
				 in
				     p_nondet_split_use (conc, c);
				     wait_insert conc;
				     true
				 end
			end
		then ()
	    else let val fulldefP = (dec_pdef P; fully_defined P)
		     val res_auto =		     
			 if fulldefP
			     then (new_fully_defined_ok := !new_fully_defined_ok U {P};
				   resolve_auto_def)
			 else resolve_auto
		 in
		     do_resolve_auto (c, res_auto);
		     (* Finally, update autoinfoq: *)
		     prog_rec_auto ();
		     clause_compile_auto (P, f, Bs)
		 end
	  | resolve_P_f (c as CL (h as HVAR P, {}, nil, Bs)) =
	    (* epsilon-clause *)
	    (case Bs of
		 {_ => B} => (* clause is P(x1) <= P1(x1), ..., with P1(x1) selected.
			      Resolve with all automata clauses P1(f(...)) <= ... *)
		 (* [don't use resolve_selx_def]
		   (case fully_defineds B of
			{} =>
		  *)
			  (if resolve_selx (h, B, c, c)
			       then (say_rem_subsumed_premise ();
				     h_rem_def h)
			   else (* Now update selxq, and iselxq *)
			       insert_selxq (h, B)
			   )
		 (* [don't use resolve_selx_def]
		      | Pdefs =>
			(resolve_selx_def (h, B \ Pdefs, Pdefs, c);
			 say_rem_fully_defined_parent ();
			 h_rem_def h
			  ))
		  *)
	       | _ => (* clause is just P(x): resolve with all clauses C \/ -P(...) *)
		 (let val fulldefP = (dec_pdef P; fully_defined P)
		      val res_auto =		     
			  if fulldefP
			      then resolve_auto_def
			  else resolve_auto
		      val backs = ref {}
		  in
		      (* first try to resolve with some C \/ -P (f (...))
		       with -P(f(...)) selected *)
		      (case selfq_get P of
			   SOME fmapr =>
			   (t_iter fmapr
			    (fn (f, clsr) =>
				(t_iter clsr
				 (fn ((h', al'1), Bsr') =>
				     (iterate
					let val c' = CL (h', {}, al'1, Bs')
					    fun res_2 (al' as (a' as (P', t' as f' $ _)) :: rest', acc') =
						(if P=P' andalso f=f'
						     then let val al'' = revappend (acc', rest')
							      val c'' = CL (h', {}, al'', Bs')
							      val mgu' = MGU_AUTO_X1_IS t'
							      val acu' = AC_UNIV P
							  in
							      p_auto_resolve (c'', c', [(acu', mgu')]);
							      if null al''
								  then wait_insert c''
							      else if res_auto (h', al'', nil, Bs', nil,
										c'', c')
								  then (say_rem_subsumed_premise ();
									backs := !backs U {c'})
							      else ()
							  end
						 else ();
						     res_2 (rest', a'::acc'))
					      | res_2 _ = ()
					in
					    res_2 (al'1, nil)
					end
				      | Bs' in set !Bsr'
				      end;
					false)))))
			 | _ => false);
		      iterate
			b_set_auto c' (* was b_set c'; b_set_auto is auto_back_subsume
				       in case auto_back is used.  This is used here because
				       this will also remove c' from auto_back; in
				       theory also removes clauses subsumed by c', but
				       they should have been removed already. *)
		      | c' in set !backs
		      end;
		      backs := {};
		      (* then resolve with clauses C \/ -P(x) with -P(x) selected *)
		      (case selxq_get P of
			   SOME cls =>
			   (t_iter cls
			    (fn (h', Br) =>
				(iterate
				   (let val c' = CL (h', {}, nil, {1 => B})
					val B' = B \ {P}
					val Bs' = case B' of
						      {} => {}
						    | _ => {1 => B'}
					val c'' = CL (h', {}, nil, Bs')
				    in
					(*ps_check_empty (q_skeleta B');*)
					p_auto_resolve (c'', c',
							[(AC_UNIV P,
							  MGU_AUTO_X1_IS (V 1))]);
					case h' of
					    HFUN _ => wait_insert c''
					  | _ =>
					    if empty B'
						then wait_insert c''
						    (* [don't use resolve_selx_def]
					    else if fulldefP
						then let val Pdefs = fully_defineds B'
						     in
							 resolve_selx_def (h',
									   B' \ Pdefs,
									   Pdefs,
									   c'');
							 say_rem_subsumed_premise ();
							 backs := !backs U {c'}
						     end
						     *)
					    else if resolve_selx (h', B', c'',
								  c')
						then (say_rem_subsumed_premise ();
						      backs := !backs U {c'})
					    else ()
				    end handle NoPathSetEvt => ())
				 | B in set !Br
				 end;
				   false)
			      | _ => raise ResolvePF_BadSelX))
			 | _ => false);
		      iterate
			b_set_auto c' (* was b_set c'; b_set_auto is auto_back_subsume
				       in case auto_back is used.  This is used here because
				       this will also remove c' from auto_back; in
				       theory also removes clauses subsumed by c', but
				       they should have been removed already. *)
		      | c' in set !backs
		      end;
		      backs := {};
		      prog_rec_univ ();
		      (* and backward subsume: *)
		      elim_subsumed_by_univ P;
		      (* Now update univq *)
		      univq := !univq U {P}
		  end))
	  | resolve_P_f (c as CL (h, {}, nil, Bs)) =
	    (case Bs of
		 {} => (* clause is just h. *)
		   (case h of
			HBOT _ => record_bot c
		      | HQ q =>
			(case selqq_get q of
			     SOME clr =>
			     (t_iter clr
			      (fn ((h', al'), Bsr) =>
				  (iterate
				     let val conc = CL (h', restql, al', Bs')
					 val c' = CL (h', {q} U restql, al', Bs')
				     in
					 p_q_resolve (conc, c', q);
					 wait_insert conc
				     end
				   | (restql, Bs') in set !Bsr
				   end;
				     false));
			      selqq_remove q)
			   | _ => ();
			     prog_rec_ne ();
			     (* Now update qq: *)
			     new_q (q, wait_insert)
			     )
		      | _ => raise ResolvePF_BadHead)
	       | {1 => B} => (* clause is q <= P1(x1), ..., with P1(x1) selected.
			      Resolve with all automata clauses P1(f(...)) <= ... *)
		 (* [don't use resolve_selx_def]
		 (case fully_defineds B of
		      {} =>
		  *)
			(if resolve_selx (h, B, c, c)
			     then (say_rem_subsumed_premise ();
				   h_rem_def h)
			 else (* Now update selxq and iselxq *)
			     insert_selxq (h, B)
			     )
		 (* [don't use resolve_selx_def]
		    | Pdefs =>
		      (resolve_selx_def (h, B \ Pdefs, Pdefs, c);
		       say_rem_fully_defined_parent ();
		       h_rem_def h))
		  *)
	       | _ => raise ResolvePF_BlackHole
		 )
	  | resolve_P_f _ = raise ResolvePF_BlackHole; (* remaining cases for resolve_P_f:
							should never happen. *)

        fun resolve_with_sorts_first (c as CL (h, ql, al, Bs)) =
	    let val al' = sort_simplify (al, Bs)
		val Bs' = sort_simplify_Bs Bs
	    in
		if al=al' andalso Bs=Bs'
		    then resolve_P_f c
		else let val c' = CL (h, ql, al', Bs')
			 val sigma0 = MGU_AUTO_X1_IS (V 1)
			 val wits = sort_simplify_with_witnesses (al, Bs)
			     U {(c, sigma0)
			       | c in set sort_simplify_Bs_with_witnesses (Bs, Bs')}
		     in
			 p_sort_simplify (c', c, wits);
			 prog_sort_simplify ();
			 do_fast (fn () => wait_insert c');
			 say_rem_subsumed_premise ();
			 h_rem_def h
		     end
	    end;

	val do_resolve = if sortsimplp
			     then resolve_with_sorts_first
			 else resolve_P_f

	fun restart () =
	    (univq := {}; qq := {}; t_reset selfq; t_reset selxq; t_reset selqq; botq := {};
	     t_reset autoinfoq; t_reset splitdefq;
	     t_reset partially_defined;
	     new_fully_defined := {}; new_fully_defined_ok := {};
	     t_reset deep_abbrevs
	     )

	fun resolve () =
	    (let val (dfs, cc) = scc (!predicate_graph, P_ROOT)
		 val (condensed, root) = scc_condense (!predicate_graph, P_ROOT, cc)
		 val numbering = revtopsort (condensed, root)
		 val inv_cc = overwrite [{P => low
					 | P in set preds}
					| low => preds in map cc]
		 val dfsinfo = {P => (dfsnum, ?numbering (?inv_cc P))
			       | P => dfsnum in map dfs}
		 val sccinfo = cc O inv numbering
	     in
		 dfs_info := dfsinfo;
		 scc_info := sccinfo;
		 dfs_q_info := {};
		 restart ();
		 let val (sk, bots) = compute_skeleta (!clause_list, maxpathlen)
		 in
		     skeleta := sk;
		     skel_bots := bots
		 end;
		 sure_facts := {};
	     (*
		 let val (facts, bots) = compute_witnesses (!clause_list, wantproof)
		 in
		     sure_facts := facts;
		     iterate
		       record_bot (CL (HBOT botname, {}, nil, {}))
		     | botname => up in map bots
		     end
		 end;
	      *)
		 do_verbose (3, fn () => (#put stderr "Found ";
					  print stderr (pack (card sccinfo));
					  #put stderr " strongly connected components:\n";
					  iterate
					    (#put stderr "  [";
					     print stderr (pack low);
					     #put stderr "] ";
					     let val cc = sort (fn (pred, pred') =>
								   #1 (?dfsinfo pred) > #1 (?dfsinfo pred'))
						     (?sccinfo low)
						 val delimr = ref ""
					     in
						 iterate
						   (#put stderr (!delimr);
						    delimr := ", ";
						    case pred of
							P_ROOT => #put stderr "*"
						      | P_BOT botname => #put stderr botname
						      | P_PRED P => #put stderr P)
						 | pred in list cc
						 end;
						 #put stderr "\n"
					     end)
					  | low in list sort (op <) sccinfo
					  end;
					  #put stderr "Skeleta:\n";
					  iterate
					    (#put stderr P;
					     #put stderr ": ";
					     perr_pathset (?(!skeleta) P);
					     #put stderr "\n")
					  | P in list pred_sort (!skeleta)
					    val ps = ?(!skeleta) P
					  end;
					  #flush stderr ()))
	     end;
	     let val fsig = clause_list_sig (!clause_list)
		 val ir = ref 0
	     in
		 fargsq := {f => (ir := 0;
				  (k, 1 to k, f $ [V (inc ir; !ir)
						  |while !ir<k]))
			   | f => k in map fsig}
	     end;
	     (* Now insert all (useful) clauses into waitq. *)
	     iterate
	       if useful c
		   then (let val CL (_, _, al, Bs, ...) = c
			 in
			     ps_match_al (al, ps_match_Bs (Bs, {}));
			     wait_insert c
			 end handle NoPathSetEvt => ())
	       else (p_useless c;
		     case c of (* c is useless, but we need to produce a model of it:
				just take the head to be always true. *)
			 CL (HVAR P, ...) => univq := !univq U {P}
		       | CL (HFUN (P, f, ...), ...) =>
			 (* univq := !univq U {P} *)
			 clause_compile_auto (P, f, {})
		       | _ => raise ResolveUseful)
	     | c in list !clause_list
	     end;
	     (*clause_list := nil;*)
	     (* Idea: Once all clauses have been inserted into waitq, do a first
	      round of resolution, with smash=SMASH_ONE_NEG_LIST; this
	      computes an over-approximation of the least Herbrand model,
	      by having wait_insert remove all atoms of depth>=2 except possibly
	      one in each clause. *)
	     while true do
		 let val c = ( (*check_pdef ();*)
			      wait_pop ())
		 in
		     (*p_flush ();*)
		     if ct_subsumed_try c
			 orelse ct_subsumed c
			 then (case c of
				   CL (HFUN _, {}, nil, ...) =>
				   prog_rem_subsumed_forward_auto ()
				 | _ =>
				   prog_rem_subsumed_forward ();
				   p_forw_subsume c;
				   rem_def c)
		     else (prog_pick (); p_pick c;
			   ( (* auto_back_subsume (c (*, fn () => check_pdef_except_c c *) ); *)
			    do_resolve c;
			    while not (empty (!new_fully_defined)) do
				let val fdef = !new_fully_defined
				in
				    new_fully_defined := {};
				    iterate
				      if P inset !new_fully_defined_ok
					  then (* P became fully defined because we just
						dealt with an automaton clause with head P,
						and this was the last clause with head P.
						Just remove all clauses with a P in the body
						(in selfq).  They will never be resolved on P. *)
					      iterate
						(prog_rem_fully_defined_backward ();
						 b_set_auto c (* was b_set c; b_set_auto is auto_back_subsume
							       in case auto_back is used.  This is used here because
							       this will also remove c from auto_back; in
							       theory also removes clauses subsumed by c, but
							       they should have been removed already. *)
						 )
					      | c in set P_clauses P
					      end
				      else (* P became fully defined because we erased the last
					    non-automaton clause with head P and no other clause
					    with head P was pending: we have to resolve
					    all clauses having a P in the body (in selfq) now. *)
					  iterate
					    (* inspired from the "| resolve_P_f (c as CL (h, {}, al as [_, ...], Bs)) ="
					     case of resolve_P_f, subcase "some_fully_defined_al al". *)
					    (resolve_auto_def (h, al, nil, Bs, nil, c, c);
					     say_rem_fully_defined_parent_implicit ();
					     b_set_auto c)
					  | c as CL (h, _ (* {} *), al, Bs) in set P_clauses P
					  end
				    | P in set fdef
				    end
				end;
				new_fully_defined_ok := {}
			    ))
		 end)
		 handle MHeapEmptyEvt => flush_all ()
    in
	|[ new_clause = new_clause,
	   resolve = resolve,
	   get_automaton = (fn () => (t_collect autoinfoq
				      (fn (P, fmap) =>
					  {P => t_collect fmap
					    (fn (f, ref blks) =>
						let val (k, vars, ...) = ?(!fargsq) f
						    val Bss =
							blkls_from_blocks () blks
						    val blkls =
							{blkl_from_Bs (Bsauto, k)
							| Bsauto in set Bss}
						in
						    {f => (blkls, k, vars)}
						end
						)}
					  ),
					  !univq)),
	   get_clauses = (fn () => !clause_list @ get_clauses ()),
	   get_true_botnames = (fn () => !botq)
	   ]|
    end;

fun clause_from_automaton_clause (AC_UNIV P) =
    CL (HVAR P, {}, nil, {})
  | clause_from_automaton_clause (AC_Q q) =
    CL (HQ q, {}, nil, {})
  | clause_from_automaton_clause (AC_POP (P, f, bl)) =
    let val ir = ref 0
	val Bs = {(inc ir; !ir) => B
		 | B in list bl}
	val k = len bl
	val vars = 1 to k
	val t = (ir := 0; f $ [V (inc ir; !ir)
			      | _ in list bl])
    in
	CL (HFUN (P, f, k, vars, t), {}, nil, Bs)
    end
  | clause_from_automaton_clause (AC_POP_RAW c) = c;

val matches_abbrv = da_matches;

fun clean_automaton (Pmap, umap) =
    AUTO ({P => {f => ({blkl | blkl in set blkls}, k, vars)
		| f => (blkls, k, vars) in map fmap}
	  | P => fmap in map Pmap
	    such that not (matches_abbrv P)},
	    {P | P in set umap
	     such that not (matches_abbrv P)});
