%UG

| ?- listing.
become_effective(offer(A,B,C), D) :-
        reach(offer(A,B,C), B, D),
        \+become_effective(withdrawl(A,B,offer(A,B,C)),B,_),
        \+become_effective(revocation(A,B,offer(A,B,C)),B,_).
become_effective(acceptance(A,B,C), D) :-
        become_effective(offer(B,A,_), _),
        dispatch(acceptance(A,B,C), B, _),
        reach(acceptance(A,B,C), B, D).

become_effective(withdrawl(A,B,offer(A,B,C)), B, D) :-
        irrevocable(offer(A,B,C)),
        reach(withdrawl(A,B,offer(A,B,C)), B, D),
        \+ (reach(offer(A,B,C),B,E),before(E,D)).
become_effective(revocation(A,B,offer(A,B,C)), B, D) :-
        \+irrevocable(offer(A,B,C)),
        reach(revocation(A,B,offer(A,B,C)), B, D),
        (   \+dispatch(acceptance(B,A,E),A,F)
        ;   dispatch(acceptance(B,A,E), A, F),
            before(D, F)
        ).

before(A, B) :-
        A@<B.

dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), anzai, t0410).

is_concluded(contract(A,B,C), D) :-
        become_effective(acceptance(B,A,offer(A,B,C)), D).

reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')), bernard, t0408).
reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), bernard, t0409).
reach(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), anzai, t0410).

yes
| ?- is_concluded(X,T).
no
| ?- trace.
% The debugger will first creep -- showing everything (trace)
yes
% trace
| ?- is_concluded(X,T).
        1      1 Call: is_concluded(_463,_483) ?
        2      2 Call: become_effective(acceptance(_1106,_1105,offer(_1105,_1106,_1107)),_483) ?
        3      3 Call: become_effective(offer(_1105,_1106,_1773),_1776) ?
        4      4 Call: reach(offer(_1105,_1106,_1773),_1106,_1776) ?
        4      4 Exit: reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')),bernard,t0408) ?
        5      4 Call: become_effective(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2497) ?
        6      5 Call: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ?
        6      5 Fail: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ? 
        5      4 Fail: become_effective(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2497) ?
        7      4 Call: become_effective(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2483) ?
        8      5 Call: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ?
        8      5 Fail: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ?
        9      5 Call: reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2483) ?
        9      5 Exit: reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,t0409) ?
       10      5 Call: dispatch(acceptance(bernard,anzai,_4668),anzai,_4672) ?
       10      5 Exit: dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410) ?
       11      5 Call: dispatch(acceptance(bernard,anzai,_4668),anzai,_4672) ?
       11      5 Exit: dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410) ?
       12      5 Call: before(t0409,t0410) ?
       13      6 Call: t0409@<t0410 ?
       13      6 Exit: t0409@<t0410 ?
       12      5 Exit: before(t0409,t0410) ?
        7      4 Exit: become_effective(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,t0409) ?
        3      3 Fail: become_effective(offer(_1105,_1106,_1773),_1776) ?
        2      2 Fail: become_effective(acceptance(_1106,_1105,offer(_1105,_1106,_1107)),_483) ?
        1      1 Fail: is_concluded(_463,_483) ?
no
% trace
| ?-

/* %%HY
取消効力発生により「契約不成立」が証明されましたね。おめでとう。
しかし、その理由には若干問題があります。
取消効力発生の効果は「申込効力不発生」で良いのでしょうか。もう一度考えてみて下さい。
*/