Or maybe program synthesis combined by LLMs might be the way?
It does seem like the Cyc people hit the wall with simply collecting facts. Having to have a human in the loop.
The problem I think is if you have LLMs figuring out the propositions, the whole system is just as prone to garbage-in-garbage-out as LLMs are.