Verbose level: 1 Formula AG((p7 IMPLIES EF(~p7))) holds Encoding time: 0.002 sec Verification time: 0.016 sec Encoding memory: 9.762 MB Memory (total): 23.39 MB TOTAL time: 0.018 sec STAT; 0.002 ; 0.016 ; 9.762 ; 23.39 ; 0.018