A problem that the result of subsumption is correct, but the final result is wrong

[DerZc]

Hi,

I find another problem in subsumption that maybe not same with #2322

The problem as below:

.decl kdof(A:unsigned, B:number)
.decl rmkg(A:number, B:number)
.decl antg(A:number, B:number, C:unsigned, D:number, E:number) magic btree
.decl ovqb(A:number, B:unsigned, C:unsigned, D:unsigned) no_magic
.decl agwv(A:unsigned, B:number)
.decl khkw(A:number, B:number, C:number, D:unsigned, E:number, F:unsigned, G:unsigned)



kdof(1, -2).
kdof(3, -6).
kdof(1, 9).
kdof(6, 10).
kdof(4, 6).
rmkg(5, 6).
rmkg(-8, 0).
rmkg(2, 9).
rmkg(-3, 8).
rmkg(3, -6).


antg(A, A, B, A, A) :- kdof(B, A), kdof(B, A).
ovqb(A^-3, C, C, C*19) :- antg(B, A, C, B, A).
agwv(B, A) :- kdof(B, A), !rmkg(A, A).
agwv(B, A1) <= agwv(B, A2) :- A1<A2.
khkw(A, A, A, B, A, B, B) :- agwv(B, A), !ovqb(A, B, B, B).

.output khkw

And the result of khkw is:

-6      -6      -6      3       -6      3       3
-2      -2      -2      1       -2      1       1
6       6       6       4       6       4       4
9       9       9       1       9       1       1
10      10      10      6       10      6       6

But the correct result of khkw should be:

-6	-6	-6	3	-6	3	3
6	6	6	4	6	4	4
9	9	9	1	9	1	1
10	10	10	6	10	6	6

If we modify the output .output khkw to .output agwv, the result of agwv is:

1       9
3       -6
4       6
6       10

So there can't be five rows in the result of khkw

[DerZc]

I tried to reduce this test case, but find if I remove the !ovqb(A, B, B, B) in last rule, the result will become correct. but I output the result of ovqb and find:

0       1       1       19
0       3       3       57
0       4       4       76
0       6       6       114

It shouldn't have influence.

Or remove the magic of antg, the result also become correct.

[DerZc]

I reduce the test case to a simpler one:

.decl kdof(A:unsigned, B:number)
.decl ovqb(A:number, B:unsigned) magic
.decl khkw(A:number, B:unsigned)

kdof(1, -2).
kdof(1, 9).

ovqb(A^-3, B) :- kdof(B, A).
kdof(B, A1) <= kdof(B, A2) :- A1<A2.
khkw(A, B) :- kdof(B, A), !ovqb(A, B).

.output khkw

The result is:

-2      1
9       1

But if I remove the magic, it can produce the correct result:

9       1

But the result of kdof is correct, whether there is maigc.