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=      27 States=   1e+06 Transitions= 1.59882e+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
cpu4: Depth=      27 States=   1e+06 Transitions= 1.65873e+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
cpu1: Depth=      27 States=   1e+06 Transitions= 1.57518e+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.41586e+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=      27 States=   1e+06 Transitions= 1.28591e+06 Memory= 448.654  
cpu1: Depth=      27 States=   2e+06 Transitions= 3.2825e+06 Memory= 0.000    
cpu4: Depth=      27 States=   2e+06 Transitions= 3.17265e+06 Memory= 0.000    
cpu2: Depth=      27 States=   2e+06 Transitions= 2.64274e+06 Memory= 0.000    
cpu0: Depth=      27 States=   2e+06 Transitions= 2.84474e+06 Memory= 448.654  
cpu3: Depth=      27 States=   2e+06 Transitions= 3.08566e+06 Memory= 0.000    
cpu1: Depth=      27 States=   3e+06 Transitions= 4.9711e+06 Memory= 0.000    
cpu0: Depth=      27 States=   3e+06 Transitions= 4.50224e+06 Memory= 448.654  
cpu2: Depth=      27 States=   3e+06 Transitions= 4.01244e+06 Memory= 0.000    
cpu4: Depth=      27 States=   3e+06 Transitions= 4.21485e+06 Memory= 0.000    
cpu1: Depth=      27 States=   4e+06 Transitions= 6.11682e+06 Memory= 0.000    
cpu3: Depth=      27 States=   3e+06 Transitions= 4.76097e+06 Memory= 0.000    
cpu0: Depth=      27 States=   4e+06 Transitions= 6.18095e+06 Memory= 448.654  
cpu2: Depth=      27 States=   4e+06 Transitions= 5.62245e+06 Memory= 0.000    
cpu4: Depth=      27 States=   4e+06 Transitions= 5.24867e+06 Memory= 0.000    
cpu1: Depth=      27 States=   5e+06 Transitions= 7.15512e+06 Memory= 0.000    
cpu3: Depth=      27 States=   4e+06 Transitions= 6.38384e+06 Memory= 0.000    
cpu0: Depth=      27 States=   5e+06 Transitions= 7.84476e+06 Memory= 448.654  
cpu2: Depth=      27 States=   5e+06 Transitions= 7.24468e+06 Memory= 0.000    
cpu4: Depth=      27 States=   5e+06 Transitions= 6.61614e+06 Memory= 0.000    
cpu3: Depth=      27 States=   5e+06 Transitions= 7.58838e+06 Memory= 0.000    
cpu0: Depth=      27 States=   6e+06 Transitions= 9.48852e+06 Memory= 448.654  
cpu1: Depth=      27 States=   6e+06 Transitions= 8.19484e+06 Memory= 0.000    
cpu2: Depth=      27 States=   6e+06 Transitions= 8.89583e+06 Memory= 0.000    
cpu4: Depth=      27 States=   6e+06 Transitions= 8.09829e+06 Memory= 0.000    
cpu3: Depth=      27 States=   6e+06 Transitions= 8.63074e+06 Memory= 0.000    
cpu0: Depth=      27 States=   7e+06 Transitions= 1.10874e+07 Memory= 448.654  
cpu1: Depth=      27 States=   7e+06 Transitions= 9.21639e+06 Memory= 0.000    
cpu2: Depth=      27 States=   7e+06 Transitions= 1.04928e+07 Memory= 0.000    
cpu0: Depth=      27 States=   8e+06 Transitions= 1.23263e+07 Memory= 448.654  
cpu4: Depth=      27 States=   7e+06 Transitions= 9.74121e+06 Memory= 0.000    
cpu1: Depth=      27 States=   8e+06 Transitions= 1.05906e+07 Memory= 0.000    
cpu3: Depth=      27 States=   7e+06 Transitions= 9.66743e+06 Memory= 0.000    
cpu2: Depth=      27 States=   8e+06 Transitions= 1.21224e+07 Memory= 0.000    
cpu0: Depth=      27 States=   9e+06 Transitions= 1.33662e+07 Memory= 448.654  
cpu4: Depth=      27 States=   8e+06 Transitions= 1.12846e+07 Memory= 0.000    
cpu1: Depth=      27 States=   9e+06 Transitions= 1.20747e+07 Memory= 0.000    
cpu3: Depth=      27 States=   8e+06 Transitions= 1.06937e+07 Memory= 0.000    
cpu2: Depth=      27 States=   9e+06 Transitions= 1.36504e+07 Memory= 0.000    
cpu0: Depth=      27 States=   1e+07 Transitions= 1.44037e+07 Memory= 448.654  
cpu4: Depth=      27 States=   9e+06 Transitions= 1.29188e+07 Memory= 0.000    
cpu1: Depth=      27 States=   1e+07 Transitions= 1.36336e+07 Memory= 0.000    
cpu2: Depth=      27 States=   1e+07 Transitions= 1.5065e+07 Memory= 0.000    
cpu3: Depth=      27 States=   9e+06 Transitions= 1.17645e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.1e+07 Transitions= 1.54464e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.1e+07 Transitions= 1.6105e+07 Memory= 0.000    
cpu4: Depth=      27 States=   1e+07 Transitions= 1.44837e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.1e+07 Transitions= 1.51721e+07 Memory= 0.000    
cpu3: Depth=      27 States=   1e+07 Transitions= 1.31179e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.2e+07 Transitions= 1.64813e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.2e+07 Transitions= 1.71387e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.1e+07 Transitions= 1.59801e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.2e+07 Transitions= 1.67411e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.3e+07 Transitions= 1.7507e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.3e+07 Transitions= 1.81782e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.1e+07 Transitions= 1.46352e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.2e+07 Transitions= 1.75142e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.3e+07 Transitions= 1.82604e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.4e+07 Transitions= 1.86129e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.4e+07 Transitions= 1.92208e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.2e+07 Transitions= 1.61076e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.3e+07 Transitions= 1.86838e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.4e+07 Transitions= 1.97597e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.5e+07 Transitions= 1.99508e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.5e+07 Transitions= 2.02615e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.4e+07 Transitions= 1.97178e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.3e+07 Transitions= 1.75737e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.5e+07 Transitions= 2.12832e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.6e+07 Transitions= 2.14006e+07 Memory= 448.654  
cpu2: Depth=      27 States= 1.6e+07 Transitions= 2.12885e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.5e+07 Transitions= 2.07675e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.4e+07 Transitions= 1.9088e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.7e+07 Transitions= 2.23301e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.7e+07 Transitions= 2.29282e+07 Memory= 448.654  
cpu1: Depth=      27 States= 1.6e+07 Transitions= 2.27701e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.6e+07 Transitions= 2.18092e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.8e+07 Transitions= 2.35403e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.7e+07 Transitions= 2.39219e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.8e+07 Transitions= 2.43912e+07 Memory= 448.654  
cpu3: Depth=      27 States= 1.5e+07 Transitions= 2.05286e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.7e+07 Transitions= 2.28535e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.8e+07 Transitions= 2.49801e+07 Memory= 0.000    
cpu2: Depth=      27 States= 1.9e+07 Transitions= 2.48808e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.9e+07 Transitions= 2.59433e+07 Memory= 448.654  
cpu4: Depth=      27 States= 1.8e+07 Transitions= 2.38972e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.6e+07 Transitions= 2.19851e+07 Memory= 0.000    
cpu1: Depth=      27 States= 1.9e+07 Transitions= 2.60283e+07 Memory= 0.000    
cpu2: Depth=      27 States=   2e+07 Transitions= 2.63467e+07 Memory= 0.000    
cpu4: Depth=      27 States= 1.9e+07 Transitions= 2.49413e+07 Memory= 0.000    
cpu0: Depth=      27 States=   2e+07 Transitions= 2.74325e+07 Memory= 448.654  
cpu3: Depth=      27 States= 1.7e+07 Transitions= 2.343e+07 Memory= 0.000    
cpu1: Depth=      27 States=   2e+07 Transitions= 2.7075e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.1e+07 Transitions= 2.78617e+07 Memory= 0.000    
cpu4: Depth=      27 States=   2e+07 Transitions= 2.5993e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.1e+07 Transitions= 2.88978e+07 Memory= 448.654  
cpu1: Depth=      27 States= 2.1e+07 Transitions= 2.81245e+07 Memory= 0.000    
cpu3: Depth=      27 States= 1.8e+07 Transitions= 2.47793e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.2e+07 Transitions= 2.9388e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.1e+07 Transitions= 2.72191e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.2e+07 Transitions= 3.0408e+07 Memory= 448.654  
cpu3: Depth=      27 States= 1.9e+07 Transitions= 2.58379e+07 Memory= 0.000    
cpu1: Depth=      27 States= 2.2e+07 Transitions= 2.9178e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.3e+07 Transitions= 3.0895e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.2e+07 Transitions= 2.85596e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.3e+07 Transitions= 3.18689e+07 Memory= 448.654  
cpu1: Depth=      27 States= 2.3e+07 Transitions= 3.02299e+07 Memory= 0.000    
cpu3: Depth=      27 States=   2e+07 Transitions= 2.68859e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.4e+07 Transitions= 3.23435e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.3e+07 Transitions= 3.00213e+07 Memory= 0.000    
cpu1: Depth=      27 States= 2.4e+07 Transitions= 3.1292e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.1e+07 Transitions= 2.79452e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.4e+07 Transitions= 3.33078e+07 Memory= 448.654  
cpu2: Depth=      27 States= 2.5e+07 Transitions= 3.38366e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.4e+07 Transitions= 3.15269e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.5e+07 Transitions= 3.45089e+07 Memory= 448.654  
cpu1: Depth=      27 States= 2.5e+07 Transitions= 3.25309e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.2e+07 Transitions= 2.90045e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.6e+07 Transitions= 3.52986e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.5e+07 Transitions= 3.30199e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.6e+07 Transitions= 3.55698e+07 Memory= 448.654  
cpu3: Depth=      27 States= 2.3e+07 Transitions= 3.00687e+07 Memory= 0.000    
cpu1: Depth=      27 States= 2.6e+07 Transitions= 3.38437e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.4e+07 Transitions= 3.11316e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.7e+07 Transitions= 3.67146e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.6e+07 Transitions= 3.45133e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.7e+07 Transitions= 3.66314e+07 Memory= 448.654  
cpu1: Depth=      27 States= 2.7e+07 Transitions= 3.53424e+07 Memory= 0.000    
cpu2: Depth=      27 States= 2.8e+07 Transitions= 3.8127e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.5e+07 Transitions= 3.22659e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.7e+07 Transitions= 3.60081e+07 Memory= 0.000    
cpu1: Depth=      27 States= 2.8e+07 Transitions= 3.68795e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.8e+07 Transitions= 3.77129e+07 Memory= 448.654  
cpu2: Depth=      27 States= 2.9e+07 Transitions= 3.92043e+07 Memory= 0.000    
cpu1: Depth=      27 States= 2.9e+07 Transitions= 3.83922e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.8e+07 Transitions= 3.74909e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.9e+07 Transitions= 3.87895e+07 Memory= 448.654  
cpu3: Depth=      27 States= 2.6e+07 Transitions= 3.3586e+07 Memory= 0.000    
cpu1: Depth=      27 States=   3e+07 Transitions= 3.99264e+07 Memory= 0.000    
cpu4: Depth=      27 States= 2.9e+07 Transitions= 3.89168e+07 Memory= 0.000    
cpu2: Depth=      27 States=   3e+07 Transitions= 4.0292e+07 Memory= 0.000    
cpu0: Depth=      27 States=   3e+07 Transitions= 3.98685e+07 Memory= 448.654  
cpu3: Depth=      27 States= 2.7e+07 Transitions= 3.50825e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.1e+07 Transitions= 4.14306e+07 Memory= 0.000    
cpu4: Depth=      27 States=   3e+07 Transitions= 4.03472e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.1e+07 Transitions= 4.10796e+07 Memory= 448.654  
cpu2: Depth=      27 States= 3.1e+07 Transitions= 4.13862e+07 Memory= 0.000    
cpu3: Depth=      27 States= 2.8e+07 Transitions= 3.65907e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.2e+07 Transitions= 4.29523e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.2e+07 Transitions= 4.25572e+07 Memory= 448.654  
cpu4: Depth=      27 States= 3.1e+07 Transitions= 4.14557e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.3e+07 Transitions= 4.44626e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.2e+07 Transitions= 4.24867e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.3e+07 Transitions= 4.41985e+07 Memory= 448.654  
cpu3: Depth=      27 States= 2.9e+07 Transitions= 3.81667e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.4e+07 Transitions= 4.58611e+07 Memory= 448.654  
cpu2: Depth=      27 States= 3.3e+07 Transitions= 4.38396e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.4e+07 Transitions= 4.57549e+07 Memory= 0.000    
cpu3: Depth=      27 States=   3e+07 Transitions= 3.97103e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.5e+07 Transitions= 4.75397e+07 Memory= 448.654  
cpu4: Depth=      27 States= 3.2e+07 Transitions= 4.25609e+07 Memory= 0.000    
cpu2: Depth=      27 States= 3.4e+07 Transitions= 4.55532e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.1e+07 Transitions= 4.12503e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.6e+07 Transitions= 4.91782e+07 Memory= 448.654  
cpu2: Depth=      27 States= 3.5e+07 Transitions= 4.72782e+07 Memory= 0.000    
cpu4: Depth=      27 States= 3.3e+07 Transitions= 4.38821e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.7e+07 Transitions= 5.08595e+07 Memory= 448.654  
cpu2: Depth=      27 States= 3.6e+07 Transitions= 4.89961e+07 Memory= 0.000    
cpu1: Depth=      27 States= 3.5e+07 Transitions= 4.69049e+07 Memory= 0.000    
cpu3: Depth=      27 States= 3.2e+07 Transitions= 4.26278e+07 Memory= 0.000    
cpu4: Depth=      27 States= 3.4e+07 Transitions= 4.55883e+07 Memory= 0.000    
cpu1: done -- local memcnt 0 Mb
cpu1: states stored  35600055	matched  12251130
cpu2: done -- local memcnt 0 Mb
cpu2: cpu1: locks: global         0	other      776643
cpu1: waits: states 1.3620639e+09	slots           0

states stored  36955569	matched  13603942
cpu3: done -- local memcnt 0 Mb
cpu3: cpu2: locks: global        15	other      897958
cpu2: waits: states 1.3147573e+09	slots           0

states stored  32304057	matched  10856014
cpu4: done -- local memcnt 0 Mb
cpu4: states stored  34002531	matched  11590576
cpu3: locks: global        23	other      106231
cpu3: waits: states 4.0767257e+08	slots           0

cpu0: cpu4: locks: global         5	other      748504
cpu4: waits: states 1.7199419e+09	slots           0

done -- local memcnt 448.654 Mb
cpu0: states stored  37814772	matched  14311892
cpu0: locks: global      1357	other      911968
cpu0: waits: states 1.1390748e+09	slots           0

(Spin Version 5.0.0 -- 8 May 2007)
	+ Multi-Core (NCORE=5 -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
1.7667698e+08 states, stored
 62613554 states, matched
2.3929054e+08 transitions (= stored+matched)
 69489342 atomic steps

hash factor: 6.07743 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
35046.399	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)
320.000  	memory used for shared work-queues
320.071  	other (proc and chan stacks)
0.049    	memory lost to fragmentation
448.654  	total actual memory usage

Successor counts:
  0	    120185	(0.1342 % of total)
  1	  86970770	(97.13 % of total)
  2	    882558	(0.9857 % of total)
  4	    532298	(0.5945 % of total)
 14	    256025	(0.2859 % of total)
 16	    775697	(0.8663 % of total)
mean 1.193 (without 0: 1.195)

cpu0: elapsed time 145 seconds (1.76677e+08 states)
cpu0: rate 1.21436e+06 states/second