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
not counted, because Redlog considers those to be not atomic formulas but
rlatnum(a = 0 or (b = 0 and b = 0));
rlatnum(a = 0 and true);
- rlatl — list of atomic formulas