rlatnum – number of atomic formulas

## Calling Sequence

rlatnum \((\,\varphi\,)\)

## Arguments

\(\varphi\) | — | first-order formula |

## Returns

\(n\) | — | integer |

## Description

Count the number of atomic formulas occurring in \(\varphi\) including multiplicities. This is often used as an indicator for the size of a formula. For determining, in contrast, the number of different atomic formulas use rlatl in combination with length.

Occurrences of the truth values `true`

and `false`

are
not counted, because Redlog considers those to be not atomic formulas but
logical constants.

## Examples

```
rlatnum(a = 0 or (b = 0 and b = 0));
```

rlatnum(a = 0 and true);

## See Also

- rlatl — list of atomic formulas