Hi there,
also thanks from my side to Florian for running the competition.
and some REJECT (I don't ... https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/526)
Here is what I see in the proof of Waldmann_23/size-10-alpha-2-num-58.ari
there is the following rule (among others)
b1 (b1 (b1 (b1 (b0 (a0 (x)))))) -> b1 (b1 (b0 (x)))
this is labeled according to CeTA (when instantiating x by 0)
b13(b13(b13(b12(b00(a00(x)))))) -> b13(b12(b00(x)))
using the following interpretation that is given in certificate
[a0(x1)] = 4*x1 + 0 (mod 4) = 0 [a1(x1)] = 4*x1 + 1 (mod 4) = 1 [b0(x1)] = 4*x1 + 2 (mod 4) = 2 [b1(x1)] = 4*x1 + 3 (mod 4) = 3
When calculating this by hand it looks correct to me, though there might be some misunderstanding in the labeling function: when working with carrier {0,..,3}, so everything is "mod 4", there is no point in adding 4*x1 in the interpretations. Perhaps this is the problem???
Nevertheless, Matchbox produces the following labeled rule (when instantiating x by 0)
b10(b10(b10(b11(b03(a00(x)))))) -> b10(b11(b00(x)))
which seems to have used a different interpretation. Therefore, CeTA complains at this step.
Best, René