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