Maude> (search)
1 : N(princ-msg A & princ-msg B & encrypt pkB(nonce-msg F1 & princ-msg A)),START-2 B,T_initiator_Init2 A F0,F0 B F1
2 : N(princ-msg B & princ-msg A & encrypt pkA(nonce-msg F1 & nonce-msg F3)),T_initiator_Init2 A F0,T_responder_Resp2 B F2,
    F0 B F1,F2 A F3
3 : N(princ-msg A & princ-msg B & encrypt pkB(nonce-msg F3)),TERMINATED-1 A,T_responder_Resp2 B F2,F2 A F3
4 : TERMINATED-1 A,TERMINATED-2 B

Maude> (search !)
1 : TERMINATED-1 A,TERMINATED-2 B