let is_BS (clause: clause) : bool =
  List.for_all
    (fun literal ->
       match literal.atom with
         | Var _ ->
             failwith "Term.is_BS"
               
         | Const _ ->
             true
               
         | Func func ->
             Tools.array_for_all
               (fun term ->
                  match term with
                    | Var _
                    | Const _ ->
                        true
                          
                    | Func _ ->
                        false
               )
               func.subterms
    )
    clause