axiom:* *->Ab<A>a A->BD B->[bda,9] C->[babc,9] D->[Cba,4]