There was a minor bug in the previous numbers. knuth-bendix had the wrong curry unknown. Here is the correct entry: curry unknown curry known knuth-bendix 166,541,352 16,502