[Termtools] Question on AC rewriting in TermComp

Hello. When a symbol is declared AC in the TRS format, which relation is (dis)proved terminating? Is it rewriting with matching modulo AC or rewriting modulo AC, i.e. rewriting on AC-classes?