([ack_in](s(1),s(2)) >= [u21](ack_in(s(1),2),1) /\  /\ [ack_in](s(1),s(2)) >= [ack_in](s(1),2) /\ [u21](ack_out(2),1) >= [ack_in](1,2) /\ [ack_in](s(1),0) >= [ack_in](1,s(0)) /\
ack_in(0,2) >= ack_out(s(2)) /\  /\ ack_in(s(1),0) >= u11(ack_in(1,s(0))) /\ ack_in(s(1),s(2)) >= u21(ack_in(s(1),2),1) /\ u11(ack_out(2)) >= ack_out(2) /\ u21(ack_out(2),1) >= u22(ack_in(1,2)) /\ u22(ack_out(2)) >= ack_out(2) /\
([ack_in](s(1),s(2)) > [u21](ack_in(s(1),2),1) \/  \/ [ack_in](s(1),s(2)) > [ack_in](s(1),2) \/ [u21](ack_out(2),1) > [ack_in](1,2) \/ [ack_in](s(1),0) > [ack_in](1,s(0)))) /\


 /\


([u21](ack_out(2),1) >= [u22](ack_in(1,2)) /\  /\
ack_in(0,2) >= ack_out(s(2)) /\  /\ ack_in(s(1),0) >= u11(ack_in(1,s(0))) /\ ack_in(s(1),s(2)) >= u21(ack_in(s(1),2),1) /\ u11(ack_out(2)) >= ack_out(2) /\ u21(ack_out(2),1) >= u22(ack_in(1,2)) /\ u22(ack_out(2)) >= ack_out(2) /\
([u21](ack_out(2),1) > [u22](ack_in(1,2)) \/ )) /\


([ack_in](s(1),0) >= [u11](ack_in(1,s(0))) /\  /\
ack_in(0,2) >= ack_out(s(2)) /\  /\ ack_in(s(1),0) >= u11(ack_in(1,s(0))) /\ ack_in(s(1),s(2)) >= u21(ack_in(s(1),2),1) /\ u11(ack_out(2)) >= ack_out(2) /\ u21(ack_out(2),1) >= u22(ack_in(1,2)) /\ u22(ack_out(2)) >= ack_out(2) /\
([ack_in](s(1),0) > [u11](ack_in(1,s(0))) \/ ))