:- dynamic lt/2,j/3.

name(l).

dom(x). dom(y). dom(u). dom(z). dom(v). dom(w). 

_ axiom assump : (true => j(x,y,u),j(u,z,v),j(y,z,w)). 
_ axiom goal_ax  : (j(x,w,V),lt(v,V),lt(V,v) => goal).           
 
_ axiom lt_refl(X) : (dom(X) => lt(X,X)).
_ axiom lt_trans(X,Y,Z) : (lt(X,Y),lt(Y,Z) => lt(X,Z)).
_ axiom ub_join(X,Y,Z) : (j(X,Y,Z) => lt(X,Z),lt(Y,Z)).
_ axiom lub_join(X,Y,Z,U) : (j(X,Y,Z),lt(X,U),lt(Y,U) => lt(Z,U)).
_ axiom lt_j(X,Y) : (lt(X,Y) => j(X,Y,Y)).
_ axiom commute_j(X,Y,Z) : (j(X,Y,Z) => j(Y,X,Z)).
_ axiom up_latt(X,Y) : (dom(X),dom(Y) => dom(U),j(X,Y,U)).