Solution (source code)

= Solution

Reading the <abstract syntax tree> recursively gives the eight distinct <subformulas>
$$
\boxed{A,\ B,\ C,\ \neg A,\ \neg B,\ C\to\neg A,\ \neg B\land(C\to\neg A),\ A\lor(\neg B\land(C\to\neg A)).}
$$
A <subformula> includes the complete <propositional formula> itself as well as the operands of its connectives. There are nine occurrences in the <abstract syntax tree>, because the atomic formula $A$ occurs twice, but only eight different <propositional formulas> in the set.