%theorem(all(x,box p(x)) <=> box all(x,p(x))).
logic(k).
translation(relational).
domain(decreasing).
%outputfile('k1.s').
outputfile('k.s').