@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 75 and seed 3281488420435719798 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 7776] (Windows 10 10.0 amd64, Oracle Corporation 11.0.2 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file C:\lamport\books\fred\book-specs\Fischer.toolbox\Invariance of LInv\MC.tla
Parsing file C:\lamport\books\fred\book-specs\Fischer.toolbox\Invariance of LInv\Fischer.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\TLC.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Integers.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Naturals.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\TLAPS.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Sequences.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module TLAPS
Semantic processing of module Fischer
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-10-14 14:16:09)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state generated at 2024-10-14 14:16:10.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(19) at 2024-10-14 14:16:13: 602,400 states generated (602,400 s/min), 161,558 distinct states found (161,558 ds/min), 42,595 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 4.4E-8
  based on the actual fingerprints:  val = 1.0E-9
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-14 14:16:20
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 18, col 1 to line 18, col 4 of module Fischer>: 1:1
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 18, col 12 to line 18, col 19 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 19, col 17 to line 19, col 40 of module Fischer: 1:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 24 to line 19, col 28 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 16 of module MC: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 2 to line 11, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 6 to line 11, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 10 to line 11, col 11 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 14 to line 11, col 15 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 20, col 17 to line 20, col 35 of module Fischer: 1:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 20, col 24 to line 20, col 28 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 16 of module MC: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 2 to line 11, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 6 to line 11, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 10 to line 11, col 11 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 14 to line 11, col 15 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 21, col 12 to line 21, col 18 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Ncs line 23, col 1 to line 23, col 6 of module Fischer>: 62519:304524
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 23, col 14 to line 23, col 26 of module Fischer: 2192788
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 23, col 14 to line 23, col 18 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 24, col 18 to line 24, col 48 of module Fischer: 304524
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 25, col 18 to line 25, col 41 of module Fischer: 304524
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Wait line 27, col 1 to line 27, col 7 of module Fischer>: 34025:284433
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 27, col 15 to line 27, col 28 of module Fischer: 2172697
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 27, col 15 to line 27, col 19 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 28, col 15 to line 28, col 23 of module Fischer: 896014
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 28, col 15 to line 28, col 15 of module Fischer: 611581
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 28, col 20 to line 28, col 23 of module Fischer: 611581
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 29, col 15 to line 29, col 42 of module Fischer: 284433
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 30, col 15 to line 30, col 43 of module Fischer: 284433
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 31, col 15 to line 31, col 34 of module Fischer: 284433
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W1 line 34, col 1 to line 34, col 5 of module Fischer>: 44419:118770
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 34, col 13 to line 34, col 24 of module Fischer: 2007034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 34, col 13 to line 34, col 17 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 35, col 13 to line 35, col 18 of module Fischer: 118770
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 13 to line 36, col 40 of module Fischer: 118770
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 37, col 13 to line 37, col 41 of module Fischer: 118770
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 38, col 13 to line 38, col 22 of module Fischer: 118770
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W2 line 40, col 1 to line 40, col 5 of module Fischer>: 87297:606031
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 40, col 13 to line 40, col 24 of module Fischer: 2494295
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 40, col 13 to line 40, col 17 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 41, col 13 to line 41, col 34 of module Fischer: 606031
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 41, col 13 to line 41, col 23 of module Fischer: 738667
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 41, col 28 to line 41, col 34 of module Fischer: 738667
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 42, col 13 to line 42, col 67 of module Fischer: 606031
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 43, col 13 to line 43, col 36 of module Fischer: 606031
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Cs line 45, col 1 to line 45, col 5 of module Fischer>: 56067:57361
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 45, col 13 to line 45, col 24 of module Fischer: 1945625
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 45, col 13 to line 45, col 17 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 46, col 13 to line 46, col 43 of module Fischer: 57361
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 47, col 13 to line 47, col 36 of module Fischer: 57361
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Exit line 49, col 1 to line 49, col 7 of module Fischer>: 56659:57361
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 49, col 15 to line 49, col 28 of module Fischer: 1945625
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 49, col 15 to line 49, col 19 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 50, col 15 to line 50, col 23 of module Fischer: 57361
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 51, col 15 to line 51, col 44 of module Fischer: 57361
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 52, col 15 to line 52, col 35 of module Fischer: 57361
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Time line 54, col 1 to line 54, col 4 of module Fischer>: 131079:745305
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 54, col 12 to line 54, col 43 of module Fischer: 745305
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 54, col 21 to line 54, col 43 of module Fischer: 472066:1371826
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 54, col 36 to line 54, col 42 of module Fischer: 7553056
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 54, col 28 to line 54, col 32 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 55, col 29 to line 55, col 67 of module Fischer: 2901689
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 55, col 30 to line 55, col 41 of module Fischer: 3324256
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 55, col 48 to line 55, col 66 of module Fischer: 79531
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 55, col 48 to line 55, col 51 of module Fischer: 242500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 55, col 56 to line 55, col 66 of module Fischer: 242500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 55, col 21 to line 55, col 25 of module Fischer: 899760
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 11, col 1 to line 11, col 16 of module MC: 899760:4498800
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 2 to line 11, col 3 of module MC: 899760
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 6 to line 11, col 7 of module MC: 899760
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 10 to line 11, col 11 of module MC: 899760
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 14 to line 11, col 15 of module MC: 899760
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 56, col 12 to line 56, col 34 of module Fischer: 745305
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<LInv line 86, col 1 to line 86, col 4 of module Fischer>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 86, col 9 to line 87, col 57 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 86, col 12 to line 86, col 14 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 67, col 8 to line 74, col 74 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 67, col 11 to line 67, col 16 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 13, col 11 to line 16, col 26 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 13, col 14 to line 13, col 36 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 13, col 14 to line 13, col 14 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 13, col 20 to line 13, col 36 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 13, col 20 to line 13, col 24 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||||line 13, col 31 to line 13, col 36 of module Fischer: 472066:944132
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 13, col 32 to line 13, col 35 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 14, col 14 to line 14, col 72 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 15, col 14 to line 15, col 36 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 16, col 14 to line 16, col 26 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 68, col 11 to line 74, col 74 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 69, col 14 to line 74, col 74 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 69, col 17 to line 69, col 66 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 69, col 18 to line 69, col 29 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 69, col 36 to line 69, col 65 of module Fischer: 118770
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 70, col 17 to line 71, col 60 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 70, col 18 to line 70, col 41 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 71, col 21 to line 71, col 60 of module Fischer: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 71, col 22 to line 71, col 26 of module Fischer: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 71, col 32 to line 71, col 60 of module Fischer: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 71, col 49 to line 71, col 60 of module Fischer: 458888
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 71, col 41 to line 71, col 45 of module Fischer: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||||||line 11, col 1 to line 11, col 16 of module MC: 114722:573610
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||||line 11, col 2 to line 11, col 3 of module MC: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||||line 11, col 6 to line 11, col 7 of module MC: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||||line 11, col 10 to line 11, col 11 of module MC: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||||line 11, col 14 to line 11, col 15 of module MC: 114722
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 72, col 17 to line 74, col 74 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 72, col 17 to line 72, col 41 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 72, col 18 to line 72, col 29 of module Fischer: 1888264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 72, col 36 to line 72, col 40 of module Fischer: 738667
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 73, col 19 to line 74, col 74 of module Fischer: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 73, col 36 to line 74, col 74 of module Fischer: 663424
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 73, col 37 to line 73, col 48 of module Fischer: 663424
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 74, col 40 to line 74, col 74 of module Fischer: 22424
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 73, col 28 to line 73, col 32 of module Fischer: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||||||line 11, col 1 to line 11, col 16 of module MC: 165856:829280
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 2 to line 11, col 3 of module MC: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 6 to line 11, col 7 of module MC: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 10 to line 11, col 11 of module MC: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 14 to line 11, col 15 of module MC: 165856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 68, col 20 to line 68, col 24 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||line 11, col 1 to line 11, col 16 of module MC: 472066:2360330
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 2 to line 11, col 3 of module MC: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 6 to line 11, col 7 of module MC: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 10 to line 11, col 11 of module MC: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 14 to line 11, col 15 of module MC: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 87, col 12 to line 87, col 57 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 87, col 13 to line 87, col 20 of module Fischer: 472066
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 87, col 27 to line 87, col 56 of module Fischer: 280578
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(36) at 2024-10-14 14:16:21: 2,173,786 states generated (10,481,970 s/min), 472,066 distinct states found (2,276,296 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
2173786 states generated, 472066 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 36.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 15 and the 95th percentile is 3).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 12475ms at (2024-10-14 14:16:21)
@!@!@ENDMSG 2186 @!@!@
