Task 530b157_1 of AppWorld (H. Trivedi et al., "AppWorld: A Controllable
World of Apps and People for Benchmarking Interactive Coding Agents", ACL
2024). The task, in natural language:

    Kristin paid for the groceries. Pay her back on Venmo the amount in
    her text messages, with the note "Groceries", then send her the text
    message "It is done." (a text message, not a voice message).

The parent agent does not use the apps itself: it splits the task among
three sub-agents, in this order, and keeps the completion of the task.

    1 Messages   find the amount and the phone number of Kristin in the
                 text messages (phone tools, among them voice messages)
    2 Payment    pay Kristin on Venmo (the only one with the Venmo tools)
    3 Text       send the text message (phone tools)

Variables (Boolean), one per tool call of a sub-agent, since a call does
not say who makes it
    voice1, voice3   1 or 3 sends a voice message
    tx2              2 creates a Venmo transaction
    desc_ok          the note of the transaction is "Groceries"
    paid             the payment is done (written by the Venmo tool)
    text3            3 sends a text message
    msg_ok           the text is "It is done."
    complete         the parent marks the task complete

The contract of the parent: the rules of the user and what the user asked
for (H)
    H1   G (text3 -> paid)        the text comes after the payment
    H2   G (paid -> G !tx2)       pay once
    H3   G (tx2 -> desc_ok)       the note is "Groceries"
    H4   G (text3 -> msg_ok)      the text is "It is done."
    H5   G (!voice1 & !voice3)    no voice message
    H6   F tx2                    deliver: the payment
    H7   F text3                  deliver: the text
    H8   F complete               deliver: the task marked complete

The contracts of the sub-agents
    Messages   G !voice1 (the rule of the voice tool it holds)
    Payment    H2, H3, H6, and how the Venmo tool writes paid
    Text       from the rules of its tools: H1, H4, G !voice3
               after the quotient: also F text3, under the start
               condition that the payment is done (F paid)
    Keep       H8 (the parent)
