((p100/\~p101)/\(((((p101->p100)/\(p102->p101))/\((p100->((p0->[](p100->p0))/\(~p0->[](p100->~p0))))/\(p101->((p1->[](p101->p1))/\(~p1->[](p101->~p1))))))/\((p100/\~p101)->(<>((p101/\~p102)/\p1)/\<>((p101/\~p102)/\~p1))))/\[]((((p101->p100)/\(p102->p101))/\((p100->((p0->[](p100->p0))/\(~p0->[](p100->~p0))))/\(p101->((p1->[](p101->p1))/\(~p1->[](p101->~p1))))))/\((p100/\~p101)->(<>((p101/\~p102)/\p1)/\<>((p101/\~p102)/\~p1))))))