<2> (a1\/(<3> (b1\/[5](a1\/b1)) /\ ~<4> (b1\/[5](a1\/b1)))) /\ ~<3> (a1\/(<3>(b1\/[5](a1\/b1))/\~<4>(b1\/[5](a1\/b1))))