You mean, the U’, for which U’(A()) is provably equal to U() depends on the order in which you enumerate U’-s? Hmm, counterintuitive, but it makes sense… A() with a different order would be a different A(), so it would produce a different U’...
Just as a wild shot, what would happen if you try every possible ordering of U’-s and then choose the ordering that produces the best result? Let’s say there is a maximal length for U’ that you are willing to consider, and you have a loop iterating over all possible orderings of U’-s of up to that length. In each iteration of the loop you try to prove things in the specific order, find the argmax, store it, restore the proof system back to its initial state, and go to the next iteration. When everything finishes, use the best found ordering.
I expect, the results will now depend on the order in which the orderings are considered...
You mean, the U’, for which U’(A()) is provably equal to U() depends on the order in which you enumerate U’-s? Hmm, counterintuitive, but it makes sense… A() with a different order would be a different A(), so it would produce a different U’...
Just as a wild shot, what would happen if you try every possible ordering of U’-s and then choose the ordering that produces the best result? Let’s say there is a maximal length for U’ that you are willing to consider, and you have a loop iterating over all possible orderings of U’-s of up to that length. In each iteration of the loop you try to prove things in the specific order, find the argmax, store it, restore the proof system back to its initial state, and go to the next iteration. When everything finishes, use the best found ordering.
I expect, the results will now depend on the order in which the orderings are considered...
[EDIT: Yes, this is stupid. Please disregard]