let is_Horn (clause: literal list) : bool =
let rec is_horn' (clause: literal list) (pos_count: bool) : bool =
match clause with
| [] ->
true
| literal :: tail ->
if literal.sign then begin
if pos_count then
false
else
is_horn' tail true
end
else
is_horn' tail pos_count
in
is_horn' clause false