Yes, I think I know what you mean... it just feels as if there must be an easy technical proof, but, I can't find it...

So I tried to change the solution again, to make the proof easier:

def U(): Enumerate proofs by length up to a very large N if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5" then return (A()==1 ? 5 : 0) Enumerate proofs by length up to a very large N if found any other proof of the form "A()==a implies U()==u, and A()!=a implies U()<=u" then return (A()==a ? u-1 : u+1) return (A()==2 ? 10 : 0)

With this, Provable(S) implies S directly, so S is provable, so A must find it, because there are no other short-proof moral arguments if A an U are consistent.

But the provability of S does not depend on A, so U() will never get past the first loop, no matter against which agent it is played. So this is a wrong solution to the original problem. And the previous one would be wrong for the same reason, even if I did find the proof...