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

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder