var Leak;
 
const maxleak=1, minsep=2, winlen=11, leakbound=3;
 
define des1 as
[] ([Leak] => (tlen <= maxleak) ) ;
 
define des2 as
[] ( [Leak]^[!Leak]^<Leak> => (tlen >= minsep)  ) ;
 
define concl as
 [](tlen <= winlen => tdur Leak <= leakbound) ;
 
infer
des1 &&  des2 => concl
.