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