AG ( (<usr1_ai1_VoidReply><usr3_ai3_ce2><usr3_ai3_re5><ai2_VoidReply>true) => <usr1_ai1_VoidReply><usr3_ai3_ce2>(<usr3_ai3_re5><ai2_VoidReply><ai3_ce3><error>true) )
AG ( (<usr3_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><ai1_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2>true & <usr3_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><ai1_VoidReply><ai3_ce3><error>true) => <usr3_ai1_VoidReply><usr2_ai1_ce1>(<usr2_ai1_re1><ai1_VoidReply><ai3_ce3><error>true & <usr2_ai1_re1><ai1_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><ni1_ne1>true) )
AG ( (<usr1_ni1_ne1><usr3_ai3_ce2>true & <ai3_ce3><usr3_ai3_ce4>true) => <ai3_ce3><usr3_ai3_ce4>(<usr3_ai3_re3><ai3_re3><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true) )
AG ( (<usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true & <ai3_ce3><usr3_ai3_ce4>true) => <ai4_ce1><usr4_ai1_ce1>(<usr4_ai1_VoidReply><usr3_ai4_ce1><usr3_ai4_re2><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true & <usr4_ai1_VoidReply><usr3_ai4_ce1><usr3_ai4_re2><ai4_VoidReply><ai3_ce3><usr3_ai3_ce4>true) )
AG ( (<ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <ai3_ce3><usr3_ai3_ce4>true) => <ai4_ce1><usr4_ai1_ce1>(<usr4_ai1_VoidReply><usr3_ai4_ce1><usr3_ai4_re1><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><ai3_ce3><usr3_ai3_ce4>true & <usr4_ai1_VoidReply><usr3_ai4_ce1><usr3_ai4_re1><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<usr4_ai1_VoidReply><ai3_re1><ai3_ce3><usr3_ai3_ce4>true & <usr4_ai1_VoidReply><ai3_re1><ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2>true) => <usr4_ai1_VoidReply><ai3_re1>(<ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <ai3_ce3><usr3_ai3_ce4>true) )
AG ( (<usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><ai3_ce3><error>true & <usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) => <usr3_ai2_VoidReply><usr2_ai1_ce1>(<usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><ai3_ce3><error>true & <usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<usr4_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <usr4_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><ai3_ce3><usr3_ai3_ce4>true) => EF (<usr3_ai2_re2><ai2_re2><ai3_ce3><usr3_ai3_ce4>true & <usr3_ai2_re2><ai2_re2><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true) )
AG ( (<usr3_ai3_re2><ai3_re2><ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <usr3_ai3_re2><ai3_re2><ai3_ce3><error>true) => <usr3_ai3_re1><usr4_ai1_ce1>(<usr4_ai1_VoidReply><ai3_re1><ai3_ce3><error>true & <usr4_ai1_VoidReply><ai3_re1><ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<usr3_ai2_re2><ai2_re2><ai3_ce3><usr3_ai3_ce4>true & <usr3_ai2_re2><ai2_re2><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true) => <usr3_ai2_re2><ai2_re2>(<usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true & <ai3_ce3><usr3_ai3_ce4>true) )
AG ( (<usr2_ai1_re1><ai2_re1><ai3_ce3><error>true & <usr2_ai1_re1><ai2_re1><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><none>true) => EF (<usr3_ai3_re6><ni1_ne2__ai1_VoidReply><ai3_ce3><error>true & <usr3_ai3_re5><ai1_VoidReply>true) )
AG ( (<usr3_ai3_re5><ni1_ne1__ai2_VoidReply>true) => <usr3_ai3_re6><ai2_VoidReply>(<ai2_ce2><usr3_ai2_ce2>true & <ai3_ce3><error>true) )
AG ( (<usr2_ai1_re1><ai4_VoidReply><ai3_ce3><error>true & <usr2_ai1_re1><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><ni1_ne1>true) => EF (<usr3_ai4_re2><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re6><ni1_ne2>true & <usr3_ai4_re2><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><ni1_ne1>true & <usr3_ai4_re2><ai4_VoidReply><ai3_ce3><error>true) )
AG ( (<usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><ai3_ce3><usr3_ai3_ce4>true & <usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_re1><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><ni1_ne1>true) => EF (<usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><ai3_ce3><usr3_ai3_ce4>true & <usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <ai3_ce3><usr3_ai3_ce4>true) => <ai3_ce3><usr3_ai3_ce4>(<usr3_ai3_re3><ai3_re3><ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2>true & <ai3_ce3><usr3_ai3_ce4>true) => <ai2_ce3><usr3_ai2_ce3>(<usr3_ai2_re2><ai2_re2><ai3_ce3><usr3_ai3_ce4>true & <usr3_ai2_re2><ai2_re2><ai2_ce2><usr3_ai2_ce2><usr3_ai2_VoidReply><usr2_ai1_ce1><usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><ni1_ne1>true) )
AG ( (<usr3_ai3_re6><ni1_ne2__ai2_re1>true) => <usr3_ai3_re5><ai2_re1>(<ai2_ce2><usr3_ai2_ce2>true & <ai3_ce3><error>true) )
AG ( (<usr3_ai3_re5><ni1_ne1__ai4_VoidReply>true) => <usr3_ai3_re6><ni1_ne2__ai4_VoidReply>(<ai2_ce2><usr3_ai2_ce2>true & <ai3_ce3><usr3_ai3_ce4>true) )
AG ( (<ai1_ce2><error>true & <usr3_ai2_re2><error>true & <usr2_ai1_re1><error>true) => EF (<usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><ai3_ce3><usr3_ai3_ce4>true & <usr2_ai1_re1><usr1_ai1_ce1><usr1_ai1_VoidReply><ai4_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) )
AG ( (<usr2_ai1_re1><ai2_VoidReply><ai3_ce3><error>true & <usr2_ai1_re1><ai2_VoidReply><usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true) => <usr2_ai1_re1><ai2_VoidReply>(<usr1_ni1_ne1><usr3_ai3_ce2><usr3_ai3_re5><none>true & <ai3_ce3><error>true) )
