warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu1: Depth=      27 States=   1e+06 Transitions= 1.70547e+06 Memory= 0.000    
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu3: Depth=      27 States=   1e+06 Transitions= 1.70678e+06 Memory= 0.000    
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu0: Depth=      21 States=   1e+06 Transitions= 1.04189e+06 Memory= 384.654  
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu2: Depth=      21 States=   1e+06 Transitions= 1.03686e+06 Memory= 0.000    
cpu1: Depth=      27 States=   2e+06 Transitions= 3.4118e+06 Memory= 0.000    
cpu3: Depth=      27 States=   2e+06 Transitions= 3.38686e+06 Memory= 0.000    
cpu1: Depth=      27 States=   3e+06 Transitions= 5.04729e+06 Memory= 0.000    
cpu3: Depth=      27 States=   3e+06 Transitions= 5.05868e+06 Memory= 0.000    
cpu0: Depth=      21 States=   2e+06 Transitions= 2.07658e+06 Memory= 384.654  
cpu2: Depth=      21 States=   2e+06 Transitions= 2.08167e+06 Memory= 0.000    
cpu1: Depth=      27 States=   4e+06 Transitions= 6.72021e+06 Memory= 0.000    
cpu3: Depth=      27 States=   4e+06 Transitions= 6.68241e+06 Memory= 0.000    
cpu0: Depth=      21 States=   3e+06 Transitions= 3.1438e+06 Memory= 384.654  
cpu2: Depth=      21 States=   3e+06 Transitions= 3.11795e+06 Memory= 0.000    
cpu1: Depth=      27 States=   5e+06 Transitions= 8.34406e+06 Memory= 0.000    
cpu3: Depth=      27 States=   5e+06 Transitions= 8.29819e+06 Memory= 0.000    
cpu2: Depth=      27 States=   4e+06 Transitions= 4.19288e+06 Memory= 0.000    
cpu0: Depth=      21 States=   4e+06 Transitions= 4.18911e+06 Memory= 384.654  
cpu1: Depth=      27 States=   6e+06 Transitions= 9.93911e+06 Memory= 0.000    
cpu3: Depth=      27 States=   6e+06 Transitions= 9.9099e+06 Memory= 0.000    
cpu2: Depth=      27 States=   5e+06 Transitions= 5.2329e+06 Memory= 0.000    
cpu0: Depth=      21 States=   5e+06 Transitions= 5.22121e+06 Memory= 384.654  
cpu1: Depth=      27 States=   7e+06 Transitions= 1.14827e+07 Memory= 0.000    
cpu3: Depth=      27 States=   7e+06 Transitions= 1.14651e+07 Memory= 0.000    
cpu0: Depth=      21 States=   6e+06 Transitions= 6.2523e+06 Memory= 384.654  
cpu2: Depth=      27 States=   6e+06 Transitions= 6.28373e+06 Memory= 0.000    
cpu1: Depth=      27 States=   8e+06 Transitions= 1.3102e+07 Memory= 0.000    
cpu3: Depth=      27 States=   8e+06 Transitions= 1.30602e+07 Memory= 0.000    
cpu0: Depth=      27 States=   7e+06 Transitions= 7.33387e+06 Memory= 384.654  
cpu2: Depth=      27 States=   7e+06 Transitions= 7.31892e+06 Memory= 0.000    
cpu1: Depth=      27 States=   9e+06 Transitions= 1.46491e+07 Memory= 0.000    
cpu3: Depth=      27 States=   9e+06 Transitions= 1.45153e+07 Memory= 0.000    
cpu0: Depth=      27 States=   8e+06 Transitions= 8.38669e+06 Memory= 384.654  
cpu2: Depth=      27 States=   8e+06 Transitions= 8.35645e+06 Memory= 0.000    
cpu1: Depth=      27 States=   1e+07 Transitions= 1.61557e+07 Memory= 0.000    
cpu3: Depth=      27 States=   1e+07 Transitions= 1.60524e+07 Memory= 0.000    
cpu0: Depth=      27 States=   9e+06 Transitions= 9.42516e+06 Memory= 384.654  
cpu2: Depth=      27 States=   9e+06 Transitions= 9.38824e+06 Memory= 0.000    
cpu1: Depth=      27 States= 1.1e+07 Transitions= 1.77041e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.1e+07 Transitions= 1.76059e+07 Memory= 0.000    
cpu2: Depth=      27 States=   1e+07 Transitions= 1.04704e+07 Memory= 0.000    
cpu0: Depth=      27 States=   1e+07 Transitions= 1.04655e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.2e+07 Transitions= 1.91332e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.1e+07 Transitions= 1.15104e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.1e+07 Transitions= 1.14939e+07 Memory= 384.654  
cpu3: Depth=      27 States= 1.2e+07 Transitions= 1.90538e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.2e+07 Transitions= 1.25564e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.2e+07 Transitions= 1.2535e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.3e+07 Transitions= 2.05878e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.3e+07 Transitions= 2.05268e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.3e+07 Transitions= 1.35718e+07 Memory= 384.654  
cpu2: Depth=      27 States= 1.3e+07 Transitions= 1.36044e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.4e+07 Transitions= 2.20897e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.4e+07 Transitions= 2.20259e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.4e+07 Transitions= 1.46408e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.4e+07 Transitions= 1.46206e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.5e+07 Transitions= 2.35369e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.5e+07 Transitions= 1.56744e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.5e+07 Transitions= 1.56831e+07 Memory= 384.654  
cpu3: Depth=      27 States= 1.5e+07 Transitions= 2.34285e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.6e+07 Transitions= 1.67123e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.6e+07 Transitions= 1.67373e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.6e+07 Transitions= 2.49493e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.6e+07 Transitions= 2.485e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.7e+07 Transitions= 1.77532e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.7e+07 Transitions= 1.77768e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.7e+07 Transitions= 2.63559e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.8e+07 Transitions= 1.87978e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.7e+07 Transitions= 2.62783e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.8e+07 Transitions= 1.88288e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.8e+07 Transitions= 2.77957e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.9e+07 Transitions= 1.98395e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.9e+07 Transitions= 1.98687e+07 Memory= 384.654  
cpu3: Depth=      27 States= 1.8e+07 Transitions= 2.77279e+07 Memory= 0.000    
cpu2: Depth=      27 States=   2e+07 Transitions= 2.09208e+07 Memory= 0.000    
cpu0: Depth=      27 States=   2e+07 Transitions= 2.0909e+07 Memory= 384.654  
cpu1: Depth=      27 States= 1.9e+07 Transitions= 2.91595e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.9e+07 Transitions= 2.91119e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.1e+07 Transitions= 2.19802e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.1e+07 Transitions= 2.195e+07 Memory= 384.654  
cpu1: Depth=      27 States=   2e+07 Transitions= 3.055e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.2e+07 Transitions= 2.30251e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.2e+07 Transitions= 2.29955e+07 Memory= 384.654  
cpu3: Depth=      27 States=   2e+07 Transitions= 3.04698e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.3e+07 Transitions= 2.40741e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.3e+07 Transitions= 2.40409e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.1e+07 Transitions= 3.19363e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.1e+07 Transitions= 3.18508e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.4e+07 Transitions= 2.51283e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.4e+07 Transitions= 2.50882e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.2e+07 Transitions= 3.3338e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.5e+07 Transitions= 2.61744e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.5e+07 Transitions= 2.61342e+07 Memory= 384.654  
cpu3: Depth=      27 States= 2.2e+07 Transitions= 3.32278e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.6e+07 Transitions= 2.7215e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.6e+07 Transitions= 2.71972e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.3e+07 Transitions= 3.47119e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.3e+07 Transitions= 3.45609e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.7e+07 Transitions= 2.82644e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.7e+07 Transitions= 2.82623e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.4e+07 Transitions= 3.60652e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.8e+07 Transitions= 2.93178e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.8e+07 Transitions= 2.93184e+07 Memory= 384.654  
cpu3: Depth=      27 States= 2.4e+07 Transitions= 3.59105e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.9e+07 Transitions= 3.03693e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.9e+07 Transitions= 3.03738e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.5e+07 Transitions= 3.74047e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.5e+07 Transitions= 3.72738e+07 Memory= 0.000    
cpu2: Depth=      27 States=   3e+07 Transitions= 3.14265e+07 Memory= 0.000    
cpu0: Depth=      27 States=   3e+07 Transitions= 3.14386e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.6e+07 Transitions= 3.87482e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.1e+07 Transitions= 3.24819e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.1e+07 Transitions= 3.24955e+07 Memory= 384.654  
cpu3: Depth=      27 States= 2.6e+07 Transitions= 3.86412e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.2e+07 Transitions= 3.35511e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.2e+07 Transitions= 3.35493e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.7e+07 Transitions= 4.00712e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.7e+07 Transitions= 3.99997e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.3e+07 Transitions= 3.46293e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.3e+07 Transitions= 3.46081e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.8e+07 Transitions= 4.14181e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.4e+07 Transitions= 3.56736e+07 Memory= 384.654  
cpu2: Depth=      27 States= 3.4e+07 Transitions= 3.56972e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.8e+07 Transitions= 4.13291e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.5e+07 Transitions= 3.67383e+07 Memory= 384.654  
cpu1: Depth=      27 States= 2.9e+07 Transitions= 4.27402e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.5e+07 Transitions= 3.67696e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.9e+07 Transitions= 4.26539e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.6e+07 Transitions= 3.78062e+07 Memory= 384.654  
cpu2: Depth=      27 States= 3.6e+07 Transitions= 3.78484e+07 Memory= 0.000    
cpu1: Depth=      27 States=   3e+07 Transitions= 4.40994e+07 Memory= 0.000    
cpu3: Depth=      27 States=   3e+07 Transitions= 4.39878e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.7e+07 Transitions= 3.88743e+07 Memory= 384.654  
cpu2: Depth=      27 States= 3.7e+07 Transitions= 3.89186e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.1e+07 Transitions= 4.54456e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.8e+07 Transitions= 3.99648e+07 Memory= 384.654  
cpu2: Depth=      27 States= 3.8e+07 Transitions= 3.9985e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.1e+07 Transitions= 4.53293e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.2e+07 Transitions= 4.67872e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.9e+07 Transitions= 4.10679e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.9e+07 Transitions= 4.10633e+07 Memory= 384.654  
cpu3: Depth=      27 States= 3.2e+07 Transitions= 4.66878e+07 Memory= 0.000    
cpu2: Depth=      27 States=   4e+07 Transitions= 4.21455e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.3e+07 Transitions= 4.80987e+07 Memory= 0.000    
cpu0: Depth=      27 States=   4e+07 Transitions= 4.21514e+07 Memory= 384.654  
cpu3: Depth=      27 States= 3.3e+07 Transitions= 4.80235e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.1e+07 Transitions= 4.32313e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.4e+07 Transitions= 4.94415e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.1e+07 Transitions= 4.32459e+07 Memory= 384.654  
cpu3: Depth=      27 States= 3.4e+07 Transitions= 4.93919e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.2e+07 Transitions= 4.43138e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.2e+07 Transitions= 4.4326e+07 Memory= 384.654  
cpu1: Depth=      27 States= 3.5e+07 Transitions= 5.07714e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.5e+07 Transitions= 5.07376e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.3e+07 Transitions= 4.54457e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.3e+07 Transitions= 4.54264e+07 Memory= 384.654  
cpu1: Depth=      27 States= 3.6e+07 Transitions= 5.21826e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.6e+07 Transitions= 5.20926e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.4e+07 Transitions= 4.65528e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.4e+07 Transitions= 4.65196e+07 Memory= 384.654  
cpu1: Depth=      27 States= 3.7e+07 Transitions= 5.3545e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.7e+07 Transitions= 5.34368e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.5e+07 Transitions= 4.76261e+07 Memory= 384.654  
cpu1: Depth=      27 States= 3.8e+07 Transitions= 5.49299e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.5e+07 Transitions= 4.76677e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.8e+07 Transitions= 5.48117e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.9e+07 Transitions= 5.6357e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.6e+07 Transitions= 4.87563e+07 Memory= 384.654  
cpu2: Depth=      27 States= 4.6e+07 Transitions= 4.87833e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.9e+07 Transitions= 5.62575e+07 Memory= 0.000    
cpu1: Depth=      27 States=   4e+07 Transitions= 5.77043e+07 Memory= 0.000    
cpu3: Depth=      27 States=   4e+07 Transitions= 5.76889e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.7e+07 Transitions= 4.98956e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.7e+07 Transitions= 4.98907e+07 Memory= 384.654  
cpu1: Depth=      27 States= 4.1e+07 Transitions= 5.9123e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.1e+07 Transitions= 5.91096e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.8e+07 Transitions= 5.1037e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.2e+07 Transitions= 6.0586e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.8e+07 Transitions= 5.10196e+07 Memory= 384.654  
cpu3: Depth=      27 States= 4.2e+07 Transitions= 6.05794e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.3e+07 Transitions= 6.20797e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.3e+07 Transitions= 6.20363e+07 Memory= 0.000    
cpu2: Depth=      27 States= 4.9e+07 Transitions= 5.21813e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.9e+07 Transitions= 5.21586e+07 Memory= 384.654  
cpu1: Depth=      27 States= 4.4e+07 Transitions= 6.35935e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.4e+07 Transitions= 6.3549e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.5e+07 Transitions= 6.51233e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.5e+07 Transitions= 6.50702e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.6e+07 Transitions= 6.67225e+07 Memory= 0.000    
cpu2: Depth=      27 States=   5e+07 Transitions= 5.33465e+07 Memory= 0.000    
cpu0: Depth=      27 States=   5e+07 Transitions= 5.33214e+07 Memory= 384.654  
cpu3: Depth=      27 States= 4.6e+07 Transitions= 6.66648e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.7e+07 Transitions= 6.83304e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.7e+07 Transitions= 6.83212e+07 Memory= 0.000    
cpu1: Depth=      27 States= 4.8e+07 Transitions= 6.99892e+07 Memory= 0.000    
cpu3: Depth=      27 States= 4.8e+07 Transitions= 7.00084e+07 Memory= 0.000    
cpu1: done -- local memcnt 0 Mb
cpu1: states stored  48933195	matched  22659139
cpu2: done -- local memcnt 0 Mb
cpu1: locks: global         0	other       78784
cpu1: waits: states   6510593	slots           0

cpu2: states stored  50835507	matched   3562777
cpu3: cpu2: locks: global        32	other      103826
cpu2: waits: states 3.6509276e+09	slots           0

done -- local memcnt 0 Mb
cpu3: states stored  48443318	matched  22331563
cpu0: done -- local memcnt 384.654 Mb
cpu0: states stored  50741761	matched   3532468
cpu0: locks: global         0	other      126548
cpu0: waits: states 3.7379326e+09	slots           0

(Spin Version 5.0.0 -- 8 May 2007)
	+ Multi-Core (NCORE=4 -z20)
	+ Partial Order Reduction

Bit statespace search for:
	never claim         	+
	assertion violations	+ (if within scope of claim)
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by never claim)

State-vector 180 byte, depth reached 27, errors: 0
cpu3: locks: global       189	other       50256
cpu3: waits: states  10394425	slots           0

1.9895378e+08 states, stored
 52085947 states, matched
2.5103973e+08 transitions (= stored+matched)
 79999524 atomic steps

hash factor: 5.39694 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
39465.319	equivalent memory usage for states (stored*(State-vector + overhead))
128.000  	memory used for hash array (-w30)
0.076    	memory used for bit stack
0.458    	memory used for DFS stack (-m10000)
256.000  	memory used for shared work-queues
256.071  	other (proc and chan stacks)
0.049    	memory lost to fragmentation
384.654  	total actual memory usage

Successor counts:
  0	    575053	(0.5666 % of total)
  1	  97701977	(96.27 % of total)
  2	   2391610	(2.357 % of total)
  4	    599903	(0.5911 % of total)
 14	     55051	(0.05424 % of total)
 16	    164955	(0.1625 % of total)
mean 1.067 (without 0: 1.073)

cpu0: elapsed time 184 seconds (1.98954e+08 states)
cpu0: rate 1.07933e+06 states/second