%   Theorem = dia box p<=>dia box dia box p.

predicates([p,acc]).
precedence([:,::,o,accf,sk1,sk2,sk3,sk4,sk5,sk6,p,acc]).

%   Skolem-functions([o,sk1,sk2,sk3,sk4,sk5,sk6]).

acc((sk1::accf):o,X2),acc((sk2::accf):o,X4),acc((sk3(X4)::accf):X4,X6) -> p(X2),p(X6).
acc(o,X7),p((sk4(X7)::accf):X7),acc(o,X9),acc((sk5(X9)::accf):X9,X11),p((sk6(X11,X9)::accf):X11) -> [].
acc(o,X13).
acc(X14,X14).
acc(X15,X16) -> acc(X15,(X17::accf):X16).