synthesise believes(B, recentlySaid(A, (B, Nb)))
display %1
display %2
display %3
display %4
select %3
display

declare nonce Nb

synthesise %1
display %1
display %2
display %3
select %2
display

mark assumption %1
display

synthesise %0
display %1
display %2
display %3
display %4
select %4
display

substitute phi3 recentlySaid(S, said(A, (B, Nb)))
display

mark assumption %1
display

synthesise %0
display %1
display %2
display %3
display %4
select %2
display

csubstitute C2 Cbs
display

mark assumption %0
mark assumption %2
mark assumption %3
mark goal %4
display

synthesise %5
display %1
display %2
display %3
display %4
select %3
display

csubstitute C4 Cas
mark assumption %6
mark assumption %7
display

save