Distributivity check in Prolog

Suppose I have an equivalence relation eq, and multiple binary operators o_1, o_2, ... o_n. I want to find out which operations distribute over others. Assuming that I have a knowledge base that can determine whether two expressions are equivalent, a simple solution is to just enter all possible queries :

(for left-distributivity)

?- eq(o_1(Z,o_1(X,Y)),o_1(o_1(Z,X),o_1(Z,Y))). 
?- eq(o_1(Z,o_2(X,Y)),o_2(o_1(Z,X),o_1(Z,Y))). 
?- eq(o_1(Z,o_3(X,Y)),o_3(o_1(Z,X),o_1(Z,Y))). 

...

?- eq(o_2(Z,o_2(X,Y)),o_2(o_2(Z,X),o_2(Z,Y))). 
?- eq(o_2(Z,o_3(X,Y)),o_3(o_2(Z,X),o_2(Z,Y))). 

...

?- eq(o_n(Z,o_n(X,Y)),o_n(o_n(Z,X),o_n(Z,Y))).

but there must be better ways to do this. For starters, I'd like to define a predicate left_dist such that left_dist(o_m,o_k) would generate the corresponding query for me. I initially thought I'd do this by using call, as in

left_dist(O_m,O_k) :-
   eq(call(O_m,Z,call(O_k,X,Y)),call(O_k,call(O_m,Z,X),call(O_m,Z,Y))).

but the nested calls do not work for reasons outlined in this question, and I guess it's not a good way to approach Prolog programming either.

So the question is : how can I define left_dist, or otherwise simplify the queries above, in Prolog?

Left distributivity means that for all x,y,z: x*(y+z)=(x*y)+(x*z)

Now you do not mention concrete domains, so I assume that all relations know them already. This assumes that Add_3 and Mult_3 always terminate.

not_left_dist(Mult_3, Add_3) :-
   call(Add_3, Y, Z, YZ),
   call(Mult_3, X, YZ, LHS),
   call(Mult_3, X, Y, XY),
   call(Mult_3, X, Z, XZ),
   call(Add_3, XY, XZ, RHS),
   neq(LHS, RHS).

left_dist(Mult_3, Add_3) :-
   iwhen(ground(Mult_3+Add_3), \+ not_left_dist(Mult_3, Add_3) ).

This uses iwhen/2.