Require length-in-conclusion form for strings inferences (#5953)

Require length-in-conclusion form for strings inferences (#5953)

Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.

It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.

Fixes #5940.

Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.