INFO     Running translator.
INFO     translator input: ['/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl', '/home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-13.pddl']
INFO     translator arguments: []
INFO     translator time limit: None
INFO     translator memory limit: None
INFO     callstring: /home/pluehne/.usr/bin/python /home/wv/bin/linux/64/fast-downward-10997/builds/release64/bin/translate/translate.py /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/domain.pddl /home/pluehne/Documents/ASP/pddl-instances/ipc-2011/domains/barman-sequential-satisficing/instances/instance-13.pddl
Parsing...
Parsing: [0.050s CPU, 0.048s wall-clock]
Normalizing task... [0.000s CPU, 0.004s wall-clock]
Instantiating...
Generating Datalog program... [0.010s CPU, 0.013s wall-clock]
Normalizing Datalog program...
Normalizing Datalog program: [0.070s CPU, 0.070s wall-clock]
Preparing model... [0.040s CPU, 0.037s wall-clock]
Generated 115 rules.
Computing model... [0.510s CPU, 0.520s wall-clock]
3094 relevant atoms
3221 auxiliary atoms
6315 final queue length
10878 total queue pushes
Completing instantiation... [0.960s CPU, 0.964s wall-clock]
Instantiating: [1.600s CPU, 1.610s wall-clock]
Computing fact groups...
Finding invariants...
24 initial candidates
Finding invariants: [0.120s CPU, 0.115s wall-clock]
Checking invariant weight... [0.000s CPU, 0.001s wall-clock]
Instantiating groups... [0.010s CPU, 0.009s wall-clock]
Collecting mutex groups... [0.000s CPU, 0.001s wall-clock]
Choosing groups...
328 uncovered facts
Choosing groups: [0.000s CPU, 0.002s wall-clock]
Building translation key... [0.010s CPU, 0.012s wall-clock]
Computing fact groups: [0.170s CPU, 0.166s wall-clock]
Building STRIPS to SAS dictionary... [0.000s CPU, 0.003s wall-clock]
Building dictionary for full mutex groups... [0.010s CPU, 0.003s wall-clock]
Building mutex information...
Building mutex information: [0.000s CPU, 0.003s wall-clock]
Translating task...
Processing axioms...
Simplifying axioms... [0.000s CPU, 0.000s wall-clock]
Processing axioms: [0.050s CPU, 0.052s wall-clock]
Translating task: [1.000s CPU, 1.000s wall-clock]
3672 effect conditions simplified
0 implied preconditions added
Detecting unreachable propositions...
0 operators removed
0 axioms removed
3 propositions removed
Detecting unreachable propositions: [0.490s CPU, 0.491s wall-clock]
Reordering and filtering variables...
331 of 331 variables necessary.
15 of 18 mutex groups necessary.
2194 of 2194 operators necessary.
0 of 0 axiom rules necessary.
Reordering and filtering variables: [0.400s CPU, 0.403s wall-clock]
Translator variables: 331
Translator derived variables: 0
Translator facts: 691
Translator goal facts: 13
Translator mutex groups: 15
Translator total mutex groups size: 45
Translator operators: 2194
Translator axioms: 0
Translator task size: 21018
Translator peak memory: 48332 KB
Writing output... [0.430s CPU, 0.460s wall-clock]
Done! [4.190s CPU, 4.231s wall-clock]
planner.py version 0.0.1

Time:	 0.86s
Memory: 107MB

Iteration 1
Queue:		 [(0,0,0,True), (1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 0
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 1
Time         : 1.030s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.860s

Choices      : 0       
Conflicts    : 0        (Analyzed: 0)
Restarts     : 0       
Problems     : 1        (Average Length: 2.00 Splits: 0)
Lemmas       : 0        (Deleted: 0)
  Binary     : 0        (Ratio:   0.00%)
  Ternary    : 0        (Ratio:   0.00%)
  Conflict   : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 0        (Average:  0.00 Max:   0 Sum:      0)
  Executed   : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio: 100.00%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 0        (Eliminated:    0 Frozen:    0)
Constraints  : 0        (Binary:   0.0% Ternary:   0.0% Other:   0.0%)

Memory Peak  : 243MB
Max. Length  : 0 steps
Models       : 0

[endof: stats after solve call]
Solving Time:	 0.01s
Memory:		 179MB (+72MB)
UNSAT
Iteration Time:	 0.01s

Iteration 2
Queue:		 [(1,5,0,True), (2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 0
Expected Memory: 179MB
Grounding...	 [('step', [1]), ('step', [2]), ('step', [3]), ('step', [4]), ('step', [5]), ('check', [5])]
Grounding Time:	 0.26s
Memory:		 179MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 2
Time         : 1.433s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 1.260s

Choices      : 335      (Domain: 109)
Conflicts    : 40       (Analyzed: 39)
Restarts     : 0       
Problems     : 2        (Average Length: 4.50 Splits: 0)
Lemmas       : 39       (Deleted: 0)
  Binary     : 6        (Ratio:  15.38%)
  Ternary    : 2        (Ratio:   5.13%)
  Conflict   : 39       (Average Length:    5.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 39       (Average:  8.62 Max: 215 Sum:    336)
  Executed   : 38       (Average:  8.59 Max: 215 Sum:    335 Ratio:  99.70%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.30%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 16256    (Eliminated:    0 Frozen:  160)
Constraints  : 53667    (Binary:  95.3% Ternary:   3.3% Other:   1.4%)

Memory Peak  : 243MB
Max. Length  : 0 steps
Models       : 0

[endof: stats after solve call]
Solving Time:	 0.02s
Memory:		 183MB (+4MB)
UNSAT
Iteration Time:	 0.41s

Iteration 3
Queue:		 [(2,10,0,True), (3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 5
Expected Memory: 187.0MB
Grounding...	 [('step', [6]), ('step', [7]), ('step', [8]), ('step', [9]), ('step', [10]), ('check', [10])]
Grounding Time:	 0.31s
Memory:		 190MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 1+
Calls        : 3
Time         : 1.940s (Solving: 0.05s 1st Model: 0.05s Unsat: 0.00s)
CPU Time     : 1.768s

Choices      : 2722     (Domain: 2398)
Conflicts    : 259      (Analyzed: 258)
Restarts     : 1        (Average: 258.00 Last: 88)
Model-Level  : 232.0   
Problems     : 3        (Average Length: 7.00 Splits: 0)
Lemmas       : 258      (Deleted: 0)
  Binary     : 49       (Ratio:  18.99%)
  Ternary    : 10       (Ratio:   3.88%)
  Conflict   : 258      (Average Length:  141.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 258      (Average:  9.59 Max: 215 Sum:   2474)
  Executed   : 257      (Average:  9.59 Max: 215 Sum:   2473 Ratio:  99.96%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.04%)

Rules        : 60629   
Atoms        : 60629   
Bodies       : 1        (Original: 0)
Tight        : Yes
Variables    : 35632    (Eliminated:    0 Frozen:  320)
Constraints  : 211962   (Binary:  95.6% Ternary:   3.2% Other:   1.2%)

Memory Peak  : 243MB
Max. Length  : 5 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 0.07s
Memory:		 198MB (+8MB)
SAT
Testing...
NOT SERIALIZABLE
Testing Time:	 1.11s
Memory:		 232MB (+34MB)
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 4
Time         : 3.474s (Solving: 1.26s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 3.304s

Choices      : 30145    (Domain: 22365)
Conflicts    : 3230     (Analyzed: 3228)
Restarts     : 34       (Average: 94.94 Last: 88)
Model-Level  : 232.0   
Problems     : 4        (Average Length: 8.25 Splits: 0)
Lemmas       : 3228     (Deleted: 881)
  Binary     : 397      (Ratio:  12.30%)
  Ternary    : 151      (Ratio:   4.68%)
  Conflict   : 3228     (Average Length:  107.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 3228     (Average:  9.19 Max: 279 Sum:  29664)
  Executed   : 3210     (Average:  9.14 Max: 279 Sum:  29492 Ratio:  99.42%)
  Bounded    : 18       (Average:  9.56 Max:  12 Sum:    172 Ratio:   0.58%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 56254    (Eliminated:    0 Frozen: 15821)
Constraints  : 347145   (Binary:  91.4% Ternary:   7.0% Other:   1.7%)

Memory Peak  : 243MB
Max. Length  : 5 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 1.29s
Memory:		 232MB (+0MB)
UNSAT
Iteration Time:	 2.92s

Iteration 4
Queue:		 [(3,15,0,True), (4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 10
Expected Memory: 247.0MB
Grounding...	 [('step', [11]), ('step', [12]), ('step', [13]), ('step', [14]), ('step', [15]), ('check', [15])]
Grounding Time:	 0.53s
Memory:		 233MB (+1MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 5
Time         : 8.845s (Solving: 5.86s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 8.676s

Choices      : 103836   (Domain: 87068)
Conflicts    : 12512    (Analyzed: 12510)
Restarts     : 134      (Average: 93.36 Last: 88)
Model-Level  : 232.0   
Problems     : 5        (Average Length: 10.00 Splits: 0)
Lemmas       : 12510    (Deleted: 7749)
  Binary     : 1063     (Ratio:   8.50%)
  Ternary    : 432      (Ratio:   3.45%)
  Conflict   : 12510    (Average Length:  252.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 12510    (Average:  7.94 Max: 279 Sum:  99386)
  Executed   : 12486    (Average:  7.92 Max: 279 Sum:  99128 Ratio:  99.74%)
  Bounded    : 24       (Average: 10.75 Max:  17 Sum:    258 Ratio:   0.26%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 93745    (Eliminated:    0 Frozen: 27481)
Constraints  : 616110   (Binary:  91.4% Ternary:   6.9% Other:   1.7%)

Memory Peak  : 256MB
Max. Length  : 10 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.64s
Memory:		 256MB (+23MB)
UNKNOWN
Iteration Time:	 5.38s

Iteration 5
Queue:		 [(4,20,0,True), (5,25,0,True), (6,30,0,True)]
Grounded Until:	 15
Expected Memory: 280.0MB
Grounding...	 [('step', [16]), ('step', [17]), ('step', [18]), ('step', [19]), ('step', [20]), ('check', [20])]
Grounding Time:	 0.52s
Memory:		 260MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 6
Time         : 14.658s (Solving: 10.90s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 14.492s

Choices      : 211303   (Domain: 180150)
Conflicts    : 21112    (Analyzed: 21110)
Restarts     : 234      (Average: 90.21 Last: 88)
Model-Level  : 232.0   
Problems     : 6        (Average Length: 12.00 Splits: 0)
Lemmas       : 21110    (Deleted: 13943)
  Binary     : 1736     (Ratio:   8.22%)
  Ternary    : 559      (Ratio:   2.65%)
  Conflict   : 21110    (Average Length:  469.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 21110    (Average:  9.38 Max: 279 Sum: 198058)
  Executed   : 21086    (Average:  9.37 Max: 279 Sum: 197800 Ratio:  99.87%)
  Bounded    : 24       (Average: 10.75 Max:  17 Sum:    258 Ratio:   0.13%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 131236   (Eliminated:    0 Frozen: 39141)
Constraints  : 895929   (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 279MB
Max. Length  : 15 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.08s
Memory:		 276MB (+16MB)
UNKNOWN
Iteration Time:	 5.82s

Iteration 6
Queue:		 [(5,25,0,True), (6,30,0,True)]
Grounded Until:	 20
Expected Memory: 300.0MB
Grounding...	 [('step', [21]), ('step', [22]), ('step', [23]), ('step', [24]), ('step', [25]), ('check', [25])]
Grounding Time:	 0.59s
Memory:		 297MB (+21MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 7
Time         : 22.194s (Solving: 17.55s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 22.032s

Choices      : 342485   (Domain: 297737)
Conflicts    : 30164    (Analyzed: 30162)
Restarts     : 334      (Average: 90.31 Last: 140)
Model-Level  : 232.0   
Problems     : 7        (Average Length: 14.14 Splits: 0)
Lemmas       : 30162    (Deleted: 23746)
  Binary     : 2202     (Ratio:   7.30%)
  Ternary    : 639      (Ratio:   2.12%)
  Conflict   : 30162    (Average Length:  754.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 30162    (Average: 10.51 Max: 279 Sum: 317028)
  Executed   : 30138    (Average: 10.50 Max: 279 Sum: 316770 Ratio:  99.92%)
  Bounded    : 24       (Average: 10.75 Max:  17 Sum:    258 Ratio:   0.08%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 168727   (Eliminated:    0 Frozen: 50801)
Constraints  : 1178389  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 321MB
Max. Length  : 20 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.70s
Memory:		 309MB (+12MB)
UNKNOWN
Iteration Time:	 7.55s

Iteration 7
Queue:		 [(6,30,0,True)]
Grounded Until:	 25
Expected Memory: 342.0MB
Grounding...	 [('step', [26]), ('step', [27]), ('step', [28]), ('step', [29]), ('step', [30]), ('check', [30])]
Grounding Time:	 0.51s
Memory:		 320MB (+11MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 8
Time         : 29.950s (Solving: 24.48s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 29.792s

Choices      : 512179   (Domain: 456274)
Conflicts    : 39563    (Analyzed: 39561)
Restarts     : 434      (Average: 91.15 Last: 140)
Model-Level  : 232.0   
Problems     : 8        (Average Length: 16.38 Splits: 0)
Lemmas       : 39561    (Deleted: 31975)
  Binary     : 2733     (Ratio:   6.91%)
  Ternary    : 842      (Ratio:   2.13%)
  Conflict   : 39561    (Average Length:  835.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 39561    (Average: 12.00 Max: 376 Sum: 474587)
  Executed   : 39537    (Average: 11.99 Max: 376 Sum: 474329 Ratio:  99.95%)
  Bounded    : 24       (Average: 10.75 Max:  17 Sum:    258 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1460849  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 351MB
Max. Length  : 25 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.99s
Memory:		 351MB (+31MB)
UNKNOWN
Iteration Time:	 7.77s

Iteration 8
Queue:		 [(3,15,1,True), (4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 9
Time         : 35.005s (Solving: 29.48s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 34.848s

Choices      : 572468   (Domain: 513333)
Conflicts    : 48077    (Analyzed: 48075)
Restarts     : 534      (Average: 90.03 Last: 140)
Model-Level  : 232.0   
Problems     : 9        (Average Length: 18.11 Splits: 0)
Lemmas       : 48075    (Deleted: 38492)
  Binary     : 3056     (Ratio:   6.36%)
  Ternary    : 952      (Ratio:   1.98%)
  Conflict   : 48075    (Average Length:  744.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 48075    (Average: 11.05 Max: 376 Sum: 531408)
  Executed   : 48042    (Average: 11.04 Max: 376 Sum: 530893 Ratio:  99.90%)
  Bounded    : 33       (Average: 15.61 Max:  32 Sum:    515 Ratio:   0.10%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1460849  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 351MB
Max. Length  : 30 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.04s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 5.06s

Iteration 9
Queue:		 [(4,20,1,True), (5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 10
Time         : 41.742s (Solving: 36.16s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 41.588s

Choices      : 691097   (Domain: 625619)
Conflicts    : 57169    (Analyzed: 57167)
Restarts     : 634      (Average: 90.17 Last: 140)
Model-Level  : 232.0   
Problems     : 10       (Average Length: 19.50 Splits: 0)
Lemmas       : 57167    (Deleted: 47025)
  Binary     : 3594     (Ratio:   6.29%)
  Ternary    : 1037     (Ratio:   1.81%)
  Conflict   : 57167    (Average Length:  653.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 57167    (Average: 11.29 Max: 376 Sum: 645285)
  Executed   : 57116    (Average: 11.27 Max: 376 Sum: 644194 Ratio:  99.83%)
  Bounded    : 51       (Average: 21.39 Max:  32 Sum:   1091 Ratio:   0.17%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1447526  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 351MB
Max. Length  : 30 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.72s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 6.74s

Iteration 10
Queue:		 [(5,25,1,True), (6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 11
Time         : 48.237s (Solving: 42.60s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 48.084s

Choices      : 813665   (Domain: 742103)
Conflicts    : 65982    (Analyzed: 65980)
Restarts     : 734      (Average: 89.89 Last: 140)
Model-Level  : 232.0   
Problems     : 11       (Average Length: 20.64 Splits: 0)
Lemmas       : 65980    (Deleted: 55101)
  Binary     : 3910     (Ratio:   5.93%)
  Ternary    : 1091     (Ratio:   1.65%)
  Conflict   : 65980    (Average Length:  594.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 65980    (Average: 11.54 Max: 376 Sum: 761486)
  Executed   : 65928    (Average: 11.52 Max: 376 Sum: 760363 Ratio:  99.85%)
  Bounded    : 52       (Average: 21.60 Max:  32 Sum:   1123 Ratio:   0.15%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1421367  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 351MB
Max. Length  : 30 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.48s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 6.50s

Iteration 11
Queue:		 [(6,30,1,True), (7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 12
Time         : 54.791s (Solving: 49.10s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 54.640s

Choices      : 975683   (Domain: 896919)
Conflicts    : 75075    (Analyzed: 75073)
Restarts     : 834      (Average: 90.02 Last: 140)
Model-Level  : 232.0   
Problems     : 12       (Average Length: 21.58 Splits: 0)
Lemmas       : 75073    (Deleted: 63176)
  Binary     : 4079     (Ratio:   5.43%)
  Ternary    : 1153     (Ratio:   1.54%)
  Conflict   : 75073    (Average Length:  548.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 75073    (Average: 12.21 Max: 379 Sum: 916690)
  Executed   : 75011    (Average: 12.19 Max: 379 Sum: 915267 Ratio:  99.84%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.16%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 206218   (Eliminated:    0 Frozen: 62461)
Constraints  : 1421353  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 351MB
Max. Length  : 30 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.54s
Memory:		 351MB (+0MB)
UNKNOWN
Iteration Time:	 6.56s

Iteration 12
Queue:		 [(7,35,0,True), (8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 30
Expected Memory: 393.0MB
Grounding...	 [('step', [31]), ('step', [32]), ('step', [33]), ('step', [34]), ('step', [35]), ('check', [35])]
Grounding Time:	 0.51s
Memory:		 351MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 13
Time         : 62.263s (Solving: 55.73s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 62.116s

Choices      : 1166383  (Domain: 1081139)
Conflicts    : 83872    (Analyzed: 83870)
Restarts     : 934      (Average: 89.80 Last: 140)
Model-Level  : 232.0   
Problems     : 13       (Average Length: 22.77 Splits: 0)
Lemmas       : 83870    (Deleted: 73543)
  Binary     : 4283     (Ratio:   5.11%)
  Ternary    : 1158     (Ratio:   1.38%)
  Conflict   : 83870    (Average Length:  577.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 83870    (Average: 13.07 Max: 379 Sum: 1095790)
  Executed   : 83808    (Average: 13.05 Max: 379 Sum: 1094367 Ratio:  99.87%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.13%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 243709   (Eliminated:    0 Frozen: 74121)
Constraints  : 1698855  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 387MB
Max. Length  : 30 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.69s
Memory:		 366MB (+15MB)
UNKNOWN
Iteration Time:	 7.49s

Iteration 13
Queue:		 [(8,40,0,True), (9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 35
Expected Memory: 408.0MB
Grounding...	 [('step', [36]), ('step', [37]), ('step', [38]), ('step', [39]), ('step', [40]), ('check', [40])]
Grounding Time:	 0.52s
Memory:		 373MB (+7MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 14
Time         : 70.787s (Solving: 63.38s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 70.644s

Choices      : 1441455  (Domain: 1349673)
Conflicts    : 93173    (Analyzed: 93171)
Restarts     : 1034     (Average: 90.11 Last: 171)
Model-Level  : 232.0   
Problems     : 14       (Average Length: 24.14 Splits: 0)
Lemmas       : 93171    (Deleted: 81922)
  Binary     : 4510     (Ratio:   4.84%)
  Ternary    : 1170     (Ratio:   1.26%)
  Conflict   : 93171    (Average Length:  591.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 93171    (Average: 14.57 Max: 379 Sum: 1357385)
  Executed   : 93109    (Average: 14.55 Max: 379 Sum: 1355962 Ratio:  99.90%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.10%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 281200   (Eliminated:    0 Frozen: 85781)
Constraints  : 1981315  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 413MB
Max. Length  : 35 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.72s
Memory:		 388MB (+15MB)
UNKNOWN
Iteration Time:	 8.54s

Iteration 14
Queue:		 [(9,45,0,True), (10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 40
Expected Memory: 430.0MB
Grounding...	 [('step', [41]), ('step', [42]), ('step', [43]), ('step', [44]), ('step', [45]), ('check', [45])]
Grounding Time:	 0.55s
Memory:		 398MB (+10MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 15
Time         : 78.832s (Solving: 70.49s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 78.692s

Choices      : 1705836  (Domain: 1608291)
Conflicts    : 101908   (Analyzed: 101906)
Restarts     : 1134     (Average: 89.86 Last: 171)
Model-Level  : 232.0   
Problems     : 15       (Average Length: 25.67 Splits: 0)
Lemmas       : 101906   (Deleted: 90852)
  Binary     : 4725     (Ratio:   4.64%)
  Ternary    : 1182     (Ratio:   1.16%)
  Conflict   : 101906   (Average Length:  611.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 101906   (Average: 15.76 Max: 379 Sum: 1606482)
  Executed   : 101844   (Average: 15.75 Max: 379 Sum: 1605059 Ratio:  99.91%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.09%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 318691   (Eliminated:    0 Frozen: 97441)
Constraints  : 2263775  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 444MB
Max. Length  : 40 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.19s
Memory:		 443MB (+45MB)
UNKNOWN
Iteration Time:	 8.06s

Iteration 15
Queue:		 [(10,50,0,True), (11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 45
Expected Memory: 498.0MB
Grounding...	 [('step', [46]), ('step', [47]), ('step', [48]), ('step', [49]), ('step', [50]), ('check', [50])]
Grounding Time:	 0.71s
Memory:		 455MB (+12MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 16
Time         : 87.817s (Solving: 78.36s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 87.684s

Choices      : 2055917  (Domain: 1950118)
Conflicts    : 111026   (Analyzed: 111024)
Restarts     : 1234     (Average: 89.97 Last: 171)
Model-Level  : 232.0   
Problems     : 16       (Average Length: 27.31 Splits: 0)
Lemmas       : 111024   (Deleted: 99174)
  Binary     : 4895     (Ratio:   4.41%)
  Ternary    : 1192     (Ratio:   1.07%)
  Conflict   : 111024   (Average Length:  621.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 111024   (Average: 17.46 Max: 446 Sum: 1938272)
  Executed   : 110962   (Average: 17.45 Max: 446 Sum: 1936849 Ratio:  99.93%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 356182   (Eliminated:    0 Frozen: 109101)
Constraints  : 2546235  (Binary:  91.3% Ternary:   6.9% Other:   1.8%)

Memory Peak  : 503MB
Max. Length  : 45 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.95s
Memory:		 466MB (+11MB)
UNKNOWN
Iteration Time:	 9.00s

Iteration 16
Queue:		 [(11,55,0,True), (12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 50
Expected Memory: 521.0MB
Grounding...	 [('step', [51]), ('step', [52]), ('step', [53]), ('step', [54]), ('step', [55]), ('check', [55])]
Grounding Time:	 0.51s
Memory:		 470MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 17
Time         : 97.681s (Solving: 87.30s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 97.552s

Choices      : 2398484  (Domain: 2284416)
Conflicts    : 119941   (Analyzed: 119939)
Restarts     : 1334     (Average: 89.91 Last: 171)
Model-Level  : 232.0   
Problems     : 17       (Average Length: 29.06 Splits: 0)
Lemmas       : 119939   (Deleted: 107938)
  Binary     : 5014     (Ratio:   4.18%)
  Ternary    : 1207     (Ratio:   1.01%)
  Conflict   : 119939   (Average Length:  645.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 119939   (Average: 18.85 Max: 499 Sum: 2260480)
  Executed   : 119877   (Average: 18.84 Max: 499 Sum: 2259057 Ratio:  99.94%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 393673   (Eliminated:    0 Frozen: 120761)
Constraints  : 2828695  (Binary:  91.3% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 526MB
Max. Length  : 50 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.03s
Memory:		 489MB (+19MB)
UNKNOWN
Iteration Time:	 9.88s

Iteration 17
Queue:		 [(12,60,0,True), (13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 55
Expected Memory: 544.0MB
Grounding...	 [('step', [56]), ('step', [57]), ('step', [58]), ('step', [59]), ('step', [60]), ('check', [60])]
Grounding Time:	 0.51s
Memory:		 495MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 18
Time         : 106.588s (Solving: 95.26s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 106.464s

Choices      : 2642560  (Domain: 2523631)
Conflicts    : 127720   (Analyzed: 127718)
Restarts     : 1434     (Average: 89.06 Last: 171)
Model-Level  : 232.0   
Problems     : 18       (Average Length: 30.89 Splits: 0)
Lemmas       : 127718   (Deleted: 114420)
  Binary     : 5093     (Ratio:   3.99%)
  Ternary    : 1214     (Ratio:   0.95%)
  Conflict   : 127718   (Average Length:  676.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 127718   (Average: 19.44 Max: 569 Sum: 2482581)
  Executed   : 127656   (Average: 19.43 Max: 569 Sum: 2481158 Ratio:  99.94%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 431164   (Eliminated:    0 Frozen: 132421)
Constraints  : 3111155  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 556MB
Max. Length  : 55 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.05s
Memory:		 552MB (+57MB)
UNKNOWN
Iteration Time:	 8.92s

Iteration 18
Queue:		 [(13,65,0,True), (14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 60
Expected Memory: 615.0MB
Grounding...	 [('step', [61]), ('step', [62]), ('step', [63]), ('step', [64]), ('step', [65]), ('check', [65])]
Grounding Time:	 0.55s
Memory:		 552MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 19
Time         : 116.529s (Solving: 104.18s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 116.408s

Choices      : 2932709  (Domain: 2808890)
Conflicts    : 135866   (Analyzed: 135864)
Restarts     : 1534     (Average: 88.57 Last: 171)
Model-Level  : 232.0   
Problems     : 19       (Average Length: 32.79 Splits: 0)
Lemmas       : 135864   (Deleted: 121994)
  Binary     : 5150     (Ratio:   3.79%)
  Ternary    : 1221     (Ratio:   0.90%)
  Conflict   : 135864   (Average Length:  710.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 135864   (Average: 20.22 Max: 611 Sum: 2747824)
  Executed   : 135802   (Average: 20.21 Max: 611 Sum: 2746401 Ratio:  99.95%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 468655   (Eliminated:    0 Frozen: 144081)
Constraints  : 3393615  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 610MB
Max. Length  : 60 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.02s
Memory:		 558MB (+6MB)
UNKNOWN
Iteration Time:	 9.95s

Iteration 19
Queue:		 [(14,70,0,True), (15,75,0,True), (16,80,0,True)]
Grounded Until:	 65
Expected Memory: 621.0MB
Grounding...	 [('step', [66]), ('step', [67]), ('step', [68]), ('step', [69]), ('step', [70]), ('check', [70])]
Grounding Time:	 0.69s
Memory:		 562MB (+4MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 20
Time         : 127.471s (Solving: 113.82s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 127.356s

Choices      : 3303866  (Domain: 3174338)
Conflicts    : 144117   (Analyzed: 144115)
Restarts     : 1634     (Average: 88.20 Last: 171)
Model-Level  : 232.0   
Problems     : 20       (Average Length: 34.75 Splits: 0)
Lemmas       : 144115   (Deleted: 129925)
  Binary     : 5189     (Ratio:   3.60%)
  Ternary    : 1228     (Ratio:   0.85%)
  Conflict   : 144115   (Average Length:  754.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 144115   (Average: 21.46 Max: 635 Sum: 3093045)
  Executed   : 144053   (Average: 21.45 Max: 635 Sum: 3091622 Ratio:  99.95%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 506146   (Eliminated:    0 Frozen: 155741)
Constraints  : 3676075  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 632MB
Max. Length  : 65 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.77s
Memory:		 583MB (+21MB)
UNKNOWN
Iteration Time:	 10.96s

Iteration 20
Queue:		 [(15,75,0,True), (16,80,0,True)]
Grounded Until:	 70
Expected Memory: 646.0MB
Grounding...	 [('step', [71]), ('step', [72]), ('step', [73]), ('step', [74]), ('step', [75]), ('check', [75])]
Grounding Time:	 0.52s
Memory:		 586MB (+3MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 21
Time         : 138.933s (Solving: 124.26s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 138.824s

Choices      : 3707054  (Domain: 3571644)
Conflicts    : 152100   (Analyzed: 152098)
Restarts     : 1734     (Average: 87.72 Last: 171)
Model-Level  : 232.0   
Problems     : 21       (Average Length: 36.76 Splits: 0)
Lemmas       : 152098   (Deleted: 137993)
  Binary     : 5235     (Ratio:   3.44%)
  Ternary    : 1231     (Ratio:   0.81%)
  Conflict   : 152098   (Average Length:  787.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 152098   (Average: 22.81 Max: 738 Sum: 3468709)
  Executed   : 152036   (Average: 22.80 Max: 738 Sum: 3467286 Ratio:  99.96%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.04%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 543637   (Eliminated:    0 Frozen: 167401)
Constraints  : 3958535  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 667MB
Max. Length  : 70 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.55s
Memory:		 612MB (+26MB)
UNKNOWN
Iteration Time:	 11.48s

Iteration 21
Queue:		 [(16,80,0,True)]
Grounded Until:	 75
Expected Memory: 675.0MB
Grounding...	 [('step', [76]), ('step', [77]), ('step', [78]), ('step', [79]), ('step', [80]), ('check', [80])]
Grounding Time:	 0.55s
Memory:		 612MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 22
Time         : 149.974s (Solving: 134.21s 1st Model: 0.05s Unsat: 1.21s)
CPU Time     : 149.872s

Choices      : 4059006  (Domain: 3920012)
Conflicts    : 160160   (Analyzed: 160158)
Restarts     : 1834     (Average: 87.33 Last: 171)
Model-Level  : 232.0   
Problems     : 22       (Average Length: 38.82 Splits: 0)
Lemmas       : 160158   (Deleted: 145865)
  Binary     : 5268     (Ratio:   3.29%)
  Ternary    : 1232     (Ratio:   0.77%)
  Conflict   : 160158   (Average Length:  816.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 160158   (Average: 23.68 Max: 757 Sum: 3792366)
  Executed   : 160096   (Average: 23.67 Max: 757 Sum: 3790943 Ratio:  99.96%)
  Bounded    : 62       (Average: 22.95 Max:  32 Sum:   1423 Ratio:   0.04%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4240995  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 75 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.07s
Memory:		 634MB (+22MB)
UNKNOWN
Iteration Time:	 11.06s

Iteration 22
Queue:		 [(3,15,2,True), (4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0
Calls        : 23
Time         : 153.223s (Solving: 137.32s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 153.120s

Choices      : 4102110  (Domain: 3956848)
Conflicts    : 165846   (Analyzed: 165843)
Restarts     : 1896     (Average: 87.47 Last: 171)
Model-Level  : 232.0   
Problems     : 23       (Average Length: 40.70 Splits: 0)
Lemmas       : 165843   (Deleted: 151150)
  Binary     : 5391     (Ratio:   3.25%)
  Ternary    : 1260     (Ratio:   0.76%)
  Conflict   : 165843   (Average Length:  798.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 165843   (Average: 23.11 Max: 757 Sum: 3832765)
  Executed   : 165780   (Average: 23.10 Max: 757 Sum: 3831341 Ratio:  99.96%)
  Bounded    : 63       (Average: 22.60 Max:  32 Sum:   1424 Ratio:   0.04%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4240995  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 3.20s
Memory:		 634MB (+0MB)
UNSAT
Iteration Time:	 3.25s

Iteration 23
Queue:		 [(4,20,2,True), (5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 24
Time         : 159.643s (Solving: 143.60s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 159.544s

Choices      : 4185039  (Domain: 4034081)
Conflicts    : 175012   (Analyzed: 175009)
Restarts     : 1996     (Average: 87.68 Last: 171)
Model-Level  : 232.0   
Problems     : 24       (Average Length: 42.42 Splits: 0)
Lemmas       : 175009   (Deleted: 158813)
  Binary     : 5520     (Ratio:   3.15%)
  Ternary    : 1305     (Ratio:   0.75%)
  Conflict   : 175009   (Average Length:  768.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 175009   (Average: 22.34 Max: 757 Sum: 3909668)
  Executed   : 174941   (Average: 22.33 Max: 757 Sum: 3907844 Ratio:  99.95%)
  Bounded    : 68       (Average: 26.82 Max:  82 Sum:   1824 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4240995  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.37s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 6.43s

Iteration 24
Queue:		 [(5,25,2,True), (6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 25
Time         : 165.668s (Solving: 149.50s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 165.572s

Choices      : 4286134  (Domain: 4130555)
Conflicts    : 183460   (Analyzed: 183457)
Restarts     : 2096     (Average: 87.53 Last: 171)
Model-Level  : 232.0   
Problems     : 25       (Average Length: 44.00 Splits: 0)
Lemmas       : 183457   (Deleted: 165507)
  Binary     : 5683     (Ratio:   3.10%)
  Ternary    : 1337     (Ratio:   0.73%)
  Conflict   : 183457   (Average Length:  742.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 183457   (Average: 21.82 Max: 757 Sum: 4003175)
  Executed   : 183385   (Average: 21.81 Max: 757 Sum: 4001028 Ratio:  99.95%)
  Bounded    : 72       (Average: 29.82 Max:  82 Sum:   2147 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4238341  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.98s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 6.03s

Iteration 25
Queue:		 [(6,30,2,True), (7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 26
Time         : 173.591s (Solving: 157.30s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 173.500s

Choices      : 4427678  (Domain: 4268820)
Conflicts    : 192474   (Analyzed: 192471)
Restarts     : 2196     (Average: 87.65 Last: 171)
Model-Level  : 232.0   
Problems     : 26       (Average Length: 45.46 Splits: 0)
Lemmas       : 192471   (Deleted: 175226)
  Binary     : 5896     (Ratio:   3.06%)
  Ternary    : 1418     (Ratio:   0.74%)
  Conflict   : 192471   (Average Length:  715.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 192471   (Average: 21.50 Max: 757 Sum: 4138345)
  Executed   : 192393   (Average: 21.49 Max: 757 Sum: 4135707 Ratio:  99.94%)
  Bounded    : 78       (Average: 33.82 Max:  82 Sum:   2638 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4235686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.88s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 7.93s

Iteration 26
Queue:		 [(7,35,1,True), (8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 27
Time         : 181.098s (Solving: 164.69s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 181.012s

Choices      : 4592519  (Domain: 4428597)
Conflicts    : 201935   (Analyzed: 201932)
Restarts     : 2296     (Average: 87.95 Last: 171)
Model-Level  : 232.0   
Problems     : 27       (Average Length: 46.81 Splits: 0)
Lemmas       : 201932   (Deleted: 183642)
  Binary     : 6076     (Ratio:   3.01%)
  Ternary    : 1447     (Ratio:   0.72%)
  Conflict   : 201932   (Average Length:  693.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 201932   (Average: 21.26 Max: 757 Sum: 4293207)
  Executed   : 201850   (Average: 21.25 Max: 757 Sum: 4290246 Ratio:  99.93%)
  Bounded    : 82       (Average: 36.11 Max:  82 Sum:   2961 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4235616  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.47s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 7.51s

Iteration 27
Queue:		 [(8,40,1,True), (9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 28
Time         : 187.709s (Solving: 171.19s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 187.624s

Choices      : 4727569  (Domain: 4561362)
Conflicts    : 210487   (Analyzed: 210484)
Restarts     : 2396     (Average: 87.85 Last: 171)
Model-Level  : 232.0   
Problems     : 28       (Average Length: 48.07 Splits: 0)
Lemmas       : 210484   (Deleted: 190748)
  Binary     : 6158     (Ratio:   2.93%)
  Ternary    : 1477     (Ratio:   0.70%)
  Conflict   : 210484   (Average Length:  679.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 210484   (Average: 20.97 Max: 757 Sum: 4414229)
  Executed   : 210402   (Average: 20.96 Max: 757 Sum: 4411268 Ratio:  99.93%)
  Bounded    : 82       (Average: 36.11 Max:  82 Sum:   2961 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4233123  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.57s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 6.62s

Iteration 28
Queue:		 [(9,45,1,True), (10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 29
Time         : 195.681s (Solving: 179.05s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 195.600s

Choices      : 4887925  (Domain: 4719575)
Conflicts    : 219292   (Analyzed: 219289)
Restarts     : 2496     (Average: 87.86 Last: 171)
Model-Level  : 232.0   
Problems     : 29       (Average Length: 49.24 Splits: 0)
Lemmas       : 219289   (Deleted: 200807)
  Binary     : 6237     (Ratio:   2.84%)
  Ternary    : 1495     (Ratio:   0.68%)
  Conflict   : 219289   (Average Length:  664.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 219289   (Average: 20.81 Max: 757 Sum: 4562664)
  Executed   : 219206   (Average: 20.79 Max: 757 Sum: 4559621 Ratio:  99.93%)
  Bounded    : 83       (Average: 36.66 Max:  82 Sum:   3043 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4233123  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.94s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 7.98s

Iteration 29
Queue:		 [(10,50,1,True), (11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 30
Time         : 203.399s (Solving: 186.63s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 203.316s

Choices      : 5071989  (Domain: 4901353)
Conflicts    : 228260   (Analyzed: 228257)
Restarts     : 2596     (Average: 87.93 Last: 171)
Model-Level  : 232.0   
Problems     : 30       (Average Length: 50.33 Splits: 0)
Lemmas       : 228257   (Deleted: 209279)
  Binary     : 6308     (Ratio:   2.76%)
  Ternary    : 1518     (Ratio:   0.67%)
  Conflict   : 228257   (Average Length:  651.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 228257   (Average: 20.74 Max: 757 Sum: 4733668)
  Executed   : 228171   (Average: 20.72 Max: 757 Sum: 4730379 Ratio:  99.93%)
  Bounded    : 86       (Average: 38.24 Max:  82 Sum:   3289 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4233109  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.66s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 7.72s

Iteration 30
Queue:		 [(11,55,1,True), (12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 31
Time         : 211.840s (Solving: 194.95s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 211.764s

Choices      : 5313058  (Domain: 5140075)
Conflicts    : 236990   (Analyzed: 236987)
Restarts     : 2696     (Average: 87.90 Last: 171)
Model-Level  : 232.0   
Problems     : 31       (Average Length: 51.35 Splits: 0)
Lemmas       : 236987   (Deleted: 217931)
  Binary     : 6370     (Ratio:   2.69%)
  Ternary    : 1537     (Ratio:   0.65%)
  Conflict   : 236987   (Average Length:  639.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 236987   (Average: 20.93 Max: 757 Sum: 4959477)
  Executed   : 236898   (Average: 20.91 Max: 757 Sum: 4955942 Ratio:  99.93%)
  Bounded    : 89       (Average: 39.72 Max:  82 Sum:   3535 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225687  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.41s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 8.45s

Iteration 31
Queue:		 [(12,60,1,True), (13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 32
Time         : 221.004s (Solving: 203.98s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 220.932s

Choices      : 5542471  (Domain: 5367579)
Conflicts    : 246068   (Analyzed: 246065)
Restarts     : 2796     (Average: 88.01 Last: 171)
Model-Level  : 232.0   
Problems     : 32       (Average Length: 52.31 Splits: 0)
Lemmas       : 246065   (Deleted: 226327)
  Binary     : 6435     (Ratio:   2.62%)
  Ternary    : 1552     (Ratio:   0.63%)
  Conflict   : 246065   (Average Length:  626.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 246065   (Average: 21.03 Max: 757 Sum: 5175088)
  Executed   : 245976   (Average: 21.02 Max: 757 Sum: 5171553 Ratio:  99.93%)
  Bounded    : 89       (Average: 39.72 Max:  82 Sum:   3535 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225645  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.12s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 9.17s

Iteration 32
Queue:		 [(13,65,1,True), (14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 33
Time         : 229.704s (Solving: 212.56s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 229.636s

Choices      : 5750754  (Domain: 5573773)
Conflicts    : 255157   (Analyzed: 255154)
Restarts     : 2896     (Average: 88.11 Last: 171)
Model-Level  : 232.0   
Problems     : 33       (Average Length: 53.21 Splits: 0)
Lemmas       : 255154   (Deleted: 235100)
  Binary     : 6488     (Ratio:   2.54%)
  Ternary    : 1566     (Ratio:   0.61%)
  Conflict   : 255154   (Average Length:  614.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 255154   (Average: 21.03 Max: 838 Sum: 5366586)
  Executed   : 255064   (Average: 21.02 Max: 838 Sum: 5362969 Ratio:  99.93%)
  Bounded    : 90       (Average: 40.19 Max:  82 Sum:   3617 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225645  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.67s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 8.71s

Iteration 33
Queue:		 [(14,70,1,True), (15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 34
Time         : 239.332s (Solving: 222.04s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 239.268s

Choices      : 6060054  (Domain: 5880820)
Conflicts    : 264307   (Analyzed: 264304)
Restarts     : 2996     (Average: 88.22 Last: 171)
Model-Level  : 232.0   
Problems     : 34       (Average Length: 54.06 Splits: 0)
Lemmas       : 264304   (Deleted: 243919)
  Binary     : 6557     (Ratio:   2.48%)
  Ternary    : 1576     (Ratio:   0.60%)
  Conflict   : 264304   (Average Length:  605.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 264304   (Average: 21.40 Max: 838 Sum: 5655935)
  Executed   : 264212   (Average: 21.39 Max: 838 Sum: 5652154 Ratio:  99.93%)
  Bounded    : 92       (Average: 41.10 Max:  82 Sum:   3781 Ratio:   0.07%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225619  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.58s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 9.64s

Iteration 34
Queue:		 [(15,75,1,True), (16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 35
Time         : 249.187s (Solving: 231.77s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 249.128s

Choices      : 6410855  (Domain: 6229173)
Conflicts    : 273012   (Analyzed: 273009)
Restarts     : 3096     (Average: 88.18 Last: 171)
Model-Level  : 232.0   
Problems     : 35       (Average Length: 54.86 Splits: 0)
Lemmas       : 273009   (Deleted: 252778)
  Binary     : 6645     (Ratio:   2.43%)
  Ternary    : 1588     (Ratio:   0.58%)
  Conflict   : 273009   (Average Length:  596.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 273009   (Average: 21.94 Max: 838 Sum: 5989657)
  Executed   : 272916   (Average: 21.93 Max: 838 Sum: 5985794 Ratio:  99.94%)
  Bounded    : 93       (Average: 41.54 Max:  82 Sum:   3863 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225591  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.81s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 9.86s

Iteration 35
Queue:		 [(16,80,1,True), (17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 36
Time         : 260.772s (Solving: 243.21s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 260.716s

Choices      : 6824452  (Domain: 6640165)
Conflicts    : 282018   (Analyzed: 282015)
Restarts     : 3196     (Average: 88.24 Last: 171)
Model-Level  : 232.0   
Problems     : 36       (Average Length: 55.61 Splits: 0)
Lemmas       : 282015   (Deleted: 261088)
  Binary     : 6710     (Ratio:   2.38%)
  Ternary    : 1606     (Ratio:   0.57%)
  Conflict   : 282015   (Average Length:  588.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 282015   (Average: 22.64 Max: 858 Sum: 6385189)
  Executed   : 281919   (Average: 22.63 Max: 858 Sum: 6381080 Ratio:  99.94%)
  Bounded    : 96       (Average: 42.80 Max:  82 Sum:   4109 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 581128   (Eliminated:    0 Frozen: 179061)
Constraints  : 4225577  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 693MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 11.53s
Memory:		 634MB (+0MB)
UNKNOWN
Iteration Time:	 11.59s

Iteration 36
Queue:		 [(17,85,0,True), (18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 80
Expected Memory: 697.0MB
Grounding...	 [('step', [81]), ('step', [82]), ('step', [83]), ('step', [84]), ('step', [85]), ('check', [85])]
Grounding Time:	 0.54s
Memory:		 634MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 37
Time         : 271.623s (Solving: 252.97s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 271.572s

Choices      : 7411320  (Domain: 7222276)
Conflicts    : 291091   (Analyzed: 291088)
Restarts     : 3296     (Average: 88.32 Last: 171)
Model-Level  : 232.0   
Problems     : 37       (Average Length: 56.46 Splits: 0)
Lemmas       : 291088   (Deleted: 271360)
  Binary     : 6802     (Ratio:   2.34%)
  Ternary    : 1620     (Ratio:   0.56%)
  Conflict   : 291088   (Average Length:  592.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 291088   (Average: 23.86 Max: 858 Sum: 6944736)
  Executed   : 290992   (Average: 23.84 Max: 858 Sum: 6940627 Ratio:  99.94%)
  Bounded    : 96       (Average: 42.80 Max:  82 Sum:   4109 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 618619   (Eliminated:    0 Frozen: 190721)
Constraints  : 4507997  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 721MB
Max. Length  : 80 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.88s
Memory:		 656MB (+22MB)
UNKNOWN
Iteration Time:	 10.86s

Iteration 37
Queue:		 [(18,90,0,True), (19,95,0,True), (20,100,0,True)]
Grounded Until:	 85
Expected Memory: 719.0MB
Grounding...	 [('step', [86]), ('step', [87]), ('step', [88]), ('step', [89]), ('step', [90]), ('check', [90])]
Grounding Time:	 0.54s
Memory:		 656MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 38
Time         : 282.965s (Solving: 263.19s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 282.920s

Choices      : 7871747  (Domain: 7678415)
Conflicts    : 300144   (Analyzed: 300141)
Restarts     : 3396     (Average: 88.38 Last: 171)
Model-Level  : 232.0   
Problems     : 38       (Average Length: 57.39 Splits: 0)
Lemmas       : 300141   (Deleted: 279896)
  Binary     : 6830     (Ratio:   2.28%)
  Ternary    : 1624     (Ratio:   0.54%)
  Conflict   : 300141   (Average Length:  607.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 300141   (Average: 24.57 Max: 872 Sum: 7372975)
  Executed   : 300045   (Average: 24.55 Max: 872 Sum: 7368866 Ratio:  99.94%)
  Bounded    : 96       (Average: 42.80 Max:  82 Sum:   4109 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 656110   (Eliminated:    0 Frozen: 202381)
Constraints  : 4790457  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 747MB
Max. Length  : 85 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.35s
Memory:		 736MB (+80MB)
UNKNOWN
Iteration Time:	 11.36s

Iteration 38
Queue:		 [(19,95,0,True), (20,100,0,True)]
Grounded Until:	 90
Expected Memory: 816.0MB
Grounding...	 [('step', [91]), ('step', [92]), ('step', [93]), ('step', [94]), ('step', [95]), ('check', [95])]
Grounding Time:	 0.57s
Memory:		 736MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 39
Time         : 294.377s (Solving: 273.45s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 294.336s

Choices      : 8308208  (Domain: 8111509)
Conflicts    : 308200   (Analyzed: 308197)
Restarts     : 3496     (Average: 88.16 Last: 171)
Model-Level  : 232.0   
Problems     : 39       (Average Length: 58.41 Splits: 0)
Lemmas       : 308197   (Deleted: 287291)
  Binary     : 6860     (Ratio:   2.23%)
  Ternary    : 1625     (Ratio:   0.53%)
  Conflict   : 308197   (Average Length:  622.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 308197   (Average: 25.23 Max: 908 Sum: 7776203)
  Executed   : 308101   (Average: 25.22 Max: 908 Sum: 7772094 Ratio:  99.95%)
  Bounded    : 96       (Average: 42.80 Max:  82 Sum:   4109 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 693601   (Eliminated:    0 Frozen: 214041)
Constraints  : 5072917  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 821MB
Max. Length  : 90 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.39s
Memory:		 741MB (+5MB)
UNKNOWN
Iteration Time:	 11.43s

Iteration 39
Queue:		 [(20,100,0,True)]
Grounded Until:	 95
Expected Memory: 821.0MB
Grounding...	 [('step', [96]), ('step', [97]), ('step', [98]), ('step', [99]), ('step', [100]), ('check', [100])]
Grounding Time:	 0.89s
Memory:		 791MB (+50MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 40
Time         : 306.163s (Solving: 283.74s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 306.128s

Choices      : 8710733  (Domain: 8511380)
Conflicts    : 316103   (Analyzed: 316100)
Restarts     : 3596     (Average: 87.90 Last: 171)
Model-Level  : 232.0   
Problems     : 40       (Average Length: 59.50 Splits: 0)
Lemmas       : 316100   (Deleted: 295218)
  Binary     : 6901     (Ratio:   2.18%)
  Ternary    : 1637     (Ratio:   0.52%)
  Conflict   : 316100   (Average Length:  638.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 316100   (Average: 25.76 Max: 976 Sum: 8144273)
  Executed   : 316004   (Average: 25.75 Max: 976 Sum: 8140164 Ratio:  99.95%)
  Bounded    : 96       (Average: 42.80 Max:  82 Sum:   4109 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5355377  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 95 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.43s
Memory:		 796MB (+5MB)
UNKNOWN
Iteration Time:	 11.80s

Iteration 40
Queue:		 [(4,20,3,True), (5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 41
Time         : 312.207s (Solving: 289.62s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 312.176s

Choices      : 8779008  (Domain: 8577752)
Conflicts    : 324510   (Analyzed: 324507)
Restarts     : 3696     (Average: 87.80 Last: 171)
Model-Level  : 232.0   
Problems     : 41       (Average Length: 60.54 Splits: 0)
Lemmas       : 324507   (Deleted: 301177)
  Binary     : 6958     (Ratio:   2.14%)
  Ternary    : 1650     (Ratio:   0.51%)
  Conflict   : 324507   (Average Length:  627.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 324507   (Average: 25.28 Max: 976 Sum: 8204966)
  Executed   : 324410   (Average: 25.27 Max: 976 Sum: 8200755 Ratio:  99.95%)
  Bounded    : 97       (Average: 43.41 Max: 102 Sum:   4211 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5355377  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.99s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 6.05s

Iteration 41
Queue:		 [(5,25,3,True), (6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 42
Time         : 318.722s (Solving: 295.99s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 318.692s

Choices      : 8860079  (Domain: 8657179)
Conflicts    : 332935   (Analyzed: 332932)
Restarts     : 3796     (Average: 87.71 Last: 171)
Model-Level  : 232.0   
Problems     : 42       (Average Length: 61.52 Splits: 0)
Lemmas       : 332932   (Deleted: 308970)
  Binary     : 7018     (Ratio:   2.11%)
  Ternary    : 1657     (Ratio:   0.50%)
  Conflict   : 332932   (Average Length:  618.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 332932   (Average: 24.86 Max: 976 Sum: 8278011)
  Executed   : 332835   (Average: 24.85 Max: 976 Sum: 8273800 Ratio:  99.95%)
  Bounded    : 97       (Average: 43.41 Max: 102 Sum:   4211 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352748  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.47s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 6.52s

Iteration 42
Queue:		 [(6,30,3,True), (7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 43
Time         : 326.155s (Solving: 303.28s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 326.128s

Choices      : 8969018  (Domain: 8764164)
Conflicts    : 341388   (Analyzed: 341385)
Restarts     : 3896     (Average: 87.62 Last: 171)
Model-Level  : 232.0   
Problems     : 43       (Average Length: 62.47 Splits: 0)
Lemmas       : 341385   (Deleted: 317209)
  Binary     : 7071     (Ratio:   2.07%)
  Ternary    : 1684     (Ratio:   0.49%)
  Conflict   : 341385   (Average Length:  609.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 341385   (Average: 24.54 Max: 976 Sum: 8377527)
  Executed   : 341288   (Average: 24.53 Max: 976 Sum: 8373316 Ratio:  99.95%)
  Bounded    : 97       (Average: 43.41 Max: 102 Sum:   4211 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352748  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.38s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.44s

Iteration 43
Queue:		 [(7,35,2,True), (8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 44
Time         : 333.597s (Solving: 310.58s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 333.576s

Choices      : 9054468  (Domain: 8848518)
Conflicts    : 349464   (Analyzed: 349461)
Restarts     : 3996     (Average: 87.45 Last: 171)
Model-Level  : 232.0   
Problems     : 44       (Average Length: 63.36 Splits: 0)
Lemmas       : 349461   (Deleted: 325382)
  Binary     : 7126     (Ratio:   2.04%)
  Ternary    : 1707     (Ratio:   0.49%)
  Conflict   : 349461   (Average Length:  602.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 349461   (Average: 24.19 Max: 976 Sum: 8453195)
  Executed   : 349363   (Average: 24.18 Max: 976 Sum: 8448882 Ratio:  99.95%)
  Bounded    : 98       (Average: 44.01 Max: 102 Sum:   4313 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352748  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.40s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.45s

Iteration 44
Queue:		 [(8,40,2,True), (9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 45
Time         : 340.901s (Solving: 317.71s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 340.868s

Choices      : 9186967  (Domain: 8978634)
Conflicts    : 357687   (Analyzed: 357684)
Restarts     : 4096     (Average: 87.33 Last: 171)
Model-Level  : 232.0   
Problems     : 45       (Average Length: 64.22 Splits: 0)
Lemmas       : 357684   (Deleted: 333183)
  Binary     : 7178     (Ratio:   2.01%)
  Ternary    : 1714     (Ratio:   0.48%)
  Conflict   : 357684   (Average Length:  592.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 357684   (Average: 23.98 Max: 976 Sum: 8575597)
  Executed   : 357586   (Average: 23.96 Max: 976 Sum: 8571284 Ratio:  99.95%)
  Bounded    : 98       (Average: 44.01 Max: 102 Sum:   4313 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352722  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.23s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.30s

Iteration 45
Queue:		 [(9,45,2,True), (10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 46
Time         : 348.726s (Solving: 325.35s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 348.696s

Choices      : 9343737  (Domain: 9133438)
Conflicts    : 365581   (Analyzed: 365578)
Restarts     : 4196     (Average: 87.13 Last: 171)
Model-Level  : 232.0   
Problems     : 46       (Average Length: 65.04 Splits: 0)
Lemmas       : 365578   (Deleted: 341177)
  Binary     : 7228     (Ratio:   1.98%)
  Ternary    : 1721     (Ratio:   0.47%)
  Conflict   : 365578   (Average Length:  585.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 365578   (Average: 23.86 Max: 976 Sum: 8721816)
  Executed   : 365479   (Average: 23.85 Max: 976 Sum: 8717401 Ratio:  99.95%)
  Bounded    : 99       (Average: 44.60 Max: 102 Sum:   4415 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352722  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.76s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.83s

Iteration 46
Queue:		 [(10,50,2,True), (11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 47
Time         : 355.707s (Solving: 332.16s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 355.680s

Choices      : 9427166  (Domain: 9216582)
Conflicts    : 373489   (Analyzed: 373486)
Restarts     : 4296     (Average: 86.94 Last: 171)
Model-Level  : 232.0   
Problems     : 47       (Average Length: 65.83 Splits: 0)
Lemmas       : 373486   (Deleted: 348809)
  Binary     : 7263     (Ratio:   1.94%)
  Ternary    : 1733     (Ratio:   0.46%)
  Conflict   : 373486   (Average Length:  577.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 373486   (Average: 23.55 Max: 976 Sum: 8796662)
  Executed   : 373386   (Average: 23.54 Max: 976 Sum: 8792150 Ratio:  99.95%)
  Bounded    : 100      (Average: 45.12 Max: 102 Sum:   4512 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352708  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.92s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 6.99s

Iteration 47
Queue:		 [(11,55,2,True), (12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 48
Time         : 362.947s (Solving: 339.25s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 362.924s

Choices      : 9586802  (Domain: 9374669)
Conflicts    : 381596   (Analyzed: 381593)
Restarts     : 4396     (Average: 86.80 Last: 171)
Model-Level  : 232.0   
Problems     : 48       (Average Length: 66.58 Splits: 0)
Lemmas       : 381593   (Deleted: 356383)
  Binary     : 7368     (Ratio:   1.93%)
  Ternary    : 1762     (Ratio:   0.46%)
  Conflict   : 381593   (Average Length:  569.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 381593   (Average: 23.44 Max: 976 Sum: 8945143)
  Executed   : 381492   (Average: 23.43 Max: 976 Sum: 8940534 Ratio:  99.95%)
  Bounded    : 101      (Average: 45.63 Max: 102 Sum:   4609 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352708  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.19s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.25s

Iteration 48
Queue:		 [(12,60,2,True), (13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 49
Time         : 369.737s (Solving: 345.90s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 369.716s

Choices      : 9713904  (Domain: 9500881)
Conflicts    : 389120   (Analyzed: 389117)
Restarts     : 4496     (Average: 86.55 Last: 171)
Model-Level  : 232.0   
Problems     : 49       (Average Length: 67.31 Splits: 0)
Lemmas       : 389117   (Deleted: 364193)
  Binary     : 7472     (Ratio:   1.92%)
  Ternary    : 1770     (Ratio:   0.45%)
  Conflict   : 389117   (Average Length:  562.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 389117   (Average: 23.29 Max: 976 Sum: 9061016)
  Executed   : 389014   (Average: 23.27 Max: 976 Sum: 9056208 Ratio:  99.95%)
  Bounded    : 103      (Average: 46.68 Max: 102 Sum:   4808 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352708  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.75s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 6.80s

Iteration 49
Queue:		 [(13,65,2,True), (14,70,2,False), (15,75,2,False), (16,80,2,False), (17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 50
Time         : 377.489s (Solving: 353.49s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 377.472s

Choices      : 9909629  (Domain: 9693884)
Conflicts    : 397372   (Analyzed: 397369)
Restarts     : 4596     (Average: 86.46 Last: 171)
Model-Level  : 232.0   
Problems     : 50       (Average Length: 68.00 Splits: 0)
Lemmas       : 397369   (Deleted: 371429)
  Binary     : 7533     (Ratio:   1.90%)
  Ternary    : 1790     (Ratio:   0.45%)
  Conflict   : 397369   (Average Length:  555.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 397369   (Average: 23.25 Max: 976 Sum: 9238811)
  Executed   : 397266   (Average: 23.24 Max: 976 Sum: 9234003 Ratio:  99.95%)
  Bounded    : 103      (Average: 46.68 Max: 102 Sum:   4808 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352694  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.70s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.76s

Iteration 50
Queue:		 [(17,85,1,True), (18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 51
Time         : 386.707s (Solving: 362.55s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 386.692s

Choices      : 10247994 (Domain: 10029074)
Conflicts    : 406075   (Analyzed: 406072)
Restarts     : 4696     (Average: 86.47 Last: 171)
Model-Level  : 232.0   
Problems     : 51       (Average Length: 68.67 Splits: 0)
Lemmas       : 406072   (Deleted: 381556)
  Binary     : 7597     (Ratio:   1.87%)
  Ternary    : 1803     (Ratio:   0.44%)
  Conflict   : 406072   (Average Length:  548.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 406072   (Average: 23.54 Max: 1125 Sum: 9557408)
  Executed   : 405967   (Average: 23.52 Max: 1125 Sum: 9552396 Ratio:  99.95%)
  Bounded    : 105      (Average: 47.73 Max: 102 Sum:   5012 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352694  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.16s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 9.22s

Iteration 51
Queue:		 [(18,90,1,True), (19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 52
Time         : 395.291s (Solving: 370.96s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 395.280s

Choices      : 10468451 (Domain: 10248704)
Conflicts    : 414573   (Analyzed: 414570)
Restarts     : 4796     (Average: 86.44 Last: 171)
Model-Level  : 232.0   
Problems     : 52       (Average Length: 69.31 Splits: 0)
Lemmas       : 414570   (Deleted: 387835)
  Binary     : 7631     (Ratio:   1.84%)
  Ternary    : 1818     (Ratio:   0.44%)
  Conflict   : 414570   (Average Length:  541.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 414570   (Average: 23.55 Max: 1125 Sum: 9761448)
  Executed   : 414465   (Average: 23.53 Max: 1125 Sum: 9756436 Ratio:  99.95%)
  Bounded    : 105      (Average: 47.73 Max: 102 Sum:   5012 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352654  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.53s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 8.59s

Iteration 52
Queue:		 [(19,95,1,True), (20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 53
Time         : 402.682s (Solving: 378.21s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 402.676s

Choices      : 10655507 (Domain: 10435367)
Conflicts    : 422518   (Analyzed: 422515)
Restarts     : 4896     (Average: 86.30 Last: 171)
Model-Level  : 232.0   
Problems     : 53       (Average Length: 69.92 Splits: 0)
Lemmas       : 422515   (Deleted: 396161)
  Binary     : 7676     (Ratio:   1.82%)
  Ternary    : 1827     (Ratio:   0.43%)
  Conflict   : 422515   (Average Length:  536.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 422515   (Average: 23.51 Max: 1125 Sum: 9933522)
  Executed   : 422409   (Average: 23.50 Max: 1125 Sum: 9928413 Ratio:  99.95%)
  Bounded    : 106      (Average: 48.20 Max: 102 Sum:   5109 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352654  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.35s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 7.40s

Iteration 53
Queue:		 [(20,100,1,True), (21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 54
Time         : 411.744s (Solving: 387.10s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 411.740s

Choices      : 10904706 (Domain: 10683252)
Conflicts    : 430740   (Analyzed: 430737)
Restarts     : 4996     (Average: 86.22 Last: 171)
Model-Level  : 232.0   
Problems     : 54       (Average Length: 70.52 Splits: 0)
Lemmas       : 430737   (Deleted: 403890)
  Binary     : 7708     (Ratio:   1.79%)
  Ternary    : 1839     (Ratio:   0.43%)
  Conflict   : 430737   (Average Length:  530.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 430737   (Average: 23.61 Max: 1255 Sum: 10167548)
  Executed   : 430629   (Average: 23.59 Max: 1255 Sum: 10162235 Ratio:  99.95%)
  Bounded    : 108      (Average: 49.19 Max: 102 Sum:   5313 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 731092   (Eliminated:    0 Frozen: 225701)
Constraints  : 5352654  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 880MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.00s
Memory:		 796MB (+0MB)
UNKNOWN
Iteration Time:	 9.07s

Iteration 54
Queue:		 [(21,105,0,True), (22,110,0,True), (23,115,0,True)]
Grounded Until:	 100
Expected Memory: 876.0MB
Grounding...	 [('step', [101]), ('step', [102]), ('step', [103]), ('step', [104]), ('step', [105]), ('check', [105])]
Grounding Time:	 0.52s
Memory:		 796MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 55
Time         : 423.335s (Solving: 397.54s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 423.336s

Choices      : 11691607 (Domain: 11464606)
Conflicts    : 439636   (Analyzed: 439633)
Restarts     : 5096     (Average: 86.27 Last: 171)
Model-Level  : 232.0   
Problems     : 55       (Average Length: 71.18 Splits: 0)
Lemmas       : 439633   (Deleted: 415679)
  Binary     : 7765     (Ratio:   1.77%)
  Ternary    : 1842     (Ratio:   0.42%)
  Conflict   : 439633   (Average Length:  532.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 439633   (Average: 24.84 Max: 1255 Sum: 10920793)
  Executed   : 439525   (Average: 24.83 Max: 1255 Sum: 10915480 Ratio:  99.95%)
  Bounded    : 108      (Average: 49.19 Max: 102 Sum:   5313 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 768583   (Eliminated:    0 Frozen: 237361)
Constraints  : 5635087  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 891MB
Max. Length  : 100 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.58s
Memory:		 805MB (+9MB)
UNKNOWN
Iteration Time:	 11.60s

Iteration 55
Queue:		 [(22,110,0,True), (23,115,0,True)]
Grounded Until:	 105
Expected Memory: 885.0MB
Grounding...	 [('step', [106]), ('step', [107]), ('step', [108]), ('step', [109]), ('step', [110]), ('check', [110])]
Grounding Time:	 0.52s
Memory:		 811MB (+6MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 56
Time         : 436.034s (Solving: 409.08s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 436.040s

Choices      : 12226711 (Domain: 11996210)
Conflicts    : 448542   (Analyzed: 448539)
Restarts     : 5196     (Average: 86.32 Last: 171)
Model-Level  : 232.0   
Problems     : 56       (Average Length: 71.91 Splits: 0)
Lemmas       : 448539   (Deleted: 424246)
  Binary     : 7795     (Ratio:   1.74%)
  Ternary    : 1842     (Ratio:   0.41%)
  Conflict   : 448539   (Average Length:  539.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 448539   (Average: 25.46 Max: 1255 Sum: 11418465)
  Executed   : 448431   (Average: 25.45 Max: 1255 Sum: 11413152 Ratio:  99.95%)
  Bounded    : 108      (Average: 49.19 Max: 102 Sum:   5313 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 806074   (Eliminated:    0 Frozen: 249021)
Constraints  : 5917547  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 925MB
Max. Length  : 105 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 11.69s
Memory:		 831MB (+20MB)
UNKNOWN
Iteration Time:	 12.71s

Iteration 56
Queue:		 [(23,115,0,True)]
Grounded Until:	 110
Expected Memory: 911.0MB
Grounding...	 [('step', [111]), ('step', [112]), ('step', [113]), ('step', [114]), ('step', [115]), ('check', [115])]
Grounding Time:	 0.52s
Memory:		 831MB (+0MB)
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 57
Time         : 448.553s (Solving: 420.41s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 448.564s

Choices      : 12777819 (Domain: 12543726)
Conflicts    : 456698   (Analyzed: 456695)
Restarts     : 5296     (Average: 86.23 Last: 171)
Model-Level  : 232.0   
Problems     : 57       (Average Length: 72.70 Splits: 0)
Lemmas       : 456695   (Deleted: 431287)
  Binary     : 7812     (Ratio:   1.71%)
  Ternary    : 1844     (Ratio:   0.40%)
  Conflict   : 456695   (Average Length:  551.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 456695   (Average: 26.12 Max: 1255 Sum: 11930574)
  Executed   : 456587   (Average: 26.11 Max: 1255 Sum: 11925261 Ratio:  99.96%)
  Bounded    : 108      (Average: 49.19 Max: 102 Sum:   5313 Ratio:   0.04%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6200007  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 110 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 11.49s
Memory:		 855MB (+24MB)
UNKNOWN
Iteration Time:	 12.53s

Iteration 57
Queue:		 [(4,20,4,True), (5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 58
Time         : 454.666s (Solving: 426.36s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 454.680s

Choices      : 12837631 (Domain: 12602369)
Conflicts    : 464801   (Analyzed: 464798)
Restarts     : 5396     (Average: 86.14 Last: 171)
Model-Level  : 232.0   
Problems     : 58       (Average Length: 73.47 Splits: 0)
Lemmas       : 464798   (Deleted: 437188)
  Binary     : 7850     (Ratio:   1.69%)
  Ternary    : 1848     (Ratio:   0.40%)
  Conflict   : 464798   (Average Length:  544.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 464798   (Average: 25.78 Max: 1255 Sum: 11982730)
  Executed   : 464690   (Average: 25.77 Max: 1255 Sum: 11977417 Ratio:  99.96%)
  Bounded    : 108      (Average: 49.19 Max: 102 Sum:   5313 Ratio:   0.04%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6200007  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.06s
Memory:		 864MB (+9MB)
UNKNOWN
Iteration Time:	 6.12s

Iteration 58
Queue:		 [(5,25,4,True), (6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 59
Time         : 459.614s (Solving: 431.11s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 459.632s

Choices      : 12889429 (Domain: 12653674)
Conflicts    : 472760   (Analyzed: 472757)
Restarts     : 5496     (Average: 86.02 Last: 171)
Model-Level  : 232.0   
Problems     : 59       (Average Length: 74.20 Splits: 0)
Lemmas       : 472757   (Deleted: 445115)
  Binary     : 7873     (Ratio:   1.67%)
  Ternary    : 1862     (Ratio:   0.39%)
  Conflict   : 472757   (Average Length:  539.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 472757   (Average: 25.44 Max: 1255 Sum: 12027384)
  Executed   : 472648   (Average: 25.43 Max: 1255 Sum: 12021954 Ratio:  99.95%)
  Bounded    : 109      (Average: 49.82 Max: 117 Sum:   5430 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6200007  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.88s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 4.95s

Iteration 59
Queue:		 [(6,30,4,True), (7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 60
Time         : 465.895s (Solving: 437.23s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 465.916s

Choices      : 12967705 (Domain: 12730950)
Conflicts    : 480690   (Analyzed: 480687)
Restarts     : 5596     (Average: 85.90 Last: 171)
Model-Level  : 232.0   
Problems     : 60       (Average Length: 74.92 Splits: 0)
Lemmas       : 480687   (Deleted: 452891)
  Binary     : 7896     (Ratio:   1.64%)
  Ternary    : 1870     (Ratio:   0.39%)
  Conflict   : 480687   (Average Length:  533.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 480687   (Average: 25.17 Max: 1255 Sum: 12098432)
  Executed   : 480576   (Average: 25.16 Max: 1255 Sum: 12092768 Ratio:  99.95%)
  Bounded    : 111      (Average: 51.03 Max: 117 Sum:   5664 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199981  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.23s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.29s

Iteration 60
Queue:		 [(7,35,3,True), (8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 61
Time         : 472.239s (Solving: 443.39s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 472.260s

Choices      : 13061292 (Domain: 12823535)
Conflicts    : 489048   (Analyzed: 489045)
Restarts     : 5696     (Average: 85.86 Last: 171)
Model-Level  : 232.0   
Problems     : 61       (Average Length: 75.61 Splits: 0)
Lemmas       : 489045   (Deleted: 460661)
  Binary     : 7926     (Ratio:   1.62%)
  Ternary    : 1876     (Ratio:   0.38%)
  Conflict   : 489045   (Average Length:  528.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 489045   (Average: 24.91 Max: 1255 Sum: 12183637)
  Executed   : 488934   (Average: 24.90 Max: 1255 Sum: 12177973 Ratio:  99.95%)
  Bounded    : 111      (Average: 51.03 Max: 117 Sum:   5664 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199953  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.28s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.35s

Iteration 61
Queue:		 [(8,40,3,True), (9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 62
Time         : 479.138s (Solving: 450.13s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 479.164s

Choices      : 13173458 (Domain: 12934492)
Conflicts    : 497517   (Analyzed: 497514)
Restarts     : 5796     (Average: 85.84 Last: 171)
Model-Level  : 232.0   
Problems     : 62       (Average Length: 76.27 Splits: 0)
Lemmas       : 497514   (Deleted: 468817)
  Binary     : 7948     (Ratio:   1.60%)
  Ternary    : 1885     (Ratio:   0.38%)
  Conflict   : 497514   (Average Length:  523.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 497514   (Average: 24.69 Max: 1255 Sum: 12284824)
  Executed   : 497403   (Average: 24.68 Max: 1255 Sum: 12279160 Ratio:  99.95%)
  Bounded    : 111      (Average: 51.03 Max: 117 Sum:   5664 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199953  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.85s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.90s

Iteration 62
Queue:		 [(9,45,3,True), (10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 63
Time         : 485.927s (Solving: 456.73s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 485.956s

Choices      : 13300298 (Domain: 13057486)
Conflicts    : 506050   (Analyzed: 506047)
Restarts     : 5896     (Average: 85.83 Last: 171)
Model-Level  : 232.0   
Problems     : 63       (Average Length: 76.92 Splits: 0)
Lemmas       : 506047   (Deleted: 477031)
  Binary     : 7986     (Ratio:   1.58%)
  Ternary    : 1894     (Ratio:   0.37%)
  Conflict   : 506047   (Average Length:  518.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 506047   (Average: 24.50 Max: 1255 Sum: 12398827)
  Executed   : 505935   (Average: 24.49 Max: 1255 Sum: 12393046 Ratio:  99.95%)
  Bounded    : 112      (Average: 51.62 Max: 117 Sum:   5781 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199953  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.72s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.79s

Iteration 63
Queue:		 [(10,50,3,True), (11,55,3,False), (12,60,3,False), (13,65,3,False), (14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 64
Time         : 493.510s (Solving: 464.14s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 493.540s

Choices      : 13421584 (Domain: 13177905)
Conflicts    : 514137   (Analyzed: 514134)
Restarts     : 5996     (Average: 85.75 Last: 171)
Model-Level  : 232.0   
Problems     : 64       (Average Length: 77.55 Splits: 0)
Lemmas       : 514134   (Deleted: 485398)
  Binary     : 8014     (Ratio:   1.56%)
  Ternary    : 1902     (Ratio:   0.37%)
  Conflict   : 514134   (Average Length:  514.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 514134   (Average: 24.33 Max: 1255 Sum: 12508768)
  Executed   : 514021   (Average: 24.32 Max: 1255 Sum: 12502870 Ratio:  99.95%)
  Bounded    : 113      (Average: 52.19 Max: 117 Sum:   5898 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199939  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.53s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.59s

Iteration 64
Queue:		 [(14,70,2,True), (15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 65
Time         : 501.235s (Solving: 471.70s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 501.268s

Choices      : 13608120 (Domain: 13363769)
Conflicts    : 522146   (Analyzed: 522143)
Restarts     : 6096     (Average: 85.65 Last: 171)
Model-Level  : 232.0   
Problems     : 65       (Average Length: 78.15 Splits: 0)
Lemmas       : 522143   (Deleted: 493183)
  Binary     : 8127     (Ratio:   1.56%)
  Ternary    : 1939     (Ratio:   0.37%)
  Conflict   : 522143   (Average Length:  509.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 522143   (Average: 24.29 Max: 1255 Sum: 12682648)
  Executed   : 522028   (Average: 24.28 Max: 1255 Sum: 12676526 Ratio:  99.95%)
  Bounded    : 115      (Average: 53.23 Max: 117 Sum:   6122 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199925  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.67s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.73s

Iteration 65
Queue:		 [(15,75,2,True), (16,80,2,False), (17,85,2,False), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 66
Time         : 510.193s (Solving: 480.49s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 510.228s

Choices      : 13859353 (Domain: 13613977)
Conflicts    : 530618   (Analyzed: 530615)
Restarts     : 6196     (Average: 85.64 Last: 171)
Model-Level  : 232.0   
Problems     : 66       (Average Length: 78.74 Splits: 0)
Lemmas       : 530615   (Deleted: 500870)
  Binary     : 8147     (Ratio:   1.54%)
  Ternary    : 1955     (Ratio:   0.37%)
  Conflict   : 530615   (Average Length:  504.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 530615   (Average: 24.35 Max: 1255 Sum: 12919187)
  Executed   : 530500   (Average: 24.34 Max: 1255 Sum: 12913065 Ratio:  99.95%)
  Bounded    : 115      (Average: 53.23 Max: 117 Sum:   6122 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199925  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.90s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.96s

Iteration 66
Queue:		 [(21,105,1,True), (22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 67
Time         : 518.956s (Solving: 489.08s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 518.996s

Choices      : 14022844 (Domain: 13777305)
Conflicts    : 538772   (Analyzed: 538769)
Restarts     : 6296     (Average: 85.57 Last: 171)
Model-Level  : 232.0   
Problems     : 67       (Average Length: 79.31 Splits: 0)
Lemmas       : 538769   (Deleted: 509149)
  Binary     : 8176     (Ratio:   1.52%)
  Ternary    : 1966     (Ratio:   0.36%)
  Conflict   : 538769   (Average Length:  500.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 538769   (Average: 24.25 Max: 1255 Sum: 13066793)
  Executed   : 538654   (Average: 24.24 Max: 1255 Sum: 13060671 Ratio:  99.95%)
  Bounded    : 115      (Average: 53.23 Max: 117 Sum:   6122 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199925  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.71s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.77s

Iteration 67
Queue:		 [(22,110,1,True), (23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 68
Time         : 528.763s (Solving: 498.72s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 528.804s

Choices      : 14246213 (Domain: 14000272)
Conflicts    : 547115   (Analyzed: 547112)
Restarts     : 6396     (Average: 85.54 Last: 171)
Model-Level  : 232.0   
Problems     : 68       (Average Length: 79.87 Splits: 0)
Lemmas       : 547112   (Deleted: 517088)
  Binary     : 8199     (Ratio:   1.50%)
  Ternary    : 1972     (Ratio:   0.36%)
  Conflict   : 547112   (Average Length:  496.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 547112   (Average: 24.26 Max: 1255 Sum: 13273255)
  Executed   : 546995   (Average: 24.25 Max: 1255 Sum: 13266899 Ratio:  99.95%)
  Bounded    : 117      (Average: 54.32 Max: 117 Sum:   6356 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199925  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.76s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 9.81s

Iteration 68
Queue:		 [(23,115,1,True)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 69
Time         : 536.753s (Solving: 506.52s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 536.796s

Choices      : 14430681 (Domain: 14183957)
Conflicts    : 555430   (Analyzed: 555427)
Restarts     : 6496     (Average: 85.50 Last: 171)
Model-Level  : 232.0   
Problems     : 69       (Average Length: 80.41 Splits: 0)
Lemmas       : 555427   (Deleted: 525178)
  Binary     : 8268     (Ratio:   1.49%)
  Ternary    : 1992     (Ratio:   0.36%)
  Conflict   : 555427   (Average Length:  492.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 555427   (Average: 24.20 Max: 1255 Sum: 13440856)
  Executed   : 555307   (Average: 24.19 Max: 1255 Sum: 13434154 Ratio:  99.95%)
  Bounded    : 120      (Average: 55.85 Max: 117 Sum:   6702 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199897  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.92s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.99s

Iteration 69
Queue:		 [(4,20,5,True), (5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 70
Time         : 542.749s (Solving: 512.35s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 542.796s

Choices      : 14476363 (Domain: 14229056)
Conflicts    : 563997   (Analyzed: 563994)
Restarts     : 6596     (Average: 85.51 Last: 171)
Model-Level  : 232.0   
Problems     : 70       (Average Length: 80.93 Splits: 0)
Lemmas       : 563994   (Deleted: 533282)
  Binary     : 8326     (Ratio:   1.48%)
  Ternary    : 2004     (Ratio:   0.36%)
  Conflict   : 563994   (Average Length:  488.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 563994   (Average: 23.90 Max: 1255 Sum: 13480190)
  Executed   : 563872   (Average: 23.89 Max: 1255 Sum: 13473255 Ratio:  99.95%)
  Bounded    : 122      (Average: 56.84 Max: 117 Sum:   6935 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199869  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.94s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.00s

Iteration 70
Queue:		 [(5,25,5,True), (6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 71
Time         : 548.770s (Solving: 518.18s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 548.820s

Choices      : 14543972 (Domain: 14296189)
Conflicts    : 572433   (Analyzed: 572430)
Restarts     : 6696     (Average: 85.49 Last: 171)
Model-Level  : 232.0   
Problems     : 71       (Average Length: 81.44 Splits: 0)
Lemmas       : 572430   (Deleted: 541649)
  Binary     : 8412     (Ratio:   1.47%)
  Ternary    : 2034     (Ratio:   0.36%)
  Conflict   : 572430   (Average Length:  485.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 572430   (Average: 23.65 Max: 1255 Sum: 13539606)
  Executed   : 572308   (Average: 23.64 Max: 1255 Sum: 13532671 Ratio:  99.95%)
  Bounded    : 122      (Average: 56.84 Max: 117 Sum:   6935 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199851  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.95s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.03s

Iteration 71
Queue:		 [(6,30,5,True), (7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 72
Time         : 554.809s (Solving: 524.05s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 554.864s

Choices      : 14603441 (Domain: 14355082)
Conflicts    : 580793   (Analyzed: 580790)
Restarts     : 6796     (Average: 85.46 Last: 171)
Model-Level  : 232.0   
Problems     : 72       (Average Length: 81.93 Splits: 0)
Lemmas       : 580790   (Deleted: 549752)
  Binary     : 8433     (Ratio:   1.45%)
  Ternary    : 2046     (Ratio:   0.35%)
  Conflict   : 580790   (Average Length:  481.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 580790   (Average: 23.40 Max: 1255 Sum: 13591492)
  Executed   : 580666   (Average: 23.39 Max: 1255 Sum: 13584323 Ratio:  99.95%)
  Bounded    : 124      (Average: 57.81 Max: 117 Sum:   7169 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199851  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.98s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.05s

Iteration 72
Queue:		 [(7,35,4,True), (8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 73
Time         : 560.984s (Solving: 530.04s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 561.040s

Choices      : 14648334 (Domain: 14399718)
Conflicts    : 588764   (Analyzed: 588761)
Restarts     : 6896     (Average: 85.38 Last: 171)
Model-Level  : 232.0   
Problems     : 73       (Average Length: 82.41 Splits: 0)
Lemmas       : 588761   (Deleted: 557942)
  Binary     : 8451     (Ratio:   1.44%)
  Ternary    : 2055     (Ratio:   0.35%)
  Conflict   : 588761   (Average Length:  477.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 588761   (Average: 23.15 Max: 1255 Sum: 13628719)
  Executed   : 588636   (Average: 23.14 Max: 1255 Sum: 13621433 Ratio:  99.95%)
  Bounded    : 125      (Average: 58.29 Max: 117 Sum:   7286 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199811  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.11s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.18s

Iteration 73
Queue:		 [(8,40,4,True), (9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 74
Time         : 568.288s (Solving: 537.16s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 568.344s

Choices      : 14766229 (Domain: 14514654)
Conflicts    : 597013   (Analyzed: 597010)
Restarts     : 6996     (Average: 85.34 Last: 171)
Model-Level  : 232.0   
Problems     : 74       (Average Length: 82.88 Splits: 0)
Lemmas       : 597010   (Deleted: 565679)
  Binary     : 8486     (Ratio:   1.42%)
  Ternary    : 2094     (Ratio:   0.35%)
  Conflict   : 597010   (Average Length:  474.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 597010   (Average: 23.01 Max: 1255 Sum: 13735053)
  Executed   : 596885   (Average: 22.99 Max: 1255 Sum: 13727767 Ratio:  99.95%)
  Bounded    : 125      (Average: 58.29 Max: 117 Sum:   7286 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199798  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.24s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.31s

Iteration 74
Queue:		 [(9,45,4,True), (10,50,4,False), (11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 75
Time         : 575.591s (Solving: 544.28s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 575.648s

Choices      : 14857657 (Domain: 14605739)
Conflicts    : 605469   (Analyzed: 605466)
Restarts     : 7096     (Average: 85.32 Last: 171)
Model-Level  : 232.0   
Problems     : 75       (Average Length: 83.33 Splits: 0)
Lemmas       : 605466   (Deleted: 573690)
  Binary     : 8514     (Ratio:   1.41%)
  Ternary    : 2099     (Ratio:   0.35%)
  Conflict   : 605466   (Average Length:  471.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 605466   (Average: 22.82 Max: 1255 Sum: 13817027)
  Executed   : 605340   (Average: 22.81 Max: 1255 Sum: 13809624 Ratio:  99.95%)
  Bounded    : 126      (Average: 58.75 Max: 117 Sum:   7403 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199798  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.24s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.31s

Iteration 75
Queue:		 [(11,55,3,True), (12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 76
Time         : 584.071s (Solving: 552.57s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 584.132s

Choices      : 15009738 (Domain: 14755250)
Conflicts    : 614692   (Analyzed: 614689)
Restarts     : 7196     (Average: 85.42 Last: 171)
Model-Level  : 232.0   
Problems     : 76       (Average Length: 83.78 Splits: 0)
Lemmas       : 614689   (Deleted: 583961)
  Binary     : 8604     (Ratio:   1.40%)
  Ternary    : 2146     (Ratio:   0.35%)
  Conflict   : 614689   (Average Length:  468.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 614689   (Average: 22.69 Max: 1255 Sum: 13949496)
  Executed   : 614561   (Average: 22.68 Max: 1255 Sum: 13941859 Ratio:  99.95%)
  Bounded    : 128      (Average: 59.66 Max: 117 Sum:   7637 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199772  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.42s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.49s

Iteration 76
Queue:		 [(12,60,3,True), (13,65,3,False), (14,70,3,False), (15,75,3,False), (16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 77
Time         : 593.492s (Solving: 561.82s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 593.556s

Choices      : 15218644 (Domain: 14961012)
Conflicts    : 623205   (Analyzed: 623202)
Restarts     : 7296     (Average: 85.42 Last: 171)
Model-Level  : 232.0   
Problems     : 77       (Average Length: 84.21 Splits: 0)
Lemmas       : 623202   (Deleted: 590712)
  Binary     : 8679     (Ratio:   1.39%)
  Ternary    : 2167     (Ratio:   0.35%)
  Conflict   : 623202   (Average Length:  467.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 623202   (Average: 22.68 Max: 1255 Sum: 14132954)
  Executed   : 623071   (Average: 22.67 Max: 1255 Sum: 14124976 Ratio:  99.94%)
  Bounded    : 131      (Average: 60.90 Max: 117 Sum:   7978 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199745  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.37s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 9.43s

Iteration 77
Queue:		 [(16,80,2,True), (17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 78
Time         : 600.937s (Solving: 569.11s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 601.004s

Choices      : 15408713 (Domain: 15150060)
Conflicts    : 631232   (Analyzed: 631229)
Restarts     : 7396     (Average: 85.35 Last: 171)
Model-Level  : 232.0   
Problems     : 78       (Average Length: 84.63 Splits: 0)
Lemmas       : 631229   (Deleted: 598987)
  Binary     : 8746     (Ratio:   1.39%)
  Ternary    : 2178     (Ratio:   0.35%)
  Conflict   : 631229   (Average Length:  465.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 631229   (Average: 22.66 Max: 1255 Sum: 14306296)
  Executed   : 631098   (Average: 22.65 Max: 1255 Sum: 14298318 Ratio:  99.94%)
  Bounded    : 131      (Average: 60.90 Max: 117 Sum:   7978 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199731  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.39s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.45s

Iteration 78
Queue:		 [(17,85,2,True), (18,90,2,False), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 79
Time         : 612.785s (Solving: 580.77s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 612.860s

Choices      : 16008986 (Domain: 15746727)
Conflicts    : 640420   (Analyzed: 640417)
Restarts     : 7496     (Average: 85.43 Last: 171)
Model-Level  : 232.0   
Problems     : 79       (Average Length: 85.04 Splits: 0)
Lemmas       : 640417   (Deleted: 608932)
  Binary     : 8888     (Ratio:   1.39%)
  Ternary    : 2183     (Ratio:   0.34%)
  Conflict   : 640417   (Average Length:  463.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 640417   (Average: 23.24 Max: 1255 Sum: 14884055)
  Executed   : 640286   (Average: 23.23 Max: 1255 Sum: 14876077 Ratio:  99.95%)
  Bounded    : 131      (Average: 60.90 Max: 117 Sum:   7978 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199731  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 11.79s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 11.86s

Iteration 79
Queue:		 [(4,20,6,True), (5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 80
Time         : 620.247s (Solving: 588.06s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 620.324s

Choices      : 16048282 (Domain: 15786023)
Conflicts    : 648780   (Analyzed: 648777)
Restarts     : 7596     (Average: 85.41 Last: 171)
Model-Level  : 232.0   
Problems     : 80       (Average Length: 85.44 Splits: 0)
Lemmas       : 648777   (Deleted: 615663)
  Binary     : 8909     (Ratio:   1.37%)
  Ternary    : 2194     (Ratio:   0.34%)
  Conflict   : 648777   (Average Length:  461.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 648777   (Average: 22.99 Max: 1255 Sum: 14918338)
  Executed   : 648644   (Average: 22.98 Max: 1255 Sum: 14910136 Ratio:  99.95%)
  Bounded    : 133      (Average: 61.67 Max: 117 Sum:   8202 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199731  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.40s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.47s

Iteration 80
Queue:		 [(5,25,6,True), (6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 81
Time         : 626.545s (Solving: 594.16s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 626.624s

Choices      : 16137076 (Domain: 15873284)
Conflicts    : 656802   (Analyzed: 656799)
Restarts     : 7696     (Average: 85.34 Last: 171)
Model-Level  : 232.0   
Problems     : 81       (Average Length: 85.83 Splits: 0)
Lemmas       : 656799   (Deleted: 623811)
  Binary     : 8968     (Ratio:   1.37%)
  Ternary    : 2205     (Ratio:   0.34%)
  Conflict   : 656799   (Average Length:  459.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 656799   (Average: 22.84 Max: 1255 Sum: 14999276)
  Executed   : 656665   (Average: 22.82 Max: 1255 Sum: 14990957 Ratio:  99.94%)
  Bounded    : 134      (Average: 62.08 Max: 117 Sum:   8319 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199731  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.22s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.30s

Iteration 81
Queue:		 [(6,30,6,True), (7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 82
Time         : 632.132s (Solving: 599.57s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 632.212s

Choices      : 16206027 (Domain: 15940612)
Conflicts    : 664955   (Analyzed: 664952)
Restarts     : 7796     (Average: 85.29 Last: 171)
Model-Level  : 232.0   
Problems     : 82       (Average Length: 86.21 Splits: 0)
Lemmas       : 664952   (Deleted: 631579)
  Binary     : 9003     (Ratio:   1.35%)
  Ternary    : 2210     (Ratio:   0.33%)
  Conflict   : 664952   (Average Length:  456.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 664952   (Average: 22.65 Max: 1255 Sum: 15060121)
  Executed   : 664817   (Average: 22.64 Max: 1255 Sum: 15051685 Ratio:  99.94%)
  Bounded    : 135      (Average: 62.49 Max: 117 Sum:   8436 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199713  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.52s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 5.59s

Iteration 82
Queue:		 [(7,35,5,True), (8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 83
Time         : 638.816s (Solving: 606.07s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 638.900s

Choices      : 16282916 (Domain: 16016607)
Conflicts    : 673108   (Analyzed: 673105)
Restarts     : 7896     (Average: 85.25 Last: 171)
Model-Level  : 232.0   
Problems     : 83       (Average Length: 86.58 Splits: 0)
Lemmas       : 673105   (Deleted: 639552)
  Binary     : 9041     (Ratio:   1.34%)
  Ternary    : 2218     (Ratio:   0.33%)
  Conflict   : 673105   (Average Length:  453.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 673105   (Average: 22.48 Max: 1255 Sum: 15129881)
  Executed   : 672969   (Average: 22.47 Max: 1255 Sum: 15121328 Ratio:  99.94%)
  Bounded    : 136      (Average: 62.89 Max: 117 Sum:   8553 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199699  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.62s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.69s

Iteration 83
Queue:		 [(8,40,5,True), (9,45,5,False), (10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 84
Time         : 645.906s (Solving: 613.00s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 645.992s

Choices      : 16363245 (Domain: 16094472)
Conflicts    : 681207   (Analyzed: 681204)
Restarts     : 7996     (Average: 85.19 Last: 171)
Model-Level  : 232.0   
Problems     : 84       (Average Length: 86.94 Splits: 0)
Lemmas       : 681204   (Deleted: 647474)
  Binary     : 9072     (Ratio:   1.33%)
  Ternary    : 2237     (Ratio:   0.33%)
  Conflict   : 681204   (Average Length:  450.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 681204   (Average: 22.31 Max: 1255 Sum: 15200981)
  Executed   : 681067   (Average: 22.30 Max: 1255 Sum: 15192311 Ratio:  99.94%)
  Bounded    : 137      (Average: 63.28 Max: 117 Sum:   8670 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199686  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.04s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.10s

Iteration 84
Queue:		 [(10,50,4,True), (11,55,4,False), (12,60,4,False), (13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 85
Time         : 653.672s (Solving: 620.60s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 653.760s

Choices      : 16517040 (Domain: 16247104)
Conflicts    : 689478   (Analyzed: 689475)
Restarts     : 8096     (Average: 85.16 Last: 171)
Model-Level  : 232.0   
Problems     : 85       (Average Length: 87.29 Splits: 0)
Lemmas       : 689475   (Deleted: 655346)
  Binary     : 9100     (Ratio:   1.32%)
  Ternary    : 2243     (Ratio:   0.33%)
  Conflict   : 689475   (Average Length:  448.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 689475   (Average: 22.25 Max: 1255 Sum: 15343975)
  Executed   : 689337   (Average: 22.24 Max: 1255 Sum: 15335193 Ratio:  99.94%)
  Bounded    : 138      (Average: 63.64 Max: 117 Sum:   8782 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.72s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.77s

Iteration 85
Queue:		 [(13,65,3,True), (14,70,3,False), (15,75,3,False), (16,80,3,False), (17,85,3,False), (18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 86
Time         : 661.244s (Solving: 627.99s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 661.336s

Choices      : 16663361 (Domain: 16393175)
Conflicts    : 697585   (Analyzed: 697582)
Restarts     : 8196     (Average: 85.11 Last: 171)
Model-Level  : 232.0   
Problems     : 86       (Average Length: 87.64 Splits: 0)
Lemmas       : 697582   (Deleted: 663440)
  Binary     : 9110     (Ratio:   1.31%)
  Ternary    : 2248     (Ratio:   0.32%)
  Conflict   : 697582   (Average Length:  446.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 697582   (Average: 22.19 Max: 1255 Sum: 15478518)
  Executed   : 697444   (Average: 22.18 Max: 1255 Sum: 15469736 Ratio:  99.94%)
  Bounded    : 138      (Average: 63.64 Max: 117 Sum:   8782 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.51s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 7.58s

Iteration 86
Queue:		 [(18,90,2,True), (19,95,2,False), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 87
Time         : 669.860s (Solving: 636.44s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 669.956s

Choices      : 16967845 (Domain: 16696168)
Conflicts    : 706302   (Analyzed: 706299)
Restarts     : 8296     (Average: 85.14 Last: 171)
Model-Level  : 232.0   
Problems     : 87       (Average Length: 87.98 Splits: 0)
Lemmas       : 706299   (Deleted: 673596)
  Binary     : 9147     (Ratio:   1.30%)
  Ternary    : 2259     (Ratio:   0.32%)
  Conflict   : 706299   (Average Length:  443.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 706299   (Average: 22.32 Max: 1255 Sum: 15766043)
  Executed   : 706161   (Average: 22.31 Max: 1255 Sum: 15757261 Ratio:  99.94%)
  Bounded    : 138      (Average: 63.64 Max: 117 Sum:   8782 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.57s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.62s

Iteration 87
Queue:		 [(4,20,7,True), (5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 88
Time         : 678.540s (Solving: 644.95s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 678.640s

Choices      : 17023325 (Domain: 16751648)
Conflicts    : 714224   (Analyzed: 714221)
Restarts     : 8396     (Average: 85.07 Last: 171)
Model-Level  : 232.0   
Problems     : 88       (Average Length: 88.31 Splits: 0)
Lemmas       : 714221   (Deleted: 680251)
  Binary     : 9211     (Ratio:   1.29%)
  Ternary    : 2273     (Ratio:   0.32%)
  Conflict   : 714221   (Average Length:  447.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 714221   (Average: 22.14 Max: 1255 Sum: 15815875)
  Executed   : 714081   (Average: 22.13 Max: 1255 Sum: 15807091 Ratio:  99.94%)
  Bounded    : 140      (Average: 62.74 Max: 117 Sum:   8784 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.62s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.69s

Iteration 88
Queue:		 [(5,25,7,True), (6,30,7,False), (7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 89
Time         : 684.332s (Solving: 650.57s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 684.432s

Choices      : 17085073 (Domain: 16812824)
Conflicts    : 722111   (Analyzed: 722108)
Restarts     : 8496     (Average: 84.99 Last: 171)
Model-Level  : 232.0   
Problems     : 89       (Average Length: 88.63 Splits: 0)
Lemmas       : 722108   (Deleted: 687535)
  Binary     : 9264     (Ratio:   1.28%)
  Ternary    : 2282     (Ratio:   0.32%)
  Conflict   : 722108   (Average Length:  445.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 722108   (Average: 21.98 Max: 1255 Sum: 15870681)
  Executed   : 721967   (Average: 21.97 Max: 1255 Sum: 15861785 Ratio:  99.94%)
  Bounded    : 141      (Average: 63.09 Max: 117 Sum:   8896 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.74s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 5.80s

Iteration 89
Queue:		 [(7,35,6,True), (8,40,6,False), (9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 90
Time         : 689.861s (Solving: 655.90s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 689.964s

Choices      : 17172619 (Domain: 16899545)
Conflicts    : 730083   (Analyzed: 730080)
Restarts     : 8596     (Average: 84.93 Last: 171)
Model-Level  : 232.0   
Problems     : 90       (Average Length: 88.94 Splits: 0)
Lemmas       : 730080   (Deleted: 695234)
  Binary     : 9312     (Ratio:   1.28%)
  Ternary    : 2295     (Ratio:   0.31%)
  Conflict   : 730080   (Average Length:  442.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 730080   (Average: 21.85 Max: 1255 Sum: 15949579)
  Executed   : 729939   (Average: 21.83 Max: 1255 Sum: 15940683 Ratio:  99.94%)
  Bounded    : 141      (Average: 63.09 Max: 117 Sum:   8896 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.45s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 5.53s

Iteration 90
Queue:		 [(9,45,5,True), (10,50,5,False), (11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 91
Time         : 696.333s (Solving: 662.19s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 696.440s

Choices      : 17283931 (Domain: 17009930)
Conflicts    : 738257   (Analyzed: 738254)
Restarts     : 8696     (Average: 84.90 Last: 171)
Model-Level  : 232.0   
Problems     : 91       (Average Length: 89.25 Splits: 0)
Lemmas       : 738254   (Deleted: 702930)
  Binary     : 9374     (Ratio:   1.27%)
  Ternary    : 2313     (Ratio:   0.31%)
  Conflict   : 738254   (Average Length:  440.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 738254   (Average: 21.74 Max: 1255 Sum: 16051813)
  Executed   : 738113   (Average: 21.73 Max: 1255 Sum: 16042917 Ratio:  99.94%)
  Bounded    : 141      (Average: 63.09 Max: 117 Sum:   8896 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.41s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.48s

Iteration 91
Queue:		 [(11,55,4,True), (12,60,4,False), (13,65,4,False), (14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 92
Time         : 704.865s (Solving: 670.53s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 704.980s

Choices      : 17490762 (Domain: 17213696)
Conflicts    : 746898   (Analyzed: 746895)
Restarts     : 8796     (Average: 84.91 Last: 171)
Model-Level  : 232.0   
Problems     : 92       (Average Length: 89.55 Splits: 0)
Lemmas       : 746895   (Deleted: 713000)
  Binary     : 9483     (Ratio:   1.27%)
  Ternary    : 2341     (Ratio:   0.31%)
  Conflict   : 746895   (Average Length:  439.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 746895   (Average: 21.75 Max: 1255 Sum: 16245810)
  Executed   : 746753   (Average: 21.74 Max: 1255 Sum: 16236797 Ratio:  99.94%)
  Bounded    : 142      (Average: 63.47 Max: 117 Sum:   9013 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199672  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.47s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 8.54s

Iteration 92
Queue:		 [(14,70,3,True), (15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 93
Time         : 711.574s (Solving: 677.08s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 711.692s

Choices      : 17643841 (Domain: 17366195)
Conflicts    : 754994   (Analyzed: 754991)
Restarts     : 8896     (Average: 84.87 Last: 171)
Model-Level  : 232.0   
Problems     : 93       (Average Length: 89.85 Splits: 0)
Lemmas       : 754991   (Deleted: 719198)
  Binary     : 9522     (Ratio:   1.26%)
  Ternary    : 2350     (Ratio:   0.31%)
  Conflict   : 754991   (Average Length:  437.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 754991   (Average: 21.70 Max: 1255 Sum: 16385754)
  Executed   : 754849   (Average: 21.69 Max: 1255 Sum: 16376741 Ratio:  99.94%)
  Bounded    : 142      (Average: 63.47 Max: 117 Sum:   9013 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199658  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.66s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.71s

Iteration 93
Queue:		 [(15,75,3,True), (16,80,3,False), (17,85,3,False), (18,90,3,False), (19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 94
Time         : 718.441s (Solving: 683.78s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 718.564s

Choices      : 17829841 (Domain: 17550556)
Conflicts    : 763031   (Analyzed: 763028)
Restarts     : 8996     (Average: 84.82 Last: 171)
Model-Level  : 232.0   
Problems     : 94       (Average Length: 90.14 Splits: 0)
Lemmas       : 763028   (Deleted: 727001)
  Binary     : 9604     (Ratio:   1.26%)
  Ternary    : 2392     (Ratio:   0.31%)
  Conflict   : 763028   (Average Length:  435.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 763028   (Average: 21.70 Max: 1255 Sum: 16558880)
  Executed   : 762886   (Average: 21.69 Max: 1255 Sum: 16549867 Ratio:  99.95%)
  Bounded    : 142      (Average: 63.47 Max: 117 Sum:   9013 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199658  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.82s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.87s

Iteration 94
Queue:		 [(19,95,2,True), (20,100,2,False), (21,105,2,False), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 95
Time         : 725.122s (Solving: 690.29s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 725.248s

Choices      : 18029566 (Domain: 17749953)
Conflicts    : 771173   (Analyzed: 771170)
Restarts     : 9096     (Average: 84.78 Last: 171)
Model-Level  : 232.0   
Problems     : 95       (Average Length: 90.42 Splits: 0)
Lemmas       : 771170   (Deleted: 734817)
  Binary     : 9652     (Ratio:   1.25%)
  Ternary    : 2410     (Ratio:   0.31%)
  Conflict   : 771170   (Average Length:  433.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 771170   (Average: 21.71 Max: 1255 Sum: 16743421)
  Executed   : 771027   (Average: 21.70 Max: 1255 Sum: 16734291 Ratio:  99.95%)
  Bounded    : 143      (Average: 63.85 Max: 117 Sum:   9130 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199658  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.62s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 6.69s

Iteration 95
Queue:		 [(4,20,8,True), (5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 96
Time         : 729.522s (Solving: 694.50s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 729.648s

Choices      : 18078479 (Domain: 17798866)
Conflicts    : 778962   (Analyzed: 778959)
Restarts     : 9196     (Average: 84.71 Last: 171)
Model-Level  : 232.0   
Problems     : 96       (Average Length: 90.70 Splits: 0)
Lemmas       : 778959   (Deleted: 742711)
  Binary     : 9718     (Ratio:   1.25%)
  Ternary    : 2416     (Ratio:   0.31%)
  Conflict   : 778959   (Average Length:  433.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 778959   (Average: 21.55 Max: 1255 Sum: 16786341)
  Executed   : 778815   (Average: 21.54 Max: 1255 Sum: 16777210 Ratio:  99.95%)
  Bounded    : 144      (Average: 63.41 Max: 117 Sum:   9131 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199632  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 954MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.33s
Memory:		 864MB (+0MB)
UNKNOWN
Iteration Time:	 4.41s

Iteration 96
Queue:		 [(5,25,8,True), (6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 97
Time         : 735.184s (Solving: 699.99s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 735.312s

Choices      : 18151359 (Domain: 17868891)
Conflicts    : 787251   (Analyzed: 787248)
Restarts     : 9296     (Average: 84.69 Last: 171)
Model-Level  : 232.0   
Problems     : 97       (Average Length: 90.97 Splits: 0)
Lemmas       : 787248   (Deleted: 750207)
  Binary     : 9900     (Ratio:   1.26%)
  Ternary    : 2449     (Ratio:   0.31%)
  Conflict   : 787248   (Average Length:  434.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 787248   (Average: 21.40 Max: 1255 Sum: 16848464)
  Executed   : 787103   (Average: 21.39 Max: 1255 Sum: 16839216 Ratio:  99.95%)
  Bounded    : 145      (Average: 63.78 Max: 117 Sum:   9248 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199632  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.61s
Memory:		 928MB (+64MB)
UNKNOWN
Iteration Time:	 5.67s

Iteration 97
Queue:		 [(6,30,7,True), (7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 98
Time         : 740.519s (Solving: 705.13s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 740.648s

Choices      : 18232293 (Domain: 17948471)
Conflicts    : 795773   (Analyzed: 795770)
Restarts     : 9396     (Average: 84.69 Last: 171)
Model-Level  : 232.0   
Problems     : 98       (Average Length: 91.23 Splits: 0)
Lemmas       : 795770   (Deleted: 757967)
  Binary     : 10039    (Ratio:   1.26%)
  Ternary    : 2478     (Ratio:   0.31%)
  Conflict   : 795770   (Average Length:  432.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 795770   (Average: 21.26 Max: 1255 Sum: 16919453)
  Executed   : 795624   (Average: 21.25 Max: 1255 Sum: 16910093 Ratio:  99.94%)
  Bounded    : 146      (Average: 64.11 Max: 117 Sum:   9360 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.26s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 5.34s

Iteration 98
Queue:		 [(7,35,7,True), (8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 99
Time         : 746.059s (Solving: 710.49s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 746.192s

Choices      : 18312744 (Domain: 18028258)
Conflicts    : 803882   (Analyzed: 803879)
Restarts     : 9496     (Average: 84.65 Last: 171)
Model-Level  : 232.0   
Problems     : 99       (Average Length: 91.49 Splits: 0)
Lemmas       : 803879   (Deleted: 766153)
  Binary     : 10163    (Ratio:   1.26%)
  Ternary    : 2503     (Ratio:   0.31%)
  Conflict   : 803879   (Average Length:  430.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 803879   (Average: 21.14 Max: 1255 Sum: 16991304)
  Executed   : 803733   (Average: 21.13 Max: 1255 Sum: 16981944 Ratio:  99.94%)
  Bounded    : 146      (Average: 64.11 Max: 117 Sum:   9360 Ratio:   0.06%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.48s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 5.55s

Iteration 99
Queue:		 [(8,40,6,True), (9,45,6,False), (10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 100
Time         : 752.945s (Solving: 717.21s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 753.080s

Choices      : 18413605 (Domain: 18127692)
Conflicts    : 812225   (Analyzed: 812222)
Restarts     : 9596     (Average: 84.64 Last: 171)
Model-Level  : 232.0   
Problems     : 100      (Average Length: 91.75 Splits: 0)
Lemmas       : 812222   (Deleted: 774009)
  Binary     : 10330    (Ratio:   1.27%)
  Ternary    : 2531     (Ratio:   0.31%)
  Conflict   : 812222   (Average Length:  429.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 812222   (Average: 21.03 Max: 1255 Sum: 17082239)
  Executed   : 812076   (Average: 21.02 Max: 1255 Sum: 17072879 Ratio:  99.95%)
  Bounded    : 146      (Average: 64.11 Max: 117 Sum:   9360 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.83s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.89s

Iteration 100
Queue:		 [(10,50,5,True), (11,55,5,False), (12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 101
Time         : 761.264s (Solving: 725.36s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 761.400s

Choices      : 18595494 (Domain: 18308080)
Conflicts    : 821264   (Analyzed: 821261)
Restarts     : 9696     (Average: 84.70 Last: 171)
Model-Level  : 232.0   
Problems     : 101      (Average Length: 92.00 Splits: 0)
Lemmas       : 821261   (Deleted: 783859)
  Binary     : 10613    (Ratio:   1.29%)
  Ternary    : 2570     (Ratio:   0.31%)
  Conflict   : 821261   (Average Length:  427.9 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 821261   (Average: 21.01 Max: 1255 Sum: 17250844)
  Executed   : 821114   (Average: 20.99 Max: 1255 Sum: 17241373 Ratio:  99.95%)
  Bounded    : 147      (Average: 64.43 Max: 117 Sum:   9471 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 8.27s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 8.32s

Iteration 101
Queue:		 [(12,60,4,True), (13,65,4,False), (14,70,4,False), (15,75,4,False), (16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 102
Time         : 770.505s (Solving: 734.42s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 770.644s

Choices      : 18918807 (Domain: 18625022)
Conflicts    : 830335   (Analyzed: 830332)
Restarts     : 9796     (Average: 84.76 Last: 171)
Model-Level  : 232.0   
Problems     : 102      (Average Length: 92.25 Splits: 0)
Lemmas       : 830332   (Deleted: 792218)
  Binary     : 10950    (Ratio:   1.32%)
  Ternary    : 2589     (Ratio:   0.31%)
  Conflict   : 830332   (Average Length:  430.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 830332   (Average: 21.14 Max: 1255 Sum: 17551481)
  Executed   : 830185   (Average: 21.13 Max: 1255 Sum: 17542010 Ratio:  99.95%)
  Bounded    : 147      (Average: 64.43 Max: 117 Sum:   9471 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.18s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 9.25s

Iteration 102
Queue:		 [(16,80,3,True), (17,85,3,False), (18,90,3,False), (19,95,3,False), (20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 103
Time         : 777.723s (Solving: 741.45s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 777.864s

Choices      : 19124132 (Domain: 18828510)
Conflicts    : 838825   (Analyzed: 838822)
Restarts     : 9896     (Average: 84.76 Last: 171)
Model-Level  : 232.0   
Problems     : 103      (Average Length: 92.49 Splits: 0)
Lemmas       : 838822   (Deleted: 798859)
  Binary     : 11053    (Ratio:   1.32%)
  Ternary    : 2599     (Ratio:   0.31%)
  Conflict   : 838822   (Average Length:  429.3 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 838822   (Average: 21.15 Max: 1255 Sum: 17741113)
  Executed   : 838675   (Average: 21.14 Max: 1255 Sum: 17731642 Ratio:  99.95%)
  Bounded    : 147      (Average: 64.43 Max: 117 Sum:   9471 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.15s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 7.22s

Iteration 103
Queue:		 [(20,100,2,True), (21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 104
Time         : 788.463s (Solving: 752.00s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 788.612s

Choices      : 19701381 (Domain: 19402290)
Conflicts    : 848031   (Analyzed: 848028)
Restarts     : 9996     (Average: 84.84 Last: 171)
Model-Level  : 232.0   
Problems     : 104      (Average Length: 92.72 Splits: 0)
Lemmas       : 848028   (Deleted: 809121)
  Binary     : 11317    (Ratio:   1.33%)
  Ternary    : 2641     (Ratio:   0.31%)
  Conflict   : 848028   (Average Length:  431.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 848028   (Average: 21.57 Max: 1255 Sum: 18290718)
  Executed   : 847880   (Average: 21.56 Max: 1255 Sum: 18281130 Ratio:  99.95%)
  Bounded    : 148      (Average: 64.78 Max: 117 Sum:   9588 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199618  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 10.67s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 10.75s

Iteration 104
Queue:		 [(21,105,2,True), (22,110,2,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 105
Time         : 795.621s (Solving: 758.99s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 795.772s

Choices      : 19895402 (Domain: 19594792)
Conflicts    : 856218   (Analyzed: 856215)
Restarts     : 10096    (Average: 84.81 Last: 171)
Model-Level  : 232.0   
Problems     : 105      (Average Length: 92.95 Splits: 0)
Lemmas       : 856215   (Deleted: 815791)
  Binary     : 11376    (Ratio:   1.33%)
  Ternary    : 2652     (Ratio:   0.31%)
  Conflict   : 856215   (Average Length:  430.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 856215   (Average: 21.57 Max: 1255 Sum: 18464797)
  Executed   : 856067   (Average: 21.55 Max: 1255 Sum: 18455209 Ratio:  99.95%)
  Bounded    : 148      (Average: 64.78 Max: 117 Sum:   9588 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199592  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.10s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 7.16s

Iteration 105
Queue:		 [(4,20,9,True), (5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 106
Time         : 801.352s (Solving: 764.54s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 801.504s

Choices      : 19944559 (Domain: 19643949)
Conflicts    : 864440   (Analyzed: 864437)
Restarts     : 10196    (Average: 84.78 Last: 171)
Model-Level  : 232.0   
Problems     : 106      (Average Length: 93.18 Splits: 0)
Lemmas       : 864437   (Deleted: 823762)
  Binary     : 11406    (Ratio:   1.32%)
  Ternary    : 2658     (Ratio:   0.31%)
  Conflict   : 864437   (Average Length:  433.5 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 864437   (Average: 21.41 Max: 1255 Sum: 18507477)
  Executed   : 864289   (Average: 21.40 Max: 1255 Sum: 18497889 Ratio:  99.95%)
  Bounded    : 148      (Average: 64.78 Max: 117 Sum:   9588 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199592  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.67s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 5.74s

Iteration 106
Queue:		 [(5,25,9,True), (6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 107
Time         : 805.448s (Solving: 768.47s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 805.600s

Choices      : 19988885 (Domain: 19688274)
Conflicts    : 872178   (Analyzed: 872175)
Restarts     : 10296    (Average: 84.71 Last: 171)
Model-Level  : 232.0   
Problems     : 107      (Average Length: 93.40 Splits: 0)
Lemmas       : 872175   (Deleted: 831768)
  Binary     : 11418    (Ratio:   1.31%)
  Ternary    : 2662     (Ratio:   0.31%)
  Conflict   : 872175   (Average Length:  431.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 872175   (Average: 21.26 Max: 1255 Sum: 18545209)
  Executed   : 872027   (Average: 21.25 Max: 1255 Sum: 18535621 Ratio:  99.95%)
  Bounded    : 148      (Average: 64.78 Max: 117 Sum:   9588 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199592  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.04s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 4.10s

Iteration 107
Queue:		 [(6,30,8,True), (7,35,8,False), (8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 108
Time         : 810.421s (Solving: 773.24s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 810.576s

Choices      : 20037491 (Domain: 19736863)
Conflicts    : 880181   (Analyzed: 880178)
Restarts     : 10396    (Average: 84.67 Last: 171)
Model-Level  : 232.0   
Problems     : 108      (Average Length: 93.62 Splits: 0)
Lemmas       : 880178   (Deleted: 839406)
  Binary     : 11459    (Ratio:   1.30%)
  Ternary    : 2665     (Ratio:   0.30%)
  Conflict   : 880178   (Average Length:  430.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 880178   (Average: 21.12 Max: 1255 Sum: 18585904)
  Executed   : 880030   (Average: 21.11 Max: 1255 Sum: 18576316 Ratio:  99.95%)
  Bounded    : 148      (Average: 64.78 Max: 117 Sum:   9588 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199592  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.90s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 4.98s

Iteration 108
Queue:		 [(8,40,7,True), (9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 109
Time         : 815.883s (Solving: 778.53s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 816.040s

Choices      : 20115050 (Domain: 19813758)
Conflicts    : 888846   (Analyzed: 888843)
Restarts     : 10496    (Average: 84.68 Last: 171)
Model-Level  : 232.0   
Problems     : 109      (Average Length: 93.83 Splits: 0)
Lemmas       : 888843   (Deleted: 849414)
  Binary     : 11526    (Ratio:   1.30%)
  Ternary    : 2672     (Ratio:   0.30%)
  Conflict   : 888843   (Average Length:  429.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 888843   (Average: 20.99 Max: 1255 Sum: 18653657)
  Executed   : 888694   (Average: 20.98 Max: 1255 Sum: 18643952 Ratio:  99.95%)
  Bounded    : 149      (Average: 65.13 Max: 117 Sum:   9705 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199592  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.40s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 5.47s

Iteration 109
Queue:		 [(9,45,6,True), (10,50,6,False), (11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 110
Time         : 821.560s (Solving: 784.04s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 821.720s

Choices      : 20198480 (Domain: 19896292)
Conflicts    : 897392   (Analyzed: 897389)
Restarts     : 10596    (Average: 84.69 Last: 171)
Model-Level  : 232.0   
Problems     : 110      (Average Length: 94.05 Splits: 0)
Lemmas       : 897389   (Deleted: 855689)
  Binary     : 11593    (Ratio:   1.29%)
  Ternary    : 2680     (Ratio:   0.30%)
  Conflict   : 897389   (Average Length:  428.6 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 897389   (Average: 20.87 Max: 1255 Sum: 18724903)
  Executed   : 897239   (Average: 20.86 Max: 1255 Sum: 18715087 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 5.62s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 5.68s

Iteration 110
Queue:		 [(11,55,5,True), (12,60,5,False), (13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 111
Time         : 827.783s (Solving: 790.10s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 827.944s

Choices      : 20306281 (Domain: 20003331)
Conflicts    : 906318   (Analyzed: 906315)
Restarts     : 10696    (Average: 84.73 Last: 171)
Model-Level  : 232.0   
Problems     : 111      (Average Length: 94.25 Splits: 0)
Lemmas       : 906315   (Deleted: 866143)
  Binary     : 11663    (Ratio:   1.29%)
  Ternary    : 2685     (Ratio:   0.30%)
  Conflict   : 906315   (Average Length:  428.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 906315   (Average: 20.76 Max: 1255 Sum: 18819535)
  Executed   : 906165   (Average: 20.75 Max: 1255 Sum: 18809719 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.17s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.23s

Iteration 111
Queue:		 [(13,65,4,True), (14,70,4,False), (15,75,4,False), (16,80,4,False), (17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 112
Time         : 834.747s (Solving: 796.88s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 834.912s

Choices      : 20478106 (Domain: 20173609)
Conflicts    : 915300   (Analyzed: 915297)
Restarts     : 10796    (Average: 84.78 Last: 171)
Model-Level  : 232.0   
Problems     : 112      (Average Length: 94.46 Splits: 0)
Lemmas       : 915297   (Deleted: 874724)
  Binary     : 11740    (Ratio:   1.28%)
  Ternary    : 2693     (Ratio:   0.29%)
  Conflict   : 915297   (Average Length:  428.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 915297   (Average: 20.73 Max: 1255 Sum: 18974143)
  Executed   : 915147   (Average: 20.72 Max: 1255 Sum: 18964327 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.91s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.97s

Iteration 112
Queue:		 [(17,85,3,True), (18,90,3,False), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 113
Time         : 842.427s (Solving: 804.35s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 842.596s

Choices      : 20711753 (Domain: 20405971)
Conflicts    : 923784   (Analyzed: 923781)
Restarts     : 10896    (Average: 84.78 Last: 171)
Model-Level  : 232.0   
Problems     : 113      (Average Length: 94.65 Splits: 0)
Lemmas       : 923781   (Deleted: 881314)
  Binary     : 11799    (Ratio:   1.28%)
  Ternary    : 2694     (Ratio:   0.29%)
  Conflict   : 923781   (Average Length:  428.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 923781   (Average: 20.77 Max: 1255 Sum: 19188706)
  Executed   : 923631   (Average: 20.76 Max: 1255 Sum: 19178890 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 7.61s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 7.69s

Iteration 113
Queue:		 [(22,110,2,True), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 114
Time         : 851.828s (Solving: 813.59s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 851.988s

Choices      : 21189121 (Domain: 20881118)
Conflicts    : 932545   (Analyzed: 932542)
Restarts     : 10996    (Average: 84.81 Last: 171)
Model-Level  : 232.0   
Problems     : 114      (Average Length: 94.85 Splits: 0)
Lemmas       : 932542   (Deleted: 891689)
  Binary     : 11872    (Ratio:   1.27%)
  Ternary    : 2702     (Ratio:   0.29%)
  Conflict   : 932542   (Average Length:  428.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 932542   (Average: 21.06 Max: 1255 Sum: 19640168)
  Executed   : 932392   (Average: 21.05 Max: 1255 Sum: 19630352 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 9.33s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 9.39s

Iteration 114
Queue:		 [(4,20,10,True), (5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Blocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 115
Time         : 858.081s (Solving: 819.64s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 858.244s

Choices      : 21237814 (Domain: 20929811)
Conflicts    : 940422   (Analyzed: 940419)
Restarts     : 11096    (Average: 84.75 Last: 171)
Model-Level  : 232.0   
Problems     : 115      (Average Length: 95.04 Splits: 0)
Lemmas       : 940419   (Deleted: 898064)
  Binary     : 11895    (Ratio:   1.26%)
  Ternary    : 2711     (Ratio:   0.29%)
  Conflict   : 940419   (Average Length:  432.1 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 940419   (Average: 20.93 Max: 1255 Sum: 19683560)
  Executed   : 940269   (Average: 20.92 Max: 1255 Sum: 19673744 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.18s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.26s

Iteration 115
Queue:		 [(5,25,10,True), (6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 116
Time         : 862.634s (Solving: 824.01s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 862.800s

Choices      : 21283934 (Domain: 20975706)
Conflicts    : 948329   (Analyzed: 948326)
Restarts     : 11196    (Average: 84.70 Last: 171)
Model-Level  : 232.0   
Problems     : 116      (Average Length: 95.23 Splits: 0)
Lemmas       : 948326   (Deleted: 905749)
  Binary     : 11918    (Ratio:   1.26%)
  Ternary    : 2716     (Ratio:   0.29%)
  Conflict   : 948326   (Average Length:  430.8 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 948326   (Average: 20.80 Max: 1255 Sum: 19722535)
  Executed   : 948176   (Average: 20.79 Max: 1255 Sum: 19712719 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.49s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 4.56s

Iteration 116
Queue:		 [(6,30,9,True), (7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 117
Time         : 867.156s (Solving: 828.36s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 867.324s

Choices      : 21344350 (Domain: 21035360)
Conflicts    : 956539   (Analyzed: 956536)
Restarts     : 11296    (Average: 84.68 Last: 171)
Model-Level  : 232.0   
Problems     : 117      (Average Length: 95.42 Splits: 0)
Lemmas       : 956536   (Deleted: 913462)
  Binary     : 11977    (Ratio:   1.25%)
  Ternary    : 2720     (Ratio:   0.28%)
  Conflict   : 956536   (Average Length:  429.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 956536   (Average: 20.67 Max: 1255 Sum: 19773460)
  Executed   : 956386   (Average: 20.66 Max: 1255 Sum: 19763644 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 4.47s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 4.53s

Iteration 117
Queue:		 [(7,35,8,True), (8,40,8,False), (9,45,7,False), (10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 118
Time         : 873.554s (Solving: 834.56s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 873.728s

Choices      : 21446233 (Domain: 21135993)
Conflicts    : 965893   (Analyzed: 965890)
Restarts     : 11396    (Average: 84.76 Last: 176)
Model-Level  : 232.0   
Problems     : 118      (Average Length: 95.60 Splits: 0)
Lemmas       : 965890   (Deleted: 923594)
  Binary     : 12124    (Ratio:   1.26%)
  Ternary    : 2726     (Ratio:   0.28%)
  Conflict   : 965890   (Average Length:  430.0 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 965890   (Average: 20.56 Max: 1255 Sum: 19862055)
  Executed   : 965740   (Average: 20.55 Max: 1255 Sum: 19852239 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.32s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.40s

Iteration 118
Queue:		 [(10,50,6,True), (11,55,6,False), (12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 119
Time         : 880.387s (Solving: 841.21s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 880.564s

Choices      : 21576988 (Domain: 21265977)
Conflicts    : 974504   (Analyzed: 974501)
Restarts     : 11496    (Average: 84.77 Last: 176)
Model-Level  : 232.0   
Problems     : 119      (Average Length: 95.78 Splits: 0)
Lemmas       : 974501   (Deleted: 932636)
  Binary     : 12188    (Ratio:   1.25%)
  Ternary    : 2732     (Ratio:   0.28%)
  Conflict   : 974501   (Average Length:  430.4 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 974501   (Average: 20.50 Max: 1255 Sum: 19978233)
  Executed   : 974351   (Average: 20.49 Max: 1255 Sum: 19968417 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.77s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 6.84s

Iteration 119
Queue:		 [(12,60,5,True), (13,65,5,False), (14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
[start: stats after solve call]

Models       : 0+
Calls        : 120
Time         : 887.424s (Solving: 848.08s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 887.604s

Choices      : 21753795 (Domain: 21441284)
Conflicts    : 983478   (Analyzed: 983475)
Restarts     : 11596    (Average: 84.81 Last: 176)
Model-Level  : 232.0   
Problems     : 120      (Average Length: 95.96 Splits: 0)
Lemmas       : 983475   (Deleted: 941030)
  Binary     : 12258    (Ratio:   1.25%)
  Ternary    : 2742     (Ratio:   0.28%)
  Conflict   : 983475   (Average Length:  430.2 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 983475   (Average: 20.48 Max: 1255 Sum: 20139125)
  Executed   : 983325   (Average: 20.47 Max: 1255 Sum: 20129309 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1

[endof: stats after solve call]
Solving Time:	 6.99s
Memory:		 928MB (+0MB)
UNKNOWN
Iteration Time:	 7.04s

Iteration 120
Queue:		 [(14,70,4,True), (15,75,4,False), (16,80,4,False), (17,85,4,False), (18,90,3,True), (19,95,3,False), (20,100,3,False), (21,105,3,False), (22,110,3,False), (23,115,2,False)]
Grounded Until:	 115
Unblocking actions...
Solving...
*** Info : (planner): INTERRUPTED by signal!
UNKNOWN

INTERRUPTED  : 1

Models       : 0+
Calls        : 121
Time         : 892.630s (Solving: 853.08s 1st Model: 0.05s Unsat: 4.31s)
CPU Time     : 892.792s

Choices      : 21924673 (Domain: 21611322)
Conflicts    : 989110   (Analyzed: 989107)
Restarts     : 11656    (Average: 84.86 Last: 176)
Model-Level  : 232.0   
Problems     : 121      (Average Length: 96.13 Splits: 0)
Lemmas       : 989107   (Deleted: 945509)
  Binary     : 12327    (Ratio:   1.25%)
  Ternary    : 2742     (Ratio:   0.28%)
  Conflict   : 989107   (Average Length:  430.7 Ratio: 100.00%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 0        (Average Length:    0.0 Ratio:   0.00%) 
Backjumps    : 989107   (Average: 20.52 Max: 1255 Sum: 20298469)
  Executed   : 988957   (Average: 20.51 Max: 1255 Sum: 20288653 Ratio:  99.95%)
  Bounded    : 150      (Average: 65.44 Max: 117 Sum:   9816 Ratio:   0.05%)

Rules        : 150283   (Original: 135818)
Atoms        : 72365   
Bodies       : 65513    (Original: 51047)
  Count      : 841      (Original: 2348)
Equivalences : 15742    (Atom=Atom: 82 Body=Body: 0 Other: 15660)
Tight        : Yes
Variables    : 843565   (Eliminated:    0 Frozen: 260681)
Constraints  : 6199578  (Binary:  91.2% Ternary:   7.0% Other:   1.8%)

Memory Peak  : 992MB
Max. Length  : 115 steps
Models       : 1