AG ( (<usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne3><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ni1_ne5><usr2_ai1_ce1>true) => <ai1_ce1><usr1_ai1_ce1>(<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true & <usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne5><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ni1_ne6><error>true) => EF (<usr1_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><usr2_ai1_ce1>true) )
AG ( (<usr1_ni1_ne6><error>true) => EF (<usr1_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ni1_ne6><usr2_ai1_ce1>true) => <usr1_ni1_ne4><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ni1_ne6><usr2_ai1_ce1>true) => <usr1_ni1_ne6><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ai1_VoidReply><ni1_ne3__ai1_VoidReply><usr1_ni1_ne6><usr2_ai1_ce1>true) => EF (<usr1_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><usr2_ai1_ce1>true) )
AG ( (<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne2><none>(<usr1_ai1_VoidReply><ni1_ne2__ai1_VoidReply><usr1_ni1_ne5><usr2_ai1_ce1>true) )
AG ( (<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><usr2_ai1_ce1>true) => <usr1_ai1_VoidReply><ai1_VoidReply>(<usr1_ni1_ne6><usr2_ai1_ce1>true & <usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne3><none>(<usr1_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ni1_ne6><usr2_ai1_ce1>true) => <ai1_ce2><usr1_ai1_ce2>(<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true & <usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ni1_ne6><usr2_ai1_ce1>true & <usr1_ni1_ne5><ni1_ne5>true) => <usr1_ni1_ne3><ni1_ne3>(<usr1_ni1_ne6><usr2_ai1_ce1>true & <usr1_ni1_ne5><usr2_ai1_ce1>true) )
AG ( (<usr1_ni1_ne6><ni1_ne6>true & <usr1_ni1_ne5><usr2_ai1_ce1>true) => <ai1_ce1><usr1_ai1_ce1>(<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true & <usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne5><none>(<usr1_ai1_VoidReply><usr2_ai1_ce1><usr2_ai1_VoidReply><ai1_VoidReply><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ai1_VoidReply><ni1_ne4__ai1_VoidReply>true) => <usr1_ai1_VoidReply><ni1_ne4__ai1_VoidReply>(<usr1_ni1_ne6><usr2_ai1_ce1>true & <usr1_ni1_ne5><usr2_ai1_ce1>true) )
AG ( (<usr1_ni1_ne6><usr2_ai1_ce1>true) => <usr1_ni1_ne2><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne5><ni1_ne5>true) )
AG ( (<usr1_ai1_VoidReply><ni1_ne5__ai1_VoidReply>true) => <usr1_ai1_VoidReply><ni1_ne5__ai1_VoidReply>(<usr1_ni1_ne6><ni1_ne6>true & <usr1_ni1_ne5><usr2_ai1_ce1>true) )
AG ( (<usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ni1_ne1><usr2_ai1_ce1>(<usr2_ai1_VoidReply><none><usr1_ni1_ne6><ni1_ne6>true) )
AG ( (<usr1_ai1_VoidReply><ni1_ne6__ai1_VoidReply><usr1_ni1_ne5><usr2_ai1_ce1>true) => <usr1_ai1_VoidReply><ni1_ne6__ai1_VoidReply>(<usr1_ni1_ne6><usr2_ai1_ce1>true & <usr1_ni1_ne5><usr2_ai1_ce1>true) )
