OrdC 1 is with_binary_products