goals_limit := 1; Unify.search_bound := 40; Unify.trace_bound := 40; with_paths ["J", "JVM", "BV"] use_thy "Digest";