% preservation of the Diamond Property under reflexive closure
% r rewrite relation, e equality, re reflexive closure of r

fof(assump,axiom, (((re(a, b) & re(a, c))))).
fof(goal_ax,axiom, ! [A]:((re(b, A) & re(c, A)) => ((goal)))).
fof(ref_e,axiom, ! [A]:(((e(A, A))))).
fof(sym_e,axiom, ! [A, B]:((e(A, B)) => ((e(B, A))))).
fof(congl,axiom, ! [A, B, C]:((e(A, B) & re(B, C)) => ((re(A, C))))).
fof(e_in_re,axiom, ! [A, B]:((e(A, B)) => ((re(A, B))))).
fof(r_in_re,axiom, ! [A, B]:((r(A, B)) => ((re(A, B))))).
fof(e_or_r,axiom, ! [A, B]:((re(A, B)) => ((e(A, B)) | (r(A, B))))).
fof(dp_r,axiom, ! [A, B, C]:((r(A, B) & r(A, C)) => (? [D] : (r(B, D) & r(C, D))))).
fof(goal_to_be_proved,conjecture,goal).