@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 80 and seed -1480600621184801018 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 25012] (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\Inductive Invariance of Inv\MC.tla
Parsing file C:\lamport\books\fred\book-specs\Fischer.toolbox\Inductive Invariance of Inv\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 TLAPS
Semantic processing of module Fischer
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-10-14 17:15:55)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 16 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 32 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 64 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 128 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 256 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 512 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 1024 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2048 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4096 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8192 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 16384 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 32768 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 65536 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 131072 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 262144 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 524288 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 1048576 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1281039 distinct states generated at 2024-10-14 17:16:12.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(1) at 2024-10-14 17:16:15: 2,892,503 states generated (2,892,503 s/min), 1,281,039 distinct states found (1,281,039 ds/min), 959,402 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.6E-7
  based on the actual fingerprints:  val = 7.9E-10
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-14 17:16:23
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Inv line 95, col 1 to line 95, col 3 of module Fischer>: 1281039:5668704
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 90, col 20 to line 90, col 36 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 90, col 20 to line 90, col 24 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 90, col 31 to line 90, col 36 of module Fischer: 1:2
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 90, col 32 to line 90, col 35 of module Fischer: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 91, col 21 to line 91, col 72 of module Fischer: 4:2592
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 91, col 22 to line 91, col 26 of module Fischer: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 91, col 31 to line 91, col 71 of module Fischer: 4:1212
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 92, col 21 to line 92, col 36 of module Fischer: 864:1889568
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 92, col 22 to line 92, col 26 of module Fischer: 864
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 92, col 31 to line 92, col 35 of module Fischer: 864
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 93, col 14 to line 93, col 26 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 93, col 22 to line 93, col 26 of module Fischer: 629856
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 96, col 11 to line 102, col 74 of module Fischer: 5668704
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 97, col 14 to line 102, col 74 of module Fischer: 11155952
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 97, col 17 to line 97, col 66 of module Fischer: 11155952
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 97, col 18 to line 97, col 29 of module Fischer: 11155952
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 97, col 36 to line 97, col 65 of module Fischer: 1710812
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 98, col 17 to line 99, col 60 of module Fischer: 9955091
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 98, col 18 to line 98, col 41 of module Fischer: 9955091
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 99, col 21 to line 99, col 60 of module Fischer: 3778056
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 99, col 22 to line 99, col 26 of module Fischer: 3778056
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 99, col 32 to line 99, col 60 of module Fischer: 874566
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 99, col 49 to line 99, col 60 of module Fischer: 2460870
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 99, col 41 to line 99, col 45 of module Fischer: 874566
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||||line 11, col 1 to line 11, col 12 of module MC: 874566:3335436
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 2 to line 11, col 3 of module MC: 874566
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 6 to line 11, col 7 of module MC: 874566
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 10 to line 11, col 11 of module MC: 874566
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 100, col 17 to line 102, col 74 of module Fischer: 6820013
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 100, col 17 to line 100, col 41 of module Fischer: 6820013
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 100, col 18 to line 100, col 29 of module Fischer: 6820013
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 100, col 36 to line 100, col 40 of module Fischer: 1889028
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 101, col 19 to line 102, col 74 of module Fischer: 437283
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 101, col 36 to line 102, col 74 of module Fischer: 1277751
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 101, col 37 to line 101, col 48 of module Fischer: 1277751
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 102, col 40 to line 102, col 74 of module Fischer: 120976
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 101, col 28 to line 101, col 32 of module Fischer: 437283
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||line 11, col 1 to line 11, col 12 of module MC: 437283:1715034
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 2 to line 11, col 3 of module MC: 437283
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 6 to line 11, col 7 of module MC: 437283
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 11, col 10 to line 11, col 11 of module MC: 437283
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 96, col 20 to line 96, col 24 of module Fischer: 5668704
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 12 of module MC: 5668704:16824656
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 2 to line 11, col 3 of module MC: 5668704
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 6 to line 11, col 7 of module MC: 5668704
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 10 to line 11, col 11 of module MC: 5668704
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Ncs line 43, col 1 to line 43, col 6 of module Fischer>: 0:1087506
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 43, col 14 to line 43, col 26 of module Fischer: 4930623
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 43, col 14 to line 43, col 18 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 44, col 14 to line 44, col 44 of module Fischer: 1087506
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 45, col 14 to line 45, col 37 of module Fischer: 1087506
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Wait line 47, col 1 to line 47, col 7 of module Fischer>: 0:213975
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 47, col 15 to line 47, col 28 of module Fischer: 4057092
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 47, col 15 to line 47, col 19 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 48, col 15 to line 48, col 23 of module Fischer: 1301481
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 48, col 15 to line 48, col 15 of module Fischer: 1087506
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 48, col 20 to line 48, col 23 of module Fischer: 1087506
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 49, col 15 to line 49, col 42 of module Fischer: 213975
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 50, col 15 to line 50, col 43 of module Fischer: 213975
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 51, col 15 to line 51, col 34 of module Fischer: 213975
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W1 line 53, col 1 to line 53, col 5 of module Fischer>: 0:240924
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 53, col 13 to line 53, col 24 of module Fischer: 4084041
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 53, col 13 to line 53, col 17 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 54, col 13 to line 54, col 18 of module Fischer: 240924
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 55, col 13 to line 55, col 40 of module Fischer: 240924
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 56, col 13 to line 56, col 41 of module Fischer: 240924
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 57, col 13 to line 57, col 22 of module Fischer: 240924
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W2 line 59, col 1 to line 59, col 5 of module Fischer>: 0:275247
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 59, col 13 to line 59, col 24 of module Fischer: 4118364
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 59, col 13 to line 59, col 17 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 60, col 13 to line 60, col 34 of module Fischer: 275247
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 60, col 13 to line 60, col 23 of module Fischer: 1072887
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 60, col 28 to line 60, col 34 of module Fischer: 1072887
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 61, col 13 to line 61, col 67 of module Fischer: 275247
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 62, col 13 to line 62, col 36 of module Fischer: 275247
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Cs line 64, col 1 to line 64, col 5 of module Fischer>: 0:177147
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 64, col 13 to line 64, col 24 of module Fischer: 4020264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 64, col 13 to line 64, col 17 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 65, col 13 to line 65, col 43 of module Fischer: 177147
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 66, col 13 to line 66, col 36 of module Fischer: 177147
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Exit line 68, col 1 to line 68, col 7 of module Fischer>: 0:177147
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 68, col 15 to line 68, col 28 of module Fischer: 4020264
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 68, col 15 to line 68, col 19 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 69, col 15 to line 69, col 23 of module Fischer: 177147
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 15 to line 70, col 44 of module Fischer: 177147
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 15 to line 71, col 35 of module Fischer: 177147
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Time line 73, col 1 to line 73, col 4 of module Fischer>: 0:4444186
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 73, col 12 to line 73, col 43 of module Fischer: 4444186
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 73, col 21 to line 73, col 43 of module Fischer: 1281039:6321394
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 73, col 36 to line 73, col 42 of module Fischer: 11529351
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 73, col 28 to line 73, col 32 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 29 to line 74, col 67 of module Fischer: 13128102
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 30 to line 74, col 41 of module Fischer: 14492902
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 48 to line 74, col 66 of module Fischer: 204456
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 74, col 48 to line 74, col 51 of module Fischer: 808362
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 74, col 56 to line 74, col 66 of module Fischer: 808362
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 21 to line 74, col 25 of module Fischer: 5040355
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 11, col 1 to line 11, col 12 of module MC: 5040355:20161420
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 2 to line 11, col 3 of module MC: 5040355
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 6 to line 11, col 7 of module MC: 5040355
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 10 to line 11, col 11 of module MC: 5040355
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 75, col 12 to line 75, col 34 of module Fischer: 4444186
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<Inv line 95, col 1 to line 95, col 3 of module Fischer>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 95, col 8 to line 102, col 74 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 95, col 11 to line 95, col 16 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 90, col 11 to line 93, col 26 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 90, col 14 to line 90, col 36 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 90, col 14 to line 90, col 14 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 90, col 20 to line 90, col 36 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 90, col 20 to line 90, col 24 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||line 90, col 31 to line 90, col 36 of module Fischer: 1281039:2562078
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 90, col 32 to line 90, col 35 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 91, col 14 to line 91, col 72 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 92, col 14 to line 92, col 36 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 93, col 14 to line 93, col 26 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 96, col 11 to line 102, col 74 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 97, col 14 to line 102, col 74 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 97, col 17 to line 97, col 66 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 97, col 18 to line 97, col 29 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 97, col 36 to line 97, col 65 of module Fischer: 240924
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 98, col 17 to line 99, col 60 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 98, col 18 to line 98, col 41 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 99, col 21 to line 99, col 60 of module Fischer: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 99, col 22 to line 99, col 26 of module Fischer: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 99, col 32 to line 99, col 60 of module Fischer: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 99, col 49 to line 99, col 60 of module Fischer: 1062882
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 99, col 41 to line 99, col 45 of module Fischer: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||||line 11, col 1 to line 11, col 12 of module MC: 354294:1417176
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 11, col 2 to line 11, col 3 of module MC: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 11, col 6 to line 11, col 7 of module MC: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 11, col 10 to line 11, col 11 of module MC: 354294
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 100, col 17 to line 102, col 74 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 100, col 17 to line 100, col 41 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 100, col 18 to line 100, col 29 of module Fischer: 3843117
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 100, col 36 to line 100, col 40 of module Fischer: 1072887
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 101, col 19 to line 102, col 74 of module Fischer: 199356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 101, col 36 to line 102, col 74 of module Fischer: 598068
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 101, col 37 to line 101, col 48 of module Fischer: 598068
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 102, col 40 to line 102, col 74 of module Fischer: 23196
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 101, col 28 to line 101, col 32 of module Fischer: 199356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||||line 11, col 1 to line 11, col 12 of module MC: 199356:797424
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 2 to line 11, col 3 of module MC: 199356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 6 to line 11, col 7 of module MC: 199356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 10 to line 11, col 11 of module MC: 199356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 96, col 20 to line 96, col 24 of module Fischer: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||line 11, col 1 to line 11, col 12 of module MC: 1281039:5124156
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 2 to line 11, col 3 of module MC: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 6 to line 11, col 7 of module MC: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 10 to line 11, col 11 of module MC: 1281039
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(1) at 2024-10-14 17:16:23: 7,897,171 states generated (14,659,229 s/min), 1,281,039 distinct states found (2,377,945 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
7897171 states generated, 1281039 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 1.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 32368ms at (2024-10-14 17:16:23)
@!@!@ENDMSG 2186 @!@!@
