Two-Variable Logic with Counting and Trees

We consider the two-variable logic with counting quantifiers (C²) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C² and it is no longer a fragment of the first order logic. In particular, it can express that a structure is a ranked tree, a cycle or a connected graph of bounded degree. It is also strictly more expressive than the first-order logic with two variables and two successor relations of two finite linear orders. We give a decision procedure for the satisfiability problem for this logic. The procedure runs in NEXPTIME, which is optimal since the satisfiability problem for plain C² is NEXPTIME-complete.