Hello. I wonder what is the semantics of higher-order rewriting used in the competition. I cannot find this specified anywhere. Precisely: what is the theory used for matching? Alpha-conversion only? Or alpha-beta-eta? Thanks. Frederic.