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