AG ( (<usr2_ai3_re5><ai3_re5><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_re3><ai3_re3><usr1_ni1_ne1><usr2_ai3_ce3>true & <usr2_ai3_re4><error>true) => <usr2_ai3_re5><ai3_re5>(<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true & <ai3_ce5><error>true) )
AG ( (<usr2_ai3_re2><ai2_VoidReply>true) => <usr2_ai3_re1><ni1_ne1__ai2_VoidReply>(<ai3_ce5><error>true & <ai4_ce1><usr2_ai4_ce1>true) )
AG ( (<usr3_ai1_re1><ai2_re1><ai3_ce5><usr2_ai3_ce5>true & <usr3_ai1_re1><ai2_re1><usr1_ni1_ne1><usr2_ai3_ce3>true) => <usr3_ai1_re1><ai2_re1>(<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true & <ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<ai4_ce2><usr2_ai4_ce2><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <ai3_ce5><usr2_ai3_ce5>true) => <ai3_ce8><usr2_ai3_ce8>(<usr2_ai3_re2><ai3_re2><ai4_ce2><usr2_ai4_ce2><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_re2><ai3_re2><ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <ai3_ce5><error>true) => <ai3_ce7><usr2_ai3_ce7>(<usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_VoidReply><ai3_VoidReply><ai3_ce5><error>true) )
AG ( (<usr2_ai3_re1><none>true & <usr2_ai3_re2><ni1_ne2>true) => <usr2_ai3_re1><none>(<ai3_ce5><error>true & <ai4_ce1><usr2_ai4_ce1>true) )
AG ( (<usr3_ai1_re1><ai2_VoidReply><ai3_ce5><usr2_ai3_ce5>true & <usr3_ai1_re1><ai2_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) => <usr3_ai1_re1><ai2_VoidReply>(<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true & <ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<usr3_ai1_re1><ai4_VoidReply><ai3_ce5><usr2_ai3_ce5>true & <usr3_ai1_re1><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true) => EF (<usr2_ai4_re2><ai4_VoidReply><ai3_ce5><usr2_ai3_ce5>true & <usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true) )
AG ( (<usr2_ai3_re4><ai3_re4><ai3_ce5><usr2_ai3_ce5>true & <usr2_ai3_re5><error>true & <usr2_ai3_re3><ai3_re3><ai4_ce2><usr2_ai4_ce2><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true) => <usr2_ai3_re3><ai3_re3>(<ai4_ce2><usr2_ai4_ce2><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<ai3_ce5><error>true & <ai4_ce1><usr2_ai4_ce1><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) => <ai4_ce1><usr2_ai4_ce1>(<usr2_ai4_re2><ai4_VoidReply><ai3_ce5><error>true & <usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) )
AG ( (<usr2_ai2_re2><ai2_re2><ai3_ce5><usr2_ai3_ce5>true & <usr2_ai2_re3><ai2_re3><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) => EF (<usr2_ai3_VoidReply><ai3_VoidReply><ai3_ce5><error>true & <usr2_ai3_VoidReply><ai3_VoidReply><ai4_ce1><usr2_ai4_ce1><usr2_ai4_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) )
AG ( (<usr2_ai2_VoidReply><error>true & <usr2_ai4_re2><error>true) => EF (<usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_VoidReply><ai3_VoidReply><ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true & <usr2_ai3_VoidReply><ai3_VoidReply><ai3_ce5><usr2_ai3_ce5>true) => EF (<usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <usr2_ai3_VoidReply><ai3_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_VoidReply><ai3_VoidReply><ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<usr2_ai2_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <usr2_ai2_re3><ai2_re3><ai3_ce5><usr2_ai3_ce5>true) => <usr2_ai2_re1><usr3_ai1_ce1>(<usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><ai3_ce5><usr2_ai3_ce5>true & <usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true) )
AG ( (<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true & <ai3_ce5><usr2_ai3_ce5>true) => <ai2_ce2><usr2_ai2_ce2>(<usr2_ai2_re2><ai2_re2><ai3_ce5><usr2_ai3_ce5>true & <usr2_ai2_re3><ai2_re3><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true) )
AG ( (<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <ai3_ce5><usr2_ai3_ce5>true) => <ai3_ce8><usr2_ai3_ce8>(<usr2_ai3_re1><ai3_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><ni1_ne2>true & <usr2_ai3_re1><ai3_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><ni1_ne1>true & <usr2_ai3_re2><ai3_re2><ai3_ce5><usr2_ai3_ce5>true) )
AG ( (<usr3_ai1_re1><ai4_VoidReply><ai3_ce5><error>true & <usr3_ai1_re1><ai4_VoidReply><usr1_ni1_ne1><usr2_ai3_ce3>true) => <usr3_ai1_re1><ai4_VoidReply>(<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re1><none>true & <ai3_ce5><error>true) )
AG ( (<usr2_ai3_re1><none>true & <usr2_ai3_re2><ni1_ne2>true) => <usr2_ai3_re2><ni1_ne2>(<ai3_ce5><error>true & <ai4_ce1><usr2_ai4_ce1>true) )
AG ( (<usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true & <ai3_ce5><error>true) => <ai3_ce6><usr2_ai3_ce6>(<usr2_ai3_re1><ai3_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true & <usr2_ai3_re2><ai3_re2><ai3_ce5><error>true) )
AG ( (<usr2_ai2_re1><usr3_ai1_ce1><usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true & <usr2_ai2_re3><ai2_re3><ai3_ce5><error>true) => <usr2_ai2_re1><usr3_ai1_ce1>(<usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><ai3_ce5><error>true & <usr3_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr2_ai3_ce3><usr2_ai3_re2><none>true) )
